--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/Benchmarks/HOL-datatype/Verilog.thy Fri Jul 16 12:02:06 1999 +0200
@@ -0,0 +1,141 @@
+(* Title: Admin/Benchmarks/HOL-datatype/Verilog.thy
+ ID: $Id$
+*)
+
+Verilog = Main +
+
+(* ------------------------------------------------------------------------- *)
+(* Example from Daryl: a Verilog grammar. *)
+(* ------------------------------------------------------------------------- *)
+
+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