1	# A ZIP archive read through the official File effects. The end record locates
2	# the central directory, which names every entry with its size and the offset of
3	# its local header; the entry's bytes follow that header. Only stored entries
4	# are read, the form torch.save writes.
5	import Base
6	import ./storage_bytes.bend as Bytes
7	
8	# An entry: its name as bytes, the offset of its local header, its length and
9	# its compression method, 0 for stored.
10	type Record is Data:
11	  Record{name: List<&2,U32>,header: U32,length: U32,method: U32}
12	
13	type Listing is Data:
14	  Records{records: List<&2,Record>}
15	  Unreadable{detail: String}
16	
17	type Fetched is Type:
18	  Fetched{file: File,bytes: Maybe<&2,List<&2,U32>>}
19	
20	def Read() -> Type:
21	  File & Result<&1,&1,U32 & String,List<&2,U32>>
22	
23	def Sized() -> Type:
24	  File & Result<&1,&1,U32 & String,U32>
25	
26	# Signatures, least significant byte first.
27	def central_signature() -> U32:
28	  33639248
29	
30	def local_signature() -> U32:
31	  67324752
32	
33	def end_signature() -> List<&2,U32>:
34	  [80,75,5,6]
35	
36	# A central directory entry is 46 bytes, then its name, extra field and comment.
37	def records(fuel: Nat,valid: Bool,+bytes: List<&2,U32>,found: List<&2,Record>) -> Listing:
38	  match fuel valid:
39	    case 0n valid: Records{List.reverse(&2,Record,found)}
40	    case 1n+rest False{}: Unreadable{"has a damaged central directory"}
41	    case 1n+rest True{}:
42	      +name_length = Bytes.u16_at(bytes,28n)
43	      +skipped = U32.to_nat((46 + name_length + Bytes.u16_at(bytes,30n) + Bytes.u16_at(bytes,32n) : U32))
44	      +next = List.drop(&2,U32,bytes,skipped)
45	      records(rest,U32.is_eq(Bytes.u32_at(next,0n),central_signature()),next,
46	        Record{List.take(&2,U32,List.drop(&2,U32,bytes,46n),U32.to_nat(name_length)),Bytes.u32_at(bytes,42n),Bytes.u32_at(bytes,24n),Bytes.u16_at(bytes,10n)} <> found)
47	
48	def directory_read(result: Result<&1,&1,U32 & String,List<&2,U32>>,+count: U32) -> Listing:
49	  match result:
50	    case Fail{error}: Unreadable{"cannot be read"}
51	    case Done{+bytes}: records(U32.to_nat(count),U32.is_eq(Bytes.u32_at(bytes,0n),central_signature()),bytes,[])
52	
53	def directory_fetched(read: Read(),+count: U32) -> File & Listing:
54	  (file,result) = read
55	  (file,directory_read(result,count))
56	
57	def ending(wide: Bool,file: File,+count: U32,+size: U32,+offset: U32) -> IO(File & Listing):
58	  match wide:
59	    case True{}: IO.pure(File & Listing,(file,Unreadable{"is a ZIP64 archive"}))
60	    case False{}:
61	      do IO<File & Listing>:
62	        read : Read() <- File.read_at(file,offset,size)
63	        IO.pure(File & Listing,directory_fetched(read,count))
64	
65	# The end record: entry count at byte 10, directory size at 12 and offset at 16.
66	# A count or an offset of all ones means ZIP64, which a 32-bit file never needs.
67	def end_found(found: Maybe<&2,U32>,+tail: List<&2,U32>,file: File) -> IO(File & Listing):
68	  match found:
69	    case None{}: IO.pure(File & Listing,(file,Unreadable{"is not a ZIP archive"}))
70	    case Some{+start}:
71	      +count = Bytes.u16_at(tail,U32.to_nat((start + 10 : U32)))
72	      +size = Bytes.u32_at(tail,U32.to_nat((start + 12 : U32)))
73	      +offset = Bytes.u32_at(tail,U32.to_nat((start + 16 : U32)))
74	      ending(U32.is_eq(count,65535) || U32.is_eq(offset,4294967295),file,count,size,offset)
75	
76	def tail_read(result: Result<&1,&1,U32 & String,List<&2,U32>>,file: File) -> IO(File & Listing):
77	  match result:
78	    case Fail{error}: IO.pure(File & Listing,(file,Unreadable{"cannot be read"}))
79	    case Done{+tail}: end_found(Bytes.last_start(tail,end_signature(),0,None{}),tail,file)
80	
81	def tail_fetched(read: Read()) -> IO(File & Listing):
82	  (file,result) = read
83	  tail_read(result,file)
84	
85	# The end record is 22 bytes plus a comment of at most 65535.
86	def measured(result: Result<&1,&1,U32 & String,U32>,file: File) -> IO(File & Listing):
87	  match result:
88	    case Fail{error}: IO.pure(File & Listing,(file,Unreadable{"cannot be measured"}))
89	    case Done{+size}:
90	      +tail = U32.min(size,65557)
91	      do IO<File & Listing>:
92	        read : Read() <- File.read_at(file,(size - tail : U32),tail)
93	        tail_fetched(read)
94	
95	def sized(sized: Sized()) -> IO(File & Listing):
96	  (file,result) = sized
97	  measured(result,file)
98	
99	# The entries of an open file, in directory order.
100	def directory(file: File) -> IO(File & Listing):
101	  do IO<File & Listing>:
102	    size : Sized() <- File.size(file)
103	    sized(size)
104	
105	def find(records: List<&2,Record>,+name: List<&2,U32>) -> Maybe<&2,Record>:
106	  match records:
107	    case Nil{}: None{}
108	    case Con{Record{+entry,+header,+length,+method},rest}:
109	      Bool.pick(Maybe<&2,Record>,Bytes.same(entry,name),Some{Record{entry,header,length,method}},find(rest,name))
110	
111	def first_matching(records: List<&2,Record>,+suffix: List<&2,U32>) -> Maybe<&2,Record>:
112	  match records:
113	    case Nil{}: None{}
114	    case Con{Record{+entry,+header,+length,+method},rest}:
115	      Bool.pick(Maybe<&2,Record>,Bytes.ends(entry,suffix),Some{Record{entry,header,length,method}},first_matching(rest,suffix))
116	
117	# The local header is 30 bytes, then the name and the extra field; the data follows.
118	def located(valid: Bool,+bytes: List<&2,U32>,+header: U32) -> Maybe<&2,U32>:
119	  match valid:
120	    case False{}: None{}
121	    case True{}: Some{(header + 30 + Bytes.u16_at(bytes,26n) + Bytes.u16_at(bytes,28n) : U32)}
122	
123	def header_read(result: Result<&1,&1,U32 & String,List<&2,U32>>,+header: U32) -> Maybe<&2,U32>:
124	  match result:
125	    case Fail{error}: None{}
126	    case Done{+bytes}: located(U32.is_eq(Bytes.u32_at(bytes,0n),local_signature()),bytes,header)
127	
128	def header_fetched(read: Read(),+header: U32) -> File & Maybe<&2,U32>:
129	  (file,result) = read
130	  (file,header_read(result,header))
131	
132	# The offset of the first byte of a stored entry. A compressed entry has none.
133	def stored_offset(stored: Bool,file: File,+header: U32) -> IO(File & Maybe<&2,U32>):
134	  match stored:
135	    case True{}:
136	      do IO<File & Maybe<&2,U32>>:
137	        read : Read() <- File.read_at(file,header,30)
138	        IO.pure(File & Maybe<&2,U32>,header_fetched(read,header))
139	    case False{}: IO.pure(File & Maybe<&2,U32>,(file,None{}))
140	
141	def data_offset(file: File,+record: Record) -> IO(File & Maybe<&2,U32>):
142	  Record{name,+header,length,+method} = record
143	  stored_offset(U32.is_eq(method,0),file,header)
144	
145	def entry_read(result: Result<&1,&1,U32 & String,List<&2,U32>>,+length: U32) -> Maybe<&2,List<&2,U32>>:
146	  match result:
147	    case Fail{error}: None{}
148	    case Done{+bytes}: Bool.pick(Maybe<&2,List<&2,U32>>,Nat.is_eq(List.length(&2,U32,bytes),U32.to_nat(length)),Some{bytes},None{})
149	
150	def entry_fetched(read: Read(),+length: U32) -> Fetched:
151	  (file,result) = read
152	  Fetched{file,entry_read(result,length)}
153	
154	def entry_at(offset: Maybe<&2,U32>,file: File,+length: U32) -> IO(Fetched):
155	  match offset:
156	    case None{}: IO.pure(Fetched,Fetched{file,None{}})
157	    case Some{offset}:
158	      do IO<Fetched>:
159	        read : Read() <- File.read_at(file,offset,length)
160	        IO.pure(Fetched,entry_fetched(read,length))
161	
162	def entry_located(located: File & Maybe<&2,U32>,+length: U32) -> IO(Fetched):
163	  (file,offset) = located
164	  entry_at(offset,file,length)
165	
166	# Every byte of a stored entry in one read, for small entries.
167	def entry(file: File,+record: Record) -> IO(Fetched):
168	  Record{name,header,+length,method} = record
169	  do IO<Fetched>:
170	    located : File & Maybe<&2,U32> <- data_offset(file,Record{name,header,length,method})
171	    entry_located(located,length)