diff options
Diffstat (limited to 'src/Compilers/Z/ArithmeticSimplifier.v')
| -rw-r--r-- | src/Compilers/Z/ArithmeticSimplifier.v | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/src/Compilers/Z/ArithmeticSimplifier.v b/src/Compilers/Z/ArithmeticSimplifier.v index b2621c625..f0d3e19ab 100644 --- a/src/Compilers/Z/ArithmeticSimplifier.v +++ b/src/Compilers/Z/ArithmeticSimplifier.v @@ -20,9 +20,18 @@ Section language. : option (interp_flat_type inverted_expr t) := match x in Syntax.exprf _ _ t return option (interp_flat_type _ t) with | Op t1 (Tbase _) opc args - => Some (match opc in op src dst return exprf dst -> exprf src -> inverted_expr match dst with Tbase t => t | _ => TZ end with + => Some (match opc in op src dst + return exprf dst + -> exprf src + -> match dst with + | Tbase t => inverted_expr t + | Prod _ _ => True + | _ => inverted_expr TZ + end + with | OpConst _ z => fun _ _ => const_of _ z | Opp TZ TZ => fun _ args => neg_expr _ args + | AddWithGetCarry _ _ _ _ _ _ => fun _ _ => I | _ => fun e _ => gen_expr _ e end (Op opc args) args) | TT => Some tt @@ -175,6 +184,9 @@ Section language. | Lor _ _ _ as opc | OpConst _ _ as opc | Opp _ _ as opc + | Zselect _ _ _ _ as opc + | AddWithCarry _ _ _ _ as opc + | AddWithGetCarry _ _ _ _ _ _ as opc => Op opc end. End with_var. |