Examples/rectypes.ml

   1 (* ========================================================================= *)
   2 (* Some (mutually, nested) recursive types from various sources.             *)
   3 (* ========================================================================= *)
   4
   5 time define_type "Term = Var A B | App bool Termlist;
   6               Termlist = Empty | Consp Term Termlist";;
   7
   8 time define_type "List = Nil | Cons A List";;
   9
  10 time define_type "Btree = Leaf A | Node B Btree Btree";;
  11
  12 time define_type "Command = Assign ind Expression
  13                     | If Expression Command
  14                     | Ite Expression Command Command
  15                     | While Expression Command
  16                     | Do Command Expression;
  17             Expression = Constant num
  18                        | Variable ind
  19                        | Summ Expression Expression
  20                        | Product Expression Expression";;
  21
  22 time define_type "testa = empty_testa | cons_testa testa testb;
  23             testb = contentb L testc;
  24             testc = connection M testa";;
  25
  26 time define_type "atexp = Varb ind | Let dec exp;
  27             exp   = Exp1 atexp | Exp2 exp atexp | Exp3 matching;
  28             matching = Match1 rule | Matches rule matching;
  29             rule  = Rule pat exp;
  30             dec   = Val valbind | Local dec dec | Decs dec dec;
  31             valbind = Single pat exp | Multi pat exp valbind | Rec valbind;
  32             pat = Wild | Varpat ind";;
  33
  34 time define_type "tri = ONE | TWO | THREE";;
  35
  36 (* ------------------------------------------------------------------------- *)
  37 (* A couple from Steve Brackin's work.                                       *)
  38 (* ------------------------------------------------------------------------- *)
  39
  40 time define_type "T = X1 | X2 | X3 | X4 | X5 | X6 | X7 | X8 | X9 | X10 | X11 |
  41                 X12 | X13 | X14 | X15 | X16 | X17 | X18 | X19 | X20 | X21 |
  42                 X22 | X23 | X24 | X25 | X26 | X27 | X28 | X29 | X30 | X31 |
  43                 X32 | X33 | X34";;
  44
  45 time define_type "TY1 = NoF__ | Fk__ A TY2;
  46             TY2 = Ta__ bool | Td__ bool | Tf__ TY1 | Tk__ bool | Tp__ bool
  47                 | App__ A TY1 TY2 TY3 | Pair__ TY2 TY2;
  48             TY3 = NoS__ | Fresh__ TY2 | Trustworthy__ A
  49                 | PrivateKey__ A B C | PublicKey__ A B C
  50                 | Conveyed__ A TY2 | Possesses__ A TY2 | Received__ A TY2
  51                 | Recognizes__ A TY2 | NeverMalFromSelf__ A B TY2
  52                 | Sends__ A TY2 B | SharedSecret__ A TY2 B
  53                 | Believes__ A TY3 | And__ TY3 TY3";;
  54
  55 (* ------------------------------------------------------------------------- *)
  56 (* Some with nesting of various kinds, plus required auxiliaries.            *)
  57 (* ------------------------------------------------------------------------- *)
  58
  59 let term_INDUCTION,term_RECURSION = time define_type
  60   "term = Vari int | Fni int (term list)";;
  61
  62 let bintree_INDUCTION,bintree_RECURSION = time define_type
  63   "bintree = Leafb | Branchb (bintree # bintree)";;
  64
  65 let etree_INDUCTION,etree_RECURSION = time define_type
  66   "etree = Terminal | Nonterminal (num + etree)";;
  67
  68 let ptree_INDUCTION,ptree_RECURSION = time define_type
  69   "ptree = Only (ptree option)";;
  70
  71 let mut_INDUCTION,mut_RECURSION = time define_type
  72   "mutual = Mutual A mutual D otherone | Friend D otherone;
  73    otherone = Great C | Expectations mutual otherone";;
  74
  75 let groof_INDUCTION,groof_RECURSION = time define_type
  76   "groof = Wu bool
  77          | Wibble (A,groof,L)mutual
  78          | Wobble groof groof";;
  79
  80 let biterm_INDUCTION,biterm_RECURSION = time define_type
  81   "biterm = Variab int
  82           | Fnapp (biterm list + biterm list)";;
  83
  84 let triterm_INDUCTION,triterm_RECURSION = time define_type
  85   "triterm = Var0 int
  86           | Fun2 (triterm list + triterm list)
  87           | Fun1 (triterm list)";;
  88
  89 let xtree_INDUCTION,xtree_RECURSION = time define_type
  90     "xtree = Leafx A
  91            | Branchx (xtree list)";;
  92
  93 let simper_INDUCTION,simper_RECURSION = time define_type
  94   "simper = Leaves A B
  95           | Bough (simper xtree)";;
  96
  97 let array_INDUCTION,array_RECURSION = time define_type
  98   "array = Array num (A list)";;
  99
 100 let value_INDUCTION,value_RECURSION = time define_type
 101   "value = Integer num
 102          | Boolean bool
 103          | List_of (value list)
 104          | Tree_of (value xtree)
 105          | Array_of (value array)";;
 106
 107 let example_INDUCTION,example_RECURSION = time define_type
 108   "command = Assignment (num list # expression list)
 109            | Sequence (command list);
 110    expression = Numeral num
 111               | Plus (expression # expression)
 112               | Valof command";;
 113
 114 let zonk_INDUCTION,zonk_RECURSION = time define_type
 115   "zonk = Stonk ((zonk,pink,A)mutual)list # expression
 116         | Tonk zonk (pink list)
 117         | Honk num;
 118    pink = Floyd (zonk # pink)
 119         | Purple num
 120         | Rain (A # pink)";;
 121
 122 (* ------------------------------------------------------------------------- *)
 123 (* Example from Konrad Slind: 68000 instruction set.                         *)
 124 (* ------------------------------------------------------------------------- *)
 125
 126 time define_type "Size = Byte | Word | Long";;
 127
 128 time define_type "DataRegister
 129               = RegD0
 130               | RegD1
 131               | RegD2
 132               | RegD3
 133               | RegD4
 134               | RegD5
 135               | RegD6
 136               | RegD7";;
 137
 138 time define_type "AddressRegister
 139               = RegA0
 140               | RegA1
 141               | RegA2
 142               | RegA3
 143               | RegA4
 144               | RegA5
 145               | RegA6
 146               | RegA7";;
 147
 148 time define_type "DataOrAddressRegister
 149               = data DataRegister
 150               | address AddressRegister";;
 151
 152 time define_type "Condition
 153               = Hi
 154               | Ls
 155               | Cc
 156               | Cs
 157               | Ne
 158               | Eq
 159               | Vc
 160               | Vs
 161               | Pl
 162               | Mi
 163               | Ge
 164               | Lt
 165               | Gt
 166               | Le";;
 167
 168 time define_type "AddressingMode
 169         = immediate num
 170         | direct DataOrAddressRegister
 171         | indirect AddressRegister
 172         | postinc AddressRegister
 173         | predec AddressRegister
 174         | indirectdisp num AddressRegister
 175         | indirectindex num AddressRegister DataOrAddressRegister Size
 176         | absolute num
 177         | pcdisp num
 178         | pcindex num DataOrAddressRegister Size";;
 179
 180 time define_type "M68kInstruction
 181     = ABCD AddressingMode AddressingMode
 182     | ADD Size AddressingMode AddressingMode
 183     | ADDA Size AddressingMode AddressRegister
 184     | ADDI Size num AddressingMode
 185     | ADDQ Size num AddressingMode
 186     | ADDX Size AddressingMode AddressingMode
 187     | AND Size AddressingMode AddressingMode
 188     | ANDI Size num AddressingMode
 189     | ANDItoCCR num
 190     | ANDItoSR num
 191     | ASL Size AddressingMode DataRegister
 192     | ASLW AddressingMode
 193     | ASR Size AddressingMode DataRegister
 194     | ASRW AddressingMode
 195     | Bcc Condition Size num
 196     | BTST Size AddressingMode AddressingMode
 197     | BCHG Size AddressingMode AddressingMode
 198     | BCLR Size AddressingMode AddressingMode
 199     | BSET Size AddressingMode AddressingMode
 200     | BRA Size num
 201     | BSR Size num
 202     | CHK AddressingMode DataRegister
 203     | CLR Size AddressingMode
 204     | CMP Size AddressingMode DataRegister
 205     | CMPA Size AddressingMode AddressRegister
 206     | CMPI Size num AddressingMode
 207     | CMPM Size AddressRegister AddressRegister
 208     | DBT DataRegister num
 209     | DBF DataRegister num
 210     | DBcc Condition DataRegister num
 211     | DIVS AddressingMode DataRegister
 212     | DIVU AddressingMode DataRegister
 213     | EOR Size DataRegister AddressingMode
 214     | EORI Size num AddressingMode
 215     | EORItoCCR num
 216     | EORItoSR num
 217     | EXG DataOrAddressRegister DataOrAddressRegister
 218     | EXT Size DataRegister
 219     | ILLEGAL
 220     | JMP AddressingMode
 221     | JSR AddressingMode
 222     | LEA AddressingMode AddressRegister
 223     | LINK AddressRegister num
 224     | LSL Size AddressingMode DataRegister
 225     | LSLW AddressingMode
 226     | LSR Size AddressingMode DataRegister
 227     | LSRW AddressingMode
 228     | MOVE Size AddressingMode AddressingMode
 229     | MOVEtoCCR AddressingMode
 230     | MOVEtoSR AddressingMode
 231     | MOVEfromSR AddressingMode
 232     | MOVEtoUSP AddressingMode
 233     | MOVEfromUSP AddressingMode
 234     | MOVEA Size AddressingMode AddressRegister
 235     | MOVEMto Size AddressingMode DataOrAddressRegister list
 236     | MOVEMfrom Size DataOrAddressRegister list AddressingMode
 237     | MOVEP Size AddressingMode AddressingMode
 238     | MOVEQ num DataRegister
 239     | MULS AddressingMode DataRegister
 240     | MULU AddressingMode DataRegister
 241     | NBCD AddressingMode
 242     | NEG Size AddressingMode
 243     | NEGX Size AddressingMode
 244     | NOP
 245     | NOT Size AddressingMode
 246     | OR Size AddressingMode AddressingMode
 247     | ORI Size num AddressingMode
 248     | ORItoCCR num
 249     | ORItoSR num
 250     | PEA AddressingMode
 251     | RESET
 252     | ROL Size AddressingMode DataRegister
 253     | ROLW AddressingMode
 254     | ROR Size AddressingMode DataRegister
 255     | RORW AddressingMode
 256     | ROXL Size AddressingMode DataRegister
 257     | ROXLW AddressingMode
 258     | ROXR Size AddressingMode DataRegister
 259     | ROXRW AddressingMode
 260     | RTE
 261     | RTR
 262     | RTS
 263     | SBCD AddressingMode AddressingMode
 264     | ST AddressingMode
 265     | SF AddressingMode
 266     | Scc Condition AddressingMode
 267     | STOP num
 268     | SUB Size AddressingMode AddressingMode
 269     | SUBA Size AddressingMode AddressingMode
 270     | SUBI Size num AddressingMode
 271     | SUBQ Size num AddressingMode
 272     | SUBX Size AddressingMode AddressingMode
 273     | SWAP DataRegister
 274     | TAS AddressingMode
 275     | TRAP num
 276     | TRAPV
 277     | TST Size AddressingMode
 278     | UNLK AddressRegister";;
 279
 280 (* ------------------------------------------------------------------------- *)
 281 (* Example from Myra VanInwegen: part of the syntax of SML.                  *)
 282 (* ------------------------------------------------------------------------- *)
 283
 284 let string_INDUCTION,string_RECURSION = time define_type
 285   "string = EMPTY_STRING | CONS_STRING num string";;
 286
 287 let strid_INDUCTION,strid_RECURSION = time define_type
 288   "strid = STRID string;
 289    var = VAR string;
 290    con = CON string;
 291    scon = SCINT int | SCSTR string;
 292    excon = EXCON string;
 293    label = LABEL string";;
 294
 295 let nonemptylist_INDUCTION,nonemptylist_RECURSION = time define_type
 296   "nonemptylist = Head_and_tail A (A list)";;
 297
 298 let long_INDUCTION,long_RECURSION = time define_type
 299   "long = BASE A | QUALIFIED strid long";;
 300
 301 let myra_INDUCTION,myra_RECURSION = time define_type
 302   "atpat_e = WILDCARDatpat_e
 303            | SCONatpat_e scon
 304            | VARatpat_e var
 305            | CONatpat_e (con long)
 306            | EXCONatpat_e (excon long)
 307            | RECORDatpat_e (patrow_e option)
 308            | PARatpat_e pat_e;
 309
 310    patrow_e = DOTDOTDOT_e
 311             | PATROW_e label pat_e (patrow_e option);
 312
 313    pat_e = ATPATpat_e atpat_e
 314          | CONpat_e (con long) atpat_e
 315          | EXCONpat_e (excon long) atpat_e
 316          | LAYEREDpat_e var pat_e;
 317
 318    conbind_e = CONBIND_e con (conbind_e option);
 319
 320    datbind_e = DATBIND_e conbind_e (datbind_e option);
 321
 322    exbind_e = EXBIND1_e excon (exbind_e option)
 323             | EXBIND2_e excon (excon long) (exbind_e option);
 324
 325    atexp_e = SCONatexp_e scon
 326            | VARatexp_e (var long)
 327            | CONatexp_e (con long)
 328            | EXCONatexp_e (excon long)
 329            | RECORDatexp_e (exprow_e option)
 330            | LETatexp_e dec_e exp_e
 331            | PARatexp_e exp_e;
 332
 333    exprow_e = EXPROW_e label exp_e (exprow_e option);
 334
 335    exp_e = ATEXPexp_e atexp_e
 336          | APPexp_e exp_e atexp_e
 337          | HANDLEexp_e exp_e match_e
 338          | RAISEexp_e exp_e
 339          | FNexp_e match_e;
 340
 341    match_e = MATCH_e mrule_e (match_e option);
 342
 343    mrule_e = MRULE_e pat_e exp_e;
 344
 345    dec_e = VALdec_e valbind_e
 346          | DATATYPEdec_e datbind_e
 347          | ABSTYPEdec_e datbind_e dec_e
 348          | EXCEPTdec_e exbind_e
 349          | LOCALdec_e dec_e dec_e
 350          | OPENdec_e ((strid long) nonemptylist)
 351          | EMPTYdec_e
 352          | SEQdec_e dec_e dec_e;
 353
 354    valbind_e = PLAINvalbind_e pat_e exp_e (valbind_e option)
 355              | RECvalbind_e valbind_e";;
 356
 357 (* ------------------------------------------------------------------------- *)
 358 (* Example from Daryl Stewart: a Verilog grammar.                            *)
 359 (* ------------------------------------------------------------------------- *)
 360
 361 let daryl_INDUCTION,daryl_RECURSION = time define_type
 362   "Source_text
 363      = module string (string list) (Module_item list)
 364      | Source_textMeta string;
 365   Module_item
 366      = declaration Declaration
 367      | initial Statement
 368      | always Statement
 369      | assign Lvalue Exprn
 370      | Module_itemMeta string;
 371   Declaration
 372      = reg_declaration (Range option) (string list)
 373      | net_declaration (Range option) (string list)
 374      | input_declaration (Range option) (string list)
 375      | output_declaration (Range option) (string list)
 376      | DeclarationMeta string;
 377   Range = range Exprn Exprn | RangeMeta string;
 378   Statement
 379      = clock_statement Clock Statement_or_null
 380      | blocking_assignment Lvalue Exprn
 381      | non_blocking_assignment Lvalue Exprn
 382      | conditional_statement
 383           Exprn Statement_or_null (Statement_or_null option)
 384      | case_statement Exprn (Case_item list)
 385      | while_loop Exprn Statement
 386      | repeat_loop Exprn Statement
 387      | for_loop
 388           Lvalue Exprn Exprn Lvalue Exprn Statement
 389      | forever_loop Statement
 390      | disable string
 391      | seq_block (string option) (Statement list)
 392      | StatementMeta string;
 393   Statement_or_null
 394      = statement Statement | null_statement | Statement_or_nullMeta string;
 395   Clock
 396      = posedge string
 397      | negedge string
 398      | clock string
 399      | ClockMeta string;
 400   Case_item
 401      = case_item (Exprn list) Statement_or_null
 402      | default_case_item Statement_or_null
 403      | Case_itemMeta string;
 404   Exprn
 405      = plus Exprn Exprn
 406      | minus Exprn Exprn
 407      | lshift Exprn Exprn
 408      | rshift Exprn Exprn
 409      | lt Exprn Exprn
 410      | leq Exprn Exprn
 411      | gt Exprn Exprn
 412      | geq Exprn Exprn
 413      | logeq Exprn Exprn
 414      | logneq Exprn Exprn
 415      | caseeq Exprn Exprn
 416      | caseneq Exprn Exprn
 417      | bitand Exprn Exprn
 418      | bitxor Exprn Exprn
 419      | bitor Exprn Exprn
 420      | logand Exprn Exprn
 421      | logor Exprn Exprn
 422      | conditional Exprn Exprn Exprn
 423      | positive Primary
 424      | negative Primary
 425      | lognot Primary
 426      | bitnot Primary
 427      | reducand Primary
 428      | reducxor Primary
 429      | reducor Primary
 430      | reducnand Primary
 431      | reducxnor Primary
 432      | reducnor Primary
 433      | primary Primary
 434      | ExpressionMeta string;
 435   Primary
 436      = primary_number Number
 437      | primary_IDENTIFIER string
 438      | primary_bit_select string Exprn
 439      | primary_part_select string Exprn Exprn
 440      | primary_gen_bit_select Exprn Exprn
 441      | primary_gen_part_select Exprn Exprn Exprn
 442      | primary_concatenation Concatenation
 443      | primary_multiple_concatenation Multiple_concatenation
 444      | brackets Exprn
 445      | PrimaryMeta string;
 446   Lvalue
 447      = lvalue string
 448      | lvalue_bit_select string Exprn
 449      | lvalue_part_select string Exprn Exprn
 450      | lvalue_concatenation Concatenation
 451      | LvalueMeta string;
 452   Number
 453      = decimal string
 454      | based string option string
 455      | NumberMeta string;
 456   Concatenation
 457      = concatenation (Exprn list) | ConcatenationMeta string;
 458   Multiple_concatenation
 459      = multiple_concatenation Exprn (Exprn list)
 460      | Multiple_concatenationMeta string;
 461   meta
 462      = Meta_Source_text Source_text
 463      | Meta_Module_item Module_item
 464      | Meta_Declaration Declaration
 465      | Meta_Range Range
 466      | Meta_Statement Statement
 467      | Meta_Statement_or_null Statement_or_null
 468      | Meta_Clock Clock
 469      | Meta_Case_item Case_item
 470      | Meta_Expression Exprn
 471      | Meta_Primary Primary
 472      | Meta_Lvalue Lvalue
 473      | Meta_Number Number
 474      | Meta_Concatenation Concatenation
 475      | Meta_Multiple_concatenation Multiple_concatenation";;