From 8c3b8fd19a522e128fc2852e3c9fe4fbd1e3465c Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Mon, 27 Apr 2026 10:54:08 +0100 Subject: [PATCH 01/14] Redo row parsing --- brat/Brat/Checker.hs | 15 +-- brat/Brat/Checker/Helpers.hs | 20 ++-- brat/Brat/Elaborator.hs | 33 +++++- brat/Brat/Parser.hs | 102 ++++++++---------- brat/Brat/Syntax/Common.hs | 20 ++-- brat/Brat/Syntax/Concrete.hs | 16 +-- brat/Brat/Syntax/Core.hs | 10 +- brat/Brat/Syntax/Raw.hs | 90 +++++----------- brat/Brat/Unelaborator.hs | 52 +++------ brat/test/Test/Syntax/Let.hs | 4 +- brat/test/golden/binding/let.brat.golden | 2 +- .../golden/error/apply_two_thunks.brat.golden | 2 +- brat/test/golden/error/empty_into.brat.golden | 4 +- .../error/fanout-diff-types.brat.golden | 2 +- .../error/fanout-not-enough-overs.brat.golden | 2 +- brat/test/golden/error/pair.brat.golden | 4 +- .../error/portpull-ambiguous.brat.golden | 2 +- brat/test/golden/error/portpull.brat.golden | 2 +- .../golden/error/remaining_holes.brat.golden | 4 +- .../error/toplevel-leftovers.brat.golden | 4 +- .../error/toplevel-leftovers2.brat.golden | 4 +- .../error/toplevel-leftovers3.brat.golden | 2 +- .../error/vectorise-type-mismatch.brat.golden | 2 +- brat/test/golden/error/vectorise3.brat.golden | 2 +- brat/test/golden/graph/addN2.brat.graph | 2 +- brat/test/golden/graph/cons.brat.graph | 4 +- brat/test/golden/graph/id.brat.graph | 2 +- brat/test/golden/graph/kernel.brat.graph | 22 ++-- brat/test/golden/graph/list.brat.graph | 2 +- brat/test/golden/graph/num.brat.graph | 4 +- brat/test/golden/graph/pair.brat.graph | 2 +- brat/test/golden/graph/rx.brat.graph | 8 +- brat/test/golden/graph/swap.brat.graph | 2 +- brat/test/golden/graph/two.brat.graph | 2 +- brat/test/golden/graph/vec.brat.graph | 2 +- .../kernel/kernel_application.brat.golden | 2 +- 36 files changed, 198 insertions(+), 256 deletions(-) diff --git a/brat/Brat/Checker.hs b/brat/Brat/Checker.hs index 2c7508e1..7c9ccd58 100644 --- a/brat/Brat/Checker.hs +++ b/brat/Brat/Checker.hs @@ -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)]) @@ -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 []) diff --git a/brat/Brat/Checker/Helpers.hs b/brat/Brat/Checker/Helpers.hs index 618fc4f6..636a8e33 100644 --- a/brat/Brat/Checker/Helpers.hs +++ b/brat/Brat/Checker/Helpers.hs @@ -109,13 +109,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 @@ -133,10 +127,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 = "" @@ -150,14 +141,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 aux where aux (p, ty) = Named p ty + 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 diff --git a/brat/Brat/Elaborator.hs b/brat/Brat/Elaborator.hs index 2546dca3..77203308 100644 --- a/brat/Brat/Elaborator.hs +++ b/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) <$> traverse elabSigElem ts pure $ SomeRaw' (a ::::: ts) elaborate' (FInto a b) = elaborate' (FApp b a) elaborate' (FOf n e) = do @@ -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 @@ -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 diff --git a/brat/Brat/Parser.hs b/brat/Brat/Parser.hs index 84b34aae..43c52491 100644 --- a/brat/Brat/Parser.hs +++ b/brat/Brat/Parser.hs @@ -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 ((**^)) @@ -259,40 +257,37 @@ typekind = try (fmap (const Nat) <$> matchFC Hash) <|> kindHelper Lexer.Dollar S 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' @@ -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 @@ -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) @@ -515,7 +510,7 @@ expr' p = choice $ (try . getParser <$> enumFrom p) ++ [atomExpr] 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 @@ -594,27 +589,14 @@ expr' p = choice $ (try . getParser <$> enumFrom p) ++ [atomExpr] 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 @@ -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) @@ -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 @@ -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 diff --git a/brat/Brat/Syntax/Common.hs b/brat/Brat/Syntax/Common.hs index f393755d..aaf843f7 100644 --- a/brat/Brat/Syntax/Common.hs +++ b/brat/Brat/Syntax/Common.hs @@ -38,7 +38,8 @@ module Brat.Syntax.Common (PortName, ArithOp(..), pattern Dollar, pattern Star, - Precedence(..) + Precedence(..), + TypeAliasF(..) ) where import Brat.FC @@ -46,7 +47,6 @@ import Brat.QualName import Brat.Syntax.Abstractor import Brat.Syntax.Port -import Data.Bifunctor (first) import Data.List (intercalate) import Data.Kind (Type) import Data.Type.Equality (TestEquality(..), (:~:)(..)) @@ -200,14 +200,18 @@ instance Show Import where showSelection (ImportPartial fns) = "(":(unWC <$> fns) ++ [")"] showSelection (ImportHiding fns) = "hiding (":(unWC <$> fns) ++ [")"] -showSig :: Show ty => [(String, ty)] -> String +showSig :: (Show ty) => [TypeRowElem ty] -> String showSig [] = "()" -showSig (x:xs) - = intercalate ", " [ '(':p ++ " :: " ++ show ty ++ ")" - | (p, ty) <- x:xs] +showSig (hd:tl) = parens $ concat (tail (showElem hd) ++ [unwords (showElem x) | x <- tl]) + where + parens x = '(':x ++ ")" + + showElem (Anon ty) = [",", show ty] + showElem (Named p ty) = [",", '(':p ++ " :: " ++ show ty ++ ")"] showRow :: Show ty => [(NamedPort e, ty)] -> String -showRow = showSig . fmap (first portName) +showRow = parens . intercalate ", " . fmap (\(np, ty) -> unwords [portName np, "::", show ty]) + where parens x = '(':x ++ ")" data ArithOp = Add | Sub | Mul | Div | Pow deriving (Eq, Show) @@ -228,3 +232,5 @@ data Precedence | PAnn | PApp deriving (Bounded, Enum, Eq, Ord, Show) + +data TypeAliasF tm = TypeAlias FC QualName [(PortName,TypeKind)] tm deriving Show diff --git a/brat/Brat/Syntax/Concrete.hs b/brat/Brat/Syntax/Concrete.hs index 10bcb2e0..3b306bfc 100644 --- a/brat/Brat/Syntax/Concrete.hs +++ b/brat/Brat/Syntax/Concrete.hs @@ -6,19 +6,21 @@ import Brat.FC import Brat.QualName import Brat.Syntax.Common import Brat.Syntax.FuncDecl (FuncDecl(..)) -import Brat.Syntax.Raw import Brat.Syntax.Simple +type FAlias = TypeAliasF Flat +type FEnv = ([FDecl], [FAlias]) + +type FlatIO = TypeRowElem (WC (KindOr Flat)) + data FBody = FClauses (NonEmpty (WC Abstractor, WC Flat)) | FNoLhs (WC Flat) | FUndefined deriving Show -type FDecl = FuncDecl [RawIO] FBody +type FDecl = FuncDecl [FlatIO] FBody deriving instance Show FDecl -type FEnv = ([FDecl], [RawAlias]) - data Flat = FVar QualName @@ -32,7 +34,7 @@ data Flat | FInto (WC Flat) (WC Flat) | FArith ArithOp (WC Flat) (WC Flat) | FLambda (NonEmpty (WC Abstractor, WC Flat)) - | FAnnotation (WC Flat) [RawIO] + | FAnnotation (WC Flat) [FlatIO] | FLetIn (WC Abstractor) (WC Flat) (WC Flat) | FSimple SimpleTerm | FHole String @@ -40,8 +42,8 @@ data Flat | FEmpty | FPull [PortName] (WC Flat) -- We can get away with not elaborating type signatures in the short term - | FFn RawCType - | FKernel RawKType + | FFn (CType' FlatIO) + | FKernel (CType' (TypeRowElem (WC Flat))) | FUnderscore | FPass | FFanOut diff --git a/brat/Brat/Syntax/Core.hs b/brat/Brat/Syntax/Core.hs index 286b2f0f..2d414a13 100644 --- a/brat/Brat/Syntax/Core.hs +++ b/brat/Brat/Syntax/Core.hs @@ -3,7 +3,6 @@ module Brat.Syntax.Core (Term(..) ,Output ,InOut ,CType - ,CoreFuncDecl ,Precedence(..) ,precedence ) where @@ -17,7 +16,6 @@ import Brat.FC import Brat.Naming import Brat.QualName import Brat.Syntax.Common -import Brat.Syntax.FuncDecl import Brat.Syntax.Simple import Data.Kind (Type) @@ -29,8 +27,6 @@ type InOut = (PortName, KindOr (Term Chk Noun)) type CType = CType' InOut -type CoreFuncDecl = FuncDecl [InOut] (FunBody Term Noun) - data Term :: Dir -> Kind -> Type where Simple :: SimpleTerm -> Term Chk Noun Let :: WC Abstractor -> WC (Term Syn Noun) -> WC (Term d k) -> Term d k @@ -54,7 +50,7 @@ data Term :: Dir -> Kind -> Type where Of :: WC (Term Chk Noun) -> WC (Term d Noun) -> Term d Noun -- 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 -- Composition: values fed from source (first) into dest (second), -- of number/type determined by the source (:-:) :: WC (Term Syn k) -> WC (Term d UVerb) -> Term d k @@ -67,9 +63,9 @@ data Term :: Dir -> Kind -> Type where -- Type constructors Con :: QualName -> WC (Term Chk Noun) -> Term Chk Noun -- Brat function types - C :: CType' (PortName, KindOr (Term Chk Noun)) -> Term Chk Noun + C :: CType' (TypeRowElem (KindOr (Term Chk Noun))) -> Term Chk Noun -- Kernel types - K :: CType' (PortName, Term Chk Noun) -> Term Chk Noun + K :: CType' (TypeRowElem (Term Chk Noun)) -> Term Chk Noun FanOut :: Term Syn UVerb FanIn :: Term Chk UVerb diff --git a/brat/Brat/Syntax/Raw.hs b/brat/Brat/Syntax/Raw.hs index 956cc55f..4c48db2b 100644 --- a/brat/Brat/Syntax/Raw.hs +++ b/brat/Brat/Syntax/Raw.hs @@ -6,9 +6,7 @@ import Control.Monad (unless, when) import Control.Monad.Except import Control.Monad.Reader import Control.Monad.State -import Data.Bifunctor import Data.Kind (Type) -import Data.List.NonEmpty (fromList, NonEmpty(..)) import Data.Map (disjoint, member, union) import qualified Data.Map as M import Data.Tuple.HT (thd3) @@ -23,7 +21,7 @@ import Brat.Syntax.Common import Brat.Syntax.Core import Brat.Syntax.FuncDecl (FunBody(..), FuncDecl(..)) import Brat.Syntax.Simple -import Util (names, (**^)) +import Util ((**^)) type family TypeOf (k :: Kind) :: Type where TypeOf Noun = [InOut] @@ -31,29 +29,22 @@ type family TypeOf (k :: Kind) :: Type where type RawVType = Raw Chk Noun +-- Raw stuff that's also used in Brat.Syntax.Concrete type RawIO = TypeRowElem (KindOr RawVType) type RawCType = CType' RawIO type RawKType = CType' (TypeRowElem RawVType) -data TypeAliasF tm = TypeAlias FC QualName [(PortName,TypeKind)] tm deriving Show -type RawAlias = TypeAliasF (Raw Chk Noun) type TypeAlias = TypeAliasF (Term Chk Noun) type TypeAliasTable = M.Map QualName TypeAlias +type RawAlias = TypeAliasF (Raw Chk Noun) + + type RawEnv = ([RawFuncDecl], [RawAlias], TypeAliasTable) type RawFuncDecl = FuncDecl [RawIO] (FunBody Raw Noun) - -addNames :: TypeRow ty -> [(PortName, ty)] -addNames tms = aux (fromList names) tms - where - -- aux is passed the infinite list `names`, so we can use the partial function - -- `fromList` to repeatedly convert it to NonEmpty so GHC doesn't complain - -- about the missing case `aux [] _` - aux (n :| ns) ((Anon tm):tms) = (n, tm) : aux (fromList ns) tms - aux ns ((Named n tm):tms) = (n, tm) : aux ns tms - aux _ [] = [] +type CoreFuncDecl = FuncDecl (TypeRow (KindOr (Term Chk Noun))) (FunBody Term Noun) data Raw :: Dir -> Kind -> Type where RSimple :: SimpleTerm -> Raw Chk Noun @@ -134,7 +125,6 @@ instance Show (Raw d k) where type Desugar = StateT Namespace (ReaderT (RawEnv, Bwd QualName) (Except Error)) --- instance {-# OVERLAPPING #-} MonadFail Desugar where instance {-# OVERLAPPING #-} MonadFail Desugar where fail = throwError . desugarErr @@ -164,23 +154,6 @@ isAlias name = do pure $ M.member name aliases -{- -findDuplicates :: Env -> Desugar () -findDuplicates (ndecls, vdecls, aliases) - = aux $ concat [(fst &&& show . fst . snd) <$> (unWC <$> ndecls) - ,(fst &&& show . fst . snd) <$> (unWC <$> vdecls) - ,(fst &&& show . snd) <$> aliases] - where - aux :: [(String, String)] -> Desugar () - aux xs = case filter ((1<).length) [ filter ((==x).fst) xs | (x,_) <- xs ] of - [] -> pure () -- all good - ([]:_) -> undefined -- this should be unreachable - -- TODO: Include FC - ((x:xs):_) -> desugarErr . unlines $ (("Multiple definitions of " ++ fst x) - :(snd <$> (x:xs)) - ) --} - desugarErr :: String -> Error desugarErr = dumbErr . DesugarErr @@ -194,10 +167,16 @@ class Desugarable ty where desugar' :: ty -> Desugar (Desugared ty) -instance Desugarable ty => Desugarable (TypeRow ty) where - type Desugared (TypeRow ty) = TypeRow (Desugared ty) - desugar' = traverse (traverse desugar') +instance Desugarable ty => Desugarable (TypeRowElem ty) where + type Desugared (TypeRowElem ty) = TypeRowElem (Desugared ty) + desugar' (Anon ty) = Anon <$> desugar' ty + desugar' (Named x ty) = Named x <$> desugar' ty + +instance Desugarable (TypeRowElem ty) => Desugarable [TypeRowElem ty] where + type Desugared [TypeRowElem ty] = [Desugared (TypeRowElem ty)] + desugar' = traverse desugar' +-- Desugaring terms instance (Kindable k) => Desugarable (Raw d k) where type Desugared (Raw d k) = Term d k -- TODO: holes need to know their arity for type checking @@ -239,7 +218,7 @@ instance (Kindable k) => Desugarable (Raw d k) where desugar' (fun ::$:: arg) = (:$:) <$> desugar fun <*> desugar arg desugar' (tm ::::: outputs) = do tm <- desugar tm - (tys, ()) <- desugarBind outputs $ pure () + tys <- traverse desugar' outputs pure (tm ::: tys) desugar' (syn ::-:: verb) = (:-:) <$> desugar syn <*> desugar verb desugar' (RLambda c cs) = Lambda <$> (id **^ desugar) c <*> traverse (id **^ desugar) cs @@ -251,15 +230,12 @@ instance (Kindable k) => Desugarable (Raw d k) where desugar' RFanIn = pure FanIn desugar' (ROf n e) = Of <$> desugar n <*> desugar e -instance Desugarable ty => Desugarable (PortName, ty) where - type Desugared (PortName, ty) = (PortName, Desugared ty) - desugar' (p, ty) = (p,) <$> desugar' ty - instance Desugarable (CType' (TypeRowElem RawVType)) where - type Desugared (CType' (TypeRowElem RawVType)) = CType' (PortName, Term Chk Noun) + type Desugared (CType' (TypeRowElem RawVType)) = CType' (TypeRowElem (Term Chk Noun)) + desugar' :: CType' (TypeRowElem RawVType) -> Desugar (CType' (TypeRowElem (Term Chk Noun))) desugar' (ss :-> ts) = do - ss <- traverse desugar' (addNames ss) - ts <- traverse desugar' (addNames ts) + ss <- traverse desugar' ss + ts <- traverse desugar' ts pure (ss :-> ts) isConOrAlias :: QualName -> Desugar Bool @@ -283,27 +259,9 @@ instance Desugarable ty => Desugarable (KindOr ty) where desugar' (Left k) = pure (Left k) desugar' (Right ty) = Right <$> desugar' ty -desugarBind :: forall t. [RawIO] - -> Desugar t - -> Desugar ([(PortName, KindOr (Term Chk Noun))], t) -desugarBind tys m = worker (addNames tys) - where - worker :: [(PortName, KindOr (Raw Chk Noun))] - -> Desugar ([(PortName, KindOr (Term Chk Noun))], t) - worker ((p, Left k):ns) = do - (ns, t) <- local (second (:< PrefixName [] p)) $ worker ns - pure ((p, Left k):ns, t) - worker ((p, Right ty):ns) = do - ty <- desugar' ty - (ns, t) <- worker ns - pure ((p, Right ty):ns, t) - worker [] = ([],) <$> m - -instance Desugarable (CType' RawIO) where - type Desugared (CType' RawIO) = CType' (PortName, KindOr (Term Chk Noun)) - desugar' (ss :-> ts) = do - (ss, (ts, ())) <- desugarBind ss $ desugarBind ts $ pure () - pure $ ss :-> ts +instance Desugarable (CType' RawIO) where + type Desugared (CType' RawIO) = CType' (TypeRowElem (KindOr (Term Chk Noun))) + desugar' (ss :-> ts) = (:->) <$> desugar' ss <*> desugar' ts instance Desugarable RawAlias where type Desugared RawAlias = TypeAlias @@ -326,7 +284,7 @@ desugarVBody Undefined = pure Undefined instance Desugarable RawFuncDecl where type Desugared RawFuncDecl = CoreFuncDecl desugar' d@FuncDecl{..} = do - tys <- addNames <$> desugar' fnSig + tys <- desugar' fnSig noun <- desugarNBody fnBody pure $ d { fnBody = noun , fnSig = tys diff --git a/brat/Brat/Unelaborator.hs b/brat/Brat/Unelaborator.hs index b06509f0..3578e20c 100644 --- a/brat/Brat/Unelaborator.hs +++ b/brat/Brat/Unelaborator.hs @@ -1,12 +1,11 @@ module Brat.Unelaborator (unelab) where -import Brat.FC (unWC) +import Brat.FC (WC(..), dummyFC, unWC) import Brat.Syntax.Concrete (Flat(..)) import Brat.Syntax.Common (Dir(..), Kind(..), Diry(..), Kindy(..) - ,KindOr, PortName, TypeRowElem(Named), CType'(..) + ,KindOr, TypeRowElem(..), CType'(..) ) import Brat.Syntax.Core (Term(..)) -import Brat.Syntax.Raw (Raw(..), RawVType) import Data.Bifunctor (second) import Data.List.NonEmpty (NonEmpty(..)) @@ -28,49 +27,28 @@ unelab _ ky (Pull ps tm) = FPull ps (unelab Chky ky <$> tm) unelab _ _ (Var v) = FVar v unelab dy ky (Arith op lhs rhs) = FArith op (unelab dy ky <$> lhs) (unelab dy ky <$> rhs) unelab dy _ (Of n e) = FOf (unelab Chky Nouny <$> n) (unelab dy Nouny <$> e) -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))] + f = fmap (fmap (dummyFC . fmap (unelab Chky Nouny))) unelab dy ky (top :-: bot) = case ky of Nouny -> FInto (unelab Syny Nouny <$> top) (unelab dy UVerby <$> bot) _ -> FApp (unelab Syny ky <$> top) (unelab dy UVerby <$> bot) unelab dy ky (f :$: s) = FApp (unelab dy KVerby <$> f) (unelab Chky ky <$> s) unelab dy _ (Lambda (abs,rhs) cs) = FLambda ((abs, unelab dy Nouny <$> rhs) :| (second (fmap (unelab Chky Nouny)) <$> cs)) unelab _ _ (Con c args) = FCon c (unelab Chky Nouny <$> args) -unelab _ _ (C (ss :-> ts)) = FFn (toRawRo ss :-> toRawRo ts) -unelab _ _ (K cty) = FKernel $ fmap (\(p, ty) -> Named p (toRaw ty)) cty +unelab _ _ (C (ss :-> ts)) = FFn ((unelabRo ss) + :-> + (unelabRo ts) + ) +unelab _ _ (K (ss :-> ts)) = FKernel (unelabKernRo ss :-> unelabKernRo ts) unelab _ _ Identity = FIdentity unelab _ _ (Hope ident) = FHope ident unelab _ _ FanIn = FFanIn unelab _ _ FanOut = FFanOut --- This is needed for concrete terms which embed a type as a list of `Raw` things -toRaw :: Term d k -> Raw d k -toRaw (Simple tm) = RSimple tm -toRaw (Let abs thing body) = RLet abs (toRaw <$> thing) (toRaw <$> body) -toRaw (NHole name) = RNHole (show name) -toRaw (VHole name) = RVHole (show name) -toRaw Empty = REmpty -toRaw (a :|: b) = (toRaw <$> a) ::|:: (toRaw <$> b) -toRaw Pass = RPass -toRaw (Th th) = RTh $ toRaw <$> th -toRaw (TypedTh th) = RTypedTh $ toRaw <$> th -toRaw (Force tm) = RForce $ toRaw <$> tm -toRaw (Emb tm) = REmb $ toRaw <$> tm -toRaw (Forget tm) = RForget $ toRaw <$> tm -toRaw (Pull ps tm) = RPull ps $ toRaw <$> tm -toRaw (Var v) = RVar v -toRaw (Arith op lhs rhs) = RArith op (toRaw <$> lhs) (toRaw <$> rhs) -toRaw (Of n e) = ROf (toRaw <$> n) (toRaw <$> e) -toRaw (tm ::: outs) = (toRaw <$> tm) ::::: toRawRo outs -toRaw (top :-: bot) = (toRaw <$> top) ::-:: (toRaw <$> bot) -toRaw (f :$: s) = (toRaw <$> f) ::$:: (toRaw <$> s) -toRaw (Lambda (abs,rhs) cs) = RLambda (abs, toRaw <$> rhs) (second (fmap toRaw) <$> cs) -toRaw (Con c args) = RCon c (toRaw <$> args) -toRaw (C (ss :-> ts)) = RFn (toRawRo ss :-> toRawRo ts) -toRaw (K cty) = RKernel $ (\(p, ty) -> Named p (toRaw ty)) <$> cty -toRaw Identity = RIdentity -toRaw (Hope ident) = RHope ident -toRaw FanIn = RFanIn -toRaw FanOut = RFanOut +unelabKernRo :: [TypeRowElem (Term Chk Noun)] -> [TypeRowElem (WC Flat)] +unelabKernRo = fmap (fmap (dummyFC . unelab Chky Nouny)) -toRawRo :: [(PortName, KindOr (Term Chk Noun))] -> [TypeRowElem (KindOr RawVType)] -toRawRo = fmap (\(p, bty) -> Named p (second toRaw bty)) +unelabRo :: [(TypeRowElem (KindOr (Term Chk Noun)))] -> [TypeRowElem (WC (KindOr Flat))] +unelabRo = fmap (fmap (dummyFC . fmap (unelab Chky Nouny))) diff --git a/brat/test/Test/Syntax/Let.hs b/brat/test/Test/Syntax/Let.hs index bd748872..71dcd966 100644 --- a/brat/test/Test/Syntax/Let.hs +++ b/brat/test/Test/Syntax/Let.hs @@ -28,8 +28,8 @@ test = testCase "let" $ tm = Let (dummyFC ("x" :||: "y")) (dummyFC (dummyFC (num 1 :|: num 2) - ::: [("a", Right (Con (plain "Int") (dummyFC Empty))) - ,("b", Right (Con (plain "Int") (dummyFC Empty))) + ::: [Named "a" (Right (Con (plain "Int") (dummyFC Empty))) + ,Named "b" (Right (Con (plain "Int") (dummyFC Empty))) ]) ) (dummyFC (Var "x")) diff --git a/brat/test/golden/binding/let.brat.golden b/brat/test/golden/binding/let.brat.golden index 95c5c1c9..86ac42af 100644 --- a/brat/test/golden/binding/let.brat.golden +++ b/brat/test/golden/binding/let.brat.golden @@ -3,5 +3,5 @@ badBinding = let x = twoThings in x ^^^^^^^^^^^^^^^^^^^^^^ Internal error: Expected empty unders after abstract, got: - (b1 :: Int) + (_1 :: Int) diff --git a/brat/test/golden/error/apply_two_thunks.brat.golden b/brat/test/golden/error/apply_two_thunks.brat.golden index a91ab7f1..ec1da67f 100644 --- a/brat/test/golden/error/apply_two_thunks.brat.golden +++ b/brat/test/golden/error/apply_two_thunks.brat.golden @@ -3,5 +3,5 @@ go(n) = thunks(n) ^^^^^^^^^ Type error: Expected function thunks() to consume all of its arguments (「n」) - but found leftovers: (a1 :: Int) + but found leftovers: (_0 :: Int) diff --git a/brat/test/golden/error/empty_into.brat.golden b/brat/test/golden/error/empty_into.brat.golden index 9f669992..fe635cc5 100644 --- a/brat/test/golden/error/empty_into.brat.golden +++ b/brat/test/golden/error/empty_into.brat.golden @@ -3,7 +3,7 @@ intoErr = |> makeInt ^^^^^^^^^^ Type mismatch when checking makeInt()(()) -Expected: (a1 :: Bool) -But got: (a1 :: Int) +Expected: (_0 :: Bool) +But got: (_0 :: Int) diff --git a/brat/test/golden/error/fanout-diff-types.brat.golden b/brat/test/golden/error/fanout-diff-types.brat.golden index abde4a2f..82430baa 100644 --- a/brat/test/golden/error/fanout-diff-types.brat.golden +++ b/brat/test/golden/error/fanout-diff-types.brat.golden @@ -3,7 +3,7 @@ f = { [/\] } ^^^^ Type mismatch when checking [/\] -Expected: (b1 :: Bit) +Expected: (_1 :: Bit) But got: (head :: Qubit) diff --git a/brat/test/golden/error/fanout-not-enough-overs.brat.golden b/brat/test/golden/error/fanout-not-enough-overs.brat.golden index a1ac9d3c..7cb723fb 100644 --- a/brat/test/golden/error/fanout-not-enough-overs.brat.golden +++ b/brat/test/golden/error/fanout-not-enough-overs.brat.golden @@ -2,5 +2,5 @@ Error in test/golden/error/fanout-not-enough-overs.brat on line 2: f = { [/\] } ^^^^^^^^ - Expected function to return additional values of type: (c1 :: Nat) + Expected function to return additional values of type: (_3 :: Nat) diff --git a/brat/test/golden/error/pair.brat.golden b/brat/test/golden/error/pair.brat.golden index 51074f8a..33fd6b91 100644 --- a/brat/test/golden/error/pair.brat.golden +++ b/brat/test/golden/error/pair.brat.golden @@ -3,7 +3,7 @@ pair = row -- Distinct from a pair ^^^ Type mismatch when checking row -Expected: (a1 :: [Int,Bool]) -But got: (a1 :: Int), (b1 :: Bool) +Expected: (_0 :: [Int,Bool]) +But got: (_0 :: Int, _1 :: Bool) diff --git a/brat/test/golden/error/portpull-ambiguous.brat.golden b/brat/test/golden/error/portpull-ambiguous.brat.golden index bc45791d..f9d0e292 100644 --- a/brat/test/golden/error/portpull-ambiguous.brat.golden +++ b/brat/test/golden/error/portpull-ambiguous.brat.golden @@ -2,5 +2,5 @@ Error in test/golden/error/portpull-ambiguous.brat on line 6: id2 = x, y => (id,id)(a1:x, y) ^^^^^^^^^ - Port a1 is ambiguous in (a1 :: Nat), (a1 :: Nat) + Port not found: a1 in (_0 :: Nat, _0 :: Nat) diff --git a/brat/test/golden/error/portpull.brat.golden b/brat/test/golden/error/portpull.brat.golden index f6a2fd2a..7d0e7bc0 100644 --- a/brat/test/golden/error/portpull.brat.golden +++ b/brat/test/golden/error/portpull.brat.golden @@ -2,5 +2,5 @@ Error in test/golden/error/portpull.brat on line 6: id2 = x,y => (id, id)(a1:x, y) ^^^^^^^^^ - Port a1 is ambiguous in (a1 :: Nat), (a1 :: Nat) + Port not found: a1 in (_0 :: Nat, _0 :: Nat) diff --git a/brat/test/golden/error/remaining_holes.brat.golden b/brat/test/golden/error/remaining_holes.brat.golden index 73ae06cc..829d801b 100644 --- a/brat/test/golden/error/remaining_holes.brat.golden +++ b/brat/test/golden/error/remaining_holes.brat.golden @@ -1,4 +1,4 @@ Can't compile file with remaining holes - ?a_hole :: (a1 :: Bit) - ?b_hole :: (thunk :: { (a1 :: Int) -> (a1 :: List(Int)) }) + ?a_hole :: (_0 :: Bit) + ?b_hole :: (thunk :: { (_0 :: Int) -> (_1 :: List(Int)) }) diff --git a/brat/test/golden/error/toplevel-leftovers.brat.golden b/brat/test/golden/error/toplevel-leftovers.brat.golden index 797eac59..222e5cb4 100644 --- a/brat/test/golden/error/toplevel-leftovers.brat.golden +++ b/brat/test/golden/error/toplevel-leftovers.brat.golden @@ -3,7 +3,7 @@ f = 42 ^^ Type mismatch when checking f -Expected: (a1 :: Nat), (b1 :: Bool) -But got: (a1 :: Nat) +Expected: (_0 :: Nat, _1 :: Bool) +But got: (_0 :: Nat) diff --git a/brat/test/golden/error/toplevel-leftovers2.brat.golden b/brat/test/golden/error/toplevel-leftovers2.brat.golden index 7951cf7e..47ac772b 100644 --- a/brat/test/golden/error/toplevel-leftovers2.brat.golden +++ b/brat/test/golden/error/toplevel-leftovers2.brat.golden @@ -4,7 +4,7 @@ f(x) = x Type mismatch when checking x => 「x」 -Expected: (a1 :: Nat), (b1 :: Bool) -But got: (a1 :: Nat) +Expected: (_1 :: Nat, _2 :: Bool) +But got: (_1 :: Nat) diff --git a/brat/test/golden/error/toplevel-leftovers3.brat.golden b/brat/test/golden/error/toplevel-leftovers3.brat.golden index 84290ebb..b661fdff 100644 --- a/brat/test/golden/error/toplevel-leftovers3.brat.golden +++ b/brat/test/golden/error/toplevel-leftovers3.brat.golden @@ -2,5 +2,5 @@ Error in test/golden/error/toplevel-leftovers3.brat on line 2: f(x) = x ^ - Type error: Inputs (b1 :: Bool) weren't used + Type error: Inputs (_1 :: Bool) weren't used diff --git a/brat/test/golden/error/vectorise-type-mismatch.brat.golden b/brat/test/golden/error/vectorise-type-mismatch.brat.golden index 85d0a773..22634fd0 100644 --- a/brat/test/golden/error/vectorise-type-mismatch.brat.golden +++ b/brat/test/golden/error/vectorise-type-mismatch.brat.golden @@ -3,6 +3,6 @@ panic = 2 of 42 ^^^^^^^ Type error: Got: Vector of length 2 -Expected: (a1 :: Vec(Nat, 1)) +Expected: (_0 :: Vec(Nat, 1)) diff --git a/brat/test/golden/error/vectorise3.brat.golden b/brat/test/golden/error/vectorise3.brat.golden index b21f57b1..1e44756c 100644 --- a/brat/test/golden/error/vectorise3.brat.golden +++ b/brat/test/golden/error/vectorise3.brat.golden @@ -3,5 +3,5 @@ f(_, _, n, f, xs) = (n of f)(xs) ^^^^^^^^^^^^ Type error: Expected function 「n」 of f() to consume all of its arguments (「xs」) - but found leftovers: (b1 :: Vec(VApp VPar Ex checking_vectorise3_check_defs_1_f_$lhs_3_lambda_fake_source 0 B0, VPar Ex checking_vectorise3_check_defs_1_f_$lhs_3_lambda_fake_source 2)) + but found leftovers: (_1 :: Vec(VApp VPar Ex checking_vectorise3_check_defs_1_f_$lhs_3_lambda_fake_source 0 B0, VPar Ex checking_vectorise3_check_defs_1_f_$lhs_3_lambda_fake_source 2)) diff --git a/brat/test/golden/graph/addN2.brat.graph b/brat/test/golden/graph/addN2.brat.graph index 7dfa6937..fb55e830 100644 --- a/brat/test/golden/graph/addN2.brat.graph +++ b/brat/test/golden/graph/addN2.brat.graph @@ -18,7 +18,7 @@ Nodes: (addN2.brat_globals_Int_12,BratNode (Constructor Int) [] [("value",[])]) (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) })]) Wires: (Ex addN2.brat_check_defs_1_addN_LambdaChk_9_checkClauses_1_$rhs_4_Eval 0,Int,In addN2.brat_check_defs_1_addN_LambdaChk_9_checkClauses_1_lambda.0_rhs/out_2 0) diff --git a/brat/test/golden/graph/cons.brat.graph b/brat/test/golden/graph/cons.brat.graph index 7dc26783..fe6f49bc 100644 --- a/brat/test/golden/graph/cons.brat.graph +++ b/brat/test/golden/graph/cons.brat.graph @@ -30,8 +30,8 @@ Nodes: (cons.brat_globals_Vec_6,BratNode (Constructor Vec) [("X",[]),("n",Nat)] [("value",[])]) (cons.brat_globals_const_3,BratNode (Const 2) [] [("value",Nat)]) (cons.brat_globals_const_8,BratNode (Const 3) [] [("value",Nat)]) -(cons.brat_globals_decl_4_two,BratNode Id [("a1",Vec(Int, 2))] [("a1",Vec(Int, 2))]) -(cons.brat_globals_decl_9_three,BratNode Id [("a1",Vec(Int, 3))] [("a1",Vec(Int, 3))]) +(cons.brat_globals_decl_4_two,BratNode Id [("_0",Vec(Int, 2))] [("_0",Vec(Int, 2))]) +(cons.brat_globals_decl_9_three,BratNode Id [("_0",Vec(Int, 3))] [("_0",Vec(Int, 3))]) Wires: (Ex cons.brat_check_defs_1_three_2_$rhs_check'Con__2 0,[],In cons.brat_check_defs_1_three_2_$rhs_check'Con_$!_pat2val 0) diff --git a/brat/test/golden/graph/id.brat.graph b/brat/test/golden/graph/id.brat.graph index 7d16ffe1..e6a6e03d 100644 --- a/brat/test/golden/graph/id.brat.graph +++ b/brat/test/golden/graph/id.brat.graph @@ -11,7 +11,7 @@ Nodes: (id.brat_check_defs_1_main_$rhs_check'Th_thunk_thunk_2,BratNode (Box id.brat_check_defs_1_main_$rhs_check'Th_thunk/in id.brat_check_defs_1_main_$rhs_check'Th_thunk/out_1) [] [("thunk",{ (a :: Qubit) -o (b :: Qubit) })]) (id.brat_globals_Qubit_2,BratNode (Constructor Qubit) [] [("value",[])]) (id.brat_globals_Qubit_4,BratNode (Constructor Qubit) [] [("value",[])]) -(id.brat_globals_decl_5_main,BratNode Id [("a1",{ (a :: Qubit) -o (b :: Qubit) })] [("a1",{ (a :: Qubit) -o (b :: Qubit) })]) +(id.brat_globals_decl_5_main,BratNode Id [("_0",{ (a :: Qubit) -o (b :: Qubit) })] [("_0",{ (a :: Qubit) -o (b :: Qubit) })]) Wires: (Ex id.brat_check_defs_1_main_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/in_1 0,Qubit,In id.brat_check_defs_1_main_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/out_2 0) diff --git a/brat/test/golden/graph/kernel.brat.graph b/brat/test/golden/graph/kernel.brat.graph index 130eb5b5..f5bcae9a 100644 --- a/brat/test/golden/graph/kernel.brat.graph +++ b/brat/test/golden/graph/kernel.brat.graph @@ -1,7 +1,7 @@ Nodes: -(kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in,KernelNode Source [] [("a1",Qubit),("b1",Qubit),("c1",Qubit)]) -(kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/out_1,KernelNode Target [("a1",Vec(Qubit, 3))] []) -(kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup_thunk_2,BratNode (Box kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/out_1) [] [("thunk",{ (a1 :: Qubit), (b1 :: Qubit), (c1 :: Qubit) -o (a1 :: Vec(Qubit, 3)) })]) +(kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in,KernelNode Source [] [("_0",Qubit),("_1",Qubit),("_2",Qubit)]) +(kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/out_1,KernelNode Target [("_0",Vec(Qubit, 3))] []) +(kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup_thunk_2,BratNode (Box kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/out_1) [] [("thunk",{ (_0 :: Qubit), (_1 :: Qubit), (_2 :: Qubit) -o (_0 :: Vec(Qubit, 3)) })]) (kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con__2,BratNode (Dummy $) [] [("dummy",[])]) (kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_$!_numpat2val_1,BratNode Id [("",Nat)] [("",Nat)]) (kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_$!_pat2val,BratNode Id [("",[])] [("",[])]) @@ -25,19 +25,19 @@ Nodes: (kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_typeEqsTail_1_$!_1_buildConst,BratNode (Const 2) [] [("value",Nat)]) (kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_typeEqsTail_1_$!_1_buildConst_2,BratNode (Const 0) [] [("value",Nat)]) (kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/in_1,KernelNode Source [] [("q0",Qubit),("q1",Qubit),("q2",Qubit)]) -(kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/out_2,KernelNode Target [("a1",Vec(Qubit, 3))] []) -(kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs_thunk_3,BratNode (Box kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/in_1 kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/out_2) [] [("thunk",{ (q0 :: Qubit), (q1 :: Qubit), (q2 :: Qubit) -o (a1 :: Vec(Qubit, 3)) })]) -(kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_lambda,KernelNode (PatternMatch ((TestMatchData Kerny (MatchSequence {matchInputs = [(NamedPort {end = Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in 0, portName = "a1"},Qubit),(NamedPort {end = Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in 1, portName = "b1"},Qubit),(NamedPort {end = Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in 2, portName = "c1"},Qubit)], matchTests = [], matchOutputs = [(NamedPort {end = Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in 0, portName = "a1"},Qubit),(NamedPort {end = Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in 1, portName = "b1"},Qubit),(NamedPort {end = Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in 2, portName = "c1"},Qubit)]}),kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs_thunk_3) :| [])) [("a1",Qubit),("b1",Qubit),("c1",Qubit)] [("a1",Vec(Qubit, 3))]) -(kernel.brat_check_defs_1_id3_$rhs_check'Th_thunk/in,KernelNode Source [] [("a1",Qubit),("b1",Qubit),("c1",Qubit)]) -(kernel.brat_check_defs_1_id3_$rhs_check'Th_thunk/out_1,KernelNode Target [("a1",Vec(Qubit, 3))] []) -(kernel.brat_check_defs_1_id3_$rhs_check'Th_thunk_thunk_2,BratNode (Box kernel.brat_check_defs_1_id3_$rhs_check'Th_thunk/in kernel.brat_check_defs_1_id3_$rhs_check'Th_thunk/out_1) [] [("thunk",{ (a1 :: Qubit), (b1 :: Qubit), (c1 :: Qubit) -o (a1 :: Vec(Qubit, 3)) })]) +(kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/out_2,KernelNode Target [("_0",Vec(Qubit, 3))] []) +(kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs_thunk_3,BratNode (Box kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/in_1 kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/out_2) [] [("thunk",{ (q0 :: Qubit), (q1 :: Qubit), (q2 :: Qubit) -o (_0 :: Vec(Qubit, 3)) })]) +(kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_lambda,KernelNode (PatternMatch ((TestMatchData Kerny (MatchSequence {matchInputs = [(NamedPort {end = Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in 0, portName = "_0"},Qubit),(NamedPort {end = Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in 1, portName = "_1"},Qubit),(NamedPort {end = Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in 2, portName = "_2"},Qubit)], matchTests = [], matchOutputs = [(NamedPort {end = Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in 0, portName = "_0"},Qubit),(NamedPort {end = Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in 1, portName = "_1"},Qubit),(NamedPort {end = Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in 2, portName = "_2"},Qubit)]}),kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs_thunk_3) :| [])) [("_0",Qubit),("_1",Qubit),("_2",Qubit)] [("_0",Vec(Qubit, 3))]) +(kernel.brat_check_defs_1_id3_$rhs_check'Th_thunk/in,KernelNode Source [] [("_0",Qubit),("_1",Qubit),("_2",Qubit)]) +(kernel.brat_check_defs_1_id3_$rhs_check'Th_thunk/out_1,KernelNode Target [("_0",Vec(Qubit, 3))] []) +(kernel.brat_check_defs_1_id3_$rhs_check'Th_thunk_thunk_2,BratNode (Box kernel.brat_check_defs_1_id3_$rhs_check'Th_thunk/in kernel.brat_check_defs_1_id3_$rhs_check'Th_thunk/out_1) [] [("thunk",{ (_0 :: Qubit), (_1 :: Qubit), (_2 :: Qubit) -o (_0 :: Vec(Qubit, 3)) })]) (kernel.brat_globals_Qubit_2,BratNode (Constructor Qubit) [] [("value",[])]) (kernel.brat_globals_Qubit_3,BratNode (Constructor Qubit) [] [("value",[])]) (kernel.brat_globals_Qubit_4,BratNode (Constructor Qubit) [] [("value",[])]) (kernel.brat_globals_Qubit_7,BratNode (Constructor Qubit) [] [("value",[])]) (kernel.brat_globals_Vec_6,BratNode (Constructor Vec) [("X",[]),("n",Nat)] [("value",[])]) (kernel.brat_globals_const_8,BratNode (Const 3) [] [("value",Nat)]) -(kernel.brat_globals_decl_9_id3,BratNode Id [("a1",{ (a1 :: Qubit), (b1 :: Qubit), (c1 :: Qubit) -o (a1 :: Vec(Qubit, 3)) })] [("a1",{ (a1 :: Qubit), (b1 :: Qubit), (c1 :: Qubit) -o (a1 :: Vec(Qubit, 3)) })]) +(kernel.brat_globals_decl_9_id3,BratNode Id [("_0",{ (_0 :: Qubit), (_1 :: Qubit), (_2 :: Qubit) -o (_0 :: Vec(Qubit, 3)) })] [("_0",{ (_0 :: Qubit), (_1 :: Qubit), (_2 :: Qubit) -o (_0 :: Vec(Qubit, 3)) })]) Wires: (Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con__2 0,[],In kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_$!_pat2val 0) @@ -62,7 +62,7 @@ Wires: (Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_thunk/in 0,Qubit,In kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_lambda 0) (Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_thunk/in 1,Qubit,In kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_lambda 1) (Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_thunk/in 2,Qubit,In kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_lambda 2) -(Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_thunk_thunk_2 0,{ (a1 :: Qubit), (b1 :: Qubit), (c1 :: Qubit) -o (a1 :: Vec(Qubit, 3)) },In kernel.brat_globals_decl_9_id3 0) +(Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_thunk_thunk_2 0,{ (_0 :: Qubit), (_1 :: Qubit), (_2 :: Qubit) -o (_0 :: Vec(Qubit, 3)) },In kernel.brat_globals_decl_9_id3 0) (Ex kernel.brat_globals_Qubit_2 0,[],In kernel.brat_globals___kcr__1 0) (Ex kernel.brat_globals_Qubit_3 0,[],In kernel.brat_globals___kcr__1 1) (Ex kernel.brat_globals_Qubit_4 0,[],In kernel.brat_globals___kcr__1 2) diff --git a/brat/test/golden/graph/list.brat.graph b/brat/test/golden/graph/list.brat.graph index 5b7fb356..77e74475 100644 --- a/brat/test/golden/graph/list.brat.graph +++ b/brat/test/golden/graph/list.brat.graph @@ -16,7 +16,7 @@ Nodes: (list.brat_check_defs_1_xs_$rhs_check'Con_const_4,BratNode (Const 1) [] [("value",Int)]) (list.brat_globals_Int_2,BratNode (Constructor Int) [] [("value",[])]) (list.brat_globals_List_1,BratNode (Constructor List) [("listValue",[])] [("value",[])]) -(list.brat_globals_decl_3_xs,BratNode Id [("a1",List(Int))] [("a1",List(Int))]) +(list.brat_globals_decl_3_xs,BratNode Id [("_0",List(Int))] [("_0",List(Int))]) Wires: (Ex list.brat_check_defs_1_xs_$rhs_check'Con__2 0,[],In list.brat_check_defs_1_xs_$rhs_check'Con_$!_pat2val 0) diff --git a/brat/test/golden/graph/num.brat.graph b/brat/test/golden/graph/num.brat.graph index 099d7e13..5365a1e0 100644 --- a/brat/test/golden/graph/num.brat.graph +++ b/brat/test/golden/graph/num.brat.graph @@ -5,8 +5,8 @@ Nodes: (num.brat_check_defs_1_n_$rhs_check'Con_succ_1,BratNode (Constructor succ) [("value",Nat)] [("value",Nat)]) (num.brat_globals_Int_4,BratNode (Constructor Int) [] [("value",[])]) (num.brat_globals_Nat_1,BratNode (Constructor Nat) [] [("value",[])]) -(num.brat_globals_decl_2_n,BratNode Id [("a1",Nat)] [("a1",Nat)]) -(num.brat_globals_decl_5_m,BratNode Id [("a1",Int)] [("a1",Int)]) +(num.brat_globals_decl_2_n,BratNode Id [("_0",Nat)] [("_0",Nat)]) +(num.brat_globals_decl_5_m,BratNode Id [("_0",Int)] [("_0",Int)]) Wires: (Ex num.brat_check_defs_1_m_2_$rhs_check'Con_const_2 0,Int,In num.brat_check_defs_1_m_2_$rhs_check'Con_doub_1 0) diff --git a/brat/test/golden/graph/pair.brat.graph b/brat/test/golden/graph/pair.brat.graph index 7ac1db68..065f7796 100644 --- a/brat/test/golden/graph/pair.brat.graph +++ b/brat/test/golden/graph/pair.brat.graph @@ -16,7 +16,7 @@ Nodes: (pair.brat_globals_Int_2,BratNode (Constructor Int) [] [("value",[])]) (pair.brat_globals_cons_1,BratNode (Constructor cons) [("head",[]),("tail",[])] [("value",[])]) (pair.brat_globals_cons_3,BratNode (Constructor cons) [("head",[]),("tail",[])] [("value",[])]) -(pair.brat_globals_decl_6_xs,BratNode Id [("a1",[Int,Bool])] [("a1",[Int,Bool])]) +(pair.brat_globals_decl_6_xs,BratNode Id [("_0",[Int,Bool])] [("_0",[Int,Bool])]) (pair.brat_globals_nil_5,BratNode (Constructor nil) [] [("value",[])]) Wires: diff --git a/brat/test/golden/graph/rx.brat.graph b/brat/test/golden/graph/rx.brat.graph index f0767503..38869cc3 100644 --- a/brat/test/golden/graph/rx.brat.graph +++ b/brat/test/golden/graph/rx.brat.graph @@ -13,7 +13,7 @@ Nodes: (rx.brat_check_defs_1_nums_$rhs_const,BratNode (Const 1) [] [("value",Int)]) (rx.brat_check_defs_1_nums_$rhs_const_1,BratNode (Const 2) [] [("value",Int)]) (rx.brat_check_defs_1_nums_$rhs_const_2,BratNode (Const 3) [] [("value",Int)]) -(rx.brat_check_defs_1_xish_1_$rhs_Eval,BratNode (Eval (Ex rx.brat_globals_prim_7_Rx 0)) [("th",Float)] [("a1",{ (rxa :: Qubit) -o (rxb :: Qubit) })]) +(rx.brat_check_defs_1_xish_1_$rhs_Eval,BratNode (Eval (Ex rx.brat_globals_prim_7_Rx 0)) [("th",Float)] [("_1",{ (rxa :: Qubit) -o (rxb :: Qubit) })]) (rx.brat_check_defs_1_xish_1_$rhs_const_1,BratNode (Const 30.0) [] [("value",Float)]) (rx.brat_globals_Float_2,BratNode (Constructor Float) [] [("value",[])]) (rx.brat_globals_Int_9,BratNode (Constructor Int) [] [("value",[])]) @@ -26,9 +26,9 @@ Nodes: (rx.brat_globals_Qubit_21,BratNode (Constructor Qubit) [] [("value",[])]) (rx.brat_globals_Qubit_23,BratNode (Constructor Qubit) [] [("value",[])]) (rx.brat_globals_decl_12_nums,BratNode Id [("x",Int),("y",Int),("z",Int)] [("x",Int),("y",Int),("z",Int)]) -(rx.brat_globals_decl_18_xish,BratNode Id [("a1",{ (rxa :: Qubit) -o (rxb :: Qubit) })] [("a1",{ (rxa :: Qubit) -o (rxb :: Qubit) })]) -(rx.brat_globals_decl_24_main,BratNode Id [("a1",{ (a :: Qubit) -o (b :: Qubit) })] [("a1",{ (a :: Qubit) -o (b :: Qubit) })]) -(rx.brat_globals_prim_7_Rx,BratNode (Prim ("","Rx")) [] [("thunk",{ (th :: Float) -> (a1 :: { (rxa :: Qubit) -o (rxb :: Qubit) }) })]) +(rx.brat_globals_decl_18_xish,BratNode Id [("_0",{ (rxa :: Qubit) -o (rxb :: Qubit) })] [("_0",{ (rxa :: Qubit) -o (rxb :: Qubit) })]) +(rx.brat_globals_decl_24_main,BratNode Id [("_0",{ (a :: Qubit) -o (b :: Qubit) })] [("_0",{ (a :: Qubit) -o (b :: Qubit) })]) +(rx.brat_globals_prim_7_Rx,BratNode (Prim ("","Rx")) [] [("thunk",{ (th :: Float) -> (_1 :: { (rxa :: Qubit) -o (rxb :: Qubit) }) })]) Wires: (Ex rx.brat_check_defs_1_main_3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_Splice 0,Qubit,In rx.brat_check_defs_1_main_3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/out_2 0) diff --git a/brat/test/golden/graph/swap.brat.graph b/brat/test/golden/graph/swap.brat.graph index 931f8f27..876ad656 100644 --- a/brat/test/golden/graph/swap.brat.graph +++ b/brat/test/golden/graph/swap.brat.graph @@ -13,7 +13,7 @@ Nodes: (swap.brat_globals_Qubit_3,BratNode (Constructor Qubit) [] [("value",[])]) (swap.brat_globals_Qubit_5,BratNode (Constructor Qubit) [] [("value",[])]) (swap.brat_globals_Qubit_6,BratNode (Constructor Qubit) [] [("value",[])]) -(swap.brat_globals_decl_7_main,BratNode Id [("a1",{ (a :: Qubit), (b :: Qubit) -o (b :: Qubit), (a :: Qubit) })] [("a1",{ (a :: Qubit), (b :: Qubit) -o (b :: Qubit), (a :: Qubit) })]) +(swap.brat_globals_decl_7_main,BratNode Id [("_0",{ (a :: Qubit), (b :: Qubit) -o (b :: Qubit), (a :: Qubit) })] [("_0",{ (a :: Qubit), (b :: Qubit) -o (b :: Qubit), (a :: Qubit) })]) Wires: (Ex swap.brat_check_defs_1_main_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/in_1 0,Qubit,In swap.brat_check_defs_1_main_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/out_2 1) diff --git a/brat/test/golden/graph/two.brat.graph b/brat/test/golden/graph/two.brat.graph index 3afc7eab..3722863d 100644 --- a/brat/test/golden/graph/two.brat.graph +++ b/brat/test/golden/graph/two.brat.graph @@ -8,7 +8,7 @@ Nodes: (two.brat_globals_Int_7,BratNode (Constructor Int) [] [("value",[])]) (two.brat_globals_Int_10,BratNode (Constructor Int) [] [("value",[])]) (two.brat_globals_decl_8_one,BratNode Id [("n",Int)] [("n",Int)]) -(two.brat_globals_decl_11_two,BratNode Id [("a1",Int)] [("a1",Int)]) +(two.brat_globals_decl_11_two,BratNode Id [("_0",Int)] [("_0",Int)]) (two.brat_globals_prim_5_add,BratNode (Prim ("","add")) [] [("thunk",{ (a :: Int), (b :: Int) -> (c :: Int) })]) Wires: diff --git a/brat/test/golden/graph/vec.brat.graph b/brat/test/golden/graph/vec.brat.graph index 301605ea..719e888a 100644 --- a/brat/test/golden/graph/vec.brat.graph +++ b/brat/test/golden/graph/vec.brat.graph @@ -27,7 +27,7 @@ Nodes: (vec.brat_globals_Int_2,BratNode (Constructor Int) [] [("value",[])]) (vec.brat_globals_Vec_1,BratNode (Constructor Vec) [("X",[]),("n",Nat)] [("value",[])]) (vec.brat_globals_const_3,BratNode (Const 3) [] [("value",Nat)]) -(vec.brat_globals_decl_4_xs,BratNode Id [("a1",Vec(Int, 3))] [("a1",Vec(Int, 3))]) +(vec.brat_globals_decl_4_xs,BratNode Id [("_0",Vec(Int, 3))] [("_0",Vec(Int, 3))]) Wires: (Ex vec.brat_check_defs_1_xs_$rhs_check'Con__2 0,[],In vec.brat_check_defs_1_xs_$rhs_check'Con_$!_pat2val 0) diff --git a/brat/test/golden/kernel/kernel_application.brat.golden b/brat/test/golden/kernel/kernel_application.brat.golden index af09def9..0e8f7657 100644 --- a/brat/test/golden/kernel/kernel_application.brat.golden +++ b/brat/test/golden/kernel/kernel_application.brat.golden @@ -2,5 +2,5 @@ Error in test/golden/kernel/kernel_application.brat on line 16: rotate = { q => maybeRotate(true) } ^^^^^^^^^^^ - 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) }) } From fa4a0f84322595bd36d24bf37ef6363e21c7e33d Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Fri, 1 May 2026 16:16:31 +0100 Subject: [PATCH 02/14] Review comments --- brat/Brat/Checker/Helpers.hs | 2 +- brat/Brat/Syntax/Common.hs | 7 +++---- brat/Brat/Syntax/Core.hs | 4 ---- brat/Brat/Syntax/Raw.hs | 5 +---- brat/Brat/Unelaborator.hs | 5 +---- 5 files changed, 6 insertions(+), 17 deletions(-) diff --git a/brat/Brat/Checker/Helpers.hs b/brat/Brat/Checker/Helpers.hs index 636a8e33..d599c9f4 100644 --- a/brat/Brat/Checker/Helpers.hs +++ b/brat/Brat/Checker/Helpers.hs @@ -142,7 +142,7 @@ type family ThunkRowType (m :: Mode) where ThunkRowType Kernel = Term Chk Noun simpleTypeRow :: [(PortName, ty)] -> [TypeRowElem ty] -simpleTypeRow = fmap aux where aux (p, ty) = Named p ty +simpleTypeRow = fmap (uncurry Named) mkThunkTy :: Modey m -> ThunkFCType m diff --git a/brat/Brat/Syntax/Common.hs b/brat/Brat/Syntax/Common.hs index aaf843f7..a8065755 100644 --- a/brat/Brat/Syntax/Common.hs +++ b/brat/Brat/Syntax/Common.hs @@ -201,13 +201,12 @@ instance Show Import where showSelection (ImportHiding fns) = "hiding (":(unWC <$> fns) ++ [")"] showSig :: (Show ty) => [TypeRowElem ty] -> String -showSig [] = "()" -showSig (hd:tl) = parens $ concat (tail (showElem hd) ++ [unwords (showElem x) | x <- tl]) +showSig xs = parens $ intercalate ", " (showElem <$> xs) where parens x = '(':x ++ ")" - showElem (Anon ty) = [",", show ty] - showElem (Named p ty) = [",", '(':p ++ " :: " ++ show ty ++ ")"] + showElem (Anon ty) = show ty + showElem (Named p ty) = '(':p ++ " :: " ++ show ty ++ ")" showRow :: Show ty => [(NamedPort e, ty)] -> String showRow = parens . intercalate ", " . fmap (\(np, ty) -> unwords [portName np, "::", show ty]) diff --git a/brat/Brat/Syntax/Core.hs b/brat/Brat/Syntax/Core.hs index 2d414a13..32a29b15 100644 --- a/brat/Brat/Syntax/Core.hs +++ b/brat/Brat/Syntax/Core.hs @@ -1,6 +1,4 @@ module Brat.Syntax.Core (Term(..) - ,Input - ,Output ,InOut ,CType ,Precedence(..) @@ -21,8 +19,6 @@ import Brat.Syntax.Simple import Data.Kind (Type) import Data.Maybe (fromJust) -type Input = InOut -type Output = InOut type InOut = (PortName, KindOr (Term Chk Noun)) type CType = CType' InOut diff --git a/brat/Brat/Syntax/Raw.hs b/brat/Brat/Syntax/Raw.hs index 4c48db2b..f7115982 100644 --- a/brat/Brat/Syntax/Raw.hs +++ b/brat/Brat/Syntax/Raw.hs @@ -233,10 +233,7 @@ instance (Kindable k) => Desugarable (Raw d k) where instance Desugarable (CType' (TypeRowElem RawVType)) where type Desugared (CType' (TypeRowElem RawVType)) = CType' (TypeRowElem (Term Chk Noun)) desugar' :: CType' (TypeRowElem RawVType) -> Desugar (CType' (TypeRowElem (Term Chk Noun))) - desugar' (ss :-> ts) = do - ss <- traverse desugar' ss - ts <- traverse desugar' ts - pure (ss :-> ts) + desugar' cty = traverse desugar' cty isConOrAlias :: QualName -> Desugar Bool isConOrAlias c = do diff --git a/brat/Brat/Unelaborator.hs b/brat/Brat/Unelaborator.hs index 3578e20c..a4c9368e 100644 --- a/brat/Brat/Unelaborator.hs +++ b/brat/Brat/Unelaborator.hs @@ -27,10 +27,7 @@ unelab _ ky (Pull ps tm) = FPull ps (unelab Chky ky <$> tm) unelab _ _ (Var v) = FVar v unelab dy ky (Arith op lhs rhs) = FArith op (unelab dy ky <$> lhs) (unelab dy ky <$> rhs) unelab dy _ (Of n e) = FOf (unelab Chky Nouny <$> n) (unelab dy Nouny <$> e) -unelab _ _ (tm ::: outs) = FAnnotation (unelab Chky Nouny <$> tm) (f outs) - where - f :: [TypeRowElem (KindOr (Term Chk Noun))] -> [TypeRowElem (WC (KindOr Flat))] - f = fmap (fmap (dummyFC . fmap (unelab Chky Nouny))) +unelab _ _ (tm ::: outs) = FAnnotation (unelab Chky Nouny <$> tm) (unelabRo outs) unelab dy ky (top :-: bot) = case ky of Nouny -> FInto (unelab Syny Nouny <$> top) (unelab dy UVerby <$> bot) _ -> FApp (unelab Syny ky <$> top) (unelab dy UVerby <$> bot) From fed434952b66fe1705aad5ee1a4ff4280b90c242 Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Fri, 1 May 2026 16:16:52 +0100 Subject: [PATCH 03/14] Specialise flatIO --- brat/Brat/Parser.hs | 20 +++++++++---------- .../test/golden/error/portpull-ambiguous.brat | 2 +- 2 files changed, 11 insertions(+), 11 deletions(-) diff --git a/brat/Brat/Parser.hs b/brat/Brat/Parser.hs index 43c52491..69e58d9c 100644 --- a/brat/Brat/Parser.hs +++ b/brat/Brat/Parser.hs @@ -286,19 +286,19 @@ flatIO = rowElem `sepBy` void (try comma) WC kFC k <- typekind pure (Named p (WC (spanFC pFC kFC) (Left k))) -flatIO' :: Parser ty -> Parser (TypeRow ty) -flatIO' tyP = rowElem `sepBy` void (try comma) +flatIO' :: Parser (TypeRow (WC Flat)) +flatIO' = rowElem `sepBy` void (try comma) where rowElem = try (inBrackets Paren rowElem') <|> rowElem' - -- Look out if we can find ::. If not, backtrack and just do tyP. + -- Look out if we can find ::. If not, backtrack and just do `vtype`. -- For example, if we get an invalid primitive type (e.g. `Int` in -- a kernel or a misspelled type like `Intt`), we get the better - -- error message from tyP instead of complaining about a missing :: + -- error message from vtype instead of complaining about a missing :: -- (since the invalid type can be parsed as a port name) rowElem' = optional (try $ port <* match TypeColon) >>= \case - Just (WC _ p) -> Named p <$> tyP - Nothing -> Anon <$> tyP + Just (WC _ p) -> Named p <$> vtype + Nothing -> Anon <$> vtype spanningFC :: TypeRow (WC ty) -> Parser (WC (TypeRow (WC ty))) spanningFC [] = customFailure (Custom "Internal: FlatIO shouldn't be empty") @@ -343,9 +343,9 @@ cthunk = try bratFn <|> try kernel <|> thunk pure $ FFn (ss :-> ts) kernel = inBracketsFC Brace $ do - ss <- flatIO' vtype + ss <- flatIO' match Lolly - ts <- flatIO' vtype + ts <- flatIO' pure $ FKernel (ss :-> ts) @@ -782,9 +782,9 @@ declSignature = try nDecl <|> vDecl where kernel :: Parser (WC (CType' (TypeRowElem (WC Flat)))) kernel = do - WC startFC ins <- inBracketsFC Paren $ flatIO' vtype + WC startFC ins <- inBracketsFC Paren $ flatIO' match Lolly - WC endFC outs <- spanningFC =<< flatIO' vtype + WC endFC outs <- spanningFC =<< flatIO' pure (WC (spanFC startFC endFC) (ins :-> outs)) pfile :: Parser ([Import], FEnv) diff --git a/brat/test/golden/error/portpull-ambiguous.brat b/brat/test/golden/error/portpull-ambiguous.brat index 237c6fc2..f749f515 100644 --- a/brat/test/golden/error/portpull-ambiguous.brat +++ b/brat/test/golden/error/portpull-ambiguous.brat @@ -3,4 +3,4 @@ id = x => x -- This should fail because there are multiple ports called "a1" id2(Nat, Nat) -> Nat, Nat -id2 = x, y => (id,id)(a1:x, y) +id2 = x, y => (id,id)(_0:x, y) From 50b2f4180fb35f9d323cedc09a4125ac781b5cee Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Fri, 15 May 2026 13:19:47 +0100 Subject: [PATCH 04/14] refactor: Introduce `Solution` type alias --- brat/Brat/Checker.hs | 8 ++++---- brat/Brat/Checker/SolvePatterns.hs | 8 +++++--- 2 files changed, 9 insertions(+), 7 deletions(-) diff --git a/brat/Brat/Checker.hs b/brat/Brat/Checker.hs index 7c9ccd58..2a8eb285 100644 --- a/brat/Brat/Checker.hs +++ b/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,11 +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 ([(String, (Src, BinderType 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) diff --git a/brat/Brat/Checker/SolvePatterns.hs b/brat/Brat/Checker/SolvePatterns.hs index cd49a366..855ba006 100644 --- a/brat/Brat/Checker/SolvePatterns.hs +++ b/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 From 8bc5ce49b0ef232ef6819e43a1f9c3f4b5af58b0 Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Fri, 15 May 2026 13:23:44 +0100 Subject: [PATCH 05/14] Elaborable -> Elaboratable --- brat/Brat/Elaborator.hs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/brat/Brat/Elaborator.hs b/brat/Brat/Elaborator.hs index 77203308..a68cffc5 100644 --- a/brat/Brat/Elaborator.hs +++ b/brat/Brat/Elaborator.hs @@ -196,21 +196,21 @@ elaborate' FIdentity = pure $ SomeRaw' RIdentity elaborate' FUnderscore = Left (dumbErr (InternalError "Unexpected '_'")) elaborate' FFanOut = pure $ SomeRaw' RFanOut elaborate' FFanIn = pure $ SomeRaw' RFanIn -class Elaborable t where +class Elaboratable 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 +instance Elaboratable Flat where type Elaborated Flat = Raw Chk Noun elab = elaborateChkNoun -instance Elaborable t => Elaborable (KindOr t) where +instance Elaboratable t => Elaboratable (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 +elabSigElem :: Elaboratable t => TypeRowElem (WC t) -> Either Error (TypeRowElem (WC (Elaborated t))) elabSigElem (Anon ty) = Anon <$> elab ty From 7ddc09ca7e0d96c79101aa40cc0fa4f72445b166 Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Fri, 15 May 2026 13:29:04 +0100 Subject: [PATCH 06/14] traverse elabSigElem -> elabSig --- brat/Brat/Elaborator.hs | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/brat/Brat/Elaborator.hs b/brat/Brat/Elaborator.hs index a68cffc5..eee6449b 100644 --- a/brat/Brat/Elaborator.hs +++ b/brat/Brat/Elaborator.hs @@ -179,7 +179,7 @@ elaborate' (FAnnotation a ts) = do (SomeRaw a) <- elaborate a a <- assertChk a a <- assertNoun a - ts <- fmap (fmap unWC) <$> traverse elabSigElem ts + ts <- fmap (fmap unWC) <$> elabSig ts pure $ SomeRaw' (a ::::: ts) elaborate' (FInto a b) = elaborate' (FApp b a) elaborate' (FOf n e) = do @@ -188,8 +188,8 @@ elaborate' (FOf n e) = do SomeRaw e <- elaborate e e <- assertNoun e pure $ SomeRaw' (ROf n e) -elaborate' (FFn cty) = SomeRaw' . RFn . fmap (fmap unWC) <$> traverse elabSigElem cty -elaborate' (FKernel cty) = SomeRaw' . RKernel . fmap (fmap unWC) <$> traverse elabSigElem cty +elaborate' (FFn cty) = SomeRaw' . RFn . fmap (fmap unWC) <$> elabSig 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 @@ -210,11 +210,10 @@ instance Elaboratable t => Elaboratable (KindOr t) where elab (WC fc (Left k)) = pure (WC fc (Left k)) elab (WC fc (Right ty)) = fmap Right <$> elab (WC fc ty) -elabSigElem :: Elaboratable t - => TypeRowElem (WC t) - -> Either Error (TypeRowElem (WC (Elaborated t))) -elabSigElem (Anon ty) = Anon <$> elab ty -elabSigElem (Named p ty) = Named p <$> elab ty +elabSig :: Elaboratable t + => [TypeRowElem (WC t)] + -> Either Error [TypeRowElem (WC (Elaborated t))] +elabSig = traverse (traverse elab) elabBody :: FBody -> FC -> Either Error (FunBody Raw Noun) elabBody (FClauses cs) fc = ThunkOf . WC fc . Clauses <$> traverse elab1Clause cs From 977b8103b1d793a6426d596b9780a3c7295a9709 Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Fri, 15 May 2026 13:38:11 +0100 Subject: [PATCH 07/14] Automatic port names are just numbers, and now they can be pulled --- brat/Brat/Checker.hs | 2 +- brat/Brat/Elaborator.hs | 9 ++++---- brat/Brat/Parser.hs | 4 ++-- brat/test/golden/binding/let.brat.golden | 2 +- .../golden/error/apply_two_thunks.brat.golden | 2 +- brat/test/golden/error/empty_into.brat.golden | 4 ++-- .../error/fanout-diff-types.brat.golden | 2 +- .../error/fanout-not-enough-overs.brat.golden | 2 +- brat/test/golden/error/pair.brat.golden | 4 ++-- .../test/golden/error/portpull-ambiguous.brat | 4 ++-- .../error/portpull-ambiguous.brat.golden | 6 ++--- brat/test/golden/error/portpull.brat | 2 +- brat/test/golden/error/portpull.brat.golden | 2 +- .../golden/error/remaining_holes.brat.golden | 4 ++-- .../error/toplevel-leftovers.brat.golden | 4 ++-- .../error/toplevel-leftovers2.brat.golden | 4 ++-- .../error/toplevel-leftovers3.brat.golden | 2 +- .../error/vectorise-type-mismatch.brat.golden | 2 +- brat/test/golden/error/vectorise3.brat.golden | 2 +- brat/test/golden/graph/addN2.brat.graph | 2 +- brat/test/golden/graph/cons.brat.graph | 4 ++-- brat/test/golden/graph/id.brat.graph | 2 +- brat/test/golden/graph/kernel.brat.graph | 22 +++++++++---------- brat/test/golden/graph/list.brat.graph | 2 +- brat/test/golden/graph/num.brat.graph | 4 ++-- brat/test/golden/graph/pair.brat.graph | 2 +- brat/test/golden/graph/rx.brat.graph | 8 +++---- brat/test/golden/graph/swap.brat.graph | 2 +- brat/test/golden/graph/two.brat.graph | 2 +- brat/test/golden/graph/vec.brat.graph | 2 +- .../kernel/kernel_application.brat.golden | 2 +- 31 files changed, 59 insertions(+), 58 deletions(-) diff --git a/brat/Brat/Checker.hs b/brat/Brat/Checker.hs index 2a8eb285..c3c2a9a7 100644 --- a/brat/Brat/Checker.hs +++ b/brat/Brat/Checker.hs @@ -1085,7 +1085,7 @@ kindCheckRow' :: forall m n -> Checking (Int, VEnv, Some (Endz :* Ro m n)) kindCheckRow' _ ez env (_,i) [] = pure (i, env, Some (ez :* R0)) -kindCheckRow' my nys env (name, i) ((Anon ty):rest) = kindCheckRow' my nys env (name, i) ((Named ('_':show i) ty):rest) +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?? diff --git a/brat/Brat/Elaborator.hs b/brat/Brat/Elaborator.hs index eee6449b..2a411a97 100644 --- a/brat/Brat/Elaborator.hs +++ b/brat/Brat/Elaborator.hs @@ -188,19 +188,20 @@ elaborate' (FOf n e) = do SomeRaw e <- elaborate e e <- assertNoun e pure $ SomeRaw' (ROf n e) -elaborate' (FFn cty) = SomeRaw' . RFn . fmap (fmap unWC) <$> elabSig cty -elaborate' (FKernel cty) = SomeRaw' . RKernel . fmap (fmap unWC) <$> elabSig cty +elaborate' (FFn cty) = SomeRaw' . RFn . fmap (fmap unWC) <$> traverse (traverse elab) cty +elaborate' (FKernel cty) = SomeRaw' . RKernel . fmap (fmap unWC) <$> traverse (traverse elab) 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 Elaboratable t where type Elaborated t elab :: WC t -> Either Error (WC (Elaborated t)) --- This is a hack to make elabSigElem nice +-- This is a hack to make elabSig nice instance Elaboratable Flat where type Elaborated Flat = Raw Chk Noun elab = elaborateChkNoun @@ -236,7 +237,7 @@ elabBody FUndefined _ = pure Undefined elabFunDecl :: FDecl -> Either Error RawFuncDecl elabFunDecl d = do rc <- elabBody (fnBody d) (fnLoc d) - sig <- traverse elabSigElem (fnSig d) + sig <- elabSig (fnSig d) pure $ FuncDecl { fnName = fnName d , fnLoc = fnLoc d diff --git a/brat/Brat/Parser.hs b/brat/Brat/Parser.hs index 69e58d9c..619a6ea7 100644 --- a/brat/Brat/Parser.hs +++ b/brat/Brat/Parser.hs @@ -179,7 +179,7 @@ abstractor = do ps <- many (try portPull) list2Cons (APat x:xs) = PCons x <$> list2Cons xs list2Cons _ = customFailure (Custom "Internal error list2Cons") - portPull = port <* match PortColon + portPull = (try port <|> (fmap show <$> number)) <* match PortColon -- For simplicity, we can say for now that all of our infix vector patterns have -- the same precedence and associate to the right @@ -574,7 +574,7 @@ expr' p = choice $ (try . getParser <$> enumFrom p) ++ [atomExpr] where portPull :: Parser (WC String) portPull = do - WC portFC portName <- port + WC portFC portName <- try port <|> (fmap show <$> number) WC colonFC _ <- matchFC PortColon pure (WC (spanFC portFC colonFC) portName) diff --git a/brat/test/golden/binding/let.brat.golden b/brat/test/golden/binding/let.brat.golden index 86ac42af..e6bf9468 100644 --- a/brat/test/golden/binding/let.brat.golden +++ b/brat/test/golden/binding/let.brat.golden @@ -3,5 +3,5 @@ badBinding = let x = twoThings in x ^^^^^^^^^^^^^^^^^^^^^^ Internal error: Expected empty unders after abstract, got: - (_1 :: Int) + (1 :: Int) diff --git a/brat/test/golden/error/apply_two_thunks.brat.golden b/brat/test/golden/error/apply_two_thunks.brat.golden index ec1da67f..f42fcd54 100644 --- a/brat/test/golden/error/apply_two_thunks.brat.golden +++ b/brat/test/golden/error/apply_two_thunks.brat.golden @@ -3,5 +3,5 @@ go(n) = thunks(n) ^^^^^^^^^ Type error: Expected function thunks() to consume all of its arguments (「n」) - but found leftovers: (_0 :: Int) + but found leftovers: (0 :: Int) diff --git a/brat/test/golden/error/empty_into.brat.golden b/brat/test/golden/error/empty_into.brat.golden index fe635cc5..5a50fad6 100644 --- a/brat/test/golden/error/empty_into.brat.golden +++ b/brat/test/golden/error/empty_into.brat.golden @@ -3,7 +3,7 @@ intoErr = |> makeInt ^^^^^^^^^^ Type mismatch when checking makeInt()(()) -Expected: (_0 :: Bool) -But got: (_0 :: Int) +Expected: (0 :: Bool) +But got: (0 :: Int) diff --git a/brat/test/golden/error/fanout-diff-types.brat.golden b/brat/test/golden/error/fanout-diff-types.brat.golden index 82430baa..360a9487 100644 --- a/brat/test/golden/error/fanout-diff-types.brat.golden +++ b/brat/test/golden/error/fanout-diff-types.brat.golden @@ -3,7 +3,7 @@ f = { [/\] } ^^^^ Type mismatch when checking [/\] -Expected: (_1 :: Bit) +Expected: (1 :: Bit) But got: (head :: Qubit) diff --git a/brat/test/golden/error/fanout-not-enough-overs.brat.golden b/brat/test/golden/error/fanout-not-enough-overs.brat.golden index 7cb723fb..6915bbb0 100644 --- a/brat/test/golden/error/fanout-not-enough-overs.brat.golden +++ b/brat/test/golden/error/fanout-not-enough-overs.brat.golden @@ -2,5 +2,5 @@ Error in test/golden/error/fanout-not-enough-overs.brat on line 2: f = { [/\] } ^^^^^^^^ - Expected function to return additional values of type: (_3 :: Nat) + Expected function to return additional values of type: (3 :: Nat) diff --git a/brat/test/golden/error/pair.brat.golden b/brat/test/golden/error/pair.brat.golden index 33fd6b91..eb190b0b 100644 --- a/brat/test/golden/error/pair.brat.golden +++ b/brat/test/golden/error/pair.brat.golden @@ -3,7 +3,7 @@ pair = row -- Distinct from a pair ^^^ Type mismatch when checking row -Expected: (_0 :: [Int,Bool]) -But got: (_0 :: Int, _1 :: Bool) +Expected: (0 :: [Int,Bool]) +But got: (0 :: Int, 1 :: Bool) diff --git a/brat/test/golden/error/portpull-ambiguous.brat b/brat/test/golden/error/portpull-ambiguous.brat index f749f515..7b12d08d 100644 --- a/brat/test/golden/error/portpull-ambiguous.brat +++ b/brat/test/golden/error/portpull-ambiguous.brat @@ -1,6 +1,6 @@ id(Nat) -> Nat id = x => x --- This should fail because there are multiple ports called "a1" +-- This should fail because there are multiple ports called "0" id2(Nat, Nat) -> Nat, Nat -id2 = x, y => (id,id)(_0:x, y) +id2 = x, y => (id,id)(0:x, y) diff --git a/brat/test/golden/error/portpull-ambiguous.brat.golden b/brat/test/golden/error/portpull-ambiguous.brat.golden index f9d0e292..cce16f33 100644 --- a/brat/test/golden/error/portpull-ambiguous.brat.golden +++ b/brat/test/golden/error/portpull-ambiguous.brat.golden @@ -1,6 +1,6 @@ Error in test/golden/error/portpull-ambiguous.brat on line 6: -id2 = x, y => (id,id)(a1:x, y) - ^^^^^^^^^ +id2 = x, y => (id,id)(0:x, y) + ^^^^^^^^ - Port not found: a1 in (_0 :: Nat, _0 :: Nat) + Port 0 is ambiguous in (0 :: Nat, 0 :: Nat) diff --git a/brat/test/golden/error/portpull.brat b/brat/test/golden/error/portpull.brat index d9405e29..3f29c42f 100644 --- a/brat/test/golden/error/portpull.brat +++ b/brat/test/golden/error/portpull.brat @@ -3,4 +3,4 @@ id = x => x -- This one should fail because there is no port name "z" id2(Nat, Nat) -> Nat, Nat -id2 = x,y => (id, id)(a1:x, y) +id2 = x,y => (id, id)(z:x, y) diff --git a/brat/test/golden/error/portpull.brat.golden b/brat/test/golden/error/portpull.brat.golden index 7d0e7bc0..5370d8ff 100644 --- a/brat/test/golden/error/portpull.brat.golden +++ b/brat/test/golden/error/portpull.brat.golden @@ -2,5 +2,5 @@ Error in test/golden/error/portpull.brat on line 6: id2 = x,y => (id, id)(a1:x, y) ^^^^^^^^^ - Port not found: a1 in (_0 :: Nat, _0 :: Nat) + Port not found: a1 in (0 :: Nat, 0 :: Nat) diff --git a/brat/test/golden/error/remaining_holes.brat.golden b/brat/test/golden/error/remaining_holes.brat.golden index 829d801b..0178bee8 100644 --- a/brat/test/golden/error/remaining_holes.brat.golden +++ b/brat/test/golden/error/remaining_holes.brat.golden @@ -1,4 +1,4 @@ Can't compile file with remaining holes - ?a_hole :: (_0 :: Bit) - ?b_hole :: (thunk :: { (_0 :: Int) -> (_1 :: List(Int)) }) + ?a_hole :: (0 :: Bit) + ?b_hole :: (thunk :: { (0 :: Int) -> (1 :: List(Int)) }) diff --git a/brat/test/golden/error/toplevel-leftovers.brat.golden b/brat/test/golden/error/toplevel-leftovers.brat.golden index 222e5cb4..15f40d15 100644 --- a/brat/test/golden/error/toplevel-leftovers.brat.golden +++ b/brat/test/golden/error/toplevel-leftovers.brat.golden @@ -3,7 +3,7 @@ f = 42 ^^ Type mismatch when checking f -Expected: (_0 :: Nat, _1 :: Bool) -But got: (_0 :: Nat) +Expected: (0 :: Nat, 1 :: Bool) +But got: (0 :: Nat) diff --git a/brat/test/golden/error/toplevel-leftovers2.brat.golden b/brat/test/golden/error/toplevel-leftovers2.brat.golden index 47ac772b..22747075 100644 --- a/brat/test/golden/error/toplevel-leftovers2.brat.golden +++ b/brat/test/golden/error/toplevel-leftovers2.brat.golden @@ -4,7 +4,7 @@ f(x) = x Type mismatch when checking x => 「x」 -Expected: (_1 :: Nat, _2 :: Bool) -But got: (_1 :: Nat) +Expected: (1 :: Nat, 2 :: Bool) +But got: (1 :: Nat) diff --git a/brat/test/golden/error/toplevel-leftovers3.brat.golden b/brat/test/golden/error/toplevel-leftovers3.brat.golden index b661fdff..38bbeca8 100644 --- a/brat/test/golden/error/toplevel-leftovers3.brat.golden +++ b/brat/test/golden/error/toplevel-leftovers3.brat.golden @@ -2,5 +2,5 @@ Error in test/golden/error/toplevel-leftovers3.brat on line 2: f(x) = x ^ - Type error: Inputs (_1 :: Bool) weren't used + Type error: Inputs (1 :: Bool) weren't used diff --git a/brat/test/golden/error/vectorise-type-mismatch.brat.golden b/brat/test/golden/error/vectorise-type-mismatch.brat.golden index 22634fd0..faba5cc5 100644 --- a/brat/test/golden/error/vectorise-type-mismatch.brat.golden +++ b/brat/test/golden/error/vectorise-type-mismatch.brat.golden @@ -3,6 +3,6 @@ panic = 2 of 42 ^^^^^^^ Type error: Got: Vector of length 2 -Expected: (_0 :: Vec(Nat, 1)) +Expected: (0 :: Vec(Nat, 1)) diff --git a/brat/test/golden/error/vectorise3.brat.golden b/brat/test/golden/error/vectorise3.brat.golden index 1e44756c..7d25229d 100644 --- a/brat/test/golden/error/vectorise3.brat.golden +++ b/brat/test/golden/error/vectorise3.brat.golden @@ -3,5 +3,5 @@ f(_, _, n, f, xs) = (n of f)(xs) ^^^^^^^^^^^^ Type error: Expected function 「n」 of f() to consume all of its arguments (「xs」) - but found leftovers: (_1 :: Vec(VApp VPar Ex checking_vectorise3_check_defs_1_f_$lhs_3_lambda_fake_source 0 B0, VPar Ex checking_vectorise3_check_defs_1_f_$lhs_3_lambda_fake_source 2)) + but found leftovers: (1 :: Vec(VApp VPar Ex checking_vectorise3_check_defs_1_f_$lhs_3_lambda_fake_source 0 B0, VPar Ex checking_vectorise3_check_defs_1_f_$lhs_3_lambda_fake_source 2)) diff --git a/brat/test/golden/graph/addN2.brat.graph b/brat/test/golden/graph/addN2.brat.graph index fb55e830..ab7ec3d0 100644 --- a/brat/test/golden/graph/addN2.brat.graph +++ b/brat/test/golden/graph/addN2.brat.graph @@ -18,7 +18,7 @@ Nodes: (addN2.brat_globals_Int_12,BratNode (Constructor Int) [] [("value",[])]) (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")) [] [("_0",{ (a :: Int), (b :: Int) -> (c :: Int) })]) +(addN2.brat_globals_prim_8_add,BratNode (Prim ("","add")) [] [("0",{ (a :: Int), (b :: Int) -> (c :: Int) })]) Wires: (Ex addN2.brat_check_defs_1_addN_LambdaChk_9_checkClauses_1_$rhs_4_Eval 0,Int,In addN2.brat_check_defs_1_addN_LambdaChk_9_checkClauses_1_lambda.0_rhs/out_2 0) diff --git a/brat/test/golden/graph/cons.brat.graph b/brat/test/golden/graph/cons.brat.graph index fe6f49bc..4cac52cf 100644 --- a/brat/test/golden/graph/cons.brat.graph +++ b/brat/test/golden/graph/cons.brat.graph @@ -30,8 +30,8 @@ Nodes: (cons.brat_globals_Vec_6,BratNode (Constructor Vec) [("X",[]),("n",Nat)] [("value",[])]) (cons.brat_globals_const_3,BratNode (Const 2) [] [("value",Nat)]) (cons.brat_globals_const_8,BratNode (Const 3) [] [("value",Nat)]) -(cons.brat_globals_decl_4_two,BratNode Id [("_0",Vec(Int, 2))] [("_0",Vec(Int, 2))]) -(cons.brat_globals_decl_9_three,BratNode Id [("_0",Vec(Int, 3))] [("_0",Vec(Int, 3))]) +(cons.brat_globals_decl_4_two,BratNode Id [("0",Vec(Int, 2))] [("0",Vec(Int, 2))]) +(cons.brat_globals_decl_9_three,BratNode Id [("0",Vec(Int, 3))] [("0",Vec(Int, 3))]) Wires: (Ex cons.brat_check_defs_1_three_2_$rhs_check'Con__2 0,[],In cons.brat_check_defs_1_three_2_$rhs_check'Con_$!_pat2val 0) diff --git a/brat/test/golden/graph/id.brat.graph b/brat/test/golden/graph/id.brat.graph index e6a6e03d..6079c068 100644 --- a/brat/test/golden/graph/id.brat.graph +++ b/brat/test/golden/graph/id.brat.graph @@ -11,7 +11,7 @@ Nodes: (id.brat_check_defs_1_main_$rhs_check'Th_thunk_thunk_2,BratNode (Box id.brat_check_defs_1_main_$rhs_check'Th_thunk/in id.brat_check_defs_1_main_$rhs_check'Th_thunk/out_1) [] [("thunk",{ (a :: Qubit) -o (b :: Qubit) })]) (id.brat_globals_Qubit_2,BratNode (Constructor Qubit) [] [("value",[])]) (id.brat_globals_Qubit_4,BratNode (Constructor Qubit) [] [("value",[])]) -(id.brat_globals_decl_5_main,BratNode Id [("_0",{ (a :: Qubit) -o (b :: Qubit) })] [("_0",{ (a :: Qubit) -o (b :: Qubit) })]) +(id.brat_globals_decl_5_main,BratNode Id [("0",{ (a :: Qubit) -o (b :: Qubit) })] [("0",{ (a :: Qubit) -o (b :: Qubit) })]) Wires: (Ex id.brat_check_defs_1_main_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/in_1 0,Qubit,In id.brat_check_defs_1_main_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/out_2 0) diff --git a/brat/test/golden/graph/kernel.brat.graph b/brat/test/golden/graph/kernel.brat.graph index f5bcae9a..fa043a74 100644 --- a/brat/test/golden/graph/kernel.brat.graph +++ b/brat/test/golden/graph/kernel.brat.graph @@ -1,7 +1,7 @@ Nodes: -(kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in,KernelNode Source [] [("_0",Qubit),("_1",Qubit),("_2",Qubit)]) -(kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/out_1,KernelNode Target [("_0",Vec(Qubit, 3))] []) -(kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup_thunk_2,BratNode (Box kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/out_1) [] [("thunk",{ (_0 :: Qubit), (_1 :: Qubit), (_2 :: Qubit) -o (_0 :: Vec(Qubit, 3)) })]) +(kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in,KernelNode Source [] [("0",Qubit),("1",Qubit),("2",Qubit)]) +(kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/out_1,KernelNode Target [("0",Vec(Qubit, 3))] []) +(kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup_thunk_2,BratNode (Box kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/out_1) [] [("thunk",{ (0 :: Qubit), (1 :: Qubit), (2 :: Qubit) -o (0 :: Vec(Qubit, 3)) })]) (kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con__2,BratNode (Dummy $) [] [("dummy",[])]) (kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_$!_numpat2val_1,BratNode Id [("",Nat)] [("",Nat)]) (kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_$!_pat2val,BratNode Id [("",[])] [("",[])]) @@ -25,19 +25,19 @@ Nodes: (kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_typeEqsTail_1_$!_1_buildConst,BratNode (Const 2) [] [("value",Nat)]) (kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_typeEqsTail_1_$!_1_buildConst_2,BratNode (Const 0) [] [("value",Nat)]) (kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/in_1,KernelNode Source [] [("q0",Qubit),("q1",Qubit),("q2",Qubit)]) -(kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/out_2,KernelNode Target [("_0",Vec(Qubit, 3))] []) -(kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs_thunk_3,BratNode (Box kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/in_1 kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/out_2) [] [("thunk",{ (q0 :: Qubit), (q1 :: Qubit), (q2 :: Qubit) -o (_0 :: Vec(Qubit, 3)) })]) -(kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_lambda,KernelNode (PatternMatch ((TestMatchData Kerny (MatchSequence {matchInputs = [(NamedPort {end = Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in 0, portName = "_0"},Qubit),(NamedPort {end = Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in 1, portName = "_1"},Qubit),(NamedPort {end = Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in 2, portName = "_2"},Qubit)], matchTests = [], matchOutputs = [(NamedPort {end = Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in 0, portName = "_0"},Qubit),(NamedPort {end = Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in 1, portName = "_1"},Qubit),(NamedPort {end = Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in 2, portName = "_2"},Qubit)]}),kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs_thunk_3) :| [])) [("_0",Qubit),("_1",Qubit),("_2",Qubit)] [("_0",Vec(Qubit, 3))]) -(kernel.brat_check_defs_1_id3_$rhs_check'Th_thunk/in,KernelNode Source [] [("_0",Qubit),("_1",Qubit),("_2",Qubit)]) -(kernel.brat_check_defs_1_id3_$rhs_check'Th_thunk/out_1,KernelNode Target [("_0",Vec(Qubit, 3))] []) -(kernel.brat_check_defs_1_id3_$rhs_check'Th_thunk_thunk_2,BratNode (Box kernel.brat_check_defs_1_id3_$rhs_check'Th_thunk/in kernel.brat_check_defs_1_id3_$rhs_check'Th_thunk/out_1) [] [("thunk",{ (_0 :: Qubit), (_1 :: Qubit), (_2 :: Qubit) -o (_0 :: Vec(Qubit, 3)) })]) +(kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/out_2,KernelNode Target [("0",Vec(Qubit, 3))] []) +(kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs_thunk_3,BratNode (Box kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/in_1 kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/out_2) [] [("thunk",{ (q0 :: Qubit), (q1 :: Qubit), (q2 :: Qubit) -o (0 :: Vec(Qubit, 3)) })]) +(kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_lambda,KernelNode (PatternMatch ((TestMatchData Kerny (MatchSequence {matchInputs = [(NamedPort {end = Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in 0, portName = "0"},Qubit),(NamedPort {end = Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in 1, portName = "1"},Qubit),(NamedPort {end = Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in 2, portName = "2"},Qubit)], matchTests = [], matchOutputs = [(NamedPort {end = Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in 0, portName = "0"},Qubit),(NamedPort {end = Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in 1, portName = "1"},Qubit),(NamedPort {end = Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in 2, portName = "2"},Qubit)]}),kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs_thunk_3) :| [])) [("0",Qubit),("1",Qubit),("2",Qubit)] [("0",Vec(Qubit, 3))]) +(kernel.brat_check_defs_1_id3_$rhs_check'Th_thunk/in,KernelNode Source [] [("0",Qubit),("1",Qubit),("2",Qubit)]) +(kernel.brat_check_defs_1_id3_$rhs_check'Th_thunk/out_1,KernelNode Target [("0",Vec(Qubit, 3))] []) +(kernel.brat_check_defs_1_id3_$rhs_check'Th_thunk_thunk_2,BratNode (Box kernel.brat_check_defs_1_id3_$rhs_check'Th_thunk/in kernel.brat_check_defs_1_id3_$rhs_check'Th_thunk/out_1) [] [("thunk",{ (0 :: Qubit), (1 :: Qubit), (2 :: Qubit) -o (0 :: Vec(Qubit, 3)) })]) (kernel.brat_globals_Qubit_2,BratNode (Constructor Qubit) [] [("value",[])]) (kernel.brat_globals_Qubit_3,BratNode (Constructor Qubit) [] [("value",[])]) (kernel.brat_globals_Qubit_4,BratNode (Constructor Qubit) [] [("value",[])]) (kernel.brat_globals_Qubit_7,BratNode (Constructor Qubit) [] [("value",[])]) (kernel.brat_globals_Vec_6,BratNode (Constructor Vec) [("X",[]),("n",Nat)] [("value",[])]) (kernel.brat_globals_const_8,BratNode (Const 3) [] [("value",Nat)]) -(kernel.brat_globals_decl_9_id3,BratNode Id [("_0",{ (_0 :: Qubit), (_1 :: Qubit), (_2 :: Qubit) -o (_0 :: Vec(Qubit, 3)) })] [("_0",{ (_0 :: Qubit), (_1 :: Qubit), (_2 :: Qubit) -o (_0 :: Vec(Qubit, 3)) })]) +(kernel.brat_globals_decl_9_id3,BratNode Id [("0",{ (0 :: Qubit), (1 :: Qubit), (2 :: Qubit) -o (0 :: Vec(Qubit, 3)) })] [("0",{ (0 :: Qubit), (1 :: Qubit), (2 :: Qubit) -o (0 :: Vec(Qubit, 3)) })]) Wires: (Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con__2 0,[],In kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_$!_pat2val 0) @@ -62,7 +62,7 @@ Wires: (Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_thunk/in 0,Qubit,In kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_lambda 0) (Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_thunk/in 1,Qubit,In kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_lambda 1) (Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_thunk/in 2,Qubit,In kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_lambda 2) -(Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_thunk_thunk_2 0,{ (_0 :: Qubit), (_1 :: Qubit), (_2 :: Qubit) -o (_0 :: Vec(Qubit, 3)) },In kernel.brat_globals_decl_9_id3 0) +(Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_thunk_thunk_2 0,{ (0 :: Qubit), (1 :: Qubit), (2 :: Qubit) -o (0 :: Vec(Qubit, 3)) },In kernel.brat_globals_decl_9_id3 0) (Ex kernel.brat_globals_Qubit_2 0,[],In kernel.brat_globals___kcr__1 0) (Ex kernel.brat_globals_Qubit_3 0,[],In kernel.brat_globals___kcr__1 1) (Ex kernel.brat_globals_Qubit_4 0,[],In kernel.brat_globals___kcr__1 2) diff --git a/brat/test/golden/graph/list.brat.graph b/brat/test/golden/graph/list.brat.graph index 77e74475..0129f4ca 100644 --- a/brat/test/golden/graph/list.brat.graph +++ b/brat/test/golden/graph/list.brat.graph @@ -16,7 +16,7 @@ Nodes: (list.brat_check_defs_1_xs_$rhs_check'Con_const_4,BratNode (Const 1) [] [("value",Int)]) (list.brat_globals_Int_2,BratNode (Constructor Int) [] [("value",[])]) (list.brat_globals_List_1,BratNode (Constructor List) [("listValue",[])] [("value",[])]) -(list.brat_globals_decl_3_xs,BratNode Id [("_0",List(Int))] [("_0",List(Int))]) +(list.brat_globals_decl_3_xs,BratNode Id [("0",List(Int))] [("0",List(Int))]) Wires: (Ex list.brat_check_defs_1_xs_$rhs_check'Con__2 0,[],In list.brat_check_defs_1_xs_$rhs_check'Con_$!_pat2val 0) diff --git a/brat/test/golden/graph/num.brat.graph b/brat/test/golden/graph/num.brat.graph index 5365a1e0..681a87ab 100644 --- a/brat/test/golden/graph/num.brat.graph +++ b/brat/test/golden/graph/num.brat.graph @@ -5,8 +5,8 @@ Nodes: (num.brat_check_defs_1_n_$rhs_check'Con_succ_1,BratNode (Constructor succ) [("value",Nat)] [("value",Nat)]) (num.brat_globals_Int_4,BratNode (Constructor Int) [] [("value",[])]) (num.brat_globals_Nat_1,BratNode (Constructor Nat) [] [("value",[])]) -(num.brat_globals_decl_2_n,BratNode Id [("_0",Nat)] [("_0",Nat)]) -(num.brat_globals_decl_5_m,BratNode Id [("_0",Int)] [("_0",Int)]) +(num.brat_globals_decl_2_n,BratNode Id [("0",Nat)] [("0",Nat)]) +(num.brat_globals_decl_5_m,BratNode Id [("0",Int)] [("0",Int)]) Wires: (Ex num.brat_check_defs_1_m_2_$rhs_check'Con_const_2 0,Int,In num.brat_check_defs_1_m_2_$rhs_check'Con_doub_1 0) diff --git a/brat/test/golden/graph/pair.brat.graph b/brat/test/golden/graph/pair.brat.graph index 065f7796..3c36462d 100644 --- a/brat/test/golden/graph/pair.brat.graph +++ b/brat/test/golden/graph/pair.brat.graph @@ -16,7 +16,7 @@ Nodes: (pair.brat_globals_Int_2,BratNode (Constructor Int) [] [("value",[])]) (pair.brat_globals_cons_1,BratNode (Constructor cons) [("head",[]),("tail",[])] [("value",[])]) (pair.brat_globals_cons_3,BratNode (Constructor cons) [("head",[]),("tail",[])] [("value",[])]) -(pair.brat_globals_decl_6_xs,BratNode Id [("_0",[Int,Bool])] [("_0",[Int,Bool])]) +(pair.brat_globals_decl_6_xs,BratNode Id [("0",[Int,Bool])] [("0",[Int,Bool])]) (pair.brat_globals_nil_5,BratNode (Constructor nil) [] [("value",[])]) Wires: diff --git a/brat/test/golden/graph/rx.brat.graph b/brat/test/golden/graph/rx.brat.graph index 38869cc3..3c857524 100644 --- a/brat/test/golden/graph/rx.brat.graph +++ b/brat/test/golden/graph/rx.brat.graph @@ -13,7 +13,7 @@ Nodes: (rx.brat_check_defs_1_nums_$rhs_const,BratNode (Const 1) [] [("value",Int)]) (rx.brat_check_defs_1_nums_$rhs_const_1,BratNode (Const 2) [] [("value",Int)]) (rx.brat_check_defs_1_nums_$rhs_const_2,BratNode (Const 3) [] [("value",Int)]) -(rx.brat_check_defs_1_xish_1_$rhs_Eval,BratNode (Eval (Ex rx.brat_globals_prim_7_Rx 0)) [("th",Float)] [("_1",{ (rxa :: Qubit) -o (rxb :: Qubit) })]) +(rx.brat_check_defs_1_xish_1_$rhs_Eval,BratNode (Eval (Ex rx.brat_globals_prim_7_Rx 0)) [("th",Float)] [("1",{ (rxa :: Qubit) -o (rxb :: Qubit) })]) (rx.brat_check_defs_1_xish_1_$rhs_const_1,BratNode (Const 30.0) [] [("value",Float)]) (rx.brat_globals_Float_2,BratNode (Constructor Float) [] [("value",[])]) (rx.brat_globals_Int_9,BratNode (Constructor Int) [] [("value",[])]) @@ -26,9 +26,9 @@ Nodes: (rx.brat_globals_Qubit_21,BratNode (Constructor Qubit) [] [("value",[])]) (rx.brat_globals_Qubit_23,BratNode (Constructor Qubit) [] [("value",[])]) (rx.brat_globals_decl_12_nums,BratNode Id [("x",Int),("y",Int),("z",Int)] [("x",Int),("y",Int),("z",Int)]) -(rx.brat_globals_decl_18_xish,BratNode Id [("_0",{ (rxa :: Qubit) -o (rxb :: Qubit) })] [("_0",{ (rxa :: Qubit) -o (rxb :: Qubit) })]) -(rx.brat_globals_decl_24_main,BratNode Id [("_0",{ (a :: Qubit) -o (b :: Qubit) })] [("_0",{ (a :: Qubit) -o (b :: Qubit) })]) -(rx.brat_globals_prim_7_Rx,BratNode (Prim ("","Rx")) [] [("thunk",{ (th :: Float) -> (_1 :: { (rxa :: Qubit) -o (rxb :: Qubit) }) })]) +(rx.brat_globals_decl_18_xish,BratNode Id [("0",{ (rxa :: Qubit) -o (rxb :: Qubit) })] [("0",{ (rxa :: Qubit) -o (rxb :: Qubit) })]) +(rx.brat_globals_decl_24_main,BratNode Id [("0",{ (a :: Qubit) -o (b :: Qubit) })] [("0",{ (a :: Qubit) -o (b :: Qubit) })]) +(rx.brat_globals_prim_7_Rx,BratNode (Prim ("","Rx")) [] [("thunk",{ (th :: Float) -> (1 :: { (rxa :: Qubit) -o (rxb :: Qubit) }) })]) Wires: (Ex rx.brat_check_defs_1_main_3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_Splice 0,Qubit,In rx.brat_check_defs_1_main_3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/out_2 0) diff --git a/brat/test/golden/graph/swap.brat.graph b/brat/test/golden/graph/swap.brat.graph index 876ad656..9b2d49dc 100644 --- a/brat/test/golden/graph/swap.brat.graph +++ b/brat/test/golden/graph/swap.brat.graph @@ -13,7 +13,7 @@ Nodes: (swap.brat_globals_Qubit_3,BratNode (Constructor Qubit) [] [("value",[])]) (swap.brat_globals_Qubit_5,BratNode (Constructor Qubit) [] [("value",[])]) (swap.brat_globals_Qubit_6,BratNode (Constructor Qubit) [] [("value",[])]) -(swap.brat_globals_decl_7_main,BratNode Id [("_0",{ (a :: Qubit), (b :: Qubit) -o (b :: Qubit), (a :: Qubit) })] [("_0",{ (a :: Qubit), (b :: Qubit) -o (b :: Qubit), (a :: Qubit) })]) +(swap.brat_globals_decl_7_main,BratNode Id [("0",{ (a :: Qubit), (b :: Qubit) -o (b :: Qubit), (a :: Qubit) })] [("0",{ (a :: Qubit), (b :: Qubit) -o (b :: Qubit), (a :: Qubit) })]) Wires: (Ex swap.brat_check_defs_1_main_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/in_1 0,Qubit,In swap.brat_check_defs_1_main_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/out_2 1) diff --git a/brat/test/golden/graph/two.brat.graph b/brat/test/golden/graph/two.brat.graph index 3722863d..75211eab 100644 --- a/brat/test/golden/graph/two.brat.graph +++ b/brat/test/golden/graph/two.brat.graph @@ -8,7 +8,7 @@ Nodes: (two.brat_globals_Int_7,BratNode (Constructor Int) [] [("value",[])]) (two.brat_globals_Int_10,BratNode (Constructor Int) [] [("value",[])]) (two.brat_globals_decl_8_one,BratNode Id [("n",Int)] [("n",Int)]) -(two.brat_globals_decl_11_two,BratNode Id [("_0",Int)] [("_0",Int)]) +(two.brat_globals_decl_11_two,BratNode Id [("0",Int)] [("0",Int)]) (two.brat_globals_prim_5_add,BratNode (Prim ("","add")) [] [("thunk",{ (a :: Int), (b :: Int) -> (c :: Int) })]) Wires: diff --git a/brat/test/golden/graph/vec.brat.graph b/brat/test/golden/graph/vec.brat.graph index 719e888a..7d64668f 100644 --- a/brat/test/golden/graph/vec.brat.graph +++ b/brat/test/golden/graph/vec.brat.graph @@ -27,7 +27,7 @@ Nodes: (vec.brat_globals_Int_2,BratNode (Constructor Int) [] [("value",[])]) (vec.brat_globals_Vec_1,BratNode (Constructor Vec) [("X",[]),("n",Nat)] [("value",[])]) (vec.brat_globals_const_3,BratNode (Const 3) [] [("value",Nat)]) -(vec.brat_globals_decl_4_xs,BratNode Id [("_0",Vec(Int, 3))] [("_0",Vec(Int, 3))]) +(vec.brat_globals_decl_4_xs,BratNode Id [("0",Vec(Int, 3))] [("0",Vec(Int, 3))]) Wires: (Ex vec.brat_check_defs_1_xs_$rhs_check'Con__2 0,[],In vec.brat_check_defs_1_xs_$rhs_check'Con_$!_pat2val 0) diff --git a/brat/test/golden/kernel/kernel_application.brat.golden b/brat/test/golden/kernel/kernel_application.brat.golden index 0e8f7657..d95fc0fd 100644 --- a/brat/test/golden/kernel/kernel_application.brat.golden +++ b/brat/test/golden/kernel/kernel_application.brat.golden @@ -2,5 +2,5 @@ Error in test/golden/kernel/kernel_application.brat on line 16: rotate = { q => maybeRotate(true) } ^^^^^^^^^^^ - Type error: Expected a (kernel) function or vector of functions, got { (_0 :: Bool) -> (_1 :: { (_0 :: Qubit) -o (_0 :: Qubit) }) } + Type error: Expected a (kernel) function or vector of functions, got { (0 :: Bool) -> (1 :: { (0 :: Qubit) -o (0 :: Qubit) }) } From 533ea30093d22f7d0b9bc67ab7c8fae2fcd507b5 Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Fri, 15 May 2026 14:01:51 +0100 Subject: [PATCH 08/14] Oops! Update that golden file --- brat/test/golden/error/portpull.brat.golden | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/brat/test/golden/error/portpull.brat.golden b/brat/test/golden/error/portpull.brat.golden index 5370d8ff..cfe4113b 100644 --- a/brat/test/golden/error/portpull.brat.golden +++ b/brat/test/golden/error/portpull.brat.golden @@ -1,6 +1,6 @@ Error in test/golden/error/portpull.brat on line 6: -id2 = x,y => (id, id)(a1:x, y) - ^^^^^^^^^ +id2 = x,y => (id, id)(z:x, y) + ^^^^^^^^ - Port not found: a1 in (0 :: Nat, 0 :: Nat) + Port not found: z in (0 :: Nat, 0 :: Nat) From 4a3b36bc68ea30c7692a93b5b7c1b000ee80ce6e Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Fri, 15 May 2026 18:03:28 +0100 Subject: [PATCH 09/14] Don't allow generated port names to be pulled --- brat/Brat/Parser.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/brat/Brat/Parser.hs b/brat/Brat/Parser.hs index 619a6ea7..69e58d9c 100644 --- a/brat/Brat/Parser.hs +++ b/brat/Brat/Parser.hs @@ -179,7 +179,7 @@ abstractor = do ps <- many (try portPull) list2Cons (APat x:xs) = PCons x <$> list2Cons xs list2Cons _ = customFailure (Custom "Internal error list2Cons") - portPull = (try port <|> (fmap show <$> number)) <* match PortColon + portPull = port <* match PortColon -- For simplicity, we can say for now that all of our infix vector patterns have -- the same precedence and associate to the right @@ -574,7 +574,7 @@ expr' p = choice $ (try . getParser <$> enumFrom p) ++ [atomExpr] where portPull :: Parser (WC String) portPull = do - WC portFC portName <- try port <|> (fmap show <$> number) + WC portFC portName <- port WC colonFC _ <- matchFC PortColon pure (WC (spanFC portFC colonFC) portName) From 9059363d6533f42ee9f2c41916a9ac8985fb9d9d Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Fri, 15 May 2026 18:06:39 +0100 Subject: [PATCH 10/14] Update port pulling test --- brat/test/golden/error/portpull-ambiguous.brat | 6 +++--- brat/test/golden/error/portpull-ambiguous.brat.golden | 4 ++-- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/brat/test/golden/error/portpull-ambiguous.brat b/brat/test/golden/error/portpull-ambiguous.brat index 7b12d08d..86f8efbe 100644 --- a/brat/test/golden/error/portpull-ambiguous.brat +++ b/brat/test/golden/error/portpull-ambiguous.brat @@ -1,6 +1,6 @@ -id(Nat) -> Nat +id(n :: Nat) -> Nat id = x => x --- This should fail because there are multiple ports called "0" +-- This should fail because there are multiple ports called "n" id2(Nat, Nat) -> Nat, Nat -id2 = x, y => (id,id)(0:x, y) +id2 = x, y => (id,id)(n:x, y) diff --git a/brat/test/golden/error/portpull-ambiguous.brat.golden b/brat/test/golden/error/portpull-ambiguous.brat.golden index cce16f33..8aa71374 100644 --- a/brat/test/golden/error/portpull-ambiguous.brat.golden +++ b/brat/test/golden/error/portpull-ambiguous.brat.golden @@ -1,6 +1,6 @@ Error in test/golden/error/portpull-ambiguous.brat on line 6: -id2 = x, y => (id,id)(0:x, y) +id2 = x, y => (id,id)(n:x, y) ^^^^^^^^ - Port 0 is ambiguous in (0 :: Nat, 0 :: Nat) + Port n is ambiguous in (n :: Nat, n :: Nat) From 868db16a11ed2a1762984f517def9d4f4d5bd7df Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Fri, 15 May 2026 18:14:01 +0100 Subject: [PATCH 11/14] Another instance of `Solution Brat` Co-authored-by: Alan Lawrence --- brat/Brat/Checker.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/brat/Brat/Checker.hs b/brat/Brat/Checker.hs index c3c2a9a7..4942e0ff 100644 --- a/brat/Brat/Checker.hs +++ b/brat/Brat/Checker.hs @@ -793,7 +793,7 @@ checkClause my fnName cty clause = modily my $ do -> Checking (Solution Brat, [((String, TypeKind), Val Z)]) postProcessSolAndOuts sol outputs = worker B0 sol where - worker :: Bwd (String, (Src, BinderType Brat)) -> Solution 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) From 49528c5dcb448ab4f1111c8f220b4e48fe204fa2 Mon Sep 17 00:00:00 2001 From: Alan Lawrence Date: Fri, 15 May 2026 18:34:34 +0100 Subject: [PATCH 12/14] Drop Elaboratable. elabIO is fine, but elaborateKindOrFlat needs renaming --- brat/Brat/Elaborator.hs | 31 +++++++++++-------------------- 1 file changed, 11 insertions(+), 20 deletions(-) diff --git a/brat/Brat/Elaborator.hs b/brat/Brat/Elaborator.hs index 2a411a97..dc0319ec 100644 --- a/brat/Brat/Elaborator.hs +++ b/brat/Brat/Elaborator.hs @@ -179,7 +179,7 @@ elaborate' (FAnnotation a ts) = do (SomeRaw a) <- elaborate a a <- assertChk a a <- assertNoun a - ts <- fmap (fmap unWC) <$> elabSig ts + ts <- fmap (fmap unWC) <$> elabIO ts pure $ SomeRaw' (a ::::: ts) elaborate' (FInto a b) = elaborate' (FApp b a) elaborate' (FOf n e) = do @@ -188,8 +188,8 @@ elaborate' (FOf n e) = do SomeRaw e <- elaborate e e <- assertNoun e pure $ SomeRaw' (ROf n e) -elaborate' (FFn cty) = SomeRaw' . RFn . fmap (fmap unWC) <$> traverse (traverse elab) cty -elaborate' (FKernel cty) = SomeRaw' . RKernel . fmap (fmap unWC) <$> traverse (traverse elab) cty +elaborate' (FFn cty) = SomeRaw' . RFn . fmap (fmap unWC) <$> traverse (traverse elaborateKindOrFlat) cty +elaborate' (FKernel cty) = SomeRaw' . RKernel . fmap (fmap unWC) <$> traverse (traverse elaborateChkNoun) cty elaborate' FIdentity = pure $ SomeRaw' RIdentity -- We catch underscores in the top-level elaborate so this case -- should never be triggered @@ -197,24 +197,15 @@ elaborate' FUnderscore = Left (dumbErr (InternalError "Unexpected '_'")) elaborate' FFanOut = pure $ SomeRaw' RFanOut elaborate' FFanIn = pure $ SomeRaw' RFanIn -class Elaboratable t where - type Elaborated t - elab :: WC t -> Either Error (WC (Elaborated t)) +elaborateKindOrFlat :: WC (KindOr Flat) -> Either Error (WC (KindOr (Raw Chk Noun))) +elaborateKindOrFlat (WC fc (Left k)) = pure (WC fc (Left k)) +elaborateKindOrFlat (WC fc (Right ty)) = fmap Right <$> elaborateChkNoun (WC fc ty) --- This is a hack to make elabSig nice -instance Elaboratable Flat where - type Elaborated Flat = Raw Chk Noun - elab = elaborateChkNoun +elabSig :: [TypeRowElem (WC Flat)] -> Either Error [TypeRowElem (WC (Raw Chk Noun))] +elabSig = traverse (traverse elaborateChkNoun) -instance Elaboratable t => Elaboratable (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) - -elabSig :: Elaboratable t - => [TypeRowElem (WC t)] - -> Either Error [TypeRowElem (WC (Elaborated t))] -elabSig = traverse (traverse elab) +elabIO :: [FlatIO] -> Either Error [TypeRowElem (WC (KindOr (Raw Chk Noun)))] +elabIO = traverse (traverse elaborateKindOrFlat) elabBody :: FBody -> FC -> Either Error (FunBody Raw Noun) elabBody (FClauses cs) fc = ThunkOf . WC fc . Clauses <$> traverse elab1Clause cs @@ -237,7 +228,7 @@ elabBody FUndefined _ = pure Undefined elabFunDecl :: FDecl -> Either Error RawFuncDecl elabFunDecl d = do rc <- elabBody (fnBody d) (fnLoc d) - sig <- elabSig (fnSig d) + sig <- elabIO (fnSig d) pure $ FuncDecl { fnName = fnName d , fnLoc = fnLoc d From 11229de6397d95a9b82e2787e31394cd07d7d0e7 Mon Sep 17 00:00:00 2001 From: Alan Lawrence Date: Fri, 15 May 2026 18:38:54 +0100 Subject: [PATCH 13/14] generalize elabSig + elabIO over Traversable, remove the other double-traverse's --- brat/Brat/Elaborator.hs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/brat/Brat/Elaborator.hs b/brat/Brat/Elaborator.hs index dc0319ec..a7bb1294 100644 --- a/brat/Brat/Elaborator.hs +++ b/brat/Brat/Elaborator.hs @@ -188,8 +188,8 @@ elaborate' (FOf n e) = do SomeRaw e <- elaborate e e <- assertNoun e pure $ SomeRaw' (ROf n e) -elaborate' (FFn cty) = SomeRaw' . RFn . fmap (fmap unWC) <$> traverse (traverse elaborateKindOrFlat) cty -elaborate' (FKernel cty) = SomeRaw' . RKernel . fmap (fmap unWC) <$> traverse (traverse elaborateChkNoun) cty +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 @@ -201,10 +201,10 @@ elaborateKindOrFlat :: WC (KindOr Flat) -> Either Error (WC (KindOr (Raw Chk Nou elaborateKindOrFlat (WC fc (Left k)) = pure (WC fc (Left k)) elaborateKindOrFlat (WC fc (Right ty)) = fmap Right <$> elaborateChkNoun (WC fc ty) -elabSig :: [TypeRowElem (WC Flat)] -> Either Error [TypeRowElem (WC (Raw Chk Noun))] +elabSig :: Traversable t => t (TypeRowElem (WC Flat)) -> Either Error (t (TypeRowElem (WC (Raw Chk Noun)))) elabSig = traverse (traverse elaborateChkNoun) -elabIO :: [FlatIO] -> Either Error [TypeRowElem (WC (KindOr (Raw Chk Noun)))] +elabIO :: Traversable t => t FlatIO -> Either Error (t (TypeRowElem (WC (KindOr (Raw Chk Noun))))) elabIO = traverse (traverse elaborateKindOrFlat) elabBody :: FBody -> FC -> Either Error (FunBody Raw Noun) From 3d751e6ab481a6fd04ceaf28cf261e398e5fad3a Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Fri, 29 May 2026 11:07:13 +0100 Subject: [PATCH 14/14] elaborateKindOrFlat -> elaborateBratType --- brat/Brat/Elaborator.hs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/brat/Brat/Elaborator.hs b/brat/Brat/Elaborator.hs index a7bb1294..caec11f1 100644 --- a/brat/Brat/Elaborator.hs +++ b/brat/Brat/Elaborator.hs @@ -197,15 +197,15 @@ elaborate' FUnderscore = Left (dumbErr (InternalError "Unexpected '_'")) elaborate' FFanOut = pure $ SomeRaw' RFanOut elaborate' FFanIn = pure $ SomeRaw' RFanIn -elaborateKindOrFlat :: WC (KindOr Flat) -> Either Error (WC (KindOr (Raw Chk Noun))) -elaborateKindOrFlat (WC fc (Left k)) = pure (WC fc (Left k)) -elaborateKindOrFlat (WC fc (Right ty)) = fmap Right <$> elaborateChkNoun (WC fc ty) +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 elaborateKindOrFlat) +elabIO = traverse (traverse elaborateBratType) elabBody :: FBody -> FC -> Either Error (FunBody Raw Noun) elabBody (FClauses cs) fc = ThunkOf . WC fc . Clauses <$> traverse elab1Clause cs