Stable topological sort using original order.

cryspen · Jan 20, 2025 · 33e910e · 33e910e
1 parent fa1b025
commit 33e910e
Show file tree

Hide file tree

Showing 30 changed files with 1,647 additions and 1,492 deletions.
diff --git a/engine/lib/dependencies.ml b/engine/lib/dependencies.ml
@@ -41,7 +41,15 @@ module Make (F : Features.T) = struct
 
   module ItemGraph = struct
     module G = Graph.Persistent.Digraph.Concrete (Concrete_ident)
-    module Topological = Graph.Topological.Make_stable (G)
+
+    module StableG = struct
+      include Graph.Persistent.Digraph.Concrete (Int)
+
+      let empty () = empty
+    end
+
+    module Topological = Graph.Topological.Make_stable (StableG)
+    module GMap = Graph.Gmap.Edge (G) (StableG)
     module Oper = Graph.Oper.P (G)
 
     let vertices_of_item (i : item) : G.V.t list =
@@ -270,13 +278,55 @@ module Make (F : Features.T) = struct
     let g =
       ItemGraph.of_items ~original_items:items items |> ItemGraph.Oper.mirror
     in
-    let lookup (name : concrete_ident) =
-      List.find ~f:(ident_of >> Concrete_ident.equal name) items
+    let items_array = Array.of_list items in
+    let name_index =
+      items
+      |> List.mapi ~f:(fun i item -> (item.ident, i))
+      |> Map.of_alist_exn (module Concrete_ident)
+    in
+
+    let lookup (index : int) = items_array.(index) in
+    let stable_g =
+      ItemGraph.GMap.filter_map
+        (fun ((name1, name2) : concrete_ident * concrete_ident) ->
+          let to_index = Map.find name_index in
+          let i1, i2 = (to_index name1, to_index name2) in
+
+          Option.both i1 i2)
+        g
+    in
+    let stable_g =
+      List.foldi items ~init:stable_g ~f:(fun i g _ ->
+          ItemGraph.StableG.add_vertex g i)
+    in
+    let items' =
+      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' =
-      ItemGraph.Topological.fold List.cons g []
-      |> List.filter_map ~f:lookup |> List.rev
+      List.fold items' ~init:[] ~f:(fun acc item ->
+          match
+            List.find cycles ~f:(fun cycle ->
+                List.mem cycle item.ident ~equal:[%eq: concrete_ident])
+          with
+          | Some _
+            when List.exists acc ~f:(fun els ->
+                     List.mem els item ~equal:[%eq: item]) ->
+              [] :: acc
+          | Some cycle ->
+              List.map cycle ~f:(fun ident ->
+                  List.find_exn items ~f:(fun item ->
+                      [%eq: concrete_ident] item.ident ident))
+              :: acc
+          | None -> [ item ] :: acc)
+      |> List.concat
     in
