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 (* h:xref, name *)
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
65 let symbol_table = Hashtbl.create 503;;
68 Hashtbl.add symbol_table "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)"
69 (fun aid sid args acic2cexpr ->
71 (Some aid, (Symbol (Some sid, "eq",
72 None, Some "cic:/Coq/Init/Logic/eq.ind"))
73 :: List.map acic2cexpr (List.tl args)));;
75 Hashtbl.add symbol_table "cic:/Coq/Init/Logic_Type/eqT.ind#xpointer(1/1)"
76 (fun aid sid args acic2cexpr ->
78 (Some aid, (Symbol (Some sid, "eq",
79 None, Some "cic:/Coq/Init/Logic/eqT.ind"))
80 :: List.map acic2cexpr (List.tl args)));;
83 Hashtbl.add symbol_table "cic:/Coq/Init/Logic/and.ind#xpointer(1/1)"
84 (fun aid sid args acic2cexpr ->
86 (Some aid, (Symbol (Some sid, "and",
87 None, Some "cic:/Coq/Init/Logic/and.ind"))
88 :: List.map acic2cexpr args));;
91 Hashtbl.add symbol_table "cic:/Coq/Init/Logic/or.ind#xpointer(1/1)"
92 (fun aid sid args acic2cexpr ->
94 (Some aid, (Symbol (Some sid, "or",
95 None, Some "cic:/Coq/Init/Logic/or.ind"))
96 :: List.map acic2cexpr args));;
99 Hashtbl.add symbol_table "cic:/Coq/Init/Logic/iff.con"
100 (fun aid sid args acic2cexpr ->
102 (Some aid, (Symbol (Some sid, "iff",
103 None, Some "cic:/Coq/Init/Logic/iff.con"))
104 :: List.map acic2cexpr args));;
107 Hashtbl.add symbol_table "cic:/Coq/Init/Logic/not.con"
108 (fun aid sid args acic2cexpr ->
110 (Some aid, (Symbol (Some sid, "not",
111 None, Some "cic:/Coq/Init/Logic/not.con"))
112 :: List.map acic2cexpr args));;
115 Hashtbl.add symbol_table "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1)"
116 (fun aid sid args acic2cexpr ->
117 match (List.tl args) with
118 [Cic.ALambda (_,Cic.Name n,s,t)] ->
120 (Some aid, "Exists", (n,acic2cexpr s),acic2cexpr t)
121 | _ -> raise Not_found);;
123 Hashtbl.add symbol_table "cic:/Coq/Init/Logic_Type/exT.ind#xpointer(1/1)"
124 (fun aid sid args acic2cexpr ->
125 match (List.tl args) with
126 [Cic.ALambda (_,Cic.Name n,s,t)] ->
128 (Some aid, "Exists", (n,acic2cexpr s),acic2cexpr t)
129 | _ -> raise Not_found);;
132 Hashtbl.add symbol_table "cic:/Coq/Init/Peano/le.ind#xpointer(1/1)"
133 (fun aid sid args acic2cexpr ->
135 (Some aid, (Symbol (Some sid, "leq",
136 None, Some "cic:/Coq/Init/Peano/le.ind"))
137 :: List.map acic2cexpr args));;
139 Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rle.con"
140 (fun aid sid args acic2cexpr ->
142 (Some aid, (Symbol (Some sid, "leq",
143 None, Some "cic:/Coq/Reals/Rdefinitions/Rle.con"))
144 :: List.map acic2cexpr args));;
147 Hashtbl.add symbol_table "cic:/Coq/Init/Peano/lt.con"
148 (fun aid sid args acic2cexpr ->
150 (Some aid, (Symbol (Some sid, "lt",
151 None, Some "cic:/Coq/Init/Peano/lt.con"))
152 :: List.map acic2cexpr args));;
154 Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rlt.con"
155 (fun aid sid args acic2cexpr ->
157 (Some aid, (Symbol (Some sid, "lt",
158 None, Some "cic:/Coq/Reals/Rdefinitions/Rlt.con"))
159 :: List.map acic2cexpr args));;
162 Hashtbl.add symbol_table "cic:/Coq/Init/Peano/ge.con"
163 (fun aid sid args acic2cexpr ->
165 (Some aid, (Symbol (Some sid, "geq",
166 None, Some "cic:/Coq/Init/Peano/ge.con"))
167 :: List.map acic2cexpr args));;
169 Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rge.con"
170 (fun aid sid args acic2cexpr ->
172 (Some aid, (Symbol (Some sid, "geq",
173 None, Some "cic:/Coq/Reals/Rdefinitions/Rge.con"))
174 :: List.map acic2cexpr args));;
177 Hashtbl.add symbol_table "cic:/Coq/Init/Peano/gt.con"
178 (fun aid sid args acic2cexpr ->
180 (Some aid, (Symbol (Some sid, "gt",
181 None, Some "cic:/Coq/Init/Peano/gt.con"))
182 :: List.map acic2cexpr args));;
184 Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rgt.con"
185 (fun aid sid args acic2cexpr ->
187 (Some aid, (Symbol (Some sid, "gt",
188 None, Some "cic:/Coq/Reals/Rdefinitions/Rgt.con"))
189 :: List.map acic2cexpr args));;
192 Hashtbl.add symbol_table "cic:/Coq/Init/Peano/plus.con"
193 (fun aid sid args acic2cexpr ->
195 (Some aid, (Symbol (Some sid, "plus",
196 None, Some "cic:/Coq/Init/Peano/plus.con"))
197 :: List.map acic2cexpr args));;
199 Hashtbl.add symbol_table "cic:/Coq/ZArith/fast_integer/Zplus.con"
200 (fun aid sid args acic2cexpr ->
202 (Some aid, (Symbol (Some sid, "plus",
203 None, Some "cic:/Coq/ZArith/fast_integer/Zplus.con"))
204 :: List.map acic2cexpr args));;
206 Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rplus.con"
207 (fun aid sid args acic2cexpr ->
209 (Some aid, (Symbol (Some sid, "plus",
210 None, Some "cic:/Coq/Reals/Rdefinitions/Rplus.con"))
211 :: List.map acic2cexpr args));;
214 Hashtbl.add symbol_table "cic:/Coq/Init/Peano/mult.con"
215 (fun aid sid args acic2cexpr ->
217 (Some aid, (Symbol (Some sid, "times",
218 None, Some "cic:/Coq/Init/Peano/mult.con"))
219 :: List.map acic2cexpr args));;
222 Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rmult.con"
223 (fun aid sid args acic2cexpr ->
225 (Some aid, (Symbol (Some sid, "times",
226 None, Some "cic:/Coq/Reals/Rdefinitions/Rmult.con"))
227 :: List.map acic2cexpr args));;
229 Hashtbl.add symbol_table "cic:/Coq/Arith/Minus/minus.con"
230 (fun aid sid args acic2cexpr ->
232 (Some aid, (Symbol (Some sid, "minus",
233 None, Some "cic:/Coq/Arith/Minus/mult.con"))
234 :: List.map acic2cexpr args));;
249 let get_constructors uri i =
250 let inductive_types =
251 (match CicEnvironment.get_obj uri with
252 Cic.Constant _ -> assert false
253 | Cic.Variable _ -> assert false
254 | Cic.CurrentProof _ -> assert false
255 | Cic.InductiveDefinition (l,_,_) -> l
257 let (_,_,_,constructors) = List.nth inductive_types i in
261 exception NotImplemented;;
263 let acic2cexpr ids_to_inner_sorts t =
264 let rec acic2cexpr t =
265 let module C = Cic in
266 let module X = Xml in
267 let module U = UriManager in
268 let module C2A = Cic2acic in
272 | l -> Some (List.map (function (uri,t) -> (uri, acic2cexpr t)) l) in
274 C.ARel (id,idref,n,b) -> LocalVar (Some id,b)
275 | C.AVar (id,uri,subst) ->
276 Symbol (Some id, UriManager.name_of_uri uri,
277 make_subst subst, Some (UriManager.string_of_uri uri))
278 | C.AMeta (id,n,l) -> Meta (Some id,("?" ^ (string_of_int n)))
279 | C.ASort (id,s) -> Symbol (Some id,string_of_sort s,None,None)
280 | C.AImplicit _ -> raise NotImplemented
281 | C.AProd (id,n,s,t) ->
284 Appl (Some id, [Symbol (None, "arrow",None,None);
285 acic2cexpr s; acic2cexpr t])
288 (try Hashtbl.find ids_to_inner_sorts id
290 (* if the Prod does not have the sort, it means
291 that it has been generated by cic2content, and
292 thus is a statement *)
294 let binder = if sort = "Prop" then "Forall" else "Prod" in
295 let decl = (name, acic2cexpr s) in
296 Binder (Some id,binder,decl,acic2cexpr t))
297 | C.ACast (id,v,t) -> acic2cexpr v
298 | C.ALambda (id,n,s,t) ->
302 | Cic.Name name -> name) in
303 let decl = (name, acic2cexpr s) in
304 Binder (Some id,"Lambda",decl,acic2cexpr t)
305 | C.ALetIn (id,n,s,t) ->
307 Cic.Anonymous -> assert false
309 let def = (name, acic2cexpr s) in
310 Letin (Some id,def,acic2cexpr t))
311 | C.AAppl (aid,C.AConst (sid,uri,subst)::tl) ->
312 let uri_str = UriManager.string_of_uri uri in
314 (let f = Hashtbl.find symbol_table uri_str in
315 f aid sid tl acic2cexpr)
317 Appl (Some aid, Symbol (Some sid,UriManager.name_of_uri uri,
318 make_subst subst, Some uri_str)::List.map acic2cexpr tl))
319 | C.AAppl (aid,C.AMutInd (sid,uri,i,subst)::tl) ->
320 let inductive_types =
321 (match CicEnvironment.get_obj uri with
322 Cic.Constant _ -> assert false
323 | Cic.Variable _ -> assert false
324 | Cic.CurrentProof _ -> assert false
325 | Cic.InductiveDefinition (l,_,_) -> l
327 let (name,_,_,_) = List.nth inductive_types i in
328 let uri_str = UriManager.string_of_uri uri in
330 uri_str ^ "#xpointer(1/" ^ (string_of_int (i + 1)) ^ ")" in
332 (let f = Hashtbl.find symbol_table puri_str in
333 f aid sid tl acic2cexpr)
335 Appl (Some aid, Symbol (Some sid, name,
336 make_subst subst, Some uri_str)::List.map acic2cexpr tl))
338 Appl (Some id, List.map acic2cexpr li)
339 | C.AConst (id,uri,subst) ->
340 Symbol (Some id, UriManager.name_of_uri uri,
341 make_subst subst, Some (UriManager.string_of_uri uri))
342 | C.AMutInd (id,uri,i,subst) ->
343 let inductive_types =
344 (match CicEnvironment.get_obj uri with
345 Cic.Constant _ -> assert false
346 | Cic.Variable _ -> assert false
347 | Cic.CurrentProof _ -> assert false
348 | Cic.InductiveDefinition (l,_,_) -> l
350 let (name,_,_,_) = List.nth inductive_types i in
351 let uri_str = UriManager.string_of_uri uri in
352 Symbol (Some id, name, make_subst subst, Some uri_str)
353 | C.AMutConstruct (id,uri,i,j,subst) ->
354 let constructors = get_constructors uri i in
355 let (name,_) = List.nth constructors (j-1) in
356 let uri_str = UriManager.string_of_uri uri in
357 Symbol (Some id, name, make_subst subst, Some uri_str)
358 | C.AMutCase (id,uri,typeno,ty,te,patterns) ->
359 let constructors = get_constructors uri typeno in
361 List.map2 (fun c p -> (fst c, acic2cexpr p))
362 constructors patterns in
363 Case (Some id, acic2cexpr te, named_patterns)
364 | C.AFix (id, no, funs) ->
366 List.map (function (id1,n,_,_,bo) -> (n, acic2cexpr bo)) funs in
367 let (name,_) = List.nth defs no in
368 let body = LocalVar (None, name) in
369 Letrec (Some id, defs, body)
370 | C.ACoFix (id,no,funs) ->
372 List.map (function (id1,n,_,bo) -> (n, acic2cexpr bo)) funs in
373 let (name,_) = List.nth defs no in
374 let body = LocalVar (None, name) in
375 Letrec (Some id, defs, body) in