diff options
Diffstat (limited to 'src/Assembly/Pseudo.v')
| -rw-r--r-- | src/Assembly/Pseudo.v | 23 |
1 files changed, 13 insertions, 10 deletions
diff --git a/src/Assembly/Pseudo.v b/src/Assembly/Pseudo.v index 6102b9642..48e642151 100644 --- a/src/Assembly/Pseudo.v +++ b/src/Assembly/Pseudo.v @@ -1,6 +1,6 @@ Require Import QhasmUtil QhasmCommon QhasmEvalCommon QhasmUtil State. Require Import Language. -Require Import List. +Require Import List Compare_dec. Module Pseudo <: Language. Import EvalUtil ListState. @@ -113,18 +113,21 @@ Module Pseudo <: Language. Delimit Scope pseudo_notations with p. Local Open Scope pseudo_notations. - Definition indexize (n: nat) (p: (n > 0)%nat) (x: nat): Index n. - intros; exists (x mod n); - abstract (pose proof (mod_bound_pos x n); omega). + Definition indexize {n: nat} (x: nat): Index n. + intros; destruct (le_dec n 0). + + - exists 0; abstract intuition. + - exists (x mod n); abstract ( + pose proof (mod_bound_pos x n); omega). Defined. - Notation "% A" := (PVar _ (Some false) (indexize _ _ A)) + Notation "% A" := (PVar _ (Some false) (indexize A)) (at level 20, right associativity) : pseudo_notations. - Notation "$ A" := (PVar _ (Some true) (indexize _ _ A)) + Notation "$ A" := (PVar _ (Some true) (indexize A)) (at level 20, right associativity) : pseudo_notations. - Notation "A :[ B ]:" := (PMem _ _ (indexize _ _ A) (indexize _ _ B)) + Notation "A :[ B ]:" := (PMem _ _ (indexize A) (indexize B)) (at level 20, right associativity) : pseudo_notations. Notation "# A" := (PConst _ (natToWord _ A)) @@ -145,17 +148,17 @@ Module Pseudo <: Language. Notation "A :^: B" := (PBin _ Xor (PComb _ _ _ A B)) (at level 45, right associativity) : pseudo_notations. - Notation "A :>>: B" := (PShift _ Shr (indexize _ _ B) A) + Notation "A :>>: B" := (PShift _ Shr (indexize B) A) (at level 60, right associativity) : pseudo_notations. - Notation "A :<<: B" := (PShift _ Shl (indexize _ _ B) A) + Notation "A :<<: B" := (PShift _ Shl (indexize B) A) (at level 60, right associativity) : pseudo_notations. Notation "A :*: B" := (PDual _ Mult (PComb _ _ _ A B)) (at level 55, right associativity) : pseudo_notations. Notation "O :( A , B ): :?: L ::: R" := - (PIf _ _ O (indexize _ _ A) (indexize _ _ B) L R) + (PIf _ _ O (indexize A) (indexize B) L R) (at level 70, right associativity) : pseudo_notations. Notation "F :**: e" := |