aboutsummaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2020-01-24 11:27:13 +0000
committerYann Herklotz <git@yannherklotz.com>2020-01-24 11:27:13 +0000
commit9ef4601b795c121622dcc47dfbe947dc378e15bc (patch)
treec88cfccf21861f078a21dad7b33948c686b5da4f /src
parent5663ff602fd4682ed370eb8e6d830cb15894e11e (diff)
downloadvericert-9ef4601b795c121622dcc47dfbe947dc378e15bc.tar.gz
vericert-9ef4601b795c121622dcc47dfbe947dc378e15bc.zip
Reorder to let it compile again
Diffstat (limited to 'src')
-rw-r--r--src/CoqUp/Verilog.v72
1 files changed, 35 insertions, 37 deletions
diff --git a/src/CoqUp/Verilog.v b/src/CoqUp/Verilog.v
index 97e91f7..7d3c524 100644
--- a/src/CoqUp/Verilog.v
+++ b/src/CoqUp/Verilog.v
@@ -36,7 +36,42 @@ Module Verilog.
end
end.
+ Definition state : Type := Map.t value * Map.t value.
+
+ Inductive binop : Type :=
+ | Plus
+ | Minus
+ | Times
+ | Divide
+ | LT
+ | GT
+ | LE
+ | GE
+ | Eq
+ | And
+ | Or
+ | Xor.
+
+ Inductive expr : Type :=
+ | Lit (n : value)
+ | Var (s : string)
+ | Neg (a : expr)
+ | BinOp (op : binop) (a1 a2 : expr)
+ | Ternary (c t f : expr).
+
+ Inductive stmnt : Type :=
+ | Skip
+ | Block (s : list stmnt)
+ | Cond (c : expr) (st sf : stmnt)
+ | Case (c : expr) (b : list (expr * stmnt))
+ | Blocking (a b : expr)
+ | Nonblocking (a b : expr).
+
+ Inductive verilog : Type := Verilog (s : list stmnt).
+
Coercion VBool : bool >-> value.
+ Coercion Lit : value >-> expr.
+ Coercion Var : string >-> expr.
Definition value_is_bool (v : value) : bool :=
match v with
@@ -103,43 +138,6 @@ Module Verilog.
end
end.
- Definition state : Type := Map.t value * Map.t value.
-
- Inductive binop : Type :=
- | Plus
- | Minus
- | Times
- | Divide
- | LT
- | GT
- | LE
- | GE
- | Eq
- | And
- | Or
- | Xor.
-
- Inductive expr : Type :=
- | Lit (n : value)
- | Var (s : string)
- | Neg (a : expr)
- | BinOp (op : binop) (a1 a2 : expr)
- | Ternary (c t f : expr).
-
- Inductive stmnt : Type :=
- | Skip
- | Block (s : list stmnt)
- | Cond (c : expr) (st sf : stmnt)
- | Case (c : expr) (b : list (expr * stmnt))
- | Blocking (a b : expr)
- | Nonblocking (a b : expr).
-
- Inductive verilog : Type := Verilog (s : list stmnt).
-
- Coercion VBool : bool >-> value.
- Coercion Lit : value >-> expr.
- Coercion Var : string >-> expr.
-
Module VerilogNotation.
Declare Scope verilog_scope.