Skip to content

Commit d7c2db8

Browse files
zoepzoep
committed
Typing: better typing for expressions and simplifications
1 parent 17c8da1 commit d7c2db8

File tree

1 file changed

+89
-82
lines changed

1 file changed

+89
-82
lines changed

‎src/Act/Type.hs‎

Lines changed: 89 additions & 82 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,7 @@ import Data.Typeable hiding (typeRep)
2323
import Type.Reflection (typeRep)
2424

2525
import Control.Monad (when)
26+
import Data.Functor
2627
import Data.List.Extra (unsnoc)
2728
import Data.Function (on)
2829
import Data.Foldable
@@ -41,6 +42,9 @@ import Act.Syntax.Untyped (makeIface)
4142
import Act.Error
4243

4344
import Data.Type.Equality (TestEquality(..))
45+
import Data.Singletons
46+
47+
import Data.Aeson.Types (typeMismatch)
4448

4549

4650
type Err = Error String
@@ -352,7 +356,7 @@ checkDefn pn env@Env{contract} keyType vt@(FromVType valType) name (U.Defn k val
352356
-- | Type checks a postcondition, returning typed versions of its storage updates and return expression.
353357
checkPost :: Env -> U.Post -> Err ([StorageUpdate], Maybe (TypedExp Timed))
354358
checkPost env (U.Post storage maybeReturn) = do
355-
returnexp <- traverse (typedExp env) maybeReturn
359+
returnexp <- traverse (inferExpr env) maybeReturn
356360
storage' <- checkEntries storage
357361
pure (storage', returnexp)
358362
where
@@ -413,6 +417,10 @@ checkIffs env = foldr check (pure [])
413417
check (U.Iff _ exps) acc = mappend <$> traverse (checkExpr env SBoolean) exps <*> acc
414418
check (U.IffIn _ typ exps) acc = mappend <$> (mconcat <$> traverse (fmap (genInRange typ) . checkExpr env SInteger) exps) <*> acc
415419

420+
421+
-- | If an `inrange e` predicate appears in the source code, then the inrange
422+
-- predicate is propagated to all subexpressions of `e`. This elaboration step
423+
-- happens here.
416424
genInRange :: AbiType -> Exp AInteger t -> [Exp ABoolean t]
417425
genInRange t e@(LitInt _ _) = [InRange nowhere t e]
418426
genInRange t e@(TEntry _ _ _ _) = [InRange nowhere t e]
@@ -432,111 +440,111 @@ genInRange _ (ITE _ _ _ _) = error "Internal error: invalid range expression"
432440

433441
-- | Attempt to construct a `TypedExp` whose type matches the supplied `ValueType`.
434442
-- The target timing parameter will be whatever is required by the caller.
435-
checkExprVType :: Typeable t => Env -> U.Expr -> ValueType -> Err (TypedExp t)
443+
checkExprVType :: forall t. Typeable t => Env -> U.Expr -> ValueType -> Err (TypedExp t)
436444
checkExprVType env e (FromVType typ) = TExp typ <$> checkExpr env typ e
437445

438-
-- | Attempt to typecheck an untyped expression as any possible type.
439-
typedExp :: Typeable t => Env -> U.Expr -> Err (TypedExp t)
440-
typedExp env e = findSuccess (throw (getPosn e, "Cannot find a valid type for expression " <> show e))
441-
[ TExp SInteger <$> checkExpr env SInteger e
442-
, TExp SBoolean <$> checkExpr env SBoolean e
443-
, TExp SByteStr <$> checkExpr env SByteStr e
444-
]
445446

446-
-- | Helper to create to create a conjunction out of a list of expressions
447-
andExps :: [Exp ABoolean t] -> Exp ABoolean t
448-
andExps [] = LitBool nowhere True
449-
andExps (c:cs) = foldr (And nowhere) c cs
447+
typeMismatchErr :: forall a b res. Pn -> SType a -> SType b -> Err res
448+
typeMismatchErr p t1 t2 = (throw (p, "Type " <> show t1 <> " should match type " <> show t2 <> "\n Env:\n" <> show env))
449+
450+
-- | Check is the given expression can be typed with the given type\\
451+
checkExpr :: forall t a. Typeable t => Env -> SType a -> U.Expr -> Err (Exp a t)
452+
checkExpr env t1 e =
453+
-- No idea why type annotation is required here
454+
(inferExpr env e :: Err (TypedExp t)) `bindValidation` (\(TExp t2 te) ->
455+
maybe (typeMismatchErr (getPosn e) t1 t2) (\Refl -> pure te) $ testEquality t1 t2)
450456

451-
-- | Check the type of an expression and construct a typed expression
452-
checkExpr :: forall a t. Typeable t => Env -> SType a -> U.Expr -> Err (Exp a t)
453-
checkExpr env@Env{constructors, calldata} typ e = case (typ, e) of
457+
-- | Attempt to infer a type of an expression. If succesfull returns an
458+
-- existential package of the infered typed together with the typed expression.
459+
inferExpr :: forall t. Typeable t => Env -> U.Expr -> Err (TypedExp t)
460+
inferExpr env@Env{calldata, constructors} e = case e of
454461
-- Boolean expressions
455-
(SBoolean, U.ENot p v1) -> Neg p <$> checkExpr env SBoolean v1
456-
(SBoolean, U.EAnd p v1 v2) -> And p <$> checkExpr env SBoolean v1 <*> checkExpr env SBoolean v2
457-
(SBoolean, U.EOr p v1 v2) -> Or p <$> checkExpr env SBoolean v1 <*> checkExpr env SBoolean v2
458-
(SBoolean, U.EImpl p v1 v2) -> Impl p <$> checkExpr env SBoolean v1 <*> checkExpr env SBoolean v2
459-
(SBoolean, U.ELT p v1 v2) -> LT p <$> checkExpr env SInteger v1 <*> checkExpr env SInteger v2
460-
(SBoolean, U.ELEQ p v1 v2) -> LEQ p <$> checkExpr env SInteger v1 <*> checkExpr env SInteger v2
461-
(SBoolean, U.EGEQ p v1 v2) -> GEQ p <$> checkExpr env SInteger v1 <*> checkExpr env SInteger v2
462-
(SBoolean, U.EGT p v1 v2) -> GT p <$> checkExpr env SInteger v1 <*> checkExpr env SInteger v2
463-
(SBoolean, U.EEq p v1 v2) -> polycheck p Eq v1 v2
464-
(SBoolean, U.ENeq p v1 v2) -> polycheck p NEq v1 v2
465-
(SBoolean, U.BoolLit p v1) -> pure $ LitBool p v1
466-
(SBoolean, U.EInRange _ abityp v) -> andExps <$> genInRange abityp <$> checkExpr env SInteger v
462+
U.ENot p v1 -> wrapOp (Neg p) <$> checkExpr env SBoolean v1
463+
U.EAnd p v1 v2 -> wrapOp2 (And p) <$> checkExpr env SBoolean v1 <*> checkExpr env SBoolean v2
464+
U.EOr p v1 v2 -> wrapOp2 (Or p) <$> checkExpr env SBoolean v1 <*> checkExpr env SBoolean v2
465+
U.EImpl p v1 v2 -> wrapOp2 (Impl p) <$> checkExpr env SBoolean v1 <*> checkExpr env SBoolean v2
466+
U.ELT p v1 v2 -> wrapOp2 (LT p) <$> checkExpr env SInteger v1 <*> checkExpr env SInteger v2
467+
U.ELEQ p v1 v2 -> wrapOp2 (LEQ p) <$> checkExpr env SInteger v1 <*> checkExpr env SInteger v2
468+
U.EGEQ p v1 v2 -> wrapOp2 (GEQ p) <$> checkExpr env SInteger v1 <*> checkExpr env SInteger v2
469+
U.EGT p v1 v2 -> wrapOp2 (GT p) <$> checkExpr env SInteger v1 <*> checkExpr env SInteger v2
470+
U.EEq p v1 v2 -> TExp SBoolean <$> polycheck p Eq v1 v2
471+
U.ENeq p v1 v2 -> TExp SBoolean <$> polycheck p NEq v1 v2
472+
U.BoolLit p v1 -> pure $ TExp SBoolean (LitBool p v1)
473+
U.EInRange _ abityp v -> TExp SBoolean . andExps <$> genInRange abityp <$> checkExpr env SInteger v
467474

468475
-- Arithemetic expressions
469-
(SInteger, U.EAdd p v1 v2) -> Add p <$> checkExpr env SInteger v1 <*> checkExpr env SInteger v2
470-
(SInteger, U.ESub p v1 v2) -> Sub p <$> checkExpr env SInteger v1 <*> checkExpr env SInteger v2
471-
(SInteger, U.EMul p v1 v2) -> Mul p <$> checkExpr env SInteger v1 <*> checkExpr env SInteger v2
472-
(SInteger, U.EDiv p v1 v2) -> Div p <$> checkExpr env SInteger v1 <*> checkExpr env SInteger v2
473-
(SInteger, U.EMod p v1 v2) -> Mod p <$> checkExpr env SInteger v1 <*> checkExpr env SInteger v2
474-
(SInteger, U.EExp p v1 v2) -> Exp p <$> checkExpr env SInteger v1 <*> checkExpr env SInteger v2
475-
(SInteger, U.IntLit p v1) -> pure $ LitInt p v1
476-
-- Constructor calls
477-
(SInteger, U.ECreate p c args) -> case Map.lookup c constructors of
478-
Just ctrs ->
479-
let (typs, ptrs) = unzip ctrs in
476+
U.EAdd p v1 v2 -> wrapOp2 (Add p) <$> checkExpr env SInteger v1 <*> checkExpr env SInteger v2
477+
U.ESub p v1 v2 -> wrapOp2 (Sub p) <$> checkExpr env SInteger v1 <*> checkExpr env SInteger v2
478+
U.EMul p v1 v2 -> wrapOp2 (Mul p) <$> checkExpr env SInteger v1 <*> checkExpr env SInteger v2
479+
U.EDiv p v1 v2 -> wrapOp2 (Div p) <$> checkExpr env SInteger v1 <*> checkExpr env SInteger v2
480+
U.EMod p v1 v2 -> wrapOp2 (Mod p) <$> checkExpr env SInteger v1 <*> checkExpr env SInteger v2
481+
U.EExp p v1 v2 -> wrapOp2 (Exp p) <$> checkExpr env SInteger v1 <*> checkExpr env SInteger v2
482+
U.IntLit p v1 -> pure $ TExp SInteger (LitInt p v1)
483+
484+
-- Constructor calls
485+
U.ECreate p c args -> case Map.lookup c constructors of
486+
Just sig ->
487+
let (typs, ptrs) = unzip sig in
488+
-- check the types of arguments to constructor call
480489
checkIxs env p args (fmap PrimitiveType typs) `bindValidation` (\args' ->
481-
Create p c args' <$ traverse_ (uncurry $ checkContractType env) (zip args' ptrs))
490+
-- then check that all arguments that need to be valid pointers to a contract have a contract type
491+
traverse_ (uncurry $ checkContractType env) (zip args' ptrs) $>
492+
TExp SInteger (Create p c args'))
482493
Nothing -> throw (p, "Unknown constructor " <> show c)
483494

484495
-- Control
485-
(_, U.EITE p v1 v2 v3) ->
486-
((,) <$> checkExpr env typ v2 <*> checkExpr env typ v3) `bindValidation` (\(e1, e2) -> do
487-
b <- checkExpr env SBoolean v1
488-
pure $ ITE p b e1 e2)
496+
U.EITE p e1 e2 e3 ->
497+
checkExpr env SBoolean e1 `bindValidation` \b ->
498+
polycheck p (\pn t te1 te2 -> TExp t (ITE pn b te1 te2)) e2 e3
489499

490500
-- Environment variables
491-
(SInteger, U.EnvExp p v1) -> case lookup v1 globalEnv of
492-
Just AInteger -> pure $ IntEnv p v1
493-
Just AByteStr -> throw (p, "Environment variable " <> show v1 <> " has type bytestring but an expression of type integer is expected.")
494-
_ -> throw (p, "Unknown environment variable " <> show v1)
495-
(SByteStr, U.EnvExp p v1) -> case lookup v1 globalEnv of
496-
Just AInteger -> throw (p, "Environment variable " <> show v1 <> " has type integer but an expression of type bytestring is expected.")
497-
Just AByteStr -> pure $ ByEnv p v1
501+
U.EnvExp p v1 -> case lookup v1 globalEnv of
502+
Just AInteger -> pure $ TExp SInteger $ IntEnv p v1
503+
Just AByteStr -> pure $ TExp SByteStr $ ByEnv p v1
498504
_ -> throw (p, "Unknown environment variable " <> show v1)
499505

500506
-- Variable references
501507
-- Note: untimed entries in the untyped AST and in the typed AST have
502508
-- different meanings. Calldata variables are always untimed in the untimed
503509
-- AST but they become timed (with pre) in the typed AST whene they are used
504510
-- in a timed context.
505-
(_, U.EUTEntry entry) | isCalldataEntry entry -> checkVar entry
506-
(_, U.EPreEntry entry) | isCalldataEntry entry -> checkVar entry
507-
(_, U.EPostEntry entry) | isCalldataEntry entry -> error $ "Internal error: Variables cannot be post" <> show e
511+
U.EUTEntry entry | isCalldataEntry entry -> checkVar entry
512+
U.EPreEntry entry | isCalldataEntry entry -> checkVar entry
513+
U.EPostEntry entry | isCalldataEntry entry -> error $ "Internal error: Variables cannot be post" <> show e
508514
-- Storage references
509-
(_, U.EUTEntry entry) -> checkStorage entry Neither
510-
(_, U.EPreEntry entry) -> checkStorage entry Pre
511-
(_, U.EPostEntry entry) -> checkStorage entry Post
515+
U.EUTEntry entry -> checkStorage entry Neither
516+
U.EPreEntry entry -> checkStorage entry Pre
517+
U.EPostEntry entry -> checkStorage entry Post
512518

513-
-- TODO other error for unimplemented
514-
_ -> throw (getPosn e,"Type mismatch. Expression does not have type " <> show typ)
519+
_ -> throw (getPosn e, "Internal error: Cannot type expression " <> show e)
515520

516521
where
517-
checkVar :: U.Entry -> Err (Exp a t)
522+
wrapOp f e1 = TExp sing (f e1) -- use sign to let Haskell automatically derive the type here
523+
wrapOp2 f e1 e2 = TExp sing (f e1 e2)
524+
525+
polycheck :: forall z. Pn -> (forall y. Pn -> SType y -> Exp y t -> Exp y t -> z) -> U.Expr -> U.Expr -> Err z
526+
polycheck pn cons e1 e2 =
527+
inferExpr env e1 `bindValidation` \(TExp (t1 :: SType a1) (te1 :: Exp a1 t)) -> -- I don't know why type annotations are required here
528+
inferExpr env e2 `bindValidation` \(TExp (t2 :: SType a2) (te2 :: Exp a2 t)) ->
529+
maybe (typeMismatchErr pn t1 t2) (\Refl -> pure $ cons pn t1 te1 te2) $ testEquality t1 t2
530+
531+
checkVar :: U.Entry -> Err (TypedExp t)
518532
checkVar entry = case (eqT @t @Timed, eqT @t @Untimed) of
519-
(Just Refl, _) -> validateEntry env SCalldata entry `bindValidation` \(vt@(FromVType typ'), ref) ->
520-
TEntry (getPosEntry entry) Pre SCalldata (Item typ vt ref) <$ checkEq (getPosEntry entry) typ typ'
533+
(Just Refl, _) ->
534+
(\(vt@(FromVType typ), ref) -> TExp typ $ TEntry (getPosEntry entry) Pre SCalldata (Item typ vt ref)) <$> (validateEntry env SCalldata entry)
521535
(_, Just Refl) -> validateEntry env SCalldata entry `bindValidation` \(vt@(FromVType typ'), ref) ->
522-
TEntry (getPosEntry entry) Neither SCalldata (Item typ vt ref) <$ checkEq (getPosEntry entry) typ typ'
536+
(\(vt@(FromVType typ), ref) -> TExp typ $ TEntry (getPosEntry entry) Neither SCalldata (Item typ vt ref)) <$> (validateEntry env SCalldata entry)
523537
(_,_) -> error "Internal error: Timing should be either Timed or Untimed"
524538

525-
checkStorage :: forall t0. Typeable t0 => U.Entry -> Time t0 -> Err (Exp a t)
526-
checkStorage entry time = validateEntry env SStorage entry `bindValidation` \(vt@(FromVType typ'), ref) ->
527-
checkTime (getPosEntry entry) <*> (TEntry (getPosEntry entry) time SStorage (Item typ vt ref) <$ checkEq (getPosEntry entry) typ typ')
539+
-- Type check a storage variable
540+
checkStorage :: forall t0. Typeable t0 => U.Entry -> Time t0 -> Err (TypedExp t)
541+
checkStorage entry time =
542+
-- check that the timing is correct
543+
checkTime (getPosEntry entry) <*>
544+
((\(vt@(FromVType typ), ref) -> TExp typ $ TEntry (getPosEntry entry) time SStorage (Item typ vt ref)) <$> validateEntry env SStorage entry)
528545

529-
530-
polycheck :: Pn -> (forall y. Pn -> SType y -> Exp y t -> Exp y t -> Exp x t) -> U.Expr -> U.Expr -> Err (Exp x t)
531-
polycheck pn cons v1 v2 = findSuccess (throw (pn, "Cannot match the type of expression " <> show v1 <>" with expression " <> show v2))
532-
533-
-- TODO this is inefficient and produces really bad error messages. Do proper type inference instead
534-
[ cons pn SInteger <$> checkExpr env SInteger v1 <*> checkExpr env SInteger v2
535-
, cons pn SBoolean <$> checkExpr env SBoolean v1 <*> checkExpr env SBoolean v2
536-
, cons pn SByteStr <$> checkExpr env SByteStr v1 <*> checkExpr env SByteStr v2
537-
]
538-
539-
checkTime :: forall t0. Typeable t0 => Pn -> Err (Exp a t0 -> Exp a t)
546+
-- Check that an expression is typed with the right timing
547+
checkTime :: forall t0. Typeable t0 => Pn -> Err (TypedExp t0 -> TypedExp t)
540548
checkTime pn = case eqT @t @t0 of
541549
Just Refl -> pure id
542550
Nothing -> throw (pn, (tail . show $ typeRep @t) <> " variable needed here")
@@ -547,11 +555,10 @@ checkExpr env@Env{constructors, calldata} typ e = case (typ, e) of
547555
isCalldataEntry (U.EMapping _ entry _) = isCalldataEntry entry
548556
isCalldataEntry (U.EField _ entry _) = isCalldataEntry entry
549557

550-
checkEq :: forall b c. Pn -> SType b -> SType c -> Err ()
551-
checkEq p t1 t2 = maybe err (\Refl -> pure ()) $ testEquality t1 t2
552-
where
553-
err = (throw (p, "Type " <> show t1 <> " should match type " <> show t2 <> "\n Env:\n" <> show env))
554-
558+
-- | Helper to create to create a conjunction out of a list of expressions
559+
andExps :: [Exp ABoolean t] -> Exp ABoolean t
560+
andExps [] = LitBool nowhere True
561+
andExps (c:cs) = foldr (And nowhere) c cs
555562

556563

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

0 commit comments

Comments
 (0)