From e97782e3cc554821964b2bb8b44af0a58230f6a6 Mon Sep 17 00:00:00 2001 From: anqurvanillapy Date: Thu, 8 Aug 2024 12:43:29 +0800 Subject: [PATCH] Fix #1: Bugfix of checking function types Signed-off-by: anqurvanillapy --- lyzh/concrete/elab.py | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/lyzh/concrete/elab.py b/lyzh/concrete/elab.py index 89b078f..61f6a6a 100644 --- a/lyzh/concrete/elab.py +++ b/lyzh/concrete/elab.py @@ -99,12 +99,12 @@ def infer(self, e: cst.Expr) -> typing.Tuple[ast.Term, ast.Term]: # Γ , A : type ⊢ M : type # -------------------------- function type introduction rule # Γ ⊢ π (A: type) → M : type - p_typ, _ = self.infer(p.type) # 参数类型的类型一定是 Univ, 所以忽略了 + p_typ = self.check(p.type, ast.Univ()) # 参数类型的类型一定是 Univ, 但我们仍需要确保这一点 inferred_p = core.Param[ast.Term](p.name, p_typ) - # 在参数 p 的保护下, 推导 body 的类型. - b_tm, b_ty = self.guarded_infer(inferred_p, b) + # 在参数 p 的保护下, 检查 body 的类型. + b_tm = self.guarded_check(inferred_p, b, ast.Univ()) # 重新拼回去组成一个 ast.FnType. - return ast.FnType(inferred_p, b_tm), b_ty + return ast.FnType(inferred_p, b_tm), ast.Univ() case cst.App(_, f, x): # Γ ⊢ f : π (x : A) → B x : A # ------------------------------ function elimination rule @@ -130,7 +130,7 @@ def infer(self, e: cst.Expr) -> typing.Tuple[ast.Term, ast.Term]: raise AssertionError("impossible") def guarded_check( - self, p: core.Param[ast.Term], e: cst.Expr, typ: ast.Term + self, p: core.Param[ast.Term], e: cst.Expr, typ: ast.Term ) -> ast.Term: """在 p 的保护下 (即将 p 加入到本地变量中, 检查完毕后删除), 检查表达式 e 的类型是否为 typ.""" self.locals[p.name.id] = p.type @@ -142,7 +142,7 @@ def guarded_check( return ret def guarded_infer( - self, p: core.Param[ast.Term], e: cst.Expr + self, p: core.Param[ast.Term], e: cst.Expr ) -> typing.Tuple[ast.Term, ast.Term]: """在 p 的保护下 (即将 p 加入到本地变量中, 推导完毕后删除), 推导表达式 e 的类型.""" self.locals[p.name.id] = p.type