src/Pure/Isar/new_locale.ML

Initial part of locale reimplementation.

(*  Title:      Pure/Isar/expression.ML
    ID:         $Id$
    Author:     Clemens Ballarin, TU Muenchen

New locale development --- experimental.
*)

signature NEW_LOCALE =
sig
  type locale

  val test_locale: theory -> string -> bool
  val register_locale: string ->
    (string * sort) list * (Name.binding * typ option * mixfix) list ->
    term option * term list ->
    (declaration * stamp) list * (declaration * stamp) list ->
    ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * stamp) list ->
    ((string * Morphism.morphism) * stamp) list -> theory -> theory

  (* Locale name space *)
  val intern: theory -> xstring -> string
  val extern: theory -> string -> xstring

  (* Specification *)
  val params_of: theory -> string -> (Name.binding * typ option * mixfix) list
  val declarations_of: theory -> string -> declaration list * declaration list;

  (* Evaluate locales *)
  val init: string -> theory -> Proof.context

  (* Diagnostic *)
  val print_locales: theory -> unit
  val print_locale: theory -> bool -> bstring -> unit
end;


structure NewLocale: NEW_LOCALE =
struct

datatype ctxt = datatype Element.ctxt;


(*** Basics ***)

datatype locale = Loc of {
  (* extensible lists are in reverse order: decls, notes, dependencies *)
  parameters: (string * sort) list * (Name.binding * typ option * mixfix) list,
    (* type and term parameters *)
  spec: term option * term list,
    (* assumptions (as a single predicate expression) and defines *)
  decls: (declaration * stamp) list * (declaration * stamp) list,
    (* type and term syntax declarations *)
  notes: ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * stamp) list,
    (* theorem declarations *)
  dependencies: ((string * Morphism.morphism) * stamp) list
    (* locale dependencies (sublocale relation) *)
}


(*** Theory data ***)

structure LocalesData = TheoryDataFun
(
  type T = NameSpace.T * locale Symtab.table;
    (* locale namespace and locales of the theory *)

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

  fun join_locales _
    (Loc {parameters, spec, decls = (decls1, decls2), notes, dependencies},
      Loc {decls = (decls1', decls2'), notes = notes',
        dependencies = dependencies', ...}) =
        let fun s_merge x = merge (eq_snd (op =)) x in
          Loc {parameters = parameters,
            spec = spec,
            decls = (s_merge (decls1, decls1'), s_merge (decls2, decls2')),
            notes = s_merge (notes, notes'),
            dependencies = s_merge (dependencies, dependencies')
          }          
        end;
  fun merge _ ((space1, locs1), (space2, locs2)) =
    (NameSpace.merge (space1, space2), Symtab.join join_locales (locs1, locs2));
);

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 test_locale thy name = case get_locale thy name
 of SOME _ => true | NONE => false;

fun register_locale name parameters spec decls notes dependencies thy =
  thy |> LocalesData.map (fn (space, locs) =>
    (Sign.declare_name thy name space, Symtab.update (name,
      Loc {parameters = parameters, spec = spec, decls = decls, notes = notes,
        dependencies = dependencies}) locs));

fun change_locale name f thy =
  let
    val Loc {parameters, spec, decls, notes, dependencies} =
        the_locale thy name;
    val (parameters', spec', decls', notes', dependencies') =
      f (parameters, spec, decls, notes, dependencies);
  in
    thy
    |> (LocalesData.map o apsnd) (Symtab.update (name, Loc {parameters = parameters',
      spec = spec', decls = decls', notes = notes', dependencies = dependencies'}))
  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;


(*** Primitive operations ***)

fun params_of thy name =
  let
    val Loc {parameters = (_, params), ...} = the_locale thy name
  in params end;

fun declarations_of thy loc =
  let
    val Loc {decls, ...} = the_locale thy loc
  in
    decls |> apfst (map fst) |> apsnd (map fst)
  end;


(*** Target context ***)

(* round up locale dependencies in a depth-first fashion *)

local

structure Idtab = TableFun(type key = string * term list
  val ord = prod_ord string_ord (list_ord Term.fast_term_ord));

in

fun roundup thy deps =
  let
    fun add (name, morph) (deps, marked) =
      let
        val Loc {parameters = (_, params), dependencies, ...} = the_locale thy name;
        val instance = params |>
          map ((fn (b, T, _) => Free (Name.name_of b, the T)) #> Morphism.term morph);
      in
        if Idtab.defined marked (name, instance)
        then (deps, marked)
        else
          let
            val dependencies' =
              map (fn ((name, morph'), _) => (name, morph' $>  morph)) dependencies;
            val marked' = Idtab.insert (op =) ((name, instance), ()) marked;
            val (deps', marked'') = fold_rev add dependencies' ([], marked');
          in
            (cons (name, morph) deps' @ deps, marked'')
          end
      end
  in fold_rev add deps ([], Idtab.empty) |> fst end;

end;


(* full context *)

fun make_asms NONE = []
  | make_asms (SOME asm) = [((Name.no_binding, []), [(asm, [])])];

fun make_defs [] = []
  | make_defs defs = [((Name.no_binding, []), map (fn def => (def, [])) defs)];

fun note_notes (name, morph) ctxt =
  let
    val thy = ProofContext.theory_of ctxt;
    val Loc {notes, ...} = the_locale (ProofContext.theory_of ctxt) name;
    fun activate ((kind, facts), _) ctxt =
      let
        val facts' = facts |> Element.facts_map (Element.morph_ctxt morph) |>
          Attrib.map_facts (Attrib.attribute_i thy);
      in fold (fn args => Locale.local_note_prefix kind args #> snd) facts' ctxt end;
  in
    fold_rev activate notes ctxt
  end;

fun init name thy =
  let
    val Loc {parameters = (_, params), spec = (asm, defs), dependencies, ...} =
      the_locale thy name;
    val dependencies' =
      (intern thy name, Morphism.identity) :: roundup thy (map fst dependencies);
  in
    thy |> ProofContext.init |>
      ProofContext.add_fixes_i params |> snd |>
      (* FIXME type parameters *)
      fold Variable.auto_fixes (the_list asm) |>
      ProofContext.add_assms_i Assumption.assume_export (make_asms asm) |> snd |>
      fold Variable.auto_fixes defs |>
      ProofContext.add_assms_i LocalDefs.def_export (make_defs defs) |> snd |>
      fold_rev note_notes dependencies'
  end;

fun print_locale thy show_facts name =
  let
    val Loc {parameters = (tparams, params), spec = (asm, defs), notes, ...} =
      the_locale thy (intern thy name);

    val fixes = [Fixes params];
    val assumes = case asm of NONE => [] |
      SOME spec => [Assumes [(Attrib.no_binding, [(spec, [])])]];
    val defines = case defs of [] => [] |
      defs => [Defines (map (fn def => (Attrib.no_binding, (def, []))) defs)];
    val notes = if show_facts then map (Notes o fst) notes else [];
    val ctxt = ProofContext.init thy;
  in
    Pretty.big_list "locale elements:"
      (fixes @ assumes @ defines @ notes |> map (Element.pretty_ctxt ctxt) |>
        map Pretty.chunks) |> Pretty.writeln
  end;


end;