Merge pull request #935 from hacspec/handle-cyclic-module-dependencies

Handle cyclic module dependencies

engine/backends/coq/coq/coq_backend.ml

@@ -677,8 +677,8 @@ let hardcoded_coq_headers =
    Open Scope Z_scope.\n\
    Open Scope bool_scope.\n"
 
-let translate _ (_bo : BackendOptions.t) (items : AST.item list) :
-    Types.file list =
+let translate _ (_bo : BackendOptions.t) ~(bundles : AST.item list list)
+    (items : AST.item list) : Types.file list =
   U.group_items_by_namespace items
   |> Map.to_alist
   |> List.map ~f:(fun (ns, items) ->

engine/backends/coq/ssprove/ssprove_backend.ml

@@ -2404,8 +2404,8 @@ let hardcoded_coq_headers =
    Import choice.Choice.Exports.\n\n\
    Obligation Tactic := (* try timeout 8 *) solve_ssprove_obligations.\n"
 
-let translate _ (_bo : BackendOptions.t) (items : AST.item list) :
-    Types.file list =
+let translate _ (_bo : BackendOptions.t) ~(bundles : AST.item list list)
+    (items : AST.item list) : Types.file list =
   let analysis_data = StaticAnalysis.analyse items in
   U.group_items_by_namespace items
   |> Map.to_alist

engine/backends/easycrypt/easycrypt_backend.ml

@@ -332,8 +332,8 @@ let translate' (_bo : BackendOptions.t) (items : AST.item list) :
   doit Stdlib.Format.err_formatter items;
   []
 
-let translate _ (bo : BackendOptions.t) (items : AST.item list) :
-    Types.file list =
+let translate _ (bo : BackendOptions.t) ~(bundles : AST.item list list)
+    (items : AST.item list) : Types.file list =
   try translate' bo items
   with Assert_failure (file, line, col) ->
     Diagnostics.failure ~context:(Backend FStar) ~span:(Span.dummy ())

engine/backends/fstar/fstar_backend.ml

@@ -97,6 +97,11 @@ module Context = struct
   }
 end
 
+(** Convers a namespace to a module name *)
+let module_name (ns : string * string list) : string =
+  String.concat ~sep:"."
+    (List.map ~f:(map_first_letter String.uppercase) (fst ns :: snd ns))
+
 module Make
     (Attrs : Attrs.WITH_ITEMS) (Ctx : sig
       val ctx : Context.t
@@ -857,19 +862,17 @@ struct
       list =
     match e.v with
     | Alias { name; item } ->
-        let pat =
-          F.pat
-          @@ F.AST.PatVar
-               (F.id @@ U.Concrete_ident_view.to_definition_name name, None, [])
-        in
-        F.decls ~quals:[ F.AST.Unfold_for_unification_and_vcgen ]
-        @@ F.AST.TopLevelLet
-             ( NoLetQualifier,
-               [ (pat, F.term @@ F.AST.Name (pconcrete_ident item)) ] )
+        (* These should come from bundled items (in the case of cyclic module dependencies).
+           We make use of this f* feature: https://github.com/FStarLang/FStar/pull/3369 *)
+        let bundle = U.Concrete_ident_view.to_namespace item |> module_name in
+        [
+          `VerbatimImpl
+            ( Printf.sprintf "include %s {%s as %s}" bundle
+                (U.Concrete_ident_view.to_definition_name item)
+                (U.Concrete_ident_view.to_definition_name name),
+              `Newline );
+        ]
     | Fn { name; generics; body; params } ->
-        let is_rec =
-          Set.mem (U.Reducers.collect_concrete_idents#visit_expr () body) name
-        in
         let name = F.id @@ U.Concrete_ident_view.to_definition_name name in
         let pat = F.pat @@ F.AST.PatVar (name, None, []) in
         let generics = FStarBinder.of_generics e.span generics in
@@ -882,7 +885,7 @@ struct
               params
         in
         let pat = F.pat @@ F.AST.PatApp (pat, pat_args) in
-        let qualifier = F.AST.(if is_rec then Rec else NoLetQualifier) in
+        let qualifier = F.AST.(NoLetQualifier) in
         let impl =
           F.decl ~fsti:false
           @@ F.AST.TopLevelLet (qualifier, [ (pat, pexpr body) ])
@@ -1554,13 +1557,10 @@ let strings_of_item ~signature_only (bo : BackendOptions.t) m items
            if interface_mode then [ (`Impl s, `Newline); (`Intf s, `Newline) ]
            else [ (`Impl s, `Newline) ])
 
-(** Convers a namespace to a module name *)
-let module_name (ns : string * string list) : string =
-  String.concat ~sep:"."
-    (List.map ~f:(map_first_letter String.uppercase) (fst ns :: snd ns))
+type rec_prefix = NonRec | FirstMutRec | MutRec
 
-let string_of_items ~signature_only ~mod_name (bo : BackendOptions.t) m items :
-    string * string =
+let string_of_items ~signature_only ~mod_name ~bundles (bo : BackendOptions.t) m
+    items : string * string =
   let collect_trait_goal_idents =
     object
       inherit [_] Visitors.reduce as super
@@ -1600,14 +1600,48 @@ let string_of_items ~signature_only ~mod_name (bo : BackendOptions.t) m items :
           |> String.concat ~sep:"")
         ^ "\n\n"
   in
