43 lines
1.5 KiB
Haskell
43 lines
1.5 KiB
Haskell
{-# LANGUAGE BangPatterns #-}
|
|
module Check where
|
|
|
|
import Control.Monad (guard)
|
|
import Data.List ((!?))
|
|
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
|
|
kind <- findType g t
|
|
guard $ isSort kind
|
|
pure t
|
|
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
|
|
argType <- findType g t
|
|
guard $ isSort argType
|
|
bodyType <- findType (incIndices t : map incIndices g) v
|
|
resType <- findType g (Pi t bodyType)
|
|
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
|
|
guard $ isSort bodyType
|
|
pure bodyType
|