From d0574a82e5443aabaec0ead92d1e6af38d834b46 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 15 May 2017 01:39:55 -0400 Subject: Add src/Compilers/Z/Named/DeadCodeEliminationInterp.v --- src/Compilers/Named/DeadCodeEliminationInterp.v | 2 +- src/Compilers/Z/Named/DeadCodeEliminationInterp.v | 50 +++++++++++++++++++++++ 2 files changed, 51 insertions(+), 1 deletion(-) create mode 100644 src/Compilers/Z/Named/DeadCodeEliminationInterp.v (limited to 'src') diff --git a/src/Compilers/Named/DeadCodeEliminationInterp.v b/src/Compilers/Named/DeadCodeEliminationInterp.v index 185a84acd..f822e6e29 100644 --- a/src/Compilers/Named/DeadCodeEliminationInterp.v +++ b/src/Compilers/Named/DeadCodeEliminationInterp.v @@ -35,7 +35,7 @@ Section language. Lemma interp_EliminateDeadCode t e new_names - (ctxi_interp : PositiveContext _ _ base_type_code_beq base_type_code_bl) + (ctxi_interp : PContext _) (ctxr_interp : InterpContext) eout v1 v2 x : @EliminateDeadCode t e new_names = Some eout diff --git a/src/Compilers/Z/Named/DeadCodeEliminationInterp.v b/src/Compilers/Z/Named/DeadCodeEliminationInterp.v new file mode 100644 index 000000000..422e8c309 --- /dev/null +++ b/src/Compilers/Z/Named/DeadCodeEliminationInterp.v @@ -0,0 +1,50 @@ +Require Import Coq.PArith.BinPos. +Require Import Crypto.Compilers.Syntax. +Require Import Crypto.Compilers.Named.Context. +Require Import Crypto.Compilers.Named.ContextDefinitions. +Require Import Crypto.Compilers.Named.PositiveContext. +Require Import Crypto.Compilers.Z.Named.DeadCodeElimination. +Require Import Crypto.Compilers.Named.DeadCodeEliminationInterp. +Require Import Crypto.Compilers.Z.Syntax. +Require Import Crypto.Compilers.Named.Syntax. + +Section language. + Context {interp_base_type : base_type -> Type} + {interp_op : forall s d, op s d -> interp_flat_type interp_base_type s -> interp_flat_type interp_base_type d} + {Name : Type} + {InContext : Context Name (fun _ : base_type => positive)} + {InContextOk : ContextOk InContext} + {Name_beq : Name -> Name -> bool} + {InterpContext : Context Name interp_base_type} + {InterpContextOk : ContextOk InterpContext} + (Name_bl : forall n1 n2, Name_beq n1 n2 = true -> n1 = n2) + (Name_lb : forall n1 n2, n1 = n2 -> Name_beq n1 n2 = true). + + Local Notation EliminateDeadCode := (@EliminateDeadCode Name InContext). + Local Notation PContext var := (@PositiveContext base_type var base_type_beq internal_base_type_dec_bl). + + Lemma interp_EliminateDeadCode + t e new_names + (ctxi_interp : PContext _) + (ctxr_interp : InterpContext) + eout v1 v2 x + : @EliminateDeadCode t e new_names = Some eout + -> interp (interp_op:=interp_op) (ctx:=ctxr_interp) eout x = Some v1 + -> interp (interp_op:=interp_op) (ctx:=ctxi_interp) e x = Some v2 + -> v1 = v2. + Proof using InContextOk InterpContextOk Name_bl Name_lb. + eapply interp_EliminateDeadCode; eauto using internal_base_type_dec_lb. + Qed. + + Lemma InterpEliminateDeadCode + t e new_names + eout + v1 v2 x + : @EliminateDeadCode t e new_names = Some eout + -> Interp (Context:=InterpContext) (interp_op:=interp_op) eout x = Some v1 + -> Interp (Context:=PContext _) (interp_op:=interp_op) e x = Some v2 + -> v1 = v2. + Proof using InContextOk InterpContextOk Name_bl Name_lb. + apply interp_EliminateDeadCode. + Qed. +End language. -- cgit v1.2.3