Skip to content

Rename "assumed" to "builtin" #338

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 3 commits into from
Aug 28, 2024

Conversation

Nadrieril
Copy link
Member

@Nadrieril Nadrieril commented Aug 28, 2024

Fixes #231. This also removes the BoxFree builtin that no longer exists in rustc, which fixes #230.

@Nadrieril Nadrieril merged commit 6b5e110 into AeneasVerif:main Aug 28, 2024
5 of 6 checks passed
@Nadrieril Nadrieril deleted the rename-assumed-to-builtin branch August 28, 2024 13:01
@@ -20,30 +20,11 @@ module FunDeclId = Types.FunDeclId
*)
type var_id = VarId.id [@@deriving show, ord]

(** An assumed function identifier, identifying a function coming from a
(** An built-in function identifier, identifying a function coming from a
standard library.
*)
type assumed_fun_id =
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Shouldn't this also be renamed to builtin_fun_id? :)

@@ -100,7 +100,6 @@ let binop_to_string (binop : binop) : string =
let assumed_fun_id_to_string (aid : assumed_fun_id) : string =
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Same comment

parameters (if there are). Adding types which don't satisfy this
will require to update the code abstracting the signatures (to properly
take into account the lifetime constraints).

TODO: update to not hardcode the types (except `Box` maybe) and be more
modular.
TODO: move to assumed.rs?
TODO: move to builtins.rs?
*)
type assumed_ty =
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Same comment

@@ -313,12 +313,12 @@ and type_id =
*)
| TTuple
| TAssumed of assumed_ty
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Same

@Nadrieril
Copy link
Member Author

Nadrieril commented Aug 29, 2024

@sonmarcho That was intentional, this PR is only for the rust side. I'll propagate to the OCaml side separately.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Rename assumed to builtin Check that box_free is still used
2 participants