Lean.Elab.Deriving.FromToJson

source

def Lean.Elab.Deriving.FromToJson.mkJsonField (n : Lean.Name) :

Bool × Lean.Syntax

Equations

Lean.Elab.Deriving.FromToJson.mkJsonField n = let s := Lean.Name.toString n; let s₁ := String.dropRightWhile s fun a => a == Char.ofNat 63; (s != s₁, Lean.Syntax.mkStrLit s₁)

source

def Lean.Elab.Deriving.FromToJson.mkToJsonInstanceHandler (declNames : Array Lean.Name) :

Lean.Elab.Command.CommandElabM Bool

Equations

Lean.Elab.Deriving.FromToJson.mkToJsonInstanceHandler declNames = (fun mkAlts => if (Array.size declNames == 1) = true then do let a ← Lean.getEnv let a ← pure (Lean.isStructure a (Array.getOp declNames 0)) if a = true then do let cmds ← Lean.Elab.Command.liftTermElabM none do let ctx ← Lean.Elab.Deriving.mkContext "toJson" (Array.getOp declNames 0) let header ← Lean.Elab.Deriving.mkHeader ctx `Lean.ToJson 1 (Array.getOp ctx.typeInfos 0) let a ← Lean.getEnv let fields : Array Lean.Name := Lean.getStructureFieldsFlattened a (Array.getOp declNames 0) false let fields ← Array.mapM (fun field => do let discr ← pure (Lean.Elab.Deriving.FromToJson.mkJsonField field) let x : Bool × Lean.Syntax := discr match x with | (isOptField, nm) => if isOptField = 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.app #[Lean.Syntax.ident info (String.toSubstring "opt") (Lean.addMacroScope mainModule `opt scp) [(`Lean.Json.opt, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[nm, Lean.mkIdent (Array.getOp header.targetNames 0 ++ field)]]) else do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `«term[_]» #[Lean.Syntax.atom info "[", 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 #[nm, Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.tupleTail #[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 "toJson") (Lean.addMacroScope mainModule `toJson scp) [(`Lean.ToJson.toJson, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.mkIdent (Array.getOp header.targetNames 0 ++ field)]]]]]], Lean.Syntax.atom info ")"]], Lean.Syntax.atom info "]"])) fields 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 `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 (Array.getOp ctx.auxFunNames 0), 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 #[] header.binders), Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.declValSimple #[Lean.Syntax.atom info ":=", Lean.Syntax.node Lean.SourceInfo.none `«term_<|_» #[Lean.Syntax.ident info (String.toSubstring "mkObj") (Lean.addMacroScope mainModule `mkObj scp) [(`Lean.Json.mkObj, [])], Lean.Syntax.atom info "<|", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "List.join") (Lean.addMacroScope mainModule `List.join scp) [(`List.join, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `«term[_]» #[Lean.Syntax.atom info "[", Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] (Lean.Syntax.SepArray.ofElems fields).elemsAndSeps), Lean.Syntax.atom info "]"]]]], 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 a ← Lean.Elab.Deriving.mkInstanceCmds ctx `Lean.ToJson declNames true pure (#[cmd] ++ a) Array.forM Lean.Elab.Command.elabCommand cmds 0 (Array.size cmds) pure true else do let indVal ← Lean.getConstInfoInduct (Array.getOp declNames 0) let cmds ← Lean.Elab.Command.liftTermElabM none do let ctx ← Lean.Elab.Deriving.mkContext "toJson" (Array.getOp declNames 0) let toJsonFuncId : Lean.Syntax := Lean.mkIdent (Array.getOp ctx.auxFunNames 0) let mkToJson : Lean.Syntax → Lean.Expr → Lean.Elab.TermElabM Lean.Syntax := fun id type => if Lean.Expr.isAppOf type indVal.toConstantVal.name = true then do let _ ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[toJsonFuncId, Lean.Syntax.node Lean.SourceInfo.none `null #[id]]) else 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 "toJson") (Lean.addMacroScope mainModule `toJson scp) [(`Lean.ToJson.toJson, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[id]]) let header ← Lean.Elab.Deriving.mkHeader ctx `Lean.ToJson 1 (Array.getOp ctx.typeInfos 0) let discrs ← Lean.Elab.Deriving.mkDiscrs header indVal let alts ← mkAlts indVal fun ctor args userNames => match args, userNames with | #[], x => 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 "toJson") (Lean.addMacroScope mainModule `toJson scp) [(`Lean.ToJson.toJson, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.quote (Lean.Name.getString! ctor.toConstantVal.name)]]) | #[(x, t)], none => do let a ← mkToJson x t 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 "mkObj") (Lean.addMacroScope mainModule `mkObj scp) [(`Lean.Json.mkObj, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `«term[_]» #[Lean.Syntax.atom info "[", 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.quote (Lean.Name.getString! ctor.toConstantVal.name), Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.tupleTail #[Lean.Syntax.atom info ",", Lean.Syntax.node Lean.SourceInfo.none `null #[a]]]], Lean.Syntax.atom info ")"]], Lean.Syntax.atom info "]"]]]) | xs, none => do let xs ← Array.mapM (fun x => match x with | (x, t) => mkToJson x t) xs 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 "mkObj") (Lean.addMacroScope mainModule `mkObj scp) [(`Lean.Json.mkObj, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `«term[_]» #[Lean.Syntax.atom info "[", 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.quote (Lean.Name.getString! ctor.toConstantVal.name), Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.tupleTail #[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 "Json.arr") (Lean.addMacroScope mainModule `Json.arr scp) [(`Lean.Json.arr, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `«term#[_,]» #[Lean.Syntax.atom info "#[", Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] (Lean.mkSepArray (Array.map (fun xs => xs) xs) (Lean.mkAtom ","))), Lean.Syntax.atom info "]"]]]]]]], Lean.Syntax.atom info ")"]], Lean.Syntax.atom info "]"]]]) | xs, some userNames => do let xs ← Array.mapIdxM xs fun idx x => match x with | (x, t) => do let a ← mkToJson x t let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.quote (Lean.Name.getString! (Array.getOp userNames idx.val)), Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.tupleTail #[Lean.Syntax.atom info ",", Lean.Syntax.node Lean.SourceInfo.none `null #[a]]]], Lean.Syntax.atom info ")"]) 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 "mkObj") (Lean.addMacroScope mainModule `mkObj scp) [(`Lean.Json.mkObj, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `«term[_]» #[Lean.Syntax.atom info "[", 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.quote (Lean.Name.getString! ctor.toConstantVal.name), Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.tupleTail #[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 "mkObj") (Lean.addMacroScope mainModule `mkObj scp) [(`Lean.Json.mkObj, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `«term[_]» #[Lean.Syntax.atom info "[", Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] (Lean.mkSepArray (Array.map (fun xs => xs) xs) (Lean.mkAtom ","))), Lean.Syntax.atom info "]"]]]]]]], Lean.Syntax.atom info ")"]], Lean.Syntax.atom info "]"]]]) let auxCmd ← do 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)]]) let _do_jp : Lean.Syntax → PUnit → Lean.Elab.TermElabM (Array Lean.Syntax) := fun auxCmd y => do let a ← Lean.Elab.Deriving.mkInstanceCmds ctx `Lean.ToJson declNames true pure (#[auxCmd] ++ a) if ctx.usePartial = true then do let letDecls ← Lean.Elab.Deriving.mkLocalInstanceLetDecls ctx `Lean.ToJson header.argNames let r ← Lean.Elab.Deriving.mkLet letDecls auxCmd let auxCmd : Lean.Syntax := r let r ← 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 `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 #[toJsonFuncId, 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 #[] header.binders), Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.declValSimple #[Lean.Syntax.atom info ":=", auxCmd, 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 auxCmd : Lean.Syntax := r let y ← pure PUnit.unit _do_jp auxCmd y else do let r ← 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 `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 #[toJsonFuncId, 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 #[] header.binders), Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.declValSimple #[Lean.Syntax.atom info ":=", auxCmd, 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 auxCmd : Lean.Syntax := r let y ← pure PUnit.unit _do_jp auxCmd y Array.forM Lean.Elab.Command.elabCommand cmds 0 (Array.size cmds) pure true else pure false) Lean.Elab.Deriving.FromToJson.mkToJsonInstanceHandler.mkAlts

source

def Lean.Elab.Deriving.FromToJson.mkToJsonInstanceHandler.mkAlts (indVal : Lean.InductiveVal) (rhs : Lean.ConstructorVal → Array (Lean.Syntax × Lean.Expr) → Option (Array Lean.Name) → Lean.Elab.TermElabM Lean.Syntax) :

Lean.Elab.TermElabM (Array Lean.Syntax)

Equations

Lean.Elab.Deriving.FromToJson.mkToJsonInstanceHandler.mkAlts indVal rhs = Array.mapM (fun ctor => do let ctorInfo ← Lean.getConstInfoCtor ctor Lean.Meta.forallTelescopeReducing ctorInfo.toConstantVal.type fun xs type => 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 ctorArgs : Array Lean.Syntax := #[] 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 binders : Array (Lean.Syntax × Lean.Expr) := #[] let userNames : Array Lean.Name := #[] let r ← let col := { start := 0, stop := ctorInfo.numFields, step := 1 }; forIn col { fst := ctorArgs, snd := { fst := userNames, snd := binders } } fun i r => let ctorArgs := r.fst; let x := r.snd; let userNames := x.fst; let binders := x.snd; let x := Array.getOp xs (indVal.numParams + i); do let localDecl ← liftM (Lean.Meta.getLocalDecl (Lean.Expr.fvarId! x)) let _do_jp : Array Lean.Syntax → Array Lean.Name → Array (Lean.Syntax × Lean.Expr) → PUnit → Lean.Elab.TermElabM (ForInStep (MProd (Array Lean.Syntax) (MProd (Array Lean.Name) (Array (Lean.Syntax × Lean.Expr))))) := fun ctorArgs userNames binders y => do let a ← liftM (Lean.mkFreshUserName `a) let a : Lean.Syntax := Lean.mkIdent a let binders : Array (Lean.Syntax × Lean.Expr) := Array.push binders (a, Lean.LocalDecl.type localDecl) let ctorArgs : Array Lean.Syntax := Array.push ctorArgs a pure PUnit.unit pure (ForInStep.yield { fst := ctorArgs, snd := { fst := userNames, snd := binders } }) if (!Lean.Name.hasMacroScopes (Lean.LocalDecl.userName localDecl)) = true then let userNames := Array.push userNames (Lean.LocalDecl.userName localDecl); do let y ← pure PUnit.unit _do_jp ctorArgs userNames binders y else do let y ← pure PUnit.unit _do_jp ctorArgs userNames binders y let x : MProd (Array Lean.Syntax) (MProd (Array Lean.Name) (Array (Lean.Syntax × Lean.Expr))) := r match x with | { fst := ctorArgs, snd := { fst := userNames, snd := binders } } => 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 ctorInfo.toConstantVal.name], Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] ctorArgs)]) let patterns : Array Lean.Syntax := Array.push patterns a let rhs ← rhs ctorInfo binders (if (Array.size userNames == Array.size binders) = true then some userNames else none) 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])) (List.toArray indVal.ctors)

source

def Lean.Elab.Deriving.FromToJson.mkFromJsonInstanceHandler (declNames : Array Lean.Name) :

Lean.Elab.Command.CommandElabM Bool

Equations

Lean.Elab.Deriving.FromToJson.mkFromJsonInstanceHandler declNames = (fun mkAlts => if (Array.size declNames == 1) = true then do let a ← Lean.getEnv let a ← pure (Lean.isStructure a (Array.getOp declNames 0)) if a = true then do let cmds ← Lean.Elab.Command.liftTermElabM none do let ctx ← Lean.Elab.Deriving.mkContext "fromJson" (Array.getOp declNames 0) let header ← Lean.Elab.Deriving.mkHeader ctx `Lean.FromJson 0 (Array.getOp ctx.typeInfos 0) let a ← Lean.getEnv let fields : Array Lean.Name := Lean.getStructureFieldsFlattened a (Array.getOp declNames 0) false let jsonFields : Array Lean.Syntax := Array.map (Prod.snd ∘ Lean.Elab.Deriving.FromToJson.mkJsonField) fields let fields : Array Lean.Syntax := Array.map Lean.mkIdent fields let a ← Lean.Elab.Deriving.mkInductiveApp (Array.getOp ctx.typeInfos 0) header.argNames 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 `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 (Array.getOp ctx.auxFunNames 0), 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.push (Array.append #[] header.binders) (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.explicitBinder #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "j") (Lean.addMacroScope mainModule `j scp) []], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ":", Lean.Syntax.ident info (String.toSubstring "Json") (Lean.addMacroScope mainModule `Json scp) [(`Lean.Json, [])]], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info ")"])), 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 "Except") (Lean.addMacroScope mainModule `Except scp) [(`Except, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "String") (Lean.addMacroScope mainModule `String scp) [(`String, [])], a]]]]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.declValSimple #[Lean.Syntax.atom info ":=", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.do #[Lean.Syntax.atom info "do", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqIndent #[Lean.Syntax.node Lean.SourceInfo.none `null (Array.push (Array.append #[] (Array.map (fun x => match x with | (fields, jsonFields) => Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doLetArrow #[Lean.Syntax.atom info "let", Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doIdDecl #[fields, Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info "←", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doExpr #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "getObjValAs?") (Lean.addMacroScope mainModule `getObjValAs? scp) [(`Lean.Json.getObjValAs?, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "j") (Lean.addMacroScope mainModule `j scp) [], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.hole #[Lean.Syntax.atom info "_"], jsonFields]]]]], Lean.Syntax.node Lean.SourceInfo.none `null #[]]) (Array.zip fields jsonFields))) (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doReturn #[Lean.Syntax.atom info "return", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.structInst #[Lean.Syntax.atom info "{", Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] (let a := id fields; Array.map (fun x => match x with | (fields, a) => Lean.Syntax.node Lean.SourceInfo.none `group #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.structInstField #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.structInstLVal #[fields, Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ":=", a], Lean.Syntax.node Lean.SourceInfo.none `null #[]]) (Array.zip fields a))), Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.optEllipsis #[Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info "}"]]], 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 #[]]]) let a ← Lean.Elab.Deriving.mkInstanceCmds ctx `Lean.FromJson declNames true pure (#[cmd] ++ a) Array.forM Lean.Elab.Command.elabCommand cmds 0 (Array.size cmds) pure true else do let indVal ← Lean.getConstInfoInduct (Array.getOp declNames 0) let cmds ← Lean.Elab.Command.liftTermElabM none do let ctx ← Lean.Elab.Deriving.mkContext "fromJson" (Array.getOp declNames 0) let header ← Lean.Elab.Deriving.mkHeader ctx `Lean.FromJson 0 (Array.getOp ctx.typeInfos 0) let fromJsonFuncId : Lean.Syntax := Lean.mkIdent (Array.getOp ctx.auxFunNames 0) let _ ← Lean.Elab.Deriving.mkDiscrs header indVal let alts ← mkAlts indVal fromJsonFuncId let a ← 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 "Except.error") (Lean.addMacroScope mainModule `Except.error scp) [(`Except.error, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `strLit #[Lean.Syntax.atom info "\"no inductive constructor matched\""]]]) let auxCmd ← Array.foldrM (fun xs x => 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 "Except.orElseLazy") (Lean.addMacroScope mainModule `Except.orElseLazy scp) [(`Except.orElseLazy, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[xs, 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.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.node Lean.SourceInfo.none `Lean.Parser.Term.hole #[Lean.Syntax.atom info "_"]], Lean.Syntax.atom info "=>", x]], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"]]])) a alts (Array.size alts) let _do_jp : Lean.Syntax → PUnit → Lean.Elab.TermElabM (Array Lean.Syntax) := fun auxCmd y => let _do_jp := fun auxCmd y => do let a ← Lean.Elab.Deriving.mkInstanceCmds ctx `Lean.FromJson declNames true pure (#[auxCmd] ++ a); if (ctx.usePartial || indVal.isRec) = true then do let a ← Lean.Elab.Deriving.mkInductiveApp (Array.getOp ctx.typeInfos 0) header.argNames 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.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 #[fromJsonFuncId, 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.push (Array.append #[] header.binders) (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.explicitBinder #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "json") (Lean.addMacroScope mainModule `json scp) []], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ":", Lean.Syntax.ident info (String.toSubstring "Json") (Lean.addMacroScope mainModule `Json scp) [(`Lean.Json, [])]], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info ")"])), 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 "Except") (Lean.addMacroScope mainModule `Except scp) [(`Except, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "String") (Lean.addMacroScope mainModule `String scp) [(`String, [])], a]]]]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.declValSimple #[Lean.Syntax.atom info ":=", auxCmd, 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 auxCmd : Lean.Syntax := r let y ← pure PUnit.unit _do_jp auxCmd y else do let a ← Lean.Elab.Deriving.mkInductiveApp (Array.getOp ctx.typeInfos 0) header.argNames 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.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 #[fromJsonFuncId, 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.push (Array.append #[] header.binders) (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.explicitBinder #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "json") (Lean.addMacroScope mainModule `json scp) []], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ":", Lean.Syntax.ident info (String.toSubstring "Json") (Lean.addMacroScope mainModule `Json scp) [(`Lean.Json, [])]], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info ")"])), 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 "Except") (Lean.addMacroScope mainModule `Except scp) [(`Except, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "String") (Lean.addMacroScope mainModule `String scp) [(`String, [])], a]]]]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.declValSimple #[Lean.Syntax.atom info ":=", auxCmd, 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 auxCmd : Lean.Syntax := r let y ← pure PUnit.unit _do_jp auxCmd y if ctx.usePartial = true then do let letDecls ← Lean.Elab.Deriving.mkLocalInstanceLetDecls ctx `Lean.FromJson header.argNames let r ← Lean.Elab.Deriving.mkLet letDecls auxCmd let auxCmd : Lean.Syntax := r let y ← pure PUnit.unit _do_jp auxCmd y else do let y ← pure PUnit.unit _do_jp auxCmd y Array.forM Lean.Elab.Command.elabCommand cmds 0 (Array.size cmds) pure true else pure false) Lean.Elab.Deriving.FromToJson.mkFromJsonInstanceHandler.mkAlts

source

def Lean.Elab.Deriving.FromToJson.mkFromJsonInstanceHandler.mkAlts (indVal : Lean.InductiveVal) (fromJsonFuncId : Lean.Syntax) :

Lean.Elab.TermElabM (Array Lean.Syntax)

Equations

Lean.Elab.Deriving.FromToJson.mkFromJsonInstanceHandler.mkAlts indVal fromJsonFuncId = do let alts ← Array.mapM (fun ctor => do let ctorInfo ← Lean.getConstInfoCtor ctor Lean.Meta.forallTelescopeReducing ctorInfo.toConstantVal.type fun xs type => let binders := #[]; let userNames := #[]; do let r ← let col := { start := 0, stop := ctorInfo.numFields, step := 1 }; forIn col { fst := userNames, snd := binders } fun i r => let userNames := r.fst; let binders := r.snd; let x := Array.getOp xs (indVal.numParams + i); do let localDecl ← liftM (Lean.Meta.getLocalDecl (Lean.Expr.fvarId! x)) let _do_jp : Array Lean.Name → Array (Lean.Syntax × Lean.Expr) → PUnit → Lean.Elab.TermElabM (ForInStep (MProd (Array Lean.Name) (Array (Lean.Syntax × Lean.Expr)))) := fun userNames binders y => do let a ← liftM (Lean.mkFreshUserName `a) let a : Lean.Syntax := Lean.mkIdent a let binders : Array (Lean.Syntax × Lean.Expr) := Array.push binders (a, Lean.LocalDecl.type localDecl) pure PUnit.unit pure (ForInStep.yield { fst := userNames, snd := binders }) if (!Lean.Name.hasMacroScopes (Lean.LocalDecl.userName localDecl)) = true then let userNames := Array.push userNames (Lean.LocalDecl.userName localDecl); do let y ← pure PUnit.unit _do_jp userNames binders y else do let y ← pure PUnit.unit _do_jp userNames binders y let x : MProd (Array Lean.Name) (Array (Lean.Syntax × Lean.Expr)) := r match x with | { fst := userNames, snd := binders } => let mkFromJson := fun idx type => if Lean.Expr.isAppOf type indVal.toConstantVal.name = 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.doExpr #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[fromJsonFuncId, Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.arrayRef #[Lean.Syntax.ident info (String.toSubstring "jsons") (Lean.addMacroScope mainModule `jsons scp) [], Lean.Syntax.atom info "[", Lean.quote idx, Lean.Syntax.atom info "]"]]]]) else do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doExpr #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "fromJson?") (Lean.addMacroScope mainModule `fromJson? scp) [(`Lean.FromJson.fromJson?, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.arrayRef #[Lean.Syntax.ident info (String.toSubstring "jsons") (Lean.addMacroScope mainModule `jsons scp) [], Lean.Syntax.atom info "[", Lean.quote idx, Lean.Syntax.atom info "]"]]]]); let identNames := Array.map Prod.fst binders; do let fromJsons ← Array.mapIdxM binders fun idx x => match x with | (x, type) => mkFromJson idx.val type let _do_jp : Lean.Syntax → Lean.Elab.TermElabM (Lean.Syntax × Nat) := fun userNamesOpt => do let stx ← 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.node Lean.SourceInfo.none `Lean.Parser.Term.proj #[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 "Json.parseTagged") (Lean.addMacroScope mainModule `Json.parseTagged scp) [(`Lean.Json.parseTagged, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "json") (Lean.addMacroScope mainModule `json scp) [], Lean.quote (Lean.Name.getString! ctor), Lean.quote ctorInfo.numFields, Lean.quote userNamesOpt]], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"], Lean.Syntax.atom info ".", Lean.Syntax.ident info (String.toSubstring "bind") (Lean.addMacroScope mainModule `bind scp) [(`Bind.bind, [])]], 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.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 "jsons") (Lean.addMacroScope mainModule `jsons scp) []], Lean.Syntax.atom info "=>", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.do #[Lean.Syntax.atom info "do", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqIndent #[Lean.Syntax.node Lean.SourceInfo.none `null (Array.push (Array.append #[] (Array.map (fun x => match x with | (identNames, fromJsons) => Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doLetArrow #[Lean.Syntax.atom info "let", Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doIdDecl #[identNames, Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info "←", fromJsons]], Lean.Syntax.node Lean.SourceInfo.none `null #[]]) (Array.zip identNames fromJsons))) (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doReturn #[Lean.Syntax.atom info "return", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.mkIdent ctor, Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] identNames)]]], Lean.Syntax.node Lean.SourceInfo.none `null #[]]))]]]], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"]]]) pure (stx, ctorInfo.numFields) if (Array.size binders == Array.size userNames) = true then do let y ← 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 "some") (Lean.addMacroScope mainModule `some scp) [(`Option.some, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `«term#[_,]» #[Lean.Syntax.atom info "#[", Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] (let a := Array.map Lean.quote userNames; Lean.mkSepArray (Array.map (fun a => a) a) (Lean.mkAtom ","))), Lean.Syntax.atom info "]"]]]) _do_jp y else do let y ← do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.ident info (String.toSubstring "none") (Lean.addMacroScope mainModule `none scp) [(`Option.none, [])]) _do_jp y) (List.toArray indVal.ctors) let alts : Array (Lean.Syntax × Nat) := Array.qsort alts (fun x x_1 => match x with | (x, x_2) => match x_1 with | (x, y) => decide (x_2 < y)) 0 (Array.size alts - 1) pure (Array.map Prod.fst alts)