first proof reconstruction attempt, still bugged since it

[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 09399b3261b2d634352c54cc63b95614b898fb0b..5aded532907f4d9acd6e373b60633314f86d044f 100644 (file)
--- a/helm/software/components/ng_paramodulation/nCicBlob.ml
+++ b/helm/software/components/ng_paramodulation/nCicBlob.ml
@@ -84,5 +84,129 @@ module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term = struct
     NCic.Const r
   ;;
 
+  let eq_ind = 
+    let r = 
+      OCic2NCic.reference_of_oxuri 
+       (UriManager.uri_of_string 
+         "cic:/matita/logic/equality/eq_ind.con")
+    in
+    NCic.Const r
+  ;;
+
+  let eq_ind_r = 
+    let r = 
+      OCic2NCic.reference_of_oxuri 
+       (UriManager.uri_of_string 
+         "cic:/matita/logic/equality/eq_elim_r.con")
+    in
+    NCic.Const r
+  ;;
+
+  let extract lift vl t =
+    let rec pos i = function 
+      | [] -> raise Not_found 
+      | j :: tl when j <> i -> 1+ pos i tl
+      | _ -> 1
+    in
+    let vl_len = List.length vl in
+    let rec extract = function
+      | Terms.Leaf x -> NCicSubstitution.lift (vl_len+lift) x
+      | Terms.Var j -> 
+           (try NCic.Rel (pos j vl) with Not_found -> NCic.Implicit `Term) 
+      | Terms.Node l -> NCic.Appl (List.map extract l)
+    in
+      extract t
+  ;;
+
+   let rec ppfot = function 
+     | Terms.Leaf _ -> "."
+     | Terms.Var i -> "?" ^ string_of_int i
+     | Terms.Node l -> "(" ^ String.concat " " (List.map ppfot l) ^ ")"
+   ;;
+
+   let mk_predicate amount ft p vl =
+    let rec aux t p = 
+      match p with
+      | [] -> NCic.Rel 1
+      | n::tl ->
+          match t with
+          | Terms.Leaf _ 
+          | Terms.Var _ -> 
+               prerr_endline ("term: " ^ ppfot ft);            
+               prerr_endline ("path: " ^ String.concat "," 
+                 (List.map string_of_int p));
+               assert false
+          | Terms.Node l -> 
+              let l = 
+                HExtlib.list_mapi
+                  (fun t i -> 
+                    if i = n then aux t tl 
+                    else extract amount (0::vl) t)
+                  l
+              in            
+              NCic.Appl l
+    in
+      NCic.Lambda("x", NCic.Implicit `Type, aux ft (List.rev p))
+    ;;
+
+  let mk_proof (bag : NCic.term Terms.bag) steps =
+    let module Subst = FoSubst in
+    let position i l = 
+      let rec aux = function
+       | [] -> assert false
+       | (j,_) :: tl when i = j -> 1
+       | _ :: tl -> 1 + aux tl
+      in
+        aux l
+    in
+    let vars_of i l = fst (List.assoc i l) in
+    let ty_of i l = snd (List.assoc i l) in
+    let close_with_lambdas vl t = 
+      List.fold_left 
+       (fun t i -> 
+          NCic.Lambda ("x"^string_of_int i, NCic.Implicit `Type, t))
+       t vl  
+    in
+    let rec aux seen = function
+      | [] -> NCic.Rel 1
+      | id :: tl ->
+(*           prerr_endline ("Let4 : " ^string_of_int id); *)
+          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
+(*                 prerr_endline ("X" ^ ppfot lit); *)
+          match proof with
+          | Terms.Exact ft -> 
+               NCic.LetIn ("clause_" ^ string_of_int id, NCic.Implicit `Type, 
+                 close_with_lambdas vl (extract amount vl ft),
+                 aux ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl)
+          | Terms.Step (_, id1, id2, dir, pos, subst) ->
+              let proof_of_id id = 
+                let vars = 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)
+              in
+              let p_id1 = proof_of_id id1 in
+              let p_id2 = proof_of_id id2 in
+              let pred = 
+                let id1_ty = ty_of id1 seen in
+                mk_predicate amount (Subst.apply_subst subst id1_ty) pos vl
+              in
+              let eq_ind = if dir=Terms.Left2Right then eq_ind else eq_ind_r in
+               NCic.LetIn ("clause_" ^ string_of_int id, NCic.Implicit `Type, 
+                 close_with_lambdas vl
+                   (NCic.Appl [ eq_ind ; NCic.Implicit `Type; 
+                     pred; NCic.Implicit `Term; p_id1; 
+                     NCic.Implicit `Term; p_id2 ]),
+                 aux ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl)
+    in 
+      aux [] steps
+  ;;
 
  end