YEAH

diff --git a/documentation b/documentation
index 269e93139c744f83508a076206088f76e7634b81..d649bbaedbe29fe03f586ac9699b30c70b0f4348 100644 (file)
--- a/documentation
+++ b/documentation
@@ -16,7 +16,6 @@ typing rules
 (t is little tau, T is large tau, E is 'in', and + is that other symbol)
 
 
-
 [Eq, Neq]
 
 e:bool  <=  e1:t  &  e2:t

diff --git a/formalsemantics b/formalsemantics
new file mode 100644 (file)
index 0000000..a94c4db
--- /dev/null
+++ b/formalsemantics
@@ -0,0 +1,86 @@
+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''

diff --git a/syntax.cf b/syntax.cf
index d09a25c33849d524632a0b352994da59b2cf60b6..7b84054391014ef81d22f0f03d8e8866af3049ce 100644 (file)
--- a/syntax.cf
+++ b/syntax.cf
@@ -1,40 +1,53 @@
 
 -- 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 ;
 
 
@@ -43,7 +56,6 @@ coercions Exp 3 ;
 
 terminator Stm "" ;
 
-Program.  Stms ::= [Stm] ;
 
 Lt.  Op0 ::= "<" ;
 ELt. Op0 ::= "<=" ;
@@ -62,6 +74,8 @@ _. Op ::= Op2;
 _. Op ::= Op0;
 
 
+True.    Bool ::= "true" ;
+False.   Bool ::= "false" ;
 
 TInt.   Type  ::= "int" ;
 TBool.  Type  ::= "bool" ;