Admin/Benchmarks/HOL-datatype/Verilog.thy

tuned proof

(*  Title:      Admin/Benchmarks/HOL-datatype/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