pi-denotations-for-imp.md

Π denotations for ImΠ

Christiano Braga
Universidade Federal Fluminense
http://www.ic.uff.br/~cbraga

July 2019

http://github.com/ChristianoBraga/PiFramework

Introduction

A compiler for the ImΠ language is defined by means of functions mapping constructions from the ImΠ language to Π IR.

ImΠ grammar

<S> ::=  <cmd>

<cmd> ::= 'nop' | <let> | <assign> | <loop> | <call>

<call> ::= <identifier> '(' <actual> ')' 

<actual> ::= <expression> (',' <expression>)* | ε

<loop> ::= 'while' <expression> 'do' <cmd>+ 

<assign> ::= <identifier> ':=' <expression>

<let> ::= 'let' <dec> 'in' <cmd>+  

<dec> ::= <const> | <var> | <fn>
    
<const> ::= 'const' <identifier> '=' <expression>

<var> ::= 'var' <identifier> '=' <expression>

<fn> ::= 'fn' <identifier> '(' <formal> ')' '=' <cmd>

<formal> ::= <identifier> (',' <identifier>)*  | ε

<expression> ::= <bool_expression> | <arith_expression>

<bool_expression> ::= <negation> | <equality> | <conjunction> | <disjunction>
                | <lowereq> | <greatereq> | <lowerthan> | <greaterthan> 
                
<equality> ::= <arith_expression> "==" <expression>

<conjunction> ::= <bool_expression> "and" <bool_expression>

<disjunction> ::= <bool_expression> "or" <bool_expression>

<lowereq> ::= <arith_expression> "<=" <arith_expression>

<greatereq> ::= <arith_expression> ">=" <arith_expression>

<lowerthan> ::= <arith_expression> "<" <arith_expression>

<greaterthan> ::= <arith_expression> ">" <arith_expression>

<parentesisexp> ::= '(' <bool_expression> ')' 

<negation> ::= 'not' <bool_expression> 

<arith_expression> ::= <addition> | <subtraction> | <mult_expression> | <division>

<addition> ::= <mult_expression> "+" <arith_expression>

<subtraction> ::= <mult_expression> "-" <arith_expression>

<mult_expression> ::= <multiplication> | <division> | <atom> | <parentesisexp> 

<multiplication> ::= <atom> "*" <mult_expression>

<division> ::= <atom> "/" <mult_expression>

<atom> ::= <number> | <truth> | <identifier>
 
<number> ::= /\d+/ 

<identifier> ::= /(?!\d)\w+/ 

<truth> ::= 'True' | 'False' 

ImΠ examples

# The classic iterative factorial example
let var z = 1 
in 
    let var y = 10 
    in 
        while not (y == 0)
        do 
            z := z * y
            y := y - 1

# In this example we encapsulate the iterative calculation
# of the factorial within a function call.
let var z = 1
in 
    let fn f(x) =    
        let var y = x
        in      
            while not (y == 0)
            do 
                z := z * y
                y := y - 1
in f(10)

Π denotations

A Π denotation for the ImΠ language is a function

⟦⋅⟧ : Gimp → GΠ,

intentionally defined, that associates (a class of) words derivable by ImΠ's grammar with (a class of words) words derivable by Π IR grammar.

Expressions

Let ast ∈ L(Gimp),

1. ⟦ identifier(ast) ⟧ = Id(str(ast)), where function str returns a string given an <identifier>.

2. ⟦ number(ast) ⟧ = Num(int(ast)), where function int returns an integer given a <number>.

3. ⟦ addition(ast) ⟧ = Sum( ⟦ left(ast) ⟧, ⟦ right(ast) ⟧), where functions left and right return the left branch and right branches of ast, respectively.

4. ⟦ subtraction(ast) ⟧ = Sub(⟦ left(ast) ⟧, ⟦ right(ast) ⟧)

5. ⟦ multiplication(ast) ⟧ = Mul(⟦ left(ast) ⟧, ⟦ right(ast) ⟧)

6. ⟦ division(ast) ⟧ = Div(⟦ left(ast) ⟧, ⟦ right(ast) ⟧)

7. ⟦ truth(ast) ⟧ = Boo(bool(ast)), where function bool returns a Boolean value given a <truth> token.

8. ⟦ negation(ast) ⟧ = Not( ⟦ ast ⟧ )

