def redirect.dots

emerging-ezhttp@0.21.0.0 · src/redirect.bend:75

import Base

75# a path's segments with dot segments removed, `out` holding those kept so
76# far, last first
77def redirect.dots(ss: List<&2, String>, out: List<&2, String>)
78  -> List<&2, String>:
79  match ss:
80    case []:
81      List.reverse(&2, String, out)
82    case +s <> +t:
83      redirect.dots.one(String.eq(s, "."), String.eq(s, ".."),
84        List.is_empty(&2, String, t), s, out, o => redirect.dots(t, o))