Strings as a single natural number

A string becomes one Nat by encoding the list of its code points through Encodable (List Nat). Every name leaf in the term family then occupies exactly one slot in the List Nat stream, so the decoders never have to split a string out of the middle of a list. The decode is made total by defaulting to the empty string; the round-trip only ever feeds it a valid encoding.

def MeTTaIL.encStr (s : String) : ℕ

Encode a string as a single natural number.

Equations

• MeTTaIL.encStr s = Encodable.encode (List.map Char.toNat s.toList)

def MeTTaIL.decStr (n : ℕ) : String

Decode a string from a single natural number, defaulting to "" on a malformed code.

Equations

• MeTTaIL.decStr n = match Encodable.decode n with | some l => String.ofList (List.map Char.ofNat l) | none => ""

@[simp]

theorem MeTTaIL.decStr_encStr (s : String) : decStr (encStr s) = s

DottedPath

Tags: 0 for base, 1 for qualified. DottedPath does not nest through a list of itself, so the decoder is a plain prefix-style parser whose recursion is on the structurally smaller tail.

def MeTTaIL.dpEnc : DottedPath → List ℕ

Serialise a dotted path to a List Nat.

Equations

• MeTTaIL.dpEnc (MeTTaIL.DottedPath.base s) = [0, MeTTaIL.encStr s]
• MeTTaIL.dpEnc (MeTTaIL.DottedPath.qualified s rest) = 1 :: MeTTaIL.encStr s :: MeTTaIL.dpEnc rest

def MeTTaIL.dpDec : List ℕ → Option (DottedPath × List ℕ)

Parse one dotted path off the front of a List Nat, returning the remainder.

Equations

• MeTTaIL.dpDec (0 :: n :: rest) = some (MeTTaIL.DottedPath.base (MeTTaIL.decStr n), rest)
• MeTTaIL.dpDec (1 :: n :: rest) = match MeTTaIL.dpDec rest with | some (p, rest') => some (MeTTaIL.DottedPath.qualified (MeTTaIL.decStr n) p, rest') | none => none
• MeTTaIL.dpDec x✝ = none

theorem MeTTaIL.dpDec_enc (p : DottedPath) (rest : List ℕ) : dpDec (dpEnc p ++ rest) = some (p, rest)

def MeTTaIL.dpDecTop (l : List ℕ) : Option DottedPath

Decode a dotted path from a List Nat that encodes exactly one.

Equations

• MeTTaIL.dpDecTop l = Option.map Prod.fst (MeTTaIL.dpDec l)

theorem MeTTaIL.dpDecTop_enc (p : DottedPath) : dpDecTop (dpEnc p) = some p

@[implicit_reducible]

instance MeTTaIL.instEncodableDottedPath : Encodable DottedPath

Equations

• MeTTaIL.instEncodableDottedPath = Encodable.ofLeftInjection MeTTaIL.dpEnc MeTTaIL.dpDecTop MeTTaIL.dpDecTop_enc

@[implicit_reducible]

instance MeTTaIL.instLinearOrderDottedPath : LinearOrder DottedPath

Equations

• MeTTaIL.instLinearOrderDottedPath = LinearOrder.lift' Encodable.encode ⋯

Cat

Tags: 0 idCat, 1 listOf, 2 arrow, 3 prod. The only non-recursive leaf is the idCat string, encoded as one Nat. Following Mathlib's Term.listDecode, catDecAll decodes the whole stream into a List Cat and recurses only on the tail; each constructor reclaims its sub-categories from the front of the decoded suffix. arrow consumes two, listOf one, and prod consumes a count-prefixed run.

def MeTTaIL.catEnc : Cat → List ℕ

Serialise a single category by natural structural recursion. A constructor's tag is followed by its sub-categories' encodings; prod adds a count prefix so its run can be reclaimed on decode.

Equations

• MeTTaIL.catEnc (MeTTaIL.Cat.idCat s) = [0, MeTTaIL.encStr s]
• MeTTaIL.catEnc c.listOf = 1 :: MeTTaIL.catEnc c
• MeTTaIL.catEnc (d.arrow c) = 2 :: MeTTaIL.catEnc d ++ MeTTaIL.catEnc c
• MeTTaIL.catEnc (MeTTaIL.Cat.prod ds) = 3 :: ds.length :: MeTTaIL.catEncL ds

def MeTTaIL.catEncL : List Cat → List ℕ

Serialise a list of categories by concatenating their encodings.

Equations

• MeTTaIL.catEncL [] = []
• MeTTaIL.catEncL (c :: cs) = MeTTaIL.catEnc c ++ MeTTaIL.catEncL cs

