Lean.Elab.Deriving.Ord

def Lean.Elab.Deriving.Ord.mkOrdHeader (ctx : Lean.Elab.Deriving.Context) (indVal : Lean.InductiveVal) :

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

Equations

Lean.Elab.Deriving.Ord.mkOrdHeader ctx indVal = Lean.Elab.Deriving.mkHeader ctx `Ord 2 indVal

def Lean.Elab.Deriving.Ord.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.Ord.mkMatch ctx header indVal auxFunName = (fun 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.Ord.mkMatch.mkAlts indVal)

source

def Lean.Elab.Deriving.Ord.mkMatch.mkAlts (indVal : Lean.InductiveVal) :

Lean.Elab.TermElabM (Array Lean.Syntax)

Equations

Lean.Elab.Deriving.Ord.mkMatch.mkAlts indVal = 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 indPatterns : Array Lean.Syntax := #[] let r ← let col := { start := 0, stop := indVal.numIndices, step := 1 }; forIn col indPatterns fun i r => let indPatterns := 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 indPatterns : Array Lean.Syntax := Array.push indPatterns a pure PUnit.unit pure (ForInStep.yield indPatterns) let x : Array Lean.Syntax := r let indPatterns : Array Lean.Syntax := x let ctorArgs1 : Array Lean.Syntax := #[] let ctorArgs2 : Array Lean.Syntax := #[] let rhsCont : Lean.Syntax → Lean.Elab.TermElabM Lean.Syntax := fun rhs => pure rhs 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 := rhsCont } } fun i r => let ctorArgs1 := r.fst; let x := r.snd; let ctorArgs2 := x.fst; let rhsCont := x.snd; let x := Array.getOp xs (indVal.numParams + i); do let a ← liftM (Lean.Meta.inferType x) let a ← liftM (Lean.Meta.isProp a) if (Lean.Expr.containsFVar type (Lean.Expr.fvarId! x) || 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.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 := rhsCont } }) 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 rhsCont : Lean.Syntax → Lean.Elab.TermElabM Lean.Syntax := fun 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.match #[Lean.Syntax.atom info "match", Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchDiscr #[Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "compare") (Lean.addMacroScope mainModule `compare scp) [(`Ord.compare, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[a, b]]]], 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 #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchAlt #[Lean.Syntax.atom info "|", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "Ordering.lt") (Lean.addMacroScope mainModule `Ordering.lt scp) [(`Ordering.lt, [])]], Lean.Syntax.atom info "=>", Lean.Syntax.ident info (String.toSubstring "Ordering.lt") (Lean.addMacroScope mainModule `Ordering.lt scp) [(`Ordering.lt, [])]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchAlt #[Lean.Syntax.atom info "|", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "Ordering.gt") (Lean.addMacroScope mainModule `Ordering.gt scp) [(`Ordering.gt, [])]], Lean.Syntax.atom info "=>", Lean.Syntax.ident info (String.toSubstring "Ordering.gt") (Lean.addMacroScope mainModule `Ordering.gt scp) [(`Ordering.gt, [])]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchAlt #[Lean.Syntax.atom info "|", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "Ordering.eq") (Lean.addMacroScope mainModule `Ordering.eq scp) [(`Ordering.eq, [])]], Lean.Syntax.atom info "=>", rhs]]]])) >>= rhsCont pure PUnit.unit pure (ForInStep.yield { fst := ctorArgs1, snd := { fst := ctorArgs2, snd := rhsCont } }) let x : MProd (Array Lean.Syntax) (MProd (Array Lean.Syntax) (Lean.Syntax → Lean.Elab.TermElabM Lean.Syntax)) := r match x with | { fst := ctorArgs1, snd := { fst := ctorArgs2, snd := rhsCont } } => do let lPat ← 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 rPat ← 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 := indPatterns ++ #[lPat, rPat] 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 ltPatterns : Array Lean.Syntax := indPatterns ++ #[lPat, 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 gtPatterns : Array Lean.Syntax := indPatterns ++ #[a, rPat] let a ← do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.ident info (String.toSubstring "Ordering.eq") (Lean.addMacroScope mainModule `Ordering.eq scp) [(`Ordering.eq, [])]) let rhs ← rhsCont 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.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 a_1 ← do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← 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 ltPatterns => ltPatterns) ltPatterns) (Lean.mkAtom ","))), Lean.Syntax.atom info "=>", Lean.Syntax.ident info (String.toSubstring "Ordering.lt") (Lean.addMacroScope mainModule `Ordering.lt scp) [(`Ordering.lt, [])]]) let a_2 ← do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← 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 gtPatterns => gtPatterns) gtPatterns) (Lean.mkAtom ","))), Lean.Syntax.atom info "=>", Lean.Syntax.ident info (String.toSubstring "Ordering.gt") (Lean.addMacroScope mainModule `Ordering.gt scp) [(`Ordering.gt, [])]]) pure #[a, a_1, a_2] let alts : Array Lean.Syntax := alts ++ alt pure PUnit.unit pure (ForInStep.yield alts) let x : Array Lean.Syntax := r let alts : Array Lean.Syntax := x pure (Array.pop (Array.pop alts))

source

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

Lean.Elab.TermElabM Lean.Syntax

Equations

Lean.Elab.Deriving.Ord.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.Ord.mkOrdHeader ctx indVal let body ← Lean.Elab.Deriving.Ord.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 || indVal.isRec) = 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 "Ordering") (Lean.addMacroScope mainModule `Ordering scp) [(`Ordering, [])]]]], 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 "Ordering") (Lean.addMacroScope mainModule `Ordering scp) [(`Ordering, [])]]]], 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 || indVal.isRec) = true then do let letDecls ← Lean.Elab.Deriving.mkLocalInstanceLetDecls ctx `Ord 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.Ord.mkMutualBlock (ctx : Lean.Elab.Deriving.Context) :

Lean.Elab.TermElabM Lean.Syntax

Equations

Lean.Elab.Deriving.Ord.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.Ord.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 _ ← Lean.getCurrMacroScope let _ ← 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 #[] 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.Ord.mkOrdInstanceHandler (declNames : Array Lean.Name) :

Lean.Elab.Command.CommandElabM Bool

Equations

Lean.Elab.Deriving.Ord.mkOrdInstanceHandler declNames = 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.Ord.mkOrdInstanceCmds declNames) Array.forM Lean.Elab.Command.elabCommand cmds 0 (Array.size cmds) pure true else pure false