package lambdapi
Install
dune-project
Dependency
Authors
Maintainers
Sources
sha256=9b13c3121ef87cf4d3311a8a1db43db4be7f0e5e2a702fdaff04a3b3c432cb31
sha512=81e0760ca77cb862a5bdb8927aa37faf7141c4e2484a8163dad0a3eaa21cc691acb5f72279c78588c085f53dde4bd35186346378feac0ab55ac06a679cf2e60f
doc/lambdapi.export/Export/Xtc/index.html
Module Export.XtcSource
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.