updated
authorhaftmann
Thu Jul 19 21:47:34 2007 +0200 (2007-07-19)
changeset 23850f1434532a562
parent 23849 2a0e24c74593
child 23851 7921b81baf96
updated
NEWS
doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex
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/class.ocaml
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/lexicographic.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/set_list.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML
     1.1 --- a/NEWS	Thu Jul 19 15:37:37 2007 +0200
     1.2 +++ b/NEWS	Thu Jul 19 21:47:34 2007 +0200
     1.3 @@ -90,13 +90,13 @@
     1.4  code for ML and Haskell (including "class"es).  A short usage sketch:
     1.5  
     1.6      internal compilation:
     1.7 -        code_gen <list of constants (term syntax)> (SML #)
     1.8 +        code_gen <list of constants (term syntax)> in SML
     1.9      writing SML code to a file:
    1.10 -        code_gen <list of constants (term syntax)> (SML <filename>)
    1.11 +        code_gen <list of constants (term syntax)> in SML <filename>
    1.12      writing OCaml code to a file:
    1.13 -        code_gen <list of constants (term syntax)> (OCaml <filename>)
    1.14 +        code_gen <list of constants (term syntax)> in OCaml <filename>
    1.15      writing Haskell code to a bunch of files:
    1.16 -        code_gen <list of constants (term syntax)> (Haskell <filename>)
    1.17 +        code_gen <list of constants (term syntax)> in Haskell <filename>
    1.18  
    1.19  Reasonable default setup of framework in HOL/Main.
    1.20  
    1.21 @@ -541,6 +541,27 @@
    1.22  
    1.23  *** HOL ***
    1.24  
    1.25 +* Code generator library theories:
    1.26 +  * Pretty_Int represents HOL integers by big integer literals in target
    1.27 +    languages.
    1.28 +  * Pretty_Char represents HOL characters by character literals in target
    1.29 +    languages.
    1.30 +  * Pretty_Char_chr like Pretty_Char, but also offers treatment of character
    1.31 +    codes; includes Pretty_Int.
    1.32 +  * Executable_Set allows to generate code for finite sets using lists.
    1.33 +  * Executable_Rat implements rational numbers as triples (sign, enumerator,
    1.34 +    denominator).
    1.35 +  * Executable_Real implements a subset of real numbers, namly those
    1.36 +    representable by rational numbers.
    1.37 +  * Efficient_Nat implements natural numbers by integers, which in general will
    1.38 +    result in higher efficency; pattern matching with 0/Suc is eliminated;
    1.39 +    includes Pretty_Int.
    1.40 +  * ML_String provides an additional datatype ml_string; in the HOL default
    1.41 +    setup, strings in HOL are mapped to lists of HOL characters in SML; values
    1.42 +    of type ml_string are mapped to strings in SML.
    1.43 +  * ML_Int provides an additional datatype ml_int which is mapped to to SML
    1.44 +    built-in integers.
    1.45 +
    1.46  * New package for inductive predicates
    1.47  
    1.48    An n-ary predicate p with m parameters z_1, ..., z_m can now be defined via
     2.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Thu Jul 19 15:37:37 2007 +0200
     2.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Thu Jul 19 21:47:34 2007 +0200
     2.3 @@ -469,17 +469,17 @@
     2.4      \item[@{text "Pretty_Char_chr"}] like @{text "Pretty_Char"},
     2.5         but also offers treatment of character codes; includes
     2.6         @{text "Pretty_Int"}.
     2.7 -    \item[@{text "ExecutableSet"}] allows to generate code
     2.8 +    \item[@{text "Executable_Set"}] allows to generate code
     2.9         for finite sets using lists.
    2.10 -    \item[@{text "ExecutableRat"}] \label{exec_rat} implements rational
    2.11 +    \item[@{text "Executable_Rat"}] \label{exec_rat} implements rational
    2.12         numbers as triples @{text "(sign, enumerator, denominator)"}.
    2.13      \item[@{text "Executable_Real"}] implements a subset of real numbers,
    2.14         namly those representable by rational numbers.
    2.15 -    \item[@{text "EfficientNat"}] \label{eff_nat} implements natural numbers by integers,
    2.16 +    \item[@{text "Efficient_Nat"}] \label{eff_nat} implements natural numbers by integers,
    2.17         which in general will result in higher efficency; pattern
    2.18         matching with @{const "0\<Colon>nat"} / @{const "Suc"}
    2.19         is eliminated;  includes @{text "Pretty_Int"}.
    2.20 -    \item[@{text "MLString"}] provides an additional datatype @{text "mlstring"};
    2.21 +    \item[@{text "ML_String"}] provides an additional datatype @{text "mlstring"};
    2.22         in the @{text HOL} default setup, strings in HOL are mapped to list
    2.23         of @{text HOL} characters in SML; values of type @{text "mlstring"} are
    2.24         mapped to strings in SML.
    2.25 @@ -592,7 +592,7 @@
    2.26  
    2.27  text {*
    2.28    The membership test during preprocessing is rewritten,
    2.29 -  resulting in @{const List.memberl}, which itself
    2.30 +  resulting in @{const List.member}, which itself
    2.31    performs an explicit equality check.
    2.32  *}
    2.33  
    2.34 @@ -804,16 +804,6 @@
    2.35    for the type constructor's (the constant's) arguments.
    2.36  *}
    2.37  
    2.38 -code_reserved SML
    2.39 -  bool true false
    2.40 -
    2.41 -text {*
    2.42 -  To assert that the existing \qt{bool}, \qt{true} and \qt{false}
    2.43 -  is not used for generated code, we use @{text "\<CODERESERVED>"}.
    2.44 -
    2.45 -  After this setup, code looks quite more readable:
    2.46 -*}
    2.47 -
    2.48  code_gen in_interval (*<*)in SML(*>*) in SML file "examples/bool_mlbool.ML"
    2.49  
    2.50  text {*
     3.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Thu Jul 19 15:37:37 2007 +0200
     3.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Thu Jul 19 21:47:34 2007 +0200
     3.3 @@ -590,17 +590,17 @@
     3.4      \item[\isa{Pretty{\isacharunderscore}Char{\isacharunderscore}chr}] like \isa{Pretty{\isacharunderscore}Char},
     3.5         but also offers treatment of character codes; includes
     3.6         \isa{Pretty{\isacharunderscore}Int}.
     3.7 -    \item[\isa{ExecutableSet}] allows to generate code
     3.8 +    \item[\isa{Executable{\isacharunderscore}Set}] allows to generate code
     3.9         for finite sets using lists.
    3.10 -    \item[\isa{ExecutableRat}] \label{exec_rat} implements rational
    3.11 +    \item[\isa{Executable{\isacharunderscore}Rat}] \label{exec_rat} implements rational
    3.12         numbers as triples \isa{{\isacharparenleft}sign{\isacharcomma}\ enumerator{\isacharcomma}\ denominator{\isacharparenright}}.
    3.13      \item[\isa{Executable{\isacharunderscore}Real}] implements a subset of real numbers,
    3.14         namly those representable by rational numbers.
    3.15 -    \item[\isa{EfficientNat}] \label{eff_nat} implements natural numbers by integers,
    3.16 +    \item[\isa{Efficient{\isacharunderscore}Nat}] \label{eff_nat} implements natural numbers by integers,
    3.17         which in general will result in higher efficency; pattern
    3.18         matching with \isa{{\isadigit{0}}} / \isa{Suc}
    3.19         is eliminated;  includes \isa{Pretty{\isacharunderscore}Int}.
    3.20 -    \item[\isa{MLString}] provides an additional datatype \isa{mlstring};
    3.21 +    \item[\isa{ML{\isacharunderscore}String}] provides an additional datatype \isa{mlstring};
    3.22         in the \isa{HOL} default setup, strings in HOL are mapped to list
    3.23         of \isa{HOL} characters in SML; values of type \isa{mlstring} are
    3.24         mapped to strings in SML.
    3.25 @@ -1086,16 +1086,6 @@
    3.26    for the type constructor's (the constant's) arguments.%
    3.27  \end{isamarkuptext}%
    3.28  \isamarkuptrue%
    3.29 -\isacommand{code{\isacharunderscore}reserved}\isamarkupfalse%
    3.30 -\ SML\isanewline
    3.31 -\ \ bool\ true\ false%
    3.32 -\begin{isamarkuptext}%
    3.33 -To assert that the existing \qt{bool}, \qt{true} and \qt{false}
    3.34 -  is not used for generated code, we use \isa{{\isasymCODERESERVED}}.
    3.35 -
    3.36 -  After this setup, code looks quite more readable:%
    3.37 -\end{isamarkuptext}%
    3.38 -\isamarkuptrue%
    3.39  \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
    3.40  \ in{\isacharunderscore}interval\ \ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}bool{\isacharunderscore}mlbool{\isachardot}ML{\isachardoublequoteclose}%
    3.41  \begin{isamarkuptext}%
     4.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/arbitrary.ML	Thu Jul 19 15:37:37 2007 +0200
     4.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/arbitrary.ML	Thu Jul 19 21:47:34 2007 +0200
     4.3 @@ -1,6 +1,3 @@
     4.4 -structure ROOT = 
     4.5 -struct
     4.6 -
     4.7  structure Codegen = 
     4.8  struct
     4.9  
    4.10 @@ -10,5 +7,3 @@
    4.11    | dummy_option (x :: xs) = SOME x;
    4.12  
    4.13  end; (*struct Codegen*)
    4.14 -
    4.15 -end; (*struct ROOT*)
     5.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML	Thu Jul 19 15:37:37 2007 +0200
     5.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML	Thu Jul 19 21:47:34 2007 +0200
     5.3 @@ -1,6 +1,3 @@
     5.4 -structure ROOT = 
     5.5 -struct
     5.6 -
     5.7  structure Nat = 
     5.8  struct
     5.9  
    5.10 @@ -20,5 +17,3 @@
    5.11    Nat.less_eq_nat k n andalso Nat.less_eq_nat n l;
    5.12  
    5.13  end; (*struct Codegen*)
    5.14 -
    5.15 -end; (*struct ROOT*)
     6.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML	Thu Jul 19 15:37:37 2007 +0200
     6.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML	Thu Jul 19 21:47:34 2007 +0200
     6.3 @@ -1,6 +1,3 @@
     6.4 -structure ROOT = 
     6.5 -struct
     6.6 -
     6.7  structure HOL = 
     6.8  struct
     6.9  
    6.10 @@ -32,5 +29,3 @@
    6.11    HOL.anda (Nat.less_eq_nat k n) (Nat.less_eq_nat n l);
    6.12  
    6.13  end; (*struct Codegen*)
    6.14 -
    6.15 -end; (*struct ROOT*)
     7.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_mlbool.ML	Thu Jul 19 15:37:37 2007 +0200
     7.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_mlbool.ML	Thu Jul 19 21:47:34 2007 +0200
     7.3 @@ -1,6 +1,3 @@
     7.4 -structure ROOT = 
     7.5 -struct
     7.6 -
     7.7  structure Nat = 
     7.8  struct
     7.9  
    7.10 @@ -20,5 +17,3 @@
    7.11    (Nat.less_eq_nat k n) andalso (Nat.less_eq_nat n l);
    7.12  
    7.13  end; (*struct Codegen*)
    7.14 -
    7.15 -end; (*struct ROOT*)
     8.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML	Thu Jul 19 15:37:37 2007 +0200
     8.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML	Thu Jul 19 21:47:34 2007 +0200
     8.3 @@ -1,6 +1,3 @@
     8.4 -structure ROOT = 
     8.5 -struct
     8.6 -
     8.7  structure Nat = 
     8.8  struct
     8.9  
    8.10 @@ -25,5 +22,3 @@
    8.11    head (null_optiona ()) [SOME (Nat.Suc Nat.Zero_nat), NONE];
    8.12  
    8.13  end; (*struct Codegen*)
    8.14 -
    8.15 -end; (*struct ROOT*)
     9.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml	Thu Jul 19 15:37:37 2007 +0200
     9.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml	Thu Jul 19 21:47:34 2007 +0200
     9.3 @@ -1,6 +1,3 @@
     9.4 -module ROOT = 
     9.5 -struct
     9.6 -
     9.7  module Nat = 
     9.8  struct
     9.9  
    9.10 @@ -25,5 +22,3 @@
    9.11    = head (null_optiona ()) [Some (Nat.Suc Nat.Zero_nat); None];;
    9.12  
    9.13  end;; (*struct Codegen*)
    9.14 -
    9.15 -end;; (*struct ROOT*)
    10.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML	Thu Jul 19 15:37:37 2007 +0200
    10.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML	Thu Jul 19 21:47:34 2007 +0200
    10.3 @@ -1,6 +1,3 @@
    10.4 -structure ROOT = 
    10.5 -struct
    10.6 -
    10.7  structure HOL = 
    10.8  struct
    10.9  
   10.10 @@ -12,8 +9,8 @@
   10.11  structure List = 
   10.12  struct
   10.13  
   10.14 -fun memberl A_ x (y :: ys) = HOL.eq A_ x y orelse memberl A_ x ys
   10.15 -  | memberl A_ x [] = false;
   10.16 +fun member A_ x (y :: ys) = HOL.eq A_ x y orelse member A_ x ys
   10.17 +  | member A_ x [] = false;
   10.18  
   10.19  end; (*struct List*)
   10.20  
   10.21 @@ -21,12 +18,10 @@
   10.22  struct
   10.23  
   10.24  fun collect_duplicates B_ xs ys (z :: zs) =
   10.25 -  (if List.memberl B_ z xs
   10.26 -    then (if List.memberl B_ z ys then collect_duplicates B_ xs ys zs
   10.27 +  (if List.member B_ z xs
   10.28 +    then (if List.member B_ z ys then collect_duplicates B_ xs ys zs
   10.29             else collect_duplicates B_ xs (z :: ys) zs)
   10.30      else collect_duplicates B_ (z :: xs) (z :: ys) zs)
   10.31    | collect_duplicates B_ xs ys [] = xs;
   10.32  
   10.33  end; (*struct Codegen*)
   10.34 -
   10.35 -end; (*struct ROOT*)
    11.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML	Thu Jul 19 15:37:37 2007 +0200
    11.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML	Thu Jul 19 21:47:34 2007 +0200
    11.3 @@ -1,6 +1,3 @@
    11.4 -structure ROOT = 
    11.5 -struct
    11.6 -
    11.7  structure Nat = 
    11.8  struct
    11.9  
   11.10 @@ -21,5 +18,3 @@
   11.11    | fac Nat.Zero_nat = Nat.Suc Nat.Zero_nat;
   11.12  
   11.13  end; (*struct Codegen*)
   11.14 -
   11.15 -end; (*struct ROOT*)
    12.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML	Thu Jul 19 15:37:37 2007 +0200
    12.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML	Thu Jul 19 21:47:34 2007 +0200
    12.3 @@ -1,6 +1,3 @@
    12.4 -structure ROOT = 
    12.5 -struct
    12.6 -
    12.7  structure Nat = 
    12.8  struct
    12.9  
   12.10 @@ -22,5 +19,3 @@
   12.11       | Nat.Suc m => Nat.times_nat n (fac m));
   12.12  
   12.13  end; (*struct Codegen*)
   12.14 -
   12.15 -end; (*struct ROOT*)
    13.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML	Thu Jul 19 15:37:37 2007 +0200
    13.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML	Thu Jul 19 21:47:34 2007 +0200
    13.3 @@ -1,6 +1,3 @@
    13.4 -structure ROOT = 
    13.5 -struct
    13.6 -
    13.7  structure HOL = 
    13.8  struct
    13.9  
   13.10 @@ -26,5 +23,3 @@
   13.11      HOL.eq A1_ x1 x2 andalso Orderings.less_eq B_ y1 y2;
   13.12  
   13.13  end; (*struct Codegen*)
   13.14 -
   13.15 -end; (*struct ROOT*)
    14.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML	Thu Jul 19 15:37:37 2007 +0200
    14.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML	Thu Jul 19 21:47:34 2007 +0200
    14.3 @@ -1,6 +1,3 @@
    14.4 -structure ROOT = 
    14.5 -struct
    14.6 -
    14.7  structure Nat = 
    14.8  struct
    14.9  
   14.10 @@ -52,5 +49,3 @@
   14.11      List.list_all2 eq_monotype typargs1 typargs2;
   14.12  
   14.13  end; (*struct Codegen*)
   14.14 -
   14.15 -end; (*struct ROOT*)
    15.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML	Thu Jul 19 15:37:37 2007 +0200
    15.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML	Thu Jul 19 21:47:34 2007 +0200
    15.3 @@ -1,6 +1,3 @@
    15.4 -structure ROOT = 
    15.5 -struct
    15.6 -
    15.7  structure Nat = 
    15.8  struct
    15.9  
   15.10 @@ -30,5 +27,3 @@
   15.11      end;
   15.12  
   15.13  end; (*struct Codegen*)
   15.14 -
   15.15 -end; (*struct ROOT*)
    16.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML	Thu Jul 19 15:37:37 2007 +0200
    16.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML	Thu Jul 19 21:47:34 2007 +0200
    16.3 @@ -1,6 +1,3 @@
    16.4 -structure ROOT = 
    16.5 -struct
    16.6 -
    16.7  structure Nat = 
    16.8  struct
    16.9  
   16.10 @@ -24,5 +21,3 @@
   16.11    (if Nat.less_nat n k then v else pick xs (Nat.minus_nat n k));
   16.12  
   16.13  end; (*struct Codegen*)
   16.14 -
   16.15 -end; (*struct ROOT*)
    17.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/set_list.ML	Thu Jul 19 15:37:37 2007 +0200
    17.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/set_list.ML	Thu Jul 19 21:47:34 2007 +0200
    17.3 @@ -1,6 +1,3 @@
    17.4 -structure ROOT = 
    17.5 -struct
    17.6 -
    17.7  structure HOL = 
    17.8  struct
    17.9  
   17.10 @@ -15,8 +12,8 @@
   17.11  fun foldr f (x :: xs) a = f x (foldr f xs a)
   17.12    | foldr f [] a = a;
   17.13  
   17.14 -fun memberl A_ x (y :: ys) = HOL.eq A_ x y orelse memberl A_ x ys
   17.15 -  | memberl A_ x [] = false;
   17.16 +fun member A_ x (y :: ys) = HOL.eq A_ x y orelse member A_ x ys
   17.17 +  | member A_ x [] = false;
   17.18  
   17.19  end; (*struct List*)
   17.20  
   17.21 @@ -33,8 +30,6 @@
   17.22  
   17.23  fun union (Set xs) = List.foldr uniona xs empty;
   17.24  
   17.25 -fun member A_ x (Set xs) = List.memberl A_ x xs;
   17.26 +fun member A_ x (Set xs) = List.member A_ x xs;
   17.27  
   17.28  end; (*struct Set*)
   17.29 -
   17.30 -end; (*struct ROOT*)
    18.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML	Thu Jul 19 15:37:37 2007 +0200
    18.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML	Thu Jul 19 21:47:34 2007 +0200
    18.3 @@ -1,6 +1,3 @@
    18.4 -structure ROOT = 
    18.5 -struct
    18.6 -
    18.7  structure HOL = 
    18.8  struct
    18.9  
   18.10 @@ -82,5 +79,3 @@
   18.11          (Leaf (Nat.Suc Nat.Zero_nat, []))));
   18.12  
   18.13  end; (*struct Codegen*)
   18.14 -
   18.15 -end; (*struct ROOT*)