]> matita.cs.unibo.it Git - helm.git/blob - helm/interface/cic2Xml.ml
Main code clean-up.
[helm.git] / helm / interface / 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 exception BinderNotSpecified;;
32
33 let dtdname = "http://localhost:8081/getdtd?url=cic.dtd";;
34
35 (*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
36 let print_term curi =
37  let rec aux =
38   let module C = Cic in
39   let module X = Xml in
40   let module U = UriManager in
41     function
42        C.ARel (id,_,n,Some b) ->
43         X.xml_empty "REL" ["value",(string_of_int n);"binder",b;"id",id]
44      | C.ARel _ -> raise BinderNotSpecified
45      | C.AVar (id,_,uri) ->
46         let vdepth = U.depth_of_uri uri
47         and cdepth = U.depth_of_uri curi in
48          X.xml_empty "VAR"
49           ["relUri",(string_of_int (cdepth - vdepth)) ^ "," ^
50             (U.name_of_uri uri) ;
51            "id",id]
52      | C.AMeta (id,_,n) ->
53         X.xml_empty "META" ["no",(string_of_int n) ; "id",id]
54      | C.ASort (id,_,s) ->
55         let string_of_sort =
56          function
57             C.Prop -> "Prop"
58           | C.Set  -> "Set"
59           | C.Type -> "Type"
60         in
61          X.xml_empty "SORT" ["value",(string_of_sort s) ; "id",id]
62      | C.AImplicit _ -> raise NotImplemented
63      | C.AProd (id,_,C.Anonimous,s,t) ->
64         X.xml_nempty "PROD" ["id",id]
65          [< X.xml_nempty "source" [] (aux s) ;
66             X.xml_nempty "target" [] (aux t)
67          >]
68      | C.AProd (xid,_,C.Name id,s,t) ->
69        X.xml_nempty "PROD" ["id",xid]
70         [< X.xml_nempty "source" [] (aux s) ;
71            X.xml_nempty "target" ["binder",id] (aux t)
72         >]
73      | C.ACast (id,_,v,t) ->
74         X.xml_nempty "CAST" ["id",id]
75          [< X.xml_nempty "term" [] (aux v) ;
76             X.xml_nempty "type" [] (aux t)
77          >]
78      | C.ALambda (id,_,C.Anonimous,s,t) ->
79         X.xml_nempty "LAMBDA" ["id",id]
80          [< X.xml_nempty "source" [] (aux s) ;
81             X.xml_nempty "target" [] (aux t)
82          >]
83      | C.ALambda (xid,_,C.Name id,s,t) ->
84        X.xml_nempty "LAMBDA" ["id",xid]
85         [< X.xml_nempty "source" [] (aux s) ;
86            X.xml_nempty "target" ["binder",id] (aux t)
87         >]
88      | C.ALetIn (xid,_,C.Anonimous,s,t) ->
89        assert false (*CSC: significa che e' sbagliato il tipo di LetIn!!!*)
90      | C.ALetIn (xid,_,C.Name id,s,t) ->
91        X.xml_nempty "LETIN" ["id",xid]
92         [< X.xml_nempty "term" [] (aux s) ;
93            X.xml_nempty "letintarget" ["binder",id] (aux t)
94         >]
95      | C.AAppl (id,_,li) ->
96         X.xml_nempty "APPLY" ["id",id]
97          [< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>])
98          >]
99      | C.AConst (id,_,uri,_) ->
100         X.xml_empty "CONST" ["uri", (U.string_of_uri uri) ; "id",id]
101      | C.AAbst (id,_,uri) -> raise NotImplemented
102      | C.AMutInd (id,_,uri,_,i) ->
103         X.xml_empty "MUTIND"
104          ["uri", (U.string_of_uri uri) ;
105           "noType",(string_of_int i) ;
106           "id",id]
107      | C.AMutConstruct (id,_,uri,_,i,j) ->
108         X.xml_empty "MUTCONSTRUCT"
109          ["uri", (U.string_of_uri uri) ;
110           "noType",(string_of_int i) ; "noConstr",(string_of_int j) ;
111           "id",id]
112      | C.AMutCase (id,_,uri,_,typeno,ty,te,patterns) ->
113         X.xml_nempty "MUTCASE"
114          ["uriType",(U.string_of_uri uri) ;
115           "noType", (string_of_int typeno) ;
116           "id", id]
117          [< X.xml_nempty "patternsType" [] [< (aux ty) >] ;
118             X.xml_nempty "inductiveTerm" [] [< (aux te) >] ;
119             List.fold_right
120              (fun x i -> [< X.xml_nempty "pattern" [] [< aux x >] ; i>])
121              patterns [<>]
122          >]
123      | C.AFix (id, _, no, funs) ->
124        X.xml_nempty "FIX" ["noFun", (string_of_int no) ; "id",id]
125         [< List.fold_right
126             (fun (fi,ai,ti,bi) i ->
127               [< X.xml_nempty "FixFunction"
128                   ["name", fi; "recIndex", (string_of_int ai)]
129                   [< X.xml_nempty "type" [] [< aux ti >] ;
130                      X.xml_nempty "body" [] [< aux bi >]
131                   >] ;
132                  i
133               >]
134             ) funs [<>]
135         >]
136      | C.ACoFix (id,_,no,funs) ->
137        X.xml_nempty "COFIX" ["noFun", (string_of_int no) ; "id",id]
138         [< List.fold_right
139             (fun (fi,ti,bi) i ->
140               [< X.xml_nempty "CofixFunction" ["name", fi]
141                   [< X.xml_nempty "type" [] [< aux ti >] ;
142                      X.xml_nempty "body" [] [< aux bi >]
143                   >] ;
144                  i
145               >]
146             ) funs [<>]
147         >]
148  in
149   aux
150 ;;
151
152 let encode params =
153  List.fold_right
154   (fun (n,l) i ->
155     match l with
156        [] -> i
157      | _ ->
158        string_of_int n ^ ": " ^ 
159        String.concat " " (List.map UriManager.name_of_uri l) ^
160        i
161   ) params ""
162 ;;
163
164 let print_mutual_inductive_type curi (typename,inductive,arity,constructors) =
165  let module C = Cic in
166  let module X = Xml in
167   [< X.xml_nempty "InductiveType"
168       ["name",typename ;
169        "inductive",(string_of_bool inductive)
170       ]
171       [< X.xml_nempty "arity" [] (print_term curi arity) ;
172          (List.fold_right
173           (fun (name,ty,_) i ->
174             [< X.xml_nempty "Constructor" ["name",name]
175                 (print_term curi ty) ;
176                i
177             >])
178           constructors
179           [<>]
180          )
181       >]
182   >]
183 ;;
184
185 let pp obj curi =
186  let module C = Cic in
187  let module X = Xml in
188   match obj with
189      C.ADefinition (xid, _, id, te, ty, params) ->
190       [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
191          X.xml_cdata ("<!DOCTYPE Definition SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
192          X.xml_nempty "Definition"
193           (["name", id ; "id",xid] @
194            match params with
195               C.Possible _ -> raise ImpossiblePossible
196               (*CSC params are kept in inverted order in the internal *)
197               (* representation (the order of application)            *)
198             | C.Actual fv' -> ["params",(encode (List.rev fv'))])
199           [< X.xml_nempty "body" [] (print_term curi te) ;
200              X.xml_nempty "type"  [] (print_term curi ty) >]
201       >]
202    | C.AAxiom (xid, _, id, ty, params) ->
203       [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
204          X.xml_cdata ("<!DOCTYPE Axiom SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
205          X.xml_nempty "Axiom"
206           (*CSC params are kept in inverted order in the internal *)
207           (* representation (the order of application)            *)
208           ["name",id ; "params",(encode (List.rev params)) ; "id",xid]
209           [< X.xml_nempty "type" [] (print_term curi ty) >]
210       >]
211    | C.AVariable (xid, _, name, bo, ty) ->
212       [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
213          X.xml_cdata ("<!DOCTYPE Variable SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
214          X.xml_nempty "Variable" ["name",name ; "id",xid]
215           [< (match bo with
216                  None -> [<>]
217                | Some bo -> X.xml_nempty "body" [] (print_term curi bo)
218              ) ;
219              X.xml_nempty "type" [] (print_term curi ty)
220           >]
221       >]
222    | C.ACurrentProof (xid, _, name, conjs, bo, ty) ->
223       [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
224          X.xml_cdata ("<!DOCTYPE CurrentProof SYSTEM \"" ^ dtdname ^ "\">\n\n");
225          X.xml_nempty "CurrentProof" ["name",name ; "id",xid]
226           [< List.fold_right
227               (fun (j,t) i ->
228                 [< X.xml_nempty "Conjecture" ["no",(string_of_int j)]
229                     [< print_term curi t >] ; i >])
230               conjs [<>] ;
231              X.xml_nempty "body" [] [< print_term curi bo >] ;
232              X.xml_nempty "type" [] [< print_term curi ty >]
233           >]
234       >]
235    | C.AInductiveDefinition (xid, _, tys, params, paramsno) ->
236       let names =
237        List.map
238         (fun (typename,_,_,_) -> typename)
239         tys
240       in
241        [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
242           X.xml_cdata ("<!DOCTYPE InductiveDefinition SYSTEM \"" ^
243            dtdname ^ "\">\n\n") ;
244           X.xml_nempty "InductiveDefinition"
245            (*CSC params are kept in inverted order in the internal *)
246            (* representation (the order of application)            *)
247            ["noParams",string_of_int paramsno ;
248             "params",(encode (List.rev params)) ;
249             "id",xid]
250           [< List.fold_right
251               (fun x i -> [< print_mutual_inductive_type curi x ; i >])
252               tys [< >]
253            >]
254        >]
255 ;;