From 8600a3709d77ed34236c5c8af4561f4abdc6073b Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Thu, 2 Jun 2022 06:04:34 -0400 Subject: [PATCH 01/12] replace `(mut)` with `mut` in `MaybeMut` --- src/mir/test/basic.rkt | 2 +- src/mir/type-check-goal.rkt | 2 +- src/mir/type-of.rkt | 2 +- src/ty/grammar.rkt | 4 ++-- src/ty/parameters.rkt | 2 +- 5 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/mir/test/basic.rkt b/src/mir/test/basic.rkt index 359325c4..88896e61 100644 --- a/src/mir/test/basic.rkt +++ b/src/mir/test/basic.rkt @@ -15,7 +15,7 @@ (redex-let* formality-mir - ((LocalDecls_foo (term ((_0 (scalar-ty i32) (mut)) + ((LocalDecls_foo (term ((_0 (scalar-ty i32) mut) (_1 (scalar-ty i32) ()) ))) (BasicBlockData_bb0 (term (((_0 = (use (copy _1)))) return))) diff --git a/src/mir/type-check-goal.rkt b/src/mir/type-check-goal.rkt index 9aa13bc7..5e4ba99c 100644 --- a/src/mir/type-check-goal.rkt +++ b/src/mir/type-check-goal.rkt @@ -72,7 +72,7 @@ [(type-of/Place Γ Place Ty_place) (type-of/Rvalue Γ Rvalue Ty_rvalue) - #;(mutability/Place Γ Place (mut)) + #;(mutability/Place Γ Place mut) ---------------------------------------- (type-check-goal/Statement Γ (Place = Rvalue) diff --git a/src/mir/type-of.rkt b/src/mir/type-of.rkt index 9a9ea169..a091f47e 100644 --- a/src/mir/type-of.rkt +++ b/src/mir/type-of.rkt @@ -163,7 +163,7 @@ [; ref-mut (type-of/Place Γ Place Ty) ------------------------------------------ - (type-of/Rvalue Γ (ref Lt (mut) Place) (&mut Lt Ty)) + (type-of/Rvalue Γ (ref Lt mut Place) (&mut Lt Ty)) ] [; binop diff --git a/src/ty/grammar.rkt b/src/ty/grammar.rkt index a6a2b06c..edb555c7 100644 --- a/src/ty/grammar.rkt +++ b/src/ty/grammar.rkt @@ -137,7 +137,7 @@ (AssociatedTy ::= (TraitId AssociatedTyId)) ;; MaybeMut: either mut or not - (MaybeMut ::= () (mut)) + (MaybeMut ::= () mut) ;; Pairs of variables (X0, X1), used as a kind of map (VarIdPairs ::= (VarIdPair ...)) @@ -205,7 +205,7 @@ (define-metafunction formality-ty &mut : Lt Ty -> Ty - [(&mut Lt Ty) (rigid-ty (ref (mut)) (Lt Ty))] + [(&mut Lt Ty) (rigid-ty (ref mut) (Lt Ty))] ) (define-metafunction formality-ty diff --git a/src/ty/parameters.rkt b/src/ty/parameters.rkt index 13fd0bff..bd31213d 100644 --- a/src/ty/parameters.rkt +++ b/src/ty/parameters.rkt @@ -40,7 +40,7 @@ [(generics-for Env AdtId) (env-adt-generics Env AdtId)] [(generics-for Env ScalarId) (() ())] [(generics-for Env (ref ())) (((TheLt (lifetime +)) (TheTy (type +))) ((TheTy : TheLt)))] - [(generics-for Env (ref (mut))) (((TheLt (lifetime +)) (TheTy (type =))) ((TheTy : TheLt)))] + [(generics-for Env (ref mut)) (((TheLt (lifetime +)) (TheTy (type =))) ((TheTy : TheLt)))] [; tuples are covariant in their elements P1...Pn (generics-for Env (tuple number_arity)) From a160c0537248ccfc6c68d51167ab1118e623594a Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Thu, 2 Jun 2022 06:04:44 -0400 Subject: [PATCH 02/12] encode the static from #25860 --- src/mir/test/issue-25860.rkt | 165 +++++++++++++++++++++++++++++++++++ 1 file changed, 165 insertions(+) create mode 100644 src/mir/test/issue-25860.rkt diff --git a/src/mir/test/issue-25860.rkt b/src/mir/test/issue-25860.rkt new file mode 100644 index 00000000..3db47b13 --- /dev/null +++ b/src/mir/test/issue-25860.rkt @@ -0,0 +1,165 @@ +#lang racket +(require redex/reduction-semantics + "../all-check.rkt" + "../grammar.rkt" + "../../ty/grammar.rkt" + "../../util.rkt" + ) + +(module+ test + ;; Program: + ;; + ;; ``` + ;; static UNIT: &'static &'static () = &&(); + ;; fn foo<'a, 'b, T>(_: &'a &'b (), v: &'b T) -> &'a T { + ;; v + ;; } + ;; fn bad<'a, T>(x: &'a T) -> &'static T { + ;; let f: fn(_, &'a T) -> &'static T = foo; + ;; f(UNIT, x) + ;; } + ;; fn main() { + ;; let value = { + ;; let data = 22; + ;; bad(&data) + ;; }; + ;; let _ = *value; + ;; } + ;; ``` + + (redex-let* + formality-mir + + [ + ;; ``` + ;; static UNIT: &'static &'static () = &&(); + ;; { // MIR (actually, the real MIR is "promoted", but this is close enough for our purposes) + ;; let mut _0: &&(); // return place in scope 0 at src/main.rs:1:37: 1:41 + ;; let mut _1: &(); // in scope 0 at src/main.rs:1:38: 1:41 + ;; let mut _2: (); // in scope 0 at src/main.rs:1:39: 1:41 + ;; + ;; bb0: { + ;; nop; // scope 0 at src/main.rs:1:39: 1:41 + ;; _1 = &_2; // scope 0 at src/main.rs:1:38: 1:41 + ;; _0 = &_1; // scope 0 at src/main.rs:1:37: 1:41 + ;; return; // scope 0 at src/main.rs:1:37: 1:41 + ;; } + ;; } + ;; ``` + (StaticDecl_UNIT (term (UNIT (static + () ; generics + () ; where-clauses + (& static (& static unit-ty)) ; type + (∃ + ((lifetime L0) + (lifetime L1) + (lifetime L2) + (lifetime L3) + (lifetime L4) + ) + ([(_0 (& L0 (& L1 unit-ty)) mut) + (_1 (& L2 unit-ty) mut) + (_2 unit-ty mut) + ] + [(bb0 {(noop + (_1 = (ref L3 () _2)) + (_0 = (ref L4 () _1))) + return + })] + ) + ) + )))) + ] + + (traced '() + (test-equal "FIXME" "FIXME")) + ) + ) + +;; ``` +;; fn foo<'a, 'b, T>(_: &'a &'b (), v: &'b T) -> &'a T { +;; v +;; } +;; MIR { +;; debug v => _2; // in scope 0 at src/main.rs:3:34: 3:35 +;; let mut _0: &T; // return place in scope 0 at src/main.rs:3:47: 3:52 +;; +;; bb0: { +;; _0 = _2; // scope 0 at src/main.rs:4:5: 4:6 +;; return; // scope 0 at src/main.rs:5:2: 5:2 +;; } +;; } +;; +;; fn bad<'a, T>(x: &'a T) -> &'static T { +;; let f: fn(_, &'a T) -> &'static T = foo; +;; f(UNIT, x) +;; } +;; MIR { +;; debug x => _1; // in scope 0 at src/main.rs:7:15: 7:16 +;; let mut _0: &T; // return place in scope 0 at src/main.rs:7:28: 7:38 +;; let _2: fn(&&(), &T) -> &T; // in scope 0 at src/main.rs:8:9: 8:10 +;; let mut _3: fn(&&(), &T) -> &T; // in scope 0 at src/main.rs:9:5: 9:6 +;; let mut _4: &&(); // in scope 0 at src/main.rs:9:7: 9:11 +;; let _5: &&&(); // in scope 0 at src/main.rs:9:7: 9:11 +;; let mut _6: &T; // in scope 0 at src/main.rs:9:13: 9:14 +;; scope 1 { +;; debug f => _2; // in scope 1 at src/main.rs:8:9: 8:10 +;; } +;; +;; bb0: { +;; _2 = foo:: as for<'a, 'b> fn(&'a &'b (), &'b T) -> &'a T (Pointer(ReifyFnPointer)); // scope 0 at src/main.rs:8:41: 8:44 +;; // mir::Constant +;; // + span: src/main.rs:8:41: 8:44 +;; // + literal: Const { ty: for<'a, 'b> fn(&'a &'b (), &'b T) -> &'a T {foo::}, val: Value(Scalar()) } +;; _3 = _2; // scope 1 at src/main.rs:9:5: 9:6 +;; _5 = const {alloc1: &&&()}; // scope 1 at src/main.rs:9:7: 9:11 +;; // mir::Constant +;; // + span: src/main.rs:9:7: 9:11 +;; // + literal: Const { ty: &&&(), val: Value(Scalar(alloc1)) } +;; _4 = (*_5); // scope 1 at src/main.rs:9:7: 9:11 +;; _6 = _1; // scope 1 at src/main.rs:9:13: 9:14 +;; _0 = move _3(move _4, move _6) -> bb1; // scope 1 at src/main.rs:9:5: 9:15 +;; } +;; +;; bb1: { +;; return; // scope 0 at src/main.rs:10:2: 10:2 +;; } +;; } +;; +;; fn main() { +;; let value = { +;; let data = 22; +;; bad(&data) +;; }; +;; let _ = *value; +;; } +;; MIR { +;; let mut _0: (); // return place in scope 0 at src/main.rs:12:11: 12:11 +;; let _1: &i32; // in scope 0 at src/main.rs:13:9: 13:14 +;; let _2: i32; // in scope 0 at src/main.rs:14:13: 14:17 +;; let mut _3: &i32; // in scope 0 at src/main.rs:15:13: 15:18 +;; let _4: &i32; // in scope 0 at src/main.rs:15:13: 15:18 +;; scope 1 { +;; debug value => _1; // in scope 1 at src/main.rs:13:9: 13:14 +;; scope 3 { +;; } +;; } +;; scope 2 { +;; debug data => _2; // in scope 2 at src/main.rs:14:13: 14:17 +;; } +;; +;; bb0: { +;; _2 = const 22_i32; // scope 0 at src/main.rs:14:20: 14:22 +;; _4 = &_2; // scope 2 at src/main.rs:15:13: 15:18 +;; _3 = _4; // scope 2 at src/main.rs:15:13: 15:18 +;; _1 = bad::(move _3) -> bb1; // scope 2 at src/main.rs:15:9: 15:19 +;; // mir::Constant +;; // + span: src/main.rs:15:9: 15:12 +;; // + literal: Const { ty: for<'a> fn(&'a i32) -> &'static i32 {bad::}, val: Value(Scalar()) } +;; } +;; +;; bb1: { +;; return; // scope 0 at src/main.rs:18:2: 18:2 +;; } +;; } +;; ``` From dd5d7f3b7fe131fb3dea5fdf3613d52605331b03 Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Thu, 2 Jun 2022 06:06:58 -0400 Subject: [PATCH 03/12] all trusted fn bodies --- src/mir/all-check.rkt | 10 +++++++--- src/mir/grammar.rkt | 5 ++++- 2 files changed, 11 insertions(+), 4 deletions(-) diff --git a/src/mir/all-check.rkt b/src/mir/all-check.rkt index a083d7ed..90e2c504 100644 --- a/src/mir/all-check.rkt +++ b/src/mir/all-check.rkt @@ -109,8 +109,8 @@ (where/error Env_0 (env-for-decl-program DeclProgram)) ;; environment 1: instantiate the generic arguments as universal placeholders and tag - (where/error (Env_1 (Tys -> Ty where WhereClauses (∃ KindedVarIds_1 LocalsAndBlocks_1)) VarIds_∀) - (instantiate-quantified Env_0 MirBodySig)) + (where (Env_1 (Tys -> Ty where WhereClauses (∃ KindedVarIds_1 LocalsAndBlocks_1)) VarIds_∀) + (instantiate-quantified Env_0 MirBodySig)) ;; environment 2: instantiate the existential inference variables within the mir body (lifetimes, typically) (where/error (Env_2 LocalsAndBlocks_2 VarIds_∃) @@ -125,7 +125,11 @@ (unsafe-check Γ) (type-check-goal/Γ Γ GoalAtLocations) (borrow-check Γ GoalAtLocations) - ---------------------------------------- + ---------------------------------------- "mir-fn-body" (✅-FnBody DeclProgram MirBodySig) ] + + [---------------------------------------- "trusted-fn-body" + (✅-FnBody DeclProgram (∀ _ (_ -> _ where _ trusted-fn-body))) + ] ) diff --git a/src/mir/grammar.rkt b/src/mir/grammar.rkt index 43b91d73..597814cf 100644 --- a/src/mir/grammar.rkt +++ b/src/mir/grammar.rkt @@ -4,7 +4,10 @@ (define-extended-language formality-mir formality-decl ; Overridden from formality-decl - (FnBody ::= (∃ KindedVarIds LocalsAndBlocks)) + (FnBody ::= + (∃ KindedVarIds LocalsAndBlocks) + trusted-fn-body ; a special tag that is always considered to pass the type check + ) (LocalsAndBlocks ::= (LocalDecls BasicBlockDecls)) ;; A `LocalDecl` indicates the type of a local variable. From 5af11521832409accd6feffd6d4fc50c21441f43 Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Thu, 2 Jun 2022 06:32:36 -0400 Subject: [PATCH 04/12] introduce user-ty notation --- src/decl/decl-to-clause.rkt | 7 +- src/decl/grammar.rkt | 2 - src/decl/test/basic-consts.rkt | 1 + src/decl/test/basic-statics.rkt | 1 + src/decl/test/basic.rkt | 5 +- src/decl/test/coinductive/magic-issue-xxx.rkt | 12 ++-- src/decl/test/copy.rkt | 3 +- src/decl/test/drop.rkt | 5 +- src/decl/test/multi-crate.rkt | 3 +- src/logic/cosld-solve/filter.rkt | 6 +- src/logic/elaborate.rkt | 16 ++--- src/logic/test/unify-test.rkt | 8 +-- src/mir/test/basic.rkt | 9 +-- src/mir/test/issue-25860.rkt | 9 +-- src/mir/type-of.rkt | 2 +- src/ty/could-match.rkt | 7 +- src/ty/grammar.rkt | 64 ++++++------------- src/ty/test/test-alias-outlives.rkt | 9 +-- src/ty/test/test-alias-subtyping.rkt | 27 ++++---- src/ty/test/test-extrude.rkt | 1 + src/ty/test/test-gats.rkt | 8 ++- src/ty/test/test-outlives.rkt | 10 ++- src/ty/test/test-scheme.rkt | 5 +- src/ty/test/test-subtyping.rkt | 27 ++++---- src/ty/user-ty.rkt | 59 +++++++++++++++++ 25 files changed, 179 insertions(+), 127 deletions(-) create mode 100644 src/ty/user-ty.rkt diff --git a/src/decl/decl-to-clause.rkt b/src/decl/decl-to-clause.rkt index bf64f9cf..e0200c46 100644 --- a/src/decl/decl-to-clause.rkt +++ b/src/decl/decl-to-clause.rkt @@ -6,6 +6,7 @@ "../ty/relate.rkt" "../ty/could-match.rkt" "../ty/where-clauses.rkt" + "../ty/user-ty.rkt" "../ty/hook.rkt") (provide env-for-crate-decl env-for-crate-decls @@ -331,9 +332,9 @@ default-rules : () -> (Clauses Invariants) ((default-rules ()) - (((well-formed (type (scalar-ty i32))) - (well-formed (type (scalar-ty u32))) - (well-formed (type unit-ty)) + (((well-formed (type (user-ty i32))) + (well-formed (type (user-ty u32))) + (well-formed (type (user-ty ()))) ) ()) ) diff --git a/src/decl/grammar.rkt b/src/decl/grammar.rkt index caeaed51..c7847d42 100644 --- a/src/decl/grammar.rkt +++ b/src/decl/grammar.rkt @@ -4,8 +4,6 @@ crate-decl-with-id trait-decl-id item-with-id - scalar-ty - unit-ty crate-decls ) diff --git a/src/decl/test/basic-consts.rkt b/src/decl/test/basic-consts.rkt index 1847e984..dca1cddb 100644 --- a/src/decl/test/basic-consts.rkt +++ b/src/decl/test/basic-consts.rkt @@ -2,6 +2,7 @@ (require redex/reduction-semantics "../grammar.rkt" "../prove.rkt" + "../../ty/user-ty.rkt" "../../util.rkt") (module+ test diff --git a/src/decl/test/basic-statics.rkt b/src/decl/test/basic-statics.rkt index 1e083161..cc7bb0ce 100644 --- a/src/decl/test/basic-statics.rkt +++ b/src/decl/test/basic-statics.rkt @@ -3,6 +3,7 @@ "../grammar.rkt" "../prove.rkt" "../../util.rkt" + "../../ty/user-ty.rkt" "libcore.rkt") (module+ test diff --git a/src/decl/test/basic.rkt b/src/decl/test/basic.rkt index 21f80b05..4a0f4510 100644 --- a/src/decl/test/basic.rkt +++ b/src/decl/test/basic.rkt @@ -3,6 +3,7 @@ "../decl-to-clause.rkt" "../grammar.rkt" "../prove.rkt" + "../../ty/user-ty.rkt" "../../util.rkt") (module+ test @@ -14,7 +15,7 @@ formality-decl ((TraitDecl (term (Debug (trait ((type Self)) () ())))) - (TraitImplDecl (term (impl () (Debug ((scalar-ty i32))) () ()))) + (TraitImplDecl (term (impl () (Debug ((user-ty i32))) () ()))) (CrateDecl (term (TheCrate (crate (TraitDecl TraitImplDecl))))) (Env (term (env-for-crate-decl CrateDecl))) ) @@ -22,6 +23,6 @@ (traced '() (decl:test-can-prove Env - (is-implemented (Debug ((scalar-ty i32)))))) + (is-implemented (Debug ((user-ty i32)))))) ) ) diff --git a/src/decl/test/coinductive/magic-issue-xxx.rkt b/src/decl/test/coinductive/magic-issue-xxx.rkt index 9933946b..42048798 100644 --- a/src/decl/test/coinductive/magic-issue-xxx.rkt +++ b/src/decl/test/coinductive/magic-issue-xxx.rkt @@ -4,7 +4,9 @@ "../../decl-ok.rkt" "../../grammar.rkt" "../../prove.rkt" - "../../../util.rkt") + "../../../ty/user-ty.rkt" + "../../../util.rkt" + ) (module+ test (; Magic trait, implemented in terms of itself, that extends Copy @@ -12,7 +14,7 @@ formality-decl ((; struct Foo { counter: i32 } - AdtDecl_Foo (term (Foo (struct () () ((struct-variant ((counter (scalar-ty i32))))))))) + AdtDecl_Foo (term (Foo (struct () () ((struct-variant ((counter (user-ty i32))))))))) (; reference to `Foo` Ty_Foo (term (rigid-ty Foo ()))) @@ -59,7 +61,7 @@ formality-decl ((; struct Foo { counter: i32 } - AdtDecl_Foo (term (Foo (struct () () ((struct-variant ((counter (scalar-ty i32))))))))) + AdtDecl_Foo (term (Foo (struct () () ((struct-variant ((counter (user-ty i32))))))))) (; reference to `Foo` Ty_Foo (term (rigid-ty Foo ()))) @@ -105,13 +107,13 @@ formality-decl ((; struct Foo { counter: i32 } - AdtDecl_Foo (term (Foo (struct () () ((struct-variant ((counter (scalar-ty i32))))))))) + AdtDecl_Foo (term (Foo (struct () () ((struct-variant ((counter (user-ty i32))))))))) (; reference to `Foo` Ty_Foo (term (rigid-ty Foo ()))) (; struct Bar { counter: i32 } - AdtDecl_Foo (term (Foo (struct () () ((struct-variant ((counter (scalar-ty i32))))))))) + AdtDecl_Foo (term (Foo (struct () () ((struct-variant ((counter (user-ty i32))))))))) (; reference to `Bar` Ty_Bar (term (rigid-ty Bar ()))) diff --git a/src/decl/test/copy.rkt b/src/decl/test/copy.rkt index 410bf619..0f147de6 100644 --- a/src/decl/test/copy.rkt +++ b/src/decl/test/copy.rkt @@ -4,6 +4,7 @@ "../decl-ok.rkt" "../grammar.rkt" "../prove.rkt" + "../../ty/user-ty.rkt" "../../util.rkt") ;; Test the special rules for impls of the Copy trait. @@ -18,7 +19,7 @@ TraitDecl_Copy (term (rust:Copy (trait ((type Self)) () ())))) (; impl rust:Copy for i32 { } - TraitImplDecl (term (impl () (rust:Copy ((scalar-ty i32))) () ()))) + TraitImplDecl (term (impl () (rust:Copy ((user-ty i32))) () ()))) (; the crate has the struct, the trait, and the impl CrateDecl (term (TheCrate (crate (TraitDecl_Copy diff --git a/src/decl/test/drop.rkt b/src/decl/test/drop.rkt index 04e0ae43..38ff82fb 100644 --- a/src/decl/test/drop.rkt +++ b/src/decl/test/drop.rkt @@ -4,6 +4,7 @@ "../decl-ok.rkt" "../grammar.rkt" "../prove.rkt" + "../../ty/user-ty.rkt" "../../util.rkt") ;; Test the special rules for impls of the Drop trait. @@ -18,7 +19,7 @@ TraitDecl_Drop (term (rust:Drop (trait ((type Self)) () ())))) (; impl rust:Drop for i32 { } - TraitImplDecl (term (impl () (rust:Drop ((scalar-ty i32))) () ()))) + TraitImplDecl (term (impl () (rust:Drop ((user-ty i32))) () ()))) (; the crate has the struct, the trait, and the impl CrateDecl (term (TheCrate (crate (TraitDecl_Drop @@ -50,7 +51,7 @@ TraitDecl_Drop (term (rust:Drop (trait ((type Self)) () ())))) (; impl rust:Drop for Foo { } //~ ERROR - TraitImplDecl (term (impl () (rust:Drop ((rigid-ty Foo ((scalar-ty i32))))) () ()))) + TraitImplDecl (term (impl () (rust:Drop ((rigid-ty Foo ((user-ty i32))))) () ()))) (; the crate has the struct, the trait, and the impl CrateDecl (term (TheCrate (crate (AdtDecl_Foo diff --git a/src/decl/test/multi-crate.rkt b/src/decl/test/multi-crate.rkt index 28fc4ccf..d83e0ccb 100644 --- a/src/decl/test/multi-crate.rkt +++ b/src/decl/test/multi-crate.rkt @@ -4,6 +4,7 @@ "../decl-ok.rkt" "../grammar.rkt" "../prove.rkt" + "../../ty/user-ty.rkt" "../../util.rkt") (module+ test @@ -18,7 +19,7 @@ CrateDecl_A (redex-let* formality-decl ((TraitDecl (term (Debug (trait ((type Self)) () ())))) - (TraitImplDecl (term (impl () (Debug ((scalar-ty i32))) () ()))) + (TraitImplDecl (term (impl () (Debug ((user-ty i32))) () ()))) ) (term (CrateA (crate (TraitDecl TraitImplDecl)))))) diff --git a/src/logic/cosld-solve/filter.rkt b/src/logic/cosld-solve/filter.rkt index 853e37a9..6af054e2 100644 --- a/src/logic/cosld-solve/filter.rkt +++ b/src/logic/cosld-solve/filter.rkt @@ -65,7 +65,7 @@ (test-equal (term (filter-clauses EmptyEnv Clauses_test - (is-implemented (Debug ((scalar-ty i32)))))) + (is-implemented (Debug ((user-ty i32)))))) (term Clauses_test)) ; The "filtering" function we use at the logic level is ... not very precise. @@ -74,13 +74,13 @@ (test-equal (term (filter-clauses EmptyEnv Clauses_test - (is-implemented (WithDebug ((scalar-ty i32)))))) + (is-implemented (WithDebug ((user-ty i32)))))) (term Clauses_test)) (test-equal (term (filter-clauses EmptyEnv Clauses_test - (has-impl (Debug ((scalar-ty i32)))))) + (has-impl (Debug ((user-ty i32)))))) (term Clauses_test)) ) ) \ No newline at end of file diff --git a/src/logic/elaborate.rkt b/src/logic/elaborate.rkt index dd1475ff..af64f7e4 100644 --- a/src/logic/elaborate.rkt +++ b/src/logic/elaborate.rkt @@ -170,17 +170,17 @@ (traced '() (test-equal - (term (elaborate-hypothesis-one-step Env (is-implemented (Ord ((scalar-ty u32)))))) - (term ((is-implemented (Eq ((scalar-ty u32)))) - (is-implemented (PartialOrd ((scalar-ty u32)))))))) + (term (elaborate-hypothesis-one-step Env (is-implemented (Ord ((user-ty u32)))))) + (term ((is-implemented (Eq ((user-ty u32)))) + (is-implemented (PartialOrd ((user-ty u32)))))))) (traced '() (test-equal - (term (env-hypotheses (elaborate-hypotheses (env-with-hypotheses Env ((is-implemented (Ord ((scalar-ty u32))))))))) - (term ((is-implemented (Ord ((scalar-ty u32)))) - (is-implemented (Eq ((scalar-ty u32)))) - (is-implemented (PartialOrd ((scalar-ty u32)))) - (is-implemented (PartialEq ((scalar-ty u32)))))))) + (term (env-hypotheses (elaborate-hypotheses (env-with-hypotheses Env ((is-implemented (Ord ((user-ty u32))))))))) + (term ((is-implemented (Ord ((user-ty u32)))) + (is-implemented (Eq ((user-ty u32)))) + (is-implemented (PartialOrd ((user-ty u32)))) + (is-implemented (PartialEq ((user-ty u32)))))))) (traced '() (test-alpha-equivalent diff --git a/src/logic/test/unify-test.rkt b/src/logic/test/unify-test.rkt index 017ca107..8670924b 100644 --- a/src/logic/test/unify-test.rkt +++ b/src/logic/test/unify-test.rkt @@ -36,7 +36,7 @@ ; Equating `E` with `Vec` is ok (test-equal - (term (occurs-check Env_1 E (rigid-ty Vec ((scalar-ty i32))))) + (term (occurs-check Env_1 E (rigid-ty Vec ((user-ty i32))))) (term Env_1)) ; Equating `E` with `V` is not possible, @@ -148,16 +148,16 @@ ((; assume that `X: Debug` (note that `X` is an existential variable) Env_3 (term (env-with-hypotheses Env_2 ((is-implemented (Debug (Term_X))))))) (; constrain `X = i32` to yield new substitution - Env_out (term (unify Env_3 ((Term_X (scalar-ty i32))))))) + Env_out (term (unify Env_3 ((Term_X (user-ty i32))))))) ; concluded that `X = i32` - (test-equal (term (apply-substitution-from-env Env_out Term_X)) (term (scalar-ty i32))) + (test-equal (term (apply-substitution-from-env Env_out Term_X)) (term (user-ty i32))) ; starts out as `X: Debug` (test-equal (term (env-hypotheses Env_3)) (term ((is-implemented (Debug (Term_X)))))) ; changes to `i32: Debug` now that we know `X = i32` - (test-equal (term (env-hypotheses Env_out)) (term ((is-implemented (Debug ((scalar-ty i32))))))) + (test-equal (term (env-hypotheses Env_out)) (term ((is-implemented (Debug ((user-ty i32))))))) ) ) ) \ No newline at end of file diff --git a/src/mir/test/basic.rkt b/src/mir/test/basic.rkt index 88896e61..57a13a21 100644 --- a/src/mir/test/basic.rkt +++ b/src/mir/test/basic.rkt @@ -3,6 +3,7 @@ "../all-check.rkt" "../grammar.rkt" "../../ty/grammar.rkt" + "../../ty/user-ty.rkt" "../../util.rkt" ) @@ -15,8 +16,8 @@ (redex-let* formality-mir - ((LocalDecls_foo (term ((_0 (scalar-ty i32) mut) - (_1 (scalar-ty i32) ()) + ((LocalDecls_foo (term ((_0 (user-ty i32) mut) + (_1 (user-ty i32) ()) ))) (BasicBlockData_bb0 (term (((_0 = (use (copy _1)))) return))) (BasicBlockDecl_bb0 (term (bb0 BasicBlockData_bb0))) @@ -37,8 +38,8 @@ ) ))) (FnDecl_foo (term (foo (fn-decl () - ((scalar-ty i32) (scalar-ty i32)) - (scalar-ty i32) + ((user-ty i32) (user-ty i32)) + (user-ty i32) () FnBody_foo)))) (CrateDecl_the-crate (term (the-crate (crate (FnDecl_foo))))) diff --git a/src/mir/test/issue-25860.rkt b/src/mir/test/issue-25860.rkt index 3db47b13..07f94e6a 100644 --- a/src/mir/test/issue-25860.rkt +++ b/src/mir/test/issue-25860.rkt @@ -3,6 +3,7 @@ "../all-check.rkt" "../grammar.rkt" "../../ty/grammar.rkt" + "../../ty/user-ty.rkt" "../../util.rkt" ) @@ -49,7 +50,7 @@ (StaticDecl_UNIT (term (UNIT (static () ; generics () ; where-clauses - (& static (& static unit-ty)) ; type + (user-ty (& static (& static ()))) ; type (∃ ((lifetime L0) (lifetime L1) @@ -57,9 +58,9 @@ (lifetime L3) (lifetime L4) ) - ([(_0 (& L0 (& L1 unit-ty)) mut) - (_1 (& L2 unit-ty) mut) - (_2 unit-ty mut) + ([(_0 (user-ty (& L0 (& L1 ()))) mut) + (_1 (user-ty (& L2 ())) mut) + (_2 (user-ty ()) mut) ] [(bb0 {(noop (_1 = (ref L3 () _2)) diff --git a/src/mir/type-of.rkt b/src/mir/type-of.rkt index a091f47e..1b57277c 100644 --- a/src/mir/type-of.rkt +++ b/src/mir/type-of.rkt @@ -125,7 +125,7 @@ ; ; FIXME ------------------------------------------ - (type-of/Operand Γ (const _) (scalar-ty i32)) + (type-of/Operand Γ (const _) (user-ty i32)) ] ) diff --git a/src/ty/could-match.rkt b/src/ty/could-match.rkt index 797a4f03..0a3c9778 100644 --- a/src/ty/could-match.rkt +++ b/src/ty/could-match.rkt @@ -2,6 +2,7 @@ (require redex/reduction-semantics "grammar.rkt" "predicate.rkt" + "user-ty.rkt" ) (provide ty:predicates-could-match ) @@ -26,17 +27,17 @@ (module+ test (test-equal (term (ty:predicates-could-match (is-implemented (Debug (T))) - (is-implemented (Debug ((scalar-ty i32)))))) + (is-implemented (Debug ((user-ty i32)))))) (term #t)) (test-equal (term (ty:predicates-could-match (is-implemented (Debug (T))) - (is-implemented (WithDebug ((scalar-ty i32)))))) + (is-implemented (WithDebug ((user-ty i32)))))) (term #f)) (test-equal (term (ty:predicates-could-match (is-implemented (Debug (T))) - (has-impl (WithDebug ((scalar-ty i32)))))) + (has-impl (WithDebug ((user-ty i32)))))) (term #f)) ) diff --git a/src/ty/grammar.rkt b/src/ty/grammar.rkt index edb555c7..fcea2301 100644 --- a/src/ty/grammar.rkt +++ b/src/ty/grammar.rkt @@ -70,6 +70,26 @@ (AliasTy == Ty) ; ::Item == u32 ) + ;; UserTy -- rust user-facing types + ;; + ;; these match the grammar Rust user's expect. They are a notational + ;; convenience. Use the `(user-ty UserTy)` function to convert + ;; to the internal `Ty` types. + (UserTys ::= (UserTy ...)) + (UserTy ::= + (for KindedVarIds UserTy) + () + (tuple UserTy ...) + (& Lt UserTy) + (&mut Lt UserTy) + ScalarId + (AdtId UserParameter ...) + (fn UserTys -> UserTy) + (@ AliasName UserParameter ...) + VarId + ) + (UserParameter ::= UserTy Lt) + ;; Ty -- Rust types ;; ;; Most Rust types are some variation of `RigidTy`, @@ -183,48 +203,6 @@ (GenericParameter ::= (VarId KindAndVariance)) (KindAndVariance ::= (ParameterKind Variance)) (Variance := - + =) - ) - -(define-term - unit-ty - (rigid-ty (tuple 0) ()) - ) - -(define-metafunction formality-ty - scalar-ty : ScalarId -> Ty - - ((scalar-ty ScalarId) (rigid-ty ScalarId ())) - ) - -(define-metafunction formality-ty - & : Lt Ty -> Ty - - [(& Lt Ty) (rigid-ty (ref ()) (Lt Ty))] - ) - -(define-metafunction formality-ty - &mut : Lt Ty -> Ty - - [(&mut Lt Ty) (rigid-ty (ref mut) (Lt Ty))] - ) - -(define-metafunction formality-ty - box : Ty -> Ty - - [(box Ty) (rigid-ty Box (Lt Ty))] - ) - -(define-metafunction formality-ty - vec : Ty -> Ty - - [(vec Ty) (rigid-ty Vec (Lt Ty))] - ) - -(define-metafunction formality-ty - fn : Tys Ty -> Ty - [(fn (Ty_arg ...) Ty_ret) - (rigid-ty (fn-ptr "Rust" number) (Ty_arg ... Ty_ret)) - (where/error number ,(length (term (Ty_arg ...)))) - ] + (for ((ParameterKind VarId) ...) any #:refers-to (shadow VarId ...)) ) diff --git a/src/ty/test/test-alias-outlives.rkt b/src/ty/test/test-alias-outlives.rkt index 9d7f6c0d..54edb508 100644 --- a/src/ty/test/test-alias-outlives.rkt +++ b/src/ty/test/test-alias-outlives.rkt @@ -3,15 +3,16 @@ "hook.rkt" "../grammar.rkt" "../../util.rkt" + "../user-ty.rkt" ) (module+ test (define-metafunction formality-ty ;; convenience for testing: write `(item T)` to reference the alias type `Item` - item : Ty -> AliasTy + item : UserTy -> AliasTy - [(item Ty) (alias-ty Item (Ty))] + [(item UserTy) (alias-ty Item ((user-ty UserTy)))] ) (redex-let* @@ -23,7 +24,7 @@ (; Define a trait `AlwaysImpl` that is implemented for all types ∀ ((type T)) (is-implemented (AlwaysImpl (T)))) (; normalizes-to `Item>` to `T` - ∀ ((type T)) (normalizes-to (item (vec T)) T)) + ∀ ((type T)) (normalizes-to (item (Vec T)) T)) ) () () @@ -38,7 +39,7 @@ Env () () - ((item (scalar-ty i32)) + ((item i32) -outlives- static ) diff --git a/src/ty/test/test-alias-subtyping.rkt b/src/ty/test/test-alias-subtyping.rkt index 2c3d1244..c00ca952 100644 --- a/src/ty/test/test-alias-subtyping.rkt +++ b/src/ty/test/test-alias-subtyping.rkt @@ -3,6 +3,7 @@ "hook.rkt" "../grammar.rkt" "../scheme.rkt" + "../user-ty.rkt" "../../util.rkt" "../../logic/instantiate.rkt" ) @@ -11,9 +12,9 @@ (define-metafunction formality-ty ;; convenience for testing: write `(item T)` to reference the alias type `Item` - item : Ty -> AliasTy + item : UserTy -> AliasTy - [(item Ty) (alias-ty Item (Ty))] + [(item UserTy) (alias-ty Item ((user-ty UserTy)))] ) (redex-let* @@ -25,7 +26,7 @@ (; Define a trait `AlwaysImpl` that is implemented for all types ∀ ((type T)) (is-implemented (AlwaysImpl (T)))) (; normalizes-to `Item>` to `T` - ∀ ((type T)) (normalizes-to (item (vec T)) T)) + ∀ ((type T)) (normalizes-to (item (Vec T)) T)) ) () () @@ -40,9 +41,9 @@ Env () () - ((item (vec (scalar-ty i32))) + ((item (Vec i32)) <= - (scalar-ty i32) + (user-ty i32) ) ) ) @@ -75,8 +76,8 @@ (term (ty:prove-scheme Env ((∀ ((type T) (type U)))) - (((item T) == (scalar-ty i32)) - ((item U) == (scalar-ty i32))) + (((item T) == (user-ty i32)) + ((item U) == (user-ty i32))) ((item T) <= (item U) @@ -95,9 +96,9 @@ Env ((∀ ((lifetime A) (lifetime B)))) ((A : B)) - ((item (& A unit-ty)) + ((item (& A ())) <= - (item (& B unit-ty)) + (item (& B ())) ) ) ) @@ -115,9 +116,9 @@ ((A : B) (B : A) ) - ((item (& A unit-ty)) + ((item (& A ())) <= - (item (& B unit-ty)) + (item (& B ())) ) ) ) @@ -133,9 +134,9 @@ Env ((∀ ((lifetime A) (lifetime B)))) ((A : B)) - ((item (vec (& A unit-ty))) + ((item (Vec (& A ()))) <= - (item (vec (& B unit-ty))) + (item (Vec (& B ()))) ) ) ) diff --git a/src/ty/test/test-extrude.rkt b/src/ty/test/test-extrude.rkt index d542a0b2..b3f23536 100644 --- a/src/ty/test/test-extrude.rkt +++ b/src/ty/test/test-extrude.rkt @@ -4,6 +4,7 @@ "../grammar.rkt" "../extrude.rkt" "../inequalities.rkt" + "../user-ty.rkt" "../../logic/instantiate.rkt" "../../logic/env.rkt" "../../util.rkt" diff --git a/src/ty/test/test-gats.rkt b/src/ty/test/test-gats.rkt index df38a793..09eb64ce 100644 --- a/src/ty/test/test-gats.rkt +++ b/src/ty/test/test-gats.rkt @@ -3,6 +3,7 @@ "hook.rkt" "../grammar.rkt" "../scheme.rkt" + "../user-ty.rkt" "../../util.rkt" "../../logic/instantiate.rkt" ) @@ -16,9 +17,10 @@ ((; Just ignore well-formed rules, not interesting for testing subtyping ∀ ((type T)) (well-formed (type T))) (; Define a trait `Iterable` that is implemented for Vec - ∀ ((type T)) (is-implemented (Iterable ((vec T))))) + ∀ ((type T)) (is-implemented (Iterable ((user-ty (Vec T)))))) (; normalizes-to `Item, A>` to `(rigid-ty (ref ()) (A T))` - ∀ ((type T) (lifetime A)) (normalizes-to (alias-ty Item ((vec T) A)) (& A T))) + ∀ ((type T) (lifetime A)) (normalizes-to (user-ty (@ Item (Vec T) A)) + (user-ty (& A T)))) ) () () @@ -33,7 +35,7 @@ Env ((∀ ((type T) (lifetime A))) (∃ ((type U)))) () - (normalizes-to (alias-ty Item ((vec T) A)) (rigid-ty (ref ()) (A T))) + (normalizes-to (user-ty (@ Item (Vec T) A)) (user-ty (& A T))) ) ) )) diff --git a/src/ty/test/test-outlives.rkt b/src/ty/test/test-outlives.rkt index c01e6e18..43180852 100644 --- a/src/ty/test/test-outlives.rkt +++ b/src/ty/test/test-outlives.rkt @@ -3,6 +3,7 @@ "hook.rkt" "../grammar.rkt" "../scheme.rkt" + "../user-ty.rkt" "../../util.rkt" "../../logic/instantiate.rkt" ) @@ -64,7 +65,7 @@ ((∀ ((lifetime A)) (rigid-ty - (fn-ptr "" 1) + (fn-ptr _ 1) ((rigid-ty (ref ()) (A (rigid-ty u32 ()))) (rigid-ty (tuple 0) ())))) -outlives- @@ -74,7 +75,7 @@ Env () () - ((∀ ((lifetime A)) (rigid-ty (fn-ptr "" 1) ((rigid-ty (ref ()) (A (scalar-ty u32))) unit-ty))) + ((user-ty (for ((lifetime A)) (fn ((& A u32)) -> ()))) -outlives- static) )) @@ -91,10 +92,7 @@ (redex-let* formality-ty - [(Ty_fn (term (∀ ((lifetime A)) - (fn - ((& A (& B (scalar-ty i32)))) - unit-ty)))) + [(Ty_fn (term (user-ty (for ((lifetime A)) (fn ((& A (& B i32))) -> ()))))) (Goal (term (Ty_fn -outlives- B))) ] (term (ty:prove-scheme diff --git a/src/ty/test/test-scheme.rkt b/src/ty/test/test-scheme.rkt index b194ff87..eb92d7b3 100644 --- a/src/ty/test/test-scheme.rkt +++ b/src/ty/test/test-scheme.rkt @@ -4,6 +4,7 @@ "../grammar.rkt" "../scheme.rkt" "../inequalities.rkt" + "../user-ty.rkt" "../../logic/substitution.rkt" "../../logic/instantiate.rkt" ) @@ -14,8 +15,8 @@ [((Env_1 () (Ty_T)) (term (instantiate-quantified EmptyEnv (∀ ((type T)) ())))) ((Env_2 () (Ty_A Ty_B)) (term (instantiate-quantified Env_1 (∃ ((type A) (type B)) ())))) ((Env_3 () (Lt_I Lt_J Lt_K Lt_L)) (term (instantiate-quantified Env_2 (∃ ((lifetime I) (lifetime J) (lifetime K) (lifetime L)) ())))) - (Env_4 (term (env-with-var-mapped-to Env_3 Ty_A (rigid-ty (ref ()) (Lt_I (scalar-ty i32)))))) - (Env_5 (term (env-with-var-mapped-to Env_4 Ty_B (rigid-ty (ref ()) (Lt_J (scalar-ty i32)))))) + (Env_4 (term (env-with-var-mapped-to Env_3 Ty_A (rigid-ty (ref ()) (Lt_I (user-ty i32)))))) + (Env_5 (term (env-with-var-mapped-to Env_4 Ty_B (rigid-ty (ref ()) (Lt_J (user-ty i32)))))) (Env_6 (term (env-with-var-related-to-parameter Env_5 Lt_I <= Lt_K))) (Env_7 (term (env-with-var-related-to-parameter Env_6 Lt_J <= Lt_K))) (Env_8 (term (env-with-var-related-to-parameter Env_7 Lt_K <= Lt_L))) diff --git a/src/ty/test/test-subtyping.rkt b/src/ty/test/test-subtyping.rkt index b91f7537..0e47c82d 100644 --- a/src/ty/test/test-subtyping.rkt +++ b/src/ty/test/test-subtyping.rkt @@ -2,6 +2,7 @@ (require redex/reduction-semantics "hook.rkt" "../grammar.rkt" + "../user-ty.rkt" "../scheme.rkt" "../../util.rkt" "../../logic/instantiate.rkt" @@ -23,19 +24,19 @@ ) (traced '() - (ty:test-can-prove Env ((∀ ((type T)) T) <= (scalar-ty u32))) + (ty:test-can-prove Env ((∀ ((type T)) T) <= (user-ty u32))) ) (traced '() - (ty:test-can-prove Env ((scalar-ty u32) >= (∀ ((type T)) T))) + (ty:test-can-prove Env ((user-ty u32) >= (∀ ((type T)) T))) ) (traced '() - (ty:test-cannot-prove Env ((scalar-ty u32) <= (∀ ((type T)) T))) + (ty:test-cannot-prove Env ((user-ty u32) <= (∀ ((type T)) T))) ) (traced '() - (ty:test-cannot-prove Env ((∀ ((type T)) T) >= (scalar-ty u32))) + (ty:test-cannot-prove Env ((∀ ((type T)) T) >= (user-ty u32))) ) ; Cannot have an implication on the subtype side that doesn't appear on the supertype side @@ -118,7 +119,7 @@ ((∀ ((type T))) (∃ ((type U) (lifetime A)))) () - (U <= (& A T)) + (U <= (user-ty (& A T))) )) ) ) @@ -132,9 +133,9 @@ ((∀ ((type T))) ) () - ((rigid-ty (fn-ptr "" 1) (T unit-ty)) ; fn(T) + ((user-ty (fn (T) -> ())) <= - (∀ ((type T)) (fn (T) unit-ty)) ; forall fn(T) + (user-ty (for ((type T)) (fn (T) -> ()))) )))) (traced '() @@ -273,10 +274,10 @@ () ((; fn foo<'a, 'b, T>(_: &'a &'b (), v: &'b T) -> &'a T { v } ∀ ((lifetime A) (lifetime B)) - (fn ((& A (& B unit-ty)) (& B T)) (& A T))) + (user-ty (fn ((& A (& B ())) (& B T)) -> (& A T)))) <= (; fn(&'static &'x (), &'x T) -> &'static T - fn ((& static (& X unit-ty)) (& X T)) (& static T)) + user-ty (fn ((& static (& X ())) (& X T)) -> (& static T))) ) ) ) @@ -296,10 +297,10 @@ ((; fn foo<'a, 'b, T>(_: &'a &'b (), v: &'b T) -> &'a T { v } ∀ ((lifetime A) (lifetime B)) (implies ((B : A)) ; implied bound! - (fn ((& A (& B unit-ty)) (& B T)) (& A T)))) + (user-ty (fn ((& A (& B ())) (& B T)) -> (& A T))))) <= (; fn(&'static &'x (), &'x T) -> &'static T - fn ((& static (& X unit-ty)) (& X T)) (& static T)) + user-ty (fn ((& static (& X ())) (& X T)) -> (& static T))) ) ) ) @@ -318,10 +319,10 @@ ((; fn foo<'a, 'b, T>(_: &'a &'b (), v: &'b T) -> &'a T { v } ∀ ((lifetime A) (lifetime B)) (implies ((B : A)) ; implied bound! - (fn ((& A (& B unit-ty)) (& B T)) (& A T)))) + (user-ty (fn ((& A (& B ())) (& B T)) -> (& A T))))) <= (; fn(&'x &'static (), &'static T) -> &'x T - fn ((& X (& static unit-ty)) (& static T)) (& X T)) + user-ty (fn ((& X (& static ())) (& static T)) -> (& X T))) ) ) ) diff --git a/src/ty/user-ty.rkt b/src/ty/user-ty.rkt new file mode 100644 index 00000000..78a86166 --- /dev/null +++ b/src/ty/user-ty.rkt @@ -0,0 +1,59 @@ +#lang racket +(require redex/reduction-semantics + "grammar.rkt" + "predicate.rkt" + ) +(provide user-ty + ) + +(define-metafunction formality-ty + user-ty : UserTy -> Ty + + [(user-ty ()) + (rigid-ty (tuple 0) ()) + ] + + [(user-ty (tuple UserTy ...)) + (rigid-ty (tuple number_arity) ((user-ty UserTy) ...)) + (where/error number_arity ,(length (term (UserTy ...)))) + ] + + [(user-ty (& Lt UserTy)) + (rigid-ty (ref ()) (Lt (user-ty UserTy))) + ] + + [(user-ty (&mut Lt UserTy)) + (rigid-ty (ref mut) (Lt (user-ty UserTy))) + ] + + [(user-ty ScalarId) + (rigid-ty ScalarId ()) + ] + + [(user-ty (AdtId UserParameter ...)) + (rigid-ty AdtId ((user-parameter UserParameter) ...)) + ] + + [(user-ty (@ AliasName UserParameter ...)) + (alias-ty AliasName ((user-parameter UserParameter) ...)) + ] + + [(user-ty (fn (UserTy_arg ...) -> UserTy_ret)) + (rigid-ty (fn-ptr "Rust" number_args) ((user-ty UserTy_arg) ... (user-ty UserTy_ret))) + (where/error number_args ,(length (term (UserTy_arg ...)))) + ] + + [(user-ty VarId) VarId] + + [(user-ty (for KindedVarIds UserTy)) + (∀ KindedVarIds (user-ty UserTy)) + ] + ) + +(define-metafunction formality-ty + user-parameter : UserParameter -> Parameter + + [(user-parameter Lt) Lt] + + [(user-parameter UserTy) (user-ty UserTy)] + ) \ No newline at end of file From 1831b9db5e02de9640b0d3bbf6cce0d279ccd6ab Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Thu, 2 Jun 2022 19:41:09 -0400 Subject: [PATCH 05/12] use `fn` not `fn-decl` the latter was needed because `fn` was a metafunction --- src/decl/decl-ok.rkt | 2 +- src/decl/decl-to-clause.rkt | 2 +- src/decl/grammar.rkt | 14 +++++++------- src/decl/test/fns.rkt | 2 +- src/mir/all-check.rkt | 2 +- src/mir/test/basic.rkt | 10 +++++----- 6 files changed, 16 insertions(+), 16 deletions(-) diff --git a/src/decl/decl-ok.rkt b/src/decl/decl-ok.rkt index f4cae714..3de36a3e 100644 --- a/src/decl/decl-ok.rkt +++ b/src/decl/decl-ok.rkt @@ -71,7 +71,7 @@ ;; (well-formed-where-clause-goal (T : Trait_Ord ())))) ;; ;; FIXME: Actually implement that, along with for the other items - (crate-item-ok-goal _ (FnId (fn-decl KindedVarIds Tys_arg Ty_ret (WhereClause ...) FnBody))) + (crate-item-ok-goal _ (FnId (fn KindedVarIds Tys_arg Ty_ret (WhereClause ...) FnBody))) (&& ((well-formed-where-clause-goal WhereClause) ...)) ] diff --git a/src/decl/decl-to-clause.rkt b/src/decl/decl-to-clause.rkt index e0200c46..0c4c8c0d 100644 --- a/src/decl/decl-to-clause.rkt +++ b/src/decl/decl-to-clause.rkt @@ -295,7 +295,7 @@ [;; For a function declared in the crate C, like the following ;; ;; fn foo<'a, T>(&'a T) -> &'a T { ... } - (crate-item-decl-rules CrateDecls CrateId (_ (fn-decl KindedVarIds_fn Tys_arg Ty_ret WhereClauses_fn FnBody))) + (crate-item-decl-rules CrateDecls CrateId (_ (fn KindedVarIds_fn Tys_arg Ty_ret WhereClauses_fn FnBody))) (() () ()) ] diff --git a/src/decl/grammar.rkt b/src/decl/grammar.rkt index c7847d42..1b6b56e8 100644 --- a/src/decl/grammar.rkt +++ b/src/decl/grammar.rkt @@ -69,7 +69,7 @@ ;; ;; fn foo<...>(...) -> ... where ... { body } (FnDecl ::= (FnId FnContents)) - (FnContents ::= (fn-decl KindedVarIds Tys Ty WhereClauses FnBody)) + (FnContents ::= (fn KindedVarIds Tys Ty WhereClauses FnBody)) ;; Identifiers -- these are all equivalent, but we give them fresh names to help ;; clarify their purpose @@ -105,12 +105,12 @@ WhereClauses #:refers-to (shadow VarId ...) Ty #:refers-to (shadow VarId ...) FnBody #:refers-to (shadow VarId ...)) - (fn-decl FnId - ((ParameterKind VarId) ...) - Tys #:refers-to (shadow VarId ...) - Ty #:refers-to (shadow VarId ...) - WhereClauses #:refers-to (shadow VarId ...) - FnBody #:refers-to (shadow VarId ...)) + (fn FnId + ((ParameterKind VarId) ...) + Tys #:refers-to (shadow VarId ...) + Ty #:refers-to (shadow VarId ...) + WhereClauses #:refers-to (shadow VarId ...) + FnBody #:refers-to (shadow VarId ...)) ) (define-metafunction formality-decl diff --git a/src/decl/test/fns.rkt b/src/decl/test/fns.rkt index 9cab14e2..8231a4a8 100644 --- a/src/decl/test/fns.rkt +++ b/src/decl/test/fns.rkt @@ -15,7 +15,7 @@ ;; Test that we can write a function ((; fn foo<'a, T>(&'a T) -> &'a T { ... } - FnDecl_foo (term (foo (fn-decl + FnDecl_foo (term (foo (fn ((lifetime A) (type T)) ((rigid-ty (ref ()) (A (rigid-ty T ())))) (rigid-ty (ref ()) (A (rigid-ty T ()))) diff --git a/src/mir/all-check.rkt b/src/mir/all-check.rkt index 90e2c504..ed67f5ba 100644 --- a/src/mir/all-check.rkt +++ b/src/mir/all-check.rkt @@ -85,7 +85,7 @@ [; function items (prove-crate-item-ok DeclProgram FnDecl) - (where/error (FnId (fn-decl KindedVarIds Tys Ty WhereClauses FnBody)) FnDecl) + (where/error (FnId (fn KindedVarIds Tys Ty WhereClauses FnBody)) FnDecl) (✅-FnBody DeclProgram (∀ KindedVarIds (Tys -> Ty where WhereClauses FnBody))) ---------------------------------------- (✅-CrateItemDecl DeclProgram FnDecl) diff --git a/src/mir/test/basic.rkt b/src/mir/test/basic.rkt index 57a13a21..a3b03889 100644 --- a/src/mir/test/basic.rkt +++ b/src/mir/test/basic.rkt @@ -37,11 +37,11 @@ ) ) ))) - (FnDecl_foo (term (foo (fn-decl () - ((user-ty i32) (user-ty i32)) - (user-ty i32) - () - FnBody_foo)))) + (FnDecl_foo (term (foo (fn () + ((user-ty i32) (user-ty i32)) + (user-ty i32) + () + FnBody_foo)))) (CrateDecl_the-crate (term (the-crate (crate (FnDecl_foo))))) (DeclProgram (term ((CrateDecl_the-crate) the-crate))) ) From 3658c6fcd846e6edb4cab1e045e538bc6d9fcfc5 Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Thu, 2 Jun 2022 19:44:37 -0400 Subject: [PATCH 06/12] adopt helpers tailored to each kind of item --- src/decl/decl-ok.rkt | 4 ++-- src/decl/decl-to-clause.rkt | 4 ++-- src/decl/decl-wf-where-clause.rkt | 2 +- src/decl/grammar.rkt | 25 +++++++++++++++++++------ src/mir/grammar-extended.rkt | 2 +- 5 files changed, 25 insertions(+), 12 deletions(-) diff --git a/src/decl/decl-ok.rkt b/src/decl/decl-ok.rkt index 3de36a3e..6ac7d36f 100644 --- a/src/decl/decl-ok.rkt +++ b/src/decl/decl-ok.rkt @@ -209,7 +209,7 @@ )))) (where (rigid-ty AdtId Parameters) Ty_impl) - (where (AdtKind KindedVarIds_adt WhereClauses_adt _) (item-with-id CrateDecls AdtId)) + (where (AdtKind KindedVarIds_adt WhereClauses_adt _) (adt-with-id CrateDecls AdtId)) (where/error ((ParameterKind_adt VarId_adt) ...) KindedVarIds_adt) (where/error Ty_adt (rigid-ty AdtId (VarId_adt ...))) ] @@ -250,7 +250,7 @@ ))))) (where (rigid-ty AdtId Parameters) Ty_impl) - (where (AdtKind KindedVarIds_adt _ AdtVariants) (item-with-id CrateDecls AdtId)) + (where (AdtKind KindedVarIds_adt _ AdtVariants) (adt-with-id CrateDecls AdtId)) (where/error ((ParameterKind_adt VarId_adt) ...) KindedVarIds_adt) (where/error Ty_adt (rigid-ty AdtId (VarId_adt ...))) (where/error ((VariantId ((FieldId Ty_field) ...)) ...) AdtVariants) diff --git a/src/decl/decl-to-clause.rkt b/src/decl/decl-to-clause.rkt index 0c4c8c0d..9ebcdcee 100644 --- a/src/decl/decl-to-clause.rkt +++ b/src/decl/decl-to-clause.rkt @@ -281,7 +281,7 @@ ((Clause) () ()) (where/error (TraitId (Parameter_trait ...)) TraitRef) - (where/error (trait KindedVarIds_trait _ _) (item-with-id CrateDecls TraitId)) + (where/error (trait KindedVarIds_trait _ _) (trait-with-id CrateDecls TraitId)) (where/error ((ParameterKind_trait _) ...) KindedVarIds_trait) (where/error (Goal_wc ...) (where-clauses->goals WhereClauses_impl)) (where/error Clause (∀ KindedVarIds_impl @@ -381,7 +381,7 @@ [(generics-for-adt-id (CrateDecls CrateId) AdtId) (((VarId (ParameterKind =)) ...) WhereClauses) ; for now we hardcode `=` (invariance) as the variance - (where/error AdtContents (item-with-id CrateDecls AdtId)) + (where/error AdtContents (adt-with-id CrateDecls AdtId)) (where/error (AdtKind ((ParameterKind VarId) ...) WhereClauses AdtVariants) AdtContents) ] ) diff --git a/src/decl/decl-wf-where-clause.rkt b/src/decl/decl-wf-where-clause.rkt index 1e6f6c55..f40cc77a 100644 --- a/src/decl/decl-wf-where-clause.rkt +++ b/src/decl/decl-wf-where-clause.rkt @@ -40,7 +40,7 @@ ; ; * in our example above `(ParameterKind VarId) ...` would match `((type Self) (type T))` ; * and `WhereClauses` would be `(T : Bar ())` - (where/error (trait ((ParameterKind VarId) ...) WhereClauses _) (item-with-id CrateDecls TraitId)) + (where/error (trait ((ParameterKind VarId) ...) WhereClauses _) (trait-with-id CrateDecls TraitId)) ; create a substitution ((Self => A) (T => B)) (where/error (Parameter_value ...) (Ty Parameter ...)) diff --git a/src/decl/grammar.rkt b/src/decl/grammar.rkt index 1b6b56e8..dc741071 100644 --- a/src/decl/grammar.rkt +++ b/src/decl/grammar.rkt @@ -3,7 +3,8 @@ (provide formality-decl crate-decl-with-id trait-decl-id - item-with-id + trait-with-id + adt-with-id crate-decls ) @@ -139,13 +140,25 @@ ) (define-metafunction formality-decl - ;; Find the given named item amongst all the declared crates. - item-with-id : CrateDecls AnyId -> Term + ;; Find the given ADT amongst all the declared crates. + adt-with-id : CrateDecls AdtId -> AdtContents - ((item-with-id CrateDecls AnyId) - Term + ((adt-with-id CrateDecls AdtId) + AdtContents (where (_ ... CrateDecl _ ...) CrateDecls) - (where (_ (crate (_ ... (AnyId Term) _ ...))) CrateDecl) + (where (_ (crate (_ ... (AdtId AdtContents) _ ...))) CrateDecl) + ) + ) + +(define-metafunction formality-decl + ;; Find the given trait amongst all the declared crates. + trait-with-id : CrateDecls TraitId -> TraitContents + + ((trait-with-id CrateDecls TraitId) + TraitContents + + (where (_ ... CrateDecl _ ...) CrateDecls) + (where (_ (crate (_ ... (TraitId TraitContents) _ ...))) CrateDecl) ) ) diff --git a/src/mir/grammar-extended.rkt b/src/mir/grammar-extended.rkt index adc08e73..5b3406cb 100644 --- a/src/mir/grammar-extended.rkt +++ b/src/mir/grammar-extended.rkt @@ -55,7 +55,7 @@ [(decl-of-adt Γ AdtId) AdtContents (where/error (_ CrateDecls) Γ) - (where AdtContents (item-with-id CrateDecls AdtId)) + (where AdtContents (adt-with-id CrateDecls AdtId)) ] ) From b49f25421d56f9581a967fa79f1b5bae6cf1ba6d Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Thu, 2 Jun 2022 20:12:21 -0400 Subject: [PATCH 07/12] integrate AdtId into the AdtDecl, rm AdtContents --- src/decl/decl-ok.rkt | 6 +-- src/decl/decl-to-clause.rkt | 5 +-- src/decl/grammar.rkt | 17 ++++--- src/decl/test/basic-consts.rkt | 5 ++- src/decl/test/basic-statics.rkt | 5 ++- src/decl/test/coinductive/issue-43784.rkt | 6 +-- src/decl/test/coinductive/magic-issue-xxx.rkt | 16 +++---- src/decl/test/copy.rkt | 26 +++++------ src/decl/test/drop.rkt | 44 +++++++++---------- src/decl/test/multi-crate.rkt | 2 +- src/decl/test/wf-where-clauses.rkt | 22 +++++----- src/mir/grammar-extended.rkt | 6 +-- src/mir/type-of.rkt | 8 ++-- 13 files changed, 83 insertions(+), 85 deletions(-) diff --git a/src/decl/decl-ok.rkt b/src/decl/decl-ok.rkt index 6ac7d36f..10c5bb76 100644 --- a/src/decl/decl-ok.rkt +++ b/src/decl/decl-ok.rkt @@ -42,7 +42,7 @@ ;; (implies ((well-formed (type T)) ;; (is-implemented (Ord T))) ;; (well-formed (type Vec)) ...)) - (crate-item-ok-goal CrateDecls (AdtId (AdtKind KindedVarIds (WhereClause ...) AdtVariants))) + (crate-item-ok-goal CrateDecls (AdtKind AdtId KindedVarIds (WhereClause ...) AdtVariants)) Goal_wf (where/error (KindedVarId ...) KindedVarIds) @@ -209,7 +209,7 @@ )))) (where (rigid-ty AdtId Parameters) Ty_impl) - (where (AdtKind KindedVarIds_adt WhereClauses_adt _) (adt-with-id CrateDecls AdtId)) + (where (AdtKind AdtId KindedVarIds_adt WhereClauses_adt _) (adt-with-id CrateDecls AdtId)) (where/error ((ParameterKind_adt VarId_adt) ...) KindedVarIds_adt) (where/error Ty_adt (rigid-ty AdtId (VarId_adt ...))) ] @@ -250,7 +250,7 @@ ))))) (where (rigid-ty AdtId Parameters) Ty_impl) - (where (AdtKind KindedVarIds_adt _ AdtVariants) (adt-with-id CrateDecls AdtId)) + (where (AdtKind AdtId KindedVarIds_adt _ AdtVariants) (adt-with-id CrateDecls AdtId)) (where/error ((ParameterKind_adt VarId_adt) ...) KindedVarIds_adt) (where/error Ty_adt (rigid-ty AdtId (VarId_adt ...))) (where/error ((VariantId ((FieldId Ty_field) ...)) ...) AdtVariants) diff --git a/src/decl/decl-to-clause.rkt b/src/decl/decl-to-clause.rkt index 9ebcdcee..2ae98f67 100644 --- a/src/decl/decl-to-clause.rkt +++ b/src/decl/decl-to-clause.rkt @@ -176,7 +176,7 @@ ;; ;; (∀ ((type T)) ;; (well-formed (type (Foo (T)))) => (well-formed (type T))) - (crate-item-decl-rules CrateDecls CrateId (AdtId (AdtKind KindedVarIds (WhereClause ...) AdtVariants))) + (crate-item-decl-rules CrateDecls CrateId (AdtKind AdtId KindedVarIds (WhereClause ...) AdtVariants)) ((Clause) Invariants_wf Invariants_wc) (where/error ((ParameterKind VarId) ...) KindedVarIds) @@ -381,7 +381,6 @@ [(generics-for-adt-id (CrateDecls CrateId) AdtId) (((VarId (ParameterKind =)) ...) WhereClauses) ; for now we hardcode `=` (invariance) as the variance - (where/error AdtContents (adt-with-id CrateDecls AdtId)) - (where/error (AdtKind ((ParameterKind VarId) ...) WhereClauses AdtVariants) AdtContents) + (where/error (AdtKind AdtId ((ParameterKind VarId) ...) WhereClauses AdtVariants) (adt-with-id CrateDecls AdtId)) ] ) diff --git a/src/decl/grammar.rkt b/src/decl/grammar.rkt index dc741071..2c34638b 100644 --- a/src/decl/grammar.rkt +++ b/src/decl/grammar.rkt @@ -27,8 +27,7 @@ (FeatureDecl ::= (feature FeatureId)) ;; AdtDecl -- struct/enum/union declarations - (AdtDecl ::= (AdtId AdtContents)) - (AdtContents ::= (AdtKind KindedVarIds WhereClauses AdtVariants)) + (AdtDecl ::= (AdtKind AdtId KindedVarIds WhereClauses AdtVariants)) (AdtVariants ::= (AdtVariant ...)) (AdtKind ::= struct enum union) (AdtVariant ::= (VariantId FieldDecls)) @@ -141,24 +140,24 @@ (define-metafunction formality-decl ;; Find the given ADT amongst all the declared crates. - adt-with-id : CrateDecls AdtId -> AdtContents + adt-with-id : CrateDecls AdtId -> AdtDecl - ((adt-with-id CrateDecls AdtId) - AdtContents + [(adt-with-id CrateDecls AdtId) + (AdtKind AdtId KindedVarIds WhereClauses AdtVariants) (where (_ ... CrateDecl _ ...) CrateDecls) - (where (_ (crate (_ ... (AdtId AdtContents) _ ...))) CrateDecl) - ) + (where (_ (crate (_ ... (AdtKind AdtId KindedVarIds WhereClauses AdtVariants) _ ...))) CrateDecl) + ] ) (define-metafunction formality-decl ;; Find the given trait amongst all the declared crates. trait-with-id : CrateDecls TraitId -> TraitContents - ((trait-with-id CrateDecls TraitId) + [(trait-with-id CrateDecls TraitId) TraitContents (where (_ ... CrateDecl _ ...) CrateDecls) (where (_ (crate (_ ... (TraitId TraitContents) _ ...))) CrateDecl) - ) + ] ) diff --git a/src/decl/test/basic-consts.rkt b/src/decl/test/basic-consts.rkt index dca1cddb..13df3c60 100644 --- a/src/decl/test/basic-consts.rkt +++ b/src/decl/test/basic-consts.rkt @@ -10,10 +10,11 @@ (redex-let* formality-decl - ((; trait Debug { } + [(; trait Debug { } TraitDecl (term (Debug (trait ((type Self)) () ())))) (; struct Foo { } - AdtDecl_Foo (term (Foo (struct ((type T)) ((T : Debug())) ((Foo ()))))))) + AdtDecl_Foo (term (struct Foo ((type T)) ((T : Debug())) ((Foo ()))))) + ] (; test that WF checks fail if `T: Debug` is missing redex-let* diff --git a/src/decl/test/basic-statics.rkt b/src/decl/test/basic-statics.rkt index cc7bb0ce..39268bb2 100644 --- a/src/decl/test/basic-statics.rkt +++ b/src/decl/test/basic-statics.rkt @@ -10,8 +10,9 @@ (redex-let* formality-decl - ((; struct Foo { } - AdtDecl_Foo (term (Foo (struct () () ((Foo ()))))))) + [(; struct Foo { } + AdtDecl_Foo (term (struct Foo () () ((Foo ()))))) + ] (; test that Send check fails ; diff --git a/src/decl/test/coinductive/issue-43784.rkt b/src/decl/test/coinductive/issue-43784.rkt index 3b378c9d..5cd2769f 100644 --- a/src/decl/test/coinductive/issue-43784.rkt +++ b/src/decl/test/coinductive/issue-43784.rkt @@ -10,8 +10,8 @@ (redex-let* formality-decl - ((; struct Foo { } - AdtDecl_Foo (term (Foo (struct () () ((struct-variant ())))))) + [(; struct Foo { } + AdtDecl_Foo (term (struct Foo () () ((struct-variant ()))))) (; trait Copy { } TraitDecl_Copy (term (Copy (trait ((type Self)) () ())))) @@ -50,7 +50,7 @@ TraitImplDecl_CompleteB))))) (Env_B (term (env-for-crate-decl CrateDecl_B))) - ) + ] (; The crate A is not well-formed: ; diff --git a/src/decl/test/coinductive/magic-issue-xxx.rkt b/src/decl/test/coinductive/magic-issue-xxx.rkt index 42048798..99ba11ef 100644 --- a/src/decl/test/coinductive/magic-issue-xxx.rkt +++ b/src/decl/test/coinductive/magic-issue-xxx.rkt @@ -13,8 +13,8 @@ redex-let* formality-decl - ((; struct Foo { counter: i32 } - AdtDecl_Foo (term (Foo (struct () () ((struct-variant ((counter (user-ty i32))))))))) + [(; struct Foo { counter: i32 } + AdtDecl_Foo (term (struct Foo () () ((struct-variant ((counter (user-ty i32)))))))) (; reference to `Foo` Ty_Foo (term (rigid-ty Foo ()))) @@ -32,7 +32,7 @@ CrateDecl (term (TheCrate (crate (TraitDecl_Magic TraitDecl_Copy TraitImplDecl_Magic))))) (Env (term (env-for-crate-decl CrateDecl))) - ) + ] (; All decls in crate are considered 'ok'. In particular, the impl is considered 'ok', ; since its where clauses allow it to locally prove that `Self: Copy`. @@ -60,8 +60,8 @@ redex-let* formality-decl - ((; struct Foo { counter: i32 } - AdtDecl_Foo (term (Foo (struct () () ((struct-variant ((counter (user-ty i32))))))))) + [(; struct Foo { counter: i32 } + AdtDecl_Foo (term (struct Foo () () ((struct-variant ((counter (user-ty i32)))))))) (; reference to `Foo` Ty_Foo (term (rigid-ty Foo ()))) @@ -79,7 +79,7 @@ CrateDecl (term (TheCrate (crate (TraitDecl_Magic TraitDecl_Copy TraitImplDecl_Magic))))) (Env (term (env-for-crate-decl CrateDecl))) - ) + ] (; All decls in crate are considered 'ok'. traced '() @@ -107,13 +107,13 @@ formality-decl ((; struct Foo { counter: i32 } - AdtDecl_Foo (term (Foo (struct () () ((struct-variant ((counter (user-ty i32))))))))) + AdtDecl_Foo (term (struct Foo () () ((struct-variant ((counter (user-ty i32)))))))) (; reference to `Foo` Ty_Foo (term (rigid-ty Foo ()))) (; struct Bar { counter: i32 } - AdtDecl_Foo (term (Foo (struct () () ((struct-variant ((counter (user-ty i32))))))))) + AdtDecl_Foo (term (struct Foo () () ((struct-variant ((counter (user-ty i32)))))))) (; reference to `Bar` Ty_Bar (term (rigid-ty Bar ()))) diff --git a/src/decl/test/copy.rkt b/src/decl/test/copy.rkt index 0f147de6..beca371d 100644 --- a/src/decl/test/copy.rkt +++ b/src/decl/test/copy.rkt @@ -43,23 +43,23 @@ ;; Test for that `struct Foo { } struct Bar { f: Foo } impl Copy for Bar` is not permitted ;; because `Foo: Copy` does not hold. - ((; trait rust:Copy { } + [(; trait rust:Copy { } TraitDecl_Copy (term (rust:Copy (trait ((type Self)) () ())))) (; struct Foo { } - AdtDecl_Foo (term (Foo (struct - () ; no generic parameters - () ; no where clauses - ((Foo ())) ; the 1 variant (named `Foo`) - )))) + AdtDecl_Foo (term (struct Foo + () ; no generic parameters + () ; no where clauses + ((Foo ())) ; the 1 variant (named `Foo`) + ))) (; struct Bar { _: Foo } - AdtDecl_Bar (term (Bar (struct - () ; no generic parameters - () ; no where clauses - ((Bar ((f (rigid-ty Foo ())) - ))) ; the 1 variant (named `Foo`) - )))) + AdtDecl_Bar (term (struct Bar + () ; no generic parameters + () ; no where clauses + ((Bar ((f (rigid-ty Foo ())) + ))) ; the 1 variant (named `Foo`) + ))) (; impl rust:Copy for Bar { } TraitImplDecl (term (impl () (rust:Copy ((rigid-ty Bar ()))) () ()))) @@ -73,7 +73,7 @@ (; create the Env for checking things in this crate Env (term (env-for-crate-decl CrateDecl))) - ) + ] (traced '() (decl:test-cannot-prove diff --git a/src/decl/test/drop.rkt b/src/decl/test/drop.rkt index 38ff82fb..5c329f64 100644 --- a/src/decl/test/drop.rkt +++ b/src/decl/test/drop.rkt @@ -15,7 +15,7 @@ ;; Test for that `impl Drop for i32` is not permitted. - ((; trait rust:Drop { } + [(; trait rust:Drop { } TraitDecl_Drop (term (rust:Drop (trait ((type Self)) () ())))) (; impl rust:Drop for i32 { } @@ -28,7 +28,7 @@ (; create the Env for checking things in this crate Env (term (env-for-crate-decl CrateDecl))) - ) + ] (traced '() (decl:test-cannot-prove @@ -42,10 +42,10 @@ ;; Test for case where the Drop impl is for `Foo` only. - ((; struct Foo { } - AdtDecl_Foo (term (Foo (struct ((type T)) () - ((Foo ())) ; the 1 variant (named `Foo`) - )))) + [(; struct Foo { } + AdtDecl_Foo (term (struct Foo ((type T)) () + ((Foo ())) ; the 1 variant (named `Foo`) + ))) (; trait rust:Drop { } TraitDecl_Drop (term (rust:Drop (trait ((type Self)) () ())))) @@ -61,7 +61,7 @@ (; create the Env for checking things in this crate Env (term (env-for-crate-decl CrateDecl))) - ) + ] (traced '() (decl:test-cannot-prove @@ -76,10 +76,10 @@ ;; Test for case where the Drop impl adds an extra where clause ;; that doesn't follow from the struct. - ((; struct Foo { } - AdtDecl_Foo (term (Foo (struct ((type T)) () - ((Foo ())) ; the 1 variant (named `Foo`) - )))) + [(; struct Foo { } + AdtDecl_Foo (term (struct Foo ((type T)) () + ((Foo ())) ; the 1 variant (named `Foo`) + ))) (; trait Debug { } TraitDecl_Debug (term (Debug (trait ((type Self)) () ())))) @@ -96,7 +96,7 @@ TraitDecl_Drop TraitImplDecl ))))) - ) + ] (traced '() (decl:test-crate-decl-not-ok (CrateDecl) TheCrate)) ) @@ -108,10 +108,10 @@ ;; are syntactically present on the struct, but they are entailed by ;; the predicates on the struct. - ((; struct Foo { } - AdtDecl_Foo (term (Foo (struct ((type T)) () - ((Foo ())) ; the 1 variant (named `Foo`) - )))) + [(; struct Foo { } + AdtDecl_Foo (term (struct Foo ((type T)) () + ((Foo ())) ; the 1 variant (named `Foo`) + ))) (; trait rust:Drop { } TraitDecl_Drop (term (rust:Drop (trait ((type Self)) () ())))) @@ -127,7 +127,7 @@ (; create the Env for checking things in this crate Env (term (env-for-crate-decl CrateDecl))) - ) + ] (traced '() (decl:test-can-prove @@ -143,10 +143,10 @@ ;; are syntactically present on the struct, but they are entailed by ;; the predicates on the struct. - ((; struct Foo where T: Ord { } - AdtDecl_Foo (term (Foo (struct ((type T)) ((T : Ord())) - ((Foo ())) ; the 1 variant (named `Foo`) - )))) + [(; struct Foo where T: Ord { } + AdtDecl_Foo (term (struct Foo ((type T)) ((T : Ord())) + ((Foo ())) ; the 1 variant (named `Foo`) + ))) (; trait rust:Drop { } TraitDecl_Drop (term (rust:Drop (trait ((type Self)) () ())))) @@ -172,7 +172,7 @@ TraitDecl_Ord TraitImplDecl ))))) - ) + ] (traced '() (decl:test-crate-decl-ok (CrateDecl) TheCrate)) diff --git a/src/decl/test/multi-crate.rkt b/src/decl/test/multi-crate.rkt index d83e0ccb..4ab4ec3b 100644 --- a/src/decl/test/multi-crate.rkt +++ b/src/decl/test/multi-crate.rkt @@ -33,7 +33,7 @@ CrateDecl_B (redex-let* formality-decl ((TraitDecl_WithDebug (term (WithDebug (trait ((type Self) (type T)) ((T : Debug())) ())))) - (AdtDecl_Foo (term (Foo (struct ((type T)) ((T : Debug())) ((Foo ())))))) + (AdtDecl_Foo (term (struct Foo ((type T)) ((T : Debug())) ((Foo ()))))) (TraitImplDecl (term (impl ((type T)) (WithDebug ((rigid-ty Foo (T)) T)) () ()))) ) (term (CrateB (crate (TraitDecl_WithDebug AdtDecl_Foo TraitImplDecl)))))) diff --git a/src/decl/test/wf-where-clauses.rkt b/src/decl/test/wf-where-clauses.rkt index ee24f533..2e55fd7e 100644 --- a/src/decl/test/wf-where-clauses.rkt +++ b/src/decl/test/wf-where-clauses.rkt @@ -25,9 +25,9 @@ redex-let* formality-decl - ((AdtDecl_S (term (S (struct ((type A) (type B)) - ((A : Foo(B))) - ((S ())))))) + ((AdtDecl_S (term (struct S ((type A) (type B)) + ((A : Foo(B))) + ((S ()))))) (CrateDecl (term (C (crate (TraitDecl_Foo TraitDecl_Bar @@ -44,9 +44,9 @@ redex-let* formality-decl - ((AdtDecl_S (term (S (struct ((type A) (type B)) - ((A : Foo(B))) - ((S ())))))) + ((AdtDecl_S (term (struct S ((type A) (type B)) + ((A : Foo(B))) + ((S ()))))) (CrateDecl (term (C (crate ((feature expanded-implied-bounds) TraitDecl_Foo @@ -62,11 +62,11 @@ redex-let* formality-decl - ((AdtDecl_S (term (S (struct ((type A) (type B)) - ((A : Foo(B)) - (B : Bar()) - ) - ((S ())))))) + ((AdtDecl_S (term (struct S ((type A) (type B)) + ((A : Foo(B)) + (B : Bar()) + ) + ((S ()))))) (CrateDecl (term (C (crate (TraitDecl_Foo TraitDecl_Bar diff --git a/src/mir/grammar-extended.rkt b/src/mir/grammar-extended.rkt index 5b3406cb..c6c8dee9 100644 --- a/src/mir/grammar-extended.rkt +++ b/src/mir/grammar-extended.rkt @@ -50,12 +50,10 @@ (define-metafunction formality-mir-extended ;; Returns the `AdtContents` of the ADT with the given `AdtId`. - decl-of-adt : Γ AdtId -> AdtContents + decl-of-adt : Γ AdtId -> AdtDecl [(decl-of-adt Γ AdtId) - AdtContents - (where/error (_ CrateDecls) Γ) - (where AdtContents (adt-with-id CrateDecls AdtId)) + (adt-with-id (crate-decls-of-Γ CrateDecls) AdtId) ] ) diff --git a/src/mir/type-of.rkt b/src/mir/type-of.rkt index 1b57277c..cdcca88b 100644 --- a/src/mir/type-of.rkt +++ b/src/mir/type-of.rkt @@ -44,7 +44,7 @@ ; ; extract the name of the singular variant (place-type-of Γ Place (rigid-ty AdtId Parameters) ()) - (where (struct _ _ ((VariantId _))) (decl-of-adt Γ AdtId)) + (where (struct AdtId _ _ ((VariantId _))) (decl-of-adt Γ AdtId)) (field-ty Γ AdtId Parameters VariantId FieldId Ty_field) ---------------------------------- (place-type-of Γ (field Place FieldId) Ty_field ()) @@ -54,7 +54,7 @@ ; ; must have been downcast to a particular variant (place-type-of Γ Place (rigid-ty AdtId Parameters) (VariantId)) - (where (enum _ _ _) (decl-of-adt Γ AdtId)) + (where (enum AdtId _ _ _) (decl-of-adt Γ AdtId)) (field-ty Γ AdtId Parameters VariantId FieldId Ty_field) ---------------------------------- (place-type-of Γ (field Place FieldId) Ty_field ()) @@ -63,7 +63,7 @@ [; downcast to an enum variant (place-type-of Γ Place (rigid-ty AdtId Parameters) ()) - (where (enum _ _ (_ ... (VariantId _) _ ...)) (decl-of-adt Γ AdtId)) + (where (enum AdtId _ _ (_ ... (VariantId _) _ ...)) (decl-of-adt Γ AdtId)) ---------------------------------- (place-type-of Γ (downcast Place VariantId) (rigid-ty AdtId Parameters) (VariantId)) ] @@ -93,7 +93,7 @@ #:mode (field-ty I I I I I O) #:contract (field-ty Γ AdtId Parameters VariantId FieldId Ty) - [(where (_ KindedVarIds _ (_ ... (VariantId FieldDecls) _ ...)) (decl-of-adt Γ AdtId)) + [(where (_ AdtId KindedVarIds _ (_ ... (VariantId FieldDecls) _ ...)) (decl-of-adt Γ AdtId)) (where/error Substitution (create-substitution KindedVarIds Parameters)) (where (_ ... (FieldId Ty) _ ...) FieldDecls) (where/error Ty_substituted (apply-substitution Substitution Ty)) From 6db083c2ac7b3370c80f791bb66d270115f9e65d Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Thu, 2 Jun 2022 20:21:18 -0400 Subject: [PATCH 08/12] integrate TraitId into trait declarations --- src/decl/decl-ok.rkt | 4 ++-- src/decl/decl-to-clause.rkt | 4 ++-- src/decl/decl-wf-where-clause.rkt | 2 +- src/decl/grammar.rkt | 11 ++++----- src/decl/test/basic-consts.rkt | 2 +- src/decl/test/basic.rkt | 2 +- src/decl/test/coinductive/issue-43784.rkt | 6 ++--- src/decl/test/coinductive/magic-issue-xxx.rkt | 12 +++++----- src/decl/test/copy.rkt | 4 ++-- src/decl/test/drop.rkt | 16 ++++++------- src/decl/test/implied-bounds.rkt | 14 +++++------ src/decl/test/libcore.rkt | 8 +++---- src/decl/test/multi-crate.rkt | 4 ++-- src/decl/test/supertraits.rkt | 16 ++++++------- src/decl/test/wf-where-clauses.rkt | 23 +++++++++---------- 15 files changed, 63 insertions(+), 65 deletions(-) diff --git a/src/decl/decl-ok.rkt b/src/decl/decl-ok.rkt index 10c5bb76..20ea3fb4 100644 --- a/src/decl/decl-ok.rkt +++ b/src/decl/decl-ok.rkt @@ -80,7 +80,7 @@ ;; trait Foo<'a, T> where T: Ord { ... } ;; ;; we require that all the trait-item WF goals are met. - (crate-item-ok-goal CrateDecls (TraitId (trait KindedVarIds (WhereClause ...) (TraitItem ...)))) + (crate-item-ok-goal CrateDecls (trait TraitId KindedVarIds (WhereClause ...) (TraitItem ...))) (∀ KindedVarIds (implies ((well-formed KindedVarId) ... (where-clause->hypothesis WhereClause) ...) (&& (Goal_trait-item ... @@ -109,7 +109,7 @@ is-implemented (TraitId (Parameter_trait ...))) (well-formed-where-clause-goal CrateDecls WhereClause_impl) ...)))) - (where/error (TraitId (trait ((ParameterKind_trait _) ...) _ _)) (trait-decl-with-id CrateDecls TraitId)) + (where/error (trait TraitId ((ParameterKind_trait _) ...) _ _) (trait-decl-with-id CrateDecls TraitId)) (where/error (KindedVarId_impl ...) KindedVarIds_impl) (where/error (WhereClause_impl ...) WhereClauses_impl) ] diff --git a/src/decl/decl-to-clause.rkt b/src/decl/decl-to-clause.rkt index 2ae98f67..f7e82df3 100644 --- a/src/decl/decl-to-clause.rkt +++ b/src/decl/decl-to-clause.rkt @@ -222,7 +222,7 @@ ;; (is-implemented (Foo (Self 'a T))) => (well-formed (type Self)) ;; (is-implemented (Foo (Self 'a T))) => (well-formed (lifetime 'a)) ;; (is-implemented (Foo (Self 'a T))) => (well-formed (type T))) - (crate-item-decl-rules CrateDecls CrateId (TraitId (trait KindedVarIds (WhereClause ...) TraitItems))) + (crate-item-decl-rules CrateDecls CrateId (trait TraitId KindedVarIds (WhereClause ...) TraitItems)) ((Clause) (Invariant_wc ... Invariant_wf ... @@ -281,7 +281,7 @@ ((Clause) () ()) (where/error (TraitId (Parameter_trait ...)) TraitRef) - (where/error (trait KindedVarIds_trait _ _) (trait-with-id CrateDecls TraitId)) + (where/error (trait TraitId KindedVarIds_trait _ _) (trait-with-id CrateDecls TraitId)) (where/error ((ParameterKind_trait _) ...) KindedVarIds_trait) (where/error (Goal_wc ...) (where-clauses->goals WhereClauses_impl)) (where/error Clause (∀ KindedVarIds_impl diff --git a/src/decl/decl-wf-where-clause.rkt b/src/decl/decl-wf-where-clause.rkt index f40cc77a..047e6821 100644 --- a/src/decl/decl-wf-where-clause.rkt +++ b/src/decl/decl-wf-where-clause.rkt @@ -40,7 +40,7 @@ ; ; * in our example above `(ParameterKind VarId) ...` would match `((type Self) (type T))` ; * and `WhereClauses` would be `(T : Bar ())` - (where/error (trait ((ParameterKind VarId) ...) WhereClauses _) (trait-with-id CrateDecls TraitId)) + (where/error (trait TraitId ((ParameterKind VarId) ...) WhereClauses _) (trait-with-id CrateDecls TraitId)) ; create a substitution ((Self => A) (T => B)) (where/error (Parameter_value ...) (Ty Parameter ...)) diff --git a/src/decl/grammar.rkt b/src/decl/grammar.rkt index 2c34638b..721979ea 100644 --- a/src/decl/grammar.rkt +++ b/src/decl/grammar.rkt @@ -40,8 +40,7 @@ ;; TraitDecl -- trait Foo { ... } ;; ;; Unlike in Rust, the `KindedVarIds` here always include with `(type Self)` explicitly. - (TraitDecl ::= (TraitId TraitContents)) - (TraitContents ::= (trait KindedVarIds WhereClauses TraitItems)) + (TraitDecl ::= (trait TraitId KindedVarIds WhereClauses TraitItems)) ;; TraitItem -- (TraitItems ::= (TraitItem ...)) @@ -135,7 +134,7 @@ (define-metafunction formality-decl trait-decl-id : TraitDecl -> TraitId - ((trait-decl-id (TraitId TraitContents)) TraitId) + ((trait-decl-id (trait TraitId _ _ _)) TraitId) ) (define-metafunction formality-decl @@ -152,12 +151,12 @@ (define-metafunction formality-decl ;; Find the given trait amongst all the declared crates. - trait-with-id : CrateDecls TraitId -> TraitContents + trait-with-id : CrateDecls TraitId -> TraitDecl [(trait-with-id CrateDecls TraitId) - TraitContents + (trait TraitId KindedVarIds WhereClauses TraitItems) (where (_ ... CrateDecl _ ...) CrateDecls) - (where (_ (crate (_ ... (TraitId TraitContents) _ ...))) CrateDecl) + (where (_ (crate (_ ... (trait TraitId KindedVarIds WhereClauses TraitItems) _ ...))) CrateDecl) ] ) diff --git a/src/decl/test/basic-consts.rkt b/src/decl/test/basic-consts.rkt index 13df3c60..77e2dc3d 100644 --- a/src/decl/test/basic-consts.rkt +++ b/src/decl/test/basic-consts.rkt @@ -11,7 +11,7 @@ formality-decl [(; trait Debug { } - TraitDecl (term (Debug (trait ((type Self)) () ())))) + TraitDecl (term (trait Debug ((type Self)) () ()))) (; struct Foo { } AdtDecl_Foo (term (struct Foo ((type T)) ((T : Debug())) ((Foo ()))))) ] diff --git a/src/decl/test/basic.rkt b/src/decl/test/basic.rkt index 4a0f4510..62877364 100644 --- a/src/decl/test/basic.rkt +++ b/src/decl/test/basic.rkt @@ -14,7 +14,7 @@ (redex-let* formality-decl - ((TraitDecl (term (Debug (trait ((type Self)) () ())))) + ((TraitDecl (term (trait Debug ((type Self)) () ()))) (TraitImplDecl (term (impl () (Debug ((user-ty i32))) () ()))) (CrateDecl (term (TheCrate (crate (TraitDecl TraitImplDecl))))) (Env (term (env-for-crate-decl CrateDecl))) diff --git a/src/decl/test/coinductive/issue-43784.rkt b/src/decl/test/coinductive/issue-43784.rkt index 5cd2769f..bf8ff4b7 100644 --- a/src/decl/test/coinductive/issue-43784.rkt +++ b/src/decl/test/coinductive/issue-43784.rkt @@ -14,13 +14,13 @@ AdtDecl_Foo (term (struct Foo () () ((struct-variant ()))))) (; trait Copy { } - TraitDecl_Copy (term (Copy (trait ((type Self)) () ())))) + TraitDecl_Copy (term (trait Copy ((type Self)) () ()))) (; trait Partial: Copy { } - TraitDecl_Partial (term (Partial (trait ((type Self)) ((Self : Copy())) ())))) + TraitDecl_Partial (term (trait Partial((type Self)) ((Self : Copy())) ()))) (; trait Complete: Partial { } - TraitDecl_Complete (term (Complete (trait ((type Self)) ((Self : Partial())) ())))) + TraitDecl_Complete (term (trait Complete ((type Self)) ((Self : Partial())) ()))) (; impl Partial for T where T: Complete {} TraitImplDecl_Partial (term (impl ((type T)) (Partial (T)) ((T : Complete())) ()))) diff --git a/src/decl/test/coinductive/magic-issue-xxx.rkt b/src/decl/test/coinductive/magic-issue-xxx.rkt index 99ba11ef..0f3dca32 100644 --- a/src/decl/test/coinductive/magic-issue-xxx.rkt +++ b/src/decl/test/coinductive/magic-issue-xxx.rkt @@ -20,10 +20,10 @@ Ty_Foo (term (rigid-ty Foo ()))) (; trait Magic: Copy { } - TraitDecl_Magic (term (Magic (trait ((type Self)) ((Self : Copy())) ())))) + TraitDecl_Magic (term (trait Magic ((type Self)) ((Self : Copy())) ()))) (; trait Copy { } - TraitDecl_Copy (term (Copy (trait ((type Self)) () ())))) + TraitDecl_Copy (term (trait Copy ((type Self)) () ()))) (; impl Magic for T where T: Magic { } TraitImplDecl_Magic (term (impl ((type T)) (Magic (T)) ((T : Magic())) ()))) @@ -67,10 +67,10 @@ Ty_Foo (term (rigid-ty Foo ()))) (; trait Magic: Copy { } - TraitDecl_Magic (term (Magic (trait ((type Self)) ((Self : Copy())) ())))) + TraitDecl_Magic (term (trait Magic ((type Self)) ((Self : Copy())) ()))) (; trait Copy: Magic { } - TraitDecl_Copy (term (Copy (trait ((type Self)) ((Self : Magic())) ())))) + TraitDecl_Copy (term (trait Copy ((type Self)) ((Self : Magic())) ()))) (; impl Magic for T where T: Magic { } TraitImplDecl_Magic (term (impl ((type T)) (Magic (T)) ((T : Magic())) ()))) @@ -119,10 +119,10 @@ Ty_Bar (term (rigid-ty Bar ()))) (; trait Magic: Copy { } - TraitDecl_Magic (term (Magic (trait ((type Self)) ((Self : Copy())) ())))) + TraitDecl_Magic (term (trait Magic ((type Self)) ((Self : Copy())) ()))) (; trait Copy { } - TraitDecl_Copy (term (Copy (trait ((type Self)) () ())))) + TraitDecl_Copy (term (trait Copy ((type Self)) () ()))) (; impl Magic for T where T: Magic { } TraitImplDecl_Magic (term (impl ((type T)) (Magic (T)) ((T : Magic())) ()))) diff --git a/src/decl/test/copy.rkt b/src/decl/test/copy.rkt index beca371d..c47d8e8f 100644 --- a/src/decl/test/copy.rkt +++ b/src/decl/test/copy.rkt @@ -16,7 +16,7 @@ ;; Test for that `impl Copy for i32` is permitted. ((; trait rust:Copy { _: Foo } - TraitDecl_Copy (term (rust:Copy (trait ((type Self)) () ())))) + TraitDecl_Copy (term (trait rust:Copy ((type Self)) () ()))) (; impl rust:Copy for i32 { } TraitImplDecl (term (impl () (rust:Copy ((user-ty i32))) () ()))) @@ -44,7 +44,7 @@ ;; because `Foo: Copy` does not hold. [(; trait rust:Copy { } - TraitDecl_Copy (term (rust:Copy (trait ((type Self)) () ())))) + TraitDecl_Copy (term (trait rust:Copy ((type Self)) () ()))) (; struct Foo { } AdtDecl_Foo (term (struct Foo diff --git a/src/decl/test/drop.rkt b/src/decl/test/drop.rkt index 5c329f64..db38c9b5 100644 --- a/src/decl/test/drop.rkt +++ b/src/decl/test/drop.rkt @@ -16,7 +16,7 @@ ;; Test for that `impl Drop for i32` is not permitted. [(; trait rust:Drop { } - TraitDecl_Drop (term (rust:Drop (trait ((type Self)) () ())))) + TraitDecl_Drop (term (trait rust:Drop ((type Self)) () ()))) (; impl rust:Drop for i32 { } TraitImplDecl (term (impl () (rust:Drop ((user-ty i32))) () ()))) @@ -48,7 +48,7 @@ ))) (; trait rust:Drop { } - TraitDecl_Drop (term (rust:Drop (trait ((type Self)) () ())))) + TraitDecl_Drop (term (trait rust:Drop ((type Self)) () ()))) (; impl rust:Drop for Foo { } //~ ERROR TraitImplDecl (term (impl () (rust:Drop ((rigid-ty Foo ((user-ty i32))))) () ()))) @@ -82,10 +82,10 @@ ))) (; trait Debug { } - TraitDecl_Debug (term (Debug (trait ((type Self)) () ())))) + TraitDecl_Debug (term (trait Debug ((type Self)) () ()))) (; trait rust:Drop { } - TraitDecl_Drop (term (rust:Drop (trait ((type Self)) () ())))) + TraitDecl_Drop (term (trait rust:Drop ((type Self)) () ()))) (; impl rust:Drop for Foo where U: Debug { } //~ ERROR TraitImplDecl (term (impl ((type U)) (rust:Drop ((rigid-ty Foo (U)))) ((U : Debug())) ()))) @@ -114,7 +114,7 @@ ))) (; trait rust:Drop { } - TraitDecl_Drop (term (rust:Drop (trait ((type Self)) () ())))) + TraitDecl_Drop (term (trait rust:Drop ((type Self)) () ()))) (; impl rust:Drop for Foo { } TraitImplDecl (term (impl ((type U)) (rust:Drop ((rigid-ty Foo (U)))) () ()))) @@ -149,13 +149,13 @@ ))) (; trait rust:Drop { } - TraitDecl_Drop (term (rust:Drop (trait ((type Self)) () ())))) + TraitDecl_Drop (term (trait rust:Drop ((type Self)) () ()))) (; trait Eq { } - TraitDecl_Eq (term (Eq (trait ((type Self)) () ())))) + TraitDecl_Eq (term (trait Eq ((type Self)) () ()))) (; trait Ord: Eq { } - TraitDecl_Ord (term (Ord (trait ((type Self)) ((Self : Eq())) ())))) + TraitDecl_Ord (term (trait Ord ((type Self)) ((Self : Eq())) ()))) (; impl rust:Drop for Foo where T: Ord + Eq { } TraitImplDecl (term (impl ((type U)) diff --git a/src/decl/test/implied-bounds.rkt b/src/decl/test/implied-bounds.rkt index c6411fb8..3350632d 100644 --- a/src/decl/test/implied-bounds.rkt +++ b/src/decl/test/implied-bounds.rkt @@ -14,12 +14,12 @@ formality-decl ((; trait Foo where Self: Bar, T: Bar { } - TraitDecl_Foo (term (Foo (trait ((type Self) (type T)) - ((T : Bar()) (Self : Bar())) - ())))) + TraitDecl_Foo (term (trait Foo ((type Self) (type T)) + ((T : Bar()) (Self : Bar())) + ()))) (; trait Bar { } - TraitDecl_Bar (term (Bar (trait ((type Self)) () ())))) + TraitDecl_Bar (term (trait Bar ((type Self)) () ()))) (Env (term (env-for-crate-decl (C (crate (TraitDecl_Foo TraitDecl_Bar)))))) @@ -61,9 +61,9 @@ formality-decl ((; trait Foo<'l, T> where Self: 'a, T: 'a { } - TraitDecl_Foo (term (Foo (trait ((type Self) (lifetime l) (type T)) - ((T : l) (Self : l)) - ())))) + TraitDecl_Foo (term (trait Foo ((type Self) (lifetime l) (type T)) + ((T : l) (Self : l)) + ()))) (Env (term (env-for-crate-decl (C (crate (TraitDecl_Foo)))))) diff --git a/src/decl/test/libcore.rkt b/src/decl/test/libcore.rkt index 60bddf6b..85ce1b60 100644 --- a/src/decl/test/libcore.rkt +++ b/src/decl/test/libcore.rkt @@ -11,10 +11,10 @@ ,(redex-let* formality-decl [ - (TraitDecl_Send (term (rust:Send (trait ((type Self)) () ())))) - (TraitDecl_Sync (term (rust:Sync (trait ((type Self)) () ())))) - (TraitDecl_Copy (term (rust:Copy (trait ((type Self)) () ())))) - (TraitDecl_Drop (term (rust:Drop (trait ((type Self)) () ())))) + (TraitDecl_Send (term (trait rust:Send ((type Self)) () ()))) + (TraitDecl_Sync (term (trait rust:Sync ((type Self)) () ()))) + (TraitDecl_Copy (term (trait rust:Copy ((type Self)) () ()))) + (TraitDecl_Drop (term (trait rust:Drop ((type Self)) () ()))) (CrateDecl_core (term (core (crate (TraitDecl_Send TraitDecl_Sync TraitDecl_Copy diff --git a/src/decl/test/multi-crate.rkt b/src/decl/test/multi-crate.rkt index 4ab4ec3b..e87a0a69 100644 --- a/src/decl/test/multi-crate.rkt +++ b/src/decl/test/multi-crate.rkt @@ -18,7 +18,7 @@ ;; CrateDecl_A (redex-let* formality-decl - ((TraitDecl (term (Debug (trait ((type Self)) () ())))) + ((TraitDecl (term (trait Debug ((type Self)) () ()))) (TraitImplDecl (term (impl () (Debug ((user-ty i32))) () ()))) ) (term (CrateA (crate (TraitDecl TraitImplDecl)))))) @@ -32,7 +32,7 @@ ;; CrateDecl_B (redex-let* formality-decl - ((TraitDecl_WithDebug (term (WithDebug (trait ((type Self) (type T)) ((T : Debug())) ())))) + ((TraitDecl_WithDebug (term (trait WithDebug ((type Self) (type T)) ((T : Debug())) ()))) (AdtDecl_Foo (term (struct Foo ((type T)) ((T : Debug())) ((Foo ()))))) (TraitImplDecl (term (impl ((type T)) (WithDebug ((rigid-ty Foo (T)) T)) () ()))) ) diff --git a/src/decl/test/supertraits.rkt b/src/decl/test/supertraits.rkt index d62ebbe8..28d8511f 100644 --- a/src/decl/test/supertraits.rkt +++ b/src/decl/test/supertraits.rkt @@ -14,14 +14,14 @@ (redex-let* formality-decl - ((TraitDecl_PartialEq (term (PartialEq (trait ((type Self)) - () - () - )))) - (TraitDecl_Eq (term (Eq (trait ((type Self)) - ((Self : PartialEq())) - ())))) - (TraitDecl_Debug (term (Debug (trait ((type Self)) () ())))) + ((TraitDecl_PartialEq (term (trait PartialEq ((type Self)) + () + () + ))) + (TraitDecl_Eq (term (trait Eq ((type Self)) + ((Self : PartialEq())) + ()))) + (TraitDecl_Debug (term (trait Debug ((type Self)) () ()))) (CrateDecl (term (TheCrate (crate (TraitDecl_PartialEq TraitDecl_Eq))))) (Env (term (env-for-crate-decl CrateDecl))) ) diff --git a/src/decl/test/wf-where-clauses.rkt b/src/decl/test/wf-where-clauses.rkt index 2e55fd7e..cd26ffbe 100644 --- a/src/decl/test/wf-where-clauses.rkt +++ b/src/decl/test/wf-where-clauses.rkt @@ -15,10 +15,10 @@ formality-decl ((; trait Foo where T: Bar { } - TraitDecl_Foo (term (Foo (trait ((type Self) (type T)) ((T : Bar())) ())))) + TraitDecl_Foo (term (trait Foo ((type Self) (type T)) ((T : Bar())) ()))) (; trait Bar { } - TraitDecl_Bar (term (Bar (trait ((type Self)) () ())))) + TraitDecl_Bar (term (trait Bar ((type Self)) () ()))) ) (; struct S where A: Foo { } @@ -83,11 +83,10 @@ redex-let* formality-decl - ((TraitDecl_Baz (term (Baz (trait ((type Self) (type A)) - ((Self : Foo(A)) - ) - ())))) - + ((TraitDecl_Baz (term (trait Baz ((type Self) (type A)) + ((Self : Foo(A)) + ) + ()))) (CrateDecl (term (C (crate (TraitDecl_Foo TraitDecl_Bar TraitDecl_Baz @@ -103,11 +102,11 @@ redex-let* formality-decl - ((TraitDecl_Baz (term (Baz (trait ((type Self) (type A)) - ((Self : Foo(A)) - (A : Bar()) - ) - ())))) + ((TraitDecl_Baz (term (trait Baz ((type Self) (type A)) + ((Self : Foo(A)) + (A : Bar()) + ) + ()))) (CrateDecl (term (C (crate (TraitDecl_Foo TraitDecl_Bar From 294705ed8f5e94376c198f94cb437d5adab58ccb Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Thu, 2 Jun 2022 20:24:48 -0400 Subject: [PATCH 09/12] remove duplicate fn --- src/decl/decl-from-crate.rkt | 17 ----------------- src/decl/decl-ok.rkt | 3 +-- 2 files changed, 1 insertion(+), 19 deletions(-) delete mode 100644 src/decl/decl-from-crate.rkt diff --git a/src/decl/decl-from-crate.rkt b/src/decl/decl-from-crate.rkt deleted file mode 100644 index b9eb40fc..00000000 --- a/src/decl/decl-from-crate.rkt +++ /dev/null @@ -1,17 +0,0 @@ -#lang racket -(require redex/reduction-semantics - "grammar.rkt") -(provide trait-decl-with-id) - -(define-metafunction formality-decl - ;; Find the given trait amongst all the declared crates. - trait-decl-with-id : CrateDecls TraitId -> TraitDecl - - ((trait-decl-with-id CrateDecls TraitId) - TraitDecl - - (where (_ ... CrateDecl _ ...) CrateDecls) - (where (CrateId (crate (_ ... TraitDecl _ ...))) CrateDecl) - (where TraitId (trait-decl-id TraitDecl)) - ) - ) \ No newline at end of file diff --git a/src/decl/decl-ok.rkt b/src/decl/decl-ok.rkt index 20ea3fb4..e5767746 100644 --- a/src/decl/decl-ok.rkt +++ b/src/decl/decl-ok.rkt @@ -4,7 +4,6 @@ "../ty/grammar.rkt" "../logic/grammar.rkt" "../ty/where-clauses.rkt" - "decl-from-crate.rkt" "../logic/env.rkt" "decl-wf-where-clause.rkt" ) @@ -109,7 +108,7 @@ is-implemented (TraitId (Parameter_trait ...))) (well-formed-where-clause-goal CrateDecls WhereClause_impl) ...)))) - (where/error (trait TraitId ((ParameterKind_trait _) ...) _ _) (trait-decl-with-id CrateDecls TraitId)) + (where/error (trait TraitId ((ParameterKind_trait _) ...) _ _) (trait-with-id CrateDecls TraitId)) (where/error (KindedVarId_impl ...) KindedVarIds_impl) (where/error (WhereClause_impl ...) WhereClauses_impl) ] From 3f856948d13b8199ba4fb215a4287888e4823511 Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Thu, 2 Jun 2022 20:33:39 -0400 Subject: [PATCH 10/12] move ConstId and StaticId into decls --- src/decl/decl-ok.rkt | 4 +-- src/decl/grammar.rkt | 8 +++--- src/decl/test/basic-consts.rkt | 4 +-- src/decl/test/basic-statics.rkt | 4 +-- src/mir/all-check.rkt | 4 +-- src/mir/test/issue-25860.rkt | 44 ++++++++++++++++----------------- 6 files changed, 33 insertions(+), 35 deletions(-) diff --git a/src/decl/decl-ok.rkt b/src/decl/decl-ok.rkt index e5767746..20713cd9 100644 --- a/src/decl/decl-ok.rkt +++ b/src/decl/decl-ok.rkt @@ -118,7 +118,7 @@ ;; const NAMED: Foo where T: Trait; ;; ;; we require that the type is well formed assuming the where clauses are satisfied. - (crate-item-ok-goal CrateDecls (ConstId (const KindedVarIds WhereClauses Ty FnBody))) + (crate-item-ok-goal CrateDecls (const ConstId KindedVarIds WhereClauses Ty FnBody)) (∀ KindedVarIds (implies (; assuming all generic parameters are WF... @@ -139,7 +139,7 @@ ;; ;; we require that the type is well formed assuming the where clauses are satisfied ;; and that the type is `Send`. - (crate-item-ok-goal CrateDecls (StaticId (static KindedVarIds WhereClauses Ty FnBody))) + (crate-item-ok-goal CrateDecls (static StaticId KindedVarIds WhereClauses Ty FnBody)) (∀ KindedVarIds (implies (; assuming all generic parameters are WF... diff --git a/src/decl/grammar.rkt b/src/decl/grammar.rkt index 721979ea..81ad6c48 100644 --- a/src/decl/grammar.rkt +++ b/src/decl/grammar.rkt @@ -52,12 +52,10 @@ (TraitImplDecl ::= (impl KindedVarIds TraitRef WhereClauses ImplItems)) ;; Named statics - (StaticDecl ::= (StaticId StaticContents)) - (StaticContents ::= (static KindedVarIds WhereClauses Ty FnBody)) + (StaticDecl ::= (static StaticId KindedVarIds WhereClauses Ty FnBody)) ;; Named constants - (ConstDecl ::= (ConstId ConstContents)) - (ConstContents ::= (const KindedVarIds WhereClauses Ty FnBody)) + (ConstDecl ::= (const ConstId KindedVarIds WhereClauses Ty FnBody)) ;; ImplItem -- (ImplItems ::= (ImplItem ...)) @@ -99,7 +97,7 @@ WhereClauses #:refers-to (shadow VarId ...) Ty #:refers-to (shadow VarId ...) FnBody #:refers-to (shadow VarId ...)) - (static ConstId + (static StaticId ((ParameterKind VarId) ...) WhereClauses #:refers-to (shadow VarId ...) Ty #:refers-to (shadow VarId ...) diff --git a/src/decl/test/basic-consts.rkt b/src/decl/test/basic-consts.rkt index 77e2dc3d..28b201d0 100644 --- a/src/decl/test/basic-consts.rkt +++ b/src/decl/test/basic-consts.rkt @@ -21,7 +21,7 @@ formality-decl [ (; const BROKEN: Foo; - ConstDecl_broken (term (BROKEN (const ((type T)) () (rigid-ty Foo (T)) dummy-body)))) + ConstDecl_broken (term (const BROKEN ((type T)) () (rigid-ty Foo (T)) dummy-body))) (CrateDecl (term (TheCrate (crate (TraitDecl AdtDecl_Foo ConstDecl_broken))))) ] @@ -34,7 +34,7 @@ formality-decl [ (; const OK: Foo; - ConstDecl_ok (term (OK (const ((type T)) ((T : Debug())) (rigid-ty Foo (T)) dummy-body)))) + ConstDecl_ok (term (const OK ((type T)) ((T : Debug())) (rigid-ty Foo (T)) dummy-body))) (CrateDecl (term (TheCrate (crate (TraitDecl AdtDecl_Foo ConstDecl_ok))))) ] diff --git a/src/decl/test/basic-statics.rkt b/src/decl/test/basic-statics.rkt index 39268bb2..d3c425b8 100644 --- a/src/decl/test/basic-statics.rkt +++ b/src/decl/test/basic-statics.rkt @@ -20,7 +20,7 @@ redex-let* formality-decl [(; static S: Foo; - StaticDecl (term (S (static () () (rigid-ty Foo ()) fn-body)))) + StaticDecl (term (static S () () (rigid-ty Foo ()) fn-body))) (CrateDecl (term (TheCrate (crate (AdtDecl_Foo StaticDecl))))) ] @@ -36,7 +36,7 @@ redex-let* formality-decl [(; static S: Foo; - StaticDecl (term (S (static () () (rigid-ty Foo ()) dummy-body)))) + StaticDecl (term (static S () () (rigid-ty Foo ()) dummy-body))) (; impl Send for Foo TraitImplDecl_Sync (term (impl ((type T)) (rust:Sync ((rigid-ty Foo ()))) () ()))) (CrateDecl (term (TheCrate (crate (AdtDecl_Foo StaticDecl TraitImplDecl_Sync))))) diff --git a/src/mir/all-check.rkt b/src/mir/all-check.rkt index ed67f5ba..5601c628 100644 --- a/src/mir/all-check.rkt +++ b/src/mir/all-check.rkt @@ -69,7 +69,7 @@ [; constants (prove-crate-item-ok DeclProgram ConstDecl) - (where/error (_ (const KindedVarIds WhereClauses Ty FnBody)) ConstDecl) + (where/error (const _ KindedVarIds WhereClauses Ty FnBody) ConstDecl) (✅-FnBody DeclProgram (∀ KindedVarIds (() -> Ty where WhereClauses FnBody))) ---------------------------------------- (✅-CrateItemDecl DeclProgram ConstDecl) @@ -77,7 +77,7 @@ [; statics (prove-crate-item-ok DeclProgram StaticDecl) - (where/error (_ (static KindedVarIds WhereClauses Ty FnBody)) StaticDecl) + (where/error (static _ KindedVarIds WhereClauses Ty FnBody) StaticDecl) (✅-FnBody DeclProgram (∀ KindedVarIds (() -> Ty where WhereClauses FnBody))) ---------------------------------------- (✅-CrateItemDecl DeclProgram StaticDecl) diff --git a/src/mir/test/issue-25860.rkt b/src/mir/test/issue-25860.rkt index 07f94e6a..23dcd828 100644 --- a/src/mir/test/issue-25860.rkt +++ b/src/mir/test/issue-25860.rkt @@ -47,29 +47,29 @@ ;; } ;; } ;; ``` - (StaticDecl_UNIT (term (UNIT (static - () ; generics - () ; where-clauses - (user-ty (& static (& static ()))) ; type - (∃ - ((lifetime L0) - (lifetime L1) - (lifetime L2) - (lifetime L3) - (lifetime L4) + (StaticDecl_UNIT (term (static UNIT + () ; generics + () ; where-clauses + (user-ty (& static (& static ()))) ; type + (∃ + ((lifetime L0) + (lifetime L1) + (lifetime L2) + (lifetime L3) + (lifetime L4) + ) + ([(_0 (user-ty (& L0 (& L1 ()))) mut) + (_1 (user-ty (& L2 ())) mut) + (_2 (user-ty ()) mut) + ] + [(bb0 {(noop + (_1 = (ref L3 () _2)) + (_0 = (ref L4 () _1))) + return + })] + ) ) - ([(_0 (user-ty (& L0 (& L1 ()))) mut) - (_1 (user-ty (& L2 ())) mut) - (_2 (user-ty ()) mut) - ] - [(bb0 {(noop - (_1 = (ref L3 () _2)) - (_0 = (ref L4 () _1))) - return - })] - ) - ) - )))) + ))) ] (traced '() From 37ab22b1b7484747dce7e473915cc6cbbde84886 Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Thu, 2 Jun 2022 20:39:57 -0400 Subject: [PATCH 11/12] move the FnId into FnDecl --- src/decl/decl-ok.rkt | 2 +- src/decl/decl-to-clause.rkt | 2 +- src/decl/grammar.rkt | 3 +-- src/decl/test/fns.rkt | 12 ++++++------ src/mir/all-check.rkt | 2 +- src/mir/test/basic.rkt | 10 +++++----- 6 files changed, 15 insertions(+), 16 deletions(-) diff --git a/src/decl/decl-ok.rkt b/src/decl/decl-ok.rkt index 20713cd9..0bc014ee 100644 --- a/src/decl/decl-ok.rkt +++ b/src/decl/decl-ok.rkt @@ -70,7 +70,7 @@ ;; (well-formed-where-clause-goal (T : Trait_Ord ())))) ;; ;; FIXME: Actually implement that, along with for the other items - (crate-item-ok-goal _ (FnId (fn KindedVarIds Tys_arg Ty_ret (WhereClause ...) FnBody))) + (crate-item-ok-goal _ (fn FnId KindedVarIds Tys_arg Ty_ret (WhereClause ...) FnBody)) (&& ((well-formed-where-clause-goal WhereClause) ...)) ] diff --git a/src/decl/decl-to-clause.rkt b/src/decl/decl-to-clause.rkt index f7e82df3..cff96949 100644 --- a/src/decl/decl-to-clause.rkt +++ b/src/decl/decl-to-clause.rkt @@ -295,7 +295,7 @@ [;; For a function declared in the crate C, like the following ;; ;; fn foo<'a, T>(&'a T) -> &'a T { ... } - (crate-item-decl-rules CrateDecls CrateId (_ (fn KindedVarIds_fn Tys_arg Ty_ret WhereClauses_fn FnBody))) + (crate-item-decl-rules CrateDecls CrateId (fn _ KindedVarIds_fn Tys_arg Ty_ret WhereClauses_fn FnBody)) (() () ()) ] diff --git a/src/decl/grammar.rkt b/src/decl/grammar.rkt index 81ad6c48..a687c53f 100644 --- a/src/decl/grammar.rkt +++ b/src/decl/grammar.rkt @@ -65,8 +65,7 @@ ;; Function ;; ;; fn foo<...>(...) -> ... where ... { body } - (FnDecl ::= (FnId FnContents)) - (FnContents ::= (fn KindedVarIds Tys Ty WhereClauses FnBody)) + (FnDecl ::= (fn FnId KindedVarIds Tys Ty WhereClauses FnBody)) ;; Identifiers -- these are all equivalent, but we give them fresh names to help ;; clarify their purpose diff --git a/src/decl/test/fns.rkt b/src/decl/test/fns.rkt index 8231a4a8..002aae3a 100644 --- a/src/decl/test/fns.rkt +++ b/src/decl/test/fns.rkt @@ -15,12 +15,12 @@ ;; Test that we can write a function ((; fn foo<'a, T>(&'a T) -> &'a T { ... } - FnDecl_foo (term (foo (fn - ((lifetime A) (type T)) - ((rigid-ty (ref ()) (A (rigid-ty T ())))) - (rigid-ty (ref ()) (A (rigid-ty T ()))) - () - dummy-body)))) + FnDecl_foo (term (fn foo + ((lifetime A) (type T)) + ((rigid-ty (ref ()) (A (rigid-ty T ())))) + (rigid-ty (ref ()) (A (rigid-ty T ()))) + () + dummy-body))) (; the crate has a function CrateDecl (term (TheCrate (crate (FnDecl_foo))))) diff --git a/src/mir/all-check.rkt b/src/mir/all-check.rkt index 5601c628..d743baa7 100644 --- a/src/mir/all-check.rkt +++ b/src/mir/all-check.rkt @@ -85,7 +85,7 @@ [; function items (prove-crate-item-ok DeclProgram FnDecl) - (where/error (FnId (fn KindedVarIds Tys Ty WhereClauses FnBody)) FnDecl) + (where/error (fn FnId KindedVarIds Tys Ty WhereClauses FnBody) FnDecl) (✅-FnBody DeclProgram (∀ KindedVarIds (Tys -> Ty where WhereClauses FnBody))) ---------------------------------------- (✅-CrateItemDecl DeclProgram FnDecl) diff --git a/src/mir/test/basic.rkt b/src/mir/test/basic.rkt index a3b03889..4a796e6a 100644 --- a/src/mir/test/basic.rkt +++ b/src/mir/test/basic.rkt @@ -37,11 +37,11 @@ ) ) ))) - (FnDecl_foo (term (foo (fn () - ((user-ty i32) (user-ty i32)) - (user-ty i32) - () - FnBody_foo)))) + (FnDecl_foo (term (fn foo () + ((user-ty i32) (user-ty i32)) + (user-ty i32) + () + FnBody_foo))) (CrateDecl_the-crate (term (the-crate (crate (FnDecl_foo))))) (DeclProgram (term ((CrateDecl_the-crate) the-crate))) ) From d49d1d5f9a12b24e20ed778fb8835c1a1813394e Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Thu, 2 Jun 2022 21:29:31 -0400 Subject: [PATCH 12/12] introduce `where` and other punctuation makes things a lot more readable --- src/decl/decl-ok.rkt | 24 +++++----- src/decl/decl-to-clause.rkt | 10 ++--- src/decl/decl-wf-where-clause.rkt | 2 +- src/decl/grammar.rkt | 44 +++++++++---------- src/decl/test/basic-consts.rkt | 8 ++-- src/decl/test/basic-statics.rkt | 8 ++-- src/decl/test/basic.rkt | 4 +- src/decl/test/coinductive/issue-43784.rkt | 14 +++--- src/decl/test/coinductive/magic-issue-xxx.rkt | 28 ++++++------ src/decl/test/copy.rkt | 14 +++--- src/decl/test/drop.rkt | 40 ++++++++--------- src/decl/test/fns.rkt | 4 +- src/decl/test/implied-bounds.rkt | 10 ++--- src/decl/test/libcore.rkt | 8 ++-- src/decl/test/multi-crate.rkt | 10 ++--- src/decl/test/supertraits.rkt | 11 ++--- src/decl/test/wf-where-clauses.rkt | 28 ++++++------ src/mir/all-check.rkt | 6 +-- src/mir/test/basic.rkt | 6 +-- src/mir/test/issue-25860.rkt | 43 +++++++++--------- src/mir/type-of.rkt | 8 ++-- 21 files changed, 162 insertions(+), 168 deletions(-) diff --git a/src/decl/decl-ok.rkt b/src/decl/decl-ok.rkt index 0bc014ee..f14f448b 100644 --- a/src/decl/decl-ok.rkt +++ b/src/decl/decl-ok.rkt @@ -41,7 +41,7 @@ ;; (implies ((well-formed (type T)) ;; (is-implemented (Ord T))) ;; (well-formed (type Vec)) ...)) - (crate-item-ok-goal CrateDecls (AdtKind AdtId KindedVarIds (WhereClause ...) AdtVariants)) + (crate-item-ok-goal CrateDecls (AdtKind AdtId KindedVarIds where (WhereClause ...) AdtVariants)) Goal_wf (where/error (KindedVarId ...) KindedVarIds) @@ -70,7 +70,7 @@ ;; (well-formed-where-clause-goal (T : Trait_Ord ())))) ;; ;; FIXME: Actually implement that, along with for the other items - (crate-item-ok-goal _ (fn FnId KindedVarIds Tys_arg Ty_ret (WhereClause ...) FnBody)) + (crate-item-ok-goal _ (fn FnId KindedVarIds Tys_arg -> Ty_ret where (WhereClause ...) FnBody)) (&& ((well-formed-where-clause-goal WhereClause) ...)) ] @@ -79,7 +79,7 @@ ;; trait Foo<'a, T> where T: Ord { ... } ;; ;; we require that all the trait-item WF goals are met. - (crate-item-ok-goal CrateDecls (trait TraitId KindedVarIds (WhereClause ...) (TraitItem ...))) + (crate-item-ok-goal CrateDecls (trait TraitId KindedVarIds where (WhereClause ...) (TraitItem ...))) (∀ KindedVarIds (implies ((well-formed KindedVarId) ... (where-clause->hypothesis WhereClause) ...) (&& (Goal_trait-item ... @@ -95,7 +95,7 @@ ;; ;; we require that the trait is implemented, given that all generics are WF, ;; all inputs are WF, and where-clauses are satisfied. - (crate-item-ok-goal CrateDecls (impl KindedVarIds_impl (TraitId (Parameter_trait ...)) WhereClauses_impl ImplItems)) + (crate-item-ok-goal CrateDecls (impl KindedVarIds_impl (TraitId (Parameter_trait ...)) where WhereClauses_impl ImplItems)) (∀ KindedVarIds_impl (implies (; assuming all generic parameters are WF... @@ -108,7 +108,7 @@ is-implemented (TraitId (Parameter_trait ...))) (well-formed-where-clause-goal CrateDecls WhereClause_impl) ...)))) - (where/error (trait TraitId ((ParameterKind_trait _) ...) _ _) (trait-with-id CrateDecls TraitId)) + (where/error (trait TraitId ((ParameterKind_trait _) ...) where _ _) (trait-with-id CrateDecls TraitId)) (where/error (KindedVarId_impl ...) KindedVarIds_impl) (where/error (WhereClause_impl ...) WhereClauses_impl) ] @@ -118,7 +118,7 @@ ;; const NAMED: Foo where T: Trait; ;; ;; we require that the type is well formed assuming the where clauses are satisfied. - (crate-item-ok-goal CrateDecls (const ConstId KindedVarIds WhereClauses Ty FnBody)) + (crate-item-ok-goal CrateDecls (const ConstId KindedVarIds where WhereClauses : Ty = FnBody)) (∀ KindedVarIds (implies (; assuming all generic parameters are WF... @@ -139,7 +139,7 @@ ;; ;; we require that the type is well formed assuming the where clauses are satisfied ;; and that the type is `Send`. - (crate-item-ok-goal CrateDecls (static StaticId KindedVarIds WhereClauses Ty FnBody)) + (crate-item-ok-goal CrateDecls (static StaticId KindedVarIds where WhereClauses : Ty = FnBody)) (∀ KindedVarIds (implies (; assuming all generic parameters are WF... @@ -198,7 +198,7 @@ ; ; when this goal is given to the solver, it would be rejected because `T: Eq` is not provable ; (we only know that `T: Debug`). - (lang-item-ok-goals CrateDecls (impl KindedVarIds_impl (rust:Drop (Ty_impl)) (WhereClause_impl ...) _)) + (lang-item-ok-goals CrateDecls (impl KindedVarIds_impl (rust:Drop (Ty_impl)) where (WhereClause_impl ...) _)) ((∀ KindedVarIds_adt (implies (where-clauses->hypotheses WhereClauses_adt) (∃ KindedVarIds_impl @@ -208,13 +208,13 @@ )))) (where (rigid-ty AdtId Parameters) Ty_impl) - (where (AdtKind AdtId KindedVarIds_adt WhereClauses_adt _) (adt-with-id CrateDecls AdtId)) + (where (AdtKind AdtId KindedVarIds_adt where WhereClauses_adt _) (adt-with-id CrateDecls AdtId)) (where/error ((ParameterKind_adt VarId_adt) ...) KindedVarIds_adt) (where/error Ty_adt (rigid-ty AdtId (VarId_adt ...))) ] [; Impl of the Drop trait for something that is not an ADT -- always an error. - (lang-item-ok-goals CrateDecls (impl KindedVarIds_impl (rust:Drop (_ ...)) WhereClauses_impl _)) + (lang-item-ok-goals CrateDecls (impl KindedVarIds_impl (rust:Drop (_ ...)) where WhereClauses_impl _)) ((|| ())) ; unprovable goal ] @@ -239,7 +239,7 @@ ; (is-implemented (Vec: Copy))) ; ; of course, in this case, it is not provable because `Vec: Copy` is not true for any `T`. - (lang-item-ok-goals CrateDecls (impl KindedVarIds_impl (rust:Copy (Ty_impl)) (WhereClause_impl ...) ())) + (lang-item-ok-goals CrateDecls (impl KindedVarIds_impl (rust:Copy (Ty_impl)) where (WhereClause_impl ...) ())) ((∀ KindedVarIds_impl (implies ((where-clause->hypothesis WhereClause_impl) ...) (∃ KindedVarIds_adt @@ -249,7 +249,7 @@ ))))) (where (rigid-ty AdtId Parameters) Ty_impl) - (where (AdtKind AdtId KindedVarIds_adt _ AdtVariants) (adt-with-id CrateDecls AdtId)) + (where (AdtKind AdtId KindedVarIds_adt where _ AdtVariants) (adt-with-id CrateDecls AdtId)) (where/error ((ParameterKind_adt VarId_adt) ...) KindedVarIds_adt) (where/error Ty_adt (rigid-ty AdtId (VarId_adt ...))) (where/error ((VariantId ((FieldId Ty_field) ...)) ...) AdtVariants) diff --git a/src/decl/decl-to-clause.rkt b/src/decl/decl-to-clause.rkt index cff96949..2d4ce361 100644 --- a/src/decl/decl-to-clause.rkt +++ b/src/decl/decl-to-clause.rkt @@ -176,7 +176,7 @@ ;; ;; (∀ ((type T)) ;; (well-formed (type (Foo (T)))) => (well-formed (type T))) - (crate-item-decl-rules CrateDecls CrateId (AdtKind AdtId KindedVarIds (WhereClause ...) AdtVariants)) + (crate-item-decl-rules CrateDecls CrateId (AdtKind AdtId KindedVarIds where (WhereClause ...) AdtVariants)) ((Clause) Invariants_wf Invariants_wc) (where/error ((ParameterKind VarId) ...) KindedVarIds) @@ -222,7 +222,7 @@ ;; (is-implemented (Foo (Self 'a T))) => (well-formed (type Self)) ;; (is-implemented (Foo (Self 'a T))) => (well-formed (lifetime 'a)) ;; (is-implemented (Foo (Self 'a T))) => (well-formed (type T))) - (crate-item-decl-rules CrateDecls CrateId (trait TraitId KindedVarIds (WhereClause ...) TraitItems)) + (crate-item-decl-rules CrateDecls CrateId (trait TraitId KindedVarIds where (WhereClause ...) TraitItems)) ((Clause) (Invariant_wc ... Invariant_wf ... @@ -277,11 +277,11 @@ ;; (well-formed (type i32)) ;; (well-formed (lifetime 'a)) ;; (is-implemented (Ord T))) - (crate-item-decl-rules CrateDecls CrateId (impl KindedVarIds_impl TraitRef WhereClauses_impl ImplItems)) + (crate-item-decl-rules CrateDecls CrateId (impl KindedVarIds_impl TraitRef where WhereClauses_impl ImplItems)) ((Clause) () ()) (where/error (TraitId (Parameter_trait ...)) TraitRef) - (where/error (trait TraitId KindedVarIds_trait _ _) (trait-with-id CrateDecls TraitId)) + (where/error (trait TraitId KindedVarIds_trait where _ _) (trait-with-id CrateDecls TraitId)) (where/error ((ParameterKind_trait _) ...) KindedVarIds_trait) (where/error (Goal_wc ...) (where-clauses->goals WhereClauses_impl)) (where/error Clause (∀ KindedVarIds_impl @@ -295,7 +295,7 @@ [;; For a function declared in the crate C, like the following ;; ;; fn foo<'a, T>(&'a T) -> &'a T { ... } - (crate-item-decl-rules CrateDecls CrateId (fn _ KindedVarIds_fn Tys_arg Ty_ret WhereClauses_fn FnBody)) + (crate-item-decl-rules CrateDecls CrateId (fn _ KindedVarIds_fn Tys_arg -> Ty_ret where WhereClauses_fn FnBody)) (() () ()) ] diff --git a/src/decl/decl-wf-where-clause.rkt b/src/decl/decl-wf-where-clause.rkt index 047e6821..ab25edfe 100644 --- a/src/decl/decl-wf-where-clause.rkt +++ b/src/decl/decl-wf-where-clause.rkt @@ -40,7 +40,7 @@ ; ; * in our example above `(ParameterKind VarId) ...` would match `((type Self) (type T))` ; * and `WhereClauses` would be `(T : Bar ())` - (where/error (trait TraitId ((ParameterKind VarId) ...) WhereClauses _) (trait-with-id CrateDecls TraitId)) + (where/error (trait TraitId ((ParameterKind VarId) ...) where WhereClauses _) (trait-with-id CrateDecls TraitId)) ; create a substitution ((Self => A) (T => B)) (where/error (Parameter_value ...) (Ty Parameter ...)) diff --git a/src/decl/grammar.rkt b/src/decl/grammar.rkt index a687c53f..aa4ac5b2 100644 --- a/src/decl/grammar.rkt +++ b/src/decl/grammar.rkt @@ -27,7 +27,7 @@ (FeatureDecl ::= (feature FeatureId)) ;; AdtDecl -- struct/enum/union declarations - (AdtDecl ::= (AdtKind AdtId KindedVarIds WhereClauses AdtVariants)) + (AdtDecl ::= (AdtKind AdtId KindedVarIds where WhereClauses AdtVariants)) (AdtVariants ::= (AdtVariant ...)) (AdtKind ::= struct enum union) (AdtVariant ::= (VariantId FieldDecls)) @@ -40,7 +40,7 @@ ;; TraitDecl -- trait Foo { ... } ;; ;; Unlike in Rust, the `KindedVarIds` here always include with `(type Self)` explicitly. - (TraitDecl ::= (trait TraitId KindedVarIds WhereClauses TraitItems)) + (TraitDecl ::= (trait TraitId KindedVarIds where WhereClauses TraitItems)) ;; TraitItem -- (TraitItems ::= (TraitItem ...)) @@ -49,13 +49,13 @@ ;; Trait impls ;; ;; Note that trait impls do not have names. - (TraitImplDecl ::= (impl KindedVarIds TraitRef WhereClauses ImplItems)) + (TraitImplDecl ::= (impl KindedVarIds TraitRef where WhereClauses ImplItems)) ;; Named statics - (StaticDecl ::= (static StaticId KindedVarIds WhereClauses Ty FnBody)) + (StaticDecl ::= (static StaticId KindedVarIds where WhereClauses : Ty = FnBody)) ;; Named constants - (ConstDecl ::= (const ConstId KindedVarIds WhereClauses Ty FnBody)) + (ConstDecl ::= (const ConstId KindedVarIds where WhereClauses : Ty = FnBody)) ;; ImplItem -- (ImplItems ::= (ImplItem ...)) @@ -65,7 +65,7 @@ ;; Function ;; ;; fn foo<...>(...) -> ... where ... { body } - (FnDecl ::= (fn FnId KindedVarIds Tys Ty WhereClauses FnBody)) + (FnDecl ::= (fn FnId KindedVarIds Tys -> Ty where WhereClauses FnBody)) ;; Identifiers -- these are all equivalent, but we give them fresh names to help ;; clarify their purpose @@ -81,31 +81,31 @@ #:binding-forms (AdtKind AdtKind ((ParameterKind VarId) ...) - WhereClauses #:refers-to (shadow VarId ...) + where WhereClauses #:refers-to (shadow VarId ...) AdtVariants #:refers-to (shadow VarId ...)) (trait TraitId ((ParameterKind VarId) ...) - WhereClauses #:refers-to (shadow VarId ...) + where WhereClauses #:refers-to (shadow VarId ...) TraitItems #:refers-to (shadow VarId ...)) (impl ((ParameterKind VarId) ...) TraitRef #:refers-to (shadow VarId ...) - WhereClauses #:refers-to (shadow VarId ...) + where WhereClauses #:refers-to (shadow VarId ...) ImplItems #:refers-to (shadow VarId ...)) (const ConstId ((ParameterKind VarId) ...) - WhereClauses #:refers-to (shadow VarId ...) - Ty #:refers-to (shadow VarId ...) - FnBody #:refers-to (shadow VarId ...)) + where WhereClauses #:refers-to (shadow VarId ...) + : Ty #:refers-to (shadow VarId ...) + = FnBody #:refers-to (shadow VarId ...)) (static StaticId ((ParameterKind VarId) ...) - WhereClauses #:refers-to (shadow VarId ...) - Ty #:refers-to (shadow VarId ...) - FnBody #:refers-to (shadow VarId ...)) + where WhereClauses #:refers-to (shadow VarId ...) + : Ty #:refers-to (shadow VarId ...) + = FnBody #:refers-to (shadow VarId ...)) (fn FnId ((ParameterKind VarId) ...) Tys #:refers-to (shadow VarId ...) - Ty #:refers-to (shadow VarId ...) - WhereClauses #:refers-to (shadow VarId ...) + -> Ty #:refers-to (shadow VarId ...) + where WhereClauses #:refers-to (shadow VarId ...) FnBody #:refers-to (shadow VarId ...)) ) @@ -131,7 +131,7 @@ (define-metafunction formality-decl trait-decl-id : TraitDecl -> TraitId - ((trait-decl-id (trait TraitId _ _ _)) TraitId) + ((trait-decl-id (trait TraitId _ where _ _)) TraitId) ) (define-metafunction formality-decl @@ -139,10 +139,10 @@ adt-with-id : CrateDecls AdtId -> AdtDecl [(adt-with-id CrateDecls AdtId) - (AdtKind AdtId KindedVarIds WhereClauses AdtVariants) + (AdtKind AdtId KindedVarIds where WhereClauses AdtVariants) (where (_ ... CrateDecl _ ...) CrateDecls) - (where (_ (crate (_ ... (AdtKind AdtId KindedVarIds WhereClauses AdtVariants) _ ...))) CrateDecl) + (where (_ (crate (_ ... (AdtKind AdtId KindedVarIds where WhereClauses AdtVariants) _ ...))) CrateDecl) ] ) @@ -151,9 +151,9 @@ trait-with-id : CrateDecls TraitId -> TraitDecl [(trait-with-id CrateDecls TraitId) - (trait TraitId KindedVarIds WhereClauses TraitItems) + (trait TraitId KindedVarIds where WhereClauses TraitItems) (where (_ ... CrateDecl _ ...) CrateDecls) - (where (_ (crate (_ ... (trait TraitId KindedVarIds WhereClauses TraitItems) _ ...))) CrateDecl) + (where (_ (crate (_ ... (trait TraitId KindedVarIds where WhereClauses TraitItems) _ ...))) CrateDecl) ] ) diff --git a/src/decl/test/basic-consts.rkt b/src/decl/test/basic-consts.rkt index 28b201d0..a37d5775 100644 --- a/src/decl/test/basic-consts.rkt +++ b/src/decl/test/basic-consts.rkt @@ -11,9 +11,9 @@ formality-decl [(; trait Debug { } - TraitDecl (term (trait Debug ((type Self)) () ()))) + TraitDecl (term (trait Debug ((type Self)) where () ()))) (; struct Foo { } - AdtDecl_Foo (term (struct Foo ((type T)) ((T : Debug())) ((Foo ()))))) + AdtDecl_Foo (term (struct Foo ((type T)) where ((T : Debug())) ((Foo ()))))) ] (; test that WF checks fail if `T: Debug` is missing @@ -21,7 +21,7 @@ formality-decl [ (; const BROKEN: Foo; - ConstDecl_broken (term (const BROKEN ((type T)) () (rigid-ty Foo (T)) dummy-body))) + ConstDecl_broken (term (const BROKEN ((type T)) where () : (user-ty (Foo T)) = dummy-body))) (CrateDecl (term (TheCrate (crate (TraitDecl AdtDecl_Foo ConstDecl_broken))))) ] @@ -34,7 +34,7 @@ formality-decl [ (; const OK: Foo; - ConstDecl_ok (term (const OK ((type T)) ((T : Debug())) (rigid-ty Foo (T)) dummy-body))) + ConstDecl_ok (term (const OK ((type T)) where ((T : Debug())) : (user-ty (Foo T)) = dummy-body))) (CrateDecl (term (TheCrate (crate (TraitDecl AdtDecl_Foo ConstDecl_ok))))) ] diff --git a/src/decl/test/basic-statics.rkt b/src/decl/test/basic-statics.rkt index d3c425b8..a9f53673 100644 --- a/src/decl/test/basic-statics.rkt +++ b/src/decl/test/basic-statics.rkt @@ -11,7 +11,7 @@ formality-decl [(; struct Foo { } - AdtDecl_Foo (term (struct Foo () () ((Foo ()))))) + AdtDecl_Foo (term (struct Foo () where () ((Foo ()))))) ] (; test that Send check fails @@ -20,7 +20,7 @@ redex-let* formality-decl [(; static S: Foo; - StaticDecl (term (static S () () (rigid-ty Foo ()) fn-body))) + StaticDecl (term (static S () where () : (rigid-ty Foo ()) = fn-body))) (CrateDecl (term (TheCrate (crate (AdtDecl_Foo StaticDecl))))) ] @@ -36,9 +36,9 @@ redex-let* formality-decl [(; static S: Foo; - StaticDecl (term (static S () () (rigid-ty Foo ()) dummy-body))) + StaticDecl (term (static S () where () : (rigid-ty Foo ()) = dummy-body))) (; impl Send for Foo - TraitImplDecl_Sync (term (impl ((type T)) (rust:Sync ((rigid-ty Foo ()))) () ()))) + TraitImplDecl_Sync (term (impl ((type T)) (rust:Sync ((rigid-ty Foo ()))) where () ()))) (CrateDecl (term (TheCrate (crate (AdtDecl_Foo StaticDecl TraitImplDecl_Sync))))) ] diff --git a/src/decl/test/basic.rkt b/src/decl/test/basic.rkt index 62877364..53f1ed43 100644 --- a/src/decl/test/basic.rkt +++ b/src/decl/test/basic.rkt @@ -14,8 +14,8 @@ (redex-let* formality-decl - ((TraitDecl (term (trait Debug ((type Self)) () ()))) - (TraitImplDecl (term (impl () (Debug ((user-ty i32))) () ()))) + ((TraitDecl (term (trait Debug ((type Self)) where () {}))) + (TraitImplDecl (term (impl () (Debug ((user-ty i32))) where () {}))) (CrateDecl (term (TheCrate (crate (TraitDecl TraitImplDecl))))) (Env (term (env-for-crate-decl CrateDecl))) ) diff --git a/src/decl/test/coinductive/issue-43784.rkt b/src/decl/test/coinductive/issue-43784.rkt index bf8ff4b7..1f126f2f 100644 --- a/src/decl/test/coinductive/issue-43784.rkt +++ b/src/decl/test/coinductive/issue-43784.rkt @@ -11,25 +11,25 @@ formality-decl [(; struct Foo { } - AdtDecl_Foo (term (struct Foo () () ((struct-variant ()))))) + AdtDecl_Foo (term (struct Foo () where () ((struct-variant ()))))) (; trait Copy { } - TraitDecl_Copy (term (trait Copy ((type Self)) () ()))) + TraitDecl_Copy (term (trait Copy ((type Self)) where () ()))) (; trait Partial: Copy { } - TraitDecl_Partial (term (trait Partial((type Self)) ((Self : Copy())) ()))) + TraitDecl_Partial (term (trait Partial((type Self)) where ((Self : Copy())) ()))) (; trait Complete: Partial { } - TraitDecl_Complete (term (trait Complete ((type Self)) ((Self : Partial())) ()))) + TraitDecl_Complete (term (trait Complete ((type Self)) where ((Self : Partial())) ()))) (; impl Partial for T where T: Complete {} - TraitImplDecl_Partial (term (impl ((type T)) (Partial (T)) ((T : Complete())) ()))) + TraitImplDecl_Partial (term (impl ((type T)) (Partial (T)) where ((T : Complete())) ()))) (; impl Complete for T {} - TraitImplDecl_CompleteA (term (impl ((type T)) (Complete (T)) () ()))) + TraitImplDecl_CompleteA (term (impl ((type T)) (Complete (T)) where () ()))) (; impl Complete for T {} - TraitImplDecl_CompleteB (term (impl ((type T)) (Complete (T)) ((T : Partial())) ()))) + TraitImplDecl_CompleteB (term (impl ((type T)) (Complete (T)) where ((T : Partial())) ()))) (; crate A { ... } CrateDecl_A (term (A (crate (AdtDecl_Foo diff --git a/src/decl/test/coinductive/magic-issue-xxx.rkt b/src/decl/test/coinductive/magic-issue-xxx.rkt index 0f3dca32..f03ab8e0 100644 --- a/src/decl/test/coinductive/magic-issue-xxx.rkt +++ b/src/decl/test/coinductive/magic-issue-xxx.rkt @@ -14,19 +14,19 @@ formality-decl [(; struct Foo { counter: i32 } - AdtDecl_Foo (term (struct Foo () () ((struct-variant ((counter (user-ty i32)))))))) + AdtDecl_Foo (term (struct Foo () where () ((struct-variant ((counter (user-ty i32)))))))) (; reference to `Foo` Ty_Foo (term (rigid-ty Foo ()))) (; trait Magic: Copy { } - TraitDecl_Magic (term (trait Magic ((type Self)) ((Self : Copy())) ()))) + TraitDecl_Magic (term (trait Magic ((type Self)) where ((Self : Copy())) ()))) (; trait Copy { } - TraitDecl_Copy (term (trait Copy ((type Self)) () ()))) + TraitDecl_Copy (term (trait Copy ((type Self)) where () ()))) (; impl Magic for T where T: Magic { } - TraitImplDecl_Magic (term (impl ((type T)) (Magic (T)) ((T : Magic())) ()))) + TraitImplDecl_Magic (term (impl ((type T)) (Magic (T)) where ((T : Magic())) ()))) (; crate TheCrate { ... } CrateDecl (term (TheCrate (crate (TraitDecl_Magic TraitDecl_Copy TraitImplDecl_Magic))))) @@ -61,19 +61,19 @@ formality-decl [(; struct Foo { counter: i32 } - AdtDecl_Foo (term (struct Foo () () ((struct-variant ((counter (user-ty i32)))))))) + AdtDecl_Foo (term (struct Foo () where () ((struct-variant ((counter (user-ty i32)))))))) (; reference to `Foo` Ty_Foo (term (rigid-ty Foo ()))) (; trait Magic: Copy { } - TraitDecl_Magic (term (trait Magic ((type Self)) ((Self : Copy())) ()))) + TraitDecl_Magic (term (trait Magic ((type Self)) where ((Self : Copy())) {}))) (; trait Copy: Magic { } - TraitDecl_Copy (term (trait Copy ((type Self)) ((Self : Magic())) ()))) + TraitDecl_Copy (term (trait Copy ((type Self)) where ((Self : Magic())) {}))) (; impl Magic for T where T: Magic { } - TraitImplDecl_Magic (term (impl ((type T)) (Magic (T)) ((T : Magic())) ()))) + TraitImplDecl_Magic (term (impl ((type T)) (Magic (T)) where ((T : Magic())) {}))) (; crate TheCrate { ... } CrateDecl (term (TheCrate (crate (TraitDecl_Magic TraitDecl_Copy TraitImplDecl_Magic))))) @@ -107,28 +107,28 @@ formality-decl ((; struct Foo { counter: i32 } - AdtDecl_Foo (term (struct Foo () () ((struct-variant ((counter (user-ty i32)))))))) + AdtDecl_Foo (term (struct Foo () where () ((struct-variant ((counter (user-ty i32)))))))) (; reference to `Foo` Ty_Foo (term (rigid-ty Foo ()))) (; struct Bar { counter: i32 } - AdtDecl_Foo (term (struct Foo () () ((struct-variant ((counter (user-ty i32)))))))) + AdtDecl_Foo (term (struct Foo () where () ((struct-variant ((counter (user-ty i32)))))))) (; reference to `Bar` Ty_Bar (term (rigid-ty Bar ()))) (; trait Magic: Copy { } - TraitDecl_Magic (term (trait Magic ((type Self)) ((Self : Copy())) ()))) + TraitDecl_Magic (term (trait Magic ((type Self)) where ((Self : Copy())) {}))) (; trait Copy { } - TraitDecl_Copy (term (trait Copy ((type Self)) () ()))) + TraitDecl_Copy (term (trait Copy ((type Self)) where () {}))) (; impl Magic for T where T: Magic { } - TraitImplDecl_Magic (term (impl ((type T)) (Magic (T)) ((T : Magic())) ()))) + TraitImplDecl_Magic (term (impl ((type T)) (Magic (T)) where ((T : Magic())) {}))) (; impl Copy for Foo { } - TraitImplDecl_Copy (term (impl () (Copy (Ty_Foo)) () ()))) + TraitImplDecl_Copy (term (impl () (Copy (Ty_Foo)) where () {}))) (; crate TheCrate { ... } CrateDecl (term (TheCrate (crate (TraitDecl_Magic TraitDecl_Copy TraitImplDecl_Magic))))) diff --git a/src/decl/test/copy.rkt b/src/decl/test/copy.rkt index c47d8e8f..2a1c35b2 100644 --- a/src/decl/test/copy.rkt +++ b/src/decl/test/copy.rkt @@ -16,10 +16,10 @@ ;; Test for that `impl Copy for i32` is permitted. ((; trait rust:Copy { _: Foo } - TraitDecl_Copy (term (trait rust:Copy ((type Self)) () ()))) + TraitDecl_Copy (term (trait rust:Copy ((type Self)) where () ()))) (; impl rust:Copy for i32 { } - TraitImplDecl (term (impl () (rust:Copy ((user-ty i32))) () ()))) + TraitImplDecl (term (impl () (rust:Copy ((user-ty i32))) where () ()))) (; the crate has the struct, the trait, and the impl CrateDecl (term (TheCrate (crate (TraitDecl_Copy @@ -44,25 +44,25 @@ ;; because `Foo: Copy` does not hold. [(; trait rust:Copy { } - TraitDecl_Copy (term (trait rust:Copy ((type Self)) () ()))) + TraitDecl_Copy (term (trait rust:Copy ((type Self)) where () ()))) (; struct Foo { } AdtDecl_Foo (term (struct Foo () ; no generic parameters - () ; no where clauses + where () ; no where clauses ((Foo ())) ; the 1 variant (named `Foo`) ))) (; struct Bar { _: Foo } AdtDecl_Bar (term (struct Bar () ; no generic parameters - () ; no where clauses + where () ; no where clauses ((Bar ((f (rigid-ty Foo ())) ))) ; the 1 variant (named `Foo`) ))) (; impl rust:Copy for Bar { } - TraitImplDecl (term (impl () (rust:Copy ((rigid-ty Bar ()))) () ()))) + TraitImplDecl (term (impl () (rust:Copy ((rigid-ty Bar ()))) where () ()))) (; the crate has the struct, the trait, and the impl CrateDecl (term (TheCrate (crate (TraitDecl_Copy @@ -85,7 +85,7 @@ (redex-let* formality-decl [(; impl rust:Copy for Foo { } - TraitImplDecl_Foo (term (impl () (rust:Copy ((rigid-ty Foo ()))) () ()))) + TraitImplDecl_Foo (term (impl () (rust:Copy ((rigid-ty Foo ()))) where () ()))) (; the crate has the struct, the trait, and the impl CrateDecl_Pass (term (TheCrate (crate (TraitDecl_Copy diff --git a/src/decl/test/drop.rkt b/src/decl/test/drop.rkt index db38c9b5..6c091280 100644 --- a/src/decl/test/drop.rkt +++ b/src/decl/test/drop.rkt @@ -16,10 +16,10 @@ ;; Test for that `impl Drop for i32` is not permitted. [(; trait rust:Drop { } - TraitDecl_Drop (term (trait rust:Drop ((type Self)) () ()))) + TraitDecl_Drop (term (trait rust:Drop ((type Self)) where () ()))) (; impl rust:Drop for i32 { } - TraitImplDecl (term (impl () (rust:Drop ((user-ty i32))) () ()))) + TraitImplDecl (term (impl () (rust:Drop ((user-ty i32))) where () ()))) (; the crate has the struct, the trait, and the impl CrateDecl (term (TheCrate (crate (TraitDecl_Drop @@ -43,15 +43,15 @@ ;; Test for case where the Drop impl is for `Foo` only. [(; struct Foo { } - AdtDecl_Foo (term (struct Foo ((type T)) () + AdtDecl_Foo (term (struct Foo ((type T)) where () ((Foo ())) ; the 1 variant (named `Foo`) ))) (; trait rust:Drop { } - TraitDecl_Drop (term (trait rust:Drop ((type Self)) () ()))) + TraitDecl_Drop (term (trait rust:Drop ((type Self)) where () ()))) (; impl rust:Drop for Foo { } //~ ERROR - TraitImplDecl (term (impl () (rust:Drop ((rigid-ty Foo ((user-ty i32))))) () ()))) + TraitImplDecl (term (impl () (rust:Drop ((rigid-ty Foo ((user-ty i32))))) where () ()))) (; the crate has the struct, the trait, and the impl CrateDecl (term (TheCrate (crate (AdtDecl_Foo @@ -77,18 +77,18 @@ ;; that doesn't follow from the struct. [(; struct Foo { } - AdtDecl_Foo (term (struct Foo ((type T)) () + AdtDecl_Foo (term (struct Foo ((type T)) where () ((Foo ())) ; the 1 variant (named `Foo`) ))) (; trait Debug { } - TraitDecl_Debug (term (trait Debug ((type Self)) () ()))) + TraitDecl_Debug (term (trait Debug ((type Self)) where () ()))) (; trait rust:Drop { } - TraitDecl_Drop (term (trait rust:Drop ((type Self)) () ()))) + TraitDecl_Drop (term (trait rust:Drop ((type Self)) where () ()))) (; impl rust:Drop for Foo where U: Debug { } //~ ERROR - TraitImplDecl (term (impl ((type U)) (rust:Drop ((rigid-ty Foo (U)))) ((U : Debug())) ()))) + TraitImplDecl (term (impl ((type U)) (rust:Drop ((rigid-ty Foo (U)))) where ((U : Debug())) ()))) (; the crate has the struct, the trait, and the impl CrateDecl (term (TheCrate (crate (AdtDecl_Foo @@ -109,15 +109,15 @@ ;; the predicates on the struct. [(; struct Foo { } - AdtDecl_Foo (term (struct Foo ((type T)) () + AdtDecl_Foo (term (struct Foo ((type T)) where () ((Foo ())) ; the 1 variant (named `Foo`) ))) (; trait rust:Drop { } - TraitDecl_Drop (term (trait rust:Drop ((type Self)) () ()))) + TraitDecl_Drop (term (trait rust:Drop ((type Self)) where () {}))) (; impl rust:Drop for Foo { } - TraitImplDecl (term (impl ((type U)) (rust:Drop ((rigid-ty Foo (U)))) () ()))) + TraitImplDecl (term (impl ((type U)) (rust:Drop ((rigid-ty Foo (U)))) where () {}))) (; the crate has the struct, the trait, and the impl CrateDecl (term (TheCrate (crate (AdtDecl_Foo @@ -144,26 +144,26 @@ ;; the predicates on the struct. [(; struct Foo where T: Ord { } - AdtDecl_Foo (term (struct Foo ((type T)) ((T : Ord())) + AdtDecl_Foo (term (struct Foo ((type T)) where ((T : Ord())) ((Foo ())) ; the 1 variant (named `Foo`) ))) (; trait rust:Drop { } - TraitDecl_Drop (term (trait rust:Drop ((type Self)) () ()))) + TraitDecl_Drop (term (trait rust:Drop ((type Self)) where () {}))) (; trait Eq { } - TraitDecl_Eq (term (trait Eq ((type Self)) () ()))) + TraitDecl_Eq (term (trait Eq ((type Self)) where () {}))) (; trait Ord: Eq { } - TraitDecl_Ord (term (trait Ord ((type Self)) ((Self : Eq())) ()))) + TraitDecl_Ord (term (trait Ord ((type Self)) where ((Self : Eq())) {}))) (; impl rust:Drop for Foo where T: Ord + Eq { } TraitImplDecl (term (impl ((type U)) (rust:Drop ((rigid-ty Foo (U)))) - ((U : Ord()) - (U : Eq()) - ) - ()))) + where ((U : Ord()) + (U : Eq()) + ) + {}))) (; the crate has the struct, the trait, and the impl CrateDecl (term (TheCrate (crate (AdtDecl_Foo diff --git a/src/decl/test/fns.rkt b/src/decl/test/fns.rkt index 002aae3a..71a94dc3 100644 --- a/src/decl/test/fns.rkt +++ b/src/decl/test/fns.rkt @@ -18,8 +18,8 @@ FnDecl_foo (term (fn foo ((lifetime A) (type T)) ((rigid-ty (ref ()) (A (rigid-ty T ())))) - (rigid-ty (ref ()) (A (rigid-ty T ()))) - () + -> (rigid-ty (ref ()) (A (rigid-ty T ()))) + where () dummy-body))) (; the crate has a function diff --git a/src/decl/test/implied-bounds.rkt b/src/decl/test/implied-bounds.rkt index 3350632d..56a698da 100644 --- a/src/decl/test/implied-bounds.rkt +++ b/src/decl/test/implied-bounds.rkt @@ -15,11 +15,11 @@ ((; trait Foo where Self: Bar, T: Bar { } TraitDecl_Foo (term (trait Foo ((type Self) (type T)) - ((T : Bar()) (Self : Bar())) - ()))) + where ((T : Bar()) (Self : Bar())) + {}))) (; trait Bar { } - TraitDecl_Bar (term (trait Bar ((type Self)) () ()))) + TraitDecl_Bar (term (trait Bar ((type Self)) where () {}))) (Env (term (env-for-crate-decl (C (crate (TraitDecl_Foo TraitDecl_Bar)))))) @@ -62,8 +62,8 @@ ((; trait Foo<'l, T> where Self: 'a, T: 'a { } TraitDecl_Foo (term (trait Foo ((type Self) (lifetime l) (type T)) - ((T : l) (Self : l)) - ()))) + where ((T : l) (Self : l)) + {}))) (Env (term (env-for-crate-decl (C (crate (TraitDecl_Foo)))))) diff --git a/src/decl/test/libcore.rkt b/src/decl/test/libcore.rkt index 85ce1b60..82317ec7 100644 --- a/src/decl/test/libcore.rkt +++ b/src/decl/test/libcore.rkt @@ -11,10 +11,10 @@ ,(redex-let* formality-decl [ - (TraitDecl_Send (term (trait rust:Send ((type Self)) () ()))) - (TraitDecl_Sync (term (trait rust:Sync ((type Self)) () ()))) - (TraitDecl_Copy (term (trait rust:Copy ((type Self)) () ()))) - (TraitDecl_Drop (term (trait rust:Drop ((type Self)) () ()))) + (TraitDecl_Send (term (trait rust:Send ((type Self)) where () {}))) + (TraitDecl_Sync (term (trait rust:Sync ((type Self)) where () {}))) + (TraitDecl_Copy (term (trait rust:Copy ((type Self)) where () {}))) + (TraitDecl_Drop (term (trait rust:Drop ((type Self)) where () {}))) (CrateDecl_core (term (core (crate (TraitDecl_Send TraitDecl_Sync TraitDecl_Copy diff --git a/src/decl/test/multi-crate.rkt b/src/decl/test/multi-crate.rkt index e87a0a69..0292c614 100644 --- a/src/decl/test/multi-crate.rkt +++ b/src/decl/test/multi-crate.rkt @@ -18,8 +18,8 @@ ;; CrateDecl_A (redex-let* formality-decl - ((TraitDecl (term (trait Debug ((type Self)) () ()))) - (TraitImplDecl (term (impl () (Debug ((user-ty i32))) () ()))) + ((TraitDecl (term (trait Debug ((type Self)) where () {}))) + (TraitImplDecl (term (impl () (Debug ((user-ty i32))) where () {}))) ) (term (CrateA (crate (TraitDecl TraitImplDecl)))))) @@ -32,9 +32,9 @@ ;; CrateDecl_B (redex-let* formality-decl - ((TraitDecl_WithDebug (term (trait WithDebug ((type Self) (type T)) ((T : Debug())) ()))) - (AdtDecl_Foo (term (struct Foo ((type T)) ((T : Debug())) ((Foo ()))))) - (TraitImplDecl (term (impl ((type T)) (WithDebug ((rigid-ty Foo (T)) T)) () ()))) + ((TraitDecl_WithDebug (term (trait WithDebug ((type Self) (type T)) where ((T : Debug())) {}))) + (AdtDecl_Foo (term (struct Foo ((type T)) where ((T : Debug())) ((Foo ()))))) + (TraitImplDecl (term (impl ((type T)) (WithDebug ((rigid-ty Foo (T)) T)) where () ()))) ) (term (CrateB (crate (TraitDecl_WithDebug AdtDecl_Foo TraitImplDecl)))))) diff --git a/src/decl/test/supertraits.rkt b/src/decl/test/supertraits.rkt index 28d8511f..3ab2beea 100644 --- a/src/decl/test/supertraits.rkt +++ b/src/decl/test/supertraits.rkt @@ -14,14 +14,11 @@ (redex-let* formality-decl - ((TraitDecl_PartialEq (term (trait PartialEq ((type Self)) - () - () - ))) + ((TraitDecl_PartialEq (term (trait PartialEq ((type Self)) where () {}))) (TraitDecl_Eq (term (trait Eq ((type Self)) - ((Self : PartialEq())) - ()))) - (TraitDecl_Debug (term (trait Debug ((type Self)) () ()))) + where ((Self : PartialEq())) + {}))) + (TraitDecl_Debug (term (trait Debug ((type Self)) where () {}))) (CrateDecl (term (TheCrate (crate (TraitDecl_PartialEq TraitDecl_Eq))))) (Env (term (env-for-crate-decl CrateDecl))) ) diff --git a/src/decl/test/wf-where-clauses.rkt b/src/decl/test/wf-where-clauses.rkt index cd26ffbe..e1c6fc5a 100644 --- a/src/decl/test/wf-where-clauses.rkt +++ b/src/decl/test/wf-where-clauses.rkt @@ -15,10 +15,10 @@ formality-decl ((; trait Foo where T: Bar { } - TraitDecl_Foo (term (trait Foo ((type Self) (type T)) ((T : Bar())) ()))) + TraitDecl_Foo (term (trait Foo ((type Self) (type T)) where ((T : Bar())) {}))) (; trait Bar { } - TraitDecl_Bar (term (trait Bar ((type Self)) () ()))) + TraitDecl_Bar (term (trait Bar ((type Self)) where () {}))) ) (; struct S where A: Foo { } @@ -26,7 +26,7 @@ formality-decl ((AdtDecl_S (term (struct S ((type A) (type B)) - ((A : Foo(B))) + where ((A : Foo(B))) ((S ()))))) (CrateDecl (term (C (crate (TraitDecl_Foo @@ -45,7 +45,7 @@ formality-decl ((AdtDecl_S (term (struct S ((type A) (type B)) - ((A : Foo(B))) + where ((A : Foo(B))) ((S ()))))) (CrateDecl (term (C (crate ((feature expanded-implied-bounds) @@ -63,9 +63,9 @@ formality-decl ((AdtDecl_S (term (struct S ((type A) (type B)) - ((A : Foo(B)) - (B : Bar()) - ) + where ((A : Foo(B)) + (B : Bar()) + ) ((S ()))))) (CrateDecl (term (C (crate (TraitDecl_Foo @@ -84,9 +84,9 @@ formality-decl ((TraitDecl_Baz (term (trait Baz ((type Self) (type A)) - ((Self : Foo(A)) - ) - ()))) + where ((Self : Foo(A)) + ) + {}))) (CrateDecl (term (C (crate (TraitDecl_Foo TraitDecl_Bar TraitDecl_Baz @@ -103,10 +103,10 @@ formality-decl ((TraitDecl_Baz (term (trait Baz ((type Self) (type A)) - ((Self : Foo(A)) - (A : Bar()) - ) - ()))) + where ((Self : Foo(A)) + (A : Bar()) + ) + {}))) (CrateDecl (term (C (crate (TraitDecl_Foo TraitDecl_Bar diff --git a/src/mir/all-check.rkt b/src/mir/all-check.rkt index d743baa7..c862b1dc 100644 --- a/src/mir/all-check.rkt +++ b/src/mir/all-check.rkt @@ -69,7 +69,7 @@ [; constants (prove-crate-item-ok DeclProgram ConstDecl) - (where/error (const _ KindedVarIds WhereClauses Ty FnBody) ConstDecl) + (where/error (const _ KindedVarIds where WhereClauses : Ty = FnBody) ConstDecl) (✅-FnBody DeclProgram (∀ KindedVarIds (() -> Ty where WhereClauses FnBody))) ---------------------------------------- (✅-CrateItemDecl DeclProgram ConstDecl) @@ -77,7 +77,7 @@ [; statics (prove-crate-item-ok DeclProgram StaticDecl) - (where/error (static _ KindedVarIds WhereClauses Ty FnBody) StaticDecl) + (where/error (static _ KindedVarIds where WhereClauses : Ty = FnBody) StaticDecl) (✅-FnBody DeclProgram (∀ KindedVarIds (() -> Ty where WhereClauses FnBody))) ---------------------------------------- (✅-CrateItemDecl DeclProgram StaticDecl) @@ -85,7 +85,7 @@ [; function items (prove-crate-item-ok DeclProgram FnDecl) - (where/error (fn FnId KindedVarIds Tys Ty WhereClauses FnBody) FnDecl) + (where/error (fn FnId KindedVarIds Tys -> Ty where WhereClauses FnBody) FnDecl) (✅-FnBody DeclProgram (∀ KindedVarIds (Tys -> Ty where WhereClauses FnBody))) ---------------------------------------- (✅-CrateItemDecl DeclProgram FnDecl) diff --git a/src/mir/test/basic.rkt b/src/mir/test/basic.rkt index 4a796e6a..3eb96a7e 100644 --- a/src/mir/test/basic.rkt +++ b/src/mir/test/basic.rkt @@ -37,10 +37,8 @@ ) ) ))) - (FnDecl_foo (term (fn foo () - ((user-ty i32) (user-ty i32)) - (user-ty i32) - () + (FnDecl_foo (term (fn foo [] ((user-ty i32) (user-ty i32)) -> (user-ty i32) + where () FnBody_foo))) (CrateDecl_the-crate (term (the-crate (crate (FnDecl_foo))))) (DeclProgram (term ((CrateDecl_the-crate) the-crate))) diff --git a/src/mir/test/issue-25860.rkt b/src/mir/test/issue-25860.rkt index 23dcd828..4c4203a3 100644 --- a/src/mir/test/issue-25860.rkt +++ b/src/mir/test/issue-25860.rkt @@ -47,28 +47,27 @@ ;; } ;; } ;; ``` - (StaticDecl_UNIT (term (static UNIT - () ; generics - () ; where-clauses - (user-ty (& static (& static ()))) ; type - (∃ - ((lifetime L0) - (lifetime L1) - (lifetime L2) - (lifetime L3) - (lifetime L4) - ) - ([(_0 (user-ty (& L0 (& L1 ()))) mut) - (_1 (user-ty (& L2 ())) mut) - (_2 (user-ty ()) mut) - ] - [(bb0 {(noop - (_1 = (ref L3 () _2)) - (_0 = (ref L4 () _1))) - return - })] - ) - ) + (StaticDecl_UNIT (term (static UNIT () + where () + : (user-ty (& static (& static ()))) + = (∃ + ((lifetime L0) + (lifetime L1) + (lifetime L2) + (lifetime L3) + (lifetime L4) + ) + ([(_0 (user-ty (& L0 (& L1 ()))) mut) + (_1 (user-ty (& L2 ())) mut) + (_2 (user-ty ()) mut) + ] + [(bb0 {(noop + (_1 = (ref L3 () _2)) + (_0 = (ref L4 () _1))) + return + })] + ) + ) ))) ] diff --git a/src/mir/type-of.rkt b/src/mir/type-of.rkt index cdcca88b..7ce83caf 100644 --- a/src/mir/type-of.rkt +++ b/src/mir/type-of.rkt @@ -44,7 +44,7 @@ ; ; extract the name of the singular variant (place-type-of Γ Place (rigid-ty AdtId Parameters) ()) - (where (struct AdtId _ _ ((VariantId _))) (decl-of-adt Γ AdtId)) + (where (struct AdtId _ where _ ((VariantId _))) (decl-of-adt Γ AdtId)) (field-ty Γ AdtId Parameters VariantId FieldId Ty_field) ---------------------------------- (place-type-of Γ (field Place FieldId) Ty_field ()) @@ -54,7 +54,7 @@ ; ; must have been downcast to a particular variant (place-type-of Γ Place (rigid-ty AdtId Parameters) (VariantId)) - (where (enum AdtId _ _ _) (decl-of-adt Γ AdtId)) + (where (enum AdtId _ _ where _) (decl-of-adt Γ AdtId)) (field-ty Γ AdtId Parameters VariantId FieldId Ty_field) ---------------------------------- (place-type-of Γ (field Place FieldId) Ty_field ()) @@ -63,7 +63,7 @@ [; downcast to an enum variant (place-type-of Γ Place (rigid-ty AdtId Parameters) ()) - (where (enum AdtId _ _ (_ ... (VariantId _) _ ...)) (decl-of-adt Γ AdtId)) + (where (enum AdtId _ where _ (_ ... (VariantId _) _ ...)) (decl-of-adt Γ AdtId)) ---------------------------------- (place-type-of Γ (downcast Place VariantId) (rigid-ty AdtId Parameters) (VariantId)) ] @@ -93,7 +93,7 @@ #:mode (field-ty I I I I I O) #:contract (field-ty Γ AdtId Parameters VariantId FieldId Ty) - [(where (_ AdtId KindedVarIds _ (_ ... (VariantId FieldDecls) _ ...)) (decl-of-adt Γ AdtId)) + [(where (_ AdtId KindedVarIds where _ (_ ... (VariantId FieldDecls) _ ...)) (decl-of-adt Γ AdtId)) (where/error Substitution (create-substitution KindedVarIds Parameters)) (where (_ ... (FieldId Ty) _ ...) FieldDecls) (where/error Ty_substituted (apply-substitution Substitution Ty))