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