summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
authorSon HO2024-06-06 09:15:22 +0200
committerGitHub2024-06-06 09:15:22 +0200
commit961cc880311aed3319b08755c5a43816e2490d7f (patch)
tree80cc3d5db32d7198adbdf89e516484dc01e58186 /compiler
parentbaa0771885546816461e063131162b94c6954d86 (diff)
parenta4dd9fe0598328976862868097f59207846d865c (diff)
Merge pull request #233 from AeneasVerif/son/borrow-check
Add a `-borrow-check` option
Diffstat (limited to 'compiler')
-rw-r--r--compiler/BorrowCheck.ml28
-rw-r--r--compiler/Config.ml22
-rw-r--r--compiler/Extract.ml185
-rw-r--r--compiler/ExtractBase.ml74
-rw-r--r--compiler/ExtractBuiltin.ml24
-rw-r--r--compiler/ExtractTypes.ml173
-rw-r--r--compiler/Interpreter.ml42
-rw-r--r--compiler/InterpreterLoopsFixedPoint.ml29
-rw-r--r--compiler/InterpreterLoopsMatchCtxs.ml5
-rw-r--r--compiler/InterpreterPaths.ml16
-rw-r--r--compiler/Logging.ml3
-rw-r--r--compiler/Main.ml106
-rw-r--r--compiler/Print.ml3
-rw-r--r--compiler/PureMicroPasses.ml4
-rw-r--r--compiler/PureUtils.ml2
-rw-r--r--compiler/SymbolicToPure.ml2
-rw-r--r--compiler/Translate.ml42
-rw-r--r--compiler/dune1
18 files changed, 458 insertions, 303 deletions
diff --git a/compiler/BorrowCheck.ml b/compiler/BorrowCheck.ml
new file mode 100644
index 00000000..52f42c37
--- /dev/null
+++ b/compiler/BorrowCheck.ml
@@ -0,0 +1,28 @@
+open Interpreter
+open LlbcAst
+
+(** The local logger *)
+let log = Logging.borrow_check_log
+
+(** Borrow-check a crate.
+
+ Note that we don't return anything: if we find borrow-checking errors,
+ we register them and print them later.
+ *)
+let borrow_check_crate (crate : crate) : unit =
+ (* Debug *)
+ log#ldebug (lazy "translate_crate_to_pure");
+
+ (* Compute the translation context *)
+ let trans_ctx = compute_contexts crate in
+
+ (* Borrow-check *)
+ let borrow_check_fun (fdef : fun_decl) : unit =
+ match fdef.body with
+ | None -> ()
+ | Some _ ->
+ let synthesize = false in
+ let _ = evaluate_function_symbolic synthesize trans_ctx fdef in
+ ()
+ in
+ List.iter borrow_check_fun (FunDeclId.Map.values crate.fun_decls)
diff --git a/compiler/Config.ml b/compiler/Config.ml
index 0b26e2ef..cb2c86ad 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -26,12 +26,22 @@ let set_backend (b : string) : unit =
belonging to the proper set *)
raise (Failure "Unexpected")
-(** The backend to which to extract.
+(** If [true], we do not generate code and simply borrow-check the program instead.
+ This allows us to relax some sanity checks which are present in the symbolic
+ execution only to make sure we will be able to generate the pure translation.
+
+ Remark: when checking if we are borrow-checking a program, checking this
+ boolean or checking if [opt_backend] is [None] are equivalent. We need to
+ have different variables for the purpose of implementing the parsing of
+ the CI arguments.
+ *)
+let borrow_check = ref false
- We initialize it with a default value, but it always gets overwritten:
- we check that the user provides a backend argument.
- *)
-let backend = ref FStar
+(** Get the target backend *)
+let backend () : backend = Option.get !opt_backend
+
+let if_backend (f : unit -> 'a) (default : 'a) : 'a =
+ match !opt_backend with None -> default | Some _ -> f ()
(** {1 Interpreter} *)
@@ -361,7 +371,7 @@ let variant_concatenate_type_name = ref true
let use_tuple_structs = ref true
let backend_has_tuple_projectors () =
- match !backend with Lean -> true | Coq | FStar | HOL4 -> false
+ match backend () with Lean -> true | Coq | FStar | HOL4 -> false
(** We we use nested projectors for tuple (like: [(0, 1).snd.fst]) or do
we use better projector syntax? *)
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 035ea8fe..eab85054 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -58,7 +58,7 @@ let extract_fun_decl_register_names (ctx : extraction_ctx)
(* Add the termination measure *)
let ctx = ctx_add_termination_measure def ctx in
(* Add the decreases proof for Lean only *)
- match !Config.backend with
+ match backend () with
| Coq | FStar -> ctx
| HOL4 -> craise __FILE__ __LINE__ def.span "Unexpected"
| Lean -> ctx_add_decreases_proof def ctx
@@ -98,7 +98,7 @@ let extract_adt_g_value (span : Meta.span)
let extract_as_tuple () =
(* This is very annoying: in Coq, we can't write [()] for the value of
type [unit], we have to write [tt]. *)
- if !backend = Coq && field_values = [] then (
+ if backend () = Coq && field_values = [] then (
F.pp_print_string fmt "tt";
ctx)
else
@@ -108,7 +108,8 @@ let extract_adt_g_value (span : Meta.span)
*)
let lb, rb =
if List.length field_values = 1 then ("", "")
- else if !backend = Coq && is_single_pat && List.length field_values > 2
+ else if
+ backend () = Coq && is_single_pat && List.length field_values > 2
then ("'(", ")")
else ("(", ")")
in
@@ -150,7 +151,7 @@ let extract_adt_g_value (span : Meta.span)
Otherwise, it is: `let Cons x0 ... xn = ...`
*)
- is_single_pat && !Config.backend = Lean
+ is_single_pat && backend () = Lean
then (
F.pp_print_string fmt "⟨";
F.pp_print_space fmt ();
@@ -273,7 +274,7 @@ let rec extract_typed_pattern (span : Meta.span) (ctx : extraction_ctx)
block (because some of them are monadic) *)
let lets_require_wrap_in_do (span : Meta.span)
(lets : (bool * typed_pattern * texpression) list) : bool =
- match !backend with
+ match backend () with
| Lean ->
(* For Lean, we wrap in a block iff at least one of the let-bindings is monadic *)
List.exists (fun (m, _, _) -> m) lets
@@ -299,7 +300,7 @@ let lets_require_wrap_in_do (span : Meta.span)
*)
let extract_texpression_errors (fmt : F.formatter) =
- match !Config.backend with
+ match backend () with
| FStar | Coq -> F.pp_print_string fmt "admit"
| Lean -> F.pp_print_string fmt "sorry"
| HOL4 -> F.pp_print_string fmt "(* ERROR: could not generate the code *)"
@@ -360,7 +361,7 @@ and extract_App (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
const_name ctx
in
let add_brackets (s : string) =
- if !backend = Coq then "(" ^ s ^ ")" else s
+ if backend () = Coq then "(" ^ s ^ ")" else s
in
F.pp_print_string fmt ("." ^ add_brackets name))
| _ ->
@@ -472,7 +473,7 @@ and extract_function_call (span : Meta.span) (ctx : extraction_ctx)
method_name ctx
in
let add_brackets (s : string) =
- if !backend = Coq then "(" ^ s ^ ")" else s
+ if backend () = Coq then "(" ^ s ^ ")" else s
in
F.pp_print_string fmt ("." ^ add_brackets fun_name))
else
@@ -496,7 +497,7 @@ and extract_function_call (span : Meta.span) (ctx : extraction_ctx)
(* Sanity check: HOL4 doesn't support const generics *)
sanity_check __FILE__ __LINE__
- (generics.const_generics = [] || !backend <> HOL4)
+ (generics.const_generics = [] || backend () <> HOL4)
span;
(* Print the generics.
@@ -588,7 +589,7 @@ and extract_field_projector (span : Meta.span) (ctx : extraction_ctx)
let field_name =
(* Check if we need to extract the type as a tuple *)
if is_tuple_struct then
- match !backend with
+ match backend () with
| FStar | HOL4 | Coq -> FieldId.to_string proj.field_id
| Lean ->
(* Tuples in Lean are syntax sugar for nested products/pairs,
@@ -623,7 +624,7 @@ and extract_field_projector (span : Meta.span) (ctx : extraction_ctx)
Note that the first "." is added below.
*)
let field_id = FieldId.to_int proj.field_id in
- if !Config.use_nested_tuple_projectors then
+ if !use_nested_tuple_projectors then
(* Nested projection: "2.2.2..." *)
if field_id = 0 then "1"
else
@@ -640,10 +641,10 @@ and extract_field_projector (span : Meta.span) (ctx : extraction_ctx)
(* Extract the expression *)
extract_texpression span ctx fmt true arg;
(* We allow to break where the "." appears (except Lean, it's a syntax error) *)
- if !backend <> Lean then F.pp_print_break fmt 0 0;
+ if backend () <> Lean then F.pp_print_break fmt 0 0;
F.pp_print_string fmt ".";
(* If in Coq, the field projection has to be parenthesized *)
- (match !backend with
+ (match backend () with
| FStar | Lean | HOL4 -> F.pp_print_string fmt field_name
| Coq -> F.pp_print_string fmt ("(" ^ field_name ^ ")"));
(* Close the box *)
@@ -665,7 +666,7 @@ and extract_Lambda (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
(* Print the lambda - note that there should always be at least one variable *)
sanity_check __FILE__ __LINE__ (xl <> []) span;
F.pp_print_string fmt "fun";
- let with_type = !backend = Coq in
+ let with_type = backend () = Coq in
let ctx =
List.fold_left
(fun ctx x ->
@@ -674,7 +675,7 @@ and extract_Lambda (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
ctx xl
in
F.pp_print_space fmt ();
- if !backend = Lean || !backend = Coq then F.pp_print_string fmt "=>"
+ if backend () = Lean || backend () = Coq then F.pp_print_string fmt "=>"
else F.pp_print_string fmt "->";
F.pp_print_space fmt ();
(* Print the body *)
@@ -709,7 +710,7 @@ and extract_lets (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
]}
*)
let lets, next_e =
- match !backend with
+ match backend () with
| HOL4 -> destruct_lets_no_interleave span e
| FStar | Coq | Lean -> destruct_lets e
in
@@ -730,11 +731,11 @@ and extract_lets (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
* ]}
* TODO: cleanup
* *)
- if monadic && (!backend = Coq || !backend = HOL4) then (
+ if monadic && (backend () = Coq || backend () = HOL4) then (
let ctx = extract_typed_pattern span ctx fmt true true lv in
F.pp_print_space fmt ();
let arrow =
- match !backend with
+ match backend () with
| Coq | HOL4 -> "<-"
| FStar | Lean -> craise __FILE__ __LINE__ span "impossible"
in
@@ -746,7 +747,7 @@ and extract_lets (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
else (
(* Print the "let" *)
if monadic then
- match !backend with
+ match backend () with
| FStar ->
F.pp_print_string fmt "let*";
F.pp_print_space fmt ()
@@ -760,7 +761,7 @@ and extract_lets (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
let ctx = extract_typed_pattern span ctx fmt true true lv in
F.pp_print_space fmt ();
let eq =
- match !backend with
+ match backend () with
| FStar -> "="
| Coq -> ":="
| Lean -> if monadic then "←" else ":="
@@ -770,7 +771,7 @@ and extract_lets (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_space fmt ();
extract_texpression span ctx fmt false re;
(* End the let-binding *)
- (match !backend with
+ (match backend () with
| Lean ->
(* In Lean, (monadic) let-bindings don't require to end with anything *)
()
@@ -791,9 +792,9 @@ and extract_lets (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
at the end of every let-binding: let-bindings are indeed not ended
with an "in" keyword.
*)
- if !Config.backend = Lean then F.pp_open_vbox fmt 0 else F.pp_open_hvbox fmt 0;
+ if backend () = Lean then F.pp_open_vbox fmt 0 else F.pp_open_hvbox fmt 0;
(* Open parentheses *)
- if inside && !backend <> Lean then F.pp_print_string fmt "(";
+ if inside && backend () <> Lean then F.pp_print_string fmt "(";
(* If Lean and HOL4, we rely on monadic blocks, so we insert a do and open a new box
immediately *)
let wrap_in_do_od = lets_require_wrap_in_do span lets in
@@ -814,11 +815,11 @@ and extract_lets (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
(* do-box (Lean and HOL4 only) *)
if wrap_in_do_od then
- if !backend = HOL4 then (
+ if backend () = HOL4 then (
F.pp_print_space fmt ();
F.pp_print_string fmt "od");
(* Close parentheses *)
- if inside && !backend <> Lean then F.pp_print_string fmt ")";
+ if inside && backend () <> Lean then F.pp_print_string fmt ")";
(* Close the box for the whole expression *)
F.pp_close_box fmt ()
@@ -832,14 +833,14 @@ and extract_Switch (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
In the case of Lean, we rely on indentation to delimit the end of the
branches, and need to insert line breaks: we thus use a vbox.
*)
- if !Config.backend = Lean then F.pp_open_vbox fmt 0 else F.pp_open_hvbox fmt 0;
+ if backend () = Lean then F.pp_open_vbox fmt 0 else F.pp_open_hvbox fmt 0;
(* Extract the switch *)
(match body with
| If (e_then, e_else) ->
(* Open a box for the [if e] *)
F.pp_open_hovbox fmt ctx.indent_incr;
F.pp_print_string fmt "if";
- if !backend = Lean && ctx.use_dep_ite then F.pp_print_string fmt " h:";
+ if backend () = Lean && ctx.use_dep_ite then F.pp_print_string fmt " h:";
F.pp_print_space fmt ();
let scrut_inside =
PureUtils.texpression_requires_parentheses span scrut
@@ -863,7 +864,7 @@ and extract_Switch (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
(* Open the parenthesized expression *)
let print_space_after_parenth =
if parenth then (
- match !backend with
+ match backend () with
| FStar ->
F.pp_print_space fmt ();
F.pp_print_string fmt "begin";
@@ -885,7 +886,7 @@ and extract_Switch (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_close_box fmt ();
(* Close the parenthesized expression *)
(if parenth then
- match !backend with
+ match backend () with
| FStar ->
F.pp_print_space fmt ();
F.pp_print_string fmt "end"
@@ -901,7 +902,7 @@ and extract_Switch (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_open_hovbox fmt ctx.indent_incr;
(* Print the [match ... with] *)
let match_begin =
- match !backend with
+ match backend () with
| FStar -> "begin match"
| Coq -> "match"
| Lean -> if ctx.use_dep_ite then "match h:" else "match"
@@ -917,7 +918,7 @@ and extract_Switch (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
extract_texpression span ctx fmt scrut_inside scrut;
F.pp_print_space fmt ();
let match_scrut_end =
- match !backend with FStar | Coq | Lean -> "with" | HOL4 -> "of"
+ match backend () with FStar | Coq | Lean -> "with" | HOL4 -> "of"
in
F.pp_print_string fmt match_scrut_end;
(* Close the box for the [match ... with] *)
@@ -936,7 +937,7 @@ and extract_Switch (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
let ctx = extract_typed_pattern span ctx fmt false false br.pat in
F.pp_print_space fmt ();
let arrow =
- match !backend with FStar -> "->" | Coq | Lean | HOL4 -> "=>"
+ match backend () with FStar -> "->" | Coq | Lean | HOL4 -> "=>"
in
F.pp_print_string fmt arrow;
(* Close the box for the pattern *)
@@ -955,7 +956,7 @@ and extract_Switch (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
List.iter extract_branch branches;
(* End the match *)
- match !backend with
+ match backend () with
| Lean -> (*We rely on indentation in Lean *) ()
| FStar | Coq ->
F.pp_print_space fmt ();
@@ -969,11 +970,11 @@ and extract_StructUpdate (span : Meta.span) (ctx : extraction_ctx)
unit =
(* We can't update a subset of the fields in Coq (i.e., we can do
[{| x:= 3; y := 4 |}], but there is no syntax for [{| s with x := 3 |}]) *)
- sanity_check __FILE__ __LINE__ (!backend <> Coq || supd.init = None) span;
+ sanity_check __FILE__ __LINE__ (backend () <> Coq || supd.init = None) span;
(* In the case of HOL4, records with no fields are not supported and are
thus extracted to unit. We need to check that by looking up the definition *)
let extract_as_unit =
- match (!backend, supd.struct_id) with
+ match (backend (), supd.struct_id) with
| HOL4, TAdtId adt_id ->
let d = TypeDeclId.Map.find adt_id ctx.trans_ctx.type_ctx.type_decls in
d.kind = Struct []
@@ -1009,14 +1010,14 @@ and extract_StructUpdate (span : Meta.span) (ctx : extraction_ctx)
*)
(* Outer brackets *)
let olb, orb =
- match !backend with
+ match backend () with
| Lean | FStar -> (Some "{", Some "}")
| Coq -> (Some "{|", Some "|}")
| HOL4 -> (None, None)
in
(* Inner brackets *)
let ilb, irb =
- match !backend with
+ match backend () with
| Lean | FStar | Coq -> (None, None)
| HOL4 -> (Some "<|", Some "|>")
in
@@ -1030,7 +1031,7 @@ and extract_StructUpdate (span : Meta.span) (ctx : extraction_ctx)
| None -> ()
in
print_bracket true olb;
- let need_paren = inside && !backend = HOL4 in
+ let need_paren = inside && backend () = HOL4 in
if need_paren then F.pp_print_string fmt "(";
F.pp_open_hvbox fmt ctx.indent_incr;
if supd.init <> None then (
@@ -1042,10 +1043,10 @@ and extract_StructUpdate (span : Meta.span) (ctx : extraction_ctx)
print_bracket true ilb;
F.pp_open_hvbox fmt 0;
let delimiter =
- match !backend with Lean -> "," | Coq | FStar | HOL4 -> ";"
+ match backend () with Lean -> "," | Coq | FStar | HOL4 -> ";"
in
let assign =
- match !backend with Coq | Lean | HOL4 -> ":=" | FStar -> "="
+ match backend () with Coq | Lean | HOL4 -> ":=" | FStar -> "="
in
Collections.List.iter_link
(fun () ->
@@ -1093,7 +1094,7 @@ and extract_StructUpdate (span : Meta.span) (ctx : extraction_ctx)
F.pp_close_box fmt ();
(* Print the values *)
let delimiter =
- match !backend with Lean -> "," | Coq | FStar | HOL4 -> ";"
+ match backend () with Lean -> "," | Coq | FStar | HOL4 -> ";"
in
F.pp_print_space fmt ();
F.pp_open_hovbox fmt 0;
@@ -1209,7 +1210,7 @@ let extract_fun_inputs_output_parameters_types (ctx : extraction_ctx)
extract_ty def.span ctx fmt TypeDeclId.Set.empty false def.signature.output
let assert_backend_supports_decreases_clauses (span : Meta.span) =
- match !backend with
+ match backend () with
| FStar | Lean -> ()
| _ ->
craise __FILE__ __LINE__ span
@@ -1233,7 +1234,9 @@ let assert_backend_supports_decreases_clauses (span : Meta.span) =
*)
let extract_template_fstar_decreases_clause (ctx : extraction_ctx)
(fmt : F.formatter) (def : fun_decl) : unit =
- cassert __FILE__ __LINE__ (!backend = FStar) def.span
+ cassert __FILE__ __LINE__
+ (backend () = FStar)
+ def.span
"The generation of template decrease clauses is only supported for the F* \
backend";
@@ -1245,7 +1248,7 @@ let extract_template_fstar_decreases_clause (ctx : extraction_ctx)
F.pp_print_break fmt 0 0;
(* Print a comment to link the extracted type to its original rust definition *)
(let name =
- if !Config.extract_external_name_patterns && not def.is_local then
+ if !extract_external_name_patterns && not def.is_local then
Some def.llbc_name
else None
in
@@ -1302,7 +1305,9 @@ let extract_template_fstar_decreases_clause (ctx : extraction_ctx)
*)
let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx)
(fmt : F.formatter) (def : fun_decl) : unit =
- cassert __FILE__ __LINE__ (!backend = Lean) def.span
+ cassert __FILE__ __LINE__
+ (backend () = Lean)
+ def.span
"The generation of template termination and decreasing clauses is only \
supported for the Lean backend";
(*
@@ -1414,7 +1419,7 @@ let extract_fun_comment (ctx : extraction_ctx) (fmt : F.formatter)
[ comment_pre ^ loop_comment ]
in
let name =
- if !Config.extract_external_name_patterns && not def.is_local then
+ if !extract_external_name_patterns && not def.is_local then
Some def.llbc_name
else None
in
@@ -1433,7 +1438,7 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
(* Retrieve the function name *)
let def_name = ctx_get_local_function def.span def.def_id def.loop_id ctx in
(* Add a break before *)
- if !backend <> HOL4 || not (decl_is_first_from_group kind) then
+ if backend () <> HOL4 || not (decl_is_first_from_group kind) then
F.pp_print_break fmt 0 0;
(* Print a comment to link the extracted definition to its original rust definition *)
extract_fun_comment ctx fmt def;
@@ -1443,7 +1448,7 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_open_hvbox fmt 0;
F.pp_open_vbox fmt ctx.indent_incr;
(* For HOL4: we may need to put parentheses around the definition *)
- let parenthesize = !backend = HOL4 && decl_is_not_last_from_group kind in
+ let parenthesize = backend () = HOL4 && decl_is_not_last_from_group kind in
if parenthesize then F.pp_print_string fmt "(";
(* Open a box for "let FUN_NAME (PARAMS) : EFFECT =" *)
F.pp_open_hovbox fmt ctx.indent_incr;
@@ -1454,7 +1459,7 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
The boolean [is_opaque_coq] is used to detect this case.
*)
- let is_opaque_coq = !backend = Coq && is_opaque in
+ let is_opaque_coq = backend () = Coq && is_opaque in
let use_forall =
is_opaque_coq && def.signature.generics <> empty_generic_params
in
@@ -1502,7 +1507,7 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
(* [Tot] *)
if has_decreases_clause then (
assert_backend_supports_decreases_clauses def.span;
- if !backend = FStar then (
+ if backend () = FStar then (
F.pp_print_string fmt "Tot";
F.pp_print_space fmt ()));
extract_ty def.span ctx fmt TypeDeclId.Set.empty has_decreases_clause
@@ -1511,7 +1516,7 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_close_box fmt ();
(* Print the decrease clause - rk.: a function with a decreases clause
* is necessarily a transparent function *)
- if has_decreases_clause && !backend = FStar then (
+ if has_decreases_clause && backend () = FStar then (
assert_backend_supports_decreases_clauses def.span;
F.pp_print_space fmt ();
(* Open a box for the decreases clause *)
@@ -1569,7 +1574,7 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
(* Print the "=" *)
if not is_opaque then (
F.pp_print_space fmt ();
- let eq = match !backend with FStar | HOL4 -> "=" | Coq | Lean -> ":=" in
+ let eq = match backend () with FStar | HOL4 -> "=" | Coq | Lean -> ":=" in
F.pp_print_string fmt eq);
(* Close the box for "(PARAMS) : EFFECT =" *)
F.pp_close_box fmt ();
@@ -1588,7 +1593,7 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
(* Close the inner box for the definition *)
F.pp_close_box fmt ();
(* Termination clause and proof for Lean *)
- if has_decreases_clause && !backend = Lean then (
+ if has_decreases_clause && backend () = Lean then (
let def_body = Option.get def.body in
let all_vars = List.map (fun (v : var) -> v.id) def_body.inputs in
let num_fwd_inputs =
@@ -1659,10 +1664,10 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
(* Close the parentheses *)
if parenthesize then F.pp_print_string fmt ")";
(* Add the definition end delimiter *)
- if !backend = HOL4 && decl_is_not_last_from_group kind then (
+ if backend () = HOL4 && decl_is_not_last_from_group kind then (
F.pp_print_space fmt ();
F.pp_print_string fmt "/\\")
- else if !backend = Coq && decl_is_last_from_group kind then (
+ else if backend () = Coq && decl_is_last_from_group kind then (
(* This is actually an end of group delimiter. For aesthetic reasons
we print it here instead of in {!end_fun_decl_group}. *)
F.pp_print_cut fmt ();
@@ -1670,7 +1675,7 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
(* Close the outer box for the definition *)
F.pp_close_box fmt ();
(* Add breaks to insert new lines between definitions *)
- if !backend <> HOL4 || decl_is_not_last_from_group kind then
+ if backend () <> HOL4 || decl_is_not_last_from_group kind then
F.pp_print_break fmt 0 0
(** Extract an opaque function declaration to HOL4.
@@ -1733,7 +1738,7 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
(kind : decl_kind) (has_decreases_clause : bool) (def : fun_decl) : unit =
sanity_check __FILE__ __LINE__ (not def.is_global_decl_body) def.span;
(* We treat HOL4 opaque functions in a specific manner *)
- if !backend = HOL4 && Option.is_none def.body then
+ if backend () = HOL4 && Option.is_none def.body then
extract_fun_decl_hol4_opaque ctx fmt def
else extract_fun_decl_gen ctx fmt kind has_decreases_clause def
@@ -1752,7 +1757,7 @@ let extract_global_decl_body_gen (span : Meta.span) (ctx : extraction_ctx)
let is_opaque = Option.is_none extract_body in
(* HOL4: Definition wrapper *)
- if !backend = HOL4 then (
+ if backend () = HOL4 then (
(* Open a vertical box: we *must* break lines *)
F.pp_open_vbox fmt 0;
F.pp_print_string fmt ("Definition " ^ name ^ "_def:");
@@ -1797,7 +1802,7 @@ let extract_global_decl_body_gen (span : Meta.span) (ctx : extraction_ctx)
if not is_opaque then (
(* Print " =" *)
F.pp_print_space fmt ();
- let eq = match !backend with FStar | HOL4 -> "=" | Coq | Lean -> ":=" in
+ let eq = match backend () with FStar | HOL4 -> "=" | Coq | Lean -> ":=" in
F.pp_print_string fmt eq);
(* Close ": TYPE =" box (depth=2) *)
F.pp_close_box fmt ();
@@ -1817,7 +1822,7 @@ let extract_global_decl_body_gen (span : Meta.span) (ctx : extraction_ctx)
F.pp_close_box fmt ();
(* Coq: add a "." *)
- if !backend = Coq then (
+ if backend () = Coq then (
F.pp_print_cut fmt ();
F.pp_print_string fmt ".");
@@ -1825,7 +1830,7 @@ let extract_global_decl_body_gen (span : Meta.span) (ctx : extraction_ctx)
F.pp_close_box fmt ();
(* HOL4: Definition wrapper *)
- if !backend = HOL4 then (
+ if backend () = HOL4 then (
F.pp_close_box fmt ();
F.pp_print_space fmt ();
F.pp_print_string fmt "End";
@@ -1888,7 +1893,7 @@ let extract_global_decl_aux (ctx : extraction_ctx) (fmt : F.formatter)
(* Add a break then the name of the corresponding LLBC declaration *)
F.pp_print_break fmt 0 0;
let name =
- if !Config.extract_external_name_patterns && not global.is_local then
+ if !extract_external_name_patterns && not global.is_local then
Some global.llbc_name
else None
in
@@ -1918,7 +1923,7 @@ let extract_global_decl_aux (ctx : extraction_ctx) (fmt : F.formatter)
| None ->
(* No body: only generate a [val x_c : u32] declaration *)
let kind = if interface then Declared else Assumed in
- if !backend = HOL4 then
+ if backend () = HOL4 then
extract_global_decl_hol4_opaque span ctx fmt decl_name global.generics
decl_ty
else
@@ -1949,7 +1954,7 @@ let extract_global_decl_aux (ctx : extraction_ctx) (fmt : F.formatter)
let use_brackets = all_params <> [] in
(* Extract the name *)
let before, after =
- match !backend with
+ match backend () with
| FStar | Lean ->
( (fun () ->
F.pp_print_string fmt "eval_global";
@@ -1994,7 +1999,7 @@ let extract_trait_decl_register_parent_clause_names (ctx : extraction_ctx)
let name = ctx_compute_trait_parent_clause_name ctx trait_decl c in
(* Add a prefix if necessary *)
let name =
- if !Config.record_fields_short_names then name
+ if !record_fields_short_names then name
else ctx_compute_trait_decl_name ctx trait_decl ^ name
in
(c.clause_id, name))
@@ -2027,7 +2032,7 @@ let extract_trait_decl_register_constant_names (ctx : extraction_ctx)
let name = ctx_compute_trait_const_name ctx trait_decl item_name in
(* Add a prefix if necessary *)
let name =
- if !Config.record_fields_short_names then name
+ if !record_fields_short_names then name
else ctx_compute_trait_decl_name ctx trait_decl ^ name
in
(item_name, name))
@@ -2061,7 +2066,7 @@ let extract_trait_decl_type_names (ctx : extraction_ctx)
let type_name =
ctx_compute_trait_type_name ctx trait_decl item_name
in
- if !Config.record_fields_short_names then type_name
+ if !record_fields_short_names then type_name
else ctx_compute_trait_decl_name ctx trait_decl ^ type_name
in
let compute_clause_name (item_name : string) (clause : trait_clause) :
@@ -2071,7 +2076,7 @@ let extract_trait_decl_type_names (ctx : extraction_ctx)
in
(* Add a prefix if necessary *)
let name =
- if !Config.record_fields_short_names then name
+ if !record_fields_short_names then name
else ctx_compute_trait_decl_name ctx trait_decl ^ name
in
(clause.clause_id, name)
@@ -2141,7 +2146,7 @@ let extract_trait_decl_method_names (ctx : extraction_ctx)
let name = ctx_compute_fun_name f ctx in
(* Add a prefix if necessary *)
let name =
- if !Config.record_fields_short_names then name
+ if !record_fields_short_names then name
else ctx_compute_trait_decl_name ctx trait_decl ^ "_" ^ name
in
(item_name, name)
@@ -2271,7 +2276,7 @@ let extract_trait_item (ctx : extraction_ctx) (fmt : F.formatter)
(* ":" or "=" *)
F.pp_print_string fmt separator;
ty ();
- (match !Config.backend with Lean -> () | _ -> F.pp_print_string fmt ";");
+ (match backend () with Lean -> () | _ -> F.pp_print_string fmt ";");
F.pp_close_box fmt ()
let extract_trait_decl_item (ctx : extraction_ctx) (fmt : F.formatter)
@@ -2280,7 +2285,7 @@ let extract_trait_decl_item (ctx : extraction_ctx) (fmt : F.formatter)
let extract_trait_impl_item (ctx : extraction_ctx) (fmt : F.formatter)
(item_name : string) (ty : unit -> unit) : unit =
- let assign = match !Config.backend with Lean | Coq -> ":=" | _ -> "=" in
+ let assign = match backend () with Lean | Coq -> ":=" | _ -> "=" in
extract_trait_item ctx fmt item_name assign ty
(** Small helper - TODO: move *)
@@ -2325,7 +2330,7 @@ let extract_trait_decl_method_items (ctx : extraction_ctx) (fmt : F.formatter)
generics ctx
in
let backend_uses_forall =
- match !backend with Coq | Lean -> true | FStar | HOL4 -> false
+ match backend () with Coq | Lean -> true | FStar | HOL4 -> false
in
let generics_not_empty = generics <> empty_generic_params in
let use_forall = generics_not_empty && backend_uses_forall in
@@ -2350,7 +2355,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_break fmt 0 0;
(* Print a comment to link the extracted type to its original rust definition *)
(let name =
- if !Config.extract_external_name_patterns && not decl.is_local then
+ if !extract_external_name_patterns && not decl.is_local then
Some decl.llbc_name
else None
in
@@ -2364,7 +2369,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
There is just an exception with Lean: in this backend, line breaks are important
for the parsing, so we always open a vertical box.
*)
- if !Config.backend = Lean then F.pp_open_vbox fmt ctx.indent_incr
+ if backend () = Lean then F.pp_open_vbox fmt ctx.indent_incr
else (
F.pp_open_hvbox fmt 0;
F.pp_open_hvbox fmt ctx.indent_incr);
@@ -2378,7 +2383,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
(* When checking if the trait declaration is empty: we ignore the provided
methods, because for now they are extracted separately *)
let is_empty = trait_decl_is_empty { decl with provided_methods = [] } in
- if !backend = FStar && not is_empty then (
+ if backend () = FStar && not is_empty then (
F.pp_print_string fmt "noeq";
F.pp_print_space fmt ());
F.pp_print_string fmt qualif;
@@ -2396,18 +2401,18 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
type_params cg_params trait_clauses;
F.pp_print_space fmt ();
- if is_empty && !backend = FStar then (
+ if is_empty && backend () = FStar then (
F.pp_print_string fmt "= unit";
(* Outer box *)
F.pp_close_box fmt ())
- else if is_empty && !backend = Coq then (
+ else if is_empty && backend () = Coq then (
(* Coq is not very good at infering constructors *)
let cons = ctx_get_trait_constructor decl.span decl.def_id ctx in
F.pp_print_string fmt (":= " ^ cons ^ "{}.");
(* Outer box *)
F.pp_close_box fmt ())
else (
- (match !backend with
+ (match backend () with
| Lean -> F.pp_print_string fmt "where"
| FStar -> F.pp_print_string fmt "= {"
| Coq ->
@@ -2481,9 +2486,9 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
decl.required_methods;
(* Close the outer boxes for the definition *)
- if !Config.backend <> Lean then F.pp_close_box fmt ();
+ if backend () <> Lean then F.pp_close_box fmt ();
(* Close the brackets *)
- match !Config.backend with
+ match backend () with
| Lean -> ()
| Coq ->
F.pp_print_space fmt ();
@@ -2554,7 +2559,7 @@ let extract_trait_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter)
(** See {!extract_trait_decl_coq_arguments} *)
let extract_trait_decl_extra_info (ctx : extraction_ctx) (fmt : F.formatter)
(trait_decl : trait_decl) : unit =
- match !backend with
+ match backend () with
| Coq -> extract_trait_decl_coq_arguments ctx fmt trait_decl
| _ -> ()
@@ -2645,7 +2650,7 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_break fmt 0 0;
(* Print a comment to link the extracted type to its original rust definition *)
(let name, generics =
- if !Config.extract_external_name_patterns && not impl.is_local then
+ if !extract_external_name_patterns && not impl.is_local then
let decl_id = impl.impl_trait.trait_decl_id in
let trait_decl = TraitDeclId.Map.find decl_id ctx.trans_trait_decls in
let decl_ref = impl.llbc_impl_trait in
@@ -2665,7 +2670,7 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
There is just an exception with Lean: in this backend, line breaks are important
for the parsing, so we always open a vertical box.
*)
- if !Config.backend = Lean then (
+ if backend () = Lean then (
F.pp_open_vbox fmt 0;
F.pp_open_vbox fmt ctx.indent_incr)
else (
@@ -2705,11 +2710,11 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
let is_empty = trait_impl_is_empty { impl with provided_methods = [] } in
F.pp_print_space fmt ();
- if is_empty && !Config.backend = FStar then (
+ if is_empty && backend () = FStar then (
F.pp_print_string fmt "= ()";
(* Outer box *)
F.pp_close_box fmt ())
- else if is_empty && !Config.backend = Coq then (
+ else if is_empty && backend () = Coq then (
(* Coq is not very good at infering constructors *)
let cons =
ctx_get_trait_constructor impl.span impl.impl_trait.trait_decl_id ctx
@@ -2718,8 +2723,8 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
(* Outer box *)
F.pp_close_box fmt ())
else (
- if !Config.backend = Lean then F.pp_print_string fmt ":= {"
- else if !Config.backend = Coq then F.pp_print_string fmt ":= {|"
+ if backend () = Lean then F.pp_print_string fmt ":= {"
+ else if backend () = Coq then F.pp_print_string fmt ":= {|"
else F.pp_print_string fmt "= {";
(* Close the box for the name + generics *)
@@ -2811,10 +2816,10 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
(* Close the outer boxes for the definition, as well as the brackets *)
F.pp_close_box fmt ();
- if !backend = Coq then (
+ if backend () = Coq then (
F.pp_print_space fmt ();
F.pp_print_string fmt "|}.")
- else if (not (!backend = FStar)) || not is_empty then (
+ else if (not (backend () = FStar)) || not is_empty then (
F.pp_print_space fmt ();
F.pp_print_string fmt "}"));
F.pp_close_box fmt ();
@@ -2854,7 +2859,7 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
(* Open a box for the test *)
F.pp_open_hovbox fmt ctx.indent_incr;
(* Print the test *)
- (match !backend with
+ (match backend () with
| FStar ->
F.pp_print_string fmt "let _ =";
F.pp_print_space fmt ();
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 815e228f..4aac270f 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -495,14 +495,14 @@ let names_maps_add_function (id_to_string : id -> string)
names_maps =
names_maps_add id_to_string (FunId fid) span name nm
-let bool_name () = if !backend = Lean then "Bool" else "bool"
-let char_name () = if !backend = Lean then "Char" else "char"
-let str_name () = if !backend = Lean then "String" else "string"
+let bool_name () = if backend () = Lean then "Bool" else "bool"
+let char_name () = if backend () = Lean then "Char" else "char"
+let str_name () = if backend () = Lean then "String" else "string"
(** Small helper to compute the name of an int type *)
let int_name (int_ty : integer_type) : string =
let isize, usize, i_format, u_format =
- match !backend with
+ match backend () with
| FStar | Coq | HOL4 ->
("isize", "usize", format_of_string "i%d", format_of_string "u%d")
| Lean -> ("Isize", "Usize", format_of_string "I%d", format_of_string "U%d")
@@ -525,9 +525,9 @@ let scalar_name (ty : literal_type) : string =
match ty with
| TInteger ty -> int_name ty
| TBool -> (
- match !backend with FStar | Coq | HOL4 -> "bool" | Lean -> "Bool")
+ match backend () with FStar | Coq | HOL4 -> "bool" | Lean -> "Bool")
| TChar -> (
- match !backend with FStar | Coq | HOL4 -> "char" | Lean -> "Char")
+ match backend () with FStar | Coq | HOL4 -> "char" | Lean -> "Char")
(** Extraction context.
@@ -786,13 +786,13 @@ let ctx_get_termination_measure (span : Meta.span) (def_id : A.FunDeclId.id)
let unop_name (unop : unop) : string =
match unop with
| Not -> (
- match !backend with
+ match backend () with
| FStar -> "not"
| Lean -> "¬"
| Coq -> "negb"
| HOL4 -> "~")
| Neg (int_ty : integer_type) -> (
- match !backend with Lean -> "-." | _ -> int_name int_ty ^ "_neg")
+ match backend () with Lean -> "-." | _ -> int_name int_ty ^ "_neg")
| Cast _ ->
(* We never directly use the unop name in this case *)
raise (Failure "Unsupported")
@@ -821,7 +821,7 @@ let named_binop_name (binop : E.binop) (int_ty : integer_type) : string =
| _ -> raise (Failure "Unreachable")
in
(* Remark: the Lean case is actually not used *)
- match !backend with
+ match backend () with
| Lean -> int_name int_ty ^ "." ^ binop_s
| FStar | Coq | HOL4 -> int_name int_ty ^ "_" ^ binop_s
@@ -843,13 +843,14 @@ let keywords () =
named_binops
in
let misc =
- match !backend with
+ match backend () with
| FStar ->
[
"assert";
"assert_norm";
"assume";
"else";
+ "end";
"fun";
"fn";
"FStar";
@@ -882,6 +883,7 @@ let keywords () =
"Declare";
"Definition";
"else";
+ "end";
"End";
"fun";
"Fixpoint";
@@ -1042,7 +1044,7 @@ let keywords () =
let assumed_adts () : (assumed_ty * string) list =
let state =
if !use_state then
- match !backend with
+ match backend () with
| Lean -> [ (TState, "State") ]
| Coq | FStar | HOL4 -> [ (TState, "state") ]
else []
@@ -1051,7 +1053,7 @@ let assumed_adts () : (assumed_ty * string) list =
referenced in the generated translation, and easily collides
with user-defined types *)
let adts =
- match !backend with
+ match backend () with
| Lean ->
[
(TResult, "Result");
@@ -1065,7 +1067,7 @@ let assumed_adts () : (assumed_ty * string) list =
| Coq | FStar | HOL4 ->
[
(TResult, "result");
- (TFuel, if !backend = HOL4 then "num" else "nat");
+ (TFuel, if backend () = HOL4 then "num" else "nat");
(TArray, "array");
(TSlice, "slice");
(TStr, "str");
@@ -1076,14 +1078,14 @@ let assumed_adts () : (assumed_ty * string) list =
state @ adts
let assumed_struct_constructors () : (assumed_ty * string) list =
- match !backend with
+ match backend () with
| Lean -> [ (TArray, "Array.make") ]
| Coq -> [ (TArray, "mk_array") ]
| FStar -> [ (TArray, "mk_array") ]
| HOL4 -> [ (TArray, "mk_array") ]
let assumed_variants () : (assumed_ty * VariantId.id * string) list =
- match !backend with
+ match backend () with
| FStar ->
[
(TResult, result_ok_id, "Ok");
@@ -1123,7 +1125,7 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list =
]
let assumed_llbc_functions () : (A.assumed_fun_id * string) list =
- match !backend with
+ match backend () with
| FStar | Coq | HOL4 ->
[
(ArrayIndexShared, "array_index_usize");
@@ -1146,7 +1148,7 @@ let assumed_llbc_functions () : (A.assumed_fun_id * string) list =
]
let assumed_pure_functions () : (pure_assumed_fun_id * string) list =
- match !backend with
+ match backend () with
| FStar ->
[
(Return, "return");
@@ -1258,7 +1260,7 @@ let initialize_names_maps () : names_maps =
*)
let type_decl_kind_to_qualif (span : Meta.span) (kind : decl_kind)
(type_kind : type_decl_kind option) : string option =
- match !backend with
+ match backend () with
| FStar -> (
match kind with
| SingleNonRec -> Some "type"
@@ -1307,7 +1309,7 @@ let type_decl_kind_to_qualif (span : Meta.span) (kind : decl_kind)
Remark: can return [None] for some backends like HOL4.
*)
let fun_decl_kind_to_qualif (kind : decl_kind) : string option =
- match !backend with
+ match backend () with
| FStar -> (
match kind with
| SingleNonRec -> Some "let"
@@ -1342,7 +1344,7 @@ let fun_decl_kind_to_qualif (kind : decl_kind) : string option =
TODO: move inside the formatter?
*)
let type_keyword (span : Meta.span) =
- match !backend with
+ match backend () with
| FStar -> "Type0"
| Coq | Lean -> "Type"
| HOL4 -> craise __FILE__ __LINE__ span "Unexpected"
@@ -1391,7 +1393,7 @@ let ctx_compute_type_name_no_suffix (span : Meta.span) (ctx : extraction_ctx)
let ctx_compute_type_name (span : Meta.span) (ctx : extraction_ctx)
(name : llbc_name) =
let name = ctx_compute_type_name_no_suffix span ctx name in
- match !backend with
+ match backend () with
| FStar -> StringUtils.lowercase_first_letter (name ^ "_t")
| Coq | HOL4 -> name ^ "_t"
| Lean -> name
@@ -1425,7 +1427,7 @@ let ctx_compute_field_name (span : Meta.span) (ctx : extraction_ctx)
let def_name =
ctx_compute_type_name_no_suffix span ctx def_name ^ "_" ^ field_name_s
in
- match !backend with
+ match backend () with
| Lean | HOL4 -> def_name
| Coq | FStar -> StringUtils.lowercase_first_letter def_name
@@ -1435,7 +1437,7 @@ let ctx_compute_field_name (span : Meta.span) (ctx : extraction_ctx)
*)
let ctx_compute_variant_name (span : Meta.span) (ctx : extraction_ctx)
(def_name : llbc_name) (variant : string) : string =
- match !backend with
+ match backend () with
| FStar | Coq | HOL4 ->
let variant = to_camel_case variant in
if !variant_concatenate_type_name then
@@ -1465,14 +1467,14 @@ let ctx_compute_fun_name_no_suffix (span : Meta.span) (ctx : extraction_ctx)
let fname = ctx_compute_simple_name span ctx fname in
(* TODO: don't convert to snake case for Coq, HOL4, F* *)
let fname = flatten_name fname in
- match !backend with
+ match backend () with
| FStar | Coq | HOL4 -> StringUtils.lowercase_first_letter fname
| Lean -> fname
(** Provided a basename, compute the name of a global declaration. *)
let ctx_compute_global_name (span : Meta.span) (ctx : extraction_ctx)
(name : llbc_name) : string =
- match !Config.backend with
+ match Config.backend () with
| Coq | FStar | HOL4 ->
let parts =
List.map to_snake_case (ctx_compute_simple_name span ctx name)
@@ -1537,7 +1539,7 @@ let ctx_compute_trait_impl_name (ctx : extraction_ctx) (trait_decl : trait_decl)
trait_name_with_generics_to_simple_name ctx.trans_ctx name params args
in
let name = flatten_name name in
- match !backend with
+ match backend () with
| FStar -> StringUtils.lowercase_first_letter name
| Coq | HOL4 | Lean -> name
@@ -1614,7 +1616,7 @@ let ctx_compute_trait_parent_clause_name (ctx : extraction_ctx)
else ctx_compute_trait_decl_name ctx trait_decl ^ "_" ^ clause
in
let clause = clause ^ "Inst" in
- match !backend with
+ match backend () with
| FStar -> StringUtils.lowercase_first_letter clause
| Coq | HOL4 | Lean -> clause
@@ -1633,7 +1635,7 @@ let ctx_compute_trait_type_name (ctx : extraction_ctx) (trait_decl : trait_decl)
can't disambiguate fields coming from different ADTs if they have the same
names), and thus don't need to add a prefix starting with a lowercase.
*)
- match !backend with FStar -> "t" ^ name | Coq | Lean | HOL4 -> name
+ match backend () with FStar -> "t" ^ name | Coq | Lean | HOL4 -> name
let ctx_compute_trait_const_name (ctx : extraction_ctx)
(trait_decl : trait_decl) (item : string) : string =
@@ -1642,7 +1644,7 @@ let ctx_compute_trait_const_name (ctx : extraction_ctx)
else ctx_compute_trait_decl_name ctx trait_decl ^ "_" ^ item
in
(* See [trait_type_name] *)
- match !backend with FStar -> "c" ^ name | Coq | Lean | HOL4 -> name
+ match backend () with FStar -> "c" ^ name | Coq | Lean | HOL4 -> name
let ctx_compute_trait_method_name (ctx : extraction_ctx)
(trait_decl : trait_decl) (item : string) : string =
@@ -1677,7 +1679,7 @@ let ctx_compute_termination_measure_name (span : Meta.span)
let lp_suffix = default_fun_loop_suffix num_loops loop_id in
(* Compute the suffix *)
let suffix =
- match !Config.backend with
+ match Config.backend () with
| FStar -> "_decreases"
| Lean -> "_terminates"
| Coq | HOL4 -> craise __FILE__ __LINE__ span "Unexpected"
@@ -1706,7 +1708,7 @@ let ctx_compute_decreases_proof_name (span : Meta.span) (ctx : extraction_ctx)
let lp_suffix = default_fun_loop_suffix num_loops loop_id in
(* Compute the suffix *)
let suffix =
- match !Config.backend with
+ match Config.backend () with
| Lean -> "_decreases"
| FStar | Coq | HOL4 -> craise __FILE__ __LINE__ span "Unexpected"
in
@@ -1747,7 +1749,7 @@ let ctx_compute_var_basename (span : Meta.span) (ctx : extraction_ctx)
match basename with
| Some basename -> (
(* This should be a no-op *)
- match !Config.backend with
+ match Config.backend () with
| Lean -> basename
| FStar | Coq | HOL4 -> to_snake_case basename)
| None -> (
@@ -1779,7 +1781,7 @@ let ctx_compute_var_basename (span : Meta.span) (ctx : extraction_ctx)
name_from_type_ident (TypesUtils.as_ident cl))
| TVar _ -> (
(* TODO: use "t" also for F* *)
- match !backend with
+ match backend () with
| FStar -> "x" (* lacking inspiration here... *)
| Coq | Lean | HOL4 -> "t" (* lacking inspiration here... *))
| TLiteral lty -> (
@@ -1792,7 +1794,7 @@ let ctx_compute_var_basename (span : Meta.span) (ctx : extraction_ctx)
let ctx_compute_type_var_basename (_ctx : extraction_ctx) (basename : string) :
string =
(* Rust type variables are snake-case and start with a capital letter *)
- match !backend with
+ match backend () with
| FStar ->
(* This is *not* a no-op: this removes the capital letter *)
to_snake_case basename
@@ -1805,7 +1807,7 @@ let ctx_compute_type_var_basename (_ctx : extraction_ctx) (basename : string) :
let ctx_compute_const_generic_var_basename (_ctx : extraction_ctx)
(basename : string) : string =
(* Rust type variables are snake-case and start with a capital letter *)
- match !backend with
+ match backend () with
| FStar | HOL4 ->
(* This is *not* a no-op: this removes the capital letter *)
to_snake_case basename
@@ -1827,7 +1829,7 @@ let ctx_compute_trait_clause_basename (ctx : extraction_ctx)
params.trait_clauses clause_id
in
let clause = clause ^ "Inst" in
- match !backend with
+ match backend () with
| FStar | Coq | HOL4 -> StringUtils.lowercase_first_letter clause
| Lean -> clause
diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index ff936d2f..37b676bb 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -43,13 +43,13 @@ let split_on_separator (s : string) : string list =
Str.split (Str.regexp "\\(::\\|\\.\\)") s
let flatten_name (name : string list) : string =
- match !backend with
+ match backend () with
| FStar | Coq | HOL4 -> String.concat "_" name
| Lean -> String.concat "." name
(** Utility for Lean-only definitions **)
let mk_lean_only (funs : 'a list) : 'a list =
- match !backend with Lean -> funs | _ -> []
+ match backend () with Lean -> funs | _ -> []
let () =
assert (split_on_separator "x::y::z" = [ "x"; "y"; "z" ]);
@@ -61,7 +61,7 @@ let () =
is F*, Coq or HOL4, and a different value if the target is Lean.
*)
let backend_choice (fstar_coq_hol4 : 'a) (lean : 'a) : 'a =
- match !backend with Coq | FStar | HOL4 -> fstar_coq_hol4 | Lean -> lean
+ match backend () with Coq | FStar | HOL4 -> fstar_coq_hol4 | Lean -> lean
let builtin_globals : (string * string) list =
[
@@ -135,9 +135,11 @@ type type_variant_kind =
let mk_struct_constructor (type_name : string) : string =
let prefix =
- match !backend with FStar -> "Mk" | Coq | HOL4 -> "mk" | Lean -> ""
+ match backend () with FStar -> "Mk" | Coq | HOL4 -> "mk" | Lean -> ""
+ in
+ let suffix =
+ match backend () with FStar | Coq | HOL4 -> "" | Lean -> ".mk"
in
- let suffix = match !backend with FStar | Coq | HOL4 -> "" | Lean -> ".mk" in
prefix ^ type_name ^ suffix
(** The assumed types.
@@ -164,7 +166,7 @@ let builtin_types () : builtin_type_info list =
List.map
(fun (rname, name) ->
( rname,
- match !backend with
+ match backend () with
| FStar | Lean -> name
| Coq | HOL4 -> extract_name ^ "_" ^ name ))
fields
@@ -197,7 +199,7 @@ let builtin_types () : builtin_type_info list =
{
rust_name = parse_pattern "core::option::Option";
extract_name =
- (match !backend with
+ (match backend () with
| Lean -> "Option"
| Coq | FStar | HOL4 -> "option");
keep_params = None;
@@ -208,7 +210,7 @@ let builtin_types () : builtin_type_info list =
{
rust_variant_name = "None";
extract_variant_name =
- (match !backend with
+ (match backend () with
| FStar | Coq -> "None"
| Lean -> "none"
| HOL4 -> "NONE");
@@ -217,7 +219,7 @@ let builtin_types () : builtin_type_info list =
{
rust_variant_name = "Some";
extract_variant_name =
- (match !backend with
+ (match backend () with
| FStar | Coq -> "Some"
| Lean -> "some"
| HOL4 -> "SOME");
@@ -529,7 +531,7 @@ let mk_builtin_fun_effects () : (pattern * effect_info) list =
builtin_funs
let mk_builtin_fun_effects_map () =
- NameMatcherMap.of_list (mk_builtin_fun_effects ())
+ NameMatcherMap.of_list (if_backend mk_builtin_fun_effects [])
let builtin_fun_effects_map = mk_memoized mk_builtin_fun_effects_map
@@ -571,7 +573,7 @@ let builtin_trait_decls_info () =
else extract_name ^ "_" ^ item_name
in
let type_name =
- match !backend with
+ match backend () with
| FStar | Coq | HOL4 -> StringUtils.lowercase_first_letter type_name
| Lean -> type_name
in
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index cc0c351d..15e75da2 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -19,12 +19,12 @@ let extract_literal (span : Meta.span) (fmt : F.formatter) (inside : bool)
(cv : literal) : unit =
match cv with
| VScalar sv -> (
- match !backend with
+ match backend () with
| FStar -> F.pp_print_string fmt (Z.to_string sv.value)
| Coq | HOL4 | Lean ->
- let print_brackets = inside && !backend = HOL4 in
+ let print_brackets = inside && backend () = HOL4 in
if print_brackets then F.pp_print_string fmt "(";
- (match !backend with
+ (match backend () with
| Coq | Lean -> ()
| HOL4 ->
F.pp_print_string fmt ("int_to_" ^ int_name sv.int_ty);
@@ -34,7 +34,7 @@ let extract_literal (span : Meta.span) (fmt : F.formatter) (inside : bool)
if sv.value >= Z.of_int 0 then
F.pp_print_string fmt (Z.to_string sv.value)
else F.pp_print_string fmt ("(" ^ Z.to_string sv.value ^ ")");
- (match !backend with
+ (match backend () with
| Coq ->
let iname = int_name sv.int_ty in
F.pp_print_string fmt ("%" ^ iname)
@@ -46,13 +46,13 @@ let extract_literal (span : Meta.span) (fmt : F.formatter) (inside : bool)
if print_brackets then F.pp_print_string fmt ")")
| VBool b ->
let b =
- match !backend with
+ match backend () with
| HOL4 -> if b then "T" else "F"
| Coq | FStar | Lean -> if b then "true" else "false"
in
F.pp_print_string fmt b
| VChar c -> (
- match !backend with
+ match backend () with
| HOL4 ->
(* [#"a"] is a notation for [CHR 97] (97 is the ASCII code for 'a') *)
F.pp_print_string fmt ("#\"" ^ String.make 1 c ^ "\"")
@@ -99,7 +99,7 @@ let extract_unop (span : Meta.span) (extract_expr : bool -> texpression -> unit)
| Cast (src, tgt) -> (
(* HOL4 has a special treatment: because it doesn't support dependent
types, we don't have a specific operator for the cast *)
- match !backend with
+ match backend () with
| HOL4 ->
(* Casting, say, an u32 to an i32 would be done as follows:
{[
@@ -121,7 +121,7 @@ let extract_unop (span : Meta.span) (extract_expr : bool -> texpression -> unit)
(* Different cases depending on the conversion *)
(let cast_str, src, tgt =
let integer_type_to_string (ty : integer_type) : string =
- if !backend = Lean then "." ^ int_name ty
+ if backend () = Lean then "." ^ int_name ty
else
StringUtils.capitalize_first_letter
(PrintPure.integer_type_to_string ty)
@@ -129,20 +129,20 @@ let extract_unop (span : Meta.span) (extract_expr : bool -> texpression -> unit)
match (src, tgt) with
| TInteger src, TInteger tgt ->
let cast_str =
- match !backend with
+ match backend () with
| Coq | FStar -> "scalar_cast"
| Lean -> "Scalar.cast"
| HOL4 -> craise __FILE__ __LINE__ span "Unreachable"
in
let src =
- if !backend <> Lean then Some (integer_type_to_string src)
+ if backend () <> Lean then Some (integer_type_to_string src)
else None
in
let tgt = integer_type_to_string tgt in
(cast_str, src, Some tgt)
| TBool, TInteger tgt ->
let cast_str =
- match !backend with
+ match backend () with
| Coq | FStar -> "scalar_cast_bool"
| Lean -> "Scalar.cast_bool"
| HOL4 -> craise __FILE__ __LINE__ span "Unreachable"
@@ -198,7 +198,7 @@ let extract_binop (span : Meta.span)
(arg0 : texpression) (arg1 : texpression) : unit =
if inside then F.pp_print_string fmt "(";
(* Some binary operations have a special notation depending on the backend *)
- (match (!backend, binop) with
+ (match (backend (), binop) with
| HOL4, (Eq | Ne)
| (FStar | Coq | Lean), (Eq | Lt | Le | Ne | Ge | Gt)
| Lean, (Div | Rem | Add | Sub | Mul | Shl | Shr | BitXor | BitOr | BitAnd) ->
@@ -207,7 +207,7 @@ let extract_binop (span : Meta.span)
| Eq -> "="
| Lt -> "<"
| Le -> "<="
- | Ne -> if !backend = Lean then "!=" else "<>"
+ | Ne -> if backend () = Lean then "!=" else "<>"
| Ge -> ">="
| Gt -> ">"
| Div -> "/"
@@ -225,7 +225,9 @@ let extract_binop (span : Meta.span)
| BitAnd -> "&&&"
in
let binop =
- match !backend with FStar | Lean | HOL4 -> binop | Coq -> "s" ^ binop
+ match backend () with
+ | FStar | Lean | HOL4 -> binop
+ | Coq -> "s" ^ binop
in
extract_expr false arg0;
F.pp_print_space fmt ();
@@ -239,7 +241,7 @@ let extract_binop (span : Meta.span)
(* In the case of F*, for shift operations, because machine integers
are simply integers with a refinement, if the second argument is a
constant we need to provide the second implicit type argument *)
- if binop_is_shift && !backend = FStar && is_const arg1 then (
+ if binop_is_shift && backend () = FStar && is_const arg1 then (
F.pp_print_space fmt ();
let ty = ty_as_integer span arg1.ty in
F.pp_print_string fmt
@@ -275,7 +277,7 @@ let is_empty_record_type_decl_group (dg : Pure.type_decl list) : bool =
*)
let start_fun_decl_group (ctx : extraction_ctx) (fmt : F.formatter)
(is_rec : bool) (dg : Pure.fun_decl list) =
- match !backend with
+ match backend () with
| FStar | Coq | Lean -> ()
| HOL4 ->
(* In HOL4, opaque functions have a special treatment *)
@@ -304,7 +306,7 @@ let start_fun_decl_group (ctx : extraction_ctx) (fmt : F.formatter)
(** See {!start_fun_decl_group}. *)
let end_fun_decl_group (fmt : F.formatter) (is_rec : bool)
(dg : Pure.fun_decl list) =
- match !backend with
+ match backend () with
| FStar -> ()
| Coq ->
(* For aesthetic reasons, we print the Coq end group delimiter directly
@@ -335,7 +337,7 @@ let end_fun_decl_group (fmt : F.formatter) (is_rec : bool)
(** See {!start_fun_decl_group}: similar usage, but for the type declarations. *)
let start_type_decl_group (ctx : extraction_ctx) (fmt : F.formatter)
(is_rec : bool) (dg : Pure.type_decl list) =
- match !backend with
+ match backend () with
| FStar | Coq -> ()
| Lean ->
if is_rec && List.length dg > 1 then (
@@ -362,7 +364,7 @@ let start_type_decl_group (ctx : extraction_ctx) (fmt : F.formatter)
(** See {!start_fun_decl_group}. *)
let end_type_decl_group (fmt : F.formatter) (is_rec : bool)
(dg : Pure.type_decl list) =
- match !backend with
+ match backend () with
| FStar -> ()
| Coq ->
(* For aesthetic reasons, we print the Coq end group delimiter directly
@@ -394,11 +396,11 @@ let end_type_decl_group (fmt : F.formatter) (is_rec : bool)
F.pp_print_break fmt 0 0)
let unit_name () =
- match !backend with Lean -> "Unit" | Coq | FStar | HOL4 -> "unit"
+ match backend () with Lean -> "Unit" | Coq | FStar | HOL4 -> "unit"
(** Small helper *)
let extract_arrow (fmt : F.formatter) () : unit =
- if !Config.backend = Lean then F.pp_print_string fmt "→"
+ if Config.backend () = Lean then F.pp_print_string fmt "→"
else F.pp_print_string fmt "->"
let extract_const_generic (span : Meta.span) (ctx : extraction_ctx)
@@ -441,7 +443,7 @@ let extract_literal_type (_ctx : extraction_ctx) (fmt : F.formatter)
*)
let extract_ty_errors (fmt : F.formatter) : unit =
- match !Config.backend with
+ match Config.backend () with
| FStar | Coq -> F.pp_print_string fmt "admit"
| Lean -> F.pp_print_string fmt "sorry"
| HOL4 -> F.pp_print_string fmt "(* ERROR: could not generate the code *)"
@@ -463,7 +465,7 @@ let rec extract_ty (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
(fun () ->
F.pp_print_space fmt ();
let product =
- match !backend with
+ match backend () with
| FStar -> "&"
| Coq -> "*"
| Lean -> "×"
@@ -480,7 +482,7 @@ let rec extract_ty (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
In HOL4 we would write:
`('a, 'b) tree`
*)
- match !backend with
+ match backend () with
| FStar | Coq | Lean ->
let print_paren = inside && has_params in
if print_paren then F.pp_print_string fmt "(";
@@ -556,7 +558,7 @@ let rec extract_ty (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
type_name ctx
in
let add_brackets (s : string) =
- if !backend = Coq then "(" ^ s ^ ")" else s
+ if backend () = Coq then "(" ^ s ^ ")" else s
in
(* There may be a special treatment depending on the instance id.
See the comments for {!extract_trait_instance_id_with_dot}.
@@ -575,7 +577,9 @@ let rec extract_ty (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_string fmt type_name
| _ ->
(* HOL4 doesn't have 1st class types *)
- cassert __FILE__ __LINE__ (!backend <> HOL4) span
+ cassert __FILE__ __LINE__
+ (backend () <> HOL4)
+ span
"Trait types are not supported yet when generating code for HOL4";
extract_trait_ref span ctx fmt no_params_tys false trait_ref;
F.pp_print_string fmt ("." ^ add_brackets type_name))
@@ -624,14 +628,16 @@ and extract_generic_args (span : Meta.span) (ctx : extraction_ctx)
(fmt : F.formatter) (no_params_tys : TypeDeclId.Set.t)
(generics : generic_args) : unit =
let { types; const_generics; trait_refs } = generics in
- if !backend <> HOL4 then (
+ if backend () <> HOL4 then (
if types <> [] then (
F.pp_print_space fmt ();
Collections.List.iter_link (F.pp_print_space fmt)
(extract_ty span ctx fmt no_params_tys true)
types);
if const_generics <> [] then (
- cassert __FILE__ __LINE__ (!backend <> HOL4) span
+ cassert __FILE__ __LINE__
+ (backend () <> HOL4)
+ span
"Constant generics are not supported yet when generating code for HOL4";
F.pp_print_space fmt ();
Collections.List.iter_link (F.pp_print_space fmt)
@@ -682,7 +688,9 @@ and extract_trait_instance_id_with_dot (span : Meta.span) (ctx : extraction_ctx)
and extract_trait_instance_id (span : Meta.span) (ctx : extraction_ctx)
(fmt : F.formatter) (no_params_tys : TypeDeclId.Set.t) (inside : bool)
(id : trait_instance_id) : unit =
- let add_brackets (s : string) = if !backend = Coq then "(" ^ s ^ ")" else s in
+ let add_brackets (s : string) =
+ if backend () = Coq then "(" ^ s ^ ")" else s
+ in
match id with
| Self ->
(* This has a specific treatment depending on the item we're extracting
@@ -812,7 +820,7 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
in
(* Add the type name prefix for Lean *)
let name =
- if !Config.backend = Lean then
+ if Config.backend () = Lean then
let type_name =
ctx_compute_type_name def.span ctx def.llbc_name
in
@@ -859,7 +867,7 @@ let extract_type_decl_variant (span : Meta.span) (ctx : extraction_ctx)
(* [| Cons :]
* Note that we really don't want any break above so we print everything
* at once. *)
- let opt_colon = if !backend <> HOL4 then " :" else "" in
+ let opt_colon = if backend () <> HOL4 then " :" else "" in
F.pp_print_string fmt ("| " ^ cons_name ^ opt_colon);
let print_field (fid : FieldId.id) (f : field) (ctx : extraction_ctx) :
extraction_ctx =
@@ -871,7 +879,7 @@ let extract_type_decl_variant (span : Meta.span) (ctx : extraction_ctx)
* Note that when printing fields, we register the field names as
* *variables*: they don't need to be unique at the top level. *)
let ctx =
- match !backend with
+ match backend () with
| FStar -> (
match f.field_name with
| None -> ctx
@@ -887,10 +895,10 @@ let extract_type_decl_variant (span : Meta.span) (ctx : extraction_ctx)
| Coq | Lean | HOL4 -> ctx
in
(* Print the field type *)
- let inside = !backend = HOL4 in
+ let inside = backend () = HOL4 in
extract_ty span ctx fmt type_decl_group inside f.field_ty;
(* Print the arrow [->] *)
- if !backend <> HOL4 then (
+ if backend () <> HOL4 then (
F.pp_print_space fmt ();
extract_arrow fmt ());
(* Close the field box *)
@@ -904,9 +912,9 @@ let extract_type_decl_variant (span : Meta.span) (ctx : extraction_ctx)
List.fold_left (fun ctx (fid, f) -> print_field fid f ctx) ctx fields
in
(* Sanity check: HOL4 doesn't support const generics *)
- sanity_check __FILE__ __LINE__ (cg_params = [] || !backend <> HOL4) span;
+ sanity_check __FILE__ __LINE__ (cg_params = [] || backend () <> HOL4) span;
(* Print the final type *)
- if !backend <> HOL4 then (
+ if backend () <> HOL4 then (
F.pp_print_space fmt ();
F.pp_open_hovbox fmt 0;
F.pp_print_string fmt type_name;
@@ -978,7 +986,7 @@ let extract_type_decl_tuple_struct_body (span : Meta.span)
F.pp_print_space fmt ();
F.pp_print_string fmt (unit_name ()))
else
- let sep = match !backend with Coq | FStar | HOL4 -> "*" | Lean -> "×" in
+ let sep = match backend () with Coq | FStar | HOL4 -> "*" | Lean -> "×" in
Collections.List.iter_link
(fun () ->
F.pp_print_space fmt ();
@@ -1049,28 +1057,28 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
(* Note that we already printed: [type t =] *)
let is_rec = decl_is_from_rec_group kind in
let _ =
- if !backend = FStar && fields = [] then (
+ if backend () = FStar && fields = [] then (
F.pp_print_space fmt ();
F.pp_print_string fmt (unit_name ()))
- else if !backend = Lean && fields = [] then ()
+ else if backend () = Lean && fields = [] then ()
(* If the definition is recursive, we may need to extract it as an inductive
(instead of a record). We start with the "normal" case: we extract it
as a record. *)
- else if (not is_rec) || (!backend <> Coq && !backend <> Lean) then (
- if !backend <> Lean then F.pp_print_space fmt ();
+ else if (not is_rec) || (backend () <> Coq && backend () <> Lean) then (
+ if backend () <> Lean then F.pp_print_space fmt ();
(* If Coq: print the constructor name *)
(* TODO: remove superfluous test not is_rec below *)
- if !backend = Coq && not is_rec then (
+ if backend () = Coq && not is_rec then (
F.pp_print_string fmt (ctx_get_struct def.span (TAdtId def.def_id) ctx);
F.pp_print_string fmt " ");
- (match !backend with
+ (match backend () with
| Lean -> ()
| FStar | Coq -> F.pp_print_string fmt "{"
| HOL4 -> F.pp_print_string fmt "<|");
F.pp_print_break fmt 1 ctx.indent_incr;
(* The body itself *)
(* Open a box for the body *)
- (match !backend with
+ (match backend () with
| Coq | FStar | HOL4 -> F.pp_open_hvbox fmt 0
| Lean -> F.pp_open_vbox fmt 0);
(* Print the fields *)
@@ -1085,7 +1093,7 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_string fmt ":";
F.pp_print_space fmt ();
extract_ty def.span ctx fmt type_decl_group false f.field_ty;
- if !backend <> Lean then F.pp_print_string fmt ";";
+ if backend () <> Lean then F.pp_print_string fmt ";";
(* Close the box for the field *)
F.pp_close_box fmt ()
in
@@ -1095,7 +1103,7 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
fields;
(* Close the box for the body *)
F.pp_close_box fmt ();
- match !backend with
+ match backend () with
| Lean -> ()
| FStar | Coq ->
F.pp_print_space fmt ();
@@ -1107,7 +1115,7 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
(* We extract for Coq or Lean, and we have a recursive record, or a record in
a group of mutually recursive types: we extract it as an inductive type *)
cassert __FILE__ __LINE__
- (is_rec && (!backend = Coq || !backend = Lean))
+ (is_rec && (backend () = Coq || backend () = Lean))
def.span
"Constant generics are not supported yet when generating code for HOL4";
(* Small trick: in Lean we use namespaces, meaning we don't need to prefix
@@ -1115,7 +1123,7 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
i.e., instead of generating `inductive Foo := | MkFoo ...` like in Coq
we generate `inductive Foo := | mk ... *)
let cons_name =
- if !backend = Lean then "mk"
+ if backend () = Lean then "mk"
else ctx_get_struct def.span (TAdtId def.def_id) ctx
in
let def_name = ctx_get_local_type def.span def.def_id ctx in
@@ -1128,7 +1136,7 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
let extract_comment (fmt : F.formatter) (sl : string list) : unit =
(* Delimiters, space after we break a line *)
let ld, space, rd =
- match !backend with
+ match backend () with
| Coq | FStar | HOL4 -> ("(** ", 4, " *)")
| Lean -> ("/- ", 3, " -/")
in
@@ -1223,18 +1231,18 @@ let extract_generic_params (span : Meta.span) (ctx : extraction_ctx)
let all_params = List.concat [ type_params; cg_params; trait_clauses ] in
(* HOL4 doesn't support const generics *)
cassert __FILE__ __LINE__
- (cg_params = [] || !backend <> HOL4)
+ (cg_params = [] || backend () <> HOL4)
span "Constant generics are not supported yet when generating code for HOL4";
let left_bracket (implicit : bool) =
- if implicit && !backend <> FStar then F.pp_print_string fmt "{"
+ if implicit && backend () <> FStar then F.pp_print_string fmt "{"
else F.pp_print_string fmt "("
in
let right_bracket (implicit : bool) =
- if implicit && !backend <> FStar then F.pp_print_string fmt "}"
+ if implicit && backend () <> FStar then F.pp_print_string fmt "}"
else F.pp_print_string fmt ")"
in
let print_implicit_symbol (implicit : bool) =
- if implicit && !backend = FStar then F.pp_print_string fmt "#" else ()
+ if implicit && backend () = FStar then F.pp_print_string fmt "#" else ()
in
let insert_req_space () =
match space with
@@ -1254,7 +1262,7 @@ let extract_generic_params (span : Meta.span) (ctx : extraction_ctx)
(const_generics : const_generic_var list)
(trait_clauses : trait_clause list) : unit =
(* Note that in HOL4 we don't print the type parameters. *)
- if !backend <> HOL4 then (
+ if backend () <> HOL4 then (
(* Print the type parameters *)
if type_params <> [] then (
insert_req_space ();
@@ -1372,7 +1380,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
(type_decl_group : TypeDeclId.Set.t) (kind : decl_kind) (def : type_decl)
(extract_body : bool) : unit =
(* Sanity check *)
- sanity_check __FILE__ __LINE__ (extract_body || !backend <> HOL4) def.span;
+ sanity_check __FILE__ __LINE__ (extract_body || backend () <> HOL4) def.span;
let is_tuple_struct =
TypesUtils.type_decl_from_decl_id_is_tuple_struct
ctx.trans_ctx.type_ctx.type_infos def.def_id
@@ -1397,7 +1405,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
The boolean [is_opaque_coq] is used to detect this case.
*)
let is_opaque = type_kind = None in
- let is_opaque_coq = !backend = Coq && is_opaque in
+ let is_opaque_coq = backend () = Coq && is_opaque in
let use_forall = is_opaque_coq && def.generics <> empty_generic_params in
(* Retrieve the definition name *)
let def_name = ctx_get_local_type def.span def.def_id ctx in
@@ -1408,7 +1416,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
ctx
in
(* Add a break before *)
- if !backend <> HOL4 || not (decl_is_first_from_group kind) then
+ if backend () <> HOL4 || not (decl_is_first_from_group kind) then
F.pp_print_break fmt 0 0;
(* Print a comment to link the extracted type to its original rust definition *)
(let name =
@@ -1423,7 +1431,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
(* Open a box for the definition, so that whenever possible it gets printed on
* one line. Note however that in the case of Lean line breaks are important
* for parsing: we thus use a hovbox. *)
- (match !backend with
+ (match backend () with
| Coq | FStar | HOL4 -> F.pp_open_hvbox fmt 0
| Lean ->
if is_tuple_struct then F.pp_open_hvbox fmt 0 else F.pp_open_vbox fmt 0);
@@ -1433,7 +1441,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
We need this annotation, otherwise Lean sometimes doesn't manage to typecheck
the expressions when it needs to coerce the type.
*)
- if is_tuple_struct_one_or_zero_field && !backend = Lean then (
+ if is_tuple_struct_one_or_zero_field && backend () = Lean then (
F.pp_print_string fmt "@[reducible]";
F.pp_print_space fmt ())
else ();
@@ -1445,7 +1453,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
(* HOL4 doesn't support const generics, and type definitions in HOL4 don't
support trait clauses *)
cassert __FILE__ __LINE__
- ((cg_params = [] && trait_clauses = []) || !backend <> HOL4)
+ ((cg_params = [] && trait_clauses = []) || backend () <> HOL4)
def.span
"Constant generics and type definitions with trait clauses are not \
supported yet when generating code for HOL4";
@@ -1456,7 +1464,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
if extract_body then (
F.pp_print_space fmt ();
let eq =
- match !backend with
+ match backend () with
| FStar -> "="
| Coq ->
(* For Coq, the `*` is overloaded. If we want to extract a product
@@ -1493,10 +1501,10 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
type_params cg_params variants
| Opaque -> craise __FILE__ __LINE__ def.span "Unreachable");
(* Add the definition end delimiter *)
- if !backend = HOL4 && decl_is_not_last_from_group kind then (
+ if backend () = HOL4 && decl_is_not_last_from_group kind then (
F.pp_print_space fmt ();
F.pp_print_string fmt ";")
- else if !backend = Coq && decl_is_last_from_group kind then (
+ else if backend () = Coq && decl_is_last_from_group kind then (
(* This is actually an end of group delimiter. For aesthetic reasons
we print it here instead of in {!end_type_decl_group}. *)
F.pp_print_cut fmt ();
@@ -1504,7 +1512,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
(* Close the box for the definition *)
F.pp_close_box fmt ();
(* Add breaks to insert new lines between definitions *)
- if !backend <> HOL4 || decl_is_not_last_from_group kind then
+ if backend () <> HOL4 || decl_is_not_last_from_group kind then
F.pp_print_break fmt 0 0
(** Extract an opaque type declaration to HOL4.
@@ -1572,11 +1580,11 @@ let extract_type_decl (ctx : extraction_ctx) (fmt : F.formatter)
| Assumed | Declared -> false
in
if extract_body then
- if !backend = HOL4 && is_empty_record_type_decl def then
+ if backend () = HOL4 && is_empty_record_type_decl def then
extract_type_decl_hol4_empty_record ctx fmt def
else extract_type_decl_gen ctx fmt type_decl_group kind def extract_body
else
- match !backend with
+ match backend () with
| FStar | Coq | Lean ->
extract_type_decl_gen ctx fmt type_decl_group kind def extract_body
| HOL4 -> extract_type_decl_hol4_opaque ctx fmt def
@@ -1625,7 +1633,7 @@ let extract_coq_arguments_instruction (ctx : extraction_ctx) (fmt : F.formatter)
*)
let extract_type_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter)
(kind : decl_kind) (decl : type_decl) : unit =
- sanity_check __FILE__ __LINE__ (!backend = Coq) decl.span;
+ sanity_check __FILE__ __LINE__ (backend () = Coq) decl.span;
(* Generating the [Arguments] instructions is useful only if there are parameters *)
let num_params =
List.length decl.generics.types
@@ -1674,7 +1682,9 @@ let extract_type_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter)
*)
let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
(fmt : F.formatter) (kind : decl_kind) (decl : type_decl) : unit =
- sanity_check __FILE__ __LINE__ (!backend = Coq || !backend = Lean) decl.span;
+ sanity_check __FILE__ __LINE__
+ (backend () = Coq || backend () = Lean)
+ decl.span;
match decl.kind with
| Opaque | Enum _ -> ()
| Struct fields ->
@@ -1704,7 +1714,7 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
F.pp_open_hvbox fmt ctx.indent_incr;
(* For Lean: add some attributes *)
- if !backend = Lean then (
+ if backend () = Lean then (
(* Box for the attributes *)
F.pp_open_vbox fmt 0;
(* Annotate the projectors with both simp and reducible.
@@ -1717,7 +1727,7 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
(* Box for the [def ADT.proj ... :=] *)
F.pp_open_hovbox fmt ctx.indent_incr;
- (match !backend with
+ (match backend () with
| Lean -> F.pp_print_string fmt "def"
| Coq -> F.pp_print_string fmt "Definition"
| _ -> internal_error __FILE__ __LINE__ decl.span);
@@ -1729,7 +1739,7 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
let field_name =
ctx_get_field decl.span (TAdtId decl.def_id) field_id ctx
in
- if !backend = Lean then (
+ if backend () = Lean then (
F.pp_print_string fmt def_name;
F.pp_print_string fmt ".");
F.pp_print_string fmt field_name;
@@ -1795,7 +1805,7 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
F.pp_close_box fmt ();
(* Print the [end] *)
- if !backend = Coq then (
+ if backend () = Coq then (
F.pp_print_space fmt ();
F.pp_print_string fmt "end");
@@ -1804,7 +1814,7 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
(* Close the inner box projector *)
F.pp_close_box fmt ();
(* If Coq: end the definition with a "." *)
- if !backend = Coq then (
+ if backend () = Coq then (
F.pp_print_cut fmt ();
F.pp_print_string fmt ".");
(* Close the outer box for projector definition *)
@@ -1842,7 +1852,7 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
(* Close the inner box projector *)
F.pp_close_box fmt ();
(* If Coq: end the definition with a "." *)
- if !backend = Coq then (
+ if backend () = Coq then (
F.pp_print_cut fmt ();
F.pp_print_string fmt ".");
(* Close the outer box projector *)
@@ -1854,7 +1864,7 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
let extract_field_proj_and_notation (field_id : FieldId.id)
(field : field) : unit =
extract_field_proj field_id field;
- if !backend = Coq then extract_proj_notation field_id field
+ if backend () = Coq then extract_proj_notation field_id field
in
FieldId.iteri extract_field_proj_and_notation fields
@@ -1866,7 +1876,7 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
*)
let extract_type_decl_extra_info (ctx : extraction_ctx) (fmt : F.formatter)
(kind : decl_kind) (decl : type_decl) : unit =
- match !backend with
+ match backend () with
| FStar | HOL4 -> ()
| Lean | Coq ->
if
@@ -1874,7 +1884,8 @@ let extract_type_decl_extra_info (ctx : extraction_ctx) (fmt : F.formatter)
(TypesUtils.type_decl_from_decl_id_is_tuple_struct
ctx.trans_ctx.type_ctx.type_infos decl.def_id)
then (
- if !backend = Coq then extract_type_decl_coq_arguments ctx fmt kind decl;
+ if backend () = Coq then
+ extract_type_decl_coq_arguments ctx fmt kind decl;
extract_type_decl_record_field_projectors ctx fmt kind decl)
(** Extract the state type declaration. *)
@@ -1893,7 +1904,7 @@ let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx)
(* The syntax for Lean and Coq is almost identical. *)
let print_axiom () =
let axiom =
- match !backend with
+ match backend () with
| Coq -> "Axiom"
| Lean -> "axiom"
| FStar | HOL4 -> raise (Failure "Unexpected")
@@ -1905,14 +1916,14 @@ let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx)
F.pp_print_string fmt ":";
F.pp_print_space fmt ();
F.pp_print_string fmt "Type";
- if !backend = Coq then F.pp_print_string fmt "."
+ if backend () = Coq then F.pp_print_string fmt "."
in
(* The kind should be [Assumed] or [Declared] *)
(match kind with
| SingleNonRec | SingleRec | MutRecFirst | MutRecInner | MutRecLast ->
raise (Failure "Unexpected")
| Assumed -> (
- match !backend with
+ match backend () with
| FStar ->
F.pp_print_string fmt "assume";
F.pp_print_space fmt ();
@@ -1927,7 +1938,7 @@ let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx)
F.pp_print_string fmt ("val _ = new_type (\"" ^ state_name ^ "\", 0)")
| Coq | Lean -> print_axiom ())
| Declared -> (
- match !backend with
+ match backend () with
| FStar ->
F.pp_print_string fmt "val";
F.pp_print_space fmt ();
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index fb3701f3..b2e55841 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -362,6 +362,11 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
ctx)
else ctx
in
+ log#ldebug
+ (lazy
+ ("evaluate_function_symbolic_synthesize_backward_from_return: (after \
+ putting the return value in the proper abstraction)\n" ^ "\n- ctx:\n"
+ ^ Print.Contexts.eval_ctx_to_string ~span:(Some fdef.item_meta.span) ctx));
(* We now need to end the proper *input* abstractions - pay attention
* to the fact that we end the *input* abstractions, not the *return*
@@ -418,7 +423,28 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
}
]}
*)
- (None, false)
+ (* If we are borrow-checking: end the synth input abstraction to
+ check there is no borrow-checking issue.
+ Otherwise, do nothing.
+
+ We need this check because of the following:
+ {[
+ fn loop_reborrow_mut1<'a, 'b>(a: &'a mut u32, b: &'b mut u32) -> &'a mut u32 {
+ let mut x = 0;
+ while x > 0 {
+ x += 1;
+ }
+ if x > 0 {
+ a
+ } else {
+ b // Failure
+ }
+ }
+ ]}
+ (remark: this is slightly ad-hoc, and we won't need to do that
+ once we make the handling of loops more general).
+ *)
+ if !Config.borrow_check then (Some fun_abs_id, true) else (None, false)
| Some abs -> (Some abs.abs_id, false)
in
log#ldebug
@@ -489,9 +515,13 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
- the list of symbolic values introduced for the input values (this is
useful for the synthesis)
- the symbolic AST generated by the symbolic execution
+
+ If [synthesize] is [true]: we synthesize the symbolic AST that is used for
+ the translation. Otherwise, we do not (the symbolic execution then simply
+ borrow-checks the function).
*)
-let evaluate_function_symbolic (ctx : decls_ctx) (fdef : fun_decl) :
- symbolic_value list * SA.expression =
+let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
+ (fdef : fun_decl) : symbolic_value list * SA.expression option =
(* Debug *)
let name_to_string () =
Print.Types.name_to_string
@@ -616,8 +646,10 @@ let evaluate_function_symbolic (ctx : decls_ctx) (fdef : fun_decl) :
eval_function_body config (Option.get fdef.body).body ctx
in
let el = List.map (fun (ctx, res) -> finish res ctx) ctx_resl in
- cc el
- with CFailure (span, msg) -> Error (span, msg)
+ (* Finish synthesizing *)
+ if synthesize then Some (cc el) else None
+ with CFailure (span, msg) ->
+ if synthesize then Some (Error (span, msg)) else None
in
(* Return *)
(input_svs, symbolic)
diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml
index 735f3743..3760d15a 100644
--- a/compiler/InterpreterLoopsFixedPoint.ml
+++ b/compiler/InterpreterLoopsFixedPoint.ml
@@ -665,8 +665,8 @@ let compute_loop_entry_fixed_point (config : config) (span : Meta.span)
in
List.iter end_at_return (fst (eval_loop_body fp));
- (* Check that the sets of abstractions we need to end per region group are pairwise
- * disjoint *)
+ (* Check that the sets of abstractions we need to end per region group are
+ pairwise disjoint *)
let aids_union = ref AbstractionId.Set.empty in
let _ =
RegionGroupId.Map.iter
@@ -680,10 +680,13 @@ let compute_loop_entry_fixed_point (config : config) (span : Meta.span)
!fp_ended_aids
in
- (* We also check that all the regions need to end - this is not necessary per
- se, but if it doesn't happen it is bizarre and worth investigating... *)
+ (* If we generate a translation, we check that all the regions need to end
+ - this is not necessary per se, but if it doesn't happen it is bizarre and worth investigating...
+ We need this check for now for technical reasons to make the translation work.
+ If we only borrow-check, we can ignore this.
+ *)
sanity_check __FILE__ __LINE__
- (AbstractionId.Set.equal !aids_union !fp_aids)
+ (!Config.borrow_check || AbstractionId.Set.equal !aids_union !fp_aids)
span;
(* Merge the abstractions which need to be merged, and compute the map from
@@ -779,9 +782,11 @@ let compute_loop_entry_fixed_point (config : config) (span : Meta.span)
no region group, and we set them as endable just above).
If [remove_rg_id] is [false], we simply set the abstractions as non-endable
- to freeze them (we will use the fixed point as starting point for the
- symbolic execution of the loop body, and we have to make sure the input
- abstractions are frozen).
+ **when generating a pure translation** to freeze them (we will use the
+ fixed point as starting point for the symbolic execution of the loop body,
+ and we have to make sure the input abstractions are frozen).
+ If we are simply borrow-checking the program, we can set the abstraction
+ as endable.
*)
let update_loop_abstractions (remove_rg_id : bool) =
object
@@ -796,7 +801,13 @@ let compute_loop_entry_fixed_point (config : config) (span : Meta.span)
if remove_rg_id then Loop (loop_id, None, LoopSynthInput)
else abs.kind
in
- { abs with can_end = remove_rg_id; kind }
+ (* If we borrow check we can always set the abstraction as
+ endable. If we generate a pure translation we have a few
+ more constraints. *)
+ let can_end =
+ if !Config.borrow_check then true else remove_rg_id
+ in
+ { abs with can_end; kind }
| _ -> abs
end
in
diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml
index 3f7c023e..a1c0841a 100644
--- a/compiler/InterpreterLoopsMatchCtxs.ml
+++ b/compiler/InterpreterLoopsMatchCtxs.ml
@@ -1956,7 +1956,10 @@ let match_ctx_with_target (config : config) (span : Meta.span)
| Loop (loop_id', rg_id, kind) ->
sanity_check __FILE__ __LINE__ (loop_id' = loop_id) span;
sanity_check __FILE__ __LINE__ (kind = LoopSynthInput) span;
- let can_end = false in
+ (* If we borrow-check: we can set the abstractions as endable.
+ If we synthesize we have to constrain the region abstractions
+ a bit. *)
+ let can_end = !Config.borrow_check in
let kind : abs_kind = Loop (loop_id, rg_id, LoopCall) in
let abs = { abs with kind; can_end } in
super#visit_abs env abs
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index 8a924a0a..992146de 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -250,12 +250,16 @@ let rec access_projection (span : Meta.span) (access : projection_access)
Ok (ctx, { res with updated = nv })
else Error (FailSharedLoan bids))
| (_, (VLiteral _ | VAdt _ | VBottom | VBorrow _), _) as r ->
- let pe, v, ty = r in
- let pe = "- pe: " ^ show_projection_elem pe in
- let v = "- v:\n" ^ show_value v in
- let ty = "- ty:\n" ^ show_ety ty in
- craise __FILE__ __LINE__ span
- ("Inconsistent projection:\n" ^ pe ^ "\n" ^ v ^ "\n" ^ ty))
+ if v.value = VBottom then
+ craise __FILE__ __LINE__ span
+ "Can not apply a projection to the ⊥ value"
+ else
+ let pe, v, ty = r in
+ let pe = "- pe: " ^ show_projection_elem pe in
+ let v = "- v:\n" ^ show_value v in
+ let ty = "- ty:\n" ^ show_ety ty in
+ craise __FILE__ __LINE__ span
+ ("Inconsistent projection:\n" ^ pe ^ "\n" ^ v ^ "\n" ^ ty))
(** Generic function to access (read/write) the value at a given place.
diff --git a/compiler/Logging.ml b/compiler/Logging.ml
index 9b8019b2..620c5fb5 100644
--- a/compiler/Logging.ml
+++ b/compiler/Logging.ml
@@ -15,6 +15,9 @@ let regions_hierarchy_log = L.get_logger "MainLogger.RegionsHierarchy"
(** Logger for Translate *)
let translate_log = L.get_logger "MainLogger.Translate"
+(** Logger for BorrowCheck *)
+let borrow_check_log = L.get_logger "MainLogger.BorrowCheck"
+
(** Logger for Contexts *)
let contexts_log = L.get_logger "MainLogger.Contexts"
diff --git a/compiler/Main.ml b/compiler/Main.ml
index 29322049..1bf9196a 100644
--- a/compiler/Main.ml
+++ b/compiler/Main.ml
@@ -68,9 +68,13 @@ let () =
let spec_ls =
[
+ ( "-borrow-check",
+ Arg.Set borrow_check,
+ " Only borrow-check the program and do not generate any translation" );
( "-backend",
Arg.Symbol (backend_names, set_backend),
- " Specify the target backend" );
+ " Specify the target backend (" ^ String.concat ", " backend_names ^ ")"
+ );
("-dest", Arg.Set_string dest_dir, " Specify the output directory");
( "-test-units",
Arg.Set test_unit_functions,
@@ -137,6 +141,12 @@ let () =
let check_arg_name name =
assert (List.exists (fun (n, _, _) -> n = name) spec_ls)
in
+
+ let fail_with_error (msg : string) =
+ log#serror msg;
+ fail ()
+ in
+
let check_arg_implies (arg0 : bool) (name0 : string) (arg1 : bool)
(name1 : string) : unit =
check_arg_name name0;
@@ -160,6 +170,14 @@ let () =
fail ())
in
+ let check (cond : bool) (msg : string) =
+ if not cond then fail_with_error msg
+ in
+
+ let check_not (cond : bool) (msg : string) =
+ if cond then fail_with_error msg
+ in
+
if !print_llbc then main_log#set_level EL.Debug;
(* Sanity check (now that the arguments are parsed!): -template-clauses ==> decrease-clauses *)
@@ -176,44 +194,63 @@ let () =
check_arg_implies
(not !generate_lib_entry_point)
"-no-gen-lib-entry" !split_files "-split-files";
- if !lean_gen_lakefile && not (!backend = Lean) then
- log#error
+ if !lean_gen_lakefile && not (backend () = Lean) then
+ fail_with_error
"The -lean-default-lakefile option is valid only for the Lean backend";
+ if !borrow_check then (
+ check (!dest_dir = "") "Options -borrow-check and -dest are not compatible";
+ check_not !split_files
+ "Options -borrow-check and -split-files are not compatible";
+ check_not !test_unit_functions
+ "Options -borrow-check and -test-unit-functions are not compatible";
+ check_not !test_trans_unit_functions
+ "Options -borrow-check and -test-trans-units are not compatible";
+ check_not !extract_decreases_clauses
+ "Options -borrow-check and -decreases-clauses are not compatible";
+ check_not !use_state
+ "Options -borrow-check and -use-state are not compatible";
+ check_not !use_fuel "Options -borrow-check and -use-fuel are not compatible";
+ check_not !split_files
+ "Options -borrow-check and -split-files are not compatible");
+
(* Check that the user specified a backend *)
let _ =
match !opt_backend with
- | Some b -> backend := b
+ | Some _ ->
+ check_not !borrow_check
+ "Arguments `-backend` and `-borrow-check` are not compatible"
| None ->
- log#error "Backend not specified (use the `-backend` argument)";
- fail ()
+ check !borrow_check "Missing `-backend` or `-borrow-check` argument"
in
(* Set some options depending on the backend *)
let _ =
- match !backend with
- | FStar ->
- (* 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 ->
- (* 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;
- (* 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 (
- log#error "The HOL4 backend doesn't support the -use-fuel option";
- fail ())
+ match !opt_backend with
+ | None -> ()
+ | Some backend -> (
+ match backend with
+ | FStar ->
+ (* 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 ->
+ (* We don't support fuel for the Lean backend *)
+ check_not !use_fuel
+ "The Lean backend doesn't support the -use-fuel option";
+ (* Lean can disambiguate the field names *)
+ 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 (
+ log#error "The HOL4 backend doesn't support the -use-fuel option";
+ fail ()))
in
(* Retrieve and check the filename *)
@@ -251,7 +288,7 @@ let () =
(* We don't support mutually recursive definitions with decreases clauses in Lean *)
if
- !backend = Lean && !extract_decreases_clauses
+ !opt_backend = Some Lean && !extract_decreases_clauses
&& List.exists
(function
| Aeneas.LlbcAst.FunGroup (RecGroup (_ :: _)) -> true
@@ -272,8 +309,9 @@ let () =
(* Test the unit functions with the concrete interpreter *)
if !test_unit_functions then Test.test_unit_functions m;
- (* Translate the functions *)
- Aeneas.Translate.translate_crate filename dest_dir m
+ (* Translate or borrow-check the crate *)
+ if !borrow_check then Aeneas.BorrowCheck.borrow_check_crate m
+ else Aeneas.Translate.translate_crate filename dest_dir m
with Errors.CFailure (_, _) ->
(* In theory it shouldn't happen, but there may be uncaught errors -
note that we let the [Failure] exceptions go through (they are
@@ -286,7 +324,9 @@ let () =
(* Reverse the list of error messages so that we print them from the
earliest to the latest. *)
(List.rev !Errors.error_list);
- exit 1);
+ exit 1)
+ else if !borrow_check then
+ log#linfo (lazy "Crate successfully borrow-checked");
(* Print total elapsed time *)
log#linfo
diff --git a/compiler/Print.ml b/compiler/Print.ml
index 7495d6bf..8bd709d0 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -309,13 +309,14 @@ module Values = struct
let kind =
if verbose then "[kind:" ^ abs_kind_to_string abs.kind ^ "]" else ""
in
+ let can_end = if abs.can_end then "{endable}" else "{frozen}" in
indent ^ "abs@"
^ AbstractionId.to_string abs.abs_id
^ kind ^ "{parents="
^ AbstractionId.Set.to_string None abs.parents
^ "}" ^ "{regions="
^ RegionId.Set.to_string None abs.regions
- ^ "}" ^ " {\n" ^ avs ^ "\n" ^ indent ^ "}"
+ ^ "}" ^ can_end ^ " {\n" ^ avs ^ "\n" ^ indent ^ "}"
let inst_fun_sig_to_string (env : fmt_env) (sg : LlbcAst.inst_fun_sig) :
string =
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index a4319b28..a22a39ab 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -649,7 +649,7 @@ let intro_struct_updates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
(* Convert, if possible - note that for now for Lean and Coq
we don't support the structure syntax on recursive structures *)
if
- (!Config.backend <> Lean && !Config.backend <> Coq)
+ (Config.backend () <> Lean && Config.backend () <> Coq)
|| not is_rec
then
let struct_id = TAdtId adt_id in
@@ -1295,7 +1295,7 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
the shape [{ x with f := v }]).
This is not supported by Coq *)
- !Config.backend <> Coq
+ Config.backend () <> Coq
then (
(* Compute the number of occurrences of each variable *)
let occurs = ref VarId.Map.empty in
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index e7dcd933..fe5d3414 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -241,7 +241,7 @@ let rec let_group_requires_parentheses (span : Meta.span) (e : texpression) :
msg (* TODO : check if true should'nt be returned instead ? *)
let texpression_requires_parentheses span e =
- match !Config.backend with
+ match Config.backend () with
| FStar | Lean -> false
| Coq | HOL4 -> let_group_requires_parentheses span e
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 848bfe50..ba6bba68 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -3693,7 +3693,7 @@ let wrap_in_match_fuel (span : Meta.span) (fuel0 : VarId.id) (fuel : VarId.id)
let fail_branch =
mk_result_fail_texpression_with_error_id span error_out_of_fuel_id body.ty
in
- match !Config.backend with
+ match Config.backend () with
| FStar ->
(* Generate an expression:
{[
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 0f887ec8..2bc9bb25 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -31,8 +31,9 @@ let translate_function_to_symbolics (trans_ctx : trans_ctx) (fdef : fun_decl) :
| None -> None
| Some _ ->
(* Evaluate *)
- let inputs, symb = evaluate_function_symbolic trans_ctx fdef in
- Some (inputs, symb)
+ let synthesize = true in
+ let inputs, symb = evaluate_function_symbolic synthesize trans_ctx fdef in
+ Some (inputs, Option.get symb)
(** Translate a function, by generating its forward and backward translations.
@@ -665,7 +666,7 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config)
let extract_decrease decl =
let has_decr_clause = has_decreases_clause decl in
if has_decr_clause then
- match !Config.backend with
+ match Config.backend () with
| Lean ->
Extract.extract_template_lean_termination_and_decreasing ctx
fmt decl
@@ -864,7 +865,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
* internal count is consistent with the state of the file.
*)
(* Create the header *)
- (match !Config.backend with
+ (match Config.backend () with
| Lean ->
Printf.fprintf out "-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS\n";
Printf.fprintf out "-- [%s]%s\n" fi.rust_module_name fi.custom_msg
@@ -873,7 +874,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
"(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)\n";
Printf.fprintf out "(** [%s]%s *)\n" fi.rust_module_name fi.custom_msg);
(* Generate the imports *)
- (match !Config.backend with
+ (match Config.backend () with
| FStar ->
Printf.fprintf out "module %s\n" fi.module_name;
Printf.fprintf out "open Primitives\n";
@@ -957,7 +958,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
Format.pp_print_newline fmt ();
(* Close the module *)
- (match !Config.backend with
+ (match Config.backend () with
| FStar -> ()
| Lean -> if fi.in_namespace then Printf.fprintf out "end %s\n" fi.namespace
| HOL4 -> Printf.fprintf out "val _ = export_theory ()\n"
@@ -1039,7 +1040,8 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
trans_ctx;
names_maps;
indent_incr = 2;
- use_dep_ite = !Config.backend = Lean && !Config.extract_decreases_clauses;
+ use_dep_ite =
+ Config.backend () = Lean && !Config.extract_decreases_clauses;
trait_decl_id = None (* None by default *);
is_provided_method = false (* false by default *);
trans_trait_decls;
@@ -1113,13 +1115,13 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
(* Convert the case *)
let crate_name = StringUtils.to_camel_case basename in
let crate_name =
- if !Config.backend = HOL4 then
+ if Config.backend () = HOL4 then
StringUtils.lowercase_first_letter crate_name
else crate_name
in
(* We use the raw crate name for the namespaces *)
let namespace =
- match !Config.backend with
+ match Config.backend () with
| FStar | Coq | HOL4 -> crate.name
| Lean -> crate.name
in
@@ -1144,7 +1146,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
(* Lean reflects the module hierarchy within the filesystem, so we need to
create more directories *)
- if !Config.backend = Lean then (
+ if Config.backend () = Lean then (
let ( ^^ ) = Filename.concat in
if !Config.split_files then mkdir_if (dest_dir ^^ crate_name);
if needs_clauses_module then (
@@ -1156,7 +1158,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
(* Retrieve the executable's directory *)
let exe_dir = Filename.dirname Sys.argv.(0) in
let primitives_src_dest =
- match !Config.backend with
+ match Config.backend () with
| FStar -> Some ("/backends/fstar/Primitives.fst", "Primitives.fst")
| Coq -> Some ("/backends/coq/Primitives.v", "Primitives.v")
| Lean -> None
@@ -1190,18 +1192,18 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
(* Extract the file(s) *)
let module_delimiter =
- match !Config.backend with
+ match Config.backend () with
| FStar -> "."
| Coq -> "_"
| Lean -> "."
| HOL4 -> "_"
in
let file_delimiter =
- if !Config.backend = Lean then "/" else module_delimiter
+ if Config.backend () = Lean then "/" else module_delimiter
in
(* File extension for the "regular" modules *)
let ext =
- match !Config.backend with
+ match Config.backend () with
| FStar -> ".fst"
| Coq -> ".v"
| Lean -> ".lean"
@@ -1209,7 +1211,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
in
(* File extension for the opaque module *)
let opaque_ext =
- match !Config.backend with
+ match Config.backend () with
| FStar -> ".fsti"
| Coq -> ".v"
| Lean -> ".lean"
@@ -1253,7 +1255,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
For the other backends, we generate a template file as a model
for the file the user has to provide. *)
let module_suffix, opaque_imported_suffix, custom_msg =
- match !Config.backend with
+ match Config.backend () with
| FStar ->
("TypesExternal", "TypesExternal", ": external type declarations")
| HOL4 | Coq | Lean ->
@@ -1306,7 +1308,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
(* Extract the non opaque types *)
let types_filename_ext =
- match !Config.backend with
+ match Config.backend () with
| FStar -> ".fst"
| Coq -> ".v"
| Lean -> ".lean"
@@ -1377,7 +1379,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
For the other backends, we generate a template file as a model
for the file the user has to provide. *)
let module_suffix, opaque_imported_suffix, custom_msg =
- match !Config.backend with
+ match Config.backend () with
| FStar ->
( "FunsExternal",
"FunsExternal",
@@ -1445,7 +1447,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
let clauses_module =
if needs_clauses_module then
let clauses_submodule =
- if !Config.backend = Lean then module_delimiter ^ "Clauses" else ""
+ if Config.backend () = Lean then module_delimiter ^ "Clauses" else ""
in
[ crate_name ^ clauses_submodule ^ module_delimiter ^ "Clauses" ]
else []
@@ -1501,7 +1503,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
extract_file gen_config ctx file_info);
(* Generate the build file *)
- match !Config.backend with
+ match Config.backend () with
| Coq | FStar | HOL4 ->
()
(* Nothing to do - TODO: we might want to generate the _CoqProject file for Coq.
diff --git a/compiler/dune b/compiler/dune
index 6bdfd153..f987faec 100644
--- a/compiler/dune
+++ b/compiler/dune
@@ -14,6 +14,7 @@
(modules
AssociatedTypes
Assumed
+ BorrowCheck
Collections
Config
ConstStrings
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-22 15:36:55 +0000