(*  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 some basic ideas from Florian Kammueller's original version of

locales, but uses the richer infrastructure of Isar instead of the raw

meta-logic.  Furthermore, we provide structured import of contexts

(with merge and rename operations), as well as type-inference of the

signature parts, and predicate definitions of the specification text.

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.

*)

signature LOCALE =

sig

  type context

  type multi_attribute

  (* Constructors for elem, expr and elem_expr are

     currently only used for inputting locales (outer_parse.ML). *)

  datatype ('typ, 'term, 'fact, 'att) elem =

    Fixes of (string * 'typ option * mixfix option) list |

    Assumes of ((string * 'att list) * ('term * ('term list * 'term list)) list) list |

    Defines of ((string * 'att list) * ('term * 'term list)) list |

    Notes of ((string * 'att list) * ('fact * 'att list) list) list

  datatype expr =

    Locale of string |

    Rename of expr * string option list |

    Merge of expr list

  val empty: expr

  datatype 'a elem_expr = Elem of 'a | Expr of expr

  (* Abstract interface to locales *)

  type 'att element

  type 'att element_i

  type locale

  val intern: Sign.sg -> xstring -> string

  val cond_extern: Sign.sg -> string -> xstring

  val the_locale: theory -> string -> locale

  val map_attrib_element: ('att -> multi_attribute) -> 'att element ->

    multi_attribute element

  val map_attrib_element_i: ('att -> multi_attribute) -> 'att element_i ->

    multi_attribute element_i

  val map_attrib_elem_or_expr: ('att -> multi_attribute) ->

    'att element elem_expr -> multi_attribute element elem_expr

  val map_attrib_elem_or_expr_i: ('att -> multi_attribute) ->

    'att element_i elem_expr -> multi_attribute element_i elem_expr

  (* Processing of locale statements *)

  val read_context_statement: xstring option ->

    multi_attribute element elem_expr list ->

    (string * (string list * string list)) list list -> context ->

    string option * (cterm list * cterm list) * context * context * 

      (term * (term list * term list)) list list

  val cert_context_statement: string option ->

    multi_attribute element_i elem_expr list ->

    (term * (term list * term list)) list list -> context ->

    string option * (cterm list * cterm list) * context * context *

      (term * (term list * term list)) list list

  (* Diagnostic functions *)

  val print_locales: theory -> unit

  val print_locale: theory -> expr -> multi_attribute element list -> unit

  val print_global_registrations: theory -> string -> unit

  val add_locale: bool -> bstring -> expr -> multi_attribute element list -> theory -> theory

  val add_locale_i: bool -> bstring -> expr -> multi_attribute element_i list

    -> theory -> theory

  val smart_note_thmss: string -> (string * 'a) option ->

    ((bstring * theory attribute list) * (thm list * theory attribute list) list) list ->

    theory -> theory * (bstring * thm list) list

  val note_thmss: string -> xstring ->

    ((bstring * multi_attribute list) * (thmref * multi_attribute list) list) list ->

    theory -> theory * (bstring * thm list) list

  val note_thmss_i: string -> string ->

    ((bstring * multi_attribute list) * (thm list * multi_attribute list) list) list ->

    theory -> theory * (bstring * thm list) list

  val add_thmss: string -> ((string * thm list) * multi_attribute list) list ->

    theory * context -> (theory * context) * (string * thm list) list

  val instantiate: string -> string * context attribute list

    -> thm list option -> context -> context

  val prep_registration:

    string * theory attribute list -> expr -> string option list -> theory ->

    theory * ((string * term list) * term list) list * (theory -> theory)

  val global_add_witness:

    string * term list -> thm -> theory -> theory

  val setup: (theory -> theory) list

end;

structure Locale: LOCALE =

struct

(** locale elements and expressions **)

type context = ProofContext.context;

(* Locales store theory attributes (for activation in theories)

   and context attributes (for activation in contexts) *)

type multi_attribute = theory attribute * context attribute;

datatype ('typ, 'term, 'fact, 'att) elem =

  Fixes of (string * 'typ option * mixfix option) list |

  Assumes of ((string * 'att list) * ('term * ('term list * 'term list)) list) list |

  Defines of ((string * 'att list) * ('term * 'term list)) list |

  Notes of ((string * 'att list) * ('fact * 'att list) list) list;

datatype expr =

  Locale of string |

  Rename of expr * string option list |

  Merge of expr list;

val empty = Merge [];

datatype 'a elem_expr =

  Elem of 'a | Expr of expr;

type 'att element = (string, string, thmref, 'att) elem;

type 'att element_i = (typ, term, thm list, 'att) elem;

type locale =

 {predicate: cterm list * thm list,

    (* CB: For old-style locales with "(open)" this entry is ([], []).

       For new-style locales, which declare predicates, if the locale declares

       no predicates, this is also ([], []).

       If the locale declares predicates, the record field is

       ([statement], axioms), where statement is the locale predicate applied

       to the (assumed) locale parameters.  Axioms contains the projections

       from the locale predicate to the normalised assumptions of the locale

       (cf. [1], normalisation of locale expressions.)

    *)

  import: expr,                                       (*dynamic import*)

  elems: (multi_attribute element_i * stamp) list,  (*static content*)

  params: (string * typ option) list * string list}   (*all/local params*)

(** theory data **)

structure Termlisttab = TableFun(type key = term list

  val ord = Library.list_ord Term.term_ord);

structure LocalesArgs =

struct

  val name = "Isar/locales";

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

      ((string * theory attribute list) * thm list) Termlisttab.table

        Symtab.table;

    (* 1st entry: locale namespace,

       2nd entry: locales of the theory,

       3rd entry: registrations: theorems instantiating locale assumptions,

         with prefix and attributes, indexed by locale name and parameter

         instantiation *)

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

  val copy = I;

  val prep_ext = I;

  fun join_locs ({predicate, import, elems, params}: locale,

      {elems = elems', ...}: locale) =

    SOME {predicate = predicate, import = import,

      elems = gen_merge_lists eq_snd elems elems',

      params = params};

  (* joining of registrations: prefix and attributes of left theory,

     thmsss are equal *)

  fun join_regs (reg, _) = SOME reg;

  fun merge ((space1, locs1, regs1), (space2, locs2, regs2)) =

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

     Symtab.join (SOME o Termlisttab.join join_regs) (regs1, regs2));

  fun print _ (space, locs, _) =

    Pretty.strs ("locales:" :: map (NameSpace.cond_extern space o #1) (Symtab.dest locs))

    |> Pretty.writeln;

end;

structure LocalesData = TheoryDataFun(LocalesArgs);

val print_locales = LocalesData.print;

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

val cond_extern = NameSpace.cond_extern o #1 o LocalesData.get_sg;

(* access locales *)

fun declare_locale name =

  LocalesData.map (fn (space, locs, regs) =>

    (NameSpace.extend (space, [name]), locs, regs));

fun put_locale name loc =

  LocalesData.map (fn (space, locs, regs) =>

    (space, Symtab.update ((name, loc), locs), regs));

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

(* access registrations *)

(* add registration to theory, ignored if already present *)

fun global_put_registration (name, ps) attn =

  LocalesData.map (fn (space, locs, regs) =>

    (space, locs, let

        val tab = getOpt (Symtab.lookup (regs, name), Termlisttab.empty);

      in

        Symtab.update ((name, Termlisttab.update_new ((ps, (attn, [])), tab)),

          regs)

      end handle Termlisttab.DUP _ => regs));

(* add witness theorem to registration in theory,

   ignored if registration not present *)

fun global_add_witness (name, ps) thm =

  LocalesData.map (fn (space, locs, regs) =>

    (space, locs, let

        val tab = valOf (Symtab.lookup (regs, name));

        val (x, thms) = valOf (Termlisttab.lookup (tab, ps));

      in

        Symtab.update ((name, Termlisttab.update ((ps, (x, thm::thms)), tab)),

          regs)

      end handle Option => regs))

fun global_get_registration thy (name, ps) =

  case Symtab.lookup (#3 (LocalesData.get thy), name) of

      NONE => NONE

    | SOME tab => Termlisttab.lookup (tab, ps);

(* import hierarchy

   implementation could be more efficient, eg. by maintaining a database

   of dependencies *)

fun imports thy (upper, lower) =

  let

    val sign = sign_of thy;

    fun imps (Locale name) low = (name = low) orelse

      (case get_locale thy name of

           NONE => false

         | SOME {import, ...} => imps import low)

      | imps (Rename (expr, _)) low = imps expr low

      | imps (Merge es) low = exists (fn e => imps e low) es;

  in

    imps (Locale (intern sign upper)) (intern sign lower)

  end;

(* registrations *)

fun print_global_registrations thy loc =

  let

    val sg = Theory.sign_of thy;

    val loc_int = intern sg loc;

    val (_, _, regs) = LocalesData.get thy;

    val prt_term = Pretty.quote o Sign.pretty_term sg;

    fun prt_inst (ts, ((prfx, _), thms)) = let

in

      Pretty.block [Pretty.str prfx, Pretty.str ":", Pretty.brk 1,

        Pretty.list "(" ")" (map prt_term ts)]

end;

    val loc_regs = Symtab.lookup (regs, loc_int);

  in

    (case loc_regs of

        NONE => Pretty.str "No interpretations."

      | SOME r => Pretty.big_list "interpretations:"

          (map prt_inst (Termlisttab.dest r)))

    |> Pretty.writeln

  end;

(* diagnostics *)

fun err_in_locale ctxt msg ids =

  let

    val sign = ProofContext.sign_of ctxt;

    fun prt_id (name, parms) =

      [Pretty.block (Pretty.breaks (map Pretty.str (cond_extern sign name :: parms)))];

    val prt_ids = List.concat (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 raise ProofContext.CONTEXT (err_msg, ctxt) end;

(* Version for identifiers with axioms *)

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

(** primitives **)

(* renaming *)

fun rename ren x = getOpt (assoc_string (ren, x), x);

fun rename_term ren (Free (x, T)) = Free (rename ren x, T)

  | rename_term ren (t $ u) = rename_term ren t $ rename_term ren u

  | rename_term ren (Abs (x, T, t)) = Abs (x, T, rename_term ren t)

  | rename_term _ a = a;

fun rename_thm ren th =

  let

    val {sign, hyps, prop, maxidx, ...} = Thm.rep_thm th;

    val cert = Thm.cterm_of sign;

    val (xs, Ts) = Library.split_list (Library.foldl Term.add_frees ([], prop :: hyps));

    val xs' = map (rename ren) xs;

    fun cert_frees names = map (cert o Free) (names ~~ Ts);

    fun cert_vars names = map (cert o Var o apfst (rpair (maxidx + 1))) (names ~~ Ts);

  in

    if xs = xs' then th

    else

      th

      |> Drule.implies_intr_list (map cert hyps)

      |> Drule.forall_intr_list (cert_frees xs)

      |> Drule.forall_elim_list (cert_vars xs)

      |> Thm.instantiate ([], cert_vars xs ~~ cert_frees xs')

      |> (fn th' => Drule.implies_elim_list th' (map (Thm.assume o cert o rename_term ren) hyps))

  end;

fun rename_elem ren (Fixes fixes) = Fixes (fixes |> map (fn (x, T, mx) =>

      let val x' = rename ren x in

        if x = x' then (x, T, mx)

        else (x', T, if mx = NONE then mx else SOME Syntax.NoSyn)    (*drop syntax*)

      end))

  | rename_elem ren (Assumes asms) = Assumes (map (apsnd (map (fn (t, (ps, qs)) =>

      (rename_term ren t, (map (rename_term ren) ps, map (rename_term ren) qs))))) asms)

  | rename_elem ren (Defines defs) = Defines (map (apsnd (fn (t, ps) =>

      (rename_term ren t, map (rename_term ren) ps))) defs)

  | rename_elem ren (Notes facts) = Notes (map (apsnd (map (apfst (map (rename_thm ren))))) facts);

fun rename_facts prfx elem =

  let

    fun qualify (arg as ((name, atts), x)) =

      if prfx = "" orelse name = "" then arg

      else ((NameSpace.pack [prfx, name], atts), x);

  in

    (case elem of

      Fixes fixes => Fixes fixes

    | Assumes asms => Assumes (map qualify asms)

    | Defines defs => Defines (map qualify defs)

    | Notes facts => Notes (map qualify facts))

  end;

(* type instantiation *)

fun inst_type [] T = T

  | inst_type env T = Term.map_type_tfree (fn v => getOpt (assoc (env, v), TFree v)) T;

fun inst_term [] t = t

  | inst_term env t = Term.map_term_types (inst_type env) t;

fun inst_thm _ [] th = th

  | inst_thm ctxt env th =

      let

        val sign = ProofContext.sign_of ctxt;

        val cert = Thm.cterm_of sign;

        val certT = Thm.ctyp_of sign;

        val {hyps, prop, maxidx, ...} = Thm.rep_thm th;

        val tfrees = foldr Term.add_term_tfree_names [] (prop :: hyps);

        val env' = List.filter (fn ((a, _), _) => a mem_string tfrees) env;

      in

        if null env' then th

        else

          th

          |> Drule.implies_intr_list (map cert hyps)

          |> Drule.tvars_intr_list (map (#1 o #1) env')

          |> (fn (th', al) => th' |>

            Thm.instantiate ((map (fn ((a, _), T) => (valOf (assoc (al, a)), certT T)) env'), []))

          |> (fn th'' => Drule.implies_elim_list th''

              (map (Thm.assume o cert o inst_term env') hyps))

      end;

fun inst_elem _ env (Fixes fixes) =

      Fixes (map (fn (x, T, mx) => (x, Option.map (inst_type env) T, mx)) fixes)

  | inst_elem _ env (Assumes asms) = Assumes (map (apsnd (map (fn (t, (ps, qs)) =>

      (inst_term env t, (map (inst_term env) ps, map (inst_term env) qs))))) asms)

  | inst_elem _ env (Defines defs) = Defines (map (apsnd (fn (t, ps) =>

      (inst_term env t, map (inst_term env) ps))) defs)

  | inst_elem ctxt env (Notes facts) =

      Notes (map (apsnd (map (apfst (map (inst_thm ctxt env))))) facts);

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

(* parameter types *)

(* CB: frozen_tvars has the following type:

  ProofContext.context -> Term.typ list -> (Term.indexname * Term.typ) list *)

fun frozen_tvars ctxt Ts =

  let

    val tvars = rev (Library.foldl Term.add_tvarsT ([], Ts));

    val tfrees = map TFree

      (Term.invent_names (ProofContext.used_types ctxt) "'a" (length tvars) ~~ map #2 tvars);

  in map #1 tvars ~~ tfrees end;

fun unify_frozen ctxt maxidx Ts Us =

  let

    fun paramify (i, NONE) = (i, NONE)

      | paramify (i, SOME T) = apsnd SOME (TypeInfer.paramify_dummies (i, T));

    val (maxidx', Ts') = foldl_map paramify (maxidx, Ts);

    val (maxidx'', Us') = foldl_map paramify (maxidx', Us);

    val tsig = Sign.tsig_of (ProofContext.sign_of ctxt);

    fun unify (env, (SOME T, SOME U)) = (Type.unify tsig env (U, T)

          handle Type.TUNIFY =>

            raise TYPE ("unify_frozen: failed to unify types", [U, T], []))

      | unify (env, _) = env;

    val (unifier, _) = Library.foldl unify ((Vartab.empty, maxidx''), Ts' ~~ Us');

    val Vs = map (Option.map (Envir.norm_type unifier)) Us';

    val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (List.mapPartial I Vs));

  in map (Option.map (Envir.norm_type unifier')) Vs end;

fun params_of elemss = gen_distinct eq_fst (List.concat (map (snd o fst) elemss));

fun params_of' elemss = gen_distinct eq_fst (List.concat (map (snd o fst o fst) elemss));

(* CB: param_types has the following type:

  ('a * 'b option) list -> ('a * 'b) list *)

fun param_types ps = List.mapPartial (fn (_, NONE) => NONE | (x, SOME T) => SOME (x, T)) ps;

(* flatten expressions *)

local

(* CB: OUTDATED unique_parms has the following type:

     'a ->

     (('b * (('c * 'd) list * Symtab.key list)) * 'e) list ->

     (('b * ('c * 'd) list) * 'e) list  *)

fun unique_parms ctxt elemss =

  let

    val param_decls =

      List.concat (map (fn (((name, (ps, qs)), _), _) => map (rpair (name, ps)) qs) elemss)

      |> Symtab.make_multi |> Symtab.dest;

  in

    (case find_first (fn (_, ids) => length ids > 1) param_decls of

      SOME (q, ids) => err_in_locale ctxt ("Multiple declaration of parameter " ^ quote q)

          (map (apsnd (map fst)) ids)

    | NONE => map (apfst (apfst (apsnd #1))) elemss)

  end;

(* CB: unify_parms has the following type:

     ProofContext.context ->

     (string * Term.typ) list ->

     (string * Term.typ option) list list ->

     ((string * Term.sort) * Term.typ) list list *)

fun unify_parms ctxt fixed_parms raw_parmss =

  let

    val sign = ProofContext.sign_of ctxt;

    val tsig = Sign.tsig_of sign;

    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 @ List.concat (map varify_parms idx_parmss);

    fun unify T ((env, maxidx), U) =

      Type.unify tsig (env, maxidx) (U, T)

      handle Type.TUNIFY =>

        let val prt = Sign.string_of_typ sign

        in raise TYPE ("unify_parms: failed to unify types " ^

          prt U ^ " and " ^ prt T, [U, T], [])

        end

    fun unify_list (envir, T :: Us) = Library.foldl (unify T) (envir, Us)

      | unify_list (envir, []) = envir;

    val (unifier, _) = Library.foldl unify_list

      ((Vartab.empty, maxidx), map #2 (Symtab.dest (Symtab.make_multi parms)));

    val parms' = map (apsnd (Envir.norm_type unifier)) (gen_distinct eq_fst parms);

    val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map #2 parms'));

    fun inst_parms (i, ps) =

      foldr Term.add_typ_tfrees [] (List.mapPartial snd ps)

      |> List.mapPartial (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, S), T) end)

  in map inst_parms idx_parmss end;

in

(* like unify_elemss, but does not touch axioms *)

fun unify_elemss' _ _ [] = []

  | unify_elemss' _ [] [elems] = [elems]

  | unify_elemss' ctxt fixed_parms elemss =

      let

        val envs = unify_parms ctxt fixed_parms (map (#2 o #1 o #1) elemss);

        fun inst ((((name, ps), axs), elems), env) =

          (((name, map (apsnd (Option.map (inst_type env))) ps),  axs),

           map (inst_elem ctxt env) elems);

      in map inst (elemss ~~ envs) end;

fun unify_elemss _ _ [] = []

  | unify_elemss _ [] [elems] = [elems]

  | unify_elemss ctxt fixed_parms elemss =

      let

        val envs = unify_parms ctxt fixed_parms (map (#2 o #1 o #1) elemss);

        fun inst ((((name, ps), axs), elems), env) =

          (((name, map (apsnd (Option.map (inst_type env))) ps), 

            map (inst_thm ctxt env) axs), map (inst_elem ctxt env) elems);

      in map inst (elemss ~~ envs) end;

(* 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, expr) =

  let

    val thy = ProofContext.theory_of ctxt;

    (* thy used for retrieval of locale info,

       ctxt for error messages, parameter unification and instantiation

       of axioms *)

    (* TODO: consider err_in_locale with thy argument *)

    fun renaming (SOME x :: xs) (y :: ys) = (y, x) :: renaming xs ys

      | renaming (NONE :: xs) (y :: ys) = renaming xs ys

      | renaming [] _ = []

      | renaming xs [] = raise ERROR_MESSAGE ("Too many arguments in renaming: " ^

          commas (map (fn NONE => "_" | SOME x => quote x) xs));

    fun rename_parms top ren ((name, ps), (parms, axs)) =

      let val ps' = map (rename ren) ps in

        (case duplicates ps' of [] => ((name, ps'),

          if top then (map (rename ren) parms, map (rename_thm ren) axs)

          else (parms, axs))

        | dups => err_in_locale ctxt ("Duplicate parameters: " ^ commas_quote dups) [(name, ps')])

      end;

    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 {predicate = (_, axioms), import, params, ...} =

              the_locale thy name;

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

            val (ids', parms') = identify false import;

                (* acyclic import dependencies *)

            val ids'' = ids' @ [((name, ps), ([], []))];

            val ids_ax = if top then snd

                 (foldl_map (fn (axs, ((name, parms), _)) => let

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

                   val ts = List.concat (List.mapPartial (fn (Assumes asms, _) =>

                     SOME (List.concat (map (map #1 o #2) asms)) | _ => NONE) elems);

                   val (axs1, axs2) = splitAt (length ts, axs);

                 in (axs2, ((name, parms), (ps, axs1))) end) (axioms, ids''))

               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_MESSAGE msg => err_in_locale' ctxt msg ids';

            val ids'' = gen_distinct eq_fst (map (rename_parms top ren) ids');

            val parms'' = distinct (List.concat (map (#2 o #1) ids''));

          in (ids'', parms'') end

      | identify top (Merge es) =

          Library.foldl (fn ((ids, parms), e) => let

                     val (ids', parms') = identify top e

                   in (gen_merge_lists eq_fst ids ids',

                       merge_lists parms parms') end)

            (([], []), es);

    (* CB: enrich identifiers by parameter types and 

       the corresponding elements (with renamed parameters) *)

    fun eval ((name, xs), axs) =

      let

        val {params = (ps, qs), elems, ...} = the_locale thy name;

        val ren = filter_out (op =) (map #1 ps ~~ xs);

        val (params', elems') =

          if null ren then ((ps, qs), map #1 elems)

          else ((map (apfst (rename ren)) ps, map (rename ren) qs),

            map (rename_elem ren o #1) elems);

        val elems'' = map (rename_facts (space_implode "_" xs)) elems';

      in (((name, params'), axs), elems'') end;

    (* compute identifiers, merge with previous ones *)

    val idents = gen_rems eq_fst (#1 (identify true expr), prev_idents);

    (* add types to params, check for unique params and unify them *)

    val raw_elemss = unique_parms ctxt (map eval idents);

    val elemss = unify_elemss' ctxt [] raw_elemss;

    (* replace params in ids by params from axioms,

       adjust types in axioms *)

    val all_params' = params_of' elemss;

    val all_params = param_types all_params';

    val elemss' = map (fn (((name, _), (ps, axs)), elems) =>

         (((name, map (fn p => (p, assoc (all_params, p))) ps), axs), elems))

         elemss;

    fun inst_ax th = let

         val {hyps, prop, ...} = Thm.rep_thm th;

         val ps = map (apsnd SOME) (Library.foldl Term.add_frees ([], prop :: hyps));

         val [env] = unify_parms ctxt all_params [ps];

         val th' = inst_thm ctxt env th;

       in th' end;

    val final_elemss = map (fn ((id, axs), elems) =>

         ((id, map inst_ax axs), elems)) elemss';

  in (prev_idents @ idents, final_elemss) end;

end;

(* attributes *)

local

fun read_att attrib (x, srcs) = (x, map attrib srcs)

(* CB: Map attrib over

   * A context element: add attrib to attribute lists of assumptions,

     definitions and facts (on both sides for facts).

   * Locale expression: no effect. *)

fun gen_map_attrib_elem _ (Fixes fixes) = Fixes fixes

  | gen_map_attrib_elem attrib (Assumes asms) = Assumes (map (apfst (read_att attrib)) asms)

  | gen_map_attrib_elem attrib (Defines defs) = Defines (map (apfst (read_att attrib)) defs)

  | gen_map_attrib_elem attrib (Notes facts) =

      Notes (map (apfst (read_att attrib) o apsnd (map (read_att attrib))) facts)

fun gen_map_attrib_elem_expr attrib (Elem elem) = Elem (gen_map_attrib_elem attrib elem)

  | gen_map_attrib_elem_expr _ (Expr expr) = Expr expr;

in

val map_attrib_element = gen_map_attrib_elem;

val map_attrib_element_i = gen_map_attrib_elem;

val map_attrib_elem_or_expr = gen_map_attrib_elem_expr;

val map_attrib_elem_or_expr_i = gen_map_attrib_elem_expr;

end;

(* activate elements *)

local

fun export_axioms axs _ hyps th =

  th |> Drule.satisfy_hyps axs

     (* CB: replace meta-hyps, using axs, by a single meta-hyp. *)

  |> Drule.implies_intr_list (Library.drop (length axs, hyps))

     (* CB: turn remaining hyps into assumptions. *)

  |> Seq.single

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

      ((ctxt |> ProofContext.add_fixes fixes, axs), [])

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

      let

        (* extract context attributes *)

        val (Assumes asms) = map_attrib_element_i snd (Assumes asms);

        val ts = List.concat (map (map #1 o #2) asms);

        val (ps,qs) = splitAt (length ts, axs);

        val (ctxt', _) =

          ctxt |> ProofContext.fix_frees ts

          |> ProofContext.assume_i (export_axioms ps) asms;

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

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

      let

        (* extract context attributes *)

        val (Defines defs) = map_attrib_element_i snd (Defines defs);

        val (ctxt', _) =

        ctxt |> ProofContext.assume_i ProofContext.export_def

          (defs |> map (fn ((name, atts), (t, ps)) =>

            let val (c, t') = ProofContext.cert_def ctxt t

            in ((if name = "" then Thm.def_name c else name, atts), [(t', (ps, []))]) end))

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

  | activate_elem is_ext ((ctxt, axs), Notes facts) =

      let

        (* extract context attributes *)

        val (Notes facts) = map_attrib_element_i snd (Notes facts);

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

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

fun activate_elems (((name, ps), axs), elems) ctxt =

  let val ((ctxt', _), res) =

    foldl_map (activate_elem (name = "")) ((ProofContext.qualified true ctxt, axs), elems)

      handle ProofContext.CONTEXT (msg, ctxt) => err_in_locale ctxt msg [(name, map fst ps)]

  in (ProofContext.restore_qualified ctxt ctxt', res) end;

fun activate_elemss prep_facts = foldl_map (fn (ctxt, (((name, ps), axs), raw_elems)) =>

  let

    val elems = map (prep_facts ctxt) raw_elems;

    val (ctxt', res) = apsnd List.concat (activate_elems (((name, ps), axs), elems) ctxt);

  in (ctxt', (((name, ps), elems), res)) 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 get_facts or get_facts_i is used for prep_facts, these also remove

   the internal/external markers from elemss. *)

fun activate_facts prep_facts arg =

  apsnd (apsnd List.concat o Library.split_list) (activate_elemss prep_facts arg);

end;

(** prepare context elements **)

(* expressions *)

fun intern_expr sg (Locale xname) = Locale (intern sg xname)

  | intern_expr sg (Merge exprs) = Merge (map (intern_expr sg) exprs)

  | intern_expr sg (Rename (expr, xs)) = Rename (intern_expr sg expr, xs);

(* parameters *)

local

fun prep_fixes prep_vars ctxt fixes =

  let val vars = snd (foldl_map prep_vars (ctxt, map (fn (x, T, _) => ([x], T)) fixes))

  in map (fn (([x'], T'), (_, _, mx)) => (x', T', mx)) (vars ~~ fixes) end;

in

fun read_fixes x = prep_fixes ProofContext.read_vars x;

fun cert_fixes x = prep_fixes ProofContext.cert_vars x;

end;

(* propositions and bindings *)

(* CB: an internal (Int) locale element was either imported or included,

   an external (Ext) element appears directly in the locale. *)

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

(* flatten (ids, 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', elemss) where ids' is an extension of ids

   with identifiers generated for expr, and elemss is the list of

   context elements generated from expr.  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 _ (ids, Elem (Fixes fixes)) =

      (ids, [((("", map (rpair NONE o #1) fixes), []), Ext (Fixes fixes))])

  | flatten _ (ids, Elem elem) = (ids, [((("", []), []), Ext elem)])

  | flatten (ctxt, prep_expr) (ids, Expr expr) =

      apsnd (map (apsnd Int)) (flatten_expr ctxt (ids, prep_expr expr));

local

local

fun declare_int_elem (ctxt, Fixes fixes) =

      (ctxt |> ProofContext.add_fixes (map (fn (x, T, mx) =>

        (x, Option.map (Term.map_type_tfree (TypeInfer.param 0)) T, mx)) fixes), [])

  | declare_int_elem (ctxt, _) = (ctxt, []);

fun declare_ext_elem prep_fixes (ctxt, Fixes fixes) =

      (ctxt |> ProofContext.add_fixes (prep_fixes ctxt fixes), [])

  | 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_fixes (ctxt, (((name, ps), _), 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_fixes) (ctxt, [e]))

    handle ProofContext.CONTEXT (msg, ctxt) => err_in_locale ctxt msg [(name, map fst ps)]

  in (ctxt', propps) end;

in

(* CB: only called by prep_elemss. *)

fun declare_elemss prep_fixes 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 =

      ProofContext.declare_terms (map Free fixed_params) ctxt;

    val int_elemss =

      raw_elemss

      |> List.mapPartial (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_fixes) (ctxt, raw_elemss') end;

end;

local

(* CB: normalise Assumes and Defines wrt. previous definitions *)

val norm_term = Envir.beta_norm oo Term.subst_atomic;

(* CB: following code (abstract_term, abstract_thm, bind_def)

   used in eval_text for Defines elements. *)

fun abstract_term eq =    (*assumes well-formedness according to ProofContext.cert_def*)

  let

    val body = Term.strip_all_body eq;

    val vars = map Free (Term.rename_wrt_term body (Term.strip_all_vars eq));

    val (lhs, rhs) = Logic.dest_equals (Term.subst_bounds (vars, body));

    val (f, xs) = Term.strip_comb lhs;

    val eq' = Term.list_abs_free (map Term.dest_Free xs, rhs);

  in (Term.dest_Free f, eq') end;

fun abstract_thm sign eq =

  Thm.assume (Thm.cterm_of sign eq) |> Drule.gen_all |> Drule.abs_def;

fun bind_def ctxt (name, ps) ((xs, env, ths), eq) =

  let

    val ((y, T), b) = abstract_term eq;

    val b' = norm_term env b;

    val th = abstract_thm (ProofContext.sign_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 (xs, b'), (Free (y, T), b') :: env, th :: ths)

  end;

(* CB: for finish_elems (Int and Ext) *)

fun eval_text _ _ _ (text, Fixes _) = text

  | eval_text _ _ is_ext ((((exts, exts'), (ints, ints')), (xs, env, defs)), Assumes asms) =

      let

        val ts = List.concat (map (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', (Library.foldl Term.add_frees (xs, ts'), env, defs)) end

  | eval_text ctxt (id, _) _ ((spec, binds), Defines defs) =

      (spec, Library.foldl (bind_def ctxt id) (binds, map (#1 o #2) defs))

  | eval_text _ _ _ (text, Notes _) = text;

(* 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 (ProofContext.is_fixed ctxt o #1)

            (Term.add_frees ([], t)))

          in Term.list_all_free (frees, t) end;

        fun no_binds [] = []

          | no_binds _ =

              raise ProofContext.CONTEXT ("Illegal term bindings in locale element", ctxt);

      in

        (case elem of

          Assumes asms => Assumes (asms |> map (fn (a, propps) =>

            (a, map (fn (t, (ps, qs)) => (close_frees t, (no_binds ps, no_binds qs))) propps)))

        | Defines defs => Defines (defs |> map (fn (a, (t, ps)) =>

            (a, (close_frees (#2 (ProofContext.cert_def ctxt t)), no_binds ps))))

        | e => e)

      end;

fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (x, _, mx) =>

      (x, assoc_string (parms, x), mx)) fixes)

  | 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), axs), elems) =

  (((name, map (fn (x, _) => (x, assoc (parms, x))) ps), axs), elems);

fun finish_elems ctxt parms _ (text, ((id, Int e), _)) =

      let

        val [(id', es)] = unify_elemss ctxt parms [(id, e)];

        val text' = Library.foldl (eval_text ctxt id' false) (text, es);

      in (text', (id', map Int es)) end

  | finish_elems ctxt parms do_close (text, ((id, Ext e), [propp])) =

      let

        val e' = finish_ext_elem parms (closeup ctxt do_close) (e, propp);

        val text' = eval_text ctxt id true (text, e');

      in (text', (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;

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

fun prep_elemss prep_fixes 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_ctxt, raw_proppss) = declare_elemss prep_fixes 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. *)

    val raw_propps = map List.concat raw_proppss;

    val raw_propp = List.concat raw_propps;

    (* CB: add type information from fixed_params to context (declare_terms) *)

    (* CB: process patterns (conclusion and external elements only) *)

    val (ctxt, all_propp) =

      prepp (ProofContext.declare_terms (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp);

    (* CB: add type information from conclusion and external elements

       to context *)

    val ctxt = ProofContext.declare_terms (List.concat (map (map fst) all_propp)) ctxt;

    (* CB: resolve schematic variables (patterns) in conclusion and external

       elements. *)

    val all_propp' = map2 (op ~~)

      (#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp))), map (map snd) all_propp);

    val (concl, propp) = splitAt(length raw_concl, all_propp');

    val propps = unflat raw_propps propp;

    val proppss = map (uncurry unflat) (raw_proppss ~~ propps);

    (* CB: obtain all parameters from identifier part of raw_elemss *)

    val xs = map #1 (params_of' raw_elemss);

    val typing = unify_frozen ctxt 0

      (map (ProofContext.default_type raw_ctxt) xs)

      (map (ProofContext.default_type ctxt) xs);

    val parms = param_types (xs ~~ typing);

    (* CB: parms are the parameters from raw_elemss, with correct typing. *)

    (* CB: extract information from assumes and defines elements

       (fixes and notes in raw_elemss don't have an effect on text and elemss),

       compute final form of context elements. *)

    val (text, elemss) = finish_elemss ctxt parms do_close

      (((([], []), ([], [])), ([], [], [])), raw_elemss ~~ proppss);

    (* CB: text has the following structure: