X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fcontribs%2Fassembly%2Ffreescale%2Ffreescale_ocaml%2Fmatita_freescale_extra.ml;fp=matita%2Fcontribs%2Fassembly%2Ffreescale%2Ffreescale_ocaml%2Fmatita_freescale_extra.ml;h=e4600529c9450f8ef0adf74b664995965faa7353;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1

diff --git a/matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_extra.ml b/matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_extra.ml
new file mode 100644
index 000000000..e4600529c
--- /dev/null
+++ b/matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_extra.ml
@@ -0,0 +1,194 @@
+let not_bool =
+(function b -> 
+(match b with 
+   Matita_datatypes_bool.True -> Matita_datatypes_bool.False
+ | Matita_datatypes_bool.False -> Matita_datatypes_bool.True)
+)
+;;
+
+let and_bool =
+(function b1 -> (function b2 -> 
+(match b1 with 
+   Matita_datatypes_bool.True -> b2
+ | Matita_datatypes_bool.False -> Matita_datatypes_bool.False)
+))
+;;
+
+let or_bool =
+(function b1 -> (function b2 -> 
+(match b1 with 
+   Matita_datatypes_bool.True -> Matita_datatypes_bool.True
+ | Matita_datatypes_bool.False -> b2)
+))
+;;
+
+let xor_bool =
+(function b1 -> (function b2 -> 
+(match b1 with 
+   Matita_datatypes_bool.True -> (not_bool b2)
+ | Matita_datatypes_bool.False -> b2)
+))
+;;
+
+let eq_bool =
+(function b1 -> (function b2 -> 
+(match b1 with 
+   Matita_datatypes_bool.True -> b2
+ | Matita_datatypes_bool.False -> (not_bool b2))
+))
+;;
+
+type ('t1,'t2,'t3) prod3T =
+TripleT of 't1 * 't2 * 't3
+;;
+
+let prod3T_rec =
+(function f -> (function p -> 
+(match p with 
+   TripleT(t,t1,t2) -> (f t t1 t2))
+))
+;;
+
+let prod3T_rect =
+(function f -> (function p -> 
+(match p with 
+   TripleT(t,t1,t2) -> (f t t1 t2))
+))
+;;
+
+let fst3T =
+(function p -> 
+(match p with 
+   TripleT(x,_,_) -> x)
+)
+;;
+
+let snd3T =
+(function p -> 
+(match p with 
+   TripleT(_,x,_) -> x)
+)
+;;
+
+let thd3T =
+(function p -> 
+(match p with 
+   TripleT(_,_,x) -> x)
+)
+;;
+
+type ('t1,'t2,'t3,'t4) prod4T =
+QuadrupleT of 't1 * 't2 * 't3 * 't4
+;;
+
+let prod4T_rec =
+(function f -> (function p -> 
+(match p with 
+   QuadrupleT(t,t1,t2,t3) -> (f t t1 t2 t3))
+))
+;;
+
+let prod4T_rect =
+(function f -> (function p -> 
+(match p with 
+   QuadrupleT(t,t1,t2,t3) -> (f t t1 t2 t3))
+))
+;;
+
+let fst4T =
+(function p -> 
+(match p with 
+   QuadrupleT(x,_,_,_) -> x)
+)
+;;
+
+let snd4T =
+(function p -> 
+(match p with 
+   QuadrupleT(_,x,_,_) -> x)
+)
+;;
+
+let thd4T =
+(function p -> 
+(match p with 
+   QuadrupleT(_,_,x,_) -> x)
+)
+;;
+
+let fth4T =
+(function p -> 
+(match p with 
+   QuadrupleT(_,_,_,x) -> x)
+)
+;;
+
+type ('t1,'t2,'t3,'t4,'t5) prod5T =
+QuintupleT of 't1 * 't2 * 't3 * 't4 * 't5
+;;
+
+let prod5T_rec =
+(function f -> (function p -> 
+(match p with 
+   QuintupleT(t,t1,t2,t3,t4) -> (f t t1 t2 t3 t4))
+))
+;;
+
+let prod5T_rect =
+(function f -> (function p -> 
+(match p with 
+   QuintupleT(t,t1,t2,t3,t4) -> (f t t1 t2 t3 t4))
+))
+;;
+
+let fst5T =
+(function p -> 
+(match p with 
+   QuintupleT(x,_,_,_,_) -> x)
+)
+;;
+
+let snd5T =
+(function p -> 
+(match p with 
+   QuintupleT(_,x,_,_,_) -> x)
+)
+;;
+
+let thd5T =
+(function p -> 
+(match p with 
+   QuintupleT(_,_,x,_,_) -> x)
+)
+;;
+
+let frth5T =
+(function p -> 
+(match p with 
+   QuintupleT(_,_,_,x,_) -> x)
+)
+;;
+
+let ffth5T =
+(function p -> 
+(match p with 
+   QuintupleT(_,_,_,_,x) -> x)
+)
+;;
+
+let opt_map =
+(function t -> (function f -> 
+(match t with 
+   Matita_datatypes_constructors.None -> (Matita_datatypes_constructors.None)
+ | Matita_datatypes_constructors.Some(x) -> (f x))
+))
+;;
+
+let nat_of_bool =
+(function b -> 
+(match b with 
+   Matita_datatypes_bool.True -> (Matita_nat_nat.S(Matita_nat_nat.O))
+ | Matita_datatypes_bool.False -> Matita_nat_nat.O)
+)
+;;
+