X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=components%2Ftactics%2Fparamodulation%2Fequality.ml;h=0b0b73e3f27c74ff0d5fefc202d904937726253c;hb=894b08ca7d14aa7e31c35f3acb3903a1c3472a27;hp=3ac57e6fe63ed2285b06722d7e7dd04853cf298f;hpb=d8d939cc3f78a805a3c16f715912ecd96c302592;p=helm.git

diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml
index 3ac57e6fe..0b0b73e3f 100644
--- a/components/tactics/paramodulation/equality.ml
+++ b/components/tactics/paramodulation/equality.ml
@@ -23,7 +23,7 @@
  * http://cs.unibo.it/helm/.
  *)
 
-let _profiler = <:profiler<_profiler>>;;
+(* let _profiler = <:profiler<_profiler>>;; *)
 
 (* $Id: inference.ml 6245 2006-04-05 12:07:51Z tassi $ *)
 
@@ -67,6 +67,7 @@ let mk_equality (weight,p,(ty,l,r,o),m) =
   let id = freshid () in
   let eq = (uncomparable,weight,p,(ty,l,r,o),m,id) in
   Hashtbl.add id_to_eq id eq;
+
   eq
 ;;
 
@@ -93,7 +94,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
@@ -101,13 +103,39 @@ 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,_,_) =
   Pervasives.compare s1 s2
 ;;
 
