diff options
| author |  Robert Sloan <varomodt@google.com> | 2016-10-21 14:08:14 -0700 |
|---|---|---|
| committer | Robert Sloan <varomodt@google.com> | 2016-10-21 14:08:14 -0700 |
| commit | eed4e2ee6d6a60268c6729920613962ff3fc5285 (patch) | |
| tree | 4a4669505728b365149bb455904e0c211fc7833e /src/Assembly/Compile.v | |
| parent | 4225439aa82294a6d2a56fc4f622dc318e69529f (diff) | |
| parent | 37e2b17fa4daf7e85466a02e0be2ffb603f446cb (diff) | |
merge rsloan-phoas refactors into master
Diffstat (limited to 'src/Assembly/Compile.v')
| -rw-r--r-- | src/Assembly/Compile.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/Assembly/Compile.v b/src/Assembly/Compile.v index 2ff50e0e1..91eb37a16 100644 --- a/src/Assembly/Compile.v +++ b/src/Assembly/Compile.v @@ -1,6 +1,6 @@ Require Import Coq.Logic.Eqdep. -Require Import Compare_dec Sumbool. -Require Import PeanoNat Omega. +Require Import Coq.Arith.Compare_dec Coq.Bool.Sumbool. +Require Import Coq.Numbers.Natural.Peano.NPeano Coq.omega.Omega. Require Import Crypto.Assembly.PhoasCommon. Require Import Crypto.Assembly.HL. @@ -120,7 +120,7 @@ Module CompileLL. option (Reg n * list Assignment * Operation) := let mov := if (EvalUtil.mapping_dec (regM _ out) in1) - then [] + then [] else makeA (regM _ out) in1 in match op with @@ -138,7 +138,7 @@ Module CompileLL. | _ => None end - | OPmul => + | OPmul => match in2 with | regM r1 => Some (out, mov, DOp Mult out r1 None) | constM c => Some (out, mov ++ (makeA (regM _ tmp) in2), DOp Mult out tmp None) @@ -152,7 +152,7 @@ Module CompileLL. | _ => None end - | OPshiftr => + | OPshiftr => match in2 with | constM (constant _ _ w) => Some (out, mov, ROp Shr out (indexize (wordToNat w))) @@ -244,7 +244,7 @@ Module CompileLL. | TT => Const (@wzero n) | Prod t0 t1 => Pair (zeros t0) (zeros t1) end. - + Fixpoint exprF {t} (nextRegName: nat) (p: WExpr t) {struct p}: option Out := match p with | LetBinop t1 t2 t3 op x y t' eC => |