src/Pure/Isar/locale.ML

global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
theorem/interpretation: slightly more uniform treatment of after_qeds;
theorem conclusion: proper fix_frees;

(*  Title:      Pure/Isar/locale.ML
    ID:         $Id$
    Author:     Clemens Ballarin, TU Muenchen; Markus Wenzel, LMU/TU Muenchen

Locales -- Isar proof contexts as meta-level predicates, with local
syntax and implicit structures.

Draws basic ideas from Florian Kammueller's original version of
locales, but uses the richer infrastructure of Isar instead of the raw
meta-logic.  Furthermore, structured import of contexts (with merge
and rename operations) are provided, as well as type-inference of the
signature parts, and predicate definitions of the specification text.

Interpretation enables the reuse of theorems of locales in other
contexts, namely those defined by theories, structured proofs and
locales themselves.

See also:

[1] Clemens Ballarin. Locales and Locale Expressions in Isabelle/Isar.
    In Stefano Berardi et al., Types for Proofs and Programs: International
    Workshop, TYPES 2003, Torino, Italy, LNCS 3085, pages 34-50, 2004.
[2] Clemens Ballarin. Interpretation of Locales in Isabelle: Managing
    Dependencies between Locales. Technical Report TUM-I0607, Technische
    Universitaet Muenchen, 2006.
[3] Clemens Ballarin. Interpretation of Locales in Isabelle: Theories and
    Proof Contexts. In J.M. Borwein and W.M. Farmer, MKM 2006, LNAI 4108,
    pages 31-43, 2006.
*)

(* TODO:
- beta-eta normalisation of interpretation parameters
- dangling type frees in locales
- test subsumption of interpretations when merging theories
*)

signature LOCALE =
sig
  datatype expr =
    Locale of string |
    Rename of expr * (string * mixfix option) option list |
    Merge of expr list
  val empty: expr
  datatype 'a element = Elem of 'a | Expr of expr

  val intern: theory -> xstring -> string
  val extern: theory -> string -> xstring
  val init: string -> theory -> Proof.context

  (* The specification of a locale *)

  val parameters_of: theory -> string ->
    ((string * typ) * mixfix) list
  val parameters_of_expr: theory -> expr ->
    ((string * typ) * mixfix) list
  val local_asms_of: theory -> string ->
    ((string * Attrib.src list) * term list) list
  val global_asms_of: theory -> string ->
    ((string * Attrib.src list) * term list) list

  (* Processing of locale statements *)
  val read_context_statement: xstring option -> Element.context element list ->
    (string * string list) list list -> Proof.context ->
    string option * Proof.context * Proof.context * (term * term list) list list
  val cert_context_statement: string option -> Element.context_i element list ->
    (term * term list) list list -> Proof.context ->
    string option * Proof.context * Proof.context * (term * term list) list list
  val read_expr: expr -> Element.context list -> Proof.context ->
    Element.context_i list * Proof.context
  val cert_expr: expr -> Element.context_i list -> Proof.context ->
    Element.context_i list * Proof.context

  (* Diagnostic functions *)
  val print_locales: theory -> unit
  val print_locale: theory -> bool -> expr -> Element.context list -> unit
  val print_global_registrations: bool -> string -> theory -> unit
  val print_local_registrations': bool -> string -> Proof.context -> unit
  val print_local_registrations: bool -> string -> Proof.context -> unit

  val add_locale: bool -> bstring -> expr -> Element.context list -> theory
    -> (string * Proof.context (*body context!*)) * theory
  val add_locale_i: bool -> bstring -> expr -> Element.context_i list -> theory
    -> (string * Proof.context (*body context!*)) * theory

  (* Storing results *)
  val note_thmss: string -> xstring ->
    ((string * Attrib.src list) * (thmref * Attrib.src list) list) list ->
    theory -> ((string * thm list) list * (string * thm list) list) * Proof.context
  val note_thmss_i: string -> string ->
    ((string * Attrib.src list) * (thm list * Attrib.src list) list) list ->
    theory -> ((string * thm list) list * (string * thm list) list) * Proof.context
  val add_thmss: string -> string ->
    ((string * Attrib.src list) * (thm list * Attrib.src list) list) list ->
    Proof.context ->
    ((string * thm list) list * (string * thm list) list) * Proof.context
  val add_term_syntax: string -> (Proof.context -> Proof.context) -> Proof.context -> Proof.context

  val theorem: string -> Method.text option ->
    (thm list list -> Proof.context -> Proof.context) ->
    string * Attrib.src list -> Element.context element list -> Element.statement ->
    theory -> Proof.state
  val theorem_i: string -> Method.text option ->
    (thm list list -> Proof.context -> Proof.context) ->
    string * Attrib.src list -> Element.context_i element list -> Element.statement_i ->
    theory -> Proof.state
  val theorem_in_locale: string -> Method.text option ->
    (thm list list -> thm list list -> Proof.context -> Proof.context) ->
    xstring -> string * Attrib.src list -> Element.context element list -> Element.statement ->
    theory -> Proof.state
  val theorem_in_locale_i: string -> Method.text option ->
    (thm list list -> thm list list -> Proof.context -> Proof.context) ->
    string -> string * Attrib.src list -> Element.context_i element list ->
    Element.statement_i -> theory -> Proof.state
  val smart_theorem: string -> xstring option ->
    string * Attrib.src list -> Element.context element list -> Element.statement ->
    theory -> Proof.state
  val interpretation: (Proof.context -> Proof.context) ->
    string * Attrib.src list -> expr -> string option list ->
    theory -> Proof.state
  val interpretation_in_locale: (Proof.context -> Proof.context) ->
    xstring * expr -> theory -> Proof.state
  val interpret: (Proof.state -> Proof.state Seq.seq) ->
    string * Attrib.src list -> expr -> string option list ->
    bool -> Proof.state -> Proof.state
end;

structure Locale: LOCALE =
struct

fun legacy_unvarifyT thm =
  let
    val cT = Thm.ctyp_of (Thm.theory_of_thm thm);
    val tvars = rev (Drule.fold_terms Term.add_tvars thm []);
    val tfrees = map (fn ((x, _), S) => SOME (cT (TFree (x, S)))) tvars;
  in Drule.instantiate' tfrees [] thm end;

fun legacy_unvarify raw_thm =
  let
    val thm = legacy_unvarifyT raw_thm;
    val ct = Thm.cterm_of (Thm.theory_of_thm thm);
    val vars = rev (Drule.fold_terms Term.add_vars thm []);
    val frees = map (fn ((x, _), T) => SOME (ct (Free (x, T)))) vars;
  in Drule.instantiate' [] frees thm end;


(** locale elements and expressions **)

datatype ctxt = datatype Element.ctxt;

datatype expr =
  Locale of string |
  Rename of expr * (string * mixfix option) option list |
  Merge of expr list;

val empty = Merge [];

