summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
authorSon Ho2024-04-04 13:21:08 +0200
committerSon Ho2024-04-04 13:21:08 +0200
commitbac38f94aacf4a0d621b0b2d2c423db9e0c6f175 (patch)
tree1a9de8e4593f44001cbd9bd9c370c9317733feca /compiler
parent975ddb208f18cb4ba46293dd788c46eb1ce43938 (diff)
Improve the name of the backward functions further
Diffstat (limited to '')
-rw-r--r--compiler/PureUtils.ml11
-rw-r--r--compiler/SymbolicToPure.ml13
2 files changed, 19 insertions, 5 deletions
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 7e970029..67fd2c9b 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -1499,7 +1499,14 @@ 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"
@@ -1508,7 +1515,9 @@ let fresh_back_vars_for_current_fun (ctx : bs_ctx)
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 (_, ty) -> (Some "back", ty))) back_vars
+ 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