X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fparamodulation%2Fequality.ml;h=7893ecba6142ef4a5934d3edc0fd18db3ec51a14;hb=42f2dc48b4fef5b404f406bf512d6a0cde35c067;hp=7123c134a93a98056655f6cee83e55600b559945;hpb=cae7dd50468e5ba0dec9d3cf4fa14daee2c3da2e;p=helm.git

diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml
index 7123c134a..7893ecba6 100644
--- a/components/tactics/paramodulation/equality.ml
+++ b/components/tactics/paramodulation/equality.ml
@@ -96,8 +96,8 @@ 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
@@ -105,8 +105,8 @@ 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,_,_) =
@@ -202,7 +202,7 @@ let build_ens uri termlist =
   let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
   match obj with
   | Cic.Constant (_, _, _, uris, _) ->
-      assert (List.length uris <= List.length termlist);
+      (* assert (List.length uris <= List.length termlist); *)
       let rec aux = function
         | [], tl -> [], tl
         | (uri::uris), (term::tl) ->
@@ -260,7 +260,7 @@ let open_pred pred =
   match pred with 
   | 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   
+  | _ -> Utils.debug_print (lazy (CicPp.ppterm pred)); assert false   
 ;;
 
 let is_not_fixed t =
@@ -269,6 +269,48 @@ let is_not_fixed t =
 ;;
 
 let canonical t context menv = 
