feat: Add statement-level type declarations#507
Open
MikaelMayer wants to merge 17 commits intomainfrom
Open
Conversation
Add comprehensive test suite for statement-level type declarations: - Basic uninterpreted types - Polymorphic types with constructor and accessor functions - Type scoping within procedures - Integration with function declarations - Type mismatch error cases
Add infrastructure for declaring uninterpreted types within procedures: - Grammar support for type declaration statements - AST extension with typeDecl constructor - Translation from DDM to Core - Type checking integration - Evaluation semantics (no runtime effect) - Updates to all statement-handling code Current status: Core infrastructure complete, but DDM translation needs refinement to properly handle type resolution in subsequent statements.
Successfully implemented: - Grammar, AST, translation, type checking, evaluation - Types can be declared with 'type T;' syntax - Type declarations are properly added to freeVars - Single variable declarations work correctly Known limitation: - Multiple variables of the same type cause DDM translation panic - Issue: DDM's declareType treats type names as bound variables - Root cause: Mismatch between DDM scope system and type constructor resolution - Workaround needed: Custom type resolution or DDM parser modification The core infrastructure is complete and working for simple cases.
Implement new DDM annotation that adds types to global context instead of local bindings, enabling statement-level type declarations to work like program-level declarations. Changes: - Add declareGlobalType metadata to StrataDDL - Add globalType variant to BindingSpec - Handle globalType in elaborator by adding to GlobalContext - Update grammar to use declareGlobalType for statement type declarations - Update test expectations for working implementation
Add missing typeDecl cases to: - DetToNondet transformation - StatementWF proof - C_Simp translation - ProcedureInlining - DetToNondetCorrect (partial - WIP) Fixes CI build failures for statement-level type declarations.
The typeDecl case in DetToNondetCorrect needs a proof that evaluating a type declaration in the nondeterministic semantics preserves the store. Using sorry temporarily to unblock CI - proof can be completed later.
Fix lint check failures by removing trailing whitespace from: - Strata/Languages/Core/DDMTransform/Translate.lean - Strata/Languages/Core/StatementType.lean
…ype declarations Move TypeConstructor and Boundedness from Core/TypeDecl.lean to a new shared module DL/TypeConstructor.lean. Update Stmt.typeDecl to use TypeConstructor directly instead of separate name and numargs fields. This ensures consistency when TypeConstructor evolves - changes automatically propagate to both program-level and statement-level type declarations. Changes: - Create Strata/DL/TypeConstructor.lean with shared TypeConstructor - Update Stmt.typeDecl from (name : String) (numargs : Nat) to (tc : TypeConstructor) - Update all pattern matches on typeDecl across the codebase - Re-export TypeConstructor and toType from Core.TypeDecl for compatibility
Rename declareGlobalType annotation and globalType binding to declareScopedType and scopedType throughout DDM infrastructure. The term 'scoped' better reflects that these types are added to the global context for scoping purposes within statement blocks.
Add tests covering: - Basic uninterpreted types - Type scoping across procedures - Multiple distinct types in same procedure - Equality reasoning with uninterpreted types
Merge typeDeclStmt1 and typeDeclStmt4 into a single test that covers both basic type declarations and equality reasoning. This reduces redundancy while maintaining full test coverage.
MikaelMayer
commented
Mar 5, 2026
| ⟨default, none⟩ | ||
| else | ||
| let bindings := List.range tc.numargs |>.map fun i => | ||
| let argName : Ann String M := ⟨default, s!"_ty{i}"⟩ |
Contributor
Author
There was a problem hiding this comment.
could we store the type arguments names as part of this PR? That way we wouldn't need to generate these weird identifiers.
Resolve conflicts from main's removal of typeForward: - Keep scopedType, remove typeForward from BindingSpec - Adapt to new GlobalContext.ensureDefined API - Fix scopedType to properly add types to global context
Replace numargs field with params list to preserve actual parameter names from source code. This improves error messages and enables better round-tripping (type T a b prints as 'type T a b' not 'type T _ty0 _ty1'). Changes: - TypeConstructor.params replaces numargs field - Add numargs helper function for compatibility - Update all construction sites to pass parameter names - Update test expectations to reflect actual parameter names
- Remove unnecessary pattern match in elabOperation (already handled in evalBindingSpec) - Complete DetToNondetCorrect proof for typeDecl case
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
1 participant
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.
Add statement-level type declarations to Strata Core
This PR adds support for declaring uninterpreted types as statements within procedures, similar to how function declarations work at the statement level.
Motivation
To support translation to CoreSMT (a subset of Core that maps 1-1 with SMT), we need the ability to declare uninterpreted types that can be mapped to SMT's
declare-sort. Statement-level type declarations enable this while maintaining proper scoping.Changes
Implementation Plan