Fixed wrong types in proof terms

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

diff --git a/helm/software/components/ng_paramodulation/nCicBlob.ml b/helm/software/components/ng_paramodulation/nCicBlob.ml
index 621b22559a1e75a7338b1898414a73a98c008c9f..1e5e67979fb2f0f7f8b31010898b4343dcf99f61 100644 (file)
--- a/helm/software/components/ng_paramodulation/nCicBlob.ml
+++ b/helm/software/components/ng_paramodulation/nCicBlob.ml
@@ -133,7 +133,7 @@ module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term = struct
      | Terms.Node l -> "(" ^ String.concat " " (List.map ppfot l) ^ ")"
    ;;
 
-   let mk_predicate hole_type amount ft p vl =
+   let mk_predicate hole_type amount ft p1 vl =
     let rec aux t p = 
       match p with
       | [] -> NCic.Rel 1
@@ -143,7 +143,7 @@ module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term = struct
           | Terms.Var _ -> 
                prerr_endline ("term: " ^ ppfot ft);            
                prerr_endline ("path: " ^ String.concat "," 
-                 (List.map string_of_int p));
+                 (List.map string_of_int p1));
                assert false
           | Terms.Node l -> 
               let l = 
@@ -155,7 +155,7 @@ module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term = struct
               in            
               NCic.Appl l
     in
-      NCic.Lambda("x", hole_type, aux ft (List.rev p))
+      NCic.Lambda("x", hole_type, aux ft (List.rev p1))
     ;;
 
   let mk_proof (bag : NCic.term Terms.bag) mp steps =
@@ -182,28 +182,35 @@ module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term = struct
           NCic.Prod ("x"^string_of_int i, NCic.Implicit `Type, t))
        t vl  
     in
+    let get_literal id =
+      let _, lit, vl, proof = Terms.M.find id bag in
+      let lit =match lit with 
+          | Terms.Predicate t -> assert false 
+          | Terms.Equation (l,r,ty,_) -> 
+              Terms.Node [ Terms.Leaf eqP; ty; l; r]
+      in
+       lit, vl, proof
+    in
     let rec aux ongoal seen = function
       | [] -> NCic.Rel 1
       | id :: tl ->
           let amount = List.length seen in
-          let _, lit, vl, proof = Terms.M.find id bag in
-          let lit = 
-            match lit with 
-            | Terms.Predicate t -> assert false 
-            | Terms.Equation (l,r,ty,_) -> 
-                 Terms.Node [ Terms.Leaf eqP; ty; l; r]
-          in
+          let lit,vl,proof = get_literal id in
           if not ongoal && id = mp then
-            (assert (vl = []);  
+            ((*prerr_endline ("Reached meeting point, id=" ^ (string_of_int id));*)
+            assert (vl = []);  
              NCic.LetIn ("clause_" ^ string_of_int id, 
                 extract amount vl lit, 
                 (NCic.Appl [eq_refl;NCic.Implicit `Type;NCic.Implicit `Term]),
                 aux true ((id,([],lit))::seen) (id::tl)))
           else
           match proof with
-          | Terms.Exact _ when tl=[] -> aux ongoal seen tl
+          | Terms.Exact _ when tl=[] ->
+             (* prerr_endline ("Exact (tl=[]) for " ^ (string_of_int id));*)
+             aux ongoal seen tl
           | Terms.Step _ when tl=[] -> assert false
-          | Terms.Exact ft -> 
+          | Terms.Exact ft ->
+             (* prerr_endline ("Exact for " ^ (string_of_int id));*)
                NCic.LetIn ("clause_" ^ string_of_int id, 
                  close_with_forall vl (extract amount vl lit),
                  close_with_lambdas vl (extract amount vl ft),
@@ -211,11 +218,14 @@ module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term = struct
                    ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl)
           | Terms.Step (_, id1, id2, dir, pos, subst) ->
               let id, id1 = if ongoal then id1,id else id,id1 in
+             let lit,vl,_ = get_literal id in
               let proof_of_id id = 
                 let vars = List.rev (vars_of id seen) in
                 let args = List.map (Subst.apply_subst subst) vars in
                 let args = List.map (extract amount vl) args in
-                NCic.Appl (NCic.Rel (List.length vl + position id seen) :: args)
+               let rel_for_id = NCic.Rel (List.length vl + position id seen) in
+                 if args = [] then rel_for_id              
+                  else NCic.Appl (rel_for_id::args)
               in
               let p_id1 = proof_of_id id1 in
               let p_id2 = proof_of_id id2 in
@@ -229,6 +239,15 @@ module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term = struct
                       extract amount vl (Subst.apply_subst subst r)
                   | _ -> assert false
                 in
+                 (*prerr_endline "mk_predicate :";
+                 if ongoal then prerr_endline "ongoal=true"
+                 else prerr_endline "ongoal=false";
+                 prerr_endline ("id=" ^ string_of_int id);
+                 prerr_endline ("id1=" ^ string_of_int id1);
+                 prerr_endline ("id2=" ^ string_of_int id2);
+                 prerr_endline ("Positions :" ^
+                                  (String.concat ", "
+                                     (List.map string_of_int pos)));*)
                 mk_predicate 
                   id2_ty amount (Subst.apply_subst subst id1_ty) pos vl,
                 id2_ty,
@@ -241,7 +260,7 @@ module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term = struct
                   l,r,eq_ind
               in
                NCic.LetIn ("clause_" ^ string_of_int id, 
-                 close_with_forall vl (extract amount vl lit),
+                 (*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