diff --git a/Ledger/Journal.lean b/Ledger/Journal.lean index 17113e2..08cdd21 100644 --- a/Ledger/Journal.lean +++ b/Ledger/Journal.lean @@ -394,10 +394,10 @@ private def takeBalanced (opn cls : Char) : List Char → Option (List Char × L /-- Consume the annotation/cost/assertion tail of an amount: `{lot} [date] (note) @ P / @@ T / = ASSERT` in any order. -/ private partial def annotLoop (ctx : AmtCtx) (line : Nat) (a : Amount) - (tail : String) (lot : Option (Amount × Bool)) (cost : Option Amount) + (tail : String) (lot : Option (Amount × Bool × Nat)) (cost : Option Amount) (teach : List (String × Nat) := []) (afterCost : Bool := false) (costDecs : Nat := 0) : - Except String (Option (Amount × Bool) × Option Amount × + Except String (Option (Amount × Bool × Nat) × Option Amount × List (String × Nat) × Nat) := do let t := trimS tail if t.isEmpty || t == "." then @@ -428,7 +428,7 @@ private partial def annotLoop (ctx : AmtCtx) (line : Nat) (a : Amount) if afterCost then lot else match lot with | some l => some l - | none => some (lotAmt, fixated) + | none => some (lotAmt, fixated, pr.decimals) annotLoop ctx line a (String.ofList rest) lot' cost teach afterCost costDecs else if t.startsWith "[" then match takeBalanced '[' ']' t.toList with @@ -501,35 +501,39 @@ private def parseAmountField (ctx : AmtCtx) (line : Nat) (field : String) : let innerS := if innerS.startsWith "=" then trimS (innerS.drop 1).toString else innerS let pr ← parseAmount ctx line innerS - pure (some pr.amount, trimS (String.ofList rest)) + pure (some (pr.amount, pr.decimals), trimS (String.ofList rest)) | none => err line s!"unclosed leading lot in '{field}'" else pure (none, field) let r ← parseAmount ctx line field let a := r.amount let (lot, cost, teach, costDecs) ← - annotLoop ctx line a r.tail (preLot.map (·, true)) none + annotLoop ctx line a r.tail (preLot.map fun (p, d) => (p, true, d)) none -- xact.cc phase 4/6: a fixated lot with no cost derives the cost - -- from the annotation; a lot WITH a cost books the rounded - -- gain/loss (basis - cost, rounded at commodity precision plus - -- the amount's decimals) into the effective cost + -- from the annotation; a lot WITH a cost books the gain/loss + -- (basis - cost) into the effective cost, so the posting balances + -- at its lot basis exactly, whatever display precision the + -- commodity has learned (regress/3258, regress/1773). C++ rounds + -- away only the residue of a per-unit price that it rounded out of + -- a total (regress/2975); `{{TOTAL}}` divides exactly here, so + -- this model has no such residue let gainVal := match lot, cost with - | some (p, _), some c => - if p.comm == c.comm then - let gl := (p.q * a.q) - c.q - some (Amount.mk c.comm - (roundAt ((ctx.precs.lookup c.comm).getD 0 + r.decimals) gl)) + | some (p, _, _), some c => + if p.comm == c.comm then some (Amount.mk c.comm ((p.q * a.q) - c.q)) else none | _, _ => none let costVal := match lot, cost with - | some (p, _), some c => - if p.comm == c.comm then - let basis := p.q * a.q - let gl := basis - c.q - let glR := roundAt ((ctx.precs.lookup c.comm).getD 0 + r.decimals) gl - some (Amount.mk c.comm (c.q + glR)) + | some (p, _, _), some c => + if p.comm == c.comm then some (Amount.mk c.comm (p.q * a.q)) else some c | _, _ => cost - let lotVal := lot.map fun (p, _) => Amount.mk p.comm (p.q * a.q) + -- absorbing a nonzero gain widens the cost to the decimals of the + -- lot basis, and COST_PREC tagging reads the widened cost + -- (xact.cc `*post->cost += gain_loss`, regress/1773) + let costDecs := match lot, gainVal with + | some (_, _, lotDecs), some g => + if g.q != 0 then max costDecs (lotDecs + r.decimals) else costDecs + | _, _ => costDecs + let lotVal := lot.map fun (p, _, _) => Amount.mk p.comm (p.q * a.q) pure (some a, costVal, lotVal, none, r.learned, r.decimals, field.startsWith "(", teach, costDecs, gainVal) @@ -1599,7 +1603,9 @@ def run (input0 : String) (dcDefault : Bool := false) | .commBlock comm => let body := trimS t if body.startsWith "alias " then - let al := trimS (body.drop "alias ".length).toString + -- a `;` outside quotes begins a comment (regress/3313_2) + let al := trimS (stripCommodityComment + (body.drop "alias ".length).toString) let al := (unquote al).getD al st := { st with commAliases := (al, comm) :: st.commAliases } continue @@ -1749,14 +1755,17 @@ def run (input0 : String) (dcDefault : Bool := false) let nm := trimS (t.drop "@account ".length).toString st := { st with pending := .acctBlock [(0, (unquote nm).getD nm)] } else if t.startsWith "@commodity " || t.startsWith "!commodity " then + -- read as a plain `commodity` header (regress/3313) let nm := trimS (t.drop "@commodity ".length).toString - st := { st with pending := .commBlock ((unquote nm).getD nm) } + st := { st with pending := .commBlock (headerSymbol nm) } else if t.startsWith "account " || t.startsWith "account\t" then let nm := trimS (t.drop "account ".length).toString st := { st with pending := .acctBlock [(0, (unquote nm).getD nm)] } else if t.startsWith "commodity " || t.startsWith "commodity\t" then + -- the symbol is the first token, and a `;` ends a bare one + -- (regress/3313) let nm := trimS (t.drop "commodity ".length).toString - st := { st with pending := .commBlock ((unquote nm).getD nm) } + st := { st with pending := .commBlock (headerSymbol nm) } else if t.startsWith "payee " || t.startsWith "tag " then st := { st with pending := .ignoreBlock } -- label declarations else if t.startsWith "@" || t.startsWith "!" then diff --git a/Ledger/Parse.lean b/Ledger/Parse.lean index 763ff77..ecd48c2 100644 --- a/Ledger/Parse.lean +++ b/Ledger/Parse.lean @@ -297,6 +297,41 @@ def unquote (s : String) : Option String := else none | _ => none +/-- The commodity that a `commodity` header names: a quoted symbol up + to its closing quote, or else the leading run of characters up to + whitespace or a `;`, which begins a comment. As in an amount, a + backslash puts the character after it into the run, so `A\;B` names + `A;B`, and the rest of the line is ignored (C++ + `commodity_t::parse_symbol(char*&)`, regress/3313). -/ +def headerSymbol (s : String) : String := + match s.toList with + | '"' :: rest => String.ofList (rest.takeWhile (· != '"')) + | cs => + let rec go : List Char → List Char + | [] => [] + | '\\' :: c :: rest => c :: go rest + | c :: rest => + if c == ' ' || c == '\t' || c == ';' then [] else c :: go rest + String.ofList (go cs) + +/-- Cut the comment from the argument of a commodity block's `alias` + line. It begins at the first `;` that is neither inside a quoted + symbol nor escaped with a backslash, the only places that a + commodity symbol can hold one (C++ `strip_commodity_comment` in + textual_directives.cc, regress/3313_2). -/ +def stripCommodityComment (s : String) : String := + let rec go (quoted : Bool) : List Char → List Char + | [] => [] + | '"' :: rest => '"' :: go (!quoted) rest + | ';' :: rest => if quoted then ';' :: go quoted rest else [] + | '\\' :: rest => + if quoted then '\\' :: go quoted rest + else match rest with + | c :: rest' => '\\' :: c :: go quoted rest' + | [] => ['\\'] + | c :: rest => c :: go quoted rest + String.ofList (go false s.toList) + /-- Time-unit commodities canonicalize to seconds. -/ def timeFactor (s : String) : Option ℚ := if s == "s" then some 1 diff --git a/README.md b/README.md index 24f4561..2ca30d3 100644 --- a/README.md +++ b/README.md @@ -118,9 +118,10 @@ citing the regression test or the C++ source location that forced it. These conventions cover number parsing, display precision, automated transactions, commodity equivalences, and balancing tolerances, and a few of them depart from the exact-rounding rule in -witnessed places. One example is the rounded gain that a posting -carrying both a lot price and a cost books into its effective cost, -and the code marks each such departure with the test that pins it. +witnessed places. One example is the balancing tolerance that accepts +a transaction whose residual is explained by rounding each per-unit +cost to the precision in which it was written, and the code marks +each such departure with the test that pins it. This layer is considerably larger than the theory, which is itself a lesson worth having in writing: the invariants of double-entry accounting are small, while the surface conventions of twenty years