Module Core.TermSource
Internal representation of terms.
This module contains the definition of the internal representation of terms, together with smart constructors and low level operation.
Term (and symbol) representation
Representation of a possibly qualified identifier.
Sourcetype match_strat = | SequenRules are processed sequentially: a rule can be applied only if the previous ones (in the order of declaration) cannot be.
| EagerAny 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.
Sourcetype expo = | PublicVisible and usable everywhere.
| ProtecVisible everywhere but usable in LHS arguments only.
| PrivatNot visible and thus not usable.
Specify the visibility and usability of symbols outside their module.
Sourcetype prop = | Defin| Const| Injec| Commu| Assoc of boolAssociative left if true, right if false.
| AC of boolAssociative and commutative.
The priority of an infix operator is a floating-point number.
Sourcetype 'a notation = | NoNotation| Prefix of 'a| Postfix of 'a| Infix of Pratter.associativity * 'a| Zero| Succ of 'a notation| Quant| PosOne| PosDouble| PosSuccDouble| IntZero| IntPos| IntNeg
Sourcetype term = private | Vari of var| Bvar of bvarBound variables. Only used internally.
| Type| Kind| Symb of sym| Prod of term * binder| Abst of term * binder| Appl of term * term| Meta of meta * term arrayMetavariable application.
| Patt of int option * string * term arrayPattern variable application (only used in rewriting rules).
| WildWildcard (only used for surface matching, never in LHS).
| Plac of boolPlac 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.refReference cell (used in surface matching).
| LLet of term * term * binderLLet(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 context. 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 decision tree (used for rewriting).
Sourceand sym = {sym_expo : expo;sym_path : Common.Path.t;Module in which the symbol is defined.
sym_name : string;sym_type : term Timed.ref;sym_impl : bool list;Implicit arguments (true meaning implicit).
sym_prop : prop;sym_nota : float notation Timed.ref;sym_def : term option Timed.ref;sym_opaq : bool Timed.ref;sym_rules : rule list Timed.ref;sym_mstrat : match_strat;sym_dtree : dtree Timed.ref;Decision tree used for matching.
sym_pos : Common.Pos.popt;Position in source file of symbol name.
sym_decl_pos : Common.Pos.popt;Position in source file of symbol declaration without its definition.
} Representation of a user-defined symbol.
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
Sourceand rule = {lhs : term list;names : string array;Names of pattern variables.
rhs : term;arity : int;Required number of arguments to be applicable.
arities : int array;Arities of the pattern variables bound in the RHS.
vars_nb : int;Number of variables in lhs.
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,ts) is used to represent pattern variables that are identified by a name s (unique in a rewriting rule). They carry an environment ts 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 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.
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.
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. During this process, a pattern of the form Patt(Some i,_,_) 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 msubst r.rhs env to get the result of the application of the rule.
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.
binder_name b gives the name of the bound variable of b.
mbinder_names b gives the names of the bound variables of b.
mbinder_arity b gives the arity of the mbinder.
Sourceval minimize_impl : bool list -> bool list Minimize impl to enforce our invariant (see Term.sym).
create_sym path expo prop mstrat opaq name pos typ impl creates a new symbol with path path, exposition expo, property prop, opacity opaq, matching strategy mstrat, name name.elt, type typ, implicit arguments impl, position name.pos, declaration position pos, no definition and no rules.
is_constant s tells whether the symbol is a constant.
is_injective s tells whether s is injective, which is in partiular the case if s is constant.
is_private s tells whether the symbol s is private.
is_modulo s tells whether the symbol s is modulo some equations.
Sets and maps of symbols.
compare_vars x y safely compares x and y. Note that it is unsafe to compare variables using Pervasive.compare.
eq_vars x y safely computes the equality of x and y. Note that it is unsafe to compare variables with the polymorphic equality function.
new_var s creates a new var of name s.
new_var_ind s i creates a new var of name s ^ string_of_int i.
base_name x returns the base name of the variable x. Note that this base name is not unique: two distinct variables may have the same name.
uniq_name x returns a string uniquely identifying the variable x.
Sets and maps of term variables.
is_unset m returns true if m is not instantiated.
Sets and maps of metavariables.
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.
is_abst t returns true iff t is of the form Abst(_).
is_prod t returns true iff t is of the form Prod(_).
is_tref t returns true iff t is of the form TRef _.
is_symb s t tests whether t is of the form Symb(s).
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.
get_args_len t is similar to get_args t but it also returns the length of the list of arguments.
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), binder_occur b = true (useless let's are erased).
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.
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.
add_args_map f t ts is equivalent to add_args t (List.map f ts) but more efficient.
subst b v substitutes the variable bound by b with the value v.
msubst b vs substitutes the variables bound by b with the values vs. Note that the length of the vs array should match the arity of the multiple binder b.
unbind b substitutes the binder b by a fresh variable of name name if given, or the binder name otherwise. The variable and the result of the substitution are returned.
unbind2 f g is similar to unbind f, but it substitutes two binders f and g at once using the same fresh variable.
unmbind b substitutes the multiple binder b with fresh variables. This function is analogous to unbind for binders. Note that the names used to create the fresh variables are based on those of the multiple binder.
bind_var x b binds the variable x in b, producing a boxed binder.
binder f b applies f inside b.
bind_mvar xs b binds the variables of xs in b to get a boxed binder. It is the equivalent of bind_var for multiple variables.
binder_occur b tests whether the bound variable occurs in b.
is_closed b checks whether the term b is closed.
occur x b tells whether variable x occurs in the box b.
cleanup t unfold all metas and TRef's in t.
Typing context associating a 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 of unification constraints.
Sourcetype 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;
} Representation of unification problems.
Create a new empty problem.
Sourcetype subterm_pos = int list Positions in terms in reverse order. The i-th argument of a constructor has position i-1.
Type of critical pair positions (pos,l,r,p,l_p).
Type of a symbol and a rule.
Basic printing function (for debug).