# HG changeset patch # User haftmann # Date 1447487152 -3600 # Node ID 87203a0f0041993a5dbbf9c7e04f424fe8efa524 # Parent 20d4cd2ceab2b473f74635ec2702b92e3610f6c7 tuned -- share implementations as far as appropriate diff -r 20d4cd2ceab2 -r 87203a0f0041 src/Pure/Isar/interpretation.ML --- 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;