doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml
author blanchet
Tue, 17 Feb 2009 14:01:54 +0100
changeset 29956 62f931b257b7
parent 25182 64e3f45dc6f4
permissions -rw-r--r--
Reintroduce set_interpreter for Collect and op :. I removed them by accident when removing old code that dealt with the "set" type. Incidentally, there is still some broken "set" code in Refute that should be fixed (see TODO in refute.ML).
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
22308
7901493455ca added OCaml example
haftmann
parents:
diff changeset
     1
module Nat = 
7901493455ca added OCaml example
haftmann
parents:
diff changeset
     2
struct
7901493455ca added OCaml example
haftmann
parents:
diff changeset
     3
24421
acfb2413faa3 updated
haftmann
parents: 23850
diff changeset
     4
type nat = Suc of nat | Zero_nat;;
22308
7901493455ca added OCaml example
haftmann
parents:
diff changeset
     5
7901493455ca added OCaml example
haftmann
parents:
diff changeset
     6
end;; (*struct Nat*)
7901493455ca added OCaml example
haftmann
parents:
diff changeset
     7
7901493455ca added OCaml example
haftmann
parents:
diff changeset
     8
module Codegen = 
7901493455ca added OCaml example
haftmann
parents:
diff changeset
     9
struct
7901493455ca added OCaml example
haftmann
parents:
diff changeset
    10
7901493455ca added OCaml example
haftmann
parents:
diff changeset
    11
type 'a null = {null : 'a};;
7901493455ca added OCaml example
haftmann
parents:
diff changeset
    12
let null _A = _A.null;;
7901493455ca added OCaml example
haftmann
parents:
diff changeset
    13
25182
64e3f45dc6f4 updated;
wenzelm
parents: 25056
diff changeset
    14
let rec head _A = function x :: xs -> x
64e3f45dc6f4 updated;
wenzelm
parents: 25056
diff changeset
    15
                  | [] -> null _A;;
22308
7901493455ca added OCaml example
haftmann
parents:
diff changeset
    16
25056
743f3603ba8b updated;
wenzelm
parents: 24628
diff changeset
    17
let rec null_option = None;;
743f3603ba8b updated;
wenzelm
parents: 24628
diff changeset
    18
743f3603ba8b updated;
wenzelm
parents: 24628
diff changeset
    19
let null_optiona () = ({null = null_option} : ('a option) null);;
22308
7901493455ca added OCaml example
haftmann
parents:
diff changeset
    20
7901493455ca added OCaml example
haftmann
parents:
diff changeset
    21
let rec dummy
25056
743f3603ba8b updated;
wenzelm
parents: 24628
diff changeset
    22
  = head (null_optiona ()) [Some (Nat.Suc Nat.Zero_nat); None];;
22308
7901493455ca added OCaml example
haftmann
parents:
diff changeset
    23
7901493455ca added OCaml example
haftmann
parents:
diff changeset
    24
end;; (*struct Codegen*)