Lean.Elab.Deriving.Basic

source

noncomputable def Lean.Elab.DerivingHandler :

Type

Equations

Lean.Elab.DerivingHandler = (Array Lean.Name → Option Lean.Syntax → Lean.Elab.Command.CommandElabM Bool)

source

noncomputable def Lean.Elab.DerivingHandlerNoArgs :

Type

Equations

Lean.Elab.DerivingHandlerNoArgs = (Array Lean.Name → Lean.Elab.Command.CommandElabM Bool)

source

constant Lean.Elab.derivingHandlersRef :

IO.Ref (Lean.NameMap Lean.Elab.DerivingHandler)

source

def Lean.Elab.registerBuiltinDerivingHandlerWithArgs (className : Lean.Name) (handler : Lean.Elab.DerivingHandler) :

IO Unit

Equations

Lean.Elab.registerBuiltinDerivingHandlerWithArgs className handler = do let a ← Lean.initializing let _do_jp : PUnit → IO Unit := fun y => do let a ← ST.Ref.get Lean.Elab.derivingHandlersRef let _do_jp : PUnit → IO Unit := fun y => ST.Ref.modify Lean.Elab.derivingHandlersRef fun m => Lean.NameMap.insert m className handler if Lean.NameMap.contains a className = true then do let y ← throw (IO.userError (toString "failed to register deriving handler, a handler has already been registered for '" ++ toString className ++ toString "'")) _do_jp y else do let y ← pure PUnit.unit _do_jp y if a = true then do let y ← pure PUnit.unit _do_jp y else do let y ← throw (IO.userError "failed to register deriving handler, it can only be registered during initialization") _do_jp y

source

def Lean.Elab.registerBuiltinDerivingHandler (className : Lean.Name) (handler : Lean.Elab.DerivingHandlerNoArgs) :

IO Unit

Equations

Lean.Elab.registerBuiltinDerivingHandler className handler = Lean.Elab.registerBuiltinDerivingHandlerWithArgs className fun typeNames x => handler typeNames

source

def Lean.Elab.defaultHandler (className : Lean.Name) (typeNames : Array Lean.Name) :

Lean.Elab.Command.CommandElabM Unit

Equations

Lean.Elab.defaultHandler className typeNames = Lean.throwError (Lean.toMessageData "default handlers have not been implemented yet, class: '" ++ Lean.toMessageData className ++ Lean.toMessageData "' types: " ++ Lean.toMessageData typeNames ++ Lean.toMessageData "")

source

def Lean.Elab.applyDerivingHandlers (className : Lean.Name) (typeNames : Array Lean.Name) (args? : Option Lean.Syntax) :

Lean.Elab.Command.CommandElabM Unit

Equations

Lean.Elab.applyDerivingHandlers className typeNames args? = do let a ← ST.Ref.get Lean.Elab.derivingHandlersRef match Lean.NameMap.find? a className with | some handler => do let a ← handler typeNames args? if a = true then pure PUnit.unit else Lean.Elab.defaultHandler className typeNames | none => Lean.Elab.defaultHandler className typeNames

source

def Lean.Elab.elabDeriving :

Lean.Elab.Command.CommandElab

Equations