def MeTTaIL.catDecAll : List ℕ → List Cat

Decode a whole List Nat into the list of categories it encodes, recursing on the tail. A constructor reclaims its children from the front of the decoded suffix.

Equations

• MeTTaIL.catDecAll [] = []
• MeTTaIL.catDecAll (0 :: n :: rest) = MeTTaIL.Cat.idCat (MeTTaIL.decStr n) :: MeTTaIL.catDecAll rest
• MeTTaIL.catDecAll (1 :: rest) = match MeTTaIL.catDecAll rest with | c :: cs => c.listOf :: cs | [] => []
• MeTTaIL.catDecAll (2 :: rest) = match MeTTaIL.catDecAll rest with | d :: c :: cs => d.arrow c :: cs | x => []
• MeTTaIL.catDecAll (3 :: k :: rest) = MeTTaIL.Cat.prod (List.take k (MeTTaIL.catDecAll rest)) :: List.drop k (MeTTaIL.catDecAll rest)
• MeTTaIL.catDecAll x✝ = []

theorem MeTTaIL.catDecAll_enc (c : Cat) (rest : List ℕ) : catDecAll (catEnc c ++ rest) = c :: catDecAll rest

Decoding the whole stream after one category's encoding yields that category in front of whatever the suffix decodes to.

theorem MeTTaIL.catDecAll_encL (cs : List Cat) (rest : List ℕ) : catDecAll (catEncL cs ++ rest) = cs ++ catDecAll rest

Decoding the whole stream after a list of categories' encodings yields that list in front of whatever the suffix decodes to.

def MeTTaIL.catDecTop (l : List ℕ) : Option Cat

Decode a category from a List Nat that encodes exactly one.

Equations

• MeTTaIL.catDecTop l = (MeTTaIL.catDecAll l).head?

theorem MeTTaIL.catDecTop_enc (c : Cat) : catDecTop (catEnc c) = some c

@[implicit_reducible]

instance MeTTaIL.instEncodableCat : Encodable Cat

Equations

• MeTTaIL.instEncodableCat = Encodable.ofLeftInjection MeTTaIL.catEnc MeTTaIL.catDecTop MeTTaIL.catDecTop_enc

@[implicit_reducible]

instance MeTTaIL.instLinearOrderCat : LinearOrder Cat

Equations

• MeTTaIL.instLinearOrderCat = LinearOrder.lift' Encodable.encode ⋯

Label

Tags: 0 id, 1 wild, 2 listE, 3 listCons, 4 listOne. The three list labels carry a Cat, which is already Encodable, so it goes in as a single Nat. Label does not nest through a list of itself, so the decode is a plain non-recursive parser.

def MeTTaIL.lblEnc : Label → List ℕ

Serialise a label to a List Nat.

Equations

• MeTTaIL.lblEnc (MeTTaIL.Label.id s) = [0, MeTTaIL.encStr s]
• MeTTaIL.lblEnc MeTTaIL.Label.wild = [1]
• MeTTaIL.lblEnc (MeTTaIL.Label.listE c) = [2, Encodable.encode c]
• MeTTaIL.lblEnc (MeTTaIL.Label.listCons c) = [3, Encodable.encode c]
• MeTTaIL.lblEnc (MeTTaIL.Label.listOne c) = [4, Encodable.encode c]

def MeTTaIL.lblDec : List ℕ → Option (Label × List ℕ)

Parse one label off the front of a List Nat, returning the remainder. The Cat payload is decoded from its single Nat; a malformed code defaults to idCat "".

Equations

• MeTTaIL.lblDec (0 :: n :: rest) = some (MeTTaIL.Label.id (MeTTaIL.decStr n), rest)
• MeTTaIL.lblDec (1 :: rest) = some (MeTTaIL.Label.wild, rest)
• MeTTaIL.lblDec (2 :: n :: rest) = some (MeTTaIL.Label.listE ((Encodable.decode n).getD (MeTTaIL.Cat.idCat "")), rest)
• MeTTaIL.lblDec (3 :: n :: rest) = some (MeTTaIL.Label.listCons ((Encodable.decode n).getD (MeTTaIL.Cat.idCat "")), rest)
• MeTTaIL.lblDec (4 :: n :: rest) = some (MeTTaIL.Label.listOne ((Encodable.decode n).getD (MeTTaIL.Cat.idCat "")), rest)
• MeTTaIL.lblDec x✝ = none

theorem MeTTaIL.lblDec_enc (l : Label) (rest : List ℕ) : lblDec (lblEnc l ++ rest) = some (l, rest)

