]> matita.cs.unibo.it Git - helm.git/blob - helm/fix_params/cic2Xml.ml
...
[helm.git] / helm / fix_params / cic2Xml.ml
1
2 (* Copyright (C) 2000, HELM Team.
3  * 
4  * This file is part of HELM, an Hypertextual, Electronic
5  * Library of Mathematics, developed at the Computer Science
6  * Department, University of Bologna, Italy.
7  * 
8  * HELM is free software; you can redistribute it and/or
9  * modify it under the terms of the GNU General Public License
10  * as published by the Free Software Foundation; either version 2
11  * of the License, or (at your option) any later version.
12  * 
13  * HELM is distributed in the hope that it will be useful,
14  * but WITHOUT ANY WARRANTY; without even the implied warranty of
15  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
16  * GNU General Public License for more details.
17  *
18  * You should have received a copy of the GNU General Public License
19  * along with HELM; if not, write to the Free Software
20  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
21  * MA  02111-1307, USA.
22  * 
23  * For details, see the HELM World-Wide-Web page,
24  * http://cs.unibo.it/helm/.
25  *)
26
27 (*CSC codice cut & paste da cicPp e xmlcommand *)
28
29 exception ImpossiblePossible;;
30 exception NotImplemented;;
31 let dtdname = "http://localhost:8081/getdtd?url=cic.dtd";;
32
33 (*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
34 let print_term curi =
35  let rec aux =
36   let module C = Cic in
37   let module X = Xml in
38   let module U = UriManager in
39     function
40        C.ARel (id,n,b) ->
41         X.xml_empty "REL" ["value",(string_of_int n);"binder",b;"id",id]
42      | C.AVar (id,uri) ->
43         let vdepth = U.depth_of_uri uri
44         and cdepth = U.depth_of_uri curi in
45          X.xml_empty "VAR"
46           ["relUri",(string_of_int (cdepth - vdepth)) ^ "," ^
47             (U.name_of_uri uri) ;
48            "id",id]
49      | C.AMeta (id,n) ->
50         X.xml_empty "META" ["no",(string_of_int n) ; "id",id]
51      | C.ASort (id,s) ->
52         let string_of_sort =
53          function
54             C.Prop -> "Prop"
55           | C.Set  -> "Set"
56           | C.Type -> "Type"
57         in
58          X.xml_empty "SORT" ["value",(string_of_sort s) ; "id",id]
59      | C.AImplicit _ -> raise NotImplemented
60      | C.AProd (id,C.Anonimous,s,t) ->
61         X.xml_nempty "PROD" ["id",id]
62          [< X.xml_nempty "source" [] (aux s) ;
63             X.xml_nempty "target" [] (aux t)
64          >]
65      | C.AProd (xid,C.Name id,s,t) ->
66        X.xml_nempty "PROD" ["id",xid]
67         [< X.xml_nempty "source" [] (aux s) ;
68            X.xml_nempty "target" ["binder",id] (aux t)
69         >]
70      | C.ACast (id,v,t) ->
71         X.xml_nempty "CAST" ["id",id]
72          [< X.xml_nempty "term" [] (aux v) ;
73             X.xml_nempty "type" [] (aux t)
74          >]
75      | C.ALambda (id,C.Anonimous,s,t) ->
76         X.xml_nempty "LAMBDA" ["id",id]
77          [< X.xml_nempty "source" [] (aux s) ;
78             X.xml_nempty "target" [] (aux t)
79          >]
80      | C.ALambda (xid,C.Name id,s,t) ->
81        X.xml_nempty "LAMBDA" ["id",xid]
82         [< X.xml_nempty "source" [] (aux s) ;
83            X.xml_nempty "target" ["binder",id] (aux t)
84         >]
85      | C.ALetIn (xid,C.Anonimous,s,t) ->
86        assert false (*CSC: significa che e' sbagliato il tipo di LetIn!!!*)
87      | C.ALetIn (xid,C.Name id,s,t) ->
88        X.xml_nempty "LETIN" ["id",xid]
89         [< X.xml_nempty "term" [] (aux s) ;
90            X.xml_nempty "letintarget" ["binder",id] (aux t)
91         >]
92      | C.AAppl (id,li) ->
93         X.xml_nempty "APPLY" ["id",id]
94          [< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>])
95          >]
96      | C.AConst (id,uri,_) ->
97         X.xml_empty "CONST" ["uri", (U.string_of_uri uri) ; "id",id]
98      | C.AMutInd (id,uri,_,i) ->
99         X.xml_empty "MUTIND"
100          ["uri", (U.string_of_uri uri) ;
101           "noType",(string_of_int i) ;
102           "id",id]
103      | C.AMutConstruct (id,uri,_,i,j) ->
104         X.xml_empty "MUTCONSTRUCT"
105          ["uri", (U.string_of_uri uri) ;
106           "noType",(string_of_int i) ; "noConstr",(string_of_int j) ;
107           "id",id]
108      | C.AMutCase (id,uri,_,typeno,ty,te,patterns) ->
109         X.xml_nempty "MUTCASE"
110          ["uriType",(U.string_of_uri uri) ;
111           "noType", (string_of_int typeno) ;
112           "id", id]
113          [< X.xml_nempty "patternsType" [] [< (aux ty) >] ;
114             X.xml_nempty "inductiveTerm" [] [< (aux te) >] ;
115             List.fold_right
116              (fun x i -> [< X.xml_nempty "pattern" [] [< aux x >] ; i>])
117              patterns [<>]
118          >]
119      | C.AFix (id, no, funs) ->
120        X.xml_nempty "FIX" ["noFun", (string_of_int no) ; "id",id]
121         [< List.fold_right
122             (fun (fi,ai,ti,bi) i ->
123               [< X.xml_nempty "FixFunction"
124                   ["name", fi; "recIndex", (string_of_int ai)]
125                   [< X.xml_nempty "type" [] [< aux ti >] ;
126                      X.xml_nempty "body" [] [< aux bi >]
127                   >] ;
128                  i
129               >]
130             ) funs [<>]
131         >]
132      | C.ACoFix (id,no,funs) ->
133        X.xml_nempty "COFIX" ["noFun", (string_of_int no) ; "id",id]
134         [< List.fold_right
135             (fun (fi,ti,bi) i ->
136               [< X.xml_nempty "CofixFunction" ["name", fi]
137                   [< X.xml_nempty "type" [] [< aux ti >] ;
138                      X.xml_nempty "body" [] [< aux bi >]
139                   >] ;
140                  i
141               >]
142             ) funs [<>]
143         >]
144  in
145   aux
146 ;;
147
148 let encode params =
149  List.fold_right
150   (fun (n,l) i ->
151     match l with
152        [] -> i
153      | _ ->
154        string_of_int n ^ ": " ^ 
155        String.concat " " (List.map UriManager.name_of_uri l) ^
156        i
157   ) params ""
158 ;;
159
160 let print_mutual_inductive_type curi (typename,inductive,arity,constructors) =
161  let module C = Cic in
162  let module X = Xml in
163   [< X.xml_nempty "InductiveType"
164       ["name",typename ;
165        "inductive",(string_of_bool inductive)
166       ]
167       [< X.xml_nempty "arity" [] (print_term curi arity) ;
168          (List.fold_right
169           (fun (name,ty,_) i ->
170             [< X.xml_nempty "Constructor" ["name",name]
171                 (print_term curi ty) ;
172                i
173             >])
174           constructors
175           [<>]
176          )
177       >]
178   >]
179 ;;
180
181 let pp obj curi =
182  let module C = Cic in
183  let module X = Xml in
184   match obj with
185      C.ADefinition (xid, id, te, ty, params) ->
186       [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
187          X.xml_cdata ("<!DOCTYPE Definition SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
188          X.xml_nempty "Definition"
189           (["name", id ; "id",xid] @
190            match params with
191               C.Possible _ -> raise ImpossiblePossible
192               (*CSC params are kept in inverted order in the internal *)
193               (* representation (the order of application)            *)
194             | C.Actual fv' -> ["params",(encode (List.rev fv'))])
195           [< X.xml_nempty "body" [] (print_term curi te) ;
196              X.xml_nempty "type"  [] (print_term curi ty) >]
197       >]
198    | C.AAxiom (xid, id, ty, params) ->
199       [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
200          X.xml_cdata ("<!DOCTYPE Axiom SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
201          X.xml_nempty "Axiom"
202           (*CSC params are kept in inverted order in the internal *)
203           (* representation (the order of application)            *)
204           ["name",id ; "params",(encode (List.rev params)) ; "id",xid]
205           [< X.xml_nempty "type" [] (print_term curi ty) >]
206       >]
207    | C.AVariable (xid, name, bo, ty) ->
208       [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
209          X.xml_cdata ("<!DOCTYPE Variable SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
210          X.xml_nempty "Variable" ["name",name ; "id",xid]
211           [< (match bo with
212                  None -> [<>]
213                | Some bo -> X.xml_nempty "body" [] (print_term curi bo)
214              ) ;
215              X.xml_nempty "type" [] (print_term curi ty)
216           >]
217       >]
218    | C.ACurrentProof (xid, name, conjs, bo, ty) ->
219       [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
220          X.xml_cdata ("<!DOCTYPE CurrentProof SYSTEM \"" ^ dtdname ^ "\">\n\n");
221          X.xml_nempty "CurrentProof" ["name",name ; "id",xid]
222           [< List.fold_right
223               (fun (j,t) i ->
224                 [< X.xml_nempty "Conjecture" ["no",(string_of_int j)]
225                     [< print_term curi t >] ; i >])
226               conjs [<>] ;
227              X.xml_nempty "body" [] [< print_term curi bo >] ;
228              X.xml_nempty "type" [] [< print_term curi ty >]
229           >]
230       >]
231    | C.AInductiveDefinition (xid, tys, params, paramsno) ->
232       let names =
233        List.map
234         (fun (typename,_,_,_) -> typename)
235         tys
236       in
237        [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
238           X.xml_cdata ("<!DOCTYPE InductiveDefinition SYSTEM \"" ^
239            dtdname ^ "\">\n\n") ;
240           X.xml_nempty "InductiveDefinition"
241            (*CSC params are kept in inverted order in the internal *)
242            (* representation (the order of application)            *)
243            ["noParams",string_of_int paramsno ;
244             "params",(encode (List.rev params)) ;
245             "id",xid]
246           [< List.fold_right
247               (fun x i -> [< print_mutual_inductive_type curi x ; i >])
248               tys [< >]
249            >]
250        >]
251 ;;