diff --git a/brat/Brat/Checker.hs b/brat/Brat/Checker.hs index 2c7508e1..4942e0ff 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,10 +789,11 @@ checkClause my fnName cty clause = modily my $ do (Some stk) <><< (x:xs) = Some (stk :<< x) <><< xs -- Process a solution, finding Ends that support the solved types, and return a list of definitions for substituting later on - postProcessSolAndOuts :: [(String, (Src, BinderType Brat))] -> [(Tgt, BinderType Brat)] -> Checking ([(String, (Src, BinderType Brat))], [((String, TypeKind), Val Z)]) + postProcessSolAndOuts :: Solution Brat -> [(Tgt, BinderType Brat)] + -> Checking (Solution Brat, [((String, TypeKind), Val Z)]) postProcessSolAndOuts sol outputs = worker B0 sol where - worker :: Bwd (String, (Src, BinderType Brat)) -> [(String, (Src, BinderType Brat))] -> Checking ([(String, (Src, BinderType Brat))], [((String, TypeKind), Val Z)]) + worker :: Bwd (String, (Src, BinderType Brat)) -> Solution Brat -> Checking (Solution Brat, [((String, TypeKind), Val Z)]) worker zx [] = (, []) <$> outputDeps zx [] outputs worker zx (entry@(patVar, (src, Left k)):sol) = let vsrc = VApp (VPar (toEnd src)) B0 in do trackM ("processSol (kinded): " ++ show entry) @@ -1049,7 +1050,7 @@ kindCheck ((_, k):_) tm = typeErr $ "Expected " ++ show tm ++ " to have kind " + -- Checks the kinds of the types in a dependent row kindCheckRow :: Modey m -> String -- for node name - -> [(PortName, ThunkRowType m)] -- The row to process + -> [TypeRowElem (ThunkRowType m)] -- The row to process -> Checking (Some (Ro m Z)) kindCheckRow my name r = do name <- req $ Fresh $ "__kcr_" ++ name @@ -1060,7 +1061,7 @@ kindCheckRow my name r = do -- evaluation of the type of an Id node passing through such values kindCheckAnnotation :: Modey m -> String -- for node name - -> [(PortName, ThunkRowType m)] + -> [TypeRowElem (ThunkRowType m)] -> Checking (CTy m Z) kindCheckAnnotation my name outs = do trackM "kca" @@ -1080,17 +1081,19 @@ kindCheckRow' :: forall m n -> Endz n -- kind outports so far -> VEnv -- from string variable names to VPar's -> (Name, Int) -- node name and next free input (under to 'kindCheck' a type) - -> [(PortName, ThunkRowType m)] + -> [TypeRowElem (ThunkRowType m)] -> Checking (Int, VEnv, Some (Endz :* Ro m n)) kindCheckRow' _ ez env (_,i) [] = pure (i, env, Some (ez :* R0)) -kindCheckRow' Braty (ny :* s) env (name,i) ((p, Left k):rest) = do -- s is Stack Z n + +kindCheckRow' my nys env (name, i) ((Anon ty):rest) = kindCheckRow' my nys env (name, i) ((Named (show i) ty):rest) +kindCheckRow' Braty (ny :* s) env (name,i) ((Named p (Left k)):rest) = do -- s is Stack Z n let dangling = Ex name (ny2int ny) req (Declare (ExEnd dangling) Braty (Left k) Definable) -- assume none are SkolemConst?? env <- pure $ M.insert (plain p) [(NamedPort dangling p, Left k)] env (i, env, ser) <- kindCheckRow' Braty (Sy ny :* (s :<< ExEnd dangling)) env (name, i) rest case ser of Some (s_m :* ro) -> pure (i, env, Some (s_m :* REx (p,k) ro)) -kindCheckRow' my ez@(ny :* s) env (name, i) ((p, bty):rest) = case (my, bty) of +kindCheckRow' my ez@(ny :* s) env (name, i) ((Named p bty):rest) = case (my, bty) of (Braty, Right ty) -> helper ty (Star []) (Kerny, ty) -> helper ty (Dollar []) diff --git a/brat/Brat/Checker/Helpers.hs b/brat/Brat/Checker/Helpers.hs index 0e580768..8b37a57e 100644 --- a/brat/Brat/Checker/Helpers.hs +++ b/brat/Brat/Checker/Helpers.hs @@ -110,13 +110,7 @@ pullPortsRow :: Show ty -> Checking [(NamedPort e, ty)] pullPortsRow = pullPorts (portName . fst) showRow -pullPortsSig :: Show ty - => [PortName] - -> [(PortName, ty)] - -> Checking [(PortName, ty)] -pullPortsSig = pullPorts fst showSig - -pullPorts :: forall a +pullPorts :: forall a ty . (a -> PortName) -- A way to get a port name for each element -> ([a] -> String) -- A way to print the list -> [PortName] -- Things to pull to the front @@ -134,10 +128,7 @@ pullPorts toPort showFn to_pull types = ensureEmpty :: Show ty => String -> [(NamedPort e, ty)] -> Checking () ensureEmpty _ [] = pure () -ensureEmpty str xs = err $ InternalError $ "Expected empty " ++ str ++ ", got:\n " ++ showSig (rowToSig xs) - -rowToSig :: Traversable t => t (NamedPort e, ty) -> t (PortName, ty) -rowToSig = fmap $ first portName +ensureEmpty str xs = err $ InternalError $ "Expected empty " ++ str ++ ", got:\n " ++ showRow xs showMode :: Modey m -> String showMode Braty = "" @@ -151,14 +142,17 @@ type family ThunkRowType (m :: Mode) where ThunkRowType Brat = KindOr (Term Chk Noun) ThunkRowType Kernel = Term Chk Noun +simpleTypeRow :: [(PortName, ty)] -> [TypeRowElem ty] +simpleTypeRow = fmap (uncurry Named) + mkThunkTy :: Modey m -> ThunkFCType m -> [(PortName, ThunkRowType m)] -> [(PortName, ThunkRowType m)] -> Term Chk Noun -- mkThunkTy Braty fc ss ts = C (WC fc (ss :-> ts)) -mkThunkTy Braty _ ss ts = C (ss :-> ts) -mkThunkTy Kerny () ss ts = K (ss :-> ts) +mkThunkTy Braty _ ss ts = C (simpleTypeRow ss :-> simpleTypeRow ts) +mkThunkTy Kerny () ss ts = K (simpleTypeRow ss :-> simpleTypeRow ts) anext :: forall m i j k . EvMode m 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 diff --git a/brat/Brat/Elaborator.hs b/brat/Brat/Elaborator.hs index 2546dca3..caec11f1 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) <$> elabIO ts pure $ SomeRaw' (a ::::: ts) elaborate' (FInto a b) = elaborate' (FApp b a) elaborate' (FOf n e) = do @@ -187,8 +188,8 @@ elaborate' (FOf n e) = do SomeRaw e <- elaborate e e <- assertNoun e pure $ SomeRaw' (ROf n e) -elaborate' (FFn cty) = pure $ SomeRaw' (RFn cty) -elaborate' (FKernel sty) = pure $ SomeRaw' (RKernel sty) +elaborate' (FFn cty) = SomeRaw' . RFn . fmap (fmap unWC) <$> elabIO cty +elaborate' (FKernel cty) = SomeRaw' . RKernel . fmap (fmap unWC) <$> elabSig cty elaborate' FIdentity = pure $ SomeRaw' RIdentity -- We catch underscores in the top-level elaborate so this case -- should never be triggered @@ -196,6 +197,16 @@ elaborate' FUnderscore = Left (dumbErr (InternalError "Unexpected '_'")) elaborate' FFanOut = pure $ SomeRaw' RFanOut elaborate' FFanIn = pure $ SomeRaw' RFanIn +elaborateBratType :: WC (KindOr Flat) -> Either Error (WC (KindOr (Raw Chk Noun))) +elaborateBratType (WC fc (Left k)) = pure (WC fc (Left k)) +elaborateBratType (WC fc (Right ty)) = fmap Right <$> elaborateChkNoun (WC fc ty) + +elabSig :: Traversable t => t (TypeRowElem (WC Flat)) -> Either Error (t (TypeRowElem (WC (Raw Chk Noun)))) +elabSig = traverse (traverse elaborateChkNoun) + +elabIO :: Traversable t => t FlatIO -> Either Error (t (TypeRowElem (WC (KindOr (Raw Chk Noun))))) +elabIO = traverse (traverse elaborateBratType) + elabBody :: FBody -> FC -> Either Error (FunBody Raw Noun) elabBody (FClauses cs) fc = ThunkOf . WC fc . Clauses <$> traverse elab1Clause cs where @@ -217,14 +228,17 @@ elabBody FUndefined _ = pure Undefined elabFunDecl :: FDecl -> Either Error RawFuncDecl elabFunDecl d = do rc <- elabBody (fnBody d) (fnLoc d) + sig <- elabIO (fnSig d) pure $ FuncDecl { fnName = fnName d , fnLoc = fnLoc d - , fnSig = fnSig d + , fnSig = fmap unWC <$> sig -- sus , fnBody = rc , fnLocality = fnLocality d } +elabAlias :: FAlias -> Either Error RawAlias +elabAlias (TypeAlias fc name tys tm) = TypeAlias fc name tys . unWC <$> elaborateChkNoun (WC fc tm) elabEnv :: FEnv -> Either Error RawEnv -elabEnv (ds, x) = (,x,empty) <$> forM ds elabFunDecl +elabEnv (ds, as) = (,,empty) <$> traverse elabFunDecl ds <*> traverse elabAlias as diff --git a/brat/Brat/Parser.hs b/brat/Brat/Parser.hs index 33875be5..8214e596 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 ((**^)) @@ -260,59 +258,56 @@ 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 (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 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 @@ -343,15 +338,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' match Lolly - ts <- rawIO' (unWC <$> vtype) + ts <- flatIO' pure $ FKernel (ss :-> ts) @@ -516,7 +511,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 @@ -595,27 +590,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 @@ -629,9 +611,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) @@ -736,11 +718,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 @@ -781,31 +763,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' match Lolly - WC endFC outs <- spanningFC =<< rawIO' vtype + WC endFC outs <- spanningFC =<< flatIO' 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..a8065755 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,17 @@ instance Show Import where showSelection (ImportPartial fns) = "(":(unWC <$> fns) ++ [")"] showSelection (ImportHiding fns) = "hiding (":(unWC <$> fns) ++ [")"] -showSig :: Show ty => [(String, ty)] -> String -showSig [] = "()" -showSig (x:xs) - = intercalate ", " [ '(':p ++ " :: " ++ show ty ++ ")" - | (p, ty) <- x:xs] +showSig :: (Show ty) => [TypeRowElem ty] -> String +showSig xs = parens $ intercalate ", " (showElem <$> xs) + 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 +231,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..32a29b15 100644 --- a/brat/Brat/Syntax/Core.hs +++ b/brat/Brat/Syntax/Core.hs @@ -1,9 +1,6 @@ module Brat.Syntax.Core (Term(..) - ,Input - ,Output ,InOut ,CType - ,CoreFuncDecl ,Precedence(..) ,precedence ) where @@ -17,20 +14,15 @@ 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) import Data.Maybe (fromJust) -type Input = InOut -type Output = InOut 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 +46,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 +59,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..f7115982 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,16 +230,10 @@ 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) - desugar' (ss :-> ts) = do - ss <- traverse desugar' (addNames ss) - ts <- traverse desugar' (addNames ts) - pure (ss :-> ts) + type Desugared (CType' (TypeRowElem RawVType)) = CType' (TypeRowElem (Term Chk Noun)) + desugar' :: CType' (TypeRowElem RawVType) -> Desugar (CType' (TypeRowElem (Term Chk Noun))) + desugar' cty = traverse desugar' cty isConOrAlias :: QualName -> Desugar Bool isConOrAlias c = do @@ -283,27 +256,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 +281,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..a4c9368e 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,25 @@ 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) (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) 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..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: - (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..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: (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..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: (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..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: (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..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: (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..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: (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 b/brat/test/golden/error/portpull-ambiguous.brat index 237c6fc2..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 "a1" +-- This should fail because there are multiple ports called "n" id2(Nat, Nat) -> Nat, Nat -id2 = x, y => (id,id)(a1: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 bc45791d..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)(a1:x, y) - ^^^^^^^^^ +id2 = x, y => (id,id)(n:x, y) + ^^^^^^^^ - Port a1 is ambiguous in (a1 :: Nat), (a1 :: Nat) + Port n is ambiguous in (n :: Nat, n :: 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 f6a2fd2a..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 a1 is ambiguous in (a1 :: Nat), (a1 :: Nat) + Port not found: z 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..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 :: (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..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: (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..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: (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..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 (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..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: (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..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: (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..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")) [] [("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..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 [("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..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 [("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..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 [] [("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..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 [("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..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 [("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..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 [("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..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)] [("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..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 [("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..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 [("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..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 [("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..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 { (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) }) }