# HG changeset patch # User haftmann # Date 1187957657 -7200 # Node ID acfb2413faa39522df841ef1c9fea129b828cd69 # Parent 9fa337721689b80b5d2123a159cf79c310fbc0fd updated diff -r 9fa337721689 -r acfb2413faa3 doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy --- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Fri Aug 24 14:14:16 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Fri Aug 24 14:14:17 2007 +0200 @@ -469,8 +469,6 @@ \item[@{text "Pretty_Char_chr"}] like @{text "Pretty_Char"}, but also offers treatment of character codes; includes @{text "Pretty_Int"}. - \item[@{text "Executable_Set"}] allows to generate code - for finite sets using lists. \item[@{text "Executable_Rat"}] implements rational numbers. \item[@{text "Executable_Real"}] implements a subset of real numbers, @@ -935,7 +933,7 @@ how to implement finite sets by lists using the conversion @{term [source] "set \ 'a list \ 'a set"} as constructor: -*} +*} (*<*)ML {* nonfix union *} lemmas [code func del] = in_code union_empty1 union_empty2 union_insert Union_code(*>*) code_datatype set @@ -1018,35 +1016,6 @@ description of the most important ML interfaces. *} -subsection {* Basics: @{text CodeUnit} *} - -text {* - This module provides identification of (probably overloaded) - constants by unique identifiers. -*} - -text %mlref {* - \begin{mldecls} - @{index_ML_type CodeUnit.const: "string * string option"} \\ - @{index_ML CodeUnit.const_of_cexpr: "theory -> string * typ -> CodeUnit.const"} \\ - \end{mldecls} - - \begin{description} - - \item @{ML_type CodeUnit.const} is the identifier type: - the product of a \emph{string} with a list of \emph{typs}. - The \emph{string} is the constant name as represented inside Isabelle; - for overloaded constants, the attached \emph{string option} - is either @{text SOME} type constructor denoting an instance, - or @{text NONE} for the polymorphic constant. - - \item @{ML CodeUnit.const_of_cexpr}~@{text thy}~@{text "(constname, typ)"} - maps a constant expression @{text "(constname, typ)"} - to its canonical identifier. - - \end{description} -*} - subsection {* Executable theory content: @{text Code} *} text {* @@ -1060,7 +1029,7 @@ \begin{mldecls} @{index_ML Code.add_func: "bool -> thm -> theory -> theory"} \\ @{index_ML Code.del_func: "thm -> theory -> theory"} \\ - @{index_ML Code.add_funcl: "CodeUnit.const * thm list Susp.T -> theory -> theory"} \\ + @{index_ML Code.add_funcl: "string * thm list Susp.T -> theory -> theory"} \\ @{index_ML Code.add_inline: "thm -> theory -> theory"} \\ @{index_ML Code.del_inline: "thm -> theory -> theory"} \\ @{index_ML Code.add_inline_proc: "string * (theory -> cterm list -> thm list) @@ -1069,11 +1038,10 @@ @{index_ML Code.add_preproc: "string * (theory -> thm list -> thm list) -> theory -> theory"} \\ @{index_ML Code.del_preproc: "string -> theory -> theory"} \\ - @{index_ML Code.add_datatype: "string * ((string * sort) list * (string * typ list) list) - -> theory -> theory"} \\ + @{index_ML Code.add_datatype: "(string * typ) list -> theory -> theory"} \\ @{index_ML Code.get_datatype: "theory -> string -> (string * sort) list * (string * typ list) list"} \\ - @{index_ML Code.get_datatype_of_constr: "theory -> CodeUnit.const -> string option"} + @{index_ML Code.get_datatype_of_constr: "theory -> string -> string option"} \end{mldecls} \begin{description} @@ -1113,12 +1081,9 @@ \item @{ML Code.del_preproc}~@{text "name"}~@{text "thy"} removes generic preprcoessor named @{text name} from executable content. - \item @{ML Code.add_datatype}~@{text "(name, spec)"}~@{text "thy"} adds - a datatype to executable content, with type constructor - @{text name} and specification @{text spec}; @{text spec} is - a pair consisting of a list of type variable with sort - constraints and a list of constructors with name - and types of arguments. + \item @{ML Code.add_datatype}~@{text cs}~@{text thy} adds + a datatype to executable content, with generation + set @{text cs}. \item @{ML Code.get_datatype_of_constr}~@{text "thy"}~@{text "const"} returns type constructor corresponding to @@ -1132,22 +1097,13 @@ text %mlref {* \begin{mldecls} - @{index_ML CodeUnit.const_ord: "CodeUnit.const * CodeUnit.const -> order"} \\ - @{index_ML CodeUnit.eq_const: "CodeUnit.const * CodeUnit.const -> bool"} \\ - @{index_ML CodeUnit.read_const: "theory -> string -> CodeUnit.const"} \\ - @{index_ML_structure CodeUnit.Consttab} \\ - @{index_ML CodeUnit.head_func: "thm -> CodeUnit.const * typ"} \\ + @{index_ML CodeUnit.read_const: "theory -> string -> string"} \\ + @{index_ML CodeUnit.head_func: "thm -> string * typ"} \\ @{index_ML CodeUnit.rewrite_func: "thm list -> thm -> thm"} \\ \end{mldecls} \begin{description} - \item @{ML CodeUnit.const_ord},~@{ML CodeUnit.eq_const} - provide order and equality on constant identifiers. - - \item @{ML_struct CodeUnit.Consttab} - provides table structures with constant identifiers as keys. - \item @{ML CodeUnit.read_const}~@{text thy}~@{text s} reads a constant as a concrete term expression @{text s}. diff -r 9fa337721689 -r acfb2413faa3 doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Fri Aug 24 14:14:16 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Fri Aug 24 14:14:17 2007 +0200 @@ -590,8 +590,6 @@ \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{Executable{\isacharunderscore}Set}] allows to generate code - for finite sets using lists. \item[\isa{Executable{\isacharunderscore}Rat}] implements rational numbers. \item[\isa{Executable{\isacharunderscore}Real}] implements a subset of real numbers, @@ -1304,6 +1302,20 @@ as constructor:% \end{isamarkuptext}% \isamarkuptrue% +\ % +\isadelimML +% +\endisadelimML +% +\isatagML +% +\endisatagML +{\isafoldML}% +% +\isadelimML +% +\endisadelimML +\isanewline \isacommand{code{\isacharunderscore}datatype}\isamarkupfalse% \ set\isanewline \isanewline @@ -1473,52 +1485,6 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isamarkupsubsection{Basics: \isa{CodeUnit}% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -This module provides identification of (probably overloaded) - constants by unique identifiers.% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimmlref -% -\endisadelimmlref -% -\isatagmlref -% -\begin{isamarkuptext}% -\begin{mldecls} - \indexmltype{CodeUnit.const}\verb|type CodeUnit.const = string * string option| \\ - \indexml{CodeUnit.const-of-cexpr}\verb|CodeUnit.const_of_cexpr: theory -> string * typ -> CodeUnit.const| \\ - \end{mldecls} - - \begin{description} - - \item \verb|CodeUnit.const| is the identifier type: - the product of a \emph{string} with a list of \emph{typs}. - The \emph{string} is the constant name as represented inside Isabelle; - for overloaded constants, the attached \emph{string option} - is either \isa{SOME} type constructor denoting an instance, - or \isa{NONE} for the polymorphic constant. - - \item \verb|CodeUnit.const_of_cexpr|~\isa{thy}~\isa{{\isacharparenleft}constname{\isacharcomma}\ typ{\isacharparenright}} - maps a constant expression \isa{{\isacharparenleft}constname{\isacharcomma}\ typ{\isacharparenright}} - to its canonical identifier. - - \end{description}% -\end{isamarkuptext}% -\isamarkuptrue% -% -\endisatagmlref -{\isafoldmlref}% -% -\isadelimmlref -% -\endisadelimmlref -% \isamarkupsubsection{Executable theory content: \isa{Code}% } \isamarkuptrue% @@ -1543,7 +1509,7 @@ \begin{mldecls} \indexml{Code.add-func}\verb|Code.add_func: bool -> thm -> theory -> theory| \\ \indexml{Code.del-func}\verb|Code.del_func: thm -> theory -> theory| \\ - \indexml{Code.add-funcl}\verb|Code.add_funcl: CodeUnit.const * thm list Susp.T -> theory -> theory| \\ + \indexml{Code.add-funcl}\verb|Code.add_funcl: string * thm list Susp.T -> theory -> theory| \\ \indexml{Code.add-inline}\verb|Code.add_inline: thm -> theory -> theory| \\ \indexml{Code.del-inline}\verb|Code.del_inline: thm -> theory -> theory| \\ \indexml{Code.add-inline-proc}\verb|Code.add_inline_proc: string * (theory -> cterm list -> thm list)|\isasep\isanewline% @@ -1552,11 +1518,10 @@ \indexml{Code.add-preproc}\verb|Code.add_preproc: string * (theory -> thm list -> thm list)|\isasep\isanewline% \verb| -> theory -> theory| \\ \indexml{Code.del-preproc}\verb|Code.del_preproc: string -> theory -> theory| \\ - \indexml{Code.add-datatype}\verb|Code.add_datatype: string * ((string * sort) list * (string * typ list) list)|\isasep\isanewline% -\verb| -> theory -> theory| \\ + \indexml{Code.add-datatype}\verb|Code.add_datatype: (string * typ) list -> theory -> theory| \\ \indexml{Code.get-datatype}\verb|Code.get_datatype: theory -> string|\isasep\isanewline% \verb| -> (string * sort) list * (string * typ list) list| \\ - \indexml{Code.get-datatype-of-constr}\verb|Code.get_datatype_of_constr: theory -> CodeUnit.const -> string option| + \indexml{Code.get-datatype-of-constr}\verb|Code.get_datatype_of_constr: theory -> string -> string option| \end{mldecls} \begin{description} @@ -1596,12 +1561,9 @@ \item \verb|Code.del_preproc|~\isa{name}~\isa{thy} removes generic preprcoessor named \isa{name} from executable content. - \item \verb|Code.add_datatype|~\isa{{\isacharparenleft}name{\isacharcomma}\ spec{\isacharparenright}}~\isa{thy} adds - a datatype to executable content, with type constructor - \isa{name} and specification \isa{spec}; \isa{spec} is - a pair consisting of a list of type variable with sort - constraints and a list of constructors with name - and types of arguments. + \item \verb|Code.add_datatype|~\isa{cs}~\isa{thy} adds + a datatype to executable content, with generation + set \isa{cs}. \item \verb|Code.get_datatype_of_constr|~\isa{thy}~\isa{const} returns type constructor corresponding to @@ -1631,22 +1593,13 @@ % \begin{isamarkuptext}% \begin{mldecls} - \indexml{CodeUnit.const-ord}\verb|CodeUnit.const_ord: CodeUnit.const * CodeUnit.const -> order| \\ - \indexml{CodeUnit.eq-const}\verb|CodeUnit.eq_const: CodeUnit.const * CodeUnit.const -> bool| \\ - \indexml{CodeUnit.read-const}\verb|CodeUnit.read_const: theory -> string -> CodeUnit.const| \\ - \indexmlstructure{CodeUnit.Consttab}\verb|structure CodeUnit.Consttab| \\ - \indexml{CodeUnit.head-func}\verb|CodeUnit.head_func: thm -> CodeUnit.const * typ| \\ + \indexml{CodeUnit.read-const}\verb|CodeUnit.read_const: theory -> string -> string| \\ + \indexml{CodeUnit.head-func}\verb|CodeUnit.head_func: thm -> string * typ| \\ \indexml{CodeUnit.rewrite-func}\verb|CodeUnit.rewrite_func: thm list -> thm -> thm| \\ \end{mldecls} \begin{description} - \item \verb|CodeUnit.const_ord|,~\verb|CodeUnit.eq_const| - provide order and equality on constant identifiers. - - \item \verb|CodeUnit.Consttab| - provides table structures with constant identifiers as keys. - \item \verb|CodeUnit.read_const|~\isa{thy}~\isa{s} reads a constant as a concrete term expression \isa{s}. diff -r 9fa337721689 -r acfb2413faa3 doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs Fri Aug 24 14:14:16 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs Fri Aug 24 14:14:17 2007 +0200 @@ -10,11 +10,8 @@ heada (x : xs) = x; heada [] = Codegen.nulla; -null_option :: Maybe a; -null_option = Nothing; - instance Codegen.Null (Maybe b) where { - nulla = Codegen.null_option; + nulla = Nothing; }; dummy :: Maybe Nat.Nat; diff -r 9fa337721689 -r acfb2413faa3 doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML Fri Aug 24 14:14:16 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML Fri Aug 24 14:14:17 2007 +0200 @@ -1,7 +1,7 @@ structure Nat = struct -datatype nat = Zero_nat | Suc of nat; +datatype nat = Suc of nat | Zero_nat; fun less_nat n (Suc m) = less_eq_nat n m | less_nat n Zero_nat = false diff -r 9fa337721689 -r acfb2413faa3 doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML Fri Aug 24 14:14:16 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML Fri Aug 24 14:14:17 2007 +0200 @@ -1,7 +1,7 @@ structure HOL = struct -datatype boola = True | False; +datatype boola = False | True; fun anda x True = x | anda x False = False @@ -13,7 +13,7 @@ structure Nat = struct -datatype nat = Zero_nat | Suc of nat; +datatype nat = Suc of nat | Zero_nat; fun less_nat n (Suc m) = less_eq_nat n m | less_nat n Zero_nat = HOL.False diff -r 9fa337721689 -r acfb2413faa3 doc-src/IsarAdvanced/Codegen/Thy/examples/bool_mlbool.ML --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_mlbool.ML Fri Aug 24 14:14:16 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_mlbool.ML Fri Aug 24 14:14:17 2007 +0200 @@ -1,7 +1,7 @@ structure Nat = struct -datatype nat = Zero_nat | Suc of nat; +datatype nat = Suc of nat | Zero_nat; fun less_nat n (Suc m) = less_eq_nat n m | less_nat n Zero_nat = false diff -r 9fa337721689 -r acfb2413faa3 doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML Fri Aug 24 14:14:16 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML Fri Aug 24 14:14:17 2007 +0200 @@ -1,7 +1,7 @@ structure Nat = struct -datatype nat = Zero_nat | Suc of nat; +datatype nat = Suc of nat | Zero_nat; end; (*struct Nat*) @@ -14,11 +14,9 @@ fun head B_ (x :: xs) = x | head B_ [] = null B_; -val null_option : 'a option = NONE; - -fun null_optiona () = {null = null_option} : ('b option) null; +fun null_option () = {null = NONE} : ('b option) null; val dummy : Nat.nat option = - head (null_optiona ()) [SOME (Nat.Suc Nat.Zero_nat), NONE]; + head (null_option ()) [SOME (Nat.Suc Nat.Zero_nat), NONE]; end; (*struct Codegen*) diff -r 9fa337721689 -r acfb2413faa3 doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml Fri Aug 24 14:14:16 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml Fri Aug 24 14:14:17 2007 +0200 @@ -1,7 +1,7 @@ module Nat = struct -type nat = Zero_nat | Suc of nat;; +type nat = Suc of nat | Zero_nat;; end;; (*struct Nat*) @@ -14,11 +14,9 @@ let rec head _B = function x :: xs -> x | [] -> null _B;; -let rec null_option = None;; - -let null_optiona () = ({null = null_option} : ('b option) null);; +let null_option () = ({null = None} : ('b option) null);; let rec dummy - = head (null_optiona ()) [Some (Nat.Suc Nat.Zero_nat); None];; + = head (null_option ()) [Some (Nat.Suc Nat.Zero_nat); None];; end;; (*struct Codegen*) diff -r 9fa337721689 -r acfb2413faa3 doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML Fri Aug 24 14:14:16 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML Fri Aug 24 14:14:17 2007 +0200 @@ -1,15 +1,15 @@ structure HOL = struct -type 'a eq = {eq : 'a -> 'a -> bool}; -fun eq (A_:'a eq) = #eq A_; +type 'a eq = {eqop : 'a -> 'a -> bool}; +fun eqop (A_:'a eq) = #eqop A_; end; (*struct HOL*) structure List = struct -fun member A_ x (y :: ys) = HOL.eq A_ x y orelse member A_ x ys +fun member A_ x (y :: ys) = HOL.eqop A_ x y orelse member A_ x ys | member A_ x [] = false; end; (*struct List*) diff -r 9fa337721689 -r acfb2413faa3 doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML Fri Aug 24 14:14:16 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML Fri Aug 24 14:14:17 2007 +0200 @@ -1,7 +1,7 @@ structure Nat = struct -datatype nat = Zero_nat | Suc of nat; +datatype nat = Suc of nat | Zero_nat; fun plus_nat (Suc m) n = plus_nat m (Suc n) | plus_nat Zero_nat n = n; diff -r 9fa337721689 -r acfb2413faa3 doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML Fri Aug 24 14:14:16 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML Fri Aug 24 14:14:17 2007 +0200 @@ -1,7 +1,7 @@ structure Nat = struct -datatype nat = Zero_nat | Suc of nat; +datatype nat = Suc of nat | Zero_nat; fun nat_case f1 f2 Zero_nat = f1 | nat_case f1 f2 (Suc nat) = f2 nat; diff -r 9fa337721689 -r acfb2413faa3 doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML Fri Aug 24 14:14:16 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML Fri Aug 24 14:14:17 2007 +0200 @@ -1,8 +1,8 @@ structure HOL = struct -type 'a eq = {eq : 'a -> 'a -> bool}; -fun eq (A_:'a eq) = #eq A_; +type 'a eq = {eqop : 'a -> 'a -> bool}; +fun eqop (A_:'a eq) = #eqop A_; type 'a ord = {less_eq : 'a -> 'a -> bool, less : 'a -> 'a -> bool}; fun less_eq (A_:'a ord) = #less_eq A_; @@ -13,7 +13,8 @@ structure Codegen = struct -fun less_eq_product (A1_, A2_) B_ (x1, y1) (x2, y2) = - HOL.less A2_ x1 x2 orelse HOL.eq A1_ x1 x2 andalso HOL.less_eq B_ y1 y2; +fun less_eq (A1_, A2_) B_ (x1, y1) (x2, y2) = + HOL.less A2_ x1 x2 orelse + HOL.eqop A1_ x1 x2 andalso HOL.less_eq B_ y1 y2; end; (*struct Codegen*) diff -r 9fa337721689 -r acfb2413faa3 doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML Fri Aug 24 14:14:16 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML Fri Aug 24 14:14:17 2007 +0200 @@ -1,12 +1,12 @@ structure Nat = struct -datatype nat = Zero_nat | Suc of nat; +datatype nat = Suc of nat | Zero_nat; -fun eq_nat Zero_nat (Suc m) = false - | eq_nat (Suc n) Zero_nat = false - | eq_nat (Suc n) (Suc m) = eq_nat n m - | eq_nat Zero_nat Zero_nat = true; +fun eqop_nat Zero_nat (Suc m) = false + | eqop_nat (Suc n) Zero_nat = false + | eqop_nat (Suc n) (Suc m) = eqop_nat n m + | eqop_nat Zero_nat Zero_nat = true; fun plus_nat (Suc m) n = plus_nat m (Suc n) | plus_nat Zero_nat n = n; @@ -39,7 +39,7 @@ | list_all2 p xs [] = null xs | list_all2 p [] ys = null ys | list_all2 p xs ys = - Nat.eq_nat (size_list xs) (size_list ys) andalso + Nat.eqop_nat (size_list xs) (size_list ys) andalso list_all (fn a as (aa, b) => p aa b) (zip xs ys); end; (*struct List*) @@ -49,8 +49,8 @@ datatype monotype = Mono of Nat.nat * monotype list; -fun eq_monotype (Mono (tyco1, typargs1)) (Mono (tyco2, typargs2)) = - Nat.eq_nat tyco1 tyco2 andalso - List.list_all2 eq_monotype typargs1 typargs2; +fun eqop_monotype (Mono (tyco1, typargs1)) (Mono (tyco2, typargs2)) = + Nat.eqop_nat tyco1 tyco2 andalso + List.list_all2 eqop_monotype typargs1 typargs2; end; (*struct Codegen*) diff -r 9fa337721689 -r acfb2413faa3 doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML Fri Aug 24 14:14:16 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML Fri Aug 24 14:14:17 2007 +0200 @@ -8,7 +8,7 @@ structure Nat = struct -datatype nat = Zero_nat | Suc of nat; +datatype nat = Suc of nat | Zero_nat; fun less_nat n (Suc m) = less_eq_nat n m | less_nat n Zero_nat = false diff -r 9fa337721689 -r acfb2413faa3 doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML Fri Aug 24 14:14:16 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML Fri Aug 24 14:14:17 2007 +0200 @@ -1,7 +1,7 @@ structure Nat = struct -datatype nat = Zero_nat | Suc of nat; +datatype nat = Suc of nat | Zero_nat; fun less_nat n (Suc m) = less_eq_nat n m | less_nat n Zero_nat = false diff -r 9fa337721689 -r acfb2413faa3 doc-src/IsarAdvanced/Codegen/Thy/examples/set_list.ML --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/set_list.ML Fri Aug 24 14:14:16 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/set_list.ML Fri Aug 24 14:14:17 2007 +0200 @@ -1,8 +1,8 @@ structure HOL = struct -type 'a eq = {eq : 'a -> 'a -> bool}; -fun eq (A_:'a eq) = #eq A_; +type 'a eq = {eqop : 'a -> 'a -> bool}; +fun eqop (A_:'a eq) = #eqop A_; end; (*struct HOL*) @@ -12,7 +12,7 @@ fun foldr f (x :: xs) a = f x (foldr f xs a) | foldr f [] a = a; -fun member A_ x (y :: ys) = HOL.eq A_ x y orelse member A_ x ys +fun member A_ x (y :: ys) = HOL.eqop A_ x y orelse member A_ x ys | member A_ x [] = false; end; (*struct List*) @@ -26,10 +26,10 @@ fun insert x (Set xs) = Set (x :: xs); -fun uniona xs (Set ys) = List.foldr insert ys xs; - -fun union (Set xs) = List.foldr uniona xs empty; +fun union xs (Set ys) = List.foldr insert ys xs; fun member A_ x (Set xs) = List.member A_ x xs; +fun uniona (Set xs) = List.foldr union xs empty; + end; (*struct Set*) diff -r 9fa337721689 -r acfb2413faa3 doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML Fri Aug 24 14:14:16 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML Fri Aug 24 14:14:17 2007 +0200 @@ -1,8 +1,8 @@ structure HOL = struct -type 'a eq = {eq : 'a -> 'a -> bool}; -fun eq (A_:'a eq) = #eq A_; +type 'a eq = {eqop : 'a -> 'a -> bool}; +fun eqop (A_:'a eq) = #eqop A_; type 'a ord = {less_eq : 'a -> 'a -> bool, less : 'a -> 'a -> bool}; fun less_eq (A_:'a ord) = #less_eq A_; @@ -24,14 +24,14 @@ structure Nat = struct -datatype nat = Zero_nat | Suc of nat; +datatype nat = Suc of nat | Zero_nat; -fun eq_nat Zero_nat (Suc m) = false - | eq_nat (Suc n) Zero_nat = false - | eq_nat (Suc n) (Suc m) = eq_nat n m - | eq_nat Zero_nat Zero_nat = true; +fun eqop_nat Zero_nat (Suc m) = false + | eqop_nat (Suc n) Zero_nat = false + | eqop_nat (Suc n) (Suc m) = eqop_nat n m + | eqop_nat Zero_nat Zero_nat = true; -val eq_nata = {eq = eq_nat} : nat HOL.eq; +val eq_nat = {eqop = eqop_nat} : nat HOL.eq; fun less_nat n (Suc m) = less_eq_nat n m | less_nat n Zero_nat = false @@ -50,8 +50,9 @@ structure Codegen = struct -datatype ('a, 'b) searchtree = Leaf of 'a * 'b | - Branch of ('a, 'b) searchtree * 'a * ('a, 'b) searchtree; +datatype ('a, 'b) searchtree = + Branch of ('a, 'b) searchtree * 'a * ('a, 'b) searchtree | + Leaf of 'a * 'b; fun update (C1_, C2_) (it, entry) (Branch (t1, key, t2)) = (if HOL.less_eq ((Orderings.ord_order o Orderings.order_linorder) C2_) @@ -59,7 +60,7 @@ then Branch (update (C1_, C2_) (it, entry) t1, key, t2) else Branch (t1, key, update (C1_, C2_) (it, entry) t2)) | update (C1_, C2_) (it, entry) (Leaf (key, vala)) = - (if HOL.eq C1_ it key then Leaf (key, entry) + (if HOL.eqop C1_ it key then Leaf (key, entry) else (if HOL.less_eq ((Orderings.ord_order o Orderings.order_linorder) C2_) it key @@ -67,13 +68,13 @@ else Branch (Leaf (key, vala), it, Leaf (it, entry)))); val example : (Nat.nat, (Nat.nat list)) searchtree = - update (Nat.eq_nata, Nat.linorder_nat) + update (Nat.eq_nat, Nat.linorder_nat) (Nat.Suc (Nat.Suc (Nat.Suc (Nat.Suc Nat.Zero_nat))), [Nat.Suc (Nat.Suc Nat.Zero_nat), Nat.Suc (Nat.Suc Nat.Zero_nat)]) - (update (Nat.eq_nata, Nat.linorder_nat) + (update (Nat.eq_nat, Nat.linorder_nat) (Nat.Suc (Nat.Suc (Nat.Suc Nat.Zero_nat)), [Nat.Suc (Nat.Suc (Nat.Suc Nat.Zero_nat))]) - (update (Nat.eq_nata, Nat.linorder_nat) + (update (Nat.eq_nat, Nat.linorder_nat) (Nat.Suc (Nat.Suc Nat.Zero_nat), [Nat.Suc (Nat.Suc Nat.Zero_nat)]) (Leaf (Nat.Suc Nat.Zero_nat, []))));