]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/paramodulation/indexing.ml
removed a comment/bug report about let..in rendering, now fixed
[helm.git] / helm / ocaml / paramodulation / indexing.ml
1
2 let debug_print = Utils.debug_print;;
3
4
5 type retrieval_mode = Matching | Unification;;
6
7
8 let print_candidates mode term res =
9   let _ =
10     match mode with
11     | Matching ->
12         Printf.printf "| candidates Matching %s\n" (CicPp.ppterm term)
13     | Unification ->
14         Printf.printf "| candidates Unification %s\n" (CicPp.ppterm term)
15   in
16   print_endline
17     (String.concat "\n"
18        (List.map
19           (fun (p, e) ->
20              Printf.sprintf "| (%s, %s)" (Utils.string_of_pos p)
21                (Inference.string_of_equality e))
22           res));
23   print_endline "|";
24 ;;
25
26
27 let indexing_retrieval_time = ref 0.;;
28
29
30 (* let my_apply_subst subst term = *)
31 (*   let module C = Cic in *)
32 (*   let lookup lift_amount meta = *)
33 (*     match meta with *)
34 (*     | C.Meta (i, _) -> ( *)
35 (*         try *)
36 (*           let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst in *)
37 (*           (\* CicSubstitution.lift lift_amount  *\)t *)
38 (*         with Not_found -> meta *)
39 (*       ) *)
40 (*     | _ -> assert false *)
41 (*   in *)
42 (*   let rec apply_aux lift_amount =  function *)
43 (*     | C.Meta (i, l) as t -> lookup lift_amount t *)
44 (*     | C.Appl l -> C.Appl (List.map (apply_aux lift_amount) l) *)
45 (*     | C.Prod (nn, s, t) -> *)
46 (*         C.Prod (nn, apply_aux lift_amount s, apply_aux (lift_amount+1) t) *)
47 (*     | C.Lambda (nn, s, t) -> *)
48 (*         C.Lambda (nn, apply_aux lift_amount s, apply_aux (lift_amount+1) t) *)
49 (*     | t -> t *)
50 (*   in *)
51 (*   apply_aux 0 term *)
52 (* ;; *)
53
54
55 (* let apply_subst subst term = *)
56 (*   Printf.printf "| apply_subst:\n| subst: %s\n| term: %s\n" *)
57 (*     (Utils.print_subst ~prefix:" ; " subst) (CicPp.ppterm term); *)
58 (*   let res = my_apply_subst subst term in *)
59 (* (\*   let res = CicMetaSubst.apply_subst subst term in *\) *)
60 (*   Printf.printf "| res: %s\n" (CicPp.ppterm res); *)
61 (*   print_endline "|"; *)
62 (*   res *)
63 (* ;; *)
64
65 (* let apply_subst = my_apply_subst *)
66 let apply_subst = CicMetaSubst.apply_subst
67
68
69 let apply_subst =
70   let profile = CicUtil.profile "apply_subst" in
71   (fun s a -> profile (apply_subst s) a)
72 ;;
73
74
75 (*
76 (* NO INDEXING *)
77 let empty_table () = []
78
79 let index table equality =
80   let _, _, (_, l, r, ordering), _, _ = equality in
81   match ordering with
82   | Utils.Gt -> (Utils.Left, equality)::table
83   | Utils.Lt -> (Utils.Right, equality)::table
84   | _ -> (Utils.Left, equality)::(Utils.Right, equality)::table
85 ;;
86
87 let remove_index table equality =
88   List.filter (fun (p, e) -> e != equality) table
89 ;;
90
91 let in_index table equality =
92   List.exists (fun (p, e) -> e == equality) table
93 ;;
94
95 let get_candidates mode table term = table
96 *)
97
98
99 (*
100 (* PATH INDEXING *)
101 let empty_table () =
102   Path_indexing.PSTrie.empty
103 ;;
104
105 let index = Path_indexing.index
106 and remove_index = Path_indexing.remove_index
107 and in_index = Path_indexing.in_index;;
108   
109 let get_candidates mode trie term =
110   let t1 = Unix.gettimeofday () in
111   let res = 
112     let s = 
113       match mode with
114       | Matching -> Path_indexing.retrieve_generalizations trie term
115       | Unification -> Path_indexing.retrieve_unifiables trie term
116 (*       Path_indexing.retrieve_all trie term *)
117     in
118     Path_indexing.PosEqSet.elements s
119   in
120 (*   print_candidates mode term res; *)
121   let t2 = Unix.gettimeofday () in
122   indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
123   res
124 ;;
125 *)
126
127
128 (* DISCRIMINATION TREES *)
129 let empty_table () =
130   Discrimination_tree.DiscriminationTree.empty
131 ;;
132
133 let index = Discrimination_tree.index
134 and remove_index = Discrimination_tree.remove_index
135 and in_index = Discrimination_tree.in_index;;
136
137 let get_candidates mode tree term =
138   let t1 = Unix.gettimeofday () in
139   let res =
140     let s = 
141       match mode with
142       | Matching -> Discrimination_tree.retrieve_generalizations tree term
143       | Unification -> Discrimination_tree.retrieve_unifiables tree term
144     in
145     Discrimination_tree.PosEqSet.elements s
146   in
147 (*   print_candidates mode term res; *)
148 (*   print_endline (Discrimination_tree.string_of_discrimination_tree tree); *)
149 (*   print_newline (); *)
150   let t2 = Unix.gettimeofday () in
151   indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
152   res
153 ;;
154
155
156 (* let get_candidates = *)
157 (*   let profile = CicUtil.profile "Indexing.get_candidates" in *)
158 (*   (fun mode tree term -> profile (get_candidates mode tree) term) *)
159 (* ;; *)
160
161
162 let match_unif_time_ok = ref 0.;;
163 let match_unif_time_no = ref 0.;;
164
165
166 let rec find_matches metasenv context ugraph lift_amount term termty =
167   let module C = Cic in
168   let module U = Utils in
169   let module S = CicSubstitution in
170   let module M = CicMetaSubst in
171   let module HL = HelmLibraryObjects in
172   let cmp = !Utils.compare_terms in
173 (*   let names = Utils.names_of_context context in *)
174 (*   let termty, ugraph = *)
175 (*     CicTypeChecker.type_of_aux' metasenv context term ugraph *)
176 (*   in *)
177   function
178     | [] -> None
179     | candidate::tl ->
180         let pos, (_, proof, (ty, left, right, o), metas, args) = candidate in
181 (*         if not (fst (CicReduction.are_convertible *)
182 (*                        ~metasenv context termty ty ugraph)) then ( *)
183 (* (\*           debug_print ( *\) *)
184 (* (\*             Printf.sprintf "CANDIDATE HAS WRONG TYPE: %s required, %s found" *\) *)
185 (* (\*               (CicPp.pp termty names) (CicPp.pp ty names)); *\) *)
186 (*           find_matches metasenv context ugraph lift_amount term termty tl *)
187 (*         ) else *)
188           let do_match c other eq_URI =
189             let subst', metasenv', ugraph' =
190               let t1 = Unix.gettimeofday () in
191               try
192                 let r =
193                   Inference.matching (metasenv @ metas) context
194                     term (S.lift lift_amount c) ugraph in
195                 let t2 = Unix.gettimeofday () in
196                 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
197                 r
198               with Inference.MatchingFailure as e ->
199                 let t2 = Unix.gettimeofday () in
200                 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
201                 raise e
202             in
203             Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
204                   (candidate, eq_URI))
205           in
206           let c, other, eq_URI =
207             if pos = Utils.Left then left, right, HL.Logic.eq_ind_URI
208             else right, left, HL.Logic.eq_ind_r_URI
209           in
210           if o <> U.Incomparable then
211             try
212               do_match c other eq_URI
213             with Inference.MatchingFailure ->
214               find_matches metasenv context ugraph lift_amount term termty tl
215           else
216             let res =
217               try do_match c other eq_URI
218               with Inference.MatchingFailure -> None
219             in
220             match res with
221             | Some (_, s, _, _, _) ->
222                 let c' = (* M. *)apply_subst s c
223                 and other' = (* M. *)apply_subst s other in
224                 let order = cmp c' other' in
225                 let names = U.names_of_context context in
226                 if order = U.Gt then
227                   res
228                 else
229                   find_matches
230                     metasenv context ugraph lift_amount term termty tl
231             | None ->
232                 find_matches metasenv context ugraph lift_amount term termty tl
233 ;;
234
235
236 let rec find_all_matches ?(unif_fun=Inference.unification)
237     metasenv context ugraph lift_amount term termty =
238   let module C = Cic in
239   let module U = Utils in
240   let module S = CicSubstitution in
241   let module M = CicMetaSubst in
242   let module HL = HelmLibraryObjects in
243   let cmp = !Utils.compare_terms in
244 (*   let names = Utils.names_of_context context in *)
245 (*   let termty, ugraph = *)
246 (*     CicTypeChecker.type_of_aux' metasenv context term ugraph *)
247 (*   in *)
248   function
249     | [] -> []
250     | candidate::tl ->
251         let pos, (_, _, (ty, left, right, o), metas, args) = candidate in
252 (*         if not (fst (CicReduction.are_convertible *)
253 (*                        ~metasenv context termty ty ugraph)) then ( *)
254 (* (\*           debug_print ( *\) *)
255 (* (\*             Printf.sprintf "CANDIDATE HAS WRONG TYPE: %s required, %s found" *\) *)
256 (* (\*               (CicPp.pp termty names) (CicPp.pp ty names)); *\) *)
257 (*           find_all_matches ~unif_fun metasenv context ugraph *)
258 (*             lift_amount term termty tl *)
259 (*         ) else *)
260           let do_match c other eq_URI =
261             let subst', metasenv', ugraph' =
262               let t1 = Unix.gettimeofday () in
263               try
264                 let r = 
265                   unif_fun (metasenv @ metas) context
266                     term (S.lift lift_amount c) ugraph in
267                 let t2 = Unix.gettimeofday () in
268                 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
269                 r
270               with
271               | Inference.MatchingFailure
272               | CicUnification.UnificationFailure _
273               | CicUnification.Uncertain _ as e ->
274                 let t2 = Unix.gettimeofday () in
275                 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
276                 raise e
277             in
278             (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
279              (candidate, eq_URI))
280           in
281           let c, other, eq_URI =
282             if pos = Utils.Left then left, right, HL.Logic.eq_ind_URI
283             else right, left, HL.Logic.eq_ind_r_URI
284           in
285           if o <> U.Incomparable then
286             try
287               let res = do_match c other eq_URI in
288               res::(find_all_matches ~unif_fun metasenv context ugraph
289                       lift_amount term termty tl)
290             with
291             | Inference.MatchingFailure
292             | CicUnification.UnificationFailure _
293             | CicUnification.Uncertain _ ->
294               find_all_matches ~unif_fun metasenv context ugraph
295                 lift_amount term termty tl
296           else
297             try
298               let res = do_match c other eq_URI in
299               match res with
300               | _, s, _, _, _ ->
301                   let c' = (* M. *)apply_subst s c
302                   and other' = (* M. *)apply_subst s other in
303                   let order = cmp c' other' in
304                   let names = U.names_of_context context in
305                   if order <> U.Lt && order <> U.Le then
306                     res::(find_all_matches ~unif_fun metasenv context ugraph
307                             lift_amount term termty tl)
308                   else
309                     find_all_matches ~unif_fun metasenv context ugraph
310                       lift_amount term termty tl
311             with
312             | Inference.MatchingFailure
313             | CicUnification.UnificationFailure _
314             | CicUnification.Uncertain _ ->
315                 find_all_matches ~unif_fun metasenv context ugraph
316                   lift_amount term termty tl
317 ;;
318
319
320 let subsumption env table target =
321   let _, (ty, left, right, _), tmetas, _ = target in
322   let metasenv, context, ugraph = env in
323   let metasenv = metasenv @ tmetas in
324   let samesubst subst subst' =
325     let tbl = Hashtbl.create (List.length subst) in
326     List.iter (fun (m, (c, t1, t2)) -> Hashtbl.add tbl m (c, t1, t2)) subst;
327     List.for_all
328       (fun (m, (c, t1, t2)) ->
329          try
330            let c', t1', t2' = Hashtbl.find tbl m in
331            if (c = c') && (t1 = t1') && (t2 = t2') then true
332            else false
333          with Not_found ->
334            true)
335       subst'
336   in
337   let leftr =
338     match left with
339     | Cic.Meta _ -> []
340     | _ ->
341         let leftc = get_candidates Matching table left in
342         find_all_matches ~unif_fun:Inference.matching
343           metasenv context ugraph 0 left ty leftc
344   in
345   let ok what (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), _, _)), _)) =
346     try
347       let other = if pos = Utils.Left then r else l in
348       let subst', menv', ug' =
349         let t1 = Unix.gettimeofday () in
350         try
351           let r = 
352             Inference.matching metasenv context what other ugraph in
353           let t2 = Unix.gettimeofday () in
354           match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
355           r
356         with Inference.MatchingFailure as e ->
357           let t2 = Unix.gettimeofday () in
358           match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
359           raise e
360       in
361       samesubst subst subst'
362     with Inference.MatchingFailure ->
363       false
364   in
365   let r = List.exists (ok right) leftr in
366   if r then
367     true
368   else
369     let rightr =
370       match right with
371       | Cic.Meta _ -> []
372       | _ ->
373           let rightc = get_candidates Matching table right in
374           find_all_matches ~unif_fun:Inference.matching
375             metasenv context ugraph 0 right ty rightc
376     in
377     List.exists (ok left) rightr
378 ;;
379
380
381 let rec demodulate_term metasenv context ugraph table lift_amount term =
382   let module C = Cic in
383   let module S = CicSubstitution in
384   let module M = CicMetaSubst in
385   let module HL = HelmLibraryObjects in
386   let candidates = get_candidates Matching table term in
387   match term with
388   | C.Meta _ -> None
389   | term ->
390       let termty, ugraph =
391         C.Implicit None, ugraph
392 (*         CicTypeChecker.type_of_aux' metasenv context term ugraph *)
393       in
394       let res =
395         find_matches metasenv context ugraph lift_amount term termty candidates
396       in
397       if res <> None then
398         res
399       else
400         match term with
401         | C.Appl l ->
402             let res, ll = 
403               List.fold_left
404                 (fun (res, tl) t ->
405                    if res <> None then
406                      (res, tl @ [S.lift 1 t])
407                    else 
408                      let r =
409                        demodulate_term metasenv context ugraph table
410                          lift_amount t
411                      in
412                      match r with
413                      | None -> (None, tl @ [S.lift 1 t])
414                      | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
415                 (None, []) l
416             in (
417               match res with
418               | None -> None
419               | Some (_, subst, menv, ug, eq_found) ->
420                   Some (C.Appl ll, subst, menv, ug, eq_found)
421             )
422         | C.Prod (nn, s, t) ->
423             let r1 =
424               demodulate_term metasenv context ugraph table lift_amount s in (
425               match r1 with
426               | None ->
427                   let r2 =
428                     demodulate_term metasenv
429                       ((Some (nn, C.Decl s))::context) ugraph
430                       table (lift_amount+1) t
431                   in (
432                     match r2 with
433                     | None -> None
434                     | Some (t', subst, menv, ug, eq_found) ->
435                         Some (C.Prod (nn, (S.lift 1 s), t'),
436                               subst, menv, ug, eq_found)
437                   )
438               | Some (s', subst, menv, ug, eq_found) ->
439                   Some (C.Prod (nn, s', (S.lift 1 t)),
440                         subst, menv, ug, eq_found)
441             )
442         | t ->
443             None
444 ;;
445
446
447 let build_ens_for_sym_eq ty x y = 
448   [(UriManager.uri_of_string
449       "cic:/Coq/Init/Logic/Logic_lemmas/equality/A.var", ty);
450    (UriManager.uri_of_string
451       "cic:/Coq/Init/Logic/Logic_lemmas/equality/x.var", x);
452    (UriManager.uri_of_string
453       "cic:/Coq/Init/Logic/Logic_lemmas/equality/y.var", y)]
454 ;;
455
456
457 let build_newtarget_time = ref 0.;;
458
459
460 let demod_counter = ref 1;;
461
462 let rec demodulation newmeta env table sign target =
463   let module C = Cic in
464   let module S = CicSubstitution in
465   let module M = CicMetaSubst in
466   let module HL = HelmLibraryObjects in
467   let metasenv, context, ugraph = env in
468   let _, proof, (eq_ty, left, right, order), metas, args = target in
469   let metasenv' = metasenv @ metas in
470
471   let maxmeta = ref newmeta in
472   
473   let build_newtarget is_left (t, subst, menv, ug, (eq_found, eq_URI)) =
474     let time1 = Unix.gettimeofday () in
475     
476     let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
477     let what, other = if pos = Utils.Left then what, other else other, what in
478     let newterm, newproof =
479       let bo = (* M. *)apply_subst subst (S.subst other t) in
480       let t' =
481         let name = C.Name ("x_Demod_" ^ (string_of_int !demod_counter)) in
482         incr demod_counter;
483         let l, r =
484           if is_left then t, S.lift 1 right else S.lift 1 left, t in
485         (name, ty, S.lift 1 eq_ty, l, r)
486       in
487       if sign = Utils.Positive then
488         (bo,
489          Inference.ProofBlock (subst, eq_URI, t', eq_found, proof))
490       else
491         let metaproof = 
492           incr maxmeta;
493           let irl =
494             CicMkImplicit.identity_relocation_list_for_metavariable context in
495           Printf.printf "\nADDING META: %d\n" !maxmeta;
496           print_newline ();
497           C.Meta (!maxmeta, irl)
498         in
499         let target' =
500           let eq_found =
501             let proof' =
502               let ens =
503                 if pos = Utils.Left then
504                   build_ens_for_sym_eq ty what other
505                 else
506                   build_ens_for_sym_eq ty other what
507               in
508               Inference.ProofSymBlock (ens, proof')
509             in
510             let what, other =
511               if pos = Utils.Left then what, other else other, what
512             in
513             pos, (0, proof', (ty, other, what, Utils.Incomparable),
514                   menv', args')
515           in
516           let target_proof =
517             let pb =
518               Inference.ProofBlock (subst, eq_URI, t', eq_found,
519                                     Inference.BasicProof metaproof)
520             in
521             match proof with
522             | Inference.BasicProof _ ->
523                 print_endline "replacing a BasicProof";
524                 pb
525             | Inference.ProofGoalBlock (_, parent_eq) ->
526                 print_endline "replacing another ProofGoalBlock";
527                 Inference.ProofGoalBlock (pb, parent_eq)
528             | _ -> assert false
529           in
530           (0, target_proof, (eq_ty, left, right, order), metas, args)
531         in
532         let refl =
533           C.Appl [C.MutConstruct (* reflexivity *)
534                     (HelmLibraryObjects.Logic.eq_URI, 0, 1, []);
535                   eq_ty; if is_left then right else left]          
536         in
537         (bo,
538          Inference.ProofGoalBlock (Inference.BasicProof refl, target'))
539     in
540     let left, right = if is_left then newterm, right else left, newterm in
541     let m = (Inference.metas_of_term left) @ (Inference.metas_of_term right) in
542     let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas
543     and newargs =
544       List.filter
545         (function C.Meta (i, _) -> List.mem i m | _ -> assert false)
546         args
547     in
548     let ordering = !Utils.compare_terms left right in
549
550     let time2 = Unix.gettimeofday () in
551     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
552
553     let res =
554       let w = Utils.compute_equality_weight eq_ty left right in
555       (w, newproof, (eq_ty, left, right, ordering), newmetasenv, newargs)
556     in
557 (*     if sign = Utils.Positive then ( *)
558 (*       let newm, res = Inference.fix_metas !maxmeta res in *)
559 (*       maxmeta := newm; *)
560 (*       !maxmeta, res *)
561 (*     ) else *)
562     !maxmeta(* newmeta *), res
563   in
564   let res = demodulate_term metasenv' context ugraph table 0 left in
565 (*   let build_identity (w, p, (t, l, r, o), m, a) = *)
566 (*     match o with *)
567 (*     | Utils.Gt -> (w, p, (t, r, r, Utils.Eq), m, a) *)
568 (*     | _ -> (w, p, (t, l, l, Utils.Eq), m, a) *)
569 (*   in *)
570   match res with
571   | Some t ->
572       let newmeta, newtarget = build_newtarget true t in
573       if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
574         (Inference.meta_convertibility_eq target newtarget) then
575           newmeta, newtarget
576       else
577 (*         if subsumption env table newtarget then *)
578 (*           newmeta, build_identity newtarget *)
579 (*         else *)
580         demodulation newmeta env table sign newtarget
581   | None ->
582       let res = demodulate_term metasenv' context ugraph table 0 right in
583       match res with
584       | Some t ->
585           let newmeta, newtarget = build_newtarget false t in
586           if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
587             (Inference.meta_convertibility_eq target newtarget) then
588               newmeta, newtarget
589           else
590 (*             if subsumption env table newtarget then *)
591 (*               newmeta, build_identity newtarget *)
592 (*             else *)
593               demodulation newmeta env table sign newtarget
594       | None ->
595           newmeta, target
596 ;;
597
598
599 let rec betaexpand_term metasenv context ugraph table lift_amount term =
600   let module C = Cic in
601   let module S = CicSubstitution in
602   let module M = CicMetaSubst in
603   let module HL = HelmLibraryObjects in
604   let candidates = get_candidates Unification table term in
605   let res, lifted_term = 
606     match term with
607     | C.Meta (i, l) ->
608         let l', lifted_l = 
609           List.fold_right
610             (fun arg (res, lifted_tl) ->
611                match arg with
612                | Some arg ->
613                    let arg_res, lifted_arg =
614                      betaexpand_term metasenv context ugraph table
615                        lift_amount arg in
616                    let l1 =
617                      List.map
618                        (fun (t, s, m, ug, eq_found) ->
619                           (Some t)::lifted_tl, s, m, ug, eq_found)
620                        arg_res
621                    in
622                    (l1 @
623                       (List.map
624                          (fun (l, s, m, ug, eq_found) ->
625                             (Some lifted_arg)::l, s, m, ug, eq_found)
626                          res),
627                     (Some lifted_arg)::lifted_tl)
628                | None ->
629                    (List.map
630                       (fun (r, s, m, ug, eq_found) ->
631                          None::r, s, m, ug, eq_found) res, 
632                     None::lifted_tl)
633             ) l ([], [])
634         in
635         let e = 
636           List.map
637             (fun (l, s, m, ug, eq_found) ->
638                (C.Meta (i, l), s, m, ug, eq_found)) l'
639         in
640         e, C.Meta (i, lifted_l)
641           
642     | C.Rel m ->
643         [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
644           
645     | C.Prod (nn, s, t) ->
646         let l1, lifted_s =
647           betaexpand_term metasenv context ugraph table lift_amount s in
648         let l2, lifted_t =
649           betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
650             table (lift_amount+1) t in
651         let l1' =
652           List.map
653             (fun (t, s, m, ug, eq_found) ->
654                C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
655         and l2' =
656           List.map
657             (fun (t, s, m, ug, eq_found) ->
658                C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
659         l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
660           
661     | C.Appl l ->
662         let l', lifted_l =
663           List.fold_right
664             (fun arg (res, lifted_tl) ->
665                let arg_res, lifted_arg =
666                  betaexpand_term metasenv context ugraph table lift_amount arg
667                in
668                let l1 =
669                  List.map
670                    (fun (a, s, m, ug, eq_found) ->
671                       a::lifted_tl, s, m, ug, eq_found)
672                    arg_res
673                in
674                (l1 @
675                   (List.map
676                      (fun (r, s, m, ug, eq_found) ->
677                         lifted_arg::r, s, m, ug, eq_found)
678                      res),
679                 lifted_arg::lifted_tl)
680             ) l ([], [])
681         in
682         (List.map
683            (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
684          C.Appl lifted_l)
685
686     | t -> [], (S.lift lift_amount t)
687   in
688   match term with
689   | C.Meta _ -> res, lifted_term
690   | term ->
691       let termty, ugraph =
692         C.Implicit None, ugraph
693 (*         CicTypeChecker.type_of_aux' metasenv context term ugraph *)
694       in
695       let r = 
696         find_all_matches
697           metasenv context ugraph lift_amount term termty candidates
698       in
699       r @ res, lifted_term
700 ;;
701
702
703 let sup_l_counter = ref 1;;
704
705 let superposition_left newmeta (metasenv, context, ugraph) table target =
706   let module C = Cic in
707   let module S = CicSubstitution in
708   let module M = CicMetaSubst in
709   let module HL = HelmLibraryObjects in
710   let module CR = CicReduction in
711   let module U = Utils in
712   let weight, proof, (eq_ty, left, right, ordering), _, _ = target in
713   let expansions, _ =
714     let term = if ordering = U.Gt then left else right in
715     betaexpand_term metasenv context ugraph table 0 term
716   in
717   let maxmeta = ref newmeta in
718   let build_new (bo, s, m, ug, (eq_found, eq_URI)) =
719
720     print_endline "\nSUPERPOSITION LEFT\n";
721     
722     let time1 = Unix.gettimeofday () in
723     
724     let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
725     let what, other = if pos = Utils.Left then what, other else other, what in
726     let newgoal, newproof =
727       let bo' = (* M. *)apply_subst s (S.subst other bo) in
728       let t' =
729         let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in
730         incr sup_l_counter;
731         let l, r =
732           if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
733         (name, ty, S.lift 1 eq_ty, l, r)
734       in
735 (*       let bo'' = *)
736 (*         C.Appl ( *)
737 (*           [C.MutInd (HL.Logic.eq_URI, 0, []); *)
738 (*            S.lift 1 eq_ty] @ *)
739 (*             if ordering = U.Gt then [S.lift 1 bo'; S.lift 1 right] *)
740 (*             else [S.lift 1 left; S.lift 1 bo']) *)
741 (*       in *)
742 (*       let t' = *)
743 (*         let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in *)
744 (*         incr sup_l_counter; *)
745 (*         C.Lambda (name, ty, bo'') *)
746 (*       in *)
747       incr maxmeta;
748       let metaproof =
749         let irl =
750           CicMkImplicit.identity_relocation_list_for_metavariable context in
751         C.Meta (!maxmeta, irl)
752       in
753       let target' =
754         let eq_found =
755           let proof' =
756             let ens =
757               if pos = Utils.Left then
758                 build_ens_for_sym_eq ty what other
759               else
760                 build_ens_for_sym_eq ty other what
761             in
762             Inference.ProofSymBlock (ens, proof')
763           in
764           let what, other =
765             if pos = Utils.Left then what, other else other, what
766           in
767           pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args')
768         in
769         let target_proof =
770           let pb =
771             Inference.ProofBlock (s, eq_URI, t', eq_found,
772                                   Inference.BasicProof metaproof)
773           in
774           match proof with
775           | Inference.BasicProof _ ->
776               print_endline "replacing a BasicProof";
777               pb
778           | Inference.ProofGoalBlock (_, parent_eq) ->
779               print_endline "replacing another ProofGoalBlock";
780               Inference.ProofGoalBlock (pb, parent_eq)
781           | _ -> assert false
782         in
783         (weight, target_proof, (eq_ty, left, right, ordering), [], [])
784       in
785       let refl =
786         C.Appl [C.MutConstruct (* reflexivity *)
787                   (HelmLibraryObjects.Logic.eq_URI, 0, 1, []);
788                 eq_ty; if ordering = U.Gt then right else left]
789       in
790       (bo',
791        Inference.ProofGoalBlock (Inference.BasicProof refl, target'))
792     in
793     let left, right =
794       if ordering = U.Gt then newgoal, right else left, newgoal in
795     let neworder = !Utils.compare_terms left right in
796
797     let time2 = Unix.gettimeofday () in
798     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
799
800     let res =
801       let w = Utils.compute_equality_weight eq_ty left right in
802       (w, newproof, (eq_ty, left, right, neworder), [], [])
803     in
804     res
805   in
806   !maxmeta, List.map build_new expansions
807 ;;
808
809
810 let sup_r_counter = ref 1;;
811
812 let superposition_right newmeta (metasenv, context, ugraph) table target =
813   let module C = Cic in
814   let module S = CicSubstitution in
815   let module M = CicMetaSubst in
816   let module HL = HelmLibraryObjects in
817   let module CR = CicReduction in
818   let module U = Utils in
819   let _, eqproof, (eq_ty, left, right, ordering), newmetas, args = target in
820   let metasenv' = metasenv @ newmetas in
821   let maxmeta = ref newmeta in
822   let res1, res2 =
823     match ordering with
824     | U.Gt -> fst (betaexpand_term metasenv' context ugraph table 0 left), []
825     | U.Lt -> [], fst (betaexpand_term metasenv' context ugraph table 0 right)
826     | _ ->
827         let res l r =
828           List.filter
829             (fun (_, subst, _, _, _) ->
830                let subst = (* M. *)apply_subst subst in
831                let o = !Utils.compare_terms (subst l) (subst r) in
832                o <> U.Lt && o <> U.Le)
833             (fst (betaexpand_term metasenv' context ugraph table 0 l))
834         in
835         (res left right), (res right left)
836   in
837   let build_new ordering (bo, s, m, ug, (eq_found, eq_URI)) =
838
839     let time1 = Unix.gettimeofday () in
840     
841     let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
842     let what, other = if pos = Utils.Left then what, other else other, what in
843     let newgoal, newproof =
844       let bo' = (* M. *)apply_subst s (S.subst other bo) in
845       let t' =
846         let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in
847         incr sup_r_counter;
848         let l, r =
849           if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
850         (name, ty, S.lift 1 eq_ty, l, r)
851       in
852 (*       let bo'' = *)
853 (*         C.Appl ( *)
854 (*           [C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty] @ *)
855 (*             if ordering = U.Gt then [S.lift 1 bo'; S.lift 1 right] *)
856 (*             else [S.lift 1 left; S.lift 1 bo']) *)
857 (*       in *)
858 (*       let t' = *)
859 (*         let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in *)
860 (*         incr sup_r_counter; *)
861 (*         C.Lambda (name, ty, bo'') *)
862 (*       in *)
863       bo',
864       Inference.ProofBlock (s, eq_URI, t', eq_found, eqproof(* target *))
865 (*       (\* M. *\)apply_subst s *)
866 (*         (C.Appl [C.Const (eq_URI, []); ty; what; t'; *)
867 (*                  eqproof; other; proof']) *)
868     in
869     let newmeta, newequality = 
870       let left, right =
871         if ordering = U.Gt then newgoal, (* M. *)apply_subst s right
872         else (* M. *)apply_subst s left, newgoal in
873       let neworder = !Utils.compare_terms left right 
874       and newmenv = newmetas @ menv'
875       and newargs = args @ args' in
876       let eq' =
877         let w = Utils.compute_equality_weight eq_ty left right in
878         (w, newproof, (eq_ty, left, right, neworder), newmenv, newargs)
879       and env = (metasenv, context, ugraph) in
880       let newm, eq' = Inference.fix_metas !maxmeta eq' in
881       newm, eq'
882     in
883     maxmeta := newmeta;
884
885     let time2 = Unix.gettimeofday () in
886     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
887
888     newequality
889   in
890
891 (*   let build_new = *)
892 (*     let profile = CicUtil.profile "Indexing.superposition_right.build_new" in *)
893 (*     (fun o e -> profile (build_new o) e) *)
894 (*   in *)
895   
896   let new1 = List.map (build_new U.Gt) res1
897   and new2 = List.map (build_new U.Lt) res2 in
898   let ok = function
899     | _, _, (_, left, right, _), _, _ ->
900         not (fst (CR.are_convertible context left right ugraph))
901   in
902   (!maxmeta,
903    (List.filter ok (new1 @ new2)))
904 ;;