From 326b0c9f5f533efbd74db67657f19ee49dfa6c82 Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Wed, 13 Nov 2024 12:12:19 +0000 Subject: [PATCH 1/3] chore: Add HLint CI action and apply lints --- .github/workflows/hlint.yaml | 20 +++++++ brat/.hlint.yaml | 85 +++++++++++++++++++++++++++++- brat/Brat/Checker.hs | 62 +++++++++++----------- brat/Brat/Checker/Helpers.hs | 27 +++++----- brat/Brat/Checker/Monad.hs | 6 +-- brat/Brat/Checker/SolvePatterns.hs | 12 ++--- brat/Brat/Compile/Hugr.hs | 81 ++++++++++++++-------------- brat/Brat/Compiler.hs | 4 +- brat/Brat/Constructors.hs | 32 +++++------ brat/Brat/Elaborator.hs | 6 +-- brat/Brat/Eval.hs | 18 +++---- brat/Brat/Graph.hs | 2 +- brat/Brat/Lexer/Flat.hs | 7 ++- brat/Brat/Lexer/Token.hs | 4 +- brat/Brat/Load.hs | 16 +++--- brat/Brat/Parser.hs | 46 ++++++++-------- brat/Brat/Syntax/Abstractor.hs | 6 +-- brat/Brat/Syntax/Core.hs | 6 +-- brat/Brat/Syntax/Raw.hs | 12 ++--- brat/Brat/Syntax/Value.hs | 14 ++--- brat/Brat/UserName.hs | 2 +- brat/Data/Hugr.hs | 6 +-- brat/Util.hs | 10 ++-- brat/app/Main.hs | 2 +- brat/lsp/Brat/LSP/Find.hs | 4 +- brat/lsp/Driver.hs | 2 +- brat/test/Test/Abstractor.hs | 10 ++-- brat/test/Test/Checking.hs | 2 +- brat/test/Test/Compile/Hugr.hs | 4 +- brat/test/Test/Elaboration.hs | 22 ++++---- brat/test/Test/Search.hs | 2 +- brat/test/Test/TypeArith.hs | 4 +- brat/test/Test/Util.hs | 2 +- 33 files changed, 315 insertions(+), 223 deletions(-) create mode 100644 .github/workflows/hlint.yaml diff --git a/.github/workflows/hlint.yaml b/.github/workflows/hlint.yaml new file mode 100644 index 00000000..39de47b3 --- /dev/null +++ b/.github/workflows/hlint.yaml @@ -0,0 +1,20 @@ +name: Brat CI +on: + pull_request: [] + +jobs: + hlint: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + + - name: 'Setup HLint' + uses: haskell-actions/hlint-setup@v2 + + - name: 'Run HLint' + uses: haskell-actions/hlint-run@v2 + with: + path: brat/ + # https://github.com/haskell-actions/hlint-run/issues/20#issuecomment-2168787894 + hlint-bin: hlint --hint=brat/.hlint.yaml + fail-on: warning diff --git a/brat/.hlint.yaml b/brat/.hlint.yaml index 2df67984..e9080188 100644 --- a/brat/.hlint.yaml +++ b/brat/.hlint.yaml @@ -1,2 +1,83 @@ -- ignore: {name: Use <$>} -- ignore: {name: Use second} \ No newline at end of file +# HLint configuration file +# https://github.com/ndmitchell/hlint +########################## + +# This file contains a template configuration file, which is typically +# placed as .hlint.yaml in the root of your project + + +# Specify additional command line arguments +# +# - arguments: [--color, --cpp-simple, -XQuasiQuotes] + + +# Control which extensions/flags/modules/functions can be used +# +# - extensions: +# - default: false # all extension are banned by default +# - name: [PatternGuards, ViewPatterns] # only these listed extensions can be used +# - {name: CPP, within: CrossPlatform} # CPP can only be used in a given module +# +# - flags: +# - {name: -w, within: []} # -w is allowed nowhere +# +# - modules: +# - {name: [Data.Set, Data.HashSet], as: Set} # if you import Data.Set qualified, it must be as 'Set' +# - {name: Control.Arrow, within: []} # Certain modules are banned entirely +# +# - functions: +# - {name: unsafePerformIO, within: []} # unsafePerformIO can only appear in no modules + + +# Add custom hints for this project +# +# Will suggest replacing "wibbleMany [myvar]" with "wibbleOne myvar" +# - error: {lhs: "wibbleMany [x]", rhs: wibbleOne x} + +# The hints are named by the string they display in warning messages. +# For example, if you see a warning starting like +# +# Main.hs:116:51: Warning: Redundant == +# +# You can refer to that hint with `{name: Redundant ==}` (see below). + +# Turn on hints that are off by default +# +# Ban "module X(module X) where", to require a real export list +# - warn: {name: Use explicit module export list} +# +# Replace a $ b $ c with a . b $ c +# - group: {name: dollar, enabled: true} +# +# Generalise map to fmap, ++ to <> +# - group: {name: generalise, enabled: true} +# +# Warn on use of partial functions +# - group: {name: partial, enabled: true} + + +# Ignore some builtin hints +# - ignore: {name: Use let} +# - ignore: {name: Use const, within: SpecialModule} # Only within certain modules +- ignore: {name: Use const} +- ignore: {name: Use section} +- ignore: {name: Use void} +- ignore: {name: Use list comprehension} +- ignore: {name: Use newtype instead of data} +- ignore: {name: Fuse foldr/<$>} +- ignore: {name: Redundant bracket, within: Brat.Syntax.Value} +- ignore: {name: Avoid NonEmpty.unzip} # Buggy - false positives + +# Define some custom infix operators +# - fixity: infixr 3 ~^#^~ +- fixity: infixl 7 :<< +- fixity: infixr 8 <<+ +- fixity: infixl 7 :<< +- fixity: infixr 8 <<+ +- fixity: infixr 3 **^ +- fixity: infixr 3 ^** + + + +# To generate a suitable file for HLint do: +# $ hlint --default > .hlint.yaml diff --git a/brat/Brat/Checker.hs b/brat/Brat/Checker.hs index d243476b..c855e6ad 100644 --- a/brat/Brat/Checker.hs +++ b/brat/Brat/Checker.hs @@ -8,16 +8,16 @@ module Brat.Checker (checkBody ) where import Control.Exception (assert) -import Control.Monad (foldM, forM, zipWithM) +import Control.Monad (foldM, forM, zipWithM_) import Control.Monad.Freer -import Data.Bifunctor (first, second) +import Data.Bifunctor +import Data.Foldable (for_) import Data.Functor (($>), (<&>)) import Data.List ((\\)) import Data.List.NonEmpty (NonEmpty(..)) import qualified Data.List.NonEmpty as NE import qualified Data.Map as M import Data.Maybe (fromJust) -import Data.Traversable (for) import Data.Type.Equality ((:~:)(..)) import Prelude hiding (filter) @@ -44,14 +44,14 @@ import Brat.Syntax.Value import Brat.UserName import Bwd import Hasochism -import Util (zip_same_length) +import Util (zipSameLength) -- Put things into a standard form in a kind-directed manner, such that it is -- meaningful to do case analysis on them standardise :: TypeKind -> Val Z -> Checking (Val Z) -standardise k val = eval S0 val <&> (k,) >>= \case +standardise k val = eval S0 val >>= (\case (Nat, val) -> pure . VNum $ numVal val - (_, val) -> pure val + (_, val) -> pure val) . (k,) mergeEnvs :: [Env a] -> Checking (Env a) mergeEnvs = foldM combineDisjointEnvs M.empty @@ -212,12 +212,12 @@ check' (Lambda c@(WC abstFC abst, body) cs) (overs, unders) = do (_, [], fakeOvers, fakeAcc) <- anext "lambda_fake_source" Hypo (S0, Some (Zy :* S0)) R0 ins -- Hypo `check` calls need an environment, even just to compute leftovers; -- we get that env by solving `problem` reformulated in terms of the `fakeOvers` - let srcMap = fromJust $ zip_same_length (fst <$> usedOvers) (fst <$> fakeOvers) + let srcMap = fromJust $ zipSameLength (fst <$> usedOvers) (fst <$> fakeOvers) let fakeProblem = [ (fromJust (lookup src srcMap), pat) | (src, pat) <- problem ] fakeEnv <- localFC abstFC $ solve ?my fakeProblem >>= (solToEnv . snd) localEnv fakeEnv $ do (_, fakeUnders, [], _) <- anext "lambda_fake_target" Hypo fakeAcc outs R0 - Just tgtMap <- pure $ zip_same_length (fst <$> fakeUnders) unders + Just tgtMap <- pure $ zipSameLength (fst <$> fakeUnders) unders (((), ()), ((), rightFakeUnders)) <- check body ((), fakeUnders) pure (fakeUnders, rightFakeUnders, tgtMap) @@ -260,7 +260,7 @@ check' (Lambda c@(WC abstFC abst, body) cs) (overs, unders) = do retuple (NamedPort e p, ty) = (p, e, ty) - mkWires overs unders = case zip_same_length overs unders of + mkWires overs unders = case zipSameLength overs unders of Nothing -> err $ InternalError "Trying to wire up different sized lists of wires" Just conns -> traverse (\((src, ty), (tgt, _)) -> wire (src, binderToValue ?my ty, tgt)) conns @@ -435,7 +435,7 @@ check' (VHole (mnemonic, name)) connectors = do pure (((), ()), ([], [])) -- TODO: Better error message check' tm@(Con _ _) ((), []) = typeErr $ "No type to check " ++ show tm ++ " against" -check' tm@(Con vcon vargs) ((), ((hungry, ty):unders)) = case (?my, ty) of +check' tm@(Con vcon vargs) ((), (hungry, ty):unders) = case (?my, ty) of (Braty, Left k) -> do (_, leftOvers) <- kindCheck [(hungry, k)] (Con vcon vargs) ensureEmpty "kindCheck leftovers" leftOvers @@ -464,13 +464,13 @@ check' tm@(Con vcon vargs) ((), ((hungry, ty):unders)) = case (?my, ty) of ensureEmpty "con unders" leftUnders wire (dangling, ty, hungry) -check' (C cty) ((), ((hungry, ty):unders)) = case (?my, ty) of +check' (C cty) ((), (hungry, ty):unders) = case (?my, ty) of (Braty, Left k) -> do (_, leftOvers) <- kindCheck [(hungry, k)] (C cty) ensureEmpty "kindCheck leftovers" leftOvers pure (((), ()), ((), unders)) _ -> typeErr $ "Ill-kinded function type: " ++ show cty -check' (Simple tm) ((), ((hungry, ty):unders)) = do +check' (Simple tm) ((), (hungry, ty):unders) = do ty <- evalBinder ?my ty case (?my, ty, tm) of -- The only SimpleType that checks against a kind is a Nat @@ -509,12 +509,12 @@ check' FanOut ((p, ty):overs, ()) = do fanoutNodes my n (dangling, ty) elTy = do (_, [(hungry, _)], [danglingHead, danglingTail], _) <- anext "fanoutNodes" (Selector (plain "cons")) (S0, Some (Zy :* S0)) (RPr ("value", binderToValue my ty) R0) - ((RPr ("head", elTy) (RPr ("tail", TVec elTy (VNum (nConstant (n - 1)))) R0)) :: Ro m Z Z) + (RPr ("head", elTy) (RPr ("tail", TVec elTy (VNum (nConstant (n - 1)))) R0) :: Ro m Z Z) -- Wire the input into the selector node wire (dangling, binderToValue my ty, hungry) (danglingHead:) <$> fanoutNodes my (n - 1) danglingTail elTy -check' FanIn (overs, ((tgt, ty):unders)) = do +check' FanIn (overs, (tgt, ty):unders) = do ty <- eval S0 (binderToValue ?my ty) case ty of TVec elTy n @@ -548,14 +548,14 @@ check' FanIn (overs, ((tgt, ty):unders)) = do typeEq (show FanIn) k elTy (binderToValue my overTy) let tailTy = TVec elTy (VNum (nConstant (n - 1))) (_, [(hungryHead, _), (hungryTail, tailTy)], [(danglingResult, _)], _) <- anext "faninNodes" (Constructor (plain "cons")) (S0, Some (Zy :* S0)) - ((RPr ("head", elTy) (RPr ("tail", tailTy) R0)) :: Ro m Z Z) + (RPr ("head", elTy) (RPr ("tail", tailTy) R0) :: Ro m Z Z) (RPr ("value", binderToValue my ty) R0) wire (over, elTy, hungryHead) wire (danglingResult, binderToValue ?my ty, hungry) faninNodes my (n - 1) (hungryTail, tailTy) elTy overs -check' Identity ((this:leftovers), ()) = pure (((), [this]), (leftovers, ())) +check' Identity (this:leftovers, ()) = pure (((), [this]), (leftovers, ())) check' (Of n e) ((), unders) = case ?my of - Kerny -> typeErr $ "`of` not supported in kernel contexts" + Kerny -> typeErr "`of` not supported in kernel contexts" Braty -> do -- TODO: Our expectations about Id nodes in compilation might need updated? (_, [(natUnder,Left k)], [(natOver, _)], _) <- anext "Of_len" Id (S0, Some (Zy :* S0)) @@ -578,7 +578,7 @@ check' (Of n e) ((), unders) = case ?my of (repConns, tgtMap) <- mkReplicateNodes n elemUnders let (lenIns, repUnders, repOvers) = unzip3 repConns -- Wire the length into all the replicate nodes - for lenIns $ \(tgt, _) -> do + for_ lenIns $ \(tgt, _) -> do wire (natOver, kindType Nat, tgt) defineTgt tgt n (((), ()), ((), elemRightUnders)) <- check e ((), repUnders) @@ -586,13 +586,13 @@ check' (Of n e) ((), unders) = case ?my of -- in the call to getVecs, so we should work out which elements of -- the original unders weren't used, and make sure they prefix the -- unders returned from here. - let unusedVecTgts :: [Tgt] = (fromJust . flip lookup tgtMap . fst) <$> elemRightUnders + let unusedVecTgts :: [Tgt] = fromJust . flip lookup tgtMap . fst <$> elemRightUnders let (usedVecUnders, unusedVecUnders) = splitAt (length vecUnders - length unusedVecTgts) vecUnders -- Wire up the outputs of the replicate nodes to the _used_ vec -- unders. The remainder of the replicate nodes don't get used. -- (their inputs live in `elemRightUnders`) assert (length repOvers >= length usedVecUnders) $ do - zipWithM (\(dangling, _) (hungry, ty) -> wire (dangling, ty, hungry)) repOvers usedVecUnders + zipWithM_ (\(dangling, _) (hungry, ty) -> wire (dangling, ty, hungry)) repOvers usedVecUnders pure (((), ()), ((), (second Right <$> unusedVecUnders) ++ rightUnders)) _ -> localFC (fcOf e) $ typeErr "No type dependency allowed when using `of`" @@ -606,10 +606,10 @@ check' (Of n e) ((), unders) = case ?my of outputs <- getVals outputs (conns, _) <- mkReplicateNodes n outputs let (lenIns, elemIns, vecOuts) = unzip3 conns - for lenIns $ \(tgt,_) -> do + for_ lenIns $ \(tgt,_) -> do wire (natOver, kindType Nat, tgt) defineTgt tgt n - zipWithM (\(dangling, ty) (hungry, _) -> wire (dangling, ty, hungry)) outputs elemIns + zipWithM_ (\(dangling, ty) (hungry, _) -> wire (dangling, ty, hungry)) outputs elemIns pure (((), vecOuts), ((), ())) _ -> localFC (fcOf e) $ typeErr "No type dependency allowed when using `of`" where @@ -635,7 +635,7 @@ check' (Of n e) ((), unders) = case ?my of (REx ("n", Nat) (RPr ("elem", weakTy) R0)) -- the type of e (RPr ("vec", TVec weakTy (VApp (VInx VZ) B0)) R0) -- a vector of e's of length n?? (conns, tgtMap) <- mkReplicateNodes len unders - pure ((lenUnder, repUnder, repOver):conns, ((fst repUnder), t):tgtMap) + pure ((lenUnder, repUnder, repOver):conns, (fst repUnder, t):tgtMap) getVecs :: Val Z -- The length of vectors we're looking for -> [(Tgt, BinderType Brat)] @@ -720,7 +720,7 @@ checkBody fnName body cty = case body of ((box, _), _) <- makeBox (fnName ++ ".box") cty $ \conns -> do let tm = Lambda c cs (((), ()), leftovers) <- check (WC fc tm) conns - checkConnectorsUsed (fcOf (fst c), fcOf (snd c)) (show tm) conns leftovers + checkConnectorsUsed (bimap fcOf fcOf c) (show tm) conns leftovers pure box Undefined -> err (InternalError "Checking undefined clause") where @@ -737,15 +737,15 @@ checkBody fnName body cty = case body of mkArgRo :: Modey m -> Stack Z End bot -> [(NamedPort End, BinderType m)] -> Checking (Some (Stack Z End :* Ro m bot)) mkArgRo _ ez [] = pure $ Some (ez :* R0) mkArgRo Braty ez ((p, Left k):rest) = mkArgRo Braty (ez :<< end p) rest >>= \case - Some (ez' :* ro) -> pure $ Some $ ez' :* (REx (portName p, k) ro) + Some (ez' :* ro) -> pure $ Some $ ez' :* REx (portName p, k) ro mkArgRo Braty ez ((p, Right t):rest) = mkArgRo Braty ez rest >>= \case Some (ez' :* ro) -> do t <- standardise (TypeFor Brat []) t - pure $ Some $ ez' :* (RPr (portName p, abstractEndz ez t) ro) + pure $ Some $ ez' :* RPr (portName p, abstractEndz ez t) ro mkArgRo Kerny ez ((p, t):rest) = mkArgRo Kerny ez rest >>= \case Some (ez' :* ro) -> do t <- standardise (TypeFor Brat []) t - pure $ Some $ ez' :* (RPr (portName p, abstractEndz ez t) ro) + pure $ Some $ ez' :* RPr (portName p, abstractEndz ez t) ro mkKindRo :: [(PortName, TypeKind)] -> Some (Ro Brat bot) mkKindRo [] = Some R0 @@ -792,7 +792,7 @@ kindCheck ((hungry, k@(TypeFor m [])):unders) (Con c arg) = req (TLup (m, c)) >> -- va = endVal of (end kindOut), so not as useful as -- the thing we *do* define kindOut as - (_, argUnders, [(kindOut,_)], ((_ :<< _va), _)) <- + (_, argUnders, [(kindOut,_)], (_ :<< _va, _)) <- next "" Hypo (S0, Some (Zy :* S0)) aliasArgs (REx ("type",Star []) R0) -- arg is a juxtaposition (args, emptyUnders) <- kindCheck (second (\(Left k) -> k) <$> argUnders) (unWC arg) @@ -947,7 +947,7 @@ kindCheckRow' Braty (ny :* s) env (name,i) ((p, Left k):rest) = do -- s is Stack 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))) + 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 (Braty, Right ty) -> helper ty (Star []) (Kerny, ty) -> helper ty (Dollar []) @@ -962,7 +962,7 @@ kindCheckRow' my ez@(ny :* s) env (name, i) ((p, bty):rest) = case (my, bty) of v <- pure $ changeVar (ParToInx (AddZ ny) s) v (i, env, ser) <- kindCheckRow' my ez env (name, i+1) rest case ser of - Some (s_m :* ro) -> pure (i, env, Some (s_m :* (RPr (p, v) ro))) + Some (s_m :* ro) -> pure (i, env, Some (s_m :* RPr (p, v) ro)) -- Look for vectors to produce better error messages for mismatched lengths -- in terms or patterns. @@ -1048,7 +1048,7 @@ abstractPattern Braty (dangling, Left k) pat = abstractKind k pat where abstractKind :: TypeKind -> Pattern -> Checking (Env (EnvData Brat)) abstractKind _ (Bind x) = let ?my = Braty in singletonEnv x (dangling, Left k) - abstractKind _ (DontCare) = pure emptyEnv + abstractKind _ DontCare = pure emptyEnv abstractKind k (Lit x) = case (k, x) of (Nat, Num n) -> defineSrc dangling (VNum (nConstant (fromIntegral n))) $> emptyEnv (Star _, _) -> err MatchingOnTypes diff --git a/brat/Brat/Checker/Helpers.hs b/brat/Brat/Checker/Helpers.hs index f05a54b9..5e609f14 100644 --- a/brat/Brat/Checker/Helpers.hs +++ b/brat/Brat/Checker/Helpers.hs @@ -38,7 +38,7 @@ import Hasochism import Util (log2) import Control.Monad.Freer (req, Free(Ret)) -import Control.Arrow ((***)) +import Data.Bifunctor import Data.List (intercalate) import Data.Type.Equality (TestEquality(..), (:~:)(..)) import qualified Data.Map as M @@ -126,10 +126,10 @@ pullPorts toPort showFn (p:ports) types = do pull1Port p [] = fail $ "Port not found: " ++ p ++ " in " ++ showFn types pull1Port p (x@(a,_):xs) | p == toPort a - = if (p `elem` (toPort . fst <$> xs)) + = if p `elem` (toPort . fst <$> xs) then err (AmbiguousPortPull p (showFn (x:xs))) else pure (x, xs) - | otherwise = (id *** (x:)) <$> pull1Port p xs + | otherwise = second (x:) <$> pull1Port p xs combineDisjointEnvs :: M.Map UserName v -> M.Map UserName v -> Checking (M.Map UserName v) combineDisjointEnvs l r = @@ -137,7 +137,7 @@ combineDisjointEnvs l r = in if S.null commonKeys then Ret $ M.union l r else typeErr ("Variable(s) defined twice: " ++ - (intercalate "," $ map show $ S.toList commonKeys)) + intercalate "," (map show $ S.toList commonKeys)) ensureEmpty :: Show ty => String -> [(NamedPort e, ty)] -> Checking () ensureEmpty _ [] = pure () @@ -149,7 +149,7 @@ noUnders m = do pure (outs, overs) rowToSig :: Traversable t => t (NamedPort e, ty) -> t (PortName, ty) -rowToSig = fmap $ \(p,ty) -> (portName p, ty) +rowToSig = fmap $ first portName showMode :: Modey m -> String showMode Braty = "" @@ -258,7 +258,7 @@ getThunks :: Modey m ,Overs m UVerb ) getThunks _ [] = pure ([], [], []) -getThunks Braty row@((src, Right ty):rest) = ((src,) <$> eval S0 ty) >>= vectorise >>= \case +getThunks Braty row@((src, Right ty):rest) = (eval S0 ty >>= vectorise . (src,)) >>= \case (src, VFun Braty (ss :->> ts)) -> do (node, unders, overs, _) <- let ?my = Braty in anext "" (Eval (end src)) (S0, Some (Zy :* S0)) ss ts @@ -267,7 +267,7 @@ getThunks Braty row@((src, Right ty):rest) = ((src,) <$> eval S0 ty) >>= vectori -- These shouldn't happen (_, VFun _ _) -> err $ ExpectedThunk (showMode Braty) (showRow row) v -> typeErr $ "Force called on non-thunk: " ++ show v -getThunks Kerny row@((src, Right ty):rest) = ((src,) <$> eval S0 ty) >>= vectorise >>= \case +getThunks Kerny row@((src, Right ty):rest) = (eval S0 ty >>= vectorise . (src,)) >>= \case (src, VFun Kerny (ss :->> ts)) -> do (node, unders, overs, _) <- let ?my = Kerny in anext "" (Splice (end src)) (S0, Some (Zy :* S0)) ss ts (nodes, unders', overs') <- getThunks Kerny rest @@ -422,7 +422,7 @@ makeBox name cty@(ss :->> ts) body = do bres <- name -! body (overs, unders) pure (thunk, bres) (Braty, body) -> do - (bres, captures) <- name -! (captureOuterLocals $ body (overs, unders)) + (bres, captures) <- name -! captureOuterLocals (body (overs, unders)) (_, [], [thunk], _) <- next (name ++ "_thunk") (Box captures src tgt) (S0, Some (Zy :* S0)) R0 (RPr ("thunk", VFun ?my cty) R0) pure (thunk, bres) @@ -438,26 +438,25 @@ natEqOrBust :: Ny i -> Ny j -> Either ErrorMsg (i :~: j) natEqOrBust n m | Just q <- testEquality n m = pure q natEqOrBust _ _ = Left $ InternalError "We can't count" -rowToRo :: ToEnd t => Modey m -> [(String, t, BinderType m)] -> Stack Z End i -> Checking (Some ((Ro m i) :* Stack Z End)) +rowToRo :: ToEnd t => Modey m -> [(String, t, BinderType m)] -> Stack Z End i -> Checking (Some (Ro m i :* Stack Z End)) rowToRo _ [] stk = pure $ Some (R0 :* stk) rowToRo Kerny ((p, _, ty):row) S0 = do ty <- eval S0 ty rowToRo Kerny row S0 >>= \case - Some (ro :* stk) -> pure . Some $ ((RPr (p, changeVar (ParToInx (AddZ Zy) S0) ty) ro)) :* stk + Some (ro :* stk) -> pure . Some $ RPr (p, changeVar (ParToInx (AddZ Zy) S0) ty) ro :* stk rowToRo Kerny _ (_ :<< _) = err $ InternalError "rowToRo - no binding allowed in kernels" rowToRo Braty ((p, _, Right ty):row) endz = do ty <- eval S0 ty rowToRo Braty row endz >>= \case - Some (ro :* stk) -> pure . Some $ (RPr (p, changeVar (ParToInx (AddZ (stackLen endz)) endz) ty) ro) :* stk + Some (ro :* stk) -> pure . Some $ RPr (p, changeVar (ParToInx (AddZ (stackLen endz)) endz) ty) ro :* stk rowToRo Braty ((p, tgt, Left k):row) endz = rowToRo Braty row (endz :<< toEnd tgt) >>= \case - Some (ro :* stk) -> pure . Some $ (REx (p, k) ro) :* stk + Some (ro :* stk) -> pure . Some $ REx (p, k) ro :* stk roToTuple :: Ro m Z Z -> Val Z roToTuple R0 = TNil roToTuple (RPr (_, ty) ro) = TCons ty (roToTuple ro) -roToTuple (REx _ ro) = case ro of - _ -> error "the impossible happened" +roToTuple (REx _ _) = error "the impossible happened" -- Low hanging fruit that we can easily do to our normal forms of numbers runArith :: NumVal (VVar Z) -> ArithOp -> NumVal (VVar Z) -> Maybe (NumVal (VVar Z)) diff --git a/brat/Brat/Checker/Monad.hs b/brat/Brat/Checker/Monad.hs index b8a5b6b6..4b219e69 100644 --- a/brat/Brat/Checker/Monad.hs +++ b/brat/Brat/Checker/Monad.hs @@ -99,7 +99,7 @@ localAlias con (Req r k) = Req r (localAlias con . k) localFC :: FC -> Checking v -> Checking v localFC _ (Ret v) = Ret v localFC f (Req AskFC k) = localFC f (k f) -localFC f (Req (Throw (e@Err{fc=Nothing})) k) = localFC f (Req (Throw (e{fc=Just f})) k) +localFC f (Req (Throw e@Err{fc=Nothing}) k) = localFC f (Req (Throw (e{fc=Just f})) k) localFC f (Req r k) = Req r (localFC f . k) localEnv :: (?my :: Modey m) => Env (EnvData m) -> Checking v -> Checking v @@ -176,7 +176,7 @@ lookupAndUse :: UserName -> KEnv -> Either Error (Maybe ((Src, BinderType Kernel), KEnv)) lookupAndUse x kenv = case M.lookup x kenv of Nothing -> Right Nothing - Just (None, _) -> Left $ dumbErr $ TypeErr $ (show x) ++ " has already been used" + Just (None, _) -> Left $ dumbErr $ TypeErr $ show x ++ " has already been used" Just (One, rest) -> Right $ Just (rest, M.insert x (None, rest) kenv) Just (Tons, rest) -> Right $ Just (rest, M.insert x (Tons, rest) kenv) @@ -223,7 +223,7 @@ handler (Req s k) ctx g -- Receiving KDone may become possible when merging the two check functions KDone -> error "KDone in handler - this shouldn't happen" AskVEnv -> handler (k (CtxEnv { globals = globalVEnv ctx, locals = M.empty })) ctx g - ELup end -> handler (k ((M.lookup end) . valueMap . store $ ctx)) ctx g + ELup end -> handler (k (M.lookup end . valueMap . store $ ctx)) ctx g TypeOf end -> case M.lookup end . typeMap . store $ ctx of Just et -> handler (k et) ctx g Nothing -> Left (dumbErr . InternalError $ "End " ++ show end ++ " isn't Declared") diff --git a/brat/Brat/Checker/SolvePatterns.hs b/brat/Brat/Checker/SolvePatterns.hs index 272915a3..1cdcce76 100644 --- a/brat/Brat/Checker/SolvePatterns.hs +++ b/brat/Brat/Checker/SolvePatterns.hs @@ -19,7 +19,7 @@ import Hasochism import Control.Monad (unless) import Data.Bifunctor (first) -import Data.Foldable (traverse_) +import Data.Foldable (for_, traverse_) import qualified Data.Map as M import Data.Maybe (fromJust) import Data.Type.Equality ((:~:)(..), testEquality) @@ -64,9 +64,7 @@ solve my ((src, DontCare):p) = do () <- case my of Kerny -> do ty <- typeOfSrc Kerny src - if not (fromJust (copyable ty)) - then (typeErr $ "Ignoring linear variable of type " ++ show ty) - else pure () + unless (fromJust (copyable ty)) $ typeErr $ "Ignoring linear variable of type " ++ show ty Braty -> pure () solve my p solve my ((src, Bind x):p) = do @@ -144,7 +142,7 @@ solveConstructor my src (c, abs) ty p = do (_, _, _, stuff) <- next "type_args" Hypo (S0, Some (Zy :* S0)) patRo R0 (node, _, patArgWires, _) <- let ?my = my in anext "val_args" Hypo stuff R0 argRo trackM ("Constructor " ++ show c ++ "; type " ++ show ty) - case (snd stuff) of + case snd stuff of Some (_ :* patEnds) -> do trackM (show pats) trackM (show patEnds) @@ -198,9 +196,7 @@ instantiateMeta e val = do -- We can have bogus failures here because we're not normalising under lambdas -- N.B. the value argument is normalised. doesntOccur :: End -> Val n -> Either ErrorMsg () -doesntOccur e (VNum nv) = case getNumVar nv of - Just e' -> collision e e' - _ -> pure () +doesntOccur e (VNum nv) = for_ (getNumVar nv) (collision e) where getNumVar :: NumVal (VVar n) -> Maybe End getNumVar (NumValue _ (StrictMonoFun (StrictMono _ mono))) = case mono of diff --git a/brat/Brat/Compile/Hugr.hs b/brat/Brat/Compile/Hugr.hs index c5bc13f5..3a33c97d 100644 --- a/brat/Brat/Compile/Hugr.hs +++ b/brat/Brat/Compile/Hugr.hs @@ -133,7 +133,7 @@ runCheckingInCompile (Ret t) = pure t runCheckingInCompile (Req (ELup e) k) = do emap <- gets (valueMap . store) runCheckingInCompile (k (M.lookup e emap)) -runCheckingInCompile (Req _ _) = error $ "Compile monad found a command it can't handle" +runCheckingInCompile (Req _ _) = error "Compile monad found a command it can't handle" -- To be called on top-level signatures which are already Inx-closed, but not -- necessarily normalised. @@ -146,8 +146,8 @@ compileCTy (ss :->> ts )= PolyFuncType [] (FunctionType (compileRo ss) (compileR compileRo :: Ro m i j -- The Ro that we're processing -> [HugrType] -- The hugr type of the row compileRo R0 = [] -compileRo (RPr (_, ty) ro) = (compileType ty):(compileRo ro) -compileRo (REx (_, k) ro) = (compileType (kindType k)):(compileRo ro) +compileRo (RPr (_, ty) ro) = compileType ty:compileRo ro +compileRo (REx (_, k) ro) = compileType (kindType k):compileRo ro -- Val Z should already be eval'd at this point compileType :: Val n -> HugrType @@ -161,7 +161,7 @@ compileType TFloat = hugrFloat compileType ty@(TCons _ _) = htTuple (tuple ty) where tuple :: Val n -> [HugrType] - tuple (TCons hd rest) = (compileType hd):(tuple rest) + tuple (TCons hd rest) = compileType hd:tuple rest tuple TNil = [] tuple ty = error $ "Found " ++ show ty ++ " in supposed tuple type" compileType TNil = htTuple [] @@ -181,7 +181,7 @@ compileGraphTypes = traverse ((<&> compileType) . runCheckingInCompile . eval S0 -- Compile a list of types from the inputs or outputs of a node in the BRAT graph compilePorts :: [(a, Val Z)] -> Compile [HugrType] -compilePorts = compileGraphTypes . (map snd) +compilePorts = compileGraphTypes . map snd addOp :: HugrOp NodeId -> NodeId -> Compile () addOp op name | track ("addOp " ++ show op ++ show name) False = undefined @@ -249,7 +249,7 @@ renameAndSortHugr nodes edges = fmap update (Hugr (fst <$> sorted_nodes) (edges parentOf n1 /= parentOf n2 , requiresOrderEdge (nodes M.! n1), requiresOrderEdge (nodes M.! n2) ] in - [(Port src orderEdgeOffset, Port tgt orderEdgeOffset) | (src, tgt) <- (walkUp <$> interEdges)] + [(Port src orderEdgeOffset, Port tgt orderEdgeOffset) | (src, tgt) <- walkUp <$> interEdges] requiresOrderEdge :: HugrOp NodeId -> Bool requiresOrderEdge (OpMod _) = False @@ -275,7 +275,7 @@ compileClauses parent ins ((matchData, rhs) :| clauses) = do (ns, _) <- gets bratGraph -- RHS has to be a box, so it must have a function type outTys <- case nodeOuts (ns M.! rhs) of - [(_, VFun my cty)] -> (body <$> compileSig my cty) >>= \(FunctionType _ outs) -> pure outs + [(_, VFun my cty)] -> compileSig my cty >>= (\(FunctionType _ outs) -> pure outs) . body _ -> error "Expected 1 kernel function type from rhs" -- Compile the match: testResult is the port holding the dynamic match result @@ -303,7 +303,7 @@ compileClauses parent ins ((matchData, rhs) :| clauses) = do BratNode (Box _venv src tgt) _ _ -> do dfgId <- addNode "DidMatch_DFG" (OpDFG (DFG parent (FunctionType (snd <$> ins) outTys))) compileBox (src, tgt) dfgId - for (zip (fst <$> ins) (Port dfgId <$> [0..])) addEdge + for_ (zip (fst <$> ins) (Port dfgId <$> [0..])) addEdge pure $ zip (Port dfgId <$> [0..]) outTys _ -> error "RHS should be a box node" @@ -312,17 +312,17 @@ compileBox :: (Name, Name) -> NodeId -> Compile () compileBox (src, tgt) parent = for_ [src, tgt] (compileWithInputs parent) compileWithInputs :: NodeId -> Name -> Compile (Maybe NodeId) -compileWithInputs parent name = gets compiled <&> M.lookup name >>= \case +compileWithInputs parent name = gets compiled >>= (\case Just nid -> pure (Just nid) Nothing -> do (_, es) <- gets bratGraph - let in_edges = [((src, ty), portNum) | (src, ty, (In edgTgt portNum)) <- es, edgTgt == name] + let in_edges = [((src, ty), portNum) | (src, ty, In edgTgt portNum) <- es, edgTgt == name] compileNode in_edges >>= \case Nothing -> pure Nothing Just (tgtNodeId, edges) -> do registerCompiled name tgtNodeId - for edges (\(src, tgtPort) -> addEdge (src, Port tgtNodeId tgtPort)) - pure $ Just tgtNodeId + for_ edges (\(src, tgtPort) -> addEdge (src, Port tgtNodeId tgtPort)) + pure $ Just tgtNodeId) . M.lookup name where -- If we only care about the node for typechecking, then drop it and return `Nothing`. -- Otherwise, NodeId of compiled node, and list of Hugr in-edges (source and target-port) @@ -335,17 +335,20 @@ compileWithInputs parent name = gets compiled <&> M.lookup name >>= \case decls <- gets decls let (funcDef, extra_call) = decls M.! name - nod <- case extra_call of - True -> addNode ("direct_call(" ++ show funcDef ++ ")") - (OpCall (CallOp parent (FunctionType [] hTys))) - -- We are loading idNode as a value (not an Eval'd thing), and it is a FuncDef directly - -- corresponding to a Brat TLD (not that produces said TLD when eval'd) - False -> case hTys of - [HTFunc poly@(PolyFuncType [] _)] -> - addNode ("load_thunk(" ++ show funcDef ++ ")") - (OpLoadFunction (LoadFunctionOp parent poly [] (FunctionType [] [HTFunc poly]))) - [HTFunc (PolyFuncType args _)] -> error $ "Unexpected type args to " ++ show funcDef ++ ": " ++ show args - _ -> error $ "Expected a function argument when loading thunk, got: " ++ show hTys + nod <- if extra_call + then addNode ("direct_call(" ++ show funcDef ++ ")") + (OpCall (CallOp parent (FunctionType [] hTys))) + -- We are loading idNode as a value (not an Eval'd thing), and it is a FuncDef directly + -- corresponding to a Brat TLD (not that produces said TLD when eval'd) + else case hTys of + [HTFunc poly@(PolyFuncType [] _)] -> + addNode ("load_thunk(" ++ show funcDef ++ ")") + (OpLoadFunction (LoadFunctionOp parent poly [] (FunctionType [] [HTFunc poly]))) + [HTFunc (PolyFuncType args _)] -> error $ unwords ["Unexpected type args to" + ,show funcDef ++ ":" + ,show args + ] + _ -> error $ "Expected a function argument when loading thunk, got: " ++ show hTys -- the only input pure $ Just (nod, [(Port funcDef 0, 0)]) compileNode in_edges = do @@ -386,7 +389,7 @@ compileWithInputs parent name = gets compiled <&> M.lookup name >>= \case Nothing -> do hole <- do st <- get - let h = (holes st) + let h = holes st put (st { holes = h :< name}) pure (length h) addNode ("hole " ++ show hole) (OpCustom (holeOp parent hole sig)) @@ -470,7 +473,7 @@ compileWithInputs parent name = gets compiled <&> M.lookup name >>= \case ins <- compilePorts ins outs <- compilePorts outs dfgId <- addNode "DidMatch_DFG" (OpDFG (DFG parent (FunctionType ins outs))) - inputNode <- addNode ("PatternMatch.Input") (OpIn (InputNode dfgId ins)) + inputNode <- addNode "PatternMatch.Input" (OpIn (InputNode dfgId ins)) ccOuts <- compileClauses dfgId (zip (Port inputNode <$> [0..]) ins) cs addNodeWithInputs "PatternMatch.Output" (OpOut (OutputNode dfgId (snd <$> ccOuts))) ccOuts [] pure dfgId @@ -508,7 +511,7 @@ getOutPort parent p@(Ex srcNode srcPort) = do trackM $ show lifted case M.lookup p lifted of Just intercept -> pure $ Just intercept - Nothing -> compileWithInputs parent srcNode <&> (\maybe -> maybe <&> (flip Port srcPort)) + Nothing -> compileWithInputs parent srcNode <&> (\maybe -> maybe <&> flip Port srcPort) -- Execute a compilation (which takes a DFG parent) in a nested monad; -- produce a Const node containing the resulting Hugr, and a LoadConstant, @@ -554,16 +557,16 @@ compileBratBox parent name (venv, src, tgt) cty = do src_id <- addNode ("LiftedCapturesInputs" ++ show name) (OpIn (InputNode dfg_id allInputTys)) -- Now map ports in the BRAT Graph to their Hugr equivalents. -- Each captured value is read from an element of src_id, starting from 0 - let lifted = ([(src, Port src_id i) | ((src, _ty), i) <- zip params [0..]] + let lifted = [(src, Port src_id i) | ((src, _ty), i) <- zip params [0..]] -- and the original BRAT-Graph Src outports become the Hugr Input node ports *after* the captured values - ++ [(Ex src i, Port src_id (i + length params)) | i <- [0..length inputTys]]) + ++ [(Ex src i, Port src_id (i + length params)) | i <- [0..length inputTys]] st <- get put $ st {liftedOutPorts = M.fromList lifted} -- no need to return any holes compileWithInputs dfg_id tgt -- Finally, we add a `Partial` node to supply the captured params. - partialNode <- addNode "Partial" (OpCustom $ partialOp parent (box_sig) (length params)) + partialNode <- addNode "Partial" (OpCustom $ partialOp parent box_sig (length params)) addEdge (fst templatePort, Port partialNode 0) edge_srcs <- for (map fst params) $ getOutPort parent pure (partialNode, zip (map fromJust edge_srcs) [1..]) @@ -669,7 +672,7 @@ compileMatchSequence parent portTable (MatchSequence {..}) = do undoPort <- undoPrimTest parent refined oldTy prevTest -- Put it back in the right place let (as, bs) = splitAt ix other - let ins = (as ++ undoPort : bs) + let ins = as ++ undoPort : bs makeRowTag "Fail_Undo" parent 0 sumTy ins allMatched :: NodeId -> [TypedPort] -> Compile [TypedPort] @@ -700,12 +703,12 @@ getSumVariants ty = error $ "Expected a sum type, got " ++ show ty -- This should only be called by the logic which creates conditionals, because -- wires that exist in the brat graph are already going to be added at the end. -addNodeWithInputs :: String -> (HugrOp NodeId) -> [TypedPort] +addNodeWithInputs :: String -> HugrOp NodeId -> [TypedPort] -> [HugrType] -- The types of the outputs -> Compile [TypedPort] -- The output wires addNodeWithInputs name op inWires outTys = do nodeId <- addNode name op - for (zip (fst <$> inWires) (Port nodeId <$> [0..])) addEdge + for_ (zip (fst <$> inWires) (Port nodeId <$> [0..])) addEdge pure $ zip (Port nodeId <$> [0..]) outTys makeConditional :: NodeId -- Parent node id @@ -720,7 +723,7 @@ makeConditional parent discrim otherInputs cases = do unless (allRowsEqual outTyss) (error "Conditional output types didn't match") - let condOp = (OpConditional (Conditional parent rows (snd <$> otherInputs) (head outTyss))) + let condOp = OpConditional (Conditional parent rows (snd <$> otherInputs) (head outTyss)) addOp condOp condId addEdge (fst discrim, Port condId 0) traverse_ addEdge (zip (fst <$> otherInputs) (Port condId <$> [1..])) @@ -734,7 +737,7 @@ makeConditional parent discrim otherInputs cases = do let outTys = snd <$> outs outId <- addNode ("Output" ++ name) (OpOut (OutputNode caseId outTys)) - for (zip (fst <$> outs) (Port outId <$> [0..])) addEdge + for_ (zip (fst <$> outs) (Port outId <$> [0..])) addEdge addOp (OpCase (ix, Case parent (FunctionType tys outTys))) caseId pure outTys @@ -749,7 +752,7 @@ compilePrimTest :: NodeId -> PrimTest HugrType -- The test to run -> Compile TypedPort compilePrimTest parent (port, ty) (PrimCtorTest c tycon unpackingNode outputs) = do - let sumOut = (HTSum (SG (GeneralSum [[ty], snd <$> outputs]))) + let sumOut = HTSum (SG (GeneralSum [[ty], snd <$> outputs])) let sig = FunctionType [ty] [sumOut] testId <- addNode ("PrimCtorTest " ++ show c) (OpCustom (CustomOp @@ -821,7 +824,7 @@ compileModule venv = do -- return the type of the Hugr FuncDefn, whether said FuncDefn requires an extra Call, -- and the procedure for compiling the contents of the FuncDefn for execution later, -- *after* all such FuncDefns have been registered - analyseDecl :: Name -> Compile (PolyFuncType, Bool, (NodeId -> Compile ())) + analyseDecl :: Name -> Compile (PolyFuncType, Bool, NodeId -> Compile ()) analyseDecl idNode = do (ns, es) <- gets bratGraph let srcPortTys = [(srcPort, ty) | (srcPort, ty, In tgt _) <- es, tgt == idNode ] @@ -831,7 +834,7 @@ compileModule venv = do case outs of [(_, VFun Braty cty)] -> do sig <- compileSig Braty cty - pure $ (sig, False, compileBox (src, tgt)) + pure (sig, False, compileBox (src, tgt)) [(_, VFun Kerny cty)] -> do -- We're compiling, e.g. -- f :: { Qubit -o Qubit } @@ -840,7 +843,7 @@ compileModule venv = do -- computation that produces this constant. We do so by making a FuncDefn -- that takes no arguments and produces the constant kernel graph value. thunkTy <- HTFunc <$> compileSig Kerny cty - pure $ (funcReturning [thunkTy], True, \parent -> + pure (funcReturning [thunkTy], True, \parent -> withIO parent thunkTy $ compileKernBox parent input (compileBox (src, tgt)) cty) _ -> error "Box should have exactly one output of Thunk type" _ -> do -- a computation, or several values @@ -857,7 +860,7 @@ compileModule venv = do -- top-level decls that are not Prims. RHS is the brat idNode decls :: [(UserName, Name)] decls = do -- in list monad, no Compile here - (fnName, wires) <- (M.toList venv) + (fnName, wires) <- M.toList venv let (Ex idNode _) = end (fst $ head wires) -- would be better to check same for all rather than just head case hasPrefix ["checking","globals","decl"] idNode of Just _ -> pure (fnName, idNode) -- assume all ports are 0,1,2... diff --git a/brat/Brat/Compiler.hs b/brat/Brat/Compiler.hs index a4e0a804..3414bc85 100644 --- a/brat/Brat/Compiler.hs +++ b/brat/Brat/Compiler.hs @@ -76,8 +76,8 @@ compileFile libDirs file = do env <- runExceptT $ loadFilename checkRoot libDirs file (venv, _, holes, defs, outerGraph) <- eitherIO env case holes of - [] -> Right <$> (evaluate -- turns 'error' into IO 'die' - $ compile defs newRoot outerGraph venv) + [] -> Right <$> evaluate -- turns 'error' into IO 'die' + (compile defs newRoot outerGraph venv) hs -> pure $ Left (CompilingHoles hs) compileAndPrintFile :: [FilePath] -> String -> IO () diff --git a/brat/Brat/Constructors.hs b/brat/Brat/Constructors.hs index 127c9185..bd3656fe 100644 --- a/brat/Brat/Constructors.hs +++ b/brat/Brat/Constructors.hs @@ -40,65 +40,65 @@ defaultConstructors = M.fromList ,(CInt, CArgs [] Zy R0 R0) ]) ,(CNil, M.fromList - [(CList, CArgs [VPVar] (Sy Zy) (REx ("elementType", Star []) (R0)) R0) - ,(CVec, CArgs [VPVar, VPNum NP0] (Sy Zy) (REx ("elementType", Star []) (R0)) R0) + [(CList, CArgs [VPVar] (Sy Zy) (REx ("elementType", Star []) R0) R0) + ,(CVec, CArgs [VPVar, VPNum NP0] (Sy Zy) (REx ("elementType", Star []) R0) R0) ,(CNil, CArgs [] Zy R0 R0) ]) ,(CCons, M.fromList [(CList, CArgs [VPVar] (Sy Zy) - (REx ("elementType", Star []) (R0)) + (REx ("elementType", Star []) R0) (RPr ("head", VApp (VInx VZ) B0) (RPr ("tail", TList (VApp (VInx VZ) B0)) R0))) ,(CVec, CArgs [VPVar, VPNum (NP1Plus NPVar)] (Sy (Sy Zy)) - (REx ("elementType", Star []) ((REx ("tailLength", Nat) (R0)))) + (REx ("elementType", Star []) (REx ("tailLength", Nat) R0)) (RPr ("head", VApp (VInx (VS VZ)) B0) (RPr ("tail", TVec (VApp (VInx (VS VZ)) B0) (VNum $ nVar (VInx VZ))) R0))) ,(CCons, CArgs [VPVar, VPCon (plain "nil") []] (Sy Zy) - (REx ("elementType", Star []) (R0)) + (REx ("elementType", Star []) R0) (RPr ("value", VApp (VInx VZ) B0) R0)) ,(CCons, CArgs [VPVar, VPVar] (Sy (Sy Zy)) (REx ("headTy", Star []) - ((REx ("tailTy", Star []) (R0)))) + (REx ("tailTy", Star []) R0)) (RPr ("head", VApp (VInx (VS VZ)) B0) (RPr ("tail", VApp (VInx VZ) B0) R0))) ]) ,(CSnoc, M.fromList [(CList, CArgs [VPVar] (Sy Zy) - (REx ("elementType", Star []) (R0)) + (REx ("elementType", Star []) R0) (RPr ("tail", TList (VApp (VInx VZ) B0)) (RPr ("head", VApp (VInx VZ) B0) R0))) ,(CVec, CArgs [VPVar, VPNum (NP1Plus NPVar)] (Sy (Sy Zy)) - (REx ("elementType", Star []) ((REx ("tailLength", Nat) (R0)))) + (REx ("elementType", Star []) (REx ("tailLength", Nat) R0)) (RPr ("tail", TVec (VApp (VInx (VS VZ)) B0) (VNum $ nVar (VInx VZ))) (RPr ("head", VApp (VInx (VS VZ)) B0) R0))) ]) ,(CConcatEqEven, M.fromList [(CVec, CArgs [VPVar, VPNum (NP2Times NPVar)] (Sy (Sy Zy)) -- Star should be a TypeFor m forall m? - (REx ("elementType", Star []) ((REx ("halfLength", Nat) (R0)))) + (REx ("elementType", Star []) (REx ("halfLength", Nat) R0)) (RPr ("lhs", TVec (VApp (VInx (VS VZ)) B0) (VApp (VInx VZ) B0)) (RPr ("rhs", TVec (VApp (VInx (VS VZ)) B0) (VApp (VInx VZ) B0)) R0))) ]) ,(CRiffle, M.fromList [(CVec, CArgs [VPVar, VPNum (NP2Times NPVar)] (Sy (Sy Zy)) -- Star should be a TypeFor m forall m? - (REx ("elementType", Star []) ((REx ("halfLength", Nat) (R0)))) + (REx ("elementType", Star []) (REx ("halfLength", Nat) R0)) (RPr ("evens", TVec (VApp (VInx (VS VZ)) B0) (VApp (VInx VZ) B0)) (RPr ("odds", TVec (VApp (VInx (VS VZ)) B0) (VApp (VInx VZ) B0)) R0))) ]) ,(CConcatEqOdd, M.fromList [(CVec, CArgs [VPVar, VPNum (NP1Plus (NP2Times NPVar))] (Sy (Sy Zy)) -- Star should be a TypeFor m forall m? - (REx ("elementType", Star []) ((REx ("halfLength", Nat) (R0)))) + (REx ("elementType", Star []) (REx ("halfLength", Nat) R0)) (RPr ("lhs", TVec (VApp (VInx (VS VZ)) B0) (VApp (VInx VZ) B0)) (RPr ("mid", VApp (VInx (VS VZ)) B0) (RPr ("rhs", TVec (VApp (VInx (VS VZ)) B0) (VApp (VInx VZ) B0)) R0)))) ]) ,(CNone, M.fromList - [(COption, CArgs [VPVar] (Sy Zy) (REx ("ty", Star []) (R0)) R0)]) + [(COption, CArgs [VPVar] (Sy Zy) (REx ("ty", Star []) R0) R0)]) ,(CSome, M.fromList [(COption, CArgs [VPVar] (Sy Zy) - (REx ("ty", Star []) (R0)) + (REx ("ty", Star []) R0) (RPr ("value", VApp (VInx VZ) B0) R0))]) ,(CTrue, M.fromList [(CBool, CArgs [] Zy R0 R0)]) ,(CFalse, M.fromList [(CBool, CArgs [] Zy R0 R0)]) @@ -107,17 +107,17 @@ defaultConstructors = M.fromList kernelConstructors :: ConstructorMap Kernel kernelConstructors = M.fromList [(CNil, M.fromList - [(CVec, CArgs [VPVar, VPNum NP0] (Sy Zy) (REx ("elementType", Dollar []) (R0)) R0)] + [(CVec, CArgs [VPVar, VPNum NP0] (Sy Zy) (REx ("elementType", Dollar []) R0) R0)] ) ,(CCons, M.fromList [(CVec, CArgs [VPVar, VPNum (NP1Plus NPVar)] (Sy (Sy Zy)) - (REx ("elementType", Dollar []) ((REx ("tailLength", Nat) (R0)))) + (REx ("elementType", Dollar []) (REx ("tailLength", Nat) R0)) (RPr ("head", VApp (VInx (VS VZ)) B0) (RPr ("tail", TVec (VApp (VInx (VS VZ)) B0) (VNum $ nVar (VInx VZ))) R0))) ]) ,(CSnoc, M.fromList [(CVec, CArgs [VPVar, VPNum (NP1Plus NPVar)] (Sy (Sy Zy)) - (REx ("elementType", Dollar []) ((REx ("tailLength", Nat) (R0)))) + (REx ("elementType", Dollar []) (REx ("tailLength", Nat) R0)) (RPr ("tail", TVec (VApp (VInx (VS VZ)) B0) (VNum $ nVar (VInx VZ))) (RPr ("head", VApp (VInx (VS VZ)) B0) R0))) ]) diff --git a/brat/Brat/Elaborator.hs b/brat/Brat/Elaborator.hs index d5024802..da34e09b 100644 --- a/brat/Brat/Elaborator.hs +++ b/brat/Brat/Elaborator.hs @@ -1,7 +1,7 @@ module Brat.Elaborator where -import Control.Arrow ((***)) import Control.Monad (forM, (>=>)) +import Data.Bifunctor (second) import Data.List.NonEmpty (NonEmpty(..)) import Data.Map (empty) @@ -26,7 +26,7 @@ assertChk s@(WC _ r) = case dir r of deepEmb :: WC (Raw Syn k) -> WC (Raw Chk k) deepEmb (WC fc (a ::|:: b)) = WC fc (deepEmb a ::|:: deepEmb b) deepEmb (WC fc (a ::-:: b)) = WC fc (a ::-:: deepEmb b) - deepEmb (WC fc (RLambda c cs)) = WC fc (RLambda ((id *** deepEmb) c) cs) + deepEmb (WC fc (RLambda c cs)) = WC fc (RLambda (second deepEmb c) cs) deepEmb (WC fc (RLet abs a b)) = WC fc (RLet abs a (deepEmb b)) deepEmb (WC fc (ROf num exp)) = WC fc (ROf num (deepEmb exp)) -- We like to avoid RTypedTh because the body doesn't know whether it's Brat or Kernel @@ -210,7 +210,7 @@ elabBody (FNoLhs e) _ = do e <- assertChk e case kind (unWC e) of Nouny -> pure $ NoLhs e - _ -> (assertUVerb e) >>= \e -> pure $ ThunkOf (WC (fcOf e) (NoLhs e)) + _ -> assertUVerb e >>= \e -> pure $ ThunkOf (WC (fcOf e) (NoLhs e)) elabBody FUndefined _ = pure Undefined elabFunDecl :: FDecl -> Either Error RawFuncDecl diff --git a/brat/Brat/Eval.hs b/brat/Brat/Eval.hs index 7d434d80..2fc40498 100644 --- a/brat/Brat/Eval.hs +++ b/brat/Brat/Eval.hs @@ -23,7 +23,7 @@ import Brat.UserName (plain) import Control.Monad.Freer (req) import Bwd import Hasochism -import Util (zip_same_length) +import Util (zipSameLength) import Data.Bifunctor (second) import Data.Functor @@ -34,7 +34,7 @@ kindType :: TypeKind -> Val Z kindType Nat = TNat kindType (TypeFor _ []) = VCon (plain "nil") [] kindType (TypeFor m ks) - = VFun Braty $ helper ks :->> (RPr ("type", kindType (TypeFor m [])) R0) + = VFun Braty $ helper ks :->> RPr ("type", kindType (TypeFor m [])) R0 where helper :: [(PortName, TypeKind)] -> Ro Brat Z Z helper [] = R0 @@ -68,7 +68,7 @@ evalCTy :: Stack Z Sem n -> Modey m -> CTy m n -> Checking (CTy m Z) -evalCTy stk my cty = quoteCTy Zy my stk cty +evalCTy stk my = quoteCTy Zy my stk sem :: Stack Z Sem n -- An environment for looking up VInxs -> Val n -- The thing we're evaluating @@ -123,16 +123,16 @@ quote lvy (SSum my ga ts) = VSum my <$> traverse quoteVariant ts quoteVariant (Some ro) = quoteRo my ga ro lvy >>= \case (_, Some (ro :* _)) -> pure (Some ro) -quoteCTy :: Ny lv -> Modey m -> Stack Z Sem n -> (CTy m n) -> Checking (CTy m lv) +quoteCTy :: Ny lv -> Modey m -> Stack Z Sem n -> CTy m n -> Checking (CTy m lv) quoteCTy lvy my ga (ins :->> outs) = quoteRo my ga ins lvy >>= \case (ga', Some (ins' :* lvy')) -> quoteRo my ga' outs lvy' >>= \case - (_, Some (outs' :* _)) -> pure $ (ins' :->> outs') + (_, Some (outs' :* _)) -> pure (ins' :->> outs') -- first number is next Lvl to use in Value -- require every Lvl in Sem is < n (converted by n - 1 - lvl), else must fail at runtime quoteVar :: Ny n -> SVar -> VVar n quoteVar _ (SPar end) = VPar end -- no need to chase, done in semVar -quoteVar ny (SLvl lvl) = VInx $ helper ny $ (ny2int ny) - 1 - lvl +quoteVar ny (SLvl lvl) = VInx $ helper ny $ ny2int ny - 1 - lvl where helper :: Ny n -> Int -> Inx n helper Zy _ = error "Level out of bounds" @@ -215,7 +215,7 @@ getNum (SNum num) = num getNum _ = error "Should have checked kind == Num already" dropRight :: Either e r -> Either e () -dropRight = second (\_ -> ()) +dropRight = second (const ()) eqWorker :: String -- for error message -> (Ny :* Stack Z TypeKind) lv -- next Level & kinds for existing Levels @@ -251,7 +251,7 @@ eqWorker tm lvkz (Star []) (SFun m0 stk0 (ins0 :->> outs0)) (SFun m1 stk1 (ins1 Left msg -> pure (Left msg) Right (Some lvkz, stk0, stk1) -> eqRowTest m0 tm lvkz (stk0, outs0) (stk1, outs1) <&> dropRight eqWorker tm lvkz (TypeFor _ []) (SSum m0 stk0 rs0) (SSum m1 stk1 rs1) - | Just Refl <- testEquality m0 m1 = case zip_same_length rs0 rs1 of + | Just Refl <- testEquality m0 m1 = case zipSameLength rs0 rs1 of Nothing -> pure (Left (TypeErr "Mismatched sum lengths")) Just rs -> traverse eqVariant rs <&> sequence_ where @@ -292,7 +292,7 @@ eqRowTest m tm (lvy :* kz) (stk0, REx (_, k0) r0) (stk1, REx (_, k1) r1) = eqRowTest m tm _ exp act = modily m $ pure . Left $ TypeMismatch tm (show exp) (show act) eqTests :: String -> (Ny :* Stack Z TypeKind) n -> [TypeKind] -> [Sem] -> [Sem] -> Checking (Either ErrorMsg ()) - -- note alternative - traverse zip3/zip_same_len*2 + currying + -- note alternative - traverse zip3/zipSameLen*2 + currying -- to get [Either ErrorMsg ()], then sequenceA -> Either ErrorMsg [()] eqTests tm lvkz = go where diff --git a/brat/Brat/Graph.hs b/brat/Brat/Graph.hs index 5e46e93e..ad0cf617 100644 --- a/brat/Brat/Graph.hs +++ b/brat/Brat/Graph.hs @@ -115,7 +115,7 @@ toGraph (ns, ws) = G.graphFromEdges adj wiresFrom :: Name -> Graph -> [Wire] wiresFrom src (_, ws) = [ w | w@(Ex a _, _, _) <- ws, a == src ] -lookupNode :: Name -> Graph -> Maybe (Node) +lookupNode :: Name -> Graph -> Maybe Node lookupNode name (ns, _) = M.lookup name ns wireStart :: Wire -> Name diff --git a/brat/Brat/Lexer/Flat.hs b/brat/Brat/Lexer/Flat.hs index 311e1b47..1f41d5ba 100644 --- a/brat/Brat/Lexer/Flat.hs +++ b/brat/Brat/Lexer/Flat.hs @@ -41,11 +41,10 @@ qualified :: Lexer Tok qualified = ( "qualified name") $ do first <- ident <* string "." rest <- many (try $ ident <* string ".") - last <- ident - pure (QualifiedId (first :| rest) last) + QualifiedId (first :| rest) <$> ident space :: Lexer () -space = (many $ (satisfy isSpace >> return ()) <|> comment) >> return () +space = many ((satisfy isSpace >> return ()) <|> comment) >> return () where comment :: Lexer () comment = string "--" *> ((printChar `manyTill` lookAhead (void newline <|> void eof)) >> return ()) @@ -118,4 +117,4 @@ convPos :: SourcePos -> Pos convPos (SourcePos _ l c) = Pos (unPos l) (unPos c) lexFlat :: Lexer [Token] -lexFlat = token `manyTill` (try $ space >> eof) +lexFlat = token `manyTill` try (space >> eof) diff --git a/brat/Brat/Lexer/Token.hs b/brat/Brat/Lexer/Token.hs index 33ddbad6..d5f8842b 100644 --- a/brat/Brat/Lexer/Token.hs +++ b/brat/Brat/Lexer/Token.hs @@ -102,7 +102,7 @@ instance Eq Token where (Token fc t) == (Token fc' t') = t == t' && fc == fc' instance Show Token where - show (Token _ t) = (show t) ++ " " + show (Token _ t) = show t ++ " " instance Ord Token where compare (Token (FC st nd) _) (Token (FC st' nd') _) = if st == st' then compare nd nd' @@ -129,5 +129,5 @@ tokLen :: Tok -> Int tokLen = length . show instance VisualStream [Token] where - showTokens _ ts = concatMap show ts tokensLength _ = sum . fmap (\(Token _ t) -> tokLen t) + showTokens _ = concatMap show diff --git a/brat/Brat/Load.hs b/brat/Brat/Load.hs index 0e16e288..e427246e 100644 --- a/brat/Brat/Load.hs +++ b/brat/Brat/Load.hs @@ -28,6 +28,7 @@ import Control.Exception (assert) import Control.Monad (filterM, foldM, forM, forM_, unless) import Control.Monad.Except import Control.Monad.Trans.Class (lift) +import Data.Functor ( (<&>), ($>) ) import Data.List (sort) import Data.List.HT (viewR) import Data.List.NonEmpty (NonEmpty(..)) @@ -38,7 +39,6 @@ import System.Directory (doesFileExist) import System.FilePath import Prelude hiding (last) -import Data.Functor (($>)) -- A Module is a node in the dependency graph type FlatMod = ((FEnv, String) -- data at the node: declarations, and file contents @@ -108,7 +108,7 @@ checkDecl pre (VDecl FuncDecl{..}) to_define = (fnName -!) $ localFC fnLoc $ do getFunTy :: Some (Ro m Z) -> Checking (Maybe (Some (Modey :* Flip CTy Z))) getFunTy (Some (RPr (_, VFun my cty) R0)) = pure $ Just (Some (my :* Flip cty)) getFunTy (Some R0) = err $ EmptyRow name - getFunTy _ = pure $ Nothing + getFunTy _ = pure Nothing uname = PrefixName pre fnName name = show uname @@ -116,7 +116,7 @@ checkDecl pre (VDecl FuncDecl{..}) to_define = (fnName -!) $ localFC fnLoc $ do loadAlias :: TypeAlias -> Checking (UserName, 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 (:||:) AEmpty (APat . Bind . fst <$> args) + let abs = WC fc $ foldr ((:||:) . APat . Bind . fst) AEmpty args ([v], unders) <- kindCheck [(hhungry, k)] $ Th (WC fc (Lambda (abs, WC fc body) [])) ensureEmpty "loadAlias unders" unders pure (name, (args, v)) @@ -141,7 +141,7 @@ loadStmtsWithEnv ns (venv, oldDecls, oldEndData) (fname, pre, stmts, cts) = addS (entries, (_holes, kcStore, kcGraph)) <- run venv initStore globalNS $ withAliases aliases $ forM decls $ \d -> localFC (fnLoc d) $ do let name = PrefixName pre (fnName d) - (thing, ins :->> outs, sig, prefix) <- case (fnLocality d) of + (thing, ins :->> outs, sig, prefix) <- case fnLocality d of Local -> do -- kindCheckAnnotation gives the signature of an Id node, -- hence ins == outs (modulo haskell's knowledge about their scopes) @@ -198,14 +198,14 @@ loadFiles ns (cwd :| extraDirs) fname contents = do -- Validate imports liftEither . addSrcContext fname contents $ forM_ files (validateImports . f) - let allStmts = (getStmts . f) <$> files + let allStmts = getStmts . f <$> files -- remove the prefix for the starting file allStmts' <- case viewR allStmts of -- the original file should be at the end of the allStmts list Just (rest, (_, mainPrf, mainStmts, mainCts)) -> do unless (mainPrf == [fname]) $ throwError (SrcErr "" $ dumbErr (InternalError "Top of dependency graph wasn't main file")) - deps <- for rest $ \(uname,b,c,d) -> findFile uname >>= pure . (,b,c,d) + deps <- for rest $ \(uname,b,c,d) -> findFile uname <&> (,b,c,d) let main = (cwd fname ++ ".brat", [], mainStmts, mainCts) pure (deps ++ [main]) Nothing -> throwError (SrcErr "" $ dumbErr (InternalError "Empty dependency graph")) @@ -217,7 +217,7 @@ loadFiles ns (cwd :| extraDirs) fname contents = do allStmts' where -- builds a map from Import to (index in which discovered, module) - depGraph :: (M.Map Import (Int, FlatMod)) -- input map to which to add + depGraph :: M.Map Import (Int, FlatMod) -- input map to which to add -> Import -> String -> ExceptT SrcErr IO (M.Map Import (Int, FlatMod)) depGraph visited imp cts = let name = unWC (importName imp) in @@ -266,7 +266,7 @@ loadFiles ns (cwd :| extraDirs) fname contents = do (x:_) -> pure x nameToFile :: FilePath -> UserName -> String - nameToFile dir (PrefixName ps file) = dir (foldr () file ps) ++ ".brat" + nameToFile dir (PrefixName ps file) = dir foldr () file ps ++ ".brat" checkNoCycles :: [(Int, FlatMod)] -> Either SrcErr () checkNoCycles mods = diff --git a/brat/Brat/Parser.hs b/brat/Brat/Parser.hs index 0c605e5a..4522b7cd 100644 --- a/brat/Brat/Parser.hs +++ b/brat/Brat/Parser.hs @@ -164,12 +164,12 @@ abstractor = do ps <- many (try portPull) pure $ if null ps then xs else APull ps xs where binding :: Parser Abstractor - binding = (try (APat <$> bigPat) <|> round abstractor) - vecPat = square (binding `sepBy` (match Comma)) >>= list2Cons + binding = try (APat <$> bigPat) <|> round abstractor + vecPat = square (binding `sepBy` match Comma) >>= list2Cons list2Cons :: [Abstractor] -> Parser Pattern list2Cons [] = pure PNil - list2Cons (APat x:xs) = PCons x <$> (list2Cons xs) + list2Cons (APat x:xs) = PCons x <$> list2Cons xs list2Cons _ = customFailure (Custom "Internal error list2Cons") portPull = simpleName <* match PortColon @@ -200,7 +200,7 @@ abstractor = do ps <- many (try portPull) <|> try constructorsWithArgs <|> try nullaryConstructors <|> (Bind <$> simpleName) - <|> (round bigPat) + <|> round bigPat where constructor :: Parser Abstractor -> String -> Parser Pattern constructor pabs c = do @@ -292,14 +292,14 @@ functionType = try (RFn <$> ctype) <|> (RKernel <$> kernel) vec :: Parser Flat vec = (\(WC fc x) -> unWC $ vec2Cons (end fc) x) <$> withFC (square elems) where - elems = (element `chainl1` (try vecComma)) <|> pure [] + elems = (element `chainl1` try vecComma) <|> pure [] vecComma = match Comma $> (++) element = (:[]) <$> withFC (expr' (succ PJuxtPull)) mkNil fc = FCon (plain "nil") (WC fc FEmpty) vec2Cons :: Pos -> [WC Flat] -> WC Flat -- The nil element gets as FC the closing ']' of the [li,te,ral] - vec2Cons end [] = let fc = FC end{col=(col end)-1} end in WC fc (mkNil fc) + vec2Cons end [] = let fc = FC end{col=col end-1} end in WC fc (mkNil fc) -- We give each cell of the list an FC which starts with the FC -- of its head element and ends at the end of the list (the closing ']') vec2Cons end (x:xs) = let fc = FC (start $ fcOf x) end in @@ -333,7 +333,7 @@ cthunk = try bratFn <|> try kernel <|> thunk -- If we don't have a `=>` at the start of a kernel, it could (and should) -- be a verb, not the RHS of a no-arg lambda (e', n) -> let abs = braceSectionAbstractor [0..n-1] in - pure $ FLambda (((WC (fcOf e) abs), e') :| []) -- TODO: Which FC to use for the abstracor? + pure $ FLambda ((WC (fcOf e) abs, e') :| []) -- TODO: Which FC to use for the abstracor? replaceU :: WC Flat -> State Int (WC Flat) replaceU (WC fc x) = WC fc <$> replaceU' x @@ -421,7 +421,7 @@ expr' p = choice $ (try . getParser <$> enumFrom p) ++ [atomExpr] lhs <- withFC (subExpr POf) optional (kmatch KOf) >>= \case Nothing -> pure (unWC lhs) - Just () -> FOf lhs <$> (withFC ofExpr) + Just () -> FOf lhs <$> withFC ofExpr mkJuxt [x] = x mkJuxt (x:xs) = let rest = mkJuxt xs in WC (FC (start (fcOf x)) (end (fcOf rest))) (FJuxt x rest) @@ -470,9 +470,9 @@ expr' p = choice $ (try . getParser <$> enumFrom p) ++ [atomExpr] rhs <- withFC (subExpr (pred PInto)) pure $ FInto (WC lhs FEmpty) rhs - into = unWC <$> withFC (subExpr PInto) `chainl1` (divider Into FInto) + into = unWC <$> withFC (subExpr PInto) `chainl1` divider Into FInto - composition = unWC <$> withFC (subExpr PComp) `chainl1` (divider Semicolon FCompose) + composition = unWC <$> withFC (subExpr PComp) `chainl1` divider Semicolon FCompose divider :: Tok -> (WC Flat -> WC Flat -> Flat) -> Parser (WC Flat -> WC Flat -> WC Flat) divider tok f = token0 $ \case @@ -522,8 +522,7 @@ cnoun pe = do Left err -> fail (showError err) Right (SomeRaw r) -> case do r <- assertChk r - r <- assertNoun r - pure r + assertNoun r of Left err -> fail (showError err) Right r -> pure r @@ -565,18 +564,18 @@ decl = do class FCStream a where getFC :: Int -> PosState a -> FC -sp_to_fc :: SourcePos -> FC -sp_to_fc (SourcePos _ line col) = let +spToFC :: SourcePos -> FC +spToFC (SourcePos _ line col) = let l = unPos line c = unPos col in FC (Pos l c) (Pos l (c + 1)) instance FCStream String where - getFC os pst = let (_, pst') = reachOffset os pst in sp_to_fc $ pstateSourcePos pst' + getFC os pst = let (_, pst') = reachOffset os pst in spToFC $ pstateSourcePos pst' instance FCStream [Token] where getFC o PosState{..} = case drop (o - pstateOffset) pstateInput of - [] -> sp_to_fc pstateSourcePos + [] -> spToFC pstateSourcePos (Token fc _):_ -> fc parseFile :: String -> String -> Either SrcErr ([Import], FEnv) @@ -589,16 +588,14 @@ parseFile fname contents = addSrcContext fname contents $ do wrapParseErr wrapper er = let -- TODO: return all of the errors? There is generally only one. e :| errs = bundleErrors er - prettyErr = (parseErrorTextPretty e) ++ case errs of + prettyErr = parseErrorTextPretty e ++ case errs of [] -> "" - xs -> " and " ++ (show $ length xs) ++ " other errors" + xs -> " and " ++ show (length xs) ++ " other errors" fc = getFC (errorOffset e) (bundlePosState er) in Err (Just fc) $ wrapper (PE prettyErr) clauses :: String -> Parser (NonEmpty (WC Abstractor, WC Flat)) -clauses declName = label "clauses" $ - fmap (fromJust . nonEmpty) $ - some (try branch) +clauses declName = label "clauses" (fromJust . nonEmpty <$> some (try branch)) where branch = do label (declName ++ "(...) = ...") $ @@ -614,8 +611,7 @@ pimport = do kmatch KImport x <- withFC userName a <- alias - s <- selection - pure (Import x (not o) a s) + Import x (not o) a <$> selection where open :: Parser Bool open = optional (matchString "open") >>= \case @@ -645,13 +641,13 @@ pstmt = ((comment "comment") <&> \_ -> ([] , [])) where alias :: Parser RawAlias alias = withFC aliasContents <&> - \(WC fc (name, args, ty)) -> (TypeAlias fc name args ty) + \(WC fc (name, args, ty)) -> TypeAlias fc name args ty aliasContents :: Parser (UserName, [(String, TypeKind)], RawVType) aliasContents = do match (K KType) alias <- userName - args <- option [] $ round $ (simpleName `sepBy` (match Comma)) + args <- option [] $ round (simpleName `sepBy` match Comma) {- future stuff args <- option [] $ round $ (`sepBy` (match Comma)) $ do port <- port diff --git a/brat/Brat/Syntax/Abstractor.hs b/brat/Brat/Syntax/Abstractor.hs index ee18099f..91e96d35 100644 --- a/brat/Brat/Syntax/Abstractor.hs +++ b/brat/Brat/Syntax/Abstractor.hs @@ -55,14 +55,14 @@ data Abstractor | Abstractor :||: Abstractor -- Pull port name being abstracted to the front -- b:x, c:y, z -> ... - | APull [PortName] (Abstractor) + | APull [PortName] Abstractor | APat Pattern deriving Eq -instance Show (Abstractor) where +instance Show Abstractor where show AEmpty = "" show (x :||: y) = show x ++ ", " ++ show y - show (APull ps abs) = concat ((++":") <$> ps) ++ show abs + show (APull ps abs) = concatMap (++":") ps ++ show abs show (APat p) = show p occursInAbstractor :: String -> Abstractor -> Bool diff --git a/brat/Brat/Syntax/Core.hs b/brat/Brat/Syntax/Core.hs index 2b45872a..1e9b019f 100644 --- a/brat/Brat/Syntax/Core.hs +++ b/brat/Brat/Syntax/Core.hs @@ -119,7 +119,7 @@ instance Show (Term d k) where show (fun :$: arg) = bracket PApp fun ++ ('(' : show arg ++ ")") show (tm ::: ty) = bracket PAnn tm ++ " :: " ++ show ty show (a :-: b) = bracket PComp a ++ "; " ++ bracket PComp b - show (Lambda c cs) = unlines $ (showClause c : (("| "++) . showClause <$> cs)) + show (Lambda c cs) = unlines (showClause c : (("| "++) . showClause <$> cs)) where showClause (xs, bod) = show xs ++ " => " ++ bracket PLambda bod show p@(Con c arg) = case prettyPat p of @@ -130,7 +130,7 @@ instance Show (Term d k) where where prettyPat :: Term Chk Noun -> Maybe [Term Chk Noun] prettyPat (Con (PrefixName [] "nil") (WC _ Empty)) = Just [] - prettyPat (Con (PrefixName [] "cons") (WC _ (x :|: xs))) = ((unWC x) :) <$> prettyPat (unWC xs) + prettyPat (Con (PrefixName [] "cons") (WC _ (x :|: xs))) = (unWC x :) <$> prettyPat (unWC xs) prettyPat _ = Nothing show (C f) = "{" ++ show f ++ "}" @@ -147,7 +147,7 @@ bracket n (WC _ tm) = case precedence tm of -- Report tightness of binding, or `Nothing` if not a binary op precedence :: Term d k -> Maybe Precedence -precedence (Let _ _ _) = Just PLetIn +precedence (Let {}) = Just PLetIn precedence (Lambda _ _) = Just PLambda precedence (_ :-: _) = Just PComp precedence (Pull _ _) = Just PJuxtPull diff --git a/brat/Brat/Syntax/Raw.hs b/brat/Brat/Syntax/Raw.hs index 126cd815..ca707b0d 100644 --- a/brat/Brat/Syntax/Raw.hs +++ b/brat/Brat/Syntax/Raw.hs @@ -112,14 +112,14 @@ instance Show (Raw d k) where show (RForget kv) = "(Forget " ++ show kv ++ ")" show (REmb x) = '「' : show x ++ "」" show (RPull [] x) = "[]:" ++ show x - show (RPull ps x) = concat ((++":") <$> ps) ++ show x + show (RPull ps x) = concatMap (++":") ps ++ show x show (RVar x) = show x show RIdentity = "|" show (RArith op a b) = "(" ++ show op ++ " " ++ show a ++ " " ++ show b ++ ")" show (fun ::$:: arg) = show fun ++ ('(' : show arg ++ ")") show (tm ::::: ty) = show tm ++ " :: " ++ show ty show (a ::-:: b) = show a ++ "; " ++ show b - show (RLambda c cs) = unlines $ (showClause c : (("| "++) . showClause <$> cs)) + show (RLambda c cs) = unlines (showClause c : (("| "++) . showClause <$> cs)) where showClause :: forall d k. (WC Abstractor, WC (Raw d k)) -> String showClause (abs, bod) = show abs ++ " => " ++ show bod @@ -215,12 +215,12 @@ instance (Kindable k) => Desugarable (Raw d k) where table of either known constructors or known type aliases. We must transform these into `Con c arg` when desugaring. -} - desugar' (REmb syn) = case (unWC syn) of + desugar' (REmb syn) = case unWC syn of (WC _ (RForce (WC _ (RVar c)))) ::$:: a -> do isConOrAlias c >>= \case - True -> case (kind $ unWC a) of + True -> case kind $ unWC a of Nouny -> Con c <$> desugar a - _ -> throwError $ desugarErr ("Constructor applied to something that isn't a noun") + _ -> throwError $ desugarErr "Constructor applied to something that isn't a noun" False -> Emb <$> desugar syn (RVar c) -> do isConOrAlias c >>= \case @@ -239,7 +239,7 @@ instance (Kindable k) => Desugarable (Raw d k) where (tys, ()) <- desugarBind outputs $ pure () pure (tm ::: tys) desugar' (syn ::-:: verb) = (:-:) <$> desugar syn <*> desugar verb - desugar' (RLambda c cs) = Lambda <$> (id **^ desugar) c <*> (traverse (id **^ desugar) cs) + desugar' (RLambda c cs) = Lambda <$> (id **^ desugar) c <*> traverse (id **^ desugar) cs desugar' (RLet abs thing body) = Let abs <$> desugar thing <*> desugar body desugar' (RCon c arg) = Con c <$> desugar arg desugar' (RFn cty) = C <$> desugar' cty diff --git a/brat/Brat/Syntax/Value.hs b/brat/Brat/Syntax/Value.hs index c3b1e9cb..d5557f90 100644 --- a/brat/Brat/Syntax/Value.hs +++ b/brat/Brat/Syntax/Value.hs @@ -42,7 +42,7 @@ instance MODEY Brat => Show VDecl where where aux :: FuncDecl (Some (Ro Brat Z)) body -> FuncDecl String body aux (FuncDecl { .. }) = case fnSig of - Some sig -> FuncDecl { fnName = fnName, fnSig = (show sig), fnBody = fnBody, fnLoc = fnLoc, fnLocality = fnLocality } + Some sig -> FuncDecl { fnName = fnName, fnSig = show sig, fnBody = fnBody, fnLoc = fnLoc, fnLocality = fnLocality } ------------------------------------ Variable Indices ------------------------------------ -- Well scoped de Bruijn indices @@ -56,7 +56,7 @@ instance Show (Inx n) where where toNat :: forall n. Inx n -> Int toNat VZ = 0 - toNat (VS n) = 1 + (toNat n) + toNat (VS n) = 1 + toNat n data AddR :: N -> N -> N -> Type where AddZ :: Ny out -> AddR out Z out @@ -71,7 +71,7 @@ outOrInn (AddZ _) inx = Left inx outOrInn (AddS _) (VZ {- :: Inx (S tot) -}) = Right (VZ {- Inx (S inn) -}) outOrInn (AddS a) (VS inx) = case outOrInn a inx of -- inx is inner, put the VS back - Right (inx {- :: Inx inn -}) -> Right ((VS inx) {- :: Inx (S inn) -}) + Right (inx {- :: Inx inn -}) -> Right (VS inx {- :: Inx (S inn) -}) -- inx is outer, we don't care how many inner vars we passed to get to it Left (inx {- :: Inx out -}) -> Left (inx {- :: Inx out -}) @@ -291,7 +291,7 @@ instance Show x => Show (StrictMono x) where show (StrictMono 0 m) = show m show (StrictMono n m) = let a = "2^" ++ show n b = show (2 ^ n :: Int) - in (minimumBy (comparing length) [b,a]) ++ " * " ++ show m + in minimumBy (comparing length) [b,a] ++ " * " ++ show m data Monotone x = Linear x @@ -315,7 +315,7 @@ instance NumFun Fun00 where calculate Constant0 = 0 calculate (StrictMonoFun mono) = calculate mono - numValue fun00 = NumValue 0 fun00 + numValue = NumValue 0 instance NumFun StrictMono where calculate StrictMono{..} = (2 ^ multBy2ToThe) * calculate monotone @@ -514,7 +514,7 @@ instance DeBruijn VVar where instance DeBruijn Val where changeVar vc (VNum n) = VNum (fmap (changeVar vc) n) - changeVar vc (VCon c vs) = VCon c ((changeVar vc) <$> vs) + changeVar vc (VCon c vs) = VCon c (changeVar vc <$> vs) changeVar vc (VApp v ss) = VApp (changeVar vc v) (changeVar vc <$> ss) changeVar vc (VLam sc) = VLam (changeVar (weakenVC vc) sc) @@ -559,7 +559,7 @@ endVal' Kerny _ e = KVar (VPar e) endVal :: TypeKind -> End -> Val Z endVal k e = varVal k (VPar e) -varVal :: TypeKind -> (VVar n) -> Val n +varVal :: TypeKind -> VVar n -> Val n varVal Nat v = VNum (nVar v) varVal _ v = VApp v B0 diff --git a/brat/Brat/UserName.hs b/brat/Brat/UserName.hs index 22897ce4..88ec5093 100644 --- a/brat/Brat/UserName.hs +++ b/brat/Brat/UserName.hs @@ -12,4 +12,4 @@ instance Show UserName where show (PrefixName ps file) = intercalate "." (ps ++ [file]) plain :: String -> UserName -plain n = PrefixName [] n +plain = PrefixName [] diff --git a/brat/Data/Hugr.hs b/brat/Data/Hugr.hs index 69ccb2ed..4eba111e 100644 --- a/brat/Data/Hugr.hs +++ b/brat/Data/Hugr.hs @@ -244,7 +244,7 @@ instance Show CustomConst where show (CC tag cts) = "Const(" ++ tag ++ ")(" ++ show cts ++ ")" instance ToJSON CustomConst where - toJSON (CC tag cts) = object ["c" .= (pack tag) + toJSON (CC tag cts) = object ["c" .= pack tag ,"v" .= cts ] @@ -423,7 +423,7 @@ instance ToJSON node => ToJSON (CallOp node) where toJSON (CallOp parent signature_) = object ["parent" .= parent ,"op" .= ("Call" :: Text) - ,"func_sig" .= (PolyFuncType [] signature_) + ,"func_sig" .= PolyFuncType [] signature_ ,"type_args" .= ([] :: [TypeArg]) ,"instantiation" .= signature_ ] @@ -591,7 +591,7 @@ getParent (OpDefn (FuncDefn { parent = parent })) = parent getParent (OpConst (ConstOp { parent = parent })) = parent getParent (OpDFG (DFG { parent = parent })) = parent getParent (OpConditional (Conditional { parent = parent })) = parent -getParent (OpCase (_, (Case { parent = parent }))) = parent +getParent (OpCase (_, Case { parent = parent })) = parent getParent (OpIn (InputNode { parent = parent })) = parent getParent (OpOut (OutputNode { parent = parent })) = parent getParent (OpTag (TagOp { parent = parent })) = parent diff --git a/brat/Util.hs b/brat/Util.hs index 456da740..a1e7ea58 100644 --- a/brat/Util.hs +++ b/brat/Util.hs @@ -1,9 +1,9 @@ module Util where -zip_same_length :: [a] -> [b] -> Maybe [(a,b)] -zip_same_length (x:xs) (y:ys) = ((x,y):) <$> zip_same_length xs ys -zip_same_length [] [] = Just [] -zip_same_length _ _ = Nothing +zipSameLength :: [a] -> [b] -> Maybe [(a,b)] +zipSameLength (x:xs) (y:ys) = ((x,y):) <$> zipSameLength xs ys +zipSameLength [] [] = Just [] +zipSameLength _ _ = Nothing lookupBy :: (a -> Bool) -> (a -> b) -> [a] -> Maybe b lookupBy _ _ [] = Nothing @@ -18,7 +18,7 @@ duplicatesWith :: Eq b => (a -> b) -> [a] -> [a] duplicatesWith f xs = let (_, dups, _) = aux ([], [], xs) in dups where aux (visited, dups, []) = (visited, dups, []) - aux (visited, dups, (x:xs)) | f x `elem` visited = aux (visited, x:dups, xs) + aux (visited, dups, x:xs) | f x `elem` visited = aux (visited, x:dups, xs) | otherwise = aux (f x:visited, dups, xs) duplicates :: Eq a => [a] -> [a] diff --git a/brat/app/Main.hs b/brat/app/Main.hs index 8a247365..bac393b7 100644 --- a/brat/app/Main.hs +++ b/brat/app/Main.hs @@ -24,7 +24,7 @@ dotOption = strOption (long "dot" <> value "" <> help "Write graph in Dot format libOption = strOption (long "lib" <> value "" <> help "Look in extra directories for libraries (delimited with ;)") opts :: Parser Options -opts = Opt <$> astFlag <*> dotOption <*> compileFlag <*> (strArgument (metavar "FILE")) <*> libOption <*> rawFlag +opts = Opt <$> astFlag <*> dotOption <*> compileFlag <*> strArgument (metavar "FILE") <*> libOption <*> rawFlag -- Parse a list of library directories delimited by a semicolon parseLibs :: String -> [String] diff --git a/brat/lsp/Brat/LSP/Find.hs b/brat/lsp/Brat/LSP/Find.hs index 65b533fe..098ba526 100644 --- a/brat/lsp/Brat/LSP/Find.hs +++ b/brat/lsp/Brat/LSP/Find.hs @@ -3,7 +3,7 @@ module Brat.LSP.Find (Context(..), getInfo) where import Data.List.NonEmpty (NonEmpty(..), toList) -import Data.Maybe (catMaybes) +import Data.Maybe (mapMaybe) import Brat.FC import Brat.LSP.State @@ -54,7 +54,7 @@ getInfo ps pos getThing :: Pos -> WC Flat -> Maybe Flat getThing pos (WC fc x) - | pos `inside` fc = case catMaybes (getThing pos <$> subTerms x) of + | pos `inside` fc = case mapMaybe (getThing pos) (subTerms x) of [] -> Just x -- xs should be the empty list, but I don't think it's -- worth crashing the server over diff --git a/brat/lsp/Driver.hs b/brat/lsp/Driver.hs index 5192af16..63f09d85 100644 --- a/brat/lsp/Driver.hs +++ b/brat/lsp/Driver.hs @@ -104,7 +104,7 @@ loadVFile state _ msg = do . uri let fileName = toNormalizedUri fileUri file <- getVirtualFile fileName - let cwd = fromMaybe "" $ dropFileName <$> (uriToFilePath fileUri) + let cwd = maybe "" dropFileName (uriToFilePath fileUri) case file of Just (VirtualFile _version str rope) -> do let file = unpack $ toText rope diff --git a/brat/test/Test/Abstractor.hs b/brat/test/Test/Abstractor.hs index d1b08f72..652e160a 100644 --- a/brat/test/Test/Abstractor.hs +++ b/brat/test/Test/Abstractor.hs @@ -19,7 +19,7 @@ abstractor n = oneof ,chooseInt (0,n) >>= \m -> (:||:) <$> abstractor m <*> abstractor (n - m) ] where - portname = arbitrary <&> \n -> names !! (abs n) + portname = arbitrary <&> \n -> names !! abs n instance Arbitrary Abstractor where arbitrary = sized abstractor @@ -49,10 +49,10 @@ instance Arbitrary Pattern where ] con n = oneof [pure PNone ,pure PNil - ,PSome <$> (pat (n - 1)) - ,POnePlus <$> (pat (n - 1)) - ,PTwoTimes <$> (pat (n - 1)) - ,PCons <$> (pat (n `div` 2)) <*> (pat (n `div` 2)) + ,PSome <$> pat (n - 1) + ,POnePlus <$> pat (n - 1) + ,PTwoTimes <$> pat (n - 1) + ,PCons <$> pat (n `div` 2) <*> pat (n `div` 2) ] idempotency :: Abstractor -> Bool diff --git a/brat/test/Test/Checking.hs b/brat/test/Test/Checking.hs index ef0bc352..cdcc1302 100644 --- a/brat/test/Test/Checking.hs +++ b/brat/test/Test/Checking.hs @@ -28,4 +28,4 @@ parseAndCheck libDirs file = testCase (show file) $ do case env of Left err -> assertFailure (show err) Right (venv, nouns, holes, _, _) -> - ((length venv) + (length nouns) + (length holes) > 0) @? "Should produce something" + (length venv + length nouns + length holes > 0) @? "Should produce something" diff --git a/brat/test/Test/Compile/Hugr.hs b/brat/test/Test/Compile/Hugr.hs index 3698d035..11de7093 100644 --- a/brat/test/Test/Compile/Hugr.hs +++ b/brat/test/Test/Compile/Hugr.hs @@ -28,7 +28,7 @@ invalidExamples = map ((++ ".brat") . ("examples" )) -- examples that we expect not to compile. -- Note this does not include those with remaining holes; these are automatically skipped. -nonCompilingExamples = (expectedCheckingFails ++ expectedParsingFails ++ +nonCompilingExamples = expectedCheckingFails ++ expectedParsingFails ++ map ((++ ".brat") . ("examples" )) ["fzbz" ,"ising" @@ -48,7 +48,7 @@ nonCompilingExamples = (expectedCheckingFails ++ expectedParsingFails ++ ,"rus" ,"teleportation" ,"vlup_covering" - ]) + ] compileToOutput :: FilePath -> TestTree compileToOutput file = testCaseInfo (show file) $ compileFile [] file >>= \case diff --git a/brat/test/Test/Elaboration.hs b/brat/test/Test/Elaboration.hs index 58611a78..0b9ab7e3 100644 --- a/brat/test/Test/Elaboration.hs +++ b/brat/test/Test/Elaboration.hs @@ -9,7 +9,6 @@ import Brat.Syntax.Raw (kind, dir) import Brat.Syntax.Simple (SimpleTerm(..)) import Brat.FC -import Data.Functor ((<&>)) import Data.List.NonEmpty (NonEmpty(..)) import qualified Data.PartialOrd as PO import Test.Tasty @@ -64,18 +63,17 @@ instance PO.PartialOrd DirAndKind where allDKs = [Noun, KVerb, UVerb] >>= \k -> [DK Syn k, DK Chk k] -juxt_tests :: FlatTest -> TestTree -juxt_tests (FT dk1 f1) = let s1 = show dk1 in testCase ("juxt w/" ++ s1) $ sequence_ $ flats <&> - \(FT dk2 f2) -> let - s = s1 ++ "-" ++ (show dk2) - f = (FJuxt (dummyFC f1) (dummyFC f2)) - dks = [dk | dk <- allDKs, dk1 PO.<= dk, dk2 PO.<= dk] - in case PO.minima dks of - [] -> elabFails s f - [dk] -> elabTest s dk f +juxtTests :: FlatTest -> TestTree +juxtTests (FT dk1 f1) = let s1 = show dk1 in + testCase ("juxt w/" ++ s1) $ + mapM_ (\(FT dk2 f2) -> let s = s1 ++ "-" ++ show dk2 + f = FJuxt (dummyFC f1) (dummyFC f2) + dks = [dk | dk <- allDKs, dk1 PO.<= dk, dk2 PO.<= dk] + in case PO.minima dks of + [] -> elabFails s f + [dk] -> elabTest s dk f) flats elaborationTests :: TestTree elaborationTests = testGroup "elaboration" ( - [testCase "base cases" $ sequence_ (map (\(FT dk f) -> elabTest (show dk) dk f) flats)] - ++ (map juxt_tests flats) + testCase "base cases" (mapM_ (\(FT dk f) -> elabTest (show dk) dk f) flats) : map juxtTests flats ) diff --git a/brat/test/Test/Search.hs b/brat/test/Test/Search.hs index f800b0c1..0c872f8a 100644 --- a/brat/test/Test/Search.hs +++ b/brat/test/Test/Search.hs @@ -24,7 +24,7 @@ maxDepth = 5 row :: Int -> Int -> Gen (Ro Kernel Z Z) row d n = sequence [ (name,) <$> arbitrarySValue d | name <- take n names ] <&> - foldr (\this rest -> RPr this rest) R0 + foldr RPr R0 arbitrarySValue :: Int -> Gen (Val Z) arbitrarySValue d = case d of diff --git a/brat/test/Test/TypeArith.hs b/brat/test/Test/TypeArith.hs index fd1cdef7..62a3f3f3 100644 --- a/brat/test/Test/TypeArith.hs +++ b/brat/test/Test/TypeArith.hs @@ -17,7 +17,7 @@ import Test.Tasty.QuickCheck hiding ((^)) var = VPar (ExEnd (Ex (MkName []) 0)) instance Arbitrary (NumVal (VVar Z)) where - arbitrary = NumValue <$> (abs <$> arbitrary) <*> arbitrary + arbitrary = NumValue . abs <$> arbitrary <*> arbitrary instance Arbitrary (Fun00 (VVar Z)) where arbitrary = sized aux @@ -26,7 +26,7 @@ instance Arbitrary (Fun00 (VVar Z)) where aux n = oneof [pure Constant0, StrictMonoFun <$> resize (n `div` 2) arbitrary] instance Arbitrary (StrictMono (VVar Z)) where - arbitrary = StrictMono <$> (abs <$> arbitrary) <*> arbitrary + arbitrary = StrictMono . abs <$> arbitrary <*> arbitrary instance Arbitrary (Monotone (VVar Z)) where arbitrary = sized aux diff --git a/brat/test/Test/Util.hs b/brat/test/Test/Util.hs index 1f50d9cc..06e9db9a 100644 --- a/brat/test/Test/Util.hs +++ b/brat/test/Test/Util.hs @@ -12,7 +12,7 @@ import Test.Tasty import Test.Tasty.HUnit import Test.Tasty.ExpectedFailure -runEmpty m = run emptyEnv initStore root m +runEmpty = run emptyEnv initStore root assertChecking :: Checking a -> Assertion assertChecking m = case runEmpty $ localFC (FC (Pos 0 0) (Pos 0 0)) m of From 71188afa69817d2689aaa880019938529a8d2f14 Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Tue, 19 Nov 2024 11:24:43 +0000 Subject: [PATCH 2/3] Add makefile with linting rules --- brat/Makefile | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) create mode 100644 brat/Makefile diff --git a/brat/Makefile b/brat/Makefile new file mode 100644 index 00000000..5f34fe52 --- /dev/null +++ b/brat/Makefile @@ -0,0 +1,19 @@ +.PHONY: hlint-fix hlint test build + +HS_FILES := $(shell git ls-files | grep '.hs') + +build: + stack build + +hlint-fix: $(HS_FILES) + @for file in $^; do \ + echo "linting $$file"; \ + hlint $$file --refactor --refactor-options="--inplace --step"; \ + done + +hlint: $(HS_FILES) + @hlint $^ + +test: + stack test --ta "--hide-successes" + From 294e7f5a7d1799acae445138ebd4368247d01959 Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Tue, 19 Nov 2024 11:26:50 +0000 Subject: [PATCH 3/3] Add to readme --- README.md | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/README.md b/README.md index ccf21221..aad7f544 100644 --- a/README.md +++ b/README.md @@ -29,6 +29,17 @@ There is a tool in the root of the repository called `hugr_validator` (install b brat --compile my-program.brat | hugr_validator ``` +# Development +Before opening a PR, make sure to run hlint on your code, using: +```sh +make hlint +``` +or try to automatically apply fixes with: +```sh +make hlint-fix +``` + + # Reference The [`brat/examples`](brat/examples) directory contains some examples of BRAT programs. For example: