From 1d6d16585e5a0ae53ec0fbb98f8e98ad213e7d57 Mon Sep 17 00:00:00 2001
From: Jonathan Protzenko <protz@microsoft.com>
Date: Tue, 24 Oct 2023 12:43:55 -0700
Subject: [PATCH] Make lid detection more generic

---
 lib/Helpers.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/lib/Helpers.ml b/lib/Helpers.ml
index ab92adf6..6c532a62 100644
--- a/lib/Helpers.ml
+++ b/lib/Helpers.ml
@@ -267,7 +267,7 @@ let strengthen_array t e2 =
         size is non-constant, so I don't know what declaration to write"
         pexpr e2
 
-let pure_builtin_lids = ref [
+let pure_builtin_lids = [
   [ "C"; "String" ], "get";
   [ "C"; "Nullity" ], "op_Bang_Star";
   [ "LowStar"; "BufferOps" ], "op_Bang_Star";
@@ -278,12 +278,14 @@ let pure_builtin_lids = ref [
   [ "FStar"; "UInt128" ], "";
 ]
 
-let is_readonly_builtin_lid lid =
+let is_readonly_builtin_lid_ = ref (fun lid ->
   List.exists (fun lid' ->
     let lid = Idents.string_of_lident lid in
     let lid' = Idents.string_of_lident lid' in
     KString.starts_with lid lid'
-  ) !pure_builtin_lids
+  ) pure_builtin_lids)
+
+let is_readonly_builtin_lid lid = !is_readonly_builtin_lid_ lid
 
 class ['self] closed_term_visitor = object (_: 'self)
   inherit [_] reduce