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