Skip to content

Commit

Permalink
Merge pull request #393 from FStarLang/protz_builtin_lids
Browse files Browse the repository at this point in the history
Make lid detection more generic
  • Loading branch information
msprotz authored Oct 24, 2023
2 parents dd8f594 + 1d6d165 commit 7460546
Showing 1 changed file with 5 additions and 3 deletions.
8 changes: 5 additions & 3 deletions lib/Helpers.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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";
Expand All @@ -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
Expand Down

0 comments on commit 7460546

Please sign in to comment.