+let is_meta_closed goals =
+ List.for_all (fun (_, _, g) -> CicUtil.is_meta_closed g) goals
+;;
+
+
+(* applies a series of theorems/equalities to a conjunction of goals *)
+let rec apply_to_goal_conj env theorems ?passive active (depth, goals) =
+ let aux (goal, r) tl =
+ let propagate_subst subst (proof, metas, term) =
+ let rec repl = function
+ | NoProof -> NoProof
+ | BasicProof t ->
+ BasicProof (CicMetaSubst.apply_subst subst t)
+ | ProofGoalBlock (p, pb) ->
+ let pb' = repl pb in
+ ProofGoalBlock (p, pb')
+ | SubProof (t, i, p) ->
+ let t' = CicMetaSubst.apply_subst subst t in
+ let p = repl p in
+ SubProof (t', i, p)
+ | ProofSymBlock (ens, p) -> ProofSymBlock (ens, repl p)
+ | ProofBlock (s, u, nty, t, pe, p) ->
+ ProofBlock (subst @ s, u, nty, t, pe, p)
+ in (repl proof, metas, term)
+ in
+ (* let r = apply_to_goal env theorems ?passive active goal in *) (
+ match r with
+ | `No -> `No (depth, goals)
+ | `GoOn sl ->
+ let l =
+ List.map
+ (fun (s, gl) ->
+ let tl = List.map (propagate_subst s) tl in
+ sort_goal_conj env (depth+1, gl @ tl)) sl
+ in
+ `GoOn l
+ | `Ok (subst, gl) ->
+ if tl = [] then
+ `Ok (depth, gl)
+ else
+ let p, _, _ = List.hd gl in
+ let subproof =
+ let rec repl = function
+ | SubProof (_, _, p) -> repl p
+ | ProofGoalBlock (p1, p2) ->
+ ProofGoalBlock (repl p1, repl p2)
+ | p -> p
+ in
+ build_proof_term (repl p)
+ in
+ let i =
+ let rec get_meta = function
+ | SubProof (_, i, p) ->
+ let i' = get_meta p in
+ if i' = -1 then i else i'
+(* max i (get_meta p) *)
+ | ProofGoalBlock (_, p) -> get_meta p
+ | _ -> -1
+ in
+ get_meta p
+ in
+ let subst =
+ let _, (context, _, _) = List.hd subst in
+ [i, (context, subproof, Cic.Implicit None)]
+ in
+ let tl = List.map (propagate_subst subst) tl in
+ let conj = sort_goal_conj env (depth(* +1 *), tl) in
+ `GoOn ([conj])
+ )
+ in
+ if depth > !maxdepth || (List.length goals) > !maxwidth then
+ `No (depth, goals)
+ else
+ let rec search_best res = function
+ | [] -> res
+ | goal::tl ->
+ let r = apply_to_goal env theorems ?passive active goal in
+ match r with
+ | `Ok _ -> (goal, r)
+ | `No -> search_best res tl
+ | `GoOn l ->
+ let newres =
+ match res with
+ | _, `Ok _ -> assert false
+ | _, `No -> goal, r
+ | _, `GoOn l2 ->
+ if (List.length l) < (List.length l2) then goal, r else res
+ in
+ search_best newres tl
+ in
+ let hd = List.hd goals in
+ let res = hd, (apply_to_goal env theorems ?passive active hd) in
+ let best =
+ match res with
+ | _, `Ok _ -> res
+ | _, _ -> search_best res (List.tl goals)
+ in
+ let res = aux best (List.filter (fun g -> g != (fst best)) goals) in
+ match res with
+ | `GoOn ([conj]) when is_meta_closed (snd conj) &&
+ (List.length (snd conj)) < (List.length goals)->
+ apply_to_goal_conj env theorems ?passive active conj
+ | _ -> res
+;;
+
+
+(*
+module OrderedGoals = struct
+ type t = int * (Inference.proof * Cic.metasenv * Cic.term) list
+
+ let compare g1 g2 =
+ let d1, l1 = g1
+ and d2, l2 = g2 in
+ let r = d2 - d1 in
+ if r <> 0 then r
+ else let r = (List.length l1) - (List.length l2) in
+ if r <> 0 then r
+ else
+ let res = ref 0 in
+ let _ =
+ List.exists2
+ (fun (_, _, t1) (_, _, t2) ->
+ let r = Pervasives.compare t1 t2 in
+ if r <> 0 then (
+ res := r;
+ true
+ ) else
+ false) l1 l2
+ in !res
+end
+
+module GoalsSet = Set.Make(OrderedGoals);;
+
+
+exception SearchSpaceOver;;
+*)
+
+
+(*
+let apply_to_goals env is_passive_empty theorems active goals =
+ debug_print (lazy "\n\n\tapply_to_goals\n\n");
+ let add_to set goals =
+ List.fold_left (fun s g -> GoalsSet.add g s) set goals
+ in
+ let rec aux set = function
+ | [] ->
+ debug_print (lazy "HERE!!!");
+ if is_passive_empty then raise SearchSpaceOver else false, set
+ | goals::tl ->
+ let res = apply_to_goal_conj env theorems active goals in
+ match res with
+ | `Ok newgoals ->
+ let _ =
+ let d, p, t =
+ match newgoals with
+ | (d, (p, _, t)::_) -> d, p, t
+ | _ -> assert false
+ in
+ debug_print
+ (lazy
+ (Printf.sprintf "\nOK!!!!\ndepth: %d\nProof: %s\ngoal: %s\n"
+ d (string_of_proof p) (CicPp.ppterm t)))
+ in
+ true, GoalsSet.singleton newgoals
+ | `GoOn newgoals ->
+ let set' = add_to set (goals::tl) in
+ let set' = add_to set' newgoals in
+ false, set'
+ | `No newgoals ->
+ aux set tl
+ in
+ let n = List.length goals in
+ let res, goals = aux (add_to GoalsSet.empty goals) goals in
+ let goals = GoalsSet.elements goals in
+ debug_print (lazy "\n\tapply_to_goals end\n");
+ let m = List.length goals in
+ if m = n && is_passive_empty then
+ raise SearchSpaceOver
+ else
+ res, goals
+;;
+*)
+
+
+(* sorts the list of passive goals to minimize the search for a proof (doesn't
+ work that well yet...) *)
+let sort_passive_goals goals =
+ List.stable_sort
+ (fun (d1, l1) (d2, l2) ->
+ let r1 = d2 - d1
+ and r2 = (List.length l1) - (List.length l2) in
+ let foldfun ht (_, _, t) =
+ let _ = List.map (fun i -> Hashtbl.replace ht i 1) (metas_of_term t)
+ in ht
+ in
+ let m1 = Hashtbl.length (List.fold_left foldfun (Hashtbl.create 3) l1)
+ and m2 = Hashtbl.length (List.fold_left foldfun (Hashtbl.create 3) l2)
+ in let r3 = m1 - m2 in
+ if r3 <> 0 then r3
+ else if r2 <> 0 then r2
+ else r1)
+ (* let _, _, g1 = List.hd l1 *)
+(* and _, _, g2 = List.hd l2 in *)
+(* let e1 = if Inference.term_is_equality g1 then 0 else 1 *)
+(* and e2 = if Inference.term_is_equality g2 then 0 else 1 *)
+(* in let r4 = e1 - e2 in *)
+(* if r4 <> 0 then r3 else r1) *)
+ goals
+;;
+
+
+let print_goals goals =
+ (String.concat "\n"
+ (List.map
+ (fun (d, gl) ->
+ let gl' =
+ List.map
+ (fun (p, _, t) ->
+ (* (string_of_proof p) ^ ", " ^ *) (CicPp.ppterm t)) gl
+ in
+ Printf.sprintf "%d: %s" d (String.concat "; " gl')) goals))
+;;
+
+
+(* tries to prove the first conjunction in goals with applications of
+ theorems/equalities, returning new sub-goals or an indication of success *)
+let apply_goal_to_theorems dbd env theorems ?passive active goals =
+ let theorems, _ = theorems in
+ let a_goals, p_goals = goals in
+ let goal = List.hd a_goals in
+ let not_in_active gl =
+ not
+ (List.exists
+ (fun (_, gl') ->
+ if (List.length gl) = (List.length gl') then
+ List.for_all2 (fun (_, _, g1) (_, _, g2) -> g1 = g2) gl gl'
+ else
+ false)
+ a_goals)
+ in
+ let aux theorems =
+ let res = apply_to_goal_conj env theorems ?passive active goal in
+ match res with
+ | `Ok newgoals ->
+ true, ([newgoals], [])
+ | `No _ ->
+ false, (a_goals, p_goals)
+ | `GoOn newgoals ->
+ let newgoals =
+ List.filter
+ (fun (d, gl) ->
+ (d <= !maxdepth) && (List.length gl) <= !maxwidth &&
+ not_in_active gl)
+ newgoals in
+ let p_goals = newgoals @ p_goals in
+ let p_goals = sort_passive_goals p_goals in
+ false, (a_goals, p_goals)
+ in
+ aux theorems
+;;
+
+
+let apply_theorem_to_goals env theorems active goals =
+ let a_goals, p_goals = goals in
+ let theorem = List.hd (fst theorems) in
+ let theorems = [theorem] in
+ let rec aux p = function
+ | [] -> false, ([], p)
+ | goal::tl ->
+ let res = apply_to_goal_conj env theorems active goal in
+ match res with
+ | `Ok newgoals -> true, ([newgoals], [])
+ | `No _ -> aux p tl
+ | `GoOn newgoals -> aux (newgoals @ p) tl
+ in
+ let ok, (a, p) = aux p_goals a_goals in
+ if ok then
+ ok, (a, p)
+ else
+ let p_goals =
+ List.stable_sort
+ (fun (d1, l1) (d2, l2) ->
+ let r = d2 - d1 in
+ if r <> 0 then r
+ else let r = (List.length l1) - (List.length l2) in
+ if r <> 0 then r
+ else
+ let res = ref 0 in
+ let _ =
+ List.exists2
+ (fun (_, _, t1) (_, _, t2) ->
+ let r = Pervasives.compare t1 t2 in
+ if r <> 0 then (res := r; true) else false) l1 l2
+ in !res)
+ p
+ in
+ ok, (a_goals, p_goals)
+;;
+
+
+(* given-clause algorithm with lazy reduction strategy *)
+let rec given_clause dbd env goals theorems passive active =
+ let goals = simplify_goals env goals active in
+ let ok, goals = activate_goal goals in
+ (* let theorems = simplify_theorems env theorems active in *)
+ if ok then
+ let ok, goals = apply_goal_to_theorems dbd env theorems active goals in
+ if ok then
+ let proof =
+ match (fst goals) with
+ | (_, [proof, _, _])::_ -> Some proof
+ | _ -> assert false
+ in
+ ParamodulationSuccess (proof, env)
+ else
+ given_clause_aux dbd env goals theorems passive active
+ else
+(* let ok', theorems = activate_theorem theorems in *)
+ let ok', theorems = false, theorems in
+ if ok' then
+ let ok, goals = apply_theorem_to_goals env theorems active goals in
+ if ok then
+ let proof =
+ match (fst goals) with
+ | (_, [proof, _, _])::_ -> Some proof
+ | _ -> assert false
+ in
+ ParamodulationSuccess (proof, env)
+ else
+ given_clause_aux dbd env goals theorems passive active
+ else
+ if (passive_is_empty passive) then ParamodulationFailure
+ else given_clause_aux dbd env goals theorems passive active
+
+and given_clause_aux dbd env goals theorems passive active =
+ let time1 = Unix.gettimeofday () in
+
+ let selection_estimate = get_selection_estimate () in
+ let kept = size_of_passive passive in
+ let passive =
+ if !time_limit = 0. || !processed_clauses = 0 then
+ passive
+ else if !elapsed_time > !time_limit then (
+ debug_print (lazy (Printf.sprintf "Time limit (%.2f) reached: %.2f\n"
+ !time_limit !elapsed_time));
+ make_passive [] []
+ ) else if kept > selection_estimate then (
+ debug_print
+ (lazy (Printf.sprintf ("Too many passive equalities: pruning..." ^^
+ "(kept: %d, selection_estimate: %d)\n")
+ kept selection_estimate));
+ prune_passive selection_estimate active passive
+ ) else
+ passive
+ in
+
+ let time2 = Unix.gettimeofday () in
+ passive_maintainance_time := !passive_maintainance_time +. (time2 -. time1);
+
+ kept_clauses := (size_of_passive passive) + (size_of_active active);