max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: check binder names at LCNF/Check.lean

Browse source
This commit is contained in:
Leonardo de Moura 2022-09-04 16:55:42 -07:00
parent 01ca711859
commit abd37d8fd1
1 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Lean/Compiler/LCNF/Check.lean
View file

@ -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