--- a/src/HOL/SPARK/Tools/spark_vcs.ML Sat Nov 19 12:42:21 2011 +0100
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML Sat Nov 19 17:20:17 2011 +0100
@@ -880,10 +880,6 @@
prefix = prefix}}
| x => x);
-fun write_prv path s =
- let val path_prv = Path.ext "prv" path;
- in if try File.read path_prv = SOME s then () else File.write path_prv s end;
-
fun close thy =
thy |>
VCs.map (fn
@@ -892,7 +888,7 @@
(if is_some p then apfst else apsnd) (cons vc)) vcs ([], []) of
(proved, []) =>
(Thm.join_proofs (maps (the o #2 o snd) proved);
- write_prv path
+ File.write (Path.ext "prv" path)
(implode (map (fn (s, _) => snd (strip_number s) ^
" -- proved by " ^ Distribution.version ^ "\n") proved));
{pfuns = pfuns, type_map = type_map, env = NONE})
--- a/src/Pure/Isar/attrib.ML Sat Nov 19 12:42:21 2011 +0100
+++ b/src/Pure/Isar/attrib.ML Sat Nov 19 17:20:17 2011 +0100
@@ -9,6 +9,7 @@
type src = Args.src
type binding = binding * src list
val empty_binding: binding
+ val is_empty_binding: binding -> bool
val print_attributes: theory -> unit
val intern: theory -> xstring -> string
val intern_src: theory -> src -> src
@@ -60,7 +61,9 @@
type src = Args.src;
type binding = binding * src list;
+
val empty_binding: binding = (Binding.empty, []);
+fun is_empty_binding ((b, srcs): binding) = Binding.is_empty b andalso null srcs;
@@ -216,11 +219,11 @@
-(** partial evaluation **)
+(** partial evaluation -- observing rule/declaration/mixed attributes **)
local
-val strict_thm_eq = op = o pairself Thm.rep_thm;
+val strict_eq_thm = op = o pairself Thm.rep_thm;
fun apply_att src (context, th) =
let
@@ -243,7 +246,7 @@
(case decls of
[] => [(th, [src'])]
| (th2, srcs2) :: rest =>
- if strict_thm_eq (th, th2)
+ if strict_eq_thm (th, th2)
then ((th2, src' :: srcs2) :: rest)
else (th, [src']) :: (th2, srcs2) :: rest);
in ((th, NONE), (decls', context')) end
@@ -260,25 +263,27 @@
in
fun partial_evaluation ctxt facts =
- let
- val (facts', (decls, _)) =
- (facts, ([], Context.Proof (Context_Position.set_visible false ctxt))) |->
- fold_map (fn ((b, more_atts), fact) => fn res =>
- let
- val (fact', res') =
- (fact, res) |-> fold_map (fn (ths, atts) => fn res1 =>
- (ths, res1) |-> fold_map (fn th => fn res2 =>
- let
- val ((th', dyn'), res3) = fold eval (atts @ more_atts) ((th, NONE), res2);
- val th_atts' =
- (case dyn' of
- NONE => ([th'], [])
- | SOME (dyn_th', atts') => ([dyn_th'], rev atts'));
- in (th_atts', res3) end))
- |>> flat;
- in (((b, []), fact'), res') end);
- val decl_fact = (empty_binding, rev (map (fn (th, atts) => ([th], rev atts)) decls));
- in decl_fact :: facts' end;
+ (facts, Context.Proof (Context_Position.set_visible false ctxt)) |->
+ fold_map (fn ((b, more_atts), fact) => fn context =>
+ let
+ val (fact', (decls, context')) =
+ (fact, ([], context)) |-> fold_map (fn (ths, atts) => fn res1 =>
+ (ths, res1) |-> fold_map (fn th => fn res2 =>
+ let
+ val ((th', dyn'), res3) = fold eval (atts @ more_atts) ((th, NONE), res2);
+ val th_atts' =
+ (case dyn' of
+ NONE => (th', [])
+ | SOME (dyn_th', atts') => (dyn_th', rev atts'));
+ in (th_atts', res3) end))
+ |>> flat;
+ val decls' = rev (map (apsnd rev) decls);
+ val facts' =
+ if eq_list (eq_fst strict_eq_thm) (decls', fact') then
+ [((b, []), map2 (fn (th, atts1) => fn (_, atts2) => (th, atts1 @ atts2)) decls' fact')]
+ else [(empty_binding, decls'), ((b, []), fact')];
+ in (facts', context') end)
+ |> fst |> flat |> map (apsnd (map (apfst single)));
end;
--- a/src/Pure/Isar/element.ML Sat Nov 19 12:42:21 2011 +0100
+++ b/src/Pure/Isar/element.ML Sat Nov 19 17:20:17 2011 +0100
@@ -119,7 +119,7 @@
map (fn y => Pretty.block [Pretty.str " ", Pretty.keyword sep, Pretty.brk 1, y]) ys;
fun pretty_name_atts ctxt (b, atts) sep =
- if Binding.is_empty b andalso null atts then []
+ if Attrib.is_empty_binding (b, atts) then []
else
[Pretty.block (Pretty.breaks
(Binding.pretty b :: Attrib.pretty_attribs ctxt atts @ [Pretty.str sep]))];
--- a/src/Pure/Isar/expression.ML Sat Nov 19 12:42:21 2011 +0100
+++ b/src/Pure/Isar/expression.ML Sat Nov 19 17:20:17 2011 +0100
@@ -354,8 +354,9 @@
let
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 (Type_Infer.paramify_vars o
- Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT_global) parm_types;
+ val parm_types' = parm_types
+ |> map (Type_Infer.paramify_vars o
+ Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT_global);
val inst'' = map2 Type.constraint parm_types' inst';
val insts' = insts @ [(loc, (prfx, inst''))];
val (insts'', _, _, ctxt' (* FIXME not used *) ) = check_autofix insts' [] [] ctxt;
@@ -806,37 +807,34 @@
|> Variable.export_terms deps_ctxt ctxt
end;
+fun meta_rewrite ctxt = map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def);
+
+
(** Interpretation in theories and proof contexts **)
local
fun note_eqns_register deps witss attrss eqns export export' context =
- let
- fun meta_rewrite context =
- map (Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def) o
- maps snd;
- in
- context
- |> Element.generic_note_thmss Thm.lemmaK
- (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns)
- |-> (fn facts => `(fn context => meta_rewrite context facts))
- |-> (fn eqns => fold (fn ((dep, morph), wits) =>
- fn context =>
- Locale.add_registration (dep, morph $> Element.satisfy_morphism
- (map (Element.transform_witness export') wits))
- (Element.eq_morphism (Context.theory_of context) eqns |>
- Option.map (rpair true))
- export context) (deps ~~ witss))
- end;
+ context
+ |> Element.generic_note_thmss Thm.lemmaK
+ (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns)
+ |-> (fn facts => `(fn context => meta_rewrite (Context.proof_of context) (maps snd facts)))
+ |-> (fn eqns => fold (fn ((dep, morph), wits) =>
+ fn context =>
+ Locale.add_registration (dep, morph $> Element.satisfy_morphism
+ (map (Element.transform_witness export') wits))
+ (Element.eq_morphism (Context.theory_of context) eqns |>
+ Option.map (rpair true))
+ export context) (deps ~~ witss));
fun gen_interpretation prep_expr parse_prop prep_attr
- expression equations theory =
+ expression equations thy =
let
- val ((propss, deps, export), expr_ctxt) = Proof_Context.init_global theory
+ val ((propss, deps, export), expr_ctxt) = Proof_Context.init_global thy
|> prep_expr expression;
val eqns = read_with_extended_syntax parse_prop deps expr_ctxt equations;
- val attrss = map ((apsnd o map) (prep_attr theory) o fst) equations;
+ val attrss = map (apsnd (map (prep_attr thy)) o fst) equations;
val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
val export' = Variable.export_morphism goal_ctxt expr_ctxt;
@@ -851,17 +849,18 @@
let
val _ = Proof.assert_forward_or_chain state;
val ctxt = Proof.context_of state;
- val theory = Proof_Context.theory_of ctxt;
+ val thy = Proof_Context.theory_of ctxt;
val ((propss, deps, export), expr_ctxt) = prep_expr expression ctxt;
val eqns = read_with_extended_syntax parse_prop deps expr_ctxt equations;
- val attrss = map ((apsnd o map) (prep_attr theory) o fst) equations;
+ val attrss = map (apsnd (map (prep_attr thy)) o fst) equations;
val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
val export' = Variable.export_morphism goal_ctxt expr_ctxt;
- fun after_qed witss eqns = (Proof.map_context o Context.proof_map)
- (note_eqns_register deps witss attrss eqns export export');
+ fun after_qed witss eqns =
+ (Proof.map_context o Context.proof_map)
+ (note_eqns_register deps witss attrss eqns export export');
in
state
|> Element.witness_local_proof_eqs after_qed "interpret" propss eqns goal_ctxt int
@@ -886,25 +885,24 @@
fun note_eqns_dependency target deps witss attrss eqns export export' ctxt =
let
- fun meta_rewrite ctxt =
- map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) o maps snd;
+ val thy = Proof_Context.theory_of ctxt;
+
val facts =
(attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns);
- val eqns' = ctxt |> Context.Proof
- |> Element.generic_note_thmss Thm.lemmaK facts
- |> apsnd Context.the_proof (* FIXME Context.proof_map_result *)
- |-> (fn facts => `(fn ctxt => meta_rewrite ctxt facts))
+ val eqns' = ctxt
+ |> Proof_Context.note_thmss Thm.lemmaK (Attrib.map_facts (map (Attrib.attribute_i thy)) facts)
+ |-> (fn facts => `(fn ctxt => meta_rewrite ctxt (maps snd facts)))
|> fst; (* FIXME duplication to add_thmss *)
in
ctxt
- |> Locale.add_thmss target Thm.lemmaK facts
+ |> Locale.add_thmss target Thm.lemmaK (Attrib.partial_evaluation ctxt facts)
|> Proof_Context.background_theory (fold (fn ((dep, morph), wits) =>
- fn theory =>
+ fn thy =>
Locale.add_dependency target
(dep, morph $> Element.satisfy_morphism
(map (Element.transform_witness export') wits))
- (Element.eq_morphism theory eqns' |> Option.map (rpair true))
- export theory) (deps ~~ witss))
+ (Element.eq_morphism thy eqns' |> Option.map (rpair true))
+ export thy) (deps ~~ witss))
end;
fun gen_sublocale prep_expr intern parse_prop prep_attr
@@ -915,7 +913,7 @@
val ((propss, deps, export), expr_ctxt) = prep_expr expression target_ctxt;
val eqns = read_with_extended_syntax parse_prop deps expr_ctxt equations;
- val attrss = map ((apsnd o map) (prep_attr thy) o fst) equations;
+ val attrss = map (apsnd (map (prep_attr thy)) o fst) equations;
val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
val export' = Variable.export_morphism goal_ctxt expr_ctxt;
--- a/src/Pure/Isar/locale.ML Sat Nov 19 12:42:21 2011 +0100
+++ b/src/Pure/Isar/locale.ML Sat Nov 19 17:20:17 2011 +0100
@@ -343,7 +343,7 @@
val empty = (Idtab.empty, Inttab.empty);
val extend = I;
fun merge ((reg1, mix1), (reg2, mix2)) : T =
- (Idtab.join (fn id => fn (r1 as (_, s1), r2 as (_, s2)) =>
+ (Idtab.join (fn id => fn ((_, s1), (_, s2)) =>
if s1 = s2 then raise Idtab.SAME else raise Idtab.DUP id) (reg1, reg2),
merge_mixins (mix1, mix2))
handle Idtab.DUP id =>
@@ -462,7 +462,8 @@
fun activate_facts export dep context =
let
val thy = Context.theory_of context;
- val activate = activate_notes Element.init (Element.transfer_morphism o Context.theory_of) context export;
+ val activate =
+ activate_notes Element.init (Element.transfer_morphism o Context.theory_of) context export;
in
roundup thy activate (case export of NONE => Morphism.identity | SOME export => export)
dep (get_idents context, context)
@@ -556,20 +557,20 @@
(* Theorems *)
fun add_thmss loc kind facts ctxt =
- let
- val (Notes facts', ctxt') = Element.activate_i (Notes (kind, facts)) ctxt;
- val ctxt'' = ctxt' |> Proof_Context.background_theory
- ((change_locale loc o apfst o apsnd) (cons (facts', serial ()))
- #>
+ ctxt
+ |> Proof_Context.note_thmss kind
+ (Attrib.map_facts (map (Attrib.attribute_i (Proof_Context.theory_of ctxt))) facts)
+ |> snd
+ |> Proof_Context.background_theory
+ ((change_locale loc o apfst o apsnd) (cons ((kind, facts), serial ())) #>
(* Registrations *)
(fn thy => fold_rev (fn (_, morph) =>
let
- val facts'' = snd facts'
+ val facts' = facts
|> Element.facts_map (Element.transform_ctxt morph)
|> Attrib.map_facts (map (Attrib.attribute_i thy));
- in Global_Theory.note_thmss kind facts'' #> snd end)
- (registrations_of (Context.Theory thy) loc) thy))
- in ctxt'' end;
+ in snd o Global_Theory.note_thmss kind facts' end)
+ (registrations_of (Context.Theory thy) loc) thy));
(* Declarations *)
@@ -688,7 +689,7 @@
fun add_locale_deps name =
let
val dependencies =
- (map o apsnd) (instance_of thy name o op $>) (dependencies_of thy name |> map fst);
+ map (apsnd (instance_of thy name o op $>) o fst) (dependencies_of thy name);
in
fold (fn (super, ts) => fn (gr, deps) => (gr |> Graph.add_edge (super, name),
deps |> Symtab.map_default (super, Symtab.empty) (Symtab.cons_list (name, ts))))
--- a/src/Pure/Isar/specification.ML Sat Nov 19 12:42:21 2011 +0100
+++ b/src/Pure/Isar/specification.ML Sat Nov 19 17:20:17 2011 +0100
@@ -309,7 +309,7 @@
val prems = Assumption.local_prems_of elems_ctxt ctxt;
val stmt = Attrib.map_specs (map prep_att) (map fst shows ~~ propp);
val goal_ctxt = (fold o fold) (Variable.auto_fixes o fst) propp elems_ctxt;
- in ((prems, stmt, NONE), goal_ctxt) end
+ in (([], prems, stmt, NONE), goal_ctxt) end
| Element.Obtains obtains =>
let
val case_names = obtains |> map_index (fn (i, (b, _)) =>
@@ -332,18 +332,19 @@
|> fold Variable.declare_term props
|> fold_map Proof_Context.inferred_param xs;
val asm = Term.list_all_free (xs ~~ Ts, Logic.list_implies (props, thesis));
+ val _ = ctxt' |> Proof_Context.add_fixes (map (fn b => (b, NONE, NoSyn)) bs);
in
- ctxt' |> (snd o Proof_Context.add_fixes (map (fn b => (b, NONE, NoSyn)) bs));
- ctxt' |> Variable.auto_fixes asm
+ ctxt'
+ |> Variable.auto_fixes asm
|> Proof_Context.add_assms_i Assumption.assume_export
[((name, [Context_Rules.intro_query NONE]), [(asm, [])])]
|>> (fn [(_, [th])] => th)
end;
- val atts = map (Attrib.internal o K)
+ val more_atts = map (Attrib.internal o K)
[Rule_Cases.consumes (~ (length obtains)), Rule_Cases.case_names case_names];
val prems = Assumption.local_prems_of elems_ctxt ctxt;
- val stmt = [((Binding.empty, atts), [(thesis, [])])];
+ val stmt = [((Binding.empty, []), [(thesis, [])])];
val (facts, goal_ctxt) = elems_ctxt
|> (snd o Proof_Context.add_fixes [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)])
@@ -351,7 +352,7 @@
|-> (fn ths =>
Proof_Context.note_thmss "" [((Binding.name Obtain.thatN, []), [(ths, [])])] #>
#2 #> pair ths);
- in ((prems, stmt, SOME facts), goal_ctxt) end);
+ in ((more_atts, prems, stmt, SOME facts), goal_ctxt) end);
structure Theorem_Hook = Generic_Data
(
@@ -368,29 +369,29 @@
val thy = Proof_Context.theory_of lthy;
val attrib = prep_att thy;
- val atts = map attrib raw_atts;
val elems = raw_elems |> map (Element.map_ctxt_attrib attrib);
- val ((prems, stmt, facts), goal_ctxt) =
+ val ((more_atts, prems, stmt, facts), goal_ctxt) =
prep_statement attrib prep_stmt elems raw_concl lthy;
+ val atts = more_atts @ map attrib raw_atts;
fun after_qed' results goal_ctxt' =
- let val results' =
- burrow (map Goal.norm_result o Proof_Context.export goal_ctxt' lthy) results
- in
- lthy
- |> Local_Theory.notes_kind kind
- (map2 (fn (a, _) => fn ths => (a, [(ths, [])])) stmt results')
- |> (fn (res, lthy') =>
- if Binding.is_empty name andalso null atts then
+ let
+ val results' = burrow (map Goal.norm_result o Proof_Context.export goal_ctxt' lthy) results;
+ val (res, lthy') =
+ if forall (Attrib.is_empty_binding o fst) stmt then (map (pair "") results', lthy)
+ else
+ Local_Theory.notes_kind kind
+ (map2 (fn (b, _) => fn ths => (b, [(ths, [])])) stmt results') lthy;
+ val lthy'' =
+ if Attrib.is_empty_binding (name, atts) then
(Proof_Display.print_results int lthy' ((kind, ""), res); lthy')
else
let
- val ([(res_name, _)], lthy'') = lthy'
- |> Local_Theory.notes_kind kind [((name, atts), [(maps #2 res, [])])];
+ val ([(res_name, _)], lthy'') =
+ Local_Theory.notes_kind kind [((name, atts), [(maps #2 res, [])])] lthy';
val _ = Proof_Display.print_results int lthy' ((kind, res_name), res);
- in lthy'' end)
- |> after_qed results'
- end;
+ in lthy'' end;
+ in after_qed results' lthy'' end;
in
goal_ctxt
|> Proof_Context.note_thmss "" [((Binding.name Auto_Bind.assmsN, []), [(prems, [])])]