diff options
| author | Son Ho | 2023-10-26 16:15:35 +0200 |
|---|---|---|
| committer | Son Ho | 2023-10-26 16:15:35 +0200 |
| commit | 1110b3da85e93ba0755a665edd5b8c986c54cef0 (patch) | |
| tree | e668d3ca33cd412a031189ae6f281a663192a1d1 /compiler | |
| parent | c8c9be9b7d9866f9761a21adbadd923d4a79bb09 (diff) | |
Make minor modifications and update the array test for F*
Diffstat (limited to '')
| -rw-r--r-- | compiler/Driver.ml | 4 | ||||
| -rw-r--r-- | compiler/ExtractBase.ml | 22 | ||||
| -rw-r--r-- | compiler/ExtractBuiltin.ml | 5 |
3 files changed, 17 insertions, 14 deletions
diff --git a/compiler/Driver.ml b/compiler/Driver.ml index 3b9ea4d1..b660b5a5 100644 --- a/compiler/Driver.ml +++ b/compiler/Driver.ml @@ -162,7 +162,9 @@ let () = | FStar -> (* Some patterns are not supported *) decompose_monadic_let_bindings := false; - decompose_nested_let_patterns := false + decompose_nested_let_patterns := false; + (* F* can disambiguate the field names *) + record_fields_short_names := true | Coq -> (* Some patterns are not supported *) decompose_monadic_let_bindings := true; diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 8f71116c..6faa40b2 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -1332,22 +1332,20 @@ let default_fun_suffix (num_loops : int) (loop_id : LoopId.id option) let rg_suff = (* TODO: make all the backends match what is done for Lean *) match rg with - | None -> ( - match !Config.backend with - | FStar | Coq | HOL4 -> "_fwd" - | Lean -> - (* In order to avoid name conflicts: - * - if the forward is eliminated, we add the suffix "_fwd" (it won't be used) - * - otherwise, no suffix (because the backward functions will have a suffix) - *) - if num_backs = 1 && not keep_fwd then "_fwd" else "") + | None -> + if + (* In order to avoid name conflicts: + * - if the forward is eliminated, we add the suffix "_fwd" (it won't be used) + * - otherwise, no suffix (because the backward functions will have a suffix) + *) + num_backs = 1 && not keep_fwd + then "_fwd" + else "" | Some rg -> assert (num_region_groups > 0 && num_backs > 0); if num_backs = 1 then (* Exactly one backward function *) - match !Config.backend with - | FStar | Coq | HOL4 -> if not keep_fwd then "_fwd_back" else "_back" - | Lean -> if not keep_fwd then "" else "_back" + if not keep_fwd then "" else "_back" else if (* Several region groups/backward functions: - if all the regions in the group have names, we use those names diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml index 2dbacce3..c6bde9c2 100644 --- a/compiler/ExtractBuiltin.ml +++ b/compiler/ExtractBuiltin.ml @@ -149,7 +149,10 @@ let builtin_types () : builtin_type_info list = let fields = List.map (fun (rname, name) -> - (rname, backend_choice (extract_name ^ name) name)) + ( rname, + match !backend with + | FStar | Lean -> name + | Coq | HOL4 -> extract_name ^ "_" ^ name )) fields in let constructor = mk_struct_constructor extract_name in |