Changeset 2717 for extracted/aSM.mli
 Timestamp:
 Feb 23, 2013, 1:16:55 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/aSM.mli
r2649 r2717 60 60 61 61 open Identifiers 62 63 open BitVectorTrie 64 65 open Exp 62 66 63 67 open Arithmetic … … 433 437  RETI 434 438  NOP 439  JMP of subaddressing_mode 435 440 436 441 val preinstruction_rect_Type4 : … … 466 471 'a2) > (subaddressing_mode > 'a2) > (subaddressing_mode > 'a2) > 467 472 (subaddressing_mode > subaddressing_mode > 'a2) > (subaddressing_mode > 468 subaddressing_mode > 'a2) > 'a2 > 'a2 > 'a2 > 'a1 preinstruction>469 'a2 473 subaddressing_mode > 'a2) > 'a2 > 'a2 > 'a2 > (subaddressing_mode > 474 'a2) > 'a1 preinstruction > 'a2 470 475 471 476 val preinstruction_rect_Type5 : … … 501 506 'a2) > (subaddressing_mode > 'a2) > (subaddressing_mode > 'a2) > 502 507 (subaddressing_mode > subaddressing_mode > 'a2) > (subaddressing_mode > 503 subaddressing_mode > 'a2) > 'a2 > 'a2 > 'a2 > 'a1 preinstruction>504 'a2 508 subaddressing_mode > 'a2) > 'a2 > 'a2 > 'a2 > (subaddressing_mode > 509 'a2) > 'a1 preinstruction > 'a2 505 510 506 511 val preinstruction_rect_Type3 : … … 536 541 'a2) > (subaddressing_mode > 'a2) > (subaddressing_mode > 'a2) > 537 542 (subaddressing_mode > subaddressing_mode > 'a2) > (subaddressing_mode > 538 subaddressing_mode > 'a2) > 'a2 > 'a2 > 'a2 > 'a1 preinstruction>539 'a2 543 subaddressing_mode > 'a2) > 'a2 > 'a2 > 'a2 > (subaddressing_mode > 544 'a2) > 'a1 preinstruction > 'a2 540 545 541 546 val preinstruction_rect_Type2 : … … 571 576 'a2) > (subaddressing_mode > 'a2) > (subaddressing_mode > 'a2) > 572 577 (subaddressing_mode > subaddressing_mode > 'a2) > (subaddressing_mode > 573 subaddressing_mode > 'a2) > 'a2 > 'a2 > 'a2 > 'a1 preinstruction>574 'a2 578 subaddressing_mode > 'a2) > 'a2 > 'a2 > 'a2 > (subaddressing_mode > 579 'a2) > 'a1 preinstruction > 'a2 575 580 576 581 val preinstruction_rect_Type1 : … … 606 611 'a2) > (subaddressing_mode > 'a2) > (subaddressing_mode > 'a2) > 607 612 (subaddressing_mode > subaddressing_mode > 'a2) > (subaddressing_mode > 608 subaddressing_mode > 'a2) > 'a2 > 'a2 > 'a2 > 'a1 preinstruction>609 'a2 613 subaddressing_mode > 'a2) > 'a2 > 'a2 > 'a2 > (subaddressing_mode > 614 'a2) > 'a1 preinstruction > 'a2 610 615 611 616 val preinstruction_rect_Type0 : … … 641 646 'a2) > (subaddressing_mode > 'a2) > (subaddressing_mode > 'a2) > 642 647 (subaddressing_mode > subaddressing_mode > 'a2) > (subaddressing_mode > 643 subaddressing_mode > 'a2) > 'a2 > 'a2 > 'a2 > 'a1 preinstruction>644 'a2 648 subaddressing_mode > 'a2) > 'a2 > 'a2 > 'a2 > (subaddressing_mode > 649 'a2) > 'a1 preinstruction > 'a2 645 650 646 651 val preinstruction_inv_rect_Type4 : … … 680 685 subaddressing_mode > __ > 'a2) > (subaddressing_mode > 681 686 subaddressing_mode > __ > 'a2) > (__ > 'a2) > (__ > 'a2) > (__ > 682 'a2) > 'a2687 'a2) > (subaddressing_mode > __ > 'a2) > 'a2 683 688 684 689 val preinstruction_inv_rect_Type3 : … … 718 723 subaddressing_mode > __ > 'a2) > (subaddressing_mode > 719 724 subaddressing_mode > __ > 'a2) > (__ > 'a2) > (__ > 'a2) > (__ > 720 'a2) > 'a2725 'a2) > (subaddressing_mode > __ > 'a2) > 'a2 721 726 722 727 val preinstruction_inv_rect_Type2 : … … 756 761 subaddressing_mode > __ > 'a2) > (subaddressing_mode > 757 762 subaddressing_mode > __ > 'a2) > (__ > 'a2) > (__ > 'a2) > (__ > 758 'a2) > 'a2763 'a2) > (subaddressing_mode > __ > 'a2) > 'a2 759 764 760 765 val preinstruction_inv_rect_Type1 : … … 794 799 subaddressing_mode > __ > 'a2) > (subaddressing_mode > 795 800 subaddressing_mode > __ > 'a2) > (__ > 'a2) > (__ > 'a2) > (__ > 796 'a2) > 'a2801 'a2) > (subaddressing_mode > __ > 'a2) > 'a2 797 802 798 803 val preinstruction_inv_rect_Type0 : … … 832 837 subaddressing_mode > __ > 'a2) > (subaddressing_mode > 833 838 subaddressing_mode > __ > 'a2) > (__ > 'a2) > (__ > 'a2) > (__ > 834 'a2) > 'a2839 'a2) > (subaddressing_mode > __ > 'a2) > 'a2 835 840 836 841 val preinstruction_discr : 'a1 preinstruction > 'a1 preinstruction > __ … … 848 853  LJMP of subaddressing_mode 849 854  SJMP of subaddressing_mode 850  JMP of subaddressing_mode851 855  MOVC of subaddressing_mode * subaddressing_mode 852 856  RealInstruction of subaddressing_mode preinstruction … … 855 859 (subaddressing_mode > 'a1) > (subaddressing_mode > 'a1) > 856 860 (subaddressing_mode > 'a1) > (subaddressing_mode > 'a1) > 857 (subaddressing_mode > 'a1) > (subaddressing_mode > 'a1) > 858 (subaddressing_mode > subaddressing_mode > 'a1) > (subaddressing_mode 859 preinstruction > 'a1) > instruction > 'a1 861 (subaddressing_mode > 'a1) > (subaddressing_mode > subaddressing_mode > 862 'a1) > (subaddressing_mode preinstruction > 'a1) > instruction > 'a1 860 863 861 864 val instruction_rect_Type5 : 862 865 (subaddressing_mode > 'a1) > (subaddressing_mode > 'a1) > 863 866 (subaddressing_mode > 'a1) > (subaddressing_mode > 'a1) > 864 (subaddressing_mode > 'a1) > (subaddressing_mode > 'a1) > 865 (subaddressing_mode > subaddressing_mode > 'a1) > (subaddressing_mode 866 preinstruction > 'a1) > instruction > 'a1 867 (subaddressing_mode > 'a1) > (subaddressing_mode > subaddressing_mode > 868 'a1) > (subaddressing_mode preinstruction > 'a1) > instruction > 'a1 867 869 868 870 val instruction_rect_Type3 : 869 871 (subaddressing_mode > 'a1) > (subaddressing_mode > 'a1) > 870 872 (subaddressing_mode > 'a1) > (subaddressing_mode > 'a1) > 871 (subaddressing_mode > 'a1) > (subaddressing_mode > 'a1) > 872 (subaddressing_mode > subaddressing_mode > 'a1) > (subaddressing_mode 873 preinstruction > 'a1) > instruction > 'a1 873 (subaddressing_mode > 'a1) > (subaddressing_mode > subaddressing_mode > 874 'a1) > (subaddressing_mode preinstruction > 'a1) > instruction > 'a1 874 875 875 876 val instruction_rect_Type2 : 876 877 (subaddressing_mode > 'a1) > (subaddressing_mode > 'a1) > 877 878 (subaddressing_mode > 'a1) > (subaddressing_mode > 'a1) > 878 (subaddressing_mode > 'a1) > (subaddressing_mode > 'a1) > 879 (subaddressing_mode > subaddressing_mode > 'a1) > (subaddressing_mode 880 preinstruction > 'a1) > instruction > 'a1 879 (subaddressing_mode > 'a1) > (subaddressing_mode > subaddressing_mode > 880 'a1) > (subaddressing_mode preinstruction > 'a1) > instruction > 'a1 881 881 882 882 val instruction_rect_Type1 : 883 883 (subaddressing_mode > 'a1) > (subaddressing_mode > 'a1) > 884 884 (subaddressing_mode > 'a1) > (subaddressing_mode > 'a1) > 885 (subaddressing_mode > 'a1) > (subaddressing_mode > 'a1) > 886 (subaddressing_mode > subaddressing_mode > 'a1) > (subaddressing_mode 887 preinstruction > 'a1) > instruction > 'a1 885 (subaddressing_mode > 'a1) > (subaddressing_mode > subaddressing_mode > 886 'a1) > (subaddressing_mode preinstruction > 'a1) > instruction > 'a1 888 887 889 888 val instruction_rect_Type0 : 890 889 (subaddressing_mode > 'a1) > (subaddressing_mode > 'a1) > 891 890 (subaddressing_mode > 'a1) > (subaddressing_mode > 'a1) > 892 (subaddressing_mode > 'a1) > (subaddressing_mode > 'a1) > 893 (subaddressing_mode > subaddressing_mode > 'a1) > (subaddressing_mode 894 preinstruction > 'a1) > instruction > 'a1 891 (subaddressing_mode > 'a1) > (subaddressing_mode > subaddressing_mode > 892 'a1) > (subaddressing_mode preinstruction > 'a1) > instruction > 'a1 895 893 896 894 val instruction_inv_rect_Type4 : … … 898 896 __ > 'a1) > (subaddressing_mode > __ > 'a1) > (subaddressing_mode > 899 897 __ > 'a1) > (subaddressing_mode > __ > 'a1) > (subaddressing_mode > 900 __ > 'a1) > (subaddressing_mode > subaddressing_mode > __ > 'a1)>901 (subaddressing_mode preinstruction >__ > 'a1) > 'a1898 subaddressing_mode > __ > 'a1) > (subaddressing_mode preinstruction > 899 __ > 'a1) > 'a1 902 900 903 901 val instruction_inv_rect_Type3 : … … 905 903 __ > 'a1) > (subaddressing_mode > __ > 'a1) > (subaddressing_mode > 906 904 __ > 'a1) > (subaddressing_mode > __ > 'a1) > (subaddressing_mode > 907 __ > 'a1) > (subaddressing_mode > subaddressing_mode > __ > 'a1)>908 (subaddressing_mode preinstruction >__ > 'a1) > 'a1905 subaddressing_mode > __ > 'a1) > (subaddressing_mode preinstruction > 906 __ > 'a1) > 'a1 909 907 910 908 val instruction_inv_rect_Type2 : … … 912 910 __ > 'a1) > (subaddressing_mode > __ > 'a1) > (subaddressing_mode > 913 911 __ > 'a1) > (subaddressing_mode > __ > 'a1) > (subaddressing_mode > 914 __ > 'a1) > (subaddressing_mode > subaddressing_mode > __ > 'a1)>915 (subaddressing_mode preinstruction >__ > 'a1) > 'a1912 subaddressing_mode > __ > 'a1) > (subaddressing_mode preinstruction > 913 __ > 'a1) > 'a1 916 914 917 915 val instruction_inv_rect_Type1 : … … 919 917 __ > 'a1) > (subaddressing_mode > __ > 'a1) > (subaddressing_mode > 920 918 __ > 'a1) > (subaddressing_mode > __ > 'a1) > (subaddressing_mode > 921 __ > 'a1) > (subaddressing_mode > subaddressing_mode > __ > 'a1)>922 (subaddressing_mode preinstruction >__ > 'a1) > 'a1919 subaddressing_mode > __ > 'a1) > (subaddressing_mode preinstruction > 920 __ > 'a1) > 'a1 923 921 924 922 val instruction_inv_rect_Type0 : … … 926 924 __ > 'a1) > (subaddressing_mode > __ > 'a1) > (subaddressing_mode > 927 925 __ > 'a1) > (subaddressing_mode > __ > 'a1) > (subaddressing_mode > 928 __ > 'a1) > (subaddressing_mode > subaddressing_mode > __ > 'a1)>929 (subaddressing_mode preinstruction >__ > 'a1) > 'a1926 subaddressing_mode > __ > 'a1) > (subaddressing_mode preinstruction > 927 __ > 'a1) > 'a1 930 928 931 929 val instruction_discr : instruction > instruction > __ … … 934 932 935 933 val eq_instruction : instruction > instruction > Bool.bool 934 935 type word_side = 936  HIGH 937  LOW 938 939 val word_side_rect_Type4 : 'a1 > 'a1 > word_side > 'a1 940 941 val word_side_rect_Type5 : 'a1 > 'a1 > word_side > 'a1 942 943 val word_side_rect_Type3 : 'a1 > 'a1 > word_side > 'a1 944 945 val word_side_rect_Type2 : 'a1 > 'a1 > word_side > 'a1 946 947 val word_side_rect_Type1 : 'a1 > 'a1 > word_side > 'a1 948 949 val word_side_rect_Type0 : 'a1 > 'a1 > word_side > 'a1 950 951 val word_side_inv_rect_Type4 : word_side > (__ > 'a1) > (__ > 'a1) > 'a1 952 953 val word_side_inv_rect_Type3 : word_side > (__ > 'a1) > (__ > 'a1) > 'a1 954 955 val word_side_inv_rect_Type2 : word_side > (__ > 'a1) > (__ > 'a1) > 'a1 956 957 val word_side_inv_rect_Type1 : word_side > (__ > 'a1) > (__ > 'a1) > 'a1 958 959 val word_side_inv_rect_Type0 : word_side > (__ > 'a1) > (__ > 'a1) > 'a1 960 961 val word_side_discr : word_side > word_side > __ 962 963 val word_side_jmdiscr : word_side > word_side > __ 936 964 937 965 type pseudo_instruction = … … 940 968  Cost of CostLabel.costlabel 941 969  Jmp of identifier0 970  Jnz of subaddressing_mode * identifier0 * identifier0 971  MovSuccessor of subaddressing_mode * word_side * identifier0 942 972  Call of identifier0 943 973  Mov of subaddressing_mode * identifier0 … … 945 975 val pseudo_instruction_rect_Type4 : 946 976 (identifier0 preinstruction > 'a1) > (String.string > 'a1) > 947 (CostLabel.costlabel > 'a1) > (identifier0 > 'a1) > (identifier0 > 948 'a1) > (subaddressing_mode > identifier0 > 'a1) > pseudo_instruction > 949 'a1 977 (CostLabel.costlabel > 'a1) > (identifier0 > 'a1) > (subaddressing_mode 978 > identifier0 > identifier0 > 'a1) > (subaddressing_mode > word_side 979 > identifier0 > 'a1) > (identifier0 > 'a1) > (subaddressing_mode > 980 identifier0 > 'a1) > pseudo_instruction > 'a1 950 981 951 982 val pseudo_instruction_rect_Type5 : 952 983 (identifier0 preinstruction > 'a1) > (String.string > 'a1) > 953 (CostLabel.costlabel > 'a1) > (identifier0 > 'a1) > (identifier0 > 954 'a1) > (subaddressing_mode > identifier0 > 'a1) > pseudo_instruction > 955 'a1 984 (CostLabel.costlabel > 'a1) > (identifier0 > 'a1) > (subaddressing_mode 985 > identifier0 > identifier0 > 'a1) > (subaddressing_mode > word_side 986 > identifier0 > 'a1) > (identifier0 > 'a1) > (subaddressing_mode > 987 identifier0 > 'a1) > pseudo_instruction > 'a1 956 988 957 989 val pseudo_instruction_rect_Type3 : 958 990 (identifier0 preinstruction > 'a1) > (String.string > 'a1) > 959 (CostLabel.costlabel > 'a1) > (identifier0 > 'a1) > (identifier0 > 960 'a1) > (subaddressing_mode > identifier0 > 'a1) > pseudo_instruction > 961 'a1 991 (CostLabel.costlabel > 'a1) > (identifier0 > 'a1) > (subaddressing_mode 992 > identifier0 > identifier0 > 'a1) > (subaddressing_mode > word_side 993 > identifier0 > 'a1) > (identifier0 > 'a1) > (subaddressing_mode > 994 identifier0 > 'a1) > pseudo_instruction > 'a1 962 995 963 996 val pseudo_instruction_rect_Type2 : 964 997 (identifier0 preinstruction > 'a1) > (String.string > 'a1) > 965 (CostLabel.costlabel > 'a1) > (identifier0 > 'a1) > (identifier0 > 966 'a1) > (subaddressing_mode > identifier0 > 'a1) > pseudo_instruction > 967 'a1 998 (CostLabel.costlabel > 'a1) > (identifier0 > 'a1) > (subaddressing_mode 999 > identifier0 > identifier0 > 'a1) > (subaddressing_mode > word_side 1000 > identifier0 > 'a1) > (identifier0 > 'a1) > (subaddressing_mode > 1001 identifier0 > 'a1) > pseudo_instruction > 'a1 968 1002 969 1003 val pseudo_instruction_rect_Type1 : 970 1004 (identifier0 preinstruction > 'a1) > (String.string > 'a1) > 971 (CostLabel.costlabel > 'a1) > (identifier0 > 'a1) > (identifier0 > 972 'a1) > (subaddressing_mode > identifier0 > 'a1) > pseudo_instruction > 973 'a1 1005 (CostLabel.costlabel > 'a1) > (identifier0 > 'a1) > (subaddressing_mode 1006 > identifier0 > identifier0 > 'a1) > (subaddressing_mode > word_side 1007 > identifier0 > 'a1) > (identifier0 > 'a1) > (subaddressing_mode > 1008 identifier0 > 'a1) > pseudo_instruction > 'a1 974 1009 975 1010 val pseudo_instruction_rect_Type0 : 976 1011 (identifier0 preinstruction > 'a1) > (String.string > 'a1) > 977 (CostLabel.costlabel > 'a1) > (identifier0 > 'a1) > (identifier0 > 978 'a1) > (subaddressing_mode > identifier0 > 'a1) > pseudo_instruction > 979 'a1 1012 (CostLabel.costlabel > 'a1) > (identifier0 > 'a1) > (subaddressing_mode 1013 > identifier0 > identifier0 > 'a1) > (subaddressing_mode > word_side 1014 > identifier0 > 'a1) > (identifier0 > 'a1) > (subaddressing_mode > 1015 identifier0 > 'a1) > pseudo_instruction > 'a1 980 1016 981 1017 val pseudo_instruction_inv_rect_Type4 : 982 1018 pseudo_instruction > (identifier0 preinstruction > __ > 'a1) > 983 1019 (String.string > __ > 'a1) > (CostLabel.costlabel > __ > 'a1) > 984 (identifier0 > __ > 'a1) > (identifier0 > __ > 'a1) > 1020 (identifier0 > __ > 'a1) > (subaddressing_mode > identifier0 > 1021 identifier0 > __ > 'a1) > (subaddressing_mode > word_side > 1022 identifier0 > __ > 'a1) > (identifier0 > __ > 'a1) > 985 1023 (subaddressing_mode > identifier0 > __ > 'a1) > 'a1 986 1024 … … 988 1026 pseudo_instruction > (identifier0 preinstruction > __ > 'a1) > 989 1027 (String.string > __ > 'a1) > (CostLabel.costlabel > __ > 'a1) > 990 (identifier0 > __ > 'a1) > (identifier0 > __ > 'a1) > 1028 (identifier0 > __ > 'a1) > (subaddressing_mode > identifier0 > 1029 identifier0 > __ > 'a1) > (subaddressing_mode > word_side > 1030 identifier0 > __ > 'a1) > (identifier0 > __ > 'a1) > 991 1031 (subaddressing_mode > identifier0 > __ > 'a1) > 'a1 992 1032 … … 994 1034 pseudo_instruction > (identifier0 preinstruction > __ > 'a1) > 995 1035 (String.string > __ > 'a1) > (CostLabel.costlabel > __ > 'a1) > 996 (identifier0 > __ > 'a1) > (identifier0 > __ > 'a1) > 1036 (identifier0 > __ > 'a1) > (subaddressing_mode > identifier0 > 1037 identifier0 > __ > 'a1) > (subaddressing_mode > word_side > 1038 identifier0 > __ > 'a1) > (identifier0 > __ > 'a1) > 997 1039 (subaddressing_mode > identifier0 > __ > 'a1) > 'a1 998 1040 … … 1000 1042 pseudo_instruction > (identifier0 preinstruction > __ > 'a1) > 1001 1043 (String.string > __ > 'a1) > (CostLabel.costlabel > __ > 'a1) > 1002 (identifier0 > __ > 'a1) > (identifier0 > __ > 'a1) > 1044 (identifier0 > __ > 'a1) > (subaddressing_mode > identifier0 > 1045 identifier0 > __ > 'a1) > (subaddressing_mode > word_side > 1046 identifier0 > __ > 'a1) > (identifier0 > __ > 'a1) > 1003 1047 (subaddressing_mode > identifier0 > __ > 'a1) > 'a1 1004 1048 … … 1006 1050 pseudo_instruction > (identifier0 preinstruction > __ > 'a1) > 1007 1051 (String.string > __ > 'a1) > (CostLabel.costlabel > __ > 'a1) > 1008 (identifier0 > __ > 'a1) > (identifier0 > __ > 'a1) > 1052 (identifier0 > __ > 'a1) > (subaddressing_mode > identifier0 > 1053 identifier0 > __ > 'a1) > (subaddressing_mode > word_side > 1054 identifier0 > __ > 'a1) > (identifier0 > __ > 'a1) > 1009 1055 (subaddressing_mode > identifier0 > __ > 'a1) > 'a1 1010 1056 … … 1016 1062 type labelled_instruction = pseudo_instruction LabelledObjects.labelled_obj 1017 1063 1018 type preamble = 1019 (Nat.nat Identifiers.identifier_map, (identifier0, BitVector.word) 1020 Types.prod List.list) Types.prod 1064 type preamble = (identifier0, BitVector.word) Types.prod List.list 1021 1065 1022 1066 type assembly_program = instruction List.list
Note: See TracChangeset
for help on using the changeset viewer.