Coq zu OCaml Extraktion von algebraischen Typen

Question

Wenn I extrahieren folgende Coq Datentypen OCaml:

Inductive Foo := | A | B. 
Inductive Bar (f:Foo) := | C | D. 
Extraction Language Ocaml. 
Extraction "test.ml" Foo Bar. 

ich die folgende ML-Code:

type foo = 
| A 
| B 

type bar = 
| C 
| D 

Die 'bar' Typ unterscheidet sich von Coqs haben als Teil ihrer Typ-Signatur "f".

Was ist der beste Weg, um solche Typen zu definieren, damit sie OCaml gut extrahiert werden?

Answer 1

Sie können nicht: OCaml unterstützt die Indizierung von Typen nicht nach Begriffswerten und als Konsequenz machen Dinge wie Bar A keinen Sinn darin. Coq ist gezwungen, die zusätzlichen Indizes zu löschen, damit die Definitionen mit dem Typsystem von OCaml kompatibel sind.