clarified status of Legacy_XML_Syntax, despite lack of Proofterm_XML;
authorwenzelm
Mon Nov 26 16:28:22 2012 +0100 (2012-11-26)
changeset 50217ce1f0602f48e
parent 50216 de77cde57376
child 50231 81a067b188b8
clarified status of Legacy_XML_Syntax, despite lack of Proofterm_XML;
src/Pure/ROOT
src/Pure/ROOT.ML
src/Pure/Tools/find_theorems.ML
src/Pure/Tools/legacy_xml_syntax.ML
src/Pure/Tools/xml_syntax.ML
     1.1 --- a/src/Pure/ROOT	Mon Nov 26 16:22:29 2012 +0100
     1.2 +++ b/src/Pure/ROOT	Mon Nov 26 16:28:22 2012 +0100
     1.3 @@ -200,7 +200,7 @@
     1.4      "Thy/thy_output.ML"
     1.5      "Thy/thy_syntax.ML"
     1.6      "Tools/named_thms.ML"
     1.7 -    "Tools/xml_syntax.ML"
     1.8 +    "Tools/legacy_xml_syntax.ML"
     1.9      "assumption.ML"
    1.10      "axclass.ML"
    1.11      "config.ML"
     2.1 --- a/src/Pure/ROOT.ML	Mon Nov 26 16:22:29 2012 +0100
     2.2 +++ b/src/Pure/ROOT.ML	Mon Nov 26 16:28:22 2012 +0100
     2.3 @@ -283,7 +283,7 @@
     2.4  
     2.5  use "Tools/named_thms.ML";
     2.6  
     2.7 -use "Tools/xml_syntax.ML";
     2.8 +use "Tools/legacy_xml_syntax.ML";
     2.9  
    2.10  
    2.11  (* configuration for Proof General *)
     3.1 --- a/src/Pure/Tools/find_theorems.ML	Mon Nov 26 16:22:29 2012 +0100
     3.2 +++ b/src/Pure/Tools/find_theorems.ML	Mon Nov 26 16:28:22 2012 +0100
     3.3 @@ -116,17 +116,17 @@
     3.4    | xml_of_criterion Elim = XML.Elem (("Elim", []) , [])
     3.5    | xml_of_criterion Dest = XML.Elem (("Dest", []) , [])
     3.6    | xml_of_criterion Solves = XML.Elem (("Solves", []) , [])
     3.7 -  | xml_of_criterion (Simp pat) = XML.Elem (("Simp", []) , [XML_Syntax.xml_of_term pat])
     3.8 -  | xml_of_criterion (Pattern pat) = XML.Elem (("Pattern", []) , [XML_Syntax.xml_of_term pat]);
     3.9 +  | xml_of_criterion (Simp pat) = XML.Elem (("Simp", []), [Legacy_XML_Syntax.xml_of_term pat])
    3.10 +  | xml_of_criterion (Pattern pat) = XML.Elem (("Pattern", []), [Legacy_XML_Syntax.xml_of_term pat]);
    3.11  
    3.12  fun criterion_of_xml (XML.Elem (("Name", [("val", name)]), [])) = Name name
    3.13    | criterion_of_xml (XML.Elem (("Intro", []) , [])) = Intro
    3.14    | criterion_of_xml (XML.Elem (("Elim", []) , [])) = Elim
    3.15    | criterion_of_xml (XML.Elem (("Dest", []) , [])) = Dest
    3.16    | criterion_of_xml (XML.Elem (("Solves", []) , [])) = Solves
    3.17 -  | criterion_of_xml (XML.Elem (("Simp", []) , [tree])) = Simp (XML_Syntax.term_of_xml tree)
    3.18 -  | criterion_of_xml (XML.Elem (("Pattern", []) , [tree])) = Pattern (XML_Syntax.term_of_xml tree)
    3.19 -  | criterion_of_xml tree = raise XML_Syntax.XML ("criterion_of_xml: bad tree", tree);
    3.20 +  | criterion_of_xml (XML.Elem (("Simp", []), [tree])) = Simp (Legacy_XML_Syntax.term_of_xml tree)
    3.21 +  | criterion_of_xml (XML.Elem (("Pattern", []), [tree])) = Pattern (Legacy_XML_Syntax.term_of_xml tree)
    3.22 +  | criterion_of_xml tree = raise Legacy_XML_Syntax.XML ("criterion_of_xml: bad tree", tree);
    3.23  
    3.24  fun xml_of_query {goal = NONE, limit, rem_dups, criteria} =
    3.25        let
    3.26 @@ -149,7 +149,7 @@
    3.27        in
    3.28          {goal = NONE, limit = limit, rem_dups = rem_dups, criteria = criteria}
    3.29        end
    3.30 -  | query_of_xml tree = raise XML_Syntax.XML ("query_of_xml: bad tree", tree);
    3.31 +  | query_of_xml tree = raise Legacy_XML_Syntax.XML ("query_of_xml: bad tree", tree);
    3.32  
    3.33  
    3.34  
    3.35 @@ -167,7 +167,7 @@
    3.36  
    3.37  fun xml_of_theorem (Internal _) = raise Fail "xml_of_theorem: Internal"
    3.38    | xml_of_theorem (External (fact_ref, prop)) =
    3.39 -      XML.Elem (fact_ref_markup fact_ref ("External", []), [XML_Syntax.xml_of_term prop]);
    3.40 +      XML.Elem (fact_ref_markup fact_ref ("External", []), [Legacy_XML_Syntax.xml_of_term prop]);
    3.41  
    3.42  fun theorem_of_xml (XML.Elem (("External", properties), [tree])) =
    3.43        let
    3.44 @@ -177,9 +177,9 @@
    3.45            Option.map (single o Facts.Single o Markup.parse_int)
    3.46              (Properties.get properties "index");
    3.47        in
    3.48 -        External (Facts.Named ((name, pos), intvs_opt), XML_Syntax.term_of_xml tree)
    3.49 +        External (Facts.Named ((name, pos), intvs_opt), Legacy_XML_Syntax.term_of_xml tree)
    3.50        end
    3.51 -  | theorem_of_xml tree = raise XML_Syntax.XML ("theorem_of_xml: bad tree", tree);
    3.52 +  | theorem_of_xml tree = raise Legacy_XML_Syntax.XML ("theorem_of_xml: bad tree", tree);
    3.53  
    3.54  fun xml_of_result (opt_found, theorems) =
    3.55    let
    3.56 @@ -192,7 +192,7 @@
    3.57  fun result_of_xml (XML.Elem (("Result", properties), body)) =
    3.58        (Properties.get properties "found" |> Option.map Markup.parse_int,
    3.59         XML.Decode.list (theorem_of_xml o the_single) body)
    3.60 -  | result_of_xml tree = raise XML_Syntax.XML ("result_of_xml: bad tree", tree);
    3.61 +  | result_of_xml tree = raise Legacy_XML_Syntax.XML ("result_of_xml: bad tree", tree);
    3.62  
    3.63  fun prop_of (Internal (_, thm)) = Thm.full_prop_of thm
    3.64    | prop_of (External (_, prop)) = prop;
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Pure/Tools/legacy_xml_syntax.ML	Mon Nov 26 16:28:22 2012 +0100
     4.3 @@ -0,0 +1,173 @@
     4.4 +(*  Title:      Pure/Tools/legacy_xml_syntax.ML
     4.5 +    Author:     Stefan Berghofer, TU Muenchen
     4.6 +
     4.7 +Input and output of types, terms, and proofs in XML format.
     4.8 +See isabelle.xsd for a description of the syntax.
     4.9 +
    4.10 +Legacy module, see Pure/term_xml.ML etc.
    4.11 +*)
    4.12 +
    4.13 +signature LEGACY_XML_SYNTAX =
    4.14 +sig
    4.15 +  val xml_of_type: typ -> XML.tree
    4.16 +  val xml_of_term: term -> XML.tree
    4.17 +  val xml_of_proof: Proofterm.proof -> XML.tree
    4.18 +  val write_to_file: Path.T -> string -> XML.tree -> unit
    4.19 +  exception XML of string * XML.tree
    4.20 +  val type_of_xml: XML.tree -> typ
    4.21 +  val term_of_xml: XML.tree -> term
    4.22 +  val proof_of_xml: XML.tree -> Proofterm.proof
    4.23 +end;
    4.24 +
    4.25 +structure Legacy_XML_Syntax : LEGACY_XML_SYNTAX =
    4.26 +struct
    4.27 +
    4.28 +(**** XML output ****)
    4.29 +
    4.30 +fun xml_of_class name = XML.Elem (("class", [("name", name)]), []);
    4.31 +
    4.32 +fun xml_of_type (TVar ((s, i), S)) =
    4.33 +      XML.Elem (("TVar", ("name", s) :: (if i=0 then [] else [("index", string_of_int i)])),
    4.34 +        map xml_of_class S)
    4.35 +  | xml_of_type (TFree (s, S)) =
    4.36 +      XML.Elem (("TFree", [("name", s)]), map xml_of_class S)
    4.37 +  | xml_of_type (Type (s, Ts)) =
    4.38 +      XML.Elem (("Type", [("name", s)]), map xml_of_type Ts);
    4.39 +
    4.40 +fun xml_of_term (Bound i) =
    4.41 +      XML.Elem (("Bound", [("index", string_of_int i)]), [])
    4.42 +  | xml_of_term (Free (s, T)) =
    4.43 +      XML.Elem (("Free", [("name", s)]), [xml_of_type T])
    4.44 +  | xml_of_term (Var ((s, i), T)) =
    4.45 +      XML.Elem (("Var", ("name", s) :: (if i=0 then [] else [("index", string_of_int i)])),
    4.46 +        [xml_of_type T])
    4.47 +  | xml_of_term (Const (s, T)) =
    4.48 +      XML.Elem (("Const", [("name", s)]), [xml_of_type T])
    4.49 +  | xml_of_term (t $ u) =
    4.50 +      XML.Elem (("App", []), [xml_of_term t, xml_of_term u])
    4.51 +  | xml_of_term (Abs (s, T, t)) =
    4.52 +      XML.Elem (("Abs", [("vname", s)]), [xml_of_type T, xml_of_term t]);
    4.53 +
    4.54 +fun xml_of_opttypes NONE = []
    4.55 +  | xml_of_opttypes (SOME Ts) = [XML.Elem (("types", []), map xml_of_type Ts)];
    4.56 +
    4.57 +(* FIXME: the t argument of PThm and PAxm is actually redundant, since *)
    4.58 +(* it can be looked up in the theorem database. Thus, it could be      *)
    4.59 +(* omitted from the xml representation.                                *)
    4.60 +
    4.61 +(* FIXME not exhaustive *)
    4.62 +fun xml_of_proof (PBound i) =
    4.63 +      XML.Elem (("PBound", [("index", string_of_int i)]), [])
    4.64 +  | xml_of_proof (Abst (s, optT, prf)) =
    4.65 +      XML.Elem (("Abst", [("vname", s)]),
    4.66 +        (case optT of NONE => [] | SOME T => [xml_of_type T]) @ [xml_of_proof prf])
    4.67 +  | xml_of_proof (AbsP (s, optt, prf)) =
    4.68 +      XML.Elem (("AbsP", [("vname", s)]),
    4.69 +        (case optt of NONE => [] | SOME t => [xml_of_term t]) @ [xml_of_proof prf])
    4.70 +  | xml_of_proof (prf % optt) =
    4.71 +      XML.Elem (("Appt", []),
    4.72 +        xml_of_proof prf :: (case optt of NONE => [] | SOME t => [xml_of_term t]))
    4.73 +  | xml_of_proof (prf %% prf') =
    4.74 +      XML.Elem (("AppP", []), [xml_of_proof prf, xml_of_proof prf'])
    4.75 +  | xml_of_proof (Hyp t) = XML.Elem (("Hyp", []), [xml_of_term t])
    4.76 +  | xml_of_proof (PThm (_, ((s, t, optTs), _))) =
    4.77 +      XML.Elem (("PThm", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs)
    4.78 +  | xml_of_proof (PAxm (s, t, optTs)) =
    4.79 +      XML.Elem (("PAxm", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs)
    4.80 +  | xml_of_proof (Oracle (s, t, optTs)) =
    4.81 +      XML.Elem (("Oracle", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs)
    4.82 +  | xml_of_proof MinProof =
    4.83 +      XML.Elem (("MinProof", []), []);
    4.84 +
    4.85 +
    4.86 +(* useful for checking the output against a schema file *)
    4.87 +
    4.88 +fun write_to_file path elname x =
    4.89 +  File.write path
    4.90 +    ("<?xml version=\"1.0\" encoding=\"UTF-8\"?>\n" ^
    4.91 +     XML.string_of (XML.Elem ((elname,
    4.92 +         [("xmlns:xsi", "http://www.w3.org/2001/XMLSchema-instance"),
    4.93 +          ("xsi:noNamespaceSchemaLocation", "isabelle.xsd")]),
    4.94 +       [x])));
    4.95 +
    4.96 +
    4.97 +
    4.98 +(**** XML input ****)
    4.99 +
   4.100 +exception XML of string * XML.tree;
   4.101 +
   4.102 +fun class_of_xml (XML.Elem (("class", [("name", name)]), [])) = name
   4.103 +  | class_of_xml tree = raise XML ("class_of_xml: bad tree", tree);
   4.104 +
   4.105 +fun index_of_string s tree idx =
   4.106 +  (case Int.fromString idx of
   4.107 +    NONE => raise XML (s ^ ": bad index", tree)
   4.108 +  | SOME i => i);
   4.109 +
   4.110 +fun type_of_xml (tree as XML.Elem (("TVar", atts), classes)) = TVar
   4.111 +      ((case Properties.get atts "name" of
   4.112 +          NONE => raise XML ("type_of_xml: name of TVar missing", tree)
   4.113 +        | SOME name => name,
   4.114 +        the_default 0 (Option.map (index_of_string "type_of_xml" tree)
   4.115 +          (Properties.get atts "index"))),
   4.116 +       map class_of_xml classes)
   4.117 +  | type_of_xml (XML.Elem (("TFree", [("name", s)]), classes)) =
   4.118 +      TFree (s, map class_of_xml classes)
   4.119 +  | type_of_xml (XML.Elem (("Type", [("name", s)]), types)) =
   4.120 +      Type (s, map type_of_xml types)
   4.121 +  | type_of_xml tree = raise XML ("type_of_xml: bad tree", tree);
   4.122 +
   4.123 +fun term_of_xml (tree as XML.Elem (("Bound", [("index", idx)]), [])) =
   4.124 +      Bound (index_of_string "bad variable index" tree idx)
   4.125 +  | term_of_xml (XML.Elem (("Free", [("name", s)]), [typ])) =
   4.126 +      Free (s, type_of_xml typ)
   4.127 +  | term_of_xml (tree as XML.Elem (("Var", atts), [typ])) = Var
   4.128 +      ((case Properties.get atts "name" of
   4.129 +          NONE => raise XML ("type_of_xml: name of Var missing", tree)
   4.130 +        | SOME name => name,
   4.131 +        the_default 0 (Option.map (index_of_string "term_of_xml" tree)
   4.132 +          (Properties.get atts "index"))),
   4.133 +       type_of_xml typ)
   4.134 +  | term_of_xml (XML.Elem (("Const", [("name", s)]), [typ])) =
   4.135 +      Const (s, type_of_xml typ)
   4.136 +  | term_of_xml (XML.Elem (("App", []), [term, term'])) =
   4.137 +      term_of_xml term $ term_of_xml term'
   4.138 +  | term_of_xml (XML.Elem (("Abs", [("vname", s)]), [typ, term])) =
   4.139 +      Abs (s, type_of_xml typ, term_of_xml term)
   4.140 +  | term_of_xml tree = raise XML ("term_of_xml: bad tree", tree);
   4.141 +
   4.142 +fun opttypes_of_xml [] = NONE
   4.143 +  | opttypes_of_xml [XML.Elem (("types", []), types)] =
   4.144 +      SOME (map type_of_xml types)
   4.145 +  | opttypes_of_xml (tree :: _) = raise XML ("opttypes_of_xml: bad tree", tree);
   4.146 +
   4.147 +fun proof_of_xml (tree as XML.Elem (("PBound", [("index", idx)]), [])) =
   4.148 +      PBound (index_of_string "proof_of_xml" tree idx)
   4.149 +  | proof_of_xml (XML.Elem (("Abst", [("vname", s)]), [proof])) =
   4.150 +      Abst (s, NONE, proof_of_xml proof)
   4.151 +  | proof_of_xml (XML.Elem (("Abst", [("vname", s)]), [typ, proof])) =
   4.152 +      Abst (s, SOME (type_of_xml typ), proof_of_xml proof)
   4.153 +  | proof_of_xml (XML.Elem (("AbsP", [("vname", s)]), [proof])) =
   4.154 +      AbsP (s, NONE, proof_of_xml proof)
   4.155 +  | proof_of_xml (XML.Elem (("AbsP", [("vname", s)]), [term, proof])) =
   4.156 +      AbsP (s, SOME (term_of_xml term), proof_of_xml proof)
   4.157 +  | proof_of_xml (XML.Elem (("Appt", []), [proof])) =
   4.158 +      proof_of_xml proof % NONE
   4.159 +  | proof_of_xml (XML.Elem (("Appt", []), [proof, term])) =
   4.160 +      proof_of_xml proof % SOME (term_of_xml term)
   4.161 +  | proof_of_xml (XML.Elem (("AppP", []), [proof, proof'])) =
   4.162 +      proof_of_xml proof %% proof_of_xml proof'
   4.163 +  | proof_of_xml (XML.Elem (("Hyp", []), [term])) =
   4.164 +      Hyp (term_of_xml term)
   4.165 +  | proof_of_xml (XML.Elem (("PThm", [("name", s)]), term :: opttypes)) =
   4.166 +      (* FIXME? *)
   4.167 +      PThm (serial (), ((s, term_of_xml term, opttypes_of_xml opttypes),
   4.168 +        Future.value (Proofterm.approximate_proof_body MinProof)))
   4.169 +  | proof_of_xml (XML.Elem (("PAxm", [("name", s)]), term :: opttypes)) =
   4.170 +      PAxm (s, term_of_xml term, opttypes_of_xml opttypes)
   4.171 +  | proof_of_xml (XML.Elem (("Oracle", [("name", s)]), term :: opttypes)) =
   4.172 +      Oracle (s, term_of_xml term, opttypes_of_xml opttypes)
   4.173 +  | proof_of_xml (XML.Elem (("MinProof", _), _)) = MinProof
   4.174 +  | proof_of_xml tree = raise XML ("proof_of_xml: bad tree", tree);
   4.175 +
   4.176 +end;
     5.1 --- a/src/Pure/Tools/xml_syntax.ML	Mon Nov 26 16:22:29 2012 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,171 +0,0 @@
     5.4 -(*  Title:      Pure/Tools/xml_syntax.ML
     5.5 -    Author:     Stefan Berghofer, TU Muenchen
     5.6 -
     5.7 -Input and output of types, terms, and proofs in XML format.
     5.8 -See isabelle.xsd for a description of the syntax.
     5.9 -*)
    5.10 -
    5.11 -signature XML_SYNTAX =
    5.12 -sig
    5.13 -  val xml_of_type: typ -> XML.tree
    5.14 -  val xml_of_term: term -> XML.tree
    5.15 -  val xml_of_proof: Proofterm.proof -> XML.tree
    5.16 -  val write_to_file: Path.T -> string -> XML.tree -> unit
    5.17 -  exception XML of string * XML.tree
    5.18 -  val type_of_xml: XML.tree -> typ
    5.19 -  val term_of_xml: XML.tree -> term
    5.20 -  val proof_of_xml: XML.tree -> Proofterm.proof
    5.21 -end;
    5.22 -
    5.23 -structure XML_Syntax : XML_SYNTAX =
    5.24 -struct
    5.25 -
    5.26 -(**** XML output ****)
    5.27 -
    5.28 -fun xml_of_class name = XML.Elem (("class", [("name", name)]), []);
    5.29 -
    5.30 -fun xml_of_type (TVar ((s, i), S)) =
    5.31 -      XML.Elem (("TVar", ("name", s) :: (if i=0 then [] else [("index", string_of_int i)])),
    5.32 -        map xml_of_class S)
    5.33 -  | xml_of_type (TFree (s, S)) =
    5.34 -      XML.Elem (("TFree", [("name", s)]), map xml_of_class S)
    5.35 -  | xml_of_type (Type (s, Ts)) =
    5.36 -      XML.Elem (("Type", [("name", s)]), map xml_of_type Ts);
    5.37 -
    5.38 -fun xml_of_term (Bound i) =
    5.39 -      XML.Elem (("Bound", [("index", string_of_int i)]), [])
    5.40 -  | xml_of_term (Free (s, T)) =
    5.41 -      XML.Elem (("Free", [("name", s)]), [xml_of_type T])
    5.42 -  | xml_of_term (Var ((s, i), T)) =
    5.43 -      XML.Elem (("Var", ("name", s) :: (if i=0 then [] else [("index", string_of_int i)])),
    5.44 -        [xml_of_type T])
    5.45 -  | xml_of_term (Const (s, T)) =
    5.46 -      XML.Elem (("Const", [("name", s)]), [xml_of_type T])
    5.47 -  | xml_of_term (t $ u) =
    5.48 -      XML.Elem (("App", []), [xml_of_term t, xml_of_term u])
    5.49 -  | xml_of_term (Abs (s, T, t)) =
    5.50 -      XML.Elem (("Abs", [("vname", s)]), [xml_of_type T, xml_of_term t]);
    5.51 -
    5.52 -fun xml_of_opttypes NONE = []
    5.53 -  | xml_of_opttypes (SOME Ts) = [XML.Elem (("types", []), map xml_of_type Ts)];
    5.54 -
    5.55 -(* FIXME: the t argument of PThm and PAxm is actually redundant, since *)
    5.56 -(* it can be looked up in the theorem database. Thus, it could be      *)
    5.57 -(* omitted from the xml representation.                                *)
    5.58 -
    5.59 -(* FIXME not exhaustive *)
    5.60 -fun xml_of_proof (PBound i) =
    5.61 -      XML.Elem (("PBound", [("index", string_of_int i)]), [])
    5.62 -  | xml_of_proof (Abst (s, optT, prf)) =
    5.63 -      XML.Elem (("Abst", [("vname", s)]),
    5.64 -        (case optT of NONE => [] | SOME T => [xml_of_type T]) @ [xml_of_proof prf])
    5.65 -  | xml_of_proof (AbsP (s, optt, prf)) =
    5.66 -      XML.Elem (("AbsP", [("vname", s)]),
    5.67 -        (case optt of NONE => [] | SOME t => [xml_of_term t]) @ [xml_of_proof prf])
    5.68 -  | xml_of_proof (prf % optt) =
    5.69 -      XML.Elem (("Appt", []),
    5.70 -        xml_of_proof prf :: (case optt of NONE => [] | SOME t => [xml_of_term t]))
    5.71 -  | xml_of_proof (prf %% prf') =
    5.72 -      XML.Elem (("AppP", []), [xml_of_proof prf, xml_of_proof prf'])
    5.73 -  | xml_of_proof (Hyp t) = XML.Elem (("Hyp", []), [xml_of_term t])
    5.74 -  | xml_of_proof (PThm (_, ((s, t, optTs), _))) =
    5.75 -      XML.Elem (("PThm", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs)
    5.76 -  | xml_of_proof (PAxm (s, t, optTs)) =
    5.77 -      XML.Elem (("PAxm", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs)
    5.78 -  | xml_of_proof (Oracle (s, t, optTs)) =
    5.79 -      XML.Elem (("Oracle", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs)
    5.80 -  | xml_of_proof MinProof =
    5.81 -      XML.Elem (("MinProof", []), []);
    5.82 -
    5.83 -
    5.84 -(* useful for checking the output against a schema file *)
    5.85 -
    5.86 -fun write_to_file path elname x =
    5.87 -  File.write path
    5.88 -    ("<?xml version=\"1.0\" encoding=\"UTF-8\"?>\n" ^
    5.89 -     XML.string_of (XML.Elem ((elname,
    5.90 -         [("xmlns:xsi", "http://www.w3.org/2001/XMLSchema-instance"),
    5.91 -          ("xsi:noNamespaceSchemaLocation", "isabelle.xsd")]),
    5.92 -       [x])));
    5.93 -
    5.94 -
    5.95 -
    5.96 -(**** XML input ****)
    5.97 -
    5.98 -exception XML of string * XML.tree;
    5.99 -
   5.100 -fun class_of_xml (XML.Elem (("class", [("name", name)]), [])) = name
   5.101 -  | class_of_xml tree = raise XML ("class_of_xml: bad tree", tree);
   5.102 -
   5.103 -fun index_of_string s tree idx =
   5.104 -  (case Int.fromString idx of
   5.105 -    NONE => raise XML (s ^ ": bad index", tree)
   5.106 -  | SOME i => i);
   5.107 -
   5.108 -fun type_of_xml (tree as XML.Elem (("TVar", atts), classes)) = TVar
   5.109 -      ((case Properties.get atts "name" of
   5.110 -          NONE => raise XML ("type_of_xml: name of TVar missing", tree)
   5.111 -        | SOME name => name,
   5.112 -        the_default 0 (Option.map (index_of_string "type_of_xml" tree)
   5.113 -          (Properties.get atts "index"))),
   5.114 -       map class_of_xml classes)
   5.115 -  | type_of_xml (XML.Elem (("TFree", [("name", s)]), classes)) =
   5.116 -      TFree (s, map class_of_xml classes)
   5.117 -  | type_of_xml (XML.Elem (("Type", [("name", s)]), types)) =
   5.118 -      Type (s, map type_of_xml types)
   5.119 -  | type_of_xml tree = raise XML ("type_of_xml: bad tree", tree);
   5.120 -
   5.121 -fun term_of_xml (tree as XML.Elem (("Bound", [("index", idx)]), [])) =
   5.122 -      Bound (index_of_string "bad variable index" tree idx)
   5.123 -  | term_of_xml (XML.Elem (("Free", [("name", s)]), [typ])) =
   5.124 -      Free (s, type_of_xml typ)
   5.125 -  | term_of_xml (tree as XML.Elem (("Var", atts), [typ])) = Var
   5.126 -      ((case Properties.get atts "name" of
   5.127 -          NONE => raise XML ("type_of_xml: name of Var missing", tree)
   5.128 -        | SOME name => name,
   5.129 -        the_default 0 (Option.map (index_of_string "term_of_xml" tree)
   5.130 -          (Properties.get atts "index"))),
   5.131 -       type_of_xml typ)
   5.132 -  | term_of_xml (XML.Elem (("Const", [("name", s)]), [typ])) =
   5.133 -      Const (s, type_of_xml typ)
   5.134 -  | term_of_xml (XML.Elem (("App", []), [term, term'])) =
   5.135 -      term_of_xml term $ term_of_xml term'
   5.136 -  | term_of_xml (XML.Elem (("Abs", [("vname", s)]), [typ, term])) =
   5.137 -      Abs (s, type_of_xml typ, term_of_xml term)
   5.138 -  | term_of_xml tree = raise XML ("term_of_xml: bad tree", tree);
   5.139 -
   5.140 -fun opttypes_of_xml [] = NONE
   5.141 -  | opttypes_of_xml [XML.Elem (("types", []), types)] =
   5.142 -      SOME (map type_of_xml types)
   5.143 -  | opttypes_of_xml (tree :: _) = raise XML ("opttypes_of_xml: bad tree", tree);
   5.144 -
   5.145 -fun proof_of_xml (tree as XML.Elem (("PBound", [("index", idx)]), [])) =
   5.146 -      PBound (index_of_string "proof_of_xml" tree idx)
   5.147 -  | proof_of_xml (XML.Elem (("Abst", [("vname", s)]), [proof])) =
   5.148 -      Abst (s, NONE, proof_of_xml proof)
   5.149 -  | proof_of_xml (XML.Elem (("Abst", [("vname", s)]), [typ, proof])) =
   5.150 -      Abst (s, SOME (type_of_xml typ), proof_of_xml proof)
   5.151 -  | proof_of_xml (XML.Elem (("AbsP", [("vname", s)]), [proof])) =
   5.152 -      AbsP (s, NONE, proof_of_xml proof)
   5.153 -  | proof_of_xml (XML.Elem (("AbsP", [("vname", s)]), [term, proof])) =
   5.154 -      AbsP (s, SOME (term_of_xml term), proof_of_xml proof)
   5.155 -  | proof_of_xml (XML.Elem (("Appt", []), [proof])) =
   5.156 -      proof_of_xml proof % NONE
   5.157 -  | proof_of_xml (XML.Elem (("Appt", []), [proof, term])) =
   5.158 -      proof_of_xml proof % SOME (term_of_xml term)
   5.159 -  | proof_of_xml (XML.Elem (("AppP", []), [proof, proof'])) =
   5.160 -      proof_of_xml proof %% proof_of_xml proof'
   5.161 -  | proof_of_xml (XML.Elem (("Hyp", []), [term])) =
   5.162 -      Hyp (term_of_xml term)
   5.163 -  | proof_of_xml (XML.Elem (("PThm", [("name", s)]), term :: opttypes)) =
   5.164 -      (* FIXME? *)
   5.165 -      PThm (serial (), ((s, term_of_xml term, opttypes_of_xml opttypes),
   5.166 -        Future.value (Proofterm.approximate_proof_body MinProof)))
   5.167 -  | proof_of_xml (XML.Elem (("PAxm", [("name", s)]), term :: opttypes)) =
   5.168 -      PAxm (s, term_of_xml term, opttypes_of_xml opttypes)
   5.169 -  | proof_of_xml (XML.Elem (("Oracle", [("name", s)]), term :: opttypes)) =
   5.170 -      Oracle (s, term_of_xml term, opttypes_of_xml opttypes)
   5.171 -  | proof_of_xml (XML.Elem (("MinProof", _), _)) = MinProof
   5.172 -  | proof_of_xml tree = raise XML ("proof_of_xml: bad tree", tree);
   5.173 -
   5.174 -end;