Module Theory

module Theory: sig .. end

Bindings for Coq constants that are specific to the plugin; reification and translation functions.

Note: this module is highly correlated with the definitions of AAC_rewrite.v.

This module interfaces with the above Coq module; it provides facilities to interpret a term with arbitrary operators as an abstract syntax tree, and to convert an AST into a Coq term (either using the Coq "raw" terms, as written in the starting goal, or using the reified Coq datatypes we define in AAC_rewrite.v).

Both in OCaml and Coq, we represent finite multisets using weighted lists (('a*int) list), see Matcher.mset.

mk_mset ty l constructs a Coq multiset from an OCaml multiset l of Coq terms of type ty

val mk_mset : EConstr.constr -> (EConstr.constr * int) list -> EConstr.constr

Packaging modules

module Sigma: sig .. end

Environments

module Sym: sig .. end

Dynamically typed morphisms

module Stubs: sig .. end

We need to export some Coq stubs out of this module.

Building reified terms

We define a bundle of functions to build reified versions of the terms (those that will be given to the reflexive decision procedure). In particular, each field takes as first argument the index of the symbol rather than the symbol itself.

module Trans: sig .. end

Tranlations between Coq and OCaml