bingf

1 files changed, 66 insertions, 0 deletions

diff --git a/src/Assembly/Asm.v b/src/Assembly/Asm.v
new file mode 100644
index 000000000..e2186df81
--- /dev/null
+++ b/src/Assembly/Asm.v
@@ -0,0 +1,66 @@
+
+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.