Skip to content

Commit

Permalink
Reorganize the "Extract" files
Browse files Browse the repository at this point in the history
  • Loading branch information
sonmarcho committed Nov 21, 2023
1 parent 137cc73 commit b916f69
Show file tree
Hide file tree
Showing 7 changed files with 1,303 additions and 1,443 deletions.
27 changes: 27 additions & 0 deletions compiler/Config.ml
Original file line number Diff line number Diff line change
Expand Up @@ -336,3 +336,30 @@ let type_check_pure_code = ref false
(** Shall we fail hard if we encounter an issue, or should we attempt to go
as far as possible while leaving "holes" in the generated code? *)
let fail_hard = ref true

(** if true, add the type name as a prefix
to the variant names.
Ex.:
In Rust:
{[
enum List = {
Cons(u32, Box<List>),x
Nil,
}
]}
F*, if option activated:
{[
type list =
| ListCons : u32 -> list -> list
| ListNil : list
]}
F*, if option not activated:
{[
type list =
| Cons : u32 -> list -> list
| Nil : list
]}
*)
let variant_concatenate_type_name = ref true
47 changes: 23 additions & 24 deletions compiler/Extract.ml
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,6 @@
open Pure
open PureUtils
open TranslateCore
open ExtractBase
open Config
include ExtractTypes

