##### https://github.com/Deducteam/lambdapi

Tip revision:

**a7717902b83d9b4ef8a1bf7d4b0ae43aa30585aa**authored by**Frédéric Blanqui**on**19 May 2022, 08:09:55 UTC****fix code for why3 1.5.0 (#867)** Tip revision:

**a771790**term.ml

```
(** Internal representation of terms.
This module contains the definition of the internal representation of
terms, together with smart constructors and low level operation. The
representation strongly relies on the {!module:Bindlib} library, which
provides a convenient abstraction to work with binders.
@see <https://rlepigre.github.io/ocaml-bindlib/> *)
open Timed
open Lplib open Base
open Common open Debug
let log_term = Logger.make 'm' "term" "term building"
let log_term = log_term.pp
(** {3 Term (and symbol) representation} *)
(** Representation of a possibly qualified identifier. *)
type qident = Path.t * string
(** Pattern-matching strategy modifiers. *)
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. *)
(** Specify the visibility and usability of symbols outside their module. *)
type expo =
| Public (** Visible and usable everywhere. *)
| Protec (** Visible everywhere but usable in LHS arguments only. *)
| Privat (** Not visible and thus not usable. *)
(** Symbol properties. *)
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. *)
(** 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. *)
type term =
| 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
| Plac of bool
| TRef of term option 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]). *)
(** {b NOTE} that a wildcard "_" of the concrete (source code) syntax may have
a different representation depending on the application. For instance, the
{!constructor:Wild} constructor is only used when matching patterns (e.g.,
with the "rewrite" tactic). In the LHS of a rewriting {!type:rule}, we use
the {!constructor: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 {!field:Term.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 rhs = (term_env, term) Bindlib.mbinder
(** Representation of a decision tree (used for rewriting). *)
and dtree = (rhs * int) Tree_type.dtree
(** 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 {!type:sym_prop}). *)
and sym =
{ sym_expo : expo (** Visibility. *)
; sym_path : Path.t (** Module in which the symbol is defined. *)
; sym_name : string (** Name. *)
; sym_type : term ref (** Type. *)
; sym_impl : bool list (** Implicit arguments ([true] meaning implicit). *)
; sym_prop : prop (** Property. *)
; sym_def : term option ref (** Definition with ≔. *)
; sym_opaq : bool (** Opacity. *)
; sym_rules : rule list ref (** Rewriting rules. *)
; sym_mstrat: match_strat (** Matching strategy. *)
; sym_dtree : dtree ref (** Decision tree used for matching. *)
; sym_pos : Pos.popt (** Position in source file. *) }
(** {b NOTE} {!field:sym_type} holds a (timed) reference for a technical
reason related to the writing of signatures as binary files (in relation
to {!val:Sign.link} and {!val:Sign.unlink}). This is necessary to
ensure that two identical symbols are always physically equal, even across
signatures. It should NOT be otherwise mutated. *)
(** {b NOTE} We maintain the invariant that {!field: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 {!field:sym_impl} is empty if and only if
the symbol has no implicit parameters. *)
(** {b NOTE} {!field:sym_prop} restricts the possible
values of {!field:sym_def} and {!field:sym_rules} fields. A symbol is
not allowed to be given rewriting rules (or a definition) when its mode is
set to {!constructor:Constant}. Moreover, a symbol should not be given at
the same time a definition (i.e., {!field:sym_def} different from [None])
and rewriting rules (i.e., {!field:sym_rules} is non-empty). *)
(** {b NOTE} For generated symbols (recursors, axioms), {!field:sym_pos} may
not be valid positions in the source. These virtual positions are however
important for exporting lambdapi files to other formats. *)
(** {3 Representation of rewriting rules} *)
(** 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. *)
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 : Pos.popt (** Position of the rule in the source file. *) }
(** {b NOTE} The second parameter of {!constructor:Patt} holds an array of
terms. This is essential for variables binding: using an array of variables
would NOT suffice. *)
(** {b NOTE} {!field:arity} gives the number of arguments contained in the
LHS. As a consequence, it is always equal to [List.length r.lhs] and it
gives the minimal number of arguments required to match the LHS. *)
(** {b NOTE} For generated rules, {!field:rule_pos} may not be valid positions
in the source. These virtual positions are however important for exporting
lambdapi files to other formats. *)
(** The RHS (or action) or a rewriting rule is represented by a term, in which
(higher-order) variables representing "terms with environments" (see the
{!type: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 {!module: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 {!field:terms.rule.xvars} variables of {!field:terms.rule.vars}
are such RHS-only variables. *)
(** Representation of a "term with environment", which intuitively corresponds
to a term with bound variables (or a "higher-order" term) represented with
the {!constructor: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. *)
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). *)
(** The {!constructor: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 {!constructor: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
{!field: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_env array}. During this process, a pattern of the form
{!constructor: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. *)
(** {3 Metavariables and related functions} *)
(** 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 {!constructor:Meta}[(m,env)] can be unfolded. *)
and meta =
{ meta_key : int (** Unique key. *)
; meta_type : term ref (** Type. *)
; meta_arity : int (** Arity (environment size). *)
; meta_value : tmbinder option ref (** Definition. *) }
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
(** Minimize [impl] to enforce our invariant (see {!type:Terms.sym}). *)
let minimize_impl : bool list -> bool list =
let rec rem_false l = match l with false::l -> rem_false l | _ -> l in
fun l -> List.rev (rem_false (List.rev l))
(** Printing functions for debug. *)
module Raw = struct
let rec term : term pp = fun ppf t ->
match t with
| Vari v -> var ppf v
| Type -> out ppf "TYPE"
| Kind -> out ppf "KIND"
| Symb s -> sym ppf s
| Prod(a,b) ->
if Bindlib.binder_constant b then
let _, b = Bindlib.unbind b in out ppf "(%a → %a)" term a term b
else out ppf "(Π %a)" binder (a,b)
| Abst(a,b) -> out ppf "(λ %a)" binder (a,b)
| Appl(a,b) -> out ppf "(%a %a)" term a term b
| Meta(m,ts) -> out ppf "?%a%a" meta m terms ts
| Patt(i,s,ts) -> out ppf "$%a_%s%a" (D.option D.int) i s terms ts
| Plac(_) -> out ppf "_"
| TEnv(te,ts) -> out ppf "<%a>%a" tenv te terms ts
| Wild -> out ppf "_"
| TRef r -> out ppf "&%a" (Option.pp term) !r
| LLet(a,t,u) ->
let x, u = Bindlib.unbind u in
out ppf "let %a: %a ≔ %a in %a" var x term a term t term u
and terms : term array pp = fun ppf ts ->
(*if Array.length ts > 0 then*) D.array term ppf ts
and var : tvar pp = fun ppf v -> out ppf "%s" (Bindlib.name_of v)
and binder : (term * tbinder) pp = fun ppf (a,b) ->
let x, b = Bindlib.unbind b in
out ppf "%a: %a, %a" var x term a term b
and meta : meta pp = fun ppf m ->
out ppf "%d" m.meta_key
and sym : sym pp = fun ppf s -> out ppf "%s" s.sym_name
and tenv : term_env pp = fun ppf te ->
match te with
| TE_Vari v -> out ppf "%s" (Bindlib.name_of v)
| TE_Some mb ->
let vs, b = Bindlib.unmbind mb in
out ppf "%a,%a" (D.array var) vs term b
| TE_None -> ()
end
(** 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 ctxt = (tvar * term * term option) 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 bctxt = (tvar * tbox) list
(** Type of unification constraints. *)
type constr = ctxt * term * term
(** Sets and maps of term variables. *)
module Var = struct
type t = tvar
let compare = Bindlib.compare_vars
end
module VarSet = Set.Make(Var)
module VarMap = Map.Make(Var)
(** [of_tvar x] injects the [Bindlib] variable [x] in a term. *)
let of_tvar : tvar -> term = fun x -> Vari(x)
(** [new_tvar s] creates a new [tvar] of name [s]. *)
let new_tvar : string -> tvar = Bindlib.new_var of_tvar
(** [new_tvar_ind s i] creates a new [tvar] of name [s ^ string_of_int i]. *)
let new_tvar_ind : string -> int -> tvar = fun s i ->
new_tvar (Escape.add_prefix s (string_of_int i))
(** [of_tevar x] injects the [Bindlib] variable [x] in a {!type:term_env}. *)
let of_tevar : tevar -> term_env = fun x -> TE_Vari(x)
(** [new_tevar s] creates a new [tevar] with name [s]. *)
let new_tevar : string -> tevar = Bindlib.new_var of_tevar
(** Sets and maps of symbols. *)
module Sym = struct
type t = sym
let compare s1 s2 =
if s1 == s2 then 0 else
match Stdlib.compare s1.sym_name s2.sym_name with
| 0 -> Stdlib.compare s1.sym_path s2.sym_path
| n -> n
end
module SymSet = Set.Make(Sym)
module SymMap = Map.Make(Sym)
(** Sets and maps of metavariables. *)
module Meta = struct
type t = meta
let compare m1 m2 = m2.meta_key - m1.meta_key
end
module MetaSet = Set.Make(Meta)
module MetaMap = Map.Make(Meta)
(** Representation of unification problems. *)
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. *) }
type problem = problem_aux ref
(** Create a new empty problem. *)
let new_problem : unit -> problem = fun () ->
ref {to_solve = []; unsolved = []; recompute = false; metas = MetaSet.empty}
(** [create_sym path expo prop opaq name 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], no definition and no rules. *)
let create_sym : Path.t -> expo -> prop -> match_strat -> bool ->
Pos.strloc -> term -> bool list -> sym =
fun sym_path sym_expo sym_prop sym_mstrat sym_opaq
{ elt = sym_name; pos = sym_pos } typ sym_impl ->
{sym_path; sym_name; sym_type = ref typ; sym_impl; sym_def = ref None;
sym_opaq; sym_rules = ref []; sym_dtree = ref Tree_type.empty_dtree;
sym_mstrat; sym_prop; sym_expo; sym_pos }
(** [is_constant s] tells whether [s] is a constant. *)
let is_constant : sym -> bool = fun s -> s.sym_prop = Const
(** [is_injective s] tells whether [s] is injective, which is in partiular the
case if [s] is constant. *)
let is_injective : sym -> bool = fun s ->
match s.sym_prop with Const | Injec -> true | _ -> false
(** [is_private s] tells whether the symbol [s] is private. *)
let is_private : sym -> bool = fun s -> s.sym_expo = Privat
(** [is_modulo s] tells whether the symbol [s] is modulo some equations. *)
let is_modulo : sym -> bool = fun s ->
match s.sym_prop with Assoc _ | Commu | AC _ -> true | _ -> false
(** [unfold t] repeatedly unfolds the definition of the surface constructor of
[t], until a significant {!type:term} constructor is found. The term that
is returned cannot be an instantiated metavariable or term environment nor
a reference cell ({!constructor:TRef} constructor). Note that the returned
value is physically equal to [t] if no unfolding was performed. *)
let rec unfold : term -> term = fun t ->
match t with
| Meta(m, ts) ->
begin
match !(m.meta_value) with
| None -> t
| Some(b) -> unfold (Bindlib.msubst b ts)
end
| TRef(r) ->
begin
match !r with
| None -> t
| Some(v) -> unfold v
end
| _ -> t
(** {b NOTE} that {!val:unfold} must (almost) always be called before matching
over a value of type {!type:term}. *)
(** [is_abst t] returns [true] iff [t] is of the form [Abst(_)]. *)
let is_abst : term -> bool = fun t ->
match unfold t with Abst(_) -> true | _ -> false
(** [is_prod t] returns [true] iff [t] is of the form [Prod(_)]. *)
let is_prod : term -> bool = fun t ->
match unfold t with Prod(_) -> true | _ -> false
(** [is_unset m] returns [true] if [m] is not instantiated. *)
let is_unset : meta -> bool = fun m -> !(m.meta_value) = None
(** [is_symb s t] tests whether [t] is of the form [Symb(s)]. *)
let is_symb : sym -> term -> bool = fun s t ->
match unfold t with Symb(r) -> r == s | _ -> false
(** Total order on terms. *)
let cmp : term cmp =
let rec cmp t t' =
match unfold t, unfold t' with
| Vari x, Vari x' -> Bindlib.compare_vars x x'
| Type, Type
| Kind, Kind
| Wild, Wild -> 0
| Symb s, Symb s' -> Sym.compare s s'
| Prod(t,u), Prod(t',u')
| Abst(t,u), Abst(t',u') -> lex cmp cmp_binder (t,u) (t',u')
| Appl(t,u), Appl(t',u') -> lex cmp cmp (u,t) (u',t')
| Meta(m,ts), Meta(m',ts') ->
lex Meta.compare (Array.cmp cmp) (m,ts) (m',ts')
| Patt(i,s,ts), Patt(i',s',ts') ->
lex3 Stdlib.compare Stdlib.compare (Array.cmp cmp)
(i,s,ts) (i',s',ts')
| TEnv(e,ts), TEnv(e',ts') ->
lex cmp_tenv (Array.cmp cmp) (e,ts) (e',ts')
| TRef r, TRef r' -> Stdlib.compare r r'
| LLet(a,t,u), LLet(a',t',u') ->
lex3 cmp cmp cmp_binder (a,t,u) (a',t',u')
| t, t' -> cmp_tag (*cmp_map Stdlib.compare prec*) t t'
and cmp_binder t t' = let (_,t,t') = Bindlib.unbind2 t t' in cmp t t'
and cmp_mbinder t t' = let (_,t,t') = Bindlib.unmbind2 t t' in cmp t t'
and cmp_tenv e e' =
match e, e' with
| TE_Vari v, TE_Vari v' -> Bindlib.compare_vars v v'
| TE_None, TE_None -> 0
| TE_Some t, TE_Some t' -> cmp_mbinder t t'
| _ -> cmp_tag (*cmp_map Stdlib.compare prec_tenv*) e e'
in cmp
(** [get_args t] decomposes the {!type: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. *)
let get_args : term -> term * term list = fun t ->
let rec get_args t acc =
match unfold t with
| Appl(t,u) -> get_args t (u::acc)
| t -> t, acc
in get_args t []
(** [get_args_len t] is similar to [get_args t] but it also returns the length
of the list of arguments. *)
let get_args_len : term -> term * term list * int = fun t ->
let rec get_args_len acc len t =
match unfold t with
| Appl(t, u) -> get_args_len (u::acc) (len + 1) t
| t -> (t, acc, len)
in
get_args_len [] 0 t
(** 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). *)
let mk_Vari x = Vari x
let mk_Type = Type
let mk_Kind = Kind
let mk_Symb x = Symb x
let mk_Prod (a,b) = Prod (a,b)
let mk_Abst (a,b) = Abst (a,b)
let mk_Meta (m,ts) = Meta (m,ts)
let mk_Patt (i,s,ts) = Patt (i,s,ts)
let mk_Wild = Wild
let mk_Plac b = Plac b
let mk_TRef x = TRef x
let mk_LLet (a,t,u) =
if Bindlib.binder_constant u then Bindlib.subst u Kind else LLet (a,t,u)
let mk_TEnv (te,ts) =
match te with
| TE_Some mb -> Bindlib.msubst mb ts
| _ -> TEnv (te,ts)
(* We make the equality of terms modulo commutative and
associative-commutative symbols syntactic by always ordering arguments in
increasing order and by putting them in a comb form.
The term [t1 + t2 + t3] is represented by the left comb [(t1 + t2) + t3] if
+ is left associative and [t1 + (t2 + t3)] if + is right associative. *)
let mk_bin s t1 t2 = Appl(Appl(Symb s, t1), t2)
(** [mk_left_comb s t ts] builds a left comb of applications of [s] from
[t::ts] so that [mk_left_comb s t1 [t2; t3] = mk_bin s (mk_bin s t1 t2)
t3]. *)
let mk_left_comb : sym -> term -> term list -> term = fun s ->
List.fold_left (mk_bin s)
(** [mk_right_comb s ts t] builds a right comb of applications of [s] to
[ts@[p]] so that [mk_right_comb s [t1; t2] t3 = mk_bin s t1 (mk_bin s t2
t3)]. *)
let mk_right_comb : sym -> term list -> term -> term = fun s ->
List.fold_right (mk_bin s)
(** [left_aliens s t] returns the list of the biggest subterms of [t] not
headed by [s], assuming that [s] is left associative and [t] is in
canonical form. This is the reverse of [mk_left_comb]. *)
let left_aliens : sym -> term -> term list = fun s ->
let rec aliens acc = function
| [] -> acc
| u::us ->
let h, ts = get_args u in
if is_symb s h then
match ts with
| t1 :: t2 :: _ -> aliens (t2 :: acc) (t1 :: us)
| _ -> aliens (u :: acc) us
else aliens (u :: acc) us
in fun t -> aliens [] [t]
(** [right_aliens s t] returns the list of the biggest subterms of [t] not
headed by [s], assuming that [s] is right associative and [t] is in
canonical form. This is the reverse of [mk_right_comb]. *)
let right_aliens : sym -> term -> term list = fun s ->
let rec aliens acc = function
| [] -> acc
| u::us ->
let h, ts = get_args u in
if is_symb s h then
match ts with
| t1 :: t2 :: _ -> aliens (t1 :: acc) (t2 :: us)
| _ -> aliens (u :: acc) us
else aliens (u :: acc) us
in fun t -> let r = aliens [] [t] in
if Logger.log_enabled () then
log_term "right_aliens %a %a = %a"
Raw.sym s Raw.term t (D.list Raw.term) r;
r
(* unit test *)
let _ =
let s = create_sym [] Privat (AC true) Eager false (Pos.none "+") Kind [] in
let t1 = Vari (new_tvar "x1") in
let t2 = Vari (new_tvar "x2") in
let t3 = Vari (new_tvar "x3") in
let left = mk_bin s (mk_bin s t1 t2) t3 in
let right = mk_bin s t1 (mk_bin s t2 t3) in
let eq = eq_of_cmp cmp in
assert (eq (mk_left_comb s t1 [t2; t3]) left);
assert (eq (mk_right_comb s [t1; t2] t3) right);
let eq = eq_of_cmp (List.cmp cmp) in
assert (eq (left_aliens s left) [t1; t2; t3]);
assert (eq (right_aliens s right) [t3; t2; t1])
(** [mk_Appl t u] puts the application of [t] to [u] in canonical form wrt C
or AC symbols. *)
let mk_Appl : term * term -> term = fun (t, u) ->
(* if Logger.log_enabled () then
log_term "mk_Appl(%a, %a)" term t term u;
let r = *)
match get_args t with
| Symb s, [t1] ->
begin
match s.sym_prop with
| Commu when cmp t1 u > 0 -> mk_bin s u t1
| AC true -> (* left associative symbol *)
let ts = left_aliens s t1 and us = left_aliens s u in
begin
match List.sort cmp (ts @ us) with
| v::vs -> mk_left_comb s v vs
| _ -> assert false
end
| AC false -> (* right associative symbol *)
let ts = right_aliens s t1 and us = right_aliens s u in
let vs, v = List.split_last (List.sort cmp (ts @ us))
in mk_right_comb s vs v
| _ -> Appl (t, u)
end
| _ -> Appl (t, u)
(* in
if Logger.log_enabled () then
log_term "mk_Appl(%a, %a) = %a" term t term u term r;
r *)
(** 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. *)
let mk_Appl_not_canonical : term * term -> term = fun (t, u) -> Appl(t, u)
(** [add_args t args] builds the application of the {!type:term} [t] to a list
arguments [args]. When [args] is empty, the returned value is (physically)
equal to [t]. *)
let add_args : term -> term list -> term = fun t ts ->
List.fold_left (fun t u -> mk_Appl(t,u)) t ts
(** [add_args_map f t ts] is equivalent to [add_args t (List.map f ts)] but
more efficient. *)
let add_args_map : term -> (term -> term) -> term list -> term = fun t f ts ->
List.fold_left (fun t u -> mk_Appl(t, f u)) t ts
(** {3 Smart constructors and lifting (related to [Bindlib])} *)
(** [_Vari x] injects the free variable [x] into the {!type:tbox} type so that
it may be available for binding. *)
let _Vari : tvar -> tbox = Bindlib.box_var
(** [_Type] injects the constructor [Type] into the {!type:tbox} type. *)
let _Type : tbox = Bindlib.box Type
(** [_Kind] injects the constructor [Kind] into the {!type:tbox} type. *)
let _Kind : tbox = Bindlib.box Kind
(** [_Symb s] injects the constructor [Symb(s)] into the {!type:tbox} type. As
symbols are closed object they do not require lifting. *)
let _Symb : sym -> tbox = fun s -> Bindlib.box (Symb s)
(** [_Appl t u] lifts an application node to the {!type:tbox} type given boxed
terms [t] and [u]. *)
let _Appl : tbox -> tbox -> tbox =
Bindlib.box_apply2 (fun t u -> mk_Appl (t,u))
(** [_Appl_not_canonical t u] lifts an application node to the {!type: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. *)
let _Appl_not_canonical : tbox -> tbox -> tbox =
Bindlib.box_apply2 (fun t u -> Appl (t,u))
(** [_Appl_list a [b1;...;bn]] returns (... ((a b1) b2) ...) bn. *)
let _Appl_list : tbox -> tbox list -> tbox = List.fold_left _Appl
(** [_Appl_Symb f ts] returns the same result that
_Appl_l ist (_Symb [f]) [ts]. *)
let _Appl_Symb : sym -> tbox list -> tbox = fun f ts ->
_Appl_list (_Symb f) ts
(** [_Prod a b] lifts a dependent product node to the {!type:tbox} type, given
a boxed term [a] for the domain of the product, and a boxed binder [b] for
its codomain. *)
let _Prod : tbox -> tbinder Bindlib.box -> tbox =
Bindlib.box_apply2 (fun a b -> Prod(a,b))
let _Impl : tbox -> tbox -> tbox =
let v = new_tvar "_" in fun a b -> _Prod a (Bindlib.bind_var v b)
(** [_Abst a t] lifts an abstraction node to the {!type:tbox} type, given a
boxed term [a] for the domain type, and a boxed binder [t]. *)
let _Abst : tbox -> tbinder Bindlib.box -> tbox =
Bindlib.box_apply2 (fun a t -> Abst(a,t))
(** [_Meta m ts] lifts the metavariable [m] to the {!type:tbox} type given its
environment [ts]. As for symbols in {!val:_Symb}, metavariables are closed
objects so they do not require lifting. *)
let _Meta : meta -> tbox array -> tbox = fun m ts ->
Bindlib.box_apply (fun ts -> Meta(m,ts)) (Bindlib.box_array ts)
(** [_Meta_full m ts] is similar to [_Meta m ts] 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. *)
let _Meta_full : meta Bindlib.box -> tbox array -> tbox = fun m ts ->
Bindlib.box_apply2 (fun m ts -> Meta(m,ts)) m (Bindlib.box_array ts)
(** [_Patt i n ts] lifts a pattern variable to the {!type:tbox} type. *)
let _Patt : int option -> string -> tbox array -> tbox = fun i n ts ->
Bindlib.box_apply (fun ts -> Patt(i,n,ts)) (Bindlib.box_array ts)
(** [_TEnv te ts] lifts a term environment to the {!type:tbox} type. *)
let _TEnv : tebox -> tbox array -> tbox = fun te ts ->
Bindlib.box_apply2 (fun te ts -> mk_TEnv(te,ts)) te (Bindlib.box_array ts)
(** [_Wild] injects the constructor [Wild] into the {!type:tbox} type. *)
let _Wild : tbox = Bindlib.box Wild
let _Plac : bool -> tbox = fun b ->
Bindlib.box (mk_Plac b)
(** [_TRef r] injects the constructor [TRef(r)] into the {!type:tbox} type. It
should be the case that [!r] is [None]. *)
let _TRef : term option ref -> tbox = fun r ->
Bindlib.box (TRef(r))
(** [_LLet t a u] lifts let binding [let x := t : a in u<x>]. *)
let _LLet : tbox -> tbox -> tbinder Bindlib.box -> tbox =
Bindlib.box_apply3 (fun a t u -> mk_LLet(a, t, u))
(** [_TE_Vari x] injects a term environment variable [x] into the {!type:tbox}
type so that it may be available for binding. *)
let _TE_Vari : tevar -> tebox = Bindlib.box_var
(** [_TE_None] injects the constructor [TE_None] into the {!type:tbox} type.*)
let _TE_None : tebox = Bindlib.box TE_None
(** [lift mk_appl t] lifts the {!type:term} [t] to the type {!type:tbox},
using the function [mk_appl] in the case of an application. This has the
effect of gathering its free variables, making them available for binding.
Bound variable names are automatically updated in the process. *)
let lift : (tbox -> tbox -> tbox) -> term -> tbox = fun mk_appl ->
let rec lift t =
match unfold t with
| Vari x -> _Vari x
| Type -> _Type
| Kind -> _Kind
| Symb _ -> Bindlib.box t
| Prod(a,b) -> _Prod (lift a) (lift_binder b)
| Abst(a,t) -> _Abst (lift a) (lift_binder t)
| Appl(t,u) -> mk_appl (lift t) (lift u)
| Meta(r,m) -> _Meta r (Array.map lift m)
| Patt(i,n,m) -> _Patt i n (Array.map lift m)
| TEnv(te,m) -> _TEnv (lift_term_env te) (Array.map lift m)
| Wild -> _Wild
| Plac b -> _Plac b
| TRef r -> _TRef r
| LLet(a,t,u) -> _LLet (lift a) (lift t) (lift_binder u)
(* We do not use [Bindlib.box_binder] here because it is possible for a free
variable to disappear from a term through metavariable instantiation. As
a consequence we must traverse the whole term, even when we find a closed
binder, so that the metadata on nested binders is also updated. *)
and lift_binder b =
let x, t = Bindlib.unbind b in Bindlib.bind_var x (lift t)
and lift_term_env : term_env -> tebox = function
| TE_Vari x -> _TE_Vari x
| TE_None -> _TE_None
| TE_Some _ -> assert false (* Unreachable. *)
in lift
(** [lift t] lifts the {!type:term} [t] to the type {!type:tbox}. This has the
effect of gathering its free variables, making them available for binding.
Bound variable names are automatically updated in the process. *)
let lift = lift _Appl
and lift_not_canonical = lift _Appl_not_canonical
(** [bind v lift t] creates a tbinder by binding [v] in [lift t]. *)
let bind : tvar -> (term -> tbox) -> term -> tbinder =
fun v lift t -> Bindlib.unbox (Bindlib.bind_var v (lift t))
let binds : tvar array -> (term -> tbox) -> term -> tmbinder =
fun vs lift t -> Bindlib.unbox (Bindlib.bind_mvar vs (lift t))
(** [cleanup t] builds a copy of the {!type:term} [t] where every instantiated
metavariable, instantiated term environment, and reference cell has been
eliminated using {!val:unfold}. Another effect of the function is that the
the names of bound variables are updated. This is useful to avoid any form
of "visual capture" while printing terms. *)
let cleanup : term -> term = fun t -> Bindlib.unbox (lift_not_canonical t)
(** Positions in terms in reverse order. The i-th argument of a constructor
has position i-1. *)
type subterm_pos = int list
let subterm_pos : subterm_pos pp = fun ppf l -> D.(list int) ppf (List.rev l)
(** Type of critical pair positions (pos,l,r,p,l_p). *)
type cp_pos = Pos.popt * term * term * subterm_pos * 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. *)
let term_of_rhs : rule -> term = fun r ->
let fn i x =
let (name, arity) = (Bindlib.name_of x, r.arities.(i)) in
let vars = Array.init arity (new_tvar_ind "x") in
let p = _Patt (Some i) name (Array.map _Vari vars) in
TE_Some(Bindlib.unbox (Bindlib.bind_mvar vars p))
in
Bindlib.msubst r.rhs (Array.mapi fn r.vars)
(** Type of a symbol and a rule. *)
type sym_rule = sym * rule
let lhs : sym_rule -> term = fun (s, r) -> add_args (mk_Symb s) r.lhs
let rhs : sym_rule -> term = fun (_, r) -> term_of_rhs r
```