ARM/v7/arm_random_testingLib.sml

139     fun dp () = case rand_term ``:word4 -> bool -> 'reg word -> 'reg word ->
167     fun mul () = case rand_term ``:bool -> bool -> 'reg word -> 'reg word ->
168                                   'reg word -> 'reg word``
176                                   'reg word -> 'reg word``
228                                            hd (rand_term ``:'reg word``)))
236                                   'reg word -> 'reg word -> addressing_mode3``
283     fun lsm () = case rand_term ``:bool -> bool -> bool -> 'reg word``
307                       r2 I ``:'reg word -> 'reg word``
308     fun lsd load = case rand_term ``:bool -> bool -> bool -> 'reg word ->
339           optionSyntax.mk_none (if t = ``:'mode word`` then ``:word5`` else t)
372                    ``:word5 -> word2 -> 'reg word``
374                    ``:'reg word -> word2 -> 'reg word``
386                    hd (rand_term ``:'reg word``))
412                          (hd (rand_term ``:'offset word``))
414                          (hd (rand_term ``:'reg word``))
416                          ``:bool -> bool -> 'offset word``
418                          (hd (rand_term ``:'reg word``))
423                          (hd (rand_term ``:'offset word``))
425                          ``:bool -> bool -> 'offset word``
427                          ``:'reg word -> bool -> 'reg word``
432                          (hd (rand_term ``:'offset word``))
434                          (hd (rand_term ``:'reg word``))
436                          (hd (rand_term ``:'reg word``))
442             of 0 => r2 arm_astSyntax.mk_Check_Array ``:'reg word -> 'reg word``
454                      ``:bool -> 'reg word -> 'reg word -> word12``
457                      ``:bool -> 'areg word -> 'reg word -> word2 -> 'reg word``
459                      ``:bool -> 'areg word -> 'reg word -> word2 -> 'reg word``
461                      ``:'reg word -> 'reg word``
463                      ``:'reg word -> 'reg word``
465                      ``:'reg word -> 'reg word``
467                      ``:bool -> 'reg word -> word16``
469                      ``:'reg word -> 'reg word -> 'reg word -> 'reg word``
471                      ``:word2 -> bool -> bool -> 'reg word -> 'reg word ->
472                         'reg word -> 'reg word``
474                      ``:'reg word -> 'areg word -> 'reg word -> bool -> bool ->
475                         'reg word``
477                      ``:'reg word -> 'reg word -> 'reg word -> bool -> bool ->
478                         'reg word``
480                      ``:'reg word -> 'areg word -> 'reg word -> bool ->
481                         'reg word``
483                      ``:'reg word -> 'reg word -> 'reg word -> bool ->
484                         'reg word``
486                      ``:bool -> bool -> bool -> 'reg word -> 'reg word ->
487                         'reg word -> 'reg word``
489                      ``:'reg word -> 'reg word -> 'reg word -> 'reg word``
491                      ``:bool -> word5 -> 'reg word -> word5 -> bool ->
492                         'reg word``
494                      ``:bool -> word4 -> 'reg word -> 'reg word``
496                      ``:word2 -> 'reg word -> 'reg word -> 'reg word``
498                      ``:'reg word -> 'reg word -> word5 -> bool -> 'reg word``
500                      ``:bool -> 'areg word -> 'reg word -> word2 -> 'reg word``
502                      ``:word5 -> 'reg word -> word5 -> 'areg word``
504                      ``:'reg word -> 'reg word``
506                      ``:'reg word -> 'reg word``
508                      ``:bool -> word5 -> 'reg word -> word5 -> 'reg word``
510                      ``:'reg word -> 'reg word -> 'reg word``
512                      ``:'reg word -> 'areg word -> 'reg word -> 'reg word``
515                         'reg word -> 'reg word -> 'reg word``
517                      ``:bool -> 'reg word -> 'reg word -> 'reg word``
523         of 0 => r2 arm_astSyntax.mk_Status_to_Register ``:bool -> 'reg word``
525                      ``:bool -> word4 -> 'reg word``
529                      ``:word2 -> bool -> bool -> bool -> 'mode word option``
545                       ``:'reg word -> 'reg word -> word8``
548                      (hd (rand_term  ``:'reg word``), t, t2)
551                       ``:'reg word -> 'reg word``
553                       ``:'reg word -> 'reg word``
555                       ``:bool -> bool -> bool -> 'mode word``
557                       ``:bool -> bool -> bool -> 'reg word``
559                       ``:'reg word -> 'reg word -> 'reg word``
561                       ``:'reg word -> 'reg word -> 'reg word -> word8``
563                       ``:'reg word -> 'reg word -> 'reg word``
565                       val (n,d) = r2 I ``:'reg word -> 'reg word``
603                         ``:bool -> 'reg word -> 'reg word -> 'reg word``