# HG changeset patch # User haftmann # Date 1150279857 -7200 # Node ID a7be206d86552af027cd54f5de27a735455d45ec # Parent d064712bdd1dd40cc8d83c2ba829d2d71593c09a improvements in code generator diff -r d064712bdd1d -r a7be206d8655 src/Pure/Tools/ROOT.ML --- a/src/Pure/Tools/ROOT.ML Tue Jun 13 23:41:59 2006 +0200 +++ b/src/Pure/Tools/ROOT.ML Wed Jun 14 12:10:57 2006 +0200 @@ -13,6 +13,7 @@ (*code generator theorems*) use "codegen_theorems.ML"; +use "codegen_simtype.ML"; (*code generator, 2nd generation*) use "codegen_thingol.ML"; diff -r d064712bdd1d -r a7be206d8655 src/Pure/Tools/codegen_package.ML --- a/src/Pure/Tools/codegen_package.ML Tue Jun 13 23:41:59 2006 +0200 +++ b/src/Pure/Tools/codegen_package.ML Wed Jun 14 12:10:57 2006 +0200 @@ -8,13 +8,15 @@ signature CODEGEN_PACKAGE = sig - type auxtab; - type appgen = theory -> auxtab - -> (string * typ) * term list -> CodegenThingol.transact - -> CodegenThingol.iexpr * CodegenThingol.transact; + val codegen_term: term -> theory -> CodegenThingol.iexpr * theory; + val is_dtcon: string -> bool; + val consts_of_idfs: theory -> string list -> (string * typ) list; + val idfs_of_consts: theory -> (string * typ) list -> string list; + val get_root_module: theory -> CodegenThingol.module; + val get_ml_fun_datatype: theory -> (string -> string) + -> ((string * CodegenThingol.funn) list -> Pretty.T) + * ((string * CodegenThingol.datatyp) list -> Pretty.T); - val add_appconst: xstring * ((int * int) * appgen) -> theory -> theory; - val add_appconst_i: string * ((int * int) * appgen) -> theory -> theory; val add_pretty_list: string -> string -> string * (int * string) -> theory -> theory; val add_alias: string * string -> theory -> theory; @@ -24,15 +26,9 @@ -> theory -> theory; val set_int_tyco: string -> theory -> theory; - val codegen_term: term -> theory -> CodegenThingol.iexpr * theory; - val is_dtcon: string -> bool; - val consts_of_idfs: theory -> string list -> (string * typ) list; - val idfs_of_consts: theory -> (string * typ) list -> string list; - val get_root_module: theory -> CodegenThingol.module; - val get_ml_fun_datatype: theory -> (string -> string) - -> ((string * CodegenThingol.funn) list -> Pretty.T) - * ((string * CodegenThingol.datatyp) list -> Pretty.T); - + type appgen; + val add_appconst: xstring * ((int * int) * appgen) -> theory -> theory; + val add_appconst_i: string * ((int * int) * appgen) -> theory -> theory; val appgen_default: appgen; val appgen_let: (int -> term -> term list * term) -> appgen; @@ -51,7 +47,8 @@ structure ConstNameMangler: NAME_MANGLER; structure DatatypeconsNameMangler: NAME_MANGLER; structure CodegenData: THEORY_DATA; - val mk_tabs: theory -> string option -> auxtab; + type auxtab; + val mk_tabs: theory -> string list option -> auxtab; val alias_get: theory -> string -> string; val idf_of_name: theory -> string -> string -> string; val idf_of_const: theory -> auxtab -> string * typ -> string; @@ -200,7 +197,7 @@ fun re_mangle _ dst = error ("no such datatype constructor: " ^ quote dst); ); -type auxtab = (string option * deftab) +type auxtab = (bool * string list option * deftab) * (InstNameMangler.T * (typ list Symtab.table * ConstNameMangler.T) * DatatypeconsNameMangler.T); type eqextr = theory -> auxtab @@ -398,7 +395,7 @@ in SOME (c, dtco) end | NONE => NONE; -fun idf_of_const thy (tabs as (deftab, (_, (overltab1, overltab2), _))) +fun idf_of_const thy (tabs as (_, (_, (overltab1, overltab2), _))) (c, ty) = let fun get_overloaded (c, ty) = @@ -422,6 +419,24 @@ | NONE => idf_of_name thy nsp_const c end; +fun idf_of_const' thy (tabs as (_, (_, (overltab1, overltab2), _))) + (c, ty) = + let + fun get_overloaded (c, ty) = + (case Symtab.lookup overltab1 c + of SOME tys => + (case find_first (curry (Sign.typ_instance thy) ty) tys + of SOME ty' => ConstNameMangler.get thy overltab2 + (c, ty') |> SOME + | _ => NONE) + | _ => NONE) + in case get_overloaded (c, ty) + of SOME idf => idf + | NONE => case ClassPackage.lookup_const_class thy c + of SOME _ => idf_of_name thy nsp_mem c + | NONE => idf_of_name thy nsp_const c + end; + fun recconst_of_idf thy (_, (_, (_, overltab2), _)) idf = case name_of_idf thy nsp_const idf of SOME c => SOME (c, Sign.the_const_type thy c) @@ -508,16 +523,16 @@ (* definition and expression generators *) -fun check_strict thy f x (tabs as ((SOME target, deftab), tabs')) = - thy - |> CodegenData.get - |> #target_data - |> (fn data => (the oo Symtab.lookup) data target) - |> f - |> (fn tab => Symtab.lookup tab x) - |> is_none - | check_strict _ _ _ (tabs as ((NONE, _), _)) = - false; +fun check_strict thy f x ((false, _, _), _) = + false + | check_strict thy f x ((_, SOME targets, _), _) = + exists ( + is_none o (fn tab => Symtab.lookup tab x) o f o the o (Symtab.lookup ((#target_data o CodegenData.get) thy)) + ) targets + | check_strict thy f x ((true, _, _), _) = + true; + +fun no_strict ((_, targets, deftab), tabs') = ((false, targets, deftab), tabs'); fun ensure_def_class thy tabs cls trns = let @@ -610,12 +625,12 @@ case CodegenTheorems.get_funs thy (c, Logic.legacy_varifyT ty) (* FIXME *) of SOME (ty, eq_thms) => let + val msg = cat_lines ("generating code for theorems " :: map string_of_thm eq_thms); val sortctxt = ClassPackage.extract_sortctxt thy ty; fun dest_eqthm eq_thm = let val ((t, args), rhs) = - (apfst strip_comb o Logic.dest_equals - o prop_of) eq_thm; + (apfst strip_comb o Logic.dest_equals o prop_of) eq_thm; in case t of Const (c', _) => if c' = c then (args, rhs) else error ("illegal function equation for " ^ quote c @@ -625,13 +640,14 @@ fun exprgen_eq (args, rhs) trns = trns |> fold_map (exprgen_term thy tabs) args - ||>> exprgen_term thy tabs rhs + ||>> exprgen_term thy tabs rhs; in trns + |> message msg (fn trns => trns |> fold_map (exprgen_eq o dest_eqthm) eq_thms ||>> exprgen_type thy tabs ty ||>> fold_map (exprgen_tyvar_sort thy tabs) sortctxt - |-> (fn ((eqs, ity), sortctxt) => (pair o SOME) ((eqs, (sortctxt, ity)), ty)) + |-> (fn ((eqs, ity), sortctxt) => (pair o SOME) ((eqs, (sortctxt, ity)), ty))) end | NONE => (NONE, trns) and ensure_def_inst thy (tabs as (_, (insttab, _, _))) (cls, tyco) trns = @@ -827,16 +843,19 @@ trns |> appgen_default thy tabs app; -fun appgen_number_of bin_to_int thy tabs ((_, Type (_, [_, ty])), [bin]) trns = - let - val i = bin_to_int thy bin; - (*preprocessor eliminates nat and negative numerals*) - val _ = if i < 0 then error ("negative numeral: " ^ IntInf.toString i) else (); - in - trns - |> exprgen_type thy tabs ty - |-> (fn _ => pair (CodegenThingol.INum (i, ()))) - end; +fun appgen_number_of int_of_bin thy tabs (app as (c as (_, ty), [bin])) trns = + case try (int_of_bin thy) bin + of SOME i => if i < 0 then error ("negative numeral: " ^ IntInf.toString i) + (*preprocessor eliminates nat and negative numerals*) + else + trns + |> pair (CodegenThingol.INum (i, IVar "")) + (*|> exprgen_term thy (no_strict tabs) (Const c) + ||>> exprgen_term thy (no_strict tabs) bin + |-> (fn (e1, e2) => pair (CodegenThingol.INum (i, e1 `$ e2)))*) + | NONE => + trns + |> appgen_default thy tabs app; fun appgen_char char_to_index thy tabs (app as ((_, ty), _)) trns = case (char_to_index o list_comb o apfst Const) app @@ -856,7 +875,7 @@ val idf = idf_of_const thy tabs (c, ty); in trns - |> ensure_def ((K o succeed) Bot) true ("generating wfrec") idf + |> ensure_def ((K o fail) "no extraction of wfrec") false ("generating wfrec") idf |> exprgen_type thy tabs ty' ||>> (fold_map o fold_map) (exprgen_classlookup thy tabs) (ClassPackage.extract_classlookup thy (c, ty)) @@ -906,7 +925,7 @@ (** theory interface **) -fun mk_tabs thy target = +fun mk_tabs thy targets = let fun mk_insttab thy = InstNameMangler.empty @@ -970,7 +989,7 @@ val insttab = mk_insttab thy; val overltabs = mk_overltabs thy; val dtcontab = mk_dtcontab thy; - in ((target, Symtab.empty), (insttab, overltabs, dtcontab)) end; + in ((true, targets, Symtab.empty), (insttab, overltabs, dtcontab)) end; fun get_serializer target = case Symtab.lookup (!serializers) target @@ -981,26 +1000,25 @@ map_codegen_data (fn (modl, gens, target_data, logic_data) => (f modl, gens, target_data, logic_data)); -(*fun delete_defs NONE thy = +fun purge_defs NONE thy = map_module (K CodegenThingol.empty_module) thy - | delete_defs (SOME c) thy = + | purge_defs (SOME cs) thy = let val tabs = mk_tabs thy NONE; + val idfs = map (idf_of_const' thy tabs) cs; + val _ = writeln ("purging " ^ commas idfs); + fun purge idfs modl = + CodegenThingol.purge_module (filter (can (get_def modl)) idfs) modl in - map_module (CodegenThingol.purge_module []) thy + map_module (purge idfs) thy end; -does not make sense: -* primitve definitions have to be kept -* *all* overloaded defintitions for a constant have to be purged -* precondition: improved representation of definitions hidden by customary serializations -*) -fun expand_module target init gen arg thy = +fun expand_module targets init gen arg thy = thy |> CodegenTheorems.notify_dirty |> `(#modl o CodegenData.get) |> (fn (modl, thy) => - (start_transact init (gen thy (mk_tabs thy target) arg) modl, thy)) + (start_transact init (gen thy (mk_tabs thy targets) arg) modl, thy)) |-> (fn (x, modl) => map_module (K modl) #> pair x); fun rename_inconsistent thy = @@ -1009,7 +1027,7 @@ let val thy = theory thyname; fun own_tables get = - (get thy) + 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) @@ -1054,8 +1072,6 @@ (** target languages **) -val ensure_bot = map_module o CodegenThingol.ensure_bot; - (* syntax *) fun read_typ thy = @@ -1110,7 +1126,6 @@ val tyco = prep_tyco thy raw_tyco; in thy - |> ensure_bot tyco |> reader |-> (fn pretty => map_codegen_data (fn (modl, gens, target_data, logic_data) => @@ -1155,7 +1170,6 @@ val c = prep_const thy raw_const; in thy - |> ensure_bot c |> reader |-> (fn pretty => add_pretty_syntax_const c target pretty) end; @@ -1184,17 +1198,23 @@ +(** code basis change notifications **) + +val _ = Context.add_setup (CodegenTheorems.add_notify purge_defs); + + + (** toplevel interface **) local -fun generate_code target (SOME raw_consts) thy = +fun generate_code targets (SOME raw_consts) thy = let val consts = map (read_const thy) raw_consts; - val _ = case target of SOME target => (get_serializer target; ()) | _ => (); + val _ = case targets of SOME targets => (map get_serializer targets; ()) | _ => (); in thy - |> expand_module target NONE (fold_map oo ensure_def_const) consts + |> expand_module targets NONE (fold_map oo ensure_def_const) consts |-> (fn cs => pair (SOME cs)) end | generate_code _ NONE thy = @@ -1210,14 +1230,19 @@ |> CodegenData.get |> #target_data |> (fn data => (the oo Symtab.lookup) data target); - in (seri ( - (Symtab.lookup o #syntax_class) target_data, - (Option.map fst oo Symtab.lookup o #syntax_tyco) target_data, - (Option.map fst oo Symtab.lookup o #syntax_const) target_data - ) cs module : unit; thy) end; + val s_class = #syntax_class target_data + val s_tyco = #syntax_tyco target_data + val s_const = #syntax_const target_data + in + (seri ( + Symtab.lookup s_class, + (Option.map fst oo Symtab.lookup) s_tyco, + (Option.map fst oo Symtab.lookup) s_const + ) ([] (*TODO: add seri_defs here*), cs) module : unit; thy) + end; in thy - |> generate_code (SOME target) raw_consts + |> generate_code (SOME [target]) raw_consts |-> (fn cs => serialize cs) end; @@ -1232,20 +1257,19 @@ in val (generateK, serializeK, - primclassK, primtycoK, primconstK, syntax_classK, syntax_tycoK, syntax_constK, purgeK, aliasK) = ("code_generate", "code_serialize", - "code_primclass", "code_primtyco", "code_primconst", - "code_syntax_class", "code_syntax_tyco", "code_syntax_const", + "code_classapp", "code_typapp", "code_constapp", "code_purge", "code_alias"); val generateP = OuterSyntax.command generateK "generate executable code for constants" K.thy_decl ( - Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") + (Scan.option (P.$$$ "(" |-- P.list1 P.name --| P.$$$ ")") + >> (fn SOME ["-"] => SOME [] | ts => ts)) -- Scan.repeat1 P.term - >> (fn (target, raw_consts) => - Toplevel.theory (generate_code target (SOME raw_consts) #> snd)) + >> (fn (targets, raw_consts) => + Toplevel.theory (generate_code targets (SOME raw_consts) #> snd)) ); val serializeP = @@ -1262,7 +1286,7 @@ ); val syntax_classP = - OuterSyntax.command syntax_tycoK "define code syntax for class" K.thy_decl ( + OuterSyntax.command syntax_classK "define code syntax for class" K.thy_decl ( Scan.repeat1 ( P.xname -- Scan.repeat1 ( @@ -1309,7 +1333,8 @@ >> (Toplevel.theory oo fold) add_alias ); -val _ = OuterSyntax.add_parsers [generateP, serializeP, syntax_tycoP, syntax_constP, +val _ = OuterSyntax.add_parsers [generateP, serializeP, + syntax_classP, syntax_tycoP, syntax_constP, purgeP, aliasP]; end; (* local *) diff -r d064712bdd1d -r a7be206d8655 src/Pure/Tools/codegen_serializer.ML --- a/src/Pure/Tools/codegen_serializer.ML Tue Jun 13 23:41:59 2006 +0200 +++ b/src/Pure/Tools/codegen_serializer.ML Wed Jun 14 12:10:57 2006 +0200 @@ -15,7 +15,7 @@ ((string -> string option) * (string -> CodegenThingol.itype pretty_syntax option) * (string -> CodegenThingol.iexpr pretty_syntax option) - -> string list option + -> string list * string list option -> CodegenThingol.module -> unit) * OuterParse.token list; val parse_syntax: ('b -> int) -> (string -> 'b -> 'a * 'b) -> OuterParse.token list -> @@ -199,13 +199,13 @@ ((string -> string option) * (string -> itype pretty_syntax option) * (string -> iexpr pretty_syntax option) - -> string list option + -> string list * string list option -> CodegenThingol.module -> unit) * OuterParse.token list; fun abstract_serializer (target, nspgrp) name_root (from_defs, from_module, validator, postproc) postprocess (class_syntax, tyco_syntax, const_syntax) - select module = + (drop: string list, select) module = let fun from_module' resolv imps ((name_qual, name), defs) = from_module resolv imps ((name_qual, name), defs) @@ -463,7 +463,8 @@ | ml_from_expr fxy (INum (n, _)) = brackify BR [ (str o IntInf.toString) n, - str ":IntInf.int" + str ":", + str "IntInf.int" ] | ml_from_expr _ (IChar (c, _)) = (str o prefix "#" o quote) @@ -810,11 +811,9 @@ o quote o suffix ".ML" o translate_string (fn "." => "/" | s => s)) "ML" serializer | _ => Scan.fail ()); in - (parse_multi - || parse_internal serializer - || parse_single_file serializer) - >> (fn seri => fn (class_syntax, tyco_syntax, const_syntax) => seri - (class_syntax, tyco_syntax, const_syntax)) + parse_multi + || parse_internal serializer + || parse_single_file serializer end; fun mk_flat_ml_resolver names = @@ -1077,8 +1076,6 @@ in (Scan.optional (OuterParse.name >> (fn "no_typs" => false | s => Scan.fail_with (fn _ => "illegal flag: " ^ quote s) true)) true #-> (fn with_typs => parse_multi_file ((K o K) NONE) "hs" (serializer with_typs))) - >> (fn (seri) => fn (class_syntax, tyco_syntax, const_syntax) => seri - (class_syntax, tyco_syntax, const_syntax)) end; end; (* local *) diff -r d064712bdd1d -r a7be206d8655 src/Pure/Tools/codegen_simtype.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Tools/codegen_simtype.ML Wed Jun 14 12:10:57 2006 +0200 @@ -0,0 +1,96 @@ +(* Title: Pure/Tools/codegen_simtype.ML + ID: $Id$ + Author: Florian Haftmann, TU Muenchen + +Axiomatic extension of code generator: implement ("simulate") types +by other type expressions. Requires user proof but does not use +the proven theorems! +*) + +signature CODEGEN_SIMTYPE = +sig +end; + +structure CodegenSimtype: CODEGEN_SIMTYPE = +struct + +local + +fun gen_simtype prep_term do_proof (raw_repm, raw_absm) (raw_repi, raw_absi) raw_repe thy = + let + val repm = prep_term thy raw_repm; + val absm = prep_term thy raw_absm; + val repi = prep_term thy raw_repi; + val absi = prep_term thy raw_absi; + val (repe, repe_ty) = (dest_Const o prep_term thy) raw_repe; + val repe_ty' = (snd o strip_type) repe_ty; + fun dest_fun (ty as Type (_, [ty1, ty2])) = + if is_funtype ty then (ty1, ty2) + else raise TYPE ("dest_fun", [ty], []) + | dest_fun ty = raise TYPE ("dest_fun", [ty], []); + val PROP = ObjectLogic.ensure_propT thy + val (ty_abs, ty_rep) = (dest_fun o type_of) repm; + val (tyco_abs, ty_parms) = dest_Type ty_abs; + val _ = if exists (fn TFree _ => false | _ => true) ty_parms then raise TYPE ("no TFree", ty_parms, []) else (); + val repv = Free ("x", ty_rep); + val absv = Free ("x", ty_abs); + val rep_mor = Logic.mk_implies + (PROP (absi $ absv), Logic.mk_equals (absm $ (repm $ absv), absv)); + val abs_mor = Logic.mk_implies + (PROP (repi $ repv), PROP (Const (repe, ty_rep --> ty_rep --> repe_ty') $ (repm $ (absm $ repv)) $ repv)); + val rep_inv = Logic.mk_implies + (PROP (absi $ absv), PROP (repi $ (repm $ absv))); + val abs_inv = Logic.mk_implies + (PROP (repi $ repv), PROP (absi $ (absm $ repv))); + in + thy + |> do_proof (K I) [rep_mor, abs_mor, rep_inv, abs_inv] + end; + +fun gen_e_simtype do_proof = gen_simtype Sign.read_term do_proof; +fun gen_i_simtype do_proof = gen_simtype Sign.cert_term do_proof; + +fun setup_proof after_qed props thy = + thy + |> ProofContext.init + |> Proof.theorem_i PureThy.internalK NONE after_qed NONE ("", []) + (map (fn t => (("", []), [(t, [])])) props); + +fun tactic_proof tac after_qed props thy = + let + val thms = Goal.prove_multi thy [] [] props (K tac); + in + thy + |> after_qed thms + end; + +in + +val simtype = gen_e_simtype setup_proof; +val simtype_i = gen_i_simtype setup_proof; +val prove_simtype = gen_i_simtype o tactic_proof; + +end; (*local*) + +local + +structure P = OuterParse +and K = OuterKeyword + +in + +val simtypeK = "code_simtype" + +val simtypeP = + OuterSyntax.command simtypeK "simulate type in executable code" K.thy_goal ( + (P.term -- P.term -- P.term -- P.term -- P.term) + >> (fn ((((raw_repm, raw_absm), raw_repi), raw_absi), raw_repe) => + (Toplevel.print oo Toplevel.theory_to_proof) + (simtype (raw_repm, raw_absm) (raw_repi, raw_absi) raw_repe)) + ); + +val _ = OuterSyntax.add_parsers [simtypeP]; + +end; (*local*) + +end; (*struct*) diff -r d064712bdd1d -r a7be206d8655 src/Pure/Tools/codegen_theorems.ML --- a/src/Pure/Tools/codegen_theorems.ML Tue Jun 13 23:41:59 2006 +0200 +++ b/src/Pure/Tools/codegen_theorems.ML Wed Jun 14 12:10:57 2006 +0200 @@ -7,7 +7,7 @@ signature CODEGEN_THEOREMS = sig - val add_notify: (string option -> theory -> theory) -> theory -> theory; + val add_notify: ((string * typ) list option -> theory -> theory) -> theory -> theory; val add_preproc: (theory -> thm list -> thm list) -> theory -> theory; val add_fun_extr: (theory -> string * typ -> thm list) -> theory -> theory; val add_datatype_extr: (theory -> string @@ -274,6 +274,15 @@ val (_, _, inst) = fold mk_inst (vars_of thm) (maxidx + 1, [], []); in Thm.instantiate ([], inst) thm end; +fun drop_redundant thy eqs = + let + val matches = curry (Pattern.matches thy o + pairself (fst o Logic.dest_equals o prop_of)) + fun drop eqs [] = eqs + | drop eqs (eq::eqs') = + drop (eq::eqs) (filter_out (matches eq) eqs') + in drop [] eqs end; + fun make_eq thy = let val ((_, atomize), _) = get_obj thy; @@ -293,7 +302,6 @@ | NONE => err_thm "not a function equation" thm; in thm - |> debug_msg (prefix "[cg_thm] dest_fun " o Pretty.output o Display.pretty_thm) |> dest_eq thy |> dest_fun' end; @@ -320,7 +328,7 @@ then NONE else SOME c; in (wc @ map_filter same_thms zc, Symtab.join (K (merge eq)) xyt) end; -datatype notify = Notify of (serial * (string option -> theory -> theory)) list; +datatype notify = Notify of (serial * ((string * typ) list option -> theory -> theory)) list; val mk_notify = Notify; fun map_notify f (Notify notify) = mk_notify (f notify); @@ -422,7 +430,7 @@ (*Pretty.fbreaks ( *) map (fn (c, thms) => (Pretty.block o Pretty.fbreaks) ( - Pretty.str c :: map pretty_thm thms + Pretty.str c :: map pretty_thm (rev thms) ) ) funs (*) *) @ [ @@ -460,6 +468,9 @@ (* notifiers *) +fun all_typs thy c = + map (pair c) (Sign.the_const_type thy c :: (map (#lhs) o Theory.definitions_of thy) c); + fun add_notify f = map_data (fn ((dirty, notify), x) => ((dirty, notify |> map_notify (cons (serial (), f))), x)); @@ -479,14 +490,14 @@ thy |> get_reset_dirty |-> (fn (true, _) => fold (fn f => f NONE) (the_notify thy) - | (false, cs) => let val cs' = case c of NONE => cs | SOME c => c::cs - in fold (fn f => fold (f o SOME) cs') (the_notify thy) end); + | (false, cs) => let val cs' = case c of NONE => cs | SOME c => insert (op =) c cs + in fold (fn f => f (SOME (maps (all_typs thy) cs'))) (the_notify thy) end); fun notify_dirty thy = thy |> get_reset_dirty |-> (fn (true, _) => fold (fn f => f NONE) (the_notify thy) - | (false, cs) => fold (fn f => fold (f o SOME) cs) (the_notify thy)); + | (false, cs) => fold (fn f => f (SOME (maps (all_typs thy) cs))) (the_notify thy)); (* modifiers *) @@ -514,7 +525,7 @@ thy |> map_data (fn (x, (preproc, (extrs, funthms))) => (x, (preproc, (extrs, funthms |> map_funthms (fn (dirty, funs) => - (dirty, funs |> Symtab.default (c, []) |> Symtab.map_entry c (fn thms => thms @ [thm]))))))) + (dirty, funs |> Symtab.default (c, []) |> Symtab.map_entry c (cons thm))))))) |> notify_all (SOME c); fun del_fun thm thy = @@ -572,15 +583,6 @@ cons (Thm.ctyp_of thy (TVar (x_i, sort)), Thm.ctyp_of thy ty)) env []; in map (Thm.instantiate (instT, [])) thms end; -fun extr_typ thy thm = case dest_fun thy thm - of (_, (ty, _)) => ty; - -fun tap_typ thy [] = NONE - | tap_typ thy (thms as (thm::_)) = SOME (extr_typ thy thm, thms); - -fun unvarify thy thms = - #1 (ProofContext.import true thms (ProofContext.init thy)); - fun preprocess thy thms = let fun burrow_thms f [] = [] @@ -589,12 +591,20 @@ |> Conjunction.intr_list |> f |> Conjunction.elim_list; + fun extr_typ thm = case dest_fun thy thm + of (_, (ty, _)) => ty; + fun tap_typ [] = NONE + | tap_typ (thms as (thm::_)) = SOME (extr_typ thm, thms); + fun cmp_thms (thm1, thm2) = + not (Sign.typ_instance thy (extr_typ thm1, extr_typ thm2)); fun rewrite_rhs conv thm = (case (Drule.strip_comb o cprop_of) thm of (ct', [ct1, ct2]) => (case term_of ct' of Const ("==", _) => Thm.equal_elim (combination (combination (reflexive ct') (reflexive ct1)) (conv ct2)) thm | _ => raise ERROR "rewrite_rhs") | _ => raise ERROR "rewrite_rhs"); + fun unvarify thms = + #1 (ProofContext.import true thms (ProofContext.init thy)); val unfold_thms = Tactic.rewrite true (map (make_eq thy) (the_unfolds thy)); in thms @@ -602,11 +612,12 @@ |> map (Thm.transfer thy) |> fold (fn f => f thy) (the_preprocs thy) |> map (rewrite_rhs unfold_thms) - |> debug_msg (fn _ => "[cg_thm] filter") + |> debug_msg (fn _ => "[cg_thm] sorting") |> debug_msg (commas o map string_of_thm) + |> sort (make_ord cmp_thms) |> debug_msg (fn _ => "[cg_thm] common_typ") |> debug_msg (commas o map string_of_thm) - |> common_typ thy (extr_typ thy) + |> common_typ thy extr_typ |> debug_msg (fn _ => "[cg_thm] abs_norm") |> debug_msg (commas o map string_of_thm) |> map (abs_norm thy) @@ -621,8 +632,9 @@ #> debug_msg (string_of_thm) #> Drule.zero_var_indexes ) - |> unvarify thy - |> tap_typ thy + |> drop_redundant thy + |> unvarify + |> tap_typ end; diff -r d064712bdd1d -r a7be206d8655 src/Pure/Tools/codegen_thingol.ML --- a/src/Pure/Tools/codegen_thingol.ML Tue Jun 13 23:41:59 2006 +0200 +++ b/src/Pure/Tools/codegen_thingol.ML Wed Jun 14 12:10:57 2006 +0200 @@ -28,7 +28,7 @@ | IVar of vname | `$ of iexpr * iexpr | `|-> of (vname * itype) * iexpr - | INum of IntInf.int (*positive!*) * unit + | INum of IntInf.int (*positive!*) * iexpr | IChar of string (*length one!*) * iexpr | IAbs of ((iexpr * itype) * iexpr) * iexpr (* (((binding expression (ve), binding type (vty)), @@ -90,11 +90,11 @@ val project_module: string list -> module -> module; val purge_module: string list -> module -> module; val has_nsp: string -> string -> bool; - val ensure_bot: string -> module -> module; + val ensure_def: (string -> transact -> def transact_fin) -> bool -> string + -> string -> transact -> transact; val succeed: 'a -> transact -> 'a transact_fin; val fail: string -> transact -> 'a transact_fin; - val ensure_def: (string -> transact -> def transact_fin) -> bool -> string - -> string -> transact -> transact; + val message: string -> (transact -> 'a) -> transact -> 'a; val start_transact: string option -> (transact -> 'a * transact) -> module -> 'a * module; val debug: bool ref; @@ -166,7 +166,7 @@ | IVar of vname | `$ of iexpr * iexpr | `|-> of (vname * itype) * iexpr - | INum of IntInf.int (*positive!*) * unit + | INum of IntInf.int (*positive!*) * iexpr | IChar of string (*length one!*) * iexpr | IAbs of ((iexpr * itype) * iexpr) * iexpr | ICase of ((iexpr * itype) * (iexpr * iexpr) list) * iexpr; @@ -321,7 +321,7 @@ | map_pure f (e as _ `|-> _) = f e | map_pure _ (INum _) = - error ("sorry, no pure representation of numerals so far") + error ("sorry, no pure representation for numerals so far") | map_pure f (IChar (_, e0)) = f e0 | map_pure f (IAbs (_, e0)) = @@ -619,8 +619,9 @@ if null r1 andalso null r2 then Graph.add_edge else fn edge => fn gr => (Graph.add_edge_acyclic edge gr - handle Graph.CYCLES _ => error ("adding dependency " - ^ quote name1 ^ " -> " ^ quote name2 ^ " would result in module dependency cycle")) + handle Graph.CYCLES _ => + error ("adding dependency " + ^ quote name1 ^ " -> " ^ quote name2 ^ " would result in module dependency cycle")) fun add [] node = node |> add_edge (s1, s2) @@ -634,7 +635,7 @@ fun join_module _ (Module m1, Module m2) = Module (merge_module (m1, m2)) | join_module name (Def d1, Def d2) = - if eq_def (d1, d2) then Def d1 else Def d1 (*raise Graph.DUP name*) + if eq_def (d1, d2) then Def d1 else Def Bot | join_module name _ = raise Graph.DUP name in Graph.join join_module modl12 end; @@ -655,9 +656,7 @@ ((AList.make (Graph.get_node modl1) o flat o Graph.strong_conn) modl1) in diff_modl [] modl12 [] end; -local - -fun project_trans f names modl = +fun project_module names modl = let datatype pathnode = PN of (string list * (string * pathnode) list); fun mk_ipath ([], base) (PN (defs, modls)) = @@ -669,7 +668,7 @@ |> (pair defs #> PN); fun select (PN (defs, modls)) (Module module) = module - |> f (Graph.all_succs module (defs @ map fst modls)) + |> Graph.subgraph (Graph.all_succs module (defs @ map fst modls)) |> fold (fn (name, modls) => Graph.map_node name (select modls)) modls |> Module; in @@ -679,37 +678,51 @@ |> dest_modl end; -in - -val project_module = project_trans Graph.subgraph; -val purge_module = project_trans Graph.del_nodes; - -end; (*local*) - -fun imports_of modl name = +fun purge_module names modl = let - (*fun submodules prfx modl = - cons prfx - #> Graph.fold - (fn (m, (Module modl, _)) => submodules (prfx @ [m]) modl - | (_, (Def _, _)) => I) modl; - fun get_modl name = - fold (fn n => fn modl => (dest_modl oo Graph.get_node) modl n) name modl*) - fun imports prfx [] modl = - [] - | imports prfx (m::ms) modl = - map (cons m) (imports (prfx @ [m]) ms ((dest_modl oo Graph.get_node) modl m)) - @ map single (Graph.imm_succs modl m) + fun split_names names = + fold + (fn ([], name) => apfst (cons name) + | (m::ms, name) => apsnd (AList.default (op =) (m : string, []) + #> AList.map_entry (op =) m (cons (ms, name)))) + names ([], []); + fun purge names (Module modl) = + let + val (ndefs, nmodls) = split_names names; + in + modl + |> Graph.del_nodes (Graph.all_preds modl ndefs) + |> fold (fn (nmodl, names') => Graph.map_node nmodl (purge names')) nmodls + |> Module + end; in - modl - |> imports [] name - (*|> cons name - |> map (fn name => submodules name (get_modl name) []) - |> flat - |> remove (op =) name*) - |> map NameSpace.pack + Module modl + |> purge (map dest_name names) + |> dest_modl end; +fun allimports_of modl = + let + fun imps_of prfx (Module modl) imps tab = + let + val this = NameSpace.pack prfx; + val name_con = (rev o Graph.strong_conn) modl; + in + tab + |> pair [] + |> fold (fn names => fn (imps', tab) => + tab + |> fold_map (fn name => + imps_of (prfx @ [name]) (Graph.get_node modl name) (imps' @ imps)) names + |-> (fn imps'' => pair (flat imps'' @ imps'))) name_con + |-> (fn imps' => + Symtab.update_new (this, imps' @ imps) + #> pair (this :: imps')) + end + | imps_of prfx (Def _) imps tab = + ([], tab); + in snd (imps_of [] (Module modl) [] Symtab.empty) end; + fun check_samemodule names = fold (fn name => let @@ -805,14 +818,14 @@ | postprocess_def _ = I; -fun succeed some (_, modl) = (some, modl); -fun fail msg (_, modl) = raise FAIL ([msg], NONE); + +(* transaction protocol *) fun ensure_def defgen strict msg name (dep, modl) = let val msg' = (case dep of NONE => msg - | SOME dep => msg ^ ", with dependency " ^ quote dep) + | SOME dep => msg ^ ", required for " ^ quote dep) ^ (if strict then " (strict)" else " (non-strict)"); fun add_dp NONE = I | add_dp (SOME dep) = @@ -821,18 +834,13 @@ fun prep_def def modl = (check_prep_def modl def, modl); fun invoke_generator name defgen modl = - if ! soft_exc - then - defgen name (SOME name, modl) - handle FAIL exc => - if strict then raise FAIL exc - else (Bot, modl) - | e => raise FAIL (["definition generator for " ^ quote name], SOME e) - else - defgen name (SOME name, modl) - handle FAIL exc => - if strict then raise FAIL exc - else (Bot, modl); + defgen name (SOME name, modl) + handle FAIL (msgs, exc) => + if strict then raise FAIL (msg' :: msgs, exc) + else (Bot, modl) + | e => raise if ! soft_exc + then FAIL (["definition generator for " ^ quote name, msg'], SOME e) + else e; in modl |> (if can (get_def modl) name @@ -857,6 +865,14 @@ |> pair dep end; +fun succeed some (_, modl) = (some, modl); + +fun fail msg (_, modl) = raise FAIL ([msg], NONE); + +fun message msg f trns = + f trns handle FAIL (msgs, exc) => + raise FAIL (msg :: msgs, exc); + fun start_transact init f modl = let fun handle_fail f x = @@ -866,9 +882,11 @@ handle FAIL (msgs, SOME e) => ((Output.error_msg o cat_lines) ("code generation failed, while:" :: msgs); raise e); in - (init, modl) + modl + |> (if is_some init then ensure_bot (the init) else I) + |> pair init |> handle_fail f - |-> (fn x => fn (_, module) => (x, module)) + |-> (fn x => fn (_, modl) => (x, modl)) end; @@ -966,6 +984,7 @@ fun serialize seri_defs seri_module validate postprocess nsp_conn name_root module = let + val imptab = allimports_of module; val resolver = mk_deresolver module nsp_conn postprocess validate; fun sresolver s = (resolver o NameSpace.unpack) s fun mk_name prfx name = @@ -976,14 +995,14 @@ map_filter (seri prfx) ((map (AList.make (Graph.get_node module)) o rev o Graph.strong_conn) module) and seri prfx [(name, Module modl)] = - seri_module (resolver []) (map (resolver []) (imports_of module (prfx @ [name]))) + seri_module (resolver []) (map (resolver []) ((the o Symtab.lookup imptab) (NameSpace.pack (prfx @ [name])))) (mk_name prfx name, mk_contents (prfx @ [name]) modl) | seri prfx [(_, Def Bot)] = NONE | seri prfx ds = seri_defs sresolver (NameSpace.pack prfx) (map (fn (name, Def def) => (fst (mk_name prfx name), def)) ds) in - seri_module (resolver []) (imports_of module []) + seri_module (resolver []) ((the o Symtab.lookup imptab) "") (*map (resolver []) (Graph.strong_conn module |> flat |> rev)*) (("", name_root), (mk_contents [] module)) end;