Admin/Benchmarks/HOL-datatype/Verilog.thy

 (*  Title:      Admin/Benchmarks/HOL-datatype/Verilog.thy
     ID:         $Id$
 *)
 
-Verilog = Main +
+theory Verilog = Main:
 
 (* ------------------------------------------------------------------------- *)
 (* Example from Daryl: a Verilog grammar.                                    *)
 (* ------------------------------------------------------------------------- *)
 
 datatype
   Source_text
-     = module string (string list) (Module_item list)
+     = 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)
+     = 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)
+          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)
+     | seq_block "string option" "Statement list"
      | StatementMeta string
 and
   Statement_or_null
      = statement Statement | null_statement | Statement_or_nullMeta string
 and

      | negedge string
      | clock string
      | ClockMeta string
 and
   Case_item
-     = case_item (Expression list) Statement_or_null
+     = case_item "Expression list" Statement_or_null
      | default_case_item Statement_or_null
      | Case_itemMeta string
 and
   Expression
      = plus Expression Expression

      | lvalue_concatenation Concatenation
      | LvalueMeta string
 and
   Number
      = decimal string
-     | based (string option) string
+     | based "string option" string
      | NumberMeta string
 and
   Concatenation
-     = concatenation (Expression list) | ConcatenationMeta string
+     = concatenation "Expression list" | ConcatenationMeta string
 and
   Multiple_concatenation
-     = multiple_concatenation Expression (Expression list)
+     = multiple_concatenation Expression "Expression list"
      | Multiple_concatenationMeta string
 and
   meta
      = Meta_Source_text Source_text
      | Meta_Module_item Module_item