+let rec max_weight_in_proof current =
+  function
+   | Exact _ -> current
+   | Step (_, (_,id1,(_,id2),_)) ->
+       let eq1 = Hashtbl.find id_to_eq id1 in
+       let eq2 = Hashtbl.find id_to_eq id2 in  
+       let (w1,p1,(_,_,_,_),_,_) = open_equality eq1 in
+       let (w2,p2,(_,_,_,_),_,_) = open_equality eq2 in
+       let current = max current w1 in
+       let current = max_weight_in_proof current p1 in
+       let current = max current w2 in
+       max_weight_in_proof current p2
+
+let max_weight_in_goal_proof =
+  List.fold_left 
+    (fun current (_,_,id,_,_) ->
+       let eq = Hashtbl.find id_to_eq id in
+       let (w,p,(_,_,_,_),_,_) = open_equality eq in
+       let current = max current w in
+       max_weight_in_proof current p)
+
+let max_weight goal_proof proof =
+  let current = max_weight_in_proof 0 proof in
+  max_weight_in_goal_proof current goal_proof
+
 let proof_of_id id =
   try
     let (_,p,(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in
@@ -237,8 +265,35 @@ let is_not_fixed t =
    CicSubstitution.subst (Cic.Rel 1) t
 ;;
 
+let head_of_apply = function | Cic.Appl (hd::_) -> hd | t -> t;;
+let tail_of_apply = function | Cic.Appl (_::tl) -> tl | t -> [];;
+let count_args t = List.length (tail_of_apply t);;
+let rec build_nat = 
+  let u = UriManager.uri_of_string "cic:/matita/nat/nat/nat.ind" in
+  function
+    | 0 -> Cic.MutConstruct(u,0,1,[])
+    | n -> 
+        Cic.Appl [Cic.MutConstruct(u,0,2,[]);build_nat (n-1)]
+;;
+let tyof context menv t =
+  try
+    fst(CicTypeChecker.type_of_aux' menv context t CicUniv.empty_ugraph)
+  with
+  | CicTypeChecker.TypeCheckerFailure _
+  | CicTypeChecker.AssertFailure _ -> assert false
+;;
+let rec lambdaof left context = function
+  | Cic.Prod (n,s,t) ->
+      Cic.Lambda (n,s,lambdaof left context t)
+  | Cic.Appl [Cic.MutInd (uri, 0,_);ty;l;r] 
+      when LibraryObjects.is_eq_URI uri -> if left then l else r
+  | t -> 
+      let names = Utils.names_of_context context in
+      prerr_endline ("lambdaof: " ^ (CicPp.pp t names));
+      assert false
+;;
 
-let canonical t = 
+let canonical t context menv = 
   let rec remove_refl t =
     match t with
     | Cic.Appl (((Cic.Const(uri_trans,ens))::tl) as args)
@@ -255,21 +310,53 @@ let canonical t =
         Cic.LetIn (name,remove_refl bo,remove_refl rest)
     | _ -> t
   in
-  let rec canonical t =
+  let rec canonical context t =
     match t with
-      | Cic.LetIn(name,bo,rest) -> Cic.LetIn(name,canonical bo,canonical rest)
+      | Cic.LetIn(name,bo,rest) -> 
+          let context' = (Some (name,Cic.Def (bo,None)))::context in
+          Cic.LetIn(name,canonical context 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
              | Cic.Appl ((Cic.Const(uri,ens))::tl)
                  when LibraryObjects.is_sym_eq_URI uri -> 
-                   canonical (p_of_sym ens tl)
+                   canonical context (p_of_sym ens tl)
              | 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
                    mk_trans uri_trans ty r m l 
-                     (canonical (mk_sym uri_sym ty m r p2)) 
-                     (canonical (mk_sym uri_sym ty l m p1))
+                     (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])) ->
+                 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 sym_eq = Cic.Const(uri_sym,ens) in
+                 let eq_f = Cic.Const(uri_feq,[]) in
+                 let b = Cic.MutConstruct (UriManager.uri_of_string
+                   "cic:/matita/datatypes/bool/bool.ind",0,1,[])
+                 in
+                 let u = ty1 in
+                 let ctx = f in
+                 let n = build_nat (count_args p) in
+                 let h = head_of_apply p in
+                 let predl = lambdaof true context (tyof context menv h) in 
+                 let predr = lambdaof false context (tyof context menv h) in
+                 let args = tail_of_apply p in
+                 let appl = 
+                   Cic.Appl
+                    ([Cic.Const(UriManager.uri_of_string
+                      "cic:/matita/paramodulation/rewrite.con",[]);
+                      eq; sym_eq; eq_f; b; u; ctx; n; predl; predr; h] @
+                      args)
+                 in
+                 appl
+*)
+(*
              | Cic.Appl (((Cic.Const(uri_ind,ens)) as he)::tl) 
                  when LibraryObjects.is_eq_ind_URI uri_ind || 
                       LibraryObjects.is_eq_ind_r_URI uri_ind ->
@@ -293,13 +380,14 @@ let canonical t =
                  Cic.Appl 
                    [he;ty;what;pred;
                     canonical (mk_sym uri_sym ty l r p1);other;canonical p2]
+*)
              | Cic.Appl [Cic.MutConstruct (uri, 0, 1,_);_;_] as t
                  when LibraryObjects.is_eq_URI uri -> t
-             | _ -> Cic.Appl (List.map canonical args))
-      | Cic.Appl l -> Cic.Appl (List.map canonical l)
+             | _ -> Cic.Appl (List.map (canonical context) args))
+      | Cic.Appl l -> Cic.Appl (List.map (canonical context) l)
       | _ -> t
   in
-  remove_refl (canonical t)
+  remove_refl (canonical context t)
 ;;
   
 let ty_of_lambda = function
@@ -331,16 +419,33 @@ let open_eq = function
   | _ -> assert false
 ;;
 
+let mk_feq uri_feq ty ty1 left pred right t = 
+  Cic.Appl [Cic.Const(uri_feq,[]);ty;ty1;pred;left;right;t]
+;;
+
+let rec look_ahead aux = function
+  | Cic.Appl ((Cic.Const(uri_ind,ens))::tl) as t
+        when LibraryObjects.is_eq_ind_URI uri_ind || 
+             LibraryObjects.is_eq_ind_r_URI uri_ind ->
+          let ty1,what,pred,p1,other,p2 = open_eq_ind tl in
+          let ty2,eq,lp,rp = open_pred pred in 
+          let hole = Cic.Implicit (Some `Hole) in
+          let ty2 = CicSubstitution.subst hole ty2 in
+          aux ty1 (CicSubstitution.subst other lp) (CicSubstitution.subst other rp) hole ty2 t
+  | Cic.Lambda (n,s,t) -> Cic.Lambda (n,s,look_ahead aux t)
+  | t -> t
+;;
+
 let contextualize uri ty left right t = 
   let hole = Cic.Implicit (Some `Hole) in
