From 72083325ce976c3e2a306fa56e685db1688e7e16 Mon Sep 17 00:00:00 2001 From: Joscha Date: Thu, 26 Nov 2020 18:19:18 +0100 Subject: [PATCH] Display nested lambdas together --- src/Props/Lambda/Display.hs | 19 +++++++++++-------- 1 file changed, 11 insertions(+), 8 deletions(-) diff --git a/src/Props/Lambda/Display.hs b/src/Props/Lambda/Display.hs index a8630f2..3197aa5 100644 --- a/src/Props/Lambda/Display.hs +++ b/src/Props/Lambda/Display.hs @@ -7,7 +7,7 @@ module Props.Lambda.Display , displayTerm ) where -import Data.Maybe +import Data.Maybe import Numeric.Natural import qualified Data.Text as T @@ -39,8 +39,8 @@ 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 [] _ = Nothing +nth (x:_) 0 = Just x nth (_:xs) n = nth xs $ n - 1 varName :: [Name] -> Natural -> Name @@ -51,12 +51,15 @@ varName vs i = fromMaybe e $ nth vs 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 (Lambda v t) = "λ" <> v <> dLambda (v:vs) t + where + dLambda ws (Lambda w u) = " " <> w <> dLambda (w:ws) u + dLambda ws u = ". " <> dTerm f ws u dTerm f vs (App l r) = dLeft l <> " " <> dRight r where dLeft t@(Lambda _ _) = "(" <> dTerm f vs t <> ")" - dLeft t = 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 + dRight t@(App _ _) = "(" <> dTerm f vs t <> ")" + dRight t = dTerm f vs t +dTerm f _ (Ext e) = f e