diff options
| -rw-r--r-- | compiler/PureUtils.ml | 11 | ||||
| -rw-r--r-- | compiler/SymbolicToPure.ml | 13 |
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 |