|
21190
|
1 |
structure Nat =
|
|
21147
|
2 |
struct
|
|
|
3 |
|
|
24421
|
4 |
datatype nat = Suc of nat | Zero_nat;
|
|
21147
|
5 |
|
|
21190
|
6 |
end; (*struct Nat*)
|
|
21147
|
7 |
|
|
|
8 |
structure Codegen =
|
|
|
9 |
struct
|
|
|
10 |
|
|
22386
|
11 |
type 'a null = {null : 'a};
|
|
|
12 |
fun null (A_:'a null) = #null A_;
|
|
21147
|
13 |
|
|
25182
|
14 |
fun head A_ (x :: xs) = x
|
|
|
15 |
| head A_ [] = null A_;
|
|
21147
|
16 |
|
|
25056
|
17 |
val null_option : 'a option = NONE;
|
|
|
18 |
|
|
|
19 |
fun null_optiona () = {null = null_option} : ('a option) null;
|
|
21147
|
20 |
|
|
21190
|
21 |
val dummy : Nat.nat option =
|
|
25056
|
22 |
head (null_optiona ()) [SOME (Nat.Suc Nat.Zero_nat), NONE];
|
|
21147
|
23 |
|
|
|
24 |
end; (*struct Codegen*)
|