Skip to content

Commit

Permalink
Browse files Browse the repository at this point in the history
Bugfixes in rewriting engine (#641)
- Add tests on product matching
- Fixed scoping of product in LHS
- Wildcard created during tree compilation are the most general ones, any free  variable may appear.
- Updated documentation of decision trees
  • Loading branch information
gabrielhdt committed May 6, 2021
1 parent 4cdd818 commit 1e823f3
Show file tree
Hide file tree
Showing 11 changed files with 329 additions and 210 deletions.
8 changes: 8 additions & 0 deletions CHANGES.md
@@ -1,5 +1,13 @@
### Unreleased

#### Bugfixes in rewriting engine (2021-05-06)

- Add tests on product matching
- Fixed scoping of product in LHS
- Wildcard created during tree compilation are the most general ones, any free
variable may appear.
- Updated documentation of decision trees

#### Factorize type `rw_patt` (2021-04-07)

The types `Term.rw_patt` and `Syntax.p_rw_patt_aux` are merged into a
Expand Down
20 changes: 13 additions & 7 deletions docs/dtrees.rst
Expand Up @@ -36,16 +36,22 @@ Decision trees are interpreted during evaluation of terms to get the
correct rule to apply. A node is thus an instruction for the evaluation
algorithm. There are labeled nodes, labeled edges and leaves.

* Circle represent *regular* nodes. The next node is reached by performing an
atomic match between a term of the stack and the labels of the edges between
the node and its children. Let ``t`` be the term taken from the stack and
matched against the labels. The labels of the edges can be
* Circle represent *regular* nodes. Let ``n`` be the label of the node, the next
node is reached by performing an atomic match between the ``n``th term of
the stack and the labels of the edges between the node and its children. Let
``t`` be the term taken from the stack and matched against the labels. The
labels of the edges can be

* ``s_n``, the atomic match succeeds if ``t`` is the symbol ``s`` applied to
``n`` arguments, the ``n`` arguments are put back in the stack;

* ``λvarn``, the atomic match succeeds if ``t`` is an abstraction, the body is
substituted with (fresh) variable ``varn`` and put back in the stack;
* ``λvn``, the atomic match succeeds if ``t`` is an abstraction. the body is
substituted with (fresh) variable ``vn``. Both the domain of the abstraction
and the substituted body are put back into the stack;

* ``Πvn``, the atomic match succeeds if ``t`` is a product. The body is
substituted with a (fresh) variable ``vn``. Both the domain of the product
and the substituted body are put back into the stack

* ``*``, the atomic match succeeds whatever ``t`` is.

Expand All @@ -60,7 +66,7 @@ algorithm. There are labeled nodes, labeled edges and leaves.

* ``n ≡ m`` which succeeds if the ``n``\ th and ``m``\ th saved terms are
convertible,
* ``xs FV(n)`` which succeeds if the free variables of the ``n``\ th saved
* ``xs FV(n)`` which succeeds if the free variables of the ``n``\ th saved
term is a superset of the free variables ``xs``.

* Triangles represent *stack check* nodes. The next node is the left child if
Expand Down
17 changes: 9 additions & 8 deletions src/core/eval.ml
Expand Up @@ -160,8 +160,9 @@ and eq_modulo : ctxt -> term -> term -> bool = fun ctx a b ->
collections of terms.
1. The argument stack [stk] of type {!type:stack} which contains the terms
that are matched against the decision tree.
2. An array [vars] of variables that are used for non-linearity checks and
free variable checks, or that are used in the RHS.
2. An array [vars] containing subterms of the argument stack [stk] that
are filtered by a pattern variable. These terms may be used for
non-linearity or free-variable checks, or may be bound in the RHS.
The [bound] array is similar to the [vars] array except that it is used to
save terms with free variables. *)
Expand Down Expand Up @@ -195,12 +196,12 @@ and tree_walk : dtree -> ctxt -> stack -> (term * stack) option =
let rec walk tree stk cursor vars_id id_vars =
let open Tree_type in
match tree with
| Fail -> None
| Leaf(env_builder, (act, xvars)) ->
| Fail -> None
| Leaf(rhs_subst, (act, xvars)) -> (* Apply the RHS substitution *)
(* Allocate an environment where to place terms coming from the
pattern variables for the action. *)
let env_len = Bindlib.mbinder_arity act in
assert (List.length env_builder = env_len - xvars);
assert (List.length rhs_subst = env_len - xvars);
let env = Array.make env_len TE_None in
(* Retrieve terms needed in the action from the [vars] array. *)
let f (pos, (slot, xs)) =
Expand All @@ -217,7 +218,7 @@ and tree_walk : dtree -> ctxt -> stack -> (term * stack) option =
let xs = Array.map (fun e -> IntMap.find e id_vars) xs in
env.(slot) <- TE_Some(Bindlib.unbox (Bindlib.bind_mvar xs b))
in
List.iter f env_builder;
List.iter f rhs_subst;
(* Complete the array with fresh meta-variables if needed. *)
for i = env_len - xvars to env_len - 1 do
let mt = Meta.make ctx mk_Type in
Expand Down Expand Up @@ -276,7 +277,7 @@ and tree_walk : dtree -> ctxt -> stack -> (term * stack) option =
let stk = List.reconstruct left [] right in
walk t stk cursor vars_id id_vars
in
Option.map_default fn None default
Option.bind fn default
else
let s = Stdlib.(!steps) in
let (t, args) = whnf_stk ctx examined [] in
Expand All @@ -301,7 +302,7 @@ and tree_walk : dtree -> ctxt -> stack -> (term * stack) option =
let stk = List.reconstruct left [] right in
walk d stk cursor vars_id id_vars
in
Option.map_default fn None default
Option.bind fn default
in
(* [walk_binder a b id tr] matches on binder [b] of type [a]
introducing variable [id] and branching on tree [tr]. The type
Expand Down
28 changes: 0 additions & 28 deletions src/core/term.ml
Expand Up @@ -134,34 +134,6 @@ and sym =
appear only in [rhs]. *)
; xvars_nb : int (** Number of variables in [rhs] but not in [lhs]. *) }

