![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
sprintf-like
К чему был предыдущий пост. У меня тут написанный на Идрисе кодогенератор, который генерит десятки разных вариаций компенсации движения на С++, т.е. на выходе много текста. Лучше всего для этого дела подошла бы 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
Параметры пока только строковые, но зато соответствие их числа формат-строке проверяется статически.
Реализовано так:
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) ""
no subject
no subject
no subject
no subject