package lambdapi

  1. Overview
  2. Docs
package lambdapi
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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>

Sourceval syms : string Core.Term.SymMap.t ref

syms maps every symbol to a name.

bvars is the set of abstracted variables.

Sourceval nb_rules : int ref

nb_rules is the number of rewrite rules.

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

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

Sourceval type_of_pvar : Core.Term.term array ref

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

sym_name s translates the symbol name of s.

Sourceval add_sym : Core.Term.sym -> unit

add_sym declares a Lambdapi symbol.

type_sym ppf s translates the Lambdapi type symbol s.

sym ppf s translates the Lambdapi symbol s.

Sourceval add_bvar : Core.Term.tvar -> unit

add_bvar v declares an abstracted Lambdapi variable.

bvar v translates the Lambdapi bound variable v.

Sourceval pvar : int Lplib.Base.pp

pvar i translates the Lambdapi pattern variable i.

term ppf t translates the term t.

Sourceval pvar_app : (int * Core.Term.term array) Lplib.Base.pp
Sourceval add_pvars : Core.Term.sym -> Core.Term.rule -> unit

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.

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

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

sign ppf s translates the Lambdapi signature s.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct