Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Open sidebar
Why3
why3
Commits
3e70b6b9
Commit
3e70b6b9
authored
Jun 06, 2012
by
Leon Gondelman
Browse files
induction tactic (under construction) : minor changes
parent
20dda6fc
Changes
1
Hide whitespace changes
Inline
Sidebyside
Showing
1 changed file
with
90 additions
and
16 deletions
+90
16
src/transform/induction.ml
src/transform/induction.ml
+90
16
No files found.
src/transform/induction.ml
View file @
3e70b6b9
...
...
@@ 24,28 +24,91 @@ open Decl
open
Theory
open
Task
let
rec
decompose_forall
vl
f
=
match
f
.
t_node
with
let
decompose_forall
t
=
let
rec
aux
qvl_acc
t
=
match
t
.
t_node
with

Tquant
(
Tforall
,
q
)
>
let
ql
,
_
,
f
=
t_open_quant
q
in
decompose_forall
(
vl
@
ql
)
f

_
>
vl
,
f
let
qvl
,
_
,
t
=
t_open_quant
q
in
aux
(
qvl_acc
@
qvl
)
t

_
>
qvl_acc
,
t
in
let
qvl
,
t
=
aux
[]
t
in
(
List
.
fold_right
Svs
.
add
qvl
Svs
.
empty
)
,
qvl
,
t
let
t_candidates
km
qvs
t
=
let
rec
recf_candidate
vs_acc
t
=
let
vs_acc
=
match
t
.
t_node
with

Tapp
(
ls
,
tl
)
>
begin
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
Svs
.
mem
x
qvs
>
Svs
.
add
x
vs_acc

_
>
vs_acc
(*here rec call *)
end

_
>
vs_acc
end

None
>
vs_acc
end

_
>
vs_acc
in
t_fold
recf_candidate
vs_acc
t
in
recf_candidate
Svs
.
empty
t
let
print_candidates
vs
=
Svs
.
iter
(
fun
x
>
Format
.
eprintf
"candidate %a@."
Pretty
.
print_vs
x
)
vs
let
heuristic
=
Svs
.
choose
(* IMPROVE ME *)
let
make_induction
_km
qvl
_x
f
=
[
t_forall_close
qvl
[]
f
]
let
make_induction
vs
_km
qvl
t
=
let
_x
=
heuristic
vs
in
[
t_forall_close
qvl
[]
t
]
(* Term.Svs.t > Term.term > Term.Svs.t *)
let
induction
km
t0
=
let
qvs
,
qvl
,
t
=
decompose_forall
t0
in
let
vs
=
t_candidates
km
qvs
t
in
print_candidates
vs
;
if
Svs
.
is_empty
vs
then
[
t0
]
else
make_induction
vs
km
qvl
t
(* Task.task_hd option > Task.task list *)
let
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
)
(
induction
km
f
)

_
>
assert
false
let
()
=
Trans
.
register_transform_l
"induction"
(
Trans
.
store
induction
)
(***************************************************************************)
(*
(* Term.vsymbol list > Term.term > Term.vsymbol list * Term.term *)
let rec decompose_forall qvl_acc f = match f.t_node with
 Tquant (Tforall, q) >
let qvl, _, f = t_open_quant q in
decompose_forall (qvl_acc @ qvl) f
 _ > qvl_acc, f
(* Term.Svs.t > Term.term > Term.Svs.t *)
let induction km f0 =
let
qvl
,
f
=
decompose_forall
[]
f0
in
let
qvs
=
List
.
fold_right
Svs
.
add
qvl
Svs
.
empty
in
let qvs, qvl, f = decompose_forall [] f0 in
let rec candidate vs f =
let vs = match f.t_node with
 Tapp (ls, tl) > begin 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 Svs.mem x qvs > Svs.add x vs

_
>
vs
 _ > vs
(*here rec call *)
end
 _ > vs
end
...
...
@@ 55,16 +118,27 @@ let induction km f0 =
in
t_fold candidate vs f
in
let
candidates
=
candidate
Svs
.
empty
f
in
Svs
.
iter
(
fun
x
>
Format
.
eprintf
"candidate %a@."
Pretty
.
print_vs
x
)
candidates
;
if
Svs
.
is_empty
candidates
then
[
f0
]
else
let
x
=
heuristic
candidates
in
make_induction
km
qvl
x
f
let candidates =
candidate Svs.empty f in print_vs candidates;
if Svs.is_empty candidates
then [f0]
else make_induction km qvl f candidates
(* Task.task_hd option > Task.task list *)
(* recolle les déclarations initiales du but transformé *)
let induction = function
 Some { task_decl = { td_node = Decl { d_node = Dprop (Pgoal, pr, f) } };
task_known
=
km
;
task_prev
=
prev
}
>
task_prev = prev;
task_known = km } >
List.map (add_prop_decl prev Pgoal pr) (induction km f)
 _ > assert false
let () = Trans.register_transform_l "induction" (Trans.store induction)
*)
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment