1.1 --- a/src/HOL/Statespace/StateSpaceEx.thy	Wed Oct 10 15:17:40 2012 +0200
     1.2 +++ b/src/HOL/Statespace/StateSpaceEx.thy	Wed Oct 10 15:21:26 2012 +0200
     1.3 @@ -84,7 +84,7 @@
     1.4  later use and is automatically propagated to all its interpretations.
     1.5  Here is another example: *}
     1.6  
     1.7 -statespace 'a varsX = vars [n=N, b=B] + vars + x::'a
     1.8 +statespace 'a varsX = NB: vars [n=N, b=B] + vars + x::'a
     1.9  
    1.10  text {* \noindent The state space @{text "varsX"} imports two copies
    1.11  of the state space @{text "vars"}, where one has the variables renamed
    1.12 @@ -179,7 +179,7 @@
    1.13  qed
    1.14  
    1.15  
    1.16 -statespace 'a dup = 'a foo [f=F, a=A] + 'a foo +
    1.17 +statespace 'a dup = FA: 'a foo [f=F, a=A] + 'a foo +
    1.18    x::int
    1.19  
    1.20  lemma (in dup)

     2.1 --- a/src/HOL/Statespace/state_space.ML	Wed Oct 10 15:17:40 2012 +0200
     2.2 +++ b/src/HOL/Statespace/state_space.ML	Wed Oct 10 15:21:26 2012 +0200
     2.3 @@ -21,18 +21,18 @@
     2.4    val define_statespace :
     2.5       string list ->
     2.6       string ->
     2.7 -     (string list * bstring * (string * string) list) list ->
     2.8 +     ((string * bool) * (string list * bstring * (string * string) list)) list ->
     2.9       (string * string) list -> theory -> theory
    2.10    val define_statespace_i :
    2.11       string option ->
    2.12       string list ->
    2.13       string ->
    2.14 -     (typ list * bstring * (string * string) list) list ->
    2.15 +     ((string * bool) * (typ list * bstring * (string * string) list)) list ->
    2.16       (string * typ) list -> theory -> theory
    2.17  
    2.18    val statespace_decl :
    2.19       ((string list * bstring) *
    2.20 -       ((string list * xstring * (bstring * bstring) list) list *
    2.21 +       (((string * bool) * (string list * xstring * (bstring * bstring) list)) list *
    2.22          (bstring * string) list)) parser
    2.23  
    2.24  
    2.25 @@ -355,7 +355,7 @@
    2.26      val inst = map fst args ~~ Ts;
    2.27      val subst = Term.map_type_tfree (the o AList.lookup (op =) inst o fst);
    2.28      val parent_comps =
    2.29 -      maps (fn (Ts',n,rs) => parent_components thy (map subst Ts',n,rs)) parents;
    2.30 +      maps (fn (Ts',n,rs) => parent_components thy (map subst Ts', n, rs)) parents;
    2.31      val all_comps = rename renaming (parent_comps @ map (apsnd subst) components);
    2.32    in all_comps end;
    2.33  
    2.34 @@ -369,8 +369,8 @@
    2.35      val components' = map (fn (n,T) => (n,(T,full_name))) components;
    2.36      val all_comps' = map (fn (n,T) => (n,(T,full_name))) all_comps;
    2.37  
    2.38 -    fun parent_expr (_,n,rs) = (suffix namespaceN n,((n,false),Expression.Positional rs));
    2.39 -        (* FIXME: a more specific renaming-prefix (including parameter names) may be nicer *)
    2.40 +    fun parent_expr (prefix, (_, n, rs)) =
    2.41 +      (suffix namespaceN n, (prefix, Expression.Positional rs));
    2.42      val parents_expr = map parent_expr parents;
    2.43      fun distinct_types Ts =
    2.44        let val tab = fold (fn T => fn tab => Typtab.update (T,()) tab) Ts Typtab.empty;
    2.45 @@ -386,14 +386,14 @@
    2.46      fun projectT T = valueT --> T;
    2.47      fun injectT T = T --> valueT;
    2.48      val locinsts = map (fn T => (project_injectL,
    2.49 -                    (("",false),Expression.Positional
    2.50 +                    ((encode_type T,false),Expression.Positional
    2.51                               [SOME (Free (project_name T,projectT T)),
    2.52                                SOME (Free ((inject_name T,injectT T)))]))) Ts;
    2.53      val locs = maps (fn T => [(Binding.name (project_name T),NONE,NoSyn),
    2.54                                       (Binding.name (inject_name T),NONE,NoSyn)]) Ts;
    2.55      val constrains = maps (fn T => [(project_name T,projectT T),(inject_name T,injectT T)]) Ts;
    2.56  
    2.57 -    fun interprete_parent_valuetypes (Ts, pname, _) thy =
    2.58 +    fun interprete_parent_valuetypes (prefix, (Ts, pname, _)) thy =
    2.59        let
    2.60          val {args,types,...} =
    2.61               the (Symtab.lookup (StateSpaceData.get (Context.Theory thy)) pname);
    2.62 @@ -402,15 +402,15 @@
    2.63          val pars = maps ((fn T => [project_name T,inject_name T]) o subst) types;
    2.64  
    2.65          val expr = ([(suffix valuetypesN name,
    2.66 -                     (("",false),Expression.Positional (map SOME pars)))],[]);
    2.67 +                     (prefix, Expression.Positional (map SOME pars)))],[]);
    2.68        in
    2.69          prove_interpretation_in (ALLGOALS o solve_tac o Assumption.all_prems_of)
    2.70            (suffix valuetypesN name, expr) thy
    2.71        end;
    2.72  
    2.73 -    fun interprete_parent (_, pname, rs) =
    2.74 +    fun interprete_parent (prefix, (_, pname, rs)) =
    2.75        let
    2.76 -        val expr = ([(pname, (("",false), Expression.Positional rs))],[])
    2.77 +        val expr = ([(pname, (prefix, Expression.Positional rs))],[])
    2.78        in prove_interpretation_in
    2.79             (fn ctxt => Locale.intro_locales_tac false ctxt [])
    2.80             (full_name, expr) end;
    2.81 @@ -449,7 +449,7 @@
    2.82       |> namespace_definition
    2.83             (suffix namespaceN name) nameT (parents_expr,[])
    2.84             (map fst parent_comps) (map fst components)
    2.85 -     |> Context.theory_map (add_statespace full_name args parents components [])
    2.86 +     |> Context.theory_map (add_statespace full_name args (map snd parents) components [])
    2.87       |> add_locale (suffix valuetypesN name) (locinsts,locs) []
    2.88       |> Proof_Context.theory_of
    2.89       |> fold interprete_parent_valuetypes parents
    2.90 @@ -495,8 +495,13 @@
    2.91  
    2.92      val ctxt = Proof_Context.init_global thy;
    2.93  
    2.94 -    fun add_parent (Ts,pname,rs) env =
    2.95 +    fun add_parent (prefix, (Ts, pname, rs)) env =
    2.96        let
    2.97 +        val prefix' =
    2.98 +          (case prefix of
    2.99 +            ("", mandatory) => (pname, mandatory)
   2.100 +          | _ => prefix);
   2.101 +
   2.102          val full_pname = Sign.full_bname thy pname;
   2.103          val {args,components,...} =
   2.104                (case get_statespace (Context.Theory thy) full_pname of
   2.105 @@ -526,8 +531,9 @@
   2.106  
   2.107          val rs' = map (AList.lookup (op =) rs o fst) components;
   2.108          val errs =err_insts @ err_dup_renamings @ err_rename_unknowns
   2.109 -      in if null errs then ((Ts',full_pname,rs'),env')
   2.110 -         else error (cat_lines (errs @ ["in parent statespace " ^ quote pname]))
   2.111 +      in
   2.112 +        if null errs then ((prefix', (Ts', full_pname, rs')), env')
   2.113 +        else error (cat_lines (errs @ ["in parent statespace " ^ quote pname]))
   2.114        end;
   2.115  
   2.116      val (parents',env) = fold_map add_parent parents [];
   2.117 @@ -562,7 +568,7 @@
   2.118      fun fst_eq ((x:string,_),(y,_)) = x = y;
   2.119      fun snd_eq ((_,t:typ),(_,u)) = t = u;
   2.120  
   2.121 -    val raw_parent_comps = maps (parent_components thy) parents';
   2.122 +    val raw_parent_comps = maps (parent_components thy o snd) parents';
   2.123      fun check_type (n,T) =
   2.124            (case distinct (snd_eq) (filter (curry fst_eq (n,T)) raw_parent_comps) of
   2.125               []  => []
   2.126 @@ -687,8 +693,9 @@
   2.127  val renames = Scan.optional (@{keyword "["} |-- Parse.!!! (Parse.list1 rename --| @{keyword "]"})) [];
   2.128  
   2.129  val parent =
   2.130 +  Parse_Spec.locale_prefix false --
   2.131    ((type_insts -- Parse.xname) || (Parse.xname >> pair [])) -- renames
   2.132 -    >> (fn ((insts, name), renames) => (insts,name, renames));
   2.133 +    >> (fn ((prefix, (insts, name)), renames) => (prefix, (insts, name, renames)));
   2.134  
   2.135  in
   2.136  

     3.1 --- a/src/Pure/Isar/parse_spec.ML	Wed Oct 10 15:17:40 2012 +0200
     3.2 +++ b/src/Pure/Isar/parse_spec.ML	Wed Oct 10 15:21:26 2012 +0200
     3.3 @@ -24,8 +24,9 @@
     3.4    val locale_fixes: (binding * string option * mixfix) list parser
     3.5    val locale_insts: (string option list * (Attrib.binding * string) list) parser
     3.6    val class_expression: string list parser
     3.7 +  val locale_prefix: bool -> (string * bool) parser
     3.8 +  val locale_keyword: string parser
     3.9    val locale_expression: bool -> Expression.expression parser
    3.10 -  val locale_keyword: string parser
    3.11    val context_element: Element.context parser
    3.12    val statement: (Attrib.binding * (string * string list) list) list parser
    3.13    val general_statement: (Element.context list * Element.statement) parser
    3.14 @@ -113,17 +114,19 @@
    3.15  fun plus1_unless test scan =
    3.16    scan ::: Scan.repeat (Parse.$$$ "+" |-- Scan.unless test (Parse.!!! scan));
    3.17  
    3.18 -fun prefix mandatory =
    3.19 -  Parse.name --
    3.20 -    (Parse.$$$ "!" >> K true || Parse.$$$ "?" >> K false || Scan.succeed mandatory) --|
    3.21 -    Parse.$$$ ":";
    3.22 -
    3.23  val instance = Parse.where_ |--
    3.24    Parse.and_list1 (Parse.name -- (Parse.$$$ "=" |-- Parse.term)) >> Expression.Named ||
    3.25    Scan.repeat1 (Parse.maybe Parse.term) >> Expression.Positional;
    3.26  
    3.27  in
    3.28  
    3.29 +fun locale_prefix mandatory =
    3.30 +  Scan.optional
    3.31 +    (Parse.name --
    3.32 +      (Parse.$$$ "!" >> K true || Parse.$$$ "?" >> K false || Scan.succeed mandatory) --|
    3.33 +      Parse.$$$ ":")
    3.34 +    ("", false);
    3.35 +
    3.36  val locale_keyword =
    3.37    Parse.$$$ "fixes" || Parse.$$$ "constrains" || Parse.$$$ "assumes" ||
    3.38    Parse.$$$ "defines" || Parse.$$$ "notes";
    3.39 @@ -133,7 +136,7 @@
    3.40  fun locale_expression mandatory =
    3.41    let
    3.42      val expr2 = Parse.position Parse.xname;
    3.43 -    val expr1 = Scan.optional (prefix mandatory) ("", false) -- expr2 --
    3.44 +    val expr1 = locale_prefix mandatory -- expr2 --
    3.45        Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)));
    3.46      val expr0 = plus1_unless locale_keyword expr1;
    3.47    in expr0 -- Scan.optional (Parse.$$$ "for" |-- Parse.!!! locale_fixes) [] end;