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