From ec456b94471599dbfb31e0439031df8a62e4de3d Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Mon, 16 Oct 2017 14:05:01 -0700 Subject: [PATCH 1/5] Fix typo --- src/Cryptol/TypeCheck.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Cryptol/TypeCheck.hs b/src/Cryptol/TypeCheck.hs index 0e3d0d31..4b3bc0a9 100644 --- a/src/Cryptol/TypeCheck.hs +++ b/src/Cryptol/TypeCheck.hs @@ -63,7 +63,7 @@ tcExpr e0 inp = runInferM inp case res of ExtVar s -> return (EVar x, s) CurSCC e' t -> panic "Cryptol.TypeCheck.tcExpr" - [ "CurSCC outside binder checkig:" + [ "CurSCC outside binder checking:" , show e' , show t ] From 043334f8f9215b426dadf3f897658bcf51b752fc Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Mon, 16 Oct 2017 14:05:17 -0700 Subject: [PATCH 2/5] Name is `cryptol` nowadays --- tests/Main.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/Main.hs b/tests/Main.hs index 74c0ed9d..c8deab87 100644 --- a/tests/Main.hs +++ b/tests/Main.hs @@ -64,7 +64,7 @@ data Options = Options defaultOptions :: Options defaultOptions = Options - { optCryptol = "cryptol-2" + { optCryptol = "cryptol" , optOther = [] , optHelp = False , optResultDir = "output" From 6ba8849216786b4d20d61f29eac308928e30fb43 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Mon, 16 Oct 2017 14:05:31 -0700 Subject: [PATCH 3/5] Just reformat --- src/Cryptol/TypeCheck/Monad.hs | 21 +++++++++++---------- 1 file changed, 11 insertions(+), 10 deletions(-) diff --git a/src/Cryptol/TypeCheck/Monad.hs b/src/Cryptol/TypeCheck/Monad.hs index e02a86a3..0aa2ef00 100644 --- a/src/Cryptol/TypeCheck/Monad.hs +++ b/src/Cryptol/TypeCheck/Monad.hs @@ -79,6 +79,7 @@ data NameSeeds = NameSeeds } deriving (Show, Generic, NFData) -- | The initial seeds, used when checking a fresh program. +-- XXX: why does this start at 10? nameSeeds :: NameSeeds nameSeeds = NameSeeds { seedTVar = 10, seedGoal = 0 } @@ -102,16 +103,16 @@ runInferM :: TVars a => InferInput -> InferM a -> IO (InferOutput a) runInferM info (IM m) = SMT.withSolver (inpSolverConfig info) $ \solver -> do coutner <- newIORef 0 rec ro <- return RO { iRange = inpRange info - , iVars = Map.map ExtVar (inpVars info) - , iTVars = [] - , iTSyns = fmap mkExternal (inpTSyns info) - , iNewtypes = fmap mkExternal (inpNewtypes info) - , iSolvedHasLazy = iSolvedHas finalRW -- RECURSION - , iMonoBinds = inpMonoBinds info - , iSolver = solver - , iPrimNames = inpPrimNames info - , iSolveCounter = coutner - } + , iVars = Map.map ExtVar (inpVars info) + , iTVars = [] + , iTSyns = fmap mkExternal (inpTSyns info) + , iNewtypes = fmap mkExternal (inpNewtypes info) + , iSolvedHasLazy = iSolvedHas finalRW -- RECURSION + , iMonoBinds = inpMonoBinds info + , iSolver = solver + , iPrimNames = inpPrimNames info + , iSolveCounter = coutner + } (result, finalRW) <- runStateT rw $ runReaderT ro m -- RECURSION From a85ff3a54b305a659ff548c3816e6c0fea133bcf Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Mon, 16 Oct 2017 14:05:46 -0700 Subject: [PATCH 4/5] Add comments --- src/Cryptol/TypeCheck/InferTypes.hs | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/src/Cryptol/TypeCheck/InferTypes.hs b/src/Cryptol/TypeCheck/InferTypes.hs index e71aa9c8..3d470eb7 100644 --- a/src/Cryptol/TypeCheck/InferTypes.hs +++ b/src/Cryptol/TypeCheck/InferTypes.hs @@ -46,13 +46,17 @@ data SolverConfig = SolverConfig } deriving (Show, Generic, NFData) -- | The types of variables in the environment. -data VarType = ExtVar Schema -- ^ Known type - | CurSCC Expr Type -- ^ Part of current SCC +data VarType = ExtVar Schema + -- ^ Known type --- XXX: Temporary, until we figure out: --- 1. How to apply substitutions with normalization to the type Map --- 2. What are the strictness requirements --- (e.g., using Set results in a black hole) + | CurSCC {- LAZY -} Expr Type + {- ^ Part of current SCC. The expression will replace the + variable, after we are done with the SCC. In this way a + variable that gets generalized is replaced with an approproate + instantiations of itslef. -} + +-- XXX: Temporary, until we figure out, how to apply substitutions +-- with normalization to the type Map newtype Goals = Goals (Set Goal) -- Goals (TypeMap Goal) deriving (Show) From 942173b7f99a6f3f36d591fbfc2f168b148de776 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Mon, 16 Oct 2017 14:09:52 -0700 Subject: [PATCH 5/5] Add comments and fixes #473 --- src/Cryptol/TypeCheck/Infer.hs | 131 +++++++++++++++++++-------------- 1 file changed, 77 insertions(+), 54 deletions(-) diff --git a/src/Cryptol/TypeCheck/Infer.hs b/src/Cryptol/TypeCheck/Infer.hs index 2a3b9ce2..f6b55c56 100644 --- a/src/Cryptol/TypeCheck/Infer.hs +++ b/src/Cryptol/TypeCheck/Infer.hs @@ -36,6 +36,7 @@ import Cryptol.Utils.PP import qualified Data.Map as Map import Data.Map (Map) import qualified Data.Set as Set +import Data.List(foldl') import Data.Either(partitionEithers) import Data.Maybe(mapMaybe,isJust, fromMaybe) import Data.List(partition,find) @@ -185,8 +186,8 @@ checkE expr tGoal = P.EVar x -> do res <- lookupVar x (e',t) <- case res of - ExtVar s -> instantiateWith (EVar x) s [] - CurSCC e t -> return (e, t) + ExtVar s -> instantiateWith (EVar x) s [] + CurSCC e t -> return (e, t) checkHasType t tGoal return e' @@ -569,43 +570,50 @@ inferCArm armNum (m : ms) = -- be unaffected. inferBinds :: Bool -> Bool -> [P.Bind Name] -> InferM [Decl] inferBinds isTopLevel isRec binds = - mdo let dExpr (DExpr e) = e - dExpr DPrim = panic "[TypeCheck]" [ "primitive in a recursive group" ] - - exprMap = Map.fromList [ (x,inst (EVar x) (dExpr (dDefinition b))) - | b <- genBs, let x = dName b ] -- REC. - - inst e (ETAbs x e1) = inst (ETApp e (TVar (tpVar x))) e1 - inst e (EProofAbs _ e1) = inst (EProofApp e) e1 - inst e _ = e - - -- when mono-binds is enabled, and we're not checking top-level - -- declarations, mark all bindings lacking signatures as monomorphic - monoBinds <- getMonoBinds - let binds' | monoBinds && not isTopLevel = sigs ++ monos - | otherwise = binds - - (sigs,noSigs) = partition (isJust . P.bSignature) binds - monos = [ b { P.bMono = True } | b <- noSigs ] - - - ((doneBs, genCandidates), cs) <- - collectGoals $ + do -- when mono-binds is enabled, and we're not checking top-level + -- declarations, mark all bindings lacking signatures as monomorphic + monoBinds <- getMonoBinds + let (sigs,noSigs) = partition (isJust . P.bSignature) binds + monos = [ b { P.bMono = True } | b <- noSigs ] + binds' | monoBinds && not isTopLevel = sigs ++ monos + | otherwise = binds + check exprMap = {- Guess type is here, because while we check user supplied signatures we may generate additional constraints. For example, `x - y` would generate an additional constraint `x >= y`. -} - do (newEnv,todos) <- unzip `fmap` mapM (guessType exprMap) binds' - let extEnv = if isRec then withVarTypes newEnv else id + do (newEnv,todos) <- unzip `fmap` mapM (guessType exprMap) binds' + let extEnv = if isRec then withVarTypes newEnv else id + + extEnv $ + do let (sigsAndMonos,noSigGen) = partitionEithers todos + genCs <- sequence noSigGen + done <- sequence sigsAndMonos + simplifyAllConstraints + return (done, genCs) + + rec + let exprMap = Map.fromList $ map monoUse genBs + ((doneBs, genCandidates), cs) <- collectGoals (check exprMap) + genBs <- generalize genCandidates cs + + return (doneBs ++ genBs) + + where + monoUse d = (x, withQs) + where + x = dName d + as = sVars (dSignature d) + qs = sProps (dSignature d) + + appT e a = ETApp e (TVar (tpVar a)) + appP e _ = EProofApp e + + withTys = foldl' appT (EVar x) as + withQs = foldl' appP withTys qs + + - extEnv $ - do let (sigsAndMonos,noSigGen) = partitionEithers todos - genCs <- sequence noSigGen - done <- sequence sigsAndMonos - simplifyAllConstraints - return (done, genCs) - genBs <- generalize genCandidates cs -- RECURSION - return (doneBs ++ genBs) {- | Come up with a type for recursive calls to a function, and decide @@ -659,12 +667,14 @@ generalize [] gs0 = generalize bs0 gs0 = - do gs <- forM gs0 $ \g -> applySubst g - - -- XXX: Why would these bindings have signatures?? - bs <- forM bs0 $ \b -> do s <- applySubst (dSignature b) - return b { dSignature = s } + do {- First, we apply the accumulating substituion to the goals + and the inferred types, to ensure that we have the most up + to date information. -} + gs <- forM gs0 $ \g -> applySubst g + bs <- forM bs0 $ \b -> do s <- applySubst (dSignature b) + return b { dSignature = s } + -- Next, we figure out which of the free variables need to be generalized let goalFVS g = Set.filter isFreeTV $ fvs $ goal g inGoals = Set.unions $ map goalFVS gs inSigs = Set.filter isFreeTV $ fvs $ map dSignature bs @@ -672,27 +682,49 @@ generalize bs0 gs0 = asmpVs <- varsWithAsmps - - let gen0 = Set.difference candidates asmpVs stays g = any (`Set.member` gen0) $ Set.toList $ goalFVS g (here0,later) = partition stays gs + addGoals later -- these ones we keep around for to solve later - -- Figure out what might be ambigious + + {- Figure out what might be ambigious. We count something as + ambiguous if it is to be generalized, but does not appear in + the any of the inferred types. Things like that of kind `*` + are certainly ambiguous because we don't have any fancy type functions + on them. However, things of kind `#` may not actually be mabiguos. + -} let (maybeAmbig, ambig) = partition ((KNum ==) . kindOf) $ Set.toList $ Set.difference gen0 inSigs - when (not (null ambig)) $ recordError $ AmbiguousType $ map dName bs + {- See if we might be able to default some of the potentially ambiguous + numeric vairables using the constraints that will be part of the + newly generalized schema. Note that we only use the `here0` constrains + as these should be the only ones that might mention the potentially + ambiguous variable. + + XXX: It is not clear if we should do this, or simply leave the + variables as is. After all, they might not actually be ambiugous... + -} let (as0,here1,defSu,ws) = improveByDefaultingWithPure maybeAmbig here0 mapM_ recordWarning ws let here = map goal here1 + + {- This is the variables we'll be generalizing: + * any ones that survived the defaulting + * and vars in the inferred types that do not appear anywhere else. -} let as = as0 ++ Set.toList (Set.difference inSigs asmpVs) asPs = [ TParam { tpUnique = x, tpKind = k, tpName = Nothing } | TVFree x k _ _ <- as ] + + {- Finally, we replace free variables with bound ones, and fix-up + the definitions as needed to reflect that we are now working + with polymorphic things. For example, apply each occurance to the + type parameters. -} totSu <- getSubst let su = listSubst (zip as (map (TVar . tpVar) asPs)) @@ defSu @@ totSu @@ -706,25 +738,16 @@ generalize bs0 gs0 = $ apSubst su $ sType $ dSignature d } - addGoals later return (map genB bs) - +-- | Check a monomrphic binding. checkMonoB :: P.Bind Name -> Type -> InferM Decl checkMonoB b t = inRangeMb (getLoc b) $ case thing (P.bDef b) of - P.DPrim -> - return Decl { dName = thing (P.bName b) - , dSignature = Forall [] [] t - , dDefinition = DPrim - , dPragmas = P.bPragmas b - , dInfix = P.bInfix b - , dFixity = P.bFixity b - , dDoc = P.bDoc b - } + P.DPrim -> panic "checkMonoB" ["Primitive with no signature?"] P.DExpr e -> do e1 <- checkFun (pp (thing (P.bName b))) (P.bParams b) e t