wneuper/isa: comparison src/Pure/Tools/class

equal deleted inserted replaced

-:98e6a0a011f3
+:7dc7dcd63224
 -> theory -> Proof.state
 val add_instance_arity_i: (string * sort list) * sort
 -> ((bstring * term) * theory attribute list) list
 -> theory -> Proof.state
 val add_classentry: class -> xstring list -> xstring list -> theory -> theory
-val the_consts: theory -> class -> string list
-val the_tycos: theory -> class -> (string * string) list
+val syntactic_sort_of: theory -> sort -> sort
+val the_superclasses: theory -> class -> class list
+val the_consts_sign: theory -> class -> string * (string * typ) list
+val lookup_const_class: theory -> string -> class option
+val the_instances: theory -> class -> (string * string) list
+val the_inst_sign: theory -> class * string -> (string * sort) list * (string * typ) list
+val get_classtab: theory -> (string list * (string * string) list) Symtab.table
 val print_classes: theory -> unit
-val syntactic_sort_of: theory -> sort -> sort
-val get_arities: theory -> sort -> string -> sort list
-val get_superclasses: theory -> class -> class list
-val get_const_sign: theory -> string -> string -> typ
-val get_inst_consts_sign: theory -> string * class -> (string * typ) list
-val lookup_const_class: theory -> string -> class option
-val get_classtab: theory -> (string list * (string * string) list) Symtab.table
 type sortcontext = (string * sort) list
 datatype sortlookup = Instance of (class * string) * sortlookup list list
 | Lookup of class list * (string * int)
 val extract_sortctxt: theory -> typ -> sortcontext
-val extract_sortlookup: theory -> typ * typ -> sortlookup list list
+val extract_sortlookup: theory -> string * typ -> sortlookup list list
 end;
 structure ClassPackage: CLASS_PACKAGE =
 struct
 var = var,
 consts = consts,
 insts = insts @ [inst]
 });
-val the_consts = map fst o #consts oo get_class_data;
-val the_tycos = #insts oo get_class_data;
 (* classes and instances *)
+fun subst_clsvar v ty_subst =
+map_type_tfree (fn u as (w, _) =>
+if w = v then ty_subst else TFree u);
 local
 open Element
 fun gen_add_class add_locale bname raw_import raw_body thy =
 let
-fun subst_clsvar v ty_subst =
-map_type_tfree (fn u as (w, _) =>
-if w = v then ty_subst else TFree u);
 fun extract_assumes c_adds elems =
 let
 fun subst_free ts =
 let
 val get_ty = the o AList.lookup (op =) (fold Term.add_frees ts []);
 |> pair (c, ty1)
 end;
 fun get_c_given thy = map (fst o dest_def o snd o tap_def thy o fst) raw_defs;
 fun check_defs c_given c_req thy =
 let
-fun eq_c ((c1, ty1), (c2, ty2)) = c1 = c2 andalso Sign.typ_instance thy (ty1, ty2)
+fun eq_c ((c1, ty1), (c2, ty2)) = c1 = c2
+andalso Sign.typ_instance thy (ty1, ty2)
+andalso Sign.typ_instance thy (ty2, ty1)
 val _ = case fold (remove eq_c) c_given c_req
 of [] => ()
 | cs => error ("no definition(s) given for"
 ^ (commas o map (fn (c, ty) => quote (c ^ "::" ^ Sign.string_of_typ thy ty))) cs);
 val _ = case fold (remove eq_c) c_req c_given
 val add_instance_arity = fn x => gen_instance_arity (AxClass.read_arity) IsarThy.add_defs read_axm x;
 val add_instance_arity_i = fn x => gen_instance_arity (AxClass.cert_arity) IsarThy.add_defs_i (K I) x;
