lambdapi

Proof assistant for the λΠ-calculus modulo rewriting
package lambdapi
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library lambdapi.core
Module Core . Term

Term (and symbol) representation

type qident = Common.Path.t * string

Representation of a possibly qualified identifier.

type match_strat =
| Sequen(*

Rules are processed sequentially: a rule can be applied only if the previous ones (in the order of declaration) cannot be.

*)
| Eager(*

Any rule that filters a term can be applied (even if a rule defined earlier filters the term as well). This is the default.

*)

Pattern-matching strategy modifiers.

type expo =
| Public(*

Visible and usable everywhere.

*)
| Protec(*

Visible everywhere but usable in LHS arguments only.

*)
| Privat(*

Not visible and thus not usable.

*)

Specify the visibility and usability of symbols outside their module.

type prop =
| Defin(*

Definable.

*)
| Const(*

Constant.

*)
| Injec(*

Injective.

*)
| Commu(*

Commutative.

*)
| Assoc of bool(*

Associative left if true, right if false.

*)
| AC of bool(*

Associative and commutative.

*)

Symbol properties.

type term = private
| Vari of tvar(*

Free variable.

*)
| Type(*

"TYPE" constant.

*)
| Kind(*

"KIND" constant.

*)
| Symb of sym(*

User-defined symbol.

*)
| Prod of term * tbinder(*

Dependent product.

*)
| Abst of term * tbinder(*

Abstraction.

*)
| Appl of term * term(*

Term application.

*)
| Meta of meta * term array(*

Metavariable application.

*)
| Patt of int option * string * term array(*

Pattern variable application (only used in rewriting rules LHS).

*)
| TEnv of term_env * term array(*

Term environment (only used in rewriting rules RHS).

*)
| Wild(*

Wildcard (only used for surface matching, never in LHS).

*)
| Plac of bool(*

Plac b is a placeholder, or hole, for not given terms. Boolean b is true if the placeholder stands for a type.

*)
| TRef of term option Timed.ref(*

Reference cell (used in surface matching).

*)
| LLet of term * term * tbinder(*

LLet(a, t, u) is let x : a ≔ t in u (with x bound in u).

*)

Representation of a term (or types) in a general sense. Values of the type are also used, for example, in the representation of patterns or rewriting rules. Specific constructors are included for such applications, and they are considered invalid in unrelated code.

NOTE that a wildcard "_" of the concrete (source code) syntax may have a different representation depending on the application. For instance, the Wild constructor is only used when matching patterns (e.g., with the "rewrite" tactic). In the LHS of a rewriting rule, we use the Patt constructor to represend wildcards of the concrete syntax. They are thus considered to be fresh, unused pattern variables.

Representation of a rewriting rule RHS (or action) as given in the type of rewriting rules (see Term.rule.rhs) with the number of variables that are not in the LHS. In decision trees, a RHS is stored in every leaf since they correspond to matched rules.

and dtree = (rhs * int) Tree_type.dtree

Representation of a decision tree (used for rewriting).

and sym = {
sym_expo : expo;(*

Visibility.

*)
sym_path : Common.Path.t;(*

Module in which the symbol is defined.

*)
sym_name : string;(*

Name.

*)
sym_type : term Timed.ref;(*

Type.

*)
sym_impl : bool list;(*

Implicit arguments (true meaning implicit).

*)
sym_prop : prop;(*

Property.

*)
sym_def : term option Timed.ref;(*

Definition with ≔.

*)
sym_opaq : bool;(*

Opacity.

*)
sym_rules : rule list Timed.ref;(*

Rewriting rules.

*)
sym_mstrat : match_strat;(*

Matching strategy.

*)
sym_dtree : dtree Timed.ref;(*

Decision tree used for matching.

*)
sym_pos : Common.Pos.popt;(*

Position in source file.

*)
}

Representation of a user-defined symbol. Symbols carry a "mode" indicating whether they may be given rewriting rules or a definition. Invariants must be enforced for "mode" consistency (see prop).

