--- a/src/HOL/BNF_Examples/Verilog.thy Thu Sep 11 19:20:23 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,138 +0,0 @@
-(* 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