1	# pkg/path: the path arithmetic the import walk needs, lexical only. Base has
2	# no readdir and no realpath, and a module's name in a package is the path it
3	# was reached through, so `.` and `..` are resolved by text rather than by
4	# asking the file system.
5	import Base
6	
7	# where a normalisation has got to: `abs` is true for a path that began at the
8	# root, `out` the components kept so far, reversed
9	type Walk is Data:
10	  Walk{abs: Bool, out: List<&2, String>}
11	
12	# what one component of a path turned out to be
13	type Comp is Data:
14	  CSkip{}
15	  CUp{}
16	  CName{s: String}
17	
18	# a component classified. `+c` because it is both asked about and kept.
19	def comp_of(+part: String) -> Comp:
20	  Bool.pick(Comp, Bool.or(String.is_empty(part), String.eq(part, ".")), CSkip{},
21	    Bool.pick(Comp, String.eq(part, ".."), CUp{}, CName{part}))
22	
23	# a climb with nothing left to climb off: at the root it goes nowhere, and in a
24	# relative path it is kept, since the package may still be re-rooted under it
25	def up.root(abs: Bool) -> List<&2, String>:
26	  match abs:
27	    case True{}:
28	      []
29	    case False{}:
30	      [".."]
31	
32	# a climb past a component that is itself a climb keeps both
33	def up.back(same: Bool, head: String, rest: List<&2, String>) -> List<&2, String>:
34	  match same:
35	    case True{}:
36	      ".." <> (head <> rest)
37	    case False{}:
38	      rest
39	
40	# a climb against what has been kept: it cancels the last real component
41	def up.go(+head: String, rest: List<&2, String>) -> List<&2, String>:
42	  up.back(String.eq(head, ".."), head, rest)
43	
44	# a climb against what has been kept
45	def up(abs: Bool, out: List<&2, String>) -> List<&2, String>:
46	  match out:
47	    case []:
48	      up.root(abs)
49	    case h <> t:
50	      up.go(h, t)
51	
52	# a climb, with the root flag carried through
53	def up.step(+abs: Bool, out: List<&2, String>) -> Walk:
54	  Walk{abs, up(abs, out)}
55	
56	# the state once a component has been classified
57	def norm.go(st: Walk, comp: Comp) -> Walk:
58	  Walk{abs, out} = st
59	  match comp:
60	    case CSkip{}:
61	      Walk{abs, out}
62	    case CUp{}:
63	      up.step(abs, out)
64	    case CName{s}:
65	      Walk{abs, s <> out}
66	
67	# one component against the state
68	def norm.step(st: Walk, part: String) -> Walk:
69	  norm.go(st, comp_of(part))
70	
71	# a relative path with nothing left in it is the current directory
72	def norm.rel(+body: String) -> String:
73	  Bool.pick(String, String.is_empty(body), ".", body)
74	
75	# the components put back together, under the root or not
76	def norm.text(abs: Bool, body: String) -> String:
77	  match abs:
78	    case True{}:
79	      "/" ++ body
80	    case False{}:
81	      norm.rel(body)
82	
83	# the components a normalisation kept, in order
84	def norm.fin(st: Walk) -> String:
85	  Walk{abs, out} = st
86	  norm.text(abs, String.join(List.reverse(&2, String, out), "/"))
87	
88	# the walk one component at a time. Base's `List.foldl` applies an erased
89	# function parameter, which Bend's termination check cannot see through, so
90	# every def reaching it is reported as relying on unsafe code; a walk written
91	# out is structural and costs nothing.
92	def norm.walk(cs: List<&2, String>, st: Walk) -> Walk:
93	  match cs:
94	    case []:
95	      st
96	    case h <> t:
97	      norm.walk(t, norm.step(st, h))
98	
99	# a path with `.` and an inner `..` resolved by text. A leading `..` survives,
100	# because a module reached through one re-roots the package rather than
101	# escaping it.
102	def norm(+path: String) -> String:
103	  norm.fin(norm.walk(String.split(path, '/'), Walk{String.starts_with(path, "/"), []}))
104	
105	# the component carried so far, kept when nothing follows it. The list is the
106	# first argument because that is the one the walk shrinks.
107	def base.go(ps: List<&2, String>, +last: String) -> String:
108	  match ps:
109	    case []:
110	      last
111	    case +h2 <> t:
112	      base.go(t, h2)
113	
114	# the last component of a path
115	def base.last(ps: List<&2, String>) -> String:
116	  match ps:
117	    case []:
118	      ""
119	    case +h <> t:
120	      base.go(t, h)
121	
122	# the last component of a path
123	def base(path: String) -> String:
124	  base.last(String.split(path, '/'))
125	
126	# the path with its last component climbed back off
127	def dir(+path: String) -> String:
128	  norm(path ++ "/..")
129	
130	# the path before it is normalised: the second alone when there is no
131	# directory to take it relative to, the two spliced otherwise. Split out so
132	# that `norm` runs once. Under a `Bool.pick` both arms were built, so every
133	# join paid two full component walks and one concatenation it threw away.
134	def join.at(bare: Bool, left: String, right: String) -> String:
135	  match bare:
136	    case True{}:
137	      right
138	    case False{}:
139	      left ++ "/" ++ right
140	
141	# a path taken relative to a directory. An empty directory means the path is
142	# already where it should be, and never that it starts at the root.
143	def join(+left: String, +right: String) -> String:
144	  norm(join.at(String.is_empty(left), left, right))
145	
146	# the last `n` components of a path
147	def tail(path: String, count: Nat) -> String:
148	  String.join(List.reverse(&2, String,
149	    List.take(&2, String, List.reverse(&2, String, String.split(path, '/')), count)), "/")
150	
151	# whether a component is a climb
152	def up.is(part: String) -> Bool:
153	  String.eq(part, "..")
154	
155	# the climbs among components counted one at a time. Base's `List.filter`
156	# applies an erased function parameter, so it falls outside the termination
157	# check; this count is structural.
158	def ups.go(ps: List<&2, String>) -> Nat:
159	  match ps:
160	    case []:
161	      0n
162	    case +h <> t:
163	      Nat.add(Bool.pick(Nat, up.is(h), 1n, 0n), ups.go(t))
164	
165	# how many components of a path are climbs
166	def ups(path: String) -> Nat:
167	  ups.go(String.split(path, '/'))
168	
169	# a module path without its `.bend`, which is how bend names the module
170	def unbend(+path: String) -> String:
171	  Bool.pick(String, String.ends_with(path, ".bend"),
172	    String.take(path, Nat.sub(String.length(path), 5n)), path)
173	
174	# the path with `n` of its components climbed back off, which is where a
175	# package re-roots when a module of it was reached through that many `..`
176	def climb(count: Nat, path: String) -> String:
177	  match count:
178	    case 0n:
179	      norm(path)
180	    case 1n+q:
181	      climb(q, dir(path))
182	
183	# an absolute path, or a `git@` URL, as it is, or a relative path taken from
184	# `here`
185	def anchor.path(kept: Bool, +here: String, +path: String) -> String:
186	  match kept:
187	    case True{}:
188	      path
189	    case False{}:
190	      join(here, path)
191	
192	# a URL as it is, or a path
193	def anchor.at(url: Bool, +here: String, +path: String) -> String:
194	  match url:
195	    case True{}:
196	      path
197	    case False{}:
198	      anchor.path(Bool.or(String.starts_with(path, "/"),
199	        String.starts_with(path, "git@")), here, path)
200	
201	# a source as the directory `here` reads it. The ledger keeps a local path
202	# relative to the project, the way it was given, and git reads a relative path
203	# from somewhere else, so every git command is handed this instead. A URL is
204	# the same wherever it is read from.
205	def anchor(+here: String, +path: String) -> String:
206	  anchor.at(String.contains(path, "://"), here, path)