X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2FnCicProof.ml;h=0bc4dc2c2dff39664b93537df7fbf0ed8d0018dd;hb=e22808c929a9cebf5e4e2b7428ff0cbf89e1f92a;hp=d1f38487c882f4e6f488d498cdce953ed8c52271;hpb=cf01ca6479346febcdf120e483ca9ce89d53e301;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/nCicProof.ml b/helm/software/components/ng_paramodulation/nCicProof.ml
index d1f38487c..0bc4dc2c2 100644
--- a/helm/software/components/ng_paramodulation/nCicProof.ml
+++ b/helm/software/components/ng_paramodulation/nCicProof.ml
@@ -122,6 +122,30 @@ let debug c _ = c;;
       NCic.Lambda("x", hole_type, aux ft (List.rev p1))
     ;;
 
+(*
+   let mk_morphism eq amount ft p1 vl =
+    let rec aux t p = 
+      match p with
+      | [] -> eq
+      | n::tl ->
+          match t with
+          | Terms.Leaf _ 
+          | Terms.Var _ -> assert false
+          | Terms.Node l ->
+              let dag,arity = ____ in
+              let l = 
+                HExtlib.list_rev_mapi_filter
+                  (fun t i ->
+                    if i < arity then None
+                    else if i = n then Some (aux t tl) 
+                    else Some (NCic.Appl [refl ...]))
+                  l
+              in            
+              NCic.Appl (dag::l)
+    in aux ft (List.rev pl)
+    ;;
+*)
+
   let mk_proof (bag : NCic.term Terms.bag) mp subst steps =
     let module Subst = FoSubst in
     let position i l = 
@@ -245,13 +269,22 @@ let debug c _ = c;;
                 else
                   l,r,eq_ind ()
               in
-               NCic.LetIn ("clause_" ^ string_of_int id, 
-                 close_with_forall vl (extract amount vl lit),
+	      let body = aux ongoal 
+                ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl 
+	      in 
+		if NCicUntrusted.count_occurrences [] 0 body <= 1 then
+		  NCicSubstitution.subst 
+		    ~avoid_beta_redexes:true ~no_implicit:false
+                    (close_with_lambdas vl (NCic.Appl 
+		         [ eq_ind ; hole_type; l; pred; p_id1; r; p_id2 ]))
+		    body
+		else
+		  NCic.LetIn ("clause_" ^ string_of_int id, 
+	            close_with_forall vl (extract amount vl lit),
 			   (* NCic.Implicit `Type, *)
-                 close_with_lambdas vl 
-                   (NCic.Appl [ eq_ind ; hole_type; l; pred; p_id1; r; p_id2 ]),
-                 aux ongoal 
-                   ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl)
+                    close_with_lambdas vl (NCic.Appl 
+			 [ eq_ind ; hole_type; l; pred; p_id1; r; p_id2 ]),
+		    body)
     in 
       aux false [] steps, proof_type
   ;;