diff options
author | Robert Sloan <varomodt@gmail.com> | 2016-06-04 20:54:39 -0400 |
---|---|---|
committer | Robert Sloan <varomodt@gmail.com> | 2016-06-22 13:43:38 -0400 |
commit | 8f2241042d26d94b138a6f2a51287dae413b7ec2 (patch) | |
tree | f4a1de6b540bae2f211479eb2955b660a10db994 /src/Assembly/QhasmEvalCommon.v | |
parent | 2dc6b1def9685b8b1deb69a02715ae2ac21383c2 (diff) |
Huge Language / Conversion refactors
Diffstat (limited to 'src/Assembly/QhasmEvalCommon.v')
-rw-r--r-- | src/Assembly/QhasmEvalCommon.v | 46 |
1 files changed, 6 insertions, 40 deletions
diff --git a/src/Assembly/QhasmEvalCommon.v b/src/Assembly/QhasmEvalCommon.v index 83ef5b701..b12e27e19 100644 --- a/src/Assembly/QhasmEvalCommon.v +++ b/src/Assembly/QhasmEvalCommon.v @@ -1,7 +1,7 @@ Require Export QhasmCommon QhasmUtil State. Require Export ZArith Sumbool. Require Export Bedrock.Word. -Require Import Logic.Eqdep_dec. +Require Import Logic.Eqdep_dec ProofIrrelevance. Import Util. @@ -116,12 +116,11 @@ Module EvalUtil. then left _ else right _ - | (memM _ v, memM _ v') => fun _ => + | (memM _ v i, memM _ v' i') => fun _ => if (Nat.eq_dec (memName v) (memName v')) then if (Nat.eq_dec (memLength v) (memLength v')) - then left _ - else right _ - else right _ + then if (Nat.eq_dec (proj1_sig i) (proj1_sig i')) + then left _ else right _ else right _ else right _ | _ => fun _ => right _ end (eq_refl (a, b))); abstract ( @@ -137,6 +136,8 @@ Module EvalUtil. rewrite _H0 | apply (inj_pair2_eq_dec _ Nat.eq_dec) in H3 | inversion H; subst; intuition + | destruct i, i'; simpl in _H2; subst; + replace l with l0 by apply proof_irrelevance | intuition ]). Defined. @@ -170,41 +171,6 @@ Module EvalUtil. end end. - (* Mapping Identifier-Triples *) - - Definition mappingId {n} (x: Mapping n): nat * nat * nat := - match x with - | regM (reg n _ v) => (0, n, v) - | stackM (stack n _ v) => (1, n, v) - | constM (const n _ w) => (2, n, wordToNat w) - | memM _ (mem n m _ v) => (3, m, v) - end. - - Lemma id_equal: forall {n: nat} (x y: Mapping n), - x = y <-> mappingId x = mappingId y. - Proof. - intros; split; intros; try abstract (rewrite H; intuition); - destruct x as [x | x | x | x], y as [y | y | y | y]; - destruct x, y; unfold mappingId in H; simpl in H; - - repeat match goal with - | [X: (_, _, _) = (_, _, _) |- _ ] => - apply Triple_as_OT.conv in X - | [X: _ /\ _ /\ _ |- _ ] => destruct X - | [X: _ /\ _ |- _ ] => destruct X - | [A: Width _, B: Width _ |- _ ] => - replace A with B by (apply width_eq) - | [X: context[match ?a with | _ => _ end] |- _ ] => - destruct a - end; try subst; try omega; intuition. - - rewrite <- (natToWord_wordToNat w0); - rewrite <- (natToWord_wordToNat w2); - rewrite H1; intuition. - Qed. - - Definition id_dec := Triple_as_OT.eq_dec. - End EvalUtil. Module QhasmEval. |