Final subst returned by superposition and passed around.

[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 59d7e95ff65f824b0e70b968aa4b16d1ecbb9aec..65c0b16138f3d5880006cb848e3f77a45b85f73d 100644 (file)
--- a/helm/software/components/ng_paramodulation/nCicProof.ml
+++ b/helm/software/components/ng_paramodulation/nCicProof.ml
@@ -14,9 +14,8 @@
 type eq_sig_type = Eq | EqInd_l | EqInd_r | Refl
 
 let eqsig = ref (fun _ -> assert false);;
-let set_sig f = eqsig:= 
-f;;
-
+let set_sig f = eqsig:= f;;
+let get_sig = fun x -> !eqsig x;;
 
 let default_sig = function
   | Eq -> 
@@ -66,12 +65,13 @@ let set_reference_of_oxuri reference_of_oxuri =
   in eqsig:= nsig
   ;;
 
-let debug c r = prerr_endline r; c 
+(* let debug c r = prerr_endline r; c *)
+let debug c _ = c;;
 
-  let eqP() = prerr_endline "1"; prerr_endline "1"; debug (!eqsig Eq) "eqp"  ;;
-  let eq_ind() = prerr_endline "2"; debug (!eqsig EqInd_l) "eq_ind" ;;
-  let eq_ind_r() = prerr_endline "3"; debug (!eqsig EqInd_r) "eq_ind_r";; 
-  let eq_refl() = prerr_endline "4"; debug (!eqsig Refl) "refl";;
+  let eqP() = debug (!eqsig Eq) "eqp"  ;;
+  let eq_ind() = debug (!eqsig EqInd_l) "eq_ind" ;;
+  let eq_ind_r() = debug (!eqsig EqInd_r) "eq_ind_r";; 
+  let eq_refl() = debug (!eqsig Refl) "refl";;
 
 
   let extract lift vl t =
@@ -122,7 +122,7 @@ let debug c r = prerr_endline r; c
       NCic.Lambda("x", hole_type, aux ft (List.rev p1))
     ;;
 
-  let mk_proof (bag : NCic.term Terms.bag) mp steps =
+  let mk_proof (bag : NCic.term Terms.bag) mp subst steps =
     let module Subst = FoSubst in
     let position i l = 
       let rec aux = function
@@ -155,16 +155,22 @@ let debug c r = prerr_endline r; c
       in
        lit, vl, proof
     in
+    let mk_refl = function
+      | NCic.Appl [_; ty; l; _]
+         -> NCic.Appl [eq_refl();ty;l]
+      | _ -> assert false
+    in  
     let rec aux ongoal seen = function
       | [] -> NCic.Rel 1
       | id :: tl ->
           let amount = List.length seen in
           let lit,vl,proof = get_literal id in
           if not ongoal && id = mp then
+           let lit = Subst.apply_subst subst lit in
+            let eq_ty = extract amount [] lit in
+           let refl = mk_refl eq_ty in
             ((*prerr_endline ("Reached m point, id=" ^ (string_of_int id));*)
-             NCic.LetIn ("clause_" ^ string_of_int id, 
-                extract amount [] lit, 
-                (NCic.Appl [eq_refl();NCic.Implicit `Type;NCic.Implicit `Term]),
+             NCic.LetIn ("clause_" ^ string_of_int id, eq_ty, refl,
                 aux true ((id,([],lit))::seen) (id::tl)))
           else
           match proof with