Prerequisites
Description
I couldn't see a tracking issue for this, so thought I'd create one to refer to from mathlib4.
We quite often use Nat.rec and List.rec, and neither are supported by the code generator:
|
private def supportedRecursors := |
|
#[``Empty.rec, ``False.rec, ``Eq.ndrec, ``Eq.rec, ``Eq.recOn, ``Eq.casesOn, ``False.casesOn, ``Empty.casesOn, ``And.rec, ``And.casesOn] |
|
|
|
/-- This is a temporary workaround for generating better error messages for the compiler. It can be deleted after we |
|
rewrite the remaining parts of the compiler in Lean. -/ |
|
private def checkUnsupported [Monad m] [MonadEnv m] [MonadError m] (decl : Declaration) : m Unit := do |
|
let env ← getEnv |
|
decl.forExprM fun e => |
|
let unsupportedRecursor? := e.find? fun |
|
| Expr.const declName .. => |
|
((isAuxRecursor env declName && !isCasesOnRecursor env declName) || isRecCore env declName) |
|
&& !supportedRecursors.contains declName |
|
| _ => false |
|
match unsupportedRecursor? with |
|
| some (Expr.const declName ..) => throwError "code generator does not support recursor '{declName}' yet, consider using 'match ... with' and/or structural recursion" |
|
| _ => pure () |
Steps to Reproduce
Run
#eval (List.rec 0 (fun x xs ih => 0) ([] : List Nat) : Nat)
Expected behavior: Prints 0
Actual behavior:
code generator does not support recursor 'List.rec' yet, consider using 'match ... with' and/or structural recursion
Reproduces how often: 100%
Prerequisites
Description
I couldn't see a tracking issue for this, so thought I'd create one to refer to from mathlib4.
We quite often use
Nat.recandList.rec, and neither are supported by the code generator:lean4/src/Lean/CoreM.lean
Lines 280 to 295 in a125a36
Steps to Reproduce
Run
Expected behavior: Prints 0
Actual behavior:
Reproduces how often: 100%