# HG changeset patch # User wenzelm # Date 1447099489 -3600 # Node ID 6d5213bd9709ffd2d797b81eb7b0575fadc5bab7 # Parent 1bf7b186542e0c34b0afa3e30f578d253b90c88f uniform mandatory qualifier for all locale expressions, including 'statespace' parent; removed obsolete '!' syntax; diff -r 1bf7b186542e -r 6d5213bd9709 NEWS --- a/NEWS Mon Nov 09 15:48:17 2015 +0100 +++ b/NEWS Mon Nov 09 21:04:49 2015 +0100 @@ -276,12 +276,13 @@ *** Pure *** -* Qualifiers in locale expressions default to mandatory ('!') -regardless of the command. Previously, for 'locale' and 'sublocale' -the default was optional ('?'). INCOMPATIBILITY +* Qualifiers in locale expressions default to mandatory ('!') regardless +of the command. Previously, for 'locale' and 'sublocale' the default was +optional ('?'). The old synatx '!' has been discontinued. +INCOMPATIBILITY, remove '!' and add '?' as required. * Keyword 'rewrites' identifies rewrite morphisms in interpretation -commands. Previously, the keyword was 'where'. INCOMPATIBILITY +commands. Previously, the keyword was 'where'. INCOMPATIBILITY. * Command 'print_definitions' prints dependencies of definitional specifications. This functionality used to be part of 'print_theory'. @@ -501,7 +502,12 @@ * Imperative_HOL: obsolete theory Legacy_Mrec has been removed. -* Library/Omega_Words_Fun: Infinite words modeled as functions nat => 'a. +* Library/Omega_Words_Fun: Infinite words modeled as functions nat => +'a. + +* HOL-Statespace: command 'statespace' uses mandatory qualifier for +import of parent, as for general 'locale' expressions. INCOMPATIBILITY, +remove '!' and add '?' as required. *** ML *** diff -r 1bf7b186542e -r 6d5213bd9709 src/Doc/Isar_Ref/Spec.thy --- a/src/Doc/Isar_Ref/Spec.thy Mon Nov 09 15:48:17 2015 +0100 +++ b/src/Doc/Isar_Ref/Spec.thy Mon Nov 09 21:04:49 2015 +0100 @@ -462,44 +462,41 @@ subsection \Locale expressions \label{sec:locale-expr}\ text \ - A \<^emph>\locale expression\ denotes a context composed of instances - of existing locales. The context consists of the declaration - elements from the locale instances. Redundant locale instances are - omitted according to roundup. + A \<^emph>\locale expression\ denotes a context composed of instances of existing + locales. The context consists of the declaration elements from the locale + instances. Redundant locale instances are omitted according to roundup. @{rail \ @{syntax_def locale_expr}: (instance + '+') @{syntax for_fixes} ; instance: (qualifier ':')? @{syntax nameref} (pos_insts | named_insts) ; - qualifier: @{syntax name} ('?' | '!')? + qualifier: @{syntax name} ('?')? ; pos_insts: ('_' | @{syntax term})* ; named_insts: @'where' (@{syntax name} '=' @{syntax term} + @'and') \} - A locale instance consists of a reference to a locale and either - positional or named parameter instantiations. Identical - instantiations (that is, those that instantiate a parameter by itself) - may be omitted. The notation `\_\' enables to omit the - instantiation for a parameter inside a positional instantiation. + A locale instance consists of a reference to a locale and either positional + or named parameter instantiations. Identical instantiations (that is, those + that instantiate a parameter by itself) may be omitted. The notation ``\_\'' + enables to omit the instantiation for a parameter inside a positional + instantiation. - Terms in instantiations are from the context the locale expressions - is declared in. Local names may be added to this context with the - optional @{keyword "for"} clause. This is useful for shadowing names - bound in outer contexts, and for declaring syntax. In addition, - syntax declarations from one instance are effective when parsing - subsequent instances of the same expression. + Terms in instantiations are from the context the locale expressions is + declared in. Local names may be added to this context with the optional + @{keyword "for"} clause. This is useful for shadowing names bound in outer + contexts, and for declaring syntax. In addition, syntax declarations from + one instance are effective when parsing subsequent instances of the same + expression. - Instances have an optional qualifier which applies to names in - declarations. Names include local definitions and theorem names. - If present, the qualifier itself is either optional - (``\<^verbatim>\?\''), which means that it may be omitted on input of the - qualified name, or mandatory (``\<^verbatim>\!\''). If neither - ``\<^verbatim>\?\'' nor ``\<^verbatim>\!\'' are present the default - is used, which is ``mandatory''. Qualifiers play no role - in determining whether one locale instance subsumes another. + Instances have an optional qualifier which applies to names in declarations. + Names include local definitions and theorem names. If present, the qualifier + itself is either mandatory (default) or non-mandatory (when followed by + ``\<^verbatim>\?\''). Non-mandatory means that the qualifier may be omitted on input. + Qualifiers only affect name spaces; they play no role in determining whether + one locale instance subsumes another. \ diff -r 1bf7b186542e -r 6d5213bd9709 src/HOL/Statespace/state_space.ML --- a/src/HOL/Statespace/state_space.ML Mon Nov 09 15:48:17 2015 +0100 +++ b/src/HOL/Statespace/state_space.ML Mon Nov 09 21:04:49 2015 +0100 @@ -642,7 +642,7 @@ val renames = Scan.optional (@{keyword "["} |-- Parse.!!! (Parse.list1 rename --| @{keyword "]"})) []; val parent = - Parse_Spec.locale_prefix false -- + Parse_Spec.locale_prefix -- ((type_insts -- Parse.xname) || (Parse.xname >> pair [])) -- renames >> (fn ((prefix, (insts, name)), renames) => (prefix, (insts, name, renames))); diff -r 1bf7b186542e -r 6d5213bd9709 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Mon Nov 09 15:48:17 2015 +0100 +++ b/src/Pure/Isar/isar_syn.ML Mon Nov 09 21:04:49 2015 +0100 @@ -384,7 +384,7 @@ (* locales *) val locale_val = - Parse_Spec.locale_expression true -- + Parse_Spec.locale_expression -- Scan.optional (@{keyword "+"} |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] || Scan.repeat1 Parse_Spec.context_element >> pair ([], []); @@ -403,7 +403,7 @@ Toplevel.begin_local_theory true (Experiment.experiment_cmd elems #> snd))); val interpretation_args = - Parse.!!! (Parse_Spec.locale_expression true) -- + Parse.!!! Parse_Spec.locale_expression -- Scan.optional (@{keyword "rewrites"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []; @@ -817,7 +817,7 @@ val _ = Outer_Syntax.command @{command_keyword print_dependencies} "print dependencies of locale expression" - (Parse.opt_bang -- Parse_Spec.locale_expression true >> (fn (b, expr) => + (Parse.opt_bang -- Parse_Spec.locale_expression >> (fn (b, expr) => Toplevel.keep (fn state => Expression.print_dependencies (Toplevel.context_of state) b expr))); val _ = diff -r 1bf7b186542e -r 6d5213bd9709 src/Pure/Isar/parse_spec.ML --- a/src/Pure/Isar/parse_spec.ML Mon Nov 09 15:48:17 2015 +0100 +++ b/src/Pure/Isar/parse_spec.ML Mon Nov 09 21:04:49 2015 +0100 @@ -19,9 +19,9 @@ val locale_fixes: (binding * string option * mixfix) list parser val locale_insts: (string option list * (Attrib.binding * string) list) parser val class_expression: string list parser - val locale_prefix: bool -> (string * bool) parser + val locale_prefix: (string * bool) parser val locale_keyword: string parser - val locale_expression: bool -> Expression.expression parser + val locale_expression: Expression.expression parser val context_element: Element.context parser val statement: (Attrib.binding * (string * string list) list) list parser val if_statement: (Attrib.binding * (string * string list) list) list parser @@ -105,11 +105,9 @@ in -fun locale_prefix mandatory = +val locale_prefix = Scan.optional - (Parse.name -- - (Parse.$$$ "!" >> K true || Parse.$$$ "?" >> K false || Scan.succeed mandatory) --| - Parse.$$$ ":") + (Parse.name -- (Scan.option (Parse.$$$ "?") >> is_none) --| Parse.$$$ ":") ("", false); val locale_keyword = @@ -118,10 +116,11 @@ val class_expression = plus1_unless locale_keyword Parse.class; -fun locale_expression mandatory = +val locale_expression = let val expr2 = Parse.position Parse.xname; - val expr1 = locale_prefix mandatory -- expr2 -- + val expr1 = + locale_prefix -- expr2 -- Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i))); val expr0 = plus1_unless locale_keyword expr1; in expr0 -- Scan.optional (Parse.$$$ "for" |-- Parse.!!! locale_fixes) [] end; diff -r 1bf7b186542e -r 6d5213bd9709 src/Tools/permanent_interpretation.ML --- a/src/Tools/permanent_interpretation.ML Mon Nov 09 15:48:17 2015 +0100 +++ b/src/Tools/permanent_interpretation.ML Mon Nov 09 21:04:49 2015 +0100 @@ -99,7 +99,7 @@ val _ = Outer_Syntax.local_theory_to_proof @{command_keyword permanent_interpretation} "prove interpretation of locale expression into named theory" - (Parse.!!! (Parse_Spec.locale_expression true) -- + (Parse.!!! Parse_Spec.locale_expression -- Scan.optional (@{keyword "defining"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- ((Parse.binding -- Parse.opt_mixfix') --| @{keyword "="} -- Parse.term))) [] -- Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []