--- a/src/Pure/Isar/interpretation.ML Sat Nov 14 08:45:52 2015 +0100
+++ b/src/Pure/Isar/interpretation.ML Sat Nov 14 08:45:52 2015 +0100
@@ -33,43 +33,15 @@
structure Interpretation : INTERPRETATION =
struct
-local
-
(** reading **)
-(* without mixin definitions *)
-
-fun prep_with_extended_syntax prep_prop deps ctxt props =
- let
- val deps_ctxt = fold Locale.activate_declarations deps ctxt;
- in
- map (prep_prop deps_ctxt o snd) props |> Syntax.check_terms deps_ctxt
- |> Variable.export_terms deps_ctxt ctxt
- end;
+local
-fun prep_interpretation prep_expr prep_prop prep_attr expression raw_eqns initial_ctxt =
- let
- val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt;
- val eqns = prep_with_extended_syntax prep_prop deps expr_ctxt raw_eqns;
- val attrss = map (apsnd (map (prep_attr 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;
-
-val cert_interpretation =
- prep_interpretation Expression.cert_goal_expression (K I) (K I);
-
-val read_interpretation =
- prep_interpretation Expression.read_goal_expression Syntax.parse_prop Attrib.check_src;
-
-
-(* with mixin definitions *)
-
-fun prep_interpretation_with_defs prep_expr prep_term prep_prop prep_attr expression raw_defs raw_eqns initial_ctxt =
+fun prep_interpretation prep_expr prep_term prep_prop prep_attr expression raw_defs raw_eqns initial_ctxt =
let
(*reading*)
- val ((propss, deps, export), expr_ctxt1) = prep_expr expression initial_ctxt;
- val deps_ctxt = fold Locale.activate_declarations deps expr_ctxt1;
+ val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt;
+ val deps_ctxt = fold Locale.activate_declarations deps expr_ctxt;
val prep = Syntax.check_terms deps_ctxt #> Variable.export_terms deps_ctxt deps_ctxt;
val rhss = (prep o map (prep_term deps_ctxt o snd o snd)) raw_defs;
val eqns = (prep o map (prep_prop deps_ctxt o snd)) raw_eqns;
@@ -77,73 +49,35 @@
(*defining*)
val pre_defs = map2 (fn ((name, atts), ((b, mx), _)) => fn rhs =>
((b, mx), ((Thm.def_binding_optional b name, atts), rhs))) raw_defs rhss;
- val (defs, defs_ctxt) = fold_map Local_Theory.define pre_defs expr_ctxt1;
- val expr_ctxt2 = Proof_Context.transfer (Proof_Context.theory_of defs_ctxt) expr_ctxt1;
+ val (defs, forked_ctxt) = fold_map Local_Theory.define pre_defs expr_ctxt;
+ val def_ctxt = Proof_Context.transfer (Proof_Context.theory_of forked_ctxt) expr_ctxt;
val def_eqns = defs
|> map (Thm.symmetric o
- Morphism.thm (Local_Theory.standard_morphism defs_ctxt expr_ctxt2) o snd o snd);
-
- (*setting up*)
- val attrss = map (apsnd (map (prep_attr expr_ctxt2)) o fst) raw_eqns;
- val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt2;
- val export' = Variable.export_morphism goal_ctxt expr_ctxt2;
- in (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) end;
-
-val cert_interpretation_with_defs =
- prep_interpretation_with_defs Expression.cert_goal_expression (K I) (K I) (K I);
-
-val read_interpretation_with_defs =
- prep_interpretation_with_defs Expression.read_goal_expression Syntax.parse_term Syntax.parse_prop Attrib.check_src;
-
-
-(** generic interpretation machinery **)
-
-(* without mixin definitions *)
-
-local
+ Morphism.thm (Local_Theory.standard_morphism forked_ctxt def_ctxt) o snd o snd);
-fun meta_rewrite ctxt eqns =
- map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) (maps snd eqns);
-
-fun note_eqns_register note activate deps witss eqns attrss export export' ctxt =
- let
- val facts = map2 (fn attrs => fn eqn =>
- (attrs, [([Morphism.thm (export' $> export) eqn], [])])) attrss eqns;
- val (eqns', ctxt') = ctxt
- |> note Thm.theoremK facts
- |> (fn (eqns, ctxt') => (meta_rewrite ctxt' eqns, ctxt'));
- 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'
- |> fold activate' dep_morphs
- end;
+ (*setting up proof*)
+ val attrss = map (apsnd (map (prep_attr def_ctxt)) o fst) raw_eqns;
+ val goal_ctxt = fold Variable.auto_fixes eqns def_ctxt;
+ val export' = Variable.export_morphism goal_ctxt def_ctxt;
+ in (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) end;
in
-fun generic_interpretation prep_interpretation setup_proof note activate
- expression raw_eqns initial_ctxt =
- let
- val (((propss, deps, export, export'), (eqns, attrss)), goal_ctxt) =
- prep_interpretation expression raw_eqns initial_ctxt;
- fun after_qed witss eqns =
- note_eqns_register note activate deps witss eqns attrss export export';
- in setup_proof after_qed propss eqns goal_ctxt end;
+val cert_interpretation =
+ prep_interpretation Expression.cert_goal_expression (K I) (K I) (K I);
+
+val read_interpretation =
+ prep_interpretation Expression.read_goal_expression Syntax.parse_term Syntax.parse_prop Attrib.check_src;
end;
-(* without mixin definitions *)
+(** common interpretation machinery **)
local
-fun meta_rewrite eqns ctxt = (map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) (maps snd eqns), ctxt);
+fun meta_rewrite eqns ctxt =
+ (map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) (maps snd eqns), ctxt);
fun note_eqns_register note activate deps witss def_eqns eqns attrss export export' ctxt =
let
@@ -172,11 +106,16 @@
note_eqns_register note add_registration deps witss def_eqns eqns attrss export export';
in setup_proof after_qed propss eqns goal_ctxt end;
+fun generic_interpretation prep_interpretation setup_proof note add_registration expression =
+ generic_interpretation_with_defs prep_interpretation setup_proof note add_registration expression [];
+
end;
(** first dimension: proof vs. local theory **)
+local
+
(* proof *)
fun gen_interpret prep_interpretation expression raw_eqns int state =
@@ -200,10 +139,7 @@
generic_interpretation prep_interpretation Element.witness_proof_eqs
Local_Theory.notes_kind (activate lthy) expression raw_eqns lthy;
-
-(* local theory with mixin definitions *)
-
-fun gen_interpretation_with_defs prep_interpretation expression raw_defs raw_eqns =
+fun gen_interpretation prep_interpretation expression raw_defs raw_eqns =
Local_Theory.assert_bottom true
#> generic_interpretation_with_defs prep_interpretation Element.witness_proof_eqs
Local_Theory.notes_kind Local_Theory.subscription expression raw_defs raw_eqns
@@ -251,8 +187,8 @@
fun ephemeral_interpretation x =
gen_local_theory_interpretation cert_interpretation (K Locale.activate_fragment) x;
-fun permanent_interpretation x = gen_interpretation_with_defs cert_interpretation_with_defs x;
-fun permanent_interpretation_cmd x = gen_interpretation_with_defs read_interpretation_with_defs x;
+fun permanent_interpretation x = gen_interpretation cert_interpretation x;
+fun permanent_interpretation_cmd x = gen_interpretation read_interpretation x;
fun interpretation x =
gen_local_theory_interpretation cert_interpretation subscribe_or_activate x;