X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_paramodulation%2FnCicParamod.ml;h=1827d80981889d0fdc181b0fad3eb646a422ef19;hb=74c6905907b0bca229366d52450e2a6982b5b8be;hp=16ae66e5da45f76259420625ebd2311247899987;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/components/ng_paramodulation/nCicParamod.ml b/matita/components/ng_paramodulation/nCicParamod.ml
index 16ae66e5d..1827d8098 100644
--- a/matita/components/ng_paramodulation/nCicParamod.ml
+++ b/matita/components/ng_paramodulation/nCicParamod.ml
@@ -16,8 +16,9 @@ NCicBlob.set_default_eqP()
 NCicProof.set_default_sig()
 ;;
 
-let debug _ = ();;
+let noprint _ = ();;
 let print s = prerr_endline (Lazy.force s);; 
+let debug = noprint;; 
 
 module B(C : NCicBlob.NCicContext): Orderings.Blob 
   with type t = NCic.term and type input = NCic.term 
@@ -25,14 +26,14 @@ module B(C : NCicBlob.NCicContext): Orderings.Blob
 
 module NCicParamod(C : NCicBlob.NCicContext) = Paramod.Paramod(B(C))
 
-let readback ?(demod=false) rdb metasenv subst context (bag,i,fo_subst,l) =
+let readback status ?(demod=false) metasenv subst context (bag,i,fo_subst,l) =
 (*
   List.iter (fun x ->
      print_endline (Pp.pp_unit_clause ~margin:max_int
      (fst(Terms.M.find x bag)))) l; 
 *)
   (* let stamp = Unix.gettimeofday () in *)
-  let proofterm,prooftype = NCicProof.mk_proof ~demod bag i fo_subst l in
+  let proofterm,prooftype = NCicProof.mk_proof status ~demod bag i fo_subst l in
   (* debug (lazy (Printf.sprintf "Got proof term in %fs"
 		     (Unix.gettimeofday() -. stamp))); *)
 (*
@@ -49,12 +50,12 @@ let readback ?(demod=false) rdb metasenv subst context (bag,i,fo_subst,l) =
     in
       aux 0 metasenv proofterm
   in *)
-  debug (lazy (NCicPp.ppterm ~metasenv ~subst ~context proofterm));
+  debug (lazy (status#ppterm ~metasenv ~subst ~context proofterm));
 (*
   let stamp = Unix.gettimeofday () in
   let metasenv, subst, proofterm, _prooftype = 
     NCicRefiner.typeof 
-      (rdb#set_coerc_db NCicCoercion.empty_db) 
+      (status#set_coerc_db NCicCoercion.empty_db) 
       metasenv subst context proofterm None
   in
     print (lazy (Printf.sprintf "Refined in %fs"
@@ -62,7 +63,7 @@ let readback ?(demod=false) rdb metasenv subst context (bag,i,fo_subst,l) =
 *)
     proofterm, prooftype, metasenv, subst
 
-let nparamod rdb metasenv subst context t table =
+let nparamod status metasenv subst context t table =
   let module C =
     struct 
       let metasenv = metasenv
@@ -86,7 +87,7 @@ let nparamod rdb metasenv subst context t table =
   with 
   | P.Error _ | P.GaveUp | P.Timeout _ -> []
   | P.Unsatisfiable solutions -> 
-      List.map (readback rdb metasenv subst context) solutions
+      List.map (readback status metasenv subst context) solutions
 ;;
   
 module EmptyC = 
@@ -102,39 +103,82 @@ module P = NCicParamod(EmptyC)
 type state = P.state
 let empty_state = P.empty_state
 
-let forward_infer_step s t ty =
+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.Node (Terms.Var _::_)), _, (Terms.Incomparable | Terms.Invertible) -> true
+       | _, (Terms.Var _ | Terms.Node (Terms.Var _::_)),(Terms.Incomparable | Terms.Invertible) -> true
+       | _ -> false)
+    | _ -> false
+;;  
+
+let forward_infer_step0 status metasenv subst context s t ty =
   let bag = P.bag_of_state s in
+  let not_embed =
+    let sty,_,_ = 
+      NCicMetaSubst.saturate status ~delta:0  metasenv subst context ty 0 in
+      not_embeddable status subst context sty in
+  if not_embed then (debug (lazy "theorem not embeddable"); s,None)
+  else
   let bag,clause = P.mk_passive bag (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,None)
+      else
+       P.forward_infer_step (P.replace_bag s bag) clause 0, Some clause
+    else (debug (lazy "not eq"); s,None)
 ;;
 
-let index_obj s uri =
-  let obj = NCicEnvironment.get_checked_obj uri in
+let forward_infer_step status metasenv subst context s t ty =
+ fst (forward_infer_step0 status metasenv subst context s t ty)
+;;
+
+let index_obj status s uri =
+  let obj = NCicEnvironment.get_checked_obj status uri in
   debug (lazy ("indexing : " ^ (NUri.string_of_uri uri)));
   debug (lazy ("no : " ^ (string_of_int (fst (Obj.magic 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_step0 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
-    | _ -> s
+	forward_infer_step0 status [] [] [] s (NCic.Const nref) ty
+    | _ -> s,None
 ;;
 
-let demod rdb metasenv subst context s goal =
+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 _ -> []
     | P.Unsatisfiable solutions -> 
       (* print (lazy (Printf.sprintf "Got solutions in %fs"
 		     (Unix.gettimeofday() -. stamp))); *)
-      List.map (readback ~demod:true rdb metasenv subst context) solutions
+      List.map (readback ~demod:true status metasenv subst context) solutions
 ;;
 
-let paramod rdb metasenv subst context s goal =
+let paramod status metasenv subst context s goal =
+  if not_embeddable status subst context (snd goal) then [] else
   (* let stamp = Unix.gettimeofday () in *)
   match P.nparamod ~useage:true ~max_steps:max_int 
     ~timeout:(Unix.gettimeofday () +. 300.0) s goal with
@@ -142,37 +186,37 @@ let paramod rdb metasenv subst context s goal =
   | P.Unsatisfiable solutions -> 
       (* print (lazy (Printf.sprintf "Got solutions in %fs"
 		     (Unix.gettimeofday() -. stamp))); *)
-      List.map (readback rdb metasenv subst context) solutions
+      List.map (readback status metasenv subst context) solutions
 ;;
 
-let fast_eq_check rdb 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 _ -> []
   | P.Unsatisfiable solutions -> 
       (* print (lazy (Printf.sprintf "Got solutions in %fs"
 		     (Unix.gettimeofday() -. stamp))); *)
-      List.map (readback rdb metasenv subst context) solutions
+      List.map (readback status metasenv subst context) solutions
 ;;
 
-let is_equation metasenv subst context ty =
+let is_equation status metasenv subst context ty =
   let hty, _, _ = 
-    NCicMetaSubst.saturate ~delta:0 metasenv subst context
+    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 ::_) when eq = CB.eqP -> true
     | _ -> false
 ;;
 
-
 (*
-let demodulate rdb metasenv subst context s goal =
+let demodulate status metasenv subst context s goal =
   (* let stamp = Unix.gettimeofday () in *)
   match P.fast_eq_check s goal with
   | P.Error _ | P.GaveUp | P.Timeout _ -> []
   | P.Unsatisfiable solutions -> 
       (* print (lazy (Printf.sprintf "Got solutions in %fs"
 		     (Unix.gettimeofday() -. stamp))); *)
-      List.map (readback rdb metasenv subst context) solutions
+      List.map (readback status metasenv subst context) solutions
 ;;
 *)