src/Pure/Isar/expression.ML
changeset 61669 27ca6147e3b3
parent 61336 fa4ebbd350ae
child 62752 d09d71223e7a
     1.1 --- a/src/Pure/Isar/expression.ML	Sat Nov 14 08:45:51 2015 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Sat Nov 14 08:45:51 2015 +0100
     1.3 @@ -36,27 +36,11 @@
     1.4    val add_locale_cmd: binding -> binding ->
     1.5      expression -> Element.context list -> theory -> string * local_theory
     1.6  
     1.7 -  (* Interpretation *)
     1.8 +  (* Processing of locale expressions *)
     1.9    val cert_goal_expression: expression_i -> Proof.context ->
    1.10      (term list list * (string * morphism) list * morphism) * Proof.context
    1.11    val read_goal_expression: expression -> Proof.context ->
    1.12      (term list list * (string * morphism) list * morphism) * Proof.context
    1.13 -  val permanent_interpretation: expression_i -> (Attrib.binding * term) list ->
    1.14 -    local_theory -> Proof.state
    1.15 -  val ephemeral_interpretation: expression_i -> (Attrib.binding * term) list ->
    1.16 -    local_theory -> Proof.state
    1.17 -  val interpret: expression_i -> (Attrib.binding * term) list -> bool -> Proof.state -> Proof.state
    1.18 -  val interpret_cmd: expression -> (Attrib.binding * string) list ->
    1.19 -    bool -> Proof.state -> Proof.state
    1.20 -  val interpretation: expression_i -> (Attrib.binding * term) list -> local_theory -> Proof.state
    1.21 -  val interpretation_cmd: expression -> (Attrib.binding * string) list ->
    1.22 -    local_theory -> Proof.state
    1.23 -  val sublocale: expression_i -> (Attrib.binding * term) list -> local_theory -> Proof.state
    1.24 -  val sublocale_cmd: expression -> (Attrib.binding * string) list -> local_theory -> Proof.state
    1.25 -  val sublocale_global: string -> expression_i ->
    1.26 -    (Attrib.binding * term) list -> theory -> Proof.state
    1.27 -  val sublocale_global_cmd: xstring * Position.T -> expression ->
    1.28 -    (Attrib.binding * string) list -> theory -> Proof.state
    1.29  
    1.30    (* Diagnostic *)
    1.31    val print_dependencies: Proof.context -> bool -> expression -> unit
    1.32 @@ -848,155 +832,6 @@
    1.33  end;
    1.34  
    1.35  
    1.36 -(*** Interpretation ***)
    1.37 -
    1.38 -local
    1.39 -
    1.40 -(* reading *)
    1.41 -
    1.42 -fun prep_with_extended_syntax prep_prop deps ctxt props =
    1.43 -  let
    1.44 -    val deps_ctxt = fold Locale.activate_declarations deps ctxt;
    1.45 -  in
    1.46 -    map (prep_prop deps_ctxt o snd) props |> Syntax.check_terms deps_ctxt
    1.47 -      |> Variable.export_terms deps_ctxt ctxt
    1.48 -  end;
    1.49 -
    1.50 -fun prep_interpretation prep_expr prep_prop prep_attr expression raw_eqns initial_ctxt =
    1.51 -  let
    1.52 -    val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt;
    1.53 -    val eqns = prep_with_extended_syntax prep_prop deps expr_ctxt raw_eqns;
    1.54 -    val attrss = map (apsnd (map (prep_attr initial_ctxt)) o fst) raw_eqns;
    1.55 -    val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
    1.56 -    val export' = Variable.export_morphism goal_ctxt expr_ctxt;
    1.57 -  in (((propss, deps, export, export'), (eqns, attrss)), goal_ctxt) end;
    1.58 -
    1.59 -val cert_interpretation =
    1.60 -  prep_interpretation cert_goal_expression (K I) (K I);
    1.61 -
    1.62 -val read_interpretation =
    1.63 -  prep_interpretation read_goal_expression Syntax.parse_prop Attrib.check_src;
    1.64 -
    1.65 -
    1.66 -(* generic interpretation machinery *)
    1.67 -
    1.68 -fun meta_rewrite ctxt eqns =
    1.69 -  map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) (maps snd eqns);
    1.70 -
    1.71 -fun note_eqns_register note activate deps witss eqns attrss export export' ctxt =
    1.72 -  let
    1.73 -    val facts = map2 (fn attrs => fn eqn =>
    1.74 -      (attrs, [([Morphism.thm (export' $> export) eqn], [])])) attrss eqns;
    1.75 -    val (eqns', ctxt') = ctxt
    1.76 -      |> note Thm.theoremK facts
    1.77 -      |> (fn (eqns, ctxt') => (meta_rewrite ctxt' eqns, ctxt'));
    1.78 -    val dep_morphs =
    1.79 -      map2 (fn (dep, morph) => fn wits =>
    1.80 -          (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits)))
    1.81 -        deps witss;
    1.82 -    fun activate' dep_morph ctxt =
    1.83 -      activate dep_morph
    1.84 -        (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) eqns'))
    1.85 -        export ctxt;
    1.86 -  in
    1.87 -    ctxt'
    1.88 -    |> fold activate' dep_morphs
    1.89 -  end;
    1.90 -
    1.91 -fun generic_interpretation prep_interpretation setup_proof note activate
    1.92 -    expression raw_eqns initial_ctxt =
    1.93 -  let
    1.94 -    val (((propss, deps, export, export'), (eqns, attrss)), goal_ctxt) =
    1.95 -      prep_interpretation expression raw_eqns initial_ctxt;
    1.96 -    fun after_qed witss eqns =
    1.97 -      note_eqns_register note activate deps witss eqns attrss export export';
    1.98 -  in setup_proof after_qed propss eqns goal_ctxt end;
    1.99 -
   1.100 -
   1.101 -(* first dimension: proof vs. local theory *)
   1.102 -
   1.103 -fun gen_interpret prep_interpretation expression raw_eqns int state =
   1.104 -  let
   1.105 -    val _ = Proof.assert_forward_or_chain state;
   1.106 -    val ctxt = Proof.context_of state;
   1.107 -    fun lift_after_qed after_qed witss eqns =
   1.108 -      Proof.map_context (after_qed witss eqns) #> Proof.reset_facts;
   1.109 -    fun setup_proof after_qed propss eqns goal_ctxt =
   1.110 -      Element.witness_local_proof_eqs (lift_after_qed after_qed) "interpret"
   1.111 -        propss eqns goal_ctxt int state;
   1.112 -  in
   1.113 -    generic_interpretation prep_interpretation setup_proof
   1.114 -      Attrib.local_notes (Context.proof_map ooo Locale.add_registration) expression raw_eqns ctxt
   1.115 -  end;
   1.116 -
   1.117 -fun gen_local_theory_interpretation prep_interpretation activate expression raw_eqns lthy =
   1.118 -  generic_interpretation prep_interpretation Element.witness_proof_eqs
   1.119 -    Local_Theory.notes_kind (activate lthy) expression raw_eqns lthy;
   1.120 -
   1.121 -
   1.122 -(* second dimension: relation to underlying target *)
   1.123 -
   1.124 -fun subscribe_or_activate lthy =
   1.125 -  if Named_Target.is_theory lthy
   1.126 -  then Local_Theory.subscription
   1.127 -  else Locale.activate_fragment;
   1.128 -
   1.129 -fun subscribe_locale_only lthy =
   1.130 -  let
   1.131 -    val _ =
   1.132 -      if Named_Target.is_theory lthy
   1.133 -      then error "Not possible on level of global theory"
   1.134 -      else ();
   1.135 -  in Local_Theory.subscription end;
   1.136 -
   1.137 -
   1.138 -(* special case: global sublocale command *)
   1.139 -
   1.140 -fun gen_sublocale_global prep_loc prep_interpretation
   1.141 -    raw_locale expression raw_eqns thy =
   1.142 -  let
   1.143 -    val lthy = Named_Target.init (prep_loc thy raw_locale) thy;
   1.144 -    fun setup_proof after_qed =
   1.145 -      Element.witness_proof_eqs
   1.146 -        (fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit);
   1.147 -  in
   1.148 -    lthy |>
   1.149 -      generic_interpretation prep_interpretation setup_proof
   1.150 -        Local_Theory.notes_kind (subscribe_locale_only lthy) expression raw_eqns
   1.151 -  end;
   1.152 -
   1.153 -in
   1.154 -
   1.155 -
   1.156 -(* interfaces *)
   1.157 -
   1.158 -fun interpret x = gen_interpret cert_interpretation x;
   1.159 -fun interpret_cmd x = gen_interpret read_interpretation x;
   1.160 -
   1.161 -fun permanent_interpretation expression raw_eqns =
   1.162 -  Local_Theory.assert_bottom true
   1.163 -  #> gen_local_theory_interpretation cert_interpretation
   1.164 -    (K Local_Theory.subscription) expression raw_eqns;
   1.165 -
   1.166 -fun ephemeral_interpretation x =
   1.167 -  gen_local_theory_interpretation cert_interpretation (K Locale.activate_fragment) x;
   1.168 -
   1.169 -fun interpretation x =
   1.170 -  gen_local_theory_interpretation cert_interpretation subscribe_or_activate x;
   1.171 -fun interpretation_cmd x =
   1.172 -  gen_local_theory_interpretation read_interpretation subscribe_or_activate x;
   1.173 -
   1.174 -fun sublocale x =
   1.175 -  gen_local_theory_interpretation cert_interpretation subscribe_locale_only x;
   1.176 -fun sublocale_cmd x =
   1.177 -  gen_local_theory_interpretation read_interpretation subscribe_locale_only x;
   1.178 -
   1.179 -fun sublocale_global x = gen_sublocale_global (K I) cert_interpretation x;
   1.180 -fun sublocale_global_cmd x = gen_sublocale_global Locale.check read_interpretation x;
   1.181 -
   1.182 -end;
   1.183 -
   1.184 -
   1.185  (** Print the instances that would be activated by an interpretation
   1.186    of the expression in the current context (clean = false) or in an
   1.187    empty context (clean = true). **)