generics in trait syntax

Lampe/Lampe.lean

@@ -112,14 +112,14 @@ example {p Γ} {x y : Tp.denote p Tp.field} :
   sl
   aesop
 
-nr_trait_impl[bulbulizeField] <> Bulbulize<> for Field {
+nr_trait_impl[bulbulizeField] <> Bulbulize<> for Field where {
     fn bulbulize<>(x : Field) -> Field {
       #add(x, x) : Field
     };
 }
 
 
-nr_trait_impl[bulbulizeU32] <> Bulbulize<> for u32 {
+nr_trait_impl[bulbulizeU32] <> Bulbulize<> for u32 where {
   fn bulbulize<>(_x : u32) -> u32 {
       69 : u32
     }
@@ -139,11 +139,10 @@ example : STHoare p simpleTraitEnv ⟦⟧ (simpleTraitCall .field arg) (fun v =>
   · constructor
     · apply List.Mem.head
     any_goals rfl
-    rotate_left 2
-    all_goals simp only
-    . exact h![]
-    · tauto
-    · tauto
+    all_goals (simp only)
+    rotate_right 1
+    exact h![]
+    all_goals tauto
   · simp; rfl
   any_goals rfl
   simp
@@ -160,11 +159,10 @@ example : STHoare p simpleTraitEnv ⟦⟧ (simpleTraitCall (.u 32) arg) (fun v =
     · apply List.Mem.tail
       apply List.Mem.head
     any_goals rfl
-    rotate_left 2
-    all_goals simp only
-    . exact h![]
-    · tauto
-    · tauto
+    all_goals (simp only)
+    rotate_right 1
+    exact h![]
+    all_goals tauto
   · simp; rfl
   any_goals rfl
   simp

Lampe/Lampe/Ast.lean

@@ -13,17 +13,17 @@ abbrev Ident := String
 abbrev Tp.lambdaRef := Tp.ref .unit
 
 structure TraitRef where
-name : Ident
-traitGenericKinds : List Kind
-traitGenerics : HList Kind.denote traitGenericKinds
+  name : Ident
+  traitGenericKinds : List Kind
+  traitGenerics : HList Kind.denote traitGenericKinds
 
 structure TraitImplRef where
-trait : TraitRef
-self : Tp
+  trait : TraitRef
+  self : Tp
 
 structure TraitMethodImplRef where
-trait : TraitImplRef
-method : Ident
+  trait : TraitImplRef
+  method : Ident
 
 inductive FunctionIdent (rep : Tp → Type) : Type where
 | builtin : Builtin → FunctionIdent rep
@@ -73,12 +73,12 @@ structure Struct where
   fieldTypes : HList Kind.denote tyArgKinds → List Tp
 
 structure TraitImpl where
-traitGenericKinds : List Kind
-implGenericKinds : List Kind
-traitGenerics : HList Kind.denote implGenericKinds → HList Kind.denote traitGenericKinds
-constraints : HList Kind.denote implGenericKinds → List TraitImplRef
-self : HList Kind.denote implGenericKinds → Tp
-impl : HList Kind.denote implGenericKinds → List (Ident × Function)
+  traitGenericKinds : List Kind
+  implGenericKinds : List Kind
+  traitGenerics : HList Kind.denote implGenericKinds → HList Kind.denote traitGenericKinds
+  constraints : HList Kind.denote implGenericKinds → List TraitImplRef
+  self : HList Kind.denote implGenericKinds → Tp
+  impl : HList Kind.denote implGenericKinds → List (Ident × Function)
 
 -- @[reducible]
 -- def Struct.tp (s: Struct): HList Kind.denote s.tyArgKinds → Tp :=

Lampe/Lampe/Syntax.lean

@@ -105,8 +105,10 @@ syntax "|" nr_param_decl,* "|" "->" nr_type nr_expr : nr_expr
 syntax "^" nr_ident "(" nr_expr,* ")" ":" nr_type : nr_expr
 
 syntax nr_fn_decl := nr_ident "<" ident,* ">" "(" nr_param_decl,* ")" "->" nr_type "{" sepBy(nr_expr, ";", ";", allowTrailingSep) "}"
+syntax nr_trait_constraint := nr_ident "<" ident,* ">" ":" nr_ident "<" ident,* ">"
 syntax nr_trait_fn_def := "fn" nr_fn_decl
-syntax nr_trait_impl := "<" ident,* ">" nr_ident "<" ident,* ">" "for" nr_type "{" sepBy(nr_trait_fn_def, ";", ";", allowTrailingSep) "}"
+syntax nr_trait_impl := "<" ident,* ">" nr_ident "<" ident,* ">" "for" nr_type "where" sepBy(nr_trait_constraint, ",", ",", allowTrailingSep)
+  "{" sepBy(nr_trait_fn_def, ";", ";", allowTrailingSep) "}"
 
 def Expr.letMutIn (definition : Expr rep tp) (body : rep tp.ref → Expr rep tp'): Expr rep tp' :=
   let refDef := Expr.letIn definition fun v => Expr.call h![] _ (tp.ref) (.builtin .ref) h![v]
@@ -236,13 +238,14 @@ def mkFnDecl [Monad m] [MonadQuotation m] [MonadExceptOf Exception m] [MonadErro
         | $(←mkHListLit $ params.map Prod.fst) => $body⟩)
   let syn : TSyntax `term ← `(FunctionDecl.mk $(Syntax.mkStrLit name) $ Function.mk $genericsDecl $lambdaDecl)
   pure (name, syn)
-| syn => throwError s!"error at: {syn}"
+| _ => throwUnsupportedSyntax
 
 def mkTraitImpl [Monad m] [MonadQuotation m] [MonadExceptOf Exception m] [MonadError m] : Syntax → m (String × TSyntax `term)
-| `(nr_trait_impl| < $generics,* > $traitName < $traitGenerics,* > for $targetType { $fns;* }) => do
+| `(nr_trait_impl| < $generics,* > $traitName < $traitGenerics,* > for $targetType where $constraints,* { $fns;* }) => do
   let implGenericKinds ← mkListLit (← generics.getElems.toList.mapM fun _ => `(Kind.type))
   let traitGenericKinds ← mkListLit (← traitGenerics.getElems.toList.mapM fun _ => `(Kind.type))
-  let generics := generics.getElems.toList.map fun tyVar => (mkIdent $ Name.mkSimple tyVar.getId.toString)
+  let implGenerics := generics.getElems.toList.map fun tyVar => (mkIdent $ Name.mkSimple tyVar.getId.toString)
+  let traitGenerics := traitGenerics.getElems.toList.map fun tyVar => (mkIdent $ Name.mkSimple tyVar.getId.toString)
   let traitName ← mkNrIdent traitName
   let fnDecls ← mkListLit (← fns.getElems.toList.mapM fun fnSyn => match fnSyn with
     | `(nr_trait_fn_def| fn $fnDecl) => do
@@ -253,10 +256,10 @@ def mkTraitImpl [Monad m] [MonadQuotation m] [MonadExceptOf Exception m] [MonadE
   let syn : TSyntax `term ← `(TraitImpl.mk
     (traitGenericKinds := $traitGenericKinds)
     (implGenericKinds := $implGenericKinds)
-    (traitGenerics := fun _ => h![])
-    (constraints := fun _ => [])
-    (self := fun generics => match generics with | $(←mkHListLit generics) => $targetType)
-    (impl := fun generics => $fnDecls))
+    (traitGenerics := fun gs => match gs with | $(←mkHListLit implGenerics) => $(←mkHListLit traitGenerics))
+    (constraints := fun gs => match gs with | $(←mkHListLit implGenerics) => [])
+    (self := fun gs => match gs with | $(←mkHListLit implGenerics) => $targetType)
+    (impl := fun gs => match gs with | $(←mkHListLit implGenerics) => $fnDecls))
   pure (traitName, syn)
 | _ => throwUnsupportedSyntax