X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fequality.ml;h=2be5da0627d07d7c390ba622ea4d692ab6751c40;hb=e8f64678cc425f19336ff4f905f9b2f00acd6627;hp=1708ed5b8e2d382ee10410c064c6af0b5c092dbf;hpb=0e6ba9d1134a3bfe9fd4d5b4495faf0811a216df;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml
index 1708ed5b8..2be5da062 100644
--- a/helm/software/components/tactics/paramodulation/equality.ml
+++ b/helm/software/components/tactics/paramodulation/equality.ml
@@ -89,7 +89,7 @@ let string_of_equality ?env eq =
               id w (CicPp.ppterm ty)
               (CicPp.ppterm left) 
               (Utils.string_of_comparison o) (CicPp.ppterm right)
-	(String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m))
+        (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m))
   | Some (_, context, _) -> 
       let names = Utils.names_of_context context in
       let w, _, (ty, left, right, o), m , id = open_equality eq in
@@ -97,7 +97,7 @@ let string_of_equality ?env eq =
               id w (CicPp.pp ty names)
               (CicPp.pp left names) (Utils.string_of_comparison o)
               (CicPp.pp right names)
-	(String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m))
+        (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m))
 ;;
 
 let compare (_,_,_,s1,_,_) (_,_,_,s2,_,_) =
@@ -223,7 +223,7 @@ let open_eq_ind args =
 
 let open_pred pred =
   match pred with 
-  | Cic.Lambda (_,ty,(Cic.Appl [Cic.MutInd (uri, 0,_);_;l;r])) 
+  | Cic.Lambda (_,_,(Cic.Appl [Cic.MutInd (uri, 0,_);ty;l;r])) 
      when LibraryObjects.is_eq_URI uri -> ty,uri,l,r
   | _ -> prerr_endline (CicPp.ppterm pred); assert false   
 ;;
@@ -305,12 +305,12 @@ let ty_of_lambda = function
 
 let compose_contexts ctx1 ctx2 = 
   ProofEngineReduction.replace_lifting 
-    ~equality:(=) ~what:[Cic.Rel 1] ~with_what:[ctx2] ~where:ctx1
+    ~equality:(=) ~what:[Cic.Implicit(Some `Hole)] ~with_what:[ctx2] ~where:ctx1
 ;;
 
 let put_in_ctx ctx t = 
   ProofEngineReduction.replace_lifting
-    ~equality:(=) ~what:[Cic.Rel 1] ~with_what:[t] ~where:ctx
+    ~equality:(=) ~what:[Cic.Implicit (Some `Hole)] ~with_what:[t] ~where:ctx
 ;;
 
 let mk_eq uri ty l r =
@@ -328,22 +328,24 @@ let open_eq = function
 ;;
 
 let contextualize uri ty left right t = 
+  let hole = Cic.Implicit (Some `Hole) in
   (* aux [uri] [ty] [left] [right] [ctx] [t] 
    * 
    * the parameters validate this invariant  
    *   t: eq(uri) ty left right
    * that is used only by the base case
    *
-   * ctx is a term with an open (Rel 1). (Rel 1) is the empty context
+   * ctx is a term with an hole. Cic.Implicit(Some `Hole) is the empty context
+   * ty_ctx is the type of ctx_d
    *)
-    let rec aux uri ty left right ctx_d = function
+    let rec aux uri ty left right ctx_d ctx_ty = function
       | Cic.Appl ((Cic.Const(uri_sym,ens))::tl) 
         when LibraryObjects.is_sym_eq_URI uri_sym  ->
           let ty,l,r,p = open_sym ens tl in
-          mk_sym uri_sym ty l r (aux uri ty l r ctx_d p)
+          mk_sym uri_sym ty l r (aux uri ty l r ctx_d ctx_ty p)
       | Cic.LetIn (name,body,rest) ->
           (* we should go in body *)
-          Cic.LetIn (name,body,aux uri ty left right ctx_d rest)
+          Cic.LetIn (name,body,aux uri ty left right ctx_d ctx_ty rest)
       | Cic.Appl ((Cic.Const(uri_ind,ens))::tl)
         when LibraryObjects.is_eq_ind_URI uri_ind || 
              LibraryObjects.is_eq_ind_r_URI uri_ind ->
@@ -354,12 +356,13 @@ let contextualize uri ty left right t =
           let is_not_fixed_lp = is_not_fixed lp in
           let avoid_eq_ind = LibraryObjects.is_eq_ind_URI uri_ind in
           (* extract the context and the fixed term from the predicate *)
-          let m, ctx_c = 
+          let m, ctx_c, ty2 = 
             let m, ctx_c = if is_not_fixed_lp then rp,lp else lp,rp in
             (* they were under a lambda *)
-            let m =  CicSubstitution.subst (Cic.Implicit None) m in
-            let ctx_c = CicSubstitution.subst (Cic.Rel 1) ctx_c in
-            m, ctx_c          
+            let m =  CicSubstitution.subst hole m in
+            let ctx_c = CicSubstitution.subst hole ctx_c in
+            let ty2 = CicSubstitution.subst hole ty2 in
+            m, ctx_c, ty2          
           in
           (* create the compound context and put the terms under it *)
           let ctx_dc = compose_contexts ctx_d ctx_c in
@@ -372,17 +375,17 @@ let contextualize uri ty left right t =
           (* now put the proofs in the compound context *)
           let p1 = (* p1: dc_what = d_m *)
             if is_not_fixed_lp then 
-              aux uri ty1 c_what m ctx_d p1 
+              aux uri ty2 c_what m ctx_d ctx_ty p1 
             else
-              mk_sym uri_sym ty d_m dc_what
-                (aux uri ty1 m c_what ctx_d p1)
+              mk_sym uri_sym ctx_ty d_m dc_what
+                (aux uri ty2 m c_what ctx_d ctx_ty p1)
           in
           let p2 = (* p2: dc_other = dc_what *)
             if avoid_eq_ind then
-              mk_sym uri_sym ty dc_what dc_other
-                (aux uri ty1 what other ctx_dc p2)
+              mk_sym uri_sym ctx_ty dc_what dc_other
+                (aux uri ty1 what other ctx_dc ctx_ty p2)
             else
-              aux uri ty1 other what ctx_dc p2
+              aux uri ty1 other what ctx_dc ctx_ty p2
           in
           (* if pred = \x.C[x]=m --> t : C[other]=m --> trans other what m
              if pred = \x.m=C[x] --> t : m=C[other] --> trans m what other *)
@@ -391,36 +394,45 @@ let contextualize uri ty left right t =
               dc_other,dc_what,d_m,p2,p1
             else
               d_m,dc_what,dc_other,
-                (mk_sym uri_sym ty dc_what d_m p1),
-                (mk_sym uri_sym ty dc_other dc_what p2)
+                (mk_sym uri_sym ctx_ty dc_what d_m p1),
+                (mk_sym uri_sym ctx_ty dc_other dc_what p2)
           in
-          mk_trans uri_trans ty a b c paeqb pbeqc
+          mk_trans uri_trans ctx_ty a b c paeqb pbeqc
+    | t when ctx_d = hole -> t 
     | t -> 
         let uri_sym = LibraryObjects.sym_eq_URI ~eq:uri in
         let uri_ind = LibraryObjects.eq_ind_URI ~eq:uri in
         let pred = 
           (* ctx_d will go under a lambda, but put_in_ctx substitutes Rel 1 *)
-          let ctx_d = CicSubstitution.lift_from 2 1 ctx_d in (* bleah *)
-          let r = put_in_ctx ctx_d (CicSubstitution.lift 1 left) in
-          let l = ctx_d in
-          let lty = CicSubstitution.lift 1 ty in 
+          let r = CicSubstitution.lift 1 (put_in_ctx ctx_d left) in
+          let l = 
+            let ctx_d = CicSubstitution.lift 1 ctx_d in
+            put_in_ctx ctx_d (Cic.Rel 1)
+          in
+          let lty = CicSubstitution.lift 1 ctx_ty in 
           Cic.Lambda (Cic.Name "foo",ty,(mk_eq uri lty l r))
         in
         let d_left = put_in_ctx ctx_d left in
         let d_right = put_in_ctx ctx_d right in
