Generalize to support arbitrary theories.decision-procedure

The theory of natural numbers is defined in TcTypeNats.

2 files changed, 289 insertions, 681 deletions

diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index 118b99df78..960a737fb8 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -38,7 +38,7 @@ import TcEvidence
 import Outputable
 
 import TcMType ( zonkTcPredType )
-import TcTypeNats(isLinArithTyCon,decideLinArith,LinArithResult(..))
+import TcTypeNats(Theory(..), Result(..), thyVarName, linArith)
 
 import TcRnTypes
 import TcErrors
@@ -47,15 +47,17 @@ import Maybes( orElse )
 import Bag
 import MonadUtils(liftIO)
 
-import Control.Monad ( foldM )
-import Data.Maybe ( catMaybes, mapMaybe )
+import Data.Maybe ( catMaybes, mapMaybe, maybeToList )
+import qualified Data.Map as Map
+import Data.List ( tails )
 
 import VarEnv
 
-import Control.Monad( when, unless )
+import Control.Monad( when, unless, foldM, forM )
 import Pair (Pair(..))
 import Unique( hasKey )
 import UniqFM
+import UniqSet(foldUniqSet)
 import FastString ( sLit ) 
 import DynFlags
 import Util
@@ -1473,43 +1475,9 @@ doTopReactFunEq wi fl fun_tc args xi loc
     fam_ty = mkTyConApp fun_tc args
 
     try_improve_and_return
