From 94709f53208e79768f8629e980f785a7f9cd4969 Mon Sep 17 00:00:00 2001 From: William Ball Date: Mon, 11 Nov 2024 13:43:28 -0800 Subject: [PATCH] made pretty printer use -> if possible --- app/Expr.hs | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/app/Expr.hs b/app/Expr.hs index aa1d2fc..10602a0 100644 --- a/app/Expr.hs +++ b/app/Expr.hs @@ -14,6 +14,14 @@ data Expr where Pi :: Expr -> Expr -> Expr deriving (Show, Eq) +occursFree :: Integer -> Expr -> Bool +occursFree n (Var k) = n == k +occursFree _ Star = False +occursFree _ Square = False +occursFree n (App a b) = occursFree n a || occursFree n b +occursFree n (Abs a b) = occursFree n a || occursFree (n + 1) b +occursFree n (Pi a b) = occursFree n a || occursFree (n + 1) b + {- --------------------- PRETTY PRINTING ----------------------------- -} -- TODO : store parsed identifiers for better printing @@ -33,7 +41,10 @@ pretty = helper 0 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 ++ ")" + if occursFree 0 b + then + "(∏" ++ genName k ++ " : " ++ helper k ty ++ " . " ++ helper (k + 1) b ++ ")" + else "(" ++ helper k ty ++ " -> " ++ helper (k + 1) b ++ ")" {- --------------- ACTUAL MATH STUFF ---------------- -}