mikrokosmos-0.8.0: source/NamedLambda.hs

{-|
Module: NamedLambda
Description: Lambda expressions with named variables
License: GPL-3

This package deals with lambda expressions containing named variables
instead of DeBruijn indexes. It contains parsing and printing fuctions.
-}

module NamedLambda
  ( NamedLambda (LambdaVariable, LambdaAbstraction, LambdaApplication,
                 TypedPair, TypedPi1, TypedPi2,
                 TypedInl, TypedInr, TypedCase, TypedUnit, TypedAbort,
                 TypedAbsurd)
  , lambdaexp
  , toBruijn
  , nameExp
  , quicknameIndexes
  , variableNames
  )
where

import           Text.ParserCombinators.Parsec
import           Control.Applicative           ((<$>), (<*>))
import qualified Data.Map.Strict               as Map
import           Lambda
import           MultiBimap
import           Data.Maybe
import           Control.Monad

type Context  = MultiBimap Exp String

-- Parsing of Lambda Expressions.
-- The user can input a lambda expression with named variables, of
-- the form of "\x.x" or "(\a.(\b.a b))". The interpreter will parse
-- it into an internal representation.

-- | A lambda expression with named variables.
data NamedLambda = LambdaVariable String                         -- ^ variable
                 | LambdaAbstraction String NamedLambda          -- ^ lambda abstraction
                 | LambdaApplication NamedLambda NamedLambda     -- ^ function application
                 | TypedPair NamedLambda NamedLambda             -- ^ pair of expressions
                 | TypedPi1  NamedLambda                         -- ^ first projection
                 | TypedPi2  NamedLambda                         -- ^ second projection
                 | TypedInl  NamedLambda                         -- ^ left injection
                 | TypedInr  NamedLambda                         -- ^ right injection
                 | TypedCase NamedLambda NamedLambda NamedLambda -- ^ case of expressions
                 | 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
-- lambda expressions. They are parsed assuming left-associativity.
--
-- >>> parse lambdaexp "" "\\f.\\x.f x"
-- Right λf.λx.(f x)
--
-- Note that double backslashes are neccessary only when we quote strings;
-- it will work only with a simple backslash in the interpreter.
lambdaexp :: Parser NamedLambda
lambdaexp = foldl1 LambdaApplication <$> (spaces >> sepBy1 simpleexp spaces)

-- | Parses a simple lambda expression, without function applications
-- at the top level. It can be a lambda abstraction, a variable or another
-- potentially complex lambda expression enclosed in parentheses.
simpleexp :: Parser NamedLambda
simpleexp = choice
  [ try pairParser
  , try pi1Parser
  , try pi2Parser
  , try inlParser
  , try inrParser
  , try caseParser
  , try unitParser
  , try abortParser
  , try absurdParser
  , try lambdaAbstractionParser
  , try variableParser
  , try (parens lambdaexp)
  ]

-- | The returned parser parenthesizes the given parser
parens :: Parser a -> Parser a
parens = between (char '(') (char ')')

-- | Parses a variable. Any name can form a lambda variable.
variableParser :: Parser NamedLambda
variableParser = LambdaVariable <$> nameParser

-- | Allowed variable names
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 <$>
  (lambdaChar >> nameParser) <*> (char '.' >> lambdaexp)

-- | Char used to represent lambda in user's input.
lambdaChar :: Parser Char
lambdaChar = choice [try $ char '\\', try $ char 'λ']

pairParser :: Parser NamedLambda
pairParser = parens (TypedPair <$> lambdaexp <*> (char ',' >> lambdaexp))

pi1Parser, pi2Parser :: Parser NamedLambda
pi1Parser = TypedPi1 <$> (choicest namesPi1 >> lambdaexp)
pi2Parser = TypedPi2 <$> (choicest namesPi2 >> lambdaexp)

inlParser, inrParser :: Parser NamedLambda
inlParser = TypedInl <$> (choicest namesInl >> lambdaexp)
inrParser = TypedInr <$> (choicest namesInr >> lambdaexp)

caseParser :: Parser NamedLambda
caseParser =
  TypedCase <$>
  (choicest namesCase >> simpleexp) <*>
  (choicest namesOf >> simpleexp) <*>
  (choicest namesCaseSep >> simpleexp)

unitParser :: Parser NamedLambda
unitParser = choicest namesUnit >> return TypedUnit

abortParser :: Parser NamedLambda
abortParser = TypedAbort <$> (choicest namesAbort >> lambdaexp)

absurdParser :: Parser NamedLambda
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) =
  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
         -> Context                -- ^ dictionary of the names already binded on the scope
         -> NamedLambda            -- ^ initial expression
         -> Exp
-- Every lambda abstraction is inserted in the variable dictionary,
-- and every number in the dictionary increases to reflect we are entering
-- into a deeper context.
tobruijn d context (LambdaAbstraction c e) = Lambda $ tobruijn newdict context e
  where newdict = Map.insert c 1 (Map.map succ d)
-- Translation of applications is trivial.
tobruijn d context (LambdaApplication f g) = App (tobruijn d context f) (tobruijn d context g)
-- Every variable is checked on the variable dictionary and in the current scope.
tobruijn d context (LambdaVariable c) =
  case Map.lookup c d of
    Just n  -> Var n
    Nothing -> fromMaybe (Var 0) (MultiBimap.lookupR c context)
tobruijn d context (TypedPair a b) = Pair (tobruijn d context a) (tobruijn d context b)
tobruijn d context (TypedPi1 a) = Pi1 (tobruijn d context a)
tobruijn d context (TypedPi2 a) = Pi2 (tobruijn d context a)
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 d context (TypedAbort a) = Abort (tobruijn d context a)
tobruijn d context (TypedAbsurd a) = Absurd (tobruijn d context a)

-- | Transforms a lambda expression with named variables to a deBruijn index expression.
-- Uses only the dictionary of the variables in the current context. 
toBruijn :: Context     -- ^ Variable context
         -> NamedLambda -- ^ Initial lambda expression with named variables
         -> Exp
toBruijn = tobruijn Map.empty



-- | Translates a deBruijn expression into a lambda expression
-- with named variables, given a list of used and unused variable names.
nameIndexes :: [String] -> [String] -> Exp -> NamedLambda
nameIndexes _    _   (Var 0)        = LambdaVariable "undefined"
nameIndexes used _   (Var n)        = LambdaVariable (used !! pred (fromInteger n))
nameIndexes used new (Lambda e)     = LambdaAbstraction (head new) (nameIndexes (head new:used) (tail new) e)
nameIndexes used new (App f g)      = LambdaApplication (nameIndexes used new f) (nameIndexes used new g)
nameIndexes used new (Pair a b)     = TypedPair (nameIndexes used new a) (nameIndexes used new b)
nameIndexes used new (Pi1 a)        = TypedPi1 (nameIndexes used new a)
nameIndexes used new (Pi2 a)        = TypedPi2 (nameIndexes used new a)
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 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
-- alphabetic order.
nameExp :: Exp -> NamedLambda
nameExp = nameIndexes [] variableNames

-- | A list of all possible variable names in lexicographical order.
variableNames :: [String]
variableNames = concatMap (`replicateM` ['a'..'z']) [1..]