-       | isLinArithTyCon fun_tc args =
-          do { (gis,wis) <- getRelevantLinArithInerts
-             ; res <- liftIO $ decideLinArith gis wis wi
-             ; let addInerts = mapM_ insertInertItemTcS
-                   setEvidence (ct, ev) =
-                     setEvBind (ctEvId $ ctEvidence ct) ev
-             ; case res of
-                 SolvedWanted ev -> do
-                   addInerts wis
-                   setEvidence (wi, ev)
-                   traceTcS "[NATS]" (text "SOLVED WANTED")
-                 IgnoreGiven -> do
-                   addInerts wis
-                   traceTcS "[NATS]" (text "IGNORING")
-                 Impossible -> do emitInsoluble wi
-                                  traceTcS "[NATS]" (text "IMPOSSIBLE")
-                 Progress new_wanted_work new_work new_is solved -> do
-                   addInerts new_is
-                   let mkWanted (tv, xi) =
-                        do ev <- newWantedEvVarNC (mkEqPred (mkTyVarTy tv) xi)
-                           return $ CTyEqCan
-                             { cc_ev = ev, cc_tyvar = tv, cc_rhs = xi
-                             , cc_loc = cc_loc wi }
-                   mapM_ setEvidence solved
-                   new_wanted_cts <- mapM mkWanted new_wanted_work
-                   updWorkListTcS $ extendWorkListEqs $
-                     new_wanted_cts ++ new_work
-                   let dbg x ys = text x $$ nest 2 (vcat $ map ppr ys)
-                   traceTcS "[NATS]" $
-                     text "Progress" $$
-                        nest 2 (vcat
-                          [ dbg "New wanted work:" (new_wanted_cts ++ new_work)
-                          , dbg "Solved:" (map fst solved)
-                          , dbg "Inerts" new_is
-                          ]
-                        )
-             ; return $ SomeTopInt "LinArith" Stop
+       | thyRelevant linArith fun_tc args =
+          do { (gis,wis) <- getRelevantCtsFor linArith
+             ; decideExternal linArith gis wis wi
              }
 
        | otherwise = return NoTopInt
@@ -1532,20 +1500,123 @@ doTopReactFunEq wi fl fun_tc args xi loc
         xcomp _   = panic "No more goals!"
         xev = XEvTerm xcomp xdecomp
 
--- This gets givens and wanteds relevant to the numeric solver.
--- The givens are just copies of what's in the inert set, while the wanteds
--- are removed from the inert set.
-getRelevantLinArithInerts :: TcS ([Ct], [Ct])
-getRelevantLinArithInerts =
+decideExternal :: Theory t e v -> [Ct] -> [Ct] -> Ct -> TcS TopInteractResult
+decideExternal thy givenCts wantedCts goalCt =
+  do proved <- prove assumptions goal
+     if proved
+       then do when (ctFlavour goalCt == Wanted) (solve goalCt)
+               mapM_ insertInertItemTcS wantedCts
+               done Stop
+
+            -- Check if we are consistent with existing context
+       else do res <- check (goal : assumptions)
+               case res of
+                 Unsat   -> emitInsoluble goalCt >> done Stop
+                 Unknown -> improve [] >>= prune >> done (ContinueWith goalCt)
+                 Sat mo  -> improve mo >>= prune >> done (ContinueWith goalCt)
+
+  where
+  assumptions
+    | ctFlavour goalCt == Wanted = givens ++ wanteds
+    | otherwise                  = givens
+
+  improve model =
+    do let candidates =
+             [ ( thyEq thy (thyVar thy x) (thyVal thy v)
+               , (xv, thyFromValue thy v)
+               ) | (x, v) <- model, xv <- maybeToList (Map.lookup x varMap) ]
+             ++
+             [ ( thyEq thy (thyVar thy x) (thyVar thy y)
+               , (xv, mkTyVarTy yv)
+               ) | (x,xv):xs <- tails vars
+                 , (y,yv)    <- xs
+                 , eqType (tyVarKind xv) (tyVarKind yv) ]
+       fmap catMaybes $ forM candidates $ \(prop,imp) ->
+         do proved <- prove (goal : assumptions) prop
+            return (if proved then Just imp else Nothing)
+
+  prune eqs
+    | ctFlavour goalCt == Given = addWork (wantedCts ++ map toGivenEqCt eqs)
+                                    -- kick-out wanteds, hopefully none!
+    | otherwise =
+      do addWork =<< mapM toWantedEqCt eqs
+         simplifyInerts (zip wanteds wantedCts) (goal : givens)
+
+  simplifyInerts [] _ = return ()
+  simplifyInerts ((p, ct):todo) assmps =
+    do proved <- prove (map fst todo ++ assmps) p
+       if proved
+         then do solve ct
+                 simplifyInerts todo assmps
+         else do insertInertItemTcS ct
+                 simplifyInerts todo (p:assmps)
+
+  -- Convert to the theory's representations
+  givens    = map ctToTerm givenCts
+  wanteds   = map ctToTerm wantedCts
+  goal      = ctToTerm goalCt
+  vars      = getVars (goalCt : wantedCts ++ givenCts)
+  varMap    = Map.fromList vars
+
+  ctToTerm CFunEqCan { cc_fun = tc, cc_tyargs = ts, cc_rhs = xi } =
+    thyToProp thy tc (map (thyToTerm thy) ts) (thyToTerm thy xi)
+  ctToTerm ct = pprPanic "ctToTerm" (text (thyName thy) <+> ppr ct)
+
+  getVars :: [Ct] -> [(String,TyVar)]
+  getVars = map addName . foldUniqSet (:) [] . tyVarsOfTypes . concatMap ctTypes
+    where addName x = (thyVarName x, x)
+
+          ctTypes CFunEqCan { cc_tyargs = [t1,t2], cc_rhs = xi } = [t1,t2,xi]
+          ctTypes ct = pprPanic "getVarTys" (ppr ct)
+
+  -- Convenient names for common things:
+  toWantedEqCt (tv, xi) =
+    do ev <- newWantedEvVarNC (mkEqPred (mkTyVarTy tv) xi)
+       return $ CTyEqCan { cc_ev = ev, cc_tyvar = tv, cc_rhs = xi
+                         , cc_loc = cc_loc goalCt }
+
+  toGivenEqCt :: (TyVar,Xi) -> Ct
+  toGivenEqCt (tv, rhs) =
+    let lhs = mkTyVarTy tv
+    in CTyEqCan { cc_ev = CtGiven { ctev_pred = mkEqPred lhs rhs
+                                  , ctev_evtm =thyEv thy lhs rhs }
+                , cc_loc = cc_loc goalCt, cc_tyvar = tv, cc_rhs = rhs }
+
+  solve :: Ct -> TcS ()
+  solve ct    = setEvBind (ctEvId $ ctEvidence ct)
+              $ uncurry (thyEv thy) $ getEqPredTys $ ctPred ct
+
+  done :: StopOrContinue -> TcS TopInteractResult
+  done x = return (SomeTopInt (thyName thy) x)
+
+  addWork :: [Ct] -> TcS ()
+  addWork cs  = updWorkListTcS (extendWorkListCts cs)
+
+  check = liftIO . thySat thy [ (x, thyToType thy (tyVarKind xv))
+                                                    | (x,xv) <- vars ]
+
+  prove ps p =
+    do x <- check (thyNot thy p : ps)
+       case x of
+         Unsat -> return True
+         _     -> return False
+
+
+
+{- This gets givens and wanteds relevant to the specified theory.
+The givens are just copies of what's in the inert set, while the wanteds
+are removed from the inert set. -}
+getRelevantCtsFor :: Theory t e v -> TcS ([Ct], [Ct])
+getRelevantCtsFor thy =
   modifyInertTcS $ upd $ \fun_eqs->
-    let (wanteds, rest_funeqs) = partCtFamHeadMap (isArith Wanted) fun_eqs
-        givens = getCtFamHeadMapCts (isArith Given) rest_funeqs
+    let (wanteds, rest_funeqs) = partCtFamHeadMap (consider Wanted) fun_eqs
+        givens = getCtFamHeadMapCts (consider Given) rest_funeqs
     in ((bagToList givens, bagToList wanteds), rest_funeqs)
 
   where
-  isArith fl ct
+  consider fl ct
     | fl == ctFlavour ct
-    , Just (tc,tys) <- isCFunEqCan_maybe ct = isLinArithTyCon tc tys
+    , Just (tc,tys) <- isCFunEqCan_maybe ct = thyRelevant thy tc tys
     | otherwise = False
 
   upd f i =
diff --git a/compiler/typecheck/TcTypeNats.hs b/compiler/typecheck/TcTypeNats.hs
index e4373efd1c..09b12b33dd 100644
--- a/compiler/typecheck/TcTypeNats.hs
+++ b/compiler/typecheck/TcTypeNats.hs
@@ -2,9 +2,8 @@ module TcTypeNats
   ( typeNatTyCons
   , typeNatCoAxiomRules
   , TcBuiltInSynFamily(..)
-  , LinArithResult(..)
-  , decideLinArith
-  , isLinArithTyCon
+  , Theory(..), Result(..), thyVarName
+  , linArith
   ) where
 
 import Type
@@ -12,13 +11,12 @@ import Pair
 import TcType     ( TcType )
 import TyCon      ( TyCon, SynTyConRhs(..), mkSynTyCon, TyConParent(..)  )
 import Coercion   ( Role(..) )
-import TcRnTypes  ( Xi, Ct(..), CtLoc, ctFlavour, ctPred, CtFlavour(..)
-                  , CtEvidence(..) )
+import TcRnTypes  ( Xi )
 import TcEvidence ( mkTcAxiomRuleCo, TcCoercion, EvTerm(..) )
 import CoAxiom    ( CoAxiomRule(..) )
 import Name       ( Name, BuiltInSyntax(..), nameUnique, nameOccName )
 import OccName    ( occNameString )
-import Var        ( tyVarName, tyVarKind )
+import Var        ( tyVarName )
 import TysWiredIn ( typeNatKind, mkWiredInTyConName
                   , promotedBoolTyCon
                   , promotedFalseDataCon, promotedTrueDataCon
@@ -34,21 +32,13 @@ import PrelNames  ( gHC_TYPELITS
                   )
 import FamInst    ( TcBuiltInSynFamily(..) )
 import FastString ( FastString, fsLit )
-import Outputable ( ppr, panic, pprPanic )
-import UniqSet    ( foldUniqSet )
+import Outputable ( ppr, panic, pprPanic, (<+>), text, int )
 import qualified Data.Map as Map
-import           Data.Map (Map)
 import Data.Maybe ( isJust )
-import Data.List  ( tails, genericReplicate )
-import Data.List  ( genericReplicate )
 import System.Cmd ( system )
+import System.Exit ( ExitCode(..) )
 
 
-isLinArithTyCon :: TyCon -> [Xi] -> Bool
-isLinArithTyCon tc ts =
-  tc `elem` [ typeNatAddTyCon, typeNatLeqTyCon, typeNatSubTyCon ] ||
-  (tc == typeNatMulTyCon && any (isJust . isNumLitTy) ts)
-
 
 {-------------------------------------------------------------------------------
 Built-in type constructors for functions on type-lelve nats
@@ -582,56 +572,138 @@ genLog x base = Just (exactLoop 0 x)
 
 
 {- -----------------------------------------------------------------------------
-Calling an external decision procedure
+Calling an external decision procedure: generic interface
 ----------------------------------------------------------------------------- -}
 
-data LinArithResult = SolvedWanted EvTerm
-                    | IgnoreGiven
-                    | Impossible
-                    | Progress [(TyVar, Xi)] [Ct] [Ct] [(Ct, EvTerm)]
-                        -- Args:
-                        -- 1) turn into wanted and add to work list,
-                        -- 2) stick in work list, and
-                        -- 3) add to inert set
-                        -- 4) discharged, set evidence
-
-data Op   = Add | Sub | Mul | Leq | Eq | Implies | And
-           deriving Show
-
-data Term = Op Term Op Term
-          | Num Integer
-          | Bool Bool
-          | Var String
-          | Not Term
-
-termToSMT :: Term -> Expr
-termToSMT term =
-  case term of
-    Op t1 op t2 -> opToSMT op (termToSMT t1) (termToSMT t2)
-    Num x       -> fromInteger x
-    Bool x      -> if x then true else false
-    Not t       -> eNot (termToSMT t)
-    Var x       -> app x []
-
-opToSMT :: Op -> Expr -> Expr -> Expr
-opToSMT op =
-  case op of
-    Add         -> (+)
-    Sub         -> (-)
-    Mul         -> (*)
-    Leq         -> nLeq
-    Eq          -> (====)
-    Implies     -> (===>)
-    And         -> eAnd
-
-instance Show Term where
+data Theory ty expr value = Theory
+  { thyName       :: String
+
+  , thyRelevant   :: TyCon -> [Type] -> Bool
+
+  , thyToProp     :: TyCon -> [expr] -> expr -> expr
+  , thyToTerm     :: Type  -> expr
+  , thyToType     :: Kind  -> ty
+  , thyFromValue  :: value -> Xi
+
+  , thyVal        :: value  -> expr
+  , thyVar        :: String -> expr
+  , thyEq         :: expr -> expr -> expr
+  , thyNot        :: expr -> expr
+
+  , thySat        :: [(String,ty)] -> [expr] -> IO (Result value)
+  , thyEv         :: Xi -> Xi -> EvTerm
+  }
+
+data Result v   = Sat [(String, v)]
+                | Unsat
+                | Unknown
+                  deriving (Show)
+
+thyVarName :: TyVar -> String
+thyVarName x = let n = tyVarName x
+                   u = nameUnique n
+               in occNameString (nameOccName n) ++ "_" ++ show u
+
+
+
+{-------------------------------------------------------------------------------
+Concrete instance for the theory of natural numbers
+-------------------------------------------------------------------------------}
+
+data Ty     = TNat | TBool
+
+data Op     = Add | Sub | Mul | Leq | Eq
+
+data Expr   = Op Op Expr Expr
+            | Not Expr
+            | Num Integer
+            | Bool Bool
+            | Var String
+
+data Value  = VInt Integer | VBool Bool
+
+linArith :: Theory Ty Expr Value
+linArith = Theory
+  { thyName       = "linArith"
+
+  , thyRelevant   = laRelevant
+
+  , thyToProp     = laToProp
+  , thyToTerm     = laToExpr
+  , thyToType     = laToType
+  , thyFromValue  = laFromValue
+
+  , thyVal        = laValExpr
+  , thyVar        = Var
+  , thyEq         = \e1 e2 -> Op Eq e1 e2
+  , thyNot        = Not
+
+  , thySat        = laSat
+  , thyEv         = evBySMT
+  }
+
+laRelevant :: TyCon -> [Type] -> Bool
+laRelevant tc ts =
+  tc `elem` [ typeNatAddTyCon, typeNatLeqTyCon, typeNatSubTyCon ] ||
+    (tc == typeNatMulTyCon && any (isJust . isNumLitTy) ts)
+
+
+laToProp :: TyCon -> [Expr] -> Expr -> Expr
+laToProp tc [e1,e2] e = Op Eq (Op (laToOp tc) e1 e2) e
+laToProp tc es _      = pprPanic "linArith"
+                          $ text "Unexpected arity for" <+> ppr tc
+                                                        <+> int (length es)
+
+laToOp :: TyCon -> Op
+laToOp tc
+  | tc == typeNatAddTyCon = Add
+  | tc == typeNatSubTyCon = Sub
+  | tc == typeNatMulTyCon = Mul
+  | tc == typeNatLeqTyCon = Leq
+  | otherwise             = pprPanic "tyConToOp" (ppr tc)
+
+laToExpr :: Type -> Expr
+laToExpr ty
+  | Just x <- getTyVar_maybe ty             = Var (thyVarName x)
+  | Just x <- isNumLitTy ty                 = Num x
+  | Just (tc,[]) <- splitTyConApp_maybe ty
+  , Just x <- tyConToBool tc                = Bool x
+  | otherwise                               = pprPanic "typeToTerm" (ppr ty)
+
+tyConToBool :: TyCon -> Maybe Bool
+tyConToBool tc
+  | tc == promotedTrueDataCon  = Just True
+  | tc == promotedFalseDataCon = Just False
+tyConToBool _ = Nothing
+
+
+
+laFromValue :: Value -> Xi
+laFromValue (VInt n)  = num n
+laFromValue (VBool b) = bool b
+
+laValExpr :: Value -> Expr
+laValExpr (VInt n)     = Num n
+laValExpr (VBool b)    = Bool b
+
+laToType :: Kind -> Ty
+laToType k =
+  case splitTyConApp_maybe k of
+    Just (tc,[])
+      | tc == promotedBoolTyCon -> TBool
+      | tc == typeNatKindCon    -> TNat
+    _ -> pprPanic "laToType" (text "Unexpected kind:" <+> ppr k)
+
+
+-- For debugging
+instance Show Expr where
   showsPrec p v =
     case v of
       Num n -> shows n
       Var s -> showString s
       Not v -> showParen (p > 8) $ showString "!" . showsPrec 8 v
       Bool b -> shows b
