src/Pure/Tools/find_theorems.ML
author wenzelm
Mon Dec 22 16:44:24 2014 +0100 (2014-12-22 ago)
changeset 59175 bf465f335e85
parent 59098 b6ba3adb48e3
child 59498 50b60f501b05
permissions -rw-r--r--
system option "pretty_margin" is superseded by "thy_output_margin";
     1 (*  Title:      Pure/Tools/find_theorems.ML
     2     Author:     Rafal Kolanski and Gerwin Klein, NICTA
     3     Author:     Lars Noschinski and Alexander Krauss, TU Muenchen
     4 
     5 Retrieve theorems from proof context.
     6 *)
     7 
     8 signature FIND_THEOREMS =
     9 sig
    10   datatype 'term criterion =
    11     Name of string | Intro | Elim | Dest | Solves | Simp of 'term | Pattern of 'term
    12   type 'term query = {
    13     goal: thm option,
    14     limit: int option,
    15     rem_dups: bool,
    16     criteria: (bool * 'term criterion) list
    17   }
    18   val read_query: Position.T -> string -> (bool * string criterion) list
    19   val find_theorems: Proof.context -> thm option -> int option -> bool ->
    20     (bool * term criterion) list -> int option * (Facts.ref * thm) list
    21   val find_theorems_cmd: Proof.context -> thm option -> int option -> bool ->
    22     (bool * string criterion) list -> int option * (Facts.ref * thm) list
    23   val pretty_thm: Proof.context -> Facts.ref * thm -> Pretty.T
    24 end;
    25 
    26 structure Find_Theorems: FIND_THEOREMS =
    27 struct
    28 
    29 (** search criteria **)
    30 
    31 datatype 'term criterion =
    32   Name of string | Intro | Elim | Dest | Solves | Simp of 'term | Pattern of 'term;
    33 
    34 fun read_criterion _ (Name name) = Name name
    35   | read_criterion _ Intro = Intro
    36   | read_criterion _ Elim = Elim
    37   | read_criterion _ Dest = Dest
    38   | read_criterion _ Solves = Solves
    39   | read_criterion ctxt (Simp str) = Simp (Proof_Context.read_term_pattern ctxt str)
    40   | read_criterion ctxt (Pattern str) = Pattern (Proof_Context.read_term_pattern ctxt str);
    41 
    42 fun pretty_criterion ctxt (b, c) =
    43   let
    44     fun prfx s = if b then s else "-" ^ s;
    45   in
    46     (case c of
    47       Name name => Pretty.str (prfx "name: " ^ quote name)
    48     | Intro => Pretty.str (prfx "intro")
    49     | Elim => Pretty.str (prfx "elim")
    50     | Dest => Pretty.str (prfx "dest")
    51     | Solves => Pretty.str (prfx "solves")
    52     | Simp pat => Pretty.block [Pretty.str (prfx "simp:"), Pretty.brk 1,
    53         Pretty.quote (Syntax.pretty_term ctxt (Term.show_dummy_patterns pat))]
    54     | Pattern pat => Pretty.enclose (prfx "\"") "\""
    55         [Syntax.pretty_term ctxt (Term.show_dummy_patterns pat)])
    56   end;
    57 
    58 
    59 
    60 (** queries **)
    61 
    62 type 'term query = {
    63   goal: thm option,
    64   limit: int option,
    65   rem_dups: bool,
    66   criteria: (bool * 'term criterion) list
    67 };
    68 
    69 fun map_criteria f {goal, limit, rem_dups, criteria} =
    70   {goal = goal, limit = limit, rem_dups = rem_dups, criteria = f criteria};
    71 
    72 
    73 (** search criterion filters **)
    74 
    75 (*generated filters are to be of the form
    76   input: (Facts.ref * thm)
    77   output: (p:int, s:int, t:int) option, where
    78     NONE indicates no match
    79     p is the primary sorting criterion
    80       (eg. size of term)
    81     s is the secondary sorting criterion
    82       (eg. number of assumptions in the theorem)
    83     t is the tertiary sorting criterion
    84       (eg. size of the substitution for intro, elim and dest)
    85   when applying a set of filters to a thm, fold results in:
    86     (max p, max s, sum of all t)
    87 *)
    88 
    89 
    90 (* matching theorems *)
    91 
    92 fun is_nontrivial thy = Term.is_Const o Term.head_of o Object_Logic.drop_judgment thy;
    93 
    94 (*extract terms from term_src, refine them to the parts that concern us,
    95   if po try match them against obj else vice versa.
    96   trivial matches are ignored.
    97   returns: smallest substitution size*)
    98 fun is_matching_thm (extract_terms, refine_term) ctxt po obj term_src =
    99   let
   100     val thy = Proof_Context.theory_of ctxt;
   101 
   102     fun matches pat =
   103       is_nontrivial thy pat andalso
   104       Pattern.matches thy (if po then (pat, obj) else (obj, pat));
   105 
   106     fun subst_size pat =
   107       let val (_, subst) =
   108         Pattern.match thy (if po then (pat, obj) else (obj, pat)) (Vartab.empty, Vartab.empty)
   109       in Vartab.fold (fn (_, (_, t)) => fn n => size_of_term t + n) subst 0 end;
   110 
   111     fun best_match [] = NONE
   112       | best_match xs = SOME (foldl1 Int.min xs);
   113 
   114     val match_thm = matches o refine_term;
   115   in
   116     map (subst_size o refine_term) (filter match_thm (extract_terms term_src))
   117     |> best_match
   118   end;
   119 
   120 
   121 (* filter_name *)
   122 
   123 fun filter_name str_pat (thmref, _) =
   124   if match_string str_pat (Facts.name_of_ref thmref)
   125   then SOME (0, 0, 0) else NONE;
   126 
   127 
   128 (* filter intro/elim/dest/solves rules *)
   129 
   130 fun filter_dest ctxt goal (_, thm) =
   131   let
   132     val extract_dest =
   133      (fn thm => if Thm.no_prems thm then [] else [Thm.full_prop_of thm],
   134       hd o Logic.strip_imp_prems);
   135     val prems = Logic.prems_of_goal goal 1;
   136 
   137     fun try_subst prem = is_matching_thm extract_dest ctxt true prem thm;
   138     val successful = prems |> map_filter try_subst;
   139   in
   140     (*if possible, keep best substitution (one with smallest size)*)
   141     (*dest rules always have assumptions, so a dest with one
   142       assumption is as good as an intro rule with none*)
   143     if not (null successful) then
   144       SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm - 1, foldl1 Int.min successful)
   145     else NONE
   146   end;
   147 
   148 fun filter_intro ctxt goal (_, thm) =
   149   let
   150     val extract_intro = (single o Thm.full_prop_of, Logic.strip_imp_concl);
   151     val concl = Logic.concl_of_goal goal 1;
   152   in
   153     (case is_matching_thm extract_intro ctxt true concl thm of
   154       SOME k => SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm, k)
   155     | NONE => NONE)
   156   end;
   157 
   158 fun filter_elim ctxt goal (_, thm) =
   159   if Thm.nprems_of thm > 0 then
   160     let
   161       val rule = Thm.full_prop_of thm;
   162       val prems = Logic.prems_of_goal goal 1;
   163       val goal_concl = Logic.concl_of_goal goal 1;
   164       val rule_mp = hd (Logic.strip_imp_prems rule);
   165       val rule_concl = Logic.strip_imp_concl rule;
   166       fun combine t1 t2 = Const ("*combine*", dummyT --> dummyT) $ (t1 $ t2);  (* FIXME ?!? *)
   167       val rule_tree = combine rule_mp rule_concl;
   168       fun goal_tree prem = combine prem goal_concl;
   169       fun try_subst prem = is_matching_thm (single, I) ctxt true (goal_tree prem) rule_tree;
   170       val successful = prems |> map_filter try_subst;
   171     in
   172       (*elim rules always have assumptions, so an elim with one
   173         assumption is as good as an intro rule with none*)
   174       if is_nontrivial (Proof_Context.theory_of ctxt) (Thm.major_prem_of thm)
   175           andalso not (null successful) then
   176         SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm - 1, foldl1 Int.min successful)
   177       else NONE
   178     end
   179   else NONE;
   180 
   181 fun filter_solves ctxt goal =
   182   let
   183     val thy' =
   184       Proof_Context.theory_of ctxt
   185       |> Context_Position.set_visible_global (Context_Position.is_visible ctxt);
   186     val ctxt' = Proof_Context.transfer thy' ctxt;
   187     val goal' = Thm.transfer thy' goal;
   188 
   189     fun limited_etac thm i =
   190       Seq.take (Options.default_int @{system_option find_theorems_tactic_limit}) o
   191         eresolve_tac [thm] i;
   192     fun try_thm thm =
   193       if Thm.no_prems thm then resolve_tac [thm] 1 goal'
   194       else
   195         (limited_etac thm THEN_ALL_NEW (Goal.norm_hhf_tac ctxt' THEN' Method.assm_tac ctxt'))
   196           1 goal';
   197   in
   198     fn (_, thm) =>
   199       if is_some (Seq.pull (try_thm thm))
   200       then SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm, 0)
   201       else NONE
   202   end;
   203 
   204 
   205 (* filter_simp *)
   206 
   207 fun filter_simp ctxt t (_, thm) =
   208   let
   209     val mksimps = Simplifier.mksimps ctxt;
   210     val extract_simp =
   211       (map Thm.full_prop_of o mksimps, #1 o Logic.dest_equals o Logic.strip_imp_concl);
   212   in
   213     (case is_matching_thm extract_simp ctxt false t thm of
   214       SOME ss => SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm, ss)
   215     | NONE => NONE)
   216   end;
   217 
   218 
   219 (* filter_pattern *)
   220 
   221 fun expand_abs t =
   222   let
   223     val m = Term.maxidx_of_term t + 1;
   224     val vs = strip_abs_vars t;
   225     val ts = map_index (fn (k, (_, T)) => Var ((Name.aT, m + k), T)) vs;
   226   in betapplys (t, ts) end;
   227 
   228 fun get_names t = Term.add_const_names t (Term.add_free_names t []);
   229 
   230 (* Does pat match a subterm of obj? *)
   231 fun matches_subterm thy (pat, obj) =
   232   let
   233     fun msub bounds obj = Pattern.matches thy (pat, obj) orelse
   234       (case obj of
   235         Abs (_, T, t) => msub (bounds + 1) (snd (Term.dest_abs (Name.bound bounds, T, t)))
   236       | t $ u => msub bounds t orelse msub bounds u
   237       | _ => false)
   238   in msub 0 obj end;
   239 
   240 (*Including all constants and frees is only sound because matching
   241   uses higher-order patterns. If full matching were used, then
   242   constants that may be subject to beta-reduction after substitution
   243   of frees should not be included for LHS set because they could be
   244   thrown away by the substituted function.  E.g. for (?F 1 2) do not
   245   include 1 or 2, if it were possible for ?F to be (%x y. 3).  The
   246   largest possible set should always be included on the RHS.*)
   247 
   248 fun filter_pattern ctxt pat =
   249   let
   250     val pat' = (expand_abs o Envir.eta_contract) pat;
   251     val pat_consts = get_names pat';
   252     fun check ((x, thm), NONE) = check ((x, thm), SOME (get_names (Thm.full_prop_of thm)))
   253       | check ((_, thm), c as SOME thm_consts) =
   254          (if subset (op =) (pat_consts, thm_consts) andalso
   255             matches_subterm (Proof_Context.theory_of ctxt) (pat', Thm.full_prop_of thm)
   256           then SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm, 0) else NONE, c);
   257   in check end;
   258 
   259 
   260 (* interpret criteria as filters *)
   261 
   262 local
   263 
   264 fun err_no_goal c =
   265   error ("Current goal required for " ^ c ^ " search criterion");
   266 
   267 fun filter_crit _ _ (Name name) = apfst (filter_name name)
   268   | filter_crit _ NONE Intro = err_no_goal "intro"
   269   | filter_crit _ NONE Elim = err_no_goal "elim"
   270   | filter_crit _ NONE Dest = err_no_goal "dest"
   271   | filter_crit _ NONE Solves = err_no_goal "solves"
   272   | filter_crit ctxt (SOME goal) Intro = apfst (filter_intro ctxt (Thm.prop_of goal))
   273   | filter_crit ctxt (SOME goal) Elim = apfst (filter_elim ctxt (Thm.prop_of goal))
   274   | filter_crit ctxt (SOME goal) Dest = apfst (filter_dest ctxt (Thm.prop_of goal))
   275   | filter_crit ctxt (SOME goal) Solves = apfst (filter_solves ctxt goal)
   276   | filter_crit ctxt _ (Simp pat) = apfst (filter_simp ctxt pat)
   277   | filter_crit ctxt _ (Pattern pat) = filter_pattern ctxt pat;
   278 
   279 fun opt_not x = if is_some x then NONE else SOME (0, 0, 0);
   280 
   281 fun opt_add (SOME (a, c, x)) (SOME (b, d, y)) = SOME (Int.max (a,b), Int.max (c, d), x + y : int)
   282   | opt_add _ _ = NONE;
   283 
   284 fun app_filters thm =
   285   let
   286     fun app (NONE, _, _) = NONE
   287       | app (SOME v, _, []) = SOME (v, thm)
   288       | app (r, consts, f :: fs) =
   289           let val (r', consts') = f (thm, consts)
   290           in app (opt_add r r', consts', fs) end;
   291   in app end;
   292 
   293 in
   294 
   295 fun filter_criterion ctxt opt_goal (b, c) =
   296   (if b then I else (apfst opt_not)) o filter_crit ctxt opt_goal c;
   297 
   298 fun sorted_filter filters thms =
   299   let
   300     fun eval_filters thm = app_filters thm (SOME (0, 0, 0), NONE, filters);
   301 
   302     (*filters return: (thm size, number of assumptions, substitution size) option, so
   303       sort according to size of thm first, then number of assumptions,
   304       then by the substitution size, then by term order *)
   305     fun result_ord (((p0, s0, t0), (_, thm0)), ((p1, s1, t1), (_, thm1))) =
   306       prod_ord int_ord (prod_ord int_ord (prod_ord int_ord Term_Ord.term_ord))
   307          ((p1, (s1, (t1, Thm.full_prop_of thm1))), (p0, (s0, (t0, Thm.full_prop_of thm0))));
   308   in
   309     grouped 100 Par_List.map eval_filters thms
   310     |> map_filter I |> sort result_ord |> map #2
   311   end;
   312 
   313 fun lazy_filter filters =
   314   let
   315     fun lazy_match thms = Seq.make (fn () => first_match thms)
   316     and first_match [] = NONE
   317       | first_match (thm :: thms) =
   318           (case app_filters thm (SOME (0, 0, 0), NONE, filters) of
   319             NONE => first_match thms
   320           | SOME (_, t) => SOME (t, lazy_match thms));
   321   in lazy_match end;
   322 
   323 end;
   324 
   325 
   326 (* removing duplicates, preferring nicer names, roughly O(n log n) *)
   327 
   328 local
   329 
   330 val index_ord = option_ord (K EQUAL);
   331 val hidden_ord = bool_ord o apply2 Long_Name.is_hidden;
   332 val qual_ord = int_ord o apply2 Long_Name.qualification;
   333 val txt_ord = int_ord o apply2 size;
   334 
   335 fun nicer_name (x, i) (y, j) =
   336   (case hidden_ord (x, y) of EQUAL =>
   337     (case index_ord (i, j) of EQUAL =>
   338       (case qual_ord (x, y) of EQUAL => txt_ord (x, y) | ord => ord)
   339     | ord => ord)
   340   | ord => ord) <> GREATER;
   341 
   342 fun rem_cdups nicer xs =
   343   let
   344     fun rem_c rev_seen [] = rev rev_seen
   345       | rem_c rev_seen [x] = rem_c (x :: rev_seen) []
   346       | rem_c rev_seen ((x as ((n, thm), _)) :: (y as ((n', thm'), _)) :: rest) =
   347           if Thm.eq_thm_prop (thm, thm')
   348           then rem_c rev_seen ((if nicer n n' then x else y) :: rest)
   349           else rem_c (x :: rev_seen) (y :: rest);
   350   in rem_c [] xs end;
   351 
   352 in
   353 
   354 fun nicer_shortest ctxt =
   355   let
   356     fun extern_shortest name =
   357       Name_Space.extern_shortest ctxt
   358         (Facts.space_of (Proof_Context.facts_of_fact ctxt name)) name;
   359 
   360     fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) =
   361           nicer_name (extern_shortest x, i) (extern_shortest y, j)
   362       | nicer (Facts.Fact _) (Facts.Named _) = true
   363       | nicer (Facts.Named _) (Facts.Fact _) = false
   364       | nicer (Facts.Fact _) (Facts.Fact _) = true;
   365   in nicer end;
   366 
   367 fun rem_thm_dups nicer xs =
   368   (xs ~~ (1 upto length xs))
   369   |> sort (Term_Ord.fast_term_ord o apply2 (Thm.full_prop_of o #2 o #1))
   370   |> rem_cdups nicer
   371   |> sort (int_ord o apply2 #2)
   372   |> map #1;
   373 
   374 end;
   375 
   376 
   377 
   378 (** main operations **)
   379 
   380 (* filter_theorems *)
   381 
   382 fun all_facts_of ctxt =
   383   let
   384     val local_facts = Proof_Context.facts_of ctxt;
   385     val global_facts = Global_Theory.facts_of (Proof_Context.theory_of ctxt);
   386   in
   387     maps Facts.selections
   388      (Facts.dest_static false [global_facts] local_facts @
   389       Facts.dest_static false [] global_facts)
   390   end;
   391 
   392 fun filter_theorems ctxt theorems query =
   393   let
   394     val {goal = opt_goal, limit = opt_limit, rem_dups, criteria} = query;
   395     val filters = map (filter_criterion ctxt opt_goal) criteria;
   396 
   397     fun find_all theorems =
   398       let
   399         val raw_matches = sorted_filter filters theorems;
   400 
   401         val matches =
   402           if rem_dups
   403           then rem_thm_dups (nicer_shortest ctxt) raw_matches
   404           else raw_matches;
   405 
   406         val len = length matches;
   407         val lim = the_default (Options.default_int @{system_option find_theorems_limit}) opt_limit;
   408       in (SOME len, drop (Int.max (len - lim, 0)) matches) end;
   409 
   410     val find =
   411       if rem_dups orelse is_none opt_limit
   412       then find_all
   413       else pair NONE o Seq.list_of o Seq.take (the opt_limit) o lazy_filter filters;
   414 
   415   in find theorems end;
   416 
   417 fun filter_theorems_cmd ctxt theorems raw_query =
   418   filter_theorems ctxt theorems (map_criteria (map (apsnd (read_criterion ctxt))) raw_query);
   419 
   420 
   421 (* find_theorems *)
   422 
   423 local
   424 
   425 fun gen_find_theorems filter ctxt opt_goal opt_limit rem_dups raw_criteria =
   426   let
   427     val assms =
   428       Proof_Context.get_fact ctxt (Facts.named "local.assms")
   429         handle ERROR _ => [];
   430     val add_prems = Seq.hd o TRY (Method.insert_tac assms 1);
   431     val opt_goal' = Option.map add_prems opt_goal;
   432   in
   433     filter ctxt (all_facts_of ctxt)
   434       {goal = opt_goal', limit = opt_limit, rem_dups = rem_dups, criteria = raw_criteria}
   435   end;
   436 
   437 in
   438 
   439 val find_theorems = gen_find_theorems filter_theorems;
   440 val find_theorems_cmd = gen_find_theorems filter_theorems_cmd;
   441 
   442 end;
   443 
   444 
   445 (* pretty_theorems *)
   446 
   447 local
   448 
   449 fun pretty_ref ctxt thmref =
   450   let
   451     val (name, sel) =
   452       (case thmref of
   453         Facts.Named ((name, _), sel) => (name, sel)
   454       | Facts.Fact _ => raise Fail "Illegal literal fact");
   455   in
   456     [Pretty.mark (#1 (Proof_Context.markup_extern_fact ctxt name)) (Pretty.str name),
   457       Pretty.str (Facts.string_of_selection sel), Pretty.str ":", Pretty.brk 1]
   458   end;
   459 
   460 in
   461 
   462 fun pretty_thm ctxt (thmref, thm) =
   463   Pretty.block (pretty_ref ctxt thmref @ [Display.pretty_thm ctxt thm]);
   464 
   465 fun pretty_theorems state opt_limit rem_dups raw_criteria =
   466   let
   467     val ctxt = Proof.context_of state;
   468     val opt_goal = try Proof.simple_goal state |> Option.map #goal;
   469     val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
   470 
   471     val (opt_found, theorems) =
   472       filter_theorems ctxt (all_facts_of ctxt)
   473         {goal = opt_goal, limit = opt_limit, rem_dups = rem_dups, criteria = criteria};
   474     val returned = length theorems;
   475 
   476     val tally_msg =
   477       (case opt_found of
   478         NONE => "displaying " ^ string_of_int returned ^ " theorem(s)"
   479       | SOME found =>
   480           "found " ^ string_of_int found ^ " theorem(s)" ^
   481             (if returned < found
   482              then " (" ^ string_of_int returned ^ " displayed)"
   483              else ""));
   484     val position_markup = Position.markup (Position.thread_data ()) Markup.position;
   485   in
   486     Pretty.block
   487       (Pretty.fbreaks
   488         (Pretty.mark position_markup (Pretty.keyword1 "find_theorems") ::
   489           map (pretty_criterion ctxt) criteria)) ::
   490     Pretty.str "" ::
   491     (if null theorems then [Pretty.str "found nothing"]
   492      else
   493        Pretty.str (tally_msg ^ ":") ::
   494        grouped 10 Par_List.map (Pretty.item o single o pretty_thm ctxt) (rev theorems))
   495   end |> Pretty.fbreaks |> curry Pretty.blk 0;
   496 
   497 end;
   498 
   499 
   500 
   501 (** Isar command syntax **)
   502 
   503 fun proof_state st =
   504   (case try Toplevel.proof_of st of
   505     SOME state => state
   506   | NONE => Proof.init (Toplevel.context_of st));
   507 
   508 local
   509 
   510 val criterion =
   511   Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name ||
   512   Parse.reserved "intro" >> K Intro ||
   513   Parse.reserved "elim" >> K Elim ||
   514   Parse.reserved "dest" >> K Dest ||
   515   Parse.reserved "solves" >> K Solves ||
   516   Parse.reserved "simp" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.term) >> Simp ||
   517   Parse.term >> Pattern;
   518 
   519 val options =
   520   Scan.optional
   521     (Parse.$$$ "(" |--
   522       Parse.!!! (Scan.option Parse.nat -- Scan.optional (Parse.reserved "with_dups" >> K false) true
   523         --| Parse.$$$ ")")) (NONE, true);
   524 
   525 val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);
   526 
   527 val query_keywords = Keyword.add_keywords [(":", NONE)] Keyword.empty_keywords;
   528 
   529 in
   530 
   531 fun read_query pos str =
   532   Token.explode query_keywords pos str
   533   |> filter Token.is_proper
   534   |> Scan.error (Scan.finite Token.stopper (Parse.!!! (query --| Scan.ahead Parse.eof)))
   535   |> #1;
   536 
   537 val _ =
   538   Outer_Syntax.command @{command_spec "find_theorems"}
   539     "find theorems meeting specified criteria"
   540     (options -- query >> (fn ((opt_lim, rem_dups), spec) =>
   541       Toplevel.keep (fn st =>
   542         Pretty.writeln (pretty_theorems (proof_state st) opt_lim rem_dups spec))));
   543 
   544 end;
   545 
   546 
   547 
   548 (** PIDE query operation **)
   549 
   550 val _ =
   551   Query_Operation.register "find_theorems" (fn {state = st, args, output_result} =>
   552     if can Toplevel.context_of st then
   553       let
   554         val [limit_arg, allow_dups_arg, query_arg] = args;
   555         val state = proof_state st;
   556         val opt_limit = Int.fromString limit_arg;
   557         val rem_dups = allow_dups_arg = "false";
   558         val criteria = read_query Position.none query_arg;
   559       in output_result (Pretty.string_of (pretty_theorems state opt_limit rem_dups criteria)) end
   560     else error "Unknown context");
   561 
   562 end;
   563