Skip to content

add missing Bofbool case in Const_eval#6

Open
redianthus wants to merge 2 commits into
codex-semantics-library:mainfrom
redianthus:bofbool
Open

add missing Bofbool case in Const_eval#6
redianthus wants to merge 2 commits into
codex-semantics-library:mainfrom
redianthus:bofbool

Conversation

@redianthus

@redianthus redianthus commented Jun 15, 2026

Copy link
Copy Markdown

Hi @mlemerre !

We used this operation in Owi with @S41d and noticed it was missing when we started getting runtime assertion failures.

The only difference at runtime is:

| TC.Bofbool _size -> if boolean a then Z.one else Z.zero

I also had to add type annotations because of the polymorphic recursion, otherwise it would complain with:

$ dune build @install -p codex
File "terms/const_eval.ml", line 37, characters 19-20:
37 | if boolean a then Z.one else Z.zero
                ^
Error: The value a has type Operator.Function_symbol.boolean Terms.t
but an expression was expected of type 'a
This instance of Operator.Function_symbol.boolean is ambiguous:
it would escape the scope of its equation

While adding the type annotations, I realized the big mutual-recursion group was not needed and most functions could be moved out of it. Only the boolean and binary cases are mutually recursive. So I went ahead and decided to split the group in small functions, I think this is easier to read like this.

Best,

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.

1 participant