[acl2/acl2] eb6428: [Remora] Move some code.

[Alessandro Coglio]

Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: eb6428e7749047fb2587ee2e07a32c4cd842a805
https://github.com/acl2/acl2/commit/eb6428e7749047fb2587ee2e07a32c4cd842a805
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-02 (Thu, 02 Jul 2026)

Changed paths:
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/values.lisp

Log Message:
-----------
[Remora] Move some code.


Commit: 1c7932cc233c689e0c94f9470f328e513ebbea31
https://github.com/acl2/acl2/commit/1c7932cc233c689e0c94f9470f328e513ebbea31
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-02 (Thu, 02 Jul 2026)

Changed paths:
M books/kestrel/remora/values.lisp

Log Message:
-----------
[Remora] Expand/generalize some doc.


Commit: efc5287be4dd068e596f49201ebc8d0f8a594361
https://github.com/acl2/acl2/commit/efc5287be4dd068e596f49201ebc8d0f8a594361
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-02 (Thu, 02 Jul 2026)

Changed paths:
M books/kestrel/remora/values.lisp

Log Message:
-----------
[Remora] Add characterization of primop values.


Commit: 8d57308d9742206dd6d7f2af322bf41c1ceb93d7
https://github.com/acl2/acl2/commit/8d57308d9742206dd6d7f2af322bf41c1ceb93d7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-02 (Thu, 02 Jul 2026)

Changed paths:
M books/kestrel/remora/primitives-evaluation.lisp
M books/kestrel/remora/values.lisp

Log Message:
-----------
[Remora] Add guards and checks on primop values.

This is for the ones applicable to expression values.


Commit: fe78eb8d3e79018128d599ac90e999c7e2245e00
https://github.com/acl2/acl2/commit/fe78eb8d3e79018128d599ac90e999c7e2245e00
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-02 (Thu, 02 Jul 2026)

Changed paths:
M books/kestrel/remora/values.lisp

Log Message:
-----------
[Remora] Tighten some terminology.


Commit: 31e6f9197e2370fa0918fe26bddd8fe5d194e563
https://github.com/acl2/acl2/commit/31e6f9197e2370fa0918fe26bddd8fe5d194e563
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-02 (Thu, 02 Jul 2026)

Changed paths:
M books/kestrel/remora/primitives-evaluation.lisp
M books/kestrel/remora/values.lisp

Log Message:
-----------
[Remora] Improve a function name.


Commit: 47276108c9e5209f286d4203cf127419bcc8cf14
https://github.com/acl2/acl2/commit/47276108c9e5209f286d4203cf127419bcc8cf14
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-02 (Thu, 02 Jul 2026)

Changed paths:
M books/kestrel/c/language/implementation-environments/execution-character-sets.lisp
M books/kestrel/remora/abstract-syntax-matching-operations.lisp
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/ispace-equivalence.lisp
M books/kestrel/remora/static-environments.lisp
M books/kestrel/remora/type-checking.lisp

Log Message:
-----------
Merge.


Commit: 6d22f0d5e83ae93193109a3a3594ec6f882e3840
https://github.com/acl2/acl2/commit/6d22f0d5e83ae93193109a3a3594ec6f882e3840
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-02 (Thu, 02 Jul 2026)

Changed paths:
M books/kestrel/remora/type-checking.lisp

Log Message:
-----------
Merge.


Commit: 501819bef2168a4b2fcb9f4e9f66047ae36e69a5
https://github.com/acl2/acl2/commit/501819bef2168a4b2fcb9f4e9f66047ae36e69a5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-02 (Thu, 02 Jul 2026)

Changed paths:
M books/kestrel/remora/primitives-evaluation.lisp
M books/kestrel/remora/values.lisp

Log Message:
-----------
[Remora] Improve a function name.


Commit: e375097975b59cfca8a65ec8450f6ccb61d1bd48
https://github.com/acl2/acl2/commit/e375097975b59cfca8a65ec8450f6ccb61d1bd48
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-02 (Thu, 02 Jul 2026)

Changed paths:
M books/kestrel/remora/static-environments.lisp

Log Message:
-----------
[Remora] Add `length` to static semantics.


Commit: 1d36efdea1276bee9e4a0e921bf29dc338854bf7
https://github.com/acl2/acl2/commit/1d36efdea1276bee9e4a0e921bf29dc338854bf7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-02 (Thu, 02 Jul 2026)

Changed paths:
A books/kestrel/remora/dimension-equivalence-rules.lisp
M books/kestrel/remora/package.lsp
M books/kestrel/remora/static-semantics.lisp

