1	import Base
2	
3	type Parse.Cur is Data:
4	  Cur{rest: String, off: Nat}
5	
6	type Parse.Error is Data:
7	  Unexpected{offset: Nat, char: Char}
8	  Eof{offset: Nat}
9	  Overflow{offset: Nat}
10	  Extra{offset: Nat, char: Char}
11	
12	type Parse.St is Data:
13	  StOk{}
14	  StBad{c: Char}
15	  StOv{}
16	
17	type Parse.Dec is Data:
18	  Dec{value: U32, cur: Parse.Cur}
19	
20	def Parse.start(text: String) -> Parse.Cur:
21	  Cur{text, 0n}
22	
23	def Parse.peek.s(s: String) -> Maybe<&2, Char>:
24	  match s:
25	    case SNil{}:
26	      None{}
27	    case SCon{+h, _}:
28	      Some{h}
29	
30	def Parse.peek(cur: Parse.Cur) -> Maybe<&2, Char>:
31	  match cur:
32	    case Cur{rest, _}:
33	      Parse.peek.s(rest)
34	
35	def Parse.expect_char.eq(
36	  t: String, off: Nat, h: Char, eq: Bool
37	) -> Result<&2, &2, Parse.Error, Parse.Cur>:
38	  match eq:
39	    case True{}:
40	      Done{Cur{t, 1n+off}}
41	    case False{}:
42	      Fail{Unexpected{off, h}}
43	
44	def Parse.expect_char.s(
45	  s: String, off: Nat, +want: Char
46	) -> Result<&2, &2, Parse.Error, Parse.Cur>:
47	  match s:
48	    case SNil{}:
49	      Fail{Eof{off}}
50	    case SCon{+h, t}:
51	      Parse.expect_char.eq(t, off, h, Char.is_eq(h, want))
52	
53	def Parse.expect_char(
54	  cur: Parse.Cur, +want: Char
55	) -> Result<&2, &2, Parse.Error, Parse.Cur>:
56	  match cur:
57	    case Cur{rest, off}:
58	      Parse.expect_char.s(rest, off, want)
59	
60	def Parse.expect_literal.go(
61	  s: String, p: String, eq: Bool, h: Char, off: Nat
62	) -> Result<&2, &2, Parse.Error, Parse.Cur>:
63	  match s p eq:
64	    case _ _ False{}:
65	      Fail{Unexpected{off, h}}
66	    case _ SNil{} True{}:
67	      Done{Cur{s, 1n+off}}
68	    case SNil{} SCon{_, _} True{}:
69	      Fail{Eof{1n+off}}
70	    case SCon{+h2, t} SCon{ph, pt} True{}:
71	      Parse.expect_literal.go(t, pt, Char.is_eq(h2, ph), h2, 1n+off)
72	
73	def Parse.expect_literal.start(
74	  s: String, p: String, off: Nat
75	) -> Result<&2, &2, Parse.Error, Parse.Cur>:
76	  match s p:
77	    case _ SNil{}:
78	      Done{Cur{s, off}}
79	    case SNil{} SCon{_, _}:
80	      Fail{Eof{off}}
81	    case SCon{+h, t} SCon{ph, pt}:
82	      Parse.expect_literal.go(t, pt, Char.is_eq(h, ph), h, off)
83	
84	def Parse.expect_literal(
85	  cur: Parse.Cur, pat: String
86	) -> Result<&2, &2, Parse.Error, Parse.Cur>:
87	  match cur:
88	    case Cur{rest, off}:
89	      Parse.expect_literal.start(rest, pat, off)
90	
91	def Parse.ascii_digit.val(
92	  +h: Char, t: String, off: Nat, dig: Bool
93	) -> Result<&2, &2, Parse.Error, Parse.Dec>:
94	  match dig:
95	    case False{}:
96	      Fail{Unexpected{off, h}}
97	    case True{}:
98	      Done{Dec{(Char.to_u32(h) - Char.to_u32('0') : U32), Cur{t, 1n+off}}}
99	
100	def Parse.ascii_digit.s(
101	  s: String, off: Nat
102	) -> Result<&2, &2, Parse.Error, Parse.Dec>:
103	  match s:
104	    case SNil{}:
105	      Fail{Eof{off}}
106	    case SCon{+h, t}:
107	      Parse.ascii_digit.val(h, t, off, Char.is_digit(h))
108	
109	def Parse.ascii_digit(
110	  cur: Parse.Cur
111	) -> Result<&2, &2, Parse.Error, Parse.Dec>:
112	  match cur:
113	    case Cur{rest, off}:
114	      Parse.ascii_digit.s(rest, off)
115	
116	def Parse.acc.ok(+acc: U32, +d: U32, +max: U32) -> Bool:
117	  Nat.is_le(Nat.add(Nat.mul(U32.to_nat(acc), 10n), U32.to_nat(d)), U32.to_nat(max))
118	
119	def Parse.nacc(+acc: U32, +h: Char) -> U32:
120	  U32.add(U32.mul(acc, 10), (Char.to_u32(h) - Char.to_u32('0') : U32))
121	
122	def Parse.st.ov(+acc: U32, +d: U32, +max: U32, ok: Bool) -> Parse.St:
123	  match ok:
124	    case False{}:
125	      StOv{}
126	    case True{}:
127	      StOk{}
128	
129	def Parse.st.of2(+acc: U32, +h: Char, +max: U32, dig: Bool) -> Parse.St:
130	  match dig:
131	    case False{}:
132	      StBad{h}
133	    case True{}:
134	      Parse.st.ov(
135	        acc, (Char.to_u32(h) - Char.to_u32('0') : U32), max,
136	        Parse.acc.ok(acc, (Char.to_u32(h) - Char.to_u32('0') : U32), max)
137	      )
138	
139	def Parse.st.of(+acc: U32, +h: Char, +max: U32) -> Parse.St:
140	  Parse.st.of2(acc, h, max, Char.is_digit(h))
141	
142	def Parse.read_fixed.go(
143	  s: String, n: Nat, +acc: U32, off: Nat, st: Parse.St, +max: U32
144	) -> Result<&2, &2, Parse.Error, Parse.Dec>:
145	  match s n st:
146	    case _ _ StBad{c}:
147	      Fail{Unexpected{off, c}}
148	    case _ _ StOv{}:
149	      Fail{Overflow{off}}
150	    case _ 0n StOk{}:
151	      Done{Dec{acc, Cur{s, off}}}
152	    case SNil{} 1n++p StOk{}:
153	      Fail{Eof{off}}
154	    case SCon{+h, t} 1n++p StOk{}:
155	      Parse.read_fixed.go(
156	        t, p, Parse.nacc(acc, h), 1n+off, Parse.st.of(acc, h, max), max
157	      )
158	
159	def Parse.read_fixed_decimal(
160	  cur: Parse.Cur, count: Nat, max: U32
161	) -> Result<&2, &2, Parse.Error, Parse.Dec>:
162	  match cur:
163	    case Cur{rest, off}:
164	      Parse.read_fixed.go(rest, count, 0, off, StOk{}, max)
165	
166	def Parse.finish.s(
167	  s: String, off: Nat
168	) -> Result<&2, &2, Parse.Error, Unit>:
169	  match s:
170	    case SNil{}:
171	      Done{Unit{}}
172	    case SCon{h, _}:
173	      Fail{Extra{off, h}}
174	
175	def Parse.finish(
176	  cur: Parse.Cur
177	) -> Result<&2, &2, Parse.Error, Unit>:
178	  match cur:
179	    case Cur{rest, off}:
180	      Parse.finish.s(rest, off)