Merged.
--- a/doc-src/Codegen/Thy/pictures/adaption.tex Sun Mar 29 17:25:06 2009 +0200
+++ b/doc-src/Codegen/Thy/pictures/adaption.tex Sun Mar 29 17:38:01 2009 +0200
@@ -6,6 +6,12 @@
\begin{document}
+\thispagestyle{empty}
+\setlength{\fboxrule}{0.01pt}
+\setlength{\fboxsep}{4pt}
+
+\fbox{
+
\begin{tikzpicture}[scale = 0.5]
\tikzstyle water=[color = blue, thick]
\tikzstyle ice=[color = black, very thick, cap = round, join = round, fill = white]
@@ -43,4 +49,6 @@
(adaption) -- (reserved);
\end{tikzpicture}
+}
+
\end{document}
--- a/doc-src/Codegen/Thy/pictures/architecture.tex Sun Mar 29 17:25:06 2009 +0200
+++ b/doc-src/Codegen/Thy/pictures/architecture.tex Sun Mar 29 17:38:01 2009 +0200
@@ -6,6 +6,12 @@
\begin{document}
+\thispagestyle{empty}
+\setlength{\fboxrule}{0.01pt}
+\setlength{\fboxsep}{4pt}
+
+\fbox{
+
\begin{tikzpicture}[x = 4.2cm, y = 1cm]
\tikzstyle entity=[rounded corners, draw, thick, color = black, fill = white];
\tikzstyle process=[ellipse, draw, thick, color = green, fill = white];
@@ -30,4 +36,6 @@
\draw [style=process_arrow] (seri) -- (Haskell);
\end{tikzpicture}
+}
+
\end{document}
--- a/etc/isar-keywords-ZF.el Sun Mar 29 17:25:06 2009 +0200
+++ b/etc/isar-keywords-ZF.el Sun Mar 29 17:38:01 2009 +0200
@@ -18,6 +18,7 @@
"ML"
"ML_command"
"ML_prf"
+ "ML_test"
"ML_val"
"ProofGeneral\\.inform_file_processed"
"ProofGeneral\\.inform_file_retracted"
@@ -348,6 +349,7 @@
(defconst isar-keywords-theory-decl
'("ML"
+ "ML_test"
"abbreviation"
"arities"
"attribute_setup"
--- a/etc/isar-keywords.el Sun Mar 29 17:25:06 2009 +0200
+++ b/etc/isar-keywords.el Sun Mar 29 17:38:01 2009 +0200
@@ -18,6 +18,7 @@
"ML"
"ML_command"
"ML_prf"
+ "ML_test"
"ML_val"
"ProofGeneral\\.inform_file_processed"
"ProofGeneral\\.inform_file_retracted"
@@ -419,6 +420,7 @@
(defconst isar-keywords-theory-decl
'("ML"
+ "ML_test"
"abbreviation"
"arities"
"atom_decl"
--- a/lib/jedit/isabelle.xml Sun Mar 29 17:25:06 2009 +0200
+++ b/lib/jedit/isabelle.xml Sun Mar 29 17:38:01 2009 +0200
@@ -45,6 +45,7 @@
<OPERATOR>ML</OPERATOR>
<LABEL>ML_command</LABEL>
<OPERATOR>ML_prf</OPERATOR>
+ <OPERATOR>ML_test</OPERATOR>
<LABEL>ML_val</LABEL>
<OPERATOR>abbreviation</OPERATOR>
<KEYWORD4>actions</KEYWORD4>
--- a/src/HOL/Nominal/nominal_inductive2.ML Sun Mar 29 17:25:06 2009 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML Sun Mar 29 17:38:01 2009 +0200
@@ -181,7 +181,7 @@
| xs => error ("No such case(s) in inductive definition: " ^ commas_quote xs));
fun mk_avoids params name sets =
let
- val (_, ctxt') = ProofContext.add_fixes_i
+ val (_, ctxt') = ProofContext.add_fixes
(map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params) ctxt;
fun mk s =
let
--- a/src/HOL/Tools/function_package/fundef_lib.ML Sun Mar 29 17:25:06 2009 +0200
+++ b/src/HOL/Tools/function_package/fundef_lib.ML Sun Mar 29 17:38:01 2009 +0200
@@ -55,7 +55,7 @@
fun dest_all_all_ctx ctx (Const ("all", _) $ Abs (a as (n,T,b))) =
let
val [(n', _)] = Variable.variant_frees ctx [] [(n,T)]
- val (_, ctx') = ProofContext.add_fixes_i [(Binding.name n', SOME T, NoSyn)] ctx
+ val (_, ctx') = ProofContext.add_fixes [(Binding.name n', SOME T, NoSyn)] ctx
val (n'', body) = Term.dest_abs (n', T, b)
val _ = (n' = n'') orelse error "dest_all_ctx"
--- a/src/HOL/Tools/function_package/fundef_package.ML Sun Mar 29 17:25:06 2009 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML Sun Mar 29 17:38:01 2009 +0200
@@ -156,9 +156,9 @@
val goal = HOLogic.mk_Trueprop (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT)))
in
lthy
- |> ProofContext.note_thmss_i "" [((Binding.empty, [ContextRules.rule_del]), [([allI], [])])] |> snd
- |> ProofContext.note_thmss_i "" [((Binding.empty, [ContextRules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
- |> ProofContext.note_thmss_i ""
+ |> ProofContext.note_thmss "" [((Binding.empty, [ContextRules.rule_del]), [([allI], [])])] |> snd
+ |> ProofContext.note_thmss "" [((Binding.empty, [ContextRules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
+ |> ProofContext.note_thmss ""
[((Binding.name "termination", [ContextRules.intro_bang (SOME 0)]),
[([Goal.norm_result termination], [])])] |> snd
|> Proof.theorem_i NONE (total_termination_afterqed data) [[(goal, [])]]
--- a/src/Pure/Isar/attrib.ML Sun Mar 29 17:25:06 2009 +0200
+++ b/src/Pure/Isar/attrib.ML Sun Mar 29 17:38:01 2009 +0200
@@ -18,10 +18,13 @@
val attribute_i: theory -> src -> attribute
val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
val map_specs: ('a -> 'att) ->
- (('c * 'a list) * 'd) list -> (('c * 'att list) * 'd) list
+ (('c * 'a list) * 'b) list -> (('c * 'att list) * 'b) list
val map_facts: ('a -> 'att) ->
(('c * 'a list) * ('d * 'a list) list) list ->
(('c * 'att list) * ('d * 'att list) list) list
+ val map_facts_refs: ('a -> 'att) -> ('b -> 'fact) ->
+ (('c * 'a list) * ('b * 'a list) list) list ->
+ (('c * 'att list) * ('fact * 'att list) list) list
val crude_closure: Proof.context -> src -> src
val add_attributes: (bstring * (src -> attribute) * string) list -> theory -> theory
val syntax: attribute context_parser -> src -> attribute
@@ -121,14 +124,17 @@
fun attribute thy = attribute_i thy o intern_src thy;
fun eval_thms ctxt args = ProofContext.note_thmss Thm.theoremK
- [(Thm.empty_binding, map (apsnd (map (attribute (ProofContext.theory_of ctxt)))) args)] ctxt
+ [(Thm.empty_binding, args |> map (fn (a, atts) =>
+ (ProofContext.get_fact ctxt a, map (attribute (ProofContext.theory_of ctxt)) atts)))] ctxt
|> fst |> maps snd;
(* attributed declarations *)
fun map_specs f = map (apfst (apsnd (map f)));
+
fun map_facts f = map (apfst (apsnd (map f)) o apsnd (map (apsnd (map f))));
+fun map_facts_refs f g = map_facts f #> map (apsnd (map (apfst g)));
(* crude_closure *)
--- a/src/Pure/Isar/class.ML Sun Mar 29 17:25:06 2009 +0200
+++ b/src/Pure/Isar/class.ML Sun Mar 29 17:38:01 2009 +0200
@@ -225,8 +225,9 @@
|> (map o apsnd o apsnd o map_atyps o K o TFree) (Name.aT, [class]);
val all_params = Locale.params_of thy class;
val raw_params = (snd o chop (length supparams)) all_params;
- fun add_const (b, SOME raw_ty, _) thy =
+ fun add_const ((raw_c, raw_ty), _) thy =
let
+ val b = Binding.name raw_c;
val c = Sign.full_name thy b;
val ty = map_atyps (K (TFree (Name.aT, base_sort))) raw_ty;
val ty0 = Type.strip_sorts ty;
@@ -284,7 +285,7 @@
`(fn thy => calculate thy class sups base_sort param_map assm_axiom)
#-> (fn (base_morph, morph, export_morph, axiom, assm_intro, of_class) =>
Locale.add_registration (class, (morph, export_morph))
- #> Locale.activate_global_facts (class, morph $> export_morph)
+ #> Context.theory_map (Locale.activate_facts (class, morph $> export_morph))
#> register class sups params base_sort base_morph axiom assm_intro of_class))
|> TheoryTarget.init (SOME class)
|> pair class
--- a/src/Pure/Isar/class_target.ML Sun Mar 29 17:25:06 2009 +0200
+++ b/src/Pure/Isar/class_target.ML Sun Mar 29 17:38:01 2009 +0200
@@ -287,8 +287,8 @@
|> fold (fn dep_morph => Locale.add_dependency sub (sup,
dep_morph $> Element.satisfy_morphism (the_list some_wit) $> export))
(the_list some_dep_morph)
- |> (fn thy => fold_rev Locale.activate_global_facts
- (Locale.get_registrations thy) thy)
+ |> (fn thy => fold_rev (Context.theory_map o Locale.activate_facts)
+ (Locale.get_registrations thy) thy)
end;
--- a/src/Pure/Isar/code_unit.ML Sun Mar 29 17:25:06 2009 +0200
+++ b/src/Pure/Isar/code_unit.ML Sun Mar 29 17:38:01 2009 +0200
@@ -325,19 +325,18 @@
val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm
handle TERM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm)
| THM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm);
- fun vars_of t = fold_aterms
- (fn Var (v, _) => insert (op =) v
- | Free _ => bad_thm ("Illegal free variable in rewrite theorem\n"
- ^ Display.string_of_thm thm)
- | _ => I) t [];
- fun tvars_of t = fold_term_types
- (fn _ => fold_atyps (fn TVar (v, _) => insert (op =) v
- | TFree _ => bad_thm
+ fun vars_of t = fold_aterms (fn Var (v, _) => insert (op =) v
+ | Free _ => bad_thm ("Illegal free variable in rewrite theorem\n"
+ ^ Display.string_of_thm thm)
+ | _ => I) t [];
+ fun tvars_of t = fold_term_types (fn _ =>
+ fold_atyps (fn TVar (v, _) => insert (op =) v
+ | TFree _ => bad_thm
("Illegal free type variable in rewrite theorem\n" ^ Display.string_of_thm thm))) t [];
val lhs_vs = vars_of lhs;
val rhs_vs = vars_of rhs;
val lhs_tvs = tvars_of lhs;
- val rhs_tvs = tvars_of lhs;
+ val rhs_tvs = tvars_of rhs;
val _ = if null (subtract (op =) lhs_vs rhs_vs)
then ()
else bad_thm ("Free variables on right hand side of rewrite theorem\n"
--- a/src/Pure/Isar/constdefs.ML Sun Mar 29 17:25:06 2009 +0200
+++ b/src/Pure/Isar/constdefs.ML Sun Mar 29 17:38:01 2009 +0200
@@ -25,13 +25,13 @@
fun err msg ts = error (cat_lines (msg :: map (Syntax.string_of_term_global thy) ts));
val thy_ctxt = ProofContext.init thy;
- val struct_ctxt = #2 (ProofContext.add_fixes_i structs thy_ctxt);
+ val struct_ctxt = #2 (ProofContext.add_fixes structs thy_ctxt);
val ((d, mx), var_ctxt) =
(case raw_decl of
NONE => ((NONE, NoSyn), struct_ctxt)
| SOME raw_var =>
struct_ctxt |> prep_vars [raw_var] |-> (fn [(x, T, mx)] =>
- ProofContext.add_fixes_i [(x, T, mx)] #> snd #> pair (SOME x, mx)));
+ ProofContext.add_fixes [(x, T, mx)] #> snd #> pair (SOME x, mx)));
val prop = prep_prop var_ctxt raw_prop;
val (c, T) = #1 (LocalDefs.cert_def thy_ctxt (Logic.strip_imp_concl prop));
--- a/src/Pure/Isar/element.ML Sun Mar 29 17:25:06 2009 +0200
+++ b/src/Pure/Isar/element.ML Sun Mar 29 17:38:01 2009 +0200
@@ -486,7 +486,7 @@
local
fun activate_elem (Fixes fixes) ctxt =
- ctxt |> ProofContext.add_fixes_i fixes |> snd
+ ctxt |> ProofContext.add_fixes fixes |> snd
| activate_elem (Constrains _) ctxt =
ctxt
| activate_elem (Assumes asms) ctxt =
@@ -510,7 +510,7 @@
| activate_elem (Notes (kind, facts)) ctxt =
let
val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts;
- val (res, ctxt') = ctxt |> ProofContext.note_thmss_i kind facts';
+ val (res, ctxt') = ctxt |> ProofContext.note_thmss kind facts';
in ctxt' end;
fun gen_activate prep_facts raw_elems ctxt =
--- a/src/Pure/Isar/expression.ML Sun Mar 29 17:25:06 2009 +0200
+++ b/src/Pure/Isar/expression.ML Sun Mar 29 17:38:01 2009 +0200
@@ -20,14 +20,14 @@
(* Declaring locales *)
val cert_declaration: expression_i -> (Proof.context -> Proof.context) -> Element.context_i list ->
- Proof.context -> ((binding * typ option * mixfix) list * (string * morphism) list
+ Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
* Element.context_i list) * ((string * typ) list * Proof.context)
val cert_read_declaration: expression_i -> (Proof.context -> Proof.context) -> Element.context list ->
- Proof.context -> ((binding * typ option * mixfix) list * (string * morphism) list
+ Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
* Element.context_i list) * ((string * typ) list * Proof.context)
(*FIXME*)
val read_declaration: expression -> (Proof.context -> Proof.context) -> Element.context list ->
- Proof.context -> ((binding * typ option * mixfix) list * (string * morphism) list
+ Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
* Element.context_i list) * ((string * typ) list * Proof.context)
val add_locale: binding -> binding -> expression_i -> Element.context_i list ->
theory -> string * local_theory
@@ -80,22 +80,17 @@
fun parameters_of thy strict (expr, fixed) =
let
fun reject_dups message xs =
- let val dups = duplicates (op =) xs
- in
- if null dups then () else error (message ^ commas dups)
- end;
+ (case duplicates (op =) xs of
+ [] => ()
+ | dups => error (message ^ commas dups));
- fun match_bind (n, b) = (n = Binding.name_of b);
- fun parm_eq ((b1, mx1: mixfix), (b2, mx2)) =
- Binding.eq_name (b1, b2) andalso
- (mx1 = mx2 orelse
- error ("Conflicting syntax for parameter " ^ quote (Binding.str_of b1) ^ " in expression"));
+ fun parm_eq ((p1: string, mx1: mixfix), (p2, mx2)) = p1 = p2 andalso
+ (mx1 = mx2 orelse error ("Conflicting syntax for parameter " ^ quote p1 ^ " in expression"));
- fun params_loc loc =
- (Locale.params_of thy loc |> map (fn (p, _, mx) => (p, mx)), loc);
+ fun params_loc loc = Locale.params_of thy loc |> map (apfst #1);
fun params_inst (expr as (loc, (prfx, Positional insts))) =
let
- val (ps, loc') = params_loc loc;
+ val ps = params_loc loc;
val d = length ps - length insts;
val insts' =
if d < 0 then error ("More arguments than parameters in instantiation of locale " ^
@@ -103,17 +98,17 @@
else insts @ replicate d NONE;
val ps' = (ps ~~ insts') |>
map_filter (fn (p, NONE) => SOME p | (_, SOME _) => NONE);
- in (ps', (loc', (prfx, Positional insts'))) end
+ in (ps', (loc, (prfx, Positional insts'))) end
| params_inst (expr as (loc, (prfx, Named insts))) =
let
val _ = reject_dups "Duplicate instantiation of the following parameter(s): "
(map fst insts);
- val (ps, loc') = params_loc loc;
+ val ps = params_loc loc;
val ps' = fold (fn (p, _) => fn ps =>
- if AList.defined match_bind ps p then AList.delete match_bind p ps
- else error (quote p ^" not a parameter of instantiated expression.")) insts ps;
- in (ps', (loc', (prfx, Named insts))) end;
+ if AList.defined (op =) ps p then AList.delete (op =) p ps
+ else error (quote p ^ " not a parameter of instantiated expression")) insts ps;
+ in (ps', (loc, (prfx, Named insts))) end;
fun params_expr is =
let
val (is', ps') = fold_map (fn i => fn ps =>
@@ -125,7 +120,7 @@
val (implicit, expr') = params_expr expr;
- val implicit' = map (#1 #> Name.of_binding) implicit;
+ val implicit' = map #1 implicit;
val fixed' = map (#1 #> Name.of_binding) fixed;
val _ = reject_dups "Duplicate fixed parameter(s): " fixed';
val implicit'' =
@@ -133,7 +128,7 @@
else
let val _ = reject_dups
"Parameter(s) declared simultaneously in expression and for clause: " (implicit' @ fixed')
- in map (fn (b, mx) => (b, NONE, mx)) implicit end;
+ in map (fn (x, mx) => (Binding.name x, NONE, mx)) implicit end;
in (expr', implicit'' @ fixed) end;
@@ -276,7 +271,7 @@
fun declare_elem prep_vars (Fixes fixes) ctxt =
let val (vars, _) = prep_vars fixes ctxt
- in ctxt |> ProofContext.add_fixes_i vars |> snd end
+ in ctxt |> ProofContext.add_fixes vars |> snd end
| declare_elem prep_vars (Constrains csts) ctxt =
ctxt |> prep_vars (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) csts) |> snd
| declare_elem _ (Assumes _) ctxt = ctxt
@@ -319,8 +314,7 @@
fun finish_inst ctxt parms do_close (loc, (prfx, inst)) =
let
val thy = ProofContext.theory_of ctxt;
- val (parm_names, parm_types) = Locale.params_of thy loc |>
- map_split (fn (b, SOME T, _) => (Binding.name_of b, T));
+ val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst) ctxt;
in (loc, morph) end;
@@ -349,9 +343,7 @@
fun prep_insts (loc, (prfx, inst)) (i, insts, ctxt) =
let
- val (parm_names, parm_types) = Locale.params_of thy loc |>
- map_split (fn (b, SOME T, _) => (Name.of_binding b, T))
- (*FIXME return value of Locale.params_of has strange type*)
+ val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
val inst' = prep_inst ctxt parm_names inst;
val parm_types' = map (TypeInfer.paramify_vars o
Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT) parm_types;
@@ -360,7 +352,7 @@
val (insts'', _, _, ctxt' (* FIXME not used *) ) = check_autofix insts' [] [] ctxt;
val inst''' = insts'' |> List.last |> snd |> snd;
val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst''') ctxt;
- val ctxt'' = Locale.activate_declarations thy (loc, morph) ctxt;
+ val ctxt'' = Locale.activate_declarations (loc, morph) ctxt;
in (i + 1, insts', ctxt'') end;
fun prep_elem insts raw_elem (elems, ctxt) =
@@ -376,7 +368,7 @@
in check_autofix insts elems concl ctxt end;
val fors = prep_vars_inst fixed ctxt1 |> fst;
- val ctxt2 = ctxt1 |> ProofContext.add_fixes_i fors |> snd;
+ val ctxt2 = ctxt1 |> ProofContext.add_fixes fors |> snd;
val (_, insts', ctxt3) = fold prep_insts raw_insts (0, [], ctxt2);
val ctxt4 = init_body ctxt3;
val (elems, ctxt5) = fold (prep_elem insts') raw_elems ([], ctxt4);
@@ -390,9 +382,10 @@
val parms = xs ~~ Ts; (* params from expression and elements *)
val Fixes fors' = finish_primitive parms I (Fixes fors);
+ val fixed = map (fn (b, SOME T, mx) => ((Binding.name_of b, T), mx)) fors';
val (deps, elems'') = finish ctxt6 parms do_close insts elems';
- in ((fors', deps, elems'', concl), (parms, ctxt7)) end
+ in ((fixed, deps, elems'', concl), (parms, ctxt7)) end
in
@@ -432,6 +425,9 @@
(* Locale declaration: import + elements *)
+fun fix_params params =
+ ProofContext.add_fixes (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params) #> snd;
+
local
fun prep_declaration prep activate raw_import init_body raw_elems context =
@@ -440,8 +436,8 @@
prep false true raw_import init_body raw_elems [] context ;
(* Declare parameters and imported facts *)
val context' = context |>
- ProofContext.add_fixes_i fixed |> snd |>
- fold Locale.activate_local_facts deps;
+ fix_params fixed |>
+ fold (Context.proof_map o Locale.activate_facts) deps;
val (elems', _) = context' |>
ProofContext.set_stmt true |>
activate elems;
@@ -477,7 +473,7 @@
val propss = map (props_of thy) deps;
val goal_ctxt = context |>
- ProofContext.add_fixes_i fixed |> snd |>
+ fix_params fixed |>
(fold o fold) Variable.auto_fixes propss;
val export = Variable.export_morphism goal_ctxt context;
@@ -658,13 +654,13 @@
fun define_preds pname parms (((exts, exts'), (ints, ints')), defs) thy =
let
- val defs' = map (cterm_of thy #> Assumption.assume #> Drule.gen_all #> Drule.abs_def) defs;
+ val defs' = map (cterm_of thy #> Assumption.assume #> Drule.abs_def) defs;
val (a_pred, a_intro, a_axioms, thy'') =
if null exts then (NONE, NONE, [], thy)
else
let
- val aname = if null ints then pname else Binding.suffix_name ("_" ^ axiomsN) pname
+ val aname = if null ints then pname else Binding.suffix_name ("_" ^ axiomsN) pname;
val ((statement, intro, axioms), thy') =
thy
|> def_pred aname parms defs' exts exts';
@@ -737,7 +733,8 @@
val b_satisfy = Element.satisfy_morphism b_axioms;
val params = fixed @
- (body_elems |> map_filter (fn Fixes fixes => SOME fixes | _ => NONE) |> flat);
+ maps (fn Fixes fixes =>
+ map (fn (b, SOME T, mx) => ((Binding.name_of b, T), mx)) fixes | _ => []) body_elems;
val asm = if is_some b_statement then b_statement else a_statement;
val notes =
@@ -790,7 +787,7 @@
fun after_qed witss = ProofContext.theory
(fold2 (fn (name, morph) => fn wits => Locale.add_dependency target
(name, morph $> Element.satisfy_morphism wits $> export)) deps witss #>
- (fn thy => fold_rev Locale.activate_global_facts
+ (fn thy => fold_rev (Context.theory_map o Locale.activate_facts)
(Locale.get_registrations thy) thy));
in Element.witness_proof after_qed propss goal_ctxt end;
@@ -830,7 +827,7 @@
fun store_eqns_activate regs [] thy =
thy
|> fold (fn (name, morph) =>
- Locale.activate_global_facts (name, morph $> export)) regs
+ Context.theory_map (Locale.activate_facts (name, morph $> export))) regs
| store_eqns_activate regs eqs thy =
let
val eqs' = eqs |> map (Morphism.thm (export' $> export));
@@ -842,7 +839,7 @@
thy
|> fold (fn (name, morph) =>
Locale.amend_registration eq_morph (name, morph) #>
- Locale.activate_global_facts (name, morph $> eq_morph $> export)) regs
+ Context.theory_map (Locale.activate_facts (name, morph $> eq_morph $> export))) regs
|> PureThy.note_thmss Thm.lemmaK (eq_attns' ~~ map (fn eq => [([eq], [])]) eqs')
|> snd
end;
@@ -876,7 +873,7 @@
fun store_reg (name, morph) thms =
let
val morph' = morph $> Element.satisfy_morphism thms $> export;
- in Locale.activate_local_facts (name, morph') end;
+ in Context.proof_map (Locale.activate_facts (name, morph')) end;
fun after_qed wits =
Proof.map_context (fold2 store_reg regs wits);
--- a/src/Pure/Isar/local_defs.ML Sun Mar 29 17:25:06 2009 +0200
+++ b/src/Pure/Isar/local_defs.ML Sun Mar 29 17:38:01 2009 +0200
@@ -96,7 +96,7 @@
val lhss = map (fst o Logic.dest_equals) eqs;
in
ctxt
- |> ProofContext.add_fixes_i (map2 (fn x => fn mx => (x, NONE, mx)) bvars mxs) |> #2
+ |> ProofContext.add_fixes (map2 (fn x => fn mx => (x, NONE, mx)) bvars mxs) |> #2
|> fold Variable.declare_term eqs
|> ProofContext.add_assms_i def_export
(map2 (fn a => fn eq => (a, [(eq, [])])) (names ~~ atts) eqs)
@@ -115,7 +115,7 @@
val T = Term.fastype_of rhs;
val ([x'], ctxt') = ctxt
|> Variable.declare_term rhs
- |> ProofContext.add_fixes_i [(x, SOME T, mx)];
+ |> ProofContext.add_fixes [(x, SOME T, mx)];
val lhs = Free (x', T);
val _ = cert_def ctxt' (Logic.mk_equals (lhs, rhs));
fun abbrev_export _ _ = (I, Envir.expand_term_frees [((x', T), rhs)]);
--- a/src/Pure/Isar/locale.ML Sun Mar 29 17:25:06 2009 +0200
+++ b/src/Pure/Isar/locale.ML Sun Mar 29 17:38:01 2009 +0200
@@ -30,7 +30,7 @@
sig
(* Locale specification *)
val register_locale: binding ->
- (string * sort) list * (binding * typ option * mixfix) list ->
+ (string * sort) list * ((string * typ) * mixfix) list ->
term option * term list ->
thm option * thm option -> thm list ->
declaration list * declaration list ->
@@ -39,7 +39,7 @@
val intern: theory -> xstring -> string
val extern: theory -> string -> xstring
val defined: theory -> string -> bool
- val params_of: theory -> string -> (binding * typ option * mixfix) list
+ val params_of: theory -> string -> ((string * typ) * mixfix) list
val intros_of: theory -> string -> thm option * thm option
val axioms_of: theory -> string -> thm list
val instance_of: theory -> string -> morphism -> term list
@@ -56,10 +56,8 @@
val add_dependency: string -> string * morphism -> theory -> theory
(* Activation *)
- val activate_declarations: theory -> string * morphism ->
- Proof.context -> Proof.context
- val activate_global_facts: string * morphism -> theory -> theory
- val activate_local_facts: string * morphism -> Proof.context -> Proof.context
+ val activate_declarations: string * morphism -> Proof.context -> Proof.context
+ val activate_facts: string * morphism -> Context.generic -> Context.generic
val init: string -> theory -> Proof.context
(* Reasoning about locales *)
@@ -91,7 +89,7 @@
datatype locale = Loc of {
(** static part **)
- parameters: (string * sort) list * (binding * typ option * mixfix) list,
+ parameters: (string * sort) list * ((string * typ) * mixfix) list,
(* type and term parameters *)
spec: term option * term list,
(* assumptions (as a single predicate expression) and defines *)
@@ -109,8 +107,10 @@
fun mk_locale ((parameters, spec, intros, axioms), ((decls, notes), dependencies)) =
Loc {parameters = parameters, intros = intros, axioms = axioms, spec = spec,
decls = decls, notes = notes, dependencies = dependencies};
+
fun map_locale f (Loc {parameters, spec, intros, axioms, decls, notes, dependencies}) =
mk_locale (f ((parameters, spec, intros, axioms), ((decls, notes), dependencies)));
+
fun merge_locale (Loc {parameters, spec, intros, axioms, decls = (decls1, decls2),
notes, dependencies}, Loc {decls = (decls1', decls2'), notes = notes',
dependencies = dependencies', ...}) = mk_locale
@@ -163,7 +163,7 @@
fun axioms_of thy = #axioms o the_locale thy;
fun instance_of thy name morph = params_of thy name |>
- map (fn (b, T, _) => Morphism.term morph (Free (Name.of_binding b, the T)));
+ map (Morphism.term morph o Free o #1);
fun specification_of thy = #spec o the_locale thy;
@@ -178,26 +178,20 @@
(** Identifiers: activated locales in theory or proof context **)
-type identifiers = (string * term list) list;
-
-val empty = ([] : identifiers);
-
fun ident_eq thy ((n: string, ts), (m, ss)) = (m = n) andalso Pattern.matchess thy (ss, ts);
local
-datatype 'a delayed = Ready of 'a | ToDo of ('a delayed * 'a delayed);
+datatype 'a delayed = Ready of 'a | ToDo of 'a delayed * 'a delayed;
structure Identifiers = GenericDataFun
(
- type T = identifiers delayed;
- val empty = Ready empty;
+ type T = (string * term list) list delayed;
+ val empty = Ready [];
val extend = I;
fun merge _ = ToDo;
);
-in
-
fun finish thy (ToDo (i1, i2)) = merge (ident_eq thy) (finish thy i1, finish thy i2)
| finish _ (Ready ids) = ids;
@@ -206,13 +200,10 @@
Ready _ => NONE
| ids => SOME (Context.theory_map (Identifiers.put (Ready (finish thy ids))) thy)))));
-fun get_global_idents thy =
- let val (Ready ids) = (Identifiers.get o Context.Theory) thy in ids end;
-val put_global_idents = Context.theory_map o Identifiers.put o Ready;
+in
-fun get_local_idents ctxt =
- let val (Ready ids) = (Identifiers.get o Context.Proof) ctxt in ids end;
-val put_local_idents = Context.proof_map o Identifiers.put o Ready;
+val get_idents = (fn Ready ids => ids) o Identifiers.get;
+val put_idents = Identifiers.put o Ready;
end;
@@ -228,15 +219,14 @@
then error "Roundup bound exceeded (sublocale relation probably not terminating)."
else
let
- val {parameters = (_, params), dependencies, ...} = the_locale thy name;
+ val dependencies = dependencies_of thy name;
val instance = instance_of thy name morph;
in
if member (ident_eq thy) marked (name, instance)
then (deps, marked)
else
let
- val dependencies' =
- map (fn ((name, morph'), _) => (name, morph' $> morph)) dependencies;
+ val dependencies' = map (fn (name, morph') => (name, morph' $> morph)) dependencies;
val marked' = (name, instance) :: marked;
val (deps', marked'') = fold_rev (add thy (depth + 1)) dependencies' ([], marked');
in
@@ -250,7 +240,7 @@
let
(* Find all dependencies incuding new ones (which are dependencies enriching
existing registrations). *)
- val (dependencies, marked') = add thy 0 (name, morph) ([], empty);
+ val (dependencies, marked') = add thy 0 (name, morph) ([], []);
(* Filter out exisiting fragments. *)
val dependencies' = filter_out (fn (name, morph) =>
member (ident_eq thy) marked (name, instance_of thy name morph)) dependencies;
@@ -263,12 +253,14 @@
(* Declarations, facts and entire locale content *)
-fun activate_decls thy (name, morph) ctxt =
+fun activate_decls (name, morph) context =
let
+ val thy = Context.theory_of context;
val {decls = (typ_decls, term_decls), ...} = the_locale thy name;
in
- ctxt |> fold_rev (fn (decl, _) => Context.proof_map (decl morph)) typ_decls |>
- fold_rev (fn (decl, _) => Context.proof_map (decl morph)) term_decls
+ context
+ |> fold_rev (fn (decl, _) => decl morph) typ_decls
+ |> fold_rev (fn (decl, _) => decl morph) term_decls
end;
fun activate_notes activ_elem transfer thy (name, morph) input =
@@ -284,17 +276,17 @@
fun activate_all name thy activ_elem transfer (marked, input) =
let
- val {parameters = (_, params), spec = (asm, defs), ...} =
- the_locale thy name;
- in
- input |>
- (if not (null params) then activ_elem (Fixes params) else I) |>
+ val {parameters = (_, params), spec = (asm, defs), ...} = the_locale thy name;
+ val input' = input |>
+ (not (null params) ?
+ activ_elem (Fixes (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params))) |>
(* FIXME type parameters *)
- (if is_some asm then activ_elem (Assumes [(Attrib.empty_binding, [(the asm, [])])]) else I) |>
+ (case asm of SOME A => activ_elem (Assumes [(Attrib.empty_binding, [(A, [])])]) | _ => I) |>
(if not (null defs)
then activ_elem (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs))
- else I) |>
- pair marked |> roundup thy (activate_notes activ_elem transfer) (name, Morphism.identity)
+ else I);
+ in
+ roundup thy (activate_notes activ_elem transfer) (name, Morphism.identity) (marked, input')
end;
@@ -302,64 +294,65 @@
local
-fun init_global_elem (Notes (kind, facts)) thy =
- let
- val facts' = Attrib.map_facts (Attrib.attribute_i thy) facts
- in PureThy.note_thmss kind facts' thy |> snd end
-
-fun init_local_elem (Fixes fixes) ctxt = ctxt |>
- ProofContext.add_fixes_i fixes |> snd
- | init_local_elem (Assumes assms) ctxt =
+fun init_elem (Fixes fixes) (Context.Proof ctxt) =
+ Context.Proof (ProofContext.add_fixes fixes ctxt |> snd)
+ | init_elem (Assumes assms) (Context.Proof ctxt) =
let
- val assms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) assms
- in
- ctxt |> fold Variable.auto_fixes (maps (map fst o snd) assms') |>
- ProofContext.add_assms_i Assumption.assume_export assms' |> snd
- end
- | init_local_elem (Defines defs) ctxt =
+ val assms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) assms;
+ val ctxt' = ctxt
+ |> fold Variable.auto_fixes (maps (map fst o snd) assms')
+ |> ProofContext.add_assms_i Assumption.assume_export assms' |> snd;
+ in Context.Proof ctxt' end
+ | init_elem (Defines defs) (Context.Proof ctxt) =
let
- val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs
- in
- ctxt |> fold Variable.auto_fixes (map (fst o snd) defs') |>
- ProofContext.add_assms_i LocalDefs.def_export (map (fn (attn, t) => (attn, [t])) defs') |>
- snd
- end
- | init_local_elem (Notes (kind, facts)) ctxt =
+ val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
+ val ctxt' = ctxt
+ |> fold Variable.auto_fixes (map (fst o snd) defs')
+ |> ProofContext.add_assms_i LocalDefs.def_export (map (fn (attn, t) => (attn, [t])) defs')
+ |> snd;
+ in Context.Proof ctxt' end
+ | init_elem (Notes (kind, facts)) (Context.Proof ctxt) =
let
val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts
- in ProofContext.note_thmss_i kind facts' ctxt |> snd end
-
-fun cons_elem false (Notes notes) elems = elems
- | cons_elem _ elem elems = elem :: elems
+ in Context.Proof (ProofContext.note_thmss kind facts' ctxt |> snd) end
+ | init_elem (Notes (kind, facts)) (Context.Theory thy) =
+ let
+ val facts' = Attrib.map_facts (Attrib.attribute_i thy) facts
+ in Context.Theory (PureThy.note_thmss kind facts' thy |> snd) end
+ | init_elem _ (Context.Theory _) = raise Fail "Bad context element in global theory";
in
-fun activate_declarations thy dep ctxt =
- roundup thy activate_decls dep (get_local_idents ctxt, ctxt) |-> put_local_idents;
+fun activate_declarations dep ctxt =
+ let
+ val context = Context.Proof ctxt;
+ val thy = Context.theory_of context;
+ val context' = roundup thy (K activate_decls) dep (get_idents context, context) |-> put_idents;
+ in Context.the_proof context' end;
-fun activate_global_facts dep thy =
- roundup thy (activate_notes init_global_elem Element.transfer_morphism)
- dep (get_global_idents thy, thy) |-> put_global_idents;
-
-fun activate_local_facts dep ctxt =
- roundup (ProofContext.theory_of ctxt)
- (activate_notes init_local_elem (Element.transfer_morphism o ProofContext.theory_of)) dep
- (get_local_idents ctxt, ctxt) |-> put_local_idents;
+fun activate_facts dep context =
+ let
+ val thy = Context.theory_of context;
+ val activate = activate_notes init_elem (Element.transfer_morphism o Context.theory_of);
+ in roundup thy activate dep (get_idents context, context) |-> put_idents end;
fun init name thy =
- activate_all name thy init_local_elem (Element.transfer_morphism o ProofContext.theory_of)
- (empty, ProofContext.init thy) |-> put_local_idents;
+ activate_all name thy init_elem (Element.transfer_morphism o Context.theory_of)
+ ([], Context.Proof (ProofContext.init thy)) |-> put_idents |> Context.proof_of;
-fun print_locale thy show_facts name =
+fun print_locale thy show_facts raw_name =
let
- val name' = intern thy name;
- val ctxt = init name' thy
+ val name = intern thy raw_name;
+ val ctxt = init name thy;
+ fun cons_elem (elem as Notes _) = show_facts ? cons elem
+ | cons_elem elem = cons elem;
+ val elems =
+ activate_all name thy cons_elem (K (Element.transfer_morphism thy)) ([], [])
+ |> snd |> rev;
in
- Pretty.big_list "locale elements:"
- (activate_all name' thy (cons_elem show_facts) (K (Element.transfer_morphism thy))
- (empty, []) |> snd |> rev |>
- map (Element.pretty_ctxt ctxt) |> map Pretty.chunks) |> Pretty.writeln
- end
+ Pretty.big_list "locale elements:" (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)
+ |> Pretty.writeln
+ end;
end;
@@ -379,24 +372,25 @@
);
val get_registrations =
- Registrations.get #> map fst #> map (apsnd op $>);
+ Registrations.get #> map (#1 #> apsnd op $>);
fun add_registration (name, (base_morph, export)) thy =
roundup thy (fn _ => fn (name', morph') =>
- (Registrations.map o cons) ((name', (morph', export)), stamp ()))
- (name, base_morph) (get_global_idents thy, thy) |> snd
- (* FIXME |-> put_global_idents ?*);
+ Registrations.map (cons ((name', (morph', export)), stamp ())))
+ (name, base_morph) (get_idents (Context.Theory thy), thy) |> snd;
+ (* FIXME |-> put_global_idents ?*)
fun amend_registration morph (name, base_morph) thy =
let
- val regs = (Registrations.get #> map fst) thy;
+ val regs = map #1 (Registrations.get thy);
val base = instance_of thy name base_morph;
fun match (name', (morph', _)) =
name = name' andalso eq_list (op aconv) (base, instance_of thy name' morph');
val i = find_index match (rev regs);
- val _ = if i = ~1 then error ("No registration of locale " ^
+ val _ =
+ if i = ~1 then error ("No registration of locale " ^
quote (extern thy name) ^ " and parameter instantiation " ^
- space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^ " available.")
+ space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^ " available")
else ();
in
Registrations.map (nth_map (length regs - 1 - i)
--- a/src/Pure/Isar/obtain.ML Sun Mar 29 17:25:06 2009 +0200
+++ b/src/Pure/Isar/obtain.ML Sun Mar 29 17:38:01 2009 +0200
@@ -118,7 +118,7 @@
(*obtain vars*)
val (vars, vars_ctxt) = prep_vars raw_vars ctxt;
- val (_, fix_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars;
+ val (_, fix_ctxt) = vars_ctxt |> ProofContext.add_fixes vars;
val xs = map (Name.of_binding o #1) vars;
(*obtain asms*)
@@ -294,7 +294,7 @@
|> Proof.fix_i (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) parms)
|> `Proof.context_of |-> (fn fix_ctxt => Proof.assm_i
(obtain_export fix_ctxt rule (map cert ts)) [(Thm.empty_binding, asms)])
- |> Proof.add_binds_i AutoBind.no_facts
+ |> Proof.bind_terms AutoBind.no_facts
end;
val goal = Var (("guess", 0), propT);
--- a/src/Pure/Isar/proof.ML Sun Mar 29 17:25:06 2009 +0200
+++ b/src/Pure/Isar/proof.ML Sun Mar 29 17:38:01 2009 +0200
@@ -17,7 +17,7 @@
val theory_of: state -> theory
val map_context: (context -> context) -> state -> state
val map_contexts: (context -> context) -> state -> state
- val add_binds_i: (indexname * term option) list -> state -> state
+ val bind_terms: (indexname * term option) list -> state -> state
val put_thms: bool -> string * thm list option -> state -> state
val the_facts: state -> thm list
val the_fact: state -> thm
@@ -204,7 +204,7 @@
fun map_contexts f = map_all (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));
-val add_binds_i = map_context o ProofContext.add_binds_i;
+val bind_terms = map_context o ProofContext.bind_terms;
val put_thms = map_context oo ProofContext.put_thms;
@@ -531,15 +531,15 @@
local
-fun gen_fix add_fixes args =
+fun gen_fix prep_vars args =
assert_forward
- #> map_context (snd o add_fixes args)
+ #> map_context (fn ctxt => snd (ProofContext.add_fixes (prep_vars ctxt args) ctxt))
#> put_facts NONE;
in
-val fix = gen_fix ProofContext.add_fixes;
-val fix_i = gen_fix ProofContext.add_fixes_i;
+val fix = gen_fix (fn ctxt => fn args => fst (ProofContext.read_vars args ctxt));
+val fix_i = gen_fix (K I);
end;
@@ -620,29 +620,27 @@
local
-fun gen_thmss note_ctxt more_facts opt_chain opt_result prep_atts args state =
+fun gen_thmss more_facts opt_chain opt_result prep_atts prep_fact args state =
state
|> assert_forward
- |> map_context_result (note_ctxt (Attrib.map_facts (prep_atts (theory_of state)) args))
+ |> map_context_result (ProofContext.note_thmss ""
+ (Attrib.map_facts_refs (prep_atts (theory_of state)) (prep_fact (context_of state)) args))
|> these_factss (more_facts state)
||> opt_chain
|> opt_result;
in
-val note_thmss = gen_thmss (ProofContext.note_thmss "") (K []) I #2 Attrib.attribute;
-val note_thmss_i = gen_thmss (ProofContext.note_thmss_i "") (K []) I #2 (K I);
-
-val from_thmss =
- gen_thmss (ProofContext.note_thmss "") (K []) chain #2 Attrib.attribute o no_binding;
-val from_thmss_i = gen_thmss (ProofContext.note_thmss_i "") (K []) chain #2 (K I) o no_binding;
+val note_thmss = gen_thmss (K []) I #2 Attrib.attribute ProofContext.get_fact;
+val note_thmss_i = gen_thmss (K []) I #2 (K I) (K I);
-val with_thmss =
- gen_thmss (ProofContext.note_thmss "") the_facts chain #2 Attrib.attribute o no_binding;
-val with_thmss_i = gen_thmss (ProofContext.note_thmss_i "") the_facts chain #2 (K I) o no_binding;
+val from_thmss = gen_thmss (K []) chain #2 Attrib.attribute ProofContext.get_fact o no_binding;
+val from_thmss_i = gen_thmss (K []) chain #2 (K I) (K I) o no_binding;
-val local_results =
- gen_thmss (ProofContext.note_thmss_i "") (K []) I I (K I) o map (apsnd Thm.simple_fact);
+val with_thmss = gen_thmss the_facts chain #2 Attrib.attribute ProofContext.get_fact o no_binding;
+val with_thmss_i = gen_thmss the_facts chain #2 (K I) (K I) o no_binding;
+
+val local_results = gen_thmss (K []) I I (K I) (K I) o map (apsnd Thm.simple_fact);
fun get_thmss state srcs = the_facts (note_thmss [((Binding.empty, []), srcs)] state);
@@ -653,11 +651,13 @@
local
-fun gen_using f g note prep_atts args state =
+fun gen_using f g prep_atts prep_fact args state =
state
|> assert_backward
|> map_context_result
- (note "" (Attrib.map_facts (prep_atts (theory_of state)) (no_binding args)))
+ (ProofContext.note_thmss ""
+ (Attrib.map_facts_refs (prep_atts (theory_of state)) (prep_fact (context_of state))
+ (no_binding args)))
|> (fn (named_facts, state') =>
state' |> map_goal I (fn (statement, _, using, goal, before_qed, after_qed) =>
let
@@ -671,10 +671,10 @@
in
-val using = gen_using append_using (K (K I)) ProofContext.note_thmss Attrib.attribute;
-val using_i = gen_using append_using (K (K I)) ProofContext.note_thmss_i (K I);
-val unfolding = gen_using unfold_using unfold_goals ProofContext.note_thmss Attrib.attribute;
-val unfolding_i = gen_using unfold_using unfold_goals ProofContext.note_thmss_i (K I);
+val using = gen_using append_using (K (K I)) Attrib.attribute ProofContext.get_fact;
+val using_i = gen_using append_using (K (K I)) (K I) (K I);
+val unfolding = gen_using unfold_using unfold_goals Attrib.attribute ProofContext.get_fact;
+val unfolding_i = gen_using unfold_using unfold_goals (K I) (K I);
end;
@@ -695,7 +695,7 @@
in
state'
|> assume_i assumptions
- |> add_binds_i AutoBind.no_facts
+ |> bind_terms AutoBind.no_facts
|> `the_facts |-> (fn thms => note_thmss_i [((Binding.name name, []), [(thms, [])])])
end;
--- a/src/Pure/Isar/proof_context.ML Sun Mar 29 17:25:06 2009 +0200
+++ b/src/Pure/Isar/proof_context.ML Sun Mar 29 17:38:01 2009 +0200
@@ -70,8 +70,7 @@
val export: Proof.context -> Proof.context -> thm list -> thm list
val export_morphism: Proof.context -> Proof.context -> morphism
val norm_export_morphism: Proof.context -> Proof.context -> morphism
- val add_binds: (indexname * string option) list -> Proof.context -> Proof.context
- val add_binds_i: (indexname * term option) list -> Proof.context -> Proof.context
+ val bind_terms: (indexname * term option) list -> Proof.context -> Proof.context
val auto_bind_goal: term list -> Proof.context -> Proof.context
val auto_bind_facts: term list -> Proof.context -> Proof.context
val match_bind: bool -> (string list * string) list -> Proof.context -> term list * Proof.context
@@ -102,19 +101,15 @@
val mandatory_path: string -> Proof.context -> Proof.context
val restore_naming: Proof.context -> Proof.context -> Proof.context
val reset_naming: Proof.context -> Proof.context
- val note_thmss: string -> (Thm.binding * (Facts.ref * attribute list) list) list ->
- Proof.context -> (string * thm list) list * Proof.context
- val note_thmss_i: string -> (Thm.binding * (thm list * attribute list) list) list ->
+ val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list ->
Proof.context -> (string * thm list) list * Proof.context
val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context
val read_vars: (binding * string option * mixfix) list -> Proof.context ->
(binding * typ option * mixfix) list * Proof.context
val cert_vars: (binding * typ option * mixfix) list -> Proof.context ->
(binding * typ option * mixfix) list * Proof.context
- val add_fixes: (binding * string option * mixfix) list ->
- Proof.context -> string list * Proof.context
- val add_fixes_i: (binding * typ option * mixfix) list ->
- Proof.context -> string list * Proof.context
+ val add_fixes: (binding * typ option * mixfix) list -> Proof.context ->
+ string list * Proof.context
val auto_fixes: Proof.context * (term list list * 'a) -> Proof.context * (term list list * 'a)
val bind_fixes: string list -> Proof.context -> (term -> term) * Proof.context
val add_assms: Assumption.export ->
@@ -542,17 +537,17 @@
local
-structure AllowDummies = ProofDataFun(type T = bool fun init _ = false);
+structure Allow_Dummies = ProofDataFun(type T = bool fun init _ = false);
fun check_dummies ctxt t =
- if AllowDummies.get ctxt then t
+ if Allow_Dummies.get ctxt then t
else Term.no_dummy_patterns t handle TERM _ => error "Illegal dummy pattern(s) in term";
fun prepare_dummies ts = #1 (fold_map Term.replace_dummy_patterns ts 1);
in
-val allow_dummies = AllowDummies.put true;
+val allow_dummies = Allow_Dummies.put true;
fun prepare_patterns ctxt =
let val Mode {pattern, ...} = get_mode ctxt in
@@ -775,7 +770,7 @@
-(** bindings **)
+(** term bindings **)
(* simult_matches *)
@@ -785,28 +780,23 @@
| SOME (env, _) => map (apsnd snd) (Envir.alist_of env));
-(* add_binds(_i) *)
-
-local
+(* bind_terms *)
-fun gen_bind prep (xi as (x, _), raw_t) ctxt =
+val bind_terms = fold (fn (xi, t) => fn ctxt =>
ctxt
- |> Variable.add_binds [(xi, Option.map (prep (set_mode mode_default ctxt)) raw_t)];
+ |> Variable.bind_term (xi, Option.map (cert_term (set_mode mode_default ctxt)) t));
-in
+
+(* auto_bind *)
fun drop_schematic (b as (xi, SOME t)) = if Term.exists_subterm is_Var t then (xi, NONE) else b
| drop_schematic b = b;
-val add_binds = fold (gen_bind Syntax.read_term);
-val add_binds_i = fold (gen_bind cert_term);
+fun auto_bind f ts ctxt = ctxt |> bind_terms (map drop_schematic (f (theory_of ctxt) ts));
-fun auto_bind f ts ctxt = ctxt |> add_binds_i (map drop_schematic (f (theory_of ctxt) ts));
val auto_bind_goal = auto_bind AutoBind.goal;
val auto_bind_facts = auto_bind AutoBind.facts;
-end;
-
(* match_bind(_i) *)
@@ -831,8 +821,8 @@
val ctxt'' =
tap (Variable.warn_extra_tfrees ctxt)
(if gen then
- ctxt (*sic!*) |> fold Variable.declare_term (map #2 binds') |> add_binds_i binds''
- else ctxt' |> add_binds_i binds'');
+ ctxt (*sic!*) |> fold Variable.declare_term (map #2 binds') |> bind_terms binds''
+ else ctxt' |> bind_terms binds'');
in (ts, ctxt'') end;
in
@@ -868,8 +858,8 @@
(*generalize result: context evaluated now, binds added later*)
val gen = Variable.exportT_terms ctxt' ctxt;
- fun gen_binds c = c |> add_binds_i (map #1 binds ~~ map SOME (gen (map #2 binds)));
- in (ctxt' |> add_binds_i (map (apsnd SOME) binds), (propss, gen_binds)) end;
+ fun gen_binds c = c |> bind_terms (map #1 binds ~~ map SOME (gen (map #2 binds)));
+ in (ctxt' |> bind_terms (map (apsnd SOME) binds), (propss, gen_binds)) end;
in
@@ -965,25 +955,23 @@
| update_thms do_props (b, SOME ths) ctxt = ctxt |> map_facts
(Facts.add_local do_props (naming_of ctxt) (b, ths) #> snd);
-fun gen_note_thmss get k = fold_map (fn ((b, more_attrs), raw_facts) => fn ctxt =>
+in
+
+fun note_thmss kind = fold_map (fn ((b, more_attrs), raw_facts) => fn ctxt =>
let
val pos = Binding.pos_of b;
val name = full_name ctxt b;
val _ = ContextPosition.report_visible ctxt (Markup.local_fact_decl name) pos;
- val facts = PureThy.name_thmss false pos name (map (apfst (get ctxt)) raw_facts);
+ val facts = PureThy.name_thmss false pos name raw_facts;
fun app (th, attrs) x =
- swap (Library.foldl_map (Thm.proof_attributes (surround (Thm.kind k) (attrs @ more_attrs))) (x, th));
+ swap (Library.foldl_map
+ (Thm.proof_attributes (surround (Thm.kind kind) (attrs @ more_attrs))) (x, th));
val (res, ctxt') = fold_map app facts ctxt;
val thms = PureThy.name_thms false false pos name (flat res);
val Mode {stmt, ...} = get_mode ctxt;
in ((name, thms), ctxt' |> update_thms stmt (b, SOME thms)) end);
-in
-
-fun note_thmss k = gen_note_thmss get_fact k;
-fun note_thmss_i k = gen_note_thmss (K I) k;
-
fun put_thms do_props thms ctxt = ctxt
|> map_naming (K local_naming)
|> ContextPosition.set_visible false
@@ -1115,9 +1103,11 @@
error ("Illegal mixfix syntax for internal/skolem constant " ^ quote x)
else (true, (x, T, mx));
-fun gen_fixes prep raw_vars ctxt =
+in
+
+fun add_fixes raw_vars ctxt =
let
- val (vars, _) = prep raw_vars ctxt;
+ val (vars, _) = cert_vars raw_vars ctxt;
val (xs', ctxt') = Variable.add_fixes (map (Name.of_binding o #1) vars) ctxt;
val ctxt'' =
ctxt'
@@ -1127,11 +1117,6 @@
ContextPosition.report_visible ctxt (Markup.fixed_decl x') (Binding.pos_of b));
in (xs', ctxt'') end;
-in
-
-val add_fixes = gen_fixes read_vars;
-val add_fixes_i = gen_fixes cert_vars;
-
end;
@@ -1142,7 +1127,7 @@
fun bind_fixes xs ctxt =
let
- val (_, ctxt') = ctxt |> add_fixes_i (map (fn x => (Binding.name x, NONE, NoSyn)) xs);
+ val (_, ctxt') = ctxt |> add_fixes (map (fn x => (Binding.name x, NONE, NoSyn)) xs);
fun bind (t as Free (x, T)) =
if member (op =) xs x then
(case lookup_skolem ctxt' x of SOME x' => Free (x', T) | NONE => t)
@@ -1167,7 +1152,7 @@
in
ctxt2
|> auto_bind_facts (flat propss)
- |> note_thmss_i Thm.assumptionK (map fst args ~~ map (map (fn th => ([th], []))) premss)
+ |> note_thmss Thm.assumptionK (map fst args ~~ map (map (fn th => ([th], []))) premss)
end;
in
@@ -1221,7 +1206,7 @@
val RuleCases.Case {assumes, binds, cases, ...} = RuleCases.apply ts c;
in
ctxt'
- |> add_binds_i (map drop_schematic binds)
+ |> bind_terms (map drop_schematic binds)
|> add_cases true (map (apsnd SOME) cases)
|> pair (assumes, (binds, cases))
end;
--- a/src/Pure/Isar/rule_insts.ML Sun Mar 29 17:25:06 2009 +0200
+++ b/src/Pure/Isar/rule_insts.ML Sun Mar 29 17:38:01 2009 +0200
@@ -283,7 +283,7 @@
val (param_names, ctxt') = ctxt
|> Variable.declare_thm thm
|> Thm.fold_terms Variable.declare_constraints st
- |> ProofContext.add_fixes_i (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) params);
+ |> ProofContext.add_fixes (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) params);
(* Process type insts: Tinsts_env *)
fun absent xi = error
--- a/src/Pure/Isar/specification.ML Sun Mar 29 17:25:06 2009 +0200
+++ b/src/Pure/Isar/specification.ML Sun Mar 29 17:38:01 2009 +0200
@@ -108,7 +108,7 @@
val thy = ProofContext.theory_of ctxt;
val (vars, vars_ctxt) = ctxt |> prep_vars raw_vars;
- val (xs, params_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars;
+ val (xs, params_ctxt) = vars_ctxt |> ProofContext.add_fixes vars;
val Asss = (map o map) (map (parse_prop params_ctxt) o snd) raw_specss;
val names = Variable.names_of (params_ctxt |> (fold o fold o fold) Variable.declare_term Asss)
@@ -312,7 +312,7 @@
|> fold_map ProofContext.inferred_param xs;
val asm = Term.list_all_free (xs ~~ Ts, Logic.list_implies (props, thesis));
in
- ctxt' |> (snd o ProofContext.add_fixes_i (map (fn b => (b, NONE, NoSyn)) bs));
+ ctxt' |> (snd o ProofContext.add_fixes (map (fn b => (b, NONE, NoSyn)) bs));
ctxt' |> Variable.auto_fixes asm
|> ProofContext.add_assms_i Assumption.assume_export
[((name, [ContextRules.intro_query NONE]), [(asm, [])])]
@@ -325,9 +325,9 @@
val stmt = [((Binding.empty, atts), [(thesis, [])])];
val (facts, goal_ctxt) = elems_ctxt
- |> (snd o ProofContext.add_fixes_i [(Binding.name AutoBind.thesisN, NONE, NoSyn)])
+ |> (snd o ProofContext.add_fixes [(Binding.name AutoBind.thesisN, NONE, NoSyn)])
|> fold_map assume_case (obtains ~~ propp)
- |-> (fn ths => ProofContext.note_thmss_i Thm.assumptionK
+ |-> (fn ths => ProofContext.note_thmss Thm.assumptionK
[((Binding.name Obtain.thatN, []), [(ths, [])])] #> #2 #> pair ths);
in ((prems, stmt, facts), goal_ctxt) end);
@@ -370,7 +370,7 @@
end;
in
goal_ctxt
- |> ProofContext.note_thmss_i Thm.assumptionK
+ |> ProofContext.note_thmss Thm.assumptionK
[((Binding.name AutoBind.assmsN, []), [(prems, [])])]
|> snd
|> Proof.theorem_i before_qed after_qed' (map snd stmt)
--- a/src/Pure/Isar/theory_target.ML Sun Mar 29 17:25:06 2009 +0200
+++ b/src/Pure/Isar/theory_target.ML Sun Mar 29 17:38:01 2009 +0200
@@ -160,9 +160,9 @@
in
lthy |> LocalTheory.theory
(PureThy.note_thmss_grouped kind (LocalTheory.group_of lthy) global_facts #> snd)
- |> not is_locale ? LocalTheory.target (ProofContext.note_thmss_i kind global_facts #> snd)
+ |> not is_locale ? LocalTheory.target (ProofContext.note_thmss kind global_facts #> snd)
|> is_locale ? LocalTheory.target (Locale.add_thmss target kind target_facts)
- |> ProofContext.note_thmss_i kind local_facts
+ |> ProofContext.note_thmss kind local_facts
end;
--- a/src/Pure/ML/ml_antiquote.ML Sun Mar 29 17:25:06 2009 +0200
+++ b/src/Pure/ML/ml_antiquote.ML Sun Mar 29 17:38:01 2009 +0200
@@ -87,7 +87,7 @@
val _ = macro "note" (Args.context :|-- (fn ctxt =>
P.and_list1' (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms >> (fn ((a, srcs), ths) =>
((a, map (Attrib.attribute (ProofContext.theory_of ctxt)) srcs), [(ths, [])])))
- >> (fn args => #2 (ProofContext.note_thmss_i "" args ctxt))));
+ >> (fn args => #2 (ProofContext.note_thmss "" args ctxt))));
val _ = value "ctyp" (Args.typ >> (fn T =>
"Thm.ctyp_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_typ T)));
--- a/src/Pure/variable.ML Sun Mar 29 17:25:06 2009 +0200
+++ b/src/Pure/variable.ML Sun Mar 29 17:38:01 2009 +0200
@@ -30,7 +30,7 @@
val declare_thm: thm -> Proof.context -> Proof.context
val thm_context: thm -> Proof.context
val variant_frees: Proof.context -> term list -> (string * 'a) list -> (string * 'a) list
- val add_binds: (indexname * term option) list -> Proof.context -> Proof.context
+ val bind_term: indexname * term option -> Proof.context -> Proof.context
val expand_binds: Proof.context -> term -> term
val lookup_const: Proof.context -> string -> string option
val is_const: Proof.context -> string -> bool
@@ -250,15 +250,13 @@
(** term bindings **)
-fun add_bind (xi, NONE) = map_binds (Vartab.delete_safe xi)
- | add_bind ((x, i), SOME t) =
+fun bind_term (xi, NONE) = map_binds (Vartab.delete_safe xi)
+ | bind_term ((x, i), SOME t) =
let
val u = Term.close_schematic_term t;
val U = Term.fastype_of u;
in declare_term u #> map_binds (Vartab.update ((x, i), (U, u))) end;
-val add_binds = fold add_bind;
-
fun expand_binds ctxt =
let
val binds = binds_of ctxt;
@@ -486,7 +484,7 @@
val all_vars = Thm.fold_terms Term.add_vars st [];
val no_binds = map (fn (xi, _) => (xi, NONE)) all_vars;
in
- add_binds no_binds #>
+ fold bind_term no_binds #>
fold (declare_constraints o Var) all_vars #>
focus (Thm.cprem_of st i)
end;
--- a/src/Tools/code/code_target.ML Sun Mar 29 17:25:06 2009 +0200
+++ b/src/Tools/code/code_target.ML Sun Mar 29 17:38:01 2009 +0200
@@ -411,7 +411,7 @@
val names_hidden = names_class @ names_inst @ names_tyco @ names_const;
val names2 = subtract (op =) names_hidden names1;
val program3 = Graph.subgraph (not o member (op =) names_hidden) program2;
- val names_all = Graph.all_succs program2 names2;
+ val names_all = Graph.all_succs program3 names2;
val includes = abs_includes names_all;
val program4 = Graph.subgraph (member (op =) names_all) program3;
val empty_funs = filter_out (member (op =) abortable)
--- a/src/Tools/code/code_wellsorted.ML Sun Mar 29 17:25:06 2009 +0200
+++ b/src/Tools/code/code_wellsorted.ML Sun Mar 29 17:38:01 2009 +0200
@@ -353,14 +353,20 @@
fun code_deps thy consts =
let
val eqngr = code_depgr thy consts;
- fun mk_entry (const, (_, (_, parents))) =
- let
- val name = Code_Unit.string_of_const thy const;
- val nameparents = map (Code_Unit.string_of_const thy) parents;
- in { name = name, ID = name, dir = "", unfold = true,
- path = "", parents = nameparents }
- end;
- val prgr = Graph.fold ((fn x => fn xs => xs @ [x]) o mk_entry) eqngr [];
+ val constss = Graph.strong_conn eqngr;
+ val mapping = Symtab.empty |> fold (fn consts => fold (fn const =>
+ Symtab.update (const, consts)) consts) constss;
+ fun succs consts = consts
+ |> maps (Graph.imm_succs eqngr)
+ |> subtract (op =) consts
+ |> map (the o Symtab.lookup mapping)
+ |> distinct (op =);
+ val conn = [] |> fold (fn consts => cons (consts, succs consts)) constss;
+ fun namify consts = map (Code_Unit.string_of_const thy) consts
+ |> commas;
+ val prgr = map (fn (consts, constss) =>
+ { name = namify consts, ID = namify consts, dir = "", unfold = true,
+ path = "", parents = map namify constss }) conn;
in Present.display_graph prgr end;
local