Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

refactor: Rename UserName to QualName #56

Merged
merged 4 commits into from
Nov 25, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
32 changes: 21 additions & 11 deletions brat/Brat/Checker.hs
Original file line number Diff line number Diff line change
Expand Up @@ -13,11 +13,12 @@
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)

Expand All @@ -33,6 +34,7 @@
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
Expand All @@ -41,7 +43,6 @@
import Brat.Syntax.Port (ToEnd, toEnd)
import Brat.Syntax.Simple
import Brat.Syntax.Value
import Brat.UserName
import Bwd
import Hasochism
import Util (zipSameLength)
Expand All @@ -55,6 +56,15 @@

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
Expand Down Expand Up @@ -247,7 +257,7 @@
-- 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))]
Expand Down Expand Up @@ -411,7 +421,7 @@
let ss = intercalate ", " . fmap show <$> sugg
pure $ take 5 (ms ++ ss)

findMatchingNouns :: Checking [[UserName]]
findMatchingNouns :: Checking [[QualName]]
findMatchingNouns = do
-- TODO
pure []
Expand Down Expand Up @@ -443,7 +453,7 @@
(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
Expand Down Expand Up @@ -714,7 +724,7 @@
NoLhs tm -> pure (tm, (fcOf tm, fcOf tm))
Clauses (c :| cs) -> do
fc <- req AskFC
pure $ (WC fc (Lambda c cs), (bimap fcOf fcOf c))

Check warning on line 727 in brat/Brat/Checker.hs

View workflow job for this annotation

GitHub Actions / hlint

Suggestion in checkBody in module Brat.Checker: Redundant $ ▫︎ Found: "pure $ (WC fc (Lambda c cs), (bimap fcOf fcOf c))" ▫︎ Perhaps: "pure (WC fc (Lambda c cs), (bimap fcOf fcOf c))"

Check warning on line 727 in brat/Brat/Checker.hs

View workflow job for this annotation

GitHub Actions / hlint

Suggestion in checkBody in module Brat.Checker: Redundant bracket ▫︎ Found: "(WC fc (Lambda c cs), (bimap fcOf fcOf c))" ▫︎ Perhaps: "(WC fc (Lambda c cs), bimap fcOf fcOf c)"
Undefined -> err (InternalError "Checking undefined clause")
((src, _), _) <- makeBox (fnName ++ ".box") cty $ \conns@(_, unders) -> do
(((), ()), leftovers) <- check tm conns
Expand Down Expand Up @@ -962,8 +972,8 @@

-- 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
Expand Down Expand Up @@ -1070,22 +1080,22 @@
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
Expand Down
13 changes: 1 addition & 12 deletions brat/Brat/Checker/Helpers.hs
Original file line number Diff line number Diff line change
Expand Up @@ -32,17 +32,14 @@
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 ()
Expand Down Expand Up @@ -131,14 +128,6 @@
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)
Expand Down Expand Up @@ -323,7 +312,7 @@
pure src

mkMono :: Monotone (VVar Z) -> Checking Src
mkMono (Linear (VPar (ExEnd e))) = pure (NamedPort e "mono")

Check warning on line 315 in brat/Brat/Checker/Helpers.hs

View workflow job for this annotation

GitHub Actions / build

Pattern match(es) are non-exhaustive

Check warning on line 315 in brat/Brat/Checker/Helpers.hs

View workflow job for this annotation

GitHub Actions / build

Pattern match(es) are non-exhaustive
mkMono (Full sm) = do
(_, [], [(twoSrc,_)], _) <- next "2" (Const (Num 2)) (S0, Some (Zy :* S0)) R0 (RPr ("value", TNat) R0)
(_, [(lhs,_),(rhs,_)], [(powSrc,_)], _) <- next "2^" (ArithNode Pow) (S0, Some (Zy :* S0))
Expand Down Expand Up @@ -352,7 +341,7 @@
mkMapFuns over [] = pure over
mkMapFuns (valSrc, ty) ((lenSrc, len):layers) = do
(valSrc, ty@(VFun my cty)) <- mkMapFuns (valSrc, ty) layers
let weak1 = changeVar (Thinning (ThDrop ThNull))

Check warning on line 344 in brat/Brat/Checker/Helpers.hs

View workflow job for this annotation

GitHub Actions / build

• The Monomorphism Restriction applies to the binding for ‘weak1’

Check warning on line 344 in brat/Brat/Checker/Helpers.hs

View workflow job for this annotation

GitHub Actions / build

• The Monomorphism Restriction applies to the binding for ‘weak1’
vecFun <- vectorisedFun len my cty
(_, [(lenTgt,_), (valTgt, _)], [(vectorSrc, Right vecTy)], _) <-
next "" MapFun (S0, Some (Zy :* S0))
Expand Down
42 changes: 21 additions & 21 deletions brat/Brat/Checker/Monad.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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
Expand All @@ -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 ()
Expand All @@ -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)
Expand Down Expand Up @@ -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)
Expand All @@ -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)]
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oooh, that's odd. We can have qualified names of variables?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think when we have functions imported from other modules they should be qualified, like kernel.CX

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah right yes thank you. Ok - so vlup is really the misnamed one - it does not necessarily look up variables; it just looks up names. Really should be nlup or qnlup or just lup (or blup to distinguish from klup? Hey, that one's actually pronouncable in one syllable... 😁 😀 )

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)
Expand All @@ -172,7 +172,7 @@ tlup (m, c) = req (TLup (m, c)) >>= \case
Brat -> Kernel
Kernel -> Brat

lookupAndUse :: UserName -> KEnv
lookupAndUse :: QualName -> KEnv
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Similarly, if it's something that might be used then will it really be a QualName?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

variables are parsed as qualified names, so they can include prefixes

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Even kernel names? Can declare a variable of type qubit whose name has a prefix?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah I see, we could be more strict about kernel variables, you're right

-> Either Error (Maybe ((Src, BinderType Kernel), KEnv))
lookupAndUse x kenv = case M.lookup x kenv of
Nothing -> Right Nothing
Expand Down
8 changes: 4 additions & 4 deletions brat/Brat/Checker/SolvePatterns.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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))]
Expand Down Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions brat/Brat/Checker/Types.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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)

Expand Down
10 changes: 5 additions & 5 deletions brat/Brat/Compile/Hugr.hs
Original file line number Diff line number Diff line change
Expand Up @@ -16,11 +16,11 @@
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
Expand Down Expand Up @@ -187,7 +187,7 @@
addOp op name | track ("addOp " ++ show op ++ show name) False = undefined
addOp op name = do
st <- get
let new_nodes = M.alter (\Nothing -> Just op) name (nodes st) -- fail if key already present

Check warning on line 190 in brat/Brat/Compile/Hugr.hs

View workflow job for this annotation

GitHub Actions / build

Pattern match(es) are non-exhaustive

Check warning on line 190 in brat/Brat/Compile/Hugr.hs

View workflow job for this annotation

GitHub Actions / build

Pattern match(es) are non-exhaustive
put (st { nodes = new_nodes })

registerCompiled :: Name -> NodeId -> Compile ()
Expand Down Expand Up @@ -487,7 +487,7 @@
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
Expand All @@ -497,7 +497,7 @@
| 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
Expand Down Expand Up @@ -777,7 +777,7 @@
[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
Expand Down Expand Up @@ -858,7 +858,7 @@
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
Expand Down
Loading
Loading