Skip to content

Commit 9619791

Browse files
lefterislazarlefterislazar
committed
Compilation progress
1 parent 6f26796 commit 9619791

File tree

3 files changed

+27
-26
lines changed

3 files changed

+27
-26
lines changed

‎src/Act/Coq.hs‎

Lines changed: 25 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -144,7 +144,7 @@ extStep main store = inductive
144144
localStore = contractStore main store
145145

146146
substep :: Id -> (SlotType, Integer) -> Maybe (T.Text, Maybe T.Text, T.Text)
147-
substep var (StorageValue (TContract cid), _) = Just (extStepType <> "_" <> varp, Just (envDecl <+> stateDecl <+> envVar' <+> stateDecl'), body')
147+
substep var (StorageValue (ValueType (TContract cid)), _) = Just (extStepType <> "_" <> varp, Just (envDecl <+> stateDecl <+> envVar' <+> stateDecl'), body')
148148
where
149149
varp = T.pack var
150150
body' = indent 2 . implication . concat $
@@ -161,7 +161,7 @@ extStep main store = inductive
161161
substep _ _ = Nothing
162162

163163
subBounds :: Id -> Id -> (SlotType, Integer) -> Maybe T.Text
164-
subBounds stepVar var (StorageValue (TContract cid), _) | var /= stepVar = Just $ T.pack cid <.> "integerBoundsRec" <+> parens (T.pack var <+> stateVar)
164+
subBounds stepVar var (StorageValue (ValueType (TContract cid)), _) | var /= stepVar = Just $ T.pack cid <.> "integerBoundsRec" <+> parens (T.pack var <+> stateVar)
165165
subBounds _ _ _ = Nothing
166166

167167

@@ -198,7 +198,7 @@ contractAddressIn name store = inductive
198198
localStore = contractStore name store
199199

200200
subCAddr :: Id -> (SlotType, Integer) -> Maybe (T.Text, Maybe T.Text, T.Text)
201-
subCAddr var (StorageValue (TContract cid), _) = Just ("addressOf_" <> varp, Just $ parens ("p : address") <+> stateDecl, body')
201+
subCAddr var (StorageValue (ValueType (TContract cid)), _) = Just ("addressOf_" <> varp, Just $ parens ("p : address") <+> stateDecl, body')
202202
where
203203
varp = T.pack var
204204
body' = indent 2 . implication $
@@ -219,13 +219,13 @@ addressIn name store = inductive
219219
localStore = contractStore name store
220220

221221
subAddr :: Id -> (SlotType, Integer) -> Maybe (T.Text, Maybe T.Text, T.Text)
222-
subAddr var (StorageValue TAddress, _) =
222+
subAddr var (StorageValue (ValueType TAddress), _) =
223223
let varp = T.pack var in
224224
Just ("address_" <> varp, Just stateDecl, indent 5 $ addressInType <+> parens (varp <+> stateVar) <+> stateVar)
225225
subAddr _ _ = Nothing
226226

227227
slotContractName :: SlotType -> Maybe Id
228-
slotContractName (StorageValue (TContract cid)) = Just cid
228+
slotContractName (StorageValue (ValueType (TContract cid))) = Just cid
229229
slotContractName _ = Nothing
230230

231231
noAliasing :: Id -> Store -> T.Text
@@ -267,17 +267,17 @@ intBounds name store = inductive
267267
localStore = contractStore name store
268268

269269
go :: Id -> (SlotType, Integer) -> Maybe T.Text
270-
go v (StorageValue (TContract cid), _) = Just $
270+
go v (StorageValue (ValueType (TContract cid)), _) = Just $
271271
"0 <=" <+> T.pack cid <.> addrField <+> parens (T.pack v <+> stateVar) <+> "<= UINT_MAX 160"
272-
go v (StorageValue (TInteger n Unsigned), _) = Just $
272+
go v (StorageValue (ValueType (TInteger n Unsigned)), _) = Just $
273273
"0 <=" <+> T.pack v <+> stateVar <+> "<= UINT_MAX" <+> T.pack (show n)
274-
go v (StorageValue (TInteger n Signed), _) = Just $
274+
go v (StorageValue (ValueType (TInteger n Signed)), _) = Just $
275275
"INT_MIN" <+> T.pack (show n) <+> "<=" <+> T.pack v <+> stateVar <+> "<= INT_MAX" <+> T.pack (show n)
276-
go v (StorageMapping is (TContract cid), _) = Just $ parens $
276+
go v (StorageMapping is (ValueType (TContract cid)), _) = Just $ parens $
277277
"forall" <+> ixs (length is) <> ", 0 <=" <+> T.pack cid <.> addrField <+> parens (T.pack v <+> stateVar <+> ixs (length is)) <+> "<= UINT_MAX 160"
278-
go v (StorageMapping is (TInteger n Unsigned), _) = Just $ parens $
278+
go v (StorageMapping is (ValueType (TInteger n Unsigned)), _) = Just $ parens $
279279
"forall" <+> ixs (length is) <> ", 0 <=" <+> T.pack v <+> stateVar <+> ixs (length is) <+> "<= UINT_MAX" <+> T.pack (show n)
280-
go v (StorageMapping is (TInteger n Signed), _) = Just $ parens $
280+
go v (StorageMapping is (ValueType (TInteger n Signed)), _) = Just $ parens $
281281
"forall" <+> ixs (length is) <> ", INT_MIN" <+> T.pack (show n) <+> "<=" <+> T.pack v <+> stateVar <+> ixs (length is) <+> "<= INT_MAX" <+> T.pack (show n)
282282
go _ _ = Nothing
283283

@@ -292,19 +292,19 @@ intBoundsRec name store = inductive
292292
localStore = contractStore name store
293293

294294
go :: Id -> (SlotType, Integer) -> [T.Text]
295-
go v (StorageValue (TContract cid), _) =
295+
go v (StorageValue (ValueType (TContract cid)), _) =
296296
[ "0 <=" <+> T.pack cid <.> addrField <+> parens (T.pack v <+> stateVar) <+> "<= UINT_MAX 160"
297297
, T.pack cid <.> "integerBoundsRec" <+> parens (T.pack v <+> stateVar) ]
298-
go v (StorageValue (TInteger n Unsigned), _) = pure $
298+
go v (StorageValue (ValueType (TInteger n Unsigned)), _) = pure $
299299
"0 <=" <+> T.pack v <+> stateVar <+> "<= UINT_MAX" <+> T.pack (show n)
300-
go v (StorageValue (TInteger n Signed), _) = pure $
300+
go v (StorageValue (ValueType (TInteger n Signed)), _) = pure $
301301
"INT_MIN" <+> T.pack (show n) <+> "<=" <+> T.pack v <+> stateVar <+> "<= INT_MAX" <+> T.pack (show n)
302-
go v (StorageMapping is (TContract cid), _) =
302+
go v (StorageMapping is (ValueType (TContract cid)), _) =
303303
[ parens $ "forall" <+> ixs (length is) <> ", 0 <=" <+> T.pack cid <.> addrField <+> parens (T.pack v <+> stateVar <+> ixs (length is)) <+> "<= UINT_MAX 160"
304304
, parens $ "forall" <+> ixs (length is) <> "," <+> T.pack cid <.> "integerBoundsRec" <+> parens (T.pack v <+> stateVar <+> ixs (length is)) ]
305-
go v (StorageMapping is (TInteger n Unsigned), _) = pure $ parens $
305+
go v (StorageMapping is (ValueType (TInteger n Unsigned)), _) = pure $ parens $
306306
"forall" <+> ixs (length is) <> ", 0 <=" <+> T.pack v <+> stateVar <+> ixs (length is) <+> "<= UINT_MAX" <+> T.pack (show n)
307-
go v (StorageMapping is (TInteger n Signed), _) = pure $ parens $
307+
go v (StorageMapping is (ValueType (TInteger n Signed)), _) = pure $ parens $
308308
"forall" <+> ixs (length is) <> ", INT_MIN" <+> T.pack (show n) <+> "<=" <+> T.pack v <+> stateVar <+> ixs (length is) <+> "<= INT_MAX" <+> T.pack (show n)
309309
go _ _ = []
310310

@@ -643,15 +643,15 @@ updateExp (Address _ (Create _ cid args)) = do
643643
updateExp e = pure (coqexp e, [])
644644

645645
updateExpTyped :: TypedExp -> Fresh (T.Text, [T.Text])
646-
updateExpTyped (TExp _ _ te) = updateExp te
646+
updateExpTyped (TExp _ te) = updateExp te
647647

648648
unField :: Ref Storage -> Ref Storage -> Ref Storage
649649
unField rFocus (SField pn r cid x) | r == rFocus = SVar pn cid x
650650
unField rFocus (SField pn r cid x) = SField pn (unField rFocus r) cid x
651651
unField _ r' = r'
652652

653653
updateVar :: Store -> [StorageUpdate] -> (Ref Storage -> SlotType -> T.Text) -> Ref Storage -> SlotType -> Fresh (T.Text, [T.Text])
654-
updateVar store updates handler focus t@(StorageValue (ContractType cid)) =
654+
updateVar store updates handler focus t@(StorageValue (ValueType (TContract cid))) =
655655
case unsnoc groupedUpdates of
656656
Nothing -> pure (handler focus t, [])
657657
Just (_, (firstU@(Update _ _ e) NE.:| [])) | eqRef focus firstU->
@@ -673,14 +673,14 @@ updateVar store updates handler focus t@(StorageValue (ContractType cid)) =
673673
-- all updates before the last group will be overwritten and so can be ignored
674674
groupedUpdates = NE.groupBy (\_ b -> not $ eqRef focus b) focusUpdates
675675

676-
updateVar _ updates handler focus t@(StorageValue (PrimitiveType AbiAddressType)) =
676+
updateVar _ updates handler focus t@(StorageValue (ValueType TAddress)) =
677677
case unsnoc focusUpdates of
678678
Nothing -> pure (handler focus t, [])
679679
Just (_, (Update _ _ e)) -> updateExp e
680680
where
681681
focusUpdates = filter (\u -> eqRef focus u || baseRef focus u) updates
682682

683-
updateVar _ updates handler focus t@(StorageValue (PrimitiveType _)) =
683+
updateVar _ updates handler focus t@(StorageValue _) =
684684
pure (foldl updatedVal (handler focus t) (filter (eqRef focus) updates), [])
685685
where
686686
updatedVal _ (Update TByteStr _ _) = error "bytestrings not supported"
@@ -746,8 +746,8 @@ valueType (ValueType (TContract cid)) = T.pack cid <> "." <> "State" -- the type
746746
valueType (ValueType t) = abiType $ toAbiType t
747747

748748
mappingIdxType :: ValueType -> T.Text
749-
mappingIdxType (PrimitiveType t) = abiType t
750-
mappingIdxType (ContractType _) = "address" -- index by addresses, not contents of states
749+
mappingIdxType (ValueType (TContract _)) = "address" -- index by addresses, not contents of states
750+
mappingIdxType (ValueType t) = abiType $ toAbiType t
751751

752752
-- | coq syntax for an abi type
753753
abiType :: AbiType -> T.Text
@@ -868,7 +868,8 @@ typedexp (TExp _ e) = coqexp e
868868

869869
entry :: Time 'Timed -> TItem k a -> T.Text
870870
entry _ (Item TByteStr _) = error "bytestrings not supported"
871-
entry whn (Item _ r) = ref whn r
871+
entry Pre (Item _ r) = ref stateVar r
872+
entry Post (Item _ r) = ref stateVar' r
872873

873874
ref :: T.Text -> Ref k -> T.Text
874875
ref refState (SVar _ cid name) = parens $ T.pack cid <.> T.pack name <+> refState

‎src/Act/Syntax/Typed.hs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -54,7 +54,7 @@ import Data.Type.Equality (TestEquality(..), (:~:)(..))
5454
import Act.Parse as Act.Syntax.Typed (nowhere)
5555
import Act.Syntax.Types as Act.Syntax.Typed
5656
import Act.Syntax.Timing as Act.Syntax.Typed
57-
import Act.Syntax.Untyped as Act.Syntax.Typed (Pn, Interface(..), EthEnv(..), Decl(..), SlotType(..), Pointer(..), makeIface)
57+
import Act.Syntax.Untyped as Act.Syntax.Typed (Pn, Interface(..), EthEnv(..), Decl(..), SlotType(..), ArgType(..), Pointer(..), makeIface, argToAbiType)
5858

5959
-- AST post typechecking
6060
data Act t = Act Store [Contract t]

‎src/Act/Type.hs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -623,7 +623,7 @@ unsafeFindContractType :: Exp a t -> Id
623623
unsafeFindContractType (ITE _ _ a _) =
624624
unsafeFindContractType a
625625
unsafeFindContractType (Create _ c _) = c
626-
unsafeFindContractType (VarRef _ _ _ (Item _ (ContractType c) _)) = c
626+
unsafeFindContractType (VarRef _ _ _ (Item (TContract c) _)) = c
627627
unsafeFindContractType _ = error "Internal error: unsafeFindContractType called for non contract expression"
628628

629629
-- | Find the contract id of an expression with contract type

0 commit comments

Comments
 (0)