From 7d0d51373509e5f7fb9857a9f803dffa05523693 Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Thu, 26 Nov 2020 17:54:58 +0100
Subject: [PATCH] Display terms with correct parentheses

---
 src/Props/Lambda/Display.hs | 43 +++++++++++++++++++++++++++++++------
 src/Props/Lambda/Term.hs    | 30 ++++++++++++++++++++++++++
 2 files changed, 67 insertions(+), 6 deletions(-)

diff --git a/src/Props/Lambda/Display.hs b/src/Props/Lambda/Display.hs
index 2ed95a6..a8630f2 100644
--- a/src/Props/Lambda/Display.hs
+++ b/src/Props/Lambda/Display.hs
@@ -1,7 +1,15 @@
+{-# LANGUAGE OverloadedStrings #-}
+
 module Props.Lambda.Display
-  ( displayTerm
+  ( findConstNames
+  , makeVarNamesUnique
+  , findVarNames
+  , displayTerm
   ) where
 
+import Data.Maybe
+import           Numeric.Natural
+
 import qualified Data.Text         as T
 
 import           Props.Lambda.Term
@@ -19,13 +27,36 @@ constNames = chars ++ (mappend <$> constNames <*> chars)
     chars = map T.singleton ['A'..'Z']
 
 findConstNames :: Term e (Maybe Name) v -> Term e Name v
-findConstNames = undefined
+findConstNames = mapConsts (fromMaybe "[]") -- TODO implement
 
 makeVarNamesUnique :: Term e c (Maybe Name) -> Term e c (Maybe Name)
-makeVarNamesUnique = undefined
+makeVarNamesUnique = id -- TODO implement
 
 findVarNames :: Term e c (Maybe Name) -> Term e c Name
-findVarNames = undefined
+findVarNames = mapVars (fromMaybe "[]") -- TODO implement
 
-displayTerm :: (e -> T.Text) -> Term e (Maybe Name) (Maybe Name) -> T.Text
-displayTerm = undefined
+displayTerm :: (e -> T.Text) -> Term e Name Name -> T.Text
+displayTerm f = dTerm f []
+
+nth :: [a] -> Natural -> Maybe a
+nth [] _ = Nothing
+nth (x:_) 0 = Just x
+nth (_:xs) n = nth xs $ n - 1
+
+varName :: [Name] -> Natural -> Name
+varName vs i = fromMaybe e $ nth vs i
+  where
+    e = "[" <> T.pack (show i) <> "]"
+
+dTerm :: (e -> T.Text) -> [Name] -> Term e Name Name -> T.Text
+dTerm _ vs (Var i) = varName vs i
+dTerm _ _  (Const c) = c
+dTerm f vs (Lambda v t) = "λ" <> v <> ". " <> dTerm f (v:vs) t
+dTerm f _  (Ext e) = f e
+dTerm f vs (App l r) = dLeft l <> " " <> dRight r
+  where
+    dLeft t@(Lambda _ _) = "(" <> dTerm f vs t <> ")"
+    dLeft t = dTerm f vs t
+    dRight t@(Lambda _ _) = "(" <> dTerm f vs t <> ")"
+    dRight t@(App _ _) = "(" <> dTerm f vs t <> ")"
+    dRight t = dTerm f vs t
diff --git a/src/Props/Lambda/Term.hs b/src/Props/Lambda/Term.hs
index 4609016..acdfe27 100644
--- a/src/Props/Lambda/Term.hs
+++ b/src/Props/Lambda/Term.hs
@@ -1,11 +1,19 @@
+{-# LANGUAGE OverloadedStrings#-}
+
 module Props.Lambda.Term
   ( Term(..)
   , vars
+  , mapVars
   , consts
+  , mapConsts
+  , termI
+  , termY
   ) where
 
 import           Numeric.Natural
 
+import qualified Data.Text as T
+
 -- | Lambda calculus term using De Bruijn indexing and expanded to deal with
 -- naming complexity and extensions.
 data Term e c v
@@ -26,8 +34,30 @@ vars (Lambda v t) = v : vars t
 vars (App l r)    = vars l <> vars r
 vars _            = []
 
+mapVars :: (a -> b) -> Term e c a -> Term e c b
+mapVars _ (Var i) = Var i
+mapVars _ (Const c) = Const c
+mapVars f (Lambda a t) = Lambda (f a) (mapVars f t)
+mapVars f (App l r) = App (mapVars f l) (mapVars f r)
+mapVars _ (Ext e) = Ext e
+
 consts :: Term e c v -> [c]
 consts (Const c)    = [c]
 consts (Lambda _ t) = consts t
 consts (App l r)    = consts l <> consts r
 consts _            = []
+
+mapConsts :: (a -> b) -> Term e a v -> Term e b v
+mapConsts _ (Var i) = Var i
+mapConsts f (Const c) = Const (f c)
+mapConsts f (Lambda v t) = Lambda v (mapConsts f t)
+mapConsts f (App l r) = App (mapConsts f l) (mapConsts f r)
+mapConsts _ (Ext e) = Ext e
+
+termI :: Term e T.Text T.Text
+termI = Lambda "x" (Var 0)
+
+termY :: Term e T.Text T.Text
+termY = Lambda "f" $ App
+  (Lambda "x" $ App (Var 1) $ App (Var 0) (Var 0))
+  (Lambda "x" $ App (Var 1) $ App (Var 0) (Var 0))