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