2
$\begingroup$

I don't know how mature or efficient Lean 4.1.0's standard feature support is.

However, I did enjoy an interesting case about benchmarking data processing languages.The challenge is to read a json file containing only strings and after processing and counting the amount of data provided, write another json file with the counted results. https://github.com/jinyus/related_post_gen

But regardless of that, my interest is in processing basic accounting data with information from the general ledger.

{
  "ledger": {
    "account_name": "Example Company",
    "account_number": "1234567890",
    "entries": [
      {
        "entry_date": "2023-10-14",
        "description": "Opening Balance",
        "debit": 10000.00,
        "credit": 0.00
      },
      {
        "entry_date": "2023-10-15",
        "description": "Sale of Products",
        "debit": 0.00,
        "credit": 5000.00
      },
      {
        "entry_date": "2023-10-16",
        "description": "Purchase of Supplies",
        "debit": 3000.00,
        "credit": 0.00
      },
      {
        "entry_date": "2023-10-17",
        "description": "Payment from Customer",
        "debit": 2000.00,
        "credit": 0.00
      },
      {
        "entry_date": "2023-10-18",
        "description": "Utilities Expense",
        "debit": 0.00,
        "credit": 1000.00
      }
    ]
  }
}

Later, I managed to read and write files using IO.FS.readFile/IO.FS.writeFile. I also learned about the use of Json.parse to recognize the format, although it wouldn't know back to the string type.

Is it possible for lean to analyze the format (stringfy)?

I wrote this on Lean code:

import Lean
import Lean.Data.Json.Basic
import Lean.Data.Json.Parser
import Lean.Data.Json.Printer

open Lean Json ToJson FromJson

structure Entry : Type where
  entry_date: String
  description: String
  debit: Float
  credit: Float
deriving Lean.toJson, Lean.FromJson, Inhabited

-- Check types
-- #check #["foo"]
-- #check 1000.00

structure Ledger : Type where
  account_name: String
  account_number: String
  entries: Array Entry
deriving Lean.toJson, Lean.FromJson, Inhabited

def main : IO Unit := do
  let startTime ← IO.monoMsNow
  let s ← IO.FS.readFile "ledger_account.json"
  -- Test Json Parser
  -- let j := (Json.parse s)
  -- IO.println j

  -- TODO

  -- timestamp
  IO.println s!"Finished: {(← IO.monoMsNow) - startTime}ms\n"

I'm looking for some examples of data manipulation or serialization algorithms.

$\endgroup$
3
  • $\begingroup$ I’m having trouble finding your question. Do you want to know how to take an object of type Json and convert it to a parsable JSON string? Try Lean.Json.render and/or Lean.Json.pretty. Admittedly the API and documentation leave a lot to be desired at the moment. (I wonder if Json is going to be moved into Std where it would get more user-facing support.) $\endgroup$
    – Jason Rute
    Oct 14, 2023 at 14:52
  • $\begingroup$ Oh wait. It looks like printing a Json object already should use Json.pretty. So I am again not sure what you question is? $\endgroup$
    – Jason Rute
    Oct 14, 2023 at 14:56
  • $\begingroup$ Hi @JasonRute, I apologize for not clarifying or highlighting enough. But the idea is what you mentioned. Although I would like to treat the file data individually (by structure fields). $\endgroup$ Oct 14, 2023 at 16:05

1 Answer 1

1
$\begingroup$

This might be what you want. I use the derive handlers for ToJson and FromJson to connect your classes to the Json type and round trip the Json from your file. Note the need to go from the Except monad to the IO monad. (Sorry, about an earlier version of this answer which got confused about the ToJson handler.)

import Lean
import Lean.Data.Json.Basic
import Lean.Data.Json.Parser
import Lean.Data.Json.Printer

open Lean Json ToJson FromJson

structure Entry: Type where
  entry_date: String
  description: String
  --debit: Float
  --credit: Float
deriving ToJson, FromJson, Inhabited, Repr

-- Check types
-- #check #["foo"]
-- #check 1000.00

structure Ledger : Type where
  account_name: String
  account_number: String
  entries: Array Entry
deriving Lean.ToJson, Lean.FromJson, Inhabited, Repr

def get_ledger_from_json_string (s: String): Except String Ledger := do
  let j : Json <- Json.parse s
  let ledger : Ledger <- fromJson? j
  return ledger
  
def ledger_account_string := "{     \"account_name\": \"Example Company\",     \"account_number\": \"1234567890\",     \"entries\": [       {         \"entry_date\": \"2023-10-14\",         \"description\": \"Opening Balance\",         \"debit\": 10000.00,         \"credit\": 0.00       },       {         \"entry_date\": \"2023-10-15\",         \"description\": \"Sale of Products\",         \"debit\": 0.00,         \"credit\": 5000.00       },       {         \"entry_date\": \"2023-10-16\",         \"description\": \"Purchase of Supplies\",         \"debit\": 3000.00,         \"credit\": 0.00       },       {         \"entry_date\": \"2023-10-17\",         \"description\": \"Payment from Customer\",         \"debit\": 2000.00,         \"credit\": 0.00       },       {         \"entry_date\": \"2023-10-18\",         \"description\": \"Utilities Expense\",         \"debit\": 0.00,         \"credit\": 1000.00       }     ]   }"
#eval (get_ledger_from_json_string ledger_account_string)
#eval toJson (get_ledger_from_json_string ledger_account_string).toOption.get!

def main : IO Unit := do
  let startTime ← IO.monoMsNow
  let s ← IO.FS.readFile "ledger_account.json"
  -- Test Json Parser
  let ledger : Ledger <- IO.ofExcept (get_ledger_from_json_string s)
  IO.println (toJson ledger)

  -- timestamp
  IO.println s!"Finished: {(← IO.monoMsNow) - startTime}ms\n"

Edit: Also notice the format in your file is a bit off from what the program expects. Do one of the following:

  1. delete the outer object with the field "ledger" in your file (like in the inline example I provided in the code),
  2. Make another structure LedgerFile which just has a field ledger and add ToJson and FromJson handlers, or
  3. Before using the fromJson for Ledger, extract the "ledger" field from the Json object j. I think you can do this with Json.getObj?.
$\endgroup$
3
  • $\begingroup$ Lean has Json parsers in its stdlib? :o $\endgroup$ Oct 16, 2023 at 21:20
  • 1
    $\begingroup$ @AgnishomChattopadhyay Yes, a lot of Lean is built in Lean and the language server uses JSON. That is at least one reason it exists, besides being an overall standard communication format. $\endgroup$
    – Jason Rute
    Oct 17, 2023 at 3:07
  • $\begingroup$ There are also more general parsing libraries available: github.com/lurk-lab/Megaparsec.lean and github.com/fgdorais/lean4-parser These are important since Lean core is unlikely to accept new parsing features unless they impact Lean core itself. $\endgroup$ Oct 22, 2023 at 3:47

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.