diff --git a/src/Lean/Data/Json/FromToJson/Basic.lean b/src/Lean/Data/Json/FromToJson/Basic.lean index 6c2de03574..a59b65876a 100644 --- a/src/Lean/Data/Json/FromToJson/Basic.lean +++ b/src/Lean/Data/Json/FromToJson/Basic.lean @@ -226,7 +226,13 @@ def opt [ToJson α] (k : String) : Option α → List (String × Json) | none => [] | some o => [⟨k, toJson o⟩] -/-- Parses a JSON-encoded `structure` or `inductive` constructor. Used mostly by `deriving FromJson`. -/ +/-- Returns the string value or single key name, if any. -/ +def getTag? : Json → Option String + | .str tag => some tag + | .obj kvs => guard (kvs.size == 1) *> kvs.minKey? + | _ => none + +-- TODO: delete after rebootstrap def parseTagged (json : Json) (tag : String) @@ -259,5 +265,28 @@ def parseTagged | Except.error err => Except.error err | Except.error err => Except.error err +/-- +Parses a JSON-encoded `structure` or `inductive` constructor, assuming the tag has already been +checked and `nFields` is nonzero. Used mostly by `deriving FromJson`. +-/ +def parseCtorFields + (json : Json) + (tag : String) + (nFields : Nat) + (fieldNames? : Option (Array Name)) : Except String (Array Json) := do + let payload ← getObjVal? json tag + match fieldNames? with + | some fieldNames => + fieldNames.mapM (getObjVal? payload ·.getString!) + | none => + if nFields == 1 then + Except.ok #[payload] + else + let fields ← getArr? payload + if fields.size == nFields then + Except.ok fields + else + Except.error s!"incorrect number of fields: {fields.size} ≟ {nFields}" + end Json end Lean diff --git a/src/Lean/Elab/Deriving/FromToJson.lean b/src/Lean/Elab/Deriving/FromToJson.lean index cb6b4b7899..c8f2d9cd63 100644 --- a/src/Lean/Elab/Deriving/FromToJson.lean +++ b/src/Lean/Elab/Deriving/FromToJson.lean @@ -111,14 +111,18 @@ def mkFromJsonBodyForStruct (indName : Name) : TermElabM Term := do def mkFromJsonBodyForInduct (ctx : Context) (indName : Name) : TermElabM Term := do let indVal ← getConstInfoInduct indName - let alts ← mkAlts indVal - let auxTerm ← alts.foldrM (fun xs x => `(Except.orElseLazy $xs (fun _ => $x))) (← `(Except.error "no inductive constructor matched")) - `($auxTerm) + let (ctors, alts) := (← mkAlts indVal).unzip + `(match Json.getTag? json with + | some tag => match tag with + $[| $(ctors.map Syntax.mkStrLit) => $(alts)]* + | _ => Except.error "no inductive constructor matched" + | none => Except.error "no inductive tag found") where - mkAlts (indVal : InductiveVal) : TermElabM (Array Term) := do + mkAlts (indVal : InductiveVal) : TermElabM (Array (String × Term)) := do let mut alts := #[] for ctorName in indVal.ctors do let ctorInfo ← getConstInfoCtor ctorName + let ctorStr := ctorName.eraseMacroScopes.getString! let alt ← do forallTelescopeReducing ctorInfo.type fun xs _ => do let mut binders := #[] let mut userNames := #[] @@ -142,11 +146,14 @@ where else ``(none) let stx ← - `((Json.parseTagged json $(quote ctorName.eraseMacroScopes.getString!) $(quote ctorInfo.numFields) $(quote userNamesOpt)).bind - (fun jsons => do - $[let $identNames:ident ← $fromJsons:doExpr]* - return $(mkIdent ctorName):ident $identNames*)) - pure (stx, ctorInfo.numFields) + if ctorInfo.numFields == 0 then + `(return $(mkIdent ctorName):ident $identNames*) + else + `((Json.parseCtorFields json $(quote ctorStr) $(quote ctorInfo.numFields) $(quote userNamesOpt)).bind + (fun jsons => do + $[let $identNames:ident ← $fromJsons:doExpr]* + return $(mkIdent ctorName):ident $identNames*)) + pure ((ctorStr, stx), ctorInfo.numFields) alts := alts.push alt -- the smaller cases, especially the ones without fields are likely faster let alts' := alts.qsort (fun (_, x) (_, y) => x < y) diff --git a/tests/lean/derivingRpcEncoding.lean.expected.out b/tests/lean/derivingRpcEncoding.lean.expected.out index aac04bcd3e..d2fe9edf81 100644 --- a/tests/lean/derivingRpcEncoding.lean.expected.out +++ b/tests/lean/derivingRpcEncoding.lean.expected.out @@ -14,4 +14,4 @@ ok: {"a": [{"baz": {"arr": []}}, [{"a": [{"baz": {"arr": []}}, []]}]]} ok: {"a": 42} ok: "a" ok: {} -Except.error "no inductive constructor matched" +Except.error "no inductive tag found" diff --git a/tests/lean/run/bigFromJson.lean b/tests/lean/run/bigFromJson.lean new file mode 100644 index 0000000000..5ea5d6ba45 --- /dev/null +++ b/tests/lean/run/bigFromJson.lean @@ -0,0 +1,36 @@ +import Lean + +/-! This used to fail to maxrec due to an unoptimized tag matching construction. -/ + +open Lean + +inductive Big where + | v0 | v1 | v2 | v3 | v4 | v5 | v6 | v7 | v8 | v9 + | v10 | v11 | v12 | v13 | v14 | v15 | v16 | v17 | v18 | v19 + | v20 | v21 | v22 | v23 | v24 | v25 | v26 | v27 | v28 | v29 + | v30 | v31 | v32 | v33 | v34 | v35 | v36 | v37 | v38 | v39 + | v40 | v41 | v42 | v43 | v44 | v45 | v46 | v47 | v48 | v49 + | v50 | v51 | v52 | v53 | v54 | v55 | v56 | v57 | v58 | v59 + | v60 | v61 | v62 | v63 | v64 | v65 | v66 | v67 | v68 | v69 + | v70 | v71 | v72 | v73 | v74 | v75 | v76 | v77 | v78 | v79 + | v80 | v81 | v82 | v83 | v84 | v85 | v86 | v87 | v88 | v89 + | v90 | v91 | v92 | v93 | v94 | v95 | v96 | v97 | v98 | v99 + | v100 | v101 | v102 | v103 | v104 | v105 | v106 | v107 | v108 | v109 + | v110 | v111 | v112 | v113 | v114 | v115 | v116 | v117 | v118 | v119 + | v120 | v121 | v122 | v123 | v124 | v125 | v126 | v127 | v128 | v129 + | v130 | v131 | v132 | v133 | v134 | v135 | v136 | v137 | v138 | v139 + | v140 | v141 | v142 | v143 | v144 | v145 | v146 | v147 | v148 | v149 + | v150 | v151 | v152 | v153 | v154 | v155 | v156 | v157 | v158 | v159 + | v160 | v161 | v162 | v163 | v164 | v165 | v166 | v167 | v168 | v169 + | v170 | v171 | v172 | v173 | v174 | v175 | v176 | v177 | v178 | v179 + | v180 | v181 | v182 | v183 | v184 | v185 | v186 | v187 | v188 | v189 + | v190 | v191 | v192 | v193 | v194 | v195 | v196 | v197 | v198 | v199 +deriving FromJson, ToJson, Repr + +/-- info: "v103" -/ +#guard_msgs in +#eval toJson Big.v103 + +/-- info: Except.ok (Big.v103) -/ +#guard_msgs in +#eval fromJson? (α := Big) (toJson Big.v103)