Sort items in the backends module-wise instead of globally.

engine/backends/coq/coq/coq_backend.ml

@@ -762,6 +762,10 @@ let make (module M : Attrs.WITH_ITEMS) =
   new_printer
 
 let translate m _ ~bundles:_ (items : AST.item list) : Types.file list =
+  let items =
+    let module Deps = Dependencies.Make (InputLanguage) in
+    Deps.sort items
+  in
   let my_printer = make m in
   U.group_items_by_namespace items
   |> Map.to_alist

engine/backends/coq/ssprove/ssprove_backend.ml

@@ -2418,6 +2418,10 @@ let hardcoded_coq_headers =
 
 let translate _ (_bo : BackendOptions.t) ~(bundles : AST.item list list)
     (items : AST.item list) : Types.file list =
+  let items =
+    let module Deps = Dependencies.Make (InputLanguage) in
+    Deps.sort items
+  in
   let analysis_data = StaticAnalysis.analyse items in
   U.group_items_by_namespace items
   |> Map.to_alist

engine/backends/easycrypt/easycrypt_backend.ml

@@ -335,6 +335,10 @@ let translate' (_bo : BackendOptions.t) (items : AST.item list) :
 
 let translate _ (bo : BackendOptions.t) ~(bundles : AST.item list list)
     (items : AST.item list) : Types.file list =
+  let items =
+    let module Deps = Dependencies.Make (InputLanguage) in
+    Deps.sort items
+  in
   try translate' bo items
   with Assert_failure (file, line, col) ->
     Diagnostics.failure ~context:(Backend FStar) ~span:(Span.dummy ())

engine/backends/fstar/fstar_backend.ml

@@ -1748,6 +1748,10 @@ let translate_as_fstar m (bo : BackendOptions.t) ~(bundles : AST.item list list)
   U.group_items_by_namespace items
   |> Map.to_alist
   |> List.concat_map ~f:(fun (ns, items) ->
+         let items =
+           let module Deps = Dependencies.Make (InputLanguage) in
+           Deps.sort items
+         in
          let mod_name = module_name ns in
          let impl, intf = string_of_items ~mod_name ~bundles bo m items in
          let make ~ext body =

engine/backends/proverif/proverif_backend.ml

@@ -862,8 +862,13 @@ module Make (Options : OPTS) : MAKE = struct
   end)
 end
 
+open Phase_utils
+module DepGraph = Dependencies.Make (InputLanguage)
+module DepGraphR = Dependencies.Make (Features.Rust)
+
 let translate m (bo : BackendOptions.t) ~(bundles : AST.item list list)
     (items : AST.item list) : Types.file list =
