1	import Base
2	
3	# Canonical bounded decimal support for compact storage formats.
4	# The scanner consumes one character per recursive step and never splits input.
5	
6	type Error is Data:
7	  Empty{}
8	  LeadingZero{}
9	  NonDigit{}
10	  Overflow{}
11	  MissingDelimiter{}
12	
13	type Stop is Data:
14	  Delimited{delimiter: Char}
15	  Complete{}
16	
17	type Parsed is Data:
18	  Dec{value: Nat, rest: String}
19	
20	type Parse is Data:
21	  Rejected{error: Error}
22	  Accepted{parsed: Parsed}
23	
24	type Scan is Data:
25	  Reading{value: Nat, started: Bool, leading_zero: Bool}
26	  Finished{value: Nat}
27	  Failed{error: Error}
28	
29	def render(num: Nat) -> String:
30	  Nat.show(num)
31	
32	def is_digit_code(+code: U32) -> Bool:
33	  Bool.and(U32.is_le(48, code), U32.is_le(code, 57))
34	
35	def digit_dec(ok: Bool, code: U32) -> Maybe<&2, Nat>:
36	  match ok:
37	    case False{}:
38	      None{}
39	    case True{}:
40	      Some{U32.to_nat(U32.sub(code, 48))}
41	
42	def digit_of(ch: Char) -> Maybe<&2, Nat>:
43	  +code = Char.to_u32(ch)
44	  digit_dec(is_digit_code(code), code)
45	
46	def within_digit_limit(digit_ok: Bool, acc: Nat, digit: Nat, limit: Nat) -> Bool:
47	  match digit_ok:
48	    case False{}:
49	      False{}
50	    case True{}:
51	      Nat.is_le(acc, Nat.div(Nat.sub(limit, digit), 10n))
52	
53	def can_accumulate(acc: Nat, +digit: Nat, +limit: Nat) -> Bool:
54	  within_digit_limit(Nat.is_le(digit, limit), acc, digit, limit)
55	
56	def accumulated(ok: Bool, acc: Nat, digit: Nat, leading_zero: Bool) -> Scan:
57	  match ok:
58	    case False{}:
59	      Failed{Overflow{}}
60	    case True{}:
61	      Reading{Nat.add(Nat.mul(acc, 10n), digit), True{}, leading_zero}
62	
63	def next_digit_zero(started: Bool, leading_zero: Bool, +acc: Nat, +digit: Nat, limit: Nat) -> Scan:
64	  match started:
65	    case False{}:
66	      accumulated(can_accumulate(acc, digit, limit), acc, digit, True{})
67	    case True{}:
68	      match leading_zero:
69	        case True{}:
70	          Failed{LeadingZero{}}
71	        case False{}:
72	          accumulated(can_accumulate(acc, digit, limit), acc, digit, False{})
73	
74	def next_digit_nonzero(leading_zero: Bool, +acc: Nat, +digit: Nat, limit: Nat) -> Scan:
75	  match leading_zero:
76	    case True{}:
77	      Failed{LeadingZero{}}
78	    case False{}:
79	      accumulated(can_accumulate(acc, digit, limit), acc, digit, False{})
80	
81	def next_digit_value(+digit: Nat, started: Bool, leading_zero: Bool, acc: Nat, limit: Nat) -> Scan:
82	  match digit:
83	    case 0n:
84	      next_digit_zero(started, leading_zero, acc, 0n, limit)
85	    case 1n+p:
86	      next_digit_nonzero(leading_zero, acc, 1n+p, limit)
87	
88	def next_digit(+digit: Maybe<&2, Nat>, started: Bool, leading_zero: Bool, acc: Nat, limit: Nat) -> Scan:
89	  match digit:
90	    case None{}:
91	      Failed{NonDigit{}}
92	    case Some{d}:
93	      next_digit_value(d, started, leading_zero, acc, limit)
94	
95	def finish_field(started: Bool, acc: Nat) -> Scan:
96	  match started:
97	    case False{}:
98	      Failed{Empty{}}
99	    case True{}:
100	      Finished{acc}
101	
102	def delimited_step(is_delimiter: Bool, ch: Char, acc: Nat, started: Bool, leading_zero: Bool, limit: Nat) -> Scan:
103	  match is_delimiter:
104	    case True{}:
105	      finish_field(started, acc)
106	    case False{}:
107	      next_digit(digit_of(ch), started, leading_zero, acc, limit)
108	
109	def scan_step(+ch: Char, st: Scan, limit: Nat, stop: Stop) -> Scan:
110	  match st:
111	    case Finished{value}:
112	      Finished{value}
113	    case Failed{error}:
114	      Failed{error}
115	    case Reading{value, started, leading_zero}:
116	      match stop:
117	        case Complete{}:
118	          next_digit(digit_of(ch), started, leading_zero, value, limit)
119	        case Delimited{delimiter}:
120	          delimited_step(Char.is_eq(ch, delimiter), ch, value, started, leading_zero, limit)
121	
122	def complete_end(started: Bool, value: Nat, rest: String) -> Parse:
123	  match started:
124	    case False{}:
125	      Rejected{Empty{}}
126	    case True{}:
127	      Accepted{Dec{value, rest}}
128	
129	def scan_end(st: Scan, rest: String, stop: Stop) -> Parse:
130	  match st:
131	    case Finished{value}:
132	      Accepted{Dec{value, rest}}
133	    case Failed{error}:
134	      Rejected{error}
135	    case Reading{value, started, leading_zero}:
136	      match stop:
137	        case Delimited{delimiter}:
138	          Rejected{MissingDelimiter{}}
139	        case Complete{}:
140	          complete_end(started, value, rest)
141	
142	def scan(rest: String, st: Scan, +limit: Nat, +stop: Stop) -> Parse:
143	  match rest st:
144	    case _ Finished{value}:
145	      Accepted{Dec{value, rest}}
146	    case _ Failed{error}:
147	      Rejected{error}
148	    case SNil{} Reading{value, started, leading_zero}:
149	      scan_end(Reading{value, started, leading_zero}, "", stop)
150	    case SCon{c, t} Reading{value, started, leading_zero}:
151	      scan(t, scan_step(c, Reading{value, started, leading_zero}, limit, stop), limit, stop)
152	
153	def parse_with_stop(str: String, limit: Nat, stop: Stop) -> Parse:
154	  scan(str, Reading{0n, False{}, False{}}, limit, stop)
155	
156	def parse_delimited(str: String, limit: Nat, delimiter: Char) -> Parse:
157	  parse_with_stop(str, limit, Delimited{delimiter})
158	
159	def parse_semicolon(str: String, limit: Nat) -> Parse:
160	  parse_delimited(str, limit, ';')
161	
162	def parse_complete(str: String, limit: Nat) -> Parse:
163	  parse_with_stop(str, limit, Complete{})
164	
165	def parsed_value(parsed: Parsed) -> Nat:
166	  match parsed:
167	    case Dec{value, rest}:
168	      value
169	
170	def parsed_rest(parsed: Parsed) -> String:
171	  match parsed:
172	    case Dec{value, rest}:
173	      rest
174	
175	def is_accepted(outcome: Parse) -> Bool:
176	  match outcome:
177	    case Rejected{error}:
178	      False{}
179	    case Accepted{parsed}:
180	      True{}