From 45063419171a5352a0ce21507e4694946d71e564 Mon Sep 17 00:00:00 2001
From: Christopher Pulte <cp526@cam.ac.uk>
Date: Fri, 9 Aug 2024 09:36:44 +0100
Subject: [PATCH] adhoc performance improvement for resource-derived
 constraints

---
 backend/cn/lib/typing.ml | 19 ++++++++++++-------
 1 file changed, 12 insertions(+), 7 deletions(-)

diff --git a/backend/cn/lib/typing.ml b/backend/cn/lib/typing.ml
index 63f58e152..1ccd4cd81 100644
--- a/backend/cn/lib/typing.ml
+++ b/backend/cn/lib/typing.ml
@@ -440,15 +440,18 @@ let add_c_internal lc =
   return ()
 
 
-let add_r_internal loc (r, RE.O oargs) =
+let add_r_internal ?(derive_constraints = true) loc (r, RE.O oargs) =
   let@ s = get_typing_context () in
   let@ simp_ctxt = simp_ctxt () in
   let r = Simplify.ResourceTypes.simp simp_ctxt r in
   let oargs = Simplify.IndexTerms.simp simp_ctxt oargs in
   let pointer_facts =
-    Resources.pointer_facts
-      ~new_resource:(r, RE.O oargs)
-      ~old_resources:(Context.get_rs s)
+    if derive_constraints then
+      Resources.pointer_facts
+        ~new_resource:(r, RE.O oargs)
+        ~old_resources:(Context.get_rs s)
+    else
+      []
   in
   let@ () = set_typing_context (Context.add_r loc (r, O oargs) s) in
   iterM (fun x -> add_c_internal (LC.T x)) pointer_facts
@@ -701,7 +704,7 @@ let do_unfold_resources loc =
           (fun (re, i) (keep, unpack, extract) ->
             match Pack.unpack loc s.global provable_f2 re with
             | Some unpackable ->
-              let pname = RET.pp_predicate_name (RET.predicate_name (fst re)) in
+              let pname = RET.predicate_name (fst re) in
               (keep, (i, pname, unpackable) :: unpack, extract)
             | None ->
               let re_reduced, extracted =
@@ -725,11 +728,13 @@ let do_unfold_resources loc =
           let@ _, members =
             make_return_record
               loc
-              ("unpack_" ^ Pp.plain pname)
+              ("unpack_" ^ Pp.plain (RET.pp_predicate_name pname))
               (LogicalReturnTypes.binders lrt)
           in
           bind_logical_return_internal loc members lrt
-        | _i, _pname, `RES res -> iterM (add_r_internal loc) res
+        | _i, pname, `RES res ->
+          let is_owned = match pname with Owned _ -> true | _ -> false in
+          iterM (add_r_internal ~derive_constraints:(not is_owned) loc) res
       in
       let@ () = iterM do_unpack unpack in
       let@ () = iterM (add_r_internal loc) extract in