Filtering all equations that cannot be embedded (containing metas in the blob).

[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 5906bc06d3989b27c629a8ef4bbf8a952ec85313..ef78de2550fe27d69aa5c196756ede2cbd14a632 100644 (file)
--- a/matitaB/components/ng_paramodulation/nCicParamod.ml
+++ b/matitaB/components/ng_paramodulation/nCicParamod.ml
@@ -94,14 +94,46 @@ let empty_state = P.empty_state
 
 let size_of_state = P.size_of_state
 
+exception NotEmbeddable 
+
+let not_embeddable status subst context ty =
+  let rec aux = function
+    | NCic.Meta _
+    | NCic.Const _
+    | NCic.Rel _
+    | NCic.Sort _ -> ()
+    | NCic.Appl l -> List.iter aux l
+    | t -> 
+        (* cannot embed a blob term containing metas *)
+        if (NCicUntrusted.metas_of_term status subst context t = [])
+        then () 
+        else raise NotEmbeddable
+  in 
+  try aux ty; noprint (lazy ("Embeddable")); false
+  with NotEmbeddable -> debug (lazy ("Not embeddable")); true
+;;
+
+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
+  if not_embeddable status subst context ty 
+    then (debug (lazy ("theorem not embeddable")); s)
+  else
   let bag,clause = P.mk_passive bag (saturate (t,ty)) in
     if Terms.is_eq_clause clause then
-      ((*prerr_endline "is eq";*)
-      P.forward_infer_step (P.replace_bag s bag) clause 0)
+      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)
 ;;
 
@@ -120,6 +152,7 @@ let index_obj status s uri =
 ;;
 
 let demod status metasenv subst context s goal =
+  if not_embeddable status subst context (snd goal) then [] else
   (* let stamp = Unix.gettimeofday () in *)
   match P.demod s goal with
     | P.Error _ | P.GaveUp | P.Timeout _ -> []
@@ -131,6 +164,7 @@ let demod status metasenv subst context s goal =
 
 let paramod status metasenv subst context s goal =
   (* let stamp = Unix.gettimeofday () in *)
+  if not_embeddable status subst context (snd goal) then [] else
   match P.nparamod ~useage:true ~max_steps:max_int 
     ~timeout:(Unix.gettimeofday () +. 300.0) s goal with
   | P.Error _ | P.GaveUp | P.Timeout _ -> []
@@ -141,6 +175,7 @@ let paramod status metasenv subst context s goal =
 ;;
 
 let fast_eq_check status metasenv subst context s goal =
+  if not_embeddable status subst context (snd goal) then [] else
   (* let stamp = Unix.gettimeofday () in *)
   match P.fast_eq_check s goal with
   | P.Error _ | P.GaveUp | P.Timeout _ -> []