diff options
author | Jason Gross <jgross@mit.edu> | 2016-02-05 15:24:42 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2016-02-05 15:24:42 -0500 |
commit | a47b49b11d17add5ca1ea5e650d2f344219b4f7e (patch) | |
tree | 699bff16674a68d1a5dc059bfdbd2f9ca85e95a7 /src/Assembly/Asm.v | |
parent | 1f83ff39458ca80acf3192c938490cf4988b7489 (diff) |
Update build process to use COQPATH & _CoqProject
Removed all of the files not built by default; they can be resurrected from git
history. _CoqProject is the standard way to list the files in a project and to
give information to coq_makefile. COQPATH is the standard way to make use of
not-yet-installed libraries that are not part of your project (i.e., you don't
want to remove them when you `make clean`, etc.).
Diffstat (limited to 'src/Assembly/Asm.v')
-rw-r--r-- | src/Assembly/Asm.v | 66 |
1 files changed, 0 insertions, 66 deletions
diff --git a/src/Assembly/Asm.v b/src/Assembly/Asm.v deleted file mode 100644 index e2186df81..000000000 --- a/src/Assembly/Asm.v +++ /dev/null @@ -1,66 +0,0 @@ - -Require Export Bedrock.Word. - -Inductive AsmType: Set := - | Int32 | Int64 - | Float80 | Int128 - | Pointer. - -Definition Name := String. - -Inductive AsmVar (type: AsmType) := - | StackAsmVar : Name -> AsmVar - | MemoryAsmVar : Name -> AsmVar - | Register : Name -> AsmVar. - -Definition bits (type: AsmType): nat := - match type with - | Int32 => 32 - | Int64 => 64 - | Float80 => 80 - | Int128 => 128 - | Pointer => 64 - end. - -Definition isDouble (a b: AsmType): Prop := - match (a, b) with - | (Int32, Int64) => True - | (Int64, Int128) => True - | _ => False - end. - -Inductive UnaryOp := - | AsmId | AsmNot | AsmOpp. - -Inductive BinaryOp := - | AsmPlus | AsmMinus | AsmMult - | AsmDiv | AsmAnd | AsmOr - | AsmXor | AsmRShift | AsmLShift. - -Inductive AsmTerm (type: AsmType) := - | AsmConst : (word (bits type)) -> (AsmTerm type) - | AsmVarTerm : AsmVar type -> AsmTerm type - | AsmRef: AsmVar type -> AsmTerm Pointer - | AsmDeref: AsmVar Pointer -> AsmTerm type. - -Inductive AsmExpr (type: AsmType) := - | Unary : UnaryOp -> (AsmTerm type) -> (AsmExpr type) - | Binary : BinaryOp -> (AsmTerm type) -> (AsmTerm type) -> (AsmExpr type). - -Inductive AsmComputation := - | AsmDeclare : forall t, AsmVar t -> AsmComputation - | AsmSet : forall t, AsmVar t -> Expr t -> AsmComputation - | AsmDestruct : forall t1 t2, - isDouble t1 t2 -> AsmVar t1 -> AsmVar t1 -> AsmExpr t2 - -> Unit. - | AsmConstruct : forall t1 t2, - isDouble t1 t2 -> AsmVar t2 -> AsmExpr t1 -> AsmExpr t1 - -> Unit. - | AsmSeq : AsmComputation -> AsmComputation -> AsmComputation - | AsmLabel : String -> AsmComputation -> AsmComputation - | AsmGoto : String -> AsmComputation - | AsmIf : forall t, (AsmTerm t) -> AsmComputation -> AsmComputation. - -Inductive AsmSub := - | Asm: forall t, - list ((AsmVar t) * (AsmTerm t)) -> AsmComputation -> AsmTerm t. |