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;