content: {-|
  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..]
  