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.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.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 : Term.constr -> (Term.constr * int) list -> Term.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