1	# src/argv: what `run`, `exec` and `start` do with an argv. `run.plan` decides
2	# whether it can reach its program whole, and hands the effect `wire(argv)`
3	# only then; `run.with` and `start.with` perform the plan with an effect given
4	# as a parameter, so a refused plan can be seen to call none. `cmd` is the
5	# newline wire ez's `pass` effect reads.
6	import Base
7	
8	# the arguments joined on newlines, which is the wire ez's `pass` effect
9	# reads. snap's own effects are handed `wire` and `par.plan`, since an
10	# argument may hold a newline.
11	def cmd(argv: List<&2, String>) -> String:
12	  String.join(argv, "\n")
13	
14	# the arguments joined on newlines; the same as `cmd`
15	def line(argv: List<&2, String>) -> String:
16	  cmd(argv)
17	
18	# whether a string holds no copy of a char
19	def free_of(text: String, +sep: Char) -> Bool:
20	  match text:
21	    case SNil{}:
22	      True{}
23	    case SCon{ch, tail}:
24	      rest = free_of(tail, sep)
25	      Bool.and(Bool.not(Char.is_eq(ch, sep)), rest)
26	
27	# whether no string of a list holds a copy of a char
28	def free_of.all(ps: List<&2, String>, +sep: Char) -> Bool:
29	  match ps:
30	    case []:
31	      True{}
32	    case pc <> pt:
33	      rest = free_of.all(pt, sep)
34	      Bool.and(free_of(pc, sep), rest)
35	
36	# whether an argv can reach its program whole: it names a program, and no
37	# argument holds NUL, which separates them on the wire and which no program
38	# could be handed inside an argument anyway
39	def accepts(argv: List<&2, String>) -> Bool:
40	  match argv:
41	    case []:
42	      False{}
43	    case +prog <> +args:
44	      Bool.and(Bool.not(String.is_empty(prog)), free_of.all(prog <> args, '\0'))
45	
46	# the arguments as the effects want them: joined on NUL, the one char no
47	# argument can hold, so each is split back out whole
48	def wire(argv: List<&2, String>) -> String:
49	  String.join(argv, "\0")
50	
51	# what a call does with its argv: refuse it, or hand the effect this wire
52	type Step is Data:
53	  Refused{}
54	  Run{wire: String}
55	
56	# an argv accepted is run; any other is refused
57	def run.plan.of(ok: Bool, argv: List<&2, String>) -> Step:
58	  match ok:
59	    case True{}:
60	      Run{wire(argv)}
61	    case False{}:
62	      Refused{}
63	
64	# what `run`, `exec` and `start` do with an argv. It decides everything: the
65	# effect is called only with the wire of an argv this accepts.
66	def run.plan(+argv: List<&2, String>) -> Step:
67	  run.plan.of(accepts(argv), argv)
68	
69	# a step performed by an effect that waits: a refused argv answers as a
70	# program that could not be started, and the effect is never called
71	def run.with(eff: String -> IO(String), step: Step) -> IO(String):
72	  match step:
73	    case Refused{}:
74	      IO.pure(String, "127\n")
75	    case Run{w}:
76	      eff(w)
77	
78	# a step performed by an effect that does not wait: a refused argv answers
79	# as a program that could not be started, and the effect is never called
80	def start.with(eff: String -> IO(String), step: Step) -> IO(String):
81	  match step:
82	    case Refused{}:
83	      IO.pure(String, "0")
84	    case Run{w}:
85	      eff(w)