Skip to content

fix: parser: fix parsing strVal #18

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
hargoniX merged 3 commits into from
Feb 6, 2026
+364 −2
Merged

fix: parser: fix parsing strVal #18

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
d7dbba1
fix: parser: fix parsing strVal
nomeata Feb 6, 2026
271e59c
Forgot to save
nomeata Feb 6, 2026
5a28808
Yuck, do we want this in the test?
nomeata Feb 6, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 1 addition & 2 deletions Export/Parse.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -215,8 +215,7 @@ def parseExprNatLit (json : Json) : M Expr := do
return .lit (.natVal natVal)

def parseExprStrLit (json : Json) : M Expr := do
let .obj data := json | fail s!"Expr.lit strVal invalid"
let some (.str strVal) := data["strVal"]? | fail s!"Expr.lit strVal invalid"
let .str strVal := json | fail s!"Expr.lit strVal invalid"
return .lit (.strVal strVal)

def parseExprMdata (json : Json) : M Expr := do
Expand Down
363 changes: 363 additions & 0 deletions Test.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -343,3 +343,366 @@ functionWithLet
#guard_msgs in
#eval runParserTest do
dumpConstant ``functionWithLet

def literals : Nat × String := (42, "42")

/--
info: Prod
Prod.mk
Prod.rec
Nat
Nat.zero
Nat.succ
Nat.rec
List
List.nil
List.cons
List.rec
Array
Array.mk
Array.rec
LT
LT.mk
LT.rec
LT.lt
Nat.le
Nat.le.refl
Nat.le.step
Nat.le.rec
Nat.lt
instLTNat
Fin
Fin.mk
Fin.rec
outParam
HPow
HPow.mk
HPow.rec
HPow.hPow
Pow
Pow.mk
Pow.rec
Pow.pow
instHPow
NatPow
NatPow.mk
NatPow.rec
NatPow.pow
instPowNat
PUnit
PUnit.unit
PUnit.rec
PProd
PProd.mk
PProd.rec
Nat.below
Nat.brecOn.go
Nat.brecOn
Unit
OfNat
OfNat.mk
OfNat.rec
OfNat.ofNat
instOfNatNat
Nat.casesOn
Unit.unit
Nat.pow.match_1
Nat.mul.match_1
Nat.add.match_1
Nat.add
Nat.mul
Nat.pow
instNatPowNat
BitVec
BitVec.ofFin
BitVec.rec
UInt8
UInt8.ofBitVec
UInt8.rec
ByteArray
ByteArray.mk
ByteArray.rec
UInt32
UInt32.ofBitVec
UInt32.rec
Or
Or.inl
Or.inr
Or.rec
And
And.intro
And.rec
Nat.isValidChar
Fin.val
BitVec.toFin
BitVec.toNat
UInt32.toBitVec
UInt32.toNat
UInt32.isValidChar
Char
Char.mk
Char.rec
Eq
Eq.refl
Eq.rec
List.below
List.brecOn.go
List.brecOn
List.casesOn
List.toByteArray.match_1
ByteArray.casesOn
ByteArray.push.match_1
List.concat.match_1
List.concat
Array.toList
Array.push
ByteArray.push
List.toByteArray.loop
Array.emptyWithCapacity
Array.empty
ByteArray.emptyWithCapacity
ByteArray.empty
List.toByteArray
List.flatten.match_1
List.append.match_1
List.append
List.flatten
instDecidableEqList.match_1
List.map
List.flatMap
Char.val
False
False.rec
Not
Decidable
Decidable.isFalse
Decidable.isTrue
Decidable.rec
Decidable.casesOn
ite
LE
LE.mk
LE.rec
LE.le
instLENat
dite
Bool
Bool.false
Bool.true
Bool.rec
Nat.ble.match_1
Nat.ble
DecidableEq
Bool.casesOn
Bool.decEq.match_1
rfl
Bool.noConfusionType
Eq.ndrec
Bool.noConfusion
Bool.decEq
instDecidableEqBool
False.elim
Eq.casesOn
HEq
HEq.refl
HEq.rec
True
True.intro
True.rec
Nat.beq.match_1
Nat.beq
_private.Init.Prelude.0.noConfusion_of_Nat.aux.match_1_1
_private.Init.Prelude.0.noConfusion_of_Nat.aux
congrArg
noConfusion_of_Nat
Bool.ctorIdx
_private.Init.Prelude.0.Nat.le_of_ble_eq_true.match_1_1
_private.Init.Prelude.0.Nat.zero_le.match_1_1
Nat.zero_le
Nat.le.below
Nat.le.below.refl
Nat.le.below.step
Nat.le.below.rec
Nat.le.brecOn
Nat.le.below.casesOn
Eq.symm
cast
eq_of_heq
_private.Init.Prelude.0.Nat.succ_le_succ.match_1_4
HAdd
HAdd.mk
HAdd.rec
HAdd.hAdd
Add
Add.mk
Add.rec
Add.add
instHAdd
instAddNat
Nat.succ_le_succ
Nat.le_of_ble_eq_true
absurd
_private.Init.Prelude.0.Nat.ble_eq_true_of_le.match_1_4
_private.Init.Prelude.0.Nat.ble_self_eq_true.match_1_1
Nat.ble_self_eq_true
_private.Init.Prelude.0.Nat.ble_succ_eq_true.match_1_1
Nat.ble_succ_eq_true
Nat.ble_eq_true_of_le
Nat.not_le_of_not_ble_eq_true
Nat.decLe
HMod
HMod.mk
HMod.rec
HMod.hMod
Mod
Mod.mk
Mod.rec
Mod.mod
instHMod
namedPattern
Nat.mod.match_1
Nat.decLt
Nat.le.casesOn
Nat.ctorIdx
Nat.div.go.match_1
HSub
HSub.mk
HSub.rec
HSub.hSub
Sub
Sub.mk
Sub.rec
Sub.sub
instHSub
Nat.pred
Nat.sub
instSubNat
_private.Init.Prelude.0.Nat.le_trans.match_1_6
Nat.le_trans
Nat.lt_of_lt_of_le
And.casesOn
_private.Init.Prelude.0.Nat.div_rec_lemma.match_1_1
_private.Init.Prelude.0.Nat.sub_lt.match_1_1
_private.Init.Prelude.0.Nat.not_succ_le_self.match_1_1
Nat.noConfusionType
Nat.noConfusion
Nat.not_succ_le_zero
_private.Init.Prelude.0.Nat.pred_le_pred.match_1_1
Nat.le_succ
Nat.pred_le_pred
Nat.le_of_succ_le_succ
Nat.not_succ_le_self
Nat.lt_irrefl
Nat.lt_succ_of_le
Nat.le_refl
_private.Init.Prelude.0.Nat.pred_le.match_1_1
Nat.pred_le
Nat.sub_le
Nat.succ_sub_succ_eq_sub
Nat.sub_lt
Nat.div_rec_lemma
Nat.le_of_lt_succ
Nat.div_rec_fuel_lemma
Nat.modCore.go
Nat.lt_add_one
Nat.lt_succ_self
Nat.modCore
Nat.mod
Nat.instMod
_private.Init.Prelude.0.Nat.mod_lt.match_1_3
Nat.zero_lt_succ
_private.Init.Prelude.0.Nat.mod_lt.match_1_1
_private.Init.Prelude.0.Nat.modCore_lt.match_1_1
Nat.not_lt_zero
_private.Init.Prelude.0.Nat.modCoreGo_lt.match_1_1
Or.casesOn
_private.Init.Prelude.0.Or.elim.match_1_1
Or.elim
id
Or.resolve_right
GE.ge
_private.Init.Prelude.0.Nat.lt_or_ge.match_1_5
_private.Init.Prelude.0.Nat.lt_or_ge.match_1_3
Nat.le_succ_of_le
_private.Init.Prelude.0.Nat.lt_or_ge.match_1_1
Nat.eq_or_lt_of_le.match_3
Nat.eq_or_lt_of_le.match_1
Nat.eq_or_lt_of_le
Nat.lt_or_ge
Nat.lt_of_not_le
Nat.modCoreGo_lt
Nat.modCore_lt
Nat.mod_lt
Fin.Internal.ofNat
_private.Init.Prelude.0.Nat.pow_pos.match_1_1
HMul
HMul.mk
HMul.rec
HMul.hMul
Mul
Mul.mk
Mul.rec
Mul.mul
instHMul
instMulNat
_private.Init.Prelude.0.Nat.mul_pos.match_1_1
_private.Init.Prelude.0.Nat.add_pos_right.match_1_1
Nat.add_pos_right
Nat.mul_pos
Nat.pow_pos
BitVec.ofNat._proof_1
BitVec.ofNat
UInt8.ofNat
HDiv
HDiv.mk
HDiv.rec
HDiv.hDiv
Div
Div.mk
Div.rec
Div.div
instHDiv
Nat.div.go
Nat.div
Nat.instDiv
String.utf8EncodeChar
List.utf8Encode
ByteArray.IsValidUTF8
ByteArray.IsValidUTF8.intro
ByteArray.IsValidUTF8.rec
String
String.ofByteArray
String.rec
instDecidableAnd.match_1
instDecidableOr.match_1
instDecidableOr._proof_1
instDecidableOr
And.right
instDecidableAnd._proof_1
And.left
instDecidableAnd._proof_2
instDecidableAnd
BitVec.ofNatLT
UInt32.size
_private.Init.Prelude.0.isValidChar_UInt32.match_1_1
Nat.lt_trans
Decidable.decide
_private.Init.Prelude.0.of_decide_eq_true.match_1_1
_private.Init.Prelude.0.ne_true_of_eq_false.match_1_1
ne_true_of_eq_false
_private.Init.Prelude.0.decide_eq_false.match_1_1
decide_eq_false
of_decide_eq_true
_private.Init.Prelude.0.isValidChar_UInt32
Char.ofNatAux._private_1
Char.ofNatAux
Char.ofNat._proof_1
Char.ofNat._proof_2
Char.ofNat
String.ofList._proof_1
String.ofList
literals
-/
#guard_msgs in
#eval runParserTest do
dumpConstant ``literals