1 (* Copyright (C) 2000, HELM Team.
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.
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.
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.
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,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 (**************************************************************************)
30 (* Andrea Asperti <asperti@cs.unibo.it> *)
33 (**************************************************************************)
36 (* the type cexpr is inspired by OpenMath. A few primitive constructors
37 have been added, in order to take into account some special features
38 of functional expressions. Most notably: case, let in, let rec, and
39 explicit substitutons *)
42 Symbol of string option * string * subst option * string option
43 (* h:xref, name, subst, definitionURL *)
44 | LocalVar of (string option) * string (* h:xref, name *)
45 | Meta of string option * string * meta_subst (* h:xref, name, meta_subst *)
46 | Num of string option * string (* h:xref, value *)
47 | Appl of string option * cexpr list (* h:xref, args *)
48 | Binder of string option * string * decl * cexpr
49 (* h:xref, name, decl, body *)
50 | Letin of string option * def * cexpr (* h:xref, def, body *)
51 | Letrec of string option * def list * cexpr (* h:xref, def list, body *)
52 | Case of string option * cexpr * ((string * cexpr) list)
53 (* h:xref, case_expr, named-pattern list *)
56 decl = string * cexpr (* name, type *)
58 def = string * cexpr (* name, body *)
60 subst = (UriManager.uri * cexpr) list
62 meta_subst = cexpr option list
67 let symbol_table = Hashtbl.create 503;;
70 Hashtbl.add symbol_table "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)"
71 (fun aid sid args acic2cexpr ->
73 (Some aid, (Symbol (Some sid, "eq",
74 None, Some "cic:/Coq/Init/Logic/eq.ind"))
75 :: List.map acic2cexpr (List.tl args)));;
77 Hashtbl.add symbol_table "cic:/Coq/Init/Logic_Type/eqT.ind#xpointer(1/1)"
78 (fun aid sid args acic2cexpr ->
80 (Some aid, (Symbol (Some sid, "eq",
81 None, Some "cic:/Coq/Init/Logic_Type/eqT.ind"))
82 :: List.map acic2cexpr (List.tl args)));;
85 Hashtbl.add symbol_table "cic:/Coq/Init/Logic/and.ind#xpointer(1/1)"
86 (fun aid sid args acic2cexpr ->
88 (Some aid, (Symbol (Some sid, "and",
89 None, Some "cic:/Coq/Init/Logic/and.ind"))
90 :: List.map acic2cexpr args));;
93 Hashtbl.add symbol_table "cic:/Coq/Init/Logic/or.ind#xpointer(1/1)"
94 (fun aid sid args acic2cexpr ->
96 (Some aid, (Symbol (Some sid, "or",
97 None, Some "cic:/Coq/Init/Logic/or.ind"))
98 :: List.map acic2cexpr args));;
101 Hashtbl.add symbol_table "cic:/Coq/Init/Logic/iff.con"
102 (fun aid sid args acic2cexpr ->
104 (Some aid, (Symbol (Some sid, "iff",
105 None, Some "cic:/Coq/Init/Logic/iff.con"))
106 :: List.map acic2cexpr args));;
109 Hashtbl.add symbol_table "cic:/Coq/Init/Logic/not.con"
110 (fun aid sid args acic2cexpr ->
112 (Some aid, (Symbol (Some sid, "not",
113 None, Some "cic:/Coq/Init/Logic/not.con"))
114 :: List.map acic2cexpr args));;
117 Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rinv.con"
118 (fun aid sid args acic2cexpr ->
120 (Some aid, (Symbol (Some sid, "inv",
121 None, Some "cic:/Coq/Reals/Rdefinitions/Rinv.con"))
122 :: List.map acic2cexpr args));;
125 Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Ropp.con"
126 (fun aid sid args acic2cexpr ->
128 (Some aid, (Symbol (Some sid, "opp",
129 None, Some "cic:/Coq/Reals/Rdefinitions/Rinv.con"))
130 :: List.map acic2cexpr args));;
133 Hashtbl.add symbol_table "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1)"
134 (fun aid sid args acic2cexpr ->
135 match (List.tl args) with
136 [Cic.ALambda (_,Cic.Name n,s,t)] ->
138 (Some aid, "Exists", (n,acic2cexpr s),acic2cexpr t)
139 | _ -> raise Not_found);;
141 Hashtbl.add symbol_table "cic:/Coq/Init/Logic_Type/exT.ind#xpointer(1/1)"
142 (fun aid sid args acic2cexpr ->
143 match (List.tl args) with
144 [Cic.ALambda (_,Cic.Name n,s,t)] ->
146 (Some aid, "Exists", (n,acic2cexpr s),acic2cexpr t)
147 | _ -> raise Not_found);;
150 Hashtbl.add symbol_table "cic:/Coq/Init/Peano/le.ind#xpointer(1/1)"
151 (fun aid sid args acic2cexpr ->
153 (Some aid, (Symbol (Some sid, "leq",
154 None, Some "cic:/Coq/Init/Peano/le.ind"))
155 :: List.map acic2cexpr args));;
157 Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rle.con"
158 (fun aid sid args acic2cexpr ->
160 (Some aid, (Symbol (Some sid, "leq",
161 None, Some "cic:/Coq/Reals/Rdefinitions/Rle.con"))
162 :: List.map acic2cexpr args));;
165 Hashtbl.add symbol_table "cic:/Coq/Init/Peano/lt.con"
166 (fun aid sid args acic2cexpr ->
168 (Some aid, (Symbol (Some sid, "lt",
169 None, Some "cic:/Coq/Init/Peano/lt.con"))
170 :: List.map acic2cexpr args));;
172 Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rlt.con"
173 (fun aid sid args acic2cexpr ->
175 (Some aid, (Symbol (Some sid, "lt",
176 None, Some "cic:/Coq/Reals/Rdefinitions/Rlt.con"))
177 :: List.map acic2cexpr args));;
180 Hashtbl.add symbol_table "cic:/Coq/Init/Peano/ge.con"
181 (fun aid sid args acic2cexpr ->
183 (Some aid, (Symbol (Some sid, "geq",
184 None, Some "cic:/Coq/Init/Peano/ge.con"))
185 :: List.map acic2cexpr args));;
187 Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rge.con"
188 (fun aid sid args acic2cexpr ->
190 (Some aid, (Symbol (Some sid, "geq",
191 None, Some "cic:/Coq/Reals/Rdefinitions/Rge.con"))
192 :: List.map acic2cexpr args));;
195 Hashtbl.add symbol_table "cic:/Coq/Init/Peano/gt.con"
196 (fun aid sid args acic2cexpr ->
198 (Some aid, (Symbol (Some sid, "gt",
199 None, Some "cic:/Coq/Init/Peano/gt.con"))
200 :: List.map acic2cexpr args));;
202 Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rgt.con"
203 (fun aid sid args acic2cexpr ->
205 (Some aid, (Symbol (Some sid, "gt",
206 None, Some "cic:/Coq/Reals/Rdefinitions/Rgt.con"))
207 :: List.map acic2cexpr args));;
210 Hashtbl.add symbol_table "cic:/Coq/Init/Peano/plus.con"
211 (fun aid sid args acic2cexpr ->
213 (Some aid, (Symbol (Some sid, "plus",
214 None, Some "cic:/Coq/Init/Peano/plus.con"))
215 :: List.map acic2cexpr args));;
217 Hashtbl.add symbol_table "cic:/Coq/ZArith/fast_integer/Zplus.con"
218 (fun aid sid args acic2cexpr ->
220 (Some aid, (Symbol (Some sid, "plus",
221 None, Some "cic:/Coq/ZArith/fast_integer/Zplus.con"))
222 :: List.map acic2cexpr args));;
225 UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rplus.con" ;;
226 let r0_uri = UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R0.con" ;;
227 let r1_uri = UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R1.con" ;;
229 Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rplus.con"
230 (fun aid sid args acic2cexpr ->
233 (Some aid, (Symbol (Some sid, "plus",
234 None, Some "cic:/Coq/Reals/Rdefinitions/Rplus.con"))
235 :: List.map acic2cexpr args)
237 let rec aux acc = function
238 | [ Cic.AConst (nid, uri, []); n] when
239 UriManager.eq uri r1_uri ->
241 | Cic.AConst (_, uri, []) when UriManager.eq uri r1_uri ->
242 Num (Some aid, string_of_int (acc + 2))
243 | Cic.AAppl (_, Cic.AConst (_, uri, []) :: args) when
244 UriManager.eq uri rplus_uri ->
254 Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/R0.con"
255 (fun aid sid args acic2cexpr -> Num (Some sid, "0")) ;;
257 Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/R1.con"
258 (fun aid sid args acic2cexpr -> Num (Some sid, "1")) ;;
261 Hashtbl.add symbol_table "cic:/Coq/Init/Peano/mult.con"
262 (fun aid sid args acic2cexpr ->
264 (Some aid, (Symbol (Some sid, "times",
265 None, Some "cic:/Coq/Init/Peano/mult.con"))
266 :: List.map acic2cexpr args));;
269 Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rmult.con"
270 (fun aid sid args acic2cexpr ->
272 (Some aid, (Symbol (Some sid, "times",
273 None, Some "cic:/Coq/Reals/Rdefinitions/Rmult.con"))
274 :: List.map acic2cexpr args));;
276 Hashtbl.add symbol_table "cic:/Coq/Arith/Minus/minus.con"
277 (fun aid sid args acic2cexpr ->
279 (Some aid, (Symbol (Some sid, "minus",
280 None, Some "cic:/Coq/Arith/Minus/mult.con"))
281 :: List.map acic2cexpr args));;
283 Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rminus.con"
284 (fun aid sid args acic2cexpr ->
286 (Some aid, (Symbol (Some sid, "minus",
287 None, Some "cic:/Coq/Reals/Rdefinitions/Rminus.con"))
288 :: List.map acic2cexpr args));;
291 Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rdiv.con"
292 (fun aid sid args acic2cexpr ->
294 (Some aid, (Symbol (Some sid, "div",
295 None, Some "cic:/Coq/Reals/Rdefinitions/Rdiv.con"))
296 :: List.map acic2cexpr args));;
309 | Cic.CProp -> "Type"
312 let get_constructors uri i =
313 let inductive_types =
314 (match CicEnvironment.get_obj uri with
315 Cic.Constant _ -> assert false
316 | Cic.Variable _ -> assert false
317 | Cic.CurrentProof _ -> assert false
318 | Cic.InductiveDefinition (l,_,_) -> l
320 let (_,_,_,constructors) = List.nth inductive_types i in
324 exception NotImplemented;;
326 let acic2cexpr ids_to_inner_sorts t =
327 let rec acic2cexpr t =
328 let module C = Cic in
329 let module X = Xml in
330 let module U = UriManager in
331 let module C2A = Cic2acic in
335 | l -> Some (List.map (function (uri,t) -> (uri, acic2cexpr t)) l) in
337 C.ARel (id,idref,n,b) -> LocalVar (Some id,b)
338 | C.AVar (id,uri,subst) ->
339 Symbol (Some id, UriManager.name_of_uri uri,
340 make_subst subst, Some (UriManager.string_of_uri uri))
341 | C.AMeta (id,n,l) ->
346 | Some t -> Some (acic2cexpr t)
349 Meta (Some id,("?" ^ (string_of_int n)),l')
350 | C.ASort (id,s) -> Symbol (Some id,string_of_sort s,None,None)
351 | C.AImplicit _ -> raise NotImplemented
352 | C.AProd (id,n,s,t) ->
355 Appl (Some id, [Symbol (None, "arrow",None,None);
356 acic2cexpr s; acic2cexpr t])
359 (try Hashtbl.find ids_to_inner_sorts id
361 (* if the Prod does not have the sort, it means
362 that it has been generated by cic2content, and
363 thus is a statement *)
365 let binder = if sort = "Prop" then "Forall" else "Prod" in
366 let decl = (name, acic2cexpr s) in
367 Binder (Some id,binder,decl,acic2cexpr t))
368 | C.ACast (id,v,t) -> acic2cexpr v
369 | C.ALambda (id,n,s,t) ->
373 | Cic.Name name -> name) in
374 let decl = (name, acic2cexpr s) in
375 Binder (Some id,"Lambda",decl,acic2cexpr t)
376 | C.ALetIn (id,n,s,t) ->
378 Cic.Anonymous -> assert false
380 let def = (name, acic2cexpr s) in
381 Letin (Some id,def,acic2cexpr t))
382 | C.AAppl (aid,C.AConst (sid,uri,subst)::tl) ->
383 let uri_str = UriManager.string_of_uri uri in
385 (let f = Hashtbl.find symbol_table uri_str in
386 f aid sid tl acic2cexpr)
388 Appl (Some aid, Symbol (Some sid,UriManager.name_of_uri uri,
389 make_subst subst, Some uri_str)::List.map acic2cexpr tl))
390 | C.AAppl (aid,C.AMutInd (sid,uri,i,subst)::tl) ->
391 let inductive_types =
392 (match CicEnvironment.get_obj uri with
393 Cic.Constant _ -> assert false
394 | Cic.Variable _ -> assert false
395 | Cic.CurrentProof _ -> assert false
396 | Cic.InductiveDefinition (l,_,_) -> l
398 let (name,_,_,_) = List.nth inductive_types i in
399 let uri_str = UriManager.string_of_uri uri in
401 uri_str ^ "#xpointer(1/" ^ (string_of_int (i + 1)) ^ ")" in
403 (let f = Hashtbl.find symbol_table puri_str in
404 f aid sid tl acic2cexpr)
406 Appl (Some aid, Symbol (Some sid, name,
407 make_subst subst, Some uri_str)::List.map acic2cexpr tl))
409 Appl (Some id, List.map acic2cexpr li)
410 | C.AConst (id,uri,subst) ->
411 let uri_str = UriManager.string_of_uri uri in
413 let f = Hashtbl.find symbol_table uri_str in
414 f "dummy" id [] acic2cexpr
416 Symbol (Some id, UriManager.name_of_uri uri,
417 make_subst subst, Some (UriManager.string_of_uri uri)))
418 | C.AMutInd (id,uri,i,subst) ->
419 let inductive_types =
420 (match CicEnvironment.get_obj uri with
421 Cic.Constant _ -> assert false
422 | Cic.Variable _ -> assert false
423 | Cic.CurrentProof _ -> assert false
424 | Cic.InductiveDefinition (l,_,_) -> l
426 let (name,_,_,_) = List.nth inductive_types i in
427 let uri_str = UriManager.string_of_uri uri in
428 Symbol (Some id, name, make_subst subst, Some uri_str)
429 | C.AMutConstruct (id,uri,i,j,subst) ->
430 let constructors = get_constructors uri i in
431 let (name,_) = List.nth constructors (j-1) in
432 let uri_str = UriManager.string_of_uri uri in
433 Symbol (Some id, name, make_subst subst, Some uri_str)
434 | C.AMutCase (id,uri,typeno,ty,te,patterns) ->
435 let constructors = get_constructors uri typeno in
437 List.map2 (fun c p -> (fst c, acic2cexpr p))
438 constructors patterns in
439 Case (Some id, acic2cexpr te, named_patterns)
440 | C.AFix (id, no, funs) ->
442 List.map (function (id1,n,_,_,bo) -> (n, acic2cexpr bo)) funs in
443 let (name,_) = List.nth defs no in
444 let body = LocalVar (None, name) in
445 Letrec (Some id, defs, body)
446 | C.ACoFix (id,no,funs) ->
448 List.map (function (id1,n,_,bo) -> (n, acic2cexpr bo)) funs in
449 let (name,_) = List.nth defs no in
450 let body = LocalVar (None, name) in
451 Letrec (Some id, defs, body) in