-      Op a o b -> showParen (p > pOp) $ showsPrec pL a . showString opStr
+      Op o a b -> showParen (p > pOp) $ showsPrec pL a . showString opStr
                                       . showsPrec pR b
         where
           (pOp, pL, pR, opStr) =
@@ -641,151 +713,12 @@ instance Show Term where
               Mul -> (7, 7, 8, " * ")
               Leq -> (4, 5, 5, " <= ")
               Eq  -> (4, 5, 5, " == ")
-              Implies -> (1, 2, 1, " -> ")
-              And -> (3, 4, 3, " & ")
 
-tyConToOp :: TyCon -> Op
-tyConToOp tc
-  | tc == typeNatAddTyCon = Add
-  | tc == typeNatSubTyCon = Sub
-  | tc == typeNatMulTyCon = Mul
-  | tc == typeNatLeqTyCon = Leq
-  | otherwise             = pprPanic "tyConToOp" (ppr tc)
-
-tyConToBool :: TyCon -> Maybe Bool
-tyConToBool tc
-  | tc == promotedTrueDataCon  = Just True
-  | tc == promotedFalseDataCon = Just False
-tyConToBool _ = Nothing
-
-varName :: TyVar -> String
-varName x = let n = tyVarName x
-                u = nameUnique n
-            in occNameString (nameOccName n) ++ "_" ++ show u
-
-typeToTerm :: Type -> Term
-typeToTerm ty
-  | Just x <- getTyVar_maybe ty = Var (varName x)
-  | Just x <- isNumLitTy ty = Num x
-  | Just (tc,[]) <- splitTyConApp_maybe ty
-  , Just x <- tyConToBool tc = Bool x
-  | otherwise = pprPanic "typeToTerm" (ppr ty)
-
-ctToTerm :: Ct -> Term
-ctToTerm CFunEqCan { cc_fun = tc, cc_tyargs = [t1,t2], cc_rhs = xi } =
-  Op (Op (typeToTerm t1) (tyConToOp tc) (typeToTerm t2)) Eq (typeToTerm xi)
-ctToTerm ct = pprPanic "ctToTerm" (ppr ct)
-
-termToType :: VarMap -> Term -> Xi
-termToType vmap t =
-  case t of
-    Num n  -> num n
-    Bool b -> bool b
-    Var x  -> mkTyVarTy $ stringToTyVar vmap x
-    _      -> panic ("termToType: " ++ show t)
-
-stringToTyVar :: VarMap -> String -> TyVar
-stringToTyVar vmap x =
-  case Map.lookup x vmap of
-    Just ty -> ty
-    Nothing -> panic ("stringToTyVar: " ++ x)
-
-
-decideLinArith :: [Ct] -> [Ct] -> Ct -> IO LinArithResult
-decideLinArith givenCts wantedCts goalCt = decide
-  where
-  givens  = map ctToTerm givenCts
-  wanteds = map ctToTerm wantedCts
-  goal    = ctToTerm goalCt
-  varMap  = getVarTys (goalCt : wantedCts ++ givenCts)
-  flav    = ctFlavour goalCt
-
-  bySMT   = uncurry evBySMT . getEqPredTys . ctPred
-
-  noProgress = return (Progress [] [] (goalCt : wantedCts)) []
-
-  assumptions
-    | flav == Wanted = givens ++ wanteds
-    | otherwise      = givens
-
-  decide =
-    do yes <- prove varMap (assumptions ==> goal)
-       if yes
-          then return (if flav == Given then IgnoreGiven
-                                        else SolvedWanted (bySMT goalCt))
-          else checkConsistent
-
-  checkConsistent =
-    do res <- sat varMap (ands $ goal : assumptions)
-       case res of
-         Unsat   -> return Impossible
-         Unknown -> improve []
-         Sat m   -> improve m
-
-  improve model =
-    do let candidates =
-             [ (x, valueToTerm v) | (x, v) <- model ] ++
-             [ (x, Var y) | (x,xv):xs <- tails (Map.toList varMap)
-                          , (y,yv)    <- xs
-                          , eqType (tyVarKind xv) (tyVarKind yv) ]
-       eqs <- fmap concat $ mapM tryAssign candidates
-       prune eqs
-
-  tryAssign (x, t) =
-    do yes <- prove varMap (goal : assumptions ==> Op (Var x) Eq t)
-       if not yes
-          then return []
-          else return [(x, t)]
-
-  prune eqs
-    | flav == Given =
-      do let newGiven = map (mkGivenCt varMap $ cc_loc goalCt) eqs
-         return $ Progress [] (wantedCts ++ newGiven) [goalCt] []
-    | otherwise =
-      do let newWanted = [ (stringToTyVar varMap x, termToType varMap t)
-                         | (x, t) <- eqs ]
-         (newInerts, solved) <-
-            simplifyInerts (zip wanteds wantedCts)
-                           (goal : givens) [goalCt] []
-         return $ Progress newWanted [] newInerts solved
-
-  simplifyInerts [] _ done solved = return (done, solved)
-  simplifyInerts ((p, ct):todo) assmps done solved =
-    do yes <- prove varMap (map fst todo ++ assmps ==> p)
-       if yes
-          then simplifyInerts todo assmps done ((ct, bySMT ct):solved)
-          else simplifyInerts todo (p:assmps) (ct:done) solved
-
-mkGivenCt :: VarMap -> CtLoc -> (String, Term) -> Ct
-mkGivenCt varMap loc (x, t) =
-    CTyEqCan { cc_ev = ev, cc_loc = loc, cc_tyvar = tv, cc_rhs = rhs }
-  where
-    ev = CtGiven { ctev_pred = mkEqPred lhs rhs
-                 , ctev_evtm = evBySMT lhs rhs }
-    tv  = stringToTyVar varMap x
-    lhs = mkTyVarTy tv
-    rhs = termToType varMap t
-
-getVarTys :: [Ct] -> VarMap
-getVarTys = Map.fromList
-          . map addName
-          . foldUniqSet (:) []
-          . tyVarsOfTypes
-          . concatMap ctTypes
-  where
-  addName x = (varName x, x)
-
-  ctTypes CFunEqCan { cc_tyargs = [t1,t2], cc_rhs = xi } = [t1,t2,xi]
-  ctTypes ct = pprPanic "getVarTys" (ppr ct)
 
 --------------------------------------------------------------------------------
+-- Calling the solver
 
-data Result = Sat [(String, Value)]
-            | Unsat
-            | Unknown
-              deriving (Show)
-
-instance Read Result where
+instance Read (Result Value) where
   readsPrec _ xs = do ("sat", xs1) <- lex xs
                       (vs,rest) <- readParen True getVals xs1
                       return (Sat vs, rest)
@@ -804,450 +737,54 @@ instance Read Result where
                                         return ((name,val), rest1)
 
 
-
-data Value = VInt Integer | VBool Bool
-
-instance Show Value where
-  show (VInt n)  = show n
-  show (VBool b) = show b
-
 instance Read Value where
   readsPrec p s = [ (VInt n,  s')     | (n, s') <- readsPrec p s ] ++
                   [ (VBool True, s')  | ("true", s') <- lex s ] ++
                   [ (VBool False, s') | ("false", s') <- lex s ]
 
-valueToTerm :: Value -> Term
-valueToTerm (VInt n)  = Num n
-valueToTerm (VBool b) = Bool b
 
-type VarMap = Map String TyVar
-
-sat :: VarMap -> Term -> IO Result
-sat varMap t =
-  do writeFile "ghc_input.smt" $ pp script
-     system ("cvc4 --lang=smtlib2 -m ghc_input.smt > ghc_output.smt")
+laSat :: [(String,Ty)] -> [Expr] -> IO (Result Value)
+laSat varMap ts =
+  do writeFile "ghc_input.smt" script
+     _ <- system ("cvc4 --lang=smtlib2 -m ghc_input.smt > ghc_output.smt")
      txt <- readFile "ghc_output.smt"
