args removed from equalities.

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

diff --git a/components/tactics/paramodulation/inference.ml b/components/tactics/paramodulation/inference.ml
index f5508c8c146cc72bc2c418b5ae80770febf6fd4c..6582bfd258f09d5e5619345e135b49a26d6daec0 100644 (file)
--- a/components/tactics/paramodulation/inference.ml
+++ b/components/tactics/paramodulation/inference.ml
@@ -37,8 +37,7 @@ type equality =
      Cic.term *          (* left side *)
      Cic.term *          (* right side *)
      Utils.comparison) * (* ordering *)  
-    Cic.metasenv *       (* environment for metas *)
-    Cic.term list        (* arguments *)
+    Cic.metasenv        (* environment for metas *)
 
 and proof =
   | NoProof (* term is the goal missing a proof *)
@@ -55,14 +54,14 @@ let string_of_equality ?env =
   match env with
   | None -> (
       function
-        | w, _, (ty, left, right, o), _, _ ->
+        | w, _, (ty, left, right, o), _ ->
             Printf.sprintf "Weight: %d, {%s}: %s =(%s) %s" w (CicPp.ppterm ty)
               (CicPp.ppterm left) (string_of_comparison o) (CicPp.ppterm right)
     )
   | Some (_, context, _) -> (
       let names = names_of_context context in
       function
-        | w, _, (ty, left, right, o), _, _ ->
+        | w, _, (ty, left, right, o), _ ->
             Printf.sprintf "Weight: %d, {%s}: %s =(%s) %s" w (CicPp.pp ty names)
               (CicPp.pp left names) (string_of_comparison o)
               (CicPp.pp right names)
@@ -139,11 +138,11 @@ let build_proof_term ?(noproof=Cic.Implicit None) proof =
     | ProofBlock (subst, eq_URI, (name, ty), bo, (pos, eq), eqproof) ->
         let t' = Cic.Lambda (name, ty, bo) in
         let proof' =
-          let _, proof', _, _, _ = eq in
+          let _, proof', _, _ = eq in
           do_build_proof proof'
         in
         let eqproof = do_build_proof eqproof in
-        let _, _, (ty, what, other, _), menv', args' = eq in
+        let _, _, (ty, what, other, _), menv' = eq in
         let what, other =
           if pos = Utils.Left then what, other else other, what
         in
@@ -311,8 +310,8 @@ let meta_convertibility_aux table t1 t2 =
 
 
 let meta_convertibility_eq eq1 eq2 =
-  let _, _, (ty, left, right, _), _, _ = eq1
-  and _, _, (ty', left', right', _), _, _ = eq2 in
+  let _, _, (ty, left, right, _), _ = eq1
+  and _, _, (ty', left', right', _), _ = eq2 in
   if ty <> ty' then
     false
   else if (left = left') && (right = right') then
@@ -726,7 +725,7 @@ let matching metasenv1 metasenv2 context t1 t2 ugraph =
 let matching = matching1;;
 
 let check_eq context msg eq =
-  let w, proof, (eq_ty, left, right, order), metas, args = eq in
+  let w, proof, (eq_ty, left, right, order), metas = eq in
   if not (fst (CicReduction.are_convertible ~metasenv:metas context eq_ty
    (fst (CicTypeChecker.type_of_aux' metas context  left CicUniv.empty_ugraph))
    CicUniv.empty_ugraph))
@@ -773,7 +772,7 @@ let find_equalities context proof =
                     let stat = (ty,t1,t2,o) in
                     let w = compute_equality_weight stat in
                     let proof = BasicProof p in
-                    let e = (w, proof, stat, newmetas, args) in
+                    let e = (w, proof, stat, newmetas) in
                     Some e, (newmeta+1)
                 | _ -> None, newmeta
               )
@@ -785,7 +784,7 @@ let find_equalities context proof =
               let o = !Utils.compare_terms t1 t2 in
               let stat = (ty,t1,t2,o) in
               let w = compute_equality_weight stat in
-              let e = (w, BasicProof (C.Rel index), stat, [], []) in
+              let e = (w, BasicProof (C.Rel index), stat, []) in
               Some e, (newmeta+1)
           | _ -> None, newmeta
         in (
@@ -923,7 +922,7 @@ let find_library_equalities dbd context status maxmeta =
                     let stat = (ty,t1,t2,o) in
                     let w = compute_equality_weight stat in
                     let proof = BasicProof p in
-                    let e = (w, proof, stat, newmetas, args) in
+                    let e = (w, proof, stat, newmetas) in
                     Some e, (newmeta+1)
                 | _ -> None, newmeta
               )
@@ -932,7 +931,7 @@ let find_library_equalities dbd context status maxmeta =
               let o = !Utils.compare_terms t1 t2 in
               let stat = (ty,t1,t2,o) in
               let w = compute_equality_weight stat in
-              let e = (w, BasicProof term, stat, [], []) in
+              let e = (w, BasicProof term, stat, []) in
               Some e, (newmeta+1)
           | _ -> None, newmeta
         in
@@ -1135,7 +1134,7 @@ let relocate newmeta menv =
   subst, metasenv, newmeta
 
 
-let fix_metas newmeta (w, p, (ty, left, right, o), menv, args) =
+let fix_metas newmeta (w, p, (ty, left, right, o), menv) =
   (*
   let metas = (metas_of_term left)@(metas_of_term right)
     @(metas_of_term ty)@(metas_of_proof p) in
@@ -1149,7 +1148,6 @@ let fix_metas newmeta (w, p, (ty, left, right, o), menv, args) =
   let ty = CicMetaSubst.apply_subst subst ty in
   let left = CicMetaSubst.apply_subst subst left in
   let right = CicMetaSubst.apply_subst subst right in
-  let args = List.map (CicMetaSubst.apply_subst subst) args in
   let rec fix_proof = function
     | NoProof -> NoProof 
     | BasicProof term -> BasicProof (CicMetaSubst.apply_subst subst term)
@@ -1171,7 +1169,7 @@ let fix_metas newmeta (w, p, (ty, left, right, o), menv, args) =
     @(metas_of_term ty)@(metas_of_proof p) in
   let metasenv = List.filter (fun (i, _, _) -> List.mem i metas) metasenv in
   *)
-  let eq = (w, p, (ty, left, right, o), metasenv, args) in
+  let eq = (w, p, (ty, left, right, o), metasenv) in
   (* debug prerr_endline (string_of_equality eq); *)
   newmeta+1, eq  
 
@@ -1193,7 +1191,7 @@ let equality_of_term proof term =
       let o = !Utils.compare_terms t1 t2 in
       let stat = (ty,t1,t2,o) in
       let w = compute_equality_weight stat in
-      let e = (w, BasicProof proof, stat, [], []) in
+      let e = (w, BasicProof proof, stat, []) in
       e
   | _ ->
       raise TermIsNotAnEquality
@@ -1203,7 +1201,7 @@ let equality_of_term proof term =
 type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
 
 let is_weak_identity (metasenv, context, ugraph) = function
-  | (_, _, (ty, left, right, _), menv, _) -> 
+  | (_, _, (ty, left, right, _), menv) -> 
        (left = right ||
           (meta_convertibility left right)) 
           (* the test below is not a good idea since it stops
@@ -1213,7 +1211,7 @@ let is_weak_identity (metasenv, context, ugraph) = function
 ;;
 
 let is_identity (metasenv, context, ugraph) = function
-  | (_, _, (ty, left, right, _), menv, _) ->
+  | (_, _, (ty, left, right, _), menv) ->
        (left = right ||
           (* (meta_convertibility left right)) *)
            (fst (CicReduction.are_convertible 
@@ -1222,7 +1220,7 @@ let is_identity (metasenv, context, ugraph) = function
 
 
 let term_of_equality equality =
-  let _, _, (ty, left, right, _), menv, _ = equality in
+  let _, _, (ty, left, right, _), menv = equality in
   let eq i = function Cic.Meta (j, _) -> i = j | _ -> false in
   let argsno = List.length menv in
   let t =