]> matita.cs.unibo.it Git - helm.git/blob - helm/interface/cicParser3.ml
Requires and Provides now fixed
[helm.git] / helm / interface / cicParser3.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 terms level of a parser for cic objects from xml        *)
9 (* files to the internal representation. It is used by the module cicParser2  *)
10 (* (objects level). It defines an extension of the standard dom using the     *)
11 (* object-oriented extension machinery of markup: an object with a method     *)
12 (* to_cic_term that returns the internal representation of the subtree is     *)
13 (* added to each node of the dom tree                                         *)
14 (*                                                                            *)
15 (******************************************************************************)
16
17 exception IllFormedXml of int;;
18
19 (* The hashtable from the current identifiers to the object or the terms *)
20 let ids_to_targets = ref None;;
21
22 (* The list of tokens of the current section path. *)
23 (* Used to resolve relative URIs                   *)
24 let current_sp = ref [];;
25
26 (* The uri of the object been parsed *)
27 let current_uri = ref (UriManager.uri_of_string "cic:/.xml");;
28
29 (* True if annotation really matter *)
30 let process_annotations = ref false;;
31
32 (* Utility functions to map a markup attribute to something useful *)
33
34 let cic_attr_of_xml_attr =
35  function
36     Pxp_types.Value s       -> Cic.Name s
37   | Pxp_types.Implied_value -> Cic.Anonimous
38   | _             -> raise (IllFormedXml 1)
39
40 let cic_sort_of_xml_attr =
41  function
42     Pxp_types.Value "Prop" -> Cic.Prop
43   | Pxp_types.Value "Set"  -> Cic.Set
44   | Pxp_types.Value "Type" -> Cic.Type
45   | _            -> raise (IllFormedXml 2)
46
47 let int_of_xml_attr =
48  function
49     Pxp_types.Value n -> int_of_string n
50   | _       -> raise (IllFormedXml 3)
51
52 let uri_of_xml_attr =
53  function
54     Pxp_types.Value s -> UriManager.uri_of_string s
55   | _       -> raise (IllFormedXml 4)
56
57 let string_of_xml_attr =
58  function
59     Pxp_types.Value s -> s
60   | _       -> raise (IllFormedXml 5)
61
62 let binder_of_xml_attr =
63  function
64     Pxp_types.Value s -> if !process_annotations then Some s else None
65   | _       -> raise (IllFormedXml 17)
66 ;;
67
68 let register_id id node =
69  if !process_annotations then
70   match !ids_to_targets with
71      None -> assert false
72    | Some ids_to_targets ->
73       Hashtbl.add ids_to_targets id (Cic.Term node)
74 ;;
75
76 (* the "interface" of the class linked to each node of the dom tree *)
77
78 class virtual cic_term =
79   object (self)
80
81     (* fields and methods ever required by markup *)
82     val mutable node = (None : cic_term Pxp_document.node option)
83
84     method clone = {< >} 
85     method node =
86       match node with
87           None ->
88             assert false
89         | Some n -> n
90     method set_node n =
91       node <- Some n
92
93     (* a method that returns the internal representation of the tree (term) *)
94     (* rooted in this node                                                  *)
95     method virtual to_cic_term : Cic.annterm
96   end
97 ;;
98
99 (* the class of the objects linked to nodes that are not roots of cic terms *)
100 class eltype_not_of_cic =
101   object (self)
102
103      inherit cic_term
104
105      method to_cic_term = raise (IllFormedXml 6)
106   end
107 ;;
108
109 (* the class of the objects linked to nodes whose content is a cic term *)
110 (* (syntactic sugar xml entities) e.g. <type> ... </type>               *)
111 class eltype_transparent =
112   object (self)
113
114     inherit cic_term
115
116     method to_cic_term =
117      let n = self#node in
118       match n#sub_nodes with
119          [ t ]  -> t#extension#to_cic_term
120        | _  -> raise (IllFormedXml 7)
121   end
122 ;;
123
124 (* A class for each cic node type *)
125
126 class eltype_fix =
127   object (self)
128
129     inherit cic_term
130
131     method to_cic_term =
132      let n = self#node in
133       let nofun = int_of_xml_attr (n#attribute "noFun")
134       and id = string_of_xml_attr (n#attribute "id")
135       and functions =
136        let sons = n#sub_nodes in
137         List.map
138          (function
139              f when f#node_type = Pxp_document.T_element "FixFunction" ->
140               let name = string_of_xml_attr (f#attribute "name")
141               and recindex = int_of_xml_attr (f#attribute "recIndex")
142               and (ty, body) =
143                match f#sub_nodes with
144                   [t ; b] when
145                     t#node_type = Pxp_document.T_element "type" &&
146                     b#node_type = Pxp_document.T_element "body" ->
147                      (t#extension#to_cic_term, b#extension#to_cic_term)
148                 | _ -> raise (IllFormedXml 14)
149               in
150                (name, recindex, ty, body)
151            | _ -> raise (IllFormedXml 13)
152          ) sons
153       in
154        let res = Cic.AFix (id, ref None, nofun, functions) in
155         register_id id res ;
156         res
157   end
158 ;;
159
160 class eltype_cofix =
161   object (self)
162
163     inherit cic_term
164
165     method to_cic_term =
166      let n = self#node in
167       let nofun = int_of_xml_attr (n#attribute "noFun")
168       and id = string_of_xml_attr (n#attribute "id")
169       and functions =
170        let sons = n#sub_nodes in
171         List.map
172          (function
173              f when f#node_type = Pxp_document.T_element "CofixFunction" ->
174               let name = string_of_xml_attr (f#attribute "name")
175               and (ty, body) =
176                match f#sub_nodes with
177                   [t ; b] when
178                     t#node_type = Pxp_document.T_element "type" &&
179                     b#node_type = Pxp_document.T_element "body" ->
180                      (t#extension#to_cic_term, b#extension#to_cic_term)
181                 | _ -> raise (IllFormedXml 16)
182               in
183                (name, ty, body)
184            | _ -> raise (IllFormedXml 15)
185          ) sons
186       in
187        let res = Cic.ACoFix (id, ref None, nofun, functions) in
188         register_id id res ;
189         res
190   end
191 ;;
192
193 class eltype_implicit =
194   object (self)
195
196     inherit cic_term
197
198     method to_cic_term =
199      let n = self#node in
200       let id = string_of_xml_attr (n#attribute "id") in
201        let res = Cic.AImplicit (id, ref None) in
202         register_id id res ;
203         res
204   end
205 ;;
206
207 class eltype_rel =
208   object (self)
209
210     inherit cic_term
211
212     method to_cic_term =
213      let n = self#node in
214       let value  = int_of_xml_attr (n#attribute "value")
215       and binder = binder_of_xml_attr (n#attribute "binder")
216       and id = string_of_xml_attr (n#attribute "id") in
217        let res = Cic.ARel (id,ref None,value,binder) in
218         register_id id res ;
219         res
220   end
221 ;;
222
223 class eltype_meta =
224   object (self)
225
226     inherit cic_term
227
228     method to_cic_term =
229      let n = self#node in
230       let value = int_of_xml_attr (n#attribute "no")
231       and id = string_of_xml_attr (n#attribute "id") in
232        let res = Cic.AMeta (id,ref None,value) in
233         register_id id res ;
234         res
235   end
236 ;;
237
238 class eltype_var =
239   object (self)
240
241     inherit cic_term
242
243     method to_cic_term =
244      let n = self#node in
245       let name = string_of_xml_attr (n#attribute "relUri")
246       and xid = string_of_xml_attr (n#attribute "id") in
247        match Str.split (Str.regexp ",") name with
248           [index; id] ->
249            let get_prefix n =
250             let rec aux =
251              function
252                 (0,_) -> "/"
253               | (n,he::tl) when n > 0 -> "/" ^ he ^ aux (n - 1, tl)
254               | _ -> raise (IllFormedXml 19)
255             in   
256              aux (List.length !current_sp - n,!current_sp)
257            in
258             let res =
259              Cic.AVar
260               (xid,ref None, 
261                (UriManager.uri_of_string
262                 ("cic:" ^ get_prefix (int_of_string index) ^ id ^ ".var"))
263               )
264             in
265              register_id id res ;
266              res
267         | _ -> raise (IllFormedXml 18)
268   end
269 ;;
270
271 class eltype_apply =
272   object (self)
273
274     inherit cic_term
275
276     method to_cic_term =
277      let n = self#node in
278       let children = n#sub_nodes
279       and id = string_of_xml_attr (n#attribute "id") in
280        if List.length children < 2 then raise (IllFormedXml 8)
281        else
282         let res =
283          Cic.AAppl
284           (id,ref None,List.map (fun x -> x#extension#to_cic_term) children)
285         in
286          register_id id res ;
287          res
288   end
289 ;;
290
291 class eltype_cast =
292   object (self)
293
294     inherit cic_term
295
296     method to_cic_term =
297      let n = self#node in
298       let sons = n#sub_nodes
299       and id = string_of_xml_attr (n#attribute "id") in
300        match sons with
301           [te ; ty] when
302             te#node_type = Pxp_document.T_element "term" &&
303             ty#node_type = Pxp_document.T_element "type" ->
304              let term = te#extension#to_cic_term
305              and typ  = ty#extension#to_cic_term in
306               let res = Cic.ACast (id,ref None,term,typ) in
307                register_id id res ;
308                res
309         | _  -> raise (IllFormedXml 9)
310   end
311 ;;
312
313 class eltype_sort =
314   object (self)
315
316     inherit cic_term
317
318     method to_cic_term =
319      let n = self#node in
320       let sort = cic_sort_of_xml_attr (n#attribute "value")
321       and id = string_of_xml_attr (n#attribute "id") in
322        let res = Cic.ASort (id,ref None,sort) in
323         register_id id res ;
324         res
325   end
326 ;;
327
328 class eltype_abst =
329   object (self)
330
331     inherit cic_term
332
333     method to_cic_term =
334      let n = self#node in
335       let value = uri_of_xml_attr (n#attribute "uri")
336       and id = string_of_xml_attr (n#attribute "id") in
337        let res = Cic.AAbst (id,ref None,value) in
338         register_id id res ;
339         res
340   end
341 ;;
342
343 class eltype_const =
344   object (self)
345
346     inherit cic_term
347
348     method to_cic_term =
349      let module U = UriManager in
350       let n = self#node in
351        let value = uri_of_xml_attr (n#attribute "uri")
352        and id = string_of_xml_attr (n#attribute "id") in
353         let res =
354          Cic.AConst (id,ref None,value, U.relative_depth !current_uri value 0)
355         in
356          register_id id res ;
357          res
358   end
359 ;;
360
361 class eltype_mutind =
362   object (self)
363
364     inherit cic_term
365
366     method to_cic_term =
367      let module U = UriManager in
368       let n = self#node in
369        let name = uri_of_xml_attr (n#attribute "uri")
370        and noType = int_of_xml_attr (n#attribute "noType")
371        and id = string_of_xml_attr (n#attribute "id") in
372         let res =
373          Cic.AMutInd
374           (id,ref None,name, U.relative_depth !current_uri name 0, noType)
375         in
376          register_id id res ;
377          res
378   end
379 ;;
380
381 class eltype_mutconstruct =
382   object (self)
383
384     inherit cic_term
385
386     method to_cic_term =
387      let module U = UriManager in
388       let n = self#node in
389        let name = uri_of_xml_attr (n#attribute "uri")
390        and noType = int_of_xml_attr (n#attribute "noType")
391        and noConstr = int_of_xml_attr (n#attribute "noConstr")
392        and id = string_of_xml_attr (n#attribute "id") in
393         let res = 
394          Cic.AMutConstruct
395           (id, ref None, name, U.relative_depth !current_uri name 0,
396           noType, noConstr)
397         in
398          register_id id res ;
399          res
400   end
401 ;;
402
403 class eltype_prod =
404   object (self)
405
406     inherit cic_term
407
408     method to_cic_term =
409      let n = self#node in
410       let sons = n#sub_nodes
411       and id = string_of_xml_attr (n#attribute "id") in
412        match sons with
413           [s ; t] when
414             s#node_type = Pxp_document.T_element "source" &&
415             t#node_type = Pxp_document.T_element "target" ->
416              let name = cic_attr_of_xml_attr (t#attribute "binder")
417              and source = s#extension#to_cic_term
418              and target = t#extension#to_cic_term in
419               let res = Cic.AProd (id,ref None,name,source,target) in
420                register_id id res ;
421                res
422         | _  -> raise (IllFormedXml 10)
423   end
424 ;;
425
426 class eltype_mutcase =
427   object (self)
428
429     inherit cic_term
430
431     method to_cic_term =
432      let module U = UriManager in
433       let n = self#node in
434        let sons = n#sub_nodes
435        and id = string_of_xml_attr (n#attribute "id") in
436         match sons with
437            ty::te::patterns when
438              ty#node_type = Pxp_document.T_element "patternsType" &&
439              te#node_type = Pxp_document.T_element "inductiveTerm" ->
440               let ci = uri_of_xml_attr (n#attribute "uriType")
441               and typeno = int_of_xml_attr (n#attribute "noType")
442               and inductiveType = ty#extension#to_cic_term
443               and inductiveTerm = te#extension#to_cic_term
444               and lpattern= List.map (fun x -> x#extension#to_cic_term) patterns
445               in
446                let res =
447                 Cic.AMutCase (id,ref None,ci,U.relative_depth !current_uri ci 0,
448                  typeno,inductiveType,inductiveTerm,lpattern)
449                in
450                 register_id id res ;
451                 res
452          | _  -> raise (IllFormedXml 11)
453   end
454 ;;
455
456 class eltype_lambda =
457   object (self)
458
459     inherit cic_term
460
461     method to_cic_term =
462      let n = self#node in
463       let sons = n#sub_nodes
464       and id = string_of_xml_attr (n#attribute "id") in
465        match sons with
466           [s ; t] when
467             s#node_type = Pxp_document.T_element "source" &&
468             t#node_type = Pxp_document.T_element "target" ->
469              let name = cic_attr_of_xml_attr (t#attribute "binder")
470              and source = s#extension#to_cic_term
471              and target = t#extension#to_cic_term in
472               let res = Cic.ALambda (id,ref None,name,source,target) in
473                register_id id res ;
474                res
475         | _  -> raise (IllFormedXml 12)
476   end
477 ;;
478
479 class eltype_letin =
480   object (self)
481
482     inherit cic_term
483
484     method to_cic_term =
485      let n = self#node in
486       let sons = n#sub_nodes
487       and id = string_of_xml_attr (n#attribute "id") in
488        match sons with
489           [s ; t] when
490             s#node_type = Pxp_document.T_element "term" &&
491             t#node_type = Pxp_document.T_element "letintarget" ->
492              let name = cic_attr_of_xml_attr (t#attribute "binder")
493              and source = s#extension#to_cic_term
494              and target = t#extension#to_cic_term in
495               let res = Cic.ALetIn (id,ref None,name,source,target) in
496                register_id id res ;
497                res
498         | _  -> raise (IllFormedXml 12)
499   end
500 ;;
501
502 (* The definition of domspec, an hashtable that maps each node type to the *)
503 (* object that must be linked to it. Used by markup.                       *)
504
505 let domspec =
506  let module D = Pxp_document in
507   D.make_spec_from_alist
508    ~data_exemplar: (new D.data_impl (new eltype_not_of_cic))
509    ~default_element_exemplar: (new D.element_impl (new eltype_not_of_cic))
510    ~element_alist:
511     [ "REL",           (new D.element_impl (new eltype_rel)) ;
512       "VAR",           (new D.element_impl (new eltype_var)) ;
513       "META",          (new D.element_impl (new eltype_meta)) ;
514       "SORT",          (new D.element_impl (new eltype_sort)) ;
515       "IMPLICIT",      (new D.element_impl (new eltype_implicit)) ;
516       "CAST",          (new D.element_impl (new eltype_cast)) ;
517       "PROD",          (new D.element_impl (new eltype_prod)) ;
518       "LAMBDA",        (new D.element_impl (new eltype_lambda)) ;
519       "LETIN",         (new D.element_impl (new eltype_letin)) ;
520       "APPLY",         (new D.element_impl (new eltype_apply)) ;
521       "CONST",         (new D.element_impl (new eltype_const)) ;
522       "ABST",          (new D.element_impl (new eltype_abst)) ;
523       "MUTIND",        (new D.element_impl (new eltype_mutind)) ;
524       "MUTCONSTRUCT",  (new D.element_impl (new eltype_mutconstruct)) ;
525       "MUTCASE",       (new D.element_impl (new eltype_mutcase)) ;
526       "FIX",           (new D.element_impl (new eltype_fix)) ;
527       "COFIX",         (new D.element_impl (new eltype_cofix)) ;
528       "arity",         (new D.element_impl (new eltype_transparent)) ;
529       "term",          (new D.element_impl (new eltype_transparent)) ;
530       "type",          (new D.element_impl (new eltype_transparent)) ;
531       "body",          (new D.element_impl (new eltype_transparent)) ;
532       "source",        (new D.element_impl (new eltype_transparent)) ;
533       "target",        (new D.element_impl (new eltype_transparent)) ;
534       "patternsType",  (new D.element_impl (new eltype_transparent)) ;
535       "inductiveTerm", (new D.element_impl (new eltype_transparent)) ;
536       "pattern",       (new D.element_impl (new eltype_transparent))
537     ]
538    ()
539 ;;