+ 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
+ let h = Hashtbl.create 13 in
+ (* 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 =
+ let p,_,_ = proof_of_id i in
+ match p with
+ | Exact _ -> true
+ | _ ->
+ try
+ let no = Hashtbl.find h i in
+ Hashtbl.replace h i (no+1);
+ false
+ with Not_found -> Hashtbl.add h i 1;true
+ in
+ let rec aux = function
+ | Exact _ -> ()
+ | Step (_,(_,i1,(_,i2),_)) ->
+ 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 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 =
+ let proof_of_id aux id =
+ let p,l,r = proof_of_id id in
+ 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
+ | 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
+ let varname =
+ match rule with
+ | SuperpositionRight -> Cic.Name ("SupR" ^ Utils.string_of_pos pos)
+ | Demodulation -> Cic.Name ("DemEq"^ Utils.string_of_pos pos)
+ | _ -> assert false
+ in
+ let pred =
+ match pred with
+ | Cic.Lambda (_,a,b) -> Cic.Lambda (varname,a,b)
+ | _ -> 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
+ in
+ aux proof
+;;
+
+let build_goal_proof l initial ty se =
+ 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
+ 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
+ (fun (acc,n,h) id ->
+ let p,l,r = proof_of_id id in
+ let cic = build_proof_term h n p in
+ let real_cic,instance =
+ parametrize_proof cic l r (CicSubstitution.lift n mty)
+ in
+ let h = (id, instance)::lift_list h in
+ acc@[id,real_cic],n+1,h)
+ ([],0,[]) lets
+ in
+ let proof,se =
+ let rec aux se current_proof = function
+ | [] -> current_proof,se
+ | (rule,pos,id,subst,pred)::tl ->
+ let p,l,r = proof_of_id id in
+ let p = build_proof_term h letsno p in
+ let pos = if pos = Utils.Left then Utils.Right else Utils.Left in
+ let varname =
+ match rule with
+ | SuperpositionLeft -> Cic.Name ("SupL" ^ Utils.string_of_pos pos)
+ | Demodulation -> Cic.Name ("DemG"^ Utils.string_of_pos pos)
+ | _ -> assert false
+ in
+ let pred =
+ match pred with
+ | Cic.Lambda (_,a,b) -> Cic.Lambda (varname,a,b)
+ | _ -> assert false
+ in
+ let proof =
+ build_proof_step letsno subst current_proof p pos l r pred
+ in
+ let proof,se = aux se proof tl in
+ Subst.apply_subst_lift letsno subst proof,
+ List.map (fun x -> Subst.apply_subst_lift letsno subst x) se
+ in
+ aux se (build_proof_term h letsno initial) l
+ in
+ let n,proof =
+ let initial = proof in
+ List.fold_right
+ (fun (id,cic) (n,p) ->
+ n-1,
+ Cic.LetIn (
+ Cic.Name ("H"^string_of_int id),
+ cic, p))
+ lets (letsno-1,initial)
+ in
+ (proof,se)
+ (* canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty)),
+ se *)