+
     assert (
       let of_list =
         List.map ~f:ident_of >> Set.of_list (module Concrete_ident)

diff --git a/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap b/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap
@@ -35,20 +35,37 @@ module Attribute_opaque
 open Core
 open FStar.Mul
 
+assume
+val t_OpaqueStruct': v_X: usize -> v_T: Type0 -> v_U: Type0 -> eqtype
+
+let t_OpaqueStruct (v_X: usize) (v_T v_U: Type0) = t_OpaqueStruct' v_X v_T v_U
+
 assume
 val t_OpaqueEnum': v_X: usize -> v_T: Type0 -> v_U: Type0 -> eqtype
 
 let t_OpaqueEnum (v_X: usize) (v_T v_U: Type0) = t_OpaqueEnum' v_X v_T v_U
 
 assume
-val t_OpaqueStruct': v_X: usize -> v_T: Type0 -> v_U: Type0 -> eqtype
+val ff_generic': v_X: usize -> #v_T: Type0 -> #v_U: Type0 -> x: v_U
+  -> Prims.Pure (t_OpaqueEnum v_X v_T v_U) Prims.l_True (fun _ -> Prims.l_True)
 
-let t_OpaqueStruct (v_X: usize) (v_T v_U: Type0) = t_OpaqueStruct' v_X v_T v_U
+let ff_generic (v_X: usize) (#v_T #v_U: Type0) = ff_generic' v_X #v_T #v_U
 
 assume
-val impl__S1__f_s1': Prims.unit -> Prims.Pure Prims.unit Prims.l_True (fun _ -> Prims.l_True)
+val f': x: bool -> y: bool -> Prims.Pure bool Prims.l_True (fun _ -> Prims.l_True)
 
-let impl__S1__f_s1 = impl__S1__f_s1'
+let f = f'
+
+assume
+val ff_pre_post': x: bool -> y: bool
+  -> Prims.Pure bool
+      (requires x)
+      (ensures
+        fun result ->
+          let result:bool = result in
+          result =. y)
+
+let ff_pre_post = ff_pre_post'
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 assume
@@ -57,37 +74,20 @@ val impl_2': #v_U: Type0 -> {| i1: Core.Clone.t_Clone v_U |} -> t_TrGeneric i32
 let impl_2 (#v_U: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Clone.t_Clone v_U) =
   impl_2' #v_U #i1
 
-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'
-
 assume
 val v_C': u8
 
 let v_C = v_C'
 
 assume
-val f': x: bool -> y: bool -> Prims.Pure bool Prims.l_True (fun _ -> Prims.l_True)
-
-let f = f'
-
-assume
-val ff_generic': v_X: usize -> #v_T: Type0 -> #v_U: Type0 -> x: v_U
-  -> Prims.Pure (t_OpaqueEnum v_X v_T v_U) Prims.l_True (fun _ -> Prims.l_True)
+val impl__S1__f_s1': Prims.unit -> Prims.Pure Prims.unit Prims.l_True (fun _ -> Prims.l_True)
 
-let ff_generic (v_X: usize) (#v_T #v_U: Type0) = ff_generic' v_X #v_T #v_U
+let impl__S1__f_s1 = impl__S1__f_s1'
 
 assume
-val ff_pre_post': x: bool -> y: bool
-  -> Prims.Pure bool
-      (requires x)
-      (ensures
-        fun result ->
-          let result:bool = result in
-          result =. y)
+val impl__S2__f_s2': Prims.unit -> Prims.Pure Prims.unit Prims.l_True (fun _ -> Prims.l_True)
 
-let ff_pre_post = ff_pre_post'
+let impl__S2__f_s2 = impl__S2__f_s2'
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 assume
@@ -101,13 +101,22 @@ module Attribute_opaque
 open Core
 open FStar.Mul
 
-type t_S1 = | S1 : t_S1
-
-type t_S2 = | S2 : t_S2
+val t_OpaqueStruct (v_X: usize) (v_T v_U: Type0) : eqtype
 
 val t_OpaqueEnum (v_X: usize) (v_T v_U: Type0) : eqtype
 
-val t_OpaqueStruct (v_X: usize) (v_T v_U: Type0) : eqtype
+val ff_generic (v_X: usize) (#v_T #v_U: Type0) (x: v_U)
+    : Prims.Pure (t_OpaqueEnum v_X v_T v_U) Prims.l_True (fun _ -> Prims.l_True)
+
+val f (x y: bool) : Prims.Pure bool Prims.l_True (fun _ -> Prims.l_True)
+
+val ff_pre_post (x y: bool)
+    : Prims.Pure bool
+      (requires x)
+      (ensures
+        fun result ->
+          let result:bool = result in
+          result =. y)
 
 class t_TrGeneric (v_Self: Type0) (v_U: Type0) = {
   [@@@ FStar.Tactics.Typeclasses.no_method]_super_13225137425257751668:Core.Clone.t_Clone v_U;
@@ -116,27 +125,18 @@ class t_TrGeneric (v_Self: Type0) (v_U: Type0) = {
   f_f:x0: v_U -> Prims.Pure v_Self (f_f_pre x0) (fun result -> f_f_post x0 result)
 }
 
-val impl__S1__f_s1: Prims.unit -> Prims.Pure Prims.unit Prims.l_True (fun _ -> Prims.l_True)
-
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 val impl_2 (#v_U: Type0) {| i1: Core.Clone.t_Clone v_U |} : t_TrGeneric i32 v_U
 
-val impl__S2__f_s2: Prims.unit -> Prims.Pure Prims.unit Prims.l_True (fun _ -> Prims.l_True)
-
 val v_C:u8
 
-val f (x y: bool) : Prims.Pure bool Prims.l_True (fun _ -> Prims.l_True)
+type t_S1 = | S1 : t_S1
 
-val ff_generic (v_X: usize) (#v_T #v_U: Type0) (x: v_U)
-    : Prims.Pure (t_OpaqueEnum v_X v_T v_U) Prims.l_True (fun _ -> Prims.l_True)
+val impl__S1__f_s1: Prims.unit -> Prims.Pure Prims.unit Prims.l_True (fun _ -> Prims.l_True)
 
-val ff_pre_post (x y: bool)
-    : Prims.Pure bool
-      (requires x)
-      (ensures
-        fun result ->
-          let result:bool = result in
-          result =. y)
+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;