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 ---------------- -}