added command 'experiment';
authorwenzelm
Wed Apr 01 22:08:06 2015 +0200 (2015-04-01)
changeset 59901840d03805755
parent 59900 a5591a15112e
child 59902 6afbe5a99139
added command 'experiment';
NEWS
src/Doc/Isar_Ref/Spec.thy
src/Pure/Isar/experiment.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Pure.thy
src/Pure/ROOT
src/Pure/ROOT.ML
     1.1 --- a/NEWS	Wed Apr 01 21:12:05 2015 +0200
     1.2 +++ b/NEWS	Wed Apr 01 22:08:06 2015 +0200
     1.3 @@ -6,6 +6,9 @@
     1.4  
     1.5  *** General ***
     1.6  
     1.7 +* Command 'experiment' opens an anonymous locale context with private
     1.8 +naming policy.
     1.9 +
    1.10  * Structural composition of proof methods (meth1; meth2) in Isar
    1.11  corresponds to (tac1 THEN_ALL_NEW tac2) in ML.
    1.12  
     2.1 --- a/src/Doc/Isar_Ref/Spec.thy	Wed Apr 01 21:12:05 2015 +0200
     2.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Wed Apr 01 22:08:06 2015 +0200
     2.3 @@ -501,6 +501,7 @@
     2.4  text \<open>
     2.5    \begin{matharray}{rcl}
     2.6      @{command_def "locale"} & : & @{text "theory \<rightarrow> local_theory"} \\
     2.7 +    @{command_def "experiment"} & : & @{text "theory \<rightarrow> local_theory"} \\
     2.8      @{command_def "print_locale"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     2.9      @{command_def "print_locales"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    2.10      @{command_def "locale_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    2.11 @@ -513,6 +514,8 @@
    2.12    @{rail \<open>
    2.13      @@{command locale} @{syntax name} ('=' @{syntax locale})? @'begin'?
    2.14      ;
    2.15 +    @@{command experiment} (@{syntax context_elem}*) @'begin'
    2.16 +    ;
    2.17      @@{command print_locale} '!'? @{syntax nameref}
    2.18      ;
    2.19      @{syntax_def locale}: @{syntax context_elem}+ |
    2.20 @@ -610,7 +613,12 @@
    2.21    @{text "\<Longrightarrow>"} by @{text "\<longrightarrow>"} in HOL; see also
    2.22    \secref{sec:object-logic}).  Separate introduction rules @{text
    2.23    loc_axioms.intro} and @{text loc.intro} are provided as well.
    2.24 -  
    2.25 +
    2.26 +  \item @{command experiment}~@{text exprs}~@{keyword "begin"} opens an
    2.27 +  anonymous locale context with private naming policy. Specifications in its
    2.28 +  body are inaccessible from outside. This is useful to perform experiments,
    2.29 +  without polluting the name space.
    2.30 +
    2.31    \item @{command "print_locale"}~@{text "locale"} prints the
    2.32    contents of the named locale.  The command omits @{element "notes"}
    2.33    elements by default.  Use @{command "print_locale"}@{text "!"} to
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/Isar/experiment.ML	Wed Apr 01 22:08:06 2015 +0200
     3.3 @@ -0,0 +1,29 @@
     3.4 +(*  Title:      Pure/Isar/experiment.ML
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +Target for specification experiments that are mostly private.
     3.8 +*)
     3.9 +
    3.10 +signature EXPERIMENT =
    3.11 +sig
    3.12 +  val experiment: Element.context_i list -> theory -> Binding.scope * local_theory
    3.13 +  val experiment_cmd: Element.context list -> theory -> Binding.scope * local_theory
    3.14 +end;
    3.15 +
    3.16 +structure Experiment: EXPERIMENT =
    3.17 +struct
    3.18 +
    3.19 +fun gen_experiment add_locale elems thy =
    3.20 +  let
    3.21 +    val (_, lthy) = thy
    3.22 +      |> add_locale (Binding.name ("experiment" ^ serial_string ())) Binding.empty ([], []) elems;
    3.23 +    val (scope, naming) =
    3.24 +      Name_Space.new_scope (Proof_Context.naming_of (Local_Theory.target_of lthy));
    3.25 +    val naming' = naming |> Name_Space.private scope;
    3.26 +    val lthy' = lthy |> Local_Theory.map_contexts (K (Proof_Context.map_naming (K naming')));
    3.27 +  in (scope, lthy') end;
    3.28 +
    3.29 +val experiment = gen_experiment Expression.add_locale;
    3.30 +val experiment_cmd = gen_experiment Expression.add_locale_cmd;
    3.31 +
    3.32 +end;
     4.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Apr 01 21:12:05 2015 +0200
     4.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Apr 01 22:08:06 2015 +0200
     4.3 @@ -373,13 +373,19 @@
     4.4    Scan.repeat1 Parse_Spec.context_element >> pair ([], []);
     4.5  
     4.6  val _ =
     4.7 -  Outer_Syntax.command @{command_spec "locale"} "define named proof context"
     4.8 +  Outer_Syntax.command @{command_spec "locale"} "define named specification context"
     4.9      (Parse.binding --
    4.10        Scan.optional (@{keyword "="} |-- Parse.!!! locale_val) (([], []), []) -- Parse.opt_begin
    4.11        >> (fn ((name, (expr, elems)), begin) =>
    4.12            Toplevel.begin_local_theory begin
    4.13              (Expression.add_locale_cmd name Binding.empty expr elems #> snd)));
    4.14  
    4.15 +val _ =
    4.16 +  Outer_Syntax.command @{command_spec "experiment"} "open private specification context"
    4.17 +    (Scan.repeat Parse_Spec.context_element --| Parse.begin
    4.18 +      >> (fn elems =>
    4.19 +          Toplevel.begin_local_theory true (Experiment.experiment_cmd elems #> snd)));
    4.20 +
    4.21  fun interpretation_args mandatory =
    4.22    Parse.!!! (Parse_Spec.locale_expression mandatory) --
    4.23      Scan.optional
     5.1 --- a/src/Pure/Pure.thy	Wed Apr 01 21:12:05 2015 +0200
     5.2 +++ b/src/Pure/Pure.thy	Wed Apr 01 22:08:06 2015 +0200
     5.3 @@ -33,7 +33,7 @@
     5.4    and "bundle" :: thy_decl
     5.5    and "include" "including" :: prf_decl
     5.6    and "print_bundles" :: diag
     5.7 -  and "context" "locale" :: thy_decl_block
     5.8 +  and "context" "locale" "experiment" :: thy_decl_block
     5.9    and "sublocale" "interpretation" :: thy_goal
    5.10    and "interpret" :: prf_goal % "proof"
    5.11    and "class" :: thy_decl_block
     6.1 --- a/src/Pure/ROOT	Wed Apr 01 21:12:05 2015 +0200
     6.2 +++ b/src/Pure/ROOT	Wed Apr 01 22:08:06 2015 +0200
     6.3 @@ -121,6 +121,7 @@
     6.4      "Isar/code.ML"
     6.5      "Isar/context_rules.ML"
     6.6      "Isar/element.ML"
     6.7 +    "Isar/experiment.ML"
     6.8      "Isar/expression.ML"
     6.9      "Isar/generic_target.ML"
    6.10      "Isar/isar_cmd.ML"
     7.1 --- a/src/Pure/ROOT.ML	Wed Apr 01 21:12:05 2015 +0200
     7.2 +++ b/src/Pure/ROOT.ML	Wed Apr 01 22:08:06 2015 +0200
     7.3 @@ -273,6 +273,7 @@
     7.4  use "Isar/expression.ML";
     7.5  use "Isar/class_declaration.ML";
     7.6  use "Isar/bundle.ML";
     7.7 +use "Isar/experiment.ML";
     7.8  
     7.9  use "simplifier.ML";
    7.10  use "Tools/plugin.ML";