Skip to content

[aslspec][asl reference] stronger subsumption test for function types#1756

Merged
Roman-Manevich merged 2 commits intomasterfrom
aslspec-stronger-subsumption-test
Mar 24, 2026
Merged

[aslspec][asl reference] stronger subsumption test for function types#1756
Roman-Manevich merged 2 commits intomasterfrom
aslspec-stronger-subsumption-test

Conversation

@Roman-Manevich
Copy link
Copy Markdown
Collaborator

@Roman-Manevich Roman-Manevich commented Mar 22, 2026

The type subsumption test for functions required equivalence between the subtype and supertype. This proved to be too weak for static_env_to_env.

  • This PR strengthens the subsumption test for functions by requiring that the domain type of the subtype subsumes the domain type of the supertpe and the range type of the subtype is subsumed by the range type of the supertpe. Also, the total flag of the subtype implies the total flag of the supertype.
  • Added a rule for static_env_to_env and updated StaticEvaluation.tex with the auto-generated prose and inference rule.
  • Added a rule for apply_binop_extremities and upated SymbolicSubsumptionTesting.tex.

@Roman-Manevich Roman-Manevich changed the title [aslspec][asl reference] stronger subsumption test for functions and imported static_env_to_env to aslspec [aslspec][asl reference] stronger subsumption test for function types Mar 22, 2026
@Roman-Manevich Roman-Manevich force-pushed the aslspec-stronger-subsumption-test branch 2 times, most recently from 8807740 to bf33e4d Compare March 23, 2026 11:33
@Roman-Manevich Roman-Manevich force-pushed the aslspec-stronger-subsumption-test branch from bf33e4d to ebb2632 Compare March 23, 2026 11:47
@Roman-Manevich Roman-Manevich merged commit 97c6274 into master Mar 24, 2026
4 checks passed
@Roman-Manevich Roman-Manevich deleted the aslspec-stronger-subsumption-test branch March 24, 2026 13:09
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants