Datatype package now handles arbitrarily branching datatypes.
(* 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