Skip to content

GitLab

why3
why3
Commit 11e3593d authored by MARCHE Claude's avatar MARCHE Claude
Browse files
Options

trans compute: ressurected builtins

parent 41bd968f
Hide whitespace changes
Inline Side-by-side
Showing with 244 additions and 53 deletions
src/transform/compute.ml
View file @ 11e3593d
......@@ -344,24 +344,22 @@ let collect_rule_decl prs e d =
Reduction_engine.add_rule t e
else e
let collect_rules prs t =
let collect_rules env km prs t =
Task.task_fold
(fun e td -> match td.Theory.td_node with
| Theory.Decl d -> collect_rule_decl prs e d
| _ -> e)
(Reduction_engine.create ()) t
(Reduction_engine.create env km) t
let normalize_goal (prs : Decl.Spr.t) task =
let engine = collect_rules prs task in
let normalize_goal 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;
} ->
(*
get_builtins env;
*)
let engine = collect_rules env km prs task in
let f = Reduction_engine.normalize engine f in
begin match f.t_node with
| Ttrue -> []
......@@ -375,8 +373,8 @@ let normalize_goal (prs : Decl.Spr.t) task =
let meta = Theory.register_meta "rewrite" [Theory.MTprsymbol]
~desc:"Declares@ the@ given@ prop@ as@ a@ rewrite@ rule."
let normalize_transf =
Trans.on_tagged_pr meta (fun prs -> Trans.store (normalize_goal prs))
let normalize_transf env =
Trans.on_tagged_pr meta (fun prs -> Trans.store (normalize_goal env prs))
let () = Trans.register_transform_l "compute_in_goal" normalize_transf
let () = Trans.register_env_transform_l "compute_in_goal" normalize_transf
~desc:"Normalize@ terms@ with@ respect@ to@ rewrite@ rules@ declared as metas"
src/transform/reduction_engine.ml
View file @ 11e3593d
open Term
(* {2 builtin symbols} *)
let builtins = Hls.create 17
let ls_minus = ref ps_equ (* temporary *)
(* all builtin functions *)
exception Undetermined
let const_equality c1 c2 =
match c1,c2 with
| Number.ConstInt i1, Number.ConstInt i2 ->
BigInt.eq (Number.compute_int i1) (Number.compute_int i2)
| _ -> raise Undetermined
let value_equality t1 t2 =
match (t1.t_node,t2.t_node) with
| Tconst c1, Tconst c2 -> const_equality c1 c2
| _ -> raise Undetermined
let to_bool b = if b then t_true else t_false
let eval_equ _ls l _ty =
match l with
| [t1;t2] ->
begin
try to_bool (value_equality t1 t2)
with Undetermined -> t_equ t1 t2
end
| _ -> assert false
let eval_true _ls _l _ty = t_true
let eval_false _ls _l _ty = t_false
exception NotNum
let big_int_of_const c =
match c with
| Number.ConstInt i -> Number.compute_int i
| _ -> raise NotNum
let const_of_big_int n =
t_const (Number.ConstInt (Number.int_const_dec (BigInt.to_string n)))
let eval_int_op op ls l ty =
match l with
| [{t_node = Tconst c1};{t_node = Tconst c2}] ->
begin
try const_of_big_int (op (big_int_of_const c1) (big_int_of_const c2))
with NotNum | Division_by_zero ->
t_app ls l ty
end
| _ -> t_app ls l ty
let built_in_theories =
[ ["bool"],"Bool", [],
[ "True", None, eval_true ;
"False", None, eval_false ;
] ;
["int"],"Int", [],
[ "infix +", None, eval_int_op BigInt.add;
"infix -", None, eval_int_op BigInt.sub;
"infix *", None, eval_int_op BigInt.mul;
(*
"prefix -", Some ls_minus, eval_int_uop BigInt.minus;
"infix <", None, eval_int_rel BigInt.lt;
"infix <=", None, eval_int_rel BigInt.le;
"infix >", None, eval_int_rel BigInt.gt;
"infix >=", None, eval_int_rel BigInt.ge;
*)
] ;
(*
["int"],"MinMax", [],
[ "min", None, eval_int_op BigInt.min;
"max", None, eval_int_op BigInt.max;
] ;
["int"],"ComputerDivision", [],
[ "div", None, eval_int_op BigInt.computer_div;
"mod", None, eval_int_op BigInt.computer_mod;
] ;
["int"],"EuclideanDivision", [],
[ "div", None, eval_int_op BigInt.euclidean_div;
"mod", None, eval_int_op BigInt.euclidean_mod;
] ;
["map"],"Map", ["map", builtin_map_type],
[ "const", Some ls_map_const, eval_map_const;
"get", Some ls_map_get, eval_map_get;
"set", Some ls_map_set, eval_map_set;
] ;
*)
]
let add_builtin_th env (l,n,t,d) =
try
let th = Env.find_theory env l n in
List.iter
(fun (id,r) ->
let ts = Theory.ns_find_ts th.Theory.th_export [id] in
r ts)
t;
List.iter
(fun (id,r,f) ->
let ls = Theory.ns_find_ls th.Theory.th_export [id] in
Hls.add builtins ls f;
match r with
| None -> ()
| Some r -> r := ls)
d
with Not_found ->
Format.eprintf "[Compute] theory %s not found@." n
let get_builtins env =
Hls.clear builtins;
Hls.add builtins ps_equ eval_equ;
List.iter (add_builtin_th env) built_in_theories
(* {2 the reduction machine} *)
type rule = vsymbol list * term list * term
type engine = rule list Mls.t
type engine =
{ known_map : Decl.decl Ident.Mid.t;
rules : rule list Mls.t;
}
(*
......@@ -120,8 +253,6 @@ let first_order_matching (vars : Svs.t) (largs : term list)
exception Undetermined
let rec matching sigma t p =
match p.pat_node with
| Pwild -> sigma
......@@ -187,7 +318,7 @@ let rec reduce engine c =
cont_stack = rem;
}
| st, Kapp(ls,ty) :: rem ->
reduce_app st ls ty rem
reduce_app engine st ls ty rem
| [], Keps _ :: _ -> assert false
| Term t :: st, Keps v :: rem ->
{ value_stack = Term (t_eps_close v t) :: st;
......@@ -268,7 +399,7 @@ and reduce_eval st t sigma rem =
cont_stack = rem;
}
and reduce_app st ls ty rem =
and reduce_app engine st ls ty rem_cont =
let rec extract_first n acc l =
if n = 0 then acc,l else
match l with
......@@ -278,35 +409,41 @@ and reduce_app st ls ty rem =
in
let arity = List.length ls.ls_args in
let args,rem_st = extract_first arity [] st in
(*
try
let f = Hls.find builtins ls in
f ls tl ty
let t = f ls args ty in
{ value_stack = Term t :: rem_st;
cont_stack = rem_cont;
}
with Not_found ->
*)
(*
try
let d = Ident.Mid.find ls.ls_name env.tknown in
let d = Ident.Mid.find ls.ls_name engine.known_map in
match d.Decl.d_node with
| Decl.Dtype _ | Decl.Dprop _ -> assert false
| Decl.Dlogic dl ->
(* regular definition *)
let d = List.assq ls dl in
let l,t = Decl.open_ls_defn d in
let env' = multibind_vs l tl env in
compute_in_term env' t
let sigma =
try
List.fold_right2 Mvs.add l args Mvs.empty
with Invalid_argument _ -> assert false
in
{ value_stack = rem_st;
cont_stack = Keval(t,sigma) :: rem_cont;
}
| Decl.Dparam _ | Decl.Dind _ ->
t_app ls tl ty
(* TODO: try a rewrite rule *)
raise Not_found
| Decl.Ddata dl ->
(* constructor or projection *)
match tl with
match args with
| [ { t_node = Tapp(ls1,tl1) } ] ->
(* if ls is a projection and ls1 is a constructor,
we should compute that projection *)
let rec iter dl =
match dl with
| [] -> t_app ls tl ty
| [] -> raise Not_found
| (_,csl) :: rem ->
let rec iter2 csl =
match csl with
......@@ -319,25 +456,23 @@ and reduce_app st ls ty rem =
match prs,tl1 with
| (Some pr)::prs, t::tl1 ->
if ls_equal ls pr
then (* projection found! *) t
then (* projection found! *)
{ value_stack = Term t :: rem_st;
cont_stack = rem_cont;
}
else
iter3 prs tl1
| None::prs, _::tl1 ->
iter3 prs tl1
| _ -> t_app ls tl ty
| _ -> raise Not_found
in iter3 prs tl1
else iter2 rem2
in iter2 csl
in iter dl
| _ -> t_app ls tl ty
| _ -> raise Not_found
with Not_found ->
*)
(*
Format.eprintf "[Compute] definition of logic symbol %s not found@."
ls.ls_name.Ident.id_string;
*)
{ value_stack = Term (t_app ls args ty) :: rem_st;
cont_stack = rem;
cont_stack = rem_cont;
}
......@@ -352,12 +487,58 @@ let rec many_steps engine c n =
let c = reduce engine c in
many_steps engine c (n-1)
let normalize engine t =
let normalize engine t =
let c = { value_stack = []; cont_stack = [Keval(t,Mvs.empty)] } in
many_steps engine c 1000
let create () = Mls.empty
(* the rewrite engine *)
let create env km =
get_builtins env;
{ known_map = km ;
rules = Mls.empty;
}
exception NotARewriteRule of string
let add_rule _t _e = assert false
let extract_rule t =
let rec aux acc t =
match t.t_node with
| Tquant(Tforall,q) ->
let vs,_,t = t_open_quant q in
aux (acc @ vs) t
| Tbinop(Tiff,t1,t2) ->
begin
match t1.t_node with
| Tapp(ls,args) -> acc,ls,args,t2
| _ -> raise
(NotARewriteRule "lhs of <-> should be a predicate symbol")
end
| Tapp(ls,[t1;t2]) when ls == ps_equ ->
begin
match t1.t_node with
| Tapp(ls,args) -> acc,ls,args,t2
| _ -> raise
(NotARewriteRule "lhs of = should be a function symbol")
end
| _ -> raise
(NotARewriteRule "rule should be of the form forall ... t1 = t2 or f1 <-> f2")
in
aux [] t
let add_rule t e =
let vars,ls,args,r = extract_rule t in
let rules =
try Mls.find ls e.rules
with Not_found -> []
in
{e with rules =
Mls.add ls ((vars,args,r)::rules) e.rules}
src/transform/reduction_engine.mli
View file @ 11e3593d
......@@ -69,11 +69,14 @@ terms are normalized with respect to
type engine
val normalize : engine -> Term.term -> Term.term
val create : unit -> engine
val create : Env.env -> Decl.decl Ident.Mid.t -> engine
exception NotARewriteRule of string
val add_rule : Term.term -> engine -> engine
val normalize : engine -> Term.term -> Term.term
tests/test_compute.why
View file @ 11e3593d
......@@ -7,9 +7,9 @@ theory T
goal g3: true /\ true
goal g10: if true then 1=2 else 3=4
goal g10: if true then 1=1 else 3=4
goal g11: let x=1 in x=2
goal g11: let x=1 in x=1
use import int.Int
......@@ -22,4 +22,13 @@ theory T
goal i2: let x = { f = 4 } in
match x with { f = y } -> y + 1 > 3 end
function g int : int
axiom g4 : g 4 = 7
meta "rewrite" prop g4
goal j1 : g (2+2) = 7
end
tests/test_compute/why3session.xml
View file @ 11e3593d
......@@ -18,33 +18,33 @@
<transf name="compute_in_goal" expanded="true">
</transf>
</goal>
<goal name="g10" sum="de9cadc887ffe8cc81f58a6d7c218b44" expanded="true">
<goal name="g10" sum="4c10af77fca7fb45f92d4e4181fcc80a" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g10.1" expl="1." sum="f00e1dfbb01a6a6b20dbaf11948dcbc0">
</goal>
</transf>
</goal>
<goal name="g11" sum="8e9637aa282b824dc1ef410b939e7235" expanded="true">
<goal name="g11" sum="4d359e703e593ef835a349322d923668" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g11.1" expl="1." sum="f00e1dfbb01a6a6b20dbaf11948dcbc0">
</goal>
</transf>
</goal>
<goal name="h1" sum="5d9ea52d9f6b9033794f44b5aa590306" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="h1.1" expl="1." sum="3ec24f1a92fb220b819dc1ee528ae1b6">
</goal>
</transf>
</goal>
<goal name="i1" sum="dfe815a019525fce8a2b755ff30f708a" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="i1.1" expl="1." sum="c11f16854e4ae49e1988dc7055044e7d">
<goal name="i1.1" expl="1." sum="9b65938796ec0367c432c6b1d65fe493">
</goal>
</transf>
</goal>
<goal name="i2" sum="28f0e4a6c637d7af3829655f5173f1e7" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="i2.1" expl="1." sum="2311d64bc0d33b2e7a1b0a9f813c6a83">
<goal name="i2.1" expl="1." sum="479799d9b39348879ba94f8a07c969f6">
</goal>
</transf>
</goal>
<goal name="j1" sum="89e081884a488d0109ef1938861ab614" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="j1.1" expl="1." sum="e8153b085c774d327b6f8e32b778795d">
</goal>
</transf>
</goal>
......
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