From 6fd85e8ca4887f7cbca62a0e0790f43e11a23d36 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Tue, 29 Mar 2022 12:28:41 +0200 Subject: [PATCH] [matching]: when crossing a binder, update the env. accordingly --- src/ecEnv.ml | 13 +++--- src/ecEnv.mli | 2 +- src/ecHiGoal.ml | 4 +- src/ecMatching.ml | 100 ++++++++++++++++++++++++++++--------------- src/ecMatching.mli | 2 +- src/ecProofTerm.ml | 8 ++-- src/ecSearch.ml | 4 +- src/ecTyping.ml | 7 ++- src/phl/ecPhlPrRw.ml | 6 +-- 9 files changed, 91 insertions(+), 55 deletions(-) diff --git a/src/ecEnv.ml b/src/ecEnv.ml index fb11e65a9e..bfd1ad56ea 100644 --- a/src/ecEnv.ml +++ b/src/ecEnv.ml @@ -3446,16 +3446,17 @@ module LDecl = struct with LdeclError _ -> raise NotReducible (* ------------------------------------------------------------------ *) - let check_name_clash id hyps = + let check_name_clash ?(onlyid = false) id hyps = if has_id id hyps then error (NameClash (`Ident id)) - else + else if not onlyid then begin let s = EcIdent.name id in if s <> "_" && has_name ~dep:false s hyps then error (NameClash (`Symbol s)) + end - let add_local id ld hyps = - check_name_clash id hyps; + let add_local ?onlyid id ld hyps = + check_name_clash ?onlyid id hyps; { hyps with h_local = (id, ld) :: hyps.h_local } (* ------------------------------------------------------------------ *) @@ -3497,8 +3498,8 @@ module LDecl = struct | LD_abs_st us -> AbsStmt.bind x us env (* ------------------------------------------------------------------ *) - let add_local x k h = - let le_hyps = add_local x k (tohyps h) in + let add_local ?onlyid x k h = + let le_hyps = add_local ?onlyid x k (tohyps h) in let le_env = add_local_env x k h.le_env in { h with le_hyps; le_env; } diff --git a/src/ecEnv.mli b/src/ecEnv.mli index 5d73b3bd15..4037f86843 100644 --- a/src/ecEnv.mli +++ b/src/ecEnv.mli @@ -459,7 +459,7 @@ module LDecl : sig val baseenv : hyps -> env val ld_subst : f_subst -> local_kind -> local_kind - val add_local : EcIdent.t -> local_kind -> hyps -> hyps + val add_local : ?onlyid:bool -> EcIdent.t -> local_kind -> hyps -> hyps val by_name : symbol -> hyps -> l_local val by_id : EcIdent.t -> hyps -> local_kind diff --git a/src/ecHiGoal.ml b/src/ecHiGoal.ml index 6250d10068..62fbcaf636 100644 --- a/src/ecHiGoal.ml +++ b/src/ecHiGoal.ml @@ -663,7 +663,7 @@ let process_delta ~und_delta ?target (s, o, p) tc = if matches then begin let p = concretize_form ptenv p in let cpos = - let test = fun _ fp -> + let test = fun _ hyps fp -> let fp = match fp.f_node with | Fapp (h, hargs) when List.length hargs > na -> @@ -675,7 +675,7 @@ let process_delta ~und_delta ?target (s, o, p) tc = then `Accept (-1) else `Continue in - try FPosition.select ?o test target + try FPosition.select ?o test hyps target with InvalidOccurence -> tc_error !!tc "invalid occurences selector" in diff --git a/src/ecMatching.ml b/src/ecMatching.ml index a2c2881157..0dc9ca149d 100644 --- a/src/ecMatching.ml +++ b/src/ecMatching.ml @@ -825,50 +825,82 @@ module FPosition = struct (* ------------------------------------------------------------------ *) let select ?o test = - let rec doit1 ctxt pos fp = - match test ctxt fp with + let module Ctxt = struct + type ctxt = Sid.t * LDecl.hyps + + let add_memory (m, mty) ((ctxt, hyps) : ctxt) = + (Sid.add m ctxt, EcEnv.LDecl.add_local ~onlyid:true m (LD_mem mty) hyps) + + let add_module (mx, mty) ((ctxt, hyps) : ctxt) = + (Sid.add mx ctxt, EcEnv.LDecl.add_local ~onlyid:true mx (LD_modty mty) hyps) + + let add_local (x, xty) ((ctxt, hyps) : ctxt) = + (Sid.add x ctxt, EcEnv.LDecl.add_local ~onlyid:true x (LD_var (xty, None)) hyps) + + let add_binding ((x, gty) : binding) (ce : ctxt) = + match gty with + | GTty xty -> add_local (x, xty) ce + | GTmem m -> add_memory (x, m ) ce + | GTmodty mty -> add_module (x, mty) ce + end in + + let rec doit1 ce pos fp = + match let ctxt, env = ce in test ctxt env 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)) + | Fif (c, f1, f2) -> doit pos (`WithCtxt (ce, [c; f1; f2])) + | Fapp (f, fs) -> doit pos (`WithCtxt (ce, f :: fs)) + | Ftuple fs -> doit pos (`WithCtxt (ce, fs)) | Fmatch (b, fs, _) -> - doit pos (`WithCtxt (ctxt, b :: fs)) + doit pos (`WithCtxt (ce, 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])) + | Fquant (_, bs, f) -> + let ce = List.fold_left ((^~) Ctxt.add_binding) ce bs in + doit pos (`WithCtxt (ce, [f])) | Flet (lp, f1, f2) -> - let subctxt = List.fold_left ((^~) Sid.add) ctxt (lp_ids lp) in - doit pos (`WithSubCtxt [(ctxt, f1); (subctxt, f2)]) + let subce = List.fold_left ((^~) Ctxt.add_local) ce (lp_bind lp) in + doit pos (`WithSubCtxt [(ce, f1); (subce, f2)]) | Fproj (f, _) -> - doit pos (`WithCtxt (ctxt, [f])) + doit pos (`WithCtxt (ce, [f])) | Fpr pr -> - let subctxt = Sid.add pr.pr_mem ctxt in - doit pos (`WithSubCtxt [(ctxt, pr.pr_args); (subctxt, pr.pr_event)]) + let subce = + let env = EcEnv.LDecl.toenv (snd ce) in + let m, mty = EcEnv.Fun.prF_memenv pr.pr_mem pr.pr_fun env in + Ctxt.add_memory (m, mty) ce + in doit pos (`WithSubCtxt [(ce, pr.pr_args); (subce, pr.pr_event)]) - | FhoareF hs -> - doit pos (`WithCtxt (Sid.add EcFol.mhr ctxt, [hs.hf_pr; hs.hf_po])) + | FhoareF hf -> + let subce_pr, subce_po = + let env = EcEnv.LDecl.toenv (snd ce) in + let mpr, mpo = EcEnv.Fun.hoareF_memenv hf.hf_f env in + (Ctxt.add_memory mpr ce, Ctxt.add_memory mpo ce) in + doit pos (`WithSubCtxt [(subce_pr, hf.hf_pr); (subce_po, hf.hf_po)]) (* TODO: A: From what I undertand, there is an error there: it should be (subctxt, hs.bhf_bd) *) - | 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)])) + | FbdHoareF hf -> + let subce_pr, subce_po = + let env = EcEnv.LDecl.toenv (snd ce) in + let mpr, mpo = EcEnv.Fun.hoareF_memenv hf.bhf_f env in + (Ctxt.add_memory mpr ce, Ctxt.add_memory mpo ce) in + doit pos (`WithSubCtxt ([(subce_pr, hf.bhf_pr); + (subce_po, hf.bhf_po); + (ce , hf.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])) + | FequivF ef -> + let ce_pr, ce_po = + let env = EcEnv.LDecl.toenv (snd ce) in + let (prl, prr), (pol, por) = + EcEnv.Fun.equivF_memenv ef.ef_fl ef.ef_fr env in + (Ctxt.add_memory prr (Ctxt.add_memory prl ce), + Ctxt.add_memory por (Ctxt.add_memory pol ce)) in + doit pos (`WithSubCtxt [(ce_pr, ef.ef_pr); (ce_po, ef.ef_po)]) | _ -> None in @@ -878,16 +910,16 @@ module FPosition = struct and doit pos fps = let fps = match fps with - | `WithCtxt (ctxt, fps) -> + | `WithCtxt (ce, fps) -> List.mapi (fun i fp -> - doit1 ctxt (i::pos) fp |> omap (fun p -> (i, p))) + doit1 ce (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))) + (fun i (ce, fp) -> + doit1 ce (i::pos) fp |> omap (fun p -> (i, p))) fps in @@ -897,9 +929,9 @@ module FPosition = struct | _ -> Some (Mint.of_list fps) in - fun fp -> + fun hyps fp -> let cpos = - match doit [] (`WithCtxt (Sid.empty, [fp])) with + match doit [] (`WithCtxt ((Sid.empty, hyps), [fp])) with | None -> Mint.empty | Some p -> p in @@ -932,7 +964,7 @@ module FPosition = struct | _ -> `NoKey in - let test xconv _ tp = + let test xconv _ hyps tp = if not (keycheck tp key) then `Continue else begin let (tp, ti) = match tp.f_node with @@ -944,7 +976,7 @@ module FPosition = struct if EcReduction.xconv xconv hyps p tp then `Accept ti else `Continue end - in select ?o (test xconv) target + in select ?o (test xconv) hyps target (* ------------------------------------------------------------------ *) let map (p : ptnpos) (tx : form -> form) (f : form) = diff --git a/src/ecMatching.mli b/src/ecMatching.mli index 40a4213f83..575cf367d5 100644 --- a/src/ecMatching.mli +++ b/src/ecMatching.mli @@ -171,7 +171,7 @@ module FPosition : sig val tostring : ptnpos -> string - val select : ?o:occ -> (Sid.t -> form -> select) -> form -> ptnpos + val select : ?o:occ -> (Sid.t -> LDecl.hyps -> form -> select) -> LDecl.hyps -> form -> ptnpos val select_form : ?xconv:EcReduction.xconv -> ?keyed:bool -> LDecl.hyps -> occ option -> form -> form -> ptnpos diff --git a/src/ecProofTerm.ml b/src/ecProofTerm.ml index b17fe4649b..4b25b2daed 100644 --- a/src/ecProofTerm.ml +++ b/src/ecProofTerm.ml @@ -341,7 +341,7 @@ let pf_find_occurence let mode = { mode with fm_conv = occmode.k_conv } in - let trymatch mode bds tp = + let trymatch mode bds pte_hy tp = if not (keycheck tp key) then `Continue else let tps = @@ -357,7 +357,7 @@ let pf_find_occurence tps |> List.iter (fun tp -> if Mid.set_disjoint bds tp.f_fv then begin try - pf_form_match ~mode pt ~ptn tp; + pf_form_match ~mode { pt with pte_hy } ~ptn tp; raise (E.MatchFound tp) with EcMatching.MatchFailure -> () end); @@ -370,8 +370,8 @@ let pf_find_occurence try let _ = if rooted - then ignore (trymatch mode Mid.empty subject) - else ignore (EcMatching.FPosition.select (trymatch mode) subject) + then ignore (trymatch mode Mid.empty pt.pte_hy subject) + else ignore (EcMatching.FPosition.select (trymatch mode) pt.pte_hy subject) in raise (FindOccFailure `MatchFailure) with E.MatchFound subf -> if full && not (can_concretize pt) then begin diff --git a/src/ecSearch.ml b/src/ecSearch.ml index 8a3621c271..f7163158d5 100644 --- a/src/ecSearch.ml +++ b/src/ecSearch.ml @@ -43,7 +43,7 @@ let match_ (env : EcEnv.env) (search : search list) f = let ev = EcMatching.MEV.of_idents (Mid.keys !v) `Form in let na = List.length (snd (EcFol.destr_app ptn)) in - let trymatch _bds tp = + let trymatch _bds hyps tp = let tp = match tp.f_node with | Fapp (h, hargs) when List.length hargs > na -> @@ -59,7 +59,7 @@ let match_ (env : EcEnv.env) (search : search list) f = `Continue in try - ignore (EcMatching.FPosition.select trymatch f); + ignore (EcMatching.FPosition.select trymatch hyps f); false with E.MatchFound -> true end diff --git a/src/ecTyping.ml b/src/ecTyping.ml index 3c4541537b..c8ed87f50d 100644 --- a/src/ecTyping.ml +++ b/src/ecTyping.ml @@ -2923,7 +2923,9 @@ and trans_form_or_pattern env ?mv ?ps ue pf tt = let module E = struct exception MatchFound end in - let test = + let test hyps = + let env = EcEnv.LDecl.toenv hyps in + match ppt with | `Pattern ppt -> let ue = EcUnify.UniEnv.create None in @@ -2976,7 +2978,8 @@ and trans_form_or_pattern env ?mv ?ps ue pf tt = let test target = try - ignore (EcMatching.FPosition.select (fun _ -> test) target); + let hyps = EcEnv.LDecl.init env [] in + ignore (EcMatching.FPosition.select (fun _ -> test) hyps target); false with E.MatchFound -> true in diff --git a/src/phl/ecPhlPrRw.ml b/src/phl/ecPhlPrRw.ml index f052965148..077c0c772b 100644 --- a/src/phl/ecPhlPrRw.ml +++ b/src/phl/ecPhlPrRw.ml @@ -181,11 +181,11 @@ let t_pr_rewrite_low (s,dof) tc = | `MuSum -> select_pr (fun _ev -> true) in - let select xs fp = if select xs fp then `Accept (-1) else `Continue in - let env, _, concl = FApi.tc1_eflat tc in + let select xs _ fp = if select xs fp then `Accept (-1) else `Continue in + let env, hyps, concl = FApi.tc1_eflat tc in let torw = try - ignore (EcMatching.FPosition.select select concl); + ignore (EcMatching.FPosition.select select hyps concl); tc_error !!tc "cannot find a pattern for %s" s with FoundPr f -> f in