let parse_hint node =
let rec parse_hint_node node =
match node#node_type with
- | T_element "ring" -> Use_ring_Luke
- | T_element "fourier" -> Use_fourier_Luke
- | T_element "reflexivity" -> Use_reflexivity_Luke
- | T_element "symmetry" -> Use_symmetry_Luke
- | T_element "assumption" -> Use_assumption_Luke
- | T_element "contradiction" -> Use_contradiction_Luke
- | T_element "exists" -> Use_exists_Luke
- | T_element "split" -> Use_split_Luke
- | T_element "left" -> Use_left_Luke
- | T_element "right" -> Use_right_Luke
- | T_element "apply" -> Use_apply_Luke node#data
+ | T_element "ring" -> Use_ring
+ | T_element "fourier" -> Use_fourier
+ | T_element "reflexivity" -> Use_reflexivity
+ | T_element "symmetry" -> Use_symmetry
+ | T_element "assumption" -> Use_assumption
+ | T_element "contradiction" -> Use_contradiction
+ | T_element "exists" -> Use_exists
+ | T_element "split" -> Use_split
+ | T_element "left" -> Use_left
+ | T_element "right" -> Use_right
+ | T_element "apply" -> Use_apply node#data
| T_element "hints" ->
Hints
(List.map parse_hint_node (List.filter is_xml_element node#sub_nodes))
| None -> "<gTopLevelStatus />\n"
let rec pp_hint = function
- | Use_ring_Luke -> sprintf "<ring />"
- | Use_fourier_Luke -> sprintf "<fourier />"
- | Use_reflexivity_Luke -> sprintf "<reflexivity />"
- | Use_symmetry_Luke -> sprintf "<symmetry />"
- | Use_assumption_Luke -> sprintf "<assumption />"
- | Use_contradiction_Luke -> sprintf "<contradiction />"
- | Use_exists_Luke -> sprintf "<exists />"
- | Use_split_Luke -> sprintf "<split />"
- | Use_left_Luke -> sprintf "<left />"
- | Use_right_Luke -> sprintf "<right />"
- | Use_apply_Luke term -> sprintf "<apply>%s</apply>" term
+ | Use_ring -> sprintf "<ring />"
+ | Use_fourier -> sprintf "<fourier />"
+ | Use_reflexivity -> sprintf "<reflexivity />"
+ | Use_symmetry -> sprintf "<symmetry />"
+ | Use_assumption -> sprintf "<assumption />"
+ | Use_contradiction -> sprintf "<contradiction />"
+ | Use_exists -> sprintf "<exists />"
+ | Use_split -> sprintf "<split />"
+ | Use_left -> sprintf "<left />"
+ | Use_right -> sprintf "<right />"
+ | Use_apply term -> sprintf "<apply>%s</apply>" term
| Hints hints ->
sprintf "<hints>\n%s\n</hints>"
(String.concat "\n" (List.map pp_hint hints))