From 7458577b334b5d41e8a1cb8af9990d2e321265eb Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Mon, 25 Nov 2024 17:09:30 +0000 Subject: [PATCH] refactor: Rename UserName to QualName (#56) --- brat/Brat/Checker.hs | 32 +++++++++++++------- brat/Brat/Checker/Helpers.hs | 13 +------- brat/Brat/Checker/Monad.hs | 42 +++++++++++++------------- brat/Brat/Checker/SolvePatterns.hs | 8 ++--- brat/Brat/Checker/Types.hs | 4 +-- brat/Brat/Compile/Hugr.hs | 10 +++--- brat/Brat/Constructors.hs | 12 ++++---- brat/Brat/Constructors/Patterns.hs | 8 ++--- brat/Brat/Eval.hs | 2 +- brat/Brat/Graph.hs | 10 +++--- brat/Brat/Load.hs | 20 ++++++------ brat/Brat/Parser.hs | 24 ++++++++------- brat/Brat/{UserName.hs => QualName.hs} | 9 +++--- brat/Brat/Search.hs | 2 +- brat/Brat/Syntax/Abstractor.hs | 4 +-- brat/Brat/Syntax/Common.hs | 4 +-- brat/Brat/Syntax/Concrete.hs | 6 ++-- brat/Brat/Syntax/Core.hs | 6 ++-- brat/Brat/Syntax/Raw.hs | 18 +++++------ brat/Brat/Syntax/Value.hs | 8 ++--- brat/brat.cabal | 2 +- brat/test/Test/Elaboration.hs | 2 +- brat/test/Test/Substitution.hs | 2 +- brat/test/Test/Syntax/Let.hs | 4 +-- 24 files changed, 126 insertions(+), 126 deletions(-) rename brat/Brat/{UserName.hs => QualName.hs} (56%) diff --git a/brat/Brat/Checker.hs b/brat/Brat/Checker.hs index 0e213fc2..43524983 100644 --- a/brat/Brat/Checker.hs +++ b/brat/Brat/Checker.hs @@ -13,11 +13,12 @@ import Control.Monad.Freer import Data.Bifunctor import Data.Foldable (for_) import Data.Functor (($>), (<&>)) -import Data.List ((\\)) +import Data.List ((\\), intercalate) import Data.List.NonEmpty (NonEmpty(..)) import qualified Data.List.NonEmpty as NE import qualified Data.Map as M import Data.Maybe (fromJust) +import qualified Data.Set as S import Data.Type.Equality ((:~:)(..)) import Prelude hiding (filter) @@ -33,6 +34,7 @@ import Brat.FC hiding (end) import qualified Brat.FC as FC import Brat.Graph import Brat.Naming +import Brat.QualName -- import Brat.Search import Brat.Syntax.Abstractor (NormalisedAbstractor(..), normaliseAbstractor) import Brat.Syntax.Common @@ -41,7 +43,6 @@ import Brat.Syntax.FuncDecl (FunBody(..)) import Brat.Syntax.Port (ToEnd, toEnd) import Brat.Syntax.Simple import Brat.Syntax.Value -import Brat.UserName import Bwd import Hasochism import Util (zipSameLength) @@ -55,6 +56,15 @@ standardise k val = eval S0 val >>= (\case mergeEnvs :: [Env a] -> Checking (Env a) mergeEnvs = foldM combineDisjointEnvs M.empty + where + combineDisjointEnvs :: M.Map QualName v -> M.Map QualName v -> Checking (M.Map QualName v) + combineDisjointEnvs l r = + let commonKeys = S.intersection (M.keysSet l) (M.keysSet r) + in if S.null commonKeys + then pure $ M.union l r + else typeErr ("Variable(s) defined twice: " ++ + intercalate "," (map show $ S.toList commonKeys)) + singletonEnv :: (?my :: Modey m) => String -> (Src, BinderType m) -> Checking (Env (EnvData m)) singletonEnv x input@(p, ty) = case ?my of @@ -247,7 +257,7 @@ check' (Lambda c@(WC abstFC abst, body) cs) (overs, unders) = do -- N.B.: Here we update the port names to be the user variable names for nicer -- error messages. This mirrors previous behaviour using `abstract`, but is a -- bit of a hack. See issue #23. - solToEnv :: [(String, (Src, BinderType m))] -> Checking (M.Map UserName (EnvData m)) + solToEnv :: [(String, (Src, BinderType m))] -> Checking (M.Map QualName (EnvData m)) solToEnv xs = traverse (uncurry singletonEnv) (portNamesToBoundNames xs) >>= mergeEnvs portNamesToBoundNames :: [(String, (Src, BinderType m))] -> [(String, (Src, BinderType m))] @@ -411,7 +421,7 @@ check' (NHole (mnemonic, name)) connectors = do let ss = intercalate ", " . fmap show <$> sugg pure $ take 5 (ms ++ ss) - findMatchingNouns :: Checking [[UserName]] + findMatchingNouns :: Checking [[QualName]] findMatchingNouns = do -- TODO pure [] @@ -443,7 +453,7 @@ check' tm@(Con vcon vargs) ((), (hungry, ty):unders) = case (?my, ty) of (Braty, Right ty) -> aux Braty clup ty $> (((), ()), ((), unders)) (Kerny, _) -> aux Kerny kclup ty $> (((), ()), ((), unders)) where - aux :: Modey m -> (UserName -> UserName -> Checking (CtorArgs m)) -> Val Z -> Checking () + aux :: Modey m -> (QualName -> QualName -> Checking (CtorArgs m)) -> Val Z -> Checking () aux my lup ty = do VCon tycon tyargs <- eval S0 ty (CArgs pats nFree _ argTypeRo) <- lup vcon tycon @@ -962,8 +972,8 @@ kindCheckRow' my ez@(ny :* s) env (name, i) ((p, bty):rest) = case (my, bty) of -- Look for vectors to produce better error messages for mismatched lengths -- in terms or patterns. -detectVecErrors :: UserName -- Term constructor name - -> UserName -- Type constructor name +detectVecErrors :: QualName -- Term constructor name + -> QualName -- Type constructor name -> [Val Z] -- Type arguments -> [ValPat] -- Patterns the type arguments are checked against -> Val Z -- Type @@ -1070,13 +1080,13 @@ abstractPattern my (dangling, bty) pat@(PCon pcon abst) = case (my, bty) of helper :: Modey m -> Val Z -> TypeKind - -> (UserName -> UserName -> Checking (CtorArgs m)) + -> (QualName -> QualName -> Checking (CtorArgs m)) -> Checking (Env (EnvData m)) helper my v k lup = standardise k v >>= throwLeft . unpackTypeConstructor >>= abstractCon my lup - unpackTypeConstructor :: Val Z -> Either ErrorMsg (UserName, [Val Z]) + unpackTypeConstructor :: Val Z -> Either ErrorMsg (QualName, [Val Z]) unpackTypeConstructor (VCon tycon tyargs) = pure (tycon, tyargs) unpackTypeConstructor ty = Left (PattErr $ unwords ["Couldn't resolve pattern" ,show pat @@ -1084,8 +1094,8 @@ abstractPattern my (dangling, bty) pat@(PCon pcon abst) = case (my, bty) of ,show ty]) abstractCon :: Modey m - -> (UserName -> UserName -> Checking (CtorArgs m)) - -> (UserName, [Val Z]) + -> (QualName -> QualName -> Checking (CtorArgs m)) + -> (QualName, [Val Z]) -> Checking (Env (EnvData m)) abstractCon my lup (tycon, tyargs) = do let ty = VCon tycon tyargs diff --git a/brat/Brat/Checker/Helpers.hs b/brat/Brat/Checker/Helpers.hs index 5e609f14..f07fe96c 100644 --- a/brat/Brat/Checker/Helpers.hs +++ b/brat/Brat/Checker/Helpers.hs @@ -32,17 +32,14 @@ import Brat.Syntax.Core (Term(..)) import Brat.Syntax.Simple import Brat.Syntax.Port (ToEnd(..)) import Brat.Syntax.Value -import Brat.UserName import Bwd import Hasochism import Util (log2) -import Control.Monad.Freer (req, Free(Ret)) +import Control.Monad.Freer (req) import Data.Bifunctor -import Data.List (intercalate) import Data.Type.Equality (TestEquality(..), (:~:)(..)) import qualified Data.Map as M -import qualified Data.Set as S import Prelude hiding (last) simpleCheck :: Modey m -> Val Z -> SimpleTerm -> Either ErrorMsg () @@ -131,14 +128,6 @@ pullPorts toPort showFn (p:ports) types = do else pure (x, xs) | otherwise = second (x:) <$> pull1Port p xs -combineDisjointEnvs :: M.Map UserName v -> M.Map UserName v -> Checking (M.Map UserName v) -combineDisjointEnvs l r = - let commonKeys = S.intersection (M.keysSet l) (M.keysSet r) - in if S.null commonKeys - then Ret $ M.union l r - else typeErr ("Variable(s) defined twice: " ++ - intercalate "," (map show $ S.toList commonKeys)) - ensureEmpty :: Show ty => String -> [(NamedPort e, ty)] -> Checking () ensureEmpty _ [] = pure () ensureEmpty str xs = err $ InternalError $ "Expected empty " ++ str ++ ", got:\n " ++ showSig (rowToSig xs) diff --git a/brat/Brat/Checker/Monad.hs b/brat/Brat/Checker/Monad.hs index 4b219e69..467050f1 100644 --- a/brat/Brat/Checker/Monad.hs +++ b/brat/Brat/Checker/Monad.hs @@ -7,9 +7,9 @@ import Brat.Error (Error(..), ErrorMsg(..), dumbErr) import Brat.FC (FC) import Brat.Graph import Brat.Naming (fresh, split, Name, Namespace, FreshMonad(..)) +import Brat.QualName (QualName) import Brat.Syntax.Common import Brat.Syntax.Value -import Brat.UserName (UserName) import Hasochism import Util @@ -54,8 +54,8 @@ data Context = Ctx { globalVEnv :: VEnv , store :: Store , constructors :: ConstructorMap Brat , kconstructors :: ConstructorMap Kernel - , typeConstructors :: M.Map (Mode, UserName) [(PortName, TypeKind)] - , aliasTable :: M.Map UserName Alias + , typeConstructors :: M.Map (Mode, QualName) [(PortName, TypeKind)] + , aliasTable :: M.Map QualName Alias } data CheckingSig ty where @@ -64,24 +64,24 @@ data CheckingSig ty where Throw :: Error -> CheckingSig a LogHole :: TypedHole -> CheckingSig () AskFC :: CheckingSig FC - VLup :: UserName -> CheckingSig (Maybe [(Src, BinderType Brat)]) - KLup :: UserName -> CheckingSig (Maybe (Src, BinderType Kernel)) + VLup :: QualName -> CheckingSig (Maybe [(Src, BinderType Brat)]) + KLup :: QualName -> CheckingSig (Maybe (Src, BinderType Kernel)) -- Lookup type constructors - TLup :: (Mode, UserName) -> CheckingSig (Maybe [(PortName, TypeKind)]) + TLup :: (Mode, QualName) -> CheckingSig (Maybe [(PortName, TypeKind)]) -- Lookup term constructor - ask whether a constructor builds a certain type CLup :: FC -- File context for error reporting - -> UserName -- Value constructor - -> UserName -- Type constructor + -> QualName -- Value constructor + -> QualName -- Type constructor -> CheckingSig (CtorArgs Brat) -- Lookup kernel constructors KCLup :: FC -- File context for error reporting - -> UserName -- Value constructor - -> UserName -- Type constructor + -> QualName -- Value constructor + -> QualName -- Type constructor -> CheckingSig (CtorArgs Kernel) -- Lookup an end in the Store ELup :: End -> CheckingSig (Maybe (Val Z)) -- Lookup an alias in the table - ALup :: UserName -> CheckingSig (Maybe Alias) + ALup :: QualName -> CheckingSig (Maybe Alias) TypeOf :: End -> CheckingSig EndType AddNode :: Name -> Node -> CheckingSig () Wire :: Wire -> CheckingSig () @@ -90,7 +90,7 @@ data CheckingSig ty where Declare :: End -> Modey m -> BinderType m -> CheckingSig () Define :: End -> Val Z -> CheckingSig () -localAlias :: (UserName, Alias) -> Checking v -> Checking v +localAlias :: (QualName, Alias) -> Checking v -> Checking v localAlias _ (Ret v) = Ret v localAlias con@(name, alias) (Req (ALup u) k) | u == name = localAlias con $ k (Just alias) @@ -124,7 +124,7 @@ captureOuterLocals c = do helper (outerLocals, M.empty) c where helper :: (VEnv, VEnv) -> Checking v - -> Checking (v, M.Map UserName [(Src, BinderType Brat)]) + -> Checking (v, M.Map QualName [(Src, BinderType Brat)]) helper (_, captured) (Ret v) = Ret (v, captured) helper (avail, captured) (Req (VLup x) k) | j@(Just new) <- M.lookup x avail = helper (avail, M.insert x new captured) (k j) @@ -139,29 +139,29 @@ throwLeft :: Either ErrorMsg a -> Checking a throwLeft (Right x) = pure x throwLeft (Left msg) = err msg -vlup :: UserName -> Checking [(Src, BinderType Brat)] +vlup :: QualName -> Checking [(Src, BinderType Brat)] vlup s = do req (VLup s) >>= \case Just vty -> pure vty Nothing -> err $ VarNotFound (show s) -alup :: UserName -> Checking Alias +alup :: QualName -> Checking Alias alup s = do req (ALup s) >>= \case Just vty -> pure vty Nothing -> err $ VarNotFound (show s) -clup :: UserName -- Value constructor - -> UserName -- Type constructor +clup :: QualName -- Value constructor + -> QualName -- Type constructor -> Checking (CtorArgs Brat) clup vcon tycon = req AskFC >>= \fc -> req (CLup fc vcon tycon) -kclup :: UserName -- Value constructor - -> UserName -- Type constructor +kclup :: QualName -- Value constructor + -> QualName -- Type constructor -> Checking (CtorArgs Kernel) kclup vcon tycon = req AskFC >>= \fc -> req (KCLup fc vcon tycon) -tlup :: (Mode, UserName) -> Checking [(PortName, TypeKind)] +tlup :: (Mode, QualName) -> Checking [(PortName, TypeKind)] tlup (m, c) = req (TLup (m, c)) >>= \case Nothing -> req (TLup (otherMode, c)) >>= \case Nothing -> err $ UnrecognisedTypeCon (show c) @@ -172,7 +172,7 @@ tlup (m, c) = req (TLup (m, c)) >>= \case Brat -> Kernel Kernel -> Brat -lookupAndUse :: UserName -> KEnv +lookupAndUse :: QualName -> KEnv -> Either Error (Maybe ((Src, BinderType Kernel), KEnv)) lookupAndUse x kenv = case M.lookup x kenv of Nothing -> Right Nothing diff --git a/brat/Brat/Checker/SolvePatterns.hs b/brat/Brat/Checker/SolvePatterns.hs index 1cdcce76..608f5185 100644 --- a/brat/Brat/Checker/SolvePatterns.hs +++ b/brat/Brat/Checker/SolvePatterns.hs @@ -12,7 +12,7 @@ import Brat.Syntax.Abstractor import Brat.Syntax.Common import Brat.Syntax.Simple import Brat.Syntax.Value -import Brat.UserName +import Brat.QualName import Bwd import Control.Monad.Freer import Hasochism @@ -131,7 +131,7 @@ typeOfEnd my e = req (TypeOf e) >>= \case solveConstructor :: EvMode m => Modey m -> Src - -> (UserName, Abstractor) + -> (QualName, Abstractor) -> Val Z -> Problem -> Checking ([(Src, PrimTest (BinderType m))] @@ -367,11 +367,11 @@ argProblemsWithLeftovers srcs (NA AEmpty) p = pure (p, srcs) argProblemsWithLeftovers [] abst _ = err $ NothingToBind (show abst) lookupConstructor :: Modey m - -> UserName -- A value constructor + -> QualName -- A value constructor -> Val Z -- A corresponding type to normalise -- TODO: Something with this m -> Checking (CtorArgs m -- The needed args to the value constructor - ,(UserName, [Val Z]) -- The type constructor we normalised and its args + ,(QualName, [Val Z]) -- The type constructor we normalised and its args ) lookupConstructor my c ty = eval S0 ty >>= \case (VCon tycon args) -> (,(tycon, args)) <$> case my of diff --git a/brat/Brat/Checker/Types.hs b/brat/Brat/Checker/Types.hs index e2ff5594..9077adb0 100644 --- a/brat/Brat/Checker/Types.hs +++ b/brat/Brat/Checker/Types.hs @@ -14,9 +14,9 @@ module Brat.Checker.Types (Overs, Unders import Brat.Checker.Quantity import Brat.FC (FC) import Brat.Naming (Name) +import Brat.QualName (QualName) import Brat.Syntax.Common import Brat.Syntax.Value -import Brat.UserName (UserName) import Hasochism (N(..)) import Data.Kind (Type) @@ -53,7 +53,7 @@ type family EnvData (m :: Mode) where EnvData Brat = [(Src, BinderType Brat)] EnvData Kernel = (Quantity, (Src, BinderType Kernel)) -type Env e = M.Map UserName e +type Env e = M.Map QualName e type VEnv = Env (EnvData Brat) type KEnv = Env (EnvData Kernel) diff --git a/brat/Brat/Compile/Hugr.hs b/brat/Brat/Compile/Hugr.hs index 3a33c97d..e7be36fd 100644 --- a/brat/Brat/Compile/Hugr.hs +++ b/brat/Brat/Compile/Hugr.hs @@ -16,11 +16,11 @@ import Brat.Checker.Types (Store(..), VEnv) import Brat.Eval (eval, evalCTy, kindType) import Brat.Graph hiding (lookupNode) import Brat.Naming +import Brat.QualName import Brat.Syntax.Port import Brat.Syntax.Common import Brat.Syntax.Simple (SimpleTerm) import Brat.Syntax.Value -import Brat.UserName import Bwd import Control.Monad.Freer import Data.Hugr @@ -487,7 +487,7 @@ compileWithInputs parent name = gets compiled >>= (\case addNode "Replicate" (OpCustom (CustomOp parent "BRAT" "Replicate" sig [TAType elemTy])) x -> error $ show x ++ " should have been compiled outside of compileNode" -compileConstructor :: NodeId -> UserName -> UserName -> FunctionType -> Compile NodeId +compileConstructor :: NodeId -> QualName -> QualName -> FunctionType -> Compile NodeId compileConstructor parent tycon con sig | Just b <- isBool con = do -- A boolean value is a tag which takes no inputs and produces an empty tuple @@ -497,7 +497,7 @@ compileConstructor parent tycon con sig | otherwise = let name = "Constructor " ++ show tycon ++ "::" ++ show con in addNode name (constructorOp parent tycon con sig) where - isBool :: UserName -> Maybe Bool + isBool :: QualName -> Maybe Bool isBool CFalse = Just False isBool CTrue = Just True isBool _ = Nothing @@ -777,7 +777,7 @@ compilePrimTest parent port@(_, ty) (PrimLitTest tm) = do [port, loadPort] [sumOut] -constructorOp :: NodeId -> UserName -> UserName -> FunctionType -> HugrOp NodeId +constructorOp :: NodeId -> QualName -> QualName -> FunctionType -> HugrOp NodeId constructorOp parent tycon c sig = OpCustom (CustomOp parent "BRAT" ("Ctor::" ++ show tycon ++ "::" ++ show c) sig []) undoPrimTest :: NodeId @@ -858,7 +858,7 @@ compileModule venv = do addEdge (fst wire, Port output 0) -- top-level decls that are not Prims. RHS is the brat idNode - decls :: [(UserName, Name)] + decls :: [(QualName, Name)] decls = do -- in list monad, no Compile here (fnName, wires) <- M.toList venv let (Ex idNode _) = end (fst $ head wires) -- would be better to check same for all rather than just head diff --git a/brat/Brat/Constructors.hs b/brat/Brat/Constructors.hs index bd3656fe..16b196bc 100644 --- a/brat/Brat/Constructors.hs +++ b/brat/Brat/Constructors.hs @@ -3,9 +3,9 @@ module Brat.Constructors where import qualified Data.Map as M import Brat.Constructors.Patterns +import Brat.QualName (QualName, plain) import Brat.Syntax.Common import Brat.Syntax.Value -import Brat.UserName (UserName, plain) import Bwd import Hasochism (N(..), Ny(..)) @@ -20,8 +20,8 @@ data CtorArgs m where -> CtorArgs m type ConstructorMap m - = M.Map UserName -- The name of a constructor "C" - (M.Map UserName -- The name of the type we're checking against "Ty" + = M.Map QualName -- The name of a constructor "C" + (M.Map QualName -- The name of the type we're checking against "Ty" (CtorArgs m) ) @@ -125,7 +125,7 @@ kernelConstructors = M.fromList ,(CFalse, M.fromList [(CBit, CArgs [] Zy R0 R0)]) ] -defaultTypeConstructors :: M.Map (Mode, UserName) [(PortName, TypeKind)] +defaultTypeConstructors :: M.Map (Mode, QualName) [(PortName, TypeKind)] defaultTypeConstructors = M.fromList [((Brat, COption), [("value", Star [])]) ,((Brat, CList), [("listValue", Star [])]) @@ -149,7 +149,7 @@ defaultTypeConstructors = M.fromList -- TODO: Make type aliases more flexible. Allow different patterns and allow Nat -- kinds. Allow port pulling when applying them -- TODO: Aliases for kernel types -typeAliases :: M.Map UserName (Modey m, [ValPat], BinderType m) +typeAliases :: M.Map QualName (Modey m, [ValPat], BinderType m) typeAliases = M.empty {- Here is an example, for `type Vec5(X) = Vec(X, n)`: M.fromList $ @@ -160,7 +160,7 @@ M.fromList $ -} -} -natConstructors :: M.Map UserName (Maybe NumPat, NumVal (VVar Z) -> NumVal (VVar Z)) +natConstructors :: M.Map QualName (Maybe NumPat, NumVal (VVar Z) -> NumVal (VVar Z)) natConstructors = M.fromList [(plain "succ", (Just (NP1Plus NPVar) ,nPlus 1)) diff --git a/brat/Brat/Constructors/Patterns.hs b/brat/Brat/Constructors/Patterns.hs index 40d923a6..1388d159 100644 --- a/brat/Brat/Constructors/Patterns.hs +++ b/brat/Brat/Constructors/Patterns.hs @@ -1,9 +1,9 @@ module Brat.Constructors.Patterns where -import Brat.UserName +import Brat.QualName pattern CSucc, CDoub, CNil, CCons, CSome, CNone, CTrue, CFalse, CZero, CSnoc, - CConcatEqEven, CConcatEqOdd, CRiffle :: UserName + CConcatEqEven, CConcatEqOdd, CRiffle :: QualName pattern CSucc = PrefixName [] "succ" pattern CDoub = PrefixName [] "doub" pattern CNil = PrefixName [] "nil" @@ -18,7 +18,7 @@ pattern CConcatEqEven = PrefixName [] "concatEqEven" pattern CConcatEqOdd = PrefixName [] "concatEqOdd" pattern CRiffle = PrefixName [] "riffle" -pattern CList, CVec, CNat, CInt, COption, CBool, CBit, CFloat, CString :: UserName +pattern CList, CVec, CNat, CInt, COption, CBool, CBit, CFloat, CString :: QualName pattern CList = PrefixName [] "List" pattern CVec = PrefixName [] "Vec" pattern CNat = PrefixName [] "Nat" @@ -29,6 +29,6 @@ pattern CBit = PrefixName [] "Bit" pattern CFloat = PrefixName [] "Float" pattern CString = PrefixName [] "String" -pattern CQubit, CMoney :: UserName +pattern CQubit, CMoney :: QualName pattern CQubit = PrefixName [] "Qubit" pattern CMoney = PrefixName [] "Money" diff --git a/brat/Brat/Eval.hs b/brat/Brat/Eval.hs index 2fc40498..440e7e35 100644 --- a/brat/Brat/Eval.hs +++ b/brat/Brat/Eval.hs @@ -17,9 +17,9 @@ module Brat.Eval (EvMode(..) import Brat.Checker.Monad import Brat.Checker.Types (EndType(..)) import Brat.Error (ErrorMsg(..)) +import Brat.QualName (plain) import Brat.Syntax.Value import Brat.Syntax.Common -import Brat.UserName (plain) import Control.Monad.Freer (req) import Bwd import Hasochism diff --git a/brat/Brat/Graph.hs b/brat/Brat/Graph.hs index ad0cf617..50bad752 100644 --- a/brat/Brat/Graph.hs +++ b/brat/Brat/Graph.hs @@ -4,10 +4,10 @@ module Brat.Graph where import Brat.Checker.Types (VEnv) import Brat.Naming +import Brat.QualName import Brat.Syntax.Common import Brat.Syntax.Simple import Brat.Syntax.Value -import Brat.UserName import Hasochism (N(..)) @@ -48,8 +48,8 @@ data NodeType :: Mode -> Type where ) -> NodeType a Hypo :: NodeType a -- Hypothesis for type checking - Constructor :: UserName -> NodeType a - Selector :: UserName -> NodeType a -- TODO: Get rid of this in favour of pattern matching + Constructor :: QualName -> NodeType a + Selector :: QualName -> NodeType a -- TODO: Get rid of this in favour of pattern matching ArithNode :: ArithOp -> NodeType Brat Replicate :: NodeType Brat MapFun :: NodeType a @@ -79,8 +79,8 @@ deriving instance Show ty => Show (MatchSequence ty) data PrimTest ty = PrimCtorTest - UserName -- the data constructor - UserName -- the type constructor + QualName -- the data constructor + QualName -- the type constructor -- (CtorArgs m) -- (hope we don't need) its entry in the constructor table Name -- the name of the node which "outputs" the data packed inside [(Src, ty)] -- ...these sources for extracted data descend diff --git a/brat/Brat/Load.hs b/brat/Brat/Load.hs index e427246e..026996d5 100644 --- a/brat/Brat/Load.hs +++ b/brat/Brat/Load.hs @@ -20,7 +20,7 @@ import Brat.Syntax.Core import Brat.Syntax.FuncDecl (FunBody(..), FuncDecl(..), Locality(..)) import Brat.Syntax.Raw import Brat.Syntax.Value -import Brat.UserName +import Brat.QualName import Util (duplicates,duplicatesWith) import Hasochism @@ -47,7 +47,7 @@ type FlatMod = ((FEnv, String) -- data at the node: declarations, and file conte -- Result of checking/compiling a module type VMod = (VEnv - ,[(UserName, VDecl)] -- all symbols from all modules + ,[(QualName, VDecl)] -- all symbols from all modules ,[TypedHole] -- for just the last module ,Store -- Ends declared & defined in the module ,Graph) -- per function, first elem is name @@ -113,7 +113,7 @@ checkDecl pre (VDecl FuncDecl{..}) to_define = (fnName -!) $ localFC fnLoc $ do uname = PrefixName pre fnName name = show uname -loadAlias :: TypeAlias -> Checking (UserName, Alias) +loadAlias :: TypeAlias -> Checking (QualName, Alias) loadAlias (TypeAlias fc name args body) = localFC fc $ do (_, [(hhungry, Left k)], _, _) <- next "" Hypo (S0,Some (Zy :* S0)) (REx ("type", Star args) R0) R0 let abs = WC fc $ foldr ((:||:) . APat . Bind . fst) AEmpty args @@ -125,7 +125,7 @@ withAliases :: [TypeAlias] -> Checking a -> Checking a withAliases [] m = m withAliases (a:as) m = loadAlias a >>= \a -> localAlias a $ withAliases as m -loadStmtsWithEnv :: Namespace -> (VEnv, [(UserName, VDecl)], Store) -> (FilePath, Prefix, FEnv, String) -> Either SrcErr VMod +loadStmtsWithEnv :: Namespace -> (VEnv, [(QualName, VDecl)], Store) -> (FilePath, Prefix, FEnv, String) -> Either SrcErr VMod loadStmtsWithEnv ns (venv, oldDecls, oldEndData) (fname, pre, stmts, cts) = addSrcContext fname cts $ do -- hacky mess - cleanup! (decls, aliases) <- desugarEnv =<< elabEnv stmts @@ -165,9 +165,9 @@ loadStmtsWithEnv ns (venv, oldDecls, oldEndData) (fname, pre, stmts, cts) = addS pure $ assert (M.null remaining) () -- all to_defines were defined pure (venv, oldDecls <> vdecls, holes, oldEndData <> newEndData, kcGraph <> graph) where - checkDecl' :: M.Map UserName [(Tgt, BinderType Brat)] - -> (UserName, VDecl) - -> Checking (M.Map UserName [(Tgt, BinderType Brat)]) + checkDecl' :: M.Map QualName [(Tgt, BinderType Brat)] + -> (QualName, VDecl) + -> Checking (M.Map QualName [(Tgt, BinderType Brat)]) checkDecl' to_define (name, decl) = -- Get the decl out of the map, and delete it from things to define case M.updateLookupWithKey (\_ _ -> Nothing) name to_define of @@ -234,7 +234,7 @@ loadFiles ns (cwd :| extraDirs) fname contents = do cts <- lift $ readFile file depGraph visited' imp' cts - getStmts :: ((FEnv, String), Import, [Import]) -> (UserName, Prefix, FEnv, String) + getStmts :: ((FEnv, String), Import, [Import]) -> (QualName, Prefix, FEnv, String) getStmts (((decls, ts), cts), Import (WC _ pn@(PrefixName ps name)) qual alias sel, _) = let prefix = case (qual, alias) of (True, Nothing) -> ps ++ [name] (False, Nothing) -> [] @@ -259,13 +259,13 @@ loadFiles ns (cwd :| extraDirs) fname contents = do (WC fc dupl:_) -> throwError $ Err (Just fc) (NameClash ("Alias not unique: " ++ show dupl)) [] -> pure () - findFile :: UserName -> ExceptT SrcErr IO String + findFile :: QualName -> ExceptT SrcErr IO String findFile uname = let possibleLocations = [nameToFile dir uname | dir <- cwd:extraDirs] in filterM (lift . doesFileExist) possibleLocations >>= \case [] -> throwError $ addSrcName (show uname) $ dumbErr (FileNotFound (show uname) possibleLocations) (x:_) -> pure x - nameToFile :: FilePath -> UserName -> String + nameToFile :: FilePath -> QualName -> String nameToFile dir (PrefixName ps file) = dir foldr () file ps ++ ".brat" checkNoCycles :: [(Int, FlatMod)] -> Either SrcErr () diff --git a/brat/Brat/Parser.hs b/brat/Brat/Parser.hs index 4522b7cd..494f193b 100644 --- a/brat/Brat/Parser.hs +++ b/brat/Brat/Parser.hs @@ -6,6 +6,7 @@ import Brat.FC import Brat.Lexer (lex) import Brat.Lexer.Token (Keyword(..), Token(..), Tok(..)) import qualified Brat.Lexer.Token as Lexer +import Brat.QualName ( plain, QualName(..) ) import Brat.Syntax.Abstractor import Brat.Syntax.Common hiding (end) import qualified Brat.Syntax.Common as Syntax @@ -13,7 +14,6 @@ import Brat.Syntax.FuncDecl (FuncDecl(..), Locality(..)) import Brat.Syntax.Concrete import Brat.Syntax.Raw import Brat.Syntax.Simple -import Brat.UserName ( plain, UserName(..) ) import Brat.Elaborator import Util ((**^)) @@ -84,13 +84,15 @@ simpleName = token0 $ \case Ident str -> Just str _ -> Nothing -qualifiedName :: Parser UserName -qualifiedName = ( "qualified name") . token0 $ \case - QualifiedId prefix str -> Just (PrefixName (toList prefix) str) - _ -> Nothing +qualName :: Parser QualName +qualName = ( "name") $ try qualifiedName <|> (PrefixName [] <$> simpleName) + where + qualifiedName :: Parser QualName + qualifiedName = ( "qualified name") . token0 $ \case + QualifiedId prefix str -> Just (PrefixName (toList prefix) str) + _ -> Nothing + -userName :: Parser UserName -userName = ( "name") $ try qualifiedName <|> (PrefixName [] <$> simpleName) round :: Parser a -> Parser a round p = label "(...)" $ match LParen *> p <* match RParen @@ -125,7 +127,7 @@ string = token0 $ \case _ -> Nothing var :: Parser Flat -var = FVar <$> userName +var = FVar <$> qualName port = simpleName @@ -609,7 +611,7 @@ pimport :: Parser Import pimport = do o <- open kmatch KImport - x <- withFC userName + x <- withFC qualName a <- alias Import x (not o) a <$> selection where @@ -643,10 +645,10 @@ pstmt = ((comment "comment") <&> \_ -> ([] , [])) alias = withFC aliasContents <&> \(WC fc (name, args, ty)) -> TypeAlias fc name args ty - aliasContents :: Parser (UserName, [(String, TypeKind)], RawVType) + aliasContents :: Parser (QualName, [(String, TypeKind)], RawVType) aliasContents = do match (K KType) - alias <- userName + alias <- qualName args <- option [] $ round (simpleName `sepBy` match Comma) {- future stuff args <- option [] $ round $ (`sepBy` (match Comma)) $ do diff --git a/brat/Brat/UserName.hs b/brat/Brat/QualName.hs similarity index 56% rename from brat/Brat/UserName.hs rename to brat/Brat/QualName.hs index 88ec5093..dca5df22 100644 --- a/brat/Brat/UserName.hs +++ b/brat/Brat/QualName.hs @@ -1,15 +1,14 @@ -module Brat.UserName where +module Brat.QualName where import Data.List (intercalate) type Prefix = [String] -data UserName - = PrefixName Prefix String +data QualName = PrefixName Prefix String deriving (Eq, Ord) -instance Show UserName where +instance Show QualName where show (PrefixName ps file) = intercalate "." (ps ++ [file]) -plain :: String -> UserName +plain :: String -> QualName plain = PrefixName [] diff --git a/brat/Brat/Search.hs b/brat/Brat/Search.hs index 94254ef8..96dbbc42 100644 --- a/brat/Brat/Search.hs +++ b/brat/Brat/Search.hs @@ -2,11 +2,11 @@ module Brat.Search (vsearch) where import Brat.Constructors (CtorArgs(..), defaultConstructors) import Brat.FC +import Brat.QualName import Brat.Syntax.Core import Brat.Syntax.Common import Brat.Syntax.Value import Brat.Syntax.Simple -import Brat.UserName import Hasochism import Control.Monad (guard) diff --git a/brat/Brat/Syntax/Abstractor.hs b/brat/Brat/Syntax/Abstractor.hs index 91e96d35..c89e8a83 100644 --- a/brat/Brat/Syntax/Abstractor.hs +++ b/brat/Brat/Syntax/Abstractor.hs @@ -1,13 +1,13 @@ module Brat.Syntax.Abstractor where +import Brat.QualName import Brat.Syntax.Port import Brat.Syntax.Simple -import Brat.UserName -- Ways to bind one thing data Pattern = Bind String - | PCon UserName Abstractor + | PCon QualName Abstractor | Lit SimpleTerm | DontCare deriving Eq diff --git a/brat/Brat/Syntax/Common.hs b/brat/Brat/Syntax/Common.hs index 95d217c6..dacd8d1b 100644 --- a/brat/Brat/Syntax/Common.hs +++ b/brat/Brat/Syntax/Common.hs @@ -42,9 +42,9 @@ module Brat.Syntax.Common (PortName, ) where import Brat.FC +import Brat.QualName import Brat.Syntax.Abstractor import Brat.Syntax.Port -import Brat.UserName import Data.Bifunctor (first) import Data.List (intercalate) @@ -165,7 +165,7 @@ instance Semigroup (CType' (PortName, ty)) where (ss :-> ts) <> (us :-> vs) = (ss <> us) :-> (ts <> vs) data Import - = Import { importName :: WC UserName + = Import { importName :: WC QualName , importQualified :: Bool , importAlias :: Maybe (WC String) , importSelection :: ImportSelection diff --git a/brat/Brat/Syntax/Concrete.hs b/brat/Brat/Syntax/Concrete.hs index fd6f9ed7..d2d567f6 100644 --- a/brat/Brat/Syntax/Concrete.hs +++ b/brat/Brat/Syntax/Concrete.hs @@ -3,11 +3,11 @@ module Brat.Syntax.Concrete where import Data.List.NonEmpty import Brat.FC +import Brat.QualName import Brat.Syntax.Common import Brat.Syntax.FuncDecl (FuncDecl(..)) import Brat.Syntax.Raw import Brat.Syntax.Simple -import Brat.UserName data FBody = FClauses (NonEmpty (WC Abstractor, WC Flat)) @@ -21,7 +21,7 @@ type FEnv = ([FDecl], [RawAlias]) data Flat - = FVar UserName + = FVar QualName | FApp (WC Flat) (WC Flat) | FJuxt (WC Flat) (WC Flat) | FThunk (WC Flat) @@ -35,7 +35,7 @@ data Flat | FLetIn (WC Abstractor) (WC Flat) (WC Flat) | FSimple SimpleTerm | FHole String - | FCon UserName (WC Flat) + | FCon QualName (WC Flat) | FEmpty | FPull [PortName] (WC Flat) -- We can get away with not elaborating type signatures in the short term diff --git a/brat/Brat/Syntax/Core.hs b/brat/Brat/Syntax/Core.hs index 1e9b019f..d3c30cff 100644 --- a/brat/Brat/Syntax/Core.hs +++ b/brat/Brat/Syntax/Core.hs @@ -15,10 +15,10 @@ import Brat.Constructors.Patterns (pattern CCons, pattern CRiffle) import Brat.FC import Brat.Naming +import Brat.QualName import Brat.Syntax.Common import Brat.Syntax.FuncDecl import Brat.Syntax.Simple -import Brat.UserName import Data.Kind (Type) import Data.Maybe (fromJust) @@ -47,7 +47,7 @@ data Term :: Dir -> Kind -> Type where Emb :: WC (Term Syn k) -> Term Chk k Forget :: WC (Term d KVerb) -> Term d UVerb Pull :: [PortName] -> WC (Term Chk k) -> Term Chk k - Var :: UserName -> Term Syn Noun -- Look up in noun (value) env + Var :: QualName -> Term Syn Noun -- Look up in noun (value) env Identity :: Term Syn UVerb Arith :: ArithOp -> WC (Term Chk Noun) -> WC (Term Chk Noun) -> Term Chk Noun Of :: WC (Term Chk Noun) -> WC (Term d Noun) -> Term d Noun @@ -64,7 +64,7 @@ data Term :: Dir -> Kind -> Type where -- In `Syn`, for now, the first clause provides the type. Lambda :: (WC Abstractor, WC (Term d Noun)) -> [(WC Abstractor, WC (Term Chk Noun))] -> Term d UVerb -- Type constructors - Con :: UserName -> WC (Term Chk Noun) -> Term Chk Noun + Con :: QualName -> WC (Term Chk Noun) -> Term Chk Noun -- Brat function types C :: CType' (PortName, KindOr (Term Chk Noun)) -> Term Chk Noun -- Kernel types diff --git a/brat/Brat/Syntax/Raw.hs b/brat/Brat/Syntax/Raw.hs index ca707b0d..ca26fa79 100644 --- a/brat/Brat/Syntax/Raw.hs +++ b/brat/Brat/Syntax/Raw.hs @@ -18,11 +18,11 @@ import Brat.Constructors import Brat.Error import Brat.FC hiding (end) import Brat.Naming +import Brat.QualName import Brat.Syntax.Common import Brat.Syntax.Core import Brat.Syntax.FuncDecl (FunBody(..), FuncDecl(..)) import Brat.Syntax.Simple -import Brat.UserName import Util (names, (**^)) type family TypeOf (k :: Kind) :: Type where @@ -36,11 +36,11 @@ type RawIO = TypeRowElem (KindOr RawVType) type RawCType = CType' RawIO type RawKType = CType' (TypeRowElem RawVType) -data TypeAliasF tm = TypeAlias FC UserName [(PortName,TypeKind)] tm deriving Show +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 UserName TypeAlias +type TypeAliasTable = M.Map QualName TypeAlias type RawEnv = ([RawFuncDecl], [RawAlias], TypeAliasTable) type RawFuncDecl = FuncDecl [RawIO] (FunBody Raw Noun) @@ -69,7 +69,7 @@ data Raw :: Dir -> Kind -> Type where REmb :: WC (Raw Syn k) -> Raw Chk k RForget :: WC (Raw d KVerb) -> Raw d UVerb RPull :: [PortName] -> WC (Raw Chk k) -> Raw Chk k - RVar :: UserName -> Raw Syn Noun + RVar :: QualName -> Raw Syn Noun RIdentity :: Raw Syn UVerb RArith :: ArithOp -> WC (Raw Chk Noun) -> WC (Raw Chk Noun) -> Raw Chk Noun ROf :: WC (Raw Chk Noun) -> WC (Raw d Noun) -> Raw d Noun @@ -77,7 +77,7 @@ data Raw :: Dir -> Kind -> Type where (::-::) :: WC (Raw Syn k) -> WC (Raw d UVerb) -> Raw d k -- vertical juxtaposition (diagrammatic composition) (::$::) :: WC (Raw d KVerb) -> WC (Raw Chk k) -> Raw d k -- Eval with ChkRaw n argument RLambda :: (WC Abstractor, WC (Raw d Noun)) -> [(WC Abstractor, WC (Raw Chk Noun))] -> Raw d UVerb - RCon :: UserName -> WC (Raw Chk Noun) -> Raw Chk Noun + RCon :: QualName -> WC (Raw Chk Noun) -> Raw Chk Noun -- Function types RFn :: RawCType -> Raw Chk Noun -- Kernel types @@ -130,7 +130,7 @@ instance Show (Raw d k) where show RFanIn = "[\\/]" show (ROf n e) = "(" ++ show n ++ " of " ++ show e ++ ")" -type Desugar = StateT Namespace (ReaderT (RawEnv, Bwd UserName) (Except Error)) +type Desugar = StateT Namespace (ReaderT (RawEnv, Bwd QualName) (Except Error)) -- instance {-# OVERLAPPING #-} MonadFail Desugar where instance {-# OVERLAPPING #-} MonadFail Desugar where @@ -150,13 +150,13 @@ splitM s = do put newRoot pure ns' -isConstructor :: UserName -> Desugar Bool +isConstructor :: QualName -> Desugar Bool isConstructor c = pure (c `member` defaultConstructors || (Brat, c) `member` defaultTypeConstructors || (Kernel, c) `member` defaultTypeConstructors || c `member` natConstructors) -isAlias :: UserName -> Desugar Bool +isAlias :: QualName -> Desugar Bool isAlias name = do aliases <- asks (thd3 . fst) pure $ M.member name aliases @@ -259,7 +259,7 @@ instance Desugarable (CType' (TypeRowElem RawVType)) where ts <- traverse desugar' (addNames ts) pure (ss :-> ts) -isConOrAlias :: UserName -> Desugar Bool +isConOrAlias :: QualName -> Desugar Bool isConOrAlias c = do con <- isConstructor c ali <- isAlias c diff --git a/brat/Brat/Syntax/Value.hs b/brat/Brat/Syntax/Value.hs index d5557f90..d1783593 100644 --- a/brat/Brat/Syntax/Value.hs +++ b/brat/Brat/Syntax/Value.hs @@ -23,10 +23,10 @@ module Brat.Syntax.Value {-(VDecl )-} where import Brat.Error +import Brat.QualName import Brat.Syntax.Common import Brat.Syntax.Core (Term (..)) import Brat.Syntax.FuncDecl (FunBody, FuncDecl(..)) -import Brat.UserName import Bwd import Hasochism @@ -151,7 +151,7 @@ instance Eq (VVar n) where -- Contains Inx's up to n-1, no Lvl's data Val :: N -> Type where VNum :: NumVal (VVar n) -> Val n - VCon :: UserName -> [Val n] -> Val n + VCon :: QualName -> [Val n] -> Val n VLam :: Val (S n) -> Val n -- Just body (binds DeBruijn index n) VFun :: MODEY m => Modey m -> CTy m n -> Val n VApp :: VVar n -> Bwd (Val n) -> Val n @@ -163,7 +163,7 @@ data SVar = SPar End | SLvl Int -- Semantic value, used internally by normalization; contains Lvl's but no Inx's data Sem where SNum :: NumVal SVar -> Sem - SCon :: UserName -> [Sem] -> Sem + SCon :: QualName -> [Sem] -> Sem -- Second is just body, we do NOT substitute under the binder, -- instead we stash Sem's for each free DeBruijn index into the first member: SLam :: Stack Z Sem n -> Val (S n) -> Sem @@ -398,7 +398,7 @@ instance EvenOrOdd Monotone where data ValPat = VPVar - | VPCon UserName [ValPat] + | VPCon QualName [ValPat] | VPNum NumPat deriving Show diff --git a/brat/brat.cabal b/brat/brat.cabal index 7dc81789..58a29efa 100644 --- a/brat/brat.cabal +++ b/brat/brat.cabal @@ -77,12 +77,12 @@ library Brat.Parser, Brat.Search, Brat.Elaborator, + Brat.QualName, Brat.Syntax.Abstractor, Brat.Syntax.Concrete, Brat.Syntax.FuncDecl, Brat.Syntax.Port, Brat.Syntax.Simple, - Brat.UserName, Bwd, Control.Monad.Freer, Data.Hugr, diff --git a/brat/test/Test/Elaboration.hs b/brat/test/Test/Elaboration.hs index 0b9ab7e3..ac6d4f1f 100644 --- a/brat/test/Test/Elaboration.hs +++ b/brat/test/Test/Elaboration.hs @@ -2,7 +2,7 @@ module Test.Elaboration (elaborationTests) where import Brat.Elaborator import Brat.Error (showError) -import Brat.UserName (plain) +import Brat.QualName (plain) import Brat.Syntax.Concrete import Brat.Syntax.Common import Brat.Syntax.Raw (kind, dir) diff --git a/brat/test/Test/Substitution.hs b/brat/test/Test/Substitution.hs index b3abf25d..f9da1d3d 100644 --- a/brat/test/Test/Substitution.hs +++ b/brat/test/Test/Substitution.hs @@ -9,9 +9,9 @@ import Brat.Checker.Types import Brat.Error import Brat.Eval (typeEq) import Brat.Naming +import Brat.QualName import Brat.Syntax.Common import Brat.Syntax.Value -import Brat.UserName import Bwd import Control.Monad.Freer import Hasochism diff --git a/brat/test/Test/Syntax/Let.hs b/brat/test/Test/Syntax/Let.hs index 7fe336e5..bd748872 100644 --- a/brat/test/Test/Syntax/Let.hs +++ b/brat/test/Test/Syntax/Let.hs @@ -5,17 +5,17 @@ module Test.Syntax.Let where import Brat.Error (showError) import Brat.Checker import Brat.FC +import Brat.QualName import Brat.Syntax.Common import Brat.Syntax.Core import Brat.Syntax.Simple import Brat.Syntax.Value -import Brat.UserName import Test.Util (runEmpty) import Data.String import Test.Tasty.HUnit -instance IsString UserName where +instance IsString QualName where fromString = PrefixName [] instance IsString Abstractor where