diff -r feed7bb2a607 -r 4c16bdee47d4 src/Pure/Isar/locale.ML --- 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];