ini draft feature complete, compiling, hopefully correct

pkg/proto/lib/Deppy/Core.hs

@@ -78,30 +78,31 @@ extend handleNewBindings oldEnv = \case
 extend1 :: Typ a -> Env a -> Env (Var () a)
 extend1 t = extend \() -> t
 
-infer :: forall a. (a -> Typ a) -> Exp a -> Typ a
+type Typing = Maybe
+
+check :: Eq a => Env a -> Exp a -> Typ a -> Typing ()
+check env e t = do
+  t' <- infer env e
+  guard (t == t')
+
+infer :: forall a. Eq a => Env a -> Exp a -> Typing (Typ a)
 infer env = \case
-  Var v -> env v
+  Var v -> pure $ env v
-  Uni n -> Uni (n + 1)
+  Uni n -> pure $ Uni (n + 1)
-  Fun (Abs t b) -> Uni (max n k)
+  Lam (Abs t b) -> do
-    where
+    Uni _ <- infer env t
-      n = extractUni $ infer env t
+    (toScope -> t') <- infer (extend1 t env) (fromScope b)
-      k = extractUni $ infer (extend1 t env) (fromScope b)
+    pure $ Fun (Abs t t')
-  Lam (Abs t b) -> Fun (Abs t t')
+  Fun (Abs t b) -> do
-    where
+    Uni n <- infer env t
-      -- FIXME require t to be in a universe
+    Uni k <- infer (extend1 t env) (fromScope b)
-      t' = toScope $ infer (extend1 t env) (fromScope b)
+    pure $ Uni (max n k)
-  App x y -> t'
+  App x y -> do
-    where
+    Fun (Abs t b) <- infer env x
-      (Abs t b) = extractFun $ infer env x
+    check env y t
-      t' = undefined
+    pure $ whnf (instantiate1 y b)
 
-extractUni :: Exp a -> Natural
+whnf :: Eq a => Exp a -> Exp a
-extractUni = normalize >>> \case
+whnf = \case
-  Uni n -> n
+  App (whnf -> Lam (Abs _ b)) x -> instantiate1 x b
-
+  e -> e
-extractFun :: Exp a -> Abs a
-extractFun = normalize >>> \case
-  Fun a -> a
-
-normalize :: Exp a -> Exp a
-normalize = undefined