Merge pull request #56 from nikomatsakis/user-ty

User ty
rust-lang · Jun 3, 2022 · fb94067 · fb94067
2 parents 0d861ef + d49d1d5
commit fb94067
Show file tree

Hide file tree

Showing 39 changed files with 563 additions and 357 deletions.
diff --git a/src/decl/decl-from-crate.rkt b/src/decl/decl-from-crate.rkt
diff --git 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"
          )
@@ -42,7 +41,7 @@
    ;;         (implies ((well-formed (type T))
    ;;                   (is-implemented (Ord T)))
    ;;           (well-formed (type Vec<T>)) ...))
-   (crate-item-ok-goal CrateDecls (AdtId (AdtKind KindedVarIds (WhereClause ...) AdtVariants)))
+   (crate-item-ok-goal CrateDecls (AdtKind AdtId KindedVarIds where (WhereClause ...) AdtVariants))
    Goal_wf
 
    (where/error (KindedVarId ...) KindedVarIds)
@@ -71,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-decl 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) ...))
    ]
 
@@ -80,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 (TraitId (trait 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 ...
@@ -96,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...
@@ -109,7 +108,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 _) ...) where _ _) (trait-with-id CrateDecls TraitId))
    (where/error (KindedVarId_impl ...) KindedVarIds_impl)
    (where/error (WhereClause_impl ...) WhereClauses_impl)
    ]
@@ -119,7 +118,7 @@
    ;;     const NAMED<T>: Foo<T> 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 where WhereClauses : Ty = FnBody))
    (∀ KindedVarIds
       (implies
        (; assuming all generic parameters are WF...
@@ -140,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 where WhereClauses : Ty = FnBody))
    (∀ KindedVarIds
       (implies
        (; assuming all generic parameters are WF...
@@ -199,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
@@ -209,13 +208,13 @@
                    ))))
 
    (where (rigid-ty AdtId Parameters) Ty_impl)
