# HG changeset patch # User haftmann # Date 1135693480 -3600 # Node ID 1cad5c2b2a0bc112c0ba3ad9c902fc6bc19b3ea4 # Parent 0cec730b39426a0194ce56e30e7518b86f61bef8 substantial improvements in code generating diff -r 0cec730b3942 -r 1cad5c2b2a0b src/Pure/Tools/class_package.ML --- a/src/Pure/Tools/class_package.ML Tue Dec 27 15:24:23 2005 +0100 +++ b/src/Pure/Tools/class_package.ML Tue Dec 27 15:24:40 2005 +0100 @@ -7,7 +7,11 @@ signature CLASS_PACKAGE = sig - val add_classentry: class -> string list -> string list -> theory -> theory + val add_class: bstring -> Locale.expr -> Element.context list -> theory + -> ProofContext.context * theory + val add_class_i: bstring -> Locale.expr -> Element.context_i list -> theory + -> ProofContext.context * theory + 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 @@ -65,6 +69,8 @@ ClassesData.map (apfst (Symtab.update (class, data))); fun add_const class const = ClassesData.map (apsnd (Symtab.update (const, class))); +val the_consts = #consts oo get_class_data; +val the_tycos = #tycos oo get_class_data; (* name mangling *) @@ -76,67 +82,91 @@ #axclass_name (get_class_data thy class); -(* assign consts to type classes *) +(* classes *) local -fun gen_add_consts prep_class prep_const (raw_class, raw_consts_new) thy = +open Element + +fun gen_add_class add_locale bname raw_import raw_body thy = let - val class = prep_class thy raw_class; - val consts_new = map (prep_const thy) raw_consts_new; - val {locale_name, axclass_name, consts, tycos} = - get_class_data thy class; + fun extract_notes_consts thy elems = + elems + |> List.mapPartial + (fn (Notes notes) => SOME notes + | _ => NONE) + |> Library.flat + |> map (fn (_, facts) => map fst facts) + |> Library.flat o Library.flat + |> map prop_of + |> (fn ts => fold (curry add_term_consts) ts []) + |> tap (writeln o commas); + fun extract_tyvar_name thy tys = + fold (curry add_typ_tfrees) tys [] + |> (fn [(v, [])] => v + | [(v, sort)] => + if Sorts.sort_eq (Sign.classes_of thy) (Sign.defaultS thy, sort) + then v + else error ("sort constraint on class type variable: " ^ Sign.string_of_sort thy sort) + | [] => error ("no class type variable") + | vs => error ("more than one type variable: " ^ (commas o map (Sign.string_of_typ thy o TFree)) vs)) + fun extract_tyvar_consts thy elems = + elems + |> List.mapPartial + (fn (Fixes consts) => SOME consts + | _ => NONE) + |> Library.flat + |> map (fn (c, ty, syn) => ((c, the ty), the syn)) + |> `(fn consts => extract_tyvar_name thy (map (snd o fst) consts)); + (* fun remove_local_syntax ((c, ty), _) thy = + thy + |> Sign.add_syntax_i [(c, ty, Syntax.NoSyn)]; *) + fun add_global_const ((c, ty), syn) thy = + thy + |> Sign.add_consts_i [(c, ty, syn)] + |> `(fn thy => Sign.intern_const thy c) + fun add_axclass bname_axiom locale_pred cs thy = + thy + |> AxClass.add_axclass_i (bname, Sign.defaultS thy) + [Thm.no_attributes (bname_axiom, + Const (ObjectLogic.judgment_name thy, dummyT) $ + list_comb (Const (locale_pred, dummyT), map (fn c => Const (c, dummyT)) cs) + |> curry (inferT_axm thy) "locale_pred" |> snd)] + |-> (fn _ => `(fn thy => Sign.intern_class thy bname)) + fun print_ctxt ctxt elem = + map Pretty.writeln (Element.pretty_ctxt ctxt elem) in thy - |> put_class_data class { - locale_name = locale_name, - axclass_name = axclass_name, - consts = consts @ consts_new, - tycos = tycos - } - |> fold (add_const class) consts_new + |> add_locale bname raw_import raw_body + |-> (fn (elems : context_i list, ctxt) => + tap (fn _ => map (print_ctxt ctxt) elems) + #> tap (fn thy => extract_notes_consts thy elems) + #> `(fn thy => Locale.intern thy bname) + #-> (fn name_locale => + `(fn thy => extract_tyvar_consts thy elems) + #-> (fn (v, consts) => + fold_map add_global_const consts + #-> (fn cs => + add_axclass (bname ^ "_intro") name_locale cs + #-> (fn name_axclass => + put_class_data name_locale { + locale_name = name_locale, + axclass_name = name_axclass, + consts = cs, + tycos = [] + }) + #> fold (add_const name_locale) cs + #> pair ctxt + )))) end; in -val add_consts = gen_add_consts Sign.intern_class Sign.intern_const; -val add_consts_i = gen_add_consts (K I) (K I); +val add_class = gen_add_class (Locale.add_locale_context true); +val add_class_i = gen_add_class (Locale.add_locale_context_i true); end; (* local *) -val the_consts = #consts oo get_class_data; - - -(* assign type constructors to type classes *) - -local - -fun gen_add_tycos prep_class prep_type (raw_class, raw_tycos_new) thy = - let - val class = prep_class thy raw_class - val tycos_new = map (prep_type thy) raw_tycos_new - val {locale_name, axclass_name, consts, tycos} = - get_class_data thy class - in - thy - |> put_class_data class { - locale_name = locale_name, - axclass_name = axclass_name, - consts = consts, - tycos = tycos @ tycos_new - } - end; - -in - -fun add_tycos xs thy = - gen_add_tycos Sign.intern_class (rpair (Context.theory_name thy) oo Sign.intern_type) xs thy; -val add_tycos_i = gen_add_tycos (K I) (K I); - -end; (* local *) - -val the_tycos = #tycos oo get_class_data; - (* class queries *) @@ -156,12 +186,16 @@ end; fun get_arities thy sort tycon = - Sorts.mg_domain (Sign.classes_arities_of thy) tycon sort + Sorts.mg_domain (Sign.classes_arities_of thy) tycon (syntactic_sort_of thy sort) |> map (syntactic_sort_of thy); fun get_superclasses thy class = - Sorts.superclasses (Sign.classes_of thy) class - |> syntactic_sort_of thy; + if is_class thy class + then + Sorts.superclasses (Sign.classes_of thy) class + |> syntactic_sort_of thy + else + error ("no syntactic class: " ^ class); (* instance queries *) @@ -227,7 +261,8 @@ ) subclasses; fun mk_class_deriv thy subclasses superclass = case get_superclass_derivation (subclasses, superclass) - of (subclass::deriv) => ((rev o filter (is_class thy)) deriv, find_index_eq subclass subclasses); + of (subclass::deriv) => + ((rev o filter (is_class thy)) deriv, find_index_eq subclass subclasses); fun mk_lookup (sort_def, (Type (tycon, tys))) = let val arity_lookup = map2 (curry mk_lookup) @@ -236,7 +271,7 @@ | mk_lookup (sort_def, TVar ((vname, _), sort_use)) = let fun mk_look class = - let val (deriv, classindex) = mk_class_deriv thy sort_use 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; in @@ -250,21 +285,49 @@ (* intermediate auxiliary *) -fun add_classentry raw_class raw_consts raw_tycos thy = +fun add_classentry raw_class raw_cs raw_tycos thy = let val class = Sign.intern_class thy raw_class; + val cs = map (Sign.intern_const thy) raw_cs; + val tycos = map (rpair (Context.theory_name thy) o Sign.intern_type thy) raw_tycos; in thy |> put_class_data class { locale_name = "", axclass_name = class, - consts = [], - tycos = [] + consts = cs, + tycos = tycos } - |> add_consts (class, raw_consts) - |> add_tycos (class, raw_tycos) + |> fold (add_const class) cs end; - + + +(* toplevel interface *) + +local + +structure P = OuterParse +and K = OuterKeyword + +in + +val classK = "class_class" + +val locale_val = + (P.locale_expr -- + Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 P.context_element)) [] || + Scan.repeat1 P.context_element >> pair Locale.empty); + +val classP = + OuterSyntax.command classK "operational type classes" K.thy_decl + (P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Locale.empty, []) + >> (Toplevel.theory_context + o (fn f => swap o f) o (fn (name, (expr, elems)) => add_class name expr elems))); + +val _ = OuterSyntax.add_parsers [classP]; + +end; (* local *) + (* setup *) diff -r 0cec730b3942 -r 1cad5c2b2a0b src/Pure/Tools/codegen_package.ML --- a/src/Pure/Tools/codegen_package.ML Tue Dec 27 15:24:23 2005 +0100 +++ b/src/Pure/Tools/codegen_package.ML Tue Dec 27 15:24:40 2005 +0100 @@ -63,12 +63,16 @@ val print_codegen_generated: theory -> unit; val rename_inconsistent: theory -> theory; + + (*debugging purpose only*) structure InstNameMangler: NAME_MANGLER; structure ConstNameMangler: NAME_MANGLER; structure DatatypeconsNameMangler: NAME_MANGLER; structure CodegenData: THEORY_DATA; val mk_tabs: theory -> auxtab; val alias_get: theory -> string -> string; + val idf_of_name: theory -> string -> string -> string; + val idf_of_const: theory -> auxtab -> string * typ -> string; end; structure CodegenPackage : CODEGEN_PACKAGE = @@ -590,18 +594,27 @@ fun idf_of_const thy (tabs as ((_, clsmemtab), (_, (overltab1, overltab2), dtcontab))) (c, ty) = let - val coty = case (snd o strip_type) ty - of Type (tyco, _) => tyco - | _ => ""; - val c' = case Symtab.lookup overltab1 c - of SOME (ty_decl, tys) => ConstNameMangler.get thy overltab2 - (idf_of_name thy nsp_overl c, (ty_decl, (the oo find_first) (fn ty' => Sign.typ_instance thy (ty', ty)) tys)) - | NONE => case try (DatatypeconsNameMangler.get thy dtcontab) (c, coty) - of SOME c' => idf_of_name thy nsp_dtcon c' - | NONE => case Symtab.lookup clsmemtab c - of SOME _ => idf_of_name thy nsp_mem c - | NONE => idf_of_name thy nsp_const c; - in c' end; + fun get_overloaded (c, ty) = + case Symtab.lookup overltab1 c + of SOME (ty_decl, tys) => + (case find_first (curry (Sign.typ_instance thy) ty) tys + of SOME ty' => ConstNameMangler.get thy overltab2 + (idf_of_name thy nsp_overl c, (ty_decl, ty')) |> SOME + | _ => NONE) + | _ => NONE + fun get_datatypecons (c, ty) = + case (snd o strip_type) ty + of Type (tyco, _) => + try (DatatypeconsNameMangler.get thy dtcontab) (c, tyco) + | _ => NONE; + in case get_overloaded (c, ty) + of SOME idf => idf + | NONE => case get_datatypecons (c, ty) + of SOME c' => idf_of_name thy nsp_dtcon c' + | NONE => case Symtab.lookup clsmemtab c + of SOME _ => idf_of_name thy nsp_mem c + | NONE => idf_of_name thy nsp_const c + end; fun recconst_of_idf thy (_, (_, (_, overltab2), _)) idf = case name_of_idf thy nsp_const idf @@ -637,13 +650,14 @@ val name_dtco = (the ooo name_of_idf) thy nsp_tyco dtco; val idf_eqinst = idf_of_name thy nsp_eq_inst name_dtco; val idf_eqpred = idf_of_name thy nsp_eq_pred name_dtco; + val inst_sortlookup = map (fn (v, _) => [ClassPackage.Lookup ([], (v, 0))]) arity; fun mk_eq_pred _ trns = trns |> succeed (eqpred, []) fun mk_eq_inst _ trns = trns |> gen_ensure_def [("eqpred", mk_eq_pred)] ("generating equality predicate for " ^ quote dtco) idf_eqpred - |> succeed (Classinst (class_eq, (dtco, arity), [(fun_eq, idf_eqpred)]), []); + |> succeed (Classinst ((class_eq, (dtco, arity)), ([], [(fun_eq, (idf_eqpred, inst_sortlookup))])), []); in trns |> gen_ensure_def [("eqinst", mk_eq_inst)] ("generating equality instance for " ^ quote dtco) idf_eqinst @@ -757,31 +771,33 @@ (* application generators *) +fun mk_lookup thy tabs (ClassPackage.Instance (inst as (cls, tyco), ls)) trns = + trns + |> ensure_def_class thy tabs cls + ||>> ensure_def_inst thy tabs inst + ||>> (fold_map o fold_map) (mk_lookup thy tabs) ls + |-> (fn ((cls, i), ls) => pair (ClassPackage.Instance ((cls, i), ls))) + | mk_lookup thy tabs (ClassPackage.Lookup (clss, (v, i))) trns = + trns + |> fold_map (ensure_def_class thy tabs) clss + |-> (fn clss => pair (ClassPackage.Lookup (clss, (v |> unprefix "'", i)))); + +fun mk_itapp e [] = e + | mk_itapp e lookup = IInst (e, lookup); + fun appgen_default thy tabs ((f, ty), ts) trns = let val _ = debug 5 (fn _ => "making application of " ^ quote f) (); val ty_def = Sign.the_const_constraint thy f; - fun mk_lookup (ClassPackage.Instance (inst as (cls, tyco), ls)) trns = - trns - |> ensure_def_class thy tabs cls - ||>> ensure_def_inst thy tabs inst - ||>> (fold_map o fold_map) mk_lookup ls - |-> (fn ((cls, i), ls) => pair (ClassPackage.Instance ((cls, i), ls))) - | mk_lookup (ClassPackage.Lookup (clss, (v, i))) trns = - trns - |> fold_map (ensure_def_class thy tabs) clss - |-> (fn clss => pair (ClassPackage.Lookup (clss, (v |> unprefix "'", i)))); - fun mk_itapp e [] = e - | mk_itapp e lookup = IInst (e, lookup); in trns |> ensure_def_const thy tabs (f, ty) - ||>> (fold_map o fold_map) mk_lookup (ClassPackage.extract_sortlookup thy (ty_def, ty)) + ||>> (fold_map o fold_map) (mk_lookup thy tabs) (ClassPackage.extract_sortlookup thy (ty_def, ty)) ||>> invoke_cg_type thy tabs ty ||>> fold_map (invoke_cg_expr thy tabs) ts |-> (fn (((f, lookup), ty), es) => succeed (mk_itapp (IConst (f, ty)) lookup `$$ es)) - end + end; fun appgen_neg thy tabs (f as ("neg", Type ("fun", [ty, _])), ts) trns = let @@ -887,26 +903,46 @@ val arity = ClassPackage.get_arities thy [cls] tyco; val ms = map (fn m => (m, Sign.the_const_constraint thy m)) (ClassPackage.the_consts thy cls); val instmem_idfs = ClassPackage.get_inst_consts_sign thy (tyco, cls); + val supclss = ClassPackage.get_superclasses thy cls; fun add_vars arity clsmems (trns as (_, modl)) = case get_def modl (idf_of_name thy nsp_class cls) of Class (_, _, members, _) => ((Term.invent_names (tvars_of_itypes ((map (snd o snd)) members)) "a" (length arity) ~~ arity, clsmems), trns) + val ad_hoc_arity = map (fn (v, sort) => map_index (fn (i, _) => (ClassPackage.Lookup ([], (v, i)))) sort); + (*! THIS IS ACTUALLY VERY AD-HOC... !*) in - trns + (trns |> debug 5 (fn _ => "trying defgen class instance for (" ^ quote cls ^ ", " ^ quote tyco ^ ")") |> (fold_map o fold_map) (ensure_def_class thy tabs) arity ||>> fold_map (ensure_def_const thy tabs) ms |-> (fn (arity, ms) => add_vars arity ms) ||>> ensure_def_class thy tabs cls ||>> ensure_def_tyco thy tabs tyco - ||>> fold_map (ensure_def_const thy tabs) instmem_idfs - |-> (fn ((((arity, ms), cls), tyco), instmem_idfs) => - succeed (Classinst (cls, (tyco, arity), ms ~~ instmem_idfs), [])) + ||>> fold_map (fn supcls => ensure_def_inst thy tabs (supcls, tyco)) supclss + ||>> fold_map (fn supcls => (fold_map o fold_map) (mk_lookup thy tabs) + (ClassPackage.extract_sortlookup thy + (Type (tyco, map_index (fn (i, _) => TVar (("'a", i), [])) (ClassPackage.get_arities thy [supcls] tyco)), + Type (tyco, map_index (fn (i, sort) => TFree (string_of_int i, sort)) arity)))) supclss + ||>> fold_map (ensure_def_const thy tabs) instmem_idfs) + |-> (fn ((((((arity, ms), cls), tyco), supinsts), supinstlookup), instmem_idfs) + : ((((((string * string list) list * string list) * string) * string) + * string list) * ClassPackage.sortlookup list list list) * string list + => + succeed (Classinst ((cls, (tyco, arity)), (supclss ~~ (supinsts ~~ supinstlookup), ms ~~ map (rpair (ad_hoc_arity arity)) instmem_idfs)), [])) end | _ => trns |> fail ("no class instance found for " ^ quote inst); +(* trns + |> ensure_def_const thy tabs (f, ty) + + ||>> invoke_cg_type thy tabs ty + ||>> fold_map (invoke_cg_expr thy tabs) ts + |-> (fn (((f, lookup), ty), es) => + succeed (mk_itapp (IConst (f, ty)) lookup `$$ es))*) + + (* parametrized generators, for instantiation in HOL *) fun appgen_let strip_abs thy tabs (f as ("Let", _), ts) trns = diff -r 0cec730b3942 -r 1cad5c2b2a0b src/Pure/Tools/codegen_serializer.ML --- a/src/Pure/Tools/codegen_serializer.ML Tue Dec 27 15:24:23 2005 +0100 +++ b/src/Pure/Tools/codegen_serializer.ML Tue Dec 27 15:24:40 2005 +0100 @@ -143,15 +143,27 @@ local -fun ml_from_defs tyco_syntax const_syntax is_dicttype resolv ds = +fun ml_from_defs tyco_syntax const_syntax is_dicttyco resolv ds = let + fun is_dicttype (IType (tyco, _)) = + is_dicttyco tyco + | is_dicttype (IDictT _) = + true + | is_dicttype _ = + false; fun chunk_defs ps = let val (p_init, p_last) = split_last ps in Pretty.chunks (p_init @ [Pretty.block ([p_last, Pretty.str ";"])]) end; - val ml_label_uniq = translate_string (fn "_" => "__" | "." => "_" | c => c); + fun ml_from_label s = + let + val s' = NameSpace.unpack s; + in + NameSpace.pack (Library.drop (length s' - 2, s')) + |> translate_string (fn "_" => "__" | "." => "_" | c => c) + end; fun ml_from_type br (IType ("Pair", [t1, t2])) = brackify (eval_br_postfix br (INFX (2, L))) [ ml_from_type (INFX (2, X)) t1, @@ -191,7 +203,7 @@ | ml_from_type _ (IDictT fs) = Pretty.gen_list "," "{" "}" ( map (fn (f, ty) => - Pretty.block [Pretty.str (ml_label_uniq f ^ ": "), ml_from_type NOBR ty]) fs + Pretty.block [Pretty.str (ml_from_label f ^ ": "), ml_from_type NOBR ty]) fs ); fun ml_from_pat br (ICons (("True", []), _)) = Pretty.str "true" @@ -239,8 +251,16 @@ Pretty.str ":", Pretty.str "IntInf.int" ] - | ml_from_pat br (IVarP (v, _)) = - Pretty.str v + | ml_from_pat br (IVarP (v, ty)) = + if is_dicttype ty + then + brackify (eval_br br BR) [ + Pretty.str v, + Pretty.str ":", + ml_from_type NOBR ty + ] + else + Pretty.str v and ml_from_expr br (e as (IApp (IConst ("Cons", _), _))) = let fun dest_cons (IApp (IConst ("Cons", _), @@ -313,19 +333,19 @@ | ml_from_expr br (IDictE fs) = Pretty.gen_list "," "{" "}" ( map (fn (f, e) => - Pretty.block [Pretty.str (ml_label_uniq f ^ " = "), ml_from_expr NOBR e]) fs + Pretty.block [Pretty.str (ml_from_label f ^ " = "), ml_from_expr NOBR e]) fs ) | ml_from_expr br (ILookup ([], v)) = Pretty.str v | ml_from_expr br (ILookup ([l], v)) = brackify (eval_br br BR) [ - Pretty.str ("#" ^ (ml_label_uniq l)), + Pretty.str ("#" ^ (ml_from_label l)), Pretty.str v ] | ml_from_expr br (ILookup (ls, v)) = brackify (eval_br br BR) [ Pretty.str ("(" - ^ (ls |> map ((fn s => "#" ^ s) o ml_label_uniq) |> foldr1 (fn (l, e) => l ^ " o " ^ e)) + ^ (ls |> map ((fn s => "#" ^ s) o ml_from_label) |> foldr1 (fn (l, e) => l ^ " o " ^ e)) ^ ")"), Pretty.str v ] @@ -422,23 +442,10 @@ val definer = the (fold check_args ds NONE); fun mk_eq definer f ty (pats, expr) = let - fun mk_pat_arg p = - case itype_of_ipat p - of ty as IType (tyco, _) => - if is_dicttype tyco - then Pretty.block [ - Pretty.str "(", - ml_from_pat NOBR p, - Pretty.str ":", - ml_from_type NOBR ty, - Pretty.str ")" - ] - else ml_from_pat BR p - | _ => ml_from_pat BR p; val lhs = [Pretty.str (definer ^ " " ^ f)] @ (if null pats then [Pretty.str ":", ml_from_type NOBR ty] - else map mk_pat_arg pats) + else map (ml_from_pat BR) pats) val rhs = [Pretty.str "=", ml_from_expr NOBR expr] in Pretty.block (separate (Pretty.brk 1) (lhs @ rhs)) @@ -551,9 +558,10 @@ Pretty.str "", Pretty.str ("end; (* struct " ^ name ^ " *)") ]); - fun is_dicttype tyco = + fun is_dicttyco module tyco = NameSpace.is_qualified tyco andalso case get_def module tyco of Typesyn (_, IDictT _) => true + | Typesyn _ => false | _ => false; fun eta_expander "Pair" = 2 | eta_expander "Cons" = 2 @@ -590,7 +598,8 @@ |> debug 3 (fn _ => "eliminating classes...") |> eliminate_classes |> debug 3 (fn _ => "serializing...") - |> serialize (ml_from_defs tyco_syntax const_syntax is_dicttype) ml_from_module ml_validator nspgrp name_root + |> `(is_dicttyco) + |-> (fn is_dicttyco => serialize (ml_from_defs tyco_syntax const_syntax is_dicttyco) ml_from_module ml_validator nspgrp name_root) |> (fn p => Pretty.chunks [setmp print_mode [] (Pretty.str o mk_prims) prims, p]) end; @@ -952,7 +961,7 @@ end | haskell_from_def (name, Classmember _) = NONE - | haskell_from_def (_, Classinst ("Eq", (tyco, arity), [(_, eqpred)])) = + | haskell_from_def (_, Classinst (("Eq", (tyco, arity)), (_, [(_, (eqpred, _))]))) = Pretty.block [ Pretty.str "instance ", haskell_from_sctxt arity, @@ -963,7 +972,7 @@ Pretty.fbrk, Pretty.str ("(==) = " ^ (lower_first o resolv) eqpred) ] |> SOME - | haskell_from_def (_, Classinst (clsname, (tyco, arity), instmems)) = + | haskell_from_def (_, Classinst ((clsname, (tyco, arity)), (_, instmems))) = Pretty.block [ Pretty.str "instance ", haskell_from_sctxt arity, @@ -972,14 +981,14 @@ haskell_from_type NOBR (IType (tyco, (map (IVarT o rpair [] o fst)) arity)), Pretty.str " where", Pretty.fbrk, - Pretty.chunks (map (fn (member, const) => + Pretty.chunks (map (fn (member, (const, _)) => Pretty.str ((lower_first o resolv) member ^ " = " ^ (lower_first o resolv) const) ) instmems) ] |> SOME in case List.mapPartial (fn (name, def) => haskell_from_def (name, def)) defs of [] => NONE - | l => (SOME o Pretty.block) l + | l => (SOME o Pretty.chunks o separate (Pretty.str "")) l end; in diff -r 0cec730b3942 -r 1cad5c2b2a0b src/Pure/Tools/codegen_thingol.ML --- a/src/Pure/Tools/codegen_thingol.ML Tue Dec 27 15:24:23 2005 +0100 +++ b/src/Pure/Tools/codegen_thingol.ML Tue Dec 27 15:24:40 2005 +0100 @@ -53,7 +53,9 @@ | Datatypecons of string | Class of class list * vname * (string * (ClassPackage.sortcontext * itype)) list * string list | Classmember of class - | Classinst of class * (string * (vname * string list) list) * (string * string) list; + | Classinst of (class * (string * (vname * sort) list)) + * ((string * (string * ClassPackage.sortlookup list list)) list + * (string * (string * ClassPackage.sortlookup list list)) list); type module; type transact; type 'dst transact_fin; @@ -488,7 +490,9 @@ | Datatypecons of string | Class of class list * vname * (string * (ClassPackage.sortcontext * itype)) list * string list | Classmember of class - | Classinst of class * (string * (vname * string list) list) * (string * string) list; + | Classinst of (class * (string * (vname * sort) list)) + * ((string * (string * ClassPackage.sortlookup list list)) list + * (string * (string * ClassPackage.sortlookup list list)) list); datatype node = Def of def | Module of node Graph.T; type module = node Graph.T; @@ -549,7 +553,7 @@ Pretty.str "class member belonging to ", Pretty.str clsname ] - | pretty_def (Classinst (clsname, (tyco, arity), mems)) = + | pretty_def (Classinst ((clsname, (tyco, arity)), _)) = Pretty.block [ Pretty.str "class instance (", Pretty.str clsname, @@ -557,8 +561,7 @@ Pretty.str tyco, Pretty.str ", ", Pretty.gen_list "," "[" "]" (map (Pretty.gen_list "," "{" "}" o map Pretty.str o snd) arity), - Pretty.str ")) with ", - Pretty.gen_list "," "[" "]" (map (fn (m1, m2) => Pretty.str (m1 ^ " => " ^ m2)) mems) + Pretty.str "))" ]; fun pretty_module modl = @@ -777,10 +780,10 @@ | def => "attempted to add class member to non-class" ^ (Pretty.output o pretty_def) def |> error)]) end - | *) add_check_transform (name, Classinst (clsname, (tyco, arity), memdefs)) = + | *) add_check_transform (name, Classinst ((clsname, (tyco, arity)), (_, memdefs))) = let val _ = debug 7 (fn _ => "transformation for class instance " ^ quote tyco - ^ " of class " ^ quote clsname ^ " with " ^ (commas o map (fn (m1, m2) => m1 ^ " => " ^ m2)) memdefs) (); + ^ " of class " ^ quote clsname) (); (* fun check [Classmember (_, v, mtyp_c), Fun (_, (_, mtyp_i))] = let val mtyp_i' = instant_itype (v, tyco `%% map IVarT arity) mtyp_c; @@ -1197,41 +1200,6 @@ in transform_iexpr vname_alist e `$$ (snd o transform_lookups) ls end | transform_iexpr vname_alist e = map_iexpr transform_itype transform_ipat (transform_iexpr vname_alist) e; - fun mk_cls_typ_map v membrs ty_inst = - map (fn (m, (mctxt, ty)) => - (m, ty |> instant_itype (v, ty_inst))) membrs; - fun extract_members (cls, Class (supclss, v, membrs, _)) = - let - val ty_cls = cls `%% [IVarT (v, [])]; - val w = "d"; - val add_supclss = if null supclss then I else cons (v, supclss); - fun mk_fun (m, (mctxt, ty)) = (m, Fun ([([IVarP (w, ty_cls)], ILookup ([m], w))], - (add_supclss mctxt, ty `-> ty_cls))); - in fold (cons o mk_fun) membrs end - | extract_members _ = I; - fun introduce_dicts (Class (supcls, v, membrs, insts)) = - let - val varname_cls = Term.invent_names (tvars_of_itypes (map (snd o snd) membrs)) "a" 1 |> hd - in - Typesyn ([(varname_cls, supcls)], IDictT (mk_cls_typ_map v membrs (IVarT (varname_cls, [])))) - end - | introduce_dicts (Classinst (clsname, (tyco, arity), memdefs)) = - let - val Class (_, v, members, _) = - if clsname = class_eq - then - Class ([], "a", [(fun_eq, ([], IVarT ("a", []) `-> IVarT ("a", []) `-> Type_bool))], []) - else - get_def module clsname; - val ty = tyco `%% map IVarT arity; - val inst_typ_map = mk_cls_typ_map v members ty; - val memdefs_ty = map (fn (memname, memprim) => - (memname, (memprim, (the o AList.lookup (op =) inst_typ_map) memname))) memdefs; - in - Fun ([([], IDictE (map (apsnd IConst) memdefs_ty))], - ([], IType (clsname, [ty]))) - end - | introduce_dicts d = d; fun elim_sorts (Fun (eqs, ([], ty))) = Fun (map (fn (ps, rhs) => (map transform_ipat ps, transform_iexpr [] rhs)) eqs, ([], transform_itype ty)) @@ -1255,6 +1223,56 @@ | elim_sorts (Typesyn (vars, ty)) = Typesyn (map (fn (v, _) => (v, [])) vars, transform_itype ty) | elim_sorts d = d; + fun mk_cls_typ_map v (supclss, membrs) ty_inst = + (map (fn class => (class, IType (class, [ty_inst]))) supclss, + map (fn (m, (mctxt, ty)) => + (m, ty |> instant_itype (v, ty_inst))) membrs); + fun extract_members (cls, Class (supclss, v, membrs, _)) = + let + val ty_cls = cls `%% [IVarT (v, [])]; + val w = "d"; + val add_supclss = if null supclss then I else cons (v, supclss); + fun mk_fun (m, (mctxt, ty)) = (m, Fun ([([IVarP (w, ty_cls)], ILookup ([m], w))], + (add_supclss mctxt, ty `-> ty_cls))); + in fold (cons o mk_fun) membrs end + | extract_members _ = I; + fun introduce_dicts (Class (supclss, v, membrs, insts)) = + let + val varname_cls = Term.invent_names (tvars_of_itypes (map (snd o snd) membrs)) "a" 1 |> hd + in + Typesyn ([(varname_cls, supclss)], IDictT ((op @) (mk_cls_typ_map v (supclss, membrs) (IVarT (varname_cls, []))))) + end + | introduce_dicts (Classinst ((clsname, (tyco, arity)), (supinsts, memdefs))) = + let + val Class (supclss, v, members, _) = + if clsname = class_eq + then + Class ([], "a", [(fun_eq, ([], IVarT ("a", []) `-> IVarT ("a", []) `-> Type_bool))], []) + else + get_def module clsname; + val ty = tyco `%% map IVarT arity; + val (supinst_typ_map, mem_typ_map) = mk_cls_typ_map v (supclss, members) ty; + fun mk_meminst (m, ty) = + let + val (instname, instlookup) = (the o AList.lookup (op =) memdefs) m; + in + IInst (IConst (instname, ty), instlookup) + |> pair m + end; + val memdefs_ty = map mk_meminst mem_typ_map; + fun mk_supinst (supcls, dictty) = + let + val (instname, instlookup) = (the o AList.lookup (op =) supinsts) supcls; + in + IInst (IConst (instname, dictty), instlookup) + |> pair supcls + end; + val instdefs_ty = map mk_supinst supinst_typ_map; + in + Fun ([([], IDictE (instdefs_ty @ memdefs_ty))], + (arity, IType (clsname, [ty]))) + end + | introduce_dicts d = d; in module |> `(fn module => fold_defs extract_members module [])