[matching]: when crossing a binder, update the env. accordingly

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; }
 

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

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

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) =

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

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

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

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
 

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