ааа, убейте меня, иначе я всё забрызгаю тут1111
@default631">http://flint.cs.yale.edu/cs428/coq/doc/R...
СУТЬ:
У вас есть индуктивный тип данных для представления вашего игрушечного AST, специфичного для вашей предметной области.
У вас есть функция, преобразующая _ваши_ значения из AST в конкретные значения _coq'а_. (конечно, на функцию накладываются кое-какие ограничения, магии ведь нет.)
Теперь внимательно следите за руками: тактика "quote имявашейфункции" преобразует выражение coq'а, записанное в AST coq'а, в значение, имеющее тип данных вашего AST, согласно предоставленной функции. (значение, собственно, внутри тоже будет представлено в AST coq'а, но с ним можно работать в "userland", и, при желании, применив к нему "вашуфункцию", получить обратно значение в AST coq'а.)
Обратите внимание на направление преобразований между двумя AST.
По-моему, это что-то наподобие встроенного термоядерного camlp4.
Надо осмыслить.
(тега "академота" нет, потому что это настолько "практикота", что аж страшно становится.)
6 comments
recommend
bookmark
subscribe
(парсер лох, ссылка побилась, см. http://flint.cs.yale.edu/cs428/coq/doc/R... секцию "10.7 quote")
> У вас есть функция, преобразующая _ваши_ значения из AST в конкретные значения _coq'а_
> тактика "quote имявашейфункции" преобразует выражение coq'а, записанное в AST coq'а, в значение, имеющее тип данных вашего AST
т.е. эта тактика, принимая наше отображение, упомянутое выше, делает с выражением coq нечто похожее на действие обратного к нашему отображения; короче из нашего отображения, генерит обратное и его использует.
(/me начинает вспоминать теоремы о невозможности построения обратного отображения в общем виде, но точную формулировку вспомнить не может)
P.S. если что ссылку на мануал не читал, попробую чуть попозжее взяться.
да, там именно генерация обратного отображения. И да, не везде работает. Но я предвидел такое развитие событий, уточнив "(конечно, на функцию накладываются кое-какие ограничения, магии ведь нет.)"
кстати, если чо, ссылку на мануал необязательно читать, там не больше, чем я описал. разве что там примеры есть, и хорошие.
постараюсь найти время на ковыряние coq
ну смотри, если оно нужно. Если есть что-то, что в окамле типами записать сложно, а жутко хочется — скорее всего в coq это запишется легко, а сгенерённый камлокод будет работать. Далее, если надо что-то доказать о программе (например, тупо, что делим не на ноль) — тоже coq пригоден. А если просто кодить — на окамле быстрее, всё-таки, и по кодингу, и по скорости результата, и лучше по выразительности.