Skip to content

Commit 93d7fe6

Browse files
zoepzoep
committed
Syntax: Cleanup untyped AST
1 parent b34eced commit 93d7fe6

File tree

5 files changed

+80
-103
lines changed

5 files changed

+80
-103
lines changed

‎src/Act/Parse.y‎

Lines changed: 11 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,6 @@ import Act.Error
2626
'returns' { L RETURNS _ }
2727
'storage' { L STORAGE _ }
2828
'noop' { L NOOP _ }
29-
'iff in range' { L IFFINRANGE _ }
3029
'inRange' { L INRANGE _ }
3130
'iff' { L IFF _ }
3231
'pointers' { L POINTERS _ }
@@ -166,18 +165,18 @@ Contract : Constructor list(Transition) { Contract $1 $2 }
166165
Transition : 'behaviour' id 'of' id
167166
Interface
168167
Pointers
169-
list(Precondition)
168+
Precondition
170169
Cases
171170
Ensures { Transition (posn $1) (name $2) (name $4)
172171
$5 $6 $7 $8 $9 }
173172

174173
Constructor : 'constructor' 'of' id
175174
CInterface
176175
Pointers
177-
list(Precondition)
176+
Precondition
178177
Creation
179178
Ensures
180-
Invariants { Definition (posn $3) (name $3)
179+
Invariants { Constructor (posn $3) (name $3)
181180
$4 $5 $6 $7 $8 $9 }
182181

183182
Ensures : optblock('ensures', Expr) { $1 }
@@ -192,7 +191,7 @@ CInterface : 'interface' 'constructor' '(' seplist(Decl, ',') ')' { Interface "c
192191

193192
Pointer : id '|->' id { PointsTo (posn $2) (name $1) (name $3) }
194193

195-
Cases : Post { Direct $1 }
194+
Cases : Post { Branches [Case nowhere (BoolLit nowhere True) $1] }
196195
| nonempty(Case) { Branches $1 }
197196

198197
Case : 'case' Expr ':' Post { Case (posn $1) $2 $4 }
@@ -206,10 +205,9 @@ Returns : 'returns' Expr { $2 }
206205

207206
Storage : 'storage' nonempty(Store) { $2 }
208207

209-
Precondition : 'iff' nonempty(Expr) { Iff (posn $1) $2 }
210-
| 'iff in range' AbiType nonempty(Expr) { IffIn (posn $1) $2 $3 }
208+
Precondition : 'iff' nonempty(Expr) { $2 }
211209

212-
Store : Entry '=>' Expr { Rewrite $1 $3 }
210+
Store : Entry '=>' Expr { Update $1 $3 }
213211

214212
Entry : id { EVar (posn $1) (name $1) }
215213
| Entry '[' Expr ']' list(Index) { EMapping (posn $2) $1 ($3:$5) }
@@ -221,9 +219,10 @@ Index : '[' Expr ']' { $2 }
221219
Creation : optblock('creates',Assign) { Creates $1 }
222220

223221
Assign : StorageVar ':=' Expr { AssignVal $1 $3 }
224-
| StorageVar ':=' '[' seplist(Defn, ',') ']' { AssignMany $1 $4 }
222+
| StorageVar ':=' '[' seplist(Defn, ',') ']' { AssignMapping $1 $4 }
223+
224+
Defn : Expr ':=' Expr { Mapping $1 $3 }
225225

226-
Defn : Expr ':=' Expr { Defn $1 $3 }
227226
Decl : AbiType id { Decl $1 (name $2) }
228227

229228
StorageVar : SlotType id { StorageVar (posn $2) $1 (name $2) }
@@ -324,7 +323,7 @@ parseError ((L token pn):_) =
324323
"parsing error at token ",
325324
show token])
326325

327-
emptyConstructor :: Transition -> Definition
328-
emptyConstructor (Transition _ _ c _ _ _ _ _) = Definition nowhere c (Interface "constructor" []) [] [] (Creates []) [] []
326+
emptyConstructor :: Transition -> Constructor
327+
emptyConstructor (Transition _ _ c _ _ _ _ _) = Constructor nowhere c (Interface "constructor" []) [] [] (Creates []) [] []
329328

330329
}

‎src/Act/Syntax.hs‎

Lines changed: 15 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,7 @@ locsFromBehaviour (Behaviour _ _ _ _ preconds cases postconds rewrites returns)
3636
<> maybe [] locsFromTypedExp returns
3737

