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
data NamedLambda = LambdaVariable String
| LambdaAbstraction String NamedLambda
| LambdaApplication NamedLambda NamedLambda
| TypedPair NamedLambda NamedLambda
| TypedPi1 NamedLambda
| TypedPi2 NamedLambda
| TypedInl NamedLambda
| TypedInr NamedLambda
| TypedCase NamedLambda NamedLambda NamedLambda
| TypedUnit
| TypedAbort NamedLambda
| TypedAbsurd NamedLambda
deriving (Eq)
lambdaexp :: Parser NamedLambda
lambdaexp = foldl1 LambdaApplication <$> (spaces >> sepBy1 simpleexp spaces)
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)
]
parens :: Parser a -> Parser a
parens = between (char '(') (char ')')
variableParser :: Parser NamedLambda
variableParser = LambdaVariable <$> nameParser
nameParser :: Parser String
nameParser = many1 alphaNum
choicest :: [String] -> Parser String
choicest sl = choice (try . string <$> sl)
lambdaAbstractionParser :: Parser NamedLambda
lambdaAbstractionParser = LambdaAbstraction <$>
(lambdaChar >> nameParser) <*> (char '.' >> lambdaexp)
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)
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
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 "]
tobruijn :: Map.Map String Integer
-> Context
-> NamedLambda
-> Exp
tobruijn d context (LambdaAbstraction c e) = Lambda $ tobruijn newdict context e
where newdict = Map.insert c 1 (Map.map succ d)
tobruijn d context (LambdaApplication f g) = App (tobruijn d context f) (tobruijn d context g)
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)
toBruijn :: Context
-> NamedLambda
-> Exp
toBruijn = tobruijn Map.empty
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)
nameExp :: Exp -> NamedLambda
nameExp = nameIndexes [] variableNames
variableNames :: [String]
variableNames = concatMap (`replicateM` ['a'..'z']) [1..]