CODEWITHSUNDEEP
ocamlcoq
tom
tom

Reputation: 1588

Inspecting elements of an inductive type from OCaml

I would like to write a Coq plugin which would take an element of an inductive type and recursively pattern match on the element and preform some computation in each iteration. This sounds like a quite straight forward thing to do, but I don't really know where to start.

I have managed to find some Coq plugins, compile them and run them. But I have not found any kind of overview of Coq API to a get idea of basic concepts.

Useful resources I have found so far:

Simple example:

Let's have a simple inductive type representing expressions with a single binary operation

Inductive expr : Type :=
| var : nat  -> expr
| op  : expr -> expr -> expr

I would like to define a new Vernacular command InspectExpression which will recursively go over the expression and preform some computation. 

InspectExpression (op (op (var 0) (var 1)) (var 2)). (* expression: "(x+y)+z" *)

My ultimate goal is to generate some C++ code based on these expressions, but I don't think that is important for the question/answer.

Upvotes: 2

Views: 102

Answers (1)

ejgallego
ejgallego

Reputation: 6852

The canonical source these days is the official Coq Plugin Tutorial which while up-to-date, needs some help both with Google fu [so it appears first in searches] and with formatting / presentation.

I'd say start there, and don't hesitate to open bugs in the Coq issue tracker if you would like to get some other kind of examples included.

Coq's discourse and Gitter channel are also very useful devices for plugin developers.

Upvotes: 2

Related Questions