[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