From 9b420b3810d4ed2149c431467e14f01e0e036f14 Mon Sep 17 00:00:00 2001
From: "Iavor S. Diatchki" <diatchki@galois.com>
Date: Wed, 17 Dec 2014 15:40:26 -0800
Subject: [PATCH] Convert simplified terms back into goal terms.

---
 src/Cryptol/TypeCheck/Solve.hs         | 15 +++++++++++----
 src/Cryptol/TypeCheck/Solver/CrySAT.hs | 22 ++++++++++++++--------
 2 files changed, 25 insertions(+), 12 deletions(-)

diff --git a/src/Cryptol/TypeCheck/Solve.hs b/src/Cryptol/TypeCheck/Solve.hs
index 696a5755..a2d98439 100644
--- a/src/Cryptol/TypeCheck/Solve.hs
+++ b/src/Cryptol/TypeCheck/Solve.hs
@@ -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,14 +144,21 @@ 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)" $
-                          mapM_ (debugLog s . ($ "") . SMT.showsSExpr  . Num.smtpLinPart) def
+                    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
 
diff --git a/src/Cryptol/TypeCheck/Solver/CrySAT.hs b/src/Cryptol/TypeCheck/Solver/CrySAT.hs
index 0aead4f1..6bc4e9a7 100644
--- a/src/Cryptol/TypeCheck/Solver/CrySAT.hs
+++ b/src/Cryptol/TypeCheck/Solver/CrySAT.hs
@@ -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