From fed2acb6ba1700bdbca5c16bdab6c1df5c172cd3 Mon Sep 17 00:00:00 2001 From: cstml Date: Thu, 29 Jul 2021 21:25:32 +0100 Subject: [PATCH] linting: dealt with all warnings --- FMCt.cabal | 3 +- src/FMCt/Evaluator.hs | 95 +++++++------------ src/FMCt/Examples.hs | 42 ++++++++- src/FMCt/Parsing.hs | 45 ++++----- src/FMCt/Pretty.hs | 9 +- src/FMCt/Syntax.hs | 36 +++++--- src/FMCt/TypeChecker.hs | 200 +++++++++++++--------------------------- 7 files changed, 186 insertions(+), 244 deletions(-) diff --git a/FMCt.cabal b/FMCt.cabal index ec9a539..9f4a2ed 100644 --- a/FMCt.cabal +++ b/FMCt.cabal @@ -13,7 +13,8 @@ extra-source-files: CHANGELOG.md, common common-specs Ghc-Options: -Wno-name-shadowing - -- -Wall + -Wall + -Wno-unuused-top-binds -- -Wcompat -- -Wincomplete-uni-patterns -- -Wredundant-constraints diff --git a/src/FMCt/Evaluator.hs b/src/FMCt/Evaluator.hs index 1ef908a..a062166 100644 --- a/src/FMCt/Evaluator.hs +++ b/src/FMCt/Evaluator.hs @@ -1,26 +1,24 @@ {-#LANGUAGE ScopedTypeVariables#-} module FMCt.Evaluator - ( eval + ( Binds + , Memory + , State + , emptyMem + , eval , eval1 - , tCheck' , eval1' , evalToString + , tCheck' , tryEval1 - , State - , Binds - , Memory - , emptyMem ) where -import Control.DeepSeq -import Control.Exception (try, IOException, catch) +import Control.Exception (try, IOException) import Data.Map (Map, (!?)) -import FMCt.Syntax (Tm(..), Lo(..), Vv, Type(..)) +import FMCt.Syntax (Tm(..), Lo(..), Vv ) import Text.Read (readMaybe) -import FMCt.TypeChecker (typeCheck, Derivation, TError) +import FMCt.TypeChecker (typeCheck, TError) import qualified Control.Exception as E import qualified Data.Map as M -import Control.Monad (void) -- | Memory is a Map between a location and a list of Terms. type Memory = Map Lo [Tm] @@ -40,16 +38,9 @@ push t l (m,b) = case m !? l of Nothing -> (M.insert l [t] m, b) Just x -> (M.insert l (t:x) m, b) --- | Pops a term from λ location to a given location -pushL :: Lo -> State -> State -pushL l st@(m,b) = case m !? Ho of - Nothing -> error "Empty Stack when attempting to pop λ location" - Just (x:xs) -> push x l (M.insert Ho xs m, b) - Just _ -> error "Empty Stack when attempting to pop λ location" - -- | Binds a term to a value and puts in the memory bind :: Vv -> Lo -> State -> State -bind vv l st@(m,b) = case m !? l of +bind vv l (m,b) = case m !? l of Nothing -> error $ "Empty Location " ++ show l Just [] -> error $ "Empty Location " ++ show l Just (x:xs) -> (M.insert l xs m, M.insert vv [x] b) @@ -68,40 +59,43 @@ pop n l st@(m,b) -- | Hacky way to add numbers - TODO: refactor adds :: String -> String -> String adds x y = case (readMaybe x :: Maybe Int, readMaybe y :: Maybe Int) of - (Just x, Just y) -> show $ x + y + (Just x', Just y') -> show $ x' + y' _ -> x ++ y +-- | Hacky way to add numbers - TODO: refactor add :: State -> State -add st@(m,b) = t +add (m,b) = t where t = case m !? Ho of - Just [] -> error "Empty Stack" + Nothing -> error "Not enough numbers to add! Empty Stack!" + Just [] -> error "Not enough numbers to add! Empty Stack!" + Just [_] -> error "Not enough numbers to add!" Just (x:y:xs) -> case (x, y) of - (V x _ , V y _) -> push (V (x `adds` y) St) Ho (M.insert Ho xs m, b) + (V x' _ , V y' _) -> push (V (x' `adds` y') St) Ho (M.insert Ho xs m, b) + (_,_) -> error $ "Cannot add these terms" + evaluate :: Tm -> State -> State evaluate (V "+" c) m = evaluate c $ add (pop 2 Ho m) - where - intermediary = add $ pop 2 Ho m evaluate St m = m -- does nothing -evaluate (V x c) st@(m,b) = evaluate c nt -- places value @ lambda pos +evaluate (V x c) st@(_,b) = evaluate c nt -- places value @ lambda pos where - nt = if unbound then push (V x St) Ho st + nt = if unbound + then push (V x St) Ho st else push (head et) Ho st - et = case b !? x of - Just x -> x - _ -> error "This should have never happened - pushing unbound" - unbound = case b !? x of - Nothing -> True - _ -> False -evaluate (B v ty lo tm) m = evaluate tm (bind v lo m) -- pops and binds the term -evaluate (P te l t') st@(m,b) = evaluate t' (push te l st) -- pushes the term ---evaluate (E t t') st@(m,b) = evaluate t' (evaluate t st) -- evaluates the term + + et = maybe (error "This should have never happened - pushing unbound") id $ + b !? x + + unbound = maybe False (const True) $ b !? x + +evaluate (B v _ lo tm) m = evaluate tm (bind v lo m) -- pops and binds the term +evaluate (P te l t') st = evaluate t' (push te l st) -- pushes the term -- | The Empty FMCt Evaluator state. emptyMem :: State -emptyMem = (M.empty, M.empty) +emptyMem = (,) M.empty M.empty -- | Takes a list of terms and evaluates them one after another starting from -- the head. @@ -138,7 +132,7 @@ evalToString term = do tc <- tCheck' term case tc of Left e -> pure $ show e - Right x -> pure . show $ eval1 term + Right _ -> pure . show $ eval1 term -- | Evaluates a term and fails safely. tryEval1 :: Tm -> IO (Either IOException State) @@ -146,29 +140,4 @@ tryEval1 term = do x :: Either IOException State <- try $ E.evaluate $ eval1 term return x -evalIO :: State -> IO () -evalIO st@(m,b) = case m !? Out of - Just (x:xs) -> print (show x) - >> evalIO (M.insert Out xs m, b) - Just [] -> return () - Nothing -> return () - --- Some simple examples -ex7 = eval1 $ -- [1.2.*]..x.3.4 - P (V "1" $ V "2" St) La -- [1 . 2 . *] - (B "x" (TVec [] :=> TVec [TLoc Ho $ TCon "a"]) La -- - $ V "x" -- x - $ V "3" -- 3 - $ V "4" -- 4 - $ V "+" -- + - $ V "+" -- + - St) -- Star - -ex8 = eval1 -- 1 . 2 . _ . x . + - (V "1" -- 1 - $ V "2" -- 2 - $ B "x" (TVec [TLoc Ho $ TCon "a"]) Ho -- - $ V "x" -- x - $ V "+" St) -- + - diff --git a/src/FMCt/Examples.hs b/src/FMCt/Examples.hs index 0b15599..2739ad4 100644 --- a/src/FMCt/Examples.hs +++ b/src/FMCt/Examples.hs @@ -1,10 +1,16 @@ +{-# OPTIONS_GHC -Wno-unused-top-binds -Wno-missing-signatures#-} module FMCt.Examples - (examplesList) + ( examplesList + , pEx + , runPEx + ) where import FMCt.Parsing (parseFMC) import FMCt.TypeChecker (derive, fuse, consumes, consume) -import FMCt.Syntax (T, Type(..), Lo(..)) +import FMCt.Syntax (T, Type(..), Lo(..), Tm(..)) +import FMCt.Evaluator +examplesList :: [String] examplesList = [term1] where term1 :: String @@ -61,3 +67,35 @@ exCons' = (TCon "a" :=> TVec[TCon "b"]) `consume` (TCon "b" :=> TCon "c") -- | Wrapped in two vectors. exCons'' = (TCon "a" :=> TVec[TVec[TCon "b"]]) `consume` (TCon "b" :=> TCon "c") exCons2 = (TCon "a" :=> TCon "b") `consume` (TCon "" :=> TCon "c") + +-------------------------------------------------------------------------------- +-- parse example +runPEx = parseFMC <$> pEx +pEx = [pEx1, pEx2, pEx3, pEx4, pEx5] + where + pEx1 = "x . y . [*]. [*] . " + pEx2 = "x . y . [*]. [*] . " + pEx3 = "x . y . [*]. [*] . (int))>" + pEx4 = "x . y . [*]. [*] . (a) => (b))>" -- higher order type + pEx5 = "x . y . [*]. [*] . (int)), (b(int))>" + + + +-------------------------------------------------------------------------------- +-- Some simple Evaluator examples +ex7 = eval1 $ -- [1.2.*]..x.3.4 + P (V "1" $ V "2" St) La -- [1 . 2 . *] + (B "x" (TVec [] :=> TVec [TLoc Ho $ TCon "a"]) La -- + $ V "x" -- x + $ V "3" -- 3 + $ V "4" -- 4 + $ V "+" -- + + $ V "+" -- + + St) -- Star + +ex8 = eval1 -- 1 . 2 . _ . x . + + (V "1" -- 1 + $ V "2" -- 2 + $ B "x" (TVec [TLoc Ho $ TCon "a"]) Ho -- + $ V "x" -- x + $ V "+" St) -- + diff --git a/src/FMCt/Parsing.hs b/src/FMCt/Parsing.hs index 2b3ac48..8c2b669 100644 --- a/src/FMCt/Parsing.hs +++ b/src/FMCt/Parsing.hs @@ -3,19 +3,23 @@ module FMCt.Parsing , parseType , parseFMCtoString , parseFMC' + , PError(..) ) where import Control.Monad (void) -import Control.Exception hiding (try) - -import FMCt.Syntax (Tm(..), Lo(..), T(..), Type(..)) +import qualified Control.Exception as E +import Control.Exception (Exception) +import FMCt.Syntax (Tm(..), Lo(..), T, Type(..)) import Text.ParserCombinators.Parsec +data PError = PTermErr String + | PTypeErr String + deriving Show +instance Exception PError + -- | Main Parsing Function. (Unsafe) parseFMC :: String -> Tm -parseFMC x = case parse term "FMCParser" x of - Right x -> x - Left e -> error $ show e +parseFMC x = either (E.throw . PTermErr . show) id $ parse term "FMCParser" x -- | Main Parsing Function. (Safe) parseFMC' :: String -> Either ParseError Tm @@ -23,15 +27,12 @@ parseFMC' x = parse term "FMCParser" x -- | Utility Parsing Function used for the FMCt-Web. parseFMCtoString :: String -> String -parseFMCtoString x = case parse term "FMCParser" x of - Right x -> show x - Left e -> show e +parseFMCtoString x = either show show $ parse term "FMCParser" x -- | Type Parser. parseType :: String -> T -parseType x = case parse termType "TypeParser" x of - Right x -> x - Left e -> error $ show e +parseType x = either (E.throw . PTypeErr . show) id $ parse termType "TypeParser" x + -- | Term Parser. term :: Parser Tm @@ -90,7 +91,7 @@ type TConstant = String typeConstant :: Parser TConstant typeConstant = many1 alpha <> many alphaNumeric - +{- -- | Home Constants are constants that are on the lambda row -- -- Examples: @@ -99,7 +100,7 @@ homeType :: Parser T homeType = do typeC <- between (char '(') (char ')') termType return $ TLoc La typeC - +-} -- | Constant Type -- -- Example: @@ -144,11 +145,11 @@ emptyType = do void (char 'e') <|> spaces return $ TCon "" -nestedType :: Parser T -nestedType = do - l <- location - ts <- between (spaces >> char '(' >> spaces) (spaces >> char ')' >> spaces) termType - return $ TLoc l ts +-- nestedType :: Parser T +-- nestedType = do +-- l <- location +-- ts <- between (spaces >> char '(' >> spaces) (spaces >> char ')' >> spaces) termType +-- return $ TLoc l ts higherType :: Parser T higherType = do @@ -175,9 +176,3 @@ alphaNumeric = alpha <|> numeric operators :: Parser Char operators = oneOf "+-/%=!?" --- parse example -ex1 = parseTest term "x . y . [*]. [*] . " -ex2 = parseTest term "x . y . [*]. [*] . " -ex3 = parseTest term "x . y . [*]. [*] . (int))>" -ex4 = parseTest term "x . y . [*]. [*] . (a) => (b))>" -- higher order type -ex5 = parseTest term "x . y . [*]. [*] . (int)), (b(int))>" diff --git a/src/FMCt/Pretty.hs b/src/FMCt/Pretty.hs index fd42527..0541ea0 100644 --- a/src/FMCt/Pretty.hs +++ b/src/FMCt/Pretty.hs @@ -12,13 +12,14 @@ printStack (m,b) = "Memory: \n" ++ printer mem ++ "Bindings: \n" ++ printer bin mem = M.toList m bin = M.toList b printer [] = "" - printer (x@(l,ts):xs) = show l ++ "[" ++ show ts ++ "]" ++ "\n" ++ printer xs + printer ((l,ts):xs) = show l ++ "[" ++ show ts ++ "]" ++ "\n" ++ printer xs -printOutput (m,b) = "Output: \n" ++ printer out +printOutput :: State -> String +printOutput (m,_) = "Output: \n" ++ printer out where out = maybe [] reverse (m M.!? Out) - printer x = case x of - [] -> "" + printer = \case + [] -> "" (x:xs) -> show x ++ "\n" ++ printer xs diff --git a/src/FMCt/Syntax.hs b/src/FMCt/Syntax.hs index 6a60783..934543b 100644 --- a/src/FMCt/Syntax.hs +++ b/src/FMCt/Syntax.hs @@ -39,14 +39,28 @@ type T = Type String -- | Type data structure data Type a = TCon a -- ^ Type Constant. - | TVar a -- ^ Type Variable - (like haskell forall - WIP) +-- | TVar a -- ^ Type Variable - (like haskell forall - WIP) | TVec [Type a] -- ^ Type Vector | TLoc Lo (Type a) -- ^ Location Parametrised Type. | Type a :=> Type a -- ^ A FMC Type. deriving (Eq, Ord) --- | TypedTerms -type TTm = (Tm, T) + +instance Semigroup T where + TVec [] <> x = x + x <> TVec[] = x + TCon "" <> x = x + x <> TCon "" = x + xx@(TCon _) <> yy@(TCon _) = TVec [xx,yy] + TVec x <> TVec y = TVec $ x ++ y + xx@(TLoc l x) <> yy@(TLoc l' y) | l == l' = TLoc l $ x <> y + | otherwise = TVec [xx,yy] + xx <> yy = TVec [xx,yy] + +instance Monoid T where + mempty = TCon "" + + -------------------------------------------- -- Location = {out, in, rnd, nd, x, γ, λ} -- @@ -60,9 +74,9 @@ data Lo = Out -- ^ User Output Location - can only be pushed to. | Ho -- ^ Home stack : γ ∈ A. | La -- ^ Default push Location: λ ∈ A. | Lo String -- ^ any other location: x ∈ A. - | InInt -- ^ User Input Location for Ints - | InBool -- ^ User Input Location for Bools - | InChar -- ^ User Input Location for Chars +-- | InInt -- ^ User Input Location for Ints +-- | InBool -- ^ User Input Location for Bools +-- | InChar -- ^ User Input Location for Chars deriving (Eq, Ord) -------------------------------------------------------------------------------- @@ -81,7 +95,7 @@ instance Show (Type String) where show x = case x of TCon "" -> " " TCon y -> y - TVec x -> mconcat ["(", init $ mconcat $ (flip (++) ",") <$> show <$> x , ")"] + TVec _x -> mconcat ["(", init $ mconcat $ (flip (++) ",") <$> show <$> _x , ")"] TLoc l y -> show l ++ "(" ++ show y ++ ")" t1 :=> t2 -> mconcat ["(", show t1, " => ", show t2, ")"] @@ -92,11 +106,3 @@ instance Show Tm where V v t -> v ++ "." ++ show t -- untyped version St -> "*" -instance Functor Type where - fmap f term - = case term of - TCon x -> TCon $ f x - TVar x -> TVar $ f x - TLoc l x -> TLoc l $ f <$> x - a :=> b -> (f <$> a) :=> (f <$> b) - diff --git a/src/FMCt/TypeChecker.hs b/src/FMCt/TypeChecker.hs index 25fcf14..73acb89 100644 --- a/src/FMCt/TypeChecker.hs +++ b/src/FMCt/TypeChecker.hs @@ -11,14 +11,7 @@ module FMCt.TypeChecker ) where -import Control.DeepSeq import FMCt.Syntax -import Data.List (sort) -import qualified Data.Map as M -import FMCt.Parsing (parseType, parseFMC) -import Text.Read (readMaybe) -import Data.Monoid -import Control.Monad.State import Control.Exception -- | Typechecking Errors. @@ -36,29 +29,13 @@ type Context = [(Term, T)] type Judgement = (Context, Term, T) data Derivation - = Star Judgement - | Variable Judgement - | Abstraction Judgement Derivation - | Application Judgement Derivation - | Fusion Judgement Derivation Derivation + = Star !Judgement + | Variable !Judgement + | Abstraction !Judgement !Derivation + | Application !Judgement !Derivation + | Fusion !Judgement !Derivation !Derivation type Term = Tm -type TypedTerm = (Term, T) -type TVariable = String - -instance Semigroup T where - TVec [] <> x = x - x <> TVec[] = x - TCon "" <> x = x - x <> TCon "" = x - xx@(TCon x) <> yy@(TCon y) = TVec [xx,yy] - TVec x <> TVec y = TVec $ x ++ y - xx@(TLoc l x) <> yy@(TLoc l' y) | l == l' = TLoc l $ x <> y - | otherwise = TVec [xx,yy] - xx <> yy = TVec [xx,yy] - -instance Monoid T where - mempty = TCon "" -------------------------------------------------------------------------------- -- TypeCheck Function @@ -68,6 +45,7 @@ typeCheck = derive -------------------------------------------------------------------------------- -- Aux Functions +getJudgement :: Derivation -> Judgement getJudgement = \case Star j -> j Variable j -> j @@ -77,7 +55,7 @@ getJudgement = \case freshTypeVar :: [T] freshTypeVar = TCon <$> [ mconcat $ [[x],[z],show y] - | y <- [1..] + | y <- [1..] :: [Integer] , x <- ['A'..'Z'] , z <- ['A'..'Z'] ] @@ -88,8 +66,8 @@ freshVarTypes = TVec . (:[]) <$> freshTypeVar splitStream :: [a] -> ([a],[a]) splitStream x = (,) l r where - l = snd <$> (filter ( odd . fst ) $ zip [1..] x) - r = snd <$> (filter ( not . odd . fst ) $ zip [1..] x) + l = snd <$> (filter ( odd . fst ) $ zip ([1..] :: [Integer]) x) + r = snd <$> (filter ( not . odd . fst ) $ zip ([1..] :: [Integer]) x) -------------------------------------------------------------------------------- -- @@ -101,12 +79,7 @@ fuseTypesD dL dR = ty tR = (getJType . getJudgement) dR :: T ty = fuse tL tR -newtype MT = MT T - -toMT :: T -> MT -toMT x@(t1 :=> t2) = MT x -toMT _ = error "Not Machine Type" - +getJType :: Judgement -> T getJType (_,_,x) = x -- | Second step is to add our known variables to the context @@ -136,7 +109,7 @@ derive = derive' freshVarTypes [(St, TCon [] :=> TCon [])] mergeCtx ox oy = makeSet ox oy where makeSet [] x = x - makeSet (t@(term,ty):xs) [] = t : makeSet xs oy + makeSet (t:xs) [] = t : makeSet xs oy makeSet t@((term,ty):xs) ((term',ty'):ys) = if term /= term' then makeSet t ys else if ty == ty' then makeSet xs oy @@ -160,7 +133,7 @@ derive = derive' freshVarTypes [(St, TCon [] :=> TCon [])] where ty = getType term ctx - V x St -> Variable (ctx, term, ty) + V _ St -> Variable (ctx, term, ty) where ty = getType term ctx @@ -206,43 +179,43 @@ derive = derive' freshVarTypes [(St, TCon [] :=> TCon [])] fuse :: T -> T -> T fuse = \case - x@(TCon "") -> normaliseT + TCon "" -> normaliseT - x@(TVec []) -> normaliseT + TVec [] -> normaliseT x@(TCon _) -> \case - y@(TCon "") -> x + TCon "" -> x y@(TCon _) -> TVec [x,y] - y@(TVec []) -> TVec [x] - yy@(TVec (y:ys)) -> fuse (fuse x y) (TVec ys) - y@(TLoc l t) -> TVec [x,y] - y@(t1 :=> t2) -> either (throw . ErrWrongT) normaliseT $ consume y (mempty :=> x) + TVec [] -> TVec [x] + TVec (y:ys) -> fuse (fuse x y) (TVec ys) + y@(TLoc _ _) -> TVec [x,y] + y@(_ :=> _) -> either (throw . ErrWrongT) normaliseT $ consume y (mempty :=> x) - xxx@(TVec xx@(x:xs)) -> \case - y@(TCon "") -> xxx + xxx@(TVec xx@(x:_)) -> \case + TCon "" -> xxx y@(TCon _) -> TVec $ xx ++ [y] - y@(TVec []) -> xxx - yy@(TVec (y:ys)) -> fuse (fuse xxx y) (TVec ys) - y@(TLoc l t) -> TVec [x,y] - y@(t1 :=> t2) -> either (throw . ErrWrongT) normaliseT $ consume y (mempty :=> xxx) + TVec [] -> xxx + TVec (y:ys) -> fuse (fuse xxx y) (TVec ys) + y@(TLoc _ _) -> TVec [x,y] + y@(_ :=> _) -> either (throw . ErrWrongT) normaliseT $ consume y (mempty :=> xxx) x@(TLoc l t) -> \case - y@(TCon "") -> x + TCon "" -> x y@(TCon _) -> TVec $ x : y : [] - y@(TVec []) -> x - yy@(TVec (y:ys)) -> fuse (fuse x y) (TVec ys) + TVec [] -> x + TVec (y:ys) -> fuse (fuse x y) (TVec ys) y@(TLoc l' t') -> if l == l' then TLoc l $ fuse t t' else TVec [x,y] - y@(t1 :=> t2) -> either (throw . ErrWrongT) normaliseT $ consume y (mempty :=> x) + y@(_ :=> _) -> either (throw . ErrWrongT) normaliseT $ consume y (mempty :=> x) - x@(t1 :=> t2) -> \case - y@(TCon "") -> x + x@(_ :=> _) -> \case + TCon "" -> x y@(TCon _) -> fuse (mempty :=> y) x - y@(TVec []) -> x - yy@(TVec (y:ys)) -> fuse (fuse x y) (TVec ys) - y@(TLoc l' t') -> fuse (mempty :=> y) x - y@(t1' :=> t2') -> either (throw . ErrWrongT) normaliseT $ consume x y + TVec [] -> x + TVec (y:ys) -> fuse (fuse x y) (TVec ys) + y@(TLoc _ _) -> fuse (mempty :=> y) x + y@(_ :=> _) -> either (throw . ErrWrongT) normaliseT $ consume x y consumes :: T -- ^ Requires - What the term will consume @@ -268,10 +241,11 @@ consumes = \case in (,) res2 (left1 <> left2) yy -> (xx,yy) - xxx@(TVec xx@(x:xs)) -> \case - TCon "" -> (,) xxx mempty - TVec [] -> (,) xxx mempty - yyy@(TVec yy@(y:ys)) -> let + xxx@(TVec (x:xs)) -> \case + TCon "" -> (,) xxx mempty + TVec [] -> (,) xxx mempty + TVec (y:ys) -> + let (res1,left1) = consumes xxx y (res2,left2) = consumes res1 (TVec ys) in @@ -291,11 +265,7 @@ consumes = \case if l == l' then let - (res, left) = consumes t t' - - res' = if res == mempty || res == TVec [] - then mempty - else TLoc l res + (res, left) = consumes t t' left' = if left == mempty || left == TVec [] then mempty @@ -309,7 +279,7 @@ consumes = \case -- TLoc doesn't interact with any other type. y -> (,) x y - x@(tIn :=> tOut) -> + x@(_ :=> _) -> \y -> if x == y then (,) mempty mempty @@ -317,18 +287,16 @@ consumes = \case -- | Normalise gets rid of empty Types at locations. normaliseT :: T -> T -normaliseT x@(TCon _) = x -normaliseT x@(TVec []) = mempty -normaliseT (TLoc _ (TVec [])) = mempty -normaliseT (TLoc _ (TCon "")) = mempty -normaliseT (TVec (x:[])) = normaliseT x -normaliseT (t1 :=> t2) = normaliseT t1 :=> normaliseT t2 -normaliseT (TVec x) = TVec $ fEmpty $ normaliseT <$> x - where - fEmpty :: [T] -> [T] - fEmpty = filter (not . aux) - aux x = x == (mempty :: T) || x == TCon "" || x == TVec [] -normaliseT x = id x -- Just to be sure it gets through. +normaliseT = \case + x@(TCon _) -> x + TVec [] -> mempty + TLoc _ (TVec []) -> mempty + TLoc _ (TCon "") -> mempty + TVec (x:[]) -> normaliseT x + t1 :=> t2 -> normaliseT t1 :=> normaliseT t2 + TVec x -> TVec $ fEmpty $ normaliseT <$> x + where fEmpty = filter (not . aux); aux y = y == TCon "" || y == TVec [] + x -> id x -- Just to be sure it gets through. -- | Consume consume :: T -> T -> Either String T @@ -356,10 +324,9 @@ consume t1@(tIn :=> tOut) t2@(tIn' :=> tOut') = result , ". Resulting Type: " , show intermediary ] +consume _ _ = (throw . ErrWrongT) $ "Cannot consume types which are not of the form (* => *)" -- Show Instance -type DisplayLine = (( Int, Int, Int), [String]) - instance Show Derivation where show d = unlines (reverse strs) where @@ -381,65 +348,30 @@ instance Show Derivation where showD :: Derivation -> (Int,Int,Int,[String]) showD (Star j) = (0,k,0,[s,showL 0 k 0]) where s = showJ j; k = length s showD (Variable j) = (0,k,0,[s,showL 0 k 0]) where s = showJ j; k = length s - showD (Abstraction j d) = addrule (showJ j) (showD d) - showD (Application j d) = addrule (showJ j) (showD d) - showD (Fusion j d e) = addrule (showJ j) (sidebyside (showD d) (showD e)) + showD (Abstraction j d') = addrule (showJ j) (showD d') + showD (Application j d') = addrule (showJ j) (showD d') + showD (Fusion j d' e) = addrule (showJ j) (sidebyside (showD d') (showD e)) addrule :: String -> (Int,Int,Int,[String]) -> (Int,Int,Int,[String]) addrule x (l,m,r,xs) - | k <= m = (ll,k,rr, (replicate ll ' ' ++ x ++ replicate rr ' ') - : showL l m r - : xs) + | k <= m + = (ll,k,rr, (replicate ll ' ' ++ x ++ replicate rr ' ') : showL l m r : xs) | k <= l+m+r - = ( ll - , k - , rr - , (replicate ll ' ' ++ x ++ replicate rr ' ') - : showL ll k rr - : xs - ) + = ( ll , k , rr , (replicate ll ' ' ++ x ++ replicate rr ' ') : showL ll k rr : xs ) | otherwise - = ( 0 - , k - , 0 - , x - : replicate k '-' - : [ replicate (-ll) ' ' - ++ y - ++ replicate (-rr) ' ' - | y <- xs - ] - ) - where - k = length x - i = div (m - k) 2 - ll = l+i - rr = r+m-k-i + = ( 0 , k , 0 , x : replicate k '-' : [ replicate (-ll) ' ' ++ y ++ replicate (-rr) ' ' | y <- xs ] ) + where k = length x; i = div (m - k) 2; ll = l+i; rr = r+m-k-i extend :: Int -> [String] -> [String] - extend i strs = strs ++ repeat (replicate i ' ') + extend i strs' = strs' ++ repeat (replicate i ' ') - sidebyside - :: (Int,Int,Int,[String]) - -> (Int,Int,Int,[String]) - -> (Int,Int,Int,[String]) + sidebyside :: (Int,Int,Int,[String]) -> (Int,Int,Int,[String]) -> (Int,Int,Int,[String]) sidebyside (l1,m1,r1,d1) (l2,m2,r2,d2) | length d1 > length d2 - = ( l1 - , m1+r1+2+l2+m2 - , r2 - , [ x ++ " " ++ y - | (x,y) <- zip d1 (extend (l2+m2+r2) d2) - ] - ) + = ( l1, m1+r1+2+l2+m2, r2, [ x ++ " " ++ y | (x,y) <- zip d1 (extend (l2+m2+r2) d2)]) + | otherwise - = ( l1 - , m1+r1+2+l2+m2 - , r2 - , [ x ++ " " ++ y - | (x,y) <- zip (extend (l1+m1+r1) d1) d2 - ] - ) + = ( l1 , m1+r1+2+l2+m2 , r2 , [ x ++ " " ++ y | (x,y) <- zip (extend (l1+m1+r1) d1) d2])