--- a/src/Pure/Isar/locale.ML Tue Nov 06 01:17:27 2001 +0100
+++ b/src/Pure/Isar/locale.ML Tue Nov 06 01:18:46 2001 +0100
@@ -4,20 +4,21 @@
License: GPL (GNU GENERAL PUBLIC LICENSE)
Locales -- Isar proof contexts as meta-level predicates, with local
-syntax and implicit structures.
+syntax and implicit structures. Draws basic ideas from Florian
+Kammueller's original version of locales, but uses the rich
+infrastructure of Isar instead of the raw meta-logic.
TODO:
- - reset scope context on qed of legacy goal (!??);
- - implicit closure of ``loose'' free vars;
- - avoid dynamic scoping of facts/atts
- (use thms_closure for globals, even within att expressions);
- - scope of implicit fixed in elementents vs. locales (!??);
- - remove scope stuff;
+ - 'print_locales' command (also PG menu?);
+ - cert_elem (do *not* cert_def, yet) (!?);
+ - ensure unique defines;
+ - local syntax (mostly in ProofContext);
*)
signature BASIC_LOCALE =
sig
val print_locales: theory -> unit
+ val print_locale: theory -> xstring -> unit
end;
signature LOCALE =
@@ -36,21 +37,15 @@
type locale
val intern: Sign.sg -> xstring -> string
val cond_extern: Sign.sg -> string -> xstring
- val intern_att: ('att -> context attribute) ->
+ val attribute: ('att -> context attribute) ->
('typ, 'term, 'thm, 'att) elem -> ('typ, 'term, 'thm, context attribute) elem
val activate_elements: context attribute element list -> context -> context
val activate_elements_i: context attribute element_i list -> context -> context
val activate_locale: xstring -> context -> context
val activate_locale_i: string -> context -> context
-(*
- val add_locale: bstring -> xstring option -> (string * string * mixfix) list ->
- ((string * context attribute list) * string) list ->
- ((string * context attribute list) * string) list -> theory -> theory
- val add_locale_i: bstring -> xstring option -> (string * typ * mixfix) list ->
- ((string * context attribute list) * term) list ->
- ((string * context attribute list) * term) list -> theory -> theory
- val read_prop_schematic: Sign.sg -> string -> cterm
-*)
+ val add_locale: bstring -> xstring list -> context attribute element list -> theory -> theory
+ val add_locale_i: bstring -> xstring list -> context attribute element_i list -> theory -> theory
+ val store_thm: string -> (string * thm) * context attribute list -> theory -> theory
val setup: (theory -> theory) list
end;
@@ -73,7 +68,10 @@
type 'att element = (string, string, string, 'att) elem;
type 'att element_i = (typ, term, thm list, 'att) elem;
-type locale = (thm -> string) * string list * context attribute element_i list;
+type locale = {imports: string list, elements: context attribute element_i list, closed: bool};
+
+fun make_locale imports elements closed =
+ {imports = imports, elements = elements, closed = closed}: locale;
fun fixes_of_elem (Fixes fixes) = map #1 fixes
@@ -81,36 +79,27 @@
fun frees_of_elem _ = []; (* FIXME *)
+(*fun close_locale {imports, elements, closed = _} = make_locale imports elements true;*)
+fun close_locale x = x; (* FIXME tmp *)
+
(** theory data **)
(* data kind 'Pure/locales' *)
-type locale_data =
- {space: NameSpace.T,
- locales: locale Symtab.table,
- scope: ((string * locale) list * context option) ref};
-
-fun make_locale_data space locales scope =
- {space = space, locales = locales, scope = scope}: locale_data;
-
-val empty_scope = ([], None);
-
structure LocalesArgs =
struct
val name = "Isar/locales";
- type T = locale_data;
+ type T = NameSpace.T * locale Symtab.table;
- val empty = make_locale_data NameSpace.empty Symtab.empty (ref empty_scope);
- fun copy {space, locales, scope = ref r} = make_locale_data space locales (ref r);
- fun prep_ext {space, locales, scope = _} = make_locale_data space locales (ref empty_scope);
- fun merge ({space = space1, locales = locales1, scope = _},
- {space = space2, locales = locales2, scope = _}) =
- make_locale_data (NameSpace.merge (space1, space2))
- (Symtab.merge (K true) (locales1, locales2)) (ref empty_scope);
+ val empty = (NameSpace.empty, Symtab.empty);
+ val copy = I;
+ fun prep_ext (space, locales) = (space, Symtab.map close_locale locales);
+ fun merge ((space1, locales1), (space2, locales2)) =
+ (NameSpace.merge (space1, space2), Symtab.merge (K true) (locales1, locales2));
- fun print _ {space, locales, scope = _} =
+ fun print _ (space, locales) =
Pretty.strs ("locales:" :: map (NameSpace.cond_extern space o #1) (Symtab.dest locales))
|> Pretty.writeln;
end;
@@ -118,18 +107,19 @@
structure LocalesData = TheoryDataFun(LocalesArgs);
val print_locales = LocalesData.print;
-val intern = NameSpace.intern o #space o LocalesData.get_sg;
-val cond_extern = NameSpace.cond_extern o #space o LocalesData.get_sg;
+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 get_locale_sg sg name = Symtab.lookup (#locales (LocalesData.get_sg sg), name);
-val get_locale = get_locale_sg o Theory.sign_of;
+fun declare_locale name =
+ LocalesData.map (apfst (fn space => (NameSpace.extend (space, [name]))));
-fun put_locale (name, locale) = LocalesData.map (fn {space, locales, scope} =>
- make_locale_data (NameSpace.extend (space, [name]))
- (Symtab.update ((name, locale), locales)) scope);
+fun put_locale name locale =
+ LocalesData.map (apsnd (fn locales => Symtab.update ((name, locale), locales)));
+
+fun get_locale thy name = Symtab.lookup (#2 (LocalesData.get thy), name);
fun the_locale thy name =
(case get_locale thy name of
@@ -137,31 +127,13 @@
| None => error ("Unknown locale " ^ quote name));
-(* access scope *)
-
-fun get_scope_sg sg =
- if Sign.eq_sg (sg, Theory.sign_of ProtoPure.thy) then empty_scope
- else ! (#scope (LocalesData.get_sg sg));
-
-val get_scope = get_scope_sg o Theory.sign_of;
-val nonempty_scope_sg = not o null o #1 o get_scope_sg;
-
-fun change_scope f thy =
- let val {scope, ...} = LocalesData.get thy
- in scope := f (! scope); thy end;
-
-fun print_scope thy =
- Pretty.writeln (Pretty.strs ("current scope:" ::
- rev (map (cond_extern (Theory.sign_of thy) o #1) (#1 (get_scope thy)))));
-
-
(* print locales *) (* FIXME activate local syntax *)
fun pretty_locale thy xname =
let
val sg = Theory.sign_of thy;
val name = intern sg xname;
- val (_, ancestors, elements) = the_locale thy name;
+ val {imports, elements, closed = _} = the_locale thy name;
val prt_typ = Pretty.quote o Sign.pretty_typ sg;
val prt_term = Pretty.quote o Sign.pretty_term sg;
@@ -191,48 +163,53 @@
| prt_elem (Uses _) = Pretty.str "FIXME";
val prt_header = Pretty.block (Pretty.str ("locale " ^ cond_extern sg name ^ " =") ::
- (if null ancestors then [] else
- (flat (separate [Pretty.str "+", Pretty.brk 1] (map (single o Pretty.str) ancestors)) @
+ (if null imports then [] else
+ (flat (separate [Pretty.str "+", Pretty.brk 1] (map (single o Pretty.str) imports)) @
[Pretty.str "+"])));
in Pretty.block (Pretty.fbreaks (prt_header :: map prt_elem elements)) end;
val print_locale = Pretty.writeln oo pretty_locale;
-(** internalization of theorems and attributes **)
-fun int_att attrib (x, srcs) = (x, map attrib srcs);
+(** internalize elements **)
+
+(* read_elem *)
-fun intern_att _ (Fixes fixes) = Fixes fixes
- | intern_att attrib (Assumes asms) = Assumes (map (apfst (int_att attrib)) asms)
- | intern_att attrib (Defines defs) = Defines (map (apfst (int_att attrib)) defs)
- | intern_att attrib (Notes facts) =
+fun read_elem ctxt =
+ fn Fixes fixes =>
+ let val vars =
+ #2 (foldl_map ProofContext.read_vars (ctxt, map (fn (x, T, _) => ([x], T)) fixes))
+ in Fixes (map2 (fn (([x'], T'), (_, _, mx)) => (x', T', mx)) (vars, fixes)) end
+ | Assumes asms =>
+ Assumes (map #1 asms ~~ #2 (ProofContext.read_propp (ctxt, map #2 asms)))
+ | Defines defs =>
+ let val propps =
+ #2 (ProofContext.read_propp (ctxt, map (fn (_, (t, ps)) => [(t, (ps, []))]) defs))
+ in Defines (map #1 defs ~~ map (fn [(t', (ps', []))] => (t', ps')) propps) end
+ | Notes facts =>
+ Notes (map (apsnd (map (apfst (ProofContext.get_thms ctxt)))) facts)
+ | Uses FIXME => Uses FIXME;
+
+
+(* prepare attributes *)
+
+local fun int_att attrib (x, srcs) = (x, map attrib srcs) in
+
+fun attribute _ (Fixes fixes) = Fixes fixes
+ | attribute attrib (Assumes asms) = Assumes (map (apfst (int_att attrib)) asms)
+ | attribute attrib (Defines defs) = Defines (map (apfst (int_att attrib)) defs)
+ | attribute attrib (Notes facts) =
Notes (map (apfst (int_att attrib) o apsnd (map (int_att attrib))) facts)
- | intern_att _ (Uses FIXME) = Uses FIXME;
+ | attribute _ (Uses FIXME) = Uses FIXME;
+
+end;
(** activate locales **)
-fun close_frees ctxt t =
- let val frees = rev (filter_out (ProofContext.is_fixed ctxt o #1) (Drule.add_frees ([], t)))
- in Term.list_all_free (frees, t) end;
-
-fun read_elem ctxt =
- fn (Fixes fixes) =>
- let val vars =
- #2 (foldl_map ProofContext.read_vars (ctxt, map (fn (x, T, _) => ([x], T)) fixes))
- in Fixes (map2 (fn (([x'], T'), (_, _, mx)) => (x', T', mx)) (vars, fixes)) end
- | (Assumes asms) =>
- Assumes (map #1 asms ~~ #2 (ProofContext.read_propp (ctxt, map #2 asms)))
- | (Defines defs) =>
- let val propps =
- #2 (ProofContext.read_propp (ctxt, map (fn (_, (t, ps)) => [(t, (ps, []))]) defs))
- in Defines (map #1 defs ~~ map (fn [(t', (ps', []))] => (t', ps')) propps) end
- | (Notes facts) =>
- Notes (map (apsnd (map (apfst (ProofContext.get_thms ctxt)))) facts)
- | (Uses FIXME) => Uses FIXME;
-
+(* activatation primitive *)
fun activate (ctxt, Fixes fixes) =
ProofContext.fix_direct (map (fn (x, T, FIXME) => ([x], T)) fixes) ctxt
@@ -244,74 +221,92 @@
| activate (ctxt, Notes facts) = #1 (ProofContext.have_thmss facts ctxt)
| activate (ctxt, Uses FIXME) = ctxt;
-fun read_activate (ctxt, elem) =
- let val elem' = read_elem ctxt elem
- in (activate (ctxt, elem'), elem') end;
+
+(* activate operations *)
fun activate_elements_i elems ctxt = foldl activate (ctxt, elems);
-fun activate_elements elems ctxt = foldl (#1 o read_activate) (ctxt, elems);
+fun activate_elements elems ctxt =
+ foldl ((fn (ctxt, elem) => activate (ctxt, read_elem ctxt elem))) (ctxt, elems);
-fun with_locale f name ctxt =
+fun activate_locale_elements (ctxt, name) =
let
val thy = ProofContext.theory_of ctxt;
- val locale = the_locale thy name;
+ val {elements, ...} = the_locale thy name; (*exception ERROR*)
in
- f locale ctxt handle ProofContext.CONTEXT (msg, c) =>
+ activate_elements_i elements ctxt handle ProofContext.CONTEXT (msg, c) =>
raise ProofContext.CONTEXT (msg ^ "\nThe error(s) above occurred in locale " ^
quote (cond_extern (Theory.sign_of thy) name), c)
end;
-val activate_locale_elements = with_locale (activate_elements_i o #3);
-
-fun activate_locale_ancestors name ctxt =
- foldl (fn (c, es) => activate_locale_elements es c)
- (ctxt, #2 (the_locale (ProofContext.theory_of ctxt) name));
-
fun activate_locale_i name ctxt =
- ctxt |> activate_locale_ancestors name |> activate_locale_elements name;
+ activate_locale_elements (foldl activate_locale_elements
+ (ctxt, #imports (the_locale (ProofContext.theory_of ctxt) name)), name);
fun activate_locale xname ctxt =
activate_locale_i (intern (ProofContext.sign_of ctxt) xname) ctxt;
-(* FIXME
(** define locales **)
-(* concrete syntax *)
+(* closeup dangling frees *)
+
+fun close_frees_wrt ctxt t =
+ let val frees = rev (filter_out (ProofContext.is_fixed ctxt o #1) (Drule.add_frees ([], t)))
+ in curry Term.list_all_free frees end;
-fun mark_syn c = "\\<^locale>" ^ c;
-
-fun mk_loc_tr c ts = list_comb (Free (c, dummyT), ts);
+fun closeup ctxt (Assumes asms) = Assumes (asms |> map (fn (a, propps) =>
+ (a, propps |> map (fn (t, (ps1, ps2)) =>
+ let val close = close_frees_wrt ctxt t in (close t, (map close ps1, map close ps2)) end))))
+ | closeup ctxt (Defines defs) = Defines (defs |> map (fn (a, (t, ps)) =>
+ let
+ val t' = ProofContext.cert_def ctxt t;
+ val close = close_frees_wrt ctxt t';
+ in (a, (close t', map close ps)) end))
+ | closeup ctxt elem = elem;
-(* add_locale *)
+(* add_locale(_i) *)
-fun gen_add_locale prep_typ prep_term bname bpar raw_fixes raw_assumes raw_defs thy =
- let val sign = Theory.sign_of thy;
-
+fun gen_add_locale prep_locale prep_elem bname raw_imports raw_elems thy =
+ let
+ val sign = Theory.sign_of thy;
val name = Sign.full_name sign bname;
-
- val (envSb, old_loc_fixes, _) =
- case bpar of
- Some loc => (get_defaults thy loc)
- | None => ([],[],[]);
+ val _ =
+ if is_none (get_locale thy name) then () else
+ error ("Duplicate definition of locale " ^ quote name);
- val old_nosyn = case bpar of
- Some loc => #nosyn(#2(the_locale thy loc))
- | None => [];
+ val imports = map (prep_locale sign) raw_imports;
+ val imports_ctxt = foldl activate_locale_elements (ProofContext.init thy, imports);
+ fun prep (ctxt, raw_elem) =
+ let val elem = closeup ctxt (prep_elem ctxt raw_elem)
+ in (activate (ctxt, elem), elem) end;
+ val (locale_ctxt, elems) = foldl_map prep (imports_ctxt, raw_elems);
+ in
+ thy
+ |> declare_locale name
+ |> put_locale name (make_locale imports elems false)
+ end;
+
+val add_locale = gen_add_locale intern read_elem;
+val add_locale_i = gen_add_locale (K I) (K I);
+
- (* Get the full name of the parent *)
- val parent = case bparent of
- Some loc => Some(#1(the_locale thy loc))
- | None => None;
+
+(** store results **) (* FIXME test atts!? *)
- (* prepare locale fixes *)
+fun store_thm name ((a, th), atts) thy =
+ let
+ val note = Notes [((a, atts), [([Thm.name_thm (a, th)], [])])];
+ val {imports, elements, closed} = the_locale thy name;
+ in
+ if closed then error ("Cannot store results in closed locale: " ^ quote name)
+ else thy |> put_locale name (make_locale imports (elements @ [note]) closed)
+ end;
- fun prep_const (envS, (raw_c, raw_T, raw_mx)) =
- let
- val c = Syntax.const_name raw_c raw_mx;
- val c_syn = mark_syn c;
+
+(* FIXME old
+
val mx = Syntax.fix_mixfix raw_c raw_mx;
val (envS', T) = prep_typ sign (envS, raw_T) handle ERROR =>
error ("The error(s) above occured in locale constant " ^ quote c);
@@ -325,53 +320,11 @@
val nosyn = old_nosyn @ (map (#1 o #1) (filter (fn x => (#3(#2 x)) = NoSyn) loc_fixes_syn));
val loc_trfuns = mapfilter #3 loc_fixes_syn;
-
- (* 1st stage: syntax_thy *)
-
val syntax_thy =
thy
|> Theory.add_modesyntax_i ("", true) loc_syn
|> Theory.add_trfuns ([], loc_trfuns, [], []);
- val syntax_sign = Theory.sign_of syntax_thy;
-
-
- (* prepare assumes and defs *)
-
- fun prep_axiom (env, (a, raw_t)) =
- let
- val (env', t) = prep_term syntax_sign (env, (a, raw_t)) handle ERROR =>
- error ("The error(s) above occured in locale rule / definition " ^ quote a);
- in (env', (a, t)) end;
-
- val ((envS1, envT1, used1), loc_assumes) =
- foldl_map prep_axiom ((envS0, loc_fixes, map fst envS0), raw_assumes);
- val (defaults, loc_defs) =
- foldl_map prep_axiom ((envS1, envT1, used1), raw_defs);
-
- val old_loc_fixes = collect_fixes syntax_sign;
- val new_loc_fixes = (map #1 loc_fixes);
- val all_loc_fixes = old_loc_fixes @ new_loc_fixes;
-
- val (defaults, loc_defs_terms) =
- foldl_map (abs_over_free all_loc_fixes) (defaults, loc_defs);
- val loc_defs_thms =
- map (apsnd (prep_hyps (map #1 loc_fixes) syntax_sign)) loc_defs_terms;
- val (defaults, loc_thms_terms) =
- foldl_map (abs_over_free all_loc_fixes) (defaults, loc_assumes);
- val loc_thms = map (apsnd (prep_hyps (map #1 loc_fixes) syntax_sign))
- (loc_thms_terms)
- @ loc_defs_thms;
-
-
- (* error messages *)
-
- fun locale_error msg = error (msg ^ "\nFor locale " ^ quote name);
-
- val err_dup_locale =
- if is_none (get_locale thy name) then []
- else ["Duplicate definition of locale " ^ quote name];
-
(* check if definientes are locale constants
(in the same locale, so no redefining!) *)
val err_def_head =
@@ -401,99 +354,11 @@
in if check then []
else ["nonfixed variable on right hand side of a locale definition in locale " ^ quote name]
end;
-
- val errs = err_dup_locale @ err_def_head @ err_var_rhs;
- in
- if null errs then ()
- else error (cat_lines errs);
-
- syntax_thy
- |> put_locale (name,
- make_locale parent loc_fixes nosyn loc_thms_terms
- loc_defs_terms loc_thms defaults)
- end;
-
-
-val add_locale = gen_add_locale read_typ read_axm;
-val add_locale_i = gen_add_locale cert_typ cert_axm;
-
-
-
-(*
-(** support for legacy proof scripts (cf. goals.ML) **) (* FIXME move to goals.ML (!?) *)
-
-(* hyps_in_scope *)
-
-fun hyps_in_scope sg hyps =
- let val locs = map #2 (#1 (get_scope_sg sg))
- in gen_subset Term.aconv (hyps, map #2 (flat (map #assumes locs @ map #defines locs))) end;
-
-
-(* get theorems *)
-
-fun thmx get_local get_global name =
- let val thy = Context.the_context () in
- (case #2 (get_scope thy) of
- None => get_global thy name
- | Some ctxt => get_local ctxt name)
- end;
-
-val thm = thmx ProofContext.get_thm PureThy.get_thm;
-val thms = thmx ProofContext.get_thms PureThy.get_thms;
-
-
-(** scope operations -- for old-style goals **) (* FIXME move to goals.ML (!?) *)
-
-(* open *)
-
-local
-
-fun is_open thy name = exists (equal name o #1) (#1 (get_scope thy));
-
-fun open_loc thy name =
- let
- val (ancestors, elements) = the_locale thy name;
- in
- (case #parent locale of None => thy
- | Some par =>
- if is_open thy par then thy
- else (writeln ("Opening locale " ^ quote par ^ "(required by " ^ quote name ^ ")");
- open_loc name thy))
- |> change_scope (fn (locs, _) => ((name, locale) :: locs, None))
- end;
-
-in
-
-fun open_locale xname thy =
- let val name = intern (Theory.sign_of thy) xname in
- if is_open thy name then (warning ("Locale " ^ quote name ^ " already open"); thy)
- else open_loc name thy
- end;
-
-end;
-
-
-(* close *)
-
-fun close_locale xname thy =
- let val name = intern_locale (Theory.sign_of thy) xname in
- thy |> change_scope (fn ([], _) => error "Currently no open locales"
- | ((name', _) :: locs, _) =>
- if name <> name' then error ("Locale " ^ quote name ^ " not at top of scope")
- else (locs, None))
- end;
-
-
-(* implicit context versions *)
-
-fun Open_locale xname = (open_locale xname (Context.the_context ()); ());
-fun Close_locale xname = (close_locale xname (Context.the_context ()); ());
-fun Print_scope () = (print_scope (Context.the_context ()); ());
*)
(** locale theory setup **)
-*)
+
val setup =
[LocalesData.init];