Merge branch 'main' into afromher_shifts

1 files changed, 41 insertions, 51 deletions

diff --git a/compiler/Driver.ml b/compiler/Main.ml
index b646a53d..7f98f581 100644
--- a/compiler/Driver.ml
+++ b/compiler/Main.ml
@@ -1,15 +1,10 @@
 open Aeneas.LlbcOfJson
 open Aeneas.Logging
-module T = Aeneas.Types
-module A = Aeneas.LlbcAst
-module I = Aeneas.Interpreter
+open Aeneas.LlbcAst
+open Aeneas.Interpreter
 module EL = Easy_logging.Logging
-module TA = Aeneas.TypesAnalysis
-module Micro = Aeneas.PureMicroPasses
-module Print = Aeneas.Print
-module PrePasses = Aeneas.PrePasses
-module Translate = Aeneas.Translate
 open Aeneas.Config
+open Aeneas
 
 (** The local logger *)
 let log = main_log
@@ -17,11 +12,16 @@ let log = main_log
 let _ =
   (* Set up the logging - for now we use default values - TODO: use the
    * command-line arguments *)
-  (* By setting a level for the main_logger_handler, we filter everything *)
+  (* By setting a level for the main_logger_handler, we filter everything.
+     To have a good trace: one should switch between Info and Debug.
+  *)
   Easy_logging.Handlers.set_level main_logger_handler EL.Debug;
   main_log#set_level EL.Info;
   llbc_of_json_logger#set_level EL.Info;
+  regions_hierarchy_log#set_level EL.Info;
   pre_passes_log#set_level EL.Info;
+  associated_types_log#set_level EL.Info;
+  contexts_log#set_level EL.Info;
   interpreter_log#set_level EL.Info;
   statements_log#set_level EL.Info;
   loops_match_ctxs_log#set_level EL.Info;
@@ -37,7 +37,8 @@ let _ =
   pure_utils_log#set_level EL.Info;
   symbolic_to_pure_log#set_level EL.Info;
   pure_micro_passes_log#set_level EL.Info;
-  pure_to_extract_log#set_level EL.Info;
+  extract_log#set_level EL.Info;
+  builtin_log#set_level EL.Info;
   translate_log#set_level EL.Info;
   scc_log#set_level EL.Info;
   reorder_decls_log#set_level EL.Info
@@ -62,6 +63,9 @@ let () =
   (* Read the command line arguments *)
   let dest_dir = ref "" in
 
+  (* Print the imported llbc *)
+  let print_llbc = ref false in
+
   let spec =
     [
       ( "-backend",
@@ -86,9 +90,9 @@ let () =
         Arg.Set extract_decreases_clauses,
         " Use decreases clauses/termination measures for the recursive \
          definitions" );
-      ( "-no-state",
-        Arg.Clear use_state,
-        " Do not use state-error monads, simply use error monads" );
+      ( "-state",
+        Arg.Set use_state,
+        " Use a *state*-error monads, instead of an error monads" );
       ( "-use-fuel",
         Arg.Set use_fuel,
         " Use a fuel parameter to control divergence" );
@@ -99,14 +103,14 @@ let () =
         Arg.Set extract_template_decreases_clauses,
         " Generate templates for the required decreases clauses/termination \
          measures, in a dedicated file. Implies -decreases-clauses" );
-      ( "-no-split-files",
-        Arg.Clear split_files,
-        " Do not split the definitions between different files for types, \
-         functions, etc." );
-      ( "-no-check-inv",
-        Arg.Clear check_invariants,
-        " Deactivate the invariant sanity checks performed at every evaluation \
-         step. Dramatically increases speed." );
+      ( "-split-files",
+        Arg.Set split_files,
+        " Split the definitions between different files for types, functions, \
+         etc." );
+      ( "-checks",
+        Arg.Set sanity_checks,
+        " Activate extensive sanity checks (warning: causes a ~100 times slow \
+         down)." );
       ( "-no-gen-lib-entry",
         Arg.Clear generate_lib_entry_point,
         " Do not generate the entry point file for the generated library (only \
@@ -114,6 +118,8 @@ let () =
       ( "-lean-default-lakefile",
         Arg.Clear lean_gen_lakefile,
         " Generate a default lakefile.lean (Lean only)" );
+      ("-print-llbc", Arg.Set print_llbc, " Print the imported LLBC");
+      ("-k", Arg.Clear fail_hard, " Do not fail hard in case of error");
     ]
   in
 
@@ -127,6 +133,7 @@ let () =
   in
 
   if !extract_template_decreases_clauses then extract_decreases_clauses := true;
+  if !print_llbc then main_log#set_level EL.Debug;
 
   (* Sanity check (now that the arguments are parsed!): -template-clauses ==> decrease-clauses *)
   assert (!extract_decreases_clauses || not !extract_template_decreases_clauses);
@@ -158,20 +165,23 @@ let () =
     | FStar ->
         (* Some patterns are not supported *)
         decompose_monadic_let_bindings := false;
-        decompose_nested_let_patterns := false
+        decompose_nested_let_patterns := false;
+        (* F* can disambiguate the field names *)
+        record_fields_short_names := true
     | Coq ->
         (* Some patterns are not supported *)
         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");
         (* We don't support fuel for the Lean backend *)
         if !use_fuel then (
           log#error "The Lean backend doesn't support the -use-fuel option";
           fail ());
         (* Lean can disambiguate the field names *)
-        record_fields_short_names := true
+        record_fields_short_names := true;
+        (* We exploit the fact that the variant name should always be
+           prefixed with the type name to prevent collisions *)
+        variant_concatenate_type_name := false
     | HOL4 ->
         (* We don't support fuel for the HOL4 backend *)
         if !use_fuel then (
@@ -212,33 +222,13 @@ 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 =
-        A.FunDeclId.Map.exists
-          (fun _ -> Aeneas.LlbcAstUtils.fun_decl_has_loops)
-          m.functions
-      in
-      if has_loops then log#lwarning (lazy "Support for loops is experimental");
-
-      (* If we target Lean, we request the crates to be split into several files
-         whenever there are opaque functions *)
-      if
-        !backend = Lean
-        && A.FunDeclId.Map.exists
-             (fun _ (d : A.fun_decl) -> d.body = None)
-             m.functions
-        && not !split_files
-      then (
-        log#error
-          "For Lean, we request the -split-file option whenever using opaque \
-           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)
+             (function
+               | Aeneas.LlbcAst.FunGroup (RecGroup (_ :: _)) -> true
+               | _ -> false)
              m.declarations
       then (
         log#error
@@ -248,15 +238,15 @@ let () =
         fail ());
 
       (* Apply the pre-passes *)
-      let m = PrePasses.apply_passes m in
+      let m = Aeneas.PrePasses.apply_passes m in
 
       (* Some options for the execution *)
 
       (* Test the unit functions with the concrete interpreter *)
-      if !test_unit_functions then I.Test.test_unit_functions m;
+      if !test_unit_functions then Test.test_unit_functions m;
 
       (* Translate the functions *)
-      Translate.translate_crate filename dest_dir m;
+      Aeneas.Translate.translate_crate filename dest_dir m;
 
       (* Print total elapsed time *)
       log#linfo