let changed', goal = demodulate passive_table goal in
(changed || changed'), goal
in
-(* let _ = *)
-(* let p, _, t = goal in *)
-(* debug_print *)
-(* (lazy *)
-(* (Printf.sprintf "Goal after demodulation: %s, %s" *)
-(* (string_of_proof p) (CicPp.ppterm t))) *)
-(* in *)
+ let _ =
+ let p, _, t = goal in
+ debug_print
+ (lazy
+ (Printf.sprintf "Goal after demodulation: %s, %s"
+ (string_of_proof p) (CicPp.ppterm t)))
+ in
changed, goal
;;
let eqterm =
C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right] in
let gproof, gmetas, gterm = goal in
+ debug_print
+ (lazy
+ (Printf.sprintf "APPLY EQUALITY TO GOAL: %s, %s"
+ (string_of_equality equality) (CicPp.ppterm gterm)));
try
let subst, metasenv', _ =
let menv = metasenv @ metas @ gmetas in
;;
-let apply_to_goal env theorems active goal =
+let apply_to_goal env theorems ?passive active goal =
let metasenv, context, ugraph = env in
let proof, metas, term = goal in
debug_print
in
let r, s, l =
if Inference.term_is_equality term then
- let rec appleq = function
+ let _ = debug_print (lazy "OK, is equality!!") in
+ let rec appleq_a = function
| [] -> false, [], []
| (Positive, equality)::tl ->
let ok, s, newproof = apply_equality_to_goal env equality goal in
- if ok then true, s, [newproof, metas, term] else appleq tl
- | _::tl -> appleq tl
+ if ok then true, s, [newproof, metas, term] else appleq_a tl
+ | _::tl -> appleq_a tl
+ in
+ let rec appleq_p = function
+ | [] -> false, [], []
+ | equality::tl ->
+ let ok, s, newproof = apply_equality_to_goal env equality goal in
+ if ok then true, s, [newproof, metas, term] else appleq_p tl
in
let al, _ = active in
- appleq al
+ match passive with
+ | None -> appleq_a al
+ | Some (_, (pl, _), _) ->
+ let r, s, l = appleq_a al in if r then r, s, l else appleq_p pl
else
false, [], []
in
;;
-let apply_to_goal_conj env theorems active (depth, goals) =
+let apply_to_goal_conj env theorems ?passive active (depth, goals) =
let rec aux = function
| goal::tl ->
let propagate_subst subst (proof, metas, term) =
ProofBlock (subst @ s, u, nty, t, pe, p)
in (repl proof, metas, term)
in
- let r = apply_to_goal env theorems active goal in (
+ let r = apply_to_goal env theorems ?passive active goal in (
match r with
| `No -> `No (depth, goals)
| `GoOn sl (* (subst, gl) *) ->
;;
-let apply_goal_to_theorems dbd env theorems active goals =
+let apply_goal_to_theorems dbd env theorems ?passive active goals =
(* let theorems, _ = theorems in *)
let context_hyp, library_thms = theorems in
let thm_uris =
let rec aux = function
| [] -> false, (a_goals, p_goals)
| theorem::tl ->
- let res = apply_to_goal_conj env [theorem] active goal in
+ let res = apply_to_goal_conj env [theorem] ?passive active goal in
match res with
| `Ok newgoals ->
true, ([newgoals], [])
(Printf.sprintf "\ngoals = \nactive\n%s\npassive\n%s\n"
(print_goals (fst goals)) (print_goals (snd goals))))
in
- let ok, goals = apply_goal_to_theorems dbd env theorems active goals in
+ let ok, goals =
+ apply_goal_to_theorems dbd env theorems ~passive active goals
+ in
if ok then
let proof =
match (fst goals) with