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

fix: jp case at check

Browse source
This commit is contained in:
Leonardo de Moura 2022-08-24 11:50:00 -07:00
parent 3a2758a59b
commit 8102e1e31b
1 changed files with 11 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -24,13 +24,10 @@ abbrev CheckM := ReaderT Context $ StateRefT State InferTypeM
def checkFVar (fvarId : FVarId) : CheckM Unit :=
unless (← read).vars.contains fvarId do
throwError "invalid out of scope free variable {fvarId.name}"
let localDecl ← getLocalDecl fvarId
throwError "invalid out of scope free variable {localDecl.userName}"
def checkApp (f : Expr) (args : Array Expr) : CheckM Unit := do
unless f.isConst || f.isFVar do
throwError "unexpected function application, function must be a constant or free variable{indentExpr (mkAppN f args)}"
if f.isFVar then
checkFVar f.fvarId!
def checkAppArgs (f : Expr) (args : Array Expr) : CheckM Unit := do
let mut fType ← inferType f
let mut j := 0
for i in [:args.size] do
@ -58,6 +55,13 @@ def checkApp (f : Expr) (args : Array Expr) : CheckM Unit := do
checkFVar arg.fvarId!
fType := b
def checkApp (f : Expr) (args : Array Expr) : CheckM Unit := do
unless f.isConst || f.isFVar do
throwError "unexpected function application, function must be a constant or free variable{indentExpr (mkAppN f args)}"
if f.isFVar then
checkFVar f.fvarId!
checkAppArgs f args
def checkExpr (e : Expr) : CheckM Unit :=
match e with
| .lit _ => pure ()
@ -153,7 +157,7 @@ partial def check (code : Code) : CheckM Expr := do
withFVarId decl.fvarId do check k
| .jp decl k => checkFunDecl decl; withJp decl.fvarId do check k
| .cases c => checkCases c
| .jmp fvarId args => checkJpInScope fvarId; checkApp (.fvar fvarId) args; code.inferType
| .jmp fvarId args => checkJpInScope fvarId; checkAppArgs (.fvar fvarId) args; code.inferType
| .return fvarId => checkFVar fvarId; code.inferType
| .unreach .. => code.inferType