Skip to content

Commit

Permalink
linting: dealt with all warnings
Browse files Browse the repository at this point in the history
  • Loading branch information
cstml committed Jul 30, 2021
1 parent 7911524 commit fed2acb
Show file tree
Hide file tree
Showing 7 changed files with 186 additions and 244 deletions.
3 changes: 2 additions & 1 deletion FMCt.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
95 changes: 32 additions & 63 deletions src/FMCt/Evaluator.hs
Original file line number Diff line number Diff line change
@@ -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]
Expand All @@ -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)
Expand All @@ -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.
Expand Down Expand Up @@ -138,37 +132,12 @@ 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)
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:t>.x.3.4
P (V "1" $ V "2" St) La -- [1 . 2 . *]
(B "x" (TVec [] :=> TVec [TLoc Ho $ TCon "a"]) La -- <x:t>
$ V "x" -- x
$ V "3" -- 3
$ V "4" -- 4
$ V "+" -- +
$ V "+" -- +
St) -- Star

ex8 = eval1 -- 1 . 2 . <x:t>_ . x . +
(V "1" -- 1
$ V "2" -- 2
$ B "x" (TVec [TLoc Ho $ TCon "a"]) Ho -- <x>
$ V "x" -- x
$ V "+" St) -- +


42 changes: 40 additions & 2 deletions src/FMCt/Examples.hs
Original file line number Diff line number Diff line change
@@ -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
Expand Down Expand Up @@ -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 . [*]. [*] . <x:((int,bool))>"
pEx2 = "x . y . [*]. [*] . <x:_>"
pEx3 = "x . y . [*]. [*] . <x:(a(int,bool) => (int))>"
pEx4 = "x . y . [*]. [*] . <x:(a(a) => (a) => (b))>" -- higher order type
pEx5 = "x . y . [*]. [*] . <x:(a(ab,b) => (int)), (b(int))>"



--------------------------------------------------------------------------------
-- Some simple Evaluator examples
ex7 = eval1 $ -- [1.2.*].<x:t>.x.3.4
P (V "1" $ V "2" St) La -- [1 . 2 . *]
(B "x" (TVec [] :=> TVec [TLoc Ho $ TCon "a"]) La -- <x:t>
$ V "x" -- x
$ V "3" -- 3
$ V "4" -- 4
$ V "+" -- +
$ V "+" -- +
St) -- Star

ex8 = eval1 -- 1 . 2 . <x:t>_ . x . +
(V "1" -- 1
$ V "2" -- 2
$ B "x" (TVec [TLoc Ho $ TCon "a"]) Ho -- <x>
$ V "x" -- x
$ V "+" St) -- +
45 changes: 20 additions & 25 deletions src/FMCt/Parsing.hs
Original file line number Diff line number Diff line change
Expand Up @@ -3,35 +3,36 @@ 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
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
Expand Down Expand Up @@ -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:
Expand All @@ -99,7 +100,7 @@ homeType :: Parser T
homeType = do
typeC <- between (char '(') (char ')') termType
return $ TLoc La typeC

-}
-- | Constant Type
--
-- Example:
Expand Down Expand Up @@ -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
Expand All @@ -175,9 +176,3 @@ alphaNumeric = alpha <|> numeric
operators :: Parser Char
operators = oneOf "+-/%=!?"

-- parse example
ex1 = parseTest term "x . y . [*]. [*] . <x:((int,bool))>"
ex2 = parseTest term "x . y . [*]. [*] . <x:_>"
ex3 = parseTest term "x . y . [*]. [*] . <x:(a(int,bool) => (int))>"
ex4 = parseTest term "x . y . [*]. [*] . <x:(a(a) => (a) => (b))>" -- higher order type
ex5 = parseTest term "x . y . [*]. [*] . <x:(a(ab,b) => (int)), (b(int))>"
9 changes: 5 additions & 4 deletions src/FMCt/Pretty.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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


Expand Down
36 changes: 21 additions & 15 deletions src/FMCt/Syntax.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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, γ, λ} --
Expand All @@ -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)

--------------------------------------------------------------------------------
Expand All @@ -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, ")"]

Expand All @@ -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)

Loading

0 comments on commit fed2acb

Please sign in to comment.