diff options
-rw-r--r-- | src/hls/GiblePargen.v | 2 | ||||
-rw-r--r-- | src/hls/GiblePargenproof.v | 17 |
2 files changed, 13 insertions, 6 deletions
diff --git a/src/hls/GiblePargen.v b/src/hls/GiblePargen.v index 7c9a898..eaf452a 100644 --- a/src/hls/GiblePargen.v +++ b/src/hls/GiblePargen.v @@ -16,6 +16,8 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) +Require Coq.Program.Basics. + Require Import compcert.backend.Registers. Require Import compcert.common.AST. Require Import compcert.common.Globalenvs. diff --git a/src/hls/GiblePargenproof.v b/src/hls/GiblePargenproof.v index 8754ce5..f53cb87 100644 --- a/src/hls/GiblePargenproof.v +++ b/src/hls/GiblePargenproof.v @@ -1976,14 +1976,19 @@ all be evaluable. eapply all_evaluable2_cons in H0. eauto. Qed. + Lemma all_evaluable_pred_ret : + forall A B G (ctx: @ctx G) (sem: @Abstr.ctx G -> A -> B -> Prop) + (a: A) (b: B), + sem ctx a b -> + all_evaluable2 ctx sem (pred_ret a). + Admitted. + Lemma eval_predf_seq_app_evaluable : - forall A B C D (ctx: @ctx A) (sem: @Abstr.ctx A -> C -> D -> Prop) - (a: predicated (B -> C)) b, - all_evaluable2 ctx sem a -> - all_evaluable2 ctx sem b -> - all_evaluable2 ctx sem (seq_app a b). + forall A B G (ctx: @ctx G) (sem: @Abstr.ctx G -> A -> B -> Prop) (l: predicated A) a, + all_evaluable2 ctx sem l -> + all_evaluable2 ctx sem (seq_app a l). Proof. - intros. + intros. unfold seq_app. Lemma eval_predf_update_evaluable : forall A (ctx: @ctx A) curr_p next_p f f_next instr, |