Reuse some code in the defaulting mechanism.

src/Cryptol/TypeCheck/Defaulting.hs

@@ -39,8 +39,7 @@ defaultExpr' :: FilePath -> [String] -> Range -> Expr -> Schema
 defaultExpr' prog args r e s =
   if all (\v -> kindOf v == KNum) (sVars s)
      then do let params = map tpVar (sVars s)
-                 goals  = [ Goal CtDefaulting r p | p <- sProps s ]
-             mbSubst <- tryGetModel prog args params goals
+             mbSubst <- tryGetModel prog args params (sProps s)
              case mbSubst of
                Just su -> return $ do tys <- mapM (bindParam su) params
                                       return (zip (sVars s) tys, appExpr tys)

src/Cryptol/TypeCheck/Solve.hs

@@ -511,37 +511,12 @@ tryGetModel ::
   String ->
   [String] ->
   [TVar] ->   -- variables to try defaulting
-  [Goal] ->   -- constraints
+  [Prop] ->   -- constraints
     IO (Maybe Subst)
-tryGetModel prog args xs gs =
-  Num.withSolver prog args False $ \ s -> tryGetModelWith s xs gs
+tryGetModel prog args xs ps =
+  Num.withSolver prog args False $ \ s ->
+    -- We are only interested in finite instantiations
+    Num.getModel s (map (pFin . TVar) xs ++ ps)
 
-tryGetModelWith ::
-  Num.Solver ->
-  [TVar] ->
-  [Goal] ->   -- constraints
-    IO (Maybe Subst)
-tryGetModelWith s xs goals =
-  do mbModel <- Num.getModel s goals
-     case mbModel of
-       Just model -> checkModel $ defaultingSubst
-                                $ listSubst [ (tv,tNum i) | (tv,i) <- Map.elems model
-                                                          , tv `elem` xs ]
-       Nothing    -> return Nothing
 
-  where
 
-  -- make sure that the constraints can be simplified when using this
-  -- model.
-  checkModel su =
-    do let gs = apSubst su goals
-       res <- simpGoals s gs
-       case res of
-
-         -- conservatively, require that all goals are discharged by the model
-         Right (goals',su')
-           | null goals' -> return (Just (su' @@ su))
-           | otherwise   -> return Nothing
-
-         -- simplification failed under this substitution, the model is invalid.
-         Left _ -> return Nothing

src/Cryptol/TypeCheck/Solver/CrySAT.hs

@@ -39,6 +39,7 @@ import           Data.Maybe ( mapMaybe, fromMaybe )
 import           Data.Map (Map)
 import qualified Data.Map as Map
 import           Data.Foldable ( any, all )
+import           Data.Traversable ( for )
 import           Data.Set ( Set )
 import qualified Data.Set as Set
 import           Data.IORef ( IORef, newIORef, readIORef, modifyIORef',
@@ -245,9 +246,17 @@ simplifyProps s props =
 --  * We assume that the constraints are well-defined.
 --  * Modifies the set of assumptions.
 assumeProps :: Solver -> [Cry.Prop] -> IO VarMap
-assumeProps s props =
-  do mapM_ (assert s . simpProp) (map cryDefinedProp ps ++ ps)
-     return (Map.unions varMaps)
+assumeProps s props = fmap fst (assumeProps' s props)
+
+
+-- | Add the given constraints as assumptions.
+--  * We assume that the constraints are well-defined.
+--  * Modifies the set of assumptions.
+assumeProps' :: Solver -> [Cry.Prop] -> IO (VarMap, [SimpProp])
+assumeProps' s props =
+  do let simpProps = map simpProp (map cryDefinedProp ps ++ ps)
+     mapM_ (assert s) simpProps
+     return (Map.unions varMaps, simpProps)
   where (ps,varMaps) = unzip (mapMaybe exportProp props)
   -- XXX: Instead of asserting one at a time, perhaps we should
   -- assert a conjunction.  That way, we could simplify the whole thing
@@ -303,45 +312,38 @@ improveByDefn uvs p =
     | otherwise                   = Just (x,e)
 
 
-type Model = Map Name (Cry.TVar,Integer)
+{- | Attempt to find a substituion that, when applied, makes all of the
+given properties hold. -}
+getModel :: Solver -> [Cry.Prop] -> IO (Maybe Cry.Subst)
+getModel s props = withScope s $
+  do (varMap,ps) <- assumeProps' s props
+     res         <- SMT.check (solver s)
 
--- | Attempt to find a finite model for the variables involved in a set of
--- goals.
-getModel :: Solver -> [Goal] -> IO (Maybe Model)
-getModel s goals = withScope s $
-
-  do varMap <- assumeProps s (map goal goals)
-     assumeAllFin varMap
-     res <- SMT.check (solver s)
      case res of
-       SMT.Sat -> extractModel varMap
-       _       -> return Nothing
+       SMT.Sat ->
+          do vs <- getVals (solver s) (Map.keys varMap)
+             -- This is guaranteed to be a model only for the *linear*
+             -- properties, so now we check if it works for the rest too.
+
+             let su1  = fmap K vs
+                 ps1  = [ fromMaybe p (apSubst su1 p) | SimpProp p <- ps ]
+                 ok p = case crySimplify p of
+                          PTrue -> True
+                          _     -> False
+
+                 su2 = Cry.listSubst
+                     $ Map.elems
+                     $ Map.intersectionWith (,) varMap (fmap numTy vs)
+
+             return (guard (all ok ps1) >> return su2)
+
+
+       _ -> return Nothing
+
 
   where
-
-  assumeAllFin varMap =
-    mapM_ assertFin (Map.keys varMap)
-
-  assertFin n =
-       SMT.assert (solver s) (SMT.const (smtFinName n))
-
-  extractModel varMap =
-    do binds <- forM (Map.toList varMap) $ \ (n,tv) ->
-                  do mb <- getInst n
-                     case mb of
-                       Just i  -> return (Just (n,(tv,i)))
-                       Nothing -> return Nothing
-
-       return (Map.fromList `fmap` sequence binds)
-
-  -- check to see if the variable became inf, otherwise extract its value.
-  getInst n =
-    do val <- SMT.getConst (solver s) (smtName n)
-       case val of
-         SMT.Int i -> return (Just i)
-         _         -> return Nothing
-
-
+  numTy Inf     = Cry.tInf
+  numTy (Nat k) = Cry.tNum k
 
 --------------------------------------------------------------------------------