summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/Config.ml5
-rw-r--r--compiler/ExtractToBackend.ml (renamed from compiler/ExtractToFStar.ml)0
-rw-r--r--compiler/Pure.ml2
-rw-r--r--compiler/PureMicroPasses.ml2
-rw-r--r--compiler/PureUtils.ml2
-rw-r--r--compiler/Translate.ml46
-rw-r--r--compiler/dune2
7 files changed, 30 insertions, 29 deletions
diff --git a/compiler/Config.ml b/compiler/Config.ml
index 1f91645b..c9723bd4 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -66,11 +66,12 @@ let use_state = ref true (* TODO *)
(st1, y) <-- f_fwd x st0;
...
x' <-- f_back x st0 y';
- }]
+ ]}
The second format is easier to reason about, but the first one is
necessary to properly handle some Rust functions which use internal
- mutability such as {{:https://doc.rust-lang.org/std/cell/struct.RefCell.html#method.try_borrow_mut} [RefCell::try_mut_borrow]}:
+ mutability such as
+ {{:https://doc.rust-lang.org/std/cell/struct.RefCell.html#method.try_borrow_mut}[RefCell::try_mut_borrow]}:
in order to model this behaviour we would need a state, and calling the backward
function would update the state by reinserting the updated value in it.
*)
diff --git a/compiler/ExtractToFStar.ml b/compiler/ExtractToBackend.ml
index fc04ce90..fc04ce90 100644
--- a/compiler/ExtractToFStar.ml
+++ b/compiler/ExtractToBackend.ml
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index fda2b3a6..b0114baa 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -500,7 +500,7 @@ type fun_effect_info = {
(** [true] if the function group is stateful. By *function group*, we mean
the set [{ forward function } U { backward functions }].
- We need this because of the option {!Config.backward_no_state_update}:
+ We need this because of the option {!val:Config.backward_no_state_update}:
if it is [true], then in case of a backward function {!stateful} is [false],
but we might need to know whether the corresponding forward function
is stateful or not.
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 132dc02e..30fc4989 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -1083,7 +1083,7 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
(** Decompose the monadic let-bindings.
- See the explanations in {!Config.decompose_monadic_let_bindings}
+ See the explanations in {!val:Config.decompose_monadic_let_bindings}
*)
let decompose_monadic_let_bindings (_ctx : trans_ctx) (def : fun_decl) :
fun_decl =
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index 0f16b5b4..ff55f322 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -73,7 +73,7 @@ let make_type_subst (vars : type_var list) (tys : ty list) : TypeVarId.id -> ty
in
fun id -> TypeVarId.Map.find id mp
-(** Retrieve the list of fields for the given variant of a {!type:Pure.type_decl}.
+(** Retrieve the list of fields for the given variant of a {!type:Aeneas.Pure.type_decl}.
Raises [Invalid_argument] if the arguments are incorrect.
*)
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 0171412b..79d1c913 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -343,7 +343,7 @@ let module_has_opaque_decls (ctx : gen_ctx) : bool * bool =
let extract_definitions (fmt : Format.formatter) (config : gen_config)
(ctx : gen_ctx) : unit =
(* Export the definition groups to the file, in the proper order *)
- let export_type (qualif : ExtractToFStar.type_decl_qualif)
+ let export_type (qualif : ExtractToBackend.type_decl_qualif)
(id : Pure.TypeDeclId.id) : unit =
(* Retrive the declaration *)
let def = Pure.TypeDeclId.Map.find id ctx.trans_types in
@@ -353,8 +353,8 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
| Enum _ | Struct _ -> (false, qualif)
| Opaque ->
let qualif =
- if config.interface then ExtractToFStar.TypeVal
- else ExtractToFStar.AssumeType
+ if config.interface then ExtractToBackend.TypeVal
+ else ExtractToBackend.AssumeType
in
(true, qualif)
in
@@ -363,7 +363,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
if
(is_opaque && config.extract_opaque)
|| ((not is_opaque) && config.extract_transparent)
- then ExtractToFStar.extract_type_decl ctx.extract_ctx fmt qualif def
+ then ExtractToBackend.extract_type_decl ctx.extract_ctx fmt qualif def
in
(* Utility to check a function has a decrease clause *)
@@ -393,7 +393,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
(fun (_, (fwd, _)) ->
let has_decr_clause = has_decreases_clause fwd in
if has_decr_clause then
- ExtractToFStar.extract_template_decreases_clause ctx.extract_ctx fmt
+ ExtractToBackend.extract_template_decreases_clause ctx.extract_ctx fmt
fwd)
pure_ls;
(* Extract the function definitions *)
@@ -413,12 +413,12 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
let is_opaque = Option.is_none fwd_def.Pure.body in
let qualif =
if is_opaque then
- if config.interface then ExtractToFStar.Val
- else ExtractToFStar.AssumeVal
- else if not is_rec then ExtractToFStar.Let
+ if config.interface then ExtractToBackend.Val
+ else ExtractToBackend.AssumeVal
+ else if not is_rec then ExtractToBackend.Let
else if is_mut_rec then
- if i = 0 then ExtractToFStar.LetRec else ExtractToFStar.And
- else ExtractToFStar.LetRec
+ if i = 0 then ExtractToBackend.LetRec else ExtractToBackend.And
+ else ExtractToBackend.LetRec
in
let has_decr_clause =
has_decreases_clause def && config.extract_decreases_clauses
@@ -428,7 +428,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
((not is_opaque) && config.extract_transparent)
|| (is_opaque && config.extract_opaque)
then
- ExtractToFStar.extract_fun_decl ctx.extract_ctx fmt qualif
+ ExtractToBackend.extract_fun_decl ctx.extract_ctx fmt qualif
has_decr_clause def)
fls);
(* Insert unit tests if necessary *)
@@ -436,7 +436,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
List.iter
(fun (keep_fwd, (fwd, _)) ->
if keep_fwd then
- ExtractToFStar.extract_unit_test_if_unit_fun ctx.extract_ctx fmt fwd)
+ ExtractToBackend.extract_unit_test_if_unit_fun ctx.extract_ctx fmt fwd)
pure_ls
in
@@ -454,29 +454,29 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
((not is_opaque) && config.extract_transparent)
|| (is_opaque && config.extract_opaque)
then
- ExtractToFStar.extract_global_decl ctx.extract_ctx fmt global body
+ ExtractToBackend.extract_global_decl ctx.extract_ctx fmt global body
config.interface
in
let export_state_type () : unit =
let qualif =
- if config.interface then ExtractToFStar.TypeVal
- else ExtractToFStar.AssumeType
+ if config.interface then ExtractToBackend.TypeVal
+ else ExtractToBackend.AssumeType
in
- ExtractToFStar.extract_state_type fmt ctx.extract_ctx qualif
+ ExtractToBackend.extract_state_type fmt ctx.extract_ctx qualif
in
let export_decl (decl : A.declaration_group) : unit =
match decl with
| Type (NonRec id) ->
- if config.extract_types then export_type ExtractToFStar.Type id
+ if config.extract_types then export_type ExtractToBackend.Type id
| Type (Rec ids) ->
(* Rk.: we shouldn't have (mutually) recursive opaque types *)
if config.extract_types then
List.iteri
(fun i id ->
let qualif =
- if i = 0 then ExtractToFStar.Type else ExtractToFStar.And
+ if i = 0 then ExtractToBackend.Type else ExtractToBackend.And
in
export_type qualif id)
ids
@@ -569,12 +569,12 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
* language, as well as some primitive names ("u32", etc.) *)
let variant_concatenate_type_name = true in
let fstar_fmt =
- ExtractToFStar.mk_formatter trans_ctx crate.name
+ ExtractToBackend.mk_formatter trans_ctx crate.name
variant_concatenate_type_name
in
let names_map =
PureToExtract.initialize_names_map fstar_fmt
- ExtractToFStar.fstar_names_map_init
+ ExtractToBackend.fstar_names_map_init
in
let ctx =
{ PureToExtract.trans_ctx; names_map; fmt = fstar_fmt; indent_incr = 2 }
@@ -596,7 +596,7 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
* sure there are no name clashes. *)
let ctx =
List.fold_left
- (fun ctx def -> ExtractToFStar.extract_type_decl_register_names ctx def)
+ (fun ctx def -> ExtractToBackend.extract_type_decl_register_names ctx def)
ctx trans_types
in
@@ -612,13 +612,13 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
let is_global = (fst def).Pure.is_global_decl_body in
if is_global then ctx
else
- ExtractToFStar.extract_fun_decl_register_names ctx keep_fwd
+ ExtractToBackend.extract_fun_decl_register_names ctx keep_fwd
gen_decr_clause def)
ctx trans_funs
in
let ctx =
- List.fold_left ExtractToFStar.extract_global_decl_register_names ctx
+ List.fold_left ExtractToBackend.extract_global_decl_register_names ctx
crate.globals
in
diff --git a/compiler/dune b/compiler/dune
index 85f4b75b..10aa9b10 100644
--- a/compiler/dune
+++ b/compiler/dune
@@ -20,7 +20,7 @@
Cps
Expressions
ExpressionsUtils
- ExtractToFStar
+ ExtractToBackend
FunsAnalysis
Identifiers
InterpreterBorrowsCore
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-19 03:57:45 +0000