--- a/src/Pure/Isar/locale.ML Thu Nov 01 21:10:13 2001 +0100
+++ b/src/Pure/Isar/locale.ML Thu Nov 01 21:10:47 2001 +0100
@@ -1,54 +1,38 @@
-(* Title: Pure/locale.ML
+(* Title: Pure/Isar/locale.ML
ID: $Id$
Author: Florian Kammueller, University of Cambridge
Author: Markus Wenzel, TU Muenchen
License: GPL (GNU GENERAL PUBLIC LICENSE)
-Locales. The theory section 'locale' declarings constants, assumptions and
-definitions that have local scope. Typical form is
-
- locale Locale_name =
- fixes (*variables that are fixed in the locale's scope*)
- v :: T
- assumes (*meta-hypothesis that hold in the locale*)
- Asm_name "meta-formula"
- defines (*local definitions of fixed variables in terms of others*)
- v_def "v x == ...x..."
+Locales. The theory section 'locale' declarings constants, assumptions
+and definitions that have local scope.
TODO:
- - operations on locales: renaming.
+ - reset scope context on qed of legacy goal (!??);
+ - Notes: source form (of atts etc.) (!????);
*)
signature BASIC_LOCALE =
sig
val print_locales: theory -> unit
- val thm: xstring -> thm
- val thms: xstring -> thm list
- val Open_locale: xstring -> unit
- val Close_locale: xstring -> unit
- val Print_scope: unit -> unit
end;
signature LOCALE =
sig
include BASIC_LOCALE
- val get_thm: theory -> xstring -> thm
- val get_thms: theory -> xstring -> thm list
type locale
- val add_locale: bstring -> (bstring option) -> (string * string * mixfix) list ->
- (string * string) list -> (string * string) list -> theory -> theory
- val add_locale_i: bstring -> (bstring option) -> (string * typ * mixfix) list ->
- (string * term) list -> (string * term) list -> theory -> theory
- val open_locale: xstring -> theory -> theory
- val close_locale: xstring -> theory -> theory
- val print_scope: theory -> unit
- val in_locale: term list -> Sign.sg -> bool
- val is_open_loc_sg: Sign.sg -> bool
- val is_open_loc: theory -> bool
- val read_cterm: Sign.sg -> string * typ -> cterm
- val get_scope: theory -> (string * locale) list
- val get_scope_sg: Sign.sg -> (string * locale) list
- val collect_consts: Sign.sg -> string list
+ type expression
+ type ('a, 'b) element
+ val cond_extern: Sign.sg -> string -> xstring
+(*
+ val add_locale: bstring -> xstring option -> (string * string * mixfix) list ->
+ ((string * ProofContext.context attribute list) * string) list ->
+ ((string * ProofContext.context attribute list) * string) list -> theory -> theory
+ val add_locale_i: bstring -> xstring option -> (string * typ * mixfix) list ->
+ ((string * ProofContext.context attribute list) * term) list ->
+ ((string * ProofContext.context attribute list) * term) list -> theory -> theory
+ val read_prop_schematic: Sign.sg -> string -> cterm
+*)
val setup: (theory -> theory) list
end;
@@ -56,41 +40,23 @@
struct
-(** type locale **)
+(** locale elements and locales **)
-type locale =
- {ancestor: string option,
- consts: (string * typ) list,
- nosyn: string list,
- rules: (string * term) list,
- defs: (string * term) list,
- thms: (string * thm) list,
- defaults: (string * sort) list * (string * typ) list * string list};
+type context = ProofContext.context;
-fun make_locale ancestor consts nosyn rules defs thms defaults =
- {ancestor = ancestor, consts = consts, nosyn = nosyn, rules = rules,
- defs = defs, thms = thms, defaults = defaults}: locale;
+type expression = unit; (* FIXME *)
-fun pretty_locale sg (name, {ancestor, consts, rules, defs, nosyn = _, thms = _, defaults = _}) =
- let
- val prt_typ = Pretty.quote o Sign.pretty_typ sg;
- val prt_term = Pretty.quote o Sign.pretty_term sg;
-
- fun pretty_const (c, T) = Pretty.block
- [Pretty.str (c ^ " ::"), Pretty.brk 1, prt_typ T];
+datatype ('typ, 'term) element =
+ Fixes of (string * 'typ * mixfix option) list |
+ Assumes of ((string * context attribute list) * ('term * ('term list * 'term list)) list) list |
+ Defines of ((string * context attribute list) * ('term * 'term list)) list |
+ Notes of ((string * context attribute list) * (thm list * context attribute list) list) list |
+ Uses of expression;
- fun pretty_axiom (a, t) = Pretty.block
- [Pretty.str (a ^ ":"), Pretty.brk 1, prt_term t];
+fun fixes_of_elem (Fixes fixes) = map #1 fixes
+ | fixes_of_elem _ = [];
- val anc = case ancestor of
- None => ""
- | Some(loc) => ((Sign.base_name loc) ^ " +")
- in
- Pretty.big_list (name ^ " = " ^ anc)
- [Pretty.big_list "consts:" (map pretty_const consts),
- Pretty.big_list "rules:" (map pretty_axiom rules),
- Pretty.big_list "defs:" (map pretty_axiom defs)]
- end;
+fun frees_of_elem _ = []; (* FIXME *)
@@ -98,175 +64,170 @@
(* data kind 'Pure/locales' *)
+type locale = string list * (typ, term) element list;
+
type locale_data =
{space: NameSpace.T,
locales: locale Symtab.table,
- scope: (string * locale) list ref};
+ scope: ((string * locale) list * ProofContext.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 = "Pure/locales";
+ val name = "Isar/locales";
type T = locale_data;
- val empty = make_locale_data NameSpace.empty Symtab.empty (ref []);
- fun copy {space, locales, scope = ref locs} = make_locale_data space locales (ref locs);
- fun prep_ext {space, locales, scope = _} = make_locale_data space locales (ref []);
+ 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 []);
+ (Symtab.merge (K true) (locales1, locales2)) (ref empty_scope);
- fun print sg {space, locales, scope} =
- let
- fun extrn name =
- if ! long_names then name else NameSpace.extern space name;
- val locs = map (apfst extrn) (Symtab.dest locales);
- val scope_names = rev (map (extrn o fst) (! scope));
- in
- [Display.pretty_name_space ("locale name space", space),
- Pretty.big_list "locales:" (map (pretty_locale sg) locs),
- Pretty.strs ("current scope:" :: scope_names)]
- |> Pretty.chunks |> Pretty.writeln
- end;
+ fun print _ {space, locales, scope = _} =
+ Pretty.strs ("locales:" :: map (NameSpace.cond_extern space o #1) (Symtab.dest locales))
+ |> Pretty.writeln;
end;
-
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;
+
(* 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 put_locale (name, locale) thy =
- let
- val {space, locales, scope} = LocalesData.get thy;
- val space' = NameSpace.extend (space, [name]);
- val locales' = Symtab.update ((name, locale), locales);
- in thy |> LocalesData.put (make_locale_data space' locales' scope) end;
+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 lookup_locale thy xname =
- let
- val {space, locales, ...} = LocalesData.get thy;
- val name = NameSpace.intern space xname;
- in apsome (pair name) (get_locale thy name) end;
+fun the_locale thy name =
+ (case get_locale thy name of
+ Some loc => loc
+ | None => error ("Unknown locale " ^ quote name));
(* access scope *)
fun get_scope_sg sg =
- if Sign.eq_sg (sg, Theory.sign_of ProtoPure.thy) then []
+ 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) end;
+ 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 *)
+
+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 prt_typ = Pretty.quote o Sign.pretty_typ sg;
+ val prt_term = Pretty.quote o Sign.pretty_term sg;
+
+ fun prt_syn syn =
+ let val s = (case syn of None => "(structure)" | Some mx => Syntax.string_of_mixfix mx)
+ in if s = "" then [] else [Pretty.brk 4, Pretty.str s] end;
+ fun prt_fix (x, T, syn) = Pretty.block (Pretty.str (x ^ " ::") :: Pretty.brk 1 ::
+ prt_typ T :: Pretty.brk 1 :: prt_syn syn);
+
+ fun prt_asm ((a, _), ts) = Pretty.block
+ (Pretty.breaks (Pretty.str (a ^ ":") :: map (prt_term o fst) ts));
+ fun prt_asms asms = Pretty.block
+ (flat (separate [Pretty.fbrk, Pretty.str "and"] (map (single o prt_asm) asms)));
+
+ fun prt_def ((a, _), (t, _)) = Pretty.block
+ [Pretty.str (a ^ ":"), Pretty.brk 1, prt_term t];
+
+ fun prt_fact ((a, _), ths) = Pretty.block
+ (Pretty.breaks (Pretty.str (a ^ ":") :: map Display.pretty_thm (flat (map fst ths))));
+
+ fun prt_elem (Fixes fixes) = Pretty.big_list "fixes" (map prt_fix fixes)
+ | prt_elem (Assumes asms) = Pretty.big_list "assumes" (map prt_asm asms)
+ | prt_elem (Defines defs) = Pretty.big_list "defines" (map prt_def defs)
+ | prt_elem (Notes facts) = Pretty.big_list "notes" (map prt_fact facts)
+ | 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)) @
+ [Pretty.str "+"])));
+ in Pretty.block (Pretty.fbreaks (prt_header :: map prt_elem elements)) end;
+
+val print_locale = Pretty.writeln oo pretty_locale;
-(** scope operations **)
-
-(* change scope *)
+(** activate locales **)
-fun the_locale thy xname =
- (case lookup_locale thy xname of
- Some loc => loc
- | None => error ("Unknown locale " ^ quote xname));
+(* FIXME old
+fun pack_def eq =
+ let
+ val (lhs, rhs) = Logic.dest_equals eq;
+ val (f, xs) = Term.strip_comb lhs;
+ in (xs, Logic.mk_equals (f, foldr (uncurry lambda) (xs, rhs))) end;
-fun open_locale xname thy =
- let val loc = the_locale thy xname;
- val anc = #ancestor(#2(loc));
- val cur_sc = get_scope thy;
- fun opn lc th = (change_scope (cons lc) th; th)
- in case anc of
- None => opn loc thy
- | Some(loc') =>
- if loc' mem (map fst cur_sc)
- then opn loc thy
- else (warning ("Opening locale " ^ quote loc' ^ ", required by " ^
- quote xname);
- opn loc (open_locale (Sign.base_name loc') thy))
- end;
+fun unpack_def xs thm =
+ let
+ val cxs = map (Thm.cterm_of (Thm.sign_of_thm thm)) xs;
+ fun unpack (th, cx) =
+ Thm.combination th (Thm.reflexive cx)
+ |> MetaSimplifier.fconv_rule (Thm.beta_conversion true);
+ in foldl unpack (thm, cxs) end;
-fun pop_locale [] = error "Currently no open locales"
- | pop_locale (_ :: locs) = locs;
-
-fun close_locale name thy =
- let val lname = (case get_scope thy of (ln,_)::_ => ln
- | _ => error "No locales are open!")
- val ok = (name = Sign.base_name lname) handle _ => false
- in if ok then (change_scope pop_locale thy; thy)
- else error ("locale " ^ name ^ " is not top of scope; top is " ^ lname)
- end;
-
-fun print_scope thy =
-Pretty.writeln (Pretty.strs ("current scope:" :: rev(map (Sign.base_name o fst) (get_scope thy))));
-
-(*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 ()); ());
+fun prep_def ((name, atts), eq) =
+ let val (xs, eq') = pack_def eq
+ in ((name, Drule.rule_attribute (K (unpack_def xs)) :: atts), [(eq', ([], []))]) end;
+*)
-(** functions for goals.ML **)
+fun activate (Fixes fixes) =
+ ProofContext.fix_direct (map (fn (x, T, FIXME) => ([x], Some T)) fixes)
+ | activate (Assumes asms) = #1 o ProofContext.assume_i ProofContext.export_assume asms
+ | activate (Defines defs) = #1 o ProofContext.assume_i ProofContext.export_def
+ (map (fn (a, (t, ps)) => (a, [(t, (ps, []))])) defs)
+ | activate (Notes facts) = #1 o ProofContext.have_thmss facts
+ | activate (Uses FIXME) = I;
-(* in_locale: check if hyps (: term list) of a proof are contained in the
- (current) scope. This function is needed in prepare_proof. It needs to
- refer to the signature, because theory is not available in prepare_proof. *)
+val activate_elements = foldl (fn (c, elem) => activate elem c);
-fun in_locale hyps sg =
- let val cur_sc = get_scope_sg sg;
- val rule_lists = map (#rules o snd) cur_sc;
- val def_lists = map (#defs o snd) cur_sc;
- val rules = map snd (foldr (op union) (rule_lists, []));
- val defs = map snd (foldr (op union) (def_lists, []));
- val defnrules = rules @ defs;
- in
- hyps subset defnrules
- end;
+fun activate_locale_elems (ctxt, name) =
+ let
+ val thy = ProofContext.theory_of ctxt;
+ val elems = #2 (the_locale thy name);
+ in
+ activate_elements (ctxt, elems) 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;
+
+fun activate_locale name ctxt =
+ foldl activate_locale_elems
+ (ctxt, (#1 (the_locale (ProofContext.theory_of ctxt) name) @ [name]));
-(* is_open_loc: check if any locale is open, i.e. in the scope of the current thy *)
-fun is_open_loc_sg sign =
- let val cur_sc = get_scope_sg sign
- in not(null(cur_sc)) end;
-val is_open_loc = is_open_loc_sg o Theory.sign_of;
-
-
-(* get theorems *)
-
-fun get_thm_locale name ((_, {thms, ...}: locale)) = assoc (thms, name);
-
-fun get_thmx f get thy name =
- (case get_first (get_thm_locale name) (get_scope thy) of
- Some thm => f thm
- | None => get thy name);
-
-val get_thm = get_thmx I PureThy.get_thm;
-val get_thms = get_thmx (fn x => [x]) PureThy.get_thms;
-
-fun thm name = get_thm (Context.the_context ()) name;
-fun thms name = get_thms (Context.the_context ()) name;
-
-
-(* get the defaults of a locale, for extension *)
-
-fun get_defaults thy name =
- let val (lname, loc) = the_locale thy name;
- in #defaults(loc)
- end;
-
-
+(* FIXME
(** define locales **)
(* prepare types *)
@@ -285,80 +246,6 @@
(* prepare props *)
-val add_frees = foldl_aterms (fn (vs, Free v) => v ins vs | (vs, _) => vs);
-
-fun enter_term t (envS, envT, used) =
- (Term.add_term_tfrees (t, envS), add_frees (envT, t), Term.add_term_tfree_names (t, used));
-
-fun read_axm sg ((envS, envT, used), (name, s)) =
- let
- fun def_sort (x, ~1) = assoc (envS, x)
- | def_sort _ = None;
- fun def_type (x, ~1) = assoc (envT, x)
- | def_type _ = None;
- val (_, t) = Theory.read_def_axm (sg, def_type, def_sort) used (name, s);
- in
- (enter_term t (envS, envT, used), t)
- end;
-
-
-fun cert_axm sg ((envS, envT, used), (name, raw_t)) =
- let val (_, t) = Theory.cert_axm sg (name, raw_t)
- in (enter_term t (envS, envT, used), t) end;
-
-
-(* Locale.read_cterm: read in a string as a certified term, and respect the bindings
- that already exist for subterms. If no locale is open, this function is equal to
- Thm.read_cterm *)
-
-fun read_cterm sign =
- let val cur_sc = get_scope_sg sign;
- val defaults = map (#defaults o snd) cur_sc;
- val envS = flat (map #1 defaults);
- val envT = flat (map #2 defaults);
- val used = flat (map #3 defaults);
- fun def_sort (x, ~1) = assoc (envS, x)
- | def_sort _ = None;
- fun def_type (x, ~1) = assoc (envT, x)
- | def_type _ = None;
- in (if (is_open_loc_sg sign)
- then (#1 o read_def_cterm (sign, def_type, def_sort) used true)
- else Thm.read_cterm sign)
- end;
-
-(* basic functions needed for definitions and display *)
-(* collect all locale constants of a scope, i.e. a list of locales *)
-fun collect_consts sg =
- let val cur_sc = get_scope_sg sg;
- val locale_list = map snd cur_sc;
- val const_list = flat (map #consts locale_list)
- in map fst const_list end;
-
-(* filter out the Free's in a term *)
-fun list_frees t =
- case t of Const(c,T) => []
- | Var(v,T) => []
- | Free(v,T)=> [Free(v,T)]
- | Bound x => []
- | Abs(a,T,u) => list_frees u
- | t1 $ t2 => (list_frees t1) @ (list_frees t2);
-
-(* filter out all Free's in a term that are not contained
- in a list of strings. Used to prepare definitions. The list of strings
- will be the consts of the scope. We filter out the "free" Free's to be
- able to bind them *)
-fun difflist term clist =
- let val flist = list_frees term;
- fun builddiff [] sl = []
- | builddiff (t :: tl) sl =
- let val Free(v,T) = t
- in
- if (v mem sl)
- then builddiff tl sl
- else t :: (builddiff tl sl)
- end;
- in distinct(builddiff flist clist) end;
-
(* Bind a term with !! over a list of "free" Free's.
To enable definitions like x + y == .... (without quantifier).
Complications, because x and y have to be removed from defaults *)
@@ -384,26 +271,26 @@
(* add_locale *)
-fun gen_add_locale prep_typ prep_term bname bancestor raw_consts raw_rules raw_defs thy =
+fun gen_add_locale prep_typ prep_term bname bpar raw_fixes raw_assumes raw_defs thy =
let val sign = Theory.sign_of thy;
val name = Sign.full_name sign bname;
- val (envSb, old_loc_consts, _) =
- case bancestor of
- Some(loc) => (get_defaults thy loc)
+ val (envSb, old_loc_fixes, _) =
+ case bpar of
+ Some loc => (get_defaults thy loc)
| None => ([],[],[]);
- val old_nosyn = case bancestor of
- Some(loc) => #nosyn(#2(the_locale thy loc))
+ val old_nosyn = case bpar of
+ Some loc => #nosyn(#2(the_locale thy loc))
| None => [];
- (* Get the full name of the ancestor *)
- val ancestor = case bancestor of
- Some(loc) => Some(#1(the_locale thy loc))
+ (* Get the full name of the parent *)
+ val parent = case bparent of
+ Some loc => Some(#1(the_locale thy loc))
| None => None;
- (* prepare locale consts *)
+ (* prepare locale fixes *)
fun prep_const (envS, (raw_c, raw_T, raw_mx)) =
let
@@ -415,12 +302,12 @@
val trfun = if mx = Syntax.NoSyn then None else Some (c_syn, mk_loc_tr c);
in (envS', ((c, T), (c_syn, T, mx), trfun)) end;
- val (envS0, loc_consts_syn) = foldl_map prep_const (envSb, raw_consts);
- val loc_consts = map #1 loc_consts_syn;
- val loc_consts = old_loc_consts @ loc_consts;
- val loc_syn = map #2 loc_consts_syn;
- val nosyn = old_nosyn @ (map (#1 o #1) (filter (fn x => (#3(#2 x)) = NoSyn) loc_consts_syn));
- val loc_trfuns = mapfilter #3 loc_consts_syn;
+ val (envS0, loc_fixes_syn) = foldl_map prep_const (envSb, raw_fixes);
+ val loc_fixes = map #1 loc_fixes_syn;
+ val loc_fixes = old_loc_fixes @ loc_fixes;
+ val loc_syn = map #2 loc_fixes_syn;
+ 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 *)
@@ -433,7 +320,7 @@
val syntax_sign = Theory.sign_of syntax_thy;
- (* prepare rules and defs *)
+ (* prepare assumes and defs *)
fun prep_axiom (env, (a, raw_t)) =
let
@@ -441,27 +328,27 @@
error ("The error(s) above occured in locale rule / definition " ^ quote a);
in (env', (a, t)) end;
- val ((envS1, envT1, used1), loc_rules) =
- foldl_map prep_axiom ((envS0, loc_consts, map fst envS0), raw_rules);
- val (defaults, loc_defs) =
- foldl_map prep_axiom ((envS1, envT1, used1), raw_defs);
+ 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_consts = collect_consts syntax_sign;
- val new_loc_consts = (map #1 loc_consts);
- val all_loc_consts = old_loc_consts @ new_loc_consts;
+ 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_consts) (defaults, loc_defs);
- val loc_defs_thms =
- map (apsnd (prep_hyps (map #1 loc_consts) syntax_sign)) loc_defs_terms;
- val (defaults, loc_thms_terms) =
- foldl_map (abs_over_free all_loc_consts) (defaults, loc_rules);
- val loc_thms = map (apsnd (prep_hyps (map #1 loc_consts) syntax_sign))
- (loc_thms_terms)
+ 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 *)
+ (* error messages *)
fun locale_error msg = error (msg ^ "\nFor locale " ^ quote name);
@@ -469,31 +356,31 @@
if is_none (get_locale thy name) then []
else ["Duplicate definition of locale " ^ quote name];
- (* check if definientes are locale constants
+ (* check if definientes are locale constants
(in the same locale, so no redefining!) *)
val err_def_head =
- let fun peal_appl t =
- case t of
+ let fun peal_appl t =
+ case t of
t1 $ t2 => peal_appl t1
| Free(t) => t
| _ => locale_error ("Bad form of LHS in locale definition");
- fun lhs (_, Const ("==" , _) $ d1 $ d2) = peal_appl d1
- | lhs _ = locale_error ("Definitions must use the == relation");
+ fun lhs (_, Const ("==" , _) $ d1 $ d2) = peal_appl d1
+ | lhs _ = locale_error ("Definitions must use the == relation");
val defs = map lhs loc_defs;
- val check = defs subset loc_consts
- in if check then []
+ val check = defs subset loc_fixes
+ in if check then []
else ["defined item not declared fixed in locale " ^ quote name]
- end;
+ end;
(* check that variables on rhs of definitions are either fixed or on lhs *)
- val err_var_rhs =
- let fun compare_var_sides (t, (_, Const ("==", _) $ d1 $ d2)) =
- let val varl1 = difflist d1 all_loc_consts;
- val varl2 = difflist d2 all_loc_consts
- in t andalso (varl2 subset varl1)
- end
- | compare_var_sides (_,_) =
- locale_error ("Definitions must use the == relation")
+ val err_var_rhs =
+ let fun compare_var_sides (t, (_, Const ("==", _) $ d1 $ d2)) =
+ let val varl1 = difflist d1 all_loc_fixes;
+ val varl2 = difflist d2 all_loc_fixes
+ in t andalso (varl2 subset varl1)
+ end
+ | compare_var_sides (_,_) =
+ locale_error ("Definitions must use the == relation")
val check = foldl compare_var_sides (true, loc_defs)
in if check then []
else ["nonfixed variable on right hand side of a locale definition in locale " ^ quote name]
@@ -505,8 +392,8 @@
else error (cat_lines errs);
syntax_thy
- |> put_locale (name,
- make_locale ancestor loc_consts nosyn loc_thms_terms
+ |> put_locale (name,
+ make_locale parent loc_fixes nosyn loc_thms_terms
loc_defs_terms loc_thms defaults)
end;
@@ -514,45 +401,83 @@
val add_locale = gen_add_locale read_typ read_axm;
val add_locale_i = gen_add_locale cert_typ cert_axm;
-(** print functions **)
-(* idea: substitute all locale contants (Free's) that are syntactical by their
- "real" constant representation (i.e. \\<^locale>constname).
- - function const_ssubst does this substitution
- - function Locale.pretty_term:
- if locale is open then do this substitution & then call Sign.pretty_term
- else call Sign.pretty_term
-*)
-(* substitutes all Free variables s in t by Const's s *)
-fun const_ssubst t s =
- case t of
- Free(v,T) => if v = s then Const("\\<^locale>" ^ s,T) else Free(v,T)
- | Const(c,T) => Const(c,T)
- | Var(v,T) => Var(v,T)
- | Bound x => Bound x
- | Abs(a,T,u) => Abs(a,T, const_ssubst u s)
- | t1 $ t2 => const_ssubst t1 s $ const_ssubst t2 s;
+
+
+(*
+(** 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;
+
-(* FIXME: improve: can be expressed with foldl *)
-fun const_ssubst_list [] t = t
- | const_ssubst_list (s :: l) t = const_ssubst_list l (const_ssubst t s);
+(* get theorems *)
-(* Locale.pretty_term *)
-fun pretty_term sign =
- if (is_open_loc_sg sign) then
- let val locale_list = map snd(get_scope_sg sign);
- val nosyn = flat (map #nosyn locale_list);
- val str_list = (collect_consts sign) \\ nosyn
- in Sign.pretty_term sign o (const_ssubst_list str_list)
- end
- else Sign.pretty_term sign;
+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];