From bcb7305dc83884593f27221e10fc755eabce10f0 Mon Sep 17 00:00:00 2001 From: Henry Blanchette Date: Fri, 20 May 2022 16:06:28 -0700 Subject: [PATCH 1/3] added new REPLException for when instance polymorphic variables not found during checking --- src/Cryptol/REPL/Monad.hs | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/Cryptol/REPL/Monad.hs b/src/Cryptol/REPL/Monad.hs index 5476d5f62..1f29c10c8 100644 --- a/src/Cryptol/REPL/Monad.hs +++ b/src/Cryptol/REPL/Monad.hs @@ -329,6 +329,7 @@ data REPLException | Unsupported Unsupported | ModuleSystemError NameDisp M.ModuleError | EvalPolyError T.Schema + | InstantiationsNotFound T.Schema | TypeNotTestable T.Type | EvalInParamModule [M.Name] | SBVError String @@ -358,6 +359,8 @@ instance PP REPLException where TooWide e -> pp e EvalPolyError s -> text "Cannot evaluate polymorphic value." $$ text "Type:" <+> pp s + InstantiationsNotFound s -> text "Cannot find instantiations for some type variables." + $$ text "Type:" <+> pp s TypeNotTestable t -> text "The expression is not of a testable type." $$ text "Type:" <+> pp t EvalInParamModule xs -> nest 2 $ vsep $ From 93367b22422b4027580679d817cff14e00699a8f Mon Sep 17 00:00:00 2001 From: Henry Blanchette Date: Fri, 20 May 2022 16:07:42 -0700 Subject: [PATCH 2/3] replEvalCheckedExpr now returns Maybe --- src/Cryptol/REPL/Command.hs | 51 ++++++++++++++++++++----------------- 1 file changed, 28 insertions(+), 23 deletions(-) diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs index d28ea1e60..b81ab5a41 100644 --- a/src/Cryptol/REPL/Command.hs +++ b/src/Cryptol/REPL/Command.hs @@ -431,10 +431,13 @@ qcExpr :: T.Schema -> REPL TestReport qcExpr qcMode exprDoc texpr schema = - do (val,ty) <- replEvalCheckedExpr texpr schema + do (val,ty) <- replEvalCheckedExpr texpr schema >>= \mb_res -> case mb_res of + Just res -> pure res + Nothing -> raise (EvalPolyError schema) testNum <- (toInteger :: Int -> Integer) <$> getKnownUser "tests" tenv <- E.envTypes . M.deEnv <$> getDynEnv let tyv = E.evalValType tenv ty + -- tv has already had polymorphism instantiated percentRef <- io $ newIORef Nothing testsRef <- io $ newIORef 0 @@ -801,7 +804,9 @@ proveSatExpr isSat rng exprDoc texpr schema = do printSafetyViolation :: T.Expr -> T.Schema -> [E.GenValue Concrete] -> REPL () printSafetyViolation texpr schema vs = catch - (do (fn,_) <- replEvalCheckedExpr texpr schema + (do fn <- replEvalCheckedExpr texpr schema >>= \mb_res -> case mb_res of + Just (fn, _) -> pure fn + Nothing -> raise (EvalPolyError schema) rEval (E.forceValue =<< foldM (\f v -> E.fromVFun Concrete f (pure v)) fn vs)) (\case EvalError eex -> rPutStrLn (show (pp eex)) @@ -1552,9 +1557,11 @@ replSpecExpr e = liftModuleCmd $ S.specialize e replEvalExpr :: P.Expr P.PName -> REPL (Concrete.Value, T.Type) replEvalExpr expr = do (_,def,sig) <- replCheckExpr expr - replEvalCheckedExpr def sig + replEvalCheckedExpr def sig >>= \mb_res -> case mb_res of + Just res -> pure res + Nothing -> raise (InstantiationsNotFound sig) -replEvalCheckedExpr :: T.Expr -> T.Schema -> REPL (Concrete.Value, T.Type) +replEvalCheckedExpr :: T.Expr -> T.Schema -> REPL (Maybe (Concrete.Value, T.Type)) replEvalCheckedExpr def sig = do validEvalContext def validEvalContext sig @@ -1562,29 +1569,27 @@ replEvalCheckedExpr def sig = s <- getTCSolver mbDef <- io (defaultReplExpr s def sig) - (def1,ty) <- - case mbDef of - Nothing -> raise (EvalPolyError sig) - Just (tys,def1) -> - do warnDefaults tys - let su = T.listParamSubst tys - return (def1, T.apSubst su (T.sType sig)) + case mbDef of + Nothing -> pure Nothing + Just (tys, def1) -> + do warnDefaults tys + let su = T.listParamSubst tys + let ty = T.apSubst su (T.sType sig) + whenDebug (rPutStrLn (dump def1)) - whenDebug (rPutStrLn (dump def1)) + tenv <- E.envTypes . M.deEnv <$> getDynEnv + let tyv = E.evalValType tenv ty - tenv <- E.envTypes . M.deEnv <$> getDynEnv - let tyv = E.evalValType tenv ty - - -- add "it" to the namespace via a new declaration - itVar <- bindItVariable tyv def1 + -- add "it" to the namespace via a new declaration + itVar <- bindItVariable tyv def1 - let itExpr = case getLoc def of - Nothing -> T.EVar itVar - Just rng -> T.ELocated rng (T.EVar itVar) + let itExpr = case getLoc def of + Nothing -> T.EVar itVar + Just rng -> T.ELocated rng (T.EVar itVar) - -- evaluate the it variable - val <- liftModuleCmd (rethrowEvalError . M.evalExpr itExpr) - return (val,ty) + -- evaluate the it variable + val <- liftModuleCmd (rethrowEvalError . M.evalExpr itExpr) + return $ Just (val,ty) where warnDefaults ts = case ts of From 07f2c5761017578488acb75a3d081cf6de7f6c2e Mon Sep 17 00:00:00 2001 From: Henry Blanchette Date: Fri, 20 May 2022 16:13:24 -0700 Subject: [PATCH 3/3] explanation for new exception: InstantiationsNotFound --- src/Cryptol/REPL/Command.hs | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs index b81ab5a41..4c5e0dd84 100644 --- a/src/Cryptol/REPL/Command.hs +++ b/src/Cryptol/REPL/Command.hs @@ -433,7 +433,11 @@ qcExpr :: qcExpr qcMode exprDoc texpr schema = do (val,ty) <- replEvalCheckedExpr texpr schema >>= \mb_res -> case mb_res of Just res -> pure res - Nothing -> raise (EvalPolyError schema) + -- If instance is not found, doesn't necessarily mean that there is no instance. + -- And due to nondeterminism in result from the solver (for finding solution to + -- numeric type constraints), `:check` can get to this exception sometimes, but + -- successfully find an instance and test with it other times. + Nothing -> raise (InstantiationsNotFound schema) testNum <- (toInteger :: Int -> Integer) <$> getKnownUser "tests" tenv <- E.envTypes . M.deEnv <$> getDynEnv let tyv = E.evalValType tenv ty @@ -1559,7 +1563,7 @@ replEvalExpr expr = do (_,def,sig) <- replCheckExpr expr replEvalCheckedExpr def sig >>= \mb_res -> case mb_res of Just res -> pure res - Nothing -> raise (InstantiationsNotFound sig) + Nothing -> raise (EvalPolyError sig) replEvalCheckedExpr :: T.Expr -> T.Schema -> REPL (Maybe (Concrete.Value, T.Type)) replEvalCheckedExpr def sig =