Skip to content
GitLab
Commit 7c2ead74 authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft
Browse files

add reification transformation (wip)

parent 96afb1a7
Hide whitespace changes
Inline Side-by-side
Makefile.in
View file @ 7c2ead74
......@@ -190,7 +190,7 @@ LIB_TRANSFORM = simplify_formula inlining split_goal induction \
eliminate_epsilon intro_projections_counterexmp \
intro_vc_vars_counterexmp prepare_for_counterexmp \
instantiate_predicate smoke_detector \
induction_pr prop_curry eliminate_literal
induction_pr prop_curry eliminate_literal reification
LIB_PRINTER = cntexmp_printer alt_ergo why3printer smtv1 smtv2 coq\
pvs isabelle \
......
examples/in_progress/multiprecision/compute.mlw
View file @ 7c2ead74
......@@ -465,37 +465,83 @@ let ghost function normalize (x:t') : t'
ensures { eq' result x }
= insertion_sort_mon x
lemma norm: forall x1 x2: t, y:vars.
normalize (conv x1) = normalize (conv x2) -> interp x1 y = interp x2 y
let lemma norm (x1 x2: t) (y:vars)
requires { normalize (conv x1) = normalize (conv x2) }
ensures { interp x1 y = interp x2 y }
= ()
let lemma norm' (x1 x2: t')
requires { normalize x1 = normalize x2 }
ensures { eq' x1 x2 }
= ()
lemma norm': forall x1 x2: t'. normalize x1 = normalize x2 -> eq' x1 x2
meta reify_target function interp
goal g: forall x y. x * y = y * x
end
module ReifyTests
use import int.Int
let predicate eq0_int (x:int) = x=0
clone export AssocAlgebra with type r = int, type a = int, constant R.zero = Int.zero, constant R.one = Int.one, function R.(+) = (+), function R.(-_) = (-_), function R.(*) = (*),constant A.zero = Int.zero, constant one = Int.one, function (+) = (+), function A.(-_) = (-_), function ( *) = ( *), function (@) = ( *), goal AUnitary, goal ANonTrivial, goal ExtDistSumA, goal ExtDistSumR, goal AssocMulExt, goal UnitExt, goal CommMulExt, val eq0 = eq0_int, goal A.MulAssoc.Assoc, goal A.Unit_def_l, goal A.Unit_def_r, goal A.Comm, goal A.Assoc
use import AssocAlgebraDecision
meta reify_target function interp
goal g: forall x y. x * y = y * x
end
module Matrix
use import int.Int
use import int.MinMax
use import matrices.Matrix
use import matrices.MatrixArithmetic
use import matrices.BlockMul
constant d : int
axiom DimNonNeg : d >= 0
function extf (c: int) (a:mat int) : int -> int -> int =
fun x y -> c * (get a x y)
function ext (c: int) (a:mat int) : mat int =
create (rows a) (cols a) (extf c a)
function addm (a b: mat int) : mat int =
create (max a.rows b.rows) (max a.cols b.cols) (add2f a b)
constant d : int
axiom DimNonNeg : d >= 0
constant zero11 : mat int = zero d d
constant one11 : mat int = create d d (fun _ _ -> 1)
constant zero11 : mat int = zero 0 0
constant one11 : mat int = create d d (fun x y -> if x=y then 1 else 0)
let predicate eq0_int (x:int) = x=0
clone export AssocAlgebra with type r = int, type a = mat int, constant R.zero = Int.zero, constant R.one = Int.one, function R.(+) = (+), function R.(-_) = (-_), function R.(*) = (*),constant A.zero = zero11, constant one = one11, function (+) = add, function A.(-_) = opp, function ( *) = mul, function (@) = ext, goal AUnitary, goal ANonTrivial, goal ExtDistSumA, goal ExtDistSumR, goal AssocMulExt, goal UnitExt, goal CommMulExt, val eq0 = eq0_int
clone export AssocAlgebra with type r = int, type a = mat int, constant R.zero = Int.zero, constant R.one = Int.one, function R.(+) = (+), function R.(-_) = (-_), function R.(*) = (*),constant A.zero = zero11, constant one = one11, function (+) = add, function A.(-_) = opp, function ( *) = mul, function (@) = ext, goal AUnitary, goal ANonTrivial, goal ExtDistSumA, goal ExtDistSumR, goal AssocMulExt, goal UnitExt, goal CommMulExt, val eq0 = eq0_int, goal A.MulAssoc.Assoc, goal A.Unit_def_l, goal A.Unit_def_r, goal A.Comm, goal A.Assoc
predicate quarters (a a11 a12 a21 a22: mat int) =
(rows a11 = rows a12 = rows a21 = rows a22 = cols a11 = cols a12 = cols a21 = cols a22) /\
rows a = cols a = 2 * rows a11 /\
a11 = block a 0 a11.rows 0 a11.cols /\ a12 = block a 0 a11.rows a11.cols a11.cols /\
a21 = block a a11.rows a11.rows 0 a11.cols /\ a22 = block a a11.rows a11.rows a11.cols a11.cols
let lemma naive_blocks (a b c a11 a12 a21 a22 b11 b12 b21 b22 c11 c12 c21 c22: mat int)
requires { quarters a a11 a12 a21 a22 }
requires { quarters b b11 b12 b21 b22 }
requires { quarters c c11 c12 c21 c22 }
requires { c11 = add (mul a11 b11) (mul b11 b22) }
requires { c12 = add (mul a11 b12) (mul a12 b22) }
requires { c21 = add (mul a21 b11) (mul a22 b21) }
requires { c22 = add (mul a21 b12) (mul a22 b22) }
ensures { c = mul a b }
=
()
use import AssocAlgebraDecision
......
examples/in_progress/multiprecision/compute/why3session.xml
View file @ 7c2ead74
......@@ -7,6 +7,8 @@
<prover id="2" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="2000"/>
<prover id="3" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="2000"/>
<prover id="4" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="5" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="2000"/>
<prover id="6" name="CVC4" version="1.4" alternative="noBV" timelimit="5" steplimit="0" memlimit="2000"/>
<file name="../compute.mlw" expanded="true">
<theory name="UnitaryCommutativeRingDecision" sum="f010a5ed2c748e31ccaccc0292b55495">
<goal name="VC mon_append" expl="VC for mon_append">
......@@ -185,7 +187,7 @@
</theory>
<theory name="AssocAlgebra" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="AssocAlgebraDecision" sum="bee23ddea5475b0e934c7a637429ecf5">
<theory name="AssocAlgebraDecision" sum="cd72537220c542d80824e2433ae6eb82" expanded="true">
<goal name="VC mon_append" expl="VC for mon_append">
<proof prover="1"><result status="valid" time="0.08"/></proof>
</goal>
......@@ -321,25 +323,118 @@
<goal name="VC normalize" expl="VC for normalize">
<proof prover="0"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
<goal name="norm" expl="">
<goal name="VC norm" expl="VC for norm">
<proof prover="0"><result status="valid" time="0.01" steps="18"/></proof>
</goal>
<goal name="norm&apos;" expl="">
<goal name="VC norm&apos;" expl="VC for norm&apos;">
<proof prover="0"><result status="valid" time="0.01" steps="17"/></proof>
</goal>
<goal name="g" expl="" expanded="true">
<transf name="reify_in_goal" expanded="true">
<goal name="g.1" expl="">
</goal>
</transf>
</goal>
</theory>
<theory name="Matrix" sum="df65c6acebd2109674a28fa86f5a4661">
<theory name="ReifyTests" sum="09053f82ecaf1fb136e738fe5030ac4c" expanded="true">
<goal name="VC eq0_int" expl="VC for eq0_int">
<proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
<goal name="A.Assoc" expl="">
<proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
<goal name="A.Unit_def_l" expl="">
<proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
<goal name="A.Unit_def_r" expl="">
<proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
<goal name="A.Comm" expl="">
<proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
<goal name="A.MulAssoc.Assoc" expl="">
<proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
<goal name="AUnitary" expl="">
<proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
<goal name="ANonTrivial" expl="">
<proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
<goal name="ExtDistSumA" expl="">
<proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
<goal name="ExtDistSumR" expl="">
<proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
<goal name="AssocMulExt" expl="">
<proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
<goal name="UnitExt" expl="">
<proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
<goal name="CommMulExt" expl="">
<proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
<goal name="VC eq0" expl="VC for eq0">
<proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
<goal name="g" expl="">
</goal>
</theory>
<theory name="Matrix" sum="dcd79758644cb2e40daabcc2e39533b1" expanded="true">
<goal name="VC eq0_int" expl="VC for eq0_int">
<proof prover="0"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
<goal name="A.Assoc" expl="" expanded="true">
<proof prover="0"><result status="unknown" time="0.07"/></proof>
<proof prover="1"><result status="timeout" time="4.95"/></proof>
<proof prover="2"><result status="timeout" time="5.00"/></proof>
<proof prover="3"><result status="timeout" time="5.00"/></proof>
<proof prover="5"><result status="timeout" time="5.00"/></proof>
<transf name="compute_in_goal" expanded="true">
<goal name="Assoc.1" expl="" expanded="true">
<proof prover="0"><result status="unknown" time="0.02"/></proof>
<proof prover="1"><result status="timeout" time="4.98"/></proof>
<proof prover="2"><result status="timeout" time="5.00"/></proof>
<proof prover="3"><result status="timeout" time="5.00"/></proof>
</goal>
</transf>
</goal>
<goal name="A.Unit_def_l" expl="" expanded="true">
<proof prover="0"><result status="timeout" time="5.00"/></proof>
<proof prover="1"><result status="timeout" time="4.98"/></proof>
<proof prover="2"><result status="timeout" time="5.00"/></proof>
<proof prover="3"><result status="timeout" time="5.00"/></proof>
<proof prover="6"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="A.Unit_def_r" expl="" expanded="true">
<proof prover="3"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="A.Comm" expl="" expanded="true">
<proof prover="2"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="A.MulAssoc.Assoc" expl="">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<transf name="smoke_detector_top">
<goal name="Assoc.1" expl="">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
<goal name="AUnitary" expl="">
<proof prover="1"><result status="valid" time="0.04"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
<transf name="smoke_detector_top">
<goal name="AUnitary.1" expl="">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
</transf>
</goal>
<goal name="ANonTrivial" expl="">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="ExtDistSumA" expl="">
<proof prover="1"><result status="valid" time="0.03"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="ExtDistSumR" expl="">
<proof prover="1"><result status="valid" time="0.03"/></proof>
......@@ -348,14 +443,38 @@
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="UnitExt" expl="">
<proof prover="0"><result status="timeout" time="4.99"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="timeout" time="5.00"/></proof>
<proof prover="5"><result status="timeout" time="5.00"/></proof>
<transf name="compute_in_goal">
<goal name="UnitExt.1" expl="">
<proof prover="0"><result status="timeout" time="4.98"/></proof>
<proof prover="1"><result status="valid" time="0.05"/></proof>
<proof prover="2"><result status="timeout" time="10.00"/></proof>
<proof prover="3"><result status="timeout" time="5.00"/></proof>
<proof prover="5"><result status="timeout" time="5.00"/></proof>
</goal>
</transf>
</goal>
<goal name="CommMulExt" expl="">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
<transf name="smoke_detector_deep">
<goal name="CommMulExt.1" expl="">
<proof prover="1"><result status="valid" time="0.05"/></proof>
</goal>
</transf>
</goal>
<goal name="VC eq0" expl="VC for eq0">
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
<goal name="VC naive_blocks" expl="VC for naive_blocks">
<transf name="smoke_detector_deep">
<goal name="VC naive_blocks.1" expl="VC for naive_blocks">
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
src/mlw/cprinter.ml
View file @ 7c2ead74
......@@ -777,6 +777,7 @@ module MLToC = struct
end
| Lsym _ -> raise (Unsupported "LDsym")
| Lrec _ -> raise (Unsupported "LDrec") (* TODO for rec at least*)
| Lany _ -> raise (Unsupported "Lany")
end
| Eif (cond, th, el) ->
let cd,cs = expr info {env with computes_return_value = false} cond in
......
src/transform/reification.ml 0 → 100644
View file @ 7c2ead74
open Term
open Ty
open Decl
open Theory
let meta_reify_target = Theory.register_meta_excl "reify_target" [Theory.MTlsymbol]
~desc:"Declares@ the@ given@ type@ as@ target@ for@ reification,@ with@ its@ interpretation@ function." (*FIXME desc*)
(*let meta_reify_invert = Theory.register_meta "reify_invert" [Theory.MTlsymbol]
~desc:"Declares@ that@ the@ given@ interpretation@ function@ can@ be@ inverted@ during@ the@ reification."*)
(* target: t = V int | ...
interp: t -> (int -> 'a) -> 'a *)
let rec fold_left3 f accu l1 l2 l3 =
match (l1, l2, l3) with
| a1::l1, a2::l2, a3::l3 -> fold_left3 f (f accu a1 a2 a3) l1 l2 l3
| [], [], [] -> accu
| _ -> raise (Invalid_argument "fold_left3")
let collect_reify_targets_t =
Trans.on_meta_excl meta_reify_target
(function
| None -> raise Exit
| Some [Theory.MAls i]
-> Trans.return i
| _ -> assert false)
exception Exit
let debug = false
let reify_goal interp task =
let kn = Task.task_known task in
let ty_vars, ty_val = match interp.ls_args, interp.ls_value with
| [ _ty_target; ty_vars ], Some ty_val
when ty_equal ty_vars (ty_func ty_int ty_val)
-> ty_vars, ty_val
| _ -> raise Exit in
let ly = create_fsymbol (Ident.id_fresh "y") [] ty_vars in
let y = t_app ly [] (Some ty_vars) in
let rec invert_pat vl (env, fr) (p,f) t =
if debug
then Format.printf "invert_pat p %a f %a t %a@."
Pretty.print_pat p Pretty.print_term f Pretty.print_term t;
match p.pat_node, f.t_node, t.t_node with
| Pwild, _, _ -> raise Exit
| Papp (cs, [{pat_node = Pvar v1}]),
Tapp (ffa,[{t_node = Tvar vy}; {t_node = Tvar v2}]),
Tvar _
| Papp (cs, [{pat_node = Pvar v1}]),
Tapp (ffa,[{t_node = Tvar vy}; {t_node = Tvar v2}]),
Tapp(_, [])
when ty_equal v1.vs_ty ty_int
&& Svs.mem v1 p.pat_vars
&& vs_equal v1 v2
&& ls_equal ffa fs_func_app
&& List.exists (fun vs -> vs_equal vs vy) vl (*FIXME*)
->
if debug then Format.printf "case var@.";
let rty = cs.ls_value in
if Mterm.mem t env
then
begin
if debug then Format.printf "%a exists@." Pretty.print_term t;
(*(env,fr,t_app fs_func_app [yt; t_nat_const (Mvs.find v env)] rty) ???*)
(env, fr, t_app cs [t_nat_const (Mterm.find t env)] rty)
end
else
begin
if debug then Format.printf "%a is new@." Pretty.print_term t;
let env = Mterm.add t fr env in
(env, fr+1, t_app cs [t_nat_const fr] rty)
end
(* | Papp (cs, [{pat_node = Pvar v1}]),
Tapp (ffa,[{t_node = Tvar vy}; {t_node = Tvar v2}]), Tapp (ls, []) ->
Format.printf "yes@."; raise Exit*)
| Papp (cs, pl), Tapp(ls1, la1), Tapp(ls2, la2) when ls_equal ls1 ls2
->
if debug then Format.printf "case app@.";
(* same head symbol, match parameters *)
let env, fr, rl =
fold_left3
(fun (env, fr, acc) p f t ->
let env, fr, t = invert_pat vl (env, fr) (p, f) t in
if debug then Format.printf "param matched@.";
(env, fr, t::acc))
(env, fr, []) pl la1 la2 in
env, fr, t_app cs (List.rev rl) cs.ls_value
| Papp _, Tapp (ls1, _), Tapp(ls2, _) ->
if debug then Format.printf "head symbol mismatch %a %a@."
Pretty.print_ls ls1 Pretty.print_ls ls2;
raise Exit
| Por (p1, p2), _, _ ->
if debug then Format.printf "case or@.";
begin try invert_pat vl (env, fr) (p1, f) t
with Exit -> invert_pat vl (env, fr) (p2, f) t
end
| Pvar _, Tapp (ls, _la), _ when ls_equal ls interp
-> if debug then Format.printf "case interp@.";
invert_interp (env, fr) ls t
(*| Papp (cs, pl), Tapp (ls1, la1), _ when Sls.mem ls1 !reify_invert
-> (* Cst c -> morph c <- 42 ? *) *)
| _ -> raise Exit
(* interp x y <- t ? *)
and invert_interp (env, fr) ls (t:term) = (*la ?*)
let ld = Opt.get (find_logic_definition kn ls) in
let vl, f = open_ls_defn ld in
(*assert (oty_equal f.t_ty t.t_ty);*)
if debug then Format.printf "invert_interp ls %a t %a@."
Pretty.print_ls ls Pretty.print_term t;
match f.t_node, t.t_node with
| Tcase (x, bl), _ ->
(*FIXME*)
assert (List.length vl = 2);
(match x.t_node with Tvar v when vs_equal v (List.hd vl) -> () | _ -> assert false);
if debug then Format.printf "case match@.";
let rec aux = function
| [] -> raise Exit
| tb::l ->
try invert_pat vl (env, fr) (t_open_branch tb) t
with Exit -> if debug then Format.printf "match failed@.";aux l in
aux bl
| _ -> raise Exit
in
let rec reify_term (env, fr) (t:term) =
if debug then Format.printf "reify_term %a@." Pretty.print_term t;
match t.t_node with
| Tapp(ls, [t1; t2]) when ls_equal ls ps_equ ->
if debug then Format.printf "case =@.";
let (env, fr, t1) = reify_term (env, fr) t1 in
let (env, fr, t2) = reify_term (env, fr) t2 in
env, fr, t_equ t1 t2
| Tquant (Tforall, _) ->
raise Exit (* we introduce premises before the transformation *)
| _ -> (*FIXME*)
ignore (oty_match Mtv.empty t.t_ty interp.ls_value);
if debug then Format.printf "case interp@.";
let env, fr, x = invert_interp (env, fr) interp t in
env, fr, t_app interp [x; y] (Some ty_val)
(*| _ ->
if debug then
Format.printf "wrong type: t.ty %a interp.ls_value %a@."
Pretty.print_ty (Opt.get t.t_ty)
Pretty.print_ty (Opt.get interp.ls_value);
raise Exit*)
in
let open Task in
match task with
| Some
{ task_decl =
{ td_node = Decl { d_node = Dprop (Pgoal, pr, f) } };
task_prev = prev;
} ->
begin try
if debug then Format.printf "start@.";
let (env, _fr, t) = reify_term (Mterm.empty, 0) f in
if debug then Format.printf "building y map@.";
let d = create_param_decl ly in
let prev = Task.add_decl prev d in
let prev = Mterm.fold
(fun t i prev ->
let et = t_equ (t_app fs_func_app [y; t_nat_const i] (Some ty_val))
t in
if debug then Format.printf "eq_term ok@.";
let pr = Decl.create_prsymbol (Ident.id_fresh "y_val") in
let d = Decl.create_prop_decl Paxiom pr et in
Task.add_decl prev d)
env prev in
if debug then Format.printf "building goal@.";
let d = Decl.create_prop_decl Pgoal pr t in
Task.add_decl prev d
with Exit -> task end
| _ -> assert false
let reify_goal_t interp = Trans.store (reify_goal interp)
let reify_in_goal = (Trans.compose Introduction.introduce_premises
(Trans.bind collect_reify_targets_t reify_goal_t))
let () = Trans.register_transform
"reify_in_goal"
~desc:"Reify@ goal@ to@ declared@ target@ datatype."
reify_in_goal
(*
Local Variables:
compile-command: "unset LANG; make -C ../.."
End:
*)
src/transform/reification.mli 0 → 100644
View file @ 7c2ead74
val meta_reify_target : Theory.meta
val reify_in_goal : Task.task Trans.trans
Supports Markdown
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