1	# remove/plan: `ez remove` as a pure planner. It asks nothing: its World is
2	# the name asked for, the ledger's text (None when there is no ez.toml) and
3	# `.gitignore`'s text ("" when there is none), and its planner is one function
4	# from that World to a Plan. The interpreter (remove/run.bend) reads the two
5	# files, calls it, and runs what it returns.
6	#
7	# The plan, when the ledger reads and names the dependency: ez.toml written
8	# with the dependency dropped (`Rend.remove`); `.gitignore` written with the
9	# allowlist `I.sync` derives from what is left, when that changes it; and
10	# the committed tree `.ez/lib/<hash>` of a dependency that was vendored
11	# removed, unless a dependency that is left still names that hash. Anything
12	# else is a refusal, with no effect at all: no ledger, one that does not
13	# parse, or a name the ledger does not have, which `cargo remove` refuses too.
14	#
15	# The Effect, Plan and Outcome types are the lock's (lock/plan.bend), which
16	# the add design moves to a shared plan/plan.bend later; see "Update (A1,
17	# A4)" in docs/rfc/ez-add-planner.md.
18	import Base
19	import ../lock/plan.bend as P
20	import ../ledger/manifest.bend as M
21	import ../ledger/render.bend as Rend
22	import ../ledger/ignore.bend as I
23	
24	# what `ez remove` reads: the name it was given, the ledger's text or None,
25	# and the ignore file's text, "" when there is none
26	type World is Data:
27	  World{name: String, ledger: Maybe<&2, String>, ignore: String}
28	
29	# the ledger's path, which is fixed
30	def toml() -> String:
31	  "ez.toml"
32	
33	# the ignore file's path, which is fixed
34	def ignore.file() -> String:
35	  ".gitignore"
36	
37	# the ledger as read: what the file says, or, with no file, a read that did
38	# not parse and says why. A missing ledger is not an empty one to write back.
39	def read.of(got: Maybe<&2, String>) -> M.Read:
40	  match got:
41	    case None{}:
42	      M.Bad{"no " ++ toml() ++ " here; ez remove works on a project's " ++
43	        "ledger, and ez init makes one"}
44	    case Some{text}:
45	      M.parse(text)
46	
47	# the dependencies of a ledger that was read
48	def deps.of(manifest: M.Manifest) -> List<&2, M.Dep>:
49	  M.Manifest{_n, _e, _b, _h, _pa, _pv, ds, _ts} = manifest
50	  ds
51	
52	# the rest of a scan only when this one was not it
53	def any.step(hit: Bool, rest: Unit -> Bool) -> Bool:
54	  match hit:
55	    case True{}:
56	      True{}
57	    case False{}:
58	      rest(Unit{})
59	
60	# whether a dependency has this name
61	def named(ds: List<&2, M.Dep>, +name: String) -> Bool:
62	  match ds:
63	    case []:
64	      False{}
65	    case +h <> t:
66	      any.step(String.eq(M.dep.name(h), name), _u => named(t, name))
67	
68	# whether a dependency names this hash
69	def holds(ds: List<&2, M.Dep>, +hash: String) -> Bool:
70	  match ds:
71	    case []:
72	      False{}
73	    case +h <> t:
74	      any.step(String.eq(M.dep.hash(h), hash), _u => holds(t, hash))
75	
76	# whether a char may stand in a hash that names a directory under `.ez/lib`
77	def char.ok(+ch: Char) -> Bool:
78	  Bool.not(Bool.or(Char.is_eq(ch, '/'), Char.is_eq(ch, '\\')))
79	
80	# whether every char of a text may
81	def chars.ok(text: String) -> Bool:
82	  match text:
83	    case SNil{}:
84	      True{}
85	    case SCon{+h, t}:
86	      +rest = chars.ok(t)
87	      Bool.and(char.ok(h), rest)
88	
89	# a hash `rm -rf .ez/lib/<hash>` removes one tree for: a `0x` name with no
90	# path separator in it. `M.parse` does not check a hash's shape, and a ledger
91	# is text a person edits, so this is checked before a tree is removed.
92	def safe(+hash: String) -> Bool:
93	  Bool.and(String.starts_with(hash, "0x"), chars.ok(hash))
94	
95	# a vendored hash, removed ahead of the rest when it is safe to remove and no
96	# dependency that is left names it
97	def gone.hash(keep: Bool, +hash: String, rest: List<&2, String>) -> List<&2, String>:
98	  match keep:
99	    case True{}:
100	      rest
101	    case False{}:
102	      hash <> rest
103	
104	# a dependency's committed tree, when it is the one removed and is vendored
105	def gone.put(hit: Bool, +hash: String, +left: List<&2, M.Dep>, rest: List<&2, String>) -> List<&2, String>:
106	  match hit:
107	    case True{}:
108	      gone.hash(Bool.or(holds(left, hash), Bool.not(safe(hash))), hash, rest)
109	    case False{}:
110	      rest
111	
112	# the committed trees removing `name` leaves no dependency to name: the hash
113	# of each vendored dependency by that name that none in `left` names
114	def gone(ds: List<&2, M.Dep>, +name: String, +left: List<&2, M.Dep>) -> List<&2, String>:
115	  match ds:
116	    case []:
117	      []
118	    case +h <> t:
119	      gone.put(Bool.and(String.eq(M.dep.name(h), name),
120	        M.source.vendor(M.source.dep(h))), M.dep.hash(h), left, gone(t, name, left))
121	
122	# `.gitignore` written ahead of the rest when the allowlist changes it
123	def ignore.put(same: Bool, +next: String, rest: List<&2, P.Effect>) -> List<&2, P.Effect>:
124	  match same:
125	    case True{}:
126	      rest
127	    case False{}:
128	      P.Write{ignore.file(), next} <> rest
129	
130	# what `ez remove` does to a ledger that names the dependency: the ledger
131	# written without it, the allowlist derived from what is left, and each
132	# committed tree it leaves unnamed removed
133	def edits(+led: M.Manifest, +name: String, +ignore: String) -> List<&2, P.Effect>:
134	  +left = deps.of(Rend.remove(led, name))
135	  +next = I.sync(left, ignore)
136	  P.Write{toml(), Rend.show(Rend.remove(led, name))} <>
137	    ignore.put(String.eq(next, ignore), next,
138	      P.drops.of(gone(deps.of(led), name, left), []))
139	
140	# the refusal for a name the ledger does not have
141	def absent(+name: String) -> String:
142	  "ez: " ++ toml() ++ " has no dependency named " ++ name
143	
144	# the refusal for a ledger that names the dependency but, with it dropped,
145	# cannot be written so that it reads back (EZ-LED-4), or for a name it does
146	# not have
147	def refusal(named: Bool, +name: String) -> String:
148	  Bool.pick(String, named, Rend.unrenderable(), absent(name))
149	
150	# the plan for a ledger that read: the edits when it names the dependency and
151	# the ledger left can be written, a refusal when not
152	def plan.has(has: Bool, +led: M.Manifest, +name: String, +ignore: String) -> P.Plan:
153	  match has:
154	    case True{}:
155	      P.Plan{edits(led, name, ignore), P.Success{}}
156	    case False{}:
157	      P.Plan{[], P.Refused{refusal(named(deps.of(led), name), name)}}
158	
159	# the plan for the ledger as read. One that did not read, or is not there,
160	# is refused before anything else, and its reason is the one every command
161	# that edits a ledger gives.
162	def plan.read(led: M.Read, +name: String, +ignore: String) -> P.Plan:
163	  match led:
164	    case M.Bad{why}:
165	      P.Plan{[], P.Refused{"ez: " ++ M.show(M.Bad{why})}}
166	    case M.Good{+m}:
167	      plan.has(Bool.and(named(deps.of(m), name), Rend.renderable(Rend.remove(m, name))),
168	        m, name, ignore)
169	
170	# `ez remove` over a World
171	def plan(world: World) -> P.Plan:
172	  World{+n, l, +ig} = world
173	  plan.read(read.of(l), n, ig)
174	
175	# whether a plan ends in a refusal
176	def refuses.plan(pl: P.Plan) -> Bool:
177	  P.Plan{_es, outcome} = pl
178	  match outcome:
179	    case P.Success{}:
180	      False{}
181	    case P.Refused{_why}:
182	      True{}
183	
184	# whether `ez remove` refuses on a World
185	def refuses(world: World) -> Bool:
186	  refuses.plan(plan(world))
187	
188	# what a path holds once a plan has run, when it held `was` before
189	def after(wrote: P.Wrote, +was: String) -> String:
190	  match wrote:
191	    case P.Kept{}:
192	      was
193	    case P.Put{text}:
194	      text