module Cryptol.TypeCheck.Solve
( simplifyAllConstraints
, proveImplication
, wfType
, wfTypeFunction
, improveByDefaultingWith
, defaultReplExpr
, simpType
, simpTypeMaybe
) where
import Cryptol.Parser.Position (emptyRange)
import Cryptol.TypeCheck.PP(pp)
import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.Monad
import Cryptol.TypeCheck.Subst
(apSubst,fvs,singleSubst,substToList, isEmptySubst,
emptySubst,Subst,listSubst, (@@), Subst,
apSubstMaybe)
import Cryptol.TypeCheck.Solver.Class
import Cryptol.TypeCheck.Solver.Selector(tryHasGoal)
import qualified Cryptol.TypeCheck.Solver.Numeric.AST as Num
import qualified Cryptol.TypeCheck.Solver.Numeric.ImportExport as Num
import Cryptol.TypeCheck.Solver.Numeric.Interval (Interval)
import qualified Cryptol.TypeCheck.Solver.Numeric.Simplify1 as Num
import qualified Cryptol.TypeCheck.Solver.Numeric.SimplifyExpr as Num
import qualified Cryptol.TypeCheck.Solver.CrySAT as Num
import Cryptol.TypeCheck.Solver.CrySAT (debugBlock, DebugLog(..))
import Cryptol.TypeCheck.Solver.Simplify (tryRewritePropAsSubst)
import Cryptol.Utils.PP (text)
import Cryptol.Utils.Panic(panic)
import Cryptol.Utils.Misc(anyJust)
import Control.Monad (unless, guard)
import Data.Either(partitionEithers)
import Data.Maybe(catMaybes, fromMaybe, mapMaybe)
import Data.Map ( Map )
import qualified Data.Map as Map
import Data.Set ( Set )
import qualified Data.Set as Set
wfTypeFunction :: TFun -> [Type] -> [Prop]
wfTypeFunction TCSub [a,b] = [ a >== b, pFin b]
wfTypeFunction TCDiv [a,b] = [ b >== tOne, pFin a ]
wfTypeFunction TCMod [a,b] = [ b >== tOne, pFin a ]
wfTypeFunction TCLenFromThen [a,b,w] =
[ pFin a, pFin b, pFin w, a =/= b, w >== tWidth a ]
wfTypeFunction TCLenFromThenTo [a,b,c] = [ pFin a, pFin b, pFin c, a =/= b ]
wfTypeFunction _ _ = []
wfType :: Type -> [Prop]
wfType t =
case t of
TCon c ts ->
let ps = concatMap wfType ts
in case c of
TF f -> wfTypeFunction f ts ++ ps
_ -> ps
TVar _ -> []
TUser _ _ s -> wfType s
TRec fs -> concatMap (wfType . snd) fs
simplifyAllConstraints :: InferM ()
simplifyAllConstraints =
do mapM_ tryHasGoal =<< getHasGoals
gs <- getGoals
solver <- getSolver
(mb,su) <- io (simpGoals' solver gs)
extendSubst su
case mb of
Right gs1 -> addGoals gs1
Left badGs -> mapM_ (recordError . UnsolvedGoal True) badGs
proveImplication :: Name -> [TParam] -> [Prop] -> [Goal] -> InferM Subst
proveImplication lnam as ps gs =
do evars <- varsWithAsmps
solver <- getSolver
(mbErr,su) <- io (proveImplicationIO solver lnam evars as ps gs)
case mbErr of
Right ws -> mapM_ recordWarning ws
Left err -> recordError err
return su
proveImplicationIO :: Num.Solver
-> Name
-> Set TVar
-> [TParam]
-> [Prop]
-> [Goal]
-> IO (Either Error [Warning], Subst)
proveImplicationIO _ _ _ _ [] [] = return (Right [], emptySubst)
proveImplicationIO s lname varsInEnv as ps gs =
debugBlock s "proveImplicationIO" $
do debugBlock s "assumes" (debugLog s ps)
debugBlock s "shows" (debugLog s gs)
debugLog s "1. ------------------"
_simpPs <- Num.assumeProps s ps
mbImps <- Num.check s
debugLog s "2. ------------------"
case mbImps of
Nothing ->
do debugLog s "(contradiction in assumptions)"
return (Left $ UnusableFunction lname ps, emptySubst)
Just (imps,extra) ->
do let su = importImps imps
gs0 = apSubst su gs
debugBlock s "improvement from assumptions:" $ debugLog s su
let (scs,invalid) = importSideConds extra
unless (null invalid) $
panic "proveImplicationIO" ( "Unable to import all side conditions:"
: map (show . Num.ppProp) invalid )
let gs1 = filter ((`notElem` ps) . goal) gs0
debugLog s "3. ---------------------"
(mb,su1) <- simpGoals' s (scs ++ gs1)
case mb of
Left badGs -> reportUnsolved badGs (su1 @@ su)
Right [] -> return (Right [], su1 @@ su)
Right us ->
do let vs = Set.filter isFreeTV $ fvs $ map goal us
dVars = Set.toList (vs `Set.difference` varsInEnv)
(_,us1,su2,ws) <- improveByDefaultingWith s dVars us
case us1 of
[] -> return (Right ws, su2 @@ su1 @@ su)
_ -> reportUnsolved us1 (su2 @@ su1 @@ su)
where
reportUnsolved us su =
return ( Left $ UnsolvedDelcayedCt
$ DelayedCt { dctSource = lname
, dctForall = as
, dctAsmps = ps
, dctGoals = us
}, su)
simpGoals' :: Num.Solver -> [Goal] -> IO (Either [Goal] [Goal], Subst)
simpGoals' s gs0 = go emptySubst [] (wellFormed gs0 ++ gs0)
where
wellFormed gs = [ g { goal = p } | g <- gs, p <- wfType (goal g) ]
go su old [] = return (Right old, su)
go su old gs =
do gs1 <- simplifyConstraintTerms s gs
res <- solveConstraints s old gs1
case res of
Left err -> return (Left err, su)
Right gs2 ->
do let gs3 = gs2 ++ old
mb <- computeImprovements s gs3
case mb of
Left err -> return (Left err, su)
Right impSu ->
let (unchanged,changed) =
partitionEithers (map (applyImp impSu) gs3)
new = wellFormed changed
in go (impSu @@ su) unchanged (new ++ changed)
applyImp su g = case apSubstMaybe su (goal g) of
Nothing -> Left g
Just p -> Right g { goal = p }
simplifyConstraintTerms :: Num.Solver -> [Goal] -> IO [Goal]
simplifyConstraintTerms s gs =
debugBlock s "Simplifying terms" $ return (map simpGoal gs)
where simpGoal g = g { goal = simpProp (goal g) }
solveConstraints :: Num.Solver ->
[Goal] ->
[Goal] ->
IO (Either [Goal] [Goal])
solveConstraints s otherGs gs0 =
debugBlock s "Solving constraints" $ solveClassCts [] [] gs0
where
otherNumerics = [ g | Right g <- map Num.numericRight otherGs ]
solveClassCts unsolvedClass numerics [] =
do unsolvedNum <- solveNumerics s otherNumerics numerics
return (Right (unsolvedClass ++ unsolvedNum))
solveClassCts unsolved numerics (g : gs) =
case Num.numericRight g of
Right n -> solveClassCts unsolved (n : numerics) gs
Left c ->
case classStep c of
Unsolvable -> return (Left [g])
Unsolved -> solveClassCts (g : unsolved) numerics gs
Solved Nothing subs -> solveClassCts unsolved numerics (subs ++ gs)
Solved (Just su) _ -> panic "solveClassCts"
[ "Unexpected substituion", show su ]
solveNumerics :: Num.Solver ->
[(Goal,Num.Prop)] ->
[(Goal,Num.Prop)] ->
IO [Goal]
solveNumerics s consultGs solveGs =
Num.withScope s $
do _ <- Num.assumeProps s (map (goal . fst) consultGs)
Num.simplifyProps s (map Num.knownDefined solveGs)
computeImprovements :: Num.Solver -> [Goal] -> IO (Either [Goal] Subst)
computeImprovements s gs =
debugBlock s "Computing improvements" $
do let nums = [ g | Right g <- map Num.numericRight gs ]
res <- Num.withScope s $
do _ <- Num.assumeProps s (map (goal . fst) nums)
mb <- Num.check s
case mb of
Nothing -> return Nothing
Just (suish,_ps1) ->
do let (su,_ps2) = importSplitImps suish
Right ints <- Num.getIntervals s
return (Just (ints,su))
case res of
Just (ints,su)
| isEmptySubst su
, (x,t) : _ <- mapMaybe (improveByDefn ints) gs ->
do let su' = singleSubst x t
debugLog s ("Improve by definition: " ++ show (pp su'))
return (Right su')
| otherwise -> return (Right su)
Nothing ->
do bad <- Num.minimizeContradictionSimpDef s
(map Num.knownDefined nums)
return (Left bad)
improveByDefn :: Map TVar Interval -> Goal -> Maybe (TVar,Type)
improveByDefn ints Goal { .. } =
do (var,ty) <- tryRewritePropAsSubst ints goal
return (var,simpType ty)
importSplitImps :: Map Num.Name Num.Expr -> (Subst, [Prop])
importSplitImps = mk . partitionEithers . map imp . Map.toList
where
mk (uni,props) = (listSubst (catMaybes uni), props)
imp (x,e) = case (x, Num.importType e) of
(Num.UserName tv, Just ty) ->
case tv of
TVFree {} -> Left (Just (tv,ty))
TVBound {} -> Right (TVar tv =#= ty)
_ -> Left Nothing
importImps :: Map Num.Name Num.Expr -> Subst
importImps = listSubst . map imp . Map.toList
where
imp (x,e) = case (x, Num.importType e) of
(Num.UserName tv, Just ty) -> (tv,ty)
_ -> panic "importImps" [ "Failed to import:", show x, show e ]
importSideConds :: [Num.Prop] -> ([Goal],[Num.Prop])
importSideConds = go [] []
where
go ok bad [] = ([ Goal CtImprovement emptyRange g | g <- ok], bad)
go ok bad (p:ps) = case Num.importProp p of
Just p' -> go (p' ++ ok) bad ps
Nothing -> go ok (p:bad) ps
improveByDefaultingWith ::
Num.Solver ->
[TVar] ->
[Goal] ->
IO ( [TVar]
, [Goal]
, Subst
, [Warning]
)
improveByDefaultingWith s as ps =
classify (Map.fromList [ (a,([],Set.empty)) | a <- as ]) [] [] ps
where
classify leqs fins others [] =
do let
(defs, newOthers) = select [] [] (fvs others) (Map.toList leqs)
su = listSubst defs
(mb,su1) <- simpGoals' s (newOthers ++ others ++ apSubst su fins)
case mb of
Right gs1 ->
let warn (x,t) =
case x of
TVFree _ _ _ d -> DefaultingTo d t
TVBound {} -> panic "Crypto.TypeCheck.Infer"
[ "tryDefault attempted to default a quantified variable."
]
newSu = su1 @@ su
names = Set.fromList $ map fst $ fromMaybe [] $ substToList newSu
in return ( [ a | a <- as, not (a `Set.member` names) ]
, gs1
, newSu
, map warn defs
)
Left _ -> return (as,ps,su1 @@ su,[])
classify leqs fins others (prop : more) =
case tNoUser (goal prop) of
TCon (PC PFin) [ _ ] -> classify leqs (prop : fins) others more
TCon (PC PGeq) [ TVar x, t ]
| x `elem` as && x `Set.notMember` freeRHS ->
classify leqs' fins others more
where freeRHS = fvs t
add (xs1,vs1) (xs2,vs2) = (xs1 ++ xs2, Set.union vs1 vs2)
leqs' = Map.insertWith add x ([(t,prop)],freeRHS) leqs
_ -> classify leqs fins (prop : others) more
select yes no _ [] = ([ (x, t) | (x,t) <- yes ] ,no)
select yes no otherFree ((x,(rhsG,vs)) : more) =
select newYes newNo newFree newMore
where
(ts,gs) = unzip rhsG
(newYes,newNo,newFree,newMore)
| x `Set.member` otherFree = noDefaulting
| otherwise =
let deps = [ y | (y,(_,yvs)) <- more, x `Set.member` yvs ]
recs = filter (`Set.member` vs) deps
in if not (null recs) || isBoundTV x
then noDefaulting
else yesDefaulting
where
noDefaulting = ( yes, gs ++ no, vs `Set.union` otherFree, more )
yesDefaulting =
let ty = case ts of
[] -> tNum (0::Int)
_ -> foldr1 tMax ts
su1 = singleSubst x ty
in ( (x,ty) : [ (y,apSubst su1 t) | (y,t) <- yes ]
, no
, otherFree
, [ (y, (apSubst su1 ts1, vs1)) | (y,(ts1,vs1)) <- more ]
)
defaultReplExpr :: Num.Solver -> Expr -> Schema
-> IO (Maybe ([(TParam,Type)], Expr))
defaultReplExpr so e s =
if all (\v -> kindOf v == KNum) (sVars s)
then do let params = map tpVar (sVars s)
mbSubst <- tryGetModel so params (sProps s)
case mbSubst of
Just su ->
do (res,su1) <- simpGoals' so (map (makeGoal su) (sProps s))
return $
case res of
Right [] | isEmptySubst su1 ->
do tys <- mapM (bindParam su) params
return (zip (sVars s) tys, appExpr tys)
_ -> Nothing
_ -> return Nothing
else return Nothing
where
makeGoal su p = Goal { goalSource = error "goal source"
, goalRange = error "goal range"
, goal = apSubst su p
}
bindParam su tp =
do let ty = TVar tp
ty' = apSubst su ty
guard (ty /= ty')
return ty'
appExpr tys = foldl (\e1 _ -> EProofApp e1) (foldl ETApp e tys) (sProps s)
tryGetModel ::
Num.Solver ->
[TVar] ->
[Prop] ->
IO (Maybe Subst)
tryGetModel s xs ps =
Num.getModel s (map (pFin . TVar) xs ++ ps)
simpType :: Type -> Type
simpType ty = fromMaybe ty (simpTypeMaybe ty)
simpProp :: Prop -> Prop
simpProp p = case p of
TUser f ts q -> TUser f (map simpType ts) (simpProp q)
TCon c ts -> TCon c (map simpType ts)
TVar {} -> panic "simpProp" ["variable", show p]
TRec {} -> panic "simpProp" ["record", show p]
simpTypeMaybe :: Type -> Maybe Type
simpTypeMaybe ty =
case ty of
TCon c ts ->
case c of
TF {} -> do e <- Num.exportType ty
e1 <- Num.crySimpExprMaybe e
Num.importType e1
_ -> TCon c `fmap` anyJust simpTypeMaybe ts
TVar _ -> Nothing
TUser x ts t -> TUser x ts `fmap` simpTypeMaybe t
TRec fs ->
do let (ls,ts) = unzip fs
ts' <- anyJust simpTypeMaybe ts
return (TRec (zip ls ts'))
_testSimpGoals :: IO ()
_testSimpGoals = Num.withSolver cfg $ \s ->
do mapM_ dump asmps
mapM_ (dump .goal) gs
_ <- Num.assumeProps s asmps
_mbImps <- Num.check s
(mb,_) <- simpGoals' s gs
case mb of
Right _ -> debugLog s "End of test"
Left _ -> debugLog s "Impossible"
where
cfg = SolverConfig { solverPath = "z3"
, solverArgs = [ "-smt2", "-in" ]
, solverVerbose = 1
}
asmps = []
gs = map fakeGoal [ tv 0 =#= tMin (num 10) (tv 1)
, tv 1 =#= num 10
]
fakeGoal p = Goal { goalSource = undefined, goalRange = undefined, goal = p }
tv n = TVar (TVFree n KNum Set.empty (text "test var"))
_btv n = TVar (TVBound n KNum)
num x = tNum (x :: Int)
dump a = do putStrLn "-------------------_"
case Num.exportProp a of
Just b -> do print $ Num.ppProp' $ Num.propToProp' b
putStrLn "-------------------"
Nothing -> print "can't export"