--- a/NEWS Thu Jul 19 15:37:37 2007 +0200
+++ b/NEWS Thu Jul 19 21:47:34 2007 +0200
@@ -90,13 +90,13 @@
code for ML and Haskell (including "class"es). A short usage sketch:
internal compilation:
- code_gen <list of constants (term syntax)> (SML #)
+ code_gen <list of constants (term syntax)> in SML
writing SML code to a file:
- code_gen <list of constants (term syntax)> (SML <filename>)
+ code_gen <list of constants (term syntax)> in SML <filename>
writing OCaml code to a file:
- code_gen <list of constants (term syntax)> (OCaml <filename>)
+ code_gen <list of constants (term syntax)> in OCaml <filename>
writing Haskell code to a bunch of files:
- code_gen <list of constants (term syntax)> (Haskell <filename>)
+ code_gen <list of constants (term syntax)> in Haskell <filename>
Reasonable default setup of framework in HOL/Main.
@@ -541,6 +541,27 @@
*** HOL ***
+* Code generator library theories:
+ * Pretty_Int represents HOL integers by big integer literals in target
+ languages.
+ * Pretty_Char represents HOL characters by character literals in target
+ languages.
+ * Pretty_Char_chr like Pretty_Char, but also offers treatment of character
+ codes; includes Pretty_Int.
+ * Executable_Set allows to generate code for finite sets using lists.
+ * Executable_Rat implements rational numbers as triples (sign, enumerator,
+ denominator).
+ * Executable_Real implements a subset of real numbers, namly those
+ representable by rational numbers.
+ * Efficient_Nat implements natural numbers by integers, which in general will
+ result in higher efficency; pattern matching with 0/Suc is eliminated;
+ includes Pretty_Int.
+ * ML_String provides an additional datatype ml_string; in the HOL default
+ setup, strings in HOL are mapped to lists of HOL characters in SML; values
+ of type ml_string are mapped to strings in SML.
+ * ML_Int provides an additional datatype ml_int which is mapped to to SML
+ built-in integers.
+
* New package for inductive predicates
An n-ary predicate p with m parameters z_1, ..., z_m can now be defined via
--- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Thu Jul 19 15:37:37 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Thu Jul 19 21:47:34 2007 +0200
@@ -469,17 +469,17 @@
\item[@{text "Pretty_Char_chr"}] like @{text "Pretty_Char"},
but also offers treatment of character codes; includes
@{text "Pretty_Int"}.
- \item[@{text "ExecutableSet"}] allows to generate code
+ \item[@{text "Executable_Set"}] allows to generate code
for finite sets using lists.
- \item[@{text "ExecutableRat"}] \label{exec_rat} implements rational
+ \item[@{text "Executable_Rat"}] \label{exec_rat} implements rational
numbers as triples @{text "(sign, enumerator, denominator)"}.
\item[@{text "Executable_Real"}] implements a subset of real numbers,
namly those representable by rational numbers.
- \item[@{text "EfficientNat"}] \label{eff_nat} implements natural numbers by integers,
+ \item[@{text "Efficient_Nat"}] \label{eff_nat} implements natural numbers by integers,
which in general will result in higher efficency; pattern
matching with @{const "0\<Colon>nat"} / @{const "Suc"}
is eliminated; includes @{text "Pretty_Int"}.
- \item[@{text "MLString"}] provides an additional datatype @{text "mlstring"};
+ \item[@{text "ML_String"}] provides an additional datatype @{text "mlstring"};
in the @{text HOL} default setup, strings in HOL are mapped to list
of @{text HOL} characters in SML; values of type @{text "mlstring"} are
mapped to strings in SML.
@@ -592,7 +592,7 @@
text {*
The membership test during preprocessing is rewritten,
- resulting in @{const List.memberl}, which itself
+ resulting in @{const List.member}, which itself
performs an explicit equality check.
*}
@@ -804,16 +804,6 @@
for the type constructor's (the constant's) arguments.
*}
-code_reserved SML
- bool true false
-
-text {*
- To assert that the existing \qt{bool}, \qt{true} and \qt{false}
- is not used for generated code, we use @{text "\<CODERESERVED>"}.
-
- After this setup, code looks quite more readable:
-*}
-
code_gen in_interval (*<*)in SML(*>*) in SML file "examples/bool_mlbool.ML"
text {*
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Thu Jul 19 15:37:37 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Thu Jul 19 21:47:34 2007 +0200
@@ -590,17 +590,17 @@
\item[\isa{Pretty{\isacharunderscore}Char{\isacharunderscore}chr}] like \isa{Pretty{\isacharunderscore}Char},
but also offers treatment of character codes; includes
\isa{Pretty{\isacharunderscore}Int}.
- \item[\isa{ExecutableSet}] allows to generate code
+ \item[\isa{Executable{\isacharunderscore}Set}] allows to generate code
for finite sets using lists.
- \item[\isa{ExecutableRat}] \label{exec_rat} implements rational
+ \item[\isa{Executable{\isacharunderscore}Rat}] \label{exec_rat} implements rational
numbers as triples \isa{{\isacharparenleft}sign{\isacharcomma}\ enumerator{\isacharcomma}\ denominator{\isacharparenright}}.
\item[\isa{Executable{\isacharunderscore}Real}] implements a subset of real numbers,
namly those representable by rational numbers.
- \item[\isa{EfficientNat}] \label{eff_nat} implements natural numbers by integers,
+ \item[\isa{Efficient{\isacharunderscore}Nat}] \label{eff_nat} implements natural numbers by integers,
which in general will result in higher efficency; pattern
matching with \isa{{\isadigit{0}}} / \isa{Suc}
is eliminated; includes \isa{Pretty{\isacharunderscore}Int}.
- \item[\isa{MLString}] provides an additional datatype \isa{mlstring};
+ \item[\isa{ML{\isacharunderscore}String}] provides an additional datatype \isa{mlstring};
in the \isa{HOL} default setup, strings in HOL are mapped to list
of \isa{HOL} characters in SML; values of type \isa{mlstring} are
mapped to strings in SML.
@@ -1086,16 +1086,6 @@
for the type constructor's (the constant's) arguments.%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{code{\isacharunderscore}reserved}\isamarkupfalse%
-\ SML\isanewline
-\ \ bool\ true\ false%
-\begin{isamarkuptext}%
-To assert that the existing \qt{bool}, \qt{true} and \qt{false}
- is not used for generated code, we use \isa{{\isasymCODERESERVED}}.
-
- After this setup, code looks quite more readable:%
-\end{isamarkuptext}%
-\isamarkuptrue%
\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
\ in{\isacharunderscore}interval\ \ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}bool{\isacharunderscore}mlbool{\isachardot}ML{\isachardoublequoteclose}%
\begin{isamarkuptext}%
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/arbitrary.ML Thu Jul 19 15:37:37 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/arbitrary.ML Thu Jul 19 21:47:34 2007 +0200
@@ -1,6 +1,3 @@
-structure ROOT =
-struct
-
structure Codegen =
struct
@@ -10,5 +7,3 @@
| dummy_option (x :: xs) = SOME x;
end; (*struct Codegen*)
-
-end; (*struct ROOT*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML Thu Jul 19 15:37:37 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML Thu Jul 19 21:47:34 2007 +0200
@@ -1,6 +1,3 @@
-structure ROOT =
-struct
-
structure Nat =
struct
@@ -20,5 +17,3 @@
Nat.less_eq_nat k n andalso Nat.less_eq_nat n l;
end; (*struct Codegen*)
-
-end; (*struct ROOT*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML Thu Jul 19 15:37:37 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML Thu Jul 19 21:47:34 2007 +0200
@@ -1,6 +1,3 @@
-structure ROOT =
-struct
-
structure HOL =
struct
@@ -32,5 +29,3 @@
HOL.anda (Nat.less_eq_nat k n) (Nat.less_eq_nat n l);
end; (*struct Codegen*)
-
-end; (*struct ROOT*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_mlbool.ML Thu Jul 19 15:37:37 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_mlbool.ML Thu Jul 19 21:47:34 2007 +0200
@@ -1,6 +1,3 @@
-structure ROOT =
-struct
-
structure Nat =
struct
@@ -20,5 +17,3 @@
(Nat.less_eq_nat k n) andalso (Nat.less_eq_nat n l);
end; (*struct Codegen*)
-
-end; (*struct ROOT*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML Thu Jul 19 15:37:37 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML Thu Jul 19 21:47:34 2007 +0200
@@ -1,6 +1,3 @@
-structure ROOT =
-struct
-
structure Nat =
struct
@@ -25,5 +22,3 @@
head (null_optiona ()) [SOME (Nat.Suc Nat.Zero_nat), NONE];
end; (*struct Codegen*)
-
-end; (*struct ROOT*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml Thu Jul 19 15:37:37 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml Thu Jul 19 21:47:34 2007 +0200
@@ -1,6 +1,3 @@
-module ROOT =
-struct
-
module Nat =
struct
@@ -25,5 +22,3 @@
= head (null_optiona ()) [Some (Nat.Suc Nat.Zero_nat); None];;
end;; (*struct Codegen*)
-
-end;; (*struct ROOT*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML Thu Jul 19 15:37:37 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML Thu Jul 19 21:47:34 2007 +0200
@@ -1,6 +1,3 @@
-structure ROOT =
-struct
-
structure HOL =
struct
@@ -12,8 +9,8 @@
structure List =
struct
-fun memberl A_ x (y :: ys) = HOL.eq A_ x y orelse memberl A_ x ys
- | memberl A_ x [] = false;
+fun member A_ x (y :: ys) = HOL.eq A_ x y orelse member A_ x ys
+ | member A_ x [] = false;
end; (*struct List*)
@@ -21,12 +18,10 @@
struct
fun collect_duplicates B_ xs ys (z :: zs) =
- (if List.memberl B_ z xs
- then (if List.memberl B_ z ys then collect_duplicates B_ xs ys zs
+ (if List.member B_ z xs
+ then (if List.member B_ z ys then collect_duplicates B_ xs ys zs
else collect_duplicates B_ xs (z :: ys) zs)
else collect_duplicates B_ (z :: xs) (z :: ys) zs)
| collect_duplicates B_ xs ys [] = xs;
end; (*struct Codegen*)
-
-end; (*struct ROOT*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML Thu Jul 19 15:37:37 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML Thu Jul 19 21:47:34 2007 +0200
@@ -1,6 +1,3 @@
-structure ROOT =
-struct
-
structure Nat =
struct
@@ -21,5 +18,3 @@
| fac Nat.Zero_nat = Nat.Suc Nat.Zero_nat;
end; (*struct Codegen*)
-
-end; (*struct ROOT*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML Thu Jul 19 15:37:37 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML Thu Jul 19 21:47:34 2007 +0200
@@ -1,6 +1,3 @@
-structure ROOT =
-struct
-
structure Nat =
struct
@@ -22,5 +19,3 @@
| Nat.Suc m => Nat.times_nat n (fac m));
end; (*struct Codegen*)
-
-end; (*struct ROOT*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML Thu Jul 19 15:37:37 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML Thu Jul 19 21:47:34 2007 +0200
@@ -1,6 +1,3 @@
-structure ROOT =
-struct
-
structure HOL =
struct
@@ -26,5 +23,3 @@
HOL.eq A1_ x1 x2 andalso Orderings.less_eq B_ y1 y2;
end; (*struct Codegen*)
-
-end; (*struct ROOT*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML Thu Jul 19 15:37:37 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML Thu Jul 19 21:47:34 2007 +0200
@@ -1,6 +1,3 @@
-structure ROOT =
-struct
-
structure Nat =
struct
@@ -52,5 +49,3 @@
List.list_all2 eq_monotype typargs1 typargs2;
end; (*struct Codegen*)
-
-end; (*struct ROOT*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML Thu Jul 19 15:37:37 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML Thu Jul 19 21:47:34 2007 +0200
@@ -1,6 +1,3 @@
-structure ROOT =
-struct
-
structure Nat =
struct
@@ -30,5 +27,3 @@
end;
end; (*struct Codegen*)
-
-end; (*struct ROOT*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML Thu Jul 19 15:37:37 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML Thu Jul 19 21:47:34 2007 +0200
@@ -1,6 +1,3 @@
-structure ROOT =
-struct
-
structure Nat =
struct
@@ -24,5 +21,3 @@
(if Nat.less_nat n k then v else pick xs (Nat.minus_nat n k));
end; (*struct Codegen*)
-
-end; (*struct ROOT*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/set_list.ML Thu Jul 19 15:37:37 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/set_list.ML Thu Jul 19 21:47:34 2007 +0200
@@ -1,6 +1,3 @@
-structure ROOT =
-struct
-
structure HOL =
struct
@@ -15,8 +12,8 @@
fun foldr f (x :: xs) a = f x (foldr f xs a)
| foldr f [] a = a;
-fun memberl A_ x (y :: ys) = HOL.eq A_ x y orelse memberl A_ x ys
- | memberl A_ x [] = false;
+fun member A_ x (y :: ys) = HOL.eq A_ x y orelse member A_ x ys
+ | member A_ x [] = false;
end; (*struct List*)
@@ -33,8 +30,6 @@
fun union (Set xs) = List.foldr uniona xs empty;
-fun member A_ x (Set xs) = List.memberl A_ x xs;
+fun member A_ x (Set xs) = List.member A_ x xs;
end; (*struct Set*)
-
-end; (*struct ROOT*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML Thu Jul 19 15:37:37 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML Thu Jul 19 21:47:34 2007 +0200
@@ -1,6 +1,3 @@
-structure ROOT =
-struct
-
structure HOL =
struct
@@ -82,5 +79,3 @@
(Leaf (Nat.Suc Nat.Zero_nat, []))));
end; (*struct Codegen*)
-
-end; (*struct ROOT*)