diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-10 16:15:57 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-02-20 10:03:03 +0100 |
| commit | 6b9a9124d3bd24fe9305df613547139f6f609c60 (patch) | |
| tree | 59d3dacf28fc8088190b90c7f037ead219b4e877 /intf | |
| parent | 407e154baa44609dea9f6f1ade746e24d60e2513 (diff) | |
Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.
The motivations are:
- To reflect the concrete syntax more closely.
- To factorize the different places where "contexts" are internalized:
before this patch, there is a different treatment of `Definition f
'(x,y) := x+y` and `Definition f := fun '(x,y) => x+y`, and a hack
to interpret `Definition f `pat := c : t`. With the patch, the fix
to avoid seeing a variable named `pat` works for both `fun 'x =>
...` and `Definition f 'x := ...`.
The drawbacks are:
- Counterpart to reflecting the concrete syntax more closerly, there
are more redundancies in the syntax. For instance, the case `CLetIn
(na,b,t,c)` can appears also in the form `CProdN (CLocalDef
(na,b,t)::rest,d)` and `CLambdaN (CLocalDef (na,b,t)::rest,d)`.
- Changes in the API, hence adaptation of plugins referring to `constr_expr` needed.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/constrexpr.ml | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml index fbf9e248a..2575b71ea 100644 --- a/intf/constrexpr.ml +++ b/intf/constrexpr.ml @@ -70,8 +70,8 @@ and constr_expr_r = | CRef of reference * instance_expr option | CFix of Id.t Loc.located * fix_expr list | CCoFix of Id.t Loc.located * cofix_expr list - | CProdN of binder_expr list * constr_expr - | CLambdaN of binder_expr list * constr_expr + | CProdN of local_binder_expr list * constr_expr + | CLambdaN of local_binder_expr list * constr_expr | CLetIn of Name.t Loc.located * constr_expr * constr_expr option * constr_expr | CAppExpl of (proj_flag * reference * instance_expr option) * constr_expr list | CApp of (proj_flag * constr_expr) * @@ -107,9 +107,6 @@ and case_expr = constr_expr (* expression that is being matched and branch_expr = (cases_pattern_expr list list * constr_expr) Loc.located -and binder_expr = - Name.t Loc.located list * binder_kind * constr_expr - and fix_expr = Id.t Loc.located * (Id.t Loc.located option * recursion_order_expr) * local_binder_expr list * constr_expr * constr_expr |