target-sensitive user-level commands interpretation and sublocale
authorhaftmann
Tue Apr 23 11:14:50 2013 +0200 (2013-04-23)
changeset 51737718866dda2fa
parent 51736 1f66d74b8ce3
child 51738 9e4220605179
target-sensitive user-level commands interpretation and sublocale
src/HOL/Statespace/state_space.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/isar_syn.ML
     1.1 --- a/src/HOL/Statespace/state_space.ML	Tue Apr 23 11:14:50 2013 +0200
     1.2 +++ b/src/HOL/Statespace/state_space.ML	Tue Apr 23 11:14:50 2013 +0200
     1.3 @@ -144,7 +144,7 @@
     1.4  
     1.5  fun prove_interpretation_in ctxt_tac (name, expr) thy =
     1.6     thy
     1.7 -   |> Expression.sublocale_cmd I (name, Position.none) (expression_no_pos expr) []
     1.8 +   |> Expression.sublocale_global_cmd I (name, Position.none) (expression_no_pos expr) []
     1.9     |> Proof.global_terminal_proof
    1.10           ((Method.Basic (fn ctxt => SIMPLE_METHOD (ctxt_tac ctxt)), Position.no_range), NONE)
    1.11     |> Proof_Context.theory_of
     2.1 --- a/src/Pure/Isar/expression.ML	Tue Apr 23 11:14:50 2013 +0200
     2.2 +++ b/src/Pure/Isar/expression.ML	Tue Apr 23 11:14:50 2013 +0200
     2.3 @@ -44,11 +44,13 @@
     2.4    val interpret: expression_i -> (Attrib.binding * term) list -> bool -> Proof.state -> Proof.state
     2.5    val interpret_cmd: expression -> (Attrib.binding * string) list ->
     2.6      bool -> Proof.state -> Proof.state
     2.7 -  val interpretation: expression_i -> (Attrib.binding * term) list -> theory -> Proof.state
     2.8 -  val interpretation_cmd: expression -> (Attrib.binding * string) list -> theory -> Proof.state
     2.9 -  val sublocale: (local_theory -> local_theory) -> string -> expression_i ->
    2.10 +  val interpretation: expression_i -> (Attrib.binding * term) list -> local_theory -> Proof.state
    2.11 +  val interpretation_cmd: expression -> (Attrib.binding * string) list -> local_theory -> Proof.state
    2.12 +  val sublocale: expression_i -> (Attrib.binding * term) list -> local_theory -> Proof.state
    2.13 +  val sublocale_cmd: expression -> (Attrib.binding * string) list -> local_theory -> Proof.state
    2.14 +  val sublocale_global: (local_theory -> local_theory) -> string -> expression_i ->
    2.15      (Attrib.binding * term) list -> theory -> Proof.state
    2.16 -  val sublocale_cmd: (local_theory -> local_theory) -> xstring * Position.T -> expression ->
    2.17 +  val sublocale_global_cmd: (local_theory -> local_theory) -> xstring * Position.T -> expression ->
    2.18      (Attrib.binding * string) list -> theory -> Proof.state
    2.19  
    2.20    (* Diagnostic *)
    2.21 @@ -855,8 +857,10 @@
    2.22  
    2.23  val activate_proof = Context.proof_map ooo Locale.add_registration;
    2.24  val activate_local_theory = Local_Theory.target ooo activate_proof;
    2.25 -val add_registration = Proof_Context.background_theory o Context.theory_map ooo Locale.add_registration;
    2.26 -fun add_dependency locale = Proof_Context.background_theory ooo Locale.add_dependency locale;
    2.27 +val add_registration = Local_Theory.raw_theory o Context.theory_map ooo Locale.add_registration;
    2.28 +val add_registration_global = Proof_Context.background_theory o Context.theory_map ooo Locale.add_registration;
    2.29 +fun add_dependency locale = Local_Theory.raw_theory ooo Locale.add_dependency locale;
    2.30 +fun add_dependency_global locale = Proof_Context.background_theory ooo Locale.add_dependency locale;
    2.31  
    2.32  fun gen_interpret prep_expr parse_prop prep_attr expression raw_eqns int state =
    2.33    let
    2.34 @@ -870,20 +874,37 @@
    2.35        Attrib.local_notes activate_proof I expression raw_eqns ctxt
    2.36    end;
    2.37  
    2.38 -fun gen_interpretation prep_expr parse_prop prep_attr expression raw_eqns thy =
    2.39 -  thy
    2.40 -  |> Named_Target.theory_init
    2.41 -  |> generic_interpretation prep_expr parse_prop prep_attr Element.witness_proof_eqs
    2.42 -      Local_Theory.notes_kind add_registration I expression raw_eqns;
    2.43 +fun gen_interpretation prep_expr parse_prop prep_attr expression raw_eqns lthy =
    2.44 +  let
    2.45 +    val is_theory = Option.map #target (Named_Target.peek lthy) = SOME ""
    2.46 +      andalso Local_Theory.level lthy = 1;
    2.47 +    val activate = if is_theory then add_registration else activate_local_theory;
    2.48 +  in
    2.49 +    lthy
    2.50 +    |> generic_interpretation prep_expr parse_prop prep_attr Element.witness_proof_eqs
    2.51 +        Local_Theory.notes_kind activate I expression raw_eqns
    2.52 +  end;
    2.53  
    2.54 -fun gen_sublocale prep_expr prep_loc parse_prop prep_attr before_exit raw_locale expression raw_eqns thy =
    2.55 +fun gen_sublocale prep_expr parse_prop prep_attr expression raw_eqns lthy =
    2.56 +  let
    2.57 +    val locale =
    2.58 +      case Option.map #target (Named_Target.peek lthy) of
    2.59 +          SOME locale => locale
    2.60 +        | _ => error "Not in a locale target";
    2.61 +  in
    2.62 +    lthy
    2.63 +    |> generic_interpretation prep_expr parse_prop prep_attr Element.witness_proof_eqs
    2.64 +        Local_Theory.notes_kind (add_dependency locale) (Named_Target.reinit lthy) expression raw_eqns
    2.65 +  end;
    2.66 +  
    2.67 +fun gen_sublocale_global prep_expr prep_loc parse_prop prep_attr before_exit raw_locale expression raw_eqns thy =
    2.68    let
    2.69      val locale = prep_loc thy raw_locale;
    2.70    in
    2.71      thy
    2.72      |> Named_Target.init before_exit locale
    2.73      |> generic_interpretation prep_expr parse_prop prep_attr Element.witness_proof_eqs
    2.74 -        Local_Theory.notes_kind (add_dependency locale) I expression raw_eqns
    2.75 +        Local_Theory.notes_kind (add_dependency_global locale) I expression raw_eqns
    2.76    end;
    2.77  
    2.78  in
    2.79 @@ -916,16 +937,20 @@
    2.80    end;
    2.81  
    2.82  fun interpret x = gen_interpret cert_goal_expression (K I) (K I) x;
    2.83 -fun interpret_cmd x = gen_interpret read_goal_expression
    2.84 -  Syntax.parse_prop Attrib.intern_src x;
    2.85 +fun interpret_cmd x =
    2.86 +  gen_interpret read_goal_expression Syntax.parse_prop Attrib.intern_src x;
    2.87  
    2.88  fun interpretation x = gen_interpretation cert_goal_expression (K I) (K I) x;
    2.89 -fun interpretation_cmd x = gen_interpretation read_goal_expression
    2.90 -  Syntax.parse_prop Attrib.intern_src x;
    2.91 +fun interpretation_cmd x =
    2.92 +  gen_interpretation read_goal_expression Syntax.parse_prop Attrib.intern_src x;
    2.93  
    2.94 -fun sublocale x = gen_sublocale cert_goal_expression (K I) (K I) (K I) x;
    2.95 +fun sublocale x = gen_sublocale cert_goal_expression (K I) (K I) x;
    2.96  fun sublocale_cmd x =
    2.97 -  gen_sublocale read_goal_expression Locale.check Syntax.parse_prop Attrib.intern_src x;
    2.98 +  gen_sublocale read_goal_expression Syntax.parse_prop Attrib.intern_src x;
    2.99 +
   2.100 +fun sublocale_global x = gen_sublocale_global cert_goal_expression (K I) (K I) (K I) x;
   2.101 +fun sublocale_global_cmd x =
   2.102 +  gen_sublocale_global read_goal_expression Locale.check Syntax.parse_prop Attrib.intern_src x;
   2.103  
   2.104  end;
   2.105  
     3.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Apr 23 11:14:50 2013 +0200
     3.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Apr 23 11:14:50 2013 +0200
     3.3 @@ -419,17 +419,20 @@
     3.4  val _ =
     3.5    Outer_Syntax.command @{command_spec "sublocale"}
     3.6      "prove sublocale relation between a locale and a locale expression"
     3.7 -    (Parse.position Parse.xname --| (@{keyword "\<subseteq>"} || @{keyword "<"}) --
     3.8 +    ((Parse.position Parse.xname --| (@{keyword "\<subseteq>"} || @{keyword "<"}) --
     3.9        parse_interpretation_arguments false
    3.10        >> (fn (loc, (expr, equations)) =>
    3.11 -          Toplevel.print o Toplevel.theory_to_proof (Expression.sublocale_cmd I loc expr equations)));
    3.12 +          Toplevel.print o Toplevel.theory_to_proof (Expression.sublocale_global_cmd I loc expr equations)))
    3.13 +    || parse_interpretation_arguments false
    3.14 +      >> (fn (expr, equations) => Toplevel.print o
    3.15 +          Toplevel.local_theory_to_proof NONE (Expression.sublocale_cmd expr equations)));
    3.16  
    3.17  val _ =
    3.18    Outer_Syntax.command @{command_spec "interpretation"}
    3.19 -    "prove interpretation of locale expression in theory"
    3.20 +    "prove interpretation of locale expression in local theory"
    3.21      (parse_interpretation_arguments true
    3.22        >> (fn (expr, equations) => Toplevel.print o
    3.23 -          Toplevel.theory_to_proof (Expression.interpretation_cmd expr equations)));
    3.24 +          Toplevel.local_theory_to_proof NONE (Expression.interpretation_cmd expr equations)));
    3.25  
    3.26  val _ =
    3.27    Outer_Syntax.command @{command_spec "interpret"}