Log Message:
-----------
Merge.


Commit: c5e6db7d57193fe30526b48d366ad5b8fc41b662
https://github.com/acl2/acl2/commit/c5e6db7d57193fe30526b48d366ad5b8fc41b662
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-02 (Thu, 02 Jul 2026)

Changed paths:
M books/kestrel/axe/hit-counts.lisp
M books/kestrel/axe/jvm/lifter.lisp
M books/kestrel/axe/jvm/rule-lists-jvm.lisp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/utilities/if.lisp

Log Message:
-----------
Merge.


Commit: c5dcce7248047229b2aa5665e618605b5481f410
https://github.com/acl2/acl2/commit/c5dcce7248047229b2aa5665e618605b5481f410
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-03 (Fri, 03 Jul 2026)

Changed paths:
M books/kestrel/remora/primitives-evaluation.lisp
M books/kestrel/remora/values.lisp

Log Message:
-----------
[Remora] Start adding support for `length`.

Extend primitive operation values with the various stages of `length`.


Commit: 65dd35b41c601c69a2f042451871ae61bad87870
https://github.com/acl2/acl2/commit/65dd35b41c601c69a2f042451871ae61bad87870
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-03 (Fri, 03 Jul 2026)

Changed paths:
M books/kestrel/axe/node-replacement-alist-for-context.lisp
M books/kestrel/axe/node-replacement-array.lisp
M books/kestrel/axe/refined-assumption-alists3.lisp
M books/kestrel/axe/rewriter.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/acl2-customization.lsp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/cert.acl2
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_al_8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_al_8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_al_8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_ax_16.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_ax_16.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_ax_16.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_bl_8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_bl_8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_bl_8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_bx_16.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_bx_16.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_bx_16.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_eax_32.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_eax_32.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_eax_32.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_ebx_32.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_ebx_32.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_ebx_32.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_mem16.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_mem16.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_mem16.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_mem32.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_mem32.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_mem32.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_mem64.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_mem64.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_mem64.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_mem8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_mem8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_mem8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_rax_64.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_rax_64.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_rax_64.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_rbx_64.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_rbx_64.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_rbx_64.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/acl2-customization.lsp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/cert.acl2
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_al_bl_8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_al_bl_8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_al_bl_8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_al_imm8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_al_imm8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_al_imm8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_al_mem8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_al_mem8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_al_mem8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_ax_bx_16.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_ax_bx_16.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_ax_bx_16.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_ax_imm16.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_ax_imm16.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_ax_imm16.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_ax_mem16.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_ax_mem16.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_ax_mem16.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_bl_imm8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_bl_imm8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_bl_imm8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_bx_imm16.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_bx_imm16.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_bx_imm16.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_bx_imm8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_bx_imm8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_bx_imm8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_eax_ebx_32.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_eax_ebx_32.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_eax_ebx_32.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_eax_imm32.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_eax_imm32.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_eax_imm32.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_eax_mem32.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_eax_mem32.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_eax_mem32.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_ebx_imm32.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_ebx_imm32.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_ebx_imm32.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_ebx_imm8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_ebx_imm8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_ebx_imm8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem16_ax.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem16_ax.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem16_ax.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem16_imm16.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem16_imm16.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem16_imm16.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem16_imm8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem16_imm8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem16_imm8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem32_eax.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem32_eax.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem32_eax.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem32_imm32.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem32_imm32.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem32_imm32.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem32_imm8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem32_imm8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem32_imm8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem64_imm32.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem64_imm32.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem64_imm32.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem64_imm8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem64_imm8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem64_imm8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem64_rax.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem64_rax.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem64_rax.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem8_al.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem8_al.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem8_al.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem8_imm8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem8_imm8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem8_imm8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_rax_imm32.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_rax_imm32.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_rax_imm32.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_rax_mem64.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_rax_mem64.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_rax_mem64.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_rax_rbx_64.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_rax_rbx_64.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_rax_rbx_64.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_rbx_imm32.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_rbx_imm32.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_rbx_imm32.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_rbx_imm8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_rbx_imm8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_rbx_imm8.lisp
M books/kestrel/remora/type-equivalence.lisp
M books/kestrel/remora/values.lisp
R books/misc/records-bsd.lisp

Log Message:
-----------
Merge and resolve conflicts.


Commit: 2413ba7f2a9a6dda3a823765eb77cf50974c18b8
https://github.com/acl2/acl2/commit/2413ba7f2a9a6dda3a823765eb77cf50974c18b8
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-03 (Fri, 03 Jul 2026)

Changed paths:
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/primitives-evaluation.lisp

