# HG changeset patch # User paulson # Date 913368999 -3600 # Node ID 259e4f2114e19aef98ad597d6d85ae67f78124b4 # Parent 4a3fc834288ea23d3cdfd0166d111e7a2e523b48 the + facility for locales, by Florian diff -r 4a3fc834288e -r 259e4f2114e1 src/Pure/Thy/context.ML --- a/src/Pure/Thy/context.ML Fri Dec 11 10:34:03 1998 +0100 +++ b/src/Pure/Thy/context.ML Fri Dec 11 10:36:39 1998 +0100 @@ -14,7 +14,8 @@ val Goal: string -> thm list val Goalw: thm list -> string -> thm list val Open_locale: xstring -> unit - val Close_locale: unit -> unit + val Close_locale: xstring -> unit + val Print_scope: unit -> unit val Export: thm -> thm end; @@ -89,7 +90,8 @@ (* scope manipulation *) fun Open_locale xname = (Locale.open_locale xname (the_context ()); ()); -fun Close_locale () = (Locale.close_locale (the_context ()); ()); +fun Close_locale xname = (Locale.close_locale xname (the_context ()); ()); +fun Print_scope () = (Locale.print_scope (the_context()); ()); fun Export th = export_thy (the_context ()) th; end; diff -r 4a3fc834288e -r 259e4f2114e1 src/Pure/Thy/thy_parse.ML --- a/src/Pure/Thy/thy_parse.ML Fri Dec 11 10:34:03 1998 +0100 +++ b/src/Pure/Thy/thy_parse.ML Fri Dec 11 10:36:39 1998 +0100 @@ -423,7 +423,8 @@ (* locale *) val locale_decl = - (name --$$ "=") -- + (name --$$ "=") -- + (optional ((ident >> (fn x => parens ("Some" ^ quote x))) --$$ "+") ("None")) -- ("fixes" $$-- (repeat (name --$$ "::" -- !! (typ -- opt_mixfix)) >> (mk_big_list o map mk_triple2))) -- @@ -435,7 +436,7 @@ ("defines" $$-- (repeat ((ident >> quote) -- !! string) >> (mk_list o map mk_pair))) "[]") - >> (fn (((nm, cs), asms), defs) => cat_lines [nm, cs, asms, defs]); + >> (fn ((((nm, ext), cs), asms), defs) => cat_lines [nm, ext, cs, asms, defs]); diff -r 4a3fc834288e -r 259e4f2114e1 src/Pure/locale.ML --- a/src/Pure/locale.ML Fri Dec 11 10:34:03 1998 +0100 +++ b/src/Pure/locale.ML Fri Dec 11 10:36:39 1998 +0100 @@ -14,7 +14,7 @@ v_def "v x == ...x..." TODO: - - operations on locales: extension, renaming. + - operations on locales: renaming. *) signature BASIC_LOCALE = @@ -30,12 +30,13 @@ val get_thm: theory -> xstring -> thm val get_thms: theory -> xstring -> thm list type locale - val add_locale: bstring -> (string * string * mixfix) list -> + val add_locale: bstring -> (bstring option) -> (string * string * mixfix) list -> (string * string) list -> (string * string) list -> theory -> theory - val add_locale_i: bstring -> (string * typ * mixfix) list -> + 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: 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 @@ -53,18 +54,19 @@ (** type locale **) type locale = - {consts: (string * typ) list, + {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}; -fun make_locale consts nosyn rules defs thms defaults = - {consts = consts, nosyn = nosyn, rules = rules, defs = defs, - thms = thms, defaults = defaults}: locale; +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; -fun pretty_locale sg (name, {consts, rules, defs, nosyn = _, thms = _, defaults = _}) = +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; @@ -74,8 +76,12 @@ fun pretty_axiom (a, t) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, prt_term t]; + + val anc = case ancestor of + None => "" + | Some(loc) => ((Sign.base_name loc) ^ " +") in - Pretty.big_list (name ^ " =") + 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)] @@ -168,13 +174,34 @@ | None => error ("Unknown locale " ^ quote xname)); fun open_locale xname thy = - (change_scope (cons (the_locale thy xname)) thy; 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 (Pretty.writeln(Pretty.str + ("Opening locale " ^ quote loc' ^ ", required by " ^ quote xname)); + opn loc (open_locale (Sign.base_name loc') thy)) + end; fun pop_locale [] = error "Currently no open locales" | pop_locale (_ :: locs) = locs; -fun close_locale thy = (change_scope pop_locale thy; thy); +fun close_locale name thy = + let val cur_sc = get_scope thy; + val lname = if null(cur_sc) then "" else (fst (hd cur_sc)); + val bname = Sign.base_name lname + in if (name = bname) then (change_scope pop_locale thy; thy) + else (Pretty.writeln(Pretty.str ("locale " ^ name ^ " is not top of scope")); + Pretty.writeln(Pretty.str ("Command has no effect, top is " ^ lname)); thy) + end; +fun print_scope thy = +Pretty.writeln (Pretty.strs ("current scope:" :: rev(map (Sign.base_name o fst) (get_scope thy)))); (** functions for goals.ML **) @@ -215,6 +242,12 @@ val get_thms = get_thmx (fn x => [x]) PureThy.get_thms; +(* 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; (** define locales **) @@ -334,13 +367,26 @@ (* add_locale *) -fun gen_add_locale prep_typ prep_term bname raw_consts raw_rules raw_defs thy = +fun gen_add_locale prep_typ prep_term bname bancestor raw_consts raw_rules 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) + | None => ([],[],[]); - (* prepare locale consts *) + val old_nosyn = case bancestor 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)) + | None => None; + + (* prepare locale consts *) fun prep_const (envS, (raw_c, raw_T, raw_mx)) = let @@ -352,10 +398,11 @@ 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 ([], raw_consts); + 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 = map (#1 o #1) (filter (fn x => (#3(#2 x)) = NoSyn) 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; @@ -433,8 +480,8 @@ syntax_thy |> put_locale (name, - make_locale loc_consts nosyn loc_thms_terms loc_defs_terms - loc_thms defaults) + make_locale ancestor loc_consts nosyn loc_thms_terms + loc_defs_terms loc_thms defaults) end;