Описание тега coq-extraction

Вопросы с тегом
0 ответов

Coq учебник по evars, e* тактика, контексты?

Я пытался найти хорошее руководство / чтение / набор упражнений по контекстам Coq, evars, e* тактике и т. Д. В идеале я хочу создать контекст Coq с некоторыми абстрагированными переменными, которые я заполню позже при извлечении OCaml или Haskell. В…
13 фев '18 в 16:14
0 ответов

Извлечь функтор из Coq в Ocaml, используя механизм извлечения Coq

У меня есть функция PolyInterpretation ( http://color.inria.fr/doc/CoLoR.PolyInt.APolyInt.html) Definition PolyInterpretation := forall f : Sig, poly (arity f). и подпись модуля TPolyInt( http://color.inria.fr/doc/CoLoR.PolyInt.APolyInt_MA.html) Mod…
22 мар '13 в 09:54
1 ответ

Как установить имя модуля при извлечении Coq в Haskell

Когда я извлекаю / компилирую Coq в Haskell, используя Extraction Language Haskell. в файле Coq и работает coqtop -compile mymodule.v > MyModule.hsЯ получаю модуль Haskell, который начинается с module Main where, Есть ли возможность установить по…
14 сен '17 в 15:39
1 ответ

Извлечение coq типа nat в какой тип ocaml, чтобы я мог иметь сертифицированную программу

В Coq Извлечение из типа nat в int или же big_int не сертифицированы (они эффективны). Как в этих ссылках ниже: http://coq.inria.fr/V8.3/stdlib/Coq.extraction.ExtrOcamlNatBigInt.html и http://coq.inria.fr/distrib/8.3/stdlib/Coq.extraction.ExtrOcamlN…
29 авг '14 в 02:08
1 ответ

Извлечение Coq: отказано в разрешении

Когда я выполняю следующие команды в CoqIDE: Extraction Language Haskell. Extraction "Code.hs" my_function. Я получаю следующую ошибку: System error: "Code.hs: Permission denied" Если я попробую вместо этого: Extraction Language Haskell. Extraction …
18 дек '15 в 05:54
1 ответ

Строка OCaml и строка Coq (извлечение из Coq в OCaml)

Я использовал извлечение из Coq в OCaml, где у меня есть тип Z, N, positive Я не использую, чтобы извлечь его в int OCaml. Тогда тип, который я имею после извлечения: type positive = | Coq_xI of positive | Coq_xO of positive | Coq_xH type coq_N = | …
02 сен '14 в 03:03
1 ответ

Механизм извлечения Coq генерирует "failwith "AXIOM TO REALIZE""

У меня есть структура модуля внутри этого модуля, я объявляю использование переменной для некоторой функции внутри module A, Module A. Variable a : nat. End A. Тогда я использую механизм извлечения. Extraction Language Ocaml. Set Extraction Optimize…
07 мар '13 в 06:09
1 ответ

Что делает команда Coq Require Import Ltac?

Когда я смотрю на проект QuickChick, я столкнулся с предложением Require Import Ltac. Я не знаю, что это делает и где Ltac Модуль есть. Я нашел файл plugins/ltac/Ltac.v, но это не могло быть так, поскольку этот файл пуст (кстати, зачем вообще включа…
30 мар '18 в 20:33
1 ответ

Что такое EvalOp в Coq CompCert

Определение EvalOp находится в compcert.backend.SplitLongproof: Ltac EvalOp := eauto; match goal with | [ |- eval_exprlist _ _ _ _ _ Enil _ ] => constructor | [ |- eval_exprlist _ _ _ _ _ (_:::_) _ ] => econstructor; EvalOp | [ |- eval_expr _ …
26 мар '18 в 21:45
1 ответ

Как извлечь Coq's Z в целое число Хаскелла

Я пытаюсь извлечь в Haskell программу на Coq, которая использует Z номера. Я хочу отобразить Coq's Z на целое число Хаскелла. Я нашел несколько библиотек для этой цели, но не для Хаскелла. Для этого нет библиотеки? Мне нужны извлечения (найдены здес…
07 май '18 в 17:17
1 ответ

Используйте функцию после сгенерированного извлечения из Coq в Ocaml

У меня есть папка tmp который генерируется после того, как я делаю извлечение из coq в ocaml. ~/tmp/cpf0.ml cpf0.mli cpf0.o cpf0.cmi cpf0.cmx cpf0.cmo main.ml это файл, который я использую для вызова одной функции в cpf0: let prf = Cpf0.proof;; Я по…
24 мар '12 в 03:45
1 ответ

Генерация кода на Haskell из COQ: используется логическое значение или значение арности

В настоящее время я пытаюсь сгенерировать код на Haskell из моей леммы проверки программы, которая выглядит следующим образом: Lemma the_thing_is_ok : forall (e:Something), Matches e (calculate_value e). Сразу после окончания моего раздела я делаю: …
27 ноя '14 в 17:14
1 ответ

Можно ли извлечь Positive, Nat для int32, Z для int?

Привет, я пишу извлечение из Coq в Ocaml, я хотел бы преобразовать тип: positive --> int32 N -> int32 но я хочу сохранить тип Z является int Вот код, который я делаю, чтобы извлечь эти условия: Require Import ZArith NArith. Require Import Extr…
02 май '12 в 04:14
1 ответ

Извлечь в файл OCaml с помощью "Рекурсивное извлечение" в Coq

Я хочу извлечь функцию foo в Coq для OCaml файл. Потому что моя настоящая функция должна использовать Recursive ExtractionКогда я запускаю программу, она выводит извлеченный код OCaml на cmd, Но я хотел бы вывести его в файл, например: foo.ml Recurs…
10 апр '13 в 08:15
1 ответ

Можете ли вы автоматически добавлять операторы импорта Haskell при извлечении из Coq?

Я делаю извлечение из Coq в Haskell, которое требует импорта нескольких модулей на конец Haskell. Есть ли какая-либо функция извлечения Coq, которая позволяет делать это автоматически? Я знаю, что мог бы просто написать сценарий для этого, но я бы п…
30 апр '18 в 14:32
2 ответа

string_dec и строка в библиотеке Ocaml

У меня есть файл: String0.ml извлеченный из String.v (Это из библиотеки Coq) String.ml: это струнная библиотека Ocaml После извлечения моего тестового файла из Coq в Ocaml, я хочу использовать String.ml в библиотеке Ocaml, поэтому я пишу команду зам…
10 апр '12 в 08:09
1 ответ

Конвертировать nat в big_int для извлечения Coq в Ocaml

Я делаю извлечение конвертировать nat в big_int Когда я использовал библиотеку: ExtrOcamlNatBigInt, она не возвращает правильный тип для big_int в Ocaml Поэтому я изменяю его (файл ExtrOcamlNatBigInt), но не могу найти способ определить функцию nat_…
17 апр '12 в 07:17
2 ответа

Можно ли писать программы на C, используя Coq?

Я знаю, что можно извлечь программы Coq в программы на Haskell и OCaml. Есть ли способ сделать это с C? Я представляю библиотеку, которая моделирует язык Си. Возможно, такая библиотека будет содержать коллекцию аксиом о том, как конструкции C взаимо…
23 окт '17 в 21:03
1 ответ

Каковы исходные цели, отложенные цели и заброшенные цели в Coq?

Я использую ideslave Coq (он же протокол XML). По телефону <call val="Goal"><unit/></call>, типичная обратная связь выглядит <value val="good"><option val="some"><goals><list><goal><string>239&lt…
11 мар '18 в 05:11
1 ответ

Coq XML Protocol: вероятная неисправность PrintAST

Я использую протокол XML из Coq 8.6.1. Когда я попробовал вызов PrintAst, мне не удалось получить AST, но вместо этого я получил "todo". Это неисправность или я сделал что-то не так? Как я должен получить AST от печатного вызова AST? Вот мой случай:…
09 дек '17 в 22:48