def Actus.IO.Parse.jsonToFloat (j : Lean.Json) : Except String Float

A JSON number, or a numeric string ("1000.0"), to Float.

Equations

• Actus.IO.Parse.jsonToFloat (Lean.Json.num n) = Except.ok n.toFloat
• Actus.IO.Parse.jsonToFloat (Lean.Json.str s) = do let j' ← Lean.Json.parse s let n ← j'.getNum? pure n.toFloat
• Actus.IO.Parse.jsonToFloat j = Except.error (toString "expected number, got " ++ toString j.compress)

def Actus.IO.Parse.parseDate (s : String) : Except String Protocol.LocalTime

ISO-8601 date(-time) string "YYYY-MM-DD[THH:MM:SS]" to LocalTime. (The 23:59:59 end-of-day convention extends accrual to the next midnight but the event is still stamped on the written date, so the date part is taken as-is.)

Equations

• One or more equations did not get rendered due to their size.

def Actus.IO.Parse.isEndOfDay (s : String) : Bool

Is the timestamp end-of-day (…T23:59:59)?

Equations

• Actus.IO.Parse.isEndOfDay s = ((List.drop 1 (s.splitOn "T")).headD "").startsWith "23:59:59"

def Actus.IO.Parse.parseDateRoll (s : String) : Except String Protocol.LocalTime

Like parseDate, but a 23:59:59 end-of-day timestamp rolls to the next midnight (used for event dates so computed and expected events align).

Equations

• Actus.IO.Parse.parseDateRoll s = do let base ← Actus.IO.Parse.parseDate s pure (if Actus.IO.Parse.isEndOfDay s = true then Actus.Util.Date.addDays base 1 else base)

def Actus.IO.Parse.parseCycle (s : String) : Except String Protocol.Cycle

ACTUS cycle string, e.g. "P1ML1" (period 1 Month, long stub) or the older "1M-" form, to Cycle. The leading P and a trailing stub marker (L0/L1, or a +/- suffix) are both accepted; L1 or + mark a long stub.

Equations

• One or more equations did not get rendered due to their size.

def Actus.IO.Parse.contractTypeOf : String → Except String Protocol.ContractType

Equations

• One or more equations did not get rendered due to their size.

def Actus.IO.Parse.contractRoleOf : String → Except String Protocol.ContractRole

Equations

• One or more equations did not get rendered due to their size.

def Actus.IO.Parse.dayCountOf : String → Except String Protocol.DayCountConvention

Equations

• One or more equations did not get rendered due to their size.

def Actus.IO.Parse.eomOf : String → Except String Protocol.EndOfMonthConvention

Equations

• Actus.IO.Parse.eomOf = Actus.IO.Parse.enum✝ "endOfMonthConvention" [("EOM", Actus.Protocol.EndOfMonthConvention.EOMC_EOM), ("SD", Actus.Protocol.EndOfMonthConvention.EOMC_SD)]

def Actus.IO.Parse.bdcOf : String → Except String Protocol.BusinessDayConvention

Equations

• One or more equations did not get rendered due to their size.

def Actus.IO.Parse.calendarOf : String → Except String Protocol.Calendar

Equations

• One or more equations did not get rendered due to their size.

def Actus.IO.Parse.referenceRoleOf : String → Except String Protocol.ReferenceRole

Equations

• One or more equations did not get rendered due to their size.

def Actus.IO.Parse.performanceOf : String → Except String Protocol.Performance

Equations

• One or more equations did not get rendered due to their size.

def Actus.IO.Parse.creditEventTypeOf : String → Except String Protocol.CreditEventTypeCovered

Equations

• One or more equations did not get rendered due to their size.

def Actus.IO.Parse.guaranteedExposureOf : String → Except String Protocol.CreditEventGuaranteedExposure

Equations

• One or more equations did not get rendered due to their size.

def Actus.IO.Parse.feeBasisOf : String → Except String Protocol.FeeBasis

Equations

• Actus.IO.Parse.feeBasisOf = Actus.IO.Parse.enum✝ "feeBasis" [("A", Actus.Protocol.FeeBasis.FEB_A), ("N", Actus.Protocol.FeeBasis.FEB_N)]

