Merge remote-tracking branch 'origin/main' into acl/refactor-vectorise

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,22 +1080,22 @@ 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
                                                      ,"with type"
                                                      ,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

brat/Brat/Checker/Helpers.hs

@@ -32,18 +32,15 @@ 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.Foldable (foldrM)
-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 ()
@@ -132,14 +129,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)

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

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

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)
 

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