diff options
author | Son HO | 2024-03-09 01:12:20 +0100 |
---|---|---|
committer | GitHub | 2024-03-09 01:12:20 +0100 |
commit | 14171474f9a4a45874d181cdb6567c7af7dc32cd (patch) | |
tree | f4c7dcd5b172e8922487dec83070e2c38e7b441a /backends | |
parent | 169d011cbfa83d853d0148bbf6b946e6ccbe4c4c (diff) | |
parent | 46f2f1c0c4c37f089e42c82d76d79817101c5407 (diff) |
Merge pull request #85 from AeneasVerif/son/fix_loops3
Fix some issues with the loops
Diffstat (limited to 'backends')
-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 |