From 06545dc8192312cef0230111edb6374b3e016fa8 Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Wed, 14 Sep 2022 13:54:58 -0400 Subject: [PATCH 1/4] add a fn-def type and adjust type of fn constants but we're not really testing it in any useful way --- racket-src/body/type-of.rkt | 37 ++++++++++++++++++++++++++++-------- racket-src/decl/env.rkt | 15 +++++++++++++++ racket-src/ty/grammar.rkt | 1 + racket-src/ty/hook.rkt | 12 ++++++++++++ racket-src/ty/parameters.rkt | 23 ++++++++++++++++++---- racket-src/ty/test/hook.rkt | 1 + 6 files changed, 77 insertions(+), 12 deletions(-) diff --git a/racket-src/body/type-of.rkt b/racket-src/body/type-of.rkt index 4914ea95..6daa0710 100644 --- a/racket-src/body/type-of.rkt +++ b/racket-src/body/type-of.rkt @@ -125,14 +125,35 @@ (type-of/Constant Γ false (user-ty bool))] [; function - (where/error (fn _ KindedVarIds (Ty_arg ...) -> Ty_ret _ _ _) (find-fn Γ FnId)) - (where/error (KindedVarId_subst ..._n KindedVarId_other ...) KindedVarIds) - (where/error Substitution (create-substitution (KindedVarId_subst ...) (Parameter ...))) - (where/error (Ty_argsubst ...) ((apply-substitution Substitution Ty_arg) ...)) - (where/error Ty_retsubst (apply-substitution Substitution Ty_ret)) - (where/error number_args ,(length (term (Ty_arg ...)))) - (where/error Ty_fnptr (rigid-ty (fn-ptr "Rust" number_args) (Ty_argsubst ... Ty_retsubst))) - (where/error Ty (∀ (KindedVarId_other ...) Ty_fnptr)) + ; + ; Subtle: functions in Rust today have early/late-bound parameters, + ; but we include both in the FnDef type (unlike rustc). The current assumption + ; is that the first N parameters (however many are supplied) are early-bound, + ; and the remainder are late. Therefore, we want to result a type like + ; + ; (∀ KindedVarIds_late (fn-def FnId (Parameter ... KindedVarIds_late)))Γ + (where/error (fn _ KindedVarIds _ -> _ where Biformulas _) (find-fn Γ FnId)) + + ; Split the generics from the function into early/late + (where/error (KindedVarId_early ..._n KindedVarId_late ...) KindedVarIds) + + ; Create a substitution from early-bound parameters to the values from user + (where/error Substitution_early (create-substitution (KindedVarId_early ...) (Parameter ...))) + (where/error Biformulas_early (apply-substitution Substitution_early Biformulas)) + + ; Apply that substitution + (where/error Ty_fn (rigid-ty (fn-def FnId) (Parameter ... KindedVarId_late ...))) + + ; Construct the final type + ; + ; Note that it has implications to assert that the where-clauses hold. + ; Is this quite right? We want them for at least the biformulas that relate + ; to the late-bound lifetimes, and it seems wrong to do anything fancy, so + ; I think we want them all. + ; + ; The idea is that, when we apply the call, we'll have to discharge all those + ; implications, and the same will be true to cast to a final type. + (where/error Ty (∀ (KindedVarId_late ...) (implies Biformulas_early Ty_fn))) ------------------------------------------ (type-of/Constant Γ (fn-ptr FnId (Parameter ..._n)) Ty)] diff --git a/racket-src/decl/env.rkt b/racket-src/decl/env.rkt index af0b6fa5..e1f94712 100644 --- a/racket-src/decl/env.rkt +++ b/racket-src/decl/env.rkt @@ -69,6 +69,8 @@ (term (decl:categorize-goal ,goal))) (lambda (adt-id) (term (generics-for-adt-id CrateDecls ,adt-id))) + (lambda (fn-id) + (term (generics-for-fn-id CrateDecls ,fn-id))) )) (where/error (CrateDecls CrateId) DeclProgram) @@ -86,4 +88,17 @@ (((VarId (ParameterKind =)) ...) Biformulas) ; for now we hardcode `=` (invariance) as the variance (where/error (AdtKind AdtId ((ParameterKind VarId) ...) Biformulas AdtVariants) (adt-with-id CrateDecls AdtId)) ] + ) + +(define-metafunction formality-decl + ;; Part of the "hook" for a formality-decl program: + ;; + ;; Create the clauses for solving a given predicate + ;; (right now the predicate is not used). + generics-for-fn-id : CrateDecls FnId -> Generics + + [(generics-for-fn-id CrateDecls FnId) + (((VarId (ParameterKind =)) ...) Biformulas) ; for now we hardcode `=` (invariance) as the variance + (where/error (fn FnId [(ParameterKind VarId) ...] _ -> _ where Biformulas _) (fn-with-id CrateDecls FnId)) + ] ) \ No newline at end of file diff --git a/racket-src/ty/grammar.rkt b/racket-src/ty/grammar.rkt index 7de2ced7..f2c86d66 100644 --- a/racket-src/ty/grammar.rkt +++ b/racket-src/ty/grammar.rkt @@ -113,6 +113,7 @@ (ref MaybeMut) ; `&mut` or `&`, expects a lifetime + type parameter (tuple number) ; tuple of given arity (fn-ptr Abi number) ; fn types + (fn-def FnId) ; the zero-sized type derived from a type definition ) ;; AliasTy -- an *alias* type is basically a *type lambda*. You can either *normalize* it diff --git a/racket-src/ty/hook.rkt b/racket-src/ty/hook.rkt index d7a3ea86..4010928a 100644 --- a/racket-src/ty/hook.rkt +++ b/racket-src/ty/hook.rkt @@ -12,7 +12,9 @@ ;; Extends the core logic hook with the ability to query variance: ;; ;; adt-generics : AdtId -> Generics +;; fn-generics : FnId -> Generics (struct formality-ty-hook formality-logic-hook (adt-generics + fn-generics )) (define-metafunction formality-ty @@ -25,6 +27,16 @@ ] ) +(define-metafunction formality-ty + ;; Returns the variance for each of the parameters to an function + env-fn-generics : Env FnId -> Generics + + [(env-fn-generics Env FnId) + ,((formality-ty-hook-fn-generics (term any)) (term FnId)) + (where/error (Hook: any) (env-hook Env)) + ] + ) + (define-metafunction formality-ty ty:categorize-goal : Goal -> Goal/Categorization diff --git a/racket-src/ty/parameters.rkt b/racket-src/ty/parameters.rkt index e8797747..6b5ce6f8 100644 --- a/racket-src/ty/parameters.rkt +++ b/racket-src/ty/parameters.rkt @@ -37,11 +37,26 @@ ;; a `RigidName`. generics-for : Env RigidName -> Generics - [(generics-for Env AdtId) (env-adt-generics Env AdtId)] - [(generics-for Env ScalarId) (() ())] - [(generics-for Env (ref ())) (((TheLt (lifetime +)) (TheTy (type +))) + [; For an ADT like `Vec`, consult its definition to see what generic parameters it has. + (generics-for Env AdtId) (env-adt-generics Env AdtId)] + + [; For a fn, consult its definition to see what generic parameters it has. + (generics-for Env (fn-def FnId)) (env-fn-generics Env FnId)] + + [; Scalars like u32 have no generic parameters. + ; + ; Effectively they are modeled as `struct u32`. + (generics-for Env ScalarId) (() ())] + + [; We model `&'a T` as a type with two parameters, `'a` and `T`, + ; where `T: 'a`. + ; + ; Kind of like `struct Ref<'a, T> where T: 'a` + (generics-for Env (ref ())) (((TheLt (lifetime +)) (TheTy (type +))) [(TheTy -outlives- TheLt)])] - [(generics-for Env (ref mut)) (((TheLt (lifetime +)) (TheTy (type =))) + + [; We model `&'a mut T` the same way. + (generics-for Env (ref mut)) (((TheLt (lifetime +)) (TheTy (type =))) [(TheTy -outlives- TheLt)])] [; tuples are covariant in their elements P1...Pn diff --git a/racket-src/ty/test/hook.rkt b/racket-src/ty/test/hook.rkt index cd4041d3..f1f3b249 100644 --- a/racket-src/ty/test/hook.rkt +++ b/racket-src/ty/test/hook.rkt @@ -35,6 +35,7 @@ (lambda (predicate1) (term (ty:debone-predicate ,predicate1))) (lambda (goal) (term (ty:categorize-goal ,goal))) (lambda (adt-id) (term (find-adt-generics ,adt-id ((AdtId Generics) ...)))) + (lambda (fn-id) (term NotDefined)) )))) ] ) From 745b118bb7ddca3734809160b39f4d566249d80a Mon Sep 17 00:00:00 2001 From: Dominik Stolz Date: Wed, 14 Sep 2022 23:33:55 +0200 Subject: [PATCH 2/4] Fix fn-def type construction in type-of/Constant --- racket-src/body/type-of.rkt | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) diff --git a/racket-src/body/type-of.rkt b/racket-src/body/type-of.rkt index 6daa0710..aac8311b 100644 --- a/racket-src/body/type-of.rkt +++ b/racket-src/body/type-of.rkt @@ -129,20 +129,25 @@ ; Subtle: functions in Rust today have early/late-bound parameters, ; but we include both in the FnDef type (unlike rustc). The current assumption ; is that the first N parameters (however many are supplied) are early-bound, - ; and the remainder are late. Therefore, we want to result a type like + ; and the remainder are late. Therefore, the constant + ; + ; (fn-ptr foo [P_1 … P_n]) + ; + ; referring to a function foo with the formal variables V_1, …, V_m gets the type + ; + ; (∀ [V_n+1 … V_m] (implies Biformulas (rigid-ty (fn-def foo) [P_1 … P_n V_n+1 … V_m]))) ; - ; (∀ KindedVarIds_late (fn-def FnId (Parameter ... KindedVarIds_late)))Γ (where/error (fn _ KindedVarIds _ -> _ where Biformulas _) (find-fn Γ FnId)) ; Split the generics from the function into early/late - (where/error (KindedVarId_early ..._n KindedVarId_late ...) KindedVarIds) + (where/error (KindedVarId_early ..._n (ParameterKind_late VarId_late) ...) KindedVarIds) ; Create a substitution from early-bound parameters to the values from user (where/error Substitution_early (create-substitution (KindedVarId_early ...) (Parameter ...))) (where/error Biformulas_early (apply-substitution Substitution_early Biformulas)) ; Apply that substitution - (where/error Ty_fn (rigid-ty (fn-def FnId) (Parameter ... KindedVarId_late ...))) + (where/error Ty_fn (rigid-ty (fn-def FnId) (Parameter ... VarId_late ...))) ; Construct the final type ; @@ -153,7 +158,7 @@ ; ; The idea is that, when we apply the call, we'll have to discharge all those ; implications, and the same will be true to cast to a final type. - (where/error Ty (∀ (KindedVarId_late ...) (implies Biformulas_early Ty_fn))) + (where/error Ty (∀ ((ParameterKind_late VarId_late) ...) (implies Biformulas_early Ty_fn))) ------------------------------------------ (type-of/Constant Γ (fn-ptr FnId (Parameter ..._n)) Ty)] From 4a8abfb2ffffd142cc9d8cb78fe5dc75bc78d009 Mon Sep 17 00:00:00 2001 From: Dominik Stolz Date: Thu, 15 Sep 2022 17:16:25 +0200 Subject: [PATCH 3/4] Move FnId to ty grammar --- racket-src/decl/grammar.rkt | 3 +-- racket-src/ty/grammar.rkt | 2 +- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/racket-src/decl/grammar.rkt b/racket-src/decl/grammar.rkt index 58bfd561..4faea027 100644 --- a/racket-src/decl/grammar.rkt +++ b/racket-src/decl/grammar.rkt @@ -115,8 +115,7 @@ StaticId VariantId FeatureId - FieldId - FnId) variable-not-otherwise-mentioned) + FieldId) variable-not-otherwise-mentioned) #:binding-forms (AdtKind AdtKind diff --git a/racket-src/ty/grammar.rkt b/racket-src/ty/grammar.rkt index f2c86d66..5835076c 100644 --- a/racket-src/ty/grammar.rkt +++ b/racket-src/ty/grammar.rkt @@ -191,7 +191,7 @@ ;; Identifiers -- these are all equivalent, but we give them fresh names to help ;; clarify their purpose - (AdtId AliasId TraitId AssociatedTyId AliasTyId ::= + (AdtId AliasId TraitId AssociatedTyId AliasTyId FnId ::= variable-not-otherwise-mentioned) ;; Signature From c1afaae034b830db0f66b4c2122d363bd6befad0 Mon Sep 17 00:00:00 2001 From: Dominik Stolz Date: Thu, 15 Sep 2022 17:20:46 +0200 Subject: [PATCH 4/4] Generate fn-def types --- src/gen/ty.rs | 21 +++++++++++++++------ 1 file changed, 15 insertions(+), 6 deletions(-) diff --git a/src/gen/ty.rs b/src/gen/ty.rs index 0b92f274..1a1502c6 100644 --- a/src/gen/ty.rs +++ b/src/gen/ty.rs @@ -93,7 +93,6 @@ impl<'tcx> FormalityGen<'tcx> { rustc_hir::Mutability::Mut => format!("(&mut {lifetime_str} {ty_str})"), } } - ty::TyKind::FnDef(_, _) => todo!(), ty::TyKind::FnPtr(fn_sig) => { let inputs = fn_sig .skip_binder() @@ -182,11 +181,21 @@ impl<'tcx> FormalityGen<'tcx> { } pub fn emit_ty(&self, ty: ty::Ty<'tcx>) -> String { - if let ty::TyKind::Param(param_ty) = ty.kind() { - format!("{}", param_ty.name) - } else { - // convert UserTy to Ty by calling the user-ty metafunction - format!("(mf-apply user-ty {})", self.emit_user_ty(ty)) + match ty.kind() { + ty::TyKind::FnDef(def_id, substs) => { + let fn_id = self.emit_def_path(*def_id); + let params = substs + .iter() + .map(|arg| self.emit_param(arg)) + .intersperse(" ".to_string()) + .collect::(); + format!("(rigid-ty (fn-def {fn_id}) [{params}])") + } + ty::TyKind::Param(param_ty) => format!("{}", param_ty.name), + _ => { + // convert UserTy to Ty by calling the user-ty metafunction + format!("(mf-apply user-ty {})", self.emit_user_ty(ty)) + } } }