# HG changeset patch # User wenzelm # Date 1004645447 -3600 # Node ID 035ab884b9e0ba165a8b17d9575cac2732ba8ee1 # Parent 8d2372c6b5f3deace7444ab7de69db8c31d17897 beginnings of new locales (not yet functional); diff -r 8d2372c6b5f3 -r 035ab884b9e0 src/Pure/Isar/locale.ML --- 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];