From 21a40acea1a354f8653651f60807599572f01797 Mon Sep 17 00:00:00 2001
From: lcnr <rust@lcnr.de>
Date: Mon, 11 Apr 2022 09:00:25 +0200
Subject: [PATCH] start adding const parameters

---
 book/src/layers.md                     |  2 +-
 src/decl/test/const-generics/basic.rkt | 32 ++++++++++++++++++++++++++
 src/ty/grammar.rkt                     | 15 +++++++++---
 3 files changed, 45 insertions(+), 4 deletions(-)
 create mode 100644 src/decl/test/const-generics/basic.rkt

diff --git a/book/src/layers.md b/book/src/layers.md
index 1b7f1796..ee364b1b 100644
--- a/book/src/layers.md
+++ b/book/src/layers.md
@@ -27,7 +27,7 @@ like `forall<T> { Implemented(T: Eq) => HasImpl(Vec<T>: Eq) }`.
 (The distinction between `HasImpl` and `Implemented` is covered below.)
 
 This layer also defines the well-formedness checks for those items.
-For example, `struct Foo { f1: T1 }` is well-formed if `T` is well-formed.
+For example, `struct Foo { f1: T }` is well-formed if `T` is well-formed.
 
 ## The MIR type system layer (`formality-mir`)
 
diff --git a/src/decl/test/const-generics/basic.rkt b/src/decl/test/const-generics/basic.rkt
new file mode 100644
index 00000000..8a0e253f
--- /dev/null
+++ b/src/decl/test/const-generics/basic.rkt
@@ -0,0 +1,32 @@
+#lang racket
+(require redex/reduction-semantics
+         "../../decl-to-clause.rkt"
+         "../../decl-ok.rkt"
+         "../../grammar.rkt"
+         "../../prove.rkt"
+         "../../../util.rkt")
+
+(module+ test
+  ;; Program:
+  ;;
+  ;; struct Foo;
+  ;; trait Bar<const N: usize> {}
+  ;; impl<const M: usize> Bar<M> for Foo {}
+  (redex-let*
+   formality-decl
+   ((KindedVarId_M (term ((CtKind (scalar-ty usize)) M)))
+    (TraitDecl (term (Bar (trait ((TyKind Self) ((CtKind (scalar-ty usize)) N)) () ()))))
+    (AdtDecl_Foo (term (Foo (struct () () ((Foo ()))))))
+    (CtKind_M (term M))
+    (Ct_M (term ((scalar-ty usize) CtKind_M)))
+    (TraitRef_Bar (term (Bar ((TyRigid Foo ()) Ct_M))))
+    (TraitImplDecl (term (impl (KindedVarId_M) TraitRef_Bar () ())))
+    (CrateDecl (term (TheCrate (crate (TraitDecl AdtDecl_Foo TraitImplDecl)))))
+    (Env (term (env-for-crate-decl CrateDecl)))
+
+    ;; `TheCrate` can prove `forall<const M: usize> Bar<M>: Foo`
+    (Goal (term (ForAll (KindedVarId_M) (Implemented TraitRef_Bar))))
+    )
+    (traced '()
+            (decl:test-can-prove Env Goal)))
+  )
diff --git a/src/ty/grammar.rkt b/src/ty/grammar.rkt
index 66b42395..3c77ebc1 100644
--- a/src/ty/grammar.rkt
+++ b/src/ty/grammar.rkt
@@ -19,12 +19,12 @@
   ;; lifetime, etc)
   ;;
   ;; Overridden from formality-logic.
-  (ParameterKind ::= TyKind LtKind)
+  (ParameterKind ::= TyKind LtKind (CtKind Ty))
 
   ;; Parameter: value for a generic parameter
   ;;
   ;; Overridden from formality-logic.
-  (Parameter ::= Ty Lt)
+  (Parameter ::= Ty Lt Ct)
 
   ;; ANCHOR:Predicates
   ;; `Predicate` -- the atomic items that we can prove
@@ -99,6 +99,15 @@
   ;; Treat ABIs as opaque strings (for now, at least)
   (Abi ::= string)
 
+  ;; Ct -- Rust constants in the type system.
+  ;;
+  ;; TODO: Also add non-leaf things here.
+  (Ct ::= (Ty CtKind))
+  (CtKind ::=
+      (Leaf number)          ; A value tree leaf.
+      VarId                  ; Bound, existential (inference), or universal (placeholder) variable.
+      )
+
   ;; Lt -- Rust lifetimes
   ;;
   ;; Very similar to types `Ty` in terms of how they are represented
@@ -124,7 +133,7 @@
   (VarInequality ::= (Parameters_lb <= VarId <= Parameters_ub))
 
   ;; Scalars -- numbers, booleans
-  (ScalarId ::= i8 u8 i16 u16 i32 u32 i64 u64 i128 u128 bool)
+  (ScalarId ::= i8 u8 i16 u16 i32 u32 i64 u64 i128 u128 isize usize bool)
 
   ;; Identifiers -- these are all equivalent, but we give them fresh names to help
   ;; clarify their purpose