# HG changeset patch # User wenzelm # Date 1349875286 -7200 # Node ID acafcac41690e0ff15a149d3cf4f825727b9671d # Parent a344f1a2121184b3886635d5c67c1b6fc8c90a49 more explicit namespace prefix for 'statespace' -- duplicate facts; diff -r a344f1a21211 -r acafcac41690 src/HOL/Statespace/StateSpaceEx.thy --- a/src/HOL/Statespace/StateSpaceEx.thy Wed Oct 10 15:17:40 2012 +0200 +++ b/src/HOL/Statespace/StateSpaceEx.thy Wed Oct 10 15:21:26 2012 +0200 @@ -84,7 +84,7 @@ later use and is automatically propagated to all its interpretations. Here is another example: *} -statespace 'a varsX = vars [n=N, b=B] + vars + x::'a +statespace 'a varsX = NB: vars [n=N, b=B] + vars + x::'a text {* \noindent The state space @{text "varsX"} imports two copies of the state space @{text "vars"}, where one has the variables renamed @@ -179,7 +179,7 @@ qed -statespace 'a dup = 'a foo [f=F, a=A] + 'a foo + +statespace 'a dup = FA: 'a foo [f=F, a=A] + 'a foo + x::int lemma (in dup) diff -r a344f1a21211 -r acafcac41690 src/HOL/Statespace/state_space.ML --- a/src/HOL/Statespace/state_space.ML Wed Oct 10 15:17:40 2012 +0200 +++ b/src/HOL/Statespace/state_space.ML Wed Oct 10 15:21:26 2012 +0200 @@ -21,18 +21,18 @@ val define_statespace : string list -> string -> - (string list * bstring * (string * string) list) list -> + ((string * bool) * (string list * bstring * (string * string) list)) list -> (string * string) list -> theory -> theory val define_statespace_i : string option -> string list -> string -> - (typ list * bstring * (string * string) list) list -> + ((string * bool) * (typ list * bstring * (string * string) list)) list -> (string * typ) list -> theory -> theory val statespace_decl : ((string list * bstring) * - ((string list * xstring * (bstring * bstring) list) list * + (((string * bool) * (string list * xstring * (bstring * bstring) list)) list * (bstring * string) list)) parser @@ -355,7 +355,7 @@ val inst = map fst args ~~ Ts; val subst = Term.map_type_tfree (the o AList.lookup (op =) inst o fst); val parent_comps = - maps (fn (Ts',n,rs) => parent_components thy (map subst Ts',n,rs)) parents; + maps (fn (Ts',n,rs) => parent_components thy (map subst Ts', n, rs)) parents; val all_comps = rename renaming (parent_comps @ map (apsnd subst) components); in all_comps end; @@ -369,8 +369,8 @@ val components' = map (fn (n,T) => (n,(T,full_name))) components; val all_comps' = map (fn (n,T) => (n,(T,full_name))) all_comps; - fun parent_expr (_,n,rs) = (suffix namespaceN n,((n,false),Expression.Positional rs)); - (* FIXME: a more specific renaming-prefix (including parameter names) may be nicer *) + fun parent_expr (prefix, (_, n, rs)) = + (suffix namespaceN n, (prefix, Expression.Positional rs)); val parents_expr = map parent_expr parents; fun distinct_types Ts = let val tab = fold (fn T => fn tab => Typtab.update (T,()) tab) Ts Typtab.empty; @@ -386,14 +386,14 @@ fun projectT T = valueT --> T; fun injectT T = T --> valueT; val locinsts = map (fn T => (project_injectL, - (("",false),Expression.Positional + ((encode_type T,false),Expression.Positional [SOME (Free (project_name T,projectT T)), SOME (Free ((inject_name T,injectT T)))]))) Ts; val locs = maps (fn T => [(Binding.name (project_name T),NONE,NoSyn), (Binding.name (inject_name T),NONE,NoSyn)]) Ts; val constrains = maps (fn T => [(project_name T,projectT T),(inject_name T,injectT T)]) Ts; - fun interprete_parent_valuetypes (Ts, pname, _) thy = + fun interprete_parent_valuetypes (prefix, (Ts, pname, _)) thy = let val {args,types,...} = the (Symtab.lookup (StateSpaceData.get (Context.Theory thy)) pname); @@ -402,15 +402,15 @@ val pars = maps ((fn T => [project_name T,inject_name T]) o subst) types; val expr = ([(suffix valuetypesN name, - (("",false),Expression.Positional (map SOME pars)))],[]); + (prefix, Expression.Positional (map SOME pars)))],[]); in prove_interpretation_in (ALLGOALS o solve_tac o Assumption.all_prems_of) (suffix valuetypesN name, expr) thy end; - fun interprete_parent (_, pname, rs) = + fun interprete_parent (prefix, (_, pname, rs)) = let - val expr = ([(pname, (("",false), Expression.Positional rs))],[]) + val expr = ([(pname, (prefix, Expression.Positional rs))],[]) in prove_interpretation_in (fn ctxt => Locale.intro_locales_tac false ctxt []) (full_name, expr) end; @@ -449,7 +449,7 @@ |> namespace_definition (suffix namespaceN name) nameT (parents_expr,[]) (map fst parent_comps) (map fst components) - |> Context.theory_map (add_statespace full_name args parents components []) + |> Context.theory_map (add_statespace full_name args (map snd parents) components []) |> add_locale (suffix valuetypesN name) (locinsts,locs) [] |> Proof_Context.theory_of |> fold interprete_parent_valuetypes parents @@ -495,8 +495,13 @@ val ctxt = Proof_Context.init_global thy; - fun add_parent (Ts,pname,rs) env = + fun add_parent (prefix, (Ts, pname, rs)) env = let + val prefix' = + (case prefix of + ("", mandatory) => (pname, mandatory) + | _ => prefix); + val full_pname = Sign.full_bname thy pname; val {args,components,...} = (case get_statespace (Context.Theory thy) full_pname of @@ -526,8 +531,9 @@ val rs' = map (AList.lookup (op =) rs o fst) components; val errs =err_insts @ err_dup_renamings @ err_rename_unknowns - in if null errs then ((Ts',full_pname,rs'),env') - else error (cat_lines (errs @ ["in parent statespace " ^ quote pname])) + in + if null errs then ((prefix', (Ts', full_pname, rs')), env') + else error (cat_lines (errs @ ["in parent statespace " ^ quote pname])) end; val (parents',env) = fold_map add_parent parents []; @@ -562,7 +568,7 @@ fun fst_eq ((x:string,_),(y,_)) = x = y; fun snd_eq ((_,t:typ),(_,u)) = t = u; - val raw_parent_comps = maps (parent_components thy) parents'; + val raw_parent_comps = maps (parent_components thy o snd) parents'; fun check_type (n,T) = (case distinct (snd_eq) (filter (curry fst_eq (n,T)) raw_parent_comps) of [] => [] @@ -687,8 +693,9 @@ val renames = Scan.optional (@{keyword "["} |-- Parse.!!! (Parse.list1 rename --| @{keyword "]"})) []; val parent = + Parse_Spec.locale_prefix false -- ((type_insts -- Parse.xname) || (Parse.xname >> pair [])) -- renames - >> (fn ((insts, name), renames) => (insts,name, renames)); + >> (fn ((prefix, (insts, name)), renames) => (prefix, (insts, name, renames))); in diff -r a344f1a21211 -r acafcac41690 src/Pure/Isar/parse_spec.ML --- a/src/Pure/Isar/parse_spec.ML Wed Oct 10 15:17:40 2012 +0200 +++ b/src/Pure/Isar/parse_spec.ML Wed Oct 10 15:21:26 2012 +0200 @@ -24,8 +24,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_keyword: string parser val locale_expression: bool -> Expression.expression parser - val locale_keyword: string parser val context_element: Element.context parser val statement: (Attrib.binding * (string * string list) list) list parser val general_statement: (Element.context list * Element.statement) parser @@ -113,17 +114,19 @@ fun plus1_unless test scan = scan ::: Scan.repeat (Parse.$$$ "+" |-- Scan.unless test (Parse.!!! scan)); -fun prefix mandatory = - Parse.name -- - (Parse.$$$ "!" >> K true || Parse.$$$ "?" >> K false || Scan.succeed mandatory) --| - Parse.$$$ ":"; - val instance = Parse.where_ |-- Parse.and_list1 (Parse.name -- (Parse.$$$ "=" |-- Parse.term)) >> Expression.Named || Scan.repeat1 (Parse.maybe Parse.term) >> Expression.Positional; in +fun locale_prefix mandatory = + Scan.optional + (Parse.name -- + (Parse.$$$ "!" >> K true || Parse.$$$ "?" >> K false || Scan.succeed mandatory) --| + Parse.$$$ ":") + ("", false); + val locale_keyword = Parse.$$$ "fixes" || Parse.$$$ "constrains" || Parse.$$$ "assumes" || Parse.$$$ "defines" || Parse.$$$ "notes"; @@ -133,7 +136,7 @@ fun locale_expression mandatory = let val expr2 = Parse.position Parse.xname; - val expr1 = Scan.optional (prefix mandatory) ("", false) -- expr2 -- + val expr1 = locale_prefix mandatory -- 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;