1	import Base
2	
3	# Shared boundary for native distance executables. Keep validation ahead of
4	# distance evaluation, including empty-input shortcuts in either algorithm.
5	type InputStatus is Data:
6	  Supported{}
7	  NonAscii{}
8	  TooLong{}
9	
10	def max_sequence_length() -> Nat:
11	  4096n
12	
13	def scan_ascii(rest: Unit -> InputStatus, ascii: Bool) -> InputStatus:
14	  match ascii:
15	    case True{}:
16	      rest(Unit{})
17	    case False{}:
18	      NonAscii{}
19	
20	# Inspect at most limit + 1 characters, without an unbounded length pass.
21	# Match the empty string first so a sequence exactly at the limit is valid.
22	def scan(sequence: String, remaining: Nat) -> InputStatus:
23	  match sequence remaining:
24	    case SNil{} _:
25	      Supported{}
26	    case SCon{h, t} 0n:
27	      TooLong{}
28	    case SCon{h, t} 1n+p:
29	      +code = Char.to_u32(h)
30	      scan_ascii(_ => scan(t, p),
31	        Bool.and(U32.is_gt(code, 0), U32.is_le(code, 127)))
32	
33	def combine(query: InputStatus, target: InputStatus) -> InputStatus:
34	  match query:
35	    case Supported{}:
36	      target
37	    case NonAscii{}:
38	      NonAscii{}
39	    case TooLong{}:
40	      TooLong{}
41	
42	def validate(query: String, target: String) -> InputStatus:
43	  q t = scan(query, max_sequence_length()) scan(target, max_sequence_length())
44	  combine(q, t)
45	
46	def respond(~distance: String -> String -> Nat, query: String, target: String,
47	            status: InputStatus) -> IO(Unit):
48	  match status:
49	    case Supported{}:
50	      IO.print(Nat.show(distance(query, target)))
51	    case NonAscii{}:
52	      IO.die(Unit, 2, "Sequences must contain only non-NUL ASCII characters (U+0001..U+007F)")
53	    case TooLong{}:
54	      IO.die(Unit, 2, "Sequence length exceeds maximum of " ++
55	        Nat.show(max_sequence_length()) ++ " ASCII characters per sequence")
56	
57	def run(~distance: String -> String -> Nat, args: List<String>) -> IO(Unit):
58	  match args:
59	    # IO.args includes argv[0]; the native runtime consumes flags before --.
60	    case Con{_, Con{+query, Con{+target, Nil{}}}}:
61	      respond(~distance, query, target, validate(query, target))
62	    case _:
63	      IO.die(Unit, 2, "Expected QUERY TARGET")