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