Stream types for Unicode Character Database (UCD) files.

Unicode data files are semicolon ; (U+003B) separated fields, except for Unihan files and a few others that are tab (U+0009) separated. White spaces around field values are not significant. Line comments are prefixed with a number sign # (U+0023).

structure Unicode.UCDStream (withComments : Bool := false) extends String.Slice : Type

UCD stream type

Comments and blank lines are omitted in this stream type. Use UCDStreamWithComments if you need comments.

• str : String
• startInclusive : self.str.Pos
• endExclusive : self.str.Pos
• startInclusive_le_endExclusive : self.startInclusive ≤ self.endExclusive
• isUnihan : Bool

  isUnihan is true if the records are tab separated

@[instance_reducible]

instance Unicode.instInhabitedUCDStream {a✝ : Bool} : Inhabited (UCDStream a✝)

Equations

• Unicode.instInhabitedUCDStream = { default := Unicode.instInhabitedUCDStream.default }

@[reducible, inline]

abbrev Unicode.UCDStreamWithComments : Type

UCD stream type with comments

Comments and blank lines are included in this stream type. Use UCDStream if you do not need comments.

Equations

• Unicode.UCDStreamWithComments = Unicode.UCDStream true

@[reducible, inline]

abbrev Unicode.UCDStream.ofStringSlice (str : String.Slice) (withComments isUnihan : Bool := false) : UCDStream withComments

Make a UCDStream from a string slice

Equations

• Unicode.UCDStream.ofStringSlice str withComments isUnihan = { toSlice := str, isUnihan := isUnihan }

@[reducible, inline]

abbrev Unicode.UCDStream.ofString (str : String) (withComments isUnihan : Bool := false) : UCDStream withComments

Make a UCDStream from a string

Equations

• Unicode.UCDStream.ofString str withComments isUnihan = Unicode.UCDStream.ofStringSlice str.toSlice withComments isUnihan

@[reducible, inline]

abbrev Unicode.UCDStream.ofSubstring (str : Substring.Raw) (withComments isUnihan : Bool := false) : UCDStream withComments

Make a UCDStream from a substring

Equations

• Unicode.UCDStream.ofSubstring str withComments isUnihan = Unicode.UCDStream.ofStringSlice str.toString.toSlice withComments isUnihan

@[reducible, inline]

abbrev Unicode.UCDStream.ofFile (path : System.FilePath) (withComments isUnihan : Bool := false) : IO (UCDStream withComments)

Make a UCDStream from a file

Equations

• Unicode.UCDStream.ofFile path withComments isUnihan = (fun (str : String) => Unicode.UCDStream.ofString str withComments isUnihan) <$> IO.FS.readFile path

def Unicode.UCDStream.nextLine? {withComments : Bool} (stream : UCDStream withComments) : Option (String.Slice × String.Slice × UCDStream withComments)

Get the next line from the UCDStream

Equations

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

@[instance_reducible]

instance Unicode.UCDStream.instStreamFalseArraySlice : Std.Stream UCDStream (Array String.Slice)

Equations

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

@[instance_reducible]

instance Unicode.UCDStream.instStreamUCDStreamWithCommentsProdArraySlice : Std.Stream UCDStreamWithComments (Array String.Slice × String.Slice)

Equations

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