Objective Caml - Суббота, 30 марта 2013

Objective Caml

ocaml@conference.jabber.ru

Суббота, 30 марта 2013< ^ >

Конфигурация комнаты

Участники комнаты

GMT+4
[00:09:45] ermine вышел(а) из комнаты
[00:57:54] Kakadu вышел(а) из комнаты
[02:39:57] strobegen вышел(а) из комнаты
[06:20:41] komar вышел(а) из комнаты: Replaced by new connection
[06:20:41] komar вошёл(а) в комнату
[07:54:05] zinid вошёл(а) в комнату
[08:50:04] strobegen вошёл(а) в комнату
[10:02:29] Kakadu вошёл(а) в комнату
[10:49:57] ermine вошёл(а) в комнату
[12:05:22] f[x] вошёл(а) в комнату
[12:23:21] <ermine> gds: насчет коммутативности сложения - нашла вот это http://staff.aist.go.jp/reynald.affeldt/types02/lundi.html
[12:28:20] <aleksey> ermine: если искать примеры, то проще в исходники библиотеки coq глянуть, там все эти теоремы арифметики есть
[12:29:46] <ermine> aleksey: и кого грепать?
[12:31:58] <aleksey> ermine: в данном случае Plus.v
[12:34:50] <ermine> aleksey: а как там зовеца эта теорема?
[12:38:20] <ermine> aleksey: поискала финдом plus.v в исходниках коки - не нашелся
[12:38:47] <ermine> проще уж гуглить и находить всякую лабуду и читать, читать, читать до посинения
[12:38:55] <aleksey> Plus.v
[12:39:20] <ermine> хотя вон в той страничке говорится что надо сначала доказать plus n 0, я это вчера своим мозгом уже осилила
[12:39:45] <ermine> ага, есть
[13:04:12] Typhon вошёл(а) в комнату
[13:13:13] f[x] вышел(а) из комнаты
[13:52:42] Typhon вышел(а) из комнаты
[13:53:22] Typhon вошёл(а) в комнату
[14:02:34] ermine получила такой же затык в следующем упражнении coq: double n = n+n, где double - функция дублирования типа fixpoint double n = s (s (double n))
[14:02:50] <ermine> видимо пока не постигла дзена
[14:08:22] Typhon вышел(а) из комнаты
[14:21:23] Typhon вошёл(а) в комнату
[15:10:00] f[x] вошёл(а) в комнату
[15:17:05] <gds> ermine: так с коммутативностью плюса -- что непонятно в моём доказательстве?
[15:54:51] <gds> ermine: вообще, для доказательств вещей про плюс нужно учитывать, что он рекурсивен по первому аргументу, то есть, будет разворачиваться и упрощаться тогда, когда известна его структура.  А про double -- опять же, самые очевидные способы применил, http://paste.in.ua/8156/
[15:55:20] <gds> ("его структура" -- структура первого аргумента.  Например, является ли он O или S n')
[16:02:16] <gds> ermine: и вот, через rewrite plus_comm я преобразовал S (n' + S n') в S (S n' + n'), то есть, структура первого аргумента стала известна, и посредством simpl всё это упростилось до S (S (n' + n')).
[16:10:05] <ermine> gds: у меня пока сложности в том, что если auto осиливает остаток доказательства, то я вручную не могу подобрать сочетание induction/destruct/rewrite для ублажения выражений типа    S (S (S (S n' + 1))) = S (S (S (S (S n'))))
[16:11:02] <ermine> и гипотезы в это не лезут из-за лишних S в ненужных местах
[16:11:07] <aleksey> injection
[16:11:49] <gds> конкретно это выражение -- заведи себе лемму n = m -> S n = S m, затем "progress apply имялеммы", по крайней мере лишние S уберутся.  Дальше -- зависит от дальнейших проблем.
[16:13:58] <ermine> apply еще не проходили (хотя я про нее зна)
[16:14:19] <ermine> всё что проходили - это деструкт, индукция и реврайт :)
[16:14:35] <ermine> вот такая вот неленивая аскетичность
[16:14:54] <ermine> даже elim не проходили еще
[16:15:13] <aleksey> ну для того что gds описал этого хватит
[16:16:30] <gds> и это выражение через destruct не имеет смысла мучить, так как destruct -- он для [ко]индуктивных типов данных и для гипотез.  Через induction -- ну, если поможет induction n', то почему бы и нет, но конкретно тут -- навряд ли.  Через rewrite -- разве что переписать какие-то куски из выражения, чтобы довести до одинакового вида левую и правую часть, чтобы потом reflexivity.
[16:27:12] <Kakadu> Так-с. Я не могу по-простому сохранить в с++ном объекте значение типа value потому что данные в памяти могут подвинуться мусорщиком, а запретить подвижение мусорщиком нельзя. Следовательно, надо генерит хорошее имя и делать Callback.register. Я ничего не пропустил?
[16:30:27] <f[x]> пропустил
[16:30:35] <f[x]> gc roots
[16:30:46] <f[x]> caml_register_global_root и caml_register_generational_root
[16:30:46] <gds> Kakadu: зарегистрируй как global root.
[16:30:53] <Kakadu> не поможет же
[16:31:25] <f[x]> и число рутов лучше свести к минимуму
[16:31:34] <Kakadu> "...just before or just after a valid value is stored in v for the first time. You must not call any of the OCaml runtime functions or macros between registering and storing the value."
[16:31:44] <f[x]> и что?
[16:31:49] <Kakadu> А у меня по факту вначале создание, а потом регистрирование
[16:32:09] <f[x]> регистрируется value*
[16:32:17] <f[x]> сначала сохраняешь туда Val_unit
[16:32:29] <f[x]> потом создаёшь своё значение и записываешь туда
[16:33:11] <gds> f[x]: вроде как раз такой подход не катит: "between registering and storing" у тебя "создаёшь своё значение".
[16:33:44] <Kakadu> У меня по факту значение создается в камле, а register_global_root будет работать в сишечке после создания
[16:34:37] <aleksey> всё равно, главное чтоб gc знал что в том месте надо обновить адрес если данные будут двигаться
[16:35:04] <gds> значение из камла сохраняй куда-то в CAMLlocal-переменную, затем мгновенно сохраняй его в своё value и выполняй regiseter global root (& своё value).
[16:37:07] <Kakadu> а можно "своё value" заменить на (своё long)
[16:37:09] <Kakadu> ?
[16:37:49] Kakadu ещё придется разюираться почему камлокод пивисает
[16:39:34] <Kakadu> с register_global_root перестал падать, начал повисать в некотором месте. Будем разбираться
[16:41:49] <gds> лучше использовать value, если работаешь со значениями окамла.
[16:47:34] <Kakadu> http://paste.kde.org/712268/raw/ как-то так не работает. Спустя некоторое время объект камлёвый исчезает
[16:49:42] <aleksey> после & должно быть место где хранится value, а не параметр функции
[16:51:52] <f[x]> gds: это ограничение для того чтобы по root'у мусорщик не полез в тартарары
[16:52:00] <f[x]> а если туда val_unit сохранить то всё ок
[16:54:22] <Kakadu> aleksey: т.е. если я хочу сохранить где-то в дебрях иерархии QObject (откуда никак не достать lvalue), то это жопа. А если я захочу сохранить в приватном поле объекта --- то это должно быть норм?
[16:55:25] <aleksey> ага, надо как-то сообщать gc где оно хранится
[16:57:22] <Kakadu> ясно. Пойду пробовать
[17:18:15] tilarids вошёл(а) в комнату
[18:30:18] Zbroyar вошёл(а) в комнату
[18:46:10] zinid вышел(а) из комнаты
[18:50:51] tilarids вышел(а) из комнаты: Computer went to sleep
[19:12:31] Zbroyar вышел(а) из комнаты
[19:26:23] Typhon вышел(а) из комнаты
[19:39:36] f[x] вышел(а) из комнаты
[19:39:55] Typhon вошёл(а) в комнату
[19:48:18] Typhon вышел(а) из комнаты
[19:48:51] Typhon вошёл(а) в комнату
[20:15:24] Typhon вышел(а) из комнаты
[20:42:26] Typhon вошёл(а) в комнату
[20:42:56] Typhon вышел(а) из комнаты
[20:43:20] Typhon вошёл(а) в комнату
[20:48:17] Typhon вышел(а) из комнаты
[20:49:46] Typhon вошёл(а) в комнату
[20:55:48] Typhon вышел(а) из комнаты
[20:57:45] Typhon вошёл(а) в комнату
[21:03:54] Typhon вышел(а) из комнаты
[21:04:36] Typhon вошёл(а) в комнату
[21:05:09] Typhon вышел(а) из комнаты
[21:08:03] Typhon вошёл(а) в комнату
[21:08:51] Typhon вышел(а) из комнаты: Replaced by new connection
[21:09:01] Typhon вошёл(а) в комнату
[21:22:12] Typhon вышел(а) из комнаты
[21:29:34] Typhon вошёл(а) в комнату
[21:34:34] Typhon вышел(а) из комнаты
[21:45:29] Typhon вошёл(а) в комнату
[21:50:21] Typhon вышел(а) из комнаты: Replaced by new connection
[21:50:31] Typhon вошёл(а) в комнату
[21:58:09] Typhon вышел(а) из комнаты
[22:38:21] Typhon вошёл(а) в комнату
[22:41:34] Typhon вышел(а) из комнаты
[22:47:23] f[x] вошёл(а) в комнату
[22:55:23] f[x] вышел(а) из комнаты
[23:41:59] ermine вышел(а) из комнаты