From 174bb3c20a40d9cda3c95a734b28757e30aee86b Mon Sep 17 00:00:00 2001 From: "Iavor S. Diatchki" Date: Thu, 23 Feb 2017 15:18:05 -0800 Subject: [PATCH] Remove ECast The invariant that this used to ensure does not hold anymore, so it was more confusing than not to have it. --- src/Cryptol/Eval.hs | 2 -- src/Cryptol/Eval/Reference.hs | 1 - src/Cryptol/Transform/MonoValues.hs | 1 - src/Cryptol/Transform/Specialize.hs | 2 -- src/Cryptol/TypeCheck/AST.hs | 20 -------------------- src/Cryptol/TypeCheck/Infer.hs | 20 ++++++++++++-------- src/Cryptol/TypeCheck/Instantiate.hs | 6 +----- src/Cryptol/TypeCheck/Sanity.hs | 6 ------ src/Cryptol/TypeCheck/Solver/Selector.hs | 19 +++++++++---------- src/Cryptol/TypeCheck/Subst.hs | 1 - src/Cryptol/TypeCheck/TypeOf.hs | 2 -- 11 files changed, 22 insertions(+), 58 deletions(-) diff --git a/src/Cryptol/Eval.hs b/src/Cryptol/Eval.hs index ac603180..b1107023 100644 --- a/src/Cryptol/Eval.hs +++ b/src/Cryptol/Eval.hs @@ -146,8 +146,6 @@ evalExpr env expr = case expr of EProofAbs _ e -> evalExpr env e EProofApp e -> evalExpr env e - ECast e _ty -> evalExpr env e - EWhere e ds -> {-# SCC "evalExpr->EWhere" #-} do env' <- evalDecls ds env evalExpr env' e diff --git a/src/Cryptol/Eval/Reference.hs b/src/Cryptol/Eval/Reference.hs index 1d585e3b..c1df1887 100644 --- a/src/Cryptol/Eval/Reference.hs +++ b/src/Cryptol/Eval/Reference.hs @@ -188,7 +188,6 @@ evalExpr env expr = EAbs n _ty b -> VFun (\v -> evalExpr (bindVar (n, v) env) b) EProofAbs _ e -> evalExpr env e EProofApp e -> evalExpr env e - ECast e _ty -> evalExpr env e EWhere e dgs -> evalExpr (foldl evalDeclGroup env dgs) e diff --git a/src/Cryptol/Transform/MonoValues.hs b/src/Cryptol/Transform/MonoValues.hs index d25d07d5..292fcff7 100644 --- a/src/Cryptol/Transform/MonoValues.hs +++ b/src/Cryptol/Transform/MonoValues.hs @@ -195,7 +195,6 @@ rewE rews = go EProofAbs x e -> EProofAbs x <$> go e - ECast e t -> ECast <$> go e <*> return t EWhere e dgs -> EWhere <$> go e <*> inLocal (mapM (rewDeclGroup rews) dgs) diff --git a/src/Cryptol/Transform/Specialize.hs b/src/Cryptol/Transform/Specialize.hs index 2a44d51e..810d67e8 100644 --- a/src/Cryptol/Transform/Specialize.hs +++ b/src/Cryptol/Transform/Specialize.hs @@ -99,8 +99,6 @@ specializeExpr expr = EAbs qn t e -> EAbs qn t <$> specializeExpr e EProofAbs p e -> EProofAbs p <$> specializeExpr e EProofApp {} -> specializeConst expr - ECast e t -> ECast <$> specializeExpr e <*> pure t - -- TODO: if typeOf e == t, then drop the coercion. EWhere e dgs -> specializeEWhere e dgs specializeMatch :: Match -> SpecM Match diff --git a/src/Cryptol/TypeCheck/AST.hs b/src/Cryptol/TypeCheck/AST.hs index c239e1d1..7e6f9324 100644 --- a/src/Cryptol/TypeCheck/AST.hs +++ b/src/Cryptol/TypeCheck/AST.hs @@ -92,23 +92,6 @@ data Expr = EList [Expr] Type -- ^ List value (with type of elements) | EProofApp Expr {- proof -} - {- | if e : t1, then cast e : t2 - as long as we can prove that 't1 = t2'. - We could express this in terms of a built-in constant. - `cast :: {a,b} (a =*= b) => a -> b` - - Using the constant is a bit verbose though, because we - end up with both the source and target type. So, instead - we use this language construct, which only stores the - target type, and the source type can be reconstructed - from the expression. - - Another way to think of this is simply as an expression - with an explicit type annotation. - -} - | ECast Expr Type - - | EWhere Expr [DeclGroup] deriving (Show, Generic, NFData) @@ -220,9 +203,6 @@ instance PP (WithNames Expr) where ETApp e t -> optParens (prec > 3) $ ppWP 3 e <+> ppWP 4 t - ECast e t -> optParens (prec > 0) - ( ppWP 2 e <+> text ":" <+> ppW t ) - EWhere e ds -> optParens (prec > 0) ( ppW e $$ text "where" $$ nest 2 (vcat (map ppW ds)) diff --git a/src/Cryptol/TypeCheck/Infer.hs b/src/Cryptol/TypeCheck/Infer.hs index 2f916aa6..0eb0a625 100644 --- a/src/Cryptol/TypeCheck/Infer.hs +++ b/src/Cryptol/TypeCheck/Infer.hs @@ -108,7 +108,8 @@ appTys expr ts tGoal = ExtVar s -> instantiateWith (EVar x) s ts CurSCC e t -> instantiateWith e (Forall [] [] t) ts - checkHasType e' t tGoal + checkHasType t tGoal + return e' P.ELit l -> do e <- desugarLiteral False l appTys e ts tGoal @@ -147,7 +148,8 @@ appTys expr ts tGoal = (ie,t) <- instantiateWith e' (Forall [] [] tGoal) ts -- XXX seems weird to need to do this, as t should be the same -- as tGoal - checkHasType ie t tGoal + checkHasType t tGoal + return ie inferTyParam :: P.TypeInst Name -> InferM (Located (Maybe Ident, Type)) @@ -186,7 +188,8 @@ checkE expr tGoal = ExtVar s -> instantiateWith (EVar x) s [] CurSCC e t -> return (e, t) - checkHasType e' t tGoal + checkHasType t tGoal + return e' P.ELit l -> (`checkE` tGoal) =<< desugarLiteral False l @@ -308,7 +311,8 @@ checkE expr tGoal = P.ETyped e t -> do tSig <- checkTypeOfKind t KType e' <- checkE e tSig - checkHasType e' tSig tGoal + checkHasType tSig tGoal + return e' P.ETypeVal t -> do l <- curRange @@ -455,12 +459,12 @@ expectFun = go [] newType (text "argument" <+> ordinal ix) KType -checkHasType :: Expr -> Type -> Type -> InferM Expr -checkHasType e inferredType givenType = +checkHasType :: Type -> Type -> InferM () +checkHasType inferredType givenType = do ps <- unify givenType inferredType case ps of - [] -> return e - _ -> newGoals CtExactType ps >> return (ECast e givenType) + [] -> return () + _ -> newGoals CtExactType ps checkFun :: Doc -> [P.Pattern Name] -> P.Expr Name -> Type -> InferM Expr diff --git a/src/Cryptol/TypeCheck/Instantiate.hs b/src/Cryptol/TypeCheck/Instantiate.hs index 4703b5e5..420c2626 100644 --- a/src/Cryptol/TypeCheck/Instantiate.hs +++ b/src/Cryptol/TypeCheck/Instantiate.hs @@ -75,15 +75,11 @@ instantiateWithPos e (Forall as ps t) ts = The arguments that are provided will be instantiated as requested, the rest will be instantiated with fresh type variables. -Note that we assume that type parameters are not normalized. -Generally, the resulting expression will look something like this: - -ECast (EProofApp (ETApp e t)) t1 +EProofApp (ETApp e t) where - There will be one `ETApp t` for each insantiated type parameter; - there will be one `EProofApp` for each constraint on the schema; - - there will be `ECast` if we had equality constraints from normalization. -} instantiateWithNames :: Expr -> Schema -> [Located (Ident,Type)] -> InferM (Expr,Type) diff --git a/src/Cryptol/TypeCheck/Sanity.hs b/src/Cryptol/TypeCheck/Sanity.hs index f8b3f8d0..afe48038 100644 --- a/src/Cryptol/TypeCheck/Sanity.hs +++ b/src/Cryptol/TypeCheck/Sanity.hs @@ -318,12 +318,6 @@ exprSchema expr = (_,_) -> reportError (BadProofTyVars as) - ECast e t -> - do checkTypeIs KType t - t1 <- exprType e - convertible t t1 - return (tMono t) - -- XXX: Check that defined things are disitnct? EWhere e dgs -> let go [] = exprSchema e diff --git a/src/Cryptol/TypeCheck/Solver/Selector.hs b/src/Cryptol/TypeCheck/Solver/Selector.hs index 819d2ae3..e35cfec3 100644 --- a/src/Cryptol/TypeCheck/Solver/Selector.hs +++ b/src/Cryptol/TypeCheck/Solver/Selector.hs @@ -40,20 +40,20 @@ listType n = return (tSeq (tNum n) elems) -improveSelector :: Selector -> Type -> InferM (Expr -> Expr) +improveSelector :: Selector -> Type -> InferM () improveSelector sel outerT = case sel of RecordSel _ mb -> cvt recordType mb TupleSel _ mb -> cvt tupleType mb ListSel _ mb -> cvt listType mb where - cvt _ Nothing = return id + cvt _ Nothing = return () cvt f (Just a) = do ty <- f a cs <- unify ty outerT case cs of - [] -> return id + [] -> return () _ -> do newGoals CtExactType cs - return (`ECast` ty) + return () {- | Compute the type of a field based on the selector. @@ -120,18 +120,17 @@ solveSelector sel outerT = tryHasGoal :: HasGoal -> InferM () tryHasGoal has | TCon (PC (PHas sel)) [ th, ft ] <- goal (hasGoal has) = - do outerCast <- improveSelector sel th + do improveSelector sel th outerT <- tNoUser `fmap` applySubst th mbInnerT <- solveSelector sel outerT case mbInnerT of Nothing -> addHasGoal has Just innerT -> do cs <- unify innerT ft - innerCast <- case cs of - [] -> return id - _ -> do newGoals CtExactType cs - return (`ECast` ft) - solveHasGoal (hasName has) (innerCast . (`ESel` sel) . outerCast) + case cs of + [] -> return () + _ -> newGoals CtExactType cs + solveHasGoal (hasName has) (`ESel` sel) | otherwise = panic "hasGoalSolved" [ "Unexpected selector proposition:" diff --git a/src/Cryptol/TypeCheck/Subst.hs b/src/Cryptol/TypeCheck/Subst.hs index 3ddc000e..06ae9734 100644 --- a/src/Cryptol/TypeCheck/Subst.hs +++ b/src/Cryptol/TypeCheck/Subst.hs @@ -255,7 +255,6 @@ instance TVars Expr where ETApp e t -> ETApp (go e) (apSubst su t) EProofAbs p e -> EProofAbs (apSubst su p) (go e) EProofApp e -> EProofApp (go e) - ECast e t -> ECast (go e) (apSubst su t) EVar {} -> expr diff --git a/src/Cryptol/TypeCheck/TypeOf.hs b/src/Cryptol/TypeCheck/TypeOf.hs index 69647b7d..2aa2026a 100644 --- a/src/Cryptol/TypeCheck/TypeOf.hs +++ b/src/Cryptol/TypeCheck/TypeOf.hs @@ -40,7 +40,6 @@ fastTypeOf tyenv expr = Just (_, t) -> t Nothing -> panic "Cryptol.TypeCheck.TypeOf.fastTypeOf" [ "EApp with non-function operator" ] - ECast _ t -> t -- Polymorphic fragment EVar {} -> polymorphic ETAbs {} -> polymorphic @@ -93,7 +92,6 @@ fastSchemaOf tyenv expr = EComp {} -> monomorphic EApp {} -> monomorphic EAbs {} -> monomorphic - ECast {} -> monomorphic where monomorphic = Forall [] [] (fastTypeOf tyenv expr)