Book the gain between a lot basis and its cost exactly

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

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

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