src/Pure/Isar/expression.ML
changeset 52140 88a69da5d3fa
parent 52119 90ba620333d0
child 52148 893b15200ec1
     1.1 --- a/src/Pure/Isar/expression.ML	Sat May 25 13:59:08 2013 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Sat May 25 15:44:08 2013 +0200
     1.3 @@ -810,29 +810,34 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun read_with_extended_syntax parse_prop deps ctxt props =
     1.8 +(* reading *)
     1.9 +
    1.10 +fun read_with_extended_syntax prep_prop deps ctxt props =
    1.11    let
    1.12      val deps_ctxt = fold Locale.activate_declarations deps ctxt;
    1.13    in
    1.14 -    map (parse_prop deps_ctxt o snd) props |> Syntax.check_terms deps_ctxt
    1.15 +    map (prep_prop deps_ctxt o snd) props |> Syntax.check_terms deps_ctxt
    1.16        |> Variable.export_terms deps_ctxt ctxt
    1.17    end;
    1.18  
    1.19 -fun read_interpretation prep_expr parse_prop prep_attr expression raw_eqns initial_ctxt =
    1.20 +fun read_interpretation prep_expr prep_prop prep_attr expression raw_eqns initial_ctxt =
    1.21    let
    1.22      val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt;
    1.23 -    val eqns = read_with_extended_syntax parse_prop deps expr_ctxt raw_eqns;
    1.24 +    val eqns = read_with_extended_syntax prep_prop deps expr_ctxt raw_eqns;
    1.25      val attrss = map (apsnd (map (prep_attr (Proof_Context.theory_of initial_ctxt))) o fst) raw_eqns;
    1.26      val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
    1.27      val export' = Variable.export_morphism goal_ctxt expr_ctxt;
    1.28    in (((propss, deps, export, export'), (eqns, attrss)), goal_ctxt) end;
    1.29  
    1.30 +
    1.31 +(* generic interpretation machinery *)
    1.32 +
    1.33  fun meta_rewrite eqns ctxt = (map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) (maps snd eqns), ctxt);
    1.34  
    1.35  fun note_eqns_register note activate deps witss eqns attrss export export' ctxt =
    1.36    let
    1.37 -    val facts = 
    1.38 -      (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns);
    1.39 +    val facts = map2 (fn attrs => fn eqn =>
    1.40 +      (attrs, [([Morphism.thm (export' $> export) eqn], [])])) attrss eqns;
    1.41      val (eqns', ctxt') = ctxt
    1.42        |> note Thm.lemmaK facts
    1.43        |-> meta_rewrite;
    1.44 @@ -845,24 +850,22 @@
    1.45      |> fold activate' dep_morphs
    1.46    end;
    1.47  
    1.48 -fun generic_interpretation prep_expr parse_prop prep_attr setup_proof note add_registration
    1.49 +fun generic_interpretation prep_expr prep_prop prep_attr setup_proof note activate
    1.50      expression raw_eqns initial_ctxt = 
    1.51    let
    1.52      val (((propss, deps, export, export'), (eqns, attrss)), goal_ctxt) = 
    1.53 -      read_interpretation prep_expr parse_prop prep_attr expression raw_eqns initial_ctxt;
    1.54 +      read_interpretation prep_expr prep_prop prep_attr expression raw_eqns initial_ctxt;
    1.55      fun after_qed witss eqns =
    1.56 -      note_eqns_register note add_registration deps witss eqns attrss export export';
    1.57 +      note_eqns_register note activate deps witss eqns attrss export export';
    1.58    in setup_proof after_qed propss eqns goal_ctxt end;
    1.59  
    1.60 -val activate_proof = Context.proof_map ooo Locale.add_registration;
    1.61 -val activate_local_theory = Local_Theory.surface_target ooo activate_proof;
    1.62 -val add_registration = Local_Theory.raw_theory o Context.theory_map ooo Locale.add_registration;
    1.63 -fun add_dependency locale dep_morph mixin export =
    1.64 -  (Local_Theory.raw_theory ooo Locale.add_dependency locale) dep_morph mixin export
    1.65 -  #> activate_local_theory dep_morph mixin export;
    1.66 -fun add_dependency_global locale = Proof_Context.background_theory ooo Locale.add_dependency locale;
    1.67 +
    1.68 +(* various flavours of interpretation *)
    1.69  
    1.70 -fun gen_interpret prep_expr parse_prop prep_attr expression raw_eqns int state =
    1.71 +fun assert_not_theory lthy = if Named_Target.is_theory lthy
    1.72 +  then error "Not possible on level of global theory" else ();
    1.73 +
    1.74 +fun gen_interpret prep_expr prep_prop prep_attr expression raw_eqns int state =
    1.75    let
    1.76      val _ = Proof.assert_forward_or_chain state;
    1.77      val ctxt = Proof.context_of state;
    1.78 @@ -870,43 +873,40 @@
    1.79      fun setup_proof after_qed propss eqns goal_ctxt = 
    1.80        Element.witness_local_proof_eqs (lift_after_qed after_qed) "interpret" propss eqns goal_ctxt int state;
    1.81    in
    1.82 -    generic_interpretation prep_expr parse_prop prep_attr setup_proof
    1.83 -      Attrib.local_notes activate_proof expression raw_eqns ctxt
    1.84 +    generic_interpretation prep_expr prep_prop prep_attr setup_proof
    1.85 +      Attrib.local_notes (Context.proof_map ooo Locale.add_registration) expression raw_eqns ctxt
    1.86    end;
    1.87  
    1.88 -fun gen_interpretation prep_expr parse_prop prep_attr expression raw_eqns lthy =
    1.89 +fun gen_interpretation prep_expr prep_prop prep_attr expression raw_eqns lthy =
    1.90 +  if Named_Target.is_theory lthy
    1.91 +  then 
    1.92 +    lthy
    1.93 +    |> generic_interpretation prep_expr prep_prop prep_attr Element.witness_proof_eqs
    1.94 +        Local_Theory.notes_kind Local_Theory.add_registration expression raw_eqns
    1.95 +  else
    1.96 +    lthy
    1.97 +    |> generic_interpretation prep_expr prep_prop prep_attr Element.witness_proof_eqs
    1.98 +        Local_Theory.notes_kind Local_Theory.activate expression raw_eqns;
    1.99 +
   1.100 +fun gen_sublocale prep_expr prep_prop prep_attr expression raw_eqns lthy =
   1.101    let
   1.102 -    val is_theory = Option.map #target (Named_Target.peek lthy) = SOME ""
   1.103 -      andalso Local_Theory.level lthy = 1;
   1.104 -    val activate = if is_theory then add_registration else activate_local_theory;
   1.105 -    val mark_brittle = if is_theory then I else Local_Theory.mark_brittle;
   1.106 +    val _ = assert_not_theory lthy;
   1.107 +    val locale = Named_Target.the_name lthy;
   1.108    in
   1.109      lthy
   1.110 -    |> mark_brittle
   1.111 -    |> generic_interpretation prep_expr parse_prop prep_attr Element.witness_proof_eqs
   1.112 -        Local_Theory.notes_kind activate expression raw_eqns
   1.113 -  end;
   1.114 -
   1.115 -fun gen_sublocale prep_expr parse_prop prep_attr expression raw_eqns lthy =
   1.116 -  let
   1.117 -    val locale =
   1.118 -      case Option.map #target (Named_Target.peek lthy) of
   1.119 -          SOME locale => locale
   1.120 -        | _ => error "Not in a locale target";
   1.121 -  in
   1.122 -    lthy
   1.123 -    |> generic_interpretation prep_expr parse_prop prep_attr Element.witness_proof_eqs
   1.124 -        Local_Theory.notes_kind (add_dependency locale) expression raw_eqns
   1.125 +    |> generic_interpretation prep_expr prep_prop prep_attr Element.witness_proof_eqs
   1.126 +        Local_Theory.notes_kind (Local_Theory.add_dependency locale) expression raw_eqns
   1.127    end;
   1.128    
   1.129 -fun gen_sublocale_global prep_expr prep_loc parse_prop prep_attr before_exit raw_locale expression raw_eqns thy =
   1.130 +fun gen_sublocale_global prep_expr prep_loc prep_prop prep_attr before_exit raw_locale expression raw_eqns thy =
   1.131    let
   1.132      val locale = prep_loc thy raw_locale;
   1.133 +    val add_dependency_global = Proof_Context.background_theory ooo Locale.add_dependency locale;
   1.134    in
   1.135      thy
   1.136      |> Named_Target.init before_exit locale
   1.137 -    |> generic_interpretation prep_expr parse_prop prep_attr Element.witness_proof_eqs
   1.138 -        Local_Theory.notes_kind (add_dependency_global locale) expression raw_eqns
   1.139 +    |> generic_interpretation prep_expr prep_prop prep_attr Element.witness_proof_eqs
   1.140 +        Local_Theory.notes_kind add_dependency_global expression raw_eqns
   1.141    end;
   1.142  
   1.143  in
   1.144 @@ -914,27 +914,22 @@
   1.145  fun permanent_interpretation expression raw_eqns lthy =
   1.146    let
   1.147      val _ = Local_Theory.assert_bottom true lthy;
   1.148 -    val target = case Named_Target.peek lthy of
   1.149 -          SOME { target, ... } => target
   1.150 -        | NONE => error "Not in a named target";
   1.151 -    val is_theory = (target = "");
   1.152 -    val activate = if is_theory then add_registration else add_dependency target;
   1.153 +    val target = Named_Target.the_name lthy;
   1.154 +    val subscribe = if target = "" then Local_Theory.add_registration
   1.155 +      else Local_Theory.add_dependency target;
   1.156    in
   1.157      lthy
   1.158      |> generic_interpretation cert_goal_expression (K I) (K I) Element.witness_proof_eqs
   1.159 -        Local_Theory.notes_kind activate expression raw_eqns
   1.160 +        Local_Theory.notes_kind subscribe expression raw_eqns
   1.161    end;
   1.162  
   1.163  fun ephemeral_interpretation expression raw_eqns lthy =
   1.164    let
   1.165 -    val _ = if Option.map #target (Named_Target.peek lthy) = SOME ""
   1.166 -      andalso Local_Theory.level lthy = 1
   1.167 -      then error "Not possible on level of global theory" else ();
   1.168 +    val _ = assert_not_theory lthy;
   1.169    in
   1.170      lthy
   1.171 -    |> Local_Theory.mark_brittle
   1.172      |> generic_interpretation cert_goal_expression (K I) (K I) Element.witness_proof_eqs
   1.173 -        Local_Theory.notes_kind activate_local_theory expression raw_eqns
   1.174 +        Local_Theory.notes_kind Local_Theory.activate expression raw_eqns
   1.175    end;
   1.176  
   1.177  fun interpret x = gen_interpret cert_goal_expression (K I) (K I) x;