Repository : ssh://darcs.haskell.org//srv/darcs/ghc On branch : type-nats
http://hackage.haskell.org/trac/ghc/changeset/cd229c2f1ee7382269ef3eafb446ab39cd763402 >--------------------------------------------------------------- commit cd229c2f1ee7382269ef3eafb446ab39cd763402 Author: Iavor S. Diatchki <[email protected]> Date: Sun Jul 15 12:30:33 2012 -0700 Some comments on `ActiveRule`s. >--------------------------------------------------------------- compiler/typecheck/TcTypeNats.hs | 23 +++++++++++++---------- 1 files changed, 13 insertions(+), 10 deletions(-) diff --git a/compiler/typecheck/TcTypeNats.hs b/compiler/typecheck/TcTypeNats.hs index c8087d7..c70b9e9 100644 --- a/compiler/typecheck/TcTypeNats.hs +++ b/compiler/typecheck/TcTypeNats.hs @@ -344,20 +344,23 @@ solveWithAxiom _ = Nothing -- An `ActiveRule` is a partially constructed proof for some predicate. data ActiveRule = AR { isSym :: Bool -- See Note [Symmetric Rules] - , proof :: [Type] -> [EvTerm] -> EvTerm + + -- This is the instantiation of the rule. , doneTys :: [TypePat] + + -- These are equations that we already solved, and are ready to be used. + -- The `Int` records the position of the evidence when the rule fires. , doneArgs :: [(Int,EvTerm)] + -- These are equations that we need to solve before the rule can fire. + -- The `Int` records the position of the evidence when the rule fires. , todoArgs :: [(Int,(TypePat,TypePat))] - {- todoArgs == - [ (n, (cvt t1, cvt t2)) - | (n,(t1,t2)) <- zip [ 0 .. ] (co_axr_asmps axRule) - , n `notElem` map fst doneArgs - , let cvt = apSimpSubst doneArgs . toTypePat (co_axr_tvs axRule) - ] - -} - - , concl :: (TypePat,TypePat) + + -- This is what we'll prove when the rule fires. + , concl :: (TypePat,TypePat) + + -- This is the evidence we'll use when the rule fires. + , proof :: [Type] -> [EvTerm] -> EvTerm } {- Note [Symmetric Rules] _______________________________________________ Cvs-ghc mailing list [email protected] http://www.haskell.org/mailman/listinfo/cvs-ghc
