]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/tactics/paramodulation/indexing.ml
Unable to parse my own output. Fixed.
[helm.git] / helm / software / 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 (* $Id$ *)
27
28 module Index = Equality_indexing.DT (* discrimination tree based indexing *)
29 (*
30 module Index = Equality_indexing.DT (* path tree based indexing *)
31 *)
32
33 let beta_expand_time = ref 0.;;
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), eq_URI)) ->
63         Printf.sprintf "Some: (%s, %s, %s)" 
64           (Utils.string_of_pos p)
65           (Inference.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                (Inference.string_of_equality ?env e))
89           res));
90 ;;
91
92
93 let indexing_retrieval_time = ref 0.;;
94
95
96 let apply_subst = CicMetaSubst.apply_subst
97
98 let index = Index.index
99 let remove_index = Index.remove_index
100 let in_index = Index.in_index
101 let empty = Index.empty 
102 let init_index = Index.init_index
103
104 let check_disjoint_invariant subst metasenv msg =
105   if (List.exists 
106         (fun (i,_,_) -> (List.exists (fun (j,_) -> i=j) subst)) metasenv)
107   then 
108     begin 
109       prerr_endline ("not disjoint: " ^ msg);
110       assert false
111     end
112 ;;
113
114 let check_for_duplicates metas msg =
115 let _ = 
116     try
117       ignore(CicUtil.lookup_meta 190 metas);
118       prerr_endline ("eccoci in " ^ msg);
119     with
120         CicUtil.Meta_not_found _ -> () in
121 if List.length metas <> 
122   List.length (HExtlib.list_uniq (List.sort Pervasives.compare metas)) then
123     begin 
124       prerr_endline ("DUPLICATI " ^ msg);
125       prerr_endline (CicMetaSubst.ppmetasenv [] metas);
126       assert false
127     end
128 ;;
129
130 let check_res res msg =
131   match res with
132       Some (t, subst, menv, ug, (eq_found, eq_URI)) ->
133         let eqs = Inference.string_of_equality (snd eq_found) in
134         check_disjoint_invariant subst menv msg;
135         check_for_duplicates menv (msg ^ "\nchecking " ^ eqs);
136     | None -> ()
137 ;;
138
139 let check_target context target msg =
140   let w, proof, (eq_ty, left, right, order), metas, args = target in
141   (* check that metas does not contains duplicates *)
142   let eqs = Inference.string_of_equality target in
143   let _ = check_for_duplicates metas (msg ^ "\nchecking " ^ eqs) in
144   let actual = (Inference.metas_of_term left)@(Inference.metas_of_term right)
145     @(Inference.metas_of_term eq_ty)@(Inference.metas_of_proof proof) in
146   let menv = List.filter (fun (i, _, _) -> List.mem i actual) metas in
147   let _ = if menv <> metas then 
148     begin 
149       prerr_endline ("extra metas " ^ msg);
150       prerr_endline (CicMetaSubst.ppmetasenv [] metas);
151       prerr_endline "**********************";
152       prerr_endline (CicMetaSubst.ppmetasenv [] menv);
153       prerr_endline ("left: " ^ (CicPp.ppterm left));
154       prerr_endline ("right: " ^ (CicPp.ppterm right)); 
155       prerr_endline ("ty: " ^ (CicPp.ppterm eq_ty));
156       assert false
157     end 
158   else () in
159   try 
160       CicTypeChecker.type_of_aux'
161         metas context (Inference.build_proof_term proof) CicUniv.empty_ugraph
162   with e ->  
163       prerr_endline msg;
164       prerr_endline (Inference.string_of_proof proof);
165       prerr_endline (CicPp.ppterm (Inference.build_proof_term proof));
166       prerr_endline ("+++++++++++++left: " ^ (CicPp.ppterm left));
167       prerr_endline ("+++++++++++++right: " ^ (CicPp.ppterm right)); 
168       raise e
169 ;;
170
171
172 (* returns a list of all the equalities in the tree that are in relation
173    "mode" with the given term, where mode can be either Matching or
174    Unification.
175
176    Format of the return value: list of tuples in the form:
177    (position - Left or Right - of the term that matched the given one in this
178      equality,
179     equality found)
180    
181    Note that if equality is "left = right", if the ordering is left > right,
182    the position will always be Left, and if the ordering is left < right,
183    position will be Right.
184 *)
185 let local_max = ref 100;;
186
187 let make_variant (p,eq) =
188   let maxmeta, eq = Inference.fix_metas !local_max eq in
189   local_max := maxmeta;
190   p, eq
191 ;;
192
193 let get_candidates ?env mode tree term =
194   let t1 = Unix.gettimeofday () in
195   let res =
196     let s = 
197       match mode with
198       | Matching -> Index.retrieve_generalizations tree term
199       | Unification -> Index.retrieve_unifiables tree term
200     in
201     Index.PosEqSet.elements s
202   in
203 (*   print_endline (Discrimination_tree.string_of_discrimination_tree tree); *)
204 (*   print_newline (); *)
205   let t2 = Unix.gettimeofday () in
206   indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1); 
207  (* make fresh instances *)
208   res 
209 ;;
210
211
212 let match_unif_time_ok = ref 0.;;
213 let match_unif_time_no = ref 0.;;
214
215
216 (*
217   finds the first equality in the index that matches "term", of type "termty"
218   termty can be Implicit if it is not needed. The result (one of the sides of
219   the equality, actually) should be not greater (wrt the term ordering) than
220   term
221
222   Format of the return value:
223
224   (term to substitute, [Cic.Rel 1 properly lifted - see the various
225                         build_newtarget functions inside the various
226                         demodulation_* functions]
227    substitution used for the matching,
228    metasenv,
229    ugraph, [substitution, metasenv and ugraph have the same meaning as those
230    returned by CicUnification.fo_unif]
231    (equality where the matching term was found, [i.e. the equality to use as
232                                                 rewrite rule]
233     uri [either eq_ind_URI or eq_ind_r_URI, depending on the direction of
234          the equality: this is used to build the proof term, again see one of
235          the build_newtarget functions]
236    ))
237 *)
238 let rec find_matches metasenv context ugraph lift_amount term termty =
239   let module C = Cic in
240   let module U = Utils in
241   let module S = CicSubstitution in
242   let module M = CicMetaSubst in
243   let module HL = HelmLibraryObjects in
244   let cmp = !Utils.compare_terms in
245   let check = match termty with C.Implicit None -> false | _ -> true in
246   function
247     | [] -> None
248     | candidate::tl ->
249         let pos, (_, proof, (ty, left, right, o), metas, args) = candidate in
250         if Utils.debug_metas then 
251           ignore(check_target context (snd candidate) "find_matches");
252         if Utils.debug_res then 
253           begin
254             let c = "eq = " ^ (Inference.string_of_equality (snd candidate)) ^ "\n"in
255             let t = "t = " ^ (CicPp.ppterm term) ^ "\n" in
256             let m = "metas = " ^ (CicMetaSubst.ppmetasenv [] metas) ^ "\n" in
257             let p = "proof = " ^ (CicPp.ppterm (Inference.build_proof_term proof))  ^ "\n" in
258               check_for_duplicates metas "gia nella metas";
259               check_for_duplicates (metasenv @ metas) ("not disjoint" ^ c ^ t ^ m ^ p)
260           end;
261         if check && not (fst (CicReduction.are_convertible
262                                 ~metasenv context termty ty ugraph)) then (
263           find_matches metasenv context ugraph lift_amount term termty tl
264         ) else
265           let do_match c eq_URI =
266             let subst', metasenv', ugraph' =
267               let t1 = Unix.gettimeofday () in
268               try
269                 let r =
270                   ( Inference.matching metasenv metas context 
271                     term (S.lift lift_amount c)) ugraph
272                 in
273                 let t2 = Unix.gettimeofday () in
274                 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
275                 r
276               with 
277                 | Inference.MatchingFailure as e ->
278                 let t2 = Unix.gettimeofday () in
279                 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
280                   raise e
281                 | CicUtil.Meta_not_found _ as exn -> raise exn
282             in
283             Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
284                   (candidate, eq_URI))
285           in
286           let c, other, eq_URI =
287             if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
288             else right, left, Utils.eq_ind_r_URI ()
289           in
290           if o <> U.Incomparable then
291             let res =
292               try
293                 do_match c eq_URI
294               with Inference.MatchingFailure ->
295                 find_matches metasenv context ugraph lift_amount term termty tl
296             in
297               if Utils.debug_res then ignore (check_res res "find1");
298               res
299           else
300             let res =
301               try do_match c eq_URI
302               with Inference.MatchingFailure -> None
303             in
304             if Utils.debug_res then ignore (check_res res "find2");
305             match res with
306             | Some (_, s, _, _, _) ->
307                 let c' = apply_subst s c in
308                 (* 
309              let other' = U.guarded_simpl context (apply_subst s other) in *)
310                 let other' = apply_subst s other in
311                 let order = cmp c' other' in
312                 if order = U.Gt then
313                   res
314                 else
315                   find_matches
316                     metasenv context ugraph lift_amount term termty tl
317             | None ->
318                 find_matches metasenv context ugraph lift_amount term termty tl
319 ;;
320
321
322 (*
323   as above, but finds all the matching equalities, and the matching condition
324   can be either Inference.matching or Inference.unification
325 *)
326 let rec find_all_matches ?(unif_fun=Inference.unification)
327     metasenv context ugraph lift_amount term termty =
328   let module C = Cic in
329   let module U = Utils in
330   let module S = CicSubstitution in
331   let module M = CicMetaSubst in
332   let module HL = HelmLibraryObjects in
333   let cmp = !Utils.compare_terms in
334   function
335     | [] -> []
336     | candidate::tl ->
337         let pos, (_, _, (ty, left, right, o), metas, args) = candidate in
338         let do_match c eq_URI =
339           let subst', metasenv', ugraph' =
340             let t1 = Unix.gettimeofday () in
341             try
342               let r = 
343                 unif_fun metasenv metas context
344                   term (S.lift lift_amount c) ugraph in
345               let t2 = Unix.gettimeofday () in
346               match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
347               r
348             with
349             | Inference.MatchingFailure
350             | CicUnification.UnificationFailure _
351             | CicUnification.Uncertain _ as e ->
352                 let t2 = Unix.gettimeofday () in
353                 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
354                 raise e
355           in
356           (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
357            (candidate, eq_URI))
358         in
359         let c, other, eq_URI =
360           if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
361           else right, left, Utils.eq_ind_r_URI ()
362         in
363         if o <> U.Incomparable then
364           try
365             let res = do_match c eq_URI in
366             res::(find_all_matches ~unif_fun metasenv context ugraph
367                     lift_amount term termty tl)
368           with
369           | Inference.MatchingFailure
370           | CicUnification.UnificationFailure _
371           | CicUnification.Uncertain _ ->
372               find_all_matches ~unif_fun metasenv context ugraph
373                 lift_amount term termty tl
374         else
375           try
376             let res = do_match c eq_URI in
377             match res with
378             | _, s, _, _, _ ->
379                 let c' = apply_subst s c
380                 and other' = apply_subst s other in
381                 let order = cmp c' other' in
382                 if order <> U.Lt && order <> U.Le then
383                   res::(find_all_matches ~unif_fun metasenv context ugraph
384                           lift_amount term termty tl)
385                 else
386                   find_all_matches ~unif_fun metasenv context ugraph
387                     lift_amount term termty tl
388           with
389           | Inference.MatchingFailure
390           | CicUnification.UnificationFailure _
391           | CicUnification.Uncertain _ ->
392               find_all_matches ~unif_fun metasenv context ugraph
393                 lift_amount term termty tl
394 ;;
395
396
397 (*
398   returns true if target is subsumed by some equality in table
399 *)
400 let subsumption env table target =
401   let _, _, (ty, left, right, _), tmetas, _ = target in
402   let metasenv, context, ugraph = env in
403   let metasenv = metasenv @ tmetas in
404   let samesubst subst subst' =
405     let tbl = Hashtbl.create (List.length subst) in
406     List.iter (fun (m, (c, t1, t2)) -> Hashtbl.add tbl m (c, t1, t2)) subst;
407     List.for_all
408       (fun (m, (c, t1, t2)) ->
409          try
410            let c', t1', t2' = Hashtbl.find tbl m in
411            if (c = c') && (t1 = t1') && (t2 = t2') then true
412            else false
413          with Not_found ->
414            true)
415       subst'
416   in
417   let leftr =
418     match left with
419     | Cic.Meta _ -> []
420     | _ ->
421         let leftc = get_candidates Matching table left in
422         find_all_matches ~unif_fun:Inference.matching
423           metasenv context ugraph 0 left ty leftc
424   in
425   let rec ok what = function
426     | [] -> false, []
427     | (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), m, _)), _))::tl ->
428         try
429           let other = if pos = Utils.Left then r else l in
430           let subst', menv', ug' =
431             let t1 = Unix.gettimeofday () in
432             try
433               let r = 
434                 Inference.matching menv m context what other ugraph
435               in
436               let t2 = Unix.gettimeofday () in
437               match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
438               r
439             with Inference.MatchingFailure as e ->
440               let t2 = Unix.gettimeofday () in
441               match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
442               raise e
443           in
444           if samesubst subst subst' then
445             true, subst
446           else
447             ok what tl
448         with Inference.MatchingFailure ->
449           ok what tl
450   in
451   let r, subst = ok right leftr in
452   let r, s =
453     if r then
454       true, subst
455     else
456       let rightr =
457         match right with
458           | Cic.Meta _ -> []
459           | _ ->
460               let rightc = get_candidates Matching table right in
461                 find_all_matches ~unif_fun:Inference.matching
462                   metasenv context ugraph 0 right ty rightc
463       in
464         ok left rightr
465   in
466 (*     (if r then  *)
467 (*        debug_print  *)
468 (*       (lazy *)
469 (*          (Printf.sprintf "SUBSUMPTION! %s\n%s\n" *)
470 (*             (Inference.string_of_equality target) (Utils.print_subst s)))); *)
471     r, s
472 ;;
473
474 let rec demodulation_aux ?from ?(typecheck=false) 
475   metasenv context ugraph table lift_amount term =
476   (* Printf.eprintf "term = %s\n" (CicPp.ppterm term); *)
477   let module C = Cic in
478   let module S = CicSubstitution in
479   let module M = CicMetaSubst in
480   let module HL = HelmLibraryObjects in
481   let candidates = 
482     get_candidates ~env:(metasenv,context,ugraph) Matching table term in
483 (*   let candidates = List.map make_variant candidates in *)
484   let res =
485     match term with
486       | C.Meta _ -> None
487       | term ->
488           let termty, ugraph =
489             if typecheck then
490               CicTypeChecker.type_of_aux' metasenv context term ugraph
491             else
492               C.Implicit None, ugraph
493           in
494           let res =
495             find_matches metasenv context ugraph lift_amount term termty candidates
496           in
497           if Utils.debug_res then ignore(check_res res "demod1"); 
498             if res <> None then
499               res
500             else
501               match term with
502                 | C.Appl l ->
503                     let res, ll = 
504                       List.fold_left
505                         (fun (res, tl) t ->
506                            if res <> None then
507                              (res, tl @ [S.lift 1 t])
508                            else 
509                              let r =
510                                demodulation_aux ~from:"1" metasenv context ugraph table
511                                  lift_amount t
512                              in
513                                match r with
514                                  | None -> (None, tl @ [S.lift 1 t])
515                                  | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
516                         (None, []) l
517                     in (
518                         match res with
519                           | None -> None
520                           | Some (_, subst, menv, ug, eq_found) ->
521                               Some (C.Appl ll, subst, menv, ug, eq_found)
522                       )
523                 | C.Prod (nn, s, t) ->
524                     let r1 =
525                       demodulation_aux ~from:"2"
526                         metasenv context ugraph table lift_amount s in (
527                         match r1 with
528                           | None ->
529                               let r2 =
530                                 demodulation_aux metasenv
531                                   ((Some (nn, C.Decl s))::context) ugraph
532                                   table (lift_amount+1) t
533                               in (
534                                   match r2 with
535                                     | None -> None
536                                     | Some (t', subst, menv, ug, eq_found) ->
537                                         Some (C.Prod (nn, (S.lift 1 s), t'),
538                                               subst, menv, ug, eq_found)
539                                 )
540                           | Some (s', subst, menv, ug, eq_found) ->
541                               Some (C.Prod (nn, s', (S.lift 1 t)),
542                                     subst, menv, ug, eq_found)
543                       )
544                 | C.Lambda (nn, s, t) ->
545                     let r1 =
546                       demodulation_aux 
547                         metasenv context ugraph table lift_amount s in (
548                         match r1 with
549                           | None ->
550                               let r2 =
551                                 demodulation_aux metasenv
552                                   ((Some (nn, C.Decl s))::context) ugraph
553                                   table (lift_amount+1) t
554                               in (
555                                   match r2 with
556                                     | None -> None
557                                     | Some (t', subst, menv, ug, eq_found) ->
558                                         Some (C.Lambda (nn, (S.lift 1 s), t'),
559                                               subst, menv, ug, eq_found)
560                                 )
561                           | Some (s', subst, menv, ug, eq_found) ->
562                               Some (C.Lambda (nn, s', (S.lift 1 t)),
563                                     subst, menv, ug, eq_found)
564                       )
565                 | t ->
566                     None
567   in
568   if Utils.debug_res then ignore(check_res res "demod_aux output"); 
569   res
570 ;;
571
572
573 let build_newtarget_time = ref 0.;;
574
575
576 let demod_counter = ref 1;;
577
578 exception Foo
579
580 (** demodulation, when target is an equality *)
581 let rec demodulation_equality ?from newmeta env table sign target =
582   let module C = Cic in
583   let module S = CicSubstitution in
584   let module M = CicMetaSubst in
585   let module HL = HelmLibraryObjects in
586   let module U = Utils in
587   let metasenv, context, ugraph = env in
588   let w, proof, (eq_ty, left, right, order), metas, args = target in
589   (* first, we simplify *)
590   let right = U.guarded_simpl context right in
591   let left = U.guarded_simpl context left in
592   let order = !Utils.compare_terms left right in
593   let stat = (eq_ty, left, right, order) in 
594   let w = Utils.compute_equality_weight stat in
595   let target = w, proof, stat, metas, args in
596   if Utils.debug_metas then 
597     ignore(check_target context target "demod equalities input");
598   let metasenv' = (* metasenv @ *) metas in
599   let maxmeta = ref newmeta in
600   
601   let build_newtarget is_left (t, subst, menv, ug, (eq_found, eq_URI)) =
602     let time1 = Unix.gettimeofday () in
603     
604     if Utils.debug_metas then
605       begin
606         ignore(check_for_duplicates menv "input1");
607         ignore(check_disjoint_invariant subst menv "input2");
608         let substs = CicMetaSubst.ppsubst subst in 
609         ignore(check_target context (snd eq_found) ("input3" ^ substs))
610       end;
611     let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
612     let ty =
613     try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
614       with CicUtil.Meta_not_found _ -> ty
615     in
616     let what, other = if pos = Utils.Left then what, other else other, what in
617     let newterm, newproof =
618       let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
619       let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in
620       incr demod_counter;
621       let bo' =
622         let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
623           C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
624                   S.lift 1 eq_ty; l; r]
625       in
626       if sign = Utils.Positive then
627           (bo,
628            Inference.ProofBlock (
629              subst, eq_URI, (name, ty), bo'(* t' *), eq_found, proof))
630       else
631         let metaproof = 
632           incr maxmeta;
633           let irl =
634             CicMkImplicit.identity_relocation_list_for_metavariable context in
635 (*           debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
636 (*           print_newline (); *)
637           C.Meta (!maxmeta, irl)
638         in
639           let eq_found =
640             let proof' =
641               let termlist =
642                 if pos = Utils.Left then [ty; what; other]
643                 else [ty; other; what]
644               in
645               Inference.ProofSymBlock (termlist, proof')
646             in
647             let what, other =
648               if pos = Utils.Left then what, other else other, what
649             in
650             pos, (0, proof', (ty, other, what, Utils.Incomparable),
651                   menv', args')
652           in
653           let target_proof =
654             let pb =
655               Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
656                                     eq_found, Inference.BasicProof metaproof)
657             in
658             match proof with
659             | Inference.BasicProof _ ->
660                 (* print_endline "replacing a BasicProof"; *)
661                 pb
662             | Inference.ProofGoalBlock (_, parent_proof) ->
663               
664   (* print_endline "replacing another ProofGoalBlock"; *)
665                 Inference.ProofGoalBlock (pb, parent_proof)
666             | _ -> assert false
667           in
668         let refl =
669           C.Appl [C.MutConstruct (* reflexivity *)
670                     (LibraryObjects.eq_URI (), 0, 1, []);
671                   eq_ty; if is_left then right else left]          
672         in
673         (bo,
674          Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
675     in
676     let newmenv = (* Inference.filter subst *) menv in
677     let _ = 
678       if Utils.debug_metas then 
679         try ignore(CicTypeChecker.type_of_aux'
680           newmenv context (Inference.build_proof_term newproof) ugraph);
681           () 
682         with exc ->                   
683           prerr_endline "sempre lui";
684           prerr_endline (CicMetaSubst.ppsubst subst);
685           prerr_endline (CicPp.ppterm (Inference.build_proof_term newproof));
686           prerr_endline ("+++++++++++++termine: " ^ (CicPp.ppterm t));
687           prerr_endline ("+++++++++++++what: " ^ (CicPp.ppterm what));
688           prerr_endline ("+++++++++++++other: " ^ (CicPp.ppterm other));
689           prerr_endline ("+++++++++++++subst: " ^ (CicMetaSubst.ppsubst subst));
690           raise exc;
691       else () 
692     in
693     let left, right = if is_left then newterm, right else left, newterm in
694     let ordering = !Utils.compare_terms left right in
695     let stat = (eq_ty, left, right, ordering) in
696     let time2 = Unix.gettimeofday () in
697     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
698     let res =
699       let w = Utils.compute_equality_weight stat in
700       (w, newproof, stat,newmenv,args) in
701     if Utils.debug_metas then 
702       ignore(check_target context res "buildnew_target output");
703     !maxmeta, res 
704   in
705
706   let res = demodulation_aux ~from:"3" metasenv' context ugraph table 0 left in
707   if Utils.debug_res then check_res res "demod result";
708   let newmeta, newtarget = 
709     match res with
710     | Some t ->
711         let newmeta, newtarget = build_newtarget true t in
712           if (Inference.is_weak_identity (metasenv', context, ugraph) newtarget) ||
713             (Inference.meta_convertibility_eq target newtarget) then
714               newmeta, newtarget
715           else 
716             demodulation_equality newmeta env table sign newtarget
717     | None ->
718         let res = demodulation_aux metasenv' context ugraph table 0 right in
719         if Utils.debug_res then check_res res "demod result 1"; 
720           match res with
721           | Some t ->
722               let newmeta, newtarget = build_newtarget false t in
723                 if (Inference.is_weak_identity (metasenv', context, ugraph) newtarget) ||
724                   (Inference.meta_convertibility_eq target newtarget) then
725                     newmeta, newtarget
726                 else
727                    demodulation_equality newmeta env table sign newtarget
728           | None ->
729               newmeta, target
730   in
731   (* newmeta, newtarget *)
732   newmeta,newtarget 
733 ;;
734
735
736 (**
737    Performs the beta expansion of the term "term" w.r.t. "table",
738    i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
739    in table.
740 *)
741 let rec betaexpand_term metasenv context ugraph table lift_amount term =
742   let module C = Cic in
743   let module S = CicSubstitution in
744   let module M = CicMetaSubst in
745   let module HL = HelmLibraryObjects in
746   let candidates = get_candidates Unification table term in
747   
748   let res, lifted_term = 
749     match term with
750     | C.Meta (i, l) ->
751         let l', lifted_l =
752           List.fold_right
753             (fun arg (res, lifted_tl) ->
754                match arg with
755                | Some arg ->
756                    let arg_res, lifted_arg =
757                      betaexpand_term metasenv context ugraph table
758                        lift_amount arg in
759                    let l1 =
760                      List.map
761                        (fun (t, s, m, ug, eq_found) ->
762                           (Some t)::lifted_tl, s, m, ug, eq_found)
763                        arg_res
764                    in
765                    (l1 @
766                       (List.map
767                          (fun (l, s, m, ug, eq_found) ->
768                             (Some lifted_arg)::l, s, m, ug, eq_found)
769                          res),
770                     (Some lifted_arg)::lifted_tl)
771                | None ->
772                    (List.map
773                       (fun (r, s, m, ug, eq_found) ->
774                          None::r, s, m, ug, eq_found) res,
775                     None::lifted_tl)
776             ) l ([], [])
777         in
778         let e =
779           List.map
780             (fun (l, s, m, ug, eq_found) ->
781                (C.Meta (i, l), s, m, ug, eq_found)) l'
782         in
783         e, C.Meta (i, lifted_l)
784           
785     | C.Rel m ->
786         [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
787           
788     | C.Prod (nn, s, t) ->
789         let l1, lifted_s =
790           betaexpand_term metasenv context ugraph table lift_amount s in
791         let l2, lifted_t =
792           betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
793             table (lift_amount+1) t in
794         let l1' =
795           List.map
796             (fun (t, s, m, ug, eq_found) ->
797                C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
798         and l2' =
799           List.map
800             (fun (t, s, m, ug, eq_found) ->
801                C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
802         l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
803           
804     | C.Lambda (nn, s, t) ->
805         let l1, lifted_s =
806           betaexpand_term metasenv context ugraph table lift_amount s in
807         let l2, lifted_t =
808           betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
809             table (lift_amount+1) t in
810         let l1' =
811           List.map
812             (fun (t, s, m, ug, eq_found) ->
813                C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
814         and l2' =
815           List.map
816             (fun (t, s, m, ug, eq_found) ->
817                C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
818         l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
819
820     | C.Appl l ->
821         let l', lifted_l =
822           List.fold_right
823             (fun arg (res, lifted_tl) ->
824                let arg_res, lifted_arg =
825                  betaexpand_term metasenv context ugraph table lift_amount arg
826                in
827                let l1 =
828                  List.map
829                    (fun (a, s, m, ug, eq_found) ->
830                       a::lifted_tl, s, m, ug, eq_found)
831                    arg_res
832                in
833                (l1 @
834                   (List.map
835                      (fun (r, s, m, ug, eq_found) ->
836                         lifted_arg::r, s, m, ug, eq_found)
837                      res),
838                 lifted_arg::lifted_tl)
839             ) l ([], [])
840         in
841         (List.map
842            (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
843          C.Appl lifted_l)
844
845     | t -> [], (S.lift lift_amount t)
846   in
847   match term with
848   | C.Meta (i, l) -> res, lifted_term
849   | term ->
850       let termty, ugraph =
851         C.Implicit None, ugraph
852 (*         CicTypeChecker.type_of_aux' metasenv context term ugraph *)
853       in
854       let r = 
855         find_all_matches
856           metasenv context ugraph lift_amount term termty candidates
857       in
858       r @ res, lifted_term
859 ;;
860
861
862 let sup_l_counter = ref 1;;
863
864 (**
865    superposition_left 
866    returns a list of new clauses inferred with a left superposition step
867    the negative equation "target" and one of the positive equations in "table"
868 *)
869 let superposition_left newmeta (metasenv, context, ugraph) table target =
870   let module C = Cic in
871   let module S = CicSubstitution in
872   let module M = CicMetaSubst in
873   let module HL = HelmLibraryObjects in
874   let module CR = CicReduction in
875   let module U = Utils in
876   let weight, proof, (eq_ty, left, right, ordering), menv, _ = target in
877   if Utils.debug_metas then
878     ignore(check_target context target "superpositionleft");
879   let expansions, _ =
880     let term = if ordering = U.Gt then left else right in
881       begin 
882         let t1 = Unix.gettimeofday () in
883         let res = betaexpand_term metasenv context ugraph table 0 term in
884         let t2 = Unix.gettimeofday () in
885           beta_expand_time := !beta_expand_time  +. (t2 -. t1);
886         res
887       end
888   in
889   let maxmeta = ref newmeta in
890   let build_new (bo, s, m, ug, (eq_found, eq_URI)) =
891 (*     debug_print (lazy "\nSUPERPOSITION LEFT\n"); *)
892     let time1 = Unix.gettimeofday () in
893     
894     let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
895     let what, other = if pos = Utils.Left then what, other else other, what in
896     let newgoal, newproof =
897       let bo' =  U.guarded_simpl context (apply_subst s (S.subst other bo)) in
898       let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in
899       incr sup_l_counter;
900       let bo'' = 
901         let l, r =
902           if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
903         C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
904                 S.lift 1 eq_ty; l; r]
905       in
906       incr maxmeta;
907       let metaproof =
908         let irl =
909           CicMkImplicit.identity_relocation_list_for_metavariable context in
910         C.Meta (!maxmeta, irl)
911       in
912       let eq_found =
913         let proof' =
914           let termlist =
915             if pos = Utils.Left then [ty; what; other]
916             else [ty; other; what]
917           in
918           Inference.ProofSymBlock (termlist, proof')
919         in
920         let what, other =
921           if pos = Utils.Left then what, other else other, what
922         in
923         pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args')
924       in
925       let target_proof =
926         let pb =
927           Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found,
928                                 Inference.BasicProof metaproof)
929         in
930         match proof with
931         | Inference.BasicProof _ ->
932 (*             debug_print (lazy "replacing a BasicProof"); *)
933             pb
934         | Inference.ProofGoalBlock (_, parent_proof) ->
935 (*             debug_print (lazy "replacing another ProofGoalBlock"); *)
936             Inference.ProofGoalBlock (pb, parent_proof)
937         | _ -> assert false
938       in
939       let refl =
940         C.Appl [C.MutConstruct (* reflexivity *)
941                   (LibraryObjects.eq_URI (), 0, 1, []);
942                 eq_ty; if ordering = U.Gt then right else left]
943       in
944       (bo',
945        Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
946     in
947     let left, right =
948       if ordering = U.Gt then newgoal, right else left, newgoal in
949     let neworder = !Utils.compare_terms left right in
950     let stat = (eq_ty, left, right, neworder) in
951     let newmenv = (* Inference.filter s *) menv in  
952     let time2 = Unix.gettimeofday () in
953     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
954
955     let w = Utils.compute_equality_weight stat in
956     (w, newproof, stat, newmenv, []) 
957
958   in
959   !maxmeta, List.map build_new expansions
960 ;;
961
962
963 let sup_r_counter = ref 1;;
964
965 (**
966    superposition_right
967    returns a list of new clauses inferred with a right superposition step
968    between the positive equation "target" and one in the "table" "newmeta" is
969    the first free meta index, i.e. the first number above the highest meta
970    index: its updated value is also returned
971 *)
972 let superposition_right newmeta (metasenv, context, ugraph) table target =
973   let module C = Cic in
974   let module S = CicSubstitution in
975   let module M = CicMetaSubst in
976   let module HL = HelmLibraryObjects in
977   let module CR = CicReduction in
978   let module U = Utils in 
979   let w, eqproof, (eq_ty, left, right, ordering), newmetas, args = target in 
980   if Utils.debug_metas then 
981     ignore (check_target context target "superpositionright");
982   let metasenv' = newmetas in
983   let maxmeta = ref newmeta in
984   let res1, res2 =
985     let betaexpand_term metasenv context ugraph table d term =
986       let t1 = Unix.gettimeofday () in
987       let res = betaexpand_term metasenv context ugraph table d term in
988       let t2 = Unix.gettimeofday () in
989         beta_expand_time := !beta_expand_time  +. (t2 -. t1);
990         res
991     in
992     match ordering with
993     | U.Gt -> fst (betaexpand_term metasenv' context ugraph table 0 left), []
994     | U.Lt -> [], fst (betaexpand_term metasenv' context ugraph table 0 right)
995     | _ ->
996         let res l r =
997           List.filter
998             (fun (_, subst, _, _, _) ->
999                let subst = apply_subst subst in
1000                let o = !Utils.compare_terms (subst l) (subst r) in
1001                o <> U.Lt && o <> U.Le)
1002             (fst (betaexpand_term metasenv' context ugraph table 0 l))
1003         in
1004         (res left right), (res right left)
1005   in
1006   let build_new ordering ((bo, s, m, ug, (eq_found, eq_URI)) as input) =
1007     if Utils.debug_metas then 
1008       ignore (check_target context (snd eq_found) "buildnew1" );
1009     let time1 = Unix.gettimeofday () in
1010     
1011     let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
1012     let what, other = if pos = Utils.Left then what, other else other, what in
1013     let newgoal, newproof =
1014       (* qua *)
1015       let bo' = Utils.guarded_simpl context (apply_subst s (S.subst other bo)) in
1016       let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in
1017       incr sup_r_counter;
1018       let bo'' =
1019         let l, r =
1020           if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
1021         C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
1022                 S.lift 1 eq_ty; l; r]
1023       in
1024       bo',
1025       Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, eqproof)
1026     in
1027     let newmeta, newequality = 
1028       let left, right =
1029         if ordering = U.Gt then newgoal, apply_subst s right
1030         else apply_subst s left, newgoal in
1031       let neworder = !Utils.compare_terms left right in
1032       let newmenv = (* Inference.filter s *) m in
1033       let newargs = args @ args' in
1034       let stat = (eq_ty, left, right, neworder) in
1035       let eq' =
1036         let w = Utils.compute_equality_weight stat in
1037         (w, newproof, stat, newmenv, newargs) in
1038       if Utils.debug_metas then 
1039         ignore (check_target context eq' "buildnew3");
1040       let newm, eq' = Inference.fix_metas !maxmeta eq' in
1041       if Utils.debug_metas then 
1042         ignore (check_target context eq' "buildnew4");
1043       newm, eq'
1044     in
1045     maxmeta := newmeta;
1046     let time2 = Unix.gettimeofday () in
1047     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
1048     if Utils.debug_metas then 
1049       ignore(check_target context newequality "buildnew2"); 
1050     newequality
1051   in
1052   let new1 = List.map (build_new U.Gt) res1
1053   and new2 = List.map (build_new U.Lt) res2 in
1054   let ok e = not (Inference.is_identity (metasenv', context, ugraph) e) in
1055   (!maxmeta,
1056    (List.filter ok (new1 @ new2)))
1057 ;;
1058
1059
1060 (** demodulation, when the target is a goal *)
1061 let rec demodulation_goal newmeta env table goal =
1062   let module C = Cic in
1063   let module S = CicSubstitution in
1064   let module M = CicMetaSubst in
1065   let module HL = HelmLibraryObjects in
1066   let metasenv, context, ugraph = env in
1067   let maxmeta = ref newmeta in
1068   let proof, metas, term = goal in
1069   let term = Utils.guarded_simpl (~debug:true) context term in
1070   let goal = proof, metas, term in
1071   let metasenv' = metas in
1072
1073   let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) =
1074     let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
1075     let what, other = if pos = Utils.Left then what, other else other, what in
1076     let ty =
1077       try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
1078       with CicUtil.Meta_not_found _ -> ty
1079     in
1080     let newterm, newproof =
1081       let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
1082       let bo' = apply_subst subst t in 
1083       let name = C.Name ("x_DemodGoal_" ^ (string_of_int !demod_counter)) in
1084       incr demod_counter;
1085       let metaproof = 
1086         incr maxmeta;
1087         let irl =
1088           CicMkImplicit.identity_relocation_list_for_metavariable context in
1089 (*         debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
1090         C.Meta (!maxmeta, irl)
1091       in
1092       let eq_found =
1093         let proof' =
1094           let termlist =
1095             if pos = Utils.Left then [ty; what; other]
1096             else [ty; other; what]
1097           in
1098           Inference.ProofSymBlock (termlist, proof')
1099         in
1100         let what, other =
1101           if pos = Utils.Left then what, other else other, what
1102         in
1103         pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args')
1104       in
1105       let goal_proof =
1106         let pb =
1107           Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
1108                                 eq_found, Inference.BasicProof metaproof)
1109         in
1110         let rec repl = function
1111           | Inference.NoProof ->
1112 (*               debug_print (lazy "replacing a NoProof"); *)
1113               pb
1114           | Inference.BasicProof _ ->
1115 (*               debug_print (lazy "replacing a BasicProof"); *)
1116               pb
1117           | Inference.ProofGoalBlock (_, parent_proof) ->
1118 (*               debug_print (lazy "replacing another ProofGoalBlock"); *)
1119               Inference.ProofGoalBlock (pb, parent_proof)
1120           | Inference.SubProof (term, meta_index, p)  ->
1121               Inference.SubProof (term, meta_index, repl p)
1122           | _ -> assert false
1123         in repl proof
1124       in
1125       bo, Inference.ProofGoalBlock (Inference.NoProof, goal_proof)
1126     in
1127     let newmetasenv = (* Inference.filter subst *) menv in
1128     !maxmeta, (newproof, newmetasenv, newterm)
1129   in  
1130   let res =
1131     demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 term
1132   in
1133   match res with
1134   | Some t ->
1135       let newmeta, newgoal = build_newgoal t in
1136       let _, _, newg = newgoal in
1137       if Inference.meta_convertibility term newg then
1138         newmeta, newgoal
1139       else
1140         demodulation_goal newmeta env table newgoal
1141   | None ->
1142       newmeta, goal
1143 ;;
1144
1145
1146 (** demodulation, when the target is a theorem *)
1147 let rec demodulation_theorem newmeta env table theorem =
1148   let module C = Cic in
1149   let module S = CicSubstitution in
1150   let module M = CicMetaSubst in
1151   let module HL = HelmLibraryObjects in
1152   let metasenv, context, ugraph = env in
1153   let maxmeta = ref newmeta in
1154   let term, termty, metas = theorem in
1155   let metasenv' = metas in
1156   
1157   let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
1158     let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
1159     let what, other = if pos = Utils.Left then what, other else other, what in
1160     let newterm, newty =
1161       let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
1162       let bo' = apply_subst subst t in 
1163       let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in
1164       incr demod_counter;
1165       let newproof =
1166         Inference.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
1167                               Inference.BasicProof term)
1168       in
1169       (Inference.build_proof_term newproof, bo)
1170     in    
1171     
1172     let m = Inference.metas_of_term newterm in
1173     !maxmeta, (newterm, newty, menv)
1174   in  
1175   let res =
1176     demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 termty
1177   in
1178   match res with
1179   | Some t ->
1180       let newmeta, newthm = build_newtheorem t in
1181       let newt, newty, _ = newthm in
1182       if Inference.meta_convertibility termty newty then
1183         newmeta, newthm
1184       else
1185         demodulation_theorem newmeta env table newthm
1186   | None ->
1187       newmeta, theorem
1188 ;;
1189