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*)