--- 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";
--- 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 *)
--- 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 *)
--- /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*)
--- 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;
--- 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;