sprintf-like

[thedeemon]

К чему был предыдущий пост. У меня тут написанный на Идрисе кодогенератор, который генерит десятки разных вариаций компенсации движения на С++, т.е. на выходе много текста. Лучше всего для этого дела подошла бы string interpolation, но в Идрисе такого нету и не предвидится. В окамле вон есть модуль Printf, где вызов вроде
Printf.sprintf "%d %s of beer" 99 "bottles"
вернет строчку
"99 bottles of beer"
и компилятор проверит, что число и типы параметров соответствуют формат-строке, это умение встроено в сам компилятор как специальный случай для этого модуля, насколько я помню. Но в Идрисе такого тоже нет, поэтому приходилось просто соединять строчки оператором ++, получалось не слишком удобно. Теперь же вот сделал себе упрощенный аналог sprintf, который просто вставляет строчки в нужные позиции. Вместо
"bigLuma.halveBlockHP(" ++ vec st ++", " ++ block ++ ");"
"PBlock<"++ w++"> "++block++" = halfLuma.makePBlock<"++w++">();"
теперь просто
ins "bigLuma.halveBlockHP($, $);" (vec st) block
ins "PBlock<$> $ = halfLuma.makePBlock<$>();" w block w
Параметры пока только строковые, но зато соответствие их числа формат-строке проверяется статически.

Реализовано так:

numS : String -> Nat
numS = List.length . filter (=='$') . unpack

prnType : Nat -> Type
prnType Z = String
prnType (S k) = String -> prnType k

prn : (n:Nat) -> List String -> String -> prnType n
prn Z [s] acc = acc ++ s
prn (S k) (s::rest) acc = \x => prn k rest (acc ++ s ++ x)

ins : (fmt:String) -> prnType (numS fmt)
ins src = prn (numS src) (Strings.split (=='$') src) ""

Comments

[dmytrish.livejournal.com]

Лучше всего для этого дела подошла бы string interpolation, но в Идрисе такого нету и не предвидится. — а что именно мешает запилить, или это тема не для чайников?

[thedeemon.livejournal.com]

Как я понимаю, это надо или в компилятор поддержку вставлять (а авторам не до того), либо макросы, которых пока тоже нет.