--- a/src/FOL/IFOL.thy Wed Aug 10 18:02:16 2011 -0700
+++ b/src/FOL/IFOL.thy Wed Aug 10 18:07:32 2011 -0700
@@ -7,6 +7,7 @@
theory IFOL
imports Pure
uses
+ "~~/src/Tools/misc_legacy.ML"
"~~/src/Provers/splitter.ML"
"~~/src/Provers/hypsubst.ML"
"~~/src/Tools/IsaPlanner/zipper.ML"
--- a/src/FOL/IsaMakefile Wed Aug 10 18:02:16 2011 -0700
+++ b/src/FOL/IsaMakefile Wed Aug 10 18:07:32 2011 -0700
@@ -29,8 +29,9 @@
$(OUT)/FOL: $(OUT)/Pure $(SRC)/Provers/blast.ML \
$(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
- $(SRC)/Tools/case_product.ML $(SRC)/Tools/IsaPlanner/zipper.ML \
- $(SRC)/Tools/IsaPlanner/isand.ML $(SRC)/Tools/IsaPlanner/rw_tools.ML \
+ $(SRC)/Tools/case_product.ML $(SRC)/Tools/misc_legacy.ML \
+ $(SRC)/Tools/IsaPlanner/zipper.ML $(SRC)/Tools/IsaPlanner/isand.ML \
+ $(SRC)/Tools/IsaPlanner/rw_tools.ML \
$(SRC)/Tools/IsaPlanner/rw_inst.ML $(SRC)/Tools/eqsubst.ML \
$(SRC)/Provers/hypsubst.ML $(SRC)/Tools/induct.ML \
$(SRC)/Tools/intuitionistic.ML $(SRC)/Tools/atomize_elim.ML \
--- a/src/FOLP/IFOLP.thy Wed Aug 10 18:02:16 2011 -0700
+++ b/src/FOLP/IFOLP.thy Wed Aug 10 18:07:32 2011 -0700
@@ -7,7 +7,7 @@
theory IFOLP
imports Pure
-uses ("hypsubst.ML") ("intprover.ML")
+uses "~~/src/Tools/misc_legacy.ML" ("hypsubst.ML") ("intprover.ML")
begin
setup Pure_Thy.old_appl_syntax_setup
--- a/src/FOLP/IsaMakefile Wed Aug 10 18:02:16 2011 -0700
+++ b/src/FOLP/IsaMakefile Wed Aug 10 18:07:32 2011 -0700
@@ -26,7 +26,7 @@
@cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure
$(OUT)/FOLP: $(OUT)/Pure FOLP.thy IFOLP.thy ROOT.ML classical.ML \
- hypsubst.ML intprover.ML simp.ML simpdata.ML
+ hypsubst.ML intprover.ML simp.ML simpdata.ML $(SRC)/Tools/misc_legacy.ML
@$(ISABELLE_TOOL) usedir -b $(OUT)/Pure FOLP
--- a/src/FOLP/simp.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/FOLP/simp.ML Wed Aug 10 18:07:32 2011 -0700
@@ -155,21 +155,21 @@
(*ccs contains the names of the constants possessing congruence rules*)
fun add_hidden_vars ccs =
let fun add_hvars tm hvars = case tm of
- Abs(_,_,body) => OldTerm.add_term_vars(body,hvars)
+ Abs(_,_,body) => Misc_Legacy.add_term_vars(body,hvars)
| _$_ => let val (f,args) = strip_comb tm
in case f of
Const(c,T) =>
if member (op =) ccs c
then fold_rev add_hvars args hvars
- else OldTerm.add_term_vars (tm, hvars)
- | _ => OldTerm.add_term_vars (tm, hvars)
+ else Misc_Legacy.add_term_vars (tm, hvars)
+ | _ => Misc_Legacy.add_term_vars (tm, hvars)
end
| _ => hvars;
in add_hvars end;
fun add_new_asm_vars new_asms =
let fun itf (tm, at) vars =
- if at then vars else OldTerm.add_term_vars(tm,vars)
+ if at then vars else Misc_Legacy.add_term_vars(tm,vars)
fun add_list(tm,al,vars) = let val (_,tml) = strip_comb tm
in if length(tml)=length(al)
then fold_rev itf (tml ~~ al) vars
@@ -197,7 +197,7 @@
val hvars = add_new_asm_vars new_asms (rhs,hvars)
fun it_asms asm hvars =
if atomic asm then add_new_asm_vars new_asms (asm,hvars)
- else OldTerm.add_term_frees(asm,hvars)
+ else Misc_Legacy.add_term_frees(asm,hvars)
val hvars = fold_rev it_asms asms hvars
val hvs = map (#1 o dest_Var) hvars
val refl1_tac = refl_tac 1
@@ -543,7 +543,7 @@
fun find_subst sg T =
let fun find (thm::thms) =
let val (Const(_,cT), va, vb) = dest_red(hd(prems_of thm));
- val [P] = subtract (op =) [va, vb] (OldTerm.add_term_vars (concl_of thm, []));
+ val [P] = subtract (op =) [va, vb] (Misc_Legacy.add_term_vars (concl_of thm, []));
val eqT::_ = binder_types cT
in if Sign.typ_instance sg (T,eqT) then SOME(thm,va,vb,P)
else find thms
--- a/src/HOL/Decision_Procs/Cooper.thy Wed Aug 10 18:02:16 2011 -0700
+++ b/src/HOL/Decision_Procs/Cooper.thy Wed Aug 10 18:07:32 2011 -0700
@@ -1996,7 +1996,7 @@
let
val thy = Thm.theory_of_cterm ct;
val t = Thm.term_of ct;
- val fs = OldTerm.term_frees t;
+ val fs = Misc_Legacy.term_frees t;
val bs = term_bools [] t;
val vs = map_index swap fs;
val ps = map_index swap bs;
--- a/src/HOL/Decision_Procs/MIR.thy Wed Aug 10 18:02:16 2011 -0700
+++ b/src/HOL/Decision_Procs/MIR.thy Wed Aug 10 18:07:32 2011 -0700
@@ -5635,7 +5635,7 @@
let
val thy = Thm.theory_of_cterm ct;
val t = Thm.term_of ct;
- val fs = OldTerm.term_frees t;
+ val fs = Misc_Legacy.term_frees t;
val vs = map_index swap fs;
val qe = if proofs then @{code mirlfrqe} else @{code mircfrqe};
val t' = (term_of_fm vs o qe o fm_of_term vs) t;
--- a/src/HOL/Decision_Procs/commutative_ring_tac.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML Wed Aug 10 18:07:32 2011 -0700
@@ -68,7 +68,7 @@
fun reif_eq thy (eq as Const(@{const_name HOL.eq}, Type("fun", [T, _])) $ lhs $ rhs) =
if Sign.of_sort thy (T, cr_sort) then
let
- val fs = OldTerm.term_frees eq;
+ val fs = Misc_Legacy.term_frees eq;
val cvs = cterm_of thy (HOLogic.mk_list T fs);
val clhs = cterm_of thy (reif_polex T fs lhs);
val crhs = cterm_of thy (reif_polex T fs rhs);
--- a/src/HOL/Decision_Procs/cooper_tac.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Wed Aug 10 18:07:32 2011 -0700
@@ -55,7 +55,7 @@
val (fm',np) = List.foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
(List.foldr HOLogic.mk_imp c rhs, np) ps
val (vs, _) = List.partition (fn t => q orelse (type_of t) = nT)
- (OldTerm.term_frees fm' @ OldTerm.term_vars fm');
+ (Misc_Legacy.term_frees fm' @ Misc_Legacy.term_vars fm');
val fm2 = List.foldr mk_all2 fm' vs
in (fm2, np + length vs, length rhs) end;
--- a/src/HOL/Decision_Procs/ferrack_tac.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML Wed Aug 10 18:07:32 2011 -0700
@@ -61,7 +61,7 @@
val (fm',np) = List.foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
(List.foldr HOLogic.mk_imp c rhs, np) ps
val (vs, _) = List.partition (fn t => q orelse (type_of t) = HOLogic.natT)
- (OldTerm.term_frees fm' @ OldTerm.term_vars fm');
+ (Misc_Legacy.term_frees fm' @ Misc_Legacy.term_vars fm');
val fm2 = List.foldr mk_all2 fm' vs
in (fm2, np + length vs, length rhs) end;
--- a/src/HOL/Decision_Procs/langford.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/HOL/Decision_Procs/langford.ML Wed Aug 10 18:07:32 2011 -0700
@@ -113,7 +113,7 @@
val eqI = instantiate' [] [SOME ll, SOME rr] @{thm iffI}
in Thm.implies_elim (Thm.implies_elim eqI thl) thr |> mk_meta_eq end;
-fun contains x ct = member (op aconv) (OldTerm.term_frees (term_of ct)) (term_of x);
+fun contains x ct = member (op aconv) (Misc_Legacy.term_frees (term_of ct)) (term_of x);
fun is_eqx x eq = case term_of eq of
Const(@{const_name HOL.eq},_)$l$r => l aconv term_of x orelse r aconv term_of x
--- a/src/HOL/Decision_Procs/mir_tac.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/HOL/Decision_Procs/mir_tac.ML Wed Aug 10 18:07:32 2011 -0700
@@ -76,7 +76,7 @@
val (fm',np) = List.foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
(List.foldr HOLogic.mk_imp c rhs, np) ps
val (vs, _) = List.partition (fn t => q orelse (type_of t) = nT)
- (OldTerm.term_frees fm' @ OldTerm.term_vars fm');
+ (Misc_Legacy.term_frees fm' @ Misc_Legacy.term_vars fm');
val fm2 = List.foldr mk_all2 fm' vs
in (fm2, np + length vs, length rhs) end;
--- a/src/HOL/HOL.thy Wed Aug 10 18:02:16 2011 -0700
+++ b/src/HOL/HOL.thy Wed Aug 10 18:07:32 2011 -0700
@@ -15,7 +15,6 @@
"~~/src/Tools/intuitionistic.ML"
"~~/src/Tools/project_rule.ML"
"~~/src/Tools/cong_tac.ML"
- "~~/src/Tools/misc_legacy.ML"
"~~/src/Provers/hypsubst.ML"
"~~/src/Provers/splitter.ML"
"~~/src/Provers/classical.ML"
--- a/src/HOL/Import/proof_kernel.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/HOL/Import/proof_kernel.ML Wed Aug 10 18:07:32 2011 -0700
@@ -1059,7 +1059,7 @@
val ct = cprop_of thm
val t = term_of ct
val thy = theory_of_cterm ct
- val frees = OldTerm.term_frees t
+ val frees = Misc_Legacy.term_frees t
val freenames = Term.add_free_names t []
val is_old_name = member (op =) freenames
fun name_of (Free (n, _)) = n
@@ -1339,9 +1339,9 @@
let
val _ = message "INST_TYPE:"
val _ = if_debug pth hth
- val tys_before = OldTerm.add_term_tfrees (prop_of th,[])
+ val tys_before = Misc_Legacy.add_term_tfrees (prop_of th,[])
val th1 = Thm.varifyT_global th
- val tys_after = OldTerm.add_term_tvars (prop_of th1,[])
+ val tys_after = Misc_Legacy.add_term_tvars (prop_of th1,[])
val tyinst = map (fn (bef, iS) =>
(case try (Lib.assoc (TFree bef)) lambda of
SOME ty => (ctyp_of thy (TVar iS), ctyp_of thy ty)
@@ -2002,7 +2002,7 @@
val c = case concl_of th2 of
_ $ (Const(@{const_name Ex},_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c
| _ => raise ERR "new_type_definition" "Bad type definition theorem"
- val tfrees = OldTerm.term_tfrees c
+ val tfrees = Misc_Legacy.term_tfrees c
val tnames = map fst tfrees
val tsyn = mk_syn thy tycname
val typ = (tycname,tnames,tsyn)
@@ -2075,7 +2075,7 @@
val c = case concl_of th2 of
_ $ (Const(@{const_name Ex},_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c
| _ => raise ERR "type_introduction" "Bad type definition theorem"
- val tfrees = OldTerm.term_tfrees c
+ val tfrees = Misc_Legacy.term_tfrees c
val tnames = sort_strings (map fst tfrees)
val tsyn = mk_syn thy tycname
val typ = (tycname,tnames,tsyn)
--- a/src/HOL/Import/shuffler.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/HOL/Import/shuffler.ML Wed Aug 10 18:07:32 2011 -0700
@@ -223,8 +223,8 @@
fun freeze_thaw_term t =
let
- val tvars = OldTerm.term_tvars t
- val tfree_names = OldTerm.add_term_tfree_names(t,[])
+ val tvars = Misc_Legacy.term_tvars t
+ val tfree_names = Misc_Legacy.add_term_tfree_names(t,[])
val (type_inst,_) =
fold (fn (w as (v,_), S) => fn (inst, used) =>
let
@@ -243,7 +243,7 @@
| inst_tfrees thy ((name,U)::rest) thm =
let
val cU = ctyp_of thy U
- val tfrees = OldTerm.add_term_tfrees (prop_of thm,[])
+ val tfrees = Misc_Legacy.add_term_tfrees (prop_of thm,[])
val (rens, thm') = Thm.varifyT_global'
(remove (op = o apsnd fst) name tfrees) thm
val mid =
@@ -494,7 +494,7 @@
let
val thy = Thm.theory_of_thm th
val c = prop_of th
- val vars = OldTerm.add_term_frees (c, OldTerm.add_term_vars(c,[]))
+ val vars = Misc_Legacy.add_term_frees (c, Misc_Legacy.add_term_vars(c,[]))
in
Drule.forall_intr_list (map (cterm_of thy) vars) th
end
@@ -560,7 +560,7 @@
fun set_prop thy t =
let
- val vars = OldTerm.add_term_frees (t, OldTerm.add_term_vars (t,[]))
+ val vars = Misc_Legacy.add_term_frees (t, Misc_Legacy.add_term_vars (t,[]))
val closed_t = fold_rev Logic.all vars t
val rew_th = norm_term thy closed_t
val rhs = Thm.rhs_of rew_th
--- a/src/HOL/IsaMakefile Wed Aug 10 18:02:16 2011 -0700
+++ b/src/HOL/IsaMakefile Wed Aug 10 18:07:32 2011 -0700
@@ -122,7 +122,6 @@
$(SRC)/Provers/hypsubst.ML \
$(SRC)/Provers/quantifier1.ML \
$(SRC)/Provers/splitter.ML \
- $(SRC)/Tools/cache_io.ML \
$(SRC)/Tools/Code/code_haskell.ML \
$(SRC)/Tools/Code/code_ml.ML \
$(SRC)/Tools/Code/code_namespace.ML \
@@ -139,7 +138,9 @@
$(SRC)/Tools/IsaPlanner/rw_tools.ML \
$(SRC)/Tools/IsaPlanner/zipper.ML \
$(SRC)/Tools/atomize_elim.ML \
+ $(SRC)/Tools/cache_io.ML \
$(SRC)/Tools/case_product.ML \
+ $(SRC)/Tools/codegen.ML \
$(SRC)/Tools/coherent.ML \
$(SRC)/Tools/cong_tac.ML \
$(SRC)/Tools/eqsubst.ML \
--- a/src/HOL/Matrix/Compute_Oracle/linker.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/HOL/Matrix/Compute_Oracle/linker.ML Wed Aug 10 18:07:32 2011 -0700
@@ -90,7 +90,7 @@
let
val cs = distinct_constants (filter is_polymorphic cs)
val old_cs = cs
-(* fun collect_tvars ty tab = fold (fn v => fn tab => Typtab.update (TVar v, ()) tab) (OldTerm.typ_tvars ty) tab
+(* fun collect_tvars ty tab = fold (fn v => fn tab => Typtab.update (TVar v, ()) tab) (Misc_Legacy.typ_tvars ty) tab
val tvars_count = length (Typtab.keys (fold (fn c => fn tab => collect_tvars (typ_of_constant c) tab) cs Typtab.empty))
fun tvars_of ty = collect_tvars ty Typtab.empty
val cs = map (fn c => (c, tvars_of (typ_of_constant c))) cs
@@ -259,10 +259,10 @@
let
val (left, right) = collect_consts_of_thm th
val polycs = filter Linker.is_polymorphic left
- val tytab = fold (fn p => fn tab => fold (fn n => fn tab => Typtab.update (TVar n, ()) tab) (OldTerm.typ_tvars (Linker.typ_of_constant p)) tab) polycs Typtab.empty
+ val tytab = fold (fn p => fn tab => fold (fn n => fn tab => Typtab.update (TVar n, ()) tab) (Misc_Legacy.typ_tvars (Linker.typ_of_constant p)) tab) polycs Typtab.empty
fun check_const (c::cs) cs' =
let
- val tvars = OldTerm.typ_tvars (Linker.typ_of_constant c)
+ val tvars = Misc_Legacy.typ_tvars (Linker.typ_of_constant c)
val wrong = fold (fn n => fn wrong => wrong orelse is_none (Typtab.lookup tytab (TVar n))) tvars false
in
if wrong then raise PCompute "right hand side of theorem contains type variables which do not occur on the left hand side"
--- a/src/HOL/Matrix/matrixlp.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/HOL/Matrix/matrixlp.ML Wed Aug 10 18:07:32 2011 -0700
@@ -19,7 +19,7 @@
fun inst_real thm =
let val certT = ctyp_of (Thm.theory_of_thm thm) in
Drule.export_without_context (Thm.instantiate
- ([(certT (TVar (hd (OldTerm.term_tvars (prop_of thm)))), certT HOLogic.realT)], []) thm)
+ ([(certT (TVar (hd (Misc_Legacy.term_tvars (prop_of thm)))), certT HOLogic.realT)], []) thm)
end
local
@@ -57,7 +57,7 @@
let
val certT = Thm.ctyp_of (Thm.theory_of_thm thm);
val ord = prod_ord (prod_ord string_ord int_ord) (list_ord string_ord)
- val v = TVar (hd (sort ord (OldTerm.term_tvars (prop_of thm))))
+ val v = TVar (hd (sort ord (Misc_Legacy.term_tvars (prop_of thm))))
in
Drule.export_without_context (Thm.instantiate ([(certT v, certT ty)], []) thm)
end
--- a/src/HOL/Nominal/nominal_datatype.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/HOL/Nominal/nominal_datatype.ML Wed Aug 10 18:07:32 2011 -0700
@@ -1414,7 +1414,7 @@
val _ = warning "defining recursion combinator ...";
- val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
+ val used = List.foldr Misc_Legacy.add_typ_tfree_names [] recTs;
val (rec_result_Ts', rec_fn_Ts') = Datatype_Prop.make_primrec_Ts descr' sorts used;
--- a/src/HOL/Nominal/nominal_fresh_fun.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML Wed Aug 10 18:07:32 2011 -0700
@@ -69,7 +69,7 @@
val bvs = map_index (Bound o fst) ps;
(* select variables of the right class *)
val vs = filter (fn t => is_of_fs_name (fastype_of1 (Ts, t)))
- (OldTerm.term_frees goal @ bvs);
+ (Misc_Legacy.term_frees goal @ bvs);
(* build the tuple *)
val s = (Library.foldr1 (fn (v, s) =>
HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s) vs)
@@ -78,7 +78,7 @@
val at_name_inst_thm = get_dyn_thm thy ("at_"^atom_basename^"_inst") atom_basename;
val exists_fresh' = at_name_inst_thm RS at_exists_fresh';
(* find the variable we want to instantiate *)
- val x = hd (OldTerm.term_vars (prop_of exists_fresh'));
+ val x = hd (Misc_Legacy.term_vars (prop_of exists_fresh'));
in
(cut_inst_tac_term' [(x,s)] exists_fresh' 1 THEN
rtac fs_name_thm 1 THEN
@@ -137,7 +137,7 @@
val fresh_perm_app = Global_Theory.get_thms thy "fresh_perm_app";
val ss' = ss addsimps fresh_prod::abs_fresh;
val ss'' = ss' addsimps fresh_perm_app;
- val x = hd (tl (OldTerm.term_vars (prop_of exI)));
+ val x = hd (tl (Misc_Legacy.term_vars (prop_of exI)));
val goal = nth (prems_of thm) (i-1);
val atom_name_opt = get_inner_fresh_fun goal;
val n = length (Logic.strip_params goal);
@@ -152,7 +152,7 @@
val pt_name_inst = get_dyn_thm thy ("pt_"^atom_basename^"_inst") atom_basename;
val at_name_inst = get_dyn_thm thy ("at_"^atom_basename^"_inst") atom_basename;
fun inst_fresh vars params i st =
- let val vars' = OldTerm.term_vars (prop_of st);
+ let val vars' = Misc_Legacy.term_vars (prop_of st);
val thy = theory_of_thm st;
in case subtract (op =) vars vars' of
[x] => Seq.single (Thm.instantiate ([],[(cterm_of thy x,cterm_of thy (list_abs (params,Bound 0)))]) st)
@@ -161,7 +161,7 @@
in
((fn st =>
let
- val vars = OldTerm.term_vars (prop_of st);
+ val vars = Misc_Legacy.term_vars (prop_of st);
val params = Logic.strip_params (nth (prems_of st) (i-1))
(* The tactics which solve the subgoals generated
by the conditionnal rewrite rule. *)
--- a/src/HOL/Nominal/nominal_primrec.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/HOL/Nominal/nominal_primrec.ML Wed Aug 10 18:07:32 2011 -0700
@@ -76,7 +76,7 @@
else
(check_vars "repeated variable names in pattern: " (duplicates (op =) lfrees);
check_vars "extra variables on rhs: "
- (map dest_Free (OldTerm.term_frees rhs) |> subtract (op =) lfrees
+ (map dest_Free (Misc_Legacy.term_frees rhs) |> subtract (op =) lfrees
|> filter_out (is_fixed o fst));
case AList.lookup (op =) rec_fns fname of
NONE =>
--- a/src/HOL/Statespace/state_space.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/HOL/Statespace/state_space.ML Wed Aug 10 18:07:32 2011 -0700
@@ -472,7 +472,7 @@
let
val ctxt' = fold (Variable.declare_typ o TFree) env ctxt;
val T = Syntax.read_typ ctxt' raw_T;
- val env' = OldTerm.add_typ_tfrees (T, env);
+ val env' = Misc_Legacy.add_typ_tfrees (T, env);
in (T, env') end;
fun cert_typ ctxt raw_T env =
@@ -480,7 +480,7 @@
val thy = Proof_Context.theory_of ctxt;
val T = Type.no_tvars (Sign.certify_typ thy raw_T)
handle TYPE (msg, _, _) => error msg;
- val env' = OldTerm.add_typ_tfrees (T, env);
+ val env' = Misc_Legacy.add_typ_tfrees (T, env);
in (T, env') end;
fun gen_define_statespace prep_typ state_space args name parents comps thy =
--- a/src/HOL/Tools/ATP/atp_reconstruct.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Wed Aug 10 18:07:32 2011 -0700
@@ -545,12 +545,12 @@
|> HOLogic.dest_eq
in
(Definition (name, t1, t2),
- fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt)
+ fold Variable.declare_term (maps Misc_Legacy.term_frees [t1, t2]) ctxt)
end
| decode_line sym_tab (Inference (name, u, deps)) ctxt =
let val t = u |> uncombined_etc_prop_from_atp ctxt true sym_tab in
(Inference (name, t, deps),
- fold Variable.declare_term (OldTerm.term_frees t) ctxt)
+ fold Variable.declare_term (Misc_Legacy.term_frees t) ctxt)
end
fun decode_lines ctxt sym_tab lines =
fst (fold_map (decode_line sym_tab) lines ctxt)
--- a/src/HOL/Tools/ATP/atp_translate.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/HOL/Tools/ATP/atp_translate.ML Wed Aug 10 18:07:32 2011 -0700
@@ -1457,8 +1457,8 @@
#> List.foldl add_classes Symtab.empty
#> delete_type #> Symtab.keys
-val tfree_classes_of_terms = classes_of_terms OldTerm.term_tfrees
-val tvar_classes_of_terms = classes_of_terms OldTerm.term_tvars
+val tfree_classes_of_terms = classes_of_terms Misc_Legacy.term_tfrees
+val tvar_classes_of_terms = classes_of_terms Misc_Legacy.term_tvars
fun fold_type_constrs f (Type (s, Ts)) x =
fold (fold_type_constrs f) Ts (f (s, x))
--- a/src/HOL/Tools/Datatype/datatype.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/HOL/Tools/Datatype/datatype.ML Wed Aug 10 18:07:32 2011 -0700
@@ -77,7 +77,7 @@
else Balanced_Tree.make (fn (T, U) => Type (@{type_name Sum_Type.sum}, [T, U])) branchTs;
val arities = remove (op =) 0 (Datatype_Aux.get_arities descr');
val unneeded_vars =
- subtract (op =) (List.foldr OldTerm.add_typ_tfree_names [] (leafTs' @ branchTs)) (hd tyvars);
+ subtract (op =) (List.foldr Misc_Legacy.add_typ_tfree_names [] (leafTs' @ branchTs)) (hd tyvars);
val leafTs = leafTs' @ map (fn n => TFree (n, (the o AList.lookup (op =) sorts) n)) unneeded_vars;
val recTs = Datatype_Aux.get_rec_types descr' sorts;
val (newTs, oldTs) = chop (length (hd descr)) recTs;
@@ -372,7 +372,7 @@
val prop = Thm.prop_of thm;
val _ $ (_ $ ((S as Const (_, Type (_, [U, _]))) $ _ )) $
(_ $ (_ $ (r $ (a $ _)) $ _)) = Type.legacy_freeze prop;
- val used = OldTerm.add_term_tfree_names (a, []);
+ val used = Misc_Legacy.add_term_tfree_names (a, []);
fun mk_thm i =
let
@@ -676,7 +676,7 @@
let
val (cargs', sorts'') = fold_map (prep_typ tmp_thy) cargs sorts';
val _ =
- (case subtract (op =) tvs (fold (curry OldTerm.add_typ_tfree_names) cargs' []) of
+ (case subtract (op =) tvs (fold (curry Misc_Legacy.add_typ_tfree_names) cargs' []) of
[] => ()
| vs => error ("Extra type variables on rhs: " ^ commas vs));
val c = Sign.full_name_path tmp_thy tname' cname;
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Wed Aug 10 18:07:32 2011 -0700
@@ -91,7 +91,7 @@
val descr' = flat descr;
val recTs = Datatype_Aux.get_rec_types descr' sorts;
- val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
+ val used = List.foldr Misc_Legacy.add_typ_tfree_names [] recTs;
val newTs = take (length (hd descr)) recTs;
val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
@@ -279,7 +279,7 @@
val descr' = flat descr;
val recTs = Datatype_Aux.get_rec_types descr' sorts;
- val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
+ val used = List.foldr Misc_Legacy.add_typ_tfree_names [] recTs;
val newTs = take (length (hd descr)) recTs;
val T' = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS);
--- a/src/HOL/Tools/Datatype/datatype_aux.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML Wed Aug 10 18:07:32 2011 -0700
@@ -144,7 +144,7 @@
fun abstr (t1, t2) =
(case t1 of
NONE =>
- (case flt (OldTerm.term_frees t2) of
+ (case flt (Misc_Legacy.term_frees t2) of
[Free (s, T)] => SOME (absfree (s, T, t2))
| _ => NONE)
| SOME (_ $ t') => SOME (Abs ("x", fastype_of t', abstract_over (t', t2))))
--- a/src/HOL/Tools/Datatype/datatype_case.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/HOL/Tools/Datatype/datatype_case.ML Wed Aug 10 18:07:32 2011 -0700
@@ -318,7 +318,7 @@
val _ = if length zs < i then raise CASE_ERROR ("", 0) else ();
val (xs, ys) = chop i zs;
val u = list_abs (ys, strip_abs_body t);
- val xs' = map Free (Name.variant_list (OldTerm.add_term_names (u, used))
+ val xs' = map Free (Name.variant_list (Misc_Legacy.add_term_names (u, used))
(map fst xs) ~~ map snd xs)
in (xs', subst_bounds (rev xs', u)) end;
fun is_dependent i t =
@@ -379,9 +379,9 @@
fun strip_case'' dest (pat, rhs) =
(case dest (Term.add_free_names pat []) rhs of
SOME (exp as Free _, clauses) =>
- if member op aconv (OldTerm.term_frees pat) exp andalso
+ if member op aconv (Misc_Legacy.term_frees pat) exp andalso
not (exists (fn (_, rhs') =>
- member op aconv (OldTerm.term_frees rhs') exp) clauses)
+ member op aconv (Misc_Legacy.term_frees rhs') exp) clauses)
then
maps (strip_case'' dest) (map (fn (pat', rhs') =>
(subst_free [(exp, pat')] pat, rhs')) clauses)
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Wed Aug 10 18:07:32 2011 -0700
@@ -331,8 +331,8 @@
let
val ts1 = take i ts;
val t :: ts2 = drop i ts;
- val names = List.foldr OldTerm.add_term_names
- (map (fst o fst o dest_Var) (List.foldr OldTerm.add_term_vars [] ts1)) ts1;
+ val names = List.foldr Misc_Legacy.add_term_names
+ (map (fst o fst o dest_Var) (List.foldr Misc_Legacy.add_term_vars [] ts1)) ts1;
val (Ts, dT) = split_last (take (i+1) (binder_types T));
fun pcase [] [] [] gr = ([], gr)
--- a/src/HOL/Tools/Datatype/datatype_data.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/HOL/Tools/Datatype/datatype_data.ML Wed Aug 10 18:07:32 2011 -0700
@@ -398,7 +398,7 @@
Syntax.string_of_typ ctxt T);
fun type_of_constr (cT as (_, T)) =
let
- val frees = OldTerm.typ_tfrees T;
+ val frees = Misc_Legacy.typ_tfrees T;
val (tyco, vs) = (apsnd o map) dest_TFree (dest_Type (body_type T))
handle TYPE _ => no_constr cT
val _ = if has_duplicates (eq_fst (op =)) vs then no_constr cT else ();
--- a/src/HOL/Tools/Datatype/datatype_prop.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML Wed Aug 10 18:07:32 2011 -0700
@@ -210,7 +210,7 @@
let
val descr' = flat descr;
val recTs = Datatype_Aux.get_rec_types descr' sorts;
- val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
+ val used = List.foldr Misc_Legacy.add_typ_tfree_names [] recTs;
val (rec_result_Ts, reccomb_fn_Ts) = make_primrec_Ts descr sorts used;
@@ -261,7 +261,7 @@
let
val descr' = flat descr;
val recTs = Datatype_Aux.get_rec_types descr' sorts;
- val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
+ val used = List.foldr Misc_Legacy.add_typ_tfree_names [] recTs;
val newTs = take (length (hd descr)) recTs;
val T' = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS);
@@ -308,7 +308,7 @@
let
val descr' = flat descr;
val recTs = Datatype_Aux.get_rec_types descr' sorts;
- val used' = List.foldr OldTerm.add_typ_tfree_names [] recTs;
+ val used' = List.foldr Misc_Legacy.add_typ_tfree_names [] recTs;
val newTs = take (length (hd descr)) recTs;
val T' = TFree (singleton (Name.variant_list used') "'t", HOLogic.typeS);
val P = Free ("P", T' --> HOLogic.boolT);
--- a/src/HOL/Tools/Meson/meson_clausify.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Wed Aug 10 18:07:32 2011 -0700
@@ -65,7 +65,7 @@
fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (_, T, p))) rhss =
(*Existential: declare a Skolem function, then insert into body and continue*)
let
- val args = OldTerm.term_frees body
+ val args = Misc_Legacy.term_frees body
(* Forms a lambda-abstraction over the formal parameters *)
val rhs =
list_abs_free (map dest_Free args,
@@ -75,7 +75,7 @@
in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end
| dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) rhss =
(*Universal quant: insert a free variable into body and continue*)
- let val fname = singleton (Name.variant_list (OldTerm.add_term_names (p, []))) a
+ let val fname = singleton (Name.variant_list (Misc_Legacy.add_term_names (p, []))) a
in dec_sko (subst_bound (Free(fname,T), p)) rhss end
| dec_sko (@{const conj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
| dec_sko (@{const disj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
@@ -92,9 +92,9 @@
| is_quasi_lambda_free (Abs _) = false
| is_quasi_lambda_free _ = true
-val [f_B,g_B] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_B}));
-val [g_C,f_C] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_C}));
-val [f_S,g_S] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_S}));
+val [f_B,g_B] = map (cterm_of @{theory}) (Misc_Legacy.term_vars (prop_of @{thm abs_B}));
+val [g_C,f_C] = map (cterm_of @{theory}) (Misc_Legacy.term_vars (prop_of @{thm abs_C}));
+val [f_S,g_S] = map (cterm_of @{theory}) (Misc_Legacy.term_vars (prop_of @{thm abs_S}));
(* FIXME: Requires more use of cterm constructors. *)
fun abstract ct =
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Wed Aug 10 18:07:32 2011 -0700
@@ -372,7 +372,7 @@
val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
val _ = trace_msg ctxt (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
val eq_terms = map (pairself (cterm_of thy))
- (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
+ (ListPair.zip (Misc_Legacy.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
in cterm_instantiate eq_terms subst' end;
val factor = Seq.hd o distinct_subgoals_tac
--- a/src/HOL/Tools/Qelim/cooper.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/HOL/Tools/Qelim/cooper.ML Wed Aug 10 18:07:32 2011 -0700
@@ -560,7 +560,7 @@
fun conv ctxt p =
Qelim.gen_qelim_conv (Simplifier.rewrite conv_ss) (Simplifier.rewrite presburger_ss) (Simplifier.rewrite conv_ss)
- (cons o term_of) (OldTerm.term_frees (term_of p)) (linearize_conv ctxt) (integer_nnf_conv ctxt)
+ (cons o term_of) (Misc_Legacy.term_frees (term_of p)) (linearize_conv ctxt) (integer_nnf_conv ctxt)
(cooperex_conv ctxt) p
handle CTERM s => raise COOPER "bad cterm"
| THM s => raise COOPER "bad thm"
@@ -759,8 +759,8 @@
in
fun is_relevant ctxt ct =
subset (op aconv) (term_constants (term_of ct) , snd (get ctxt))
- andalso forall (fn Free (_,T) => member (op =) [@{typ int}, @{typ nat}] T) (OldTerm.term_frees (term_of ct))
- andalso forall (fn Var (_,T) => member (op =) [@{typ int}, @{typ nat}] T) (OldTerm.term_vars (term_of ct));
+ andalso forall (fn Free (_,T) => member (op =) [@{typ int}, @{typ nat}] T) (Misc_Legacy.term_frees (term_of ct))
+ andalso forall (fn Var (_,T) => member (op =) [@{typ int}, @{typ nat}] T) (Misc_Legacy.term_vars (term_of ct));
fun int_nat_terms ctxt ct =
let
--- a/src/HOL/Tools/Sledgehammer/async_manager.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/HOL/Tools/Sledgehammer/async_manager.ML Wed Aug 10 18:07:32 2011 -0700
@@ -144,7 +144,7 @@
NONE
else
let
- val _ = List.app (Simple_Thread.interrupt o #1) canceling
+ val _ = List.app (Simple_Thread.interrupt_unsynchronized o #1) canceling
val canceling' = filter (Thread.isActive o #1) canceling
val state' = make_state manager timeout_heap' active canceling' messages store;
in SOME (map #2 timeout_threads, state') end
--- a/src/HOL/Tools/TFL/casesplit.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/HOL/Tools/TFL/casesplit.ML Wed Aug 10 18:07:32 2011 -0700
@@ -56,9 +56,9 @@
val abs_ct = ctermify abst;
val free_ct = ctermify x;
- val casethm_vars = rev (OldTerm.term_vars (Thm.concl_of case_thm));
+ val casethm_vars = rev (Misc_Legacy.term_vars (Thm.concl_of case_thm));
- val casethm_tvars = OldTerm.term_tvars (Thm.concl_of case_thm);
+ val casethm_tvars = Misc_Legacy.term_tvars (Thm.concl_of case_thm);
val (Pv, Dv, type_insts) =
case (Thm.concl_of case_thm) of
(_ $ ((Pv as Var(P,Pty)) $ (Dv as Var(D, Dty)))) =>
--- a/src/HOL/Tools/TFL/rules.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/HOL/Tools/TFL/rules.ML Wed Aug 10 18:07:32 2011 -0700
@@ -160,7 +160,7 @@
*---------------------------------------------------------------------------*)
local val thy = Thm.theory_of_thm disjI1
val prop = Thm.prop_of disjI1
- val [P,Q] = OldTerm.term_vars prop
+ val [P,Q] = Misc_Legacy.term_vars prop
val disj1 = Thm.forall_intr (Thm.cterm_of thy Q) disjI1
in
fun DISJ1 thm tm = thm RS (Thm.forall_elim (Dcterm.drop_prop tm) disj1)
@@ -169,7 +169,7 @@
local val thy = Thm.theory_of_thm disjI2
val prop = Thm.prop_of disjI2
- val [P,Q] = OldTerm.term_vars prop
+ val [P,Q] = Misc_Legacy.term_vars prop
val disj2 = Thm.forall_intr (Thm.cterm_of thy P) disjI2
in
fun DISJ2 tm thm = thm RS (Thm.forall_elim (Dcterm.drop_prop tm) disj2)
@@ -263,7 +263,7 @@
local (* this is fragile *)
val thy = Thm.theory_of_thm spec
val prop = Thm.prop_of spec
- val x = hd (tl (OldTerm.term_vars prop))
+ val x = hd (tl (Misc_Legacy.term_vars prop))
val cTV = ctyp_of thy (type_of x)
val gspec = Thm.forall_intr (cterm_of thy x) spec
in
@@ -280,7 +280,7 @@
(* Not optimized! Too complicated. *)
local val thy = Thm.theory_of_thm allI
val prop = Thm.prop_of allI
- val [P] = OldTerm.add_term_vars (prop, [])
+ val [P] = Misc_Legacy.add_term_vars (prop, [])
fun cty_theta s = map (fn (i, (S, ty)) => (ctyp_of s (TVar (i, S)), ctyp_of s ty))
fun ctm_theta s = map (fn (i, (_, tm2)) =>
let val ctm2 = cterm_of s tm2
@@ -310,7 +310,7 @@
let val thy = Thm.theory_of_thm thm
val prop = Thm.prop_of thm
val tycheck = cterm_of thy
- val vlist = map tycheck (OldTerm.add_term_vars (prop, []))
+ val vlist = map tycheck (Misc_Legacy.add_term_vars (prop, []))
in GENL vlist thm
end;
@@ -350,7 +350,7 @@
local val thy = Thm.theory_of_thm exI
val prop = Thm.prop_of exI
- val [P,x] = OldTerm.term_vars prop
+ val [P,x] = Misc_Legacy.term_vars prop
in
fun EXISTS (template,witness) thm =
let val thy = Thm.theory_of_thm thm
@@ -501,7 +501,7 @@
val (f,args) = USyntax.strip_comb (get_lhs eq)
val (vstrl,_) = USyntax.strip_abs f
val names =
- Name.variant_list (OldTerm.add_term_names(body, [])) (map (#1 o dest_Free) vstrl)
+ Name.variant_list (Misc_Legacy.add_term_names(body, [])) (map (#1 o dest_Free) vstrl)
in get (rst, n+1, (names,n)::L) end
handle TERM _ => get (rst, n+1, L)
| Utils.ERR _ => get (rst, n+1, L);
@@ -742,7 +742,7 @@
val thy = Thm.theory_of_thm thm
val Const("==>",_) $ (Const(@{const_name Trueprop},_) $ A) $ _ = Thm.prop_of thm
fun genl tm = let val vlist = subtract (op aconv) globals
- (OldTerm.add_term_frees(tm,[]))
+ (Misc_Legacy.add_term_frees(tm,[]))
in fold_rev Forall vlist tm
end
(*--------------------------------------------------------------
@@ -780,7 +780,7 @@
(if (is_cong thm) then cong_prover else restrict_prover) ss thm
end
val ctm = cprop_of th
- val names = OldTerm.add_term_names (term_of ctm, [])
+ val names = Misc_Legacy.add_term_names (term_of ctm, [])
val th1 = Raw_Simplifier.rewrite_cterm (false,true,false)
(prover names) (ss0 addsimps [cut_lemma'] addeqcongs congs) ctm
val th2 = Thm.equal_elim th1 th
--- a/src/HOL/Tools/TFL/tfl.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/HOL/Tools/TFL/tfl.ML Wed Aug 10 18:07:32 2011 -0700
@@ -322,7 +322,7 @@
val dummy = map (no_repeat_vars thy) pats
val rows = ListPair.zip (map (fn x => ([]:term list,[x])) pats,
map_index (fn (i, t) => (t,(i,true))) R)
- val names = List.foldr OldTerm.add_term_names [] R
+ val names = List.foldr Misc_Legacy.add_term_names [] R
val atype = type_of(hd pats)
and aname = singleton (Name.variant_list names) "a"
val a = Free(aname,atype)
@@ -480,7 +480,7 @@
val tych = Thry.typecheck thy
val WFREC_THM0 = Rules.ISPEC (tych functional) Thms.WFREC_COROLLARY
val Const(@{const_name All},_) $ Abs(Rname,Rtype,_) = concl WFREC_THM0
- val R = Free (singleton (Name.variant_list (List.foldr OldTerm.add_term_names [] eqns)) Rname,
+ val R = Free (singleton (Name.variant_list (List.foldr Misc_Legacy.add_term_names [] eqns)) Rname,
Rtype)
val WFREC_THM = Rules.ISPECL [tych R, tych g] WFREC_THM0
val ([proto_def, WFR],_) = USyntax.strip_imp(concl WFREC_THM)
@@ -677,7 +677,7 @@
let val tych = Thry.typecheck thy
val ty_info = Thry.induct_info thy
in fn pats =>
- let val names = List.foldr OldTerm.add_term_names [] pats
+ let val names = List.foldr Misc_Legacy.add_term_names [] pats
val T = type_of (hd pats)
val aname = singleton (Name.variant_list names) "a"
val vname = singleton (Name.variant_list (aname::names)) "v"
@@ -830,7 +830,7 @@
val (pats,TCsl) = ListPair.unzip pat_TCs_list
val case_thm = complete_cases thy pats
val domain = (type_of o hd) pats
- val Pname = singleton (Name.variant_list (List.foldr (Library.foldr OldTerm.add_term_names)
+ val Pname = singleton (Name.variant_list (List.foldr (Library.foldr Misc_Legacy.add_term_names)
[] (pats::TCsl))) "P"
val P = Free(Pname, domain --> HOLogic.boolT)
val Sinduct = Rules.SPEC (tych P) Sinduction
@@ -843,7 +843,7 @@
val proved_cases = map (prove_case fconst thy) tasks
val v =
Free (singleton
- (Name.variant_list (List.foldr OldTerm.add_term_names [] (map concl proved_cases))) "v",
+ (Name.variant_list (List.foldr Misc_Legacy.add_term_names [] (map concl proved_cases))) "v",
domain)
val vtyped = tych v
val substs = map (Rules.SYM o Rules.ASSUME o tych o (curry HOLogic.mk_eq v)) pats
--- a/src/HOL/Tools/TFL/usyntax.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/HOL/Tools/TFL/usyntax.ML Wed Aug 10 18:07:32 2011 -0700
@@ -112,7 +112,7 @@
val is_vartype = can dest_vtype;
-val type_vars = map mk_prim_vartype o OldTerm.typ_tvars
+val type_vars = map mk_prim_vartype o Misc_Legacy.typ_tvars
fun type_varsl L = distinct (op =) (fold (curry op @ o type_vars) L []);
val alpha = mk_vartype "'a"
@@ -142,7 +142,7 @@
-val type_vars_in_term = map mk_prim_vartype o OldTerm.term_tvars;
+val type_vars_in_term = map mk_prim_vartype o Misc_Legacy.term_tvars;
@@ -319,7 +319,7 @@
(* Need to reverse? *)
-fun gen_all tm = list_mk_forall(OldTerm.term_frees tm, tm);
+fun gen_all tm = list_mk_forall(Misc_Legacy.term_frees tm, tm);
(* Destructing a cterm to a list of Terms *)
fun strip_comb tm =
--- a/src/HOL/Tools/choice_specification.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/HOL/Tools/choice_specification.ML Wed Aug 10 18:07:32 2011 -0700
@@ -18,7 +18,7 @@
fun close_form t =
fold_rev (fn (s, T) => fn t => HOLogic.mk_all (s, T, t))
- (map dest_Free (OldTerm.term_frees t)) t
+ (map dest_Free (Misc_Legacy.term_frees t)) t
local
fun mk_definitional [] arg = arg
@@ -122,7 +122,7 @@
fun proc_single prop =
let
- val frees = OldTerm.term_frees prop
+ val frees = Misc_Legacy.term_frees prop
val _ = forall (fn v => Sign.of_sort thy (type_of v,HOLogic.typeS)) frees
orelse error "Specificaton: Only free variables of sort 'type' allowed"
val prop_closed = close_form prop
--- a/src/HOL/Tools/cnf_funcs.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/HOL/Tools/cnf_funcs.ML Wed Aug 10 18:07:32 2011 -0700
@@ -511,7 +511,7 @@
NONE
in
Int.max (max, the_default 0 idx)
- end) (OldTerm.term_frees simp) 0)
+ end) (Misc_Legacy.term_frees simp) 0)
(* finally, convert to definitional CNF (this should preserve the simplification) *)
val cnfx_thm = make_under_quantifiers ctxt make_cnfx_thm_from_nnf simp
(*###
--- a/src/HOL/Tools/inductive_codegen.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/HOL/Tools/inductive_codegen.ML Wed Aug 10 18:07:32 2011 -0700
@@ -141,7 +141,7 @@
(fn (m, rnd) => string_of_mode m ^
(if rnd then " (random)" else "")) ms)) modes));
-val term_vs = map (fst o fst o dest_Var) o OldTerm.term_vars;
+val term_vs = map (fst o fst o dest_Var) o Misc_Legacy.term_vars;
val terms_vs = distinct (op =) o maps term_vs;
(** collect all Vars in a term (with duplicates!) **)
--- a/src/HOL/Tools/record.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/HOL/Tools/record.ML Wed Aug 10 18:07:32 2011 -0700
@@ -1512,7 +1512,7 @@
let
val ctxt' = fold (Variable.declare_typ o TFree) env ctxt;
val T = Syntax.read_typ ctxt' raw_T;
- val env' = OldTerm.add_typ_tfrees (T, env);
+ val env' = Misc_Legacy.add_typ_tfrees (T, env);
in (T, env') end;
fun cert_typ ctxt raw_T env =
@@ -1520,7 +1520,7 @@
val thy = Proof_Context.theory_of ctxt;
val T = Type.no_tvars (Sign.certify_typ thy raw_T)
handle TYPE (msg, _, _) => error msg;
- val env' = OldTerm.add_typ_tfrees (T, env);
+ val env' = Misc_Legacy.add_typ_tfrees (T, env);
in (T, env') end;
--- a/src/HOL/Tools/refute.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/HOL/Tools/refute.ML Wed Aug 10 18:07:32 2011 -0700
@@ -403,7 +403,7 @@
fun close_form t =
let
(* (Term.indexname * Term.typ) list *)
- val vars = sort_wrt (fst o fst) (map dest_Var (OldTerm.term_vars t))
+ val vars = sort_wrt (fst o fst) (map dest_Var (Misc_Legacy.term_vars t))
in
fold (fn ((x, i), T) => fn t' =>
Term.all T $ Abs (x, T, abstract_over (Var ((x, i), T), t'))) vars t
@@ -1212,7 +1212,7 @@
(* existential closure over schematic variables *)
(* (Term.indexname * Term.typ) list *)
- val vars = sort_wrt (fst o fst) (map dest_Var (OldTerm.term_vars t))
+ val vars = sort_wrt (fst o fst) (map dest_Var (Misc_Legacy.term_vars t))
(* Term.term *)
val ex_closure = fold (fn ((x, i), T) => fn t' =>
HOLogic.exists_const T $
--- a/src/HOL/Tools/split_rule.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/HOL/Tools/split_rule.ML Wed Aug 10 18:07:32 2011 -0700
@@ -88,7 +88,7 @@
(*curries ALL function variables occurring in a rule's conclusion*)
fun split_rule rl =
- fold_rev split_rule_var' (OldTerm.term_vars (concl_of rl)) rl
+ fold_rev split_rule_var' (Misc_Legacy.term_vars (concl_of rl)) rl
|> remove_internal_split
|> Drule.export_without_context;
--- a/src/Pure/Concurrent/bash.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/Pure/Concurrent/bash.ML Wed Aug 10 18:07:32 2011 -0700
@@ -73,7 +73,7 @@
in () end;
fun cleanup () =
- (Simple_Thread.interrupt system_thread;
+ (Simple_Thread.interrupt_unsynchronized system_thread;
try File.rm script_path;
try File.rm output_path;
try File.rm pid_path);
--- a/src/Pure/Concurrent/future.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/Pure/Concurrent/future.ML Wed Aug 10 18:07:32 2011 -0700
@@ -39,9 +39,13 @@
val task_of: 'a future -> Task_Queue.task
val peek: 'a future -> 'a Exn.result option
val is_finished: 'a future -> bool
- val forks:
- {name: string, group: Task_Queue.group option, deps: Task_Queue.task list, pri: int} ->
- (unit -> 'a) list -> 'a future list
+ val interruptible_task: ('a -> 'b) -> 'a -> 'b
+ val cancel_group: Task_Queue.group -> unit
+ val cancel: 'a future -> unit
+ type fork_params =
+ {name: string, group: Task_Queue.group option, deps: Task_Queue.task list,
+ pri: int, interrupts: bool}
+ val forks: fork_params -> (unit -> 'a) list -> 'a future list
val fork_pri: int -> (unit -> 'a) -> 'a future
val fork: (unit -> 'a) -> 'a future
val join_results: 'a future list -> 'a Exn.result list
@@ -49,16 +53,11 @@
val join: 'a future -> 'a
val value: 'a -> 'a future
val map: ('a -> 'b) -> 'a future -> 'b future
- val cond_forks:
- {name: string, group: Task_Queue.group option, deps: Task_Queue.task list, pri: int} ->
- (unit -> 'a) list -> 'a future list
+ val cond_forks: fork_params -> (unit -> 'a) list -> 'a future list
val promise_group: Task_Queue.group -> 'a future
val promise: unit -> 'a future
val fulfill_result: 'a future -> 'a Exn.result -> unit
val fulfill: 'a future -> 'a -> unit
- val interruptible_task: ('a -> 'b) -> 'a -> 'b
- val cancel_group: Task_Queue.group -> unit
- val cancel: 'a future -> unit
val shutdown: unit -> unit
val status: (unit -> 'a) -> 'a
end;
@@ -74,8 +73,7 @@
val tag = Universal.tag () : Task_Queue.task option Universal.tag;
in
fun worker_task () = the_default NONE (Thread.getLocal tag);
- fun setmp_worker_task data f x =
- Library.setmp_thread_data tag (worker_task ()) (SOME data) f x;
+ fun setmp_worker_task task f x = setmp_thread_data tag (worker_task ()) (SOME task) f x;
end;
val worker_group = Option.map Task_Queue.group_of_task o worker_task;
@@ -107,19 +105,6 @@
fun peek x = Single_Assignment.peek (result_of x);
fun is_finished x = is_some (peek x);
-fun assign_result group result res =
- let
- val _ = Single_Assignment.assign result res
- handle exn as Fail _ =>
- (case Single_Assignment.peek result of
- SOME (Exn.Exn e) => reraise (if Exn.is_interrupt e then e else exn)
- | _ => reraise exn);
- val ok =
- (case the (Single_Assignment.peek result) of
- Exn.Exn exn => (Task_Queue.cancel_group group exn; false)
- | Exn.Res _ => true);
- in ok end;
-
(** scheduling **)
@@ -173,23 +158,16 @@
fold (fn (_, state_ref) => fn i => if ! state_ref = state then i + 1 else i) (! workers) 0;
-(* execute future jobs *)
+(* cancellation primitives *)
-fun future_job group (e: unit -> 'a) =
- let
- val result = Single_Assignment.var "future" : 'a result;
- val pos = Position.thread_data ();
- fun job ok =
- let
- val res =
- if ok then
- Exn.capture (fn () =>
- Multithreading.with_attributes Multithreading.private_interrupts
- (fn _ => Position.setmp_thread_data pos e ()) before
- Multithreading.interrupted ()) ()
- else Exn.interrupt_exn;
- in assign_result group result res end;
- in (result, job) end;
+fun interruptible_task f x =
+ if Multithreading.available then
+ Multithreading.with_attributes
+ (if is_some (worker_task ())
+ then Multithreading.private_interrupts
+ else Multithreading.public_interrupts)
+ (fn _ => f x)
+ else interruptible f x;
fun cancel_now group = (*requires SYNCHRONIZED*)
Task_Queue.cancel (! queue) group;
@@ -198,7 +176,10 @@
(Unsynchronized.change canceled (insert Task_Queue.eq_group group);
broadcast scheduler_event);
-fun execute (task, jobs) =
+
+(* worker threads *)
+
+fun worker_exec (task, jobs) =
let
val group = Task_Queue.group_of_task task;
val valid = not (Task_Queue.is_canceled group);
@@ -215,6 +196,7 @@
val _ = SYNCHRONIZED "finish" (fn () =>
let
val maximal = Unsynchronized.change_result queue (Task_Queue.finish task);
+ val _ = Exn.capture Multithreading.interrupted ();
val _ =
if ok then ()
else if cancel_now group then ()
@@ -224,9 +206,6 @@
in () end);
in () end;
-
-(* worker threads *)
-
fun worker_wait active cond = (*requires SYNCHRONIZED*)
let
val state =
@@ -253,7 +232,7 @@
fun worker_loop name =
(case SYNCHRONIZED name (fn () => worker_next ()) of
NONE => ()
- | SOME work => (Exn.capture Multithreading.interrupted (); execute work; worker_loop name));
+ | SOME work => (Exn.capture Multithreading.interrupted (); worker_exec work; worker_loop name));
fun worker_start name = (*requires SYNCHRONIZED*)
Unsynchronized.change workers (cons (Simple_Thread.fork false (fn () => worker_loop name),
@@ -397,9 +376,58 @@
(** futures **)
+(* cancellation *)
+
+(*cancel: present and future group members will be interrupted eventually*)
+fun cancel_group group = SYNCHRONIZED "cancel" (fn () =>
+ (if cancel_now group then () else cancel_later group;
+ signal work_available; scheduler_check ()));
+
+fun cancel x = cancel_group (Task_Queue.group_of_task (task_of x));
+
+
+(* future jobs *)
+
+fun assign_result group result res =
+ let
+ val _ = Single_Assignment.assign result res
+ handle exn as Fail _ =>
+ (case Single_Assignment.peek result of
+ SOME (Exn.Exn e) => reraise (if Exn.is_interrupt e then e else exn)
+ | _ => reraise exn);
+ val ok =
+ (case the (Single_Assignment.peek result) of
+ Exn.Exn exn =>
+ (SYNCHRONIZED "cancel" (fn () => Task_Queue.cancel_group group exn); false)
+ | Exn.Res _ => true);
+ in ok end;
+
+fun future_job group interrupts (e: unit -> 'a) =
+ let
+ val result = Single_Assignment.var "future" : 'a result;
+ val pos = Position.thread_data ();
+ fun job ok =
+ let
+ val res =
+ if ok then
+ Exn.capture (fn () =>
+ Multithreading.with_attributes
+ (if interrupts
+ then Multithreading.private_interrupts else Multithreading.no_interrupts)
+ (fn _ => Position.setmp_thread_data pos e ()) before
+ Multithreading.interrupted ()) ()
+ else Exn.interrupt_exn;
+ in assign_result group result res end;
+ in (result, job) end;
+
+
(* fork *)
-fun forks {name, group, deps, pri} es =
+type fork_params =
+ {name: string, group: Task_Queue.group option, deps: Task_Queue.task list,
+ pri: int, interrupts: bool};
+
+fun forks ({name, group, deps, pri, interrupts}: fork_params) es =
if null es then []
else
let
@@ -409,7 +437,7 @@
| SOME grp => grp);
fun enqueue e queue =
let
- val (result, job) = future_job grp e;
+ val (result, job) = future_job grp interrupts e;
val (task, queue') = Task_Queue.enqueue name grp deps pri job queue;
val future = Future {promised = false, task = task, result = result};
in (future, queue') end;
@@ -424,7 +452,9 @@
in futures end)
end;
-fun fork_pri pri e = singleton (forks {name = "", group = NONE, deps = [], pri = pri}) e;
+fun fork_pri pri e =
+ singleton (forks {name = "", group = NONE, deps = [], pri = pri, interrupts = true}) e;
+
fun fork e = fork_pri 0 e;
@@ -452,7 +482,8 @@
| (SOME work, deps') => SOME (work, deps'));
fun execute_work NONE = ()
- | execute_work (SOME (work, deps')) = (worker_joining (fn () => execute work); join_work deps')
+ | execute_work (SOME (work, deps')) =
+ (worker_joining (fn () => worker_exec work); join_work deps')
and join_work deps =
Multithreading.with_attributes Multithreading.no_interrupts
(fn _ => execute_work (SYNCHRONIZED "join" (fn () => join_next deps)));
@@ -475,7 +506,7 @@
fun join x = Exn.release (join_result x);
-(* fast-path versions -- bypassing full task management *)
+(* fast-path versions -- bypassing task queue *)
fun value (x: 'a) =
let
@@ -489,7 +520,7 @@
let
val task = task_of x;
val group = Task_Queue.new_group (SOME (Task_Queue.group_of_task task));
- val (result, job) = future_job group (fn () => f (join x));
+ val (result, job) = future_job group true (fn () => f (join x));
val extended = SYNCHRONIZED "extend" (fn () =>
(case Task_Queue.extend task job (! queue) of
@@ -499,8 +530,8 @@
if extended then Future {promised = false, task = task, result = result}
else
singleton
- (forks {name = "Future.map", group = SOME group,
- deps = [task], pri = Task_Queue.pri_of_task task})
+ (forks {name = "Future.map", group = SOME group, deps = [task],
+ pri = Task_Queue.pri_of_task task, interrupts = true})
(fn () => f (join x))
end;
@@ -538,7 +569,7 @@
SYNCHRONIZED "fulfill_result" (fn () =>
Unsynchronized.change_result queue
(Task_Queue.dequeue_passive (Thread.self ()) task));
- in if still_passive then execute (task, [job]) else () end);
+ in if still_passive then worker_exec (task, [job]) else () end);
val _ =
if is_some (Single_Assignment.peek result) then ()
else worker_waiting [task] (fn () => ignore (Single_Assignment.await result));
@@ -547,25 +578,6 @@
fun fulfill x res = fulfill_result x (Exn.Res res);
-(* cancellation *)
-
-fun interruptible_task f x =
- if Multithreading.available then
- Multithreading.with_attributes
- (if is_some (worker_task ())
- then Multithreading.private_interrupts
- else Multithreading.public_interrupts)
- (fn _ => f x)
- else interruptible f x;
-
-(*cancel: present and future group members will be interrupted eventually*)
-fun cancel_group group = SYNCHRONIZED "cancel" (fn () =>
- (if cancel_now group then () else cancel_later group;
- signal work_available; scheduler_check ()));
-
-fun cancel x = cancel_group (Task_Queue.group_of_task (task_of x));
-
-
(* shutdown *)
fun shutdown () =
--- a/src/Pure/Concurrent/par_list.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/Pure/Concurrent/par_list.ML Wed Aug 10 18:07:32 2011 -0700
@@ -35,7 +35,7 @@
let
val group = Task_Queue.new_group (Future.worker_group ());
val futures =
- Future.forks {name = name, group = SOME group, deps = [], pri = 0}
+ Future.forks {name = name, group = SOME group, deps = [], pri = 0, interrupts = true}
(map (fn x => fn () => f x) xs);
val results = Future.join_results futures
handle exn => (if Exn.is_interrupt exn then Future.cancel_group group else (); reraise exn);
--- a/src/Pure/Concurrent/simple_thread.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/Pure/Concurrent/simple_thread.ML Wed Aug 10 18:07:32 2011 -0700
@@ -8,7 +8,7 @@
sig
val attributes: bool -> Thread.threadAttribute list
val fork: bool -> (unit -> unit) -> Thread.thread
- val interrupt: Thread.thread -> unit
+ val interrupt_unsynchronized: Thread.thread -> unit
val synchronized: string -> Mutex.mutex -> (unit -> 'a) -> 'a
end;
@@ -24,7 +24,7 @@
body () handle exn => if Exn.is_interrupt exn then () else reraise exn),
attributes interrupts);
-fun interrupt thread = Thread.interrupt thread handle Thread _ => ();
+fun interrupt_unsynchronized thread = Thread.interrupt thread handle Thread _ => ();
(* basic synchronization *)
--- a/src/Pure/Concurrent/task_queue.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/Pure/Concurrent/task_queue.ML Wed Aug 10 18:07:32 2011 -0700
@@ -247,7 +247,7 @@
val running =
Tasks.fold (#1 #> get_job jobs #> (fn Running t => insert Thread.equal t | _ => I))
(get_tasks groups (group_id group)) [];
- val _ = List.app Simple_Thread.interrupt running;
+ val _ = List.app Simple_Thread.interrupt_unsynchronized running;
in null running end;
fun cancel_all (Queue {jobs, ...}) =
@@ -262,7 +262,7 @@
| _ => (groups, running))
end;
val (running_groups, running) = Task_Graph.fold cancel_job jobs ([], []);
- val _ = List.app Simple_Thread.interrupt running;
+ val _ = List.app Simple_Thread.interrupt_unsynchronized running;
in running_groups end;
--- a/src/Pure/Concurrent/time_limit.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/Pure/Concurrent/time_limit.ML Wed Aug 10 18:07:32 2011 -0700
@@ -30,12 +30,12 @@
val main = Thread.self ();
val timeout = Unsynchronized.ref false;
val watchdog = Simple_Thread.fork true (fn () =>
- (OS.Process.sleep time; timeout := true; Thread.interrupt main));
+ (OS.Process.sleep time; timeout := true; Simple_Thread.interrupt_unsynchronized main));
val result =
Exn.capture (fn () => Multithreading.with_attributes orig_atts (fn _ => f x)) ();
- val _ = Thread.interrupt watchdog handle Thread _ => ();
+ val _ = Simple_Thread.interrupt_unsynchronized watchdog;
val _ = while Thread.isActive watchdog do OS.Process.sleep wait_time;
val test = Exn.capture Multithreading.interrupted ();
--- a/src/Pure/IsaMakefile Wed Aug 10 18:02:16 2011 -0700
+++ b/src/Pure/IsaMakefile Wed Aug 10 18:07:32 2011 -0700
@@ -210,7 +210,6 @@
Tools/xml_syntax.ML \
assumption.ML \
axclass.ML \
- codegen.ML \
config.ML \
conjunction.ML \
consts.ML \
@@ -233,7 +232,6 @@
morphism.ML \
name.ML \
net.ML \
- old_term.ML \
pattern.ML \
primitive_defs.ML \
proofterm.ML \
--- a/src/Pure/PIDE/document.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/Pure/PIDE/document.ML Wed Aug 10 18:07:32 2011 -0700
@@ -228,7 +228,7 @@
ignore
(singleton
(Future.forks {name = "Document.async_state",
- group = SOME (Task_Queue.new_group NONE), deps = [], pri = 0})
+ group = SOME (Task_Queue.new_group NONE), deps = [], pri = 0, interrupts = true})
(fn () =>
Toplevel.setmp_thread_position tr
(fn () => Toplevel.print_state false st) ()));
@@ -359,7 +359,8 @@
| force_exec (SOME exec_id) = ignore (Lazy.force (the_exec state exec_id));
val execution' = (* FIXME proper node deps *)
- Future.forks {name = "Document.execute", group = NONE, deps = [], pri = 1}
+ Future.forks
+ {name = "Document.execute", group = NONE, deps = [], pri = 1, interrupts = true}
[fn () =>
node_names_of version |> List.app (fn name =>
fold_entries NONE (fn (_, exec) => fn () => force_exec exec)
--- a/src/Pure/Proof/reconstruct.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/Pure/Proof/reconstruct.ML Wed Aug 10 18:07:32 2011 -0700
@@ -288,9 +288,9 @@
val _ = message "Collecting constraints...";
val (t, prf, cs, env, _) = make_constraints_cprf thy
(Envir.empty (Proofterm.maxidx_proof cprf ~1)) cprf';
- val cs' = map (fn p => (true, p, uncurry (union (op =))
- (pairself (map (fst o dest_Var) o OldTerm.term_vars) p)))
- (map (pairself (Envir.norm_term env)) ((t, prop')::cs));
+ val cs' =
+ map (pairself (Envir.norm_term env)) ((t, prop') :: cs)
+ |> map (fn p => (true, p, Term.add_var_names (#1 p) (Term.add_var_names (#2 p) [])));
val _ = message ("Solving remaining constraints (" ^ string_of_int (length cs') ^ ") ...");
val env' = solve thy cs' env
in
--- a/src/Pure/ROOT.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/Pure/ROOT.ML Wed Aug 10 18:07:32 2011 -0700
@@ -119,7 +119,6 @@
use "term_ord.ML";
use "term_subst.ML";
use "term_xml.ML";
-use "old_term.ML";
use "General/name_space.ML";
use "sorts.ML";
use "type.ML";
@@ -279,8 +278,6 @@
use "Tools/find_theorems.ML";
use "Tools/find_consts.ML";
-use "codegen.ML";
-
(* configuration for Proof General *)
--- a/src/Pure/Syntax/syntax.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/Pure/Syntax/syntax.ML Wed Aug 10 18:07:32 2011 -0700
@@ -489,7 +489,7 @@
fun future_gram deps e =
singleton
(Future.cond_forks {name = "Syntax.gram", group = NONE,
- deps = map Future.task_of deps, pri = 0}) e;
+ deps = map Future.task_of deps, pri = 0, interrupts = true}) e;
datatype syntax =
Syntax of {
--- a/src/Pure/System/isabelle_system.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/Pure/System/isabelle_system.ML Wed Aug 10 18:07:32 2011 -0700
@@ -96,7 +96,7 @@
(_, 0) => f path
| (out, _) => error (perhaps (try (unsuffix "\n")) out)));
-fun bash_output_fifo script f =
+fun bash_output_fifo script f = (* FIXME blocks on Cygwin 1.7.x *)
with_tmp_fifo (fn fifo =>
uninterruptible (fn restore_attributes => fn () =>
(case Bash.process (script ^ " > " ^ File.shell_path fifo ^ " &") of
--- a/src/Pure/Thy/thy_info.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/Pure/Thy/thy_info.ML Wed Aug 10 18:07:32 2011 -0700
@@ -205,7 +205,9 @@
val future =
singleton
- (Future.forks {name = "theory:" ^ name, group = NONE, deps = task_deps, pri = 0})
+ (Future.forks
+ {name = "theory:" ^ name, group = NONE, deps = task_deps, pri = 0,
+ interrupts = true})
(fn () =>
(case map_filter failed deps of
[] => body (map (#1 o Future.join o get) parents)
--- a/src/Pure/Thy/thy_load.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/Pure/Thy/thy_load.ML Wed Aug 10 18:07:32 2011 -0700
@@ -189,7 +189,7 @@
val present =
singleton (Future.cond_forks {name = "Outer_Syntax.present:" ^ name, group = NONE,
- deps = map Future.task_of results, pri = 0})
+ deps = map Future.task_of results, pri = 0, interrupts = true})
(fn () =>
Thy_Output.present_thy (#1 lexs) Keyword.command_tags
(Outer_Syntax.is_markup outer_syntax)
--- a/src/Pure/codegen.ML Wed Aug 10 18:02:16 2011 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1049 +0,0 @@
-(* Title: Pure/codegen.ML
- Author: Stefan Berghofer, TU Muenchen
-
-Generic code generator.
-*)
-
-signature CODEGEN =
-sig
- val quiet_mode : bool Unsynchronized.ref
- val message : string -> unit
- val margin : int Unsynchronized.ref
- val string_of : Pretty.T -> string
- val str : string -> Pretty.T
-
- datatype 'a mixfix =
- Arg
- | Ignore
- | Module
- | Pretty of Pretty.T
- | Quote of 'a;
-
- type deftab
- type node
- type codegr
- type 'a codegen
-
- val add_codegen: string -> term codegen -> theory -> theory
- val add_tycodegen: string -> typ codegen -> theory -> theory
- val add_preprocessor: (theory -> thm list -> thm list) -> theory -> theory
- val preprocess: theory -> thm list -> thm list
- val preprocess_term: theory -> term -> term
- val print_codegens: theory -> unit
- val generate_code: theory -> string list -> string list -> string -> (string * string) list ->
- (string * string) list * codegr
- val generate_code_i: theory -> string list -> string list -> string -> (string * term) list ->
- (string * string) list * codegr
- val assoc_const: string * (term mixfix list *
- (string * string) list) -> theory -> theory
- val assoc_const_i: (string * typ) * (term mixfix list *
- (string * string) list) -> theory -> theory
- val assoc_type: xstring * (typ mixfix list *
- (string * string) list) -> theory -> theory
- val get_assoc_code: theory -> string * typ ->
- (term mixfix list * (string * string) list) option
- val get_assoc_type: theory -> string ->
- (typ mixfix list * (string * string) list) option
- val codegen_error: codegr -> string -> string -> 'a
- val invoke_codegen: theory -> string list -> deftab -> string -> string -> bool ->
- term -> codegr -> Pretty.T * codegr
- val invoke_tycodegen: theory -> string list -> deftab -> string -> string -> bool ->
- typ -> codegr -> Pretty.T * codegr
- val mk_id: string -> string
- val mk_qual_id: string -> string * string -> string
- val mk_const_id: string -> string -> codegr -> (string * string) * codegr
- val get_const_id: codegr -> string -> string * string
- val mk_type_id: string -> string -> codegr -> (string * string) * codegr
- val get_type_id: codegr -> string -> string * string
- val thyname_of_type: theory -> string -> string
- val thyname_of_const: theory -> string -> string
- val rename_terms: term list -> term list
- val rename_term: term -> term
- val new_names: term -> string list -> string list
- val new_name: term -> string -> string
- val if_library: string list -> 'a -> 'a -> 'a
- val get_defn: theory -> deftab -> string -> typ ->
- ((typ * (string * thm)) * int option) option
- val is_instance: typ -> typ -> bool
- val parens: Pretty.T -> Pretty.T
- val mk_app: bool -> Pretty.T -> Pretty.T list -> Pretty.T
- val mk_tuple: Pretty.T list -> Pretty.T
- val mk_let: (Pretty.T * Pretty.T) list -> Pretty.T -> Pretty.T
- val eta_expand: term -> term list -> int -> term
- val strip_tname: string -> string
- val mk_type: bool -> typ -> Pretty.T
- val mk_term_of: codegr -> string -> bool -> typ -> Pretty.T
- val mk_gen: codegr -> string -> bool -> string list -> string -> typ -> Pretty.T
- val poke_test_fn: (int -> term list option) -> unit
- val poke_eval_fn: (unit -> term) -> unit
- val test_term: Proof.context -> term -> int -> term list option
- val eval_term: Proof.context -> term -> term
- val evaluation_conv: Proof.context -> conv
- val parse_mixfix: (string -> 'a) -> string -> 'a mixfix list
- val quotes_of: 'a mixfix list -> 'a list
- val num_args_of: 'a mixfix list -> int
- val replace_quotes: 'b list -> 'a mixfix list -> 'b mixfix list
- val mk_deftab: theory -> deftab
- val map_unfold: (simpset -> simpset) -> theory -> theory
- val add_unfold: thm -> theory -> theory
- val del_unfold: thm -> theory -> theory
-
- val get_node: codegr -> string -> node
- val add_edge: string * string -> codegr -> codegr
- val add_edge_acyclic: string * string -> codegr -> codegr
- val del_nodes: string list -> codegr -> codegr
- val map_node: string -> (node -> node) -> codegr -> codegr
- val new_node: string * node -> codegr -> codegr
-
- val setup: theory -> theory
-end;
-
-structure Codegen : CODEGEN =
-struct
-
-val quiet_mode = Unsynchronized.ref true;
-fun message s = if !quiet_mode then () else writeln s;
-
-val margin = Unsynchronized.ref 80;
-
-fun string_of p = Print_Mode.setmp [] (Pretty.string_of_margin (!margin)) p;
-
-val str = Print_Mode.setmp [] Pretty.str;
-
-(**** Mixfix syntax ****)
-
-datatype 'a mixfix =
- Arg
- | Ignore
- | Module
- | Pretty of Pretty.T
- | Quote of 'a;
-
-fun is_arg Arg = true
- | is_arg Ignore = true
- | is_arg _ = false;
-
-fun quotes_of [] = []
- | quotes_of (Quote q :: ms) = q :: quotes_of ms
- | quotes_of (_ :: ms) = quotes_of ms;
-
-fun args_of [] xs = ([], xs)
- | args_of (Arg :: ms) (x :: xs) = apfst (cons x) (args_of ms xs)
- | args_of (Ignore :: ms) (_ :: xs) = args_of ms xs
- | args_of (_ :: ms) xs = args_of ms xs;
-
-fun num_args_of x = length (filter is_arg x);
-
-
-(**** theory data ****)
-
-(* preprocessed definition table *)
-
-type deftab =
- (typ * (* type of constant *)
- (string * (* name of theory containing definition of constant *)
- thm)) (* definition theorem *)
- list Symtab.table;
-
-(* code dependency graph *)
-
-type nametab = (string * string) Symtab.table * unit Symtab.table;
-
-fun merge_nametabs ((tab, used) : nametab, (tab', used')) =
- (Symtab.merge op = (tab, tab'), Symtab.merge op = (used, used'));
-
-type node =
- (exn option * (* slot for arbitrary data *)
- string * (* name of structure containing piece of code *)
- string); (* piece of code *)
-
-type codegr =
- node Graph.T *
- (nametab * (* table for assigned constant names *)
- nametab); (* table for assigned type names *)
-
-val emptygr : codegr = (Graph.empty,
- ((Symtab.empty, Symtab.empty), (Symtab.empty, Symtab.empty)));
-
-(* type of code generators *)
-
-type 'a codegen =
- theory -> (* theory in which generate_code was called *)
- string list -> (* mode *)
- deftab -> (* definition table (for efficiency) *)
- string -> (* node name of caller (for recording dependencies) *)
- string -> (* module name of caller (for modular code generation) *)
- bool -> (* whether to parenthesize generated expression *)
- 'a -> (* item to generate code from *)
- codegr -> (* code dependency graph *)
- (Pretty.T * codegr) option;
-
-
-(* theory data *)
-
-structure CodegenData = Theory_Data
-(
- type T =
- {codegens : (string * term codegen) list,
- tycodegens : (string * typ codegen) list,
- consts : ((string * typ) * (term mixfix list * (string * string) list)) list,
- types : (string * (typ mixfix list * (string * string) list)) list,
- preprocs: (stamp * (theory -> thm list -> thm list)) list,
- modules: codegr Symtab.table};
-
- val empty =
- {codegens = [], tycodegens = [], consts = [], types = [],
- preprocs = [], modules = Symtab.empty};
- val extend = I;
-
- fun merge
- ({codegens = codegens1, tycodegens = tycodegens1,
- consts = consts1, types = types1,
- preprocs = preprocs1, modules = modules1} : T,
- {codegens = codegens2, tycodegens = tycodegens2,
- consts = consts2, types = types2,
- preprocs = preprocs2, modules = modules2}) : T =
- {codegens = AList.merge (op =) (K true) (codegens1, codegens2),
- tycodegens = AList.merge (op =) (K true) (tycodegens1, tycodegens2),
- consts = AList.merge (op =) (K true) (consts1, consts2),
- types = AList.merge (op =) (K true) (types1, types2),
- preprocs = AList.merge (op =) (K true) (preprocs1, preprocs2),
- modules = Symtab.merge (K true) (modules1, modules2)};
-);
-
-fun print_codegens thy =
- let val {codegens, tycodegens, ...} = CodegenData.get thy in
- Pretty.writeln (Pretty.chunks
- [Pretty.strs ("term code generators:" :: map fst codegens),
- Pretty.strs ("type code generators:" :: map fst tycodegens)])
- end;
-
-
-
-(**** access modules ****)
-
-fun get_modules thy = #modules (CodegenData.get thy);
-
-fun map_modules f thy =
- let val {codegens, tycodegens, consts, types, preprocs, modules} =
- CodegenData.get thy;
- in CodegenData.put {codegens = codegens, tycodegens = tycodegens,
- consts = consts, types = types, preprocs = preprocs,
- modules = f modules} thy
- end;
-
-
-(**** add new code generators to theory ****)
-
-fun add_codegen name f thy =
- let val {codegens, tycodegens, consts, types, preprocs, modules} =
- CodegenData.get thy
- in (case AList.lookup (op =) codegens name of
- NONE => CodegenData.put {codegens = (name, f) :: codegens,
- tycodegens = tycodegens, consts = consts, types = types,
- preprocs = preprocs, modules = modules} thy
- | SOME _ => error ("Code generator " ^ name ^ " already declared"))
- end;
-
-fun add_tycodegen name f thy =
- let val {codegens, tycodegens, consts, types, preprocs, modules} =
- CodegenData.get thy
- in (case AList.lookup (op =) tycodegens name of
- NONE => CodegenData.put {tycodegens = (name, f) :: tycodegens,
- codegens = codegens, consts = consts, types = types,
- preprocs = preprocs, modules = modules} thy
- | SOME _ => error ("Code generator " ^ name ^ " already declared"))
- end;
-
-
-(**** preprocessors ****)
-
-fun add_preprocessor p thy =
- let val {codegens, tycodegens, consts, types, preprocs, modules} =
- CodegenData.get thy
- in CodegenData.put {tycodegens = tycodegens,
- codegens = codegens, consts = consts, types = types,
- preprocs = (stamp (), p) :: preprocs,
- modules = modules} thy
- end;
-
-fun preprocess thy =
- let val {preprocs, ...} = CodegenData.get thy
- in fold (fn (_, f) => f thy) preprocs end;
-
-fun preprocess_term thy t =
- let
- val x = Free (singleton (Name.variant_list (OldTerm.add_term_names (t, []))) "x", fastype_of t);
- (* fake definition *)
- val eq = Skip_Proof.make_thm thy (Logic.mk_equals (x, t));
- fun err () = error "preprocess_term: bad preprocessor"
- in case map prop_of (preprocess thy [eq]) of
- [Const ("==", _) $ x' $ t'] => if x = x' then t' else err ()
- | _ => err ()
- end;
-
-structure UnfoldData = Theory_Data
-(
- type T = simpset;
- val empty = empty_ss;
- val extend = I;
- val merge = merge_ss;
-);
-
-val map_unfold = UnfoldData.map;
-val add_unfold = map_unfold o Simplifier.add_simp;
-val del_unfold = map_unfold o Simplifier.del_simp;
-
-fun unfold_preprocessor thy =
- let val ss = Simplifier.global_context thy (UnfoldData.get thy)
- in map (Thm.transfer thy #> Simplifier.full_simplify ss) end;
-
-
-(**** associate constants with target language code ****)
-
-fun gen_assoc_const prep_const (raw_const, syn) thy =
- let
- val {codegens, tycodegens, consts, types, preprocs, modules} =
- CodegenData.get thy;
- val (cname, T) = prep_const thy raw_const;
- in
- if num_args_of (fst syn) > length (binder_types T) then
- error ("More arguments than in corresponding type of " ^ cname)
- else case AList.lookup (op =) consts (cname, T) of
- NONE => CodegenData.put {codegens = codegens,
- tycodegens = tycodegens,
- consts = ((cname, T), syn) :: consts,
- types = types, preprocs = preprocs,
- modules = modules} thy
- | SOME _ => error ("Constant " ^ cname ^ " already associated with code")
- end;
-
-val assoc_const_i = gen_assoc_const (K I);
-val assoc_const = gen_assoc_const Code.read_bare_const;
-
-
-(**** associate types with target language types ****)
-
-fun assoc_type (s, syn) thy =
- let
- val {codegens, tycodegens, consts, types, preprocs, modules} =
- CodegenData.get thy;
- val tc = Sign.intern_type thy s;
- in
- case Symtab.lookup (snd (#types (Type.rep_tsig (Sign.tsig_of thy)))) tc of
- SOME (Type.LogicalType i) =>
- if num_args_of (fst syn) > i then
- error ("More arguments than corresponding type constructor " ^ s)
- else
- (case AList.lookup (op =) types tc of
- NONE => CodegenData.put {codegens = codegens,
- tycodegens = tycodegens, consts = consts,
- types = (tc, syn) :: types,
- preprocs = preprocs, modules = modules} thy
- | SOME _ => error ("Type " ^ tc ^ " already associated with code"))
- | _ => error ("Not a type constructor: " ^ s)
- end;
-
-fun get_assoc_type thy = AList.lookup (op =) ((#types o CodegenData.get) thy);
-
-
-(**** make valid ML identifiers ****)
-
-fun is_ascii_letdig x = Symbol.is_ascii_letter x orelse
- Symbol.is_ascii_digit x orelse Symbol.is_ascii_quasi x;
-
-fun dest_sym s =
- (case split_last (snd (take_prefix (fn c => c = "\\") (raw_explode s))) of
- ("<" :: "^" :: xs, ">") => (true, implode xs)
- | ("<" :: xs, ">") => (false, implode xs)
- | _ => raise Fail "dest_sym");
-
-fun mk_id s = if s = "" then "" else
- let
- fun check_str [] = []
- | check_str xs = (case take_prefix is_ascii_letdig xs of
- ([], " " :: zs) => check_str zs
- | ([], z :: zs) =>
- if size z = 1 then string_of_int (ord z) :: check_str zs
- else (case dest_sym z of
- (true, "isub") => check_str zs
- | (true, "isup") => "" :: check_str zs
- | (ctrl, s') => (if ctrl then "ctrl_" ^ s' else s') :: check_str zs)
- | (ys, zs) => implode ys :: check_str zs);
- val s' = space_implode "_" (maps (check_str o Symbol.explode) (Long_Name.explode s))
- in
- if Symbol.is_ascii_letter (hd (raw_explode s')) then s' else "id_" ^ s'
- end;
-
-fun mk_long_id (p as (tab, used)) module s =
- let
- fun find_name [] = raise Fail "mk_long_id"
- | find_name (ys :: yss) =
- let
- val s' = Long_Name.implode ys
- val s'' = Long_Name.append module s'
- in case Symtab.lookup used s'' of
- NONE => ((module, s'),
- (Symtab.update_new (s, (module, s')) tab,
- Symtab.update_new (s'', ()) used))
- | SOME _ => find_name yss
- end
- in case Symtab.lookup tab s of
- NONE => find_name (Library.suffixes1 (Long_Name.explode s))
- | SOME name => (name, p)
- end;
-
-(* module: module name for caller *)
-(* module': module name for callee *)
-(* if caller and callee reside in different modules, use qualified access *)
-
-fun mk_qual_id module (module', s) =
- if module = module' orelse module' = "" then s else module' ^ "." ^ s;
-
-fun mk_const_id module cname (gr, (tab1, tab2)) =
- let
- val ((module, s), tab1') = mk_long_id tab1 module cname
- val s' = mk_id s;
- val s'' = if ML_Syntax.is_reserved s' then s' ^ "_const" else s'
- in (((module, s'')), (gr, (tab1', tab2))) end;
-
-fun get_const_id (gr, (tab1, tab2)) cname =
- case Symtab.lookup (fst tab1) cname of
- NONE => error ("get_const_id: no such constant: " ^ quote cname)
- | SOME (module, s) =>
- let
- val s' = mk_id s;
- val s'' = if ML_Syntax.is_reserved s' then s' ^ "_const" else s'
- in (module, s'') end;
-
-fun mk_type_id module tyname (gr, (tab1, tab2)) =
- let
- val ((module, s), tab2') = mk_long_id tab2 module tyname
- val s' = mk_id s;
- val s'' = if ML_Syntax.is_reserved s' then s' ^ "_type" else s'
- in ((module, s''), (gr, (tab1, tab2'))) end;
-
-fun get_type_id (gr, (tab1, tab2)) tyname =
- case Symtab.lookup (fst tab2) tyname of
- NONE => error ("get_type_id: no such type: " ^ quote tyname)
- | SOME (module, s) =>
- let
- val s' = mk_id s;
- val s'' = if ML_Syntax.is_reserved s' then s' ^ "_type" else s'
- in (module, s'') end;
-
-fun get_type_id' f tab tyname = apsnd f (get_type_id tab tyname);
-
-fun get_node (gr, x) k = Graph.get_node gr k;
-fun add_edge e (gr, x) = (Graph.add_edge e gr, x);
-fun add_edge_acyclic e (gr, x) = (Graph.add_edge_acyclic e gr, x);
-fun del_nodes ks (gr, x) = (Graph.del_nodes ks gr, x);
-fun map_node k f (gr, x) = (Graph.map_node k f gr, x);
-fun new_node p (gr, x) = (Graph.new_node p gr, x);
-
-fun thyname_of_type thy = #theory_name o Name_Space.the_entry (Sign.type_space thy);
-fun thyname_of_const thy = #theory_name o Name_Space.the_entry (Sign.const_space thy);
-
-fun rename_terms ts =
- let
- val names = List.foldr OldTerm.add_term_names
- (map (fst o fst) (rev (fold Term.add_vars ts []))) ts;
- val reserved = filter ML_Syntax.is_reserved names;
- val (illegal, alt_names) = split_list (map_filter (fn s =>
- let val s' = mk_id s in if s = s' then NONE else SOME (s, s') end) names)
- val ps = (reserved @ illegal) ~~
- Name.variant_list names (map (suffix "'") reserved @ alt_names);
-
- fun rename_id s = AList.lookup (op =) ps s |> the_default s;
-
- fun rename (Var ((a, i), T)) = Var ((rename_id a, i), T)
- | rename (Free (a, T)) = Free (rename_id a, T)
- | rename (Abs (s, T, t)) = Abs (s, T, rename t)
- | rename (t $ u) = rename t $ rename u
- | rename t = t;
- in
- map rename ts
- end;
-
-val rename_term = hd o rename_terms o single;
-
-
-(**** retrieve definition of constant ****)
-
-fun is_instance T1 T2 =
- Type.raw_instance (T1, if null (OldTerm.typ_tfrees T2) then T2 else Logic.varifyT_global T2);
-
-fun get_assoc_code thy (s, T) = Option.map snd (find_first (fn ((s', T'), _) =>
- s = s' andalso is_instance T T') (#consts (CodegenData.get thy)));
-
-fun get_aux_code mode xs = map_filter (fn (m, code) =>
- if m = "" orelse member (op =) mode m then SOME code else NONE) xs;
-
-fun dest_prim_def t =
- let
- val (lhs, rhs) = Logic.dest_equals t;
- val (c, args) = strip_comb lhs;
- val (s, T) = dest_Const c
- in if forall is_Var args then SOME (s, (T, (args, rhs))) else NONE
- end handle TERM _ => NONE;
-
-fun mk_deftab thy =
- let
- val axmss =
- map (fn thy' => (Context.theory_name thy', Theory.axiom_table thy'))
- (Theory.nodes_of thy);
- fun add_def thyname (name, t) =
- (case dest_prim_def t of
- NONE => I
- | SOME (s, (T, _)) => Symtab.map_default (s, [])
- (cons (T, (thyname, Thm.axiom thy name))));
- in
- fold (fn (thyname, axms) => Symtab.fold (add_def thyname) axms) axmss Symtab.empty
- end;
-
-fun prep_prim_def thy thm =
- let
- val prop = case preprocess thy [thm]
- of [thm'] => Thm.prop_of thm'
- | _ => error "mk_deftab: bad preprocessor"
- in ((Option.map o apsnd o apsnd)
- (fn (args, rhs) => split_last (rename_terms (args @ [rhs]))) o dest_prim_def) prop
- end;
-
-fun get_defn thy defs s T = (case Symtab.lookup defs s of
- NONE => NONE
- | SOME ds =>
- let val i = find_index (is_instance T o fst) ds
- in if i >= 0 then
- SOME (nth ds i, if length ds = 1 then NONE else SOME i)
- else NONE
- end);
-
-
-(**** invoke suitable code generator for term / type ****)
-
-fun codegen_error (gr, _) dep s =
- error (s ^ "\nrequired by:\n" ^ commas (Graph.all_succs gr [dep]));
-
-fun invoke_codegen thy mode defs dep module brack t gr = (case get_first
- (fn (_, f) => f thy mode defs dep module brack t gr) (#codegens (CodegenData.get thy)) of
- NONE => codegen_error gr dep ("Unable to generate code for term:\n" ^
- Syntax.string_of_term_global thy t)
- | SOME x => x);
-
-fun invoke_tycodegen thy mode defs dep module brack T gr = (case get_first
- (fn (_, f) => f thy mode defs dep module brack T gr ) (#tycodegens (CodegenData.get thy)) of
- NONE => codegen_error gr dep ("Unable to generate code for type:\n" ^
- Syntax.string_of_typ_global thy T)
- | SOME x => x);
-
-
-(**** code generator for mixfix expressions ****)
-
-fun parens p = Pretty.block [str "(", p, str ")"];
-
-fun pretty_fn [] p = [p]
- | pretty_fn (x::xs) p = str ("fn " ^ x ^ " =>") ::
- Pretty.brk 1 :: pretty_fn xs p;
-
-fun pretty_mixfix _ _ [] [] _ = []
- | pretty_mixfix module module' (Arg :: ms) (p :: ps) qs =
- p :: pretty_mixfix module module' ms ps qs
- | pretty_mixfix module module' (Ignore :: ms) ps qs =
- pretty_mixfix module module' ms ps qs
- | pretty_mixfix module module' (Module :: ms) ps qs =
- (if module <> module'
- then cons (str (module' ^ ".")) else I)
- (pretty_mixfix module module' ms ps qs)
- | pretty_mixfix module module' (Pretty p :: ms) ps qs =
- p :: pretty_mixfix module module' ms ps qs
- | pretty_mixfix module module' (Quote _ :: ms) ps (q :: qs) =
- q :: pretty_mixfix module module' ms ps qs;
-
-fun replace_quotes [] [] = []
- | replace_quotes xs (Arg :: ms) =
- Arg :: replace_quotes xs ms
- | replace_quotes xs (Ignore :: ms) =
- Ignore :: replace_quotes xs ms
- | replace_quotes xs (Module :: ms) =
- Module :: replace_quotes xs ms
- | replace_quotes xs (Pretty p :: ms) =
- Pretty p :: replace_quotes xs ms
- | replace_quotes (x::xs) (Quote _ :: ms) =
- Quote x :: replace_quotes xs ms;
-
-
-(**** default code generators ****)
-
-fun eta_expand t ts i =
- let
- val k = length ts;
- val Ts = drop k (binder_types (fastype_of t));
- val j = i - k
- in
- List.foldr (fn (T, t) => Abs ("x", T, t))
- (list_comb (t, ts @ map Bound (j-1 downto 0))) (take j Ts)
- end;
-
-fun mk_app _ p [] = p
- | mk_app brack p ps = if brack then
- Pretty.block (str "(" ::
- separate (Pretty.brk 1) (p :: ps) @ [str ")"])
- else Pretty.block (separate (Pretty.brk 1) (p :: ps));
-
-fun new_names t xs = Name.variant_list
- (union (op =) (map (fst o fst o dest_Var) (OldTerm.term_vars t))
- (OldTerm.add_term_names (t, ML_Syntax.reserved_names))) (map mk_id xs);
-
-fun new_name t x = hd (new_names t [x]);
-
-fun if_library mode x y = if member (op =) mode "library" then x else y;
-
-fun default_codegen thy mode defs dep module brack t gr =
- let
- val (u, ts) = strip_comb t;
- fun codegens brack = fold_map (invoke_codegen thy mode defs dep module brack)
- in (case u of
- Var ((s, i), T) =>
- let
- val (ps, gr') = codegens true ts gr;
- val (_, gr'') = invoke_tycodegen thy mode defs dep module false T gr'
- in SOME (mk_app brack (str (s ^
- (if i=0 then "" else string_of_int i))) ps, gr'')
- end
-
- | Free (s, T) =>
- let
- val (ps, gr') = codegens true ts gr;
- val (_, gr'') = invoke_tycodegen thy mode defs dep module false T gr'
- in SOME (mk_app brack (str s) ps, gr'') end
-
- | Const (s, T) =>
- (case get_assoc_code thy (s, T) of
- SOME (ms, aux) =>
- let val i = num_args_of ms
- in if length ts < i then
- default_codegen thy mode defs dep module brack (eta_expand u ts i) gr
- else
- let
- val (ts1, ts2) = args_of ms ts;
- val (ps1, gr1) = codegens false ts1 gr;
- val (ps2, gr2) = codegens true ts2 gr1;
- val (ps3, gr3) = codegens false (quotes_of ms) gr2;
- val (_, gr4) = invoke_tycodegen thy mode defs dep module false
- (funpow (length ts) (hd o tl o snd o dest_Type) T) gr3;
- val (module', suffix) = (case get_defn thy defs s T of
- NONE => (if_library mode (thyname_of_const thy s) module, "")
- | SOME ((U, (module', _)), NONE) =>
- (if_library mode module' module, "")
- | SOME ((U, (module', _)), SOME i) =>
- (if_library mode module' module, " def" ^ string_of_int i));
- val node_id = s ^ suffix;
- fun p module' = mk_app brack (Pretty.block
- (pretty_mixfix module module' ms ps1 ps3)) ps2
- in SOME (case try (get_node gr4) node_id of
- NONE => (case get_aux_code mode aux of
- [] => (p module, gr4)
- | xs => (p module', add_edge (node_id, dep) (new_node
- (node_id, (NONE, module', cat_lines xs ^ "\n")) gr4)))
- | SOME (_, module'', _) =>
- (p module'', add_edge (node_id, dep) gr4))
- end
- end
- | NONE => (case get_defn thy defs s T of
- NONE => NONE
- | SOME ((U, (thyname, thm)), k) => (case prep_prim_def thy thm
- of SOME (_, (_, (args, rhs))) => let
- val module' = if_library mode thyname module;
- val suffix = (case k of NONE => "" | SOME i => " def" ^ string_of_int i);
- val node_id = s ^ suffix;
- val ((ps, def_id), gr') = gr |> codegens true ts
- ||>> mk_const_id module' (s ^ suffix);
- val p = mk_app brack (str (mk_qual_id module def_id)) ps
- in SOME (case try (get_node gr') node_id of
- NONE =>
- let
- val _ = message ("expanding definition of " ^ s);
- val Ts = binder_types U;
- val (args', rhs') =
- if not (null args) orelse null Ts then (args, rhs) else
- let val v = Free (new_name rhs "x", hd Ts)
- in ([v], betapply (rhs, v)) end;
- val (p', gr1) = invoke_codegen thy mode defs node_id module' false
- rhs' (add_edge (node_id, dep)
- (new_node (node_id, (NONE, "", "")) gr'));
- val (xs, gr2) = codegens false args' gr1;
- val (_, gr3) = invoke_tycodegen thy mode defs dep module false T gr2;
- val (ty, gr4) = invoke_tycodegen thy mode defs node_id module' false U gr3;
- in (p, map_node node_id (K (NONE, module', string_of
- (Pretty.block (separate (Pretty.brk 1)
- (if null args' then
- [str ("val " ^ snd def_id ^ " :"), ty]
- else str ("fun " ^ snd def_id) :: xs) @
- [str " =", Pretty.brk 1, p', str ";"])) ^ "\n\n")) gr4)
- end
- | SOME _ => (p, add_edge (node_id, dep) gr'))
- end
- | NONE => NONE)))
-
- | Abs _ =>
- let
- val (bs, Ts) = ListPair.unzip (strip_abs_vars u);
- val t = strip_abs_body u
- val bs' = new_names t bs;
- val (ps, gr1) = codegens true ts gr;
- val (p, gr2) = invoke_codegen thy mode defs dep module false
- (subst_bounds (map Free (rev (bs' ~~ Ts)), t)) gr1;
- in
- SOME (mk_app brack (Pretty.block (str "(" :: pretty_fn bs' p @
- [str ")"])) ps, gr2)
- end
-
- | _ => NONE)
- end;
-
-fun default_tycodegen thy mode defs dep module brack (TVar ((s, i), _)) gr =
- SOME (str (s ^ (if i = 0 then "" else string_of_int i)), gr)
- | default_tycodegen thy mode defs dep module brack (TFree (s, _)) gr =
- SOME (str s, gr)
- | default_tycodegen thy mode defs dep module brack (Type (s, Ts)) gr =
- (case AList.lookup (op =) ((#types o CodegenData.get) thy) s of
- NONE => NONE
- | SOME (ms, aux) =>
- let
- val (ps, gr') = fold_map
- (invoke_tycodegen thy mode defs dep module false)
- (fst (args_of ms Ts)) gr;
- val (qs, gr'') = fold_map
- (invoke_tycodegen thy mode defs dep module false)
- (quotes_of ms) gr';
- val module' = if_library mode (thyname_of_type thy s) module;
- val node_id = s ^ " (type)";
- fun p module' = Pretty.block (pretty_mixfix module module' ms ps qs)
- in SOME (case try (get_node gr'') node_id of
- NONE => (case get_aux_code mode aux of
- [] => (p module', gr'')
- | xs => (p module', snd (mk_type_id module' s
- (add_edge (node_id, dep) (new_node (node_id,
- (NONE, module', cat_lines xs ^ "\n")) gr'')))))
- | SOME (_, module'', _) =>
- (p module'', add_edge (node_id, dep) gr''))
- end);
-
-fun mk_tuple [p] = p
- | mk_tuple ps = Pretty.block (str "(" ::
- flat (separate [str ",", Pretty.brk 1] (map single ps)) @ [str ")"]);
-
-fun mk_let bindings body =
- Pretty.blk (0, [str "let", Pretty.brk 1,
- Pretty.blk (0, separate Pretty.fbrk (map (fn (pat, rhs) =>
- Pretty.block [str "val ", pat, str " =", Pretty.brk 1,
- rhs, str ";"]) bindings)),
- Pretty.brk 1, str "in", Pretty.brk 1, body,
- Pretty.brk 1, str "end"]);
-
-fun mk_struct name s = "structure " ^ name ^ " =\nstruct\n\n" ^ s ^ "end;\n";
-
-fun add_to_module name s = AList.map_entry (op =) (name : string) (suffix s);
-
-fun output_code gr module xs =
- let
- val code = map_filter (fn s =>
- let val c as (_, module', _) = Graph.get_node gr s
- in if module = "" orelse module = module' then SOME (s, c) else NONE end)
- (rev (Graph.all_preds gr xs));
- fun string_of_cycle (a :: b :: cs) =
- let val SOME (x, y) = get_first (fn (x, (_, a', _)) =>
- if a = a' then Option.map (pair x)
- (find_first ((fn (_, b', _) => b' = b) o Graph.get_node gr)
- (Graph.imm_succs gr x))
- else NONE) code
- in x ^ " called by " ^ y ^ "\n" ^ string_of_cycle (b :: cs) end
- | string_of_cycle _ = ""
- in
- if module = "" then
- let
- val modules = distinct (op =) (map (#2 o snd) code);
- val mod_gr = fold_rev Graph.add_edge_acyclic
- (maps (fn (s, (_, module, _)) => map (pair module)
- (filter_out (fn s => s = module) (map (#2 o Graph.get_node gr)
- (Graph.imm_succs gr s)))) code)
- (fold_rev (Graph.new_node o rpair ()) modules Graph.empty);
- val modules' =
- rev (Graph.all_preds mod_gr (map (#2 o Graph.get_node gr) xs))
- in
- List.foldl (fn ((_, (_, module, s)), ms) => add_to_module module s ms)
- (map (rpair "") modules') code
- end handle Graph.CYCLES (cs :: _) =>
- error ("Cyclic dependency of modules:\n" ^ commas cs ^
- "\n" ^ string_of_cycle cs)
- else [(module, implode (map (#3 o snd) code))]
- end;
-
-fun gen_generate_code prep_term thy mode modules module xs =
- let
- val _ = (module <> "" orelse
- member (op =) mode "library" andalso forall (fn (s, _) => s = "") xs)
- orelse error "missing module name";
- val graphs = get_modules thy;
- val defs = mk_deftab thy;
- val gr = new_node ("<Top>", (NONE, module, ""))
- (List.foldl (fn ((gr, (tab1, tab2)), (gr', (tab1', tab2'))) =>
- (Graph.merge (fn ((_, module, _), (_, module', _)) =>
- module = module') (gr, gr'),
- (merge_nametabs (tab1, tab1'), merge_nametabs (tab2, tab2')))) emptygr
- (map (fn s => case Symtab.lookup graphs s of
- NONE => error ("Undefined code module: " ^ s)
- | SOME gr => gr) modules))
- handle Graph.DUP k => error ("Duplicate code for " ^ k);
- fun expand (t as Abs _) = t
- | expand t = (case fastype_of t of
- Type ("fun", [T, U]) => Abs ("x", T, t $ Bound 0) | _ => t);
- val (ps, gr') = fold_map (fn (s, t) => fn gr => apfst (pair s)
- (invoke_codegen thy mode defs "<Top>" module false t gr))
- (map (apsnd (expand o preprocess_term thy o prep_term thy)) xs) gr;
- val code = map_filter
- (fn ("", _) => NONE
- | (s', p) => SOME (string_of (Pretty.block
- [str ("val " ^ s' ^ " ="), Pretty.brk 1, p, str ";"]))) ps;
- val code' = space_implode "\n\n" code ^ "\n\n";
- val code'' =
- map_filter (fn (name, s) =>
- if member (op =) mode "library" andalso name = module andalso null code
- then NONE
- else SOME (name, mk_struct name s))
- ((if null code then I
- else add_to_module module code')
- (output_code (fst gr') (if_library mode "" module) ["<Top>"]))
- in
- (code'', del_nodes ["<Top>"] gr')
- end;
-
-val generate_code_i = gen_generate_code Sign.cert_term;
-val generate_code =
- gen_generate_code (Syntax.read_term o Proof_Context.allow_dummies o Proof_Context.init_global);
-
-
-(**** Reflection ****)
-
-val strip_tname = implode o tl o raw_explode;
-
-fun pretty_list xs = Pretty.block (str "[" ::
- flat (separate [str ",", Pretty.brk 1] (map single xs)) @
- [str "]"]);
-
-fun mk_type p (TVar ((s, i), _)) = str
- (strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "T")
- | mk_type p (TFree (s, _)) = str (strip_tname s ^ "T")
- | mk_type p (Type (s, Ts)) = (if p then parens else I) (Pretty.block
- [str "Type", Pretty.brk 1, str ("(\"" ^ s ^ "\","),
- Pretty.brk 1, pretty_list (map (mk_type false) Ts), str ")"]);
-
-fun mk_term_of gr module p (TVar ((s, i), _)) = str
- (strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "F")
- | mk_term_of gr module p (TFree (s, _)) = str (strip_tname s ^ "F")
- | mk_term_of gr module p (Type (s, Ts)) = (if p then parens else I)
- (Pretty.block (separate (Pretty.brk 1)
- (str (mk_qual_id module
- (get_type_id' (fn s' => "term_of_" ^ s') gr s)) ::
- maps (fn T =>
- [mk_term_of gr module true T, mk_type true T]) Ts)));
-
-
-(**** Implicit results ****)
-
-structure Result = Proof_Data
-(
- type T = (int -> term list option) * (unit -> term);
- fun init _ = (fn _ => NONE, fn () => Bound 0);
-);
-
-val get_test_fn = #1 o Result.get;
-val get_eval_fn = #2 o Result.get;
-
-fun poke_test_fn f = Context.>> (Context.map_proof (Result.map (fn (_, g) => (f, g))));
-fun poke_eval_fn g = Context.>> (Context.map_proof (Result.map (fn (f, _) => (f, g))));
-
-
-(**** Test data generators ****)
-
-fun mk_gen gr module p xs a (TVar ((s, i), _)) = str
- (strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "G")
- | mk_gen gr module p xs a (TFree (s, _)) = str (strip_tname s ^ "G")
- | mk_gen gr module p xs a (Type (tyc as (s, Ts))) = (if p then parens else I)
- (Pretty.block (separate (Pretty.brk 1)
- (str (mk_qual_id module (get_type_id' (fn s' => "gen_" ^ s') gr s) ^
- (if member (op =) xs s then "'" else "")) ::
- (case tyc of
- ("fun", [T, U]) =>
- [mk_term_of gr module true T, mk_type true T,
- mk_gen gr module true xs a U, mk_type true U]
- | _ => maps (fn T =>
- [mk_gen gr module true xs a T, mk_type true T]) Ts) @
- (if member (op =) xs s then [str a] else []))));
-
-fun test_term ctxt t =
- let
- val thy = Proof_Context.theory_of ctxt;
- val (code, gr) = generate_code_i thy ["term_of", "test"] [] "Generated" [("testf", t)];
- val Ts = map snd (fst (strip_abs t));
- val args = map_index (fn (i, T) => ("arg" ^ string_of_int i, T)) Ts;
- val s = "structure Test_Term =\nstruct\n\n" ^
- cat_lines (map snd code) ^
- "\nopen Generated;\n\n" ^ string_of
- (Pretty.block [str "val () = Codegen.poke_test_fn",
- Pretty.brk 1, str ("(fn i =>"), Pretty.brk 1,
- mk_let (map (fn (s, T) =>
- (mk_tuple [str s, str (s ^ "_t")],
- Pretty.block [mk_gen gr "Generated" false [] "" T, Pretty.brk 1,
- str "i"])) args)
- (Pretty.block [str "if ",
- mk_app false (str "testf") (map (str o fst) args),
- Pretty.brk 1, str "then NONE",
- Pretty.brk 1, str "else ",
- Pretty.block [str "SOME ",
- Pretty.enum "," "[" "]" (map (fn (s, _) => str (s ^ "_t ()")) args)]]),
- str ");"]) ^
- "\n\nend;\n";
- in
- ctxt
- |> Context.proof_map (ML_Context.exec (fn () => ML_Context.eval_text false Position.none s))
- |> get_test_fn
- end;
-
-
-(**** Evaluator for terms ****)
-
-fun eval_term ctxt t =
- let
- val _ =
- legacy_feature
- "Old evaluation mechanism -- use evaluator \"code\" or method \"eval\" instead";
- val thy = Proof_Context.theory_of ctxt;
- val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse
- error "Term to be evaluated contains type variables";
- val _ = (null (Term.add_vars t []) andalso null (Term.add_frees t [])) orelse
- error "Term to be evaluated contains variables";
- val (code, gr) =
- generate_code_i thy ["term_of"] [] "Generated"
- [("result", Abs ("x", TFree ("'a", []), t))];
- val s = "structure Eval_Term =\nstruct\n\n" ^
- cat_lines (map snd code) ^
- "\nopen Generated;\n\n" ^ string_of
- (Pretty.block [str "val () = Codegen.poke_eval_fn (fn () =>",
- Pretty.brk 1,
- mk_app false (mk_term_of gr "Generated" false (fastype_of t))
- [str "(result ())"],
- str ");"]) ^
- "\n\nend;\n";
- val eval_fn =
- ctxt
- |> Context.proof_map (ML_Context.exec (fn () => ML_Context.eval_text false Position.none s))
- |> get_eval_fn;
- in eval_fn () end;
-
-val (_, evaluation_oracle) = Context.>>> (Context.map_theory_result
- (Thm.add_oracle (Binding.name "evaluation", fn (ctxt, ct) =>
- let
- val thy = Proof_Context.theory_of ctxt;
- val t = Thm.term_of ct;
- in
- if Theory.subthy (Thm.theory_of_cterm ct, thy) then
- Thm.cterm_of thy (Logic.mk_equals (t, eval_term ctxt t))
- else raise CTERM ("evaluation_oracle: bad theory", [ct])
- end)));
-
-fun evaluation_conv ctxt ct = evaluation_oracle (ctxt, ct);
-
-
-(**** Interface ****)
-
-fun parse_mixfix rd s =
- (case Scan.finite Symbol.stopper (Scan.repeat
- ( $$ "_" >> K Arg
- || $$ "?" >> K Ignore
- || $$ "\\<module>" >> K Module
- || $$ "/" |-- Scan.repeat ($$ " ") >> (Pretty o Pretty.brk o length)
- || $$ "{" |-- $$ "*" |-- Scan.repeat1
- ( $$ "'" |-- Scan.one Symbol.is_regular
- || Scan.unless ($$ "*" -- $$ "}") (Scan.one Symbol.is_regular)) --|
- $$ "*" --| $$ "}" >> (Quote o rd o implode)
- || Scan.repeat1
- ( $$ "'" |-- Scan.one Symbol.is_regular
- || Scan.unless ($$ "_" || $$ "?" || $$ "\\<module>" || $$ "/" || $$ "{" |-- $$ "*")
- (Scan.one Symbol.is_regular)) >> (Pretty o str o implode)))
- (Symbol.explode s) of
- (p, []) => p
- | _ => error ("Malformed annotation: " ^ quote s));
-
-
-val _ = List.app Keyword.keyword ["attach", "file", "contains"];
-
-fun strip_whitespace s = implode (fst (take_suffix (fn c => c = "\n" orelse c = " ")
- (snd (take_prefix (fn c => c = "\n" orelse c = " ") (raw_explode s))))) ^ "\n";
-
-val parse_attach = Scan.repeat (Parse.$$$ "attach" |--
- Scan.optional (Parse.$$$ "(" |-- Parse.xname --| Parse.$$$ ")") "" --
- (Parse.verbatim >> strip_whitespace));
-
-val _ =
- Outer_Syntax.command "types_code"
- "associate types with target language types" Keyword.thy_decl
- (Scan.repeat1 (Parse.xname --| Parse.$$$ "(" -- Parse.string --| Parse.$$$ ")" -- parse_attach) >>
- (fn xs => Toplevel.theory (fn thy => fold (assoc_type o
- (fn ((name, mfx), aux) => (name, (parse_mixfix
- (Syntax.read_typ_global thy) mfx, aux)))) xs thy)));
-
-val _ =
- Outer_Syntax.command "consts_code"
- "associate constants with target language code" Keyword.thy_decl
- (Scan.repeat1
- (Parse.term --|
- Parse.$$$ "(" -- Parse.string --| Parse.$$$ ")" -- parse_attach) >>
- (fn xs => Toplevel.theory (fn thy => fold (assoc_const o
- (fn ((const, mfx), aux) =>
- (const, (parse_mixfix (Syntax.read_term_global thy) mfx, aux)))) xs thy)));
-
-fun parse_code lib =
- Scan.optional (Parse.$$$ "(" |-- Parse.enum "," Parse.xname --| Parse.$$$ ")") [] --
- (if lib then Scan.optional Parse.name "" else Parse.name) --
- Scan.option (Parse.$$$ "file" |-- Parse.name) --
- (if lib then Scan.succeed []
- else Scan.optional (Parse.$$$ "imports" |-- Scan.repeat1 Parse.name) []) --|
- Parse.$$$ "contains" --
- ( Scan.repeat1 (Parse.name --| Parse.$$$ "=" -- Parse.term)
- || Scan.repeat1 (Parse.term >> pair "")) >>
- (fn ((((mode, module), opt_fname), modules), xs) => Toplevel.theory (fn thy =>
- let
- val _ = legacy_feature "Old code generation command -- use 'export_code' instead";
- val mode' = (if lib then insert (op =) "library" else I) (remove (op =) "library" mode);
- val (code, gr) = generate_code thy mode' modules module xs;
- val thy' = thy |> Context.theory_map (ML_Context.exec (fn () =>
- (case opt_fname of
- NONE => ML_Context.eval_text false Position.none (cat_lines (map snd code))
- | SOME fname =>
- if lib then app (fn (name, s) => File.write
- (Path.append (Path.explode fname) (Path.basic (name ^ ".ML"))) s)
- (("ROOT", implode (map (fn (name, _) =>
- "use \"" ^ name ^ ".ML\";\n") code)) :: code)
- else File.write (Path.explode fname) (snd (hd code)))));
- in
- if lib then thy'
- else map_modules (Symtab.update (module, gr)) thy'
- end));
-
-val setup = add_codegen "default" default_codegen
- #> add_tycodegen "default" default_tycodegen
- #> add_preprocessor unfold_preprocessor;
-
-val _ =
- Outer_Syntax.command "code_library"
- "generate code for terms (one structure for each theory)" Keyword.thy_decl
- (parse_code true);
-
-val _ =
- Outer_Syntax.command "code_module"
- "generate code for terms (single structure, incremental)" Keyword.thy_decl
- (parse_code false);
-
-end;
--- a/src/Pure/drule.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/Pure/drule.ML Wed Aug 10 18:07:32 2011 -0700
@@ -302,20 +302,18 @@
(*Convert all Vars in a theorem to Frees. Also return a function for
- reversing that operation. DOES NOT WORK FOR TYPE VARIABLES.
- Similar code in type/freeze_thaw*)
+ reversing that operation. DOES NOT WORK FOR TYPE VARIABLES.*)
fun legacy_freeze_thaw_robust th =
let val fth = Thm.legacy_freezeT th
val thy = Thm.theory_of_thm fth
- val {prop, tpairs, ...} = rep_thm fth
in
- case List.foldr OldTerm.add_term_vars [] (prop :: Thm.terms_of_tpairs tpairs) of
+ case Thm.fold_terms Term.add_vars fth [] of
[] => (fth, fn i => fn x => x) (*No vars: nothing to do!*)
| vars =>
- let fun newName (Var(ix,_)) = (ix, legacy_gensym (string_of_indexname ix))
+ let fun newName (ix,_) = (ix, legacy_gensym (string_of_indexname ix))
val alist = map newName vars
- fun mk_inst (Var(v,T)) =
+ fun mk_inst (v,T) =
(cterm_of thy (Var(v,T)),
cterm_of thy (Free(((the o AList.lookup (op =) alist) v), T)))
val insts = map mk_inst vars
@@ -330,17 +328,16 @@
fun legacy_freeze_thaw th =
let val fth = Thm.legacy_freezeT th
val thy = Thm.theory_of_thm fth
- val {prop, tpairs, ...} = rep_thm fth
in
- case List.foldr OldTerm.add_term_vars [] (prop :: Thm.terms_of_tpairs tpairs) of
+ case Thm.fold_terms Term.add_vars fth [] of
[] => (fth, fn x => x)
| vars =>
- let fun newName (Var(ix,_), (pairs,used)) =
+ let fun newName (ix, _) (pairs, used) =
let val v = singleton (Name.variant_list used) (string_of_indexname ix)
in ((ix,v)::pairs, v::used) end;
- val (alist, _) = List.foldr newName ([], Library.foldr OldTerm.add_term_names
- (prop :: Thm.terms_of_tpairs tpairs, [])) vars
- fun mk_inst (Var(v,T)) =
+ val (alist, _) =
+ fold_rev newName vars ([], Thm.fold_terms Term.add_free_names fth [])
+ fun mk_inst (v, T) =
(cterm_of thy (Var(v,T)),
cterm_of thy (Free(((the o AList.lookup (op =) alist) v), T)))
val insts = map mk_inst vars
--- a/src/Pure/goal.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/Pure/goal.ML Wed Aug 10 18:07:32 2011 -0700
@@ -124,12 +124,11 @@
let
val _ = forked 1;
val future =
- singleton (Future.forks {name = name, group = NONE, deps = [], pri = ~1})
+ singleton
+ (Future.forks {name = name, group = NONE, deps = [], pri = ~1, interrupts = false})
(fn () =>
- (*interruptible*)
Exn.release
- (Exn.capture Future.status e before forked ~1
- handle exn => (forked ~1; reraise exn)));
+ (Exn.capture (Future.status o Future.interruptible_task) e before forked ~1));
in future end) ();
fun fork e = fork_name "Goal.fork" e;
--- a/src/Pure/old_term.ML Wed Aug 10 18:02:16 2011 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,94 +0,0 @@
-(* Title: Pure/old_term.ML
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
-
-Some outdated term operations.
-*)
-
-signature OLD_TERM =
-sig
- val it_term_types: (typ * 'a -> 'a) -> term * 'a -> 'a
- val add_term_names: term * string list -> string list
- val add_typ_tvars: typ * (indexname * sort) list -> (indexname * sort) list
- val add_typ_tfree_names: typ * string list -> string list
- val add_typ_tfrees: typ * (string * sort) list -> (string * sort) list
- val add_term_tvars: term * (indexname * sort) list -> (indexname * sort) list
- val add_term_tfrees: term * (string * sort) list -> (string * sort) list
- val add_term_tfree_names: term * string list -> string list
- val typ_tfrees: typ -> (string * sort) list
- val typ_tvars: typ -> (indexname * sort) list
- val term_tfrees: term -> (string * sort) list
- val term_tvars: term -> (indexname * sort) list
- val add_term_vars: term * term list -> term list
- val term_vars: term -> term list
- val add_term_frees: term * term list -> term list
- val term_frees: term -> term list
-end;
-
-structure OldTerm: OLD_TERM =
-struct
-
-(*iterate a function over all types in a term*)
-fun it_term_types f =
-let fun iter(Const(_,T), a) = f(T,a)
- | iter(Free(_,T), a) = f(T,a)
- | iter(Var(_,T), a) = f(T,a)
- | iter(Abs(_,T,t), a) = iter(t,f(T,a))
- | iter(f$u, a) = iter(f, iter(u, a))
- | iter(Bound _, a) = a
-in iter end
-
-(*Accumulates the names in the term, suppressing duplicates.
- Includes Frees and Consts. For choosing unambiguous bound var names.*)
-fun add_term_names (Const(a,_), bs) = insert (op =) (Long_Name.base_name a) bs
- | add_term_names (Free(a,_), bs) = insert (op =) a bs
- | add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs))
- | add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs)
- | add_term_names (_, bs) = bs;
-
-(*Accumulates the TVars in a type, suppressing duplicates.*)
-fun add_typ_tvars(Type(_,Ts),vs) = List.foldr add_typ_tvars vs Ts
- | add_typ_tvars(TFree(_),vs) = vs
- | add_typ_tvars(TVar(v),vs) = insert (op =) v vs;
-
-(*Accumulates the TFrees in a type, suppressing duplicates.*)
-fun add_typ_tfree_names(Type(_,Ts),fs) = List.foldr add_typ_tfree_names fs Ts
- | add_typ_tfree_names(TFree(f,_),fs) = insert (op =) f fs
- | add_typ_tfree_names(TVar(_),fs) = fs;
-
-fun add_typ_tfrees(Type(_,Ts),fs) = List.foldr add_typ_tfrees fs Ts
- | add_typ_tfrees(TFree(f),fs) = insert (op =) f fs
- | add_typ_tfrees(TVar(_),fs) = fs;
-
-(*Accumulates the TVars in a term, suppressing duplicates.*)
-val add_term_tvars = it_term_types add_typ_tvars;
-
-(*Accumulates the TFrees in a term, suppressing duplicates.*)
-val add_term_tfrees = it_term_types add_typ_tfrees;
-val add_term_tfree_names = it_term_types add_typ_tfree_names;
-
-(*Non-list versions*)
-fun typ_tfrees T = add_typ_tfrees(T,[]);
-fun typ_tvars T = add_typ_tvars(T,[]);
-fun term_tfrees t = add_term_tfrees(t,[]);
-fun term_tvars t = add_term_tvars(t,[]);
-
-
-(*Accumulates the Vars in the term, suppressing duplicates.*)
-fun add_term_vars (t, vars: term list) = case t of
- Var _ => Ord_List.insert Term_Ord.term_ord t vars
- | Abs (_,_,body) => add_term_vars(body,vars)
- | f$t => add_term_vars (f, add_term_vars(t, vars))
- | _ => vars;
-
-fun term_vars t = add_term_vars(t,[]);
-
-(*Accumulates the Frees in the term, suppressing duplicates.*)
-fun add_term_frees (t, frees: term list) = case t of
- Free _ => Ord_List.insert Term_Ord.term_ord t frees
- | Abs (_,_,body) => add_term_frees(body,frees)
- | f$t => add_term_frees (f, add_term_frees(t, frees))
- | _ => frees;
-
-fun term_frees t = add_term_frees(t,[]);
-
-end;
--- a/src/Pure/proofterm.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/Pure/proofterm.ML Wed Aug 10 18:07:32 2011 -0700
@@ -461,15 +461,15 @@
fun del_conflicting_tvars envT T = Term_Subst.instantiateT
(map_filter (fn ixnS as (_, S) =>
(Type.lookup envT ixnS; NONE) handle TYPE _ =>
- SOME (ixnS, TFree ("'dummy", S))) (OldTerm.typ_tvars T)) T;
+ SOME (ixnS, TFree ("'dummy", S))) (Term.add_tvarsT T [])) T;
fun del_conflicting_vars env t = Term_Subst.instantiate
(map_filter (fn ixnS as (_, S) =>
(Type.lookup (Envir.type_env env) ixnS; NONE) handle TYPE _ =>
- SOME (ixnS, TFree ("'dummy", S))) (OldTerm.term_tvars t),
- map_filter (fn Var (ixnT as (_, T)) =>
+ SOME (ixnS, TFree ("'dummy", S))) (Term.add_tvars t []),
+ map_filter (fn (ixnT as (_, T)) =>
(Envir.lookup (env, ixnT); NONE) handle TYPE _ =>
- SOME (ixnT, Free ("dummy", T))) (OldTerm.term_vars t)) t;
+ SOME (ixnT, Free ("dummy", T))) (Term.add_vars t [])) t;
fun norm_proof env =
let
@@ -674,11 +674,12 @@
local
-fun new_name (ix, (pairs,used)) =
+fun new_name ix (pairs, used) =
let val v = singleton (Name.variant_list used) (string_of_indexname ix)
- in ((ix, v) :: pairs, v :: used) end;
+ in ((ix, v) :: pairs, v :: used) end;
-fun freeze_one alist (ix, sort) = (case AList.lookup (op =) alist ix of
+fun freeze_one alist (ix, sort) =
+ (case AList.lookup (op =) alist ix of
NONE => TVar (ix, sort)
| SOME name => TFree (name, sort));
@@ -686,15 +687,14 @@
fun legacy_freezeT t prf =
let
- val used = OldTerm.it_term_types OldTerm.add_typ_tfree_names (t, [])
- and tvars = map #1 (OldTerm.it_term_types OldTerm.add_typ_tvars (t, []));
- val (alist, _) = List.foldr new_name ([], used) tvars;
+ val used = Term.add_tfree_names t [];
+ val (alist, _) = fold_rev new_name (map #1 (Term.add_tvars t [])) ([], used);
in
(case alist of
[] => prf (*nothing to do!*)
| _ =>
- let val frzT = map_type_tvar (freeze_one alist)
- in map_proof_terms (map_types frzT) frzT prf end)
+ let val frzT = map_type_tvar (freeze_one alist)
+ in map_proof_terms (map_types frzT) frzT prf end)
end;
end;
@@ -1404,7 +1404,8 @@
| fulfill_proof_future thy promises postproc body =
singleton
(Future.forks {name = "Proofterm.fulfill_proof_future", group = NONE,
- deps = Future.task_of body :: map (Future.task_of o snd) promises, pri = 0})
+ deps = Future.task_of body :: map (Future.task_of o snd) promises, pri = 0,
+ interrupts = true})
(fn () =>
postproc (fulfill_norm_proof thy (map (apsnd Future.join) promises) (Future.join body)));
@@ -1461,7 +1462,9 @@
else if not (Multithreading.enabled ()) then Future.value (make_body0 (full_proof0 ()))
else
singleton
- (Future.forks {name = "Proofterm.prepare_thm_proof", group = NONE, deps = [], pri = ~1})
+ (Future.forks
+ {name = "Proofterm.prepare_thm_proof", group = NONE, deps = [], pri = ~1,
+ interrupts = true})
(make_body0 o full_proof0);
fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0);
--- a/src/Pure/type.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/Pure/type.ML Wed Aug 10 18:07:32 2011 -0700
@@ -358,7 +358,7 @@
local
-fun new_name (ix, (pairs, used)) =
+fun new_name ix (pairs, used) =
let val v = singleton (Name.variant_list used) (string_of_indexname ix)
in ((ix, v) :: pairs, v :: used) end;
@@ -374,18 +374,16 @@
fun legacy_freeze_thaw_type T =
let
- val used = OldTerm.add_typ_tfree_names (T, [])
- and tvars = map #1 (OldTerm.add_typ_tvars (T, []));
- val (alist, _) = List.foldr new_name ([], used) tvars;
+ val used = Term.add_tfree_namesT T [];
+ val (alist, _) = fold_rev new_name (map #1 (Term.add_tvarsT T [])) ([], used);
in (map_type_tvar (freeze_one alist) T, map_type_tfree (thaw_one (map swap alist))) end;
val legacy_freeze_type = #1 o legacy_freeze_thaw_type;
fun legacy_freeze_thaw t =
let
- val used = OldTerm.it_term_types OldTerm.add_typ_tfree_names (t, [])
- and tvars = map #1 (OldTerm.it_term_types OldTerm.add_typ_tvars (t, []));
- val (alist, _) = List.foldr new_name ([], used) tvars;
+ val used = Term.add_tfree_names t [];
+ val (alist, _) = fold_rev new_name (map #1 (Term.add_tvars t [])) ([], used);
in
(case alist of
[] => (t, fn x => x) (*nothing to do!*)
--- a/src/Tools/Code_Generator.thy Wed Aug 10 18:02:16 2011 -0700
+++ b/src/Tools/Code_Generator.thy Wed Aug 10 18:07:32 2011 -0700
@@ -7,6 +7,8 @@
theory Code_Generator
imports Pure
uses
+ "~~/src/Tools/misc_legacy.ML"
+ "~~/src/Tools/codegen.ML"
"~~/src/Tools/cache_io.ML"
"~~/src/Tools/try.ML"
"~~/src/Tools/solve_direct.ML"
--- a/src/Tools/IsaPlanner/isand.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/Tools/IsaPlanner/isand.ML Wed Aug 10 18:07:32 2011 -0700
@@ -186,8 +186,8 @@
(* change type-vars to fresh type frees *)
fun fix_tvars_to_tfrees_in_terms names ts =
let
- val tfree_names = map fst (List.foldr OldTerm.add_term_tfrees [] ts);
- val tvars = List.foldr OldTerm.add_term_tvars [] ts;
+ val tfree_names = map fst (List.foldr Misc_Legacy.add_term_tfrees [] ts);
+ val tvars = List.foldr Misc_Legacy.add_term_tvars [] ts;
val (names',renamings) =
List.foldr (fn (tv as ((n,i),s),(Ns,Rs)) =>
let val n2 = singleton (Name.variant_list Ns) n in
@@ -212,15 +212,15 @@
fun unfix_tfrees ns th =
let
val varfiytfrees = map (Term.dest_TFree o Thm.typ_of) ns
- val skiptfrees = subtract (op =) varfiytfrees (OldTerm.add_term_tfrees (Thm.prop_of th,[]));
+ val skiptfrees = subtract (op =) varfiytfrees (Misc_Legacy.add_term_tfrees (Thm.prop_of th,[]));
in #2 (Thm.varifyT_global' skiptfrees th) end;
(* change schematic/meta vars to fresh free vars, avoiding name clashes
with "names" *)
fun fix_vars_to_frees_in_terms names ts =
let
- val vars = map Term.dest_Var (List.foldr OldTerm.add_term_vars [] ts);
- val Ns = List.foldr OldTerm.add_term_names names ts;
+ val vars = map Term.dest_Var (List.foldr Misc_Legacy.add_term_vars [] ts);
+ val Ns = List.foldr Misc_Legacy.add_term_names names ts;
val (_,renamings) =
Library.foldl (fn ((Ns,Rs),v as ((n,i),ty)) =>
let val n2 = singleton (Name.variant_list Ns) n in
@@ -245,7 +245,7 @@
val ctypify = Thm.ctyp_of sgn
val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
val prop = (Thm.prop_of th);
- val tvars = List.foldr OldTerm.add_term_tvars [] (prop :: tpairs);
+ val tvars = List.foldr Misc_Legacy.add_term_tvars [] (prop :: tpairs);
val ctyfixes =
map_filter
(fn (v as ((s,i),ty)) =>
@@ -258,7 +258,7 @@
val ctermify = Thm.cterm_of sgn
val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
val prop = (Thm.prop_of th);
- val vars = map Term.dest_Var (List.foldr OldTerm.add_term_vars
+ val vars = map Term.dest_Var (List.foldr Misc_Legacy.add_term_vars
[] (prop :: tpairs));
val cfixes =
map_filter
@@ -359,7 +359,7 @@
val sgn = Thm.theory_of_thm th;
val ctermify = Thm.cterm_of sgn;
- val allfrees = map Term.dest_Free (OldTerm.term_frees (Thm.prop_of th))
+ val allfrees = map Term.dest_Free (Misc_Legacy.term_frees (Thm.prop_of th))
val cfrees = map (ctermify o Free o lookupfree allfrees) vs
val sgs = prems_of th;
@@ -419,8 +419,8 @@
let
val t = Term.strip_all_body alledt;
val alls = rev (Term.strip_all_vars alledt);
- val varnames = map (fst o fst o Term.dest_Var) (OldTerm.term_vars t)
- val names = OldTerm.add_term_names (t,varnames);
+ val varnames = map (fst o fst o Term.dest_Var) (Misc_Legacy.term_vars t)
+ val names = Misc_Legacy.add_term_names (t,varnames);
val fvs = map Free
(Name.variant_list names (map fst alls)
~~ (map snd alls));
@@ -428,8 +428,8 @@
fun fix_alls_term i t =
let
- val varnames = map (fst o fst o Term.dest_Var) (OldTerm.term_vars t)
- val names = OldTerm.add_term_names (t,varnames);
+ val varnames = map (fst o fst o Term.dest_Var) (Misc_Legacy.term_vars t)
+ val names = Misc_Legacy.add_term_names (t,varnames);
val gt = Logic.get_goal t i;
val body = Term.strip_all_body gt;
val alls = rev (Term.strip_all_vars gt);
--- a/src/Tools/IsaPlanner/rw_inst.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/Tools/IsaPlanner/rw_inst.ML Wed Aug 10 18:07:32 2011 -0700
@@ -71,7 +71,7 @@
val (tpairl,tpairr) = Library.split_list (#tpairs rep)
val prop = #prop rep
in
- List.foldr OldTerm.add_term_names [] (prop :: (tpairl @ (tpairr @ hyps)))
+ List.foldr Misc_Legacy.add_term_names [] (prop :: (tpairl @ (tpairr @ hyps)))
end;
(* Given a list of variables that were bound, and a that has been
@@ -136,13 +136,13 @@
fun mk_renamings tgt rule_inst =
let
val rule_conds = Thm.prems_of rule_inst
- val names = List.foldr OldTerm.add_term_names [] (tgt :: rule_conds);
+ val names = List.foldr Misc_Legacy.add_term_names [] (tgt :: rule_conds);
val (conds_tyvs,cond_vs) =
Library.foldl (fn ((tyvs, vs), t) =>
- (union (op =) (OldTerm.term_tvars t) tyvs,
- union (op =) (map Term.dest_Var (OldTerm.term_vars t)) vs))
+ (union (op =) (Misc_Legacy.term_tvars t) tyvs,
+ union (op =) (map Term.dest_Var (Misc_Legacy.term_vars t)) vs))
(([],[]), rule_conds);
- val termvars = map Term.dest_Var (OldTerm.term_vars tgt);
+ val termvars = map Term.dest_Var (Misc_Legacy.term_vars tgt);
val vars_to_fix = union (op =) termvars cond_vs;
val (renamings, names2) =
List.foldr (fn (((n,i),ty), (vs, names')) =>
@@ -165,8 +165,8 @@
val ignore_ixs = map fst ignore_insts;
val (tvars, tfrees) =
List.foldr (fn (t, (varixs, tfrees)) =>
- (OldTerm.add_term_tvars (t,varixs),
- OldTerm.add_term_tfrees (t,tfrees)))
+ (Misc_Legacy.add_term_tvars (t,varixs),
+ Misc_Legacy.add_term_tfrees (t,tfrees)))
([],[]) ts;
val unfixed_tvars =
filter (fn (ix,s) => not (member (op =) ignore_ixs ix)) tvars;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/codegen.ML Wed Aug 10 18:07:32 2011 -0700
@@ -0,0 +1,1049 @@
+(* Title: Tools/codegen.ML
+ Author: Stefan Berghofer, TU Muenchen
+
+Old code generator.
+*)
+
+signature CODEGEN =
+sig
+ val quiet_mode : bool Unsynchronized.ref
+ val message : string -> unit
+ val margin : int Unsynchronized.ref
+ val string_of : Pretty.T -> string
+ val str : string -> Pretty.T
+
+ datatype 'a mixfix =
+ Arg
+ | Ignore
+ | Module
+ | Pretty of Pretty.T
+ | Quote of 'a;
+
+ type deftab
+ type node
+ type codegr
+ type 'a codegen
+
+ val add_codegen: string -> term codegen -> theory -> theory
+ val add_tycodegen: string -> typ codegen -> theory -> theory
+ val add_preprocessor: (theory -> thm list -> thm list) -> theory -> theory
+ val preprocess: theory -> thm list -> thm list
+ val preprocess_term: theory -> term -> term
+ val print_codegens: theory -> unit
+ val generate_code: theory -> string list -> string list -> string -> (string * string) list ->
+ (string * string) list * codegr
+ val generate_code_i: theory -> string list -> string list -> string -> (string * term) list ->
+ (string * string) list * codegr
+ val assoc_const: string * (term mixfix list *
+ (string * string) list) -> theory -> theory
+ val assoc_const_i: (string * typ) * (term mixfix list *
+ (string * string) list) -> theory -> theory
+ val assoc_type: xstring * (typ mixfix list *
+ (string * string) list) -> theory -> theory
+ val get_assoc_code: theory -> string * typ ->
+ (term mixfix list * (string * string) list) option
+ val get_assoc_type: theory -> string ->
+ (typ mixfix list * (string * string) list) option
+ val codegen_error: codegr -> string -> string -> 'a
+ val invoke_codegen: theory -> string list -> deftab -> string -> string -> bool ->
+ term -> codegr -> Pretty.T * codegr
+ val invoke_tycodegen: theory -> string list -> deftab -> string -> string -> bool ->
+ typ -> codegr -> Pretty.T * codegr
+ val mk_id: string -> string
+ val mk_qual_id: string -> string * string -> string
+ val mk_const_id: string -> string -> codegr -> (string * string) * codegr
+ val get_const_id: codegr -> string -> string * string
+ val mk_type_id: string -> string -> codegr -> (string * string) * codegr
+ val get_type_id: codegr -> string -> string * string
+ val thyname_of_type: theory -> string -> string
+ val thyname_of_const: theory -> string -> string
+ val rename_terms: term list -> term list
+ val rename_term: term -> term
+ val new_names: term -> string list -> string list
+ val new_name: term -> string -> string
+ val if_library: string list -> 'a -> 'a -> 'a
+ val get_defn: theory -> deftab -> string -> typ ->
+ ((typ * (string * thm)) * int option) option
+ val is_instance: typ -> typ -> bool
+ val parens: Pretty.T -> Pretty.T
+ val mk_app: bool -> Pretty.T -> Pretty.T list -> Pretty.T
+ val mk_tuple: Pretty.T list -> Pretty.T
+ val mk_let: (Pretty.T * Pretty.T) list -> Pretty.T -> Pretty.T
+ val eta_expand: term -> term list -> int -> term
+ val strip_tname: string -> string
+ val mk_type: bool -> typ -> Pretty.T
+ val mk_term_of: codegr -> string -> bool -> typ -> Pretty.T
+ val mk_gen: codegr -> string -> bool -> string list -> string -> typ -> Pretty.T
+ val poke_test_fn: (int -> term list option) -> unit
+ val poke_eval_fn: (unit -> term) -> unit
+ val test_term: Proof.context -> term -> int -> term list option
+ val eval_term: Proof.context -> term -> term
+ val evaluation_conv: Proof.context -> conv
+ val parse_mixfix: (string -> 'a) -> string -> 'a mixfix list
+ val quotes_of: 'a mixfix list -> 'a list
+ val num_args_of: 'a mixfix list -> int
+ val replace_quotes: 'b list -> 'a mixfix list -> 'b mixfix list
+ val mk_deftab: theory -> deftab
+ val map_unfold: (simpset -> simpset) -> theory -> theory
+ val add_unfold: thm -> theory -> theory
+ val del_unfold: thm -> theory -> theory
+
+ val get_node: codegr -> string -> node
+ val add_edge: string * string -> codegr -> codegr
+ val add_edge_acyclic: string * string -> codegr -> codegr
+ val del_nodes: string list -> codegr -> codegr
+ val map_node: string -> (node -> node) -> codegr -> codegr
+ val new_node: string * node -> codegr -> codegr
+
+ val setup: theory -> theory
+end;
+
+structure Codegen : CODEGEN =
+struct
+
+val quiet_mode = Unsynchronized.ref true;
+fun message s = if !quiet_mode then () else writeln s;
+
+val margin = Unsynchronized.ref 80;
+
+fun string_of p = Print_Mode.setmp [] (Pretty.string_of_margin (!margin)) p;
+
+val str = Print_Mode.setmp [] Pretty.str;
+
+(**** Mixfix syntax ****)
+
+datatype 'a mixfix =
+ Arg
+ | Ignore
+ | Module
+ | Pretty of Pretty.T
+ | Quote of 'a;
+
+fun is_arg Arg = true
+ | is_arg Ignore = true
+ | is_arg _ = false;
+
+fun quotes_of [] = []
+ | quotes_of (Quote q :: ms) = q :: quotes_of ms
+ | quotes_of (_ :: ms) = quotes_of ms;
+
+fun args_of [] xs = ([], xs)
+ | args_of (Arg :: ms) (x :: xs) = apfst (cons x) (args_of ms xs)
+ | args_of (Ignore :: ms) (_ :: xs) = args_of ms xs
+ | args_of (_ :: ms) xs = args_of ms xs;
+
+fun num_args_of x = length (filter is_arg x);
+
+
+(**** theory data ****)
+
+(* preprocessed definition table *)
+
+type deftab =
+ (typ * (* type of constant *)
+ (string * (* name of theory containing definition of constant *)
+ thm)) (* definition theorem *)
+ list Symtab.table;
+
+(* code dependency graph *)
+
+type nametab = (string * string) Symtab.table * unit Symtab.table;
+
+fun merge_nametabs ((tab, used) : nametab, (tab', used')) =
+ (Symtab.merge op = (tab, tab'), Symtab.merge op = (used, used'));
+
+type node =
+ (exn option * (* slot for arbitrary data *)
+ string * (* name of structure containing piece of code *)
+ string); (* piece of code *)
+
+type codegr =
+ node Graph.T *
+ (nametab * (* table for assigned constant names *)
+ nametab); (* table for assigned type names *)
+
+val emptygr : codegr = (Graph.empty,
+ ((Symtab.empty, Symtab.empty), (Symtab.empty, Symtab.empty)));
+
+(* type of code generators *)
+
+type 'a codegen =
+ theory -> (* theory in which generate_code was called *)
+ string list -> (* mode *)
+ deftab -> (* definition table (for efficiency) *)
+ string -> (* node name of caller (for recording dependencies) *)
+ string -> (* module name of caller (for modular code generation) *)
+ bool -> (* whether to parenthesize generated expression *)
+ 'a -> (* item to generate code from *)
+ codegr -> (* code dependency graph *)
+ (Pretty.T * codegr) option;
+
+
+(* theory data *)
+
+structure CodegenData = Theory_Data
+(
+ type T =
+ {codegens : (string * term codegen) list,
+ tycodegens : (string * typ codegen) list,
+ consts : ((string * typ) * (term mixfix list * (string * string) list)) list,
+ types : (string * (typ mixfix list * (string * string) list)) list,
+ preprocs: (stamp * (theory -> thm list -> thm list)) list,
+ modules: codegr Symtab.table};
+
+ val empty =
+ {codegens = [], tycodegens = [], consts = [], types = [],
+ preprocs = [], modules = Symtab.empty};
+ val extend = I;
+
+ fun merge
+ ({codegens = codegens1, tycodegens = tycodegens1,
+ consts = consts1, types = types1,
+ preprocs = preprocs1, modules = modules1} : T,
+ {codegens = codegens2, tycodegens = tycodegens2,
+ consts = consts2, types = types2,
+ preprocs = preprocs2, modules = modules2}) : T =
+ {codegens = AList.merge (op =) (K true) (codegens1, codegens2),
+ tycodegens = AList.merge (op =) (K true) (tycodegens1, tycodegens2),
+ consts = AList.merge (op =) (K true) (consts1, consts2),
+ types = AList.merge (op =) (K true) (types1, types2),
+ preprocs = AList.merge (op =) (K true) (preprocs1, preprocs2),
+ modules = Symtab.merge (K true) (modules1, modules2)};
+);
+
+fun print_codegens thy =
+ let val {codegens, tycodegens, ...} = CodegenData.get thy in
+ Pretty.writeln (Pretty.chunks
+ [Pretty.strs ("term code generators:" :: map fst codegens),
+ Pretty.strs ("type code generators:" :: map fst tycodegens)])
+ end;
+
+
+
+(**** access modules ****)
+
+fun get_modules thy = #modules (CodegenData.get thy);
+
+fun map_modules f thy =
+ let val {codegens, tycodegens, consts, types, preprocs, modules} =
+ CodegenData.get thy;
+ in CodegenData.put {codegens = codegens, tycodegens = tycodegens,
+ consts = consts, types = types, preprocs = preprocs,
+ modules = f modules} thy
+ end;
+
+
+(**** add new code generators to theory ****)
+
+fun add_codegen name f thy =
+ let val {codegens, tycodegens, consts, types, preprocs, modules} =
+ CodegenData.get thy
+ in (case AList.lookup (op =) codegens name of
+ NONE => CodegenData.put {codegens = (name, f) :: codegens,
+ tycodegens = tycodegens, consts = consts, types = types,
+ preprocs = preprocs, modules = modules} thy
+ | SOME _ => error ("Code generator " ^ name ^ " already declared"))
+ end;
+
+fun add_tycodegen name f thy =
+ let val {codegens, tycodegens, consts, types, preprocs, modules} =
+ CodegenData.get thy
+ in (case AList.lookup (op =) tycodegens name of
+ NONE => CodegenData.put {tycodegens = (name, f) :: tycodegens,
+ codegens = codegens, consts = consts, types = types,
+ preprocs = preprocs, modules = modules} thy
+ | SOME _ => error ("Code generator " ^ name ^ " already declared"))
+ end;
+
+
+(**** preprocessors ****)
+
+fun add_preprocessor p thy =
+ let val {codegens, tycodegens, consts, types, preprocs, modules} =
+ CodegenData.get thy
+ in CodegenData.put {tycodegens = tycodegens,
+ codegens = codegens, consts = consts, types = types,
+ preprocs = (stamp (), p) :: preprocs,
+ modules = modules} thy
+ end;
+
+fun preprocess thy =
+ let val {preprocs, ...} = CodegenData.get thy
+ in fold (fn (_, f) => f thy) preprocs end;
+
+fun preprocess_term thy t =
+ let
+ val x = Free (singleton (Name.variant_list (Misc_Legacy.add_term_names (t, []))) "x", fastype_of t);
+ (* fake definition *)
+ val eq = Skip_Proof.make_thm thy (Logic.mk_equals (x, t));
+ fun err () = error "preprocess_term: bad preprocessor"
+ in case map prop_of (preprocess thy [eq]) of
+ [Const ("==", _) $ x' $ t'] => if x = x' then t' else err ()
+ | _ => err ()
+ end;
+
+structure UnfoldData = Theory_Data
+(
+ type T = simpset;
+ val empty = empty_ss;
+ val extend = I;
+ val merge = merge_ss;
+);
+
+val map_unfold = UnfoldData.map;
+val add_unfold = map_unfold o Simplifier.add_simp;
+val del_unfold = map_unfold o Simplifier.del_simp;
+
+fun unfold_preprocessor thy =
+ let val ss = Simplifier.global_context thy (UnfoldData.get thy)
+ in map (Thm.transfer thy #> Simplifier.full_simplify ss) end;
+
+
+(**** associate constants with target language code ****)
+
+fun gen_assoc_const prep_const (raw_const, syn) thy =
+ let
+ val {codegens, tycodegens, consts, types, preprocs, modules} =
+ CodegenData.get thy;
+ val (cname, T) = prep_const thy raw_const;
+ in
+ if num_args_of (fst syn) > length (binder_types T) then
+ error ("More arguments than in corresponding type of " ^ cname)
+ else case AList.lookup (op =) consts (cname, T) of
+ NONE => CodegenData.put {codegens = codegens,
+ tycodegens = tycodegens,
+ consts = ((cname, T), syn) :: consts,
+ types = types, preprocs = preprocs,
+ modules = modules} thy
+ | SOME _ => error ("Constant " ^ cname ^ " already associated with code")
+ end;
+
+val assoc_const_i = gen_assoc_const (K I);
+val assoc_const = gen_assoc_const Code.read_bare_const;
+
+
+(**** associate types with target language types ****)
+
+fun assoc_type (s, syn) thy =
+ let
+ val {codegens, tycodegens, consts, types, preprocs, modules} =
+ CodegenData.get thy;
+ val tc = Sign.intern_type thy s;
+ in
+ case Symtab.lookup (snd (#types (Type.rep_tsig (Sign.tsig_of thy)))) tc of
+ SOME (Type.LogicalType i) =>
+ if num_args_of (fst syn) > i then
+ error ("More arguments than corresponding type constructor " ^ s)
+ else
+ (case AList.lookup (op =) types tc of
+ NONE => CodegenData.put {codegens = codegens,
+ tycodegens = tycodegens, consts = consts,
+ types = (tc, syn) :: types,
+ preprocs = preprocs, modules = modules} thy
+ | SOME _ => error ("Type " ^ tc ^ " already associated with code"))
+ | _ => error ("Not a type constructor: " ^ s)
+ end;
+
+fun get_assoc_type thy = AList.lookup (op =) ((#types o CodegenData.get) thy);
+
+
+(**** make valid ML identifiers ****)
+
+fun is_ascii_letdig x = Symbol.is_ascii_letter x orelse
+ Symbol.is_ascii_digit x orelse Symbol.is_ascii_quasi x;
+
+fun dest_sym s =
+ (case split_last (snd (take_prefix (fn c => c = "\\") (raw_explode s))) of
+ ("<" :: "^" :: xs, ">") => (true, implode xs)
+ | ("<" :: xs, ">") => (false, implode xs)
+ | _ => raise Fail "dest_sym");
+
+fun mk_id s = if s = "" then "" else
+ let
+ fun check_str [] = []
+ | check_str xs = (case take_prefix is_ascii_letdig xs of
+ ([], " " :: zs) => check_str zs
+ | ([], z :: zs) =>
+ if size z = 1 then string_of_int (ord z) :: check_str zs
+ else (case dest_sym z of
+ (true, "isub") => check_str zs
+ | (true, "isup") => "" :: check_str zs
+ | (ctrl, s') => (if ctrl then "ctrl_" ^ s' else s') :: check_str zs)
+ | (ys, zs) => implode ys :: check_str zs);
+ val s' = space_implode "_" (maps (check_str o Symbol.explode) (Long_Name.explode s))
+ in
+ if Symbol.is_ascii_letter (hd (raw_explode s')) then s' else "id_" ^ s'
+ end;
+
+fun mk_long_id (p as (tab, used)) module s =
+ let
+ fun find_name [] = raise Fail "mk_long_id"
+ | find_name (ys :: yss) =
+ let
+ val s' = Long_Name.implode ys
+ val s'' = Long_Name.append module s'
+ in case Symtab.lookup used s'' of
+ NONE => ((module, s'),
+ (Symtab.update_new (s, (module, s')) tab,
+ Symtab.update_new (s'', ()) used))
+ | SOME _ => find_name yss
+ end
+ in case Symtab.lookup tab s of
+ NONE => find_name (Library.suffixes1 (Long_Name.explode s))
+ | SOME name => (name, p)
+ end;
+
+(* module: module name for caller *)
+(* module': module name for callee *)
+(* if caller and callee reside in different modules, use qualified access *)
+
+fun mk_qual_id module (module', s) =
+ if module = module' orelse module' = "" then s else module' ^ "." ^ s;
+
+fun mk_const_id module cname (gr, (tab1, tab2)) =
+ let
+ val ((module, s), tab1') = mk_long_id tab1 module cname
+ val s' = mk_id s;
+ val s'' = if ML_Syntax.is_reserved s' then s' ^ "_const" else s'
+ in (((module, s'')), (gr, (tab1', tab2))) end;
+
+fun get_const_id (gr, (tab1, tab2)) cname =
+ case Symtab.lookup (fst tab1) cname of
+ NONE => error ("get_const_id: no such constant: " ^ quote cname)
+ | SOME (module, s) =>
+ let
+ val s' = mk_id s;
+ val s'' = if ML_Syntax.is_reserved s' then s' ^ "_const" else s'
+ in (module, s'') end;
+
+fun mk_type_id module tyname (gr, (tab1, tab2)) =
+ let
+ val ((module, s), tab2') = mk_long_id tab2 module tyname
+ val s' = mk_id s;
+ val s'' = if ML_Syntax.is_reserved s' then s' ^ "_type" else s'
+ in ((module, s''), (gr, (tab1, tab2'))) end;
+
+fun get_type_id (gr, (tab1, tab2)) tyname =
+ case Symtab.lookup (fst tab2) tyname of
+ NONE => error ("get_type_id: no such type: " ^ quote tyname)
+ | SOME (module, s) =>
+ let
+ val s' = mk_id s;
+ val s'' = if ML_Syntax.is_reserved s' then s' ^ "_type" else s'
+ in (module, s'') end;
+
+fun get_type_id' f tab tyname = apsnd f (get_type_id tab tyname);
+
+fun get_node (gr, x) k = Graph.get_node gr k;
+fun add_edge e (gr, x) = (Graph.add_edge e gr, x);
+fun add_edge_acyclic e (gr, x) = (Graph.add_edge_acyclic e gr, x);
+fun del_nodes ks (gr, x) = (Graph.del_nodes ks gr, x);
+fun map_node k f (gr, x) = (Graph.map_node k f gr, x);
+fun new_node p (gr, x) = (Graph.new_node p gr, x);
+
+fun thyname_of_type thy = #theory_name o Name_Space.the_entry (Sign.type_space thy);
+fun thyname_of_const thy = #theory_name o Name_Space.the_entry (Sign.const_space thy);
+
+fun rename_terms ts =
+ let
+ val names = List.foldr Misc_Legacy.add_term_names
+ (map (fst o fst) (rev (fold Term.add_vars ts []))) ts;
+ val reserved = filter ML_Syntax.is_reserved names;
+ val (illegal, alt_names) = split_list (map_filter (fn s =>
+ let val s' = mk_id s in if s = s' then NONE else SOME (s, s') end) names)
+ val ps = (reserved @ illegal) ~~
+ Name.variant_list names (map (suffix "'") reserved @ alt_names);
+
+ fun rename_id s = AList.lookup (op =) ps s |> the_default s;
+
+ fun rename (Var ((a, i), T)) = Var ((rename_id a, i), T)
+ | rename (Free (a, T)) = Free (rename_id a, T)
+ | rename (Abs (s, T, t)) = Abs (s, T, rename t)
+ | rename (t $ u) = rename t $ rename u
+ | rename t = t;
+ in
+ map rename ts
+ end;
+
+val rename_term = hd o rename_terms o single;
+
+
+(**** retrieve definition of constant ****)
+
+fun is_instance T1 T2 =
+ Type.raw_instance (T1, if null (Misc_Legacy.typ_tfrees T2) then T2 else Logic.varifyT_global T2);
+
+fun get_assoc_code thy (s, T) = Option.map snd (find_first (fn ((s', T'), _) =>
+ s = s' andalso is_instance T T') (#consts (CodegenData.get thy)));
+
+fun get_aux_code mode xs = map_filter (fn (m, code) =>
+ if m = "" orelse member (op =) mode m then SOME code else NONE) xs;
+
+fun dest_prim_def t =
+ let
+ val (lhs, rhs) = Logic.dest_equals t;
+ val (c, args) = strip_comb lhs;
+ val (s, T) = dest_Const c
+ in if forall is_Var args then SOME (s, (T, (args, rhs))) else NONE
+ end handle TERM _ => NONE;
+
+fun mk_deftab thy =
+ let
+ val axmss =
+ map (fn thy' => (Context.theory_name thy', Theory.axiom_table thy'))
+ (Theory.nodes_of thy);
+ fun add_def thyname (name, t) =
+ (case dest_prim_def t of
+ NONE => I
+ | SOME (s, (T, _)) => Symtab.map_default (s, [])
+ (cons (T, (thyname, Thm.axiom thy name))));
+ in
+ fold (fn (thyname, axms) => Symtab.fold (add_def thyname) axms) axmss Symtab.empty
+ end;
+
+fun prep_prim_def thy thm =
+ let
+ val prop = case preprocess thy [thm]
+ of [thm'] => Thm.prop_of thm'
+ | _ => error "mk_deftab: bad preprocessor"
+ in ((Option.map o apsnd o apsnd)
+ (fn (args, rhs) => split_last (rename_terms (args @ [rhs]))) o dest_prim_def) prop
+ end;
+
+fun get_defn thy defs s T = (case Symtab.lookup defs s of
+ NONE => NONE
+ | SOME ds =>
+ let val i = find_index (is_instance T o fst) ds
+ in if i >= 0 then
+ SOME (nth ds i, if length ds = 1 then NONE else SOME i)
+ else NONE
+ end);
+
+
+(**** invoke suitable code generator for term / type ****)
+
+fun codegen_error (gr, _) dep s =
+ error (s ^ "\nrequired by:\n" ^ commas (Graph.all_succs gr [dep]));
+
+fun invoke_codegen thy mode defs dep module brack t gr = (case get_first
+ (fn (_, f) => f thy mode defs dep module brack t gr) (#codegens (CodegenData.get thy)) of
+ NONE => codegen_error gr dep ("Unable to generate code for term:\n" ^
+ Syntax.string_of_term_global thy t)
+ | SOME x => x);
+
+fun invoke_tycodegen thy mode defs dep module brack T gr = (case get_first
+ (fn (_, f) => f thy mode defs dep module brack T gr ) (#tycodegens (CodegenData.get thy)) of
+ NONE => codegen_error gr dep ("Unable to generate code for type:\n" ^
+ Syntax.string_of_typ_global thy T)
+ | SOME x => x);
+
+
+(**** code generator for mixfix expressions ****)
+
+fun parens p = Pretty.block [str "(", p, str ")"];
+
+fun pretty_fn [] p = [p]
+ | pretty_fn (x::xs) p = str ("fn " ^ x ^ " =>") ::
+ Pretty.brk 1 :: pretty_fn xs p;
+
+fun pretty_mixfix _ _ [] [] _ = []
+ | pretty_mixfix module module' (Arg :: ms) (p :: ps) qs =
+ p :: pretty_mixfix module module' ms ps qs
+ | pretty_mixfix module module' (Ignore :: ms) ps qs =
+ pretty_mixfix module module' ms ps qs
+ | pretty_mixfix module module' (Module :: ms) ps qs =
+ (if module <> module'
+ then cons (str (module' ^ ".")) else I)
+ (pretty_mixfix module module' ms ps qs)
+ | pretty_mixfix module module' (Pretty p :: ms) ps qs =
+ p :: pretty_mixfix module module' ms ps qs
+ | pretty_mixfix module module' (Quote _ :: ms) ps (q :: qs) =
+ q :: pretty_mixfix module module' ms ps qs;
+
+fun replace_quotes [] [] = []
+ | replace_quotes xs (Arg :: ms) =
+ Arg :: replace_quotes xs ms
+ | replace_quotes xs (Ignore :: ms) =
+ Ignore :: replace_quotes xs ms
+ | replace_quotes xs (Module :: ms) =
+ Module :: replace_quotes xs ms
+ | replace_quotes xs (Pretty p :: ms) =
+ Pretty p :: replace_quotes xs ms
+ | replace_quotes (x::xs) (Quote _ :: ms) =
+ Quote x :: replace_quotes xs ms;
+
+
+(**** default code generators ****)
+
+fun eta_expand t ts i =
+ let
+ val k = length ts;
+ val Ts = drop k (binder_types (fastype_of t));
+ val j = i - k
+ in
+ List.foldr (fn (T, t) => Abs ("x", T, t))
+ (list_comb (t, ts @ map Bound (j-1 downto 0))) (take j Ts)
+ end;
+
+fun mk_app _ p [] = p
+ | mk_app brack p ps = if brack then
+ Pretty.block (str "(" ::
+ separate (Pretty.brk 1) (p :: ps) @ [str ")"])
+ else Pretty.block (separate (Pretty.brk 1) (p :: ps));
+
+fun new_names t xs = Name.variant_list
+ (union (op =) (map (fst o fst o dest_Var) (Misc_Legacy.term_vars t))
+ (Misc_Legacy.add_term_names (t, ML_Syntax.reserved_names))) (map mk_id xs);
+
+fun new_name t x = hd (new_names t [x]);
+
+fun if_library mode x y = if member (op =) mode "library" then x else y;
+
+fun default_codegen thy mode defs dep module brack t gr =
+ let
+ val (u, ts) = strip_comb t;
+ fun codegens brack = fold_map (invoke_codegen thy mode defs dep module brack)
+ in (case u of
+ Var ((s, i), T) =>
+ let
+ val (ps, gr') = codegens true ts gr;
+ val (_, gr'') = invoke_tycodegen thy mode defs dep module false T gr'
+ in SOME (mk_app brack (str (s ^
+ (if i=0 then "" else string_of_int i))) ps, gr'')
+ end
+
+ | Free (s, T) =>
+ let
+ val (ps, gr') = codegens true ts gr;
+ val (_, gr'') = invoke_tycodegen thy mode defs dep module false T gr'
+ in SOME (mk_app brack (str s) ps, gr'') end
+
+ | Const (s, T) =>
+ (case get_assoc_code thy (s, T) of
+ SOME (ms, aux) =>
+ let val i = num_args_of ms
+ in if length ts < i then
+ default_codegen thy mode defs dep module brack (eta_expand u ts i) gr
+ else
+ let
+ val (ts1, ts2) = args_of ms ts;
+ val (ps1, gr1) = codegens false ts1 gr;
+ val (ps2, gr2) = codegens true ts2 gr1;
+ val (ps3, gr3) = codegens false (quotes_of ms) gr2;
+ val (_, gr4) = invoke_tycodegen thy mode defs dep module false
+ (funpow (length ts) (hd o tl o snd o dest_Type) T) gr3;
+ val (module', suffix) = (case get_defn thy defs s T of
+ NONE => (if_library mode (thyname_of_const thy s) module, "")
+ | SOME ((U, (module', _)), NONE) =>
+ (if_library mode module' module, "")
+ | SOME ((U, (module', _)), SOME i) =>
+ (if_library mode module' module, " def" ^ string_of_int i));
+ val node_id = s ^ suffix;
+ fun p module' = mk_app brack (Pretty.block
+ (pretty_mixfix module module' ms ps1 ps3)) ps2
+ in SOME (case try (get_node gr4) node_id of
+ NONE => (case get_aux_code mode aux of
+ [] => (p module, gr4)
+ | xs => (p module', add_edge (node_id, dep) (new_node
+ (node_id, (NONE, module', cat_lines xs ^ "\n")) gr4)))
+ | SOME (_, module'', _) =>
+ (p module'', add_edge (node_id, dep) gr4))
+ end
+ end
+ | NONE => (case get_defn thy defs s T of
+ NONE => NONE
+ | SOME ((U, (thyname, thm)), k) => (case prep_prim_def thy thm
+ of SOME (_, (_, (args, rhs))) => let
+ val module' = if_library mode thyname module;
+ val suffix = (case k of NONE => "" | SOME i => " def" ^ string_of_int i);
+ val node_id = s ^ suffix;
+ val ((ps, def_id), gr') = gr |> codegens true ts
+ ||>> mk_const_id module' (s ^ suffix);
+ val p = mk_app brack (str (mk_qual_id module def_id)) ps
+ in SOME (case try (get_node gr') node_id of
+ NONE =>
+ let
+ val _ = message ("expanding definition of " ^ s);
+ val Ts = binder_types U;
+ val (args', rhs') =
+ if not (null args) orelse null Ts then (args, rhs) else
+ let val v = Free (new_name rhs "x", hd Ts)
+ in ([v], betapply (rhs, v)) end;
+ val (p', gr1) = invoke_codegen thy mode defs node_id module' false
+ rhs' (add_edge (node_id, dep)
+ (new_node (node_id, (NONE, "", "")) gr'));
+ val (xs, gr2) = codegens false args' gr1;
+ val (_, gr3) = invoke_tycodegen thy mode defs dep module false T gr2;
+ val (ty, gr4) = invoke_tycodegen thy mode defs node_id module' false U gr3;
+ in (p, map_node node_id (K (NONE, module', string_of
+ (Pretty.block (separate (Pretty.brk 1)
+ (if null args' then
+ [str ("val " ^ snd def_id ^ " :"), ty]
+ else str ("fun " ^ snd def_id) :: xs) @
+ [str " =", Pretty.brk 1, p', str ";"])) ^ "\n\n")) gr4)
+ end
+ | SOME _ => (p, add_edge (node_id, dep) gr'))
+ end
+ | NONE => NONE)))
+
+ | Abs _ =>
+ let
+ val (bs, Ts) = ListPair.unzip (strip_abs_vars u);
+ val t = strip_abs_body u
+ val bs' = new_names t bs;
+ val (ps, gr1) = codegens true ts gr;
+ val (p, gr2) = invoke_codegen thy mode defs dep module false
+ (subst_bounds (map Free (rev (bs' ~~ Ts)), t)) gr1;
+ in
+ SOME (mk_app brack (Pretty.block (str "(" :: pretty_fn bs' p @
+ [str ")"])) ps, gr2)
+ end
+
+ | _ => NONE)
+ end;
+
+fun default_tycodegen thy mode defs dep module brack (TVar ((s, i), _)) gr =
+ SOME (str (s ^ (if i = 0 then "" else string_of_int i)), gr)
+ | default_tycodegen thy mode defs dep module brack (TFree (s, _)) gr =
+ SOME (str s, gr)
+ | default_tycodegen thy mode defs dep module brack (Type (s, Ts)) gr =
+ (case AList.lookup (op =) ((#types o CodegenData.get) thy) s of
+ NONE => NONE
+ | SOME (ms, aux) =>
+ let
+ val (ps, gr') = fold_map
+ (invoke_tycodegen thy mode defs dep module false)
+ (fst (args_of ms Ts)) gr;
+ val (qs, gr'') = fold_map
+ (invoke_tycodegen thy mode defs dep module false)
+ (quotes_of ms) gr';
+ val module' = if_library mode (thyname_of_type thy s) module;
+ val node_id = s ^ " (type)";
+ fun p module' = Pretty.block (pretty_mixfix module module' ms ps qs)
+ in SOME (case try (get_node gr'') node_id of
+ NONE => (case get_aux_code mode aux of
+ [] => (p module', gr'')
+ | xs => (p module', snd (mk_type_id module' s
+ (add_edge (node_id, dep) (new_node (node_id,
+ (NONE, module', cat_lines xs ^ "\n")) gr'')))))
+ | SOME (_, module'', _) =>
+ (p module'', add_edge (node_id, dep) gr''))
+ end);
+
+fun mk_tuple [p] = p
+ | mk_tuple ps = Pretty.block (str "(" ::
+ flat (separate [str ",", Pretty.brk 1] (map single ps)) @ [str ")"]);
+
+fun mk_let bindings body =
+ Pretty.blk (0, [str "let", Pretty.brk 1,
+ Pretty.blk (0, separate Pretty.fbrk (map (fn (pat, rhs) =>
+ Pretty.block [str "val ", pat, str " =", Pretty.brk 1,
+ rhs, str ";"]) bindings)),
+ Pretty.brk 1, str "in", Pretty.brk 1, body,
+ Pretty.brk 1, str "end"]);
+
+fun mk_struct name s = "structure " ^ name ^ " =\nstruct\n\n" ^ s ^ "end;\n";
+
+fun add_to_module name s = AList.map_entry (op =) (name : string) (suffix s);
+
+fun output_code gr module xs =
+ let
+ val code = map_filter (fn s =>
+ let val c as (_, module', _) = Graph.get_node gr s
+ in if module = "" orelse module = module' then SOME (s, c) else NONE end)
+ (rev (Graph.all_preds gr xs));
+ fun string_of_cycle (a :: b :: cs) =
+ let val SOME (x, y) = get_first (fn (x, (_, a', _)) =>
+ if a = a' then Option.map (pair x)
+ (find_first ((fn (_, b', _) => b' = b) o Graph.get_node gr)
+ (Graph.imm_succs gr x))
+ else NONE) code
+ in x ^ " called by " ^ y ^ "\n" ^ string_of_cycle (b :: cs) end
+ | string_of_cycle _ = ""
+ in
+ if module = "" then
+ let
+ val modules = distinct (op =) (map (#2 o snd) code);
+ val mod_gr = fold_rev Graph.add_edge_acyclic
+ (maps (fn (s, (_, module, _)) => map (pair module)
+ (filter_out (fn s => s = module) (map (#2 o Graph.get_node gr)
+ (Graph.imm_succs gr s)))) code)
+ (fold_rev (Graph.new_node o rpair ()) modules Graph.empty);
+ val modules' =
+ rev (Graph.all_preds mod_gr (map (#2 o Graph.get_node gr) xs))
+ in
+ List.foldl (fn ((_, (_, module, s)), ms) => add_to_module module s ms)
+ (map (rpair "") modules') code
+ end handle Graph.CYCLES (cs :: _) =>
+ error ("Cyclic dependency of modules:\n" ^ commas cs ^
+ "\n" ^ string_of_cycle cs)
+ else [(module, implode (map (#3 o snd) code))]
+ end;
+
+fun gen_generate_code prep_term thy mode modules module xs =
+ let
+ val _ = (module <> "" orelse
+ member (op =) mode "library" andalso forall (fn (s, _) => s = "") xs)
+ orelse error "missing module name";
+ val graphs = get_modules thy;
+ val defs = mk_deftab thy;
+ val gr = new_node ("<Top>", (NONE, module, ""))
+ (List.foldl (fn ((gr, (tab1, tab2)), (gr', (tab1', tab2'))) =>
+ (Graph.merge (fn ((_, module, _), (_, module', _)) =>
+ module = module') (gr, gr'),
+ (merge_nametabs (tab1, tab1'), merge_nametabs (tab2, tab2')))) emptygr
+ (map (fn s => case Symtab.lookup graphs s of
+ NONE => error ("Undefined code module: " ^ s)
+ | SOME gr => gr) modules))
+ handle Graph.DUP k => error ("Duplicate code for " ^ k);
+ fun expand (t as Abs _) = t
+ | expand t = (case fastype_of t of
+ Type ("fun", [T, U]) => Abs ("x", T, t $ Bound 0) | _ => t);
+ val (ps, gr') = fold_map (fn (s, t) => fn gr => apfst (pair s)
+ (invoke_codegen thy mode defs "<Top>" module false t gr))
+ (map (apsnd (expand o preprocess_term thy o prep_term thy)) xs) gr;
+ val code = map_filter
+ (fn ("", _) => NONE
+ | (s', p) => SOME (string_of (Pretty.block
+ [str ("val " ^ s' ^ " ="), Pretty.brk 1, p, str ";"]))) ps;
+ val code' = space_implode "\n\n" code ^ "\n\n";
+ val code'' =
+ map_filter (fn (name, s) =>
+ if member (op =) mode "library" andalso name = module andalso null code
+ then NONE
+ else SOME (name, mk_struct name s))
+ ((if null code then I
+ else add_to_module module code')
+ (output_code (fst gr') (if_library mode "" module) ["<Top>"]))
+ in
+ (code'', del_nodes ["<Top>"] gr')
+ end;
+
+val generate_code_i = gen_generate_code Sign.cert_term;
+val generate_code =
+ gen_generate_code (Syntax.read_term o Proof_Context.allow_dummies o Proof_Context.init_global);
+
+
+(**** Reflection ****)
+
+val strip_tname = implode o tl o raw_explode;
+
+fun pretty_list xs = Pretty.block (str "[" ::
+ flat (separate [str ",", Pretty.brk 1] (map single xs)) @
+ [str "]"]);
+
+fun mk_type p (TVar ((s, i), _)) = str
+ (strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "T")
+ | mk_type p (TFree (s, _)) = str (strip_tname s ^ "T")
+ | mk_type p (Type (s, Ts)) = (if p then parens else I) (Pretty.block
+ [str "Type", Pretty.brk 1, str ("(\"" ^ s ^ "\","),
+ Pretty.brk 1, pretty_list (map (mk_type false) Ts), str ")"]);
+
+fun mk_term_of gr module p (TVar ((s, i), _)) = str
+ (strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "F")
+ | mk_term_of gr module p (TFree (s, _)) = str (strip_tname s ^ "F")
+ | mk_term_of gr module p (Type (s, Ts)) = (if p then parens else I)
+ (Pretty.block (separate (Pretty.brk 1)
+ (str (mk_qual_id module
+ (get_type_id' (fn s' => "term_of_" ^ s') gr s)) ::
+ maps (fn T =>
+ [mk_term_of gr module true T, mk_type true T]) Ts)));
+
+
+(**** Implicit results ****)
+
+structure Result = Proof_Data
+(
+ type T = (int -> term list option) * (unit -> term);
+ fun init _ = (fn _ => NONE, fn () => Bound 0);
+);
+
+val get_test_fn = #1 o Result.get;
+val get_eval_fn = #2 o Result.get;
+
+fun poke_test_fn f = Context.>> (Context.map_proof (Result.map (fn (_, g) => (f, g))));
+fun poke_eval_fn g = Context.>> (Context.map_proof (Result.map (fn (f, _) => (f, g))));
+
+
+(**** Test data generators ****)
+
+fun mk_gen gr module p xs a (TVar ((s, i), _)) = str
+ (strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "G")
+ | mk_gen gr module p xs a (TFree (s, _)) = str (strip_tname s ^ "G")
+ | mk_gen gr module p xs a (Type (tyc as (s, Ts))) = (if p then parens else I)
+ (Pretty.block (separate (Pretty.brk 1)
+ (str (mk_qual_id module (get_type_id' (fn s' => "gen_" ^ s') gr s) ^
+ (if member (op =) xs s then "'" else "")) ::
+ (case tyc of
+ ("fun", [T, U]) =>
+ [mk_term_of gr module true T, mk_type true T,
+ mk_gen gr module true xs a U, mk_type true U]
+ | _ => maps (fn T =>
+ [mk_gen gr module true xs a T, mk_type true T]) Ts) @
+ (if member (op =) xs s then [str a] else []))));
+
+fun test_term ctxt t =
+ let
+ val thy = Proof_Context.theory_of ctxt;
+ val (code, gr) = generate_code_i thy ["term_of", "test"] [] "Generated" [("testf", t)];
+ val Ts = map snd (fst (strip_abs t));
+ val args = map_index (fn (i, T) => ("arg" ^ string_of_int i, T)) Ts;
+ val s = "structure Test_Term =\nstruct\n\n" ^
+ cat_lines (map snd code) ^
+ "\nopen Generated;\n\n" ^ string_of
+ (Pretty.block [str "val () = Codegen.poke_test_fn",
+ Pretty.brk 1, str ("(fn i =>"), Pretty.brk 1,
+ mk_let (map (fn (s, T) =>
+ (mk_tuple [str s, str (s ^ "_t")],
+ Pretty.block [mk_gen gr "Generated" false [] "" T, Pretty.brk 1,
+ str "i"])) args)
+ (Pretty.block [str "if ",
+ mk_app false (str "testf") (map (str o fst) args),
+ Pretty.brk 1, str "then NONE",
+ Pretty.brk 1, str "else ",
+ Pretty.block [str "SOME ",
+ Pretty.enum "," "[" "]" (map (fn (s, _) => str (s ^ "_t ()")) args)]]),
+ str ");"]) ^
+ "\n\nend;\n";
+ in
+ ctxt
+ |> Context.proof_map (ML_Context.exec (fn () => ML_Context.eval_text false Position.none s))
+ |> get_test_fn
+ end;
+
+
+(**** Evaluator for terms ****)
+
+fun eval_term ctxt t =
+ let
+ val _ =
+ legacy_feature
+ "Old evaluation mechanism -- use evaluator \"code\" or method \"eval\" instead";
+ val thy = Proof_Context.theory_of ctxt;
+ val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse
+ error "Term to be evaluated contains type variables";
+ val _ = (null (Term.add_vars t []) andalso null (Term.add_frees t [])) orelse
+ error "Term to be evaluated contains variables";
+ val (code, gr) =
+ generate_code_i thy ["term_of"] [] "Generated"
+ [("result", Abs ("x", TFree ("'a", []), t))];
+ val s = "structure Eval_Term =\nstruct\n\n" ^
+ cat_lines (map snd code) ^
+ "\nopen Generated;\n\n" ^ string_of
+ (Pretty.block [str "val () = Codegen.poke_eval_fn (fn () =>",
+ Pretty.brk 1,
+ mk_app false (mk_term_of gr "Generated" false (fastype_of t))
+ [str "(result ())"],
+ str ");"]) ^
+ "\n\nend;\n";
+ val eval_fn =
+ ctxt
+ |> Context.proof_map (ML_Context.exec (fn () => ML_Context.eval_text false Position.none s))
+ |> get_eval_fn;
+ in eval_fn () end;
+
+val (_, evaluation_oracle) = Context.>>> (Context.map_theory_result
+ (Thm.add_oracle (Binding.name "evaluation", fn (ctxt, ct) =>
+ let
+ val thy = Proof_Context.theory_of ctxt;
+ val t = Thm.term_of ct;
+ in
+ if Theory.subthy (Thm.theory_of_cterm ct, thy) then
+ Thm.cterm_of thy (Logic.mk_equals (t, eval_term ctxt t))
+ else raise CTERM ("evaluation_oracle: bad theory", [ct])
+ end)));
+
+fun evaluation_conv ctxt ct = evaluation_oracle (ctxt, ct);
+
+
+(**** Interface ****)
+
+fun parse_mixfix rd s =
+ (case Scan.finite Symbol.stopper (Scan.repeat
+ ( $$ "_" >> K Arg
+ || $$ "?" >> K Ignore
+ || $$ "\<module>" >> K Module
+ || $$ "/" |-- Scan.repeat ($$ " ") >> (Pretty o Pretty.brk o length)
+ || $$ "{" |-- $$ "*" |-- Scan.repeat1
+ ( $$ "'" |-- Scan.one Symbol.is_regular
+ || Scan.unless ($$ "*" -- $$ "}") (Scan.one Symbol.is_regular)) --|
+ $$ "*" --| $$ "}" >> (Quote o rd o implode)
+ || Scan.repeat1
+ ( $$ "'" |-- Scan.one Symbol.is_regular
+ || Scan.unless ($$ "_" || $$ "?" || $$ "\<module>" || $$ "/" || $$ "{" |-- $$ "*")
+ (Scan.one Symbol.is_regular)) >> (Pretty o str o implode)))
+ (Symbol.explode s) of
+ (p, []) => p
+ | _ => error ("Malformed annotation: " ^ quote s));
+
+
+val _ = List.app Keyword.keyword ["attach", "file", "contains"];
+
+fun strip_whitespace s = implode (fst (take_suffix (fn c => c = "\n" orelse c = " ")
+ (snd (take_prefix (fn c => c = "\n" orelse c = " ") (raw_explode s))))) ^ "\n";
+
+val parse_attach = Scan.repeat (Parse.$$$ "attach" |--
+ Scan.optional (Parse.$$$ "(" |-- Parse.xname --| Parse.$$$ ")") "" --
+ (Parse.verbatim >> strip_whitespace));
+
+val _ =
+ Outer_Syntax.command "types_code"
+ "associate types with target language types" Keyword.thy_decl
+ (Scan.repeat1 (Parse.xname --| Parse.$$$ "(" -- Parse.string --| Parse.$$$ ")" -- parse_attach) >>
+ (fn xs => Toplevel.theory (fn thy => fold (assoc_type o
+ (fn ((name, mfx), aux) => (name, (parse_mixfix
+ (Syntax.read_typ_global thy) mfx, aux)))) xs thy)));
+
+val _ =
+ Outer_Syntax.command "consts_code"
+ "associate constants with target language code" Keyword.thy_decl
+ (Scan.repeat1
+ (Parse.term --|
+ Parse.$$$ "(" -- Parse.string --| Parse.$$$ ")" -- parse_attach) >>
+ (fn xs => Toplevel.theory (fn thy => fold (assoc_const o
+ (fn ((const, mfx), aux) =>
+ (const, (parse_mixfix (Syntax.read_term_global thy) mfx, aux)))) xs thy)));
+
+fun parse_code lib =
+ Scan.optional (Parse.$$$ "(" |-- Parse.enum "," Parse.xname --| Parse.$$$ ")") [] --
+ (if lib then Scan.optional Parse.name "" else Parse.name) --
+ Scan.option (Parse.$$$ "file" |-- Parse.name) --
+ (if lib then Scan.succeed []
+ else Scan.optional (Parse.$$$ "imports" |-- Scan.repeat1 Parse.name) []) --|
+ Parse.$$$ "contains" --
+ ( Scan.repeat1 (Parse.name --| Parse.$$$ "=" -- Parse.term)
+ || Scan.repeat1 (Parse.term >> pair "")) >>
+ (fn ((((mode, module), opt_fname), modules), xs) => Toplevel.theory (fn thy =>
+ let
+ val _ = legacy_feature "Old code generation command -- use 'export_code' instead";
+ val mode' = (if lib then insert (op =) "library" else I) (remove (op =) "library" mode);
+ val (code, gr) = generate_code thy mode' modules module xs;
+ val thy' = thy |> Context.theory_map (ML_Context.exec (fn () =>
+ (case opt_fname of
+ NONE => ML_Context.eval_text false Position.none (cat_lines (map snd code))
+ | SOME fname =>
+ if lib then app (fn (name, s) => File.write
+ (Path.append (Path.explode fname) (Path.basic (name ^ ".ML"))) s)
+ (("ROOT", implode (map (fn (name, _) =>
+ "use \"" ^ name ^ ".ML\";\n") code)) :: code)
+ else File.write (Path.explode fname) (snd (hd code)))));
+ in
+ if lib then thy'
+ else map_modules (Symtab.update (module, gr)) thy'
+ end));
+
+val setup = add_codegen "default" default_codegen
+ #> add_tycodegen "default" default_tycodegen
+ #> add_preprocessor unfold_preprocessor;
+
+val _ =
+ Outer_Syntax.command "code_library"
+ "generate code for terms (one structure for each theory)" Keyword.thy_decl
+ (parse_code true);
+
+val _ =
+ Outer_Syntax.command "code_module"
+ "generate code for terms (single structure, incremental)" Keyword.thy_decl
+ (parse_code false);
+
+end;
--- a/src/Tools/misc_legacy.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/Tools/misc_legacy.ML Wed Aug 10 18:07:32 2011 -0700
@@ -5,6 +5,22 @@
signature MISC_LEGACY =
sig
+ val it_term_types: (typ * 'a -> 'a) -> term * 'a -> 'a
+ val add_term_names: term * string list -> string list
+ val add_typ_tvars: typ * (indexname * sort) list -> (indexname * sort) list
+ val add_typ_tfree_names: typ * string list -> string list
+ val add_typ_tfrees: typ * (string * sort) list -> (string * sort) list
+ val add_term_tvars: term * (indexname * sort) list -> (indexname * sort) list
+ val add_term_tfrees: term * (string * sort) list -> (string * sort) list
+ val add_term_tfree_names: term * string list -> string list
+ val typ_tfrees: typ -> (string * sort) list
+ val typ_tvars: typ -> (indexname * sort) list
+ val term_tfrees: term -> (string * sort) list
+ val term_tvars: term -> (indexname * sort) list
+ val add_term_vars: term * term list -> term list
+ val term_vars: term -> term list
+ val add_term_frees: term * term list -> term list
+ val term_frees: term -> term list
val mk_defpair: term * term -> string * term
val get_def: theory -> xstring -> thm
val simple_read_term: theory -> typ -> string -> term
@@ -14,6 +30,71 @@
structure Misc_Legacy: MISC_LEGACY =
struct
+(*iterate a function over all types in a term*)
+fun it_term_types f =
+let fun iter(Const(_,T), a) = f(T,a)
+ | iter(Free(_,T), a) = f(T,a)
+ | iter(Var(_,T), a) = f(T,a)
+ | iter(Abs(_,T,t), a) = iter(t,f(T,a))
+ | iter(f$u, a) = iter(f, iter(u, a))
+ | iter(Bound _, a) = a
+in iter end
+
+(*Accumulates the names in the term, suppressing duplicates.
+ Includes Frees and Consts. For choosing unambiguous bound var names.*)
+fun add_term_names (Const(a,_), bs) = insert (op =) (Long_Name.base_name a) bs
+ | add_term_names (Free(a,_), bs) = insert (op =) a bs
+ | add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs))
+ | add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs)
+ | add_term_names (_, bs) = bs;
+
+(*Accumulates the TVars in a type, suppressing duplicates.*)
+fun add_typ_tvars(Type(_,Ts),vs) = List.foldr add_typ_tvars vs Ts
+ | add_typ_tvars(TFree(_),vs) = vs
+ | add_typ_tvars(TVar(v),vs) = insert (op =) v vs;
+
+(*Accumulates the TFrees in a type, suppressing duplicates.*)
+fun add_typ_tfree_names(Type(_,Ts),fs) = List.foldr add_typ_tfree_names fs Ts
+ | add_typ_tfree_names(TFree(f,_),fs) = insert (op =) f fs
+ | add_typ_tfree_names(TVar(_),fs) = fs;
+
+fun add_typ_tfrees(Type(_,Ts),fs) = List.foldr add_typ_tfrees fs Ts
+ | add_typ_tfrees(TFree(f),fs) = insert (op =) f fs
+ | add_typ_tfrees(TVar(_),fs) = fs;
+
+(*Accumulates the TVars in a term, suppressing duplicates.*)
+val add_term_tvars = it_term_types add_typ_tvars;
+
+(*Accumulates the TFrees in a term, suppressing duplicates.*)
+val add_term_tfrees = it_term_types add_typ_tfrees;
+val add_term_tfree_names = it_term_types add_typ_tfree_names;
+
+(*Non-list versions*)
+fun typ_tfrees T = add_typ_tfrees(T,[]);
+fun typ_tvars T = add_typ_tvars(T,[]);
+fun term_tfrees t = add_term_tfrees(t,[]);
+fun term_tvars t = add_term_tvars(t,[]);
+
+
+(*Accumulates the Vars in the term, suppressing duplicates.*)
+fun add_term_vars (t, vars: term list) = case t of
+ Var _ => Ord_List.insert Term_Ord.term_ord t vars
+ | Abs (_,_,body) => add_term_vars(body,vars)
+ | f$t => add_term_vars (f, add_term_vars(t, vars))
+ | _ => vars;
+
+fun term_vars t = add_term_vars(t,[]);
+
+(*Accumulates the Frees in the term, suppressing duplicates.*)
+fun add_term_frees (t, frees: term list) = case t of
+ Free _ => Ord_List.insert Term_Ord.term_ord t frees
+ | Abs (_,_,body) => add_term_frees(body,frees)
+ | f$t => add_term_frees (f, add_term_frees(t, frees))
+ | _ => frees;
+
+fun term_frees t = add_term_frees(t,[]);
+
+
fun mk_defpair (lhs, rhs) =
(case Term.head_of lhs of
Const (name, _) =>
--- a/src/ZF/Tools/inductive_package.ML Wed Aug 10 18:02:16 2011 -0700
+++ b/src/ZF/Tools/inductive_package.ML Wed Aug 10 18:07:32 2011 -0700
@@ -96,7 +96,7 @@
Syntax.string_of_term ctxt t);
(*** Construct the fixedpoint definition ***)
- val mk_variant = singleton (Name.variant_list (List.foldr OldTerm.add_term_names [] intr_tms));
+ val mk_variant = singleton (Name.variant_list (List.foldr Misc_Legacy.add_term_names [] intr_tms));
val z' = mk_variant"z" and X' = mk_variant"X" and w' = mk_variant"w";
@@ -108,7 +108,7 @@
fun fp_part intr = (*quantify over rule's free vars except parameters*)
let val prems = map dest_tprop (Logic.strip_imp_prems intr)
val dummy = List.app (fn rec_hd => List.app (Ind_Syntax.chk_prem rec_hd) prems) rec_hds
- val exfrees = subtract (op =) rec_params (OldTerm.term_frees intr)
+ val exfrees = subtract (op =) rec_params (Misc_Legacy.term_frees intr)
val zeq = FOLogic.mk_eq (Free(z', Ind_Syntax.iT), #1 (Ind_Syntax.rule_concl intr))
in List.foldr FOLogic.mk_exists
(Balanced_Tree.make FOLogic.mk_conj (zeq::prems)) exfrees
@@ -296,7 +296,7 @@
(*Make a premise of the induction rule.*)
fun induct_prem ind_alist intr =
- let val quantfrees = map dest_Free (subtract (op =) rec_params (OldTerm.term_frees intr))
+ let val quantfrees = map dest_Free (subtract (op =) rec_params (Misc_Legacy.term_frees intr))
val iprems = List.foldr (add_induct_prem ind_alist) []
(Logic.strip_imp_prems intr)
val (t,X) = Ind_Syntax.rule_concl intr