Assert false is no longer true due to tooflex filtering.

[helm.git] / matitaB / components / ng_paramodulation / nCicParamod.ml

diff --git a/matitaB/components/ng_paramodulation/nCicParamod.ml b/matitaB/components/ng_paramodulation/nCicParamod.ml
index 0f92c66209f08838469c5ded84e0284ad56b1005..67eca9fce3ed0eab1a7e6eddb3b25b1c88fdee2a 100644 (file)
--- a/matitaB/components/ng_paramodulation/nCicParamod.ml
+++ b/matitaB/components/ng_paramodulation/nCicParamod.ml
@@ -92,14 +92,27 @@ module P = NCicParamod
 type state = P.state
 let empty_state = P.empty_state
 
+let size_of_state = P.size_of_state
+
+let tooflex (_,l,_,_) =
+  match l with
+    | Terms.Equation (l,r,_,o) ->
+      (match l,r,o with
+       | Terms.Var _, _, (Terms.Incomparable | Terms.Invertible) -> true
+       | _, Terms.Var _,(Terms.Incomparable | Terms.Invertible) -> true
+       | _ -> false)
+    | _ -> false
+;;  
+
 let forward_infer_step status metasenv subst context s t ty =
   let bag = P.bag_of_state s in
   let saturate (t,ty) = 
     NCicBlob.saturate status metasenv subst context t ty in
-  let bag,clause = P.mk_passive bag (t,ty) in
+  let bag,clause = P.mk_passive bag (saturate (t,ty)) in
     if Terms.is_eq_clause clause then
-      P.forward_infer_step (P.replace_bag s bag) clause 0
-    else (debug (lazy "not eq"); s)
+      if tooflex clause then (debug (lazy "pruning tooflex"); s)
+      else P.forward_infer_step (P.replace_bag s bag) clause 0
+    else ((*print (lazy "not eq");*) s)
 ;;
 
 let index_obj status s uri =
@@ -152,7 +165,7 @@ let is_equation status metasenv subst context ty =
     NCicMetaSubst.saturate status ~delta:0 metasenv subst context
       ty 0 
   in match hty with
-    | NCic.Appl (eq ::tl) when eq = CB.eqP -> true
+    | NCic.Appl (eq ::tl) when eq = CB.eqP() -> true
     | _ -> false
 ;;