summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2023-09-03 16:51:36 +0200
committerSon Ho2023-09-03 16:51:36 +0200
commit0e0f3d586e7e74003ebff129a1e91b87602467e7 (patch)
treecb5c8e42605650f002861460f6b4f6daa0ad0fcb
parenta2f19257651df3c8473e17ef73a5389b9cb89bbf (diff)
Make more progress
Diffstat (limited to '')
-rw-r--r--compiler/Extract.ml19
-rw-r--r--compiler/ExtractBase.ml2
-rw-r--r--compiler/Translate.ml70
3 files changed, 67 insertions, 24 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index e140ea1c..17f850a3 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -1650,7 +1650,7 @@ let insert_req_space (fmt : F.formatter) (space : bool ref) : unit =
We add the trait self clause for provided methods (see {!TraitSelfClauseId}).
*)
let extract_trait_self_clause (insert_req_space : unit -> unit)
- (ctx : extraction_ctx) (fmt : F.formatter) (trait_decl : A.trait_decl)
+ (ctx : extraction_ctx) (fmt : F.formatter) (trait_decl : trait_decl)
(params : string list) : unit =
insert_req_space ();
F.pp_print_string fmt "(";
@@ -1673,7 +1673,7 @@ let extract_trait_self_clause (insert_req_space : unit -> unit)
*)
let extract_generic_params (ctx : extraction_ctx) (fmt : F.formatter)
(no_params_tys : TypeDeclId.Set.t) (use_forall : bool) (as_implicits : bool)
- (space : bool ref option) (trait_decl : A.trait_decl option)
+ (space : bool ref option) (trait_decl : trait_decl option)
(generics : generic_params) (type_params : string list)
(cg_params : string list) (trait_clauses : string list) : unit =
let all_params = List.concat [ type_params; cg_params; trait_clauses ] in
@@ -3111,10 +3111,7 @@ let extract_fun_parameters (space : bool ref) (ctx : extraction_ctx)
let ctx, trait_decl =
match def.kind with
| TraitMethodProvided (decl_id, _) ->
- let trait_decl =
- T.TraitDeclId.Map.find decl_id
- ctx.trans_ctx.trait_decls_context.trait_decls
- in
+ 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
(ctx, Some trait_decl)
@@ -3887,6 +3884,16 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
(* Add a break to insert lines between declarations *)
F.pp_print_break fmt 0 0
+(** Similar to {!extract_type_decl_register_names} *)
+let extract_trait_decl_register_names (ctx : extraction_ctx) (d : trait_decl) :
+ extraction_ctx =
+ raise (Failure "TODO")
+
+(** Similar to {!extract_type_decl_register_names} *)
+let extract_trait_impl_register_names (ctx : extraction_ctx) (d : trait_impl) :
+ extraction_ctx =
+ raise (Failure "TODO")
+
(** Extract a trait declaration *)
let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
(trait_decl : trait_decl) : unit =
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 251d8b36..2855b3b9 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -654,6 +654,8 @@ type extraction_ctx = {
trait_decl_id : trait_decl_id option;
(** If we are extracting a trait declaration, identifies it *)
is_provided_method : bool;
+ trans_trait_decls : Pure.trait_decl Pure.TraitDeclId.Map.t;
+ trans_trait_impls : Pure.trait_impl Pure.TraitImplId.Map.t;
}
(** Debugging function, used when communicating name collisions to the user,
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 790dbe14..8df69961 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -301,8 +301,13 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
(* Return *)
(pure_forward, pure_backwards)
+(* TODO: factor out the return type *)
let translate_crate_to_pure (crate : A.crate) :
- trans_ctx * Pure.type_decl list * (bool * pure_fun_translation) list =
+ trans_ctx
+ * Pure.type_decl list
+ * (bool * pure_fun_translation) list
+ * Pure.trait_decl list
+ * Pure.trait_impl list =
(* Debug *)
log#ldebug (lazy "translate_crate_to_pure");
@@ -368,13 +373,28 @@ let translate_crate_to_pure (crate : A.crate) :
(A.FunDeclId.Map.values crate.functions)
in
+ (* Translate the trait declarations *)
+ let type_infos = trans_ctx.type_context.type_infos in
+ let trait_decls =
+ List.map
+ (SymbolicToPure.translate_trait_decl type_infos)
+ (T.TraitDeclId.Map.values trans_ctx.trait_decls_context.trait_decls)
+ in
+
+ (* Translate the trait implementations *)
+ let trait_impls =
+ List.map
+ (SymbolicToPure.translate_trait_impl type_infos)
+ (T.TraitImplId.Map.values trans_ctx.trait_impls_context.trait_impls)
+ in
+
(* Apply the micro-passes *)
let pure_translations =
Micro.apply_passes_to_pure_fun_translations trans_ctx pure_translations
in
(* Return *)
- (trans_ctx, type_decls, pure_translations)
+ (trans_ctx, type_decls, pure_translations, trait_decls, trait_impls)
(** Extraction context *)
type gen_ctx = {
@@ -735,14 +755,8 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config)
let export_trait_decl (fmt : Format.formatter) (_config : gen_config)
(ctx : gen_ctx) (trait_decl_id : Pure.trait_decl_id) : unit =
let trait_decl =
- T.TraitDeclId.Map.find trait_decl_id
- ctx.extract_ctx.trans_ctx.trait_decls_context.trait_decls
+ T.TraitDeclId.Map.find trait_decl_id ctx.extract_ctx.trans_trait_decls
in
- (* We translate the trait declaration on the fly (note that
- trait declarations do not directly contain functions, constants,
- etc.: they simply refer to them). *)
- let type_infos = ctx.extract_ctx.trans_ctx.type_context.type_infos in
- let trait_decl = SymbolicToPure.translate_trait_decl type_infos trait_decl in
let ctx = ctx.extract_ctx in
let ctx = { ctx with trait_decl_id = Some trait_decl.def_id } in
Extract.extract_trait_decl ctx fmt trait_decl
@@ -751,14 +765,8 @@ let export_trait_decl (fmt : Format.formatter) (_config : gen_config)
let export_trait_impl (fmt : Format.formatter) (_config : gen_config)
(ctx : gen_ctx) (trait_impl_id : Pure.trait_impl_id) : unit =
let trait_impl =
- T.TraitImplId.Map.find trait_impl_id
- ctx.extract_ctx.trans_ctx.trait_impls_context.trait_impls
+ T.TraitImplId.Map.find trait_impl_id ctx.extract_ctx.trans_trait_impls
in
- (* We translate the trait implementation on the fly (note that
- trait implementations do not directly contain functions, constants,
- etc.: they simply refer to them). *)
- let type_infos = ctx.extract_ctx.trans_ctx.type_context.type_infos in
- let trait_impl = SymbolicToPure.translate_trait_impl type_infos trait_impl in
Extract.extract_trait_impl ctx.extract_ctx fmt trait_impl
(** A generic utility to generate the extracted definitions: as we may want to
@@ -978,7 +986,9 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
unit =
(* Translate the module to the pure AST *)
- let trans_ctx, trans_types, trans_funs = translate_crate_to_pure crate in
+ let trans_ctx, trans_types, trans_funs, trans_trait_decls, trans_trait_impls =
+ translate_crate_to_pure crate
+ in
(* Initialize the extraction context - for now we extract only to F*.
* We initialize the names map by registering the keywords used in the
@@ -997,6 +1007,18 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
in
(* Put everything in the context *)
let ctx =
+ let trans_trait_decls =
+ T.TraitDeclId.Map.of_list
+ (List.map
+ (fun (d : Pure.trait_decl) -> (d.def_id, d))
+ trans_trait_decls)
+ in
+ let trans_trait_impls =
+ T.TraitImplId.Map.of_list
+ (List.map
+ (fun (d : Pure.trait_impl) -> (d.def_id, d))
+ trans_trait_impls)
+ in
{
ExtractBase.trans_ctx;
names_map;
@@ -1008,6 +1030,8 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
fun_name_info = PureUtils.RegularFunIdMap.empty;
trait_decl_id = None (* None by default *);
is_provided_method = false (* false by default *);
+ trans_trait_decls;
+ trans_trait_impls;
}
in
@@ -1034,7 +1058,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
in
let rec_functions = PureUtils.FunLoopIdSet.of_list rec_functions in
- (* Register unique names for all the top-level types, globals and functions.
+ (* Register unique names for all the top-level types, globals, functions...
* Note that the order in which we generate the names doesn't matter:
* we just need to generate a mapping from identifier to name, and make
* sure there are no name clashes. *)
@@ -1071,6 +1095,16 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
(A.GlobalDeclId.Map.values crate.globals)
in
+ let ctx =
+ List.fold_left Extract.extract_trait_decl_register_names ctx
+ trans_trait_decls
+ in
+
+ let ctx =
+ List.fold_left Extract.extract_trait_impl_register_names ctx
+ trans_trait_impls
+ in
+
(* Open the output file *)
(* First compute the filename by replacing the extension and converting the
* case (rust module names are snake case) *)