[commit: ghc] type-nats: A few simple interval functions. (cdedac5)

Iavor Diatchki diatchki at galois.com
Mon Mar 4 01:34:50 CET 2013


Repository : http://darcs.haskell.org/ghc.git/

On branch  : type-nats

http://hackage.haskell.org/trac/ghc/changeset/cdedac52c0bc1f19d121578e2e67ef62ed67316a

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

commit cdedac52c0bc1f19d121578e2e67ef62ed67316a
Author: Iavor S. Diatchki <iavor.diatchki at gmail.com>
Date:   Sun Mar 3 16:34:39 2013 -0800

    A few simple interval functions.

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

 compiler/typecheck/TcTypeNatsEval.hs | 30 ++++++++++++++++++++++++++++++
 1 file changed, 30 insertions(+)

diff --git a/compiler/typecheck/TcTypeNatsEval.hs b/compiler/typecheck/TcTypeNatsEval.hs
index 3bbdafb..cd6bee6 100644
--- a/compiler/typecheck/TcTypeNatsEval.hs
+++ b/compiler/typecheck/TcTypeNatsEval.hs
@@ -109,6 +109,36 @@ divide x y  = case divMod x y of
 -- | Natural numbers with a top infinity element. (No negative numbers!)
 data InfNat = Nat Integer | Infinity  deriving (Show,Eq,Ord)
 
+{- | @x + y = z at .  Compute lower bound for @z@ in terms of the lower bounds
+for @x@ and @ y at . -}
+addLower :: Integer -> Integer -> Integer
+addLower x y = x + y
+
+{- | @x + y = z at .  Compute upper bound for @z@ in terms of the upper bounds
+for @x@ and @ y at . -}
+addUpper :: InfNat -> InfNat -> InfNat
+addUpper (Nat x) (Nat y)  = Nat (x + y)
+addUpper _       _        = Infinity
+
+{- | @x * y = z at .  Compute lower bound for @z@ in terms of the lower bounds
+for @x@ and @ y at . -}
+mulLower :: Integer -> Integer -> Integer
+mulLower x y = x * y
+
+{- | @x * y = z at .  Compute upper bound for @z@ in terms of the upper bounds
+for @x@ and @ y at . -}
+mulUpper :: InfNat -> InfNat -> InfNat
+mulUpper (Nat x) (Nat y)  = Nat (x * y)
+mulUpper (Nat 0) _        = Nat 0
+mulUpper _       (Nat 0)  = Nat 0
+mulUpper _       _        = Infinity
+
+{- | @x ^ y = z at .  Compute lower bound for @z@ in terms of the lower bounds
+for @x@ and @ y at . -}
+expLower :: Integer -> Integer -> Integer
+expLower x y | x > 0 = x ^ y
+expLower x y         = 0
+
 {- | Consider @x + y = z at .  This function computes a lower bound for @x@,
 using the upper bound for @y@ and the lower bound for @z at . -}
 subLower :: Integer -> InfNat -> Integer





More information about the ghc-commits mailing list