# HG changeset patch # User haftmann # Date 1366708490 -7200 # Node ID d504e349e951265965a47aa3a00ae2c1cf19c1b5 # Parent 70abecafe9ac6ca8b9c87c0a8e8c5c724695222c tuned diff -r 70abecafe9ac -r d504e349e951 src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Mon Apr 22 18:39:12 2013 +0200 +++ b/src/Pure/Isar/expression.ML Tue Apr 23 11:14:50 2013 +0200 @@ -39,15 +39,15 @@ (term list list * (string * morphism) list * morphism) * Proof.context val read_goal_expression: expression -> Proof.context -> (term list list * (string * morphism) list * morphism) * Proof.context + val interpret: expression_i -> (Attrib.binding * term) list -> bool -> Proof.state -> Proof.state + val interpret_cmd: expression -> (Attrib.binding * string) list -> + bool -> Proof.state -> Proof.state + val interpretation: expression_i -> (Attrib.binding * term) list -> theory -> Proof.state + val interpretation_cmd: expression -> (Attrib.binding * string) list -> theory -> Proof.state val sublocale: (local_theory -> local_theory) -> string -> expression_i -> (Attrib.binding * term) list -> theory -> Proof.state val sublocale_cmd: (local_theory -> local_theory) -> xstring * Position.T -> expression -> (Attrib.binding * string) list -> theory -> Proof.state - val interpretation: expression_i -> (Attrib.binding * term) list -> theory -> Proof.state - val interpretation_cmd: expression -> (Attrib.binding * string) list -> theory -> Proof.state - val interpret: expression_i -> (Attrib.binding * term) list -> bool -> Proof.state -> Proof.state - val interpret_cmd: expression -> (Attrib.binding * string) list -> - bool -> Proof.state -> Proof.state (* Diagnostic *) val print_dependencies: Proof.context -> bool -> expression -> unit @@ -814,52 +814,48 @@ |> Variable.export_terms deps_ctxt ctxt end; -fun read_interpretation prep_expr parse_prop prep_attr expression equations initial_ctxt = +fun read_interpretation prep_expr parse_prop prep_attr expression raw_eqns initial_ctxt = let val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt; - val eqns = read_with_extended_syntax parse_prop deps expr_ctxt equations; - val attrss = map (apsnd (map (prep_attr (Proof_Context.theory_of initial_ctxt))) o fst) equations; + val eqns = read_with_extended_syntax parse_prop deps expr_ctxt raw_eqns; + val attrss = map (apsnd (map (prep_attr (Proof_Context.theory_of initial_ctxt))) o fst) raw_eqns; val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt; val export' = Variable.export_morphism goal_ctxt expr_ctxt; in (((propss, deps, export, export'), (eqns, attrss)), goal_ctxt) end; -fun meta_rewrite ctxt = map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def); +fun meta_rewrite eqns ctxt = (map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) (maps snd eqns), ctxt); -fun note_eqns_register note add_registration deps witss eqns attrss export export' ctxt = +fun note_eqns_register note activate reinit deps witss eqns attrss export export' ctxt = let val facts = (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns); val (eqns', ctxt') = ctxt |> note Thm.lemmaK facts - |-> (fn facts' => `(fn ctxt'' => meta_rewrite ctxt'' (maps snd facts'))); + |-> meta_rewrite; + val dep_morphs = map2 (fn (dep, morph) => fn wits => + (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))) deps witss; + fun activate' dep_morph ctxt = activate dep_morph + (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) eqns')) export ctxt; in ctxt' - |> fold2 (fn (dep, morph) => fn wits => fn ctxt'' => - add_registration - (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits)) - (Element.eq_morphism (Proof_Context.theory_of ctxt'') eqns' |> Option.map (rpair true)) - export ctxt'') deps witss + |> fold activate' dep_morphs + |> reinit end; fun generic_interpretation prep_expr parse_prop prep_attr setup_proof note add_registration - expression equations initial_ctxt = + reinit expression raw_eqns initial_ctxt = let val (((propss, deps, export, export'), (eqns, attrss)), goal_ctxt) = - read_interpretation prep_expr parse_prop prep_attr expression equations initial_ctxt; + read_interpretation prep_expr parse_prop prep_attr expression raw_eqns initial_ctxt; fun after_qed witss eqns = - note_eqns_register note add_registration deps witss eqns attrss export export'; + note_eqns_register note add_registration reinit deps witss eqns attrss export export'; in setup_proof after_qed propss eqns goal_ctxt end; -fun gen_interpretation prep_expr parse_prop prep_attr expression equations thy = - thy - |> Named_Target.theory_init - |> generic_interpretation prep_expr parse_prop prep_attr - Element.witness_proof_eqs - Local_Theory.notes_kind - (Proof_Context.background_theory o Context.theory_map ooo Locale.add_registration) - expression equations; +val activate_only = Context.proof_map ooo Locale.add_registration; +val add_registration = Proof_Context.background_theory o Context.theory_map ooo Locale.add_registration; +fun add_dependency locale = Proof_Context.background_theory ooo Locale.add_dependency locale; -fun gen_interpret prep_expr parse_prop prep_attr expression equations int state = +fun gen_interpret prep_expr parse_prop prep_attr expression raw_eqns int state = let val _ = Proof.assert_forward_or_chain state; val ctxt = Proof.context_of state; @@ -867,36 +863,36 @@ fun setup_proof after_qed propss eqns goal_ctxt = Element.witness_local_proof_eqs (lift_after_qed after_qed) "interpret" propss eqns goal_ctxt int state; in - generic_interpretation prep_expr parse_prop prep_attr - setup_proof - Attrib.local_notes - (Context.proof_map ooo Locale.add_registration) - expression equations ctxt + generic_interpretation prep_expr parse_prop prep_attr setup_proof + Attrib.local_notes activate_only I expression raw_eqns ctxt end; - -fun gen_sublocale prep_expr prep_loc parse_prop prep_attr before_exit raw_locale expression equations thy = + +fun gen_interpretation prep_expr parse_prop prep_attr expression raw_eqns thy = + thy + |> Named_Target.theory_init + |> generic_interpretation prep_expr parse_prop prep_attr Element.witness_proof_eqs + Local_Theory.notes_kind add_registration I expression raw_eqns; + +fun gen_sublocale prep_expr prep_loc parse_prop prep_attr before_exit raw_locale expression raw_eqns thy = let val locale = prep_loc thy raw_locale; in thy |> Named_Target.init before_exit locale - |> generic_interpretation prep_expr parse_prop prep_attr - Element.witness_proof_eqs - Local_Theory.notes_kind - (Proof_Context.background_theory ooo Locale.add_dependency locale) - expression equations + |> generic_interpretation prep_expr parse_prop prep_attr Element.witness_proof_eqs + Local_Theory.notes_kind (add_dependency locale) I expression raw_eqns end; in +fun interpret x = gen_interpret cert_goal_expression (K I) (K I) x; +fun interpret_cmd x = gen_interpret read_goal_expression + Syntax.parse_prop Attrib.intern_src x; + fun interpretation x = gen_interpretation cert_goal_expression (K I) (K I) x; fun interpretation_cmd x = gen_interpretation read_goal_expression Syntax.parse_prop Attrib.intern_src x; -fun interpret x = gen_interpret cert_goal_expression (K I) (K I) x; -fun interpret_cmd x = gen_interpret read_goal_expression - Syntax.parse_prop Attrib.intern_src x; - fun sublocale x = gen_sublocale cert_goal_expression (K I) (K I) (K I) x; fun sublocale_cmd x = gen_sublocale read_goal_expression Locale.check Syntax.parse_prop Attrib.intern_src x;