mikrokosmos 0.6.0 → 0.8.0
raw patch · 15 files changed
+1051/−667 lines, 15 filesdep +processdep +tasty-golden
Dependencies added: process, tasty-golden
Files
- README.md +7/−3
- mikrokosmos.cabal +20/−9
- source/Format.hs +10/−2
- source/Interpreter.hs +144/−54
- source/Lambda.hs +1/−1
- source/Libraries.hs +106/−0
- source/Main.hs +80/−79
- source/NamedLambda.hs +87/−21
- source/Ski.hs +14/−14
- source/Stlc/Block.hs +87/−0
- source/Stlc/Gentzen.hs +188/−0
- source/Stlc/Types.hs +275/−0
- source/Types.hs +0/−268
- std.mkr +0/−192
- tests/test.hs +32/−24
README.md view
@@ -1,7 +1,10 @@ # mikrokosmos +++ <p align="center">- <img src ="https://raw.githubusercontent.com/M42/mikrokosmos/master/docs/icon.svg.png" />+ <img src ="https://raw.githubusercontent.com/mroman42/mikrokosmos/master/docs/icon.svg.png" /> </p> **Mikrokosmos** is a λ-calculus interpreter, borrowing its name from the series of@@ -9,6 +12,7 @@ It aims to provide students with a tool to learn and understand λ-calculus. It supports both untyped λ-calculus 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).+ * [Try Mikrokosmos!](https://mroman42.github.io/mikrokosmos/)+ * [Mikrokosmos tutorial](https://mroman42.github.io/mikrokosmos/tutorial.html).+ * [Mikrokosmos user's guide](https://mroman42.github.io/mikrokosmos/userguide.html). * [Mikrokosmos on Hackage](https://hackage.haskell.org/package/mikrokosmos).
mikrokosmos.cabal view
@@ -1,23 +1,22 @@ name: mikrokosmos-version: 0.6.0+version: 0.8.0 synopsis: Lambda calculus interpreter description: A didactic untyped lambda calculus interpreter.-homepage: https://github.com/M42/mikrokosmos-bug-reports: https://github.com/M42/mikrokosmos/issues+homepage: https://github.com/mroman42/mikrokosmos+bug-reports: https://github.com/mroman42/mikrokosmos/issues license: GPL-3 license-file: LICENSE-author: Mario Román (M42)+author: Mario Román (mroman42) maintainer: mromang08+github@gmail.com category: Language build-type: Simple extra-source-files: README.md cabal-version: >=1.10 tested-with: GHC == 8.0.2-extra-source-files: std.mkr source-repository head type: git- location: git://github.com/M42/mikrokosmos.git+ location: git://github.com/mroman42/mikrokosmos.git @@ -36,6 +35,7 @@ tasty, tasty-hunit, tasty-quickcheck,+ tasty-golden, directory >= 1.0 other-modules: Format@@ -45,7 +45,10 @@ Interpreter Environment Ski- Types+ Libraries+ Stlc.Types+ Stlc.Gentzen+ Stlc.Block default-language: Haskell2010 ghc-options: -Wall@@ -60,6 +63,7 @@ source main-is: test.hs+ build-depends: base >=4.7 && <5, mtl >=2.2, containers >= 0.5,@@ -71,8 +75,11 @@ options, tasty, tasty-hunit,+ tasty-golden, tasty-quickcheck,- directory >= 1.0+ directory >= 1.0,+ process+ other-modules: Format Lambda NamedLambda@@ -80,4 +87,8 @@ Interpreter Environment Ski- Types+ Libraries+ Stlc.Types+ Stlc.Gentzen+ Stlc.Block+
source/Format.hs view
@@ -32,6 +32,7 @@ , errorTypeConstructors , errorUndefinedText , errorUnknownCommand+ , errorNotFoundText ) where @@ -85,6 +86,7 @@ , formatType , formatPrompt , formatLoading+ , formatError , end ] @@ -118,6 +120,12 @@ "Error: undefined terms on the lambda expression" ++ end +errorNotFoundText :: String+errorNotFoundText =+ formatError +++ "Error: module or dependencies cannot be found"+ ++ end+ restartText :: String restartText = "Mikrokosmos context has been cleaned up" @@ -150,10 +158,10 @@ formatFormula ++ "Version " ++ version ++ ". GNU General Public License Version 3." ++ end ] --- | Version complete text+-- | Version, complete text versionText :: String versionText = "Mikrokosmos, version " ++ version -- | Version version :: String-version = "0.6.0"+version = "0.8.0"
source/Interpreter.hs view
@@ -15,6 +15,9 @@ , multipleAct , Action (..) , actionParser+ , executeWithEnv+ , librariesEnv+ , preformat ) where @@ -27,45 +30,115 @@ import Environment import NamedLambda import Lambda+import Libraries import Ski-import Types+import Stlc.Types+import Stlc.Gentzen +-- | Execute a block of code in a given environment+executeWithEnv :: Environment -> String -> (String, Environment)+executeWithEnv initEnv block = do+ let parsing = map (parse actionParser "" . preformat) . filter (/="") . lines $ block+ let actions = mapMaybe (\x -> case x of+ Left _ -> Nothing+ Right a -> Just a) parsing+ case runState (multipleAct actions) initEnv of+ (outputs, env) -> (unlines outputs, env)++-- | Default environment plus standard libraries+librariesEnv :: Environment+librariesEnv = snd $ executeWithEnv defaultEnv stdlibraries++-- | Preformats text before sending it to the interpreter+preformat :: String -> String+preformat = reverse . dropWhile (==' ') . reverse . dropWhile (==' ')+ -- | Interpreter action. It can be a language action (binding and evaluation) -- or an interpreter specific one, such as "quit". data InterpreterAction = Interpret Action -- ^ Language action- | EmptyLine -- ^ Empty line, it will be ignored- | Error -- ^ Error on the interpreter | Quit -- ^ Close the interpreter- | Restart -- ^ Restarts the environment | Load String -- ^ Load the given file- | SetVerbose Bool -- ^ Changes verbosity- | 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; -- all on the following possible forms. data Action = Bind (String, NamedLambda) -- ^ bind a name to an expression | EvalBind (String, NamedLambda) -- ^ bind a name to an expression and simplify it | Execute NamedLambda -- ^ execute an expression+ | Diagram NamedLambda -- ^ show the diagram of a lambda expression+ | SimpDiagram NamedLambda -- ^ show the diagram of the simplified expression | Comment -- ^ comment-+ | EmptyLine -- ^ empty line, it will be ignored+ | Error -- ^ error on the interpreter+ | Restart -- ^ restarts the environment+ | Help -- ^ shows help+ | Ask String -- ^ asks for the definition of a function+ | SetVerbose Bool -- ^ changes verbosity+ | SetColor Bool -- ^ changes colors+ | SetSki Bool -- ^ changes ski output+ | SetTypes Bool -- ^ changes type configuration+ | SetTopo Bool + -- | Executes a language action. Given a context and an action, returns -- the new context after the action and a text output. act :: Action -> State Environment [String] act Comment = return [""]-act (Bind (s,le)) =- do modify (\env -> addBind env s (toBruijn (context env) le))- return [""]-act (EvalBind (s,le)) =- do modify (\env -> addBind env s (simplifyAll $ toBruijn (context env) le))- return [""]+act (Bind (s,le)) = do+ modify (\env -> addBind env s (toBruijn (context env) le))+ return [""]+act (EvalBind (s,le)) = do+ modify (\env -> addBind env s (simplifyAll $ toBruijn (context env) le))+ return [""] act (Execute le) = executeExpression le+act (Diagram le) = drawDiagram False le+act (SimpDiagram le) = drawDiagram True le+act EmptyLine = return [""]+act Error = return [errorUnknownCommand ++ "\n"]+act Restart = put defaultEnv >> return [restartText ++ "\n"]+act Help = return [helpText ++ "\n"]+act (SetVerbose setting) = setOption setting changeVerbose "verbose: "+act (SetColor setting) = setOption setting changeColor "color mode: "+act (SetSki setting) = setOption setting changeSkioutput "ski mode: "+act (SetTypes setting) = setOption setting changeTypes "types: "+act (SetTopo setting) = setOption setting changeTopo "topology: "+act (Ask func) = return $ askfor func ++-- | Asks for the name of a function.+askfor :: String -> [String]+askfor func = case stdquery func of+ Nothing -> ["Error: the function '" ++ func ++ "' is not defined on the standard library.\n"]+ Just f -> [description f ++ "\n", "Defined as: " ++ code f,"\n"]+ ++-- | Sets the given option on/off.+setOption :: Bool ->+ (Environment -> Bool -> Environment) ->+ String ->+ State Environment [String]+setOption setting change message = do+ modify (`change` setting)+ env <- get+ return [messageenv env ++ "\n"]+ where messageenv env =+ (if getColor env then formatFormula else "") ++ message +++ (if setting then "on" else "off") ++ end++drawDiagram :: Bool -> NamedLambda -> State Environment [String]+drawDiagram wantsimplification le = do+ env <- get+ let bruijn = toBruijn (context env) le+ let isopen = isOpenExp bruijn+ let simpbruijn = simplifyAll bruijn+ let maybediagram = gentzendiagram (if wantsimplification then simpbruijn else bruijn)++ return $+ if isopen then [errorUndefinedText ++ "\n"] else+ case maybediagram of+ Nothing -> [errorNonTypeableText ++ "\n"]+ Just diagram -> map (++ "\n") . lines $ showProofTree diagram+ -- | Executes a lambda expression. Given the context, returns the new -- context after the evaluation. executeExpression :: NamedLambda -> State Environment [String]@@ -78,6 +151,8 @@ let verbose = getVerbose env let completeexp = showCompleteExp env $ simplifyAll bruijn let isopen = isOpenExp bruijn+ let coloring = getColor env+ let decolorif = if coloring then id else decolor return $ if isopen then [errorUndefinedText ++ "\n"] else@@ -86,7 +161,7 @@ if not verbose then [completeexp ++ "\n"] else [unlines $ [show le] ++- [unlines $ map showReduction $ simplifySteps bruijn] +++ [unlines $ map (decolorif . showReduction) $ simplifySteps bruijn] ++ [completeexp] ] @@ -100,25 +175,22 @@ -- | Shows an expression and the name that is bound to the expression -- in the current context showCompleteExp :: Environment -> Exp -> String-showCompleteExp environment expr = let- lambdaname = show $ nameExp expr- skiname = if getSki environment- then formatSubs2 ++ " ⇒ " ++ show (skiabs $ nameExp expr) ++ end- else ""- inferredtype = typeinference expr- typename = if getTypes environment- then formatType ++ " :: " ++ (case inferredtype of- Just s -> if getTopo environment- then show (Top s)- else show s- Nothing -> "Type error!") ++ end- else ""- expName = case getExpressionName environment expr of- Nothing -> ""- Just exname -> formatName ++ " ⇒ " ++ exname ++ end- in- lambdaname ++ skiname ++ expName ++ typename ++ end- +showCompleteExp environment expr = + lambdaname ++ skiname ++ expName ++ typename ++ end+ where+ coloring = getColor environment+ ifvoid b x = if b then x else ""+ typesset = getTypes environment+ skiset = getSki environment+ lambdaname = show $ nameExp expr+ skiname = ifvoid skiset $ formatSubs2 ++ " ⇒ " ++ show (skiabs $ nameExp expr) ++ end+ inferredtype = case typeinference expr of+ Just s -> if getTopo environment then show (Top s) else show s+ Nothing -> "Type error!"+ typename = ifvoid typesset $ ifvoid coloring formatType ++ " :: " ++ inferredtype ++ end+ expName = case getExpressionName environment expr of+ Just exname -> ifvoid coloring formatName ++ " ⇒ " ++ exname ++ end+ Nothing -> "" -- Parsing of interpreter command line commands.@@ -127,14 +199,7 @@ interpreteractionParser = choice [ try interpretParser , try quitParser- , try restartParser , try loadParser- , try verboseParser- , try colorParser- , try skiOutputParser- , try typesParser- , try topoParser- , try helpParser ] -- | Parses a language action as an interpreter action.@@ -143,16 +208,37 @@ -- | Parses a language action. actionParser :: Parser Action-actionParser = choice- [ try bindParser- , try evalbindParser- , try executeParser- , try commentParser+actionParser = choice $ map try+ [ simpdiagramParser+ , diagramParser+ , bindParser+ , evalbindParser+ , executeParser+ , commentParser+ , helpParser+ , askParser+ , restartParser+ , verboseParser+ , colorParser+ , skiOutputParser+ , typesParser+ , topoParser ] ++-- | Parses a diagram request+diagramParser :: Parser Action+diagramParser = Diagram <$> (string "@ " >> lambdaexp)++-- | Parses a simplfication and diagram request+simpdiagramParser :: Parser Action+simpdiagramParser = SimpDiagram <$> (string "@@ " >> lambdaexp)+ -- | Parses a binding between a variable an its representation. bindParser :: Parser Action-bindParser = fmap Bind $ (,) <$> many1 alphaNum <*> (spaces >> string "!=" >> spaces >> lambdaexp)+bindParser = fmap Bind $ (,) <$>+ many1 alphaNum <*>+ (spaces >> choice [try (string "!="), try (string ":=")] >> spaces >> lambdaexp) -- | Parses a binding and evaluation expression between a variable an its representation evalbindParser :: Parser Action@@ -162,18 +248,22 @@ executeParser :: Parser Action executeParser = Execute <$> lambdaexp +-- | Parses a definition request to the interpreter.+askParser :: Parser Action+askParser = Ask <$> (string ":? " >> many1 alphaNum)+ -- | Parses comments. commentParser :: Parser Action commentParser = string "#" >> many anyChar >> return Comment --- | Parses a "quit" command.-quitParser, restartParser, helpParser :: Parser InterpreterAction+quitParser :: Parser InterpreterAction quitParser = string ":quit" >> return Quit+restartParser, helpParser :: Parser Action restartParser = string ":restart" >> return Restart helpParser = string ":help" >> return Help -- | Parses a change in a setting-settingParser :: (Bool -> InterpreterAction) -> String -> Parser InterpreterAction+settingParser :: (Bool -> Action) -> String -> Parser Action settingParser setSetting settingname = choice [ try settingonParser , try settingoffParser@@ -183,7 +273,7 @@ settingoffParser = string (settingname ++ " off") >> return (setSetting False) -- | Multiple setting parsers-verboseParser, colorParser, skiOutputParser, typesParser, topoParser :: Parser InterpreterAction+verboseParser, colorParser, skiOutputParser, typesParser, topoParser :: Parser Action verboseParser = settingParser SetVerbose ":verbose" colorParser = settingParser SetColor ":color" skiOutputParser = settingParser SetSki ":ski"
source/Lambda.hs view
@@ -89,7 +89,7 @@ -- Reductions of lambda expressions. -- | Applies repeated simplification to the expression until it stabilizes and--- returns the final simplified expression.+-- returns the final simplified expression. -- -- >>> simplifyAll $ App (Lambda (Var 1)) (Lambda (Var 1)) -- λ1
+ source/Libraries.hs view
@@ -0,0 +1,106 @@+module Libraries+ ( stdlibraries+ , stdmap+ , stdquery+ , code+ , name+ , description+ )+where++import qualified Data.Map as M+import Control.Arrow++stdlibraries :: String+stdlibraries = unlines $ map code stdfunctions++stdquery :: String -> Maybe Function+stdquery = flip M.lookup stdmap++stdmap :: M.Map String Function+stdmap = M.fromList $ map (name &&& id) stdfunctions++data Function = Function+ { name :: String+ , code :: String+ , description :: String+ }+ deriving (Show)++stdfunctions :: [Function]+stdfunctions = + [ Function "id" "id = \\x.x" "Identity function. Returns its argument unchanged."+ , Function "const" "const = \\x.\\y.x" "Binay function evaluating to its first argument."+ , Function "compose" "compose = \\f.\\g.\\x.f (g x)" "Function composition."+ , Function "true" "true = \\a.\\b.a" "Boolean 'true', using Church encoding."+ , Function "false" "false = \\a.\\b.b" "Boolean 'false', using Church encoding."+ , Function "and" "and = \\p.\\q.p q p" "Boolean conjunction."+ , Function "or" "or = \\p.\\q.p p q" "Boolean disjunction."+ , Function "not" "not = \\b.b false true" "Boolean negation."+ , Function "implies" "implies = \\a.\\b.or (not a) b" "Boolean implication."+ , Function "ifelse" "ifelse = (\\x.x)" "Identity function, can be used as a boolean case analysis."+ , Function "succ" "succ = \\n.\\f.\\x.f (n f x)" "Return the successor of a natural number."+ , Function "0" "0 = \\f.\\x.x" "The natural number 0, using Church encoding."+ , Function "plus" "plus = \\m.\\n.\\f.\\x.m f (n f x)" "Adds two natural numbers."+ , Function "mult" "mult = \\m.\\n.\\f.\\x.m (n f) x" "Multiplies two natural numbers."+ , Function "pred" "pred = \\n.\\f.\\x.n (\\g.(\\h.h (g f))) (\\u.x) (\\u.u)" "Predecessor of a natural number"+ , Function "minus" "minus = \\m.\\n.(n pred) m" "Substracts two natural numbers"+ , Function "iszero" "iszero = \\n.(n (\\x.false) true)" "Returns true if the natural number is zero."+ , Function "leq" "leq = \\m.\\n.(iszero (minus m n))" "Returns true if the first argument is a natural number lesser or equal than the second."+ , Function "geq" "geq = \\m.\\n.(iszero (minus n m))" "Returns true if the first argument is a natural number greater or equal than the second."+ , Function "lt" "lt = \\m.\\n.not (geq m n)" "Returns true if the first argument is a natural number lesser than the second."+ , Function "gt" "gt = \\m.\\n.not (leq m n)" "Returns true if the first argument is a natural number greater than the second."+ , Function "eq" "eq = \\m.\\n.(and (leq m n) (leq n m))" "Returns true if the two natural numbers are equal."+ , Function "S" "S = \\x.\\y.\\z. x z (y z)" "S combinator. Substitution operator."+ , Function "K" "K = \\x.\\y.x" "K combinator. Constant operator."+ , Function "I" "I = S K K" "I combinator. Identity operator."+ , Function "C" "C = \\f.\\x.\\y.f y x" "C combinator."+ , Function "B" "B = \\f.\\g.\\x.f (g x)" "B combinator."+ , Function "W" "W = \\x.\\y.(y y)" "W combinator."+ , Function "Y" "Y != \\f.(\\x.f (x x))(\\x.f (x x))" "Y combinator. Fixed-point combinator."+ , Function "tuple" "tuple = \\x.\\y.\\z.z x y" "Untyped tuple constructor. Takes a and b and returns the tuple (a,b)."+ , Function "first" "first = \\p.p true" "Untyped tuple projection. Returns the first element of a tuple."+ , Function "second" "second = \\p.p false" "Untyped tuple projection. Returns the second element of a tuple."+ , Function "cons" "cons = \\h.\\t.\\c.\\n.(c h (t c n))" "List constructor. Appends an element to the head of the list."+ , Function "nil" "nil = \\c.\\n.n" "List constructor. Creates the empty list."+ , Function "foldr" "foldr = \\o.\\n.\\l.(l o n)" "List folding. Combines the elements of the list using a binary operation."+ , Function "fold" "fold = \\o.\\n.\\l.(l o n)" "List folding. Combines the elements of the list using a binary operation."+ , Function "head" "head = fold const nil" "Returns the head of a list."+ , Function "tail" "tail = \\l.first (l (\\a.\\b.tuple (second b) (cons a (second b))) (tuple nil nil))" "Extracts the head of a list."+ , Function "take" "take = \\n.\\l.first (n (\\t.tuple (cons (head (second t)) (first t)) (tail (second t))) (tuple nil l))" "Extracts all the elements except the head of a list"+ , Function "sum" "sum = (foldr plus 0)" "Adds a list of natural numbers."+ , Function "prod" "prod = (foldr mult (succ 0))" "Multiplies a list of natural numbers."+ , Function "length" "length = (foldr (\\h.\\t.succ t) 0)" "Returns the length of a list."+ , Function "map" "map = (\\f.(foldr (\\h.\\t.cons (f h) t) nil))" "Maps a function over a list. Returns a list obtained by applying the function to each element of the original list."+ , Function "filter" "filter = \\p.(foldr (\\h.\\t.((p h) (cons h t) t)) nil)" "Filters a list with a predicate. Returns a list containing only the elements that satisfy the predicate."+ , Function "node" "node = \\x.\\l.\\r.\\f.\\n.(f x (l f n) (r f n))" "Binary tree constructor. Creates a tree whose root is given by the first argument and whose left and right subtrees are given by the second and third arguments, respectively."+ , Function "omega" "omega := (\\x.(x x))(\\x.(x x))" "Omega combinator. An example of a non-reducible lambda calculus expression."+ , Function "fix" "fix := (\\f.(\\x.f (x x)) (\\x.f (x x)))" "Fixed-point combinator. Given f, returns an element x such that f x = x."+ , Function "fact" "fact := fix (\\f.\\n.iszero n (succ 0) (mult n (f (pred n))))" "Factorial of a natural number."+ , Function "fib" "fib := fix (\\f.\\n.iszero n (succ 0) (plus (f (pred n)) (f (pred (pred n)))))" "Returns the n-th Fibonacci number."+ , Function "naturals" "naturals := fix (compose (cons 0) (map (plus 1)))" "Infinite list of the natural numbers."+ , Function "infinity" "infinity := fix succ" "Fixed point of the successor function on the natural numbers."+ , Function "division" "division := fix (\\d.\\q.\\a.\\b. lt a b (tuple q a) (d (succ q) (minus a b) b)) 0" "Integer division between natural numbers. Returns the quotient and the modulo."+ , Function "mu" "mu := \\p.fix (\\f.\\n.(p n) n (f (succ n))) 0" "Göedel mu-operator. Finds the first natural number satisfying a certain predicate."+ , Function "div" "div := \\a.\\b.first (division a b)" "Quotient of the division between two natural numbers."+ , Function "mod" "mod := \\a.\\b.second (division a b)" "Modulo of the division between two natural numbers."+ , Function "pair" "pair = \\x.\\y.(x,y)" "Pair constructor of the simply-typed lambda calculus."+ , Function "fst" "fst = \\x.FST x" "First projection of a typed pair."+ , Function "snd" "snd = \\x.SND x" "Second projection of a typed pair."+ , Function "inl" "inl = \\x.INL x" "First injection of a typed sum."+ , Function "inr" "inr = \\x.INR x" "Second injection of a typed sum."+ , Function "caseof" "caseof = \\x.\\y.\\z.CASE x OF (\\a.y a);(\\a.z a)" "Case analysis of a sum type."+ , Function "unit" "unit = UNIT" "The only element of the unit type."+ , Function "abort" "abort = \\x.ABORT x" "Takes an element of the empty type and creates an element of any given type."+ , Function "absurd" "absurd = \\x.ABSURD x" "Takes an element of the empty type and creates an element of any given type."+ ] ++ natsdef+ where+ fnat :: Int -> Function+ fnat n = Function+ (show (n+1))+ (show (n+1) ++ " = succ " ++ show n)+ ("The natural number " ++ show (n+1) ++ ", using Church encoding.")+ + natsdef :: [Function]+ natsdef = map fnat [0..999]+
source/Main.hs view
@@ -4,6 +4,7 @@ import Control.Monad.State import Control.Exception import Data.List+import Data.Foldable (forM_) import System.Directory import System.Console.Haskeline import Text.ParserCombinators.Parsec hiding (try)@@ -13,7 +14,7 @@ import Options hiding (defaultOptions) --- Lambda interpreter+-- Lambda interpreter. -- The actions of the interpreter are written here. It allows to execute normal -- actions (bindings and evaluation), and interpreter specific actions, as "quit" -- or "load".@@ -22,19 +23,23 @@ -- | Runs the interpreter with default settings and an empty context. main :: IO () main =- -- 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- -- Reads the flags- ->- if flagVersion opts- then putStrLn versionText- else case args of+ -- Uses the Options library, which requires the program to start+ -- with runCommand. The command-line flags are stored in opts and+ -- other command line arguments are stored in args.+ runCommand $ \opts args -> do+ -- Reads the libaries flag. If activated, it will not automatically+ -- load the libraries.+ let initialEnv = if flagLibs opts then defaultEnv else librariesEnv+ -- Reads the rest of the flags. The --version flag shows the current+ -- version of the interpreter. An optional argument may be used to+ -- indicate a file to load.+ if flagVersion opts+ then putStrLn versionText+ else case args of [] -> runInputT defaultSettings- (outputStrLn initialText >> interpreterLoop defaultEnv)+ (outputStrLn initialText >> interpreterLoop initialEnv) [filename] -> executeFile filename _ -> putStrLn "Wrong number of arguments" @@ -47,68 +52,59 @@ let interpreteraction = case minput of Nothing -> Quit- Just "" -> EmptyLine+ Just "" -> Interpret EmptyLine Just input ->- case parse interpreteractionParser "" input of- Left _ -> Error+ case parse interpreteractionParser "" (preformat input) of+ Left _ -> Interpret 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++ newenvironment <- executeAction environment interpreteraction+ forM_ newenvironment interpreterLoop+ ++-- | Executes the parsed action, every action may affect the context+-- in a way, and returns the control to the interpreter.+executeAction :: Environment -> InterpreterAction -> InputT IO (Maybe Environment)+executeAction environment interpreteraction = + case interpreteraction of -- Interprets an action- of Interpret action -> case runState (act action) environment of (output, newenv) -> do outputActions newenv output- interpreterLoop newenv+ return $ Just 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])- files <- lift $ mapM findFilename modules- -- Concats all the module contents- maybeactions <- fmap concat . sequence <$> lift (mapM loadFile files)- case maybeactions of+ readallmoduledeps <- lift $ readAllModuleDepsRecursively [modulename]+ case readallmoduledeps 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- -- Ignores the empty line- EmptyLine -> interpreterLoop environment+ outputStrLn errorNotFoundText+ return $ Just environment+ Just readallmodules -> do+ let modules = nub readallmodules+ files <- lift $ mapM findFilename modules+ -- Concats all the module contents+ case sequence files of+ Nothing -> do+ outputStrLn errorNotFoundText+ return $ Just environment+ Just allfiles -> do+ maybeactions <- fmap concat . sequence <$> lift (mapM loadFile allfiles)+ case maybeactions of+ Nothing -> do+ outputStrLn "Error loading file"+ return $ Just environment+ Just actions ->+ case runState (multipleAct actions) environment of+ (output, newenv) -> do+ outputActions newenv output+ return $ Just newenv -- Exits the interpreter- Quit -> return ()- -- Restarts the interpreter context- Restart -> outputStrLn restartText >> interpreterLoop defaultEnv- -- Unknown command- Error -> outputStrLn errorUnknownCommand >> interpreterLoop environment- -- Sets the verbose option- 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+ Quit -> return Nothing --- | 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, -- formats and prints them in console. outputActions :: Environment -> [String] -> InputT IO ()@@ -127,14 +123,14 @@ -- Loading and reading files -- | Loads the given filename and returns the complete list of actions. -- Returns Nothing if there is an error reading or parsing the file.-loadFile :: String -> IO (Maybe [Action])+loadFile :: Filename -> IO (Maybe [Action]) loadFile filename = do putStrLn $ formatLoading ++ "Loading " ++ filename ++ "..." ++ end input <- try $ readFile filename :: IO (Either IOException String) case input of Left _ -> return Nothing Right inputs -> do- let parsing = map (parse actionParser "") $ filter (/="") $ lines inputs+ let parsing = map (parse actionParser "" . preformat) . filter (/="") . lines $ inputs let actions = map (\x -> case x of Left _ -> Nothing Right a -> Just a) parsing@@ -149,11 +145,7 @@ 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-+ (outputs, _) -> mapM_ putStr outputs -- | Reads module dependencies readFileDependencies :: Filename -> IO [Modulename]@@ -164,43 +156,51 @@ Right inputs -> return $ map (drop 9) (filter (isPrefixOf "#INCLUDE ") $ filter (/="") $ lines inputs) --- | Reads all the dependencies from a module list-readAllModuleDeps :: [Modulename] -> IO [Modulename]+-- | Reads all the dependencies from a module list.+-- Returns an error if a dependency cannot be found+readAllModuleDeps :: [Modulename] -> IO (Maybe [Modulename]) readAllModuleDeps modulenames = do files <- mapM findFilename modulenames- deps <- mapM readFileDependencies files- return $ concat deps+ deps <- mapM (mapM readFileDependencies) files+ return (concat <$> sequence deps) --- | Read module dependencies recursively-readAllModuleDepsRecursively :: [Modulename] -> IO [Modulename]+-- | Read module dependencies recursively.+-- Returns an error if a dependency cannot be found+readAllModuleDepsRecursively :: [Modulename] -> IO (Maybe [Modulename]) readAllModuleDepsRecursively modulenames = do- newmodulenames <- readAllModuleDeps modulenames- let allmodulenames = nub (newmodulenames ++ modulenames)- if modulenames == allmodulenames- then return modulenames- else readAllModuleDepsRecursively allmodulenames+ maybenewmodulenames <- readAllModuleDeps modulenames+ case maybenewmodulenames of+ Nothing -> return Nothing+ Just newmodulenames -> do+ let allmodulenames = nub (newmodulenames ++ modulenames)+ if modulenames == allmodulenames+ then return (Just modulenames)+ else readAllModuleDepsRecursively allmodulenames -- | Given a module name, returns the filename associated with it-findFilename :: Modulename -> IO Filename+findFilename :: Modulename -> IO (Maybe Filename) findFilename s = do appdir <- getAppUserDataDirectory "mikrokosmos" homedir <- getHomeDirectory -- Looks for the module in the common locations- head <$> filterM doesFileExist+ headMaybe <$> filterM doesFileExist [ "lib/" ++ s ++ ".mkr" , "./" ++ s ++ ".mkr" , appdir ++ "/" ++ s ++ ".mkr" , homedir ++ "/" ++ s ++ ".mkr" , "/usr/lib/mikrokosmos/" ++ s ++ ".mkr" ]+ where+ headMaybe [] = Nothing+ headMaybe (x:_) = Just x --- Flags -- | Flags datatype data MainFlags = MainFlags { flagExec :: String , flagVersion :: Bool+ , flagLibs :: Bool } instance Options MainFlags where@@ -208,3 +208,4 @@ defineOptions = pure MainFlags <*> simpleOption "exec" "" "A file to execute and show its results" <*> simpleOption "version" False "Show program version"+ <*> simpleOption "no-libs" False "Runs mikrokosmos without standard libraries"
source/NamedLambda.hs view
@@ -15,6 +15,8 @@ , lambdaexp , toBruijn , nameExp+ , quicknameIndexes+ , variableNames ) where @@ -91,6 +93,9 @@ nameParser :: Parser String nameParser = many1 alphaNum +choicest :: [String] -> Parser String+choicest sl = choice (try . string <$> sl)+ -- | Parses a lambda abstraction. The '\' is used as lambda. lambdaAbstractionParser :: Parser NamedLambda lambdaAbstractionParser = LambdaAbstraction <$>@@ -104,47 +109,92 @@ pairParser = parens (TypedPair <$> lambdaexp <*> (char ',' >> lambdaexp)) pi1Parser, pi2Parser :: Parser NamedLambda-pi1Parser = TypedPi1 <$> (string "FST " >> lambdaexp)-pi2Parser = TypedPi2 <$> (string "SND " >> lambdaexp)+pi1Parser = TypedPi1 <$> (choicest namesPi1 >> lambdaexp)+pi2Parser = TypedPi2 <$> (choicest namesPi2 >> lambdaexp) inlParser, inrParser :: Parser NamedLambda-inlParser = TypedInl <$> (string "INL " >> lambdaexp)-inrParser = TypedInr <$> (string "INR " >> lambdaexp)+inlParser = TypedInl <$> (choicest namesInl >> lambdaexp)+inrParser = TypedInr <$> (choicest namesInr >> lambdaexp) caseParser :: Parser NamedLambda-caseParser = TypedCase <$> (string "CASE " >> simpleexp) <*> (string " OF " >> simpleexp) <*> (string ";" >> simpleexp)+caseParser =+ TypedCase <$>+ (choicest namesCase >> simpleexp) <*>+ (choicest namesOf >> simpleexp) <*>+ (choicest namesCaseSep >> simpleexp) unitParser :: Parser NamedLambda-unitParser = string "UNIT" >> return TypedUnit+unitParser = choicest namesUnit >> return TypedUnit abortParser :: Parser NamedLambda-abortParser = TypedAbort <$> (string "ABORT " >> lambdaexp)+abortParser = TypedAbort <$> (choicest namesAbort >> lambdaexp) absurdParser :: Parser NamedLambda-absurdParser = TypedAbsurd <$> (string "ABSURD " >> lambdaexp)+absurdParser = TypedAbsurd <$> (choicest namesAbsurd >> lambdaexp) -- | Shows a lambda expression with named variables. -- Parentheses are ignored; they are written only around applications. showNamedLambda :: NamedLambda -> String-showNamedLambda (LambdaVariable c) = c-showNamedLambda (LambdaAbstraction c e) = "λ" ++ c ++ "." ++ showNamedLambda e ++ ""-showNamedLambda (LambdaApplication f g) = "(" ++ showNamedLambda f ++ " " ++ showNamedLambda g ++ ")"-showNamedLambda (TypedPair a b) = "(" ++ showNamedLambda a ++ "," ++ showNamedLambda b ++ ")"-showNamedLambda (TypedPi1 a) = "(" ++ "FST " ++ showNamedLambda a ++ ")"-showNamedLambda (TypedPi2 a) = "(" ++ "SND " ++ showNamedLambda a ++ ")"-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 (TypedAbort a) = "(" ++ "ABORT " ++ showNamedLambda a ++ ")"-showNamedLambda (TypedAbsurd a) = "(" ++ "ABSURD " ++ showNamedLambda a ++ ")"+showNamedLambda (LambdaVariable c) = c+showNamedLambda (LambdaAbstraction c e) = "λ" ++ c ++ "." ++ showNamedLambda e+showNamedLambda (LambdaApplication f g) =+ showNamedLambdaPar f ++ " " ++ showNamedLambdaPar g+showNamedLambda (TypedPair a b) =+ "(" ++ showNamedLambda a ++ "," ++ showNamedLambda b ++ ")"+showNamedLambda (TypedPi1 a) = head namesPi1 ++ showNamedLambdaPar a+showNamedLambda (TypedPi2 a) = head namesPi2 ++ showNamedLambdaPar a+showNamedLambda (TypedInl a) = head namesInl ++ showNamedLambdaPar a+showNamedLambda (TypedInr a) = head namesInr ++ showNamedLambdaPar a+showNamedLambda (TypedCase a b c) =+ last namesCase +++ showNamedLambda a +++ last namesOf ++ showNamedLambda b ++ head namesCaseSep ++ showNamedLambda c+showNamedLambda TypedUnit = head namesUnit+showNamedLambda (TypedAbort a) = head namesAbort ++ showNamedLambdaPar a+showNamedLambda (TypedAbsurd a) = head namesAbsurd ++ showNamedLambdaPar a +showNamedLambdaPar :: NamedLambda -> String+showNamedLambdaPar l@(LambdaVariable _) = showNamedLambda l+showNamedLambdaPar l@TypedUnit = showNamedLambda l+showNamedLambdaPar l@(TypedPair _ _) = showNamedLambda l+showNamedLambdaPar l = "(" ++ showNamedLambda l ++ ")"+ instance Show NamedLambda where show = showNamedLambda +-- Name type constructors+namesPi1 :: [String]+namesPi1 = ["π₁ ", "FST "] +namesPi2 :: [String]+namesPi2 = ["π₂ ", "SND "] +namesInl :: [String]+namesInl = ["ιnl ", "INL "]++namesInr :: [String]+namesInr = ["ιnr ", "INR "]++namesCase :: [String]+namesCase = ["CASE ", "Case ", "ᴄᴀꜱᴇ "]++namesOf :: [String]+namesOf = [" OF ", " Of ", " ᴏꜰ "]++namesCaseSep :: [String]+namesCaseSep = ["; ", ";"]++namesUnit :: [String]+namesUnit = ["★", "UNIT"]++namesAbort :: [String]+namesAbort = ["□ ", "ABORT "]++namesAbsurd :: [String]+namesAbsurd = ["■ ", "ABSURD "]++ -- | Translates a named variable expression into a DeBruijn one. -- Uses a dictionary of already binded numbers and variables. tobruijn :: Map.Map String Integer -- ^ dictionary of the names of the variables used@@ -195,9 +245,25 @@ 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)+++quicknameIndexes :: Int -> [String] -> Exp -> NamedLambda+quicknameIndexes _ _ (Var 0) = LambdaVariable "undefined"+quicknameIndexes n vars (Var m) = LambdaVariable (vars !! (n - fromInteger m))+quicknameIndexes n vars (Lambda e) = LambdaAbstraction (vars !! n) (quicknameIndexes (succ n) vars e)+quicknameIndexes n vars (App f g) = LambdaApplication (quicknameIndexes n vars f) (quicknameIndexes n vars g)+quicknameIndexes n vars (Pair a b) = TypedPair (quicknameIndexes n vars a) (quicknameIndexes n vars b)+quicknameIndexes n vars (Pi1 a) = TypedPi1 (quicknameIndexes n vars a)+quicknameIndexes n vars (Pi2 a) = TypedPi2 (quicknameIndexes n vars a)+quicknameIndexes n vars (Inl a) = TypedInl (quicknameIndexes n vars a)+quicknameIndexes n vars (Inr a) = TypedInr (quicknameIndexes n vars a)+quicknameIndexes n vars (Caseof a b c) = TypedCase (quicknameIndexes n vars a) (quicknameIndexes n vars b) (quicknameIndexes n vars c)+quicknameIndexes _ _ Unit = TypedUnit+quicknameIndexes n vars (Abort a) = TypedAbort (quicknameIndexes n vars a)+quicknameIndexes n vars (Absurd a) = TypedAbsurd (quicknameIndexes n vars a) -- | Gives names to every variable in a deBruijn expression using
source/Ski.hs view
@@ -45,21 +45,21 @@ showski (Comb x (Cte c)) = showski x ++ showski (Cte c) showski (Comb x (Comb u v)) = showski x ++ "(" ++ showski (Comb u v) ++ ")" showski (Comb x a) = showski x ++ showski a-showski (Spair) = "[PAIR]"-showski (Spi1) = "[FST]"-showski (Spi2) = "[SND]"-showski (Sinl) = "[INL]"-showski (Sinr) = "[INR]"-showski (Scase) = "[CASEOF]"-showski (Sunit) = "[UNIT]"-showski (Sabort) = "[ABORT]"-showski (Sabsurd) = "[ABSURD]"+showski Spair = "[PAIR]"+showski Spi1 = "[FST]"+showski Spi2 = "[SND]"+showski Sinl = "[INL]"+showski Sinr = "[INR]"+showski Scase = "[CASEOF]"+showski Sunit = "[UNIT]"+showski Sabort = "[ABORT]"+showski Sabsurd = "[ABSURD]" -- | SKI abstraction of a named lambda term. From a lambda expression -- creates a SKI equivalent expression. The following algorithm is a -- version of the algorithm 9.10 on the Hindley-Seldin book. skiabs :: NamedLambda -> Ski-skiabs (LambdaVariable x) = Cte x+skiabs (LambdaVariable x) = Cte x skiabs (LambdaApplication m n) = Comb (skiabs m) (skiabs n) skiabs (LambdaAbstraction x m) = bracketabs x (skiabs m) skiabs (TypedPair a b) = Comb (Comb Spair (skiabs a)) (skiabs b)@@ -68,7 +68,7 @@ skiabs (TypedInl a) = Comb Sinl (skiabs a) skiabs (TypedInr a) = Comb Sinr (skiabs a) skiabs (TypedCase a b c) = Comb (Comb (Comb Scase (skiabs a)) (skiabs b)) (skiabs c)-skiabs (TypedUnit) = Sunit+skiabs TypedUnit = Sunit skiabs (TypedAbort a) = Comb Sabort (skiabs a) skiabs (TypedAbsurd a) = Comb Sabsurd (skiabs a) @@ -82,9 +82,9 @@ | freein x u = Comb K (Comb u (Cte y)) | otherwise = Comb (Comb S (bracketabs x u)) (bracketabs x (Cte y)) bracketabs x (Comb u v)- | freein x (Comb u v) = Comb K (Comb u v)- | otherwise = Comb (Comb S (bracketabs x u)) (bracketabs x v)-bracketabs _ a = Comb K a+ | freein x (Comb u v) = Comb K (Comb u v)+ | otherwise = Comb (Comb S (bracketabs x u)) (bracketabs x v)+bracketabs _ a = Comb K a -- | Checks if a given variable is used on a SKI expression. freein :: String -> Ski -> Bool
+ source/Stlc/Block.hs view
@@ -0,0 +1,87 @@+module Stlc.Block+ ( Block+ , textBlock+ , deductionBlock+ , box+ )+where ++import Data.Monoid++newtype Block = Block { getBlock :: [String] }+ deriving (Eq, Ord)++instance Monoid Block where+ mappend = joinBlocks+ mempty = Block [[]]++instance Show Block where+ show = unlines . getBlock+++hsepChar :: Char+hsepChar = '─'++spaceChar :: Char+spaceChar = ' '++height :: Block -> Int+height = length . getBlock++width :: Block -> Int+width (Block []) = 0+width (Block (x:_)) = length x++-- | Horizontal join+joinBlocks :: Block -> Block -> Block+joinBlocks u@(Block a) v@(Block b) = Block $ zipWith (++) us vs+ where+ us = replicate (mh - uh) (replicate uw spaceChar) ++ a+ vs = replicate (mh - vh) (replicate vw spaceChar) ++ b+ uh = height u+ vh = height v+ mh = max uh vh+ uw = width u+ vw = width v++-- | Vertical join+stackBlocks :: String -> Block -> Block -> Block+stackBlocks label u v = Block $ getBlock ut ++ [hline] ++ getBlock vt+ where+ mw = max (width u) (width v)+ us = centerBlock mw u+ vs = centerBlock mw v+ hline = replicate mw hsepChar ++ label+ ut = us <> Block [replicate (length label) ' ']+ vt = vs <> Block [replicate (length label) ' ']+++centerBlock :: Int -> Block -> Block+centerBlock n = Block . map (centerString n) . getBlock++centerString :: Int -> String -> String+centerString n s = centered+ where+ w = length s+ diff = n - w+ semicentered = replicate (diff `div` 2 + diff `mod` 2) ' ' ++ s+ centered = take n (semicentered ++ repeat ' ')++-- | Inserts a text into a text block+textBlock :: String -> Block+textBlock s = Block [centerString (length s) s]++-- | Draws a logical inference in a text block+deductionBlock :: Block -> String -> [Block] -> Block+deductionBlock inference label blocks = stackBlocks label top inference+ where+ top = if not (null blocks)+ then foldr1 (\x y -> x <> Block [" "] <> y) blocks+ else Block [""]++-- | Draws a box around a text block+box :: Block -> Block+box c@(Block cm) = Block $+ ["╭" ++ replicate (width c) '─' ++ "╮"] +++ map (" " ++) cm +++ ["╰" ++ replicate (width c) '─' ++ "╯"]
+ source/Stlc/Gentzen.hs view
@@ -0,0 +1,188 @@+module Stlc.Gentzen+ ( gentzendiagram+ , showProofTree+ )+where++import Stlc.Types+import Stlc.Block+import Lambda+import NamedLambda+import Data.Bifunctor+import qualified Data.Map as Map+++data ProofTree a l = Inference a | Deduction a l [ProofTree a l]++instance Bifunctor ProofTree where+ bimap f _ (Inference a) = Inference (f a)+ bimap f g (Deduction a l ps) = Deduction (f a) (g l) (map (bimap f g) ps)++proofBlock :: ProofTree String String -> Block+proofBlock (Inference x) = textBlock x+proofBlock (Deduction x l xs) = deductionBlock (textBlock x) l (map proofBlock xs)++-- | Draws a complete derivation tree+showProofTree :: ProofTree String String -> String+showProofTree = show . box . proofBlock+++data Label = Lponens | Labs | Lpair | Lpi1 | Lpi2+ | Linr | Linl | Lcase | Lunit | Labort | Labsurd+ +instance Show Label where+ show Lponens = "(→)"+ show Labs = "(λ)"+ show Lpair = "(,)"+ show Lpi1 = "(π₁)"+ show Lpi2 = "(π₂)"+ show Linl = "(ιnl)"+ show Linr = "(ιnr)"+ show Lcase = "(Case)"+ show Lunit = "(★)"+ show Labort = "(□)"+ show Labsurd = "(■)"++type Depth = Int+type TermDiagram = (Exp,Depth,Type)+++-- | Gets a type derivation diagram of the term.+-- It fails if the term is non-typeable.+gentzendiagram :: Exp -> Maybe (ProofTree String String)+gentzendiagram l = do+ (_, d) <- typeinfer' variables 0 emptyctx l (Tvar 0)+ maintype <- typeinfer variables emptyctx l (Tvar 0) <*> pure (Tvar 0)+ let (normtemplate, _) = normalizeTemplate Map.empty 0 maintype+ return (bimap (showTermDiagram normtemplate) show d)+ where+ showTermDiagram normtemplate (expl, depth, t) =+ show (quicknameIndexes depth variableNames expl) +++ " ∷ " +++ show (applynormalization normtemplate t)++-- | Type inference algorithm. Infers a type from a given context and expression+-- with a set of constraints represented by a unifier type. The result type must+-- be unifiable with this given type.+-- Generalized version.+typeinfer' :: [Variable] -- ^ List of fresh variables+ -> Depth -- ^ Lambda abstraction depth+ -> Context -- ^ Type context+ -> Exp -- ^ Lambda expression whose type has to be inferred+ -> Type -- ^ Constraint+ -> Maybe (Substitution, ProofTree TermDiagram Label)+ +typeinfer' [] _ _ _ _ = Nothing+typeinfer' [_] _ _ _ _ = Nothing++typeinfer' _ depth ctx l@(Var n) b+ | Map.member n ctx = do+ var <- Map.lookup n ctx+ ss <- unify var b+ return (ss, Inference (l, depth, ss b))+ | otherwise = Nothing++typeinfer' (x:vars) depth ctx l@(App p q) b = do+ (sigma, d1) <- typeinfer' (evens vars) depth ctx p (Arrow (Tvar x) b)+ (tau, d2) <- typeinfer' (odds vars) depth (applyctx sigma ctx) q (sigma (Tvar x))+ let ss = tau . sigma+ let fulld1 = bimap (\(d1e,d1d,d1t) -> (d1e,d1d,tau d1t)) id d1+ return (ss, Deduction (l, depth, ss b) Lponens [fulld1,d2])+ where+ odds [] = []+ odds [_] = []+ odds (_:e:xs) = e : odds xs+ evens [] = []+ evens [e] = [e]+ evens (e:_:xs) = e : evens xs+++typeinfer' (a:x:vars) depth ctx l@(Lambda p) b = do+ sigma <- unify b (Arrow (Tvar a) (Tvar x))+ let nctx = applyctx sigma (Map.insert 1 (sigma $ Tvar a) (incrementindices ctx))+ (tau, d2) <- typeinfer' vars (succ depth) nctx p (sigma $ Tvar x)+ let ss = tau . sigma+ return (ss, Deduction (l, depth, ss b) Labs [d2])++typeinfer' (x:y:vars) depth ctx l@(Pair m n) a = do+ sigma <- unify a (Times (Tvar x) (Tvar y))+ (tau, d1) <- typeinfer' (evens vars) depth (applyctx sigma ctx) m (sigma (Tvar x))+ (rho, d2) <- typeinfer' (odds vars) depth (applyctx (tau . sigma) ctx) n (tau (sigma (Tvar y)))+ let ss = rho . tau . sigma+ let fulld1 = bimap (\(d1e,d1d,d1t) -> (d1e,d1d,rho d1t)) id d1+ return (ss, Deduction (l, depth, ss a) Lpair [fulld1,d2])+ where+ odds [] = []+ odds [_] = []+ odds (_:e:xs) = e : odds xs+ evens [] = []+ evens [e] = [e]+ evens (e:_:xs) = e : evens xs+++typeinfer' (y:vars) depth ctx l@(Pi1 m) a = do+ (sigma, d1) <- typeinfer' vars depth ctx m (Times a (Tvar y))+ let ss = sigma+ return (ss, Deduction (l, depth, ss a) Lpi1 [d1])+ +typeinfer' (x:vars) depth ctx l@(Pi2 m) b = do+ (sigma, d1) <- typeinfer' vars depth ctx m (Times (Tvar x) b)+ let ss = sigma+ return (ss, Deduction (l, depth, ss b) Lpi2 [d1])++typeinfer' (x:y:vars) depth ctx l@(Inl m) a = do+ sigma <- unify a (Union (Tvar x) (Tvar y))+ (tau, d1) <- typeinfer' vars depth (applyctx sigma ctx) m (sigma (Tvar x))+ let ss = tau . sigma+ return (ss, Deduction (l, depth, ss a) Linl [d1])++typeinfer' (x:y:vars) depth ctx l@(Inr m) a = do+ sigma <- unify a (Union (Tvar x) (Tvar y))+ (tau, d1) <- typeinfer' vars depth (applyctx sigma ctx) m (sigma (Tvar y))+ let ss = tau . sigma+ return (ss, Deduction (l, depth, ss a) Linr [d1])++typeinfer' (x:y:vars) depth ctx l@(Caseof m f g) a = do+ (sigma, d1) <- typeinfer' (third1 vars) depth ctx f (Arrow (Tvar x) a)+ (tau, d2) <- typeinfer' (third2 vars) depth (applyctx sigma ctx) g (Arrow (sigma $ Tvar y) (sigma a))+ (rho, d3) <- typeinfer' (third3 vars) depth (applyctx (tau . sigma) ctx) m (Union (tau . sigma $ Tvar x) (tau . sigma $ Tvar y))+ let ss = rho . tau . sigma+ let fulld1 = bimap (\(d1e,d1d,d1t) -> (d1e,d1d,(rho . tau) d1t)) id d1+ let fulld2 = bimap (\(d2e,d2d,d2t) -> (d2e,d2d,rho d2t)) id d2+ -- Pruning the tree to make it match the natural deduction case rule+ case fulld1 of+ Deduction _ Labs [reald1] ->+ case fulld2 of+ Deduction _ Labs [reald2] -> return (ss, Deduction (l, depth, ss a) Lcase [reald1,reald2,d3])+ _ -> Nothing+ _ -> Nothing+ + where+ third1 [] = []+ third1 [_] = []+ third1 [_,_] = []+ third1 (_:_:e:xs) = e : third1 xs+ third2 [] = []+ third2 [_] = []+ third2 [_,e] = [e]+ third2 (_:e:_:xs) = e : third2 xs+ third3 [] = []+ third3 [e] = [e]+ third3 [e,_] = [e]+ third3 (e:_:_:xs) = e : third3 xs++typeinfer' _ depth _ l@Unit a = do+ ss <- unify Unitty a+ return (ss, Deduction (l, depth, ss a) Lunit [])++typeinfer' vars depth ctx l@(Abort m) a = do+ (ss, d1) <- typeinfer' vars depth ctx m Bottom+ return (ss, Deduction (l, depth, ss a) Labort [d1])++typeinfer' vars depth ctx l@(Absurd m) a = do+ sigma <- unify Bottom a+ (tau, d1) <- typeinfer' vars depth (applyctx sigma ctx) m Bottom+ let ss = tau . sigma+ return (ss, Deduction (l, depth, ss a) Labsurd [d1])++
+ source/Stlc/Types.hs view
@@ -0,0 +1,275 @@+module Stlc.Types+ ( Type (Tvar, Arrow, Times, Union, Unitty, Bottom)+ , typeinference+ , typeinfer+ , unify+ , applyctx+ , emptyctx+ , incrementindices+ , variables+ , normalizeTemplate+ , applynormalization+ , Top (Top)+ , Context+ , Variable+ , Substitution+ )+where++import Control.Monad+import Lambda++import qualified Data.Map as Map++-- | 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++-- | A type variable is an integer.+type Variable = Integer++-- | A type substitution is a function that can be applied to any type+-- to get a new one.+type Substitution = Type -> Type++-- | 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+ deriving (Eq)++instance Show Type where+ 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 = "⊥"++showparens :: Type -> String+showparens (Tvar t) = show (Tvar t)+showparens Unitty = show Unitty+showparens Bottom = show Bottom+showparens m = "(" ++ show m ++ ")"+ +-- | Creates the substitution given by the change of a variable for+-- the given type.+subs :: Variable -> Type -> Substitution+subs x typ (Tvar y)+ | x == y = typ+ | otherwise = Tvar y+subs x typ (Arrow a b) = Arrow (subs x typ a) (subs x typ b)+subs x typ (Times a b) = Times (subs x typ a) (subs x typ b)+subs x typ (Union a b) = Union (subs x typ a) (subs x typ b)+subs _ _ Unitty = Unitty+subs _ _ Bottom = Bottom++-- | Returns true if the given variable appears on the type.+occurs :: Variable -> Type -> Bool+occurs x (Tvar y) = x == y+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 _ Bottom = False++-- | Unifies two types with their most general unifier. Returns the substitution+-- that transforms any of the types into the unifier.+unify :: Type -> Type -> Maybe Substitution+unify (Tvar x) (Tvar y)+ | x == y = Just id+ | otherwise = Just (subs x (Tvar y))+unify (Tvar x) b+ | occurs x b = Nothing+ | otherwise = Just (subs x b)+unify a (Tvar y)+ | occurs y a = Nothing+ | otherwise = Just (subs y a)+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++-- | The empty context.+emptyctx :: Context+emptyctx = Map.empty++-- | Increments all the indices of a given context. It is useful for+-- adapting the context to a new scope.+incrementindices :: Context -> Context+incrementindices = Map.mapKeys succ++-- | Type inference algorithm. Infers a type from a given context and expression+-- with a set of constraints represented by a unifier type. The result type must+-- be unifiable with this given type.+typeinfer :: [Variable] -- ^ List of fresh variables+ -> Context -- ^ Type context+ -> Exp -- ^ Lambda expression whose type has to be inferred+ -> Type -- ^ Constraint+ -> Maybe Substitution+ +typeinfer [] _ _ _ = Nothing+typeinfer [_] _ _ _ = Nothing++typeinfer _ ctx (Var n) b+ | Map.member n ctx = do+ var <- Map.lookup n ctx+ unify var b+ | otherwise = Nothing++typeinfer (x:vars) ctx (App p q) b = do+ sigma <- typeinfer (evens vars) ctx p (Arrow (Tvar x) b)+ tau <- typeinfer (odds vars) (applyctx sigma ctx) q (sigma (Tvar x))+ return (tau . sigma)+ where+ odds [] = []+ odds [_] = []+ odds (_:e:xs) = e : odds xs+ evens [] = []+ evens [e] = [e]+ evens (e:_:xs) = e : evens xs+++typeinfer (a:x:vars) ctx (Lambda p) b = do+ sigma <- unify b (Arrow (Tvar a) (Tvar x))+ let nctx = applyctx sigma (Map.insert 1 (sigma $ Tvar a) (incrementindices ctx))+ tau <- typeinfer vars nctx p (sigma $ Tvar x)+ return (tau . sigma)++typeinfer (x:y:vars) ctx (Pair m n) a = do+ sigma <- unify a (Times (Tvar x) (Tvar y))+ tau <- typeinfer (evens vars) (applyctx sigma ctx) m (sigma (Tvar x))+ rho <- typeinfer (odds vars) (applyctx (tau . sigma) ctx) n (tau (sigma (Tvar y)))+ return (rho . tau . sigma)+ where+ odds [] = []+ odds [_] = []+ odds (_:e:xs) = e : odds xs+ evens [] = []+ evens [e] = [e]+ evens (e:_:xs) = e : evens xs+++typeinfer (y:vars) ctx (Pi1 m) a = typeinfer vars ctx m (Times a (Tvar y))+typeinfer (x:vars) ctx (Pi2 m) b = typeinfer vars ctx m (Times (Tvar x) b)++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))+ 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))+ return (tau . sigma)++typeinfer (x:y:vars) ctx (Caseof m f g) a = do+ sigma <- typeinfer (third1 vars) ctx f (Arrow (Tvar x) a)+ tau <- typeinfer (third2 vars) (applyctx sigma ctx) g (Arrow (sigma $ Tvar y) (sigma a))+ rho <- typeinfer (third3 vars) (applyctx (tau . sigma) ctx) m (Union (tau . sigma $ Tvar x) (tau . sigma $ Tvar y))+ return (rho . tau . sigma)+ where+ third1 [] = []+ third1 [_] = []+ third1 [_,_] = []+ third1 (_:_:e:xs) = e : third1 xs+ third2 [] = []+ third2 [_] = []+ third2 [_,e] = [e]+ third2 (_:e:_:xs) = e : third2 xs+ third3 [] = []+ third3 [e] = [e]+ third3 [e,_] = [e]+ third3 (e:_:_:xs) = e : third3 xs++typeinfer _ _ Unit a = unify Unitty a++typeinfer vars ctx (Abort m) _ = typeinfer vars ctx m Bottom++typeinfer vars ctx (Absurd m) a = do+ sigma <- unify Bottom a+ tau <- typeinfer vars (applyctx sigma ctx) m Bottom+ return (tau . sigma)+ ++-- | Type inference of a lambda expression.+typeinference :: Exp -> Maybe Type+typeinference e = normalize <$> (typeinfer variables emptyctx e (Tvar 0) <*> pure (Tvar 0))++-- | List of possible variable names.+typevariableNames :: [String]+typevariableNames = concatMap (`replicateM` ['A'..'Z']) [1..]++-- | Infinite list of variables.+variables :: [Variable]+variables = [1..]+++-- | Substitutes a set of type variables on a type template for the smaller+-- possible ones.+normalizeTemplate :: Map.Map Integer Integer -> Integer -> Type -> (Map.Map Integer Integer, Integer)+normalizeTemplate sub n (Tvar m) = case Map.lookup m sub of+ Just _ -> (sub, n)+ Nothing -> (Map.insert m n sub, succ n)+normalizeTemplate sub n (Arrow a b) =+ let (nsub, nn) = normalizeTemplate sub n a in normalizeTemplate nsub nn b+normalizeTemplate sub n (Times a b) =+ let (nsub, nn) = normalizeTemplate sub n a in normalizeTemplate nsub nn b+normalizeTemplate sub n (Union a b) =+ let (nsub, nn) = normalizeTemplate sub n a in normalizeTemplate nsub nn b+normalizeTemplate sub n Unitty = (sub, n)+normalizeTemplate sub n Bottom = (sub, n)++-- | 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+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)+applynormalization _ Unitty = Unitty+applynormalization _ Bottom = Bottom++++-- | Normalizes a type, that is, substitutes the set of type variables for+-- 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) ++ ")"
− source/Types.hs
@@ -1,268 +0,0 @@-module Types- ( Type (Tvar, Arrow, Times, Union, Unitty, Bottom)- , typeinference- , Top (Top)- )-where--import Control.Monad-import Lambda--import qualified Data.Map as Map---- | 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---- | A type variable is an integer.-type Variable = Integer---- | A type substitution is a function that can be applied to any type--- to get a new one.-type Substitution = Type -> Type---- | 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- deriving (Eq)--instance Show Type where- 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) = "⊥"--showparens :: Type -> String-showparens (Tvar t) = show (Tvar t)-showparens Unitty = show Unitty-showparens Bottom = show Bottom-showparens m = "(" ++ show m ++ ")"- --- | Creates the substitution given by the change of a variable for--- the given type.-subs :: Variable -> Type -> Substitution-subs x typ (Tvar y)- | x == y = typ- | otherwise = Tvar y-subs x typ (Arrow a b) = Arrow (subs x typ a) (subs x typ b)-subs x typ (Times a b) = Times (subs x typ a) (subs x typ b)-subs x typ (Union a b) = Union (subs x typ a) (subs x typ b)-subs _ _ Unitty = Unitty-subs _ _ Bottom = Bottom---- | Returns true if the given variable appears on the type.-occurs :: Variable -> Type -> Bool-occurs x (Tvar y) = x == y-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 _ (Bottom) = False---- | Unifies two types with their most general unifier. Returns the substitution--- that transforms any of the types into the unifier.-unify :: Type -> Type -> Maybe Substitution-unify (Tvar x) (Tvar y)- | x == y = Just id- | otherwise = Just (subs x (Tvar y))-unify (Tvar x) b- | occurs x b = Nothing- | otherwise = Just (subs x b)-unify a (Tvar y)- | occurs y a = Nothing- | otherwise = Just (subs y a)-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---- | The empty context.-emptyctx :: Context-emptyctx = Map.empty---- | Increments all the indices of a given context. It is useful for--- adapting the context to a new scope.-incrementindices :: Context -> Context-incrementindices = Map.mapKeys succ---- | Type inference algorithm. Infers a type from a given context and expression--- with a set of constraints represented by a unifier type. The result type must--- be unifiable with this given type.-typeinfer :: [Variable] -- ^ List of fresh variables- -> Context -- ^ Type context- -> Exp -- ^ Lambda expression whose type has to be inferred- -> Type -- ^ Constraint- -> Maybe Substitution- -typeinfer [] _ _ _ = Nothing-typeinfer [_] _ _ _ = Nothing--typeinfer _ ctx (Var n) b- | Map.member n ctx = do- var <- Map.lookup n ctx- unify var b- | otherwise = Nothing--typeinfer (x:vars) ctx (App p q) b = do- sigma <- typeinfer (evens vars) ctx p (Arrow (Tvar x) b)- tau <- typeinfer (odds vars) (applyctx sigma ctx) q (sigma (Tvar x))- return (tau . sigma)- where- odds [] = []- odds [_] = []- odds (_:e:xs) = e : odds xs- evens [] = []- evens [e] = [e]- evens (e:_:xs) = e : evens xs---typeinfer (a:x:vars) ctx (Lambda p) b = do- sigma <- unify b (Arrow (Tvar a) (Tvar x))- let nctx = applyctx sigma (Map.insert 1 (sigma $ Tvar a) (incrementindices ctx))- tau <- typeinfer vars nctx p (sigma $ Tvar x)- return (tau . sigma)--typeinfer (x:y:vars) ctx (Pair m n) a = do- sigma <- unify a (Times (Tvar x) (Tvar y))- tau <- typeinfer (evens vars) (applyctx sigma ctx) m (sigma (Tvar x))- rho <- typeinfer (odds vars) (applyctx (tau . sigma) ctx) n (tau (sigma (Tvar y)))- return (rho . tau . sigma)- where- odds [] = []- odds [_] = []- odds (_:e:xs) = e : odds xs- evens [] = []- evens [e] = [e]- evens (e:_:xs) = e : evens xs---typeinfer (y:vars) ctx (Pi1 m) a = typeinfer vars ctx m (Times a (Tvar y))-typeinfer (x:vars) ctx (Pi2 m) b = typeinfer vars ctx m (Times (Tvar x) b)--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))- 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))- return (tau . sigma)--typeinfer (x:y:vars) ctx (Caseof m f g) a = do- sigma <- typeinfer (third1 vars) ctx f (Arrow (Tvar x) a)- tau <- typeinfer (third2 vars) (applyctx sigma ctx) g (Arrow (sigma $ Tvar y) (sigma a))- rho <- typeinfer (third3 vars) (applyctx (tau . sigma) ctx) m (Union (tau . sigma $ Tvar x) (tau . sigma $ Tvar y))- return (rho . tau . sigma)- where- third1 [] = []- third1 [_] = []- third1 [_,_] = []- third1 (_:_:e:xs) = e : third1 xs- third2 [] = []- third2 [_] = []- third2 [_,e] = [e]- third2 (_:e:_:xs) = e : third2 xs- third3 [] = []- third3 [e] = [e]- third3 [e,_] = [e]- third3 (e:_:_:xs) = e : third3 xs--typeinfer _ _ Unit a = unify Unitty a--typeinfer vars ctx (Abort m) _ = typeinfer vars ctx m Bottom--typeinfer vars ctx (Absurd m) a = do- sigma <- unify Bottom a- tau <- typeinfer vars (applyctx sigma ctx) m Bottom- return (tau . sigma)- ---- | Type inference of a lambda expression.-typeinference :: Exp -> Maybe Type-typeinference e = normalize <$> (typeinfer variables emptyctx e (Tvar 0) <*> pure (Tvar 0))---- | List of possible variable names.-typevariableNames :: [String]-typevariableNames = concatMap (`replicateM` ['A'..'Z']) [1..]---- | Infinite list of variables.-variables :: [Variable]-variables = [1..]----- | Substitutes a set of type variables on a type template for the smaller--- possible ones.-normalizeTemplate :: Map.Map Integer Integer -> Integer -> Type -> (Map.Map Integer Integer, Integer)-normalizeTemplate sub n (Tvar m) = case Map.lookup m sub of- Just _ -> (sub, n)- Nothing -> (Map.insert m n sub, succ n)-normalizeTemplate sub n (Arrow a b) =- let (nsub, nn) = normalizeTemplate sub n a in normalizeTemplate nsub nn b-normalizeTemplate sub n (Times a b) =- let (nsub, nn) = normalizeTemplate sub n a in normalizeTemplate nsub nn b-normalizeTemplate sub n (Union a b) =- let (nsub, nn) = normalizeTemplate sub n a in normalizeTemplate nsub nn b-normalizeTemplate sub n Unitty = (sub, n)-normalizeTemplate sub n Bottom = (sub, n)---- | 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-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)-applynormalization _ Unitty = Unitty-applynormalization _ Bottom = Bottom------ | Normalizes a type, that is, substitutes the set of type variables for--- 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) ++ ")"
− std.mkr
@@ -1,192 +0,0 @@-## Standard library ##--# This is the standard library for the Mikrokosmos untyped lambda calculus-# interpreter. It contains basic logic and arithmetic operations.-# You can read more about Church encoding in its wikipedia page:-# https://en.wikipedia.org/wiki/Church_encoding-#-# This library is licensed under CC0.-----## Logic-# Uses Church Booleans-true = \a.\b.a-false = \a.\b.b--# Basic logic gates-and = \p.\q.p q p-or = \p.\q.p p q-not = \b.b false true--# Conditional-ifelse = (\x.x)-----## Arithmethic-# This library uses Church numerals to represent natural numbers-# Succesor of a natural number is defined with 0-succ = \n.\f.\x.f (n f x)-0 = \f.\x.x--# Basic operations on natural numbers-plus = \m.\n.\f.\x.m f (n f x)-mult = \m.\n.\f.\x.m (n f) x--# Substraction-pred = \n.\f.\x.n (\g.(\h.h (g f))) (\u.x) (\u.u)-minus = \m.\n.(n pred) m--# Predicates on natural numbers-iszero = \n.(n (\x.false) true)-leq = \m.\n.(iszero (minus m n))-eq = \m.\n.(and (leq m n) (leq n m))-----## Data structures-# Pairs-pair = \x.\y.\z.z x y-first = \p.p true-second = \p.p false--# Lists-# Uses the right-fold representation of lists.-# The representation of a list is its foldr function.-cons = \h.\t.\c.\n.(c h (t c n))-nil = \c.\n.n--# Folds-foldr = \o.\n.\l.(l o n)-sum = (foldr plus 0)-prod = (foldr mult (succ 0))-length = (foldr (\h.\t.succ t) 0)--# Map-# Writes map as a foldr.-map = (\f.(foldr (\h.\t.cons (f h) t) nil))-filter = \p.(foldr (\h.\t.((p h) (cons h t) t)) nil)--# Trees-# Uses the fold representation of a binary tree-# Its nil is the same one as the list representation-node = \x.\l.\r.\f.\n.(f x (l f n) (r f n))-----## Fixpoint operator and recursion-fix != (\f.(\x.f (x x)) (\x.f (x x)))-fact != fix (\f.\n.iszero n (succ 0) (mult n (f (pred n))))-fib != fix (\f.\n.iszero n (succ 0) (plus (f (pred n)) (f (pred (pred n)))))-----## APPENDIX-## Natural numbers-# List of 100 first natural numbers-1 = succ 0-2 = succ 1-3 = succ 2-4 = succ 3-5 = succ 4-6 = succ 5-7 = succ 6-8 = succ 7-9 = succ 8-10 = succ 9-11 = succ 10-12 = succ 11-13 = succ 12-14 = succ 13-15 = succ 14-16 = succ 15-17 = succ 16-18 = succ 17-19 = succ 18-20 = succ 19-21 = succ 20-22 = succ 21-23 = succ 22-24 = succ 23-25 = succ 24-26 = succ 25-27 = succ 26-28 = succ 27-29 = succ 28-30 = succ 29-31 = succ 30-32 = succ 31-33 = succ 32-34 = succ 33-35 = succ 34-36 = succ 35-37 = succ 36-38 = succ 37-39 = succ 38-40 = succ 39-41 = succ 40-42 = succ 41-43 = succ 42-44 = succ 43-45 = succ 44-46 = succ 45-47 = succ 46-48 = succ 47-49 = succ 48-50 = succ 49-51 = succ 50-52 = succ 51-53 = succ 52-54 = succ 53-55 = succ 54-56 = succ 55-57 = succ 56-58 = succ 57-59 = succ 58-60 = succ 59-61 = succ 60-62 = succ 61-63 = succ 62-64 = succ 63-65 = succ 64-66 = succ 65-67 = succ 66-68 = succ 67-69 = succ 68-70 = succ 69-71 = succ 70-72 = succ 71-73 = succ 72-74 = succ 73-75 = succ 74-76 = succ 75-77 = succ 76-78 = succ 77-79 = succ 78-80 = succ 79-81 = succ 80-82 = succ 81-83 = succ 82-84 = succ 83-85 = succ 84-86 = succ 85-87 = succ 86-88 = succ 87-89 = succ 88-90 = succ 89-91 = succ 90-92 = succ 91-93 = succ 92-94 = succ 93-95 = succ 94-96 = succ 95-97 = succ 96-98 = succ 97-99 = succ 98-100 = succ 99
tests/test.hs view
@@ -1,13 +1,16 @@ import Test.Tasty import Test.Tasty.HUnit import Test.Tasty.QuickCheck as QC+import Test.Tasty.Golden as TG+import System.Process import Text.ParserCombinators.Parsec import NamedLambda import Lambda-import Types+import Stlc.Types import Ski import Environment+import Interpreter main :: IO ()@@ -19,6 +22,8 @@ , typeinferTests , skiabsTests , lambdaProps+ , parserProps+ , goldenTests ] -- Unit tests@@ -53,7 +58,7 @@ 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)))))))))+ 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) ]@@ -75,31 +80,23 @@ ] --- Lambda properties++-- Quickcheck 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+ [ QC.testProperty "Expression -> named -> expression" $+ \expr -> toBruijn emptyContext (nameExp expr) == expr+ , QC.testProperty "Open expressions are not allowed" $+ \expr -> not (isOpenExp expr) ]- --- 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)--- ]+parserProps :: TestTree+parserProps = testGroup "Parser properties (quickcheck)"+ [ QC.testProperty "Comments are ignored" $+ \str -> case parse interpreteractionParser "" ("#" ++ str) of+ Right (Interpret Comment) -> True+ _ -> False+ ] -- Arbitrary typed lambda expressions@@ -109,7 +106,7 @@ 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 0 = Var <$> (toInteger <$> choose (1, lim)) lambda lim size = oneof [ Var <$> (toInteger <$> choose (1, lim)) , Lambda <$> lambda (succ lim) (size-1)@@ -129,3 +126,14 @@ , Abort <$> lambda lim (size-1) , Absurd <$> lambda lim (size-1) ]+++-- Golden test+goldenTests :: TestTree+goldenTests = testGroup "Golden tests (tasty-golden)"+ [ goldenVsFile "Main golden test"+ "tests/goldenfile.golden"+ "tests/testingfile"+ (callCommand "mikrokosmos tests/testing.mkr > tests/testingfile")+ ]+