From 073944893309b6789ce627fad17a8eef6912068f Mon Sep 17 00:00:00 2001
From: Iavor Diatchki <iavor.diatchki@gmail.com>
Date: Wed, 11 Jul 2018 15:11:29 -0700
Subject: [PATCH] Do and-goal splitting in more places.

This alleviates some of the problems in #522
---
 src/Cryptol/TypeCheck/Infer.hs |  8 ++++----
 src/Cryptol/TypeCheck/Monad.hs | 14 +++++++++++++-
 src/Cryptol/TypeCheck/Subst.hs | 11 +++++++++--
 3 files changed, 26 insertions(+), 7 deletions(-)

diff --git a/src/Cryptol/TypeCheck/Infer.hs b/src/Cryptol/TypeCheck/Infer.hs
index e9df8ad4..08d64f99 100644
--- a/src/Cryptol/TypeCheck/Infer.hs
+++ b/src/Cryptol/TypeCheck/Infer.hs
@@ -695,7 +695,7 @@ generalize bs0 gs0 =
   do {- First, we apply the accumulating substitution to the goals
         and the inferred types, to ensure that we have the most up
         to date information. -}
-     gs <- forM gs0 $ \g -> applySubst g
+     gs <- applySubstGoals gs0
      bs <- forM bs0 $ \b -> do s <- applySubst (dSignature b)
                                return b { dSignature = s }
 
@@ -801,7 +801,7 @@ checkSigB b (Forall as asmps0 t0, validSchema) = case thing (P.bDef b) of
                    addGoals validSchema
                    () <- simplifyAllConstraints  -- XXX: using `asmps` also?
                    return e1
-     cs <- applySubst cs0
+     cs <- applySubstGoals cs0
 
      let findKeep vs keep todo =
           let stays (_,cvs)    = not $ Set.null $ Set.intersection vs cvs
@@ -816,12 +816,12 @@ checkSigB b (Forall as asmps0 t0, validSchema) = case thing (P.bDef b) of
 
      addGoals leave
 
-     asmps1 <- applySubst asmps0
+     asmps1 <- applySubstPreds asmps0
 
      su <- proveImplication (Just (thing (P.bName b))) as asmps1 stay
      extendSubst su
 
-     let asmps  = apSubst su asmps1
+     let asmps  = concatMap pSplitAnd (apSubst su asmps1)
      t      <- applySubst t0
      e2     <- applySubst e1
 
diff --git a/src/Cryptol/TypeCheck/Monad.hs b/src/Cryptol/TypeCheck/Monad.hs
index 3c0e77f7..ae151aa5 100644
--- a/src/Cryptol/TypeCheck/Monad.hs
+++ b/src/Cryptol/TypeCheck/Monad.hs
@@ -343,7 +343,8 @@ newGoals src ps = addGoals =<< mapM (newGoal src) ps
 The substitution IS applied to them. -}
 getGoals :: InferM [Goal]
 getGoals =
-  do goals <- applySubst =<< IM (sets $ \s -> (iCts s, s { iCts = emptyGoals }))
+  do goals <- applySubst =<<
+                  IM (sets $ \s -> (iCts s, s { iCts = emptyGoals }))
      return (fromGoals goals)
 
 -- | Add a bunch of goals that need solving.
@@ -504,6 +505,17 @@ applySubst t =
   do su <- getSubst
      return (apSubst su t)
 
+applySubstPreds :: [Prop] -> InferM [Prop]
+applySubstPreds ps =
+  do ps1 <- applySubst ps
+     return (concatMap pSplitAnd ps1)
+
+
+applySubstGoals :: [Goal] -> InferM [Goal]
+applySubstGoals gs =
+  do gs1 <- applySubst gs
+     return [ g { goal = p } | g <- gs1, p <- pSplitAnd (goal g) ]
+
 -- | Get the substitution that we have accumulated so far.
 getSubst :: InferM Subst
 getSubst = IM $ fmap iSubst get
diff --git a/src/Cryptol/TypeCheck/Subst.hs b/src/Cryptol/TypeCheck/Subst.hs
index efab986f..2c654911 100644
--- a/src/Cryptol/TypeCheck/Subst.hs
+++ b/src/Cryptol/TypeCheck/Subst.hs
@@ -232,7 +232,8 @@ capture, because we rely on the 'Subst' datatype invariant to ensure
 that variable scopes will be properly preserved. -}
 
 instance TVars Schema where
-  apSubst su (Forall xs ps t) = Forall xs (apSubst su ps) (apSubst su t)
+  apSubst su (Forall xs ps t) = Forall xs (concatMap pSplitAnd (apSubst su ps))
+                                          (apSubst su t)
 
 instance TVars Expr where
   apSubst su = go
@@ -243,7 +244,13 @@ instance TVars Expr where
         EAbs x t e1   -> EAbs x (apSubst su t) (go e1)
         ETAbs a e     -> ETAbs a (go e)
         ETApp e t     -> ETApp (go e) (apSubst su t)
-        EProofAbs p e -> EProofAbs (apSubst su p) (go e)
+        EProofAbs p e -> EProofAbs hmm (go e)
+          where hmm = case pSplitAnd (apSubst su p) of
+                        [p1] -> p1
+                        _  -> panic "apSubst@EProofAbs"
+                                [ "Predicate split or disappeared after"
+                                , "we applied a substitution." ]
+
         EProofApp e   -> EProofApp (go e)
 
         EVar {}       -> expr