Repository : ssh://darcs.haskell.org//srv/darcs/ghc

On branch  : type-nats

http://hackage.haskell.org/trac/ghc/changeset/4e6f3e872dd952aa6b3c1e70c74cc89af6f1ce18

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

commit 4e6f3e872dd952aa6b3c1e70c74cc89af6f1ce18
Author: Iavor S. Diatchki <iavor.diatc...@gmail.com>
Date:   Tue Dec 25 11:51:27 2012 -0800

    Add `TnExp0L` to iff rules.

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

 compiler/typecheck/TcTypeNatsRules.hs |   10 +++++-----
 1 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/compiler/typecheck/TcTypeNatsRules.hs 
b/compiler/typecheck/TcTypeNatsRules.hs
index ffde1b9..8c12d65 100644
--- a/compiler/typecheck/TcTypeNatsRules.hs
+++ b/compiler/typecheck/TcTypeNatsRules.hs
@@ -106,8 +106,6 @@ axLeqDef = mkDef 3 "LeqDef" $ \a b ->
              mkLeq (mkNumLitTy a) (mkNumLitTy b) === mkBoolLiTy (a <= b)
 
 
--- XXX: We should be able to cope with some assumptions in backward
--- reasoning too.
 bRules :: [CoAxiomRule]
 bRules =
   [ bRule 10 "Add0L" (mkAdd n0 a === a)
@@ -118,7 +116,7 @@ bRules =
   , bRule 14 "Mul1L" (mkMul n1 a === a)
   , bRule 15 "Mul1R" (mkMul a n1 === a)
 
-  -- TnExp0L:  (1 <= n) => 0 ^ n ~ 0
+  -- TnExp0L:  see iffRules
   , bRule 17 "TnExp0R" (mkExp a n0 === n1)
   , bRule 18 "TnExp1L" (mkExp n1 a === n1)
   , bRule 19 "TnExp1R" (mkExp a n1 === a)
@@ -254,11 +252,13 @@ widenRules =
 
 iffRules :: [CoAxiomRule]
 iffRules =
-  [ mkAx 65 "SubI" (take 3 natVars) [ mkAdd a b === c ] (mkSub c b === a)
+  [ mkAx 65 "SubI"    (take 3 natVars) [ mkAdd a b === c ] (mkSub c b === a)
+  , mkAx 67 "TnExp0L" (take 1 natVars) [ n1 <== a        ] (mkExp n0 a === n0)
   ]
   where
   a : b : c : _ = map mkTyVarTy natVars
-
+  n0 = mkNumLitTy 0
+  n1 = mkNumLitTy 1
 
 
 



_______________________________________________
Cvs-ghc mailing list
Cvs-ghc@haskell.org
http://www.haskell.org/mailman/listinfo/cvs-ghc

Reply via email to