# HG changeset patch
# User haftmann
# Date 1172846596 -3600
# Node ID cc2be3315e728f47c81ec5b048e6ceebc775f1b3
# Parent  33a46e6c7f048e70149d44b248bf03163da1c097
syntax for "class attach const"

diff -r 33a46e6c7f04 -r cc2be3315e72 doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
--- 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
diff -r 33a46e6c7f04 -r cc2be3315e72 doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex
--- 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}};
diff -r 33a46e6c7f04 -r cc2be3315e72 src/HOL/Code_Generator.thy
--- 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 *}
diff -r 33a46e6c7f04 -r cc2be3315e72 src/Pure/Isar/isar_syn.ML
--- 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 ((
diff -r 33a46e6c7f04 -r cc2be3315e72 src/Pure/Tools/class_package.ML
--- 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*)
 
diff -r 33a46e6c7f04 -r cc2be3315e72 src/Pure/axclass.ML
--- 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