src/Pure/Isar/locale.ML
author ballarin
Thu Mar 24 17:03:37 2005 +0100 (2005-03-24 ago)
changeset 15624 484178635bd8
parent 15623 8b40f741597c
child 15696 1da4ce092c0b
permissions -rw-r--r--
Further work on interpretation commands. New command `interpret' for
interpretation in proof contexts.
     1 (*  Title:      Pure/Isar/locale.ML
     2     ID:         $Id$
     3     Author:     Clemens Ballarin, TU Muenchen; Markus Wenzel, LMU/TU Muenchen
     4 
     5 Locales -- Isar proof contexts as meta-level predicates, with local
     6 syntax and implicit structures.
     7 
     8 Draws some basic ideas from Florian Kammueller's original version of
     9 locales, but uses the richer infrastructure of Isar instead of the raw
    10 meta-logic.  Furthermore, we provide structured import of contexts
    11 (with merge and rename operations), as well as type-inference of the
    12 signature parts, and predicate definitions of the specification text.
    13 
    14 See also:
    15 
    16 [1] Clemens Ballarin. Locales and Locale Expressions in Isabelle/Isar.
    17     In Stefano Berardi et al., Types for Proofs and Programs: International
    18     Workshop, TYPES 2003, Torino, Italy, LNCS 3085, pages 34-50, 2004.
    19 *)
    20 
    21 signature LOCALE =
    22 sig
    23   type context
    24   type multi_attribute
    25 
    26   (* Constructors for elem, expr and elem_expr are
    27      currently only used for inputting locales (outer_parse.ML). *)
    28   datatype ('typ, 'term, 'fact, 'att) elem =
    29     Fixes of (string * 'typ option * mixfix option) list |
    30     Assumes of ((string * 'att list) * ('term * ('term list * 'term list)) list) list |
    31     Defines of ((string * 'att list) * ('term * 'term list)) list |
    32     Notes of ((string * 'att list) * ('fact * 'att list) list) list
    33   datatype expr =
    34     Locale of string |
    35     Rename of expr * string option list |
    36     Merge of expr list
    37   val empty: expr
    38   datatype 'a elem_expr = Elem of 'a | Expr of expr
    39 
    40   (* Abstract interface to locales *)
    41   type 'att element
    42   type 'att element_i
    43   type locale
    44   val intern: Sign.sg -> xstring -> string
    45   val cond_extern: Sign.sg -> string -> xstring
    46   val the_locale: theory -> string -> locale
    47   val map_attrib_element: ('att -> multi_attribute) -> 'att element ->
    48     multi_attribute element
    49   val map_attrib_element_i: ('att -> multi_attribute) -> 'att element_i ->
    50     multi_attribute element_i
    51   val map_attrib_elem_or_expr: ('att -> multi_attribute) ->
    52     'att element elem_expr -> multi_attribute element elem_expr
    53   val map_attrib_elem_or_expr_i: ('att -> multi_attribute) ->
    54     'att element_i elem_expr -> multi_attribute element_i elem_expr
    55 
    56   (* Processing of locale statements *)
    57   val read_context_statement: xstring option ->
    58     multi_attribute element elem_expr list ->
    59     (string * (string list * string list)) list list -> context ->
    60     string option * (cterm list * cterm list) * context * context * 
    61       (term * (term list * term list)) list list
    62   val cert_context_statement: string option ->
    63     multi_attribute element_i elem_expr list ->
    64     (term * (term list * term list)) list list -> context ->
    65     string option * (cterm list * cterm list) * context * context *
    66       (term * (term list * term list)) list list
    67 
    68   (* Diagnostic functions *)
    69   val print_locales: theory -> unit
    70   val print_locale: theory -> expr -> multi_attribute element list -> unit
    71   val print_global_registrations: string -> theory -> unit
    72   val print_local_registrations: string -> context -> unit
    73 
    74   val add_locale: bool -> bstring -> expr -> multi_attribute element list -> theory -> theory
    75   val add_locale_i: bool -> bstring -> expr -> multi_attribute element_i list
    76     -> theory -> theory
    77   val smart_note_thmss: string -> (string * 'a) option ->
    78     ((bstring * theory attribute list) * (thm list * theory attribute list) list) list ->
    79     theory -> theory * (bstring * thm list) list
    80   val note_thmss: string -> xstring ->
    81     ((bstring * multi_attribute list) * (thmref * multi_attribute list) list) list ->
    82     theory -> theory * (bstring * thm list) list
    83   val note_thmss_i: string -> string ->
    84     ((bstring * multi_attribute list) * (thm list * multi_attribute list) list) list ->
    85     theory -> theory * (bstring * thm list) list
    86   val add_thmss: string -> ((string * thm list) * multi_attribute list) list ->
    87     theory * context -> (theory * context) * (string * thm list) list
    88 
    89   (* Locale interpretation *)
    90   val instantiate: string -> string * context attribute list
    91     -> thm list option -> context -> context
    92   val prep_global_registration:
    93     string * theory attribute list -> expr -> string option list -> theory ->
    94     theory * ((string * term list) * term list) list * (theory -> theory)
    95   val prep_local_registration:
    96     string * context attribute list -> expr -> string option list -> context ->
    97     context * ((string * term list) * term list) list * (context -> context)
    98   val add_global_witness:
    99     string * term list -> thm -> theory -> theory
   100   val add_local_witness:
   101     string * term list -> thm -> context -> context
   102 
   103   (* Theory setup for locales *)
   104   val setup: (theory -> theory) list
   105 end;
   106 
   107 structure Locale: LOCALE =
   108 struct
   109 
   110 (** locale elements and expressions **)
   111 
   112 type context = ProofContext.context;
   113 
   114 (* Locales store theory attributes (for activation in theories)
   115    and context attributes (for activation in contexts) *)
   116 type multi_attribute = theory attribute * context attribute;
   117 
   118 datatype ('typ, 'term, 'fact, 'att) elem =
   119   Fixes of (string * 'typ option * mixfix option) list |
   120   Assumes of ((string * 'att list) * ('term * ('term list * 'term list)) list) list |
   121   Defines of ((string * 'att list) * ('term * 'term list)) list |
   122   Notes of ((string * 'att list) * ('fact * 'att list) list) list;
   123 
   124 datatype expr =
   125   Locale of string |
   126   Rename of expr * string option list |
   127   Merge of expr list;
   128 
   129 val empty = Merge [];
   130 
   131 datatype 'a elem_expr =
   132   Elem of 'a | Expr of expr;
   133 
   134 type 'att element = (string, string, thmref, 'att) elem;
   135 type 'att element_i = (typ, term, thm list, 'att) elem;
   136 
   137 type locale =
   138  {predicate: cterm list * thm list,
   139     (* CB: For old-style locales with "(open)" this entry is ([], []).
   140        For new-style locales, which declare predicates, if the locale declares
   141        no predicates, this is also ([], []).
   142        If the locale declares predicates, the record field is
   143        ([statement], axioms), where statement is the locale predicate applied
   144        to the (assumed) locale parameters.  Axioms contains the projections
   145        from the locale predicate to the normalised assumptions of the locale
   146        (cf. [1], normalisation of locale expressions.)
   147     *)
   148   import: expr,                                       (*dynamic import*)
   149   elems: (multi_attribute element_i * stamp) list,    (*static content*)
   150   params: (string * typ option) list * string list}   (*all/local params*)
   151 
   152 
   153 (** theory data **)
   154 
   155 structure Termlisttab = TableFun(type key = term list
   156   val ord = Library.list_ord Term.term_ord);
   157 
   158 structure GlobalLocalesArgs =
   159 struct
   160   val name = "Isar/locales";
   161   type T = NameSpace.T * locale Symtab.table *
   162       ((string * theory attribute list) * thm list) Termlisttab.table
   163         Symtab.table;
   164     (* 1st entry: locale namespace,
   165        2nd entry: locales of the theory,
   166        3rd entry: registrations: theorems instantiating locale assumptions,
   167          with prefix and attributes, indexed by locale name and parameter
   168          instantiation *)
   169 
   170   val empty = (NameSpace.empty, Symtab.empty, Symtab.empty);
   171   val copy = I;
   172   val prep_ext = I;
   173 
   174   fun join_locs ({predicate, import, elems, params}: locale,
   175       {elems = elems', ...}: locale) =
   176     SOME {predicate = predicate, import = import,
   177       elems = gen_merge_lists eq_snd elems elems',
   178       params = params};
   179   (* joining of registrations: prefix and attributes of left theory,
   180      thmsss are equal *)
   181   fun join_regs (reg, _) = SOME reg;
   182   fun merge ((space1, locs1, regs1), (space2, locs2, regs2)) =
   183     (NameSpace.merge (space1, space2), Symtab.join join_locs (locs1, locs2),
   184      Symtab.join (SOME o Termlisttab.join join_regs) (regs1, regs2));
   185 
   186   fun print _ (space, locs, _) =
   187     Pretty.strs ("locales:" :: map (NameSpace.cond_extern space o #1) (Symtab.dest locs))
   188     |> Pretty.writeln;
   189 end;
   190 
   191 structure GlobalLocalesData = TheoryDataFun(GlobalLocalesArgs);
   192 
   193 (** context data **)
   194 
   195 structure LocalLocalesArgs =
   196 struct
   197   val name = "Isar/locales";
   198   type T = ((string * context attribute list) * thm list) Termlisttab.table
   199            Symtab.table;
   200     (* registrations: theorems instantiating locale assumptions,
   201          with prefix and attributes, indexed by locale name and parameter
   202          instantiation *)
   203   fun init _ = Symtab.empty;
   204   fun print _ _ = ();
   205 end;
   206 
   207 structure LocalLocalesData = ProofDataFun(LocalLocalesArgs);
   208 
   209 
   210 (* access locales *)
   211 
   212 val print_locales = GlobalLocalesData.print;
   213 
   214 val intern = NameSpace.intern o #1 o GlobalLocalesData.get_sg;
   215 val cond_extern = NameSpace.cond_extern o #1 o GlobalLocalesData.get_sg;
   216 
   217 fun declare_locale name =
   218   GlobalLocalesData.map (fn (space, locs, regs) =>
   219     (NameSpace.extend (space, [name]), locs, regs));
   220 
   221 fun put_locale name loc =
   222   GlobalLocalesData.map (fn (space, locs, regs) =>
   223     (space, Symtab.update ((name, loc), locs), regs));
   224 
   225 fun get_locale thy name = Symtab.lookup (#2 (GlobalLocalesData.get thy), name);
   226 
   227 fun the_locale thy name =
   228   (case get_locale thy name of
   229     SOME loc => loc
   230   | NONE => error ("Unknown locale " ^ quote name));
   231 
   232 
   233 (* access registrations *)
   234 
   235 (* retrieve registration from theory or context *)
   236 
   237 fun gen_get_registration get thy_ctxt (name, ps) =
   238   case Symtab.lookup (get thy_ctxt, name) of
   239       NONE => NONE
   240     | SOME tab => Termlisttab.lookup (tab, ps);
   241 
   242 val get_global_registration =
   243      gen_get_registration (#3 o GlobalLocalesData.get);
   244 val get_local_registration =
   245      gen_get_registration LocalLocalesData.get;
   246 
   247 val test_global_registration = isSome oo get_global_registration;
   248 val test_local_registration = isSome oo get_local_registration;
   249 fun smart_test_registration ctxt id =
   250   let
   251     val thy = ProofContext.theory_of ctxt;
   252   in
   253     test_global_registration thy id orelse test_local_registration ctxt id
   254   end;
   255 
   256 
   257 (* add registration to theory or context, ignored if already present *)
   258 
   259 fun gen_put_registration map (name, ps) attn =
   260   map (fn regs =>
   261       let
   262         val tab = getOpt (Symtab.lookup (regs, name), Termlisttab.empty);
   263       in
   264         Symtab.update ((name, Termlisttab.update_new ((ps, (attn, [])), tab)),
   265           regs)
   266       end handle Termlisttab.DUP _ => regs);
   267 
   268 val put_global_registration =
   269      gen_put_registration (fn f =>
   270        GlobalLocalesData.map (fn (space, locs, regs) =>
   271          (space, locs, f regs)));
   272 val put_local_registration = gen_put_registration LocalLocalesData.map;
   273 
   274 fun smart_put_registration id attn ctxt =
   275   (* ignore registration if already present in theory *)
   276      let
   277        val thy = ProofContext.theory_of ctxt;
   278      in case get_global_registration thy id of
   279           NONE => put_local_registration id attn ctxt
   280         | SOME _ => ctxt
   281      end;
   282 
   283 
   284 (* add witness theorem to registration in theory or context,
   285    ignored if registration not present *)
   286 
   287 fun gen_add_witness map (name, ps) thm =
   288   map (fn regs =>
   289       let
   290         val tab = valOf (Symtab.lookup (regs, name));
   291         val (x, thms) = valOf (Termlisttab.lookup (tab, ps));
   292       in
   293         Symtab.update ((name, Termlisttab.update ((ps, (x, thm::thms)), tab)),
   294           regs)
   295       end handle Option => regs);
   296 
   297 val add_global_witness =
   298      gen_add_witness (fn f =>
   299        GlobalLocalesData.map (fn (space, locs, regs) =>
   300          (space, locs, f regs)));
   301 val add_local_witness = gen_add_witness LocalLocalesData.map;
   302 
   303 
   304 (* import hierarchy
   305    implementation could be more efficient, eg. by maintaining a database
   306    of dependencies *)
   307 
   308 fun imports thy (upper, lower) =
   309   let
   310     val sign = sign_of thy;
   311     fun imps (Locale name) low = (name = low) orelse
   312       (case get_locale thy name of
   313            NONE => false
   314          | SOME {import, ...} => imps import low)
   315       | imps (Rename (expr, _)) low = imps expr low
   316       | imps (Merge es) low = exists (fn e => imps e low) es;
   317   in
   318     imps (Locale (intern sign upper)) (intern sign lower)
   319   end;
   320 
   321 
   322 (* printing of registrations *)
   323 
   324 fun gen_print_registrations get_regs get_sign msg loc thy_ctxt =
   325   let
   326     val sg = get_sign thy_ctxt;
   327     val loc_int = intern sg loc;
   328     val regs = get_regs thy_ctxt;
   329     val prt_term = Pretty.quote o Sign.pretty_term sg;
   330     fun prt_inst (ts, ((prfx, _), thms)) =
   331       Pretty.block [Pretty.str prfx, Pretty.str ":", Pretty.brk 1,
   332         Pretty.list "(" ")" (map prt_term ts)];
   333     val loc_regs = Symtab.lookup (regs, loc_int);
   334   in
   335     (case loc_regs of
   336         NONE => Pretty.str ("No interpretations in " ^ msg ^ ".")
   337       | SOME r => Pretty.big_list ("Interpretations in " ^ msg ^ ":")
   338           (map prt_inst (Termlisttab.dest r)))
   339     |> Pretty.writeln
   340   end;
   341 
   342 val print_global_registrations =
   343      gen_print_registrations (#3 o GlobalLocalesData.get)
   344        Theory.sign_of "theory";
   345 val print_local_registrations' =
   346      gen_print_registrations LocalLocalesData.get
   347        ProofContext.sign_of "context";
   348 fun print_local_registrations loc ctxt =
   349   (print_global_registrations loc (ProofContext.theory_of ctxt);
   350    print_local_registrations' loc ctxt);
   351 
   352 
   353 (* diagnostics *)
   354 
   355 fun err_in_locale ctxt msg ids =
   356   let
   357     val sign = ProofContext.sign_of ctxt;
   358     fun prt_id (name, parms) =
   359       [Pretty.block (Pretty.breaks (map Pretty.str (cond_extern sign name :: parms)))];
   360     val prt_ids = List.concat (separate [Pretty.str " +", Pretty.brk 1] (map prt_id ids));
   361     val err_msg =
   362       if forall (equal "" o #1) ids then msg
   363       else msg ^ "\n" ^ Pretty.string_of (Pretty.block
   364         (Pretty.str "The error(s) above occurred in locale:" :: Pretty.brk 1 :: prt_ids));
   365   in raise ProofContext.CONTEXT (err_msg, ctxt) end;
   366 
   367 (* Version for identifiers with axioms *)
   368 
   369 fun err_in_locale' ctxt msg ids' = err_in_locale ctxt msg (map fst ids');
   370 
   371 
   372 (** primitives **)
   373 
   374 (* renaming *)
   375 
   376 fun rename ren x = getOpt (assoc_string (ren, x), x);
   377 
   378 fun rename_term ren (Free (x, T)) = Free (rename ren x, T)
   379   | rename_term ren (t $ u) = rename_term ren t $ rename_term ren u
   380   | rename_term ren (Abs (x, T, t)) = Abs (x, T, rename_term ren t)
   381   | rename_term _ a = a;
   382 
   383 fun rename_thm ren th =
   384   let
   385     val {sign, hyps, prop, maxidx, ...} = Thm.rep_thm th;
   386     val cert = Thm.cterm_of sign;
   387     val (xs, Ts) = Library.split_list (Library.foldl Term.add_frees ([], prop :: hyps));
   388     val xs' = map (rename ren) xs;
   389     fun cert_frees names = map (cert o Free) (names ~~ Ts);
   390     fun cert_vars names = map (cert o Var o apfst (rpair (maxidx + 1))) (names ~~ Ts);
   391   in
   392     if xs = xs' then th
   393     else
   394       th
   395       |> Drule.implies_intr_list (map cert hyps)
   396       |> Drule.forall_intr_list (cert_frees xs)
   397       |> Drule.forall_elim_list (cert_vars xs)
   398       |> Thm.instantiate ([], cert_vars xs ~~ cert_frees xs')
   399       |> (fn th' => Drule.implies_elim_list th' (map (Thm.assume o cert o rename_term ren) hyps))
   400   end;
   401 
   402 fun rename_elem ren (Fixes fixes) = Fixes (fixes |> map (fn (x, T, mx) =>
   403       let val x' = rename ren x in
   404         if x = x' then (x, T, mx)
   405         else (x', T, if mx = NONE then mx else SOME Syntax.NoSyn)    (*drop syntax*)
   406       end))
   407   | rename_elem ren (Assumes asms) = Assumes (map (apsnd (map (fn (t, (ps, qs)) =>
   408       (rename_term ren t, (map (rename_term ren) ps, map (rename_term ren) qs))))) asms)
   409   | rename_elem ren (Defines defs) = Defines (map (apsnd (fn (t, ps) =>
   410       (rename_term ren t, map (rename_term ren) ps))) defs)
   411   | rename_elem ren (Notes facts) = Notes (map (apsnd (map (apfst (map (rename_thm ren))))) facts);
   412 
   413 fun rename_facts prfx elem =
   414   let
   415     fun qualify (arg as ((name, atts), x)) =
   416       if prfx = "" orelse name = "" then arg
   417       else ((NameSpace.pack [prfx, name], atts), x);
   418   in
   419     (case elem of
   420       Fixes fixes => Fixes fixes
   421     | Assumes asms => Assumes (map qualify asms)
   422     | Defines defs => Defines (map qualify defs)
   423     | Notes facts => Notes (map qualify facts))
   424   end;
   425 
   426 
   427 (* type instantiation *)
   428 
   429 fun inst_type [] T = T
   430   | inst_type env T = Term.map_type_tfree (fn v => getOpt (assoc (env, v), TFree v)) T;
   431 
   432 fun inst_term [] t = t
   433   | inst_term env t = Term.map_term_types (inst_type env) t;
   434 
   435 fun inst_thm _ [] th = th
   436   | inst_thm ctxt env th =
   437       let
   438         val sign = ProofContext.sign_of ctxt;
   439         val cert = Thm.cterm_of sign;
   440         val certT = Thm.ctyp_of sign;
   441         val {hyps, prop, maxidx, ...} = Thm.rep_thm th;
   442         val tfrees = foldr Term.add_term_tfree_names [] (prop :: hyps);
   443         val env' = List.filter (fn ((a, _), _) => a mem_string tfrees) env;
   444       in
   445         if null env' then th
   446         else
   447           th
   448           |> Drule.implies_intr_list (map cert hyps)
   449           |> Drule.tvars_intr_list (map (#1 o #1) env')
   450           |> (fn (th', al) => th' |>
   451             Thm.instantiate ((map (fn ((a, _), T) => (valOf (assoc (al, a)), certT T)) env'), []))
   452           |> (fn th'' => Drule.implies_elim_list th''
   453               (map (Thm.assume o cert o inst_term env') hyps))
   454       end;
   455 
   456 fun inst_elem _ env (Fixes fixes) =
   457       Fixes (map (fn (x, T, mx) => (x, Option.map (inst_type env) T, mx)) fixes)
   458   | inst_elem _ env (Assumes asms) = Assumes (map (apsnd (map (fn (t, (ps, qs)) =>
   459       (inst_term env t, (map (inst_term env) ps, map (inst_term env) qs))))) asms)
   460   | inst_elem _ env (Defines defs) = Defines (map (apsnd (fn (t, ps) =>
   461       (inst_term env t, map (inst_term env) ps))) defs)
   462   | inst_elem ctxt env (Notes facts) =
   463       Notes (map (apsnd (map (apfst (map (inst_thm ctxt env))))) facts);
   464 
   465 
   466 
   467 (** structured contexts: rename + merge + implicit type instantiation **)
   468 
   469 (* parameter types *)
   470 
   471 (* CB: frozen_tvars has the following type:
   472   ProofContext.context -> Term.typ list -> (Term.indexname * Term.typ) list *)
   473 
   474 fun frozen_tvars ctxt Ts =
   475   let
   476     val tvars = rev (Library.foldl Term.add_tvarsT ([], Ts));
   477     val tfrees = map TFree
   478       (Term.invent_names (ProofContext.used_types ctxt) "'a" (length tvars) ~~ map #2 tvars);
   479   in map #1 tvars ~~ tfrees end;
   480 
   481 fun unify_frozen ctxt maxidx Ts Us =
   482   let
   483     fun paramify (i, NONE) = (i, NONE)
   484       | paramify (i, SOME T) = apsnd SOME (TypeInfer.paramify_dummies (i, T));
   485 
   486     val (maxidx', Ts') = foldl_map paramify (maxidx, Ts);
   487     val (maxidx'', Us') = foldl_map paramify (maxidx', Us);
   488     val tsig = Sign.tsig_of (ProofContext.sign_of ctxt);
   489 
   490     fun unify (env, (SOME T, SOME U)) = (Type.unify tsig env (U, T)
   491           handle Type.TUNIFY =>
   492             raise TYPE ("unify_frozen: failed to unify types", [U, T], []))
   493       | unify (env, _) = env;
   494     val (unifier, _) = Library.foldl unify ((Vartab.empty, maxidx''), Ts' ~~ Us');
   495     val Vs = map (Option.map (Envir.norm_type unifier)) Us';
   496     val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (List.mapPartial I Vs));
   497   in map (Option.map (Envir.norm_type unifier')) Vs end;
   498 
   499 fun params_of elemss = gen_distinct eq_fst (List.concat (map (snd o fst) elemss));
   500 fun params_of' elemss = gen_distinct eq_fst (List.concat (map (snd o fst o fst) elemss));
   501 
   502 (* CB: param_types has the following type:
   503   ('a * 'b option) list -> ('a * 'b) list *)
   504 fun param_types ps = List.mapPartial (fn (_, NONE) => NONE | (x, SOME T) => SOME (x, T)) ps;
   505 
   506 
   507 (* flatten expressions *)
   508 
   509 local
   510 
   511 (* CB: OUTDATED unique_parms has the following type:
   512      'a ->
   513      (('b * (('c * 'd) list * Symtab.key list)) * 'e) list ->
   514      (('b * ('c * 'd) list) * 'e) list  *)
   515 
   516 fun unique_parms ctxt elemss =
   517   let
   518     val param_decls =
   519       List.concat (map (fn (((name, (ps, qs)), _), _) => map (rpair (name, ps)) qs) elemss)
   520       |> Symtab.make_multi |> Symtab.dest;
   521   in
   522     (case find_first (fn (_, ids) => length ids > 1) param_decls of
   523       SOME (q, ids) => err_in_locale ctxt ("Multiple declaration of parameter " ^ quote q)
   524           (map (apsnd (map fst)) ids)
   525     | NONE => map (apfst (apfst (apsnd #1))) elemss)
   526   end;
   527 
   528 (* CB: unify_parms has the following type:
   529      ProofContext.context ->
   530      (string * Term.typ) list ->
   531      (string * Term.typ option) list list ->
   532      ((string * Term.sort) * Term.typ) list list *)
   533 
   534 fun unify_parms ctxt fixed_parms raw_parmss =
   535   let
   536     val sign = ProofContext.sign_of ctxt;
   537     val tsig = Sign.tsig_of sign;
   538     val maxidx = length raw_parmss;
   539     val idx_parmss = (0 upto maxidx - 1) ~~ raw_parmss;
   540 
   541     fun varify i = Term.map_type_tfree (fn (a, S) => TVar ((a, i), S));
   542     fun varify_parms (i, ps) = map (apsnd (varify i)) (param_types ps);
   543     val parms = fixed_parms @ List.concat (map varify_parms idx_parmss);
   544 
   545     fun unify T ((env, maxidx), U) =
   546       Type.unify tsig (env, maxidx) (U, T)
   547       handle Type.TUNIFY =>
   548         let val prt = Sign.string_of_typ sign
   549         in raise TYPE ("unify_parms: failed to unify types " ^
   550           prt U ^ " and " ^ prt T, [U, T], [])
   551         end
   552     fun unify_list (envir, T :: Us) = Library.foldl (unify T) (envir, Us)
   553       | unify_list (envir, []) = envir;
   554     val (unifier, _) = Library.foldl unify_list
   555       ((Vartab.empty, maxidx), map #2 (Symtab.dest (Symtab.make_multi parms)));
   556 
   557     val parms' = map (apsnd (Envir.norm_type unifier)) (gen_distinct eq_fst parms);
   558     val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map #2 parms'));
   559 
   560     fun inst_parms (i, ps) =
   561       foldr Term.add_typ_tfrees [] (List.mapPartial snd ps)
   562       |> List.mapPartial (fn (a, S) =>
   563           let val T = Envir.norm_type unifier' (TVar ((a, i), S))
   564           in if T = TFree (a, S) then NONE else SOME ((a, S), T) end)
   565   in map inst_parms idx_parmss end;
   566 
   567 in
   568 
   569 (* like unify_elemss, but does not touch axioms *)
   570 
   571 fun unify_elemss' _ _ [] = []
   572   | unify_elemss' _ [] [elems] = [elems]
   573   | unify_elemss' ctxt fixed_parms elemss =
   574       let
   575         val envs = unify_parms ctxt fixed_parms (map (#2 o #1 o #1) elemss);
   576         fun inst ((((name, ps), axs), elems), env) =
   577           (((name, map (apsnd (Option.map (inst_type env))) ps),  axs),
   578            map (inst_elem ctxt env) elems);
   579       in map inst (elemss ~~ envs) end;
   580 
   581 fun unify_elemss _ _ [] = []
   582   | unify_elemss _ [] [elems] = [elems]
   583   | unify_elemss ctxt fixed_parms elemss =
   584       let
   585         val envs = unify_parms ctxt fixed_parms (map (#2 o #1 o #1) elemss);
   586         fun inst ((((name, ps), axs), elems), env) =
   587           (((name, map (apsnd (Option.map (inst_type env))) ps), 
   588             map (inst_thm ctxt env) axs), map (inst_elem ctxt env) elems);
   589       in map inst (elemss ~~ envs) end;
   590 
   591 (* flatten_expr:
   592    Extend list of identifiers by those new in locale expression expr.
   593    Compute corresponding list of lists of locale elements (one entry per
   594    identifier).
   595 
   596    Identifiers represent locale fragments and are in an extended form:
   597      ((name, ps), (ax_ps, axs))
   598    (name, ps) is the locale name with all its parameters.
   599    (ax_ps, axs) is the locale axioms with its parameters;
   600      axs are always taken from the top level of the locale hierarchy,
   601      hence axioms may contain additional parameters from later fragments:
   602      ps subset of ax_ps.  axs is either singleton or empty.
   603 
   604    Elements are enriched by identifier-like information:
   605      (((name, ax_ps), axs), elems)
   606    The parameters in ax_ps are the axiom parameters, but enriched by type
   607    info: now each entry is a pair of string and typ option.  Axioms are
   608    type-instantiated.
   609 
   610 *)
   611 
   612 fun flatten_expr ctxt (prev_idents, expr) =
   613   let
   614     val thy = ProofContext.theory_of ctxt;
   615     (* thy used for retrieval of locale info,
   616        ctxt for error messages, parameter unification and instantiation
   617        of axioms *)
   618     (* TODO: consider err_in_locale with thy argument *)
   619 
   620     fun renaming (SOME x :: xs) (y :: ys) = (y, x) :: renaming xs ys
   621       | renaming (NONE :: xs) (y :: ys) = renaming xs ys
   622       | renaming [] _ = []
   623       | renaming xs [] = raise ERROR_MESSAGE ("Too many arguments in renaming: " ^
   624           commas (map (fn NONE => "_" | SOME x => quote x) xs));
   625 
   626     fun rename_parms top ren ((name, ps), (parms, axs)) =
   627       let val ps' = map (rename ren) ps in
   628         (case duplicates ps' of [] => ((name, ps'),
   629           if top then (map (rename ren) parms, map (rename_thm ren) axs)
   630           else (parms, axs))
   631         | dups => err_in_locale ctxt ("Duplicate parameters: " ^ commas_quote dups) [(name, ps')])
   632       end;
   633 
   634     fun identify top (Locale name) =
   635     (* CB: ids_ax is a list of tuples of the form ((name, ps), axs),
   636        where name is a locale name, ps a list of parameter names and axs
   637        a list of axioms relating to the identifier, axs is empty unless
   638        identify at top level (top = true);
   639        parms is accumulated list of parameters *)
   640           let
   641             val {predicate = (_, axioms), import, params, ...} =
   642               the_locale thy name;
   643             val ps = map #1 (#1 params);
   644             val (ids', parms') = identify false import;
   645                 (* acyclic import dependencies *)
   646             val ids'' = ids' @ [((name, ps), ([], []))];
   647             val ids_ax = if top then snd
   648                  (foldl_map (fn (axs, ((name, parms), _)) => let
   649                    val {elems, ...} = the_locale thy name;
   650                    val ts = List.concat (List.mapPartial (fn (Assumes asms, _) =>
   651                      SOME (List.concat (map (map #1 o #2) asms)) | _ => NONE) elems);
   652                    val (axs1, axs2) = splitAt (length ts, axs);
   653                  in (axs2, ((name, parms), (ps, axs1))) end) (axioms, ids''))
   654                else ids'';
   655           in (ids_ax, merge_lists parms' ps) end
   656       | identify top (Rename (e, xs)) =
   657           let
   658             val (ids', parms') = identify top e;
   659             val ren = renaming xs parms'
   660               handle ERROR_MESSAGE msg => err_in_locale' ctxt msg ids';
   661             val ids'' = gen_distinct eq_fst (map (rename_parms top ren) ids');
   662             val parms'' = distinct (List.concat (map (#2 o #1) ids''));
   663           in (ids'', parms'') end
   664       | identify top (Merge es) =
   665           Library.foldl (fn ((ids, parms), e) => let
   666                      val (ids', parms') = identify top e
   667                    in (gen_merge_lists eq_fst ids ids',
   668                        merge_lists parms parms') end)
   669             (([], []), es);
   670 
   671     (* CB: enrich identifiers by parameter types and 
   672        the corresponding elements (with renamed parameters) *)
   673 
   674     fun eval ((name, xs), axs) =
   675       let
   676         val {params = (ps, qs), elems, ...} = the_locale thy name;
   677         val ren = filter_out (op =) (map #1 ps ~~ xs);
   678         val (params', elems') =
   679           if null ren then ((ps, qs), map #1 elems)
   680           else ((map (apfst (rename ren)) ps, map (rename ren) qs),
   681             map (rename_elem ren o #1) elems);
   682         val elems'' = map (rename_facts (space_implode "_" xs)) elems';
   683       in (((name, params'), axs), elems'') end;
   684 
   685     (* compute identifiers, merge with previous ones *)
   686     val idents = gen_rems eq_fst (#1 (identify true expr), prev_idents);
   687     (* add types to params, check for unique params and unify them *)
   688     val raw_elemss = unique_parms ctxt (map eval idents);
   689     val elemss = unify_elemss' ctxt [] raw_elemss;
   690     (* replace params in ids by params from axioms,
   691        adjust types in axioms *)
   692     val all_params' = params_of' elemss;
   693     val all_params = param_types all_params';
   694     val elemss' = map (fn (((name, _), (ps, axs)), elems) =>
   695          (((name, map (fn p => (p, assoc (all_params, p))) ps), axs), elems))
   696          elemss;
   697     fun inst_ax th = let
   698          val {hyps, prop, ...} = Thm.rep_thm th;
   699          val ps = map (apsnd SOME) (Library.foldl Term.add_frees ([], prop :: hyps));
   700          val [env] = unify_parms ctxt all_params [ps];
   701          val th' = inst_thm ctxt env th;
   702        in th' end;
   703     val final_elemss = map (fn ((id, axs), elems) =>
   704          ((id, map inst_ax axs), elems)) elemss';
   705   in (prev_idents @ idents, final_elemss) end;
   706 
   707 end;
   708 
   709 
   710 (* attributes *)
   711 
   712 local
   713 
   714 fun read_att attrib (x, srcs) = (x, map attrib srcs)
   715 
   716 (* CB: Map attrib over
   717    * A context element: add attrib to attribute lists of assumptions,
   718      definitions and facts (on both sides for facts).
   719    * Locale expression: no effect. *)
   720 
   721 fun gen_map_attrib_elem _ (Fixes fixes) = Fixes fixes
   722   | gen_map_attrib_elem attrib (Assumes asms) = Assumes (map (apfst (read_att attrib)) asms)
   723   | gen_map_attrib_elem attrib (Defines defs) = Defines (map (apfst (read_att attrib)) defs)
   724   | gen_map_attrib_elem attrib (Notes facts) =
   725       Notes (map (apfst (read_att attrib) o apsnd (map (read_att attrib))) facts)
   726 
   727 fun gen_map_attrib_elem_expr attrib (Elem elem) = Elem (gen_map_attrib_elem attrib elem)
   728   | gen_map_attrib_elem_expr _ (Expr expr) = Expr expr;
   729 
   730 in
   731 
   732 val map_attrib_element = gen_map_attrib_elem;
   733 val map_attrib_element_i = gen_map_attrib_elem;
   734 val map_attrib_elem_or_expr = gen_map_attrib_elem_expr;
   735 val map_attrib_elem_or_expr_i = gen_map_attrib_elem_expr;
   736 
   737 end;
   738 
   739 
   740 (* activate elements *)
   741 
   742 local
   743 
   744 fun export_axioms axs _ hyps th =
   745   th |> Drule.satisfy_hyps axs
   746      (* CB: replace meta-hyps, using axs, by a single meta-hyp. *)
   747   |> Drule.implies_intr_list (Library.drop (length axs, hyps))
   748      (* CB: turn remaining hyps into assumptions. *)
   749   |> Seq.single
   750 
   751 fun activate_elem _ ((ctxt, axs), Fixes fixes) =
   752       ((ctxt |> ProofContext.add_fixes fixes, axs), [])
   753   | activate_elem _ ((ctxt, axs), Assumes asms) =
   754       let
   755         (* extract context attributes *)
   756         val (Assumes asms) = map_attrib_element_i snd (Assumes asms);
   757         val ts = List.concat (map (map #1 o #2) asms);
   758         val (ps,qs) = splitAt (length ts, axs);
   759         val (ctxt', _) =
   760           ctxt |> ProofContext.fix_frees ts
   761           |> ProofContext.assume_i (export_axioms ps) asms;
   762       in ((ctxt', qs), []) end
   763   | activate_elem _ ((ctxt, axs), Defines defs) =
   764       let
   765         (* extract context attributes *)
   766         val (Defines defs) = map_attrib_element_i snd (Defines defs);
   767         val (ctxt', _) =
   768         ctxt |> ProofContext.assume_i ProofContext.export_def
   769           (defs |> map (fn ((name, atts), (t, ps)) =>
   770             let val (c, t') = ProofContext.cert_def ctxt t
   771             in ((if name = "" then Thm.def_name c else name, atts), [(t', (ps, []))]) end))
   772       in ((ctxt', axs), []) end
   773   | activate_elem is_ext ((ctxt, axs), Notes facts) =
   774       let
   775         (* extract context attributes *)
   776         val (Notes facts) = map_attrib_element_i snd (Notes facts);
   777         val (ctxt', res) = ctxt |> ProofContext.note_thmss_i facts
   778       in ((ctxt', axs), if is_ext then res else []) end;
   779 
   780 fun activate_elems (((name, ps), axs), elems) ctxt =
   781   let val ((ctxt', _), res) =
   782     foldl_map (activate_elem (name = "")) ((ProofContext.qualified true ctxt, axs), elems)
   783       handle ProofContext.CONTEXT (msg, ctxt) => err_in_locale ctxt msg [(name, map fst ps)]
   784   in (ProofContext.restore_qualified ctxt ctxt', res) end;
   785 
   786 fun activate_elemss prep_facts = foldl_map (fn (ctxt, (((name, ps), axs), raw_elems)) =>
   787   let
   788     val elems = map (prep_facts ctxt) raw_elems;
   789     val (ctxt', res) = apsnd List.concat (activate_elems (((name, ps), axs), elems) ctxt);
   790   in (ctxt', (((name, ps), elems), res)) end);
   791 
   792 in
   793 
   794 (* CB: activate_facts prep_facts (ctxt, elemss),
   795    where elemss is a list of pairs consisting of identifiers and
   796    context elements, extends ctxt by the context elements yielding
   797    ctxt' and returns (ctxt', (elemss', facts)).
   798    Identifiers in the argument are of the form ((name, ps), axs) and
   799    assumptions use the axioms in the identifiers to set up exporters
   800    in ctxt'.  elemss' does not contain identifiers and is obtained
   801    from elemss and the intermediate context with prep_facts.
   802    If get_facts or get_facts_i is used for prep_facts, these also remove
   803    the internal/external markers from elemss. *)
   804 
   805 fun activate_facts prep_facts arg =
   806   apsnd (apsnd List.concat o Library.split_list) (activate_elemss prep_facts arg);
   807 
   808 end;
   809 
   810 
   811 (** prepare context elements **)
   812 
   813 (* expressions *)
   814 
   815 fun intern_expr sg (Locale xname) = Locale (intern sg xname)
   816   | intern_expr sg (Merge exprs) = Merge (map (intern_expr sg) exprs)
   817   | intern_expr sg (Rename (expr, xs)) = Rename (intern_expr sg expr, xs);
   818 
   819 
   820 (* parameters *)
   821 
   822 local
   823 
   824 fun prep_fixes prep_vars ctxt fixes =
   825   let val vars = snd (foldl_map prep_vars (ctxt, map (fn (x, T, _) => ([x], T)) fixes))
   826   in map (fn (([x'], T'), (_, _, mx)) => (x', T', mx)) (vars ~~ fixes) end;
   827 
   828 in
   829 
   830 fun read_fixes x = prep_fixes ProofContext.read_vars x;
   831 fun cert_fixes x = prep_fixes ProofContext.cert_vars x;
   832 
   833 end;
   834 
   835 
   836 (* propositions and bindings *)
   837 
   838 (* CB: an internal (Int) locale element was either imported or included,
   839    an external (Ext) element appears directly in the locale. *)
   840 
   841 datatype ('a, 'b) int_ext = Int of 'a | Ext of 'b;
   842 
   843 (* flatten (ids, expr) normalises expr (which is either a locale
   844    expression or a single context element) wrt.
   845    to the list ids of already accumulated identifiers.
   846    It returns (ids', elemss) where ids' is an extension of ids
   847    with identifiers generated for expr, and elemss is the list of
   848    context elements generated from expr.  For details, see flatten_expr.
   849    Additionally, for a locale expression, the elems are grouped into a single
   850    Int; individual context elements are marked Ext.  In this case, the
   851    identifier-like information of the element is as follows:
   852    - for Fixes: (("", ps), []) where the ps have type info NONE
   853    - for other elements: (("", []), []).
   854    The implementation of activate_facts relies on identifier names being
   855    empty strings for external elements.
   856 *)
   857 
   858 fun flatten _ (ids, Elem (Fixes fixes)) =
   859       (ids, [((("", map (rpair NONE o #1) fixes), []), Ext (Fixes fixes))])
   860   | flatten _ (ids, Elem elem) = (ids, [((("", []), []), Ext elem)])
   861   | flatten (ctxt, prep_expr) (ids, Expr expr) =
   862       apsnd (map (apsnd Int)) (flatten_expr ctxt (ids, prep_expr expr));
   863 
   864 local
   865 
   866 local
   867 
   868 fun declare_int_elem (ctxt, Fixes fixes) =
   869       (ctxt |> ProofContext.add_fixes (map (fn (x, T, mx) =>
   870         (x, Option.map (Term.map_type_tfree (TypeInfer.param 0)) T, mx)) fixes), [])
   871   | declare_int_elem (ctxt, _) = (ctxt, []);
   872 
   873 fun declare_ext_elem prep_fixes (ctxt, Fixes fixes) =
   874       (ctxt |> ProofContext.add_fixes (prep_fixes ctxt fixes), [])
   875   | declare_ext_elem _ (ctxt, Assumes asms) = (ctxt, map #2 asms)
   876   | declare_ext_elem _ (ctxt, Defines defs) = (ctxt, map (fn (_, (t, ps)) => [(t, (ps, []))]) defs)
   877   | declare_ext_elem _ (ctxt, Notes facts) = (ctxt, []);
   878 
   879 fun declare_elems prep_fixes (ctxt, (((name, ps), _), elems)) =
   880   let val (ctxt', propps) =
   881     (case elems of
   882       Int es => foldl_map declare_int_elem (ctxt, es)
   883     | Ext e => foldl_map (declare_ext_elem prep_fixes) (ctxt, [e]))
   884     handle ProofContext.CONTEXT (msg, ctxt) => err_in_locale ctxt msg [(name, map fst ps)]
   885   in (ctxt', propps) end;
   886 
   887 in
   888 
   889 (* CB: only called by prep_elemss. *)
   890 
   891 fun declare_elemss prep_fixes fixed_params raw_elemss ctxt =
   892   let
   893     (* CB: fix of type bug of goal in target with context elements.
   894        Parameters new in context elements must receive types that are
   895        distinct from types of parameters in target (fixed_params).  *)
   896     val ctxt_with_fixed =
   897       ProofContext.declare_terms (map Free fixed_params) ctxt;
   898     val int_elemss =
   899       raw_elemss
   900       |> List.mapPartial (fn (id, Int es) => SOME (id, es) | _ => NONE)
   901       |> unify_elemss ctxt_with_fixed fixed_params;
   902     val (_, raw_elemss') =
   903       foldl_map (fn ((_, es) :: elemss, (id, Int _)) => (elemss, (id, Int es)) | x => x)
   904         (int_elemss, raw_elemss);
   905   in foldl_map (declare_elems prep_fixes) (ctxt, raw_elemss') end;
   906 
   907 end;
   908 
   909 local
   910 
   911 (* CB: normalise Assumes and Defines wrt. previous definitions *)
   912 
   913 val norm_term = Envir.beta_norm oo Term.subst_atomic;
   914 
   915 (* CB: following code (abstract_term, abstract_thm, bind_def)
   916    used in eval_text for Defines elements. *)
   917 
   918 fun abstract_term eq =    (*assumes well-formedness according to ProofContext.cert_def*)
   919   let
   920     val body = Term.strip_all_body eq;
   921     val vars = map Free (Term.rename_wrt_term body (Term.strip_all_vars eq));
   922     val (lhs, rhs) = Logic.dest_equals (Term.subst_bounds (vars, body));
   923     val (f, xs) = Term.strip_comb lhs;
   924     val eq' = Term.list_abs_free (map Term.dest_Free xs, rhs);
   925   in (Term.dest_Free f, eq') end;
   926 
   927 fun abstract_thm sign eq =
   928   Thm.assume (Thm.cterm_of sign eq) |> Drule.gen_all |> Drule.abs_def;
   929 
   930 fun bind_def ctxt (name, ps) ((xs, env, ths), eq) =
   931   let
   932     val ((y, T), b) = abstract_term eq;
   933     val b' = norm_term env b;
   934     val th = abstract_thm (ProofContext.sign_of ctxt) eq;
   935     fun err msg = err_in_locale ctxt (msg ^ ": " ^ quote y) [(name, map fst ps)];
   936   in
   937     conditional (exists (equal y o #1) xs) (fn () =>
   938       err "Attempt to define previously specified variable");
   939     conditional (exists (fn (Free (y', _), _) => y = y' | _ => false) env) (fn () =>
   940       err "Attempt to redefine variable");
   941     (Term.add_frees (xs, b'), (Free (y, T), b') :: env, th :: ths)
   942   end;
   943 
   944 (* CB: for finish_elems (Int and Ext) *)
   945 
   946 fun eval_text _ _ _ (text, Fixes _) = text
   947   | eval_text _ _ is_ext ((((exts, exts'), (ints, ints')), (xs, env, defs)), Assumes asms) =
   948       let
   949         val ts = List.concat (map (map #1 o #2) asms);
   950         val ts' = map (norm_term env) ts;
   951         val spec' =
   952           if is_ext then ((exts @ ts, exts' @ ts'), (ints, ints'))
   953           else ((exts, exts'), (ints @ ts, ints' @ ts'));
   954       in (spec', (Library.foldl Term.add_frees (xs, ts'), env, defs)) end
   955   | eval_text ctxt (id, _) _ ((spec, binds), Defines defs) =
   956       (spec, Library.foldl (bind_def ctxt id) (binds, map (#1 o #2) defs))
   957   | eval_text _ _ _ (text, Notes _) = text;
   958 
   959 (* CB: for finish_elems (Ext) *)
   960 
   961 fun closeup _ false elem = elem
   962   | closeup ctxt true elem =
   963       let
   964         fun close_frees t =
   965           let val frees = rev (filter_out (ProofContext.is_fixed ctxt o #1)
   966             (Term.add_frees ([], t)))
   967           in Term.list_all_free (frees, t) end;
   968 
   969         fun no_binds [] = []
   970           | no_binds _ =
   971               raise ProofContext.CONTEXT ("Illegal term bindings in locale element", ctxt);
   972       in
   973         (case elem of
   974           Assumes asms => Assumes (asms |> map (fn (a, propps) =>
   975             (a, map (fn (t, (ps, qs)) => (close_frees t, (no_binds ps, no_binds qs))) propps)))
   976         | Defines defs => Defines (defs |> map (fn (a, (t, ps)) =>
   977             (a, (close_frees (#2 (ProofContext.cert_def ctxt t)), no_binds ps))))
   978         | e => e)
   979       end;
   980 
   981 
   982 fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (x, _, mx) =>
   983       (x, assoc_string (parms, x), mx)) fixes)
   984   | finish_ext_elem _ close (Assumes asms, propp) =
   985       close (Assumes (map #1 asms ~~ propp))
   986   | finish_ext_elem _ close (Defines defs, propp) =
   987       close (Defines (map #1 defs ~~ map (fn [(t, (ps, []))] => (t, ps)) propp))
   988   | finish_ext_elem _ _ (Notes facts, _) = Notes facts;
   989 
   990 (* CB: finish_parms introduces type info from parms to identifiers *)
   991 (* CB: only needed for types that have been NONE so far???
   992    If so, which are these??? *)
   993 
   994 fun finish_parms parms (((name, ps), axs), elems) =
   995   (((name, map (fn (x, _) => (x, assoc (parms, x))) ps), axs), elems);
   996 
   997 fun finish_elems ctxt parms _ (text, ((id, Int e), _)) =
   998       let
   999         val [(id', es)] = unify_elemss ctxt parms [(id, e)];
  1000         val text' = Library.foldl (eval_text ctxt id' false) (text, es);
  1001       in (text', (id', map Int es)) end
  1002   | finish_elems ctxt parms do_close (text, ((id, Ext e), [propp])) =
  1003       let
  1004         val e' = finish_ext_elem parms (closeup ctxt do_close) (e, propp);
  1005         val text' = eval_text ctxt id true (text, e');
  1006       in (text', (id, [Ext e'])) end;
  1007 
  1008 in
  1009 
  1010 (* CB: only called by prep_elemss *)
  1011 
  1012 fun finish_elemss ctxt parms do_close =
  1013   foldl_map (apsnd (finish_parms parms) o finish_elems ctxt parms do_close);
  1014 
  1015 end;
  1016 
  1017 (* CB: type inference and consistency checks for locales *)
  1018 
  1019 fun prep_elemss prep_fixes prepp do_close context fixed_params raw_elemss raw_concl =
  1020   let
  1021     (* CB: contexts computed in the course of this function are discarded.
  1022        They are used for type inference and consistency checks only. *)
  1023     (* CB: fixed_params are the parameters (with types) of the target locale,
  1024        empty list if there is no target. *)
  1025     (* CB: raw_elemss are list of pairs consisting of identifiers and
  1026        context elements, the latter marked as internal or external. *)
  1027     val (raw_ctxt, raw_proppss) = declare_elemss prep_fixes fixed_params raw_elemss context;
  1028     (* CB: raw_ctxt is context with additional fixed variables derived from
  1029        the fixes elements in raw_elemss,
  1030        raw_proppss contains assumptions and definitions from the
  1031        external elements in raw_elemss. *)
  1032     val raw_propps = map List.concat raw_proppss;
  1033     val raw_propp = List.concat raw_propps;
  1034 
  1035     (* CB: add type information from fixed_params to context (declare_terms) *)
  1036     (* CB: process patterns (conclusion and external elements only) *)
  1037     val (ctxt, all_propp) =
  1038       prepp (ProofContext.declare_terms (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp);
  1039     
  1040     (* CB: add type information from conclusion and external elements
  1041        to context *)
  1042     val ctxt = ProofContext.declare_terms (List.concat (map (map fst) all_propp)) ctxt;
  1043 
  1044     (* CB: resolve schematic variables (patterns) in conclusion and external
  1045        elements. *)
  1046     val all_propp' = map2 (op ~~)
  1047       (#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp))), map (map snd) all_propp);
  1048     val (concl, propp) = splitAt(length raw_concl, all_propp');
  1049     val propps = unflat raw_propps propp;
  1050     val proppss = map (uncurry unflat) (raw_proppss ~~ propps);
  1051 
  1052     (* CB: obtain all parameters from identifier part of raw_elemss *)
  1053     val xs = map #1 (params_of' raw_elemss);
  1054     val typing = unify_frozen ctxt 0
  1055       (map (ProofContext.default_type raw_ctxt) xs)
  1056       (map (ProofContext.default_type ctxt) xs);
  1057     val parms = param_types (xs ~~ typing);
  1058     (* CB: parms are the parameters from raw_elemss, with correct typing. *)
  1059 
  1060     (* CB: extract information from assumes and defines elements
  1061        (fixes and notes in raw_elemss don't have an effect on text and elemss),
  1062        compute final form of context elements. *)
  1063     val (text, elemss) = finish_elemss ctxt parms do_close
  1064       (((([], []), ([], [])), ([], [], [])), raw_elemss ~~ proppss);
  1065     (* CB: text has the following structure:
  1066            (((exts, exts'), (ints, ints')), (xs, env, defs))
  1067        where
  1068          exts: external assumptions (terms in external assumes elements)
  1069          exts': dito, normalised wrt. env
  1070          ints: internal assumptions (terms in internal assumes elements)
  1071          ints': dito, normalised wrt. env
  1072          xs: the free variables in exts' and ints' and rhss of definitions,
  1073            this includes parameters except defined parameters
  1074          env: list of term pairs encoding substitutions, where the first term
  1075            is a free variable; substitutions represent defines elements and
  1076            the rhs is normalised wrt. the previous env
  1077          defs: theorems representing the substitutions from defines elements
  1078            (thms are normalised wrt. env).
  1079        elemss is an updated version of raw_elemss:
  1080          - type info added to Fixes
  1081          - axiom and definition statement replaced by corresponding one
  1082            from proppss in Assumes and Defines
  1083          - Facts unchanged
  1084        *)
  1085   in ((parms, elemss, concl), text) end;
  1086 
  1087 in
  1088 
  1089 fun read_elemss x = prep_elemss read_fixes ProofContext.read_propp_schematic x;
  1090 fun cert_elemss x = prep_elemss cert_fixes ProofContext.cert_propp_schematic x;
  1091 
  1092 end;
  1093 
  1094 
  1095 (* facts *)
  1096 
  1097 local
  1098 
  1099 fun prep_name ctxt (name, atts) =
  1100   (* CB: reject qualified theorem names in locale declarations *)
  1101   if NameSpace.is_qualified name then
  1102     raise ProofContext.CONTEXT ("Illegal qualified name: " ^ quote name, ctxt)
  1103   else (name, atts);
  1104 
  1105 fun prep_facts _ _ (Int elem) = elem
  1106   | prep_facts _ _ (Ext (Fixes fixes)) = Fixes fixes
  1107   | prep_facts _ ctxt (Ext (Assumes asms)) = Assumes (map (apfst (prep_name ctxt)) asms)
  1108   | prep_facts _ ctxt (Ext (Defines defs)) = Defines (map (apfst (prep_name ctxt)) defs)
  1109   | prep_facts get ctxt (Ext (Notes facts)) = Notes (facts |> map (fn (a, bs) =>
  1110       (prep_name ctxt a, map (apfst (get ctxt)) bs)));
  1111 
  1112 in
  1113 
  1114 fun get_facts x = prep_facts ProofContext.get_thms x;
  1115 fun get_facts_i x = prep_facts (K I) x;
  1116 
  1117 end;
  1118 
  1119 
  1120 (* full context statements: import + elements + conclusion *)
  1121 
  1122 local
  1123 
  1124 fun prep_context_statement prep_expr prep_elemss prep_facts
  1125     do_close fixed_params import elements raw_concl context =
  1126   let
  1127     val sign = ProofContext.sign_of context;
  1128 
  1129     val (import_ids, raw_import_elemss) = flatten (context, prep_expr sign) ([], Expr import);
  1130     (* CB: normalise "includes" among elements *)
  1131     val raw_elemss = List.concat (#2 ((foldl_map (flatten (context, prep_expr sign))
  1132       (import_ids, elements))));
  1133     (* CB: raw_import_elemss @ raw_elemss is the normalised list of
  1134        context elements obtained from import and elements. *)
  1135     val ((parms, all_elemss, concl), (spec, (_, _, defs))) = prep_elemss do_close
  1136       context fixed_params (raw_import_elemss @ raw_elemss) raw_concl;
  1137     (* CB: all_elemss and parms contain the correct parameter types *)
  1138     val (ps,qs) = splitAt(length raw_import_elemss, all_elemss)
  1139     val (import_ctxt, (import_elemss, _)) =
  1140       activate_facts prep_facts (context, ps);
  1141 
  1142     val (ctxt, (elemss, _)) =
  1143       activate_facts prep_facts (import_ctxt, qs);
  1144     val stmt = gen_distinct Term.aconv
  1145        (List.concat (map (fn ((_, axs), _) =>
  1146          List.concat (map (#hyps o Thm.rep_thm) axs)) qs));
  1147     val cstmt = map (cterm_of sign) stmt;
  1148   in
  1149     ((((import_ctxt, import_elemss), (ctxt, elemss)), (parms, spec, defs)), (cstmt, concl))
  1150   end;
  1151 
  1152 val gen_context = prep_context_statement intern_expr read_elemss get_facts;
  1153 val gen_context_i = prep_context_statement (K I) cert_elemss get_facts_i;
  1154 
  1155 fun gen_statement prep_locale prep_ctxt raw_locale elems concl ctxt =
  1156   let
  1157     val thy = ProofContext.theory_of ctxt;
  1158     val locale = Option.map (prep_locale (Theory.sign_of thy)) raw_locale;
  1159     val (target_stmt, fixed_params, import) =
  1160       (case locale of NONE => ([], [], empty)
  1161       | SOME name =>
  1162           let val {predicate = (stmt, _), params = (ps, _), ...} =
  1163             the_locale thy name
  1164           in (stmt, param_types ps, Locale name) end);
  1165     val ((((locale_ctxt, _), (elems_ctxt, _)), _), (elems_stmt, concl')) =
  1166       prep_ctxt false fixed_params import elems concl ctxt;
  1167   in (locale, (target_stmt, elems_stmt), locale_ctxt, elems_ctxt, concl') end;
  1168 
  1169 in
  1170 
  1171 (* CB: processing of locales for add_locale(_i) and print_locale *)
  1172   (* CB: arguments are: x->import, y->body (elements), z->context *)
  1173 fun read_context x y z = #1 (gen_context true [] x (map Elem y) [] z);
  1174 fun cert_context x y z = #1 (gen_context_i true [] x (map Elem y) [] z);
  1175 
  1176 (* CB: processing of locales for note_thmss(_i),
  1177    Proof.multi_theorem(_i) and antiquotations with option "locale" *)
  1178 val read_context_statement = gen_statement intern gen_context;
  1179 val cert_context_statement = gen_statement (K I) gen_context_i;
  1180 
  1181 end;
  1182 
  1183 
  1184 (** CB: experimental instantiation mechanism **)
  1185 
  1186 fun instantiate loc_name (prfx, attribs) raw_inst ctxt =
  1187   let
  1188     val thy = ProofContext.theory_of ctxt;
  1189     val sign = Theory.sign_of thy;
  1190     val tsig = Sign.tsig_of sign;
  1191     val cert = cterm_of sign;
  1192 
  1193     (** process the locale **)
  1194 
  1195     val {predicate = (_, axioms), params = (ps, _), ...} =
  1196       the_locale thy (intern sign loc_name);
  1197     val fixed_params = param_types ps;
  1198     val init = ProofContext.init thy;
  1199     val (_, raw_elemss) =
  1200           flatten (init, intern_expr sign) ([], Expr (Locale loc_name));
  1201     val ((parms, all_elemss, concl),
  1202          (spec as (_, (ints, _)), (xs, env, defs))) =
  1203       read_elemss false (* do_close *) init
  1204         fixed_params (* could also put [] here??? *) raw_elemss
  1205         [] (* concl *);
  1206 
  1207     (** analyse the instantiation theorem inst **)
  1208 
  1209     val inst = case raw_inst of
  1210         NONE => if null ints
  1211 	  then NONE
  1212 	  else error "Locale has assumptions but no chained fact was found"
  1213       | SOME [] => if null ints
  1214 	  then NONE
  1215 	  else error "Locale has assumptions but no chained fact was found"
  1216       | SOME [thm] => if null ints
  1217 	  then (warning "Locale has no assumptions: fact ignored"; NONE)
  1218 	  else SOME thm
  1219       | SOME _ => error "Multiple facts are not allowed";
  1220 
  1221     val args = case inst of
  1222             NONE => []
  1223           | SOME thm => thm |> prop_of |> ObjectLogic.drop_judgment sign
  1224               |> Term.strip_comb
  1225               |>> (fn t as (Const (s, _)) => if (intern sign loc_name = s)
  1226                         then t
  1227                         else error ("Constant " ^ quote loc_name ^
  1228                           " expected but constant " ^ quote s ^ " was found")
  1229                     | t => error ("Constant " ^ quote loc_name ^ " expected \
  1230                           \but term " ^ quote (Sign.string_of_term sign t) ^
  1231                           " was found"))
  1232               |> snd;
  1233     val cargs = map cert args;
  1234 
  1235     (* process parameters: match their types with those of arguments *)
  1236 
  1237     val def_names = map (fn (Free (s, _), _) => s) env;
  1238     val (defined, assumed) = List.partition
  1239           (fn (s, _) => s mem def_names) fixed_params;
  1240     val cassumed = map (cert o Free) assumed;
  1241     val cdefined = map (cert o Free) defined;
  1242 
  1243     val param_types = map snd assumed;
  1244     val v_param_types = map Type.varifyT param_types;
  1245     val arg_types = map Term.fastype_of args;
  1246     val Tenv = Library.foldl (Type.typ_match tsig)
  1247           (Vartab.empty, v_param_types ~~ arg_types)
  1248           handle UnequalLengths => error "Number of parameters does not \
  1249             \match number of arguments of chained fact";
  1250     (* get their sorts *)
  1251     val tfrees = foldr Term.add_typ_tfrees [] param_types
  1252     val Tenv' = map
  1253           (fn ((a, i), T) => ((a, valOf (assoc_string (tfrees, a))), T))
  1254           (Vartab.dest Tenv);
  1255 
  1256     (* process (internal) elements *)
  1257 
  1258     fun inst_type [] T = T
  1259       | inst_type env T =
  1260           Term.map_type_tfree (fn v => getOpt (assoc (env, v), TFree v)) T;
  1261 
  1262     fun inst_term [] t = t
  1263       | inst_term env t = Term.map_term_types (inst_type env) t;
  1264 
  1265     (* parameters with argument types *)
  1266 
  1267     val cparams' = map (cterm_of sign o inst_term Tenv' o term_of) cassumed;
  1268     val cdefined' = map (cert o inst_term Tenv' o term_of) cdefined;
  1269     val cdefining = map (cert o inst_term Tenv' o snd) env;
  1270 
  1271     fun inst_thm _ [] th = th
  1272       | inst_thm ctxt Tenv th =
  1273 	  let
  1274 	    val sign = ProofContext.sign_of ctxt;
  1275 	    val cert = Thm.cterm_of sign;
  1276 	    val certT = Thm.ctyp_of sign;
  1277 	    val {hyps, prop, maxidx, ...} = Thm.rep_thm th;
  1278 	    val tfrees = foldr Term.add_term_tfree_names [] (prop :: hyps);
  1279 	    val Tenv' = List.filter (fn ((a, _), _) => a mem_string tfrees) Tenv;
  1280 	  in
  1281 	    if null Tenv' then th
  1282 	    else
  1283 	      th
  1284 	      |> Drule.implies_intr_list (map cert hyps)
  1285 	      |> Drule.tvars_intr_list (map (#1 o #1) Tenv')
  1286 	      |> (fn (th', al) => th' |>
  1287 		Thm.instantiate ((map (fn ((a, _), T) =>
  1288                   (valOf (assoc (al, a)), certT T)) Tenv'), []))
  1289 	      |> (fn th'' => Drule.implies_elim_list th''
  1290 		  (map (Thm.assume o cert o inst_term Tenv') hyps))
  1291 	  end;
  1292 
  1293     fun inst_thm' thm =
  1294       let
  1295         (* not all axs are normally applicable *)
  1296         val hyps = #hyps (rep_thm thm);
  1297         val ass = map (fn ax => (prop_of ax, ax)) axioms;
  1298         val axs' = Library.foldl (fn (axs, hyp) => 
  1299               (case gen_assoc (op aconv) (ass, hyp) of NONE => axs
  1300                  | SOME ax => axs @ [ax])) ([], hyps);
  1301         val thm' = Drule.satisfy_hyps axs' thm;
  1302         (* instantiate types *)
  1303         val thm'' = inst_thm ctxt Tenv' thm';
  1304         (* substitute arguments and discharge hypotheses *)
  1305         val thm''' = case inst of
  1306                 NONE => thm''
  1307               | SOME inst_thm => let
  1308 		    val hyps = #hyps (rep_thm thm'');
  1309 		    val th = thm'' |> implies_intr_hyps
  1310 		      |> forall_intr_list (cparams' @ cdefined')
  1311 		      |> forall_elim_list (cargs @ cdefining)
  1312 		    (* th has premises of the form either inst_thm or x==x *)
  1313 		    fun mk hyp = if Logic.is_equals hyp
  1314 			  then hyp |> Logic.dest_equals |> snd |> cert
  1315 				 |> reflexive
  1316 			  else inst_thm
  1317                   in implies_elim_list th (map mk hyps)
  1318                   end;
  1319       in thm''' end;
  1320 
  1321     val prefix_fact =
  1322       if prfx = "" then I
  1323       else (fn "" => ""
  1324              | s => NameSpace.append prfx s);
  1325 
  1326     fun inst_elem (ctxt, (Ext _)) = ctxt
  1327       | inst_elem (ctxt, (Int (Notes facts))) =
  1328               (* instantiate fact *)
  1329           let (* extract context attributes *)
  1330               val (Notes facts) = map_attrib_element_i snd (Notes facts);
  1331               val facts' =
  1332                 map (apsnd (map (apfst (map inst_thm')))) facts
  1333 		handle THM (msg, n, thms) => error ("Exception THM " ^
  1334 		  string_of_int n ^ " raised\n" ^
  1335 		  "Note: instantiate does not support old-style locales \
  1336                   \declared with (open)\n" ^ msg ^ "\n" ^
  1337 		  cat_lines (map string_of_thm thms))
  1338               (* rename fact *)
  1339               val facts'' = map (apfst (apfst prefix_fact)) facts'
  1340               (* add attributes *)
  1341               val facts''' = map (apfst (apsnd (fn atts => atts @ attribs))) facts''
  1342           in fst (ProofContext.note_thmss_i facts''' ctxt)
  1343           end
  1344       | inst_elem (ctxt, (Int _)) = ctxt;
  1345 
  1346     fun inst_elems (ctxt, (id, elems)) = Library.foldl inst_elem (ctxt, elems);
  1347 
  1348     fun inst_elemss ctxt elemss = Library.foldl inst_elems (ctxt, elemss);
  1349 
  1350     (* main part *)
  1351 
  1352     val ctxt' = ProofContext.qualified true ctxt;
  1353   in ProofContext.restore_qualified ctxt (inst_elemss ctxt' all_elemss)
  1354   end;
  1355 
  1356 
  1357 (** define locales **)
  1358 
  1359 (* print locale *)
  1360 
  1361 fun print_locale thy import body =
  1362   let
  1363     val thy_ctxt = ProofContext.init thy;
  1364     val (((_, import_elemss), (ctxt, elemss)), _) = read_context import body thy_ctxt;
  1365     val all_elems = List.concat (map #2 (import_elemss @ elemss));
  1366 
  1367     val prt_typ = Pretty.quote o ProofContext.pretty_typ ctxt;
  1368     val prt_term = Pretty.quote o ProofContext.pretty_term ctxt;
  1369     val prt_thm = Pretty.quote o ProofContext.pretty_thm ctxt;
  1370 
  1371     fun prt_syn syn =
  1372       let val s = (case syn of NONE => "(structure)" | SOME mx => Syntax.string_of_mixfix mx)
  1373       in if s = "" then [] else [Pretty.brk 2, Pretty.str s] end;
  1374     fun prt_fix (x, SOME T, syn) = Pretty.block (Pretty.str (x ^ " ::") :: Pretty.brk 1 ::
  1375           prt_typ T :: Pretty.brk 1 :: prt_syn syn)
  1376       | prt_fix (x, NONE, syn) = Pretty.block (Pretty.str x :: Pretty.brk 1 :: prt_syn syn);
  1377 
  1378     fun prt_name "" = [Pretty.brk 1]
  1379       | prt_name name = [Pretty.str (ProofContext.cond_extern ctxt name ^ ":"), Pretty.brk 1];
  1380     fun prt_asm ((a, _), ts) = Pretty.block (prt_name a @ Pretty.breaks (map (prt_term o fst) ts));
  1381     fun prt_def ((a, _), (t, _)) = Pretty.block (prt_name a @ [prt_term t]);
  1382     fun prt_fact ((a, _), ths) = Pretty.block
  1383       (prt_name a @ Pretty.breaks (map prt_thm (List.concat (map fst ths))));
  1384 
  1385     fun items _ [] = []
  1386       | items prfx (x :: xs) = Pretty.block [Pretty.str prfx, Pretty.brk 1, x] :: items "  and" xs;
  1387     fun prt_elem (Fixes fixes) = items "fixes" (map prt_fix fixes)
  1388       | prt_elem (Assumes asms) = items "assumes" (map prt_asm asms)
  1389       | prt_elem (Defines defs) = items "defines" (map prt_def defs)
  1390       | prt_elem (Notes facts) = items "notes" (map prt_fact facts);
  1391   in
  1392     Pretty.big_list "context elements:" (map (Pretty.chunks o prt_elem) all_elems)
  1393     |> Pretty.writeln
  1394   end;
  1395 
  1396 
  1397 (* store results *)
  1398 
  1399 local
  1400 
  1401 fun hide_bound_names names thy =
  1402   thy |> PureThy.hide_thms false
  1403     (map (Sign.full_name (Theory.sign_of thy)) (filter_out (equal "") names));
  1404 
  1405 in
  1406 
  1407 fun note_thmss_qualified kind name args thy =
  1408   thy
  1409   |> Theory.add_path (Sign.base_name name)
  1410   |> PureThy.note_thmss_i (Drule.kind kind) args
  1411   |>> hide_bound_names (map (#1 o #1) args)
  1412   |>> Theory.parent_path;
  1413 
  1414 fun note_thms_qualified' kind (arg as ((name, atts), thms)) thy =
  1415   let
  1416     val qname = NameSpace.unpack name
  1417   in
  1418     if length qname <= 1
  1419     then PureThy.note_thmss_i kind [arg] thy
  1420   else let val (prfx, n) = split_last qname
  1421     in thy
  1422       |> Theory.add_path (NameSpace.pack prfx)
  1423       |> PureThy.note_thmss_i kind [((n, atts), thms)]
  1424       |>> funpow (length prfx) Theory.parent_path
  1425     end
  1426   end;
  1427 
  1428 (* prfx may be empty (not yet), names (in args) may be qualified *)
  1429 
  1430 fun note_thmss_qualified' kind prfx args thy =
  1431   thy
  1432   |> Theory.add_path (Sign.base_name prfx)
  1433   |> (fn thy => Library.foldl (fn ((thy, res), arg) =>
  1434         let val (thy', res') = note_thms_qualified' (Drule.kind kind) arg thy
  1435         in (thy', res @ res') end) ((thy, []), args))
  1436 (*  |>> hide_bound_names (map (#1 o #1) args) *)
  1437   |>> Theory.parent_path;
  1438 
  1439 fun smart_note_thmss kind NONE = PureThy.note_thmss_i (Drule.kind kind)
  1440   | smart_note_thmss kind (SOME (loc, _)) = note_thmss_qualified kind loc;
  1441   (* CB: only used in Proof.finish_global. *)
  1442 
  1443 end;
  1444 
  1445 local
  1446 
  1447 fun put_facts loc args thy =
  1448   let
  1449     val {predicate, import, elems, params} = the_locale thy loc;
  1450     val note = Notes (map (fn ((a, more_atts), th_atts) =>
  1451       ((a, more_atts), map (apfst (map (curry Thm.name_thm a))) th_atts)) args);
  1452   in thy |> put_locale loc {predicate = predicate, import = import, elems = elems @ [(note, stamp ())],
  1453     params = params} end;
  1454 
  1455 fun gen_note_thmss prep_locale get_thms kind raw_loc raw_args thy =
  1456   let
  1457     val thy_ctxt = ProofContext.init thy;
  1458     val loc = prep_locale (Theory.sign_of thy) raw_loc;
  1459     val (_, (stmt, _), loc_ctxt, _, _) =
  1460       cert_context_statement (SOME loc) [] [] thy_ctxt;
  1461     val args = map (apsnd (map (apfst (get_thms loc_ctxt)))) raw_args;
  1462     (* convert multi attributes to context attributes for
  1463        ProofContext.note_thmss_i *)
  1464     val args'' = args
  1465           |> map (apfst (apsnd (map snd)))
  1466           |> map (apsnd (map (apsnd (map snd))));
  1467     val export = ProofContext.export_standard stmt loc_ctxt thy_ctxt;
  1468     val results = map (map export o #2) (#2 (ProofContext.note_thmss_i args'' loc_ctxt));
  1469     val args' = map (rpair [] o #1 o #1) args ~~ map (single o Thm.no_attributes) results;
  1470   in
  1471     thy
  1472     |> put_facts loc args
  1473     |> note_thmss_qualified kind loc args'
  1474   end;
  1475 
  1476 in
  1477 
  1478 (* CB: note_thmss(_i) is the base for the Isar commands
  1479    "theorems (in loc)" and "declare (in loc)". *)
  1480 
  1481 val note_thmss = gen_note_thmss intern ProofContext.get_thms;
  1482 val note_thmss_i = gen_note_thmss (K I) (K I);
  1483 
  1484 (* CB: only used in Proof.finish_global. *)
  1485 
  1486 fun add_thmss loc args (thy, ctxt) =
  1487   let
  1488     val args' = map (fn ((a, ths), atts) => ((a, atts), [(ths, [])])) args;
  1489     val thy' = put_facts loc args' thy;
  1490     val (ctxt', (_, facts')) =
  1491       activate_facts (K I) (ctxt, [((("", []), []), [Notes args'])]);
  1492   in ((thy', ctxt'), facts') end;
  1493 
  1494 end;
  1495 
  1496 
  1497 (* predicate text *)
  1498 (* CB: generate locale predicates and delta predicates *)
  1499 
  1500 local
  1501 
  1502 (* introN: name of theorems for introduction rules of locale and
  1503      delta predicates;
  1504    axiomsN: name of theorem set with destruct rules for locale predicates,
  1505      also name suffix of delta predicates. *)
  1506 
  1507 val introN = "intro";
  1508 val axiomsN = "axioms";
  1509 
  1510 fun atomize_spec sign ts =
  1511   let
  1512     val t = foldr1 Logic.mk_conjunction ts;
  1513     val body = ObjectLogic.atomize_term sign t;
  1514     val bodyT = Term.fastype_of body;
  1515   in
  1516     if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of sign t))
  1517     else (body, bodyT, ObjectLogic.atomize_rule sign (Thm.cterm_of sign t))
  1518   end;
  1519 
  1520 fun aprop_tr' n c = (c, fn args =>
  1521   if length args = n then Syntax.const "_aprop" $ Term.list_comb (Syntax.free c, args)
  1522   else raise Match);
  1523 
  1524 (* CB: define one predicate including its intro rule and axioms
  1525    - bname: predicate name
  1526    - parms: locale parameters
  1527    - defs: thms representing substitutions from defines elements
  1528    - ts: terms representing locale assumptions (not normalised wrt. defs)
  1529    - norm_ts: terms representing locale assumptions (normalised wrt. defs)
  1530    - thy: the theory
  1531 *)
  1532 
  1533 fun def_pred bname parms defs ts norm_ts thy =
  1534   let
  1535     val sign = Theory.sign_of thy;
  1536     val name = Sign.full_name sign bname;
  1537 
  1538     val (body, bodyT, body_eq) = atomize_spec sign norm_ts;
  1539     val env = Term.add_term_free_names (body, []);
  1540     val xs = List.filter (fn (x, _) => x mem_string env) parms;
  1541     val Ts = map #2 xs;
  1542     val extraTs = (Term.term_tfrees body \\ foldr Term.add_typ_tfrees [] Ts)
  1543       |> Library.sort_wrt #1 |> map TFree;
  1544     val predT = map Term.itselfT extraTs ---> Ts ---> bodyT;
  1545 
  1546     val args = map Logic.mk_type extraTs @ map Free xs;
  1547     val head = Term.list_comb (Const (name, predT), args);
  1548     val statement = ObjectLogic.assert_propT sign head;
  1549 
  1550     val (defs_thy, [pred_def]) =
  1551       thy
  1552       |> (if bodyT <> propT then I else
  1553         Theory.add_trfuns ([], [], map (aprop_tr' (length args)) (NameSpace.accesses' name), []))
  1554       |> Theory.add_consts_i [(bname, predT, Syntax.NoSyn)]
  1555       |> PureThy.add_defs_i false [((Thm.def_name bname, Logic.mk_equals (head, body)), [])];
  1556 
  1557     val defs_sign = Theory.sign_of defs_thy;
  1558     val cert = Thm.cterm_of defs_sign;
  1559 
  1560     val intro = Tactic.prove_standard defs_sign [] norm_ts statement (fn _ =>
  1561       Tactic.rewrite_goals_tac [pred_def] THEN
  1562       Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
  1563       Tactic.compose_tac (false, Drule.conj_intr_list (map (Thm.assume o cert) norm_ts), 0) 1);
  1564 
  1565     val conjuncts =
  1566       Drule.equal_elim_rule1 OF [Thm.symmetric body_eq,
  1567         Tactic.rewrite_rule [pred_def] (Thm.assume (cert statement))]
  1568       |> Drule.conj_elim_precise (length ts);
  1569     val axioms = (ts ~~ conjuncts) |> map (fn (t, ax) =>
  1570       Tactic.prove defs_sign [] [] t (fn _ =>
  1571         Tactic.rewrite_goals_tac defs THEN
  1572         Tactic.compose_tac (false, ax, 0) 1));
  1573   in (defs_thy, (statement, intro, axioms)) end;
  1574 
  1575 (* CB: modify the locale elements:
  1576    - assumes elements become notes elements,
  1577    - notes elements are lifted
  1578 *)
  1579 
  1580 fun change_elem _ (axms, Assumes asms) =
  1581       apsnd Notes ((axms, asms) |> foldl_map (fn (axs, (a, spec)) =>
  1582         let val (ps,qs) = splitAt(length spec, axs)
  1583         in (qs, (a, [(ps, [])])) end))
  1584   | change_elem f (axms, Notes facts) = (axms, Notes (map (apsnd (map (apfst (map f)))) facts))
  1585   | change_elem _ e = e;
  1586 
  1587 (* CB: changes only "new" elems, these have identifier ("", _). *)
  1588 
  1589 fun change_elemss axioms elemss = (axioms, elemss) |> foldl_map
  1590   (fn (axms, (id as ("", _), es)) =>
  1591     foldl_map (change_elem (Drule.satisfy_hyps axioms)) (axms, es) |> apsnd (pair id)
  1592   | x => x) |> #2;
  1593 
  1594 in
  1595 
  1596 (* CB: main predicate definition function *)
  1597 
  1598 fun define_preds bname (parms, ((exts, exts'), (ints, ints')), defs) elemss thy =
  1599   let
  1600     val (thy', (elemss', more_ts)) =
  1601       if null exts then (thy, (elemss, []))
  1602       else
  1603         let
  1604           val aname = if null ints then bname else bname ^ "_" ^ axiomsN;
  1605           val (def_thy, (statement, intro, axioms)) =
  1606             thy |> def_pred aname parms defs exts exts';
  1607           val elemss' = change_elemss axioms elemss @
  1608             [(("", []), [Assumes [((bname ^ "_" ^ axiomsN, []), [(statement, ([], []))])]])];
  1609         in
  1610           def_thy |> note_thmss_qualified "" aname
  1611             [((introN, []), [([intro], [])])]
  1612           |> #1 |> rpair (elemss', [statement])
  1613         end;
  1614     val (thy'', predicate) =
  1615       if null ints then (thy', ([], []))
  1616       else
  1617         let
  1618           val (def_thy, (statement, intro, axioms)) =
  1619             thy' |> def_pred bname parms defs (ints @ more_ts) (ints' @ more_ts);
  1620           val cstatement = Thm.cterm_of (Theory.sign_of def_thy) statement;
  1621         in
  1622           def_thy |> note_thmss_qualified "" bname
  1623             [((introN, []), [([intro], [])]),
  1624              ((axiomsN, []), [(map Drule.standard axioms, [])])]
  1625           |> #1 |> rpair ([cstatement], axioms)
  1626         end;
  1627   in (thy'', (elemss', predicate)) end;
  1628 
  1629 end;
  1630 
  1631 
  1632 (* add_locale(_i) *)
  1633 
  1634 local
  1635 
  1636 fun gen_add_locale prep_ctxt prep_expr do_pred bname raw_import raw_body thy =
  1637   (* CB: do_pred controls generation of predicates.
  1638          true -> with, false -> without predicates. *)
  1639   let
  1640     val sign = Theory.sign_of thy;
  1641     val name = Sign.full_name sign bname;
  1642     val _ = conditional (isSome (get_locale thy name)) (fn () =>
  1643       error ("Duplicate definition of locale " ^ quote name));
  1644 
  1645     val thy_ctxt = ProofContext.init thy;
  1646     val (((import_ctxt, import_elemss), (body_ctxt, body_elemss)), text) =
  1647       prep_ctxt raw_import raw_body thy_ctxt;
  1648     val elemss = import_elemss @ body_elemss;
  1649 
  1650     val (pred_thy, (elemss', predicate as (predicate_statement, predicate_axioms))) =
  1651       if do_pred then thy |> define_preds bname text elemss
  1652       else (thy, (elemss, ([], [])));
  1653     val pred_ctxt = ProofContext.init pred_thy;
  1654 
  1655     fun axiomify axioms elemss = 
  1656       (axioms, elemss) |> foldl_map (fn (axs, (id, elems)) => let
  1657                    val ts = List.concat (List.mapPartial (fn (Assumes asms) =>
  1658                      SOME (List.concat (map (map #1 o #2) asms)) | _ => NONE) elems);
  1659                    val (axs1, axs2) = splitAt (length ts, axs);
  1660                  in (axs2, ((id, axs1), elems)) end)
  1661         |> snd;
  1662     val (ctxt, (_, facts)) = activate_facts (K I)
  1663       (pred_ctxt, axiomify predicate_axioms elemss');
  1664     val export = ProofContext.export_standard predicate_statement ctxt pred_ctxt;
  1665     val facts' = facts |> map (fn (a, ths) => ((a, []), [(map export ths, [])]));
  1666   in
  1667     pred_thy
  1668     |> note_thmss_qualified "" name facts' |> #1
  1669     |> declare_locale name
  1670     |> put_locale name {predicate = predicate, import = prep_expr sign raw_import,
  1671         elems = map (fn e => (e, stamp ())) (List.concat (map #2 (List.filter (equal "" o #1 o #1) elemss'))),
  1672         params = (params_of elemss', map #1 (params_of body_elemss))}
  1673   end;
  1674 
  1675 in
  1676 
  1677 val add_locale = gen_add_locale read_context intern_expr;
  1678 
  1679 val add_locale_i = gen_add_locale cert_context (K I);
  1680 
  1681 end;
  1682 
  1683 
  1684 
  1685 (** Interpretation commands **)
  1686 
  1687 local
  1688 
  1689 (** instantiate free vars **)
  1690 
  1691 (* instantiate TFrees *)
  1692 
  1693 fun tinst_type tinst T = if Symtab.is_empty tinst
  1694       then T
  1695       else Term.map_type_tfree
  1696         (fn (v as (x, _)) => getOpt (Symtab.lookup (tinst, x), (TFree v))) T;
  1697 
  1698 fun tinst_term tinst t = if Symtab.is_empty tinst
  1699       then t
  1700       else Term.map_term_types (tinst_type tinst) t;
  1701 
  1702 fun tinst_thm sg tinst thm = if Symtab.is_empty tinst
  1703       then thm
  1704       else let
  1705           val cert = Thm.cterm_of sg;
  1706           val certT = Thm.ctyp_of sg;
  1707           val {hyps, prop, ...} = Thm.rep_thm thm;
  1708           val tfrees = foldr Term.add_term_tfree_names [] (prop :: hyps);
  1709           val tinst' = Symtab.dest tinst |>
  1710                 List.filter (fn (a, _) => a mem_string tfrees);
  1711         in
  1712           if null tinst' then thm
  1713           else thm |> Drule.implies_intr_list (map cert hyps)
  1714             |> Drule.tvars_intr_list (map #1 tinst')
  1715             |> (fn (th, al) => th |> Thm.instantiate
  1716                 ((map (fn (a, T) => (valOf (assoc (al, a)), certT T)) tinst'),
  1717                   []))
  1718             |> (fn th => Drule.implies_elim_list th
  1719                  (map (Thm.assume o cert o tinst_term tinst) hyps))
  1720         end;
  1721 
  1722 fun tinst_elem _ tinst (Fixes fixes) =
  1723       Fixes (map (fn (x, T, mx) => (x, Option.map (tinst_type tinst) T, mx)) fixes)
  1724   | tinst_elem _ tinst (Assumes asms) =
  1725       Assumes (map (apsnd (map (fn (t, (ps, qs)) =>
  1726         (tinst_term tinst t,
  1727           (map (tinst_term tinst) ps, map (tinst_term tinst) qs))))) asms)
  1728   | tinst_elem _ tinst (Defines defs) =
  1729       Defines (map (apsnd (fn (t, ps) =>
  1730         (tinst_term tinst t, map (tinst_term tinst) ps))) defs)
  1731   | tinst_elem sg tinst (Notes facts) =
  1732       Notes (map (apsnd (map (apfst (map (tinst_thm sg tinst))))) facts);
  1733 
  1734 (* instantiate TFrees and Frees *)
  1735 
  1736 fun inst_term (inst, tinst) = if Symtab.is_empty inst
  1737       then tinst_term tinst
  1738       else (* instantiate terms and types simultaneously *)
  1739         let
  1740           fun instf (Const (x, T)) = Const (x, tinst_type tinst T)
  1741             | instf (Free (x, T)) = (case Symtab.lookup (inst, x) of
  1742                  NONE => Free (x, tinst_type tinst T)
  1743                | SOME t => t)
  1744             | instf (Var (xi, T)) = Var (xi, tinst_type tinst T)
  1745             | instf (b as Bound _) = b
  1746             | instf (Abs (x, T, t)) = Abs (x, tinst_type tinst T, instf t)
  1747             | instf (s $ t) = instf s $ instf t
  1748         in instf end;
  1749 
  1750 fun inst_thm sg (inst, tinst) thm = if Symtab.is_empty inst
  1751       then tinst_thm sg tinst thm
  1752       else let
  1753           val cert = Thm.cterm_of sg;
  1754           val certT = Thm.ctyp_of sg;
  1755           val {hyps, prop, ...} = Thm.rep_thm thm;
  1756           (* type instantiations *)
  1757           val tfrees = foldr Term.add_term_tfree_names [] (prop :: hyps);
  1758           val tinst' = Symtab.dest tinst |>
  1759                 List.filter (fn (a, _) => a mem_string tfrees);
  1760           (* term instantiations;
  1761              note: lhss are type instantiated, because
  1762                    type insts will be done first*)
  1763           val frees = foldr Term.add_term_frees [] (prop :: hyps);
  1764           val inst' = Symtab.dest inst |>
  1765                 List.mapPartial (fn (a, t) =>
  1766                   get_first (fn (Free (x, T)) => 
  1767                     if a = x then SOME (Free (x, tinst_type tinst T), t)
  1768                     else NONE) frees);
  1769         in
  1770           if null tinst' andalso null inst' then tinst_thm sg tinst thm
  1771           else thm |> Drule.implies_intr_list (map cert hyps)
  1772             |> Drule.tvars_intr_list (map #1 tinst')
  1773             |> (fn (th, al) => th |> Thm.instantiate
  1774                 ((map (fn (a, T) => (valOf (assoc (al, a)), certT T)) tinst'),
  1775                   []))
  1776             |> Drule.forall_intr_list (map (cert o #1) inst')
  1777             |> Drule.forall_elim_list (map (cert o #2) inst') 
  1778             |> (fn th => Drule.implies_elim_list th
  1779                  (map (Thm.assume o cert o inst_term (inst, tinst)) hyps))
  1780         end;
  1781 
  1782 fun inst_elem _ (_, tinst) (Fixes fixes) =
  1783       Fixes (map (fn (x, T, mx) => (x, Option.map (tinst_type tinst) T, mx)) fixes)
  1784   | inst_elem _ inst (Assumes asms) =
  1785       Assumes (map (apsnd (map (fn (t, (ps, qs)) =>
  1786         (inst_term inst t,
  1787           (map (inst_term inst) ps, map (inst_term inst) qs))))) asms)
  1788   | inst_elem _ inst (Defines defs) =
  1789       Defines (map (apsnd (fn (t, ps) =>
  1790         (inst_term inst t, map (inst_term inst) ps))) defs)
  1791   | inst_elem sg inst (Notes facts) =
  1792       Notes (map (apsnd (map (apfst (map (inst_thm sg inst))))) facts);
  1793 
  1794 fun inst_elems sign inst ((n, ps), elems) =
  1795       ((n, map (inst_term inst) ps), map (inst_elem sign inst) elems);
  1796 
  1797 (* extract proof obligations (assms and defs) from elements *)
  1798 
  1799 (* check if defining equation has become t == t, these are dropped
  1800    in extract_asms_elem, as they lead to trivial proof obligations *)
  1801 (* currently disabled *)
  1802 fun check_def (_, (def, _)) = SOME def;
  1803 (*
  1804 fun check_def (_, (def, _)) =
  1805       if def |> Logic.dest_equals |> op aconv
  1806       then NONE else SOME def;
  1807 *)
  1808 
  1809 fun extract_asms_elem (ts, Fixes _) = ts
  1810   | extract_asms_elem (ts, Assumes asms) =
  1811       ts @ List.concat (map (fn (_, ams) => map (fn (t, _) => t) ams) asms)
  1812   | extract_asms_elem (ts, Defines defs) =
  1813       ts @ List.mapPartial check_def defs
  1814   | extract_asms_elem (ts, Notes _) = ts;
  1815 
  1816 fun extract_asms_elems (id, elems) =
  1817       (id, Library.foldl extract_asms_elem ([], elems));
  1818 
  1819 fun extract_asms_elemss elemss =
  1820       map extract_asms_elems elemss;
  1821 
  1822 (* activate instantiated facts in theory or context *)
  1823 
  1824 fun activate_facts_elem _ _ _ _ (thy_ctxt, Fixes _) = thy_ctxt
  1825   | activate_facts_elem _ _ _ _ (thy_ctxt, Assumes _) = thy_ctxt
  1826   | activate_facts_elem _ _ _ _ (thy_ctxt, Defines _) = thy_ctxt
  1827   | activate_facts_elem note_thmss which
  1828         disch (prfx, atts) (thy_ctxt, Notes facts) =
  1829       let
  1830         (* extract theory or context attributes *)
  1831         val (Notes facts) = map_attrib_element_i which (Notes facts);
  1832         (* add attributs from registration *)
  1833         val facts' = map (apfst (apsnd (fn a => a @ atts))) facts;
  1834         (* discharge hyps and varify *)
  1835         val facts'' = map (apsnd (map (apfst (map disch)))) facts';
  1836         (* prefix names *)
  1837         val facts''' = map (apfst (apfst (fn name =>
  1838           if prfx = "" orelse name = "" then name
  1839           else NameSpace.pack [prfx, name]))) facts'';
  1840       in
  1841         fst (note_thmss prfx facts''' thy_ctxt)
  1842       end;
  1843 
  1844 fun activate_facts_elems get_reg note_thmss which
  1845         disch (thy_ctxt, (id, elems)) =
  1846       let
  1847         val ((prfx, atts2), _) = valOf (get_reg thy_ctxt id)
  1848           handle Option => error ("(internal) unknown registration of " ^
  1849             quote (fst id) ^ " while activating facts.");
  1850       in
  1851         Library.foldl (activate_facts_elem note_thmss which
  1852           disch (prfx, atts2)) (thy_ctxt, elems)
  1853       end;
  1854 
  1855 fun gen_activate_facts_elemss get_reg note_thmss which standard
  1856         all_elemss new_elemss thy_ctxt =
  1857       let
  1858         val prems = List.concat (List.mapPartial (fn (id, _) =>
  1859               Option.map snd (get_reg thy_ctxt id)
  1860                 handle Option => error ("(internal) unknown registration of " ^
  1861                   quote (fst id) ^ " while activating facts.")) all_elemss);
  1862       in Library.foldl (activate_facts_elems get_reg note_thmss which
  1863         (standard o Drule.satisfy_hyps prems)) (thy_ctxt, new_elemss) end;
  1864 
  1865 fun loc_accesses prfx name =
  1866   (* full qualified name is T.p.r.n where
  1867        T: theory name, p: interpretation prefix, r: renaming prefix, n: name
  1868   *)
  1869      if prfx = "" then
  1870        case NameSpace.unpack name of
  1871 	   [] => [""]
  1872 	 | [T, n] => map NameSpace.pack [[T, n], [n]]
  1873 	 | [T, r, n] => map NameSpace.pack [[T, r, n], (*[T, n],*) [r, n], [n]]
  1874 	 | _ => error ("Locale accesses: illegal name " ^ quote name)
  1875      else case NameSpace.unpack name of
  1876            [] => [""]
  1877          | [T, p, n] => map NameSpace.pack [[T, p, n], [p, n]]
  1878          | [T, p, r, n] => map NameSpace.pack
  1879              [[T, p, r, n], [T, p, n], [p, r, n], [p, n]]
  1880          | _ => error ("Locale accesses: illegal name " ^ quote name);
  1881 
  1882 val global_activate_facts_elemss = gen_activate_facts_elemss
  1883       get_global_registration
  1884       (fn prfx => PureThy.note_thmss_qualified_i (loc_accesses prfx)
  1885         (Drule.kind ""))
  1886       fst Drule.standard;
  1887 val local_activate_facts_elemss = gen_activate_facts_elemss
  1888       get_local_registration (fn prfx => fn _ => fn ctxt => (ctxt, ctxt)) snd I;
  1889 (*
  1890 val local_activate_facts_elemss = gen_activate_facts_elemss
  1891       get_local_registration (fn prfx => ProofContext.note_thmss_i) snd I;
  1892 *)
  1893 
  1894 fun gen_prep_registration mk_ctxt read_terms test_reg put_reg activate
  1895     attn expr insts thy_ctxt =
  1896   let
  1897     val ctxt = mk_ctxt thy_ctxt;
  1898     val sign = ProofContext.sign_of ctxt;
  1899 
  1900     val (ids, raw_elemss) =
  1901           flatten (ctxt, intern_expr sign) ([], Expr expr);
  1902     val do_close = false;  (* effect unknown *)
  1903     val ((parms, all_elemss, _), (spec, (xs, defs, _))) =
  1904           read_elemss do_close ctxt [] raw_elemss [];
  1905 
  1906 
  1907     (** compute instantiation **)
  1908 
  1909     (* check user input *)
  1910     val insts = if length parms < length insts
  1911          then error "More arguments than parameters in instantiation."
  1912          else insts @ replicate (length parms - length insts) NONE;
  1913 
  1914     val (ps, pTs) = split_list parms;
  1915     val pvTs = map Type.varifyT pTs;
  1916 
  1917     (* instantiations given by user *)
  1918     val given = List.mapPartial (fn (_, (NONE, _)) => NONE
  1919          | (x, (SOME inst, T)) => SOME (x, (inst, T))) (ps ~~ (insts ~~ pvTs));
  1920     val (given_ps, given_insts) = split_list given;
  1921     val tvars = foldr Term.add_typ_tvars [] pvTs;
  1922     val used = foldr Term.add_typ_varnames [] pvTs;
  1923     fun sorts (a, i) = assoc (tvars, (a, i));
  1924     val (vs, vinst) = read_terms thy_ctxt sorts used given_insts;
  1925     (* replace new types (which are TFrees) by ones with new names *)
  1926     val new_Tnames = foldr Term.add_term_tfree_names [] vs;
  1927     val new_Tnames' = Term.invent_names used "'a" (length new_Tnames);
  1928     val renameT = Term.map_type_tfree (fn (a, s) =>
  1929           TFree (valOf (assoc (new_Tnames ~~ new_Tnames', a)), s));
  1930     val rename = Term.map_term_types renameT;
  1931 
  1932     val tinst = Symtab.make (map
  1933                 (fn ((x, 0), T) => (x, T |> renameT |> Type.unvarifyT)
  1934                   | ((_, n), _) => error "Var in prep_registration") vinst);
  1935     val inst = Symtab.make (given_ps ~~ map (Logic.unvarify o rename) vs);
  1936 
  1937     (* defined params without user input *)
  1938     val not_given = List.mapPartial (fn (x, (NONE, T)) => SOME (x, T)
  1939          | (_, (SOME _, _)) => NONE) (ps ~~ (insts ~~ pTs));
  1940     fun add_def ((inst, tinst), (p, pT)) =
  1941       let
  1942         val (t, T) = case find_first (fn (Free (a, _), _) => a = p) defs of
  1943                NONE => error ("Instance missing for parameter " ^ quote p)
  1944              | SOME (Free (_, T), t) => (t, T);
  1945         val d = t |> inst_term (inst, tinst) |> Envir.beta_norm;
  1946       in (Symtab.update_new ((p, d), inst), tinst) end;
  1947     val (inst, tinst) = Library.foldl add_def ((inst, tinst), not_given);
  1948   
  1949 
  1950     (** compute proof obligations **)
  1951 
  1952     (* restore "small" ids *)
  1953     val ids' = map (fn ((n, ps), _) =>
  1954           (n, map (fn p => Free (p, valOf (assoc (parms, p)))) ps)) ids;
  1955 
  1956     (* instantiate ids and elements *)
  1957     val inst_elemss = map
  1958           (fn (id, (_, elems)) => inst_elems sign (inst, tinst) (id, 
  1959             map (fn Int e => e) elems)) 
  1960           (ids' ~~ all_elemss);
  1961 
  1962     (* remove fragments already registered with theory or context *)
  1963     val new_inst_elemss = List.filter (fn (id, _) =>
  1964           not (test_reg thy_ctxt id)) inst_elemss;
  1965 
  1966     val propss = extract_asms_elemss new_inst_elemss;
  1967 
  1968 
  1969     (** add registrations to theory,
  1970         without theorems, these are added after the proof **)
  1971 
  1972     val thy_ctxt' = Library.foldl (fn (thy_ctxt, (id, _)) =>
  1973           put_reg id attn thy_ctxt) (thy_ctxt, new_inst_elemss);
  1974 
  1975   in (thy_ctxt', propss, activate inst_elemss new_inst_elemss) end;
  1976 
  1977 in
  1978 
  1979 val prep_global_registration = gen_prep_registration
  1980      ProofContext.init
  1981      (fn thy => fn sorts => fn used =>
  1982        Sign.read_def_terms (Theory.sign_of thy, K NONE, sorts) used true)
  1983      test_global_registration
  1984      put_global_registration
  1985      global_activate_facts_elemss;
  1986 
  1987 val prep_local_registration = gen_prep_registration
  1988      I
  1989      (fn ctxt => ProofContext.read_termTs ctxt (K false) (K NONE))
  1990      smart_test_registration
  1991      put_local_registration
  1992      local_activate_facts_elemss;
  1993 
  1994 end;  (* local *)
  1995 
  1996 
  1997 
  1998 (** locale theory setup **)
  1999 
  2000 val setup =
  2001  [GlobalLocalesData.init, LocalLocalesData.init,
  2002   add_locale_i true "var" empty [Fixes [(Syntax.internal "x", NONE, SOME Syntax.NoSyn)]],
  2003   add_locale_i true "struct" empty [Fixes [(Syntax.internal "S", NONE, NONE)]]];
  2004 
  2005 end;