Skip to content

Commit 457b8ef

Browse files
committed
WIP in typing
1 parent d95389c commit 457b8ef

File tree

1 file changed

+34
-9
lines changed

1 file changed

+34
-9
lines changed

src/Act/Type.hs

Lines changed: 34 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -384,6 +384,36 @@ validateEntry env entry =
384384
-- TODO can mappings be assigned?
385385
StorageMapping _ _ -> throw (getPosEntry entry, "Top-level expressions cannot have mapping type")
386386

387+
388+
checkVar :: forall t. Typeable t => Env -> U.Entry -> Err (SlotType, StorageRef t)
389+
checkVar Env{contract,store,calldata} (U.EVar p name) = case (Map.lookup name store, Map.lookup name calldata) of
390+
(Just _, Just _) -> throw (p, "Ambiguous variable " <> name)
391+
(Just typ, Nothing) -> pure (typ, SVar p contract name)
392+
(Nothing, Just _) -> throw (p, "Variable " <> name <> " is not a storage variable")
393+
(Nothing, Nothing) -> throw (p, "Unknown storage variable " <> show name)
394+
-- TODO more consitent check of name overlap between calldata and storage
395+
checkVar env (U.EMapping p e args) =
396+
checkEntry env e `bindValidation` \(typ, ref) -> case typ of
397+
StorageValue _ -> throw (p, "Expression should have a mapping type" <> show e)
398+
StorageMapping argtyps restyp -> (StorageValue restyp,) . SMapping p ref <$> checkIxs env p args (NonEmpty.toList argtyps)
399+
checkVar env@Env{theirs} (U.EField p e x) =
400+
checkEntry env e `bindValidation` \(typ, ref) -> case typ of
401+
StorageValue (ContractType c) -> case Map.lookup c theirs of
402+
Just cenv -> case Map.lookup x cenv of
403+
Just (t, _) -> pure (t, SField p ref c x)
404+
Nothing -> throw (p, "Contract " <> c <> " does not have field " <> x)
405+
Nothing -> error $ "Internal error: Invalid contract type " <> show c
406+
_ -> throw (p, "Expression should have a contract type" <> show e)
407+
408+
409+
410+
validateVar :: forall t. Typeable t => Env -> U.Entry -> Err (AbiType, VarRef t)
411+
validateVar env entry =
412+
checkEntry env entry `bindValidation` \(typ, ref) -> case typ of
413+
StorageValue t -> pure (t, ref)
414+
-- TODO can mappings be assigned?
415+
StorageMapping _ _ -> throw (getPosEntry entry, "Top-level expressions cannot have mapping type")
416+
387417
-- | Typechecks a non-constant rewrite.
388418
checkStorageExpr :: Env -> U.Entry -> U.Expr -> Err StorageUpdate
389419
checkStorageExpr env entry expr =
@@ -486,7 +516,8 @@ checkExpr env@Env{constructors} typ e = case (typ, e) of
486516
Just AByteStr -> pure $ ByEnv p v1
487517
_ -> throw (p, "Unknown environment variable " <> show v1)
488518
-- Variable references
489-
(_, U.EUTEntry entry) | isCalldataEntry env entry -> checkCalldataEntry env entry
519+
(_, U.EUTEntry entry) | isCalldataEntry env entry -> validateVar env entry `bindValidation` \(at@(FromAbi varType), ref) ->
520+
checkTime (getPosEntry entry) <*> (Var (getPosEntry entry) typ at ref <$ checkEq (getPosEntry entry) typ varTyp)
490521
(_, U.EUTEntry entry) -> validateEntry env entry `bindValidation` \(vt@(FromVType typ'), ref) ->
491522
checkTime (getPosEntry entry) <*> (TEntry (getPosEntry entry) Neither (Item typ vt ref) <$ checkEq (getPosEntry entry) typ typ')
492523
(_, U.EPreEntry entry) -> validateEntry env entry `bindValidation` \(vt@(FromVType typ'), ref) ->
@@ -512,21 +543,14 @@ checkExpr env@Env{constructors} typ e = case (typ, e) of
512543
Just Refl -> pure id
513544
Nothing -> throw (pn, (tail . show $ typeRep @t) <> " variable needed here")
514545

546+
-- TODO FIX
515547
isCalldataEntry Env{calldata} (U.EVar _ name) = case Map.lookup name calldata of
516548
Just _ -> True
517549
_ -> False
518550
isCalldataEntry _ _ = False
519551

520-
checkCalldataEntry Env{store,calldata} (U.EVar p name) = case (Map.lookup name store, Map.lookup name calldata) of
521-
(Nothing, Nothing) -> throw (p, "Unknown variable " <> name)
522-
(Just _, Just _) -> throw (p, "Ambiguous variable " <> name)
523-
(Nothing, Just at@(FromAbi varType)) -> Var p typ at name <$ checkEq p typ varType
524-
(Just _, Nothing) -> error "Internal error: variable must be in calldata"
525-
checkCalldataEntry _ _ = error "Internal error: variable cannot be mapping or contract field"
526-
527552

528553
-- | Find the contract id of an expression with contract type
529-
-- TODO fix
530554
checkContractType :: Env -> SType a -> Exp a t -> Err (Maybe Id)
531555
checkContractType env SInteger (ITE p _ a b) =
532556
checkContractType env SInteger a `bindValidation` \oc1 ->
@@ -535,6 +559,7 @@ checkContractType env SInteger (ITE p _ a b) =
535559
(Just c1, Just c2) -> Just c1 <$ assert (p, "Type of if-then-else branches does not match") (c1 == c2)
536560
(_, _ )-> pure Nothing
537561
checkContractType _ SInteger (Create _ c _) = pure $ Just c
562+
-- TODO Fix
538563
checkContractType Env{pointers} SInteger (Var _ _ _ x) =
539564
case Map.lookup x pointers of
540565
Just c -> pure $ Just c

0 commit comments

Comments
 (0)