OpenTheory Interpretation File Format

Overview

An OpenTheory interpretation file encodes a renaming of higher order logic symbols. Interpretation files take the form of text files using the UTF-8 encoding, and describe a set of symbol renamings.

Here is an example interpretation file:

###############################################################################
# Interpretations for instantiating the parametric modular theory
###############################################################################

type "Number.Modular.modular" as "Data.Word.word"

const "Number.Modular.*" as "Data.Word.*"
const "Number.Modular.+" as "Data.Word.+"
const "Number.Modular.-" as "Data.Word.-"
const "Number.Modular.<" as "Data.Word.<"
const "Number.Modular.<=" as "Data.Word.<="
const "Number.Modular.^" as "Data.Word.^"
const "Number.Modular.~" as "Data.Word.~"
const "Number.Modular.fromNatural" as "Data.Word.fromNatural"
const "Number.Modular.modulus" as "Data.Word.modulus"
const "Number.Modular.random" as "Data.Word.random"
const "Number.Modular.toNatural" as "Data.Word.toNatural"

Each line of an interpretation file is either a comment line or a renaming line:

A comment line is either blank or has # as its first character.
A renaming line has the form KIND "NAME" as "NAME".

Comment lines are ignored when processing the file.

Renaming lines use the following syntax:

KIND: This declares the kind of symbol being renamed: the legal values are type (to rename a type operator) and const (to rename a constant).
"NAME": This declares the name of the symbol before and after renaming: the legal values are the same as the legal quoted string commands in article files.

The renaming line KIND "X" as "Y" means the symbol with kind KIND and name "X" will be renamed to "Y". The renaming lines in the interpretation file must comprise a well-defined function: it is an error to have multiple renamings of the form KIND "X" as "Y" with the same KIND and "X" (even if they all agree on the "Y").