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