diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-01-24 11:27:13 +0000 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-01-24 11:27:13 +0000 |
commit | 9ef4601b795c121622dcc47dfbe947dc378e15bc (patch) | |
tree | c88cfccf21861f078a21dad7b33948c686b5da4f /src/CoqUp | |
parent | 5663ff602fd4682ed370eb8e6d830cb15894e11e (diff) | |
download | vericert-9ef4601b795c121622dcc47dfbe947dc378e15bc.tar.gz vericert-9ef4601b795c121622dcc47dfbe947dc378e15bc.zip |
Reorder to let it compile again
Diffstat (limited to 'src/CoqUp')
-rw-r--r-- | src/CoqUp/Verilog.v | 72 |
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. |