storage_bytes.bend
stelliferous@0.0.3.0 · 87 lines · 0 definitions
1# Bytes read from a file, as a list of words 0..255: positions, little-endian
2# numbers, prefixes and text.
3import Base
4
5def at(bytes: List<&2,U32>,index: Nat) -> U32:
6 match bytes index:
7 case Nil{} index: 0
8 case Con{byte,rest} 0n: byte
9 case Con{byte,rest} 1n+before: at(rest,before)
10
11# A number stored least significant byte first; a position past the end reads 0.
12def u16_at(+bytes: List<&2,U32>,+index: Nat) -> U32:
13 (at(bytes,index) + at(bytes,1n+index) * 256 : U32)
14
15def u32_at(+bytes: List<&2,U32>,+index: Nat) -> U32:
16 (u16_at(bytes,index) + u16_at(bytes,2n+index) * 65536 : U32)
17
18def starts(pattern: List<&2,U32>,bytes: List<&2,U32>) -> Bool:
19 match pattern bytes:
20 case Nil{} bytes: True{}
21 case Con{first,rest} Nil{}: False{}
22 case Con{first,rest} Con{byte,more}: U32.is_eq(first,byte) && starts(rest,more)
23
24def ends(+bytes: List<&2,U32>,+pattern: List<&2,U32>) -> Bool:
25 starts(pattern,List.drop(&2,U32,bytes,Nat.sub(List.length(&2,U32,bytes),List.length(&2,U32,pattern))))
26
27def same(left: List<&2,U32>,right: List<&2,U32>) -> Bool:
28 match left right:
29 case Nil{} Nil{}: True{}
30 case Nil{} Con{byte,rest}: False{}
31 case Con{byte,rest} Nil{}: False{}
32 case Con{first,rest} Con{second,more}: U32.is_eq(first,second) && same(rest,more)
33
34# The position of the last occurrence of the pattern, if any.
35def last_start(bytes: List<&2,U32>,+pattern: List<&2,U32>,+index: U32,+best: Maybe<&2,U32>) -> Maybe<&2,U32>:
36 match bytes:
37 case Nil{}: best
38 case Con{+byte,+rest}:
39 last_start(rest,pattern,(index + 1 : U32),Bool.pick(Maybe<&2,U32>,starts(pattern,byte <> rest),Some{index},best))
40
41# ASCII text as bytes.
42def codes(text: String) -> List<&2,U32>:
43 match text:
44 case SNil{}: []
45 case SCon{head,tail}: Char.to_u32(head) <> codes(tail)
46
47# UTF-8 bytes as text. A lead byte opens a code point of one to four bytes; each
48# continuation byte adds six bits. A byte that fits no sequence is taken as is.
49
50type Decoding is Data:
51 Decoding{characters: List<&2,Char>,code: U32,remaining: U32}
52
53def opened(four: Bool,three: Bool,two: Bool,+byte: U32,characters: List<&2,Char>) -> Decoding:
54 match four three two:
55 case True{} three two: Decoding{characters,(byte - 240 : U32),3}
56 case False{} True{} two: Decoding{characters,(byte - 224 : U32),2}
57 case False{} False{} True{}: Decoding{characters,(byte - 192 : U32),1}
58 case False{} False{} False{}: Decoding{Char.from_u32(byte) <> characters,0,0}
59
60def lead(+byte: U32,characters: List<&2,Char>) -> Decoding:
61 opened(U32.is_le(240,byte),U32.is_le(224,byte),U32.is_le(192,byte),byte,characters)
62
63def continued(last: Bool,+byte: U32,characters: List<&2,Char>,+code: U32,+remaining: U32) -> Decoding:
64 match last:
65 case True{}: Decoding{Char.from_u32((code * 64 + byte - 128 : U32)) <> characters,0,0}
66 case False{}: Decoding{characters,(code * 64 + byte - 128 : U32),(remaining - 1 : U32)}
67
68def stepped(fresh: Bool,+byte: U32,characters: List<&2,Char>,+code: U32,+remaining: U32) -> Decoding:
69 match fresh:
70 case True{}: lead(byte,characters)
71 case False{}: continued(U32.is_eq(remaining,1),byte,characters,code,remaining)
72
73def absorbed(+byte: U32,decoding: Decoding) -> Decoding:
74 Decoding{characters,+code,+remaining} = decoding
75 stepped(U32.is_zero(remaining),byte,characters,code,remaining)
76
77def finished(decoding: Decoding) -> String:
78 Decoding{characters,code,remaining} = decoding
79 String.from_list(List.reverse(&2,Char,characters))
80
81def decoded(bytes: List<&2,U32>,decoding: Decoding) -> String:
82 match bytes:
83 case Nil{}: finished(decoding)
84 case Con{byte,rest}: decoded(rest,absorbed(byte,decoding))
85
86def text(bytes: List<&2,U32>) -> String:
87 decoded(bytes,Decoding{[],0,0})