Some changes towards integration of setoid-rewriting.

[helm.git] / helm / software / components / ng_paramodulation / nCicProof.ml

diff --git a/helm/software/components/ng_paramodulation/nCicProof.ml b/helm/software/components/ng_paramodulation/nCicProof.ml
index d1f38487c882f4e6f488d498cdce953ed8c52271..0bc4dc2c2dff39664b93537df7fbf0ed8d0018dd 100644 (file)
--- 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
   ;;