diff options
| -rw-r--r-- | _CoqProject | 3 | ||||
| -rw-r--r-- | src/Compilers/Z/InlineConstAndOp.v | 7 | ||||
| -rw-r--r-- | src/Compilers/Z/InlineConstAndOpInterp.v | 11 | ||||
| -rw-r--r-- | src/Compilers/Z/InlineConstAndOpWf.v | 11 |
4 files changed, 32 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject index babe95a3a..e86e74678 100644 --- a/_CoqProject +++ b/_CoqProject @@ -149,6 +149,9 @@ src/Compilers/Z/CommonSubexpressionEliminationWf.v src/Compilers/Z/FoldTypes.v src/Compilers/Z/HexNotationConstants.v src/Compilers/Z/Inline.v +src/Compilers/Z/InlineConstAndOp.v +src/Compilers/Z/InlineConstAndOpInterp.v +src/Compilers/Z/InlineConstAndOpWf.v src/Compilers/Z/InlineInterp.v src/Compilers/Z/InlineWf.v src/Compilers/Z/InterpSideConditions.v diff --git a/src/Compilers/Z/InlineConstAndOp.v b/src/Compilers/Z/InlineConstAndOp.v new file mode 100644 index 000000000..bdcc0a21b --- /dev/null +++ b/src/Compilers/Z/InlineConstAndOp.v @@ -0,0 +1,7 @@ +Require Import Crypto.Compilers.Syntax. +Require Import Crypto.Compilers.InlineConstAndOp. +Require Import Crypto.Compilers.Z.Syntax. +Require Import Crypto.Compilers.Z.Syntax.Util. + +Definition InlineConstAndOp {t} (e : Expr t) : Expr t + := @InlineConstAndOp base_type op interp_base_type interp_op make_const t e. diff --git a/src/Compilers/Z/InlineConstAndOpInterp.v b/src/Compilers/Z/InlineConstAndOpInterp.v new file mode 100644 index 000000000..417085929 --- /dev/null +++ b/src/Compilers/Z/InlineConstAndOpInterp.v @@ -0,0 +1,11 @@ +Require Import Crypto.Compilers.Syntax. +Require Import Crypto.Compilers.Wf. +Require Import Crypto.Compilers.InlineConstAndOpInterp. +Require Import Crypto.Compilers.Z.Syntax. +Require Import Crypto.Compilers.Z.InlineConstAndOp. + +Definition InterpInlineConstAndOp {t} (e : Expr t) (Hwf : Wf e) + : forall x, Interp (InlineConstAndOp e) x = Interp e x + := @InterpInlineConstAndOp _ _ _ _ _ t e Hwf Syntax.Util.make_const_correct. + +Hint Rewrite @InterpInlineConstAndOp using solve_wf_side_condition : reflective_interp. diff --git a/src/Compilers/Z/InlineConstAndOpWf.v b/src/Compilers/Z/InlineConstAndOpWf.v new file mode 100644 index 000000000..aa0f41d07 --- /dev/null +++ b/src/Compilers/Z/InlineConstAndOpWf.v @@ -0,0 +1,11 @@ +Require Import Crypto.Compilers.Syntax. +Require Import Crypto.Compilers.Wf. +Require Import Crypto.Compilers.InlineConstAndOpWf. +Require Import Crypto.Compilers.Z.Syntax. +Require Import Crypto.Compilers.Z.InlineConstAndOp. + +Definition Wf_InlineConstAndOp {t} (e : Expr t) (Hwf : Wf e) + : Wf (InlineConstAndOp e) + := @Wf_InlineConstAndOp _ _ _ _ _ t e Hwf. + +Hint Resolve Wf_InlineConstAndOp : wf. |