doc-src/IsarAdvanced/Codegen/Thy/examples/example.ML
changeset 30228 2aaf339fb7c1
parent 30224 79136ce06bdb
parent 30227 853abb4853cc
child 30229 9861257b18e6
child 30243 09d5944e224e
equal deleted inserted replaced
30224:79136ce06bdb 30228:2aaf339fb7c1
     1 structure Example = 
       
     2 struct
       
     3 
       
     4 fun foldl f a [] = a
       
     5   | foldl f a (x :: xs) = foldl f (f a x) xs;
       
     6 
       
     7 fun rev xs = foldl (fn xsa => fn x => x :: xsa) [] xs;
       
     8 
       
     9 fun list_case f1 f2 (a :: lista) = f2 a lista
       
    10   | list_case f1 f2 [] = f1;
       
    11 
       
    12 datatype 'a queue = AQueue of 'a list * 'a list;
       
    13 
       
    14 val empty : 'a queue = AQueue ([], [])
       
    15 
       
    16 fun dequeue (AQueue ([], [])) = (NONE, AQueue ([], []))
       
    17   | dequeue (AQueue (xs, y :: ys)) = (SOME y, AQueue (xs, ys))
       
    18   | dequeue (AQueue (v :: va, [])) =
       
    19     let
       
    20       val y :: ys = rev (v :: va);
       
    21     in
       
    22       (SOME y, AQueue ([], ys))
       
    23     end;
       
    24 
       
    25 fun enqueue x (AQueue (xs, ys)) = AQueue (x :: xs, ys);
       
    26 
       
    27 end; (*struct Example*)