X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fequality.ml;h=b7a8a9f6b2b0ef31783d8183d226bb1d7b4e8707;hb=4ab3123d6a8e5080009d7b471b0cefd05f4817ed;hp=1e9e97ec58f3147733356cfde501a72bdf83da74;hpb=50844b0116c863862434c7c673c5caaf6ff78cdf;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml
index 1e9e97ec5..b7a8a9f6b 100644
--- a/helm/software/components/tactics/paramodulation/equality.ml
+++ b/helm/software/components/tactics/paramodulation/equality.ml
@@ -23,6 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
+(* let _profiler = <:profiler<_profiler>>;; *)
+
 (* $Id: inference.ml 6245 2006-04-05 12:07:51Z tassi $ *)
 
 type rule = SuperpositionRight | SuperpositionLeft | Demodulation
@@ -44,6 +46,8 @@ and proof =
 and goal_proof = (rule * Utils.pos * int * Subst.substitution * Cic.term) list
 ;;
 
+type goal = goal_proof * Cic.metasenv * Cic.term
+
 (* globals *)
 let maxid = ref 0;;
 let id_to_eq = Hashtbl.create 1024;;
@@ -63,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
 ;;
 
@@ -89,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
@@ -97,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
@@ -233,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)
@@ -251,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 ->
@@ -289,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
@@ -327,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) 
@@ -344,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 ->
@@ -400,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
 ;;
@@ -430,7 +541,7 @@ 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))
+        Step (Subst.concat subst s,(rule, id1, (pos,id2), pred))
 ;;
 	
 let build_proof_step eq lift subst p1 p2 pos l r pred =
@@ -461,12 +572,15 @@ let build_proof_step eq lift subst p1 p2 pos l r pred =
 ;;
 
 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 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 
+  (* ?if they are under a lambda? *)
+(*
   let parameters = 
     HExtlib.list_uniq (List.sort Pervasives.compare 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) 
@@ -487,7 +601,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)) 
@@ -524,12 +638,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
 
@@ -576,9 +692,12 @@ let rec find_deps m i =
 
 let topological_sort l = 
   (* build the partial order relation *)
-  let m = 
-    List.fold_left (fun m i -> find_deps m i)
-    M.empty l
+  let m = List.fold_left (fun m i -> find_deps m i) M.empty l in
+  let m = (* keep only deps inside l *) 
+    List.fold_left 
+      (fun m' i ->
+        M.add i (List.filter (fun x -> List.mem x l) (M.find i m)) m') 
+      M.empty l 
   in
   let m = M.map (fun x -> Some x) m in
   (* utils *)
@@ -599,7 +718,8 @@ let topological_sort l =
       let res = ok @ res in
       if ok = [] then res else aux m res
   in
-  aux m []
+  let rc = List.rev (aux m []) in
+  rc
 ;;
   
 
@@ -646,7 +766,8 @@ let build_proof_term eq h lift proof =
     try List.assoc id h,l,r with Not_found -> aux p, l, r
   in
   let rec aux = function
-     | Exact term -> CicSubstitution.lift lift term
+     | Exact term -> 
+         CicSubstitution.lift lift term
      | Step (subst,(rule, id1, (pos,id2), pred)) ->
          let p1,_,_ = proof_of_id aux id1 in
          let p2,l,r = proof_of_id aux id2 in
@@ -661,7 +782,7 @@ let build_proof_term eq h lift proof =
            | Cic.Lambda (_,a,b) -> Cic.Lambda (varname,a,b)
            | _ -> assert false
          in
-         let p =   build_proof_step eq 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);
@@ -671,7 +792,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
@@ -726,7 +847,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)),
+   canonical 
+     (contextualize_rewrites proof (CicSubstitution.lift letsno ty))
+     context menv,
    se 
 ;;
 
@@ -747,6 +870,15 @@ let metas_of_proof p =
   Utils.metas_of_term p
 ;;
 
+let remove_local_context eq =
+   let w, p, (ty, left, right, o), menv,id = open_equality eq in
+   let p = Utils.remove_local_context p in
+   let ty = Utils.remove_local_context ty in
+   let left = Utils.remove_local_context left in
+   let right = Utils.remove_local_context right in
+   w, p, (ty, left, right, o), menv, id
+;;
+
 let relocate newmeta menv to_be_relocated =
   let subst, newmetasenv, newmeta = 
     List.fold_right 
@@ -761,6 +893,20 @@ let relocate newmeta menv to_be_relocated =
   let menv = Subst.apply_subst_metasenv subst menv @ newmetasenv in
   subst, menv, newmeta
 
+let fix_metas_goal newmeta goal =
+  let (proof, menv, ty) = goal in
+  let to_be_relocated = 
+    HExtlib.list_uniq (List.sort Pervasives.compare (Utils.metas_of_term ty))
+  in
+  let subst, menv, newmeta = relocate newmeta menv to_be_relocated in
+  let ty = Subst.apply_subst subst ty in
+  let proof = 
+    match proof with
+    | [] -> assert false (* is a nonsense to relocate the initial goal *)
+    | (r,pos,id,s,p) :: tl -> (r,pos,id,Subst.concat subst s,p) :: tl
+  in
+  newmeta+1,(proof, menv, ty)
+;;
 
 let fix_metas newmeta eq = 
   let w, p, (ty, left, right, o), menv,_ = open_equality eq in
@@ -989,3 +1135,120 @@ let symmetric eq_ty l id uri m =
     (Demodulation,id1,(Utils.Left,id),pred))
 ;;
 
+module IntOT = struct
+  type t = int
+  let compare = Pervasives.compare
+end
+
+module IntSet = Set.Make(IntOT);;
+
+let n_purged = ref 0;;
+
+let collect alive1 alive2 alive3 =
+(*   let _ = <:start<collect>> in *)
+  let deps_of id = 
+    let p,_,_ = proof_of_id id in  
+    match p with
+    | Exact _ -> IntSet.empty
+    | Step (_,(_,id1,(_,id2),_)) ->
+          IntSet.add id1 (IntSet.add id2 IntSet.empty)
+  in
+  let rec close s = 
+    let news = IntSet.fold (fun id s -> IntSet.union (deps_of id) s) s s in
+    if IntSet.equal news s then s else close news
+  in
+  let l_to_s s l = List.fold_left (fun s x -> IntSet.add x s) s l in
+  let alive_set = l_to_s (l_to_s (l_to_s IntSet.empty alive2) alive1) alive3 in
+  let closed_alive_set = close alive_set in
+  let to_purge = 
+    Hashtbl.fold 
+      (fun k _ s -> 
+        if not (IntSet.mem k closed_alive_set) then
+          k::s else s) id_to_eq []
+  in
+  n_purged := !n_purged + List.length to_purge;
+  List.iter (Hashtbl.remove id_to_eq) to_purge;
+(*   let _ = <:stop<collect>> in ()   *)
+;;
+
+let id_of e = 
+  let _,_,_,_,id = open_equality e in id
+;;
+
+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 []
+;;
+