src/Pure/Tools/class_package.ML
author haftmann
Tue, 14 Feb 2006 17:07:11 +0100
changeset 19038 62c5f7591a43
parent 18963 3adfc9dfb30a
child 19102 db27ca6a6cd6
permissions -rw-r--r--
improved handling of iml abstractions
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
18168
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
     1
(*  Title:      Pure/Tools/class_package.ML
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
     2
    ID:         $Id$
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
     3
    Author:     Florian Haftmann, TU Muenchen
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
     4
18755
eb3733779aa8 slight steps forward
haftmann
parents: 18728
diff changeset
     5
Type classes, simulated by locales.
18168
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
     6
*)
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
     7
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
     8
signature CLASS_PACKAGE =
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
     9
sig
18755
eb3733779aa8 slight steps forward
haftmann
parents: 18728
diff changeset
    10
  val add_class: bstring -> class list -> Element.context list -> theory
18515
1cad5c2b2a0b substantial improvements in code generating
haftmann
parents: 18380
diff changeset
    11
    -> ProofContext.context * theory
18755
eb3733779aa8 slight steps forward
haftmann
parents: 18728
diff changeset
    12
  val add_class_i: bstring -> class list -> Element.context_i list -> theory
18515
1cad5c2b2a0b substantial improvements in code generating
haftmann
parents: 18380
diff changeset
    13
    -> ProofContext.context * theory
18575
9ccfd1d1e874 substantial additions using locales
haftmann
parents: 18550
diff changeset
    14
  val add_instance_arity: (xstring * string list) * string
9ccfd1d1e874 substantial additions using locales
haftmann
parents: 18550
diff changeset
    15
    -> ((bstring * string) * Attrib.src list) list
9ccfd1d1e874 substantial additions using locales
haftmann
parents: 18550
diff changeset
    16
    -> theory -> Proof.state
9ccfd1d1e874 substantial additions using locales
haftmann
parents: 18550
diff changeset
    17
  val add_instance_arity_i: (string * sort list) * sort
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    18
    -> ((bstring * term) * attribute list) list
18575
9ccfd1d1e874 substantial additions using locales
haftmann
parents: 18550
diff changeset
    19
    -> theory -> Proof.state
18849
05a16861d3a5 added three times overloaded Isar instance command
haftmann
parents: 18829
diff changeset
    20
  val add_classentry: class -> xstring list -> theory -> theory
05a16861d3a5 added three times overloaded Isar instance command
haftmann
parents: 18829
diff changeset
    21
  val add_classinsts: class -> xstring list -> theory -> theory
18168
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
    22
18755
eb3733779aa8 slight steps forward
haftmann
parents: 18728
diff changeset
    23
  val intern_class: theory -> xstring -> string
eb3733779aa8 slight steps forward
haftmann
parents: 18728
diff changeset
    24
  val extern_class: theory -> string -> xstring
eb3733779aa8 slight steps forward
haftmann
parents: 18728
diff changeset
    25
  val certify_class: theory -> class -> class
18884
df1e3c93c50a name clarifications
haftmann
parents: 18864
diff changeset
    26
  val operational_sort_of: theory -> sort -> sort
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
    27
  val the_superclasses: theory -> class -> class list
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
    28
  val the_consts_sign: theory -> class -> string * (string * typ) list
18168
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
    29
  val lookup_const_class: theory -> string -> class option
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
    30
  val the_instances: theory -> class -> (string * string) list
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
    31
  val the_inst_sign: theory -> class * string -> (string * sort) list * (string * typ) list
18168
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
    32
  val get_classtab: theory -> (string list * (string * string) list) Symtab.table
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
    33
  val print_classes: theory -> unit
18168
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
    34
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
    35
  type sortcontext = (string * sort) list
18884
df1e3c93c50a name clarifications
haftmann
parents: 18864
diff changeset
    36
  datatype classlookup = Instance of (class * string) * classlookup list list
df1e3c93c50a name clarifications
haftmann
parents: 18864
diff changeset
    37
                       | Lookup of class list * (string * int)
18168
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
    38
  val extract_sortctxt: theory -> typ -> sortcontext
18884
df1e3c93c50a name clarifications
haftmann
parents: 18864
diff changeset
    39
  val extract_classlookup: theory -> string * typ -> classlookup list list
df1e3c93c50a name clarifications
haftmann
parents: 18864
diff changeset
    40
  val extract_classlookup_inst: theory -> class * string -> class -> classlookup list list
18168
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
    41
end;
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
    42
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
    43
structure ClassPackage: CLASS_PACKAGE =
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
    44
struct
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
    45
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
    46
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18702
diff changeset
    47
(* theory data *)
18168
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
    48
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
    49
type class_data = {
18575
9ccfd1d1e874 substantial additions using locales
haftmann
parents: 18550
diff changeset
    50
  superclasses: class list,
9ccfd1d1e874 substantial additions using locales
haftmann
parents: 18550
diff changeset
    51
  name_locale: string,
9ccfd1d1e874 substantial additions using locales
haftmann
parents: 18550
diff changeset
    52
  name_axclass: string,
9ccfd1d1e874 substantial additions using locales
haftmann
parents: 18550
diff changeset
    53
  var: string,
9ccfd1d1e874 substantial additions using locales
haftmann
parents: 18550
diff changeset
    54
  consts: (string * typ) list,
9ccfd1d1e874 substantial additions using locales
haftmann
parents: 18550
diff changeset
    55
  insts: (string * string) list
18168
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
    56
};
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
    57
18575
9ccfd1d1e874 substantial additions using locales
haftmann
parents: 18550
diff changeset
    58
