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

fix BadPortPull error message; refactor pullPorts not to require tuple #65

Merged
merged 3 commits into from
Dec 6, 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
16 changes: 8 additions & 8 deletions brat/Brat/Checker/Helpers.hs
Original file line number Diff line number Diff line change
Expand Up @@ -101,27 +101,27 @@
=> [PortName]
-> [(NamedPort e, ty)]
-> Checking [(NamedPort e, ty)]
pullPortsRow = pullPorts portName showRow
pullPortsRow = pullPorts (portName . fst) showRow

pullPortsSig :: Show ty
=> [PortName]
-> [(PortName, ty)]
-> Checking [(PortName, ty)]
pullPortsSig = pullPorts id showSig
pullPortsSig = pullPorts fst showSig

pullPorts :: forall a ty

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

View workflow job for this annotation

GitHub Actions / build

Unused quantified type variable ‘ty’

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

View workflow job for this annotation

GitHub Actions / build

Unused quantified type variable ‘ty’
. (a -> PortName) -- A way to get a port name for each element
-> ([(a, ty)] -> String) -- A way to print the list
-> ([a] -> String) -- A way to print the list
-> [PortName] -- Things to pull to the front
-> [(a, ty)] -- The list to rearrange
-> Checking [(a, ty)]
-> [a] -- The list to rearrange
-> Checking [a]
pullPorts toPort showFn to_pull types =
-- the "state" here is the things still available to be pulled
(\(pulled, rest) -> pulled ++ rest) <$> runStateT (mapM pull1Port to_pull) types

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

View workflow job for this annotation

GitHub Actions / hlint

Suggestion in pullPorts in module Brat.Checker.Helpers: Use uncurry ▫︎ Found: "\\ (pulled, rest) -> pulled ++ rest" ▫︎ Perhaps: "uncurry (++)" ▫︎ Note: increases laziness
where
pull1Port :: PortName -> StateT [(a, ty)] Checking (a, ty)
pull1Port p = StateT $ \available -> case partition ((== p) . toPort . fst) available of
([], _) -> err $ BadPortPull $ "Port not found: " ++ p ++ " in " ++ showFn available
pull1Port :: PortName -> StateT [a] Checking a
pull1Port p = StateT $ \available -> case partition ((== p) . toPort) available of
([], _) -> err $ BadPortPull p (showFn available)
([found], remaining) -> pure (found, remaining)
(_, _) -> err $ AmbiguousPortPull p (showFn available)

Expand Down Expand Up @@ -306,7 +306,7 @@
pure src

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

Check warning on line 309 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 309 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 All @@ -333,7 +333,7 @@
-> (Src, CTy m Z) -- The input to this level of mapfun
-> Checking (Src, CTy m Z)
mkMapFun (lenSrc, len) (valSrc, cty) = do
let weak1 = changeVar (Thinning (ThDrop ThNull))

Check warning on line 336 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 336 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 (VFun my' cty))], _) <-
next "MapFun" MapFun (S0, Some (Zy :* S0))
Expand Down
2 changes: 1 addition & 1 deletion brat/Brat/Checker/SolvePatterns.hs
Original file line number Diff line number Diff line change
Expand Up @@ -372,7 +372,7 @@ argProblems srcs na p = argProblemsWithLeftovers srcs na p >>= \case
_ -> err $ UnificationError "Pattern doesn't match expected length for constructor args"

argProblemsWithLeftovers :: [Src] -> NormalisedAbstractor -> Problem -> Checking (Problem, [Src])
argProblemsWithLeftovers srcs (NA (APull ps abs)) p = pullPorts portName show ps (map (, ()) srcs) >>= \srcs -> argProblemsWithLeftovers (fst <$> srcs) (NA abs) p
argProblemsWithLeftovers srcs (NA (APull ps abs)) p = pullPorts portName show ps srcs >>= \srcs -> argProblemsWithLeftovers srcs (NA abs) p
argProblemsWithLeftovers (src:srcs) na p | Just (pat, na) <- unconsNA na = first ((src, pat):) <$> argProblemsWithLeftovers srcs na p
argProblemsWithLeftovers srcs (NA AEmpty) p = pure (p, srcs)
argProblemsWithLeftovers [] abst _ = err $ NothingToBind (show abst)
Expand Down
7 changes: 4 additions & 3 deletions brat/Brat/Error.hs
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@
) where

import Brat.FC
import Brat.Syntax.Port (PortName)

import Data.List (intercalate)
import System.Exit
Expand Down Expand Up @@ -60,8 +61,8 @@
| FileNotFound String [String]
| SymbolNotFound String String
| InternalError String
| AmbiguousPortPull String String
| BadPortPull String
| AmbiguousPortPull PortName String
| BadPortPull PortName String
| VConNotFound String
| TyConNotFound String String
| MatchingOnTypes
Expand Down Expand Up @@ -139,7 +140,7 @@
show (SymbolNotFound s i) = "Symbol `" ++ s ++ "` not found in `" ++ i ++ "`"
show (InternalError x) = "Internal error: " ++ x
show (AmbiguousPortPull p row) = "Port " ++ p ++ " is ambiguous in " ++ row
show (BadPortPull x) = "Port " ++ x ++ " can't be pulled because it depends on a previous port"
show (BadPortPull p row) = "Port not found: " ++ p ++ " in " ++ row
show (VConNotFound x) = "Value constructor not recognised: " ++ x
show (TyConNotFound ty v) = show v ++ " is not a valid constructor for type " ++ ty
show MatchingOnTypes = "Trying to pattern match on a type"
Expand Down Expand Up @@ -212,8 +213,8 @@
ls = lines contents
in case endLineN - startLineN of
0 -> [ls!!startLineN, highlightSection startCol endCol]
n | n > 0 -> let (first:rest) = drop (startLineN - 1) $ take (endLineN + 1) ls

Check warning on line 216 in brat/Brat/Error.hs

View workflow job for this annotation

GitHub Actions / build

Pattern match(es) are non-exhaustive

Check warning on line 216 in brat/Brat/Error.hs

View workflow job for this annotation

GitHub Actions / build

Pattern match(es) are non-exhaustive
(last:rmid) = reverse rest

Check warning on line 217 in brat/Brat/Error.hs

View workflow job for this annotation

GitHub Actions / build

Pattern match(es) are non-exhaustive

Check warning on line 217 in brat/Brat/Error.hs

View workflow job for this annotation

GitHub Actions / build

Pattern match(es) are non-exhaustive
in [first, highlightSection startCol (length first)]
++ (reverse rmid >>= (\l -> [l, highlightSection 0 (length l)]))
++ [last, highlightSection 0 endCol]
Expand Down
Loading