-     {-
-     putStrLn (replicate 50 '-')
-     print t
-     putStrLn (replicate 50 '-')
-     putStrLn txt
-     putStrLn (replicate 50 '-')
-     -}
      case reads txt of
        [(v,_)] -> return v
        _ -> panic $ "sat:\n" ++ txt
   where
-  declareVar (x,tv) =
-    case splitTyConApp_maybe (tyVarKind tv) of
-      Just (tc,[])
-        | tc == promotedBoolTyCon -> [ CmdDeclareFun (N x) [] tBool ]
-        | tc == typeNatKindCon    -> [ CmdDeclareFun (N x) [] tInt
-                                     , CmdAssert (nGeq (app x []) 0)
-                                     ]
-
-      -- XXX: Could we encounter a kind variable?
-      _ -> pprPanic "sat" (ppr (tyVarKind tv))
-
-  script =
-    Script $ [ CmdSetLogic (N "QF_LIA") ]
-          ++ concatMap declareVar (Map.toList varMap)
-          ++ [ CmdAssert (termToSMT t)
-             , CmdCheckSat
-             , CmdGetValue [ app x [] | x <- Map.keys varMap ]
-             ]
-
-
-prove :: VarMap -> Term -> IO Bool
-prove varMap p =
-  do x <- sat varMap (Not p)
-     case x of
-       Unsat -> return True
-       _     -> return False
-
-ands :: [Term] -> Term
-ands [] = Bool True
-ands ps = foldr1 (\x y -> Op x And y) ps
+  sexpr ws = "(" ++ unwords ws ++ ")"
 
-infixr 1 ==>
-
-(==>) :: [Term] -> Term -> Term
-[] ==> q  = q
-ps ==> q  = Op (ands ps) Implies q
-
-
---------------------------------------------------------------------------------
-
-
-
-
-newtype SmtName  = N String
-                deriving (Eq,Ord,Show)
-
-data Ident    = I SmtName [Integer]
-                deriving (Eq,Ord,Show)
-
-data Quant    = Exists | Forall
-                deriving (Eq,Ord,Show)
-
-data Binder   = Bind { bindVar :: SmtName, bindSmtType :: SmtType }
-                deriving (Eq,Ord,Show)
-
-data Defn     = Defn { defVar :: SmtName, defExpr :: Expr }
-                deriving (Eq,Ord,Show)
-
-data Literal  = LitNum Integer
-              | LitFrac Rational
-              | LitStr String
-                deriving (Eq,Ord,Show)
-
-data SmtType     = TApp Ident [SmtType]
-              | TVar SmtName
-                deriving (Eq,Ord,Show)
-
-data Expr     = Lit Literal
-              | App Ident (Maybe SmtType) [Expr]
-              | Quant Quant [Binder] Expr
-              | Let [Defn] Expr
-              | Annot Expr [Attr]
-                deriving (Eq,Ord,Show)
-
-data Attr     = Attr { attrName :: SmtName , attrVal :: Maybe AttrVal }
-                deriving (Eq,Ord,Show)
-
-type AttrVal  = Expr    -- A bit of an approximation....
-
-
-data Option
-  = OptPrintSuccess Bool
-  | OptExpandDefinitions Bool
-  | OptInteractiveMode Bool
-  | OptProduceProofs Bool
-  | OptProduceUnsatCores Bool
-  | OptProduceModels Bool
-  | OptProduceAssignments Bool
-  | OptRegularOutputChannel String
-  | OptDiagnosticOutputChannel String
-  | OptRandomSeed Integer
-  | OptVerbosity Integer
-  | OptAttr Attr
-
-data InfoFlag
-  = InfoAllStatistics
-  | InfoErrorBehavior
-  | InfoName
-  | InfoAuthors
-  | InfoVersion
-  | InfoStatus
-  | InfoReasonUnknown
-  | InfoAttr Attr
-
-data Command
-  = CmdSetLogic SmtName
-  | CmdSetOption Option
-  | CmdSetInfo Attr
-  | CmdDeclareSmtType SmtName Integer
-  | CmdDefineSmtType SmtName [SmtName] SmtType
-  | CmdDeclareFun SmtName [SmtType] SmtType
-  | CmdDefineFun SmtName [Binder] SmtType Expr
-  | CmdPush Integer
-  | CmdPop Integer
-  | CmdAssert Expr
-  | CmdCheckSat
-  | CmdGetAssertions
-  | CmdGetValue [Expr]
-  | CmdGetProof
-  | CmdGetUnsatCore
-  | CmdGetInfo InfoFlag
-  | CmdGetOption SmtName
-  | CmdExit
-
-newtype Script = Script [Command]
-
-
---------------------------------------------------------------------------------
--- To make it a bit simpler to write terms in the above AST
--- we provide some instances.  They are intended to be used only
--- for writing simple literals, and not any of the computational
--- operations associated with the classes.
-
-{-
--- Strings
-instance IsString SmtName      where fromString   = N
-instance IsString Ident     where fromString x = I (fromString x) []
-instance IsString SmtType      where fromString x = TApp (fromString x) []
-instance IsString Expr      where fromString   = Lit . LitStr . fromString
--}
-
--- Integers
-
--- NOTE: Some of these might not mean anything, depending on the theory.
-instance Num Expr where
-  fromInteger x = Lit (LitNum x)
-  x + y         = app "+"      [x,y]
-  x - y         = app "-"      [x,y]
-  x * y         = app "*"      [x,y]
-  signum x      = app "signum" [x]
-  abs x         = app "abs"    [x]
-
-
--- Fractional numbers
-instance Fractional Expr where
-  fromRational x  = Lit (LitFrac x)
-  x / y           = app "/" [x,y]
-
-app :: String -> [Expr] -> Expr
-app f es = App (I (N f) []) Nothing es
-
---------------------------------------------------------------------------------
-type Doc = String
-
-x <+> y   = fsep [x,y]
-(<>)      = (++)
-nest _ x  = x
-integer   = show
-char x    = [x]
-parens x  = "(" ++ x ++ ")"
-fsep      = unwords
-x $$ y    = x ++ "\n" ++ y
-vcat      = unlines
-text      = id
-empty     = ""
-
-
-class PP t where
-  pp :: t -> Doc
-
-instance PP Bool where
-  pp True   = text "true"
-  pp False  = text "false"
-
-instance PP Integer where
-  pp        = integer
-
-ppString :: String -> Doc
-ppString = text . show
-
-instance PP SmtName where
-  pp (N x) = text x
-
-instance PP Ident where
-  pp (I x []) = pp x
-  pp (I x is) = parens (char '_' <+> pp x <+> fsep (map integer is))
-
-instance PP Attr where
-  pp (Attr x v) = char ':' <> pp x <+> maybe empty pp v
-
-instance PP Quant where
-  pp Forall = text "forall"
-  pp Exists = text "exists"
-
-instance PP Expr where
-  pp expr =
-    case expr of
-
-      Lit l     -> pp l
-
-      App c ty ts  ->
-        case ts of
-          [] -> ppFun
-          _  -> parens (ppFun <+> fsep (map pp ts))
-
-        where ppFun = case ty of
-                        Nothing -> pp c
-                        Just t  -> parens (text "as" <+> pp c <+> pp t)
-
-      Quant q bs e ->
-        case bs of
-          [] -> pp e
-          _  -> parens (pp q <+> parens (fsep (map pp bs)) $$ nest 2 (pp e))
-
-      Let ds e ->
-        case ds of
-          [] -> pp e
-          _  -> parens (text "let" <+> (parens (vcat (map pp ds)) $$ pp e))
-
-      Annot e as ->
-        case as of
-          [] -> pp e
-          _  -> parens (char '!' <+> pp e $$ nest 2 (vcat (map pp as)))
-
-
-instance PP Binder where
-  pp (Bind x t) = parens (pp x <+> pp t)
-
-instance PP Defn where
-  pp (Defn x e)   = parens (pp x <+> pp e)
-
-instance PP SmtType where
-  pp ty =
+  declareVar (x,ty) =
     case ty of
