Commit 2d518596 authored by Sylvain Dailler's avatar Sylvain Dailler

apply: add debugging information

parent dc8d92b8
......@@ -38,6 +38,12 @@ let rewrite_subgoals = "rewrite premises"
(* Equality hypothesis generated by using [replace] *)
let replace_hypothesis = "equality hypothesis"
(* Printing substitution *)
let print_subst fmt (mvs: Term.term Mvs.t) =
Format.fprintf fmt "Print subst@.";
Mvs.iter (fun k e -> Format.fprintf fmt "key = %a, term = %a@."
Pretty.print_vs k Pretty.print_term e) mvs
(* Do as intros: introduce all premises of hypothesis pr and return a triple
(goal, list_premises, binded variables) *)
let intros f =
......@@ -161,8 +167,10 @@ let matching_with_terms ~trans_name lv llet_vs left_term right_term withed_terms
raise (Arg_trans_pattern (trans_name, p1, p2))
| Reduction_engine.NoMatch None -> raise (Arg_trans trans_name)
Debug.dprintf debug_matching
"subst after first first_order_matching:\n%a@." print_subst subst;
let subst_ty, subst =
let withed_terms = match withed_terms with None -> [] | Some l -> l in
let withed_terms = Opt.get_def [] withed_terms in
with_terms ~trans_name subst_ty subst lv withed_terms
subst_ty, subst
......@@ -223,11 +231,15 @@ let apply pr withed_terms : Task.task Trans.tlist = (fun task ->
match matching_with_terms ~trans_name:"apply" lv llet_vs nt g withed_terms with
| exception e -> raise e
| subst_ty, subst ->
Debug.dprintf debug_matching "subst after matching with terms:\n%a@."
print_subst subst;
let inst_nt = t_ty_subst subst_ty subst nt in
(* Safety guard: we check that the goal was indeed the instantiated
hypothesis *)
if (Term.t_equal_nt_na inst_nt g) then
let new_goals = generate_new_subgoals ~subst ~subst_ty llet lp in
Debug.dprintf debug_matching "Printing new_goals to introduce:\n%a@."
(Pp.print_list Pp.newline Pretty.print_term) new_goals;
let create_goal h =
let pr = create_prsymbol (gen_ident ?loc:g.t_loc "G") in
Task.add_decl task (create_goal ~expl:apply_subgoals pr h)
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment