From 41af6d4f2e8195621a76780f3454782adef6efb0 Mon Sep 17 00:00:00 2001
From: Pierre-Yves Strub <pierre-yves@strub.nu>
Date: Thu, 26 Sep 2024 09:12:32 +0200
Subject: [PATCH] Allow generalizing memories

---
 src/ecHiGoal.ml | 51 +++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 51 insertions(+)

diff --git a/src/ecHiGoal.ml b/src/ecHiGoal.ml
index 6250d1006..d17728f74 100644
--- a/src/ecHiGoal.ml
+++ b/src/ecHiGoal.ml
@@ -1675,6 +1675,57 @@ let process_generalize1 ?(doeq = false) pattern (tc : tcenv1) =
             let id = fst (LDecl.by_name s hyps) in
             t_generalize_hyp ~clear id tc
 
+        | PFmem { pl_loc = loc; pl_desc = m; } -> begin
+            if doeq then
+              tacuerror "cannot generate an equation when generalizing a memory";
+
+            let m, lc =
+              try
+                LDecl.by_name m hyps
+              with LDecl.LdeclError (LookupError _) ->
+                tc_error !!tc ~loc "cannot find memory `%s'" m
+            in
+
+            let lc = match lc with LD_mem mt -> mt | _ -> assert false in
+
+            if is_none occ then
+              t_generalize_hyp ~clear m tc
+            else begin
+              let occ = norm_rwocc occ in
+
+              let ptnpos =
+                try
+                  FPosition.select ?o:occ (fun ctxt f ->
+                    if Sid.mem m ctxt then
+                      `Continue
+                    else
+                      match f.f_node with
+                      | Fglob (_, m')
+                      | Fpvar (_, m')
+                      | Fpr   { pr_mem = m' }  when EcIdent.id_equal m m' -> `Accept 0
+                      | _ -> `Continue
+                  ) concl
+                with InvalidOccurence -> tacuerror "invalid occurence selector"
+              in
+
+              let m' = EcIdent.fresh m in
+
+              let newconcl =
+                concl |> FPosition.map ptnpos (fun f ->
+                  match f.f_node with
+                  | Fglob (a, _) -> f_glob a m'
+                  | Fpvar (p, _) -> f_pvar p f.f_ty m'
+                  | Fpr   pr     -> f_pr_r { pr with pr_mem = m' }
+                  | _            -> assert false
+                ) in
+
+              let newconcl = f_forall [(m', GTmem lc)] newconcl in
+              let pt = ptcut ~args:[PAMemory m] newconcl in
+      
+              EcLowGoal.t_apply pt tc
+            end
+          end
+ 
         | _ ->
           let (ptenv, p) =
             let (ps, ue), p = TTC.tc1_process_pattern tc pf in