def Ion.isIonFile (bytes : ByteArray) : Bool

Returns true if this starts with the Ion binary version marker.

Equations

• Ion.isIonFile bytes = ByteArray.startsWith✝ bytes Ion.binaryVersionMarker

structure Ion.Position : Type

• indices : Array Nat

@[implicit_reducible]

instance Ion.instReprPosition : Repr Position

Equations

• Ion.instReprPosition = { reprPrec := Ion.instReprPosition.repr }

def Ion.instReprPosition.repr : Position → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Ion.Position.instToString : ToString Position

Equations

• Ion.Position.instToString = { toString := fun (p : Ion.Position) => have l := (Array.map toString p.indices).toList; ".".intercalate ("root" :: l) }

def Ion.SymbolTable.localSymbolTableValue (tbl : SymbolTable) : Ion SymbolId

Create value

Equations

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

def Ion.SymbolTable.ofLocalSymbolTable (v : Ion SymbolId) : Except (Position × String) SymbolTable

Equations

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

def Ion.InternM (α : Type) : Type

Monad for constructing local symbol table for values.

Equations

• Ion.InternM = StateM Ion.SymbolTable

@[implicit_reducible]

instance Ion.instMonadInternM : Monad InternM

Equations

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

def Ion.runIntern {α : Type} (act : InternM α) (symbols : SymbolTable := SymbolTable.system) : SymbolTable × α

Equations

• Ion.runIntern act symbols = match act symbols with | (v, tbl) => (tbl, v)

def Ion.internSymbol (s : String) : InternM SymbolId

Equations

• Ion.internSymbol s = Ion.SymbolTable.intern s

@[irreducible]

def Ion.Ion.mapSymbolM {m : Type → Type u_1} {α β : Type} [Monad m] (f : α → m β) : Ion α → m (Ion β)

Resolve string symbols to symbol ids by constructing local symbol table.

Equations

• One or more equations did not get rendered due to their size.
• Ion.Ion.mapSymbolM f { app := Ion.IonF.null tp } = pure (Ion.Ion.null tp)
• Ion.Ion.mapSymbolM f { app := Ion.IonF.bool x_1 } = pure (Ion.Ion.bool x_1)
• Ion.Ion.mapSymbolM f { app := Ion.IonF.int x_1 } = pure (Ion.Ion.int x_1)
• Ion.Ion.mapSymbolM f { app := Ion.IonF.float f_1 } = pure (Ion.Ion.float f_1)
• Ion.Ion.mapSymbolM f { app := Ion.IonF.decimal d } = pure (Ion.Ion.decimal d)
• Ion.Ion.mapSymbolM f { app := Ion.IonF.string s } = pure (Ion.Ion.string s)
• Ion.Ion.mapSymbolM f { app := Ion.IonF.symbol s } = Ion.Ion.symbol <$> f s
• Ion.Ion.mapSymbolM f { app := Ion.IonF.blob s } = pure (Ion.Ion.blob s)
• Ion.Ion.mapSymbolM f { app := Ion.IonF.annotation l v } = do let l ← Array.mapM f l let __do_lift ← Ion.Ion.mapSymbolM f v pure (Ion.Ion.annotation l __do_lift)

def Ion.Ion.intern : Ion String → InternM (Ion SymbolId)

Resolve string symbols to symbol ids by constructing local symbol table.

Equations

• Ion.Ion.intern = Ion.Ion.mapSymbolM Ion.internSymbol

def Ion.Ion.unintern (tbl : SymbolTable) (v : Ion SymbolId) : Ion String

Equations

• Ion.Ion.unintern tbl v = (Ion.Ion.mapSymbolM (fun (s : Ion.SymbolId) => pure tbl[s]!) v).run

def Ion.intern (values : List (Ion String)) (symbols : SymbolTable := SymbolTable.system) : Array (Ion SymbolId)

Equations

• Ion.intern values symbols = match Ion.runIntern (List.mapM (fun (x : Ion.Ion String) => x.intern) values) symbols with | (tbl, v) => (tbl.localSymbolTableValue :: v).toArray

def Ion.internAndSerialize (values : List (Ion String)) (symbols : SymbolTable := SymbolTable.system) : ByteArray

Write values

Equations

• Ion.internAndSerialize values symbols = Ion.serialize (Ion.intern values symbols)

def Ion.writeBinaryFile (path : System.FilePath) (values : List (Ion String)) (symbols : SymbolTable := SymbolTable.system) : IO Unit

Write a list of Ion values to file.

Equations

• Ion.writeBinaryFile path values symbols = IO.FS.writeBinFile path (Ion.internAndSerialize values symbols)