Commit 4703fddb authored by Leon Gondelman's avatar Leon Gondelman

induction tactic (wip)

parent 0e668c54
......@@ -27,30 +27,22 @@ open Task
let debug = Debug.register_flag "induction"
(*
let print_candidates vs =
Svs.iter (fun x -> Format.printf ": %a" Pretty.print_vs x) vs
(*if Debug.test_flag debug then
Format.printf "\n Ind_var type: %a @ \n" Pretty.print_ty ty; *)
type ind_info =
{tact : string ;
cands : Term.Svs.t;
ind_v : Term.vsymbol;
itsk : Term.term;
pred : Term.term;
shma : Term.term list;
sg : Term.term;
}
let show_info i =
Printf.printf "Induction tactic: \n"
(*Format.printf "Init_task: %a \n" Pretty.print_term i.itsk*)
(* if Debug.test_flag debug then
begin
Format.printf "Init_task: %a @ \n" Pretty.print_term init_t
end; *)
Format.printf "\nInduction tactic: %s @." i.tact;
Format.printf "Initial task: %a @.Candidates: " Pretty.print_term i.itsk;
Svs.iter (fun x -> Format.printf "%a @." Pretty.print_vs x) i.cands;
Format.printf "Induction on variable: %a @." Pretty.print_vs i.ind_v;
Format.printf "Induction predicate: %a @." Pretty.print_term i.pred;
Format.printf "Induction sub-task: %a \n@." Pretty.print_term i.sg
(* if Debug.test_flag debug then begin
print_string "sigma_inst: ";
......@@ -58,23 +50,6 @@ let show_info i =
Pretty.print_tv x Pretty.print_ty tx ) sigma
end; *)
(*if Debug.test_flag debug then
Format.printf "Ind_pred: @ %a @ \n" Pretty.print_term p; *)
(*if Debug.test_flag debug then
Format.printf "Induction sub-task: %a @ \n" Pretty.print_term goal;*)
(*if Debug.test_flag debug then
begin
let data = {
tact = ""; cands = vs; ind_v = x; itsk = init_t;
pred = p; shma = []}
in if data = data then () else ()
end; *)
*)
let decompose_forall t =
let rec aux qvl_acc t = match t.t_node with
| Tquant (Tforall, qt) ->
......@@ -91,7 +66,7 @@ let defn_candidate vs_acc km ls tl qvs =
| Some defn ->
begin match ls_defn_decrease defn with
| [i] -> arg_candidate (List.nth tl i).t_node
| _ -> vs_acc
| _ -> vs_acc
end
| None -> vs_acc
......@@ -150,11 +125,17 @@ let make_induction vs km qvl t =
else goal) goal ind_vl
in
let goal = t_forall_close (qvl1 @ ind_vl) [] goal in
goal
if Debug.test_flag debug then
begin
let data = {
tact = ""; cands = vs; ind_v = x;
itsk = t_forall_close qvl [] t ;
pred = p; sg = goal}
in show_info data
end; goal
in
let _ = t_forall_close qvl [] t in
let cl = find_constructors km ts in
List.map make_case cl
List.map make_case cl
let induction km t0 =
......@@ -236,7 +217,6 @@ let make_induction vs km qvl t =
*)
let make_induction vs km qvl t =
let x, ts, ty = heuristic vs in
let sigma = ty_match Mtv.empty ty x.vs_ty in
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment