1	# ezsys/src/errno: a file operation's failure written as Python writes an
2	# OSError: `[Errno N] <strerror>: <repr(path)>`. The text of a code is
3	# glibc's, from a table of common Linux codes; a code the table does not
4	# list is written with the message it came with. The path is written as
5	# Python's repr(str) writes it, for the characters up to U+00FF.
6	import Base
7	
8	# the codes and their texts, reusable
9	def err.Table() -> Data:
10	  List<&2, Sigma<&2, &2, U32, _ => String>>
11	
12	# the common Linux codes and glibc's text for each, as os.strerror gives it
13	def err.table() -> err.Table():
14	  [
15	    (1, "Operation not permitted"),
16	    (2, "No such file or directory"),
17	    (3, "No such process"),
18	    (4, "Interrupted system call"),
19	    (5, "Input/output error"),
20	    (6, "No such device or address"),
21	    (7, "Argument list too long"),
22	    (8, "Exec format error"),
23	    (9, "Bad file descriptor"),
24	    (10, "No child processes"),
25	    (11, "Resource temporarily unavailable"),
26	    (12, "Cannot allocate memory"),
27	    (13, "Permission denied"),
28	    (14, "Bad address"),
29	    (15, "Block device required"),
30	    (16, "Device or resource busy"),
31	    (17, "File exists"),
32	    (18, "Invalid cross-device link"),
33	    (19, "No such device"),
34	    (20, "Not a directory"),
35	    (21, "Is a directory"),
36	    (22, "Invalid argument"),
37	    (23, "Too many open files in system"),
38	    (24, "Too many open files"),
39	    (25, "Inappropriate ioctl for device"),
40	    (26, "Text file busy"),
41	    (27, "File too large"),
42	    (28, "No space left on device"),
43	    (29, "Illegal seek"),
44	    (30, "Read-only file system"),
45	    (31, "Too many links"),
46	    (32, "Broken pipe"),
47	    (33, "Numerical argument out of domain"),
48	    (34, "Numerical result out of range"),
49	    (35, "Resource deadlock avoided"),
50	    (36, "File name too long"),
51	    (37, "No locks available"),
52	    (38, "Function not implemented"),
53	    (39, "Directory not empty"),
54	    (40, "Too many levels of symbolic links"),
55	    (84, "Invalid or incomplete multibyte or wide character"),
56	    (95, "Operation not supported"),
57	    (110, "Connection timed out"),
58	    (111, "Connection refused"),
59	    (112, "Host is down"),
60	    (113, "No route to host"),
61	    (116, "Stale file handle"),
62	    (122, "Disk quota exceeded"),
63	    (125, "Operation canceled")
64	  ]
65	
66	# what is written when hit holds, else what the rest writes
67	def err.when(hit: Bool, yes: Unit -> String, no: Unit -> String) -> String:
68	  match hit:
69	    case True{}:
70	      yes(Unit{})
71	    case False{}:
72	      no(Unit{})
73	
74	# the text of the first pair with the code, or why when there is none
75	def err.look(table: err.Table(), +code: U32, +why: String) -> String:
76	  match table:
77	    case Nil{}:
78	      why
79	    case Con{(k, text), rest}:
80	      err.when(U32.is_eq(code, k), _u => text, _u => err.look(rest, code, why))
81	
82	# a code's text: the table's, or why when the table does not list it
83	def err.text(+code: U32, +why: String) -> String:
84	  err.look(err.table(), code, why)
85	
86	# the quote a path is written between: " when it holds a ' and no ", else '
87	def err.quote.pick(dq: Bool) -> Char:
88	  match dq:
89	    case True{}:
90	      '"'
91	    case False{}:
92	      '\''
93	
94	# the quote repr picks for a path
95	def err.quote(+path: String) -> Char:
96	  err.quote.pick(Bool.and(String.contains(path, "'"),
97	    Bool.not(String.contains(path, "\""))))
98	
99	# the code points repr writes as \xhh: below U+0020, U+007F to U+00A0, and
100	# U+00AD
101	def err.hexed(+cp: U32) -> Bool:
102	  Bool.or(U32.is_lt(cp, 32),
103	    Bool.or(Bool.and(U32.is_ge(cp, 127), U32.is_le(cp, 160)),
104	      U32.is_eq(cp, 173)))
105	
106	# a digit's character, or '0' past the digits
107	def err.hex.or(got: Maybe<&2, Char>) -> Char:
108	  match got:
109	    case None{}:
110	      '0'
111	    case Some{chr}:
112	      chr
113	
114	# the lowercase hex digit of a number's last four bits
115	def err.hex.digit(num: U32) -> Char:
116	  err.hex.or(String.get("0123456789abcdef", U32.to_nat((num % 16 : U32))))
117	
118	# two lowercase hex digits of a number's last eight bits
119	def err.hex2(+cp: U32) -> String:
120	  SCon{err.hex.digit((cp / 16 : U32)), SCon{err.hex.digit(cp), SNil{}}}
121	
122	# a control character: \t, \n, \r, or \xhh
123	def err.ctl(+cp: U32) -> String:
124	  err.when(U32.is_eq(cp, 9), _u => "\\t",
125	    _u => err.when(U32.is_eq(cp, 10), _v => "\\n",
126	      _v => err.when(U32.is_eq(cp, 13), _w => "\\r",
127	        _w => "\\x" ++ err.hex2(cp))))
128	
129	# any other character: a backslash or the quote escaped, else itself
130	def err.plain(+qt: Char, +cp: U32) -> String:
131	  err.when(U32.is_eq(cp, 92), _u => "\\\\",
132	    _u => err.when(Char.is_eq(Chr{cp}, qt), _v => SCon{'\\', SCon{qt, SNil{}}},
133	      _v => SCon{Chr{cp}, SNil{}}))
134	
135	# one character of a path between the quote q
136	def err.esc(+qt: Char, chr: Char) -> String:
137	  match chr:
138	    case Chr{+cp}:
139	      err.when(err.hexed(cp), _u => err.ctl(cp), _u => err.plain(qt, cp))
140	
141	# a path's characters between the quote q
142	def err.go(+qt: Char, path: String) -> String:
143	  match path:
144	    case SNil{}:
145	      SNil{}
146	    case SCon{chr, t}:
147	      err.esc(qt, chr) ++ err.go(qt, t)
148	
149	# a path as Python's repr(str) writes it
150	def err.repr(+path: String) -> String:
151	  +qt = err.quote(path)
152	  SCon{qt, err.go(qt, path) ++ SCon{qt, SNil{}}}
153	
154	# a failed file operation as Python's OSError writes it
155	def err.os(+code: U32, +why: String, +path: String) -> String:
156	  "[Errno " ++ U32.show(code) ++ "] " ++ err.text(code, why) ++ ": "
157	    ++ err.repr(path)