-        let refl_eq = mk_refl uri ty d_left in
-        mk_sym uri_sym ty d_right d_left
+        let refl_eq = mk_refl uri ctx_ty d_left in
+        mk_sym uri_sym ctx_ty d_right d_left
           (mk_eq_ind uri_ind ty left pred refl_eq right t)
   in
-  let empty_context = Cic.Rel 1 in
-  aux uri ty left right empty_context t
+  aux uri ty left right hole ty t
 ;;
 
 let contextualize_rewrites t ty = 
   let eq,ty,l,r = open_eq ty in
   contextualize eq ty l r t
 ;;
-  
+
+let add_subst subst =
+  function
+    | Exact t -> Exact (Subst.apply_subst subst t)
+    | Step (s,(rule, id1, (pos,id2), pred)) -> 
+	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 p1 = Subst.apply_subst_lift lift subst p1 in
   let p2 = Subst.apply_subst_lift lift subst p2 in
@@ -522,12 +534,12 @@ let string_of_id names id =
     | Exact t -> 
         Printf.sprintf "%d = %s: %s = %s [%s]" id
           (CicPp.pp t names) (CicPp.pp l names) (CicPp.pp r names)
-	(String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m))
+        (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m))
     | Step (_,(step,id1, (_,id2), _) ) ->
         Printf.sprintf "%6d: %s %6d %6d   %s = %s [%s]" id
           (string_of_rule step)
           id1 id2 (CicPp.pp l names) (CicPp.pp r names)
-	(String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m))
+        (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m))
   with
       Not_found -> assert false
 
@@ -549,6 +561,54 @@ let pp_proof names goalproof proof subst id initial_goal =
   "\nand then subsumed by " ^ string_of_int id ^ " when " ^ Subst.ppsubst subst
 ;;
 
+module OT = 
+  struct
+    type t = int
+    let compare = Pervasives.compare
+  end
+
+module M = Map.Make(OT)
+
+let rec find_deps m i = 
+  if M.mem i m then m
+  else 
+    let p,_,_ = proof_of_id i in
+    match p with
+    | Exact _ -> M.add i [] m
+    | 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
+;;
+
+let topological_sort l = 
+  (* build the partial order relation *)
+  let m = 
+    List.fold_left (fun m i -> find_deps m i)
+    M.empty l
+  in
+  let m = M.map (fun x -> Some x) m in
+  (* utils *)
+  let keys m = M.fold (fun i _ acc -> i::acc) m [] in
+  let split l m = List.filter (fun i -> M.find i m = Some []) l in
+  let purge l m = 
+    M.mapi 
+      (fun k v -> if List.mem k l then None else 
+         match v with
+         | None -> None
+         | Some ll -> Some (List.filter (fun i -> not (List.mem i l)) ll)) 
+      m
+  in
+  let rec aux m = 
+      let keys = keys m in
+      let ok = split keys m in
+      let m = purge ok m in
+      ok @ (if ok = [] then [] else aux m)
+  in
+  aux m
+;;
+  
+
 (* returns the list of ids that should be factorized *)
 let get_duplicate_step_in_wfo l p =
   let ol = List.rev l in
@@ -556,39 +616,33 @@ let get_duplicate_step_in_wfo l p =
   (* NOTE: here the n parameter is an approximation of the dependency 
      between equations. To do things seriously we should maintain a 
      dependency graph. This approximation is not perfect. *)
-  let add i n = 
+  let add i = 
     let p,_,_ = proof_of_id i in 
     match p with 
     | Exact _ -> true
     | _ -> 
         try 
-          let (pos,no) = Hashtbl.find h i in
-          Hashtbl.replace h i (pos,no+1);
+          let no = Hashtbl.find h i in
+          Hashtbl.replace h i (no+1);
           false
-        with Not_found -> Hashtbl.add h i (n,1);true
+        with Not_found -> Hashtbl.add h i 1;true
   in
-  let rec aux n = function
-    | Exact _ -> n
+  let rec aux = function
+    | Exact _ -> ()
     | Step (_,(_,i1,(_,i2),_)) -> 
