some actual find_theorems functionality;
authorwenzelm
Fri Aug 02 22:46:54 2013 +0200 (2013-08-02)
changeset 52855fb1f026c48ff
parent 52854 92932931bd82
child 52856 46c339daaff2
some actual find_theorems functionality;
src/Pure/Tools/find_theorems.ML
src/Tools/WWW_Find/find_theorems.ML
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Fri Aug 02 22:17:53 2013 +0200
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Fri Aug 02 22:46:54 2013 +0200
     1.3 @@ -21,7 +21,7 @@
     1.4    }
     1.5  
     1.6    val read_criterion: Proof.context -> string criterion -> term criterion
     1.7 -  val query_parser: (bool * string criterion) list parser
     1.8 +  val parse_query: string -> (bool * string criterion) list
     1.9  
    1.10    val xml_of_query: term query -> XML.tree
    1.11    val query_of_xml: XML.tree -> term query
    1.12 @@ -496,7 +496,7 @@
    1.13  end;
    1.14  
    1.15  
    1.16 -(* print_theorems *)
    1.17 +(* pretty_theorems *)
    1.18  
    1.19  fun all_facts_of ctxt =
    1.20    let
    1.21 @@ -572,11 +572,12 @@
    1.22  
    1.23  fun pretty_thm ctxt (thmref, thm) = pretty_theorem ctxt (Internal (thmref, thm));
    1.24  
    1.25 -fun gen_print_theorems find ctxt opt_goal opt_limit rem_dups raw_criteria =
    1.26 +fun pretty_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
    1.27    let
    1.28      val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
    1.29 -    val (foundo, theorems) = find
    1.30 -      {goal = opt_goal, limit = opt_limit, rem_dups = rem_dups, criteria = criteria};
    1.31 +    val (foundo, theorems) =
    1.32 +      filter_theorems ctxt (map Internal (all_facts_of ctxt))
    1.33 +        {goal = opt_goal, limit = opt_limit, rem_dups = rem_dups, criteria = criteria};
    1.34      val returned = length theorems;
    1.35  
    1.36      val tally_msg =
    1.37 @@ -594,10 +595,13 @@
    1.38       else
    1.39        [Pretty.str (tally_msg ^ ":"), Pretty.str ""] @
    1.40          grouped 10 Par_List.map (pretty_theorem ctxt) theorems)
    1.41 -  end |> Pretty.fbreaks |> curry Pretty.blk 0 |> Pretty.writeln;
    1.42 +  end |> Pretty.fbreaks |> curry Pretty.blk 0;
    1.43  
    1.44 -fun print_theorems ctxt =
    1.45 -  gen_print_theorems (filter_theorems ctxt (map Internal (all_facts_of ctxt))) ctxt;
    1.46 +fun pretty_theorems_cmd state opt_lim rem_dups spec =
    1.47 +  let
    1.48 +    val ctxt = Toplevel.context_of state;
    1.49 +    val opt_goal = try (Proof.simple_goal o Toplevel.proof_of) state |> Option.map #goal;
    1.50 +  in pretty_theorems ctxt opt_goal opt_lim rem_dups spec end;
    1.51  
    1.52  
    1.53  
    1.54 @@ -619,20 +623,25 @@
    1.55      (Parse.$$$ "(" |--
    1.56        Parse.!!! (Scan.option Parse.nat -- Scan.optional (Parse.reserved "with_dups" >> K false) true
    1.57          --| Parse.$$$ ")")) (NONE, true);
    1.58 +
    1.59 +val query_parser = Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion));
    1.60 +
    1.61  in
    1.62  
    1.63 -val query_parser = Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion));
    1.64 +(* FIXME proper wrapper for parser combinator *)
    1.65 +fun parse_query str =
    1.66 +  (str ^ ";")
    1.67 +  |> Outer_Syntax.scan Position.start
    1.68 +  |> filter Token.is_proper
    1.69 +  |> Scan.error query_parser
    1.70 +  |> fst;
    1.71  
    1.72  val _ =
    1.73    Outer_Syntax.improper_command @{command_spec "find_theorems"}
    1.74      "find theorems meeting specified criteria"
    1.75 -    (options -- query_parser
    1.76 -      >> (fn ((opt_lim, rem_dups), spec) =>
    1.77 -        Toplevel.keep (fn state =>
    1.78 -          let
    1.79 -            val ctxt = Toplevel.context_of state;
    1.80 -            val opt_goal = try (Proof.simple_goal o Toplevel.proof_of) state |> Option.map #goal;
    1.81 -          in print_theorems ctxt opt_goal opt_lim rem_dups spec end)));
    1.82 +    (options -- query_parser >> (fn ((opt_lim, rem_dups), spec) =>
    1.83 +      Toplevel.keep (fn state =>
    1.84 +        Pretty.writeln (pretty_theorems_cmd state opt_lim rem_dups spec))));
    1.85  
    1.86  end;
    1.87  
    1.88 @@ -647,8 +656,14 @@
    1.89      (case args of
    1.90        [instance, query] =>
    1.91        SOME {delay = NONE, pri = 0, persistent = false,
    1.92 -        print_fn = fn _ => fn st =>
    1.93 -          Output.result [(Markup.kindN, find_theoremsN), (Markup.instanceN, instance)] query}
    1.94 +        print_fn = fn _ => fn state =>
    1.95 +          let
    1.96 +            val msg =
    1.97 +              Pretty.string_of (pretty_theorems_cmd state NONE false (parse_query query))
    1.98 +                handle exn =>
    1.99 +                  if Exn.is_interrupt exn then reraise exn
   1.100 +                  else ML_Compiler.exn_message exn;  (* FIXME error markup!? *)
   1.101 +          in Output.result [(Markup.kindN, find_theoremsN), (Markup.instanceN, instance)] msg end}
   1.102      | _ => NONE));
   1.103  
   1.104  end;
     2.1 --- a/src/Tools/WWW_Find/find_theorems.ML	Fri Aug 02 22:17:53 2013 +0200
     2.2 +++ b/src/Tools/WWW_Find/find_theorems.ML	Fri Aug 02 22:46:54 2013 +0200
     2.3 @@ -16,12 +16,7 @@
     2.4      val args = Symtab.lookup arg_data;
     2.5  
     2.6      val query_str = the_default "" (args "query");
     2.7 -    fun get_query () =
     2.8 -      (query_str ^ ";")
     2.9 -      |> Outer_Syntax.scan Position.start
    2.10 -      |> filter Token.is_proper
    2.11 -      |> Scan.error Find_Theorems.query_parser
    2.12 -      |> fst;
    2.13 +    fun get_query () = Find_Theorems.parse_query query_str;
    2.14  
    2.15      val limit = case args "limit" of
    2.16          NONE => default_limit