/**
* Integer arithmetic and comparison.
*/
module term/integer
imports
lang/dynamic-rules
strategies
is-int =
?i; prim("SSL_is_int", i)
strategies
/**
* Adds two numbers (integer or real)
*/
add = ?(x,y); (prim("SSL_addi",x,y) <+ prim("SSL_addr",x,y))
/**
* Adds two integers
*/
addi = ?(x,y); prim("SSL_addi",x,y)
/**
* Adds two integers
*/
int-add(|y) =
?x; prim("SSL_addi", x, y)
/**
* Adds two reals
*/
addr = ?(x,y); prim("SSL_addr",x,y)
strategies
/**
* Subtracts two numbers (integer or real)
*/
subt = ?(x,y); (prim("SSL_subti",x,y) <+ prim("SSL_subtr",x,y))
/**
* Subtracts two integers
*/
subti = ?(x,y); prim("SSL_subti",x,y)
/**
* Subtracts two integers
*/
int-subt(|y) =
?x; prim("SSL_subti", x, y)
/**
* Subtracts two reals
*/
subtr = ?(x,y); prim("SSL_subtr",x,y)
strategies
/**
* Multiplies two numbers (integer or real)
*/
mul = ?(x,y); (prim("SSL_muli",x,y) <+ prim("SSL_mulr",x,y))
/**
* Multiplies two integers
*/
muli = ?(x,y); prim("SSL_muli",x,y)
/**
* Multiplies two reals
*/
mulr = ?(x,y); prim("SSL_mulr",x,y)
strategies
/**
* Divides two numbers (integer or real)
*/
div = ?(x,y); (prim("SSL_divi",x,y) <+ prim("SSL_divr",x,y))
/**
* Divides two integers
*/
divi = ?(x,y); prim("SSL_divi",x,y)
/**
* Divides two reals
*/
divr = ?(x,y); prim("SSL_divr",x,y)
strategies
/**
* Returns the modulo (remainder after division) of two integers or reals.
*/
mod =
modi <+ modr
/**
* Returns the modulo (remainder after division) of two integers
*/
modi =
?(x,y); prim("SSL_modi",x,y)
/**
* Returns the modulo (remainder after division) of two floats
*/
modr =
?(x,y); prim("SSL_modr",x,y)
strategies
gt = ?(x,y); test(prim("SSL_gti",x,y) <+ prim("SSL_gtr",x,y))
gti = ?(x,y); test(prim("SSL_gti",x,y))
gtr = ?(x,y); test(prim("SSL_gtr",x,y))
geq = ?(x,x) <+ gt
lt = not(geq)
leq = not(gt)
strategies
/**
* @type Int -> Int
*/
int-leq(|y) =
not(int-gt(|y))
/**
* @type Int -> Int
*/
int-gt(|y) =
?x; where(prim("SSL_gti",x,y))
/**
* @type Int -> Int
*/
int-lt(|y) =
?x; where(prim("SSL_lti", x, y))
strategies
// :: Int * Int * Int -> fail?
leq-leq = comp-comp(leq, leq)
leq-lt = comp-comp(leq, lt)
lt-leq = comp-comp(lt, leq)
lt-lt = comp-comp(lt, lt)
// Int * Int -> fail?, Int * Int -> fail? :: Int * Int * Int -> fail?
comp-comp(s1, s2) =
?(x, y, z)
; where(<s1> (x, y); <s2> (y, z))
strategies
/**
* @type Int -> fail?
*/
even = where(<mod> (<id>, 2) => 0)
/**
* @type (Int, Int) -> Int
*/
max = gt < Fst + Snd
min = gt < Snd + Fst
/**
* @type Int -> Int
*/
pos = where(<geq> (<id>, 0))
neg = where(<lt> (<id>, 0))
int = ?x; prim("SSL_int",x)
strategies
/**
* Sets a seed for the following sequence of next-random calls.
* Typically, the seed is set to the Unix time (the result of the strategy time).
*
* @see man srand
* @since 0.9.4
* @type Int -> ()
*/
set-random-seed = ?seed; prim("SSL_srand", seed)
/**
* Gets the maximum random number that will be returned by the next-random number generator.
* Corresponds to RAND_MAX in C.
*
* @type _ -> Int()
*/
get-random-max = prim("SSL_RAND_MAX")
/**
* Returns a random number between 0 and get-random-max.
*
* For a given seed, this strategy always returns the same sequence of numbers.
* If no seed value has been set using set-random-seed, then the seed is 1, which
* means that the sequence of random numbers will always be the same if you set no seed.
*
* @see man rand
* @since 0.9.4
* @type _ -> Int
*/
next-random = prim("SSL_rand")
strategies
apply-int-to-str-tuple(s) =
(string-to-int, string-to-int) ; s ; int-to-string
addS = apply-int-to-str-tuple(add)
subtS = apply-int-to-str-tuple(subt)
mulS = apply-int-to-str-tuple(mul)
divS = apply-int-to-str-tuple(div)
modS = apply-int-to-str-tuple(mod)
maxS = apply-int-to-str-tuple(max)
minS = apply-int-to-str-tuple(min)
gtS = where((string-to-int, string-to-int); gt)
geqS = where((string-to-int, string-to-int); geq)
ltS = where((string-to-int, string-to-int); lt)
leqS = where((string-to-int, string-to-int); leq)
/**
* Increments a number.
*
* @type Int -> Int
*/
inc = <add> (<id>, 1)
/**
* Increments an integer
*
* @type Int -> Int
*/
int-inc =
int-add(|1)
/**
* Decrements a number.
*
* @type Int -> Int
*/
dec = <subt> (<id>, 1)
/**
* Decrements an integer.
*
* @type Int -> Int
*/
int-dec =
int-subt(|1)
strategies
log2 =
!(<id>, 0);
repeat((!(<divi>(<id>, 2), <mod; ?0>(<id>, 2)); Fst, inc));
?(1, <id>)
strategies
gcd =
(abs,abs)
; let gcd' = \ (x,0) -> x \ + \ (x,y) -> <gcd'>(y,<mod>(x,y)) \
in
gcd'
end
abs =
(is-int + is-real)
; if neg then
<subt> (0, <id>)
end
signature
constructors
Infinite : IntI
: Int -> IntI
rules
add-inf =
let add-inf1: (Infinite(), _) -> Infinite()
add-inf2: (_, Infinite()) -> Infinite()
in (add-inf1 + add-inf2) <+ add
end
lt-inf = ?(<is-int>, Infinite()) <+ (is-int, is-int); lt
strategies
new-counter =
new; reset-counter
reset-counter = ?c;
where(<set-counter> (c, 0))
set-counter =
?(c,n); rules( Counter : c -> n )
get-counter =
Counter <+ <set-counter> (<id>, 0); !0
next-counter =
?c; get-counter; inc; where(<set-counter> (c, <id>))
strategies
int-to-string = ?x; prim("SSL_int_to_string",x)
string-to-int = ?x; prim("SSL_string_to_int",x)
/**
* Conversion of strings to integers
*/
strategies
/**
* @type String -> Int
* @inc hex-string-test
*/
hex-string-to-int = <generic-string-to-int> (<id>, 16)
/**
* @type String -> Int
* @inc dec-string-test
*/
dec-string-to-int = <generic-string-to-int> (<id>, 10)
oct-string-to-int = <generic-string-to-int> (<id>, 8)
/**
* @type String -> Int
* @inc bin-string-test
*/
bin-string-to-int = <generic-string-to-int> (<id>, 2)
/**
* @type List(Char) -> Int
*/
hex-chars-to-int = <generic-chars-to-int> (<id>, 16)
/**
* @type List(Char) -> Int
*/
dec-chars-to-int = <generic-chars-to-int> (<id>, 10)
/**
* @type List(Char) -> Int
*/
oct-chars-to-int = <generic-chars-to-int> (<id>, 8)
/**
* @type List(Char) -> Int
*/
bin-chars-to-int = <generic-chars-to-int> (<id>, 2)
/**
* @type String * Int -> Int
*/
generic-string-to-int =
(explode-string, id)
; generic-chars-to-int
/**
* @type List(Char) * Int -> Int
*/
generic-chars-to-int =
neg-chars-to-int <+ pos-chars-to-int
// :: List(Char) * Int -> Int
neg-chars-to-int:
(['-' | chars], radix) -> <mul> (-1, <pos-chars-to-int> (chars, radix))
where <gt> (<length> chars, 0)
// :: List(Char) * Int -> Int
pos-chars-to-int =
?([char | chars], r)
; <foldl(<add> (<char-to-digit> (<Fst>, r), <mul> (<Snd>, r)))>
(chars, <char-to-digit> (char, r))
// :: Char -> Int
char-to-digit:
(x, radix) -> result
where <is-num> x
; <subt> (x, '0') => result
; <lt> (result, radix)
char-to-digit:
(x, 16) -> <add> (10, <subt> (x, 'a'))
where <leq-leq> ('a', x, 'f')
char-to-digit:
(x, 16) -> <add> (10, <subt> (x, 'A'))
where <leq-leq> ('A', x, 'F')