-(* class queries *)
+(* queries *)
-fun is_class thy cls = lookup_class_data thy cls |> Option.map (not o null o #consts) |> the_default false;
+fun is_class thy cls =
+lookup_class_data thy cls
+|> Option.map (not o null o #consts)
+|> the_default false;
 fun syntactic_sort_of thy sort =
 let
 val classes = Sign.classes_of thy;
 fun get_sort cls =
 map get_sort sort
 |> Library.flat
 |> Sorts.norm_sort classes
 end;
-fun get_arities thy sort tycon =
+fun the_superclasses thy class =
-Sorts.mg_domain (Sign.classes_arities_of thy) tycon (syntactic_sort_of thy sort)
-|> map (syntactic_sort_of thy);
-fun get_superclasses thy class =
 if is_class thy class
 then
 Sorts.superclasses (Sign.classes_of thy) class
 |> syntactic_sort_of thy
 else
 error ("no syntactic class: " ^ class);
+fun the_consts_sign thy class =
-(* instance queries *)
+let
+val data = (the oo Symtab.lookup) ((fst o ClassData.get) thy) class
-fun mk_const_sign thy class tvar ty =
+in (#var data, #consts data) end;
-let
-val (ty', thaw) = Type.freeze_thaw_type ty;
+fun lookup_const_class thy =
-val tvars_used = Term.add_tfreesT ty' [];
+Symtab.lookup ((snd o ClassData.get) thy);
-val tvar_rename = hd (Term.invent_names (map fst tvars_used) tvar 1);
-in
+fun the_instances thy class =
-ty'
+(#insts o the o Symtab.lookup ((fst o ClassData.get) thy)) class;
-|> map_type_tfree (fn (tvar', sort) =>
-if Sorts.sort_eq (Sign.classes_of thy) ([class], sort)
+fun the_inst_sign thy (class, tyco) =
-then TFree (tvar, [])
+let
-else if tvar' = tvar
+val _ = if is_class thy class then () else error ("no syntactic class: " ^ class);
-then TVar ((tvar_rename, 0), sort)
+val arity =
-else TFree (tvar', sort))
+Sorts.mg_domain (Sign.classes_arities_of thy) tyco [class]
-|> thaw
+|> map (syntactic_sort_of thy);
-end;
+val clsvar = (#var o the o Symtab.lookup ((fst o ClassData.get) thy)) class;
+val const_sign = (snd o the_consts_sign thy) class;
-fun get_const_sign thy tvar const =
+fun add_var sort used =
 let
-val class = (the o lookup_const_class thy) const;
+val v = hd (Term.invent_names used "'a" 1)
-val ty = Sign.the_const_constraint thy const;
+in ((v, sort), v::used) end;
-in mk_const_sign thy class tvar ty end;
+val (vsorts, _) =
+[]
-fun get_inst_consts_sign thy (tyco, class) =
+|> fold (fn (_, ty) => curry (gen_union (op =))
-let
+((map (fst o fst) o typ_tvars) ty @ (map fst o typ_tfrees) ty)) const_sign
-val consts = the_consts thy class;
+|> fold_map add_var arity;
-val arities = get_arities thy [class] tyco;
+val ty_inst = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) vsorts);
-val const_signs = map (get_const_sign thy "'a") consts;
+val inst_signs = map (apsnd (subst_clsvar clsvar ty_inst)) const_sign;
-val vars_used = fold (fn ty => curry (gen_union (op =))
+in (vsorts, inst_signs) end;
-(map fst (typ_tfrees ty) |> remove (op =) "'a")) const_signs [];
-val vars_new = Term.invent_names vars_used "'a" (length arities);
-val typ_arity = Type (tyco, map2 (curry TFree) vars_new arities);
-val instmem_signs =
-map (typ_subst_TVars [(("'a", 0), typ_arity)]) const_signs;
-in consts ~~ instmem_signs end;
 fun get_classtab thy =
 Symtab.fold
 (fn (class, { consts = consts, insts = insts, ... }) =>
 Symtab.update_new (class, (map fst consts, insts)))
-(fst (ClassData.get thy)) Symtab.empty;
+((fst o ClassData.get) thy) Symtab.empty;
 (* extracting dictionary obligations from types *)
 type sortcontext = (string * sort) list;
 fun extract_sortctxt thy ty =
-(typ_tfrees o Type.no_tvars) ty
+(typ_tfrees o fst o Type.freeze_thaw_type) ty
 |> map (apsnd (syntactic_sort_of thy))
 |> filter (not o null o snd);
 datatype sortlookup = Instance of (class * string) * sortlookup list list
 | Lookup of class list * (string * int)
-fun extract_sortlookup thy (raw_typ_def, raw_typ_use) =
+fun extract_sortlookup thy (c, raw_typ_use) =
 let
+val raw_typ_def = Sign.the_const_constraint thy c;
 val typ_def = Type.varifyT raw_typ_def;
 val typ_use = Type.varifyT raw_typ_use;
 val match_tab = Sign.typ_match thy (typ_def, typ_use) Vartab.empty;
 fun tab_lookup vname = (the o Vartab.lookup match_tab) (vname, 0);
 fun get_superclass_derivation (subclasses, superclass) =
 let
 fun mk_look class =
 let val (deriv, classindex) = mk_class_deriv thy (syntactic_sort_of thy sort_use) class
 in Lookup (deriv, (vname, classindex)) end;
 in map mk_look sort_def end;
+fun reorder_sortctxt ctxt =
+case lookup_const_class thy c
+of NONE => ctxt
+| SOME class =>
+let
+val data = (the o Symtab.lookup ((fst o ClassData.get) thy)) class;
+val sign = (Type.varifyT o the o AList.lookup (op =) (#consts data)) c;
+val match_tab = Sign.typ_match thy (sign, typ_def) Vartab.empty;
+val v : string = case Vartab.lookup match_tab (#var data, 0)
+of SOME (_, TVar ((v, _), _)) => v;
+in
+(v, (the o AList.lookup (op =) ctxt) v) :: AList.delete (op =) v ctxt
+end;
 in
 extract_sortctxt thy ((fst o Type.freeze_thaw_type) raw_typ_def)
+|> reorder_sortctxt
 |> map (tab_lookup o fst)
 |> map (apfst (syntactic_sort_of thy))
 |> filter (not o null o fst)
 |> map mk_lookup
 end;
 (* intermediate auxiliary *)
 fun add_classentry raw_class raw_cs raw_insts thy =
 let
 val class = Sign.intern_class thy raw_class;
-val cs = raw_cs |> map (Sign.intern_const thy);
+val cs_proto =
+raw_cs
+|> map (Sign.intern_const thy)
+|> map (fn c => (c, Sign.the_const_constraint thy c));
+val used =
+[]
+|> fold (fn (_, ty) => curry (gen_union (op =))
+((map (fst o fst) o typ_tvars) ty @ (map fst o typ_tfrees) ty)) cs_proto
+val v = hd (Term.invent_names used "'a" 1);
+val cs =
+cs_proto
+|> map (fn (c, ty) => (c, map_type_tvar (fn var as ((tvar', _), sort) =>
+if Sorts.sort_eq (Sign.classes_of thy) ([class], sort)
+then TFree (v, [])
+else TVar var
+) ty));
 val insts = map (rpair (Context.theory_name thy) o Sign.intern_type thy) raw_insts;
 in
 thy
-|> add_class_data (class, ([], "", class, "", map (rpair dummyT) cs))
+|> add_class_data (class, ([], "", class, v, cs))
 |> fold (curry add_inst_data class) insts
 end;
 (* toplevel interface *)

changeset 18702	7dc7dcd63224
parent 18670	c3f445b92aff
child 18708	4b3dadb4fe33