datatype 'a element =
  Elem of 'a | Expr of expr;

fun map_elem f (Elem e) = Elem (f e)
  | map_elem _ (Expr e) = Expr e;

type locale =
 {axiom: Element.witness list,
    (* For locales that define predicates this is [A [A]], where A is the locale
       specification.  Otherwise [].
       Only required to generate the right witnesses for locales with predicates. *)
  import: expr,                                                     (*dynamic import*)
  elems: (Element.context_i * stamp) list,
    (* Static content, neither Fixes nor Constrains elements *)
  params: ((string * typ) * mixfix) list,                           (*all params*)
  lparams: string list,                                             (*local params*)
  term_syntax: ((Proof.context -> Proof.context) * stamp) list, (* FIXME depend on morphism *)
  regs: ((string * string list) * Element.witness list) list,
    (* Registrations: indentifiers and witnesses of locales interpreted in the locale. *)
  intros: thm list * thm list}
    (* Introduction rules: of delta predicate and locale predicate. *)

(* CB: an internal (Int) locale element was either imported or included,
   an external (Ext) element appears directly in the locale text. *)

datatype ('a, 'b) int_ext = Int of 'a | Ext of 'b;



(** management of registrations in theories and proof contexts **)

structure Registrations :
  sig
    type T
    val empty: T
    val join: T * T -> T
    val dest: theory -> T ->
      (term list * ((string * Attrib.src list) * Element.witness list)) list
    val lookup: theory -> T * term list ->
      ((string * Attrib.src list) * Element.witness list) option
    val insert: theory -> term list * (string * Attrib.src list) -> T ->
      T * (term list * ((string * Attrib.src list) * Element.witness list)) list
    val add_witness: term list -> Element.witness -> T -> T
  end =