NOTE that sym_type holds a (timed) reference for a technical reason related to the writing of signatures as binary files (in relation to Sign.link and Sign.unlink). This is necessary to enforce ensure that two identical symbols are always physically equal, even across signatures. It should NOT be otherwise mutated.

NOTE we maintain the invariant that sym_impl never ends with false. Indeed, this information would be redundant. If a symbol has more arguments than there are booleans in the list then the extra arguments are all explicit. Finally, note that sym_impl is empty if and only if the symbol has no implicit parameters.

NOTE the value of the sym_prop field of symbols restricts the value of their sym_def and sym_rules fields. A symbol is not allowed to be given rewriting rules (or a definition) when its mode is set to Const. Moreover, a symbol should not be given at the same time a definition (i.e., sym_def different from None) and rewriting rules (i.e., sym_rules is non-empty).

Representation of rewriting rules

and rule = {
lhs : term list;(*

Left hand side (LHS).

*)
rhs : rhs;(*

Right hand side (RHS).

*)
arity : int;(*

Required number of arguments to be applicable.

*)
arities : int array;(*

Arities of the pattern variables bound in the RHS.

*)
vars : tevar array;(*

Bindlib variables used to build rhs. The last xvars_nb variables appear only in rhs.

*)
xvars_nb : int;(*

Number of variables in rhs but not in lhs.

*)
rule_pos : Common.Pos.popt;(*

Position of the rule in the source file.

*)
}

Representation of a rewriting rule. A rewriting rule is mainly formed of a LHS (left hand side), which is the pattern that should be matched for the rule to apply, and a RHS (right hand side) giving the action to perform if the rule applies. More explanations are given below.

The LHS (or pattern) of a rewriting rule is always formed of a head symbol (on which the rule is defined) applied to a list of pattern arguments. The list of arguments is given in lhs, but the head symbol itself is not stored in the rule, since rules are stored in symbols. In the pattern arguments of a LHS, Patt(i,s,env) is used to represent pattern variables that are identified by a name s (unique in a rewriting rule). They carry an environment env that should only contain distinct variables (terms of the form Vari(x)). They correspond to the set of all the variables that may appear free in a matched term. The optional integer i corresponds to the reserved index for the matched term in the environment of the RHS during matching.

For instance, with the rule f $X $Y $Y $Z ↪ $X:

  • $X is represented by Patt(Some 0, "X", [||]) since it occurs in the RHS of the rule (and it is actually the only one),
  • $Y is represented by Patt(Some 1, "Y", [||]) as it occurs more than once in the LHS (the rule is non-linear in this variable),
  • $Z is represented by Patt(Some 2, "Z", [||]) even though it is not bound in the RHS and it appears linearly. Note that wildcards (in the concrete syntax) are represented in the same way, and with a unique name (in the rule) that is generated automatically.

Then, the term f t u v w matches the LHS with a substitution represented by an array of terms (or rather “term environments”) a of length 3 if we have a.(0) = t, a.(1) = u, a.(1) = v and a.(2) = w.

TODO memorising w in the substitution is sub-optimal. In practice, the term matched by $Z should be ignored.

NOTE that the second parameter of the Patt constructor holds an array of terms. This is essential for variables binding: using an array of variables would NOT suffice.

NOTE that the value of the arity field (of a rewriting rule) gives the number of arguments contained in its LHS. As a consequence, the value of r.arity is always equal to List.length r.lhs and it gives the minimal number of arguments required to match the LHS of the rule.

The RHS (or action) or a rewriting rule is represented by a term, in which (higher-order) variables representing "terms with environments" (see the term_env type) are bound. To effectively apply the rewriting rule, these bound variables must be substituted using "terms with environments" that are constructed when matching the LHS of the rule.

All variables of rewriting rules that appear in the RHS must appear in the LHS. This constraint is checked in Tool.Sr.In the case of unification rules, we allow variables to appear only in the RHS. In that case, these variables are replaced by fresh meta-variables each time the rule is used. The last Term.rule.xvars_nb variables of Term.rule.vars are such RHS-only variables.

