diff options
author | Son Ho | 2024-06-05 14:32:19 +0200 |
---|---|---|
committer | Son Ho | 2024-06-05 14:32:19 +0200 |
commit | 35c6b1c3c3dbd1b782cb00206c773021f5c74765 (patch) | |
tree | c103860afdc8c24c16ac8bbf1c705e956bf5a16a /compiler | |
parent | baa0771885546816461e063131162b94c6954d86 (diff) |
Add an option to run Aeneas as a borrow checker
Diffstat (limited to '')
-rw-r--r-- | compiler/Config.ml | 22 | ||||
-rw-r--r-- | compiler/Extract.ml | 185 | ||||
-rw-r--r-- | compiler/ExtractBase.ml | 72 | ||||
-rw-r--r-- | compiler/ExtractBuiltin.ml | 24 | ||||
-rw-r--r-- | compiler/ExtractTypes.ml | 173 | ||||
-rw-r--r-- | compiler/Main.ml | 97 | ||||
-rw-r--r-- | compiler/PureMicroPasses.ml | 4 | ||||
-rw-r--r-- | compiler/PureUtils.ml | 2 | ||||
-rw-r--r-- | compiler/SymbolicToPure.ml | 2 | ||||
-rw-r--r-- | compiler/Translate.ml | 37 |
10 files changed, 342 insertions, 276 deletions
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..3346c328 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,7 +843,7 @@ let keywords () = named_binops in let misc = - match !backend with + match backend () with | FStar -> [ "assert"; @@ -1042,7 +1042,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 +1051,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 +1065,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 +1076,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 +1123,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 +1146,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 +1258,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 +1307,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 +1342,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 +1391,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 +1425,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 +1435,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 +1465,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 +1537,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 +1614,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 +1633,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 +1642,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 +1677,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 +1706,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 +1747,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 +1779,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 +1792,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 +1805,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 +1827,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/Main.ml b/compiler/Main.ml index 29322049..557a3993 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 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..690bff5c 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -665,7 +665,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 +864,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 +873,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 +957,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 +1039,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 +1114,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 +1145,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 +1157,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 +1191,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 +1210,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 +1254,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 +1307,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 +1378,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 +1446,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 +1502,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. |