GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-18 05:21:57 +03:00
Code Issues Projects Releases Wiki Activity

Convert simplified terms back into goal terms.

Browse Source
This commit is contained in:
Iavor S. Diatchki 2014-12-17 15:40:26 -08:00
parent 76dc6994c1
commit 9b420b3810
2 changed files with 25 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
src/Cryptol/TypeCheck/Solve.hs
View File

@ -81,7 +81,7 @@ debugBlock s name m =
return a
debugLog :: Num.Solver -> String -> IO ()
debugLog _ _ = return ()
debugLog s x = SMT.logMessage (Num.logger s) x
proveImplication' :: LQName -> [TParam] -> [Prop] -> [Goal] ->
IO (Either Error Subst)
@ -144,13 +144,20 @@ simpGoals :: Num.Solver -> [Goal] -> IO (Maybe ([Goal],Subst))
simpGoals s gs0 =
do let (unsolvedClassCts,numCts) = solveClassCts gs0
varMap = Map.unions [ vm | ((_,vm),_) <- numCts ]
updCt prop (g,vs) = case Num.importProp varMap prop of
Just [g1] -> (g { goal = g1 }, vs)
-- XXX: Could we get multiple gs?
_ -> (g, vs)
case numCts of
[] -> return $ Just (unsolvedClassCts, emptySubst)
_ -> do mbOk <- Num.checkDefined s uvs numCts
_ -> do mbOk <- Num.checkDefined s updCt uvs numCts
case mbOk of
Nothing -> return Nothing
Just (nonDef,def,imps) ->
do debugBlock s "simpGoals results (defined)" $
do debugBlock s ("simpGoals results") $
do debugBlock s "possibly not defined" $
mapM_ (debugLog s . show . pp . goal . fst) nonDef
debugBlock s "defined" $
mapM_ (debugLog s . ($ "") . SMT.showsSExpr . Num.smtpLinPart) def
let (su,extraProps) = importSplitImps varMap imps

22
src/Cryptol/TypeCheck/Solver/CrySAT.hs
View File

@ -45,16 +45,17 @@ The result is like this:
and simplified the arguments to the input Prop.
* ImpMap: We computed some improvements. -}
checkDefined :: Solver ->
(Prop -> a -> a) {- ^ Update a goal -} ->
Set Name {- ^ Unification variables -} ->
[(a,Prop)] {- ^ Goals -} ->
IO (Maybe ( [a] -- could not prove
, [SMTProp (a,Prop)] -- proved ok and simplified terms
, ImpMap -- computed improvements
))
checkDefined s uniVars props0 = withScope s (go Map.empty [] props0)
checkDefined s updCt uniVars props0 = withScope s (go Map.empty [] props0)
where
go knownImps done notDone =
do (newNotDone, novelDone) <- checkDefined' s notDone
do (newNotDone, novelDone) <- checkDefined' s updCt notDone
(possible, imps) <- check s uniVars
if not possible
then return Nothing
@ -82,12 +83,12 @@ checkDefined s uniVars props0 = withScope s (go Map.empty [] props0)
Nothing -> ct
Just p' ->
let p2 = crySimpPropExpr p'
in (prepareProp p2) { smtpOther = (g,p2) }
in (prepareProp p2) { smtpOther = (updCt p2 g,p2) }
updNotDone su (g,p) =
case apSubst su p of
Nothing -> (g,p)
Just p' -> (g,p')
Just p' -> (updCt p' g,p')
-- | Check that a bunch of constraints are all defined.
@ -95,8 +96,9 @@ checkDefined s uniVars props0 = withScope s (go Map.empty [] props0)
-- component, and the ones that are defined in the second component.
-- * Well defined constraints are asserted at this point.
-- * The expressions in the defined constraints are simplified.
checkDefined' :: Solver -> [(a,Prop)] -> IO ([(a,Prop)], [SMTProp (a,Prop)])
checkDefined' s props0 =
checkDefined' :: Solver -> (Prop -> a -> a) ->
[(a,Prop)] -> IO ([(a,Prop)], [SMTProp (a,Prop)])
checkDefined' s updCt props0 =
go False [] [] [ (a, p, prepareProp (cryDefinedProp p)) | (a,p) <- props0 ]
where
@ -112,8 +114,12 @@ checkDefined' s props0 =
-- Process one constraint.
go ch isDef isNotDef ((ct,p,q) : more) =
do proved <- prove s q
if proved then do let p' = crySimpPropExpr p
r = (prepareProp p') { smtpOther = (ct,p') }
if proved then do let r = case crySimpPropExprMaybe p of
Nothing -> (prepareProp p)
{ smtpOther = (ct,p) }
Just p' -> (prepareProp p')
{ smtpOther = (updCt p' ct, p') }
assert s r -- add defined prop as an assumption
go True (r : isDef) isNotDef more
else go ch isDef ((ct,p,q) : isNotDef) more