structure ClassData = TheoryDataFun (
18168
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
    59
  struct
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
    60
    val name = "Pure/classes";
19038
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
    61
    type T = class_data Symtab.table * (class Symtab.table * string Symtab.table);
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
    62
    val empty = (Symtab.empty, (Symtab.empty, Symtab.empty));
18168
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
    63
    val copy = I;
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
    64
    val extend = I;
19038
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
    65
    fun merge _ ((t1, (c1, l1)), (t2, (c2, l2)))=
18168
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
    66
      (Symtab.merge (op =) (t1, t2),
19038
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
    67
       (Symtab.merge (op =) (c1, c2), Symtab.merge (op =) (l1, l2)));
18575
9ccfd1d1e874 substantial additions using locales
haftmann
parents: 18550
diff changeset
    68
    fun print thy (tab, _) =
9ccfd1d1e874 substantial additions using locales
haftmann
parents: 18550
diff changeset
    69
      let
9ccfd1d1e874 substantial additions using locales
haftmann
parents: 18550
diff changeset
    70
        fun pretty_class (name, {superclasses, name_locale, name_axclass, var, consts, insts}) =
9ccfd1d1e874 substantial additions using locales
haftmann
parents: 18550
diff changeset
    71
          (Pretty.block o Pretty.fbreaks) [
9ccfd1d1e874 substantial additions using locales
haftmann
parents: 18550
diff changeset
    72
            Pretty.str ("class " ^ name ^ ":"),
9ccfd1d1e874 substantial additions using locales
haftmann
parents: 18550
diff changeset
    73
            (Pretty.block o Pretty.fbreaks) (
9ccfd1d1e874 substantial additions using locales
haftmann
parents: 18550
diff changeset
    74
              Pretty.str "superclasses: "
9ccfd1d1e874 substantial additions using locales
haftmann
parents: 18550
diff changeset
    75
              :: map Pretty.str superclasses
9ccfd1d1e874 substantial additions using locales
haftmann
parents: 18550
diff changeset
    76
            ),
9ccfd1d1e874 substantial additions using locales
haftmann
parents: 18550
diff changeset
    77
            Pretty.str ("locale: " ^ name_locale),
9ccfd1d1e874 substantial additions using locales
haftmann
parents: 18550
diff changeset
    78
            Pretty.str ("axclass: " ^ name_axclass),
9ccfd1d1e874 substantial additions using locales
haftmann
parents: 18550
diff changeset
    79
            Pretty.str ("class variable: " ^ var),
9ccfd1d1e874 substantial additions using locales
haftmann
parents: 18550
diff changeset
    80
            (Pretty.block o Pretty.fbreaks) (
9ccfd1d1e874 substantial additions using locales
haftmann
parents: 18550
diff changeset
    81
              Pretty.str "constants: "
9ccfd1d1e874 substantial additions using locales
haftmann
parents: 18550
diff changeset
    82
              :: map (fn (c, ty) => Pretty.str (c ^ " :: " ^ Sign.string_of_typ thy ty)) consts
9ccfd1d1e874 substantial additions using locales
haftmann
parents: 18550
diff changeset
    83
            ),
9ccfd1d1e874 substantial additions using locales
haftmann
parents: 18550
diff changeset
    84
            (Pretty.block o Pretty.fbreaks) (
9ccfd1d1e874 substantial additions using locales
haftmann
parents: 18550
diff changeset
    85
              Pretty.str "instances: "
9ccfd1d1e874 substantial additions using locales
haftmann
parents: 18550
diff changeset
    86
              :: map (fn (tyco, thyname) => Pretty.str (tyco ^ ", in theory " ^ thyname)) insts
9ccfd1d1e874 substantial additions using locales
haftmann
parents: 18550
diff changeset
    87
            )
9ccfd1d1e874 substantial additions using locales
haftmann
parents: 18550
diff changeset
    88
          ]
9ccfd1d1e874 substantial additions using locales
haftmann
parents: 18550
diff changeset
    89
      in
9ccfd1d1e874 substantial additions using locales
haftmann
parents: 18550
diff changeset
    90
        (Pretty.writeln o Pretty.chunks o map pretty_class o Symtab.dest) tab
9ccfd1d1e874 substantial additions using locales
haftmann
parents: 18550
diff changeset
    91
      end;
18168
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
    92
  end
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
    93
);
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
    94
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18702
diff changeset
    95
val _ = Context.add_setup ClassData.init;
18575
9ccfd1d1e874 substantial additions using locales
haftmann
parents: 18550
diff changeset
    96
val print_classes = ClassData.print;
9ccfd1d1e874 substantial additions using locales
haftmann
parents: 18550
diff changeset
    97
19038
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
    98
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
    99
(* queries *)
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   100
18575
9ccfd1d1e874 substantial additions using locales
haftmann
parents: 18550
diff changeset
   101
val lookup_class_data = Symtab.lookup o fst o ClassData.get;
19038
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   102
val lookup_const_class = Symtab.lookup o fst o snd o ClassData.get;
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   103
val lookup_locale_class = Symtab.lookup o snd o snd o ClassData.get;
18168
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   104
19038
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   105
fun the_class_data thy class =
18168
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   106
  case lookup_class_data thy class
18755
eb3733779aa8 slight steps forward
haftmann
parents: 18728
diff changeset
   107
    of NONE => error ("undeclared operational class " ^ quote class)
18168
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   108
     | SOME data => data;
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   109
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   110
fun is_class thy cls =
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   111
  lookup_class_data thy cls
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   112
  |> Option.map (not o null o #consts)
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   113
  |> the_default false;
18168
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   114
18884
df1e3c93c50a name clarifications
haftmann
parents: 18864
diff changeset
   115
fun operational_sort_of thy sort =
18360
a2c9506b62a7 improved class handling
haftmann
parents: 18335
diff changeset
   116
  let
a2c9506b62a7 improved class handling
haftmann
parents: 18335
diff changeset
   117
    val classes = Sign.classes_of thy;
a2c9506b62a7 improved class handling
haftmann
parents: 18335
diff changeset
   118
    fun get_sort cls =
a2c9506b62a7 improved class handling
haftmann
parents: 18335
diff changeset
   119
      if is_class thy cls
a2c9506b62a7 improved class handling
haftmann
parents: 18335
diff changeset
   120
      then [cls]
18884
df1e3c93c50a name clarifications
haftmann
parents: 18864
diff changeset
   121
      else operational_sort_of thy (Sorts.superclasses classes cls);
18360
a2c9506b62a7 improved class handling
haftmann
parents: 18335
diff changeset
   122
  in
a2c9506b62a7 improved class handling
haftmann
parents: 18335
diff changeset
   123
    map get_sort sort
a2c9506b62a7 improved class handling
haftmann
parents: 18335
diff changeset
   124
    |> Library.flat
a2c9506b62a7 improved class handling
haftmann
parents: 18335
diff changeset
   125
    |> Sorts.norm_sort classes
a2c9506b62a7 improved class handling
haftmann
parents: 18335
diff changeset
   126
  end;
18168
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   127
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   128
fun the_superclasses thy class =
18515
1cad5c2b2a0b substantial improvements in code generating
haftmann
parents: 18380
diff changeset
   129
  if is_class thy class
1cad5c2b2a0b substantial improvements in code generating
haftmann
parents: 18380
diff changeset
   130
  then
1cad5c2b2a0b substantial improvements in code generating
haftmann
parents: 18380
diff changeset
   131
    Sorts.superclasses (Sign.classes_of thy) class
18884
df1e3c93c50a name clarifications
haftmann
parents: 18864
diff changeset
   132
    |> operational_sort_of thy
18515
1cad5c2b2a0b substantial improvements in code generating
haftmann
parents: 18380
diff changeset
   133
  else
1cad5c2b2a0b substantial improvements in code generating
haftmann
parents: 18380
diff changeset
   134
    error ("no syntactic class: " ^ class);
18168
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   135
19038
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   136
fun the_ancestry thy classes =
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   137
  let
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   138
    fun ancestry class anc =
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   139
      anc
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   140
      |> cons class
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   141
      |> fold ancestry (the_superclasses thy class);
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   142
  in fold ancestry classes [] end;
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   143
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   144
fun subst_clsvar v ty_subst =
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   145
  map_type_tfree (fn u as (w, _) =>
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   146
    if w = v then ty_subst else TFree u);
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   147
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   148
fun the_consts_sign thy class =
18168
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   149
  let
19038
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   150
    val data = the_class_data thy class
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   151
  in (#var data, #consts data) end;
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   152
19038
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   153
val the_instances =
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   154
  #insts oo the_class_data;
18168
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   155
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   156
fun the_inst_sign thy (class, tyco) =
18168
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   157
  let
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   158
    val _ = if is_class thy class then () else error ("no syntactic class: " ^ class);
19038
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   159
    val arity =
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   160
      Sorts.mg_domain (Sign.classes_arities_of thy) tyco [class]
18884
df1e3c93c50a name clarifications
haftmann
parents: 18864
diff changeset
   161
      |> map (operational_sort_of thy);
19038
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   162
    val clsvar = (#var o the_class_data thy) class;
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   163
    val const_sign = (snd o the_consts_sign thy) class;
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   164
    fun add_var sort used =
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   165
      let
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   166
        val v = hd (Term.invent_names used "'a" 1)
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   167
      in ((v, sort), v::used) end;
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   168
    val (vsorts, _) =
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   169
      []
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   170
      |> fold (fn (_, ty) => curry (gen_union (op =))
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   171
           ((map (fst o fst) o typ_tvars) ty @ (map fst o typ_tfrees) ty)) const_sign
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   172
      |> fold_map add_var arity;
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   173
    val ty_inst = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) vsorts);
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   174
    val inst_signs = map (apsnd (subst_clsvar clsvar ty_inst)) const_sign;
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   175
  in (vsorts, inst_signs) end;
18168
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   176
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   177
fun get_classtab thy =
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   178
  Symtab.fold
18575
9ccfd1d1e874 substantial additions using locales
haftmann
parents: 18550
diff changeset
   179
    (fn (class, { consts = consts, insts = insts, ... }) =>
9ccfd1d1e874 substantial additions using locales
haftmann
parents: 18550
diff changeset
   180
      Symtab.update_new (class, (map fst consts, insts)))
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   181
       ((fst o ClassData.get) thy) Symtab.empty;
18168
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   182
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   183
19038
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   184
(* updaters *)
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   185
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   186
fun add_class_data (class, (superclasses, name_locale, name_axclass, classvar, consts)) =
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   187
  ClassData.map (fn (classtab, (consttab, loctab)) => (
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   188
    classtab
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   189
    |> Symtab.update (class, {
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   190
         superclasses = superclasses,
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   191
         name_locale = name_locale,
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   192
         name_axclass = name_axclass,
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   193
         var = classvar,
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   194
         consts = consts,
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   195
         insts = []
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   196
       }),
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   197
    (consttab
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   198
    |> fold (fn (c, _) => Symtab.update (c, class)) consts,
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   199
    loctab
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   200
    |> Symtab.update (name_locale, class))
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   201
  ));
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   202
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   203
fun add_inst_data (class, inst) =
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   204
  (ClassData.map o apfst o Symtab.map_entry class)
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   205
    (fn {superclasses, name_locale, name_axclass, var, consts, insts}
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   206
      => {
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   207
           superclasses = superclasses,
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   208
           name_locale = name_locale,
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   209
           name_axclass = name_axclass,
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   210
           var = var,
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   211
           consts = consts,
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   212
           insts = insts @ [inst]
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   213
          });
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   214
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   215
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   216
(* name handling *)
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   217
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   218
fun certify_class thy class =
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   219
  (the_class_data thy class; class);
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   220
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   221
fun intern_class thy raw_class =
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   222
  certify_class thy (Sign.intern_class thy raw_class);
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   223
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   224
fun extern_class thy class =
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   225
  Sign.extern_class thy (certify_class thy class);
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   226
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   227
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   228
(* classes and instances *)
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   229
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   230
local
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   231
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   232
fun intern_expr thy (Locale.Locale xname) = Locale.Locale (Locale.intern thy xname)
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   233
  | intern_expr thy (Locale.Merge exprs) = Locale.Merge (map (intern_expr thy) exprs)
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   234
  | intern_expr thy (Locale.Rename (expr, xs)) = Locale.Rename (intern_expr thy expr, xs);
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   235
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   236
fun gen_add_class add_locale prep_expr eval_expr do_proof bname raw_expr raw_body thy =
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   237
  let
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   238
    val ((import_asms, supclasses), locexpr) = (eval_expr thy o prep_expr thy) raw_expr;
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   239
    val supsort =
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   240
      supclasses
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   241
      |> map (#name_axclass o the_class_data thy)
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   242
      |> Sorts.certify_sort (Sign.classes_of thy)
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   243
      |> null ? K (Sign.defaultS thy);
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   244
    val _ = writeln ("got sort: " ^ Sign.string_of_sort thy supsort);
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   245
    val _ = writeln ("got asms: " ^ (cat_lines o map (Sign.string_of_term thy) o Library.flat o map (snd o fst)) import_asms);
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   246
    val supcs = (Library.flat o map (snd o the_consts_sign thy) o the_ancestry thy) supclasses;
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   247
    fun mk_c_lookup c_global supcs c_adds =
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   248
      map2 (fn ((c, _), _) => pair c) c_global supcs @ c_adds;
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   249
    fun extract_tyvar_consts thy name_locale =
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   250
      let
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   251
        fun extract_tyvar_name thy tys =
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   252
          fold (curry add_typ_tfrees) tys []
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   253
          |> (fn [(v, sort)] =>
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   254
                    if Sorts.sort_le (Sign.classes_of thy) (swap (sort, supsort))
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   255
                    then v
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   256
                    else error ("illegal sort constraint on class type variable: " ^ Sign.string_of_sort thy sort)
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   257
               | [] => error ("no class type variable")
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   258
               | vs => error ("more than one type variable: " ^ (commas o map (Sign.string_of_typ thy o TFree)) vs))
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   259
        val raw_consts =
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   260
          Locale.parameters_of thy name_locale
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   261
          |> map (apsnd Syntax.unlocalize_mixfix)
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   262
          |> Library.chop (length supcs);
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   263
        val v = (extract_tyvar_name thy o map (snd o fst) o op @) raw_consts;
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   264
        fun subst_ty cs =
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   265
          map ((apfst o apsnd) (subst_clsvar v (TFree (v, [])))) cs;
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   266
        val consts = (subst_ty (fst raw_consts), subst_ty (snd raw_consts));
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   267
        (*val _ = (writeln o commas o map (fst o fst)) (fst consts);
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   268
        val _ = (writeln o commas o map (fst o fst)) (snd consts);*)
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   269
      in (v, consts) end;
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   270
    fun add_global_const v ((c, ty), syn) thy =
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   271
      thy
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   272
      |> Sign.add_consts_i [(c, ty |> subst_clsvar v (TFree (v, Sign.defaultS thy)), syn)]
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   273
      |> `(fn thy => (c, (Sign.intern_const thy c, ty)))
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   274
    fun subst_assume c_lookup renaming =
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   275
      map_aterms (fn Free (c, ty) => Const ((fst o the o AList.lookup (op =) c_lookup o perhaps (AList.lookup (op =) renaming)) c, ty)
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   276
                   | t => t)
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   277
    fun extract_assumes thy name_locale c_lookup =
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   278
      map (rpair []) (Locale.local_asms_of thy name_locale) @ import_asms
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   279
      |> map (fn (((name, atts), ts), renaming) => ((name, map (Attrib.attribute thy) atts), (map (subst_assume c_lookup renaming)) ts));
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   280
    fun rearrange_assumes ((name, atts), ts) =
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   281
      map (rpair atts o pair "") ts
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   282
    fun add_global_constraint v class (_, (c, ty)) thy =
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   283
      thy
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   284
      |> Sign.add_const_constraint_i (c, subst_clsvar v (TVar ((v, 0), [class])) ty);
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   285
    fun ad_hoc_const thy class v (c, ty) =
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   286
      let
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   287
        val ty' = subst_clsvar v (TFree (v, [class])) ty;
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   288
        val s_ty = setmp print_mode [] (setmp show_types true (setmp show_sorts true (Sign.string_of_typ thy))) ty';
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   289
        val s = c ^ "::" ^ enclose "(" ")" s_ty;
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   290
        val _ = writeln ("our constant: " ^ s);
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   291
      in SOME s end;
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   292
    fun interpret name_locale name_axclass v cs ax_axioms thy =
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   293
      thy
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   294
      |> Locale.interpretation (NameSpace.base name_locale, [])
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   295
           (Locale.Locale name_locale) (map (ad_hoc_const thy name_axclass v) cs)
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   296
      |> do_proof ax_axioms;
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   297
  in
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   298
    thy
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   299
    |> add_locale bname locexpr raw_body
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   300
    |-> (fn ctxt =>
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   301
       `(fn thy => Locale.intern thy bname)
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   302
    #-> (fn name_locale =>
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   303
          `(fn thy => extract_tyvar_consts thy name_locale)
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   304
    #-> (fn (v, (c_global, c_defs)) =>
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   305
          fold_map (add_global_const v) c_defs
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   306
    #-> (fn c_adds =>
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   307
       `(fn thy => extract_assumes thy name_locale (mk_c_lookup c_global supcs c_adds))
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   308
    #-> (fn assumes =>
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   309
          AxClass.add_axclass_i (bname, supsort) ((Library.flat o map rearrange_assumes) assumes))
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   310
    #-> (fn { axioms = ax_axioms : thm list, ...} =>
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   311
          `(fn thy => Sign.intern_class thy bname)
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   312
    #-> (fn name_axclass =>
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   313
          fold (add_global_constraint v name_axclass) c_adds
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   314
    #> add_class_data (name_locale, (supclasses, name_locale, name_axclass, v, map snd c_adds))
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   315
    #> interpret name_locale name_axclass v (supcs @ map snd c_adds) ax_axioms
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   316
    ))))))
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   317
  end;
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   318
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   319
fun eval_expr_supclasses thy [] = (([], []), Locale.empty)
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   320
  | eval_expr_supclasses thy supclasses =
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   321
      (([], supclasses),
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   322
        (Locale.Merge o map (Locale.Locale o #name_locale o the_class_data thy)) supclasses);
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   323
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   324
in
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   325
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   326
val add_class = gen_add_class (Locale.add_locale true) (map o intern_class)
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   327
  eval_expr_supclasses (fn ax_axioms => Proof.global_terminal_proof (Method.Basic (Method.fact ax_axioms), NONE));
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   328
val add_class_i = gen_add_class (Locale.add_locale_i true) (map o certify_class)
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   329
  eval_expr_supclasses (fn ax_axioms => Proof.global_terminal_proof (Method.Basic (Method.fact ax_axioms), NONE));
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   330
val add_class_exp = gen_add_class (Locale.add_locale true) (map o intern_class)
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   331
  eval_expr_supclasses (K I);
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   332
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   333
end; (* local *)
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   334
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   335
fun gen_instance_arity prep_arity add_defs tap_def raw_arity raw_defs thy =
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   336
  let
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   337
    val pp = Sign.pp thy;
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   338
    val arity as (tyco, asorts, sort) = prep_arity thy ((fn ((x, y), z) => (x, y, z)) raw_arity);
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   339
    val ty_inst = Type (tyco, map2 (curry TVar o rpair 0) (Term.invent_names [] "'a" (length asorts)) asorts)
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   340
    fun get_c_req class =
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   341
      let
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   342
        val data = the_class_data thy class;
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   343
        val subst_ty = map_type_tfree (fn (var as (v, _)) =>
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   344
          if #var data = v then ty_inst else TFree var)
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   345
      in (map (apsnd subst_ty) o #consts) data end;
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   346
    val c_req = (Library.flat o map get_c_req) sort;
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   347
    fun get_remove_contraint c thy =
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   348
      let
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   349
        val ty1 = Sign.the_const_constraint thy c;
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   350
        val ty2 = Sign.the_const_type thy c;
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   351
      in
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   352
        thy
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   353
        |> Sign.add_const_constraint_i (c, ty2)
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   354
        |> pair (c, ty1)
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   355
      end;
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   356
    fun check_defs raw_defs c_req thy =
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   357
      let
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   358
        val thy' = thy |> Theory.copy |> Sign.add_arities_i [(tyco, asorts, sort)];
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   359
        fun get_c raw_def =
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   360
          (fst o Sign.cert_def pp o snd o tap_def thy' o fst) raw_def;
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   361
        val c_given = map get_c raw_defs;
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   362
(*         spec_opt_name   *)
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   363
        fun eq_c ((c1, ty1), (c2, ty2)) =
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   364
          let
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   365
            val ty1' = Type.varifyT ty1;
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   366
            val ty2' = Type.varifyT ty2;
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   367
          in
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   368
            c1 = c2
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   369
            andalso Sign.typ_instance thy (ty1', ty2')
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   370
            andalso Sign.typ_instance thy (ty2', ty1')
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   371
          end;
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   372
        val _ = case fold (remove eq_c) c_req c_given
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   373
         of [] => ()
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   374
          | cs => error ("superfluous definition(s) given for "
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   375
                    ^ (commas o map (fn (c, ty) => quote (c ^ "::" ^ Sign.string_of_typ thy ty))) cs);
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   376
        (*val _ = case fold (remove eq_c) c_given c_req
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   377
      of [] => ()
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   378
          | cs => error ("no definition(s) given for "
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   379
                    ^ (commas o map (fn (c, ty) => quote (c ^ "::" ^ Sign.string_of_typ thy ty))) cs);*)
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   380
      in thy end;
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   381
    fun after_qed cs =
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   382
      fold Sign.add_const_constraint_i cs
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   383
      #> fold (fn class => add_inst_data (class, (tyco, Context.theory_name thy))) sort;
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   384
  in
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   385
    thy
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   386
    |> tap (fn thy => check_defs raw_defs c_req thy)
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   387
    |> fold_map get_remove_contraint (map fst c_req)
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   388
    ||> add_defs (true, raw_defs)
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   389
    |-> (fn cs => AxClass.instance_arity_i (after_qed cs) arity)
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   390
  end;
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   391
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   392
val add_instance_arity = gen_instance_arity (AxClass.read_arity) IsarThy.add_defs read_axm;
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   393
val add_instance_arity_i = gen_instance_arity (AxClass.cert_arity) IsarThy.add_defs_i (K I);
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   394
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   395
18168
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   396
(* extracting dictionary obligations from types *)
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   397
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   398
type sortcontext = (string * sort) list;
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   399
18335
99baddf6b0d0 various improvements
haftmann
parents: 18330
diff changeset
   400
fun extract_sortctxt thy ty =
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   401
  (typ_tfrees o fst o Type.freeze_thaw_type) ty
18884
df1e3c93c50a name clarifications
haftmann
parents: 18864
diff changeset
   402
  |> map (apsnd (operational_sort_of thy))
18168
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   403
  |> filter (not o null o snd);
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   404
18884
df1e3c93c50a name clarifications
haftmann
parents: 18864
diff changeset
   405
datatype classlookup = Instance of (class * string) * classlookup list list
18168
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   406
                    | Lookup of class list * (string * int)
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   407
18864
a87c0aeae92f more coherent lookup extraction functions
haftmann
parents: 18849
diff changeset
   408
fun extract_lookup thy sortctxt raw_typ_def raw_typ_use =
18168
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   409
  let
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   410
    val typ_def = Type.varifyT raw_typ_def;
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   411
    val typ_use = Type.varifyT raw_typ_use;
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   412
    val match_tab = Sign.typ_match thy (typ_def, typ_use) Vartab.empty;
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   413
    fun tab_lookup vname = (the o Vartab.lookup match_tab) (vname, 0);
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   414
    fun get_superclass_derivation (subclasses, superclass) =
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   415
      (the oo get_first) (fn subclass =>
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   416
        Sorts.class_le_path (Sign.classes_of thy) (subclass, superclass)
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   417
      ) subclasses;
18884
df1e3c93c50a name clarifications
haftmann
parents: 18864
diff changeset
   418
    fun find_index_class subclass subclasses =
df1e3c93c50a name clarifications
haftmann
parents: 18864
diff changeset
   419
      let
df1e3c93c50a name clarifications
haftmann
parents: 18864
diff changeset
   420
        val i = find_index_eq subclass subclasses;
df1e3c93c50a name clarifications
haftmann
parents: 18864
diff changeset
   421
        val _ = if i < 0 then error "could not find class" else ();
df1e3c93c50a name clarifications
haftmann
parents: 18864
diff changeset
   422
      in case subclasses
df1e3c93c50a name clarifications
haftmann
parents: 18864
diff changeset
   423
       of [_] => ~1
df1e3c93c50a name clarifications
haftmann
parents: 18864
diff changeset
   424
        | _ => i
df1e3c93c50a name clarifications
haftmann
parents: 18864
diff changeset
   425
      end;
18168
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   426
    fun mk_class_deriv thy subclasses superclass =
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   427
      case get_superclass_derivation (subclasses, superclass)
18515
1cad5c2b2a0b substantial improvements in code generating
haftmann
parents: 18380
diff changeset
   428
      of (subclass::deriv) =>
18884
df1e3c93c50a name clarifications
haftmann
parents: 18864
diff changeset
   429
        ((rev o filter (is_class thy)) deriv, find_index_class subclass subclasses);
18168
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   430
    fun mk_lookup (sort_def, (Type (tycon, tys))) =
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   431
          let
18330
444f16d232a2 introduced new map2, fold
haftmann
parents: 18304
diff changeset
   432
            val arity_lookup = map2 (curry mk_lookup)
18884
df1e3c93c50a name clarifications
haftmann
parents: 18864
diff changeset
   433
              (map (operational_sort_of thy) (Sorts.mg_domain (Sign.classes_arities_of thy) tycon sort_def)) tys
18168
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   434
          in map (fn class => Instance ((class, tycon), arity_lookup)) sort_def end
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   435
      | mk_lookup (sort_def, TVar ((vname, _), sort_use)) =
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   436
          let
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   437
            fun mk_look class =
18884
df1e3c93c50a name clarifications
haftmann
parents: 18864
diff changeset
   438
              let val (deriv, classindex) = mk_class_deriv thy (operational_sort_of thy sort_use) class
18168
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   439
              in Lookup (deriv, (vname, classindex)) end;
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   440
          in map mk_look sort_def end;
18864
a87c0aeae92f more coherent lookup extraction functions
haftmann
parents: 18849
diff changeset
   441
  in
a87c0aeae92f more coherent lookup extraction functions
haftmann
parents: 18849
diff changeset
   442
    sortctxt
a87c0aeae92f more coherent lookup extraction functions
haftmann
parents: 18849
diff changeset
   443
    |> map (tab_lookup o fst)
18884
df1e3c93c50a name clarifications
haftmann
parents: 18864
diff changeset
   444
    |> map (apfst (operational_sort_of thy))
18864
a87c0aeae92f more coherent lookup extraction functions
haftmann
parents: 18849
diff changeset
   445
    |> filter (not o null o fst)
a87c0aeae92f more coherent lookup extraction functions
haftmann
parents: 18849
diff changeset
   446
    |> map mk_lookup
a87c0aeae92f more coherent lookup extraction functions
haftmann
parents: 18849
diff changeset
   447
  end;
a87c0aeae92f more coherent lookup extraction functions
haftmann
parents: 18849
diff changeset
   448
18884
df1e3c93c50a name clarifications
haftmann
parents: 18864
diff changeset
   449
fun extract_classlookup thy (c, raw_typ_use) =
18864
a87c0aeae92f more coherent lookup extraction functions
haftmann
parents: 18849
diff changeset
   450
  let
a87c0aeae92f more coherent lookup extraction functions
haftmann
parents: 18849
diff changeset
   451
    val raw_typ_def = Sign.the_const_constraint thy c;
a87c0aeae92f more coherent lookup extraction functions
haftmann
parents: 18849
diff changeset
   452
    val typ_def = Type.varifyT raw_typ_def;
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   453
    fun reorder_sortctxt ctxt =
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   454
      case lookup_const_class thy c
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   455
       of NONE => ctxt
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   456
        | SOME class =>
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   457
            let
19038
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   458
              val data = the_class_data thy class;
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   459
              val sign = (Type.varifyT o the o AList.lookup (op =) (#consts data)) c;
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   460
              val match_tab = Sign.typ_match thy (sign, typ_def) Vartab.empty;
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   461
              val v : string = case Vartab.lookup match_tab (#var data, 0)
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   462
                of SOME (_, TVar ((v, _), _)) => v;
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   463
            in
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   464
              (v, (the o AList.lookup (op =) ctxt) v) :: AList.delete (op =) v ctxt
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   465
            end;
18168
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   466
  in
18864
a87c0aeae92f more coherent lookup extraction functions
haftmann
parents: 18849
diff changeset
   467
    extract_lookup thy
a87c0aeae92f more coherent lookup extraction functions
haftmann
parents: 18849
diff changeset
   468
      (reorder_sortctxt (extract_sortctxt thy ((fst o Type.freeze_thaw_type) raw_typ_def)))
a87c0aeae92f more coherent lookup extraction functions
haftmann
parents: 18849
diff changeset
   469
      raw_typ_def raw_typ_use
18168
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   470
  end;
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   471
18884
df1e3c93c50a name clarifications
haftmann
parents: 18864
diff changeset
   472
fun extract_classlookup_inst thy (class, tyco) supclass =
18864
a87c0aeae92f more coherent lookup extraction functions
haftmann
parents: 18849
diff changeset
   473
  let
a87c0aeae92f more coherent lookup extraction functions
haftmann
parents: 18849
diff changeset
   474
    fun mk_typ class = Type (tyco, (map TFree o fst o the_inst_sign thy) (class, tyco))
a87c0aeae92f more coherent lookup extraction functions
haftmann
parents: 18849
diff changeset
   475
    val typ_def = mk_typ class;
a87c0aeae92f more coherent lookup extraction functions
haftmann
parents: 18849
diff changeset
   476
    val typ_use = mk_typ supclass;
a87c0aeae92f more coherent lookup extraction functions
haftmann
parents: 18849
diff changeset
   477
  in
a87c0aeae92f more coherent lookup extraction functions
haftmann
parents: 18849
diff changeset
   478
    extract_lookup thy (extract_sortctxt thy typ_def) typ_def typ_use
a87c0aeae92f more coherent lookup extraction functions
haftmann
parents: 18849
diff changeset
   479
  end;
18168
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   480
18884
df1e3c93c50a name clarifications
haftmann
parents: 18864
diff changeset
   481
18335
99baddf6b0d0 various improvements
haftmann
parents: 18330
diff changeset
   482
(* intermediate auxiliary *)
18168
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   483
18849
05a16861d3a5 added three times overloaded Isar instance command
haftmann
parents: 18829
diff changeset
   484
fun add_classentry raw_class raw_cs thy =
18168
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   485
  let
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   486
    val class = Sign.intern_class thy raw_class;
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   487
    val cs_proto =
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   488
      raw_cs
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   489
      |> map (Sign.intern_const thy)
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   490
      |> map (fn c => (c, Sign.the_const_constraint thy c));
19038
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   491
    val used =
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   492
      []
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   493
      |> fold (fn (_, ty) => curry (gen_union (op =))
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   494
           ((map (fst o fst) o typ_tvars) ty @ (map fst o typ_tfrees) ty)) cs_proto
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   495
    val v = hd (Term.invent_names used "'a" 1);
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   496
    val cs =
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   497
      cs_proto
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   498
      |> map (fn (c, ty) => (c, map_type_tvar (fn var as ((tvar', _), sort) =>
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   499
          if Sorts.sort_eq (Sign.classes_of thy) ([class], sort)
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   500
          then TFree (v, [])
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   501
          else TVar var
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   502
         ) ty));
18168
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   503
  in
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   504
    thy
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18670
diff changeset
   505
    |> add_class_data (class, ([], "", class, v, cs))
18849
05a16861d3a5 added three times overloaded Isar instance command
haftmann
parents: 18829
diff changeset
   506
  end;
05a16861d3a5 added three times overloaded Isar instance command
haftmann
parents: 18829
diff changeset
   507
05a16861d3a5 added three times overloaded Isar instance command
haftmann
parents: 18829
diff changeset
   508
fun add_classinsts raw_class raw_insts thy =
05a16861d3a5 added three times overloaded Isar instance command
haftmann
parents: 18829
diff changeset
   509
  let
05a16861d3a5 added three times overloaded Isar instance command
haftmann
parents: 18829
diff changeset
   510
    val class = Sign.intern_class thy raw_class;
05a16861d3a5 added three times overloaded Isar instance command
haftmann
parents: 18829
diff changeset
   511
    val insts = map (rpair (Context.theory_name thy) o Sign.intern_type thy) raw_insts;
05a16861d3a5 added three times overloaded Isar instance command
haftmann
parents: 18829
diff changeset
   512
  in
05a16861d3a5 added three times overloaded Isar instance command
haftmann
parents: 18829
diff changeset
   513
    thy
18575
9ccfd1d1e874 substantial additions using locales
haftmann
parents: 18550
diff changeset
   514
    |> fold (curry add_inst_data class) insts
18335
99baddf6b0d0 various improvements
haftmann
parents: 18330
diff changeset
   515
  end;
18515
1cad5c2b2a0b substantial improvements in code generating
haftmann
parents: 18380
diff changeset
   516
1cad5c2b2a0b substantial improvements in code generating
haftmann
parents: 18380
diff changeset
   517
(* toplevel interface *)
1cad5c2b2a0b substantial improvements in code generating
haftmann
parents: 18380
diff changeset
   518
1cad5c2b2a0b substantial improvements in code generating
haftmann
parents: 18380
diff changeset
   519
local
1cad5c2b2a0b substantial improvements in code generating
haftmann
parents: 18380
diff changeset
   520
1cad5c2b2a0b substantial improvements in code generating
haftmann
parents: 18380
diff changeset
   521
structure P = OuterParse
1cad5c2b2a0b substantial improvements in code generating
haftmann
parents: 18380
diff changeset
   522
and K = OuterKeyword
1cad5c2b2a0b substantial improvements in code generating
haftmann
parents: 18380
diff changeset
   523
1cad5c2b2a0b substantial improvements in code generating
haftmann
parents: 18380
diff changeset
   524
in
1cad5c2b2a0b substantial improvements in code generating
haftmann
parents: 18380
diff changeset
   525
18849
05a16861d3a5 added three times overloaded Isar instance command
haftmann
parents: 18829
diff changeset
   526
val (classK, instanceK) = ("class", "instance")
18515
1cad5c2b2a0b substantial improvements in code generating
haftmann
parents: 18380
diff changeset
   527
18911
74edab16166f alternative syntax for instances
haftmann
parents: 18884
diff changeset
   528
val parse_inst =
74edab16166f alternative syntax for instances
haftmann
parents: 18884
diff changeset
   529
  P.xname -- (
74edab16166f alternative syntax for instances
haftmann
parents: 18884
diff changeset
   530
    Scan.repeat P.sort --| P.$$$ "::" -- P.sort
74edab16166f alternative syntax for instances
haftmann
parents: 18884
diff changeset
   531
    || P.$$$ "::" |-- P.!!! P.arity
74edab16166f alternative syntax for instances
haftmann
parents: 18884
diff changeset
   532
  )
74edab16166f alternative syntax for instances
haftmann
parents: 18884
diff changeset
   533
  >> (fn (tyco, (asorts, sort)) => ((tyco, asorts), sort))
74edab16166f alternative syntax for instances
haftmann
parents: 18884
diff changeset
   534
19038
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   535
val locale_val =
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   536
  (P.locale_expr --
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   537
    Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 P.context_element)) [] ||
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   538
  Scan.repeat1 P.context_element >> pair Locale.empty);
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   539
18515
1cad5c2b2a0b substantial improvements in code generating
haftmann
parents: 18380
diff changeset
   540
val classP =
18849
05a16861d3a5 added three times overloaded Isar instance command
haftmann
parents: 18829
diff changeset
   541
  OuterSyntax.command classK "operational type classes" K.thy_decl (
05a16861d3a5 added three times overloaded Isar instance command
haftmann
parents: 18829
diff changeset
   542
    P.name --| P.$$$ "="
05a16861d3a5 added three times overloaded Isar instance command
haftmann
parents: 18829
diff changeset
   543
    -- Scan.optional (Scan.repeat1 (P.name --| P.$$$ "+")) []
05a16861d3a5 added three times overloaded Isar instance command
haftmann
parents: 18829
diff changeset
   544
    -- Scan.optional (P.!!! (Scan.repeat1 P.context_element)) []
18515
1cad5c2b2a0b substantial improvements in code generating
haftmann
parents: 18380
diff changeset
   545
      >> (Toplevel.theory_context
18804
d42708f5c186 swapped Toplevel.theory_context;
wenzelm
parents: 18755
diff changeset
   546
          o (fn ((bname, supclasses), elems) => add_class bname supclasses elems)));
18515
1cad5c2b2a0b substantial improvements in code generating
haftmann
parents: 18380
diff changeset
   547
18918
5590770e1b09 minor improvements
haftmann
parents: 18911
diff changeset
   548
val classP_exp =
5590770e1b09 minor improvements
haftmann
parents: 18911
diff changeset
   549
  OuterSyntax.command (classK ^ "_exp") "operational type classes" K.thy_goal (
5590770e1b09 minor improvements
haftmann
parents: 18911
diff changeset
   550
    P.name --| P.$$$ "="
5590770e1b09 minor improvements
haftmann
parents: 18911
diff changeset
   551
    -- Scan.optional (Scan.repeat1 (P.name --| P.$$$ "+")) []
5590770e1b09 minor improvements
haftmann
parents: 18911
diff changeset
   552
    -- Scan.optional (P.!!! (Scan.repeat1 P.context_element)) []
19038
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 18963
diff changeset
   553
      >> ((Toplevel.print oo Toplevel.theory_to_proof)
18918
5590770e1b09 minor improvements
haftmann
parents: 18911
diff changeset
   554
          o (fn ((bname, supclasses), elems) => add_class_exp bname supclasses elems)));
5590770e1b09 minor improvements
haftmann
parents: 18911
diff changeset
   555
18575
9ccfd1d1e874 substantial additions using locales
haftmann
parents: 18550
diff changeset
   556
val instanceP =
18849
05a16861d3a5 added three times overloaded Isar instance command
haftmann
parents: 18829
diff changeset
   557
  OuterSyntax.command instanceK "prove type arity or subclass relation" K.thy_goal ((
05a16861d3a5 added three times overloaded Isar instance command
haftmann
parents: 18829
diff changeset
   558
      P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) >> AxClass.instance_subclass
18911
74edab16166f alternative syntax for instances
haftmann
parents: 18884
diff changeset
   559
      || parse_inst -- Scan.repeat P.spec_name
74edab16166f alternative syntax for instances
haftmann
parents: 18884
diff changeset
   560
           >> (fn (((tyco, asorts), sort), []) => AxClass.instance_arity I (tyco, asorts, sort)
74edab16166f alternative syntax for instances
haftmann
parents: 18884
diff changeset
   561
                | (inst, defs) => add_instance_arity inst defs)
18849
05a16861d3a5 added three times overloaded Isar instance command
haftmann
parents: 18829
diff changeset
   562
    ) >> (Toplevel.print oo Toplevel.theory_to_proof));
18575
9ccfd1d1e874 substantial additions using locales
haftmann
parents: 18550
diff changeset
   563
18918
5590770e1b09 minor improvements
haftmann
parents: 18911
diff changeset
   564
val _ = OuterSyntax.add_parsers [classP, classP_exp, instanceP];
18515
1cad5c2b2a0b substantial improvements in code generating
haftmann
parents: 18380
diff changeset
   565
1cad5c2b2a0b substantial improvements in code generating
haftmann
parents: 18380
diff changeset
   566
end; (* local *)
1cad5c2b2a0b substantial improvements in code generating
haftmann
parents: 18380
diff changeset
   567
18168
d35daf321b8a class_package - operational view on type classes
haftmann
parents:
diff changeset
   568
end; (* struct *)