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