From 4d8413d41d4dc81b9cc12f22de2624938aa7f643 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 21 Nov 2011 11:57:28 +0000
Subject: [PATCH] Filtering all equations that cannot be embedded (containing
 metas in the blob).

---
 .../ng_paramodulation/nCicParamod.ml          | 25 +++++++++++++++++++
 1 file changed, 25 insertions(+)

diff --git a/matitaB/components/ng_paramodulation/nCicParamod.ml b/matitaB/components/ng_paramodulation/nCicParamod.ml
index 67eca9fce..ef78de255 100644
--- a/matitaB/components/ng_paramodulation/nCicParamod.ml
+++ b/matitaB/components/ng_paramodulation/nCicParamod.ml
@@ -94,6 +94,25 @@ 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) ->
@@ -108,6 +127,9 @@ 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
       if tooflex clause then (debug (lazy "pruning tooflex"); s)
@@ -130,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 _ -> []
@@ -141,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 _ -> []
@@ -151,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 _ -> []
-- 
2.39.2