Commit c4320ca0 authored by Yiannis Tsiouris's avatar Yiannis Tsiouris

Add types to Credit module and export

parent 37a60823
--
-- orbit-int credits (for checking termination of orbit computation)
--
module Credit( credit
module Credit( -- Types
ACredit
, Credit
-- Functions
, credit
, credit_atomic
, debit_atomic
, debit_atomic_nz
......@@ -20,9 +24,11 @@ module Credit( credit
-- represented by the empty list. The maximally possible credit, 1,
-- is represented by [0].
type ACredit = Int
type Credit = [ACredit]
-- credit_atomic(K, C) adds the atomic credit 1/{2^K} to the credit C.
credit_atomic :: Int -> [Int] -> [Int]
credit_atomic :: Int -> Credit -> Credit
credit_atomic k [] = [k]
credit_atomic k (c : cs) | k > c = k : c : cs
| k == c = credit_atomic (k - 1) cs
......@@ -30,7 +36,7 @@ credit_atomic k (c : cs) | k > c = k : c : cs
-- credit(C1, C2) returns a list representing the sum of the credit
-- represented by the lists C1 and C2.
credit :: [Int] -> [Int] -> [Int]
credit :: Credit -> Credit -> Credit
credit c1 c2 = foldl (flip credit_atomic) c2 c1
-- debit_atomic(C) returns a pair {K',C'} where K' is an integer
......@@ -38,7 +44,7 @@ credit c1 c2 = foldl (flip credit_atomic) c2 c1
-- some credit (which may be zero) such that the sum of the credits
-- represented by K' and C' equals the credit represented by C.
-- Precondition: C must represent non-zero credit.
debit_atomic :: [Int] -> (Int, [Int])
debit_atomic :: Credit -> (ACredit, Credit)
debit_atomic (c : cs) = (c, cs) -- debit smallest unit of credit
-- debit_atomic_nz(C) returns a pair {K',C'} where K' is an integer
......@@ -46,25 +52,25 @@ debit_atomic (c : cs) = (c, cs) -- debit smallest unit of credit
-- some non-zero credit such that the sum of the credits
-- represented by K' and C' equals the credit represented by C.
-- Precondition: C must represent non-zero credit.
debit_atomic_nz :: [Int] -> (Int, [Int])
debit_atomic_nz :: Credit -> (ACredit, Credit)
debit_atomic_nz [c] = (c + 1, [c + 1]) -- debit half the credit
debit_atomic_nz (c : cs) = (c, cs) -- debit smallest unit of credit;
-- case only applies if Cs non-empty
-- zero/0 produces zero credit.
zero :: [Int]
zero :: Credit
zero = []
-- one/0 produces credit one.
one :: [Int]
one :: Credit
one = [0]
-- is_zero/1 tests whether its argument represents zero credit.
is_zero :: [Int] -> Bool
is_zero :: Credit -> Bool
is_zero [] = True
is_zero _ = False
-- is_one/1 tests whether its argument represents maximal credit 1.
is_one :: [Int] -> Bool
is_one :: Credit -> Bool
is_one [0] = True
is_one _ = False
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment