Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

fix(engine/deps): preserve definitions order whenever possible #1151

Closed
wants to merge 2 commits into from
Closed

fix(engine/deps): preserve definitions order whenever possible #1151

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
aa33ea4
fix(engine/deps): preserve definitions order whenever possible
W95Psp Nov 28, 2024
9f1120b
bless tests
W95Psp Jan 14, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
24 changes: 12 additions & 12 deletions engine/lib/dependencies.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -270,20 +270,20 @@ 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
in
let closure = ItemGraph.Oper.transitive_closure ~reflexive:true g in
let items' =
ItemGraph.Topological.fold List.cons g []
|> List.filter_map ~f:lookup |> List.rev
in
assert (
let of_list =
List.map ~f:ident_of >> Set.of_list (module Concrete_ident)
let compare a b =
let a, b = (a.ident, b.ident) in
let ab = ItemGraph.G.mem_edge closure a b in
let ba = ItemGraph.G.mem_edge closure b a in
match (ab, ba) with
| true, false -> -1
| false, true -> 1
| true, true -> 0
| false, false -> 0
in
let items = of_list items in
let items' = of_list items' in
Set.equal items items');
List.stable_sort ~compare items
in
items'

let filter_by_inclusion_clauses' ~original_items
Expand Down
98 changes: 49 additions & 49 deletions test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,49 +35,27 @@ module Attribute_opaque
open Core
open FStar.Mul

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

let t_OpaqueStruct (v_X: usize) (v_T v_U: Type0) = t_OpaqueStruct' 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)

let impl__S1__f_s1 = impl__S1__f_s1'

[@@ FStar.Tactics.Typeclasses.tcinstance]
assume
val impl_2': #v_U: Type0 -> {| i1: Core.Clone.t_Clone v_U |} -> t_TrGeneric i32 v_U

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)
val t_OpaqueEnum': v_X: usize -> v_T: Type0 -> v_U: Type0 -> eqtype

let impl__S2__f_s2 = impl__S2__f_s2'
let t_OpaqueEnum (v_X: usize) (v_T v_U: Type0) = t_OpaqueEnum' v_X v_T v_U

assume
val v_C': u8
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 v_C = v_C'
let ff_generic (v_X: usize) (#v_T #v_U: Type0) = ff_generic' v_X #v_T #v_U

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)

let ff_generic (v_X: usize) (#v_T #v_U: Type0) = ff_generic' v_X #v_T #v_U

assume
val ff_pre_post': x: bool -> y: bool
-> Prims.Pure bool
Expand All @@ -94,42 +72,44 @@ assume
val impl_T_for_u8': t_T u8

let impl_T_for_u8 = impl_T_for_u8'
'''
"Attribute_opaque.fsti" = '''
module Attribute_opaque
#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
open Core
open FStar.Mul

type t_S1 = | S1 : t_S1
[@@ FStar.Tactics.Typeclasses.tcinstance]
assume
val impl_2': #v_U: Type0 -> {| i1: Core.Clone.t_Clone v_U |} -> t_TrGeneric i32 v_U

type t_S2 = | S2 : t_S2
let impl_2 (#v_U: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Clone.t_Clone v_U) =
impl_2' #v_U #i1

val t_OpaqueEnum (v_X: usize) (v_T v_U: Type0) : eqtype
assume
val v_C': u8

val t_OpaqueStruct (v_X: usize) (v_T v_U: Type0) : eqtype
let v_C = v_C'

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;
f_f_post:v_U -> v_Self -> Type0;
f_f:x0: v_U -> Prims.Pure v_Self (f_f_pre x0) (fun result -> f_f_post x0 result)
}
assume
val impl__S1__f_s1': Prims.unit -> Prims.Pure Prims.unit 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 impl__S1__f_s1 = impl__S1__f_s1'

[@@ FStar.Tactics.Typeclasses.tcinstance]
val impl_2 (#v_U: Type0) {| i1: Core.Clone.t_Clone v_U |} : t_TrGeneric i32 v_U
assume
val impl__S2__f_s2': Prims.unit -> Prims.Pure Prims.unit Prims.l_True (fun _ -> Prims.l_True)

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'
'''
"Attribute_opaque.fsti" = '''
module Attribute_opaque
#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
open Core
open FStar.Mul

val v_C:u8
val t_OpaqueStruct (v_X: usize) (v_T v_U: Type0) : eqtype

val f (x y: bool) : Prims.Pure bool Prims.l_True (fun _ -> Prims.l_True)
val t_OpaqueEnum (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)
Expand All @@ -151,4 +131,24 @@ class t_T (v_Self: Type0) = {

[@@ 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;
f_f_post:v_U -> v_Self -> Type0;
f_f:x0: v_U -> Prims.Pure v_Self (f_f_pre x0) (fun result -> f_f_post x0 result)
}

[@@ FStar.Tactics.Typeclasses.tcinstance]
val impl_2 (#v_U: Type0) {| i1: Core.Clone.t_Clone v_U |} : t_TrGeneric i32 v_U

val v_C:u8

type t_S1 = | S1 : t_S1

val impl__S1__f_s1: Prims.unit -> Prims.Pure Prims.unit Prims.l_True (fun _ -> Prims.l_True)

type t_S2 = | S2 : t_S2

val impl__S2__f_s2: Prims.unit -> Prims.Pure Prims.unit Prims.l_True (fun _ -> Prims.l_True)
'''
Loading
Loading