args removed from equalities.

[helm.git] / components / tactics / paramodulation / indexing.ml

diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml
index bbc60562089780ec0c0956bca1ba768e8676b71a..48abdf84e2eceea23eefaf0057828c297ca1dec2 100644 (file)
--- a/components/tactics/paramodulation/indexing.ml
+++ b/components/tactics/paramodulation/indexing.ml
@@ -112,13 +112,7 @@ let check_disjoint_invariant subst metasenv msg =
 ;;
 
 let check_for_duplicates metas msg =
-let _ = 
-    try
-      ignore(CicUtil.lookup_meta 190 metas);
-      prerr_endline ("eccoci in " ^ msg);
-    with
-       CicUtil.Meta_not_found _ -> () in
-if List.length metas <> 
+  if List.length metas <> 
   List.length (HExtlib.list_uniq (List.sort Pervasives.compare metas)) then
     begin 
       prerr_endline ("DUPLICATI " ^ msg);
@@ -137,7 +131,7 @@ let check_res res msg =
 ;;
 
 let check_target context target msg =
-  let w, proof, (eq_ty, left, right, order), metas, args = target in
+  let w, proof, (eq_ty, left, right, order), metas = target in
   (* check that metas does not contains duplicates *)
   let eqs = Inference.string_of_equality target in
   let _ = check_for_duplicates metas (msg ^ "\nchecking " ^ eqs) in
@@ -246,7 +240,7 @@ let rec find_matches metasenv context ugraph lift_amount term termty =
   function
     | [] -> None
     | candidate::tl ->
-        let pos, (_, proof, (ty, left, right, o), metas, args) = candidate in
+        let pos, (_, proof, (ty, left, right, o), metas) = candidate in
         if Utils.debug_metas then 
          ignore(check_target context (snd candidate) "find_matches");
         if Utils.debug_res then 
@@ -334,7 +328,7 @@ let rec find_all_matches ?(unif_fun=Inference.unification)
   function
     | [] -> []
     | candidate::tl ->
-        let pos, (_, _, (ty, left, right, o), metas, args) = candidate in
+        let pos, (_, _, (ty, left, right, o), metas) = candidate in
         let do_match c eq_URI =
           let subst', metasenv', ugraph' =
             let t1 = Unix.gettimeofday () in
@@ -398,7 +392,7 @@ let rec find_all_matches ?(unif_fun=Inference.unification)
   returns true if target is subsumed by some equality in table
 *)
 let subsumption env table target =
-  let _, _, (ty, left, right, _), tmetas, _ = target in
+  let _, _, (ty, left, right, _), tmetas = target in
   let metasenv, context, ugraph = env in
   let metasenv = metasenv @ tmetas in
   let samesubst subst subst' =
@@ -424,7 +418,7 @@ let subsumption env table target =
   in
   let rec ok what = function
     | [] -> false, []
-    | (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), m, _)), _))::tl ->
+    | (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), m)), _))::tl ->
         try
           let other = if pos = Utils.Left then r else l in
           let subst', menv', ug' =
@@ -585,14 +579,14 @@ let rec demodulation_equality ?from newmeta env table sign target =
   let module HL = HelmLibraryObjects in
   let module U = Utils in
   let metasenv, context, ugraph = env in
-  let w, proof, (eq_ty, left, right, order), metas, args = target in
+  let w, proof, (eq_ty, left, right, order), metas = target in
   (* first, we simplify *)
   let right = U.guarded_simpl context right in
   let left = U.guarded_simpl context left in
   let order = !Utils.compare_terms left right in
   let stat = (eq_ty, left, right, order) in 
   let w = Utils.compute_equality_weight stat in
-  let target = w, proof, stat, metas, args in
+  let target = w, proof, stat, metas in
   if Utils.debug_metas then 
     ignore(check_target context target "demod equalities input");
   let metasenv' = (* metasenv @ *) metas in
@@ -608,7 +602,7 @@ let rec demodulation_equality ?from newmeta env table sign target =
         let substs = CicMetaSubst.ppsubst subst in 
        ignore(check_target context (snd eq_found) ("input3" ^ substs))
       end;
-    let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
+    let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
     let ty =
     try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
       with CicUtil.Meta_not_found _ -> ty
@@ -647,8 +641,7 @@ let rec demodulation_equality ?from newmeta env table sign target =
             let what, other =
               if pos = Utils.Left then what, other else other, what
             in
