Sub-expansion pass #195

DCupello1 · 2025-11-12T15:20:50Z

This pass expands the subtyping patterns that appear in the LHS of
function clauses and type family arguments.

It achieves this through the following steps:

For each argument, we collect every unique sub expression.
Then, for each sub expression, we collect every case that is
possible in the subtype. If the specific case additionally carries
values, then we generate binds to add in the function scope.
With all of these cases, for each unique sub expression, we compute
the cartesian product in order to absolutely grab all the possible cases.
See $cvtop to see how this might be done.
Once we have calculated the product, we generate a subst for each product
and proceed to generate the clause/type instance.
Finally, we filter out binds that refer to the subst ids.

For example, take the following types and function:

  syntax A = t1 nat | t2 nat nat
  syntax B = t1 nat | t2 nat nat | t3 | t4 

  def $foo(B) : nat
  def $foo(x : A <: B) = 1
  def $foo(t3) = 2
  def $foo(t4) = 3

Would be transformed as such:

  def $foo(B) : nat
  def $foo{n : nat}(t1(n)) = 1
  def $foo{n1 : nat, n2 : nat}(t2(n1, n2)) = 1
  def $foo(t3) = 2
  def $foo(t4) = 3

To give a slightly more involved example:

  syntax A = t1 | t2
  syntax B = t1 | t2

  def $foo(B) : nat
  def $foo(x : A <: B, y : A <: B) = 1
  def $foo(t3) = 2
  def $foo(t4) = 3

Would be transformed as such:

  syntax A = t1 | t2
  syntax B = t1 | t2 | t3

  def $foo(B) : nat
  def $foo(t1, t1) = 1
  def $foo(t2, t1) = 1
  def $foo(t1, t2) = 1
  def $foo(t2, t2) = 1
  def $foo(t3) = 2
  def $foo(t4) = 3

Currently it has a similar limitation as the sub pass: if you expand type families, then the evaluator (which the validator uses) cannot show that types are in fact equivalent.

Currently a draft pull request until the rework of middlend testing goes through.

nomeata · 2025-11-12T15:58:25Z

Nice!

Once we have calculated the product, we generate a subst for each product
and proceed to generate the clause/type instance.
Finally, we filter out binds that do not appear in the substed rhs.

What would be an example for a binding that can be removed that was not already in the domain of the generated substitution?

DCupello1 · 2025-11-12T16:46:03Z

What would be an example for a binding that can be removed that was not already in the domain of the generated substitution?

In the previous implementation, I made it so that the case expressions generated from the subtype would also generate the binds as well if necessary.

So take this example (as above):

  def $foo(B) : nat
  def $foo{n : nat}(t1(n)) = 1
  def $foo{n1 : nat, n2 : nat}(t2(n1, n2)) = 1
  def $foo(t3) = 2
  def $foo(t4) = 3

However, to make it simple, I would collect all the binds of all of the case expressions and apply it to all of them. So I would have [n, n1, n2] for both the first match and the second match. To mitigate this, I filter any binds that don't appear in in the rhs and premises.

I didn't like this approach, so I have changed it so that the case expressions actually carry the binds with them as well. This means I only filter at the end now to remove the subst ids (in the case above it would be x)

…fted subst generation to own function

DCupello1 · 2025-11-13T11:33:46Z

