Commit 57fe5aeb authored by Nicolas Lenz's avatar Nicolas Lenz
Browse files

Init

parent eb90cdec
# ---> Haskell
*.template
pages/
out/
*.cabal
dist
dist-*
cabal-dev
*.o
*.hi
*.chi
*.chs.h
*.dyn_o
*.dyn_hi
.hpc
.hsenv
.cabal-sandbox/
cabal.sandbox.config
*.prof
*.aux
*.hp
*.eventlog
.stack-work/
cabal.project.local
cabal.project.local~
.HTF/
.ghc.environment.*
.vscode
# Typesystem
# Type Systems
Testing out various type systems in Haskell.
Currently allows for primitive expressions to be evaluated allowing for "true", "false", "if E then E else E", "0", "succ E", "pred E", "isZero E" and "(E)" where E is an expression.
Run with `stack run` to open the test shell interface. Enter an expression in the shell to see it parsed and evaluated.
E.g.
```
expr> if (isZero (succ 0)) then succ 0 else pred (succ 0)
Term: If (IsZero (Succ Zero)) (Succ Zero) (Pred (Succ Zero))
Result: Just Zero
expr>
```
name: type-systems
version: "0.0.0"
license: Apache-2.0
dependencies:
- base
- relude
- megaparsec
- haskeline
default-extensions:
- NoImplicitPrelude
- OverloadedStrings
- RecordWildCards
- LambdaCase
executables:
type-systems:
main: Main.hs
source-dirs: src
module Expr where
import Relude
data Expr
= ETrue
| EFalse
| If Expr Expr Expr
| Zero
| Succ Expr
| Pred Expr
| IsZero Expr
deriving (Show)
ex1 :: Expr
ex1 = If (IsZero (Succ Zero)) (Succ Zero) (Pred (Succ Zero))
-- | Checks whether an expression is a value, that is, an expression containing only literals
isValue :: Expr -> Bool
isValue ETrue = True
isValue EFalse = True
isValue (If _ _ _) = False
isValue Zero = True
isValue (Succ e) = isValue e
isValue (Pred _) = False
isValue (IsZero _) = False
-- | Performs a single evaluation step on an expression. Returns Nothing if no evaluation can be applied
evalStep :: Expr -> Maybe Expr
evalStep (If ETrue e1 e2) = Just e1
evalStep (If EFalse e1 e2) = Just e2
evalStep (If e e1 e2) = (\e -> If e e1 e2) <$> evalStep e
evalStep (Succ e) = Succ <$> evalStep e
evalStep (Pred Zero) = Just Zero
evalStep (Pred (Succ e)) = Just e
evalStep (Pred e) = Pred <$> evalStep e
evalStep (IsZero Zero) = Just ETrue
evalStep (IsZero (Succ e))
| isValue e = Just EFalse
| otherwise = Nothing
evalStep (IsZero e) = IsZero <$> evalStep e
evalStep _ = Nothing
-- | Multi-step evaluation (is reflective)
evalMulti :: Expr -> Expr
evalMulti e = maybe e evalMulti (evalStep e)
-- | Evaluation that checks whether for stuckness. Returns fully evaluated value or Nothing.
eval :: Expr -> Maybe Expr
eval e
| isValue e' = Just e'
| otherwise = Nothing
where e' = evalMulti e
module Main where
import Relude
import System.Console.Haskeline
import Text.Megaparsec
import Text.Megaparsec.Error
import Parser
import Expr
main :: IO ()
main = runInputT defaultSettings loop where
loop :: InputT IO ()
loop = getInputLine "expr> " >>= \case
Nothing -> return ()
Just ":q" -> return ()
Just input -> do
case parse file "shell" (toText input) of
Left err -> outputStrLn $ errorBundlePretty err
Right inputP -> do
putStr "Term: "
putStrLn $ show inputP
putStr "Result: "
putStrLn $ show $ eval inputP
loop
module Parser where
import Relude
import Text.Megaparsec
import Text.Megaparsec.Char
import qualified Text.Megaparsec.Char.Lexer as L
import Expr
type Parser = Parsec Void Text
sc :: Parser ()
sc = L.space
space1
(L.skipLineComment "//")
(L.skipBlockCommentNested "/*" "*/")
lexeme :: Parser a -> Parser a
lexeme = L.lexeme sc
symbol :: Text -> Parser Text
symbol = L.symbol sc
parens :: Parser a -> Parser a
parens = between (symbol "(") (symbol ")")
file :: Parser Expr
file = between sc (sc >> eof) expr
expr :: Parser Expr
expr = choice
[ ETrue <$ symbol "true" <?> "true literal"
, EFalse <$ symbol "false" <?> "false literal"
, If <$ symbol "if" <*> expr <* symbol "then" <*> expr <* symbol "else" <*> expr <?> "if expression"
, Zero <$ symbol "0" <?> "0 literal"
, Succ <$ symbol "succ" <*> expr <?> "succ"
, Pred <$ symbol "pred" <*> expr <?> "pred"
, IsZero <$ symbol "isZero" <*> expr <?> "isZero"
, parens expr <?> "supexpression"
]
resolver: lts-18.16
# This file was autogenerated by Stack.
# You should not edit this file by hand.
# For more information, please see the documentation at:
# https://docs.haskellstack.org/en/stable/lock_files
snapshots:
- original: lts-18.16
completed:
url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/18/16.yaml
sha256: cdead65fca0323144b346c94286186f4969bf85594d649c49c7557295675d8a5
size: 586286
packages: []
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment