doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML
author wenzelm
Tue Oct 16 17:07:40 2007 +0200 (2007-10-16)
changeset 25056 743f3603ba8b
parent 24628 33137422d7fd
child 25182 64e3f45dc6f4
permissions -rw-r--r--
updated;
haftmann@21190
     1
structure Nat = 
haftmann@21147
     2
struct
haftmann@21147
     3
haftmann@24421
     4
datatype nat = Suc of nat | Zero_nat;
haftmann@21147
     5
haftmann@21190
     6
end; (*struct Nat*)
haftmann@21147
     7
haftmann@21147
     8
structure Codegen = 
haftmann@21147
     9
struct
haftmann@21147
    10
haftmann@22386
    11
type 'a null = {null : 'a};
haftmann@22386
    12
fun null (A_:'a null) = #null A_;
haftmann@21147
    13
haftmann@22798
    14
fun head B_ (x :: xs) = x
haftmann@22798
    15
  | head B_ [] = null B_;
haftmann@21147
    16
wenzelm@25056
    17
val null_option : 'a option = NONE;
wenzelm@25056
    18
wenzelm@25056
    19
fun null_optiona () = {null = null_option} : ('a option) null;
haftmann@21147
    20
haftmann@21190
    21
val dummy : Nat.nat option =
wenzelm@25056
    22
  head (null_optiona ()) [SOME (Nat.Suc Nat.Zero_nat), NONE];
haftmann@21147
    23
haftmann@21147
    24
end; (*struct Codegen*)