Lean.Elab.Deriving.BEq

def Lean.Elab.Deriving.BEq.mkBEqHeader (ctx : Lean.Elab.Deriving.Context) (indVal : Lean.InductiveVal) :

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

Equations

Lean.Elab.Deriving.BEq.mkBEqHeader ctx indVal = Lean.Elab.Deriving.mkHeader ctx `BEq 2 indVal

def Lean.Elab.Deriving.BEq.mkMatch (ctx : Lean.Elab.Deriving.Context) (header : Lean.Elab.Deriving.Header) (indVal : Lean.InductiveVal) (auxFunName : Lean.Name) :

Lean.Elab.TermElabM Lean.Syntax

Equations

Lean.Elab.Deriving.BEq.mkMatch ctx header indVal auxFunName = (fun mkElseAlt mkAlts => do let discrs ← Lean.Elab.Deriving.mkDiscrs header indVal let alts ← mkAlts let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.match #[Lean.Syntax.atom info "match", Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] (Lean.mkSepArray (Array.map (fun discrs => discrs) discrs) (Lean.mkAtom ","))), Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info "with", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchAlts #[Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] alts)]])) (Lean.Elab.Deriving.BEq.mkMatch.mkElseAlt indVal) (Lean.Elab.Deriving.BEq.mkMatch.mkAlts indVal auxFunName)

source

def Lean.Elab.Deriving.BEq.mkMatch.mkElseAlt (indVal : Lean.InductiveVal) :

Lean.Elab.TermElabM Lean.Syntax

Equations

Lean.Elab.Deriving.BEq.mkMatch.mkElseAlt indVal = let patterns := #[]; do let r ← let col := { start := 0, stop := indVal.numIndices, step := 1 }; forIn col patterns fun i r => let patterns := r; do let a ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.hole #[Lean.Syntax.atom info "_"]) let patterns : Array Lean.Syntax := Array.push patterns a pure PUnit.unit pure (ForInStep.yield patterns) let x : Array Lean.Syntax := r let patterns : Array Lean.Syntax := x let a ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.hole #[Lean.Syntax.atom info "_"]) let patterns : Array Lean.Syntax := Array.push patterns a let a ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.hole #[Lean.Syntax.atom info "_"]) let patterns : Array Lean.Syntax := Array.push patterns a let altRhs ← do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.ident info (String.toSubstring "false") (Lean.addMacroScope mainModule `false scp) [(`Bool.false, [])]) let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchAlt #[Lean.Syntax.atom info "|", Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] (Lean.mkSepArray (Array.map (fun patterns => patterns) patterns) (Lean.mkAtom ","))), Lean.Syntax.atom info "=>", altRhs])

source

def Lean.Elab.Deriving.BEq.mkMatch.mkAlts (indVal : Lean.InductiveVal) (auxFunName : Lean.Name) :

Lean.Elab.TermElabM (Array Lean.Syntax)

Equations

Lean.Elab.Deriving.BEq.mkMatch.mkAlts indVal auxFunName = let alts := #[]; do let r ← let col := indVal.ctors; forIn col alts fun ctorName r => let alts := r; do let ctorInfo ← Lean.getConstInfoCtor ctorName let alt ← Lean.Meta.forallTelescopeReducing ctorInfo.toConstantVal.type fun xs type => do let type ← liftM (Lean.Core.betaReduce type) let patterns : Array Lean.Syntax := #[] let r ← let col := { start := 0, stop := indVal.numIndices, step := 1 }; forIn col patterns fun i r => let patterns := r; do let a ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.hole #[Lean.Syntax.atom info "_"]) let patterns : Array Lean.Syntax := Array.push patterns a pure PUnit.unit pure (ForInStep.yield patterns) let x : Array Lean.Syntax := r let patterns : Array Lean.Syntax := x let ctorArgs1 : Array Lean.Syntax := #[] let ctorArgs2 : Array Lean.Syntax := #[] let rhs ← do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.ident info (String.toSubstring "true") (Lean.addMacroScope mainModule `true scp) [(`Bool.true, [])]) let r ← let col := { start := 0, stop := indVal.numParams, step := 1 }; forIn col { fst := ctorArgs1, snd := ctorArgs2 } fun i r => let ctorArgs1 := r.fst; let ctorArgs2 := r.snd; do let a ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.hole #[Lean.Syntax.atom info "_"]) let ctorArgs1 : Array Lean.Syntax := Array.push ctorArgs1 a let a ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.hole #[Lean.Syntax.atom info "_"]) let ctorArgs2 : Array Lean.Syntax := Array.push ctorArgs2 a pure PUnit.unit pure (ForInStep.yield { fst := ctorArgs1, snd := ctorArgs2 }) let x : MProd (Array Lean.Syntax) (Array Lean.Syntax) := r match x with | { fst := ctorArgs1, snd := ctorArgs2 } => do let r ← let col := { start := 0, stop := ctorInfo.numFields, step := 1 }; forIn col { fst := ctorArgs1, snd := { fst := ctorArgs2, snd := rhs } } fun i r => let ctorArgs1 := r.fst; let x := r.snd; let ctorArgs2 := x.fst; let rhs := x.snd; let x := Array.getOp xs (indVal.numParams + i); if Lean.Expr.containsFVar type (Lean.Expr.fvarId! x) = true then do let a ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.hole #[Lean.Syntax.atom info "_"]) let ctorArgs1 : Array Lean.Syntax := Array.push ctorArgs1 a let a ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.hole #[Lean.Syntax.atom info "_"]) let ctorArgs2 : Array Lean.Syntax := Array.push ctorArgs2 a pure PUnit.unit pure (ForInStep.yield { fst := ctorArgs1, snd := { fst := ctorArgs2, snd := rhs } }) else do let a ← liftM (Lean.mkFreshUserName `a) let a : Lean.Syntax := Lean.mkIdent a let a_1 ← liftM (Lean.mkFreshUserName `b) let b : Lean.Syntax := Lean.mkIdent a_1 let ctorArgs1 : Array Lean.Syntax := Array.push ctorArgs1 a let ctorArgs2 : Array Lean.Syntax := Array.push ctorArgs2 b let a_2 ← liftM (Lean.Meta.inferType x) if Lean.Expr.isAppOf a_2 indVal.toConstantVal.name = true then do let r ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `«term_&&_» #[rhs, Lean.Syntax.atom info "&&", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.mkIdent auxFunName, Lean.Syntax.node Lean.SourceInfo.none `null #[a, b]]]) let rhs : Lean.Syntax := r pure PUnit.unit pure (ForInStep.yield { fst := ctorArgs1, snd := { fst := ctorArgs2, snd := rhs } }) else do let r ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `«term_&&_» #[rhs, Lean.Syntax.atom info "&&", Lean.Syntax.node Lean.SourceInfo.none `«term_==_» #[a, Lean.Syntax.atom info "==", b]]) let rhs : Lean.Syntax := r pure PUnit.unit pure (ForInStep.yield { fst := ctorArgs1, snd := { fst := ctorArgs2, snd := rhs } }) let x : MProd (Array Lean.Syntax) (MProd (Array Lean.Syntax) Lean.Syntax) := r match x with | { fst := ctorArgs1, snd := { fst := ctorArgs2, snd := rhs } } => do let a ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.explicit #[Lean.Syntax.atom info "@", Lean.mkIdent ctorName], Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] ctorArgs1)]) let patterns : Array Lean.Syntax := Array.push patterns a let a ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.explicit #[Lean.Syntax.atom info "@", Lean.mkIdent ctorName], Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] ctorArgs2)]) let patterns : Array Lean.Syntax := Array.push patterns a let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchAlt #[Lean.Syntax.atom info "|", Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] (Lean.mkSepArray (Array.map (fun patterns => patterns) patterns) (Lean.mkAtom ","))), Lean.Syntax.atom info "=>", rhs]) let alts : Array Lean.Syntax := Array.push alts alt pure PUnit.unit pure (ForInStep.yield alts) let x : Array Lean.Syntax := r let alts : Array Lean.Syntax := x let a ← Lean.Elab.Deriving.BEq.mkMatch.mkElseAlt indVal let alts : Array Lean.Syntax := Array.push alts a pure alts

source

def Lean.Elab.Deriving.BEq.mkAuxFunction (ctx : Lean.Elab.Deriving.Context) (i : Nat) :

Lean.Elab.TermElabM Lean.Syntax

Equations

Lean.Elab.Deriving.BEq.mkAuxFunction ctx i = do let auxFunName ← pure (Array.getOp ctx.auxFunNames i) let indVal ← pure (Array.getOp ctx.typeInfos i) let header ← Lean.Elab.Deriving.BEq.mkBEqHeader ctx indVal let body ← Lean.Elab.Deriving.BEq.mkMatch ctx header indVal auxFunName let _do_jp : Lean.Syntax → PUnit → Lean.Elab.TermElabM Lean.Syntax := fun body y => let binders := header.binders; if ctx.usePartial = true then do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← 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 `Lean.Parser.Command.private #[Lean.Syntax.atom info "private"]], 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.partial #[Lean.Syntax.atom info "partial"]]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.def #[Lean.Syntax.atom info "def", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.declId #[Lean.mkIdent auxFunName, Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.optDeclSig #[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 ":", Lean.Syntax.ident info (String.toSubstring "Bool") (Lean.addMacroScope mainModule `Bool scp) [(`Bool, [])]]]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.declValSimple #[Lean.Syntax.atom info ":=", body, 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 #[]]]) else do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← 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 `Lean.Parser.Command.private #[Lean.Syntax.atom info "private"]], 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.def #[Lean.Syntax.atom info "def", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.declId #[Lean.mkIdent auxFunName, Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.optDeclSig #[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 ":", Lean.Syntax.ident info (String.toSubstring "Bool") (Lean.addMacroScope mainModule `Bool scp) [(`Bool, [])]]]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.declValSimple #[Lean.Syntax.atom info ":=", body, 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 #[]]]) if ctx.usePartial = true then do let letDecls ← Lean.Elab.Deriving.mkLocalInstanceLetDecls ctx `BEq header.argNames let r ← Lean.Elab.Deriving.mkLet letDecls body let body : Lean.Syntax := r let y ← pure PUnit.unit _do_jp body y else do let y ← pure PUnit.unit _do_jp body y

source

def Lean.Elab.Deriving.BEq.mkMutualBlock (ctx : Lean.Elab.Deriving.Context) :

Lean.Elab.TermElabM Lean.Syntax

Equations

Lean.Elab.Deriving.BEq.mkMutualBlock ctx = let auxDefs := #[]; do let r ← let col := { start := 0, stop := Array.size ctx.typeInfos, step := 1 }; forIn col auxDefs fun i r => let auxDefs := r; do let a ← Lean.Elab.Deriving.BEq.mkAuxFunction ctx i let auxDefs : Array Lean.Syntax := Array.push auxDefs a pure PUnit.unit pure (ForInStep.yield auxDefs) let x : Array Lean.Syntax := r let auxDefs : Array Lean.Syntax := x let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.mutual #[Lean.Syntax.atom info "mutual", Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.set_option #[Lean.Syntax.atom info "set_option", Lean.Syntax.ident info (String.toSubstring "match.ignoreUnusedAlts") (Lean.addMacroScope mainModule `match.ignoreUnusedAlts scp) [(`Lean.Parser.Term.match, ["ignoreUnusedAlts"])], Lean.Syntax.atom info "true"]] auxDefs), Lean.Syntax.atom info "end", Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[]])

source

def Lean.Elab.Deriving.BEq.mkBEqInstanceHandler (declNames : Array Lean.Name) :

Lean.Elab.Command.CommandElabM Bool

Equations

Lean.Elab.Deriving.BEq.mkBEqInstanceHandler declNames = do let a ← Lean.isEnumType (Array.getOp declNames 0) if (Array.size declNames == 1 && a) = true then do let cmds ← Lean.Elab.Command.liftTermElabM none (Lean.Elab.Deriving.BEq.mkBEqEnumCmd (Array.getOp declNames 0)) Array.forM Lean.Elab.Command.elabCommand cmds 0 (Array.size cmds) pure true else do let a ← Array.allM Lean.isInductive declNames 0 (Array.size declNames) if (a && decide (Array.size declNames > 0)) = true then do let cmds ← Lean.Elab.Command.liftTermElabM none (Lean.Elab.Deriving.BEq.mkBEqInstanceCmds declNames) Array.forM Lean.Elab.Command.elabCommand cmds 0 (Array.size cmds) pure true else pure false