matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_aux_bases.ml

   1 type oct =
   2 O0
   3  | O1
   4  | O2
   5  | O3
   6  | O4
   7  | O5
   8  | O6
   9  | O7
  10 ;;
  11
  12 let oct_rec =
  13 (function p -> (function p1 -> (function p2 -> (function p3 -> (function p4 -> (function p5 -> (function p6 -> (function p7 -> (function o ->
  14 (match o with
  15    O0 -> p
  16  | O1 -> p1
  17  | O2 -> p2
  18  | O3 -> p3
  19  | O4 -> p4
  20  | O5 -> p5
  21  | O6 -> p6
  22  | O7 -> p7)
  23 )))))))))
  24 ;;
  25
  26 let oct_rect =
  27 (function p -> (function p1 -> (function p2 -> (function p3 -> (function p4 -> (function p5 -> (function p6 -> (function p7 -> (function o ->
  28 (match o with
  29    O0 -> p
  30  | O1 -> p1
  31  | O2 -> p2
  32  | O3 -> p3
  33  | O4 -> p4
  34  | O5 -> p5
  35  | O6 -> p6
  36  | O7 -> p7)
  37 )))))))))
  38 ;;
  39
  40 let exadecim_of_oct =
  41 (function o ->
  42 (match o with
  43    O0 -> Matita_freescale_exadecim.X0
  44  | O1 -> Matita_freescale_exadecim.X1
  45  | O2 -> Matita_freescale_exadecim.X2
  46  | O3 -> Matita_freescale_exadecim.X3
  47  | O4 -> Matita_freescale_exadecim.X4
  48  | O5 -> Matita_freescale_exadecim.X5
  49  | O6 -> Matita_freescale_exadecim.X6
  50  | O7 -> Matita_freescale_exadecim.X7)
  51 )
  52 ;;
  53
  54 let nat_OF_oct =
  55 (function a -> (Matita_freescale_exadecim.nat_of_exadecim (exadecim_of_oct a)))
  56 ;;
  57
  58 let forall_oct =
  59 (function p -> (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (p O0) (p O1)) (p O2)) (p O3)) (p O4)) (p O5)) (p O6)) (p O7)))
  60 ;;
  61
  62 type bitrigesim =
  63 T00
  64  | T01
  65  | T02
  66  | T03
  67  | T04
  68  | T05
  69  | T06
  70  | T07
  71  | T08
  72  | T09
  73  | T0A
  74  | T0B
  75  | T0C
  76  | T0D
  77  | T0E
  78  | T0F
  79  | T10
  80  | T11
  81  | T12
  82  | T13
  83  | T14
  84  | T15
  85  | T16
  86  | T17
  87  | T18
  88  | T19
  89  | T1A
  90  | T1B
  91  | T1C
  92  | T1D
  93  | T1E
  94  | T1F
  95 ;;
  96
  97 let bitrigesim_rec =
  98 (function p -> (function p1 -> (function p2 -> (function p3 -> (function p4 -> (function p5 -> (function p6 -> (function p7 -> (function p8 -> (function p9 -> (function p10 -> (function p11 -> (function p12 -> (function p13 -> (function p14 -> (function p15 -> (function p16 -> (function p17 -> (function p18 -> (function p19 -> (function p20 -> (function p21 -> (function p22 -> (function p23 -> (function p24 -> (function p25 -> (function p26 -> (function p27 -> (function p28 -> (function p29 -> (function p30 -> (function p31 -> (function b ->
  99 (match b with
 100    T00 -> p
 101  | T01 -> p1
 102  | T02 -> p2
 103  | T03 -> p3
 104  | T04 -> p4
 105  | T05 -> p5
 106  | T06 -> p6
 107  | T07 -> p7
 108  | T08 -> p8
 109  | T09 -> p9
 110  | T0A -> p10
 111  | T0B -> p11
 112  | T0C -> p12
 113  | T0D -> p13
 114  | T0E -> p14
 115  | T0F -> p15
 116  | T10 -> p16
 117  | T11 -> p17
 118  | T12 -> p18
 119  | T13 -> p19
 120  | T14 -> p20
 121  | T15 -> p21
 122  | T16 -> p22
 123  | T17 -> p23
 124  | T18 -> p24
 125  | T19 -> p25
 126  | T1A -> p26
 127  | T1B -> p27
 128  | T1C -> p28
 129  | T1D -> p29
 130  | T1E -> p30
 131  | T1F -> p31)
 132 )))))))))))))))))))))))))))))))))
 133 ;;
 134
 135 let bitrigesim_rect =
 136 (function p -> (function p1 -> (function p2 -> (function p3 -> (function p4 -> (function p5 -> (function p6 -> (function p7 -> (function p8 -> (function p9 -> (function p10 -> (function p11 -> (function p12 -> (function p13 -> (function p14 -> (function p15 -> (function p16 -> (function p17 -> (function p18 -> (function p19 -> (function p20 -> (function p21 -> (function p22 -> (function p23 -> (function p24 -> (function p25 -> (function p26 -> (function p27 -> (function p28 -> (function p29 -> (function p30 -> (function p31 -> (function b ->
 137 (match b with
 138    T00 -> p
 139  | T01 -> p1
 140  | T02 -> p2
 141  | T03 -> p3
 142  | T04 -> p4
 143  | T05 -> p5
 144  | T06 -> p6
 145  | T07 -> p7
 146  | T08 -> p8
 147  | T09 -> p9
 148  | T0A -> p10
 149  | T0B -> p11
 150  | T0C -> p12
 151  | T0D -> p13
 152  | T0E -> p14
 153  | T0F -> p15
 154  | T10 -> p16
 155  | T11 -> p17
 156  | T12 -> p18
 157  | T13 -> p19
 158  | T14 -> p20
 159  | T15 -> p21
 160  | T16 -> p22
 161  | T17 -> p23
 162  | T18 -> p24
 163  | T19 -> p25
 164  | T1A -> p26
 165  | T1B -> p27
 166  | T1C -> p28
 167  | T1D -> p29
 168  | T1E -> p30
 169  | T1F -> p31)
 170 )))))))))))))))))))))))))))))))))
 171 ;;
 172
 173 let byte8_of_bitrigesim =
 174 (function t ->
 175 (match t with
 176    T00 -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
 177  | T01 -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1))
 178  | T02 -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X2))
 179  | T03 -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X3))
 180  | T04 -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X4))
 181  | T05 -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X5))
 182  | T06 -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X6))
 183  | T07 -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X7))
 184  | T08 -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X8))
 185  | T09 -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X9))
 186  | T0A -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XA))
 187  | T0B -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XB))
 188  | T0C -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XC))
 189  | T0D -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XD))
 190  | T0E -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XE))
 191  | T0F -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XF))
 192  | T10 -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X0))
 193  | T11 -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X1))
 194  | T12 -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X2))
 195  | T13 -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X3))
 196  | T14 -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X4))
 197  | T15 -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X5))
 198  | T16 -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X6))
 199  | T17 -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X7))
 200  | T18 -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X8))
 201  | T19 -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X9))
 202  | T1A -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XA))
 203  | T1B -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XB))
 204  | T1C -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XC))
 205  | T1D -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XD))
 206  | T1E -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XE))
 207  | T1F -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XF)))
 208 )
 209 ;;
 210
 211 let nat_OF_bitrigesim =
 212 (function a -> (Matita_freescale_byte8.nat_of_byte8 (byte8_of_bitrigesim a)))
 213 ;;
 214
 215 let forall_bitrigesim =
 216 (function p -> (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (p T00) (p T01)) (p T02)) (p T03)) (p T04)) (p T05)) (p T06)) (p T07)) (p T08)) (p T09)) (p T0A)) (p T0B)) (p T0C)) (p T0D)) (p T0E)) (p T0F)) (p T10)) (p T11)) (p T12)) (p T13)) (p T14)) (p T15)) (p T16)) (p T17)) (p T18)) (p T19)) (p T1A)) (p T1B)) (p T1C)) (p T1D)) (p T1E)) (p T1F)))
 217 ;;
 218