3838
locsFromConstructor :: Annotated.Constructor -> [Annotated.StorageLocation]
39-
locsFromConstructor (Constructor _ _ _ pre post inv initialStorage) = nub $
39+
locsFromConstructor (Annotated.Constructor _ _ _ pre post inv initialStorage) = nub $
4040
concatMap locsFromExp pre
4141
<> concatMap locsFromExp post
4242
<> concatMap locsFromInvariant inv
@@ -52,23 +52,23 @@ locsFromInvariant (Invariant _ pre bounds (predpre, predpost)) =
5252
------------------------------------
5353

5454
nameOfContract :: Contract t -> Id
55-
nameOfContract (Contract (Constructor cname _ _ _ _ _ _) _) = cname
55+
nameOfContract (Contract (Annotated.Constructor cname _ _ _ _ _ _) _) = cname
5656

5757
behvsFromAct :: Agnostic.Act t -> [Behaviour t]
5858
behvsFromAct (Act _ contracts) = behvsFromContracts contracts
5959

6060
behvsFromContracts :: [Contract t] -> [Behaviour t]
6161
behvsFromContracts contracts = concatMap (\(Contract _ b) -> b) contracts
6262

63-
constrFromContracts :: [Contract t] -> [Constructor t]
63+
constrFromContracts :: [Contract t] -> [Agnostic.Constructor t]
6464
constrFromContracts contracts = fmap (\(Contract c _) -> c) contracts
6565

6666
locsFromUpdate :: StorageUpdate t -> [StorageLocation t]
6767
locsFromUpdate update = nub $ case update of
68-
(Update _ item e) -> locsFromItem SStorage item <> locsFromExp e
68+
(Annotated.Update _ item e) -> locsFromItem SStorage item <> locsFromExp e
6969

7070
locFromUpdate :: StorageUpdate t -> StorageLocation t
71-
locFromUpdate (Update _ item _) = _Loc item
71+
locFromUpdate (Annotated.Update _ item _) = _Loc item
7272

7373
locsFromItem :: SRefKind k -> TItem a k t -> [StorageLocation t]
7474
locsFromItem SCalldata item = concatMap locsFromTypedExp (ixsFromItem item)
@@ -164,7 +164,7 @@ createsFromContract (Contract constr behvs) =
164164
createsFromConstructor constr <> concatMap createsFromBehaviour behvs
165165

166166
createsFromConstructor :: Typed.Constructor -> [Id]
167-
createsFromConstructor (Constructor _ _ _ pre post inv initialStorage) = nub $
167+
createsFromConstructor (Typed.Constructor _ _ _ pre post inv initialStorage) = nub $
168168
concatMap createsFromExp pre
169169
<> concatMap createsFromExp post
170170
<> concatMap createsFromInvariant inv
@@ -176,7 +176,7 @@ createsFromInvariant (Invariant _ pre bounds ipred) =
176176

177177
createsFromUpdate :: StorageUpdate t ->[Id]
178178
createsFromUpdate update = nub $ case update of
179-
Update _ item e -> createsFromItem item <> createsFromExp e
179+
Typed.Update _ item e -> createsFromItem item <> createsFromExp e
180180

181181
createsFromBehaviour :: Behaviour t -> [Id]
182182
createsFromBehaviour (Behaviour _ _ _ _ _ preconds postconds rewrites returns) = nub $
@@ -191,7 +191,7 @@ pointersFromContract (Contract constr behvs) =
191191
nub $ pointersFromConstructor constr <> concatMap pointersFromBehaviour behvs
192192

193193
pointersFromConstructor :: Typed.Constructor -> [Id]
194-
pointersFromConstructor (Constructor _ _ ptrs _ _ _ _) =
194+
pointersFromConstructor (Typed.Constructor _ _ ptrs _ _ _ _) =
195195
map (\(PointsTo _ _ c) -> c) ptrs
196196

