From 74265941348a06803d27ea91bb37993326e0d551 Mon Sep 17 00:00:00 2001
From: William Ball <williampi103@gmail.com>
Date: Mon, 11 Nov 2024 13:52:50 -0800
Subject: [PATCH] minor refactoring

---
 app/Check.hs | 12 +++---------
 app/Expr.hs  |  4 ++--
 2 files changed, 5 insertions(+), 11 deletions(-)

diff --git a/app/Check.hs b/app/Check.hs
index 377135a..98547f8 100644
--- a/app/Check.hs
+++ b/app/Check.hs
@@ -1,16 +1,14 @@
-{-# LANGUAGE BangPatterns #-}
+-- {-# LANGUAGE BangPatterns #-}
 module Check where
 
 import Control.Monad (guard)
 import Data.List ((!?))
-import Debug.Trace (trace)
+
+-- import Debug.Trace (trace)
 import Expr
 
 type Context = [Expr]
 
--- λ S : * . λ P : ∏ x : S . * . ∏ x : S . P x
--- lambda S : * . lambda P : Pi x : S . * . lambda Q : Pi x : S . * . lambda H : (Pi x : S . Pi h : P x . Q x) . lambda G : (Pi x : S . P x) . lambda x : S . H x (G x)
--- lambda S : * . lambda P : (Pi x : S . *). lambda H : (Pi x : S . P x) . lambda x : S . H x
 findType :: Context -> Expr -> Maybe Expr
 findType g (Var k) = do
     t <- g !? fromInteger k
@@ -20,11 +18,8 @@ findType g (Var k) = do
 findType _ Star = Just Square
 findType _ Square = Nothing
 findType g (App m n) = do
-    let !_ = trace ("app: " ++ show m ++ "\t" ++ show n) False
     Pi a b <- findType g m
-    let !_ = trace ("Pi: " ++ show a ++ " . " ++ show b) False
     a' <- findType g n
-    let !_ = trace ("a': " ++ show a' ++ "\n") False
     guard $ betaEquiv a a'
     pure $ subst n b
 findType g (Abs t v) = do
@@ -35,7 +30,6 @@ findType g (Abs t v) = do
     guard $ isSort resType
     pure $ Pi t bodyType
 findType g (Pi t v) = do
-    let !_ = trace ("Pi rule: " ++ show t ++ "\t" ++ show v ++ "\n") False
     argType <- findType g t
     guard $ isSort argType
     bodyType <- findType (incIndices t : map incIndices g) v
diff --git a/app/Expr.hs b/app/Expr.hs
index 10602a0..4723aa2 100644
--- a/app/Expr.hs
+++ b/app/Expr.hs
@@ -18,7 +18,7 @@ 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 (App a b) = on (||) (occursFree n) a 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
 
@@ -67,7 +67,7 @@ incIndices = mapIndices (Var . (+ 1))
 decIndices :: Expr -> Expr
 decIndices = mapIndices (Var . subtract 1)
 
--- substitute 0 for s *AND* decrement indices; only use after reducing a redex.
+-- substitute s for 0 *AND* decrement indices; only use after reducing a redex.
 subst :: Expr -> Expr -> Expr
 subst s (Var 0) = s
 subst _ (Var n) = Var $ n - 1