and term_env =
| TE_Vari of tevar(*

Free "term with environment" variable (used to build a RHS).

*)
| TE_Some of tmbinder(*

Actual "term with environment" (used to instantiate a RHS).

*)
| TE_None(*

Dummy term environment (used during matching).

*)

Representation of a "term with environment", which intuitively corresponds to a term with bound variables (or a "higher-order" term) represented with the TE_Some constructor. Other constructors are included so that "terms with environments" can be bound in the RHS of rewriting rules. This is purely technical.

The TEnv(te,env) constructor intuitively corresponds to a term te with free variables together with an explicit environment env. Note that the binding of the environment actually occurs in te, when the constructor is of the form TE_Some(b). Indeed, te holds a multiple binder b that binds every free variables of the term at once. We then apply the substitution by performing a Bindlib substitution of b with the environment env.

During evaluation, we only try to apply rewriting rules when we reduce the application of a symbol s to a list of argument ts. At this point, the symbol s contains every rule r that can potentially be applied in its sym_rules field. To check if a rule r applies, we match the elements of r.lhs with those of ts while building an environment env of type {!type:Term.term_env} array. During this process, a pattern of the form Patt(Some i,s,e) matched against a term u will results in env.(i) being set to u. If all terms of ts can be matched against corresponding patterns, then environment env is fully constructed and it can hence be substituted in r.rhs with Bindlib.msubst r.rhs env to get the result of the application of the rule.

and meta = {
meta_key : int;(*

Unique key.

*)
meta_type : term Timed.ref;(*

Type.

*)
meta_arity : int;(*

Arity (environment size).

*)
meta_value : tmbinder option Timed.ref;(*

Definition.

*)
}

Representation of a metavariable, which corresponds to a yet unknown term typable in some context. The substitution of the free variables of the context is suspended until the metavariable is instantiated (i.e., set to a particular term). When a metavariable m is instantiated, the suspended substitution is unlocked and terms of the form Meta(m,env) can be unfolded.

and tbinder = ( term, term ) Bindlib.binder
and tmbinder = ( term, term ) Bindlib.mbinder
and tvar = term Bindlib.var
and tevar = term_env Bindlib.var
type tbox = term Bindlib.box
type tebox = term_env Bindlib.box
val minimize_impl : bool list -> bool list

Minimize impl to enforce our invariant (see Term.sym).

module Raw : sig ... end

Basic printing function (for debug).

type ctxt = (tvar * term * term option) list

Typing context associating a Bindlib variable to a type and possibly a definition. The typing environment x1:A1,..,xn:An is represented by the list xn:An;..;x1:A1 in reverse order (last added variable comes first).

type bctxt = (tvar * tbox) list

Typing context with lifted terms. Used to optimise type checking and avoid lifting terms several times. Definitions are not included because these contexts are used to create meta variables types, which do not use let definitions.

type constr = ctxt * term * term

Type of unification constraints.

module Var : Map.OrderedType with type t = tvar

Sets and maps of term variables.

module VarSet : Set.S with type elt = tvar
module VarMap : Map.S with type key = tvar
val of_tvar : tvar -> term

of_tvar x injects the Bindlib variable x in a term.

val new_tvar : string -> tvar

new_tvar s creates a new tvar of name s.

val new_tvar_ind : string -> int -> tvar

new_tvar_ind s i creates a new tvar of name s ^ string_of_int i.

val of_tevar : tevar -> term_env

of_tevar x injects the Bindlib variable x in a term_env.

val new_tevar : string -> tevar

new_tevar s creates a new tevar with name s.

module Sym : Map.OrderedType with type t = sym

Sets and maps of symbols.

module SymSet : Set.S with type elt = sym
module SymMap : Map.S with type key = sym
val create_sym : Common.Path.t -> expo -> prop -> match_strat -> bool -> Common.Pos.strloc -> term -> bool list -> sym

create_sym path expo prop opaq name typ impl creates a new symbol with position pos, path path, exposition expo, property prop, opacity opaq, matching strategy mstrat, name name.elt, type typ, implicit arguments impl, position name.pos, no definition and no rules.

