# HG changeset patch # User haftmann # Date 1142342709 -3600 # Node ID f3ce97b5661aa032a10a6009e4c9f5b51f3fc18e # Parent 1f7c69a5faac414e3153394bdbbe199fb2787641 refined representation of instance dictionaries diff -r 1f7c69a5faac -r f3ce97b5661a src/Pure/Tools/class_package.ML --- a/src/Pure/Tools/class_package.ML Mon Mar 13 10:41:04 2006 +0100 +++ b/src/Pure/Tools/class_package.ML Tue Mar 14 14:25:09 2006 +0100 @@ -24,6 +24,8 @@ val instance_sort_i: class * sort -> theory -> Proof.state val prove_instance_sort: tactic -> class * sort -> theory -> theory + val use_cp_instance: bool ref; + val intern_class: theory -> xstring -> class val intern_sort: theory -> sort -> sort val extern_class: theory -> class -> xstring @@ -45,10 +47,11 @@ type sortcontext = (string * sort) list datatype classlookup = Instance of (class * string) * classlookup list list - | Lookup of class list * (string * int) + | Lookup of class list * (string * (int * int)) val extract_sortctxt: theory -> typ -> sortcontext val extract_classlookup: theory -> string * typ -> classlookup list list val extract_classlookup_inst: theory -> class * string -> class -> classlookup list list + val extract_classlookup_member: theory -> typ * typ -> classlookup list list end; structure ClassPackage: CLASS_PACKAGE = @@ -176,7 +179,7 @@ let val _ = if is_class thy class then () else error ("no syntactic class: " ^ class); val arity = - (fst o the o AList.lookup (op =) (the_instances thy class)) tyco + Sorts.mg_domain (Sign.classes_arities_of thy) tyco [class]; val clsvar = (#var o the_class_data thy) class; val const_sign = (snd o the_consts_sign thy) class; fun add_var sort used = @@ -497,11 +500,10 @@ |> Sign.add_const_constraint_i (c, NONE) |> pair (c, Type.unvarifyT ty) end; - fun check_defs raw_defs c_req thy = + fun check_defs0 thy raw_defs c_req = let - val thy' = (Sign.add_arities_i [(tyco, asorts, sort)] o Theory.copy) thy; fun get_c raw_def = - (fst o Sign.cert_def pp o tap_def thy' o snd) raw_def; + (fst o Sign.cert_def pp o tap_def thy o snd) raw_def; val c_given = map get_c raw_defs; fun eq_c ((c1, ty1), (c2, ty2)) = let @@ -509,18 +511,22 @@ val ty2' = Type.varifyT ty2; in c1 = c2 - andalso Sign.typ_instance thy' (ty1', ty2') - andalso Sign.typ_instance thy' (ty2', ty1') + andalso Sign.typ_instance thy (ty1', ty2') + andalso Sign.typ_instance thy (ty2', ty1') end; val _ = case fold (remove eq_c) c_req c_given of [] => () | cs => error ("superfluous definition(s) given for " - ^ (commas o map (fn (c, ty) => quote (c ^ "::" ^ Sign.string_of_typ thy' ty))) cs); + ^ (commas o map (fn (c, ty) => quote (c ^ "::" ^ Sign.string_of_typ thy ty))) cs); 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); - in thy end; + ^ (commas o map (fn (c, ty) => quote (c ^ "::" ^ Sign.string_of_typ thy ty))) cs); + in () end; + fun check_defs1 raw_defs c_req thy = + let + val thy' = (Sign.add_arities_i [(tyco, asorts, sort)] o Theory.copy) thy + in (check_defs0 thy' raw_defs c_req; thy) end; fun mangle_alldef_name tyco sort = Thm.def_name ((space_implode "_" o map NameSpace.base) sort ^ "_" ^ NameSpace.base tyco); fun note_all tyco sort thms thy = @@ -530,10 +536,12 @@ fun after_qed cs thy = thy |> fold Sign.add_const_constraint_i (map (apsnd SOME) cs) - |> fold (fn class => add_inst_data (class, (tyco, (asorts, Context.theory_name thy)))) sort; + |> fold (fn class => + add_inst_data (class, (tyco, + (map (operational_sort_of thy) asorts, Context.theory_name thy)))) sort; in theory - |> check_defs raw_defs cs + |> check_defs1 raw_defs cs |> fold_map get_remove_contraint (map fst cs) ||>> add_defs tyco (map (pair NONE) raw_defs) |-> (fn (cs, defnames) => note_all tyco sort defnames #> pair cs) @@ -629,15 +637,15 @@ |> filter (not o null o snd); datatype classlookup = Instance of (class * string) * classlookup list list - | Lookup of class list * (string * int) + | Lookup of class list * (string * (int * int)) fun pretty_lookup' (Instance ((class, tyco), lss)) = (Pretty.block o Pretty.breaks) ( Pretty.enum "," "{" "}" [Pretty.str class, Pretty.str tyco] :: map pretty_lookup lss ) - | pretty_lookup' (Lookup (classes, (v, i))) = - Pretty.enum " <" "[" "]" (map Pretty.str classes @ [Pretty.str (v ^ "!" ^ string_of_int i)]) + | pretty_lookup' (Lookup (classes, (v, (i, j)))) = + Pretty.enum " <" "[" "]" (map Pretty.str classes @ [Pretty.str (v ^ "!" ^ string_of_int i ^ "/" ^ string_of_int j)]) and pretty_lookup ls = (Pretty.enum "," "(" ")" o map pretty_lookup') ls; fun extract_lookup thy sortctxt raw_typ_def raw_typ_use = @@ -651,8 +659,7 @@ val (i, (subclass::deriv)) = (the oo get_index) (fn subclass => get_superclass_derivation thy (subclass, superclass) ) subclasses; - val i' = if length subclasses = 1 then ~1 else i; - in (rev deriv, i') end; + in (rev deriv, (i, length subclasses)) end; fun mk_lookup (sort_def, (Type (tyco, tys))) = map (fn class => Instance ((class, tyco), map2 (curry mk_lookup) @@ -705,6 +712,8 @@ extract_lookup thy (extract_sortctxt thy typ_def) typ_def typ_use end; +fun extract_classlookup_member thy (ty_decl, ty_use) = + extract_lookup thy (extract_sortctxt thy ty_decl) ty_decl ty_use; (* toplevel interface *) @@ -717,10 +726,13 @@ val (classK, instanceK) = ("class", "instance") +val use_cp_instance = ref false; + fun wrap_add_instance_subclass (class, sort) thy = case Sign.read_sort thy sort of [class'] => - if (is_some o lookup_class_data thy o Sign.intern_class thy) class + if ! use_cp_instance + andalso (is_some o lookup_class_data thy o Sign.intern_class thy) class andalso (is_some o lookup_class_data thy o Sign.intern_class thy) class' then instance_sort (class, sort) thy diff -r 1f7c69a5faac -r f3ce97b5661a src/Pure/Tools/codegen_package.ML --- a/src/Pure/Tools/codegen_package.ML Mon Mar 13 10:41:04 2006 +0100 +++ b/src/Pure/Tools/codegen_package.ML Tue Mar 14 14:25:09 2006 +0100 @@ -691,10 +691,10 @@ |> ensure_def_inst thy tabs inst ||>> (fold_map o fold_map) (exprgen_classlookup thy tabs) ls |-> (fn (inst, ls) => pair (Instance (inst, ls))) - | exprgen_classlookup thy tabs (ClassPackage.Lookup (clss, (v, i))) trns = + | exprgen_classlookup thy tabs (ClassPackage.Lookup (clss, (v, (i, j)))) trns = trns |> fold_map (ensure_def_class thy tabs) clss - |-> (fn clss => pair (Lookup (clss, (v |> unprefix "'", i)))) + |-> (fn clss => pair (Lookup (clss, (v |> unprefix "'", if j = 1 then ~1 else i)))) and mk_fun thy tabs restrict (c, ty1) trns = case get_first (fn (name, eqx) => (eqx (c, ty1))) (get_eqextrs thy tabs) of SOME ((eq_thms, default), ty2) => @@ -734,7 +734,7 @@ ||>> (exprsgen_eqs thy tabs o the_list o Option.map mk_default) default ||>> exprsgen_type thy tabs [ty3] ||>> fold_map (exprgen_tyvar_sort thy tabs) sortctxt - |-> (fn (((eqs, eq_default), [ty]), sortctxt) => (pair o SOME) (eqs @ eq_default, (sortctxt, ty))) + |-> (fn (((eqs, eq_default), [ty]), sortctxt) => (pair o SOME) ((eqs @ eq_default, (sortctxt, ty)), ty3)) end | NONE => (NONE, trns) and ensure_def_inst thy (tabs as (_, (insttab, _, _))) (cls, tyco) trns = @@ -754,8 +754,12 @@ fun gen_membr (m, ty) trns = trns |> mk_fun thy tabs true (m, ty) - |-> (fn SOME funn => pair (idf_of_name thy nsp_mem m, (idf_of_name thy nsp_instmem m, funn)) - | NONE => error ("could not derive definition for member " ^ quote m)); + |-> (fn NONE => error ("could not derive definition for member " ^ quote m) + | SOME (funn, ty_use) => + (fold_map o fold_map) (exprgen_classlookup thy tabs) + (ClassPackage.extract_classlookup_member thy (ty, ty_use)) + #-> (fn lss => + pair (idf_of_name thy nsp_mem m, ((idf_of_name thy nsp_instmem m, funn), lss)))); in trns |> debug 5 (fn _ => "trying defgen class instance for (" ^ quote cls @@ -786,7 +790,7 @@ of SOME (c, ty) => trns |> mk_fun thy tabs false (c, ty) - |-> (fn (SOME funn) => succeed (Fun funn) + |-> (fn SOME (funn, _) => succeed (Fun funn) | NONE => fail ("no defining equations found for " ^ quote c)) | NONE => trns @@ -908,7 +912,8 @@ (* function extractors *) fun eqextr_defs thy (deftab, _) (c, ty) = - Option.mapPartial (get_first (fn (ty', (thm, _)) => if eq_typ thy (ty, ty') + Option.mapPartial (get_first (fn (ty', (thm, _)) => + if eq_typ thy (ty, ty') then SOME ([thm], ty') else NONE )) (Symtab.lookup deftab c); diff -r 1f7c69a5faac -r f3ce97b5661a src/Pure/Tools/codegen_serializer.ML --- a/src/Pure/Tools/codegen_serializer.ML Mon Mar 13 10:41:04 2006 +0100 +++ b/src/Pure/Tools/codegen_serializer.ML Tue Mar 14 14:25:09 2006 +0100 @@ -407,7 +407,8 @@ str v, str ":", case sort - of [class] => mk_class v class + of [] => str "unit" + | [class] => mk_class v class | _ => Pretty.enum " *" "" "" (map (mk_class v) sort), str ")" ] @@ -437,7 +438,8 @@ | from_classlookup fxy (Lookup (classes, (v, i))) = from_lookup BR (string_of_int (i+1) :: classes) (str v) in case ls - of [l] => from_classlookup fxy l + of [] => str "()" + | [l] => from_classlookup fxy l | ls => (Pretty.list "(" ")" o map (from_classlookup NOBR)) ls end; fun ml_from_tycoexpr fxy (tyco, tys) = @@ -738,43 +740,46 @@ :: (str o resolv) supinst :: map (ml_from_sortlookup NOBR) lss ); - fun from_memdef (m, (m', def)) = + fun from_memdef (m, ((m', def), lss)) = (ml_from_funs [(m', def)], (Pretty.block o Pretty.breaks) ( ml_from_label m :: str "=" :: (str o resolv) m' - :: map (str o fst) arity + :: map (ml_from_sortlookup NOBR) lss )); + fun mk_corp rhs = + (Pretty.block o Pretty.breaks) ( + str definer + :: (str o resolv) name + :: map ml_from_tyvar arity + @ [str "=", rhs] + ); fun mk_memdefs supclassexprs [] = Pretty.enum "," "{" "};" ( supclassexprs - ) + ) |> mk_corp | mk_memdefs supclassexprs memdefs = let val (defs, assigns) = (split_list o map from_memdef) memdefs; in Pretty.chunks [ - [str ("let"), Pretty.fbrk, defs |> Pretty.chunks] - |> Pretty.block, - [str ("in "), Pretty.enum "," "{" "} : " - (supclassexprs @ assigns), - ml_from_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity]), - str " end;"] - |> Pretty.block - ] + Pretty.block [ + str "local", + Pretty.fbrk, + Pretty.chunks defs + ], + Pretty.block [str "in", Pretty.brk 1, + (mk_corp o Pretty.block o Pretty.breaks) [ + Pretty.enum "," "{" "}" (supclassexprs @ assigns), + str ":", + ml_from_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity]) + ] + ], + str "end; (* instance *)" + ] end; in - Pretty.block [ - (Pretty.block o Pretty.breaks) ( - str definer - :: (str o resolv) name - :: map ml_from_tyvar arity - ), - Pretty.brk 1, - str "=", - Pretty.brk 1, - mk_memdefs (map from_supclass suparities) memdefs - ] |> SOME + mk_memdefs (map from_supclass suparities) memdefs |> SOME end | ml_from_def (name, CodegenThingol.Classinstmember) = NONE; in case defs @@ -1071,7 +1076,7 @@ hs_from_type BR (tyco `%% map (ITyVar o fst) arity), str " where", Pretty.fbrk, - Pretty.chunks (map (fn (m, (_, (eqs, ty))) => hs_from_funeqs (m, (eqs, ty))) memdefs) + Pretty.chunks (map (fn (m, ((_, (eqs, ty)), _)) => hs_from_funeqs (m, (eqs, ty))) memdefs) ] |> SOME | hs_from_def (_, CodegenThingol.Classinstmember) = NONE diff -r 1f7c69a5faac -r f3ce97b5661a src/Pure/Tools/codegen_thingol.ML --- a/src/Pure/Tools/codegen_thingol.ML Mon Mar 13 10:41:04 2006 +0100 +++ b/src/Pure/Tools/codegen_thingol.ML Tue Mar 14 14:25:09 2006 +0100 @@ -75,7 +75,7 @@ | Classmember of class | Classinst of ((class * (string * (vname * sort) list)) * (class * (string * iclasslookup list list)) list) - * (string * (string * funn)) list + * (string * ((string * funn) * iclasslookup list list)) list | Classinstmember; type module; type transact; @@ -419,7 +419,7 @@ | Classmember of class | Classinst of ((class * (string * (vname * sort) list)) * (class * (string * iclasslookup list list)) list) - * (string * (string * funn)) list + * (string * ((string * funn) * iclasslookup list list)) list | Classinstmember; datatype node = Def of def | Module of node Graph.T; @@ -799,12 +799,12 @@ fun mk_memdef (m, (sortctxt, ty)) = case AList.lookup (op =) memdefs m of NONE => error ("missing definition for member " ^ quote m) - | SOME (m', (eqs, (sortctxt', ty'))) => + | SOME ((m', (eqs, (sortctxt', ty'))), lss) => let val sortctxt'' = sortctxt |> fold (fn v_sort => AList.update (op =) v_sort) arity; val ty'' = instant_itype (instant (v, tyco `%% map (ITyVar o fst) arity)) ty; in if eq_ityp ((sortctxt'', ty''), (sortctxt', ty')) - then (m, (m', (check_funeqs eqs, (sortctxt', ty')))) + then (m, ((m', (check_funeqs eqs, (sortctxt', ty'))), lss)) else error ("inconsistent type for member definition " ^ quote m ^ " [" ^ v ^ "]: " ^ (Pretty.output o Pretty.block o Pretty.breaks) [ @@ -839,8 +839,8 @@ ) membrs ) | postprocess_def (name, Classinst (_, memdefs)) = - (check_samemodule (name :: map (fst o snd) memdefs); - fold (fn (_, (m', _)) => + (check_samemodule (name :: map (fst o fst o snd) memdefs); + fold (fn (_, ((m', _), _)) => add_def_incr (m', Classinstmember) ) memdefs )