X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2FnCicBlob.ml;h=1e5e67979fb2f0f7f8b31010898b4343dcf99f61;hb=c091ca7a030a85a529543de98e45c54284028b63;hp=e01edfae309e30053ea336e3aeee2d35ba658536;hpb=b97a7976503b2d2e5cbc9199f848135a324775a8;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/nCicBlob.ml b/helm/software/components/ng_paramodulation/nCicBlob.ml
index e01edfae3..1e5e67979 100644
--- a/helm/software/components/ng_paramodulation/nCicBlob.ml
+++ b/helm/software/components/ng_paramodulation/nCicBlob.ml
@@ -27,10 +27,22 @@ module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term = struct
   let rec compare x y = 
     match x,y with
     | NCic.Rel i, NCic.Rel j -> i-j
+    | NCic.Meta (i,_), NCic.Meta (j,_) -> i-j
     | NCic.Const r1, NCic.Const r2 -> NReference.compare r1 r2
-    | NCic.Appl l1, NCic.Appl l2 -> assert false (* TODO *)
+    | NCic.Appl l1, NCic.Appl l2 -> FoUtils.lexicograph compare l1 l2
+    | NCic.Rel _, ( NCic.Meta _ | NCic.Const _ | NCic.Appl _ ) -> ~-1
+    | ( NCic.Meta _ | NCic.Const _ | NCic.Appl _ ), NCic.Rel _ -> 1
+    | NCic.Const _, ( NCic.Meta _ | NCic.Appl _ ) -> ~-1
+    | ( NCic.Meta _ | NCic.Appl _ ), NCic.Const _ -> 1
+    | NCic.Appl _, NCic.Meta _ -> ~-1
+    | NCic.Meta _, NCic.Appl _ -> 1
     | _ -> assert false
   ;;
+  
+  let compare x y = 
+    if NCicReduction.alpha_eq C.metasenv C.subst C.context x y then 0 
+    else compare x y
+  ;;
 
   let pp t = 
     NCicPp.ppterm ~context:C.context ~metasenv:C.metasenv ~subst:C.subst t;;
@@ -46,6 +58,215 @@ module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term = struct
 	  (fun (r,v) t -> let r1,v1 = embed t in (r1::r),aux [] v v1) ([],[]) l
 	in (Terms.Node (List.rev res)), vars
     | t -> Terms.Leaf t, []
-;;
+  ;;
+
+  let embed t = fst (embed t) ;;
+
+  let saturate t ty = 
+    let sty, _, args = 
+      NCicMetaSubst.saturate ~delta:max_int C.metasenv C.subst C.context
+        ty 0
+    in
+    let proof = 
+      if args = [] then Terms.Leaf t 
+      else Terms.Node (Terms.Leaf t :: List.map embed args)
+    in
+    let sty = embed sty in
+    proof, sty
+  ;;
+
+  let eqP = 
+    let r = 
+      OCic2NCic.reference_of_oxuri 
+       (UriManager.uri_of_string 
+         "cic:/matita/logic/equality/eq.ind#xpointer(1/1)")
+    in
+    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 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=[] ->
+	      (* 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 = 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
+		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