(* --------------------------------------------------------------------
* Copyright (c) - 2012--2015 - IMDEA Software Institute
* Copyright (c) - 2012--2015 - Inria
*
* Distributed under the terms of the CeCILL-C-V1 license
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
open EcIdent
open EcUtils
open EcTypes
open EcModules
open EcBigInt.Notations
module BI = EcBigInt
(* -------------------------------------------------------------------- *)
include EcCoreFol
(* -------------------------------------------------------------------- *)
let f_eqparams f1 ty1 vs1 m1 f2 ty2 vs2 m2 =
let f_pvlocs f ty vs m =
let arg = f_pvarg f ty m in
if List.length vs = 1 then [arg]
else
let t = Array.of_list vs in
let t = Array.mapi (fun i vd -> f_proj arg i vd.v_type) t in
Array.to_list t
in
match vs1, vs2 with
| Some vs1, Some vs2 ->
if List.length vs1 = List.length vs2
then f_eqs (f_pvlocs f1 ty1 vs1 m1) (f_pvlocs f2 ty2 vs2 m2)
else f_eq (f_tuple (f_pvlocs f1 ty1 vs1 m1))
(f_tuple (f_pvlocs f2 ty2 vs2 m2))
| Some vs1, None ->
f_eq (f_tuple (f_pvlocs f1 ty1 vs1 m1)) (f_pvarg f2 ty2 m2)
| None, Some vs2 ->
f_eq (f_pvarg f1 ty1 m1) (f_tuple (f_pvlocs f2 ty2 vs2 m2))
| None, None ->
f_eq (f_pvarg f1 ty1 m1) (f_pvarg f2 ty2 m2)
let f_eqres f1 ty1 m1 f2 ty2 m2 =
f_eq (f_pvar (pv_res f1) ty1 m1) (f_pvar (pv_res f2) ty2 m2)
let f_eqglob mp1 m1 mp2 m2 =
f_eq (f_glob mp1 m1) (f_glob mp2 m2)
(* -------------------------------------------------------------------- *)
let f_op_real_of_int = f_op EcCoreLib.CI_Real.p_real_of_int [] (tfun tint treal) (* CORELIB *)
let f_real_of_int f = f_app f_op_real_of_int [f] treal
let f_rint n = f_real_of_int (f_int n)
let f_r0 = f_rint BI.zero
let f_r1 = f_rint BI.one
let destr_rint f =
match f.f_node with
| Fapp (op, [f1]) when f_equal f_op_real_of_int op -> begin
try destr_int f1 with DestrError _ -> destr_error "destr_rint"
end
| _ -> destr_error "destr_rint"
(* -------------------------------------------------------------------- *)
let fop_int_le = f_op EcCoreLib.CI_Int .p_int_le [] (toarrow [tint ; tint ] tbool)
let fop_int_lt = f_op EcCoreLib.CI_Int .p_int_lt [] (toarrow [tint ; tint ] tbool)
let fop_real_le = f_op EcCoreLib.CI_Real.p_real_le [] (toarrow [treal; treal] tbool)
let fop_real_lt = f_op EcCoreLib.CI_Real.p_real_lt [] (toarrow [treal; treal] tbool)
let fop_real_add = f_op EcCoreLib.CI_Real.p_real_add [] (toarrow [treal; treal] treal)
let fop_real_sub = f_op EcCoreLib.CI_Real.p_real_sub [] (toarrow [treal; treal] treal)
let fop_real_mul = f_op EcCoreLib.CI_Real.p_real_mul [] (toarrow [treal; treal] treal)
let fop_real_div = f_op EcCoreLib.CI_Real.p_real_div [] (toarrow [treal; treal] treal)
let f_int_le f1 f2 = f_app fop_int_le [f1; f2] tbool
let f_int_lt f1 f2 = f_app fop_int_lt [f1; f2] tbool
(* -------------------------------------------------------------------- *)
let f_real_le f1 f2 = f_app fop_real_le [f1; f2] tbool
let f_real_lt f1 f2 = f_app fop_real_lt [f1; f2] tbool
let f_real_add f1 f2 = f_app fop_real_add [f1; f2] treal
let f_real_sub f1 f2 = f_app fop_real_sub [f1; f2] treal
let f_real_mul f1 f2 = f_app fop_real_mul [f1; f2] treal
let f_real_div f1 f2 = f_app fop_real_div [f1; f2] treal
(* -------------------------------------------------------------------- *)
let fop_in_supp ty = f_op EcCoreLib.CI_Distr.p_in_supp [ty] (toarrow [ty; tdistr ty] tbool)
let fop_mu_x ty = f_op EcCoreLib.CI_Distr.p_mu_x [ty] (toarrow [tdistr ty; ty] treal)
let fop_mu ty = f_op EcCoreLib.CI_Distr.p_mu [ty] (toarrow [tdistr ty; tcpred ty] treal)
let f_in_supp f1 f2 = f_app (fop_in_supp f1.f_ty) [f1; f2] tbool
let f_mu_x f1 f2 = f_app (fop_mu_x f2.f_ty) [f1; f2] treal
let f_mu_ty ty f1 f2 = f_app (fop_mu ty) [f1;f2] treal
let f_mu env f1 f2 = f_mu_ty (EcUnify.destr_tdistr env f1.f_ty) f1 f2
let fop_weight ty = f_op EcCoreLib.CI_Distr.p_weight [ty] (tfun (tdistr ty) treal) (* CORELIB *)
let f_weight ty d = f_app (fop_weight ty) [d] treal
let fop_b2r =
f_op EcCoreLib.CI_Real.p_b2r [] (toarrow [tbool] treal) (* CORELIB *)
let f_real_of_bool f = f_app fop_b2r [f] treal
let fop_muf ty =
f_op EcCoreLib.CI_Distr.p_muf [ty] (toarrow [toarrow [ty] treal; tdistr ty] treal) (* CORELIB *)
let f_muf_ty ty f1 f2 = f_app (fop_muf ty) [f1;f2] treal
let f_muf env f1 f2 = f_muf_ty (EcUnify.tfun_dom env f1.f_ty) f1 f2
let f_integr env f mu =
let ty = EcUnify.tfun_dom env f.f_ty in
f_muf_ty ty f (f_local mu (tdistr ty))
let f_muf_b2r (m,ty) f mu =
(f_muf_ty ty
(f_lambda [m,GTty ty] (f_real_of_bool f))
(f_local mu (tdistr ty)))
let f_square (m, ty) f mu =
f_eq (f_muf_b2r (m,ty) (f_not f) mu) f_r0
let f_mulossless env mu =
let ty = EcUnify.destr_tdistr env mu.f_ty in
let x = EcIdent.create "x" in
f_eq (f_muf_ty ty (f_lambda [x,GTty ty] f_r1) mu) f_r1
(* -------------------------------------------------------------------- *)
let f_losslessF f = f_bdHoareF f_true f f_true FHeq f_r1
(* -------------------------------------------------------------------- *)
let f_identity ?(name = "x") ty =
let name = EcIdent.create name in
f_lambda [name, GTty ty] (f_local name ty)
(* -------------------------------------------------------------------- *)
let f_int_opp_simpl f =
match f.f_node with
| Fapp (op, [f]) when f_equal op fop_int_opp -> f
| _ -> if f_equal f_i0 f then f_i0 else f_int_opp f
let f_int_add_simpl f1 f2 =
try f_int (destr_int f1 +^ destr_int f2)
with DestrError _ ->
if f_equal f_i0 f1 then f2
else if f_equal f_i0 f2 then f1
else f_int_add f1 f2
let f_int_sub_simpl f1 f2 =
if f_equal f1 f2 then f_i0 else
try f_int (destr_int f1 -^ destr_int f2)
with DestrError _ ->
if f_equal f_i0 f1 then f_int_opp_simpl f2
else if f_equal f_i0 f2 then f1
else f_int_sub f1 f2
let f_int_mul_simpl f1 f2 =
try f_int (destr_int f1 *^ destr_int f2)
with DestrError _ ->
if f_equal f_i0 f1 || f_equal f_i0 f2 then f_i0
else if f_equal f_i1 f1 then f2
else if f_equal f_i1 f2 then f1
else f_int_mul f1 f2
(* -------------------------------------------------------------------- *)
let destr_rdivint f =
match f.f_node with
| Fapp (op, [f1; f2]) when f_equal op fop_real_div -> begin
try (destr_rint f1, destr_rint f2)
with DestrError _ -> destr_error "rdivint"
end
| _ -> destr_error "rdivint"
let norm_real_int_div n1 n2 =
if BI.sign n2 = 0 then f_real_div (f_rint n1) (f_rint n2) else
if BI.sign n1 = 0 then f_r0 else
let n1, n2 =
match BI.gcd n1 n2 with
| n when BI.equal n BI.one -> (n1, n2)
| n -> (n1/^n, n2/^n)
in
if BI.equal n1 BI.zero then f_r0
else if BI.equal n2 BI.one then f_rint n1
else if BI.sign n2 < 0 then f_real_div (f_rint (~^n1)) (f_rint (~^n2))
else f_real_div (f_rint n1) (f_rint n2)
let f_real_add_simpl f1 f2 =
try f_rint (destr_rint f1 +^ destr_rint f2)
with DestrError _ ->
try
let (n1, d1), (n2, d2) = destr_rdivint f1, destr_rdivint f2 in
if BI.sign d1 = 0 || BI.sign d2 = 0
then norm_real_int_div (n1 *^ n2) BI.zero
else norm_real_int_div (n1*^d2 +^ n2*^d1) (d1*^d2)
with DestrError _ ->
if f_equal f_r0 f1 then f2
else if f_equal f_r0 f2 then f1
else f_real_add f1 f2
let f_real_sub_simpl f1 f2 =
try f_rint (destr_rint f1 -^ destr_rint f2)
with DestrError _ ->
try
let (n1, d1), (n2, d2) = destr_rdivint f1, destr_rdivint f2 in
if BI.sign d1 = 0 || BI.sign d2 = 0
then norm_real_int_div (n1 -^ n2) BI.zero
else norm_real_int_div (n1*^d2 -^ n2*^d1) (d1*^d2)
with DestrError _ ->
if f_equal f_r0 f2 then f1 else f_real_sub f1 f2
let rec f_real_mul_simpl f1 f2 =
match f1.f_node, f2.f_node with
| Fapp (op1, [f1_1; f1_2]), Fapp (op2, [f2_1; f2_2])
when f_equal op1 fop_real_div
&& f_equal op2 fop_real_div
-> f_real_div_simpl
(f_real_mul_simpl f1_1 f2_1)
(f_real_mul_simpl f1_2 f2_2)
| _, Fapp (op2, [f2_1; f2_2]) when f_equal op2 fop_real_div ->
f_real_div_simpl (f_real_mul_simpl f1 f2_1) f2_2
| Fapp (op1, [f1_1; f1_2]), _ when f_equal op1 fop_real_div ->
f_real_div_simpl (f_real_mul_simpl f1_1 f2) f1_2
| _ ->
try f_rint (destr_rint f1 *^ destr_rint f2)
with DestrError _ ->
if f_equal f_r0 f1 || f_equal f_r0 f2 then f_r0
else if f_equal f_r1 f1 then f2
else if f_equal f_r1 f2 then f1
else f_real_mul f1 f2
and f_real_div_simpl f1 f2 =
match f1.f_node, f2.f_node with
| Fapp (op1, [f1_1; f1_2]), Fapp (op2, [f2_1; f2_2])
when f_equal op1 fop_real_div
&& f_equal op2 fop_real_div
-> f_real_div_simpl
(f_real_mul_simpl f1_1 f2_2)
(f_real_mul_simpl f1_2 f2_1)
| _, Fapp (op2, [f2_1; f2_2]) when f_equal op2 fop_real_div ->
f_real_div_simpl (f_real_mul_simpl f1 f2_2) f2_1
| Fapp (op, [f1_1; f1_2]), _ when f_equal op fop_real_div ->
f_real_div_simpl f1_1 (f_real_mul_simpl f1_2 f2)
| _ ->
try norm_real_int_div (destr_rint f1) (destr_rint f2)
with DestrError _ ->
if f_equal f2 f_r1 then f1 else f_real_div f1 f2
(* -------------------------------------------------------------------- *)
let rec f_let_simpl lp f1 f2 =
match lp with
| LSymbol (id, _) -> begin
match Mid.find_opt id (f_fv f2) with
| None -> f2
| Some i ->
if i = 1 || can_subst f1
then Fsubst.f_subst_local id f1 f2
else f_let lp f1 f2
end
| LTuple ids -> begin
match f1.f_node with
| Ftuple fs ->
let (d, s) =
List.fold_left2 (fun (d, s) (id, ty) f1 ->
match Mid.find_opt id (f_fv f2) with
| None -> (d, s)
| Some i ->
if i = 1 || can_subst f1
then (d, Mid.add id f1 s)
else (((id, ty), f1) :: d, s))
([], Mid.empty) ids fs
in
List.fold_left
(fun f2 (id, f1) -> f_let (LSymbol id) f1 f2)
(Fsubst.subst_locals s f2) d
| _ ->
let x = EcIdent.create "tpl" in
let ty = ttuple (List.map snd ids) in
let lpx = LSymbol(x,ty) in
let fx = f_local x ty in
let tu = f_tuple (List.mapi (fun i (_,ty') -> f_proj fx i ty') ids) in
f_let_simpl lpx f1 (f_let_simpl lp tu f2)
end
| LRecord (_, ids) ->
let check (id, _) =
id |> omap (fun id -> not (Mid.mem id (f_fv f2))) |> odfl true
in if List.for_all check ids then f2 else f_let lp f1 f2
let f_lets_simpl =
(* FIXME : optimize this *)
List.fold_right (fun (lp,f1) f2 -> f_let_simpl lp f1 f2)
let rec f_app_simpl f args ty =
f_betared (f_app f args ty)
and f_betared f =
let tx fo fp = if f_equal fo fp || can_betared fo then fp else f_betared fp in
match f.f_node with
| Fapp ({ f_node = Fquant (Llambda, bds, body)}, args) ->
let (bds1, bds2), (args1, args2) = List.prefix2 bds args in
let bind = fun subst (x, _) arg -> Fsubst.f_bind_local subst x arg in
let subst = Fsubst.f_subst_id in
let subst = List.fold_left2 bind subst bds1 args1 in
f_app (f_quant Llambda bds2 (Fsubst.f_subst ~tx subst body)) args2 f.f_ty
| _ -> f
and can_betared f =
match f.f_node with
| Fapp ({ f_node = Fquant (Llambda, _, _)}, _) -> true
| _ -> false
let f_forall_simpl b f =
let b = List.filter (fun (id,_) -> Mid.mem id (f_fv f)) b in
f_forall b f
let f_exists_simpl b f =
let b = List.filter (fun (id,_) -> Mid.mem id (f_fv f)) b in
f_exists b f
let f_quant_simpl q b f =
if q = Lforall then f_forall_simpl b f else f_exists b f
let f_not_simpl f =
if is_not f then destr_not f
else if is_true f then f_false
else if is_false f then f_true
else f_not f
let f_and_simpl f1 f2 =
if is_true f1 then f2
else if is_false f1 then f_false
else if is_true f2 then f1
else if is_false f2 then f_false
else f_and f1 f2
let f_ands_simpl = List.fold_right f_and_simpl
let f_anda_simpl f1 f2 =
if is_true f1 then f2
else if is_false f1 then f_false
else if is_true f2 then f1
else if is_false f2 then f_false
else f_anda f1 f2
let f_andas_simpl = List.fold_right f_anda_simpl
let f_or_simpl f1 f2 =
if is_true f1 then f_true
else if is_false f1 then f2
else if is_true f2 then f_true
else if is_false f2 then f1
else f_or f1 f2
let f_ora_simpl f1 f2 =
if is_true f1 then f_true
else if is_false f1 then f2
else if is_true f2 then f_true
else if is_false f2 then f1
else f_ora f1 f2
let f_imp_simpl f1 f2 =
if is_true f1 then f2
else if is_false f1 || is_true f2 then f_true
else if is_false f2 then f_not_simpl f1
else
if f_equal f1 f2 then f_true
else f_imp f1 f2
(* FIXME : simplify x = f1 => f2 into x = f1 => f2{x<-f2} *)
let bool_val f =
if is_true f then Some true
else if is_false f then Some false
else None
let f_proj_simpl f i ty =
match f.f_node with
| Ftuple args -> List.nth args i
| _ -> f_proj f i ty
let f_if_simpl f1 f2 f3 =
if f_equal f2 f3 then f2
else match bool_val f1, bool_val f2, bool_val f3 with
| Some true, _, _ -> f2
| Some false, _, _ -> f3
| _, Some true, _ -> f_imp_simpl (f_not_simpl f1) f3
| _, Some false, _ -> f_anda_simpl (f_not_simpl f1) f3
| _, _, Some true -> f_imp_simpl f1 f2
| _, _, Some false -> f_anda_simpl f1 f2
| _, _, _ -> f_if f1 f2 f3
let f_imps_simpl = List.fold_right f_imp_simpl
let rec f_iff_simpl f1 f2 =
if f_equal f1 f2 then f_true
else if is_true f1 then f2
else if is_false f1 then f_not_simpl f2
else if is_true f2 then f1
else if is_false f2 then f_not_simpl f1
else
match f1.f_node, f2.f_node with
| Fapp ({f_node = Fop (op1, [])}, [f1]),
Fapp ({f_node = Fop (op2, [])}, [f2]) when
(EcPath.p_equal op1 EcCoreLib.CI_Bool.p_not &&
EcPath.p_equal op2 EcCoreLib.CI_Bool.p_not)
-> f_iff_simpl f1 f2
| _ -> f_iff f1 f2
let rec f_eq_simpl f1 f2 =
if f_equal f1 f2 then f_true
else match f1.f_node, f2.f_node with
| Fint _ , Fint _ -> f_false
| Fapp (op1, [{f_node = Fint _}]), Fapp (op2, [{f_node = Fint _}])
when f_equal op1 f_op_real_of_int &&
f_equal op2 f_op_real_of_int
-> f_false
| Fop (op1, []), Fop (op2, []) when
(EcPath.p_equal op1 EcCoreLib.CI_Bool.p_true &&
EcPath.p_equal op2 EcCoreLib.CI_Bool.p_false )
|| (EcPath.p_equal op2 EcCoreLib.CI_Bool.p_true &&
EcPath.p_equal op1 EcCoreLib.CI_Bool.p_false )
-> f_false
| Ftuple fs1, Ftuple fs2 when List.length fs1 = List.length fs2 ->
f_andas_simpl (List.map2 f_eq_simpl fs1 fs2) f_true
| _ -> f_eq f1 f2
let f_int_le_simpl f1 f2 =
if f_equal f1 f2 then f_true
else match f1.f_node, f2.f_node with
| Fint x1, Fint x2 -> f_bool (BI.compare x1 x2 <= 0)
| _, _ -> f_int_le f1 f2
let f_int_lt_simpl f1 f2 =
if f_equal f1 f2 then f_false
else match f1.f_node, f2.f_node with
| Fint x1 , Fint x2 -> f_bool (BI.compare x1 x2 < 0)
| _, _ -> f_int_lt f1 f2
let f_real_le_simpl f1 f2 =
if f_equal f1 f2 then f_true else
match f1.f_node, f2.f_node with
| Fapp (op1, [{f_node = Fint x1}]), Fapp (op2, [{f_node = Fint x2}])
when f_equal op1 f_op_real_of_int
&& f_equal op2 f_op_real_of_int
-> f_bool (BI.compare x1 x2 <= 0)
| _, _ -> f_real_le f1 f2
let f_real_lt_simpl f1 f2 =
if f_equal f1 f2 then f_false else
match f1.f_node, f2.f_node with
| Fapp (op1, [{f_node = Fint x1}]), Fapp (op2, [{f_node = Fint x2}])
when f_equal op1 f_op_real_of_int
&& f_equal op2 f_op_real_of_int
-> f_bool (BI.compare x1 x2 < 0)
| _, _ -> f_real_lt f1 f2
(* -------------------------------------------------------------------- *)
type op_kind = [
| `True
| `False
| `Not
| `And of [`Asym | `Sym]
| `Or of [`Asym | `Sym]
| `Imp
| `Iff
| `Eq
| `Int_le
| `Int_lt
| `Real_le
| `Real_lt
| `Int_add
| `Int_sub
| `Int_mul
| `Int_pow
| `Int_opp
| `Real_add
| `Real_sub
| `Real_mul
| `Real_div
]
let operators =
let operators =
[EcCoreLib.CI_Bool.p_true , `True ;
EcCoreLib.CI_Bool.p_false , `False ;
EcCoreLib.CI_Bool.p_not , `Not ;
EcCoreLib.CI_Bool.p_anda , `And `Asym;
EcCoreLib.CI_Bool.p_and , `And `Sym ;
EcCoreLib.CI_Bool.p_ora , `Or `Asym;
EcCoreLib.CI_Bool.p_or , `Or `Sym ;
EcCoreLib.CI_Bool.p_imp , `Imp ;
EcCoreLib.CI_Bool.p_iff , `Iff ;
EcCoreLib.CI_Bool.p_eq , `Eq ;
EcCoreLib.CI_Int .p_int_le , `Int_le ;
EcCoreLib.CI_Int .p_int_lt , `Int_lt ;
EcCoreLib.CI_Int .p_int_add , `Int_add ;
EcCoreLib.CI_Int .p_int_sub , `Int_sub ;
EcCoreLib.CI_Int .p_int_mul , `Int_mul ;
EcCoreLib.CI_Int .p_int_opp , `Int_opp ;
EcCoreLib.CI_Int .p_int_pow , `Int_pow ;
EcCoreLib.CI_Real.p_real_add, `Real_add ;
EcCoreLib.CI_Real.p_real_sub, `Real_sub ;
EcCoreLib.CI_Real.p_real_mul, `Real_mul ;
EcCoreLib.CI_Real.p_real_div, `Real_div ;
EcCoreLib.CI_Real.p_real_le , `Real_le ;
EcCoreLib.CI_Real.p_real_lt , `Real_lt ; ]
in
let tbl = EcPath.Hp.create 11 in
List.iter (fun (p, k) -> EcPath.Hp.add tbl p k) operators;
tbl
(* -------------------------------------------------------------------- *)
let op_kind (p : EcPath.path) : op_kind option =
EcPath.Hp.find_opt operators p
(* -------------------------------------------------------------------- *)
let is_logical_op op =
match op_kind op with
| Some (
`Not | `And _ | `Or _ | `Imp | `Iff | `Eq
| `Int_le | `Int_lt | `Real_le | `Real_lt
| `Int_add | `Int_sub | `Int_mul
| `Real_add | `Real_sub | `Real_mul | `Real_div
) -> true
| _ -> false
(* -------------------------------------------------------------------- *)
type sform =
| SFint of BI.zint
| SFlocal of EcIdent.t
| SFpvar of EcTypes.prog_var * form
| SFglob of EcPath.mpath * form
| SFif of form * form * form
| SFmatch of form * form list * ty
| SFlet of lpattern * form * form
| SFtuple of form list
| SFproj of form * int
| SFquant of quantif * (EcIdent.t * gty) * form Lazy.t
| SFtrue
| SFfalse
| SFnot of form
| SFand of [`Asym | `Sym] * (form * form)
| SFor of [`Asym | `Sym] * (form * form)
| SFimp of form * form
| SFiff of form * form
| SFeq of form * form
| SFop of (EcPath.path * ty list) * (form list)
| SFhoareF of hoareF
| SFhoareS of hoareS
| SFbdHoareF of bdHoareF
| SFbdHoareS of bdHoareS
| SFequivF of equivF
| SFequivS of equivS
| SFpr of pr
| SFother of form
let sform_of_op (op, ty) args =
match op_kind op, args with
| Some (`True ), [] -> SFtrue
| Some (`False), [] -> SFfalse
| Some (`Not ), [f] -> SFnot f
| Some (`And b), [f1; f2] -> SFand (b, (f1, f2))
| Some (`Or b), [f1; f2] -> SFor (b, (f1, f2))
| Some (`Imp ), [f1; f2] -> SFimp (f1, f2)
| Some (`Iff ), [f1; f2] -> SFiff (f1, f2)
| Some (`Eq ), [f1; f2] -> SFeq (f1, f2)
| _ -> SFop ((op, ty), args)
let rec sform_of_form fp =
match fp.f_node with
| Fint i -> SFint i
| Flocal x -> SFlocal x
| Fpvar (x, me) -> SFpvar (x, me)
| Fglob (m, me) -> SFglob (m, me)
| Fif (c, f1, f2) -> SFif (c, f1, f2)
| Fmatch (b, fs, ty) -> SFmatch (b, fs, ty)
| Flet (lv, f1, f2) -> SFlet (lv, f1, f2)
| Ftuple fs -> SFtuple fs
| Fproj (f, i) -> SFproj (f,i)
| Fquant (_, [ ] , f) -> sform_of_form f
| Fquant (q, [b] , f) -> SFquant (q, b, lazy f)
| Fquant (q, b::bs, f) -> SFquant (q, b, lazy (f_quant q bs f))
| FhoareF hf -> SFhoareF hf
| FhoareS hs -> SFhoareS hs
| FbdHoareF hf -> SFbdHoareF hf
| FbdHoareS hs -> SFbdHoareS hs
| FequivF ef -> SFequivF ef
| FequivS es -> SFequivS es
| Fpr pr -> SFpr pr
| Fop (op, ty) ->
sform_of_op (op, ty) []
| Fapp ({ f_node = Fop (op, ty) }, args) ->
sform_of_op (op, ty) args
| _ -> SFother fp
(* destr_exists_prenex destructs recursively existentials in a formula
* whenever possible.
* For instance:
* - E x p1 /\ E y p2 -> [x,y] (p1 /\ p2)
* - E x p1 /\ E x p2 -> [] (E x p1 /\ E x p2)
* - p1 => E x p2 -> [x] (p1 => p2)
* - E x p1 => p2 -> [] (E x p1 => p2)
*)
(* Did we really need this function ? *)
let destr_exists_prenex f =
let disjoint bds1 bds2 =
List.for_all
(fun (id1, _) ->
List.for_all (fun (id2, _) -> not (EcIdent.id_equal id1 id2)) bds2)
bds1
in
let rec prenex_exists bds p =
match sform_of_form p with
| SFand (`Sym, (f1, f2)) ->
let (bds1, f1) = prenex_exists [] f1 in
let (bds2, f2) = prenex_exists [] f2 in
if disjoint bds1 bds2
then (bds1@bds2@bds, f_and f1 f2)
else (bds, p)
| SFor (`Sym, (f1, f2)) ->
let (bds1, f1) = prenex_exists [] f1 in
let (bds2, f2) = prenex_exists [] f2 in
if disjoint bds1 bds2
then (bds1@bds2@bds, f_or f1 f2)
else (bds, p)
| SFimp (f1, f2) ->
let (bds2, f2) = prenex_exists bds f2 in
(bds2@bds, f_imp f1 f2)
| SFquant (Lexists, bd, lazy p) ->
let (bds, p) = prenex_exists bds p in
(bd::bds, p)
| SFif (f, ft, fe) ->
let (bds1, f1) = prenex_exists [] ft in
let (bds2, f2) = prenex_exists [] fe in
if disjoint bds1 bds2
then (bds1@bds2@bds, f_if f f1 f2)
else (bds, p)
| _ -> (bds, p)
in
(* Make it fail as with destr_exists *)
match prenex_exists [] f with
| [] , _ -> destr_error "exists"
| bds, f -> (bds, f)
(* -------------------------------------------------------------------- *)
let get_lambda1 env f =
match decompose_lambda f with
| [], _ ->
let x = EcIdent.create "x" in
let t,ty = EcUnify.destr_tfun env f.f_ty in
x, t, f_app f [f_local x t] ty
| (x,t):: bd, b -> x, gty_as_ty t, f_lambda bd b
let open_mu_binding env f =
let mu,ty,f = get_lambda1 env f in
let mt = EcUnify.destr_tdmem env ty in
(mu,mt),f
let close_mu_binding (mu,mt) f =
f_lambda [mu, GTty (tdistr (tmem mt))] f
let f_pred2forall env f =
let x,t,f = get_lambda1 env f in
f_forall [x,GTty t] f
let destr_muf_b2r_not env f =
let destr_op_app op f =
let (op', _), args = destr_op_app f in
if not (EcPath.p_equal op op') then EcUtils.destr_error "op_app";
args in
let destr_op_app2 op f =
let args = destr_op_app op f in
if List.length args <> 2 then EcUtils.destr_error "op_app";
EcUtils.as_seq2 args in
let destr_op_app1 op f =
let args = destr_op_app op f in
if List.length args <> 1 then EcUtils.destr_error "op_app";
EcUtils.as_seq1 args in
let f1, fmu = destr_op_app2 EcCoreLib.CI_Distr.p_muf f in
let x,t,fbody = get_lambda1 env f1 in
(* check that fbody = b2r (! p ) *)
let np = destr_op_app1 EcCoreLib.CI_Real.p_b2r fbody in
let p = destr_not np in
f_lambda [x,GTty t] p, fmu
let is_muf_b2r_not env f = is_from_destr (destr_muf_b2r_not env) f