[commit: ghc] decision-procedure: Checkpoint (c9f3be7)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : decision-procedure
Link       : http://ghc.haskell.org/trac/ghc/changeset/c9f3be7c1f1768dddf98d8fd3c5287b13072a920/ghc

>---------------------------------------------------------------

commit c9f3be7c1f1768dddf98d8fd3c5287b13072a920
Author: Iavor S. Diatchki <iavor.diatchki at gmail.com>
Date:   Wed Oct 16 01:19:46 2013 -0700

    Checkpoint


>---------------------------------------------------------------

c9f3be7c1f1768dddf98d8fd3c5287b13072a920
 compiler/typecheck/TcInteract.lhs |   34 +++++++++++++++++++++-------------
 compiler/typecheck/TcSMonad.lhs   |    4 ++++
 compiler/typecheck/TcTypeNats.hs  |   37 +++++++++++++++++++++++++++++++++++--
 3 files changed, 60 insertions(+), 15 deletions(-)

diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index b87c5bd..5f6da43 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -38,12 +38,14 @@ import TcEvidence
 import Outputable
 
 import TcMType ( zonkTcPredType )
+import TcTypeNats(isLinArithTyCon,decideLinArith,LinArithResult(..))
 
 import TcRnTypes
 import TcErrors
 import TcSMonad
 import Maybes( orElse )
 import Bag
+import MonadUtils(liftIO)
 
 import Control.Monad ( foldM )
 import Data.Maybe ( catMaybes, mapMaybe )
@@ -1444,7 +1446,7 @@ doTopReactDict inerts fl cls xis loc
 --------------------
 doTopReactFunEq :: Ct -> CtEvidence -> TyCon -> [Xi] -> Xi
                 -> CtLoc -> TcS TopInteractResult
-doTopReactFunEq _ct fl fun_tc args xi loc
+doTopReactFunEq wi fl fun_tc args xi loc
   = ASSERT(isSynFamilyTyCon fun_tc) -- No associated data families have
                                      -- reached this far 
     -- Look in the cache of solved funeqs
@@ -1470,18 +1472,24 @@ doTopReactFunEq _ct fl fun_tc args xi loc
   where
     fam_ty = mkTyConApp fun_tc args
 
-    try_improve_and_return =
-      do { case isBuiltInSynFamTyCon_maybe fun_tc of
-             Just ops ->
-               do { let eqns = sfInteractTop ops args xi
-                  ; impsMb <- mapM (\(Pair x y) -> newDerived (mkTcEqPred x y))
-                                   eqns
-                  ; let work = map (mkNonCanonical loc) (catMaybes impsMb)
-                  ; unless (null work) (updWorkListTcS (extendWorkListEqs work))
-                  }
-             _ -> return ()
-         ; return NoTopInt
-         }
+    try_improve_and_return
+       | isLinArithTyCon fun_tc =
+          do { (gis,wis) <- undefined -- getRelevantLinArithInerts
+             ; res <- liftIO $ decideLinArith gis wis wi
+             ; let addInerts = mapM_ insertInertItemTcS
+             ; case res of
+                 SolvedWanted ev -> do
+                   addInerts wis
+                   setEvBind (ctEvId $ ctEvidence wi) ev
+                 IgnoreGiven -> do
+                   addInerts wis
+                 Progress new_work new_is -> do
+                   addInerts new_is
+                   updWorkListTcS $ extendWorkListEqs new_work
+             ; return $ SomeTopInt "LinArith" Stop
+             }
+
+       | otherwise = return NoTopInt
 
     succeed_with :: String -> TcCoercion -> TcType -> TcS TopInteractResult
     succeed_with str co rhs_ty    -- co :: fun_tc args ~ rhs_ty
diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs
index f8c5e04..11d6a31 100644
--- a/compiler/typecheck/TcSMonad.lhs
+++ b/compiler/typecheck/TcSMonad.lhs
@@ -996,6 +996,10 @@ instance Monad TcS where
   fail err  = TcS (\_ -> fail err) 
   m >>= k   = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
 
+-- Currently, this is just used to call an external decision procedure
+instance MonadIO TcS where
+  liftIO m = TcS (\_ -> liftIO m)
+
 -- Basic functionality 
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 wrapTcS :: TcM a -> TcS a 
diff --git a/compiler/typecheck/TcTypeNats.hs b/compiler/typecheck/TcTypeNats.hs
index d11a8e0..cbd2950 100644
--- a/compiler/typecheck/TcTypeNats.hs
+++ b/compiler/typecheck/TcTypeNats.hs
@@ -2,6 +2,9 @@ module TcTypeNats
   ( typeNatTyCons
   , typeNatCoAxiomRules
   , TcBuiltInSynFamily(..)
+  , LinArithResult(..)
+  , decideLinArith
+  , isLinArithTyCon
   ) where
 
 import Type
@@ -9,8 +12,8 @@ import Pair
 import TcType     ( TcType )
 import TyCon      ( TyCon, SynTyConRhs(..), mkSynTyCon, TyConParent(..)  )
 import Coercion   ( Role(..) )
-import TcRnTypes  ( Xi )
-import TcEvidence ( mkTcAxiomRuleCo, TcCoercion )
+import TcRnTypes  ( Xi, Ct )
+import TcEvidence ( mkTcAxiomRuleCo, TcCoercion, EvTerm )
 import CoAxiom    ( CoAxiomRule(..) )
 import Name       ( Name, BuiltInSyntax(..) )
 import TysWiredIn ( typeNatKind, mkWiredInTyConName
@@ -30,6 +33,12 @@ import FastString ( FastString, fsLit )
 import qualified Data.Map as Map
 import Data.Maybe ( isJust )
 
+
+isLinArithTyCon :: TyCon -> Bool
+isLinArithTyCon tc = tc `elem` [ typeNatAddTyCon, typeNatMulTyCon,
+                                 typeNatLeqTyCon, typeNatSubTyCon ]
+
+
 {-------------------------------------------------------------------------------
 Built-in type constructors for functions on type-lelve nats
 -}
@@ -190,8 +199,24 @@ typeNatCoAxiomRules = Map.fromList $ map (\x -> (coaxrName x, x))
   , axLeqRefl
   , axLeq0L
   , axSubDef
+  , decisionProcedure "z3"
   ]
 
+decisionProcedure :: String -> CoAxiomRule
+decisionProcedure name =
+  CoAxiomRule
+    { coaxrName      = fsLit name
+    , coaxrTypeArity = 2
+    , coaxrAsmpRoles = []
+    , coaxrRole      = Nominal
+    , coaxrProves    = \ts cs ->
+        case (ts,cs) of
+          ([s,t],[]) -> return (s === t)
+          _          -> Nothing
+    }
+
+
+
 
 
 {-------------------------------------------------------------------------------
@@ -540,7 +565,15 @@ genLog x base = Just (exactLoop 0 x)
 
 
 
+{- -----------------------------------------------------------------------------
+Calling an external decision procedure
+----------------------------------------------------------------------------- -}
 
+data LinArithResult = SolvedWanted EvTerm
+                    | IgnoreGiven
+                    | Progress [Ct] [Ct] -- new work and new inerts
 
+decideLinArith :: [Ct] -> [Ct] -> Ct -> IO LinArithResult
+decideLinArith = undefined