val is_constant : sym -> bool

is_constant s tells whether the symbol is a constant.

val is_injective : sym -> bool

is_injective s tells whether s is injective, which is in partiular the case if s is constant.

val is_private : sym -> bool

is_private s tells whether the symbol s is private.

val is_modulo : sym -> bool

is_modulo s tells whether the symbol s is modulo some equations.

module Meta : Map.OrderedType with type t = meta

Sets and maps of metavariables.

module MetaSet : Set.S with type elt = Meta.t
module MetaMap : Map.S with type key = Meta.t
type problem_aux = {
to_solve : constr list;(*

List of unification problems to solve.

*)
unsolved : constr list;(*

List of unification problems that could not be solved.

*)
recompute : bool;(*

Indicates whether unsolved problems should be rechecked.

*)
metas : MetaSet.t;(*

Set of unsolved metas.

*)
}

Representation of unification problems.

type problem = problem_aux Timed.ref
val new_problem : unit -> problem

Create a new empty problem.

val unfold : term -> term

unfold t repeatedly unfolds the definition of the surface constructor of t, until a significant term constructor is found. The term that is returned cannot be an instantiated metavariable, term environment or reference cell. The returned value is physically equal to t if no unfolding was performed.

NOTE that unfold must (almost) always be called before matching over a value of type term.

Total orders terms.

val is_abst : term -> bool

is_abst t returns true iff t is of the form Abst(_).

val is_prod : term -> bool

is_prod t returns true iff t is of the form Prod(_).

val is_unset : meta -> bool

is_unset m returns true if m is not instantiated.

val is_symb : sym -> term -> bool

is_symb s t tests whether t is of the form Symb(s).

val get_args : term -> term * term list

get_args t decomposes the term t into a pair (h,args), where h is the head term of t and args is the list of arguments applied to h in t. The returned h cannot be an Appl node.

val get_args_len : term -> term * term list * int

get_args_len t is similar to get_args t but it also returns the length of the list of arguments.

val mk_Vari : tvar -> term

