# HG changeset patch # User wenzelm # Date 1313004266 -7200 # Node ID fa98623f1006e6d80fed503eb64a583bd5855934 # Parent 691c52e900cab050b18f1958a21f5e6571d756a3# Parent 44adaa6db327d501c70c035b0af90f94f48e3863 merged diff -r 691c52e900ca -r fa98623f1006 src/FOL/IFOL.thy --- a/src/FOL/IFOL.thy Wed Aug 10 09:23:42 2011 -0700 +++ b/src/FOL/IFOL.thy Wed Aug 10 21:24:26 2011 +0200 @@ -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" diff -r 691c52e900ca -r fa98623f1006 src/FOL/IsaMakefile --- a/src/FOL/IsaMakefile Wed Aug 10 09:23:42 2011 -0700 +++ b/src/FOL/IsaMakefile Wed Aug 10 21:24:26 2011 +0200 @@ -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 \ diff -r 691c52e900ca -r fa98623f1006 src/FOLP/IFOLP.thy --- a/src/FOLP/IFOLP.thy Wed Aug 10 09:23:42 2011 -0700 +++ b/src/FOLP/IFOLP.thy Wed Aug 10 21:24:26 2011 +0200 @@ -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 diff -r 691c52e900ca -r fa98623f1006 src/FOLP/IsaMakefile --- a/src/FOLP/IsaMakefile Wed Aug 10 09:23:42 2011 -0700 +++ b/src/FOLP/IsaMakefile Wed Aug 10 21:24:26 2011 +0200 @@ -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 diff -r 691c52e900ca -r fa98623f1006 src/FOLP/simp.ML --- a/src/FOLP/simp.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/FOLP/simp.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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 diff -r 691c52e900ca -r fa98623f1006 src/HOL/Decision_Procs/Cooper.thy --- a/src/HOL/Decision_Procs/Cooper.thy Wed Aug 10 09:23:42 2011 -0700 +++ b/src/HOL/Decision_Procs/Cooper.thy Wed Aug 10 21:24:26 2011 +0200 @@ -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; diff -r 691c52e900ca -r fa98623f1006 src/HOL/Decision_Procs/MIR.thy --- a/src/HOL/Decision_Procs/MIR.thy Wed Aug 10 09:23:42 2011 -0700 +++ b/src/HOL/Decision_Procs/MIR.thy Wed Aug 10 21:24:26 2011 +0200 @@ -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; diff -r 691c52e900ca -r fa98623f1006 src/HOL/Decision_Procs/commutative_ring_tac.ML --- a/src/HOL/Decision_Procs/commutative_ring_tac.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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); diff -r 691c52e900ca -r fa98623f1006 src/HOL/Decision_Procs/cooper_tac.ML --- a/src/HOL/Decision_Procs/cooper_tac.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/HOL/Decision_Procs/cooper_tac.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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; diff -r 691c52e900ca -r fa98623f1006 src/HOL/Decision_Procs/ferrack_tac.ML --- a/src/HOL/Decision_Procs/ferrack_tac.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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; diff -r 691c52e900ca -r fa98623f1006 src/HOL/Decision_Procs/langford.ML --- a/src/HOL/Decision_Procs/langford.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/HOL/Decision_Procs/langford.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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 diff -r 691c52e900ca -r fa98623f1006 src/HOL/Decision_Procs/mir_tac.ML --- a/src/HOL/Decision_Procs/mir_tac.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/HOL/Decision_Procs/mir_tac.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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; diff -r 691c52e900ca -r fa98623f1006 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Wed Aug 10 09:23:42 2011 -0700 +++ b/src/HOL/HOL.thy Wed Aug 10 21:24:26 2011 +0200 @@ -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" diff -r 691c52e900ca -r fa98623f1006 src/HOL/Import/proof_kernel.ML --- a/src/HOL/Import/proof_kernel.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/HOL/Import/proof_kernel.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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) diff -r 691c52e900ca -r fa98623f1006 src/HOL/Import/shuffler.ML --- a/src/HOL/Import/shuffler.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/HOL/Import/shuffler.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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 diff -r 691c52e900ca -r fa98623f1006 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Aug 10 09:23:42 2011 -0700 +++ b/src/HOL/IsaMakefile Wed Aug 10 21:24:26 2011 +0200 @@ -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 \ diff -r 691c52e900ca -r fa98623f1006 src/HOL/Matrix/Compute_Oracle/linker.ML --- a/src/HOL/Matrix/Compute_Oracle/linker.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/HOL/Matrix/Compute_Oracle/linker.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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" diff -r 691c52e900ca -r fa98623f1006 src/HOL/Matrix/matrixlp.ML --- a/src/HOL/Matrix/matrixlp.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/HOL/Matrix/matrixlp.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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 diff -r 691c52e900ca -r fa98623f1006 src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/HOL/Nominal/nominal_datatype.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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; diff -r 691c52e900ca -r fa98623f1006 src/HOL/Nominal/nominal_fresh_fun.ML --- a/src/HOL/Nominal/nominal_fresh_fun.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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. *) diff -r 691c52e900ca -r fa98623f1006 src/HOL/Nominal/nominal_primrec.ML --- a/src/HOL/Nominal/nominal_primrec.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/HOL/Nominal/nominal_primrec.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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 => diff -r 691c52e900ca -r fa98623f1006 src/HOL/Statespace/state_space.ML --- a/src/HOL/Statespace/state_space.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/HOL/Statespace/state_space.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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 = diff -r 691c52e900ca -r fa98623f1006 src/HOL/Tools/ATP/atp_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_reconstruct.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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) diff -r 691c52e900ca -r fa98623f1006 src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/HOL/Tools/ATP/atp_translate.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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)) diff -r 691c52e900ca -r fa98623f1006 src/HOL/Tools/Datatype/datatype.ML --- a/src/HOL/Tools/Datatype/datatype.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/HOL/Tools/Datatype/datatype.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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; diff -r 691c52e900ca -r fa98623f1006 src/HOL/Tools/Datatype/datatype_abs_proofs.ML --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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); diff -r 691c52e900ca -r fa98623f1006 src/HOL/Tools/Datatype/datatype_aux.ML --- a/src/HOL/Tools/Datatype/datatype_aux.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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)))) diff -r 691c52e900ca -r fa98623f1006 src/HOL/Tools/Datatype/datatype_case.ML --- a/src/HOL/Tools/Datatype/datatype_case.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/HOL/Tools/Datatype/datatype_case.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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) diff -r 691c52e900ca -r fa98623f1006 src/HOL/Tools/Datatype/datatype_codegen.ML --- a/src/HOL/Tools/Datatype/datatype_codegen.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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) diff -r 691c52e900ca -r fa98623f1006 src/HOL/Tools/Datatype/datatype_data.ML --- a/src/HOL/Tools/Datatype/datatype_data.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/HOL/Tools/Datatype/datatype_data.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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 (); diff -r 691c52e900ca -r fa98623f1006 src/HOL/Tools/Datatype/datatype_prop.ML --- a/src/HOL/Tools/Datatype/datatype_prop.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/HOL/Tools/Datatype/datatype_prop.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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); diff -r 691c52e900ca -r fa98623f1006 src/HOL/Tools/Meson/meson_clausify.ML --- a/src/HOL/Tools/Meson/meson_clausify.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/HOL/Tools/Meson/meson_clausify.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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 = diff -r 691c52e900ca -r fa98623f1006 src/HOL/Tools/Metis/metis_reconstruct.ML --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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 diff -r 691c52e900ca -r fa98623f1006 src/HOL/Tools/Qelim/cooper.ML --- a/src/HOL/Tools/Qelim/cooper.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/HOL/Tools/Qelim/cooper.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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 diff -r 691c52e900ca -r fa98623f1006 src/HOL/Tools/Sledgehammer/async_manager.ML --- a/src/HOL/Tools/Sledgehammer/async_manager.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/HOL/Tools/Sledgehammer/async_manager.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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 diff -r 691c52e900ca -r fa98623f1006 src/HOL/Tools/TFL/casesplit.ML --- a/src/HOL/Tools/TFL/casesplit.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/HOL/Tools/TFL/casesplit.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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)))) => diff -r 691c52e900ca -r fa98623f1006 src/HOL/Tools/TFL/rules.ML --- a/src/HOL/Tools/TFL/rules.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/HOL/Tools/TFL/rules.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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 diff -r 691c52e900ca -r fa98623f1006 src/HOL/Tools/TFL/tfl.ML --- a/src/HOL/Tools/TFL/tfl.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/HOL/Tools/TFL/tfl.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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 diff -r 691c52e900ca -r fa98623f1006 src/HOL/Tools/TFL/usyntax.ML --- a/src/HOL/Tools/TFL/usyntax.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/HOL/Tools/TFL/usyntax.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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 = diff -r 691c52e900ca -r fa98623f1006 src/HOL/Tools/choice_specification.ML --- a/src/HOL/Tools/choice_specification.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/HOL/Tools/choice_specification.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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 diff -r 691c52e900ca -r fa98623f1006 src/HOL/Tools/cnf_funcs.ML --- a/src/HOL/Tools/cnf_funcs.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/HOL/Tools/cnf_funcs.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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 (*### diff -r 691c52e900ca -r fa98623f1006 src/HOL/Tools/inductive_codegen.ML --- a/src/HOL/Tools/inductive_codegen.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/HOL/Tools/inductive_codegen.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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!) **) diff -r 691c52e900ca -r fa98623f1006 src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/HOL/Tools/record.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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; diff -r 691c52e900ca -r fa98623f1006 src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/HOL/Tools/refute.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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 $ diff -r 691c52e900ca -r fa98623f1006 src/HOL/Tools/split_rule.ML --- a/src/HOL/Tools/split_rule.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/HOL/Tools/split_rule.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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; diff -r 691c52e900ca -r fa98623f1006 src/Pure/Concurrent/bash.ML --- a/src/Pure/Concurrent/bash.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/Pure/Concurrent/bash.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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); diff -r 691c52e900ca -r fa98623f1006 src/Pure/Concurrent/future.ML --- a/src/Pure/Concurrent/future.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/Pure/Concurrent/future.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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 () = diff -r 691c52e900ca -r fa98623f1006 src/Pure/Concurrent/par_list.ML --- a/src/Pure/Concurrent/par_list.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/Pure/Concurrent/par_list.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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); diff -r 691c52e900ca -r fa98623f1006 src/Pure/Concurrent/simple_thread.ML --- a/src/Pure/Concurrent/simple_thread.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/Pure/Concurrent/simple_thread.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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 *) diff -r 691c52e900ca -r fa98623f1006 src/Pure/Concurrent/task_queue.ML --- a/src/Pure/Concurrent/task_queue.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/Pure/Concurrent/task_queue.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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; diff -r 691c52e900ca -r fa98623f1006 src/Pure/Concurrent/time_limit.ML --- a/src/Pure/Concurrent/time_limit.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/Pure/Concurrent/time_limit.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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 (); diff -r 691c52e900ca -r fa98623f1006 src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Wed Aug 10 09:23:42 2011 -0700 +++ b/src/Pure/IsaMakefile Wed Aug 10 21:24:26 2011 +0200 @@ -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 \ diff -r 691c52e900ca -r fa98623f1006 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/Pure/PIDE/document.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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) diff -r 691c52e900ca -r fa98623f1006 src/Pure/Proof/reconstruct.ML --- a/src/Pure/Proof/reconstruct.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/Pure/Proof/reconstruct.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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 diff -r 691c52e900ca -r fa98623f1006 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/Pure/ROOT.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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 *) diff -r 691c52e900ca -r fa98623f1006 src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/Pure/Syntax/syntax.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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 { diff -r 691c52e900ca -r fa98623f1006 src/Pure/System/isabelle_system.ML --- a/src/Pure/System/isabelle_system.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/Pure/System/isabelle_system.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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 diff -r 691c52e900ca -r fa98623f1006 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/Pure/Thy/thy_info.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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) diff -r 691c52e900ca -r fa98623f1006 src/Pure/Thy/thy_load.ML --- a/src/Pure/Thy/thy_load.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/Pure/Thy/thy_load.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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) diff -r 691c52e900ca -r fa98623f1006 src/Pure/codegen.ML --- a/src/Pure/codegen.ML Wed Aug 10 09:23:42 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 ("", (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 "" 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) [""])) - in - (code'', del_nodes [""] 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 - || $$ "\\" >> 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 ($$ "_" || $$ "?" || $$ "\\" || $$ "/" || $$ "{" |-- $$ "*") - (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; diff -r 691c52e900ca -r fa98623f1006 src/Pure/drule.ML --- a/src/Pure/drule.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/Pure/drule.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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 diff -r 691c52e900ca -r fa98623f1006 src/Pure/goal.ML --- a/src/Pure/goal.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/Pure/goal.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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; diff -r 691c52e900ca -r fa98623f1006 src/Pure/old_term.ML --- a/src/Pure/old_term.ML Wed Aug 10 09:23:42 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; diff -r 691c52e900ca -r fa98623f1006 src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/Pure/proofterm.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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); diff -r 691c52e900ca -r fa98623f1006 src/Pure/type.ML --- a/src/Pure/type.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/Pure/type.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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!*) diff -r 691c52e900ca -r fa98623f1006 src/Tools/Code_Generator.thy --- a/src/Tools/Code_Generator.thy Wed Aug 10 09:23:42 2011 -0700 +++ b/src/Tools/Code_Generator.thy Wed Aug 10 21:24:26 2011 +0200 @@ -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" diff -r 691c52e900ca -r fa98623f1006 src/Tools/IsaPlanner/isand.ML --- a/src/Tools/IsaPlanner/isand.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/Tools/IsaPlanner/isand.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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); diff -r 691c52e900ca -r fa98623f1006 src/Tools/IsaPlanner/rw_inst.ML --- a/src/Tools/IsaPlanner/rw_inst.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/Tools/IsaPlanner/rw_inst.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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; diff -r 691c52e900ca -r fa98623f1006 src/Tools/codegen.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/codegen.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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 ("", (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 "" 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) [""])) + in + (code'', del_nodes [""] 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 + || $$ "\" >> 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 ($$ "_" || $$ "?" || $$ "\" || $$ "/" || $$ "{" |-- $$ "*") + (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; diff -r 691c52e900ca -r fa98623f1006 src/Tools/misc_legacy.ML --- a/src/Tools/misc_legacy.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/Tools/misc_legacy.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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, _) => diff -r 691c52e900ca -r fa98623f1006 src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Wed Aug 10 09:23:42 2011 -0700 +++ b/src/ZF/Tools/inductive_package.ML Wed Aug 10 21:24:26 2011 +0200 @@ -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