Sort items before late-skip.

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
@@ -117,10 +116,9 @@ 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 bundles, _ =
-      let module DepGraph = Dependencies.Make (InputLanguage) in
-      DepGraph.recursive_bundles items
-    in
+    let module Deps = Dependencies.Make (InputLanguage) in
+    let items = Deps.global_sort items in
+    let bundles, _ = Deps.recursive_bundles items in
     let items =
       List.filter items ~f:(fun (i : AST.item) ->
           Attrs.late_skip i.attrs |> not)

engine/lib/ast_utils.ml

@@ -1285,22 +1285,25 @@ module Make (F : Features.T) = struct
     include U
     module Map = Map.M (U)
   end
-end
-
-module MakeWithNamePolicy (F : Features.T) (NP : Concrete_ident.NAME_POLICY) =
-struct
-  include Make (F)
-  open AST
-  module Concrete_ident_view = Concrete_ident.MakeViewAPI (NP)
 
-  let group_items_by_namespace (items : item list) : item list StringList.Map.t
-      =
+  let group_items_by_namespace_generic to_namespace (items : item list) :
+      item list StringList.Map.t =
     let h = Hashtbl.create (module StringList) in
     List.iter items ~f:(fun item ->
-        let ns = Concrete_ident_view.to_namespace item.ident in
+        let ns = to_namespace item.ident in
         let items = Hashtbl.find_or_add h ns ~default:(fun _ -> ref []) in
         items := !items @ [ item ]);
     Map.of_iteri_exn
       (module StringList)
       ~iteri:(Hashtbl.map h ~f:( ! ) |> Hashtbl.iteri)
 end
+
+module MakeWithNamePolicy (F : Features.T) (NP : Concrete_ident.NAME_POLICY) =
+struct
+  include Make (F)
+  open AST
+  module Concrete_ident_view = Concrete_ident.MakeViewAPI (NP)
+
+  let group_items_by_namespace : item list -> item list StringList.Map.t =
+    group_items_by_namespace_generic Concrete_ident_view.to_namespace
+end

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/concrete_ident/concrete_ident.ml

@@ -631,6 +631,18 @@ module Create = struct
     let path = List.drop_last_exn old.def_id.path @ [ last ] in
     { old with def_id = { old.def_id with path } }
 
+  let replace_last old chunk =
+    {
+      old with
+      def_id =
+        {
+          old.def_id with
+          path =
+            List.drop_last_exn old.def_id.path
+            @ [ { data = Imported.ValueNs chunk; disambiguator = 0 } ];
+        };
+    }
+
   let constructor name =
     let path = name.def_id.path @ [ { data = Ctor; disambiguator = 0 } ] in
     { name with def_id = { name.def_id with path } }

engine/lib/concrete_ident/concrete_ident.mli

@@ -39,6 +39,9 @@ module Create : sig
   (** [map_last f ident] applies [f] on the last chunk of [ident]'s
       path if it holds a string *)
 
+  val replace_last : t -> string -> t
+  (** [replace_last ident chunk] repalces the last chunk of [ident] by [chunk] *)
+
   val add_disambiguator : t -> int -> t
   (** [add_disambiguator ident d] changes the disambiguator on
       the last chunk of [ident]'s path to [d] *)

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)
@@ -239,6 +239,10 @@ module Make (F : Features.T) = struct
     let cycles g : Namespace.Set.t list =
       SCC.scc_list g |> List.map ~f:(Set.of_list (module Namespace))
 
+    let order g : Namespace.t list =
+      let module ModTopo = Graph.Topological.Make_stable (G) in
+      ModTopo.fold (fun ns l -> ns :: l) g []
+
     open Graph.Graphviz.Dot (struct
       include G
 
@@ -278,8 +282,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 +298,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,6 +326,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 =
@@ -332,6 +357,22 @@ module Make (F : Features.T) = struct
       Set.equal items items');
     items'
 
+  let global_sort (items : item list) : item list =
+    let sorted_by_namespace =
+      U.group_items_by_namespace_generic
+        Concrete_ident.DefaultViewAPI.to_namespace items
+      |> Map.data
+      |> List.map ~f:(fun items -> sort items)
+    in
+    let sorted_namespaces = ModGraph.order (ModGraph.of_items items) in
+    List.concat_map sorted_namespaces ~f:(fun namespace ->
+        List.find sorted_by_namespace ~f:(fun items ->
+            List.exists items ~f:(fun item ->
+                Namespace.equal
+                  (Namespace.of_concrete_ident item.ident)
+                  namespace))
+        |> Option.value ~default:[])
+
   let filter_by_inclusion_clauses' ~original_items
       (clauses : Types.inclusion_clause list) (items : item list) :
       item list * Concrete_ident.t Hash_set.t =
@@ -434,7 +475,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/dependencies.mli

@@ -3,7 +3,7 @@ module Make (F : Features.T) : sig
 
   val uid_associated_items : AST.item list -> Ast.attrs -> AST.item list
   val bundle_cyclic_modules : AST.item list -> AST.item list
-  val sort : AST.item list -> AST.item list
+  val global_sort : AST.item list -> AST.item list
   val recursive_bundles : AST.item list -> AST.item list list * AST.item list
 
   val filter_by_inclusion_clauses :

engine/lib/phases/phase_transform_hax_lib_inline.ml

@@ -71,6 +71,8 @@ module%inlined_contents Make (F : Features.T) = struct
     let first_global_ident (pat : B.pat) : global_ident option =
       UB.Reducers.collect_global_idents#visit_pat () pat |> Set.choose
 
+    let counter = ref 0
+
     let rec dexpr' span (expr : A.expr') : B.expr' =
       quote_of_expr' span expr
       |> Option.map ~f:(fun quote : B.expr' -> B.Quote quote)
@@ -206,7 +208,18 @@ 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))
+                   counter := !counter + 1;
+                   ( B.
+                       {
+                         v;
+                         span;
+                         ident =
+                           (* TODO: Replace with a proper unique ident. *)
+                           Concrete_ident.Create.replace_last item.ident
+                             ("__hax_quote__" ^ Int.to_string !counter);
+                         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*"
 '''