--- 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 \<Colon> 'a list \<Rightarrow> '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}.
--- 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}.
--- 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;
--- 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
--- 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
--- 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
--- 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*)
--- 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*)
--- 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*)
--- 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;
--- 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;
--- 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*)
--- 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*)
--- 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
--- 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
--- 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*)
--- 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, []))));