summaryrefslogtreecommitdiff
path: root/backends
diff options
context:
space:
mode:
authorSon HO2024-03-09 01:12:20 +0100
committerGitHub2024-03-09 01:12:20 +0100
commit14171474f9a4a45874d181cdb6567c7af7dc32cd (patch)
treef4c7dcd5b172e8922487dec83070e2c38e7b441a /backends
parent169d011cbfa83d853d0148bbf6b946e6ccbe4c4c (diff)
parent46f2f1c0c4c37f089e42c82d76d79817101c5407 (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.lean30
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