doc-src/Codegen/Thy/examples/example.ML
author blanchet
Wed, 13 Jul 2011 22:16:19 +0200
changeset 43811 402e1a0d93d9
parent 38460 628fee3eb449
child 48863 881e8a96e617
permissions -rw-r--r--
better temp name creation for Nitrox -- still very hackish though, but should get us through CASC-23 and CASC-J6

structure Example : sig
  val id : 'a -> 'a
  val fold : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
  val rev : 'a list -> 'a list
  datatype 'a queue = AQueue of 'a list * 'a list
  val empty : 'a queue
  val dequeue : 'a queue -> 'a option * 'a queue
  val enqueue : 'a -> 'a queue -> 'a queue
end = struct

fun id x = (fn xa => xa) x;

fun fold f [] = id
  | fold f (x :: xs) = fold f xs o f x;

fun rev xs = fold (fn a => fn b => a :: b) xs [];

datatype 'a queue = AQueue of 'a list * 'a list;

val empty : 'a queue = AQueue ([], []);

fun dequeue (AQueue ([], [])) = (NONE, AQueue ([], []))
  | dequeue (AQueue (xs, y :: ys)) = (SOME y, AQueue (xs, ys))
  | dequeue (AQueue (v :: va, [])) =
    let
      val y :: ys = rev (v :: va);
    in
      (SOME y, AQueue ([], ys))
    end;

fun enqueue x (AQueue (xs, ys)) = AQueue (x :: xs, ys);

end; (*struct Example*)