doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML
author haftmann
Thu Jan 04 17:17:48 2007 +0100 (2007-01-04)
changeset 21994 dfa5133dbe73
parent 21993 4b802a9e0738
child 22015 12b94d7f7e1f
permissions -rw-r--r--
updated manual
     1 structure ROOT = 
     2 struct
     3 
     4 structure Code_Generator = 
     5 struct
     6 
     7 type 'a eq = {op_eq_ : 'a -> 'a -> bool};
     8 fun op_eq (A_:'a eq) = #op_eq_ A_;
     9 
    10 end; (*struct Code_Generator*)
    11 
    12 structure List = 
    13 struct
    14 
    15 fun memberl (A_:'a Code_Generator.eq) x (y :: ys) =
    16   (Code_Generator.op_eq A_ x y orelse memberl A_ x ys)
    17   | memberl (A_:'a Code_Generator.eq) x [] = false;
    18 
    19 end; (*struct List*)
    20 
    21 structure Codegen = 
    22 struct
    23 
    24 fun collect_duplicates (A_:'a Code_Generator.eq) xs ys (z :: zs) =
    25   (if List.memberl A_ z xs
    26     then (if List.memberl A_ z ys then collect_duplicates A_ xs ys zs
    27            else collect_duplicates A_ xs (z :: ys) zs)
    28     else collect_duplicates A_ (z :: xs) (z :: ys) zs)
    29   | collect_duplicates (A_:'a Code_Generator.eq) y ys [] = y;
    30 
    31 end; (*struct Codegen*)
    32 
    33 end; (*struct ROOT*)