Coq plugin for printing term abstract syntax trees and their digests
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
.gitignore
.travis-ci.sh
.travis.yml
AST.v
LICENSE
Makefile
README.md
_CoqProject
adler32.ml
adler32.mli
ast.ml4
ast_plugin.mlpack
descr
opam

README.md

AST Coq Plugin

Build Status

A Coq plugin for printing semi-canonical abstract syntax trees (ASTs) with unique kernel names or digests of such trees.

Requirements

Building

The easiest way to install the plugin is via OPAM:

opam repo add proofengineering-dev http://opam-dev.proofengineering.org
opam install coq-ast

To build the plugin manually, run make in the root directory. Then, to install it, run make install.

Usage Examples

(* require and import plugin *)
Require Import AST.AST.

(* constants to analyze *)
Require Import List.

(* print list of identifier ASTs as JSON to stdout *)
AST map filter.

(* print list of identifier ASTs as JSON to file *)
AST "asts.json" map filter.

(* print MD5 digests of identifiers as JSON to stdout *)
Digest MD5 map filter.

(* print Adler32 digests of identifiers as JSON to stdout *)
Digest ADLER32 map filter.

(* print MD5 digests of identifiers as JSON to file digests.json *)
Digest MD5 "digests.json" map filter.

(* print ASTs for all identifiers in modules List and Logic as JSON to file asts.json *)
ModuleAST "asts.json" Logic List.

(* print MD5 digests for all identifiers in modules List and Logic as JSON to file digests.json *)
ModuleDigest MD5 "digests.json" Logic List.