the + facility for locales, by Florian
authorpaulson
Fri Dec 11 10:36:39 1998 +0100 (1998-12-11)
changeset 6022259e4f2114e1
parent 6021 4a3fc834288e
child 6023 832b9269dedd
the + facility for locales, by Florian
src/Pure/Thy/context.ML
src/Pure/Thy/thy_parse.ML
src/Pure/locale.ML
     1.1 --- a/src/Pure/Thy/context.ML	Fri Dec 11 10:34:03 1998 +0100
     1.2 +++ b/src/Pure/Thy/context.ML	Fri Dec 11 10:36:39 1998 +0100
     1.3 @@ -14,7 +14,8 @@
     1.4    val Goal: string -> thm list
     1.5    val Goalw: thm list -> string -> thm list
     1.6    val Open_locale: xstring -> unit
     1.7 -  val Close_locale: unit -> unit
     1.8 +  val Close_locale: xstring -> unit
     1.9 +  val Print_scope: unit -> unit
    1.10    val Export: thm -> thm
    1.11  end;
    1.12  
    1.13 @@ -89,7 +90,8 @@
    1.14  (* scope manipulation *)
    1.15  
    1.16  fun Open_locale xname = (Locale.open_locale xname (the_context ()); ());
    1.17 -fun Close_locale () = (Locale.close_locale (the_context ()); ());
    1.18 +fun Close_locale xname = (Locale.close_locale xname (the_context ()); ());
    1.19 +fun Print_scope () = (Locale.print_scope (the_context()); ());
    1.20  fun Export th = export_thy (the_context ()) th;
    1.21  
    1.22  end;
     2.1 --- a/src/Pure/Thy/thy_parse.ML	Fri Dec 11 10:34:03 1998 +0100
     2.2 +++ b/src/Pure/Thy/thy_parse.ML	Fri Dec 11 10:36:39 1998 +0100
     2.3 @@ -423,7 +423,8 @@
     2.4  (* locale *)
     2.5  
     2.6  val locale_decl =
     2.7 -  (name --$$ "=") --
     2.8 +  (name --$$ "=") -- 
     2.9 +    (optional ((ident >> (fn x => parens ("Some" ^ quote x))) --$$ "+") ("None")) --
    2.10      ("fixes" $$--
    2.11        (repeat (name --$$ "::" -- !! (typ -- opt_mixfix)) 
    2.12         >> (mk_big_list o map mk_triple2))) --
    2.13 @@ -435,7 +436,7 @@
    2.14       ("defines" $$-- (repeat ((ident >> quote) -- !! string) 
    2.15  		      >> (mk_list o map mk_pair)))
    2.16       "[]")
    2.17 -  >> (fn (((nm, cs), asms), defs) => cat_lines [nm, cs, asms, defs]);
    2.18 +  >> (fn ((((nm, ext), cs), asms), defs) => cat_lines [nm, ext, cs, asms, defs]);
    2.19  
    2.20  
    2.21  
     3.1 --- a/src/Pure/locale.ML	Fri Dec 11 10:34:03 1998 +0100
     3.2 +++ b/src/Pure/locale.ML	Fri Dec 11 10:36:39 1998 +0100
     3.3 @@ -14,7 +14,7 @@
     3.4  	v_def "v x == ...x..."
     3.5  
     3.6  TODO:
     3.7 -  - operations on locales: extension, renaming.
     3.8 +  - operations on locales: renaming.
     3.9  *)
    3.10  
    3.11  signature BASIC_LOCALE =
    3.12 @@ -30,12 +30,13 @@
    3.13    val get_thm: theory -> xstring -> thm
    3.14    val get_thms: theory -> xstring -> thm list
    3.15    type locale
    3.16 -  val add_locale: bstring -> (string * string * mixfix) list ->
    3.17 +  val add_locale: bstring -> (bstring option) -> (string * string * mixfix) list ->
    3.18      (string * string) list -> (string * string) list -> theory -> theory
    3.19 -  val add_locale_i: bstring -> (string * typ * mixfix) list ->
    3.20 +  val add_locale_i: bstring -> (bstring option) -> (string * typ * mixfix) list ->
    3.21      (string * term) list -> (string * term) list -> theory -> theory
    3.22    val open_locale: xstring -> theory -> theory
    3.23 -  val close_locale: theory -> theory
    3.24 +  val close_locale: xstring -> theory -> theory
    3.25 +  val print_scope: theory -> unit
    3.26    val in_locale: term list -> Sign.sg -> bool
    3.27    val is_open_loc_sg: Sign.sg -> bool
    3.28    val is_open_loc: theory -> bool
    3.29 @@ -53,18 +54,19 @@
    3.30  (** type locale **)
    3.31  
    3.32  type locale =
    3.33 - {consts: (string * typ) list,
    3.34 + {ancestor: string option,
    3.35 +  consts: (string * typ) list,
    3.36    nosyn: string list,
    3.37    rules: (string * term) list,
    3.38    defs: (string * term) list,
    3.39    thms: (string * thm) list,
    3.40    defaults: (string * sort) list * (string * typ) list * string list};
    3.41  
    3.42 -fun make_locale consts nosyn rules defs thms defaults =
    3.43 -  {consts = consts, nosyn = nosyn, rules = rules, defs = defs,
    3.44 -    thms = thms, defaults = defaults}: locale;
    3.45 +fun make_locale ancestor consts nosyn rules defs thms defaults =
    3.46 +  {ancestor = ancestor, consts = consts, nosyn = nosyn, rules = rules, 
    3.47 +   defs = defs, thms = thms, defaults = defaults}: locale;
    3.48  
    3.49 -fun pretty_locale sg (name, {consts, rules, defs, nosyn = _, thms = _, defaults = _}) =
    3.50 +fun pretty_locale sg (name, {ancestor, consts, rules, defs, nosyn = _, thms = _, defaults = _}) =
    3.51    let
    3.52      val prt_typ = Pretty.quote o Sign.pretty_typ sg;
    3.53      val prt_term = Pretty.quote o Sign.pretty_term sg;
    3.54 @@ -74,8 +76,12 @@
    3.55  
    3.56      fun pretty_axiom (a, t) = Pretty.block
    3.57        [Pretty.str (a ^ ":"), Pretty.brk 1, prt_term t];
    3.58 +
    3.59 +    val anc = case ancestor of
    3.60 +                  None => ""
    3.61 +                | Some(loc) => ((Sign.base_name loc) ^ " +")
    3.62    in
    3.63 -    Pretty.big_list (name ^ " =")
    3.64 +    Pretty.big_list (name ^ " = " ^ anc)
    3.65       [Pretty.big_list "consts:" (map pretty_const consts),
    3.66        Pretty.big_list "rules:" (map pretty_axiom rules),
    3.67        Pretty.big_list "defs:" (map pretty_axiom defs)]
    3.68 @@ -168,13 +174,34 @@
    3.69    | None => error ("Unknown locale " ^ quote xname));
    3.70  
    3.71  fun open_locale xname thy =
    3.72 -  (change_scope (cons (the_locale thy xname)) thy; thy);
    3.73 +  let val loc = the_locale thy xname;
    3.74 +      val anc = #ancestor(#2(loc));
    3.75 +      val cur_sc = get_scope thy;
    3.76 +      fun opn lc th = (change_scope (cons lc) th; th)
    3.77 +  in case anc of
    3.78 +         None => opn loc thy
    3.79 +       | Some(loc') => 
    3.80 +           if loc' mem (map fst cur_sc) 
    3.81 +           then opn loc thy
    3.82 +           else (Pretty.writeln(Pretty.str 
    3.83 +                   ("Opening locale " ^ quote loc' ^ ", required by " ^ quote xname));
    3.84 +                 opn loc (open_locale (Sign.base_name loc') thy))
    3.85 +  end;
    3.86  
    3.87  fun pop_locale [] = error "Currently no open locales"
    3.88    | pop_locale (_ :: locs) = locs;
    3.89  
    3.90 -fun close_locale thy = (change_scope pop_locale thy; thy);
    3.91 +fun close_locale name thy = 
    3.92 +   let val cur_sc = get_scope thy;
    3.93 +       val lname = if null(cur_sc) then "" else (fst (hd cur_sc));
    3.94 +       val bname = Sign.base_name lname
    3.95 +   in if (name = bname) then (change_scope pop_locale thy; thy)
    3.96 +      else (Pretty.writeln(Pretty.str ("locale " ^ name ^ " is not top of scope"));
    3.97 +            Pretty.writeln(Pretty.str ("Command has no effect, top is " ^ lname)); thy)
    3.98 +   end;
    3.99  
   3.100 +fun print_scope thy = 
   3.101 +Pretty.writeln (Pretty.strs ("current scope:" :: rev(map (Sign.base_name o fst) (get_scope thy))));
   3.102  
   3.103  (** functions for goals.ML **)
   3.104  
   3.105 @@ -215,6 +242,12 @@
   3.106  
   3.107  val get_thms = get_thmx (fn x => [x]) PureThy.get_thms;
   3.108  
   3.109 +(* get the defaults of a locale, for extension *)
   3.110 +
   3.111 +fun get_defaults thy name = 
   3.112 +  let val (lname, loc) = the_locale thy name;
   3.113 +  in #defaults(loc)
   3.114 +  end;
   3.115  
   3.116  
   3.117  (** define locales **)
   3.118 @@ -334,13 +367,26 @@
   3.119  
   3.120  (* add_locale *)
   3.121  
   3.122 -fun gen_add_locale prep_typ prep_term bname raw_consts raw_rules raw_defs thy =
   3.123 +fun gen_add_locale prep_typ prep_term bname bancestor raw_consts raw_rules raw_defs thy =
   3.124    let val sign = Theory.sign_of thy;
   3.125  
   3.126      val name = Sign.full_name sign bname;
   3.127  
   3.128 +    val (envSb, old_loc_consts, _) = 
   3.129 +                    case bancestor of
   3.130 +                       Some(loc) => (get_defaults thy loc)
   3.131 +                     | None      => ([],[],[]);
   3.132  
   3.133 -    (* prepare locale consts *)
   3.134 +    val old_nosyn = case bancestor of 
   3.135 +                       Some(loc) => #nosyn(#2(the_locale thy loc))
   3.136 +                     | None      => [];
   3.137 +
   3.138 +    (* Get the full name of the ancestor *)
   3.139 +    val ancestor = case bancestor of 
   3.140 +                       Some(loc) => Some(#1(the_locale thy loc))
   3.141 +                     | None      => None;
   3.142 +
   3.143 +     (* prepare locale consts *)
   3.144  
   3.145      fun prep_const (envS, (raw_c, raw_T, raw_mx)) =
   3.146        let
   3.147 @@ -352,10 +398,11 @@
   3.148          val trfun = if mx = Syntax.NoSyn then None else Some (c_syn, mk_loc_tr c);
   3.149        in (envS', ((c, T), (c_syn, T, mx), trfun)) end;
   3.150  
   3.151 -    val (envS0, loc_consts_syn) = foldl_map prep_const ([], raw_consts);
   3.152 +    val (envS0, loc_consts_syn) = foldl_map prep_const (envSb, raw_consts);
   3.153      val loc_consts = map #1 loc_consts_syn;
   3.154 +    val loc_consts = old_loc_consts @ loc_consts;
   3.155      val loc_syn = map #2 loc_consts_syn;
   3.156 -    val nosyn = map (#1 o #1) (filter (fn x => (#3(#2 x)) = NoSyn) loc_consts_syn);
   3.157 +    val nosyn = old_nosyn @ (map (#1 o #1) (filter (fn x => (#3(#2 x)) = NoSyn) loc_consts_syn));
   3.158      val loc_trfuns = mapfilter #3 loc_consts_syn;
   3.159  
   3.160  
   3.161 @@ -433,8 +480,8 @@
   3.162  
   3.163      syntax_thy
   3.164      |> put_locale (name, 
   3.165 -		   make_locale loc_consts nosyn loc_thms_terms loc_defs_terms
   3.166 -		               loc_thms defaults)
   3.167 +		   make_locale ancestor loc_consts nosyn loc_thms_terms 
   3.168 +                                        loc_defs_terms   loc_thms defaults)
   3.169    end;
   3.170  
   3.171