X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2FnCicBlob.ml;h=2ed7eef23b005efff510e2daa6a9619f9ea67d84;hb=8e4367191fdfd125596658e35d4b99cd3047a5bc;hp=dcc2aba30310678b83bfcf10b3504f9158554213;hpb=a200ab05cafa2e2b1075d04235042ee8e99f046e;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/nCicBlob.ml b/helm/software/components/ng_paramodulation/nCicBlob.ml
index dcc2aba30..2ed7eef23 100644
--- a/helm/software/components/ng_paramodulation/nCicBlob.ml
+++ b/helm/software/components/ng_paramodulation/nCicBlob.ml
@@ -18,7 +18,8 @@ module type NCicContext =
     val context : NCic.context
   end
 
-module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term = struct
+module NCicBlob(C : NCicContext) : Terms.Blob 
+with type t = NCic.term and type input = NCic.term = struct
 
   type t = NCic.term
 
@@ -47,6 +48,8 @@ module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term = struct
   let pp t = 
     NCicPp.ppterm ~context:C.context ~metasenv:C.metasenv ~subst:C.subst t;;
 
+  type input = NCic.term
+
   let rec embed = function
     | NCic.Meta (i,_) -> Terms.Var i, [i]
     | NCic.Appl l ->
@@ -84,192 +87,4 @@ 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 eq_refl = 
-    let r = 
-      OCic2NCic.reference_of_oxuri 
-       (UriManager.uri_of_string 
-         "cic:/matita/logic/equality/eq.ind#xpointer(1/1/1)")
-    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 hole_type amount ft p1 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 p1));
-               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", hole_type, aux ft (List.rev p1))
-    ;;
-
-  let mk_proof (bag : NCic.term Terms.bag) mp 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 close_with_forall vl t = 
-      List.fold_left 
-       (fun t i -> 
-          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 = get_literal id in
-          if not ongoal && id = mp then
-            ((*prerr_endline ("Reached m 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=[] ->
-	      (* prerr_endline ("Exact (tl=[]) for " ^ (string_of_int id));*)
-	      aux ongoal seen tl
-          | Terms.Step _ when tl=[] -> assert false
-          | 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),
-                 aux ongoal 
-                   ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl)
-          | Terms.Step (_, id1, id2, dir, pos, subst) ->
-              let id, id1,(lit,vl,proof) =
-		if ongoal then id1,id,get_literal id1
-		else id,id1,(lit,vl,proof)
-	      in
-	      let vl = if ongoal then Subst.filter subst vl else vl 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
-		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
-              let pred, hole_type, l, r = 
-                let id1_ty = ty_of id1 seen in
-                let id2_ty,l,r = 
-                  match ty_of id2 seen with
-                  | Terms.Node [ _; t; l; r ] -> 
-                      extract amount vl (Subst.apply_subst subst t),
-                      extract amount vl (Subst.apply_subst subst l),
-                      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,
-                l,r
-              in
-              let l, r, eq_ind = 
-                if (ongoal=true) = (dir=Terms.Left2Right) then
-                  r,l,eq_ind_r
-                else
-                  l,r,eq_ind
-              in
-               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)
-    in 
-      aux false [] steps
-  ;;
-
  end