refactor: Row parsing #116

acl-cqc · 2026-05-01T11:21:31Z

Drive-by but this does read like a few more type aliases wouldn't hurt. How is a tuple of

a list of tuples (String, (Src, BinderType Brat))

a list of tuples ((String, TypeKind), Val Z)

...together "a list of definitions for substituting later on"? ah, the first element is a new solution, the second element is the list for substituting? I'm wondering what all these Strings are too...

acl-cqc · 2026-05-01T11:25:37Z

Does this give a partial match warning? It might be ok, but if Haskell is complaining then you might consider yet another function (kindCheckRow'', hah) that takes just the String inside the Named (and the type) instead of TypeRowElem, as you

acl-cqc · 2026-05-01T11:23:59Z

drive-by but there is no commonality between these two cases, can we make them toplevel cases?

acl-cqc · 2026-05-01T11:04:46Z

Suggested change

simpleTypeRow = fmap aux where aux (p, ty) = Named p ty

simpleTypeRow = fmap $ \(p, ty) -> Named p ty

Suggested change

simpleTypeRow = fmap aux where aux (p, ty) = Named p ty

simpleTypeRow = fmap (uncurry Named)

acl-cqc · 2026-05-01T11:30:25Z

I am really sorry but this does have to be Elaboratable.

acl-cqc · 2026-05-01T11:32:56Z

I am suspicious that the only two types that are Elaborable here are Flat and KindOr Flat....

acl-cqc · 2026-05-01T11:31:40Z

You can't make TypeRowElem derive Functor or something here and use fmap elab instead of elabSigElem here can you? Then we could do away with Elabor(at)able altogether...

acl-cqc · 2026-05-01T11:33:57Z

Seems harmless, I mean we can't really be confused between what has WC and not can we? Why is this sus?

It seems strange to be throwing away this information in elaboration...

acl-cqc · 2026-05-01T11:44:48Z

technically I think this is not necessarily even flat? Given that depends on the ty you parse in?

but in practice the only uses are all flatIO' vtype - which makes this a Parser (TypeRow (WC Flat)) - can you specialise it to that? (And maybe distinguish the names better flatIO' vs flatIO !)

acl-cqc · 2026-05-01T11:49:21Z

Yeah we were removing the WC before, there is still a WC here now and we are not removing it....is that ok? Or is that 'sus'? ;)

Still sus! But now we're one step further into the process without throwing away the FCs 😆

acl-cqc · 2026-05-01T11:56:53Z

Or make WC a Functor and keep the old code here?
(Type sigs for nDecl and vDecl probably a bit OTT here given simplicity of declSignature)

-Original file line number
+Diff line change
@@ Expand Up / @@ -789,7 +789,8 @@ checkClause my fnName cty clause = modily my $ do @@
       (Some stk) <><< (x:xs) = Some (stk :<< x) <><< xs
       -- Process a solution, finding Ends that support the solved types, and return a list of definitions for substituting later on
-      postProcessSolAndOuts :: [(String, (Src, BinderType Brat))] -> [(Tgt, BinderType Brat)] -> Checking ([(String, (Src, BinderType Brat))], [((String, TypeKind), Val Z)])
+      postProcessSolAndOuts :: [(String, (Src, BinderType Brat))] -> [(Tgt, BinderType Brat)]
+                            -> Checking ([(String, (Src, BinderType Brat))], [((String, TypeKind), Val Z)])
       postProcessSolAndOuts sol outputs = worker B0 sol
        where
         worker :: Bwd (String, (Src, BinderType Brat)) -> [(String, (Src, BinderType Brat))] -> Checking ([(String, (Src, BinderType Brat))], [((String, TypeKind), Val Z)])
@@ Expand Down Expand Up @@
     -- Checks the kinds of the types in a dependent row
     kindCheckRow :: Modey m
                  -> String -- for node name
-                 -> [(PortName, ThunkRowType m)] -- The row to process
+                 -> [TypeRowElem (ThunkRowType m)] -- The row to process
                  -> Checking (Some (Ro m Z))
     kindCheckRow my name r = do
       name <- req $ Fresh $ "__kcr_" ++ name
@@ Expand All / @@ -1060,7 +1061,7 @@ kindCheckRow my name r = do @@
     -- evaluation of the type of an Id node passing through such values
     kindCheckAnnotation :: Modey m
                         -> String -- for node name
