diff options
| author | Emilio Jesus Gallego Arias | 2019-04-16 18:58:54 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-04-16 18:58:54 +0200 |
| commit | d5d556a31b0711845a1f9df83f9b0b75281c11b6 (patch) | |
| tree | 871b7e98ab648eb313639aafd18e89f9423221c5 /interp | |
| parent | f69b14496b0783c2281db482682540b2e419b967 (diff) | |
[ast] [constrexpr] Make recursion_order_expr an AST node.
This is a bit more uniform.
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrexpr.ml | 5 | ||||
| -rw-r--r-- | interp/constrexpr_ops.ml | 6 |
2 files changed, 7 insertions, 4 deletions
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml index 653bb68f30..9f778d99e9 100644 --- a/interp/constrexpr.ml +++ b/interp/constrexpr.ml @@ -134,16 +134,17 @@ and branch_expr = (cases_pattern_expr list list * constr_expr) CAst.t and fix_expr = - lident * (recursion_order_expr CAst.t) option * + lident * recursion_order_expr option * local_binder_expr list * constr_expr * constr_expr and cofix_expr = lident * local_binder_expr list * constr_expr * constr_expr -and recursion_order_expr = +and recursion_order_expr_r = | CStructRec of lident | CWfRec of lident * constr_expr | CMeasureRec of lident option * constr_expr * constr_expr option (** argument, measure, relation *) +and recursion_order_expr = recursion_order_expr_r CAst.t (* Anonymous defs allowed ?? *) and local_binder_expr = diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index db860e0c3b..443473d5b6 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -198,7 +198,7 @@ and branch_expr_eq {CAst.v=(p1, e1)} {CAst.v=(p2, e2)} = and fix_expr_eq (id1,r1,bl1,a1,b1) (id2,r2,bl2,a2,b2) = (eq_ast Id.equal id1 id2) && - Option.equal (eq_ast recursion_order_expr_eq) r1 r2 && + Option.equal recursion_order_expr_eq r1 r2 && List.equal local_binder_eq bl1 bl2 && constr_expr_eq a1 a2 && constr_expr_eq b1 b2 @@ -209,7 +209,7 @@ and cofix_expr_eq (id1,bl1,a1,b1) (id2,bl2,a2,b2) = constr_expr_eq a1 a2 && constr_expr_eq b1 b2 -and recursion_order_expr_eq r1 r2 = match r1, r2 with +and recursion_order_expr_eq_r r1 r2 = match r1, r2 with | CStructRec i1, CStructRec i2 -> eq_ast Id.equal i1 i2 | CWfRec (i1,e1), CWfRec (i2,e2) -> constr_expr_eq e1 e2 @@ -218,6 +218,8 @@ and recursion_order_expr_eq r1 r2 = match r1, r2 with constr_expr_eq e1 e2 && Option.equal constr_expr_eq o1 o2 | _ -> false +and recursion_order_expr_eq r1 r2 = eq_ast recursion_order_expr_eq_r r1 r2 + and local_binder_eq l1 l2 = match l1, l2 with | CLocalDef (n1, e1, t1), CLocalDef (n2, e2, t2) -> eq_ast Name.equal n1 n2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq t1 t2 |