lambdapi 2.5.1 · OCaml Package

This module provides a function to translate a simply typed signature to the XTC format used in the termination competition.

see https://raw.githubusercontent.com/TermCOMP/TPDB/master/xml/xtc.xsd
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>

val syms : string Core.Term.SymMap.t Stdlib.ref

syms maps every symbol to a name.

val bvars : Lplib.Extra.IntSet.t Stdlib.ref

bvars is the set of abstracted variables.

val nb_rules : int Stdlib.ref

nb_rules is the number of rewrite rules.

val pvars : (int * int * Core.Term.term) list Stdlib.ref

pvars is the list of all pattern variables with their type.

val type_of_pvar : Core.Term.term array Stdlib.ref

typ is a reference to the types of the pvars of the current rules.

val sym_name : Core.Term.sym Lplib.Base.pp

sym_name s translates the symbol name of s.

val add_sym : Core.Term.sym -> unit

add_sym declares a Lambdapi symbol.

val type_sym : Core.Term.sym Lplib.Base.pp

type_sym ppf s translates the Lambdapi type symbol s.

val sym : Core.Term.sym Lplib.Base.pp

sym ppf s translates the Lambdapi symbol s.

val add_bvar : Core.Term.tvar -> unit

add_bvar v declares an abstracted Lambdapi variable.

val bvar : Core.Term.tvar Lplib.Base.pp

bvar v translates the Lambdapi bound variable v.

val pvar : int Lplib.Base.pp

pvar i translates the Lambdapi pattern variable i.

val term : Core.Term.term Lplib.Base.pp

term ppf t translates the term t.

val head : Core.Term.term Lplib.Base.pp

val pvar_app : (int * Core.Term.term array) Lplib.Base.pp

val typ : Core.Term.term Lplib.Base.pp

val add_pvars : Core.Term.sym -> Core.Term.rule -> unit

add_pvars s r adds the types of the pvars of r in pvars.

val rule : (Core.Term.term * Core.Term.term) Lplib.Base.pp

rule ppf r translates the pair of terms r as a rule.

val sym_rule : Core.Term.sym -> Core.Term.rule Lplib.Base.pp

sym_rule ppf s r increases the number of rules and translates the sym_rule r.

val rules_of_sym : Core.Term.sym Lplib.Base.pp

Translate the rules of symbol s.

val rules_of_sign : Core.Sign.t Lplib.Base.pp

Translate the rules of a dependency except if it is a ghost signature.

val sign : Core.Sign.t Lplib.Base.pp

sign ppf s translates the Lambdapi signature s.

package lambdapi