def Actus.IO.Parse.icbOf : String → Except String Protocol.InterestCalculationBase

Equations

• One or more equations did not get rendered due to their size.

def Actus.IO.Parse.penaltyTypeOf : String → Except String Protocol.PenaltyType

Equations

• One or more equations did not get rendered due to their size.

def Actus.IO.Parse.prepaymentOf : String → Except String Protocol.PrepaymentEffect

Equations

• One or more equations did not get rendered due to their size.

def Actus.IO.Parse.scalingEffectOf : String → Except String Protocol.ScalingEffect

Equations

• One or more equations did not get rendered due to their size.

partial def Actus.IO.Parse.termsFromJson (j : Lean.Json) : Except String (Contract.Terms Float)

Decode a terms object into ContractTerms Float.

def Actus.IO.Parse.termsFromString (s : String) : Except String (Contract.Terms Float)

Decode a terms object given as a raw JSON string.

Equations

• Actus.IO.Parse.termsFromString s = do let __do_lift ← Lean.Json.parse s Actus.IO.Parse.termsFromJson __do_lift

def Actus.IO.Parse.eventTypeOf : String → Except String Protocol.EventType

Equations

• One or more equations did not get rendered due to their size.

def Actus.IO.Parse.riskFactorsFromJson (j : Lean.Json) (ct : Contract.Terms Float) : Except String (Contract.RiskFactorEnv Float)

Build a RiskFactorEnv from a test case's dataObserved, wiring the rate-reset market series (Oʳᶠ(RRMO,·)). Settlement-currency factor is 1 (single-currency reference cases); prepayment/annuity default to none.

Equations

• One or more equations did not get rendered due to their size.

structure Actus.IO.Parse.ObservedEvent : Type

One expected event from eventsObserved.

• type : Protocol.EventType
• time : Protocol.LocalTime
• payoff : Float

def Actus.IO.Parse.instReprObservedEvent.repr : ObservedEvent → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Actus.IO.Parse.instReprObservedEvent : Repr ObservedEvent

Equations

• Actus.IO.Parse.instReprObservedEvent = { reprPrec := Actus.IO.Parse.instReprObservedEvent.repr }

structure Actus.IO.Parse.TestCase : Type

One actus-tests entry.

• identifier : String
• terms : Contract.Terms Float
• horizon : Option Protocol.LocalTime
• events : List ObservedEvent

def Actus.IO.Parse.testCaseFromJson (j : Lean.Json) : Except String TestCase

Decode one test entry: its terms, horizon to, and expected events (results, falling back to eventsObserved).

Equations

• One or more equations did not get rendered due to their size.

def Actus.IO.Parse.testFileFromJson (j : Lean.Json) : Except String (List (String × TestCase))

Decode a whole actus-tests file: a JSON object keyed by test id.

Equations

• One or more equations did not get rendered due to their size.
• Actus.IO.Parse.testFileFromJson j = Except.error "expected a JSON object keyed by test id"

def Actus.IO.Parse.testFileFromString (s : String) : Except String (List (String × TestCase))

Decode a whole actus-tests file given as a raw JSON string.

Equations

• Actus.IO.Parse.testFileFromString s = do let __do_lift ← Lean.Json.parse s Actus.IO.Parse.testFileFromJson __do_lift

def Actus.IO.Parse.cashflowsOf (ct : Contract.Terms Float) (rf : Contract.RiskFactorEnv Float) : Protocol.Cashflows

Run the lending engine appropriate to the parsed contractType. Returns [] for contract types outside the implemented lending family.

Equations

• One or more equations did not get rendered due to their size.

def Actus.IO.Parse.cashflowsOfTestCase (tc : TestCase) (raw : Lean.Json) : Except String Protocol.Cashflows

Parse a test case and compute its cashflows under its own observed risk factors — the full file → cashflows pipeline.

Equations

• Actus.IO.Parse.cashflowsOfTestCase tc raw = do let rf ← Actus.IO.Parse.riskFactorsFromJson raw tc.terms pure (Actus.IO.Parse.cashflowsOf tc.terms rf)