-            pos, (0, proof', (ty, other, what, Utils.Incomparable),
-                  menv', args')
+            pos, (0, proof', (ty, other, what, Utils.Incomparable),menv')
           in
           let target_proof =
             let pb =
@@ -697,7 +690,7 @@ let rec demodulation_equality ?from newmeta env table sign target =
     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
     let res =
       let w = Utils.compute_equality_weight stat in
-      (w, newproof, stat,newmenv,args) in
+      (w, newproof, stat,newmenv) in
     if Utils.debug_metas then 
       ignore(check_target context res "buildnew_target output");
     !maxmeta, res 
@@ -873,7 +866,7 @@ let superposition_left newmeta (metasenv, context, ugraph) table target =
   let module HL = HelmLibraryObjects in
   let module CR = CicReduction in
   let module U = Utils in
-  let weight, proof, (eq_ty, left, right, ordering), menv, _ = target in
+  let weight, proof, (eq_ty, left, right, ordering), menv = target in
   if Utils.debug_metas then
     ignore(check_target context target "superpositionleft");
   let expansions, _ =
@@ -891,7 +884,7 @@ let superposition_left newmeta (metasenv, context, ugraph) table target =
 (*     debug_print (lazy "\nSUPERPOSITION LEFT\n"); *)
     let time1 = Unix.gettimeofday () in
     
-    let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
+    let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
     let what, other = if pos = Utils.Left then what, other else other, what in
     let newgoal, newproof =
       let bo' =  U.guarded_simpl context (apply_subst s (S.subst other bo)) in
@@ -920,7 +913,7 @@ let superposition_left newmeta (metasenv, context, ugraph) table target =
         let what, other =
           if pos = Utils.Left then what, other else other, what
         in
-        pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args')
+        pos, (0, proof', (ty, other, what, Utils.Incomparable), menv')
       in
       let target_proof =
         let pb =
@@ -953,7 +946,7 @@ let superposition_left newmeta (metasenv, context, ugraph) table target =
     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
 
     let w = Utils.compute_equality_weight stat in
-    (w, newproof, stat, newmenv, []) 
+    (w, newproof, stat, newmenv) 
 
   in
   !maxmeta, List.map build_new expansions
@@ -976,7 +969,7 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
   let module HL = HelmLibraryObjects in
   let module CR = CicReduction in
   let module U = Utils in 
-  let w, eqproof, (eq_ty, left, right, ordering), newmetas, args = target in 
+  let w, eqproof, (eq_ty, left, right, ordering), newmetas = target in 
   if Utils.debug_metas then 
     ignore (check_target context target "superpositionright");
   let metasenv' = newmetas in
@@ -1008,7 +1001,7 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
       ignore (check_target context (snd eq_found) "buildnew1" );
     let time1 = Unix.gettimeofday () in
     
-    let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
+    let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
     let what, other = if pos = Utils.Left then what, other else other, what in
     let newgoal, newproof =
       (* qua *)
@@ -1030,11 +1023,10 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
         else apply_subst s left, newgoal in
       let neworder = !Utils.compare_terms left right in
       let newmenv = (* Inference.filter s *) m in
-      let newargs = args @ args' in
       let stat = (eq_ty, left, right, neworder) in
       let eq' =
         let w = Utils.compute_equality_weight stat in
-        (w, newproof, stat, newmenv, newargs) in
+        (w, newproof, stat, newmenv) in
       if Utils.debug_metas then 
        ignore (check_target context eq' "buildnew3");
       let newm, eq' = Inference.fix_metas !maxmeta eq' in
@@ -1071,7 +1063,7 @@ let rec demodulation_goal newmeta env table goal =
   let metasenv' = metas in
 
   let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) =
-    let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
+    let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
     let what, other = if pos = Utils.Left then what, other else other, what in
     let ty =
       try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
@@ -1100,7 +1092,7 @@ let rec demodulation_goal newmeta env table goal =
         let what, other =
           if pos = Utils.Left then what, other else other, what
         in
-        pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args')
+        pos, (0, proof', (ty, other, what, Utils.Incomparable), menv')
       in
       let goal_proof =
         let pb =
@@ -1155,7 +1147,7 @@ let rec demodulation_theorem newmeta env table theorem =
   let metasenv' = metas in
   
   let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
-    let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
+    let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
     let what, other = if pos = Utils.Left then what, other else other, what in
     let newterm, newty =
       let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in