# HG changeset patch
# User haftmann
# Date 1222771756 -7200
# Node ID 05d202350b8d0ff1d7af59edaa4444ed57a076a6
# Parent  293b166c45c5a1ec9bb019e04fec8344b8c8a332
reorganized examples

diff -r 293b166c45c5 -r 05d202350b8d doc-src/IsarAdvanced/Codegen/Thy/examples/Example.hs
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/Example.hs	Tue Sep 30 12:49:16 2008 +0200
@@ -0,0 +1,31 @@
+module Example where {
+
+
+foldla :: forall a b. (a -> b -> a) -> a -> [b] -> a;
+foldla f a [] = a;
+foldla f a (x : xs) = foldla f (f a x) xs;
+
+rev :: forall a. [a] -> [a];
+rev xs = foldla (\ xsa x -> x : xsa) [] xs;
+
+list_case :: forall t a. t -> (a -> [a] -> t) -> [a] -> t;
+list_case f1 f2 (a : list) = f2 a list;
+list_case f1 f2 [] = f1;
+
+data Queue a = Queue [a] [a];
+
+empty :: forall a. Queue a;
+empty = Queue [] [];
+
+dequeue :: forall a. Queue a -> (Maybe a, Queue a);
+dequeue (Queue [] []) = (Nothing, Queue [] []);
+dequeue (Queue xs (y : ys)) = (Just y, Queue xs ys);
+dequeue (Queue (v : va) []) =
+  let {
+    (y : ys) = rev (v : va);
+  } in (Just y, Queue [] ys);
+
+enqueue :: forall a. a -> Queue a -> Queue a;
+enqueue x (Queue xs ys) = Queue (x : xs) ys;
+
+}
diff -r 293b166c45c5 -r 05d202350b8d doc-src/IsarAdvanced/Codegen/Thy/examples/example.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/example.ML	Tue Sep 30 12:49:16 2008 +0200
@@ -0,0 +1,27 @@
+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*)