]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/cic_transformations/content_expressions.ml
snapshot
[helm.git] / helm / ocaml / cic_transformations / content_expressions.ml
1 (* Copyright (C) 2000, HELM Team.
2  * 
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.
6  * 
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.
11  * 
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.
16  *
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,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://cs.unibo.it/helm/.
24  *)
25
26 (**************************************************************************)
27 (*                                                                        *)
28 (*                           PROJECT HELM                                 *)
29 (*                                                                        *)
30 (*                Andrea Asperti <asperti@cs.unibo.it>                    *)
31 (*                             27/6/2003                                   *)
32 (*                                                                        *)
33 (**************************************************************************)
34
35
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 substitutions *)
40
41 type cexpr =
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 *)
54
55 and 
56   decl = string * cexpr               (* name, type *)
57 and
58   def = string * cexpr               (* name, body *)
59 and
60   subst = (UriManager.uri * cexpr) list
61 and
62   meta_subst = cexpr option list
63 ;;
64
65 (* NOTATION *)
66
67 let symbol_table = Hashtbl.create 503;;
68
69 (* eq *)
70 Hashtbl.add symbol_table HelmLibraryObjects.Logic.eq_XURI
71   (fun aid sid args acic2cexpr ->
72    Appl 
73     (Some aid, (Symbol (Some sid, "eq",
74           None, Some HelmLibraryObjects.Logic.eq_SURI))
75      :: List.map acic2cexpr (List.tl args)));;   
76
77 (* and *)
78 Hashtbl.add symbol_table HelmLibraryObjects.Logic.and_XURI 
79   (fun aid sid args acic2cexpr ->
80    Appl 
81     (Some aid, (Symbol (Some sid, "and",
82           None, Some HelmLibraryObjects.Logic.and_SURI))
83      :: List.map acic2cexpr args));;
84
85 (* or *)
86 Hashtbl.add symbol_table HelmLibraryObjects.Logic.or_XURI 
87   (fun aid sid args acic2cexpr ->
88    Appl 
89     (Some aid, (Symbol (Some sid, "or",
90           None, Some HelmLibraryObjects.Logic.or_SURI))
91      :: List.map acic2cexpr args));;
92
93 (* iff *)
94 Hashtbl.add symbol_table HelmLibraryObjects.Logic.iff_SURI
95   (fun aid sid args acic2cexpr ->
96    Appl 
97     (Some aid, (Symbol (Some sid, "iff",
98           None, Some HelmLibraryObjects.Logic.iff_SURI))
99      :: List.map acic2cexpr args));;
100
101 (* not *)
102 Hashtbl.add symbol_table HelmLibraryObjects.Logic.not_SURI
103   (fun aid sid args acic2cexpr ->
104    Appl 
105     (Some aid, (Symbol (Some sid, "not",
106           None, Some HelmLibraryObjects.Logic.not_SURI))
107      :: List.map acic2cexpr args));;
108
109 (* Rinv *)
110 Hashtbl.add symbol_table HelmLibraryObjects.Reals.rinv_SURI
111   (fun aid sid args acic2cexpr ->
112    Appl 
113     (Some aid, (Symbol (Some sid, "inv",
114           None, Some HelmLibraryObjects.Reals.rinv_SURI))
115      :: List.map acic2cexpr args));;
116
117 (* Ropp *)
118 Hashtbl.add symbol_table HelmLibraryObjects.Reals.ropp_SURI
119   (fun aid sid args acic2cexpr ->
120    Appl 
121     (Some aid, (Symbol (Some sid, "opp",
122           None, Some HelmLibraryObjects.Reals.ropp_SURI))
123      :: List.map acic2cexpr args));;
124
125 (* exists *)
126 Hashtbl.add symbol_table HelmLibraryObjects.Logic.ex_XURI 
127   (fun aid sid args acic2cexpr ->
128    match (List.tl args) with
129      [Cic.ALambda (_,Cic.Name n,s,t)] ->
130        Binder 
131         (Some aid, "Exists", (n,acic2cexpr s),acic2cexpr t)
132   | _ -> raise Not_found);;
133
134 (* leq *) 
135 Hashtbl.add symbol_table HelmLibraryObjects.Peano.le_XURI
136   (fun aid sid args acic2cexpr ->
137    Appl
138     (Some aid, (Symbol (Some sid, "leq",
139           None, Some HelmLibraryObjects.Peano.le_SURI))
140      :: List.map acic2cexpr args));;
141
142 Hashtbl.add symbol_table HelmLibraryObjects.Reals.rle_SURI
143   (fun aid sid args acic2cexpr ->
144    Appl 
145     (Some aid, (Symbol (Some sid, "leq",
146           None, Some HelmLibraryObjects.Reals.rle_SURI))
147      :: List.map acic2cexpr args));;
148
149 (* lt *)
150 Hashtbl.add symbol_table HelmLibraryObjects.Peano.lt_SURI
151   (fun aid sid args acic2cexpr ->
152    Appl 
153     (Some aid, (Symbol (Some sid, "lt",
154           None, Some HelmLibraryObjects.Peano.lt_SURI))
155      :: List.map acic2cexpr args));;
156
157 Hashtbl.add symbol_table HelmLibraryObjects.Reals.rlt_SURI
158   (fun aid sid args acic2cexpr ->
159    Appl 
160     (Some aid, (Symbol (Some sid, "lt",
161           None, Some HelmLibraryObjects.Reals.rlt_SURI))
162      :: List.map acic2cexpr args));;
163
164 (* geq *)
165 Hashtbl.add symbol_table HelmLibraryObjects.Peano.ge_SURI
166   (fun aid sid args acic2cexpr ->
167    Appl 
168     (Some aid, (Symbol (Some sid, "geq",
169           None, Some HelmLibraryObjects.Peano.ge_SURI))
170      :: List.map acic2cexpr args));;
171
172 Hashtbl.add symbol_table HelmLibraryObjects.Reals.rge_SURI
173   (fun aid sid args acic2cexpr ->
174    Appl 
175     (Some aid, (Symbol (Some sid, "geq",
176           None, Some HelmLibraryObjects.Reals.rge_SURI))
177      :: List.map acic2cexpr args));;
178
179 (* gt *)
180 Hashtbl.add symbol_table HelmLibraryObjects.Peano.gt_SURI
181   (fun aid sid args acic2cexpr ->
182    Appl 
183     (Some aid, (Symbol (Some sid, "gt",
184           None, Some HelmLibraryObjects.Peano.gt_SURI))
185      :: List.map acic2cexpr args));;
186
187 Hashtbl.add symbol_table HelmLibraryObjects.Reals.rgt_SURI
188   (fun aid sid args acic2cexpr ->
189    Appl 
190     (Some aid, (Symbol (Some sid, "gt",
191           None, Some HelmLibraryObjects.Reals.rgt_SURI))
192      :: List.map acic2cexpr args));;
193
194 (* plus *)
195 Hashtbl.add symbol_table HelmLibraryObjects.Peano.plus_SURI
196   (fun aid sid args acic2cexpr ->
197    Appl 
198     (Some aid, (Symbol (Some sid, "plus",
199           None, Some HelmLibraryObjects.Peano.plus_SURI))
200      :: List.map acic2cexpr args));;
201
202 Hashtbl.add symbol_table HelmLibraryObjects.BinInt.zplus_SURI
203   (fun aid sid args acic2cexpr ->
204    Appl 
205     (Some aid, (Symbol (Some sid, "plus",
206           None, Some HelmLibraryObjects.BinInt.zplus_SURI))
207      :: List.map acic2cexpr args));;
208
209 Hashtbl.add symbol_table HelmLibraryObjects.Reals.rplus_SURI
210   (fun aid sid args acic2cexpr ->
211    let appl () =
212      Appl 
213       (Some aid, (Symbol (Some sid, "plus",
214             None, Some HelmLibraryObjects.Reals.rplus_SURI))
215        :: List.map acic2cexpr args)
216    in
217     let rec aux acc = function
218       | [ Cic.AConst (nid, uri, []); n] when
219           UriManager.eq uri HelmLibraryObjects.Reals.r1_URI ->
220             (match n with
221             | Cic.AConst (_, uri, []) when
222                UriManager.eq uri HelmLibraryObjects.Reals.r1_URI ->
223                 Num (Some aid, string_of_int (acc + 2))
224             | Cic.AAppl (_, Cic.AConst (_, uri, []) :: args) when
225                 UriManager.eq uri HelmLibraryObjects.Reals.rplus_URI ->
226                   aux (acc + 1) args
227             | _ -> appl ())
228       | _ -> appl ()
229     in
230     aux 0 args)
231 ;;
232
233 (* zero and one *)
234
235 Hashtbl.add symbol_table HelmLibraryObjects.Reals.r0_SURI
236   (fun aid sid args acic2cexpr -> Num (Some sid, "0")) ;;
237
238 Hashtbl.add symbol_table HelmLibraryObjects.Reals.r1_SURI
239   (fun aid sid args acic2cexpr -> Num (Some sid, "1")) ;;
240
241 (* times *) 
242 Hashtbl.add symbol_table HelmLibraryObjects.Peano.mult_SURI
243   (fun aid sid args acic2cexpr ->
244    Appl 
245     (Some aid, (Symbol (Some sid, "times",
246           None, Some HelmLibraryObjects.Peano.mult_SURI))
247      :: List.map acic2cexpr args));;
248
249
250 Hashtbl.add symbol_table HelmLibraryObjects.Reals.rmult_SURI
251   (fun aid sid args acic2cexpr ->
252    Appl 
253     (Some aid, (Symbol (Some sid, "times",
254           None, Some HelmLibraryObjects.Reals.rmult_SURI))
255      :: List.map acic2cexpr args));;
256 (* minus *)
257 Hashtbl.add symbol_table HelmLibraryObjects.Peano.minus_SURI
258   (fun aid sid args acic2cexpr ->
259    Appl 
260     (Some aid, (Symbol (Some sid, "minus",
261           None, Some HelmLibraryObjects.Peano.minus_SURI))
262      :: List.map acic2cexpr args));;
263
264 Hashtbl.add symbol_table HelmLibraryObjects.Reals.rminus_SURI
265   (fun aid sid args acic2cexpr ->
266    Appl 
267     (Some aid, (Symbol (Some sid, "minus",
268           None, Some HelmLibraryObjects.Reals.rminus_SURI))
269      :: List.map acic2cexpr args));;
270
271 (* div *)
272 Hashtbl.add symbol_table HelmLibraryObjects.Reals.rdiv_SURI
273   (fun aid sid args acic2cexpr ->
274    Appl 
275     (Some aid, (Symbol (Some sid, "div",
276           None, Some HelmLibraryObjects.Reals.rdiv_SURI))
277      :: List.map acic2cexpr args));;
278
279
280
281
282 (* END NOTATION *)
283
284  
285 let string_of_sort =
286   function 
287     Cic.Prop  -> "Prop"
288   | Cic.Set   -> "Set"
289   | Cic.Type _ -> "Type" (* TASSI *)
290   | Cic.CProp -> "Type"
291 ;;
292
293 let get_constructors uri i =
294   let inductive_types =
295     (match CicEnvironment.get_obj uri with
296          Cic.Constant _ -> assert false
297      | Cic.Variable _ -> assert false
298      | Cic.CurrentProof _ -> assert false
299      | Cic.InductiveDefinition (l,_,_) -> l 
300     ) in
301    let (_,_,_,constructors) = List.nth inductive_types i in
302    constructors
303 ;;
304
305 exception NotImplemented;;
306
307 let acic2cexpr ids_to_inner_sorts t =
308   let rec acic2cexpr t =
309     let module C = Cic in
310     let module X = Xml in
311     let module U = UriManager in
312     let module C2A = Cic2acic in
313     let make_subst = 
314       function 
315           [] -> None
316         | l -> Some (List.map (function (uri,t) -> (uri, acic2cexpr t)) l) in
317     match t with 
318       C.ARel (id,idref,n,b) -> LocalVar (Some id,b)
319     | C.AVar (id,uri,subst) ->
320         Symbol (Some id, UriManager.name_of_uri uri, 
321           make_subst subst, Some (UriManager.string_of_uri uri))
322     | C.AMeta (id,n,l) ->
323        let l' =
324         List.rev_map
325          (function
326              None -> None
327            | Some t -> Some (acic2cexpr t)
328          ) l
329        in
330         Meta (Some id,("?" ^ (string_of_int n)),l')
331     | C.ASort (id,s) -> Symbol (Some id,string_of_sort s,None,None)
332     | C.AImplicit _ -> raise NotImplemented
333     | C.AProd (id,n,s,t) ->
334         (match n with
335            Cic.Anonymous ->
336              Appl (Some id, [Symbol (None, "arrow",None,None); 
337                acic2cexpr s; acic2cexpr t])
338          | Cic.Name name -> 
339              let sort = 
340                (try Hashtbl.find ids_to_inner_sorts id 
341                 with Not_found -> 
342                    (* if the Prod does not have the sort, it means
343                       that it has been generated by cic2content, and
344                       thus is a statement *)
345                   "Prop") in
346              let binder = if sort = "Prop" then "Forall" else "Prod" in
347              let decl = (name, acic2cexpr s) in 
348              Binder (Some id,binder,decl,acic2cexpr t)) 
349     | C.ACast (id,v,t) -> acic2cexpr v
350     | C.ALambda (id,n,s,t) ->
351         let name =
352           (match n with
353              Cic.Anonymous -> "_"
354            | Cic.Name name -> name) in
355         let decl = (name, acic2cexpr s) in 
356         Binder (Some id,"Lambda",decl,acic2cexpr t)
357     | C.ALetIn (id,n,s,t) ->
358         (match n with
359            Cic.Anonymous -> assert false
360          | Cic.Name name ->
361              let def = (name, acic2cexpr s) in
362              Letin (Some id,def,acic2cexpr t))
363     | C.AAppl (aid,C.AConst (sid,uri,subst)::tl) ->
364         let uri_str = UriManager.string_of_uri uri in
365         (try 
366           (let f = Hashtbl.find symbol_table uri_str in
367            f aid sid tl acic2cexpr)
368         with Not_found ->
369           Appl (Some aid, Symbol (Some sid,UriManager.name_of_uri uri, 
370           make_subst subst, Some uri_str)::List.map acic2cexpr tl)) 
371     | C.AAppl (aid,C.AMutInd (sid,uri,i,subst)::tl) ->
372         let inductive_types = 
373           (match CicEnvironment.get_obj uri with
374              Cic.Constant _ -> assert false
375            | Cic.Variable _ -> assert false
376            | Cic.CurrentProof _ -> assert false
377            | Cic.InductiveDefinition (l,_,_) -> l 
378           ) in
379         let (name,_,_,_) = List.nth inductive_types i in
380         let uri_str = UriManager.string_of_uri uri in
381         let puri_str =
382          uri_str ^ "#xpointer(1/" ^ (string_of_int (i + 1)) ^ ")" in
383         (try 
384           (let f = Hashtbl.find symbol_table puri_str in
385            f aid sid tl acic2cexpr)
386          with Not_found ->
387            Appl (Some aid, Symbol (Some sid, name, 
388            make_subst subst, Some uri_str)::List.map acic2cexpr tl)) 
389     | C.AAppl (id,li) ->
390         Appl (Some id, List.map acic2cexpr li)
391     | C.AConst (id,uri,subst) ->
392         let uri_str = UriManager.string_of_uri uri in
393         (try
394           let f = Hashtbl.find symbol_table uri_str in
395           f "dummy" id [] acic2cexpr
396         with Not_found ->
397           Symbol (Some id, UriManager.name_of_uri uri, 
398             make_subst subst, Some (UriManager.string_of_uri uri)))
399     | C.AMutInd (id,uri,i,subst) ->
400         let inductive_types = 
401           (match CicEnvironment.get_obj uri with
402              Cic.Constant _ -> assert false
403            | Cic.Variable _ -> assert false
404            | Cic.CurrentProof _ -> assert false
405            | Cic.InductiveDefinition (l,_,_) -> l 
406           ) in
407         let (name,_,_,_) = List.nth inductive_types i in
408         let uri_str = UriManager.string_of_uri uri in
409         Symbol (Some id, name, make_subst subst, Some uri_str)
410     | C.AMutConstruct (id,uri,i,j,subst) ->
411         let constructors = get_constructors uri i in
412         let (name,_) = List.nth constructors (j-1) in
413         let uri_str = UriManager.string_of_uri uri in
414         Symbol (Some id, name, make_subst subst, Some uri_str)
415     | C.AMutCase (id,uri,typeno,ty,te,patterns) ->
416         let constructors = get_constructors uri typeno in
417         let named_patterns =
418           List.map2 (fun c p -> (fst c, acic2cexpr p)) 
419             constructors patterns in
420         Case (Some id, acic2cexpr te, named_patterns)
421     | C.AFix (id, no, funs) -> 
422         let defs = 
423           List.map (function (id1,n,_,_,bo) -> (n, acic2cexpr bo)) funs in
424         let (name,_) = List.nth defs no in
425         let body = LocalVar (None, name)  in
426         Letrec (Some id, defs, body)
427     | C.ACoFix (id,no,funs) -> 
428         let defs = 
429           List.map (function (id1,n,_,bo) -> (n, acic2cexpr bo)) funs in
430         let (name,_) = List.nth defs no in
431         let body = LocalVar (None, name)  in
432         Letrec (Some id, defs, body) in
433   acic2cexpr t
434 ;;
435
436
437
438
439
440
441
442
443
444
445