X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2FnCicBlob.ml;h=c1c7a9071fdee01ed9ad69959782f7e73886ad25;hb=12f96bd48b460d06f9858a334ee7c52d6831712f;hp=5aded532907f4d9acd6e373b60633314f86d044f;hpb=8de1a75899a83dd31e856804bd448c1bd87d9ab3;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/nCicBlob.ml b/helm/software/components/ng_paramodulation/nCicBlob.ml
index 5aded5329..c1c7a9071 100644
--- a/helm/software/components/ng_paramodulation/nCicBlob.ml
+++ b/helm/software/components/ng_paramodulation/nCicBlob.ml
@@ -11,6 +11,40 @@
 
 (* $Id: terms.mli 9822 2009-06-03 15:37:06Z tassi $ *)
 
+let eqPref = ref (fun _ -> assert false);;
+let set_eqP t = eqPref := fun _ -> t;;
+
+let default_eqP() = 
+  let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/eq.ind" in
+  let ref = NReference.reference_of_spec uri (NReference.Ind(true,0,2)) in
+    NCic.Const ref
+;;
+
+let equivalence_relation =
+  let uri = NUri.uri_of_string "cic:/matita/ng/properties/relations/eq_rel.con"
+  in
+  let ref = NReference.reference_of_spec uri (NReference.Fix(0,1,2)) 
+  in NCic.Const ref
+
+let setoid_eq =
+  let uri = NUri.uri_of_string "cic:/matita/ng/sets/setoids/eq.con" in
+  let ref = NReference.reference_of_spec uri (NReference.Fix(0,0,2)) 
+  in NCic.Const ref
+
+let set_default_eqP() = eqPref := default_eqP
+
+let set_reference_of_oxuri f = 
+  let eqnew = function 
+      _ -> 
+	let r = f(UriManager.uri_of_string 
+          "cic:/matita/logic/equality/eq.ind#xpointer(1/1)")
+	in
+	  NCic.Const r
+  in
+    eqPref := eqnew
+;;
+
+
 module type NCicContext =
   sig
     val metasenv : NCic.metasenv
@@ -18,17 +52,32 @@ 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
 
-  let eq x y = NCicReduction.alpha_eq C.metasenv C.subst C.context x y;;
+  let eq x y = x = y;;
+    (* NCicReduction.alpha_eq C.metasenv C.subst C.context x y;; *)
+
+  let height_of_ref = function
+    | NReference.Def h -> h
+    | NReference.Fix(_,_,h) -> h
+    | _ -> 0
+
+  let compare_refs (NReference.Ref (u1,r1)) (NReference.Ref (u2,r2)) =
+    let x = height_of_ref r2 - height_of_ref r1 in
+      if x = 0 then 
+	Hashtbl.hash (NUri.string_of_uri u1,r1) - 
+	  Hashtbl.hash (NUri.string_of_uri u2,r2)
+      else x 
 
   let rec compare x y = 
     match x,y with
-    | NCic.Rel i, NCic.Rel j -> i-j
+    | NCic.Rel i, NCic.Rel j -> j-i
     | NCic.Meta (i,_), NCic.Meta (j,_) -> i-j
-    | NCic.Const r1, NCic.Const r2 -> NReference.compare r1 r2
+    | NCic.Const r1, NCic.Const r2 -> compare_refs r1 r2
+    (*NReference.compare r1 r2*)
     | 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
@@ -36,17 +85,34 @@ module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term = struct
     | ( NCic.Meta _ | NCic.Appl _ ), NCic.Const _ -> 1
     | NCic.Appl _, NCic.Meta _ -> ~-1
     | NCic.Meta _, NCic.Appl _ -> 1
-    | _ -> assert false
+    | _ -> Pervasives.compare x y
+	(* was assert false, but why? *)
+	
   ;;
   
   let compare x y = 
-    if NCicReduction.alpha_eq C.metasenv C.subst C.context x y then 0 
+    (* if NCicReduction.alpha_eq C.metasenv C.subst C.context x y  then 0 *)
+    if x = y  then 0
     else compare x y
   ;;
 
+  let eqP = (!eqPref)()
+  ;;
+
+  let is_eq = function
+    | Terms.Node [ Terms.Leaf eqt ; ty; l; r ] when eq eqP eqt ->
+        Some (ty,l,r) 
+(*
+    | Terms.Node [ Terms.Leaf eqt ; _; Terms.Node [Terms.Leaf eqt2 ; ty]; l; r]
+	when eq equivalence_relation eqt && eq setoid_eq eqt2 ->
+        Some (ty,l,r) *)
+    | _ -> None
+
   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 ->
@@ -64,7 +130,7 @@ module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term = struct
 
   let saturate t ty = 
     let sty, _, args = 
-      NCicMetaSubst.saturate ~delta:max_int C.metasenv C.subst C.context
+      NCicMetaSubst.saturate ~delta:0 C.metasenv C.subst C.context
         ty 0
     in
     let proof = 
@@ -74,139 +140,5 @@ module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term = struct
     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 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