From b4bad8df4eabb17c71dfa7b24d79d62fc06d0a70 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 7 Mar 2023 08:40:55 +0100
Subject: Print warnings for the Lean backend and loops

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

diff --git a/compiler/Driver.ml b/compiler/Driver.ml
index f460f73d..1dbd611a 100644
--- a/compiler/Driver.ml
+++ b/compiler/Driver.ml
@@ -80,7 +80,7 @@ let () =
       ( "-test-trans-units",
         Arg.Set test_trans_unit_functions,
         " Test the translated unit functions with the target theorem\n\
-        \                         prover's normalizer" );
+        \                             prover's normalizer" );
       ( "-decreases-clauses",
         Arg.Set extract_decreases_clauses,
         " Use decreases clauses for the recursive definitions" );
@@ -96,16 +96,15 @@ let () =
       ( "-template-clauses",
         Arg.Set extract_template_decreases_clauses,
         " Generate templates for the required decreases clauses, in a \
-          dedicated file. Implies -decreases-clauses"
-      );
+         dedicated file. Implies -decreases-clauses" );
       ( "-no-split-files",
         Arg.Clear split_files,
         " Don't split the definitions between different files for types, \
-          functions, etc." );
+         functions, etc." );
       ( "-no-check-inv",
         Arg.Clear check_invariants,
         " Deactivate the invariant sanity checks performed at every step of \
-          evaluation. Dramatically saves speed." );
+         evaluation. Dramatically saves speed." );
     ]
   in
 
@@ -118,8 +117,7 @@ let () =
     exit 1
   in
 
-  if !extract_template_decreases_clauses then
-    extract_decreases_clauses := true;
+  if !extract_template_decreases_clauses then extract_decreases_clauses := true;
 
   (* Sanity check (now that the arguments are parsed!): -template-clauses ==> decrease-clauses *)
   assert (!extract_decreases_clauses || not !extract_template_decreases_clauses);
@@ -152,7 +150,8 @@ let () =
         decompose_monadic_let_bindings := true;
         decompose_nested_let_patterns := true
     | Lean ->
-        ()
+        (* The Lean backend is experimental: print a warning *)
+        log#lwarning (lazy "The Lean backend is experimental")
   in
 
   (* Retrieve and check the filename *)
@@ -188,6 +187,12 @@ let () =
       log#linfo (lazy ("Imported: " ^ filename));
       log#ldebug (lazy ("\n" ^ Print.Crate.crate_to_string m ^ "\n"));
 
+      (* Print a warning if the crate contains loops (loops are experimental for now) *)
+      let has_loops =
+        List.exists Aeneas.LlbcAstUtils.fun_decl_has_loops m.functions
+      in
+      if has_loops then log#lwarning (lazy "Support for loops is experimental");
+
       (* Apply the pre-passes *)
       let m = PrePasses.apply_passes m in
 
-- 
cgit v1.2.3