diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/Compilers/Z/Inline.v | 3 | ||||
-rw-r--r-- | src/Compilers/Z/InlineInterp.v | 6 | ||||
-rw-r--r-- | src/Compilers/Z/InlineWf.v | 6 | ||||
-rw-r--r-- | src/Compilers/Z/Syntax/Util.v | 7 |
4 files changed, 20 insertions, 2 deletions
diff --git a/src/Compilers/Z/Inline.v b/src/Compilers/Z/Inline.v index 8a8bea98b..df46c0ecf 100644 --- a/src/Compilers/Z/Inline.v +++ b/src/Compilers/Z/Inline.v @@ -3,5 +3,8 @@ Require Import Crypto.Compilers.Inline. Require Import Crypto.Compilers.Z.Syntax. Require Import Crypto.Compilers.Z.Syntax.Util. +Definition InlineConstAndOpp {t} (e : Expr base_type op t) : Expr base_type op t + := @InlineConst base_type op (is_const_or_opp) t e. + Definition InlineConst {t} (e : Expr base_type op t) : Expr base_type op t := @InlineConst base_type op (is_const) t e. diff --git a/src/Compilers/Z/InlineInterp.v b/src/Compilers/Z/InlineInterp.v index b0cd0b8df..46e5064e9 100644 --- a/src/Compilers/Z/InlineInterp.v +++ b/src/Compilers/Z/InlineInterp.v @@ -4,8 +4,12 @@ Require Import Crypto.Compilers.InlineInterp. Require Import Crypto.Compilers.Z.Syntax. Require Import Crypto.Compilers.Z.Inline. +Definition InterpInlineConstAndOpp {interp_base_type interp_op} {t} (e : Expr base_type op t) (Hwf : Wf e) + : forall x, Interp interp_op (InlineConstAndOpp e) x = Interp interp_op e x + := @InterpInlineConst _ interp_base_type _ _ _ t e Hwf. + Definition InterpInlineConst {interp_base_type interp_op} {t} (e : Expr base_type op t) (Hwf : Wf e) : forall x, Interp interp_op (InlineConst e) x = Interp interp_op e x := @InterpInlineConst _ interp_base_type _ _ _ t e Hwf. -Hint Rewrite @InterpInlineConst using solve_wf_side_condition : reflective_interp. +Hint Rewrite @InterpInlineConstAndOpp @InterpInlineConst using solve_wf_side_condition : reflective_interp. diff --git a/src/Compilers/Z/InlineWf.v b/src/Compilers/Z/InlineWf.v index 32b84aa1f..d6b846460 100644 --- a/src/Compilers/Z/InlineWf.v +++ b/src/Compilers/Z/InlineWf.v @@ -4,8 +4,12 @@ Require Import Crypto.Compilers.InlineWf. Require Import Crypto.Compilers.Z.Syntax. Require Import Crypto.Compilers.Z.Inline. +Definition Wf_InlineConstAndOpp {t} (e : Expr base_type op t) (Hwf : Wf e) + : Wf (InlineConstAndOpp e) + := @Wf_InlineConst _ _ _ t e Hwf. + Definition Wf_InlineConst {t} (e : Expr base_type op t) (Hwf : Wf e) : Wf (InlineConst e) := @Wf_InlineConst _ _ _ t e Hwf. -Hint Resolve Wf_InlineConst : wf. +Hint Resolve Wf_InlineConstAndOpp Wf_InlineConst : wf. diff --git a/src/Compilers/Z/Syntax/Util.v b/src/Compilers/Z/Syntax/Util.v index b84a00dee..daf3d65be 100644 --- a/src/Compilers/Z/Syntax/Util.v +++ b/src/Compilers/Z/Syntax/Util.v @@ -18,6 +18,13 @@ Definition make_const t : interp_base_type t -> op Unit (Tbase t) Definition is_const s d (v : op s d) : bool := match v with OpConst _ _ => true | _ => false end. Arguments is_const [s d] v. +Definition is_opp s d (v : op s d) : bool + := match v with Opp _ _ => true | _ => false end. +Arguments is_opp [s d] v. +Definition is_const_or_opp s d (v : op s d) : bool + := (is_const v || is_opp v)%bool. +Arguments is_const_or_opp [s d] v. + Definition cast_back_flat_const {var t f V} (v : interp_flat_type interp_base_type (@SmartFlatTypeMap base_type var f t V)) |