+  let remove_cycles t =
+   let is_transitive =
+    function
+       Cic.Appl (Cic.Const (uri_trans,_)::_)
+        when LibraryObjects.is_trans_eq_URI uri_trans ->
+         true
+     | _ -> false in
+   let rec collect =
+    function
+       Cic.Appl (Cic.Const (uri_trans,ens)::tl)
+        when LibraryObjects.is_trans_eq_URI uri_trans ->
+         let ty,l,m,r,p1,p2 = open_trans ens tl in
+          (if is_transitive p1 then fst (collect p1) else [l,p1]) @
+           (if is_transitive p2 then fst (collect p2) else [m,p2]),
+          (r, uri_trans, ty)
+     | t -> assert false in
+   let rec cut_to_last_duplicate l acc =
+    function
+       [] -> List.rev acc
+     | (l',p)::tl when l=l' -> 
+if acc <> [] then
+Utils.debug_print (lazy ("!!! RISPARMIO " ^ string_of_int (List.length acc) ^ " PASSI"));
+         cut_to_last_duplicate l [l',p] tl
+     | (l',p)::tl ->
+         cut_to_last_duplicate l ((l',p)::acc) tl
+   in
+   let rec rebuild =
+    function
+       (l,_)::_::_ as steps, ((r,uri_trans,ty) as last) ->
+         (match cut_to_last_duplicate l [] steps with
+             (l,p1)::((m,_)::_::_ as tl) ->
+               mk_trans uri_trans ty l m r p1 (rebuild (tl,last))
+           | [l,p1 ; m,p2] -> mk_trans uri_trans ty l m r p1 p2
+           | [l,p1] -> p1
+           | [] -> assert false)
+     | _ -> assert false
+   in
+    if is_transitive t then
+     rebuild (collect t)
+    else
+     t
+  in
   let rec remove_refl t =
     match t with
     | Cic.Appl (((Cic.Const(uri_trans,ens))::tl) as args)
@@ -285,11 +327,18 @@ let canonical t context menv =
         Cic.LetIn (name,remove_refl bo,remove_refl rest)
     | _ -> t
   in
-  let rec canonical context t =
+  let rec canonical_trough_lambda context = function
+    | Cic.Lambda(name,ty,bo) -> 
+        let context' = (Some (name,Cic.Decl ty))::context in
+        Cic.Lambda(name,ty,canonical_trough_lambda context' bo)
+    | t -> canonical context t
+
+  and canonical context t =
     match t with
       | Cic.LetIn(name,bo,rest) -> 
+          let bo = canonical_trough_lambda context bo in
           let context' = (Some (name,Cic.Def (bo,None)))::context in
-          Cic.LetIn(name,canonical context bo,canonical context' rest)
+          Cic.LetIn(name,bo,canonical context' rest)
       | Cic.Appl (((Cic.Const(uri_sym,ens))::tl) as args)
           when LibraryObjects.is_sym_eq_URI uri_sym ->
           (match p_of_sym ens tl with
@@ -302,29 +351,32 @@ let canonical t context menv =
                    mk_trans uri_trans ty r m l 
                      (canonical context (mk_sym uri_sym ty m r p2)) 
                      (canonical context (mk_sym uri_sym ty l m p1))
-             | Cic.Appl (([Cic.Const(uri_feq,ens);ty1;ty2;f;x;y;p])) ->
+             | Cic.Appl (([Cic.Const(uri_feq,ens);ty1;ty2;f;x;y;p]))
+                 when LibraryObjects.is_eq_f_URI uri_feq ->
                  let eq = LibraryObjects.eq_URI_of_eq_f_URI uri_feq in
                  let eq_f_sym =
                    Cic.Const (LibraryObjects.eq_f_sym_URI ~eq, [])
                  in
-                 Cic.Appl (([eq_f_sym;ty1;ty2;f;x;y;p]))  
+                 let rc = Cic.Appl [eq_f_sym;ty1;ty2;f;x;y;p] in
+                 Utils.debug_print (lazy ("CANONICAL " ^ CicPp.ppterm rc));
+                 rc
              | Cic.Appl [Cic.MutConstruct (uri, 0, 1,_);_;_] as t
                  when LibraryObjects.is_eq_URI uri -> t
              | _ -> Cic.Appl (List.map (canonical context) args))
       | Cic.Appl l -> Cic.Appl (List.map (canonical context) l)
       | _ -> t
   in
-  remove_refl (canonical context t)
+   remove_cycles (remove_refl (canonical context t))
 ;;
   
 let compose_contexts ctx1 ctx2 = 
   ProofEngineReduction.replace_lifting 
-    ~equality:(=) ~what:[Cic.Implicit(Some `Hole)] ~with_what:[ctx2] ~where:ctx1
+  ~equality:(fun _ ->(=)) ~context:[] ~what:[Cic.Implicit(Some `Hole)] ~with_what:[ctx2] ~where:ctx1
 ;;
 
 let put_in_ctx ctx t = 
   ProofEngineReduction.replace_lifting
-    ~equality:(=) ~what:[Cic.Implicit (Some `Hole)] ~with_what:[t] ~where:ctx
+  ~equality:(fun _ -> (=)) ~context:[] ~what:[Cic.Implicit (Some `Hole)] ~with_what:[t] ~where:ctx
 ;;
 
 let mk_eq uri ty l r =
@@ -372,7 +424,8 @@ let contextualize uri ty left right t =
    * ctx is a term with an hole. Cic.Implicit(Some `Hole) is the empty context
    * ctx_ty is the type of ctx
    *)
-    let rec aux uri ty left right ctx_d ctx_ty = function
+    let rec aux uri ty left right ctx_d ctx_ty t =
+      match t with 
       | 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
@@ -407,8 +460,8 @@ let contextualize uri ty left right t =
           let c_what = put_in_ctx ctx_c what in
           (* now put the proofs in the compound context *)
           let p1 = (* p1: dc_what = d_m *)
-            if is_not_fixed_lp then 
-              aux uri ty2 c_what m ctx_d ctx_ty p1 
+            if is_not_fixed_lp then
+              aux uri ty2 c_what m ctx_d ctx_ty p1
             else
               mk_sym uri_sym ctx_ty d_m dc_what
                 (aux uri ty2 m c_what ctx_d ctx_ty p1)
@@ -417,7 +470,7 @@ let contextualize uri ty left right t =
             if avoid_eq_ind then
               mk_sym uri_sym ctx_ty dc_what dc_other
                 (aux uri ty1 what other ctx_dc ctx_ty p2)
-            else
+             else
               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
@@ -496,8 +549,8 @@ let build_proof_step eq lift subst p1 p2 pos l r pred =
     p
 ;;
 
-let parametrize_proof p l r ty = 
-  let uniq l = HExtlib.list_uniq (List.sort Pervasives.compare l) in
+let parametrize_proof p l r = 
+  let uniq l = HExtlib.list_uniq (List.sort (fun (i,_) (j,_) -> Pervasives.compare i j) l) in
   let mot = CicUtil.metas_of_term_set in
   let parameters = uniq (mot p @ mot l @ mot r) in 
   (* ?if they are under a lambda? *)
@@ -506,6 +559,21 @@ let parametrize_proof p l r ty =
     HExtlib.list_uniq (List.sort Pervasives.compare parameters) 
   in
 *)
+  (* resorts l such that *hopefully* dependencies can be inferred *)
+  let guess_dependency p l =
+    match p with
+    | Cic.Appl ((Cic.Const(uri_ind,ens))::tl) 
+        when LibraryObjects.is_eq_ind_URI uri_ind || 
+             LibraryObjects.is_eq_ind_r_URI uri_ind ->
+        let ty,_,_,_,_,_ = open_eq_ind tl in
+        let metas = CicUtil.metas_of_term ty in
+        let nondep, dep = 
+          List.partition (fun (i,_) -> List.exists (fun (j,_) -> j=i) metas) l
+        in
+        nondep@dep
+    | _ -> l
+  in
+  let parameters = guess_dependency p parameters in
   let what = List.map (fun (i,l) -> Cic.Meta (i,l)) parameters in 
   let with_what, lift_no = 
     List.fold_right (fun _ (acc,n) -> ((Cic.Rel n)::acc),n+1) what ([],1) 
@@ -513,14 +581,12 @@ let parametrize_proof p l r ty =
   let p = CicSubstitution.lift (lift_no-1) p in
   let p = 
     ProofEngineReduction.replace_lifting
-    ~equality:(fun t1 t2 -> 
+    ~equality:(fun _ t1 t2 -> 
       match t1,t2 with Cic.Meta (i,_),Cic.Meta(j,_) -> i=j | _ -> false) 
+    ~context:[]
     ~what ~with_what ~where:p
   in
-  let ty_of_m _ = ty (*function 
-    | Cic.Meta (i,_) -> List.assoc i menv 
-    | _ -> assert false *)
-  in
+  let ty_of_m _ = Cic.Implicit (Some `Type) in
   let args, proof,_ = 
     List.fold_left 
       (fun (instance,p,n) m -> 
@@ -558,19 +624,19 @@ let wfo bag goalproof proof id =
 let string_of_id (id_to_eq,_) names id = 
   if id = 0 then "" else 
   try
-    let (_,p,(_,l,r,_),m,_) = open_equality (Hashtbl.find id_to_eq id) in
+    let (_,p,(t,l,r,_),m,_) = open_equality (Hashtbl.find id_to_eq id) in
     match p with
     | 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)) *)
-    | Step (_,(step,id1, (_,id2), _) ) ->
-        Printf.sprintf "%6d: %s %6d %6d   %s = %s [%s]" id
+(*           "..." *)
+         (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m)) 
+    | Step (_,(step,id1, (dir,id2), p) ) ->
+        Printf.sprintf "%6d: %s %6d %6d   %s =(%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)) *)
-          "..."
+          id1 id2 (CicPp.pp l names) (CicPp.pp t names) (CicPp.pp r names)
+         (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m)) 
+          (*"..."*)
   with
       Not_found -> assert false
 
@@ -721,7 +787,6 @@ let build_goal_proof bag eq l initial ty se context menv =
   let se = List.map (fun i -> Cic.Meta (i,[])) se in 
   let lets = get_duplicate_step_in_wfo bag 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 lets,_,h = 
     List.fold_left
@@ -729,7 +794,7 @@ let build_goal_proof bag eq l initial ty se context menv =
         let p,l,r = proof_of_id bag id in
         let cic = build_proof_term bag eq h n p in
         let real_cic,instance = 
-          parametrize_proof cic l r (CicSubstitution.lift n mty)
+          parametrize_proof cic l r 
         in
         let h = (id, instance)::lift_list h in
         acc@[id,real_cic],n+1,h) 
@@ -839,7 +904,8 @@ let fix_metas bag newmeta eq =
 (* 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 @
+         Utils.metas_of_term ty)) 
   in
   let subst, metasenv, newmeta = relocate newmeta menv to_be_relocated in
   let ty = Subst.apply_subst subst ty in
@@ -960,7 +1026,6 @@ let meta_convertibility_eq eq1 eq2 =
         false
 ;;
 
-
 let meta_convertibility t1 t2 =
   if t1 = t2 then
     true
@@ -972,6 +1037,32 @@ let meta_convertibility t1 t2 =
       false
 ;;
 
+let meta_convertibility_subst t1 t2 menv =
+  if t1 = t2 then
+    Some([])
+  else
+    try
+      let (l,_) = meta_convertibility_aux ([],[]) t1 t2 in
+      let subst =
+	List.map
+	  (fun (x,y) ->
+	     try 
+	       let (_,c,t) = CicUtil.lookup_meta x menv in
+	       let irl = 
+		 CicMkImplicit.identity_relocation_list_for_metavariable c in
+	       (y,(c,Cic.Meta(x,irl),t))
+	     with CicUtil.Meta_not_found _ ->
+	       try 
+		 let (_,c,t) = CicUtil.lookup_meta y menv in
+		 let irl =  
+		   CicMkImplicit.identity_relocation_list_for_metavariable c in
+		   (x,(c,Cic.Meta(y,irl),t))
+	       with CicUtil.Meta_not_found _ -> assert false) l in   
+	Some subst
+    with NotMetaConvertible ->
+      None
+;;
+
 exception TermIsNotAnEquality;;
 
 let term_is_equality term =
@@ -1132,7 +1223,7 @@ let rec pp_proofterm name t context =
               when Pcre.pmatch ~pat:"eq_f" (UriManager.string_of_uri uri)->
                 pp true p
           | Cic.Appl [Cic.Const (uri,[]);_;_;_;_;_;p] 
-              when Pcre.pmatch ~pat:"eq_f1" (UriManager.string_of_uri uri)->
+              when Pcre.pmatch ~pat:"eq_OF_eq" (UriManager.string_of_uri uri)->
                 pp true p
           | Cic.Appl [Cic.MutConstruct (uri,_,_,[]);_;_;t;p] 
               when Pcre.pmatch ~pat:"ex.ind" (UriManager.string_of_uri uri)->
@@ -1169,3 +1260,104 @@ let pp_proofterm t =
   pp_proofterm (Some (Cic.Name "Hypothesis")) t []
 ;;
 
+let initial_nameset_list = [
+ "x"; "y"; "z"; "t"; "u"; "v"; "a"; "b"; "c"; "d"; 
+ "e"; "l"; "m"; "n"; "o"; "p"; "q"; "r"; 
+]
+
+module S = Set.Make(String)
+
+let initial_nameset = List.fold_right S.add initial_nameset_list S.empty, [];;
+
+let freshname (nameset, subst) term = 
+  let m = CicUtil.metas_of_term term in
+  let nameset, subst = 
+    List.fold_left 
+      (fun (set,rc) (m,_) -> 
+        if List.mem_assoc m rc then set,rc else
+        let name = S.choose set in
+        let set = S.remove name set in
+        set, 
+        (m,Cic.Const(UriManager.uri_of_string 
+             ("cic:/"^name^".con"),[]))::rc)
+      (nameset,subst) m
+  in
+  let term = 
+   ProofEngineReduction.replace
+    ~equality:(fun i t -> match t with Cic.Meta (j,_) -> i=j| _ -> false) 
+    ~what:(List.map fst subst) 
+    ~with_what:(List.map snd subst) ~where:term
+  in
+  (nameset, subst), term
+;;
+
+let remove_names_in_context (set,subst) names =
+  List.fold_left
+    (fun s n -> 
+      match n with Some (Cic.Name n) -> S.remove n s | _ -> s) 
+    set names, subst
+;;
+
+let string_of_id2 (id_to_eq,_) names nameset id = 
+  if id = 0 then "" else 
+  try
+    let (_,_,(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in
+    let nameset, l = freshname nameset l in
+    let nameset, r = freshname nameset r in
+    Printf.sprintf "%s = %s" (CicPp.pp l names) (CicPp.pp r names)
+  with
+      Not_found -> assert false
+;;
+
+let draw_proof bag names goal_proof proof id =
+  let b = Buffer.create 100 in
+  let fmt = Format.formatter_of_buffer b in 
+  let sint = string_of_int in
+  let fst3 (x,_,_) = x in
+  let visited = ref [] in
+  let nameset = remove_names_in_context initial_nameset names in
+  let rec fact id = function
+    | Exact t -> 
+        if not (List.mem id !visited) then
+          begin
+          visited := id :: !visited;
+          let nameset, t = freshname nameset t in
+          let t = CicPp.pp t names in
+          GraphvizPp.Dot.node (sint id) 
+          ~attrs:["label",t^":"^string_of_id2 bag names nameset id;
+          "shape","rectangle"] fmt;
+          end
+    | Step (_,(_,id1,(_,id2),_)) ->
+        GraphvizPp.Dot.edge (sint id) (sint id1) fmt;
+        GraphvizPp.Dot.edge (sint id) (sint id2) fmt;
+        let p1,_,_ = proof_of_id bag id1 in
+        let p2,_,_ = proof_of_id bag id2 in
+        fact id1 p1;
+        fact id2 p2;
+        if not (List.mem id !visited); then
+          begin
+          visited := id :: !visited;
+          GraphvizPp.Dot.node (sint id) 
+          ~attrs:["label",sint id^":"^string_of_id2 bag names nameset id;
+                  "shape","ellipse"] fmt
+          end
+  in
+  let sleft acc (_,_,id,_,_) =
+    if acc != 0 then GraphvizPp.Dot.edge (sint acc) (sint id) fmt;
+    fact id (fst3 (proof_of_id bag id));
+    id
+  in
+  GraphvizPp.Dot.header ~node_attrs:["fontsize","10"; ] fmt;
+  ignore(List.fold_left sleft id goal_proof);
+  GraphvizPp.Dot.trailer fmt;
+  let oc = open_out "/tmp/matita_paramod.dot" in
+  Buffer.output_buffer oc b;
+  close_out oc;
+  Utils.debug_print (lazy "dot!");
+  ignore(Unix.system 
+    "dot -Tps -o /tmp/matita_paramod.eps /tmp/matita_paramod.dot"
+(* "cat /tmp/matita_paramod.dot| tred | dot -Tps -o /tmp/matita_paramod.eps" *)
+  );
+  ignore(Unix.system "gv /tmp/matita_paramod.eps");
+;;
+