--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Datatype_Examples/Verilog.thy Thu Sep 11 19:26:59 2014 +0200
@@ -0,0 +1,138 @@
+(* Title: HOL/Datatype_Benchmark/Verilog.thy
+
+Example from Daryl: a Verilog grammar.
+*)
+
+theory Verilog imports Main begin
+
+datatype
+ Source_text
+ = module string "string list" "Module_item list"
+ | Source_textMeta string
+and
+ Module_item
+ = "declaration" Declaration
+ | initial Statement
+ | always Statement
+ | assign Lvalue Expression
+ | Module_itemMeta string
+and
+ Declaration
+ = reg_declaration "Range option" "string list"
+ | net_declaration "Range option" "string list"
+ | input_declaration "Range option" "string list"
+ | output_declaration "Range option" "string list"
+ | DeclarationMeta string
+and
+ Range = range Expression Expression | RangeMeta string
+and
+ Statement
+ = clock_statement Clock Statement_or_null
+ | blocking_assignment Lvalue Expression
+ | non_blocking_assignment Lvalue Expression
+ | conditional_statement
+ Expression Statement_or_null "Statement_or_null option"
+ | case_statement Expression "Case_item list"
+ | while_loop Expression Statement
+ | repeat_loop Expression Statement
+ | for_loop
+ Lvalue Expression Expression Lvalue Expression Statement
+ | forever_loop Statement
+ | disable string
+ | seq_block "string option" "Statement list"
+ | StatementMeta string
+and
+ Statement_or_null
+ = statement Statement | null_statement | Statement_or_nullMeta string
+and
+ Clock
+ = posedge string
+ | negedge string
+ | clock string
+ | ClockMeta string
+and
+ Case_item
+ = case_item "Expression list" Statement_or_null
+ | default_case_item Statement_or_null
+ | Case_itemMeta string
+and
+ Expression
+ = plus Expression Expression
+ | minus Expression Expression
+ | lshift Expression Expression
+ | rshift Expression Expression
+ | lt Expression Expression
+ | leq Expression Expression
+ | gt Expression Expression
+ | geq Expression Expression
+ | logeq Expression Expression
+ | logneq Expression Expression
+ | caseeq Expression Expression
+ | caseneq Expression Expression
+ | bitand Expression Expression
+ | bitxor Expression Expression
+ | bitor Expression Expression
+ | logand Expression Expression
+ | logor Expression Expression
+ | conditional Expression Expression Expression
+ | positive Primary
+ | negative Primary
+ | lognot Primary
+ | bitnot Primary
+ | reducand Primary
+ | reducxor Primary
+ | reducor Primary
+ | reducnand Primary
+ | reducxnor Primary
+ | reducnor Primary
+ | primary Primary
+ | ExpressionMeta string
+and
+ Primary
+ = primary_number Number
+ | primary_IDENTIFIER string
+ | primary_bit_select string Expression
+ | primary_part_select string Expression Expression
+ | primary_gen_bit_select Expression Expression
+ | primary_gen_part_select Expression Expression Expression
+ | primary_concatenation Concatenation
+ | primary_multiple_concatenation Multiple_concatenation
+ | brackets Expression
+ | PrimaryMeta string
+and
+ Lvalue
+ = lvalue string
+ | lvalue_bit_select string Expression
+ | lvalue_part_select string Expression Expression
+ | lvalue_concatenation Concatenation
+ | LvalueMeta string
+and
+ Number
+ = decimal string
+ | based "string option" string
+ | NumberMeta string
+and
+ Concatenation
+ = concatenation "Expression list" | ConcatenationMeta string
+and
+ Multiple_concatenation
+ = multiple_concatenation Expression "Expression list"
+ | Multiple_concatenationMeta string
+and
+ meta
+ = Meta_Source_text Source_text
+ | Meta_Module_item Module_item
+ | Meta_Declaration Declaration
+ | Meta_Range Range
+ | Meta_Statement Statement
+ | Meta_Statement_or_null Statement_or_null
+ | Meta_Clock Clock
+ | Meta_Case_item Case_item
+ | Meta_Expression Expression
+ | Meta_Primary Primary
+ | Meta_Lvalue Lvalue
+ | Meta_Number Number
+ | Meta_Concatenation Concatenation
+ | Meta_Multiple_concatenation Multiple_concatenation
+
+end