--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Thu Jan 04 17:11:09 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Thu Jan 04 17:17:48 2007 +0100
@@ -984,7 +984,7 @@
\ \ {\isacharparenleft}\isakeyword{attach}\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}{\isacharparenright}%
\begin{isamarkuptext}%
This merely introduces a class \isa{eq} with corresponding
- operation \isa{foo{\isachardot}op\ {\isacharequal}};
+ operation \isa{op\ {\isacharequal}};
the preprocessing framework does the rest.%
\end{isamarkuptext}%
\isamarkuptrue%
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs Thu Jan 04 17:11:09 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs Thu Jan 04 17:17:48 2007 +0100
@@ -6,6 +6,7 @@
heada :: (Codegen.Null a) => ([a] -> a)
heada (y : xs) = y
+heada [] = Codegen.nulla
null_option :: Maybe b
null_option = Nothing
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/arbitrary.ML Thu Jan 04 17:11:09 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/arbitrary.ML Thu Jan 04 17:17:48 2007 +0100
@@ -6,7 +6,8 @@
val arbitrary_option : 'a option = NONE;
-fun dummy_option [] = arbitrary_option;
+fun dummy_option [] = arbitrary_option
+ | dummy_option (x :: xs) = SOME x;
end; (*struct Codegen*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML Thu Jan 04 17:11:09 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML Thu Jan 04 17:17:48 2007 +0100
@@ -4,7 +4,8 @@
structure HOL =
struct
-fun nota false = true;
+fun nota false = true
+ | nota true = false;
end; (*struct HOL*)
@@ -13,7 +14,9 @@
datatype nat = Zero_nat | Suc of nat;
-fun less_nat Zero_nat (Suc n) = true;
+fun less_nat Zero_nat (Suc n) = true
+ | less_nat n Zero_nat = false
+ | less_nat (Suc m) (Suc n) = less_nat m n;
fun less_eq_nat m n = HOL.nota (less_nat n m);
@@ -22,9 +25,8 @@
structure Codegen =
struct
-fun in_interval (k, l) n = (Nat.less_eq_nat k n andalso Nat.less_eq_nat n l)
- | in_interval (k, l) n =
- (Nat.less_eq_nat k n andalso Nat.less_eq_nat n l);
+fun in_interval (k, l) n =
+ (Nat.less_eq_nat k n andalso Nat.less_eq_nat n l);
end; (*struct Codegen*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML Thu Jan 04 17:11:09 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML Thu Jan 04 17:17:48 2007 +0100
@@ -6,9 +6,13 @@
datatype boola = True | False;
-fun nota False = True;
+fun nota False = True
+ | nota True = False;
-fun op_conj y True = y;
+fun op_conj y True = y
+ | op_conj x False = False
+ | op_conj True y = y
+ | op_conj False x = False;
end; (*struct HOL*)
@@ -17,7 +21,9 @@
datatype nat = Zero_nat | Suc of nat;
-fun less_nat Zero_nat (Suc n) = HOL.True;
+fun less_nat Zero_nat (Suc n) = HOL.True
+ | less_nat n Zero_nat = HOL.False
+ | less_nat (Suc m) (Suc n) = less_nat m n;
fun less_eq_nat m n = HOL.nota (less_nat n m);
@@ -27,9 +33,7 @@
struct
fun in_interval (k, l) n =
- HOL.op_conj (Nat.less_eq_nat k n) (Nat.less_eq_nat n l)
- | in_interval (k, l) n =
- HOL.op_conj (Nat.less_eq_nat k n) (Nat.less_eq_nat n l);
+ HOL.op_conj (Nat.less_eq_nat k n) (Nat.less_eq_nat n l);
end; (*struct Codegen*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_mlbool.ML Thu Jan 04 17:11:09 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_mlbool.ML Thu Jan 04 17:17:48 2007 +0100
@@ -4,7 +4,8 @@
structure HOL =
struct
-fun nota false = true;
+fun nota false = true
+ | nota true = false;
end; (*struct HOL*)
@@ -13,7 +14,9 @@
datatype nat = Zero_nat | Suc of nat;
-fun less_nat Zero_nat (Suc n) = true;
+fun less_nat Zero_nat (Suc n) = true
+ | less_nat n Zero_nat = false
+ | less_nat (Suc m) (Suc n) = less_nat m n;
fun less_eq_nat m n = HOL.nota (less_nat n m);
@@ -23,9 +26,7 @@
struct
fun in_interval (k, l) n =
- (Nat.less_eq_nat k n) andalso (Nat.less_eq_nat n l)
- | in_interval (k, l) n =
- (Nat.less_eq_nat k n) andalso (Nat.less_eq_nat n l);
+ (Nat.less_eq_nat k n) andalso (Nat.less_eq_nat n l);
end; (*struct Codegen*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML Thu Jan 04 17:11:09 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML Thu Jan 04 17:17:48 2007 +0100
@@ -14,7 +14,8 @@
type 'a null = {null_ : 'a};
fun null (A_:'a null) = #null_ A_;
-fun head (A_:'a null) (y :: xs) = y;
+fun head (A_:'a null) (y :: xs) = y
+ | head (A_:'a null) [] = null A_;
val null_option : 'b option = NONE;
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML Thu Jan 04 17:11:09 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML Thu Jan 04 17:17:48 2007 +0100
@@ -13,7 +13,8 @@
struct
fun memberl (A_:'a Code_Generator.eq) x (y :: ys) =
- (Code_Generator.op_eq A_ x y orelse memberl A_ x ys);
+ (Code_Generator.op_eq A_ x y orelse memberl A_ x ys)
+ | memberl (A_:'a Code_Generator.eq) x [] = false;
end; (*struct List*)
@@ -24,7 +25,8 @@
(if List.memberl A_ z xs
then (if List.memberl A_ z ys then collect_duplicates A_ xs ys zs
else collect_duplicates A_ xs (z :: ys) zs)
- else collect_duplicates A_ (z :: xs) (z :: ys) zs);
+ else collect_duplicates A_ (z :: xs) (z :: ys) zs)
+ | collect_duplicates (A_:'a Code_Generator.eq) y ys [] = y;
end; (*struct Codegen*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML Thu Jan 04 17:11:09 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML Thu Jan 04 17:17:48 2007 +0100
@@ -7,16 +7,18 @@
datatype nat = Zero_nat | Suc of nat;
fun plus_nat (Suc m) n = plus_nat m (Suc n)
- | plus_nat (Suc m) n = Suc (plus_nat m n);
+ | plus_nat Zero_nat y = y;
-fun times_nat (Suc m) n = plus_nat n (times_nat m n);
+fun times_nat (Suc m) n = plus_nat n (times_nat m n)
+ | times_nat Zero_nat n = Zero_nat;
end; (*struct Nat*)
structure Codegen =
struct
-fun fac (Nat.Suc n) = Nat.times_nat (Nat.Suc n) (fac n);
+fun fac (Nat.Suc n) = Nat.times_nat (Nat.Suc n) (fac n)
+ | fac Nat.Zero_nat = Nat.Suc Nat.Zero_nat;
end; (*struct Codegen*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML Thu Jan 04 17:11:09 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML Thu Jan 04 17:17:48 2007 +0100
@@ -7,9 +7,10 @@
datatype nat = Zero_nat | Suc of nat;
fun plus_nat (Suc m) n = plus_nat m (Suc n)
- | plus_nat (Suc m) n = Suc (plus_nat m n);
+ | plus_nat Zero_nat y = y;
-fun times_nat (Suc m) n = plus_nat n (times_nat m n);
+fun times_nat (Suc m) n = plus_nat n (times_nat m n)
+ | times_nat Zero_nat n = Zero_nat;
end; (*struct Nat*)
@@ -18,8 +19,7 @@
fun fac n =
(case n of Nat.Zero_nat => Nat.Suc Nat.Zero_nat
- | Nat.Suc m => Nat.times_nat n (fac m))
- | fac (Nat.Suc n) = Nat.times_nat (Nat.Suc n) (fac n);
+ | Nat.Suc m => Nat.times_nat n (fac m));
end; (*struct Codegen*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/lookup.ML Thu Jan 04 17:11:09 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/lookup.ML Thu Jan 04 17:17:48 2007 +0100
@@ -5,7 +5,8 @@
struct
fun lookup ((k, v) :: xs) l =
- (if ((k : string) = l) then SOME v else lookup xs l);
+ (if ((k : string) = l) then SOME v else lookup xs l)
+ | lookup [] l = NONE;
end; (*struct Codegen*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML Thu Jan 04 17:11:09 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML Thu Jan 04 17:17:48 2007 +0100
@@ -6,9 +6,13 @@
datatype nat = Zero_nat | Suc of nat;
-fun less_nat Zero_nat (Suc n) = true;
+fun less_nat Zero_nat (Suc n) = true
+ | less_nat n Zero_nat = false
+ | less_nat (Suc m) (Suc n) = less_nat m n;
-fun minus_nat (Suc m) (Suc n) = minus_nat m n;
+fun minus_nat (Suc m) (Suc n) = minus_nat m n
+ | minus_nat Zero_nat n = Zero_nat
+ | minus_nat y Zero_nat = y;
end; (*struct Nat*)
@@ -16,7 +20,13 @@
struct
fun pick ((k, v) :: xs) n =
- (if Nat.less_nat n k then v else pick xs (Nat.minus_nat n k));
+ (if Nat.less_nat n k then v else pick xs (Nat.minus_nat n k))
+ | pick (x :: xs) n =
+ let
+ val (k, v) = x;
+ in
+ (if Nat.less_nat n k then v else pick xs (Nat.minus_nat n k))
+ end;
end; (*struct Codegen*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML Thu Jan 04 17:11:09 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML Thu Jan 04 17:17:48 2007 +0100
@@ -6,9 +6,13 @@
datatype nat = Zero_nat | Suc of nat;
-fun less_nat Zero_nat (Suc n) = true;
+fun less_nat Zero_nat (Suc n) = true
+ | less_nat n Zero_nat = false
+ | less_nat (Suc m) (Suc n) = less_nat m n;
-fun minus_nat (Suc m) (Suc n) = minus_nat m n;
+fun minus_nat (Suc m) (Suc n) = minus_nat m n
+ | minus_nat Zero_nat n = Zero_nat
+ | minus_nat y Zero_nat = y;
end; (*struct Nat*)