summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--compiler/Extract.ml4
-rw-r--r--compiler/ExtractBase.ml21
-rw-r--r--compiler/ExtractName.ml57
-rw-r--r--compiler/Interpreter.ml6
-rw-r--r--compiler/LlbcAstUtils.ml2
-rw-r--r--compiler/Pure.ml4
-rw-r--r--compiler/Translate.ml2
7 files changed, 57 insertions, 39 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index b9c6b1b0..46f6a1ca 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -19,7 +19,7 @@ let extract_fun_decl_register_names (ctx : extraction_ctx)
only use their type for the fields of the records we generate for the trait
declarations *)
match def.f.kind with
- | TraitMethodDecl _ -> ctx
+ | TraitItemDecl _ -> ctx
| _ -> (
(* Check if the function is builtin *)
let builtin =
@@ -1108,7 +1108,7 @@ let extract_fun_parameters (space : bool ref) (ctx : extraction_ctx)
*)
let ctx, trait_decl =
match def.kind with
- | TraitMethodProvided (decl_id, _) ->
+ | TraitItemProvided (decl_id, _) ->
let trait_decl = T.TraitDeclId.Map.find decl_id ctx.trans_trait_decls in
let ctx, _ = ctx_add_trait_self_clause ctx in
let ctx = { ctx with is_provided_method = true } in
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index e0614af1..5e97cd21 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -1374,10 +1374,11 @@ let ctx_compute_fun_name_no_suffix (ctx : extraction_ctx) (fname : llbc_name) :
(** Provided a basename, compute the name of a global declaration. *)
let ctx_compute_global_name (ctx : extraction_ctx) (name : llbc_name) : string =
- (* Converting to snake case also lowercases the letters (in Rust, global
- * names are written in capital letters). *)
- let parts = List.map to_snake_case (ctx_compute_simple_name ctx name) in
- String.concat "_" parts
+ match !Config.backend with
+ | Coq | FStar | HOL4 ->
+ let parts = List.map to_snake_case (ctx_compute_simple_name ctx name) in
+ String.concat "_" parts
+ | Lean -> flatten_name (ctx_compute_simple_name ctx name)
(** Helper function: generate a suffix for a function name, i.e., generates
a suffix like "_loop", "loop1", etc. to append to a function name.
@@ -1511,6 +1512,7 @@ let ctx_compute_trait_parent_clause_name (ctx : extraction_ctx)
if !Config.record_fields_short_names then clause
else ctx_compute_trait_decl_name ctx trait_decl ^ "_" ^ clause
in
+ let clause = clause ^ "Inst" in
match !backend with
| FStar -> StringUtils.lowercase_first_letter clause
| Coq | HOL4 | Lean -> clause
@@ -1888,8 +1890,15 @@ let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) :
(* Not the case: "standard" registration *)
let name = ctx_compute_global_name ctx def.name in
let body = FunId (FromLlbc (FunId (FRegular def.body), None)) in
- let ctx = ctx_add decl (name ^ "_c") ctx in
- let ctx = ctx_add body (name ^ "_body") ctx in
+ (* If this is a provided constant (i.e., the default value for a constant
+ in a trait declaration) we add a suffix. Otherwise there is a clash
+ between the name for the default constant and the name for the field
+ in the trait declaration *)
+ let suffix =
+ match def.kind with TraitItemProvided _ -> "_default" | _ -> ""
+ in
+ let ctx = ctx_add decl (name ^ suffix) ctx in
+ let ctx = ctx_add body (name ^ suffix ^ "_body") ctx in
ctx
let ctx_compute_fun_name (def : fun_decl) (ctx : extraction_ctx) : string =
diff --git a/compiler/ExtractName.ml b/compiler/ExtractName.ml
index b53f4cdd..dfac6546 100644
--- a/compiler/ExtractName.ml
+++ b/compiler/ExtractName.ml
@@ -39,37 +39,46 @@ let pattern_to_extract_name (name : pattern) : string list =
| GRegion (RVar _) -> true
| _ -> false
in
- let all_vars = List.for_all is_var in
- let elem_to_string (e : pattern_elem) : string =
- match e with
- | PIdent _ -> pattern_elem_to_string c e
- | PImpl ty -> (
+ let all_distinct_vars = List.for_all is_var in
+
+ (* This is a bit of a hack: we want to simplify the occurrences of
+ tuples of two variables, arrays with only variables, slices with
+ only variables, etc.
+ We explore the pattern and replace such occurrences with a specific name.
+ *)
+ let visitor =
+ object
+ inherit [_] map_pattern as super
+
+ method! visit_PImpl _ ty =
+ (* TODO: Option *)
match ty with
| EComp id -> (
(* Retrieve the last ident *)
let id = Collections.List.last id in
match id with
- | PIdent (s, g) ->
- if all_vars g then s else pattern_elem_to_string c id
+ | PIdent (s, g) as id ->
+ if all_distinct_vars g then PImpl (EComp [ PIdent (s, []) ])
+ else super#visit_PImpl () (EComp [ id ])
| PImpl _ -> raise (Failure "Unreachable"))
- | EPrimAdt (adt, g) ->
- if all_vars g then
- match adt with
- | TTuple ->
- let l = List.length g in
- if l = 2 then "Pair" else expr_to_string c ty
- | TArray -> "Array"
- | TSlice -> "Slice"
- else expr_to_string c ty
- | ERef _ | EVar _ | EArrow _ | ERawPtr _ ->
- (* We simply convert the pattern to a string. This is not very
- satisfying but we should rarely get there. *)
- expr_to_string c ty)
- in
- let rec pattern_to_string (n : pattern) : string list =
- match n with [] -> [] | e :: n -> elem_to_string e :: pattern_to_string n
+ | _ -> super#visit_PImpl () ty
+
+ method! visit_EPrimAdt _ adt g =
+ if all_distinct_vars g then
+ match adt with
+ | TTuple ->
+ let l = List.length g in
+ if l = 2 then EComp [ PIdent ("Pair", []) ]
+ else super#visit_EPrimAdt () adt g
+ | TArray -> EComp [ PIdent ("Array", []) ]
+ | TSlice -> EComp [ PIdent ("Slice", []) ]
+ (*else if adt = TTuple && List.length g = 2 then
+ super#visit_EComp () [ PIdent ("Pair", g) ]*)
+ else super#visit_EPrimAdt () adt g
+ end
in
- pattern_to_string name
+ let name = visitor#visit_pattern () name in
+ List.map (pattern_elem_to_string c) name
let pattern_to_type_extract_name = pattern_to_extract_name
let pattern_to_fun_extract_name = pattern_to_extract_name
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index fd3e334b..ccae4588 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -68,12 +68,12 @@ let normalize_inst_fun_sig (ctx : eval_ctx) (sg : inst_fun_sig) : inst_fun_sig =
normalize because a trait clause was instantiated with a specific trait ref).
*)
let symbolic_instantiate_fun_sig (ctx : eval_ctx) (sg : fun_sig)
- (regions_hierarchy : region_var_groups) (kind : fun_kind) :
+ (regions_hierarchy : region_var_groups) (kind : item_kind) :
eval_ctx * inst_fun_sig =
let tr_self =
match kind with
- | RegularKind | TraitMethodImpl _ -> UnknownTrait __FUNCTION__
- | TraitMethodDecl _ | TraitMethodProvided _ -> Self
+ | RegularKind | TraitItemImpl _ -> UnknownTrait __FUNCTION__
+ | TraitItemDecl _ | TraitItemProvided _ -> Self
in
let generics =
let { regions; types; const_generics; trait_clauses } = sg.generics in
diff --git a/compiler/LlbcAstUtils.ml b/compiler/LlbcAstUtils.ml
index d3fac032..1053c9ab 100644
--- a/compiler/LlbcAstUtils.ml
+++ b/compiler/LlbcAstUtils.ml
@@ -44,7 +44,7 @@ let crate_get_opaque_non_builtin_decls (k : crate) (filter_assumed : bool) :
d.body = None
(* Something to pay attention to: we must ignore trait method *declarations*
(which don't have a body but must not be considered as opaque) *)
- && (match d.kind with TraitMethodDecl _ -> false | _ -> true)
+ && (match d.kind with TraitItemDecl _ -> false | _ -> true)
&& ((not filter_assumed)
|| (not (NameMatcherMap.mem ctx d.name builtin_globals_map))
&& not (NameMatcherMap.mem ctx d.name (builtin_funs_map ())))
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index dd7a4acf..33c23cc3 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -1063,13 +1063,13 @@ type fun_body = {
}
[@@deriving show]
-type fun_kind = A.fun_kind [@@deriving show]
+type item_kind = A.item_kind [@@deriving show]
type fun_decl = {
def_id : FunDeclId.id;
is_local : bool;
meta : meta;
- kind : fun_kind;
+ kind : item_kind;
num_loops : int;
(** The number of loops in the parent forward function (basically the number
of loops appearing in the original Rust functions, unless some loops are
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index c12de045..48a3685b 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -730,7 +730,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
the trait declarations themselves, there is no point in having
separate type definitions) *)
match pure_fun.f.Pure.kind with
- | TraitMethodDecl _ -> ()
+ | TraitItemDecl _ -> ()
| _ ->
(* Translate *)
export_functions_group [ pure_fun ])
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-18 17:19:08 +0000