Skip to content

Commit

Permalink
Revert "Move trait methods in cyclic dependencies bundling."
Browse files Browse the repository at this point in the history
This reverts commit 43829c4.
  • Loading branch information
maximebuyse committed Jan 30, 2025
1 parent b5bceaf commit 5530d5a
Show file tree
Hide file tree
Showing 3 changed files with 0 additions and 72 deletions.
5 changes: 0 additions & 5 deletions engine/lib/dependencies.ml
Original file line number Diff line number Diff line change
Expand Up @@ -561,11 +561,6 @@ module Make (F : Features.T) = struct
( name,
Concrete_ident.Create.move_under ~new_parent:new_name name
)))
| Some { v = Trait { items; _ }; _ } ->
List.map items ~f:(fun { ti_ident; _ } ->
( ti_ident,
Concrete_ident.Create.move_under ~new_parent:new_name ti_ident
))
| _ -> []
in
let variant_and_constructors_renamings =
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -259,56 +259,6 @@ include Cyclic_modules.M1.Cyclic_bundle_892895908 {b as b}

include Cyclic_modules.M1.Cyclic_bundle_892895908 {c as c}
'''
"Cyclic_modules.Moved_trait.Nested.fst" = '''
module Cyclic_modules.Moved_trait.Nested
#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
open Core
open FStar.Mul

include Cyclic_modules.Moved_trait.Rec_bundle_963167032 {t_St as t_St}

include Cyclic_modules.Moved_trait.Rec_bundle_963167032 {g as g}
'''
"Cyclic_modules.Moved_trait.Rec_bundle_963167032.fst" = '''
module Cyclic_modules.Moved_trait.Rec_bundle_963167032
#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
open Core
open FStar.Mul

class v_Tr (v_Self: Type0) = {
f_f_pre:v_Self -> Type0;
f_f_post:v_Self -> Prims.unit -> Type0;
f_f:x0: v_Self -> Prims.Pure Prims.unit (f_f_pre x0) (fun result -> f_f_post x0 result)
}

type t_St = | St : t_St

[@@ FStar.Tactics.Typeclasses.tcinstance]
let impl: v_Tr t_St =
{
f_f_pre = (fun (self: t_St) -> true);
f_f_post = (fun (self: t_St) (out: Prims.unit) -> true);
f_f = fun (self: t_St) -> ()
}

let g (x: t_St) : Prims.unit = f_f #t_St #FStar.Tactics.Typeclasses.solve x
'''
"Cyclic_modules.Moved_trait.fst" = '''
module Cyclic_modules.Moved_trait
#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
open Core
open FStar.Mul

include Cyclic_modules.Moved_trait.Rec_bundle_963167032 {v_Tr as v_Tr}

include Cyclic_modules.Moved_trait.Rec_bundle_963167032 {f_f_pre as f_f_pre}

include Cyclic_modules.Moved_trait.Rec_bundle_963167032 {f_f_post as f_f_post}

include Cyclic_modules.Moved_trait.Rec_bundle_963167032 {f_f as f_f}

include Cyclic_modules.Moved_trait.Rec_bundle_963167032 {impl as impl}
'''
"Cyclic_modules.Rec.fst" = '''
module Cyclic_modules.Rec
#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
Expand Down
17 changes: 0 additions & 17 deletions tests/cyclic-modules/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -178,20 +178,3 @@ pub mod late_skip_b {
super::late_skip_a::f()
}
}

pub mod moved_trait {
impl Tr for nested::St {
fn f(self) {}
}
pub trait Tr {
fn f(self);
}

pub mod nested {
use super::Tr;
pub struct St {}
fn g(x: St) {
x.f()
}
}
}

0 comments on commit 5530d5a

Please sign in to comment.