(*  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 map_elem: ('a -> 'b) -> 'a element -> 'b element

  val intern: theory -> xstring -> string

  val intern_expr: theory -> expr -> expr

  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

  (* Theorems *)

  val intros: theory -> string -> thm list * thm list

  val dests: theory -> string -> thm list

  (* Not part of the official interface.  DO NOT USE *)

  val facts_of: theory -> string

    -> ((string * Attrib.src list) * (thm list * Attrib.src list) list) 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 read_context_statement_i: string 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_registrations: bool -> string -> Proof.context -> unit

  val add_locale: string -> bstring -> expr -> Element.context list -> theory

    -> string * Proof.context

  val add_locale_i: string -> bstring -> expr -> Element.context_i list -> theory

    -> string * Proof.context

  (* Tactics *)

  val intro_locales_tac: bool -> Proof.context -> thm list -> tactic

  (* Storing results *)

  val add_thmss: string -> string ->

    ((string * Attrib.src list) * (thm list * Attrib.src list) list) list ->

    Proof.context -> Proof.context

  val add_type_syntax: string -> declaration -> Proof.context -> Proof.context

  val add_term_syntax: string -> declaration -> Proof.context -> Proof.context

  val add_declaration: string -> declaration -> Proof.context -> Proof.context

  val interpretation_i: (Proof.context -> Proof.context) ->

    (bool * string) * Attrib.src list -> expr ->

    term option list * ((bstring * Attrib.src list) * term) list ->

    theory -> Proof.state

  val interpretation: (Proof.context -> Proof.context) ->

    (bool * string) * Attrib.src list -> expr ->

    string option list * ((bstring * Attrib.src list) * string) list ->

    theory -> Proof.state

  val interpretation_in_locale: (Proof.context -> Proof.context) ->

    xstring * expr -> theory -> Proof.state

  val interpret_i: (Proof.state -> Proof.state Seq.seq) ->

    (bool * string) * Attrib.src list -> expr ->

    term option list * ((bstring * Attrib.src list) * term) list ->

    bool -> Proof.state -> Proof.state

  val interpret: (Proof.state -> Proof.state Seq.seq) ->

    (bool * string) * Attrib.src list -> expr ->

    string option list * ((bstring * Attrib.src list) * string) list ->

    bool -> Proof.state -> Proof.state

end;

structure Locale: LOCALE =

struct

(* legacy operations *)

fun merge_lists _ xs [] = xs

  | merge_lists _ [] ys = ys

  | merge_lists eq xs ys = xs @ filter_out (member eq xs) ys;

fun merge_alists eq xs = merge_lists (eq_fst eq) xs;

(** 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 decl = declaration * stamp;

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. *)

  elems: (Element.context_i * stamp) list,

    (* Static content, neither Fixes nor Constrains elements *)

  params: ((string * typ) * mixfix) list,                             (*all params*)

  decls: decl list * decl list,                    (*type/term_syntax declarations*)

  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. *)

  dests: thm list}

    (* Destruction rules: projections from locale predicate to predicates of fragments. *)

