--- /dev/null
+INTERPOL - ANTICS
++++++++++++++++++
+
+
+
+<e,o> |> v means that e evaluates to v in the state o.
+
+
+
+
+basic arithmetic operations.
+
+(PLUS)
+<e1 + e2, o> |> v <= <e1,o> |> v1 & <e2,o> |> v2 & v is the sum of v1 and v2
+
+
+(MINUS)
+<e1 - e2, o> |> v <= <e1,o> |> v1 & <e2,o> |> v2 & v is v1 subtracted from v2
+
+
+(MULT)
+<e1 * e2, o> |> v <= <e1,o> |> v1 & <e2,o> |> v2 & v is the product of v1 and v2
+
+
+(DIV)
+<e1 / e2, o> |> v <= <e1,o> |> v1 & <e2,o> |> v2 & v is v1 divided by v2
+
+
+
+basic comparative operations.
+
+
+(Less Than)
+
+<e1 < e2, o> |> true <= <e1,o> |> v1 & <e2,o> |> v2 & v1 is smaller than v2
+<e1 < e2, o> |> false <= <e1,o> |> v1 & <e2,o> |> v2 & v1 is larger than or as large as v2
+
+<e1 <= e2, o> |> true <= <e1,o> |> v1 & <e2,o> |> v2 & v1 is smaller than or as small as v2
+<e1 <= e2, o> |> false <= <e1,o> |> v1 & <e2,o> |> v2 & v1 is larger than v2
+
++similar rules apply for greater than+
+
+
+(Equal, Not Equal)
+
+<e1 == e2, o> |> true <= <e1,o> |> v1 & <e2,o> |> v2 & v1 is equal to v2
+<e1 == e2, o> |> false <= <e1,o> |> v1 & <e2,o> |> v2 & v1 is not equal to v2
+
+<e1 != e2, o> |> true <= <e1,o> |> v1 & <e2,o> |> v2 & v1 is not equal to to v2
+<e1 != e2, o> |> false <= <e1,o> |> v1 & <e2,o> |> v2 & v1 is equal to v2
+
+
+
+(Not, Neg)
+
+<!e, o> |> false <= <e,o> |> true
+<!e, o> |> true <= <e,o> |> false
+
+<-e, o> |> v2 <= <e,o> |> v1 & v2 is the negative value of v1
+
+
+
+
+(Int)
+<n,o> |> n <=
+
+(Bool)
+<b,o> |> b <=
+
+
+
+
+
+(If)
+<if e s1 else s2, o> |> o' <= <e,o> |> true & <s1, o> |> o'
+<if e s1 else s2, o> |> o' <= <e,o> |> false & <s2, o> |> o'
+
+(While)
+<while e s, o> |> o'' <= <e,o> |> true & <s,o> |> o' & <while e s, o'> |> o''
+<while e s, o> |> o <= <e,o> |> false
+
+(Assign)
+<x = e, o> |> o[x->v] <= <e,o> |> v
+
+(Seq)
+<s1; s2, o> |> o'' <= <s1,o> |> o' & <s2, o'> |> o''
-- ordinary rules
-True. Bool ::= "true" ;
-False. Bool ::= "false" ;
+Program. Stms ::= [Stm] ;
+
+SExp. Stm ::= Exp ";" ;
+SBlock. Stm ::= "{" [Stm] "}" ;
SDecl. Stm ::= Type Ident "=" Exp ";" ;
decl. Stm ::= Type Ident ";" ;
define decl t v = SDecl t v EDefault ;
-SExp. Stm ::= Exp ";" ;
-SBlock. Stm ::= "{" [Stm] "}" ;
-if. Stm ::= "if" "(" Exp ")" Stm ;
+
+SWhile. Stm ::= "while" "(" Exp ")" Stm ;
SIf. Stm ::= "if" "(" Exp ")" Stm "else" Stm ;
+if. Stm ::= "if" "(" Exp ")" Stm ;
define if e s = SIf e s SNoop ;
-SWhile. Stm ::= "while" "(" Exp ")" Stm ;
+
-- SFor. Stm ::= "for" "(" Stm Exp ";" Exp ")" Stm ;
SPrint. Stm ::= "print" Exp ";" ;
+
+
EAss. Exp ::= Ident "=" Exp;
+
compExp. Exp ::= Exp1 Op0 Exp1 ;
define compExp e1 o e2 = BiOpExp e1 o e2 ;
+
op1. Exp1 ::= Exp1 Op1 Exp2 ;
define op1 e1 o e2 = BiOpExp e1 o e2 ;
+
op2. Exp2 ::= Exp2 Op2 Exp3 ;
define op2 e1 o e2 = BiOpExp e1 o e2 ;
+
postIncr. Exp3 ::= Ident "++" ;
define postIncr i = EPost i Plus ;
+
postDecr. Exp3 ::= Ident "--" ;
define postDecr i = EPost i Minus ;
+
EVar. Exp3 ::= Ident ;
EInt. Exp3 ::= Integer ;
+EBool. Exp3 ::= Bool ;
+
ENeg. Exp3 ::= "-" Exp3 ;
ENot. Exp3 ::= "!" Exp3 ;
-EBool. Exp3 ::= Bool ;
+
EReadI. Exp3 ::= "readInt" ;
EReadB. Exp3 ::= "readBool" ;
+
coercions Exp 3 ;
terminator Stm "" ;
-Program. Stms ::= [Stm] ;
Lt. Op0 ::= "<" ;
ELt. Op0 ::= "<=" ;
_. Op ::= Op0;
+True. Bool ::= "true" ;
+False. Bool ::= "false" ;
TInt. Type ::= "int" ;
TBool. Type ::= "bool" ;