src/HOL/Datatype_Benchmark/Verilog.thy
author huffman
Fri Mar 30 12:32:35 2012 +0200 (2012-03-30)
changeset 47220 52426c62b5d0
parent 45860 93eda35a8377
permissions -rw-r--r--
replace lemmas eval_nat_numeral with a simpler reformulation
wenzelm@45860
     1
(*  Title:      HOL/Datatype_Benchmark/Verilog.thy
wenzelm@33695
     2
wenzelm@33695
     3
Example from Daryl: a Verilog grammar.
berghofe@7013
     4
*)
berghofe@7013
     5
haftmann@16417
     6
theory Verilog imports Main begin
berghofe@7013
     7
berghofe@7013
     8
datatype
berghofe@7013
     9
  Source_text
wenzelm@7373
    10
     = module string "string list" "Module_item list"
berghofe@7013
    11
     | Source_textMeta string
berghofe@7013
    12
and
berghofe@7013
    13
  Module_item
wenzelm@22875
    14
     = "declaration" Declaration
berghofe@7013
    15
     | initial Statement
berghofe@7013
    16
     | always Statement
berghofe@7013
    17
     | assign Lvalue Expression
berghofe@7013
    18
     | Module_itemMeta string
berghofe@7013
    19
and
berghofe@7013
    20
  Declaration
wenzelm@7373
    21
     = reg_declaration "Range option" "string list"
wenzelm@7373
    22
     | net_declaration "Range option" "string list"
wenzelm@7373
    23
     | input_declaration "Range option" "string list"
wenzelm@7373
    24
     | output_declaration "Range option" "string list"
berghofe@7013
    25
     | DeclarationMeta string
berghofe@7013
    26
and
berghofe@7013
    27
  Range = range Expression Expression | RangeMeta string
berghofe@7013
    28
and
berghofe@7013
    29
  Statement
berghofe@7013
    30
     = clock_statement Clock Statement_or_null
berghofe@7013
    31
     | blocking_assignment Lvalue Expression
berghofe@7013
    32
     | non_blocking_assignment Lvalue Expression
berghofe@7013
    33
     | conditional_statement
wenzelm@7373
    34
          Expression Statement_or_null "Statement_or_null option"
wenzelm@7373
    35
     | case_statement Expression "Case_item list"
berghofe@7013
    36
     | while_loop Expression Statement
berghofe@7013
    37
     | repeat_loop Expression Statement
berghofe@7013
    38
     | for_loop
berghofe@7013
    39
          Lvalue Expression Expression Lvalue Expression Statement
berghofe@7013
    40
     | forever_loop Statement
berghofe@7013
    41
     | disable string
wenzelm@7373
    42
     | seq_block "string option" "Statement list"
berghofe@7013
    43
     | StatementMeta string
berghofe@7013
    44
and
berghofe@7013
    45
  Statement_or_null
berghofe@7013
    46
     = statement Statement | null_statement | Statement_or_nullMeta string
berghofe@7013
    47
and
berghofe@7013
    48
  Clock
berghofe@7013
    49
     = posedge string
berghofe@7013
    50
     | negedge string
berghofe@7013
    51
     | clock string
berghofe@7013
    52
     | ClockMeta string
berghofe@7013
    53
and
berghofe@7013
    54
  Case_item
wenzelm@7373
    55
     = case_item "Expression list" Statement_or_null
berghofe@7013
    56
     | default_case_item Statement_or_null
berghofe@7013
    57
     | Case_itemMeta string
berghofe@7013
    58
and
berghofe@7013
    59
  Expression
berghofe@7013
    60
     = plus Expression Expression
berghofe@7013
    61
     | minus Expression Expression
berghofe@7013
    62
     | lshift Expression Expression
berghofe@7013
    63
     | rshift Expression Expression
berghofe@7013
    64
     | lt Expression Expression
berghofe@7013
    65
     | leq Expression Expression
berghofe@7013
    66
     | gt Expression Expression
berghofe@7013
    67
     | geq Expression Expression
