diff options
| -rw-r--r-- | compiler/typecheck/TcInteract.lhs | 118 | ||||
| -rw-r--r-- | compiler/typecheck/TcSMonad.lhs | 10 | ||||
| -rw-r--r-- | compiler/typecheck/TcTypeNats.hs | 765 |
3 files changed, 881 insertions, 12 deletions
diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs index 42e04650c1..02c5866018 100644 --- a/compiler/typecheck/TcInteract.lhs +++ b/compiler/typecheck/TcInteract.lhs @@ -14,7 +14,6 @@ import VarSet import Type import Unify import InstEnv( lookupInstEnv, instanceDFunId ) -import CoAxiom(sfInteractTop, sfInteractInert) import Var import TcType @@ -33,6 +32,7 @@ import FamInstEnv ( FamInstEnvs, instNewTyConTF_maybe ) import TcEvidence import Outputable +import TcTypeNats import TcRnTypes import TcErrors import TcSMonad @@ -50,6 +50,8 @@ import Unique( hasKey ) import FastString ( sLit, fsLit ) import DynFlags import Util + +import System.IO(hPutStrLn,stderr) \end{code} ********************************************************************** @@ -87,9 +89,9 @@ solveInteractGiven loc old_fsks givens | null givens -- Shortcut for common case = return (True, old_fsks) | otherwise - = do { implics1 <- solveInteract fsk_bag + = do { implics1 <- solveInteractWithExtern True fsk_bag - ; (no_eqs, more_fsks, implics2) <- getGivenInfo (solveInteract given_bag) + ; (no_eqs, more_fsks, implics2) <- getGivenInfo (solveInteractWithExtern True given_bag) ; MASSERT( isEmptyBag implics1 && isEmptyBag implics2 ) -- empty implics because we discard Given equalities between -- foralls (see Note [Do not decompose given polytype equalities] @@ -115,11 +117,16 @@ solveInteractGiven loc old_fsks givens -- The main solver loop implements Note [Basic Simplifier Plan] --------------------------------------------------------------- + solveInteract :: Cts -> TcS (Bag Implication) +solveInteract = solveInteractWithExtern False + +solveInteractWithExtern :: Bool -- ^ Are we in the given stage? + -> Cts -> TcS (Bag Implication) -- Returns the final InertSet in TcS -- Has no effect on work-list or residual-iplications -solveInteract cts - = {-# SCC "solveInteract" #-} +solveInteractWithExtern inGivenStage cts + = {-# SCC "solveInteractWithExtern" #-} withWorkList cts $ do { dyn_flags <- getDynFlags ; solve_loop (maxSubGoalDepth dyn_flags) } @@ -129,12 +136,111 @@ solveInteract cts do { sel <- selectNextWorkItem max_depth ; case sel of NoWorkRemaining -- Done, successfuly (modulo frozen) - -> return () + -> do moreWork <- interactExternSolver inGivenStage + if moreWork then solve_loop max_depth + else return () MaxDepthExceeded cnt ct -- Failure, depth exceeded -> wrapErrTcS $ solverDepthErrorTcS cnt (ctEvidence ct) NextWorkItem ct -- More work, loop around! -> do { runSolverPipeline thePipeline ct; solve_loop max_depth } } +interactExternSolver :: Bool -- ^ Are we in given stage? + -> TcS Bool -- ^ Did we generatew new work. +interactExternSolver inGivenStage = + do extSol $ hPutStrLn stderr $ "=== EXT SOL: " ++ (if inGivenStage then "[G]" else "[W/D]") + iSet <- getTcSInerts + let iCans = inert_cans iSet + + relevantCt + | inGivenStage = isGivenCt + | otherwise = not . isGivenCt + + (relFeqs, otherFeqs) = partitionFunEqs relevantCt (inert_funeqs iCans) + relList = bagToList relFeqs + othersList = funEqsToList otherFeqs + + eqs = inert_eqs iCans + + {- `survived` should be a sub-set of the inert funeqs. + This function rebuilds the inert set, after we've remove a constraint + (e.g., because they were solved, or caused a contradiciton. -} + + rebuildInerts survived = + do let new_feqs = foldr addCt otherFeqs survived + new_iCans = iCans { inert_funeqs = new_feqs } + setTcSInerts iSet { inert_cans = new_iCans } + + -- Sanity checking: + when (inGivenStage && not (null othersList)) $ + panicTcS (text "Non given constraints in given stage" $$ + (vcat $ map ppr othersList)) + + + withSol $ \sol -> + do extSol $ extSolAssert sol othersList + + + res <- extSol $ extSolImprove sol inGivenStage relList + case res of + + -- Kick-out constraints that lead to a contradiciton + -- and add them as insoluable. + ExtSolContradiction bad_feqs ok_feqs -> + do rebuildInerts ok_feqs + mapM_ emitInsoluble bad_feqs + return False + + -- Consistent + ExtSolOk newWork + + -- We found some new work to do. + | let reallyNew + | inGivenStage = newWork + | otherwise = filter (notKnownEq eqs) newWork + , not (null reallyNew) -> + do updWorkListTcS (extendWorkListEqs reallyNew) + return True + + -- Nothing else to do. + | inGivenStage -> return False + + -- No new work, try to solve wanted constraints. + | otherwise -> + do let (wanteds, derived) = partition isWantedCt relList + (solved, unsolved) <- extSol $ extSolSolve sol wanteds + case solved of + [] -> return False -- Shortcut for common case. + _ -> do rebuildInerts (unsolved ++ derived) + let setEv (ev,ct) = + setEvBind (ctev_evar (cc_ev ct)) ev + mapM_ setEv solved + return False + + + where + notKnownEq eqs ct = + case getEqPredTys_maybe (ctPred ct) of + Just (_,tvt,ty) + | Just tv <- getTyVar_maybe tvt -> + all (not . tcEqType ty) + [ t | CTyEqCan { cc_rhs = t } <- findTyEqs eqs tv ] + _ -> True + + + addCt ct mp = + case ct of + CFunEqCan { cc_fun = tc, cc_tyargs = tys } -> addFunEq mp tc tys ct + _ -> panic "Not FunEq constraint while rebuilding external work." + + withSol k = do s <- extSol (newExternalSolver "cvc4" + [ "--incremental", "--lang=smtlib2" ]) + + a <- k s + extSol (extSolStop s) + return a + + + type WorkItem = Ct type SimplifierStage = WorkItem -> TcS StopOrContinue diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs index 898e2b8c13..60ff5d26c8 100644 --- a/compiler/typecheck/TcSMonad.lhs +++ b/compiler/typecheck/TcSMonad.lhs @@ -76,6 +76,7 @@ module TcSMonad ( findFunEq, findTyEqs, findDict, findDictsByClass, addDict, addDictsByClass, delDict, partitionDicts, findFunEqsByTyCon, findFunEqs, addFunEq, replaceFunEqs, partitionFunEqs, + emptyFunEqs, funEqsToList, instDFunType, -- Instantiation newFlexiTcSTy, instFlexiTcS, instFlexiTcSHelperTcS, @@ -84,6 +85,8 @@ module TcSMonad ( Untouchables, isTouchableMetaTyVarTcS, isFilledMetaTyVar_maybe, zonkTyVarsAndFV, + extSol, + getDefaultInfo, getDynFlags, getGlobalRdrEnvTcS, matchFam, matchOpenFam, @@ -1947,3 +1950,10 @@ deferTcSForAllEq role loc (tvs1,body1) (tvs2,body2) } \end{code} +Interaction with an External SMT Solver +--------------------------------------- + +\begin{code} +extSol :: IO a -> TcS a +extSol m = TcS $ \_ -> liftIO m +\end{code} diff --git a/compiler/typecheck/TcTypeNats.hs b/compiler/typecheck/TcTypeNats.hs index 37fc6e0cdb..bd60f8f053 100644 --- a/compiler/typecheck/TcTypeNats.hs +++ b/compiler/typecheck/TcTypeNats.hs @@ -2,17 +2,22 @@ module TcTypeNats ( typeNatTyCons , typeNatCoAxiomRules , BuiltInSynFamily(..) + , ExternalSolver(..), ExtSolRes(..), newExternalSolver ) where import Type import Pair import TcType ( TcType, tcEqType ) +import TcEvidence ( mkTcAxiomRuleCo, EvTerm(..) ) import TyCon ( TyCon, SynTyConRhs(..), mkSynTyCon, TyConParent(..) ) import Coercion ( Role(..) ) -import TcRnTypes ( Xi ) +import TcRnTypes ( Xi, Ct(..), ctPred, CtEvidence(..), mkNonCanonical + , CtLoc, ctLoc, isGivenCt ) import CoAxiom ( CoAxiomRule(..), BuiltInSynFamily(..) ) -import Name ( Name, BuiltInSyntax(..) ) -import TysWiredIn ( typeNatKind, typeSymbolKind +import Name ( Name, BuiltInSyntax(..), nameOccName, nameUnique ) +import OccName ( occNameString ) +import Var ( tyVarName, tyVarKind ) +import TysWiredIn ( typeNatKind, typeSymbolKind, typeNatKindCon , mkWiredInTyConName , promotedBoolTyCon , promotedFalseDataCon, promotedTrueDataCon @@ -31,9 +36,24 @@ import PrelNames ( gHC_TYPELITS , typeNatCmpTyFamNameKey , typeSymbolCmpTyFamNameKey ) +import Panic (panic) import FastString ( FastString, fsLit ) +import UniqFM ( UniqFM, emptyUFM, unitUFM, plusUFM, eltsUFM ) +import Data.Map (Map) import qualified Data.Map as Map -import Data.Maybe ( isJust ) +import Data.Maybe ( isJust, mapMaybe ) +import Data.Char ( isSpace ) +import Data.List ( unfoldr, foldl', partition, sortBy, groupBy ) +import Data.IORef ( IORef, newIORef, atomicModifyIORef', + atomicModifyIORef, modifyIORef' + , readIORef + ) +import Control.Monad ( forever, msum ) +import Control.Concurrent ( forkIO ) +import qualified Control.Exception as X +import System.Process ( runInteractiveProcess, waitForProcess ) +import System.IO ( hPutStrLn, hFlush, hGetContents, hGetLine, + stderr ) {------------------------------------------------------------------------------- Built-in type constructors for functions on type-lelve nats @@ -270,9 +290,27 @@ typeNatCoAxiomRules = Map.fromList $ map (\x -> (coaxrName x, x)) ] +decisionProcedure :: String -> CoAxiomRule +decisionProcedure name = + CoAxiomRule + { coaxrName = fsLit name + , coaxrTypeArity = 2 + , coaxrAsmpRoles = [] + , coaxrRole = Nominal + , coaxrProves = \ts cs -> + case (ts,cs) of + ([s,t],[]) -> return (s === t) + _ -> Nothing + } -{------------------------------------------------------------------------------- -Various utilities for making axioms and types + +evBySMT :: String -> (Type, Type) -> EvTerm +evBySMT name (t1,t2) = + EvCoercion $ mkTcAxiomRuleCo (decisionProcedure name) [t1,t2] [] + + + +-- Various utilities for making axioms and types -------------------------------------------------------------------------------} (.+.) :: Type -> Type -> Type @@ -681,7 +719,722 @@ genLog x base = Just (exactLoop 0 x) +-------------------------------------------------------------------------------- +-- Interface + +data ExternalSolver = ExternalSolver + { extSolAssert :: [Ct] -> IO () + -- ^ Add some assertions. + -- Changes assertions. + + , extSolImprove :: Bool {- are we in the given stage -} + -> [Ct] -> IO ExtSolRes + -- ^ Check for consistency and new work. + -- Does not change assertions. + + , extSolSolve :: [Ct] -> IO ([(EvTerm,Ct)], [Ct]) + -- ^ Solve some constraints. + -- Does not change assertions. + + , extSolStop :: IO () + -- ^ Exit the solver. + -- The solver should not be used after this is called. + } + +data ExtSolRes + = ExtSolContradiction {- inconsistent -} [Ct] + {- all others -} [Ct] + -- ^ There is no model for assertions. + + | ExtSolOk [Ct] + -- ^ New work (facts that will hold in all models) + +-------------------------------------------------------------------------------- +-- Concrete implementation + +newExternalSolver :: FilePath -> [String] -> IO ExternalSolver +newExternalSolver exe opts = + do proc <- startSolverProcess exe opts + + -- Prep the solver + solverSimpleCmd proc [ "set-option", ":print-success", "true" ] + solverSimpleCmd proc [ "set-option", ":produce-models", "true" ] + solverSimpleCmd proc [ "set-logic", "QF_LIA" ] + + viRef <- newIORef emptyVarInfo + + let dbg = solverDebug proc + + return ExternalSolver + { extSolAssert = \cts -> + do dbg "=== ASSERT ===" + (_,ours) <- solverPrepare proc viRef cts + let expr (_,e,_) = e + mapM_ (solverAssume proc . expr) ours + mapM_ (solverDebug proc . show . expr) ours + + , extSolImprove = \b cts -> do dbg "=== IMPROVE ===" + solverImprove proc viRef b cts + + , extSolSolve = \cts -> do dbg "=== SOLVE ===" + solverSimplify proc viRef cts + + , extSolStop = solverStop proc + } + +mkNewFact :: CtLoc -> Bool -> (Type,Type) -> CtEvidence +mkNewFact newLoc withEv (t1,t2) + | withEv = CtGiven { ctev_pred = newPred + , ctev_evtm = evBySMT "SMT" (t1,t2) + , ctev_loc = newLoc + } + | otherwise = CtDerived { ctev_pred = newPred + , ctev_loc = newLoc + } + where + newPred = mkEqPred t1 t2 + +-- A command with no interesting result. +solverAckCmd :: SolverProcess -> SExpr -> IO () +solverAckCmd proc c = + do res <- solverDo proc c + case res of + SAtom "success" -> return () + _ -> fail $ unlines + [ "Unexpected result from the SMT solver:" + , " Expected: success" + , " Result: " ++ renderSExpr res "" + ] + +-- A command entirely made out of atoms, with no interesting result. +solverSimpleCmd :: SolverProcess -> [String] -> IO () +solverSimpleCmd proc = solverAckCmd proc . SList . map SAtom + + + +-- Checkpoint state +solverPush :: SolverProcess -> IORef VarInfo -> IO () +solverPush proc viRef = + do solverSimpleCmd proc [ "push", "1" ] + modifyIORef' viRef startScope + +-- Restore to last check-point +solverPop :: SolverProcess -> IORef VarInfo -> IO () +solverPop proc viRef = + do solverSimpleCmd proc [ "pop", "1" ] + modifyIORef' viRef endScope + + +-- Assume a fact +solverAssume :: SolverProcess -> SExpr -> IO () +solverAssume proc e = solverAckCmd proc $ SList [ SAtom "assert", e ] + +-- Declare a new variable +solverDeclare :: SolverProcess -> IORef VarInfo -> (TyVar, String, Ty) -> IO () +solverDeclare proc viRef (tv,x,ty) = + do status <- atomicModifyIORef' viRef (declareVar tv) + case status of + Declared -> return () + Undeclared -> + do solverAckCmd proc $ + SList [SAtom "declare-fun", SAtom x, SList [], smtTy ty] + mapM_ (solverAssume proc) (smtExtraConstraints x ty) + +data SmtRes = Unsat | Unknown | Sat + +-- Check if assumptions are consistent. Does not return a model. +solverCheck :: SolverProcess -> IO SmtRes +solverCheck proc = + do res <- solverDo proc (SList [ SAtom "check-sat" ]) + case res of + SAtom "unsat" -> return Unsat + SAtom "unknown" -> return Unknown + SAtom "sat" -> return Sat + _ -> fail $ unlines + [ "Unexpected result from the SMT solver:" + , " Expected: unsat, unknown, or sat" + , " Result: " ++ renderSExpr res "" + ] + +-- Prove something by concluding that a counter-example is impossible. +solverProve :: SolverProcess -> IORef VarInfo -> SExpr -> IO Bool +solverProve proc viRef e = + debug $ + do solverPush proc viRef + solverAssume proc $ SList [ SAtom "not", e ] + res <- solverCheck proc + solverPop proc viRef + case res of + Unsat -> return True + _ -> return False + + where + debug m = do solverDebug proc ("Prove: " ++ show e) + solverDebugNext proc + res <- m + solverDebug proc (show res) + solverDebugPrev proc + return res + +-- Get values for the variables that are in scope. +solverGetModel :: SolverProcess -> VarInfo -> IO [(String,SExpr)] +solverGetModel proc vi = + do res <- solverDo proc + $ SList [ SAtom "get-value", SList [ SAtom v | v <- inScope vi ] ] + case res of + SList xs -> return [ (x,v) | SList [ SAtom x, v ] <- xs ] + _ -> fail $ unlines + [ "Unexpected response from the SMT solver:" + , " Exptected: a list" + , " Result: " ++ renderSExpr res "" + ] + +{- Try to generalize some facts for a model. + +In particular, we look for facts of the form: + * x = K, where `K` is a constant, and + * x = y, where `y` is a variable. + +Returns only the new facts. +-} +solverImproveModel :: SolverProcess -> IORef VarInfo -> + [(String,SExpr)] -> IO [ (String,SExpr) ] +solverImproveModel proc viRef imps = + do xs <- constEq [] imps + solverDebug proc $ "Improvements: " ++ unwords [ x ++ " = " ++ renderSExpr e "," | (x,e) <- xs ] + return xs + where + + constEq imps [] = return imps + constEq imps ((x,v) : more) = + -- First we check if this is the only possible concrete value for `x`: + do proved <- solverProve proc viRef (SList [ SAtom "=", SAtom x, v ]) + if proved + then constEq ((x,v) : imps) more + -- If two variables `x` and `y` have the same value in this model, + -- then we check if they must be equal in all models. + else let (candidates,others) = partition ((== v) . snd) more + in varEq x imps others candidates + + + varEq _ imps more [] = constEq imps more + varEq x imps more (def@(y,_) : ys) = + do let e = SAtom y + -- Check if `x` and `y` must be the same in all models. + proved <- solverProve proc viRef (SList [ SAtom "=", SAtom x, e ]) + if proved + then varEq x ((x, e) : imps) more ys + else varEq x imps (def : more) ys + + +-------------------------------------------------------------------------------- +-- Higher level operations on collections of constraints. + + +-- Identify our constraints, and declare their variables in the current scope. +solverPrepare :: SolverProcess -> IORef VarInfo -> + [Ct] -> IO ([Ct], [(Ct,SExpr,Maybe TyVar)]) +solverPrepare proc viRef = go [] [] + where + go others ours [] = return (others, ours) + go others ours (ct : cts) = + case knownCt ct of + Just (vars,e,mbV) -> + do let g = if isGivenCt ct then "[G] " else "[W/D] " + solverDebug proc (g ++ show e) + mapM_ (solverDeclare proc viRef) (eltsUFM vars) + go others ((ct,e,mbV) : ours) cts + Nothing -> + go (ct : others) ours cts + + +{- +Check a list of constraints for consistency, and computer derived work. +Does not affect set off assertions in the solver. +-} +solverImprove :: SolverProcess -> IORef VarInfo + -> Bool -- ^ Should we generate given constraints? + -- If not, we generate derived ones. + -> [Ct] + -> IO ExtSolRes +solverImprove proc viRef withEv cts = + do push -- declare variables + (others,ours') <- solverPrepare proc viRef cts + let ours = [ (ct,e) | (ct,e,_) <- ours' ] + case ours of + [] -> do pop -- declarations + return (ExtSolOk []) + + (oneOfOurs,_) : _ -> + do push -- assumptions + mapM_ (assume . snd) ours + status <- check + + res <- + case status of + + -- Inconsistent: find a smaller example, then stop. + Unsat -> + do pop -- assumptions + mbRes <- solverFindConstraidction proc viRef others ours + case mbRes of + Nothing -> + fail "Bug: Failed to reporoduce contradiciton." + Just (core,rest) -> + return $ ExtSolContradiction core rest + + -- We don't know: treat as consistent. + Unknown -> do pop -- assumptions + return (ExtSolOk []) + + -- Consistent: try to compute derived work. + Sat -> + do m <- solverGetModel proc =<< readIORef viRef + + imps <- solverImproveModel proc viRef m + pop -- assumptions + + vi <- readIORef viRef + + let loc = ctLoc oneOfOurs -- XXX: Better location? + toCt (x,e) = + do tv <- varToTyVar x vi + ty <- sExprToType vi e + return $ mkNonCanonical + $ mkNewFact loc withEv (mkTyVarTy tv, ty) + return $ ExtSolOk $ mapMaybe toCt imps + + pop -- declarations + return res + where + push = solverPush proc viRef + pop = solverPop proc viRef + assume = solverAssume proc + check = solverCheck proc + + +{- Identify a sub-set of constraints that leads to a contradiction. + +We call this when we find out that a collection of constraints is +inconsistent: instead of marking them _all_ as insoluable, +we identify a sub-set that is the real cause of the problem. + +* Assumes that the variables in our constarints have been declared. +* Does not change the assertions in the solver. +-} +solverFindConstraidction :: + SolverProcess -> -- Solver + IORef VarInfo -> -- Scoping of variables + [Ct] -> -- Constraints not relevant to us + [(Ct,SExpr)] -> -- Our constraints + IO (Maybe ( [Ct] -- Constraints that cause a contradiciotn + , [Ct] -- All other constraints (both others and ours) + ) + ) +solverFindConstraidction proc viRef others ours = + do push -- scope for `needed` + minimize others [] ours + + where + check = solverCheck proc + push = solverPush proc viRef + pop = solverPop proc viRef + assume = solverAssume proc + + minimize notNeeded needed maybeNeeded = + do res <- check + case res of + Unsat -> do pop -- remove `needed` scope. + return $ Just (needed, map fst maybeNeeded ++ notNeeded) + _ -> do push -- scope for `maybeNeeded` + search notNeeded needed [] maybeNeeded + + search _ needed _ [] = + do pop -- Remove `maybeNeeded` + pop -- Remove `needed` + case needed of + [] -> return Nothing -- No definite contradictions + _ -> fail "Bug: we found a contradiction, and then lost it!" + + search notNeeded needed maybeNeeded ((ct,e) : more) = + do assume e -- Add to `maybeNeeded` + res <- check + case res of + + Unsat -> -- We found a contradiction using `needed` and `maybeNeeded`. + do pop -- remove `maybeNedded` + assume e -- add to `needed` + minimize (map fst more ++ notNeeded) (ct : needed) maybeNeeded + + -- No contradiction, keep searching. + _ -> search notNeeded needed ((ct,e) : maybeNeeded) more + + + +{- Try to solve as much as possible from the given list of constraints. +Returns the solved constraints (with evidence), and all other constraints. +-} +{- +Note [In What Order to Solve Wanteds?] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Consider this example: + +ex4 :: p a -> p b -> p ((a + a) + b) -> p (2 * a + b) +ex4 _ = id + +A: a + a = u +B: x + b = v +C: 2 * a = w +D: w + b = v + +If we solve `B` or `D` first, then we are essnetially done, +as all the others can be substituted within each other. + +However, what if we happen to consider `C` first? + +(A,B,D) => C + +This goal is essentially: + +((a + a) + b ~ (2 * a) + b) => (a + a) ~ 2 * a + +which can be proved by cancelling `b` on both sides. + +Now, we are left with just `A,B,D`, which amounts to having +to prove: + +(a + a) + b ~ w + b + +We can't do this because we've lost the information about `w`. +To avoid this, we first try to solve equations that have the same varibal +on the RHS (e.g., F xs ~ a, G ys ~ a). + +-} + + +{- +Note [Incompleteness of the General Approach] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Another tricky example, which illustrates the incompleteness of +the general method: + +x :: f (n + 2) +x = undefined + +y :: f (m + 1) +y = x + +The definition for `x` is accepted, but `y` is rejected. +The reason is that to accept it we need to infer that `m` must +be instantiated to `n + 1`. The current system does not support this +kind of improvement, because it only ever tries to instantiate variables +to constants or other variables and here we need to instantiate `m` +with a more complex expression, namely, `n + 1`. +-} + + +solverSimplify :: SolverProcess -> IORef VarInfo -> + [Ct] -> IO ([(EvTerm,Ct)], [Ct]) +solverSimplify proc viRef cts = + do push -- `unsolved` scope + (others,ours) <- solverPrepare proc viRef cts + let r = reorder ours + solverDebug proc "Reordered:" + mapM_ (solverDebug proc . show . snd) r + go others [] r + where + push = solverPush proc viRef + pop = solverPop proc viRef + assume = solverAssume proc + + go unsolved solved [] = + do pop -- remove `unsolved` scope + return (solved, unsolved) + + go unsolved solved ((ct,e) : more) = + do push -- Temporarily assume everything else. + solverDebug proc "Temporary assuming:" + solverDebugNext proc + mapM_ (assume . snd) more + mapM_ (solverDebug proc . show . snd) more + solverDebugPrev proc + proved <- solverProve proc viRef e + pop + if proved + then let ev = evBySMT "SMT" $ getEqPredTys $ ctPred ct + in go unsolved ((ev,ct) : solved) more + else do assume e -- add to `unsolved` + go (ct : unsolved) solved more + + reorder = map dropVar + . concat + . sortBy longer -- most vars first + . groupBy sameVars -- join together eqns for same variable + . sortBy cmpVars -- first sort by variable + + where + cmpVars (_,_,v1) (_,_,v2) = compare v1 v2 + sameVars (_,_,v1) (_,_,v2) = v1 == v2 + longer xs ys = compare (length ys) (length xs) + dropVar (ct,e,_) = (ct,e) + + + + + +-------------------------------------------------------------------------------- + +smtTy :: Ty -> SExpr +smtTy ty = + SAtom $ + case ty of + TNat -> "Int" + TBool -> "Bool" + +smtExtraConstraints :: String -> Ty -> [SExpr] +smtExtraConstraints x ty = + case ty of + TNat -> [ smtLeq (smtNum 0) (smtVar x) ] + TBool -> [ ] + +smtVar :: String -> SExpr +smtVar = SAtom + +smtEq :: SExpr -> SExpr -> SExpr +smtEq e1 e2 = SList [ SAtom "=", e1, e2 ] + +smtLeq :: SExpr -> SExpr -> SExpr +smtLeq e1 e2 = SList [ SAtom "<=", e1, e2 ] + +smtBool :: Bool -> SExpr +smtBool b = SAtom (if b then "true" else "false") + +smtNum :: Integer -> SExpr +smtNum x = SAtom (show x) + + + + +-------------------------------------------------------------------------------- +-- Recognizing constraints that we can work with. + + +data Ty = TNat | TBool +type VarTypes = UniqFM (TyVar,String,Ty) + + +{- | See if this constraint is one ofthe ones that we understand. +If the constraint is of the form `F ts ~ a`, where `a` is a type-variable, +we also return `a`. This is used to decide in what order to solve +constraints, see `solverSimplify`. -} +knownCt :: Ct -> Maybe (VarTypes, SExpr, Maybe TyVar) +knownCt ct = + case ct of + CFunEqCan _ f args rhs -> + do (vs1,e1) <- knownTerm f args + (vs2,e2) <- knownXi rhs + return (plusUFM vs1 vs2, smtEq e1 e2, getTyVar_maybe rhs) + _ -> Nothing + +knownTerm :: TyCon -> [Xi] -> Maybe (VarTypes, SExpr) +knownTerm tc xis = + do op <- knownTC tc + as <- mapM knownXi xis + -- XXX: Check for linearity here? + let (varMaps,es) = unzip as + return (foldl' plusUFM emptyUFM varMaps, SList (op : es)) +knownTC :: TyCon -> Maybe SExpr +knownTC tc + | tc == typeNatAddTyCon = Just $ SAtom "+" + | tc == typeNatSubTyCon = Just $ SAtom "-" + | tc == typeNatMulTyCon = Just $ SAtom "*" + | tc == typeNatLeqTyCon = Just $ SAtom "<=" + | otherwise = Nothing + +knownXi :: Xi -> Maybe (VarTypes, SExpr) +knownXi xi + | Just x <- getTyVar_maybe xi = knownVar x + | Just x <- isNumLitTy xi = Just (emptyUFM, smtNum x) + | Just x <- isBoolLitTy xi = Just (emptyUFM, smtBool x) + | otherwise = Nothing + +knownVar :: TyVar -> Maybe (VarTypes, SExpr) +knownVar x = + do t <- knownKind (tyVarKind x) + let v = thyVarName x + return (unitUFM x (x, v, t), SAtom v) + +knownKind :: Kind -> Maybe Ty +knownKind k = + case splitTyConApp_maybe k of + Just (tc,[]) + | tc == promotedBoolTyCon -> Just TBool + | tc == typeNatKindCon -> Just TNat + _ -> Nothing + +thyVarName :: TyVar -> String +thyVarName x = occNameString (nameOccName n) ++ "_" ++ show u + where n = tyVarName x + u = nameUnique n + + +-- From a value back into a type +sExprToType :: VarInfo -> SExpr -> Maybe Type +sExprToType vi expr = + case expr of + SAtom "false" -> Just (bool False) + SAtom "true" -> Just (bool True) + SAtom s + | [(n,"")] <- reads s -> Just (num n) + SAtom s + | Just v <- varToTyVar s vi -> Just (mkTyVarTy v) + _ -> Nothing + + + + +-------------------------------------------------------------------------------- + +-- Information about declared variables, so that we know how to extarct +-- models, and map them back into types. +data VarInfo = VarInfo + { smtCurScope :: Map String TyVar + , smtOtherScopes :: [Map String TyVar] + } + +emptyVarInfo :: VarInfo +emptyVarInfo = VarInfo + { smtCurScope = Map.empty + , smtOtherScopes = [] + } + +inScope :: VarInfo -> [String] +inScope vi = Map.keys $ Map.unions $ smtCurScope vi : smtOtherScopes vi + +startScope :: VarInfo -> VarInfo +startScope vi = vi { smtCurScope = Map.empty + , smtOtherScopes = smtCurScope vi : smtOtherScopes vi } + +endScope :: VarInfo -> VarInfo +endScope vi = + case smtOtherScopes vi of + [] -> panic "endScope with no start scope" + s : ss -> vi + { smtCurScope = s + , smtOtherScopes = ss + } + +varToTyVar :: String -> VarInfo -> Maybe TyVar +varToTyVar x vi = msum $ map (Map.lookup x) $ smtCurScope vi : smtOtherScopes vi + + +data VarStatus = Undeclared | Declared + +-- | Update var info, and indicate if we need to declare the variable. +declareVar :: TyVar -> VarInfo -> (VarInfo, VarStatus) +declareVar tv vi + | x `Map.member` smtCurScope vi = (vi, Declared) + | any (x `Map.member`) (smtOtherScopes vi) = (vi, Declared) + | otherwise = + ( vi { smtCurScope = Map.insert x tv (smtCurScope vi) }, Undeclared ) + where x = thyVarName tv + + + + + + +-------------------------------------------------------------------------------- +-- Low-level interaction with the solver process. + +data SExpr = SAtom String | SList [SExpr] + deriving Eq + +instance Show SExpr where + showsPrec _ = renderSExpr + +data SolverProcess = SolverProcess + { solverDo :: SExpr -> IO SExpr + , solverStop :: IO () + + -- For debguggning + , solverDebug :: String -> IO () + , solverDebugNext :: IO () + , solverDebugPrev :: IO () + } + +startSolverProcess :: String -> [String] -> IO SolverProcess +startSolverProcess exe opts = + do (hIn, hOut, hErr, h) <- runInteractiveProcess exe opts Nothing Nothing + + dbgNest <- newIORef (0 :: Int) + let dbgMsg x = do n <- readIORef dbgNest + hPutStrLn stderr (replicate n ' ' ++ x) + dbgNext = modifyIORef' dbgNest (+2) + dbgPrev = modifyIORef' dbgNest (subtract 2) + + -- XXX: Ignore errors for now. + _ <- forkIO $ do forever (putStrLn =<< hGetLine hErr) + `X.catch` \X.SomeException {} -> return () + + -- XXX: No real error-handling here. + getResponse <- + do txt <- hGetContents hOut + ref <- newIORef (unfoldr parseSExpr txt) + return $ + atomicModifyIORef ref $ \xs -> + case xs of + [] -> (xs, Nothing) + y : ys -> (ys, Just y) + + let cmd' c = do let e = renderSExpr c "" + -- dbgMsg ("[->] " ++ e) + hPutStrLn hIn e + hFlush hIn + + return SolverProcess + { solverDo = \c -> do cmd' c + mb <- getResponse + case mb of + Just res -> + do -- dbgMsg ("[<-] " ++ renderSExpr res "") + return res + Nothing -> fail "Missing response from solver" + , solverStop = + do cmd' (SList [SAtom "exit"]) + _exitCode <- waitForProcess h + return () + + , solverDebug = dbgMsg + , solverDebugNext = dbgNext + , solverDebugPrev = dbgPrev + } + +renderSExpr :: SExpr -> ShowS +renderSExpr ex = + case ex of + SAtom x -> showString x + SList es -> showChar '(' . + foldr (\e m -> renderSExpr e . showChar ' ' . m) + (showChar ')') es + +parseSExpr :: String -> Maybe (SExpr, String) +parseSExpr (c : more) | isSpace c = parseSExpr more +parseSExpr ('(' : more) = do (xs,more1) <- list more + return (SList xs, more1) + where + list (c : txt) | isSpace c = list txt + list (')' : txt) = return ([], txt) + list txt = do (v,txt1) <- parseSExpr txt + (vs,txt2) <- list txt1 + return (v:vs, txt2) +parseSExpr txt = case break end txt of + (as,bs) | not (null as) -> Just (SAtom as, bs) + _ -> Nothing + where end x = x == ')' || isSpace x |