diff options
| author |  Robert Sloan <varomodt@gmail.com> | 2016-05-05 16:24:20 -0400 |
|---|---|---|
| committer | Robert Sloan <varomodt@gmail.com> | 2016-06-22 13:43:24 -0400 |
| commit | ccd6cc8f48fe9c312a716ce01d547626d7d13b9a (patch) | |
| tree | 7d51b6511a5d847ea38a8c91b7486737edb5a515 /src/Assembly/Pseudo.v | |
| parent | d3d4d2ff20798f4904b33b4e835dc2dde003b09d (diff) | |
Finished first draft of PseudoConversions
Diffstat (limited to 'src/Assembly/Pseudo.v')
| -rw-r--r-- | src/Assembly/Pseudo.v | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/src/Assembly/Pseudo.v b/src/Assembly/Pseudo.v index edb95d38a..10f9f4ab2 100644 --- a/src/Assembly/Pseudo.v +++ b/src/Assembly/Pseudo.v @@ -43,7 +43,7 @@ Module Pseudo (M: PseudoMachine) <: Language. Definition State := list const. Inductive WBinOp: Set := - | Wplus: WBinOp | Wmult: WBinOp + | Wplus: WBinOp | Wminus: WBinOp | Wand: WBinOp. Inductive WNatOp: Set := @@ -57,8 +57,8 @@ Module Pseudo (M: PseudoMachine) <: Language. | PConst: forall n, const -> Pseudo n 1 | PBin: forall n, WBinOp -> Pseudo n 1 -> Pseudo n 1 -> Pseudo n 1 - | PNat: forall n, WNatOp -> nat -> Pseudo n 1 - | PShift: forall n, WShiftOp -> Pseudo n 1 -> nat -> Pseudo n 1 + | PNat: forall n, WNatOp -> Index width -> Pseudo n 1 + | PShift: forall n, WShiftOp -> Pseudo n 1 -> Index width -> Pseudo n 1 | PLet: forall n k m, Pseudo n k -> Pseudo (n + k) m -> Pseudo n m | PComp: forall n k m, Pseudo n k -> Pseudo k m -> Pseudo n m @@ -74,7 +74,6 @@ Module Pseudo (M: PseudoMachine) <: Language. Definition applyBin (op: WBinOp) (a b: word width): option (list const) := match op with | Wplus => Some [(wplus a b)] - | Wmult => Some [(wmult a b)] | Wminus => Some [(wminus a b)] | Wand => Some [(wand a b)] end. |