+let apply_goal_to_theorems dbd env theorems active goals =
+(* let theorems, _ = theorems in *)
+ let context_hyp, library_thms = theorems in
+ let thm_uris =
+ List.fold_left
+ (fun s (u, _, _, _) -> UriManager.UriSet.add u s)
+ UriManager.UriSet.empty library_thms
+ in
+ let a_goals, p_goals = goals in
+ let goal = List.hd a_goals in
+ let rec aux = function
+ | [] -> false, (a_goals, p_goals)
+ | theorem::tl ->
+ let res = apply_to_goal_conj env [theorem] active goal in
+ match res with
+ | `Ok newgoals ->
+ true, ([newgoals], [])
+ | `No _ ->
+ aux tl
+(* false, (a_goals, p_goals) *)
+ | `GoOn newgoals ->
+ let res, (ag, pg) = aux tl in
+ if res then
+ res, (ag, pg)
+ else
+ let newgoals =
+ List.filter
+ (fun (d, gl) ->
+ (d <= !maxdepth) && (List.length gl) <= !maxwidth)
+ newgoals in
+ let p_goals = newgoals @ pg in
+ let p_goals =
+ List.stable_sort
+ (fun (d1, l1) (d2, l2) -> (List.length l1) - (List.length l2))
+ p_goals
+ in
+ res, (ag, p_goals)
+ in
+ let theorems =
+(* let ty = *)
+(* match goal with *)
+(* | (_, (_, _, t)::_) -> t *)
+(* | _ -> assert false *)
+(* in *)
+(* if CicUtil.is_meta_closed ty then *)
+(* let _ = *)
+(* debug_print (lazy (Printf.sprintf "META CLOSED: %s" (CicPp.ppterm ty))) *)
+(* in *)
+(* let metasenv, context, ugraph = env in *)
+(* let uris = *)
+(* MetadataConstraints.sigmatch ~dbd (MetadataConstraints.signature_of ty) *)
+(* in *)
+(* let uris = List.sort (fun (i, _) (j, _) -> Pervasives.compare i j) uris in *)
+(* let uris = *)
+(* List.filter *)
+(* (fun u -> UriManager.UriSet.mem u thm_uris) (List.map snd uris) *)
+(* in *)
+(* List.map *)
+(* (fun u -> *)
+(* let t = CicUtil.term_of_uri u in *)
+(* let ty, _ = CicTypeChecker.type_of_aux' metasenv context t ugraph in *)
+(* (t, ty, [])) *)
+(* uris *)
+(* else *)
+ List.map (fun (_, t, ty, m) -> (t, ty, m)) library_thms
+ in
+ aux (context_hyp @ 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)
+;;
+
+
+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 =