berghofe@7013
    68
     | logeq Expression Expression
berghofe@7013
    69
     | logneq Expression Expression
berghofe@7013
    70
     | caseeq Expression Expression
berghofe@7013
    71
     | caseneq Expression Expression
berghofe@7013
    72
     | bitand Expression Expression
berghofe@7013
    73
     | bitxor Expression Expression
berghofe@7013
    74
     | bitor Expression Expression
berghofe@7013
    75
     | logand Expression Expression
berghofe@7013
    76
     | logor Expression Expression
berghofe@7013
    77
     | conditional Expression Expression Expression
berghofe@7013
    78
     | positive Primary
berghofe@7013
    79
     | negative Primary
berghofe@7013
    80
     | lognot Primary
berghofe@7013
    81
     | bitnot Primary
berghofe@7013
    82
     | reducand Primary
berghofe@7013
    83
     | reducxor Primary
berghofe@7013
    84
     | reducor Primary
berghofe@7013
    85
     | reducnand Primary
berghofe@7013
    86
     | reducxnor Primary
berghofe@7013
    87
     | reducnor Primary
berghofe@7013
    88
     | primary Primary
berghofe@7013
    89
     | ExpressionMeta string
berghofe@7013
    90
and
berghofe@7013
    91
  Primary
berghofe@7013
    92
     = primary_number Number
berghofe@7013
    93
     | primary_IDENTIFIER string
berghofe@7013
    94
     | primary_bit_select string Expression
berghofe@7013
    95
     | primary_part_select string Expression Expression
berghofe@7013
    96
     | primary_gen_bit_select Expression Expression
berghofe@7013
    97
     | primary_gen_part_select Expression Expression Expression
berghofe@7013
    98
     | primary_concatenation Concatenation
berghofe@7013
    99
     | primary_multiple_concatenation Multiple_concatenation
berghofe@7013
   100
     | brackets Expression
berghofe@7013
   101
     | PrimaryMeta string
berghofe@7013
   102
and
berghofe@7013
   103
  Lvalue
berghofe@7013
   104
     = lvalue string
berghofe@7013
   105
     | lvalue_bit_select string Expression
berghofe@7013
   106
     | lvalue_part_select string Expression Expression
berghofe@7013
   107
     | lvalue_concatenation Concatenation
berghofe@7013
   108
     | LvalueMeta string
berghofe@7013
   109
and
berghofe@7013
   110
  Number
berghofe@7013
   111
     = decimal string
wenzelm@7373
   112
     | based "string option" string
berghofe@7013
   113
     | NumberMeta string
berghofe@7013
   114
and
berghofe@7013
   115
  Concatenation
wenzelm@7373
   116
     = concatenation "Expression list" | ConcatenationMeta string
berghofe@7013
   117
and
berghofe@7013
   118
  Multiple_concatenation
wenzelm@7373
   119
     = multiple_concatenation Expression "Expression list"
berghofe@7013
   120
     | Multiple_concatenationMeta string
berghofe@7013
   121
and
berghofe@7013
   122
  meta
berghofe@7013
   123
     = Meta_Source_text Source_text
berghofe@7013
   124
     | Meta_Module_item Module_item
berghofe@7013
   125
     | Meta_Declaration Declaration
berghofe@7013
   126
     | Meta_Range Range
berghofe@7013
   127
     | Meta_Statement Statement
berghofe@7013
   128
     | Meta_Statement_or_null Statement_or_null
berghofe@7013
   129
     | Meta_Clock Clock
berghofe@7013
   130
     | Meta_Case_item Case_item
berghofe@7013
   131
     | Meta_Expression Expression
berghofe@7013
   132
     | Meta_Primary Primary
berghofe@7013
   133
     | Meta_Lvalue Lvalue
berghofe@7013
   134
     | Meta_Number Number
berghofe@7013
   135
     | Meta_Concatenation Concatenation
berghofe@7013
   136
     | Meta_Multiple_concatenation Multiple_concatenation
berghofe@7013
   137
berghofe@7013
   138
end