Файловый ввод/вывод в Coq через ynot

У кого-нибудь есть небольшой рабочий фрагмент кода для чтения строк из файла в Coq (похоже, это делает библиотека ynot, но я не могу понять)?

Ynot можно найти здесь: http://ynot.cs.harvard.edu/ Дистрибутив содержит Каталог IO в примерах, который включает FS.v, который определяет такие вещи, как:

Fixpoint ReadFile (fm : fd_model) (ms : list mode) (fd : File fm ms) (str : string) {struct str} : Trace :=  
   match str with  
       | EmptyString => Read fd None :: nil  
       | String a b => (ReadFile fd b) ++ (Read fd (Some a) :: nil)  
   end.

Но я не могу понять, как его вызвать.

Я пробовал такие вещи, как:

Eval compute in ReadFile (File (FileModel "demo.txt") [R]).  
                          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^  
Error: The term "File (FileModel "demo.txt") [R]" has type "Set" while it is expected to have type "File ?16 ?17".

Точно так же проект Quark (http://goto.ucsd.edu/quark/) определяет VCRIO.v с альтернативные механизмы.

Любая помощь приветствуется!


io coq
person user3888753    schedule 29.07.2014    source источник

Ответы (2)


arrow_upward
5
arrow_downward

В общем, вы не сможете выполнять файловый ввод-вывод непосредственно внутри Coq по той простой причине, что базовый язык Gallina является чистым и тотальным.

В частности, функция ReadFile, на которую вы смотрите, — это не функция, которая читает файл, а функция, которая вычисляет трассировку, сгенерированную действием чтения файла.

Способ, которым мы обходим это в Quark (и его преемнике Reflex http://goto.ucsd.edu/reflex), заключается в следующем: аксиоматизировать эти эффективные действия, см., например, https://github.com/UCSD-PL/kraken/blob/master/reflex/coq/ReflexIO.v из строки 323 для аксиоматизированного типа наших примитивов.

Итак, на стороне Coq мы рассуждаем об использовании этого монадического эффективного типа, а затем, когда код извлечен, эти аксиомы реализуются с помощью функций OCaml соответствующего типа, см. здесь https://github.com/UCSD-PL/kraken/blob/master/reflex/ml/primitives/ReflexImpl.ml строка 111.

Это, очевидно, увеличивает вашу доверенную вычислительную базу, поскольку вам нужно убедиться, что ваши примитивы делают именно то, что вы аксиоматизировали, и не более того.

Напомним, что мы не можем выполнять эффективные операции в самой Gallina, поэтому мы аксиомируем эти действия и действительно можем выполнять их только с извлеченным кодом OCaml.

Я не знаю ни одной техники, которая позволила бы вам делать это с богатыми типами внутри Gallina.

person Ptival    schedule 30.07.2014

arrow_upward
2
arrow_downward

Моделирование ввода-вывода (посредством его аксиоматизации) и настройка его для извлечения (путем реализации) аналогично использованию FFI Haskell. Однако вы не сможете запустить код в доказательствах или с помощью интерпретатора. Вы сможете запустить его, только распаковав и скомпилировав. Но это просто досадное неудобство. Представьте, если бы вы определили plus следующим образом:

Axiom plus : nat -> nat -> nat.
Infix "+" := plus.
Axiom plus_0 : forall n1, n1 + 0 = n1.
Axiom plus_S : forall n1 n2, n1 + (S n2) = S (n1 + n2).

Это не будет исполняемым, но вы все равно сможете доказать все, что вам нужно, чтобы доказать plus. Однако сроки доказательства были бы больше. Например, eq_refl больше не будет доказательством 2 + 2 = 4. Кроме того, Coq больше не будет проводить проверку работоспособности.

Для части "реализация", если вы извлекаете в Haskell, вы делаете что-то вроде этого:

Extract Constant plus => "(\ n1 n2 -> case n2 of
  O -> n1
  S n3 -> S (plus n1 n3))".

А потом извлекаешь.

Extraction Language Haskell.
Recursive Extraction plus.

Теперь попробуйте извлечь, не осознавая.

person Community    schedule 31.07.2014