package lambdapi
-
lambdapi.tool
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
package lambdapi
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
Representation of an atomic pattern constructor.
type t = | Symb of Common.Path.t * string * int(*Symbol identified by a fully qualified name (module path and name) and its arity in the pattern.
*)| Vari of int(*A bound variable identified by a (branch-wise) unique integer. These variables are used with a bidirectional map (implemented as two maps) to a higher order (Bindlib) variable. They are also used in the environment builder to refer to the higher order variables a term may depend on.
*)
Atomic pattern constructor. Term are identified by these constructors in the trees. During matching (in Eval.tree_walk), terms are transformed into these constructors to get the right sub-tree.
NOTE the effective arity carried by the representation of a symbol is specific to a given symbol instance. Indeed, a symbol (in the sense of Term.sym) may lead to several constructors, with different effective arities. In the pattern “f g (g $x)” for example, symbol g is used with arity 0 (first occurence) and 1 (second occurence).
val pp : t Lplib.Base.pppp oc c prints tree constructor c to output channel o.