Conversation
gabriel-barrett
force-pushed
the
type-alias
branch
5 times, most recently
from
fb8b6f0 to
1cf0414
Compare
arthurpaulino
left a comment
arthurpaulino
left a comment
There was a problem hiding this comment.
Looking mostly good!
Besides my comments below, I should say that the files where the new U64 type has most value are the hash-related ones, Blake3.lean and Sha256.lean.
These U64s on the kernel types will be soon replaced by single Gs anyways.
Tests/Aiur/Aiur.lean
Outdated
| fn alias_basic(x: U8) -> U8 { | ||
| x + x | ||
| } | ||
|
|
||
| fn alias_array(x: U64) -> G { | ||
| x[0] + x[7] | ||
| } | ||
|
|
||
| fn alias_tuple(p: Pair) -> G { | ||
| let (a, b) = p; | ||
| a * b | ||
| } | ||
|
|
||
| fn alias_nested(x: U32) -> U8 { | ||
| let ((a, _), _) = x; | ||
| a | ||
| } | ||
|
|
||
| fn alias_in_struct() -> Pair { | ||
| (3, 4) | ||
| } |
There was a problem hiding this comment.
Can these tests be merged into a single one? They're so simple I'm not sure it's worth paying their costs. The thing is: type aliases are eliminated on the simplification+compilation phase and don't result on novel bytecode operators. In that sense, it should suffice to have an unified, bulkier, test exercising such type expansions.
Ix/Aiur/Simple.lean
Outdated
| -- The first check happens on the original terms (but with expanded types). | ||
| decls.foldlM (init := ()) fun _ (_, decl) => match decl with | ||
| | .function f => do let _ ← (checkFunction f) (getFunctionContext f decls); pure () | ||
| | _ => pure () |
There was a problem hiding this comment.
This is now slightly more cryptic. Can it be simplified towards what we have on main?
There was a problem hiding this comment.
It used to check the toplevel functions, but the declarations hold the functions with expanded types. But HashMap does not have forM, so it looks slightly uglier. Plus, toplevel functions are separated, and declarations have other stuff like datatypes and constructors, that's why it has a match statement now
gabriel-barrett
force-pushed
the
type-alias
branch
2 times, most recently
from
394d79c to
93c030c
Compare
Add IndexMap.forM and use it in checkAndSimplify for cleaner iteration over declarations when only side effects (type-checking) are needed.
gabriel-barrett
force-pushed
the
type-alias
branch
from
3fa6aaa to
e210bb2
Compare
3 participants
Adds type aliases to Aiur, for example, U64 = [G; 8]