Skip to content

GitLab

why3
why3
Commit f0b904bf authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft
Browse files
Options

Add meta rewrite_def declarations programmatically during reflection

parent 97f52506
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 606 additions and 643 deletions
examples/multiprecision/add/why3session.xml
View file @ f0b904bf
......@@ -257,7 +257,7 @@
<goal name="VC add_limbs.14.0.0" expl="assertion" proved="true">
<transf name="reflection_f" proved="true" arg1="mp_decision">
<goal name="VC add_limbs.14.0.0.0" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.39"/></proof>
<proof prover="0"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="VC add_limbs.14.0.0.1" proved="true">
<proof prover="3"><result status="valid" time="0.23"/></proof>
......@@ -539,7 +539,7 @@
<goal name="VC add.55.0.0" expl="assertion" proved="true">
<transf name="reflection_f" proved="true" arg1="mp_decision">
<goal name="VC add.55.0.0.0" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.24"/></proof>
<proof prover="0"><result status="valid" time="0.43"/></proof>
</goal>
<goal name="VC add.55.0.0.1" proved="true">
<proof prover="3"><result status="valid" time="0.19"/></proof>
......@@ -621,7 +621,7 @@
<goal name="VC add.74.0.0" expl="assertion" proved="true">
<transf name="reflection_f" proved="true" arg1="mp_decision">
<goal name="VC add.74.0.0.0" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.22"/></proof>
<proof prover="0"><result status="valid" time="0.42"/></proof>
</goal>
<goal name="VC add.74.0.0.1" proved="true">
<proof prover="3"><result status="valid" time="0.30"/></proof>
......@@ -738,7 +738,7 @@
<goal name="VC add_in_place.17.0.0" expl="assertion" proved="true">
<transf name="reflection_f" proved="true" arg1="mp_decision">
<goal name="VC add_in_place.17.0.0.0" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.18"/></proof>
<proof prover="0"><result status="valid" time="0.36"/></proof>
</goal>
<goal name="VC add_in_place.17.0.0.1" proved="true">
<proof prover="3"><result status="valid" time="0.28"/></proof>
......
examples/multiprecision/div/why3session.xml
View file @ f0b904bf
......@@ -5204,7 +5204,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC div_sb_qr.157.0.0.0.29" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC div_sb_qr.157.0.0.0.30" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......@@ -5306,10 +5306,10 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC div_sb_qr.157.0.0.0.63" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC div_sb_qr.157.0.0.0.64" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC div_sb_qr.157.0.0.0.65" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
......@@ -5474,7 +5474,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC div_sb_qr.157.0.0.0.119" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC div_sb_qr.157.0.0.0.120" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......@@ -5867,7 +5867,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC div_sb_qr.163.0.0.0.32" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC div_sb_qr.163.0.0.0.33" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......@@ -5939,7 +5939,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC div_sb_qr.163.0.0.0.56" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC div_sb_qr.163.0.0.0.57" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......@@ -5954,7 +5954,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC div_sb_qr.163.0.0.0.61" proved="true">
<proof prover="3"><result status="valid" time="0.27"/></proof>
<proof prover="3"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="VC div_sb_qr.163.0.0.0.62" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
......@@ -5966,16 +5966,16 @@
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC div_sb_qr.163.0.0.0.65" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC div_sb_qr.163.0.0.0.66" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC div_sb_qr.163.0.0.0.67" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC div_sb_qr.163.0.0.0.68" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC div_sb_qr.163.0.0.0.69" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......@@ -6017,7 +6017,7 @@
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC div_sb_qr.163.0.0.0.82" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC div_sb_qr.163.0.0.0.83" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......@@ -6038,7 +6038,7 @@
<proof prover="3"><result status="valid" time="0.30"/></proof>
</goal>
<goal name="VC div_sb_qr.163.0.0.0.89" proved="true">
<proof prover="3"><result status="valid" time="0.22"/></proof>
<proof prover="3"><result status="valid" time="0.27"/></proof>
</goal>
<goal name="VC div_sb_qr.163.0.0.0.90" proved="true">
<proof prover="3"><result status="valid" time="0.26"/></proof>
......@@ -6137,10 +6137,10 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC div_sb_qr.163.0.0.0.122" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC div_sb_qr.163.0.0.0.123" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC div_sb_qr.163.0.0.0.124" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......@@ -7510,10 +7510,10 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC div_sb_qr.239.0.0.0.14" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC div_sb_qr.239.0.0.0.15" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC div_sb_qr.239.0.0.0.16" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......@@ -7528,7 +7528,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC div_sb_qr.239.0.0.0.20" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC div_sb_qr.239.0.0.0.21" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......@@ -7675,7 +7675,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC div_sb_qr.239.0.0.0.69" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC div_sb_qr.239.0.0.0.70" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......@@ -7684,7 +7684,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC div_sb_qr.239.0.0.0.72" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC div_sb_qr.239.0.0.0.73" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......@@ -7696,13 +7696,13 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC div_sb_qr.239.0.0.0.76" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC div_sb_qr.239.0.0.0.77" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC div_sb_qr.239.0.0.0.78" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC div_sb_qr.239.0.0.0.79" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
......@@ -7711,7 +7711,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC div_sb_qr.239.0.0.0.81" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC div_sb_qr.239.0.0.0.82" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......@@ -7753,7 +7753,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC div_sb_qr.239.0.0.0.95" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC div_sb_qr.239.0.0.0.96" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......@@ -8100,10 +8100,10 @@
<proof prover="3"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="VC div_sb_qr.239.0.0.2" proved="true">
<proof prover="2" timelimit="1"><result status="valid" time="0.50"/></proof>
<proof prover="2" timelimit="1"><result status="valid" time="0.32"/></proof>
</goal>
<goal name="VC div_sb_qr.239.0.0.3" proved="true">
<proof prover="2" timelimit="1"><result status="valid" time="0.50"/></proof>
<proof prover="2" timelimit="1"><result status="valid" time="0.32"/></proof>
</goal>
</transf>
</goal>
......
examples/multiprecision/lineardecision.mlw
View file @ f0b904bf
......@@ -85,8 +85,6 @@ function interp (e:expr) (y:vars) (z:C.cvars) : C.a
| Cst c -> C.interp c z
end
meta rewrite_def function interp
use import bool.Bool
use import list.List
......@@ -128,16 +126,12 @@ let rec lemma ctx_bound_w (l:context) (b1 b2:int)
function interp_eq (g:equality) (y:vars) (z:C.cvars) : bool
= match g with (g1, g2) -> interp g1 y z = interp g2 y z end
meta rewrite_def function interp_eq
function interp_ctx (l: context) (g: equality) (y: vars) (z:C.cvars) : bool
= match l with
| Nil -> interp_eq g y z
| Cons h t -> (interp_eq h y z) -> (interp_ctx t g y z)
end
meta rewrite_def function interp_ctx
use import mach.int.Int63
use import seq.Seq
use import mach.array.Array63
......@@ -734,8 +728,6 @@ function interp_c (e:cprod) (y:vars) (z:C.cvars) : C.a
| Times e1 e2 -> C.(*) (interp_c e1 y z) (interp_c e2 y z)
end
meta rewrite_def function interp_c
function interp' (e:expr') (y:vars) (z:C.cvars) : C.a
= match e with
| Sum e1 e2 -> C.(+) (interp' e1 y z) (interp' e2 y z)
......@@ -746,8 +738,6 @@ function interp' (e:expr') (y:vars) (z:C.cvars) : C.a
| Coeff c -> C.interp c z
end
meta rewrite_def function interp'
(*exception NonLinear*)
type equality' = (expr', expr')
......@@ -756,16 +746,12 @@ type context' = list equality'
function interp_eq' (g:equality') (y:vars) (z:C.cvars) : bool
= match g with (g1, g2) -> interp' g1 y z = interp' g2 y z end
meta rewrite_def function interp_eq'
function interp_ctx' (l: context') (g: equality') (y: vars) (z:C.cvars) : bool
= match l with
| Nil -> interp_eq' g y z
| Cons h t -> (interp_eq' h y z) -> (interp_ctx' t g y z)
end
meta rewrite_def function interp_ctx'
let rec predicate valid_expr' (e:expr')
variant { e }
= match e with
......@@ -843,8 +829,6 @@ use import real.RealInfix
use import real.FromInt
use import int.Abs
(*meta coercion function from_int*)
type t = (int, int)
type rvars = int -> real
......@@ -858,8 +842,6 @@ function rinterp (t:t) (v:rvars) : real
| (n,d) -> from_int n /. from_int d
end
meta rewrite_def function rinterp
let lemma prod_compat_eq (a b c:real)
requires { c <> 0.0 }
requires { a *. c = b *. c }
......@@ -1016,8 +998,6 @@ function interp_id (t:t') (v:int -> int) : int
| Error -> 0 (* never created *)
end
meta rewrite_def function interp_id
let constant izero = IC 0
let constant ione = IC 1
......@@ -1059,8 +1039,6 @@ let ghost function m_y (y:int -> int): (int -> real)
ensures { forall i. result i = from_int (y i) }
= fun i -> from_int (y i)
meta rewrite_def function m_y
let m (t:t') : (int, int)
ensures { forall z. rinterp result (m_y z) = from_int (interp_id t z) }
raises { NError -> true }
......@@ -1187,8 +1165,6 @@ constant rradix: real = from_int (M.radix)
function qinterp (q:Q.t) : real
= match q with (n,d) -> from_int n /. from_int d end
meta rewrite_def function qinterp
lemma qinterp_def: forall q v. qinterp q = Q.rinterp q v
function interp_exp (e:exp) (y:evars) : int
......@@ -1200,16 +1176,12 @@ function interp_exp (e:exp) (y:evars) : int
| Minus e' -> - (interp_exp e' y)
end
meta rewrite_def function interp_exp
function minterp (t:t) (y:evars) : real
= match t with
(q,e) ->
qinterp q *. pow rradix (from_int (interp_exp e y))
end
meta rewrite_def function minterp
exception MPError
let rec opp_exp (e:exp)
......@@ -1447,8 +1419,6 @@ function mpinterp (t:t) (y:evars) : int
| R -> M.radix
end
meta rewrite_def function mpinterp
(* TODO restructure stuff so that expr, eq, ctx, valid_ can be imported without having to implement these *)
let mpadd (a b:t) : t
......@@ -1524,8 +1494,6 @@ let rec function m (t:t) : R.coeff
| R -> ((1,1), Lit 1) (* or ((radix, 1), Lit 0) ? *)
end
meta rewrite_def function m
let ghost function m_y (y:int->int): (int -> real)
ensures { forall i. result i = from_int (y i) }
= fun i -> from_int (y i)
......@@ -1538,8 +1506,6 @@ let rec function m_cprod (e:cprod) : R.cprod
| Times c1 c2 -> R.Times (m_cprod c1) (m_cprod c2)
end
meta rewrite_def function m_cprod
let rec function m_expr (e:expr') : R.expr'
ensures { forall y z. pos_expr' e z -> R.interp' result (m_y y) z
= from_int (interp' e y z) }
......@@ -1553,16 +1519,12 @@ let rec function m_expr (e:expr') : R.expr'
| ProdR c e -> R.ProdR (m_cprod c) (m_expr e)
end
meta rewrite_def function m_expr
let function m_eq (eq:equality') : R.equality'
ensures { forall y z. pos_eq' eq z -> (R.interp_eq' result (m_y y) z
<-> interp_eq' eq y z) }
ensures { valid_eq' eq -> R.valid_eq' result }
= match eq with (e1,e2) -> (m_expr e1, m_expr e2) end
meta rewrite_def function m_eq
use import list.Length
let rec function m_ctx (ctx:context') : R.context'
......@@ -1579,8 +1541,6 @@ let rec function m_ctx (ctx:context') : R.context'
r
end
meta rewrite_def function m_ctx
let mp_decision (l: context') (g: equality') : bool
requires { valid_ctx' l }
requires { valid_eq' g }
......@@ -2072,21 +2032,15 @@ function interp_term (t:term) (b:int->value) : value =
| Add t1 t2 -> add (interp_term t1 b) (interp_term t2 b)
end
meta rewrite_def function interp_term
function interp_fmla (f:fmla) (l:int) (b:int->value) : bool =
match f with
| Foo t -> foo (interp_term t b)
| Forall f -> forall v. interp_fmla f (l-1) b[l <- v]
end
meta rewrite_def function interp_fmla
function interp (f:fmla) (b: int -> value) : bool =
interp_fmla f (-1) b
meta rewrite_def function interp
let f (f:fmla) : bool
ensures { result -> forall b. interp f b }
= false
......
examples/multiprecision/mul/why3session.xml
View file @ f0b904bf
......@@ -89,7 +89,7 @@
<goal name="VC mul_limb.16.0.0" expl="assertion" proved="true">
<transf name="reflection_f" proved="true" arg1="mp_decision">
<goal name="VC mul_limb.16.0.0.0" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.22"/></proof>
<proof prover="0"><result status="valid" time="0.35"/></proof>
</goal>
<goal name="VC mul_limb.16.0.0.1" proved="true">
<proof prover="3"><result status="valid" time="0.32"/></proof>
......@@ -284,7 +284,7 @@
<goal name="VC addmul_limb.22.0.0" expl="assertion" proved="true">
<transf name="reflection_f" proved="true" arg1="mp_decision">
<goal name="VC addmul_limb.22.0.0.0" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.38"/></proof>
<proof prover="0"><result status="valid" time="0.23"/></proof>
</goal>
<goal name="VC addmul_limb.22.0.0.1" proved="true">
<proof prover="3"><result status="valid" time="0.27"/></proof>
......@@ -524,7 +524,7 @@
<proof prover="0"><result status="valid" time="0.43"/></proof>
</goal>
<goal name="VC mul_limbs.38.0.0.0.0.0.1" proved="true">
<proof prover="3"><result status="valid" time="1.31"/></proof>
<proof prover="3"><result status="valid" time="2.06"/></proof>
</goal>
</transf>
</goal>
......@@ -1109,10 +1109,10 @@
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC mul.41.0.0.0.0.0.0.14" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC mul.41.0.0.0.0.0.0.15" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC mul.41.0.0.0.0.0.0.16" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
......@@ -1121,7 +1121,7 @@
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC mul.41.0.0.0.0.0.0.18" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC mul.41.0.0.0.0.0.0.19" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......@@ -1136,7 +1136,7 @@
<proof prover="3"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="VC mul.41.0.0.0.0.0.0.23" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC mul.41.0.0.0.0.0.0.24" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......@@ -1154,7 +1154,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC mul.41.0.0.0.0.0.0.29" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC mul.41.0.0.0.0.0.0.30" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......@@ -1208,7 +1208,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC mul.41.0.0.0.0.0.0.47" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC mul.41.0.0.0.0.0.0.48" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......@@ -1232,10 +1232,10 @@
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC mul.41.0.0.0.0.0.0.55" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC mul.41.0.0.0.0.0.0.56" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC mul.41.0.0.0.0.0.0.57" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
......@@ -1253,7 +1253,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC mul.41.0.0.0.0.0.0.62" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC mul.41.0.0.0.0.0.0.63" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......@@ -1301,7 +1301,7 @@
<proof prover="3"><result status="valid" time="0.26"/></proof>
</goal>
<goal name="VC mul.41.0.0.0.0.0.0.78" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC mul.41.0.0.0.0.0.0.79" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
......@@ -1328,7 +1328,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC mul.41.0.0.0.0.0.0.87" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC mul.41.0.0.0.0.0.0.88" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......
examples/multiprecision/sub/why3session.xml
View file @ f0b904bf
......@@ -343,7 +343,7 @@
<goal name="VC sub.15.0.0" expl="assertion" proved="true">
<transf name="reflection_f" proved="true" arg1="mp_decision">
<goal name="VC sub.15.0.0.0" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="4.29"/></proof>
<proof prover="0"><result status="valid" time="3.64"/></proof>
</goal>
<goal name="VC sub.15.0.0.1" proved="true">
<proof prover="3"><result status="valid" time="0.22"/></proof>
......@@ -437,7 +437,7 @@
<goal name="VC sub.38.0.0" expl="assertion" proved="true">
<transf name="reflection_f" proved="true" arg1="mp_decision">
<goal name="VC sub.38.0.0.0" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.24"/></proof>
<proof prover="0"><result status="valid" time="0.56"/></proof>
</goal>
<goal name="VC sub.38.0.0.1" proved="true">
<proof prover="3"><result status="valid" time="0.28"/></proof>
......@@ -596,7 +596,7 @@
<goal name="VC sub.73.0.0" expl="assertion" proved="true">
<transf name="reflection_f" proved="true" arg1="mp_decision">
<goal name="VC sub.73.0.0.0" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.24"/></proof>
<proof prover="0"><result status="valid" time="0.46"/></proof>
</goal>
<goal name="VC sub.73.0.0.1" proved="true">
<proof prover="3"><result status="valid" time="0.19"/></proof>
......@@ -854,7 +854,7 @@
<goal name="VC sub_in_place.50.0.0" expl="assertion" proved="true">
<transf name="reflection_f" proved="true" arg1="mp_decision">
<goal name="VC sub_in_place.50.0.0.0" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.21"/></proof>
<proof prover="0"><result status="valid" time="0.37"/></proof>
</goal>
<goal name="VC sub_in_place.50.0.0.1" proved="true">
<proof prover="3"><result status="valid" time="0.23"/></proof>
......
src/transform/reflection.ml
View file @ f0b904bf
......@@ -27,6 +27,7 @@ type reify_env = { kn: known_map;
crc_map: Coercion.t;
ty_to_map: vsymbol Mty.t;
env: Env.env;
interps: Sls.t; (* functions that were inverted*)
task: Task.task;
bound_vars: Svs.t; (* bound variables, do not map them in a var map*)
bound_fr: int; (* separate, negative index for bound vars*)
......@@ -42,6 +43,7 @@ let init_renv kn crc lv env task =
crc_map = crc;
ty_to_map = Mty.empty;
env = env;
interps = Sls.empty;
task = task;
bound_vars = Svs.empty;
bound_fr = -1;
......@@ -309,7 +311,7 @@ let rec reify_term renv t rt =
let vl, f = open_ls_defn ld in
Debug.dprintf debug_reification "invert_interp ls %a t %a@."
Pretty.print_ls ls Pretty.print_term t;
invert_body renv ls vl f t
invert_body { renv with interps = Sls.add ls renv.interps } ls vl f t
and invert_body renv ls vl f t =
match f.t_node with
| Tvar v when vs_equal v (List.hd vl) -> renv, t
......@@ -345,6 +347,7 @@ let rec reify_term renv t rt =
let vl, f = open_ls_defn ld in
Debug.dprintf debug_reification "invert_ctx_interp ls %a @."
Pretty.print_ls ls;
let renv = { renv with interps = Sls.add ls renv.interps } in
invert_ctx_body renv ls vl f t l g
and invert_ctx_body renv ls vl f t l g =
match f.t_node with
......@@ -520,7 +523,7 @@ let build_vars_map renv prev =
renv.store (prev,[]) in
subst, prev, mapdecls, defdecls
let build_goals do_trans prev mapdecls defdecls subst env lp g rt =
let build_goals do_trans renv prev mapdecls defdecls subst env lp g rt =
Debug.dprintf debug_refl "building goals@.";
let inst_rt = t_subst subst rt in