]> matita.cs.unibo.it Git - helm.git/blob - helm/interface/annotation2Xml.ml
Requires and Provides now fixed
[helm.git] / helm / interface / annotation2Xml.ml
1 (*CSC codice cut & paste da cicPp e xmlcommand *)
2
3 exception ImpossiblePossible;;
4 exception NotImplemented;;
5 exception BinderNotSpecified;;
6
7 let dtdname = "http://localhost:8081/getdtd?url=annotations.dtd";;
8
9 (*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
10 let print_term =
11  let rec aux =
12   let module C = Cic in
13   let module X = Xml in
14   let module U = UriManager in
15     function
16        C.ARel (id,ann,_,_) ->
17         (match !ann with
18             None -> [<>]
19           | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
20         )
21      | C.AVar (id,ann,_) ->
22         (match !ann with
23             None -> [<>]
24           | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
25         )
26      | C.AMeta (id,ann,_) ->
27         (match !ann with
28             None -> [<>]
29           | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
30         )
31      | C.ASort (id,ann,_) ->
32         (match !ann with
33             None -> [<>]
34           | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
35         )
36      | C.AImplicit _ -> raise NotImplemented
37      | C.AProd (id,ann,_,s,t) ->
38         [< (match !ann with
39                None -> [<>]
40              | Some ann ->
41                 (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
42            ) ;
43            aux s ;
44            aux t
45         >]
46      | C.ACast (id,ann,v,t) ->
47         [< (match !ann with
48                None -> [<>]
49              | Some ann ->
50                 (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
51            ) ;
52            aux v ;
53            aux t
54         >]
55      | C.ALambda (id,ann,_,s,t) ->
56         [< (match !ann with
57                None -> [<>]
58              | Some ann ->
59                 (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
60            ) ;
61            aux s ;
62            aux t
63         >]
64      | C.ALetIn (id,ann,_,s,t) ->
65         [< (match !ann with
66                None -> [<>]
67              | Some ann ->
68                 (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
69            ) ;
70            aux s ;
71            aux t
72         >]
73      | C.AAppl (id,ann,li) ->
74         [< (match !ann with
75                None -> [<>]
76              | Some ann ->
77                 (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
78            ) ;
79            List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>]
80         >]
81      | C.AConst (id,ann,_,_) ->
82         (match !ann with
83             None -> [<>]
84           | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
85         )
86      | C.AAbst (id,ann,_) -> raise NotImplemented
87      | C.AMutInd (id,ann,_,_,_) ->
88         (match !ann with
89             None -> [<>]
90           | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
91         )
92      | C.AMutConstruct (id,ann,_,_,_,_) ->
93         (match !ann with
94             None -> [<>]
95           | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
96         )
97      | C.AMutCase (id,ann,_,_,_,ty,te,patterns) ->
98         [< (match !ann with
99                None -> [<>]
100              | Some ann ->
101                 (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
102            ) ;
103            aux ty ;
104            aux te ;
105            List.fold_right
106             (fun x i -> [< aux x ; i>])
107             patterns [<>]
108         >]
109      | C.AFix (id, ann, _, funs) ->
110         [< (match !ann with
111                None -> [<>]
112              | Some ann ->
113                 (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
114            ) ;
115            List.fold_right
116             (fun (_,_,ti,bi) i -> [< aux ti ; aux bi ; i >]) funs [<>]
117         >]
118      | C.ACoFix (id, ann,no,funs) ->
119         [< (match !ann with
120                None -> [<>]
121              | Some ann ->
122                 (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
123            ) ;
124            List.fold_right
125             (fun (_,ti,bi) i -> [< aux ti ; aux bi ; i >]) funs [<>]
126         >]
127  in
128   aux
129 ;;
130
131 let print_mutual_inductive_type (_,_,arity,constructors) =
132  [< print_term arity ;
133     List.fold_right
134      (fun (name,ty,_) i -> [< print_term ty ; i >]) constructors [<>]
135  >]
136 ;;
137
138 let target_uri_of_annotation_uri uri =
139  Str.replace_first (Str.regexp "\.ann$") "" (UriManager.string_of_uri uri)
140 ;;
141
142 let pp_annotation obj curi =
143  let module C = Cic in
144  let module X = Xml in
145   [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
146      X.xml_cdata ("<!DOCTYPE Annotations SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
147      X.xml_nempty "Annotations" ["of", target_uri_of_annotation_uri curi]
148       begin
149        match obj with
150          C.ADefinition (xid, ann, _, te, ty, _) ->
151           [< (match !ann with
152                  None -> [<>]
153                | Some ann ->
154                   X.xml_nempty "Annotation" ["of", xid] (X.xml_cdata ann)
155              ) ;
156              print_term te ;
157              print_term ty
158           >]
159        | C.AAxiom (xid, ann, _, ty, _) ->
160           [< (match !ann with
161                  None -> [<>]
162                | Some ann ->
163                   X.xml_nempty "Annotation" ["of", xid] (X.xml_cdata ann)
164              ) ;
165              print_term ty
166           >]
167        | C.AVariable (xid, ann, _, bo, ty) ->
168           [< (match !ann with
169                  None -> [<>]
170                | Some ann ->
171                   X.xml_nempty "Annotation" ["of", xid] (X.xml_cdata ann)
172              ) ;
173              (match bo with
174                  None -> [<>]
175                | Some bo -> print_term bo
176              ) ;
177              print_term ty
178           >]
179        | C.ACurrentProof (xid, ann, _, conjs, bo, ty) ->
180           [< (match !ann with
181                  None -> [<>]
182                | Some ann ->
183                   X.xml_nempty "Annotation" ["of", xid] (X.xml_cdata ann)
184              ) ;
185              List.fold_right
186               (fun (_,t) i -> [< print_term t ; i >])
187               conjs [<>] ;
188              print_term bo ;
189              print_term ty
190           >]
191        | C.AInductiveDefinition (xid, ann, tys, params, paramsno) ->
192           [< (match !ann with
193                  None -> [<>]
194                | Some ann ->
195                   X.xml_nempty "Annotation" ["of", xid] (X.xml_cdata ann)
196              ) ;
197              List.fold_right
198               (fun x i -> [< print_mutual_inductive_type x ; i >])
199               tys [< >]
200           >]
201       end
202   >]
203 ;;