/** * 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')