Lean.Elab.Deriving.Util

Lean.Elab.Deriving.mkInstImplicitBinders className indVal argNames = Lean.Meta.forallBoundedTelescope indVal.toConstantVal.type (some indVal.numParams) fun xs x => let binders := #[]; do let r ← let col := { start := 0, stop := Array.size xs, step := 1 }; forIn col binders fun i r => let binders := r; do let r ← tryCatch (let x := Array.getOp xs i; do let c ← liftM (Lean.Meta.mkAppM className #[x]) let a ← liftM (Lean.Meta.isTypeCorrect c) if a = true then let argName := Array.getOp argNames i; do let binder ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.instBinder #[Lean.Syntax.atom info "[", Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.mkIdent className, Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.mkIdent argName]], Lean.Syntax.atom info "]"]) let binders : Array Lean.Syntax := Array.push binders binder let y ← pure PUnit.unit pure { fst := y, snd := binders } else do let y ← pure PUnit.unit pure { fst := y, snd := binders }) fun x => do let y ← pure () pure { fst := y, snd := binders } let x : Array Lean.Syntax := r.snd let binders : Array Lean.Syntax := x pure r.fst pure (ForInStep.yield binders) let x : Array Lean.Syntax := r let binders : Array Lean.Syntax := x pure binders

source

structure Lean.Elab.Deriving.Context :

Type

typeInfos : Array Lean.InductiveVal
auxFunNames : Array Lean.Name
usePartial : Bool

source

def Lean.Elab.Deriving.mkContext (fnPrefix : String) (typeName : Lean.Name) :

Lean.Elab.TermElabM Lean.Elab.Deriving.Context

Equations

Lean.Elab.Deriving.mkContext fnPrefix typeName = do let indVal ← Lean.getConstInfoInduct typeName let typeInfos : Array Lean.InductiveVal := #[] let r ← let col := indVal.all; forIn col typeInfos fun typeName r => let typeInfos := r; do let a ← Lean.getConstInfoInduct typeName let r ← pure (Array.push typeInfos a) let typeInfos : Array Lean.InductiveVal := r pure PUnit.unit pure (ForInStep.yield typeInfos) let x : Array Lean.InductiveVal := r let typeInfos : Array Lean.InductiveVal := x let auxFunNames : Array Lean.Name := #[] let r ← let col := indVal.all; forIn col auxFunNames fun typeName r => let auxFunNames := r; match Lean.Name.eraseMacroScopes typeName with | Lean.Name.str x t x_1 => do let a ← liftM (Lean.mkFreshUserName (Lean.Name.mkSimple (fnPrefix ++ t))) let auxFunNames : Array Lean.Name := Array.push auxFunNames a pure PUnit.unit pure (ForInStep.yield auxFunNames) | x => do let a ← liftM (Lean.mkFreshUserName `instFn) let auxFunNames : Array Lean.Name := Array.push auxFunNames a pure PUnit.unit pure (ForInStep.yield auxFunNames) let x : Array Lean.Name := r let auxFunNames : Array Lean.Name := x let cls : Lean.Name := `Elab.Deriving.beq let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.Elab.TermElabM Lean.Elab.Deriving.Context := fun y => let usePartial := indVal.isNested || decide (Array.size typeInfos > 1); pure { typeInfos := typeInfos, auxFunNames := auxFunNames, usePartial := usePartial } if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "" ++ Lean.toMessageData auxFunNames ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y

source

def Lean.Elab.Deriving.mkLocalInstanceLetDecls (ctx : Lean.Elab.Deriving.Context) (className : Lean.Name) (argNames : Array Lean.Name) :

Lean.Elab.TermElabM (Array Lean.Syntax)

Equations

Lean.Elab.Deriving.mkLocalInstanceLetDecls ctx className argNames = let letDecls := #[]; do let r ← let col := { start := 0, stop := Array.size ctx.typeInfos, step := 1 }; forIn col letDecls fun i r => let letDecls := r; let indVal := Array.getOp ctx.typeInfos i; let auxFunName := Array.getOp ctx.auxFunNames i; do let currArgNames ← Lean.Elab.Deriving.mkInductArgNames indVal let numParams : Nat := indVal.numParams let currIndices : Subarray Lean.Name := let a := currArgNames; Array.toSubarray a numParams (Array.size a) let binders ← Lean.Elab.Deriving.mkImplicitBinders (Array.ofSubarray currIndices) let argNamesNew : Subarray Lean.Name := Array.toSubarray argNames 0 numParams ++ currIndices let indType ← Lean.Elab.Deriving.mkInductiveApp indVal (Array.ofSubarray argNamesNew) let type ← do let _ ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.mkIdent className, Lean.Syntax.node Lean.SourceInfo.none `null #[indType]]) let val ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.anonymousCtor #[Lean.Syntax.atom info "⟨", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.mkIdent auxFunName], Lean.Syntax.atom info "⟩"]) let instName ← liftM (Lean.mkFreshUserName `localinst) let letDecl ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.letDecl #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.letIdDecl #[Lean.mkIdent instName, Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] binders), Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.typeSpec #[Lean.Syntax.atom info ":", type]], Lean.Syntax.atom info ":=", val]]) let letDecls : Array Lean.Syntax := Array.push letDecls letDecl pure PUnit.unit pure (ForInStep.yield letDecls) let x : Array Lean.Syntax := r let letDecls : Array Lean.Syntax := x pure letDecls