9. ⟦ equality(ast) ⟧ = Eq(⟦ left(ast) ⟧, ⟦ right(ast) ⟧)

10. ⟦ lowerthan(ast) ⟧ = Lt(⟦ left(ast) ⟧, ⟦ right(ast) ⟧)

11. ⟦ greaterthan(ast) ⟧ = Gt(⟦ left(ast) ⟧, ⟦ right(ast) ⟧)

12. ⟦ lowereq(ast) ⟧ = Le⟦ left(ast) ⟧, ⟦ right(ast) ⟧)

13. ⟦ greatereq(ast) ⟧ = Ge(⟦ left(ast) ⟧, ⟦ right(ast) ⟧)

14. ⟦ conjunction(ast) ⟧ = And(⟦ left(ast) ⟧, ⟦ right(ast) ⟧)

15. ⟦ disconjunction(ast) ⟧ = Or(⟦ left(ast) ⟧, ⟦ right(ast) ⟧)

16. ⟦ nop(ast) ⟧ = Nop

Declarations

Let _mkAbs : <formal> × <cmd> → <Abs> be

mkAbs([], c) = Abs([], ⟦ c ⟧) mkAbs(h :: ls, b) = Abs(⟦ h ⟧ :: mkFor(ls), ⟦ c ⟧)

and mkFor : <identifier>* → <Id>*

_mkFor([]) = []
mkFor(h :: ls) = ⟦ h ⟧ :: mkFor(ls)

1. ⟦ var(ast) ⟧ = Bind(⟦ left(ast) ⟧, Ref(⟦ right(ast) ⟧))

2. ⟦ const(ast) ⟧ = Bind(⟦ left(ast) ⟧, ⟦ right(ast) ⟧)

3. ⟦ fn(ast) ⟧ = Bind(⟦ fst(ast) ⟧, mkAbs(snd(ast), trd(ast))

4. ⟦ rfn(ast) ⟧ = Rbnd(⟦ fst(ast) ⟧, mkAbs(snd(ast), trd(ast))

Commands

Let mkCSeq : <cmd>+ → <CSeq> be defined by the following equations,

mkCSeq([h]) = h,
mkCSeq(h::ls) = CSeq(⟦ h ⟧ , mkCSeq(ls)),

and mkAct : <actual> → <Exp>* be as follows

mkAct([]) = [],
mkAct(h::ls) = ⟦ h ⟧ :: mkAct(ls)).

1. ⟦ assign(ast) ⟧ = Assign(⟦ left(ast) ⟧, ⟦ right(ast) ⟧)

2. ⟦ let(ast) ⟧ = Blk(⟦ left(ast) ⟧, ⟦ right(ast) ⟧), if _right(ast) ∈ <cmd>

3. ⟦ let(ast) ⟧ = Blk(⟦ left(ast) ⟧, mkCSeq(right(ast))), if right(ast) ∈ <cmd>+

4. ⟦ loop(ast) ⟧ = Loop(⟦ left(ast) ⟧, ⟦ right(ast) ⟧), if right(ast) ∈ <cmd>

5. ⟦ loop(ast) ⟧ = Loop(⟦ left(ast) ⟧, mkCSeq(right(ast))), if right(ast) ∈ <cmd>+

6. ⟦ call(ast) ⟧ = Call(⟦ left(ast) ⟧, mkAct(right(ast)))

Example application of Π denotations for ImΠ

• For the iteractive factorial:

Π IR AST: Blk(Bind(Id(z), Ref(Num(1))), 
            Blk(Bind(Id(y), Ref(Num(10))), 
                Loop(Not(Eq(Id(y), Num(0))), 
                     CSeq(Assign(Id(z), Mul(Id(z), Id(y))), 
                          Assign(Id(y), Sub(Id(y), Num(1)))))))

• For the functional factorial:

Π IR AST: Blk(Bind(Id(z), Ref(Num(1))), 
            Blk(Bind(Id(f), 
                        Abs(Id(x), 
                            Blk(Bind(Id(y), Ref(Id(x))), 
                                Loop(Not(Eq(Id(y), Num(0))), 
                                     CSeq(Assign(Id(z), Mul(Id(z), Id(y))), 
                                          Assign(Id(y), Sub(Id(y), Num(1)))))))), 
                Call(Id(f), [Num(10)])))