Lean.Elab.elabDeriving x = let discr := x; if Lean.Syntax.isOfKind discr `Lean.Parser.Command.deriving = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr_2 := Lean.Syntax.getArg discr 1; let discr_3 := Lean.Syntax.getArg discr 2; match OptionM.run (Array.sequenceMap (Array.getSepElems (Lean.Syntax.getArgs discr_3)) fun x => let discr := x; if Lean.Syntax.isOfKind discr `group = true then let discr_4 := Lean.Syntax.getArg discr 0; let discr_5 := Lean.Syntax.getArg discr 1; let yes := fun x argss? => let classes := discr_4; some (classes, argss?); if Lean.Syntax.isNone discr_5 = true then yes () none else let discr_6 := discr_5; if Lean.Syntax.matchesNull discr_6 2 = true then let discr := Lean.Syntax.getArg discr_6 0; let discr := Lean.Syntax.getArg discr_6 1; let argss? := discr; yes () (some argss?) else let discr_7 := discr_5; let discr := Lean.Syntax.getArg discr 1; none else let discr := x; none) with | some tuples => let argss? := Array.map (fun x => match x with | (classes, argss?) => argss?) tuples; let classes := Array.map (fun x => match x with | (classes, argss?) => classes) tuples; let discr_4 := Lean.Syntax.getArg discr 3; let discr_5 := Lean.Syntax.getArg discr 4; match OptionM.run (Array.sequenceMap (Array.getSepElems (Lean.Syntax.getArgs discr_5)) fun x => let discr := x; let declNames := discr; some declNames) with | some declNames => do let declNames ← Array.mapM (fun id => Lean.Elab.resolveGlobalConstNoOverloadWithInfo id) declNames let s : Subarray (Option Lean.Syntax) := toStream argss? let r ← forIn classes s fun cls r => let s := r; match Stream.next? s with | none => pure (ForInStep.done s) | some (args?, s') => let s := s'; do tryCatch (do let className ← Lean.Elab.resolveGlobalConstNoOverloadWithInfo cls Lean.withRef cls (let _do_jp := fun y => Lean.Elab.applyDerivingHandlers className declNames args?; if (Array.size declNames == 1 && Option.isNone args?) = true then do let a ← Lean.Elab.tryApplyDefHandler className (Array.getOp declNames 0) if a = true then pure () else do let y ← pure PUnit.unit _do_jp y else do let y ← pure PUnit.unit _do_jp y)) fun ex => Lean.Elab.logException ex pure (ForInStep.yield s) let x : Subarray (Option Lean.Syntax) := r let s : Subarray (Option Lean.Syntax) := x pure PUnit.unit | none => let discr := Lean.Syntax.getArg discr 4; Lean.Elab.throwUnsupportedSyntax | none => let discr_4 := Lean.Syntax.getArg discr 2; let discr_5 := Lean.Syntax.getArg discr 3; let discr := Lean.Syntax.getArg discr 4; Lean.Elab.throwUnsupportedSyntax else let discr := x; Lean.Elab.throwUnsupportedSyntax

source

structure Lean.Elab.DerivingClassView :

Type

ref : Lean.Syntax
className : Lean.Name
args? : Option Lean.Syntax

source

def Lean.Elab.getOptDerivingClasses {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadResolveName m] [inst : Lean.MonadError m] [inst : Lean.Elab.MonadInfoTree m] (optDeriving : Lean.Syntax) :

m (Array Lean.Elab.DerivingClassView)

Equations

Lean.Elab.getOptDerivingClasses optDeriving = let discr := optDeriving; if Lean.Syntax.isOfKind discr `Lean.Parser.Command.optDeriving = true then let discr_1 := Lean.Syntax.getArg discr 0; if Lean.Syntax.matchesNull discr_1 2 = true then let discr := Lean.Syntax.getArg discr_1 0; let discr := Lean.Syntax.getArg discr_1 1; match OptionM.run (Array.sequenceMap (Array.getSepElems (Lean.Syntax.getArgs discr)) fun x => let discr := x; if Lean.Syntax.isOfKind discr `group = true then let discr_2 := Lean.Syntax.getArg discr 0; let discr_3 := Lean.Syntax.getArg discr 1; let yes := fun x argss? => let classes := discr_2; some (classes, argss?); if Lean.Syntax.isNone discr_3 = true then yes () none else let discr_4 := discr_3; if Lean.Syntax.matchesNull discr_4 2 = true then let discr := Lean.Syntax.getArg discr_4 0; let discr := Lean.Syntax.getArg discr_4 1; let argss? := discr; yes () (some argss?) else let discr_5 := discr_3; let discr := Lean.Syntax.getArg discr 1; none else let discr := x; none) with | some tuples => let argss? := Array.map (fun x => match x with | (classes, argss?) => argss?) tuples; let classes := Array.map (fun x => match x with | (classes, argss?) => classes) tuples; let ret := #[]; let s := toStream argss?; do let r ← forIn classes { fst := s, snd := ret } fun cls r => let s := r.fst; let ret := r.snd; match Stream.next? s with | none => pure (ForInStep.done { fst := s, snd := ret }) | some (args?, s') => let s := s'; do let className ← Lean.Elab.resolveGlobalConstNoOverloadWithInfo cls let ret : Array Lean.Elab.DerivingClassView := Array.push ret { ref := cls, className := className, args? := args? } pure PUnit.unit pure (ForInStep.yield { fst := s, snd := ret }) let x : MProd (Subarray (Option Lean.Syntax)) (Array Lean.Elab.DerivingClassView) := r match x with | { fst := s, snd := ret } => pure ret | none => let discr := Lean.Syntax.getArg discr_1 1; pure #[] else let discr := Lean.Syntax.getArg discr 0; pure #[] else let discr := optDeriving; pure #[]

source

def Lean.Elab.DerivingClassView.applyHandlers (view : Lean.Elab.DerivingClassView) (declNames : Array Lean.Name) :

Lean.Elab.Command.CommandElabM Unit

Equations

Lean.Elab.DerivingClassView.applyHandlers view declNames = Lean.withRef view.ref (Lean.Elab.applyDerivingHandlers view.className declNames view.args?)