uniform mandatory qualifier for all locale expressions, including 'statespace' parent;
authorwenzelm
Mon Nov 09 21:04:49 2015 +0100 (2015-11-09)
changeset 616066d5213bd9709
parent 61605 1bf7b186542e
child 61607 a99125aa964f
uniform mandatory qualifier for all locale expressions, including 'statespace' parent;
removed obsolete '!' syntax;
NEWS
src/Doc/Isar_Ref/Spec.thy
src/HOL/Statespace/state_space.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/parse_spec.ML
src/Tools/permanent_interpretation.ML
     1.1 --- a/NEWS	Mon Nov 09 15:48:17 2015 +0100
     1.2 +++ b/NEWS	Mon Nov 09 21:04:49 2015 +0100
     1.3 @@ -276,12 +276,13 @@
     1.4  
     1.5  *** Pure ***
     1.6  
     1.7 -* Qualifiers in locale expressions default to mandatory ('!')
     1.8 -regardless of the command.  Previously, for 'locale' and 'sublocale'
     1.9 -the default was optional ('?').  INCOMPATIBILITY
    1.10 +* Qualifiers in locale expressions default to mandatory ('!') regardless
    1.11 +of the command. Previously, for 'locale' and 'sublocale' the default was
    1.12 +optional ('?'). The old synatx '!' has been discontinued.
    1.13 +INCOMPATIBILITY, remove '!' and add '?' as required.
    1.14  
    1.15  * Keyword 'rewrites' identifies rewrite morphisms in interpretation
    1.16 -commands.  Previously, the keyword was 'where'.  INCOMPATIBILITY
    1.17 +commands.  Previously, the keyword was 'where'.  INCOMPATIBILITY.
    1.18  
    1.19  * Command 'print_definitions' prints dependencies of definitional
    1.20  specifications. This functionality used to be part of 'print_theory'.
    1.21 @@ -501,7 +502,12 @@
    1.22  
    1.23  * Imperative_HOL: obsolete theory Legacy_Mrec has been removed.
    1.24  
    1.25 -* Library/Omega_Words_Fun: Infinite words modeled as functions nat => 'a.
    1.26 +* Library/Omega_Words_Fun: Infinite words modeled as functions nat =>
    1.27 +'a.
    1.28 +
    1.29 +* HOL-Statespace: command 'statespace' uses mandatory qualifier for
    1.30 +import of parent, as for general 'locale' expressions. INCOMPATIBILITY,
    1.31 +remove '!' and add '?' as required.
    1.32  
    1.33  
    1.34  *** ML ***
     2.1 --- a/src/Doc/Isar_Ref/Spec.thy	Mon Nov 09 15:48:17 2015 +0100
     2.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Mon Nov 09 21:04:49 2015 +0100
     2.3 @@ -462,44 +462,41 @@
     2.4  subsection \<open>Locale expressions \label{sec:locale-expr}\<close>
     2.5  
     2.6  text \<open>
     2.7 -  A \<^emph>\<open>locale expression\<close> denotes a context composed of instances
     2.8 -  of existing locales.  The context consists of the declaration
     2.9 -  elements from the locale instances.  Redundant locale instances are
    2.10 -  omitted according to roundup.
    2.11 +  A \<^emph>\<open>locale expression\<close> denotes a context composed of instances of existing
    2.12 +  locales. The context consists of the declaration elements from the locale
    2.13 +  instances. Redundant locale instances are omitted according to roundup.
    2.14  
    2.15    @{rail \<open>
    2.16      @{syntax_def locale_expr}: (instance + '+') @{syntax for_fixes}
    2.17      ;
    2.18      instance: (qualifier ':')? @{syntax nameref} (pos_insts | named_insts)
    2.19      ;
    2.20 -    qualifier: @{syntax name} ('?' | '!')?
    2.21 +    qualifier: @{syntax name} ('?')?
    2.22      ;
    2.23      pos_insts: ('_' | @{syntax term})*
    2.24      ;
    2.25      named_insts: @'where' (@{syntax name} '=' @{syntax term} + @'and')
    2.26    \<close>}
    2.27  
    2.28 -  A locale instance consists of a reference to a locale and either
    2.29 -  positional or named parameter instantiations.  Identical
    2.30 -  instantiations (that is, those that instantiate a parameter by itself)
    2.31 -  may be omitted.  The notation `\<open>_\<close>' enables to omit the
    2.32 -  instantiation for a parameter inside a positional instantiation.
    2.33 +  A locale instance consists of a reference to a locale and either positional
    2.34 +  or named parameter instantiations. Identical instantiations (that is, those
    2.35 +  that instantiate a parameter by itself) may be omitted. The notation ``\<open>_\<close>''
    2.36 +  enables to omit the instantiation for a parameter inside a positional
    2.37 +  instantiation.
    2.38  
    2.39 -  Terms in instantiations are from the context the locale expressions
    2.40 -  is declared in.  Local names may be added to this context with the
    2.41 -  optional @{keyword "for"} clause.  This is useful for shadowing names
    2.42 -  bound in outer contexts, and for declaring syntax.  In addition,
    2.43 -  syntax declarations from one instance are effective when parsing
    2.44 -  subsequent instances of the same expression.
    2.45 +  Terms in instantiations are from the context the locale expressions is
    2.46 +  declared in. Local names may be added to this context with the optional
    2.47 +  @{keyword "for"} clause. This is useful for shadowing names bound in outer
    2.48 +  contexts, and for declaring syntax. In addition, syntax declarations from
    2.49 +  one instance are effective when parsing subsequent instances of the same
    2.50 +  expression.
    2.51  
    2.52 -  Instances have an optional qualifier which applies to names in
    2.53 -  declarations.  Names include local definitions and theorem names.
    2.54 -  If present, the qualifier itself is either optional
    2.55 -  (``\<^verbatim>\<open>?\<close>''), which means that it may be omitted on input of the
    2.56 -  qualified name, or mandatory (``\<^verbatim>\<open>!\<close>'').  If neither
    2.57 -  ``\<^verbatim>\<open>?\<close>'' nor ``\<^verbatim>\<open>!\<close>'' are present the default
    2.58 -  is used, which is ``mandatory''.  Qualifiers play no role
    2.59 -  in determining whether one locale instance subsumes another.
    2.60 +  Instances have an optional qualifier which applies to names in declarations.
    2.61 +  Names include local definitions and theorem names. If present, the qualifier
    2.62 +  itself is either mandatory (default) or non-mandatory (when followed by
    2.63 +  ``\<^verbatim>\<open>?\<close>''). Non-mandatory means that the qualifier may be omitted on input.
    2.64 +  Qualifiers only affect name spaces; they play no role in determining whether
    2.65 +  one locale instance subsumes another.
    2.66  \<close>
    2.67  
    2.68  
     3.1 --- a/src/HOL/Statespace/state_space.ML	Mon Nov 09 15:48:17 2015 +0100
     3.2 +++ b/src/HOL/Statespace/state_space.ML	Mon Nov 09 21:04:49 2015 +0100
     3.3 @@ -642,7 +642,7 @@
     3.4  val renames = Scan.optional (@{keyword "["} |-- Parse.!!! (Parse.list1 rename --| @{keyword "]"})) [];
     3.5  
     3.6  val parent =
     3.7 -  Parse_Spec.locale_prefix false --
     3.8 +  Parse_Spec.locale_prefix --
     3.9    ((type_insts -- Parse.xname) || (Parse.xname >> pair [])) -- renames
    3.10      >> (fn ((prefix, (insts, name)), renames) => (prefix, (insts, name, renames)));
    3.11  
     4.1 --- a/src/Pure/Isar/isar_syn.ML	Mon Nov 09 15:48:17 2015 +0100
     4.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon Nov 09 21:04:49 2015 +0100
     4.3 @@ -384,7 +384,7 @@
     4.4  (* locales *)
     4.5  
     4.6  val locale_val =
     4.7 -  Parse_Spec.locale_expression true --
     4.8 +  Parse_Spec.locale_expression --
     4.9      Scan.optional (@{keyword "+"} |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] ||
    4.10    Scan.repeat1 Parse_Spec.context_element >> pair ([], []);
    4.11  
    4.12 @@ -403,7 +403,7 @@
    4.13            Toplevel.begin_local_theory true (Experiment.experiment_cmd elems #> snd)));
    4.14  
    4.15  val interpretation_args =
    4.16 -  Parse.!!! (Parse_Spec.locale_expression true) --
    4.17 +  Parse.!!! Parse_Spec.locale_expression --
    4.18      Scan.optional
    4.19        (@{keyword "rewrites"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [];
    4.20  
    4.21 @@ -817,7 +817,7 @@
    4.22  val _ =
    4.23    Outer_Syntax.command @{command_keyword print_dependencies}
    4.24      "print dependencies of locale expression"
    4.25 -    (Parse.opt_bang -- Parse_Spec.locale_expression true >> (fn (b, expr) =>
    4.26 +    (Parse.opt_bang -- Parse_Spec.locale_expression >> (fn (b, expr) =>
    4.27        Toplevel.keep (fn state => Expression.print_dependencies (Toplevel.context_of state) b expr)));
    4.28  
    4.29  val _ =
     5.1 --- a/src/Pure/Isar/parse_spec.ML	Mon Nov 09 15:48:17 2015 +0100
     5.2 +++ b/src/Pure/Isar/parse_spec.ML	Mon Nov 09 21:04:49 2015 +0100
     5.3 @@ -19,9 +19,9 @@
     5.4    val locale_fixes: (binding * string option * mixfix) list parser
     5.5    val locale_insts: (string option list * (Attrib.binding * string) list) parser
     5.6    val class_expression: string list parser
     5.7 -  val locale_prefix: bool -> (string * bool) parser
     5.8 +  val locale_prefix: (string * bool) parser
     5.9    val locale_keyword: string parser
    5.10 -  val locale_expression: bool -> Expression.expression parser
    5.11 +  val locale_expression: Expression.expression parser
    5.12    val context_element: Element.context parser
    5.13    val statement: (Attrib.binding * (string * string list) list) list parser
    5.14    val if_statement: (Attrib.binding * (string * string list) list) list parser
    5.15 @@ -105,11 +105,9 @@
    5.16  
    5.17  in
    5.18  
    5.19 -fun locale_prefix mandatory =
    5.20 +val locale_prefix =
    5.21    Scan.optional
    5.22 -    (Parse.name --
    5.23 -      (Parse.$$$ "!" >> K true || Parse.$$$ "?" >> K false || Scan.succeed mandatory) --|
    5.24 -      Parse.$$$ ":")
    5.25 +    (Parse.name -- (Scan.option (Parse.$$$ "?") >> is_none) --| Parse.$$$ ":")
    5.26      ("", false);
    5.27  
    5.28  val locale_keyword =
    5.29 @@ -118,10 +116,11 @@
    5.30  
    5.31  val class_expression = plus1_unless locale_keyword Parse.class;
    5.32  
    5.33 -fun locale_expression mandatory =
    5.34 +val locale_expression =
    5.35    let
    5.36      val expr2 = Parse.position Parse.xname;
    5.37 -    val expr1 = locale_prefix mandatory -- expr2 --
    5.38 +    val expr1 =
    5.39 +      locale_prefix -- expr2 --
    5.40        Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)));
    5.41      val expr0 = plus1_unless locale_keyword expr1;
    5.42    in expr0 -- Scan.optional (Parse.$$$ "for" |-- Parse.!!! locale_fixes) [] end;
     6.1 --- a/src/Tools/permanent_interpretation.ML	Mon Nov 09 15:48:17 2015 +0100
     6.2 +++ b/src/Tools/permanent_interpretation.ML	Mon Nov 09 21:04:49 2015 +0100
     6.3 @@ -99,7 +99,7 @@
     6.4  val _ =
     6.5    Outer_Syntax.local_theory_to_proof @{command_keyword permanent_interpretation}
     6.6      "prove interpretation of locale expression into named theory"
     6.7 -    (Parse.!!! (Parse_Spec.locale_expression true) --
     6.8 +    (Parse.!!! Parse_Spec.locale_expression --
     6.9        Scan.optional (@{keyword "defining"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
    6.10          -- ((Parse.binding -- Parse.opt_mixfix') --| @{keyword "="} -- Parse.term))) [] --
    6.11        Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []