X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fparamodulation%2Fequality.ml;h=1e9e97ec58f3147733356cfde501a72bdf83da74;hb=ba6b5ca0dfc2e49ac2dbb1b49c29a87844a34f76;hp=2be5da0627d07d7c390ba622ea4d692ab6751c40;hpb=8ced9658902a93c14e5d5b43511e4cbcd90337e0;p=helm.git

diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml
index 2be5da062..1e9e97ec5 100644
--- a/components/tactics/paramodulation/equality.ml
+++ b/components/tactics/paramodulation/equality.ml
@@ -433,7 +433,7 @@ let add_subst subst =
 	Step (Subst.concat subst s,(rule, id1, (pos,id2), pred))
 ;;
 	
-let build_proof_step ?(sym=false) lift subst p1 p2 pos l r pred =
+let build_proof_step eq lift subst p1 p2 pos l r pred =
   let p1 = Subst.apply_subst_lift lift subst p1 in
   let p2 = Subst.apply_subst_lift lift subst p2 in
   let l  = CicSubstitution.lift lift l in
@@ -453,27 +453,17 @@ let build_proof_step ?(sym=false) lift subst p1 p2 pos l r pred =
   let p =
     match pos with
       | Utils.Left ->
-        mk_eq_ind (Utils.eq_ind_URI ()) ty what pred p1 other p2
+        mk_eq_ind (LibraryObjects.eq_ind_URI ~eq) ty what pred p1 other p2
       | Utils.Right ->
-        mk_eq_ind (Utils.eq_ind_r_URI ()) ty what pred p1 other p2
+        mk_eq_ind (LibraryObjects.eq_ind_r_URI ~eq) ty what pred p1 other p2
   in
-  if sym then
-    let uri,pl,pr = 
-      let eq,_,pl,pr = open_eq body in
-      LibraryObjects.sym_eq_URI ~eq, pl, pr
-    in
-    let l = CicSubstitution.subst other pl in
-    let r = CicSubstitution.subst other pr in
-    mk_sym uri ty l r p
-  else
     p
 ;;
 
 let parametrize_proof p l r ty = 
-  let parameters = CicUtil.metas_of_term p 
-@ CicUtil.metas_of_term l 
-@ CicUtil.metas_of_term r
-in (* ?if they are under a lambda? *)
+  let parameters = 
+    CicUtil.metas_of_term p @ CicUtil.metas_of_term l @ CicUtil.metas_of_term r
+  in (* ?if they are under a lambda? *)
   let parameters = 
     HExtlib.list_uniq (List.sort Pervasives.compare parameters) 
   in
@@ -578,7 +568,10 @@ let rec find_deps m i =
     | Step (_,(_,id1,(_,id2),_)) -> 
         let m = find_deps m id1 in
         let m = find_deps m id2 in
-        M.add i (M.find id1 m @ M.find id2 m @ [id1;id2]) m
+        (* without the uniq there is a stack overflow doing concatenation *)
+        let xxx = [id1;id2] @ M.find id1 m @ M.find id2 m in 
+        let xxx = HExtlib.list_uniq (List.sort Pervasives.compare xxx) in
+        M.add i xxx m
 ;;
 
 let topological_sort l = 
@@ -599,13 +592,14 @@ let topological_sort l =
          | Some ll -> Some (List.filter (fun i -> not (List.mem i l)) ll)) 
       m
   in
-  let rec aux m = 
+  let rec aux m res = 
       let keys = keys m in
       let ok = split keys m in
       let m = purge ok m in
-      ok @ (if ok = [] then [] else aux m)
+      let res = ok @ res in
+      if ok = [] then res else aux m res
   in
-  aux m
+  aux m []
 ;;
   
 
@@ -642,10 +636,11 @@ let get_duplicate_step_in_wfo l p =
   (* now h is complete *)
   let proofs = Hashtbl.fold (fun k count acc-> (k,count)::acc) h [] in
   let proofs = List.filter (fun (_,c) -> c > 1) proofs in
-  topological_sort (List.map (fun (i,_) -> i) proofs)
+  let res = topological_sort (List.map (fun (i,_) -> i) proofs) in
+  res
 ;;
 
-let build_proof_term h lift proof =
+let build_proof_term eq h lift proof =
   let proof_of_id aux id =
     let p,l,r = proof_of_id id in
     try List.assoc id h,l,r with Not_found -> aux p, l, r
@@ -666,7 +661,7 @@ let build_proof_term h lift proof =
            | Cic.Lambda (_,a,b) -> Cic.Lambda (varname,a,b)
            | _ -> assert false
          in