-   (where (AdtKind KindedVarIds_adt WhereClauses_adt _) (item-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
    ]
 
@@ -240,7 +239,7 @@
    ;          (is-implemented (Vec<T>: Copy)))
    ;
    ; of course, in this case, it is not provable because `Vec<T>: 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
@@ -250,7 +249,7 @@
                        )))))
 
    (where (rigid-ty AdtId Parameters) Ty_impl)
-   (where (AdtKind KindedVarIds_adt _ AdtVariants) (item-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
@@ -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
@@ -175,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 where (WhereClause ...) AdtVariants))
    ((Clause) Invariants_wf Invariants_wc)
 
    (where/error ((ParameterKind VarId) ...) KindedVarIds)
@@ -221,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 where (WhereClause ...) TraitItems))
    ((Clause)
     (Invariant_wc ...
      Invariant_wf ...
@@ -276,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 KindedVarIds_trait _ _) (item-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
@@ -294,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 where WhereClauses_fn FnBody))
    (() () ())
    ]
 
@@ -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 ())))
      )
     ())
    )
@@ -380,7 +381,6 @@
 
   [(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 (AdtKind ((ParameterKind VarId) ...) WhereClauses AdtVariants) AdtContents)
+   (where/error (AdtKind AdtId ((ParameterKind VarId) ...) WhereClauses AdtVariants) (adt-with-id CrateDecls AdtId))
    ]
   )
diff --git 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 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
@@ -3,9 +3,8 @@
 (provide formality-decl
          crate-decl-with-id
          trait-decl-id
-         item-with-id
-         scalar-ty
-         unit-ty
+         trait-with-id
+         adt-with-id
          crate-decls
          )
 
@@ -28,8 +27,7 @@
   (FeatureDecl ::= (feature FeatureId))
 
   ;; AdtDecl -- struct/enum/union declarations
-  (AdtDecl ::= (AdtId AdtContents))
-  (AdtContents ::= (AdtKind KindedVarIds WhereClauses AdtVariants))
+  (AdtDecl ::= (AdtKind AdtId KindedVarIds where WhereClauses AdtVariants))
   (AdtVariants ::= (AdtVariant ...))
   (AdtKind ::= struct enum union)
   (AdtVariant ::= (VariantId FieldDecls))
@@ -42,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 where WhereClauses TraitItems))
 
   ;; TraitItem --
   (TraitItems ::= (TraitItem ...))
@@ -52,15 +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 ::= (StaticId StaticContents))
-  (StaticContents ::= (static KindedVarIds WhereClauses Ty FnBody))
+  (StaticDecl ::= (static StaticId KindedVarIds where WhereClauses : Ty = FnBody))
 
   ;; Named constants
-  (ConstDecl ::= (ConstId ConstContents))
-  (ConstContents ::= (const KindedVarIds WhereClauses Ty FnBody))
+  (ConstDecl ::= (const ConstId KindedVarIds where WhereClauses : Ty = FnBody))
 
   ;; ImplItem --
   (ImplItems ::= (ImplItem ...))
@@ -70,8 +65,7 @@
   ;; Function
   ;;
   ;; fn foo<...>(...) -> ... where ... { body }
-  (FnDecl ::= (FnId FnContents))
-  (FnContents ::= (fn-decl 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
@@ -87,32 +81,32 @@
   #: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 ...))
-  (static ConstId
+         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 ...))
-  (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 ...))
+          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 ...)
+      where WhereClauses #:refers-to (shadow VarId ...)
+      FnBody #:refers-to (shadow VarId ...))
   )
 
 (define-metafunction formality-decl
@@ -137,17 +131,29 @@
 (define-metafunction formality-decl
   trait-decl-id : TraitDecl -> TraitId
 
-  ((trait-decl-id (TraitId TraitContents)) TraitId)
+  ((trait-decl-id (trait TraitId _ where _ _)) TraitId)
   )
 
 (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 -> AdtDecl
 
-  ((item-with-id CrateDecls AnyId)
-   Term
+  [(adt-with-id CrateDecls AdtId)
+   (AdtKind AdtId KindedVarIds where WhereClauses AdtVariants)
 
    (where (_ ... CrateDecl _ ...) CrateDecls)
-   (where (_ (crate (_ ... (AnyId Term) _ ...))) CrateDecl)
-   )
+   (where (_ (crate (_ ... (AdtKind AdtId KindedVarIds where WhereClauses AdtVariants) _ ...))) CrateDecl)
+   ]
+  )
+
+(define-metafunction formality-decl
+  ;; Find the given trait amongst all the declared crates.
+  trait-with-id : CrateDecls TraitId -> TraitDecl
+
+  [(trait-with-id CrateDecls TraitId)
+   (trait TraitId KindedVarIds where WhereClauses TraitItems)
+
+   (where (_ ... CrateDecl _ ...) CrateDecls)
+   (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
@@ -2,24 +2,26 @@
 (require redex/reduction-semantics
          "../grammar.rkt"
          "../prove.rkt"
+         "../../ty/user-ty.rkt"
          "../../util.rkt")
 
 (module+ test
   (current-traced-metafunctions '(relate/one compare/one/substituted equate/one/substituted))
   (redex-let*
    formality-decl
 
-   ((; trait Debug { }
-     TraitDecl (term (Debug (trait ((type Self)) () ()))))
+   [(; trait Debug { }
+     TraitDecl (term (trait Debug ((type Self)) where () ())))
     (; struct Foo<T: Debug> { }
-     AdtDecl_Foo (term (Foo (struct ((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
     redex-let*
     formality-decl
     [
      (; const BROKEN<T>: Foo<T>;
-      ConstDecl_broken (term (BROKEN (const ((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)))))
      ]
 
@@ -32,7 +34,7 @@
     formality-decl
     [
      (; const OK<T: Debug>: Foo<T>;
-      ConstDecl_ok (term (OK (const ((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)))))
      ]