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 6e91b902830a166b7963b3d21aced7f1664e421f..ef78de2550fe27d69aa5c196756ede2cbd14a632 100644 (file)
--- a/matitaB/components/ng_paramodulation/nCicParamod.ml
+++ b/matitaB/components/ng_paramodulation/nCicParamod.ml
@@ -20,11 +20,11 @@ let noprint _ = ();;
 let print s = prerr_endline (Lazy.force s);; 
 let debug = noprint;; 
 
-module B(C : NCicBlob.NCicContext): Orderings.Blob 
+module B : Orderings.Blob 
   with type t = NCic.term and type input = NCic.term 
-  = Orderings.LPO(NCicBlob.NCicBlob(C))
+  = Orderings.LPO(NCicBlob.NCicBlob)
 
-module NCicParamod(C : NCicBlob.NCicContext) = Paramod.Paramod(B(C))
+module NCicParamod = Paramod.Paramod(B)
 
 let readback status ?(demod=false) metasenv subst context (bag,i,fo_subst,l) =
 (*
@@ -64,22 +64,18 @@ let readback status ?(demod=false) metasenv subst context (bag,i,fo_subst,l) =
     proofterm, prooftype, metasenv, subst
 
 let nparamod status metasenv subst context t table =
-  let module C =
-    struct 
-      let metasenv = metasenv
-      let subst = subst
-      let context = context 
-    end 
-  in
-  let module B = B(C) in
-  let module P = NCicParamod(C) in
+  let module P = NCicParamod in
   let module Pp = Pp.Pp(B) in
   let bag, maxvar = Terms.empty_bag, 0 in
+  let saturate (t,ty) = 
+    NCicBlob.saturate status metasenv subst context t ty in
   let (bag,maxvar), goals = 
-    HExtlib.list_mapi_acc (fun x _ a -> P.mk_goal a x) (bag,maxvar) [t]
+    HExtlib.list_mapi_acc 
+      (fun x _ a -> P.mk_goal a (saturate x)) (bag,maxvar) [t]
   in
-  let (bag,maxvar), passives = 
-    HExtlib.list_mapi_acc (fun x _ a -> P.mk_passive a x) (bag,maxvar) table
+  let (bag,maxvar), passives =
+    HExtlib.list_mapi_acc 
+      (fun x _ a -> P.mk_passive a (saturate x))  (bag,maxvar) table
   in
   match 
     P.paramod ~useage:true ~max_steps:max_int ~timeout:(Unix.gettimeofday () +. 300.0) 
@@ -90,25 +86,55 @@ let nparamod status metasenv subst context t table =
       List.map (readback status metasenv subst context) solutions
 ;;
   
-module EmptyC = 
-  struct
-    let metasenv = []
-    let subst = []
-    let context = []
-  end
-
-module CB = NCicBlob.NCicBlob(EmptyC)
-module P = NCicParamod(EmptyC)
+module CB = NCicBlob.NCicBlob
+module P = NCicParamod
 
 type state = P.state
 let empty_state = P.empty_state
 
-let forward_infer_step s t ty =
+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 bag,clause = P.mk_passive bag (t,ty) 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
-      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 =
@@ -118,14 +144,15 @@ let index_obj status s uri =
   match obj with
     | (_,_,[],[],NCic.Constant(_,_,None,ty,_)) ->
         let nref = NReference.reference_of_spec uri NReference.Decl in
-       forward_infer_step s (NCic.Const nref) ty
+       forward_infer_step status [] [] [] s (NCic.Const nref) ty
     | (_,d,[],[],NCic.Constant(_,_,Some(_),ty,_)) ->
         let nref = NReference.reference_of_spec uri (NReference.Def d) in
-       forward_infer_step s (NCic.Const nref) ty
+       forward_infer_step status [] [] [] s (NCic.Const nref) ty
     | _ -> s
 ;;
 
 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 _ -> []
@@ -137,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 _ -> []
@@ -147,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 _ -> []
@@ -161,7 +190,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
 ;;