From 53cc08ece5b7d447fbee698b7fbc5b64b2a176eb Mon Sep 17 00:00:00 2001 From: "Iavor S. Diatchki" Date: Tue, 16 Dec 2014 15:18:49 -0800 Subject: [PATCH] Fix a bug with being inconsistent with how we make substitutions. --- src/Cryptol/TypeCheck/Solve.hs | 56 ++++++++++++++------- src/Cryptol/TypeCheck/Solver/CrySAT.hs | 4 +- src/Cryptol/TypeCheck/Solver/Numeric/SMT.hs | 10 +++- 3 files changed, 48 insertions(+), 22 deletions(-) diff --git a/src/Cryptol/TypeCheck/Solve.hs b/src/Cryptol/TypeCheck/Solve.hs index 3cb8d76d..696a5755 100644 --- a/src/Cryptol/TypeCheck/Solve.hs +++ b/src/Cryptol/TypeCheck/Solve.hs @@ -26,6 +26,7 @@ import qualified Cryptol.TypeCheck.Solver.Numeric.ImportExport as Num import qualified Cryptol.TypeCheck.Solver.CrySAT as Num import Cryptol.Utils.Panic(panic) import Cryptol.Parser.Position(rCombs) +import Cryptol.Utils.PP(pp) import Cryptol.TypeCheck.Defaulting(tryDefaultWith) @@ -35,6 +36,7 @@ import qualified Data.Map as Map import Data.Maybe ( fromMaybe ) import Data.Set ( Set ) import qualified Data.Set as Set +import qualified SimpleSMT as SMT -- Add additional constraints that ensure validity of type function. checkTypeFunction :: TFun -> [Type] -> [Prop] @@ -69,14 +71,29 @@ proveImplication lnam as ps gs = Right su -> return su Left err -> recordError err >> return emptySubst +debugBlock :: Num.Solver -> String -> IO a -> IO a +debugBlock s name m = + do let logger = Num.logger s + debugLog s name + SMT.logTab logger + a <- m + SMT.logUntab logger + return a + +debugLog :: Num.Solver -> String -> IO () +debugLog _ _ = return () + proveImplication' :: LQName -> [TParam] -> [Prop] -> [Goal] -> IO (Either Error Subst) proveImplication' lname as ps gs = Num.withSolver $ \s -> - do putStrLn "PROVING" - mapM_ print gs - putStrLn "--------------" + debugBlock s "proveImplication'" $ + do debugBlock s "assumes" $ + mapM_ (debugLog s . show . pp) ps + debugBlock s "shows" $ + mapM_ (debugLog s . show . pp . goal) gs + varMap <- Num.assumeProps s ps @@ -84,28 +101,29 @@ proveImplication' lname as ps gs = let su = importImps varMap imps gs0 = apSubst su gs - print su + debugBlock s "substitution" $ debugLog s (show (pp su)) if not possible then return $ Left $ UnusableFunction (thing lname) ps else -- XXX: Use imps do let gs1 = filter ((`notElem` ps) . goal) gs0 - gs2 <- simpGoals s gs1 - print gs2 + mb <- simpGoals s gs1 -- XXX: Minimize the goals invovled in the conflict - let gs3 = fromMaybe (gs1,emptySubst) gs2 + let gs3 = fromMaybe (gs1,emptySubst) mb case gs3 of ([],su1) -> return (Right su1) -- XXX: Do we need the su? - (us,_) -> return $ Left - $ UnsolvedDelcayedCt - $ DelayedCt { dctSource = lname - , dctForall = as - , dctAsmps = ps - , dctGoals = us - } + (us,su2) -> + do debugBlock s "2nd su:" (debugLog s . show . pp $ su2) + return $ Left + $ UnsolvedDelcayedCt + $ DelayedCt { dctSource = lname + , dctForall = as + , dctAsmps = ps + , dctGoals = us + } uniVars :: FVS a => a -> Set Num.Name uniVars = Set.map Num.exportVar . Set.filter isUni . fvs @@ -132,7 +150,10 @@ simpGoals s gs0 = case mbOk of Nothing -> return Nothing Just (nonDef,def,imps) -> - do let (su,extraProps) = importSplitImps varMap imps + do debugBlock s "simpGoals results (defined)" $ + mapM_ (debugLog s . ($ "") . SMT.showsSExpr . Num.smtpLinPart) def + + let (su,extraProps) = importSplitImps varMap imps let def1 = eliminateSimpleGEQ def toGoal = @@ -181,10 +202,7 @@ importSplitImps varMap = mk . partitionEithers . map imp . Map.toList (Just tv, Just ty) -> case tv of TVFree {} -> Left (tv,ty) - TVBound {} -> - case ty of - TVar tv2@(TVFree {}) -> Left (tv2, TVar tv) - _ -> Right (TVar tv =#= ty) + TVBound {} -> Right (TVar tv =#= ty) _ -> panic "importImps" [ "Failed to import:", show x, show e ] diff --git a/src/Cryptol/TypeCheck/Solver/CrySAT.hs b/src/Cryptol/TypeCheck/Solver/CrySAT.hs index b8a45372..f48e5eb1 100644 --- a/src/Cryptol/TypeCheck/Solver/CrySAT.hs +++ b/src/Cryptol/TypeCheck/Solver/CrySAT.hs @@ -4,8 +4,8 @@ module Cryptol.TypeCheck.Solver.CrySAT ( withScope, withSolver , assumeProps, checkDefined, simplifyProps , check - , Solver - , SMTProp, smtpOther + , Solver, logger + , SMTProp (..) ) where import qualified Cryptol.TypeCheck.AST as Cry diff --git a/src/Cryptol/TypeCheck/Solver/Numeric/SMT.hs b/src/Cryptol/TypeCheck/Solver/Numeric/SMT.hs index 60d8622d..4cf0f4e0 100644 --- a/src/Cryptol/TypeCheck/Solver/Numeric/SMT.hs +++ b/src/Cryptol/TypeCheck/Solver/Numeric/SMT.hs @@ -13,6 +13,7 @@ import Cryptol.TypeCheck.Solver.Numeric.AST import Cryptol.Utils.Panic ( panic ) import Control.Monad ( ap, guard ) +import Data.List ( partition ) import Data.Map ( Map ) import qualified Data.Map as Map import Data.Set ( Set ) @@ -144,8 +145,15 @@ smtFinName x = "fin_" ++ show (ppName x) -- | Given a model, compute a set of equations of the form `x = e`, -- that are impleied by the model. cryImproveModel :: SMT.Solver -> Set Name -> Map Name Expr -> IO (Map Name Expr) -cryImproveModel solver uniVars m = go Map.empty (Map.toList m) +cryImproveModel solver uniVars m = go Map.empty initialTodo + -- XXX: Hook in linRel where + -- Process unification variables first. That way, if we get `x = y`, we'd + -- prefer `x` to be a unificaiton variabl.e + initialTodo = uncurry (++) $ partition isUniVar $ Map.toList m + isUniVar (x,_) = x `Set.member` uniVars + + go done [] = return done go done ((x,e) : rest) = do yesK <- cryMustEqualK solver x e