remove Pn from Transition

src/Parse.y

@@ -163,7 +163,7 @@ Transition : 'behaviour' id 'of' id
              Interface
              list(Precondition)
              Cases
-             Ensures                                  { Transition (posn $2) (name $2) (name $4)
+             Ensures                                  { Transition (name $2) (name $4)
                                                         $5 $6 $7 $8 }
 
 Constructor : 'constructor' 'of' id
@@ -305,6 +305,7 @@ Expr : '(' Expr ')'                                   { $2 }
 {
 
 nowhere = AlexPn 0 0 0
+
 lastPos = AlexPn (-1) (-1) (-1)
 
 validsize :: Int -> Bool

src/Syntax/Untyped.hs

@@ -22,7 +22,7 @@ newtype Act = Main [RawBehaviour]
   deriving (Eq, Show)
 
 data RawBehaviour
-  = Transition Pn Id Id Interface [IffH] Cases Ensures
+  = Transition Id Id Interface [IffH] Cases Ensures
   | Definition Pn Id Interface [IffH] Creates [ExtStorage] Ensures Invariants
   deriving (Eq, Show)
 

src/Type.hs

@@ -118,7 +118,7 @@ mkEnv contract store decls = Env
 
 -- checks a transition given a typing of its storage variables
 splitBehaviour :: Store -> U.RawBehaviour -> Err [Claim]
-splitBehaviour store (U.Transition _ name contract iface@(Interface _ decls) iffs cases posts) =
+splitBehaviour store (U.Transition name contract iface@(Interface _ decls) iffs cases posts) =
   noIllegalWilds *>
   -- constrain integer calldata variables (TODO: other types)
   fmap concatMap (caseClaims

tests/frontend/pass/array/array.act.parsed.hs

@@ -1 +1 @@
-[Transition (AlexPn 10 1 11) "f" "A" f(address[2] xs) [] (Direct (Post [] [] (Just (EUTEntry (AlexPn 53 4 9) "xs" [IntLit (AlexPn 56 4 12) 1])))) []]
+[Transition "f" "A" f(address[2] xs) [] (Direct (Post [] [] (Just (EUTEntry (AlexPn 53 4 9) "xs" [IntLit (AlexPn 56 4 12) 1])))) []]

tests/frontend/pass/creation/createMultiple.act.parsed.hs

@@ -1 +1 @@
-[Definition (AlexPn 15 1 16) "B" constructor() [] (Creates [AssignVal (StorageVar (AlexPn 60 5 11) address "a") (IntLit (AlexPn 65 5 16) 0)]) [] [] [],Transition (AlexPn 78 7 11) "create_a" "B" create_a() [Iff (AlexPn 114 10 1) [EEq (AlexPn 131 11 14) (EnvExp (AlexPn 121 11 4) Callvalue) (IntLit (AlexPn 134 11 17) 0)]] (Direct (Post [Rewrite (PEntry (AlexPn 148 14 4) "a" []) (ENewaddr (AlexPn 153 14 9) (EnvExp (AlexPn 161 14 17) This) (EnvExp (AlexPn 167 14 23) Nonce))] [ExtCreates "A" (ENewaddr (AlexPn 239 17 14) (EnvExp (AlexPn 247 17 22) This) (EnvExp (AlexPn 253 17 28) Nonce)) [AssignVal (StorageVar (AlexPn 268 18 9) uint256 "x") (IntLit (AlexPn 273 18 14) 1)]] Nothing)) []]
+[Definition (AlexPn 15 1 16) "B" constructor() [] (Creates [AssignVal (StorageVar (AlexPn 60 5 11) address "a") (IntLit (AlexPn 65 5 16) 0)]) [] [] [],Transition "create_a" "B" create_a() [Iff (AlexPn 114 10 1) [EEq (AlexPn 131 11 14) (EnvExp (AlexPn 121 11 4) Callvalue) (IntLit (AlexPn 134 11 17) 0)]] (Direct (Post [Rewrite (PEntry (AlexPn 148 14 4) "a" []) (ENewaddr (AlexPn 153 14 9) (EnvExp (AlexPn 161 14 17) This) (EnvExp (AlexPn 167 14 23) Nonce))] [ExtCreates "A" (ENewaddr (AlexPn 239 17 14) (EnvExp (AlexPn 247 17 22) This) (EnvExp (AlexPn 253 17 28) Nonce)) [AssignVal (StorageVar (AlexPn 268 18 9) uint256 "x") (IntLit (AlexPn 273 18 14) 1)]] Nothing)) []]

tests/frontend/pass/multi/multi.act.parsed.hs

@@ -1 +1 @@
-[Definition (AlexPn 15 1 16) "a" constructor() [] (Creates [AssignVal (StorageVar (AlexPn 58 5 9) uint256 "x") (IntLit (AlexPn 63 5 14) 0)]) [] [] [],Definition (AlexPn 81 7 16) "B" constructor() [] (Creates [AssignVal (StorageVar (AlexPn 124 11 9) uint256 "y") (IntLit (AlexPn 129 11 14) 0)]) [] [] [],Transition (AlexPn 143 14 11) "remote" "B" set_remote(uint256 z) [Iff (AlexPn 185 17 1) [EEq (AlexPn 202 18 14) (EnvExp (AlexPn 192 18 4) Callvalue) (IntLit (AlexPn 205 18 17) 0)]] (Direct (Post [] [ExtStorage "a" [Rewrite (PEntry (AlexPn 373 24 4) "x" []) (EUTEntry (AlexPn 378 24 9) "z" [])]] Nothing)) [],Transition (AlexPn 391 26 11) "multi" "B" set_remote(uint256 z) [Iff (AlexPn 432 29 1) [EEq (AlexPn 449 30 14) (EnvExp (AlexPn 439 30 4) Callvalue) (IntLit (AlexPn 452 30 17) 0)]] (Direct (Post [Rewrite (PEntry (AlexPn 520 34 4) "y" []) (IntLit (AlexPn 525 34 9) 1)] [ExtStorage "a" [Rewrite (PEntry (AlexPn 544 37 4) "x" []) (EUTEntry (AlexPn 549 37 9) "z" [])]] Nothing)) []]
+[Definition (AlexPn 15 1 16) "a" constructor() [] (Creates [AssignVal (StorageVar (AlexPn 58 5 9) uint256 "x") (IntLit (AlexPn 63 5 14) 0)]) [] [] [],Definition (AlexPn 81 7 16) "B" constructor() [] (Creates [AssignVal (StorageVar (AlexPn 124 11 9) uint256 "y") (IntLit (AlexPn 129 11 14) 0)]) [] [] [],Transition "remote" "B" set_remote(uint256 z) [Iff (AlexPn 185 17 1) [EEq (AlexPn 202 18 14) (EnvExp (AlexPn 192 18 4) Callvalue) (IntLit (AlexPn 205 18 17) 0)]] (Direct (Post [] [ExtStorage "a" [Rewrite (PEntry (AlexPn 373 24 4) "x" []) (EUTEntry (AlexPn 378 24 9) "z" [])]] Nothing)) [],Transition "multi" "B" set_remote(uint256 z) [Iff (AlexPn 432 29 1) [EEq (AlexPn 449 30 14) (EnvExp (AlexPn 439 30 4) Callvalue) (IntLit (AlexPn 452 30 17) 0)]] (Direct (Post [Rewrite (PEntry (AlexPn 520 34 4) "y" []) (IntLit (AlexPn 525 34 9) 1)] [ExtStorage "a" [Rewrite (PEntry (AlexPn 544 37 4) "x" []) (EUTEntry (AlexPn 549 37 9) "z" [])]] Nothing)) []]

tests/frontend/pass/safemath/safemathraw.act.parsed.hs

@@ -1 +1 @@
-[Transition (AlexPn 10 1 11) "add" "SafeAdd" add(uint256 x, uint256 y) [IffIn (AlexPn 62 4 1) uint256 [EAdd (AlexPn 90 6 7) (EUTEntry (AlexPn 88 6 5) "x" []) (EUTEntry (AlexPn 92 6 9) "y" [])],Iff (AlexPn 95 8 1) [EEq (AlexPn 114 10 15) (EnvExp (AlexPn 104 10 5) Callvalue) (IntLit (AlexPn 117 10 18) 0)]] (Direct (Post [] [] (Just (EAdd (AlexPn 130 12 11) (EUTEntry (AlexPn 128 12 9) "x" []) (EUTEntry (AlexPn 132 12 13) "y" []))))) []]
+[Transition "add" "SafeAdd" add(uint256 x, uint256 y) [IffIn (AlexPn 62 4 1) uint256 [EAdd (AlexPn 90 6 7) (EUTEntry (AlexPn 88 6 5) "x" []) (EUTEntry (AlexPn 92 6 9) "y" [])],Iff (AlexPn 95 8 1) [EEq (AlexPn 114 10 15) (EnvExp (AlexPn 104 10 5) Callvalue) (IntLit (AlexPn 117 10 18) 0)]] (Direct (Post [] [] (Just (EAdd (AlexPn 130 12 11) (EUTEntry (AlexPn 128 12 9) "x" []) (EUTEntry (AlexPn 132 12 13) "y" []))))) []]

tests/frontend/pass/smoke/smoke.act.parsed.hs

@@ -1 +1 @@
-[Transition (AlexPn 10 1 11) "f" "A" f(uint256 x) [] (Direct (Post [] [] (Just (IntLit (AlexPn 46 4 9) 1)))) []]
+[Transition "f" "A" f(uint256 x) [] (Direct (Post [] [] (Just (IntLit (AlexPn 46 4 9) 1)))) []]

tests/frontend/pass/staticstore/staticstore.act.parsed.hs

@@ -1 +1 @@
-[Transition (AlexPn 10 1 11) "f" "C" f() [IffIn (AlexPn 32 4 1) uint256 [EAdd (AlexPn 60 6 7) (EUTEntry (AlexPn 58 6 5) "x" []) (EUTEntry (AlexPn 62 6 9) "y" [])]] (Direct (Post [Constant (PEntry (AlexPn 78 10 5) "x" []),Constant (PEntry (AlexPn 85 11 5) "y" [])] [] (Just (EAdd (AlexPn 98 13 11) (EUTEntry (AlexPn 96 13 9) "x" []) (EUTEntry (AlexPn 100 13 13) "y" []))))) []]
+[Transition "f" "C" f() [IffIn (AlexPn 32 4 1) uint256 [EAdd (AlexPn 60 6 7) (EUTEntry (AlexPn 58 6 5) "x" []) (EUTEntry (AlexPn 62 6 9) "y" [])]] (Direct (Post [Constant (PEntry (AlexPn 78 10 5) "x" []),Constant (PEntry (AlexPn 85 11 5) "y" [])] [] (Just (EAdd (AlexPn 98 13 11) (EUTEntry (AlexPn 96 13 9) "x" []) (EUTEntry (AlexPn 100 13 13) "y" []))))) []]