-
Notifications
You must be signed in to change notification settings - Fork 5
Open
Labels
area:semanticsK semantics definitionsK semantics definitionsarea:typesType systemType systempriority:p2Valuable but can waitValuable but can waitstatus:triageNew, not yet organizedNew, not yet organizedtype:featureNew capability or enhancementNew capability or enhancement
Description
Problem
Type information in the K semantics is accessed indirectly through Ty indices (ty(Int)). Every time type data is needed, a lookupTy(TY) call retrieves it from the type table.
This indirection:
- Adds complexity and reduces readability of semantic rules
- Creates extra simplification overhead for the Haskell backend
Proposal
Inline all Ty indices to actual type data, eliminating the lookupTy indirection layer.
The inlining could be done at the Python layer or at the stable-mir-json level. Recursive types (e.g., self-referential structs) are not a blocker — the current system already has mechanisms like typeof to express them.
Scope
TY / lookupTy appears ~81 times across the semantics files, primarily in:
rt/data.md,rt/types.md,rt/value.mdkmir.md,intrinsics.md
Acceptance Criteria
- All
lookupTy(TY)calls eliminated or replaced with direct type data - Existing tests pass
Reactions are currently unavailable
Metadata
Metadata
Assignees
Labels
area:semanticsK semantics definitionsK semantics definitionsarea:typesType systemType systempriority:p2Valuable but can waitValuable but can waitstatus:triageNew, not yet organizedNew, not yet organizedtype:featureNew capability or enhancementNew capability or enhancement