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