]> matita.cs.unibo.it Git - helm.git/blob - components/tactics/paramodulation/indexing.ml
Bug fixed in injection: lifting was not performed correctly, but it worked
[helm.git] / components / tactics / paramodulation / indexing.ml
1 (* Copyright (C) 2005, HELM Team.
2  * 
3  * This file is part of HELM, an Hypertextual, Electronic
4  * Library of Mathematics, developed at the Computer Science
5  * Department, University of Bologna, Italy.
6  * 
7  * HELM is free software; you can redistribute it and/or
8  * modify it under the terms of the GNU General Public License
9  * as published by the Free Software Foundation; either version 2
10  * of the License, or (at your option) any later version.
11  * 
12  * HELM is distributed in the hope that it will be useful,
13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
15  * GNU General Public License for more details.
16  *
17  * You should have received a copy of the GNU General Public License
18  * along with HELM; if not, write to the Free Software
19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://cs.unibo.it/helm/.
24  *)
25
26 (* let _profiler = <:profiler<_profiler>>;; *)
27
28 (* $Id$ *)
29
30 module Index = Equality_indexing.DT (* discrimination tree based indexing *)
31 (*
32 module Index = Equality_indexing.DT (* path tree based indexing *)
33 *)
34
35 let debug_print = Utils.debug_print;;
36
37 (* 
38 for debugging 
39 let check_equation env equation msg =
40   let w, proof, (eq_ty, left, right, order), metas, args = equation in
41   let metasenv, context, ugraph = env 
42   let metasenv' = metasenv @ metas in
43     try
44       CicTypeChecker.type_of_aux' metasenv' context left ugraph;
45       CicTypeChecker.type_of_aux' metasenv' context right ugraph;
46       ()
47     with 
48         CicUtil.Meta_not_found _ as exn ->
49           begin
50             prerr_endline msg; 
51             prerr_endline (CicPp.ppterm left);
52             prerr_endline (CicPp.ppterm right);
53             raise exn
54           end 
55 *)
56
57 type retrieval_mode = Matching | Unification;;
58
59 let string_of_res ?env =
60   function
61       None -> "None"
62     | Some (t, s, m, u, (p,e)) ->
63         Printf.sprintf "Some: (%s, %s, %s)" 
64           (Utils.string_of_pos p)
65           (Equality.string_of_equality ?env e)
66           (CicPp.ppterm t)
67 ;;
68
69 let print_res ?env res = 
70   prerr_endline 
71     (String.concat "\n"
72        (List.map (string_of_res ?env) res))
73 ;;
74
75 let print_candidates ?env mode term res =
76   let _ =
77     match mode with
78     | Matching ->
79         prerr_endline ("| candidates Matching " ^ (CicPp.ppterm term))
80     | Unification ->
81         prerr_endline ("| candidates Unification " ^ (CicPp.ppterm term))
82   in
83   prerr_endline 
84     (String.concat "\n"
85        (List.map
86           (fun (p, e) ->
87              Printf.sprintf "| (%s, %s)" (Utils.string_of_pos p)
88                (Equality.string_of_equality ?env e))
89           res));
90 ;;
91
92
93 let apply_subst = Subst.apply_subst
94
95 let index = Index.index
96 let remove_index = Index.remove_index
97 let in_index = Index.in_index
98 let empty = Index.empty 
99 let init_index = Index.init_index
100
101 let check_disjoint_invariant subst metasenv msg =
102   if (List.exists 
103         (fun (i,_,_) -> (Subst.is_in_subst i subst)) metasenv)
104   then 
105     begin 
106       prerr_endline ("not disjoint: " ^ msg);
107       assert false
108     end
109 ;;
110
111 let check_for_duplicates metas msg =
112   if List.length metas <> 
113   List.length (HExtlib.list_uniq (List.sort Pervasives.compare metas)) then
114     begin 
115       prerr_endline ("DUPLICATI " ^ msg);
116       prerr_endline (CicMetaSubst.ppmetasenv [] metas);
117       assert false
118     end
119 ;;
120
121 let check_res res msg =
122   match res with
123       Some (t, subst, menv, ug, eq_found) ->
124         let eqs = Equality.string_of_equality (snd eq_found) in
125         check_disjoint_invariant subst menv msg;
126         check_for_duplicates menv (msg ^ "\nchecking " ^ eqs);
127     | None -> ()
128 ;;
129
130 let check_target context target msg =
131   let w, proof, (eq_ty, left, right, order), metas,_ = 
132     Equality.open_equality target in
133   (* check that metas does not contains duplicates *)
134   let eqs = Equality.string_of_equality target in
135   let _ = check_for_duplicates metas (msg ^ "\nchecking " ^ eqs) in
136   let actual = (Utils.metas_of_term left)@(Utils.metas_of_term right)
137     @(Utils.metas_of_term eq_ty)@(Equality.metas_of_proof proof)  in
138   let menv = List.filter (fun (i, _, _) -> List.mem i actual) metas in
139   let _ = if menv <> metas then 
140     begin 
141       prerr_endline ("extra metas " ^ msg);
142       prerr_endline (CicMetaSubst.ppmetasenv [] metas);
143       prerr_endline "**********************";
144       prerr_endline (CicMetaSubst.ppmetasenv [] menv);
145       prerr_endline ("left: " ^ (CicPp.ppterm left));
146       prerr_endline ("right: " ^ (CicPp.ppterm right)); 
147       prerr_endline ("ty: " ^ (CicPp.ppterm eq_ty));
148       assert false
149     end
150   else () in ()
151 (*
152   try 
153       ignore(CicTypeChecker.type_of_aux'
154         metas context (Inference.build_proof_term proof) CicUniv.empty_ugraph)
155   with e ->  
156       prerr_endline msg;
157       prerr_endline (Inference.string_of_proof proof);
158       prerr_endline (CicPp.ppterm (Inference.build_proof_term proof));
159       prerr_endline ("+++++++++++++left: " ^ (CicPp.ppterm left));
160       prerr_endline ("+++++++++++++right: " ^ (CicPp.ppterm right)); 
161       raise e 
162 *)
163
164
165 (* returns a list of all the equalities in the tree that are in relation
166    "mode" with the given term, where mode can be either Matching or
167    Unification.
168
169    Format of the return value: list of tuples in the form:
170    (position - Left or Right - of the term that matched the given one in this
171      equality,
172     equality found)
173    
174    Note that if equality is "left = right", if the ordering is left > right,
175    the position will always be Left, and if the ordering is left < right,
176    position will be Right.
177 *)
178
179 let get_candidates ?env mode tree term =
180   let s = 
181     match mode with
182     | Matching -> 
183         Index.retrieve_generalizations tree term
184     | Unification -> 
185         Index.retrieve_unifiables tree term
186         
187   in
188   Index.PosEqSet.elements s
189 ;;
190
191 (*
192   finds the first equality in the index that matches "term", of type "termty"
193   termty can be Implicit if it is not needed. The result (one of the sides of
194   the equality, actually) should be not greater (wrt the term ordering) than
195   term
196
197   Format of the return value:
198
199   (term to substitute, [Cic.Rel 1 properly lifted - see the various
200                         build_newtarget functions inside the various
201                         demodulation_* functions]
202    substitution used for the matching,
203    metasenv,
204    ugraph, [substitution, metasenv and ugraph have the same meaning as those
205    returned by CicUnification.fo_unif]
206    (equality where the matching term was found, [i.e. the equality to use as
207                                                 rewrite rule]
208     uri [either eq_ind_URI or eq_ind_r_URI, depending on the direction of
209          the equality: this is used to build the proof term, again see one of
210          the build_newtarget functions]
211    ))
212 *)
213 let rec find_matches metasenv context ugraph lift_amount term termty =
214   let module C = Cic in
215   let module U = Utils in
216   let module S = CicSubstitution in
217   let module M = CicMetaSubst in
218   let module HL = HelmLibraryObjects in
219   let cmp = !Utils.compare_terms in
220   let check = match termty with C.Implicit None -> false | _ -> true in
221   function
222     | [] -> None
223     | candidate::tl ->
224         let pos, equality = candidate in
225         let (_, proof, (ty, left, right, o), metas,_) = 
226           Equality.open_equality equality 
227         in
228         if Utils.debug_metas then 
229           ignore(check_target context (snd candidate) "find_matches");
230         if Utils.debug_res then 
231           begin
232             let c="eq = "^(Equality.string_of_equality (snd candidate)) ^ "\n"in
233             let t="t = " ^ (CicPp.ppterm term) ^ "\n" in
234             let m="metas = " ^ (CicMetaSubst.ppmetasenv [] metas) ^ "\n" in
235 (*
236             let p="proof = "^
237               (CicPp.ppterm(Equality.build_proof_term proof))^"\n" 
238             in
239 *)
240               check_for_duplicates metas "gia nella metas";
241               check_for_duplicates (metasenv@metas) ("not disjoint"^c^t^m(*^p*))
242           end;
243         if check && not (fst (CicReduction.are_convertible
244                                 ~metasenv context termty ty ugraph)) then (
245           find_matches metasenv context ugraph lift_amount term termty tl
246         ) else
247           let do_match c =
248             let subst', metasenv', ugraph' =
249               Inference.matching 
250                 metasenv metas context term (S.lift lift_amount c) ugraph
251             in
252             Some (Cic.Rel(1+lift_amount),subst',metasenv',ugraph',candidate)
253           in
254           let c, other =
255             if pos = Utils.Left then left, right
256             else right, left
257           in
258           if o <> U.Incomparable then
259             let res =
260               try
261                 do_match c 
262               with Inference.MatchingFailure ->
263                 find_matches metasenv context ugraph lift_amount term termty tl
264             in
265               if Utils.debug_res then ignore (check_res res "find1");
266               res
267           else
268             let res =
269               try do_match c 
270               with Inference.MatchingFailure -> None
271             in
272             if Utils.debug_res then ignore (check_res res "find2");
273             match res with
274             | Some (_, s, _, _, _) ->
275                 let c' = apply_subst s c in
276                 (* 
277              let other' = U.guarded_simpl context (apply_subst s other) in *)
278                 let other' = apply_subst s other in
279                 let order = cmp c' other' in
280                 if order = U.Gt then
281                   res
282                 else
283                   find_matches
284                     metasenv context ugraph lift_amount term termty tl
285             | None ->
286                 find_matches metasenv context ugraph lift_amount term termty tl
287 ;;
288
289 let find_matches metasenv context ugraph lift_amount term termty =
290   find_matches metasenv context ugraph lift_amount term termty
291 ;;
292
293 (*
294   as above, but finds all the matching equalities, and the matching condition
295   can be either Inference.matching or Inference.unification
296 *)
297 let rec find_all_matches ?(unif_fun=Inference.unification)
298     metasenv context ugraph lift_amount term termty =
299   let module C = Cic in
300   let module U = Utils in
301   let module S = CicSubstitution in
302   let module M = CicMetaSubst in
303   let module HL = HelmLibraryObjects in
304   let cmp = !Utils.compare_terms in
305   function
306     | [] -> []
307     | candidate::tl ->
308         let pos, equality = candidate in 
309         let (_,_,(ty,left,right,o),metas,_)=Equality.open_equality equality in
310         let do_match c =
311           let subst', metasenv', ugraph' =
312             unif_fun metasenv metas context term (S.lift lift_amount c) ugraph
313           in
314           (C.Rel (1+lift_amount),subst',metasenv',ugraph',candidate)
315         in
316         let c, other =
317           if pos = Utils.Left then left, right
318           else right, left
319         in
320         if o <> U.Incomparable then
321           try
322             let res = do_match c in
323             res::(find_all_matches ~unif_fun metasenv context ugraph
324                     lift_amount term termty tl)
325           with
326           | Inference.MatchingFailure
327           | CicUnification.UnificationFailure _
328           | CicUnification.Uncertain _ ->
329               find_all_matches ~unif_fun metasenv context ugraph
330                 lift_amount term termty tl
331         else
332           try
333             let res = do_match c in
334             match res with
335             | _, s, _, _, _ ->
336                 let c' = apply_subst s c
337                 and other' = apply_subst s other in
338                 let order = cmp c' other' in
339                 if order <> U.Lt && order <> U.Le then
340                   res::(find_all_matches ~unif_fun metasenv context ugraph
341                           lift_amount term termty tl)
342                 else
343                   find_all_matches ~unif_fun metasenv context ugraph
344                     lift_amount term termty tl
345           with
346           | Inference.MatchingFailure
347           | CicUnification.UnificationFailure _
348           | CicUnification.Uncertain _ ->
349               find_all_matches ~unif_fun metasenv context ugraph
350                 lift_amount term termty tl
351 ;;
352
353 let find_all_matches 
354   ?unif_fun metasenv context ugraph lift_amount term termty l 
355 =
356     find_all_matches 
357       ?unif_fun metasenv context ugraph lift_amount term termty l 
358   (*prerr_endline "CANDIDATES:";
359   List.iter (fun (_,x)->prerr_endline (Inference.string_of_equality x)) l;
360   prerr_endline ("MATCHING:" ^ CicPp.ppterm term ^ " are " ^ string_of_int
361   (List.length rc));*)
362 ;;
363 (*
364   returns true if target is subsumed by some equality in table
365 *)
366 let print_res l =
367   prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug,
368     ((pos,equation),_)) -> Equality.string_of_equality equation)l))
369 ;;
370
371 let subsumption_aux use_unification env table target = 
372   let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
373   let metasenv, context, ugraph = env in
374   let metasenv = tmetas in
375   let predicate, unif_fun = 
376     if use_unification then
377       Unification, Inference.unification
378     else
379       Matching, Inference.matching
380   in
381   let leftr =
382     match left with
383     | Cic.Meta _ when not use_unification -> []   
384     | _ ->
385         let leftc = get_candidates predicate table left in
386         find_all_matches ~unif_fun
387           metasenv context ugraph 0 left ty leftc
388   in
389   let rec ok what leftorright = function
390     | [] -> None
391     | (_, subst, menv, ug, (pos,equation))::tl ->
392         let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
393         try
394           let other = if pos = Utils.Left then r else l in
395           let what' = Subst.apply_subst subst what in
396           let other' = Subst.apply_subst subst other in
397           let subst', menv', ug' =
398             unif_fun metasenv m context what' other' ugraph
399           in
400           (match Subst.merge_subst_if_possible subst subst' with
401           | None -> ok what leftorright tl
402           | Some s -> Some (s, equation, leftorright <> pos ))
403         with 
404         | Inference.MatchingFailure 
405         | CicUnification.UnificationFailure _ -> ok what leftorright tl
406   in
407   match ok right Utils.Left  leftr with
408   | Some _ as res -> res
409   | None -> 
410       let rightr =
411         match right with
412           | Cic.Meta _ when not use_unification -> [] 
413           | _ ->
414               let rightc = get_candidates predicate table right in
415                 find_all_matches ~unif_fun
416                   metasenv context ugraph 0 right ty rightc
417       in
418         ok left Utils.Right rightr 
419 ;;
420
421 let subsumption x y z =
422   subsumption_aux false x y z
423 ;;
424
425 let unification x y z = 
426   subsumption_aux true x y z
427 ;;
428
429 let rec demodulation_aux ?from ?(typecheck=false) 
430   metasenv context ugraph table lift_amount term =
431 (*  Printf.eprintf "term = %s\n" (CicPp.ppterm term);*)
432   let module C = Cic in
433   let module S = CicSubstitution in
434   let module M = CicMetaSubst in
435   let module HL = HelmLibraryObjects in
436   let candidates = 
437     get_candidates 
438       ~env:(metasenv,context,ugraph) (* Unification *) Matching table term 
439   in
440   let res =
441     match term with
442       | C.Meta _ -> None
443       | term ->
444           let termty, ugraph =
445             if typecheck then
446               CicTypeChecker.type_of_aux' metasenv context term ugraph
447             else
448               C.Implicit None, ugraph
449           in
450           let res =
451             find_matches metasenv context ugraph lift_amount term termty candidates
452           in
453           if Utils.debug_res then ignore(check_res res "demod1"); 
454             if res <> None then
455               res
456             else
457               match term with
458                 | C.Appl l ->
459                     let res, ll = 
460                       List.fold_left
461                         (fun (res, tl) t ->
462                            if res <> None then
463                              (res, tl @ [S.lift 1 t])
464                            else 
465                              let r =
466                                demodulation_aux ~from:"1" metasenv context ugraph table
467                                  lift_amount t
468                              in
469                                match r with
470                                  | None -> (None, tl @ [S.lift 1 t])
471                                  | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
472                         (None, []) l
473                     in (
474                         match res with
475                           | None -> None
476                           | Some (_, subst, menv, ug, eq_found) ->
477                               Some (C.Appl ll, subst, menv, ug, eq_found)
478                       )
479                 | C.Prod (nn, s, t) ->
480                     let r1 =
481                       demodulation_aux ~from:"2"
482                         metasenv context ugraph table lift_amount s in (
483                         match r1 with
484                           | None ->
485                               let r2 =
486                                 demodulation_aux metasenv
487                                   ((Some (nn, C.Decl s))::context) ugraph
488                                   table (lift_amount+1) t
489                               in (
490                                   match r2 with
491                                     | None -> None
492                                     | Some (t', subst, menv, ug, eq_found) ->
493                                         Some (C.Prod (nn, (S.lift 1 s), t'),
494                                               subst, menv, ug, eq_found)
495                                 )
496                           | Some (s', subst, menv, ug, eq_found) ->
497                               Some (C.Prod (nn, s', (S.lift 1 t)),
498                                     subst, menv, ug, eq_found)
499                       )
500                 | C.Lambda (nn, s, t) ->
501                     let r1 =
502                       demodulation_aux 
503                         metasenv context ugraph table lift_amount s in (
504                         match r1 with
505                           | None ->
506                               let r2 =
507                                 demodulation_aux metasenv
508                                   ((Some (nn, C.Decl s))::context) ugraph
509                                   table (lift_amount+1) t
510                               in (
511                                   match r2 with
512                                     | None -> None
513                                     | Some (t', subst, menv, ug, eq_found) ->
514                                         Some (C.Lambda (nn, (S.lift 1 s), t'),
515                                               subst, menv, ug, eq_found)
516                                 )
517                           | Some (s', subst, menv, ug, eq_found) ->
518                               Some (C.Lambda (nn, s', (S.lift 1 t)),
519                                     subst, menv, ug, eq_found)
520                       )
521                 | t ->
522                     None
523   in
524   if Utils.debug_res then ignore(check_res res "demod_aux output"); 
525   res
526 ;;
527
528 exception Foo
529
530 (** demodulation, when target is an equality *)
531 let rec demodulation_equality ?from eq_uri newmeta env table target =
532   let module C = Cic in
533   let module S = CicSubstitution in
534   let module M = CicMetaSubst in
535   let module HL = HelmLibraryObjects in
536   let module U = Utils in
537   let metasenv, context, ugraph = env in
538   let w, proof, (eq_ty, left, right, order), metas, id = 
539     Equality.open_equality target 
540   in
541   (* first, we simplify *)
542 (*   let right = U.guarded_simpl context right in *)
543 (*   let left = U.guarded_simpl context left in *)
544 (*   let order = !Utils.compare_terms left right in *)
545 (*   let stat = (eq_ty, left, right, order) in  *)
546 (*  let w = Utils.compute_equality_weight stat in*)
547   (* let target = Equality.mk_equality (w, proof, stat, metas) in *)
548   if Utils.debug_metas then 
549     ignore(check_target context target "demod equalities input");
550   let metasenv' = (* metasenv @ *) metas in
551   let maxmeta = ref newmeta in
552   
553   let build_newtarget is_left (t, subst, menv, ug, eq_found) =
554     
555     if Utils.debug_metas then
556       begin
557         ignore(check_for_duplicates menv "input1");
558         ignore(check_disjoint_invariant subst menv "input2");
559         let substs = Subst.ppsubst subst in 
560         ignore(check_target context (snd eq_found) ("input3" ^ substs))
561       end;
562     let pos, equality = eq_found in
563     let (_, proof', 
564         (ty, what, other, _), menv',id') = Equality.open_equality equality in
565     let ty =
566       try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
567       with CicUtil.Meta_not_found _ -> ty
568     in
569     let what, other = if pos = Utils.Left then what, other else other, what in
570     let newterm, newproof =
571       let bo = 
572         Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
573 (*      let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in*)
574       let name = C.Name "x" in
575       let bo' =
576         let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
577           C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
578       in
579           (bo, (Equality.Step (subst,(Equality.Demodulation, id,(pos,id'),
580           (Cic.Lambda (name, ty, bo'))))))
581     in
582     let newmenv = menv in
583     let left, right = if is_left then newterm, right else left, newterm in
584     let ordering = !Utils.compare_terms left right in
585     let stat = (eq_ty, left, right, ordering) in
586     let res =
587       let w = Utils.compute_equality_weight stat in
588           (Equality.mk_equality (w, newproof, stat,newmenv))
589     in
590     if Utils.debug_metas then 
591       ignore(check_target context res "buildnew_target output");
592     !maxmeta, res 
593   in
594
595   let res = demodulation_aux ~from:"3" metasenv' context ugraph table 0 left in
596   if Utils.debug_res then check_res res "demod result";
597   let newmeta, newtarget = 
598     match res with
599     | Some t ->
600         let newmeta, newtarget = build_newtarget true t in
601           assert (not (Equality.meta_convertibility_eq target newtarget));
602           if (Equality.is_weak_identity newtarget) ||
603             (Equality.meta_convertibility_eq target newtarget) then
604               newmeta, newtarget
605           else 
606             demodulation_equality ?from eq_uri newmeta env table newtarget
607     | None ->
608         let res = demodulation_aux metasenv' context ugraph table 0 right in
609         if Utils.debug_res then check_res res "demod result 1"; 
610           match res with
611           | Some t ->
612               let newmeta, newtarget = build_newtarget false t in
613                 if (Equality.is_weak_identity newtarget) ||
614                   (Equality.meta_convertibility_eq target newtarget) then
615                     newmeta, newtarget
616                 else
617                    demodulation_equality ?from eq_uri newmeta env table newtarget
618           | None ->
619               newmeta, target
620   in
621   (* newmeta, newtarget *)
622   newmeta,newtarget 
623 ;;
624
625 (**
626    Performs the beta expansion of the term "term" w.r.t. "table",
627    i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
628    in table.
629 *)
630 let rec betaexpand_term 
631   ?(subterms_only=false) metasenv context ugraph table lift_amount term 
632 =
633   let module C = Cic in
634   let module S = CicSubstitution in
635   let module M = CicMetaSubst in
636   let module HL = HelmLibraryObjects in
637   
638   let res, lifted_term = 
639     match term with
640     | C.Meta (i, l) ->
641         let l = [] in
642         let l', lifted_l =
643           List.fold_right
644             (fun arg (res, lifted_tl) ->
645                match arg with
646                | Some arg ->
647                    let arg_res, lifted_arg =
648                      betaexpand_term metasenv context ugraph table
649                        lift_amount arg in
650                    let l1 =
651                      List.map
652                        (fun (t, s, m, ug, eq_found) ->
653                           (Some t)::lifted_tl, s, m, ug, eq_found)
654                        arg_res
655                    in
656                    (l1 @
657                       (List.map
658                          (fun (l, s, m, ug, eq_found) ->
659                             (Some lifted_arg)::l, s, m, ug, eq_found)
660                          res),
661                     (Some lifted_arg)::lifted_tl)
662                | None ->
663                    (List.map
664                       (fun (r, s, m, ug, eq_found) ->
665                          None::r, s, m, ug, eq_found) res,
666                     None::lifted_tl)
667             ) l ([], [])
668         in
669         let e =
670           List.map
671             (fun (l, s, m, ug, eq_found) ->
672                (C.Meta (i, l), s, m, ug, eq_found)) l'
673         in
674         e, C.Meta (i, lifted_l)
675           
676     | C.Rel m ->
677         [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
678           
679     | C.Prod (nn, s, t) ->
680         let l1, lifted_s =
681           betaexpand_term metasenv context ugraph table lift_amount s in
682         let l2, lifted_t =
683           betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
684             table (lift_amount+1) t in
685         let l1' =
686           List.map
687             (fun (t, s, m, ug, eq_found) ->
688                C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
689         and l2' =
690           List.map
691             (fun (t, s, m, ug, eq_found) ->
692                C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
693         l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
694           
695     | C.Lambda (nn, s, t) ->
696         let l1, lifted_s =
697           betaexpand_term metasenv context ugraph table lift_amount s in
698         let l2, lifted_t =
699           betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
700             table (lift_amount+1) t in
701         let l1' =
702           List.map
703             (fun (t, s, m, ug, eq_found) ->
704                C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
705         and l2' =
706           List.map
707             (fun (t, s, m, ug, eq_found) ->
708                C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
709         l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
710
711     | C.Appl l ->
712         let l', lifted_l =
713           List.fold_left
714             (fun (res, lifted_tl) arg ->
715                let arg_res, lifted_arg =
716                  betaexpand_term metasenv context ugraph table lift_amount arg
717                in
718                let l1 =
719                  List.map
720                    (fun (a, s, m, ug, eq_found) ->
721                       a::lifted_tl, s, m, ug, eq_found)
722                    arg_res
723                in
724                (l1 @
725                   (List.map
726                      (fun (r, s, m, ug, eq_found) ->
727                         lifted_arg::r, s, m, ug, eq_found)
728                      res),
729                 lifted_arg::lifted_tl)
730             ) ([], []) (List.rev l)
731         in
732         (List.map
733            (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
734          C.Appl lifted_l)
735
736     | t -> [], (S.lift lift_amount t)
737   in
738   match term with
739   | C.Meta (i, l) -> res, lifted_term
740   | term ->
741       let termty, ugraph =
742         C.Implicit None, ugraph
743 (*         CicTypeChecker.type_of_aux' metasenv context term ugraph *)
744       in
745       let candidates = get_candidates Unification table term in
746       let r = 
747         if subterms_only then 
748           [] 
749         else 
750           find_all_matches
751             metasenv context ugraph lift_amount term termty candidates
752       in
753       r @ res, lifted_term
754 ;;
755
756 (**
757    superposition_right
758    returns a list of new clauses inferred with a right superposition step
759    between the positive equation "target" and one in the "table" "newmeta" is
760    the first free meta index, i.e. the first number above the highest meta
761    index: its updated value is also returned
762 *)
763 let superposition_right 
764   ?(subterms_only=false) eq_uri newmeta (metasenv, context, ugraph) table target=
765   let module C = Cic in
766   let module S = CicSubstitution in
767   let module M = CicMetaSubst in
768   let module HL = HelmLibraryObjects in
769   let module CR = CicReduction in
770   let module U = Utils in 
771   let w, eqproof, (eq_ty, left, right, ordering), newmetas,id = 
772     Equality.open_equality target 
773   in 
774   if Utils.debug_metas then 
775     ignore (check_target context target "superpositionright");
776   let metasenv' = newmetas in
777   let maxmeta = ref newmeta in
778   let res1, res2 =
779     match ordering with
780     | U.Gt -> 
781         fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 left), []
782     | U.Lt -> 
783         [], fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 right)
784     | _ ->
785         let res l r =
786           List.filter
787             (fun (_, subst, _, _, _) ->
788                let subst = apply_subst subst in
789                let o = !Utils.compare_terms (subst l) (subst r) in
790                o <> U.Lt && o <> U.Le)
791             (fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 l))
792         in
793         (res left right), (res right left)
794   in
795   let build_new ordering (bo, s, m, ug, eq_found) =
796     if Utils.debug_metas then 
797       ignore (check_target context (snd eq_found) "buildnew1" );
798     
799     let pos, equality =  eq_found in
800     let (_, proof', (ty, what, other, _), menv',id') = 
801       Equality.open_equality  equality in
802     let what, other = if pos = Utils.Left then what, other else other, what in
803
804     let newgoal, newproof =
805       (* qua *)
806       let bo' =
807         Utils.guarded_simpl context (apply_subst s (S.subst other bo)) 
808       in
809       let name = C.Name "x" in
810       let bo'' =
811         let l, r =
812           if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
813         C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
814       in
815       bo',
816         Equality.Step 
817           (s,(Equality.SuperpositionRight,
818                id,(pos,id'),(Cic.Lambda(name,ty,bo''))))
819     in
820     let newmeta, newequality = 
821       let left, right =
822         if ordering = U.Gt then newgoal, apply_subst s right
823         else apply_subst s left, newgoal in
824       let neworder = !Utils.compare_terms left right in
825       let newmenv = (* Inference.filter s *) m in
826       let stat = (eq_ty, left, right, neworder) in
827       let eq' =
828         let w = Utils.compute_equality_weight stat in
829         Equality.mk_equality (w, newproof, stat, newmenv) in
830       if Utils.debug_metas then 
831         ignore (check_target context eq' "buildnew3");
832       let newm, eq' = Equality.fix_metas !maxmeta eq' in
833       if Utils.debug_metas then 
834         ignore (check_target context eq' "buildnew4");
835       newm, eq'
836     in
837     maxmeta := newmeta;
838     if Utils.debug_metas then 
839       ignore(check_target context newequality "buildnew2"); 
840     newequality
841   in
842   let new1 = List.map (build_new U.Gt) res1
843   and new2 = List.map (build_new U.Lt) res2 in
844   let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
845   (!maxmeta,
846    (List.filter ok (new1 @ new2)))
847 ;;
848
849 (** demodulation, when the target is a theorem *)
850 let rec demodulation_theorem newmeta env table theorem =
851   let module C = Cic in
852   let module S = CicSubstitution in
853   let module M = CicMetaSubst in
854   let module HL = HelmLibraryObjects in
855   let metasenv, context, ugraph = env in
856   let maxmeta = ref newmeta in
857   let term, termty, metas = theorem in
858   let metasenv' = metas in
859   
860   let build_newtheorem (t, subst, menv, ug, eq_found) =
861     let pos, equality = eq_found in
862     let (_, proof', (ty, what, other, _), menv',id) = 
863       Equality.open_equality equality in
864     let what, other = if pos = Utils.Left then what, other else other, what in
865     let newterm, newty =
866       let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
867 (*      let bo' = apply_subst subst t in *)
868 (*      let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in*)
869 (*
870       let newproofold =
871         Equality.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
872                               Equality.BasicProof (Equality.empty_subst,term))
873       in
874       (Equality.build_proof_term_old newproofold, bo)
875 *)
876       (* TODO, not ported to the new proofs *) 
877       if true then assert false; term, bo
878     in    
879     !maxmeta, (newterm, newty, menv)
880   in  
881   let res =
882     demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 termty
883   in
884   match res with
885   | Some t ->
886       let newmeta, newthm = build_newtheorem t in
887       let newt, newty, _ = newthm in
888       if Equality.meta_convertibility termty newty then
889         newmeta, newthm
890       else
891         demodulation_theorem newmeta env table newthm
892   | None ->
893       newmeta, theorem
894 ;;
895
896 (*****************************************************************************)
897 (**                         OPERATIONS ON GOALS                             **)
898 (**                                                                         **)
899 (**                DEMODULATION_GOAL & SUPERPOSITION_LEFT                   **)
900 (*****************************************************************************)
901
902 let open_goal g =
903   match g with
904   | (proof,menv,Cic.Appl[(Cic.MutInd(uri,0,_)) as eq;ty;l;r]) -> 
905       assert (LibraryObjects.is_eq_URI uri);
906       proof,menv,eq,ty,l,r
907   | _ -> assert false
908 ;;
909
910 let ty_of_goal (_,_,ty) = ty ;;
911
912 (* checks if two goals are metaconvertible *)
913 let goal_metaconvertibility_eq g1 g2 = 
914   Equality.meta_convertibility (ty_of_goal g1) (ty_of_goal g2)
915 ;;
916
917 (* when the betaexpand_term function is called on the left/right side of the
918  * goal, the predicate has to be fixed
919  * C[x] ---> (eq ty unchanged C[x])
920  * [posu] is the side of the [unchanged] term in the original goal
921  *)
922 let fix_expansion goal posu (t, subst, menv, ug, eq_f) = 
923   let _,_,eq,ty,l,r = open_goal goal in
924   let unchanged = if posu = Utils.Left then l else r in
925   let unchanged = CicSubstitution.lift 1 unchanged in
926   let ty = CicSubstitution.lift 1 ty in
927   let pred = 
928     match posu with
929     | Utils.Left -> Cic.Appl [eq;ty;unchanged;t]
930     | Utils.Right -> Cic.Appl [eq;ty;t;unchanged]
931   in
932   (pred, subst, menv, ug, eq_f)
933 ;;
934
935 (* ginve the old [goal], the side that has not changed [posu] and the 
936  * expansion builds a new goal *)
937 let build_newgoal context goal posu rule expansion =
938   let goalproof,_,_,_,_,_ = open_goal goal in
939   let (t,subst,menv,ug,eq_found) = fix_expansion goal posu expansion in
940   let pos, equality = eq_found in
941   let (_, proof', (ty, what, other, _), menv',id) = 
942     Equality.open_equality equality in
943   let what, other = if pos = Utils.Left then what, other else other, what in
944   let newterm, newgoalproof =
945     let bo = 
946       Utils.guarded_simpl context 
947         (apply_subst subst (CicSubstitution.subst other t)) 
948     in
949     let bo' = (*apply_subst subst*) t in 
950     let name = Cic.Name "x" in
951     let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in
952     bo, (newgoalproofstep::goalproof)
953   in
954   let newmetasenv = (* Inference.filter subst *) menv in
955   (newgoalproof, newmetasenv, newterm)
956 ;;
957
958 (**
959    superposition_left 
960    returns a list of new clauses inferred with a left superposition step
961    the negative equation "target" and one of the positive equations in "table"
962 *)
963 let superposition_left (metasenv, context, ugraph) table goal maxmeta = 
964   let names = Utils.names_of_context context in
965   let proof,menv,eq,ty,l,r = open_goal goal in
966   let c = !Utils.compare_terms l r in
967   let newgoals = 
968     if c = Utils.Incomparable then
969       begin
970       let expansionsl, _ = betaexpand_term menv context ugraph table 0 l in
971       let expansionsr, _ = betaexpand_term menv context ugraph table 0 r in
972       (* prerr_endline "incomparable"; 
973       prerr_endline (string_of_int (List.length expansionsl));
974       prerr_endline (string_of_int (List.length expansionsr));
975       *)
976       List.map (build_newgoal context goal Utils.Right Equality.SuperpositionLeft) expansionsl
977       @
978       List.map (build_newgoal context goal Utils.Left Equality.SuperpositionLeft) expansionsr
979       end
980     else
981         match c with 
982         | Utils.Gt -> (* prerr_endline "GT"; *) 
983             let big,small,possmall = l,r,Utils.Right in
984             let expansions, _ = betaexpand_term menv context ugraph table 0 big in
985             List.map 
986               (build_newgoal context goal possmall Equality.SuperpositionLeft) 
987               expansions
988         | Utils.Lt -> (* prerr_endline "LT"; *) 
989             let big,small,possmall = r,l,Utils.Left in
990             let expansions, _ = betaexpand_term menv context ugraph table 0 big in
991             List.map 
992               (build_newgoal context goal possmall Equality.SuperpositionLeft) 
993               expansions
994         | Utils.Eq -> []
995         | _ ->
996             prerr_endline 
997               ("NOT GT, LT NOR EQ : "^CicPp.pp l names^" - "^CicPp.pp r names);
998             assert false
999   in
1000   (* rinfresco le meta *)
1001   List.fold_right
1002     (fun g (max,acc) -> 
1003        let max,g = Equality.fix_metas_goal max g in max,g::acc) 
1004     newgoals (maxmeta,[])
1005 ;;
1006
1007 (** demodulation, when the target is a goal *)
1008 let rec demodulation_goal env table goal =
1009   let goalproof,menv,_,_,left,right = open_goal goal in
1010   let _, context, ugraph = env in
1011 (*  let term = Utils.guarded_simpl (~debug:true) context term in*)
1012   let do_right () = 
1013       let resright = demodulation_aux menv context ugraph table 0 right in
1014       match resright with
1015       | Some t ->
1016           let newg = 
1017             build_newgoal context goal Utils.Left Equality.Demodulation t 
1018           in
1019           if goal_metaconvertibility_eq goal newg then
1020             false, goal
1021           else
1022             true, snd (demodulation_goal env table newg)
1023       | None -> false, goal
1024   in
1025   let resleft = demodulation_aux menv context ugraph table 0 left in
1026   match resleft with
1027   | Some t ->
1028       let newg = build_newgoal context goal Utils.Right Equality.Demodulation t in
1029       if goal_metaconvertibility_eq goal newg then
1030         do_right ()
1031       else
1032         true, snd (demodulation_goal env table newg)
1033   | None -> do_right ()
1034 ;;
1035
1036 let get_stats () = "" ;;