# HG changeset patch # User haftmann # Date 1135174756 -3600 # Node ID 6720b5010a57077fc56404123448fdd4dd5f36df # Parent 2b2fbc32550e0b9a468196ff1f4d8028b91d63d8 slight improvements in name handling diff -r 2b2fbc32550e -r 6720b5010a57 src/Pure/Tools/codegen_package.ML --- a/src/Pure/Tools/codegen_package.ML Wed Dec 21 15:18:57 2005 +0100 +++ b/src/Pure/Tools/codegen_package.ML Wed Dec 21 15:19:16 2005 +0100 @@ -11,7 +11,7 @@ signature CODEGEN_PACKAGE = sig - type deftab; + type auxtab; type exprgen_term; type appgen; type defgen; @@ -28,29 +28,22 @@ val add_syntax_const: string -> ((xstring * string option) * string) * (string option * (string * string list)) option -> theory -> theory; - val add_syntax_const_i: string -> (string * CodegenThingol.iexpr Codegen.mixfix list) + val add_syntax_const_i: string -> ((string * typ) * CodegenThingol.iexpr Codegen.mixfix list) * (string * (string * string list)) option -> theory -> theory; val add_alias: string * string -> theory -> theory; val set_is_datatype: (theory -> string -> bool) -> theory -> theory; + val set_get_all_datatype_cons : (theory -> (string * string list) list) + -> theory -> theory; - val idf_of_name: theory -> string -> string -> string; - val name_of_idf: theory -> string -> string -> string option; - val idf_of_inst: theory -> deftab -> class * string -> string; - val inst_of_idf: theory -> deftab -> string -> (class * string) option; - val idf_of_tname: theory -> string -> string; - val tname_of_idf: theory -> string -> string option; - val idf_of_cname: theory -> deftab -> string * typ -> string; - val cname_of_idf: theory -> deftab -> string -> (string * typ) option; - - val invoke_cg_type: theory -> deftab + val invoke_cg_type: theory -> auxtab -> typ -> CodegenThingol.transact -> CodegenThingol.itype * CodegenThingol.transact; - val invoke_cg_expr: theory -> deftab + val invoke_cg_expr: theory -> auxtab -> term -> CodegenThingol.transact -> CodegenThingol.iexpr * CodegenThingol.transact; - val ensure_def_tyco: theory -> deftab + val ensure_def_tyco: theory -> auxtab -> string -> CodegenThingol.transact -> string * CodegenThingol.transact; - val ensure_def_const: theory -> deftab - -> string -> CodegenThingol.transact -> string * CodegenThingol.transact; + val ensure_def_const: theory -> auxtab + -> string * typ -> CodegenThingol.transact -> string * CodegenThingol.transact; val appgen_let: (int -> term -> term list * term) -> appgen; @@ -69,9 +62,13 @@ -> defgen; val print_codegen_generated: theory -> unit; - val mk_deftab: theory -> deftab; + val rename_inconsistent: theory -> theory; + structure InstNameMangler: NAME_MANGLER; + structure ConstNameMangler: NAME_MANGLER; + structure DatatypeconsNameMangler: NAME_MANGLER; structure CodegenData: THEORY_DATA; - structure Insttab: TABLE; + val mk_tabs: theory -> auxtab; + val alias_get: theory -> string -> string; end; structure CodegenPackage : CODEGEN_PACKAGE = @@ -88,8 +85,10 @@ (* auxiliary *) +fun devarify_type ty = (fst o Type.freeze_thaw_type) ty; fun devarify_term t = (fst o Type.freeze_thaw) t; -fun devarify_type ty = (fst o Type.freeze_thaw_type) ty; + +val is_number = is_some o Int.fromString; fun newline_correct s = s @@ -99,46 +98,103 @@ | xs => xs) o explode) |> space_implode "\n"; -(* code generator instantiation, part 1 *) -structure Insttab = TableFun( - type key = string * string - val ord = prod_ord fast_string_ord fast_string_ord -); - -type deftab = ((typ * string) list Symtab.table - * (string * typ) Symtab.table) - * (term list * term * typ) Symtab.table - * (string Insttab.table - * (string * string) Symtab.table - * class Symtab.table); - -type exprgen_sort = theory -> deftab -> (sort, sort) gen_exprgen; -type exprgen_type = theory -> deftab -> (typ, itype) gen_exprgen; -type exprgen_term = theory -> deftab -> (term, iexpr) gen_exprgen; -type appgen = theory -> deftab -> ((string * typ) * term list, iexpr) gen_exprgen; -type defgen = theory -> deftab -> gen_defgen; - - -(* namespace conventions *) +(* shallo name spaces *) val nsp_class = "class"; -val nsp_type = "type"; +val nsp_tyco = "tyco"; val nsp_const = "const"; -val nsp_dtcon = "dtcon"; (*NOT OPERATIONAL YET*) +val nsp_overl = "overl"; +val nsp_dtcon = "dtcon"; val nsp_mem = "mem"; val nsp_inst = "inst"; val nsp_eq_inst = "eq_inst"; val nsp_eq_pred = "eq"; +(* code generator data types *) + +structure InstNameMangler = NameManglerFun ( + type ctxt = theory; + type src = string * (class * string); + val ord = prod_ord string_ord (prod_ord string_ord string_ord); + fun mk thy ((thyname, (cls, tyco)), i) = + NameSpace.base cls ^ "_" ^ NameSpace.base tyco ^ implode (replicate i "'") + |> NameSpace.append thyname; + fun is_valid _ _ = true; + fun maybe_unique _ _ = NONE; + fun re_mangle _ dst = error ("no such instance: " ^ quote dst); +); + +structure ConstNameMangler = NameManglerFun ( + type ctxt = theory; + type src = string * (typ * typ); + val ord = prod_ord string_ord (prod_ord Term.typ_ord Term.typ_ord); + fun mk thy ((c, (ty_decl, ty)), i) = + let + fun mangle (Type (tyco, tys)) = + NameSpace.base tyco :: Library.flat (List.mapPartial mangle tys) |> SOME + | mangle _ = + NONE + in + Vartab.empty + |> Sign.typ_match thy (ty_decl, ty) + |> map (snd o snd) o Vartab.dest + |> List.mapPartial mangle + |> Library.flat + |> null ? K ["x"] + |> cons c + |> space_implode "_" + |> curry (op ^ o swap) ((implode oo replicate) i "'") + end; + fun is_valid _ _ = true; + fun maybe_unique _ _ = NONE; + fun re_mangle _ dst = error ("no such constant: " ^ quote dst); +); + +structure DatatypeconsNameMangler = NameManglerFun ( + type ctxt = theory; + type src = string * string; + val ord = prod_ord string_ord string_ord; + fun mk thy (("0", "nat"), _) = + "Nat.Zero" + | mk thy ((co, dtco), i) = + let + fun basename 0 = NameSpace.base co + | basename i = NameSpace.base dtco ^ "_" ^ NameSpace.base co ^ "_" ^ (implode oo replicate) (i-1) "'"; + fun strip_dtco name = + case (rev o NameSpace.unpack) name + of x1::x2::xs => + if x2 = NameSpace.base dtco + then NameSpace.pack (x1::xs) + else name + | _ => name; + in + NameSpace.append (NameSpace.drop_base dtco) (basename i) + |> strip_dtco + end; + fun is_valid _ _ = true; + fun maybe_unique _ _ = NONE; + fun re_mangle _ dst = error ("no such datatype constructor: " ^ quote dst); +); + +type auxtab = ((typ * (term list * term)) Symtab.table * string Symtab.table) + * (InstNameMangler.T * ((typ * typ list) Symtab.table * ConstNameMangler.T) * DatatypeconsNameMangler.T); + +type exprgen_sort = theory -> auxtab -> (sort, sort) gen_exprgen; +type exprgen_type = theory -> auxtab -> (typ, itype) gen_exprgen; +type exprgen_term = theory -> auxtab -> (term, iexpr) gen_exprgen; +type appgen = theory -> auxtab -> ((string * typ) * term list, iexpr) gen_exprgen; +type defgen = theory -> auxtab -> gen_defgen; + + (* serializer *) val serializer_ml = let val name_root = "Generated"; val nsp_conn = [ - [nsp_class, nsp_type], [nsp_const, nsp_dtcon, nsp_inst, nsp_mem, nsp_eq_inst, nsp_eq_pred] + [nsp_class, nsp_tyco], [nsp_const, nsp_overl, nsp_dtcon, nsp_mem, nsp_inst, nsp_eq_inst, nsp_eq_pred] ]; in CodegenSerializer.ml_from_thingol nsp_conn name_root end; @@ -146,12 +202,12 @@ let val name_root = "Generated"; val nsp_conn = [ - [nsp_class], [nsp_type], [nsp_const, nsp_mem, nsp_eq_pred], [nsp_dtcon], [nsp_inst, nsp_eq_inst] + [nsp_class], [nsp_tyco], [nsp_const, nsp_overl, nsp_mem, nsp_eq_pred], [nsp_dtcon], [nsp_inst, nsp_eq_inst] ]; in CodegenSerializer.haskell_from_thingol nsp_conn name_root end; -(* theory data for codegen *) +(* theory data for code generator *) type gens = { exprgens_sort: (string * (exprgen_sort * stamp)) list, @@ -161,17 +217,12 @@ defgens: (string * (defgen * stamp)) list }; -val empty_gens = { - exprgens_sort = Symtab.empty, exprgens_type = Symtab.empty, - exprgens_term = Symtab.empty, defgens = Symtab.empty, appgens = Symtab.empty -}; - fun map_gens f { exprgens_sort, exprgens_type, exprgens_term, appgens, defgens } = let val (exprgens_sort, exprgens_type, exprgens_term, appgens, defgens) = f (exprgens_sort, exprgens_type, exprgens_term, appgens, defgens) in { exprgens_sort = exprgens_sort, exprgens_type = exprgens_type, - exprgens_term = exprgens_term, appgens = appgens, defgens = defgens } end; + exprgens_term = exprgens_term, appgens = appgens, defgens = defgens } : gens end; fun merge_gens ({ exprgens_sort = exprgens_sort1, exprgens_type = exprgens_type1, @@ -189,15 +240,11 @@ lookups_const: (typ * iexpr) list Symtab.table } -val empty_lookups = { - lookups_tyco = Symtab.empty, lookups_const = Symtab.empty -}; - fun map_lookups f { lookups_tyco, lookups_const } = let val (lookups_tyco, lookups_const) = f (lookups_tyco, lookups_const) - in { lookups_tyco = lookups_tyco, lookups_const = lookups_const } end; + in { lookups_tyco = lookups_tyco, lookups_const = lookups_const } : lookups end; fun merge_lookups ({ lookups_tyco = lookups_tyco1, lookups_const = lookups_const1 }, @@ -207,18 +254,19 @@ type logic_data = { is_datatype: ((theory -> string -> bool) * stamp) option, + get_all_datatype_cons: ((theory -> (string * string list) list) * stamp) option, alias: string Symtab.table * string Symtab.table }; -fun map_logic_data f { is_datatype, alias } = +fun map_logic_data f { is_datatype, get_all_datatype_cons, alias } = let - val (is_datatype, alias) = - f (is_datatype, alias) - in { is_datatype = is_datatype, alias = alias } end; + val ((is_datatype, get_all_datatype_cons), alias) = + f ((is_datatype, get_all_datatype_cons), alias) + in { is_datatype = is_datatype, get_all_datatype_cons = get_all_datatype_cons, alias = alias } : logic_data end; fun merge_logic_data - ({ is_datatype = is_datatype1, alias = alias1 }, - { is_datatype = is_datatype2, alias = alias2 }) = + ({ is_datatype = is_datatype1, get_all_datatype_cons = get_all_datatype_cons1, alias = alias1 }, + { is_datatype = is_datatype2, get_all_datatype_cons = get_all_datatype_cons2, alias = alias2 }) = let fun merge_opt _ (x1, NONE) = x1 | merge_opt _ (NONE, x2) = x2 @@ -226,6 +274,7 @@ if eq (x1, x2) then SOME x1 else error ("incompatible options during merge"); in { is_datatype = merge_opt (eq_snd (op =)) (is_datatype1, is_datatype2), + get_all_datatype_cons = merge_opt (eq_snd (op =)) (get_all_datatype_cons1, get_all_datatype_cons2), alias = (Symtab.merge (op =) (fst alias1, fst alias2), Symtab.merge (op =) (snd alias1, snd alias2)) } : logic_data end; @@ -242,7 +291,8 @@ val (primitives, syntax_tyco, syntax_const) = f (primitives, syntax_tyco, syntax_const) in { serializer = serializer, primitives = primitives, - syntax_tyco = syntax_tyco, syntax_const = syntax_const } end; + syntax_tyco = syntax_tyco, syntax_const = syntax_const } : serialize_data + end; fun merge_serialize_data ({ serializer = serializer, primitives = primitives1, @@ -268,7 +318,8 @@ modl = empty_module, gens = { exprgens_sort = [], exprgens_type = [], exprgens_term = [], appgens = [], defgens = [] } : gens, lookups = { lookups_tyco = Symtab.empty, lookups_const = Symtab.empty } : lookups, - logic_data = { is_datatype = NONE, alias = (Symtab.empty, Symtab.empty) } : logic_data, + logic_data = { is_datatype = NONE, get_all_datatype_cons = NONE, + alias = (Symtab.empty, Symtab.empty) } : logic_data, serialize_data = Symtab.empty |> Symtab.update ("ml", @@ -370,7 +421,8 @@ |> Output.update_warn (op =) ("overwriting existing definition definition generator " ^ name) (name, (dg, stamp ())))), lookups, serialize_data, logic_data)); -val get_lookups_tyco = #lookups_tyco o #lookups o CodegenData.get; +fun get_defgens thy tabs = + (map (apsnd (fn (dg, _) => dg thy tabs)) o #defgens o #gens o CodegenData.get) thy; fun add_lookup_tyco (src, dst) = map_codegen_data @@ -382,6 +434,8 @@ lookups_const)), serialize_data, logic_data)); +val lookup_tyco = Symtab.lookup o #lookups_tyco o #lookups o CodegenData.get; + fun add_lookup_const ((src, ty), dst) = map_codegen_data (fn (modl, gens, lookups, serialize_data, logic_data) => @@ -392,12 +446,33 @@ lookups_const |> Symtab.update_multi (src, (ty, dst)))), serialize_data, logic_data)); +fun lookup_const thy (f, ty) = + (Symtab.lookup_multi o #lookups_const o #lookups o CodegenData.get) thy f + |> (fn tab => AList.lookup (Sign.typ_instance thy) tab ty); + fun set_is_datatype f = map_codegen_data (fn (modl, gens, lookups, serialize_data, logic_data) => (modl, gens, lookups, serialize_data, logic_data - |> map_logic_data (apfst (K (SOME (f, stamp ())))))); + |> map_logic_data ((apfst o apfst) (K (SOME (f, stamp ())))))); + +fun is_datatype thy = + case (#is_datatype o #logic_data o CodegenData.get) thy + of NONE => K false + | SOME (f, _) => f thy; + +fun set_get_all_datatype_cons f = + map_codegen_data + (fn (modl, gens, lookups, serialize_data, logic_data) => + (modl, gens, lookups, serialize_data, + logic_data + |> map_logic_data ((apfst o apsnd) (K (SOME (f, stamp ())))))); + +fun get_all_datatype_cons thy = + case (#get_all_datatype_cons o #logic_data o CodegenData.get) thy + of NONE => [] + | SOME (f, _) => f thy; fun add_alias (src, dst) = map_codegen_data @@ -409,171 +484,194 @@ tab_rev |> Symtab.update (dst, src)))))); -(* code generator name mangling *) - -val is_number = is_some o Int.fromString; +(* name handling *) -val dtype_mangle = "dtype"; -fun is_datatype thy = - case (#is_datatype o #logic_data o CodegenData.get) thy - of NONE => K false - | SOME (f, _) => f thy; +val nsp_class = "class"; +val nsp_tyco = "tyco"; +val nsp_const = "const"; +val nsp_overl = "overl"; +val nsp_dtcon = "dtcon"; +val nsp_mem = "mem"; +val nsp_inst = "inst"; +val nsp_eq_inst = "eq_inst"; +val nsp_eq_pred = "eq"; -fun idf_of_name thy shallow name = - if is_number name - then name - else - name - |> NameSpace.unpack - |> split_last - |> apsnd ((perhaps o Symtab.lookup) ((fst o #alias o #logic_data o CodegenData.get) thy) #> single #> cons shallow) - |> (op @) - |> NameSpace.pack; +val alias_get = perhaps o Symtab.lookup o fst o #alias o #logic_data o CodegenData.get; +val alias_rev = perhaps o Symtab.lookup o snd o #alias o #logic_data o CodegenData.get; -fun name_of_idf thy nsp idf = +fun add_nsp shallow name = + name + |> NameSpace.unpack + |> split_last + |> apsnd (single #> cons shallow) + |> (op @) + |> NameSpace.pack; +fun dest_nsp nsp idf = let val idf' = NameSpace.unpack idf; val (idf'', idf_base) = split_last idf'; val (modl, shallow) = split_last idf''; in if nsp = shallow - then SOME (NameSpace.pack (modl @ [ - (perhaps o Symtab.lookup) ((snd o #alias o #logic_data o CodegenData.get) thy) idf_base])) + then (SOME o NameSpace.pack) (modl @ [idf_base]) else NONE end; -fun idf_of_inst thy (_, _, (clstab, _, _)) (cls, tyco) = - (the o Insttab.lookup clstab) (cls, tyco); - -fun inst_of_idf thy (_, _, (_, clstab_rev, _)) idf = - Symtab.lookup clstab_rev idf; - -fun idf_of_tname thy tyco = - if not (Symtab.defined (get_lookups_tyco thy) tyco) - andalso tyco <> "nat" andalso is_datatype thy tyco - then - tyco - |> (fn tyco => NameSpace.append tyco nsp_type) - |> (fn tyco => NameSpace.append tyco dtype_mangle) +fun idf_of_name thy shallow name = + if is_number name + then name else - tyco - |> idf_of_name thy nsp_type; + name + |> alias_get thy + |> add_nsp shallow; +fun name_of_idf thy shallow idf = + idf + |> dest_nsp shallow + |> Option.map (alias_rev thy); -fun tname_of_idf thy idf = - if NameSpace.base idf = dtype_mangle - andalso (NameSpace.base o NameSpace.drop_base) idf = nsp_type - then - if is_datatype thy ((NameSpace.drop_base o NameSpace.drop_base) idf) - then (NameSpace.drop_base o NameSpace.drop_base) idf |> SOME - else name_of_idf thy nsp_type idf - else name_of_idf thy nsp_type idf; - -fun idf_of_cname thy ((overl, _), _, _) (name, ty) = - case Symtab.lookup overl name - of NONE => idf_of_name thy nsp_const name - | SOME tab => (the o AList.lookup (Sign.typ_instance thy) tab) ty +(* code generator instantiation *) -fun cname_of_idf thy ((_, overl_rev), _, _) idf = - case Symtab.lookup overl_rev idf - of NONE => - (case name_of_idf thy nsp_const idf - of NONE => (case name_of_idf thy nsp_mem idf - of NONE => NONE - | SOME n => SOME (n, Sign.the_const_constraint thy n)) - | SOME n => SOME (n, Sign.the_const_constraint thy n)) - | s => s; - - -(* code generator instantiation, part 2 *) - -fun invoke_cg_sort thy defs sort trns = +fun invoke_cg_sort thy tabs sort trns = gen_invoke - ((map (apsnd (fn (cg, _) => cg thy defs)) o #exprgens_sort o #gens o CodegenData.get) thy) + ((map (apsnd (fn (cg, _) => cg thy tabs)) o #exprgens_sort o #gens o CodegenData.get) thy) ("generating sort " ^ (quote o Sign.string_of_sort thy) sort) sort trns; -fun invoke_cg_type thy defs ty trns = +fun invoke_cg_type thy tabs ty trns = gen_invoke - ((map (apsnd (fn (cg, _) => cg thy defs)) o #exprgens_type o #gens o CodegenData.get) thy) + ((map (apsnd (fn (cg, _) => cg thy tabs)) o #exprgens_type o #gens o CodegenData.get) thy) ("generating type " ^ (quote o Sign.string_of_typ thy) ty) ty trns; -fun invoke_cg_expr thy defs t trns = +fun invoke_cg_expr thy tabs t trns = gen_invoke - ((map (apsnd (fn (cg, _) => cg thy defs)) o #exprgens_term o #gens o CodegenData.get) thy) + ((map (apsnd (fn (cg, _) => cg thy tabs)) o #exprgens_term o #gens o CodegenData.get) thy) ("generating expression " ^ (quote o Sign.string_of_term thy) t) t trns; -fun invoke_appgen thy defs (app as ((f, ty), ts)) trns = +fun invoke_appgen thy tabs (app as ((f, ty), ts)) trns = gen_invoke - ((map (apsnd (fn (ag, _) => ag thy defs)) o #appgens o #gens o CodegenData.get) thy) + ((map (apsnd (fn (ag, _) => ag thy tabs)) o #appgens o #gens o CodegenData.get) thy) ("generating application " ^ f ^ "::" ^ (Sign.string_of_typ thy) ty ^ " " ^ enclose "(" ")" (commas (map (Sign.string_of_term thy) ts))) app trns; -fun find_lookup_expr thy (f, ty) = - Symtab.lookup_multi ((#lookups_const o #lookups o CodegenData.get) thy) f - |> (fn tab => AList.lookup (Sign.typ_instance thy) tab ty); - -fun get_defgens thy defs = - (map (apsnd (fn (dg, _) => dg thy defs)) o #defgens o #gens o CodegenData.get) thy; +fun ensure_def_class thy tabs cls trns = + let + val cls' = idf_of_name thy nsp_class cls; + in + trns + |> debug 4 (fn _ => "generating class " ^ quote cls) + |> gen_ensure_def (get_defgens thy tabs) ("generating class " ^ quote cls) cls' + |> pair cls' + end; -fun ensure_def_class thy defs cls trns = - trns - |> debug 4 (fn _ => "generating class " ^ quote cls) - |> gen_ensure_def (get_defgens thy defs) ("generating class " ^ quote cls) cls - |> pair cls; +fun ensure_def_inst thy (tabs as (_, (insttab, _, _))) (cls, tyco) trns = + let + val thyname = (the o AList.lookup (op =) (ClassPackage.the_tycos thy cls)) tyco; + val inst = idf_of_name thy nsp_inst (InstNameMangler.get thy insttab (thyname, (cls, tyco))); + in + trns + |> debug 4 (fn _ => "generating instance " ^ quote cls ^ " / " ^ quote tyco) + |> gen_ensure_def (get_defgens thy tabs) ("generating instance " ^ quote cls ^ " / " ^ quote tyco) inst + |> pair inst + end; -fun ensure_def_instance thy defs inst trns = - trns - |> debug 4 (fn _ => "generating instance " ^ quote inst) - |> gen_ensure_def (get_defgens thy defs) ("generating instance " ^ quote inst) inst - |> pair inst; - -fun ensure_def_tyco thy defs tyco trns = - if NameSpace.is_qualified tyco - then case Option.mapPartial (Symtab.lookup (get_lookups_tyco thy)) (tname_of_idf thy tyco) +fun ensure_def_tyco thy tabs tyco trns = + let + val tyco' = idf_of_name thy nsp_tyco tyco; + in case lookup_tyco thy tyco of NONE => trns |> debug 4 (fn _ => "generating type constructor " ^ quote tyco) - |> gen_ensure_def (get_defgens thy defs) ("generating type constructor " ^ quote tyco) tyco - |> pair tyco + |> gen_ensure_def (get_defgens thy tabs) ("generating type constructor " ^ quote tyco) tyco' + |> pair tyco' | SOME tyco => trns |> pair tyco - else (tyco, trns); + end; + +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_decl)) 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 ensure_def_const thy defs f trns = - if NameSpace.is_qualified f - then case Option.mapPartial (find_lookup_expr thy) (cname_of_idf thy defs f) +fun recconst_of_idf thy (_, (_, (_, overltab2), _)) idf = + case name_of_idf thy nsp_const idf + of SOME c => SOME (c, Sign.the_const_constraint thy c) + | NONE => ( + case dest_nsp nsp_overl idf + of SOME _ => + idf + |> ConstNameMangler.rev thy overltab2 + |> apfst (the o name_of_idf thy nsp_overl) + |> apsnd snd + |> SOME + | NONE => NONE + ); + +fun ensure_def_const thy (tabs as ((_, clsmemtab), (_, overltab, dtcontab))) (c, ty) trns = + let + val c' = idf_of_const thy tabs (c, ty); + in case lookup_const thy (c, ty) of NONE => trns - |> debug 4 (fn _ => "generating constant " ^ quote f) - |> invoke_cg_type thy defs (cname_of_idf thy defs f |> the |> snd |> devarify_type) - ||> gen_ensure_def (get_defgens thy defs) ("generating constant " ^ quote f) f - |-> (fn _ => pair f) - | SOME (IConst (f, ty)) => + |> debug 4 (fn _ => "generating constant " ^ quote c) + |> invoke_cg_type thy tabs (ty |> devarify_type) + ||> gen_ensure_def (get_defgens thy tabs) ("generating constant " ^ quote c) c' + |-> (fn _ => pair c') + | SOME (IConst (c, ty)) => trns - |> pair f - else (f, trns); + |> pair c + end; -fun mk_fun thy defs eqs ty trns = +fun ensure_def_eq thy tabs (dtco, (eqpred, arity)) trns = + let + 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; + 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)]), []); + in + trns + |> gen_ensure_def [("eqinst", mk_eq_inst)] ("generating equality instance for " ^ quote dtco) idf_eqinst + end; + + +(* code generator auxiliary *) + +fun mk_fun thy tabs eqs ty trns = let val sortctxt = ClassPackage.extract_sortctxt thy ty; fun mk_sortvar (v, sort) trns = trns - |> invoke_cg_sort thy defs sort + |> invoke_cg_sort thy tabs sort |-> (fn sort => pair (unprefix "'" v, sort)) fun mk_eq (args, rhs) trns = trns - |> fold_map (invoke_cg_expr thy defs o devarify_term) args - ||>> (invoke_cg_expr thy defs o devarify_term) rhs + |> fold_map (invoke_cg_expr thy tabs o devarify_term) args + ||>> (invoke_cg_expr thy tabs o devarify_term) rhs |-> (fn (args, rhs) => pair (map ipat_of_iexpr args, rhs)) in trns |> fold_map mk_eq eqs - ||>> invoke_cg_type thy defs (devarify_type ty) + ||>> invoke_cg_type thy tabs (devarify_type ty) ||>> fold_map mk_sortvar sortctxt |-> (fn ((eqs, ty), sortctxt) => pair (Fun (eqs, (sortctxt, ty)))) end; -fun fix_nargs thy defs gen (imin, imax) (t, ts) trns = +fun fix_nargs thy tabs gen (imin, imax) (t, ts) trns = if length ts < imin then let val d = imin - length ts; @@ -582,7 +680,7 @@ in trns |> debug 10 (fn _ => "eta-expanding") - |> fold_map (invoke_cg_type thy defs) tys + |> fold_map (invoke_cg_type thy tabs) tys ||>> gen (t, ts @ map2 (curry Free) vs tys) |-> (fn (tys, e) => succeed ((vs ~~ tys) `|--> e)) end @@ -590,7 +688,7 @@ trns |> debug 10 (fn _ => "splitting arguments (" ^ string_of_int imax ^ ", " ^ string_of_int (length ts) ^ ")") |> gen (t, Library.take (imax, ts)) - ||>> fold_map (invoke_cg_expr thy defs) (Library.drop (imax, ts)) + ||>> fold_map (invoke_cg_expr thy tabs) (Library.drop (imax, ts)) |-> succeed o mk_apps else trns @@ -599,149 +697,126 @@ |-> succeed; -(* code generators *) +(* expression generators *) -fun exprgen_sort_default thy defs sort trns = +fun exprgen_sort_default thy tabs sort trns = trns - |> fold_map (ensure_def_class thy defs) - (sort |> ClassPackage.syntactic_sort_of thy |> map (idf_of_name thy nsp_class)) + |> fold_map (ensure_def_class thy tabs) (ClassPackage.syntactic_sort_of thy sort) |-> (fn sort => succeed sort) -fun exprgen_type_default thy defs (TVar _) trns = +fun exprgen_type_default thy tabs (TVar _) trns = error "TVar encountered during code generation" - | exprgen_type_default thy defs (TFree (v, sort)) trns = + | exprgen_type_default thy tabs (TFree (v, sort)) trns = trns - |> invoke_cg_sort thy defs sort + |> invoke_cg_sort thy tabs sort |-> (fn sort => succeed (IVarT (v |> unprefix "'", sort))) - | exprgen_type_default thy defs (Type ("fun", [t1, t2])) trns = + | exprgen_type_default thy tabs (Type ("fun", [t1, t2])) trns = trns - |> invoke_cg_type thy defs t1 - ||>> invoke_cg_type thy defs t2 + |> invoke_cg_type thy tabs t1 + ||>> invoke_cg_type thy tabs t2 |-> (fn (t1', t2') => succeed (t1' `-> t2')) - | exprgen_type_default thy defs (Type (tyco, tys)) trns = + | exprgen_type_default thy tabs (Type (tyco, tys)) trns = trns - |> ensure_def_tyco thy defs (idf_of_tname thy tyco) - ||>> fold_map (invoke_cg_type thy defs) tys + |> ensure_def_tyco thy tabs tyco + ||>> fold_map (invoke_cg_type thy tabs) tys |-> (fn (tyco, tys) => succeed (tyco `%% tys)) -fun exprgen_term_default thy defs (Const (f, ty)) trns = +fun exprgen_term_default thy tabs (Const (f, ty)) trns = trns - |> invoke_appgen thy defs ((f, ty), []) + |> invoke_appgen thy tabs ((f, ty), []) |-> (fn e => succeed e) - | exprgen_term_default thy defs (Var ((v, i), ty)) trns = + | exprgen_term_default thy tabs (Var ((v, i), ty)) trns = trns - |> invoke_cg_type thy defs ty + |> invoke_cg_type thy tabs ty |-> (fn ty => succeed (IVarE (if i = 0 then v else v ^ "_" ^ string_of_int i, ty))) - | exprgen_term_default thy defs (Free (v, ty)) trns = + | exprgen_term_default thy tabs (Free (v, ty)) trns = trns - |> invoke_cg_type thy defs ty + |> invoke_cg_type thy tabs ty |-> (fn ty => succeed (IVarE (v, ty))) - | exprgen_term_default thy defs (Abs (v, ty, t)) trns = + | exprgen_term_default thy tabs (Abs (v, ty, t)) trns = trns - |> invoke_cg_type thy defs ty - ||>> invoke_cg_expr thy defs (subst_bound (Free (v, ty), t)) + |> invoke_cg_type thy tabs ty + ||>> invoke_cg_expr thy tabs (subst_bound (Free (v, ty), t)) |-> (fn (ty, e) => succeed ((v, ty) `|-> e)) - | exprgen_term_default thy defs (t as t1 $ t2) trns = + | exprgen_term_default thy tabs (t as t1 $ t2) trns = let val (t', ts) = strip_comb t in case t' of Const (f, ty) => trns - |> invoke_appgen thy defs ((f, ty), ts) + |> invoke_appgen thy tabs ((f, ty), ts) |-> (fn e => succeed e) | _ => trns - |> invoke_cg_expr thy defs t' - ||>> fold_map (invoke_cg_expr thy defs) ts + |> invoke_cg_expr thy tabs t' + ||>> fold_map (invoke_cg_expr thy tabs) ts |-> (fn (e, es) => succeed (e `$$ es)) end; -fun appgen_default thy defs ((f, ty), ts) trns = + +(* application generators *) + +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; - val _ = debug 10 (fn _ => "making application (2)") (); - fun mk_lookup (ClassPackage.Instance (i, ls)) trns = + fun mk_lookup (ClassPackage.Instance (inst as (cls, tyco), ls)) trns = trns - |> ensure_def_class thy defs ((idf_of_name thy nsp_class o fst) i) - ||>> ensure_def_instance thy defs (idf_of_inst thy defs i) + |> 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 defs) (map (idf_of_name thy nsp_class) clss) + |> fold_map (ensure_def_class thy tabs) clss |-> (fn clss => pair (ClassPackage.Lookup (clss, (v |> unprefix "'", i)))); - val _ = debug 10 (fn _ => "making application (3)") (); fun mk_itapp e [] = e | mk_itapp e lookup = IInst (e, lookup); in trns - |> debug 10 (fn _ => "making application (4): " ^ f ^ "::" ^ Sign.string_of_typ thy ty ^ " <~> " ^ Sign.string_of_typ thy ty_def) - |> ensure_def_const thy defs (idf_of_cname thy defs (f, ty)) - ||> debug 10 (fn _ => "making application (5)") + |> ensure_def_const thy tabs (f, ty) ||>> (fold_map o fold_map) mk_lookup (ClassPackage.extract_sortlookup thy (ty_def, ty)) - ||> debug 10 (fn _ => "making application (6)") - ||>> invoke_cg_type thy defs ty - ||> debug 10 (fn _ => "making application (7)") - ||>> fold_map (invoke_cg_expr thy defs) ts - ||> debug 10 (fn _ => "making application (8)") + ||>> 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 -fun appgen_neg thy defs (f as ("neg", Type ("fun", [ty, _])), ts) trns = +fun appgen_neg thy tabs (f as ("neg", Type ("fun", [ty, _])), ts) trns = let fun gen_neg _ trns = trns - |> invoke_cg_expr thy defs (Const ("op >", ty --> ty --> Type ("bool", [])) $ Const ("0", ty)) + |> invoke_cg_expr thy tabs (Const ("op >", ty --> ty --> Type ("bool", [])) $ Const ("0", ty)) in trns - |> fix_nargs thy defs gen_neg (0, 0) (Const f, ts) + |> fix_nargs thy tabs gen_neg (0, 0) (Const f, ts) end - | appgen_neg thy defs ((f, _), _) trns = + | appgen_neg thy tabs ((f, _), _) trns = trns |> fail ("not a negation: " ^ quote f); -fun appgen_eq thy defs (f as ("op =", Type ("fun", [ty, _])), ts) trns = +fun appgen_eq thy tabs (f as ("op =", Type ("fun", [ty, _])), ts) trns = let - fun mk_eq_pred_inst (dtco, (eqpred, arity)) trns = - let - val name_dtco = (the oo tname_of_idf) thy 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; - 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)]), []) - in - trns - |> gen_ensure_def [("eqinst", mk_eq_inst)] ("generating equality instance for " ^ quote dtco) idf_eqinst - end; fun mk_eq_expr (_, [t1, t2]) trns = trns - |> invoke_eq (invoke_cg_type thy defs) mk_eq_pred_inst ty + |> invoke_eq (invoke_cg_type thy tabs) (ensure_def_eq thy tabs) ty |-> (fn false => error ("could not derive equality for " ^ Sign.string_of_typ thy ty) | true => fn trns => trns - |> invoke_cg_expr thy defs t1 - ||>> invoke_cg_expr thy defs t2 + |> invoke_cg_expr thy tabs t1 + ||>> invoke_cg_expr thy tabs t2 |-> (fn (e1, e2) => pair (Fun_eq `$ e1 `$ e2))) in trns - |> fix_nargs thy defs mk_eq_expr (2, 2) (Const f, ts) + |> fix_nargs thy tabs mk_eq_expr (2, 2) (Const f, ts) end - | appgen_eq thy defs ((f, _), _) trns = + | appgen_eq thy tabs ((f, _), _) trns = trns |> fail ("not an equality: " ^ quote f); -(* invoke_eq: ((string * def) -> transact -> transact) -> itype -> transact -> bool * transact; *) - (* definition generators *) -fun defgen_tyco_fallback thy defs tyco trns = +fun defgen_tyco_fallback thy tabs tyco trns = if Symtab.fold (fn (_, { syntax_tyco, ... }) => fn b => b orelse Symtab.defined syntax_tyco tyco) ((#serialize_data o CodegenData.get) thy) false then @@ -752,41 +827,41 @@ trns |> fail ("no code generation fallback for " ^ quote tyco) -fun defgen_const_fallback thy defs f trns = - if Symtab.fold (fn (_, { syntax_const, ... }) => fn b => b orelse Symtab.defined syntax_const f) +fun defgen_const_fallback thy tabs c trns = + if Symtab.fold (fn (_, { syntax_const, ... }) => fn b => b orelse Symtab.defined syntax_const c) ((#serialize_data o CodegenData.get) thy) false then trns - |> debug 5 (fn _ => "trying defgen const fallback for " ^ quote f) + |> debug 5 (fn _ => "trying defgen const fallback for " ^ quote c) |> succeed (Nop, []) else trns - |> fail ("no code generation fallback for " ^ quote f) + |> fail ("no code generation fallback for " ^ quote c) -fun defgen_defs thy (defs as (_, defs', _)) f trns = - case Symtab.lookup defs' f - of SOME (args, rhs, ty) => +fun defgen_defs thy (tabs as ((deftab, _), _)) c trns = + case Symtab.lookup deftab c + of SOME (ty, (args, rhs)) => trns - |> debug 5 (fn _ => "trying defgen def for " ^ quote f) - |> mk_fun thy defs [(args, rhs)] (devarify_type ty) + |> debug 5 (fn _ => "trying defgen def for " ^ quote c) + |> mk_fun thy tabs [(args, rhs)] (devarify_type ty) |-> (fn def => succeed (def, [])) - | _ => trns |> fail ("no definition found for " ^ quote f); + | _ => trns |> fail ("no definition found for " ^ quote c); -fun defgen_clsdecl thy defs cls trns = +fun defgen_clsdecl thy (tabs as (_, (insttab, _, _))) (cls : string) trns = case name_of_idf thy nsp_class cls of SOME cls => let - val memnames = ClassPackage.the_consts thy cls; + val memnames = ClassPackage.the_consts thy (cls : string); val memtypes = map (devarify_type o ClassPackage.get_const_sign thy "'a") memnames; val memctxt = map (ClassPackage.extract_sortctxt thy) memtypes; val memidfs = map (idf_of_name thy nsp_mem) memnames; - val instnames = map (curry (idf_of_inst thy defs) cls) ((map fst o ClassPackage.the_tycos thy) cls); + fun mk_instname (tyco, thyname) = idf_of_name thy nsp_inst (InstNameMangler.get thy insttab (thyname, (cls, tyco))) + val instnames = map mk_instname (ClassPackage.the_tycos thy cls); in trns |> debug 5 (fn _ => "trying defgen class declaration for " ^ quote cls) - |> fold_map (ensure_def_class thy defs) - (map (idf_of_name thy nsp_class) (ClassPackage.get_superclasses thy cls)) - ||>> fold_map (invoke_cg_type thy defs) memtypes + |> fold_map (ensure_def_class thy tabs) (ClassPackage.get_superclasses thy cls) + ||>> fold_map (invoke_cg_type thy tabs) memtypes |-> (fn (supcls, memtypes) => succeed (Class (supcls, "a", memidfs ~~ (memctxt ~~ memtypes), []), memidfs @ instnames)) end @@ -794,55 +869,46 @@ trns |> fail ("no class definition found for " ^ quote cls); -fun defgen_clsmem thy (defs as (_, _, _)) f trns = - case name_of_idf thy nsp_mem f - of SOME clsmem => +fun defgen_clsmem thy tabs m trns = + case name_of_idf thy nsp_mem m + of SOME m => trns - |> debug 5 (fn _ => "trying defgen class member for " ^ quote f) - |> ensure_def_class thy defs (idf_of_name thy nsp_class ((the o ClassPackage.lookup_const_class thy) clsmem)) + |> debug 5 (fn _ => "trying defgen class member for " ^ quote m) + |> ensure_def_class thy tabs ((the o ClassPackage.lookup_const_class thy) m) |-> (fn cls => succeed (Classmember cls, [])) | _ => - trns |> fail ("no class member found for " ^ quote f) + trns |> fail ("no class member found for " ^ quote m) -fun defgen_clsinst thy defs clsinst trns = - case inst_of_idf thy defs clsinst - of SOME (cls, tyco) => +fun defgen_clsinst thy (tabs as (_, (insttab, _, _))) inst trns = + case Option.map (InstNameMangler.rev thy insttab) (name_of_idf thy nsp_inst inst) + of SOME (_, (cls, tyco)) => let - val _ = debug 10 (fn _ => "(1) CLSINST " ^ cls ^ " - " ^ tyco) () - val arity = (map o map) (idf_of_name thy nsp_class) - (ClassPackage.get_arities thy [cls] tyco); - val _ = debug 10 (fn _ => "(2) CLSINST " ^ cls ^ " - " ^ tyco) () - val clsmems = map (idf_of_name thy nsp_mem) - (ClassPackage.the_consts thy cls); - val _ = debug 10 (fn _ => "(3) CLSINST " ^ cls ^ " - " ^ tyco) () - val _ = debug 10 (fn _ => AList.string_of_alist I (Sign.string_of_typ thy) (ClassPackage.get_inst_consts_sign thy (tyco, cls))) () - val instmem_idfs = map (idf_of_cname thy defs) - (ClassPackage.get_inst_consts_sign thy (tyco, cls)); - val _ = debug 10 (fn _ => "(4) CLSINST " ^ cls ^ " - " ^ tyco) () + 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); 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 _ = debug 10 (fn _ => "(5) CLSINST " ^ cls ^ " - " ^ tyco) () in trns |> debug 5 (fn _ => "trying defgen class instance for (" ^ quote cls ^ ", " ^ quote tyco ^ ")") - |> (fold_map o fold_map) (ensure_def_class thy defs) arity - ||>> fold_map (ensure_def_const thy defs) clsmems - |-> (fn (arity, clsmems) => add_vars arity clsmems) - ||>> ensure_def_class thy defs (idf_of_name thy nsp_class cls) - ||>> ensure_def_tyco thy defs (idf_of_tname thy tyco) - ||>> fold_map (ensure_def_const thy defs) instmem_idfs - |-> (fn ((((arity, clsmems), cls), tyco), instmem_idfs) => - succeed (Classinst (cls, (tyco, arity), clsmems ~~ instmem_idfs), [])) + |> (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), [])) end | _ => - trns |> fail ("no class instance found for " ^ quote clsinst); + trns |> fail ("no class instance found for " ^ quote inst); (* parametrized generators, for instantiation in HOL *) -fun appgen_let strip_abs thy defs (f as ("Let", _), ts) trns = +fun appgen_let strip_abs thy tabs (f as ("Let", _), ts) trns = let fun dest_let (l as Const ("Let", _) $ t $ u) = (case strip_abs 1 u @@ -851,8 +917,8 @@ | dest_let t = ([], t); fun mk_let (l, r) trns = trns - |> invoke_cg_expr thy defs l - ||>> invoke_cg_expr thy defs r + |> invoke_cg_expr thy tabs l + ||>> invoke_cg_expr thy tabs r |-> (fn (l, r) => pair (r, ipat_of_iexpr l)); fun gen_let (t1, [t2, t3]) trns = let @@ -860,38 +926,38 @@ in trns |> fold_map mk_let lets - ||>> invoke_cg_expr thy defs body + ||>> invoke_cg_expr thy tabs body |-> (fn (lets, body) => pair (Library.foldr (fn ((e, p), body) => ICase (e, [(p, body)])) (lets, body))) end; in trns - |> fix_nargs thy defs gen_let (2, 2) (Const f, ts) + |> fix_nargs thy tabs gen_let (2, 2) (Const f, ts) end - | appgen_let strip_abs thy defs ((f, _), _) trns = + | appgen_let strip_abs thy tabs ((f, _), _) trns = trns |> fail ("not a let: " ^ quote f); -fun appgen_split strip_abs thy defs (f as ("split", _), ts) trns = +fun appgen_split strip_abs thy tabs (f as ("split", _), ts) trns = let fun gen_split (t1, [t2]) trns = let val ([p], body) = strip_abs 1 (t1 $ t2) in trns - |> invoke_cg_expr thy defs p - ||>> invoke_cg_expr thy defs body + |> invoke_cg_expr thy tabs p + ||>> invoke_cg_expr thy tabs body |-> (fn (IVarE v, body) => pair (IAbs (v, body))) end in trns - |> fix_nargs thy defs gen_split (1, 1) (Const f, ts) + |> fix_nargs thy tabs gen_split (1, 1) (Const f, ts) end - | appgen_split strip_abs thy defs ((f, _), _) trns = + | appgen_split strip_abs thy tabs ((f, _), _) trns = trns |> fail ("not a split: " ^ quote f); -fun appgen_number_of dest_binum mk_int_to_nat thy defs (f as ("Numeral.number_of", +fun appgen_number_of dest_binum mk_int_to_nat thy tabs (f as ("Numeral.number_of", Type ("fun", [_, Type ("IntDef.int", [])])), ts) trns = let fun gen_num (_, [bin]) trns = @@ -901,23 +967,23 @@ => error ("not a number: " ^ Sign.string_of_term thy bin)) in trns - |> fix_nargs thy defs gen_num (1, 1) (Const f, ts) + |> fix_nargs thy tabs gen_num (1, 1) (Const f, ts) end - | appgen_number_of dest_binum mk_int_to_nat thy defs (f as ("Numeral.number_of", + | appgen_number_of dest_binum mk_int_to_nat thy tabs (f as ("Numeral.number_of", Type ("fun", [_, Type ("nat", [])])), ts) trns = let fun gen_num (_, [bin]) trns = trns - |> invoke_cg_expr thy defs (mk_int_to_nat bin) + |> invoke_cg_expr thy tabs (mk_int_to_nat bin) in trns - |> fix_nargs thy defs gen_num (1, 1) (Const f, ts) + |> fix_nargs thy tabs gen_num (1, 1) (Const f, ts) end - | appgen_number_of dest_binum mk_int_to_nat thy defs ((f, _), _) trns = + | appgen_number_of dest_binum mk_int_to_nat thy tabs ((f, _), _) trns = trns |> fail ("not a number_of: " ^ quote f); -fun appgen_case get_case_const_data thy defs ((f, ty), ts) trns = +fun appgen_case get_case_const_data thy tabs ((f, ty), ts) trns = let fun cg_case_d gen_names dty (((cname, i), ty), t) trns = let @@ -927,21 +993,19 @@ val t' = Envir.beta_norm (list_comb (t, frees)); in trns - |> invoke_cg_expr thy defs (list_comb (Const (cname, tys ---> dty), frees)) - ||>> invoke_cg_expr thy defs t' + |> invoke_cg_expr thy tabs (list_comb (Const (cname, tys ---> dty), frees)) + ||>> invoke_cg_expr thy tabs t' |-> (fn (ep, e) => pair (ipat_of_iexpr ep, e)) end; fun cg_case dty cs (_, ts) trns = let val (ts', t) = split_last ts - val _ = debug 10 (fn _ => " in " ^ Sign.string_of_typ thy dty ^ ", pairing " - ^ (commas o map (fst o fst)) cs ^ " with " ^ (commas o map (Sign.string_of_term thy)) ts') (); fun gen_names i = variantlist (replicate i "x", foldr add_term_names (map (fst o fst o dest_Var) (foldr add_term_vars [] ts)) ts) in trns - |> invoke_cg_expr thy defs t + |> invoke_cg_expr thy tabs t ||>> fold_map (cg_case_d gen_names dty) (cs ~~ ts') |-> (fn (t, ds) => pair (ICase (t, ds))) end; @@ -955,180 +1019,145 @@ val (tys, dty) = (split_last o fst o strip_type) ty; in trns - |> debug 9 (fn _ => "for case const " ^ f ^ "::" - ^ Sign.string_of_typ thy ty ^ ",\n with " ^ AList.string_of_alist I string_of_int cs - ^ ",\n given as args " ^ (commas o map (Sign.string_of_term thy)) ts - ^ ",\n with significant length " ^ string_of_int (length cs + 1)) - |> fix_nargs thy defs (cg_case dty (cs ~~ tys)) + |> fix_nargs thy tabs (cg_case dty (cs ~~ tys)) (length cs + 1, length cs + 1) (Const (f, ty), ts) end end; -fun defgen_datatype get_datatype get_datacons thy defs idf trns = - case tname_of_idf thy idf +fun defgen_datatype get_datatype get_datacons thy (tabs as (_, (_, _, dtcontab))) dtco trns = + case name_of_idf thy nsp_tyco dtco of SOME dtco => (case get_datatype thy dtco of SOME (vars, cos) => let val cotys = map (the o get_datacons thy o rpair dtco) cos; - val coidfs = cos - |> map (idf_of_name thy nsp_const) - |> map (fn "0" => "const.Zero" | c => c); + val coidfs = map (fn co => (DatatypeconsNameMangler.get thy dtcontab (co, dtco)) |> + idf_of_name thy nsp_dtcon) cos; in trns |> debug 5 (fn _ => "trying defgen datatype for " ^ quote dtco) - |> fold_map (invoke_cg_sort thy defs) (map snd vars) - ||>> (fold_map o fold_map) (invoke_cg_type thy defs o devarify_type) cotys + |> fold_map (invoke_cg_sort thy tabs) (map snd vars) + ||>> (fold_map o fold_map) (invoke_cg_type thy tabs o devarify_type) cotys |-> (fn (sorts, tys) => succeed (Datatype (map2 (fn (v, _) => fn sort => (unprefix "'" v, sort)) vars sorts, coidfs ~~ tys, []), - coidfs - (* |> add_eqinst get_datacons thy (snd trns) dtname cnames *))) - (*! VARIABLEN, EQTYPE !*) + coidfs)) end | NONE => trns |> fail ("no datatype found for " ^ quote dtco)) | NONE => trns - |> fail ("not a type constructor: " ^ quote idf) + |> fail ("not a type constructor: " ^ quote dtco) -fun defgen_datacons get_datacons thy defs f trns = - let - fun the_type "0" = SOME "nat" - | the_type c = - case strip_type (Sign.the_const_constraint thy c) - of (_, Type (dtname, _)) => SOME dtname - | _ => NONE - in - case cname_of_idf thy defs f - of SOME (c, _) => - (case the_type c - of SOME dtname => - (case get_datacons thy (c, dtname) - of SOME _ => - trns - |> debug 5 (fn _ => "trying defgen datatype constructor for " ^ quote c) - |> ensure_def_tyco thy defs (idf_of_tname thy dtname) - |-> (fn dtname => succeed (Datatypecons dtname, [])) - | NONE => - trns - |> fail ("no datatype constructor found for " ^ quote f)) - | NONE => - trns - |> fail ("no datatype constructor found for " ^ quote f)) - | _ => - trns - |> fail ("not a constant: " ^ quote f) - end; +fun defgen_datacons get_datacons thy (tabs as (_, (_, _, dtcontab))) co trns = + case Option.map (DatatypeconsNameMangler.rev thy dtcontab) (name_of_idf thy nsp_dtcon co) + of SOME (co, dtco) => + trns + |> debug 5 (fn _ => "trying defgen datatype constructor for " ^ quote co) + |> ensure_def_tyco thy tabs dtco + |-> (fn tyco => succeed (Datatypecons tyco, [])) + | _ => + trns + |> fail ("not a datatype constructor: " ^ quote co); -fun defgen_recfun get_equations thy defs f trns = - case cname_of_idf thy defs f - of SOME (f, ty) => +fun defgen_recfun get_equations thy tabs c trns = + case recconst_of_idf thy tabs c + of SOME (c, ty) => let - val (eqs, ty) = get_equations thy (f, ty); + val (eqs, ty) = get_equations thy (c, ty); in case eqs of (_::_) => trns - |> debug 5 (fn _ => "trying defgen recfun for " ^ quote f) - |> mk_fun thy defs eqs (devarify_type ty) + |> debug 5 (fn _ => "trying defgen recfun for " ^ quote c) + |> mk_fun thy tabs eqs (devarify_type ty) |-> (fn def => succeed (def, [])) | _ => trns - |> fail ("no recursive definition found for " ^ quote f) + |> fail ("no recursive definition found for " ^ quote c) end | NONE => trns - |> fail ("not a constant: " ^ quote f); + |> fail ("not a constant: " ^ quote c); (* theory interface *) -fun mk_deftab thy = +fun mk_tabs thy = let - fun mangle_tyname (ty_decl, ty_def) = + fun extract_defs thy = let - fun mangle (Type (tyco, tys)) = - NameSpace.base tyco :: Library.flat (List.mapPartial mangle tys) |> SOME - | mangle _ = - NONE + fun dest t = + let + val (lhs, rhs) = Logic.dest_equals t; + val (c, args) = strip_comb lhs; + val (s, T) = dest_Const c + in if forall is_Var args then SOME (s, (T, (args, rhs))) else NONE + end handle TERM _ => NONE; + fun prep_def def = (case Codegen.preprocess thy [def] of + [def'] => prop_of def' | _ => error "mk_auxtab: bad preprocessor"); + fun add_def (name, t) defs = (case dest t of + NONE => defs + | SOME _ => (case (dest o prep_def oo Thm.get_axiom) thy name of + NONE => defs + | SOME (s, (T, (args, rhs))) => Symtab.update + (s, (T, (split_last (args @ [rhs]))) :: + if_none (Symtab.lookup defs s) []) defs)) in - Vartab.empty - |> Sign.typ_match thy (ty_decl, ty_def) - |> map (snd o snd) o Vartab.dest - |> List.mapPartial mangle - |> Library.flat - |> null ? K ["x"] - |> space_implode "_" + Symtab.empty + |> fold (Symtab.fold add_def) (map + (snd o #axioms o Theory.rep_theory) (thy :: Theory.ancestors_of thy)) end; - fun mangle_instname thyname (cls, tyco) = - idf_of_name thy nsp_inst - (NameSpace.append thyname (NameSpace.base cls ^ "_" ^ NameSpace.base tyco)) - fun add_clsmems classtab ((overl, overl_rev), defs, (clstab, clstab_rev, clsmems)) = - ((overl - |> Symtab.fold - (fn (class, (clsmems, _)) => - fold - (fn clsmem => - Symtab.default (clsmem, []) - #> Symtab.map_entry clsmem - (cons (Sign.the_const_type thy clsmem, idf_of_name thy nsp_mem clsmem)) - ) clsmems - ) classtab, - overl_rev - |> Symtab.fold - (fn (class, (clsmems, _)) => - fold - (fn clsmem => - Symtab.update_new - (idf_of_name thy nsp_mem clsmem, (clsmem, Sign.the_const_type thy clsmem)) - ) clsmems - ) classtab), - defs, - (clstab - |> Symtab.fold - (fn (cls, (_, clsinsts)) => fold - (fn (tyco, thyname) => Insttab.update ((cls, tyco), mangle_instname thyname (cls, tyco))) clsinsts) - classtab, - clstab_rev - |> Symtab.fold - (fn (cls, (_, clsinsts)) => fold - (fn (tyco, thyname) => Symtab.update (mangle_instname thyname (cls, tyco), (cls, tyco))) clsinsts) - classtab, - clsmems - |> Symtab.fold - (fn (class, (clsmems, _)) => fold - (fn clsmem => Symtab.update (clsmem, class)) clsmems) - classtab)) - fun add_def (name, [(ty, (_, (args, rhs)))]) (overl, defs, clstab) = - (overl, - defs |> Symtab.update_new (idf_of_name thy nsp_const name, (args, rhs, ty)), - clstab) - | add_def (name, ds) ((overl, overl_rev), defs, clstab) = - let - val ty_decl = Sign.the_const_constraint thy name; - fun mk_idf ("0", Type ("nat", [])) = "const.Zero" - | mk_idf ("1", Type ("nat", [])) = "." - | mk_idf (nm, ty) = - if is_number nm - then nm - else idf_of_name thy nsp_const nm - ^ "_" ^ mangle_tyname (ty_decl, ty) - val overl_lookups = map - (fn (ty, (_, (args, rhs))) => (ty, mk_idf (name, ty), args, rhs)) ds; - in - ((overl - |> Symtab.default (name, []) - |> Symtab.map_entry name (append (map (fn (ty, idf, _, _) => (ty, idf)) overl_lookups)), - overl_rev - |> fold Symtab.update_new (map (fn (ty, idf, _, _) => (idf, (name, ty))) overl_lookups)), - defs - |> fold Symtab.update_new (map (fn (ty, idf, args, rhs) => (idf, (args, rhs, ty))) overl_lookups), clstab) - end; in - ((Symtab.empty, Symtab.empty), Symtab.empty, (Insttab.empty, Symtab.empty, Symtab.empty)) - |> add_clsmems (ClassPackage.get_classtab thy) - |> fold add_def (Codegen.mk_deftab thy |> Symtab.dest) - end; + fun mk_insttab thy = + InstNameMangler.empty + |> Symtab.fold_map + (fn (cls, (_, clsinsts)) => fold_map + (fn (tyco, thyname) => InstNameMangler.declare thy (thyname, (cls, tyco))) clsinsts) + (ClassPackage.get_classtab thy) + |-> (fn _ => I); + fun mk_overltabs thy defs = + (Symtab.empty, ConstNameMangler.empty) + |> Symtab.fold + (fn (c, [_]) => I + | ("0", _) => I + | (c, tytab) => + (fn (overltab1, overltab2) => ( + overltab1 + |> Symtab.update_new (c, (Sign.the_const_constraint thy c, map fst tytab)), + overltab2 + |> fold (fn (ty, _) => ConstNameMangler.declare thy (idf_of_name thy nsp_overl c, (Sign.the_const_constraint thy c, ty)) #> snd) tytab + ))) defs; + fun mk_dtcontab thy = + DatatypeconsNameMangler.empty + |> fold_map + (fn (co, dtcos) => DatatypeconsNameMangler.declare_multi thy + (map (pair co) dtcos)) + (get_all_datatype_cons thy) + |-> (fn _ => I); + fun mk_deftab thy defs overltab = + Symtab.empty + |> Symtab.fold + (fn (c, [ty_cdef]) => + Symtab.update_new (idf_of_name thy nsp_const c, ty_cdef) + | ("0", _) => I + | (c, cdefs) => fold (fn (ty, cdef) => + let + val c' = ConstNameMangler.get thy overltab + (idf_of_name thy nsp_overl c, (Sign.the_const_constraint thy c, ty)) + in Symtab.update_new (c', (ty, cdef)) end) cdefs) defs; + fun mk_clsmemtab thy = + Symtab.empty + |> Symtab.fold + (fn (class, (clsmems, _)) => fold + (fn clsmem => Symtab.update (clsmem, class)) clsmems) + (ClassPackage.get_classtab thy); + val defs = extract_defs thy; + val insttab = mk_insttab thy; + val overltabs = mk_overltabs thy defs; + val dtcontab = mk_dtcontab thy; + val deftab = mk_deftab thy defs (snd overltabs); + val clsmemtab = mk_clsmemtab thy; + in ((deftab, clsmemtab), (insttab, overltabs, dtcontab)) end; fun check_for_serializer serial_name serialize_data = if Symtab.defined serialize_data serial_name @@ -1169,7 +1198,7 @@ (map_serialize_data (fn (primitives, syntax_tyco, syntax_const) => (primitives |> add_primdef primdef, - syntax_tyco |> Symtab.update_new (tyco, mfx), + syntax_tyco |> Symtab.update_new (idf_of_name thy nsp_tyco tyco, mfx), syntax_const))), logic_data))) end; @@ -1194,23 +1223,24 @@ (Codegen.quotes_of proto_mfx); in thy - |> expand_module (mk_deftab thy) generate + |> expand_module (mk_tabs thy) generate |-> (fn tys => pair (Codegen.replace_quotes tys proto_mfx)) end; in - gen_add_syntax_tyco (fn thy => idf_of_tname thy o Sign.intern_type thy) + gen_add_syntax_tyco Sign.intern_type prep_mfx mk_name (newline_correct o Symbol.strip_blanks) end; -fun gen_add_syntax_const prep_const prep_mfx prep_primname prep_primdef serial_name ((raw_f, raw_mfx), primdef) thy = +fun gen_add_syntax_const prep_const prep_mfx prep_primname prep_primdef serial_name ((raw_c, raw_mfx), primdef) thy = let - val f = prep_const thy raw_f; - val _ = if member (op =) prims f - then error ("attempted to re-define primitive " ^ quote f) + val (c, ty) = prep_const thy raw_c; + val tabs = mk_tabs thy; + val _ = if member (op =) prims c + then error ("attempted to re-define primitive " ^ quote c) else () fun add_primdef NONE = I | add_primdef (SOME (name, (def, deps))) = - CodegenSerializer.add_prim (prep_primname thy f name, (prep_primdef def, deps)) + CodegenSerializer.add_prim (prep_primname thy c name, (prep_primdef def, deps)) in thy |> prep_mfx raw_mfx @@ -1222,22 +1252,21 @@ (fn (primitives, syntax_tyco, syntax_const) => (primitives |> add_primdef primdef, syntax_tyco, - syntax_const |> Symtab.update_new (f, mfx)))), + syntax_const |> Symtab.update_new (idf_of_const thy tabs (c, ty), mfx)))), logic_data))) end; val add_syntax_const_i = gen_add_syntax_const (K I) pair ((K o K) I) I; val add_syntax_const = let - fun prep_const thy (raw_f, raw_ty) = + fun prep_const thy (raw_c, raw_ty) = let - val defs = mk_deftab thy; - val f = Sign.intern_const thy raw_f; + val c = Sign.intern_const thy raw_c; val ty = raw_ty |> Option.map (Sign.read_tyname thy) - |> the_default (Sign.the_const_constraint thy f); - in idf_of_cname thy defs (f, ty) end; + |> the_default (Sign.the_const_constraint thy c); + in (c, ty) end; fun mk_name _ _ (SOME name) = name | mk_name thy f NONE = let @@ -1255,7 +1284,7 @@ (Codegen.quotes_of proto_mfx); in thy - |> expand_module (mk_deftab thy) generate + |> expand_module (mk_tabs thy) generate |-> (fn es => pair (Codegen.replace_quotes es proto_mfx)) end; in @@ -1279,13 +1308,13 @@ fun generate_code consts thy = let - val defs = mk_deftab thy; - val consts' = map (idf_of_cname thy defs o mk_const thy) consts; - fun generate thy defs = fold_map (ensure_def_const thy defs) consts' + val tabs = mk_tabs thy; + val consts' = map (mk_const thy) consts; + fun generate thy tabs = fold_map (ensure_def_const thy tabs) consts' in thy - |> expand_module defs generate - |-> (fn _ => pair consts') + |> expand_module tabs generate + |-> (fn consts => pair consts) end; fun serialize_code serial_name filename consts thy = @@ -1321,6 +1350,33 @@ end; +(* inconsistent names *) + +fun rename_inconsistent thy = + let + fun get_inconsistent thyname = + let + val thy = theory thyname; + fun own_tables get = + (get thy) + |> fold (Symtab.fold (Symtab.remove (K true)) o get) (Theory.parents_of thy) + |> Symtab.keys; + val names = own_tables (#2 o #types o Type.rep_tsig o Sign.tsig_of) + @ own_tables (#2 o #declarations o Consts.dest o #consts o Sign.rep_sg); + fun diff names = + fold (fn name => + if is_prefix (op =) (NameSpace.unpack thyname) (NameSpace.unpack name) + then I + else cons (name, NameSpace.append thyname (NameSpace.base name))) names []; + in diff names end; + val inconsistent = map get_inconsistent (ThyInfo.names ()) |> Library.flat; + fun add (src, dst) thy = + if (is_some oo Symtab.lookup o fst o #alias o #logic_data o CodegenData.get) thy src + then (warning ("code generator alias already defined for " ^ quote src ^ ", will not overwrite"); thy) + else add_alias (src, dst) thy + in fold add inconsistent thy end; + + (* toplevel interface *) local @@ -1431,30 +1487,36 @@ add_defgen ("defs", defgen_defs), add_defgen ("clsmem", defgen_clsmem), add_defgen ("clsinst", defgen_clsinst), - add_alias ("op <>", "op_neq"), + add_alias ("op -->", "HOL.op_implies"), + add_alias ("op +", "HOL.op_add"), + add_alias ("op -", "HOL.op_minus"), + add_alias ("op *", "HOL.op_times"), +(* add_alias ("0", "Nat.Zero"), *) + add_alias ("op <>", "HOL.op_neq"), add_alias ("op >=", "op_ge"), add_alias ("op >", "op_gt"), add_alias ("op <=", "op_le"), add_alias ("op <", "op_lt"), - add_alias ("op +", "op_add"), - add_alias ("op -", "op_minus"), - add_alias ("op *", "op_times"), - add_alias ("op @", "op_append"), + add_alias ("List.op @", "List.append"), + add_alias ("List.op mem", "List.member"), + add_alias ("Divides.op div", "Divides.div"), + add_alias ("Divides.op dvd", "Divides.dvd"), + add_alias ("Divides.op mod", "Divides.mod"), add_lookup_tyco ("bool", type_bool), + add_lookup_tyco ("*", type_pair), add_lookup_tyco ("IntDef.int", type_integer), add_lookup_tyco ("List.list", type_list), - add_lookup_tyco ("*", type_pair), add_lookup_const (("True", bool), Cons_true), add_lookup_const (("False", bool), Cons_false), add_lookup_const (("Not", bool --> bool), Fun_not), add_lookup_const (("op &", bool --> bool --> bool), Fun_and), add_lookup_const (("op |", bool --> bool --> bool), Fun_or), add_lookup_const (("HOL.If", bool --> A --> A --> A), Fun_if), - add_lookup_const (("List.list.Cons", A --> list A --> list A), Cons_cons), - add_lookup_const (("List.list.Nil", list A), Cons_nil), add_lookup_const (("Pair", A --> B --> pair A B), Cons_pair), add_lookup_const (("fst", pair A B --> A), Fun_fst), add_lookup_const (("snd", pair A B --> B), Fun_snd), + add_lookup_const (("List.list.Cons", A --> list A --> list A), Cons_cons), + add_lookup_const (("List.list.Nil", list A), Cons_nil), add_lookup_const (("1", nat), IApp ( IConst ("const.Suc", IFun (IType ("type.nat", []), IFun (IType ("type.nat", []), IType ("type.nat", [])))), @@ -1467,8 +1529,7 @@ add_lookup_const (("uminus", int --> int), Fun_minus), add_lookup_const (("op <", int --> int --> bool), Fun_lt), add_lookup_const (("op <=", int --> int --> bool), Fun_le), - add_lookup_const (("Wellfounded_Recursion.wfrec", ((A --> B) --> A --> B) --> A --> B), Fun_wfrec), - add_lookup_const (("op =", A --> A --> bool), Fun_eq) + add_lookup_const (("Wellfounded_Recursion.wfrec", ((A --> B) --> A --> B) --> A --> B), Fun_wfrec) ] end; (* "op /" ??? *) diff -r 2b2fbc32550e -r 6720b5010a57 src/Pure/Tools/codegen_serializer.ML --- a/src/Pure/Tools/codegen_serializer.ML Wed Dec 21 15:18:57 2005 +0100 +++ b/src/Pure/Tools/codegen_serializer.ML Wed Dec 21 15:19:16 2005 +0100 @@ -409,7 +409,6 @@ in mk_app_p br (pr (map (ml_from_expr BR) es1) (ml_from_expr BR)) es2 end; fun ml_from_funs (ds as d::ds_tl) = let - val _ = debug 15 (fn _ => "(1) FUN") (); fun mk_definer [] = "val" | mk_definer _ = "fun" fun check_args (_, Fun ((pats, _)::_, _)) NONE = @@ -420,12 +419,9 @@ else error ("mixing simultaneous vals and funs not implemented") | check_args _ _ = error ("function definition block containing other definitions than functions") - val _ = debug 15 (fn _ => "(2) FUN") (); val definer = the (fold check_args ds NONE); - val _ = debug 15 (fn _ => "(3) FUN") (); fun mk_eq definer f ty (pats, expr) = let - val _ = debug 15 (fn _ => "(5) FUN") (); fun mk_pat_arg p = case itype_of_ipat p of ty as IType (tyco, _) => @@ -439,20 +435,16 @@ ] else ml_from_pat BR p | _ => ml_from_pat BR p; - val _ = debug 15 (fn _ => "(6) FUN") (); val lhs = [Pretty.str (definer ^ " " ^ f)] @ (if null pats then [Pretty.str ":", ml_from_type NOBR ty] else map mk_pat_arg pats) - val _ = debug 15 (fn _ => "(7) FUN") (); val rhs = [Pretty.str "=", ml_from_expr NOBR expr] - val _ = debug 15 (fn _ => "(8) FUN") (); in Pretty.block (separate (Pretty.brk 1) (lhs @ rhs)) end fun mk_fun definer (f, Fun (eqs as eq::eq_tl, (_, ty))) = let - val _ = debug 15 (fn _ => "(4) FUN") (); val (pats_hd::pats_tl) = (fst o split_list) eqs; val shift = if null eq_tl then I else map (Pretty.block o single); in (Pretty.block o Pretty.fbreaks o shift) ( @@ -520,12 +512,11 @@ NONE | ml_from_def (name, Classinst _) = error ("can't serialize instance declaration " ^ quote name ^ " to ML") - in (debug 10 (fn _ => "*** defs " ^ commas (map (fn (n, d) => n ^ " = " ^ (Pretty.output o pretty_def) d) ds)) (); - case ds + in case ds of (_, Fun _)::_ => ml_from_funs ds | (_, Datatypecons _)::_ => ml_from_datatypes ds | (_, Datatype _)::_ => ml_from_datatypes ds - | [d] => ml_from_def d) + | [d] => ml_from_def d end; in @@ -561,7 +552,7 @@ Pretty.str ("end; (* struct " ^ name ^ " *)") ]); fun is_dicttype tyco = - case get_def module tyco + NameSpace.is_qualified tyco andalso case get_def module tyco of Typesyn (_, IDictT _) => true | _ => false; fun eta_expander "Pair" = 2 @@ -588,7 +579,6 @@ else 0; in module - |> debug 12 (Pretty.output o pretty_module) |> debug 3 (fn _ => "selecting submodule...") |> (if is_some select then (partof o the) select else I) |> debug 3 (fn _ => "eta-expanding...") @@ -599,7 +589,6 @@ |> tupelize_cons |> debug 3 (fn _ => "eliminating classes...") |> eliminate_classes - |> debug 12 (Pretty.output o pretty_module) |> debug 3 (fn _ => "serializing...") |> serialize (ml_from_defs tyco_syntax const_syntax is_dicttype) ml_from_module ml_validator nspgrp name_root |> (fn p => Pretty.chunks [setmp print_mode [] (Pretty.str o mk_prims) prims, p]) @@ -894,9 +883,7 @@ else error ("empty statement during serialization: " ^ quote name) | haskell_from_def (name, Fun (eqs, (_, ty))) = let - val _ = print "(1) FUN"; fun from_eq name (args, rhs) = - (print args; print rhs; Pretty.block [ Pretty.str (lower_first name), Pretty.block (map (fn p => Pretty.block [Pretty.brk 1, haskell_from_pat BR p]) args), @@ -904,8 +891,7 @@ Pretty.str ("="), Pretty.brk 1, haskell_from_expr NOBR rhs - ]) - val _ = print "(2) FUN"; + ] in Pretty.chunks [ Pretty.block [ @@ -991,7 +977,7 @@ ) instmems) ] |> SOME in - case List.mapPartial (fn (name, def) => (print ("serializing " ^ name); haskell_from_def (name, def))) defs + case List.mapPartial (fn (name, def) => haskell_from_def (name, def)) defs of [] => NONE | l => (SOME o Pretty.block) l end; @@ -1047,7 +1033,6 @@ | _ => false; in module - |> debug 12 (Pretty.output o pretty_module) |> debug 3 (fn _ => "selecting submodule...") |> (if is_some select then (partof o the) select else I) |> debug 3 (fn _ => "eta-expanding...") diff -r 2b2fbc32550e -r 6720b5010a57 src/Pure/Tools/codegen_thingol.ML --- a/src/Pure/Tools/codegen_thingol.ML Wed Dec 21 15:18:57 2005 +0100 +++ b/src/Pure/Tools/codegen_thingol.ML Wed Dec 21 15:19:16 2005 +0100 @@ -124,6 +124,8 @@ -> (string * Pretty.T list -> Pretty.T) -> (string -> string option) -> string list list -> string -> module -> Pretty.T + + val get_prefix: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list * ('a list * 'a list) end; signature CODEGEN_THINGOL_OP = @@ -167,13 +169,13 @@ val (ys, xs') = map_yield f xs in (y::ys, x'::xs') end; -fun get_prefix eq ([], ys) = ([], [], ys) - | get_prefix eq (xs, []) = ([], xs, []) +fun get_prefix eq ([], ys) = ([], ([], ys)) + | get_prefix eq (xs, []) = ([], (xs, [])) | get_prefix eq (xs as x::xs', ys as y::ys') = if eq (x, y) then - let val (ps', xs'', ys'') = get_prefix eq (xs', ys') - in (x::ps', xs'', ys'') end - else ([], xs, ys); + let val (ps', xys'') = get_prefix eq (xs', ys') + in (x::ps', xys'') end + else ([], (xs, ys)); (** language core - types, pattern, expressions **) @@ -555,7 +557,8 @@ Pretty.str tyco, Pretty.str ", ", Pretty.gen_list "," "[" "]" (map (Pretty.gen_list "," "{" "}" o map Pretty.str o snd) arity), - Pretty.str "))" + Pretty.str ")) with ", + Pretty.gen_list "," "[" "]" (map (fn (m1, m2) => Pretty.str (m1 ^ " => " ^ m2)) mems) ]; fun pretty_module modl = @@ -653,8 +656,8 @@ let val m1 = dest_name name1 |> apsnd single |> (op @); val m2 = dest_name name2 |> apsnd single |> (op @); - val (ms, r1, r2) = get_prefix (op =) (m1, m2); - val (ms, s1::r1, s2::r2) = get_prefix (op =) (m1, m2); + val (ms, (r1, r2)) = get_prefix (op =) (m1, m2); + val (ms, (s1::r1, s2::r2)) = get_prefix (op =) (m1, m2); val add_edge = if null r1 andalso null r2 then Graph.add_edge @@ -777,7 +780,7 @@ | *) add_check_transform (name, Classinst (clsname, (tyco, arity), memdefs)) = let val _ = debug 7 (fn _ => "transformation for class instance " ^ quote tyco - ^ " of class " ^ quote clsname) (); + ^ " of class " ^ quote clsname ^ " with " ^ (commas o map (fn (m1, m2) => m1 ^ " => " ^ m2)) memdefs) (); (* fun check [Classmember (_, v, mtyp_c), Fun (_, (_, mtyp_i))] = let val mtyp_i' = instant_itype (v, tyco `%% map IVarT arity) mtyp_c; @@ -901,8 +904,10 @@ modl |> debug 9 (fn _ => "creating node " ^ quote name) |> add_def (name, Nop) + |> debug 9 (fn _ => "checking creation of node " ^ quote name) |> select_generator (fn gname => "trying code generator " ^ gname ^ " for definition of " ^ quote name) name defgens + |> debug 9 (fn _ => "checking creation of node " ^ quote name) |> check_fail msg |-> (fn (def, names') => add (name, def) @@ -1206,16 +1211,12 @@ | extract_members _ = I; fun introduce_dicts (Class (supcls, v, membrs, insts)) = let - val _ = writeln "TRANSFORMING CLASS"; - val _ = print (Class (supcls, v, membrs, insts)); 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 _ = writeln "TRANSFORMING CLASSINST"; - val _ = print (Classinst (clsname, (tyco, arity), memdefs)); val Class (_, v, members, _) = if clsname = class_eq then @@ -1232,37 +1233,27 @@ end | introduce_dicts d = d; fun elim_sorts (Fun (eqs, ([], ty))) = - (writeln "TRANSFORMING FUN ()"; Fun (map (fn (ps, rhs) => (map transform_ipat ps, transform_iexpr [] rhs)) eqs, - ([], transform_itype ty))) + ([], transform_itype ty)) | elim_sorts (Fun (eqs, (sortctxt, ty))) = let - val _ = writeln "TRANSFORMING FUN (1)"; val varnames_ctxt = burrow (Term.invent_names ((vars_of_iexprs o map snd) eqs @ (vars_of_ipats o Library.flat o map fst) eqs) "d" o length) (map snd sortctxt); - val _ = writeln "TRANSFORMING FUN (2)"; val vname_alist = map2 (fn (vt, sort) => fn vs => (vt, vs ~~ sort)) - sortctxt varnames_ctxt |> print; - val _ = writeln "TRANSFORMING FUN (3)"; + sortctxt varnames_ctxt; val ty' = map (op ** o (fn (vt, vss) => map (fn (_, cls) => cls `%% [IVarT (vt, [])]) vss)) vname_alist `--> transform_itype ty; - val _ = writeln "TRANSFORMING FUN (4)"; val ps_add = map (XXp o (fn (vt, vss) => map (fn (v, cls) => IVarP (v, cls `%% [IVarT (vt, [])])) vss)) vname_alist; - val _ = writeln "TRANSFORMING FUN (5)"; - in Fun (map (fn (ps, rhs) => (ps_add @ map transform_ipat ps, transform_iexpr vname_alist rhs)) eqs, ([], ty')) before writeln "TRANSFORMING FUN (6)" end + in Fun (map (fn (ps, rhs) => (ps_add @ map transform_ipat ps, transform_iexpr vname_alist rhs)) eqs, ([], ty')) end | elim_sorts (Datatype (vars, constrs, insts)) = - (writeln "TRANSFORMING DATATYPE (1)"; Datatype (map (fn (v, _) => (v, [])) vars, map (apsnd (map transform_itype)) constrs, insts) - before writeln "TRANSFORMING DATATYPE (2)") | elim_sorts (Typesyn (vars, ty)) = - (writeln "TRANSFORMING TYPESYN (1)"; Typesyn (map (fn (v, _) => (v, [])) vars, transform_itype ty) - before writeln "TRANSFORMING TYPESYN (2)") | elim_sorts d = d; in module @@ -1349,7 +1340,7 @@ val modl' = if null modl then [] else (NameSpace.unpack o the o Symtab.lookup tab o NameSpace.pack) modl; val name' = (NameSpace.unpack o the o Symtab.lookup tab) name in - (NameSpace.pack o #3 o get_prefix (op =)) (modl', name') + (NameSpace.pack o snd o snd o get_prefix (op =)) (modl', name') |> debug 12 (fn name' => "resolving " ^ quote name ^ " to " ^ quote name' ^ " in " ^ (quote o NameSpace.pack) modl) end else name @@ -1360,21 +1351,16 @@ fun serialize s_def s_module validate nspgrp name_root module = let - val _ = debug 15 (fn _ => "serialize 1") (); val resolvtab = mk_resolvtab nspgrp validate module; - val _ = debug 15 (fn _ => "serialize 2") (); val resolver = mk_resolv resolvtab; - val _ = debug 15 (fn _ => "serialize 3") (); fun seri prfx ([(name, Module module)]) = - (debug 15 (fn _ => "serializing module " ^ quote name) (); s_module (resolver prfx (prfx @ [name] |> NameSpace.pack), List.mapPartial (seri (prfx @ [name])) ((map (AList.make (Graph.get_node module)) o rev o Graph.strong_conn) module)) - |> SOME) + |> SOME | seri prfx ds = - (debug 15 (fn _ => "serializing definitions " ^ (commas o map fst) ds) (); s_def (resolver prfx) (map - (fn (name, Def def) => (resolver prfx (prfx @ [name] |> NameSpace.pack), def)) ds)) + (fn (name, Def def) => (resolver prfx (prfx @ [name] |> NameSpace.pack), def)) ds) in setmp print_mode [] (fn _ => s_module (name_root, (List.mapPartial (seri []) ((map (AList.make (Graph.get_node module)) o rev o Graph.strong_conn) module)))) ()