more compact representation of different situations for interpretation
authorhaftmann
Sun Dec 29 23:21:13 2013 +0100 (2013-12-29)
changeset 548770a9337337277
parent 54876 8fab871a2a6f
child 54878 710e8f36a917
more compact representation of different situations for interpretation
src/Pure/Isar/expression.ML
     1.1 --- a/src/Pure/Isar/expression.ML	Sun Dec 29 23:21:12 2013 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Sun Dec 29 23:21:13 2013 +0100
     1.3 @@ -819,7 +819,7 @@
     1.4  
     1.5  (* reading *)
     1.6  
     1.7 -fun read_with_extended_syntax prep_prop deps ctxt props =
     1.8 +fun prep_with_extended_syntax prep_prop deps ctxt props =
     1.9    let
    1.10      val deps_ctxt = fold Locale.activate_declarations deps ctxt;
    1.11    in
    1.12 @@ -827,15 +827,18 @@
    1.13        |> Variable.export_terms deps_ctxt ctxt
    1.14    end;
    1.15  
    1.16 -fun read_interpretation prep_expr prep_prop prep_attr expression raw_eqns initial_ctxt =
    1.17 +fun prep_interpretation prep_expr prep_prop prep_attr expression raw_eqns initial_ctxt =
    1.18    let
    1.19      val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt;
    1.20 -    val eqns = read_with_extended_syntax prep_prop deps expr_ctxt raw_eqns;
    1.21 +    val eqns = prep_with_extended_syntax prep_prop deps expr_ctxt raw_eqns;
    1.22      val attrss = map (apsnd (map (prep_attr (Proof_Context.theory_of initial_ctxt))) o fst) raw_eqns;
    1.23      val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
    1.24      val export' = Variable.export_morphism goal_ctxt expr_ctxt;
    1.25    in (((propss, deps, export, export'), (eqns, attrss)), goal_ctxt) end;
    1.26  
    1.27 +val cert_interpretation = prep_interpretation cert_goal_expression (K I) (K I);
    1.28 +val read_interpretation = prep_interpretation read_goal_expression Syntax.parse_prop Attrib.intern_src;
    1.29 +
    1.30  
    1.31  (* generic interpretation machinery *)
    1.32  
    1.33 @@ -857,19 +860,19 @@
    1.34      |> fold activate' dep_morphs
    1.35    end;
    1.36  
    1.37 -fun generic_interpretation prep_expr prep_prop prep_attr setup_proof note activate
    1.38 +fun generic_interpretation prep_interpretation setup_proof note activate
    1.39      expression raw_eqns initial_ctxt = 
    1.40    let
    1.41      val (((propss, deps, export, export'), (eqns, attrss)), goal_ctxt) = 
    1.42 -      read_interpretation prep_expr prep_prop prep_attr expression raw_eqns initial_ctxt;
    1.43 +      prep_interpretation expression raw_eqns initial_ctxt;
    1.44      fun after_qed witss eqns =
    1.45        note_eqns_register note activate deps witss eqns attrss export export';
    1.46    in setup_proof after_qed propss eqns goal_ctxt end;
    1.47  
    1.48  
    1.49 -(* various flavours of interpretation *)
    1.50 +(* first dimension: proof vs. local theory *)
    1.51  
    1.52 -fun gen_interpret prep_expr prep_prop prep_attr expression raw_eqns int state =
    1.53 +fun gen_interpret prep_interpretation expression raw_eqns int state =
    1.54    let
    1.55      val _ = Proof.assert_forward_or_chain state;
    1.56      val ctxt = Proof.context_of state;
    1.57 @@ -877,71 +880,61 @@
    1.58      fun setup_proof after_qed propss eqns goal_ctxt = 
    1.59        Element.witness_local_proof_eqs (lift_after_qed after_qed) "interpret" propss eqns goal_ctxt int state;
    1.60    in
    1.61 -    generic_interpretation prep_expr prep_prop prep_attr setup_proof
    1.62 +    generic_interpretation prep_interpretation setup_proof
    1.63        Attrib.local_notes (Context.proof_map ooo Locale.add_registration) expression raw_eqns ctxt
    1.64    end;
    1.65  
    1.66 -fun gen_interpretation prep_expr prep_prop prep_attr expression raw_eqns lthy =
    1.67 +fun gen_local_theory_interpretation prep_interpretation activate expression raw_eqns lthy =
    1.68 +  generic_interpretation prep_interpretation Element.witness_proof_eqs
    1.69 +    Local_Theory.notes_kind (activate lthy) expression raw_eqns lthy;
    1.70 +
    1.71 +
    1.72 +(* second dimension: relation to underlying target *)
    1.73 +
    1.74 +fun subscribe lthy =
    1.75    if Named_Target.is_theory lthy
    1.76 -  then 
    1.77 -    lthy
    1.78 -    |> generic_interpretation prep_expr prep_prop prep_attr Element.witness_proof_eqs
    1.79 -        Local_Theory.notes_kind Generic_Target.theory_registration expression raw_eqns
    1.80 -  else
    1.81 -    lthy
    1.82 -    |> generic_interpretation prep_expr prep_prop prep_attr Element.witness_proof_eqs
    1.83 -        Local_Theory.notes_kind Local_Theory.activate expression raw_eqns;
    1.84 +  then Generic_Target.theory_registration
    1.85 +  else Generic_Target.locale_dependency (Named_Target.the_name lthy);
    1.86  
    1.87 -fun gen_sublocale prep_expr prep_prop prep_attr expression raw_eqns lthy =
    1.88 +fun subscribe_or_activate lthy =
    1.89 +  if Named_Target.is_theory lthy
    1.90 +  then subscribe lthy
    1.91 +  else Local_Theory.activate;
    1.92 +
    1.93 +fun subscribe_locale_only lthy =
    1.94    let
    1.95      val _ = if Named_Target.is_theory lthy
    1.96        then error "Not possible on level of global theory" else ();
    1.97 -    val locale = Named_Target.the_name lthy;
    1.98 -  in
    1.99 -    lthy
   1.100 -    |> generic_interpretation prep_expr prep_prop prep_attr Element.witness_proof_eqs
   1.101 -        Local_Theory.notes_kind (Generic_Target.locale_dependency locale) expression raw_eqns
   1.102 -  end;
   1.103 -  
   1.104 -fun gen_sublocale_global prep_expr prep_loc prep_prop prep_attr before_exit raw_locale expression raw_eqns thy =
   1.105 +  in subscribe lthy end;
   1.106 +
   1.107 +
   1.108 +(* special case: global sublocale command *)
   1.109 +
   1.110 +fun gen_sublocale_global prep_loc prep_interpretation before_exit raw_locale expression raw_eqns thy =
   1.111    thy
   1.112    |> Named_Target.init before_exit (prep_loc thy raw_locale)
   1.113 -  |> gen_sublocale prep_expr prep_prop prep_attr expression raw_eqns
   1.114 +  |> gen_local_theory_interpretation prep_interpretation subscribe_locale_only expression raw_eqns
   1.115  
   1.116  in
   1.117  
   1.118 -fun permanent_interpretation expression raw_eqns lthy =
   1.119 -  let
   1.120 -    val _ = Local_Theory.assert_bottom true lthy;
   1.121 -    val target = Named_Target.the_name lthy;
   1.122 -    val subscribe = if target = "" then Generic_Target.theory_registration
   1.123 -      else Generic_Target.locale_dependency target;
   1.124 -  in
   1.125 -    lthy
   1.126 -    |> generic_interpretation cert_goal_expression (K I) (K I) Element.witness_proof_eqs
   1.127 -        Local_Theory.notes_kind subscribe expression raw_eqns
   1.128 -  end;
   1.129 +
   1.130 +(* interfaces *)
   1.131 +
   1.132 +fun interpret x = gen_interpret cert_interpretation x;
   1.133 +fun interpret_cmd x = gen_interpret read_interpretation x;
   1.134 +
   1.135 +fun permanent_interpretation x = gen_local_theory_interpretation cert_interpretation subscribe x;
   1.136  
   1.137 -fun ephemeral_interpretation expression raw_eqns lthy =
   1.138 -  lthy
   1.139 -  |> generic_interpretation cert_goal_expression (K I) (K I) Element.witness_proof_eqs
   1.140 -      Local_Theory.notes_kind Local_Theory.activate expression raw_eqns
   1.141 +fun ephemeral_interpretation x = gen_local_theory_interpretation cert_interpretation (K Local_Theory.activate) x;
   1.142  
   1.143 -fun interpret x = gen_interpret cert_goal_expression (K I) (K I) x;
   1.144 -fun interpret_cmd x =
   1.145 -  gen_interpret read_goal_expression Syntax.parse_prop Attrib.intern_src x;
   1.146 +fun interpretation x = gen_local_theory_interpretation cert_interpretation subscribe_or_activate x;
   1.147 +fun interpretation_cmd x = gen_local_theory_interpretation read_interpretation subscribe_or_activate x;
   1.148  
   1.149 -fun interpretation x = gen_interpretation cert_goal_expression (K I) (K I) x;
   1.150 -fun interpretation_cmd x =
   1.151 -  gen_interpretation read_goal_expression Syntax.parse_prop Attrib.intern_src x;
   1.152 +fun sublocale x = gen_local_theory_interpretation cert_interpretation subscribe_locale_only x;
   1.153 +fun sublocale_cmd x = gen_local_theory_interpretation read_interpretation subscribe_locale_only x;
   1.154  
   1.155 -fun sublocale x = gen_sublocale cert_goal_expression (K I) (K I) x;
   1.156 -fun sublocale_cmd x =
   1.157 -  gen_sublocale read_goal_expression Syntax.parse_prop Attrib.intern_src x;
   1.158 -
   1.159 -fun sublocale_global x = gen_sublocale_global cert_goal_expression (K I) (K I) (K I) x;
   1.160 -fun sublocale_global_cmd x =
   1.161 -  gen_sublocale_global read_goal_expression Locale.check Syntax.parse_prop Attrib.intern_src x;
   1.162 +fun sublocale_global x = gen_sublocale_global (K I) cert_interpretation x;
   1.163 +fun sublocale_global_cmd x = gen_sublocale_global Locale.check read_interpretation x;
   1.164  
   1.165  end;
   1.166