doc-src/IsarAdvanced/Codegen/Thy/examples/example.ML
author wenzelm
Thu, 09 Oct 2008 20:53:24 +0200
changeset 28555 d59712ee942c
parent 28421 05d202350b8d
child 29297 62e0f892e525
permissions -rw-r--r--
added enabled; removed pseudo-parallel version of profile -- CRITICAL prevents future join;

structure Example = 
struct

fun foldl f a [] = a
  | foldl f a (x :: xs) = foldl f (f a x) xs;

fun rev xs = foldl (fn xsa => fn x => x :: xsa) [] xs;

fun list_case f1 f2 (a :: lista) = f2 a lista
  | list_case f1 f2 [] = f1;

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

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

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

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

end; (*struct Example*)