refactor: Row parsing

brat/Brat/Checker.hs

@@ -28,7 +28,7 @@ import Brat.Checker.Helpers
 import Brat.Checker.Monad
 import Brat.Checker.Quantity
 import Brat.Checker.SolveHoles (typeEq)
-import Brat.Checker.SolvePatterns (argProblems, argProblemsWithLeftovers, solve, typeOfEnd)
+import Brat.Checker.SolvePatterns (argProblems, argProblemsWithLeftovers, solve, typeOfEnd, Solution)
 import Brat.Checker.Types
 import Brat.Constructors
 import Brat.Error
@@ -789,10 +789,11 @@ 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 :: Solution Brat -> [(Tgt, BinderType Brat)]
+                        -> Checking (Solution 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)])
+    worker :: Bwd (String, (Src, BinderType Brat)) -> Solution Brat -> Checking (Solution Brat, [((String, TypeKind), Val Z)])
     worker zx [] = (, []) <$> outputDeps zx [] outputs
     worker zx (entry@(patVar, (src, Left k)):sol) = let vsrc = VApp (VPar (toEnd src)) B0 in do
       trackM ("processSol (kinded): " ++ show entry)
@@ -1049,7 +1050,7 @@ kindCheck ((_, k):_) tm = typeErr $ "Expected " ++ show tm ++ " to have kind " +
 -- 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
@@ -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"
@@ -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 [])
 

brat/Brat/Checker/Helpers.hs

@@ -110,13 +110,7 @@ pullPortsRow :: Show ty
              -> Checking [(NamedPort e, ty)]
 pullPortsRow = pullPorts (portName . fst) showRow
 
-pullPortsSig :: Show ty
-             => [PortName]
-             -> [(PortName, ty)]
-             -> Checking [(PortName, ty)]
-pullPortsSig = pullPorts fst showSig
-
-pullPorts :: forall a
+pullPorts :: forall a ty
            . (a -> PortName) -- A way to get a port name for each element
           -> ([a] -> String) -- A way to print the list
           -> [PortName] -- Things to pull to the front
@@ -134,10 +128,7 @@ pullPorts toPort showFn to_pull types =
 
 ensureEmpty :: Show ty => String -> [(NamedPort e, ty)] -> Checking ()
 ensureEmpty _ [] = pure ()
-ensureEmpty str xs = err $ InternalError $ "Expected empty " ++ str ++ ", got:\n  " ++ showSig (rowToSig xs)
-
-rowToSig :: Traversable t => t (NamedPort e, ty) -> t (PortName, ty)
-rowToSig = fmap $ first portName
+ensureEmpty str xs = err $ InternalError $ "Expected empty " ++ str ++ ", got:\n  " ++ showRow xs
 
 showMode :: Modey m -> String
 showMode Braty = ""
@@ -151,14 +142,17 @@ type family ThunkRowType (m :: Mode) where
   ThunkRowType Brat = KindOr (Term Chk Noun)
   ThunkRowType Kernel = Term Chk Noun
 
+simpleTypeRow :: [(PortName, ty)] -> [TypeRowElem ty]
+simpleTypeRow = fmap (uncurry Named)
+
 mkThunkTy :: Modey m
           -> ThunkFCType m
           -> [(PortName, ThunkRowType m)]
           -> [(PortName, ThunkRowType m)]
           -> Term Chk Noun
 -- mkThunkTy Braty fc ss ts = C (WC fc (ss :-> ts))
-mkThunkTy Braty _ ss ts = C (ss :-> ts)
-mkThunkTy Kerny () ss ts = K (ss :-> ts)
+mkThunkTy Braty _ ss ts = C (simpleTypeRow ss :-> simpleTypeRow ts)
+mkThunkTy Kerny () ss ts = K (simpleTypeRow ss :-> simpleTypeRow ts)
 
 anext :: forall m i j k
        . EvMode m

brat/Brat/Checker/SolvePatterns.hs

@@ -1,4 +1,4 @@
-module Brat.Checker.SolvePatterns (argProblems, argProblemsWithLeftovers, solve, typeOfEnd) where
+module Brat.Checker.SolvePatterns (argProblems, argProblemsWithLeftovers, solve, typeOfEnd, Solution) where
 
 import Brat.Checker.Monad
 import Brat.Checker.Helpers
@@ -40,6 +40,8 @@ import Data.Type.Equality ((:~:)(..), testEquality)
 -- N.B. we make no assumptions about the values and types being normalised wrt `endVals`
 type Problem = [({-Int,-} Src, Pattern)] -- let's not do fiddly positional arithmetic on the fly
 
+type Solution m = [(String, (Src, BinderType m))]
+
 typeOfSrc my src = typeOfEnd my (ExEnd (end src))
 
 -- Solve is given a `Problem` (a mapping from wires to patterns) and uses this
@@ -59,7 +61,7 @@ solve :: forall m. Modey m
        -> Problem
        -> Checking (-- [(Int, Test)] -- too much too hugr too soon?
                     [(Src, PrimTest (BinderType m))]
-                   ,[(String, (Src, BinderType m))] -- Remember the names given by programmers
+                   ,Solution m -- Remember the names given by programmers
                    )
 solve _ [] = pure ([], [])
 solve my ((src, DontCare):p) = do
@@ -145,7 +147,7 @@ solveConstructor :: EvMode m
                  -> Val Z
                  -> Problem
                  -> Checking ([(Src, PrimTest (BinderType m))]
-                             ,[(String, (Src, BinderType m))]
+                             ,Solution m
                              )
 solveConstructor my src (c, abs) ty p = do
   (CArgs pats _ patRo argRo, (tycon, tyargs)) <- lookupConstructor my c ty

brat/Brat/Elaborator.hs

@@ -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)
@@ -179,6 +179,7 @@ elaborate' (FAnnotation a ts) = do
   (SomeRaw a) <- elaborate a
   a <- assertChk a
   a <- assertNoun a
+  ts <- fmap (fmap unWC) <$> elabIO ts
   pure $ SomeRaw' (a ::::: ts)
 elaborate' (FInto a b) = elaborate' (FApp b a)
 elaborate' (FOf n e) = do
@@ -187,15 +188,25 @@ 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) <$> elabIO cty
+elaborate' (FKernel cty) = SomeRaw' . RKernel . fmap (fmap unWC) <$> elabSig 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
 
+elaborateBratType :: WC (KindOr Flat) -> Either Error (WC (KindOr (Raw Chk Noun)))
+elaborateBratType (WC fc (Left k)) = pure (WC fc (Left k))
+elaborateBratType (WC fc (Right ty)) = fmap Right <$> elaborateChkNoun (WC fc ty)
+
+elabSig :: Traversable t => t (TypeRowElem (WC Flat)) -> Either Error (t (TypeRowElem (WC (Raw Chk Noun))))
+elabSig = traverse (traverse elaborateChkNoun)
+
+elabIO :: Traversable t => t FlatIO -> Either Error (t (TypeRowElem (WC (KindOr (Raw Chk Noun)))))
+elabIO = traverse (traverse elaborateBratType)
+
 elabBody :: FBody -> FC -> Either Error (FunBody Raw Noun)
 elabBody (FClauses cs) fc = ThunkOf . WC fc . Clauses <$> traverse elab1Clause cs
  where
@@ -217,14 +228,17 @@ elabBody FUndefined _ = pure Undefined
 elabFunDecl :: FDecl -> Either Error RawFuncDecl
 elabFunDecl d = do
   rc <- elabBody (fnBody d) (fnLoc d)
+  sig <- elabIO (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