# HG changeset patch # User haftmann # Date 1132762602 -3600 # Node ID 2eea98bbf65081b801eb857bbdd56122d6d8171d # Parent 4dc1f30af6a1ccedb21087eabb886beadcbb5d95 improved failure tracking diff -r 4dc1f30af6a1 -r 2eea98bbf650 src/Pure/Tools/codegen_package.ML --- a/src/Pure/Tools/codegen_package.ML Tue Nov 22 19:37:36 2005 +0100 +++ b/src/Pure/Tools/codegen_package.ML Wed Nov 23 17:16:42 2005 +0100 @@ -37,6 +37,8 @@ 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; @@ -66,7 +68,8 @@ val print_codegen_modl: theory -> unit; val mk_deftab: theory -> deftab; - structure CodegenData : THEORY_DATA; + structure CodegenData: THEORY_DATA; + structure Insttab: TABLE; end; structure CodegenPackage : CODEGEN_PACKAGE = @@ -91,9 +94,9 @@ * (term list * term * typ) Symtab.table * (string Insttab.table * (string * string) Symtab.table - * (class * (string * typ)) Symtab.table); + * class Symtab.table); -type codegen_class = theory -> deftab -> (class, class) gen_codegen; +type codegen_sort = theory -> deftab -> (sort, sort) gen_codegen; type codegen_type = theory -> deftab -> (typ, itype) gen_codegen; type codegen_expr = theory -> deftab -> (term, iexpr) gen_codegen; type defgen = theory -> deftab -> gen_defgen; @@ -127,30 +130,30 @@ (* theory data for codegen *) type gens = { - codegens_class: (string * (codegen_class * stamp)) list, + codegens_sort: (string * (codegen_sort * stamp)) list, codegens_type: (string * (codegen_type * stamp)) list, codegens_expr: (string * (codegen_expr * stamp)) list, defgens: (string * (defgen * stamp)) list }; val empty_gens = { - codegens_class = Symtab.empty, codegens_type = Symtab.empty, + codegens_sort = Symtab.empty, codegens_type = Symtab.empty, codegens_expr = Symtab.empty, defgens = Symtab.empty }; -fun map_gens f { codegens_class, codegens_type, codegens_expr, defgens } = +fun map_gens f { codegens_sort, codegens_type, codegens_expr, defgens } = let - val (codegens_class, codegens_type, codegens_expr, defgens) = - f (codegens_class, codegens_type, codegens_expr, defgens) - in { codegens_class = codegens_class, codegens_type = codegens_type, + val (codegens_sort, codegens_type, codegens_expr, defgens) = + f (codegens_sort, codegens_type, codegens_expr, defgens) + in { codegens_sort = codegens_sort, codegens_type = codegens_type, codegens_expr = codegens_expr, defgens = defgens } end; fun merge_gens - ({ codegens_class = codegens_class1, codegens_type = codegens_type1, + ({ codegens_sort = codegens_sort1, codegens_type = codegens_type1, codegens_expr = codegens_expr1, defgens = defgens1 }, - { codegens_class = codegens_class2, codegens_type = codegens_type2, + { codegens_sort = codegens_sort2, codegens_type = codegens_type2, codegens_expr = codegens_expr2, defgens = defgens2 }) = - { codegens_class = AList.merge (op =) (eq_snd (op =)) (codegens_class1, codegens_class2), + { codegens_sort = AList.merge (op =) (eq_snd (op =)) (codegens_sort1, codegens_sort2), codegens_type = AList.merge (op =) (eq_snd (op =)) (codegens_type1, codegens_type2), codegens_expr = AList.merge (op =) (eq_snd (op =)) (codegens_expr1, codegens_expr2), defgens = AList.merge (op =) (eq_snd (op =)) (defgens1, defgens2) }; @@ -237,13 +240,13 @@ }; val empty = { modl = empty_module, - gens = { codegens_class = [], codegens_type = [], codegens_expr = [], defgens = [] } : gens, + gens = { codegens_sort = [], codegens_type = [], codegens_expr = [], defgens = [] } : gens, lookups = { lookups_tyco = Symtab.empty, lookups_const = Symtab.empty } : lookups, logic_data = { is_datatype = NONE, alias = (Symtab.empty, Symtab.empty) } : logic_data, serialize_data = Symtab.empty |> Symtab.update ("ml", - { serializer = serializer_ml, + { serializer = serializer_ml : CodegenSerializer.serializer, primitives = CodegenSerializer.empty_prims |> CodegenSerializer.add_prim ("fst", ("fun fst (x, _) = x;", [])) @@ -251,7 +254,7 @@ |> CodegenSerializer.add_prim ("wfrec", ("fun wfrec f x = f (wfrec f) x;", [])), syntax_tyco = Symtab.empty, syntax_const = Symtab.empty }) |> Symtab.update ("haskell", - { serializer = serializer_hs, primitives = CodegenSerializer.empty_prims, + { serializer = serializer_hs : CodegenSerializer.serializer, primitives = CodegenSerializer.empty_prims, syntax_tyco = Symtab.empty, syntax_const = Symtab.empty }) } : T; val copy = I; @@ -282,13 +285,13 @@ val print_codegen_modl = writeln o Pretty.output o pretty_module o #modl o CodegenData.get; -fun add_codegen_class (name, cg) = +fun add_codegen_sort (name, cg) = map_codegen_data (fn (modl, gens, lookups, serialize_data, logic_data) => (modl, gens |> map_gens - (fn (codegens_class, codegens_type, codegens_expr, defgens) => - (codegens_class + (fn (codegens_sort, codegens_type, codegens_expr, defgens) => + (codegens_sort |> Output.update_warn (op =) ("overwriting existing class code generator " ^ name) (name, (cg, stamp ())), codegens_type, codegens_expr, defgens)), lookups, serialize_data, logic_data)); @@ -297,8 +300,8 @@ (fn (modl, gens, lookups, serialize_data, logic_data) => (modl, gens |> map_gens - (fn (codegens_class, codegens_type, codegens_expr, defgens) => - (codegens_class, + (fn (codegens_sort, codegens_type, codegens_expr, defgens) => + (codegens_sort, codegens_type |> Output.update_warn (op =) ("overwriting existing type code generator " ^ name) (name, (cg, stamp ())), codegens_expr, defgens)), lookups, serialize_data, logic_data)); @@ -308,8 +311,8 @@ (fn (modl, gens, lookups, serialize_data, logic_data) => (modl, gens |> map_gens - (fn (codegens_class, codegens_type, codegens_expr, defgens) => - (codegens_class, codegens_type, + (fn (codegens_sort, codegens_type, codegens_expr, defgens) => + (codegens_sort, codegens_type, codegens_expr |> Output.update_warn (op =) ("overwriting existing expression code generator " ^ name) (name, (cg, stamp ())), defgens)), @@ -320,8 +323,8 @@ (fn (modl, gens, lookups, serialize_data, logic_data) => (modl, gens |> map_gens - (fn (codegens_class, codegens_type, codegens_expr, defgens) => - (codegens_class, codegens_type, codegens_expr, + (fn (codegens_sort, codegens_type, codegens_expr, defgens) => + (codegens_sort, codegens_type, codegens_expr, defgens |> Output.update_warn (op =) ("overwriting existing definition code generator " ^ name) (name, (dg, stamp ())))), lookups, serialize_data, logic_data)); @@ -424,23 +427,19 @@ else name_of_idf thy nsp_type idf else name_of_idf thy nsp_type idf; -fun idf_of_cname thy ((overl, _), _, (_, _, clsmems)) (name, ty) = +fun idf_of_cname thy ((overl, _), _, _) (name, ty) = case Symtab.lookup overl name - of NONE => - (case Symtab.lookup clsmems name - of NONE => idf_of_name thy nsp_const name - | SOME (_, (idf, ty')) => - if Type.raw_instance (ty', ty) - then idf - else idf_of_name thy nsp_const name) - | SOME tab => (the o AList.lookup (Sign.typ_instance thy) tab) ty; + of NONE => idf_of_name thy nsp_const name + | SOME tab => (the o AList.lookup (Sign.typ_instance thy) tab) ty 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; @@ -457,28 +456,28 @@ (* code generator instantiation, part 2 *) -fun invoke_cg_class thy defs class trns = +fun invoke_cg_sort thy defs sort trns = gen_invoke - ((map (apsnd (fn (cg, _) => cg thy defs)) o #codegens_class o #gens o CodegenData.get) thy) - class class trns; + ((map (apsnd (fn (cg, _) => cg thy defs)) o #codegens_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 = gen_invoke ((map (apsnd (fn (cg, _) => cg thy defs)) o #codegens_type o #gens o CodegenData.get) thy) - (Sign.string_of_typ thy ty) ty trns; + ("generating type " ^ (quote o Sign.string_of_typ thy) ty) ty trns; fun invoke_cg_expr thy defs t trns = gen_invoke ((map (apsnd (fn (cg, _) => cg thy defs)) o #codegens_expr o #gens o CodegenData.get) thy) - (Sign.string_of_term thy t) t trns; + ("generating expression " ^ (quote o Sign.string_of_term thy) t) t trns; 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 defs cls_or_inst trns = - if cls_or_inst = "ClassSimple.Eq_proto" then error ("Krach!") - else trns - |> gen_ensure_def (get_defgens thy defs) ("class/instance " ^ quote cls_or_inst) cls_or_inst + trns + |> debug 4 (fn _ => "generating class or instance " ^ quote cls_or_inst) + |> gen_ensure_def (get_defgens thy defs) ("generating class/instance " ^ quote cls_or_inst) cls_or_inst |> pair cls_or_inst; fun ensure_def_tyco thy defs tyco trns = @@ -486,7 +485,8 @@ then case Option.mapPartial (Symtab.lookup (get_lookups_tyco thy)) (tname_of_idf thy tyco) of NONE => trns - |> gen_ensure_def (get_defgens thy defs) ("type constructor " ^ quote tyco) tyco + |> debug 4 (fn _ => "generating type constructor " ^ quote tyco) + |> gen_ensure_def (get_defgens thy defs) ("generating type constructor " ^ quote tyco) tyco |> pair tyco | SOME tyco => trns @@ -498,8 +498,9 @@ then case Option.mapPartial (find_lookup_expr thy) (cname_of_idf thy defs f) of NONE => trns - |> invoke_cg_type thy defs (Sign.the_const_constraint thy (cname_of_idf thy defs f |> the |> fst)) - ||> gen_ensure_def (get_defgens thy defs) ("constant " ^ quote f) f + |> debug 4 (fn _ => "generating constant " ^ quote f) + |> invoke_cg_type thy defs (cname_of_idf thy defs f |> the |> snd) + ||> gen_ensure_def (get_defgens thy defs) ("generating constant " ^ quote f) f |-> (fn ty' => pair f) | SOME (IConst (f, ty)) => trns @@ -511,7 +512,7 @@ val sortctxt = ClassPackage.extract_sortctxt thy ty; fun mk_sortvar (v, sort) trns = trns - |> fold_map (invoke_cg_class thy defs) sort + |> invoke_cg_sort thy defs sort |-> (fn sort => pair (unprefix "'" v, sort)) fun mk_eq (args, rhs) trns = trns @@ -528,10 +529,12 @@ fun mk_app thy defs f ty_use args 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 = trns - |> invoke_cg_class thy defs ((idf_of_name thy nsp_class o fst) i) + |> ensure_def_class thy defs ((idf_of_name thy nsp_class o fst) i) ||>> ensure_def_class thy defs (idf_of_inst thy defs i) ||>> (fold_map o fold_map) mk_lookup ls |-> (fn ((cls, i), ls) => pair (ClassPackage.Instance ((cls, i), ls))) @@ -539,14 +542,20 @@ trns |> fold_map (ensure_def_class thy defs) (map (idf_of_name thy nsp_class) clss) |-> (fn clss => pair (ClassPackage.Lookup (clss, (name_of_tvar (TFree (v, [])), 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_use) |> ensure_def_const thy defs (idf_of_cname thy defs (f, ty_use)) + |> debug 10 (fn _ => "making application (5)") ||>> fold_map (invoke_cg_expr thy defs) args + |> debug 10 (fn _ => "making application (6)") ||>> (fold_map o fold_map) mk_lookup (ClassPackage.extract_sortlookup thy (ty_def, ty_use)) + |> debug 10 (fn _ => "making application (7)") ||>> invoke_cg_type thy defs ty_use + |> debug 10 (fn _ => "making application (8)") |-> (fn (((f, args), lookup), ty_use) => pair (mk_apps (mk_itapp (IConst (f, ty_use)) lookup, args))) end; @@ -563,18 +572,19 @@ (* code generators *) -fun codegen_class_default thy defs cls trns = +fun codegen_sort_default thy defs sort trns = trns - |> ensure_def_class thy defs cls - |-> (fn cls => succeed cls) + |> fold_map (ensure_def_class thy defs) + (sort |> filter (ClassPackage.is_class thy) |> map (idf_of_name thy nsp_class)) + |-> (fn sort => succeed sort) fun codegen_type_default thy defs (v as TVar (_, sort)) trns = trns - |> fold_map (invoke_cg_class thy defs) (sort |> filter (ClassPackage.is_class thy) |> map (idf_of_name thy nsp_class)) + |> invoke_cg_sort thy defs sort |-> (fn sort => succeed (IVarT (name_of_tvar v, sort))) | codegen_type_default thy defs (v as TFree (_, sort)) trns = trns - |> fold_map (invoke_cg_class thy defs) (sort |> filter (ClassPackage.is_class thy) |> map (idf_of_name thy nsp_class)) + |> invoke_cg_sort thy defs sort |-> (fn sort => succeed (IVarT (name_of_tvar v, sort))) | codegen_type_default thy defs (Type ("fun", [t1, t2])) trns = trns @@ -651,21 +661,23 @@ (* definition generators *) -fun defgen_fallback_tyco thy defs tyco trns = +fun defgen_tyco_fallback thy defs 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 trns + |> debug 5 (fn _ => "trying defgen tyco fallback for " ^ quote tyco) |> succeed (Nop, []) else trns |> fail ("no code generation fallback for " ^ quote tyco) -fun defgen_fallback_const thy defs f trns = +fun defgen_const_fallback thy defs f trns = if Symtab.fold (fn (_, { syntax_const, ... }) => fn b => b orelse Symtab.defined syntax_const f) ((#serialize_data o CodegenData.get) thy) false then trns + |> debug 5 (fn _ => "trying defgen const fallback for " ^ quote f) |> succeed (Nop, []) else trns @@ -675,6 +687,7 @@ case Symtab.lookup defs' f of SOME (args, rhs, ty) => trns + |> debug 5 (fn _ => "trying defgen def for " ^ quote f) |> mk_fun thy defs [(args, rhs)] ty |-> (fn def => succeed (def, [])) | _ => trns |> fail ("no definition found for " ^ quote f); @@ -683,12 +696,12 @@ case name_of_idf thy nsp_class cls of SOME cls => trns - |> debug 5 (fn _ => "generating class decl " ^ quote cls) + |> 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)) |-> (fn supcls => succeed (Class (supcls, [], []), map (idf_of_name thy nsp_mem) (ClassPackage.the_consts thy cls) - @ map (curry (idf_of_inst thy defs) cls) ((map snd o ClassPackage.the_tycos thy) cls))) + @ map (curry (idf_of_inst thy defs) cls) ((map fst o ClassPackage.the_tycos thy) cls))) | _ => trns |> fail ("no class definition found for " ^ quote cls); @@ -701,6 +714,7 @@ val (tvar, ty) = ClassPackage.get_const_sign thy clsmem; in trns + |> debug 5 (fn _ => "trying defgen class member for " ^ quote f) |> invoke_cg_type thy defs ty |-> (fn ty => succeed (Classmember (cls, name_of_tvar (TFree (tvar, [])), ty), [])) end @@ -719,6 +733,7 @@ (ClassPackage.get_inst_consts_sign thy (tyco, cls)); in trns + |> debug 5 (fn _ => "trying defgen class instance for (" ^ quote cls ^ ", " ^ quote tyco ^ ")") |> ensure_def_class thy defs (idf_of_name thy nsp_class cls) ||>> ensure_def_tyco thy defs (idf_of_tname thy tyco) ||>> (fold_map o fold_map) (ensure_def_class thy defs) arity @@ -789,7 +804,6 @@ | codegen_number_of dest_binum mk_int_to_nat thy defs (Const ("Numeral.number_of", Type ("fun", [_, Type ("nat", [])])) $ bin) trns = trns - |> debug 8 (fn _ => "generating nat for " ^ Sign.string_of_term thy bin) |> invoke_cg_expr thy defs (mk_int_to_nat bin) |-> (fn expr => succeed expr) | codegen_number_of dest_binum mk_int_to_nat thy defs t trns = @@ -802,6 +816,7 @@ (case get_datatype thy tyco of SOME (vs, cnames) => trns + |> debug 5 (fn _ => "trying defgen datatype for " ^ quote dtname) |> succeed (Datatype (map (rpair [] o unprefix "'") vs, [], []), cnames |> map (idf_of_name thy nsp_const) @@ -830,6 +845,7 @@ (case get_datacons thy (c, dtname) of SOME tyargs => trns + |> debug 5 (fn _ => "trying defgen datatype constructor for " ^ quote c) |> ensure_def_tyco thy defs (idf_of_tname thy dtname) ||>> fold_map (invoke_cg_type thy defs) tyargs |-> (fn (dtname, tys) => succeed (Datatypecons (dtname, tys), [])) @@ -853,6 +869,7 @@ case eqs of (_::_) => trns + |> debug 5 (fn _ => "trying defgen recfun for " ^ quote f) |> mk_fun thy defs eqs ty |-> (fn def => succeed (def, [])) | _ => @@ -901,7 +918,6 @@ val overl_lookups = map (fn (ty, (_, (args, rhs))) => (ty, mk_idf (name, ty), args, rhs)) ds; in - (*!!!*) ((overl |> Symtab.update_new (name, 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), @@ -910,8 +926,27 @@ fun mk_instname thyname (cls, tyco) = idf_of_name thy nsp_inst (NameSpace.append thyname (NameSpace.base cls ^ "_" ^ NameSpace.base tyco)) - fun add_clsmems classtab (overl, defs, (clstab, clstab_rev, clsmems)) = - (overl, defs, + 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 @@ -925,7 +960,7 @@ clsmems |> Symtab.fold (fn (class, (clsmems, _)) => fold - (fn clsmem => Symtab.update (idf_of_name thy nsp_mem clsmem, (class, (clsmem, Sign.the_const_constraint thy clsmem)))) clsmems) + (fn clsmem => Symtab.update (clsmem, class)) clsmems) classtab)) in ((Symtab.empty, Symtab.empty), Symtab.empty, (Insttab.empty, Symtab.empty, Symtab.empty)) @@ -933,9 +968,8 @@ |> add_clsmems (ClassPackage.get_classtab thy) end; -fun expand_module gen thy = +fun expand_module defs gen thy = let - val defs = mk_deftab thy; fun put_module modl = map_codegen_data (fn (_, gens, lookups, serialize_data, logic_data) => (modl, gens, lookups, serialize_data, logic_data)); @@ -949,7 +983,7 @@ (* syntax *) -fun gen_add_syntax_tyco prep_tyco prep_mfx prep_primname serializer ((raw_tyco, raw_mfx), primdef) thy = +fun gen_add_syntax_tyco prep_tyco prep_mfx prep_primname serial_name ((raw_tyco, raw_mfx), primdef) thy = let val tyco = prep_tyco thy raw_tyco; val _ = if member (op =) prims tyco @@ -964,7 +998,7 @@ |-> (fn mfx => map_codegen_data (fn (modl, gens, lookups, serialize_data, logic_data) => (modl, gens, lookups, - serialize_data |> Symtab.map_entry serializer + serialize_data |> Symtab.map_entry serial_name (map_serialize_data (fn (primitives, syntax_tyco, syntax_const) => (primitives |> add_primdef primdef, @@ -993,7 +1027,7 @@ (Codegen.quotes_of proto_mfx); in thy - |> expand_module generate + |> expand_module (mk_deftab thy) generate |-> (fn tys => pair (Codegen.replace_quotes tys proto_mfx)) end; in @@ -1001,7 +1035,7 @@ prep_mfx mk_name end; -fun gen_add_syntax_const prep_const prep_mfx prep_primname serializer ((raw_f, raw_mfx), primdef) thy = +fun gen_add_syntax_const prep_const prep_mfx prep_primname serial_name ((raw_f, raw_mfx), primdef) thy = let val f = prep_const thy raw_f; val _ = if member (op =) prims f @@ -1016,7 +1050,7 @@ |-> (fn mfx => map_codegen_data (fn (modl, gens, lookups, serialize_data, logic_data) => (modl, gens, lookups, - serialize_data |> Symtab.map_entry serializer + serialize_data |> Symtab.map_entry serial_name (map_serialize_data (fn (primitives, syntax_tyco, syntax_const) => (primitives |> add_primdef primdef, @@ -1054,7 +1088,7 @@ (Codegen.quotes_of proto_mfx); in thy - |> expand_module generate + |> expand_module (mk_deftab thy) generate |-> (fn es => pair (Codegen.replace_quotes es proto_mfx)) end; in @@ -1064,15 +1098,29 @@ (* code generation *) -fun generate_code consts thy = +fun get_serializer thy serial_name = + (#serializer o (fn data => (the oo Symtab.lookup) data serial_name) + o #serialize_data o CodegenData.get) thy; + +fun mk_const thy f = let - fun generate thy defs = fold_map (ensure_def_const thy defs) consts + val f' = Sign.intern_const thy f; + in (f', Sign.the_const_constraint thy f') end; + +fun gen_generate_code consts thy = + let + val defs = mk_deftab thy; + val consts' = map (idf_of_cname thy defs) consts; + fun generate thy defs = fold_map (ensure_def_const thy defs) consts' in thy - |> expand_module generate - |-> (fn _ => I) + |> expand_module defs generate + |-> (fn _ => pair consts') end; +fun generate_code consts thy = + gen_generate_code (map (mk_const thy) consts) thy; + fun serialize_code serial_name filename consts thy = let fun mk_sfun tab name args f = @@ -1083,19 +1131,22 @@ |> CodegenData.get |> #serialize_data |> (fn data => (the oo Symtab.lookup) data serial_name) - val serializer = #serializer serialize_data + val serializer' = (get_serializer thy serial_name) ((mk_sfun o #syntax_tyco) serialize_data) ((mk_sfun o #syntax_const) serialize_data) - (#primitives serialize_data) + (#primitives serialize_data); + val _ = serializer' : string list option -> module -> Pretty.T; val compile_it = serial_name = "ml" andalso filename = "-"; fun use_code code = if compile_it then use_text Context.ml_output false code else File.write (Path.unpack filename) (code ^ "\n"); + val consts' = Option.map (map (mk_const thy)) consts; in thy - |> (if is_some consts then generate_code (the consts) else I) - |> `(serializer consts o #modl o CodegenData.get) + |> (if is_some consts then gen_generate_code (the consts') else pair []) + |-> (fn [] => `(serializer' NONE o #modl o CodegenData.get) + | consts => `(serializer' (SOME consts) o #modl o CodegenData.get)) |-> (fn code => ((use_code o Pretty.output) code; I)) end; @@ -1116,15 +1167,15 @@ OuterSyntax.command generateK "generate executable code for constants" K.thy_decl ( Scan.repeat1 P.name >> (fn consts => - Toplevel.theory (generate_code consts)) + Toplevel.theory (generate_code consts #> snd)) ); val serializeP = - OuterSyntax.command generateK "serialize executable code for constants" K.thy_decl ( + OuterSyntax.command serializeK "serialize executable code for constants" K.thy_decl ( P.name -- P.name -- Scan.option ( - P.$$$ serializeK + P.$$$ extractingK |-- Scan.repeat1 P.name ) >> (fn ((serial_name, filename), consts) => @@ -1149,10 +1200,10 @@ -- (P.string -- Scan.optional (P.$$$ dependingK |-- P.list1 P.string) []) ) ) - >> (fn (serializer, xs) => + >> (fn (serial_name, xs) => (Toplevel.theory oo fold) (fn ((tyco, raw_mfx), raw_def) => - add_syntax_tyco serializer ((tyco, raw_mfx), raw_def)) xs) + add_syntax_tyco serial_name ((tyco, raw_mfx), raw_def)) xs) ); val syntax_constP = @@ -1166,10 +1217,10 @@ -- (P.string -- Scan.optional (P.$$$ dependingK |-- P.list1 P.string) []) ) ) - >> (fn (serializer, xs) => + >> (fn (serial_name, xs) => (Toplevel.theory oo fold) (fn ((f, raw_mfx), raw_def) => - add_syntax_const serializer ((f, raw_mfx), raw_def)) xs) + add_syntax_const serial_name ((f, raw_mfx), raw_def)) xs) ); val _ = OuterSyntax.add_parsers [generateP, serializeP, aliasP, syntax_tycoP, syntax_constP]; @@ -1188,14 +1239,14 @@ val B = TVar (("'b", 0), []); in Context.add_setup [ CodegenData.init, - add_codegen_class ("default", codegen_class_default), + add_codegen_sort ("default", codegen_sort_default), add_codegen_type ("default", codegen_type_default), add_codegen_expr ("default", codegen_expr_default), (* add_codegen_expr ("eq", codegen_eq), *) add_codegen_expr ("neg", codegen_neg), add_defgen ("clsdecl", defgen_clsdecl), - add_defgen ("fallback_tyco", defgen_fallback_tyco), - add_defgen ("fallback_const", defgen_fallback_const), + add_defgen ("tyco_fallback", defgen_tyco_fallback), + add_defgen ("const_fallback", defgen_const_fallback), add_defgen ("defs", defgen_defs), add_defgen ("clsmem", defgen_clsmem), add_defgen ("clsinst", defgen_clsinst), @@ -1208,13 +1259,13 @@ 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 (("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.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), diff -r 4dc1f30af6a1 -r 2eea98bbf650 src/Pure/Tools/codegen_serializer.ML --- a/src/Pure/Tools/codegen_serializer.ML Tue Nov 22 19:37:36 2005 +0100 +++ b/src/Pure/Tools/codegen_serializer.ML Wed Nov 23 17:16:42 2005 +0100 @@ -19,6 +19,7 @@ -> (string list * Pretty.T) option; type serializer = CodegenThingol.itype pretty_syntax -> CodegenThingol.iexpr pretty_syntax -> primitives -> string list option -> CodegenThingol.module -> Pretty.T; + type parm_serializer = OuterParse.token list -> serializer * OuterParse.token list; val ml_from_thingol: string list list -> string -> serializer; end; @@ -67,6 +68,7 @@ -> (string list * Pretty.T) option; type serializer = CodegenThingol.itype pretty_syntax -> CodegenThingol.iexpr pretty_syntax -> primitives -> string list option -> CodegenThingol.module -> Pretty.T; +type parm_serializer = OuterParse.token list -> serializer * OuterParse.token list; datatype lrx = L | R | X; @@ -373,18 +375,12 @@ let val args = map (ml_from_iexpr BR) es val brackify' = K (eval_br br BR) ? (single #> Pretty.enclose "(" ")") - fun prepend_abs v body = - Pretty.block [Pretty.str ("fn " ^ v ^ " =>"), Pretty.brk 1, body] in case sconst f args (ml_from_iexpr BR) of NONE => brackify (eval_br br BR) (Pretty.str (resolv f) :: args) - | SOME ([], p) => + | SOME (_, p) => brackify' p - | SOME (vars, p) => - p - |> fold_rev prepend_abs vars - |> brackify' end; fun ml_from_funs (ds as d::ds_tl) = let @@ -432,7 +428,6 @@ end; fun ml_from_datatypes ds = let - val _ = debug 9 (fn _ => map (pretty_def o snd) ds |> Pretty.chunks |> Pretty.output) (); fun check_typ_dup ty xs = if AList.defined (op =) xs ty then error ("double datatype definition: " ^ quote ty) @@ -554,6 +549,8 @@ |> (if is_some select then (partof o the) select else I) |> debug 3 (fn _ => "eta-expanding...") |> eta_expand eta_expander + |> debug 3 (fn _ => "eta-expanding polydefs...") + |> eta_expand_poly |> debug 5 (Pretty.output o pretty_module) |> debug 3 (fn _ => "tupelizing datatypes...") |> tupelize_cons @@ -563,6 +560,12 @@ |> serialize (ml_from_defs styco sconst) ml_from_module (ml_validator prims) nspgrp name_root end; +fun ml_from_thingol' nspgrp name_root = + Scan.optional ( + OuterParse.$$$ "(" |-- OuterParse.list1 OuterParse.text --| OuterParse.$$$ ")" + ) [] + >> (fn _ => ml_from_thingol nspgrp name_root); + (* ML infix precedence 7 / * div mod 6 + - ^ diff -r 4dc1f30af6a1 -r 2eea98bbf650 src/Pure/Tools/codegen_thingol.ML --- a/src/Pure/Tools/codegen_thingol.ML Tue Nov 22 19:37:36 2005 +0100 +++ b/src/Pure/Tools/codegen_thingol.ML Wed Nov 23 17:16:42 2005 +0100 @@ -112,6 +112,7 @@ val debug_level : int ref; val debug : int -> ('a -> string) -> 'a -> 'a; + val soft_exc: bool ref; val serialize: ((string -> string) -> (string * def) list -> Pretty.T) @@ -138,6 +139,7 @@ val debug_level = ref 0; fun debug d f x = (if d <= !debug_level then Output.debug (f x) else (); x); +val soft_exc = ref true; fun foldl' f (l, []) = the l | foldl' f (_, (r::rs)) = @@ -423,11 +425,11 @@ datatype node = Def of def | Module of node Graph.T; type module = node Graph.T; type transact = Graph.key list * module; -datatype 'dst transact_res = Succeed of 'dst | Fail of string; +datatype 'dst transact_res = Succeed of 'dst | Fail of string list * exn option; type 'dst transact_fin = 'dst transact_res * transact; type ('src, 'dst) gen_codegen = 'src -> transact -> 'dst transact_fin; type gen_defgen = string -> transact -> (def * string list) transact_fin; -exception FAIL of string; +exception FAIL of string list * exn option; val eq_def = (op =); @@ -467,11 +469,29 @@ Pretty.gen_list " ->" "" "" (map pretty_itype tys @ [Pretty.str dtname]) ] | pretty_def (Class (supcls, mems, insts)) = - Pretty.str "Class ..." + Pretty.block [ + Pretty.str "class extending", + Pretty.gen_list "," "[" "]" (map Pretty.str supcls), + Pretty.str "with ", + Pretty.gen_list "," "[" "]" (map Pretty.str mems), + Pretty.str "instances ", + Pretty.gen_list "," "[" "]" (map Pretty.str insts) + ] | pretty_def (Classmember (cls, v, ty)) = - Pretty.str "Classmember ..." - | pretty_def (Classinst (cls, insts, mems)) = - Pretty.str "Classinst ..." + Pretty.block [ + Pretty.str "class member belonging to ", + Pretty.str cls + ] + | pretty_def (Classinst (cls, (tyco, arity), mems)) = + Pretty.block [ + Pretty.str "class instance (", + Pretty.str cls, + Pretty.str ", (", + Pretty.str tyco, + Pretty.str ", ", + Pretty.gen_list "," "[" "]" (map (Pretty.gen_list "," "{" "}" o map Pretty.str) arity), + Pretty.str "))" + ]; fun pretty_module modl = let @@ -627,14 +647,19 @@ end; fun add_check_transform (name, (Datatypecons (dtname, _))) = + (debug 7 (fn _ => "transformation for datatype constructor " ^ quote name + ^ " of datatype " ^ quote dtname) (); ([([dtname], fn [Datatype (_, _, [])] => NONE | _ => "attempted to add constructor to already instantiating datatype" |> SOME)], [(dtname, fn Datatype (vs, cs, clss) => Datatype (vs, name::cs, clss) | def => "attempted to add datatype constructor to non-datatype: " ^ (Pretty.output o pretty_def) def |> error)]) + ) | add_check_transform (name, Classmember (clsname, v, ty)) = let + val _ = debug 7 (fn _ => "transformation for class member " ^ quote name + ^ " of class " ^ quote clsname) (); fun check_var (IType (tyco, tys)) s = fold check_var tys s | check_var (IFun (ty1, ty2)) s = @@ -658,17 +683,26 @@ end | add_check_transform (name, Classinst (clsname, (tyco, arity), memdefs)) = let + val _ = debug 7 (fn _ => "transformation for class instance " ^ quote tyco + ^ " of class " ^ quote clsname) (); fun check [Classmember (_, v, mtyp_c), Fun (_, (_, mtyp_i))] = - let - val mtyp_i' = instant_itype (v, tyco `%% - map2 IVarT ((invent_var_t_names [mtyp_c] (length arity) [] "a"), arity)) mtyp_c; - in if eq_itype (mtyp_i', mtyp_i) (*! PERHAPS TOO STRICT !*) - then NONE - else "wrong type signature for class member: " - ^ (Pretty.output o pretty_itype) mtyp_i' ^ " expected," - ^ (Pretty.output o pretty_itype) mtyp_i ^ " given" |> SOME end + let + val _ = writeln "CHECK RUNNING (1)"; + val mtyp_i' = instant_itype (v, tyco `%% + map2 IVarT ((invent_var_t_names [mtyp_c] (length arity) [] "a"), arity)) mtyp_c; + val _ = writeln "CHECK RUNNING (2)"; + in let val XXX = ( + if eq_itype (mtyp_i', mtyp_i) (*! PERHAPS TOO STRICT !*) + then NONE + else "wrong type signature for class member: " + ^ (Pretty.output o pretty_itype) mtyp_i' ^ " expected," + ^ (Pretty.output o pretty_itype) mtyp_i ^ " given" |> SOME + ) in (writeln "CHECK RUNNING (3)"; XXX) end end + | check defs = + "non-well-formed definitions encountered for classmembers: " + ^ (commas o map (quote o Pretty.output o pretty_def)) defs |> SOME in - (map (fn (memname, memprim) => ((writeln memname; writeln memprim; [memname, memprim]), check)) memdefs, + (map (fn (memname, memprim) => ([memname, memprim], check)) memdefs, [(clsname, fn Class (supcs, mems, insts) => Class (supcs, mems, name::insts) | def => "attempted to add class instance to non-class" @@ -681,28 +715,45 @@ end | add_check_transform _ = ([], []); -fun succeed some = (pair o Succeed) some; -fun fail msg = (pair o Fail) msg; +fun succeed some = pair (Succeed some); +fun fail msg = pair (Fail ([msg], NONE)); -fun check_fail msg' (Succeed dst, trns) = (dst, trns) - | check_fail msg' (Fail errmsg, _) = (tracing ("ROLLBACK CHECK: " ^ errmsg ^ "\n" ^ msg'); raise FAIL errmsg); - -fun handle_fail msg f modl = - f modl handle FAIL msg' => ([], modl) |> fail (msg ^ "\n" ^ msg'); +fun check_fail _ (Succeed dst, trns) = (dst, trns) + | check_fail msg (Fail (msgs, e), _) = raise FAIL (msg::msgs, e); -fun select_generator print_msg src [] trns = - fail ("no code generator available") trns - | select_generator print_msg src [(gname, cgen)] trns = - (print_msg gname; cgen src trns) - | select_generator print_msg src ((gname, cgen)::cgens) trns = - case cgen src trns - of result as (Succeed _, _) => - (print_msg gname; result) - | _ => select_generator print_msg src cgens trns +fun select_generator _ _ [] modl = + ([], modl) |> fail ("no code generator available") + | select_generator mk_msg src gens modl = + let + fun handle_fail msgs f = + let + fun handl trns = + trns |> f + handle FAIL exc => (Fail exc, ([], modl)) + in + if ! soft_exc + then + ([], modl) |> handl + handle e => (Fail (msgs, SOME e), ([], modl)) + else + ([], modl) |> handl + end; + fun select msgs [(gname, gen)] = + handle_fail (msgs @ [mk_msg gname]) (gen src) + fun select msgs ((gname, gen)::gens) = + let + val msgs' = msgs @ [mk_msg gname] + in case handle_fail msgs' (gen src) + of (Fail (_, NONE), _) => + select msgs' gens + | result => + result + end; + in select [] gens end; fun gen_invoke codegens msg src (deps, modl) = - ([], modl) - |> select_generator (fn gname => "choosing code generator " ^ gname ^ " for source " ^ quote msg) + modl + |> select_generator (fn gname => "trying code generator " ^ gname ^ " for source " ^ quote msg) src codegens |> check_fail msg ||> (fn (deps', modl') => (append deps' deps, modl')); @@ -713,41 +764,78 @@ let val (checks, trans) = add_check_transform (name, def); fun check (check_defs, checker) modl = - case checker (check_defs |> filter NameSpace.is_qualified |> map (get_def modl)) - of NONE => modl - | SOME e => raise FAIL e; + let + val _ = writeln ("CHECK (1): " ^ commas check_defs) + fun get_def' s = + if NameSpace.is_qualified s + then get_def modl s + else Nop + val defs = + check_defs + |> map get_def'; + val _ = writeln ("CHECK (2): " ^ commas check_defs) + in + let val XXX = case checker defs + of NONE => modl + | SOME e => raise FAIL ([e], NONE) + in (writeln "CHECK (3)"; XXX) end + end; fun transform (name, f) modl = modl - |> K (NameSpace.is_qualified name) ? map_def name f; + |> debug 9 (fn _ => "transforming node " ^ name) + |> (if NameSpace.is_qualified name then map_def name f else I); in modl + |> debug 10 (fn _ => "considering addition of " ^ name + ^ " := " ^ (Pretty.output o pretty_def) def) + |> debug 10 (fn _ => "consistency checks") |> fold check checks + |> debug 10 (fn _ => "dependencies") |> fold (curry add_dep name) deps + |> debug 10 (fn _ => "adding") |> map_def name (fn _ => def) + |> debug 10 (fn _ => "transforming") |> fold transform trans + |> debug 10 (fn _ => "adding done") end; fun ensure_node name modl = + (debug 9 (fn _ => "testing node " ^ quote name) (); if can (get_def modl) name - then ([name], modl) + then + modl + |> debug 9 (fn _ => "asserting node " ^ quote name) + |> pair [name] else - ([], modl |> add_def (name, Nop)) - |> select_generator (fn gname => "choosing code generator " ^ gname ^ " for definition of " ^ quote name) + modl + |> debug 9 (fn _ => "creating node " ^ quote name) + |> add_def (name, Nop) + |> select_generator (fn gname => "trying code generator " ^ gname ^ " for definition of " ^ quote name) name defgens |> check_fail msg |-> (fn (def, names') => add (name, def) #> fold_map ensure_node names') |-> (fn names' => pair (name :: Library.flat names')) + ) in modl |> ensure_node name |-> (fn names => pair (names@deps)) end; -fun start_transact f module = - ([], module) - |> f - |-> (fn x => fn (_, module) => (x, module)); +fun start_transact f modl = + let + fun handle_fail f modl = + ((([], modl) |> f) + handle FAIL (msgs, NONE) => + (error o cat_lines) ("code generation failed, while:" :: msgs)) + handle FAIL (msgs, SOME e) => + ((writeln o cat_lines) ("code generation failed, while:" :: msgs); raise e); + in + modl + |> handle_fail f + |-> (fn x => fn (_, module) => (x, module)) + end; (** primitive language constructs **)