-let pp_proof names goalproof proof =
- String.concat "\n" (List.map (string_of_id names) (wfo goalproof proof)) ^
- "\ngoal is demodulated with " ^
- (String.concat " "
- ((List.map (fun (_,i,_,_) -> string_of_int i) goalproof)))
+let pp_proof names goalproof proof subst id initial_goal =
+ String.concat "\n" (List.map (string_of_id names) (wfo goalproof proof id)) ^
+ "\ngoal:\n " ^
+ (String.concat "\n "
+ (fst (List.fold_right
+ (fun (r,pos,i,s,pred) (acc,g) ->
+ let _,_,left,right = open_eq g in
+ let ty =
+ match pos with
+ | Utils.Left -> CicReduction.head_beta_reduce (Cic.Appl[pred;right])
+ | Utils.Right -> CicReduction.head_beta_reduce (Cic.Appl[pred;left])
+ in
+ let ty = Subst.apply_subst s ty in
+ ("("^ string_of_rule r ^ " " ^ string_of_int i^") -> "
+ ^ CicPp.pp ty names) :: acc,ty) goalproof ([],initial_goal)))) ^
+ "\nand then subsumed by " ^ string_of_int id ^ " when " ^ Subst.ppsubst subst
+;;
+
+module OT =
+ struct
+ type t = int
+ let compare = Pervasives.compare
+ end
+
+module M = Map.Make(OT)
+
+let rec find_deps m i =
+ if M.mem i m then m
+ else
+ let p,_,_ = proof_of_id i in
+ match p with
+ | Exact _ -> M.add i [] m
+ | Step (_,(_,id1,(_,id2),_)) ->
+ let m = find_deps m id1 in
+ let m = find_deps m id2 in
+ M.add i (M.find id1 m @ M.find id2 m @ [id1;id2]) m
+;;
+
+let topological_sort l =
+ (* build the partial order relation *)
+ let m =
+ List.fold_left (fun m i -> find_deps m i)
+ M.empty l
+ in
+ 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