feat: parametrised deriving handlers

src/Lean/Elab/Deriving/Basic.lean

@@ -1,18 +1,19 @@
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
+Authors: Leonardo de Moura, Wojciech Nawrocki
 -/
 import Lean.Elab.Command
 
 namespace Lean.Elab
 open Command
 
-def DerivingHandler := (typeNames : Array Name) → CommandElabM Bool
+def DerivingHandler := (typeNames : Array Name) → (args? : Option Syntax) → CommandElabM Bool
+def DerivingHandlerNoArgs := (typeNames : Array Name) → CommandElabM Bool
 
 builtin_initialize derivingHandlersRef : IO.Ref (NameMap DerivingHandler) ← IO.mkRef {}
 
-def registerBuiltinDerivingHandler (className : Name) (handler : DerivingHandler) : IO Unit := do
+def registerBuiltinDerivingHandler' (className : Name) (handler : DerivingHandler) : IO Unit := do
   let initializing ← IO.initializing
   unless initializing do
     throw (IO.userError "failed to register deriving handler, it can only be registered during initialization")
@@ -20,23 +21,26 @@ def registerBuiltinDerivingHandler (className : Name) (handler : DerivingHandler
     throw (IO.userError s!"failed to register deriving handler, a handler has already been registered for '{className}'")
   derivingHandlersRef.modify fun m => m.insert className handler
 
+def registerBuiltinDerivingHandler (className : Name) (handler : DerivingHandlerNoArgs) : IO Unit := do
+  registerBuiltinDerivingHandler' className fun typeNames _ => handler typeNames
+
 def defaultHandler (className : Name) (typeNames : Array Name) : CommandElabM Unit := do
   throwError "default handlers have not been implemented yet, class: '{className}' types: {typeNames}"
 
-def applyDerivingHandlers (className : Name) (typeNames : Array Name) : CommandElabM Unit := do
+def applyDerivingHandlers (className : Name) (typeNames : Array Name) (args? : Option Syntax) : CommandElabM Unit := do
   match (← derivingHandlersRef.get).find? className with
   | some handler =>
-    unless (← handler typeNames) do
+    unless (← handler typeNames args?) do
       defaultHandler className typeNames
   | none => defaultHandler className typeNames
 
 @[builtinCommandElab «deriving»] def elabDeriving : CommandElab
-  | `(deriving instance $[$classes],* for $[$declNames],*) => do
-     let classes ← classes.mapM resolveGlobalConstNoOverloadWithInfo
+  | `(deriving instance $[$classes $[with $argss?]?],* for $[$declNames],*) => do
      let declNames ← declNames.mapM resolveGlobalConstNoOverloadWithInfo
-     for cls in classes do
+     for cls in classes, args? in argss? do
        try
-         applyDerivingHandlers cls declNames
+         let className ← resolveGlobalConstNoOverloadWithInfo cls
+         withRef cls do applyDerivingHandlers className declNames args?
        catch ex =>
          logException ex
   | _ => throwUnsupportedSyntax
@@ -44,18 +48,22 @@ def applyDerivingHandlers (className : Name) (typeNames : Array Name) : CommandE
 structure DerivingClassView where
   ref : Syntax
   className : Name
+  args? : Option Syntax
 
-/- leading_parser optional (atomic ("deriving " >> notSymbol "instance") >> sepBy1 ident ", ") -/
+/- def derivingClasses  := sepBy1 (ident >> optional (" with " >> Term.structInst)) ", "
+leading_parser optional ("deriving " >> derivingClasses) -/
 def getOptDerivingClasses [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadInfoTree m] (optDeriving : Syntax) : m (Array DerivingClassView) := do
-  if optDeriving.isNone then
-    return #[]
-  else
-    optDeriving[0][1].getSepArgs.mapM fun ident => do
-      let className ← resolveGlobalConstNoOverloadWithInfo ident
-      return { ref := ident, className := className }
+  match optDeriving with
+  | `(Parser.Command.optDeriving| deriving $[$classes $[with $argss?]?],*) =>
+    let mut ret := #[]
+    for cls in classes, args? in argss? do
+      let className ← resolveGlobalConstNoOverloadWithInfo cls
+      ret := ret.push { ref := cls, className := className, args? }
+    return ret
+  | _ => return #[]
 
 def DerivingClassView.applyHandlers (view : DerivingClassView) (declNames : Array Name) : CommandElabM Unit :=
-  withRef view.ref do applyDerivingHandlers view.className declNames
+  withRef view.ref do applyDerivingHandlers view.className declNames view.args?
 
 builtin_initialize
   registerTraceClass `Elab.Deriving

src/Lean/Parser/Command.lean

@@ -45,7 +45,8 @@ def «axiom»          := leading_parser "axiom " >> declId >> declSig
 def «example»        := leading_parser "example " >> declSig >> declVal
 def inferMod         := leading_parser atomic (symbol "{" >> "}")
 def ctor             := leading_parser "\n| " >> declModifiers true >> ident >> optional inferMod >> optDeclSig
-def optDeriving      := leading_parser optional (atomic ("deriving " >> notSymbol "instance") >> sepBy1 ident ", ")
+def derivingClasses  := sepBy1 (ident >> optional (" with " >> Term.structInst)) ", "
+def optDeriving      := leading_parser optional (atomic ("deriving " >> notSymbol "instance") >> derivingClasses)
 def «inductive»      := leading_parser "inductive " >> declId >> optDeclSig >> optional (symbol ":=" <|> "where") >> many ctor >> optDeriving
 def classInductive   := leading_parser atomic (group (symbol "class " >> "inductive ")) >> declId >> optDeclSig >> optional (symbol ":=" <|> "where") >> many ctor >> optDeriving
 def structExplicitBinder := leading_parser atomic (declModifiers true >> "(") >> many1 ident >> optional inferMod >> optDeclSig >> optional Term.binderDefault >> ")"
@@ -63,7 +64,7 @@ def «structure»          := leading_parser
     >> optDeriving
 @[builtinCommandParser] def declaration := leading_parser
 declModifiers false >> («abbrev» <|> «def» <|> «theorem» <|> «constant» <|> «instance» <|> «axiom» <|> «example» <|> «inductive» <|> classInductive <|> «structure»)
-@[builtinCommandParser] def «deriving»     := leading_parser "deriving " >> "instance " >> sepBy1 ident ", " >> " for " >> sepBy1 ident ", "
+@[builtinCommandParser] def «deriving»     := leading_parser "deriving " >> "instance " >> derivingClasses >> " for " >> sepBy1 ident ", "
 @[builtinCommandParser] def «section»      := leading_parser "section " >> optional ident
 @[builtinCommandParser] def «namespace»    := leading_parser "namespace " >> ident
 @[builtinCommandParser] def «end»          := leading_parser "end " >> optional ident