syntax for "class attach const"
authorhaftmann
Fri Mar 02 15:43:16 2007 +0100 (2007-03-02 ago)
changeset 22385cc2be3315e72
parent 22384 33a46e6c7f04
child 22386 4ebe883b02ff
syntax for "class attach const"
doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex
src/HOL/Code_Generator.thy
src/Pure/Isar/isar_syn.ML
src/Pure/Tools/class_package.ML
src/Pure/axclass.ML
     1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Fri Mar 02 15:43:15 2007 +0100
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Fri Mar 02 15:43:16 2007 +0100
     1.3 @@ -749,8 +749,7 @@
     1.4  consts "op =" :: "'a"
     1.5  (*>*)
     1.6  
     1.7 -axclass eq \<subseteq> type
     1.8 -  (attach "op =")
     1.9 +class eq (attach "op =") = notes reflexive
    1.10  
    1.11  text {*
    1.12    This merely introduces a class @{text eq} with corresponding
     2.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Fri Mar 02 15:43:15 2007 +0100
     2.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Fri Mar 02 15:43:16 2007 +0100
     2.3 @@ -985,9 +985,8 @@
     2.4  %
     2.5  \endisadelimML
     2.6  \isanewline
     2.7 -\isacommand{axclass}\isamarkupfalse%
     2.8 -\ eq\ {\isasymsubseteq}\ type\isanewline
     2.9 -\ \ {\isacharparenleft}\isakeyword{attach}\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}{\isacharparenright}%
    2.10 +\isacommand{class}\isamarkupfalse%
    2.11 +\ eq\ {\isacharparenleft}\isakeyword{attach}\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}{\isacharparenright}\ {\isacharequal}\ \isakeyword{notes}\ reflexive%
    2.12  \begin{isamarkuptext}%
    2.13  This merely introduces a class \isa{eq} with corresponding
    2.14    operation \isa{op\ {\isacharequal}};
     3.1 --- a/src/HOL/Code_Generator.thy	Fri Mar 02 15:43:15 2007 +0100
     3.2 +++ b/src/HOL/Code_Generator.thy	Fri Mar 02 15:43:16 2007 +0100
     3.3 @@ -8,7 +8,7 @@
     3.4  imports HOL
     3.5  begin
     3.6  
     3.7 -subsection {* ML code generator *}
     3.8 +subsection {* SML code generator setup *}
     3.9  
    3.10  types_code
    3.11    "bool"  ("bool")
    3.12 @@ -75,8 +75,7 @@
    3.13  
    3.14  text {* operational equality for code generation *}
    3.15  
    3.16 -axclass eq \<subseteq> type
    3.17 -  (attach "op =")
    3.18 +class eq (attach "op =") = notes reflexive
    3.19  
    3.20  
    3.21  text {* equality for Haskell *}
     4.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Mar 02 15:43:15 2007 +0100
     4.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Mar 02 15:43:16 2007 +0100
     4.3 @@ -88,9 +88,8 @@
     4.4    OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl
     4.5      (P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
     4.6          P.!!! (P.list1 P.xname)) []
     4.7 -        -- Scan.optional (P.$$$ "(" |-- P.$$$ "attach" |-- Scan.repeat P.term --| P.$$$ ")") []
     4.8          -- Scan.repeat (SpecParse.thm_name ":" -- (P.prop >> single))
     4.9 -      >> (fn ((x, y), z) => Toplevel.theory (snd o AxClass.define_class x y z)));
    4.10 +      >> (fn (x, y) => Toplevel.theory (snd o AxClass.define_class x [] y)));
    4.11  
    4.12  
    4.13  (* types *)
    4.14 @@ -412,15 +411,16 @@
    4.15  
    4.16  val classP =
    4.17    OuterSyntax.command "class" "define type class" K.thy_decl (
    4.18 -    P.name --| P.$$$ "="
    4.19 -    -- (
    4.20 +    P.name
    4.21 +    -- Scan.optional (P.$$$ "(" |-- P.$$$ "attach" |-- Scan.repeat P.term --| P.$$$ ")") []
    4.22 +    --| P.$$$ "=" -- (
    4.23        class_subP --| P.$$$ "+" -- class_bodyP
    4.24        || class_subP >> rpair []
    4.25        || class_bodyP >> pair [])
    4.26      -- P.opt_begin
    4.27 -    >> (fn ((bname, (supclasses, elems)), begin) =>
    4.28 +    >> (fn (((bname, add_consts), (supclasses, elems)), begin) =>
    4.29          Toplevel.begin_local_theory begin
    4.30 -          (ClassPackage.class_cmd bname supclasses elems #-> TheoryTarget.begin)));
    4.31 +          (ClassPackage.class_cmd bname supclasses elems add_consts #-> TheoryTarget.begin)));
    4.32  
    4.33  val instanceP =
    4.34    OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal ((
     5.1 --- a/src/Pure/Tools/class_package.ML	Fri Mar 02 15:43:15 2007 +0100
     5.2 +++ b/src/Pure/Tools/class_package.ML	Fri Mar 02 15:43:16 2007 +0100
     5.3 @@ -9,10 +9,10 @@
     5.4  sig
     5.5    val fork_mixfix: bool -> string option -> mixfix -> mixfix * mixfix
     5.6  
     5.7 -  val class: bstring -> class list -> Element.context_i Locale.element list -> theory ->
     5.8 -    string * Proof.context
     5.9 -  val class_cmd: bstring -> string list -> Element.context Locale.element list -> theory ->
    5.10 -    string * Proof.context
    5.11 +  val class: bstring -> class list -> Element.context_i Locale.element list
    5.12 +    -> string list -> theory -> string * Proof.context
    5.13 +  val class_cmd: bstring -> string list -> Element.context Locale.element list
    5.14 +    -> string list -> theory -> string * Proof.context
    5.15    val instance_arity: arity list -> ((bstring * Attrib.src list) * term) list
    5.16      -> theory -> Proof.state
    5.17    val instance_arity_cmd: (bstring * string list * string) list
    5.18 @@ -33,6 +33,7 @@
    5.19    val class_of_locale: theory -> string -> class option
    5.20    val add_def_in_class: local_theory -> string
    5.21      -> (string * Syntax.mixfix) * ((string * Attrib.src list) * (term * thm)) -> theory -> theory
    5.22 +  val fully_qualified: bool ref;
    5.23  
    5.24    val print_classes: theory -> unit
    5.25    val intro_classes_tac: thm list -> tactic
    5.26 @@ -81,7 +82,7 @@
    5.27  
    5.28  (* introducing axclasses with implicit parameter handling *)
    5.29  
    5.30 -fun axclass_params (name, raw_superclasses) raw_consts raw_dep_axioms thy =
    5.31 +fun axclass_params (name, raw_superclasses) raw_consts raw_dep_axioms other_consts thy =
    5.32    let
    5.33      val superclasses = map (Sign.certify_class thy) raw_superclasses;
    5.34      val consts = (map o apfst o apsnd) (Sign.certify_typ thy) raw_consts;
    5.35 @@ -97,7 +98,7 @@
    5.36      thy
    5.37      |> fold_map add_const consts
    5.38      |-> (fn cs => mk_axioms cs
    5.39 -    #-> (fn axioms_prop => AxClass.define_class_i (name, superclasses) (map fst cs) axioms_prop
    5.40 +    #-> (fn axioms_prop => AxClass.define_class_i (name, superclasses) (map fst cs @ other_consts) axioms_prop
    5.41      #-> (fn class => `(fn thy => AxClass.get_definition thy class)
    5.42      #-> (fn {intro, axioms, ...} => fold (add_constraint class) cs
    5.43      #> pair (class, ((intro, (map Thm.prop_of axioms, axioms)), cs))))))
    5.44 @@ -426,6 +427,8 @@
    5.45  
    5.46  (* classes and instances *)
    5.47  
    5.48 +val fully_qualified = ref false;
    5.49 +
    5.50  local
    5.51  
    5.52  fun add_axclass (name, supsort) params axs thy =
    5.53 @@ -441,7 +444,7 @@
    5.54  fun read_class thy =
    5.55    certify_class thy o Sign.intern_class thy;
    5.56  
    5.57 -fun gen_class add_locale prep_class bname raw_supclasses raw_elems thy =
    5.58 +fun gen_class add_locale prep_class prep_param bname raw_supclasses raw_elems raw_other_consts thy =
    5.59    let
    5.60      (*FIXME need proper concept for reading locale statements*)
    5.61      fun subst_classtyvar (_, _) =
    5.62 @@ -450,6 +453,7 @@
    5.63            error ("Sort constraint illegal in type class, for type variable " ^ v ^ "::" ^ Sign.string_of_sort thy sort);
    5.64      (*val subst_classtyvars = Element.map_ctxt {name = I, var = I, term = I,
    5.65        typ = Term.map_type_tfree subst_classtyvar, fact = I, attrib = I};*)
    5.66 +    val other_consts = map (prep_param thy) raw_other_consts;
    5.67      val elems = fold_rev (fn Locale.Elem e => cons e | _ => I)
    5.68        raw_elems []; (*FIXME make include possible here?*)
    5.69      val supclasses = map (prep_class thy) raw_supclasses;
    5.70 @@ -505,7 +509,7 @@
    5.71      |-> (fn name_locale => ProofContext.theory_result (
    5.72        `(fn thy => extract_params thy name_locale)
    5.73        #-> (fn (param_names, params) =>
    5.74 -        axclass_params (bname, supsort) params (extract_assumes name_locale params)
    5.75 +        axclass_params (bname, supsort) params (extract_assumes name_locale params) other_consts
    5.76        #-> (fn (name_axclass, ((_, (ax_terms, ax_axioms)), consts)) =>
    5.77          `(fn thy => extract_axiom_names thy name_locale)
    5.78        #-> (fn axiom_names =>
    5.79 @@ -513,7 +517,7 @@
    5.80            (name_locale, map (fst o fst) params ~~ map fst consts,
    5.81              map2 make_witness ax_terms ax_axioms, axiom_names))
    5.82        #> prove_interpretation ((ALLGOALS o ProofContext.fact_tac) ax_axioms)
    5.83 -          ((true, Logic.const_of_class bname), []) (Locale.Locale name_locale)
    5.84 +          ((!fully_qualified, Logic.const_of_class bname), []) (Locale.Locale name_locale)
    5.85            (mk_instT name_axclass, mk_inst name_axclass param_names (map snd supconsts @ consts))
    5.86        #> pair name_axclass
    5.87        )))))
    5.88 @@ -521,8 +525,8 @@
    5.89  
    5.90  in
    5.91  
    5.92 -val class_cmd = gen_class Locale.add_locale read_class;
    5.93 -val class = gen_class Locale.add_locale_i certify_class;
    5.94 +val class_cmd = gen_class Locale.add_locale read_class AxClass.read_param;
    5.95 +val class = gen_class Locale.add_locale_i certify_class (K I);
    5.96  
    5.97  end; (*local*)
    5.98  
     6.1 --- a/src/Pure/axclass.ML	Fri Mar 02 15:43:15 2007 +0100
     6.2 +++ b/src/Pure/axclass.ML	Fri Mar 02 15:43:16 2007 +0100
     6.3 @@ -25,6 +25,7 @@
     6.4      ((bstring * Attrib.src list) * string list) list -> theory -> class * theory
     6.5    val define_class_i: bstring * class list -> string list ->
     6.6      ((bstring * attribute list) * term list) list -> theory -> class * theory
     6.7 +  val read_param: theory -> string -> string
     6.8    val axiomatize_class: bstring * xstring list -> theory -> theory
     6.9    val axiomatize_class_i: bstring * class list -> theory -> theory
    6.10    val axiomatize_classrel: (xstring * xstring) list -> theory -> theory
    6.11 @@ -269,8 +270,6 @@
    6.12  
    6.13  (** class definitions **)
    6.14  
    6.15 -local
    6.16 -
    6.17  fun read_param thy raw_t =
    6.18    let
    6.19      val t = Sign.read_term thy raw_t
    6.20 @@ -279,6 +278,8 @@
    6.21      | NONE => error ("Not a constant: " ^ Sign.string_of_term thy t)
    6.22    end;
    6.23  
    6.24 +local
    6.25 +
    6.26  fun def_class prep_class prep_att prep_param prep_propp
    6.27      (bclass, raw_super) raw_params raw_specs thy =
    6.28    let