def CordialMiners.encodeFact {Wave : Type u_1} {Hash : Type u_2} (eW : Wave → Sexpr) (eH : Hash → Sexpr) : TrecFact Wave Hash → Sexpr

Encode a coarse fact as a MeTTaIL atom: a head symbol naming the fact, followed by its encoded fields. The ordered prefix is encoded as the head symbol consed onto the encoded hash list.

Equations

• CordialMiners.encodeFact eW eH (CordialMiners.TrecFact.propose w h) = CordialMiners.Sexpr.app [CordialMiners.Sexpr.sym "propose", eW w, eH h]
• CordialMiners.encodeFact eW eH (CordialMiners.TrecFact.qApprove w h) = CordialMiners.Sexpr.app [CordialMiners.Sexpr.sym "q-approve", eW w, eH h]
• CordialMiners.encodeFact eW eH (CordialMiners.TrecFact.certThresh w h) = CordialMiners.Sexpr.app [CordialMiners.Sexpr.sym "cert-threshold", eW w, eH h]
• CordialMiners.encodeFact eW eH (CordialMiners.TrecFact.final w h) = CordialMiners.Sexpr.app [CordialMiners.Sexpr.sym "final", eW w, eH h]
• CordialMiners.encodeFact eW eH (CordialMiners.TrecFact.finalLeader w h) = CordialMiners.Sexpr.app [CordialMiners.Sexpr.sym "final-leader", eW w, eH h]
• CordialMiners.encodeFact eW eH (CordialMiners.TrecFact.orderedPrefix hs) = CordialMiners.Sexpr.app (CordialMiners.Sexpr.sym "ordered-prefix" :: List.map eH hs)

def CordialMiners.decodeFact {Wave : Type u_1} {Hash : Type u_2} (dW : Sexpr → Option Wave) (dH : Sexpr → Option Hash) : Sexpr → Option (TrecFact Wave Hash)

Parse a MeTTaIL atom back into a coarse fact, matching on the head symbol and field arity. Anything that does not match a known shape decodes to none.

Equations

• One or more equations did not get rendered due to their size.
• CordialMiners.decodeFact dW dH (CordialMiners.Sexpr.app (CordialMiners.Sexpr.sym "ordered-prefix" :: rest)) = Option.map CordialMiners.TrecFact.orderedPrefix (List.mapM dH rest)
• CordialMiners.decodeFact dW dH x✝ = none

theorem CordialMiners.mapM_map_leftInv {Hash : Type u_2} (e : Hash → Sexpr) (d : Sexpr → Option Hash) (hd : ∀ (a : Hash), d (e a) = some a) (l : List Hash) : List.mapM d (List.map e l) = some l

A list of encoded items decodes back to the original list, given a field codec that is a left inverse. The list mirror of the round-trip property.

theorem CordialMiners.extract_decode_encode {Wave : Type u_1} {Hash : Type u_2} (eW : Wave → Sexpr) (eH : Hash → Sexpr) (dW : Sexpr → Option Wave) (dH : Sexpr → Option Hash) (hW : ∀ (w : Wave), dW (eW w) = some w) (hH : ∀ (h : Hash), dH (eH h) = some h) (f : TrecFact Wave Hash) : decodeFact dW dH (encodeFact eW eH f) = some f

Extraction is lossless: decoding an encoded fact recovers it exactly, provided the field codecs are left inverses (dW (eW w) = some w and dH (eH h) = some h). Every coarse fact therefore has a faithful MeTTaIL image.