+  let items = DepGraph.sort items in
   let (module M : MAKE) =
     (module Make (struct
       let options = bo
@@ -877,10 +882,6 @@ let translate m (bo : BackendOptions.t) ~(bundles : AST.item list list)
   in
   [ lib_file ]
 
-open Phase_utils
-module DepGraph = Dependencies.Make (InputLanguage)
-module DepGraphR = Dependencies.Make (Features.Rust)
-
 module TransformToInputLanguage =
   [%functor_application
   Phases.Reject.Unsafe(Features.Rust)

engine/bin/lib.ml

@@ -75,7 +75,6 @@ let import_thir_items (include_clauses : Types.inclusion_clause list)
   in
   Hax_io.write
     (ItemProcessed (List.filter_map ~f:(fun i -> Span.owner_hint i.span) items));
-  let items = Deps.sort items in
   (* Extract error reports for the items we actually extract *)
   let reports =
     List.concat_map

engine/lib/attr_payloads.ml

@@ -154,6 +154,7 @@ module Make (F : Features.T) (Error : Phase_utils.ERROR) = struct
   (* TODO: Maybe rename me `graph` or something? *)
   module type WITH_ITEMS = sig
     val item_uid_map : item UId.Map.t
+    val try_item_of_uid : UId.t -> item option
     val item_of_uid : UId.t -> item
     val associated_items_per_roles : attrs -> item list AssocRole.Map.t
     val associated_item : AssocRole.t -> attrs -> item option
@@ -222,8 +223,10 @@ module Make (F : Features.T) (Error : Phase_utils.ERROR) = struct
       in
       map_of_alist (module UId) l ~dup
 
+    let try_item_of_uid (uid : UId.t) : item option = Map.find item_uid_map uid
+
     let item_of_uid (uid : UId.t) : item =
-      Map.find item_uid_map uid
+      try_item_of_uid uid
       |> Option.value_or_thunk ~default:(fun () ->
              Error.assertion_failure (Span.dummy ())
              @@ "Could not find item with UID "

engine/lib/dependencies.ml

@@ -37,7 +37,7 @@ module Make (F : Features.T) = struct
     let open Attrs.WithItems (struct
       let items = items
     end) in
-    raw_associated_item >> List.map ~f:(snd >> item_of_uid)
+    raw_associated_item >> List.filter_map ~f:(snd >> try_item_of_uid)
 
   module ItemGraph = struct
     module G = Graph.Persistent.Digraph.Concrete (Concrete_ident)
@@ -278,8 +278,6 @@ module Make (F : Features.T) = struct
     let g =
       ItemGraph.of_items ~original_items:items items |> ItemGraph.Oper.mirror
     in
-    let items_array = Array.of_list items in
-    let lookup (index : int) = items_array.(index) in
     let stable_g =
       let to_index =
         items
@@ -296,15 +294,17 @@ module Make (F : Features.T) = struct
           ItemGraph.GInt.add_vertex g i)
     in
     let items' =
+      let items_array = Array.of_list items in
+      let lookup (index : int) = items_array.(index) in
       ItemGraph.Topological.fold List.cons stable_g [] |> List.map ~f:lookup
     in
     (* Stable topological sort doesn't guarantee to group cycles together.
        We make this correction to ensure mutually recursive items are grouped. *)
-    let cycles =
-      ItemGraph.MutRec.SCC.scc_list g
-      |> List.filter ~f:(fun cycle -> List.length cycle > 1)
-    in
     let items' =
+      let cycles =
+        ItemGraph.MutRec.SCC.scc_list g
+        |> List.filter ~f:(fun cycle -> List.length cycle > 1)
+      in
       List.fold items' ~init:[] ~f:(fun acc item ->
           match
             List.find cycles ~f:(fun cycle ->
@@ -322,7 +322,27 @@ module Make (F : Features.T) = struct
           | None -> [ item ] :: acc)
       |> List.concat
     in
-
+    (* Quote items must be placed right before or after their origin *)
+    let items' =
+      let quotes =
+        List.filter_map items' ~f:(fun item ->
+            match item.v with
+            | Quote { origin; _ } -> Some (origin, item)
+            | _ -> None)
+      in
+      List.fold quotes ~init:items' ~f:(fun items' (origin, quote_item) ->
+          match origin.position with
+          | `Before | `After ->
+              List.concat_map items' ~f:(fun item ->
+                  if [%eq: concrete_ident] origin.item_ident item.ident then
+                    match origin.position with
+                    | `After -> [ item; quote_item ]
+                    | _ -> [ quote_item; item ]
+                  else if [%eq: concrete_ident] quote_item.ident item.ident then
+                    []
+                  else [ item ])
+          | `Replace -> items')
+    in
     assert (
       let of_list =
         List.map ~f:ident_of >> Set.of_list (module Concrete_ident)
@@ -434,7 +454,12 @@ module Make (F : Features.T) = struct
             List.filter ~f:(fun att -> Attrs.late_skip [ att ]) item.attrs
           in
 
-          { item with v = Alias { name = old_ident; item = new_ident }; attrs })
+          {
+            item with
+            v = Alias { name = old_ident; item = new_ident };
+            attrs;
+            ident = old_ident;
+          })
     in
     item' :: aliases
 

engine/lib/phases/phase_transform_hax_lib_inline.ml

@@ -206,7 +206,22 @@ module%inlined_contents Make (F : Features.T) = struct
                      Quote { quote; origin }
                    in
                    let attrs = [ Attr_payloads.to_attr attr assoc_item.span ] in
-                   (B.{ v; span; ident = item.ident; attrs }, position))
+                   ( B.
+                       {
+                         v;
+                         span;
+                         ident =
+                           (* TODO: Replace with a proper unique ident. *)
+                           item.ident
+                           |> Concrete_ident.Create.map_last ~f:(fun s ->
+                                  s ^ "__hax_quote__"
+                                  ^
+                                  match position with
+                                  | After -> "after"
+                                  | Before -> "before");
+                         attrs;
+                       },
+                     position ))
             |> List.partition_tf ~f:(snd >> [%matches? Types.Before])
             |> map_fst *** map_fst
           with Diagnostics.SpanFreeError.Exn (Data (context, kind)) ->

