package lambdapi

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

This module provides a function to translate a signature to the HRS format used in the confluence competition.

  • see http://project-coco.uibk.ac.at/problems/hrs.php

    .

    • Lambdapi terms are translated to the following HRS term algebra with a unique type t:

    A : t -> t -> t // for application

    L : t -> (t -> t) -> t // for λ

    B : t -> t -> (t -> t) -> t // for let

    P : t -> (t -> t) -> t // for Π

    Function symbols and variables are translated as symbols of type t.

    Pattern variables of arity n are translated as variables of type t -> ... -> t with n times ->.

    • In the hrs format, variable names must be distinct from function symbol names. So bound variables are translated into positive integers and pattern variables are prefixed by "$".
    • There is no clash between function symbol names and A, B, L, P because function symbol names are fully qualified.
    • Function symbol names are fully qualified but "." is replaced by "_" because "." cannot be used in identifiers ("." is used in lambda abstractions).
    • Two occurrences of the same pattern variable name may have two different arities (in two different rules). So pattern variable names are prefixed by the rule number.

    TO DO:

    • HRS does not accept unicode characters.
    • Optim: output only the symbols used in the rules.
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.

module V : sig ... end

pvars map every pattern variable name to its arity.

module VMap : sig ... end
val pvars : int VMap.t Stdlib.ref

sym_name s translates the symbol name of s.

val add_sym : Core.Term.sym -> unit

add_sym declares a Lambdapi symbol.

sym ppf s translates the Lambdapi symbol s.

val add_bvar : Core.Term.tvar -> unit

add_bvar v declares an abstracted Lambdapi variable.

bvar v translates the Lambdapi variable v.

val pvar : int Lplib.Base.pp

pvar i translates the pattern variable index i.

val add_pvar : int -> int -> unit

add_pvar i k declares a pvar of index i and arity k.

term ppf t translates the term t.

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.

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.

sign ppf s translates the Lambdapi signature s.