From efb0cd6eafbb25a51bba64ac613d910dcec4cfe7 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 15 May 2023 13:18:30 +0200
Subject: Add a sanity check in Driver.ml

---
 compiler/Driver.ml | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/compiler/Driver.ml b/compiler/Driver.ml
index 12a6f075..d8418278 100644
--- a/compiler/Driver.ml
+++ b/compiler/Driver.ml
@@ -211,6 +211,19 @@ let () =
            functions";
         fail ());
 
+      (* We don't support mutually recursive definitions with decreases clauses in Lean *)
+      if
+        !backend = Lean && !extract_decreases_clauses
+        && List.exists
+             (function Aeneas.LlbcAst.Fun (Rec (_ :: _)) -> true | _ -> false)
+             m.declarations
+      then (
+        log#error
+          "The Lean backend doesn't support the use of \
+           decreasing_by/termination_by clauses with mutually recursive \
+           definitions";
+        fail ());
+
       (* Apply the pre-passes *)
       let m = PrePasses.apply_passes m in
 
-- 
cgit v1.2.3