diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-05-10 19:19:45 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-05-22 15:15:49 +0200 |
| commit | 2c01ce4b5d52a9f86553d07a83a237902b0cbc64 (patch) | |
| tree | 72ebf527bfcd5b28ed86bf07631b26f9f62088fc /plugins/romega | |
| parent | 7547cd5ea5ca48a3c1128349e423e464254bc357 (diff) | |
refl_omega: refactoring of normalize_equation
Diffstat (limited to 'plugins/romega')
| -rw-r--r-- | plugins/romega/refl_omega.ml | 22 |
1 files changed, 9 insertions, 13 deletions
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index ad934aca2..866f91b85 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -668,25 +668,21 @@ let negate_oper = function Eq -> Neq | Neq -> Eq | Leq -> Gt | Geq -> Lt | Lt -> Geq | Gt -> Leq let normalize_equation env (negated,depends,origin,path) (oper,t1,t2) = - let mk_step t1 t2 f kind = - let t = f t1 t2 in + let mk_step t1 t2 t kind = let trace, oterm = normalize_linear_term env t in let equa = omega_of_oformula env kind oterm in { e_comp = oper; e_left = t1; e_right = t2; e_negated = negated; e_depends = depends; e_origin = { o_hyp = origin; o_path = List.rev path }; - e_trace = trace; e_omega = equa } in + e_trace = trace; e_omega = equa } + in try match (if negated then (negate_oper oper) else oper) with - | Eq -> mk_step t1 t2 (fun o1 o2 -> Oplus (o1,Oopp o2)) EQUA - | Neq -> mk_step t1 t2 (fun o1 o2 -> Oplus (o1,Oopp o2)) DISE - | Leq -> mk_step t1 t2 (fun o1 o2 -> Oplus (o2,Oopp o1)) INEQ - | Geq -> mk_step t1 t2 (fun o1 o2 -> Oplus (o1,Oopp o2)) INEQ - | Lt -> - mk_step t1 t2 (fun o1 o2 -> Oplus (Oplus(o2,Oint negone),Oopp o1)) - INEQ - | Gt -> - mk_step t1 t2 (fun o1 o2 -> Oplus (Oplus(o1,Oint negone),Oopp o2)) - INEQ + | Eq -> mk_step t1 t2 (Oplus (t1,Oopp t2)) EQUA + | Neq -> mk_step t1 t2 (Oplus (t1,Oopp t2)) DISE + | Leq -> mk_step t1 t2 (Oplus (t2,Oopp t1)) INEQ + | Geq -> mk_step t1 t2 (Oplus (t1,Oopp t2)) INEQ + | Lt -> mk_step t1 t2 (Oplus (Oplus(t2,Oint negone),Oopp t1)) INEQ + | Gt -> mk_step t1 t2 (Oplus (Oplus(t1,Oint negone),Oopp t2)) INEQ with e when Logic.catchable_exception e -> raise e (* \section{Compilation des hypothèses} *) |