Ntrie/ntrie_tests.ml

   1 (* -*- holl -*- *)
   2
   3 (* ========================================================================= *)
   4 (* Conversions for ntries.                                                   *)
   5 (* ========================================================================= *)
   6
   7 (* ------------------------------------------------------------------------- *)
   8 (* NTRIE_IN_CONV                                                             *)
   9 (* ------------------------------------------------------------------------- *)
  10
  11 NTRIE_IN_CONV `2 IN NTRIE NEMPTY`;;
  12 NTRIE_IN_CONV `0 IN NTRIE NZERO`;;
  13 NTRIE_IN_CONV `0 IN NTRIE (NNODE NZERO NZERO)`;;
  14 NTRIE_IN_CONV `0 IN NTRIE (NNODE NZERO NZERO)`;;
  15 NTRIE_IN_CONV `1 IN NTRIE NZERO`;;
  16 NTRIE_IN_CONV `1 IN NTRIE (NNODE NEMPTY NZERO)`;;
  17 NTRIE_IN_CONV `1 IN NTRIE (NNODE NZERO NEMPTY)`;;
  18 NTRIE_IN_CONV `1 IN NTRIE (NNODE NZERO NZERO)`;;
  19 NTRIE_IN_CONV `2 IN NTRIE (NNODE NZERO NZERO)`;;
  20 NTRIE_IN_CONV `3 IN NTRIE (NNODE NZERO NZERO)`;;
  21
  22 (* ------------------------------------------------------------------------- *)
  23 (* NTRIE_EQ_CONV                                                             *)
  24 (* ------------------------------------------------------------------------- *)
  25
  26 NTRIE_EQ_CONV `NTRIE NEMPTY = NTRIE NZERO`;;
  27 NTRIE_EQ_CONV `NTRIE NZERO = NTRIE NZERO`;;
  28 NTRIE_EQ_CONV `NTRIE (NNODE NZERO NEMPTY) = NTRIE NZERO`;;
  29 NTRIE_EQ_CONV `NTRIE (NNODE NEMPTY NZERO) = NTRIE NZERO`;;
  30 NTRIE_EQ_CONV `NTRIE (NNODE NZERO NEMPTY) = NTRIE (NNODE NZERO NZERO)`;;
  31 NTRIE_EQ_CONV `NTRIE (NNODE NEMPTY NZERO) = NTRIE (NNODE NZERO NZERO)`;;
  32 NTRIE_EQ_CONV `NTRIE (NNODE NEMPTY NEMPTY) = NTRIE NEMPTY`;;
  33
  34 (* ------------------------------------------------------------------------- *)
  35 (* NTRIE_SUBSET_CONV                                                         *)
  36 (* ------------------------------------------------------------------------- *)
  37
  38 NTRIE_SUBSET_CONV `NTRIE NZERO SUBSET NTRIE NEMPTY`;;
  39 NTRIE_SUBSET_CONV `NTRIE NEMPTY SUBSET NTRIE NZERO`;;
  40 NTRIE_SUBSET_CONV
  41   `NTRIE (NNODE NZERO NEMPTY) SUBSET NTRIE (NNODE NZERO NZERO)`;;
  42 NTRIE_SUBSET_CONV
  43   `NTRIE (NNODE NEMPTY NZERO) SUBSET NTRIE (NNODE NZERO NZERO)`;;
  44
  45 (* ------------------------------------------------------------------------- *)
  46 (* NTRIE_DISJOINT_CONV                                                       *)
  47 (* ------------------------------------------------------------------------- *)
  48
  49 NTRIE_DISJOINT_CONV `DISJOINT (NTRIE NEMPTY) (NTRIE NEMPTY)`;;
  50 NTRIE_DISJOINT_CONV
  51   `DISJOINT (NTRIE (NNODE NEMPTY NZERO)) (NTRIE (NNODE NZERO NEMPTY))`;;
  52 NTRIE_DISJOINT_CONV
  53   `DISJOINT (NTRIE (NNODE NEMPTY NZERO)) (NTRIE (NNODE NEMPTY NZERO))`;;
  54
  55 (* ------------------------------------------------------------------------- *)
  56 (* NTRIE_SING_CONV                                                           *)
  57 (* ------------------------------------------------------------------------- *)
  58
  59 NTRIE_SING_CONV `{10}`;;
  60 NTRIE_SING_CONV `{1000}`;;
  61 NTRIE_SING_CONV `{100000}`;;
  62
  63 (* ------------------------------------------------------------------------- *)
  64 (* NTRIE_INSERT_CONV                                                         *)
  65 (* ------------------------------------------------------------------------- *)
  66
  67 NTRIE_INSERT_CONV `2 INSERT NTRIE NEMPTY`;;
  68 NTRIE_INSERT_CONV `0 INSERT NTRIE NZERO`;;
  69 NTRIE_INSERT_CONV `NUMERAL (BIT1 _0) INSERT NTRIE NZERO`;;
  70 NTRIE_INSERT_CONV `NUMERAL (BIT0 _0) INSERT NTRIE (NNODE NZERO NZERO)`;;
  71 NTRIE_INSERT_CONV `NUMERAL _0 INSERT NTRIE (NNODE NZERO NZERO)`;;
  72 NTRIE_INSERT_CONV `NUMERAL (BIT1 _0) INSERT NTRIE (NNODE NZERO NZERO)`;;
  73 NTRIE_INSERT_CONV `NUMERAL (BIT0 _0) INSERT NTRIE NZERO`;;
  74 NTRIE_INSERT_CONV `NUMERAL (BIT0 (BIT1 (BIT1 _0))) INSERT NTRIE NZERO`;;
  75
  76 (* ------------------------------------------------------------------------- *)
  77 (* NTRIE_UNION_CONV                                                          *)
  78 (* ------------------------------------------------------------------------- *)
  79
  80 NTRIE_UNION_CONV `NTRIE NEMPTY UNION NTRIE NEMPTY`;;
  81 NTRIE_UNION_CONV `NTRIE NEMPTY UNION NTRIE NZERO`;;
  82 NTRIE_UNION_CONV `NTRIE (NNODE NZERO NZERO) UNION NTRIE NZERO`;;
  83 NTRIE_UNION_CONV `NTRIE (NNODE NEMPTY NZERO) UNION NTRIE NZERO`;;
  84 NTRIE_UNION_CONV `NTRIE (NNODE NZERO NEMPTY) UNION NTRIE NZERO`;;
  85
  86 (* ------------------------------------------------------------------------- *)
  87 (* NTRIE_INTER_CONV                                                          *)
  88 (* ------------------------------------------------------------------------- *)
  89
  90 NTRIE_INTER_CONV `NTRIE NEMPTY INTER NTRIE NEMPTY`;;
  91 NTRIE_INTER_CONV `NTRIE NEMPTY INTER NTRIE NZERO`;;
  92 NTRIE_INTER_CONV `NTRIE (NNODE NZERO NZERO) INTER NTRIE NZERO`;;
  93 NTRIE_INTER_CONV `NTRIE (NNODE NEMPTY NZERO) INTER NTRIE NZERO`;;
  94 NTRIE_INTER_CONV `NTRIE (NNODE NZERO NEMPTY) INTER NTRIE NZERO`;;
  95 NTRIE_INTER_CONV
  96   `NTRIE (NNODE NEMPTY NEMPTY) INTER NTRIE (NNODE NEMPTY NEMPTY)`;;
  97
  98 (* ------------------------------------------------------------------------- *)
  99 (* NTRIE_DELETE_CONV                                                         *)
 100 (* ------------------------------------------------------------------------- *)
 101
 102 NTRIE_DELETE_CONV `NTRIE NEMPTY DELETE 0`;;
 103 NTRIE_DELETE_CONV `NTRIE NZERO DELETE 0`;;
 104 NTRIE_DELETE_CONV `NTRIE (NNODE NZERO NEMPTY) DELETE 0`;;
 105 NTRIE_DELETE_CONV `NTRIE (NNODE NEMPTY NZERO) DELETE 0`;;
 106 NTRIE_DELETE_CONV `NTRIE (NNODE NEMPTY NZERO) DELETE 1`;;
 107 NTRIE_DELETE_CONV `NTRIE (NNODE NZERO NEMPTY) DELETE 1`;;
 108
 109 (* ------------------------------------------------------------------------- *)
 110 (* NTRIE_DIFF_CONV                                                           *)
 111 (* ------------------------------------------------------------------------- *)
 112
 113 NTRIE_DIFF_CONV `NTRIE NEMPTY DIFF NTRIE NZERO`;;
 114 NTRIE_DIFF_CONV `NTRIE NZERO DIFF NTRIE NZERO`;;
 115 NTRIE_DIFF_CONV `NTRIE (NNODE NZERO NEMPTY) DIFF NTRIE (NNODE NZERO NEMPTY)`;;
 116 NTRIE_DIFF_CONV `NTRIE (NNODE NEMPTY NZERO) DIFF NTRIE (NNODE NZERO NEMPTY)`;;
 117 NTRIE_DIFF_CONV `NTRIE (NNODE NZERO NZERO) DIFF NTRIE (NNODE NEMPTY NZERO)`;;
 118 NTRIE_DIFF_CONV `NTRIE (NNODE NZERO NZERO) DIFF NTRIE (NNODE NZERO NEMPTY)`;;
 119
 120 (* ------------------------------------------------------------------------- *)
 121 (* NTRIE_IMAGE_CONV                                                          *)
 122 (* ------------------------------------------------------------------------- *)
 123
 124 NTRIE_IMAGE_CONV NUM_ADD_CONV `IMAGE ((+) 2) (NTRIE NEMPTY)`;;
 125 NTRIE_IMAGE_CONV NUM_ADD_CONV `IMAGE ((+) 2) (NTRIE NZERO)`;;
 126 NTRIE_IMAGE_CONV NUM_ADD_CONV `IMAGE ((+) 2) (NTRIE (NNODE NZERO NEMPTY))`;;
 127 NTRIE_IMAGE_CONV NUM_ADD_CONV `IMAGE ((+) 2) (NTRIE (NNODE NZERO NZERO))`;;
 128 NTRIE_IMAGE_CONV NUM_ADD_CONV `IMAGE ((+) 2) (NTRIE (NNODE NEMPTY NZERO))`;;
 129 NTRIE_IMAGE_CONV NUM_ADD_CONV `IMAGE ((+) 2) (NTRIE (NNODE NEMPTY NEMPTY))`;;
 130 NTRIE_IMAGE_CONV NUM_ADD_CONV `IMAGE ((+) 2) (NTRIE (NNODE (NNODE NEMPTY NZERO) NEMPTY))`;;
 131
 132 NTRIE_IMAGE_CONV NUM_ADD_CONV `IMAGE (\n. n + 2) (NTRIE NEMPTY)`;;
 133 NTRIE_IMAGE_CONV NUM_ADD_CONV `IMAGE (\n. n + 2) (NTRIE NZERO)`;;
 134 NTRIE_IMAGE_CONV NUM_ADD_CONV `IMAGE (\n. n + 2) (NTRIE (NNODE NZERO NEMPTY))`;;
 135 NTRIE_IMAGE_CONV NUM_ADD_CONV `IMAGE (\n. n + 2) (NTRIE (NNODE NZERO NZERO))`;;
 136 NTRIE_IMAGE_CONV NUM_ADD_CONV `IMAGE (\n. n + 2) (NTRIE (NNODE NEMPTY NZERO))`;;
 137 NTRIE_IMAGE_CONV NUM_ADD_CONV `IMAGE (\n. n + 2) (NTRIE (NNODE NEMPTY NEMPTY))`;;
 138 NTRIE_IMAGE_CONV NUM_ADD_CONV `IMAGE (\n. n + 2) (NTRIE (NNODE (NNODE NEMPTY NZERO) NEMPTY))`;;
 139 NTRIE_IMAGE_CONV NUM_ADD_CONV `IMAGE (\n. n + 2) (NTRIE (NNODE NEMPTY (NNODE NEMPTY NZERO)))`;;
 140
 141 (* ------------------------------------------------------------------------- *)
 142 (* NTRIE_DECODE                                                              *)
 143 (* ------------------------------------------------------------------------- *)
 144
 145 NTRIE_DECODE_CONV `NTRIE NEMPTY`;;
 146 NTRIE_DECODE_CONV `NTRIE NZERO`;;
 147 NTRIE_DECODE_CONV `NTRIE (NNODE NZERO NEMPTY)`;;
 148 NTRIE_DECODE_CONV `NTRIE (NNODE NZERO NZERO)`;;
 149 NTRIE_DECODE_CONV `NTRIE (NNODE NEMPTY NZERO)`;;
 150 NTRIE_DECODE_CONV `NTRIE (NNODE NEMPTY NEMPTY)`;;
 151 NTRIE_DECODE_CONV `NTRIE (NNODE (NNODE NEMPTY NZERO) NEMPTY)`;;
 152
 153 (* ------------------------------------------------------------------------- *)
 154 (* NTRIE_ENCODE                                                              *)
 155 (* ------------------------------------------------------------------------- *)
 156
 157 NTRIE_ENCODE_CONV `{}:num->bool`;;
 158 NTRIE_ENCODE_CONV `{1,2,3}`;;
 159 ONCE_DEPTH_CONV NTRIE_ENCODE_CONV `{1,2,3} UNION {3,4,5}`;;
 160
 161 (* ------------------------------------------------------------------------- *)
 162 (* Final hack-together.                                                      *)
 163 (* ------------------------------------------------------------------------- *)
 164
 165 NTRIE_COMPUTE NTRIE_REDUCE_CONV `{1,2,3} UNION ({3,4} UNION {6,7} UNION {1,7})`;;
 166 NTRIE_COMPUTE NTRIE_REDUCE_CONV `{1,2,3} INTER ({3,4} UNION {6,7} UNION {1,7})`;;
 167 NTRIE_COMPUTE NTRIE_REDUCE_CONV `{1,2,3} DIFF ({3,4} UNION {6,7} UNION {1,7})`;;
 168 NTRIE_COMPUTE NTRIE_REDUCE_CONV `{1,2,3} DIFF ({3,4} UNION {6,7} INTER {1,7})`;;
 169 NTRIE_COMPUTE NTRIE_REDUCE_CONV `3 IN {1,2,3} INTER ({3,4} UNION {6,7} UNION {1,7})`;;
 170 NTRIE_COMPUTE NTRIE_REDUCE_CONV `11 IN {1,2,3} INTER ({3,4} UNION {6,7} UNION {1,7})`;;
 171 NTRIE_COMPUTE NTRIE_REDUCE_CONV `{5,2,3} = {3,2,5}`;;
 172 NTRIE_COMPUTE NTRIE_REDUCE_CONV `{5,2,3,2} = {3,2,5}`;;
 173 NTRIE_COMPUTE NTRIE_REDUCE_CONV `{5,2,3,2} = {3,2,1,5}`;;
 174 NTRIE_COMPUTE NTRIE_REDUCE_CONV `{5,2,3,2} DELETE 2 = {3,5}`;;
 175 NTRIE_COMPUTE NTRIE_REDUCE_CONV `{5,2,3} SUBSET {3,2,5}`;;
 176 NTRIE_COMPUTE NTRIE_REDUCE_CONV `{5,2,3,7} SUBSET {3,2,5}`;;
 177 NTRIE_COMPUTE NTRIE_REDUCE_CONV `{5,2,3,2} SUBSET {3,2,1,5}`;;
 178 NTRIE_COMPUTE NTRIE_REDUCE_CONV `{5,2,3} PSUBSET {3,2,5}`;;
 179 NTRIE_COMPUTE NTRIE_REDUCE_CONV `{5,2,3} PSUBSET {3,2,0,5}`;;
 180 NTRIE_COMPUTE NTRIE_REDUCE_CONV `DISJOINT {12,3,2,1} {3,2,7,9}`;;
 181 NTRIE_COMPUTE NTRIE_REDUCE_CONV `DISJOINT {12,3,1} {2,7,9}`;;