Expand Down Expand Up @@ -236,12 +235,10 @@ let rec extract_typed_pattern (ctx : extraction_ctx) (fmt : F.formatter)
(is_let : bool) (inside : bool) (v : typed_pattern) : extraction_ctx =
match v.value with
| PatConstant cv ->
ctx.fmt.extract_literal fmt inside cv;
extract_literal fmt inside cv;
ctx
| PatVar (v, _) ->
let vname =
ctx.fmt.var_basename ctx.names_maps.names_map.names_set v.basename v.ty
in
let vname = ctx_compute_var_basename ctx v.basename v.ty in
let ctx, vname = ctx_add_var vname v.id ctx in
F.pp_print_string fmt vname;
ctx
Expand Down Expand Up @@ -274,7 +271,7 @@ let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter)
| CVar var_id ->
let var_name = ctx_get_const_generic_var var_id ctx in
F.pp_print_string fmt var_name
| Const cv -> ctx.fmt.extract_literal fmt inside cv
| Const cv -> extract_literal fmt inside cv
| App _ ->
let app, args = destruct_apps e in
extract_App ctx fmt inside app args
Expand Down Expand Up @@ -354,10 +351,10 @@ and extract_function_call (ctx : extraction_ctx) (fmt : F.formatter)
* Note that the way we generate the translation, we shouldn't get the
* case where we have no argument (all functions are fully instantiated,
* and no AST transformation introduces partial calls). *)
ctx.fmt.extract_unop (extract_texpression ctx fmt) fmt inside unop arg
extract_unop (extract_texpression ctx fmt) fmt inside unop arg
| Binop (binop, int_ty), [ arg0; arg1 ] ->
(* Number of arguments: similar to unop *)
ctx.fmt.extract_binop
extract_binop
(extract_texpression ctx fmt)
fmt inside binop int_ty arg0 arg1
| Fun fun_id, _ ->
Expand Down Expand Up @@ -1359,7 +1356,7 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
is_opaque_coq && def.signature.generics <> empty_generic_params
in
(* Print the qualifier ("assume", etc.). *)
let qualif = ctx.fmt.fun_decl_kind_to_qualif kind in
let qualif = fun_decl_kind_to_qualif kind in
(match qualif with
| Some qualif ->
F.pp_print_string fmt qualif;
Expand Down Expand Up @@ -1655,7 +1652,7 @@ let extract_global_decl_body_gen (ctx : extraction_ctx) (fmt : F.formatter)
(* Open "QUALIF NAME : TYPE =" box (depth=1) *)
F.pp_open_hovbox fmt ctx.indent_incr;
(* Print "QUALIF NAME " *)
(match ctx.fmt.fun_decl_kind_to_qualif kind with
(match fun_decl_kind_to_qualif kind with
| Some qualif ->
F.pp_print_string fmt qualif;
F.pp_print_space fmt ()
Expand Down Expand Up @@ -1824,11 +1821,11 @@ let extract_trait_decl_register_parent_clause_names (ctx : extraction_ctx)
| None ->
List.map
(fun (c : trait_clause) ->
let name = ctx.fmt.trait_parent_clause_name trait_decl c in
let name = ctx_compute_trait_parent_clause_name ctx trait_decl c in
(* Add a prefix if necessary *)
let name =
if !Config.record_fields_short_names then name
else ctx.fmt.trait_decl_name trait_decl ^ name
else ctx_compute_trait_decl_name ctx trait_decl ^ name
in
(c.clause_id, name))
trait_decl.parent_clauses
Expand All @@ -1855,11 +1852,11 @@ let extract_trait_decl_register_constant_names (ctx : extraction_ctx)
| None ->
List.map
(fun (item_name, _) ->
let name = ctx.fmt.trait_const_name trait_decl item_name in
let name = ctx_compute_trait_const_name ctx trait_decl item_name in
(* Add a prefix if necessary *)
let name =
if !Config.record_fields_short_names then name
else ctx.fmt.trait_decl_name trait_decl ^ name
else ctx_compute_trait_decl_name ctx trait_decl ^ name
in
(item_name, name))
consts
Expand Down Expand Up @@ -1887,19 +1884,21 @@ let extract_trait_decl_type_names (ctx : extraction_ctx)
match builtin_info with
| None ->
let compute_type_name (item_name : string) : string =
let type_name = ctx.fmt.trait_type_name trait_decl item_name in
let type_name =
ctx_compute_trait_type_name ctx trait_decl item_name
in
if !Config.record_fields_short_names then type_name
else ctx.fmt.trait_decl_name trait_decl ^ type_name
else ctx_compute_trait_decl_name ctx trait_decl ^ type_name
in
let compute_clause_name (item_name : string) (clause : trait_clause) :
TraitClauseId.id * string =
let name =
ctx.fmt.trait_type_clause_name trait_decl item_name clause
ctx_compute_trait_type_clause_name ctx trait_decl item_name clause
in
(* Add a prefix if necessary *)
let name =
if !Config.record_fields_short_names then name
else ctx.fmt.trait_decl_name trait_decl ^ name
else ctx_compute_trait_decl_name ctx trait_decl ^ name
in
(clause.clause_id, name)
in
Expand Down Expand Up @@ -1971,7 +1970,7 @@ let extract_trait_decl_method_names (ctx : extraction_ctx)
(* Add a prefix if necessary *)
let name =
if !Config.record_fields_short_names then name
else ctx.fmt.trait_decl_name trait_decl ^ "_" ^ name
else ctx_compute_trait_decl_name ctx trait_decl ^ "_" ^ name
in
(f.back_id, name)
in
Expand Down Expand Up @@ -2036,8 +2035,8 @@ let extract_trait_decl_register_names (ctx : extraction_ctx)
let trait_name, trait_constructor =
match builtin_info with
| None ->
( ctx.fmt.trait_decl_name trait_decl,
ctx.fmt.trait_decl_constructor trait_decl )
( ctx_compute_trait_decl_name ctx trait_decl,
ctx_compute_trait_decl_constructor ctx trait_decl )
| Some info -> (info.extract_name, info.constructor)
in
let ctx = ctx_add (TraitDeclId trait_decl.def_id) trait_name ctx in
Expand Down Expand Up @@ -2101,7 +2100,7 @@ let extract_trait_impl_register_names (ctx : extraction_ctx)
(* Compute the name *)
let name =
match builtin_info with
| None -> ctx.fmt.trait_impl_name trait_decl trait_impl
| None -> ctx_compute_trait_impl_name ctx trait_decl trait_impl
| Some name -> name
in
ctx_add (TraitImplId trait_impl.def_id) name ctx
Expand Down Expand Up @@ -2214,7 +2213,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
(* Open the box for the name + generics *)
F.pp_open_hovbox fmt ctx.indent_incr;
let qualif =
Option.get (ctx.fmt.type_decl_kind_to_qualif SingleNonRec (Some Struct))
Option.get (type_decl_kind_to_qualif SingleNonRec (Some Struct))
in
(* When checking if the trait declaration is empty: we ignore the provided
methods, because for now they are extracted separately *)
Expand Down Expand Up @@ -2505,7 +2504,7 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
(* `let (....) : Trait ... =` *)
(* Open the box for the name + generics *)
F.pp_open_hovbox fmt ctx.indent_incr;
(match ctx.fmt.fun_decl_kind_to_qualif SingleNonRec with
(match fun_decl_kind_to_qualif SingleNonRec with
| Some qualif ->
F.pp_print_string fmt qualif;
F.pp_print_space fmt ()
Expand Down
Loading

0 comments on commit b916f69

Please sign in to comment.