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