]> matita.cs.unibo.it Git - helm.git/blob - helm/interface/cicParser2.ml
Requires and Provides now fixed
[helm.git] / helm / interface / cicParser2.ml
1 (******************************************************************************)
2 (*                                                                            *)
3 (*                               PROJECT HELM                                 *)
4 (*                                                                            *)
5 (*                Claudio Sacerdoti Coen <sacerdot@@cs.unibo.it>              *)
6 (*                                 24/01/2000                                 *)
7 (*                                                                            *)
8 (* This module is the objects level of a parser for cic objects from xml      *)
9 (* files to the internal representation. It uses the module cicParser3        *)
10 (* cicParser3 (terms level) and it is used only through cicParser2 (top       *)
11 (* level).                                                                    *)
12 (*                                                                            *)
13 (******************************************************************************)
14
15 exception IllFormedXml of int;;
16 exception NotImplemented;;
17
18 (* Utility functions that transform a Pxp attribute into something useful *)
19
20 (* mk_absolute_uris "n1: v1 ... vn n2 : u1 ... un ...."      *)
21 (* returns [(n1,[absolute_uri_for_v1 ; ... ; absolute_uri_for_vn]) ; (n2,...) *)
22 let mk_absolute_uris s =
23  let l = (Str.split (Str.regexp ":") s) in
24   let absolute_of_relative n v =
25    let module P3 = CicParser3 in
26     let rec mkburi =
27      function
28         (0,_) -> "/"
29       | (n,he::tl) when n > 0 ->
30          "/" ^ he ^ mkburi (n - 1, tl)
31       | _ -> raise (IllFormedXml 12)
32     in
33      let m = List.length !P3.current_sp - (int_of_string n) in
34       let buri = mkburi (m, !P3.current_sp) in
35        UriManager.uri_of_string ("cic:" ^ buri ^ v ^ ".var")
36   in
37    let rec absolutize =
38     function
39        [] -> []
40      | [no ; vs] ->
41         let vars = (Str.split (Str.regexp " ") vs) in
42          [(int_of_string no, List.map (absolute_of_relative no) vars)]
43      | no::vs::tl -> 
44         let vars = (Str.split (Str.regexp " ") vs) in
45          let rec add_prefix =
46           function
47              [no2] -> ([], no2)
48            | he::tl ->
49               let (pvars, no2) = add_prefix tl in
50                ((absolute_of_relative no he)::pvars, no2)
51            | _ -> raise (IllFormedXml 11)
52          in
53           let (pvars, no2) = add_prefix vars in
54            (int_of_string no, pvars)::(absolutize (no2::tl))
55      | _ -> raise (IllFormedXml 10)
56    in
57     (* last parameter must be applied first *)
58     absolutize l
59 ;;
60
61 let option_uri_list_of_attr a1 a2 =
62  let module T = Pxp_types in
63   let parameters =
64    match a1 with
65       T.Value s -> mk_absolute_uris s
66     | _ -> raise (IllFormedXml 0)
67   in
68    match a2 with
69       T.Value "POSSIBLE" -> Cic.Possible parameters
70     | T.Implied_value -> Cic.Actual parameters
71     | _ -> raise (IllFormedXml 0)
72 ;;
73
74 let uri_list_of_attr a =
75  let module T = Pxp_types in
76   match a with
77      T.Value s -> mk_absolute_uris s
78    | _ -> raise (IllFormedXml 0)
79 ;;
80
81 let string_of_attr a =
82  let module T = Pxp_types in
83   match a with
84      T.Value s -> s
85    | _ -> raise (IllFormedXml 0)
86 ;;
87
88 let int_of_attr a =
89  int_of_string (string_of_attr a)
90 ;;
91
92 let bool_of_attr a =
93  bool_of_string (string_of_attr a)
94 ;;
95
96 (* Other utility functions *)
97
98 let get_content n =
99  match n#sub_nodes with
100     [ t ] -> t
101   | _     -> raise (IllFormedXml 1)
102 ;;
103
104 let register_id id node =
105  if !CicParser3.process_annotations then
106   match !CicParser3.ids_to_targets with
107      None -> assert false
108    | Some ids_to_targets ->
109       Hashtbl.add ids_to_targets id (Cic.Object node)
110 ;;
111
112 (* Functions that, given the list of sons of a node of the cic dom (objects   *)
113 (* level), retrieve the internal representation associated to the node.       *)
114 (* Everytime a cic term subtree is found, it is translated to the internal    *)
115 (* representation using the method to_cic_term defined in cicParser3.         *)
116 (* Each function raise IllFormedXml if something goes wrong, but this should  *)
117 (* be impossible due to the presence of the dtd                               *)
118 (* The functions should really be obvious looking at their name and the cic   *)
119 (* dtd                                                                        *)
120
121 (* called when a CurrentProof is found *)
122 let get_conjs_value_type l =
123  let rec rget (c, v, t) l =
124   let module D = Pxp_document in
125    match l with
126       [] -> (c, v, t)
127     | conj::tl when conj#node_type = D.T_element "Conjecture" ->
128        let no = int_of_attr (conj#attribute "no")
129        and typ = (get_content conj)#extension#to_cic_term in
130         rget ((no, typ)::c, v, t) tl
131     | value::tl when value#node_type = D.T_element "body" ->
132        let v' = (get_content value)#extension#to_cic_term in
133         (match v with
134             None -> rget (c, Some v', t) tl
135           | _    -> raise (IllFormedXml 2)
136         )
137     | typ::tl when typ#node_type = D.T_element "type" ->
138        let t' = (get_content typ)#extension#to_cic_term in
139         (match t with
140             None -> rget (c, v, Some t') tl
141           | _    -> raise (IllFormedXml 3)
142         )
143     | _ -> raise (IllFormedXml 4)
144  in
145   match rget ([], None, None) l with
146      (c, Some v, Some t) -> (c, v, t)
147    | _ -> raise (IllFormedXml 5)
148 ;;
149
150 (* used only by get_inductive_types; called one time for each inductive  *)
151 (* definitions in a block of inductive definitions                       *)
152 let get_names_arity_constructors l =
153  let rec rget (a,c) l =
154   let module D = Pxp_document in
155    match l with
156       [] -> (a, c)
157     | arity::tl when arity#node_type = D.T_element "arity" ->
158        let a' = (get_content arity)#extension#to_cic_term in
159         rget (Some a',c) tl
160     | con::tl when con#node_type = D.T_element "Constructor" ->
161        let id = string_of_attr (con#attribute "name")
162        and ty = (get_content con)#extension#to_cic_term in
163          rget (a,(id,ty,ref None)::c) tl
164     | _ -> raise (IllFormedXml 9)
165  in
166   match rget (None,[]) l with
167      (Some a, c) -> (a, List.rev c)
168    | _ -> raise (IllFormedXml 8)
169 ;;
170
171 (* called when an InductiveDefinition is found *)
172 let rec get_inductive_types =
173  function
174     []     -> []
175   | he::tl ->
176      let tyname    = string_of_attr (he#attribute "name")
177      and inductive = bool_of_attr   (he#attribute "inductive")
178      and (arity,cons) =
179       get_names_arity_constructors (he#sub_nodes)
180      in
181       (tyname,inductive,arity,cons)::(get_inductive_types tl) (*CSC 0 a caso *)
182 ;;
183
184 (* This is the main function and also the only one used directly from *)
185 (* cicParser. Given the root of the dom tree, it returns the internal *)
186 (* representation of the cic object described in the tree             *)
187 (* It uses the previous functions and the to_cic_term method defined  *)
188 (* in cicParser3 (used for subtrees that encode cic terms)            *)
189 let rec get_term n =
190  let module D = Pxp_document in
191  let module C = Cic in
192   let ntype = n # node_type in
193   match ntype with
194     D.T_element "Definition" ->
195       let id = string_of_attr (n # attribute "name")
196       and params =
197        option_uri_list_of_attr (n#attribute "params") (n#attribute "paramMode")
198       and (value, typ) = 
199        let sons = n#sub_nodes in
200         match sons with
201           [v ; t] when
202             v#node_type = D.T_element "body" &&
203             t#node_type = D.T_element "type" ->
204              let v' = get_content v
205              and t' = get_content t in
206               (v'#extension#to_cic_term, t'#extension#to_cic_term)
207         | _ -> raise (IllFormedXml 6)
208       and xid = string_of_attr (n#attribute "id") in
209        let res = C.ADefinition (xid, ref None, id, value, typ, params) in
210         register_id xid res ;
211         res
212   | D.T_element "Axiom" ->
213       let id = string_of_attr (n # attribute "name")
214       and params = uri_list_of_attr (n # attribute "params")
215       and typ = 
216        (get_content (get_content n))#extension#to_cic_term
217       and xid = string_of_attr (n#attribute "id") in
218        let res = C.AAxiom (xid, ref None, id, typ, params) in
219         register_id xid res ;
220         res
221   | D.T_element "CurrentProof" ->
222      let name = string_of_attr (n#attribute "name")
223      and xid = string_of_attr (n#attribute "id") in
224      let sons = n#sub_nodes in
225       let (conjs, value, typ) = get_conjs_value_type sons in
226        let res = C.ACurrentProof (xid, ref None, name, conjs, value, typ) in
227         register_id xid res ;
228         res
229   | D.T_element "InductiveDefinition" ->
230      let sons = n#sub_nodes
231      and xid = string_of_attr (n#attribute "id") in
232       let inductiveTypes = get_inductive_types sons
233       and params = uri_list_of_attr (n#attribute "params")
234       and nparams = int_of_attr (n#attribute "noParams") in
235        let res =
236         C.AInductiveDefinition (xid, ref None, inductiveTypes, params, nparams)
237        in
238         register_id xid res ;
239         res
240   | D.T_element "Variable" ->
241      let name = string_of_attr (n#attribute "name")
242      and xid = string_of_attr (n#attribute "id")
243      and (body, typ) = 
244       let sons = n#sub_nodes in
245        match sons with
246           [b ; t] when
247             b#node_type = D.T_element "body" &&
248             t#node_type = D.T_element "type" ->
249              let b' = get_content b
250              and t' = get_content t in
251               (Some (b'#extension#to_cic_term), t'#extension#to_cic_term)
252         | [t] when t#node_type = D.T_element "type" ->
253              let t' = get_content t in
254               (None, t'#extension#to_cic_term)
255         | _ -> raise (IllFormedXml 6)
256      in
257       let res = C.AVariable (xid,ref None,name,body,typ) in
258        register_id xid res ;
259        res
260   | D.T_element _
261   | D.T_data
262   | _ ->
263      raise (IllFormedXml 7)
264 ;;