--- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Fri Mar 02 15:43:15 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Fri Mar 02 15:43:16 2007 +0100
@@ -749,8 +749,7 @@
consts "op =" :: "'a"
(*>*)
-axclass eq \<subseteq> type
- (attach "op =")
+class eq (attach "op =") = notes reflexive
text {*
This merely introduces a class @{text eq} with corresponding
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Fri Mar 02 15:43:15 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Fri Mar 02 15:43:16 2007 +0100
@@ -985,9 +985,8 @@
%
\endisadelimML
\isanewline
-\isacommand{axclass}\isamarkupfalse%
-\ eq\ {\isasymsubseteq}\ type\isanewline
-\ \ {\isacharparenleft}\isakeyword{attach}\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}{\isacharparenright}%
+\isacommand{class}\isamarkupfalse%
+\ eq\ {\isacharparenleft}\isakeyword{attach}\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}{\isacharparenright}\ {\isacharequal}\ \isakeyword{notes}\ reflexive%
\begin{isamarkuptext}%
This merely introduces a class \isa{eq} with corresponding
operation \isa{op\ {\isacharequal}};
--- a/src/HOL/Code_Generator.thy Fri Mar 02 15:43:15 2007 +0100
+++ b/src/HOL/Code_Generator.thy Fri Mar 02 15:43:16 2007 +0100
@@ -8,7 +8,7 @@
imports HOL
begin
-subsection {* ML code generator *}
+subsection {* SML code generator setup *}
types_code
"bool" ("bool")
@@ -75,8 +75,7 @@
text {* operational equality for code generation *}
-axclass eq \<subseteq> type
- (attach "op =")
+class eq (attach "op =") = notes reflexive
text {* equality for Haskell *}
--- a/src/Pure/Isar/isar_syn.ML Fri Mar 02 15:43:15 2007 +0100
+++ b/src/Pure/Isar/isar_syn.ML Fri Mar 02 15:43:16 2007 +0100
@@ -88,9 +88,8 @@
OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl
(P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
P.!!! (P.list1 P.xname)) []
- -- Scan.optional (P.$$$ "(" |-- P.$$$ "attach" |-- Scan.repeat P.term --| P.$$$ ")") []
-- Scan.repeat (SpecParse.thm_name ":" -- (P.prop >> single))
- >> (fn ((x, y), z) => Toplevel.theory (snd o AxClass.define_class x y z)));
+ >> (fn (x, y) => Toplevel.theory (snd o AxClass.define_class x [] y)));
(* types *)
@@ -412,15 +411,16 @@
val classP =
OuterSyntax.command "class" "define type class" K.thy_decl (
- P.name --| P.$$$ "="
- -- (
+ P.name
+ -- Scan.optional (P.$$$ "(" |-- P.$$$ "attach" |-- Scan.repeat P.term --| P.$$$ ")") []
+ --| P.$$$ "=" -- (
class_subP --| P.$$$ "+" -- class_bodyP
|| class_subP >> rpair []
|| class_bodyP >> pair [])
-- P.opt_begin
- >> (fn ((bname, (supclasses, elems)), begin) =>
+ >> (fn (((bname, add_consts), (supclasses, elems)), begin) =>
Toplevel.begin_local_theory begin
- (ClassPackage.class_cmd bname supclasses elems #-> TheoryTarget.begin)));
+ (ClassPackage.class_cmd bname supclasses elems add_consts #-> TheoryTarget.begin)));
val instanceP =
OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal ((
--- a/src/Pure/Tools/class_package.ML Fri Mar 02 15:43:15 2007 +0100
+++ b/src/Pure/Tools/class_package.ML Fri Mar 02 15:43:16 2007 +0100
@@ -9,10 +9,10 @@
sig
val fork_mixfix: bool -> string option -> mixfix -> mixfix * mixfix
- val class: bstring -> class list -> Element.context_i Locale.element list -> theory ->
- string * Proof.context
- val class_cmd: bstring -> string list -> Element.context Locale.element list -> theory ->
- string * Proof.context
+ val class: bstring -> class list -> Element.context_i Locale.element list
+ -> string list -> theory -> string * Proof.context
+ val class_cmd: bstring -> string list -> Element.context Locale.element list
+ -> string list -> theory -> string * Proof.context
val instance_arity: arity list -> ((bstring * Attrib.src list) * term) list
-> theory -> Proof.state
val instance_arity_cmd: (bstring * string list * string) list
@@ -33,6 +33,7 @@
val class_of_locale: theory -> string -> class option
val add_def_in_class: local_theory -> string
-> (string * Syntax.mixfix) * ((string * Attrib.src list) * (term * thm)) -> theory -> theory
+ val fully_qualified: bool ref;
val print_classes: theory -> unit
val intro_classes_tac: thm list -> tactic
@@ -81,7 +82,7 @@
(* introducing axclasses with implicit parameter handling *)
-fun axclass_params (name, raw_superclasses) raw_consts raw_dep_axioms thy =
+fun axclass_params (name, raw_superclasses) raw_consts raw_dep_axioms other_consts thy =
let
val superclasses = map (Sign.certify_class thy) raw_superclasses;
val consts = (map o apfst o apsnd) (Sign.certify_typ thy) raw_consts;
@@ -97,7 +98,7 @@
thy
|> fold_map add_const consts
|-> (fn cs => mk_axioms cs
- #-> (fn axioms_prop => AxClass.define_class_i (name, superclasses) (map fst cs) axioms_prop
+ #-> (fn axioms_prop => AxClass.define_class_i (name, superclasses) (map fst cs @ other_consts) axioms_prop
#-> (fn class => `(fn thy => AxClass.get_definition thy class)
#-> (fn {intro, axioms, ...} => fold (add_constraint class) cs
#> pair (class, ((intro, (map Thm.prop_of axioms, axioms)), cs))))))
@@ -426,6 +427,8 @@
(* classes and instances *)
+val fully_qualified = ref false;
+
local
fun add_axclass (name, supsort) params axs thy =
@@ -441,7 +444,7 @@
fun read_class thy =
certify_class thy o Sign.intern_class thy;
-fun gen_class add_locale prep_class bname raw_supclasses raw_elems thy =
+fun gen_class add_locale prep_class prep_param bname raw_supclasses raw_elems raw_other_consts thy =
let
(*FIXME need proper concept for reading locale statements*)
fun subst_classtyvar (_, _) =
@@ -450,6 +453,7 @@
error ("Sort constraint illegal in type class, for type variable " ^ v ^ "::" ^ Sign.string_of_sort thy sort);
(*val subst_classtyvars = Element.map_ctxt {name = I, var = I, term = I,
typ = Term.map_type_tfree subst_classtyvar, fact = I, attrib = I};*)
+ val other_consts = map (prep_param thy) raw_other_consts;
val elems = fold_rev (fn Locale.Elem e => cons e | _ => I)
raw_elems []; (*FIXME make include possible here?*)
val supclasses = map (prep_class thy) raw_supclasses;
@@ -505,7 +509,7 @@
|-> (fn name_locale => ProofContext.theory_result (
`(fn thy => extract_params thy name_locale)
#-> (fn (param_names, params) =>
- axclass_params (bname, supsort) params (extract_assumes name_locale params)
+ axclass_params (bname, supsort) params (extract_assumes name_locale params) other_consts
#-> (fn (name_axclass, ((_, (ax_terms, ax_axioms)), consts)) =>
`(fn thy => extract_axiom_names thy name_locale)
#-> (fn axiom_names =>
@@ -513,7 +517,7 @@
(name_locale, map (fst o fst) params ~~ map fst consts,
map2 make_witness ax_terms ax_axioms, axiom_names))
#> prove_interpretation ((ALLGOALS o ProofContext.fact_tac) ax_axioms)
- ((true, Logic.const_of_class bname), []) (Locale.Locale name_locale)
+ ((!fully_qualified, Logic.const_of_class bname), []) (Locale.Locale name_locale)
(mk_instT name_axclass, mk_inst name_axclass param_names (map snd supconsts @ consts))
#> pair name_axclass
)))))
@@ -521,8 +525,8 @@
in
-val class_cmd = gen_class Locale.add_locale read_class;
-val class = gen_class Locale.add_locale_i certify_class;
+val class_cmd = gen_class Locale.add_locale read_class AxClass.read_param;
+val class = gen_class Locale.add_locale_i certify_class (K I);
end; (*local*)
--- a/src/Pure/axclass.ML Fri Mar 02 15:43:15 2007 +0100
+++ b/src/Pure/axclass.ML Fri Mar 02 15:43:16 2007 +0100
@@ -25,6 +25,7 @@
((bstring * Attrib.src list) * string list) list -> theory -> class * theory
val define_class_i: bstring * class list -> string list ->
((bstring * attribute list) * term list) list -> theory -> class * theory
+ val read_param: theory -> string -> string
val axiomatize_class: bstring * xstring list -> theory -> theory
val axiomatize_class_i: bstring * class list -> theory -> theory
val axiomatize_classrel: (xstring * xstring) list -> theory -> theory
@@ -269,8 +270,6 @@
(** class definitions **)
-local
-
fun read_param thy raw_t =
let
val t = Sign.read_term thy raw_t
@@ -279,6 +278,8 @@
| NONE => error ("Not a constant: " ^ Sign.string_of_term thy t)
end;
+local
+
fun def_class prep_class prep_att prep_param prep_propp
(bclass, raw_super) raw_params raw_specs thy =
let