struct
  (* a registration consists of theorems (actually, witnesses) instantiating locale
     assumptions and prefix and attributes, indexed by parameter instantiation *)
  type T = ((string * Attrib.src list) * Element.witness list) Termtab.table;

  val empty = Termtab.empty;

  (* term list represented as single term, for simultaneous matching *)
  fun termify ts =
    Term.list_comb (Const ("", map fastype_of ts ---> propT), ts);
  fun untermify t =
    let fun ut (Const _) ts = ts
          | ut (s $ t) ts = ut s (t::ts)
    in ut t [] end;

  (* joining of registrations: prefix and attributes of left theory,
     thms are equal, no attempt to subsumption testing *)
  fun join (r1, r2) = Termtab.join (fn _ => fn (reg, _) => reg) (r1, r2);

  fun dest_transfer thy regs =
    Termtab.dest regs |> map (apsnd (apsnd (map (Element.transfer_witness thy))));

  fun dest thy regs = dest_transfer thy regs |> map (apfst untermify);

  (* registrations that subsume t *)
  fun subsumers thy t regs =
    filter (fn (t', _) => Pattern.matches thy (t', t)) (dest_transfer thy regs);

  (* look up registration, pick one that subsumes the query *)
  fun lookup thy (regs, ts) =
    let
      val t = termify ts;
      val subs = subsumers thy t regs;
    in (case subs of
        [] => NONE
      | ((t', (attn, thms)) :: _) => let
            val (tinst, inst) = Pattern.match thy (t', t) (Vartab.empty, Vartab.empty);
            (* thms contain Frees, not Vars *)
            val tinst' = tinst |> Vartab.dest
                 |> map (fn ((x, 0), (_, T)) => (x, Logic.legacy_unvarifyT T))
                 |> Symtab.make;
            val inst' = inst |> Vartab.dest
                 |> map (fn ((x, 0), (_, t)) => (x, Logic.legacy_unvarify t))
                 |> Symtab.make;
          in
            SOME (attn, map (Element.inst_witness thy (tinst', inst')) thms)
          end)
    end;

  (* add registration if not subsumed by ones already present,
     additionally returns registrations that are strictly subsumed *)
  fun insert thy (ts, attn) regs =
    let
      val t = termify ts;
      val subs = subsumers thy t regs ;
    in (case subs of
        [] => let
                val sups =
                  filter (fn (t', _) => Pattern.matches thy (t, t')) (dest_transfer thy regs);
                val sups' = map (apfst untermify) sups
              in (Termtab.update (t, (attn, [])) regs, sups') end
      | _ => (regs, []))
    end;

  (* add witness theorem to registration,
     only if instantiation is exact, otherwise exception Option raised *)
  fun add_witness ts thm regs =
    let
      val t = termify ts;
      val (x, thms) = the (Termtab.lookup regs t);
    in
      Termtab.update (t, (x, thm::thms)) regs
    end;
end;


(** theory data **)

structure GlobalLocalesData = TheoryDataFun
(struct
  val name = "Isar/locales";
  type T = NameSpace.T * locale Symtab.table * Registrations.T Symtab.table;
    (* 1st entry: locale namespace,
       2nd entry: locales of the theory,
       3rd entry: registrations, indexed by locale name *)

  val empty = (NameSpace.empty, Symtab.empty, Symtab.empty);
  val copy = I;
  val extend = I;

  fun join_locs _ ({axiom, import, elems, params, lparams, term_syntax, regs, intros}: locale,
      {elems = elems', term_syntax = term_syntax', regs = regs', ...}: locale) =
     {axiom = axiom,
      import = import,
      elems = gen_merge_lists (eq_snd (op =)) elems elems',
      params = params,
      lparams = lparams,
      term_syntax = Library.merge (eq_snd (op =)) (term_syntax, term_syntax'),
      regs = merge_alists regs regs',
      intros = intros};
  fun merge _ ((space1, locs1, regs1), (space2, locs2, regs2)) =
    (NameSpace.merge (space1, space2), Symtab.join join_locs (locs1, locs2),
     Symtab.join (K Registrations.join) (regs1, regs2));

  fun print _ (space, locs, _) =
    Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (space, locs)))
    |> Pretty.writeln;
end);

val _ = Context.add_setup GlobalLocalesData.init;



(** context data **)

structure LocalLocalesData = ProofDataFun
(struct
  val name = "Isar/locales";
  type T = Registrations.T Symtab.table;
    (* registrations, indexed by locale name *)
  fun init _ = Symtab.empty;
  fun print _ _ = ();
end);

val _ = Context.add_setup LocalLocalesData.init;


(* access locales *)

val print_locales = GlobalLocalesData.print;

val intern = NameSpace.intern o #1 o GlobalLocalesData.get;
val extern = NameSpace.extern o #1 o GlobalLocalesData.get;

fun declare_locale name thy =
  thy |> GlobalLocalesData.map (fn (space, locs, regs) =>
    (Sign.declare_name thy name space, locs, regs));

fun put_locale name loc =
  GlobalLocalesData.map (fn (space, locs, regs) =>
    (space, Symtab.update (name, loc) locs, regs));

fun get_locale thy name = Symtab.lookup (#2 (GlobalLocalesData.get thy)) name;

fun the_locale thy name =
  (case get_locale thy name of
    SOME loc => loc
  | NONE => error ("Unknown locale " ^ quote name));

fun change_locale name f thy =
  let
    val {axiom, import, elems, params, lparams, term_syntax, regs, intros} =
        the_locale thy name;
    val (axiom', import', elems', params', lparams', term_syntax', regs', intros') =
      f (axiom, import, elems, params, lparams, term_syntax, regs, intros);
  in
    put_locale name {axiom = axiom', import = import', elems = elems',
      params = params', lparams = lparams', term_syntax = term_syntax', regs = regs',
      intros = intros'} thy
  end;


(* access registrations *)

(* Ids of global registrations are varified,
   Ids of local registrations are not.
   Thms of registrations are never varified. *)

(* retrieve registration from theory or context *)

fun gen_get_registrations get thy_of thy_ctxt name =
  case Symtab.lookup (get thy_ctxt) name of
      NONE => []
    | SOME reg => Registrations.dest (thy_of thy_ctxt) reg;

val get_global_registrations =
     gen_get_registrations (#3 o GlobalLocalesData.get) I;
val get_local_registrations =
     gen_get_registrations LocalLocalesData.get ProofContext.theory_of;

fun gen_get_registration get thy_of thy_ctxt (name, ps) =
  case Symtab.lookup (get thy_ctxt) name of
      NONE => NONE
    | SOME reg => Registrations.lookup (thy_of thy_ctxt) (reg, ps);

val get_global_registration =
     gen_get_registration (#3 o GlobalLocalesData.get) I;
val get_local_registration =
     gen_get_registration LocalLocalesData.get ProofContext.theory_of;

val test_global_registration = is_some oo get_global_registration;
val test_local_registration = is_some oo get_local_registration;
fun smart_test_registration ctxt id =
  let
    val thy = ProofContext.theory_of ctxt;
  in
    test_global_registration thy id orelse test_local_registration ctxt id
  end;


(* add registration to theory or context, ignored if subsumed *)

fun gen_put_registration map_data thy_of (name, ps) attn thy_ctxt =
  map_data (fn regs =>
    let
      val thy = thy_of thy_ctxt;
      val reg = the_default Registrations.empty (Symtab.lookup regs name);
      val (reg', sups) = Registrations.insert thy (ps, attn) reg;
      val _ = if not (null sups) then warning
                ("Subsumed interpretation(s) of locale " ^
                 quote (extern thy name) ^
                 "\nby interpretation(s) with the following prefix(es):\n" ^
                  commas_quote (map (fn (_, ((s, _), _)) => s) sups))
              else ();
    in Symtab.update (name, reg') regs end) thy_ctxt;

val put_global_registration =
     gen_put_registration (fn f =>
       GlobalLocalesData.map (fn (space, locs, regs) => (space, locs, f regs))) I;
val put_local_registration =
     gen_put_registration LocalLocalesData.map ProofContext.theory_of;

fun put_registration_in_locale name id =
  change_locale name (fn (axiom, import, elems, params, lparams, term_syntax, regs, intros) =>
    (axiom, import, elems, params, lparams, term_syntax, regs @ [(id, [])], intros));


(* add witness theorem to registration in theory or context,
   ignored if registration not present *)

fun add_witness (name, ps) thm =
  Symtab.map_entry name (Registrations.add_witness ps thm);

fun add_global_witness id thm =
  GlobalLocalesData.map (fn (space, locs, regs) => (space, locs, add_witness id thm regs));

val add_local_witness = LocalLocalesData.map oo add_witness;

fun add_witness_in_locale name id thm =
  change_locale name (fn (axiom, import, elems, params, lparams, term_syntax, regs, intros) =>
    let
      fun add (id', thms) =
        if id = id' then (id', thm :: thms) else (id', thms);
    in (axiom, import, elems, params, lparams, term_syntax, map add regs, intros) end);


(* printing of registrations *)

fun gen_print_registrations get_regs mk_ctxt msg show_wits loc thy_ctxt =
  let
    val ctxt = mk_ctxt thy_ctxt;
    val thy = ProofContext.theory_of ctxt;

    val prt_term = Pretty.quote o ProofContext.pretty_term ctxt;
    fun prt_inst ts =
        Pretty.enclose "(" ")" (Pretty.breaks (map prt_term ts));
    fun prt_attn (prfx, atts) =
        Pretty.breaks (Pretty.str prfx :: Args.pretty_attribs ctxt atts);
    fun prt_witns witns = Pretty.enclose "[" "]"
      (Pretty.breaks (map (prt_term o Element.witness_prop) witns));
    fun prt_reg (ts, (("", []), witns)) =
        if show_wits
          then Pretty.block [prt_inst ts, Pretty.fbrk, prt_witns witns]
          else prt_inst ts
      | prt_reg (ts, (attn, witns)) =
        if show_wits
          then Pretty.block ((prt_attn attn @
            [Pretty.str ":", Pretty.brk 1, prt_inst ts, Pretty.fbrk,
              prt_witns witns]))
          else Pretty.block ((prt_attn attn @
            [Pretty.str ":", Pretty.brk 1, prt_inst ts]));

    val loc_int = intern thy loc;
    val regs = get_regs thy_ctxt;
    val loc_regs = Symtab.lookup regs loc_int;
  in
    (case loc_regs of
        NONE => Pretty.str ("no interpretations in " ^ msg)
      | SOME r => let
            val r' = Registrations.dest thy r;
            val r'' = Library.sort_wrt (fn (_, ((prfx, _), _)) => prfx) r';
          in Pretty.big_list ("interpretations in " ^ msg ^ ":")
            (map prt_reg r'')
          end)
    |> Pretty.writeln
  end;

val print_global_registrations =
     gen_print_registrations (#3 o GlobalLocalesData.get)
       ProofContext.init "theory";
val print_local_registrations' =
     gen_print_registrations LocalLocalesData.get
       I "context";
fun print_local_registrations show_wits loc ctxt =
  (print_global_registrations show_wits loc (ProofContext.theory_of ctxt);
   print_local_registrations' show_wits loc ctxt);


(* diagnostics *)

fun err_in_locale ctxt msg ids =
  let
    val thy = ProofContext.theory_of ctxt;
    fun prt_id (name, parms) =
      [Pretty.block (Pretty.breaks (map Pretty.str (extern thy name :: parms)))];
    val prt_ids = flat (separate [Pretty.str " +", Pretty.brk 1] (map prt_id ids));
    val err_msg =
      if forall (equal "" o #1) ids then msg
      else msg ^ "\n" ^ Pretty.string_of (Pretty.block
        (Pretty.str "The error(s) above occurred in locale:" :: Pretty.brk 1 :: prt_ids));
  in error err_msg end;

fun err_in_locale' ctxt msg ids' = err_in_locale ctxt msg (map fst ids');


fun pretty_ren NONE = Pretty.str "_"
  | pretty_ren (SOME (x, NONE)) = Pretty.str x
  | pretty_ren (SOME (x, SOME syn)) =
      Pretty.block [Pretty.str x, Pretty.brk 1, Syntax.pretty_mixfix syn];

fun pretty_expr thy (Locale name) = Pretty.str (extern thy name)
  | pretty_expr thy (Rename (expr, xs)) =
      Pretty.block [pretty_expr thy expr, Pretty.brk 1, Pretty.block (map pretty_ren xs |> Pretty.breaks)]
  | pretty_expr thy (Merge es) =
      Pretty.separate "+" (map (pretty_expr thy) es) |> Pretty.block;

fun err_in_expr _ msg (Merge []) = error msg
  | err_in_expr ctxt msg expr =
    error (msg ^ "\n" ^ Pretty.string_of (Pretty.block
      [Pretty.str "The error(s) above occured in locale expression:", Pretty.brk 1,
       pretty_expr (ProofContext.theory_of ctxt) expr]));


(** structured contexts: rename + merge + implicit type instantiation **)

(* parameter types *)

fun frozen_tvars ctxt Ts =
  #1 (Variable.importT_inst (map Logic.mk_type Ts) ctxt)
  |> map (fn ((xi, S), T) => (xi, (S, T)));

fun unify_frozen ctxt maxidx Ts Us =
  let
    fun paramify NONE i = (NONE, i)
      | paramify (SOME T) i = apfst SOME (TypeInfer.paramify_dummies T i);

    val (Ts', maxidx') = fold_map paramify Ts maxidx;
    val (Us', maxidx'') = fold_map paramify Us maxidx';
    val thy = ProofContext.theory_of ctxt;

    fun unify (SOME T, SOME U) env = (Sign.typ_unify thy (U, T) env
          handle Type.TUNIFY => raise TYPE ("unify_frozen: failed to unify types", [U, T], []))
      | unify _ env = env;
    val (unifier, _) = fold unify (Ts' ~~ Us') (Vartab.empty, maxidx'');
    val Vs = map (Option.map (Envir.norm_type unifier)) Us';
    val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map_filter I Vs));
  in map (Option.map (Envir.norm_type unifier')) Vs end;

fun params_of elemss = distinct (eq_fst (op = : string * string -> bool)) (maps (snd o fst) elemss);
fun params_of' elemss = distinct (eq_fst (op = : string * string -> bool)) (maps (snd o fst o fst) elemss);


(* CB: param_types has the following type:
  ('a * 'b option) list -> ('a * 'b) list *)
fun param_types ps = map_filter (fn (_, NONE) => NONE | (x, SOME T) => SOME (x, T)) ps;


fun merge_syntax ctxt ids ss = Symtab.merge (op = : mixfix * mixfix -> bool) ss
  handle Symtab.DUPS xs => err_in_locale ctxt
    ("Conflicting syntax for parameter(s): " ^ commas_quote xs) (map fst ids);


(* Distinction of assumed vs. derived identifiers.
   The former may have axioms relating assumptions of the context to
   assumptions of the specification fragment (for locales with
   predicates).  The latter have witnesses relating assumptions of the
   specification fragment to assumptions of other (assumed) specification
   fragments. *)

datatype 'a mode = Assumed of 'a | Derived of 'a;

fun map_mode f (Assumed x) = Assumed (f x)
  | map_mode f (Derived x) = Derived (f x);


(* flatten expressions *)

local

fun unify_parms ctxt fixed_parms raw_parmss =
  let
    val thy = ProofContext.theory_of ctxt;
    val maxidx = length raw_parmss;
    val idx_parmss = (0 upto maxidx - 1) ~~ raw_parmss;

    fun varify i = Term.map_type_tfree (fn (a, S) => TVar ((a, i), S));
    fun varify_parms (i, ps) = map (apsnd (varify i)) (param_types ps);
    val parms = fixed_parms @ maps varify_parms idx_parmss;

    fun unify T U envir = Sign.typ_unify thy (U, T) envir
      handle Type.TUNIFY =>
        let val prt = Sign.string_of_typ thy in
          raise TYPE ("unify_parms: failed to unify types " ^
            prt U ^ " and " ^ prt T, [U, T], [])
        end;
    fun unify_list (T :: Us) = fold (unify T) Us
      | unify_list [] = I;
    val (unifier, _) = fold unify_list (map #2 (Symtab.dest (Symtab.make_list parms)))
      (Vartab.empty, maxidx);

    val parms' = map (apsnd (Envir.norm_type unifier)) (distinct (eq_fst (op =)) parms);
    val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map #2 parms'));

    fun inst_parms (i, ps) =
      foldr Term.add_typ_tfrees [] (map_filter snd ps)
      |> map_filter (fn (a, S) =>
          let val T = Envir.norm_type unifier' (TVar ((a, i), S))
          in if T = TFree (a, S) then NONE else SOME (a, T) end)
      |> Symtab.make;
  in map inst_parms idx_parmss end;

in

fun unify_elemss _ _ [] = []
  | unify_elemss _ [] [elems] = [elems]
  | unify_elemss ctxt fixed_parms elemss =
      let
        val thy = ProofContext.theory_of ctxt;
        val envs = unify_parms ctxt fixed_parms (map (snd o fst o fst) elemss);
        fun inst ((((name, ps), mode), elems), env) =
          (((name, map (apsnd (Option.map (Element.instT_type env))) ps),
              map_mode (map (Element.instT_witness thy env)) mode),
            map (Element.instT_ctxt thy env) elems);
      in map inst (elemss ~~ envs) end;


fun renaming xs parms = zip_options parms xs
  handle Library.UnequalLengths =>
    error ("Too many arguments in renaming: " ^
      commas (map (fn NONE => "_" | SOME x => quote (fst x)) xs));


(* params_of_expr:
   Compute parameters (with types and syntax) of locale expression.
*)

fun params_of_expr ctxt fixed_params expr (prev_parms, prev_types, prev_syn) =
  let
    val thy = ProofContext.theory_of ctxt;

    fun merge_tenvs fixed tenv1 tenv2 =
        let
          val [env1, env2] = unify_parms ctxt fixed
                [tenv1 |> Symtab.dest |> map (apsnd SOME),
                 tenv2 |> Symtab.dest |> map (apsnd SOME)]
        in
          Symtab.merge (op =) (Symtab.map (Element.instT_type env1) tenv1,
            Symtab.map (Element.instT_type env2) tenv2)
        end;

    fun merge_syn expr syn1 syn2 =
        Symtab.merge (op = : mixfix * mixfix -> bool) (syn1, syn2)
        handle Symtab.DUPS xs => err_in_expr ctxt
          ("Conflicting syntax for parameter(s): " ^ commas_quote xs) expr;

    fun params_of (expr as Locale name) =
          let
            val {import, params, ...} = the_locale thy name;
            val parms = map (fst o fst) params;
            val (parms', types', syn') = params_of import;
            val all_parms = merge_lists parms' parms;
            val all_types = merge_tenvs [] types' (params |> map fst |> Symtab.make);
            val all_syn = merge_syn expr syn' (params |> map (apfst fst) |> Symtab.make);
          in (all_parms, all_types, all_syn) end
      | params_of (expr as Rename (e, xs)) =
          let
            val (parms', types', syn') = params_of e;
            val ren = renaming xs parms';
            (* renaming may reduce number of parameters *)
            val new_parms = map (Element.rename ren) parms' |> distinct (op =);
            val ren_syn = syn' |> Symtab.dest |> map (Element.rename_var ren);
            val new_syn = fold (Symtab.insert (op =)) ren_syn Symtab.empty
                handle Symtab.DUP x =>
                  err_in_expr ctxt ("Conflicting syntax for parameter: " ^ quote x) expr;
            val syn_types = map (apsnd (fn mx => SOME (Type.freeze_type (#1 (TypeInfer.paramify_dummies (TypeInfer.mixfixT mx) 0))))) (Symtab.dest new_syn);
            val ren_types = types' |> Symtab.dest |> map (apfst (Element.rename ren));
            val (env :: _) = unify_parms ctxt []
                ((ren_types |> map (apsnd SOME)) :: map single syn_types);
            val new_types = fold (Symtab.insert (op =))
                (map (apsnd (Element.instT_type env)) ren_types) Symtab.empty;
          in (new_parms, new_types, new_syn) end
      | params_of (Merge es) =
          fold (fn e => fn (parms, types, syn) =>
                   let
                     val (parms', types', syn') = params_of e
                   in
                     (merge_lists parms parms', merge_tenvs [] types types',
                      merge_syn e syn syn')
                   end)
            es ([], Symtab.empty, Symtab.empty)

      val (parms, types, syn) = params_of expr;
    in
      (merge_lists prev_parms parms, merge_tenvs fixed_params prev_types types,
       merge_syn expr prev_syn syn)
    end;

fun make_params_ids params = [(("", params), ([], Assumed []))];
fun make_raw_params_elemss (params, tenv, syn) =
    [((("", map (fn p => (p, Symtab.lookup tenv p)) params), Assumed []),
      Int [Fixes (map (fn p =>
        (p, Symtab.lookup tenv p, Symtab.lookup syn p |> the)) params)])];


(* flatten_expr:
   Extend list of identifiers by those new in locale expression expr.
   Compute corresponding list of lists of locale elements (one entry per
   identifier).

   Identifiers represent locale fragments and are in an extended form:
     ((name, ps), (ax_ps, axs))
   (name, ps) is the locale name with all its parameters.
   (ax_ps, axs) is the locale axioms with its parameters;
     axs are always taken from the top level of the locale hierarchy,
     hence axioms may contain additional parameters from later fragments:
     ps subset of ax_ps.  axs is either singleton or empty.

   Elements are enriched by identifier-like information:
     (((name, ax_ps), axs), elems)
   The parameters in ax_ps are the axiom parameters, but enriched by type
   info: now each entry is a pair of string and typ option.  Axioms are
   type-instantiated.

*)

fun flatten_expr ctxt ((prev_idents, prev_syntax), expr) =
  let
    val thy = ProofContext.theory_of ctxt;

    fun rename_parms top ren ((name, ps), (parms, mode)) =
        ((name, map (Element.rename ren) ps),
         if top
         then (map (Element.rename ren) parms,
               map_mode (map (Element.rename_witness ren)) mode)
         else (parms, mode));

    (* add (name, ps) and its registrations, recursively; adjust hyps of witnesses *)

    fun add_with_regs ((name, pTs), mode) (wits, ids, visited) =
        if member (fn (a, (b, _)) => a = b) visited (name, map #1 pTs)
        then (wits, ids, visited)
        else
          let
            val {params, regs, ...} = the_locale thy name;
            val pTs' = map #1 params;
            val ren = map #1 pTs' ~~ map (fn (x, _) => (x, NONE)) pTs;
              (* dummy syntax, since required by rename *)
            val pTs'' = map (fn ((p, _), (_, T)) => (p, T)) (pTs ~~ pTs');
            val [env] = unify_parms ctxt pTs [map (apsnd SOME) pTs''];
              (* propagate parameter types, to keep them consistent *)
            val regs' = map (fn ((name, ps), wits) =>
                ((name, map (Element.rename ren) ps),
                 map (Element.transfer_witness thy) wits)) regs;
            val new_regs = regs';
            val new_ids = map fst new_regs;
            val new_idTs = map (apsnd (map (fn p => (p, (the o AList.lookup (op =) pTs) p)))) new_ids;

            val new_wits = new_regs |> map (#2 #> map
              (Element.instT_witness thy env #> Element.rename_witness ren #>
                Element.satisfy_witness wits));
            val new_ids' = map (fn (id, wits) =>
                (id, ([], Derived wits))) (new_ids ~~ new_wits);
            val new_idTs' = map (fn ((n, pTs), (_, ([], mode))) =>
                ((n, pTs), mode)) (new_idTs ~~ new_ids');
            val new_id = ((name, map #1 pTs), ([], mode));
            val (wits', ids', visited') = fold add_with_regs new_idTs'
              (wits @ flat new_wits, ids, visited @ [new_id]);
          in
            (wits', ids' @ [new_id], visited')
          end;

    (* distribute top-level axioms over assumed ids *)

    fun axiomify all_ps ((name, parms), (_, Assumed _)) axioms =
        let
          val {elems, ...} = the_locale thy name;
          val ts = maps
            (fn (Assumes asms, _) => maps (map #1 o #2) asms
              | _ => [])
            elems;
          val (axs1, axs2) = chop (length ts) axioms;
        in (((name, parms), (all_ps, Assumed axs1)), axs2) end
      | axiomify all_ps (id, (_, Derived ths)) axioms =
          ((id, (all_ps, Derived ths)), axioms);

    (* identifiers of an expression *)

    fun identify top (Locale name) =
    (* CB: ids_ax is a list of tuples of the form ((name, ps), axs),
       where name is a locale name, ps a list of parameter names and axs
       a list of axioms relating to the identifier, axs is empty unless
       identify at top level (top = true);
       parms is accumulated list of parameters *)
          let
            val {axiom, import, params, ...} = the_locale thy name;
            val ps = map (#1 o #1) params;
            val (ids', parms') = identify false import;
                (* acyclic import dependencies *)

            val (_, ids'', _) = add_with_regs ((name, map #1 params), Assumed []) ([], ids', ids');
            val ids_ax = if top then fst (fold_map (axiomify ps) ids'' axiom) else ids'';
            in (ids_ax, merge_lists parms' ps) end
      | identify top (Rename (e, xs)) =
          let
            val (ids', parms') = identify top e;
            val ren = renaming xs parms'
              handle ERROR msg => err_in_locale' ctxt msg ids';

            val ids'' = distinct (eq_fst (op =)) (map (rename_parms top ren) ids');
            val parms'' = distinct (op =) (maps (#2 o #1) ids'');
          in (ids'', parms'') end
      | identify top (Merge es) =
          fold (fn e => fn (ids, parms) =>
                   let
                     val (ids', parms') = identify top e
                   in
                     (merge_alists ids ids', merge_lists parms parms')
                   end)
            es ([], []);

    fun inst_wit all_params (t, th) = let
         val {hyps, prop, ...} = Thm.rep_thm th;
         val ps = map (apsnd SOME) (fold Term.add_frees (prop :: hyps) []);
         val [env] = unify_parms ctxt all_params [ps];
         val t' = Element.instT_term env t;
         val th' = Element.instT_thm thy env th;
       in (t', th') end;

    fun eval all_params tenv syn ((name, params), (locale_params, mode)) =
      let
        val {params = ps_mx, elems = elems_stamped, ...} = the_locale thy name;
        val elems = map fst elems_stamped;
        val ps = map fst ps_mx;
        fun lookup_syn x = (case Symtab.lookup syn x of SOME Structure => NONE | opt => opt);
        val locale_params' = map (fn p => (p, Symtab.lookup tenv p |> the)) locale_params;
        val mode' = map_mode (map (Element.map_witness (inst_wit all_params))) mode;
        val ren = map fst ps ~~ map (fn p => (p, lookup_syn p)) params;
        val [env] = unify_parms ctxt all_params [map (apfst (Element.rename ren) o apsnd SOME) ps];
        val elems' = elems
              |> map (Element.rename_ctxt ren)
              |> map (Element.map_ctxt {var = I, typ = I, term = I, fact = I, attrib = I,
                   name = NameSpace.qualified (space_implode "_" params)})
              |> map (Element.instT_ctxt thy env)
      in (((name, map (apsnd SOME) locale_params'), mode'), elems') end;

    (* parameters, their types and syntax *)
    val (all_params', tenv, syn) = params_of_expr ctxt [] expr ([], Symtab.empty, Symtab.empty);
    val all_params = map (fn p => (p, Symtab.lookup tenv p |> the)) all_params';
    (* compute identifiers and syntax, merge with previous ones *)
    val (ids, _) = identify true expr;
    val idents = gen_rems (eq_fst (op =)) (ids, prev_idents);
    val syntax = merge_syntax ctxt ids (syn, prev_syntax);
    (* type-instantiate elements *)
    val final_elemss = map (eval all_params tenv syntax) idents;
  in ((prev_idents @ idents, syntax), final_elemss) end;

end;


(* activate elements *)

local

fun axioms_export axs _ hyps =
  Element.satisfy_thm axs
  #> Drule.implies_intr_list (Library.drop (length axs, hyps));


(* NB: derived ids contain only facts at this stage *)

fun activate_elem _ _ ((ctxt, mode), Fixes fixes) =
      ((ctxt |> ProofContext.add_fixes_i fixes |> snd, mode), [])
  | activate_elem _ _ ((ctxt, mode), Constrains _) =
      ((ctxt, mode), [])
  | activate_elem ax_in_ctxt _ ((ctxt, Assumed axs), Assumes asms) =
      let
        val asms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) asms;
        val ts = maps (map #1 o #2) asms';
        val (ps, qs) = chop (length ts) axs;
        val (_, ctxt') =
          ctxt |> fold Variable.fix_frees ts
          |> ProofContext.add_assms_i (axioms_export (if ax_in_ctxt then ps else [])) asms';
      in ((ctxt', Assumed qs), []) end
  | activate_elem _ _ ((ctxt, Derived ths), Assumes asms) =
      ((ctxt, Derived ths), [])
  | activate_elem _ _ ((ctxt, Assumed axs), Defines defs) =
      let
        val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
        val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
            let val ((c, _), t') = LocalDefs.cert_def ctxt t
            in (t', ((if name = "" then Thm.def_name c else name, atts), [(t', ps)])) end);
        val (_, ctxt') =
          ctxt |> fold (Variable.fix_frees o #1) asms
          |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms);
      in ((ctxt', Assumed axs), []) end
  | activate_elem _ _ ((ctxt, Derived ths), Defines defs) =
      ((ctxt, Derived ths), [])
  | activate_elem _ is_ext ((ctxt, mode), Notes facts) =
      let
        val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts;
        val (res, ctxt') = ctxt |> ProofContext.note_thmss_i facts';
      in ((ctxt', mode), if is_ext then res else []) end;

fun activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt =
  let
    val thy = ProofContext.theory_of ctxt;
    val ((ctxt', _), res) =
        foldl_map (activate_elem ax_in_ctxt (name = "")) ((ProofContext.qualified_names ctxt, mode), elems)
      handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)]
    val ctxt'' = if name = "" then ctxt'
          else let
              val ps' = map (fn (n, SOME T) => Free (n, T)) ps;
              val ctxt'' = put_local_registration (name, ps') ("", []) ctxt'
            in case mode of
                Assumed axs =>
                  fold (add_local_witness (name, ps') o
                    Element.assume_witness thy o Element.witness_prop) axs ctxt''
              | Derived ths => fold (add_local_witness (name, ps')) ths ctxt''
            end
  in (ProofContext.restore_naming ctxt ctxt'', res) end;

fun activate_elemss ax_in_ctxt prep_facts =
    fold_map (fn (((name, ps), mode), raw_elems) => fn ctxt =>
      let
        val elems = map (prep_facts ctxt) raw_elems;
        val (ctxt', res) = apsnd flat
            (activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt);
        val elems' = elems |> map (Element.map_ctxt
          {name = I, var = I, typ = I, term = I, fact = I, attrib = Args.closure});
      in (((((name, ps), mode), elems'), res), ctxt') end);

in

(* CB: activate_facts prep_facts (ctxt, elemss),
   where elemss is a list of pairs consisting of identifiers and
   context elements, extends ctxt by the context elements yielding
   ctxt' and returns (ctxt', (elemss', facts)).
   Identifiers in the argument are of the form ((name, ps), axs) and
   assumptions use the axioms in the identifiers to set up exporters
   in ctxt'.  elemss' does not contain identifiers and is obtained
   from elemss and the intermediate context with prep_facts.
   If read_facts or cert_facts is used for prep_facts, these also remove
   the internal/external markers from elemss. *)

fun activate_facts ax_in_ctxt prep_facts (ctxt, args) =
  let val ((elemss, factss), ctxt') = activate_elemss ax_in_ctxt prep_facts args ctxt |>> split_list
  in (ctxt', (elemss, flat factss)) end;

end;



(** prepare locale elements **)

(* expressions *)

fun intern_expr thy (Locale xname) = Locale (intern thy xname)
  | intern_expr thy (Merge exprs) = Merge (map (intern_expr thy) exprs)
  | intern_expr thy (Rename (expr, xs)) = Rename (intern_expr thy expr, xs);


(* propositions and bindings *)

(* flatten (ctxt, prep_expr) ((ids, syn), expr)
   normalises expr (which is either a locale
   expression or a single context element) wrt.
   to the list ids of already accumulated identifiers.
   It returns ((ids', syn'), elemss) where ids' is an extension of ids
   with identifiers generated for expr, and elemss is the list of
   context elements generated from expr.
   syn and syn' are symtabs mapping parameter names to their syntax.  syn'
   is an extension of syn.
   For details, see flatten_expr.

   Additionally, for a locale expression, the elems are grouped into a single
   Int; individual context elements are marked Ext.  In this case, the
   identifier-like information of the element is as follows:
   - for Fixes: (("", ps), []) where the ps have type info NONE
   - for other elements: (("", []), []).
   The implementation of activate_facts relies on identifier names being
   empty strings for external elements.
*)

fun flatten (ctxt, _) ((ids, syn), Elem (Fixes fixes)) = let
        val ids' = ids @ [(("", map #1 fixes), ([], Assumed []))]
      in
        ((ids',
         merge_syntax ctxt ids'
           (syn, Symtab.make (map (fn fx => (#1 fx, #3 fx)) fixes))
           handle Symtab.DUPS xs => err_in_locale ctxt
             ("Conflicting syntax for parameters: " ^ commas_quote xs)
             (map #1 ids')),
         [((("", map (rpair NONE o #1) fixes), Assumed []), Ext (Fixes fixes))])
      end
  | flatten _ ((ids, syn), Elem elem) =
      ((ids @ [(("", []), ([], Assumed []))], syn), [((("", []), Assumed []), Ext elem)])
  | flatten (ctxt, prep_expr) ((ids, syn), Expr expr) =
      apsnd (map (apsnd Int)) (flatten_expr ctxt ((ids, syn), prep_expr expr));

local

local

fun declare_int_elem (ctxt, Fixes fixes) =
      (ctxt |> ProofContext.add_fixes_i (map (fn (x, T, mx) =>
        (x, Option.map (Term.map_type_tfree (TypeInfer.param 0)) T, mx)) fixes) |> snd, [])
  | declare_int_elem (ctxt, _) = (ctxt, []);

fun declare_ext_elem prep_vars (ctxt, Fixes fixes) =
      let val (vars, _) = prep_vars fixes ctxt
      in (ctxt |> ProofContext.add_fixes_i vars |> snd, []) end
  | declare_ext_elem prep_vars (ctxt, Constrains csts) =
      let val (_, ctxt') = prep_vars (map (fn (x, T) => (x, SOME T, NoSyn)) csts) ctxt
      in (ctxt', []) end
  | declare_ext_elem _ (ctxt, Assumes asms) = (ctxt, map #2 asms)
  | declare_ext_elem _ (ctxt, Defines defs) = (ctxt, map (fn (_, (t, ps)) => [(t, ps)]) defs)
  | declare_ext_elem _ (ctxt, Notes facts) = (ctxt, []);

fun declare_elems prep_vars (ctxt, (((name, ps), Assumed _), elems)) =
    let val (ctxt', propps) =
      (case elems of
        Int es => foldl_map declare_int_elem (ctxt, es)
      | Ext e => foldl_map (declare_ext_elem prep_vars) (ctxt, [e]))
      handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)]
    in (ctxt', propps) end
  | declare_elems _ (ctxt, ((_, Derived _), elems)) = (ctxt, []);

in

fun declare_elemss prep_vars fixed_params raw_elemss ctxt =
  let
    (* CB: fix of type bug of goal in target with context elements.
       Parameters new in context elements must receive types that are
       distinct from types of parameters in target (fixed_params).  *)
    val ctxt_with_fixed =
      fold Variable.declare_term (map Free fixed_params) ctxt;
    val int_elemss =
      raw_elemss
      |> map_filter (fn (id, Int es) => SOME (id, es) | _ => NONE)
      |> unify_elemss ctxt_with_fixed fixed_params;
    val (_, raw_elemss') =
      foldl_map (fn ((_, es) :: elemss, (id, Int _)) => (elemss, (id, Int es)) | x => x)
        (int_elemss, raw_elemss);
  in foldl_map (declare_elems prep_vars) (ctxt, raw_elemss') end;

end;

local

val norm_term = Envir.beta_norm oo Term.subst_atomic;

fun abstract_thm thy eq =
  Thm.assume (Thm.cterm_of thy eq) |> Drule.gen_all |> Drule.abs_def;

fun bind_def ctxt (name, ps) eq (xs, env, ths) =
  let
    val ((y, T), b) = LocalDefs.abs_def eq;
    val b' = norm_term env b;
    val th = abstract_thm (ProofContext.theory_of ctxt) eq;
    fun err msg = err_in_locale ctxt (msg ^ ": " ^ quote y) [(name, map fst ps)];
  in
    conditional (exists (equal y o #1) xs) (fn () =>
      err "Attempt to define previously specified variable");
    conditional (exists (fn (Free (y', _), _) => y = y' | _ => false) env) (fn () =>
      err "Attempt to redefine variable");
    (Term.add_frees b' xs, (Free (y, T), b') :: env, th :: ths)
  end;


(* CB: for finish_elems (Int and Ext),
   extracts specification, only of assumed elements *)

fun eval_text _ _ _ (Fixes _) text = text
  | eval_text _ _ _ (Constrains _) text = text
  | eval_text _ (_, Assumed _) is_ext (Assumes asms)
        (((exts, exts'), (ints, ints')), (xs, env, defs)) =
      let
        val ts = maps (map #1 o #2) asms;
        val ts' = map (norm_term env) ts;
        val spec' =
          if is_ext then ((exts @ ts, exts' @ ts'), (ints, ints'))
          else ((exts, exts'), (ints @ ts, ints' @ ts'));
      in (spec', (fold Term.add_frees ts' xs, env, defs)) end
  | eval_text _ (_, Derived _) _ (Assumes _) text = text
  | eval_text ctxt (id, Assumed _) _ (Defines defs) (spec, binds) =
      (spec, fold (bind_def ctxt id o #1 o #2) defs binds)
  | eval_text _ (_, Derived _) _ (Defines _) text = text
  | eval_text _ _ _ (Notes _) text = text;


(* for finish_elems (Int),
   remove redundant elements of derived identifiers,
   turn assumptions and definitions into facts,
   adjust hypotheses of facts using witnesses *)

fun finish_derived _ _ (Assumed _) (Fixes fixes) = SOME (Fixes fixes)
  | finish_derived _ _ (Assumed _) (Constrains csts) = SOME (Constrains csts)
  | finish_derived _ _ (Assumed _) (Assumes asms) = SOME (Assumes asms)
  | finish_derived _ _ (Assumed _) (Defines defs) = SOME (Defines defs)

  | finish_derived _ _ (Derived _) (Fixes _) = NONE
  | finish_derived _ _ (Derived _) (Constrains _) = NONE
  | finish_derived sign wits (Derived _) (Assumes asms) = asms
      |> map (apsnd (map (fn (a, _) => ([Thm.assume (cterm_of sign a)], []))))
      |> Notes |> Element.map_ctxt_values I I (Element.satisfy_thm wits) |> SOME
  | finish_derived sign wits (Derived _) (Defines defs) = defs
      |> map (apsnd (fn (d, _) => [([Thm.assume (cterm_of sign d)], [])]))
      |> Notes |> Element.map_ctxt_values I I (Element.satisfy_thm wits) |> SOME

  | finish_derived _ wits _ (Notes facts) = (Notes facts)
      |> Element.map_ctxt_values I I (Element.satisfy_thm wits) |> SOME;

(* CB: for finish_elems (Ext) *)

fun closeup _ false elem = elem
  | closeup ctxt true elem =
      let
        fun close_frees t =
          let val frees = rev (filter_out (Variable.is_fixed ctxt o #1) (Term.add_frees t []))
          in Term.list_all_free (frees, t) end;

        fun no_binds [] = []
          | no_binds _ = error "Illegal term bindings in locale element";
      in
        (case elem of
          Assumes asms => Assumes (asms |> map (fn (a, propps) =>
            (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps)))
        | Defines defs => Defines (defs |> map (fn (a, (t, ps)) =>
            (a, (close_frees (#2 (LocalDefs.cert_def ctxt t)), no_binds ps))))
        | e => e)
      end;


fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (x, _, mx) =>
      (x, AList.lookup (op =) parms x, mx)) fixes)
  | finish_ext_elem parms _ (Constrains _, _) = Constrains []
  | finish_ext_elem _ close (Assumes asms, propp) =
      close (Assumes (map #1 asms ~~ propp))
  | finish_ext_elem _ close (Defines defs, propp) =
      close (Defines (map #1 defs ~~ map (fn [(t, ps)] => (t, ps)) propp))
  | finish_ext_elem _ _ (Notes facts, _) = Notes facts;


(* CB: finish_parms introduces type info from parms to identifiers *)
(* CB: only needed for types that have been NONE so far???
   If so, which are these??? *)

fun finish_parms parms (((name, ps), mode), elems) =
  (((name, map (fn (x, _) => (x, AList.lookup (op = : string * string -> bool) parms x)) ps), mode), elems);

fun finish_elems ctxt parms _ ((text, wits), ((id, Int e), _)) =
      let
        val [(id' as (_, mode), es)] = unify_elemss ctxt parms [(id, e)];
        val wits' = case mode of Assumed _ => wits | Derived ths => wits @ ths;
        val text' = fold (eval_text ctxt id' false) es text;
        val es' = map_filter
              (finish_derived (ProofContext.theory_of ctxt) wits' mode) es;
      in ((text', wits'), (id', map Int es')) end
  | finish_elems ctxt parms do_close ((text, wits), ((id, Ext e), [propp])) =
      let
        val e' = finish_ext_elem parms (closeup ctxt do_close) (e, propp);
        val text' = eval_text ctxt id true e' text;
      in ((text', wits), (id, [Ext e'])) end

in

(* CB: only called by prep_elemss *)

fun finish_elemss ctxt parms do_close =
  foldl_map (apsnd (finish_parms parms) o finish_elems ctxt parms do_close);

end;


(* Remove duplicate Defines elements: temporary workaround to fix Afp/Category. *)

fun defs_ord (defs1, defs2) =
    list_ord (fn ((_, (d1, _)), (_, (d2, _))) =>
      Term.fast_term_ord (d1, d2)) (defs1, defs2);
structure Defstab =
    TableFun(type key = ((string * Attrib.src list) * (term * term list)) list
        val ord = defs_ord);

fun rem_dup_defs es ds =
    fold_map (fn e as (Defines defs) => (fn ds =>
                 if Defstab.defined ds defs
                 then (Defines [], ds)
                 else (e, Defstab.update (defs, ()) ds))
               | e => (fn ds => (e, ds))) es ds;
fun rem_dup_elemss (Int es) ds = apfst Int (rem_dup_defs es ds)
  | rem_dup_elemss (Ext e) ds = (Ext e, ds);
fun rem_dup_defines raw_elemss =
    fold_map (fn (id as (_, (Assumed _)), es) => (fn ds =>
                     apfst (pair id) (rem_dup_elemss es ds))
               | (id as (_, (Derived _)), es) => (fn ds =>
                     ((id, es), ds))) raw_elemss Defstab.empty |> #1;

(* CB: type inference and consistency checks for locales.

   Works by building a context (through declare_elemss), extracting the
   required information and adjusting the context elements (finish_elemss).
   Can also universally close free vars in assms and defs.  This is only
   needed for Ext elements and controlled by parameter do_close.

   Only elements of assumed identifiers are considered.
*)

fun prep_elemss prep_vars prepp do_close context fixed_params raw_elemss raw_concl =
  let
    (* CB: contexts computed in the course of this function are discarded.
       They are used for type inference and consistency checks only. *)
    (* CB: fixed_params are the parameters (with types) of the target locale,
       empty list if there is no target. *)
    (* CB: raw_elemss are list of pairs consisting of identifiers and
       context elements, the latter marked as internal or external. *)
    val raw_elemss = rem_dup_defines raw_elemss;
    val (raw_ctxt, raw_proppss) = declare_elemss prep_vars fixed_params raw_elemss context;
    (* CB: raw_ctxt is context with additional fixed variables derived from
       the fixes elements in raw_elemss,
       raw_proppss contains assumptions and definitions from the
       external elements in raw_elemss. *)
    fun prep_prop raw_propp (raw_ctxt, raw_concl)  =
      let
        (* CB: add type information from fixed_params to context (declare_term) *)
        (* CB: process patterns (conclusion and external elements only) *)
        val (ctxt, all_propp) =
          prepp (fold Variable.declare_term (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp);
        (* CB: add type information from conclusion and external elements to context *)
        val ctxt = fold Variable.declare_term (maps (map fst) all_propp) ctxt;
        (* CB: resolve schematic variables (patterns) in conclusion and external elements. *)
        val all_propp' = map2 (curry (op ~~))
          (#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp)))) (map (map snd) all_propp);
        val (concl, propp) = chop (length raw_concl) all_propp';
      in (propp, (ctxt, concl)) end

    val (proppss, (ctxt, concl)) =
      (fold_burrow o fold_burrow) prep_prop raw_proppss (raw_ctxt, raw_concl);