source

def Lean.Elab.Deriving.mkLet (letDecls : Array Lean.Syntax) (body : Lean.Syntax) :

Lean.Elab.TermElabM Lean.Syntax

Equations

Lean.Elab.Deriving.mkLet letDecls body = Array.foldrM (fun letDecl body => do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.let #[Lean.Syntax.atom info "let", letDecl, Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"], body])) body letDecls (Array.size letDecls)

source

def Lean.Elab.Deriving.mkInstanceCmds (ctx : Lean.Elab.Deriving.Context) (className : Lean.Name) (typeNames : Array Lean.Name) (useAnonCtor : optParam Bool true) :

Lean.Elab.TermElabM (Array Lean.Syntax)

Equations

Lean.Elab.Deriving.mkInstanceCmds ctx className typeNames useAnonCtor = let instances := #[]; do let r ← let col := { start := 0, stop := Array.size ctx.typeInfos, step := 1 }; forIn col instances fun i r => let instances := r; let indVal := Array.getOp ctx.typeInfos i; if Array.contains typeNames indVal.toConstantVal.name = true then let auxFunName := Array.getOp ctx.auxFunNames i; do let argNames ← Lean.Elab.Deriving.mkInductArgNames indVal let binders ← Lean.Elab.Deriving.mkImplicitBinders argNames let a ← Lean.Elab.Deriving.mkInstImplicitBinders className indVal argNames let binders : Array Lean.Syntax := binders ++ a let indType ← Lean.Elab.Deriving.mkInductiveApp indVal argNames let type ← do let _ ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.mkIdent className, Lean.Syntax.node Lean.SourceInfo.none `null #[indType]]) let _do_jp : Array Lean.Syntax → Lean.Syntax → Lean.Elab.TermElabM (ForInStep (Array Lean.Syntax)) := fun instances val => do let instCmd ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.declaration #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.declModifiers #[Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.instance #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.attrKind #[Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info "instance", Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.declSig #[Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] binders), Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.typeSpec #[Lean.Syntax.atom info ":", type]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.declValSimple #[Lean.Syntax.atom info ":=", val, Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[]]]) let instances : Array Lean.Syntax := Array.push instances instCmd pure PUnit.unit pure (ForInStep.yield instances) if useAnonCtor = true then do let y ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.anonymousCtor #[Lean.Syntax.atom info "⟨", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.mkIdent auxFunName], Lean.Syntax.atom info "⟩"]) _do_jp instances y else do let y ← pure (Lean.mkIdent auxFunName) _do_jp instances y else do pure PUnit.unit pure (ForInStep.yield instances) let x : Array Lean.Syntax := r let instances : Array Lean.Syntax := x pure instances

source

def Lean.Elab.Deriving.mkDiscr (varName : Lean.Name) :

Lean.Elab.TermElabM Lean.Syntax

Equations

Lean.Elab.Deriving.mkDiscr varName = do let _ ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchDiscr #[Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.mkIdent varName])

source

structure Lean.Elab.Deriving.Header :

Type

source

def Lean.Elab.Deriving.mkHeader (ctx : Lean.Elab.Deriving.Context) (className : Lean.Name) (arity : Nat) (indVal : Lean.InductiveVal) :

Lean.Elab.TermElabM Lean.Elab.Deriving.Header

Equations

Lean.Elab.Deriving.mkHeader ctx className arity indVal = do let argNames ← Lean.Elab.Deriving.mkInductArgNames indVal let binders ← Lean.Elab.Deriving.mkImplicitBinders argNames let targetType ← Lean.Elab.Deriving.mkInductiveApp indVal argNames let targetNames : Array Lean.Name := #[] let r ← let col := { start := 0, stop := arity, step := 1 }; forIn col targetNames fun i r => let targetNames := r; do let a ← liftM (Lean.mkFreshUserName `x) let targetNames : Array Lean.Name := Array.push targetNames a pure PUnit.unit pure (ForInStep.yield targetNames) let x : Array Lean.Name := r let targetNames : Array Lean.Name := x let a ← Lean.Elab.Deriving.mkInstImplicitBinders className indVal argNames let binders : Array Lean.Syntax := binders ++ a let a ← Array.mapM (fun targetName => do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.explicitBinder #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.mkIdent targetName], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ":", targetType], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info ")"])) targetNames let binders : Array Lean.Syntax := binders ++ a pure { binders := binders, argNames := argNames, targetNames := targetNames, targetType := targetType }

source

def Lean.Elab.Deriving.mkDiscrs (header : Lean.Elab.Deriving.Header) (indVal : Lean.InductiveVal) :

Lean.Elab.TermElabM (Array Lean.Syntax)

Equations

Lean.Elab.Deriving.mkDiscrs header indVal = let discrs := #[]; do let r ← let col := let a := header.argNames; Array.toSubarray a indVal.numParams (Array.size a); forIn col discrs fun argName r => let discrs := r; do let a ← Lean.Elab.Deriving.mkDiscr argName let discrs : Array Lean.Syntax := Array.push discrs a pure PUnit.unit pure (ForInStep.yield discrs) let x : Array Lean.Syntax := r let discrs : Array Lean.Syntax := x let a ← Array.mapM Lean.Elab.Deriving.mkDiscr header.targetNames pure (discrs ++ a)