1	# Bytes read from a file, as a list of words 0..255: positions, little-endian
2	# numbers, prefixes and text.
3	import Base
4	
5	def 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.
12	def u16_at(+bytes: List<&2,U32>,+index: Nat) -> U32:
13	  (at(bytes,index) + at(bytes,1n+index) * 256 : U32)
14	
15	def u32_at(+bytes: List<&2,U32>,+index: Nat) -> U32:
16	  (u16_at(bytes,index) + u16_at(bytes,2n+index) * 65536 : U32)
17	
18	def 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	
24	def 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	
27	def 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.
35	def 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.
42	def 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	
50	type Decoding is Data:
51	  Decoding{characters: List<&2,Char>,code: U32,remaining: U32}
52	
53	def 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	
60	def 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	
63	def 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	
68	def 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	
73	def absorbed(+byte: U32,decoding: Decoding) -> Decoding:
74	  Decoding{characters,+code,+remaining} = decoding
75	  stepped(U32.is_zero(remaining),byte,characters,code,remaining)
76	
77	def finished(decoding: Decoding) -> String:
78	  Decoding{characters,code,remaining} = decoding
79	  String.from_list(List.reverse(&2,Char,characters))
80	
81	def 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	
86	def text(bytes: List<&2,U32>) -> String:
87	  decoded(bytes,Decoding{[],0,0})