Lean.Elab.Deriving.Hashable

def Lean.Elab.Deriving.Hashable.mkHashableHeader (ctx : Lean.Elab.Deriving.Context) (indVal : Lean.InductiveVal) :

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

Equations

Lean.Elab.Deriving.Hashable.mkHashableHeader ctx indVal = Lean.Elab.Deriving.mkHeader ctx `Hashable 1 indVal

def Lean.Elab.Deriving.Hashable.mkMatch (ctx : Lean.Elab.Deriving.Context) (header : Lean.Elab.Deriving.Header) (indVal : Lean.InductiveVal) (auxFuncIdx : Nat) :

Lean.Elab.TermElabM Lean.Syntax

Equations

Lean.Elab.Deriving.Hashable.mkMatch ctx header indVal auxFuncIdx = (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.Hashable.mkMatch.mkAlts ctx indVal)

source

def Lean.Elab.Deriving.Hashable.mkMatch.mkAlts (ctx : Lean.Elab.Deriving.Context) (indVal : Lean.InductiveVal) :

Lean.Elab.TermElabM (Array Lean.Syntax)

Equations

Lean.Elab.Deriving.Hashable.mkMatch.mkAlts ctx indVal = let alts := #[]; let ctorIdx := 0; let allIndVals := List.toArray indVal.all; do let r ← let col := indVal.ctors; forIn col { fst := ctorIdx, snd := alts } fun ctorName r => let ctorIdx := r.fst; let alts := r.snd; do let ctorInfo ← Lean.getConstInfoCtor ctorName let alt ← Lean.Meta.forallTelescopeReducing ctorInfo.toConstantVal.type fun xs type => do let _ ← 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 ctorArgs : Array Lean.Syntax := #[] let rhs ← do let _ ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.quote ctorIdx) let r ← let col := { start := 0, stop := indVal.numParams, step := 1 }; forIn col ctorArgs fun i r => let ctorArgs := 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 ctorArgs : Array Lean.Syntax := Array.push ctorArgs a pure PUnit.unit pure (ForInStep.yield ctorArgs) let x : Array Lean.Syntax := r let ctorArgs : Array Lean.Syntax := x let r ← let col := { start := 0, stop := ctorInfo.numFields, step := 1 }; forIn col { fst := ctorArgs, snd := rhs } fun i r => let ctorArgs := r.fst; let rhs := r.snd; let x := Array.getOp xs (indVal.numParams + i); do let xTy ← liftM (Lean.Meta.inferType x) let typeName : Lean.Name := Lean.Expr.constName! (Lean.Expr.getAppFn xTy) let a ← liftM (Lean.mkFreshUserName `a) let a : Lean.Syntax := Lean.mkIdent a let ctorArgs : Array Lean.Syntax := Array.push ctorArgs a match Array.findIdx? allIndVals fun a => a == typeName with | some x => do let r ← 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 "mixHash") (Lean.addMacroScope mainModule `mixHash scp) [(`mixHash, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[rhs, 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.app #[Lean.mkIdent (Array.getOp ctx.auxFunNames x), Lean.Syntax.node Lean.SourceInfo.none `null #[a]], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"]]]) let rhs : Lean.Syntax := r pure PUnit.unit pure (ForInStep.yield { fst := ctorArgs, snd := rhs }) | none => do let r ← 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 "mixHash") (Lean.addMacroScope mainModule `mixHash scp) [(`mixHash, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[rhs, 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.app #[Lean.Syntax.ident info (String.toSubstring "hash") (Lean.addMacroScope mainModule `hash scp) [(`Hashable.hash, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[a]], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"]]]) let rhs : Lean.Syntax := r pure PUnit.unit pure (ForInStep.yield { fst := ctorArgs, snd := rhs }) let x : MProd (Array Lean.Syntax) Lean.Syntax := r match x with | { fst := ctorArgs, 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 #[] ctorArgs)]) 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 let ctorIdx : Nat := ctorIdx + 1 pure PUnit.unit pure (ForInStep.yield { fst := ctorIdx, snd := alts }) let x : MProd Nat (Array Lean.Syntax) := r match x with | { fst := ctorIdx, snd := alts } => pure alts

source

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

Lean.Elab.TermElabM Lean.Syntax

Equations

Lean.Elab.Deriving.Hashable.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.Hashable.mkHashableHeader ctx indVal let body ← Lean.Elab.Deriving.Hashable.mkMatch ctx header indVal i let binders : Array Lean.Syntax := 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 "UInt64") (Lean.addMacroScope mainModule `UInt64 scp) [(`UInt64, [])]]]], 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 "UInt64") (Lean.addMacroScope mainModule `UInt64 scp) [(`UInt64, [])]]]], 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 #[]]])

source

def Lean.Elab.Deriving.Hashable.mkHashFuncs (ctx : Lean.Elab.Deriving.Context) :

Lean.Elab.TermElabM Lean.Syntax

Equations

Lean.Elab.Deriving.Hashable.mkHashFuncs 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.Hashable.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.Hashable.mkHashableHandler (declNames : Array Lean.Name) :

Lean.Elab.Command.CommandElabM Bool

Equations

Lean.Elab.Deriving.Hashable.mkHashableHandler 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.Hashable.mkHashableInstanceCmds declNames) Array.forM Lean.Elab.Command.elabCommand cmds 0 (Array.size cmds) pure true else pure false