public class FolTranslator
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
java.util.Map<Stmt,java.lang.String> |
alignments |
java.util.Map<Axiom,byte[][]> |
boundVars |
ProofAsst |
pa |
java.util.Map<Axiom,Axiom> |
syntaxToDefn |
Constructor and Description |
---|
FolTranslator(ProofAsst pa,
SetMMConstants sc)
Create a new
FolTranslator instance. |
Modifier and Type | Method and Description |
---|---|
java.lang.String |
align(Stmt stmt) |
byte[][] |
getBoundVars(Axiom syntax)
Gets the bound variable data for a given syntax axiom.
|
LFType |
translateAssrt(Assrt assrt) |
LFTerm |
translateProof(Assrt assrt) |
LFTerm.LFVar |
var(VarHyp vh,
LFType type)
Mangles variable names to make them valid identifiers.
|
public final ProofAsst pa
public final java.util.Map<Axiom,byte[][]> boundVars
public final java.util.Map<Stmt,java.lang.String> alignments
public FolTranslator(ProofAsst pa, SetMMConstants sc) throws SetMMException
FolTranslator
instance.pa
- The parent ProofAsst
instance.sc
- The parent SetMMConstants
instance (this class only
works on set.mm
).SetMMException
- If this database does not look like set.mmpublic byte[][] getBoundVars(Axiom syntax) throws SetMMException
byte[]
for each variable in the constructor, in database order.
The non-set variables are null, and the set variable entries are a list
over the variables again.
The byte
value at this index is 1
if there are bound
occurrences of the set variable in the other variable, and 2
if
there are free occurrences of the set variable. If both occur (i.e. the
set variable occurs both bound and free, such as in df-sb) it is set to
3
, and 0
if neither occurs (which should not happen
unless the set variable is not used in the definition at all).
The value of the array at two set variables is not meaningful and can be
anything, except that a variable is considered to appear free w.r.t
itself (i.e. (boundVars[i][i] & 2) != 0
when it appears free in
the definition.
syntax
- the syntax axiomSetMMException
- if bound variable data is not available for the
syntaxpublic java.lang.String align(Stmt stmt)
public LFTerm.LFVar var(VarHyp vh, LFType type)
vh
- Input variable hyptype
- variable typepublic LFType translateAssrt(Assrt assrt) throws SetMMException
SetMMException
public LFTerm translateProof(Assrt assrt) throws SetMMException
SetMMException