100 |
100 |
101 fun index_of_string s tree idx = (case Int.fromString idx of |
101 fun index_of_string s tree idx = (case Int.fromString idx of |
102 NONE => raise XML (s ^ ": bad index", tree) | SOME i => i); |
102 NONE => raise XML (s ^ ": bad index", tree) | SOME i => i); |
103 |
103 |
104 fun type_of_xml (tree as XML.Elem ("TVar", atts, classes)) = TVar |
104 fun type_of_xml (tree as XML.Elem ("TVar", atts, classes)) = TVar |
105 ((case AList.lookup op = atts "name" of |
105 ((case Properties.get atts "name" of |
106 NONE => raise XML ("type_of_xml: name of TVar missing", tree) |
106 NONE => raise XML ("type_of_xml: name of TVar missing", tree) |
107 | SOME name => name, |
107 | SOME name => name, |
108 the_default 0 (Option.map (index_of_string "type_of_xml" tree) |
108 the_default 0 (Option.map (index_of_string "type_of_xml" tree) |
109 (AList.lookup op = atts "index"))), |
109 (Properties.get atts "index"))), |
110 map class_of_xml classes) |
110 map class_of_xml classes) |
111 | type_of_xml (XML.Elem ("TFree", [("name", s)], classes)) = |
111 | type_of_xml (XML.Elem ("TFree", [("name", s)], classes)) = |
112 TFree (s, map class_of_xml classes) |
112 TFree (s, map class_of_xml classes) |
113 | type_of_xml (XML.Elem ("Type", [("name", s)], types)) = |
113 | type_of_xml (XML.Elem ("Type", [("name", s)], types)) = |
114 Type (s, map type_of_xml types) |
114 Type (s, map type_of_xml types) |
117 fun term_of_xml (tree as XML.Elem ("Bound", [("index", idx)], [])) = |
117 fun term_of_xml (tree as XML.Elem ("Bound", [("index", idx)], [])) = |
118 Bound (index_of_string "bad variable index" tree idx) |
118 Bound (index_of_string "bad variable index" tree idx) |
119 | term_of_xml (XML.Elem ("Free", [("name", s)], [typ])) = |
119 | term_of_xml (XML.Elem ("Free", [("name", s)], [typ])) = |
120 Free (s, type_of_xml typ) |
120 Free (s, type_of_xml typ) |
121 | term_of_xml (tree as XML.Elem ("Var", atts, [typ])) = Var |
121 | term_of_xml (tree as XML.Elem ("Var", atts, [typ])) = Var |
122 ((case AList.lookup op = atts "name" of |
122 ((case Properties.get atts "name" of |
123 NONE => raise XML ("type_of_xml: name of Var missing", tree) |
123 NONE => raise XML ("type_of_xml: name of Var missing", tree) |
124 | SOME name => name, |
124 | SOME name => name, |
125 the_default 0 (Option.map (index_of_string "term_of_xml" tree) |
125 the_default 0 (Option.map (index_of_string "term_of_xml" tree) |
126 (AList.lookup op = atts "index"))), |
126 (Properties.get atts "index"))), |
127 type_of_xml typ) |
127 type_of_xml typ) |
128 | term_of_xml (XML.Elem ("Const", [("name", s)], [typ])) = |
128 | term_of_xml (XML.Elem ("Const", [("name", s)], [typ])) = |
129 Const (s, type_of_xml typ) |
129 Const (s, type_of_xml typ) |
130 | term_of_xml (XML.Elem ("App", [], [term, term'])) = |
130 | term_of_xml (XML.Elem ("App", [], [term, term'])) = |
131 term_of_xml term $ term_of_xml term' |
131 term_of_xml term $ term_of_xml term' |