# HG changeset patch # User haftmann # Date 1184874454 -7200 # Node ID f1434532a562fd06d67bfd0124cc8b8d4b07e37a # Parent 2a0e24c74593e0bde5210754ed953eba01fd7075 updated diff -r 2a0e24c74593 -r f1434532a562 NEWS --- 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 (SML #) + code_gen in SML writing SML code to a file: - code_gen (SML ) + code_gen in SML writing OCaml code to a file: - code_gen (OCaml ) + code_gen in OCaml writing Haskell code to a bunch of files: - code_gen (Haskell ) + code_gen in Haskell 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 diff -r 2a0e24c74593 -r f1434532a562 doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy --- 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\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 "\"}. - - After this setup, code looks quite more readable: -*} - code_gen in_interval (*<*)in SML(*>*) in SML file "examples/bool_mlbool.ML" text {* diff -r 2a0e24c74593 -r f1434532a562 doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex --- 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}% diff -r 2a0e24c74593 -r f1434532a562 doc-src/IsarAdvanced/Codegen/Thy/examples/arbitrary.ML --- 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*) diff -r 2a0e24c74593 -r f1434532a562 doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML --- 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*) diff -r 2a0e24c74593 -r f1434532a562 doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML --- 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*) diff -r 2a0e24c74593 -r f1434532a562 doc-src/IsarAdvanced/Codegen/Thy/examples/bool_mlbool.ML --- 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*) diff -r 2a0e24c74593 -r f1434532a562 doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML --- 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*) diff -r 2a0e24c74593 -r f1434532a562 doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml --- 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*) diff -r 2a0e24c74593 -r f1434532a562 doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML --- 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*) diff -r 2a0e24c74593 -r f1434532a562 doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML --- 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*) diff -r 2a0e24c74593 -r f1434532a562 doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML --- 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*) diff -r 2a0e24c74593 -r f1434532a562 doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML --- 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*) diff -r 2a0e24c74593 -r f1434532a562 doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML --- 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*) diff -r 2a0e24c74593 -r f1434532a562 doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML --- 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*) diff -r 2a0e24c74593 -r f1434532a562 doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML --- 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*) diff -r 2a0e24c74593 -r f1434532a562 doc-src/IsarAdvanced/Codegen/Thy/examples/set_list.ML --- 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*) diff -r 2a0e24c74593 -r f1434532a562 doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML --- 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*)