[commit: ghc] type-nats: A bit more integration for reasoning about order. (81609b6)
Iavor Diatchki
diatchki at galois.com
Tue Sep 4 07:48:49 CEST 2012
Repository : ssh://darcs.haskell.org//srv/darcs/ghc
On branch : type-nats
http://hackage.haskell.org/trac/ghc/changeset/81609b630c719b85a5b0de127d431ae5a0029174
>---------------------------------------------------------------
commit 81609b630c719b85a5b0de127d431ae5a0029174
Author: Iavor S. Diatchki <iavor.diatchki at gmail.com>
Date: Mon Sep 3 22:48:42 2012 -0700
A bit more integration for reasoning about order.
>---------------------------------------------------------------
compiler/typecheck/TcTypeNats.hs | 62 +++++++++++++++++++++++++--------
compiler/typecheck/TcTypeNatsRules.hs | 5 ---
2 files changed, 47 insertions(+), 20 deletions(-)
diff --git a/compiler/typecheck/TcTypeNats.hs b/compiler/typecheck/TcTypeNats.hs
index fc0fc7c..d8bf9e7 100644
--- a/compiler/typecheck/TcTypeNats.hs
+++ b/compiler/typecheck/TcTypeNats.hs
@@ -24,7 +24,6 @@ import Type ( Type, isNumLitTy, getTyVar_maybe, isTyVarTy, mkNumLitTy
import TysWiredIn ( typeNatAddTyCon
, typeNatMulTyCon
, typeNatExpTyCon
- -- , typeNatLeqTyCon
, trueTy, falseTy
)
import Bag ( bagToList )
@@ -66,7 +65,7 @@ import TcSMonad ( TcS, emitFrozenError, setEvBind
import Data.Maybe ( isNothing, mapMaybe )
import Data.List ( sortBy, partition, find )
import Data.Ord ( comparing )
-import Control.Monad ( msum, guard, when, mplus )
+import Control.Monad ( msum, guard, when )
import qualified Data.Set as S
import qualified Data.Map as M
@@ -162,10 +161,14 @@ this happened automatically because of the custom system for reasoning
about <=.
-}
deepSolve :: [Ct] -> Ct -> Maybe EvTerm
-deepSolve asmps ct = solve ct `mplus` fmap ev (find this (widenAsmps asmps))
+deepSolve asmps0 ct = msum [ solve ct
+ , solveLeq leq ct
+ , fmap ev (find this (widenAsmps asmps))
+ ]
where
ev = ctEvTerm . ctEvidence
this = sameCt ct
+ (leq,asmps) = makeLeqModel asmps0
impossible :: Ct -> Bool
@@ -410,6 +413,14 @@ solveWithAxiom (CFunEqCan { cc_fun = tc, cc_tyargs = ts, cc_rhs = t }) =
return ev
solveWithAxiom _ = Nothing
+solveLeq :: LeqFacts -> Ct -> Maybe EvTerm
+solveLeq m ct =
+ do (t1,t2) <- isLeqCt ct
+ let (_,m1) = leqInsNode t1 m
+ (_,m2) = leqInsNode t2 m1
+ leqReachable m2 t1 t2
+
+
--------------------------------------------------------------------------------
-- An `ActiveRule` is a partially constructed proof for some predicate.
@@ -706,6 +717,7 @@ getFacts =
return $ bagToList $ fst $ partCtFamHeadMap isGivenCt
$ inert_funeqs $ inert_cans is
+-- Get constraints with evidence (given or wanted)
getEvCt:: TcS [Ct]
getEvCt =
do is <- getTcSInerts
@@ -713,6 +725,7 @@ getEvCt =
$ inert_funeqs $ inert_cans is
where hasEv c = isGivenCt c || isWantedCt c
+-- Get all constraints (given, wanted, derived)
getAllCts :: TcS [Ct]
getAllCts =
do is <- getTcSInerts
@@ -740,6 +753,7 @@ interactCt withEv ct asmps =
: funRule typeNatExpTyCon
: map activate (widen ++ impRules)
+ -- (leq, asmps) = makeLeqModel asmps0
newWork = interactActiveRules active asmps
in partition isBad $ if withEv then map ruleResultToGiven newWork
else map ruleResultToDerived newWork
@@ -869,6 +883,8 @@ leqReachable m smaller larger =
in search vis (notDone new `S.union` notDone rest)
{-
+The linking function is a bit complex because we keep the ordering database
+minimal.
This diagram illustrates what we do when we link two nodes (leqLink).
@@ -898,10 +914,12 @@ leqLink :: EvTerm -> (Type,LeqEdges) -> (Type,LeqEdges) ->
leqLink ev (lower, ledges) (upper, uedges) m0 =
- let uus = S.mapMonotonic (LeqType . leqTarget) (leqAbove uedges)
- lls = S.mapMonotonic (LeqType . leqTarget) (leqBelow ledges)
+ let leqTgt = LeqType . leqTarget
- rm x = S.filter (not . (`S.member` x) . LeqType . leqTarget)
+ uus = S.mapMonotonic leqTgt (leqAbove uedges)
+ lls = S.mapMonotonic leqTgt (leqBelow ledges)
+
+ rm x = S.filter (not . (`S.member` x) . leqTgt)
newLedges = ledges { leqAbove =
S.insert (LeqEdge { leqProof = ev
@@ -989,13 +1007,6 @@ leqInsNode t model@(LeqFacts m0) =
_ <- isNumLitTy n
return (n,(n,e))
--- | Try to find a proof that the first term is smaller then the second.
-leqProve :: LeqFacts -> Type -> Type -> Maybe EvTerm
-leqProve model s t =
- let (_,m1) = leqInsNode s model
- (_,m2) = leqInsNode t m1
- in leqReachable m2 s t
-
-- | The result of trying to extend a collection of facts with a new one.
data AddLeqFact
@@ -1024,8 +1035,28 @@ addFact ev t1 t2 m0 =
but propose an equality instead. -}
Just pOp -> LeqImproved (useAxiom leqAsym [t1,t2] [ev, pOp])
-
-
+-- | Construct an ordering model and return the remaining, not-leq constraints.
+makeLeqModel :: [Ct] -> (LeqFacts,[Ct])
+makeLeqModel = foldr add (noLeqFacts,[])
+ where
+ add ct (m,rest)
+ | Just (t1,t2) <- isLeqCt ct
+ , Just ev <- ctEvTermMaybe ct
+ , LeqAdded m1 <- addFact ev t1 t2 m = (m1, rest)
+ add ct (m,rest) = (m, ct : rest)
+
+-- | Is this an `a <= b` constraint?
+isLeqCt :: Ct -> Maybe (Type, Type)
+isLeqCt (CFunEqCan { cc_fun = tc, cc_tyargs = [t1,t2], cc_rhs = t })
+ | tyConName tc == typeNatLeqTyFamName && eqType t trueTy = Just (t1,t2)
+isLeqCt _ = Nothing
+
+-- | Get the evidence associated with a constraint, if any.
+ctEvTermMaybe :: Ct -> Maybe EvTerm
+ctEvTermMaybe ct =
+ do let ev = ctEvidence ct
+ guard $ not $ isDerived ev
+ return (ctEvTerm ev)
--------------------------------------------------------------------------------
@@ -1033,3 +1064,4 @@ addFact ev t1 t2 m0 =
natTrace :: String -> SDoc -> TcS ()
natTrace x y = traceTcS ("[NATS] " ++ x) y
+
diff --git a/compiler/typecheck/TcTypeNatsRules.hs b/compiler/typecheck/TcTypeNatsRules.hs
index 2ad2446..fd50862 100644
--- a/compiler/typecheck/TcTypeNatsRules.hs
+++ b/compiler/typecheck/TcTypeNatsRules.hs
@@ -108,9 +108,6 @@ bRules =
, bRule 17 "TnExp0R" (mkExp a n0 === n1)
, bRule 18 "TnExp1L" (mkExp n1 a === n1)
, bRule 19 "TnExp1R" (mkExp a n1 === a)
-
- , leq0
- , leqRefl
]
where
bRule s n = mkAx s n (take 1 natVars) []
@@ -174,8 +171,6 @@ widenRules =
, (True, mkAx 41 "MulComm" (take 3 natVars)
[ mkMul a b === c ] (mkMul b a === c))
- , (False, leqTrans)
-
, (False, mkAx 43 "AddAssoc1" (take 6 natVars)
[ mkAdd a b === x, mkAdd b c === y, mkAdd a y === z ] (mkAdd x c === z))
More information about the Cvs-ghc
mailing list