[codex] Implement PR11.11c user-defined generics#201
[codex] Implement PR11.11c user-defined generics#201berkeleynerd merged 5 commits intoberkeleynerd:mainfrom
Conversation
There was a problem hiding this comment.
Pull request overview
Implements PR11.11c Safe-native user-defined generics across the Safe frontend, including parsing, semantic resolution/monomorphization, cross-package import/export via interface artifacts, and output contract bumps to typed-v6 / safei-v5.
Changes:
- Added Safe-native generic type/function declarations (
of ...+ optionalwith T: interface) and explicit generic actuals at use sites. - Implemented frontend monomorphization for generic calls/types prior to MIR, including cross-package imported generic templates.
- Updated artifact contracts/docs and test/proof harnesses + added PR11.11c fixtures (positive/negative/interface/build).
Reviewed changes
Copilot reviewed 32 out of 32 changed files in this pull request and generated 3 comments.
Show a summary per file
| File | Description |
|---|---|
| tests/positive/pr1111c_generic_constraint.safe | Positive fixture for constrained generic function template + instantiation. |
| tests/positive/pr1111c_generic_basics.safe | Positive fixture for generic type + generic identity function + explicit actuals. |
| tests/negative/neg_pr1111c_unsupported_generic_type.safe | Negative fixture: rejects unsupported generic type forms in this milestone. |
| tests/negative/neg_pr1111c_missing_type_args.safe | Negative fixture: rejects generic call sites without explicit type args. |
| tests/negative/neg_pr1111c_missing_member.safe | Negative fixture: rejects instantiation when constraint interface member is missing. |
| tests/negative/neg_pr1111c_interface_actual.safe | Negative fixture: rejects interface types used as generic actuals. |
| tests/negative/neg_pr1111c_free_call_constraint.safe | Negative fixture for constrained generic template calling convention restrictions. |
| tests/negative/neg_pr1111c_ada_generic_keyword.safe | Negative fixture: rejects Ada generic keyword units in Safe source. |
| tests/interfaces/provider_generic.safe | Interface provider exporting public generic type/function. |
| tests/interfaces/client_generic.safe | Interface client importing and instantiating provider generics. |
| tests/build/pr1111c_provider_build.safe | Build fixture for public generic exports. |
| tests/build/pr1111c_imported_build.safe | Build fixture for importing and instantiating generics across packages. |
| tests/build/pr1111c_generic_build.safe | Build fixture for local generics + printing results. |
| spec/08-syntax-summary.md | Grammar updates for generic formal parts and generic actual parts. |
| spec/02-restrictions.md | Clarifies Ada generics remain excluded while Safe-native generics are admitted. |
| scripts/validate_output_contracts.py | Adds typed-v6/safei-v5 validation + generic metadata validation. |
| scripts/run_tests.py | Adds PR11.11c cases and emits dependency interfaces for local with-based builds. |
| scripts/run_proofs.py | Adds PR11.11c checkpoint fixture group and summary reporting. |
| scripts/_lib/proof_inventory.py | Registers PR11.11c proof checkpoint fixtures. |
| docs/tutorial.md | Documents Safe-native generics in the tutorial narrative. |
| docs/PR11.x-series-proposed.md | Updates PR11 generics proposal section and contract bump notes. |
| docs/artifact_contract.md | Updates frozen artifact formats and documents generic metadata fields. |
| compiler/ast_schema.json | Extends AST schema with generic formals + generic arguments and GenericFormal node. |
| compiler_impl/src/safe_frontend-mir_model.ads | Adds generic metadata fields to type/subprogram descriptors. |
| compiler_impl/src/safe_frontend-interfaces.ads | Extends interface model to carry generic subprogram metadata. |
| compiler_impl/src/safe_frontend-interfaces.adb | Parses/accepts safei-v5 and loads generic metadata from JSON. |
| compiler_impl/src/safe_frontend-check_resolve.adb | Implements generic template tracking, instantiation, specialization, and import handling. |
| compiler_impl/src/safe_frontend-check_parse.adb | Parses generic formals (of ... with ...) and name-site generic actuals (of ...). |
| compiler_impl/src/safe_frontend-check_model.ads | Extends frontend model with generic formals + generic args on names/type specs. |
| compiler_impl/src/safe_frontend-check_lower.adb | Skips lowering generic templates (monomorphized away pre-MIR). |
| compiler_impl/src/safe_frontend-check_emit.adb | Emits AST/typed/safei updates, including template source for imported generics. |
| compiler_impl/src/safe_frontend-ada_emit.adb | Avoids emitting generic templates; ensures specialized bodies are emitted. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
There was a problem hiding this comment.
Pull request overview
Copilot reviewed 34 out of 34 changed files in this pull request and generated 3 comments.
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
There was a problem hiding this comment.
Pull request overview
Copilot reviewed 35 out of 35 changed files in this pull request and generated 2 comments.
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| is | ||
| Result : FT.UString := | ||
| FT.To_UString | ||
| (Prefix & Sanitize_Type_Name_Component (Method_Target_Tail_Name (Name))); |
There was a problem hiding this comment.
Generic_Specialization_Name uses Method_Target_Tail_Name (Name) (dropping the package qualifier) when forming the synthetic specialization identifier. This can cause name collisions when two different packages export generics with the same base name (e.g., pkg1.identity and pkg2.identity), leading to overwriting entries in Current_Synthetic_Functions / Current_Generic_Type_Instantiations and mis-resolving calls/types. Consider incorporating a sanitized form of the full qualified name (or origin package) into the specialization name so it is unique per generic template across imports.
| (Prefix & Sanitize_Type_Name_Component (Method_Target_Tail_Name (Name))); | |
| (Prefix & Sanitize_Type_Name_Component (Canonical_Name (Name))); |
| if not Imported_Subprograms.Is_Empty then | ||
| for Item of Imported_Subprograms loop | ||
| declare | ||
| Qualified_Name : constant String := UString_Value (Item.Name); | ||
| Short_Name : constant String := Method_Target_Tail_Name (Qualified_Name); | ||
| Info : Function_Info; | ||
| begin | ||
| if From_Package (Qualified_Name) | ||
| and then Short_Name /= Qualified_Name | ||
| and then not Has_Function (Visible_Functions, Short_Name) | ||
| then |
There was a problem hiding this comment.
Add_Imported_Package_Local_Aliases creates short-name entries in Visible_Functions for imported subprograms, but it doesn’t create a corresponding short-name mapping in Current_Generic_Function_Templates. If an imported generic template body calls another generic template from its origin package using the unqualified name (common for same-package calls), Specialize_Generic_Call won’t find the template (it only keys on the qualified name), so the call won’t be monomorphized and can leak Generic_Args past the frontend. Consider adding a short-name alias for generic templates (e.g., when the qualified template exists) or teaching generic-call specialization to resolve unqualified names against Origin_Package.
|
Follow-up for the two post-merge review findings is now open in PR #202. That branch fixes:
It also carries the current roadmap rename/update that was sitting locally. |
Summary
Implements PR11.11c Safe-native user-defined generics.
This adds:
of ...typed-v6/safei-v5contract support for generic metadataWhat changed
Validation
cd compiler_impl && alr buildpython3 scripts/run_tests.py->764 passed, 1 skipped, 0 failedpython3 scripts/run_samples.py->19 passed, 0 failedpython3 scripts/run_proofs.py->186 proved, 0 failedPR11.11c checkpoint: 5 proved, 0 failedNotes
tests/negative/neg_chan_empty_recv.safe, unchanged from the existing deadlock-analysis deferral.