diff options
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/Config.ml | 2 | ||||
| -rw-r--r-- | compiler/ExtractBase.ml | 6 | ||||
| -rw-r--r-- | compiler/Main.ml | 3 | ||||
| -rw-r--r-- | compiler/PureUtils.ml | 11 | ||||
| -rw-r--r-- | compiler/SymbolicToPure.ml | 35 |
5 files changed, 39 insertions, 18 deletions
diff --git a/compiler/Config.ml b/compiler/Config.ml index 099cdc8b..0b26e2ef 100644 --- a/compiler/Config.ml +++ b/compiler/Config.ml @@ -368,4 +368,4 @@ let backend_has_tuple_projectors () = let use_nested_tuple_projectors = ref false (** Generate name patterns for the external definitions we encounter *) -let extract_external_name_patterns = ref false +let extract_external_name_patterns = ref true diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index f8d3cd96..ce8c38ba 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -1679,9 +1679,11 @@ let ctx_compute_var_basename (meta : Meta.meta) (ctx : extraction_ctx) in (* If there is a basename, we use it *) match basename with - | Some basename -> + | Some basename -> ( (* This should be a no-op *) - to_snake_case basename + match !Config.backend with + | Lean -> basename + | FStar | Coq | HOL4 -> to_snake_case basename) | None -> ( (* No basename: we use the first letter of the type *) match ty with diff --git a/compiler/Main.ml b/compiler/Main.ml index 64d8ae2b..db200f37 100644 --- a/compiler/Main.ml +++ b/compiler/Main.ml @@ -120,9 +120,6 @@ let () = Arg.Set use_nested_tuple_projectors, " Use nested projectors for tuples (e.g., (0, 1).snd.fst instead of \ (0, 1).1)." ); - ( "-ext-name-pats", - Arg.Set extract_external_name_patterns, - " Generate name patterns for the external definitions we find." ); ] in diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml index 4bc90872..6f44bb74 100644 --- a/compiler/PureUtils.ml +++ b/compiler/PureUtils.ml @@ -75,10 +75,15 @@ let inputs_info_is_wf (info : inputs_info) : bool = let fun_sig_info_is_wf (info : fun_sig_info) : bool = inputs_info_is_wf info.fwd_info +let opt_dest_arrow_ty (ty : ty) : (ty * ty) option = + match ty with TArrow (arg_ty, ret_ty) -> Some (arg_ty, ret_ty) | _ -> None + +let is_arrow_ty (ty : ty) : bool = Option.is_some (opt_dest_arrow_ty ty) + let dest_arrow_ty (meta : Meta.meta) (ty : ty) : ty * ty = - match ty with - | TArrow (arg_ty, ret_ty) -> (arg_ty, ret_ty) - | _ -> craise __FILE__ __LINE__ meta "Not an arrow type" + match opt_dest_arrow_ty ty with + | Some (arg_ty, ret_ty) -> (arg_ty, ret_ty) + | None -> craise __FILE__ __LINE__ meta "Not an arrow type" let compute_literal_type (cv : literal) : literal_type = match cv with diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 0c30f44c..5cd13072 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -1499,9 +1499,27 @@ let fresh_back_vars_for_current_fun (ctx : bs_ctx) let back_vars = List.map (fun (name, ty) -> - match ty with None -> None | Some ty -> Some (name, ty)) + match ty with + | None -> None + | Some ty -> + (* If the type is not an arrow type, don't use the name "back" + (it is a backward function with no inputs, that is to say a + value) *) + let name = if is_arrow_ty ty then name else None in + Some (name, ty)) back_vars in + (* If there is one backward function or less, we use the name "back" + (there is no point in using the lifetime name, and it makes the + code generation more stable) *) + let num_back_vars = List.length (List.filter_map (fun x -> x) back_vars) in + let back_vars = + if num_back_vars = 1 then + List.map + (Option.map (fun (name, ty) -> (Option.map (fun _ -> "back") name, ty))) + back_vars + else back_vars + in fresh_opt_vars back_vars ctx (** IMPORTANT: do not use this one directly, but rather {!symbolic_value_to_texpression} *) @@ -2240,15 +2258,14 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : (fun ty -> match ty with | None -> None - | Some (back_sg, ty) -> - (* We insert a name for the variable only if the function - can fail: if it can fail, it means the call returns a backward - function. Otherwise, it directly returns the value given - back by the backward function, which means we shouldn't - give it a name like "back..." (it doesn't make sense) *) + | Some (_back_sg, ty) -> + (* We insert a name for the variable only if the type + is an arrow type. If it is not, it means the backward + function is degenerate (it takes no inputs) so it is + not a function anymore but a value: it doesn't make + sense to use a name like "back...". *) let name = - if back_sg.effect_info.can_fail then Some back_fun_name - else None + if is_arrow_ty ty then Some back_fun_name else None in Some (name, ty)) back_tys) |