-	let go_on_1 = add i1 n in
-	let go_on_2 = add i2 n in
-        max 
-         (if go_on_1 then aux (n+1) (let p,_,_ = proof_of_id i1 in p) else n+1)
-         (if go_on_2 then aux (n+1) (let p,_,_ = proof_of_id i2 in p) else n+1)
-  in
-  let i = aux 0 p in 
-  let _ = 
-    List.fold_left 
-      (fun acc (_,_,id,_,_) -> aux acc (let p,_,_ = proof_of_id id in p))
-      i ol
-  in
+        let go_on_1 = add i1 in
+        let go_on_2 = add i2 in
+        if go_on_1 then aux (let p,_,_ = proof_of_id i1 in p);
+        if go_on_2 then aux (let p,_,_ = proof_of_id i2 in p)
+  in
+  aux p;
+  List.iter
+    (fun (_,_,id,_,_) -> aux (let p,_,_ = proof_of_id id in p))
+    ol;
   (* now h is complete *)
-  let proofs = Hashtbl.fold (fun k (pos,count) acc->(k,pos,count)::acc) h [] in
-  let proofs = List.filter (fun (_,_,c) -> c > 1) proofs in
-  let proofs = 
-    List.sort (fun (_,c1,_) (_,c2,_) -> Pervasives.compare c2 c1) proofs 
-  in
-  List.map (fun (i,_,_) -> i) proofs
+  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 build_proof_term h lift proof =
@@ -613,11 +667,11 @@ let build_proof_term h lift proof =
            | _ -> assert false
          in
          let p =   build_proof_step 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);
-	   assert cond;*)
-	   p
+(*         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);
+           assert cond;*)
+           p
   in
    aux proof
 ;;
@@ -678,13 +732,14 @@ let build_goal_proof l initial ty se =
           cic, p))
     lets (letsno-1,initial)
   in
-  (*canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty))*)proof, se
+   canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty)),
+   se 
 ;;
 
 let refl_proof ty term = 
   Cic.Appl 
     [Cic.MutConstruct 
-       (LibraryObjects.eq_URI (), 0, 1, []);
+       (Utils.eq_URI (), 0, 1, []);
        ty; term]
 ;;
 
@@ -711,9 +766,10 @@ let relocate newmeta menv to_be_relocated =
 let fix_metas newmeta eq = 
   let w, p, (ty, left, right, o), menv,_ = open_equality eq in
   let to_be_relocated = 
+(* List.map (fun i ,_,_ -> i) menv *)
     HExtlib.list_uniq 
       (List.sort Pervasives.compare 
-	 (Utils.metas_of_term left @ Utils.metas_of_term right)) 
+         (Utils.metas_of_term left @ Utils.metas_of_term right)) 
   in
   let subst, metasenv, newmeta = relocate newmeta menv to_be_relocated in
   let ty = Subst.apply_subst subst ty in
@@ -735,6 +791,7 @@ let meta_convertibility_aux table t1 t2 =
   let rec aux ((table_l, table_r) as table) t1 t2 =
     match t1, t2 with
     | C.Meta (m1, tl1), C.Meta (m2, tl2) ->
+        let tl1, tl2 = [],[] in
         let m1_binding, table_l =
           try List.assoc m1 table_l, table_l
           with Not_found -> m2, (m1, m2)::table_l
@@ -858,14 +915,14 @@ let meta_convertibility t1 t2 =
 exception TermIsNotAnEquality;;
 
 let term_is_equality term =
-  let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in
+  let iseq uri = UriManager.eq uri (Utils.eq_URI ()) in
   match term with
   | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _] when iseq uri -> true
   | _ -> false
 ;;
 
 let equality_of_term proof term =
-  let eq_uri = LibraryObjects.eq_URI () in
+  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 ->
@@ -897,7 +954,7 @@ let term_of_equality equality =
   let argsno = List.length menv in
   let t =
     CicSubstitution.lift argsno
-      (Cic.Appl [Cic.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right])
+      (Cic.Appl [Cic.MutInd (Utils.eq_URI (), 0, []); ty; left; right])
   in
   snd (
     List.fold_right