doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML
author wenzelm
Sat, 04 Nov 2006 12:53:35 +0100
changeset 21167 276dd93cfa97
parent 21147 737a94f047e3
child 21172 eea3c9048c7a
permissions -rw-r--r--
optional argument for timespan (default 100);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
21147
737a94f047e3 continued tutorial
haftmann
parents:
diff changeset
     1
structure ROOT = 
737a94f047e3 continued tutorial
haftmann
parents:
diff changeset
     2
struct
737a94f047e3 continued tutorial
haftmann
parents:
diff changeset
     3
737a94f047e3 continued tutorial
haftmann
parents:
diff changeset
     4
structure IntDef = 
737a94f047e3 continued tutorial
haftmann
parents:
diff changeset
     5
struct
737a94f047e3 continued tutorial
haftmann
parents:
diff changeset
     6
737a94f047e3 continued tutorial
haftmann
parents:
diff changeset
     7
datatype nat = Zero_nat | Succ_nat of nat;
737a94f047e3 continued tutorial
haftmann
parents:
diff changeset
     8
737a94f047e3 continued tutorial
haftmann
parents:
diff changeset
     9
fun plus_nat (Succ_nat m) n = plus_nat m (Succ_nat n)
737a94f047e3 continued tutorial
haftmann
parents:
diff changeset
    10
  | plus_nat Zero_nat y = y;
737a94f047e3 continued tutorial
haftmann
parents:
diff changeset
    11
737a94f047e3 continued tutorial
haftmann
parents:
diff changeset
    12
fun times_nat (Succ_nat m) n = plus_nat n (times_nat m n)
737a94f047e3 continued tutorial
haftmann
parents:
diff changeset
    13
  | times_nat Zero_nat na = Zero_nat;
737a94f047e3 continued tutorial
haftmann
parents:
diff changeset
    14
737a94f047e3 continued tutorial
haftmann
parents:
diff changeset
    15
end; (*struct IntDef*)
737a94f047e3 continued tutorial
haftmann
parents:
diff changeset
    16
737a94f047e3 continued tutorial
haftmann
parents:
diff changeset
    17
structure Codegen = 
737a94f047e3 continued tutorial
haftmann
parents:
diff changeset
    18
struct
737a94f047e3 continued tutorial
haftmann
parents:
diff changeset
    19
737a94f047e3 continued tutorial
haftmann
parents:
diff changeset
    20
fun fac n =
737a94f047e3 continued tutorial
haftmann
parents:
diff changeset
    21
  (case n of IntDef.Zero_nat => IntDef.Succ_nat IntDef.Zero_nat
737a94f047e3 continued tutorial
haftmann
parents:
diff changeset
    22
     | IntDef.Succ_nat ma => IntDef.times_nat n (fac ma));
737a94f047e3 continued tutorial
haftmann
parents:
diff changeset
    23
737a94f047e3 continued tutorial
haftmann
parents:
diff changeset
    24
end; (*struct Codegen*)
737a94f047e3 continued tutorial
haftmann
parents:
diff changeset
    25
737a94f047e3 continued tutorial
haftmann
parents:
diff changeset
    26
end; (*struct ROOT*)