added before_exit continuation for named targets (locale, class etc.), e.g. for final check/cleanup as in VC management;
authorwenzelm
Sun Jan 16 14:57:14 2011 +0100 (2011-01-16)
changeset 4158545d7da4e4ccf
parent 41584 2b07a4212d6d
child 41586 1f930561a560
added before_exit continuation for named targets (locale, class etc.), e.g. for final check/cleanup as in VC management;
src/HOL/Statespace/ROOT.ML
src/HOL/Statespace/state_space.ML
src/Pure/Isar/class_declaration.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/named_target.ML
     1.1 --- a/src/HOL/Statespace/ROOT.ML	Sat Jan 15 22:40:17 2011 +0100
     1.2 +++ b/src/HOL/Statespace/ROOT.ML	Sun Jan 16 14:57:14 2011 +0100
     1.3 @@ -1,1 +1,1 @@
     1.4 -use_thys ["StateSpaceEx"];
     1.5 \ No newline at end of file
     1.6 +use_thys ["StateSpaceEx"];
     2.1 --- a/src/HOL/Statespace/state_space.ML	Sat Jan 15 22:40:17 2011 +0100
     2.2 +++ b/src/HOL/Statespace/state_space.ML	Sun Jan 16 14:57:14 2011 +0100
     2.3 @@ -145,20 +145,20 @@
     2.4  
     2.5  fun prove_interpretation_in ctxt_tac (name, expr) thy =
     2.6     thy
     2.7 -   |> Expression.sublocale_cmd name expr []
     2.8 +   |> Expression.sublocale_cmd I name expr []
     2.9     |> Proof.global_terminal_proof
    2.10           (Method.Basic (fn ctxt => SIMPLE_METHOD (ctxt_tac ctxt)), NONE)
    2.11     |> ProofContext.theory_of
    2.12  
    2.13  fun add_locale name expr elems thy =
    2.14    thy 
    2.15 -  |> Expression.add_locale (Binding.name name) (Binding.name name) expr elems
    2.16 +  |> Expression.add_locale I (Binding.name name) (Binding.name name) expr elems
    2.17    |> snd
    2.18    |> Local_Theory.exit;
    2.19  
    2.20  fun add_locale_cmd name expr elems thy =
    2.21    thy 
    2.22 -  |> Expression.add_locale_cmd (Binding.name name) Binding.empty expr elems
    2.23 +  |> Expression.add_locale_cmd I (Binding.name name) Binding.empty expr elems
    2.24    |> snd
    2.25    |> Local_Theory.exit;
    2.26  
    2.27 @@ -349,7 +349,7 @@
    2.28  
    2.29  fun add_declaration name decl thy =
    2.30    thy
    2.31 -  |> Named_Target.init name
    2.32 +  |> Named_Target.init I name
    2.33    |> (fn lthy => Local_Theory.declaration false (decl lthy) lthy)
    2.34    |> Local_Theory.exit_global;
    2.35  
     3.1 --- a/src/Pure/Isar/class_declaration.ML	Sat Jan 15 22:40:17 2011 +0100
     3.2 +++ b/src/Pure/Isar/class_declaration.ML	Sun Jan 16 14:57:14 2011 +0100
     3.3 @@ -6,13 +6,14 @@
     3.4  
     3.5  signature CLASS_DECLARATION =
     3.6  sig
     3.7 -  val class: binding -> class list -> Element.context_i list
     3.8 -    -> theory -> string * local_theory
     3.9 -  val class_cmd: binding -> xstring list -> Element.context list
    3.10 -    -> theory -> string * local_theory
    3.11 -  val prove_subclass: tactic -> class -> local_theory -> local_theory
    3.12 -  val subclass: class -> local_theory -> Proof.state
    3.13 -  val subclass_cmd: xstring -> local_theory -> Proof.state
    3.14 +  val class: (local_theory -> local_theory) -> binding -> class list ->
    3.15 +    Element.context_i list -> theory -> string * local_theory
    3.16 +  val class_cmd: (local_theory -> local_theory) -> binding -> xstring list ->
    3.17 +    Element.context list -> theory -> string * local_theory
    3.18 +  val prove_subclass: (local_theory -> local_theory) -> tactic -> class ->
    3.19 +    local_theory -> local_theory
    3.20 +  val subclass: (local_theory -> local_theory) -> class -> local_theory -> Proof.state
    3.21 +  val subclass_cmd: (local_theory -> local_theory) -> xstring -> local_theory -> Proof.state
    3.22  end;
    3.23  
    3.24  structure Class_Declaration: CLASS_DECLARATION =
    3.25 @@ -288,14 +289,14 @@
    3.26      #> pair (param_map, params, assm_axiom)))
    3.27    end;
    3.28  
    3.29 -fun gen_class prep_class_spec b raw_supclasses raw_elems thy =
    3.30 +fun gen_class prep_class_spec before_exit b raw_supclasses raw_elems thy =
    3.31    let
    3.32      val class = Sign.full_name thy b;
    3.33      val (((sups, supparam_names), (supsort, base_sort, supexpr)), (elems, global_syntax)) =
    3.34        prep_class_spec thy raw_supclasses raw_elems;
    3.35    in
    3.36      thy
    3.37 -    |> Expression.add_locale b (Binding.qualify true "class" b) supexpr elems
    3.38 +    |> Expression.add_locale I b (Binding.qualify true "class" b) supexpr elems
    3.39      |> snd |> Local_Theory.exit_global
    3.40      |> adjungate_axclass b class base_sort sups supsort supparam_names global_syntax
    3.41      ||> Theory.checkpoint
    3.42 @@ -305,7 +306,7 @@
    3.43         Context.theory_map (Locale.add_registration (class, base_morph)
    3.44           (Option.map (rpair true) eq_morph) export_morph)
    3.45      #> Class.register class sups params base_sort base_morph export_morph axiom assm_intro of_class))
    3.46 -    |> Named_Target.init class
    3.47 +    |> Named_Target.init before_exit class
    3.48      |> pair class
    3.49    end;
    3.50  
    3.51 @@ -321,7 +322,7 @@
    3.52  
    3.53  local
    3.54  
    3.55 -fun gen_subclass prep_class do_proof raw_sup lthy =
    3.56 +fun gen_subclass prep_class do_proof before_exit raw_sup lthy =
    3.57    let
    3.58      val thy = ProofContext.theory_of lthy;
    3.59      val proto_sup = prep_class thy raw_sup;
    3.60 @@ -338,7 +339,7 @@
    3.61      fun after_qed some_wit =
    3.62        ProofContext.background_theory (Class.register_subclass (sub, sup)
    3.63          some_dep_morph some_wit export)
    3.64 -      #> ProofContext.theory_of #> Named_Target.init sub;
    3.65 +      #> ProofContext.theory_of #> Named_Target.init before_exit sub;
    3.66    in do_proof after_qed some_prop goal_ctxt end;
    3.67  
    3.68  fun user_proof after_qed some_prop =
    3.69 @@ -352,7 +353,7 @@
    3.70  in
    3.71  
    3.72  val subclass = gen_subclass (K I) user_proof;
    3.73 -fun prove_subclass tac = gen_subclass (K I) (tactic_proof tac);
    3.74 +fun prove_subclass before_exit tac = gen_subclass (K I) (tactic_proof tac) before_exit;
    3.75  val subclass_cmd = gen_subclass (ProofContext.read_class o ProofContext.init_global) user_proof;
    3.76  
    3.77  end; (*local*)
     4.1 --- a/src/Pure/Isar/expression.ML	Sat Jan 15 22:40:17 2011 +0100
     4.2 +++ b/src/Pure/Isar/expression.ML	Sun Jan 16 14:57:14 2011 +0100
     4.3 @@ -29,20 +29,20 @@
     4.4    val read_declaration: expression -> (Proof.context -> Proof.context) -> Element.context list ->
     4.5      Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
     4.6        * Element.context_i list) * ((string * typ) list * Proof.context)
     4.7 -  val add_locale: binding -> binding -> expression_i -> Element.context_i list ->
     4.8 -    theory -> string * local_theory
     4.9 -  val add_locale_cmd: binding -> binding -> expression -> Element.context list ->
    4.10 -    theory -> string * local_theory
    4.11 +  val add_locale: (local_theory -> local_theory) -> binding -> binding ->
    4.12 +    expression_i -> Element.context_i list -> theory -> string * local_theory
    4.13 +  val add_locale_cmd: (local_theory -> local_theory) -> binding -> binding ->
    4.14 +    expression -> Element.context list -> theory -> string * local_theory
    4.15  
    4.16    (* Interpretation *)
    4.17    val cert_goal_expression: expression_i -> Proof.context ->
    4.18      (term list list * (string * morphism) list * morphism) * Proof.context
    4.19    val read_goal_expression: expression -> Proof.context ->
    4.20      (term list list * (string * morphism) list * morphism) * Proof.context
    4.21 -  val sublocale: string -> expression_i -> (Attrib.binding * term) list ->
    4.22 -    theory -> Proof.state
    4.23 -  val sublocale_cmd: string -> expression -> (Attrib.binding * string) list ->
    4.24 -    theory -> Proof.state
    4.25 +  val sublocale: (local_theory -> local_theory) -> string -> expression_i ->
    4.26 +    (Attrib.binding * term) list -> theory -> Proof.state
    4.27 +  val sublocale_cmd: (local_theory -> local_theory) -> string -> expression ->
    4.28 +    (Attrib.binding * string) list -> theory -> Proof.state
    4.29    val interpretation: expression_i -> (Attrib.binding * term) list ->
    4.30      theory -> Proof.state
    4.31    val interpretation_cmd: expression -> (Attrib.binding * string) list ->
    4.32 @@ -731,7 +731,7 @@
    4.33    | defines_to_notes _ e = e;
    4.34  
    4.35  fun gen_add_locale prep_decl
    4.36 -    binding raw_predicate_binding raw_import raw_body thy =
    4.37 +    before_exit binding raw_predicate_binding raw_import raw_body thy =
    4.38    let
    4.39      val name = Sign.full_name thy binding;
    4.40      val _ = Locale.defined thy name andalso
    4.41 @@ -784,7 +784,7 @@
    4.42      val loc_ctxt = thy'
    4.43        |> Locale.register_locale binding (extraTs, params)
    4.44            (asm, rev defs) (a_intro, b_intro) axioms [] (rev notes) (rev deps')
    4.45 -      |> Named_Target.init name
    4.46 +      |> Named_Target.init before_exit name
    4.47        |> fold (fn (kind, facts) => Local_Theory.notes_kind kind facts #> snd) notes';
    4.48  
    4.49    in (name, loc_ctxt) end;
    4.50 @@ -900,11 +900,11 @@
    4.51            export theory) (deps ~~ witss))
    4.52    end;
    4.53  
    4.54 -fun gen_sublocale prep_expr intern parse_prop prep_attr raw_target
    4.55 -    expression equations thy =
    4.56 +fun gen_sublocale prep_expr intern parse_prop prep_attr
    4.57 +    before_exit raw_target expression equations thy =
    4.58    let
    4.59      val target = intern thy raw_target;
    4.60 -    val target_ctxt = Named_Target.init target thy;
    4.61 +    val target_ctxt = Named_Target.init before_exit target thy;
    4.62      val ((propss, deps, export), expr_ctxt) = prep_expr expression target_ctxt;
    4.63  
    4.64      val eqns = map (parse_prop expr_ctxt o snd) equations |> Syntax.check_terms expr_ctxt;
    4.65 @@ -919,8 +919,8 @@
    4.66  in
    4.67  
    4.68  fun sublocale x = gen_sublocale cert_goal_expression (K I) (K I) (K I) x;
    4.69 -fun sublocale_cmd x = gen_sublocale read_goal_expression Locale.intern
    4.70 -  Syntax.parse_prop Attrib.intern_src x;
    4.71 +fun sublocale_cmd x =
    4.72 +  gen_sublocale read_goal_expression Locale.intern Syntax.parse_prop Attrib.intern_src x;
    4.73  
    4.74  end;
    4.75  
     5.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Jan 15 22:40:17 2011 +0100
     5.2 +++ b/src/Pure/Isar/isar_syn.ML	Sun Jan 16 14:57:14 2011 +0100
     5.3 @@ -413,7 +413,7 @@
     5.4        Scan.optional (Parse.$$$ "=" |-- Parse.!!! locale_val) (([], []), []) -- Parse.opt_begin
     5.5        >> (fn ((name, (expr, elems)), begin) =>
     5.6            (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
     5.7 -            (Expression.add_locale_cmd name Binding.empty expr elems #> snd)));
     5.8 +            (Expression.add_locale_cmd I name Binding.empty expr elems #> snd)));
     5.9  
    5.10  fun parse_interpretation_arguments mandatory =
    5.11    Parse.!!! (Parse_Spec.locale_expression mandatory) --
    5.12 @@ -426,7 +426,7 @@
    5.13      (Parse.xname --| (Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") --
    5.14        parse_interpretation_arguments false
    5.15        >> (fn (loc, (expr, equations)) =>
    5.16 -          Toplevel.print o Toplevel.theory_to_proof (Expression.sublocale_cmd loc expr equations)));
    5.17 +          Toplevel.print o Toplevel.theory_to_proof (Expression.sublocale_cmd I loc expr equations)));
    5.18  
    5.19  val _ =
    5.20    Outer_Syntax.command "interpretation"
    5.21 @@ -456,11 +456,11 @@
    5.22     (Parse.binding -- Scan.optional (Parse.$$$ "=" |-- class_val) ([], []) -- Parse.opt_begin
    5.23      >> (fn ((name, (supclasses, elems)), begin) =>
    5.24          (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
    5.25 -          (Class_Declaration.class_cmd name supclasses elems #> snd)));
    5.26 +          (Class_Declaration.class_cmd I name supclasses elems #> snd)));
    5.27  
    5.28  val _ =
    5.29    Outer_Syntax.local_theory_to_proof "subclass" "prove a subclass relation" Keyword.thy_goal
    5.30 -    (Parse.xname >> Class_Declaration.subclass_cmd);
    5.31 +    (Parse.xname >> Class_Declaration.subclass_cmd I);
    5.32  
    5.33  val _ =
    5.34    Outer_Syntax.command "instantiation" "instantiate and prove type arity" Keyword.thy_decl
     6.1 --- a/src/Pure/Isar/named_target.ML	Sat Jan 15 22:40:17 2011 +0100
     6.2 +++ b/src/Pure/Isar/named_target.ML	Sun Jan 16 14:57:14 2011 +0100
     6.3 @@ -7,7 +7,7 @@
     6.4  
     6.5  signature NAMED_TARGET =
     6.6  sig
     6.7 -  val init: string -> theory -> local_theory
     6.8 +  val init: (local_theory -> local_theory) -> string -> theory -> local_theory
     6.9    val theory_init: theory -> local_theory
    6.10    val reinit: local_theory -> local_theory -> local_theory
    6.11    val context_cmd: xstring -> theory -> local_theory
    6.12 @@ -19,12 +19,18 @@
    6.13  
    6.14  (* context data *)
    6.15  
    6.16 -datatype target = Target of {target: string, is_locale: bool, is_class: bool};
    6.17 +datatype target =
    6.18 +  Target of {target: string, is_locale: bool, is_class: bool,
    6.19 +    before_exit: local_theory -> local_theory};
    6.20  
    6.21 -fun named_target _ "" = Target {target = "", is_locale = false, is_class = false}
    6.22 -  | named_target thy locale =
    6.23 +fun make_target target is_locale is_class before_exit =
    6.24 +  Target {target = target, is_locale = is_locale, is_class = is_class,
    6.25 +    before_exit = before_exit};
    6.26 +
    6.27 +fun named_target _ "" before_exit = make_target "" false false before_exit
    6.28 +  | named_target thy locale before_exit =
    6.29        if Locale.defined thy locale
    6.30 -      then Target {target = locale, is_locale = true, is_class = Class.is_class thy locale}
    6.31 +      then make_target locale true (Class.is_class thy locale) before_exit
    6.32        else error ("No such locale: " ^ quote locale);
    6.33  
    6.34  structure Data = Proof_Data
    6.35 @@ -33,7 +39,9 @@
    6.36    fun init _ = NONE;
    6.37  );
    6.38  
    6.39 -val peek = Option.map (fn Target args => args) o Data.get;
    6.40 +val peek =
    6.41 +  Data.get #> Option.map (fn Target {target, is_locale, is_class, ...} =>
    6.42 +    {target = target, is_locale = is_locale, is_class = is_class});
    6.43  
    6.44  
    6.45  (* generic declarations *)
    6.46 @@ -169,14 +177,14 @@
    6.47  
    6.48  (* init *)
    6.49  
    6.50 -fun init_context (Target {target, is_locale, is_class}) =
    6.51 +fun init_context (Target {target, is_locale, is_class, ...}) =
    6.52    if not is_locale then ProofContext.init_global
    6.53    else if not is_class then Locale.init target
    6.54    else Class.init target;
    6.55  
    6.56 -fun init target thy =
    6.57 +fun init before_exit target thy =
    6.58    let
    6.59 -    val ta = named_target thy target;
    6.60 +    val ta = named_target thy target before_exit;
    6.61    in
    6.62      thy
    6.63      |> init_context ta
    6.64 @@ -190,17 +198,17 @@
    6.65          syntax_declaration = fn pervasive => target_declaration ta
    6.66            {syntax = true, pervasive = pervasive},
    6.67          pretty = pretty ta,
    6.68 -        exit = Local_Theory.target_of}
    6.69 +        exit = Local_Theory.target_of o before_exit}
    6.70    end;
    6.71  
    6.72 -val theory_init = init "";
    6.73 +val theory_init = init I "";
    6.74  
    6.75  fun reinit lthy =
    6.76 -  (case peek lthy of
    6.77 -    SOME {target, ...} => init target o Local_Theory.exit_global
    6.78 +  (case Data.get lthy of
    6.79 +    SOME (Target {target, before_exit, ...}) => init before_exit target o Local_Theory.exit_global
    6.80    | NONE => error "Not in a named target");
    6.81  
    6.82 -fun context_cmd "-" thy = init "" thy
    6.83 -  | context_cmd target thy = init (Locale.intern thy target) thy;
    6.84 +fun context_cmd "-" thy = init I "" thy
    6.85 +  | context_cmd target thy = init I (Locale.intern thy target) thy;
    6.86  
    6.87  end;