package lambdapi
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=9bc8ae3694dd51bd5742e7aba760bd2878c4b0e5ef9b3d4a7b06f3cd303b611d
sha512=c812c3129b3d85b0c4d7e741d11137dbb4fe2a0aaba3a5968409080b742924ecb506280c19ad83ef6bc910346db96d87780313fa7683c29345edae16ae79c704
doc/lambdapi.export/Export/Xtc/index.html
Module Export.Xtc
Source
This module provides a function to translate a simply typed signature to the XTC format used in the termination competition.
Remarks:
- SizeChangeTool accepts an extension of the XTC format with lambda and application in types and:
<arrow> <var>...</var> <type>...</type> <type>...</type> </arrow>
<typeLevelRule> <TLlhs>...</TLlhs> <TLrhs>...</TLrhs> </typeLevelRule>
syms
maps every symbol to a name.
bvars
is the set of abstracted variables.
pvars
is the list of all pattern variables with their type.
typ
is a reference to the types of the pvars of the current rules.
sym_name s
translates the symbol name of s
.
add_sym
declares a Lambdapi symbol.
type_sym ppf s
translates the Lambdapi type symbol s
.
sym ppf s
translates the Lambdapi symbol s
.
add_bvar v
declares an abstracted Lambdapi variable.
bvar v
translates the Lambdapi bound variable v
.
pvar i
translates the Lambdapi pattern variable i
.
term ppf t
translates the term t
.
add_pvars s r
adds the types of the pvars of r
in pvars
.
rule ppf r
translates the pair of terms r
as a rule.
sym_rule ppf s r
increases the number of rules and translates the sym_rule r
.
Translate the rules of symbol s
.
Translate the rules of a dependency except if it is a ghost signature.
sign ppf s
translates the Lambdapi signature s
.