[commit: ghc] wip/ext-solver: Evidence for proofs generate by external solver (fefcfc8)

[git at git.haskell.org]

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

On branch  : wip/ext-solver
Link       : http://ghc.haskell.org/trac/ghc/changeset/fefcfc8fa9f3c522012d2147510e3f7381fd3b95/ghc

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

commit fefcfc8fa9f3c522012d2147510e3f7381fd3b95
Author: Iavor S. Diatchki <iavor.diatchki at gmail.com>
Date:   Mon Apr 28 23:29:25 2014 -0700

    Evidence for proofs generate by external solver


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

fefcfc8fa9f3c522012d2147510e3f7381fd3b95
 compiler/typecheck/TcTypeNats.hs |   24 ++++++++++++++++++++++--
 1 file changed, 22 insertions(+), 2 deletions(-)

diff --git a/compiler/typecheck/TcTypeNats.hs b/compiler/typecheck/TcTypeNats.hs
index 63d101f..66894a1 100644
--- a/compiler/typecheck/TcTypeNats.hs
+++ b/compiler/typecheck/TcTypeNats.hs
@@ -3,11 +3,13 @@ module TcTypeNats
   , typeNatCoAxiomRules
   , BuiltInSynFamily(..)
   , ExternalSolver(..), ExtSolRes(..), newExternalSolver
+  , evBySMT
   ) where
 
 import Type
 import Pair
 import TcType     ( TcType, tcEqType )
+import TcEvidence ( mkTcAxiomRuleCo, EvTerm(..) )
 import TyCon      ( TyCon, SynTyConRhs(..), mkSynTyCon, TyConParent(..)  )
 import Coercion   ( Role(..) )
 import TcRnTypes  ( Xi, Ct(..) )
@@ -288,9 +290,27 @@ typeNatCoAxiomRules = Map.fromList $ map (\x -> (coaxrName x, x))
   ]
 
 
+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
+    }
 
-{-------------------------------------------------------------------------------
-Various utilities for making axioms and types
+
+evBySMT :: String -> (Type, Type) -> EvTerm
+evBySMT name (t1,t2) =
+  EvCoercion $ mkTcAxiomRuleCo (decisionProcedure name) [t1,t2] []
+
+
+
+-- Various utilities for making axioms and types
 -------------------------------------------------------------------------------}
 
 (.+.) :: Type -> Type -> Type