def
Lean.Elab.Deriving.DecEq.mkDecEqHeader
(ctx : Lean.Elab.Deriving.Context)
(indVal : Lean.InductiveVal)
:
Equations
- Lean.Elab.Deriving.DecEq.mkDecEqHeader ctx indVal = Lean.Elab.Deriving.mkHeader ctx `DecidableEq 2 indVal
def
Lean.Elab.Deriving.DecEq.mkMatch
(ctx : Lean.Elab.Deriving.Context)
(header : Lean.Elab.Deriving.Header)
(indVal : Lean.InductiveVal)
(auxFunName : Lean.Name)
(argNames : Array Lean.Name)
:
Equations
- Lean.Elab.Deriving.DecEq.mkMatch ctx header indVal auxFunName argNames = (fun mkSameCtorRhs 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.DecEq.mkMatch.mkSameCtorRhs auxFunName) (Lean.Elab.Deriving.DecEq.mkMatch.mkAlts indVal auxFunName)
Equations
- Lean.Elab.Deriving.DecEq.mkMatch.mkSameCtorRhs auxFunName [] = do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "isTrue") (Lean.addMacroScope mainModule `isTrue scp) [(`Decidable.isTrue, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "rfl") (Lean.addMacroScope mainModule `rfl scp) [(`rfl, [])]]])
- Lean.Elab.Deriving.DecEq.mkMatch.mkSameCtorRhs auxFunName ((a, b, recField) :: todo) = Lean.withFreshMacroScope do let a ← Lean.Elab.Deriving.DecEq.mkMatch.mkSameCtorRhs auxFunName todo let rhs ← do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `termDepIfThenElse #[Lean.Syntax.atom info "if", Lean.Syntax.ident info (String.toSubstring "h") (Lean.addMacroScope mainModule `h scp) [], Lean.Syntax.atom info ":", Lean.Syntax.node Lean.SourceInfo.none `«term_=_» #[a, Lean.Syntax.atom info "=", b], Lean.Syntax.atom info "then", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.byTactic #[Lean.Syntax.atom info "by", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.tacticSeq #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.tacticSeq1Indented #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `group #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.subst #[Lean.Syntax.atom info "subst", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "h") (Lean.addMacroScope mainModule `h scp) []]], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"]], Lean.Syntax.node Lean.SourceInfo.none `group #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.exact #[Lean.Syntax.atom info "exact", a], Lean.Syntax.node Lean.SourceInfo.none `null #[]]]]]], Lean.Syntax.atom info "else", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "isFalse") (Lean.addMacroScope mainModule `isFalse scp) [(`Decidable.isFalse, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.byTactic #[Lean.Syntax.atom info "by", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.tacticSeq #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.tacticSeq1Indented #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `group #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.intro #[Lean.Syntax.atom info "intro", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "n") (Lean.addMacroScope mainModule `n scp) []]], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"]], Lean.Syntax.node Lean.SourceInfo.none `group #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.injection #[Lean.Syntax.atom info "injection", Lean.Syntax.ident info (String.toSubstring "n") (Lean.addMacroScope mainModule `n scp) [], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"]], Lean.Syntax.node Lean.SourceInfo.none `group #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.apply #[Lean.Syntax.atom info "apply", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "h") (Lean.addMacroScope mainModule `h scp) [], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.hole #[Lean.Syntax.atom info "_"]]]], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"]], Lean.Syntax.node Lean.SourceInfo.none `group #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.assumption #[Lean.Syntax.atom info "assumption"], Lean.Syntax.node Lean.SourceInfo.none `null #[]]]]]], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"]]]]) if recField = 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.Term.let #[Lean.Syntax.atom info "let", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.letDecl #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.letIdDecl #[Lean.Syntax.ident info (String.toSubstring "inst") (Lean.addMacroScope mainModule `inst scp) [], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[], 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]]]], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"], rhs]) else pure rhs
Equations
- Lean.Elab.Deriving.DecEq.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 r ← let col := indVal.ctors; forIn col alts fun ctorName₂ r => let alts := r; 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 if (ctorName₁ == ctorName₂) = true then do let alt ← Lean.Meta.forallTelescopeReducing ctorInfo.toConstantVal.type fun xs type => do let type ← liftM (Lean.Core.betaReduce type) let patterns : Array Lean.Syntax := patterns let ctorArgs1 : Array Lean.Syntax := #[] let ctorArgs2 : Array Lean.Syntax := #[] 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 } => let todo := #[]; do let r ← let col := { start := 0, stop := ctorInfo.numFields, step := 1 }; forIn col { fst := ctorArgs1, snd := { fst := ctorArgs2, snd := todo } } fun i r => let ctorArgs1 := r.fst; let x := r.snd; let ctorArgs2 := x.fst; let todo := 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 := todo } }) 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) let recField : Bool := Lean.Expr.isAppOf a_2 indVal.toConstantVal.name let todo : Array (Lean.Syntax × Lean.Syntax × Bool) := Array.push todo (a, b, recField) pure PUnit.unit pure (ForInStep.yield { fst := ctorArgs1, snd := { fst := ctorArgs2, snd := todo } }) let x : MProd (Array Lean.Syntax) (MProd (Array Lean.Syntax) (Array (Lean.Syntax × Lean.Syntax × Bool))) := r match x with | { fst := ctorArgs1, snd := { fst := ctorArgs2, snd := todo } } => 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 rhs ← Lean.Elab.Deriving.DecEq.mkMatch.mkSameCtorRhs auxFunName (Array.toList todo) 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) else do let a ← liftM (Lean.Meta.compatibleCtors ctorName₁ ctorName₂) if a = 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.app #[Lean.mkIdent ctorName₁, Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.ellipsis #[Lean.Syntax.atom info ".."]]]) let a_1 ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.mkIdent ctorName₂, Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.ellipsis #[Lean.Syntax.atom info ".."]]]) let patterns : Array Lean.Syntax := patterns ++ #[a, a_1] let rhs ← do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "isFalse") (Lean.addMacroScope mainModule `isFalse scp) [(`Decidable.isFalse, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.byTactic #[Lean.Syntax.atom info "by", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.tacticSeq #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.tacticSeq1Indented #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `group #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.intro #[Lean.Syntax.atom info "intro", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "h") (Lean.addMacroScope mainModule `h scp) []]], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"]], Lean.Syntax.node Lean.SourceInfo.none `group #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.injection #[Lean.Syntax.atom info "injection", Lean.Syntax.ident info (String.toSubstring "h") (Lean.addMacroScope mainModule `h scp) [], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.node Lean.SourceInfo.none `null #[]]]]]], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"]]]) let a ← do 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 r ← pure (Array.push alts a) let alts : Array Lean.Syntax := r pure PUnit.unit pure (ForInStep.yield alts) else do pure PUnit.unit pure (ForInStep.yield alts) let x : Array Lean.Syntax := r let alts : Array Lean.Syntax := x pure PUnit.unit pure (ForInStep.yield alts) let x : Array Lean.Syntax := r let alts : Array Lean.Syntax := x pure alts
Equations
- Lean.Elab.Deriving.DecEq.mkAuxFunction ctx = do let auxFunName ← pure (Array.getOp ctx.auxFunNames 0) let indVal ← pure (Array.getOp ctx.typeInfos 0) let header ← Lean.Elab.Deriving.DecEq.mkDecEqHeader ctx indVal let body ← Lean.Elab.Deriving.DecEq.mkMatch ctx header indVal auxFunName header.argNames let binders : Array Lean.Syntax := header.binders let type ← do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "Decidable") (Lean.addMacroScope mainModule `Decidable scp) [(`Decidable, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `«term_=_» #[Lean.mkIdent (Array.getOp header.targetNames 0), Lean.Syntax.atom info "=", Lean.mkIdent (Array.getOp header.targetNames 1)], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"]]]) 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 `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 ":", type]]], 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 #[]]])
Equations
- Lean.Elab.Deriving.DecEq.mkDecEqCmds indVal = do let ctx ← Lean.Elab.Deriving.mkContext "decEq" indVal.toConstantVal.name let a ← Lean.Elab.Deriving.DecEq.mkAuxFunction ctx let a_1 ← Lean.Elab.Deriving.mkInstanceCmds ctx `DecidableEq #[indVal.toConstantVal.name] false let cmds : Array Lean.Syntax := #[a] ++ a_1 let cls : Lean.Name := `Elab.Deriving.decEq let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.Elab.TermElabM (Array Lean.Syntax) := fun y => pure cmds if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "\n" ++ Lean.toMessageData cmds ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y
Equations
- Lean.Elab.Deriving.DecEq.mkDecEq declName = do let indVal ← Lean.getConstInfoInduct declName if indVal.isNested = true then pure false else do let cmds ← Lean.Elab.Command.liftTermElabM none (Lean.Elab.Deriving.DecEq.mkDecEqCmds indVal) Array.forM Lean.Elab.Command.elabCommand cmds 0 (Array.size cmds) pure true
Equations
- Lean.Elab.Deriving.DecEq.mkEnumOfNat declName = do let indVal ← Lean.getConstInfoInduct declName let enumType : Lean.Expr := Lean.mkConst declName let ctors : Array Lean.Name := List.toArray indVal.ctors Lean.Meta.withLocalDeclD `n (Lean.mkConst `Nat) fun n => let cond := Lean.mkConst `cond [Lean.levelZero]; (fun mkDecTree => do let value ← Lean.Meta.mkLambdaFVars #[n] (mkDecTree 0 (Array.size ctors)) false true let type ← Lean.Meta.mkArrow (Lean.mkConst `Nat) enumType Lean.addAndCompile (Lean.Declaration.defnDecl { toConstantVal := { name := Lean.Name.mkStr declName "ofNat", levelParams := [], type := type }, value := value, hints := Lean.ReducibilityHints.abbrev, safety := Lean.DefinitionSafety.safe })) (Lean.Elab.Deriving.DecEq.mkEnumOfNat.mkDecTree enumType ctors n cond)
Equations
- Lean.Elab.Deriving.DecEq.mkEnumOfNatThm declName = do let indVal ← Lean.getConstInfoInduct declName let toCtorIdx : Lean.Expr := Lean.mkConst (Lean.Name.mkStr declName "toCtorIdx") let ofNat : Lean.Expr := Lean.mkConst (Lean.Name.mkStr declName "ofNat") let enumType : Lean.Expr := Lean.mkConst declName let eqEnum : Lean.Expr := Lean.mkApp (Lean.mkConst `Eq [Lean.levelOne]) enumType let rflEnum : Lean.Expr := Lean.mkApp (Lean.mkConst `Eq.refl [Lean.levelOne]) enumType let ctors : List Lean.Name := indVal.ctors Lean.Meta.withLocalDeclD `x enumType fun x => let resultType := Lean.mkApp2 eqEnum (Lean.mkApp ofNat (Lean.mkApp toCtorIdx x)) x; do let motive ← Lean.Meta.mkLambdaFVars #[x] resultType false true let casesOn : Lean.Expr := Lean.mkConst (Lean.mkCasesOnName declName) [Lean.levelZero] let value : Lean.Expr := Lean.mkApp2 casesOn motive x let r ← forIn ctors value fun ctor r => let value := r; let value := Lean.mkApp value (Lean.mkApp rflEnum (Lean.mkConst ctor)); do pure PUnit.unit pure (ForInStep.yield value) let x_1 : Lean.Expr := r let value : Lean.Expr := x_1 let r ← Lean.Meta.mkLambdaFVars #[x] value false true let value : Lean.Expr := r let type ← Lean.Meta.mkForallFVars #[x] resultType false true Lean.addAndCompile (Lean.Declaration.thmDecl { toConstantVal := { name := Lean.Name.mkStr declName "ofNat_toCtorIdx", levelParams := [], type := type }, value := value })
Equations
- Lean.Elab.Deriving.DecEq.mkDecEqEnum declName = do Lean.Elab.Command.liftTermElabM none (liftM (Lean.Elab.Deriving.DecEq.mkEnumOfNat declName)) Lean.Elab.Command.liftTermElabM none (liftM (Lean.Elab.Deriving.DecEq.mkEnumOfNatThm declName)) let ofNatIdent : Lean.Syntax := Lean.mkIdent (Lean.Name.mkStr declName "ofNat") let auxThmIdent : Lean.Syntax := Lean.mkIdent (Lean.Name.mkStr declName "ofNat_toCtorIdx") let _ ← Lean.getConstInfoInduct declName let cmd ← 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 `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 #[], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.typeSpec #[Lean.Syntax.atom info ":", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "DecidableEq") (Lean.addMacroScope mainModule `DecidableEq scp) [(`DecidableEq, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.mkIdent declName]]]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.declValSimple #[Lean.Syntax.atom info ":=", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.fun #[Lean.Syntax.atom info "fun", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.basicFun #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "x") (Lean.addMacroScope mainModule `x scp) [], Lean.Syntax.ident info (String.toSubstring "y") (Lean.addMacroScope mainModule `y scp) []], Lean.Syntax.atom info "=>", Lean.Syntax.node Lean.SourceInfo.none `termDepIfThenElse #[Lean.Syntax.atom info "if", Lean.Syntax.ident info (String.toSubstring "h") (Lean.addMacroScope mainModule `h scp) [], Lean.Syntax.atom info ":", Lean.Syntax.node Lean.SourceInfo.none `«term_=_» #[Lean.Syntax.ident info (String.toSubstring "x.toCtorIdx") (Lean.addMacroScope mainModule `x.toCtorIdx scp) [], Lean.Syntax.atom info "=", Lean.Syntax.ident info (String.toSubstring "y.toCtorIdx") (Lean.addMacroScope mainModule `y.toCtorIdx scp) []], Lean.Syntax.atom info "then", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "isTrue") (Lean.addMacroScope mainModule `isTrue scp) [(`Decidable.isTrue, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.byTactic #[Lean.Syntax.atom info "by", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.tacticSeq #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.tacticSeq1Indented #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `group #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.first #[Lean.Syntax.atom info "first", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `group #[Lean.Syntax.atom info "|", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.tacticSeq #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.tacticSeq1Indented #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `group #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.«tacticHave__:=_» #[Lean.Syntax.atom info "have", Lean.Syntax.ident info (String.toSubstring "aux") (Lean.addMacroScope mainModule `aux scp) [], Lean.Syntax.atom info ":=", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "congrArg") (Lean.addMacroScope mainModule `congrArg scp) [(`congrArg, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[ofNatIdent, Lean.Syntax.ident info (String.toSubstring "h") (Lean.addMacroScope mainModule `h scp) []]]], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"]], Lean.Syntax.node Lean.SourceInfo.none `group #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.rwSeq #[Lean.Syntax.atom info "rw", Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.rwRuleSeq #[Lean.Syntax.atom info "[", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.rwRule #[Lean.Syntax.node Lean.SourceInfo.none `null #[], auxThmIdent], Lean.Syntax.atom info ",", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.rwRule #[Lean.Syntax.node Lean.SourceInfo.none `null #[], auxThmIdent]], Lean.Syntax.atom info "]"], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.location #[Lean.Syntax.atom info "at", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.locationHyp #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "aux") (Lean.addMacroScope mainModule `aux scp) []], Lean.Syntax.node Lean.SourceInfo.none `null #[]]]]], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"]], Lean.Syntax.node Lean.SourceInfo.none `group #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.assumption #[Lean.Syntax.atom info "assumption"], Lean.Syntax.node Lean.SourceInfo.none `null #[]]]]]], Lean.Syntax.node Lean.SourceInfo.none `group #[Lean.Syntax.atom info "|", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.tacticSeq #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.tacticSeq1Indented #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `group #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.tacticRfl #[Lean.Syntax.atom info "rfl"], Lean.Syntax.node Lean.SourceInfo.none `null #[]]]]]]]], Lean.Syntax.node Lean.SourceInfo.none `null #[]]]]]], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"]]], Lean.Syntax.atom info "else", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "isFalse") (Lean.addMacroScope mainModule `isFalse scp) [(`Decidable.isFalse, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.fun #[Lean.Syntax.atom info "fun", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.basicFun #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "h") (Lean.addMacroScope mainModule `h scp) []], Lean.Syntax.atom info "=>", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.byTactic #[Lean.Syntax.atom info "by", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.tacticSeq #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.tacticSeq1Indented #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `group #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.subst #[Lean.Syntax.atom info "subst", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "h") (Lean.addMacroScope mainModule `h scp) []]], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"]], Lean.Syntax.node Lean.SourceInfo.none `group #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.contradiction #[Lean.Syntax.atom info "contradiction"], 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 #[]]]) let cls : Lean.Name := `Elab.Deriving.decEq let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.Elab.Command.CommandElabM Unit := fun y => Lean.Elab.Command.elabCommand cmd if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "\n" ++ Lean.toMessageData cmd ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y
Equations
- Lean.Elab.Deriving.DecEq.mkDecEqInstanceHandler declNames = if (Array.size declNames != 1) = true then pure false else do let a ← Lean.isEnumType (Array.getOp declNames 0) if a = true then do Lean.Elab.Deriving.DecEq.mkDecEqEnum (Array.getOp declNames 0) pure true else Lean.Elab.Deriving.DecEq.mkDecEq (Array.getOp declNames 0)