Skip to content

GitLab

Commit 8704af6f authored by Leon Gondelman's avatar Leon Gondelman
Browse files

induction tactic (wip): tdef, fdef, int_pos

parent 10f315fb
Show whitespace changes
Inline Side-by-side
src/transform/induction.ml
View file @ 8704af6f
......@@ -32,8 +32,26 @@ let debug = Debug.register_flag "induction"
(******* Data type induction principle *********)
(*********************************************************)
(**********************************************************************)
type tyscheme = (pattern * Svs.t) list
let tyscheme_inst f (km : Decl.known_map) x tx =
let inst_branch = (fun (p, vset) ->
t_close_branch p ( Svs.fold (fun v tacc ->
(Term.t_implies (t_subst_single x (t_var v) tx) tacc )) vset tx))
in
t_case (t_var x) (List.map inst_branch ((f km x tx) : tyscheme))
let split_quantifiers x qvl =
let rec aux left = function
| hd :: tl when vs_equal x hd -> List.rev left, tl
| hd :: tl -> aux (hd :: left) tl
| [] -> assert false
in aux [] qvl
let decompose_forall t =
let rec aux qvl_acc t = match t.t_node with
| Tquant (Tforall, qt) ->
......@@ -42,91 +60,97 @@ let decompose_forall t =
in
let qvl, t = aux [] t in (List.fold_right Svs.add qvl Svs.empty), qvl, t
let defn_candidate vs_acc km ls tl qvs =
let arg_candidate = function
| Tvar x when Svs.mem x qvs -> Svs.add x vs_acc
| _ -> vs_acc
in match (find_logic_definition km ls) with
let t_candidates filter km qvs t =
let int_candidate = (fun acc t ->
match t.t_node with
| Tvar x when Svs.mem x qvs && ty_equal x.vs_ty ty_int ->
Svs.add x acc
| _ -> acc)
in
let arg_candidate = (fun acc t ->
match t.t_node with
| Tvar x when Svs.mem x qvs ->
begin match x.vs_ty.ty_node with
| Tyvar _ -> acc
| Tyapp _ -> Svs.add x acc
end
| _ -> acc)
in
let defn_candidate = (fun vs_acc ls tl ->
match (find_logic_definition km ls) with
| Some defn ->
let vs_acc = List.fold_left int_candidate vs_acc tl in
begin match ls_defn_decrease defn with
| [i] -> arg_candidate (List.nth tl i).t_node
| [i] -> arg_candidate vs_acc (List.nth tl i)
| _ -> vs_acc
end
| None -> vs_acc
let t_candidates km qvs t =
| None -> vs_acc)
in
let rec t_candidate vs_acc t =
let vs_acc = match t.t_node with
| Tapp (ls, tl) -> defn_candidate vs_acc km ls tl qvs
| Tapp (ls, tl) -> defn_candidate vs_acc ls tl
| _ -> vs_acc
in t_fold t_candidate vs_acc t
in t_candidate Svs.empty t
in Svs.filter filter (t_candidate Svs.empty t)
let heuristic_svs vset = Svs.choose vset
let split_quantifiers x qvl =
let rec aux left = function
| hd :: tl when vs_equal x hd -> List.rev left, tl
| hd :: tl -> aux (hd :: left) tl
| [] -> assert false
in aux [] qvl
(*
let heuristic_forall_close (qvl1, qvl2) t =
t_forall_close (qvl1 @ qvl2) [] t
*) (*fix me qvl2 generalized *)
(**********************************************************************)
let filter_tydef v = not (ty_equal v.vs_ty ty_int)
(* Decl.known_map -> Term.vsymbol -> Term.term -> tyscheme *)
let tyscheme_genvt km x (_t : Term.term) =
let tyscheme_vsty km x (_t : Term.term) =
let ts,ty = match x.vs_ty.ty_node with
| Tyapp _ when ty_equal x.vs_ty ty_int -> assert false
| Tyvar _ -> assert false
| Tyapp (ts, _) -> ts, ty_app ts (List.map ty_var ts.ts_args)
| Tyvar _ -> assert false in
let sigma = ty_match Mtv.empty ty x.vs_ty
in
let ty_str = (fun ty ->
let sigma = ty_match Mtv.empty ty x.vs_ty in
let ty_str ty =
let s = match ty.ty_node with
| Tyapp (ts, _) -> ts.ts_name.id_string
| Tyvar tv -> tv.tv_name.id_string
in if s = "" then "x" else String.make 1 s.[0])
in if s = "" then "x" else String.make 1 s.[0]
in
let ty_vs = (fun ty ->
let ty_vs ty =
let ty = ty_inst sigma ty in
Term.create_vsymbol (Ident.id_fresh (ty_str ty)) ty)
Term.create_vsymbol (Ident.id_fresh (ty_str ty)) ty
in
let tyscheme_constructor = (fun (ls, _) ->
let tyscheme_constructor (ls, _) =
let vlst = List.map ty_vs ls.ls_args in
let plst = List.map pat_var vlst in
let vset = List.fold_left
(fun s v ->
if ty_equal x.vs_ty v.vs_ty then Svs.add v s else s)
Svs.empty vlst
in pat_app ls plst x.vs_ty, vset)
in pat_app ls plst x.vs_ty, vset
in
let cl = find_constructors km ts in
((List.map tyscheme_constructor cl) : tyscheme)
let tyscheme_genfd = tyscheme_genvt
let tyscheme_inst f (km : Decl.known_map) x tx =
let inst_branch = (fun (p, vset) ->
t_close_branch p ( Svs.fold (fun v tacc ->
(Term.t_implies (t_subst_single x (t_var v) tx) tacc )) vset tx))
in
t_case (t_var x) (List.map inst_branch ((f km x tx) : tyscheme))
let induction km t0 =
let qvs, qvl, t = decompose_forall t0 in
let vset = t_candidates km qvs t in
if Svs.is_empty vset
then [t0]
let vset = t_candidates filter_tydef km qvs t in
if Svs.is_empty vset then [t0]
else
let x = Svs.choose vset in
let _qvl1, _qvl2 = split_quantifiers x qvl in
let tcase = tyscheme_inst tyscheme_genvt km x t in
let tcase = t_forall_close qvl [] tcase in
let x = heuristic_svs vset in
let qvl1, qvl2 = split_quantifiers x qvl in
let t = t_forall_close qvl2 [] t in
let tcase = tyscheme_inst tyscheme_vsty km x t in
let tcase = t_forall_close [x] [] tcase in
let tcase = t_forall_close qvl1 [] tcase in
if Debug.test_flag debug then
(Format.printf "Old Task: %a \n@." Pretty.print_term t0;
Format.printf "New Task: %a \n@." Pretty.print_term tcase);
[t_forall_close qvl [] tcase]
[tcase]
let induction = function
......@@ -136,107 +160,100 @@ let induction = function
List.map (add_prop_decl prev Pgoal pr) (induction km f)
| _ -> assert false
let () = Trans.register_transform_l "induction" (Trans.store induction)
let () =
Trans.register_transform_l "induction_ty_vsty" (Trans.store induction)
(*
(**********************************************************************)
let t_defn_candidates km vs t =
let defn_collect = (fun acc ls tl ->
match (find_logic_definition km ls) with
| Some defn ->
begin match ls_defn_decrease defn with
| [i] ->
begin match (List.nth tl i).t_node with
| Tvar x when vs_equal x vs -> Mls.add ls (i, defn) acc
| _ -> acc
end
| _ -> acc
end
| None -> acc)
in
let rec t_collect = (fun acc t ->
let acc = match t.t_node with
| Tapp (ls, tl) -> defn_collect acc ls tl
| _ -> acc
in t_fold t_collect acc t)
in t_collect (Mls.empty) t
type ind_info =
{tact : string ;
cands : Term.Svs.t;
ind_v : Term.vsymbol;
ind_ty : ty;
itsk : Term.term;
pred : Term.term;
sg : Term.term;
}
let show_info i =
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_vsty i.ind_v;
Format.printf "Induction on type: %a @." Pretty.print_ty i.ind_ty;
Format.printf "Induction predicate: %a @." Pretty.print_term i.pred;
Format.printf "Induction sub-task: %a \n@." Pretty.print_term i.sg
type htree = | Snode of (vsymbol * pattern * htree) list
| Sleaf of Svs.t
let print_ty_skm skm =
List.iter
(fun (p,svs) ->
Format.printf "@[ %a : @]" Pretty.print_pat p;
Svs.iter (Format.printf "%a " Pretty.print_vs) svs;
Format.printf "@.")
skm
let empty = Sleaf Svs.empty
let defn_htree _km fls x i t =
let rec t_htree acc t =
match t.t_node with
| Tcase ({t_node = (Tvar y)}, bl) when ty_equal x.vs_ty y.vs_ty ->
case_htree acc y bl
| Tapp (ls, tl) when ls_equal ls fls ->
begin
match (List.nth tl i).t_node with
| Tvar y -> push acc (Sleaf (Svs.add y Svs.empty))
| _ -> assert false
end
| Tapp (_, tl) -> app_htree acc tl
| _ -> acc
let indv_ty x = match x.vs_ty.ty_node with
| Tyapp (ts, _) -> ts, ty_app ts (List.map ty_var ts.ts_args)
| Tyvar _ -> assert false
and app_htree acc tl =
List.fold_left (fun acc t -> t_htree acc t ) acc tl
let heuristic vss =
let x = Svs.choose vss in
let ts, ty = indv_ty x in
x, ts, ty
and case_htree acc y bl =
let ptl = List.map (fun b ->
let (p,t) = t_open_branch b in (p, t)) bl in
let sml = List.map (fun (p,t) -> (y, p, t_htree empty t)) ptl in
push acc (Snode sml)
let name_from_type ty =
let s = match ty.ty_node with
| Tyapp (ts, _) -> ts.ts_name.id_string
| Tyvar tv -> tv.tv_name.id_string
and push acc sm = match acc with
| Snode l -> Snode (List.map (fun (x,p,s) -> (x,p, push s sm)) l)
| Sleaf svs0 -> match sm with
| Snode sml ->
Snode ((List.map (fun (x,p,s) ->
(x,p, push (Sleaf svs0) s))) sml)
| Sleaf svs1 -> Sleaf (Svs.union svs0 svs1)
in
if s = "" then "x" else String.make 1 s.[0]
t_htree (Sleaf Svs.empty) t
let htree_tyscheme _ht = ([] : tyscheme)
(* Decl.known_map -> Term.vsymbol -> Term.term -> tyscheme *)
let tyscheme_fdef_one km x t =
let (ls, (i, _defn)) = Mls.choose (t_defn_candidates km x t) in
let ht = defn_htree km ls x i t in
htree_tyscheme ht
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
let induction km t0 =
let qvs, qvl, t = decompose_forall t0 in
let vset = t_candidates (fun _ -> true) km qvs t in
if Svs.is_empty vset
then [t0]
else
let x = heuristic_svs vset in
let qvl1, qvl2 = split_quantifiers x qvl in
let p = t_forall_close qvl2 [] t in
let make_case (ls, _) =
let create_var ty =
let ty = ty_inst sigma ty in
let id = Ident.id_fresh (name_from_type ty) in
Term.create_vsymbol id ty
in
let ind_vl = List.map create_var ls.ls_args in
let ind_tl = List.map t_var ind_vl in
let goal = t_subst_single x (t_app ls ind_tl (Some x.vs_ty)) p in
let goal = List.fold_left
(fun goal vs ->
if ty_equal vs.vs_ty x.vs_ty
then Term.t_implies (t_subst_single x (t_var vs) p) goal
else goal) goal ind_vl
in
let goal = t_forall_close (qvl1 @ ind_vl) [] goal in
let t = t_forall_close qvl2 [] t in
let t = tyscheme_inst tyscheme_fdef_one km x t in
let t = t_forall_close [x] [] t in
let t = t_forall_close qvl1 [] t in
if Debug.test_flag debug then
begin
let data = {
tact = ""; cands = vs; ind_v = x;
ind_ty = ty;
itsk = t_forall_close qvl [] t ;
pred = p; sg = goal}
in show_info data
end; goal
in
let cl = find_constructors km ts in
List.map make_case cl
let induction km t0 =
let qvs, _qvl, t = decompose_forall t0 in
let vs = t_candidates km qvs t in
if Svs.is_empty vs then [t0] else
let x, _ts, _ty = heuristic vs in
let () = print_ty_skm (tyscheme_genvt km x t) in
[t0]
(* make_induction vs km qvl t *)
(Format.printf "Old Task: %a \n@." Pretty.print_term t0;
Format.printf "New Task: %a \n@." Pretty.print_term t);
[t]
let induction = function
| Some { task_decl = { td_node = Decl { d_node = Dprop (Pgoal, pr, f) } };
......@@ -245,87 +262,87 @@ let induction = function
List.map (add_prop_decl prev Pgoal pr) (induction km f)
| _ -> assert false
let () = Trans.register_transform_l "induction" (Trans.store induction)
*)
(*********************************************************)
(******* Induction tactic on function definition *********)
(*********************************************************)
type scheme = | Snode of (vsymbol * pattern * scheme) list
| Sleaf of Svs.t
let empty = Sleaf Svs.empty
let () =
Trans.register_transform_l "induction_ty_fdef" (Trans.store induction)
(**********************************************************************)
let filter_int v = ty_equal v.vs_ty ty_int
let int_strong_induction (le_int,lt_int) x t =
let k = Term.create_vsymbol (Ident.id_clone x.vs_name) ty_int in
(* 0 <= k < x *)
let ineq = t_and (ps_app le_int [t_int_const "0"; t_var k])
(ps_app lt_int [t_var k; t_var x]) in
(* forall k. 0 <= k < x -> P[x <- k] *)
let ih =
t_forall_close [k] [] (t_implies ineq (t_subst_single x (t_var k) t)) in
t_forall_close [x] [] (t_implies ih t)
let induction km (le_int,lt_int) t0 =
let qvs, qvl, t = decompose_forall t0 in
let vset = t_candidates filter_int km qvs t in
if Svs.is_empty vset
then [t0]
else begin
let x = heuristic_svs vset in
let qvl1, qvl2 = split_quantifiers x qvl in
let t = t_forall_close qvl2 [] t in
let t = int_strong_induction (le_int,lt_int) x t in
let t = t_forall_close qvl1 [] t in
if Debug.test_flag debug then
(Format.printf "Old Task: %a \n@." Pretty.print_term t0;
Format.printf "New Task: %a \n@." Pretty.print_term t);
[t]
end
let rec print_scheme fmt = function
| Snode l ->
Format.fprintf fmt "Snode@[<hov 2>[";
List.iter (fun (x,p,s) ->
Format.printf "@[(%a,@ %a,@ %a)@];@ "
Pretty.print_vs x Pretty.print_pat p print_scheme s)
l;
Format.fprintf fmt "@]]"
| Sleaf s ->
if Svs.cardinal s = 0 then
Format.fprintf fmt "Sleaf .. "
else
( Format.fprintf fmt "Sleaf ";
Svs.iter (fun x -> Format.printf "%a " Pretty.print_vs x) s )
let make_scheme _km fls x i t =
let rec t_scheme acc t =
match t.t_node with
| Tcase ({t_node = (Tvar y)}, bl) when ty_equal x.vs_ty y.vs_ty ->
case_scheme acc y bl
| Tapp (ls, tl) when ls_equal ls fls ->
let induction th_int = function
| Some
{ task_decl = { td_node = Decl { d_node = Dprop (Pgoal, pr, f) } };
task_prev = prev; task_known = km } as t ->
begin
match (List.nth tl i).t_node with
| Tvar y -> push acc (Sleaf (Svs.add y Svs.empty))
try
let le_int = ns_find_ls th_int.th_export ["infix <="] in
let lt_int = ns_find_ls th_int.th_export ["infix <"] in
if not (Mid.mem le_int.ls_name km) then raise Exit;
List.map (add_prop_decl prev Pgoal pr)
(induction km (le_int, lt_int) f)
with Exit -> [t] end
| _ -> assert false
end
| Tapp (_, tl) -> app_scheme acc tl
| _ -> acc
and app_scheme acc tl =
List.fold_left (fun acc t -> t_scheme acc t ) acc tl
and case_scheme acc y bl =
let ptl = List.map (fun b -> let (p,t) = t_open_branch b in (p, t)) bl in
let sml = List.map (fun (p,t) -> (y, p, t_scheme empty t)) ptl in
push acc (Snode sml)
and push acc sm = match acc with
| Snode l -> Snode (List.map (fun (x,p,s) -> (x,p, push s sm)) l)
| Sleaf svs0 -> match sm with
| Snode sml ->
Snode ((List.map (fun (x,p,s) -> (x,p, push (Sleaf svs0) s))) sml)
| Sleaf svs1 -> Sleaf (Svs.union svs0 svs1)
in
t_scheme (Sleaf Svs.empty) t
let () =
Trans.register_env_transform_l "induction_int"
(fun env ->
let th_int = Env.find_theory env ["int"] "Int" in
Trans.store (induction th_int))
(**********************************************************************)
(*TODO
1° km x t -> htree (optimized)
2° htree -> tyscheme
3° defn list -> htree
4° predicate induction
4° benchmark
4° labels à la {induction j} {induction false} {induction_int}
5° common tactic
6° mutual recursion
7° lexicographic orders
8° termination criterium
9° warnings
10° indentation
*)
(*********************************************************)
(******************* ATTIC **********************)
(*
let t_iter_scheme km t =
let ty_cl ts =
......@@ -411,8 +428,6 @@ let t_iter_compile_first km t =
in
Format.printf "%a \n @." Pretty.print_term (t_patc t)
(*
t_tcase (acc,n) (t, tbl)
| _ -> t
......@@ -461,6 +476,75 @@ t_tcase (acc,n) (t, tbl)
*)
(*
let functional_induction km t0 =
let qvs, _qvl, t = decompose_forall t0 in
let vmap = t_collect_data km qvs t in
let x, lmap = Mvs.choose vmap in
let (ls, (i, defn)) = Mls.choose lmap in
let (_,t) = open_ls_defn defn in
Format.printf "%a@." print_scheme (make_scheme km ls x i t);
[t0]
let _ = Mls.iter (fun _ls (_i,defn) ->
let (_,t) = open_ls_defn defn in t_iter_compile_first km t) lmap in
if (Mvs.is_empty vmap)
then
[t0]
else
[t0]
*)
(*
let functional_induction = function
| Some { task_decl = { td_node = Decl { d_node = Dprop (Pgoal, pr, f) } };
task_prev = prev;
task_known = km } ->
List.map (add_prop_decl prev Pgoal pr) (functional_induction km f)
| _ -> assert false
let () = Trans.register_transform_l
"induction_on_function_definition"
(Trans.store functional_induction)
*)
(*
Local Variables:
compile-command: "unset LANG; make -C ../.."
End:
*)
(*
let rec print_scheme fmt = function
| Snode l ->
Format.fprintf fmt "Snode@[<hov 2>[";
List.iter (fun (x,p,s) ->
Format.printf "@[(%a,@ %a,@ %a)@];@ "
Pretty.print_vs x Pretty.print_pat p print_scheme s)
l;
Format.fprintf fmt "@]]"
| Sleaf s ->
if Svs.cardinal s = 0 then
Format.fprintf fmt "Sleaf .. "
else
( Format.fprintf fmt "Sleaf ";
Svs.iter (fun x -> Format.printf "%a " Pretty.print_vs x) s )
let t_collect_data km qvs t =
let defn_collect_data acc ls tl =
......@@ -492,50 +576,124 @@ let t_collect_data km qvs t =
in t_fold t_collect acc t
in t_collect (Mvs.empty) t
*)
let functional_induction km t0 =
let qvs, _qvl, t = decompose_forall t0 in
let vmap = t_collect_data km qvs t in
let x, lmap = Mvs.choose vmap in
let (ls, (i, defn)) = Mls.choose lmap in
let (_,t) = open_ls_defn defn in
Format.printf "%a@." print_scheme (make_scheme km ls x i t);
[t0]
(*
let _ = Mls.iter (fun _ls (_i,defn) ->
let (_,t) = open_ls_defn defn in t_iter_compile_first km t) lmap in
if (Mvs.is_empty vmap)
then
[t0]
else
[t0]
*)
type ind_info =
{tact : string ;
cands : Term.Svs.t;
ind_v : Term.vsymbol;
ind_ty : ty;