From abd37d8fd1c9e2dffbad5e05758081efba922199 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 4 Sep 2022 16:55:42 -0700 Subject: [PATCH] feat: check binder names at `LCNF/Check.lean` --- src/Lean/Compiler/LCNF/Check.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/Lean/Compiler/LCNF/Check.lean b/src/Lean/Compiler/LCNF/Check.lean index cc388bb543..156920acc4 100644 --- a/src/Lean/Compiler/LCNF/Check.lean +++ b/src/Lean/Compiler/LCNF/Check.lean @@ -93,6 +93,8 @@ def checkJpInScope (jp : FVarId) : CheckM Unit := do def checkParam (param : Param) : CheckM Unit := do let localDecl ← getLocalDecl param.fvarId + unless localDecl.userName == param.binderName do + throwError "LCNF parameter mismatch at `{param.binderName}`, binder name in local context `{localDecl.userName}`" unless localDecl.type == param.type do throwError "LCNF parameter mismatch at `{param.binderName}`, type in local context{indentExpr localDecl.type}\nexpected{indentExpr param.type}" @@ -105,6 +107,8 @@ def checkLetDecl (letDecl : LetDecl) : CheckM Unit := do unless compatibleTypes letDecl.type valueType do throwError "type mismatch at `{letDecl.binderName}`, value has type{indentExpr valueType}\nbut is expected to have type{indentExpr letDecl.type}" let localDecl ← getLocalDecl letDecl.fvarId + unless localDecl.userName == letDecl.binderName do + throwError "LCNF let declaration mismatch at `{letDecl.binderName}`, binder name in local context `{localDecl.userName}`" unless localDecl.type == letDecl.type do throwError "LCNF let declaration mismatch at `{letDecl.binderName}`, type in local context{indentExpr localDecl.type}\nexpected{indentExpr letDecl.type}" unless localDecl.value == letDecl.value do @@ -140,6 +144,8 @@ partial def checkFunDeclCore (declName : Name) (type : Expr) (params : Array Par partial def checkFunDecl (funDecl : FunDecl) : CheckM Unit := do checkFunDeclCore funDecl.binderName funDecl.type funDecl.params funDecl.value let localDecl ← getLocalDecl funDecl.fvarId + unless localDecl.userName == funDecl.binderName do + throwError "LCNF local function declaration mismatch at `{funDecl.binderName}`, binder name in local context `{localDecl.userName}`" unless localDecl.type == funDecl.type do throwError "LCNF local function declaration mismatch at `{funDecl.binderName}`, type in local context{indentExpr localDecl.type}\nexpected{indentExpr funDecl.type}" unless (← getFunDecl funDecl.fvarId) == funDecl do