summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/TypeCheck.hs20
1 files changed, 20 insertions, 0 deletions
diff --git a/src/TypeCheck.hs b/src/TypeCheck.hs
index 6777ec8..bc25419 100644
--- a/src/TypeCheck.hs
+++ b/src/TypeCheck.hs
@@ -97,17 +97,37 @@ inferW env term = do
infer :: Env -> Term -> TM (OfType Term Term)
infer env = \case
+ -- Γ |- t ~~> τ -- this is infer, dropping the term result (don't need that)
+ -- τ ~WHNF~> τ'
+ -- ----
+ -- Γ |- t ~~>_W τ'
+
+
+ -- ----
+ -- Set i : Set (isucc i)
TSet i -> do
return (TSet i :| TSet (TISucc i))
+ -- ----
+ -- Setω i : Setω (i + 1)
TSetw i -> do
return (TSetw i :| TSetw (succ i))
+ -- x : τ \in Γ
+ -- ----
+ -- Γ |- x : τ
TVar n -> do
case Map.lookup n env of
Just (_ :| ty) -> return (TVar n :| ty)
Nothing -> throw $ "Variable out of scope: " ++ n
+ -- Γ |- a ~~>_W τ₁
+ -- Γ, x : a |- b ~~>_W τ₂
+ -- k₁ <- ArgKind(τ₁)
+ -- k₂ <- ArgKind(τ₂)
+ -- τ <- ArgKindLower(k₁ <> k₂)
+ -- ----
+ -- Γ |- Π (x : a) b : τ
TPi x a b -> do
inferW env a >>= \case
a' :| (argumentKind -> Just kindA) -> do