src/Pure/Tools/xml_syntax.ML
author wenzelm
Sun Nov 11 20:31:46 2012 +0100 (2012-11-11)
changeset 50081 9b92ee8dec98
parent 38228 ada3ab6b9085
permissions -rw-r--r--
tuned;
     1 (*  Title:      Pure/Tools/xml_syntax.ML
     2     Author:     Stefan Berghofer, TU Muenchen
     3 
     4 Input and output of types, terms, and proofs in XML format.
     5 See isabelle.xsd for a description of the syntax.
     6 *)
     7 
     8 signature XML_SYNTAX =
     9 sig
    10   val xml_of_type: typ -> XML.tree
    11   val xml_of_term: term -> XML.tree
    12   val xml_of_proof: Proofterm.proof -> XML.tree
    13   val write_to_file: Path.T -> string -> XML.tree -> unit
    14   exception XML of string * XML.tree
    15   val type_of_xml: XML.tree -> typ
    16   val term_of_xml: XML.tree -> term
    17   val proof_of_xml: XML.tree -> Proofterm.proof
    18 end;
    19 
    20 structure XML_Syntax : XML_SYNTAX =
    21 struct
    22 
    23 (**** XML output ****)
    24 
    25 fun xml_of_class name = XML.Elem (("class", [("name", name)]), []);
    26 
    27 fun xml_of_type (TVar ((s, i), S)) =
    28       XML.Elem (("TVar", ("name", s) :: (if i=0 then [] else [("index", string_of_int i)])),
    29         map xml_of_class S)
    30   | xml_of_type (TFree (s, S)) =
    31       XML.Elem (("TFree", [("name", s)]), map xml_of_class S)
    32   | xml_of_type (Type (s, Ts)) =
    33       XML.Elem (("Type", [("name", s)]), map xml_of_type Ts);
    34 
    35 fun xml_of_term (Bound i) =
    36       XML.Elem (("Bound", [("index", string_of_int i)]), [])
    37   | xml_of_term (Free (s, T)) =
    38       XML.Elem (("Free", [("name", s)]), [xml_of_type T])
    39   | xml_of_term (Var ((s, i), T)) =
    40       XML.Elem (("Var", ("name", s) :: (if i=0 then [] else [("index", string_of_int i)])),
    41         [xml_of_type T])
    42   | xml_of_term (Const (s, T)) =
    43       XML.Elem (("Const", [("name", s)]), [xml_of_type T])
    44   | xml_of_term (t $ u) =
    45       XML.Elem (("App", []), [xml_of_term t, xml_of_term u])
    46   | xml_of_term (Abs (s, T, t)) =
    47       XML.Elem (("Abs", [("vname", s)]), [xml_of_type T, xml_of_term t]);
    48 
    49 fun xml_of_opttypes NONE = []
    50   | xml_of_opttypes (SOME Ts) = [XML.Elem (("types", []), map xml_of_type Ts)];
    51 
    52 (* FIXME: the t argument of PThm and PAxm is actually redundant, since *)
    53 (* it can be looked up in the theorem database. Thus, it could be      *)
    54 (* omitted from the xml representation.                                *)
    55 
    56 (* FIXME not exhaustive *)
    57 fun xml_of_proof (PBound i) =
    58       XML.Elem (("PBound", [("index", string_of_int i)]), [])
    59   | xml_of_proof (Abst (s, optT, prf)) =
    60       XML.Elem (("Abst", [("vname", s)]),
    61         (case optT of NONE => [] | SOME T => [xml_of_type T]) @ [xml_of_proof prf])
    62   | xml_of_proof (AbsP (s, optt, prf)) =
    63       XML.Elem (("AbsP", [("vname", s)]),
    64         (case optt of NONE => [] | SOME t => [xml_of_term t]) @ [xml_of_proof prf])
    65   | xml_of_proof (prf % optt) =
    66       XML.Elem (("Appt", []),
    67         xml_of_proof prf :: (case optt of NONE => [] | SOME t => [xml_of_term t]))
    68   | xml_of_proof (prf %% prf') =
    69       XML.Elem (("AppP", []), [xml_of_proof prf, xml_of_proof prf'])
    70   | xml_of_proof (Hyp t) = XML.Elem (("Hyp", []), [xml_of_term t])
    71   | xml_of_proof (PThm (_, ((s, t, optTs), _))) =
    72       XML.Elem (("PThm", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs)
    73   | xml_of_proof (PAxm (s, t, optTs)) =
    74       XML.Elem (("PAxm", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs)
    75   | xml_of_proof (Oracle (s, t, optTs)) =
    76       XML.Elem (("Oracle", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs)
    77   | xml_of_proof MinProof =
    78       XML.Elem (("MinProof", []), []);
    79 
    80 
    81 (* useful for checking the output against a schema file *)
    82 
    83 fun write_to_file path elname x =
    84   File.write path
    85     ("<?xml version=\"1.0\" encoding=\"UTF-8\"?>\n" ^
    86      XML.string_of (XML.Elem ((elname,
    87          [("xmlns:xsi", "http://www.w3.org/2001/XMLSchema-instance"),
    88           ("xsi:noNamespaceSchemaLocation", "isabelle.xsd")]),
    89        [x])));
    90 
    91 
    92 
    93 (**** XML input ****)
    94 
    95 exception XML of string * XML.tree;
    96 
    97 fun class_of_xml (XML.Elem (("class", [("name", name)]), [])) = name
    98   | class_of_xml tree = raise XML ("class_of_xml: bad tree", tree);
    99 
   100 fun index_of_string s tree idx =
   101   (case Int.fromString idx of
   102     NONE => raise XML (s ^ ": bad index", tree)
   103   | SOME i => i);
   104 
   105 fun type_of_xml (tree as XML.Elem (("TVar", atts), classes)) = TVar
   106       ((case Properties.get atts "name" of
   107           NONE => raise XML ("type_of_xml: name of TVar missing", tree)
   108         | SOME name => name,
   109         the_default 0 (Option.map (index_of_string "type_of_xml" tree)
   110           (Properties.get atts "index"))),
   111        map class_of_xml classes)
   112   | type_of_xml (XML.Elem (("TFree", [("name", s)]), classes)) =
   113       TFree (s, map class_of_xml classes)
   114   | type_of_xml (XML.Elem (("Type", [("name", s)]), types)) =
   115       Type (s, map type_of_xml types)
   116   | type_of_xml tree = raise XML ("type_of_xml: bad tree", tree);
   117 
   118 fun term_of_xml (tree as XML.Elem (("Bound", [("index", idx)]), [])) =
   119       Bound (index_of_string "bad variable index" tree idx)
   120   | term_of_xml (XML.Elem (("Free", [("name", s)]), [typ])) =
   121       Free (s, type_of_xml typ)
   122   | term_of_xml (tree as XML.Elem (("Var", atts), [typ])) = Var
   123       ((case Properties.get atts "name" of
   124           NONE => raise XML ("type_of_xml: name of Var missing", tree)
   125         | SOME name => name,
   126         the_default 0 (Option.map (index_of_string "term_of_xml" tree)
   127           (Properties.get atts "index"))),
   128        type_of_xml typ)
   129   | term_of_xml (XML.Elem (("Const", [("name", s)]), [typ])) =
   130       Const (s, type_of_xml typ)
   131   | term_of_xml (XML.Elem (("App", []), [term, term'])) =
   132       term_of_xml term $ term_of_xml term'
   133   | term_of_xml (XML.Elem (("Abs", [("vname", s)]), [typ, term])) =
   134       Abs (s, type_of_xml typ, term_of_xml term)
   135   | term_of_xml tree = raise XML ("term_of_xml: bad tree", tree);
   136 
   137 fun opttypes_of_xml [] = NONE
   138   | opttypes_of_xml [XML.Elem (("types", []), types)] =
   139       SOME (map type_of_xml types)
   140   | opttypes_of_xml (tree :: _) = raise XML ("opttypes_of_xml: bad tree", tree);
   141 
   142 fun proof_of_xml (tree as XML.Elem (("PBound", [("index", idx)]), [])) =
   143       PBound (index_of_string "proof_of_xml" tree idx)
   144   | proof_of_xml (XML.Elem (("Abst", [("vname", s)]), [proof])) =
   145       Abst (s, NONE, proof_of_xml proof)
   146   | proof_of_xml (XML.Elem (("Abst", [("vname", s)]), [typ, proof])) =
   147       Abst (s, SOME (type_of_xml typ), proof_of_xml proof)
   148   | proof_of_xml (XML.Elem (("AbsP", [("vname", s)]), [proof])) =
   149       AbsP (s, NONE, proof_of_xml proof)
   150   | proof_of_xml (XML.Elem (("AbsP", [("vname", s)]), [term, proof])) =
   151       AbsP (s, SOME (term_of_xml term), proof_of_xml proof)
   152   | proof_of_xml (XML.Elem (("Appt", []), [proof])) =
   153       proof_of_xml proof % NONE
   154   | proof_of_xml (XML.Elem (("Appt", []), [proof, term])) =
   155       proof_of_xml proof % SOME (term_of_xml term)
   156   | proof_of_xml (XML.Elem (("AppP", []), [proof, proof'])) =
   157       proof_of_xml proof %% proof_of_xml proof'
   158   | proof_of_xml (XML.Elem (("Hyp", []), [term])) =
   159       Hyp (term_of_xml term)
   160   | proof_of_xml (XML.Elem (("PThm", [("name", s)]), term :: opttypes)) =
   161       (* FIXME? *)
   162       PThm (serial (), ((s, term_of_xml term, opttypes_of_xml opttypes),
   163         Future.value (Proofterm.approximate_proof_body MinProof)))
   164   | proof_of_xml (XML.Elem (("PAxm", [("name", s)]), term :: opttypes)) =
   165       PAxm (s, term_of_xml term, opttypes_of_xml opttypes)
   166   | proof_of_xml (XML.Elem (("Oracle", [("name", s)]), term :: opttypes)) =
   167       Oracle (s, term_of_xml term, opttypes_of_xml opttypes)
   168   | proof_of_xml (XML.Elem (("MinProof", _), _)) = MinProof
   169   | proof_of_xml tree = raise XML ("proof_of_xml: bad tree", tree);
   170 
   171 end;