package lambdapi

  1. Overview
  2. Docs
Proof assistant for the λΠ-calculus modulo rewriting

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (12)

Authors

  1. D
    Deducteam

Maintainers

  1. D
    dedukti-dev@inria.fr

Sources

lambdapi-3.0.0.tbz
sha256=1066aed2618fd8e6a400c5147dbf55ea977ce8d3fe2e518ac6785c6775a1b8be
sha512=f7f499626aba92e070ae69581299a58525973fdbfd04a160ed3ac89209fb6cbe307b816d0b23e1b75bc83467ce8b4b0530c6f9816eaf58f7a07fde65a450106c

doc/lambdapi.core/Core/Tree/CP/index.html

Module Tree.CPSource

Module providing a representation for pools of conditions.

Sourcemodule PSet : sig ... end

Functional sets of pairs of integers.

Sourcetype t = {
  1. variables : int Lplib.Extra.IntMap.t;
    (*

    An association (e, v) maps the slot of a pattern variable (the first argument of a Term.term.Patt) to its slot in the array vars of the Eval.tree_walk function. It is used to remember non linearity constraints.

    *)
  2. nl_conds : PSet.t;
    (*

    Set of convertibility constraints (i,j) with i < j. The constraint (i,j) is satisfied if the terms stored at indices i and j in the vars array of the Eval.tree_walk function are convertible.

    *)
  3. fv_conds : int array Lplib.Extra.IntMap.t;
    (*

    A mapping of i to xs represents a free variable condition that can only be satisfied if only the free variables of x appear in the term stored at slot i in the vars array of Eval.tree_walk.

    *)
}

A pool of (convertibility and free variable) conditions.

Sourceval empty : t

empty is the condition pool holding no condition.

Sourceval is_empty : t -> bool

is_empty pool tells whether the pool of constraints is empty.

Sourceval register_nl : int -> int -> t -> t

register_nl slot i pool registers the fact that the slot slot in the vars array correspond to a term stored at index i in the environment for the RHS. The first time that such a slot is associated to i, it is registered to serve as a reference point for testing convertibility when (and if) another such slot is (ever) encountered. When that is the case, a convertibility constraint is registered between the term stored in the slot slot and the term stored in the reference slot.

Sourceval register_fv : int -> int array -> t -> t

register_fv slot xs pool registers a free variables constraint for the variables in xs on the slot slot of the vars array in pool.

Sourceval constrained_nl : int -> t -> bool

constrained_nl i pool tells whether index i in the RHS's environment has already been associated to a variable of the vars array.

Sourceval is_contained : Tree_type.tree_cond -> t -> bool

is_contained cond pool tells whether the condition cond is contained in the pool pool.

Sourceval remove : Tree_type.tree_cond -> t -> t

remove cond pool removes condition cond from the pool pool.

Sourceval choose : t list -> Tree_type.tree_cond option

choose pools selects a condition to check in the pools of pools. The heuristic is to first select convertibility constraints.