Add transformation of nameless to named term and generator for nameless terms

Author: nigosto

src/Generator.hs

@@ -14,4 +14,4 @@ generateNamelessTerm (NamelessVariable var) = show var
 generateNamelessTerm (NamelessApplication lhs rhs) = concatMap (\term -> case term of
   var@(NamelessVariable _) -> generateNamelessTerm var
   _ -> '(':generateNamelessTerm term ++ [')']) [lhs, rhs]
-generateNamelessTerm (NamelessAbstraction depth body) = 'λ':generateNamelessTerm body
+generateNamelessTerm (NamelessAbstraction body) = 'λ':generateNamelessTerm body

src/Main.hs

@@ -1,31 +1,31 @@
 module Main where
 
-import Prelude hiding (lookup)
-import System.IO (hSetBuffering, stdout, BufferMode (BlockBuffering))
-import Parser (parseTerm, Term (Variable))
-import Substitution.Named (substitute)
-import Generator (generateTerm, generateNamelessTerm)
-import Transformer (toNameless)
 import Data.Map (empty, lookup)
+import Generator (generateNamelessTerm, generateTerm)
+import Parser (Term (Variable), parseTerm)
+import Substitution.Named (substitute)
 import Substitution.Nameless (substituteNameless)
+import System.IO (BufferMode (BlockBuffering), hSetBuffering, stdout)
+import Transformer (toNamed, toNameless)
+import Prelude hiding (lookup)
 
 main :: IO ()
 main = do
   hSetBuffering stdout $ BlockBuffering $ Just 1
   term <- putStr "Input term: " >> getLine
   var <- putStr "Input variable to substitute: " >> getLine -- not using getChr intentionally
-  if length var /= 1 
-  then error "please provide valid variable"
-  else do
-    let (namelessTerm, context) = toNameless (parseTerm term) 0 [] empty
-        substituteVariable = head var `lookup` context 
-    case substituteVariable of
-      Nothing -> error "please provide valid variable"
-      Just index -> do 
-        substituteTerm <- putStr "Input substitution term: " >> getLine
-        let (substituteNamelessTerm, _) = toNameless (parseTerm substituteTerm) 0 [] context
-        putStrLn $ generateNamelessTerm $ substituteNameless namelessTerm index substituteNamelessTerm
+  if length var /= 1
+    then error "please provide valid variable"
+    else do
+      let (namelessTerm, context) = toNameless $ parseTerm term
+          substituteVariable = head var `lookup` context
+      substituteTerm <- putStr "Input substitution term: " >> getLine
+      case substituteVariable of
+        Nothing -> putStrLn term
+        Just index ->
+          let (substituteNamelessTerm, updatedContext) = toNameless $ parseTerm substituteTerm
+           in putStrLn $ generateTerm $ toNamed (substituteNameless namelessTerm index substituteNamelessTerm) updatedContext
 
-    -- let substituteVariable = head var
-    -- substituteTerm <- putStr "Input substitution term: " >> getLine
-    -- putStrLn $ generateTerm $ substitute (parseTerm term) substituteVariable (parseTerm substituteTerm)
+-- let substituteVariable = head var
+-- substituteTerm <- putStr "Input substitution term: " >> getLine
+-- putStrLn $ generateTerm $ substitute (parseTerm term) substituteVariable (parseTerm substituteTerm)

src/Substitution/Nameless.hs

@@ -6,7 +6,7 @@ shift c d var@(NamelessVariable k)
     | 0 <= k && k < c = var
     | otherwise = NamelessVariable (k + d)
 shift c d (NamelessApplication lhs rhs) = NamelessApplication (shift c d lhs) (shift c d rhs)
-shift c d (NamelessAbstraction depth body) = NamelessAbstraction depth (shift (c + 1) d body)
+shift c d (NamelessAbstraction body) = NamelessAbstraction $ shift (c + 1) d body
 
 singleShift :: NamelessTerm -> NamelessTerm
 singleShift = shift 0 1
@@ -17,5 +17,5 @@ substituteNameless (NamelessVariable var) x term
     | otherwise = NamelessVariable var
 substituteNameless (NamelessApplication lhs rhs) x term =
     NamelessApplication (substituteNameless lhs x term) (substituteNameless rhs x term)
-substituteNameless (NamelessAbstraction depth body) x term =
-    NamelessAbstraction depth (substituteNameless body (x + 1) (singleShift term))
+substituteNameless (NamelessAbstraction body) x term =
+    NamelessAbstraction $ substituteNameless body (x + 1) (singleShift term)

src/Transformer.hs

@@ -4,39 +4,58 @@ module Transformer where
 
 import Prelude hiding (lookup)
 import Parser (Term (Variable, Application, Abstraction))
-import Data.Map (Map, member, lookup, insert, size)
+import Data.Map (Map, member, lookup, insert, size, foldrWithKey, findMin, keys, empty)
 import Data.List (elemIndex, union)
+import Data.Char (chr, ord)
 
 data NamelessTerm
   = NamelessVariable Int
   | NamelessApplication NamelessTerm NamelessTerm
-  | NamelessAbstraction Int NamelessTerm
+  | NamelessAbstraction NamelessTerm
   deriving (Show)
 
 type NamingContext = Map Char Int
-type BoundVariable = [Char]
+type BoundVariables = [Char]
 
-toNameless :: Term -> Int -> BoundVariable -> NamingContext -> (NamelessTerm, NamingContext)
-toNameless (Variable var) depth bv context = case var `elemIndex` bv of
+toNamelessWithContext :: Term -> Int -> BoundVariables -> NamingContext -> (NamelessTerm, NamingContext)
+toNamelessWithContext (Variable var) depth bv context = case var `elemIndex` bv of
     Nothing -> case lookup var context of
         Nothing -> let index = size context
                    in (NamelessVariable (index + depth), insert var index context)
         Just index -> (NamelessVariable (index + depth), context)
     Just index -> (NamelessVariable index, context)
 
-toNameless (Application lhs rhs) depth bv context =
-    let namelessLhs = toNameless lhs depth bv context
-        namelessRhs = toNameless rhs depth bv (snd namelessLhs)
+toNamelessWithContext (Application lhs rhs) depth bv context =
+    let namelessLhs = toNamelessWithContext lhs depth bv context
+        namelessRhs = toNamelessWithContext rhs depth bv (snd namelessLhs)
     in (NamelessApplication (fst namelessLhs) (fst namelessRhs), snd namelessRhs)
 
-toNameless (Abstraction argument body) depth bv context = 
-    let namelessBody = toNameless body (depth + 1) (insertBoundVariable argument bv) context
-    in (NamelessAbstraction depth (fst namelessBody), snd namelessBody)
+toNamelessWithContext (Abstraction argument body) depth bv context =
+    let namelessBody = toNamelessWithContext body (depth + 1) (insertBoundVariable argument bv) context
+    in (NamelessAbstraction (fst namelessBody), snd namelessBody)
     where insertBoundVariable var bv = if var `elem` bv then bv else var:bv
 
--- a = Abstraction 'y' (Application (Variable 'x') (Application (Variable 'y') (Abstraction 'x' (Variable 'x'))))
--- /x -> xy => Abstraction x (Application (Variable x) (Variable y))
--- /01 => NamelessAbstraction 1 (NamelessApplication (Variable 0) (Variable 1))
-
--- /y -> xy/x -> x => /10/0
--- (NamelessAbstraction (NamelessApplication (NamelessVariable 1) (NamelessApplication (NamelessVariable 0) (NamelessAbstraction (NamelessVariable 1))))
+toNameless :: Term -> (NamelessTerm, NamingContext)
+toNameless term = toNamelessWithContext term 0 [] empty
+
+toNamedWithContext :: NamelessTerm  -> BoundVariables -> NamingContext -> Term
+toNamedWithContext (NamelessVariable var) bv context
+    | var >= length bv = Variable $ findKey (var - length bv) context
+    | otherwise = Variable (bv !! var)
+toNamedWithContext (NamelessApplication lhs rhs) bv context =
+    Application (toNamedWithContext lhs bv context) (toNamedWithContext rhs bv context)
+toNamedWithContext (NamelessAbstraction body) bv context = let updatedBoundVariables = extendBoundVariables bv
+    in Abstraction (head updatedBoundVariables) (toNamedWithContext body updatedBoundVariables context)
+    where extendBoundVariables :: BoundVariables -> BoundVariables
+          extendBoundVariables [] = if 'a' `member` context then [nextVariable 'a' context] else "a"
+          extendBoundVariables bv@(x:_) = nextVariable x context:bv
+
+toNamed :: NamelessTerm -> NamingContext -> Term
+toNamed term = toNamedWithContext term []
+
+findKey :: Eq v => v -> Map k v -> k
+findKey value map = foldrWithKey (\k v res -> if v == value then k else res) (fst $ findMin map) map
+
+nextVariable :: Char -> NamingContext -> Char
+nextVariable var context = let next = chr $ ord var + 1
+    in if next `member` context then nextVariable next context else next