[commit: ghc] type-nats: Some simple rules about interactions between computation and ordering. (9df3de5)

[Iavor Diatchki]

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

On branch  : type-nats

http://hackage.haskell.org/trac/ghc/changeset/9df3de5f5566735e175d64e193f3c46cf95d2ff1

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

commit 9df3de5f5566735e175d64e193f3c46cf95d2ff1
Author: Iavor S. Diatchki <iavor.diatchki at gmail.com>
Date:   Tue Sep 11 14:54:14 2012 -0700

    Some simple rules about interactions between computation and ordering.

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

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

diff --git a/compiler/typecheck/TcTypeNatsRules.hs b/compiler/typecheck/TcTypeNatsRules.hs
index fd50862..8f82b50 100644
--- a/compiler/typecheck/TcTypeNatsRules.hs
+++ b/compiler/typecheck/TcTypeNatsRules.hs
@@ -183,9 +183,32 @@ widenRules =
   , (False, mkAx 46 "MulAssoc2" (take 6 natVars)
       [ mkMul a b === x, mkMul b c === y, mkMul x c === z ] (mkMul a y === z))
 
+
+  -- XXX: Some simple interactions between operators and ordering.
+  -- A proper interval analysis would do better.
+  , (True, mkAx 50 "LeqAdd1" (take 3 natVars)
+      [ mkAdd a b === c ] (a <== c))
+
+  , (True, mkAx 51 "LeqAdd2" (take 3 natVars)
+      [ mkAdd a b === c ] (b <== c))
+
+  , (True, mkAx 52 "LeqMul1" (take 3 natVars)
+      [ n1 <== b, mkMul a b === c ] (a <== c))
+
+  , (True, mkAx 53 "LeqMul2" (take 3 natVars)
+      [ n1 <== a, mkMul a b === c ] (b <== c))
+
+  , (True, mkAx 54 "LeqExp1" (take 3 natVars)
+      [ n1 <== b, mkExp a b === c ] (a <== c))
+
+  , (True, mkAx 54 "LeqExp2" (take 3 natVars)
+      [ n2 <== a, mkExp a b === c ] (b <== c))
+
   ]
   where
   a : b : c : x : y : z : _ = map mkTyVarTy natVars
+  n1 = mkNumLitTy 1
+  n2 = mkNumLitTy 2