Commit ae2ebcd9 authored by Sylvain Dailler's avatar Sylvain Dailler

Adding compute in hypothesis (compute_hyp) and simpl (step).

Both use the same primitive function as compute.
Added a step counting for step by step computation in reduction engine
(for simpl).
parent 26ab9529
......@@ -187,7 +187,7 @@ LIB_MLW = ity expr dexpr pdecl pmodule
LIB_PARSER = ptree glob parser typing lexer
LIB_TRANSFORM = simplify_formula inlining split_goal \
detect_polymorphism reduction_engine compute \
args_wrapper detect_polymorphism reduction_engine compute \
eliminate_definition eliminate_algebraic \
eliminate_inductive eliminate_let eliminate_if \
libencoding discriminate encoding encoding_select \
......@@ -199,7 +199,7 @@ LIB_TRANSFORM = simplify_formula inlining split_goal \
intro_vc_vars_counterexmp prepare_for_counterexmp \
eval_match instantiate_predicate smoke_detector \
prop_curry \
args_wrapper generic_arg_trans_utils case apply \
generic_arg_trans_utils case apply \
ind_itp destruct cut \
eliminate_literal induction induction_pr
......
module Test
use import int.Int
axiom a : 15 = 2 + 3 + 6
goal g: True
end
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<file name="../13_compute_in.mlw">
<theory name="Test" sum="c291ec30c4881b6eb0ae96cce497dffc">
<goal name="g">
<transf name="compute_hyp" arg1="in" arg2="a">
<goal name="g.0">
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
theory Test
goal g10: if true then 1=1 else 3=4
goal g11: let x=1 in x=1
end
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<file name="../14_simpl.mlw" proved="true">
<theory name="Test" proved="true" sum="22cf7419b518c45bfba8210f6a346e58">
<goal name="g10" proved="true">
<transf name="step" arg1="in" arg2="g10">
<goal name="g10.0">
<transf name="step" arg1="in" arg2="g10">
<goal name="g10.0.0">
</goal>
</transf>
</goal>
</transf>
<transf name="step" proved="true" >
<goal name="g10.0" proved="true">
<transf name="step" proved="true" >
</transf>
</goal>
</transf>
</goal>
<goal name="g11" proved="true">
<transf name="step" proved="true" arg1="in" arg2="g11">
<goal name="g11.0" proved="true">
<transf name="step" proved="true" arg1="in" arg2="g11">
<goal name="g11.0.0" proved="true">
<transf name="step" proved="true" >
</transf>
</goal>
</transf>
</goal>
</transf>
<transf name="step" >
<goal name="g11.0">
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
......@@ -11,9 +11,8 @@
open Term
open Decl
open Task
open Theory
open Reduction_engine
open Args_wrapper
let meta_rewrite = Theory.register_meta "rewrite" [Theory.MTprsymbol]
~desc:"Declares@ the@ given@ proposition@ as@ a@ rewrite@ rule."
......@@ -58,42 +57,49 @@ let collect_rules p env km prs t =
)
(create p env km) acc
let normalize_goal p env (prs : Decl.Spr.t) task =
match task with
| Some
{ task_decl =
{ td_node = Decl { d_node = Dprop (Pgoal, pr, f) } };
task_prev = prev;
task_known = km;
} ->
let engine = collect_rules p env km prs task in
let f = normalize ~limit:!compute_max_steps engine f in
begin match f.t_node with
| Ttrue -> []
| _ ->
let d = Decl.create_prop_decl Pgoal pr f in
[Task.add_decl prev d]
end
| _ -> assert false
let normalize_goal_transf p env : 'a Trans.trans =
let tr : 'a Trans.trans =
Trans.on_tagged_pr meta_rewrite
(fun prs -> if p.compute_defs
then Trans.store (normalize_goal p env prs)
else Trans.on_tagged_ls meta_rewrite_def
(fun lss -> let p = { p with compute_def_set = lss } in
Trans.store (normalize_goal p env prs)
))
let normalize_hyp_or_goal ?pr_norm ?step_limit engine : Task.task Trans.tlist =
let step_limit =
if step_limit = None then Some !compute_max_steps else step_limit
in
Trans.decl_l (fun d ->
match d.d_node with
| Dprop (Pgoal, pr, t) when pr_norm = None ->
let t = normalize ?step_limit ~limit:!compute_max_steps engine t in
begin match t.t_node with
| Ttrue -> []
| _ ->
let d = Decl.create_prop_decl Pgoal pr t in
[[d]]
end
| Dprop (k, pr, t) when Opt.fold (fun _ -> pr_equal pr) false pr_norm ->
let t = normalize ?step_limit:step_limit ~limit:!compute_max_steps engine t in
let d = Decl.create_prop_decl k pr t in
[[d]]
| _ -> [[d]]) None
let craft_engine p env prs task =
let km = Task.task_known task in
collect_rules p env km prs task
let collect_rules_trans p env : Reduction_engine.engine Trans.trans =
Trans.on_tagged_pr meta_rewrite
(fun prs -> if p.compute_defs
then Trans.store (craft_engine p env prs)
else Trans.on_tagged_ls meta_rewrite_def
(fun lss -> let p = { p with compute_def_set = lss } in
Trans.store (craft_engine p env prs)
))
let normalize_goal_transf ?pr_norm ?step_limit p env : 'a Trans.trans =
let tr = collect_rules_trans p env in
Trans.on_meta_excl meta_compute_max_steps
(function
| None -> tr
| Some [Theory.MAint n] -> compute_max_steps := n; tr
| None ->
Trans.bind tr (fun engine -> normalize_hyp_or_goal ?pr_norm ?step_limit engine)
| Some [Theory.MAint n] -> compute_max_steps := n;
Trans.bind tr (fun engine -> normalize_hyp_or_goal ?pr_norm ?step_limit engine)
| _ -> assert false)
let normalize_goal_transf_all env =
let p = { compute_defs = true;
compute_builtin = true;
......@@ -116,3 +122,26 @@ let () =
let () =
Trans.register_env_transform_l "compute_specified" normalize_goal_transf_few
~desc:"Rewrite@ goal@ using@ specified@ rules"
let normalize_hyp step_limit pr_norm env =
let p = { compute_defs = true;
compute_builtin = true;
compute_def_set = Term.Mls.empty;
} in
normalize_goal_transf ?pr_norm ?step_limit p env
let () = wrap_and_register ~desc:"experimental: Takes a prsymbol and reduce \
one \"elementary\" step."
"step"
(Topt ("in", Tprsymbol Tenvtrans_l)) (normalize_hyp (Some 1))
let () = wrap_and_register ~desc:"experimental: Same as step except that it \
reduces the given number of steps."
"steps"
(Tint (Topt ("in", Tprsymbol Tenvtrans_l))) (fun n -> normalize_hyp (Some n))
let () = wrap_and_register ~desc:"Performs@ possible@ computations@ in@ given \
hypothesis@ including@ by@ declared@ rewrite@ rules"
"compute_hyp"
(Topt ("in", Tprsymbol Tenvtrans_l)) (normalize_hyp None)
......@@ -249,13 +249,13 @@ type engine =
model([t],[]) = t
model(t1::..::tn::t,f::s) = model(f(t1,..,tn)::t,s)
where f as arity n
where f is of arity n
A given term can be "exploded" into a configuration by reversing the
rules above
During reduction, the terms in the first stack are kept in normal
form. The normalization process can be defined as the repeated
form (value). The normalization process can be defined as the repeated
application of the following rules.
([t],[]) --> t // t is in normal form
......@@ -291,6 +291,11 @@ type config = {
}
(* This global variable is used to approximate a count of the elementary
simplifications that are done during normalization. This is used for
transformation step. *)
let rec_step_limit = ref 0
exception NoMatch of (term * term) option
exception NoMatchpat of (pattern * pattern) option
......@@ -547,9 +552,11 @@ let rec reduce engine c =
begin
match v with
| Term { t_node = Ttrue } ->
incr(rec_step_limit);
{ value_stack = st ;
cont_stack = (Keval(t2,sigma),t_label_copy orig t2) :: rem }
| Term { t_node = Tfalse } ->
incr(rec_step_limit);
{ value_stack = st ;
cont_stack = (Keval(t3,sigma),t_label_copy orig t3) :: rem }
| Term t1 -> begin
......@@ -557,6 +564,7 @@ let rec reduce engine c =
| Tapp (ls,[b0;{ t_node = Tapp (ls1,_) }]) , Tapp(ls2,_) , Tapp(ls3,_)
when ls_equal ls ps_equ && ls_equal ls1 fs_bool_true &&
ls_equal ls2 fs_bool_true && ls_equal ls3 fs_bool_false ->
incr(rec_step_limit);
{ value_stack = Term (t_label_copy orig b0) :: st;
cont_stack = rem }
| _ ->
......@@ -571,6 +579,7 @@ let rec reduce engine c =
end
| [], (Klet _, _) :: _ -> assert false
| t1 :: st, (Klet(v,t2,sigma), orig) :: rem ->
incr(rec_step_limit);
let t1 = term_of_value t1 in
{ value_stack = st;
cont_stack =
......@@ -583,12 +592,14 @@ let rec reduce engine c =
| ([] | [_] | Int _ :: _ | Term _ :: Int _ :: _),
(Kbinop _, _) :: _ -> assert false
| (Term t1) :: (Term t2) :: st, (Kbinop op, orig) :: rem ->
incr(rec_step_limit);
{ value_stack = Term (t_label_copy orig (t_binary_simp op t2 t1)) :: st;
cont_stack = rem;
}
| [], (Knot,_) :: _ -> assert false
| Int _ :: _ , (Knot,_) :: _ -> assert false
| (Term t) :: st, (Knot, orig) :: rem ->
incr(rec_step_limit);
{ value_stack = Term (t_label_copy orig (t_not_simp t)) :: st;
cont_stack = rem;
}
......@@ -640,6 +651,7 @@ and reduce_match st u ~orig tbl sigma cont =
mv'';
Format.eprintf "@]@.";
*)
incr(rec_step_limit);
{ value_stack = st;
cont_stack = (Keval(t,mv''), t_label_copy orig t) :: cont;
}
......@@ -664,6 +676,7 @@ and reduce_eval st t ~orig sigma rem =
begin
try
let t = Mvs.find v sigma in
incr(rec_step_limit);
{ value_stack = Term (t_label_copy orig t) :: st ;
cont_stack = rem;
}
......@@ -882,6 +895,7 @@ and reduce_app_no_equ engine st ls ~orig ty rem_cont =
Format.eprintf "@.";
*)
let mv,rhs = t_subst_types mt mv rhs in
incr(rec_step_limit);
{ value_stack = rem_st;
cont_stack = (Keval(rhs,mv),orig) :: rem_cont;
}
......@@ -957,6 +971,7 @@ and reduce_equ (* engine *) ~orig st v1 v2 cont =
match v1,v2 with
| Int n1, Int n2 ->
let b = to_bool (BigInt.eq n1 n2) in
incr(rec_step_limit);
{ value_stack = Term (t_label_copy orig b) :: st;
cont_stack = cont;
}
......@@ -965,6 +980,7 @@ and reduce_equ (* engine *) ~orig st v1 v2 cont =
try
let n' = big_int_of_const c in
let b = to_bool (BigInt.eq n n') in
incr(rec_step_limit);
{ value_stack = Term (t_label_copy orig b) :: st;
cont_stack = cont;
}
......@@ -981,6 +997,7 @@ and reduce_equ (* engine *) ~orig st v1 v2 cont =
and reduce_term_equ ~orig st t1 t2 cont =
if t_equal t1 t2 then
let () = incr(rec_step_limit) in
{ value_stack = Term (t_label_copy orig t_true) :: st;
cont_stack = cont;
}
......@@ -994,6 +1011,7 @@ and reduce_term_equ ~orig st t1 t2 cont =
BigInt.eq (Number.compute_int_constant i1)
(Number.compute_int_constant i2)
in
incr(rec_step_limit);
{ value_stack = Term (t_label_copy orig (to_bool b)) :: st;
cont_stack = cont;
}
......@@ -1016,6 +1034,7 @@ and reduce_term_equ ~orig st t1 t2 cont =
let sigma,t =
aux Mvs.empty t_true ls1.ls_args tl1 tl2
in
let () = incr(rec_step_limit) in
{ value_stack = st;
cont_stack = (Keval(t,sigma),orig) :: cont;
}
......@@ -1026,6 +1045,7 @@ and reduce_term_equ ~orig st t1 t2 cont =
| Tif (b,{ t_node = Tapp(ls1,_) },{ t_node = Tapp(ls2,_) }) , Tapp(ls3,_)
when ls_equal ls3 fs_bool_true && ls_equal ls1 fs_bool_true &&
ls_equal ls2 fs_bool_false ->
incr(rec_step_limit);
{ value_stack = Term (t_label_copy orig b) :: st;
cont_stack = cont }
| _ -> raise Undetermined
......@@ -1072,7 +1092,8 @@ let rec reconstruct c =
(** iterated reductions *)
let normalize ~limit engine t0 =
let normalize ?step_limit ~limit engine t0 =
rec_step_limit := 0;
let rec many_steps c n =
match c.value_stack, c.cont_stack with
| [Term t], [] -> t
......@@ -1084,9 +1105,18 @@ let normalize ~limit engine t0 =
Pretty.print_term t0 limit;
reconstruct c
end
else
let c = reduce engine c in
many_steps c (n+1)
else begin
match step_limit with
| None ->
let c = reduce engine c in
many_steps c (n+1)
| Some step_limit ->
if !rec_step_limit >= step_limit then
reconstruct c
else
let c = reduce engine c in
many_steps c (n+1)
end
in
let c = { value_stack = [];
cont_stack = [Keval(t0,Mvs.empty),t0] ;
......@@ -1094,11 +1124,6 @@ let normalize ~limit engine t0 =
in
many_steps c 0
(* the rewrite engine *)
let create p env km =
......@@ -1130,7 +1155,9 @@ let extract_rule _km t =
*)
let check_vars acc t1 t2 =
(* check that quantified variables all appear in the lefthand side *)
(* check that quantified variables all appear in the lefthand side
(quantified variables not appearing could be removed and those appearing
on right hand side cannot be guessed during rewriting). *)
let vars_lhs = t_vars t1 in
if Svs.exists (fun vs -> not (Mvs.mem vs vars_lhs)) acc
then raise (NotARewriteRule "lhs should contain all variables");
......@@ -1141,7 +1168,6 @@ let extract_rule _km t =
then raise (NotARewriteRule "lhs should contain all type variables")
in
let rec aux acc t =
match t.t_node with
| Tquant(Tforall,q) ->
......
......@@ -105,14 +105,17 @@ val add_rule : Term.term -> engine -> engine
*)
val normalize : limit:int -> engine -> Term.term -> Term.term
val normalize : ?step_limit:int -> limit:int -> engine -> Term.term -> Term.term
(** [normalize e t] normalizes the term [t] with respect to the engine
[e]
parameter [limit] provides a maximum number of steps for execution.
When limit is reached, the partially reduced term is returned.
parameter [step_limit] provides a maximum number of steps on reductions
that would change the term even after reconstruction.
*)
open Term
exception NoMatch of (term * term) option
......
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