diff options
| -rw-r--r-- | compiler/Driver.ml | 21 |
1 files 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 |