summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
Diffstat (limited to 'compiler')
-rw-r--r--compiler/ExtractBase.ml85
-rw-r--r--compiler/PureUtils.ml11
-rw-r--r--compiler/SymbolicToPure.ml35
3 files changed, 86 insertions, 45 deletions
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index ba75f580..6130528c 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -237,7 +237,7 @@ module IdSet = Collections.MakeSet (IdOrderedType)
*)
type names_map = {
id_to_name : string IdMap.t;
- name_to_id : id StringMap.t;
+ name_to_id : (id * Meta.meta option) StringMap.t;
(** The name to id map is used to look for name clashes, and generate nice
debugging messages: if there is a name clash, it is useful to know
precisely which identifiers are mapped to the same name...
@@ -253,42 +253,53 @@ let empty_names_map : names_map =
}
(** Small helper to report name collision *)
-let report_name_collision (id_to_string : id -> string) (id1 : id) (id2 : id)
+let report_name_collision (id_to_string : id -> string)
+ ((id1, meta1) : id * Meta.meta option) (id2 : id) (meta2 : Meta.meta option)
(name : string) : unit =
- let id1 = "\n- " ^ id_to_string id1 in
- let id2 = "\n- " ^ id_to_string id2 in
+ let meta_to_string (meta : Meta.meta option) =
+ match meta with
+ | None -> ""
+ | Some meta -> "\n " ^ Errors.meta_to_string meta.span
+ in
+ let id1 = "\n- " ^ id_to_string id1 ^ meta_to_string meta1 in
+ let id2 = "\n- " ^ id_to_string id2 ^ meta_to_string meta2 in
let err =
"Name clash detected: the following identifiers are bound to the same name \
\"" ^ name ^ "\":" ^ id1 ^ id2
^ "\nYou may want to rename some of your definitions, or report an issue."
in
- (* If we fail hard on errors, raise an exception *)
+ (* Register the error.
+
+ We don't link this error to any meta information because we already put
+ the span information about the two problematic definitions in the error
+ message above. *)
save_error __FILE__ __LINE__ None err
-let names_map_get_id_from_name (name : string) (nm : names_map) : id option =
+let names_map_get_id_from_name (name : string) (nm : names_map) :
+ (id * Meta.meta option) option =
StringMap.find_opt name nm.name_to_id
let names_map_check_collision (id_to_string : id -> string) (id : id)
- (name : string) (nm : names_map) : unit =
+ (meta : Meta.meta option) (name : string) (nm : names_map) : unit =
match names_map_get_id_from_name name nm with
| None -> () (* Ok *)
| Some clash ->
(* There is a clash: print a nice debugging message for the user *)
- report_name_collision id_to_string clash id name
+ report_name_collision id_to_string clash id meta name
(** Insert bindings in a names map without checking for collisions *)
-let names_map_add_unchecked (id : id) (name : string) (nm : names_map) :
- names_map =
+let names_map_add_unchecked ((id, meta) : id * Meta.meta option) (name : string)
+ (nm : names_map) : names_map =
(* Insert *)
let id_to_name = IdMap.add id name nm.id_to_name in
- let name_to_id = StringMap.add name id nm.name_to_id in
+ let name_to_id = StringMap.add name (id, meta) nm.name_to_id in
let names_set = StringSet.add name nm.names_set in
{ id_to_name; name_to_id; names_set }
-let names_map_add (id_to_string : id -> string) (id : id) (name : string)
- (nm : names_map) : names_map =
+let names_map_add (id_to_string : id -> string) ((id, meta) : id * meta option)
+ (name : string) (nm : names_map) : names_map =
(* Check if there is a clash *)
- names_map_check_collision id_to_string id name nm;
+ names_map_check_collision id_to_string id meta name nm;
(* Sanity check *)
(if StringSet.mem name nm.names_set then
let err =
@@ -296,9 +307,9 @@ let names_map_add (id_to_string : id -> string) (id : id) (name : string)
^ ":\nThe chosen name is already in the names set: " ^ name
in
(* If we fail hard on errors, raise an exception *)
- save_error __FILE__ __LINE__ None err);
+ save_error __FILE__ __LINE__ meta err);
(* Insert *)
- names_map_add_unchecked id name nm
+ names_map_add_unchecked (id, meta) name nm
(** The unsafe names map stores mappings from identifiers to names which might
collide. For some backends and some names, it might be acceptable to have
@@ -384,8 +395,8 @@ let allow_collisions (id : id) : bool =
(** The [id_to_string] function to print nice debugging messages if there are
collisions *)
-let names_maps_add (id_to_string : id -> string) (id : id) (name : string)
- (nm : names_maps) : names_maps =
+let names_maps_add (id_to_string : id -> string) (id : id)
+ (meta : Meta.meta option) (name : string) (nm : names_maps) : names_maps =
(* We do not use the same name map if we allow/disallow collisions.
We notably use it for field names: some backends like Lean can use the
type information to disambiguate field projections.
@@ -400,7 +411,7 @@ let names_maps_add (id_to_string : id -> string) (id : id) (name : string)
*)
if allow_collisions id then (
(* Check with the ids which are considered to be strict on collisions *)
- names_map_check_collision id_to_string id name nm.strict_names_map;
+ names_map_check_collision id_to_string id meta name nm.strict_names_map;
{
nm with
unsafe_names_map = unsafe_names_map_add id name nm.unsafe_names_map;
@@ -415,10 +426,10 @@ let names_maps_add (id_to_string : id -> string) (id : id) (name : string)
*)
let strict_names_map =
if strict_collisions id then
- names_map_add id_to_string id name nm.strict_names_map
+ names_map_add id_to_string (id, meta) name nm.strict_names_map
else nm.strict_names_map
in
- let names_map = names_map_add id_to_string id name nm.names_map in
+ let names_map = names_map_add id_to_string (id, meta) name nm.names_map in
{ nm with strict_names_map; names_map }
(** The [id_to_string] function to print nice debugging messages if there are
@@ -468,20 +479,21 @@ type names_map_init = {
let names_maps_add_assumed_type (id_to_string : id -> string) (id : assumed_ty)
(name : string) (nm : names_maps) : names_maps =
- names_maps_add id_to_string (TypeId (TAssumed id)) name nm
+ names_maps_add id_to_string (TypeId (TAssumed id)) None name nm
let names_maps_add_assumed_struct (id_to_string : id -> string)
(id : assumed_ty) (name : string) (nm : names_maps) : names_maps =
- names_maps_add id_to_string (StructId (TAssumed id)) name nm
+ names_maps_add id_to_string (StructId (TAssumed id)) None name nm
let names_maps_add_assumed_variant (id_to_string : id -> string)
(id : assumed_ty) (variant_id : VariantId.id) (name : string)
(nm : names_maps) : names_maps =
- names_maps_add id_to_string (VariantId (TAssumed id, variant_id)) name nm
+ names_maps_add id_to_string (VariantId (TAssumed id, variant_id)) None name nm
-let names_maps_add_function (id_to_string : id -> string) (fid : fun_id)
- (name : string) (nm : names_maps) : names_maps =
- names_maps_add id_to_string (FunId fid) name nm
+let names_maps_add_function (id_to_string : id -> string)
+ ((fid, meta) : fun_id * meta option) (name : string) (nm : names_maps) :
+ names_maps =
+ names_maps_add id_to_string (FunId fid) meta name nm
let bool_name () = if !backend = Lean then "Bool" else "bool"
let char_name () = if !backend = Lean then "Char" else "char"
@@ -659,7 +671,9 @@ let id_to_string (meta : Meta.meta option) (id : id) (ctx : extraction_ctx) :
let ctx_add (meta : Meta.meta) (id : id) (name : string) (ctx : extraction_ctx)
: extraction_ctx =
let id_to_string (id : id) : string = id_to_string (Some meta) id ctx in
- let names_maps = names_maps_add id_to_string id name ctx.names_maps in
+ let names_maps =
+ names_maps_add id_to_string id (Some meta) name ctx.names_maps
+ in
{ ctx with names_maps }
let ctx_get (meta : Meta.meta option) (id : id) (ctx : extraction_ctx) : string
@@ -1125,7 +1139,7 @@ let initialize_names_maps () : names_maps =
(* There is duplication in the keywords so we don't check the collisions
while registering them (what is important is that there are no collisions
between keywords and user-defined identifiers) *)
- names_map_add_unchecked UnknownId name nm)
+ names_map_add_unchecked (UnknownId, None) name nm)
strict_names_map keywords
in
let nm = { names_map; unsafe_names_map; strict_names_map } in
@@ -1155,9 +1169,12 @@ let initialize_names_maps () : names_maps =
in
let assumed_functions =
List.map
- (fun (fid, name) -> (FromLlbc (Pure.FunId (FAssumed fid), None), name))
+ (fun (fid, name) ->
+ ((FromLlbc (Pure.FunId (FAssumed fid), None), None), name))
init.assumed_llbc_functions
- @ List.map (fun (fid, name) -> (Pure fid, name)) init.assumed_pure_functions
+ @ List.map
+ (fun (fid, name) -> ((Pure fid, None), name))
+ init.assumed_pure_functions
in
let nm =
List.fold_left
@@ -1662,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/PureUtils.ml b/compiler/PureUtils.ml
index 87f0b5f7..1bef43b4 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 53ab1c08..f036cc37 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} *)
@@ -2244,15 +2262,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)
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-21 04:37:59 +0000