# Syntax: Change rewrite arrow to <-

src/Act/Lex.x

@@ -90,6 +90,7 @@ tokens :-
   -- symbols
   ":="                                  { mk ASSIGN }
   "=>"                                  { mk ARROW }
+  "<-"                                  { mk LARROW }
   "|->"                                 { mk POINTSTO }
   "=="                                  { mk EQEQ }
   "=/="                                 { mk NEQ }
@@ -186,6 +187,8 @@ data LEX =
   -- symbols
   | ASSIGN
   | ARROW
+  | LARROW
+  | POINTSTO
   | EQEQ
   | NEQ
   | GE

src/Act/Parse.y

@@ -77,6 +77,7 @@ import Act.Error
   -- symbols
   ':='                        { L ASSIGN _ }
   '=>'                        { L ARROW _ }
+  '<-'                        { L LARROW _ }
   '|->'                       { L POINTSTO _ }
   '=='                        { L EQEQ _ }
   '=/='                       { L NEQ _ }
@@ -209,7 +210,7 @@ Storage : 'storage' nonempty(Store)                   { $2 }
 Precondition : 'iff' nonempty(Expr)                   { Iff (posn $1) $2 }
              | 'iff in range' AbiType nonempty(Expr)  { IffIn (posn $1) $2 $3 }
 
-Store : Entry '=>' Expr                               { Rewrite $1 $3 }
+Store : Entry '<-' Expr                               { Rewrite $1 $3 }
 
 Entry : id                                            { EVar (posn $1) (name $1) }
       | Entry '[' Expr ']' list(Index)                { EMapping (posn $2) $1 ($3:$5) }

src/Act/Print.hs

@@ -165,7 +165,7 @@ prettyLocation :: StorageLocation t -> String
 prettyLocation (Loc _ item) = prettyItem item
 
 prettyUpdate :: StorageUpdate t -> String
-prettyUpdate (Update _ item e) = prettyItem item <> " => " <> prettyExp e
+prettyUpdate (Update _ item e) = prettyItem item <> " <- " <> prettyExp e
 
 prettyEnv :: EthEnv -> String
 prettyEnv e = case e of

tests/postconditions/pass/assignment_poststate.act

@@ -0,0 +1,14 @@
+constructor of C
+interface constructor(uint x0)
+
+creates
+
+  uint x := x0
+
+behaviour f of C
+interface f()
+
+storage
+  x <- post(x)
+
+returns post(x) 

tests/postconditions/pass/assignment_prestate.act

@@ -1,17 +1,14 @@
 constructor of C
-interface constructor(uint24 _x)
+interface constructor(uint x0)
 
 creates
 
-  uint24 x := _x
+  uint x := x0
 
 behaviour f of C
-interface f(uint24 y)
+interface f()
 
 storage
+  x <- pre(x)
 
-  x => x + y
-
-ensures
-
-  post(x) == pre(x) + y
+returns pre(x)

tests/postconditions/pass/increase.act

@@ -10,13 +10,13 @@ interface increase(uint24 new_x)
 
 case new_x > x:
   storage
-    x => new_x
+    x <- new_x
 
   returns post(x) - pre(x)
 
 case new_x <= x:
   storage
-    x => x + new_x
+    x <- x + new_x
 
   returns post(x) - pre(x)