diff --git a/app/Expr.hs b/app/Expr.hs index 1e76dc7..99797e9 100644 --- a/app/Expr.hs +++ b/app/Expr.hs @@ -3,15 +3,39 @@ module Expr where import Data.Function (on) +import Data.List (genericDrop) data Expr where - Var :: Integer -> Expr - Star :: Expr - Square :: Expr - App :: Expr -> Expr -> Expr - Abs :: Expr -> Expr -> Expr - Pi :: Expr -> Expr -> Expr - deriving (Show, Eq) + Var :: Integer -> Expr + Star :: Expr + Square :: Expr + App :: Expr -> Expr -> Expr + Abs :: Expr -> Expr -> Expr + Pi :: Expr -> Expr -> Expr + deriving (Show, Eq) + +{- --------------------- PRETTY PRINTING ----------------------------- -} + +-- TODO : store parsed identifiers for better printing +genName :: Integer -> String +genName k = case genericDrop k ["x", "y", "z", "w", "u", "v"] of + [] -> 'x' : show (k - 6) + (v : _) -> v + +pretty :: Expr -> String +pretty = helper 0 + where + helper :: Integer -> Expr -> String + helper k (Var n) = genName $ k - n - 1 + helper _ Star = "*" + helper _ Square = "□" + helper k (App e1 e2) = "(" ++ helper k e1 ++ " " ++ helper k e2 ++ ")" + helper k (Abs ty b) = + "(λ" ++ genName k ++ " : " ++ helper k ty ++ " . " ++ helper (k + 1) b ++ ")" + helper k (Pi ty b) = + "(∏" ++ genName k ++ " : " ++ helper k ty ++ " . " ++ helper (k + 1) b ++ ")" + +{- --------------- ACTUAL MATH STUFF ---------------- -} isSort :: Expr -> Bool isSort Star = True diff --git a/app/Main.hs b/app/Main.hs index 4ea706c..5ea8da9 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -1,13 +1,14 @@ module Main where +import Expr import Parser import System.IO main :: IO () main = do - _ <- putStr "> " - _ <- hFlush stdout - input <- getLine - case pAll input of - Left err -> putStrLn err - Right expr -> print expr + _ <- putStr "> " + _ <- hFlush stdout + input <- getLine + case pAll input of + Left err -> putStrLn err + Right expr -> putStrLn $ pretty expr