https://github.com/EasyCrypt/easycrypt
Tip revision: 7c35bc466c977edb46bcc1a4fc4e069c212f2a20 authored by Alley Stoughton on 28 April 2021, 13:36:14 UTC
Simplified recursion theorem to not use predecs, but just well-founded
Simplified recursion theorem to not use predecs, but just well-founded
Tip revision: 7c35bc4
ecMatching.ml
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2016 - IMDEA Software Institute
* Copyright (c) - 2012--2018 - Inria
* Copyright (c) - 2012--2018 - Ecole Polytechnique
*
* Distributed under the terms of the CeCILL-C-V1 license
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
(* Expressions / formulas matching for tactics *)
(* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
open EcUtils
open EcMaps
open EcIdent
open EcParsetree
open EcEnv
open EcTypes
open EcModules
open EcFol
open EcGenRegexp
(* -------------------------------------------------------------------- *)
module Zipper = struct
exception InvalidCPos
module P = EcPath
type ('a, 'state) folder =
'a -> 'state -> instr -> 'state * instr list
type ipath =
| ZTop
| ZWhile of expr * spath
| ZIfThen of expr * spath * stmt
| ZIfElse of expr * stmt * spath
and spath = (instr list * instr list) * ipath
type zipper = {
z_head : instr list; (* instructions on my left (rev) *)
z_tail : instr list; (* instructions on my right (me incl.) *)
z_path : ipath; (* path (zipper) leading to me *)
}
let cpos (i : int) : codepos1 = (0, `ByPos i)
let zipper hd tl zpr = { z_head = hd; z_tail = tl; z_path = zpr; }
let find_by_cp_match ((i, cm) : int option * cp_match) (s : stmt) =
let rec progress (acc : instr list) (s : instr list) (i : int) =
if i <= 0 then
let shd = oget (List.Exceptionless.hd acc) in
let stl = oget (List.Exceptionless.tl acc) in
(stl, shd, s)
else
let ir, s =
match s with [] -> raise InvalidCPos | ir :: s -> (ir, s)
in
let i =
match ir.i_node, cm with
| Swhile _, `While -> i-1
| Sif _, `If -> i-1
| Sasgn _, `Assign -> i-1
| Srnd _, `Sample -> i-1
| Scall _, `Call -> i-1
| _ , _ -> i
in progress (ir :: acc) s i
in
let i = odfl 1 i in if i = 0 then raise InvalidCPos;
let rev, i = (i < 0), abs i in
let s1, ir, s2 =
progress [] (if rev then List.rev s.s_node else s.s_node) i in
match rev with
| false -> (s1, ir, s2)
| true -> (s2, ir, s1)
let split_at_cp_base ~after (cb : cp_base) (s : stmt) =
match cb with
| `ByPos i -> begin
let i = if i < 0 then List.length s.s_node + i else i in
try List.takedrop (i - if after then 0 else 1) s.s_node
with (Invalid_argument _ | Not_found) -> raise InvalidCPos
end
| `ByMatch (i, cm) ->
let (s1, i, s2) = find_by_cp_match (i, cm) s in
match after with
| false -> (List.rev s1, i :: s2)
| true -> (List.rev_append s1 [i], s2)
let split_at_cpos1 ~after ((ipos, cb) : codepos1) s =
let (s1, s2) = split_at_cp_base ~after cb s in
let (s1, s2) =
match ipos with
| off when off > 0 ->
let (ss1, ss2) =
try List.takedrop off s2
with (Invalid_argument _ | Not_found) -> raise InvalidCPos in
(s1 @ ss1, ss2)
| off when off < 0 ->
let (ss1, ss2) =
try List.takedrop (List.length s1 + off) s1
with (Invalid_argument _ | Not_found) -> raise InvalidCPos in
(ss1, ss2 @ s2)
| _ -> (s1, s2)
in (s1, s2)
let find_by_cpos1 ?(rev = true) (cpos1 : codepos1) s =
match split_at_cpos1 ~after:false cpos1 s with
| (s1, i :: s2) -> ((if rev then List.rev s1 else s1), i, s2)
| _ -> raise InvalidCPos
let zipper_at_nm_cpos1 ((cp1, sub) : codepos1 * int) s zpr =
let (s1, i, s2) = find_by_cpos1 cp1 s in
match i.i_node, sub with
| Swhile (e, sw), 0 ->
(ZWhile (e, ((s1, s2), zpr)), sw)
| Sif (e, ifs1, ifs2), 0 ->
(ZIfThen (e, ((s1, s2), zpr), ifs2), ifs1)
| Sif (e, ifs1, ifs2), 1 ->
(ZIfElse (e, ifs1, ((s1, s2), zpr)), ifs2)
| _ -> raise InvalidCPos
let zipper_of_cpos ((nm, cp1) : codepos) s =
let zpr, s =
List.fold_left
(fun (zpr, s) nm1 -> zipper_at_nm_cpos1 nm1 s zpr)
(ZTop, s) nm in
let s1, i, s2 = find_by_cpos1 cp1 s in
zipper s1 (i :: s2) zpr
let split_at_cpos1 cpos1 s =
split_at_cpos1 ~after:true cpos1 s
let may_split_at_cpos1 ?(rev = false) cpos1 s =
ofdfl
(fun () -> if rev then (s.s_node, []) else ([], s.s_node))
(omap (split_at_cpos1^~ s) cpos1)
let rec zip i ((hd, tl), ip) =
let s = stmt (List.rev_append hd (List.ocons i tl)) in
match ip with
| ZTop -> s
| ZWhile (e, sp) -> zip (Some (i_while (e, s))) sp
| ZIfThen (e, sp, se) -> zip (Some (i_if (e, s, se))) sp
| ZIfElse (e, se, sp) -> zip (Some (i_if (e, se, s))) sp
let zip zpr = zip None ((zpr.z_head, zpr.z_tail), zpr.z_path)
let after ~strict zpr =
let rec doit acc ip =
match ip with
| ZTop -> acc
| ZWhile (_, ((_, is), ip)) -> doit (is :: acc) ip
| ZIfThen (_, ((_, is), ip), _) -> doit (is :: acc) ip
| ZIfElse (_, _, ((_, is), ip)) -> doit (is :: acc) ip
in
let after =
match zpr.z_tail, strict with
| [] , _ -> doit [[]] zpr.z_path
| is , false -> doit [is] zpr.z_path
| _ :: is, true -> doit [is] zpr.z_path
in
List.rev after
let rec fold env cpos f state s =
let zpr = zipper_of_cpos cpos s in
match zpr.z_tail with
| [] -> raise InvalidCPos
| i :: tl -> begin
match f env state i with
| (state', [i']) when i == i' && state == state' -> (state, s)
| (state', si ) -> (state', zip { zpr with z_tail = si @ tl })
end
end
(* -------------------------------------------------------------------- *)
type 'a evmap = {
ev_map : ('a option) Mid.t;
ev_unset : int;
}
module EV = struct
let empty : 'a evmap = {
ev_map = Mid.empty;
ev_unset = 0;
}
let add (x : ident) (m : 'a evmap) =
let chg = function Some _ -> assert false | None -> Some None in
let map = Mid.change chg x m.ev_map in
{ ev_map = map; ev_unset = m.ev_unset + 1; }
let mem (x : ident) (m : 'a evmap) =
EcUtils.is_some (Mid.find_opt x m.ev_map)
let set (x : ident) (v : 'a) (m : 'a evmap) =
let chg = function
| None | Some (Some _) -> assert false
| Some None -> Some (Some v)
in
{ ev_map = Mid.change chg x m.ev_map; ev_unset = m.ev_unset - 1; }
let get (x : ident) (m : 'a evmap) =
match Mid.find_opt x m.ev_map with
| None -> None
| Some None -> Some `Unset
| Some (Some a) -> Some (`Set a)
let isset (x : ident) (m : 'a evmap) =
match get x m with
| Some (`Set _) -> true
| _ -> false
let doget (x : ident) (m : 'a evmap) =
match get x m with
| Some (`Set a) -> a
| _ -> assert false
let of_idents (ids : ident list) : 'a evmap =
List.fold_left ((^~) add) empty ids
let fold (f : ident -> 'a -> 'b -> 'b) ev state =
Mid.fold
(fun x t s -> match t with Some t -> f x t s | None -> s)
ev.ev_map state
let filled (m : 'a evmap) = (m.ev_unset = 0)
end
(* -------------------------------------------------------------------- *)
type mevmap = {
evm_form : form evmap;
evm_mem : EcMemory.memory evmap;
evm_mod : EcPath.mpath evmap;
}
(* -------------------------------------------------------------------- *)
module MEV = struct
type item = [
| `Form of form
| `Mem of EcMemory.memory
| `Mod of EcPath.mpath
]
type kind = [ `Form | `Mem | `Mod ]
let empty : mevmap = {
evm_form = EV.empty;
evm_mem = EV.empty;
evm_mod = EV.empty;
}
let of_idents ids k =
match k with
| `Form -> { empty with evm_form = EV.of_idents ids }
| `Mem -> { empty with evm_mem = EV.of_idents ids }
| `Mod -> { empty with evm_mod = EV.of_idents ids }
let add x k m =
match k with
| `Form -> { m with evm_form = EV.add x m.evm_form }
| `Mem -> { m with evm_mem = EV.add x m.evm_mem }
| `Mod -> { m with evm_mod = EV.add x m.evm_mod }
let mem x k m =
match k with
| `Form -> EV.mem x m.evm_form
| `Mem -> EV.mem x m.evm_mem
| `Mod -> EV.mem x m.evm_mod
let set x v m =
match v with
| `Form v -> { m with evm_form = EV.set x v m.evm_form }
| `Mem v -> { m with evm_mem = EV.set x v m.evm_mem }
| `Mod v -> { m with evm_mod = EV.set x v m.evm_mod }
let get x k m =
let tx f = function `Unset -> `Unset | `Set x -> `Set (f x) in
match k with
| `Form -> omap (tx (fun x -> `Form x)) (EV.get x m.evm_form)
| `Mem -> omap (tx (fun x -> `Mem x)) (EV.get x m.evm_mem )
| `Mod -> omap (tx (fun x -> `Mod x)) (EV.get x m.evm_mod )
let isset x k m =
match k with
| `Form -> EV.isset x m.evm_form
| `Mem -> EV.isset x m.evm_mem
| `Mod -> EV.isset x m.evm_mod
let filled m =
EV.filled m.evm_form
&& EV.filled m.evm_mem
&& EV.filled m.evm_mod
let fold (f : _ -> item -> _ -> _) m v =
let v = EV.fold (fun x k v -> f x (`Form k) v) m.evm_form v in
let v = EV.fold (fun x k v -> f x (`Mem k) v) m.evm_mem v in
let v = EV.fold (fun x k v -> f x (`Mod k) v) m.evm_mod v in
v
let assubst ue ev =
let tysubst = { ty_subst_id with ts_u = EcUnify.UniEnv.assubst ue } in
let subst = Fsubst.f_subst_init ~sty:tysubst () in
let subst = EV.fold (fun x m s -> Fsubst.f_bind_mem s x m) ev.evm_mem subst in
let subst = EV.fold (fun x m s -> Fsubst.f_bind_mod s x m) ev.evm_mod subst in
let seen = ref Sid.empty in
let rec for_ident x binding subst =
if Sid.mem x !seen then subst else begin
seen := Sid.add x !seen;
match binding with None -> subst | Some f ->
let subst =
Mid.fold2_inter (fun x bdx _ -> for_ident x bdx)
ev.evm_form.ev_map f.f_fv subst in
Fsubst.f_bind_local subst x (Fsubst.f_subst subst f)
end
in
Mid.fold_left
(fun acc x bd -> for_ident x bd acc)
subst ev.evm_form.ev_map
end
(* -------------------------------------------------------------------- *)
exception MatchFailure
type fmoptions = {
fm_delta : bool;
fm_conv : bool;
fm_horder : bool;
}
let fmsearch =
{ fm_delta = false;
fm_conv = false;
fm_horder = true ; }
let fmrigid = {
fm_delta = false;
fm_conv = true ;
fm_horder = true ; }
let fmdelta = {
fm_delta = true ;
fm_conv = true ;
fm_horder = true ; }
let fmnotation = {
fm_delta = false;
fm_conv = false;
fm_horder = false; }
(* -------------------------------------------------------------------- *)
(* Rigid unification *)
let f_match_core opts hyps (ue, ev) ~ptn subject =
let ue = EcUnify.UniEnv.copy ue in
let ev = ref ev in
let iscvar = function
| { f_node = Flocal x } -> is_none (EV.get x !ev.evm_form)
| _ -> false
in
let conv =
match opts.fm_conv with
| true -> EcReduction.is_conv ~ri:EcReduction.full_compat hyps
| false -> EcReduction.is_alpha_eq hyps
in
let rec doit env ((subst, mxs) as ilc) ptn subject =
let failure =
let oue, oev = (EcUnify.UniEnv.copy ue, !ev) in
fun () ->
EcUnify.UniEnv.restore ~dst:ue ~src:oue; ev := oev;
raise MatchFailure
in
let default () =
if opts.fm_conv then begin
let subject = Fsubst.f_subst subst subject in
let ptn = Fsubst.f_subst (MEV.assubst ue !ev) ptn in
if not (conv ptn subject) then
failure ()
end else failure ()
in
try
match ptn.f_node, subject.f_node with
| Flocal x1, Flocal x2 when Mid.mem x1 mxs -> begin
if not (id_equal (oget (Mid.find_opt x1 mxs)) x2) then
failure ();
try EcUnify.unify env ue ptn.f_ty subject.f_ty
with EcUnify.UnificationFailure _ -> failure ()
end
| Flocal x1, Flocal x2 when id_equal x1 x2 -> begin
try EcUnify.unify env ue ptn.f_ty subject.f_ty
with EcUnify.UnificationFailure _ -> failure ()
end
| Flocal x, _ -> begin
match EV.get x !ev.evm_form with
| None ->
raise MatchFailure
| Some `Unset ->
let ssbj = Fsubst.f_subst subst subject in
let ssbj = Fsubst.f_subst (MEV.assubst ue !ev) ssbj in
if not (Mid.set_disjoint mxs ssbj.f_fv) then
raise MatchFailure;
begin
try EcUnify.unify env ue ptn.f_ty subject.f_ty
with EcUnify.UnificationFailure _ -> failure ();
end;
ev := { !ev with evm_form = EV.set x ssbj !ev.evm_form }
| Some (`Set a) -> begin
let ssbj = Fsubst.f_subst subst subject in
if not (conv ssbj a) then
let ssbj = Fsubst.f_subst (MEV.assubst ue !ev) subject in
if not (conv ssbj a) then
doit env ilc a ssbj
else
try EcUnify.unify env ue ptn.f_ty subject.f_ty
with EcUnify.UnificationFailure _ -> failure ()
else
try EcUnify.unify env ue ptn.f_ty subject.f_ty
with EcUnify.UnificationFailure _ -> failure ()
end
end
| Fapp (f1, fs1), _ -> begin
try
match subject.f_node with
| Fapp (f2, fs2) -> begin
try doit_args env ilc (f1::fs1) (f2::fs2)
with MatchFailure when opts.fm_conv ->
let rptn = f_betared ptn in
if (ptn.f_tag <> rptn.f_tag)
then doit env ilc rptn subject
else failure ()
end
| _ -> failure ()
with MatchFailure when opts.fm_horder ->
match f1.f_node with
| Flocal f when
not (Mid.mem f mxs)
&& (EV.get f !ev.evm_form = Some `Unset)
&& List.for_all iscvar fs1
->
let oargs = List.map destr_local fs1 in
if not (List.is_unique ~eq:id_equal oargs) then
failure ();
let xsubst, bindings =
List.map_fold
(fun xsubst x ->
let x, xty = (destr_local x, x.f_ty) in
let nx = EcIdent.fresh x in
let xsubst =
Mid.find_opt x mxs
|> omap (fun y -> Fsubst.f_bind_rename xsubst y nx xty)
|> odfl xsubst
in (xsubst, (nx, GTty xty)))
Fsubst.f_subst_id fs1 in
let ssbj = Fsubst.f_subst xsubst subject in
let ssbj = Fsubst.f_subst subst ssbj in
if not (Mid.set_disjoint mxs ssbj.f_fv) then
failure ();
begin
let fty = toarrow (List.map f_ty fs1) ssbj.f_ty in
try EcUnify.unify env ue f1.f_ty fty
with EcUnify.UnificationFailure _ -> failure ();
end;
let ssbj = f_lambda bindings ssbj in
ev := { !ev with evm_form = EV.set f ssbj !ev.evm_form }
| _ -> default ()
end
| Fquant (b1, q1, f1), Fquant (b2, q2, f2) when b1 = b2 ->
let n1, n2 = List.length q1, List.length q2 in
let q1, r1 = List.split_at (min n1 n2) q1 in
let q2, r2 = List.split_at (min n1 n2) q2 in
let (env, subst, mxs) = doit_bindings env (subst, mxs) q1 q2 in
doit env (subst, mxs) (f_quant b1 r1 f1) (f_quant b2 r2 f2)
| Fquant _, Fquant _ ->
failure ();
| Fpvar (pv1, m1), Fpvar (pv2, m2) ->
let pv1 = EcEnv.NormMp.norm_pvar env pv1 in
let pv2 = EcEnv.NormMp.norm_pvar env pv2 in
if not (EcTypes.pv_equal pv1 pv2) then
failure ();
doit_mem env mxs m1 m2
| Fif (c1, t1, e1), Fif (c2, t2, e2) ->
List.iter2 (doit env ilc) [c1; t1; e1] [c2; t2; e2]
| Fmatch (b1, fs1, ty1), Fmatch (b2, fs2, ty2) -> begin
(try EcUnify.unify env ue ty1 ty2
with EcUnify.UnificationFailure _ -> failure ());
if List.length fs1 <> List.length fs2 then
failure ();
List.iter2 (doit env ilc) (b1 :: fs1) (b2 :: fs2)
end
| Fint i1, Fint i2 ->
if not (EcBigInt.equal i1 i2) then failure ();
| Fglob (mp1, me1), Fglob (mp2, me2) ->
let mp1 = EcEnv.NormMp.norm_mpath env mp1 in
let mp2 = EcEnv.NormMp.norm_mpath env mp2 in
if not (EcPath.m_equal mp1 mp2) then
failure ();
doit_mem env mxs me1 me2
| Ftuple fs1, Ftuple fs2 ->
if List.length fs1 <> List.length fs2 then
failure ();
List.iter2 (doit env ilc) fs1 fs2
| Fproj (f1, i), Fproj (f2, j) ->
if i <> j then failure () else doit env ilc f1 f2
| Fop (op1, tys1), Fop (op2, tys2) -> begin
if not (EcPath.p_equal op1 op2) then
failure ();
try List.iter2 (EcUnify.unify env ue) tys1 tys2
with EcUnify.UnificationFailure _ -> failure ()
end
| FhoareF hf1, FhoareF hf2 -> begin
if not (EcReduction.EqTest.for_xp env hf1.hf_f hf2.hf_f) then
failure ();
let mxs = Mid.add EcFol.mhr EcFol.mhr mxs in
List.iter2 (doit env (subst, mxs))
[hf1.hf_pr; hf1.hf_po] [hf2.hf_pr; hf2.hf_po]
end
| FbdHoareF hf1, FbdHoareF hf2 -> begin
if not (EcReduction.EqTest.for_xp env hf1.bhf_f hf2.bhf_f) then
failure ();
if hf1.bhf_cmp <> hf2.bhf_cmp then
failure ();
let mxs = Mid.add EcFol.mhr EcFol.mhr mxs in
List.iter2 (doit env (subst, mxs))
[hf1.bhf_pr; hf1.bhf_po; hf1.bhf_bd]
[hf2.bhf_pr; hf2.bhf_po; hf2.bhf_bd]
end
| FequivF hf1, FequivF hf2 -> begin
if not (EcReduction.EqTest.for_xp env hf1.ef_fl hf2.ef_fl) then
failure ();
if not (EcReduction.EqTest.for_xp env hf1.ef_fr hf2.ef_fr) then
failure();
let mxs = Mid.add EcFol.mleft EcFol.mleft mxs in
let mxs = Mid.add EcFol.mright EcFol.mright mxs in
List.iter2
(doit env (subst, mxs))
[hf1.ef_pr; hf1.ef_po] [hf2.ef_pr; hf2.ef_po]
end
| Fpr pr1, Fpr pr2 -> begin
if not (EcReduction.EqTest.for_xp env pr1.pr_fun pr2.pr_fun) then
failure ();
doit_mem env mxs pr1.pr_mem pr2.pr_mem;
let mxs = Mid.add EcFol.mhr EcFol.mhr mxs in
List.iter2
(doit env (subst, mxs))
[pr1.pr_args; pr1.pr_event] [pr2.pr_args; pr2.pr_event]
end
| _, _ -> default ()
with MatchFailure when opts.fm_delta ->
match fst_map f_node (destr_app ptn),
fst_map f_node (destr_app subject)
with
| (Fop (op1, tys1), args1), (Fop (op2, tys2), args2) -> begin
(* try
if not (EcPath.p_equal op1 op2) then
failure ();
try
List.iter2 (EcUnify.unify env ue) tys1 tys2;
doit_args env ilc args1 args2
with EcUnify.UnificationFailure _ -> failure ()
with MatchFailure -> *)
(* Benj: Fixme user reduction ... *)
if EcEnv.Op.reducible env op1 then
doit_reduce env ((doit env ilc)^~ subject) ptn.f_ty op1 tys1 args1
else if EcEnv.Op.reducible env op2 then
doit_reduce env (doit env ilc ptn) subject.f_ty op2 tys2 args2
else
failure ()
end
| (Flocal x1, args1), _ when LDecl.can_unfold x1 hyps ->
doit_lreduce env ((doit env ilc)^~ subject) ptn.f_ty x1 args1
| _, (Flocal x2, args2) when LDecl.can_unfold x2 hyps ->
doit_lreduce env (doit env ilc ptn) subject.f_ty x2 args2
| (Fop (op1, tys1), args1), _ when EcEnv.Op.reducible env op1 ->
doit_reduce env ((doit env ilc)^~ subject) ptn.f_ty op1 tys1 args1
| _, (Fop (op2, tys2), args2) when EcEnv.Op.reducible env op2 ->
doit_reduce env (doit env ilc ptn) subject.f_ty op2 tys2 args2
| _, _ -> failure ()
and doit_args env ilc fs1 fs2 =
if List.length fs1 <> List.length fs2 then
raise MatchFailure;
List.iter2 (doit env ilc) fs1 fs2
and doit_reduce env cb ty op tys args =
let reduced =
try f_app (EcEnv.Op.reduce env op tys) args ty
with NotReducible -> raise MatchFailure in
cb (odfl reduced (EcReduction.h_red_opt EcReduction.beta_red hyps reduced))
and doit_lreduce _env cb ty x args =
let reduced =
try f_app (LDecl.unfold x hyps) args ty
with LookupFailure _ -> raise MatchFailure in
cb (odfl reduced (EcReduction.h_red_opt EcReduction.beta_red hyps reduced))
and doit_mem _env mxs m1 m2 =
match EV.get m1 !ev.evm_mem with
| None ->
if not (EcMemory.mem_equal m1 m2) then
raise MatchFailure
| Some `Unset ->
if Mid.mem m2 mxs then
raise MatchFailure;
ev := { !ev with evm_mem = EV.set m1 m2 !ev.evm_mem }
| Some (`Set m1) ->
if not (EcMemory.mem_equal m1 m2) then
raise MatchFailure
and doit_bindings env (subst, mxs) q1 q2 =
let doit_binding (env, subst, mxs) (x1, gty1) (x2, gty2) =
let gty2 = Fsubst.gty_subst subst gty2 in
assert (not (Mid.mem x1 mxs) && not (Mid.mem x2 mxs));
let env, subst =
match gty1, gty2 with
| GTty ty1, GTty ty2 ->
begin
try EcUnify.unify env ue ty1 ty2
with EcUnify.UnificationFailure _ -> raise MatchFailure
end;
let subst =
if id_equal x1 x2
then subst
else Fsubst.f_bind_rename subst x2 x1 ty2
and env = EcEnv.Var.bind_local x1 ty1 env in
(env, subst)
| GTmem None, GTmem None ->
(env, subst)
| GTmem (Some m1), GTmem (Some m2) ->
let xp1 = EcMemory.lmt_xpath m1 in
let xp2 = EcMemory.lmt_xpath m2 in
let m1 = EcMemory.lmt_bindings m1 in
let m2 = EcMemory.lmt_bindings m2 in
if not (EcPath.x_equal xp1 xp2) then
raise MatchFailure;
if not (
try
EcSymbols.Msym.equal
(fun (p1,ty1) (p2,ty2) ->
if p1 <> p2 then raise MatchFailure;
EcUnify.unify env ue ty1 ty2; true)
m1 m2
with EcUnify.UnificationFailure _ -> raise MatchFailure)
then
raise MatchFailure;
let subst =
if id_equal x1 x2
then subst
else Fsubst.f_bind_mem subst x2 x1
in (env, subst)
| GTmodty (p1, r1), GTmodty (p2, r2) ->
if not (ModTy.mod_type_equiv env p1 p2) then
raise MatchFailure;
if not (NormMp.equal_restr env r1 r2) then
raise MatchFailure;
let subst =
if id_equal x1 x2
then subst
else Fsubst.f_bind_mod subst x2 (EcPath.mident x1)
and env = EcEnv.Mod.bind_local x1 p1 r1 env in
(env, subst)
| _, _ -> raise MatchFailure
in
(env, subst, Mid.add x1 x2 mxs)
in
List.fold_left2 doit_binding (env, subst, mxs) q1 q2
in
doit (EcEnv.LDecl.toenv hyps) (Fsubst.f_subst_id, Mid.empty) ptn subject;
(ue, !ev)
let f_match opts hyps (ue, ev) ~ptn subject =
let (ue, ev) = f_match_core opts hyps (ue, ev) ~ptn subject in
if not (MEV.filled ev) then
raise MatchFailure;
let clue =
try EcUnify.UniEnv.close ue
with EcUnify.UninstanciateUni -> raise MatchFailure
in
(ue, clue, ev)
(* -------------------------------------------------------------------- *)
type ptnpos = [`Select of int | `Sub of ptnpos] Mint.t
type occ = [`Inclusive | `Exclusive] * Sint.t
exception InvalidPosition
exception InvalidOccurence
module FPosition = struct
type select = [`Accept of int | `Continue]
(* ------------------------------------------------------------------ *)
let empty : ptnpos = Mint.empty
(* ------------------------------------------------------------------ *)
let is_empty (p : ptnpos) = Mint.is_empty p
(* ------------------------------------------------------------------ *)
let rec tostring (p : ptnpos) =
let items = Mint.bindings p in
let items =
List.map
(fun (i, p) -> Printf.sprintf "%d[%s]" i (tostring1 p))
items
in
String.concat ", " items
(* ------------------------------------------------------------------ *)
and tostring1 = function
| `Select i when i < 0 -> "-"
| `Select i -> Printf.sprintf "-(%d)" i
| `Sub p -> tostring p
(* ------------------------------------------------------------------ *)
let occurences =
let rec doit1 n p =
match p with
| `Select _ -> n+1
| `Sub p -> doit n p
and doit n (ps : ptnpos) =
Mint.fold (fun _ p n -> doit1 n p) ps n
in
fun p -> doit 0 p
(* ------------------------------------------------------------------ *)
let filter ((mode, s) : occ) =
let rec doit1 n p =
match p with
| `Select _ -> begin
match mode with
| `Inclusive -> (n+1, if Sint.mem n s then Some p else None )
| `Exclusive -> (n+1, if Sint.mem n s then None else Some p)
end
| `Sub p -> begin
match doit n p with
| (n, sub) when Mint.is_empty sub -> (n, None)
| (n, sub) -> (n, Some (`Sub sub))
end
and doit n (ps : ptnpos) =
Mint.mapi_filter_fold (fun _ p n -> doit1 n p) ps n
in
fun p -> snd (doit 1 p)
(* ------------------------------------------------------------------ *)
let is_occurences_valid o cpos =
let (min, max) = (Sint.min_elt o, Sint.max_elt o) in
not (min < 1 || max > occurences cpos)
(* ------------------------------------------------------------------ *)
let select ?o test =
let rec doit1 ctxt pos fp =
match test ctxt fp with
| `Accept i -> Some (`Select i)
| `Continue -> begin
let subp =
match fp.f_node with
| Fif (c, f1, f2) -> doit pos (`WithCtxt (ctxt, [c; f1; f2]))
| Fapp (f, fs) -> doit pos (`WithCtxt (ctxt, f :: fs))
| Ftuple fs -> doit pos (`WithCtxt (ctxt, fs))
| Fmatch (b, fs, _) ->
doit pos (`WithCtxt (ctxt, b :: fs))
| Fquant (_, b, f) ->
let xs = List.pmap (function (x, GTty _) -> Some x | _ -> None) b in
let ctxt = List.fold_left ((^~) Sid.add) ctxt xs in
doit pos (`WithCtxt (ctxt, [f]))
| Flet (lp, f1, f2) ->
let subctxt = List.fold_left ((^~) Sid.add) ctxt (lp_ids lp) in
doit pos (`WithSubCtxt [(ctxt, f1); (subctxt, f2)])
| Fproj (f, _) ->
doit pos (`WithCtxt (ctxt, [f]))
| Fpr pr ->
let subctxt = Sid.add pr.pr_mem ctxt in
doit pos (`WithSubCtxt [(ctxt, pr.pr_args); (subctxt, pr.pr_event)])
| FhoareF hs ->
doit pos (`WithCtxt (Sid.add EcFol.mhr ctxt, [hs.hf_pr; hs.hf_po]))
| FbdHoareF hs ->
let subctxt = Sid.add EcFol.mhr ctxt in
doit pos (`WithSubCtxt ([(subctxt, hs.bhf_pr);
(subctxt, hs.bhf_po);
( ctxt, hs.bhf_bd)]))
| FequivF es ->
let ctxt = Sid.add EcFol.mleft ctxt in
let ctxt = Sid.add EcFol.mright ctxt in
doit pos (`WithCtxt (ctxt, [es.ef_pr; es.ef_po]))
| _ -> None
in
omap (fun p -> `Sub p) subp
end
and doit pos fps =
let fps =
match fps with
| `WithCtxt (ctxt, fps) ->
List.mapi
(fun i fp ->
doit1 ctxt (i::pos) fp |> omap (fun p -> (i, p)))
fps
| `WithSubCtxt fps ->
List.mapi
(fun i (ctxt, fp) ->
doit1 ctxt (i::pos) fp |> omap (fun p -> (i, p)))
fps
in
let fps = List.pmap identity fps in
match fps with
| [] -> None
| _ -> Some (Mint.of_list fps)
in
fun fp ->
let cpos =
match doit [] (`WithCtxt (Sid.empty, [fp])) with
| None -> Mint.empty
| Some p -> p
in
match o with
| None -> cpos
| Some o ->
if not (is_occurences_valid (snd o) cpos) then
raise InvalidOccurence;
filter o cpos
(* ------------------------------------------------------------------ *)
let select_form ?(xconv = `Conv) ?(keyed = false) hyps o p target =
let na = List.length (snd (EcFol.destr_app p)) in
let kmatch key tp =
match key, (fst (destr_app tp)).f_node with
| `NoKey , _ -> true
| `Path p, Fop (p', _) -> EcPath.p_equal p p'
| `Path _, _ -> false
| `Var x, Flocal x' -> id_equal x x'
| `Var _, _ -> false
in
let keycheck tp key = not keyed || kmatch key tp in
let key =
match (fst (destr_app p)).f_node with
| Fop (p, _) -> `Path p
| Flocal x -> `Var x
| _ -> `NoKey
in
let test xconv _ tp =
if not (keycheck tp key) then `Continue else begin
let (tp, ti) =
match tp.f_node with
| Fapp (h, hargs) when List.length hargs > na ->
let (a1, a2) = List.takedrop na hargs in
(f_app h a1 (toarrow (List.map f_ty a2) tp.f_ty), na)
| _ -> (tp, -1)
in
if EcReduction.xconv xconv hyps p tp then `Accept ti else `Continue
end
in select ?o (test xconv) target
(* ------------------------------------------------------------------ *)
let map (p : ptnpos) (tx : form -> form) (f : form) =
let rec doit1 p fp =
match p with
| `Select i when i < 0 -> tx fp
| `Select i -> begin
let (f, fs) = EcFol.destr_app fp in
if List.length fs < i then raise InvalidPosition;
let (fs1, fs2) = List.takedrop i fs in
let f' = f_app f fs1 (toarrow (List.map f_ty fs2) fp.f_ty) in
f_app (tx f') fs2 fp.f_ty
end
| `Sub p -> begin
match fp.f_node with
| Flocal _ -> raise InvalidPosition
| Fpvar _ -> raise InvalidPosition
| Fglob _ -> raise InvalidPosition
| Fop _ -> raise InvalidPosition
| Fint _ -> raise InvalidPosition
| Fquant (q, b, f) ->
let f' = as_seq1 (doit p [f]) in
FSmart.f_quant (fp, (q, b, f)) (q, b, f')
| Fif (c, f1, f2) ->
let (c', f1', f2') = as_seq3 (doit p [c; f1; f2]) in
FSmart.f_if (fp, (c, f1, f2)) (c', f1', f2')
| Fmatch (b, fs, ty) ->
let bfs = doit p (b :: fs) in
FSmart.f_match (fp, (b, fs, ty)) (List.hd bfs, List.tl bfs, ty)
| Fapp (f, fs) -> begin
match doit p (f :: fs) with
| [] -> assert false
| f' :: fs' ->
FSmart.f_app (fp, (f, fs, fp.f_ty)) (f', fs', fp.f_ty)
end
| Ftuple fs ->
let fs' = doit p fs in
FSmart.f_tuple (fp, fs) fs'
| Fproj (f, i) ->
FSmart.f_proj (fp, (f, fp.f_ty)) (as_seq1 (doit p [f]), fp.f_ty) i
| Flet (lv, f1, f2) ->
let (f1', f2') = as_seq2 (doit p [f1; f2]) in
FSmart.f_let (fp, (lv, f1, f2)) (lv, f1', f2')
| Fpr pr ->
let (args', event') = as_seq2 (doit p [pr.pr_args; pr.pr_event]) in
f_pr pr.pr_mem pr.pr_fun args' event'
| FhoareF hf ->
let (hf_pr, hf_po) = as_seq2 (doit p [hf.hf_pr; hf.hf_po]) in
f_hoareF_r { hf with hf_pr; hf_po; }
| FbdHoareF hf ->
let sub = doit p [hf.bhf_pr; hf.bhf_po; hf.bhf_bd] in
let (bhf_pr, bhf_po, bhf_bd) = as_seq3 sub in
f_bdHoareF_r { hf with bhf_pr; bhf_po; bhf_bd; }
| FequivF ef ->
let (ef_pr, ef_po) = as_seq2 (doit p [ef.ef_pr; ef.ef_po]) in
f_equivF_r { ef with ef_pr; ef_po; }
| FhoareS _ -> raise InvalidPosition
| FbdHoareS _ -> raise InvalidPosition
| FequivS _ -> raise InvalidPosition
| FeagerF _ -> raise InvalidPosition
end
and doit ps fps =
match Mint.is_empty ps with
| true -> fps
| false ->
let imin = fst (Mint.min_binding ps)
and imax = fst (Mint.max_binding ps) in
if imin < 0 || imax >= List.length fps then
raise InvalidPosition;
let fps = List.mapi (fun i x -> (x, Mint.find_opt i ps)) fps in
let fps = List.map (function (f, None) -> f | (f, Some p) -> doit1 p f) fps in
fps
in
as_seq1 (doit p [f])
(* ------------------------------------------------------------------ *)
let topattern ?x (p : ptnpos) (f : form) =
let x = match x with None -> EcIdent.create "_p" | Some x -> x in
let tx fp = f_local x fp.f_ty in (x, map p tx f)
end
(* -------------------------------------------------------------------- *)
type cptenv = CPTEnv of f_subst
let can_concretize ev ue =
EcUnify.UniEnv.closed ue && MEV.filled ev
(* -------------------------------------------------------------------------- *)
type regexp_instr = regexp1_instr gen_regexp
and regexp1_instr =
| RAssign (*of lvalue * expr*)
| RSample (*of lvalue * expr*)
| RCall (*of lvalue option * EcPath.xpath * expr list*)
| RIf of (*expr *) regexp_instr * regexp_instr
| RWhile of (*expr *) regexp_instr
module RegexpBaseInstr = struct
open Zipper
type regexp = regexp_instr
type regexp1 = regexp1_instr
type pos = int
type path = int list
type subject = instr list
type engine = {
e_zipper : zipper;
e_pos : pos;
e_path : pos list;
}
let mkengine (s : subject) = {
e_zipper = zipper [] s ZTop;
e_pos = 0;
e_path = [];
}
let position (e : engine) =
e.e_pos
let at_start (e : engine) =
List.is_empty e.e_zipper.z_head
let at_end (e : engine) =
List.is_empty e.e_zipper.z_tail
let path (e : engine) =
e.e_pos :: e.e_path
let eat_option (f : 'a -> 'a -> unit) (x : 'a option) (xn : 'a option) =
match x, xn with
| None , Some _ -> raise NoMatch
| Some _, None -> raise NoMatch
| None , None -> ()
| Some x, Some y -> f x y
let eat_list (f : 'a -> 'a -> unit) (x : 'a list) (xn : 'a list) =
try List.iter2 f x xn
with Invalid_argument _ -> raise NoMatch (* FIXME *)
let eat_lvalue (lv : lvalue) (lvn : lvalue) =
if not (lv_equal lv lvn) then raise NoMatch
let eat_expr (e : expr) (en : expr) =
if not (e_equal e en) then raise NoMatch
let eat_xpath (f : EcPath.xpath) (fn : EcPath.xpath) =
if not (EcPath.x_equal f fn) then raise NoMatch
let rec eat_base (eng : engine) (r : regexp1) =
let z = eng.e_zipper in
match z.z_tail with
| [] -> raise NoMatch
| i :: tail -> begin
match (i.i_node,r) with
| Sasgn _, RAssign
| Srnd _, RSample
| Scall _, RCall -> (eat eng, [])
| Sif (e, st, sf), RIf (stn, sfn) -> begin
let e_t = mkengine st.s_node in
let e_t =
let zp = ZIfThen (e, ((z.z_head, tail), z.z_path), sf) in
let zp = { e_t.e_zipper with z_path = zp; } in
{ e_t with e_path = 0 :: eng.e_pos :: eng.e_path; e_zipper = zp; } in
let e_f = mkengine sf.s_node in
let e_f =
let zp = ZIfElse (e, st, ((z.z_head, tail), z.z_path)) in
let zp = { e_f.e_zipper with z_path = zp; } in
{ e_f with e_path = 1 :: eng.e_pos :: eng.e_path; e_zipper = zp; } in
(eat eng, [(e_t, stn); (e_f, sfn)])
end
| Swhile (e, s), RWhile sn -> begin
let es = mkengine s.s_node in
let es =
let zp = ZWhile (e, ((z.z_head, tail), z.z_path)) in
let zp = { es.e_zipper with z_path = zp; } in
{ es with e_path = 0 :: eng.e_pos :: eng.e_path; e_zipper = zp; } in
(eat eng, [(es, sn)])
end
| _, _ -> raise NoMatch
end
and eat (e : engine) = {
e with e_zipper = zip_eat e.e_zipper;
e_pos = e.e_pos + 1;
}
and zip_eat (z : zipper) =
match z.z_tail with
| [] -> raise NoMatch
| i :: tail -> zipper (i :: z.z_head) tail z.z_path
let extract (e : engine) ((lo, hi) : pos * pos) =
if hi <= lo then [] else
let s = List.rev_append e.e_zipper.z_head e.e_zipper.z_tail in
List.of_enum (List.enum s |> Enum.skip lo |> Enum.take (hi-lo))
let rec next_zipper (z : zipper) =
match z.z_tail with
| i :: tail ->
begin match i.i_node with
| Sif (e, stmttrue, stmtfalse) ->
let z = (i::z.z_head, tail), z.z_path in
let path = ZIfThen (e, z, stmtfalse) in
let z' = zipper [] stmttrue.s_node path in
Some z'
| Swhile (e, block) ->
let z = (i::z.z_head, tail), z.z_path in
let path = ZWhile (e, z) in
let z' = zipper [] block.s_node path in
Some z'
| Sasgn _ | Srnd _ | Scall _ | _ ->
Some { z with z_head = i :: z.z_head ; z_tail = tail }
end
| [] ->
match z.z_path with
| ZTop -> None
| ZWhile (_e, ((head, tail), path)) ->
let z' = zipper head tail path in
next_zipper z'
| ZIfThen (e, father, stmtfalse) ->
let stmttrue = stmt (List.rev z.z_head) in
let z' = zipper [] stmtfalse.s_node (ZIfElse (e, stmttrue, father)) in
next_zipper z'
| ZIfElse (_e, _stmttrue, ((head, tail), path)) ->
let z' = zipper head tail path in
next_zipper z'
let next (e : engine) =
next_zipper e.e_zipper |> omap (fun z ->
{ e with e_zipper = z; e_pos = List.length z.z_head })
end
module RegexpStmt = EcGenRegexp.Regexp(RegexpBaseInstr)