wball/perga
1
0
Fork 0
Code Issues 15 Pull requests Projects Releases Packages Wiki Activity Actions

minor refactoring

Browse source
This commit is contained in:
William Ball 2024-11-11 13:52:50 -08:00
parent 94709f5320
commit 7426594134
2 changed files with 5 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
app/Check.hs
View file

@ -1,16 +1,14 @@
{-# LANGUAGE BangPatterns #-} -- {-# LANGUAGE BangPatterns #-}
module Check where module Check where
import Control.Monad (guard) import Control.Monad (guard)
import Data.List ((!?)) import Data.List ((!?))
import Debug.Trace (trace)
-- import Debug.Trace (trace)
import Expr import Expr
type Context = [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 :: Context -> Expr -> Maybe Expr
findType g (Var k) = do findType g (Var k) = do
t <- g !? fromInteger k t <- g !? fromInteger k
@ -20,11 +18,8 @@ findType g (Var k) = do
findType _ Star = Just Square findType _ Star = Just Square
findType _ Square = Nothing findType _ Square = Nothing
findType g (App m n) = do findType g (App m n) = do
let !_ = trace ("app: " ++ show m ++ "\t" ++ show n) False
Pi a b <- findType g m Pi a b <- findType g m
let !_ = trace ("Pi: " ++ show a ++ " . " ++ show b) False
a' <- findType g n a' <- findType g n
let !_ = trace ("a': " ++ show a' ++ "\n") False
guard $ betaEquiv a a' guard $ betaEquiv a a'
pure $ subst n b pure $ subst n b
findType g (Abs t v) = do findType g (Abs t v) = do
@ -35,7 +30,6 @@ findType g (Abs t v) = do
guard $ isSort resType guard $ isSort resType
pure $ Pi t bodyType pure $ Pi t bodyType
findType g (Pi t v) = do findType g (Pi t v) = do
let !_ = trace ("Pi rule: " ++ show t ++ "\t" ++ show v ++ "\n") False
argType <- findType g t argType <- findType g t
guard $ isSort argType guard $ isSort argType
bodyType <- findType (incIndices t : map incIndices g) v bodyType <- findType (incIndices t : map incIndices g) v

4
app/Expr.hs
View file

@ -18,7 +18,7 @@ occursFree :: Integer -> Expr -> Bool
occursFree n (Var k) = n == k occursFree n (Var k) = n == k
occursFree _ Star = False occursFree _ Star = False
occursFree _ Square = 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 (Abs a b) = occursFree n a || occursFree (n + 1) b
occursFree n (Pi 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 :: Expr -> Expr
decIndices = mapIndices (Var . subtract 1) 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 :: Expr -> Expr -> Expr
subst s (Var 0) = s subst s (Var 0) = s
subst _ (Var n) = Var $ n - 1 subst _ (Var n) = Var $ n - 1