diff options
| -rw-r--r-- | src/TypeCheck.hs | 20 |
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 |