Skip to content

Construct bound relation proofs before reification - #387

Open
yoohaemin wants to merge 3 commits into
masterfrom
proof-construction
Open

yoohaemin wants to merge 3 commits into
masterfrom
proof-construction

Conversation

@yoohaemin

@yoohaemin yoohaemin commented Oct 9, 2026 •

Copy link
Copy Markdown
Owner

Bind actual relation values during implicit syntax conversion, then expose the completed interpreter through a cached, parameterless Proof.reify. Composition constructs proofs from the actual child nodes. ZQuery and Fetch syntax retain the bound proof before their methods run, and existing fixed declaration proofs remain usable through a low-priority adapter.

@yoohaemin
yoohaemin changed the base branch from master to common-error October 10, 2026 02:15
Base automatically changed from common-error to master October 10, 2026 08:02
@yoohaemin
yoohaemin marked this pull request as ready for review October 10, 2026 08:04
Copilot AI balanced review requested due to automatic review settings October 10, 2026 08:04

Copilot AI left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

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

🟡 Changes recommended

The unchanged Kyo syntax can no longer resolve proofs for composed relations.

1 open finding
What changed in this PR

Binds relation values during proof construction and caches completed interpreters for reification.

Changes:

  • Converts proof derivation to relation-bound conversions.
  • Updates Fetch, ZQuery, and generator syntax.
  • Adds construction/caching regression coverage and documentation.
File Description
zquery/​src/​test/​scala/​decrel/​reify/​ZQueryProofConstructionSpec.scala Tests eager proof binding and reuse.
zquery/​src/​main/​scala-3/​decrel/​reify/​zquerySyntax.scala Caches bound proofs in Scala 3 syntax.
zquery/​src/​main/​scala-2.13/​decrel/​reify/​zquerySyntax.scala Caches bound proofs in Scala 2 syntax.
zquery-next/​src/​main/​scala/​decrel/​reify/​zqueryNextSyntax.scala Applies proof conversions to relations.
ziotest/​src/​main/​scala/​decrel/​ziotest/​gen.scala Updates generator expansion.
scalacheck/​src/​main/​scala/​decrel/​scalacheck/​gen.scala Updates generator expansion.
mdoc/​docs/​guide/​defining-relations.md Documents proof construction.
fetch/​src/​main/​scala/​decrel/​reify/​fetch.scala Binds and caches Fetch proofs.
core/​src/​test/​scala/​decrel/​reify/​ProofConstructionSpec.scala Covers binding, composition, and caching.
core/​src/​main/​scala/​decrel/​reify/​monofunctor/​proof.scala Refactors monofunctor proof derivation.
core/​src/​main/​scala/​decrel/​reify/​bifunctor/​proof.scala Refactors error-aware proof derivation.

🧠 Review effort: Balanced


💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

Comment thread core/src/main/scala/decrel/reify/monofunctor/proof.scala

Copilot AI left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

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

🔵 Needs a closer look

The cross-version implicit-derivation redesign affects several public integrations and warrants final human validation.

0 open findings

1 resolved since last review

🧠 Review effort: Balanced

This branch has not been deployed

No deployments
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.

2 participants