From 4a3c172ac9837f11c68a75ff87da7afb2ea58eb4 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Mon, 19 Jul 2021 20:19:00 -0700 Subject: [PATCH] feat: parametrised deriving handlers --- src/Lean/Elab/Deriving/Basic.lean | 42 ++++++++++++++++++------------- src/Lean/Parser/Command.lean | 5 ++-- 2 files changed, 28 insertions(+), 19 deletions(-) diff --git a/src/Lean/Elab/Deriving/Basic.lean b/src/Lean/Elab/Deriving/Basic.lean index 734d77506d..4af4fb1ff5 100644 --- a/src/Lean/Elab/Deriving/Basic.lean +++ b/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 diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index fcdd1d24bf..2c7d9e5777 100644 --- a/src/Lean/Parser/Command.lean +++ b/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