mikrokosmos 0.5.0 → 0.6.0
raw patch · 11 files changed
+418/−231 lines, 11 filesdep +tasty-quickcheck
Dependencies added: tasty-quickcheck
Files
- README.md +1/−0
- mikrokosmos.cabal +34/−1
- source/Environment.hs +10/−3
- source/Format.hs +50/−46
- source/Interpreter.hs +35/−28
- source/Lambda.hs +31/−14
- source/Main.hs +62/−93
- source/NamedLambda.hs +10/−13
- source/Ski.hs +3/−2
- source/Types.hs +51/−31
- tests/test.hs +131/−0
README.md view
@@ -10,4 +10,5 @@ and simply typed λ-calculus. * [Mikrokosmos user's guide](https://m42.github.io/mikrokosmos/).+ * [Mikrokosmos tutorial](https://github.com/M42/mikrokosmos/blob/master/docs/tutorial.ipynb). * [Mikrokosmos on Hackage](https://hackage.haskell.org/package/mikrokosmos).
mikrokosmos.cabal view
@@ -1,5 +1,5 @@ name: mikrokosmos-version: 0.5.0+version: 0.6.0 synopsis: Lambda calculus interpreter description: A didactic untyped lambda calculus interpreter. homepage: https://github.com/M42/mikrokosmos@@ -35,6 +35,7 @@ options, tasty, tasty-hunit,+ tasty-quickcheck, directory >= 1.0 other-modules: Format@@ -48,3 +49,35 @@ default-language: Haskell2010 ghc-options: -Wall+++test-suite test+ default-language:+ Haskell2010+ type:+ exitcode-stdio-1.0+ hs-source-dirs: tests+ source+ main-is:+ test.hs+ build-depends: base >=4.7 && <5,+ mtl >=2.2,+ containers >= 0.5,+ haskeline >=0.7,+ parsec >=3,+ ansi-terminal,+ multimap,+ HUnit >=1.0,+ options,+ tasty,+ tasty-hunit,+ tasty-quickcheck,+ directory >= 1.0+ other-modules: Format+ Lambda+ NamedLambda+ MultiBimap+ Interpreter+ Environment+ Ski+ Types
source/Environment.hs view
@@ -12,6 +12,7 @@ Environment , context , defaultEnv+ , emptyContext -- * Reading the environment , getVerbose@@ -19,6 +20,7 @@ , getSki , getTypes , getExpressionName+ , getTopo -- * Modifying the environment , addBind@@ -26,6 +28,7 @@ , changeVerbose , changeSkioutput , changeTypes+ , changeTopo -- * Filenames and Modulenames , Filename@@ -52,6 +55,7 @@ , color :: Bool , skioutput :: Bool , types :: Bool+ , topo :: Bool } -- | Default environment for the interpreter.@@ -63,14 +67,16 @@ , color = True , skioutput = False , types = False+ , topo = False } -- | Get current settings-getColor, getVerbose, getSki, getTypes :: Environment -> Bool+getColor, getVerbose, getSki, getTypes, getTopo :: Environment -> Bool getColor = color getVerbose = verbose getSki = skioutput getTypes = types+getTopo = topo @@ -78,7 +84,7 @@ addBind :: Environment -> String -> Exp -> Environment addBind env s e = -- If the binding already exists, it changes nothing- if elem s (MultiBimap.lookup e $ context env)+ if s `elem` MultiBimap.lookup e (context env) then env else env {context = MultiBimap.insert e s (context env)} @@ -97,7 +103,8 @@ -- | Sets the types output configuration on/off changeTypes :: Environment -> Bool -> Environment changeTypes options setting = options {types = setting}-+changeTopo :: Environment -> Bool -> Environment+changeTopo options setting = options {topo = setting} -- | Given an expression, returns its name if it is bounded to any. getExpressionName :: Environment -> Exp -> Maybe String
source/Format.hs view
@@ -27,6 +27,11 @@ , helpText , initialText , versionText+ , restartText+ , errorNonTypeableText+ , errorTypeConstructors+ , errorUndefinedText+ , errorUnknownCommand ) where @@ -34,61 +39,28 @@ import Data.List import Data.Monoid --- Colors--- | Prompt messages color-promptColor :: Color+-- | Colors used on the prompt.+promptColor, nameColor, substColor, subst2Color, typeColor, errorColor :: Color promptColor = Blue---- | Named variables color-nameColor :: Color nameColor = Green---- | Substitutions are marked with this color-substColor :: Color substColor = Cyan---- | To-be-substituted expressions are marked with this color-subst2Color :: Color subst2Color = Cyan---- | Types are marked with this color-typeColor :: Color typeColor = Yellow+errorColor = Red -- Format sequences -- | Sequence of characters that signals the format of a formula to the terminal.-formatFormula :: String+formatFormula, formatIntro, formatLoading, formatPrompt, formatName :: String+formatSubs1, formatSubs2, formatType, formatError :: String formatFormula = setSGRCode [SetConsoleIntensity NormalIntensity, SetColor Foreground Dull promptColor]---- | Sequence of characters that signals the format of the introduction to the terminal.-formatIntro :: String-formatIntro = setSGRCode [SetConsoleIntensity BoldIntensity, SetColor Foreground Dull promptColor]---- | Sequence of characters that signals the format of the loading of a module to the terminal.-formatLoading :: String+formatIntro = setSGRCode [SetConsoleIntensity BoldIntensity, SetColor Foreground Dull promptColor] formatLoading = formatIntro---- | Sequence of characters that signals the format of the prompt to the terminal.-formatPrompt :: String-formatPrompt = setSGRCode [SetConsoleIntensity BoldIntensity, SetColor Foreground Vivid promptColor]---- | Sequence of characters that signals the format of a name to the terminal.-formatName :: String-formatName = setSGRCode [SetColor Foreground Dull nameColor]---- | Sequence of characters that signals the format of a substitution to the terminal.-formatSubs1 :: String-formatSubs1 = setSGRCode [SetConsoleIntensity BoldIntensity, SetColor Foreground Dull substColor]---- | Sequence of characters that signals the format of a expression which will--- be substituted in the next reduction step to the terminal.-formatSubs2 :: String-formatSubs2 = setSGRCode [SetConsoleIntensity FaintIntensity, SetColor Foreground Dull subst2Color]---- | Sequence of characters that signals the format of a type to the terminal.-formatType :: String-formatType = setSGRCode [SetConsoleIntensity NormalIntensity, SetColor Foreground Dull typeColor]-+formatPrompt = setSGRCode [SetConsoleIntensity BoldIntensity, SetColor Foreground Vivid promptColor]+formatName = setSGRCode [SetColor Foreground Dull nameColor]+formatSubs1 = setSGRCode [SetConsoleIntensity BoldIntensity, SetColor Foreground Dull substColor]+formatSubs2 = setSGRCode [SetConsoleIntensity FaintIntensity, SetColor Foreground Dull subst2Color]+formatType = setSGRCode [SetConsoleIntensity NormalIntensity, SetColor Foreground Dull typeColor]+formatError = setSGRCode [SetConsoleIntensity NormalIntensity, SetColor Foreground Dull errorColor] -- | Sequence of characters that cleans all the format. end :: String@@ -117,7 +89,38 @@ ] +-- | Unknown command error message+errorUnknownCommand :: String+errorUnknownCommand =+ formatError +++ "Error: parse error, unknown command"+ ++ end ++-- | Non typeable expression error message.+errorNonTypeableText :: String+errorNonTypeableText =+ formatError +++ "Error: non typeable expression"+ ++ end++-- | Type constructors on untyped lambda calculus error message.+errorTypeConstructors :: String+errorTypeConstructors =+ formatError +++ "Error: this expression uses type constructors. You may want to activate ':types on'."+ ++ end++-- | Undefined expression error message.+errorUndefinedText :: String+errorUndefinedText =+ formatError +++ "Error: undefined terms on the lambda expression"+ ++ end++restartText :: String+restartText = "Mikrokosmos context has been cleaned up"+ -- | Prompt line. It is shown when the interpreter asks the user -- to introduce a new command. promptText :: String@@ -130,6 +133,7 @@ "Commands available from the prompt:", "\t<expression>\t\t evaluates the expression", "\t:quit \t\t quits the interpreter",+ "\t:restart \t\t restarts the interpreter", "\t:load <file>\t\t loads the given .mkr library or script", "\t:verbose <on/off> \t sets verbose mode on/off", "\t:color <on/off> \t sets color mode on/off",@@ -152,4 +156,4 @@ -- | Version version :: String-version = "0.5.0"+version = "0.6.0"
source/Interpreter.hs view
@@ -22,6 +22,7 @@ import Control.Monad.State.Lazy import Text.ParserCombinators.Parsec hiding (State) import Data.Char+import Data.Maybe import Format import Environment import NamedLambda@@ -42,6 +43,7 @@ | SetColor Bool -- ^ Changes colors | SetSki Bool -- ^ Changes ski output | SetTypes Bool -- ^ Changes type configuration+ | SetTopo Bool | Help -- ^ Shows help -- | Language action. The language has a number of possible valid statements;@@ -62,22 +64,32 @@ act (EvalBind (s,le)) = do modify (\env -> addBind env s (simplifyAll $ toBruijn (context env) le)) return [""]-act (Execute le) = do+act (Execute le) = executeExpression le++-- | Executes a lambda expression. Given the context, returns the new+-- context after the evaluation.+executeExpression :: NamedLambda -> State Environment [String]+executeExpression le = do env <- get let typed = getTypes env- let illtyped = typed && typeinference (toBruijn (context env) le) == Nothing- let notypes = not typed && usestypecons (toBruijn (context env) le)+ let bruijn = toBruijn (context env) le+ let illtyped = typed && isNothing (typeinference bruijn)+ let notypes = not typed && usestypecons bruijn+ let verbose = getVerbose env+ let completeexp = showCompleteExp env $ simplifyAll bruijn+ let isopen = isOpenExp bruijn - return $ if illtyped then [formatType ++ "Error: non typeable expression" ++ end ++ "\n"] else- if notypes then [formatType ++- "Error: this expression uses type constructors. You may want to activate ':types on'."- ++ end ++ "\n"] else- [ unlines $- [ show le ] ++- [ unlines $ map showReduction $ simplifySteps $ toBruijn (context env) le ] ++- [ showCompleteExp env $ simplifyAll $ toBruijn (context env) le ] - ]-+ return $+ if isopen then [errorUndefinedText ++ "\n"] else+ if illtyped then [errorNonTypeableText ++ "\n"] else+ if notypes then [errorTypeConstructors ++ "\n"] else+ if not verbose then [completeexp ++ "\n"] else+ [unlines $+ [show le] +++ [unlines $ map showReduction $ simplifySteps bruijn] +++ [completeexp]+ ]+ -- | Executes multiple actions. Given a context and a set of actions, returns -- the new context after the sequence of actions and a text output.@@ -91,12 +103,14 @@ showCompleteExp environment expr = let lambdaname = show $ nameExp expr skiname = if getSki environment- then formatSubs2 ++ " ⇒ " ++ (show $ skiabs $ nameExp expr) ++ end+ then formatSubs2 ++ " ⇒ " ++ show (skiabs $ nameExp expr) ++ end else "" inferredtype = typeinference expr typename = if getTypes environment then formatType ++ " :: " ++ (case inferredtype of- Just s -> show s+ Just s -> if getTopo environment+ then show (Top s)+ else show s Nothing -> "Type error!") ++ end else "" expName = case getExpressionName environment expr of@@ -107,9 +121,6 @@ --- -- Parsing of interpreter command line commands. -- | Parses an interpreter action. interpreteractionParser :: Parser InterpreterAction@@ -122,6 +133,7 @@ , try colorParser , try skiOutputParser , try typesParser+ , try topoParser , try helpParser ] @@ -155,16 +167,10 @@ commentParser = string "#" >> many anyChar >> return Comment -- | Parses a "quit" command.-quitParser :: Parser InterpreterAction-quitParser = string ":quit" >> return Quit---- | Parses a "restart" command.-restartParser :: Parser InterpreterAction+quitParser, restartParser, helpParser :: Parser InterpreterAction+quitParser = string ":quit" >> return Quit restartParser = string ":restart" >> return Restart---- | Parses a "help" command.-helpParser :: Parser InterpreterAction-helpParser = string ":help" >> return Help+helpParser = string ":help" >> return Help -- | Parses a change in a setting settingParser :: (Bool -> InterpreterAction) -> String -> Parser InterpreterAction@@ -177,11 +183,12 @@ settingoffParser = string (settingname ++ " off") >> return (setSetting False) -- | Multiple setting parsers-verboseParser, colorParser, skiOutputParser, typesParser :: Parser InterpreterAction+verboseParser, colorParser, skiOutputParser, typesParser, topoParser :: Parser InterpreterAction verboseParser = settingParser SetVerbose ":verbose" colorParser = settingParser SetColor ":color" skiOutputParser = settingParser SetSki ":ski" typesParser = settingParser SetTypes ":types"+topoParser = settingParser SetTopo ":topology" -- | Parses a "load-file" command.
source/Lambda.hs view
@@ -15,7 +15,7 @@ , simplifySteps , showReduction , usestypecons--- , freein+ , isOpenExp ) where @@ -40,21 +40,20 @@ instance Show Exp where show = showexp - -- | Shows an expression with DeBruijn indexes. showexp :: Exp -> String showexp (Var n) = show n showexp (Lambda e) = "λ" ++ showexp e ++ "" showexp (App f g) = "(" ++ showexp f ++ " " ++ showexp g ++ ")" showexp (Pair a b) = "(" ++ showexp a ++ "," ++ showexp b ++ ")"-showexp (Pi1 m) = "(" ++ "fst " ++ showexp m ++ ")"-showexp (Pi2 m) = "(" ++ "snd " ++ showexp m ++ ")"-showexp (Inl m) = "(" ++ "inl " ++ showexp m ++ ")"-showexp (Inr m) = "(" ++ "inr " ++ showexp m ++ ")"-showexp (Caseof m n p) = "(" ++ "case " ++ showexp m ++ " of " ++ showexp n ++ "; " ++ showexp p ++ ")"-showexp (Unit) = "*"-showexp (Abort a) = "(abort " ++ showexp a ++ ")"-showexp (Absurd a) = "(absurd " ++ showexp a ++ ")"+showexp (Pi1 m) = "(" ++ "FST " ++ showexp m ++ ")"+showexp (Pi2 m) = "(" ++ "SND " ++ showexp m ++ ")"+showexp (Inl m) = "(" ++ "INL " ++ showexp m ++ ")"+showexp (Inr m) = "(" ++ "INR " ++ showexp m ++ ")"+showexp (Caseof m n p) = "(" ++ "CASE " ++ showexp m ++ " OF " ++ showexp n ++ "; " ++ showexp p ++ ")"+showexp Unit = "*"+showexp (Abort a) = "(ABORT " ++ showexp a ++ ")"+showexp (Absurd a) = "(ABSURD " ++ showexp a ++ ")" -- | Shows an expression coloring the next reduction. showReduction :: Exp -> String@@ -64,6 +63,7 @@ showReduction (App rs x) = "(" ++ showReduction rs ++ " " ++ showReduction x ++ ")" showReduction e = show e + -- | Colors a beta reduction betaColor :: Exp -> String betaColor (App (Lambda e) x) =@@ -115,7 +115,7 @@ simplify (Lambda e) = Lambda (simplify e) simplify (App (Lambda f) x) = betared (App (Lambda f) x) simplify (App (Var e) x) = App (Var e) (simplify x)-simplify (App (App f g) x) = App (simplify (App f g)) x+simplify (App (App f g) x) = App (simplify (App f g)) (simplify x) simplify (App a b) = App (simplify a) (simplify b) simplify (Var e) = Var e simplify (Pair a b) = Pair (simplify a) (simplify b)@@ -128,7 +128,7 @@ simplify (Caseof (Inl m) a _) = App a m simplify (Caseof (Inr m) _ b) = App b m simplify (Caseof a b c) = Caseof (simplify a) (simplify b) (simplify c)-simplify (Unit) = Unit+simplify Unit = Unit simplify (Abort a) = Abort (simplify a) simplify (Absurd a) = Absurd (simplify a) @@ -151,7 +151,7 @@ substitute n x (Inl a) = Inl (substitute n x a) substitute n x (Inr a) = Inr (substitute n x a) substitute n x (Caseof a b c) = Caseof (substitute n x a) (substitute n x b) (substitute n x c)-substitute _ _ (Unit) = Unit+substitute _ _ Unit = Unit substitute n x (Abort a) = Abort (substitute n x a) substitute n x (Absurd a) = Absurd (substitute n x a) substitute n x (Var m)@@ -177,7 +177,7 @@ incrementFreeVars n (Inl a) = Inl (incrementFreeVars n a) incrementFreeVars n (Inr a) = Inr (incrementFreeVars n a) incrementFreeVars n (Caseof a b c) = Caseof (incrementFreeVars n a) (incrementFreeVars n b) (incrementFreeVars n c)-incrementFreeVars _ (Unit) = Unit+incrementFreeVars _ Unit = Unit incrementFreeVars n (Abort a) = Abort (incrementFreeVars n a) incrementFreeVars n (Absurd a) = Absurd (incrementFreeVars n a) @@ -188,8 +188,25 @@ -- freein n (Lambda e) = freein (succ n) e -- freein n (App u v) = (freein n u) && (freein n v) +-- | Returns true if the expression has at least one type constructor. usestypecons :: Exp -> Bool usestypecons (Var _) = False usestypecons (App a b) = usestypecons a || usestypecons b usestypecons (Lambda b) = usestypecons b usestypecons _ = True+++-- | Returns true if the expression contains open undefined variables.+isOpenExp :: Exp -> Bool+isOpenExp (Var n) = n == 0+isOpenExp (App a b) = isOpenExp a || isOpenExp b+isOpenExp (Lambda a) = isOpenExp a+isOpenExp (Pair a b) = isOpenExp a || isOpenExp b+isOpenExp (Pi1 a) = isOpenExp a+isOpenExp (Pi2 a) = isOpenExp a+isOpenExp (Inl a) = isOpenExp a+isOpenExp (Inr a) = isOpenExp a+isOpenExp (Caseof a b c) = isOpenExp a || isOpenExp b || isOpenExp c+isOpenExp Unit = False+isOpenExp (Abort a) = isOpenExp a+isOpenExp (Absurd a) = isOpenExp a
source/Main.hs view
@@ -25,19 +25,18 @@ -- Uses the Options library, which requires the program to start with -- runCommand. The flags are stored in opts and other command line arguments -- are stored in args.- runCommand $ \opts args -> do- + runCommand $ \opts args -- Reads the flags- case flagVersion opts of- True -> putStrLn versionText- False ->- case args of- [] -> runInputT defaultSettings ( outputStrLn initialText- >> interpreterLoop defaultEnv- )- [filename] -> executeFile filename- _ -> putStrLn "Wrong number of arguments"-+ ->+ if flagVersion opts+ then putStrLn versionText+ else case args of+ [] ->+ runInputT+ defaultSettings+ (outputStrLn initialText >> interpreterLoop defaultEnv)+ [filename] -> executeFile filename+ _ -> putStrLn "Wrong number of arguments" -- | Interpreter awaiting for an instruction. interpreterLoop :: Environment -> InputT IO ()@@ -49,88 +48,65 @@ case minput of Nothing -> Quit Just "" -> EmptyLine- Just input -> case parse interpreteractionParser "" input of- Left _ -> Error- Right a -> a-+ Just input ->+ case parse interpreteractionParser "" input of+ Left _ -> Error+ Right a -> a -- Executes the parsed action, every action may affect the- -- context in a way, and returns the control to the interpreter. - case interpreteraction of+ -- context in a way, and returns the control to the interpreter.+ case interpreteraction -- Interprets an action- Interpret action -> case runState (act action) environment of- (output, newenv) -> do- outputActions newenv output- interpreterLoop newenv-+ of+ Interpret action ->+ case runState (act action) environment of+ (output, newenv) -> do+ outputActions newenv output+ interpreterLoop newenv -- Loads a module and its dependencies given its name. -- Avoids repeated modules keeping only their first ocurrence. Load modulename -> do- modules <- lift $ (nub <$> readAllModuleDepsRecursively [modulename])+ modules <- lift (nub <$> readAllModuleDepsRecursively [modulename]) files <- lift $ mapM findFilename modules- -- Concats all the module contents- maybeactions <- (fmap concat) . sequence <$> (lift $ mapM loadFile files)+ maybeactions <- fmap concat . sequence <$> lift (mapM loadFile files) case maybeactions of Nothing -> do outputStrLn "Error loading file" interpreterLoop environment- Just actions -> case runState (multipleAct actions) environment of- (output, newenv) -> do- outputActions newenv output- interpreterLoop newenv- + Just actions ->+ case runState (multipleAct actions) environment of+ (output, newenv) -> do+ outputActions newenv output+ interpreterLoop newenv -- Ignores the empty line EmptyLine -> interpreterLoop environment- - -- Exists the interpreter+ -- Exits the interpreter Quit -> return ()- -- Restarts the interpreter context- Restart -> interpreterLoop defaultEnv-+ Restart -> outputStrLn restartText >> interpreterLoop defaultEnv -- Unknown command- Error -> do- outputStr (if getColor environment then formatFormula else "")- outputStrLn "Unknown command"- outputStr end- interpreterLoop environment-+ Error -> outputStrLn errorUnknownCommand >> interpreterLoop environment -- Sets the verbose option- SetVerbose setting -> do- outputStrLn $- (if getColor environment then formatFormula else "") ++- "verbose mode: " ++ if setting then "on" else "off" ++- end- interpreterLoop (changeVerbose environment setting)- - -- Sets the color option- SetColor setting -> do- outputStrLn $- (if getColor environment then formatFormula else "") ++- "color mode: " ++ if setting then "on" else "off" ++- end- interpreterLoop (changeColor environment setting)-- -- Sets the ski option- SetSki setting -> do- outputStrLn $- (if getColor environment then formatFormula else "") ++- "ski mode: " ++ if setting then "on" else "off" ++- end- interpreterLoop (changeSkioutput environment setting)-- -- Sets the types option- SetTypes setting -> do- outputStrLn $- (if getColor environment then formatFormula else "") ++- "types: " ++ if setting then "on" else "off" ++- end- interpreterLoop (changeTypes environment setting)-+ SetVerbose setting ->+ setOption environment setting changeVerbose "verbose: "+ SetColor setting -> setOption environment setting changeColor "color mode: "+ SetSki setting -> setOption environment setting changeSkioutput "ski mode: "+ SetTypes setting -> setOption environment setting changeTypes "types: "+ SetTopo setting -> setOption environment setting changeTopo "topo mode: " -- Prints the help Help -> outputStr helpText >> interpreterLoop environment +-- | Sets the given option on/off.+setOption :: Environment -> Bool ->+ (Environment -> Bool -> Environment) ->+ String ->+ InputT IO ()+setOption environment setting change message = do+ outputStrLn $+ (if getColor environment then formatFormula else "") +++ message ++ if setting then "on" else "off" ++ end + interpreterLoop (change environment setting) -- | Outputs results from actions. Given a list of options and outputs,@@ -141,16 +117,10 @@ mapM_ (outputStr . format) output outputStr end where- format = formatColor . formatVerbose-+ format = formatColor formatColor s | getColor environment = s | otherwise = unlines $ map decolor $ lines s- - formatVerbose "" = ""- formatVerbose s- | not (getVerbose environment) = (++"\n") . last . lines $ s- | otherwise = s @@ -160,7 +130,7 @@ loadFile :: String -> IO (Maybe [Action]) loadFile filename = do putStrLn $ formatLoading ++ "Loading " ++ filename ++ "..." ++ end- input <- try $ (readFile filename) :: IO (Either IOException String)+ input <- try $ readFile filename :: IO (Either IOException String) case input of Left _ -> return Nothing Right inputs -> do@@ -176,19 +146,19 @@ executeFile filename = do maybeloadfile <- loadFile filename case maybeloadfile of- Nothing -> putStrLn "Error loading file"- Just actions -> case runState (multipleAct actions) defaultEnv of- (outputs, _) -> mapM_ (putStr . format) outputs- where- format :: String -> String- format "" = ""- format s = (++"\n") . last . lines $ s+ Nothing -> putStrLn "Error loading file"+ Just actions ->+ case runState (multipleAct actions) defaultEnv of+ (outputs, _) -> mapM_ (putStr . format) outputs+ where format :: String -> String+ format "" = ""+ format s = (++ "\n") . last . lines $ s -- | Reads module dependencies readFileDependencies :: Filename -> IO [Modulename] readFileDependencies filename = do- input <- try $ (readFile filename) :: IO (Either IOException String)+ input <- try $ readFile filename :: IO (Either IOException String) case input of Left _ -> return [] Right inputs -> return $@@ -222,6 +192,7 @@ , "./" ++ s ++ ".mkr" , appdir ++ "/" ++ s ++ ".mkr" , homedir ++ "/" ++ s ++ ".mkr"+ , "/usr/lib/mikrokosmos/" ++ s ++ ".mkr" ] @@ -235,7 +206,5 @@ instance Options MainFlags where -- | Flags definition defineOptions = pure MainFlags- <*> simpleOption "exec" ""- "A file to execute and show its results"- <*> simpleOption "version" False- "Show program version"+ <*> simpleOption "exec" "" "A file to execute and show its results"+ <*> simpleOption "version" False "Show program version"
source/NamedLambda.hs view
@@ -46,6 +46,7 @@ | TypedUnit -- ^ unit | TypedAbort NamedLambda -- ^ abort | TypedAbsurd NamedLambda -- ^ absurd+ deriving (Eq) -- | Parses a lambda expression with named variables. -- A lambda expression is a sequence of one or more autonomous@@ -93,25 +94,21 @@ -- | Parses a lambda abstraction. The '\' is used as lambda. lambdaAbstractionParser :: Parser NamedLambda lambdaAbstractionParser = LambdaAbstraction <$>- (char lambdaChar >> nameParser) <*> (char '.' >> lambdaexp)+ (lambdaChar >> nameParser) <*> (char '.' >> lambdaexp) -- | Char used to represent lambda in user's input.-lambdaChar :: Char-lambdaChar = '\\'+lambdaChar :: Parser Char+lambdaChar = choice [try $ char '\\', try $ char 'λ'] pairParser :: Parser NamedLambda pairParser = parens (TypedPair <$> lambdaexp <*> (char ',' >> lambdaexp)) -pi1Parser :: Parser NamedLambda+pi1Parser, pi2Parser :: Parser NamedLambda pi1Parser = TypedPi1 <$> (string "FST " >> lambdaexp)--pi2Parser :: Parser NamedLambda pi2Parser = TypedPi2 <$> (string "SND " >> lambdaexp) -inlParser :: Parser NamedLambda+inlParser, inrParser :: Parser NamedLambda inlParser = TypedInl <$> (string "INL " >> lambdaexp)--inrParser :: Parser NamedLambda inrParser = TypedInr <$> (string "INR " >> lambdaexp) caseParser :: Parser NamedLambda@@ -138,7 +135,7 @@ showNamedLambda (TypedInl a) = "(" ++ "INL " ++ showNamedLambda a ++ ")" showNamedLambda (TypedInr a) = "(" ++ "INR " ++ showNamedLambda a ++ ")" showNamedLambda (TypedCase a b c) = "(" ++ "CASE " ++ showNamedLambda a ++ " of " ++ showNamedLambda b ++ "; " ++ showNamedLambda c ++ ")"-showNamedLambda (TypedUnit) = "UNIT"+showNamedLambda TypedUnit = "UNIT" showNamedLambda (TypedAbort a) = "(" ++ "ABORT " ++ showNamedLambda a ++ ")" showNamedLambda (TypedAbsurd a) = "(" ++ "ABSURD " ++ showNamedLambda a ++ ")" @@ -172,7 +169,7 @@ tobruijn d context (TypedInl a) = Inl (tobruijn d context a) tobruijn d context (TypedInr a) = Inr (tobruijn d context a) tobruijn d context (TypedCase a b c) = Caseof (tobruijn d context a) (tobruijn d context b) (tobruijn d context c)-tobruijn _ _ (TypedUnit) = Unit+tobruijn _ _ TypedUnit = Unit tobruijn d context (TypedAbort a) = Abort (tobruijn d context a) tobruijn d context (TypedAbsurd a) = Absurd (tobruijn d context a) @@ -198,9 +195,9 @@ nameIndexes used new (Inl a) = TypedInl (nameIndexes used new a) nameIndexes used new (Inr a) = TypedInr (nameIndexes used new a) nameIndexes used new (Caseof a b c) = TypedCase (nameIndexes used new a) (nameIndexes used new b) (nameIndexes used new c)-nameIndexes _ _ (Unit) = TypedUnit+nameIndexes _ _ Unit = TypedUnit nameIndexes used new (Abort a) = TypedAbort (nameIndexes used new a)-nameIndexes used new (Absurd a) = TypedAbsurd (nameIndexes used new a)+nameIndexes used new (Absurd a) = TypedAbsurd (nameIndexes used new a) -- | Gives names to every variable in a deBruijn expression using
source/Ski.hs view
@@ -9,7 +9,8 @@ -} module Ski- ( Ski (S, K, I, Comb)+ ( Ski (S, K, I, Comb, Cte,+ Spair, Spi1, Spi2, Sinl, Sinr, Scase, Sunit, Sabort, Sabsurd) , skiabs ) where@@ -87,6 +88,6 @@ -- | Checks if a given variable is used on a SKI expression. freein :: String -> Ski -> Bool-freein x (Cte y) = not (x == y)+freein x (Cte y) = x /= y freein x (Comb u v) = freein x u && freein x v freein _ _ = True
source/Types.hs view
@@ -1,8 +1,7 @@ module Types- ( Type (Tvar, Arrow)- , typeinfer+ ( Type (Tvar, Arrow, Times, Union, Unitty, Bottom) , typeinference- , normalize+ , Top (Top) ) where @@ -13,10 +12,10 @@ -- | A type context is a map from deBruijn indices to types. Given -- any lambda variable as a deBruijn index, it returns its type.-type Context = Map.Map Integer Type+type Context = Map.Map Integer Type -- | A type variable is an integer.-type Variable = Integer+type Variable = Integer -- | A type substitution is a function that can be applied to any type -- to get a new one.@@ -24,21 +23,25 @@ -- | A type template is a free type variable or an arrow between two -- types; that is, the function type.-data Type = Tvar Variable- | Arrow Type Type- | Times Type Type- | Union Type Type- | Unitty- | Bottom+data Type+ = Tvar Variable+ | Arrow Type+ Type+ | Times Type+ Type+ | Union Type+ Type+ | Unitty+ | Bottom deriving (Eq) instance Show Type where- show (Tvar t) = typevariableNames !! (fromInteger t)+ show (Tvar t) = typevariableNames !! fromInteger t show (Arrow a b) = showparens a ++ " → " ++ show b show (Times a b) = showparens a ++ " × " ++ showparens b show (Union a b) = showparens a ++ " + " ++ showparens b- show (Unitty) = "⊤"- show (Bottom) = "⊥"+ show Unitty = "⊤"+ show (Bottom) = "⊥" showparens :: Type -> String showparens (Tvar t) = show (Tvar t)@@ -64,7 +67,7 @@ occurs x (Arrow a b) = occurs x a || occurs x b occurs x (Times a b) = occurs x a || occurs x b occurs x (Union a b) = occurs x a || occurs x b-occurs _ (Unitty) = False+occurs _ Unitty = False occurs _ (Bottom) = False -- | Unifies two types with their most general unifier. Returns the substitution@@ -79,22 +82,20 @@ unify a (Tvar y) | occurs y a = Nothing | otherwise = Just (subs y a)-unify (Arrow a b) (Arrow c d) = do- p <- unify b d- q <- unify (p a) (p c)- return (q . p)-unify (Times a b) (Times c d) = do- p <- unify b d- q <- unify (p a) (p c)- return (q . p)-unify (Union a b) (Union c d) = do- p <- unify b d- q <- unify (p a) (p c)- return (q . p)+unify (Arrow a b) (Arrow c d) = unifypair (a,b) (c,d)+unify (Times a b) (Times c d) = unifypair (a,b) (c,d)+unify (Union a b) (Union c d) = unifypair (a, b) (c, d) unify Unitty Unitty = Just id unify Bottom Bottom = Just id unify _ _ = Nothing +-- | Unifies a pair of types+unifypair :: (Type,Type) -> (Type,Type) -> Maybe Substitution+unifypair (a,b) (c,d) = do+ p <- unify b d+ q <- unify (p a) (p c)+ return (q . p)+ -- | Apply a substitution to all the types on a type context. applyctx :: Substitution -> Context -> Context applyctx = Map.map@@ -164,12 +165,12 @@ typeinfer (x:y:vars) ctx (Inl m) a = do sigma <- unify a (Union (Tvar x) (Tvar y))- tau <- typeinfer vars (applyctx sigma ctx) m (sigma (Tvar x))+ tau <- typeinfer vars (applyctx sigma ctx) m (sigma (Tvar x)) return (tau . sigma) typeinfer (x:y:vars) ctx (Inr m) a = do sigma <- unify a (Union (Tvar x) (Tvar y))- tau <- typeinfer vars (applyctx sigma ctx) m (sigma (Tvar y))+ tau <- typeinfer vars (applyctx sigma ctx) m (sigma (Tvar y)) return (tau . sigma) typeinfer (x:y:vars) ctx (Caseof m f g) a = do@@ -232,8 +233,8 @@ -- | Applies a set of variable substitutions to a type to normalize it. applynormalization :: Map.Map Integer Integer -> Type -> Type applynormalization sub (Tvar m) = case Map.lookup m sub of- Just n -> (Tvar n)- Nothing -> (Tvar m)+ Just n -> Tvar n+ Nothing -> Tvar m applynormalization sub (Arrow a b) = Arrow (applynormalization sub a) (applynormalization sub b) applynormalization sub (Times a b) = Times (applynormalization sub a) (applynormalization sub b) applynormalization sub (Union a b) = Union (applynormalization sub a) (applynormalization sub b)@@ -246,3 +247,22 @@ -- the smaller possible ones. normalize :: Type -> Type normalize t = applynormalization (fst $ normalizeTemplate Map.empty 0 t) t+++++-- This is definitely not an easter egg+newtype Top = Top Type+instance Show Top where+ show (Top (Tvar t)) = typevariableNames !! fromInteger t+ show (Top (Arrow a Bottom)) = "(Ω∖" ++ showparensT (Top a) ++ ")ᴼ"+ show (Top (Arrow a b)) = "((Ω∖" ++ showparensT (Top a) ++ ") ∪ " ++ showparensT (Top b) ++ ")ᴼ"+ show (Top (Times a b)) = showparensT (Top a) ++ " ∩ " ++ showparensT (Top b)+ show (Top (Union a b)) = showparensT (Top a) ++ " ∪ " ++ showparensT (Top b)+ show (Top Unitty) = "Ω"+ show (Top (Bottom)) = "Ø"+showparensT :: Top -> String+showparensT (Top (Tvar t)) = show (Top (Tvar t))+showparensT (Top Unitty) = show (Top Unitty)+showparensT (Top Bottom) = show (Top Bottom)+showparensT (Top m) = "(" ++ show (Top m) ++ ")"
+ tests/test.hs view
@@ -0,0 +1,131 @@+import Test.Tasty+import Test.Tasty.HUnit+import Test.Tasty.QuickCheck as QC++import Text.ParserCombinators.Parsec+import NamedLambda+import Lambda+import Types+import Ski+import Environment+++main :: IO ()+main = defaultMain tests++tests :: TestTree+tests = testGroup "Tests"+ [ parserTests+ , typeinferTests+ , skiabsTests+ , lambdaProps+ ]++-- Unit tests+parserTests :: TestTree+parserTests = testGroup "Parser tests"+ [ testCase "INR parser test" $+ parse lambdaexp "" "INR (\\x.y)"+ @?=+ Right (TypedInr (LambdaAbstraction "x" (LambdaVariable "y")))++ , testCase "INL parser test" $+ parse lambdaexp "" "INL (\\ab.cd)"+ @?=+ Right (TypedInl (LambdaAbstraction "ab" (LambdaVariable "cd")))++ , testCase "Spaces between lambdas test" $+ parse lambdaexp "" "(\\x. x)"+ @?=+ Right (LambdaAbstraction "x" (LambdaVariable "x"))++ , testCase "Multiple-character variable name test" $+ parse lambdaexp "" "(\\asdf. asdf)"+ @?=+ Right (LambdaAbstraction "asdf" (LambdaVariable "asdf"))+ ]++typeinferTests :: TestTree+typeinferTests = testGroup "Type inference tests"+ [ testCase "Identity type inference" $+ typeinference (Lambda (Var 1))+ @?=+ Just (Arrow (Tvar 0) (Tvar 0))++ , testCase "Double negation of LEM" $+ typeinference (Lambda (Absurd ((App (Var 1) (Inr (Lambda (App (Var 2) (Inl (Var 1)))))))))+ @?=+ Just (Arrow (Arrow (Union (Tvar 0) (Arrow (Tvar 0) Bottom)) Bottom) Bottom)+ ]++skiabsTests :: TestTree+skiabsTests = testGroup "SKI abstraction tests"+ [ testCase "Identity SKI abstraction" $+ skiabs (LambdaAbstraction "x" (LambdaVariable "x"))+ @?=+ I++ , testCase "Numeral 2 SKI abstraction" $+ skiabs (LambdaAbstraction "a"+ (LambdaAbstraction "b"+ (LambdaApplication (LambdaVariable "a")+ (LambdaApplication (LambdaVariable "a") (LambdaVariable "b")))))+ @?=+ Comb (Comb S (Comb (Comb S (Comb K S)) K)) I+ ]+++-- Lambda properties+lambdaProps :: TestTree+lambdaProps = testGroup "Lambda expression properties (quickcheck)"+ [ QC.testProperty "expression -> named -> expression" $+ \exp -> toBruijn emptyContext (nameExp exp) == exp+ , QC.testProperty "open expressions not allowed" $+ \exp -> isOpenExp exp == False+ ]+ ++-- Arbitrary untyped lambda expressions+-- {-# LANGUAGE TypeSynonymInstances #-}+-- type UntypedExp = Exp+-- instance Arbitrary UntypedExp where+-- arbitrary = sized (untlambda 0)++-- untlambda :: Int -> Int -> Gen UntypedExp+-- untlambda 0 0 = return $ Lambda (Var 1)+-- untlambda 0 size = Lambda <$> untlambda 1 (size-1)+-- untlambda lim 0 = Var <$> (toInteger <$> (choose (1, lim)))+-- untlambda lim size = oneof+-- [ Var <$> (toInteger <$> choose (1, lim))+-- , Lambda <$> untlambda (succ lim) (size-1)+-- , App <$> untlambda lim (div size 2) <*> untlambda lim (div size 2)+-- ]+++-- Arbitrary typed lambda expressions+instance Arbitrary Exp where+ arbitrary = sized (lambda 0)++lambda :: Int -> Int -> Gen Exp+lambda 0 0 = return $ Lambda (Var 1)+lambda 0 size = Lambda <$> lambda 1 (size-1)+lambda lim 0 = Var <$> (toInteger <$> (choose (1, lim)))+lambda lim size = oneof+ [ Var <$> (toInteger <$> choose (1, lim))+ , Lambda <$> lambda (succ lim) (size-1)+ , App <$> lambda lim (div size 2) <*> lambda lim (div size 2)+ , Pair <$> lambda lim (div size 2) <*> lambda lim (div size 2)+ , Pi1 <$> (Pair <$> lambda lim (div size 2) <*> lambda lim (div size 2))+ , Pi2 <$> (Pair <$> lambda lim (div size 2) <*> lambda lim (div size 2))+ , Inl <$> lambda lim (size-1)+ , Inr <$> lambda lim (size-1)+ , Caseof <$> (Inl <$> lambda lim (div size 3))+ <*> (Lambda <$> lambda (succ lim) (div size 3))+ <*> (Lambda <$> lambda (succ lim) (div size 3))+ , Caseof <$> (Inr <$> lambda lim (div size 3))+ <*> (Lambda <$> lambda (succ lim) (div size 3))+ <*> (Lambda <$> lambda (succ lim) (div size 3))+ , return Unit+ , Abort <$> lambda lim (size-1)+ , Absurd <$> lambda lim (size-1)+ ]