From 3151e373d64f9bce6146a44cd2d3cc64cac84cbf Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 4 Sep 2023 00:59:39 +0200 Subject: Fix minor issues --- compiler/Driver.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'compiler/Driver.ml') diff --git a/compiler/Driver.ml b/compiler/Driver.ml index b646a53d..d88962db 100644 --- a/compiler/Driver.ml +++ b/compiler/Driver.ml @@ -17,7 +17,9 @@ 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; -- cgit v1.2.3 From 8b18c0da053e069b5a2d9fbf06f45eae2f05a029 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 7 Sep 2023 15:28:06 +0200 Subject: Map some globals like u32::MAX to standard definitions --- compiler/Driver.ml | 14 -------------- 1 file changed, 14 deletions(-) (limited to 'compiler/Driver.ml') diff --git a/compiler/Driver.ml b/compiler/Driver.ml index d88962db..0fde1d74 100644 --- a/compiler/Driver.ml +++ b/compiler/Driver.ml @@ -222,20 +222,6 @@ let () = 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 -- cgit v1.2.3 From 0f0e4be7dc746e2676db33f850bbeddf239eaec8 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 13 Oct 2023 00:40:37 +0200 Subject: Add sup --- compiler/Driver.ml | 2 ++ 1 file changed, 2 insertions(+) (limited to 'compiler/Driver.ml') diff --git a/compiler/Driver.ml b/compiler/Driver.ml index 0fde1d74..8a30ead9 100644 --- a/compiler/Driver.ml +++ b/compiler/Driver.ml @@ -24,6 +24,8 @@ let _ = main_log#set_level EL.Info; llbc_of_json_logger#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; -- cgit v1.2.3 From 0ba1c30f735f6e1cce771800d41042e6dc15e86f Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 16 Oct 2023 10:10:40 +0200 Subject: Fix a small issue --- compiler/Driver.ml | 2 -- 1 file changed, 2 deletions(-) (limited to 'compiler/Driver.ml') diff --git a/compiler/Driver.ml b/compiler/Driver.ml index 8a30ead9..414b042d 100644 --- a/compiler/Driver.ml +++ b/compiler/Driver.ml @@ -168,8 +168,6 @@ 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"); (* 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"; -- cgit v1.2.3 From 4f507fa565a43b419af6ea7a641a353f62213b21 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 25 Oct 2023 11:40:47 +0200 Subject: Remove the warning for loops --- compiler/Driver.ml | 8 -------- 1 file changed, 8 deletions(-) (limited to 'compiler/Driver.ml') diff --git a/compiler/Driver.ml b/compiler/Driver.ml index 414b042d..3b9ea4d1 100644 --- a/compiler/Driver.ml +++ b/compiler/Driver.ml @@ -214,14 +214,6 @@ 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"); - (* We don't support mutually recursive definitions with decreases clauses in Lean *) if !backend = Lean && !extract_decreases_clauses -- cgit v1.2.3 From 1110b3da85e93ba0755a665edd5b8c986c54cef0 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 26 Oct 2023 16:15:35 +0200 Subject: Make minor modifications and update the array test for F* --- compiler/Driver.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'compiler/Driver.ml') diff --git a/compiler/Driver.ml b/compiler/Driver.ml index 3b9ea4d1..b660b5a5 100644 --- a/compiler/Driver.ml +++ b/compiler/Driver.ml @@ -162,7 +162,9 @@ 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; -- cgit v1.2.3 From 9df1d191cfaf929b755e9d26d55811531acd939d Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 9 Nov 2023 11:21:53 +0100 Subject: Fix a small issue in AssociatedTypes --- compiler/Driver.ml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) (limited to 'compiler/Driver.ml') diff --git a/compiler/Driver.ml b/compiler/Driver.ml index b660b5a5..14668632 100644 --- a/compiler/Driver.ml +++ b/compiler/Driver.ml @@ -41,7 +41,7 @@ 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; translate_log#set_level EL.Info; scc_log#set_level EL.Info; reorder_decls_log#set_level EL.Info @@ -66,6 +66,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", @@ -118,6 +121,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 @@ -131,6 +136,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); -- cgit v1.2.3 From c57dec640d4e12c3dc66969d626bbbca2eb733fd Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 9 Nov 2023 11:43:47 +0100 Subject: Modify some options and update the Makefile --- compiler/Driver.ml | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'compiler/Driver.ml') diff --git a/compiler/Driver.ml b/compiler/Driver.ml index 14668632..128ae890 100644 --- a/compiler/Driver.ml +++ b/compiler/Driver.ml @@ -93,9 +93,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" ); @@ -106,10 +106,10 @@ 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." ); + ( "-split-files", + Arg.Set split_files, + " 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 \ -- cgit v1.2.3