def MeTTaIL.lblDecTop (l : List ℕ) : Option Label

Decode a label from a List Nat that encodes exactly one.

Equations

• MeTTaIL.lblDecTop l = Option.map Prod.fst (MeTTaIL.lblDec l)

theorem MeTTaIL.lblDecTop_enc (l : Label) : lblDecTop (lblEnc l) = some l

@[implicit_reducible]

instance MeTTaIL.instEncodableLabel : Encodable Label

Equations

• MeTTaIL.instEncodableLabel = Encodable.ofLeftInjection MeTTaIL.lblEnc MeTTaIL.lblDecTop MeTTaIL.lblDecTop_enc

@[implicit_reducible]

instance MeTTaIL.instLinearOrderLabel : LinearOrder Label

Equations

• MeTTaIL.instLinearOrderLabel = LinearOrder.lift' Encodable.encode ⋯

AST

Tags: 0 var, 1 sexp, 2 subst. The non-recursive payloads (DottedPath for var and subst, Label for sexp) are already Encodable, so each goes in as a single Nat. The recursive sub-terms flow through the stream: sexp carries a count-prefixed run of arguments and subst carries two sub-terms. As with Cat, astDecAll decodes the whole stream into a List AST, recursing on the tail, and each constructor reclaims its children from the front of the decoded suffix.

def MeTTaIL.astEnc : AST → List ℕ

Serialise a single term by natural structural recursion. The single-Nat payloads (label, dotted paths) sit next to the tag; sexp adds a count prefix for its argument run.

Equations

• MeTTaIL.astEnc (MeTTaIL.AST.var p) = [0, Encodable.encode p]
• MeTTaIL.astEnc (MeTTaIL.AST.sexp l args) = 1 :: Encodable.encode l :: args.length :: MeTTaIL.astEncL args
• MeTTaIL.astEnc (body.subst repl v) = 2 :: Encodable.encode v :: MeTTaIL.astEnc body ++ MeTTaIL.astEnc repl

def MeTTaIL.astEncL : List AST → List ℕ

Serialise a list of terms by concatenating their encodings.

Equations

• MeTTaIL.astEncL [] = []
• MeTTaIL.astEncL (a :: as) = MeTTaIL.astEnc a ++ MeTTaIL.astEncL as

def MeTTaIL.astDecAll : List ℕ → List AST

Decode a whole List Nat into the list of terms it encodes, recursing on the tail.

Equations

• MeTTaIL.astDecAll [] = []
• MeTTaIL.astDecAll (0 :: n :: rest) = MeTTaIL.AST.var ((Encodable.decode n).getD (MeTTaIL.DottedPath.base "")) :: MeTTaIL.astDecAll rest
• MeTTaIL.astDecAll (1 :: n :: k :: rest) = MeTTaIL.AST.sexp ((Encodable.decode n).getD MeTTaIL.Label.wild) (List.take k (MeTTaIL.astDecAll rest)) :: List.drop k (MeTTaIL.astDecAll rest)
• MeTTaIL.astDecAll (2 :: n :: rest) = match MeTTaIL.astDecAll rest with | body :: repl :: as => body.subst repl ((Encodable.decode n).getD (MeTTaIL.DottedPath.base "")) :: as | x => []
• MeTTaIL.astDecAll x✝ = []

theorem MeTTaIL.astDecAll_enc (a : AST) (rest : List ℕ) : astDecAll (astEnc a ++ rest) = a :: astDecAll rest

Decoding the whole stream after one term's encoding yields that term in front of whatever the suffix decodes to.

theorem MeTTaIL.astDecAll_encL (as : List AST) (rest : List ℕ) : astDecAll (astEncL as ++ rest) = as ++ astDecAll rest

Decoding the whole stream after a list of terms' encodings yields that list in front of whatever the suffix decodes to.

def MeTTaIL.astDecTop (l : List ℕ) : Option AST

Decode a term from a List Nat that encodes exactly one.

Equations

• MeTTaIL.astDecTop l = (MeTTaIL.astDecAll l).head?

theorem MeTTaIL.astDecTop_enc (a : AST) : astDecTop (astEnc a) = some a

@[implicit_reducible]

instance MeTTaIL.instEncodableAST : Encodable AST

Equations

• MeTTaIL.instEncodableAST = Encodable.ofLeftInjection MeTTaIL.astEnc MeTTaIL.astDecTop MeTTaIL.astDecTop_enc

@[implicit_reducible]

instance MeTTaIL.instLinearOrderAST : LinearOrder AST

Equations

• MeTTaIL.instLinearOrderAST = LinearOrder.lift' Encodable.encode ⋯