fun ack m n = if m = 0 then n+1 else if n = 0 then ack (m-1) 1 else ack (m-1) (ack m (n-1)) withtype {i:nat,j:nat} => int(i) -> int(j) -> [k:nat] int(k) fun loop (j, k) = if (k < j) then if (k > 1) then loop (j - k, k / 2) else 0 else j + k withtype {a:nat,b:pos} => int(a) * int(b) -> int datatype Nat with nat = Z(0) | {n:nat} S(n+1) of Nat(n) fun('a) R Z u v = u | R (S n) u v = v n (R n u v) withtype {n:nat} => Nat(n) -> 'a -> (Nat -> 'a -> 'a) -> 'a fun f91 (x) = if (x <= 100) then f91 (f91 (x + 11)) else x - 10 withtype {i:int} => int(i) -> [j:int | (i<=100 /\ j=91) \/ (i>=101 /\ j=i-10)] int(j) fun('a) qs cmp xs = case xs of [] => [] | x :: xs' => par cmp (x, [], [], xs') withtype ('a * 'a -> bool) -> {n:nat} => 'a list(n) -> 'a list(n) and('a) par cmp (x, l, r, xs) = case xs of [] => qs cmp l @ (x :: qs cmp r) | x' :: xs' => if cmp(x', x) then par cmp (x, x' :: l, r, xs') else par cmp (x, l, x' :: r, xs') withtype ('a * 'a -> bool) -> {p:nat,q:nat,r:nat} => 'a * 'a list(p) * 'a list(q) * 'a list(r) -> 'a list(p+q+r+1) datatype pattern with nat = Empty(0) (* empty string matches Empty *) | Char(1) of char (* "c" matches Char (c) *) | {i:nat,j:nat} Plus(i+j+1) of pattern(i) * pattern(j) (* cs matches Plus(p1, p2) if cs matches either p1 or p2 *) | {i:nat,j:nat} Times(i+j+1) of pattern(i) * pattern(j) (* cs matches Times(p1, p2) if a prefix of cs matches p1 and the rest matches p2 *) | {i:nat} Star(i+1) of pattern(i) (* cs matches Star(p) if cs matches some, possibly 0, copies of p *) (* 'length' computes the length of a list *) fun('a) length (xs) = let fun len ([], n) = n | len (x :: xs, n) = len (xs, n+1) withtype {i:nat,j:nat} => 'a list(i) * int(j) -> int(i+j) in len (xs, 0) end withtype {i:nat} <> => 'a list(i) -> int(i) fun acc p cs k = case p of Empty => k (cs) | Char(c) => (case cs of [] => false | c' :: cs' => if char_eq (c, c') then k (cs') else false) | Plus(p1, p2) => if acc p1 cs k then true else acc p2 cs k | Times(p1, p2) => acc p1 cs (fn cs' => acc p2 cs' k) | Star(p0) => if k (cs) then true else acc p0 cs (fn cs' => if length(cs') = length(cs) then false else acc p cs' k) withtype {n:nat} pattern(n) -> {i:nat} => char list(i) -> ({i':nat | i' <= i} char list(i') -> bool) -> bool (* 'explode' turns a string into a list of characters *) fun accept p s = acc p (explode s) (fn [] => true | _ :: _ => false) withtype <> => pattern -> string -> bool (* * 'a llist(i, n): a list of lists such that * 1. the sum of the lengths of lists in the list of lists is i, and * 2. the length of the list is n. *) datatype 'a llist with (nat, nat) = lnil(0,0) | {i:nat, j:nat, n:nat} lcons (i+j, n+1) of 'a list(i) * 'a llist (j, n) fun merge ([], ys) = ys | merge (xs, []) = xs | merge (xs as x :: xs', ys as y :: ys') = if x < y then x :: merge (xs', ys) else y :: merge (xs, ys') withtype {i:nat,j:nat} => int list(i) * int list(j) -> int list(i+j) fun initList [] = lnil | initList (l as [x]) = lcons (l, lnil) | initList (x1 :: x2 :: xs) = let val l = (if x1 < x2 then [x1, x2] else [x2, x1]: int list(2)) in lcons (l, initList xs) end withtype {i:nat} => int list(i) -> [n:nat] int llist(i, n) fun mergeList (ls as lnil) = ls | mergeList (ls as lcons (_, lnil)) = ls | mergeList (lcons (l1, lcons (l2, ls))) = lcons (merge (l1, l2), mergeList ls) withtype {i:nat,n:nat} => int llist(i,n) -> [n':nat | (n' < n /\ 2 <= n) \/ (n' = n /\ n < 2)] int llist (i, n') fun mergeAll lnil = [] | mergeAll (lcons (l, lnil)) = l | mergeAll (ls as lcons (_, lcons (_, _))) = mergeAll (mergeList ls) withtype {i:nat,n:nat} => int llist(i,n) -> int list(i) fun mergeSort l = mergeAll (initList l) withtype {i:nat} <> => int list(i) -> int list(i) (* * 'a list(n) is the type for lists of length n * [] is assigned the type 'a list(0) * op:: is assigned the type {n:nat} 'a * 'a list(n) -> 'a list(n+1) *) fun f [] k = k [] | f (c :: cs) k = (* note that #"c" represents a constant character c *) if char_eq (c, #"(") then f cs (fn cs' => (f cs' k) + 1) else if char_eq (c, #")") then k (cs) - 1 else ~1 withtype {n:nat} => char list(n) -> ({n':nat | n' <= n} char list(n') -> int) -> int