src/Pure/Tools/find_theorems.ML
changeset 43071 c9859f634cef
parent 43070 0318781be055
child 43076 7b06cd71792c
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Mon May 30 17:07:48 2011 +0200
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Mon May 30 17:07:48 2011 +0200
     1.3 @@ -26,6 +26,11 @@
     1.4    val read_criterion: Proof.context -> string criterion -> term criterion
     1.5    val query_parser: (bool * string criterion) list parser
     1.6  
     1.7 +  val xml_of_query: term query -> XML.tree
     1.8 +  val query_of_xml: XML.tree -> term query
     1.9 +  val xml_of_result: int option * theorem list -> XML.tree
    1.10 +  val result_of_xml: XML.tree -> int option * theorem list
    1.11 +
    1.12    val find_theorems: Proof.context -> thm option -> int option -> bool ->
    1.13      (bool * term criterion) list -> int option * (Facts.ref * thm) list
    1.14    val find_theorems_cmd: Proof.context -> thm option -> int option -> bool ->
    1.15 @@ -108,12 +113,86 @@
    1.16  fun map_criteria f {goal, limit, rem_dups, criteria} =
    1.17    {goal=goal, limit=limit, rem_dups=rem_dups, criteria=f criteria};
    1.18  
    1.19 +fun xml_of_criterion (Name name) = XML.Elem (("Name", [("val", name)]), [])
    1.20 +  | xml_of_criterion Intro = XML.Elem (("Intro", []) , [])
    1.21 +  | xml_of_criterion IntroIff = XML.Elem (("IntroIff", []) , [])
    1.22 +  | xml_of_criterion Elim = XML.Elem (("Elim", []) , [])
    1.23 +  | xml_of_criterion Dest = XML.Elem (("Dest", []) , [])
    1.24 +  | xml_of_criterion Solves = XML.Elem (("Solves", []) , [])
    1.25 +  | xml_of_criterion (Simp pat) = XML.Elem (("Simp", []) , [XML_Syntax.xml_of_term pat])
    1.26 +  | xml_of_criterion (Pattern pat) = XML.Elem (("Pattern", []) , [XML_Syntax.xml_of_term pat]);
    1.27 +
    1.28 +fun criterion_of_xml (XML.Elem (("Name", [("val", name)]), [])) = Name name
    1.29 +  | criterion_of_xml (XML.Elem (("Intro", []) , [])) = Intro
    1.30 +  | criterion_of_xml (XML.Elem (("IntroIff", []) , [])) = IntroIff
    1.31 +  | criterion_of_xml (XML.Elem (("Elim", []) , [])) = Elim
    1.32 +  | criterion_of_xml (XML.Elem (("Dest", []) , [])) = Dest
    1.33 +  | criterion_of_xml (XML.Elem (("Solves", []) , [])) = Solves
    1.34 +  | criterion_of_xml (XML.Elem (("Simp", []) , [tree])) = Simp (XML_Syntax.term_of_xml tree)
    1.35 +  | criterion_of_xml (XML.Elem (("Pattern", []) , [tree])) = Pattern (XML_Syntax.term_of_xml tree)
    1.36 +  | criterion_of_xml tree = raise XML_Syntax.XML ("criterion_of_xml: bad tree", tree);
    1.37 +
    1.38 +fun xml_of_query {goal=NONE, limit, rem_dups, criteria} =
    1.39 +      let
    1.40 +        val properties = []
    1.41 +          |> (if rem_dups then cons ("rem_dups", "") else I)
    1.42 +          |> (if is_some limit then cons ("limit", Markup.print_int (the limit)) else I);
    1.43 +      in
    1.44 +        XML.Elem (("Query", properties), XML_Data.make_list 
    1.45 +          (XML_Data.make_pair XML_Data.make_bool (single o xml_of_criterion)) criteria)
    1.46 +      end
    1.47 +  | xml_of_query _ = raise Fail "cannot serialize goal";
    1.48 +
    1.49 +fun query_of_xml (XML.Elem (("Query", properties), body)) =
    1.50 +      let
    1.51 +        val rem_dups = Properties.defined properties "rem_dups";
    1.52 +        val limit = Properties.get properties "limit" |> Option.map Markup.parse_int;
    1.53 +        val criteria = XML_Data.dest_list (XML_Data.dest_pair XML_Data.dest_bool 
    1.54 +          (criterion_of_xml o the_single)) body;
    1.55 +      in
    1.56 +        {goal=NONE, limit=limit, rem_dups=rem_dups, criteria=criteria}
    1.57 +      end
    1.58 +  | query_of_xml tree = raise XML_Syntax.XML ("query_of_xml: bad tree", tree);
    1.59  
    1.60  (** theorems, either internal or external (without proof) **)
    1.61  
    1.62  datatype theorem =
    1.63    Internal of Facts.ref * thm |
    1.64 -  External of Facts.ref * term;
    1.65 +  External of Facts.ref * term; (* FIXME: Facts.ref not appropriate *)
    1.66 +
    1.67 +fun fact_ref_markup (Facts.Named ((name, pos), SOME [Facts.Single i])) =
    1.68 +      Position.markup pos o Markup.properties [("name", name), ("index", Markup.print_int i)]
    1.69 +  | fact_ref_markup (Facts.Named ((name, pos), NONE)) =
    1.70 +      Position.markup pos o Markup.properties [("name", name)]
    1.71 +  | fact_ref_markup fact_ref = raise Fail "bad fact ref"
    1.72 +
    1.73 +fun xml_of_theorem (Internal _) = raise Fail "xml_of_theorem: Internal"
    1.74 +  | xml_of_theorem (External (fact_ref, prop)) =
    1.75 +      XML.Elem (fact_ref_markup fact_ref ("External", []), [XML_Syntax.xml_of_term prop])
    1.76 +
    1.77 +fun theorem_of_xml (XML.Elem (("External", properties), [tree])) =
    1.78 +    let
    1.79 +      val name = the (Properties.get properties "name");
    1.80 +      val pos = Position.of_properties properties;
    1.81 +      val intvs_opt = Option.map (single o Facts.Single o Markup.parse_int)
    1.82 +        (Properties.get properties "index");
    1.83 +    in
    1.84 +      External (Facts.Named ((name, pos), intvs_opt), XML_Syntax.term_of_xml tree)
    1.85 +    end
    1.86 +  | theorem_of_xml tree = raise XML_Syntax.XML ("theorem_of_xml: bad tree", tree);
    1.87 +
    1.88 +fun xml_of_result (opt_found, theorems) =
    1.89 +  let
    1.90 +    val properties =
    1.91 +      if is_some opt_found then [("found", Markup.print_int (the opt_found))] else [];
    1.92 +  in
    1.93 +    XML.Elem (("Result", properties), XML_Data.make_list (single o xml_of_theorem) theorems)
    1.94 +  end;
    1.95 +
    1.96 +fun result_of_xml (XML.Elem (("Result", properties), body)) =
    1.97 +      (Properties.get properties "found" |> Option.map Markup.parse_int,
    1.98 +       XML_Data.dest_list (theorem_of_xml o the_single) body)
    1.99 +  | result_of_xml tree = raise XML_Syntax.XML ("result_of_xml: bad tree", tree);
   1.100  
   1.101  fun prop_of (Internal (_, thm)) = Thm.full_prop_of thm
   1.102    | prop_of (External (_, prop)) = prop;