mikrokosmos 0.3.0 → 0.4.0
raw patch · 7 files changed
+239/−54 lines, 7 files
Files
- README.md +1/−1
- mikrokosmos.cabal +2/−1
- source/Environment.hs +17/−12
- source/Format.hs +19/−6
- source/Interpreter.hs +39/−33
- source/Main.hs +11/−1
- source/Types.hs +150/−0
README.md view
@@ -4,7 +4,7 @@ <img src ="https://raw.githubusercontent.com/M42/mikrokosmos/master/docs/icon.svg.png" /> </p> -**Mikrokosmos** is an untyped lambda calculus interpreter, borrowing its name from the series of+**Mikrokosmos** is a λ-calculus interpreter, borrowing its name from the series of progressive piano études *[Mikrokosmos](https://www.youtube.com/watch?v=VEsMk3DAzWM)* written by *Bela Bartok*. It aims to provide students with a tool to learn and understand lambda calculus.
mikrokosmos.cabal view
@@ -1,5 +1,5 @@ name: mikrokosmos-version: 0.3.0+version: 0.4.0 synopsis: Lambda calculus interpreter description: A didactic untyped lambda calculus interpreter. homepage: https://github.com/M42/mikrokosmos@@ -44,6 +44,7 @@ Interpreter Environment Ski+ Types default-language: Haskell2010 ghc-options: -Wall
source/Environment.hs view
@@ -17,6 +17,7 @@ , getVerbose , getColor , getSki+ , getTypes , getExpressionName -- * Modifying the environment@@ -24,6 +25,7 @@ , changeColor , changeVerbose , changeSkioutput+ , changeTypes -- * Filenames and Modulenames , Filename@@ -49,6 +51,7 @@ , verbose :: Bool , color :: Bool , skioutput :: Bool+ , types :: Bool } -- | Default environment for the interpreter.@@ -59,9 +62,18 @@ , verbose = False , color = True , skioutput = False+ , types = False } +-- | Get current settings+getColor, getVerbose, getSki, getTypes :: Environment -> Bool+getColor = color+getVerbose = verbose+getSki = skioutput+getTypes = types ++ -- | Adds a name binding to the environment addBind :: Environment -> String -> Exp -> Environment addBind env s e =@@ -70,18 +82,6 @@ then env else env {context = MultiBimap.insert e s (context env)} --- | Gets the color configuration-getColor :: Environment -> Bool-getColor = color---- | Gets the verbose configuration-getVerbose :: Environment -> Bool-getVerbose = verbose---- | Gets the verbose configuration-getSki :: Environment -> Bool-getSki = skioutput- -- | Sets the verbose configuration on/off. changeVerbose :: Environment -> Bool -> Environment changeVerbose options setting = options {verbose = setting}@@ -93,6 +93,11 @@ -- | Sets the ski output configuration on/off changeSkioutput :: Environment -> Bool -> Environment changeSkioutput options setting = options {skioutput = setting}++-- | Sets the types output configuration on/off+changeTypes :: Environment -> Bool -> Environment+changeTypes options setting = options {types = setting}+ -- | Given an expression, returns its name if it is bounded to any. getExpressionName :: Environment -> Exp -> Maybe String
source/Format.hs view
@@ -18,6 +18,7 @@ , formatName , formatSubs1 , formatSubs2+ , formatType , decolor , end @@ -50,6 +51,9 @@ subst2Color :: Color subst2Color = Cyan +-- | Types are marked with this color+typeColor :: Color+typeColor = Yellow -- Format sequences -- | Sequence of characters that signals the format of a formula to the terminal.@@ -81,6 +85,11 @@ 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]++ -- | Sequence of characters that cleans all the format. end :: String end = setSGRCode []@@ -101,6 +110,7 @@ , formatFormula , formatIntro , formatName+ , formatType , formatPrompt , formatLoading , end@@ -118,11 +128,14 @@ helpText = unlines [ formatFormula ++ "Commands available from the prompt:",- "\t<expression>\t evaluates the expression",- "\t:quit \t quits the interpreter",- "\t:load <file>\t loads the given .mkr library or script",- "\t:verbose \t sets verbose mode on/off",- "\t:help \t shows this help"+ "\t<expression>\t\t evaluates the expression",+ "\t:quit \t\t quits 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",+ "\t:ski <on/off> \t\t sets ski mode on/off",+ "\t:types <on/off> \t untyped/simply typed lambda calculus",+ "\t:help \t\t shows this help" ++ end ] @@ -139,4 +152,4 @@ -- | Version version :: String-version = "0.3.0"+version = "0.4.0"
source/Interpreter.hs view
@@ -27,6 +27,7 @@ import NamedLambda import Lambda import Ski+import Types -- | Interpreter action. It can be a language action (binding and evaluation)@@ -35,10 +36,12 @@ | 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 | Help -- ^ Shows help -- | Language action. The language has a number of possible valid statements;@@ -59,9 +62,13 @@ act (EvalBind (s,le)) = do modify (\env -> addBind env s (simplifyAll $ toBruijn (context env) le)) return [""]-act (Execute le) =- do env <- get- return [unlines $+act (Execute le) = do+ env <- get+ let typed = getTypes env+ let illtyped = typed && typeinference (toBruijn (context env) le) == Nothing+ + return $ if illtyped then [formatType ++ "Error: not typeable expression" ++ end ++ "\n"] else+ [ unlines $ [ show le ] ++ [ unlines $ map showReduction $ simplifySteps $ toBruijn (context env) le ] ++ [ showCompleteExp env $ simplifyAll $ toBruijn (context env) le ] @@ -82,10 +89,17 @@ 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 -> show s+ Nothing -> "Type error!") ++ end+ else ""+ expName = case getExpressionName environment expr of+ Nothing -> ""+ Just exname -> formatName ++ " ⇒ " ++ exname ++ end in- case getExpressionName environment expr of- Nothing -> lambdaname ++ skiname- Just expName -> lambdaname ++ skiname ++ formatName ++ " ⇒ " ++ expName ++ end + lambdaname ++ skiname ++ expName ++ typename ++ end @@ -98,10 +112,12 @@ interpreteractionParser = choice [ try interpretParser , try quitParser+ , try restartParser , try loadParser , try verboseParser , try colorParser , try skiOutputParser+ , try typesParser , try helpParser ] @@ -138,40 +154,30 @@ quitParser :: Parser InterpreterAction quitParser = string ":quit" >> return Quit +-- | Parses a "restart" command.+restartParser :: Parser InterpreterAction+restartParser = string ":restart" >> return Restart+ -- | Parses a "help" command. helpParser :: Parser InterpreterAction helpParser = string ":help" >> return Help --- | Parses a change in verbosity.-verboseParser :: Parser InterpreterAction-verboseParser = choice- [ try verboseonParser- , try verboseoffParser- ]- where- verboseonParser = string ":verbose on" >> return (SetVerbose True)- verboseoffParser = string ":verbose off" >> return (SetVerbose False)---- | Parses a change in color.-colorParser :: Parser InterpreterAction-colorParser = choice- [ try coloronParser- , try coloroffParser- ]- where- coloronParser = string ":color on" >> return (SetColor True)- coloroffParser = string ":color off" >> return (SetColor False)---- | Parses a change in ski output.-skiOutputParser :: Parser InterpreterAction-skiOutputParser = choice- [ try skionParser- , try skioffParser+-- | Parses a change in a setting+settingParser :: (Bool -> InterpreterAction) -> String -> Parser InterpreterAction+settingParser setSetting settingname = choice+ [ try settingonParser+ , try settingoffParser ] where- skionParser = string ":ski on" >> return (SetSki True)- skioffParser = string ":ski off" >> return (SetSki False)+ settingonParser = string (settingname ++ " on") >> return (setSetting True)+ settingoffParser = string (settingname ++ " off") >> return (setSetting False) +-- | Multiple setting parsers+verboseParser, colorParser, skiOutputParser, typesParser :: Parser InterpreterAction+verboseParser = settingParser SetVerbose ":verbose"+colorParser = settingParser SetColor ":color"+skiOutputParser = settingParser SetSki ":ski"+typesParser = settingParser SetTypes ":types" -- | Parses a "load-file" command.
source/Main.hs view
@@ -85,6 +85,9 @@ -- Exists the interpreter Quit -> return () + -- Restarts the interpreter context+ Restart -> interpreterLoop defaultEnv+ -- Unknown command Error -> do outputStr (if getColor environment then formatFormula else "")@@ -116,7 +119,14 @@ 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)+ -- Prints the help Help -> outputStr helpText >> interpreterLoop environment
+ source/Types.hs view
@@ -0,0 +1,150 @@+module Types+ ( Type (Tvar, Arrow)+ , typeinfer+ , typeinference+ , normalize+ )+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+ deriving (Eq)++instance Show Type where+ show (Tvar t) = typevariableNames !! (fromInteger t)+ show (Arrow (Tvar x) (Tvar y)) = show (Tvar x) ++ " -> " ++ show (Tvar y)+ show (Arrow (Tvar x) b ) = show (Tvar x) ++ " -> " ++ show b+ show (Arrow a (Tvar y)) = "(" ++ show a ++ ") -> " ++ show (Tvar y)+ show (Arrow a b ) = "(" ++ show a ++ ") -> " ++ show b+++-- | 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)++-- | 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++-- | 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) = 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 [a] = [a]+ 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)+++-- | 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++-- | 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)++-- | 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