WIP cleaning up AST

src/Act/Enrich.hs

@@ -82,7 +82,7 @@ mkStorageBounds refs = concatMap mkBound refs
     mkBound _ = []
 
 -- TODO why only Pre items here?
-fromItem :: TStorageItem AInteger -> Exp ABoolean
+fromItem :: TItem Storage AInteger -> Exp ABoolean
 fromItem item@(Item _ (PrimitiveType vt) _) = bound vt (TEntry nowhere Pre item)
 fromItem (Item _ (ContractType _) _) = LitBool nowhere True
 

src/Act/SMT.hs

@@ -81,7 +81,7 @@ type SMT2 = String
 
 -- | The context is a `Reader` monad which allows us to read
 -- the name of the current interface.
-type Ctx = Reader Id
+type Ctx = Reader Id -- TODO check if this is really needed
 
 -- | Specify the name to use as the current interface when creating SMT-code.
 withInterface :: Id -> Ctx SMT2 -> SMT2
@@ -625,7 +625,7 @@ expToSMT2 expr = case expr of
   Eq _ _ a b -> binop "=" a b
   NEq p s a b -> unop "not" (Eq p s a b)
   ITE _ a b c -> triop "ite" a b c
-  Var _ _ _ _ a -> varref a
+  Var _ _ item -> ventry item
   TEntry _ w item -> entry item w
   where
     unop :: String -> Exp a -> Ctx SMT2
@@ -639,16 +639,16 @@ expToSMT2 expr = case expr of
     triop op a b c = ["(" <> op <> " " <> a' <> " " <> b' <> " " <> c' <> ")"
                         | a' <- expToSMT2 a, b' <- expToSMT2 b, c' <- expToSMT2 c]
 
-    entry :: TStorageItem a -> When -> Ctx SMT2
+    entry :: TItem Storage a -> When -> Ctx SMT2
     entry item whn = case ixsFromItem item of
       []       -> pure $ nameFromItem whn item
       (ix:ixs) -> select (nameFromItem whn item) (ix :| ixs)
 
-    varref :: VarRef -> Ctx SMT2
-    varref var = case ixsFromVarRef var of
-      []       -> nameFromVarRef var
+    ventry :: TItem Calldata a -> Ctx SMT2
+    ventry (Item _ _ vref) = case ixsFromRef vref of
+      []       -> nameFromVRef vref
       (ix:ixs) -> do
-        name <- nameFromVarRef var
+        name <- nameFromVRef vref
         select name (ix :| ixs)
 
 -- | SMT2 has no support for exponentiation, but we can do some preprocessing
@@ -694,21 +694,22 @@ sType' (TExp t _) = sType $ actType t
 --- ** Variable Names ** ---
 
 -- Construct the smt2 variable name for a given storage item
-nameFromItem :: When -> TStorageItem a -> Id
-nameFromItem whn (Item _ _ ref) = nameFromStorageRef ref @@ show whn
-
-nameFromStorageRef :: StorageRef -> Id
-nameFromStorageRef (SVar _ c name) = c @@ name
-nameFromStorageRef (SMapping _ e _) = nameFromStorageRef e
-nameFromStorageRef (SField _ ref c x) = nameFromStorageRef ref @@ c @@ x
-
-nameFromVarRef :: VarRef -> Ctx Id
-nameFromVarRef (VVar _ _ name) = nameFromVarId name
-nameFromVarRef (VMapping _ v _) = nameFromVarRef v
-nameFromVarRef (VField _ ref c x) = do
-  name <- nameFromVarRef ref
+nameFromItem :: When -> TItem Storage a -> Id
+nameFromItem whn (Item _ _ ref) = nameFromRef ref @@ show whn
+
+nameFromRef :: Ref Storage -> Id
+nameFromRef (SVar _ c name) = c @@ name
+nameFromRef (SMapping _ e _) = nameFromRef e
+nameFromRef (SField _ ref c x) = nameFromRef ref @@ c @@ x
+
+nameFromVRef :: Ref Calldata -> Ctx Id
+nameFromVRef (CVar _ _ name) = nameFromVarId name
+nameFromVRef (SMapping _ e _) = nameFromVRef e
+nameFromVRef (SField _ ref c x) = do 
+  name <- nameFromVRef ref
   pure $ name @@ c @@ x
 
+
 -- Construct the smt2 variable name for a given storage location
 nameFromLoc :: When -> StorageLocation -> Id
 nameFromLoc whn (Loc _ item) = nameFromItem whn item

src/Act/Traversals.hs

@@ -20,11 +20,11 @@ instance TraversableTerm (Exp a t) where
 instance TraversableTerm (TypedExp t) where
   mapTermM = mapTypedExpM
 
-instance TraversableTerm (TStorageItem a t) where
-  mapTermM = mapTStorageItemM
+instance TraversableTerm (TItem k a t) where
+  mapTermM = mapTItemM
 
-instance TraversableTerm (StorageRef t) where
-  mapTermM = mapStorageRefM
+instance TraversableTerm (Ref k t) where
+  mapTermM = mapRefM
 
 mapExpM :: Monad m => (forall a . Exp a t -> m (Exp a t)) -> Exp b t -> m (Exp b t)
 mapExpM f = \case
@@ -137,28 +137,31 @@ mapExpM f = \case
     b' <- mapExpM f b
     c' <- mapExpM f c
     f (ITE p a' b' c')
-  Var p tm a v r -> f (Var p tm a v r)
+  Var p t i -> do
+    i' <- mapTItemM f i
+    f (Var p t i')
   TEntry p t i -> do
-    i' <- mapTStorageItemM f i
+    i' <- mapTItemM f i
     f (TEntry p t i')
 
 mapTypedExpM :: Monad m => (forall a . Exp a t -> m (Exp a t)) -> TypedExp t -> m (TypedExp t)
 mapTypedExpM f (TExp s e) = do
   e' <- f e
   pure $ TExp s e'
 
-mapTStorageItemM :: Monad m => (forall a . Exp a t -> m (Exp a t)) -> TStorageItem b t -> m (TStorageItem b t)
-mapTStorageItemM f (Item s v r) = do
-  r' <- mapStorageRefM f r
+mapTItemM :: Monad m => (forall a . Exp a t -> m (Exp a t)) -> TItem k b t -> m (TItem k b t)
+mapTItemM f (Item s v r) = do
+  r' <- mapRefM f r
   pure $ Item s v r'
 
-mapStorageRefM :: Monad m => (forall a . Exp a t -> m (Exp a t)) -> StorageRef t -> m (StorageRef t)
-mapStorageRefM f = \case
+mapRefM :: Monad m => (forall a . Exp a t -> m (Exp a t)) -> Ref k t -> m (Ref k t)
+mapRefM f = \case
   SVar p a b -> pure (SVar p a b)
+  CVar p a b -> pure (CVar p a b)
   SMapping p a b -> do
-    a' <- mapStorageRefM f a
+    a' <- mapRefM f a
     b' <- mapM (mapTypedExpM f) b
     pure $ SMapping p a' b'
   SField p r a b -> do
-    r' <- mapStorageRefM f r
+    r' <- mapRefM f r
     pure $ SField p r' a b

src/Act/Type.hs

@@ -358,7 +358,7 @@ checkPost env@Env{contract,theirs} (U.Post storage maybeReturn) = do
       , store    = Map.map fst $ Map.findWithDefault mempty name theirs
       }
 
-checkEntry :: forall t. Typeable t => Env -> U.Entry -> Err (SlotType, StorageRef t)
+checkEntry :: forall t. Typeable t => Env -> U.Entry -> Err (SlotType, Ref Storage t)
 checkEntry Env{contract,store,calldata} (U.EVar p name) = case (Map.lookup name store, Map.lookup name calldata) of
   (Just _, Just _) -> throw (p, "Ambiguous variable " <> name)
   (Just typ, Nothing) -> pure (typ, SVar p contract name)
@@ -378,38 +378,38 @@ checkEntry env@Env{theirs} (U.EField p e x) =
       Nothing -> error $ "Internal error: Invalid contract type " <> show c
     _ -> throw (p, "Expression should have a contract type" <> show e)
 
-validateEntry :: forall t. Typeable t => Env -> U.Entry -> Err (ValueType, StorageRef t)
+validateEntry :: forall t. Typeable t => Env -> U.Entry -> Err (ValueType, Ref Storage t)
 validateEntry env entry =
   checkEntry env entry `bindValidation` \(typ, ref) -> case typ of
     StorageValue t -> pure (t, ref)
     StorageMapping _ _  -> throw (getPosEntry entry, "Top-level expressions cannot have mapping type")
 
 
-checkVar :: forall t. Typeable t => Env -> U.Entry -> Err (SlotType, Maybe Id, VarRef t)
+checkVar :: forall t. Typeable t => Env -> U.Entry -> Err (SlotType, Maybe Id, Ref Calldata t)
 checkVar Env{store,calldata, pointers} (U.EVar p name) = case (Map.lookup name store, Map.lookup name calldata) of
   (Just _, Just _) -> throw (p, "Ambiguous variable " <> name)
   (Nothing, Just typ) -> do
-    pure (StorageValue (PrimitiveType typ), Map.lookup name pointers, VVar p typ name)
+    pure (StorageValue (PrimitiveType typ), Map.lookup name pointers, CVar p typ name)
   (Just _, Nothing) ->  error $ "Internal error: Variable must be a calldata variable."
   (Nothing, Nothing) -> throw (p, "Unknown variable " <> show name)
   -- TODO more consitent check of name overlap between calldata and storage
 checkVar env (U.EMapping p v args) =
   checkVar env v `bindValidation` \(typ, _, ref) -> case typ of
     StorageValue _ -> throw (p, "Expression should have a mapping type" <> show v)
     StorageMapping argtyps restyp ->
-      (StorageValue restyp, Nothing,) . VMapping p ref <$> checkIxs env p args (NonEmpty.toList argtyps)
+      (StorageValue restyp, Nothing,) . SMapping p ref <$> checkIxs env p args (NonEmpty.toList argtyps)
 checkVar env@Env{theirs} (U.EField p e x) =
   checkVar env e `bindValidation` \(_, oc, ref) -> case oc of
     Just c -> case Map.lookup c theirs of
       Just cenv -> case Map.lookup x cenv of
-        Just (st@(StorageValue (ContractType c')), _) -> pure (st, Just c', VField p ref c x)
-        Just (st, _) -> pure (st, Nothing, VField p ref c x)
+        Just (st@(StorageValue (ContractType c')), _) -> pure (st, Just c', SField p ref c x)
+        Just (st, _) -> pure (st, Nothing, SField p ref c x)
         Nothing -> throw (p, "Contract " <> c <> " does not have field " <> x)
       Nothing -> error $ "Internal error: Invalid contract type " <> show c
     _ -> throw (p, "Expression should have a contract type" <> show e)
 
 
-validateVar :: forall t. Typeable t => Env -> U.Entry -> Err (ValueType, VarRef t)
+validateVar :: forall t. Typeable t => Env -> U.Entry -> Err (ValueType, Ref Calldata t)
 validateVar env var =
   checkVar env var `bindValidation` \(typ, cid, ref) -> case typ of
     StorageValue t -> case cid of
@@ -452,7 +452,7 @@ checkIffs env = foldr check (pure [])
 
 genInRange :: AbiType -> Exp AInteger t -> [Exp ABoolean t]
 genInRange t e@(LitInt _ _) = [InRange nowhere t e]
-genInRange t e@(Var _ _ _ _ _)  = [InRange nowhere t e]
+genInRange t e@(Var _ _ _)  = [InRange nowhere t e]
 genInRange t e@(TEntry _ _ _)  = [InRange nowhere t e]
 genInRange t e@(Add _ e1 e2) = [InRange nowhere t e] <> genInRange t e1 <> genInRange t e2
 genInRange t e@(Sub _ e1 e2) = [InRange nowhere t e] <> genInRange t e1 <> genInRange t e2
@@ -538,11 +538,10 @@ checkExpr env@Env{constructors, calldata} typ e = case (typ, e) of
   (_, U.EUTEntry entry) | isCalldataEntry entry -> -- TODO more principled way of treating timings
      case (eqT @t @Timed, eqT @t @Untimed) of
        (Just Refl, _) -> validateVar env entry `bindValidation` \(vt@(FromVType typ'), ref) ->
-         Var (getPosEntry entry) Pre typ vt ref <$ checkEq (getPosEntry entry) typ typ'
+         Var (getPosEntry entry) Pre (Item typ vt ref) <$ checkEq (getPosEntry entry) typ typ'
        (_, Just Refl) -> validateVar env entry `bindValidation` \(vt@(FromVType typ'), ref) ->
-         Var (getPosEntry entry) Neither typ vt ref <$ checkEq (getPosEntry entry) typ typ'
+         Var (getPosEntry entry) Neither (Item typ vt ref) <$ checkEq (getPosEntry entry) typ typ'
        (_,_) -> error "Internal error: Timing should be either Timed or Untimed"
-       -- Var (getPosEntry entry) Neither typ vt ref <$ checkEq (getPosEntry entry) typ typ'
   (_, U.EPreEntry entry) | isCalldataEntry entry -> error "Not supported"
   (_, U.EPostEntry entry) | isCalldataEntry entry -> error "Not supported"
   -- Storage references
@@ -590,7 +589,7 @@ findContractType env (ITE p _ a b) =
     (Just c1, Just c2) -> Just c1 <$ assert (p, "Type of if-then-else branches does not match") (c1 == c2)
     (_, _ )-> pure Nothing
 findContractType _ (Create _ c _) = pure $ Just c
-findContractType _ (Var _ _ _ (ContractType c) _) = pure $ Just c
+findContractType _ (Var _ _ (Item _ (ContractType c) _)) = pure $ Just c
 findContractType _ (TEntry _ _ (Item _ (ContractType c) _)) = pure $ Just c
 findContractType _ _ =  pure Nothing