(* 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;

(** substitutions on Vars -- clone from element.ML **)

(* instantiate types *)

fun var_instT_type env =

  if Vartab.is_empty env then I

  else Term.map_type_tvar (fn (x, S) => the_default (TVar (x, S)) (Vartab.lookup env x));

fun var_instT_term env =

  if Vartab.is_empty env then I

  else Term.map_types (var_instT_type env);

fun var_inst_term (envT, env) =

  if Vartab.is_empty env then var_instT_term envT

  else

    let

      val instT = var_instT_type envT;

      fun inst (Const (x, T)) = Const (x, instT T)

        | inst (Free (x, T)) = Free(x, instT T)

        | inst (Var (xi, T)) =

            (case Vartab.lookup env xi of

              NONE => Var (xi, instT T)

            | SOME t => t)

        | inst (b as Bound _) = b

        | inst (Abs (x, T, t)) = Abs (x, instT T, inst t)

        | inst (t $ u) = inst t $ inst u;

    in Envir.beta_norm o inst end;

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

type registration =

  {attn: (bool * string) * Attrib.src list,

      (* parameters and prefix

       (if the Boolean flag is set, only accesses containing the prefix are generated,

        otherwise the prefix may be omitted when accessing theorems etc.) *)

    exp: Morphism.morphism,

      (* maps content to its originating context *)

    imp: (typ Vartab.table * typ list) * (term Vartab.table * term list),

      (* inverse of exp *)

    wits: Element.witness list,

      (* witnesses of the registration *)

    eqns: thm Termtab.table

      (* theorems (equations) interpreting derived concepts and indexed by lhs *)

  }

structure Registrations :

  sig

    type T

    val empty: T

    val join: T * T -> T

    val dest: theory -> T ->

      (term list *

        (((bool * string) * Attrib.src list) *

         (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) *

         Element.witness list *

         thm Termtab.table)) list

    val test: theory -> T * term list -> bool

    val lookup: theory ->

      T * (term list * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) ->

      (((bool * string) * Attrib.src list) *

        Element.witness list *

        thm Termtab.table) option

    val insert: theory -> term list -> ((bool * string) * Attrib.src list) ->

      (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) ->

      T ->

      T * (term list * (((bool * string) * Attrib.src list) * Element.witness list)) list

    val add_witness: term list -> Element.witness -> T -> T

    val add_equation: term list -> thm -> T -> T

  end =

struct

  (* A registration is indexed by parameter instantiation.

     NB: index is exported whereas content is internalised. *)

  type T = registration Termtab.table;

  fun mk_reg attn exp imp wits eqns =

    {attn = attn, exp = exp, imp = imp, wits = wits, eqns = eqns};

  fun map_reg f reg =

    let

      val {attn, exp, imp, wits, eqns} = reg;

      val (attn', exp', imp', wits', eqns') = f (attn, exp, imp, wits, eqns);

    in mk_reg attn' exp' imp' wits' eqns' end;

  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, attributes and morphisms of right theory;

     - witnesses are equal, no attempt to subsumption testing;

     - union of equalities, if conflicting (i.e. two eqns with equal lhs)

       eqn of right theory takes precedence *)

  fun join (r1, r2) = Termtab.join (fn _ => fn ({eqns = e1, ...}, {attn = n, exp, imp, wits = w, eqns = e2}) =>

      mk_reg n exp imp w (Termtab.join (fn _ => fn (_, e) => e) (e1, e2))) (r1, r2);

  fun dest_transfer thy regs =

    Termtab.dest regs |> map (apsnd (map_reg (fn (n, e, i, ws, es) =>

      (n, e, i, map (Element.transfer_witness thy) ws, Termtab.map (transfer thy) es))));

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

    map (apsnd (fn {attn, exp, imp, wits, eqns} => (attn, (exp, imp), wits, eqns)));

  (* registrations that subsume t *)

  fun subsumers thy t regs =

    filter (fn (t', _) => Pattern.matches thy (t', t)) (dest_transfer thy regs);

  (* test if registration that subsumes the query is present *)

  fun test thy (regs, ts) =

    not (null (subsumers thy (termify ts) regs));

  (* look up registration, pick one that subsumes the query *)

  fun lookup thy (regs, (ts, ((impT, _), (imp, _)))) =

    let

      val t = termify ts;

      val subs = subsumers thy t regs;

    in

      (case subs of

        [] => NONE

        | ((t', {attn = (prfx, atts), exp = exp', imp = ((impT', domT'), (imp', dom')), wits, eqns}) :: _) =>

          let

            val (tinst, inst) = Pattern.match thy (t', t) (Vartab.empty, Vartab.empty);

            val tinst' = domT' |> map (fn (T as TFree (x, _)) =>

                (x, T |> Morphism.typ exp' |> Envir.typ_subst_TVars tinst

                      |> var_instT_type impT)) |> Symtab.make;

            val inst' = dom' |> map (fn (t as Free (x, _)) =>

                (x, t |> Morphism.term exp' |> Envir.subst_vars (tinst, inst)

                      |> var_inst_term (impT, imp))) |> Symtab.make;

            val inst'_morph = Element.inst_morphism thy (tinst', inst');

          in SOME ((prfx, map (Args.morph_values inst'_morph) atts),

            map (Element.morph_witness inst'_morph) wits,

            Termtab.map (Morphism.thm inst'_morph) eqns)

          end)

    end;

  (* add registration if not subsumed by ones already present,

     additionally returns registrations that are strictly subsumed *)

  fun insert thy ts attn (exp, imp) 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 |> map (fn (ts, {attn, wits, ...}) => (ts, (attn, wits)))

              in (Termtab.update (t, mk_reg attn exp imp [] Termtab.empty) regs, sups') end

      | _ => (regs, []))

    end;

  fun gen_add f ts regs =

    let

      val t = termify ts;

    in

      Termtab.update (t, map_reg f (the (Termtab.lookup regs t))) regs

    end;

  (* add witness theorem to registration,

     only if instantiation is exact, otherwise exception Option raised *)

  fun add_witness ts wit regs =

    gen_add (fn (x, e, i, wits, eqns) => (x, e, i, Element.close_witness wit :: wits, eqns))

      ts regs;

  (* add equation to registration, replaces previous equation with same lhs;

     only if instantiation is exact, otherwise exception Option raised;

     exception TERM raised if not a meta equality *)

  fun add_equation ts thm regs =

    gen_add (fn (x, e, i, thms, eqns) =>

      (x, e, i, thms, Termtab.update (thm |> prop_of |> Logic.dest_equals |> fst, Thm.close_derivation thm) eqns))

      ts regs;

end;

(** theory data : locales **)

structure LocalesData = TheoryDataFun

(

  type T = NameSpace.T * locale Symtab.table;

    (* 1st entry: locale namespace,

       2nd entry: locales of the theory *)

  val empty = (NameSpace.empty, Symtab.empty);

  val copy = I;

  val extend = I;

  fun join_locales _

    ({axiom, elems, params, decls = (decls1, decls2), regs, intros, dests}: locale,

      {elems = elems', decls = (decls1', decls2'), regs = regs', ...}: locale) =

     {axiom = axiom,

      elems = merge_lists (eq_snd (op =)) elems elems',

      params = params,

      decls =

       (Library.merge (eq_snd (op =)) (decls1, decls1'),

        Library.merge (eq_snd (op =)) (decls2, decls2')),

      regs = merge_alists (op =) regs regs',

      intros = intros,

      dests = dests};

  fun merge _ ((space1, locs1), (space2, locs2)) =

    (NameSpace.merge (space1, space2), Symtab.join join_locales (locs1, locs2));

);

(** context data : registrations **)

structure RegistrationsData = GenericDataFun

(

  type T = Registrations.T Symtab.table;  (*registrations, indexed by locale name*)

  val empty = Symtab.empty;

  val extend = I;

  fun merge _ = Symtab.join (K Registrations.join);

);

(** access locales **)

val intern = NameSpace.intern o #1 o LocalesData.get;

val extern = NameSpace.extern o #1 o LocalesData.get;

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

fun the_locale thy name = case get_locale thy name

 of SOME loc => loc

  | NONE => error ("Unknown locale " ^ quote name);

fun register_locale name loc thy =

  thy |> LocalesData.map (fn (space, locs) =>

    (Sign.declare_name thy name space, Symtab.update (name, loc) locs));

fun change_locale name f thy =

  let

    val {axiom, elems, params, decls, regs, intros, dests} =

        the_locale thy name;

    val (axiom', elems', params', decls', regs', intros', dests') =

      f (axiom, elems, params, decls, regs, intros, dests);

  in

    thy

    |> (LocalesData.map o apsnd) (Symtab.update (name, {axiom = axiom',

          elems = elems', params = params',

          decls = decls', regs = regs', intros = intros', dests = dests'}))

  end;

fun print_locales thy =

  let val (space, locs) = LocalesData.get thy in

    Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (space, locs)))

    |> Pretty.writeln

  end;

(* access registrations *)

(* retrieve registration from theory or context *)

fun get_registrations ctxt name =

  case Symtab.lookup (RegistrationsData.get ctxt) name of

      NONE => []

    | SOME reg => Registrations.dest (Context.theory_of ctxt) reg;

fun get_global_registrations thy = get_registrations (Context.Theory thy);

fun get_local_registrations ctxt = get_registrations (Context.Proof ctxt);

fun get_registration ctxt imprt (name, ps) =

  case Symtab.lookup (RegistrationsData.get ctxt) name of

      NONE => NONE

    | SOME reg => Registrations.lookup (Context.theory_of ctxt) (reg, (ps, imprt));

fun get_global_registration thy = get_registration (Context.Theory thy);

fun get_local_registration ctxt = get_registration (Context.Proof ctxt);

fun test_registration ctxt (name, ps) =

  case Symtab.lookup (RegistrationsData.get ctxt) name of

      NONE => false

    | SOME reg => Registrations.test (Context.theory_of ctxt) (reg, ps);

fun test_global_registration thy = test_registration (Context.Theory thy);

fun test_local_registration ctxt = test_registration (Context.Proof ctxt);

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

fun put_registration (name, ps) attn morphs (* wits *) ctxt =

  RegistrationsData.map (fn regs =>

    let

      val thy = Context.theory_of ctxt;

      val reg = the_default Registrations.empty (Symtab.lookup regs name);

      val (reg', sups) = Registrations.insert thy ps attn morphs (* wits *) reg;

      val _ = if not (null sups) then warning

                ("Subsumed interpretation(s) of locale " ^

                 quote (extern thy name) ^

                 "\nwith the following prefix(es):" ^

                  commas_quote (map (fn (_, (((_, s), _), _)) => s) sups))

              else ();

    in Symtab.update (name, reg') regs end) ctxt;

fun put_global_registration id attn morphs =

  Context.theory_map (put_registration id attn morphs);

fun put_local_registration id attn morphs =

  Context.proof_map (put_registration id attn morphs);

fun put_registration_in_locale name id =

  change_locale name (fn (axiom, elems, params, decls, regs, intros, dests) =>

    (axiom, elems, params, decls, regs @ [(id, [])], intros, dests));

(* add witness theorem to registration, ignored if registration not present *)

fun add_witness (name, ps) thm =

  RegistrationsData.map (Symtab.map_entry name (Registrations.add_witness ps thm));

fun add_global_witness id thm = Context.theory_map (add_witness id thm);

fun add_local_witness id thm = Context.proof_map (add_witness id thm);

fun add_witness_in_locale name id thm =

  change_locale name (fn (axiom, elems, params, decls, regs, intros, dests) =>

    let

      fun add (id', thms) =

        if id = id' then (id', thm :: thms) else (id', thms);

    in (axiom, elems, params, decls, map add regs, intros, dests) end);

(* add equation to registration, ignored if registration not present *)

fun add_equation (name, ps) thm =

  RegistrationsData.map (Symtab.map_entry name (Registrations.add_equation ps thm));

fun add_global_equation id thm = Context.theory_map (add_equation id thm);

fun add_local_equation id thm = Context.proof_map (add_equation id thm);

(* printing of registrations *)

fun print_registrations show_wits loc ctxt =

  let

    val thy = ProofContext.theory_of ctxt;

    val prt_term = Pretty.quote o Syntax.pretty_term ctxt;

    fun prt_term' t = if !show_types

          then Pretty.block [prt_term t, Pretty.brk 1, Pretty.str "::",

            Pretty.brk 1, (Pretty.quote o Syntax.pretty_typ ctxt) (type_of t)]

          else prt_term t;

    val prt_thm = prt_term o prop_of;

    fun prt_inst ts =

        Pretty.enclose "(" ")" (Pretty.breaks (map prt_term' ts));

    fun prt_attn ((false, prfx), atts) =

        Pretty.breaks (Pretty.str prfx :: Pretty.str "(optional)" ::

          Attrib.pretty_attribs ctxt atts)

      | prt_attn ((true, prfx), atts) =

        Pretty.breaks (Pretty.str prfx :: Attrib.pretty_attribs ctxt atts);

    fun prt_eqns [] = Pretty.str "no equations."

      | prt_eqns eqns = Pretty.block (Pretty.str "equations:" :: Pretty.brk 1 ::

          Pretty.breaks (map prt_thm eqns));

    fun prt_core ts eqns =

          [prt_inst ts, Pretty.fbrk, prt_eqns (Termtab.dest eqns |> map snd)];

    fun prt_witns [] = Pretty.str "no witnesses."

      | prt_witns witns = Pretty.block (Pretty.str "witnesses:" :: Pretty.brk 1 ::

          Pretty.breaks (map (Element.pretty_witness ctxt) witns))

    fun prt_reg (ts, (((_, ""), []), _, witns, eqns)) =

        if show_wits

          then Pretty.block (prt_core ts eqns @ [Pretty.fbrk, prt_witns witns])

          else Pretty.block (prt_core ts eqns)

      | prt_reg (ts, (attn, _, witns, eqns)) =

        if show_wits

          then Pretty.block ((prt_attn attn @ [Pretty.str ":", Pretty.brk 1] @

            prt_core ts eqns @ [Pretty.fbrk, prt_witns witns]))

          else Pretty.block ((prt_attn attn @

            [Pretty.str ":", Pretty.brk 1] @ prt_core ts eqns));

    val loc_int = intern thy loc;

    val regs = RegistrationsData.get (Context.Proof ctxt);

    val loc_regs = Symtab.lookup regs loc_int;

  in

    (case loc_regs of

        NONE => Pretty.str ("no interpretations")

      | SOME r => let

            val r' = Registrations.dest thy r;

            val r'' = Library.sort_wrt (fn (_, (((_, prfx), _), _, _, _)) => prfx) r';

          in Pretty.big_list ("interpretations:") (map prt_reg r'') end)

    |> Pretty.writeln

  end;

(* 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);

fun params_qualified params name =

  NameSpace.qualified (space_implode "_" params) name;

(* 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.DUP x => err_in_locale ctxt

    ("Conflicting syntax for parameter: " ^ quote x) (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 T' = Envir.norm_type (fst envir) T;

          val U' = Envir.norm_type (fst envir) U;

          val prt = Syntax.string_of_typ ctxt;

        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) =

      List.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 phis = unify_parms ctxt fixed_parms (map (snd o fst o fst) elemss)

          |> map (Element.instT_morphism thy);

        fun inst ((((name, ps), mode), elems), phi) =

          (((name, map (apsnd (Option.map (Morphism.typ phi))) ps),

              map_mode (map (Element.morph_witness phi)) mode),

            map (Element.morph_ctxt phi) elems);

      in map inst (elemss ~~ phis) 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.DUP x => err_in_expr ctxt

          ("Conflicting syntax for parameter: " ^ quote x) expr;

    fun params_of (expr as Locale name) =

          let

            val {params, ...} = the_locale thy name;

          in (map (fst o fst) params, params |> map fst |> Symtab.make,

               params |> map (apfst fst) |> Symtab.make) 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 (Syntax.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 (op =) 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 (op =) 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.morph_witness (Element.rename_morphism ren))) mode)

         else (parms, mode));

    (* add (name, pTs) 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.morph_witness

                (Element.instT_morphism thy env $>

                  Element.rename_morphism ren $>

                  Element.satisfy_morphism wits)

                #> Element.close_witness));

            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, params, ...} = the_locale thy name;

            val ps = map (#1 o #1) params;

            val (_, ids'', _) = add_with_regs ((name, map #1 params), Assumed []) ([], [], []);

            val ids_ax = if top then fst (fold_map (axiomify ps) ids'' axiom) else ids'';

            in (ids_ax, 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 (op =) ids ids', merge_lists (op =) 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 elem_morphism =

          Element.rename_morphism ren $>

          Morphism.name_morphism (params_qualified params) $>

          Element.instT_morphism thy env;

        val elems' = map (Element.morph_ctxt elem_morphism) elems;

      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 = subtract (eq_fst (op =)) prev_idents ids;

    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 _ As =

  (Element.satisfy_thm axs #> Drule.implies_intr_list (Library.drop (length axs, As)), fn t => t);

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

fun activate_elem _ _ (Fixes fixes) (ctxt, mode) =

      ([], (ctxt |> ProofContext.add_fixes_i fixes |> snd, mode))

  | activate_elem _ _ (Constrains _) (ctxt, mode) =

      ([], (ctxt, mode))

  | activate_elem ax_in_ctxt _ (Assumes asms) (ctxt, Assumed axs) =

      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.auto_fixes ts

          |> ProofContext.add_assms_i (axioms_export (if ax_in_ctxt then ps else [])) asms';

      in ([], (ctxt', Assumed qs)) end

  | activate_elem _ _ (Assumes asms) (ctxt, Derived ths) =

      ([], (ctxt, Derived ths))

  | activate_elem _ _ (Defines defs) (ctxt, Assumed axs) =

      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', ((Thm.def_name_optional c name, atts), [(t', ps)])) end);

        val (_, ctxt') =

          ctxt |> fold (Variable.auto_fixes o #1) asms

          |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms);

      in ([], (ctxt', Assumed axs)) end

  | activate_elem _ _ (Defines defs) (ctxt, Derived ths) =

      ([], (ctxt, Derived ths))

  | activate_elem _ is_ext (Notes (kind, facts)) (ctxt, mode) =

      let

        val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts;

        val (res, ctxt') = ctxt |> ProofContext.note_thmss_i kind facts';

      in (if is_ext then res else [], (ctxt', mode)) end;