feat: Add statement-level type declarations#507
Draft
MikaelMayer wants to merge 8 commits intomainfrom
Draft
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
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