updated manual
authorhaftmann
Thu Jan 04 17:17:48 2007 +0100 (2007-01-04)
changeset 21994dfa5133dbe73
parent 21993 4b802a9e0738
child 21995 89d58ed34299
updated manual
doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex
doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs
doc-src/IsarAdvanced/Codegen/Thy/examples/arbitrary.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/bool_mlbool.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/lookup.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML
     1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Thu Jan 04 17:11:09 2007 +0100
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Thu Jan 04 17:17:48 2007 +0100
     1.3 @@ -984,7 +984,7 @@
     1.4  \ \ {\isacharparenleft}\isakeyword{attach}\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}{\isacharparenright}%
     1.5  \begin{isamarkuptext}%
     1.6  This merely introduces a class \isa{eq} with corresponding
     1.7 -  operation \isa{foo{\isachardot}op\ {\isacharequal}};
     1.8 +  operation \isa{op\ {\isacharequal}};
     1.9    the preprocessing framework does the rest.%
    1.10  \end{isamarkuptext}%
    1.11  \isamarkuptrue%
     2.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs	Thu Jan 04 17:11:09 2007 +0100
     2.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs	Thu Jan 04 17:17:48 2007 +0100
     2.3 @@ -6,6 +6,7 @@
     2.4  
     2.5  heada :: (Codegen.Null a) => ([a] -> a)
     2.6  heada (y : xs) = y
     2.7 +heada [] = Codegen.nulla
     2.8  
     2.9  null_option :: Maybe b
    2.10  null_option = Nothing
     3.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/arbitrary.ML	Thu Jan 04 17:11:09 2007 +0100
     3.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/arbitrary.ML	Thu Jan 04 17:17:48 2007 +0100
     3.3 @@ -6,7 +6,8 @@
     3.4  
     3.5  val arbitrary_option : 'a option = NONE;
     3.6  
     3.7 -fun dummy_option [] = arbitrary_option;
     3.8 +fun dummy_option [] = arbitrary_option
     3.9 +  | dummy_option (x :: xs) = SOME x;
    3.10  
    3.11  end; (*struct Codegen*)
    3.12  
     4.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML	Thu Jan 04 17:11:09 2007 +0100
     4.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML	Thu Jan 04 17:17:48 2007 +0100
     4.3 @@ -4,7 +4,8 @@
     4.4  structure HOL = 
     4.5  struct
     4.6  
     4.7 -fun nota false = true;
     4.8 +fun nota false = true
     4.9 +  | nota true = false;
    4.10  
    4.11  end; (*struct HOL*)
    4.12  
    4.13 @@ -13,7 +14,9 @@
    4.14  
    4.15  datatype nat = Zero_nat | Suc of nat;
    4.16  
    4.17 -fun less_nat Zero_nat (Suc n) = true;
    4.18 +fun less_nat Zero_nat (Suc n) = true
    4.19 +  | less_nat n Zero_nat = false
    4.20 +  | less_nat (Suc m) (Suc n) = less_nat m n;
    4.21  
    4.22  fun less_eq_nat m n = HOL.nota (less_nat n m);
    4.23  
    4.24 @@ -22,9 +25,8 @@
    4.25  structure Codegen = 
    4.26  struct
    4.27  
    4.28 -fun in_interval (k, l) n = (Nat.less_eq_nat k n andalso Nat.less_eq_nat n l)
    4.29 -  | in_interval (k, l) n =
    4.30 -    (Nat.less_eq_nat k n andalso Nat.less_eq_nat n l);
    4.31 +fun in_interval (k, l) n =
    4.32 +  (Nat.less_eq_nat k n andalso Nat.less_eq_nat n l);
    4.33  
    4.34  end; (*struct Codegen*)
    4.35  
     5.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML	Thu Jan 04 17:11:09 2007 +0100
     5.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML	Thu Jan 04 17:17:48 2007 +0100
     5.3 @@ -6,9 +6,13 @@
     5.4  
     5.5  datatype boola = True | False;
     5.6  
     5.7 -fun nota False = True;
     5.8 +fun nota False = True
     5.9 +  | nota True = False;
    5.10  
    5.11 -fun op_conj y True = y;
    5.12 +fun op_conj y True = y
    5.13 +  | op_conj x False = False
    5.14 +  | op_conj True y = y
    5.15 +  | op_conj False x = False;
    5.16  
    5.17  end; (*struct HOL*)
    5.18  
    5.19 @@ -17,7 +21,9 @@
    5.20  
    5.21  datatype nat = Zero_nat | Suc of nat;
    5.22  
    5.23 -fun less_nat Zero_nat (Suc n) = HOL.True;
    5.24 +fun less_nat Zero_nat (Suc n) = HOL.True
    5.25 +  | less_nat n Zero_nat = HOL.False
    5.26 +  | less_nat (Suc m) (Suc n) = less_nat m n;
    5.27  
    5.28  fun less_eq_nat m n = HOL.nota (less_nat n m);
    5.29  
    5.30 @@ -27,9 +33,7 @@
    5.31  struct
    5.32  
    5.33  fun in_interval (k, l) n =
    5.34 -  HOL.op_conj (Nat.less_eq_nat k n) (Nat.less_eq_nat n l)
    5.35 -  | in_interval (k, l) n =
    5.36 -    HOL.op_conj (Nat.less_eq_nat k n) (Nat.less_eq_nat n l);
    5.37 +  HOL.op_conj (Nat.less_eq_nat k n) (Nat.less_eq_nat n l);
    5.38  
    5.39  end; (*struct Codegen*)
    5.40  
     6.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_mlbool.ML	Thu Jan 04 17:11:09 2007 +0100
     6.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_mlbool.ML	Thu Jan 04 17:17:48 2007 +0100
     6.3 @@ -4,7 +4,8 @@
     6.4  structure HOL = 
     6.5  struct
     6.6  
     6.7 -fun nota false = true;
     6.8 +fun nota false = true
     6.9 +  | nota true = false;
    6.10  
    6.11  end; (*struct HOL*)
    6.12  
    6.13 @@ -13,7 +14,9 @@
    6.14  
    6.15  datatype nat = Zero_nat | Suc of nat;
    6.16  
    6.17 -fun less_nat Zero_nat (Suc n) = true;
    6.18 +fun less_nat Zero_nat (Suc n) = true
    6.19 +  | less_nat n Zero_nat = false
    6.20 +  | less_nat (Suc m) (Suc n) = less_nat m n;
    6.21  
    6.22  fun less_eq_nat m n = HOL.nota (less_nat n m);
    6.23  
    6.24 @@ -23,9 +26,7 @@
    6.25  struct
    6.26  
    6.27  fun in_interval (k, l) n =
    6.28 -  (Nat.less_eq_nat k n) andalso (Nat.less_eq_nat n l)
    6.29 -  | in_interval (k, l) n =
    6.30 -    (Nat.less_eq_nat k n) andalso (Nat.less_eq_nat n l);
    6.31 +  (Nat.less_eq_nat k n) andalso (Nat.less_eq_nat n l);
    6.32  
    6.33  end; (*struct Codegen*)
    6.34  
     7.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML	Thu Jan 04 17:11:09 2007 +0100
     7.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML	Thu Jan 04 17:17:48 2007 +0100
     7.3 @@ -14,7 +14,8 @@
     7.4  type 'a null = {null_ : 'a};
     7.5  fun null (A_:'a null) = #null_ A_;
     7.6  
     7.7 -fun head (A_:'a null) (y :: xs) = y;
     7.8 +fun head (A_:'a null) (y :: xs) = y
     7.9 +  | head (A_:'a null) [] = null A_;
    7.10  
    7.11  val null_option : 'b option = NONE;
    7.12  
     8.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML	Thu Jan 04 17:11:09 2007 +0100
     8.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML	Thu Jan 04 17:17:48 2007 +0100
     8.3 @@ -13,7 +13,8 @@
     8.4  struct
     8.5  
     8.6  fun memberl (A_:'a Code_Generator.eq) x (y :: ys) =
     8.7 -  (Code_Generator.op_eq A_ x y orelse memberl A_ x ys);
     8.8 +  (Code_Generator.op_eq A_ x y orelse memberl A_ x ys)
     8.9 +  | memberl (A_:'a Code_Generator.eq) x [] = false;
    8.10  
    8.11  end; (*struct List*)
    8.12  
    8.13 @@ -24,7 +25,8 @@
    8.14    (if List.memberl A_ z xs
    8.15      then (if List.memberl A_ z ys then collect_duplicates A_ xs ys zs
    8.16             else collect_duplicates A_ xs (z :: ys) zs)
    8.17 -    else collect_duplicates A_ (z :: xs) (z :: ys) zs);
    8.18 +    else collect_duplicates A_ (z :: xs) (z :: ys) zs)
    8.19 +  | collect_duplicates (A_:'a Code_Generator.eq) y ys [] = y;
    8.20  
    8.21  end; (*struct Codegen*)
    8.22  
     9.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML	Thu Jan 04 17:11:09 2007 +0100
     9.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML	Thu Jan 04 17:17:48 2007 +0100
     9.3 @@ -7,16 +7,18 @@
     9.4  datatype nat = Zero_nat | Suc of nat;
     9.5  
     9.6  fun plus_nat (Suc m) n = plus_nat m (Suc n)
     9.7 -  | plus_nat (Suc m) n = Suc (plus_nat m n);
     9.8 +  | plus_nat Zero_nat y = y;
     9.9  
    9.10 -fun times_nat (Suc m) n = plus_nat n (times_nat m n);
    9.11 +fun times_nat (Suc m) n = plus_nat n (times_nat m n)
    9.12 +  | times_nat Zero_nat n = Zero_nat;
    9.13  
    9.14  end; (*struct Nat*)
    9.15  
    9.16  structure Codegen = 
    9.17  struct
    9.18  
    9.19 -fun fac (Nat.Suc n) = Nat.times_nat (Nat.Suc n) (fac n);
    9.20 +fun fac (Nat.Suc n) = Nat.times_nat (Nat.Suc n) (fac n)
    9.21 +  | fac Nat.Zero_nat = Nat.Suc Nat.Zero_nat;
    9.22  
    9.23  end; (*struct Codegen*)
    9.24  
    10.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML	Thu Jan 04 17:11:09 2007 +0100
    10.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML	Thu Jan 04 17:17:48 2007 +0100
    10.3 @@ -7,9 +7,10 @@
    10.4  datatype nat = Zero_nat | Suc of nat;
    10.5  
    10.6  fun plus_nat (Suc m) n = plus_nat m (Suc n)
    10.7 -  | plus_nat (Suc m) n = Suc (plus_nat m n);
    10.8 +  | plus_nat Zero_nat y = y;
    10.9  
   10.10 -fun times_nat (Suc m) n = plus_nat n (times_nat m n);
   10.11 +fun times_nat (Suc m) n = plus_nat n (times_nat m n)
   10.12 +  | times_nat Zero_nat n = Zero_nat;
   10.13  
   10.14  end; (*struct Nat*)
   10.15  
   10.16 @@ -18,8 +19,7 @@
   10.17  
   10.18  fun fac n =
   10.19    (case n of Nat.Zero_nat => Nat.Suc Nat.Zero_nat
   10.20 -     | Nat.Suc m => Nat.times_nat n (fac m))
   10.21 -  | fac (Nat.Suc n) = Nat.times_nat (Nat.Suc n) (fac n);
   10.22 +     | Nat.Suc m => Nat.times_nat n (fac m));
   10.23  
   10.24  end; (*struct Codegen*)
   10.25  
    11.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/lookup.ML	Thu Jan 04 17:11:09 2007 +0100
    11.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/lookup.ML	Thu Jan 04 17:17:48 2007 +0100
    11.3 @@ -5,7 +5,8 @@
    11.4  struct
    11.5  
    11.6  fun lookup ((k, v) :: xs) l =
    11.7 -  (if ((k : string) = l) then SOME v else lookup xs l);
    11.8 +  (if ((k : string) = l) then SOME v else lookup xs l)
    11.9 +  | lookup [] l = NONE;
   11.10  
   11.11  end; (*struct Codegen*)
   11.12  
    12.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML	Thu Jan 04 17:11:09 2007 +0100
    12.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML	Thu Jan 04 17:17:48 2007 +0100
    12.3 @@ -6,9 +6,13 @@
    12.4  
    12.5  datatype nat = Zero_nat | Suc of nat;
    12.6  
    12.7 -fun less_nat Zero_nat (Suc n) = true;
    12.8 +fun less_nat Zero_nat (Suc n) = true
    12.9 +  | less_nat n Zero_nat = false
   12.10 +  | less_nat (Suc m) (Suc n) = less_nat m n;
   12.11  
   12.12 -fun minus_nat (Suc m) (Suc n) = minus_nat m n;
   12.13 +fun minus_nat (Suc m) (Suc n) = minus_nat m n
   12.14 +  | minus_nat Zero_nat n = Zero_nat
   12.15 +  | minus_nat y Zero_nat = y;
   12.16  
   12.17  end; (*struct Nat*)
   12.18  
   12.19 @@ -16,7 +20,13 @@
   12.20  struct
   12.21  
   12.22  fun pick ((k, v) :: xs) n =
   12.23 -  (if Nat.less_nat n k then v else pick xs (Nat.minus_nat n k));
   12.24 +  (if Nat.less_nat n k then v else pick xs (Nat.minus_nat n k))
   12.25 +  | pick (x :: xs) n =
   12.26 +    let
   12.27 +      val (k, v) = x;
   12.28 +    in
   12.29 +      (if Nat.less_nat n k then v else pick xs (Nat.minus_nat n k))
   12.30 +    end;
   12.31  
   12.32  end; (*struct Codegen*)
   12.33  
    13.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML	Thu Jan 04 17:11:09 2007 +0100
    13.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML	Thu Jan 04 17:17:48 2007 +0100
    13.3 @@ -6,9 +6,13 @@
    13.4  
    13.5  datatype nat = Zero_nat | Suc of nat;
    13.6  
    13.7 -fun less_nat Zero_nat (Suc n) = true;
    13.8 +fun less_nat Zero_nat (Suc n) = true
    13.9 +  | less_nat n Zero_nat = false
   13.10 +  | less_nat (Suc m) (Suc n) = less_nat m n;
   13.11  
   13.12 -fun minus_nat (Suc m) (Suc n) = minus_nat m n;
   13.13 +fun minus_nat (Suc m) (Suc n) = minus_nat m n
   13.14 +  | minus_nat Zero_nat n = Zero_nat
   13.15 +  | minus_nat y Zero_nat = y;
   13.16  
   13.17  end; (*struct Nat*)
   13.18