-         let p =   build_proof_step lift subst p1 p2 pos l r pred in
+         let p =   build_proof_step eq lift subst p1 p2 pos l r pred in
 (*         let cond =  (not (List.mem 302 (Utils.metas_of_term p)) || id1 = 8 || id1 = 132) in
            if not cond then
              prerr_endline ("ERROR " ^ string_of_int id1 ^ " " ^ string_of_int id2);
@@ -676,18 +671,17 @@ let build_proof_term h lift proof =
    aux proof
 ;;
 
-let build_goal_proof l initial ty se =
+let build_goal_proof eq l initial ty se =
   let se = List.map (fun i -> Cic.Meta (i,[])) se in 
   let lets = get_duplicate_step_in_wfo l initial in
   let letsno = List.length lets in
   let _,mty,_,_ = open_eq ty in
-  let lift_list l = List.map (fun (i,t) -> i,CicSubstitution.lift 1 t) l 
-  in
+  let lift_list l = List.map (fun (i,t) -> i,CicSubstitution.lift 1 t) l in
   let lets,_,h = 
     List.fold_left
       (fun (acc,n,h) id -> 
         let p,l,r = proof_of_id id in
-        let cic = build_proof_term h n p in
+        let cic = build_proof_term eq h n p in
         let real_cic,instance = 
           parametrize_proof cic l r (CicSubstitution.lift n mty)
         in
@@ -700,7 +694,7 @@ let build_goal_proof l initial ty se =
       | [] -> current_proof,se
       | (rule,pos,id,subst,pred)::tl ->
           let p,l,r = proof_of_id id in
-           let p = build_proof_term h letsno p in
+           let p = build_proof_term eq h letsno p in
            let pos = if pos = Utils.Left then Utils.Right else Utils.Left in
          let varname = 
            match rule with
@@ -714,13 +708,13 @@ let build_goal_proof l initial ty se =
            | _ -> assert false
          in
            let proof = 
-             build_proof_step letsno subst current_proof p pos l r pred
+             build_proof_step eq letsno subst current_proof p pos l r pred
            in
            let proof,se = aux se proof tl in
            Subst.apply_subst_lift letsno subst proof,
            List.map (fun x -> Subst.apply_subst_lift letsno subst x) se
     in
-    aux se (build_proof_term h letsno initial) l
+    aux se (build_proof_term eq h letsno initial) l
   in
   let n,proof = 
     let initial = proof in
@@ -736,15 +730,20 @@ let build_goal_proof l initial ty se =
    se 
 ;;
 
-let refl_proof ty term = 
-  Cic.Appl 
-    [Cic.MutConstruct 
-       (Utils.eq_URI (), 0, 1, []);
-       ty; term]
+let refl_proof eq_uri ty term = 
+  Cic.Appl [Cic.MutConstruct (eq_uri, 0, 1, []); ty; term]
 ;;
 
 let metas_of_proof p =
-  let p = build_proof_term [] 0 p in
+  let eq = 
+    match LibraryObjects.eq_URI () with
+    | Some u -> u 
+    | None -> 
+        raise 
+          (ProofEngineTypes.Fail 
+            (lazy "No default equality defined when calling metas_of_proof"))
+  in
+  let p = build_proof_term eq [] 0 p in
   Utils.metas_of_term p
 ;;
 
@@ -915,17 +914,16 @@ let meta_convertibility t1 t2 =
 exception TermIsNotAnEquality;;
 
 let term_is_equality term =
-  let iseq uri = UriManager.eq uri (Utils.eq_URI ()) in
   match term with
-  | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _] when iseq uri -> true
+  | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _] 
+    when LibraryObjects.is_eq_URI uri -> true
   | _ -> false
 ;;
 
 let equality_of_term proof term =
-  let eq_uri = Utils.eq_URI () in
-  let iseq uri = UriManager.eq uri eq_uri in
   match term with
-  | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
+  | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] 
+    when LibraryObjects.is_eq_URI uri ->
       let o = !Utils.compare_terms t1 t2 in
       let stat = (ty,t1,t2,o) in
       let w = Utils.compute_equality_weight stat in
@@ -948,13 +946,13 @@ let is_identity (_, context, ugraph) eq =
 ;;
 
 
-let term_of_equality equality =
+let term_of_equality eq_uri equality =
   let _, _, (ty, left, right, _), menv, _= open_equality equality in
   let eq i = function Cic.Meta (j, _) -> i = j | _ -> false in
   let argsno = List.length menv in
   let t =
     CicSubstitution.lift argsno
-      (Cic.Appl [Cic.MutInd (Utils.eq_URI (), 0, []); ty; left; right])
+      (Cic.Appl [Cic.MutInd (eq_uri, 0, []); ty; left; right])
   in
   snd (
     List.fold_right