(** 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 {!field: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 (if any) for the matched term in the environment of the
RHS during matching. When [i] is [None], then the variable is not bound in
the RHS. If it is [Some(_)], then the variables is bound in the RHS, or it
appears non-linearly in the LHS.
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(None, "Z", [||])] since it is only appears
once in the LHS, and it is not used in the RHS. 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 2 if we
have [a.(0) = t], [a.(1) = u] and [a.(1) = v]. *)

(** {b NOTE} that the second parameter of the {!constructor:Patt} constructor
holds an array of terms. This is essential for variables binding: using an
array of variables would NOT suffice. *)
Expand Down
19 changes: 10 additions & 9 deletions src/core/term.mli
Expand Up @@ -138,24 +138,25 @@ and sym =
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 (if any) for the matched term in the environment of the
RHS during matching. When [i] is [None], then the variable is not bound in
the RHS. If it is [Some(_)], then the variables is bound in the RHS, or it
appears non-linearly in the LHS.
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(None, "Z", [||])] since it is only appears
once in the LHS, and it is not used in the RHS. Note that wildcards (in
the concrete syntax) are represented in the same way, and with a unique
- [$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 2 if we
have [a.(0) = t], [a.(1) = u] and [a.(1) = v]. *)
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].
{b TODO} memorising [w] in the substitution is sub-optimal. In practice,
the term matched by [$Z] should be ignored. *)

(** {b NOTE} that the second parameter of the {!constructor:Patt} constructor
holds an array of terms. This is essential for variables binding: using an
Expand Down

0 comments on commit 1e823f3

Please sign in to comment.