test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap

@@ -67,6 +67,12 @@ val ff_pre_post': x: bool -> y: bool
 
 let ff_pre_post = ff_pre_post'
 
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+assume
+val impl_T_for_u8': t_T u8
+
+let impl_T_for_u8 = impl_T_for_u8'
+
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 assume
 val impl_2': #v_U: Type0 -> {| i1: Core.Clone.t_Clone v_U |} -> t_TrGeneric i32 v_U
@@ -88,12 +94,6 @@ assume
 val impl__S2__f_s2': Prims.unit -> Prims.Pure Prims.unit Prims.l_True (fun _ -> Prims.l_True)
 
 let impl__S2__f_s2 = impl__S2__f_s2'
-
-[@@ FStar.Tactics.Typeclasses.tcinstance]
-assume
-val impl_T_for_u8': t_T u8
-
-let impl_T_for_u8 = impl_T_for_u8'
 '''
 "Attribute_opaque.fsti" = '''
 module Attribute_opaque
@@ -118,6 +118,20 @@ val ff_pre_post (x y: bool)
           let result:bool = result in
           result =. y)
 
+class t_T (v_Self: Type0) = {
+  f_U:Type0;
+  f_c:u8;
+  f_d_pre:Prims.unit -> Type0;
+  f_d_post:Prims.unit -> Prims.unit -> Type0;
+  f_d:x0: Prims.unit -> Prims.Pure Prims.unit (f_d_pre x0) (fun result -> f_d_post x0 result);
+  f_m_pre:self___: v_Self -> x: u8 -> pred: Type0{x =. 0uy ==> pred};
+  f_m_post:v_Self -> u8 -> bool -> Type0;
+  f_m:x0: v_Self -> x1: u8 -> Prims.Pure bool (f_m_pre x0 x1) (fun result -> f_m_post x0 x1 result)
+}
+
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+val impl_T_for_u8:t_T u8
+
 class t_TrGeneric (v_Self: Type0) (v_U: Type0) = {
   [@@@ FStar.Tactics.Typeclasses.no_method]_super_13225137425257751668:Core.Clone.t_Clone v_U;
   f_f_pre:v_U -> Type0;
@@ -137,18 +151,4 @@ val impl__S1__f_s1: Prims.unit -> Prims.Pure Prims.unit Prims.l_True (fun _ -> P
 type t_S2 = | S2 : t_S2
 
 val impl__S2__f_s2: Prims.unit -> Prims.Pure Prims.unit Prims.l_True (fun _ -> Prims.l_True)
-
-class t_T (v_Self: Type0) = {
-  f_U:Type0;
-  f_c:u8;
-  f_d_pre:Prims.unit -> Type0;
-  f_d_post:Prims.unit -> Prims.unit -> Type0;
-  f_d:x0: Prims.unit -> Prims.Pure Prims.unit (f_d_pre x0) (fun result -> f_d_post x0 result);
-  f_m_pre:self___: v_Self -> x: u8 -> pred: Type0{x =. 0uy ==> pred};
-  f_m_post:v_Self -> u8 -> bool -> Type0;
-  f_m:x0: v_Self -> x1: u8 -> Prims.Pure bool (f_m_pre x0 x1) (fun result -> f_m_post x0 x1 result)
-}
-
-[@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_T_for_u8:t_T u8
 '''

test-harness/src/snapshots/toolchain__attributes into-fstar.snap

@@ -516,8 +516,6 @@ type t_Foo = {
 
 let inlined_code__V: u8 = 12uy
 
-unfold let some_function _ = "hello from F*"
-
 let before_inlined_code = "example before"
 
 let inlined_code (foo: t_Foo) : Prims.unit =
@@ -530,4 +528,6 @@ let inlined_code (foo: t_Foo) : Prims.unit =
   ()
 
 let inlined_code_after = "example after"
+
+unfold let some_function _ = "hello from F*"
 '''