Conversation
acl-cqc
left a comment
There was a problem hiding this comment.
Yes! This looks fab, thank you 👍 😄. I don't think any comments are big except possibly in Elaborator.hs. Do you object to CType' or WC being functors? I could do that myself if you like the idea.
For awhile I thought this was keeping the named/anonymous distinction into the graph, something I tried once but couldn't get through, but now I realize this is a different change, albeit probably a big step towards the former. Love it!
Maybe edit the description where you say in Core to "in Term" or something that is more clearly still talking about parsing not the brat graph. (I guess writing Brat.Syntax.Core would also make that clear)
| ThunkRowType Kernel = Term Chk Noun | ||
|
|
||
| simpleTypeRow :: [(PortName, ty)] -> [TypeRowElem ty] | ||
| simpleTypeRow = fmap aux where aux (p, ty) = Named p ty |
There was a problem hiding this comment.
| simpleTypeRow = fmap aux where aux (p, ty) = Named p ty | |
| simpleTypeRow = fmap $ \(p, ty) -> Named p ty |
There was a problem hiding this comment.
| simpleTypeRow = fmap aux where aux (p, ty) = Named p ty | |
| simpleTypeRow = fmap (uncurry Named) |
| showSig (x:xs) | ||
| = intercalate ", " [ '(':p ++ " :: " ++ show ty ++ ")" | ||
| | (p, ty) <- x:xs] | ||
| showSig (hd:tl) = parens $ concat (tail (showElem hd) ++ [unwords (showElem x) | x <- tl]) |
There was a problem hiding this comment.
- I don't see
parenshere before? - can we not use
intercalate? It look like it does a much neater job of inserting the commas than thistail (showElem hd)...(also you've dropped the space after the comma here, is that deliberate?)
There was a problem hiding this comment.
IOW
| showSig (hd:tl) = parens $ concat (tail (showElem hd) ++ [unwords (showElem x) | x <- tl]) | |
| showSig xs@(_:_) = intercalate ", " (map showElem xs) |
and remove , at the start of showElem
There was a problem hiding this comment.
Very similar to showRow of course, maybe you can combine them by converting from NamedPort to TypeRowElem
|
|
||
| -- Type annotations (annotating a term with its outputs) | ||
| (:::) :: WC (Term Chk Noun) -> [Output] -> Term Syn Noun | ||
| (:::) :: WC (Term Chk Noun) -> [TypeRowElem (KindOr (Term Chk Noun))] -> Term Syn Noun |
There was a problem hiding this comment.
can you now remove the Output type alias?
| | PApp | ||
| deriving (Bounded, Enum, Eq, Ord, Show) | ||
|
|
||
| data TypeAliasF tm = TypeAlias FC QualName [(PortName,TypeKind)] tm deriving Show |
There was a problem hiding this comment.
What's the F? that it has an FC in it? I'd be tempted to call it TypeAliasFC if you think it's important to say that, again not perfect I admit
There was a problem hiding this comment.
The F is for "Functor", to say that this is the generic definition, but I guess it'd be more consistent to call it TypeAlias'
| unelab _ _ (tm ::: outs) = FAnnotation (unelab Chky Nouny <$> tm) (toRawRo outs) | ||
| unelab _ _ (tm ::: outs) = FAnnotation (unelab Chky Nouny <$> tm) (f outs) | ||
| where | ||
| f :: [TypeRowElem (KindOr (Term Chk Noun))] -> [TypeRowElem (WC (KindOr Flat))] |
There was a problem hiding this comment.
Nit: this might be slightly easier to read as f :: (KindOr (Term Chk Noun)) -> WC (KindOr Flat) and put the outer two fmaps at the callsite
The outermost fmap is just over the list, so that could even just be map, too
There was a problem hiding this comment.
Ah, actually this is just the same as unelabRo below, so just use that
|
|
||
| Internal error: Expected empty unders after abstract, got: | ||
| (b1 :: Int) | ||
| (_1 :: Int) |
There was a problem hiding this comment.
Yes!!! That's much more sensible!!!
(Just to check - is it even possible to call something _1 and get this message yourself? We should choose the synthetic _ prefix so that it isn't...e.g. consider '0)
| ^^^^^^^^^ | ||
|
|
||
| Port a1 is ambiguous in (a1 :: Nat), (a1 :: Nat) | ||
| Port not found: a1 in (_0 :: Nat, _0 :: Nat) |
There was a problem hiding this comment.
Yay! :).
Can we try a similar test case where you explicitly pull _0 and see that that doesn't work (the element is anonymous, not named; the synthetic _ is only for printing/displaying, not pulling)?
There was a problem hiding this comment.
Good catch! The idea is that _0 isn't a valid user-supplied name for a port, but because of this it's not in our grammar for port pulling either, I'll add it back in.
I think the grammar for ports is [a-zA-Z][0-9a-zA-Z]*, so we could make the automatically inferred ports just 0,1,2...
| ^^^^^^^^^^^ | ||
|
|
||
| Type error: Expected a (kernel) function or vector of functions, got { (a1 :: Bool) -> (a1 :: { (a1 :: Qubit) -o (a1 :: Qubit) }) } | ||
| Type error: Expected a (kernel) function or vector of functions, got { (_0 :: Bool) -> (_1 :: { (_0 :: Qubit) -o (_0 :: Qubit) }) } |
There was a problem hiding this comment.
Hmmmm ok. So it would actually be a different change (but still good as a later PR I guess) to carry this on through into the later stages of the compiler, changing NamedPort to distinguish between named/unnamed (which could be done in a few different ways). I might have another go at that....
| (addN2.brat_globals_decl_13_addN,BratNode Id [("thunk",{ (inp :: Int) -> (out :: Int) })] [("thunk",{ (inp :: Int) -> (out :: Int) })]) | ||
| (addN2.brat_globals_prim_2_N,BratNode (Prim ("","N")) [] [("value",Int)]) | ||
| (addN2.brat_globals_prim_8_add,BratNode (Prim ("","add")) [] [("a1",{ (a :: Int), (b :: Int) -> (c :: Int) })]) | ||
| (addN2.brat_globals_prim_8_add,BratNode (Prim ("","add")) [] [("_0",{ (a :: Int), (b :: Int) -> (c :: Int) })]) |
There was a problem hiding this comment.
So at some point we should try to make these anonymous too, I'm not quite sure even where we'd have to change, might be NamedPort (https://github.com/Quantinuum/brat/pull/116/changes#r3173191053). Not for this PR, fine...
Redo the way we represent rows in syntax.
TermasTypeRowElem ty(= Named String ty | Anon ty) rather than adding dummy names when desugaringFlatsyntax so that it doesn't mix in anyRawterms to represent types in rowsNow,
Brat.Syntax.Rawonly really does some disambiguation between variables and constructors, and we should soon be able to get rid of it altogether!