Hook-up an SMT solver.

NOTE: This uses a very naive method to call the SMT solver:

* GHC will call a program called cvc4, which better be an SMT solver, which is in the path
* GHC will create (overwrite!) two files "ghc_input.smt" and "ghc_output,smt"
  two files in the current directory.

4 files changed, 738 insertions, 14 deletions

diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index 5f6da438c7..118b99df78 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -1473,19 +1473,42 @@ doTopReactFunEq wi fl fun_tc args xi loc
     fam_ty = mkTyConApp fun_tc args
 
     try_improve_and_return
-       | isLinArithTyCon fun_tc =
-          do { (gis,wis) <- undefined -- getRelevantLinArithInerts
+       | 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
-                   setEvBind (ctEvId $ ctEvidence wi) ev
+                   setEvidence (wi, ev)
+                   traceTcS "[NATS]" (text "SOLVED WANTED")
                  IgnoreGiven -> do
                    addInerts wis
-                 Progress new_work new_is -> do
+                   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
-                   updWorkListTcS $ extendWorkListEqs new_work
+                   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
              }
 
@@ -1508,6 +1531,27 @@ doTopReactFunEq wi fl fun_tc args xi loc
         xcomp [x] = EvCoercion (co `mkTcTransCo` evTermCoercion x)
         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 =
+  modifyInertTcS $ upd $ \fun_eqs->
+    let (wanteds, rest_funeqs) = partCtFamHeadMap (isArith Wanted) fun_eqs
+        givens = getCtFamHeadMapCts (isArith Given) rest_funeqs
+    in ((bagToList givens, bagToList wanteds), rest_funeqs)
+
+  where
+  isArith fl ct
+    | fl == ctFlavour ct
+    , Just (tc,tys) <- isCFunEqCan_maybe ct = isLinArithTyCon tc tys
+    | otherwise = False
+
+  upd f i =
+    let cans = inert_cans i
+        (a,new) = f (inert_funeqs cans)
+    in (a, i { inert_cans = cans { inert_funeqs = new } })
 \end{code}
 
 
diff --git a/compiler/typecheck/TcRnTypes.lhs b/compiler/typecheck/TcRnTypes.lhs
index 6502d6d914..6ada2c707b 100644
--- a/compiler/typecheck/TcRnTypes.lhs
+++ b/compiler/typecheck/TcRnTypes.lhs
@@ -1381,6 +1381,7 @@ data CtEvidence
     -- but if we do manage to solve it may help in solving other goals.
 
 data CtFlavour = Given | Wanted | Derived
+                  deriving Eq
 
 ctFlavour :: Ct -> CtFlavour
 ctFlavour ct = ctEvFlavour (cc_ev ct)
diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs
index 11d6a3187f..cf60921f33 100644
--- a/compiler/typecheck/TcSMonad.lhs
+++ b/compiler/typecheck/TcSMonad.lhs
@@ -79,6 +79,7 @@ module TcSMonad (
     CCanMap(..), CtTypeMap, CtFamHeadMap, CtPredMap,
     PredMap, FamHeadMap,
     partCtFamHeadMap, lookupFamHead, lookupSolvedDict,
+    getCtFamHeadMapCts,
     filterSolved,
 
     instDFunType,                              -- Instantiation
@@ -439,6 +440,10 @@ partCtFamHeadMap f (FamHeadMap ctmap)
          where 
            fam_head = funEqHead ct
 
+-- XXX: Maybe this could be more efficient?
+getCtFamHeadMapCts :: (Ct -> Bool) -> CtFamHeadMap -> Cts
+getCtFamHeadMapCts p = fst . partCtFamHeadMap p
+
 funEqHead :: Ct -> Type
 funEqHead ct = case isCFunEqCan_maybe ct of 
                  Just (tc,tys) -> mkTyConApp tc tys
diff --git a/compiler/typecheck/TcTypeNats.hs b/compiler/typecheck/TcTypeNats.hs
index cbd295008b..e4373efd1c 100644
--- a/compiler/typecheck/TcTypeNats.hs
+++ b/compiler/typecheck/TcTypeNats.hs
@@ -12,13 +12,17 @@ import Pair
 import TcType     ( TcType )
 import TyCon      ( TyCon, SynTyConRhs(..), mkSynTyCon, TyConParent(..)  )
 import Coercion   ( Role(..) )
-import TcRnTypes  ( Xi, Ct )
-import TcEvidence ( mkTcAxiomRuleCo, TcCoercion, EvTerm )
+import TcRnTypes  ( Xi, Ct(..), CtLoc, ctFlavour, ctPred, CtFlavour(..)
+                  , CtEvidence(..) )
+import TcEvidence ( mkTcAxiomRuleCo, TcCoercion, EvTerm(..) )
 import CoAxiom    ( CoAxiomRule(..) )
-import Name       ( Name, BuiltInSyntax(..) )
+import Name       ( Name, BuiltInSyntax(..), nameUnique, nameOccName )
+import OccName    ( occNameString )
+import Var        ( tyVarName, tyVarKind )
 import TysWiredIn ( typeNatKind, mkWiredInTyConName
                   , promotedBoolTyCon
                   , promotedFalseDataCon, promotedTrueDataCon
+                  , typeNatKindCon
                   )
 import TysPrim    ( tyVarList, mkArrowKinds )
 import PrelNames  ( gHC_TYPELITS
@@ -30,13 +34,20 @@ import PrelNames  ( gHC_TYPELITS
                   )
 import FamInst    ( TcBuiltInSynFamily(..) )
 import FastString ( FastString, fsLit )
+import Outputable ( ppr, panic, pprPanic )
+import UniqSet    ( foldUniqSet )
 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 )
 
 
-isLinArithTyCon :: TyCon -> Bool
-isLinArithTyCon tc = tc `elem` [ typeNatAddTyCon, typeNatMulTyCon,
-                                 typeNatLeqTyCon, typeNatSubTyCon ]
+isLinArithTyCon :: TyCon -> [Xi] -> Bool
+isLinArithTyCon tc ts =
+  tc `elem` [ typeNatAddTyCon, typeNatLeqTyCon, typeNatSubTyCon ] ||
+  (tc == typeNatMulTyCon && any (isJust . isNumLitTy) ts)
 
 
 {-------------------------------------------------------------------------------
@@ -199,7 +210,7 @@ typeNatCoAxiomRules = Map.fromList $ map (\x -> (coaxrName x, x))
   , axLeqRefl
   , axLeq0L
   , axSubDef
-  , decisionProcedure "z3"
+  , smtSolver
   ]
 
 decisionProcedure :: String -> CoAxiomRule
@@ -215,6 +226,11 @@ decisionProcedure name =
           _          -> Nothing
     }
 
+smtSolver :: CoAxiomRule
+smtSolver = decisionProcedure "smt"
+
+evBySMT :: Type -> Type -> EvTerm
+evBySMT t1 t2 = EvCoercion $ mkTcAxiomRuleCo smtSolver [t1,t2] []
 
 
 
@@ -571,9 +587,667 @@ Calling an external decision procedure
 
 data LinArithResult = SolvedWanted EvTerm
                     | IgnoreGiven
-                    | Progress [Ct] [Ct] -- new work and new inerts
+                    | 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
+  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
+                                      . showsPrec pR b
+        where
+          (pOp, pL, pR, opStr) =
+            case o of
+              Add -> (6, 6, 7, " + ")
+              Sub -> (6, 6, 7, " - ")
+              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 = undefined 
+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)
+
+--------------------------------------------------------------------------------
+
+data Result = Sat [(String, Value)]
+            | Unsat
+            | Unknown
+              deriving (Show)
+
+instance Read Result where
+  readsPrec _ xs = do ("sat", xs1) <- lex xs
+                      (vs,rest) <- readParen True getVals xs1
+                      return (Sat vs, rest)
+                ++ do ("unsat", _) <- lex xs
+                      return (Unsat, [])
+                ++ do ("unknown", _) <- lex xs
+                      return (Unknown, [])
+    where
+    getVals xs@(')' : _) = [ ([], xs) ]
+    getVals xs = do (x,cs)    <- getVal xs
+                    (rest,ds) <- getVals cs
+                    return (x : rest, ds)
+
+    getVal = readParen True $ \xs -> do (name,rest) <- lex xs
+                                        (val,rest1) <- reads rest
+                                        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")
+     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
+
+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 =
+    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" [] ]
+    ]
+
+