doc-src/Codegen/Thy/examples/Example.hs
author haftmann
Tue, 03 Mar 2009 11:00:51 +0100
changeset 30226 2f4684e2ea95
parent 29798 doc-src/IsarAdvanced/Codegen/Thy/examples/Example.hs@6df726203e39
child 31045 f0c7607bb295
permissions -rw-r--r--
more canonical directory structure of manuals
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
29297
62e0f892e525 updated generated files;
wenzelm
parents: 28421
diff changeset
     1
{-# OPTIONS_GHC -fglasgow-exts #-}
62e0f892e525 updated generated files;
wenzelm
parents: 28421
diff changeset
     2
28421
05d202350b8d reorganized examples
haftmann
parents:
diff changeset
     3
module Example where {
05d202350b8d reorganized examples
haftmann
parents:
diff changeset
     4
05d202350b8d reorganized examples
haftmann
parents:
diff changeset
     5
05d202350b8d reorganized examples
haftmann
parents:
diff changeset
     6
foldla :: forall a b. (a -> b -> a) -> a -> [b] -> a;
05d202350b8d reorganized examples
haftmann
parents:
diff changeset
     7
foldla f a [] = a;
05d202350b8d reorganized examples
haftmann
parents:
diff changeset
     8
foldla f a (x : xs) = foldla f (f a x) xs;
05d202350b8d reorganized examples
haftmann
parents:
diff changeset
     9
05d202350b8d reorganized examples
haftmann
parents:
diff changeset
    10
rev :: forall a. [a] -> [a];
05d202350b8d reorganized examples
haftmann
parents:
diff changeset
    11
rev xs = foldla (\ xsa x -> x : xsa) [] xs;
05d202350b8d reorganized examples
haftmann
parents:
diff changeset
    12
05d202350b8d reorganized examples
haftmann
parents:
diff changeset
    13
list_case :: forall t a. t -> (a -> [a] -> t) -> [a] -> t;
05d202350b8d reorganized examples
haftmann
parents:
diff changeset
    14
list_case f1 f2 (a : list) = f2 a list;
05d202350b8d reorganized examples
haftmann
parents:
diff changeset
    15
list_case f1 f2 [] = f1;
05d202350b8d reorganized examples
haftmann
parents:
diff changeset
    16
29798
6df726203e39 proper datatype abstraction example
haftmann
parents: 29297
diff changeset
    17
data Queue a = AQueue [a] [a];
28421
05d202350b8d reorganized examples
haftmann
parents:
diff changeset
    18
05d202350b8d reorganized examples
haftmann
parents:
diff changeset
    19
empty :: forall a. Queue a;
29798
6df726203e39 proper datatype abstraction example
haftmann
parents: 29297
diff changeset
    20
empty = AQueue [] [];
28421
05d202350b8d reorganized examples
haftmann
parents:
diff changeset
    21
05d202350b8d reorganized examples
haftmann
parents:
diff changeset
    22
dequeue :: forall a. Queue a -> (Maybe a, Queue a);
29798
6df726203e39 proper datatype abstraction example
haftmann
parents: 29297
diff changeset
    23
dequeue (AQueue [] []) = (Nothing, AQueue [] []);
6df726203e39 proper datatype abstraction example
haftmann
parents: 29297
diff changeset
    24
dequeue (AQueue xs (y : ys)) = (Just y, AQueue xs ys);
6df726203e39 proper datatype abstraction example
haftmann
parents: 29297
diff changeset
    25
dequeue (AQueue (v : va) []) =
28421
05d202350b8d reorganized examples
haftmann
parents:
diff changeset
    26
  let {
05d202350b8d reorganized examples
haftmann
parents:
diff changeset
    27
    (y : ys) = rev (v : va);
29798
6df726203e39 proper datatype abstraction example
haftmann
parents: 29297
diff changeset
    28
  } in (Just y, AQueue [] ys);
28421
05d202350b8d reorganized examples
haftmann
parents:
diff changeset
    29
05d202350b8d reorganized examples
haftmann
parents:
diff changeset
    30
enqueue :: forall a. a -> Queue a -> Queue a;
29798
6df726203e39 proper datatype abstraction example
haftmann
parents: 29297
diff changeset
    31
enqueue x (AQueue xs ys) = AQueue (x : xs) ys;
28421
05d202350b8d reorganized examples
haftmann
parents:
diff changeset
    32
05d202350b8d reorganized examples
haftmann
parents:
diff changeset
    33
}