Reorganize the project to prepare for new backends

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