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