Garmelon/propa-tools
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Display nested lambdas together

Browse source
This commit is contained in:
Joscha 2020-11-26 18:19:18 +01:00
parent 7d0d513735
commit 72083325ce
1 changed files with 11 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

19
src/Props/Lambda/Display.hs
View file

@ -7,7 +7,7 @@ module Props.Lambda.Display
, displayTerm , displayTerm
) where ) where
import Data.Maybe import Data.Maybe
import Numeric.Natural import Numeric.Natural
import qualified Data.Text as T import qualified Data.Text as T
@ -39,8 +39,8 @@ displayTerm :: (e -> T.Text) -> Term e Name Name -> T.Text
displayTerm f = dTerm f [] displayTerm f = dTerm f []
nth :: [a] -> Natural -> Maybe a nth :: [a] -> Natural -> Maybe a
nth [] _ = Nothing nth [] _ = Nothing
nth (x:_) 0 = Just x nth (x:_) 0 = Just x
nth (_:xs) n = nth xs $ n - 1 nth (_:xs) n = nth xs $ n - 1
varName :: [Name] -> Natural -> Name 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 :: (e -> T.Text) -> [Name] -> Term e Name Name -> T.Text
dTerm _ vs (Var i) = varName vs i dTerm _ vs (Var i) = varName vs i
dTerm _ _ (Const c) = c dTerm _ _ (Const c) = c
dTerm f vs (Lambda v t) = "λ" <> v <> ". " <> dTerm f (v:vs) t dTerm f vs (Lambda v t) = "λ" <> v <> dLambda (v:vs) t
dTerm f _ (Ext e) = f e 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 dTerm f vs (App l r) = dLeft l <> " " <> dRight r
where where
dLeft t@(Lambda _ _) = "(" <> dTerm f vs t <> ")" 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@(Lambda _ _) = "(" <> dTerm f vs t <> ")"
dRight t@(App _ _) = "(" <> dTerm f vs t <> ")" dRight t@(App _ _) = "(" <> dTerm f vs t <> ")"
dRight t = dTerm f vs t dRight t = dTerm f vs t
dTerm f _ (Ext e) = f e