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