]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/paramodulation/inference.ml
may fix the nigtly build
[helm.git] / helm / ocaml / paramodulation / inference.ml
1 open Utils;;
2
3
4 type equality =
5     int  *               (* weight *)
6     (Cic.term *          (* type *)
7      Cic.term *          (* left side *)
8      Cic.term *          (* right side *)
9      Utils.comparison) * (* ordering *)  
10     Cic.metasenv *       (* environment for metas *)
11     Cic.term list        (* arguments *)
12 ;;
13
14
15 type proof =
16   | BasicProof of Cic.term
17   | ProofBlock of
18       Cic.substitution * UriManager.uri * Cic.term * (Utils.pos * equality) *
19         equality
20   | NoProof
21 ;;
22
23
24 let string_of_equality ?env =
25   match env with
26   | None -> (
27       function
28         | _, (ty, left, right, o), _, _ ->
29             Printf.sprintf "{%s}: %s =(%s) %s" (CicPp.ppterm ty)
30               (CicPp.ppterm left) (string_of_comparison o) (CicPp.ppterm right)
31     )
32   | Some (_, context, _) -> (
33       let names = names_of_context context in
34       function
35         | _, (ty, left, right, o), _, _ ->
36             Printf.sprintf "{%s}: %s =(%s) %s" (CicPp.pp ty names)
37               (CicPp.pp left names) (string_of_comparison o)
38               (CicPp.pp right names)
39     )
40 ;;
41
42
43 let prooftable = Hashtbl.create 2001;;
44
45 let store_proof equality proof =
46   if not (Hashtbl.mem prooftable equality) then
47     Hashtbl.add prooftable equality proof
48 ;;
49
50
51 let delete_proof equality =
52 (*   Printf.printf "| Removing proof of %s" (string_of_equality equality); *)
53 (*   print_newline (); *)
54   Hashtbl.remove prooftable equality
55 ;;
56
57
58 let rec build_term_proof equality =
59 (*   Printf.printf "build_term_proof %s" (string_of_equality equality); *)
60 (*   print_newline (); *)
61   let proof = try Hashtbl.find prooftable equality with Not_found -> NoProof in
62   match proof with
63   | NoProof ->
64       Printf.fprintf stderr "WARNING: no proof for %s\n"
65         (string_of_equality equality);
66       Cic.Implicit None
67   | BasicProof term -> term
68   | ProofBlock (subst, eq_URI, t', (pos, eq), eq') ->
69 (*       Printf.printf "   ProofBlock: eq = %s, eq' = %s" *)
70 (*         (string_of_equality eq) (string_of_equality eq'); *)
71 (*       print_newline (); *)
72       let proof' = build_term_proof eq in
73       let eqproof = build_term_proof eq' in
74       let _, (ty, what, other, _), menv', args' = eq in
75       let what, other = if pos = Utils.Left then what, other else other, what in
76       CicMetaSubst.apply_subst subst
77         (Cic.Appl [Cic.Const (eq_URI, []); ty;
78                    what; t'; eqproof; other; proof'])
79 ;;
80
81
82 let rec metas_of_term = function
83   | Cic.Meta (i, c) -> [i]
84   | Cic.Var (_, ens) 
85   | Cic.Const (_, ens) 
86   | Cic.MutInd (_, _, ens) 
87   | Cic.MutConstruct (_, _, _, ens) ->
88       List.flatten (List.map (fun (u, t) -> metas_of_term t) ens)
89   | Cic.Cast (s, t)
90   | Cic.Prod (_, s, t)
91   | Cic.Lambda (_, s, t)
92   | Cic.LetIn (_, s, t) -> (metas_of_term s) @ (metas_of_term t)
93   | Cic.Appl l -> List.flatten (List.map metas_of_term l)
94   | Cic.MutCase (uri, i, s, t, l) ->
95       (metas_of_term s) @ (metas_of_term t) @
96         (List.flatten (List.map metas_of_term l))
97   | Cic.Fix (i, il) ->
98       List.flatten
99         (List.map (fun (s, i, t1, t2) ->
100                      (metas_of_term t1) @ (metas_of_term t2)) il)
101   | Cic.CoFix (i, il) ->
102       List.flatten
103         (List.map (fun (s, t1, t2) ->
104                      (metas_of_term t1) @ (metas_of_term t2)) il)
105   | _ -> []
106 ;;      
107
108
109 exception NotMetaConvertible;;
110
111 let meta_convertibility_aux table t1 t2 =
112   let module C = Cic in
113   let print_table t =
114     String.concat ", "
115       (List.map
116          (fun (k, v) -> Printf.sprintf "(%d, %d)" k v) t)
117   in
118   let rec aux ((table_l, table_r) as table) t1 t2 =
119 (*     Printf.printf "aux %s, %s\ntable_l: %s, table_r: %s\n" *)
120 (*       (CicPp.ppterm t1) (CicPp.ppterm t2) *)
121 (*       (print_table table_l) (print_table table_r); *)
122     match t1, t2 with
123     | C.Meta (m1, tl1), C.Meta (m2, tl2) ->
124         let m1_binding, table_l =
125           try List.assoc m1 table_l, table_l
126           with Not_found -> m2, (m1, m2)::table_l
127         and m2_binding, table_r =
128           try List.assoc m2 table_r, table_r
129           with Not_found -> m1, (m2, m1)::table_r
130         in
131 (*         let m1_binding, m2_binding, table = *)
132 (*           let m1b, table =  *)
133 (*             try List.assoc m1 table, table *)
134 (*             with Not_found -> m2, (m1, m2)::table *)
135 (*           in *)
136 (*           let m2b, table =  *)
137 (*             try List.assoc m2 table, table *)
138 (*             with Not_found -> m1, (m2, m1)::table *)
139 (*           in *)
140 (*           m1b, m2b, table *)
141 (*         in *)
142 (*         Printf.printf "table_l: %s\ntable_r: %s\n\n" *)
143 (*           (print_table table_l) (print_table table_r); *)
144         if (m1_binding <> m2) || (m2_binding <> m1) then
145           raise NotMetaConvertible
146         else (
147           try
148             List.fold_left2
149               (fun res t1 t2 ->
150                  match t1, t2 with
151                  | None, Some _ | Some _, None -> raise NotMetaConvertible
152                  | None, None -> res
153                  | Some t1, Some t2 -> (aux res t1 t2))
154               (table_l, table_r) tl1 tl2
155           with Invalid_argument _ ->
156             raise NotMetaConvertible
157         )
158     | C.Var (u1, ens1), C.Var (u2, ens2)
159     | C.Const (u1, ens1), C.Const (u2, ens2) when (UriManager.eq u1 u2) ->
160         aux_ens table ens1 ens2
161     | C.Cast (s1, t1), C.Cast (s2, t2)
162     | C.Prod (_, s1, t1), C.Prod (_, s2, t2)
163     | C.Lambda (_, s1, t1), C.Lambda (_, s2, t2)
164     | C.LetIn (_, s1, t1), C.LetIn (_, s2, t2) ->
165         let table = aux table s1 s2 in
166         aux table t1 t2
167     | C.Appl l1, C.Appl l2 -> (
168         try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
169         with Invalid_argument _ -> raise NotMetaConvertible
170       )
171     | C.MutInd (u1, i1, ens1), C.MutInd (u2, i2, ens2)
172         when (UriManager.eq u1 u2) && i1 = i2 -> aux_ens table ens1 ens2
173     | C.MutConstruct (u1, i1, j1, ens1), C.MutConstruct (u2, i2, j2, ens2)
174         when (UriManager.eq u1 u2) && i1 = i2 && j1 = j2 ->
175         aux_ens table ens1 ens2
176     | C.MutCase (u1, i1, s1, t1, l1), C.MutCase (u2, i2, s2, t2, l2)
177         when (UriManager.eq u1 u2) && i1 = i2 ->
178         let table = aux table s1 s2 in
179         let table = aux table t1 t2 in (
180           try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
181           with Invalid_argument _ -> raise NotMetaConvertible
182         )
183     | C.Fix (i1, il1), C.Fix (i2, il2) when i1 = i2 -> (
184         try
185           List.fold_left2
186             (fun res (n1, i1, s1, t1) (n2, i2, s2, t2) ->
187                if i1 <> i2 then raise NotMetaConvertible
188                else
189                  let res = (aux res s1 s2) in aux res t1 t2)
190             table il1 il2
191         with Invalid_argument _ -> raise NotMetaConvertible
192       )
193     | C.CoFix (i1, il1), C.CoFix (i2, il2) when i1 = i2 -> (
194         try
195           List.fold_left2
196             (fun res (n1, s1, t1) (n2, s2, t2) ->
197                let res = aux res s1 s2 in aux res t1 t2)
198             table il1 il2
199         with Invalid_argument _ -> raise NotMetaConvertible
200       )
201     | t1, t2 when t1 = t2 -> table
202     | _, _ -> raise NotMetaConvertible
203         
204   and aux_ens table ens1 ens2 =
205     let cmp (u1, t1) (u2, t2) =
206       compare (UriManager.string_of_uri u1) (UriManager.string_of_uri u2)
207     in
208     let ens1 = List.sort cmp ens1
209     and ens2 = List.sort cmp ens2 in
210     try
211       List.fold_left2
212         (fun res (u1, t1) (u2, t2) ->
213            if not (UriManager.eq u1 u2) then raise NotMetaConvertible
214            else aux res t1 t2)
215         table ens1 ens2
216     with Invalid_argument _ -> raise NotMetaConvertible
217   in
218   aux table t1 t2
219 ;;
220
221
222 let meta_convertibility_eq eq1 eq2 =
223   let _, (ty, left, right, _), _, _ = eq1
224   and _, (ty', left', right', _), _, _ = eq2 in
225   if ty <> ty' then
226     false
227   else if (left = left') && (right = right') then
228     true
229   else if (left = right') && (right = left') then
230     true
231   else
232     try
233       let table = meta_convertibility_aux ([], []) left left' in
234       let _ = meta_convertibility_aux table right right' in
235       true
236     with NotMetaConvertible ->
237       try
238         let table = meta_convertibility_aux ([], []) left right' in
239         let _ = meta_convertibility_aux table right left' in
240         true
241       with NotMetaConvertible ->
242         false
243 ;;
244
245
246 let meta_convertibility t1 t2 =
247   let f t =
248     String.concat ", "
249       (List.map
250          (fun (k, v) -> Printf.sprintf "(%d, %d)" k v) t)
251   in
252   if t1 = t2 then
253     true
254   else
255     try
256       let l, r = meta_convertibility_aux ([], []) t1 t2 in
257       (*     Printf.printf "meta_convertibility:\n%s\n%s\n\n" (f l) (f r); *)
258       true
259     with NotMetaConvertible ->
260       false
261 ;;
262
263
264 let replace_metas (* context *) term =
265   let module C = Cic in
266   let rec aux = function
267     | C.Meta (i, c) ->
268 (*         let irl = *)
269 (*           CicMkImplicit.identity_relocation_list_for_metavariable context *)
270 (*         in *)
271 (*         if c = irl then *)
272 (*           C.Implicit (Some (`MetaIndex i)) *)
273 (*         else ( *)
274 (*           Printf.printf "WARNING: c non e` un identity_relocation_list!\n%s\n" *)
275 (*             (String.concat "\n" *)
276 (*                (List.map *)
277 (*                   (function None -> "" | Some t -> CicPp.ppterm t) c)); *)
278 (*           C.Meta (i, c) *)
279 (*         ) *)
280         C.Implicit (Some (`MetaInfo (i, c)))
281     | C.Var (u, ens) -> C.Var (u, aux_ens ens)
282     | C.Const (u, ens) -> C.Const (u, aux_ens ens)
283     | C.Cast (s, t) -> C.Cast (aux s, aux t)
284     | C.Prod (name, s, t) -> C.Prod (name, aux s, aux t)
285     | C.Lambda (name, s, t) -> C.Lambda (name, aux s, aux t)
286     | C.LetIn (name, s, t) -> C.LetIn (name, aux s, aux t)
287     | C.Appl l -> C.Appl (List.map aux l)
288     | C.MutInd (uri, i, ens) -> C.MutInd (uri, i, aux_ens ens)
289     | C.MutConstruct (uri, i, j, ens) -> C.MutConstruct (uri, i, j, aux_ens ens)
290     | C.MutCase (uri, i, s, t, l) ->
291         C.MutCase (uri, i, aux s, aux t, List.map aux l)
292     | C.Fix (i, il) ->
293         let il' =
294           List.map (fun (s, i, t1, t2) -> (s, i, aux t1, aux t2)) il in
295         C.Fix (i, il')
296     | C.CoFix (i, il) ->
297         let il' =
298           List.map (fun (s, t1, t2) -> (s, aux t1, aux t2)) il in
299         C.CoFix (i, il')
300     | t -> t
301   and aux_ens ens =
302     List.map (fun (u, t) -> (u, aux t)) ens
303   in
304   aux term
305 ;;
306
307
308 let restore_metas (* context *) term =
309   let module C = Cic in
310   let rec aux = function
311     | C.Implicit (Some (`MetaInfo (i, c))) ->
312 (*         let c = *)
313 (*           CicMkImplicit.identity_relocation_list_for_metavariable context *)
314 (*         in *)
315 (*         C.Meta (i, c) *)
316 (*         let local_context:(C.term option) list = *)
317 (*           Marshal.from_string mc 0 *)
318 (*         in *)
319 (*         C.Meta (i, local_context) *)
320         C.Meta (i, c)
321     | C.Var (u, ens) -> C.Var (u, aux_ens ens)
322     | C.Const (u, ens) -> C.Const (u, aux_ens ens)
323     | C.Cast (s, t) -> C.Cast (aux s, aux t)
324     | C.Prod (name, s, t) -> C.Prod (name, aux s, aux t)
325     | C.Lambda (name, s, t) -> C.Lambda (name, aux s, aux t)
326     | C.LetIn (name, s, t) -> C.LetIn (name, aux s, aux t)
327     | C.Appl l -> C.Appl (List.map aux l)
328     | C.MutInd (uri, i, ens) -> C.MutInd (uri, i, aux_ens ens)
329     | C.MutConstruct (uri, i, j, ens) -> C.MutConstruct (uri, i, j, aux_ens ens)
330     | C.MutCase (uri, i, s, t, l) ->
331         C.MutCase (uri, i, aux s, aux t, List.map aux l)
332     | C.Fix (i, il) ->
333         let il' =
334           List.map (fun (s, i, t1, t2) -> (s, i, aux t1, aux t2)) il in
335         C.Fix (i, il')
336     | C.CoFix (i, il) ->
337         let il' =
338           List.map (fun (s, t1, t2) -> (s, aux t1, aux t2)) il in
339         C.CoFix (i, il')
340     | t -> t
341   and aux_ens ens =
342     List.map (fun (u, t) -> (u, aux t)) ens
343   in
344   aux term
345 ;;
346
347
348 let rec restore_subst (* context *) subst =
349   List.map
350     (fun (i, (c, t, ty)) ->
351        i, (c, restore_metas (* context *) t, ty))
352     subst
353 ;;
354
355
356 let rec check_irl start = function
357   | [] -> true
358   | None::tl -> check_irl (start+1) tl
359   | (Some (Cic.Rel x))::tl ->
360       if x = start then check_irl (start+1) tl else false
361   | _ -> false
362 ;;
363
364 let rec is_simple_term = function
365   | Cic.Appl ((Cic.Meta _)::_) -> false
366   | Cic.Appl l -> List.for_all is_simple_term l
367   | Cic.Meta (i, l) -> check_irl 1 l
368   | Cic.Rel _ -> true
369   | _ -> false
370 ;;
371
372
373 let lookup_subst meta subst =
374   match meta with
375   | Cic.Meta (i, _) -> (
376       try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst in t
377       with Not_found -> meta
378     )
379   | _ -> assert false
380 ;;
381
382
383 let unification_simple metasenv context t1 t2 ugraph =
384   let module C = Cic in
385   let module M = CicMetaSubst in
386   let module U = CicUnification in
387   let lookup = lookup_subst in
388   let rec occurs_check subst what where =
389     (*       Printf.printf "occurs_check %s %s" *)
390     (*         (CicPp.ppterm what) (CicPp.ppterm where); *)
391     (*       print_newline (); *)
392     match where with
393     | t when what = t -> true
394     | C.Appl l -> List.exists (occurs_check subst what) l
395     | C.Meta _ ->
396         let t = lookup where subst in
397         if t <> where then occurs_check subst what t else false
398     | _ -> false
399   in
400   let rec unif subst menv s t =
401 (*     Printf.printf "unif %s %s\n%s\n" (CicPp.ppterm s) (CicPp.ppterm t) *)
402 (*       (print_subst subst); *)
403 (*     print_newline (); *)
404     let s = match s with C.Meta _ -> lookup s subst | _ -> s
405     and t = match t with C.Meta _ -> lookup t subst | _ -> t
406     in
407     (*       Printf.printf "after apply_subst: %s %s\n%s" *)
408     (*         (CicPp.ppterm s) (CicPp.ppterm t) (print_subst subst); *)
409     (*       print_newline (); *)
410     match s, t with
411     | s, t when s = t -> subst, menv
412     | C.Meta (i, _), C.Meta (j, _) when i > j ->
413         unif subst menv t s
414     | C.Meta _, t when occurs_check subst s t ->
415         raise (U.UnificationFailure "Inference.unification.unif")
416 (*     | C.Meta (i, l), C.Meta (j, l') -> *)
417 (*         let _, _, ty = CicUtil.lookup_meta i menv in *)
418 (*         let _, _, ty' = CicUtil.lookup_meta j menv in *)
419 (*         let binding1 = lookup s subst in *)
420 (*         let binding2 = lookup t subst in *)
421 (*         let subst, menv =  *)
422 (*           if binding1 != s then *)
423 (*             if binding2 != t then *)
424 (*               unif subst menv binding1 binding2 *)
425 (*             else *)
426 (*               if binding1 = t then *)
427 (*                 subst, menv *)
428 (*               else *)
429 (*                 ((j, (context, binding1, ty'))::subst, *)
430 (*                  List.filter (fun (m, _, _) -> j <> m) menv) *)
431 (*           else *)
432 (*             if binding2 != t then *)
433 (*               if s = binding2 then *)
434 (*                 subst, menv *)
435 (*               else *)
436 (*                 ((i, (context, binding2, ty))::subst, *)
437 (*                  List.filter (fun (m, _, _) -> i <> m) menv) *)
438 (*             else *)
439 (*               ((i, (context, t, ty))::subst, *)
440 (*                List.filter (fun (m, _, _) -> i <> m) menv) *)
441 (*         in *)
442 (*         subst, menv *)
443         
444     | C.Meta (i, l), t ->
445         let _, _, ty = CicUtil.lookup_meta i menv in
446         let subst =
447           if not (List.mem_assoc i subst) then (i, (context, t, ty))::subst
448           else subst
449         in
450         let menv = List.filter (fun (m, _, _) -> i <> m) menv in
451         subst, menv
452     | _, C.Meta _ -> unif subst menv t s
453     | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt ->
454         raise (U.UnificationFailure "Inference.unification.unif")
455     | C.Appl (hds::tls), C.Appl (hdt::tlt) -> (
456         try
457           List.fold_left2
458             (fun (subst', menv) s t -> unif subst' menv s t)
459             (subst, menv) tls tlt
460         with e ->
461           raise (U.UnificationFailure "Inference.unification.unif")
462       )
463     | _, _ -> raise (U.UnificationFailure "Inference.unification.unif")
464   in
465   let subst, menv = unif [] metasenv t1 t2 in
466   (*     Printf.printf "DONE!: subst = \n%s\n" (print_subst subst); *)
467   (*     print_newline (); *)
468 (*   let rec fix_term = function *)
469 (*     | (C.Meta (i, l) as t) -> *)
470 (*         lookup t subst *)
471 (*     | C.Appl l -> C.Appl (List.map fix_term l) *)
472 (*     | t -> t *)
473 (*   in *)
474 (*   let rec fix_subst = function *)
475 (*     | [] -> [] *)
476 (*     | (i, (c, t, ty))::tl -> (i, (c, fix_term t, fix_term ty))::(fix_subst tl) *)
477 (*   in *)
478 (*   List.rev (fix_subst subst), menv, ugraph *)
479   List.rev subst, menv, ugraph
480 ;;
481
482
483 let unification metasenv context t1 t2 ugraph =
484 (*   Printf.printf "| unification %s %s\n" (CicPp.ppterm t1) (CicPp.ppterm t2); *)
485   let subst, menv, ug =
486     if not (is_simple_term t1) || not (is_simple_term t2) then
487       CicUnification.fo_unif metasenv context t1 t2 ugraph
488     else
489       unification_simple metasenv context t1 t2 ugraph
490   in
491   let rec fix_term = function
492     | (Cic.Meta (i, l) as t) ->
493         let t' = lookup_subst t subst in
494         if t <> t' then fix_term t' else t
495     | Cic.Appl l -> Cic.Appl (List.map fix_term l)
496     | t -> t
497   in
498   let rec fix_subst = function
499     | [] -> []
500     | (i, (c, t, ty))::tl -> (i, (c, fix_term t, fix_term ty))::(fix_subst tl)
501   in
502 (*   Printf.printf "| subst: %s\n" (print_subst ~prefix:" ; " subst); *)
503 (*   print_endline "|"; *)
504   (* fix_subst *) subst, menv, ug
505 ;;
506
507 (* let unification = CicUnification.fo_unif;; *)
508
509 exception MatchingFailure;;
510
511
512 let matching_simple metasenv context t1 t2 ugraph =
513   let module C = Cic in
514   let module M = CicMetaSubst in
515   let module U = CicUnification in
516   let lookup meta subst =
517     match meta with
518     | C.Meta (i, _) -> (
519         try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst in t
520         with Not_found -> meta
521       )
522     | _ -> assert false
523   in
524   let rec do_match subst menv s t =
525 (*     Printf.printf "do_match %s %s\n%s\n" (CicPp.ppterm s) (CicPp.ppterm t) *)
526 (*       (print_subst subst); *)
527 (*     print_newline (); *)
528 (*     let s = match s with C.Meta _ -> lookup s subst | _ -> s *)
529 (*     let t = match t with C.Meta _ -> lookup t subst | _ -> t in  *)
530     (*       Printf.printf "after apply_subst: %s %s\n%s" *)
531     (*         (CicPp.ppterm s) (CicPp.ppterm t) (print_subst subst); *)
532     (*       print_newline (); *)
533     match s, t with
534     | s, t when s = t -> subst, menv
535 (*     | C.Meta (i, _), C.Meta (j, _) when i > j -> *)
536 (*         do_match subst menv t s *)
537 (*     | C.Meta _, t when occurs_check subst s t -> *)
538 (*         raise MatchingFailure *)
539 (*     | s, C.Meta _ when occurs_check subst t s -> *)
540 (*         raise MatchingFailure *)
541     | s, C.Meta (i, l) ->
542         let filter_menv i menv =
543           List.filter (fun (m, _, _) -> i <> m) menv
544         in
545         let subst, menv =
546           let value = lookup t subst in
547           match value with
548 (*           | C.Meta (i', l') when Hashtbl.mem table i' -> *)
549 (*               (i', (context, s, ty))::subst, menv (\* filter_menv i' menv *\) *)
550           | value when value = t ->
551               let _, _, ty = CicUtil.lookup_meta i menv in
552               (i, (context, s, ty))::subst, filter_menv i menv
553           | value when value <> s ->
554               raise MatchingFailure
555           | value -> do_match subst menv s value
556         in
557         subst, menv
558 (*           else if value <> s then *)
559 (*             raise MatchingFailure *)
560 (*           else subst *)
561 (*           if not (List.mem_assoc i subst) then (i, (context, t, ty))::subst *)
562 (*           else subst *)
563 (*         in *)
564 (*         let menv = List.filter (fun (m, _, _) -> i <> m) menv in *)
565 (*         subst, menv *)
566 (*     | _, C.Meta _ -> do_match subst menv t s *)
567 (*     | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt -> *)
568 (*         raise MatchingFailure *)
569     | C.Appl ls, C.Appl lt -> (
570         try
571           List.fold_left2
572             (fun (subst, menv) s t -> do_match subst menv s t)
573             (subst, menv) ls lt
574         with e ->
575 (*           print_endline (Printexc.to_string e); *)
576 (*           Printf.printf "NO MATCH: %s %s\n" (CicPp.ppterm s) (CicPp.ppterm t); *)
577 (*           print_newline ();           *)
578           raise MatchingFailure
579       )
580     | _, _ ->
581 (*         Printf.printf "NO MATCH: %s %s\n" (CicPp.ppterm s) (CicPp.ppterm t); *)
582 (*         print_newline (); *)
583         raise MatchingFailure
584   in
585   let subst, menv = do_match [] metasenv t1 t2 in
586   (*     Printf.printf "DONE!: subst = \n%s\n" (print_subst subst); *)
587   (*     print_newline (); *)
588   subst, menv, ugraph
589 ;;
590
591
592 let matching metasenv context t1 t2 ugraph =
593 (*   if (is_simple_term t1) && (is_simple_term t2) then *)
594 (*     let subst, menv, ug = *)
595 (*       matching_simple metasenv context t1 t2 ugraph in *)
596 (* (\*     Printf.printf "matching %s %s:\n%s\n" *\) *)
597 (* (\*       (CicPp.ppterm t1) (CicPp.ppterm t2) (print_subst subst); *\) *)
598 (* (\*     print_newline (); *\) *)
599 (*     subst, menv, ug *)
600 (*   else *)
601     try
602       let subst, metasenv, ugraph =
603         (*       CicUnification.fo_unif metasenv context t1 t2 ugraph *)
604         unification metasenv context t1 t2 ugraph
605       in
606       let t' = CicMetaSubst.apply_subst subst t1 in
607       if not (meta_convertibility t1 t') then
608         raise MatchingFailure
609       else
610         let metas = metas_of_term t1 in
611         let fix_subst = function
612           | (i, (c, Cic.Meta (j, lc), ty)) when List.mem i metas ->
613               (j, (c, Cic.Meta (i, lc), ty))
614           | s -> s
615         in
616         let subst = List.map fix_subst subst in
617
618 (*         Printf.printf "matching %s %s:\n%s\n" *)
619 (*           (CicPp.ppterm t1) (CicPp.ppterm t2) (print_subst subst); *)
620 (*         print_newline (); *)
621
622         subst, metasenv, ugraph
623     with e ->
624 (*       Printf.printf "failed to match %s %s\n" *)
625 (*         (CicPp.ppterm t1) (CicPp.ppterm t2); *)
626       raise MatchingFailure
627 ;;
628
629 (* let matching = *)
630 (*   let profile = CicUtil.profile "Inference.matching" in *)
631 (*   (fun metasenv context t1 t2 ugraph -> *)
632 (*      profile (matching metasenv context t1 t2) ugraph) *)
633 (* ;; *)
634
635
636 let beta_expand ?(metas_ok=true) ?(match_only=false)
637     what type_of_what where context metasenv ugraph = 
638   let module S = CicSubstitution in
639   let module C = Cic in
640
641   let print_info = false in
642   
643 (*   let _ = *)
644 (*     let names = names_of_context context in *)
645 (*     Printf.printf "beta_expand:\nwhat: %s, %s\nwhere: %s, %s\n" *)
646 (*       (CicPp.pp what names) (CicPp.ppterm what) *)
647 (*       (CicPp.pp where names) (CicPp.ppterm where); *)
648 (*     print_newline (); *)
649 (*   in *)
650   (*
651     return value:
652     ((list of all possible beta expansions, subst, metasenv, ugraph),
653      lifted term)
654   *)
655   let rec aux lift_amount term context metasenv subst ugraph =
656 (*     Printf.printf "enter aux %s\n" (CicPp.ppterm term); *)
657     let res, lifted_term = 
658       match term with
659       | C.Rel m  ->
660           [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
661             
662       | C.Var (uri, exp_named_subst) ->
663           let ens', lifted_ens =
664             aux_ens lift_amount exp_named_subst context metasenv subst ugraph
665           in
666           let expansions = 
667             List.map
668               (fun (e, s, m, ug) ->
669                  (C.Var (uri, e), s, m, ug)) ens'
670           in
671           expansions, C.Var (uri, lifted_ens)
672             
673       | C.Meta (i, l) ->
674           let l', lifted_l = 
675             List.fold_right
676               (fun arg (res, lifted_tl) ->
677                  match arg with
678                  | Some arg ->
679                      let arg_res, lifted_arg =
680                        aux lift_amount arg context metasenv subst ugraph in
681                      let l1 =
682                        List.map
683                          (fun (a, s, m, ug) -> (Some a)::lifted_tl, s, m, ug)
684                          arg_res
685                      in
686                      (l1 @
687                         (List.map
688                            (fun (r, s, m, ug) -> (Some lifted_arg)::r, s, m, ug)
689                            res),
690                       (Some lifted_arg)::lifted_tl)
691                  | None ->
692                      (List.map
693                         (fun (r, s, m, ug) -> None::r, s, m, ug)
694                         res, 
695                       None::lifted_tl)
696               ) l ([], [])
697           in
698           let e = 
699             List.map
700               (fun (l, s, m, ug) ->
701                  (C.Meta (i, l), s, m, ug)) l'
702           in
703           e, C.Meta (i, lifted_l)
704             
705       | C.Sort _
706       | C.Implicit _ as t -> [], t
707           
708       | C.Cast (s, t) ->
709           let l1, lifted_s =
710             aux lift_amount s context metasenv subst ugraph in
711           let l2, lifted_t =
712             aux lift_amount t context metasenv subst ugraph
713           in
714           let l1' =
715             List.map
716               (fun (t, s, m, ug) ->
717                  C.Cast (t, lifted_t), s, m, ug) l1 in
718           let l2' =
719             List.map
720               (fun (t, s, m, ug) ->
721                  C.Cast (lifted_s, t), s, m, ug) l2 in
722           l1'@l2', C.Cast (lifted_s, lifted_t)
723             
724       | C.Prod (nn, s, t) ->
725           let l1, lifted_s =
726             aux lift_amount s context metasenv subst ugraph in
727           let l2, lifted_t =
728             aux (lift_amount+1) t ((Some (nn, C.Decl s))::context)
729               metasenv subst ugraph
730           in
731           let l1' =
732             List.map
733               (fun (t, s, m, ug) ->
734                  C.Prod (nn, t, lifted_t), s, m, ug) l1 in
735           let l2' =
736             List.map
737               (fun (t, s, m, ug) ->
738                  C.Prod (nn, lifted_s, t), s, m, ug) l2 in
739           l1'@l2', C.Prod (nn, lifted_s, lifted_t)
740
741       | C.Lambda (nn, s, t) ->
742           let l1, lifted_s =
743             aux lift_amount s context metasenv subst ugraph in
744           let l2, lifted_t =
745             aux (lift_amount+1) t ((Some (nn, C.Decl s))::context)
746               metasenv subst ugraph
747           in
748           let l1' =
749             List.map
750               (fun (t, s, m, ug) ->
751                  C.Lambda (nn, t, lifted_t), s, m, ug) l1 in
752           let l2' =
753             List.map
754               (fun (t, s, m, ug) ->
755                  C.Lambda (nn, lifted_s, t), s, m, ug) l2 in
756           l1'@l2', C.Lambda (nn, lifted_s, lifted_t)
757
758       | C.LetIn (nn, s, t) ->
759           let l1, lifted_s =
760             aux lift_amount s context metasenv subst ugraph in
761           let l2, lifted_t =
762             aux (lift_amount+1) t ((Some (nn, C.Def (s, None)))::context)
763               metasenv subst ugraph
764           in
765           let l1' =
766             List.map
767               (fun (t, s, m, ug) ->
768                  C.LetIn (nn, t, lifted_t), s, m, ug) l1 in
769           let l2' =
770             List.map
771               (fun (t, s, m, ug) ->
772                  C.LetIn (nn, lifted_s, t), s, m, ug) l2 in
773           l1'@l2', C.LetIn (nn, lifted_s, lifted_t)
774
775       | C.Appl l ->
776           let l', lifted_l =
777             aux_list lift_amount l context metasenv subst ugraph
778           in
779           (List.map (fun (l, s, m, ug) -> (C.Appl l, s, m, ug)) l',
780            C.Appl lifted_l)
781             
782       | C.Const (uri, exp_named_subst) ->
783           let ens', lifted_ens =
784             aux_ens lift_amount exp_named_subst context metasenv subst ugraph
785           in
786           let expansions = 
787             List.map
788               (fun (e, s, m, ug) ->
789                  (C.Const (uri, e), s, m, ug)) ens'
790           in
791           (expansions, C.Const (uri, lifted_ens))
792
793       | C.MutInd (uri, i ,exp_named_subst) ->
794           let ens', lifted_ens =
795             aux_ens lift_amount exp_named_subst context metasenv subst ugraph
796           in
797           let expansions = 
798             List.map
799               (fun (e, s, m, ug) ->
800                  (C.MutInd (uri, i, e), s, m, ug)) ens'
801           in
802           (expansions, C.MutInd (uri, i, lifted_ens))
803
804       | C.MutConstruct (uri, i, j, exp_named_subst) ->
805           let ens', lifted_ens =
806             aux_ens lift_amount exp_named_subst context metasenv subst ugraph
807           in
808           let expansions = 
809             List.map
810               (fun (e, s, m, ug) ->
811                  (C.MutConstruct (uri, i, j, e), s, m, ug)) ens'
812           in
813           (expansions, C.MutConstruct (uri, i, j, lifted_ens))
814
815       | C.MutCase (sp, i, outt, t, pl) ->
816           let pl_res, lifted_pl =
817             aux_list lift_amount pl context metasenv subst ugraph
818           in
819           let l1, lifted_outt =
820             aux lift_amount outt context metasenv subst ugraph in
821           let l2, lifted_t =
822             aux lift_amount t context metasenv subst ugraph in
823
824           let l1' =
825             List.map
826               (fun (outt, s, m, ug) ->
827                  C.MutCase (sp, i, outt, lifted_t, lifted_pl), s, m, ug) l1 in
828           let l2' =
829             List.map
830               (fun (t, s, m, ug) ->
831                  C.MutCase (sp, i, lifted_outt, t, lifted_pl), s, m, ug) l2 in
832           let l3' =
833             List.map
834               (fun (pl, s, m, ug) ->
835                  C.MutCase (sp, i, lifted_outt, lifted_t, pl), s, m, ug) pl_res
836           in
837           (l1'@l2'@l3', C.MutCase (sp, i, lifted_outt, lifted_t, lifted_pl))
838
839       | C.Fix (i, fl) ->
840           let len = List.length fl in
841           let fl', lifted_fl =
842             List.fold_right
843               (fun (nm, idx, ty, bo) (res, lifted_tl) ->
844                  let lifted_ty = S.lift lift_amount ty in
845                  let bo_res, lifted_bo =
846                    aux (lift_amount+len) bo context metasenv subst ugraph in
847                  let l1 =
848                    List.map
849                      (fun (a, s, m, ug) ->
850                         (nm, idx, lifted_ty, a)::lifted_tl, s, m, ug)
851                      bo_res
852                  in
853                  (l1 @
854                     (List.map
855                        (fun (r, s, m, ug) ->
856                           (nm, idx, lifted_ty, lifted_bo)::r, s, m, ug) res),
857                   (nm, idx, lifted_ty, lifted_bo)::lifted_tl)
858               ) fl ([], [])
859           in
860           (List.map
861              (fun (fl, s, m, ug) -> C.Fix (i, fl), s, m, ug) fl',
862            C.Fix (i, lifted_fl))
863             
864       | C.CoFix (i, fl) ->
865           let len = List.length fl in
866           let fl', lifted_fl =
867             List.fold_right
868               (fun (nm, ty, bo) (res, lifted_tl) ->
869                  let lifted_ty = S.lift lift_amount ty in
870                  let bo_res, lifted_bo =
871                    aux (lift_amount+len) bo context metasenv subst ugraph in
872                  let l1 =
873                    List.map
874                      (fun (a, s, m, ug) ->
875                         (nm, lifted_ty, a)::lifted_tl, s, m, ug)
876                      bo_res
877                  in
878                  (l1 @
879                     (List.map
880                        (fun (r, s, m, ug) ->
881                           (nm, lifted_ty, lifted_bo)::r, s, m, ug) res),
882                   (nm, lifted_ty, lifted_bo)::lifted_tl)
883               ) fl ([], [])
884           in
885           (List.map
886              (fun (fl, s, m, ug) -> C.CoFix (i, fl), s, m, ug) fl',
887            C.CoFix (i, lifted_fl))
888     in
889     let retval = 
890       match term with
891       | C.Meta _ when (not metas_ok) ->
892           res, lifted_term
893       | _ ->
894 (*           let term' = *)
895 (*             if match_only then replace_metas context term *)
896 (*             else term *)
897 (*           in *)
898           try
899             let subst', metasenv', ugraph' =
900 (*               Printf.printf "provo a unificare %s e %s\n" *)
901 (*                 (CicPp.ppterm (S.lift lift_amount what)) (CicPp.ppterm term); *)
902               if match_only then
903                 matching metasenv context term (S.lift lift_amount what) ugraph
904               else
905                 CicUnification.fo_unif metasenv context
906                   (S.lift lift_amount what) term ugraph
907             in
908 (*           Printf.printf "Ok, trovato: %s\n\nwhat: %s" (CicPp.ppterm term) *)
909 (*             (CicPp.ppterm (S.lift lift_amount what)); *)
910 (*           Printf.printf "substitution:\n%s\n\n" (print_subst subst'); *)
911 (*           Printf.printf "metasenv': %s\n" (print_metasenv metasenv'); *)
912             (* Printf.printf "metasenv: %s\n\n" (print_metasenv metasenv); *)
913 (*             if match_only then *)
914 (*               let t' = CicMetaSubst.apply_subst subst' term in *)
915 (*               if not (meta_convertibility term t') then ( *)
916 (*                 res, lifted_term *)
917 (*               ) else ( *)
918 (*                 let metas = metas_of_term term in *)
919 (*                 let fix_subst = function *)
920 (*                   | (i, (c, C.Meta (j, lc), ty)) when List.mem i metas -> *)
921 (*                       (j, (c, C.Meta (i, lc), ty)) *)
922 (*                   | s -> s *)
923 (*                 in *)
924 (*                 let subst' = List.map fix_subst subst' in *)
925 (*                 ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res, *)
926 (*                  lifted_term) *)
927 (*               ) *)
928 (*             else *)
929               ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res,
930                lifted_term)
931           with e ->
932             if print_info then (
933               print_endline ("beta_expand ERROR!: " ^ (Printexc.to_string e));
934             );
935             res, lifted_term
936     in
937 (*     Printf.printf "exit aux\n"; *)
938     retval
939
940   and aux_list lift_amount l context metasenv subst ugraph =
941     List.fold_right
942       (fun arg (res, lifted_tl) ->
943          let arg_res, lifted_arg =
944            aux lift_amount arg context metasenv subst ugraph in
945          let l1 = List.map
946            (fun (a, s, m, ug) -> a::lifted_tl, s, m, ug) arg_res
947          in
948          (l1 @ (List.map
949                   (fun (r, s, m, ug) -> lifted_arg::r, s, m, ug) res),
950           lifted_arg::lifted_tl)
951       ) l ([], [])
952
953   and aux_ens lift_amount exp_named_subst context metasenv subst ugraph =
954     List.fold_right
955       (fun (u, arg) (res, lifted_tl) ->
956          let arg_res, lifted_arg =
957            aux lift_amount arg context metasenv subst ugraph in
958          let l1 =
959            List.map
960              (fun (a, s, m, ug) -> (u, a)::lifted_tl, s, m, ug) arg_res
961          in
962          (l1 @ (List.map (fun (r, s, m, ug) ->
963                             (u, lifted_arg)::r, s, m, ug) res),
964           (u, lifted_arg)::lifted_tl)
965       ) exp_named_subst ([], [])
966
967   in
968   let expansions, _ =
969 (*     let where = *)
970 (*       if match_only then replace_metas (\* context *\) where *)
971 (*       else where *)
972 (*     in *)
973     if print_info then (
974       Printf.printf "searching %s inside %s\n"
975         (CicPp.ppterm what) (CicPp.ppterm where);
976     );
977     aux 0 where context metasenv [] ugraph
978   in
979   let mapfun =
980 (*     if match_only then *)
981 (*       (fun (term, subst, metasenv, ugraph) -> *)
982 (*          let term' = *)
983 (*            C.Lambda (C.Anonymous, type_of_what, restore_metas term) *)
984 (*          and subst = restore_subst subst in *)
985 (*          (term', subst, metasenv, ugraph)) *)
986 (*     else *)
987       (fun (term, subst, metasenv, ugraph) ->
988          let term' = C.Lambda (C.Anonymous, type_of_what, term) in
989          (term', subst, metasenv, ugraph))
990   in
991   List.map mapfun expansions
992 ;;
993
994
995 let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =
996   let module C = Cic in
997   let module S = CicSubstitution in
998   let module T = CicTypeChecker in
999   let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
1000   let rec aux index newmeta = function
1001     | [] -> [], newmeta
1002     | (Some (_, C.Decl (term)))::tl ->
1003         let do_find context term =
1004           match term with
1005           | C.Prod (name, s, t) ->
1006 (*               let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in *)
1007               let (head, newmetas, args, _) =
1008                 PrimitiveTactics.new_metasenv_for_apply newmeta proof
1009                   context (S.lift index term)
1010               in
1011               let newmeta =
1012                 List.fold_left
1013                   (fun maxm arg ->
1014                      match arg with
1015                      | C.Meta (i, _) -> (max maxm i)
1016                      | _ -> assert false)
1017                   newmeta args
1018               in
1019               let p =
1020                 if List.length args = 0 then
1021                   C.Rel index
1022                 else
1023                   C.Appl ((C.Rel index)::args)
1024               in (
1025                 match head with
1026                 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
1027                     Printf.printf "OK: %s\n" (CicPp.ppterm term);
1028                     let o = !Utils.compare_terms t1 t2 in
1029                     let w = compute_equality_weight ty t1 t2 in
1030                     let e = (w, (ty, t1, t2, o), newmetas, args) in
1031                     store_proof e (BasicProof p);
1032                     Some e, (newmeta+1)
1033                 | _ -> None, newmeta
1034               )
1035           | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
1036               let t1 = S.lift index t1
1037               and t2 = S.lift index t2 in
1038               let o = !Utils.compare_terms t1 t2 in
1039               let w = compute_equality_weight ty t1 t2 in
1040               let e = (w, (ty, t1, t2, o), [], []) in
1041               store_proof e (BasicProof (C.Rel index));
1042               Some e, (newmeta+1)
1043           | _ -> None, newmeta
1044         in (
1045           match do_find context term with
1046           | Some p, newmeta ->
1047               let tl, newmeta' = (aux (index+1) newmeta tl) in
1048               p::tl, max newmeta newmeta'
1049           | None, _ ->
1050               aux (index+1) newmeta tl
1051         )
1052     | _::tl ->
1053         aux (index+1) newmeta tl
1054   in
1055   aux 1 newmeta context
1056 ;;
1057
1058
1059 let fix_metas newmeta ((weight, (ty, left, right, o), menv, args) as equality) =
1060   let table = Hashtbl.create (List.length args) in
1061   let newargs, _ =
1062     List.fold_right
1063       (fun t (newargs, index) ->
1064          match t with
1065          | Cic.Meta (i, l) ->
1066              Hashtbl.add table i index;
1067              ((Cic.Meta (index, l))::newargs, index+1)
1068          | _ -> assert false)
1069       args ([], newmeta)
1070   in
1071   let repl where =
1072     ProofEngineReduction.replace ~equality:(=) ~what:args ~with_what:newargs
1073       ~where
1074   in
1075   let menv' =
1076     List.fold_right
1077       (fun (i, context, term) menv ->
1078          try
1079            let index = Hashtbl.find table i in
1080            (index, context, term)::menv
1081          with Not_found ->
1082            (i, context, term)::menv)
1083       menv []
1084   in
1085   let ty = repl ty
1086   and left = repl left
1087   and right = repl right in
1088   let metas = (metas_of_term left) @ (metas_of_term right) in
1089   let menv' = List.filter (fun (i, _, _) -> List.mem i metas) menv'
1090   and newargs =
1091     List.filter
1092       (function Cic.Meta (i, _) -> List.mem i metas | _ -> assert false) newargs
1093   in
1094   (newmeta + (List.length newargs) + 1,
1095    (weight, (ty, left, right, o), menv', newargs))
1096 ;;
1097
1098
1099 exception TermIsNotAnEquality;;
1100
1101 let equality_of_term ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) proof = function
1102   | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
1103       let o = !Utils.compare_terms t1 t2 in
1104       let w = compute_equality_weight ty t1 t2 in
1105       let e = (w, (ty, t1, t2, o), [], []) in
1106       store_proof e (BasicProof proof);
1107       e
1108 (*       (proof, (ty, t1, t2, o), [], []) *)
1109   | _ ->
1110       raise TermIsNotAnEquality
1111 ;;
1112
1113
1114 type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
1115
1116
1117 (*
1118 let superposition_left (metasenv, context, ugraph) target source =
1119   let module C = Cic in
1120   let module S = CicSubstitution in
1121   let module M = CicMetaSubst in
1122   let module HL = HelmLibraryObjects in
1123   let module CR = CicReduction in
1124   (* we assume that target is ground (does not contain metavariables): this
1125    * should always be the case (I hope, at least) *)
1126   let proof, (eq_ty, left, right, t_order), _, _ = target in
1127   let eqproof, (ty, t1, t2, s_order), newmetas, args = source in
1128
1129   let compare_terms = !Utils.compare_terms in
1130
1131   if eq_ty <> ty then
1132     []
1133   else    
1134     let where, is_left =
1135       match t_order (* compare_terms left right *) with
1136       | Lt -> right, false
1137       | Gt -> left, true
1138       | _ -> (
1139           Printf.printf "????????? %s = %s" (CicPp.ppterm left)
1140             (CicPp.ppterm right);
1141           print_newline ();
1142           assert false (* again, for ground terms this shouldn't happen... *)
1143         )
1144     in
1145     let metasenv' = newmetas @ metasenv in
1146     let result = s_order (* compare_terms t1 t2 *) in
1147     let res1, res2 = 
1148       match result with
1149       | Gt -> (beta_expand t1 ty where context metasenv' ugraph), []
1150       | Lt -> [], (beta_expand t2 ty where context metasenv' ugraph)
1151       | _ ->
1152           let res1 =
1153             List.filter
1154               (fun (t, s, m, ug) ->
1155                  compare_terms (M.apply_subst s t1) (M.apply_subst s t2) = Gt)
1156               (beta_expand t1 ty where context metasenv' ugraph)
1157           and res2 =
1158             List.filter
1159               (fun (t, s, m, ug) ->
1160                  compare_terms (M.apply_subst s t2) (M.apply_subst s t1) = Gt)
1161               (beta_expand t2 ty where context metasenv' ugraph)
1162           in
1163           res1, res2
1164     in
1165     (*   let what, other = *)
1166     (*     if is_left then left, right *)
1167     (*     else right, left *)
1168     (*   in *)
1169     let build_new what other eq_URI (t, s, m, ug) =
1170       let newgoal, newgoalproof =
1171         match t with
1172         | C.Lambda (nn, ty, bo) ->
1173             let bo' = S.subst (M.apply_subst s other) bo in
1174             let bo'' =
1175               C.Appl (
1176                 [C.MutInd (HL.Logic.eq_URI, 0, []);
1177                  S.lift 1 eq_ty] @
1178                   if is_left then [bo'; S.lift 1 right]
1179                   else [S.lift 1 left; bo'])
1180             in
1181             let t' = C.Lambda (nn, ty, bo'') in
1182             S.subst (M.apply_subst s other) bo,
1183             M.apply_subst s
1184               (C.Appl [C.Const (eq_URI, []); ty; what; t';
1185                        proof; other; eqproof])
1186         | _ -> assert false
1187       in
1188       let equation =
1189         if is_left then (eq_ty, newgoal, right, compare_terms newgoal right)
1190         else (eq_ty, left, newgoal, compare_terms left newgoal)
1191       in
1192       (newgoalproof (* eqproof *), equation, [], [])
1193     in
1194     let new1 = List.map (build_new t1 t2 HL.Logic.eq_ind_URI) res1
1195     and new2 = List.map (build_new t2 t1 HL.Logic.eq_ind_r_URI) res2 in
1196     new1 @ new2
1197 ;;
1198
1199
1200 let superposition_right newmeta (metasenv, context, ugraph) target source =
1201   let module C = Cic in
1202   let module S = CicSubstitution in
1203   let module M = CicMetaSubst in
1204   let module HL = HelmLibraryObjects in
1205   let module CR = CicReduction in
1206   let eqproof, (eq_ty, left, right, t_order), newmetas, args = target in
1207   let eqp', (ty', t1, t2, s_order), newm', args' = source in
1208   let maxmeta = ref newmeta in
1209
1210   let compare_terms = !Utils.compare_terms in
1211
1212   if eq_ty <> ty' then
1213     newmeta, []
1214   else
1215     (*   let ok term subst other other_eq_side ugraph = *)
1216     (*     match term with *)
1217     (*     | C.Lambda (nn, ty, bo) -> *)
1218     (*         let bo' = S.subst (M.apply_subst subst other) bo in *)
1219     (*         let res, _ = CR.are_convertible context bo' other_eq_side ugraph in *)
1220     (*         not res *)
1221     (*     |  _ -> assert false *)
1222     (*   in *)
1223     let condition left right what other (t, s, m, ug) =
1224       let subst = M.apply_subst s in
1225       let cmp1 = compare_terms (subst what) (subst other) in
1226       let cmp2 = compare_terms (subst left) (subst right) in
1227       (*     cmp1 = Gt && cmp2 = Gt *)
1228       cmp1 <> Lt && cmp1 <> Le && cmp2 <> Lt && cmp2 <> Le
1229         (*     && (ok t s other right ug) *)
1230     in
1231     let metasenv' = metasenv @ newmetas @ newm' in
1232     let beta_expand = beta_expand ~metas_ok:false in
1233     let cmp1 = t_order (* compare_terms left right *)
1234     and cmp2 = s_order (* compare_terms t1 t2 *) in
1235     let res1, res2, res3, res4 =
1236       let res l r s t =
1237         List.filter
1238           (condition l r s t)
1239           (beta_expand s eq_ty l context metasenv' ugraph)
1240       in
1241       match cmp1, cmp2 with
1242       | Gt, Gt ->
1243           (beta_expand t1 eq_ty left context metasenv' ugraph), [], [], []
1244       | Gt, Lt ->
1245           [], (beta_expand t2 eq_ty left context metasenv' ugraph), [], []
1246       | Lt, Gt ->
1247           [], [], (beta_expand t1 eq_ty right context metasenv' ugraph), []
1248       | Lt, Lt ->
1249           [], [], [], (beta_expand t2 eq_ty right context metasenv' ugraph)
1250       | Gt, _ ->
1251           let res1 = res left right t1 t2
1252           and res2 = res left right t2 t1 in
1253           res1, res2, [], []
1254       | Lt, _ ->
1255           let res3 = res right left t1 t2
1256           and res4 = res right left t2 t1 in
1257           [], [], res3, res4
1258       | _, Gt ->
1259           let res1 = res left right t1 t2
1260           and res3 = res right left t1 t2 in
1261           res1, [], res3, []
1262       | _, Lt ->
1263           let res2 = res left right t2 t1
1264           and res4 = res right left t2 t1 in
1265           [], res2, [], res4
1266       | _, _ ->
1267           let res1 = res left right t1 t2
1268           and res2 = res left right t2 t1
1269           and res3 = res right left t1 t2
1270           and res4 = res right left t2 t1 in
1271           res1, res2, res3, res4
1272     in
1273     let newmetas = newmetas @ newm' in
1274     let newargs = args @ args' in
1275     let build_new what other is_left eq_URI (t, s, m, ug) =
1276       (*     let what, other = *)
1277       (*       if is_left then left, right *)
1278       (*       else right, left *)
1279       (*     in *)
1280       let newterm, neweqproof =
1281         match t with
1282         | C.Lambda (nn, ty, bo) ->
1283             let bo' = M.apply_subst s (S.subst other bo) in
1284             let bo'' =
1285               C.Appl (
1286                 [C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty] @
1287                   if is_left then [bo'; S.lift 1 right]
1288                   else [S.lift 1 left; bo'])
1289             in
1290             let t' = C.Lambda (nn, ty, bo'') in
1291             bo',
1292             M.apply_subst s
1293               (C.Appl [C.Const (eq_URI, []); ty; what; t';
1294                        eqproof; other; eqp'])
1295         | _ -> assert false
1296       in
1297       let newmeta, newequality =
1298         let left, right =
1299           if is_left then (newterm, M.apply_subst s right)
1300           else (M.apply_subst s left, newterm) in
1301         let neworder = compare_terms left right in
1302         fix_metas !maxmeta
1303           (neweqproof, (eq_ty, left, right, neworder), newmetas, newargs)
1304       in
1305       maxmeta := newmeta;
1306       newequality
1307     in
1308     let new1 = List.map (build_new t1 t2 true HL.Logic.eq_ind_URI) res1
1309     and new2 = List.map (build_new t2 t1 true HL.Logic.eq_ind_r_URI) res2
1310     and new3 = List.map (build_new t1 t2 false HL.Logic.eq_ind_URI) res3
1311     and new4 = List.map (build_new t2 t1 false HL.Logic.eq_ind_r_URI) res4 in
1312     let ok = function
1313       | _, (_, left, right, _), _, _ ->
1314           not (fst (CR.are_convertible context left right ugraph))
1315     in
1316     (!maxmeta,
1317      (List.filter ok (new1 @ new2 @ new3 @ new4)))
1318 ;;
1319 *)
1320
1321
1322 let is_identity ((_, context, ugraph) as env) = function
1323   | ((_, (ty, left, right, _), _, _) as equality) ->
1324       let res =
1325         (left = right ||
1326             (fst (CicReduction.are_convertible context left right ugraph)))
1327       in
1328 (*       if res then ( *)
1329 (*         Printf.printf "is_identity: %s" (string_of_equality ~env equality); *)
1330 (*         print_newline (); *)
1331 (*       ); *)
1332       res
1333 ;;
1334
1335
1336 (*
1337 let demodulation newmeta (metasenv, context, ugraph) target source =
1338   let module C = Cic in
1339   let module S = CicSubstitution in
1340   let module M = CicMetaSubst in
1341   let module HL = HelmLibraryObjects in
1342   let module CR = CicReduction in
1343
1344   let proof, (eq_ty, left, right, t_order), metas, args = target
1345   and proof', (ty, t1, t2, s_order), metas', args' = source in
1346
1347   let compare_terms = !Utils.compare_terms in
1348   
1349   if eq_ty <> ty then
1350     newmeta, target
1351   else
1352     let first_step, get_params = 
1353       match s_order (* compare_terms t1 t2 *) with
1354       | Gt -> 1, (function
1355                     | 1 -> true, t1, t2, HL.Logic.eq_ind_URI
1356                     | 0 -> false, t1, t2, HL.Logic.eq_ind_URI
1357                     | _ -> assert false)
1358       | Lt -> 1, (function
1359                     | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI
1360                     | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI
1361                     | _ -> assert false)
1362       | _ ->
1363           let first_step = 3 in
1364           let get_params step =
1365             match step with
1366             | 3 -> true, t1, t2, HL.Logic.eq_ind_URI
1367             | 2 -> false, t1, t2, HL.Logic.eq_ind_URI
1368             | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI
1369             | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI
1370             | _ -> assert false
1371           in
1372           first_step, get_params
1373     in
1374     let rec demodulate newmeta step metasenv target =
1375       let proof, (eq_ty, left, right, t_order), metas, args = target in
1376       let is_left, what, other, eq_URI = get_params step in
1377
1378       let env = metasenv, context, ugraph in
1379       let names = names_of_context context in
1380 (*       Printf.printf *)
1381 (*         "demodulate\ntarget: %s\nwhat: %s\nother: %s\nis_left: %s\n" *)
1382 (*         (string_of_equality ~env target) (CicPp.pp what names) *)
1383 (*         (CicPp.pp other names) (string_of_bool is_left); *)
1384 (*       Printf.printf "step: %d" step; *)
1385 (*       print_newline (); *)
1386
1387       let ok (t, s, m, ug) =
1388         compare_terms (M.apply_subst s what) (M.apply_subst s other) = Gt
1389       in
1390       let res =
1391         let r = (beta_expand ~metas_ok:false ~match_only:true
1392                    what ty (if is_left then left else right)
1393                    context (metasenv @ metas) ugraph) 
1394         in
1395 (*         let m' = metas_of_term what *)
1396 (*         and m'' = metas_of_term (if is_left then left else right) in *)
1397 (*         if (List.mem 527 m'') && (List.mem 6 m') then ( *)
1398 (*           Printf.printf *)
1399 (*             "demodulate\ntarget: %s\nwhat: %s\nother: %s\nis_left: %s\n" *)
1400 (*             (string_of_equality ~env target) (CicPp.pp what names) *)
1401 (*             (CicPp.pp other names) (string_of_bool is_left); *)
1402 (*           Printf.printf "step: %d" step; *)
1403 (*           print_newline (); *)
1404 (*           print_endline "res:"; *)
1405 (*           List.iter (fun (t, s, m, ug) -> print_endline (CicPp.pp t names)) r; *)
1406 (*           print_newline (); *)
1407 (*           Printf.printf "metasenv:\n%s\n" (print_metasenv (metasenv @ metas)); *)
1408 (*           print_newline (); *)
1409 (*         ); *)
1410         List.filter ok r
1411       in
1412       match res with
1413       | [] ->
1414           if step = 0 then newmeta, target
1415           else demodulate newmeta (step-1) metasenv target
1416       | (t, s, m, ug)::_ -> 
1417           let newterm, newproof =
1418             match t with
1419             | C.Lambda (nn, ty, bo) ->
1420 (*                 let bo' = M.apply_subst s (S.subst other bo) in *)
1421                 let bo' = S.subst (M.apply_subst s other) bo in
1422                 let bo'' =
1423                   C.Appl (
1424                     [C.MutInd (HL.Logic.eq_URI, 0, []);
1425                      S.lift 1 eq_ty] @
1426                       if is_left then [bo'; S.lift 1 right]
1427                       else [S.lift 1 left; bo'])
1428                 in
1429                 let t' = C.Lambda (nn, ty, bo'') in
1430 (*                 M.apply_subst s (S.subst other bo), *)
1431                 bo', 
1432                 M.apply_subst s
1433                   (C.Appl [C.Const (eq_URI, []); ty; what; t';
1434                            proof; other; proof'])
1435             | _ -> assert false
1436           in
1437           let newmeta, newtarget =
1438             let left, right =
1439 (*               if is_left then (newterm, M.apply_subst s right) *)
1440 (*               else (M.apply_subst s left, newterm) in *)
1441               if is_left then newterm, right
1442               else left, newterm
1443             in
1444             let neworder = compare_terms left right in
1445 (*             let newmetasenv = metasenv @ metas in *)
1446 (*             let newargs = args @ args' in *)
1447 (*             fix_metas newmeta *)
1448 (*               (newproof, (eq_ty, left, right), newmetasenv, newargs) *)
1449             let m = (metas_of_term left) @ (metas_of_term right) in
1450             let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas
1451             and newargs =
1452               List.filter
1453                 (function C.Meta (i, _) -> List.mem i m | _ -> assert false)
1454                 args
1455             in
1456             newmeta,
1457             (newproof, (eq_ty, left, right, neworder), newmetasenv, newargs)
1458           in
1459 (*           Printf.printf *)
1460 (*             "demodulate, newtarget: %s\ntarget was: %s\n" *)
1461 (*             (string_of_equality ~env newtarget) *)
1462 (*             (string_of_equality ~env target); *)
1463 (* (\*           let _, _, newm, newa = newtarget in *\) *)
1464 (* (\*           Printf.printf "newmetasenv:\n%s\nnewargs:\n%s\n" *\) *)
1465 (* (\*             (print_metasenv newm) *\) *)
1466 (* (\*             (String.concat "\n" (List.map CicPp.ppterm newa)); *\) *)
1467 (*           print_newline (); *)
1468           if is_identity env newtarget then
1469             newmeta, newtarget
1470           else
1471             demodulate newmeta first_step metasenv newtarget
1472     in
1473     demodulate newmeta first_step (metasenv @ metas') target
1474 ;;
1475
1476
1477 (*
1478 let demodulation newmeta env target source =
1479   newmeta, target
1480 ;;
1481 *)
1482
1483
1484 let subsumption env target source =
1485   let _, (ty, tl, tr, _), tmetas, _ = target
1486   and _, (ty', sl, sr, _), smetas, _ = source in
1487   if ty <> ty' then
1488     false
1489   else
1490     let metasenv, context, ugraph = env in
1491     let metasenv = metasenv @ tmetas @ smetas in
1492     let names = names_of_context context in
1493     let samesubst subst subst' =
1494 (*       Printf.printf "samesubst:\nsubst: %s\nsubst': %s\n" *)
1495 (*         (print_subst subst) (print_subst subst'); *)
1496 (*       print_newline (); *)
1497       let tbl = Hashtbl.create (List.length subst) in
1498       List.iter (fun (m, (c, t1, t2)) -> Hashtbl.add tbl m (c, t1, t2)) subst;
1499       List.for_all
1500         (fun (m, (c, t1, t2)) ->
1501            try
1502              let c', t1', t2' = Hashtbl.find tbl m in
1503              if (c = c') && (t1 = t1') && (t2 = t2') then true
1504              else false
1505            with Not_found ->
1506              true)
1507         subst'
1508     in
1509     let subsaux left right left' right' =
1510       try
1511         let subst, menv, ug = matching metasenv context left left' ugraph
1512         and subst', menv', ug' = matching metasenv context right right' ugraph
1513         in
1514 (*         Printf.printf "left = right: %s = %s\n" *)
1515 (*           (CicPp.pp left names) (CicPp.pp right names); *)
1516 (*         Printf.printf "left' = right': %s = %s\n" *)
1517 (*           (CicPp.pp left' names) (CicPp.pp right' names);         *)
1518         samesubst subst subst'
1519       with e ->
1520 (*         print_endline (Printexc.to_string e); *)
1521         false
1522     in
1523     let res = 
1524       if subsaux tl tr sl sr then true
1525       else subsaux tl tr sr sl
1526     in
1527     if res then (
1528       Printf.printf "subsumption!:\ntarget: %s\nsource: %s\n"
1529         (string_of_equality ~env target) (string_of_equality ~env source);
1530       print_newline ();
1531     );
1532     res
1533 ;;
1534 *)
1535
1536
1537 let extract_differing_subterms t1 t2 =
1538   let module C = Cic in
1539   let rec aux t1 t2 =
1540     match t1, t2 with
1541     | C.Appl l1, C.Appl l2 when (List.length l1) <> (List.length l2) ->
1542         [(t1, t2)]
1543     | C.Appl (h1::tl1), C.Appl (h2::tl2) ->
1544         let res = List.concat (List.map2 aux tl1 tl2) in
1545         if h1 <> h2 then
1546           if res = [] then [(h1, h2)] else [(t1, t2)]
1547         else
1548           if List.length res > 1 then [(t1, t2)] else res
1549     | t1, t2 ->
1550         if t1 <> t2 then [(t1, t2)] else []
1551   in
1552   let res = aux t1 t2 in
1553   match res with
1554   | hd::[] -> Some hd
1555   | _ -> None
1556 ;;