Construction functions of the private type term. They ensure some invariants:

  • In a commutative function symbol application, the first argument is smaller than the second one wrt cmp.
  • In an associative and commutative function symbol application, the application is built as a left or right comb depending on the associativity of the symbol, and arguments are ordered in increasing order wrt cmp.
  • In LLet(_,_,b), Bindlib.binder_constant b = false (useless let's are erased).
val mk_Type : term
val mk_Kind : term
val mk_Symb : sym -> term
val mk_Prod : (term * tbinder) -> term
val mk_Abst : (term * tbinder) -> term
val mk_Appl : (term * term) -> term
val mk_Meta : (meta * term array) -> term
val mk_Patt : (int option * string * term array) -> term
val mk_TEnv : (term_env * term array) -> term
val mk_Wild : term
val mk_Plac : bool -> term
val mk_TRef : term option Timed.ref -> term
val mk_LLet : (term * term * tbinder) -> term
val mk_Appl_not_canonical : (term * term) -> term

mk_Appl_not_canonical t u builds the non-canonical (wrt. C and AC symbols) application of t to u. WARNING: to use only in Sign.link.

val add_args : term -> term list -> term

add_args t args builds the application of the term t to a list arguments args. When args is empty, the returned value is (physically) equal to t.

val add_args_map : term -> ( term -> term ) -> term list -> term

add_args_map f t ts is equivalent to add_args t (List.map f ts) but more efficient.

Smart constructors and lifting (related to Bindlib)

val _Vari : tvar -> tbox

_Vari x injects the free variable x into the tbox type so that it may be available for binding.

val _Type : tbox

_Type injects the constructor Type into the tbox type.

val _Kind : tbox

_Kind injects the constructor Kind into the tbox type.

val _Symb : sym -> tbox

_Symb s injects the constructor Symb(s) into the tbox type. As symbols are closed object they do not require lifting.

val _Appl : tbox -> tbox -> tbox

_Appl t u lifts an application node to the tbox type given boxed terms t and u.

val _Appl_not_canonical : tbox -> tbox -> tbox

_Appl_not_canonical t u lifts an application node to the tbox type given boxed terms t and u, without putting it in canonical form wrt. C and AC symbols. WARNING: to use in scoping of rewrite rule LHS only as it breaks some invariants.

val _Appl_list : tbox -> tbox list -> tbox

_Appl_list a [b1;...;bn] returns (... ((a b1) b2) ...) bn.

val _Appl_Symb : sym -> tbox list -> tbox

_Appl_Symb f ts returns the same result that _Appl_l ist (_Symb f) ts.

val _Prod : tbox -> tbinder Bindlib.box -> tbox

_Prod a b lifts a dependent product node to the tbox type, given a boxed term a for the domain of the product, and a boxed binder b for its codomain.

val _Impl : tbox -> tbox -> tbox
val _Abst : tbox -> tbinder Bindlib.box -> tbox

_Abst a t lifts an abstraction node to the tbox type, given a boxed term a for the domain type, and a boxed binder t.

val _Meta : meta -> tbox array -> tbox

_Meta m ar lifts the metavariable m to the tbox type given its environment ar. As for symbols in _Symb, metavariables are closed objects so they do not require lifting.

val _Meta_full : meta Bindlib.box -> tbox array -> tbox

_Meta_full m ar is similar to _Meta m ar but works with a metavariable that is boxed. This is useful in very rare cases, when metavariables need to be able to contain free term environment variables. Using this function in bad places is harmful for efficiency but not unsound.

val _Patt : int option -> string -> tbox array -> tbox

_Patt i n ar lifts a pattern variable to the tbox type.

val _TEnv : tebox -> tbox array -> tbox

_TEnv te ar lifts a term environment to the tbox type.

val _Wild : tbox

_Wild injects the constructor Wild into the tbox type.

val _Plac : bool -> tbox

_Plac injects the constructor Plac into the tbox type.

val _TRef : term option Timed.ref -> tbox

_TRef r injects the constructor TRef(r) into the tbox type. It should be the case that !r is None.

val _LLet : tbox -> tbox -> tbinder Bindlib.box -> tbox

_LVal t a u lifts val binding val x := t : a in u<x>.

val _TE_Vari : tevar -> tebox

_TE_Vari x injects a term environment variable x into the tbox type so that it may be available for binding.

val _TE_None : tebox

_TE_None injects the constructor TE_None into the tbox type.

val lift : term -> tbox

lift t lifts the term t to the tbox type. This has the effect of gathering its free variables, making them available for binding. Bound variable names are automatically updated in the process.

val lift_not_canonical : term -> tbox
val bind : tvar -> ( term -> tbox ) -> term -> tbinder

bind v lift t creates a tbinder by binding v in lift t.

val binds : tvar array -> ( term -> tbox ) -> term -> tmbinder
val cleanup : ?ctxt:Bindlib.ctxt -> term -> term

cleanup ~ctxt t builds a copy of the term t where every instantiated metavariable, instantiated term environment, and reference cell has been eliminated using unfold. Another effect of the function is that the names of bound variables are updated and taken away from ctxt. This is useful to avoid any form of "visual capture" while printing terms.

type subterm_pos = int list

Positions in terms in reverse order. The i-th argument of a constructor has position i-1.

val subterm_pos : subterm_pos Lplib.Base.pp
type cp_pos = Common.Pos.popt * term * term * subterm_pos * term

Type of critical pair positions (pos,l,r,p,l_p).

val term_of_rhs : rule -> term

term_of_rhs r converts the RHS (right hand side) of the rewriting rule r into a term. The bound higher-order variables of the original RHS are substituted using Patt constructors. They are thus represented as their LHS counterparts. This is a more convenient way of representing terms when analysing confluence or termination.

type sym_rule = sym * rule

Type of a symbol and a rule.

val lhs : sym_rule -> term
val rhs : sym_rule -> term