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