-      TApp c ts ->
-        case ts of
-          [] -> pp c
-          _  -> parens (pp c <+> fsep (map pp ts))
-      TVar x -> pp x
-
-instance PP Literal where
-  pp lit =
-    case lit of
-
-      LitNum n -> integer n
-
-      LitFrac x -> text (show (fromRational x :: Double))  -- XXX: Good enough?
-
-      LitStr x -> ppString x
-
-
-
-instance PP Option where
-  pp opt =
-    case opt of
-      OptPrintSuccess b             -> std "print-success" b
-      OptExpandDefinitions b        -> std "expand-definitions" b
-      OptInteractiveMode b          -> std "interactive-mode" b
-      OptProduceProofs b            -> std "produce-proofs" b
-      OptProduceUnsatCores b        -> std "produce-unsat-cores" b
-      OptProduceModels b            -> std "produce-models" b
-      OptProduceAssignments b       -> std "produce-assignments" b
-      OptRegularOutputChannel s     -> str "regular-output-channel" s
-      OptDiagnosticOutputChannel s  -> str "diagnostic-output-channel" s
-      OptRandomSeed n               -> std "random-seed" n
-      OptVerbosity n                -> std "verbosity" n
-      OptAttr a                     -> pp a
-
-    where mk a b  = char ':' <> text a <+> b
-          std a b = mk a (pp b)
-          str a b = mk a (ppString b)
-
-instance PP InfoFlag where
-  pp info =
-    case info of
-      InfoAllStatistics -> mk "all-statistics"
-      InfoErrorBehavior -> mk "error-behavior"
-      InfoName          -> mk "name"
-      InfoAuthors       -> mk "authors"
-      InfoVersion       -> mk "version"
-      InfoStatus        -> mk "status"
-      InfoReasonUnknown -> mk "reason-unknown"
-      InfoAttr a        -> pp a
-    where mk x = char ':' <> text x
-
-instance PP Command where
-  pp cmd =
-    case cmd of
-      CmdSetLogic n     -> std "set-logic" n
-      CmdSetOption o    -> std "set-options" o
-      CmdSetInfo a      -> std "set-info" a
-      CmdDeclareSmtType x n    -> mk "declare-sort" (pp x <+> integer n)
-      CmdDefineSmtType x as t  -> fun "define-sort" x as (pp t)
-      CmdDeclareFun x ts t  -> fun "declare-fun" x ts (pp t)
-      CmdDefineFun x bs t e -> fun "define-fun" x bs (pp t $$ nest 2 (pp e))
-      CmdPush n         -> std "push" n
-      CmdPop n          -> std "pop" n
-      CmdAssert e       -> std "assert" e
-      CmdCheckSat       -> one "check-sat"
-      CmdGetAssertions  -> one "get-assertions"
-      CmdGetValue es    -> mk  "get-value" (parens (fsep (map pp es)))
-      CmdGetProof       -> one "get-proof"
-      CmdGetUnsatCore   -> one "get-unsat-core"
-      CmdGetInfo i      -> std "get-info" i
-      CmdGetOption n    -> std "get-option" n
-      CmdExit           -> one "exit"
-    where mk x d = parens (text x <+> d)
-          one x   = mk x empty
-          std x a = mk x (pp a)
-          fun x y as d = mk x (pp y <+> parens (fsep (map pp as)) <+> d)
-
-instance PP Script where
-  pp (Script cs) = vcat (map pp cs)
-
-
-
-tBool :: SmtType
-tBool = TApp (I (N "Bool") []) []
-
-true :: Expr
-true = app "true" []
-
-false :: Expr
-false = app "false" []
-
-eNot :: Expr -> Expr
-eNot p = app "not" [p]
-
-(===>) :: Expr -> Expr -> Expr
-p ===> q = app "=>" [p,q]
-
-eAnd :: Expr -> Expr -> Expr
-eAnd p q = app "and" [p,q]
-
-eOr :: Expr -> Expr -> Expr
-eOr p q = app "or" [p,q]
-
-eXor :: Expr -> Expr -> Expr
-eXor p q = app "xor" [p,q]
-
-(====) :: Expr -> Expr -> Expr
-x ==== y = app "=" [x,y]
-
-(=/=) :: Expr -> Expr -> Expr
-x =/= y = app "distinct" [x,y]
-
-ite :: Expr -> Expr -> Expr -> Expr
-ite b x y = app "ite" [b,x,y]
-
-
-
-tInt :: SmtType
-tInt = TApp (I (N "Int") []) []
-
-nNeg :: Expr -> Expr
-nNeg x = app "-" [x]
-
-nSub :: Expr -> Expr -> Expr
-nSub x y = app "-" [x,y]
-
-nAdd :: Expr -> Expr -> Expr
-nAdd x y = app "+" [x,y]
-
-nMul :: Expr -> Expr -> Expr
-nMul x y = app "*" [x,y]
-
-nDiv :: Expr -> Expr -> Expr
-nDiv x y = app "div" [x,y]
-
-nMod :: Expr -> Expr -> Expr
-nMod x y = app "mod" [x,y]
-
-nAbs :: Expr -> Expr
-nAbs x = app "abs" [x]
-
-nLeq :: Expr -> Expr -> Expr
-nLeq x y = app "<=" [x,y]
-
-nLt :: Expr -> Expr -> Expr
-nLt x y = app "<" [x,y]
-
-nGeq :: Expr -> Expr -> Expr
-nGeq x y = app ">=" [x,y]
-
-nGt :: Expr -> Expr -> Expr
-nGt x y = app ">" [x,y]
-
-
-
-example =
-  Script
-    [ CmdSetLogic (N "QF_LIA")
-    , CmdDeclareFun (N "x") [] tInt
-    , CmdDeclareFun (N "y") [] tInt
-    , CmdDeclareFun (N "z") [] tBool
-    , CmdAssert $ nGeq (app "x" []) (app "y" []) ==== (app "z" [])
-    , CmdCheckSat
-    , CmdGetValue [ app "x" [], app "y" [], app "z" [] ]
-    ]
-
-
+      TBool -> [ sexpr [ "declare-fun", x, sexpr [], "Bool" ] ]
+      TNat  -> [ sexpr [ "declare-fun", x, sexpr [], "Int"  ]
+               , sexpr [ "assert", sexpr [ "<=", "0", x ] ]
+               ]
+
+  script = unlines
+     $ [ sexpr [ "set-logic", "QF_LIA" ] ]
+    ++ concatMap declareVar varMap
+    ++ [ sexpr ["assert", termToSMT t] | t <- ts ]
+    ++ [ sexpr [ "check-sat" ]
+       , sexpr [ "get-value", sexpr (map fst varMap) ]
+       ]
+
+
+  termToSMT term =
+    case term of
+      Op op e1 e2 -> sexpr [opToSMT op, termToSMT e1, termToSMT e2]
+      Not e       -> sexpr ["not", termToSMT e]
+      Num x | x >= 0    -> show x
+            | otherwise -> sexpr ["-", show (negate x)]
+      Bool x -> if x then "true" else "false"
+      Var x  -> x
+
+  opToSMT op =
+    case op of
+      Add -> "+"
+      Sub -> "-"
+      Mul -> "*"
+      Leq -> "<="
+      Eq  -> "="