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