+let symmetric bag eq_ty l id uri m =
+ let eq = Cic.MutInd(uri,0,[]) in
+ let pred =
+ Cic.Lambda (Cic.Name "Sym",eq_ty,
+ Cic.Appl [CicSubstitution.lift 1 eq ;
+ CicSubstitution.lift 1 eq_ty;
+ Cic.Rel 1;CicSubstitution.lift 1 l])
+ in
+ let prefl =
+ Exact (Cic.Appl
+ [Cic.MutConstruct(uri,0,1,[]);eq_ty;l])
+ in
+ let id1 =
+ let eq = mk_equality bag (0,prefl,(eq_ty,l,l,Utils.Eq),m) in
+ let (_,_,_,_,id) = open_equality eq in
+ id
+ in
+ Step(Subst.empty_subst,
+ (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 ((id_to_eq,_) as bag) alive1 alive2 alive3 =
+(* let _ = <:start<collect>> in *)
+ let deps_of id =
+ let p,_,_ = proof_of_id bag 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 []
+;;
+