September 4th, 2012

coq + inlining + "merge right"

Некоторые люди прочитали статью http://alaska-kamtchatka.blogspot.com/2012/08/merge-right.html , где была показана весьма общая функция для слияния/пересечения/разницы списков.
А господин ygrek в камлочятике прилюдно мучил MetaOCaml для инлайнинга функций-аргументов merge. Я не мог на это смотреть спокойно. Однако и сразу разобраться не смог, так как не знал многого, но вполне так узнал.
Чтобы было хоть сколько-нибудь интересно читать, рекомендую прочитать сначала исходную статью.
Потому что сейчас будет простыня.
Collapse )
Вроде ЗБС.
Можно было бы сравнение не инлайнить, но избавиться от вызова функции (будь то "(fun (a : int) b -> ...)", будь то Pervasives.compare) не получается сходу.
Мне Coq нужен не только для зависимых типов и доказательств кода, но и для инлайнинга. Я -- практичная скотина, да!
Если будут вопросы -- поясню. Потому что всё сразу пояснять -- руки устанут.