-  (* aux [uri] [ty] [left] [right] [ctx] [t] 
+  (* aux [uri] [ty] [left] [right] [ctx] [ctx_ty] [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 hole. Cic.Implicit(Some `Hole) is the empty context
-   * ty_ctx is the type of ctx_d
+   * ctx_ty is the type of ctx
    *)
     let rec aux uri ty left right ctx_d ctx_ty = function
       | Cic.Appl ((Cic.Const(uri_sym,ens))::tl) 
@@ -348,8 +453,7 @@ let contextualize uri ty left right t =
           let ty,l,r,p = open_sym ens tl in
           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 ctx_ty rest)
+          Cic.LetIn (name,look_ahead (aux uri) 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 ->
@@ -404,23 +508,26 @@ let contextualize uri ty left right t =
           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 uri_sym = LibraryObjects.sym_eq_URI ~eq:uri in *)
+(*         let uri_ind = LibraryObjects.eq_ind_URI ~eq:uri in *)
+
+        let uri_feq = LibraryObjects.eq_f_URI ~eq:uri in
         let pred = 
-          (* ctx_d will go under a lambda, but put_in_ctx substitutes Rel 1 *)
-          let r = CicSubstitution.lift 1 (put_in_ctx ctx_d left) 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))
+(*           let lty = CicSubstitution.lift 1 ctx_ty in  *)
+(*           Cic.Lambda (Cic.Name "foo",ty,(mk_eq uri lty l r)) *)
+          Cic.Lambda (Cic.Name "foo",ty,l)
         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 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)
+(*         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 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) *)
+          (mk_feq uri_feq ty ctx_ty left pred right t)
   in
   aux uri ty left right hole ty t
 ;;
@@ -467,7 +574,7 @@ let build_proof_step eq lift subst p1 p2 pos l r pred =
 let parametrize_proof p l r ty = 
   let uniq l = HExtlib.list_uniq (List.sort Pervasives.compare l) in
   let mot = CicUtil.metas_of_term_set in
-  let parameters = uniq (mot p @ mot l @ mot r) in 
+  let parameters = uniq ((*mot p @*) mot l @ mot r) in 
   (* ?if they are under a lambda? *)
   let parameters = 
     HExtlib.list_uniq (List.sort Pervasives.compare parameters) 
@@ -492,7 +599,7 @@ let parametrize_proof p l r ty =
       (fun (instance,p,n) m -> 
         (instance@[m],
         Cic.Lambda 
-          (Cic.Name ("x"^string_of_int n),
+          (Cic.Name ("X"^string_of_int n),
           CicSubstitution.lift (lift_no - n - 1) (ty_of_m m),
           p),
         n+1)) 
@@ -529,12 +636,14 @@ 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
 
@@ -681,7 +790,7 @@ let build_proof_term eq h lift proof =
    aux proof
 ;;
 
-let build_goal_proof eq l initial ty se =
+let build_goal_proof 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 l initial in
   let letsno = List.length lets in
@@ -736,9 +845,9 @@ let build_goal_proof eq l initial ty se =
           cic, p))
     lets (letsno-1,initial)
   in
-(*    canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty)),
- *    *)
-proof,
+   canonical 
+     (contextualize_rewrites proof (CicSubstitution.lift letsno ty))
+     context menv,
    se 
 ;;
 
@@ -1034,7 +1143,7 @@ module IntSet = Set.Make(IntOT);;
 let n_purged = ref 0;;
 
 let collect alive1 alive2 alive3 =
-  let _ = <:start<collect>> in
+(*   let _ = <:start<collect>> in *)
   let deps_of id = 
     let p,_,_ = proof_of_id id in  
     match p with
@@ -1057,14 +1166,87 @@ let collect alive1 alive2 alive3 =
   in
   n_purged := !n_purged + List.length to_purge;
   List.iter (Hashtbl.remove id_to_eq) to_purge;
-  let _ = <:stop<collect>> in ()  
+(*   let _ = <:stop<collect>> in ()   *)
 ;;
 
 let id_of e = 
   let _,_,_,_,id = open_equality e in id
 ;;
 
-let get_stats () = 
+let get_stats () = "" 
+(*
   <:show<Equality.>> ^ 
   "# of purged eq by the collector: " ^ string_of_int !n_purged ^ "\n"
+*)
+;;
+
+let rec pp_proofterm name t context = 
+  let rec skip_lambda tys ctx = function
+    | Cic.Lambda (n,s,t) -> skip_lambda (s::tys) ((Some n)::ctx) t
+    | t -> ctx,tys,t
+  in
+  let rename s name = 
+    match name with 
+    | Cic.Name s1 -> Cic.Name (s ^ s1)
+    | _ -> assert false
+  in
+  let rec skip_letin ctx = function
+    | Cic.LetIn (n,b,t) -> 
+        pp_proofterm (Some (rename "Lemma " n)) b ctx:: 
+          skip_letin ((Some n)::ctx) t
+    | t -> 
+        let ppterm t = CicPp.pp t ctx in
+        let rec pp inner = function
+          | Cic.Appl [Cic.Const (uri,[]);_;l;m;r;p1;p2] 
+              when Pcre.pmatch ~pat:"trans_eq" (UriManager.string_of_uri uri)->
+                if not inner then
+                  ("     " ^ ppterm l) :: pp true p1 @ 
+                            [ "   = " ^ ppterm m ] @ pp true p2 @ 
+                            [ "   = " ^ ppterm r ]
+                else
+                   pp true p1 @ 
+                            [ "   = " ^ ppterm m ] @ pp true p2 
+          | Cic.Appl [Cic.Const (uri,[]);_;l;m;p] 
+              when Pcre.pmatch ~pat:"sym_eq" (UriManager.string_of_uri uri)->
+                pp true p
+          | Cic.Appl [Cic.Const (uri,[]);_;_;_;_;_;p] 
+              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)->
+                pp true p
+          | Cic.Appl [Cic.MutConstruct (uri,_,_,[]);_;_;t;p] 
+              when Pcre.pmatch ~pat:"ex.ind" (UriManager.string_of_uri uri)->
+                      [ "witness " ^ ppterm t ] @ pp true p
+          | Cic.Appl (t::_) ->[ " [by " ^ ppterm t ^ "]"]
+          | t ->[ " [by " ^ ppterm t ^ "]"]
+        in
+        let rec compat = function
+          | a::b::tl -> (b ^ a) :: compat tl
+          | h::[] -> [h]
+          | [] -> []
+        in
+        let compat l = List.hd l :: compat (List.tl l) in
+        compat (pp false t) @ ["";""]
+  in      
+  let names, tys, body = skip_lambda [] context t in
+  let ppname name = (match name with Some (Cic.Name s) -> s | _ -> "") in
+  ppname name ^ ":\n" ^
+  (if context = [] then
+     let rec pp_l ctx = function
+          | (t,name)::tl -> 
+              "   " ^ ppname name ^ ": " ^ CicPp.pp t ctx ^ "\n" ^ 
+              pp_l (name::ctx) tl
+          | [] -> "\n\n"
+     in
+       pp_l [] (List.rev (List.combine tys names))
+   else "")
+    ^
+  String.concat "\n" (skip_letin names body)
+;;
+
+let pp_proofterm t = 
+  "\n\n" ^ 
+  pp_proofterm (Some (Cic.Name "Hypothesis")) t []
 ;;
+