author | blanchet |
Thu, 11 Sep 2014 19:26:59 +0200 | |
changeset 58309 | a09ec6daaa19 |
parent 58308 | src/HOL/BNF_Examples/Verilog.thy@0ccba1b6d00b |
child 58330 | a016c42d136d |
permissions | -rw-r--r-- |
45860 | 1 |
(* Title: HOL/Datatype_Benchmark/Verilog.thy |
33695 | 2 |
|
3 |
Example from Daryl: a Verilog grammar. |
|
7013
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
4 |
*) |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
5 |
|
16417 | 6 |
theory Verilog imports Main begin |
7013
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
7 |
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
8 |
datatype |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
9 |
Source_text |
7373 | 10 |
= module string "string list" "Module_item list" |
7013
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
11 |
| Source_textMeta string |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
12 |
and |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
13 |
Module_item |
22875 | 14 |
= "declaration" Declaration |
7013
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
15 |
| initial Statement |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
16 |
| always Statement |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
17 |
| assign Lvalue Expression |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
18 |
| Module_itemMeta string |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
19 |
and |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
20 |
Declaration |
7373 | 21 |
= reg_declaration "Range option" "string list" |
22 |
| net_declaration "Range option" "string list" |
|
23 |
| input_declaration "Range option" "string list" |
|
24 |
| output_declaration "Range option" "string list" |
|
7013
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
25 |
| DeclarationMeta string |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
26 |
and |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
27 |
Range = range Expression Expression | RangeMeta string |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
28 |
and |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
29 |
Statement |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
30 |
= clock_statement Clock Statement_or_null |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
31 |
| blocking_assignment Lvalue Expression |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
32 |
| non_blocking_assignment Lvalue Expression |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
33 |
| conditional_statement |
7373 | 34 |
Expression Statement_or_null "Statement_or_null option" |
35 |
| case_statement Expression "Case_item list" |
|
7013
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
36 |
| while_loop Expression Statement |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
37 |
| repeat_loop Expression Statement |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
38 |
| for_loop |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
39 |
Lvalue Expression Expression Lvalue Expression Statement |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
40 |
| forever_loop Statement |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
41 |
| disable string |
7373 | 42 |
| seq_block "string option" "Statement list" |
7013
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
43 |
| StatementMeta string |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
44 |
and |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
45 |
Statement_or_null |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
46 |
= statement Statement | null_statement | Statement_or_nullMeta string |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
47 |
and |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
48 |
Clock |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
49 |
= posedge string |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
50 |
| negedge string |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
51 |
| clock string |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
52 |
| ClockMeta string |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
53 |
and |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
54 |
Case_item |
7373 | 55 |
= case_item "Expression list" Statement_or_null |
7013
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
56 |
| default_case_item Statement_or_null |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
57 |
| Case_itemMeta string |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
58 |
and |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
59 |
Expression |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
60 |
= plus Expression Expression |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
61 |
| minus Expression Expression |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
62 |
| lshift Expression Expression |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
63 |
| rshift Expression Expression |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
64 |
| lt Expression Expression |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
65 |
| leq Expression Expression |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
66 |
| gt Expression Expression |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
67 |
| geq Expression Expression |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
68 |
| logeq Expression Expression |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
69 |
| logneq Expression Expression |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
70 |
| caseeq Expression Expression |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
71 |
| caseneq Expression Expression |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
72 |
| bitand Expression Expression |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
73 |
| bitxor Expression Expression |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
74 |
| bitor Expression Expression |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
75 |
| logand Expression Expression |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
76 |
| logor Expression Expression |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
77 |
| conditional Expression Expression Expression |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
78 |
| positive Primary |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
79 |
| negative Primary |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
80 |
| lognot Primary |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
81 |
| bitnot Primary |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
82 |
| reducand Primary |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
83 |
| reducxor Primary |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
84 |
| reducor Primary |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
85 |
| reducnand Primary |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
86 |
| reducxnor Primary |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
87 |
| reducnor Primary |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
88 |
| primary Primary |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
89 |
| ExpressionMeta string |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
90 |
and |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
91 |
Primary |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
92 |
= primary_number Number |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
93 |
| primary_IDENTIFIER string |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
94 |
| primary_bit_select string Expression |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
95 |
| primary_part_select string Expression Expression |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
96 |
| primary_gen_bit_select Expression Expression |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
97 |
| primary_gen_part_select Expression Expression Expression |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
98 |
| primary_concatenation Concatenation |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
99 |
| primary_multiple_concatenation Multiple_concatenation |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
100 |
| brackets Expression |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
101 |
| PrimaryMeta string |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
102 |
and |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
103 |
Lvalue |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
104 |
= lvalue string |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
105 |
| lvalue_bit_select string Expression |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
106 |
| lvalue_part_select string Expression Expression |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
107 |
| lvalue_concatenation Concatenation |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
108 |
| LvalueMeta string |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
109 |
and |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
110 |
Number |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
111 |
= decimal string |
7373 | 112 |
| based "string option" string |
7013
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
113 |
| NumberMeta string |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
114 |
and |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
115 |
Concatenation |
7373 | 116 |
= concatenation "Expression list" | ConcatenationMeta string |
7013
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
117 |
and |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
118 |
Multiple_concatenation |
7373 | 119 |
= multiple_concatenation Expression "Expression list" |
7013
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
120 |
| Multiple_concatenationMeta string |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
121 |
and |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
122 |
meta |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
123 |
= Meta_Source_text Source_text |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
124 |
| Meta_Module_item Module_item |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
125 |
| Meta_Declaration Declaration |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
126 |
| Meta_Range Range |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
127 |
| Meta_Statement Statement |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
128 |
| Meta_Statement_or_null Statement_or_null |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
129 |
| Meta_Clock Clock |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
130 |
| Meta_Case_item Case_item |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
131 |
| Meta_Expression Expression |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
132 |
| Meta_Primary Primary |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
133 |
| Meta_Lvalue Lvalue |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
134 |
| Meta_Number Number |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
135 |
| Meta_Concatenation Concatenation |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
136 |
| Meta_Multiple_concatenation Multiple_concatenation |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
137 |
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
138 |
end |