doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML
author haftmann
Thu Jan 04 17:17:48 2007 +0100 (2007-01-04)
changeset 21994 dfa5133dbe73
parent 21993 4b802a9e0738
child 22188 a63889770d57
permissions -rw-r--r--
updated manual
haftmann@21147
     1
structure ROOT = 
haftmann@21147
     2
struct
haftmann@21147
     3
haftmann@21190
     4
structure Nat = 
haftmann@21147
     5
struct
haftmann@21147
     6
haftmann@21190
     7
datatype nat = Zero_nat | Suc of nat;
haftmann@21147
     8
haftmann@21190
     9
end; (*struct Nat*)
haftmann@21147
    10
haftmann@21147
    11
structure Codegen = 
haftmann@21147
    12
struct
haftmann@21147
    13
haftmann@21147
    14
type 'a null = {null_ : 'a};
haftmann@21190
    15
fun null (A_:'a null) = #null_ A_;
haftmann@21147
    16
haftmann@21994
    17
fun head (A_:'a null) (y :: xs) = y
haftmann@21994
    18
  | head (A_:'a null) [] = null A_;
haftmann@21147
    19
haftmann@21147
    20
val null_option : 'b option = NONE;
haftmann@21147
    21
haftmann@21993
    22
fun null_optiona () = {null_ = null_option} : ('b option) null ;;
haftmann@21147
    23
haftmann@21190
    24
val dummy : Nat.nat option =
haftmann@21190
    25
  head (null_optiona ()) [SOME (Nat.Suc Nat.Zero_nat), NONE];
haftmann@21147
    26
haftmann@21147
    27
end; (*struct Codegen*)
haftmann@21147
    28
haftmann@21147
    29
end; (*struct ROOT*)