sprintf-like
Nov. 28th, 2013 04:37 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
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
Параметры пока только строковые, но зато соответствие их числа формат-строке проверяется статически.
Реализовано так:
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) ""
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
no subject
Date: 2013-11-28 01:05 pm (UTC)Надо же; я думал, что type-safe printf это poster child для зависимых типов. Ещё в статье про Cayenne было.
no subject
Date: 2013-11-28 03:17 pm (UTC)no subject
Date: 2013-11-28 01:28 pm (UTC)no subject
Date: 2013-11-28 03:11 pm (UTC)no subject
Date: 2013-11-28 03:00 pm (UTC)no subject
Date: 2013-11-28 03:09 pm (UTC)А вот сам символ $ в генерируемом С++ коде никогда не встречается, так что эскейпинг в моем случае не понадобился.
no subject
Date: 2013-11-28 04:28 pm (UTC)no subject
Date: 2013-11-28 05:10 pm (UTC)Зато сэкономил 8 месяцев отладки и 12487 строк тестов, которые понадобились бы без статической типизации.
no subject
Date: 2013-11-28 05:12 pm (UTC)no subject
Date: 2013-11-28 05:38 pm (UTC)no subject
Date: 2013-11-28 06:17 pm (UTC)no subject
Date: 2013-11-28 07:16 pm (UTC)no subject
Date: 2013-11-28 11:35 pm (UTC)no subject
Date: 2013-11-29 06:09 am (UTC)no subject
Date: 2013-11-28 05:53 pm (UTC)Впрочем, альтернативный вариант - скобочки.