1 # ezsys/src/text: text templates. A marker is an open delimiter, a key and a 2 # close delimiter, `{{name}}` for `text.fill`. The scan reads the template 3 # once, left to right, one character a step: at an open delimiter it starts a 4 # key, and the key runs to the first close delimiter after it. A known key is 5 # replaced by its value, written as it is (a value is never scanned again); 6 # an unknown key, or a marker with no close, is left as written. Markers do 7 # not nest. An empty open or close delimiter marks nothing. 8 import Base 9 10 # where the scan is: in plain text, passing over the rest of an open 11 # delimiter, inside a key, or passing over the rest of a close delimiter 12 type Mode is Data: 13 Plain{} 14 Opening{left: Nat} 15 InKey{key: String} 16 Closing{left: Nat} 17 18 # the keys and values, reusable 19 def text.Pairs() -> Data: 20 List<&2, Sigma<&2, &2, String, _ => String>> 21 22 # a caller's pairs as reusable ones, in their order 23 def text.own(xs: List<(String & String)>) -> text.Pairs(): 24 match xs: 25 case Nil{}: 26 Nil{} 27 case Con{(+key, +value), rest}: 28 Con{(key, value), text.own(rest)} 29 30 # this pair's value when its key is the one asked for, else the rest's 31 def text.value.pick( 32 hit: Bool, 33 value: String, 34 rest: Unit -> Maybe<&2, String> 35 ) -> Maybe<&2, String>: 36 match hit: 37 case True{}: 38 Some{value} 39 case False{}: 40 rest(Unit{}) 41 42 # the value a key names: the first pair with that key 43 def text.value(pairs: text.Pairs(), +key: String) -> Maybe<&2, String>: 44 match pairs: 45 case Nil{}: 46 None{} 47 case Con{(name, value), rest}: 48 text.value.pick(String.eq(name, key), value, 49 _u => text.value(rest, key)) 50 51 # the characters of a delimiter after its first 52 def text.tail(delim: String) -> Nat: 53 match delim: 54 case SNil{}: 55 0n 56 case SCon{_hd, tl}: 57 String.length(tl) 58 59 # the mode after an open delimiter's first character, with `left` to pass 60 def text.enter(left: Nat) -> Mode: 61 match left: 62 case 0n: 63 InKey{""} 64 case 1n+more: 65 Opening{more} 66 67 # the mode after a close delimiter's first character, with `left` to pass 68 def text.leave(left: Nat) -> Mode: 69 match left: 70 case 0n: 71 Plain{} 72 case 1n+more: 73 Closing{more} 74 75 # what a finished marker becomes: its value, or the marker as written 76 def text.put( 77 +open: String, 78 +close: String, 79 key: String, 80 got: Maybe<&2, String> 81 ) -> String: 82 match got: 83 case None{}: 84 open ++ (key ++ close) 85 case Some{value}: 86 value 87 88 # a character in plain text: the start of a marker, or itself 89 def text.plain(at: Bool, hd: Char, +open: String) -> String & Mode: 90 match at: 91 case False{}: 92 (SCon{hd, SNil{}}, Plain{}) 93 case True{}: 94 ("", text.enter(text.tail(open))) 95 96 # a character in a key: the start of the close delimiter, or part of the key 97 def text.shut( 98 at: Bool, 99 hd: Char, 100 +key: String, 101 +open: String, 102 +close: String, 103 +pairs: text.Pairs() 104 ) -> String & Mode: 105 match at: 106 case False{}: 107 ("", InKey{key ++ SCon{hd, SNil{}}}) 108 case True{}: 109 (text.put(open, close, key, text.value(pairs, key)), 110 text.leave(text.tail(close))) 111 112 # one character: what it writes and the mode after it 113 def text.step( 114 +hd: Char, 115 +tl: String, 116 mode: Mode, 117 +open: String, 118 +close: String, 119 +pairs: text.Pairs() 120 ) -> String & Mode: 121 match mode: 122 case Plain{}: 123 text.plain(String.starts_with(SCon{hd, tl}, open), hd, open) 124 case Opening{left}: 125 ("", text.enter(left)) 126 case InKey{key}: 127 text.shut(String.starts_with(SCon{hd, tl}, close), hd, key, open, close, 128 pairs) 129 case Closing{left}: 130 ("", text.leave(left)) 131 132 # the end of the template: an unclosed marker is written as it was 133 def text.end(mode: Mode, +open: String) -> String: 134 match mode: 135 case Plain{}: 136 "" 137 case Opening{_left}: 138 "" 139 case InKey{key}: 140 open ++ key 141 case Closing{_left}: 142 "" 143 144 # write a step's text, then scan on in the mode after it 145 def text.join(pair: String & Mode, rest: Mode -> String) -> String: 146 (out, next) = pair 147 out ++ rest(next) 148 149 # the scan 150 def text.go( 151 tpl: String, 152 mode: Mode, 153 +open: String, 154 +close: String, 155 +pairs: text.Pairs() 156 ) -> String: 157 match tpl: 158 case SNil{}: 159 text.end(mode, open) 160 case SCon{+hd, +tl}: 161 text.join(text.step(hd, tl, mode, open, close, pairs), 162 next => text.go(tl, next, open, close, pairs)) 163 164 # true when here is true, else what the rest says 165 def text.any(here: Bool, rest: Unit -> Bool) -> Bool: 166 match here: 167 case True{}: 168 True{} 169 case False{}: 170 rest(Unit{}) 171 172 # false when here is false, else what the rest says 173 def text.all(here: Bool, rest: Unit -> Bool) -> Bool: 174 match here: 175 case False{}: 176 False{} 177 case True{}: 178 rest(Unit{}) 179 180 # whether an open delimiter starts anywhere in the text 181 def text.marked(+open: String, tpl: String) -> Bool: 182 match tpl: 183 case SNil{}: 184 False{} 185 case SCon{+hd, +tl}: 186 text.any(String.starts_with(SCon{hd, tl}, open), 187 _u => text.marked(open, tl)) 188 189 # whether no close delimiter starts at any character of key, in key ++ after 190 def text.free(+close: String, key: String, +after: String) -> Bool: 191 match key: 192 case SNil{}: 193 True{} 194 case SCon{+hd, +tl}: 195 text.all(Bool.not(String.starts_with(SCon{hd, tl ++ after}, close)), 196 _u => text.free(close, tl, after)) 197 198 # every marker between open and close replaced by its key's value 199 def text.fill_with( 200 open: String, 201 close: String, 202 tpl: String, 203 pairs: text.Pairs() 204 ) -> String: 205 match open close: 206 case SNil{} _: 207 tpl 208 case SCon{_oh, _ot} SNil{}: 209 tpl 210 case SCon{oh, ot} SCon{ch, ct}: 211 text.go(tpl, Plain{}, SCon{oh, ot}, SCon{ch, ct}, pairs) 212 213 # every `{{key}}` marker replaced by its key's value 214 def text.fill(tpl: String, pairs: text.Pairs()) -> String: 215 text.fill_with("{{", "}}", tpl, pairs)