tuned
authorhaftmann
Tue Apr 23 11:14:50 2013 +0200 (2013-04-23)
changeset 51734d504e349e951
parent 51733 70abecafe9ac
child 51735 f069c7d496ca
tuned
src/Pure/Isar/expression.ML
     1.1 --- a/src/Pure/Isar/expression.ML	Mon Apr 22 18:39:12 2013 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Tue Apr 23 11:14:50 2013 +0200
     1.3 @@ -39,15 +39,15 @@
     1.4      (term list list * (string * morphism) list * morphism) * Proof.context
     1.5    val read_goal_expression: expression -> Proof.context ->
     1.6      (term list list * (string * morphism) list * morphism) * Proof.context
     1.7 +  val interpret: expression_i -> (Attrib.binding * term) list -> bool -> Proof.state -> Proof.state
     1.8 +  val interpret_cmd: expression -> (Attrib.binding * string) list ->
     1.9 +    bool -> Proof.state -> Proof.state
    1.10 +  val interpretation: expression_i -> (Attrib.binding * term) list -> theory -> Proof.state
    1.11 +  val interpretation_cmd: expression -> (Attrib.binding * string) list -> theory -> Proof.state
    1.12    val sublocale: (local_theory -> local_theory) -> string -> expression_i ->
    1.13      (Attrib.binding * term) list -> theory -> Proof.state
    1.14    val sublocale_cmd: (local_theory -> local_theory) -> xstring * Position.T -> expression ->
    1.15      (Attrib.binding * string) list -> theory -> Proof.state
    1.16 -  val interpretation: expression_i -> (Attrib.binding * term) list -> theory -> Proof.state
    1.17 -  val interpretation_cmd: expression -> (Attrib.binding * string) list -> theory -> Proof.state
    1.18 -  val interpret: expression_i -> (Attrib.binding * term) list -> bool -> Proof.state -> Proof.state
    1.19 -  val interpret_cmd: expression -> (Attrib.binding * string) list ->
    1.20 -    bool -> Proof.state -> Proof.state
    1.21  
    1.22    (* Diagnostic *)
    1.23    val print_dependencies: Proof.context -> bool -> expression -> unit
    1.24 @@ -814,52 +814,48 @@
    1.25        |> Variable.export_terms deps_ctxt ctxt
    1.26    end;
    1.27  
    1.28 -fun read_interpretation prep_expr parse_prop prep_attr expression equations initial_ctxt =
    1.29 +fun read_interpretation prep_expr parse_prop prep_attr expression raw_eqns initial_ctxt =
    1.30    let
    1.31      val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt;
    1.32 -    val eqns = read_with_extended_syntax parse_prop deps expr_ctxt equations;
    1.33 -    val attrss = map (apsnd (map (prep_attr (Proof_Context.theory_of initial_ctxt))) o fst) equations;
    1.34 +    val eqns = read_with_extended_syntax parse_prop deps expr_ctxt raw_eqns;
    1.35 +    val attrss = map (apsnd (map (prep_attr (Proof_Context.theory_of initial_ctxt))) o fst) raw_eqns;
    1.36      val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
    1.37      val export' = Variable.export_morphism goal_ctxt expr_ctxt;
    1.38    in (((propss, deps, export, export'), (eqns, attrss)), goal_ctxt) end;
    1.39  
    1.40 -fun meta_rewrite ctxt = map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def);
    1.41 +fun meta_rewrite eqns ctxt = (map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) (maps snd eqns), ctxt);
    1.42  
    1.43 -fun note_eqns_register note add_registration deps witss eqns attrss export export' ctxt =
    1.44 +fun note_eqns_register note activate reinit deps witss eqns attrss export export' ctxt =
    1.45    let
    1.46      val facts = 
    1.47        (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns);
    1.48      val (eqns', ctxt') = ctxt
    1.49        |> note Thm.lemmaK facts
    1.50 -      |-> (fn facts' => `(fn ctxt'' => meta_rewrite ctxt'' (maps snd facts')));
    1.51 +      |-> meta_rewrite;
    1.52 +    val dep_morphs = map2 (fn (dep, morph) => fn wits =>
    1.53 +      (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))) deps witss;
    1.54 +    fun activate' dep_morph ctxt = activate dep_morph
    1.55 +      (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) eqns')) export ctxt;
    1.56    in
    1.57      ctxt'
    1.58 -    |> fold2 (fn (dep, morph) => fn wits => fn ctxt'' =>
    1.59 -      add_registration
    1.60 -        (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))
    1.61 -        (Element.eq_morphism (Proof_Context.theory_of ctxt'') eqns' |> Option.map (rpair true))
    1.62 -        export ctxt'') deps witss
    1.63 +    |> fold activate' dep_morphs
    1.64 +    |> reinit
    1.65    end;
    1.66  
    1.67  fun generic_interpretation prep_expr parse_prop prep_attr setup_proof note add_registration
    1.68 -    expression equations initial_ctxt = 
    1.69 +    reinit expression raw_eqns initial_ctxt = 
    1.70    let
    1.71      val (((propss, deps, export, export'), (eqns, attrss)), goal_ctxt) = 
    1.72 -      read_interpretation prep_expr parse_prop prep_attr expression equations initial_ctxt;
    1.73 +      read_interpretation prep_expr parse_prop prep_attr expression raw_eqns initial_ctxt;
    1.74      fun after_qed witss eqns =
    1.75 -      note_eqns_register note add_registration deps witss eqns attrss export export';
    1.76 +      note_eqns_register note add_registration reinit deps witss eqns attrss export export';
    1.77    in setup_proof after_qed propss eqns goal_ctxt end;
    1.78  
    1.79 -fun gen_interpretation prep_expr parse_prop prep_attr expression equations thy =
    1.80 -  thy
    1.81 -  |> Named_Target.theory_init
    1.82 -  |> generic_interpretation prep_expr parse_prop prep_attr
    1.83 -      Element.witness_proof_eqs
    1.84 -      Local_Theory.notes_kind
    1.85 -      (Proof_Context.background_theory o Context.theory_map ooo Locale.add_registration)
    1.86 -      expression equations;
    1.87 +val activate_only = Context.proof_map ooo Locale.add_registration;
    1.88 +val add_registration = Proof_Context.background_theory o Context.theory_map ooo Locale.add_registration;
    1.89 +fun add_dependency locale = Proof_Context.background_theory ooo Locale.add_dependency locale;
    1.90  
    1.91 -fun gen_interpret prep_expr parse_prop prep_attr expression equations int state =
    1.92 +fun gen_interpret prep_expr parse_prop prep_attr expression raw_eqns int state =
    1.93    let
    1.94      val _ = Proof.assert_forward_or_chain state;
    1.95      val ctxt = Proof.context_of state;
    1.96 @@ -867,36 +863,36 @@
    1.97      fun setup_proof after_qed propss eqns goal_ctxt = 
    1.98        Element.witness_local_proof_eqs (lift_after_qed after_qed) "interpret" propss eqns goal_ctxt int state;
    1.99    in
   1.100 -    generic_interpretation prep_expr parse_prop prep_attr
   1.101 -      setup_proof
   1.102 -      Attrib.local_notes
   1.103 -      (Context.proof_map ooo Locale.add_registration)
   1.104 -      expression equations ctxt
   1.105 +    generic_interpretation prep_expr parse_prop prep_attr setup_proof
   1.106 +      Attrib.local_notes activate_only I expression raw_eqns ctxt
   1.107    end;
   1.108 - 
   1.109 -fun gen_sublocale prep_expr prep_loc parse_prop prep_attr before_exit raw_locale expression equations thy =
   1.110 +
   1.111 +fun gen_interpretation prep_expr parse_prop prep_attr expression raw_eqns thy =
   1.112 +  thy
   1.113 +  |> Named_Target.theory_init
   1.114 +  |> generic_interpretation prep_expr parse_prop prep_attr Element.witness_proof_eqs
   1.115 +      Local_Theory.notes_kind add_registration I expression raw_eqns;
   1.116 +
   1.117 +fun gen_sublocale prep_expr prep_loc parse_prop prep_attr before_exit raw_locale expression raw_eqns thy =
   1.118    let
   1.119      val locale = prep_loc thy raw_locale;
   1.120    in
   1.121      thy
   1.122      |> Named_Target.init before_exit locale
   1.123 -    |> generic_interpretation prep_expr parse_prop prep_attr
   1.124 -        Element.witness_proof_eqs
   1.125 -        Local_Theory.notes_kind
   1.126 -        (Proof_Context.background_theory ooo Locale.add_dependency locale)
   1.127 -        expression equations
   1.128 +    |> generic_interpretation prep_expr parse_prop prep_attr Element.witness_proof_eqs
   1.129 +        Local_Theory.notes_kind (add_dependency locale) I expression raw_eqns
   1.130    end;
   1.131  
   1.132  in
   1.133  
   1.134 +fun interpret x = gen_interpret cert_goal_expression (K I) (K I) x;
   1.135 +fun interpret_cmd x = gen_interpret read_goal_expression
   1.136 +  Syntax.parse_prop Attrib.intern_src x;
   1.137 +
   1.138  fun interpretation x = gen_interpretation cert_goal_expression (K I) (K I) x;
   1.139  fun interpretation_cmd x = gen_interpretation read_goal_expression
   1.140    Syntax.parse_prop Attrib.intern_src x;
   1.141  
   1.142 -fun interpret x = gen_interpret cert_goal_expression (K I) (K I) x;
   1.143 -fun interpret_cmd x = gen_interpret read_goal_expression
   1.144 -  Syntax.parse_prop Attrib.intern_src x;
   1.145 -
   1.146  fun sublocale x = gen_sublocale cert_goal_expression (K I) (K I) (K I) x;
   1.147  fun sublocale_cmd x =
   1.148    gen_sublocale read_goal_expression Locale.check Syntax.parse_prop Attrib.intern_src x;