-                        -> [(PortName, ThunkRowType m)]
+                        -> [TypeRowElem (ThunkRowType m)]
                         -> Checking (CTy m Z)
     kindCheckAnnotation my name outs = do
       trackM "kca"
@@ Expand All / @@ -1080,17 +1081,19 @@ kindCheckRow' :: forall m n @@
                   -> Endz n -- kind outports so far
                   -> VEnv -- from string variable names to VPar's
                   -> (Name, Int) -- node name and next free input (under to 'kindCheck' a type)
-                  -> [(PortName, ThunkRowType m)]
+                  -> [TypeRowElem (ThunkRowType m)]
                   -> Checking (Int, VEnv, Some (Endz :* Ro m n))
     kindCheckRow' _ ez env (_,i) [] = pure (i, env, Some (ez :* R0))
-    kindCheckRow' Braty (ny :* s) env (name,i) ((p, Left k):rest) = do -- s is Stack Z n
+    kindCheckRow' my nys env (name, i) ((Anon ty):rest) = kindCheckRow' my nys env (name, i) ((Named ('_':show i) ty):rest)
+    kindCheckRow' Braty (ny :* s) env (name,i) ((Named p (Left k)):rest) = do -- s is Stack Z n
       let dangling = Ex name (ny2int ny)
       req (Declare (ExEnd dangling) Braty (Left k) Definable) -- assume none are SkolemConst??
       env <- pure $ M.insert (plain p) [(NamedPort dangling p, Left k)] env
       (i, env, ser) <- kindCheckRow' Braty (Sy ny :* (s :<< ExEnd dangling)) env (name, i) rest
       case ser of
         Some (s_m :* ro) -> pure (i, env, Some (s_m :* REx (p,k) ro))
-    kindCheckRow' my ez@(ny :* s) env (name, i) ((p, bty):rest) = case (my, bty) of
+    kindCheckRow' my ez@(ny :* s) env (name, i) ((Named p bty):rest) = case (my, bty) of
       (Braty, Right ty) -> helper ty (Star [])
       (Kerny, ty) -> helper ty (Dollar [])
@@ Expand Down @@

-Original file line number
+Diff line change
@@ -1,6 +1,6 @@
     module Brat.Elaborator where
-    import Control.Monad (forM, (>=>))
+    import Control.Monad ((>=>))
     import Data.Bifunctor (second)
     import Data.List.NonEmpty (NonEmpty(..))
     import Data.Map (empty)
@@ Expand Down Expand Up / @@ -179,6 +179,7 @@ elaborate' (FAnnotation a ts) = do @@
       (SomeRaw a) <- elaborate a
       a <- assertChk a
       a <- assertNoun a
+      ts <- fmap (fmap unWC) <$> traverse elabSigElem ts
       pure $ SomeRaw' (a ::::: ts)
     elaborate' (FInto a b) = elaborate' (FApp b a)
     elaborate' (FOf n e) = do
@@ Expand All / @@ -187,14 +188,33 @@ elaborate' (FOf n e) = do @@
       SomeRaw e <- elaborate e
       e <- assertNoun e
       pure $ SomeRaw' (ROf n e)
-    elaborate' (FFn cty) = pure $ SomeRaw' (RFn cty)
-    elaborate' (FKernel sty) = pure $ SomeRaw' (RKernel sty)
+    elaborate' (FFn cty) = SomeRaw' . RFn . fmap (fmap unWC) <$> traverse elabSigElem cty
+    elaborate' (FKernel cty) = SomeRaw' . RKernel . fmap (fmap unWC) <$> traverse elabSigElem cty
     elaborate' FIdentity = pure $ SomeRaw' RIdentity
     -- We catch underscores in the top-level elaborate so this case
     -- should never be triggered
     elaborate' FUnderscore = Left (dumbErr (InternalError "Unexpected '_'"))
     elaborate' FFanOut = pure $ SomeRaw' RFanOut
     elaborate' FFanIn = pure $ SomeRaw' RFanIn
+    class Elaborable t where
+      type Elaborated t
+      elab :: WC t -> Either Error (WC (Elaborated t))
+    -- This is a hack to make elabSigElem nice
+    instance Elaborable Flat where
+      type Elaborated Flat = Raw Chk Noun
+      elab = elaborateChkNoun
+    instance Elaborable t => Elaborable (KindOr t) where
+      type Elaborated (KindOr t) = KindOr (Elaborated t)
+      elab (WC fc (Left k)) = pure (WC fc (Left k))
+      elab (WC fc (Right ty)) = fmap Right <$> elab (WC fc ty)
+    elabSigElem :: Elaborable t
+                => TypeRowElem (WC t)
+                -> Either Error (TypeRowElem (WC (Elaborated t)))
+    elabSigElem (Anon ty) = Anon <$> elab ty
+    elabSigElem (Named p ty) = Named p <$> elab ty
     elabBody :: FBody -> FC -> Either Error (FunBody Raw Noun)
     elabBody (FClauses cs) fc = ThunkOf . WC fc . Clauses <$> traverse elab1Clause cs
@@ Expand All / @@ -217,14 +237,17 @@ elabBody FUndefined _ = pure Undefined @@
     elabFunDecl :: FDecl -> Either Error RawFuncDecl
     elabFunDecl d = do
       rc <- elabBody (fnBody d) (fnLoc d)
+      sig <- traverse elabSigElem (fnSig d)
       pure $ FuncDecl
         { fnName = fnName d
         , fnLoc = fnLoc d
-        , fnSig = fnSig d
+        , fnSig = fmap unWC <$> sig -- sus
         , fnBody = rc
         , fnLocality = fnLocality d
         }
+    elabAlias :: FAlias -> Either Error RawAlias
+    elabAlias (TypeAlias fc name tys tm) = TypeAlias fc name tys . unWC <$> elaborateChkNoun (WC fc tm)
     elabEnv :: FEnv -> Either Error RawEnv
-    elabEnv (ds, x) = (,x,empty) <$> forM ds elabFunDecl
+    elabEnv (ds, as) = (,,empty) <$> traverse elabFunDecl ds <*> traverse elabAlias as

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

refactor: Row parsing #116

Uh oh!

Diff view

Diff view

There are no files selected for viewing

acl-cqc May 1, 2026

Uh oh!

acl-cqc May 1, 2026

Uh oh!

acl-cqc May 1, 2026

Uh oh!

acl-cqc May 1, 2026

Uh oh!

acl-cqc May 1, 2026

Uh oh!

acl-cqc May 1, 2026

Uh oh!

acl-cqc May 1, 2026

Uh oh!

acl-cqc May 1, 2026

Uh oh!

acl-cqc May 1, 2026

Uh oh!

croyzor May 1, 2026

Uh oh!

acl-cqc May 1, 2026

Uh oh!

acl-cqc May 1, 2026

Uh oh!

acl-cqc May 1, 2026

Uh oh!

croyzor May 1, 2026

Uh oh!

acl-cqc May 1, 2026

Uh oh!

Uh oh!

Uh oh!

-Original file line number
+Diff line change
@@ Expand Up / @@ -13,9 +13,7 @@ import Brat.Syntax.Common hiding (end) @@
     import qualified Brat.Syntax.Common as Syntax
     import Brat.Syntax.FuncDecl (FuncDecl(..), Locality(..))
     import Brat.Syntax.Concrete
-    import Brat.Syntax.Raw
     import Brat.Syntax.Simple
-    import Brat.Elaborator
     import Data.Bracket
     import Util ((**^))
@@ Expand Down Expand Up @@
         match TypeColon
         (p,) . unWC <$> typekind
-    vtype :: Parser (WC (Raw Chk Noun))
-    vtype = cnoun (expr' PApp)
+    vtype :: Parser (WC Flat)
+    vtype = expr' PApp
     -- Parse a row of type and kind parameters
     -- N.B. kinds must be named
     -- TODO: Update definitions so we can retain the FC info, instead of forgetting it
-    rawIOFC :: Parser (TypeRow (WC (KindOr RawVType)))
-    rawIOFC = rowElem `sepBy` void (try comma)
+    flatIO :: Parser [FlatIO]
+    flatIO = rowElem `sepBy` void (try comma)
      where
-      rowElem :: Parser (TypeRowElem (WC (KindOr RawVType)))
+      rowElem :: Parser FlatIO
       rowElem = try (inBrackets Paren rowElem') <|> rowElem'
-      rowElem' :: Parser (TypeRowElem (WC (KindOr RawVType)))
+      rowElem' :: Parser FlatIO
       rowElem' = try namedKind <|> try namedType <|> ((\(WC tyFC ty) -> Anon (WC tyFC (Right ty))) <$> vtype)
-      namedType :: Parser (TypeRowElem (WC (KindOr RawVType)))
+      namedType :: Parser FlatIO
       namedType = do
         WC pFC p <- port
         match TypeColon
         WC tyFC ty <- vtype
         pure (Named p (WC (spanFC pFC tyFC) (Right ty)))
-      namedKind :: Parser (TypeRowElem (WC (KindOr ty)))
+      namedKind :: Parser FlatIO
       namedKind = do
         WC pFC p <- port
         match TypeColon
         WC kFC k <- typekind
         pure (Named p (WC (spanFC pFC kFC) (Left k)))
-    rawIO :: Parser [RawIO]
-    rawIO = fmap (fmap unWC) <$> rawIOFC
-    rawIO' :: Parser ty -> Parser (TypeRow ty)
-    rawIO' tyP = rowElem `sepBy` void (try comma)
+    flatIO' :: Parser ty -> Parser (TypeRow ty)
+    flatIO' tyP = rowElem `sepBy` void (try comma)
      where
       rowElem = try (inBrackets Paren rowElem') <|> rowElem'
@@ Expand All / @@ -305,13 +300,13 @@ rawIO' tyP = rowElem `sepBy` void (try comma) @@
            Just (WC _ p) -> Named p <$> tyP
            Nothing -> Anon <$> tyP
-    spanningFC :: TypeRow (WC ty) -> Parser (WC (TypeRow ty))
-    spanningFC [] = customFailure (Custom "Internal: RawIO shouldn't be empty")
-    spanningFC [x] = pure (WC (fcOf $ forgetPortName x) [unWC <$> x])
-    spanningFC (x:xs) = pure (WC (spanFC (fcOf $ forgetPortName x) (fcOf . forgetPortName $ last xs)) (fmap unWC <$> (x:xs)))
+    spanningFC :: TypeRow (WC ty) -> Parser (WC (TypeRow (WC ty)))
+    spanningFC [] = customFailure (Custom "Internal: FlatIO shouldn't be empty")
+    spanningFC [x] = pure (WC (fcOf (forgetPortName x)) [x])
+    spanningFC (x:xs) = pure (WC (spanFC (fcOf (forgetPortName x)) (fcOf (forgetPortName (last xs)))) (x:xs))
-    rawIOWithSpanFC :: Parser (WC [RawIO])
-    rawIOWithSpanFC = spanningFC =<< rawIOFC
+    flatIOWithSpanFC :: Parser (WC [FlatIO])
+    flatIOWithSpanFC = spanningFC =<< flatIO
     vec :: Parser (WC Flat)
     vec = (\(WC fc x) -> WC fc (unWC (vec2Cons fc x))) <$> inBracketsFC Square elems
@@ Expand Down Expand Up / @@ -342,15 +337,15 @@ cthunk :: Parser (WC Flat) @@
     cthunk = try bratFn <|> try kernel <|> thunk
      where
       bratFn = inBracketsFC Brace $ do
-        ss <- rawIO
+        ss <- flatIO
         match Arrow
-        ts <- rawIO
+        ts <- flatIO
         pure $ FFn (ss :-> ts)
       kernel = inBracketsFC Brace $ do
-        ss <- rawIO' (unWC <$> vtype)
+        ss <- flatIO' vtype
         match Lolly
-        ts <- rawIO' (unWC <$> vtype)
+        ts <- flatIO' vtype
         pure $ FKernel (ss :-> ts)
@@ Expand Down Expand Up @@
       annotation = do
         tm <- subExpr PAnn
         colon <- matchFC TypeColon
-        WC (spanFCOf tm colon) . FAnnotation tm <$> rawIO
+        WC (spanFCOf tm colon) . FAnnotation tm <$> flatIO
       letIn :: Parser (WC Flat)
       letIn = label "let ... in" $ do
@@ Expand Down Expand Up @@
     fanout = inBracketsFC Square (FFanOut <$ match Slash <* match Backslash)
     fanin = inBracketsFC Square (FFanIn <$ match Backslash <* match Slash)
-    cnoun :: Parser (WC Flat) -> Parser (WC (Raw 'Chk 'Noun))
-    cnoun pe = do
-      e <- pe
-      case elaborate e of
-        Left err -> fail (showError err)
-        Right (SomeRaw r) -> case do
-          r <- assertChk r
-          assertNoun r
-         of
-          Left err -> fail (showError err)
-          Right r -> pure r
     decl :: Parser FDecl
     decl = do
           (fc, nm, ty, body) <- do
             WC startFC nm <- simpleName
             WC _ ty <- declSignature
             let allow_clauses = case ty of
-                                     [Named _ (Right t)] -> is_fun_ty t
-                                     [Anon (Right t)] -> is_fun_ty t
+                                     [Named _ (WC _ (Right t))] -> is_fun_ty t
+                                     [Anon (WC _ (Right t))] -> is_fun_ty t
                                      _ -> False
             WC endFC body <- if allow_clauses
                              then declClauses nm <|> declNounBody nm
@@ Expand All / @@ -628,9 +610,9 @@ decl = do @@
             , fnLocality = Local
             }
         where
-          is_fun_ty :: RawVType -> Bool
-          is_fun_ty (RFn _) = True
-          is_fun_ty (RKernel _) = True
+          is_fun_ty :: Flat -> Bool
+          is_fun_ty (FFn _) = True
+          is_fun_ty (FKernel _) = True
           is_fun_ty _ = False
           declClauses :: String -> Parser (WC FBody)
@@ Expand Down Expand Up / @@ -735,11 +717,11 @@ pstmt = ((comment <?> "comment") <&> \_ -> ([] , [])) @@
             <|> try (extDecl                         <&> \x -> ([x], []))
             <|> ((decl <?> "declaration")            <&> \x -> ([x], []))
      where
-      alias :: Parser RawAlias
+      alias :: Parser FAlias
       alias = aliasContents <&>
               \(fc, name, args, ty) -> TypeAlias fc name args ty
-      aliasContents :: Parser (FC, QualName, [(String, TypeKind)], RawVType)
+      aliasContents :: Parser (FC, QualName, [(String, TypeKind)], Flat)
       aliasContents = do
         WC startFC () <- matchFC (K KType)
         WC _ alias <- qualName
@@ Expand Down Expand Up / @@ -780,31 +762,31 @@ pstmt = ((comment <?> "comment") <&> \_ -> ([] , [])) @@
                      , fnLocality = Extern symbol
                      }
-    declSignature :: Parser (WC [RawIO])
+    declSignature :: Parser (WC [FlatIO])
     declSignature = try nDecl <|> vDecl where
-     nDecl = match TypeColon >> rawIOWithSpanFC
-     vDecl = functionSignature <&> fmap (\ty -> [Named "thunk" (Right ty)])
+     nDecl :: Parser (WC [FlatIO])
+     nDecl = match TypeColon >> flatIOWithSpanFC
+     vDecl :: Parser (WC [FlatIO])
+     vDecl = functionSignature <&> (\(WC fc ty) -> WC fc [Named "thunk" (WC fc (Right ty))])
-     functionSignature :: Parser (WC RawVType)
-     functionSignature = try (fmap RFn <$> ctype) <|> (fmap RKernel <$> kernel)
+     functionSignature :: Parser (WC Flat)
+     functionSignature = try (fmap FFn <$> ctype) <|> (fmap FKernel <$> kernel)
       where
-       ctype :: Parser (WC RawCType)
+       ctype :: Parser (WC (CType' FlatIO))
        ctype = do
-         WC startFC ins <- inBracketsFC Paren rawIO
+         WC startFC ins <- inBracketsFC Paren flatIO
          match Arrow
-         WC endFC outs <- rawIOWithSpanFC
+         WC endFC outs <- flatIOWithSpanFC
          pure (WC (spanFC startFC endFC) (ins :-> outs))
-       kernel :: Parser (WC RawKType)
+       kernel :: Parser (WC (CType' (TypeRowElem (WC Flat))))
        kernel = do
-         WC startFC ins <- inBracketsFC Paren $ rawIO' (unWC <$> vtype)
+         WC startFC ins <- inBracketsFC Paren $ flatIO' vtype
          match Lolly
-         WC endFC outs <- spanningFC =<< rawIO' vtype
+         WC endFC outs <- spanningFC =<< flatIO' vtype
          pure (WC (spanFC startFC endFC) (ins :-> outs))
     pfile :: Parser ([Import], FEnv)
     pfile = do
       imports <- many pimport
@@ Expand Down @@

refactor: Row parsing #116

Are you sure you want to change the base?

Uh oh!

refactor: Row parsing #116

Uh oh!

Uh oh!

Diff view

Diff view

There are no files selected for viewing

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!