src/Pure/locale.ML
author wenzelm
Sat Sep 04 21:01:18 1999 +0200 (1999-09-04)
changeset 7469 7a8d3dff34b8
parent 6546 995a66249a9b
child 7628 8e177a4c86a5
permissions -rw-r--r--
ProtoPure: fake empty scope;
     1 (*  Title:      Pure/locale.ML
     2     ID:         $Id$
     3     Author:     Florian Kammueller, University of Cambridge
     4 
     5 Locales. The theory section 'locale' declarings constants, assumptions and
     6 definitions that have local scope.  Typical form is
     7 
     8     locale Locale_name =
     9       fixes   (*variables that are fixed in the locale's scope*)
    10 	v :: T
    11       assumes (*meta-hypothesis that hold in the locale*)
    12 	Asm_name "meta-formula"  
    13       defines (*local definitions of fixed variables in terms of others*)
    14 	v_def "v x == ...x..."
    15 
    16 TODO:
    17   - operations on locales: renaming.
    18 *)
    19 
    20 signature BASIC_LOCALE =
    21 sig
    22   val print_locales: theory -> unit
    23   val print_goals: int -> thm -> unit
    24   val print_goals_marker: string -> int -> thm -> unit
    25   val thm: xstring -> thm
    26   val thms: xstring -> thm list
    27   val Open_locale: xstring -> unit
    28   val Close_locale: xstring -> unit
    29   val Print_scope: unit -> unit
    30 end;
    31 
    32 signature LOCALE =
    33 sig
    34   include BASIC_LOCALE
    35   val get_thm: theory -> xstring -> thm
    36   val get_thms: theory -> xstring -> thm list
    37   type locale
    38   val add_locale: bstring -> (bstring option) -> (string * string * mixfix) list ->
    39     (string * string) list -> (string * string) list -> theory -> theory
    40   val add_locale_i: bstring -> (bstring option) -> (string * typ * mixfix) list ->
    41     (string * term) list -> (string * term) list -> theory -> theory
    42   val open_locale: xstring -> theory -> theory
    43   val close_locale: xstring -> theory -> theory
    44   val print_scope: theory -> unit
    45   val in_locale: term list -> Sign.sg -> bool
    46   val is_open_loc_sg: Sign.sg -> bool
    47   val is_open_loc: theory -> bool
    48   val read_cterm: Sign.sg -> string * typ -> cterm
    49   val get_scope: theory -> (string * locale) list
    50   val get_scope_sg: Sign.sg -> (string * locale) list
    51   val collect_consts: Sign.sg -> string list
    52   val setup: (theory -> theory) list
    53 end;
    54 
    55 structure Locale: LOCALE =
    56 struct
    57 
    58 
    59 (** type locale **)
    60 
    61 type locale =
    62  {ancestor: string option,
    63   consts: (string * typ) list,
    64   nosyn: string list,
    65   rules: (string * term) list,
    66   defs: (string * term) list,
    67   thms: (string * thm) list,
    68   defaults: (string * sort) list * (string * typ) list * string list};
    69 
    70 fun make_locale ancestor consts nosyn rules defs thms defaults =
    71   {ancestor = ancestor, consts = consts, nosyn = nosyn, rules = rules, 
    72    defs = defs, thms = thms, defaults = defaults}: locale;
    73 
    74 fun pretty_locale sg (name, {ancestor, consts, rules, defs, nosyn = _, thms = _, defaults = _}) =
    75   let
    76     val prt_typ = Pretty.quote o Sign.pretty_typ sg;
    77     val prt_term = Pretty.quote o Sign.pretty_term sg;
    78 
    79     fun pretty_const (c, T) = Pretty.block
    80       [Pretty.str (c ^ " ::"), Pretty.brk 1, prt_typ T];
    81 
    82     fun pretty_axiom (a, t) = Pretty.block
    83       [Pretty.str (a ^ ":"), Pretty.brk 1, prt_term t];
    84 
    85     val anc = case ancestor of
    86                   None => ""
    87                 | Some(loc) => ((Sign.base_name loc) ^ " +")
    88   in
    89     Pretty.big_list (name ^ " = " ^ anc)
    90      [Pretty.big_list "consts:" (map pretty_const consts),
    91       Pretty.big_list "rules:" (map pretty_axiom rules),
    92       Pretty.big_list "defs:" (map pretty_axiom defs)]
    93   end;
    94 
    95 
    96 
    97 (** theory data **)
    98 
    99 (* data kind 'Pure/locales' *)
   100 
   101 type locale_data =
   102   {space: NameSpace.T,
   103     locales: locale Symtab.table,
   104     scope: (string * locale) list ref};
   105 
   106 fun make_locale_data space locales scope =
   107   {space = space, locales = locales, scope = scope}: locale_data;
   108 
   109 structure LocalesArgs =
   110 struct
   111   val name = "Pure/locales";
   112   type T = locale_data;
   113 
   114   val empty = make_locale_data NameSpace.empty Symtab.empty (ref []);
   115   fun copy {space, locales, scope = ref locs} = make_locale_data space locales (ref locs);
   116   fun prep_ext {space, locales, scope = _} = make_locale_data space locales (ref []);
   117   fun merge ({space = space1, locales = locales1, scope = _},
   118     {space = space2, locales = locales2, scope = _}) =
   119       make_locale_data (NameSpace.merge (space1, space2))
   120         (Symtab.merge (K true) (locales1, locales2))
   121         (ref []);
   122 
   123   fun print sg {space, locales, scope} =
   124     let
   125       fun extrn name =
   126         if ! long_names then name else NameSpace.extern space name;
   127       val locs = map (apfst extrn) (Symtab.dest locales);
   128       val scope_names = rev (map (extrn o fst) (! scope));
   129     in
   130       Pretty.writeln (Display.pretty_name_space ("locale name space", space));
   131       Pretty.writeln (Pretty.big_list "locales:" (map (pretty_locale sg) locs));
   132       Pretty.writeln (Pretty.strs ("current scope:" :: scope_names))
   133     end;
   134 end;
   135 
   136 
   137 structure LocalesData = TheoryDataFun(LocalesArgs);
   138 val print_locales = LocalesData.print;
   139 
   140 
   141 (* access locales *)
   142 
   143 fun get_locale_sg sg name = Symtab.lookup (#locales (LocalesData.get_sg sg), name);
   144 
   145 val get_locale = get_locale_sg o Theory.sign_of;
   146 
   147 fun put_locale (name, locale) thy =
   148   let
   149     val {space, locales, scope} = LocalesData.get thy;
   150     val space' = NameSpace.extend (space, [name]);
   151     val locales' = Symtab.update ((name, locale), locales);
   152   in thy |> LocalesData.put (make_locale_data space' locales' scope) end;
   153 
   154 fun lookup_locale thy xname =
   155   let
   156     val {space, locales, ...} = LocalesData.get thy;
   157     val name = NameSpace.intern space xname;
   158   in apsome (pair name) (get_locale thy name) end;
   159 
   160 
   161 (* access scope *)
   162 
   163 fun get_scope_sg sg =
   164   if Sign.eq_sg (sg, Theory.sign_of ProtoPure.thy) then []
   165   else ! (#scope (LocalesData.get_sg sg));
   166 
   167 val get_scope = get_scope_sg o Theory.sign_of;
   168 
   169 fun change_scope f thy =
   170   let val {scope, ...} = LocalesData.get thy
   171   in scope := f (! scope) end;
   172 
   173 
   174 
   175 (** scope operations **)
   176 
   177 (* change scope *)
   178 
   179 fun the_locale thy xname =
   180   (case lookup_locale thy xname of
   181     Some loc => loc
   182   | None => error ("Unknown locale " ^ quote xname));
   183 
   184 fun open_locale xname thy =
   185   let val loc = the_locale thy xname;
   186       val anc = #ancestor(#2(loc));
   187       val cur_sc = get_scope thy;
   188       fun opn lc th = (change_scope (cons lc) th; th)
   189   in case anc of
   190          None => opn loc thy
   191        | Some(loc') => 
   192            if loc' mem (map fst cur_sc) 
   193            then opn loc thy
   194            else (Pretty.writeln(Pretty.str 
   195                    ("Opening locale " ^ quote loc' ^ ", required by " ^ quote xname));
   196                  opn loc (open_locale (Sign.base_name loc') thy))
   197   end;
   198 
   199 fun pop_locale [] = error "Currently no open locales"
   200   | pop_locale (_ :: locs) = locs;
   201 
   202 fun close_locale name thy = 
   203    let val cur_sc = get_scope thy;
   204        val lname = if null(cur_sc) then "" else (fst (hd cur_sc));
   205        val bname = Sign.base_name lname
   206    in if (name = bname) then (change_scope pop_locale thy; thy)
   207       else (Pretty.writeln(Pretty.str ("locale " ^ name ^ " is not top of scope"));
   208             Pretty.writeln(Pretty.str ("Command has no effect, top is " ^ lname)); thy)
   209    end;
   210 
   211 fun print_scope thy = 
   212 Pretty.writeln (Pretty.strs ("current scope:" :: rev(map (Sign.base_name o fst) (get_scope thy))));
   213 
   214 (*implicit context versions*)
   215 fun Open_locale xname = (open_locale xname (Context.the_context ()); ());
   216 fun Close_locale xname = (close_locale xname (Context.the_context ()); ());
   217 fun Print_scope () = (print_scope (Context.the_context ()); ());
   218 
   219 
   220 (** functions for goals.ML **)
   221 
   222 (* in_locale: check if hyps (: term list) of a proof are contained in the
   223    (current) scope. This function is needed in prepare_proof. It needs to
   224    refer to the signature, because theory is not available in prepare_proof. *)
   225 
   226 fun in_locale hyps sg =
   227     let val cur_sc = get_scope_sg sg;
   228         val rule_lists = map (#rules o snd) cur_sc;
   229         val def_lists = map (#defs o snd) cur_sc;
   230         val rules = map snd (foldr (op union) (rule_lists, []));
   231         val defs = map snd (foldr (op union) (def_lists, []));
   232         val defnrules = rules @ defs;
   233     in
   234         hyps subset defnrules
   235     end;
   236 
   237 
   238 (* is_open_loc: check if any locale is open, i.e. in the scope of the current thy *)
   239 fun is_open_loc_sg sign =
   240     let val cur_sc = get_scope_sg sign
   241     in not(null(cur_sc)) end;
   242 
   243 val is_open_loc = is_open_loc_sg o Theory.sign_of;
   244 
   245 
   246 (* get theorems *)
   247 
   248 fun get_thm_locale name ((_, {thms, ...}: locale)) = assoc (thms, name);
   249 
   250 fun get_thmx f get thy name =
   251   (case get_first (get_thm_locale name) (get_scope thy) of
   252     Some thm => f thm
   253   | None => get thy name);
   254 
   255 val get_thm = get_thmx I PureThy.get_thm;
   256 val get_thms = get_thmx (fn x => [x]) PureThy.get_thms;
   257 
   258 fun thm name = get_thm (Context.the_context ()) name;
   259 fun thms name = get_thms (Context.the_context ()) name;
   260 
   261 
   262 (* get the defaults of a locale, for extension *)
   263 
   264 fun get_defaults thy name = 
   265   let val (lname, loc) = the_locale thy name;
   266   in #defaults(loc)
   267   end;
   268 
   269 
   270 (** define locales **)
   271 
   272 (* prepare types *)
   273 
   274 fun read_typ sg (envT, s) =
   275   let
   276     fun def_sort (x, ~1) = assoc (envT, x)
   277       | def_sort _ = None;
   278     val T = Type.no_tvars (Sign.read_typ (sg, def_sort) s) handle TYPE (msg, _, _) => error msg;
   279   in (Term.add_typ_tfrees (T, envT), T) end;
   280 
   281 fun cert_typ sg (envT, raw_T) =
   282   let val T = Type.no_tvars (Sign.certify_typ sg raw_T) handle TYPE (msg, _, _) => error msg
   283   in (Term.add_typ_tfrees (T, envT), T) end;
   284 
   285 
   286 (* prepare props *)
   287 
   288 val add_frees = foldl_aterms (fn (vs, Free v) => v ins vs | (vs, _) => vs);
   289 
   290 fun enter_term t (envS, envT, used) =
   291   (Term.add_term_tfrees (t, envS), add_frees (envT, t), Term.add_term_tfree_names (t, used));
   292 
   293 fun read_axm sg ((envS, envT, used), (name, s)) =
   294   let
   295     fun def_sort (x, ~1) = assoc (envS, x)
   296       | def_sort _ = None;
   297     fun def_type (x, ~1) = assoc (envT, x)
   298       | def_type _ = None;
   299     val (_, t) = Theory.read_def_axm (sg, def_type, def_sort) used (name, s);
   300   in
   301     (enter_term t (envS, envT, used), t)
   302   end;
   303 
   304 
   305 fun cert_axm sg ((envS, envT, used), (name, raw_t)) =
   306   let val (_, t) = Theory.cert_axm sg (name, raw_t)
   307   in (enter_term t (envS, envT, used), t) end;
   308 
   309 
   310 (* Locale.read_cterm: read in a string as a certified term, and respect the bindings
   311    that already exist for subterms. If no locale is open, this function is equal to
   312    Thm.read_cterm  *)
   313 
   314 fun read_cterm sign =
   315     let val cur_sc = get_scope_sg sign;
   316         val defaults = map (#defaults o snd) cur_sc;
   317         val envS = flat (map #1 defaults);
   318         val envT = flat (map #2 defaults);
   319         val used = flat (map #3 defaults);
   320         fun def_sort (x, ~1) = assoc (envS, x)
   321           | def_sort _ = None;
   322         fun def_type (x, ~1) = assoc (envT, x)
   323           | def_type _ = None;
   324     in (if (is_open_loc_sg sign)
   325         then (#1 o read_def_cterm (sign, def_type, def_sort) used true)
   326         else Thm.read_cterm sign)
   327     end;
   328 
   329 (* basic functions needed for definitions and display *)
   330 (* collect all locale constants of a scope, i.e. a list of locales *)
   331 fun collect_consts sg =
   332     let val cur_sc = get_scope_sg sg;
   333         val locale_list = map snd cur_sc;
   334         val const_list = flat (map #consts locale_list)
   335     in map fst const_list end;
   336 
   337 (* filter out the Free's in a term *)
   338 fun list_frees t =
   339     case t of Const(c,T) => []
   340   | Var(v,T) => []
   341   | Free(v,T)=> [Free(v,T)]
   342   | Bound x  => []
   343   | Abs(a,T,u) => list_frees u
   344   | t1 $ t2  => (list_frees t1)  @ (list_frees t2);
   345 
   346 (* filter out all Free's in a term that are not contained
   347    in a list of strings. Used to prepare definitions. The list of strings
   348    will be the consts of the scope. We filter out the "free" Free's to be
   349    able to bind them *)
   350 fun difflist term clist =
   351     let val flist = list_frees term;
   352         fun builddiff [] sl = []
   353           | builddiff (t :: tl) sl =
   354             let val Free(v,T) = t
   355             in
   356                 if (v mem sl)
   357                 then builddiff tl sl
   358                 else t :: (builddiff tl sl)
   359             end;
   360     in distinct(builddiff flist clist) end;
   361 
   362 (* Bind a term with !! over a list of "free" Free's.
   363    To enable definitions like x + y == .... (without quantifier).
   364    Complications, because x and y have to be removed from defaults *)
   365 fun abs_over_free clist ((defaults: (string * sort) list * (string * typ) list * string list), (s, term)) =
   366     let val diffl = rev(difflist term clist);
   367         fun abs_o (t, (x as Free(v,T))) = all(T) $ Abs(v, T, abstract_over (x,t))
   368           | abs_o (_ , _) = error ("Can't be: abs_over_free");
   369         val diffl' = map (fn (Free (s, T)) => s) diffl;
   370         val defaults' = (#1 defaults, filter (fn x => not((fst x) mem diffl')) (#2 defaults), #3 defaults)
   371     in (defaults', (s, foldl abs_o (term, diffl))) end;
   372 
   373 (* assume a definition, i.e assume the cterm of a definiton term and then eliminate
   374    the binding !!, so that the def can be applied as rewrite. The meta hyp will still contain !! *)
   375 fun prep_hyps clist sg = forall_elim_vars(0) o Thm.assume o (Thm.cterm_of sg);
   376 
   377 
   378 (* concrete syntax *)
   379 
   380 fun mark_syn c = "\\<^locale>" ^ c;
   381 
   382 fun mk_loc_tr c ts = list_comb (Free (c, dummyT), ts);
   383 
   384 
   385 (* add_locale *)
   386 
   387 fun gen_add_locale prep_typ prep_term bname bancestor raw_consts raw_rules raw_defs thy =
   388   let val sign = Theory.sign_of thy;
   389 
   390     val name = Sign.full_name sign bname;
   391 
   392     val (envSb, old_loc_consts, _) = 
   393                     case bancestor of
   394                        Some(loc) => (get_defaults thy loc)
   395                      | None      => ([],[],[]);
   396 
   397     val old_nosyn = case bancestor of 
   398                        Some(loc) => #nosyn(#2(the_locale thy loc))
   399                      | None      => [];
   400 
   401     (* Get the full name of the ancestor *)
   402     val ancestor = case bancestor of 
   403                        Some(loc) => Some(#1(the_locale thy loc))
   404                      | None      => None;
   405 
   406      (* prepare locale consts *)
   407 
   408     fun prep_const (envS, (raw_c, raw_T, raw_mx)) =
   409       let
   410         val c = Syntax.const_name raw_c raw_mx;
   411         val c_syn = mark_syn c;
   412         val mx = Syntax.fix_mixfix raw_c raw_mx;
   413         val (envS', T) = prep_typ sign (envS, raw_T) handle ERROR =>
   414           error ("The error(s) above occured in locale constant " ^ quote c);
   415         val trfun = if mx = Syntax.NoSyn then None else Some (c_syn, mk_loc_tr c);
   416       in (envS', ((c, T), (c_syn, T, mx), trfun)) end;
   417 
   418     val (envS0, loc_consts_syn) = foldl_map prep_const (envSb, raw_consts);
   419     val loc_consts = map #1 loc_consts_syn;
   420     val loc_consts = old_loc_consts @ loc_consts;
   421     val loc_syn = map #2 loc_consts_syn;
   422     val nosyn = old_nosyn @ (map (#1 o #1) (filter (fn x => (#3(#2 x)) = NoSyn) loc_consts_syn));
   423     val loc_trfuns = mapfilter #3 loc_consts_syn;
   424 
   425 
   426     (* 1st stage: syntax_thy *)
   427 
   428     val syntax_thy =
   429       thy
   430       |> Theory.add_modesyntax_i ("", true) loc_syn
   431       |> Theory.add_trfuns ([], loc_trfuns, [], []);
   432 
   433     val syntax_sign = Theory.sign_of syntax_thy;
   434 
   435 
   436     (* prepare rules and defs *)
   437 
   438     fun prep_axiom (env, (a, raw_t)) =
   439       let
   440         val (env', t) = prep_term syntax_sign (env, (a, raw_t)) handle ERROR =>
   441           error ("The error(s) above occured in locale rule / definition " ^ quote a);
   442       in (env', (a, t)) end;
   443 
   444     val ((envS1, envT1, used1), loc_rules) =
   445       foldl_map prep_axiom ((envS0, loc_consts, map fst envS0), raw_rules);
   446     val (defaults, loc_defs) = 
   447 	foldl_map prep_axiom ((envS1, envT1, used1), raw_defs);
   448 
   449     val old_loc_consts = collect_consts syntax_sign;
   450     val new_loc_consts = (map #1 loc_consts);
   451     val all_loc_consts = old_loc_consts @ new_loc_consts;
   452 
   453     val (defaults, loc_defs_terms) = 
   454 	foldl_map (abs_over_free all_loc_consts) (defaults, loc_defs);
   455     val loc_defs_thms = 
   456 	map (apsnd (prep_hyps (map #1 loc_consts) syntax_sign)) loc_defs_terms;
   457     val (defaults, loc_thms_terms) = 
   458 	foldl_map (abs_over_free all_loc_consts) (defaults, loc_rules);
   459     val loc_thms = map (apsnd (prep_hyps (map #1 loc_consts) syntax_sign))
   460 		       (loc_thms_terms)
   461                    @ loc_defs_thms;
   462 
   463 
   464     (* error messages *) 
   465 
   466     fun locale_error msg = error (msg ^ "\nFor locale " ^ quote name);
   467 
   468     val err_dup_locale =
   469       if is_none (get_locale thy name) then []
   470       else ["Duplicate definition of locale " ^ quote name];
   471 
   472     (* check if definientes are locale constants 
   473        (in the same locale, so no redefining!) *)
   474     val err_def_head =
   475       let fun peal_appl t = 
   476             case t of 
   477                  t1 $ t2 => peal_appl t1
   478                | Free(t) => t
   479                | _ => locale_error ("Bad form of LHS in locale definition");
   480 	  fun lhs (_, Const ("==" , _) $  d1 $ d2) = peal_appl d1
   481 	    | lhs _ = locale_error ("Definitions must use the == relation");
   482           val defs = map lhs loc_defs;
   483           val check = defs subset loc_consts
   484       in if check then [] 
   485          else ["defined item not declared fixed in locale " ^ quote name]
   486       end; 
   487 
   488     (* check that variables on rhs of definitions are either fixed or on lhs *)
   489     val err_var_rhs = 
   490       let fun compare_var_sides (t, (_, Const ("==", _) $ d1 $ d2)) = 
   491 		let val varl1 = difflist d1 all_loc_consts;
   492 		    val varl2 = difflist d2 all_loc_consts
   493 		in t andalso (varl2 subset varl1)
   494 		end
   495             | compare_var_sides (_,_) = 
   496 		locale_error ("Definitions must use the == relation")
   497           val check = foldl compare_var_sides (true, loc_defs)
   498       in if check then []
   499          else ["nonfixed variable on right hand side of a locale definition in locale " ^ quote name]
   500       end;
   501 
   502     val errs = err_dup_locale @ err_def_head @ err_var_rhs;
   503   in
   504     if null errs then ()
   505     else error (cat_lines errs);
   506 
   507     syntax_thy
   508     |> put_locale (name, 
   509 		   make_locale ancestor loc_consts nosyn loc_thms_terms 
   510                                         loc_defs_terms   loc_thms defaults)
   511   end;
   512 
   513 
   514 val add_locale = gen_add_locale read_typ read_axm;
   515 val add_locale_i = gen_add_locale cert_typ cert_axm;
   516 
   517 (** print functions **)
   518 (* idea: substitute all locale contants (Free's) that are syntactical by their
   519          "real" constant representation (i.e. \\<^locale>constname).
   520    - function const_ssubst does this substitution
   521    - function Locale.pretty_term:
   522              if locale is open then do this substitution & then call Sign.pretty_term
   523              else call Sign.pretty_term
   524 *)
   525 (* substitutes all Free variables s in t by Const's s *)
   526 fun const_ssubst t s =
   527     case t  of
   528         Free(v,T) => if v = s then Const("\\<^locale>" ^ s,T) else Free(v,T)
   529       | Const(c,T) => Const(c,T)
   530       | Var(v,T) => Var(v,T)
   531       | Bound x  => Bound x
   532       | Abs(a,T,u) => Abs(a,T, const_ssubst u s)
   533       | t1 $ t2  => const_ssubst t1 s $ const_ssubst t2 s;
   534 
   535 (* FIXME: improve: can be expressed with foldl *)
   536 fun const_ssubst_list [] t = t
   537   | const_ssubst_list (s :: l) t = const_ssubst_list l (const_ssubst t s);
   538 
   539 (* Locale.pretty_term *)
   540 fun pretty_term sign =
   541     if (is_open_loc_sg sign) then
   542         let val locale_list = map snd(get_scope_sg sign);
   543             val nosyn = flat (map #nosyn locale_list);
   544             val str_list = (collect_consts sign) \\ nosyn
   545         in Sign.pretty_term sign o (const_ssubst_list str_list)
   546         end
   547     else Sign.pretty_term sign;
   548 
   549 
   550 
   551 (** print_goals **)
   552 
   553 (*print thm A1,...,An/B in "goal style" -- premises as numbered subgoals*)
   554 
   555 local
   556 
   557   (* utils *)
   558 
   559   fun ins_entry (x, y) [] = [(x, [y])]
   560     | ins_entry (x, y) ((pair as (x', ys')) :: pairs) =
   561         if x = x' then (x', y ins ys') :: pairs
   562         else pair :: ins_entry (x, y) pairs;
   563 
   564   fun add_consts (Const (c, T), env) = ins_entry (T, (c, T)) env
   565     | add_consts (t $ u, env) = add_consts (u, add_consts (t, env))
   566     | add_consts (Abs (_, _, t), env) = add_consts (t, env)
   567     | add_consts (_, env) = env;
   568 
   569   fun add_vars (Free (x, T), env) = ins_entry (T, (x, ~1)) env
   570     | add_vars (Var (xi, T), env) = ins_entry (T, xi) env
   571     | add_vars (Abs (_, _, t), env) = add_vars (t, env)
   572     | add_vars (t $ u, env) = add_vars (u, add_vars (t, env))
   573     | add_vars (_, env) = env;
   574 
   575   fun add_varsT (Type (_, Ts), env) = foldr add_varsT (Ts, env)
   576     | add_varsT (TFree (x, S), env) = ins_entry (S, (x, ~1)) env
   577     | add_varsT (TVar (xi, S), env) = ins_entry (S, xi) env;
   578 
   579   fun sort_idxs vs = map (apsnd (sort (prod_ord string_ord int_ord))) vs;
   580   fun sort_cnsts cs = map (apsnd (sort_wrt fst)) cs;
   581 
   582 
   583   (* prepare atoms *)
   584 
   585   fun consts_of t = sort_cnsts (add_consts (t, []));
   586   fun vars_of t = sort_idxs (add_vars (t, []));
   587   fun varsT_of t = rev (sort_idxs (it_term_types add_varsT (t, [])));
   588 
   589 in
   590 
   591   fun print_goals_marker begin_goal maxgoals state =
   592     let
   593       val {sign, ...} = rep_thm state;
   594 
   595       val prt_term = pretty_term sign;
   596       val prt_typ = Sign.pretty_typ sign;
   597       val prt_sort = Sign.pretty_sort sign;
   598 
   599       fun prt_atoms prt prtT (X, xs) = Pretty.block
   600         [Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::",
   601           Pretty.brk 1, prtT X];
   602 
   603       fun prt_var (x, ~1) = prt_term (Syntax.free x)
   604         | prt_var xi = prt_term (Syntax.var xi);
   605 
   606       fun prt_varT (x, ~1) = prt_typ (TFree (x, []))
   607         | prt_varT xi = prt_typ (TVar (xi, []));
   608 
   609       val prt_consts = prt_atoms (prt_term o Const) prt_typ;
   610       val prt_vars = prt_atoms prt_var prt_typ;
   611       val prt_varsT = prt_atoms prt_varT prt_sort;
   612 
   613 
   614       fun print_list _ _ [] = ()
   615         | print_list name prt lst = (writeln "";
   616             Pretty.writeln (Pretty.big_list name (map prt lst)));
   617 
   618       fun print_subgoals (_, []) = ()
   619         | print_subgoals (n, A :: As) = (Pretty.writeln (Pretty.blk (0,
   620             [Pretty.str (begin_goal ^ " " ^ string_of_int n ^ ". "), prt_term A]));
   621               print_subgoals (n + 1, As));
   622 
   623       val print_ffpairs =
   624         print_list "Flex-flex pairs:" (prt_term o Logic.mk_flexpair);
   625 
   626       val print_consts = print_list "Constants:" prt_consts o consts_of;
   627       val print_vars = print_list "Variables:" prt_vars o vars_of;
   628       val print_varsT = print_list "Type variables:" prt_varsT o varsT_of;
   629 
   630 
   631       val {prop, ...} = rep_thm state;
   632       val (tpairs, As, B) = Logic.strip_horn prop;
   633       val ngoals = length As;
   634 
   635       fun print_gs (types, sorts) =
   636        (Pretty.writeln (prt_term B);
   637         if ngoals = 0 then writeln "No subgoals!"
   638         else if ngoals > maxgoals then
   639           (print_subgoals (1, take (maxgoals, As));
   640             writeln ("A total of " ^ string_of_int ngoals ^ " subgoals..."))
   641         else print_subgoals (1, As);
   642 
   643         print_ffpairs tpairs;
   644 
   645         if types andalso ! show_consts then print_consts prop else ();
   646         if types then print_vars prop else ();
   647         if sorts then print_varsT prop else ());
   648     in
   649       setmp show_no_free_types true
   650         (setmp show_types (! show_types orelse ! show_sorts)
   651           (setmp show_sorts false print_gs))
   652      (! show_types orelse ! show_sorts, ! show_sorts)
   653   end;
   654 
   655   val print_goals = print_goals_marker "";
   656 
   657 end;
   658 
   659 
   660 
   661 (** locale theory setup **)
   662 
   663 val setup =
   664  [LocalesData.init];
   665 
   666 end;
   667 
   668 structure BasicLocale: BASIC_LOCALE = Locale;
   669 open BasicLocale;