]> matita.cs.unibo.it Git - helm.git/blob - components/tactics/paramodulation/equality.ml
57c440860a78dc3016ba1b3c11917861d9b13a5b
[helm.git] / components / tactics / paramodulation / equality.ml
1 (* cOpyright (C) 2005, 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 (* $Id: inference.ml 6245 2006-04-05 12:07:51Z tassi $ *)
27
28 type rule = SuperpositionRight | SuperpositionLeft | Demodulation
29 type uncomparable = int -> int 
30 type equality =
31     uncomparable *       (* trick to break structural equality *)
32     int  *               (* weight *)
33     proof * 
34     (Cic.term *          (* type *)
35      Cic.term *          (* left side *)
36      Cic.term *          (* right side *)
37      Utils.comparison) * (* ordering *)  
38     Cic.metasenv  *      (* environment for metas *)
39     int                  (* id *)
40 and proof = 
41   | Exact of Cic.term
42   | Step of Subst.substitution * (rule * int*(Utils.pos*int)* Cic.term) 
43             (* subst, (rule,eq1, eq2,predicate) *)  
44 and goal_proof = (Utils.pos * int * Subst.substitution * Cic.term) list
45 ;;
46
47 (* globals *)
48 let maxid = ref 0;;
49 let id_to_eq = Hashtbl.create 1024;;
50
51 let freshid () =
52   incr maxid; !maxid
53 ;;
54
55 let reset () = 
56   maxid := 0;
57   Hashtbl.clear  id_to_eq
58 ;;
59
60 let uncomparable = fun _ -> 0
61
62 let mk_equality (weight,p,(ty,l,r,o),m) =
63   let id = freshid () in
64   let eq = (uncomparable,weight,p,(ty,l,r,o),m,id) in
65   Hashtbl.add id_to_eq id eq;
66   eq
67 ;;
68
69 let mk_tmp_equality (weight,(ty,l,r,o),m) =
70   let id = -1 in
71   uncomparable,weight,Exact (Cic.Implicit None),(ty,l,r,o),m,id
72 ;;
73
74
75 let open_equality (_,weight,proof,(ty,l,r,o),m,id) = 
76   (weight,proof,(ty,l,r,o),m,id)
77
78 let string_of_equality ?env eq =
79   match env with
80   | None ->
81       let w, _, (ty, left, right, o), _ , id = open_equality eq in
82       Printf.sprintf "Id: %d, Weight: %d, {%s}: %s =(%s) %s" 
83               id w (CicPp.ppterm ty)
84               (CicPp.ppterm left) 
85               (Utils.string_of_comparison o) (CicPp.ppterm right)
86   | Some (_, context, _) -> 
87       let names = Utils.names_of_context context in
88       let w, _, (ty, left, right, o), _ , id = open_equality eq in
89       Printf.sprintf "Id: %d, Weight: %d, {%s}: %s =(%s) %s" 
90               id w (CicPp.pp ty names)
91               (CicPp.pp left names) (Utils.string_of_comparison o)
92               (CicPp.pp right names)
93 ;;
94
95 let compare (_,_,_,s1,_,_) (_,_,_,s2,_,_) =
96   Pervasives.compare s1 s2
97 ;;
98
99 let proof_of_id id =
100   try
101     let (_,p,(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in
102       p,l,r
103   with
104       Not_found -> assert false
105
106
107 let string_of_proof ?(names=[]) p gp = 
108   let str_of_rule = function
109     | SuperpositionRight -> "SupR"
110     | SuperpositionLeft -> "SupL"
111     | Demodulation -> "Demod"
112   in
113   let str_of_pos = function
114     | Utils.Left -> "left"
115     | Utils.Right -> "right"
116   in
117   let fst3 (x,_,_) = x in
118   let rec aux margin name = 
119     let prefix = String.make margin ' ' ^ name ^ ": " in function 
120     | Exact t -> 
121         Printf.sprintf "%sExact (%s)\n" 
122           prefix (CicPp.pp t names)
123     | Step (subst,(rule,eq1,(pos,eq2),pred)) -> 
124         Printf.sprintf "%s%s(%s|%d with %d dir %s pred %s))\n"
125           prefix (str_of_rule rule) (Subst.ppsubst ~names subst) eq1 eq2 (str_of_pos pos) 
126           (CicPp.pp pred names)^ 
127         aux (margin+1) (Printf.sprintf "%d" eq1) (fst3 (proof_of_id eq1)) ^ 
128         aux (margin+1) (Printf.sprintf "%d" eq2) (fst3 (proof_of_id eq2)) 
129   in
130   aux 0 "" p ^ 
131   String.concat "\n" 
132     (List.map 
133       (fun (pos,i,s,t) -> 
134         (Printf.sprintf 
135           "GOAL: %s %d %s %s\n" 
136             (str_of_pos pos) i (Subst.ppsubst ~names s) (CicPp.pp t names)) ^ 
137         aux 1 (Printf.sprintf "%d " i) (fst3 (proof_of_id i)))
138       gp)
139 ;;
140
141 let rec depend eq id =
142   let (_,p,(_,_,_,_),_,ideq) = open_equality eq in
143   if id = ideq then true else  
144   match p with
145       Exact _ -> false
146     | Step (_,(_,id1,(_,id2),_)) ->
147         let eq1 = Hashtbl.find id_to_eq id1 in
148         let eq2 = Hashtbl.find id_to_eq id2 in  
149         depend eq1 id || depend eq2 id
150 ;;
151
152 let ppsubst = Subst.ppsubst ~names:[];;
153
154 (* returns an explicit named subst and a list of arguments for sym_eq_URI *)
155 let build_ens uri termlist =
156   let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
157   match obj with
158   | Cic.Constant (_, _, _, uris, _) ->
159       assert (List.length uris <= List.length termlist);
160       let rec aux = function
161         | [], tl -> [], tl
162         | (uri::uris), (term::tl) ->
163             let ens, args = aux (uris, tl) in
164             (uri, term)::ens, args
165         | _, _ -> assert false
166       in
167       aux (uris, termlist)
168   | _ -> assert false
169 ;;
170
171 let mk_sym uri ty t1 t2 p =
172   let ens, args =  build_ens uri [ty;t1;t2;p] in
173     Cic.Appl (Cic.Const(uri, ens) :: args)
174 ;;
175
176 let mk_trans uri ty t1 t2 t3 p12 p23 =
177   let ens, args = build_ens uri [ty;t1;t2;t3;p12;p23] in
178     Cic.Appl (Cic.Const (uri, ens) :: args)
179 ;;
180
181 let mk_eq_ind uri ty what pred p1 other p2 =
182  Cic.Appl [Cic.Const (uri, []); ty; what; pred; p1; other; p2]
183 ;;
184
185 let p_of_sym ens tl =
186   let args = List.map snd ens @ tl in
187   match args with 
188     | [_;_;_;p] -> p 
189     | _ -> assert false 
190 ;;
191
192 let open_trans ens tl =
193   let args = List.map snd ens @ tl in
194   match args with 
195     | [ty;l;m;r;p1;p2] -> ty,l,m,r,p1,p2
196     | _ -> assert false   
197 ;;
198
199 let open_eq_ind args =
200   match args with 
201   | [ty;l;pred;pl;r;pleqr] -> ty,l,pred,pl,r,pleqr
202   | _ -> assert false   
203 ;;
204
205 let open_pred pred =
206   match pred with 
207   | Cic.Lambda (_,ty,(Cic.Appl [Cic.MutInd (uri, 0,_);_;l;r])) 
208      when LibraryObjects.is_eq_URI uri -> ty,uri,l,r
209   | _ -> prerr_endline (CicPp.ppterm pred); assert false   
210 ;;
211
212 let is_not_fixed t =
213    CicSubstitution.subst (Cic.Implicit None) t <>
214    CicSubstitution.subst (Cic.Rel 1) t
215 ;;
216
217
218 let canonical t = 
219   let rec remove_refl t =
220     match t with
221     | Cic.Appl (((Cic.Const(uri_trans,ens))::tl) as args)
222           when LibraryObjects.is_trans_eq_URI uri_trans ->
223           let ty,l,m,r,p1,p2 = open_trans ens tl in
224             (match p1,p2 with
225               | Cic.Appl [Cic.MutConstruct (uri, 0, 1,_);_;_],p2 -> 
226                   remove_refl p2
227               | p1,Cic.Appl [Cic.MutConstruct (uri, 0, 1,_);_;_] -> 
228                   remove_refl p1
229               | _ -> Cic.Appl (List.map remove_refl args))
230     | Cic.Appl l -> Cic.Appl (List.map remove_refl l)
231     | Cic.LetIn (name,bo,rest) ->
232         Cic.LetIn (name,remove_refl bo,remove_refl rest)
233     | _ -> t
234   in
235   let rec canonical t =
236     match t with
237       | Cic.LetIn(name,bo,rest) -> Cic.LetIn(name,canonical bo,canonical rest)
238       | Cic.Appl (((Cic.Const(uri_sym,ens))::tl) as args)
239           when LibraryObjects.is_sym_eq_URI uri_sym ->
240           (match p_of_sym ens tl with
241              | Cic.Appl ((Cic.Const(uri,ens))::tl)
242                  when LibraryObjects.is_sym_eq_URI uri -> 
243                    canonical (p_of_sym ens tl)
244              | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
245                  when LibraryObjects.is_trans_eq_URI uri_trans ->
246                  let ty,l,m,r,p1,p2 = open_trans ens tl in
247                    mk_trans uri_trans ty r m l 
248                      (canonical (mk_sym uri_sym ty m r p2)) 
249                      (canonical (mk_sym uri_sym ty l m p1))
250              | Cic.Appl (((Cic.Const(uri_ind,ens)) as he)::tl) 
251                  when LibraryObjects.is_eq_ind_URI uri_ind || 
252                       LibraryObjects.is_eq_ind_r_URI uri_ind ->
253                  let ty, what, pred, p1, other, p2 =
254                    match tl with
255                    | [ty;what;pred;p1;other;p2] -> ty, what, pred, p1, other, p2
256                    | _ -> assert false
257                  in
258                  let pred,l,r = 
259                    match pred with
260                    | Cic.Lambda (name,s,Cic.Appl [Cic.MutInd(uri,0,ens);ty;l;r])
261                        when LibraryObjects.is_eq_URI uri ->
262                          Cic.Lambda 
263                            (name,s,Cic.Appl [Cic.MutInd(uri,0,ens);ty;r;l]),l,r
264                    | _ -> 
265                        prerr_endline (CicPp.ppterm pred);
266                        assert false
267                  in
268                  let l = CicSubstitution.subst what l in
269                  let r = CicSubstitution.subst what r in
270                  Cic.Appl 
271                    [he;ty;what;pred;
272                     canonical (mk_sym uri_sym ty l r p1);other;canonical p2]
273              | Cic.Appl [Cic.MutConstruct (uri, 0, 1,_);_;_] as t
274                  when LibraryObjects.is_eq_URI uri -> t
275              | _ -> Cic.Appl (List.map canonical args))
276       | Cic.Appl l -> Cic.Appl (List.map canonical l)
277       | _ -> t
278   in
279   remove_refl (canonical t)
280 ;;
281   
282 let ty_of_lambda = function
283   | Cic.Lambda (_,ty,_) -> ty
284   | _ -> assert false 
285 ;;
286
287 let compose_contexts ctx1 ctx2 = 
288   ProofEngineReduction.replace_lifting 
289     ~equality:(=) ~what:[Cic.Rel 1] ~with_what:[ctx2] ~where:ctx1
290 ;;
291
292 let put_in_ctx ctx t = 
293   ProofEngineReduction.replace_lifting
294     ~equality:(=) ~what:[Cic.Rel 1] ~with_what:[t] ~where:ctx
295 ;;
296
297 let mk_eq uri ty l r =
298   Cic.Appl [Cic.MutInd(uri,0,[]);ty;l;r]
299 ;;
300
301 let mk_refl uri ty t = 
302   Cic.Appl [Cic.MutConstruct(uri,0,1,[]);ty;t]
303 ;;
304
305 let open_eq = function 
306   | Cic.Appl [Cic.MutInd(uri,0,[]);ty;l;r] when LibraryObjects.is_eq_URI uri ->
307       uri, ty, l ,r
308   | _ -> assert false
309 ;;
310
311 let contextualize uri ty left right t = 
312   (* aux [uri] [ty] [left] [right] [ctx] [t] 
313    * 
314    * the parameters validate this invariant  
315    *   t: eq(uri) ty left right
316    * that is used only by the base case
317    *
318    * ctx is a term with an open (Rel 1). (Rel 1) is the empty context
319    *)
320     let rec aux uri ty left right ctx_d = function
321       | Cic.LetIn (name,body,rest) ->
322           (* we should go in body *)
323           Cic.LetIn (name,body,aux uri ty left right ctx_d rest)
324       | Cic.Appl ((Cic.Const(uri_ind,ens))::tl)
325         when LibraryObjects.is_eq_ind_URI uri_ind || 
326              LibraryObjects.is_eq_ind_r_URI uri_ind ->
327           let ty1,what,pred,p1,other,p2 = open_eq_ind tl in
328           let ty2,eq,lp,rp = open_pred pred in 
329           let uri_trans = LibraryObjects.trans_eq_URI ~eq:uri in
330           let uri_sym = LibraryObjects.sym_eq_URI ~eq:uri in
331           let is_not_fixed_lp = is_not_fixed lp in
332           let avoid_eq_ind = LibraryObjects.is_eq_ind_URI uri_ind in
333           (* extract the context and the fixed term from the predicate *)
334           let m, ctx_c = 
335             let m, ctx_c = if is_not_fixed_lp then rp,lp else lp,rp in
336             (* they were under a lambda *)
337             let m =  CicSubstitution.subst (Cic.Implicit None) m in
338             let ctx_c = CicSubstitution.subst (Cic.Rel 1) ctx_c in
339             m, ctx_c          
340           in
341           (* create the compound context and put the terms under it *)
342           let ctx_dc = compose_contexts ctx_d ctx_c in
343           let dc_what = put_in_ctx ctx_dc what in
344           let dc_other = put_in_ctx ctx_dc other in
345           (* m is already in ctx_c so it is put in ctx_d only *)
346           let d_m = put_in_ctx ctx_d m in
347           (* we also need what in ctx_c *)
348           let c_what = put_in_ctx ctx_c what in
349           (* now put the proofs in the compound context *)
350           let p1 = (* p1: dc_what = d_m *)
351             if is_not_fixed_lp then 
352               aux uri ty1 c_what m ctx_d p1 
353             else
354               mk_sym uri_sym ty d_m dc_what
355                 (aux uri ty1 m c_what ctx_d p1)
356           in
357           let p2 = (* p2: dc_other = dc_what *)
358             if avoid_eq_ind then
359               mk_sym uri_sym ty dc_what dc_other
360                 (aux uri ty1 what other ctx_dc p2)
361             else
362               aux uri ty1 other what ctx_dc p2
363           in
364           (* if pred = \x.C[x]=m --> t : C[other]=m --> trans other what m
365              if pred = \x.m=C[x] --> t : m=C[other] --> trans m what other *)
366           let a,b,c,paeqb,pbeqc =
367             if is_not_fixed_lp then
368               dc_other,dc_what,d_m,p2,p1
369             else
370               d_m,dc_what,dc_other,
371                 (mk_sym uri_sym ty dc_what d_m p1),
372                 (mk_sym uri_sym ty dc_other dc_what p2)
373           in
374           mk_trans uri_trans ty a b c paeqb pbeqc
375     | t -> 
376         let uri_sym = LibraryObjects.sym_eq_URI ~eq:uri in
377         let uri_ind = LibraryObjects.eq_ind_URI ~eq:uri in
378         let pred = 
379           (* ctx_d will go under a lambda, but put_in_ctx substitutes Rel 1 *)
380           let ctx_d = CicSubstitution.lift_from 2 1 ctx_d in (* bleah *)
381           let r = put_in_ctx ctx_d (CicSubstitution.lift 1 left) in
382           let l = ctx_d in
383           let lty = CicSubstitution.lift 1 ty in 
384           Cic.Lambda (Cic.Name "foo",ty,(mk_eq uri lty l r))
385         in
386         let d_left = put_in_ctx ctx_d left in
387         let d_right = put_in_ctx ctx_d right in
388         let refl_eq = mk_refl uri ty d_left in
389         mk_sym uri_sym ty d_right d_left
390           (mk_eq_ind uri_ind ty left pred refl_eq right t)
391   in
392   let empty_context = Cic.Rel 1 in
393   aux uri ty left right empty_context t
394 ;;
395
396 let contextualize_rewrites t ty = 
397   let eq,ty,l,r = open_eq ty in
398   contextualize eq ty l r t
399 ;;
400   
401 let build_proof_step lift subst p1 p2 pos l r pred =
402   let p1 = Subst.apply_subst_lift lift subst p1 in
403   let p2 = Subst.apply_subst_lift lift subst p2 in
404   let l  = CicSubstitution.lift lift l in
405   let l = Subst.apply_subst_lift lift subst l in
406   let r  = CicSubstitution.lift lift r in
407   let r = Subst.apply_subst_lift lift subst r in
408   let pred = CicSubstitution.lift lift pred in
409   let pred = Subst.apply_subst_lift lift subst pred in
410   let ty,body = 
411     match pred with
412       | Cic.Lambda (_,ty,body) -> ty,body 
413       | _ -> assert false
414   in
415   let what, other = 
416     if pos = Utils.Left then l,r else r,l
417   in
418     match pos with
419       | Utils.Left ->
420         mk_eq_ind (Utils.eq_ind_URI ()) ty what pred p1 other p2
421       | Utils.Right ->
422         mk_eq_ind (Utils.eq_ind_r_URI ()) ty what pred p1 other p2
423 ;;
424
425 let parametrize_proof p l r ty = 
426   let parameters = CicUtil.metas_of_term p 
427 @ CicUtil.metas_of_term l 
428 @ CicUtil.metas_of_term r
429 in (* ?if they are under a lambda? *)
430   let parameters = 
431     HExtlib.list_uniq (List.sort Pervasives.compare parameters) 
432   in
433   let what = List.map (fun (i,l) -> Cic.Meta (i,l)) parameters in 
434   let with_what, lift_no = 
435     List.fold_right (fun _ (acc,n) -> ((Cic.Rel n)::acc),n+1) what ([],1) 
436   in
437   let p = CicSubstitution.lift (lift_no-1) p in
438   let p = 
439     ProofEngineReduction.replace_lifting
440     ~equality:(fun t1 t2 -> match t1,t2 with Cic.Meta (i,_),Cic.Meta(j,_) -> i=j | _ -> false) ~what ~with_what ~where:p
441   in
442   let ty_of_m _ = ty (*function 
443     | Cic.Meta (i,_) -> List.assoc i menv 
444     | _ -> assert false *)
445   in
446   let args, proof,_ = 
447     List.fold_left 
448       (fun (instance,p,n) m -> 
449         (instance@[m],
450         Cic.Lambda 
451           (Cic.Name ("x"^string_of_int n),
452           CicSubstitution.lift (lift_no - n - 1) (ty_of_m m),
453           p),
454         n+1)) 
455       ([Cic.Rel 1],p,1) 
456       what
457   in
458   let instance = match args with | [x] -> x | _ -> Cic.Appl args in
459   proof, instance
460 ;;
461
462 let wfo goalproof proof =
463   let rec aux acc id =
464     let p,_,_ = proof_of_id id in
465     match p with
466     | Exact _ -> if (List.mem id acc) then acc else id :: acc
467     | Step (_,(_,id1, (_,id2), _)) -> 
468         let acc = if not (List.mem id1 acc) then aux acc id1 else acc in
469         let acc = if not (List.mem id2 acc) then aux acc id2 else acc in
470         id :: acc
471   in
472   let acc = 
473     match proof with
474       | Exact _ -> []
475       | Step (_,(_,id1, (_,id2), _)) -> aux (aux [] id1) id2
476   in 
477   List.fold_left (fun acc (_,id,_,_) -> aux acc id) acc goalproof
478 ;;
479
480 let string_of_id names id = 
481   try
482     let (_,p,(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in
483     match p with
484     | Exact t -> 
485         Printf.sprintf "%d = %s: %s = %s" id
486           (CicPp.pp t names) (CicPp.pp l names) (CicPp.pp r names)
487     | Step (_,(step,id1, (_,id2), _) ) ->
488         Printf.sprintf "%6d: %s %6d %6d   %s = %s" id
489           (if step = SuperpositionRight then "SupR" else "Demo") 
490           id1 id2 (CicPp.pp l names) (CicPp.pp r names)
491   with
492       Not_found -> assert false
493
494 let pp_proof names goalproof proof =
495   String.concat "\n" (List.map (string_of_id names) (wfo goalproof proof)) ^ 
496   "\ngoal is demodulated with " ^ 
497     (String.concat " " 
498       ((List.map (fun (_,i,_,_) -> string_of_int i) goalproof)))
499 ;;
500
501 (* returns the list of ids that should be factorized *)
502 let get_duplicate_step_in_wfo l p =
503   let ol = List.rev l in
504   let h = Hashtbl.create 13 in
505   let add i n = 
506     let p,_,_ = proof_of_id i in 
507     match p with 
508     | Exact _ -> true
509     | _ -> 
510         try let (pos,no) = Hashtbl.find h i in Hashtbl.replace h i (pos,no+1);false
511         with Not_found -> Hashtbl.add h i (n,1);true
512   in
513   let rec aux n = function
514     | Exact _ -> n
515     | Step (_,(_,i1,(_,i2),_)) -> 
516         let go_on_1 = add i1 n in
517         let go_on_2 = add i2 n in
518         max 
519          (if go_on_1 then aux (n+1) (let p,_,_ = proof_of_id i1 in p) else n+1)
520          (if go_on_2 then aux (n+1) (let p,_,_ = proof_of_id i2 in p) else n+1)
521   in
522   let i = aux 0 p in 
523   let _ = 
524     List.fold_left 
525       (fun acc (_,id,_,_) -> aux acc (let p,_,_ = proof_of_id id in p))
526       i ol
527   in
528   (* now h is complete *)
529   let proofs = Hashtbl.fold (fun k (pos,count) acc->(k,pos,count)::acc) h [] in
530   let proofs = List.filter (fun (_,_,c) -> c > 1) proofs in
531   let proofs = 
532     List.sort (fun (_,c1,_) (_,c2,_) -> Pervasives.compare c2 c1) proofs 
533   in
534   List.map (fun (i,_,_) -> i) proofs
535 ;;
536
537 let build_proof_term h lift proof =
538   let proof_of_id aux id =
539     let p,l,r = proof_of_id id in
540     try List.assoc id h,l,r with Not_found -> aux p, l, r
541   in
542   let rec aux = function
543      | Exact term -> CicSubstitution.lift lift term
544      | Step (subst,(_, id1, (pos,id2), pred)) ->
545          let p1,_,_ = proof_of_id aux id1 in
546          let p2,l,r = proof_of_id aux id2 in
547            build_proof_step lift subst p1 p2 pos l r pred
548   in
549    aux proof
550 ;;
551
552 let build_goal_proof l initial ty se =
553   let se = List.map (fun i -> Cic.Meta (i,[])) se in 
554   let lets = get_duplicate_step_in_wfo l initial in
555   let letsno = List.length lets in
556   let _,mty,_,_ = open_eq ty in
557   let lift_list l = List.map (fun (i,t) -> i,CicSubstitution.lift 1 t) l 
558   in
559   let lets,_,h = 
560     List.fold_left
561       (fun (acc,n,h) id -> 
562         let p,l,r = proof_of_id id in
563         let cic = build_proof_term h n p in
564         let real_cic,instance = 
565           parametrize_proof cic l r (CicSubstitution.lift n mty)
566         in
567         let h = (id, instance)::lift_list h in
568         acc@[id,real_cic],n+1,h) 
569       ([],0,[]) lets
570   in
571   let proof,se = 
572     let rec aux se current_proof = function
573       | [] -> current_proof,se
574       | (pos,id,subst,pred)::tl ->
575            let p,l,r = proof_of_id id in
576            let p = build_proof_term h letsno p in
577            let pos = if pos = Utils.Left then Utils.Right else Utils.Left in
578            let proof = 
579              build_proof_step letsno subst current_proof p pos l r pred 
580            in
581            let proof,se = aux se proof tl in
582            Subst.apply_subst_lift letsno subst proof,
583            List.map (fun x -> Subst.apply_subst_lift letsno subst x) se
584     in
585     aux se (build_proof_term h letsno initial) l
586   in
587   let n,proof = 
588     let initial = proof in
589     List.fold_right
590       (fun (id,cic) (n,p) -> 
591         n-1,
592         Cic.LetIn (
593           Cic.Name ("H"^string_of_int id),
594           cic, p))
595     lets (letsno-1,initial)
596   in
597   canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty)), se
598 ;;
599
600 let refl_proof ty term = 
601   Cic.Appl 
602     [Cic.MutConstruct 
603        (LibraryObjects.eq_URI (), 0, 1, []);
604        ty; term]
605 ;;
606
607 let metas_of_proof p =
608   let p = build_proof_term [] 0 p in
609   Utils.metas_of_term p
610 ;;
611
612 let relocate newmeta menv =
613   let subst, metasenv, newmeta = 
614     List.fold_right 
615       (fun (i, context, ty) (subst, menv, maxmeta) ->         
616         let irl = [] (*
617          CicMkImplicit.identity_relocation_list_for_metavariable context *)
618         in
619         let newsubst = Subst.buildsubst i context (Cic.Meta(maxmeta,irl)) ty subst in
620         let newmeta = maxmeta, context, ty in
621         newsubst, newmeta::menv, maxmeta+1) 
622       menv (Subst.empty_subst, [], newmeta+1)
623   in
624   let metasenv = Subst.apply_subst_metasenv subst metasenv in
625   let subst = Subst.flatten_subst subst in
626   subst, metasenv, newmeta
627
628
629 let fix_metas newmeta eq = 
630   let w, p, (ty, left, right, o), menv,_ = open_equality eq in
631   let subst, metasenv, newmeta = relocate newmeta menv in
632   let ty = Subst.apply_subst subst ty in
633   let left = Subst.apply_subst subst left in
634   let right = Subst.apply_subst subst right in
635   let fix_proof = function
636     | Exact p -> Exact (Subst.apply_subst subst p)
637     | Step (s,(r,id1,(pos,id2),pred)) -> 
638         Step (Subst.concat s subst,(r,id1,(pos,id2), pred))
639   in
640   let p = fix_proof p in
641   let eq = mk_equality (w, p, (ty, left, right, o), metasenv) in
642   newmeta+1, eq  
643
644 exception NotMetaConvertible;;
645
646 let meta_convertibility_aux table t1 t2 =
647   let module C = Cic in
648   let rec aux ((table_l, table_r) as table) t1 t2 =
649     match t1, t2 with
650     | C.Meta (m1, tl1), C.Meta (m2, tl2) ->
651         let m1_binding, table_l =
652           try List.assoc m1 table_l, table_l
653           with Not_found -> m2, (m1, m2)::table_l
654         and m2_binding, table_r =
655           try List.assoc m2 table_r, table_r
656           with Not_found -> m1, (m2, m1)::table_r
657         in
658         if (m1_binding <> m2) || (m2_binding <> m1) then
659           raise NotMetaConvertible
660         else (
661           try
662             List.fold_left2
663               (fun res t1 t2 ->
664                  match t1, t2 with
665                  | None, Some _ | Some _, None -> raise NotMetaConvertible
666                  | None, None -> res
667                  | Some t1, Some t2 -> (aux res t1 t2))
668               (table_l, table_r) tl1 tl2
669           with Invalid_argument _ ->
670             raise NotMetaConvertible
671         )
672     | C.Var (u1, ens1), C.Var (u2, ens2)
673     | C.Const (u1, ens1), C.Const (u2, ens2) when (UriManager.eq u1 u2) ->
674         aux_ens table ens1 ens2
675     | C.Cast (s1, t1), C.Cast (s2, t2)
676     | C.Prod (_, s1, t1), C.Prod (_, s2, t2)
677     | C.Lambda (_, s1, t1), C.Lambda (_, s2, t2)
678     | C.LetIn (_, s1, t1), C.LetIn (_, s2, t2) ->
679         let table = aux table s1 s2 in
680         aux table t1 t2
681     | C.Appl l1, C.Appl l2 -> (
682         try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
683         with Invalid_argument _ -> raise NotMetaConvertible
684       )
685     | C.MutInd (u1, i1, ens1), C.MutInd (u2, i2, ens2)
686         when (UriManager.eq u1 u2) && i1 = i2 -> aux_ens table ens1 ens2
687     | C.MutConstruct (u1, i1, j1, ens1), C.MutConstruct (u2, i2, j2, ens2)
688         when (UriManager.eq u1 u2) && i1 = i2 && j1 = j2 ->
689         aux_ens table ens1 ens2
690     | C.MutCase (u1, i1, s1, t1, l1), C.MutCase (u2, i2, s2, t2, l2)
691         when (UriManager.eq u1 u2) && i1 = i2 ->
692         let table = aux table s1 s2 in
693         let table = aux table t1 t2 in (
694           try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
695           with Invalid_argument _ -> raise NotMetaConvertible
696         )
697     | C.Fix (i1, il1), C.Fix (i2, il2) when i1 = i2 -> (
698         try
699           List.fold_left2
700             (fun res (n1, i1, s1, t1) (n2, i2, s2, t2) ->
701                if i1 <> i2 then raise NotMetaConvertible
702                else
703                  let res = (aux res s1 s2) in aux res t1 t2)
704             table il1 il2
705         with Invalid_argument _ -> raise NotMetaConvertible
706       )
707     | C.CoFix (i1, il1), C.CoFix (i2, il2) when i1 = i2 -> (
708         try
709           List.fold_left2
710             (fun res (n1, s1, t1) (n2, s2, t2) ->
711                let res = aux res s1 s2 in aux res t1 t2)
712             table il1 il2
713         with Invalid_argument _ -> raise NotMetaConvertible
714       )
715     | t1, t2 when t1 = t2 -> table
716     | _, _ -> raise NotMetaConvertible
717         
718   and aux_ens table ens1 ens2 =
719     let cmp (u1, t1) (u2, t2) =
720       Pervasives.compare (UriManager.string_of_uri u1) (UriManager.string_of_uri u2)
721     in
722     let ens1 = List.sort cmp ens1
723     and ens2 = List.sort cmp ens2 in
724     try
725       List.fold_left2
726         (fun res (u1, t1) (u2, t2) ->
727            if not (UriManager.eq u1 u2) then raise NotMetaConvertible
728            else aux res t1 t2)
729         table ens1 ens2
730     with Invalid_argument _ -> raise NotMetaConvertible
731   in
732   aux table t1 t2
733 ;;
734
735
736 let meta_convertibility_eq eq1 eq2 =
737   let _, _, (ty, left, right, _), _,_ = open_equality eq1 in
738   let _, _, (ty', left', right', _), _,_ = open_equality eq2 in
739   if ty <> ty' then
740     false
741   else if (left = left') && (right = right') then
742     true
743   else if (left = right') && (right = left') then
744     true
745   else
746     try
747       let table = meta_convertibility_aux ([], []) left left' in
748       let _ = meta_convertibility_aux table right right' in
749       true
750     with NotMetaConvertible ->
751       try
752         let table = meta_convertibility_aux ([], []) left right' in
753         let _ = meta_convertibility_aux table right left' in
754         true
755       with NotMetaConvertible ->
756         false
757 ;;
758
759
760 let meta_convertibility t1 t2 =
761   if t1 = t2 then
762     true
763   else
764     try
765       ignore(meta_convertibility_aux ([], []) t1 t2);
766       true
767     with NotMetaConvertible ->
768       false
769 ;;
770
771 exception TermIsNotAnEquality;;
772
773 let term_is_equality term =
774   let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in
775   match term with
776   | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _] when iseq uri -> true
777   | _ -> false
778 ;;
779
780 let equality_of_term proof term =
781   let eq_uri = LibraryObjects.eq_URI () in
782   let iseq uri = UriManager.eq uri eq_uri in
783   match term with
784   | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
785       let o = !Utils.compare_terms t1 t2 in
786       let stat = (ty,t1,t2,o) in
787       let w = Utils.compute_equality_weight stat in
788       let e = mk_equality (w, Exact proof, stat,[]) in
789       e
790   | _ ->
791       raise TermIsNotAnEquality
792 ;;
793
794 let is_weak_identity eq = 
795   let _,_,(_,left, right,_),_,_ = open_equality eq in
796   left = right || meta_convertibility left right 
797 ;;
798
799 let is_identity (_, context, ugraph) eq = 
800   let _,_,(ty,left,right,_),menv,_ = open_equality eq in
801   left = right ||
802   (* (meta_convertibility left right)) *)
803   fst (CicReduction.are_convertible ~metasenv:menv context left right ugraph)
804 ;;
805
806
807 let term_of_equality equality =
808   let _, _, (ty, left, right, _), menv, _= open_equality equality in
809   let eq i = function Cic.Meta (j, _) -> i = j | _ -> false in
810   let argsno = List.length menv in
811   let t =
812     CicSubstitution.lift argsno
813       (Cic.Appl [Cic.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right])
814   in
815   snd (
816     List.fold_right
817       (fun (i,_,ty) (n, t) ->
818          let name = Cic.Name ("X" ^ (string_of_int n)) in
819          let ty = CicSubstitution.lift (n-1) ty in
820          let t = 
821            ProofEngineReduction.replace
822              ~equality:eq ~what:[i]
823              ~with_what:[Cic.Rel (argsno - (n - 1))] ~where:t
824          in
825            (n-1, Cic.Prod (name, ty, t)))
826       menv (argsno, t))
827 ;;
828