feat(types): native type-system decoration layer#26
Merged
hyperpolymath merged 2 commits intomainfrom Apr 20, 2026
Merged
Conversation
|
Codex usage limits have been reached for code reviews. Please check with the admins of this repo to increase the limits by adding credits. |
Step 3 of the native type-system plan: wire backends to consume TypeInfo
decorations, extend GNN graph awareness, and fix a pre-existing build
break.
Changes:
1. Fix pre-existing z3 build break:
- Create `src/rust/provers/outcome.rs` with `ProverOutcome` enum
(8 variants: Proved, InconsistentPremises, NoProofFound,
UnsupportedFeature, InvalidInput, Timeout, ProverError, SystemError)
- Move orphan `check` method from `impl ProverBackend for Z3Backend`
to its own `impl Z3Backend` block — it was not a trait member
- Result: `cargo check --lib` now passes cleanly (0 errors, 0 warnings)
2. Idris2 QTT multiplicity wiring:
- `export()` now reads `Definition.type_info.multiplicity` and emits
QTT annotations (`0 `, `1 `, or unrestricted) on type signatures
- Added `multiplicity_to_idris2()` helper mapping all Multiplicity
variants to Idris2 QTT syntax
- Removed duplicate local Multiplicity enum (now uses crate::types)
3. F* effect + refinement wiring:
- `to_input_format()` now reads `Definition.type_info.effects` and
emits F* effect prefixes (Tot, IO, ST, Exn, Div, GTot, ALL, Custom)
- Reads `type_info.refinement` and emits `{v:T | P}` syntax
- Added `effect_to_fstar()` helper
4. Dedukti exchange layer Sigma support:
- `term_to_dedukti()` renders `Term::Sigma` as `dk_sigma A (x => B)`
- `parse_dedukti_term()` parses `dk_sigma` back to `Term::Sigma`
5. GNN graph type-info awareness:
- Added `EdgeKind::HasMultiplicity`, `HasEffect`, `HasModality`
- `add_type_info_edges()` creates annotation nodes and edges from
hypothesis/definition type_info decorations
- Embeddings: added "sigma" label detection in feature extraction,
updated quantifier feature to include sigma binders
Test results: 587 passed, 0 failed, 0 clippy warnings.
https://claude.ai/code/session_01FYkVX52Tdn6Arp9dWfPLxq
Adds Term::Sigma (dependent pairs) to core IR and introduces a unified TypeInfo sidecar decoration spanning 8 dimensions: Universe, Multiplicity, EffectRow, refinement predicates, Modality, TemporalOp, Semiring, and relational arity. Wires backend consumers (Idris2 QTT, F* effects/refinement, Dedukti Sigma) and extends GNN with type-info-aware edge kinds. Rebased onto latest main; all new type_info fields and Sigma arms re-applied on top of upstream changes. https://claude.ai/code/session_01FYkVX52Tdn6Arp9dWfPLxq
hyperpolymath
force-pushed
the
claude/echidna-type-system-Zan8V
branch
from
a3b6813 to
f68110f
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Term::Sigma(dependent pairs) to core IR, closing a genuine gap — Pi was representable but Sigma was notsrc/rust/types/mod.rswithTypeInfosidecar decoration spanning 8 dimensions: Universe (level/cumulativity/impredicativity/HoTT), Multiplicity (QTT 0/1/ω/linear/affine/graded), EffectRow (row-polymorphic algebraic effects), refinement predicates, Modality (alethic/epistemic/doxastic/deontic/provability), TemporalOp (LTL/CTL/μ-calculus), Semiring (Boolean/tropical/Viterbi/Łukasiewicz), and relational arity (dyadic/n-ary)multiplicity, F* emits effect prefixes + refinement syntax, Dedukti renders/parses Sigma asdk_sigmaHasMultiplicity/HasEffect/HasModalityedge kinds and type-info-aware graph constructionoutcome.rsmodule, extract orphancheckmethod)Test plan
cargo check --libpasses cleanly (also fixes pre-existing z3 build break)https://claude.ai/code/session_01FYkVX52Tdn6Arp9dWfPLxq