197197
pointersFromBehaviour :: Behaviour t -> [Id]
@@ -207,7 +207,7 @@ ethEnvFromBehaviour (Behaviour _ _ _ _ preconds cases postconds rewrites returns
207207
<> maybe [] ethEnvFromTypedExp returns
208208

209209
ethEnvFromConstructor :: Annotated.Constructor -> [EthEnv]
210-
ethEnvFromConstructor (Constructor _ _ _ pre post inv initialStorage) = nub $
210+
ethEnvFromConstructor (Annotated.Constructor _ _ _ pre post inv initialStorage) = nub $
211211
concatMap ethEnvFromExp pre
212212
<> concatMap ethEnvFromExp post
213213
<> concatMap ethEnvFromInvariant inv
@@ -220,7 +220,7 @@ ethEnvFromInvariant (Invariant _ pre bounds (predpre, predpost)) =
220220

221221
ethEnvFromUpdate :: StorageUpdate t -> [EthEnv]
222222
ethEnvFromUpdate rewrite = case rewrite of
223-
Update _ item e -> nub $ ethEnvFromItem item <> ethEnvFromExp e
223+
Typed.Update _ item e -> nub $ ethEnvFromItem item <> ethEnvFromExp e
224224

225225
ethEnvFromItem :: TItem k a t -> [EthEnv]
226226
ethEnvFromItem = nub . concatMap ethEnvFromTypedExp . ixsFromItem
@@ -276,7 +276,7 @@ idFromRef (SMapping _ e _) = idFromRef e
276276
idFromRef (SField _ e _ _) = idFromRef e
277277

278278
idFromUpdate :: StorageUpdate t -> Id
279-
idFromUpdate (Update _ item _) = idFromItem item
279+
idFromUpdate (Typed.Update _ item _) = idFromItem item
280280

281281
idFromLocation :: StorageLocation t -> Id
282282
idFromLocation (Loc _ item) = idFromItem item
@@ -294,7 +294,7 @@ ixsFromLocation :: StorageLocation t -> [TypedExp t]
294294
ixsFromLocation (Loc _ item) = ixsFromItem item
295295

296296
ixsFromUpdate :: StorageUpdate t -> [TypedExp t]
297-
ixsFromUpdate (Update _ item _) = ixsFromItem item
297+
ixsFromUpdate (Typed.Update _ item _) = ixsFromItem item
298298

299299
itemType :: TItem k a t -> ActType
300300
itemType (Item t _ _) = actType t
@@ -348,7 +348,7 @@ posnFromExp e = case e of
348348
--------------------------------------
349349

350350
nameFromStorage :: Untyped.Storage -> Id
351-
nameFromStorage (Untyped.Rewrite e _) = nameFromEntry e
351+
nameFromStorage (Untyped.Update e _) = nameFromEntry e
352352

353353
nameFromEntry :: Entry -> Id
354354
nameFromEntry (EVar _ x) = x
@@ -400,8 +400,8 @@ getPosn expr = case expr of
400400
BoolLit pn _ -> pn
401401
EInRange pn _ _ -> pn
402402

403-
posFromDef :: Defn -> Pn
404-
posFromDef (Defn e _) = getPosn e
403+
posFromDef :: Mapping -> Pn
404+
posFromDef (Mapping e _) = getPosn e
405405

406406
-- | Returns all the identifiers used in an expression,
407407
-- as well all of the positions they're used in.

‎src/Act/Syntax/Types.hs‎

Lines changed: 5 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -8,9 +8,7 @@
88
{-# LANGUAGE LambdaCase #-}
99
{-# LANGUAGE ScopedTypeVariables #-}
1010
{-# LANGUAGE MultiParamTypeClasses #-}
11-
12-
-- These extensions should be removed once we remove the defs at the end of this file.
13-
{-# LANGUAGE RankNTypes, TypeApplications, StandaloneKindSignatures, PolyKinds #-}
11+
{-# LANGUAGE RankNTypes, TypeApplications, PolyKinds #-}
1412

1513
{-|
1614
Module : Syntax.Types
@@ -32,9 +30,8 @@ data ActType
3230
| ABoolean
3331
| AByteStr
3432

35-
-- | Singleton runtime witness for Act types
36-
-- Sometimes we need to examine type tags at runime. Tagging structures
37-
-- with this type will let us do that.
33+
-- | Singleton runtime witness for Act types. Sometimes we need to examine type
34+
-- tags at runtime. Tagging structures with this type will let us do that.
3835
data SType (a :: ActType) where
3936
SInteger :: SType AInteger
4037
SBoolean :: SType ABoolean
@@ -70,8 +67,8 @@ instance SingI 'AInteger where sing = SInteger
7067
instance SingI 'ABoolean where sing = SBoolean
7168
instance SingI 'AByteStr where sing = SByteStr
7269

73-
-- | Reflection of an Act type into a haskell type. Useful to define
74-
-- the result type of the evaluation function.
70+
-- | Reflection of an Act type into a haskell type. Used to define the result
71+
-- type of the evaluation function.
7572
type family TypeOf a where
7673
TypeOf 'AInteger = Integer
7774
TypeOf 'ABoolean = Bool
@@ -126,7 +123,6 @@ pattern FromVType :: () => (SingI a) => SType a -> ValueType
126123
pattern FromVType t <- (someType . fromValueType -> FromSome t)
127124
{-# COMPLETE FromVType #-}
128125

129-
130126
-- | Helper pattern to retrieve the 'SingI' instances of the type
131127
-- represented by an 'SType'.
132128
pattern SType :: () => (SingI a) => SType a

‎src/Act/Syntax/Untyped.hs‎

Lines changed: 30 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,5 @@
1-
-- data types for the parsed syntax.
2-
-- Has the correct basic structure, but doesn't necessarily type check
3-
-- It is also equipped with position information for extra debugging xp
1+
-- Data types for the Act AST after parsing. It is also equipped with position information
2+
-- for printing informative error messages.
43
{-# LANGUAGE OverloadedStrings #-}
54

65
module Act.Syntax.Untyped (module Act.Syntax.Untyped) where
@@ -20,15 +19,17 @@ type Id = String
2019
newtype Act = Main [Contract]
2120
deriving (Eq, Show)
2221

23-
data Contract = Contract Definition [Transition]
22+
data Contract = Contract Constructor [Transition]
2423
deriving (Eq, Show)
2524

26-
data Definition = Definition Pn Id Interface [Pointer] [IffH] Creates Ensures Invariants
25+
data Constructor = Constructor Pn Id Interface [Pointer] Iff Creates Ensures Invariants
2726
deriving (Eq, Show)
2827

29-
data Transition = Transition Pn Id Id Interface [Pointer] [IffH] Cases Ensures
28+
data Transition = Transition Pn Id Id Interface [Pointer] Iff Cases Ensures
3029
deriving (Eq, Show)
3130

31+
type Iff = [Expr]
32+
3233
type Ensures = [Expr]
3334

3435
type Invariants = [Expr]
@@ -45,9 +46,7 @@ data Interface = Interface Id [Decl]
4546
instance Show Interface where
4647
show (Interface a d) = a <> "(" <> intercalate ", " (fmap show d) <> ")"
4748

48-
data Cases
49-
= Direct Post
50-
| Branches [Case]
49+
newtype Cases = Branches [Case]
5150
deriving (Eq, Show)
5251

5352
data Case = Case Pn Expr Post
@@ -61,23 +60,25 @@ newtype Creates = Creates [Assign]
6160
deriving (Eq, Show)
6261

6362
data Storage
64-
= Rewrite Entry Expr
63+
= Update Entry Expr
6564
deriving (Eq, Show)
6665

67-
data Assign = AssignVal StorageVar Expr | AssignMany StorageVar [Defn] | AssignStruct StorageVar [Defn]
66+
data Assign = AssignVal StorageVar Expr | AssignMapping StorageVar [Mapping]
6867
deriving (Eq, Show)
69-
-- TODO AssignStruct is never used
7068

71-
data IffH = Iff Pn [Expr] | IffIn Pn AbiType [Expr]
69+
data StorageVar = StorageVar Pn SlotType Id
7270
deriving (Eq, Show)
7371

72+
data Decl = Decl AbiType Id
73+
deriving (Eq, Ord)
74+
7475
data Entry
7576
= EVar Pn Id
7677
| EMapping Pn Entry [Expr]
7778
| EField Pn Entry Id
7879
deriving (Eq, Show)
7980

80-
data Defn = Defn Expr Expr
81+
data Mapping = Mapping Expr Expr
8182
deriving (Eq, Show)
8283

8384
data Expr
@@ -117,23 +118,6 @@ data Expr
117118
| EInRange Pn AbiType Expr
118119
deriving (Eq, Show)
119120

120-
data EthEnv
121-
= Caller
122-
| Callvalue
123-
| Calldepth
124-
| Origin
125-
| Blockhash
126-
| Blocknumber
127-
| Difficulty
128-
| Chainid
129-
| Gaslimit
130-
| Coinbase
131-
| Timestamp
132-
| This
133-
| Nonce
134-
deriving (Show, Eq)
135-
136-
137121
data ValueType
138122
= ContractType Id
139123
| PrimitiveType AbiType
@@ -160,12 +144,21 @@ instance Show SlotType where
160144
<> ")")
161145
(show t) s
162146

163-
164-
data StorageVar = StorageVar Pn SlotType Id
165-
deriving (Eq, Show)
166-
167-
data Decl = Decl AbiType Id
168-
deriving (Eq, Ord)
147+
data EthEnv
148+
= Caller
149+
| Callvalue
150+
| Calldepth
151+
| Origin
152+
| Blockhash
153+
| Blocknumber
154+
| Difficulty
155+
| Chainid
156+
| Gaslimit
157+
| Coinbase
158+
| Timestamp
159+
| This
160+
| Nonce
161+
deriving (Show, Eq)
169162

170163
instance Show Decl where
171164
show (Decl t a) = show t <> " " <> a

0 commit comments

Comments
 (0)