Should be complete now! Though will need the uncase PR (#191) to be merged first.

nomeata · 2025-11-13T13:35:22Z

This is looking good, for example I get

 ;; ../../../../specification/wasm-3.0/1.2-syntax.types.spectec
 def $zsize(storagetype : storagetype) : nat
   ;; ../../../../specification/wasm-3.0/1.2-syntax.types.spectec
-  def $zsize{numtype : numtype}((numtype : numtype <: storagetype)) = $size(numtype)
+  def $zsize(I32_storagetype) = $size(I32_numtype)
+  ;; ../../../../specification/wasm-3.0/1.2-syntax.types.spectec
+  def $zsize(I64_storagetype) = $size(I64_numtype)
+  ;; ../../../../specification/wasm-3.0/1.2-syntax.types.spectec
+  def $zsize(F32_storagetype) = $size(F32_numtype)
   ;; ../../../../specification/wasm-3.0/1.2-syntax.types.spectec
-  def $zsize{vectype : vectype}((vectype : vectype <: storagetype)) = $vsize(vectype)
+  def $zsize(F64_storagetype) = $size(F64_numtype)
   ;; ../../../../specification/wasm-3.0/1.2-syntax.types.spectec
-  def $zsize{packtype : packtype}((packtype : packtype <: storagetype)) = $psize(packtype)
+  def $zsize(V128_storagetype) = $vsize(V128_vectype)
+  ;; ../../../../specification/wasm-3.0/1.2-syntax.types.spectec
+  def $zsize(I8_storagetype) = $psize(I8_packtype)
+  ;; ../../../../specification/wasm-3.0/1.2-syntax.types.spectec
+  def $zsize(I16_storagetype) = $psize(I16_packtype)

but with

syntax storagetype = 
  | BOT
  | I32
  | I64
  | F32
  | F64
  | V128
  | REF{`null?` : null?, heaptype : heaptype}(null?{null <- `null?`} : null?, heaptype : heaptype)
  | I8
  | I16

this is now partial…

ah, but it seems this was already the case in the source, which has

syntax storagetype hint(desc "storage type") hint(prefix "STORAGETYPE_") = valtype | packtype

def $zsize(storagetype) : nat  hint(show |%|)
def $zsize(numtype) = $size(numtype)
def $zsize(vectype) = $vsize(vectype)
def $zsize(packtype) = $psize(packtype)

Is that just a case of a missing hint(partial)?

nomeata · 2025-11-13T13:40:43Z

For cunpack I get overlapping patterns with superficially conflicting definitions

;; ../../../../specification/wasm-3.0/1.2-syntax.types.spectec
def $cunpack(storagetype : storagetype) : consttype?
  ;; ../../../../specification/wasm-3.0/1.2-syntax.types.spectec
  def $cunpack(I32_storagetype) = ?(I32_consttype)
  ;; ../../../../specification/wasm-3.0/1.2-syntax.types.spectec
  def $cunpack(I64_storagetype) = ?(I64_consttype)
  ;; ../../../../specification/wasm-3.0/1.2-syntax.types.spectec
  def $cunpack(F32_storagetype) = ?(F32_consttype)
  ;; ../../../../specification/wasm-3.0/1.2-syntax.types.spectec
  def $cunpack(F64_storagetype) = ?(F64_consttype)
  ;; ../../../../specification/wasm-3.0/1.2-syntax.types.spectec
  def $cunpack(V128_storagetype) = ?(V128_consttype)
  ;; ../../../../specification/wasm-3.0/1.2-syntax.types.spectec
  def $cunpack(I8_storagetype) = ?(I32_consttype)
  ;; ../../../../specification/wasm-3.0/1.2-syntax.types.spectec
  def $cunpack(I16_storagetype) = ?(I32_consttype)
  ;; ../../../../specification/wasm-3.0/1.2-syntax.types.spectec
  def $cunpack(I32_storagetype) = ?(($lunpack(I32_lanetype) : numtype <: consttype))
  ;; ../../../../specification/wasm-3.0/1.2-syntax.types.spectec
  def $cunpack(I64_storagetype) = ?(($lunpack(I64_lanetype) : numtype <: consttype))
  ;; ../../../../specification/wasm-3.0/1.2-syntax.types.spectec
  def $cunpack(F32_storagetype) = ?(($lunpack(F32_lanetype) : numtype <: consttype))
  ;; ../../../../specification/wasm-3.0/1.2-syntax.types.spectec
  def $cunpack(F64_storagetype) = ?(($lunpack(F64_lanetype) : numtype <: consttype))
  ;; ../../../../specification/wasm-3.0/1.2-syntax.types.spectec
  def $cunpack(I8_storagetype) = ?(($lunpack(I8_lanetype) : numtype <: consttype))
  ;; ../../../../specification/wasm-3.0/1.2-syntax.types.spectec
  def $cunpack(I16_storagetype) = ?(($lunpack(I16_lanetype) : numtype <: consttype))
  def $cunpack{x0 : storagetype}(x0) = ?()

DCupello1 · 2025-11-13T13:58:17Z

Is that just a case of a missing hint(partial)?

That seems to be the case I would say.

For cunpack I get overlapping patterns with superficially conflicting definitions

I do not handle overlapping patterns, since it might not be necessary to remove them for some targets. I could remove them easily if necessary though

nomeata · 2025-11-13T14:01:30Z

I do not handle overlapping patterns, since it might not be necessary to remove them for some targets. I could remove them easily if necessary though

At least the lean4 backend will need that. But that doesn’t mean you have to do that right away, I can also do it at some point.

DCupello1 · 2025-11-13T14:07:07Z

At least the lean4 backend will need that. But that doesn’t mean you have to do that right away, I can also do it at some point.

Rocq will also need it so will probably do it after this gets merged, either as part of this pass or a new pass.

nomeata · 2025-11-14T10:22:13Z

Rocq will also need it so will probably do it after this gets merged, either as part of this pass or a new pass.

Actually Lean has set_option match.ignoreUnusedAlts false so it’s not blocking me.

nomeata · 2025-12-03T16:22:17Z

spectec/src/middlend/subexpansion.ml

+let rec collect_sube_exp e = 
+  let c_func = collect_sube_exp in
+  match e.it with
+  (* Assumption - nested sub expressions do not exist. Must also be a varE. *)


You used the Iter module in #191, any reason to not use it here?

No real reason, probably was trying to get a more functional approach instead of using Iter.

Also since its only traversing through exp I maybe thought it was overkill.

Ah, good point. No issue, was just curious.

I wish we didn't have to duplicate the traversal logic in every pass, but 🤷🏻

Yeah... I really wish there was an easier way to make a generic traversal pass that didn't involve side effects 😅 . I'll look into it more to see if something can be done

DCupello1 added 3 commits November 12, 2025 12:09

Start on sub expansion pass. Validates up to 2.0.

7c34091

Improved handling of generated binds, and removed boilerplate code.

b68dd90

Added type family sub expansion support, and comment description of pass

255e13e

DCupello1 added 2 commits November 12, 2025 16:16

small fix on name generation.

66b12dc

Improved bind handling: each case carries its own binds now.

75b49fa

DCupello1 added 2 commits November 12, 2025 17:24

Further improvement on bind handling: now handles clauses as well. Li…

5974062

…fted subst generation to own function

Merge branch 'uncase-removal-pass' into sub-expansion-pass

c9755ef

DCupello1 marked this pull request as ready for review November 13, 2025 11:33

This was referenced Nov 13, 2025

Uncase removal pass #191

Merged

Improve ids pass #198

Open

nomeata mentioned this pull request Nov 13, 2025

mark zsize and as_deftype as partial #199

Closed

DCupello1 mentioned this pull request Nov 20, 2025

Rocq backend #207

Draft

4 tasks

Merge branch 'main' into sub-expansion-pass

3e673fc

nomeata approved these changes Dec 3, 2025

View reviewed changes

DCupello1 merged commit 0308a06 into main Dec 4, 2025
9 checks passed

Sub-expansion pass #195

Sub-expansion pass #195

Uh oh!

Conversation

DCupello1 commented Nov 12, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

nomeata commented Nov 12, 2025

Uh oh!

DCupello1 commented Nov 12, 2025

Uh oh!

DCupello1 commented Nov 13, 2025

Uh oh!

nomeata commented Nov 13, 2025

Uh oh!

nomeata commented Nov 13, 2025

Uh oh!

DCupello1 commented Nov 13, 2025

Uh oh!

nomeata commented Nov 13, 2025

Uh oh!

DCupello1 commented Nov 13, 2025

Uh oh!

nomeata commented Nov 14, 2025

Uh oh!

nomeata Dec 3, 2025

Choose a reason for hiding this comment

Uh oh!

DCupello1 Dec 4, 2025

Choose a reason for hiding this comment

Uh oh!

nomeata Dec 4, 2025

Choose a reason for hiding this comment

Uh oh!

DCupello1 Dec 4, 2025

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

DCupello1 commented Nov 12, 2025 •

edited

Loading