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

   1 let not_bool =
   2 (function b ->
   3 (match b with
   4    Matita_datatypes_bool.True -> Matita_datatypes_bool.False
   5  | Matita_datatypes_bool.False -> Matita_datatypes_bool.True)
   6 )
   7 ;;
   8
   9 let and_bool =
  10 (function b1 -> (function b2 ->
  11 (match b1 with
  12    Matita_datatypes_bool.True -> b2
  13  | Matita_datatypes_bool.False -> Matita_datatypes_bool.False)
  14 ))
  15 ;;
  16
  17 let or_bool =
  18 (function b1 -> (function b2 ->
  19 (match b1 with
  20    Matita_datatypes_bool.True -> Matita_datatypes_bool.True
  21  | Matita_datatypes_bool.False -> b2)
  22 ))
  23 ;;
  24
  25 let xor_bool =
  26 (function b1 -> (function b2 ->
  27 (match b1 with
  28    Matita_datatypes_bool.True -> (not_bool b2)
  29  | Matita_datatypes_bool.False -> b2)
  30 ))
  31 ;;
  32
  33 let eq_bool =
  34 (function b1 -> (function b2 ->
  35 (match b1 with
  36    Matita_datatypes_bool.True -> b2
  37  | Matita_datatypes_bool.False -> (not_bool b2))
  38 ))
  39 ;;
  40
  41 type ('t1,'t2,'t3) prod3T =
  42 TripleT of 't1 * 't2 * 't3
  43 ;;
  44
  45 let prod3T_rec =
  46 (function f -> (function p ->
  47 (match p with
  48    TripleT(t,t1,t2) -> (f t t1 t2))
  49 ))
  50 ;;
  51
  52 let prod3T_rect =
  53 (function f -> (function p ->
  54 (match p with
  55    TripleT(t,t1,t2) -> (f t t1 t2))
  56 ))
  57 ;;
  58
  59 let fst3T =
  60 (function p ->
  61 (match p with
  62    TripleT(x,_,_) -> x)
  63 )
  64 ;;
  65
  66 let snd3T =
  67 (function p ->
  68 (match p with
  69    TripleT(_,x,_) -> x)
  70 )
  71 ;;
  72
  73 let thd3T =
  74 (function p ->
  75 (match p with
  76    TripleT(_,_,x) -> x)
  77 )
  78 ;;
  79
  80 type ('t1,'t2,'t3,'t4) prod4T =
  81 QuadrupleT of 't1 * 't2 * 't3 * 't4
  82 ;;
  83
  84 let prod4T_rec =
  85 (function f -> (function p ->
  86 (match p with
  87    QuadrupleT(t,t1,t2,t3) -> (f t t1 t2 t3))
  88 ))
  89 ;;
  90
  91 let prod4T_rect =
  92 (function f -> (function p ->
  93 (match p with
  94    QuadrupleT(t,t1,t2,t3) -> (f t t1 t2 t3))
  95 ))
  96 ;;
  97
  98 let fst4T =
  99 (function p ->
 100 (match p with
 101    QuadrupleT(x,_,_,_) -> x)
 102 )
 103 ;;
 104
 105 let snd4T =
 106 (function p ->
 107 (match p with
 108    QuadrupleT(_,x,_,_) -> x)
 109 )
 110 ;;
 111
 112 let thd4T =
 113 (function p ->
 114 (match p with
 115    QuadrupleT(_,_,x,_) -> x)
 116 )
 117 ;;
 118
 119 let fth4T =
 120 (function p ->
 121 (match p with
 122    QuadrupleT(_,_,_,x) -> x)
 123 )
 124 ;;
 125
 126 type ('t1,'t2,'t3,'t4,'t5) prod5T =
 127 QuintupleT of 't1 * 't2 * 't3 * 't4 * 't5
 128 ;;
 129
 130 let prod5T_rec =
 131 (function f -> (function p ->
 132 (match p with
 133    QuintupleT(t,t1,t2,t3,t4) -> (f t t1 t2 t3 t4))
 134 ))
 135 ;;
 136
 137 let prod5T_rect =
 138 (function f -> (function p ->
 139 (match p with
 140    QuintupleT(t,t1,t2,t3,t4) -> (f t t1 t2 t3 t4))
 141 ))
 142 ;;
 143
 144 let fst5T =
 145 (function p ->
 146 (match p with
 147    QuintupleT(x,_,_,_,_) -> x)
 148 )
 149 ;;
 150
 151 let snd5T =
 152 (function p ->
 153 (match p with
 154    QuintupleT(_,x,_,_,_) -> x)
 155 )
 156 ;;
 157
 158 let thd5T =
 159 (function p ->
 160 (match p with
 161    QuintupleT(_,_,x,_,_) -> x)
 162 )
 163 ;;
 164
 165 let frth5T =
 166 (function p ->
 167 (match p with
 168    QuintupleT(_,_,_,x,_) -> x)
 169 )
 170 ;;
 171
 172 let ffth5T =
 173 (function p ->
 174 (match p with
 175    QuintupleT(_,_,_,_,x) -> x)
 176 )
 177 ;;
 178
 179 let opt_map =
 180 (function t -> (function f ->
 181 (match t with
 182    Matita_datatypes_constructors.None -> (Matita_datatypes_constructors.None)
 183  | Matita_datatypes_constructors.Some(x) -> (f x))
 184 ))
 185 ;;
 186
 187 let nat_of_bool =
 188 (function b ->
 189 (match b with
 190    Matita_datatypes_bool.True -> (Matita_nat_nat.S(Matita_nat_nat.O))
 191  | Matita_datatypes_bool.False -> Matita_nat_nat.O)
 192 )
 193 ;;
 194