Admin/Benchmarks/HOL-datatype/Verilog.thy

+(*  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