-  let strings =
-    List.concat_map ~f:(strings_of_item ~signature_only bo m items) items
-    |> List.map
-         ~f:
-           ((function
-              | `Impl s -> `Impl (String.strip s)
-              | `Intf s -> `Intf (String.strip s))
-           *** Fn.id)
+  let map_string ~f (str, space) =
+    ((match str with `Impl s -> `Impl (f s) | `Intf s -> `Intf (f s)), space)
+  in
+  let replace_in_strs ~pattern ~with_ =
+    List.map
+      ~f:
+        (map_string ~f:(fun str ->
+             String.substr_replace_first ~pattern ~with_ str))
+  in
+
+  (* Each of these bundles contains recursive items (mutually if the bundle has more than one element).
+     We know that these items will already be grouped together but we need to add the `rec` qualifier
+     to the first one (in the case of functions). And to replace the `let`/`type` keyword by `and`
+     for the other elements coming after. *)
+  let first_in_bundles = Array.create (List.length bundles) None in
+  let get_recursivity_prefix it =
+    match
+      List.findi bundles ~f:(fun _ bundle ->
+          List.mem bundle it ~equal:[%eq: item])
+    with
+    | Some (i, _) -> (
+        match first_in_bundles.(i) with
+        | Some first_it when [%eq: item] first_it it -> FirstMutRec
+        | Some _ -> MutRec
+        | None ->
+            first_in_bundles.(i) <- Some it;
+            FirstMutRec)
+    | None -> NonRec
+  in
+  let strings its =
+    List.concat_map
+      ~f:(fun item ->
+        let recursivity_prefix = get_recursivity_prefix item in
+        let strs = strings_of_item ~signature_only bo m items item in
+        match (recursivity_prefix, item.v) with
+        | FirstMutRec, Fn _ ->
+            replace_in_strs ~pattern:"let" ~with_:"let rec" strs
+        | MutRec, Fn _ -> replace_in_strs ~pattern:"let" ~with_:"and" strs
+        | MutRec, Type _ -> replace_in_strs ~pattern:"type" ~with_:"and" strs
+        | _ -> strs)
+      its
+    |> List.map ~f:(map_string ~f:String.strip)
     |> List.filter
          ~f:(fst >> (function `Impl s | `Intf s -> String.is_empty s) >> not)
   in
@@ -1617,7 +1651,7 @@ let string_of_items ~signature_only ~mod_name (bo : BackendOptions.t) m items :
         ~f:(fun (s, space) ->
           let* s = filter s in
           Some (s, space))
-        strings
+        (strings items)
     in
     let n = List.length l - 1 in
     let lines =
@@ -1643,8 +1677,8 @@ let fstar_headers (bo : BackendOptions.t) =
   in
   [ opts; "open Core"; "open FStar.Mul" ] |> String.concat ~sep:"\n"
 
-let translate m (bo : BackendOptions.t) (items : AST.item list) :
-    Types.file list =
+let translate m (bo : BackendOptions.t) ~(bundles : AST.item list list)
+    (items : AST.item list) : Types.file list =
   let show_view Concrete_ident.{ crate; path; definition } =
     crate :: (path @ [ definition ]) |> String.concat ~sep:"::"
   in
@@ -1663,7 +1697,7 @@ let translate m (bo : BackendOptions.t) (items : AST.item list) :
          in
          let mod_name = module_name ns in
          let impl, intf =
-           string_of_items ~signature_only ~mod_name bo m items
+           string_of_items ~signature_only ~mod_name ~bundles bo m items
          in
          let make ~ext body =
            if String.is_empty body then None
@@ -1681,7 +1715,6 @@ let translate m (bo : BackendOptions.t) (items : AST.item list) :
            [ make ~ext:"fst" impl; make ~ext:"fsti" intf ])
 
 open Phase_utils
-module DepGraph = Dependencies.Make (InputLanguage)
 module DepGraphR = Dependencies.Make (Features.Rust)
 
 module TransformToInputLanguage =
@@ -1765,6 +1798,5 @@ let apply_phases (bo : BackendOptions.t) (items : Ast.Rust.item list) :
     |> List.map ~f:unsize_as_identity
     |> List.map ~f:unsize_as_identity
     |> List.map ~f:U.Mappers.add_typ_ascription
-    (* |> DepGraph.name_me *)
   in
   items

engine/backends/proverif/proverif_backend.ml

@@ -865,8 +865,8 @@ module Make (Options : OPTS) : MAKE = struct
   end)
 end
 
-let translate m (bo : BackendOptions.t) (items : AST.item list) :
-    Types.file list =
+let translate m (bo : BackendOptions.t) ~(bundles : AST.item list list)
+    (items : AST.item list) : Types.file list =
   let (module M : MAKE) =
     (module Make (struct
       let options = bo

engine/bin/lib.ml

@@ -112,14 +112,17 @@ let run (options : Types.engine_options) : Types.output =
           ([%show: Diagnostics.Backend.t] M.backend));
     let items = apply_phases backend_options items in
     let with_items = Attrs.with_items items in
+    let module DepGraph = Dependencies.Make (InputLanguage) in
+    let items = DepGraph.bundle_cyclic_modules items in
+    let bundles, _ = DepGraph.recursive_bundles items in
     let items =
       List.filter items ~f:(fun (i : AST.item) ->
           Attrs.late_skip i.attrs |> not)
     in
     Logs.info (fun m ->
         m "Translating items with backend %s"
           ([%show: Diagnostics.Backend.t] M.backend));
-    let items = translate with_items backend_options items in
+    let items = translate with_items backend_options items ~bundles in
     items
   in
   let diagnostics, files =

engine/lib/backend.ml

@@ -31,6 +31,7 @@ module type T = sig
   val translate :
     (module Attrs.WITH_ITEMS) ->
     BackendOptions.t ->
+    bundles:AST.item list list ->
     AST.item list ->
     Types.file list