Conversation
acl-cqc
left a comment
acl-cqc
left a comment
There was a problem hiding this comment.
I can't not approve given this has examples of thinnings that execute as well as typecheck ;-) but I'd like either removal of CRefl or a good justification of why it should stay in (what it does, use in an example) first please...
| (RPr ("value", VApp (VInx VZ) B0) R0))]) | ||
| ,(CTrue, M.fromList [(CBool, CArgs [] Zy R0 R0)]) | ||
| ,(CFalse, M.fromList [(CBool, CArgs [] Zy R0 R0)]) | ||
| ,(COmit, M.fromList |
There was a problem hiding this comment.
I mean, I'm assuming we can't add the corresponding entry for CRefl here
| pattern CConcatEqOdd = PrefixName [] "concatEqOdd" | ||
| pattern CRiffle = PrefixName [] "riffle" | ||
| pattern CRefl = PrefixName [] "refl" | ||
| pattern COmit = PrefixName [] "omit" |
There was a problem hiding this comment.
Somewhere round here (where COmit is declared) we should comment that the "opposite" of COmit is CSucc, i.e. nobody should go looking for CInclude
| -- This type is WRONG | ||
| test :: Vec(X, 2) <<< Vec(X, 2) | ||
| test = {0..} -- The identity thinning | ||
| identity(n :: #) -> Thin(n, n) |
There was a problem hiding this comment.
Ok so we fix the parser failure by changing a <<< b into Thin(a,b)....I mean, that's the PR, right? 😁 😁
There was a problem hiding this comment.
It's a happy coincidence that these two functions lined up in the diff!
| go2 :: Vec(Nat, 3) | ||
| go2 = select(!, !, !, thinning1, [1,2,3,4,5]) | ||
|
|
||
| --!exec [[3]] |
|
Agreed! I thought I had pulled out the |
2 participants
Add a datatype of thinnings, with static execution in the interpreter.
This only gets us a subset of the functionality that we ultimately want, because we want to add a constraint framework that can tell when a nat is equal to the length of
omits in a thinning