Log Message:
-----------
[Remora] Add (and handle) a guard.

Also auto-eliminate some trailing whitespace.


Commit: 9db446aae8ccadeb65d025b9e407043e2e90015a
https://github.com/acl2/acl2/commit/9db446aae8ccadeb65d025b9e407043e2e90015a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-03 (Fri, 03 Jul 2026)

Changed paths:
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/primitives-evaluation.lisp

Log Message:
-----------
[Remora] Improve a function name.


Commit: af2c4483fbee8330fb2387ab50d4e89d28ea13b2
https://github.com/acl2/acl2/commit/af2c4483fbee8330fb2387ab50d4e89d28ea13b2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-03 (Fri, 03 Jul 2026)

Changed paths:
M books/kestrel/remora/primitives-evaluation.lisp

Log Message:
-----------
[Remora] Minor doc fixes, and style consistency.

This does not really change the content, except for fixing a few typos and also
making the documentation form more consistent with the rest of the library.


Commit: 266d5e8c6418e629e3ae9f7b0120966c936c7dde
https://github.com/acl2/acl2/commit/266d5e8c6418e629e3ae9f7b0120966c936c7dde
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-03 (Fri, 03 Jul 2026)

Changed paths:
M books/kestrel/remora/primitives-evaluation.lisp

Log Message:
-----------
[Remora] Add more suppor for `length`.

Specifically, add the evaluation of that primitive on expression values, once it
has been instantiated with the type and ispace values.


Commit: da0412081364092c868cb477bd6151e5a5b6f3bb
https://github.com/acl2/acl2/commit/da0412081364092c868cb477bd6151e5a5b6f3bb
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-03 (Fri, 03 Jul 2026)

Changed paths:
M books/kestrel/remora/primitives-evaluation.lisp

Log Message:
-----------
[Remora] Add a guard.


Commit: 1b588826ab6d73c0baef2d093c90a81c4bbc05a9
https://github.com/acl2/acl2/commit/1b588826ab6d73c0baef2d093c90a81c4bbc05a9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-03 (Fri, 03 Jul 2026)

Changed paths:
M books/kestrel/remora/primitives-evaluation.lisp

Log Message:
-----------
[Remora] Add guard and simplify some code.


Commit: 99955e22da3a8fe8b464bb58a6a9197530ea1d50
https://github.com/acl2/acl2/commit/99955e22da3a8fe8b464bb58a6a9197530ea1d50
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-03 (Fri, 03 Jul 2026)

Changed paths:
M books/kestrel/remora/primitives-evaluation.lisp

Log Message:
-----------
[Remora] Extend evaluation.

Add functions to apply primitive operation values that are applicable to type
and ispace values. For now only `length` is supported.


Commit: cdadea4a360aec7142ce961d3bf33d0b33ea7608
https://github.com/acl2/acl2/commit/cdadea4a360aec7142ce961d3bf33d0b33ea7608
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-03 (Fri, 03 Jul 2026)

Changed paths:
M books/kestrel/remora/evaluation.lisp

Log Message:
-----------
[Remora] Extend evaluation.

Link the evaluation of primitive operation values applicable to type and ispace
values into the main evaluation function cliques.


Commit: b034b8d6c756c5c712d913da37e5fcf55c85247c
https://github.com/acl2/acl2/commit/b034b8d6c756c5c712d913da37e5fcf55c85247c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-03 (Fri, 03 Jul 2026)

Changed paths:
M books/kestrel/remora/dynamic-environments.lisp

Log Message:
-----------
[Remora] Add `length` to dynamic environments.


Commit: 4c28b5639e4842cd1535d2154e9fec289b9981eb
https://github.com/acl2/acl2/commit/4c28b5639e4842cd1535d2154e9fec289b9981eb
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-03 (Fri, 03 Jul 2026)

Changed paths:
A books/kestrel/remora/primitives-evaluation-length-tests.lisp

Log Message:
-----------
[Remora] Add a test file for `length`.


Commit: 737e0f7a900850dfa588d6c7b0ef11a6e3870014
https://github.com/acl2/acl2/commit/737e0f7a900850dfa588d6c7b0ef11a6e3870014
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-03 (Fri, 03 Jul 2026)

Changed paths:
M books/kestrel/remora/primitives-evaluation.lisp

Log Message:
-----------
[Remora] Improve layout.


Compare: https://github.com/acl2/acl2/compare/0b7087163b15...737e0f7a9008

To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications

[Alessandro Coglio]

Branch: refs/heads/master

[Alessandro Coglio]

Branch: refs/heads/testing