src/Pure/Isar/locale.ML
author haftmann
Mon Dec 01 19:41:16 2008 +0100 (2008-12-01)
changeset 28941 128459bd72d2
parent 28940 df0cb410be35
child 28950 b2db06eb214d
permissions -rw-r--r--
new Binding module
     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 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, structured import of contexts (with merge
    11 and rename operations) are provided, as well as type-inference of the
    12 signature parts, and predicate definitions of the specification text.
    13 
    14 Interpretation enables the reuse of theorems of locales in other
    15 contexts, namely those defined by theories, structured proofs and
    16 locales themselves.
    17 
    18 See also:
    19 
    20 [1] Clemens Ballarin. Locales and Locale Expressions in Isabelle/Isar.
    21     In Stefano Berardi et al., Types for Proofs and Programs: International
    22     Workshop, TYPES 2003, Torino, Italy, LNCS 3085, pages 34-50, 2004.
    23 [2] Clemens Ballarin. Interpretation of Locales in Isabelle: Managing
    24     Dependencies between Locales. Technical Report TUM-I0607, Technische
    25     Universitaet Muenchen, 2006.
    26 [3] Clemens Ballarin. Interpretation of Locales in Isabelle: Theories and
    27     Proof Contexts. In J.M. Borwein and W.M. Farmer, MKM 2006, LNAI 4108,
    28     pages 31-43, 2006.
    29 *)
    30 
    31 (* TODO:
    32 - beta-eta normalisation of interpretation parameters
    33 - dangling type frees in locales
    34 - test subsumption of interpretations when merging theories
    35 *)
    36 
    37 signature LOCALE =
    38 sig
    39   datatype expr =
    40     Locale of string |
    41     Rename of expr * (string * mixfix option) option list |
    42     Merge of expr list
    43   val empty: expr
    44 
    45   val intern: theory -> xstring -> string
    46   val intern_expr: theory -> expr -> expr
    47   val extern: theory -> string -> xstring
    48   val init: string -> theory -> Proof.context
    49 
    50   (* The specification of a locale *)
    51   val parameters_of: theory -> string -> ((string * typ) * mixfix) list
    52   val parameters_of_expr: theory -> expr -> ((string * typ) * mixfix) list
    53   val local_asms_of: theory -> string -> (Attrib.binding * term list) list
    54   val global_asms_of: theory -> string -> (Attrib.binding * term list) list
    55 
    56   (* Theorems *)
    57   val intros: theory -> string -> thm list * thm list
    58   val dests: theory -> string -> thm list
    59   (* Not part of the official interface.  DO NOT USE *)
    60   val facts_of: theory -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list list
    61 
    62   (* Not part of the official interface.  DO NOT USE *)
    63   val declarations_of: theory -> string -> declaration list * declaration list;
    64 
    65   (* Processing of locale statements *)
    66   val read_context_statement: string option -> Element.context list ->
    67     (string * string list) list list -> Proof.context ->
    68     string option * Proof.context * Proof.context * (term * term list) list list
    69   val read_context_statement_cmd: xstring option -> Element.context list ->
    70     (string * string list) list list -> Proof.context ->
    71     string option * Proof.context * Proof.context * (term * term list) list list
    72   val cert_context_statement: string option -> Element.context_i list ->
    73     (term * term list) list list -> Proof.context ->
    74     string option * Proof.context * Proof.context * (term * term list) list list
    75   val read_expr: expr -> Element.context list -> Proof.context ->
    76     Element.context_i list * Proof.context
    77   val cert_expr: expr -> Element.context_i list -> Proof.context ->
    78     Element.context_i list * Proof.context
    79 
    80   (* Diagnostic functions *)
    81   val print_locales: theory -> unit
    82   val print_locale: theory -> bool -> expr -> Element.context list -> unit
    83   val print_registrations: bool -> string -> Proof.context -> unit
    84 
    85   val add_locale: string -> bstring -> expr -> Element.context_i list -> theory
    86     -> string * Proof.context
    87   val add_locale_cmd: bstring -> expr -> Element.context list -> theory
    88     -> string * Proof.context
    89 
    90   (* Tactics *)
    91   val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
    92 
    93   (* Storing results *)
    94   val local_note_qualified: string ->
    95     ((Name.binding * attribute list) * (thm list * attribute list) list) list ->
    96     Proof.context -> (string * thm list) list * Proof.context
    97   val add_thmss: string -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
    98     Proof.context -> Proof.context
    99   val add_type_syntax: string -> declaration -> Proof.context -> Proof.context
   100   val add_term_syntax: string -> declaration -> Proof.context -> Proof.context
   101   val add_declaration: string -> declaration -> Proof.context -> Proof.context
   102 
   103   (* Interpretation *)
   104   val get_interpret_morph: theory -> (Name.binding -> Name.binding) -> string * string ->
   105     (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) ->
   106     string -> term list -> Morphism.morphism
   107   val interpretation: (Proof.context -> Proof.context) ->
   108     (Name.binding -> Name.binding) -> expr ->
   109     term option list * (Attrib.binding * term) list ->
   110     theory ->
   111     (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * Proof.state
   112   val interpretation_cmd: string -> expr -> string option list * (Attrib.binding * string) list ->
   113     theory -> Proof.state
   114   val interpretation_in_locale: (Proof.context -> Proof.context) ->
   115     xstring * expr -> theory -> Proof.state
   116   val interpret: (Proof.state -> Proof.state Seq.seq) ->
   117     (Name.binding -> Name.binding) -> expr ->
   118     term option list * (Attrib.binding * term) list ->
   119     bool -> Proof.state ->
   120     (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * Proof.state
   121   val interpret_cmd: string -> expr -> string option list * (Attrib.binding * string) list ->
   122     bool -> Proof.state -> Proof.state
   123 end;
   124 
   125 structure Locale: LOCALE =
   126 struct
   127 
   128 (* legacy operations *)
   129 
   130 fun merge_lists _ xs [] = xs
   131   | merge_lists _ [] ys = ys
   132   | merge_lists eq xs ys = xs @ filter_out (member eq xs) ys;
   133 
   134 fun merge_alists eq xs = merge_lists (eq_fst eq) xs;
   135 
   136 
   137 (* auxiliary: noting name bindings with qualified base names *)
   138 
   139 fun global_note_qualified kind facts thy =
   140   thy
   141   |> Sign.qualified_names
   142   |> PureThy.note_thmss kind facts
   143   ||> Sign.restore_naming thy;
   144 
   145 fun local_note_qualified kind facts ctxt =
   146   ctxt
   147   |> ProofContext.qualified_names
   148   |> ProofContext.note_thmss_i kind facts
   149   ||> ProofContext.restore_naming ctxt;
   150 
   151 
   152 (** locale elements and expressions **)
   153 
   154 datatype ctxt = datatype Element.ctxt;
   155 
   156 datatype expr =
   157   Locale of string |
   158   Rename of expr * (string * mixfix option) option list |
   159   Merge of expr list;
   160 
   161 val empty = Merge [];
   162 
   163 datatype 'a element =
   164   Elem of 'a | Expr of expr;
   165 
   166 fun map_elem f (Elem e) = Elem (f e)
   167   | map_elem _ (Expr e) = Expr e;
   168 
   169 type decl = declaration * stamp;
   170 
   171 type locale =
   172  {axiom: Element.witness list,
   173     (* For locales that define predicates this is [A [A]], where A is the locale
   174        specification.  Otherwise [].
   175        Only required to generate the right witnesses for locales with predicates. *)
   176   elems: (Element.context_i * stamp) list,
   177     (* Static content, neither Fixes nor Constrains elements *)
   178   params: ((string * typ) * mixfix) list,                        (*all term params*)
   179   decls: decl list * decl list,                    (*type/term_syntax declarations*)
   180   regs: ((string * string list) * Element.witness list) list,
   181     (* Registrations: indentifiers and witnesses of locales interpreted in the locale. *)
   182   intros: thm list * thm list,
   183     (* Introduction rules: of delta predicate and locale predicate. *)
   184   dests: thm list}
   185     (* Destruction rules: projections from locale predicate to predicates of fragments. *)
   186 
   187 (* CB: an internal (Int) locale element was either imported or included,
   188    an external (Ext) element appears directly in the locale text. *)
   189 
   190 datatype ('a, 'b) int_ext = Int of 'a | Ext of 'b;
   191 
   192 
   193 
   194 (** substitutions on Vars -- clone from element.ML **)
   195 
   196 (* instantiate types *)
   197 
   198 fun var_instT_type env =
   199   if Vartab.is_empty env then I
   200   else Term.map_type_tvar (fn (x, S) => the_default (TVar (x, S)) (Vartab.lookup env x));
   201 
   202 fun var_instT_term env =
   203   if Vartab.is_empty env then I
   204   else Term.map_types (var_instT_type env);
   205 
   206 fun var_inst_term (envT, env) =
   207   if Vartab.is_empty env then var_instT_term envT
   208   else
   209     let
   210       val instT = var_instT_type envT;
   211       fun inst (Const (x, T)) = Const (x, instT T)
   212         | inst (Free (x, T)) = Free(x, instT T)
   213         | inst (Var (xi, T)) =
   214             (case Vartab.lookup env xi of
   215               NONE => Var (xi, instT T)
   216             | SOME t => t)
   217         | inst (b as Bound _) = b
   218         | inst (Abs (x, T, t)) = Abs (x, instT T, inst t)
   219         | inst (t $ u) = inst t $ inst u;
   220     in Envir.beta_norm o inst end;
   221 
   222 
   223 (** management of registrations in theories and proof contexts **)
   224 
   225 type registration =
   226   {prfx: (Name.binding -> Name.binding) * (string * string),
   227       (* first component: interpretation name morphism;
   228          second component: parameter prefix *)
   229     exp: Morphism.morphism,
   230       (* maps content to its originating context *)
   231     imp: (typ Vartab.table * typ list) * (term Vartab.table * term list),
   232       (* inverse of exp *)
   233     wits: Element.witness list,
   234       (* witnesses of the registration *)
   235     eqns: thm Termtab.table,
   236       (* theorems (equations) interpreting derived concepts and indexed by lhs *)
   237     morph: unit
   238       (* interpreting morphism *)
   239   }
   240 
   241 structure Registrations :
   242   sig
   243     type T
   244     val empty: T
   245     val join: T * T -> T
   246     val dest: theory -> T ->
   247       (term list *
   248         (((Name.binding -> Name.binding) * (string * string)) *
   249          (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) *
   250          Element.witness list *
   251          thm Termtab.table)) list
   252     val test: theory -> T * term list -> bool
   253     val lookup: theory ->
   254       T * (term list * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) ->
   255       (((Name.binding -> Name.binding) * (string * string)) * Element.witness list * thm Termtab.table) option
   256     val insert: theory -> term list -> ((Name.binding -> Name.binding) * (string * string)) ->
   257       (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) ->
   258       T ->
   259       T * (term list * (((Name.binding -> Name.binding) * (string * string)) * Element.witness list)) list
   260     val add_witness: term list -> Element.witness -> T -> T
   261     val add_equation: term list -> thm -> T -> T
   262 (*
   263     val update_morph: term list -> Morphism.morphism -> T -> T
   264     val get_morph: theory -> T ->
   265       term list * ((typ Vartab.table * typ list) * (term Vartab.table * term list)) ->
   266       Morphism.morphism
   267 *)
   268   end =
   269 struct
   270   (* A registration is indexed by parameter instantiation.
   271      NB: index is exported whereas content is internalised. *)
   272   type T = registration Termtab.table;
   273 
   274   fun mk_reg prfx exp imp wits eqns morph =
   275     {prfx = prfx, exp = exp, imp = imp, wits = wits, eqns = eqns, morph = morph};
   276 
   277   fun map_reg f reg =
   278     let
   279       val {prfx, exp, imp, wits, eqns, morph} = reg;
   280       val (prfx', exp', imp', wits', eqns', morph') = f (prfx, exp, imp, wits, eqns, morph);
   281     in mk_reg prfx' exp' imp' wits' eqns' morph' end;
   282 
   283   val empty = Termtab.empty;
   284 
   285   (* term list represented as single term, for simultaneous matching *)
   286   fun termify ts =
   287     Term.list_comb (Const ("", map fastype_of ts ---> propT), ts);
   288   fun untermify t =
   289     let fun ut (Const _) ts = ts
   290           | ut (s $ t) ts = ut s (t::ts)
   291     in ut t [] end;
   292 
   293   (* joining of registrations:
   294      - prefix and morphisms of right theory;
   295      - witnesses are equal, no attempt to subsumption testing;
   296      - union of equalities, if conflicting (i.e. two eqns with equal lhs)
   297        eqn of right theory takes precedence *)
   298   fun join (r1, r2) = Termtab.join (fn _ => fn ({eqns = e1, ...}, {prfx = n, exp, imp, wits = w, eqns = e2, morph = m}) =>
   299       mk_reg n exp imp w (Termtab.join (fn _ => fn (_, e) => e) (e1, e2)) m) (r1, r2);
   300 
   301   fun dest_transfer thy regs =
   302     Termtab.dest regs |> map (apsnd (map_reg (fn (n, e, i, ws, es, m) =>
   303       (n, e, i, map (Element.transfer_witness thy) ws, Termtab.map (transfer thy) es, m))));
   304 
   305   fun dest thy regs = dest_transfer thy regs |> map (apfst untermify) |>
   306     map (apsnd (fn {prfx, exp, imp, wits, eqns, ...} => (prfx, (exp, imp), wits, eqns)));
   307 
   308   (* registrations that subsume t *)
   309   fun subsumers thy t regs =
   310     filter (fn (t', _) => Pattern.matches thy (t', t)) (dest_transfer thy regs);
   311 
   312   (* test if registration that subsumes the query is present *)
   313   fun test thy (regs, ts) =
   314     not (null (subsumers thy (termify ts) regs));
   315       
   316   (* look up registration, pick one that subsumes the query *)
   317   fun lookup thy (regs, (ts, ((impT, _), (imp, _)))) =
   318     let
   319       val t = termify ts;
   320       val subs = subsumers thy t regs;
   321     in
   322       (case subs of
   323         [] => NONE
   324         | ((t', {prfx, exp = exp', imp = ((impT', domT'), (imp', dom')), wits, eqns, morph}) :: _) =>
   325           let
   326             val (tinst, inst) = Pattern.match thy (t', t) (Vartab.empty, Vartab.empty);
   327             val tinst' = domT' |> map (fn (T as TFree (x, _)) =>
   328                 (x, T |> Morphism.typ exp' |> Envir.typ_subst_TVars tinst
   329                       |> var_instT_type impT)) |> Symtab.make;
   330             val inst' = dom' |> map (fn (t as Free (x, _)) =>
   331                 (x, t |> Morphism.term exp' |> Envir.subst_vars (tinst, inst)
   332                       |> var_inst_term (impT, imp))) |> Symtab.make;
   333             val inst'_morph = Element.inst_morphism thy (tinst', inst');
   334           in SOME (prfx,
   335             map (Element.morph_witness inst'_morph) wits,
   336             Termtab.map (Morphism.thm inst'_morph) eqns)
   337           end)
   338     end;
   339 
   340   (* add registration if not subsumed by ones already present,
   341      additionally returns registrations that are strictly subsumed *)
   342   fun insert thy ts prfx (exp, imp) regs =
   343     let
   344       val t = termify ts;
   345       val subs = subsumers thy t regs ;
   346     in (case subs of
   347         [] => let
   348                 val sups =
   349                   filter (fn (t', _) => Pattern.matches thy (t, t')) (dest_transfer thy regs);
   350                 val sups' = map (apfst untermify) sups |> map (fn (ts, {prfx, wits, ...}) => (ts, (prfx, wits)))
   351               in (Termtab.update (t, mk_reg prfx exp imp [] Termtab.empty ()) regs, sups') end
   352       | _ => (regs, []))
   353     end;
   354 
   355   fun gen_add f ts regs =
   356     let
   357       val t = termify ts;
   358     in
   359       Termtab.update (t, map_reg f (the (Termtab.lookup regs t))) regs
   360     end;
   361 
   362   (* add witness theorem to registration,
   363      only if instantiation is exact, otherwise exception Option raised *)
   364   fun add_witness ts wit regs =
   365     gen_add (fn (x, e, i, wits, eqns, m) => (x, e, i, Element.close_witness wit :: wits, eqns, m))
   366       ts regs;
   367 
   368   (* add equation to registration, replaces previous equation with same lhs;
   369      only if instantiation is exact, otherwise exception Option raised;
   370      exception TERM raised if not a meta equality *)
   371   fun add_equation ts thm regs =
   372     gen_add (fn (x, e, i, thms, eqns, m) =>
   373       (x, e, i, thms, Termtab.update (thm |> prop_of |> Logic.dest_equals |> fst, Thm.close_derivation thm) eqns, m))
   374       ts regs;
   375 
   376 end;
   377 
   378 
   379 (** theory data : locales **)
   380 
   381 structure LocalesData = TheoryDataFun
   382 (
   383   type T = NameSpace.T * locale Symtab.table;
   384     (* 1st entry: locale namespace,
   385        2nd entry: locales of the theory *)
   386 
   387   val empty = (NameSpace.empty, Symtab.empty);
   388   val copy = I;
   389   val extend = I;
   390 
   391   fun join_locales _
   392     ({axiom, elems, params, decls = (decls1, decls2), regs, intros, dests}: locale,
   393       {elems = elems', decls = (decls1', decls2'), regs = regs', ...}: locale) =
   394      {axiom = axiom,
   395       elems = merge_lists (eq_snd (op =)) elems elems',
   396       params = params,
   397       decls =
   398        (Library.merge (eq_snd (op =)) (decls1, decls1'),
   399         Library.merge (eq_snd (op =)) (decls2, decls2')),
   400       regs = merge_alists (op =) regs regs',
   401       intros = intros,
   402       dests = dests};
   403   fun merge _ ((space1, locs1), (space2, locs2)) =
   404     (NameSpace.merge (space1, space2), Symtab.join join_locales (locs1, locs2));
   405 );
   406 
   407 
   408 
   409 (** context data : registrations **)
   410 
   411 structure RegistrationsData = GenericDataFun
   412 (
   413   type T = Registrations.T Symtab.table;  (*registrations, indexed by locale name*)
   414   val empty = Symtab.empty;
   415   val extend = I;
   416   fun merge _ = Symtab.join (K Registrations.join);
   417 );
   418 
   419 
   420 (** access locales **)
   421 
   422 val intern = NameSpace.intern o #1 o LocalesData.get;
   423 val extern = NameSpace.extern o #1 o LocalesData.get;
   424 
   425 fun get_locale thy name = Symtab.lookup (#2 (LocalesData.get thy)) name;
   426 
   427 fun the_locale thy name = case get_locale thy name
   428  of SOME loc => loc
   429   | NONE => error ("Unknown locale " ^ quote name);
   430 
   431 fun register_locale name loc thy =
   432   thy |> LocalesData.map (fn (space, locs) =>
   433     (Sign.declare_name thy name space, Symtab.update (name, loc) locs));
   434 
   435 fun change_locale name f thy =
   436   let
   437     val {axiom, elems, params, decls, regs, intros, dests} =
   438         the_locale thy name;
   439     val (axiom', elems', params', decls', regs', intros', dests') =
   440       f (axiom, elems, params, decls, regs, intros, dests);
   441   in
   442     thy
   443     |> (LocalesData.map o apsnd) (Symtab.update (name, {axiom = axiom',
   444           elems = elems', params = params',
   445           decls = decls', regs = regs', intros = intros', dests = dests'}))
   446   end;
   447 
   448 fun print_locales thy =
   449   let val (space, locs) = LocalesData.get thy in
   450     Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (space, locs)))
   451     |> Pretty.writeln
   452   end;
   453 
   454 
   455 (* access registrations *)
   456 
   457 (* retrieve registration from theory or context *)
   458 
   459 fun get_registrations ctxt name =
   460   case Symtab.lookup (RegistrationsData.get ctxt) name of
   461       NONE => []
   462     | SOME reg => Registrations.dest (Context.theory_of ctxt) reg;
   463 
   464 fun get_global_registrations thy = get_registrations (Context.Theory thy);
   465 fun get_local_registrations ctxt = get_registrations (Context.Proof ctxt);
   466 
   467 
   468 fun get_registration ctxt imprt (name, ps) =
   469   case Symtab.lookup (RegistrationsData.get ctxt) name of
   470       NONE => NONE
   471     | SOME reg => Registrations.lookup (Context.theory_of ctxt) (reg, (ps, imprt));
   472 
   473 fun get_global_registration thy = get_registration (Context.Theory thy);
   474 fun get_local_registration ctxt = get_registration (Context.Proof ctxt);
   475 
   476 
   477 fun test_registration ctxt (name, ps) =
   478   case Symtab.lookup (RegistrationsData.get ctxt) name of
   479       NONE => false
   480     | SOME reg => Registrations.test (Context.theory_of ctxt) (reg, ps);
   481 
   482 fun test_global_registration thy = test_registration (Context.Theory thy);
   483 fun test_local_registration ctxt = test_registration (Context.Proof ctxt);
   484 
   485 
   486 (* add registration to theory or context, ignored if subsumed *)
   487 
   488 fun put_registration (name, ps) prfx morphs ctxt =
   489   RegistrationsData.map (fn regs =>
   490     let
   491       val thy = Context.theory_of ctxt;
   492       val reg = the_default Registrations.empty (Symtab.lookup regs name);
   493       val (reg', sups) = Registrations.insert thy ps prfx morphs reg;
   494       val _ = if not (null sups) then warning
   495                 ("Subsumed interpretation(s) of locale " ^
   496                  quote (extern thy name) ^
   497                  "\nwith the following prefix(es):" ^
   498                   commas_quote (map (fn (_, ((_, (_, s)), _)) => s) sups))
   499               else ();
   500     in Symtab.update (name, reg') regs end) ctxt;
   501 
   502 fun put_global_registration id prfx morphs =
   503   Context.theory_map (put_registration id prfx morphs);
   504 fun put_local_registration id prfx morphs =
   505   Context.proof_map (put_registration id prfx morphs);
   506 
   507 fun put_registration_in_locale name id =
   508   change_locale name (fn (axiom, elems, params, decls, regs, intros, dests) =>
   509     (axiom, elems, params, decls, regs @ [(id, [])], intros, dests));
   510 
   511 
   512 (* add witness theorem to registration, ignored if registration not present *)
   513 
   514 fun add_witness (name, ps) thm =
   515   RegistrationsData.map (Symtab.map_entry name (Registrations.add_witness ps thm));
   516 
   517 fun add_global_witness id thm = Context.theory_map (add_witness id thm);
   518 fun add_local_witness id thm = Context.proof_map (add_witness id thm);
   519 
   520 
   521 fun add_witness_in_locale name id thm =
   522   change_locale name (fn (axiom, elems, params, decls, regs, intros, dests) =>
   523     let
   524       fun add (id', thms) =
   525         if id = id' then (id', thm :: thms) else (id', thms);
   526     in (axiom, elems, params, decls, map add regs, intros, dests) end);
   527 
   528 
   529 (* add equation to registration, ignored if registration not present *)
   530 
   531 fun add_equation (name, ps) thm =
   532   RegistrationsData.map (Symtab.map_entry name (Registrations.add_equation ps thm));
   533 
   534 fun add_global_equation id thm = Context.theory_map (add_equation id thm);
   535 fun add_local_equation id thm = Context.proof_map (add_equation id thm);
   536 
   537 (*
   538 (* update morphism of registration, ignored if registration not present *)
   539 
   540 fun update_morph (name, ps) morph =
   541   RegistrationsData.map (Symtab.map_entry name (Registrations.update_morph ps morph));
   542 
   543 fun update_global_morph id morph = Context.theory_map (update_morph id morph);
   544 fun update_local_morph id morph = Context.proof_map (update_morph id morph);
   545 *)
   546 
   547 
   548 (* printing of registrations *)
   549 
   550 fun print_registrations show_wits loc ctxt =
   551   let
   552     val thy = ProofContext.theory_of ctxt;
   553     val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
   554     fun prt_term' t = if !show_types
   555           then Pretty.block [prt_term t, Pretty.brk 1, Pretty.str "::",
   556             Pretty.brk 1, (Pretty.quote o Syntax.pretty_typ ctxt) (type_of t)]
   557           else prt_term t;
   558     val prt_thm = prt_term o prop_of;
   559     fun prt_inst ts =
   560         Pretty.enclose "(" ")" (Pretty.breaks (map prt_term' ts));
   561     fun prt_prfx ((false, prfx), param_prfx) = [Pretty.str prfx, Pretty.brk 1, Pretty.str "(optional)", Pretty.brk 1, Pretty.str param_prfx]
   562       | prt_prfx ((true, prfx), param_prfx) = [Pretty.str prfx, Pretty.brk 1, Pretty.str param_prfx];
   563     fun prt_eqns [] = Pretty.str "no equations."
   564       | prt_eqns eqns = Pretty.block (Pretty.str "equations:" :: Pretty.brk 1 ::
   565           Pretty.breaks (map prt_thm eqns));
   566     fun prt_core ts eqns =
   567           [prt_inst ts, Pretty.fbrk, prt_eqns (Termtab.dest eqns |> map snd)];
   568     fun prt_witns [] = Pretty.str "no witnesses."
   569       | prt_witns witns = Pretty.block (Pretty.str "witnesses:" :: Pretty.brk 1 ::
   570           Pretty.breaks (map (Element.pretty_witness ctxt) witns))
   571     fun prt_reg (ts, (_, _, witns, eqns)) =
   572         if show_wits
   573           then Pretty.block (prt_core ts eqns @ [Pretty.fbrk, prt_witns witns])
   574           else Pretty.block (prt_core ts eqns)
   575 
   576     val loc_int = intern thy loc;
   577     val regs = RegistrationsData.get (Context.Proof ctxt);
   578     val loc_regs = Symtab.lookup regs loc_int;
   579   in
   580     (case loc_regs of
   581         NONE => Pretty.str ("no interpretations")
   582       | SOME r => let
   583             val r' = Registrations.dest thy r;
   584             val r'' = Library.sort_wrt (fn (_, ((_, (_, prfx)), _, _, _)) => prfx) r';
   585           in Pretty.big_list ("interpretations:") (map prt_reg r'') end)
   586     |> Pretty.writeln
   587   end;
   588 
   589 
   590 (* diagnostics *)
   591 
   592 fun err_in_locale ctxt msg ids =
   593   let
   594     val thy = ProofContext.theory_of ctxt;
   595     fun prt_id (name, parms) =
   596       [Pretty.block (Pretty.breaks (map Pretty.str (extern thy name :: parms)))];
   597     val prt_ids = flat (separate [Pretty.str " +", Pretty.brk 1] (map prt_id ids));
   598     val err_msg =
   599       if forall (fn (s, _) => s = "") ids then msg
   600       else msg ^ "\n" ^ Pretty.string_of (Pretty.block
   601         (Pretty.str "The error(s) above occurred in locale:" :: Pretty.brk 1 :: prt_ids));
   602   in error err_msg end;
   603 
   604 fun err_in_locale' ctxt msg ids' = err_in_locale ctxt msg (map fst ids');
   605 
   606 
   607 fun pretty_ren NONE = Pretty.str "_"
   608   | pretty_ren (SOME (x, NONE)) = Pretty.str x
   609   | pretty_ren (SOME (x, SOME syn)) =
   610       Pretty.block [Pretty.str x, Pretty.brk 1, Syntax.pretty_mixfix syn];
   611 
   612 fun pretty_expr thy (Locale name) = Pretty.str (extern thy name)
   613   | pretty_expr thy (Rename (expr, xs)) =
   614       Pretty.block [pretty_expr thy expr, Pretty.brk 1, Pretty.block (map pretty_ren xs |> Pretty.breaks)]
   615   | pretty_expr thy (Merge es) =
   616       Pretty.separate "+" (map (pretty_expr thy) es) |> Pretty.block;
   617 
   618 fun err_in_expr _ msg (Merge []) = error msg
   619   | err_in_expr ctxt msg expr =
   620     error (msg ^ "\n" ^ Pretty.string_of (Pretty.block
   621       [Pretty.str "The error(s) above occured in locale expression:", Pretty.brk 1,
   622        pretty_expr (ProofContext.theory_of ctxt) expr]));
   623 
   624 
   625 (** structured contexts: rename + merge + implicit type instantiation **)
   626 
   627 (* parameter types *)
   628 
   629 fun frozen_tvars ctxt Ts =
   630   #1 (Variable.importT_inst (map Logic.mk_type Ts) ctxt)
   631   |> map (fn ((xi, S), T) => (xi, (S, T)));
   632 
   633 fun unify_frozen ctxt maxidx Ts Us =
   634   let
   635     fun paramify NONE i = (NONE, i)
   636       | paramify (SOME T) i = apfst SOME (TypeInfer.paramify_dummies T i);
   637 
   638     val (Ts', maxidx') = fold_map paramify Ts maxidx;
   639     val (Us', maxidx'') = fold_map paramify Us maxidx';
   640     val thy = ProofContext.theory_of ctxt;
   641 
   642     fun unify (SOME T, SOME U) env = (Sign.typ_unify thy (U, T) env
   643           handle Type.TUNIFY => raise TYPE ("unify_frozen: failed to unify types", [U, T], []))
   644       | unify _ env = env;
   645     val (unifier, _) = fold unify (Ts' ~~ Us') (Vartab.empty, maxidx'');
   646     val Vs = map (Option.map (Envir.norm_type unifier)) Us';
   647     val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map_filter I Vs));
   648   in map (Option.map (Envir.norm_type unifier')) Vs end;
   649 
   650 fun params_of elemss =
   651   distinct (eq_fst (op = : string * string -> bool)) (maps (snd o fst) elemss);
   652 
   653 fun params_of' elemss =
   654   distinct (eq_fst (op = : string * string -> bool)) (maps (snd o fst o fst) elemss);
   655 
   656 fun param_prefix locale_name params = (NameSpace.base locale_name ^ "_locale", space_implode "_" params);
   657 
   658 
   659 (* CB: param_types has the following type:
   660   ('a * 'b option) list -> ('a * 'b) list *)
   661 fun param_types ps = map_filter (fn (_, NONE) => NONE | (x, SOME T) => SOME (x, T)) ps;
   662 
   663 
   664 fun merge_syntax ctxt ids ss = Symtab.merge (op = : mixfix * mixfix -> bool) ss
   665   handle Symtab.DUP x => err_in_locale ctxt
   666     ("Conflicting syntax for parameter: " ^ quote x) (map fst ids);
   667 
   668 
   669 (* Distinction of assumed vs. derived identifiers.
   670    The former may have axioms relating assumptions of the context to
   671    assumptions of the specification fragment (for locales with
   672    predicates).  The latter have witnesses relating assumptions of the
   673    specification fragment to assumptions of other (assumed) specification
   674    fragments. *)
   675 
   676 datatype 'a mode = Assumed of 'a | Derived of 'a;
   677 
   678 fun map_mode f (Assumed x) = Assumed (f x)
   679   | map_mode f (Derived x) = Derived (f x);
   680 
   681 
   682 (* flatten expressions *)
   683 
   684 local
   685 
   686 fun unify_parms ctxt fixed_parms raw_parmss =
   687   let
   688     val thy = ProofContext.theory_of ctxt;
   689     val maxidx = length raw_parmss;
   690     val idx_parmss = (0 upto maxidx - 1) ~~ raw_parmss;
   691 
   692     fun varify i = Term.map_type_tfree (fn (a, S) => TVar ((a, i), S));
   693     fun varify_parms (i, ps) = map (apsnd (varify i)) (param_types ps);
   694     val parms = fixed_parms @ maps varify_parms idx_parmss;
   695 
   696     fun unify T U envir = Sign.typ_unify thy (U, T) envir
   697       handle Type.TUNIFY =>
   698         let
   699           val T' = Envir.norm_type (fst envir) T;
   700           val U' = Envir.norm_type (fst envir) U;
   701           val prt = Syntax.string_of_typ ctxt;
   702         in
   703           raise TYPE ("unify_parms: failed to unify types " ^
   704             prt U' ^ " and " ^ prt T', [U', T'], [])
   705         end;
   706     fun unify_list (T :: Us) = fold (unify T) Us
   707       | unify_list [] = I;
   708     val (unifier, _) = fold unify_list (map #2 (Symtab.dest (Symtab.make_list parms)))
   709       (Vartab.empty, maxidx);
   710 
   711     val parms' = map (apsnd (Envir.norm_type unifier)) (distinct (eq_fst (op =)) parms);
   712     val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map #2 parms'));
   713 
   714     fun inst_parms (i, ps) =
   715       List.foldr Term.add_typ_tfrees [] (map_filter snd ps)
   716       |> map_filter (fn (a, S) =>
   717           let val T = Envir.norm_type unifier' (TVar ((a, i), S))
   718           in if T = TFree (a, S) then NONE else SOME (a, T) end)
   719       |> Symtab.make;
   720   in map inst_parms idx_parmss end;
   721 
   722 in
   723 
   724 fun unify_elemss _ _ [] = []
   725   | unify_elemss _ [] [elems] = [elems]
   726   | unify_elemss ctxt fixed_parms elemss =
   727       let
   728         val thy = ProofContext.theory_of ctxt;
   729         val phis = unify_parms ctxt fixed_parms (map (snd o fst o fst) elemss)
   730           |> map (Element.instT_morphism thy);
   731         fun inst ((((name, ps), mode), elems), phi) =
   732           (((name, map (apsnd (Option.map (Morphism.typ phi))) ps),
   733               map_mode (map (Element.morph_witness phi)) mode),
   734             map (Element.morph_ctxt phi) elems);
   735       in map inst (elemss ~~ phis) end;
   736 
   737 
   738 fun renaming xs parms = zip_options parms xs
   739   handle Library.UnequalLengths =>
   740     error ("Too many arguments in renaming: " ^
   741       commas (map (fn NONE => "_" | SOME x => quote (fst x)) xs));
   742 
   743 
   744 (* params_of_expr:
   745    Compute parameters (with types and syntax) of locale expression.
   746 *)
   747 
   748 fun params_of_expr ctxt fixed_params expr (prev_parms, prev_types, prev_syn) =
   749   let
   750     val thy = ProofContext.theory_of ctxt;
   751 
   752     fun merge_tenvs fixed tenv1 tenv2 =
   753         let
   754           val [env1, env2] = unify_parms ctxt fixed
   755                 [tenv1 |> Symtab.dest |> map (apsnd SOME),
   756                  tenv2 |> Symtab.dest |> map (apsnd SOME)]
   757         in
   758           Symtab.merge (op =) (Symtab.map (Element.instT_type env1) tenv1,
   759             Symtab.map (Element.instT_type env2) tenv2)
   760         end;
   761 
   762     fun merge_syn expr syn1 syn2 =
   763         Symtab.merge (op = : mixfix * mixfix -> bool) (syn1, syn2)
   764         handle Symtab.DUP x => err_in_expr ctxt
   765           ("Conflicting syntax for parameter: " ^ quote x) expr;
   766 
   767     fun params_of (expr as Locale name) =
   768           let
   769             val {params, ...} = the_locale thy name;
   770           in (map (fst o fst) params, params |> map fst |> Symtab.make,
   771                params |> map (apfst fst) |> Symtab.make) end
   772       | params_of (expr as Rename (e, xs)) =
   773           let
   774             val (parms', types', syn') = params_of e;
   775             val ren = renaming xs parms';
   776             (* renaming may reduce number of parameters *)
   777             val new_parms = map (Element.rename ren) parms' |> distinct (op =);
   778             val ren_syn = syn' |> Symtab.dest |> map (Element.rename_var_name ren);
   779             val new_syn = fold (Symtab.insert (op =)) ren_syn Symtab.empty
   780                 handle Symtab.DUP x =>
   781                   err_in_expr ctxt ("Conflicting syntax for parameter: " ^ quote x) expr;
   782             val syn_types = map (apsnd (fn mx =>
   783                 SOME (Type.freeze_type (#1 (TypeInfer.paramify_dummies (Syntax.mixfixT mx) 0)))))
   784               (Symtab.dest new_syn);
   785             val ren_types = types' |> Symtab.dest |> map (apfst (Element.rename ren));
   786             val (env :: _) = unify_parms ctxt []
   787                 ((ren_types |> map (apsnd SOME)) :: map single syn_types);
   788             val new_types = fold (Symtab.insert (op =))
   789                 (map (apsnd (Element.instT_type env)) ren_types) Symtab.empty;
   790           in (new_parms, new_types, new_syn) end
   791       | params_of (Merge es) =
   792           fold (fn e => fn (parms, types, syn) =>
   793                    let
   794                      val (parms', types', syn') = params_of e
   795                    in
   796                      (merge_lists (op =) parms parms', merge_tenvs [] types types',
   797                       merge_syn e syn syn')
   798                    end)
   799             es ([], Symtab.empty, Symtab.empty)
   800 
   801       val (parms, types, syn) = params_of expr;
   802     in
   803       (merge_lists (op =) prev_parms parms, merge_tenvs fixed_params prev_types types,
   804        merge_syn expr prev_syn syn)
   805     end;
   806 
   807 fun make_params_ids params = [(("", params), ([], Assumed []))];
   808 fun make_raw_params_elemss (params, tenv, syn) =
   809     [((("", map (fn p => (p, Symtab.lookup tenv p)) params), Assumed []),
   810       Int [Fixes (map (fn p =>
   811         (Name.binding p, Symtab.lookup tenv p, Symtab.lookup syn p |> the)) params)])];
   812 
   813 
   814 (* flatten_expr:
   815    Extend list of identifiers by those new in locale expression expr.
   816    Compute corresponding list of lists of locale elements (one entry per
   817    identifier).
   818 
   819    Identifiers represent locale fragments and are in an extended form:
   820      ((name, ps), (ax_ps, axs))
   821    (name, ps) is the locale name with all its parameters.
   822    (ax_ps, axs) is the locale axioms with its parameters;
   823      axs are always taken from the top level of the locale hierarchy,
   824      hence axioms may contain additional parameters from later fragments:
   825      ps subset of ax_ps.  axs is either singleton or empty.
   826 
   827    Elements are enriched by identifier-like information:
   828      (((name, ax_ps), axs), elems)
   829    The parameters in ax_ps are the axiom parameters, but enriched by type
   830    info: now each entry is a pair of string and typ option.  Axioms are
   831    type-instantiated.
   832 
   833 *)
   834 
   835 fun flatten_expr ctxt ((prev_idents, prev_syntax), expr) =
   836   let
   837     val thy = ProofContext.theory_of ctxt;
   838 
   839     fun rename_parms top ren ((name, ps), (parms, mode)) =
   840         ((name, map (Element.rename ren) ps),
   841          if top
   842          then (map (Element.rename ren) parms,
   843                map_mode (map (Element.morph_witness (Element.rename_morphism ren))) mode)
   844          else (parms, mode));
   845 
   846     (* add (name, pTs) and its registrations, recursively; adjust hyps of witnesses *)
   847 
   848     fun add_with_regs ((name, pTs), mode) (wits, ids, visited) =
   849         if member (fn (a, (b, _)) => a = b) visited (name, map #1 pTs)
   850         then (wits, ids, visited)
   851         else
   852           let
   853             val {params, regs, ...} = the_locale thy name;
   854             val pTs' = map #1 params;
   855             val ren = map #1 pTs' ~~ map (fn (x, _) => (x, NONE)) pTs;
   856               (* dummy syntax, since required by rename *)
   857             val pTs'' = map (fn ((p, _), (_, T)) => (p, T)) (pTs ~~ pTs');
   858             val [env] = unify_parms ctxt pTs [map (apsnd SOME) pTs''];
   859               (* propagate parameter types, to keep them consistent *)
   860             val regs' = map (fn ((name, ps), wits) =>
   861                 ((name, map (Element.rename ren) ps),
   862                  map (Element.transfer_witness thy) wits)) regs;
   863             val new_regs = regs';
   864             val new_ids = map fst new_regs;
   865             val new_idTs =
   866               map (apsnd (map (fn p => (p, (the o AList.lookup (op =) pTs) p)))) new_ids;
   867 
   868             val new_wits = new_regs |> map (#2 #> map
   869               (Element.morph_witness
   870                 (Element.instT_morphism thy env $>
   871                   Element.rename_morphism ren $>
   872                   Element.satisfy_morphism wits)
   873                 #> Element.close_witness));
   874             val new_ids' = map (fn (id, wits) =>
   875                 (id, ([], Derived wits))) (new_ids ~~ new_wits);
   876             val new_idTs' = map (fn ((n, pTs), (_, ([], mode))) =>
   877                 ((n, pTs), mode)) (new_idTs ~~ new_ids');
   878             val new_id = ((name, map #1 pTs), ([], mode));
   879             val (wits', ids', visited') = fold add_with_regs new_idTs'
   880               (wits @ flat new_wits, ids, visited @ [new_id]);
   881           in
   882             (wits', ids' @ [new_id], visited')
   883           end;
   884 
   885     (* distribute top-level axioms over assumed ids *)
   886 
   887     fun axiomify all_ps ((name, parms), (_, Assumed _)) axioms =
   888         let
   889           val {elems, ...} = the_locale thy name;
   890           val ts = maps
   891             (fn (Assumes asms, _) => maps (map #1 o #2) asms
   892               | _ => [])
   893             elems;
   894           val (axs1, axs2) = chop (length ts) axioms;
   895         in (((name, parms), (all_ps, Assumed axs1)), axs2) end
   896       | axiomify all_ps (id, (_, Derived ths)) axioms =
   897           ((id, (all_ps, Derived ths)), axioms);
   898 
   899     (* identifiers of an expression *)
   900 
   901     fun identify top (Locale name) =
   902     (* CB: ids_ax is a list of tuples of the form ((name, ps), axs),
   903        where name is a locale name, ps a list of parameter names and axs
   904        a list of axioms relating to the identifier, axs is empty unless
   905        identify at top level (top = true);
   906        parms is accumulated list of parameters *)
   907           let
   908             val {axiom, params, ...} = the_locale thy name;
   909             val ps = map (#1 o #1) params;
   910             val (_, ids'', _) = add_with_regs ((name, map #1 params), Assumed []) ([], [], []);
   911             val ids_ax = if top then fst (fold_map (axiomify ps) ids'' axiom) else ids'';
   912             in (ids_ax, ps) end
   913       | identify top (Rename (e, xs)) =
   914           let
   915             val (ids', parms') = identify top e;
   916             val ren = renaming xs parms'
   917               handle ERROR msg => err_in_locale' ctxt msg ids';
   918 
   919             val ids'' = distinct (eq_fst (op =)) (map (rename_parms top ren) ids');
   920             val parms'' = distinct (op =) (maps (#2 o #1) ids'');
   921           in (ids'', parms'') end
   922       | identify top (Merge es) =
   923           fold (fn e => fn (ids, parms) =>
   924                    let
   925                      val (ids', parms') = identify top e
   926                    in
   927                      (merge_alists (op =) ids ids', merge_lists (op =) parms parms')
   928                    end)
   929             es ([], []);
   930 
   931     fun inst_wit all_params (t, th) = let
   932          val {hyps, prop, ...} = Thm.rep_thm th;
   933          val ps = map (apsnd SOME) (fold Term.add_frees (prop :: hyps) []);
   934          val [env] = unify_parms ctxt all_params [ps];
   935          val t' = Element.instT_term env t;
   936          val th' = Element.instT_thm thy env th;
   937        in (t', th') end;
   938 
   939     fun eval all_params tenv syn ((name, params), (locale_params, mode)) =
   940       let
   941         val {params = ps_mx, elems = elems_stamped, ...} = the_locale thy name;
   942         val elems = map fst elems_stamped;
   943         val ps = map fst ps_mx;
   944         fun lookup_syn x = (case Symtab.lookup syn x of SOME Structure => NONE | opt => opt);
   945         val locale_params' = map (fn p => (p, Symtab.lookup tenv p |> the)) locale_params;
   946         val mode' = map_mode (map (Element.map_witness (inst_wit all_params))) mode;
   947         val ren = map fst ps ~~ map (fn p => (p, lookup_syn p)) params;
   948         val [env] = unify_parms ctxt all_params [map (apfst (Element.rename ren) o apsnd SOME) ps];
   949         val (lprfx, pprfx) = param_prefix name params;
   950         val add_prefices = pprfx <> "" ? Binding.add_prefix false pprfx
   951           #> Binding.add_prefix false lprfx;
   952         val elem_morphism =
   953           Element.rename_morphism ren $>
   954           Morphism.name_morphism add_prefices $>
   955           Element.instT_morphism thy env;
   956         val elems' = map (Element.morph_ctxt elem_morphism) elems;
   957       in (((name, map (apsnd SOME) locale_params'), mode'), elems') end;
   958 
   959     (* parameters, their types and syntax *)
   960     val (all_params', tenv, syn) = params_of_expr ctxt [] expr ([], Symtab.empty, Symtab.empty);
   961     val all_params = map (fn p => (p, Symtab.lookup tenv p |> the)) all_params';
   962     (* compute identifiers and syntax, merge with previous ones *)
   963     val (ids, _) = identify true expr;
   964     val idents = subtract (eq_fst (op =)) prev_idents ids;
   965     val syntax = merge_syntax ctxt ids (syn, prev_syntax);
   966     (* type-instantiate elements *)
   967     val final_elemss = map (eval all_params tenv syntax) idents;
   968   in ((prev_idents @ idents, syntax), final_elemss) end;
   969 
   970 end;
   971 
   972 
   973 (* activate elements *)
   974 
   975 local
   976 
   977 fun axioms_export axs _ As =
   978   (Element.satisfy_thm axs #> Drule.implies_intr_list (Library.drop (length axs, As)), fn t => t);
   979 
   980 
   981 (* NB: derived ids contain only facts at this stage *)
   982 
   983 fun activate_elem _ _ (Fixes fixes) (ctxt, mode) =
   984       ([], (ctxt |> ProofContext.add_fixes_i fixes |> snd, mode))
   985   | activate_elem _ _ (Constrains _) (ctxt, mode) =
   986       ([], (ctxt, mode))
   987   | activate_elem ax_in_ctxt _ (Assumes asms) (ctxt, Assumed axs) =
   988       let
   989         val asms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) asms;
   990         val ts = maps (map #1 o #2) asms';
   991         val (ps, qs) = chop (length ts) axs;
   992         val (_, ctxt') =
   993           ctxt |> fold Variable.auto_fixes ts
   994           |> ProofContext.add_assms_i (axioms_export (if ax_in_ctxt then ps else [])) asms';
   995       in ([], (ctxt', Assumed qs)) end
   996   | activate_elem _ _ (Assumes asms) (ctxt, Derived ths) =
   997       ([], (ctxt, Derived ths))
   998   | activate_elem _ _ (Defines defs) (ctxt, Assumed axs) =
   999       let
  1000         val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
  1001         val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
  1002             let val ((c, _), t') = LocalDefs.cert_def ctxt t
  1003             in (t', ((Name.map_name (Thm.def_name_optional c) name, atts), [(t', ps)])) end);
  1004         val (_, ctxt') =
  1005           ctxt |> fold (Variable.auto_fixes o #1) asms
  1006           |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms);
  1007       in ([], (ctxt', Assumed axs)) end
  1008   | activate_elem _ _ (Defines defs) (ctxt, Derived ths) =
  1009       ([], (ctxt, Derived ths))
  1010   | activate_elem _ is_ext (Notes (kind, facts)) (ctxt, mode) =
  1011       let
  1012         val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts;
  1013         val (res, ctxt') = ctxt |> local_note_qualified kind facts';
  1014       in (if is_ext then (map (#1 o #1) facts' ~~ map #2 res) else [], (ctxt', mode)) end;
  1015 
  1016 fun activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt =
  1017   let
  1018     val thy = ProofContext.theory_of ctxt;
  1019     val (res, (ctxt', _)) = fold_map (activate_elem ax_in_ctxt (name = ""))
  1020         elems (ProofContext.qualified_names ctxt, mode)
  1021       handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)];
  1022     val ctxt'' = if name = "" then ctxt'
  1023           else let
  1024               val ps' = map (fn (n, SOME T) => Free (n, T)) ps;
  1025             in if test_local_registration ctxt' (name, ps') then ctxt'
  1026               else let
  1027                   val ctxt'' = put_local_registration (name, ps') (I, (NameSpace.base name, ""))
  1028                     (Morphism.identity, ((Vartab.empty, []), (Vartab.empty, []) )) ctxt'
  1029                 in case mode of
  1030                     Assumed axs =>
  1031                       fold (add_local_witness (name, ps') o
  1032                         Element.assume_witness thy o Element.witness_prop) axs ctxt''
  1033                   | Derived ths =>
  1034                      fold (add_local_witness (name, ps')) ths ctxt''
  1035                 end
  1036             end
  1037   in (ProofContext.restore_naming ctxt ctxt'', res) end;
  1038 
  1039 fun activate_elemss ax_in_ctxt prep_facts =
  1040     fold_map (fn (((name, ps), mode), raw_elems) => fn ctxt =>
  1041       let
  1042         val elems = map (prep_facts ctxt) raw_elems;
  1043         val (ctxt', res) = apsnd flat
  1044             (activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt);
  1045         val elems' = elems |> map (Element.map_ctxt_attrib Args.closure);
  1046       in (((((name, ps), mode), elems'), res), ctxt') end);
  1047 
  1048 in
  1049 
  1050 (* CB: activate_facts prep_facts elemss ctxt,
  1051    where elemss is a list of pairs consisting of identifiers and
  1052    context elements, extends ctxt by the context elements yielding
  1053    ctxt' and returns ((elemss', facts), ctxt').
  1054    Identifiers in the argument are of the form ((name, ps), axs) and
  1055    assumptions use the axioms in the identifiers to set up exporters
  1056    in ctxt'.  elemss' does not contain identifiers and is obtained
  1057    from elemss and the intermediate context with prep_facts.
  1058    If read_facts or cert_facts is used for prep_facts, these also remove
  1059    the internal/external markers from elemss. *)
  1060 
  1061 fun activate_facts ax_in_ctxt prep_facts args =
  1062   activate_elemss ax_in_ctxt prep_facts args
  1063   #>> (apsnd flat o split_list);
  1064 
  1065 end;
  1066 
  1067 
  1068 
  1069 (** prepare locale elements **)
  1070 
  1071 (* expressions *)
  1072 
  1073 fun intern_expr thy (Locale xname) = Locale (intern thy xname)
  1074   | intern_expr thy (Merge exprs) = Merge (map (intern_expr thy) exprs)
  1075   | intern_expr thy (Rename (expr, xs)) = Rename (intern_expr thy expr, xs);
  1076 
  1077 
  1078 (* propositions and bindings *)
  1079 
  1080 (* flatten (ctxt, prep_expr) ((ids, syn), expr)
  1081    normalises expr (which is either a locale
  1082    expression or a single context element) wrt.
  1083    to the list ids of already accumulated identifiers.
  1084    It returns ((ids', syn'), elemss) where ids' is an extension of ids
  1085    with identifiers generated for expr, and elemss is the list of
  1086    context elements generated from expr.
  1087    syn and syn' are symtabs mapping parameter names to their syntax.  syn'
  1088    is an extension of syn.
  1089    For details, see flatten_expr.
  1090 
  1091    Additionally, for a locale expression, the elems are grouped into a single
  1092    Int; individual context elements are marked Ext.  In this case, the
  1093    identifier-like information of the element is as follows:
  1094    - for Fixes: (("", ps), []) where the ps have type info NONE
  1095    - for other elements: (("", []), []).
  1096    The implementation of activate_facts relies on identifier names being
  1097    empty strings for external elements.
  1098 *)
  1099 
  1100 fun flatten (ctxt, _) ((ids, syn), Elem (Fixes fixes)) = let
  1101         val ids' = ids @ [(("", map (Name.name_of o #1) fixes), ([], Assumed []))]
  1102       in
  1103         ((ids',
  1104          merge_syntax ctxt ids'
  1105            (syn, Symtab.make (map (fn fx => (Name.name_of (#1 fx), #3 fx)) fixes))
  1106            handle Symtab.DUP x => err_in_locale ctxt
  1107              ("Conflicting syntax for parameter: " ^ quote x)
  1108              (map #1 ids')),
  1109          [((("", map (rpair NONE o Name.name_of o #1) fixes), Assumed []), Ext (Fixes fixes))])
  1110       end
  1111   | flatten _ ((ids, syn), Elem elem) =
  1112       ((ids @ [(("", []), ([], Assumed []))], syn), [((("", []), Assumed []), Ext elem)])
  1113   | flatten (ctxt, prep_expr) ((ids, syn), Expr expr) =
  1114       apsnd (map (apsnd Int)) (flatten_expr ctxt ((ids, syn), prep_expr expr));
  1115 
  1116 local
  1117 
  1118 local
  1119 
  1120 fun declare_int_elem (Fixes fixes) ctxt =
  1121       ([], ctxt |> ProofContext.add_fixes_i (map (fn (x, T, mx) =>
  1122         (x, Option.map (Term.map_type_tfree (TypeInfer.param 0)) T, mx)) fixes) |> snd)
  1123   | declare_int_elem _ ctxt = ([], ctxt);
  1124 
  1125 fun declare_ext_elem prep_vars (Fixes fixes) ctxt =
  1126       let val (vars, _) = prep_vars fixes ctxt
  1127       in ([], ctxt |> ProofContext.add_fixes_i vars |> snd) end
  1128   | declare_ext_elem prep_vars (Constrains csts) ctxt =
  1129       let val (_, ctxt') = prep_vars (map (fn (x, T) => (Name.binding x, SOME T, NoSyn)) csts) ctxt
  1130       in ([], ctxt') end
  1131   | declare_ext_elem _ (Assumes asms) ctxt = (map #2 asms, ctxt)
  1132   | declare_ext_elem _ (Defines defs) ctxt = (map (fn (_, (t, ps)) => [(t, ps)]) defs, ctxt)
  1133   | declare_ext_elem _ (Notes _) ctxt = ([], ctxt);
  1134 
  1135 fun declare_elems prep_vars (((name, ps), Assumed _), elems) ctxt = ((case elems
  1136      of Int es => fold_map declare_int_elem es ctxt
  1137       | Ext e => declare_ext_elem prep_vars e ctxt |>> single)
  1138           handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)])
  1139   | declare_elems _ ((_, Derived _), elems) ctxt = ([], ctxt);
  1140 
  1141 in
  1142 
  1143 fun declare_elemss prep_vars fixed_params raw_elemss ctxt =
  1144   let
  1145     (* CB: fix of type bug of goal in target with context elements.
  1146        Parameters new in context elements must receive types that are
  1147        distinct from types of parameters in target (fixed_params).  *)
  1148     val ctxt_with_fixed = 
  1149       fold Variable.declare_term (map Free fixed_params) ctxt;
  1150     val int_elemss =
  1151       raw_elemss
  1152       |> map_filter (fn (id, Int es) => SOME (id, es) | _ => NONE)
  1153       |> unify_elemss ctxt_with_fixed fixed_params;
  1154     val (raw_elemss', _) =
  1155       fold_map (curry (fn ((id, Int _), (_, es) :: elemss) => ((id, Int es), elemss) | x => x))
  1156         raw_elemss int_elemss;
  1157   in fold_map (declare_elems prep_vars) raw_elemss' ctxt end;
  1158 
  1159 end;
  1160 
  1161 local
  1162 
  1163 val norm_term = Envir.beta_norm oo Term.subst_atomic;
  1164 
  1165 fun abstract_thm thy eq =
  1166   Thm.assume (Thm.cterm_of thy eq) |> Drule.gen_all |> Drule.abs_def;
  1167 
  1168 fun bind_def ctxt (name, ps) eq (xs, env, ths) =
  1169   let
  1170     val ((y, T), b) = LocalDefs.abs_def eq;
  1171     val b' = norm_term env b;
  1172     val th = abstract_thm (ProofContext.theory_of ctxt) eq;
  1173     fun err msg = err_in_locale ctxt (msg ^ ": " ^ quote y) [(name, map fst ps)];
  1174   in
  1175     exists (fn (x, _) => x = y) xs andalso
  1176       err "Attempt to define previously specified variable";
  1177     exists (fn (Free (y', _), _) => y = y' | _ => false) env andalso
  1178       err "Attempt to redefine variable";
  1179     (Term.add_frees b' xs, (Free (y, T), b') :: env, th :: ths)
  1180   end;
  1181 
  1182 
  1183 (* CB: for finish_elems (Int and Ext),
  1184    extracts specification, only of assumed elements *)
  1185 
  1186 fun eval_text _ _ _ (Fixes _) text = text
  1187   | eval_text _ _ _ (Constrains _) text = text
  1188   | eval_text _ (_, Assumed _) is_ext (Assumes asms)
  1189         (((exts, exts'), (ints, ints')), (xs, env, defs)) =
  1190       let
  1191         val ts = maps (map #1 o #2) asms;
  1192         val ts' = map (norm_term env) ts;
  1193         val spec' =
  1194           if is_ext then ((exts @ ts, exts' @ ts'), (ints, ints'))
  1195           else ((exts, exts'), (ints @ ts, ints' @ ts'));
  1196       in (spec', (fold Term.add_frees ts' xs, env, defs)) end
  1197   | eval_text _ (_, Derived _) _ (Assumes _) text = text
  1198   | eval_text ctxt (id, Assumed _) _ (Defines defs) (spec, binds) =
  1199       (spec, fold (bind_def ctxt id o #1 o #2) defs binds)
  1200   | eval_text _ (_, Derived _) _ (Defines _) text = text
  1201   | eval_text _ _ _ (Notes _) text = text;
  1202 
  1203 
  1204 (* for finish_elems (Int),
  1205    remove redundant elements of derived identifiers,
  1206    turn assumptions and definitions into facts,
  1207    satisfy hypotheses of facts *)
  1208 
  1209 fun finish_derived _ _ (Assumed _) (Fixes fixes) = SOME (Fixes fixes)
  1210   | finish_derived _ _ (Assumed _) (Constrains csts) = SOME (Constrains csts)
  1211   | finish_derived _ _ (Assumed _) (Assumes asms) = SOME (Assumes asms)
  1212   | finish_derived _ _ (Assumed _) (Defines defs) = SOME (Defines defs)
  1213 
  1214   | finish_derived _ _ (Derived _) (Fixes _) = NONE
  1215   | finish_derived _ _ (Derived _) (Constrains _) = NONE
  1216   | finish_derived sign satisfy (Derived _) (Assumes asms) = asms
  1217       |> map (apsnd (map (fn (a, _) => ([Thm.assume (cterm_of sign a)], []))))
  1218       |> pair Thm.assumptionK |> Notes
  1219       |> Element.morph_ctxt satisfy |> SOME
  1220   | finish_derived sign satisfy (Derived _) (Defines defs) = defs
  1221       |> map (apsnd (fn (d, _) => [([Thm.assume (cterm_of sign d)], [])]))
  1222       |> pair Thm.definitionK |> Notes
  1223       |> Element.morph_ctxt satisfy |> SOME
  1224 
  1225   | finish_derived _ satisfy _ (Notes facts) = Notes facts
  1226       |> Element.morph_ctxt satisfy |> SOME;
  1227 
  1228 (* CB: for finish_elems (Ext) *)
  1229 
  1230 fun closeup _ false elem = elem
  1231   | closeup ctxt true elem =
  1232       let
  1233         fun close_frees t =
  1234           let
  1235             val rev_frees =
  1236               Term.fold_aterms (fn Free (x, T) =>
  1237                 if Variable.is_fixed ctxt x then I else insert (op =) (x, T) | _ => I) t [];
  1238           in Term.list_all_free (rev rev_frees, t) end;
  1239 
  1240         fun no_binds [] = []
  1241           | no_binds _ = error "Illegal term bindings in locale element";
  1242       in
  1243         (case elem of
  1244           Assumes asms => Assumes (asms |> map (fn (a, propps) =>
  1245             (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps)))
  1246         | Defines defs => Defines (defs |> map (fn (a, (t, ps)) =>
  1247             (a, (close_frees (#2 (LocalDefs.cert_def ctxt t)), no_binds ps))))
  1248         | e => e)
  1249       end;
  1250 
  1251 
  1252 fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (b, _, mx) =>
  1253       let val x = Name.name_of b
  1254       in (b, AList.lookup (op =) parms x, mx) end) fixes)
  1255   | finish_ext_elem parms _ (Constrains _, _) = Constrains []
  1256   | finish_ext_elem _ close (Assumes asms, propp) =
  1257       close (Assumes (map #1 asms ~~ propp))
  1258   | finish_ext_elem _ close (Defines defs, propp) =
  1259       close (Defines (map #1 defs ~~ map (fn [(t, ps)] => (t, ps)) propp))
  1260   | finish_ext_elem _ _ (Notes facts, _) = Notes facts;
  1261 
  1262 
  1263 (* CB: finish_parms introduces type info from parms to identifiers *)
  1264 (* CB: only needed for types that have been NONE so far???
  1265    If so, which are these??? *)
  1266 
  1267 fun finish_parms parms (((name, ps), mode), elems) =
  1268   (((name, map (fn (x, _) => (x, AList.lookup (op = : string * string -> bool) parms x)) ps), mode), elems);
  1269 
  1270 fun finish_elems ctxt parms _ ((text, wits), ((id, Int e), _)) =
  1271       let
  1272         val [(id' as (_, mode), es)] = unify_elemss ctxt parms [(id, e)];
  1273         val wits' = case mode of Assumed _ => wits | Derived ths => wits @ ths;
  1274         val text' = fold (eval_text ctxt id' false) es text;
  1275         val es' = map_filter
  1276           (finish_derived (ProofContext.theory_of ctxt) (Element.satisfy_morphism wits') mode) es;
  1277       in ((text', wits'), (id', map Int es')) end
  1278   | finish_elems ctxt parms do_close ((text, wits), ((id, Ext e), [propp])) =
  1279       let
  1280         val e' = finish_ext_elem parms (closeup ctxt do_close) (e, propp);
  1281         val text' = eval_text ctxt id true e' text;
  1282       in ((text', wits), (id, [Ext e'])) end
  1283 
  1284 in
  1285 
  1286 (* CB: only called by prep_elemss *)
  1287 
  1288 fun finish_elemss ctxt parms do_close =
  1289   foldl_map (apsnd (finish_parms parms) o finish_elems ctxt parms do_close);
  1290 
  1291 end;
  1292 
  1293 
  1294 (* Remove duplicate Defines elements: temporary workaround to fix Afp/Category. *)
  1295 
  1296 fun defs_ord (defs1, defs2) =
  1297     list_ord (fn ((_, (d1, _)), (_, (d2, _))) =>
  1298       Term.fast_term_ord (d1, d2)) (defs1, defs2);
  1299 structure Defstab =
  1300     TableFun(type key = (Attrib.binding * (term * term list)) list val ord = defs_ord);
  1301 
  1302 fun rem_dup_defs es ds =
  1303     fold_map (fn e as (Defines defs) => (fn ds =>
  1304                  if Defstab.defined ds defs
  1305                  then (Defines [], ds)
  1306                  else (e, Defstab.update (defs, ()) ds))
  1307                | e => (fn ds => (e, ds))) es ds;
  1308 fun rem_dup_elemss (Int es) ds = apfst Int (rem_dup_defs es ds)
  1309   | rem_dup_elemss (Ext e) ds = (Ext e, ds);
  1310 fun rem_dup_defines raw_elemss =
  1311     fold_map (fn (id as (_, (Assumed _)), es) => (fn ds =>
  1312                      apfst (pair id) (rem_dup_elemss es ds))
  1313                | (id as (_, (Derived _)), es) => (fn ds =>
  1314                      ((id, es), ds))) raw_elemss Defstab.empty |> #1;
  1315 
  1316 (* CB: type inference and consistency checks for locales.
  1317 
  1318    Works by building a context (through declare_elemss), extracting the
  1319    required information and adjusting the context elements (finish_elemss).
  1320    Can also universally close free vars in assms and defs.  This is only
  1321    needed for Ext elements and controlled by parameter do_close.
  1322 
  1323    Only elements of assumed identifiers are considered.
  1324 *)
  1325 
  1326 fun prep_elemss prep_vars prepp do_close context fixed_params raw_elemss raw_concl =
  1327   let
  1328     (* CB: contexts computed in the course of this function are discarded.
  1329        They are used for type inference and consistency checks only. *)
  1330     (* CB: fixed_params are the parameters (with types) of the target locale,
  1331        empty list if there is no target. *)
  1332     (* CB: raw_elemss are list of pairs consisting of identifiers and
  1333        context elements, the latter marked as internal or external. *)
  1334     val raw_elemss = rem_dup_defines raw_elemss;
  1335     val (raw_proppss, raw_ctxt) = declare_elemss prep_vars fixed_params raw_elemss context;
  1336     (* CB: raw_ctxt is context with additional fixed variables derived from
  1337        the fixes elements in raw_elemss,
  1338        raw_proppss contains assumptions and definitions from the
  1339        external elements in raw_elemss. *)
  1340     fun prep_prop raw_propp (raw_ctxt, raw_concl)  =
  1341       let
  1342         (* CB: add type information from fixed_params to context (declare_term) *)
  1343         (* CB: process patterns (conclusion and external elements only) *)
  1344         val (ctxt, all_propp) =
  1345           prepp (fold Variable.declare_term (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp);
  1346         (* CB: add type information from conclusion and external elements to context *)
  1347         val ctxt = fold Variable.declare_term (maps (map fst) all_propp) ctxt;
  1348         (* CB: resolve schematic variables (patterns) in conclusion and external elements. *)
  1349         val all_propp' = map2 (curry (op ~~))
  1350           (#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp)))) (map (map snd) all_propp);
  1351         val (concl, propp) = chop (length raw_concl) all_propp';
  1352       in (propp, (ctxt, concl)) end
  1353 
  1354     val (proppss, (ctxt, concl)) =
  1355       (fold_burrow o fold_burrow) prep_prop raw_proppss (raw_ctxt, raw_concl);
  1356 
  1357     (* CB: obtain all parameters from identifier part of raw_elemss *)
  1358     val xs = map #1 (params_of' raw_elemss);
  1359     val typing = unify_frozen ctxt 0
  1360       (map (Variable.default_type raw_ctxt) xs)
  1361       (map (Variable.default_type ctxt) xs);
  1362     val parms = param_types (xs ~~ typing);
  1363     (* CB: parms are the parameters from raw_elemss, with correct typing. *)
  1364 
  1365     (* CB: extract information from assumes and defines elements
  1366        (fixes, constrains and notes in raw_elemss don't have an effect on
  1367        text and elemss), compute final form of context elements. *)
  1368     val ((text, _), elemss) = finish_elemss ctxt parms do_close
  1369       ((((([], []), ([], [])), ([], [], [])), []), raw_elemss ~~ proppss);
  1370     (* CB: text has the following structure:
  1371            (((exts, exts'), (ints, ints')), (xs, env, defs))
  1372        where
  1373          exts: external assumptions (terms in external assumes elements)
  1374          exts': dito, normalised wrt. env
  1375          ints: internal assumptions (terms in internal assumes elements)
  1376          ints': dito, normalised wrt. env
  1377          xs: the free variables in exts' and ints' and rhss of definitions,
  1378            this includes parameters except defined parameters
  1379          env: list of term pairs encoding substitutions, where the first term
  1380            is a free variable; substitutions represent defines elements and
  1381            the rhs is normalised wrt. the previous env
  1382          defs: theorems representing the substitutions from defines elements
  1383            (thms are normalised wrt. env).
  1384        elemss is an updated version of raw_elemss:
  1385          - type info added to Fixes and modified in Constrains
  1386          - axiom and definition statement replaced by corresponding one
  1387            from proppss in Assumes and Defines
  1388          - Facts unchanged
  1389        *)
  1390   in ((parms, elemss, concl), text) end;
  1391 
  1392 in
  1393 
  1394 fun read_elemss x = prep_elemss ProofContext.read_vars ProofContext.read_propp_schematic x;
  1395 fun cert_elemss x = prep_elemss ProofContext.cert_vars ProofContext.cert_propp_schematic x;
  1396 
  1397 end;
  1398 
  1399 
  1400 (* facts and attributes *)
  1401 
  1402 local
  1403 
  1404 fun check_name name =
  1405   if NameSpace.is_qualified name then error ("Illegal qualified name: " ^ quote name)
  1406   else name;
  1407 
  1408 fun prep_facts _ _ _ ctxt (Int elem) = elem
  1409       |> Element.morph_ctxt (Morphism.thm_morphism (Thm.transfer (ProofContext.theory_of ctxt)))
  1410   | prep_facts prep_name get intern ctxt (Ext elem) = elem |> Element.map_ctxt
  1411      {var = I, typ = I, term = I,
  1412       name = Name.map_name prep_name,
  1413       fact = get ctxt,
  1414       attrib = Args.assignable o intern (ProofContext.theory_of ctxt)};
  1415 
  1416 in
  1417 
  1418 fun read_facts x = prep_facts check_name ProofContext.get_fact Attrib.intern_src x;
  1419 fun cert_facts x = prep_facts I (K I) (K I) x;
  1420 
  1421 end;
  1422 
  1423 
  1424 (* Get the specification of a locale *)
  1425 
  1426 (*The global specification is made from the parameters and global
  1427   assumptions, the local specification from the parameters and the
  1428   local assumptions.*)
  1429 
  1430 local
  1431 
  1432 fun gen_asms_of get thy name =
  1433   let
  1434     val ctxt = ProofContext.init thy;
  1435     val (_, raw_elemss) = flatten (ctxt, I) (([], Symtab.empty), Expr (Locale name));
  1436     val ((_, elemss, _), _) = read_elemss false ctxt [] raw_elemss [];
  1437   in
  1438     elemss |> get
  1439       |> maps (fn (_, es) => map (fn Int e => e) es)
  1440       |> maps (fn Assumes asms => asms | _ => [])
  1441       |> map (apsnd (map fst))
  1442   end;
  1443 
  1444 in
  1445 
  1446 fun parameters_of thy = #params o the_locale thy;
  1447 
  1448 fun intros thy = #intros o the_locale thy;
  1449   (*returns introduction rule for delta predicate and locale predicate
  1450     as a pair of singleton lists*)
  1451 
  1452 fun dests thy = #dests o the_locale thy;
  1453 
  1454 fun facts_of thy = map_filter (fn (Element.Notes (_, facts), _) => SOME facts
  1455   | _ => NONE) o #elems o the_locale thy;
  1456 
  1457 fun parameters_of_expr thy expr =
  1458   let
  1459     val ctxt = ProofContext.init thy;
  1460     val pts = params_of_expr ctxt [] (intern_expr thy expr)
  1461         ([], Symtab.empty, Symtab.empty);
  1462     val raw_params_elemss = make_raw_params_elemss pts;
  1463     val ((_, syn), raw_elemss) = flatten (ctxt, intern_expr thy)
  1464         (([], Symtab.empty), Expr expr);
  1465     val ((parms, _, _), _) =
  1466         read_elemss false ctxt [] (raw_params_elemss @ raw_elemss) [];
  1467   in map (fn p as (n, _) => (p, Symtab.lookup syn n |> the)) parms end;
  1468 
  1469 fun local_asms_of thy name =
  1470   gen_asms_of (single o Library.last_elem) thy name;
  1471 
  1472 fun global_asms_of thy name =
  1473   gen_asms_of I thy name;
  1474 
  1475 end;
  1476 
  1477 
  1478 (* full context statements: imports + elements + conclusion *)
  1479 
  1480 local
  1481 
  1482 fun prep_context_statement prep_expr prep_elemss prep_facts
  1483     do_close fixed_params imports elements raw_concl context =
  1484   let
  1485     val thy = ProofContext.theory_of context;
  1486 
  1487     val (import_params, import_tenv, import_syn) =
  1488       params_of_expr context fixed_params (prep_expr thy imports)
  1489         ([], Symtab.empty, Symtab.empty);
  1490     val includes = map_filter (fn Expr e => SOME e | Elem _ => NONE) elements;
  1491     val (incl_params, incl_tenv, incl_syn) = fold (params_of_expr context fixed_params)
  1492       (map (prep_expr thy) includes) (import_params, import_tenv, import_syn);
  1493 
  1494     val ((import_ids, _), raw_import_elemss) =
  1495       flatten (context, prep_expr thy) (([], Symtab.empty), Expr imports);
  1496     (* CB: normalise "includes" among elements *)
  1497     val ((ids, syn), raw_elemsss) = foldl_map (flatten (context, prep_expr thy))
  1498       ((import_ids, incl_syn), elements);
  1499 
  1500     val raw_elemss = flat raw_elemsss;
  1501     (* CB: raw_import_elemss @ raw_elemss is the normalised list of
  1502        context elements obtained from import and elements. *)
  1503     (* Now additional elements for parameters are inserted. *)
  1504     val import_params_ids = make_params_ids import_params;
  1505     val incl_params_ids =
  1506         make_params_ids (incl_params \\ import_params);
  1507     val raw_import_params_elemss =
  1508         make_raw_params_elemss (import_params, incl_tenv, incl_syn);
  1509     val raw_incl_params_elemss =
  1510         make_raw_params_elemss (incl_params \\ import_params, incl_tenv, incl_syn);
  1511     val ((parms, all_elemss, concl), (spec, (_, _, defs))) = prep_elemss do_close
  1512       context fixed_params
  1513       (raw_import_params_elemss @ raw_import_elemss @ raw_incl_params_elemss @ raw_elemss) raw_concl;
  1514 
  1515     (* replace extended ids (for axioms) by ids *)
  1516     val (import_ids', incl_ids) = chop (length import_ids) ids;
  1517     val all_ids = import_params_ids @ import_ids' @ incl_params_ids @ incl_ids;
  1518     val all_elemss' = map (fn (((_, ps), _), (((n, ps'), mode), elems)) =>
  1519         (((n, map (fn p => (p, (the o AList.lookup (op =) ps') p)) ps), mode), elems))
  1520       (all_ids ~~ all_elemss);
  1521     (* CB: all_elemss and parms contain the correct parameter types *)
  1522 
  1523     val (ps, qs) = chop (length raw_import_params_elemss + length raw_import_elemss) all_elemss';
  1524     val ((import_elemss, _), import_ctxt) =
  1525       activate_facts false prep_facts ps context;
  1526 
  1527     val ((elemss, _), ctxt) =
  1528       activate_facts false prep_facts qs (ProofContext.set_stmt true import_ctxt);
  1529   in
  1530     ((((import_ctxt, import_elemss), (ctxt, elemss, syn)),
  1531       (parms, spec, defs)), concl)
  1532   end;
  1533 
  1534 fun prep_statement prep_locale prep_ctxt raw_locale elems concl ctxt =
  1535   let
  1536     val thy = ProofContext.theory_of ctxt;
  1537     val locale = Option.map (prep_locale thy) raw_locale;
  1538     val (fixed_params, imports) =
  1539       (case locale of
  1540         NONE => ([], empty)
  1541       | SOME name =>
  1542           let val {params = ps, ...} = the_locale thy name
  1543           in (map fst ps, Locale name) end);
  1544     val ((((locale_ctxt, _), (elems_ctxt, _, _)), _), concl') =
  1545       prep_ctxt false fixed_params imports (map Elem elems) concl ctxt;
  1546   in (locale, locale_ctxt, elems_ctxt, concl') end;
  1547 
  1548 fun prep_expr prep imports body ctxt =
  1549   let
  1550     val (((_, import_elemss), (ctxt', elemss, _)), _) = prep imports body ctxt;
  1551     val all_elems = maps snd (import_elemss @ elemss);
  1552   in (all_elems, ctxt') end;
  1553 
  1554 in
  1555 
  1556 val read_ctxt = prep_context_statement intern_expr read_elemss read_facts;
  1557 val cert_ctxt = prep_context_statement (K I) cert_elemss cert_facts;
  1558 
  1559 fun read_context imports body ctxt = #1 (read_ctxt true [] imports (map Elem body) [] ctxt);
  1560 fun cert_context imports body ctxt = #1 (cert_ctxt true [] imports (map Elem body) [] ctxt);
  1561 
  1562 val read_expr = prep_expr read_context;
  1563 val cert_expr = prep_expr cert_context;
  1564 
  1565 fun read_context_statement loc = prep_statement (K I) read_ctxt loc;
  1566 fun read_context_statement_cmd loc = prep_statement intern read_ctxt loc;
  1567 fun cert_context_statement loc = prep_statement (K I) cert_ctxt loc;
  1568 
  1569 end;
  1570 
  1571 
  1572 (* init *)
  1573 
  1574 fun init loc =
  1575   ProofContext.init
  1576   #> #2 o cert_context_statement (SOME loc) [] [];
  1577 
  1578 
  1579 (* print locale *)
  1580 
  1581 fun print_locale thy show_facts imports body =
  1582   let val (all_elems, ctxt) = read_expr imports body (ProofContext.init thy) in
  1583     Pretty.big_list "locale elements:" (all_elems
  1584       |> (if show_facts then I else filter (fn Notes _ => false | _ => true))
  1585       |> map (Element.pretty_ctxt ctxt) |> filter_out null
  1586       |> map Pretty.chunks)
  1587     |> Pretty.writeln
  1588   end;
  1589 
  1590 
  1591 
  1592 (** store results **)
  1593 
  1594 (* join equations of an id with already accumulated ones *)
  1595 
  1596 fun join_eqns get_reg id eqns =
  1597   let
  1598     val eqns' = case get_reg id
  1599       of NONE => eqns
  1600         | SOME (_, _, eqns') => Termtab.join (fn _ => fn (_, e) => e) (eqns, eqns')
  1601             (* prefer equations from eqns' *)
  1602   in ((id, eqns'), eqns') end;
  1603 
  1604 
  1605 (* collect witnesses and equations up to a particular target for a
  1606    registration; requires parameters and flattened list of identifiers
  1607    instead of recomputing it from the target *)
  1608 
  1609 fun collect_witnesses ctxt (imprt as ((impT, _), (imp, _))) parms ids ext_ts = let
  1610 
  1611     val thy = ProofContext.theory_of ctxt;
  1612 
  1613     val ts = map (var_inst_term (impT, imp)) ext_ts;
  1614     val (parms, parmTs) = split_list parms;
  1615     val parmvTs = map Logic.varifyT parmTs;
  1616     val vtinst = fold (Sign.typ_match thy) (parmvTs ~~ map Term.fastype_of ts) Vartab.empty;
  1617     val tinst = Vartab.dest vtinst |> map (fn ((x, 0), (_, T)) => (x, T))
  1618         |> Symtab.make;
  1619     val inst = Symtab.make (parms ~~ ts);
  1620 
  1621     (* instantiate parameter names in ids *)
  1622     val ext_inst = Symtab.make (parms ~~ ext_ts);
  1623     fun ext_inst_names ps = map (the o Symtab.lookup ext_inst) ps;
  1624     val inst_ids = map (apfst (apsnd ext_inst_names)) ids;
  1625     val assumed_ids = map_filter (fn (id, (_, Assumed _)) => SOME id | _ => NONE) inst_ids;
  1626     val wits = maps (#2 o the o get_local_registration ctxt imprt) assumed_ids;
  1627     val eqns =
  1628       fold_map (join_eqns (get_local_registration ctxt imprt))
  1629         (map fst inst_ids) Termtab.empty |> snd |> Termtab.dest |> map snd;
  1630   in ((tinst, inst), wits, eqns) end;
  1631 
  1632 
  1633 (* compute and apply morphism *)
  1634 
  1635 fun name_morph phi_name (lprfx, pprfx) b =
  1636   b
  1637   |> (if not (Binding.is_nothing b) andalso pprfx <> ""
  1638         then Binding.add_prefix false pprfx else I)
  1639   |> (if not (Binding.is_nothing b)
  1640         then Binding.add_prefix false lprfx else I)
  1641   |> phi_name;
  1642 
  1643 fun inst_morph thy phi_name param_prfx insts prems eqns export =
  1644   let
  1645     (* standardise export morphism *)
  1646     val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export;
  1647     val exp_term = TermSubst.zero_var_indexes o Morphism.term export;
  1648       (* FIXME sync with exp_fact *)
  1649     val exp_typ = Logic.type_map exp_term;
  1650     val export' =
  1651       Morphism.morphism {name = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact};
  1652   in
  1653     Morphism.name_morphism (name_morph phi_name param_prfx) $>
  1654       Element.inst_morphism thy insts $>
  1655       Element.satisfy_morphism prems $>
  1656       Morphism.term_morphism (MetaSimplifier.rewrite_term thy eqns []) $>
  1657       Morphism.thm_morphism (MetaSimplifier.rewrite_rule eqns) $>
  1658       export'
  1659   end;
  1660 
  1661 fun activate_note thy phi_name param_prfx attrib insts prems eqns exp =
  1662   (Element.facts_map o Element.morph_ctxt)
  1663       (inst_morph thy phi_name param_prfx insts prems eqns exp)
  1664   #> Attrib.map_facts attrib;
  1665 
  1666 
  1667 (* public interface to interpretation morphism *)
  1668 
  1669 fun get_interpret_morph thy phi_name param_prfx (exp, imp) target ext_ts =
  1670   let
  1671     val parms = the_locale thy target |> #params |> map fst;
  1672     val ids = flatten (ProofContext.init thy, intern_expr thy)
  1673       (([], Symtab.empty), Expr (Locale target)) |> fst |> fst;
  1674     val (insts, prems, eqns) = collect_witnesses (ProofContext.init thy) imp parms ids ext_ts;
  1675   in
  1676     inst_morph thy phi_name param_prfx insts prems eqns exp
  1677   end;
  1678 
  1679 (* store instantiations of args for all registered interpretations
  1680    of the theory *)
  1681 
  1682 fun note_thmss_registrations target (kind, args) thy =
  1683   let
  1684     val parms = the_locale thy target |> #params |> map fst;
  1685     val ids = flatten (ProofContext.init thy, intern_expr thy)
  1686       (([], Symtab.empty), Expr (Locale target)) |> fst |> fst;
  1687 
  1688     val regs = get_global_registrations thy target;
  1689     (* add args to thy for all registrations *)
  1690 
  1691     fun activate (ext_ts, ((phi_name, param_prfx), (exp, imp), _, _)) thy =
  1692       let
  1693         val (insts, prems, eqns) = collect_witnesses (ProofContext.init thy) imp parms ids ext_ts;
  1694         val args' = args
  1695           |> activate_note thy phi_name param_prfx
  1696                (Attrib.attribute_i thy) insts prems eqns exp;
  1697       in
  1698         thy
  1699         |> global_note_qualified kind args'
  1700         |> snd
  1701       end;
  1702   in fold activate regs thy end;
  1703 
  1704 
  1705 (* locale results *)
  1706 
  1707 fun add_thmss loc kind args ctxt =
  1708   let
  1709     val (([(_, [Notes args'])], _), ctxt') =
  1710       activate_facts true cert_facts
  1711         [((("", []), Assumed []), [Ext (Notes (kind, args))])] ctxt;
  1712     val ctxt'' = ctxt' |> ProofContext.theory
  1713       (change_locale loc
  1714         (fn (axiom, elems, params, decls, regs, intros, dests) =>
  1715           (axiom, elems @ [(Notes args', stamp ())],
  1716             params, decls, regs, intros, dests))
  1717       #> note_thmss_registrations loc args');
  1718   in ctxt'' end;
  1719 
  1720 
  1721 (* declarations *)
  1722 
  1723 local
  1724 
  1725 fun decl_attrib decl phi = Thm.declaration_attribute (K (decl phi));
  1726 
  1727 fun add_decls add loc decl =
  1728   ProofContext.theory (change_locale loc
  1729     (fn (axiom, elems, params, decls, regs, intros, dests) =>
  1730       (axiom, elems, params, add (decl, stamp ()) decls, regs, intros, dests))) #>
  1731   add_thmss loc Thm.internalK
  1732     [((Name.no_binding, [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])];
  1733 
  1734 in
  1735 
  1736 val add_type_syntax = add_decls (apfst o cons);
  1737 val add_term_syntax = add_decls (apsnd o cons);
  1738 val add_declaration = add_decls (K I);
  1739 
  1740 fun declarations_of thy loc =
  1741   the_locale thy loc |> #decls |> apfst (map fst) |> apsnd (map fst);
  1742 
  1743 end;
  1744 
  1745 
  1746 
  1747 (** define locales **)
  1748 
  1749 (* predicate text *)
  1750 (* CB: generate locale predicates and delta predicates *)
  1751 
  1752 local
  1753 
  1754 (* introN: name of theorems for introduction rules of locale and
  1755      delta predicates;
  1756    axiomsN: name of theorem set with destruct rules for locale predicates,
  1757      also name suffix of delta predicates. *)
  1758 
  1759 val introN = "intro";
  1760 val axiomsN = "axioms";
  1761 
  1762 fun atomize_spec thy ts =
  1763   let
  1764     val t = Logic.mk_conjunction_balanced ts;
  1765     val body = ObjectLogic.atomize_term thy t;
  1766     val bodyT = Term.fastype_of body;
  1767   in
  1768     if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of thy t))
  1769     else (body, bodyT, ObjectLogic.atomize (Thm.cterm_of thy t))
  1770   end;
  1771 
  1772 fun aprop_tr' n c = (Syntax.constN ^ c, fn ctxt => fn args =>
  1773   if length args = n then
  1774     Syntax.const "_aprop" $
  1775       Term.list_comb (Syntax.free (Consts.extern (ProofContext.consts_of ctxt) c), args)
  1776   else raise Match);
  1777 
  1778 (* CB: define one predicate including its intro rule and axioms
  1779    - bname: predicate name
  1780    - parms: locale parameters
  1781    - defs: thms representing substitutions from defines elements
  1782    - ts: terms representing locale assumptions (not normalised wrt. defs)
  1783    - norm_ts: terms representing locale assumptions (normalised wrt. defs)
  1784    - thy: the theory
  1785 *)
  1786 
  1787 fun def_pred bname parms defs ts norm_ts thy =
  1788   let
  1789     val name = Sign.full_name thy bname;
  1790 
  1791     val (body, bodyT, body_eq) = atomize_spec thy norm_ts;
  1792     val env = Term.add_term_free_names (body, []);
  1793     val xs = filter (member (op =) env o #1) parms;
  1794     val Ts = map #2 xs;
  1795     val extraTs = (Term.term_tfrees body \\ List.foldr Term.add_typ_tfrees [] Ts)
  1796       |> Library.sort_wrt #1 |> map TFree;
  1797     val predT = map Term.itselfT extraTs ---> Ts ---> bodyT;
  1798 
  1799     val args = map Logic.mk_type extraTs @ map Free xs;
  1800     val head = Term.list_comb (Const (name, predT), args);
  1801     val statement = ObjectLogic.ensure_propT thy head;
  1802 
  1803     val ([pred_def], defs_thy) =
  1804       thy
  1805       |> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], [])
  1806       |> Sign.declare_const [] ((Name.binding bname, predT), NoSyn) |> snd
  1807       |> PureThy.add_defs false
  1808         [((Thm.def_name bname, Logic.mk_equals (head, body)), [Thm.kind_internal])];
  1809     val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;
  1810 
  1811     val cert = Thm.cterm_of defs_thy;
  1812 
  1813     val intro = Goal.prove_global defs_thy [] norm_ts statement (fn _ =>
  1814       MetaSimplifier.rewrite_goals_tac [pred_def] THEN
  1815       Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
  1816       Tactic.compose_tac (false,
  1817         Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
  1818 
  1819     val conjuncts =
  1820       (Drule.equal_elim_rule2 OF [body_eq,
  1821         MetaSimplifier.rewrite_rule [pred_def] (Thm.assume (cert statement))])
  1822       |> Conjunction.elim_balanced (length ts);
  1823     val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
  1824       Element.prove_witness defs_ctxt t
  1825        (MetaSimplifier.rewrite_goals_tac defs THEN
  1826         Tactic.compose_tac (false, ax, 0) 1));
  1827   in ((statement, intro, axioms), defs_thy) end;
  1828 
  1829 fun assumes_to_notes (Assumes asms) axms =
  1830       fold_map (fn (a, spec) => fn axs =>
  1831           let val (ps, qs) = chop (length spec) axs
  1832           in ((a, [(ps, [])]), qs) end) asms axms
  1833       |> apfst (curry Notes Thm.assumptionK)
  1834   | assumes_to_notes e axms = (e, axms);
  1835 
  1836 (* CB: the following two change only "new" elems, these have identifier ("", _). *)
  1837 
  1838 (* turn Assumes into Notes elements *)
  1839 
  1840 fun change_assumes_elemss axioms elemss =
  1841   let
  1842     val satisfy = Element.morph_ctxt (Element.satisfy_morphism axioms);
  1843     fun change (id as ("", _), es) =
  1844           fold_map assumes_to_notes (map satisfy es)
  1845           #-> (fn es' => pair (id, es'))
  1846       | change e = pair e;
  1847   in
  1848     fst (fold_map change elemss (map Element.conclude_witness axioms))
  1849   end;
  1850 
  1851 (* adjust hyps of Notes elements *)
  1852 
  1853 fun change_elemss_hyps axioms elemss =
  1854   let
  1855     val satisfy = Element.morph_ctxt (Element.satisfy_morphism axioms);
  1856     fun change (id as ("", _), es) = (id, map (fn e as Notes _ => satisfy e | e => e) es)
  1857       | change e = e;
  1858   in map change elemss end;
  1859 
  1860 in
  1861 
  1862 (* CB: main predicate definition function *)
  1863 
  1864 fun define_preds pname (parms, ((exts, exts'), (ints, ints')), defs) elemss thy =
  1865   let
  1866     val ((elemss', more_ts), a_elem, a_intro, thy'') =
  1867       if null exts then ((elemss, []), [], [], thy)
  1868       else
  1869         let
  1870           val aname = if null ints then pname else pname ^ "_" ^ axiomsN;
  1871           val ((statement, intro, axioms), thy') =
  1872             thy
  1873             |> def_pred aname parms defs exts exts';
  1874           val elemss' = change_assumes_elemss axioms elemss;
  1875           val a_elem = [(("", []),
  1876             [Assumes [((Name.binding (pname ^ "_" ^ axiomsN), []), [(statement, [])])]])];
  1877           val (_, thy'') =
  1878             thy'
  1879             |> Sign.add_path aname
  1880             |> Sign.no_base_names
  1881             |> PureThy.note_thmss Thm.internalK [((Name.binding introN, []), [([intro], [])])]
  1882             ||> Sign.restore_naming thy';
  1883         in ((elemss', [statement]), a_elem, [intro], thy'') end;
  1884     val (predicate, stmt', elemss'', b_intro, thy'''') =
  1885       if null ints then (([], []), more_ts, elemss' @ a_elem, [], thy'')
  1886       else
  1887         let
  1888           val ((statement, intro, axioms), thy''') =
  1889             thy''
  1890             |> def_pred pname parms defs (ints @ more_ts) (ints' @ more_ts);
  1891           val cstatement = Thm.cterm_of thy''' statement;
  1892           val elemss'' = change_elemss_hyps axioms elemss';
  1893           val b_elem = [(("", []),
  1894                [Assumes [((Name.binding (pname ^ "_" ^ axiomsN), []), [(statement, [])])]])];
  1895           val (_, thy'''') =
  1896             thy'''
  1897             |> Sign.add_path pname
  1898             |> Sign.no_base_names
  1899             |> PureThy.note_thmss Thm.internalK
  1900                  [((Name.binding introN, []), [([intro], [])]),
  1901                   ((Name.binding axiomsN, []),
  1902                     [(map (Drule.standard o Element.conclude_witness) axioms, [])])]
  1903             ||> Sign.restore_naming thy''';
  1904         in (([cstatement], axioms), [statement], elemss'' @ b_elem, [intro], thy'''') end;
  1905   in (((elemss'', predicate, stmt'), (a_intro, b_intro)), thy'''') end;
  1906 
  1907 end;
  1908 
  1909 
  1910 (* add_locale(_i) *)
  1911 
  1912 local
  1913 
  1914 (* turn Defines into Notes elements, accumulate definition terms *)
  1915 
  1916 fun defines_to_notes is_ext thy (Defines defs) defns =
  1917     let
  1918       val defs' = map (fn (_, (def, _)) => (Attrib.no_binding, (def, []))) defs
  1919       val notes = map (fn (a, (def, _)) =>
  1920         (a, [([assume (cterm_of thy def)], [])])) defs
  1921     in
  1922       (if is_ext then SOME (Notes (Thm.definitionK, notes)) else NONE, defns @ [Defines defs'])
  1923     end
  1924   | defines_to_notes _ _ e defns = (SOME e, defns);
  1925 
  1926 fun change_defines_elemss thy elemss defns =
  1927   let
  1928     fun change (id as (n, _), es) defns =
  1929         let
  1930           val (es', defns') = fold_map (defines_to_notes (n="") thy) es defns
  1931         in ((id, map_filter I es'), defns') end
  1932   in fold_map change elemss defns end;
  1933 
  1934 fun gen_add_locale prep_ctxt prep_expr
  1935     predicate_name bname raw_imports raw_body thy =
  1936     (* predicate_name: "" - locale with predicate named as locale
  1937         "name" - locale with predicate named "name" *)
  1938   let
  1939     val thy_ctxt = ProofContext.init thy;
  1940     val name = Sign.full_name thy bname;
  1941     val _ = is_some (get_locale thy name) andalso
  1942       error ("Duplicate definition of locale " ^ quote name);
  1943 
  1944     val (((import_ctxt, import_elemss), (body_ctxt, body_elemss, syn)),
  1945       text as (parms, ((_, exts'), _), defs)) =
  1946         prep_ctxt raw_imports raw_body thy_ctxt;
  1947     val elemss = import_elemss @ body_elemss |>
  1948       map_filter (fn ((id, Assumed axs), elems) => SOME (id, elems) | _ => NONE);
  1949 
  1950     val extraTs = List.foldr Term.add_term_tfrees [] exts' \\
  1951       List.foldr Term.add_typ_tfrees [] (map snd parms);
  1952     val _ = if null extraTs then ()
  1953       else warning ("Additional type variable(s) in locale specification " ^ quote bname);
  1954 
  1955     val predicate_name' = case predicate_name of "" => bname | _ => predicate_name;
  1956     val (elemss', defns) = change_defines_elemss thy elemss [];
  1957     val elemss'' = elemss' @ [(("", []), defns)];
  1958     val (((elemss''', predicate as (pred_statement, pred_axioms), stmt'), intros), thy') =
  1959       define_preds predicate_name' text elemss'' thy;
  1960     val regs = pred_axioms
  1961       |> fold_map (fn (id, elems) => fn wts => let
  1962              val ts = flat (map_filter (fn (Assumes asms) =>
  1963                SOME (maps (map #1 o #2) asms) | _ => NONE) elems);
  1964              val (wts1, wts2) = chop (length ts) wts;
  1965            in ((apsnd (map fst) id, wts1), wts2) end) elemss'''
  1966       |> fst
  1967       |> map_filter (fn (("", _), _) => NONE | e => SOME e);
  1968     fun axiomify axioms elemss =
  1969       (axioms, elemss) |> foldl_map (fn (axs, (id, elems)) => let
  1970                    val ts = flat (map_filter (fn (Assumes asms) =>
  1971                      SOME (maps (map #1 o #2) asms) | _ => NONE) elems);
  1972                    val (axs1, axs2) = chop (length ts) axs;
  1973                  in (axs2, ((id, Assumed axs1), elems)) end)
  1974       |> snd;
  1975     val ((_, facts), ctxt) = activate_facts true (K I)
  1976       (axiomify pred_axioms elemss''') (ProofContext.init thy');
  1977     val view_ctxt = Assumption.add_view thy_ctxt pred_statement ctxt;
  1978     val export = Thm.close_derivation o Goal.norm_result o
  1979       singleton (ProofContext.export view_ctxt thy_ctxt);
  1980     val facts' = facts |> map (fn (a, ths) => ((a, []), [(map export ths, [])]));
  1981     val elems' = maps #2 (filter (fn ((s, _), _) => s = "") elemss''');
  1982     val elems'' = map_filter (fn (Fixes _) => NONE | e => SOME e) elems';
  1983     val axs' = map (Element.assume_witness thy') stmt';
  1984     val loc_ctxt = thy'
  1985       |> Sign.add_path bname
  1986       |> Sign.no_base_names
  1987       |> PureThy.note_thmss Thm.assumptionK facts' |> snd
  1988       |> Sign.restore_naming thy'
  1989       |> register_locale name {axiom = axs',
  1990         elems = map (fn e => (e, stamp ())) elems'',
  1991         params = params_of elemss''' |> map (fn (x, SOME T) => ((x, T), the (Symtab.lookup syn x))),
  1992         decls = ([], []),
  1993         regs = regs,
  1994         intros = intros,
  1995         dests = map Element.conclude_witness pred_axioms}
  1996       |> init name;
  1997   in (name, loc_ctxt) end;
  1998 
  1999 in
  2000 
  2001 val add_locale = gen_add_locale cert_context (K I);
  2002 val add_locale_cmd = gen_add_locale read_context intern_expr "";
  2003 
  2004 end;
  2005 
  2006 val _ = Context.>> (Context.map_theory
  2007  (add_locale "" "var" empty [Fixes [(Name.binding (Name.internal "x"), NONE, NoSyn)]] #>
  2008   snd #> ProofContext.theory_of #>
  2009   add_locale "" "struct" empty [Fixes [(Name.binding (Name.internal "S"), NONE, Structure)]] #>
  2010   snd #> ProofContext.theory_of));
  2011 
  2012 
  2013 
  2014 
  2015 (** Normalisation of locale statements ---
  2016     discharges goals implied by interpretations **)
  2017 
  2018 local
  2019 
  2020 fun locale_assm_intros thy =
  2021   Symtab.fold (fn (_, {intros = (a, _), ...}) => fn intros => (a @ intros))
  2022     (#2 (LocalesData.get thy)) [];
  2023 fun locale_base_intros thy =
  2024   Symtab.fold (fn (_, {intros = (_, b), ...}) => fn intros => (b @ intros))
  2025     (#2 (LocalesData.get thy)) [];
  2026 
  2027 fun all_witnesses ctxt =
  2028   let
  2029     val thy = ProofContext.theory_of ctxt;
  2030     fun get registrations = Symtab.fold (fn (_, regs) => fn thms =>
  2031         (Registrations.dest thy regs |> map (fn (_, (_, (exp, _), wits, _)) =>
  2032           map (Element.conclude_witness #> Morphism.thm exp) wits) |> flat) @ thms)
  2033       registrations [];
  2034   in get (RegistrationsData.get (Context.Proof ctxt)) end;
  2035 
  2036 in
  2037 
  2038 fun intro_locales_tac eager ctxt facts st =
  2039   let
  2040     val wits = all_witnesses ctxt;
  2041     val thy = ProofContext.theory_of ctxt;
  2042     val intros = locale_base_intros thy @ (if eager then locale_assm_intros thy else []);
  2043   in
  2044     Method.intros_tac (wits @ intros) facts st
  2045   end;
  2046 
  2047 end;
  2048 
  2049 
  2050 (** Interpretation commands **)
  2051 
  2052 local
  2053 
  2054 (* extract proof obligations (assms and defs) from elements *)
  2055 
  2056 fun extract_asms_elems ((id, Assumed _), elems) = (id, maps Element.prems_of elems)
  2057   | extract_asms_elems ((id, Derived _), _) = (id, []);
  2058 
  2059 
  2060 (* activate instantiated facts in theory or context *)
  2061 
  2062 fun gen_activate_facts_elemss mk_ctxt note attrib put_reg add_wit add_eqn
  2063         phi_name all_elemss pss propss eq_attns (exp, imp) thmss thy_ctxt =
  2064   let
  2065     val ctxt = mk_ctxt thy_ctxt;
  2066     fun get_reg thy_ctxt = get_local_registration (mk_ctxt thy_ctxt);
  2067     fun test_reg thy_ctxt = test_local_registration (mk_ctxt thy_ctxt);
  2068 
  2069     val (all_propss, eq_props) = chop (length all_elemss) propss;
  2070     val (all_thmss, eq_thms) = chop (length all_elemss) thmss;
  2071 
  2072     (* Filter out fragments already registered. *)
  2073 
  2074     val (new_elemss, xs) = split_list (filter_out (fn (((id, _), _), _) =>
  2075           test_reg thy_ctxt id) (all_elemss ~~ (pss ~~ (all_propss ~~ all_thmss))));
  2076     val (new_pss, ys) = split_list xs;
  2077     val (new_propss, new_thmss) = split_list ys;
  2078 
  2079     val thy_ctxt' = thy_ctxt
  2080       (* add registrations *)
  2081       |> fold2 (fn ((id as (loc, _), _), _) => fn ps => put_reg id (phi_name, param_prefix loc ps) (exp, imp))
  2082            new_elemss new_pss
  2083       (* add witnesses of Assumed elements (only those generate proof obligations) *)
  2084       |> fold2 (fn (id, _) => fold (add_wit id)) new_propss new_thmss
  2085       (* add equations *)
  2086       |> fold2 (fn (id, _) => fold (add_eqn id)) eq_props
  2087           ((map o map) (Drule.abs_def o LocalDefs.meta_rewrite_rule ctxt o
  2088             Element.conclude_witness) eq_thms);
  2089 
  2090     val prems = flat (map_filter
  2091           (fn ((id, Assumed _), _) => Option.map #2 (get_reg thy_ctxt' imp id)
  2092             | ((_, Derived _), _) => NONE) all_elemss);
  2093 
  2094     val thy_ctxt'' = thy_ctxt'
  2095       (* add witnesses of Derived elements *)
  2096       |> fold (fn (id, thms) => fold
  2097            (add_wit id o Element.morph_witness (Element.satisfy_morphism prems)) thms)
  2098          (map_filter (fn ((_, Assumed _), _) => NONE
  2099             | ((id, Derived thms), _) => SOME (id, thms)) new_elemss)
  2100 
  2101     fun activate_elem phi_name param_prfx insts prems eqns exp (Notes (kind, facts)) thy_ctxt =
  2102         let
  2103           val ctxt = mk_ctxt thy_ctxt;
  2104           val thy = ProofContext.theory_of ctxt;
  2105           val facts' = facts
  2106             |> activate_note thy phi_name param_prfx
  2107                  (attrib thy_ctxt) insts prems eqns exp;
  2108         in 
  2109           thy_ctxt
  2110           |> note kind facts'
  2111           |> snd
  2112         end
  2113       | activate_elem _ _ _ _ _ _ _ thy_ctxt = thy_ctxt;
  2114 
  2115     fun activate_elems (((loc, ext_ts), _), _) ps thy_ctxt =
  2116       let
  2117         val ctxt = mk_ctxt thy_ctxt;
  2118         val thy = ProofContext.theory_of ctxt;
  2119         val {params, elems, ...} = the_locale thy loc;
  2120         val parms = map fst params;
  2121         val param_prfx = param_prefix loc ps;
  2122         val ids = flatten (ProofContext.init thy, intern_expr thy)
  2123           (([], Symtab.empty), Expr (Locale loc)) |> fst |> fst;
  2124         val (insts, prems, eqns) = collect_witnesses ctxt imp parms ids ext_ts;
  2125       in
  2126         thy_ctxt
  2127         |> fold (activate_elem phi_name param_prfx insts prems eqns exp o fst) elems
  2128       end;
  2129 
  2130   in
  2131     thy_ctxt''
  2132     (* add equations as lemmas to context *)
  2133     |> (fold2 o fold2) (fn attn => fn thm => snd o yield_singleton (note Thm.lemmaK)
  2134          ((apsnd o map) (attrib thy_ctxt'') attn, [([Element.conclude_witness thm], [])]))
  2135             (unflat eq_thms eq_attns) eq_thms
  2136     (* add interpreted facts *)
  2137     |> fold2 activate_elems new_elemss new_pss
  2138   end;
  2139 
  2140 fun global_activate_facts_elemss x = gen_activate_facts_elemss
  2141   ProofContext.init
  2142   global_note_qualified
  2143   Attrib.attribute_i
  2144   put_global_registration
  2145   add_global_witness
  2146   add_global_equation
  2147   x;
  2148 
  2149 fun local_activate_facts_elemss x = gen_activate_facts_elemss
  2150   I
  2151   local_note_qualified
  2152   (Attrib.attribute_i o ProofContext.theory_of)
  2153   put_local_registration
  2154   add_local_witness
  2155   add_local_equation
  2156   x;
  2157 
  2158 fun prep_instantiations parse_term parse_prop ctxt parms (insts, eqns) =
  2159   let
  2160     (* parameters *)
  2161     val (parm_names, parm_types) = parms |> split_list
  2162       ||> map (TypeInfer.paramify_vars o Logic.varifyT);
  2163     val type_parms = fold Term.add_tvarsT parm_types [] |> map (Logic.mk_type o TVar);
  2164     val type_parm_names = fold Term.add_tfreesT (map snd parms) [] |> map fst;
  2165 
  2166     (* parameter instantiations *)
  2167     val d = length parms - length insts;
  2168     val insts =
  2169       if d < 0 then error "More arguments than parameters in instantiation."
  2170       else insts @ replicate d NONE;
  2171     val (given_ps, given_insts) =
  2172       ((parm_names ~~ parm_types) ~~ insts) |> map_filter
  2173           (fn (_, NONE) => NONE
  2174             | ((n, T), SOME inst) => SOME ((n, T), inst))
  2175         |> split_list;
  2176     val (given_parm_names, given_parm_types) = given_ps |> split_list;
  2177 
  2178     (* parse insts / eqns *)
  2179     val given_insts' = map (parse_term ctxt) given_insts;
  2180     val eqns' = map (parse_prop ctxt) eqns;
  2181 
  2182     (* type inference and contexts *)
  2183     val arg = type_parms @ map2 TypeInfer.constrain given_parm_types given_insts' @ eqns';
  2184     val res = Syntax.check_terms ctxt arg;
  2185     val ctxt' = ctxt |> fold Variable.auto_fixes res;
  2186 
  2187     (* instantiation *)
  2188     val (type_parms'', res') = chop (length type_parms) res;
  2189     val (given_insts'', eqns'') = chop (length given_insts) res';
  2190     val instT = Symtab.make (type_parm_names ~~ map Logic.dest_type type_parms'');
  2191     val inst = Symtab.make (given_parm_names ~~ given_insts'');
  2192 
  2193     (* export from eigencontext *)
  2194     val export = Variable.export_morphism ctxt' ctxt;
  2195 
  2196     (* import, its inverse *)
  2197     val domT = fold Term.add_tfrees res [] |> map TFree;
  2198     val importT = domT |> map (fn x => (Morphism.typ export x, x))
  2199       |> map_filter (fn (TFree _, _) => NONE  (* fixed point of export *)
  2200                | (TVar y, x) => SOME (fst y, x)
  2201                | _ => error "internal: illegal export in interpretation")
  2202       |> Vartab.make;
  2203     val dom = fold Term.add_frees res [] |> map Free;
  2204     val imprt = dom |> map (fn x => (Morphism.term export x, x))
  2205       |> map_filter (fn (Free _, _) => NONE  (* fixed point of export *)
  2206                | (Var y, x) => SOME (fst y, x)
  2207                | _ => error "internal: illegal export in interpretation")
  2208       |> Vartab.make;
  2209   in (((instT, inst), eqns''), (export, ((importT, domT), (imprt, dom)))) end;
  2210 
  2211 val read_instantiations = prep_instantiations Syntax.parse_term Syntax.parse_prop;
  2212 val check_instantiations = prep_instantiations (K I) (K I);
  2213 
  2214 fun gen_prep_registration mk_ctxt test_reg activate
  2215     prep_attr prep_expr prep_insts
  2216     thy_ctxt phi_name raw_expr raw_insts =
  2217   let
  2218     val ctxt = mk_ctxt thy_ctxt;
  2219     val thy = ProofContext.theory_of ctxt;
  2220     val ctxt' = ProofContext.init thy;
  2221     fun prep_attn attn = (apsnd o map)
  2222       (Attrib.crude_closure ctxt o Args.assignable o prep_attr thy) attn;
  2223 
  2224     val expr = prep_expr thy raw_expr;
  2225 
  2226     val pts = params_of_expr ctxt' [] expr ([], Symtab.empty, Symtab.empty);
  2227     val params_ids = make_params_ids (#1 pts);
  2228     val raw_params_elemss = make_raw_params_elemss pts;
  2229     val ((ids, _), raw_elemss) = flatten (ctxt', I) (([], Symtab.empty), Expr expr);
  2230     val ((parms, all_elemss, _), (_, (_, defs, _))) =
  2231       read_elemss false ctxt' [] (raw_params_elemss @ raw_elemss) [];
  2232 
  2233     (** compute instantiation **)
  2234 
  2235     (* consistency check: equations need to be stored in a particular locale,
  2236        therefore if equations are present locale expression must be a name *)
  2237 
  2238     val _ = case (expr, snd raw_insts) of
  2239         (Locale _, _) => () | (_, []) => ()
  2240       | (_, _) => error "Interpretations with `where' only permitted if locale expression is a name.";
  2241 
  2242     (* read or certify instantiation *)
  2243     val (raw_insts', raw_eqns) = raw_insts;
  2244     val (raw_eq_attns, raw_eqns') = split_list raw_eqns;
  2245     val (((instT, inst1), eqns), morphs) = prep_insts ctxt parms (raw_insts', raw_eqns');
  2246     val eq_attns = map prep_attn raw_eq_attns;
  2247 
  2248     (* defined params without given instantiation *)
  2249     val not_given = filter_out (Symtab.defined inst1 o fst) parms;
  2250     fun add_def (p, pT) inst =
  2251       let
  2252         val (t, T) = case find_first (fn (Free (a, _), _) => a = p) defs of
  2253                NONE => error ("Instance missing for parameter " ^ quote p)
  2254              | SOME (Free (_, T), t) => (t, T);
  2255         val d = Element.inst_term (instT, inst) t;
  2256       in Symtab.update_new (p, d) inst end;
  2257     val inst2 = fold add_def not_given inst1;
  2258     val inst_morphism = Element.inst_morphism thy (instT, inst2);
  2259     (* Note: insts contain no vars. *)
  2260 
  2261     (** compute proof obligations **)
  2262 
  2263     (* restore "small" ids *)
  2264     val ids' = map (fn ((n, ps), (_, mode)) =>
  2265           ((n, map (fn p => Free (p, (the o AList.lookup (op =) parms) p)) ps), mode))
  2266         ids;
  2267     val (_, all_elemss') = chop (length raw_params_elemss) all_elemss
  2268     (* instantiate ids and elements *)
  2269     val inst_elemss = (ids' ~~ all_elemss') |> map (fn (((n, ps), _), ((_, mode), elems)) =>
  2270       ((n, map (Morphism.term (inst_morphism $> fst morphs)) ps),
  2271         map (fn Int e => Element.morph_ctxt inst_morphism e) elems)
  2272       |> apfst (fn id => (id, map_mode (map (Element.morph_witness inst_morphism)) mode)));
  2273 
  2274     (* equations *)
  2275     val eqn_elems = if null eqns then []
  2276       else [(Library.last_elem inst_elemss |> fst |> fst, eqns)];
  2277 
  2278     val propss = map extract_asms_elems inst_elemss @ eqn_elems;
  2279 
  2280   in
  2281     (propss, activate phi_name inst_elemss (map (snd o fst) ids) propss eq_attns morphs, morphs)
  2282   end;
  2283 
  2284 fun gen_prep_global_registration mk_ctxt = gen_prep_registration ProofContext.init
  2285   test_global_registration
  2286   global_activate_facts_elemss mk_ctxt;
  2287 
  2288 fun gen_prep_local_registration mk_ctxt = gen_prep_registration I
  2289   test_local_registration
  2290   local_activate_facts_elemss mk_ctxt;
  2291 
  2292 val prep_global_registration = gen_prep_global_registration
  2293   (K I) (K I) check_instantiations;
  2294 val prep_global_registration_cmd = gen_prep_global_registration
  2295   Attrib.intern_src intern_expr read_instantiations;
  2296 
  2297 val prep_local_registration = gen_prep_local_registration
  2298   (K I) (K I) check_instantiations;
  2299 val prep_local_registration_cmd = gen_prep_local_registration
  2300   Attrib.intern_src intern_expr read_instantiations;
  2301 
  2302 fun prep_registration_in_locale target expr thy =
  2303   (* target already in internal form *)
  2304   let
  2305     val ctxt = ProofContext.init thy;
  2306     val ((raw_target_ids, target_syn), _) = flatten (ctxt, I)
  2307         (([], Symtab.empty), Expr (Locale target));
  2308     val fixed = the_locale thy target |> #params |> map #1;
  2309     val ((all_ids, syn), raw_elemss) = flatten (ctxt, intern_expr thy)
  2310         ((raw_target_ids, target_syn), Expr expr);
  2311     val (target_ids, ids) = chop (length raw_target_ids) all_ids;
  2312     val ((parms, elemss, _), _) = read_elemss false ctxt fixed raw_elemss [];
  2313 
  2314     (** compute proof obligations **)
  2315 
  2316     (* restore "small" ids, with mode *)
  2317     val ids' = map (apsnd snd) ids;
  2318     (* remove Int markers *)
  2319     val elemss' = map (fn (_, es) =>
  2320         map (fn Int e => e) es) elemss
  2321     (* extract assumptions and defs *)
  2322     val ids_elemss = ids' ~~ elemss';
  2323     val propss = map extract_asms_elems ids_elemss;
  2324 
  2325     (** activation function:
  2326         - add registrations to the target locale
  2327         - add induced registrations for all global registrations of
  2328           the target, unless already present
  2329         - add facts of induced registrations to theory **)
  2330 
  2331     fun activate thmss thy =
  2332       let
  2333         val satisfy = Element.satisfy_thm (flat thmss);
  2334         val ids_elemss_thmss = ids_elemss ~~ thmss;
  2335         val regs = get_global_registrations thy target;
  2336 
  2337         fun activate_id (((id, Assumed _), _), thms) thy =
  2338             thy |> put_registration_in_locale target id
  2339                 |> fold (add_witness_in_locale target id) thms
  2340           | activate_id _ thy = thy;
  2341 
  2342         fun activate_reg (ext_ts, ((phi_name, param_prfx), (exp, imp), _, _)) thy =
  2343           let
  2344             val (insts, wits, _) = collect_witnesses (ProofContext.init thy) imp fixed target_ids ext_ts;
  2345             val inst_parms = map (the o AList.lookup (op =) (map #1 fixed ~~ ext_ts));
  2346             val disch = Element.satisfy_thm wits;
  2347             val new_elemss = filter (fn (((name, ps), _), _) =>
  2348                 not (test_global_registration thy (name, inst_parms ps))) (ids_elemss);
  2349             fun activate_assumed_id (((_, Derived _), _), _) thy = thy
  2350               | activate_assumed_id ((((name, ps), Assumed _), _), thms) thy = let
  2351                 val ps' = inst_parms ps;
  2352               in
  2353                 if test_global_registration thy (name, ps')
  2354                 then thy
  2355                 else thy
  2356                   |> put_global_registration (name, ps') (phi_name, param_prefix name ps) (exp, imp)
  2357                   |> fold (fn witn => fn thy => add_global_witness (name, ps')
  2358                      (Element.morph_witness (Element.inst_morphism thy insts) witn) thy) thms
  2359               end;
  2360 
  2361             fun activate_derived_id ((_, Assumed _), _) thy = thy
  2362               | activate_derived_id (((name, ps), Derived ths), _) thy = let
  2363                 val ps' = inst_parms ps;
  2364               in
  2365                 if test_global_registration thy (name, ps')
  2366                 then thy
  2367                 else thy
  2368                   |> put_global_registration (name, ps') (phi_name, param_prefix name ps) (exp, imp)
  2369                   |> fold (fn witn => fn thy => add_global_witness (name, ps')
  2370                        (witn |> Element.map_witness (fn (t, th) =>  (* FIXME *)
  2371                        (Element.inst_term insts t,
  2372                         disch (Element.inst_thm thy insts (satisfy th))))) thy) ths
  2373               end;
  2374 
  2375             fun activate_elem (loc, ps) (Notes (kind, facts)) thy =
  2376                 let
  2377                   val att_morphism =
  2378                     Morphism.name_morphism (name_morph phi_name param_prfx) $>
  2379                     Morphism.thm_morphism satisfy $>
  2380                     Element.inst_morphism thy insts $>
  2381                     Morphism.thm_morphism disch;
  2382                   val facts' = facts
  2383                     |> Attrib.map_facts (Attrib.attribute_i thy o Args.morph_values att_morphism)
  2384                     |> (map o apsnd o map o apfst o map) (disch o Element.inst_thm thy insts o satisfy)
  2385                     |> (map o apfst o apfst) (name_morph phi_name param_prfx);
  2386                 in
  2387                   thy
  2388                   |> global_note_qualified kind facts'
  2389                   |> snd
  2390                 end
  2391               | activate_elem _ _ thy = thy;
  2392 
  2393             fun activate_elems ((id, _), elems) thy = fold (activate_elem id) elems thy;
  2394 
  2395           in thy |> fold activate_assumed_id ids_elemss_thmss
  2396                  |> fold activate_derived_id ids_elemss
  2397                  |> fold activate_elems new_elemss end;
  2398       in
  2399         thy |> fold activate_id ids_elemss_thmss
  2400             |> fold activate_reg regs
  2401       end;
  2402 
  2403   in (propss, activate) end;
  2404 
  2405 fun prep_propp propss = propss |> map (fn (_, props) =>
  2406   map (rpair [] o Element.mark_witness) props);
  2407 
  2408 fun prep_result propps thmss =
  2409   ListPair.map (fn ((_, props), thms) => map2 Element.make_witness props thms) (propps, thmss);
  2410 
  2411 fun gen_interpretation prep_registration after_qed prfx raw_expr raw_insts thy =
  2412   (* prfx = (flag indicating full qualification, name prefix) *)
  2413   let
  2414     val (propss, activate, morphs) = prep_registration thy prfx raw_expr raw_insts;
  2415     fun after_qed' results =
  2416       ProofContext.theory (activate (prep_result propss results))
  2417       #> after_qed;
  2418   in
  2419     thy
  2420     |> ProofContext.init
  2421     |> Proof.theorem_i NONE after_qed' (prep_propp propss)
  2422     |> Element.refine_witness
  2423     |> Seq.hd
  2424     |> pair morphs
  2425   end;
  2426 
  2427 fun gen_interpret prep_registration after_qed name_morph expr insts int state =
  2428   let
  2429     val _ = Proof.assert_forward_or_chain state;
  2430     val ctxt = Proof.context_of state;
  2431     val (propss, activate, morphs) = prep_registration ctxt name_morph expr insts;
  2432     fun after_qed' results =
  2433       Proof.map_context (K (ctxt |> activate (prep_result propss results)))
  2434       #> Proof.put_facts NONE
  2435       #> after_qed;
  2436   in
  2437     state
  2438     |> Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i
  2439       "interpret" NONE after_qed' (map (pair (Name.no_binding, [])) (prep_propp propss))
  2440     |> Element.refine_witness |> Seq.hd
  2441     |> pair morphs
  2442   end;
  2443 
  2444 fun standard_name_morph interp_prfx b =
  2445   if Binding.is_nothing b then b
  2446   else Binding.map_prefix (fn ((lprfx, _) :: pprfx) =>
  2447     fold (Binding.add_prefix false o fst) pprfx
  2448     #> interp_prfx <> "" ? Binding.add_prefix true interp_prfx
  2449     #> Binding.add_prefix false lprfx
  2450   ) b;
  2451 
  2452 in
  2453 
  2454 val interpretation = gen_interpretation prep_global_registration;
  2455 fun interpretation_cmd interp_prfx = snd ooo gen_interpretation prep_global_registration_cmd
  2456   I (standard_name_morph interp_prfx);
  2457 
  2458 fun interpretation_in_locale after_qed (raw_target, expr) thy =
  2459   let
  2460     val target = intern thy raw_target;
  2461     val (propss, activate) = prep_registration_in_locale target expr thy;
  2462     val raw_propp = prep_propp propss;
  2463 
  2464     val (_, _, goal_ctxt, propp) = thy
  2465       |> ProofContext.init
  2466       |> cert_context_statement (SOME target) [] raw_propp;
  2467 
  2468     fun after_qed' results =
  2469       ProofContext.theory (activate (prep_result propss results))
  2470       #> after_qed;
  2471   in
  2472     goal_ctxt
  2473     |> Proof.theorem_i NONE after_qed' propp
  2474     |> Element.refine_witness |> Seq.hd
  2475   end;
  2476 
  2477 val interpret = gen_interpret prep_local_registration;
  2478 fun interpret_cmd interp_prfx = snd oooo gen_interpret prep_local_registration_cmd
  2479   Seq.single (standard_name_morph interp_prfx);
  2480 
  2481 end;
  2482 
  2483 end;