diff options
| -rw-r--r-- | backends/lean/Base/Diverge/Elab.lean | 30 |
1 files changed, 27 insertions, 3 deletions
diff --git a/backends/lean/Base/Diverge/Elab.lean b/backends/lean/Base/Diverge/Elab.lean index 3c2ea877..f30148dc 100644 --- a/backends/lean/Base/Diverge/Elab.lean +++ b/backends/lean/Base/Diverge/Elab.lean @@ -510,9 +510,19 @@ def mkDeclareUnaryBodies (grLvlParams : List Name) (kk_var : Expr) let i ← mkFinVal grSize id -- Check that there are no type parameters if type_info.num_params ≠ 0 then throwError "mkUnaryBodies: a recursive call was not eliminated" - -- Introduce the call to the continuation - let param_args ← mkSigmasVal type_info.params_ty [] - mkAppM' kk_var #[i, param_args] + -- We might be in a degenerate case, if the function takes no arguments + -- at all (i.e., the function is a constant). + -- For instance: + -- ``` + -- divergent def infinite_loop : Result Unit := infinite_loop + -- `` + if type_info.total_num_args == 0 then do + trace[Diverge.def.genBody.visit] "Degenerate case: total_num_args=0" + mkAppM' kk_var #[i, UnitValue, UnitValue] + else do + -- Introduce the call to the continuation + let param_args ← mkSigmasVal type_info.params_ty [] + mkAppM' kk_var #[i, param_args] else pure e | _ => pure e trace[Diverge.def.genBody.visit] "done with expression (depth: {i}): {e}" @@ -1571,6 +1581,20 @@ namespace Tests #check test1.unfold + -- Testing a degenerate case + divergent def infinite_loop : Result Unit := + do + let _ ← infinite_loop + Result.ret () + + #check infinite_loop.unfold + + -- Testing a degenerate case + divergent def infinite_loop1 : Result Unit := + infinite_loop1 + + #check infinite_loop1.unfold + /- Tests with higher-order functions -/ section HigherOrder open Ex8 |