diff options
| author | Son HO | 2024-06-06 09:15:22 +0200 |
|---|---|---|
| committer | GitHub | 2024-06-06 09:15:22 +0200 |
| commit | 961cc880311aed3319b08755c5a43816e2490d7f (patch) | |
| tree | 80cc3d5db32d7198adbdf89e516484dc01e58186 | |
| parent | baa0771885546816461e063131162b94c6954d86 (diff) | |
| parent | a4dd9fe0598328976862868097f59207846d865c (diff) | |
Merge pull request #233 from AeneasVerif/son/borrow-check
Add a `-borrow-check` option
45 files changed, 1500 insertions, 759 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 diff --git a/tests/coq/betree/Betree_Funs.v b/tests/coq/betree/Betree_Funs.v index b965d423..1c6092ba 100644 --- a/tests/coq/betree/Betree_Funs.v +++ b/tests/coq/betree/Betree_Funs.v @@ -88,45 +88,85 @@ Definition betree_upsert_update end . +(** [betree::betree::{betree::betree::List<T>#1}::len]: loop 0: + Source: 'src/betree.rs', lines 276:4-284:5 *) +Fixpoint betree_List_len_loop + (T : Type) (n : nat) (self : betree_List_t T) (len : u64) : result u64 := + match n with + | O => Fail_ OutOfFuel + | S n1 => + match self with + | Betree_List_Cons _ tl => + len1 <- u64_add len 1%u64; betree_List_len_loop T n1 tl len1 + | Betree_List_Nil => Ok len + end + end +. + (** [betree::betree::{betree::betree::List<T>#1}::len]: Source: 'src/betree.rs', lines 276:4-276:24 *) -Fixpoint betree_List_len +Definition betree_List_len (T : Type) (n : nat) (self : betree_List_t T) : result u64 := + betree_List_len_loop T n self 0%u64 +. + +(** [betree::betree::{betree::betree::List<T>#1}::reverse]: loop 0: + Source: 'src/betree.rs', lines 304:4-312:5 *) +Fixpoint betree_List_reverse_loop + (T : Type) (n : nat) (self : betree_List_t T) (out : betree_List_t T) : + result (betree_List_t T) + := match n with | O => Fail_ OutOfFuel | S n1 => match self with - | Betree_List_Cons _ tl => i <- betree_List_len T n1 tl; u64_add 1%u64 i - | Betree_List_Nil => Ok 0%u64 + | Betree_List_Cons hd tl => + betree_List_reverse_loop T n1 tl (Betree_List_Cons hd out) + | Betree_List_Nil => Ok out end end . -(** [betree::betree::{betree::betree::List<T>#1}::split_at]: - Source: 'src/betree.rs', lines 284:4-284:51 *) -Fixpoint betree_List_split_at - (T : Type) (n : nat) (self : betree_List_t T) (n1 : u64) : +(** [betree::betree::{betree::betree::List<T>#1}::reverse]: + Source: 'src/betree.rs', lines 304:4-304:32 *) +Definition betree_List_reverse + (T : Type) (n : nat) (self : betree_List_t T) : result (betree_List_t T) := + betree_List_reverse_loop T n self Betree_List_Nil +. + +(** [betree::betree::{betree::betree::List<T>#1}::split_at]: loop 0: + Source: 'src/betree.rs', lines 287:4-302:5 *) +Fixpoint betree_List_split_at_loop + (T : Type) (n : nat) (n1 : u64) (beg : betree_List_t T) + (self : betree_List_t T) : result ((betree_List_t T) * (betree_List_t T)) := match n with | O => Fail_ OutOfFuel | S n2 => - if n1 s= 0%u64 - then Ok (Betree_List_Nil, self) - else + if n1 s> 0%u64 + then match self with | Betree_List_Cons hd tl => - i <- u64_sub n1 1%u64; - p <- betree_List_split_at T n2 tl i; - let (ls0, ls1) := p in - Ok (Betree_List_Cons hd ls0, ls1) + n3 <- u64_sub n1 1%u64; + betree_List_split_at_loop T n2 n3 (Betree_List_Cons hd beg) tl | Betree_List_Nil => Fail_ Failure end + else (l <- betree_List_reverse T n2 beg; Ok (l, self)) end . +(** [betree::betree::{betree::betree::List<T>#1}::split_at]: + Source: 'src/betree.rs', lines 287:4-287:55 *) +Definition betree_List_split_at + (T : Type) (n : nat) (self : betree_List_t T) (n1 : u64) : + result ((betree_List_t T) * (betree_List_t T)) + := + betree_List_split_at_loop T n n1 Betree_List_Nil self +. + (** [betree::betree::{betree::betree::List<T>#1}::push_front]: - Source: 'src/betree.rs', lines 299:4-299:34 *) + Source: 'src/betree.rs', lines 315:4-315:34 *) Definition betree_List_push_front (T : Type) (self : betree_List_t T) (x : T) : result (betree_List_t T) := let (tl, _) := core_mem_replace (betree_List_t T) self Betree_List_Nil in @@ -134,7 +174,7 @@ Definition betree_List_push_front . (** [betree::betree::{betree::betree::List<T>#1}::pop_front]: - Source: 'src/betree.rs', lines 306:4-306:32 *) + Source: 'src/betree.rs', lines 322:4-322:32 *) Definition betree_List_pop_front (T : Type) (self : betree_List_t T) : result (T * (betree_List_t T)) := let (ls, _) := core_mem_replace (betree_List_t T) self Betree_List_Nil in @@ -145,7 +185,7 @@ Definition betree_List_pop_front . (** [betree::betree::{betree::betree::List<T>#1}::hd]: - Source: 'src/betree.rs', lines 318:4-318:22 *) + Source: 'src/betree.rs', lines 334:4-334:22 *) Definition betree_List_hd (T : Type) (self : betree_List_t T) : result T := match self with | Betree_List_Cons hd _ => Ok hd @@ -154,7 +194,7 @@ Definition betree_List_hd (T : Type) (self : betree_List_t T) : result T := . (** [betree::betree::{betree::betree::List<(u64, T)>#2}::head_has_key]: - Source: 'src/betree.rs', lines 327:4-327:44 *) + Source: 'src/betree.rs', lines 343:4-343:44 *) Definition betree_ListPairU64T_head_has_key (T : Type) (self : betree_List_t (u64 * T)) (key : u64) : result bool := match self with @@ -163,10 +203,11 @@ Definition betree_ListPairU64T_head_has_key end . -(** [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]: - Source: 'src/betree.rs', lines 339:4-339:73 *) -Fixpoint betree_ListPairU64T_partition_at_pivot - (T : Type) (n : nat) (self : betree_List_t (u64 * T)) (pivot : u64) : +(** [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]: loop 0: + Source: 'src/betree.rs', lines 355:4-370:5 *) +Fixpoint betree_ListPairU64T_partition_at_pivot_loop + (T : Type) (n : nat) (pivot : u64) (beg : betree_List_t (u64 * T)) + (end1 : betree_List_t (u64 * T)) (self : betree_List_t (u64 * T)) : result ((betree_List_t (u64 * T)) * (betree_List_t (u64 * T))) := match n with @@ -176,18 +217,32 @@ Fixpoint betree_ListPairU64T_partition_at_pivot | Betree_List_Cons hd tl => let (i, t) := hd in if i s>= pivot - then Ok (Betree_List_Nil, Betree_List_Cons (i, t) tl) - else ( - p <- betree_ListPairU64T_partition_at_pivot T n1 tl pivot; - let (ls0, ls1) := p in - Ok (Betree_List_Cons (i, t) ls0, ls1)) - | Betree_List_Nil => Ok (Betree_List_Nil, Betree_List_Nil) + then + betree_ListPairU64T_partition_at_pivot_loop T n1 pivot beg + (Betree_List_Cons (i, t) end1) tl + else + betree_ListPairU64T_partition_at_pivot_loop T n1 pivot + (Betree_List_Cons (i, t) beg) end1 tl + | Betree_List_Nil => + l <- betree_List_reverse (u64 * T) n1 beg; + l1 <- betree_List_reverse (u64 * T) n1 end1; + Ok (l, l1) end end . +(** [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]: + Source: 'src/betree.rs', lines 355:4-355:73 *) +Definition betree_ListPairU64T_partition_at_pivot + (T : Type) (n : nat) (self : betree_List_t (u64 * T)) (pivot : u64) : + result ((betree_List_t (u64 * T)) * (betree_List_t (u64 * T))) + := + betree_ListPairU64T_partition_at_pivot_loop T n pivot Betree_List_Nil + Betree_List_Nil self +. + (** [betree::betree::{betree::betree::Leaf#3}::split]: - Source: 'src/betree.rs', lines 359:4-364:17 *) + Source: 'src/betree.rs', lines 378:4-383:17 *) Definition betree_Leaf_split (n : nat) (self : betree_Leaf_t) (content : betree_List_t (u64 * u64)) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) @@ -222,9 +277,9 @@ Definition betree_Leaf_split node_id_cnt2)) . -(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]: - Source: 'src/betree.rs', lines 789:4-792:34 *) -Fixpoint betree_Node_lookup_first_message_for_key +(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]: loop 0: + Source: 'src/betree.rs', lines 792:4-810:5 *) +Fixpoint betree_Node_lookup_first_message_for_key_loop (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) : result ((betree_List_t (u64 * betree_Message_t)) * (betree_List_t (u64 * betree_Message_t) -> result (betree_List_t (u64 * betree_Message_t)))) @@ -238,21 +293,30 @@ Fixpoint betree_Node_lookup_first_message_for_key if i s>= key then Ok (Betree_List_Cons (i, m) next_msgs, Ok) else ( - p <- betree_Node_lookup_first_message_for_key n1 key next_msgs; - let (l, lookup_first_message_for_key_back) := p in - let back := + p <- betree_Node_lookup_first_message_for_key_loop n1 key next_msgs; + let (l, back) := p in + let back1 := fun (ret : betree_List_t (u64 * betree_Message_t)) => - next_msgs1 <- lookup_first_message_for_key_back ret; - Ok (Betree_List_Cons (i, m) next_msgs1) in - Ok (l, back)) + next_msgs1 <- back ret; Ok (Betree_List_Cons (i, m) next_msgs1) in + Ok (l, back1)) | Betree_List_Nil => Ok (Betree_List_Nil, Ok) end end . -(** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: - Source: 'src/betree.rs', lines 636:4-636:80 *) -Fixpoint betree_Node_lookup_in_bindings +(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]: + Source: 'src/betree.rs', lines 792:4-795:34 *) +Definition betree_Node_lookup_first_message_for_key + (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) : + result ((betree_List_t (u64 * betree_Message_t)) * (betree_List_t (u64 * + betree_Message_t) -> result (betree_List_t (u64 * betree_Message_t)))) + := + betree_Node_lookup_first_message_for_key_loop n key msgs +. + +(** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: loop 0: + Source: 'src/betree.rs', lines 649:4-660:5 *) +Fixpoint betree_Node_lookup_in_bindings_loop (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) : result (option u64) := @@ -265,15 +329,26 @@ Fixpoint betree_Node_lookup_in_bindings if i s= key then Ok (Some i1) else - if i s> key then Ok None else betree_Node_lookup_in_bindings n1 key tl + if i s> key + then Ok None + else betree_Node_lookup_in_bindings_loop n1 key tl | Betree_List_Nil => Ok None end end . -(** [betree::betree::{betree::betree::Node#5}::apply_upserts]: - Source: 'src/betree.rs', lines 819:4-819:90 *) -Fixpoint betree_Node_apply_upserts +(** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: + Source: 'src/betree.rs', lines 649:4-649:84 *) +Definition betree_Node_lookup_in_bindings + (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) : + result (option u64) + := + betree_Node_lookup_in_bindings_loop n key bindings +. + +(** [betree::betree::{betree::betree::Node#5}::apply_upserts]: loop 0: + Source: 'src/betree.rs', lines 820:4-844:5 *) +Fixpoint betree_Node_apply_upserts_loop (n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) (prev : option u64) (key : u64) : result (u64 * (betree_List_t (u64 * betree_Message_t))) @@ -292,7 +367,7 @@ Fixpoint betree_Node_apply_upserts | Betree_Message_Delete => Fail_ Failure | Betree_Message_Upsert s => v <- betree_upsert_update prev s; - betree_Node_apply_upserts n1 msgs1 (Some v) key + betree_Node_apply_upserts_loop n1 msgs1 (Some v) key end) else ( v <- core_option_Option_unwrap u64 prev; @@ -303,8 +378,18 @@ Fixpoint betree_Node_apply_upserts end . +(** [betree::betree::{betree::betree::Node#5}::apply_upserts]: + Source: 'src/betree.rs', lines 820:4-820:94 *) +Definition betree_Node_apply_upserts + (n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) (prev : option u64) + (key : u64) : + result (u64 * (betree_List_t (u64 * betree_Message_t))) + := + betree_Node_apply_upserts_loop n msgs prev key +. + (** [betree::betree::{betree::betree::Internal#4}::lookup_in_children]: - Source: 'src/betree.rs', lines 395:4-395:63 *) + Source: 'src/betree.rs', lines 414:4-414:63 *) Fixpoint betree_Internal_lookup_in_children (n : nat) (self : betree_Internal_t) (key : u64) (st : state) : result (state * ((option u64) * betree_Internal_t)) @@ -328,7 +413,7 @@ Fixpoint betree_Internal_lookup_in_children end (** [betree::betree::{betree::betree::Node#5}::lookup]: - Source: 'src/betree.rs', lines 709:4-709:58 *) + Source: 'src/betree.rs', lines 712:4-712:58 *) with betree_Node_lookup (n : nat) (self : betree_Node_t) (key : u64) (st : state) : result (state * ((option u64) * betree_Node_t)) @@ -394,9 +479,9 @@ with betree_Node_lookup end . -(** [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]: - Source: 'src/betree.rs', lines 674:4-674:77 *) -Fixpoint betree_Node_filter_messages_for_key +(** [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]: loop 0: + Source: 'src/betree.rs', lines 683:4-692:5 *) +Fixpoint betree_Node_filter_messages_for_key_loop (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) : result (betree_List_t (u64 * betree_Message_t)) := @@ -412,16 +497,25 @@ Fixpoint betree_Node_filter_messages_for_key betree_List_pop_front (u64 * betree_Message_t) (Betree_List_Cons (k, m) l); let (_, msgs1) := p1 in - betree_Node_filter_messages_for_key n1 key msgs1) + betree_Node_filter_messages_for_key_loop n1 key msgs1) else Ok (Betree_List_Cons (k, m) l) | Betree_List_Nil => Ok Betree_List_Nil end end . -(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]: - Source: 'src/betree.rs', lines 689:4-692:34 *) -Fixpoint betree_Node_lookup_first_message_after_key +(** [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]: + Source: 'src/betree.rs', lines 683:4-683:77 *) +Definition betree_Node_filter_messages_for_key + (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) : + result (betree_List_t (u64 * betree_Message_t)) + := + betree_Node_filter_messages_for_key_loop n key msgs +. + +(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]: loop 0: + Source: 'src/betree.rs', lines 694:4-706:5 *) +Fixpoint betree_Node_lookup_first_message_after_key_loop (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) : result ((betree_List_t (u64 * betree_Message_t)) * (betree_List_t (u64 * betree_Message_t) -> result (betree_List_t (u64 * betree_Message_t)))) @@ -434,21 +528,30 @@ Fixpoint betree_Node_lookup_first_message_after_key let (k, m) := p in if k s= key then ( - p1 <- betree_Node_lookup_first_message_after_key n1 key next_msgs; - let (l, lookup_first_message_after_key_back) := p1 in - let back := + p1 <- betree_Node_lookup_first_message_after_key_loop n1 key next_msgs; + let (l, back) := p1 in + let back1 := fun (ret : betree_List_t (u64 * betree_Message_t)) => - next_msgs1 <- lookup_first_message_after_key_back ret; - Ok (Betree_List_Cons (k, m) next_msgs1) in - Ok (l, back)) + next_msgs1 <- back ret; Ok (Betree_List_Cons (k, m) next_msgs1) in + Ok (l, back1)) else Ok (Betree_List_Cons (k, m) next_msgs, Ok) | Betree_List_Nil => Ok (Betree_List_Nil, Ok) end end . +(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]: + Source: 'src/betree.rs', lines 694:4-697:34 *) +Definition betree_Node_lookup_first_message_after_key + (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) : + result ((betree_List_t (u64 * betree_Message_t)) * (betree_List_t (u64 * + betree_Message_t) -> result (betree_List_t (u64 * betree_Message_t)))) + := + betree_Node_lookup_first_message_after_key_loop n key msgs +. + (** [betree::betree::{betree::betree::Node#5}::apply_to_internal]: - Source: 'src/betree.rs', lines 521:4-521:89 *) + Source: 'src/betree.rs', lines 534:4-534:89 *) Definition betree_Node_apply_to_internal (n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) (key : u64) (new_msg : betree_Message_t) : @@ -508,9 +611,9 @@ Definition betree_Node_apply_to_internal lookup_first_message_for_key_back msgs2) . -(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]: - Source: 'src/betree.rs', lines 502:4-505:5 *) -Fixpoint betree_Node_apply_messages_to_internal +(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]: loop 0: + Source: 'src/betree.rs', lines 518:4-526:5 *) +Fixpoint betree_Node_apply_messages_to_internal_loop (n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) (new_msgs : betree_List_t (u64 * betree_Message_t)) : result (betree_List_t (u64 * betree_Message_t)) @@ -522,15 +625,25 @@ Fixpoint betree_Node_apply_messages_to_internal | Betree_List_Cons new_msg new_msgs_tl => let (i, m) := new_msg in msgs1 <- betree_Node_apply_to_internal n1 msgs i m; - betree_Node_apply_messages_to_internal n1 msgs1 new_msgs_tl + betree_Node_apply_messages_to_internal_loop n1 msgs1 new_msgs_tl | Betree_List_Nil => Ok msgs end end . -(** [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]: - Source: 'src/betree.rs', lines 653:4-656:32 *) -Fixpoint betree_Node_lookup_mut_in_bindings +(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]: + Source: 'src/betree.rs', lines 518:4-521:5 *) +Definition betree_Node_apply_messages_to_internal + (n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) + (new_msgs : betree_List_t (u64 * betree_Message_t)) : + result (betree_List_t (u64 * betree_Message_t)) + := + betree_Node_apply_messages_to_internal_loop n msgs new_msgs +. + +(** [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]: loop 0: + Source: 'src/betree.rs', lines 664:4-677:5 *) +Fixpoint betree_Node_lookup_mut_in_bindings_loop (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) : result ((betree_List_t (u64 * u64)) * (betree_List_t (u64 * u64) -> result (betree_List_t (u64 * u64)))) @@ -544,20 +657,29 @@ Fixpoint betree_Node_lookup_mut_in_bindings if i s>= key then Ok (Betree_List_Cons (i, i1) tl, Ok) else ( - p <- betree_Node_lookup_mut_in_bindings n1 key tl; - let (l, lookup_mut_in_bindings_back) := p in - let back := + p <- betree_Node_lookup_mut_in_bindings_loop n1 key tl; + let (l, back) := p in + let back1 := fun (ret : betree_List_t (u64 * u64)) => - tl1 <- lookup_mut_in_bindings_back ret; - Ok (Betree_List_Cons (i, i1) tl1) in - Ok (l, back)) + tl1 <- back ret; Ok (Betree_List_Cons (i, i1) tl1) in + Ok (l, back1)) | Betree_List_Nil => Ok (Betree_List_Nil, Ok) end end . +(** [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]: + Source: 'src/betree.rs', lines 664:4-667:32 *) +Definition betree_Node_lookup_mut_in_bindings + (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) : + result ((betree_List_t (u64 * u64)) * (betree_List_t (u64 * u64) -> result + (betree_List_t (u64 * u64)))) + := + betree_Node_lookup_mut_in_bindings_loop n key bindings +. + (** [betree::betree::{betree::betree::Node#5}::apply_to_leaf]: - Source: 'src/betree.rs', lines 460:4-460:87 *) + Source: 'src/betree.rs', lines 476:4-476:87 *) Definition betree_Node_apply_to_leaf (n : nat) (bindings : betree_List_t (u64 * u64)) (key : u64) (new_msg : betree_Message_t) : @@ -594,9 +716,9 @@ Definition betree_Node_apply_to_leaf end . -(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]: - Source: 'src/betree.rs', lines 444:4-447:5 *) -Fixpoint betree_Node_apply_messages_to_leaf +(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]: loop 0: + Source: 'src/betree.rs', lines 463:4-471:5 *) +Fixpoint betree_Node_apply_messages_to_leaf_loop (n : nat) (bindings : betree_List_t (u64 * u64)) (new_msgs : betree_List_t (u64 * betree_Message_t)) : result (betree_List_t (u64 * u64)) @@ -608,14 +730,24 @@ Fixpoint betree_Node_apply_messages_to_leaf | Betree_List_Cons new_msg new_msgs_tl => let (i, m) := new_msg in bindings1 <- betree_Node_apply_to_leaf n1 bindings i m; - betree_Node_apply_messages_to_leaf n1 bindings1 new_msgs_tl + betree_Node_apply_messages_to_leaf_loop n1 bindings1 new_msgs_tl | Betree_List_Nil => Ok bindings end end . +(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]: + Source: 'src/betree.rs', lines 463:4-466:5 *) +Definition betree_Node_apply_messages_to_leaf + (n : nat) (bindings : betree_List_t (u64 * u64)) + (new_msgs : betree_List_t (u64 * betree_Message_t)) : + result (betree_List_t (u64 * u64)) + := + betree_Node_apply_messages_to_leaf_loop n bindings new_msgs +. + (** [betree::betree::{betree::betree::Internal#4}::flush]: - Source: 'src/betree.rs', lines 410:4-415:26 *) + Source: 'src/betree.rs', lines 429:4-434:26 *) Fixpoint betree_Internal_flush (n : nat) (self : betree_Internal_t) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) @@ -665,7 +797,7 @@ Fixpoint betree_Internal_flush end (** [betree::betree::{betree::betree::Node#5}::apply_messages]: - Source: 'src/betree.rs', lines 588:4-593:5 *) + Source: 'src/betree.rs', lines 601:4-606:5 *) with betree_Node_apply_messages (n : nat) (self : betree_Node_t) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) @@ -721,7 +853,7 @@ with betree_Node_apply_messages . (** [betree::betree::{betree::betree::Node#5}::apply]: - Source: 'src/betree.rs', lines 576:4-582:5 *) + Source: 'src/betree.rs', lines 589:4-595:5 *) Definition betree_Node_apply (n : nat) (self : betree_Node_t) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) (key : u64) @@ -737,7 +869,7 @@ Definition betree_Node_apply . (** [betree::betree::{betree::betree::BeTree#6}::new]: - Source: 'src/betree.rs', lines 849:4-849:60 *) + Source: 'src/betree.rs', lines 848:4-848:60 *) Definition betree_BeTree_new (min_flush_size : u64) (split_size : u64) (st : state) : result (state * betree_BeTree_t) @@ -762,7 +894,7 @@ Definition betree_BeTree_new . (** [betree::betree::{betree::betree::BeTree#6}::apply]: - Source: 'src/betree.rs', lines 868:4-868:47 *) + Source: 'src/betree.rs', lines 867:4-867:47 *) Definition betree_BeTree_apply (n : nat) (self : betree_BeTree_t) (key : u64) (msg : betree_Message_t) (st : state) : @@ -782,7 +914,7 @@ Definition betree_BeTree_apply . (** [betree::betree::{betree::betree::BeTree#6}::insert]: - Source: 'src/betree.rs', lines 874:4-874:52 *) + Source: 'src/betree.rs', lines 873:4-873:52 *) Definition betree_BeTree_insert (n : nat) (self : betree_BeTree_t) (key : u64) (value : u64) (st : state) : result (state * betree_BeTree_t) @@ -791,7 +923,7 @@ Definition betree_BeTree_insert . (** [betree::betree::{betree::betree::BeTree#6}::delete]: - Source: 'src/betree.rs', lines 880:4-880:38 *) + Source: 'src/betree.rs', lines 879:4-879:38 *) Definition betree_BeTree_delete (n : nat) (self : betree_BeTree_t) (key : u64) (st : state) : result (state * betree_BeTree_t) @@ -800,7 +932,7 @@ Definition betree_BeTree_delete . (** [betree::betree::{betree::betree::BeTree#6}::upsert]: - Source: 'src/betree.rs', lines 886:4-886:59 *) + Source: 'src/betree.rs', lines 885:4-885:59 *) Definition betree_BeTree_upsert (n : nat) (self : betree_BeTree_t) (key : u64) (upd : betree_UpsertFunState_t) (st : state) : @@ -810,7 +942,7 @@ Definition betree_BeTree_upsert . (** [betree::betree::{betree::betree::BeTree#6}::lookup]: - Source: 'src/betree.rs', lines 895:4-895:62 *) + Source: 'src/betree.rs', lines 894:4-894:62 *) Definition betree_BeTree_lookup (n : nat) (self : betree_BeTree_t) (key : u64) (st : state) : result (state * ((option u64) * betree_BeTree_t)) diff --git a/tests/fstar/betree/Betree.Clauses.Template.fst b/tests/fstar/betree/Betree.Clauses.Template.fst index fad8c5ba..d3e07c7e 100644 --- a/tests/fstar/betree/Betree.Clauses.Template.fst +++ b/tests/fstar/betree/Betree.Clauses.Template.fst @@ -7,100 +7,109 @@ open Betree.Types #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" (** [betree::betree::{betree::betree::List<T>#1}::len]: decreases clause - Source: 'src/betree.rs', lines 276:4-276:24 *) + Source: 'src/betree.rs', lines 276:4-284:5 *) unfold -let betree_List_len_decreases (t : Type0) (self : betree_List_t t) : nat = +let betree_List_len_loop_decreases (t : Type0) (self : betree_List_t t) + (len : u64) : nat = + admit () + +(** [betree::betree::{betree::betree::List<T>#1}::reverse]: decreases clause + Source: 'src/betree.rs', lines 304:4-312:5 *) +unfold +let betree_List_reverse_loop_decreases (t : Type0) (self : betree_List_t t) + (out : betree_List_t t) : nat = admit () (** [betree::betree::{betree::betree::List<T>#1}::split_at]: decreases clause - Source: 'src/betree.rs', lines 284:4-284:51 *) + Source: 'src/betree.rs', lines 287:4-302:5 *) unfold -let betree_List_split_at_decreases (t : Type0) (self : betree_List_t t) - (n : u64) : nat = +let betree_List_split_at_loop_decreases (t : Type0) (n : u64) + (beg : betree_List_t t) (self : betree_List_t t) : nat = admit () (** [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]: decreases clause - Source: 'src/betree.rs', lines 339:4-339:73 *) + Source: 'src/betree.rs', lines 355:4-370:5 *) unfold -let betree_ListPairU64T_partition_at_pivot_decreases (t : Type0) - (self : betree_List_t (u64 & t)) (pivot : u64) : nat = +let betree_ListPairU64T_partition_at_pivot_loop_decreases (t : Type0) + (pivot : u64) (beg : betree_List_t (u64 & t)) + (end1 : betree_List_t (u64 & t)) (self : betree_List_t (u64 & t)) : nat = admit () (** [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]: decreases clause - Source: 'src/betree.rs', lines 789:4-792:34 *) + Source: 'src/betree.rs', lines 792:4-810:5 *) unfold -let betree_Node_lookup_first_message_for_key_decreases (key : u64) +let betree_Node_lookup_first_message_for_key_loop_decreases (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) : nat = admit () (** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: decreases clause - Source: 'src/betree.rs', lines 636:4-636:80 *) + Source: 'src/betree.rs', lines 649:4-660:5 *) unfold -let betree_Node_lookup_in_bindings_decreases (key : u64) +let betree_Node_lookup_in_bindings_loop_decreases (key : u64) (bindings : betree_List_t (u64 & u64)) : nat = admit () (** [betree::betree::{betree::betree::Node#5}::apply_upserts]: decreases clause - Source: 'src/betree.rs', lines 819:4-819:90 *) + Source: 'src/betree.rs', lines 820:4-844:5 *) unfold -let betree_Node_apply_upserts_decreases +let betree_Node_apply_upserts_loop_decreases (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64) (key : u64) : nat = admit () (** [betree::betree::{betree::betree::Internal#4}::lookup_in_children]: decreases clause - Source: 'src/betree.rs', lines 395:4-395:63 *) + Source: 'src/betree.rs', lines 414:4-414:63 *) unfold let betree_Internal_lookup_in_children_decreases (self : betree_Internal_t) (key : u64) (st : state) : nat = admit () (** [betree::betree::{betree::betree::Node#5}::lookup]: decreases clause - Source: 'src/betree.rs', lines 709:4-709:58 *) + Source: 'src/betree.rs', lines 712:4-712:58 *) unfold let betree_Node_lookup_decreases (self : betree_Node_t) (key : u64) (st : state) : nat = admit () (** [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]: decreases clause - Source: 'src/betree.rs', lines 674:4-674:77 *) + Source: 'src/betree.rs', lines 683:4-692:5 *) unfold -let betree_Node_filter_messages_for_key_decreases (key : u64) +let betree_Node_filter_messages_for_key_loop_decreases (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) : nat = admit () (** [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]: decreases clause - Source: 'src/betree.rs', lines 689:4-692:34 *) + Source: 'src/betree.rs', lines 694:4-706:5 *) unfold -let betree_Node_lookup_first_message_after_key_decreases (key : u64) +let betree_Node_lookup_first_message_after_key_loop_decreases (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) : nat = admit () (** [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]: decreases clause - Source: 'src/betree.rs', lines 502:4-505:5 *) + Source: 'src/betree.rs', lines 518:4-526:5 *) unfold -let betree_Node_apply_messages_to_internal_decreases +let betree_Node_apply_messages_to_internal_loop_decreases (msgs : betree_List_t (u64 & betree_Message_t)) (new_msgs : betree_List_t (u64 & betree_Message_t)) : nat = admit () (** [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]: decreases clause - Source: 'src/betree.rs', lines 653:4-656:32 *) + Source: 'src/betree.rs', lines 664:4-677:5 *) unfold -let betree_Node_lookup_mut_in_bindings_decreases (key : u64) +let betree_Node_lookup_mut_in_bindings_loop_decreases (key : u64) (bindings : betree_List_t (u64 & u64)) : nat = admit () (** [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]: decreases clause - Source: 'src/betree.rs', lines 444:4-447:5 *) + Source: 'src/betree.rs', lines 463:4-471:5 *) unfold -let betree_Node_apply_messages_to_leaf_decreases +let betree_Node_apply_messages_to_leaf_loop_decreases (bindings : betree_List_t (u64 & u64)) (new_msgs : betree_List_t (u64 & betree_Message_t)) : nat = admit () (** [betree::betree::{betree::betree::Internal#4}::flush]: decreases clause - Source: 'src/betree.rs', lines 410:4-415:26 *) + Source: 'src/betree.rs', lines 429:4-434:26 *) unfold let betree_Internal_flush_decreases (self : betree_Internal_t) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) @@ -108,7 +117,7 @@ let betree_Internal_flush_decreases (self : betree_Internal_t) admit () (** [betree::betree::{betree::betree::Node#5}::apply_messages]: decreases clause - Source: 'src/betree.rs', lines 588:4-593:5 *) + Source: 'src/betree.rs', lines 601:4-606:5 *) unfold let betree_Node_apply_messages_decreases (self : betree_Node_t) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) diff --git a/tests/fstar/betree/Betree.Clauses.fst b/tests/fstar/betree/Betree.Clauses.fst index ae201cee..c50bf421 100644 --- a/tests/fstar/betree/Betree.Clauses.fst +++ b/tests/fstar/betree/Betree.Clauses.fst @@ -103,36 +103,46 @@ let wf_nat_pair_lem (p0 p1 : nat_pair) : (** [betree_main::betree::List::{1}::len]: decreases clause *) unfold -let betree_List_len_decreases (t : Type0) (self : betree_List_t t) : betree_List_t t = +let betree_List_len_loop_decreases (t : Type0) (self : betree_List_t t) (len : u64) : betree_List_t t = self -(** [betree_main::betree::List::{1}::split_at]: decreases clause *) +(** [betree::betree::{betree::betree::List<T>#1}::reverse]: decreases clause + Source: 'src/betree.rs', lines 304:4-312:5 *) unfold -let betree_List_split_at_decreases (t : Type0) (self : betree_List_t t) - (n : u64) : nat = +let betree_List_reverse_loop_decreases (t : Type0) (self : betree_List_t t) + (out : betree_List_t t) = + self + +(** [betree::betree::{betree::betree::List<T>#1}::split_at]: decreases clause + Source: 'src/betree.rs', lines 287:4-302:5 *) +unfold +let betree_List_split_at_loop_decreases (t : Type0) (n : u64) + (beg : betree_List_t t) (self : betree_List_t t) : nat = n -(** [betree_main::betree::List::{2}::partition_at_pivot]: decreases clause *) +(** [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]: decreases clause + Source: 'src/betree.rs', lines 355:4-370:5 *) unfold -let betree_ListPairU64T_partition_at_pivot_decreases (t : Type0) - (self : betree_List_t (u64 & t)) (pivot : u64) : betree_List_t (u64 & t) = +let betree_ListPairU64T_partition_at_pivot_loop_decreases (t : Type0) + (pivot : u64) (beg : betree_List_t (u64 & t)) (end0 : betree_List_t (u64 & t)) + (self : betree_List_t (u64 & t)) = self (** [betree_main::betree::Node::{5}::lookup_in_bindings]: decreases clause *) unfold -let betree_Node_lookup_in_bindings_decreases (key : u64) +let betree_Node_lookup_in_bindings_loop_decreases (key : u64) (bindings : betree_List_t (u64 & u64)) : betree_List_t (u64 & u64) = bindings (** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: decreases clause *) unfold -let betree_Node_lookup_first_message_for_key_decreases (key : u64) +let betree_Node_lookup_first_message_for_key_loop_decreases (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) : betree_List_t (u64 & betree_Message_t) = msgs (** [betree_main::betree::Node::{5}::apply_upserts]: decreases clause *) unfold -let betree_Node_apply_upserts_decreases +let betree_Node_apply_upserts_loop_decreases (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64) (key : u64) : betree_List_t (u64 & betree_Message_t) = msgs @@ -151,29 +161,29 @@ let betree_Node_lookup_decreases (self : betree_Node_t) (key : u64) (** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: decreases clause *) unfold -let betree_Node_lookup_mut_in_bindings_decreases (key : u64) +let betree_Node_lookup_mut_in_bindings_loop_decreases (key : u64) (bindings : betree_List_t (u64 & u64)) : betree_List_t (u64 & u64) = bindings unfold -let betree_Node_apply_messages_to_leaf_decreases +let betree_Node_apply_messages_to_leaf_loop_decreases (bindings : betree_List_t (u64 & u64)) (new_msgs : betree_List_t (u64 & betree_Message_t)) : betree_List_t (u64 & betree_Message_t) = new_msgs (** [betree_main::betree::Node::{5}::filter_messages_for_key]: decreases clause *) unfold -let betree_Node_filter_messages_for_key_decreases (key : u64) +let betree_Node_filter_messages_for_key_loop_decreases (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) : betree_List_t (u64 & betree_Message_t) = msgs (** [betree_main::betree::Node::{5}::lookup_first_message_after_key]: decreases clause *) unfold -let betree_Node_lookup_first_message_after_key_decreases (key : u64) +let betree_Node_lookup_first_message_after_key_loop_decreases (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) : betree_List_t (u64 & betree_Message_t) = msgs -let betree_Node_apply_messages_to_internal_decreases +let betree_Node_apply_messages_to_internal_loop_decreases (msgs : betree_List_t (u64 & betree_Message_t)) (new_msgs : betree_List_t (u64 & betree_Message_t)) : betree_List_t (u64 & betree_Message_t) = new_msgs diff --git a/tests/fstar/betree/Betree.Funs.fst b/tests/fstar/betree/Betree.Funs.fst index 07f561f5..de3ac13c 100644 --- a/tests/fstar/betree/Betree.Funs.fst +++ b/tests/fstar/betree/Betree.Funs.fst @@ -75,45 +75,76 @@ let betree_upsert_update end end +(** [betree::betree::{betree::betree::List<T>#1}::len]: loop 0: + Source: 'src/betree.rs', lines 276:4-284:5 *) +let rec betree_List_len_loop + (t : Type0) (self : betree_List_t t) (len : u64) : + Tot (result u64) (decreases (betree_List_len_loop_decreases t self len)) + = + begin match self with + | Betree_List_Cons _ tl -> + let* len1 = u64_add len 1 in betree_List_len_loop t tl len1 + | Betree_List_Nil -> Ok len + end + (** [betree::betree::{betree::betree::List<T>#1}::len]: Source: 'src/betree.rs', lines 276:4-276:24 *) -let rec betree_List_len - (t : Type0) (self : betree_List_t t) : - Tot (result u64) (decreases (betree_List_len_decreases t self)) +let betree_List_len (t : Type0) (self : betree_List_t t) : result u64 = + betree_List_len_loop t self 0 + +(** [betree::betree::{betree::betree::List<T>#1}::reverse]: loop 0: + Source: 'src/betree.rs', lines 304:4-312:5 *) +let rec betree_List_reverse_loop + (t : Type0) (self : betree_List_t t) (out : betree_List_t t) : + Tot (result (betree_List_t t)) + (decreases (betree_List_reverse_loop_decreases t self out)) = begin match self with - | Betree_List_Cons _ tl -> let* i = betree_List_len t tl in u64_add 1 i - | Betree_List_Nil -> Ok 0 + | Betree_List_Cons hd tl -> + betree_List_reverse_loop t tl (Betree_List_Cons hd out) + | Betree_List_Nil -> Ok out end -(** [betree::betree::{betree::betree::List<T>#1}::split_at]: - Source: 'src/betree.rs', lines 284:4-284:51 *) -let rec betree_List_split_at - (t : Type0) (self : betree_List_t t) (n : u64) : +(** [betree::betree::{betree::betree::List<T>#1}::reverse]: + Source: 'src/betree.rs', lines 304:4-304:32 *) +let betree_List_reverse + (t : Type0) (self : betree_List_t t) : result (betree_List_t t) = + betree_List_reverse_loop t self Betree_List_Nil + +(** [betree::betree::{betree::betree::List<T>#1}::split_at]: loop 0: + Source: 'src/betree.rs', lines 287:4-302:5 *) +let rec betree_List_split_at_loop + (t : Type0) (n : u64) (beg : betree_List_t t) (self : betree_List_t t) : Tot (result ((betree_List_t t) & (betree_List_t t))) - (decreases (betree_List_split_at_decreases t self n)) + (decreases (betree_List_split_at_loop_decreases t n beg self)) = - if n = 0 - then Ok (Betree_List_Nil, self) - else + if n > 0 + then begin match self with | Betree_List_Cons hd tl -> - let* i = u64_sub n 1 in - let* p = betree_List_split_at t tl i in - let (ls0, ls1) = p in - Ok (Betree_List_Cons hd ls0, ls1) + let* n1 = u64_sub n 1 in + betree_List_split_at_loop t n1 (Betree_List_Cons hd beg) tl | Betree_List_Nil -> Fail Failure end + else let* l = betree_List_reverse t beg in Ok (l, self) + +(** [betree::betree::{betree::betree::List<T>#1}::split_at]: + Source: 'src/betree.rs', lines 287:4-287:55 *) +let betree_List_split_at + (t : Type0) (self : betree_List_t t) (n : u64) : + result ((betree_List_t t) & (betree_List_t t)) + = + betree_List_split_at_loop t n Betree_List_Nil self (** [betree::betree::{betree::betree::List<T>#1}::push_front]: - Source: 'src/betree.rs', lines 299:4-299:34 *) + Source: 'src/betree.rs', lines 315:4-315:34 *) let betree_List_push_front (t : Type0) (self : betree_List_t t) (x : t) : result (betree_List_t t) = let (tl, _) = core_mem_replace (betree_List_t t) self Betree_List_Nil in Ok (Betree_List_Cons x tl) (** [betree::betree::{betree::betree::List<T>#1}::pop_front]: - Source: 'src/betree.rs', lines 306:4-306:32 *) + Source: 'src/betree.rs', lines 322:4-322:32 *) let betree_List_pop_front (t : Type0) (self : betree_List_t t) : result (t & (betree_List_t t)) = let (ls, _) = core_mem_replace (betree_List_t t) self Betree_List_Nil in @@ -123,7 +154,7 @@ let betree_List_pop_front end (** [betree::betree::{betree::betree::List<T>#1}::hd]: - Source: 'src/betree.rs', lines 318:4-318:22 *) + Source: 'src/betree.rs', lines 334:4-334:22 *) let betree_List_hd (t : Type0) (self : betree_List_t t) : result t = begin match self with | Betree_List_Cons hd _ -> Ok hd @@ -131,7 +162,7 @@ let betree_List_hd (t : Type0) (self : betree_List_t t) : result t = end (** [betree::betree::{betree::betree::List<(u64, T)>#2}::head_has_key]: - Source: 'src/betree.rs', lines 327:4-327:44 *) + Source: 'src/betree.rs', lines 343:4-343:44 *) let betree_ListPairU64T_head_has_key (t : Type0) (self : betree_List_t (u64 & t)) (key : u64) : result bool = begin match self with @@ -139,27 +170,43 @@ let betree_ListPairU64T_head_has_key | Betree_List_Nil -> Ok false end -(** [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]: - Source: 'src/betree.rs', lines 339:4-339:73 *) -let rec betree_ListPairU64T_partition_at_pivot - (t : Type0) (self : betree_List_t (u64 & t)) (pivot : u64) : +(** [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]: loop 0: + Source: 'src/betree.rs', lines 355:4-370:5 *) +let rec betree_ListPairU64T_partition_at_pivot_loop + (t : Type0) (pivot : u64) (beg : betree_List_t (u64 & t)) + (end1 : betree_List_t (u64 & t)) (self : betree_List_t (u64 & t)) : Tot (result ((betree_List_t (u64 & t)) & (betree_List_t (u64 & t)))) - (decreases (betree_ListPairU64T_partition_at_pivot_decreases t self pivot)) + (decreases ( + betree_ListPairU64T_partition_at_pivot_loop_decreases t pivot beg end1 + self)) = begin match self with | Betree_List_Cons hd tl -> let (i, x) = hd in if i >= pivot - then Ok (Betree_List_Nil, Betree_List_Cons (i, x) tl) + then + betree_ListPairU64T_partition_at_pivot_loop t pivot beg (Betree_List_Cons + (i, x) end1) tl else - let* p = betree_ListPairU64T_partition_at_pivot t tl pivot in - let (ls0, ls1) = p in - Ok (Betree_List_Cons (i, x) ls0, ls1) - | Betree_List_Nil -> Ok (Betree_List_Nil, Betree_List_Nil) + betree_ListPairU64T_partition_at_pivot_loop t pivot (Betree_List_Cons (i, + x) beg) end1 tl + | Betree_List_Nil -> + let* l = betree_List_reverse (u64 & t) beg in + let* l1 = betree_List_reverse (u64 & t) end1 in + Ok (l, l1) end +(** [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]: + Source: 'src/betree.rs', lines 355:4-355:73 *) +let betree_ListPairU64T_partition_at_pivot + (t : Type0) (self : betree_List_t (u64 & t)) (pivot : u64) : + result ((betree_List_t (u64 & t)) & (betree_List_t (u64 & t))) + = + betree_ListPairU64T_partition_at_pivot_loop t pivot Betree_List_Nil + Betree_List_Nil self + (** [betree::betree::{betree::betree::Leaf#3}::split]: - Source: 'src/betree.rs', lines 359:4-364:17 *) + Source: 'src/betree.rs', lines 378:4-383:17 *) let betree_Leaf_split (self : betree_Leaf_t) (content : betree_List_t (u64 & u64)) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) @@ -179,13 +226,14 @@ let betree_Leaf_split Ok (st2, ({ id = self.id; pivot = pivot; left = n; right = n1 }, node_id_cnt2)) -(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]: - Source: 'src/betree.rs', lines 789:4-792:34 *) -let rec betree_Node_lookup_first_message_for_key +(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]: loop 0: + Source: 'src/betree.rs', lines 792:4-810:5 *) +let rec betree_Node_lookup_first_message_for_key_loop (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) : Tot (result ((betree_List_t (u64 & betree_Message_t)) & (betree_List_t (u64 & betree_Message_t) -> result (betree_List_t (u64 & betree_Message_t))))) - (decreases (betree_Node_lookup_first_message_for_key_decreases key msgs)) + (decreases ( + betree_Node_lookup_first_message_for_key_loop_decreases key msgs)) = begin match msgs with | Betree_List_Cons x next_msgs -> @@ -193,39 +241,55 @@ let rec betree_Node_lookup_first_message_for_key if i >= key then Ok (Betree_List_Cons (i, m) next_msgs, Ok) else - let* (l, lookup_first_message_for_key_back) = - betree_Node_lookup_first_message_for_key key next_msgs in - let back = + let* (l, back) = + betree_Node_lookup_first_message_for_key_loop key next_msgs in + let back1 = fun ret -> - let* next_msgs1 = lookup_first_message_for_key_back ret in - Ok (Betree_List_Cons (i, m) next_msgs1) in - Ok (l, back) + let* next_msgs1 = back ret in Ok (Betree_List_Cons (i, m) next_msgs1) + in + Ok (l, back1) | Betree_List_Nil -> Ok (Betree_List_Nil, Ok) end -(** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: - Source: 'src/betree.rs', lines 636:4-636:80 *) -let rec betree_Node_lookup_in_bindings +(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]: + Source: 'src/betree.rs', lines 792:4-795:34 *) +let betree_Node_lookup_first_message_for_key + (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) : + result ((betree_List_t (u64 & betree_Message_t)) & (betree_List_t (u64 & + betree_Message_t) -> result (betree_List_t (u64 & betree_Message_t)))) + = + betree_Node_lookup_first_message_for_key_loop key msgs + +(** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: loop 0: + Source: 'src/betree.rs', lines 649:4-660:5 *) +let rec betree_Node_lookup_in_bindings_loop (key : u64) (bindings : betree_List_t (u64 & u64)) : Tot (result (option u64)) - (decreases (betree_Node_lookup_in_bindings_decreases key bindings)) + (decreases (betree_Node_lookup_in_bindings_loop_decreases key bindings)) = begin match bindings with | Betree_List_Cons hd tl -> let (i, i1) = hd in if i = key then Ok (Some i1) - else if i > key then Ok None else betree_Node_lookup_in_bindings key tl + else + if i > key then Ok None else betree_Node_lookup_in_bindings_loop key tl | Betree_List_Nil -> Ok None end -(** [betree::betree::{betree::betree::Node#5}::apply_upserts]: - Source: 'src/betree.rs', lines 819:4-819:90 *) -let rec betree_Node_apply_upserts +(** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: + Source: 'src/betree.rs', lines 649:4-649:84 *) +let betree_Node_lookup_in_bindings + (key : u64) (bindings : betree_List_t (u64 & u64)) : result (option u64) = + betree_Node_lookup_in_bindings_loop key bindings + +(** [betree::betree::{betree::betree::Node#5}::apply_upserts]: loop 0: + Source: 'src/betree.rs', lines 820:4-844:5 *) +let rec betree_Node_apply_upserts_loop (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64) (key : u64) : Tot (result (u64 & (betree_List_t (u64 & betree_Message_t)))) - (decreases (betree_Node_apply_upserts_decreases msgs prev key)) + (decreases (betree_Node_apply_upserts_loop_decreases msgs prev key)) = let* b = betree_ListPairU64T_head_has_key betree_Message_t msgs key in if b @@ -237,7 +301,7 @@ let rec betree_Node_apply_upserts | Betree_Message_Delete -> Fail Failure | Betree_Message_Upsert s -> let* v = betree_upsert_update prev s in - betree_Node_apply_upserts msgs1 (Some v) key + betree_Node_apply_upserts_loop msgs1 (Some v) key end else let* v = core_option_Option_unwrap u64 prev in @@ -246,8 +310,17 @@ let rec betree_Node_apply_upserts Betree_Message_Insert v) in Ok (v, msgs1) +(** [betree::betree::{betree::betree::Node#5}::apply_upserts]: + Source: 'src/betree.rs', lines 820:4-820:94 *) +let betree_Node_apply_upserts + (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64) + (key : u64) : + result (u64 & (betree_List_t (u64 & betree_Message_t))) + = + betree_Node_apply_upserts_loop msgs prev key + (** [betree::betree::{betree::betree::Internal#4}::lookup_in_children]: - Source: 'src/betree.rs', lines 395:4-395:63 *) + Source: 'src/betree.rs', lines 414:4-414:63 *) let rec betree_Internal_lookup_in_children (self : betree_Internal_t) (key : u64) (st : state) : Tot (result (state & ((option u64) & betree_Internal_t))) @@ -262,7 +335,7 @@ let rec betree_Internal_lookup_in_children Ok (st1, (o, { self with right = n })) (** [betree::betree::{betree::betree::Node#5}::lookup]: - Source: 'src/betree.rs', lines 709:4-709:58 *) + Source: 'src/betree.rs', lines 712:4-712:58 *) and betree_Node_lookup (self : betree_Node_t) (key : u64) (st : state) : Tot (result (state & ((option u64) & betree_Node_t))) @@ -317,12 +390,12 @@ and betree_Node_lookup Ok (st1, (o, Betree_Node_Leaf node)) end -(** [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]: - Source: 'src/betree.rs', lines 674:4-674:77 *) -let rec betree_Node_filter_messages_for_key +(** [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]: loop 0: + Source: 'src/betree.rs', lines 683:4-692:5 *) +let rec betree_Node_filter_messages_for_key_loop (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) : Tot (result (betree_List_t (u64 & betree_Message_t))) - (decreases (betree_Node_filter_messages_for_key_decreases key msgs)) + (decreases (betree_Node_filter_messages_for_key_loop_decreases key msgs)) = begin match msgs with | Betree_List_Cons p l -> @@ -332,37 +405,55 @@ let rec betree_Node_filter_messages_for_key let* (_, msgs1) = betree_List_pop_front (u64 & betree_Message_t) (Betree_List_Cons (k, m) l) in - betree_Node_filter_messages_for_key key msgs1 + betree_Node_filter_messages_for_key_loop key msgs1 else Ok (Betree_List_Cons (k, m) l) | Betree_List_Nil -> Ok Betree_List_Nil end -(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]: - Source: 'src/betree.rs', lines 689:4-692:34 *) -let rec betree_Node_lookup_first_message_after_key +(** [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]: + Source: 'src/betree.rs', lines 683:4-683:77 *) +let betree_Node_filter_messages_for_key + (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) : + result (betree_List_t (u64 & betree_Message_t)) + = + betree_Node_filter_messages_for_key_loop key msgs + +(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]: loop 0: + Source: 'src/betree.rs', lines 694:4-706:5 *) +let rec betree_Node_lookup_first_message_after_key_loop (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) : Tot (result ((betree_List_t (u64 & betree_Message_t)) & (betree_List_t (u64 & betree_Message_t) -> result (betree_List_t (u64 & betree_Message_t))))) - (decreases (betree_Node_lookup_first_message_after_key_decreases key msgs)) + (decreases ( + betree_Node_lookup_first_message_after_key_loop_decreases key msgs)) = begin match msgs with | Betree_List_Cons p next_msgs -> let (k, m) = p in if k = key then - let* (l, lookup_first_message_after_key_back) = - betree_Node_lookup_first_message_after_key key next_msgs in - let back = + let* (l, back) = + betree_Node_lookup_first_message_after_key_loop key next_msgs in + let back1 = fun ret -> - let* next_msgs1 = lookup_first_message_after_key_back ret in - Ok (Betree_List_Cons (k, m) next_msgs1) in - Ok (l, back) + let* next_msgs1 = back ret in Ok (Betree_List_Cons (k, m) next_msgs1) + in + Ok (l, back1) else Ok (Betree_List_Cons (k, m) next_msgs, Ok) | Betree_List_Nil -> Ok (Betree_List_Nil, Ok) end +(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]: + Source: 'src/betree.rs', lines 694:4-697:34 *) +let betree_Node_lookup_first_message_after_key + (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) : + result ((betree_List_t (u64 & betree_Message_t)) & (betree_List_t (u64 & + betree_Message_t) -> result (betree_List_t (u64 & betree_Message_t)))) + = + betree_Node_lookup_first_message_after_key_loop key msgs + (** [betree::betree::{betree::betree::Node#5}::apply_to_internal]: - Source: 'src/betree.rs', lines 521:4-521:89 *) + Source: 'src/betree.rs', lines 534:4-534:89 *) let betree_Node_apply_to_internal (msgs : betree_List_t (u64 & betree_Message_t)) (key : u64) (new_msg : betree_Message_t) : @@ -421,29 +512,39 @@ let betree_Node_apply_to_internal betree_List_push_front (u64 & betree_Message_t) msgs1 (key, new_msg) in lookup_first_message_for_key_back msgs2 -(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]: - Source: 'src/betree.rs', lines 502:4-505:5 *) -let rec betree_Node_apply_messages_to_internal +(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]: loop 0: + Source: 'src/betree.rs', lines 518:4-526:5 *) +let rec betree_Node_apply_messages_to_internal_loop (msgs : betree_List_t (u64 & betree_Message_t)) (new_msgs : betree_List_t (u64 & betree_Message_t)) : Tot (result (betree_List_t (u64 & betree_Message_t))) - (decreases (betree_Node_apply_messages_to_internal_decreases msgs new_msgs)) + (decreases ( + betree_Node_apply_messages_to_internal_loop_decreases msgs new_msgs)) = begin match new_msgs with | Betree_List_Cons new_msg new_msgs_tl -> let (i, m) = new_msg in let* msgs1 = betree_Node_apply_to_internal msgs i m in - betree_Node_apply_messages_to_internal msgs1 new_msgs_tl + betree_Node_apply_messages_to_internal_loop msgs1 new_msgs_tl | Betree_List_Nil -> Ok msgs end -(** [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]: - Source: 'src/betree.rs', lines 653:4-656:32 *) -let rec betree_Node_lookup_mut_in_bindings +(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]: + Source: 'src/betree.rs', lines 518:4-521:5 *) +let betree_Node_apply_messages_to_internal + (msgs : betree_List_t (u64 & betree_Message_t)) + (new_msgs : betree_List_t (u64 & betree_Message_t)) : + result (betree_List_t (u64 & betree_Message_t)) + = + betree_Node_apply_messages_to_internal_loop msgs new_msgs + +(** [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]: loop 0: + Source: 'src/betree.rs', lines 664:4-677:5 *) +let rec betree_Node_lookup_mut_in_bindings_loop (key : u64) (bindings : betree_List_t (u64 & u64)) : Tot (result ((betree_List_t (u64 & u64)) & (betree_List_t (u64 & u64) -> result (betree_List_t (u64 & u64))))) - (decreases (betree_Node_lookup_mut_in_bindings_decreases key bindings)) + (decreases (betree_Node_lookup_mut_in_bindings_loop_decreases key bindings)) = begin match bindings with | Betree_List_Cons hd tl -> @@ -451,18 +552,24 @@ let rec betree_Node_lookup_mut_in_bindings if i >= key then Ok (Betree_List_Cons (i, i1) tl, Ok) else - let* (l, lookup_mut_in_bindings_back) = - betree_Node_lookup_mut_in_bindings key tl in - let back = - fun ret -> - let* tl1 = lookup_mut_in_bindings_back ret in - Ok (Betree_List_Cons (i, i1) tl1) in - Ok (l, back) + let* (l, back) = betree_Node_lookup_mut_in_bindings_loop key tl in + let back1 = + fun ret -> let* tl1 = back ret in Ok (Betree_List_Cons (i, i1) tl1) in + Ok (l, back1) | Betree_List_Nil -> Ok (Betree_List_Nil, Ok) end +(** [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]: + Source: 'src/betree.rs', lines 664:4-667:32 *) +let betree_Node_lookup_mut_in_bindings + (key : u64) (bindings : betree_List_t (u64 & u64)) : + result ((betree_List_t (u64 & u64)) & (betree_List_t (u64 & u64) -> result + (betree_List_t (u64 & u64)))) + = + betree_Node_lookup_mut_in_bindings_loop key bindings + (** [betree::betree::{betree::betree::Node#5}::apply_to_leaf]: - Source: 'src/betree.rs', lines 460:4-460:87 *) + Source: 'src/betree.rs', lines 476:4-476:87 *) let betree_Node_apply_to_leaf (bindings : betree_List_t (u64 & u64)) (key : u64) (new_msg : betree_Message_t) : @@ -497,24 +604,34 @@ let betree_Node_apply_to_leaf lookup_mut_in_bindings_back bindings2 end -(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]: - Source: 'src/betree.rs', lines 444:4-447:5 *) -let rec betree_Node_apply_messages_to_leaf +(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]: loop 0: + Source: 'src/betree.rs', lines 463:4-471:5 *) +let rec betree_Node_apply_messages_to_leaf_loop (bindings : betree_List_t (u64 & u64)) (new_msgs : betree_List_t (u64 & betree_Message_t)) : Tot (result (betree_List_t (u64 & u64))) - (decreases (betree_Node_apply_messages_to_leaf_decreases bindings new_msgs)) + (decreases ( + betree_Node_apply_messages_to_leaf_loop_decreases bindings new_msgs)) = begin match new_msgs with | Betree_List_Cons new_msg new_msgs_tl -> let (i, m) = new_msg in let* bindings1 = betree_Node_apply_to_leaf bindings i m in - betree_Node_apply_messages_to_leaf bindings1 new_msgs_tl + betree_Node_apply_messages_to_leaf_loop bindings1 new_msgs_tl | Betree_List_Nil -> Ok bindings end +(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]: + Source: 'src/betree.rs', lines 463:4-466:5 *) +let betree_Node_apply_messages_to_leaf + (bindings : betree_List_t (u64 & u64)) + (new_msgs : betree_List_t (u64 & betree_Message_t)) : + result (betree_List_t (u64 & u64)) + = + betree_Node_apply_messages_to_leaf_loop bindings new_msgs + (** [betree::betree::{betree::betree::Internal#4}::flush]: - Source: 'src/betree.rs', lines 410:4-415:26 *) + Source: 'src/betree.rs', lines 429:4-434:26 *) let rec betree_Internal_flush (self : betree_Internal_t) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) @@ -551,7 +668,7 @@ let rec betree_Internal_flush Ok (st1, (msgs_left, ({ self with right = n }, node_id_cnt1))) (** [betree::betree::{betree::betree::Node#5}::apply_messages]: - Source: 'src/betree.rs', lines 588:4-593:5 *) + Source: 'src/betree.rs', lines 601:4-606:5 *) and betree_Node_apply_messages (self : betree_Node_t) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) @@ -592,7 +709,7 @@ and betree_Node_apply_messages end (** [betree::betree::{betree::betree::Node#5}::apply]: - Source: 'src/betree.rs', lines 576:4-582:5 *) + Source: 'src/betree.rs', lines 589:4-595:5 *) let betree_Node_apply (self : betree_Node_t) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) (key : u64) @@ -606,7 +723,7 @@ let betree_Node_apply Ok (st1, (self1, node_id_cnt1)) (** [betree::betree::{betree::betree::BeTree#6}::new]: - Source: 'src/betree.rs', lines 849:4-849:60 *) + Source: 'src/betree.rs', lines 848:4-848:60 *) let betree_BeTree_new (min_flush_size : u64) (split_size : u64) (st : state) : result (state & betree_BeTree_t) @@ -622,7 +739,7 @@ let betree_BeTree_new }) (** [betree::betree::{betree::betree::BeTree#6}::apply]: - Source: 'src/betree.rs', lines 868:4-868:47 *) + Source: 'src/betree.rs', lines 867:4-867:47 *) let betree_BeTree_apply (self : betree_BeTree_t) (key : u64) (msg : betree_Message_t) (st : state) : result (state & betree_BeTree_t) @@ -633,7 +750,7 @@ let betree_BeTree_apply Ok (st1, { self with node_id_cnt = nic; root = n }) (** [betree::betree::{betree::betree::BeTree#6}::insert]: - Source: 'src/betree.rs', lines 874:4-874:52 *) + Source: 'src/betree.rs', lines 873:4-873:52 *) let betree_BeTree_insert (self : betree_BeTree_t) (key : u64) (value : u64) (st : state) : result (state & betree_BeTree_t) @@ -641,7 +758,7 @@ let betree_BeTree_insert betree_BeTree_apply self key (Betree_Message_Insert value) st (** [betree::betree::{betree::betree::BeTree#6}::delete]: - Source: 'src/betree.rs', lines 880:4-880:38 *) + Source: 'src/betree.rs', lines 879:4-879:38 *) let betree_BeTree_delete (self : betree_BeTree_t) (key : u64) (st : state) : result (state & betree_BeTree_t) @@ -649,7 +766,7 @@ let betree_BeTree_delete betree_BeTree_apply self key Betree_Message_Delete st (** [betree::betree::{betree::betree::BeTree#6}::upsert]: - Source: 'src/betree.rs', lines 886:4-886:59 *) + Source: 'src/betree.rs', lines 885:4-885:59 *) let betree_BeTree_upsert (self : betree_BeTree_t) (key : u64) (upd : betree_UpsertFunState_t) (st : state) : @@ -658,7 +775,7 @@ let betree_BeTree_upsert betree_BeTree_apply self key (Betree_Message_Upsert upd) st (** [betree::betree::{betree::betree::BeTree#6}::lookup]: - Source: 'src/betree.rs', lines 895:4-895:62 *) + Source: 'src/betree.rs', lines 894:4-894:62 *) let betree_BeTree_lookup (self : betree_BeTree_t) (key : u64) (st : state) : result (state & ((option u64) & betree_BeTree_t)) diff --git a/tests/lean/Betree/Funs.lean b/tests/lean/Betree/Funs.lean index 8612ccbc..7d8b4714 100644 --- a/tests/lean/Betree/Funs.lean +++ b/tests/lean/Betree/Funs.lean @@ -79,42 +79,74 @@ def betree.upsert_update then prev1 - v else Result.ok 0#u64 +/- [betree::betree::{betree::betree::List<T>#1}::len]: loop 0: + Source: 'src/betree.rs', lines 276:4-284:5 -/ +divergent def betree.List.len_loop + (T : Type) (self : betree.List T) (len : U64) : Result U64 := + match self with + | betree.List.Cons _ tl => + do + let len1 ← len + 1#u64 + betree.List.len_loop T tl len1 + | betree.List.Nil => Result.ok len + /- [betree::betree::{betree::betree::List<T>#1}::len]: Source: 'src/betree.rs', lines 276:4-276:24 -/ -divergent def betree.List.len (T : Type) (self : betree.List T) : Result U64 := +def betree.List.len (T : Type) (self : betree.List T) : Result U64 := + betree.List.len_loop T self 0#u64 + +/- [betree::betree::{betree::betree::List<T>#1}::reverse]: loop 0: + Source: 'src/betree.rs', lines 304:4-312:5 -/ +divergent def betree.List.reverse_loop + (T : Type) (self : betree.List T) (out : betree.List T) : + Result (betree.List T) + := match self with - | betree.List.Cons _ tl => do - let i ← betree.List.len T tl - 1#u64 + i - | betree.List.Nil => Result.ok 0#u64 - -/- [betree::betree::{betree::betree::List<T>#1}::split_at]: - Source: 'src/betree.rs', lines 284:4-284:51 -/ -divergent def betree.List.split_at - (T : Type) (self : betree.List T) (n : U64) : + | betree.List.Cons hd tl => + betree.List.reverse_loop T tl (betree.List.Cons hd out) + | betree.List.Nil => Result.ok out + +/- [betree::betree::{betree::betree::List<T>#1}::reverse]: + Source: 'src/betree.rs', lines 304:4-304:32 -/ +def betree.List.reverse + (T : Type) (self : betree.List T) : Result (betree.List T) := + betree.List.reverse_loop T self betree.List.Nil + +/- [betree::betree::{betree::betree::List<T>#1}::split_at]: loop 0: + Source: 'src/betree.rs', lines 287:4-302:5 -/ +divergent def betree.List.split_at_loop + (T : Type) (n : U64) (beg : betree.List T) (self : betree.List T) : Result ((betree.List T) × (betree.List T)) := - if n = 0#u64 - then Result.ok (betree.List.Nil, self) - else + if n > 0#u64 + then match self with | betree.List.Cons hd tl => do - let i ← n - 1#u64 - let p ← betree.List.split_at T tl i - let (ls0, ls1) := p - Result.ok (betree.List.Cons hd ls0, ls1) + let n1 ← n - 1#u64 + betree.List.split_at_loop T n1 (betree.List.Cons hd beg) tl | betree.List.Nil => Result.fail .panic + else do + let l ← betree.List.reverse T beg + Result.ok (l, self) + +/- [betree::betree::{betree::betree::List<T>#1}::split_at]: + Source: 'src/betree.rs', lines 287:4-287:55 -/ +def betree.List.split_at + (T : Type) (self : betree.List T) (n : U64) : + Result ((betree.List T) × (betree.List T)) + := + betree.List.split_at_loop T n betree.List.Nil self /- [betree::betree::{betree::betree::List<T>#1}::push_front]: - Source: 'src/betree.rs', lines 299:4-299:34 -/ + Source: 'src/betree.rs', lines 315:4-315:34 -/ def betree.List.push_front (T : Type) (self : betree.List T) (x : T) : Result (betree.List T) := let (tl, _) := core.mem.replace (betree.List T) self betree.List.Nil Result.ok (betree.List.Cons x tl) /- [betree::betree::{betree::betree::List<T>#1}::pop_front]: - Source: 'src/betree.rs', lines 306:4-306:32 -/ + Source: 'src/betree.rs', lines 322:4-322:32 -/ def betree.List.pop_front (T : Type) (self : betree.List T) : Result (T × (betree.List T)) := let (ls, _) := core.mem.replace (betree.List T) self betree.List.Nil @@ -123,14 +155,14 @@ def betree.List.pop_front | betree.List.Nil => Result.fail .panic /- [betree::betree::{betree::betree::List<T>#1}::hd]: - Source: 'src/betree.rs', lines 318:4-318:22 -/ + Source: 'src/betree.rs', lines 334:4-334:22 -/ def betree.List.hd (T : Type) (self : betree.List T) : Result T := match self with | betree.List.Cons hd _ => Result.ok hd | betree.List.Nil => Result.fail .panic /- [betree::betree::{betree::betree::List<(u64, T)>#2}::head_has_key]: - Source: 'src/betree.rs', lines 327:4-327:44 -/ + Source: 'src/betree.rs', lines 343:4-343:44 -/ def betree.ListPairU64T.head_has_key (T : Type) (self : betree.List (U64 × T)) (key : U64) : Result Bool := match self with @@ -138,26 +170,40 @@ def betree.ListPairU64T.head_has_key Result.ok (i = key) | betree.List.Nil => Result.ok false -/- [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]: - Source: 'src/betree.rs', lines 339:4-339:73 -/ -divergent def betree.ListPairU64T.partition_at_pivot - (T : Type) (self : betree.List (U64 × T)) (pivot : U64) : +/- [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]: loop 0: + Source: 'src/betree.rs', lines 355:4-370:5 -/ +divergent def betree.ListPairU64T.partition_at_pivot_loop + (T : Type) (pivot : U64) (beg : betree.List (U64 × T)) + (end1 : betree.List (U64 × T)) (self : betree.List (U64 × T)) : Result ((betree.List (U64 × T)) × (betree.List (U64 × T))) := match self with | betree.List.Cons hd tl => let (i, t) := hd if i >= pivot - then Result.ok (betree.List.Nil, betree.List.Cons (i, t) tl) + then + betree.ListPairU64T.partition_at_pivot_loop T pivot beg (betree.List.Cons + (i, t) end1) tl else - do - let p ← betree.ListPairU64T.partition_at_pivot T tl pivot - let (ls0, ls1) := p - Result.ok (betree.List.Cons (i, t) ls0, ls1) - | betree.List.Nil => Result.ok (betree.List.Nil, betree.List.Nil) + betree.ListPairU64T.partition_at_pivot_loop T pivot (betree.List.Cons (i, + t) beg) end1 tl + | betree.List.Nil => + do + let l ← betree.List.reverse (U64 × T) beg + let l1 ← betree.List.reverse (U64 × T) end1 + Result.ok (l, l1) + +/- [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]: + Source: 'src/betree.rs', lines 355:4-355:73 -/ +def betree.ListPairU64T.partition_at_pivot + (T : Type) (self : betree.List (U64 × T)) (pivot : U64) : + Result ((betree.List (U64 × T)) × (betree.List (U64 × T))) + := + betree.ListPairU64T.partition_at_pivot_loop T pivot betree.List.Nil + betree.List.Nil self /- [betree::betree::{betree::betree::Leaf#3}::split]: - Source: 'src/betree.rs', lines 359:4-364:17 -/ + Source: 'src/betree.rs', lines 378:4-383:17 -/ def betree.Leaf.split (self : betree.Leaf) (content : betree.List (U64 × U64)) (params : betree.Params) (node_id_cnt : betree.NodeIdCounter) (st : State) : @@ -176,9 +222,9 @@ def betree.Leaf.split let n1 := betree.Node.Leaf { id := id1, size := params.split_size } Result.ok (st2, (betree.Internal.mk self.id pivot n n1, node_id_cnt2)) -/- [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]: - Source: 'src/betree.rs', lines 789:4-792:34 -/ -divergent def betree.Node.lookup_first_message_for_key +/- [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]: loop 0: + Source: 'src/betree.rs', lines 792:4-810:5 -/ +divergent def betree.Node.lookup_first_message_for_key_loop (key : U64) (msgs : betree.List (U64 × betree.Message)) : Result ((betree.List (U64 × betree.Message)) × (betree.List (U64 × betree.Message) → Result (betree.List (U64 × betree.Message)))) @@ -190,19 +236,28 @@ divergent def betree.Node.lookup_first_message_for_key then Result.ok (betree.List.Cons (i, m) next_msgs, Result.ok) else do - let (l, lookup_first_message_for_key_back) ← - betree.Node.lookup_first_message_for_key key next_msgs - let back := + let (l, back) ← + betree.Node.lookup_first_message_for_key_loop key next_msgs + let back1 := fun ret => do - let next_msgs1 ← lookup_first_message_for_key_back ret + let next_msgs1 ← back ret Result.ok (betree.List.Cons (i, m) next_msgs1) - Result.ok (l, back) + Result.ok (l, back1) | betree.List.Nil => Result.ok (betree.List.Nil, Result.ok) -/- [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: - Source: 'src/betree.rs', lines 636:4-636:80 -/ -divergent def betree.Node.lookup_in_bindings +/- [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]: + Source: 'src/betree.rs', lines 792:4-795:34 -/ +def betree.Node.lookup_first_message_for_key + (key : U64) (msgs : betree.List (U64 × betree.Message)) : + Result ((betree.List (U64 × betree.Message)) × (betree.List (U64 × + betree.Message) → Result (betree.List (U64 × betree.Message)))) + := + betree.Node.lookup_first_message_for_key_loop key msgs + +/- [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: loop 0: + Source: 'src/betree.rs', lines 649:4-660:5 -/ +divergent def betree.Node.lookup_in_bindings_loop (key : U64) (bindings : betree.List (U64 × U64)) : Result (Option U64) := match bindings with | betree.List.Cons hd tl => @@ -212,12 +267,18 @@ divergent def betree.Node.lookup_in_bindings else if i > key then Result.ok none - else betree.Node.lookup_in_bindings key tl + else betree.Node.lookup_in_bindings_loop key tl | betree.List.Nil => Result.ok none -/- [betree::betree::{betree::betree::Node#5}::apply_upserts]: - Source: 'src/betree.rs', lines 819:4-819:90 -/ -divergent def betree.Node.apply_upserts +/- [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: + Source: 'src/betree.rs', lines 649:4-649:84 -/ +def betree.Node.lookup_in_bindings + (key : U64) (bindings : betree.List (U64 × U64)) : Result (Option U64) := + betree.Node.lookup_in_bindings_loop key bindings + +/- [betree::betree::{betree::betree::Node#5}::apply_upserts]: loop 0: + Source: 'src/betree.rs', lines 820:4-844:5 -/ +divergent def betree.Node.apply_upserts_loop (msgs : betree.List (U64 × betree.Message)) (prev : Option U64) (key : U64) : Result (U64 × (betree.List (U64 × betree.Message))) @@ -235,7 +296,7 @@ divergent def betree.Node.apply_upserts | betree.Message.Upsert s => do let v ← betree.upsert_update prev s - betree.Node.apply_upserts msgs1 (some v) key + betree.Node.apply_upserts_loop msgs1 (some v) key else do let v ← core.option.Option.unwrap U64 prev @@ -244,8 +305,17 @@ divergent def betree.Node.apply_upserts betree.Message.Insert v) Result.ok (v, msgs1) +/- [betree::betree::{betree::betree::Node#5}::apply_upserts]: + Source: 'src/betree.rs', lines 820:4-820:94 -/ +def betree.Node.apply_upserts + (msgs : betree.List (U64 × betree.Message)) (prev : Option U64) (key : U64) + : + Result (U64 × (betree.List (U64 × betree.Message))) + := + betree.Node.apply_upserts_loop msgs prev key + /- [betree::betree::{betree::betree::Internal#4}::lookup_in_children]: - Source: 'src/betree.rs', lines 395:4-395:63 -/ + Source: 'src/betree.rs', lines 414:4-414:63 -/ mutual divergent def betree.Internal.lookup_in_children (self : betree.Internal) (key : U64) (st : State) : Result (State × ((Option U64) × betree.Internal)) @@ -261,7 +331,7 @@ mutual divergent def betree.Internal.lookup_in_children Result.ok (st1, (o, betree.Internal.mk self.id self.pivot self.left n)) /- [betree::betree::{betree::betree::Node#5}::lookup]: - Source: 'src/betree.rs', lines 709:4-709:58 -/ + Source: 'src/betree.rs', lines 712:4-712:58 -/ divergent def betree.Node.lookup (self : betree.Node) (key : U64) (st : State) : Result (State × ((Option U64) × betree.Node)) @@ -320,9 +390,9 @@ divergent def betree.Node.lookup end -/- [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]: - Source: 'src/betree.rs', lines 674:4-674:77 -/ -divergent def betree.Node.filter_messages_for_key +/- [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]: loop 0: + Source: 'src/betree.rs', lines 683:4-692:5 -/ +divergent def betree.Node.filter_messages_for_key_loop (key : U64) (msgs : betree.List (U64 × betree.Message)) : Result (betree.List (U64 × betree.Message)) := @@ -335,13 +405,21 @@ divergent def betree.Node.filter_messages_for_key let (_, msgs1) ← betree.List.pop_front (U64 × betree.Message) (betree.List.Cons (k, m) l) - betree.Node.filter_messages_for_key key msgs1 + betree.Node.filter_messages_for_key_loop key msgs1 else Result.ok (betree.List.Cons (k, m) l) | betree.List.Nil => Result.ok betree.List.Nil -/- [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]: - Source: 'src/betree.rs', lines 689:4-692:34 -/ -divergent def betree.Node.lookup_first_message_after_key +/- [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]: + Source: 'src/betree.rs', lines 683:4-683:77 -/ +def betree.Node.filter_messages_for_key + (key : U64) (msgs : betree.List (U64 × betree.Message)) : + Result (betree.List (U64 × betree.Message)) + := + betree.Node.filter_messages_for_key_loop key msgs + +/- [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]: loop 0: + Source: 'src/betree.rs', lines 694:4-706:5 -/ +divergent def betree.Node.lookup_first_message_after_key_loop (key : U64) (msgs : betree.List (U64 × betree.Message)) : Result ((betree.List (U64 × betree.Message)) × (betree.List (U64 × betree.Message) → Result (betree.List (U64 × betree.Message)))) @@ -352,19 +430,28 @@ divergent def betree.Node.lookup_first_message_after_key if k = key then do - let (l, lookup_first_message_after_key_back) ← - betree.Node.lookup_first_message_after_key key next_msgs - let back := + let (l, back) ← + betree.Node.lookup_first_message_after_key_loop key next_msgs + let back1 := fun ret => do - let next_msgs1 ← lookup_first_message_after_key_back ret + let next_msgs1 ← back ret Result.ok (betree.List.Cons (k, m) next_msgs1) - Result.ok (l, back) + Result.ok (l, back1) else Result.ok (betree.List.Cons (k, m) next_msgs, Result.ok) | betree.List.Nil => Result.ok (betree.List.Nil, Result.ok) +/- [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]: + Source: 'src/betree.rs', lines 694:4-697:34 -/ +def betree.Node.lookup_first_message_after_key + (key : U64) (msgs : betree.List (U64 × betree.Message)) : + Result ((betree.List (U64 × betree.Message)) × (betree.List (U64 × + betree.Message) → Result (betree.List (U64 × betree.Message)))) + := + betree.Node.lookup_first_message_after_key_loop key msgs + /- [betree::betree::{betree::betree::Node#5}::apply_to_internal]: - Source: 'src/betree.rs', lines 521:4-521:89 -/ + Source: 'src/betree.rs', lines 534:4-534:89 -/ def betree.Node.apply_to_internal (msgs : betree.List (U64 × betree.Message)) (key : U64) (new_msg : betree.Message) : @@ -427,9 +514,9 @@ def betree.Node.apply_to_internal betree.List.push_front (U64 × betree.Message) msgs1 (key, new_msg) lookup_first_message_for_key_back msgs2 -/- [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]: - Source: 'src/betree.rs', lines 502:4-505:5 -/ -divergent def betree.Node.apply_messages_to_internal +/- [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]: loop 0: + Source: 'src/betree.rs', lines 518:4-526:5 -/ +divergent def betree.Node.apply_messages_to_internal_loop (msgs : betree.List (U64 × betree.Message)) (new_msgs : betree.List (U64 × betree.Message)) : Result (betree.List (U64 × betree.Message)) @@ -439,12 +526,21 @@ divergent def betree.Node.apply_messages_to_internal do let (i, m) := new_msg let msgs1 ← betree.Node.apply_to_internal msgs i m - betree.Node.apply_messages_to_internal msgs1 new_msgs_tl + betree.Node.apply_messages_to_internal_loop msgs1 new_msgs_tl | betree.List.Nil => Result.ok msgs -/- [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]: - Source: 'src/betree.rs', lines 653:4-656:32 -/ -divergent def betree.Node.lookup_mut_in_bindings +/- [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]: + Source: 'src/betree.rs', lines 518:4-521:5 -/ +def betree.Node.apply_messages_to_internal + (msgs : betree.List (U64 × betree.Message)) + (new_msgs : betree.List (U64 × betree.Message)) : + Result (betree.List (U64 × betree.Message)) + := + betree.Node.apply_messages_to_internal_loop msgs new_msgs + +/- [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]: loop 0: + Source: 'src/betree.rs', lines 664:4-677:5 -/ +divergent def betree.Node.lookup_mut_in_bindings_loop (key : U64) (bindings : betree.List (U64 × U64)) : Result ((betree.List (U64 × U64)) × (betree.List (U64 × U64) → Result (betree.List (U64 × U64)))) @@ -456,18 +552,26 @@ divergent def betree.Node.lookup_mut_in_bindings then Result.ok (betree.List.Cons (i, i1) tl, Result.ok) else do - let (l, lookup_mut_in_bindings_back) ← - betree.Node.lookup_mut_in_bindings key tl - let back := + let (l, back) ← betree.Node.lookup_mut_in_bindings_loop key tl + let back1 := fun ret => do - let tl1 ← lookup_mut_in_bindings_back ret + let tl1 ← back ret Result.ok (betree.List.Cons (i, i1) tl1) - Result.ok (l, back) + Result.ok (l, back1) | betree.List.Nil => Result.ok (betree.List.Nil, Result.ok) +/- [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]: + Source: 'src/betree.rs', lines 664:4-667:32 -/ +def betree.Node.lookup_mut_in_bindings + (key : U64) (bindings : betree.List (U64 × U64)) : + Result ((betree.List (U64 × U64)) × (betree.List (U64 × U64) → Result + (betree.List (U64 × U64)))) + := + betree.Node.lookup_mut_in_bindings_loop key bindings + /- [betree::betree::{betree::betree::Node#5}::apply_to_leaf]: - Source: 'src/betree.rs', lines 460:4-460:87 -/ + Source: 'src/betree.rs', lines 476:4-476:87 -/ def betree.Node.apply_to_leaf (bindings : betree.List (U64 × U64)) (key : U64) (new_msg : betree.Message) : @@ -506,9 +610,9 @@ def betree.Node.apply_to_leaf let bindings2 ← betree.List.push_front (U64 × U64) bindings1 (key, v) lookup_mut_in_bindings_back bindings2 -/- [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]: - Source: 'src/betree.rs', lines 444:4-447:5 -/ -divergent def betree.Node.apply_messages_to_leaf +/- [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]: loop 0: + Source: 'src/betree.rs', lines 463:4-471:5 -/ +divergent def betree.Node.apply_messages_to_leaf_loop (bindings : betree.List (U64 × U64)) (new_msgs : betree.List (U64 × betree.Message)) : Result (betree.List (U64 × U64)) @@ -518,11 +622,20 @@ divergent def betree.Node.apply_messages_to_leaf do let (i, m) := new_msg let bindings1 ← betree.Node.apply_to_leaf bindings i m - betree.Node.apply_messages_to_leaf bindings1 new_msgs_tl + betree.Node.apply_messages_to_leaf_loop bindings1 new_msgs_tl | betree.List.Nil => Result.ok bindings +/- [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]: + Source: 'src/betree.rs', lines 463:4-466:5 -/ +def betree.Node.apply_messages_to_leaf + (bindings : betree.List (U64 × U64)) + (new_msgs : betree.List (U64 × betree.Message)) : + Result (betree.List (U64 × U64)) + := + betree.Node.apply_messages_to_leaf_loop bindings new_msgs + /- [betree::betree::{betree::betree::Internal#4}::flush]: - Source: 'src/betree.rs', lines 410:4-415:26 -/ + Source: 'src/betree.rs', lines 429:4-434:26 -/ mutual divergent def betree.Internal.flush (self : betree.Internal) (params : betree.Params) (node_id_cnt : betree.NodeIdCounter) @@ -563,7 +676,7 @@ mutual divergent def betree.Internal.flush self.left n, node_id_cnt1))) /- [betree::betree::{betree::betree::Node#5}::apply_messages]: - Source: 'src/betree.rs', lines 588:4-593:5 -/ + Source: 'src/betree.rs', lines 601:4-606:5 -/ divergent def betree.Node.apply_messages (self : betree.Node) (params : betree.Params) (node_id_cnt : betree.NodeIdCounter) @@ -610,7 +723,7 @@ divergent def betree.Node.apply_messages end /- [betree::betree::{betree::betree::Node#5}::apply]: - Source: 'src/betree.rs', lines 576:4-582:5 -/ + Source: 'src/betree.rs', lines 589:4-595:5 -/ def betree.Node.apply (self : betree.Node) (params : betree.Params) (node_id_cnt : betree.NodeIdCounter) (key : U64) (new_msg : betree.Message) @@ -625,7 +738,7 @@ def betree.Node.apply Result.ok (st1, (self1, node_id_cnt1)) /- [betree::betree::{betree::betree::BeTree#6}::new]: - Source: 'src/betree.rs', lines 849:4-849:60 -/ + Source: 'src/betree.rs', lines 848:4-848:60 -/ def betree.BeTree.new (min_flush_size : U64) (split_size : U64) (st : State) : Result (State × betree.BeTree) @@ -642,7 +755,7 @@ def betree.BeTree.new }) /- [betree::betree::{betree::betree::BeTree#6}::apply]: - Source: 'src/betree.rs', lines 868:4-868:47 -/ + Source: 'src/betree.rs', lines 867:4-867:47 -/ def betree.BeTree.apply (self : betree.BeTree) (key : U64) (msg : betree.Message) (st : State) : Result (State × betree.BeTree) @@ -654,7 +767,7 @@ def betree.BeTree.apply Result.ok (st1, { self with node_id_cnt := nic, root := n }) /- [betree::betree::{betree::betree::BeTree#6}::insert]: - Source: 'src/betree.rs', lines 874:4-874:52 -/ + Source: 'src/betree.rs', lines 873:4-873:52 -/ def betree.BeTree.insert (self : betree.BeTree) (key : U64) (value : U64) (st : State) : Result (State × betree.BeTree) @@ -662,7 +775,7 @@ def betree.BeTree.insert betree.BeTree.apply self key (betree.Message.Insert value) st /- [betree::betree::{betree::betree::BeTree#6}::delete]: - Source: 'src/betree.rs', lines 880:4-880:38 -/ + Source: 'src/betree.rs', lines 879:4-879:38 -/ def betree.BeTree.delete (self : betree.BeTree) (key : U64) (st : State) : Result (State × betree.BeTree) @@ -670,7 +783,7 @@ def betree.BeTree.delete betree.BeTree.apply self key betree.Message.Delete st /- [betree::betree::{betree::betree::BeTree#6}::upsert]: - Source: 'src/betree.rs', lines 886:4-886:59 -/ + Source: 'src/betree.rs', lines 885:4-885:59 -/ def betree.BeTree.upsert (self : betree.BeTree) (key : U64) (upd : betree.UpsertFunState) (st : State) : @@ -679,7 +792,7 @@ def betree.BeTree.upsert betree.BeTree.apply self key (betree.Message.Upsert upd) st /- [betree::betree::{betree::betree::BeTree#6}::lookup]: - Source: 'src/betree.rs', lines 895:4-895:62 -/ + Source: 'src/betree.rs', lines 894:4-894:62 -/ def betree.BeTree.lookup (self : betree.BeTree) (key : U64) (st : State) : Result (State × ((Option U64) × betree.BeTree)) diff --git a/tests/src/betree/aeneas-test-options b/tests/src/betree/aeneas-test-options index c71e01df..5a1e4180 100644 --- a/tests/src/betree/aeneas-test-options +++ b/tests/src/betree/aeneas-test-options @@ -1,4 +1,4 @@ charon-args=--polonius --opaque=betree_utils -aeneas-args=-backward-no-state-update -test-trans-units -state -split-files +[!borrow-check] aeneas-args=-backward-no-state-update -test-trans-units -state -split-files [coq] aeneas-args=-use-fuel [fstar] aeneas-args=-decreases-clauses -template-clauses diff --git a/tests/src/betree/src/betree.rs b/tests/src/betree/src/betree.rs index 12f2847d..8ba07824 100644 --- a/tests/src/betree/src/betree.rs +++ b/tests/src/betree/src/betree.rs @@ -274,25 +274,41 @@ pub fn upsert_update(prev: Option<Value>, st: UpsertFunState) -> Value { impl<T> List<T> { fn len(&self) -> u64 { - match self { - List::Nil => 0, - List::Cons(_, tl) => 1 + tl.len(), + let mut l = self; + let mut len = 0; + while let List::Cons(_, tl) = l { + len += 1; + l = tl; } + len } /// Split a list at a given length - fn split_at(self, n: u64) -> (List<T>, List<T>) { - if n == 0 { - (List::Nil, self) - } else { - match self { + fn split_at(self, mut n: u64) -> (List<T>, List<T>) { + let mut beg = List::Nil; + let mut end = self; + while n > 0 { + match end { List::Nil => unreachable!(), - List::Cons(hd, tl) => { - let (ls0, ls1) = tl.split_at(n - 1); - (List::Cons(hd, Box::new(ls0)), ls1) + List::Cons(hd, mut tl) => { + n -= 1; + end = *tl; + *tl = beg; + beg = List::Cons(hd, tl); } } } + (beg.reverse(), end) + } + + fn reverse(mut self) -> Self { + let mut out = List::Nil; + while let List::Cons(hd, mut tl) = self { + self = *tl; + *tl = out; + out = List::Cons(hd, tl); + } + out } /// Push an element at the front of the list. @@ -337,17 +353,20 @@ impl<T> Map<Key, T> { /// Note that the bindings in the map are supposed to be sorted in /// order of increasing keys. fn partition_at_pivot(self, pivot: Key) -> (Map<Key, T>, Map<Key, T>) { - match self { - List::Nil => (List::Nil, List::Nil), - List::Cons(hd, tl) => { - if hd.0 >= pivot { - (List::Nil, List::Cons(hd, tl)) - } else { - let (ls0, ls1) = tl.partition_at_pivot(pivot); - (List::Cons(hd, Box::new(ls0)), ls1) - } + let mut beg = List::Nil; + let mut end = List::Nil; + let mut curr = self; + while let List::Cons(hd, mut tl) = curr { + curr = *tl; + if hd.0 >= pivot { + *tl = end; + end = List::Cons(hd, tl); + } else { + *tl = beg; + beg = List::Cons(hd, tl); } } + (beg.reverse(), end.reverse()) } } @@ -443,14 +462,11 @@ impl Node { /// Apply a list of message to ourselves: leaf node case fn apply_messages_to_leaf<'a>( bindings: &'a mut Map<Key, Value>, - new_msgs: List<(Key, Message)>, + mut new_msgs: List<(Key, Message)>, ) { - match new_msgs { - List::Nil => (), - List::Cons(new_msg, new_msgs_tl) => { - Node::apply_to_leaf(bindings, new_msg.0, new_msg.1); - Node::apply_messages_to_leaf(bindings, *new_msgs_tl); - } + while let List::Cons(new_msg, new_msgs_tl) = new_msgs { + Node::apply_to_leaf(bindings, new_msg.0, new_msg.1); + new_msgs = *new_msgs_tl; } } @@ -501,14 +517,11 @@ impl Node { /// Apply a list of message to ourselves: internal node case fn apply_messages_to_internal<'a>( msgs: &'a mut Map<Key, Message>, - new_msgs: List<(Key, Message)>, + mut new_msgs: List<(Key, Message)>, ) { - match new_msgs { - List::Nil => (), - List::Cons(new_msg, new_msgs_tl) => { - Node::apply_to_internal(msgs, new_msg.0, new_msg.1); - Node::apply_messages_to_internal(msgs, *new_msgs_tl); - } + while let List::Cons(new_msg, new_msgs_tl) = new_msgs { + Node::apply_to_internal(msgs, new_msg.0, new_msg.1); + new_msgs = *new_msgs_tl; } } @@ -633,38 +646,34 @@ impl Node { /// Lookup a value in a list of bindings. /// Note that the values should be stored in order of increasing key. - fn lookup_in_bindings(key: Key, bindings: &Map<Key, Value>) -> Option<Value> { - match bindings { - List::Nil => Option::None, - List::Cons(hd, tl) => { - if hd.0 == key { - Option::Some(hd.1) - } else if hd.0 > key { - Option::None - } else { - Node::lookup_in_bindings(key, tl) - } + fn lookup_in_bindings(key: Key, mut bindings: &Map<Key, Value>) -> Option<Value> { + while let List::Cons(hd, tl) = bindings { + if hd.0 == key { + return Option::Some(hd.1); + } else if hd.0 > key { + return Option::None; + } else { + bindings = tl; } } + Option::None } /// Lookup a value in a list of bindings, and return a borrow to the position /// where the value is (or should be inserted, if the key is not in the bindings). fn lookup_mut_in_bindings<'a>( key: Key, - bindings: &'a mut Map<Key, Value>, + mut bindings: &'a mut Map<Key, Value>, ) -> &'a mut Map<Key, Value> { - match bindings { - List::Nil => bindings, - List::Cons(hd, tl) => { - // This requires Polonius - if hd.0 >= key { - bindings - } else { - Node::lookup_mut_in_bindings(key, tl) - } + while let List::Cons(hd, tl) = bindings { + // This requires Polonius + if hd.0 >= key { + break; + } else { + bindings = tl; } } + bindings } /// Filter all the messages which concern [key]. @@ -672,34 +681,28 @@ impl Node { /// Note that the stack of messages must start with a message for [key]: /// we stop filtering at the first message which is not about [key]. fn filter_messages_for_key<'a>(key: Key, msgs: &'a mut Map<Key, Message>) { - match msgs { - List::Nil => (), - List::Cons((k, _), _) => { - if *k == key { - msgs.pop_front(); - Node::filter_messages_for_key(key, msgs); - } else { - // Stop - () - } + while let List::Cons((k, _), _) = msgs { + if *k == key { + msgs.pop_front(); + } else { + // Stop + break; } } } fn lookup_first_message_after_key<'a>( key: Key, - msgs: &'a mut Map<Key, Message>, + mut msgs: &'a mut Map<Key, Message>, ) -> &'a mut Map<Key, Message> { - match msgs { - List::Nil => msgs, - List::Cons((k, _), next_msgs) => { - if *k == key { - Node::lookup_first_message_after_key(key, next_msgs) - } else { - msgs - } + while let List::Cons((k, _), next_msgs) = msgs { + if *k == key { + msgs = next_msgs; + } else { + break; } } + return msgs; } /// Returns the value bound to a key. @@ -788,24 +791,22 @@ impl Node { /// of the list). fn lookup_first_message_for_key<'a>( key: Key, - msgs: &'a mut Map<Key, Message>, + mut msgs: &'a mut Map<Key, Message>, ) -> &'a mut Map<Key, Message> { - match msgs { - List::Nil => msgs, - List::Cons(x, next_msgs) => { - // Rk.: we need Polonius here - // We wouldn't need Polonius if directly called the proper - // function to make the modifications here (because we wouldn't - // need to return anything). However, it would not be very - // idiomatic, especially with regards to the fact that we will - // rewrite everything with loops at some point. - if x.0 >= key { - msgs - } else { - Node::lookup_first_message_for_key(key, next_msgs) - } + while let List::Cons(x, next_msgs) = msgs { + // Rk.: we need Polonius here + // We wouldn't need Polonius if directly called the proper + // function to make the modifications here (because we wouldn't + // need to return anything). However, it would not be very + // idiomatic, especially with regards to the fact that we will + // rewrite everything with loops at some point. + if x.0 >= key { + return msgs; + } else { + msgs = next_msgs; } } + msgs } /// Apply the upserts from the current messages stack to a looked up value. @@ -816,8 +817,8 @@ impl Node { /// Note that if there are no more upserts to apply, then the value must be /// `Some`. Also note that we use the invariant that in the message stack, /// upsert messages are sorted from the first to the last to apply. - fn apply_upserts(msgs: &mut Map<Key, Message>, prev: Option<Value>, key: Key) -> Value { - if msgs.head_has_key(key) { + fn apply_upserts(msgs: &mut Map<Key, Message>, mut prev: Option<Value>, key: Key) -> Value { + while msgs.head_has_key(key) { // Pop the front message. // Note that it *must* be an upsert. let msg = msgs.pop_front(); @@ -825,9 +826,8 @@ impl Node { Message::Upsert(s) => { // Apply the update let v = upsert_update(prev, s); - let prev = Option::Some(v); + prev = Option::Some(v); // Continue - Node::apply_upserts(msgs, prev, key) } _ => { // Unreachable: we can only have [Upsert] messages @@ -835,13 +835,12 @@ impl Node { unreachable!(); } } - } else { - // We applied all the upsert messages: simply put an [Insert] - // message and return the value. - let v = prev.unwrap(); - msgs.push_front((key, Message::Insert(v))); - return v; } + // We applied all the upsert messages: simply put an [Insert] + // message and return the value. + let v = prev.unwrap(); + msgs.push_front((key, Message::Insert(v))); + v } } diff --git a/tests/src/bitwise.rs b/tests/src/bitwise.rs index fda8eff3..be12cea0 100644 --- a/tests/src/bitwise.rs +++ b/tests/src/bitwise.rs @@ -1,4 +1,4 @@ -//@ aeneas-args=-test-trans-units +//@ [!borrow-check] aeneas-args=-test-trans-units //@ [coq,fstar] subdir=misc //! Exercise the bitwise operations diff --git a/tests/src/borrow-check-negative.borrow-check.out b/tests/src/borrow-check-negative.borrow-check.out new file mode 100644 index 00000000..dc9dd5a7 --- /dev/null +++ b/tests/src/borrow-check-negative.borrow-check.out @@ -0,0 +1,15 @@ +[[92mInfo[39m ] Imported: tests/llbc/borrow_check_negative.llbc +[[91mError[39m] Can not apply a projection to the ⊥ value +Source: 'tests/src/borrow-check-negative.rs', lines 17:4-24:1 +[[91mError[39m] Can't end abstraction 8 as it is set as non-endable +Source: 'tests/src/borrow-check-negative.rs', lines 26:0-26:76 +[[91mError[39m] Can not apply a projection to the ⊥ value +Source: 'tests/src/borrow-check-negative.rs', lines 37:4-41:1 +[[91mError[39m] Can not apply a projection to the ⊥ value +Source: 'tests/src/borrow-check-negative.rs', lines 47:4-50:1 +[[91mError[39m] Can not apply a projection to the ⊥ value +Source: 'tests/src/borrow-check-negative.rs', lines 60:4-64:1 +[[91mError[39m] Can not apply a projection to the ⊥ value +Source: 'tests/src/borrow-check-negative.rs', lines 71:4-79:1 +[[91mError[39m] Can not apply a projection to the ⊥ value +Source: 'tests/src/borrow-check-negative.rs', lines 87:4-90:1 diff --git a/tests/src/borrow-check-negative.rs b/tests/src/borrow-check-negative.rs new file mode 100644 index 00000000..697546dd --- /dev/null +++ b/tests/src/borrow-check-negative.rs @@ -0,0 +1,90 @@ +//@ [!borrow-check] skip +//@ [borrow-check] known-failure +// Some negative tests for borrow checking + +// This succeeds +fn choose<'a, T>(b: bool, x: &'a mut T, y: &'a mut T) -> &'a mut T { + if b { + x + } else { + y + } +} + +pub fn choose_test() { + let mut x = 0; + let mut y = 0; + let z = choose(true, &mut x, &mut y); + *z += 1; + assert!(*z == 1); + // drop(z) + assert!(x == 1); + assert!(y == 0); + assert!(*z == 1); // z is not valid anymore +} + +fn choose_wrong<'a, 'b, T>(b: bool, x: &'a mut T, y: &'b mut T) -> &'a mut T { + if b { + x + } else { + y // Expected lifetime 'a + } +} + +fn test_mut1(b: bool) { + let mut x = 0; + let mut y = 1; + let z = if b { &mut x } else { &mut y }; + *z += 1; + assert!(x >= 0); + *z += 1; // z is not valid anymore +} + +#[allow(unused_assignments)] +fn test_mut2(b: bool) { + let mut x = 0; + let mut y = 1; + let z = if b { &x } else { &y }; + x += 1; + assert!(*z == 0); // z is not valid anymore +} + +fn test_move1<T>(x: T) -> T { + let _ = x; + return x; // x has been moved +} + +pub fn refs_test1() { + let mut x = 0; + let mut px = &mut x; + let ppx = &mut px; + **ppx = 1; + assert!(x == 1); + assert!(**ppx == 1); // ppx has ended +} + +pub fn refs_test2() { + let mut x = 0; + let mut y = 1; + let mut px = &mut x; + let py = &mut y; + let ppx = &mut px; + *ppx = py; + **ppx = 2; + assert!(*px == 2); + assert!(x == 0); + assert!(*py == 2); + assert!(y == 2); + assert!(**ppx == 2); // ppx has ended +} + +pub fn test_box1() { + use std::ops::Deref; + use std::ops::DerefMut; + let mut b: Box<i32> = Box::new(0); + let x0 = b.deref_mut(); + *x0 = 1; + let x1 = b.deref(); + assert!(*x1 == 1); + assert!(*x0 == 1); // x0 has ended +} diff --git a/tests/src/constants.rs b/tests/src/constants.rs index ac24dcd4..71d7c557 100644 --- a/tests/src/constants.rs +++ b/tests/src/constants.rs @@ -1,5 +1,5 @@ //@ charon-args=--no-code-duplication -//@ aeneas-args=-test-trans-units +//@ [!borrow-check] aeneas-args=-test-trans-units //@ [coq,fstar] subdir=misc //! Tests with constants diff --git a/tests/src/external.rs b/tests/src/external.rs index baea76e4..00acdb0b 100644 --- a/tests/src/external.rs +++ b/tests/src/external.rs @@ -1,6 +1,6 @@ //@ charon-args=--no-code-duplication -//@ aeneas-args=-state -split-files -//@ aeneas-args=-test-trans-units +//@ [!borrow-check] aeneas-args=-state -split-files +//@ [!borrow-check] aeneas-args=-test-trans-units //@ [coq,fstar] subdir=misc //! This module uses external types and functions diff --git a/tests/src/hashmap.rs b/tests/src/hashmap.rs index 19832a84..7dda2404 100644 --- a/tests/src/hashmap.rs +++ b/tests/src/hashmap.rs @@ -1,5 +1,5 @@ //@ charon-args=--opaque=utils -//@ aeneas-args=-state -split-files +//@ [!borrow-check] aeneas-args=-state -split-files //@ [coq] aeneas-args=-use-fuel //@ [fstar] aeneas-args=-decreases-clauses -template-clauses //@ [lean] aeneas-args=-no-gen-lib-entry diff --git a/tests/src/loops-borrow-check-fail.borrow-check.out b/tests/src/loops-borrow-check-fail.borrow-check.out new file mode 100644 index 00000000..34eb75f8 --- /dev/null +++ b/tests/src/loops-borrow-check-fail.borrow-check.out @@ -0,0 +1,5 @@ +[[92mInfo[39m ] Imported: tests/llbc/loops_borrow_check_fail.llbc +[[91mError[39m] Can not apply a projection to the ⊥ value +Source: 'tests/src/loops-borrow-check-fail.rs', lines 7:4-12:1 +[[91mError[39m] Can not apply a projection to the ⊥ value +Source: 'tests/src/loops-borrow-check-fail.rs', lines 17:4-21:1 diff --git a/tests/src/loops-borrow-check-fail.rs b/tests/src/loops-borrow-check-fail.rs new file mode 100644 index 00000000..24be052c --- /dev/null +++ b/tests/src/loops-borrow-check-fail.rs @@ -0,0 +1,21 @@ +//@ [!borrow-check] skip +//@ [borrow-check] known-failure + +// We need to use the general rules for joining the loans +fn loop_reborrow_mut() { + let mut x = 0; + let mut px = &mut x; + while *px > 0 { + x += 1; + px = &mut x; + } +} + +// We need to imrpove [prepare_ashared_loans] +fn iter_local_shared_borrow() { + let mut x = 0; + let mut p = &x; + loop { + p = &(*p); + } +} diff --git a/tests/src/loops-borrow-check-negative.borrow-check.out b/tests/src/loops-borrow-check-negative.borrow-check.out new file mode 100644 index 00000000..093d8b8a --- /dev/null +++ b/tests/src/loops-borrow-check-negative.borrow-check.out @@ -0,0 +1,3 @@ +[[92mInfo[39m ] Imported: tests/llbc/loops_borrow_check_negative.llbc +[[91mError[39m] Can't end abstraction 16 as it is set as non-endable +Source: 'tests/src/loops-borrow-check-negative.rs', lines 18:0-18:66 diff --git a/tests/src/loops-borrow-check-negative.rs b/tests/src/loops-borrow-check-negative.rs new file mode 100644 index 00000000..3386d581 --- /dev/null +++ b/tests/src/loops-borrow-check-negative.rs @@ -0,0 +1,28 @@ +//@ [!borrow-check] skip +//@ [borrow-check] known-failure + +// This succeeds +fn loop_a<'a>(a: &'a mut u32, b: &'a mut u32) -> &'a mut u32 { + let mut x = 0; + while x > 0 { + x += 1; + } + if x > 0 { + a + } else { + b + } +} + +// This fails +fn loop_a_b<'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 // Expect lifetime 'a + } +} diff --git a/tests/src/loops-borrow-check.rs b/tests/src/loops-borrow-check.rs new file mode 100644 index 00000000..ab300b37 --- /dev/null +++ b/tests/src/loops-borrow-check.rs @@ -0,0 +1,10 @@ +//@ [!borrow-check] skip + +fn iter_local_mut_borrow() { + let mut x = 0; + let mut p = &mut x; + loop { + p = &mut (*p); + *p += 1; + } +} diff --git a/tests/src/mutually-recursive-traits.lean.out b/tests/src/mutually-recursive-traits.lean.out index 6d638644..e2ed3abc 100644 --- a/tests/src/mutually-recursive-traits.lean.out +++ b/tests/src/mutually-recursive-traits.lean.out @@ -1,17 +1,17 @@ [[92mInfo[39m ] Imported: tests/llbc/mutually_recursive_traits.llbc -[[91mError[39m] In file Translate.ml, line 812: +[[91mError[39m] In file Translate.ml, line 813: Mutually recursive trait declarations are not supported Uncaught exception: (Failure - "In file Translate.ml, line 812:\ - \nIn file Translate.ml, line 812:\ + "In file Translate.ml, line 813:\ + \nIn file Translate.ml, line 813:\ \nMutually recursive trait declarations are not supported") Raised at Aeneas__Errors.craise_opt_span in file "Errors.ml", line 46, characters 4-76 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 -Called from Aeneas__Translate.extract_definitions in file "Translate.ml", line 835, characters 2-52 -Called from Aeneas__Translate.extract_file in file "Translate.ml", line 953, characters 2-36 -Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1501, characters 5-42 -Called from Dune__exe__Main in file "Main.ml", line 276, characters 9-61 +Called from Aeneas__Translate.extract_definitions in file "Translate.ml", line 836, characters 2-52 +Called from Aeneas__Translate.extract_file in file "Translate.ml", line 954, characters 2-36 +Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1503, characters 5-42 +Called from Dune__exe__Main in file "Main.ml", line 314, characters 14-66 diff --git a/tests/src/mutually-recursive-traits.rs b/tests/src/mutually-recursive-traits.rs index 351763b2..9bc4ca63 100644 --- a/tests/src/mutually-recursive-traits.rs +++ b/tests/src/mutually-recursive-traits.rs @@ -1,6 +1,6 @@ //@ [lean] known-failure -//@ [coq,fstar] skip -//@ subdir=misc +//@ [!lean] skip +//@ [lean] subdir=misc pub trait Trait1 { type T: Trait2; } diff --git a/tests/src/no_nested_borrows.rs b/tests/src/no_nested_borrows.rs index 6d3074ef..11c4a695 100644 --- a/tests/src/no_nested_borrows.rs +++ b/tests/src/no_nested_borrows.rs @@ -1,5 +1,5 @@ //@ charon-args=--no-code-duplication -//@ aeneas-args=-test-trans-units +//@ [!borrow-check] aeneas-args=-test-trans-units //@ [coq,fstar] subdir=misc //! This module doesn't contain **functions which use nested borrows in their //! signatures**, and doesn't contain functions with loops. diff --git a/tests/src/paper.rs b/tests/src/paper.rs index 6a4a7c31..d9fb1032 100644 --- a/tests/src/paper.rs +++ b/tests/src/paper.rs @@ -1,5 +1,5 @@ //@ charon-args=--no-code-duplication -//@ aeneas-args=-test-trans-units +//@ [!borrow-check] aeneas-args=-test-trans-units //@ [coq,fstar] subdir=misc //! The examples from the ICFP submission, all in one place. diff --git a/tests/src/polonius_list.rs b/tests/src/polonius_list.rs index b029ad02..084441aa 100644 --- a/tests/src/polonius_list.rs +++ b/tests/src/polonius_list.rs @@ -1,5 +1,5 @@ //@ charon-args=--polonius -//@ aeneas-args=-test-trans-units +//@ [!borrow-check] aeneas-args=-test-trans-units //@ [coq,fstar] subdir=misc #![allow(dead_code)] diff --git a/tests/src/string-chars.rs b/tests/src/string-chars.rs index f8490e76..9fd91752 100644 --- a/tests/src/string-chars.rs +++ b/tests/src/string-chars.rs @@ -1,5 +1,5 @@ //@ [lean] known-failure -//@ [coq,fstar] skip +//@ [!lean] skip //@ no-check-output fn main() { let s = "hello"; diff --git a/tests/test_runner/Backend.ml b/tests/test_runner/Backend.ml index d21a46fc..819081a2 100644 --- a/tests/test_runner/Backend.ml +++ b/tests/test_runner/Backend.ml @@ -1,15 +1,24 @@ (*** Define the backends we support as an enum *) -type t = Coq | Lean | FStar | HOL4 [@@deriving ord, sexp] +type t = + | Coq + | Lean + | FStar + | HOL4 + | BorrowCheck + (** Borrow check: no backend. + We use this when we only want to borrow-check the program *) +[@@deriving ord, sexp] (* TODO: reactivate HOL4 once traits are parameterized by their associated types *) -let all = [ Coq; Lean; FStar ] +let all = [ Coq; Lean; FStar; BorrowCheck ] let of_string = function | "coq" -> Coq | "lean" -> Lean | "fstar" -> FStar | "hol4" -> HOL4 + | "borrow-check" -> BorrowCheck | backend -> failwith ("Unknown backend: `" ^ backend ^ "`") let to_string = function @@ -17,6 +26,11 @@ let to_string = function | Lean -> "lean" | FStar -> "fstar" | HOL4 -> "hol4" + | BorrowCheck -> "borrow-check" + +let to_command = function + | BorrowCheck -> [ "-borrow-check" ] + | x -> [ "-backend"; to_string x ] module Map = struct (* Hack to be able to include things from the parent module with the same names *) diff --git a/tests/test_runner/Input.ml b/tests/test_runner/Input.ml index 960ffe8d..e35be96f 100644 --- a/tests/test_runner/Input.ml +++ b/tests/test_runner/Input.ml @@ -7,7 +7,7 @@ type action = Normal | Skip | KnownFailure type per_backend = { action : action; aeneas_options : string list; - subdir : string; + subdir : string option; (* Whether to store the command output to a file. Only available for known-failure tests. *) check_output : bool; } @@ -22,8 +22,11 @@ type t = { } (* The default subdirectory in which to store the outputs. *) -let default_subdir backend test_name = - match backend with Backend.Lean -> "." | _ -> test_name +let default_subdir backend test_name : string option = + match backend with + | Backend.Lean -> Some "." + | Backend.BorrowCheck -> None + | _ -> Some test_name (* Parse lines that start `//@`. Each of them modifies the options we use for the test. Supported comments: @@ -39,14 +42,21 @@ let default_subdir backend test_name = let apply_special_comment comment input = let comment = String.trim comment in (* Parse the backends if any *) - let re = Re.compile (Re.Pcre.re "^\\[([a-zA-Z,]+)\\](.*)$") in + let re = Re.compile (Re.Pcre.re "^\\[(!)?([a-zA-Z,-]+)\\](.*)$") in let comment, (backends : Backend.t list) = match Re.exec_opt re comment with | Some groups -> - let backends = Re.Group.get groups 1 in + let exclude = Re.Group.get_opt groups 1 <> None in + let backends = Re.Group.get groups 2 in let backends = String.split_on_char ',' backends in let backends = List.map Backend.of_string backends in - let rest = Re.Group.get groups 2 in + let rest = Re.Group.get groups 3 in + (* If [exclude]: we take all the backends *but* the list provided. *) + let backends = + if exclude then + List.filter (fun x -> not (List.mem x backends)) Backend.all + else backends + in (String.trim rest, backends) | None -> (comment, Backend.all) in @@ -83,9 +93,9 @@ let apply_special_comment comment input = let args = String.split_on_char ' ' args in per_backend (fun x -> { x with aeneas_options = List.append x.aeneas_options args }) - else if Option.is_some subdir then - let subdir = Option.get subdir in - per_backend (fun x -> { x with subdir }) + else if Option.is_some subdir then ( + assert (not (List.mem Backend.BorrowCheck backends)); + per_backend (fun x -> { x with subdir })) else failwith ("Unrecognized special comment: `" ^ comment ^ "`") (* Given a path to a rust file or crate, gather the details and options about how to build the test. *) diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml index c17c17be..0c3426c5 100644 --- a/tests/test_runner/run_test.ml +++ b/tests/test_runner/run_test.ml @@ -50,25 +50,35 @@ end (* Run Aeneas on a specific input with the given options *) let run_aeneas (env : runner_env) (case : Input.t) (backend : Backend.t) = let backend_str = Backend.to_string backend in + let backend_command = Backend.to_command backend in let input_file = concat_path [ env.llbc_dir; case.name ] ^ ".llbc" in let output_file = Filename.remove_extension case.path ^ "." ^ backend_str ^ ".out" in + let per_backend = Backend.Map.find backend case.per_backend in let subdir = per_backend.subdir in let check_output = per_backend.check_output in let aeneas_options = per_backend.aeneas_options in let action = per_backend.action in - let dest_dir = concat_path [ env.dest_dir; backend_str; subdir ] in + (* No destination directory if we borrow-check *) + let dest_command = + match backend with + | Backend.BorrowCheck -> [] + | _ -> + let subdir = match subdir with None -> [] | Some x -> [ x ] in + [ "-dest"; concat_path ([ env.dest_dir; backend_str ] @ subdir) ] + in (* Build the command *) - let args = - [ env.aeneas_path; input_file; "-dest"; dest_dir; "-backend"; backend_str ] - in + let args = [ env.aeneas_path; input_file ] @ dest_command @ backend_command in + (* If we target a specific backend and the test is known to fail, we abort + on error so as not to generate any files *) let abort_on_error = match action with | Skip | Normal -> [] - | KnownFailure -> [ "-abort-on-error" ] + | KnownFailure -> + if backend = Backend.BorrowCheck then [] else [ "-abort-on-error" ] in let args = List.concat [ args; aeneas_options; abort_on_error ] in let cmd = Command.make args in |