X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fcontribs%2Fassembly%2Ffreescale%2Ffreescale_ocaml%2Fmatita_freescale_word16.ml;fp=matita%2Fcontribs%2Fassembly%2Ffreescale%2Ffreescale_ocaml%2Fmatita_freescale_word16.ml;h=069774afcb7d922e0772647f1d73653f8fe88739;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1 diff --git a/matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_word16.ml b/matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_word16.ml new file mode 100644 index 000000000..069774afc --- /dev/null +++ b/matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_word16.ml @@ -0,0 +1,271 @@ +type word16 = +Mk_word16 of Matita_freescale_byte8.byte8 * Matita_freescale_byte8.byte8 +;; + +let word16_rec = +(function f -> (function w -> +(match w with + Mk_word16(b,b1) -> (f b b1)) +)) +;; + +let word16_rect = +(function f -> (function w -> +(match w with + Mk_word16(b,b1) -> (f b b1)) +)) +;; + +let w16h = +(function w -> +(match w with + Mk_word16(w16h,w16l) -> w16h) +) +;; + +let w16l = +(function w -> +(match w with + Mk_word16(w16h,w16l) -> w16l) +) +;; + +let eq_w16 = +(function w1 -> (function w2 -> (Matita_freescale_extra.and_bool (Matita_freescale_byte8.eq_b8 (w16h w1) (w16h w2)) (Matita_freescale_byte8.eq_b8 (w16l w1) (w16l w2))))) +;; + +let lt_w16 = +(function w1 -> (function w2 -> +(match (Matita_freescale_byte8.lt_b8 (w16h w1) (w16h w2)) with + Matita_datatypes_bool.True -> Matita_datatypes_bool.True + | Matita_datatypes_bool.False -> +(match (Matita_freescale_byte8.gt_b8 (w16h w1) (w16h w2)) with + Matita_datatypes_bool.True -> Matita_datatypes_bool.False + | Matita_datatypes_bool.False -> (Matita_freescale_byte8.lt_b8 (w16l w1) (w16l w2))) +) +)) +;; + +let le_w16 = +(function w1 -> (function w2 -> (Matita_freescale_extra.or_bool (eq_w16 w1 w2) (lt_w16 w1 w2)))) +;; + +let gt_w16 = +(function w1 -> (function w2 -> (Matita_freescale_extra.not_bool (le_w16 w1 w2)))) +;; + +let ge_w16 = +(function w1 -> (function w2 -> (Matita_freescale_extra.not_bool (lt_w16 w1 w2)))) +;; + +let and_w16 = +(function w1 -> (function w2 -> (Mk_word16((Matita_freescale_byte8.and_b8 (w16h w1) (w16h w2)),(Matita_freescale_byte8.and_b8 (w16l w1) (w16l w2)))))) +;; + +let or_w16 = +(function w1 -> (function w2 -> (Mk_word16((Matita_freescale_byte8.or_b8 (w16h w1) (w16h w2)),(Matita_freescale_byte8.or_b8 (w16l w1) (w16l w2)))))) +;; + +let xor_w16 = +(function w1 -> (function w2 -> (Mk_word16((Matita_freescale_byte8.xor_b8 (w16h w1) (w16h w2)),(Matita_freescale_byte8.xor_b8 (w16l w1) (w16l w2)))))) +;; + +let rcr_w16 = +(function w -> (function c -> +(match (Matita_freescale_byte8.rcr_b8 (w16h w) c) with + Matita_datatypes_constructors.Pair(wh',c') -> +(match (Matita_freescale_byte8.rcr_b8 (w16l w) c') with + Matita_datatypes_constructors.Pair(wl',c'') -> (Matita_datatypes_constructors.Pair((Mk_word16(wh',wl')),c''))) +) +)) +;; + +let shr_w16 = +(function w -> +(match (Matita_freescale_byte8.rcr_b8 (w16h w) Matita_datatypes_bool.False) with + Matita_datatypes_constructors.Pair(wh',c') -> +(match (Matita_freescale_byte8.rcr_b8 (w16l w) c') with + Matita_datatypes_constructors.Pair(wl',c'') -> (Matita_datatypes_constructors.Pair((Mk_word16(wh',wl')),c''))) +) +) +;; + +let ror_w16 = +(function w -> +(match (Matita_freescale_byte8.rcr_b8 (w16h w) Matita_datatypes_bool.False) with + Matita_datatypes_constructors.Pair(wh',c') -> +(match (Matita_freescale_byte8.rcr_b8 (w16l w) c') with + Matita_datatypes_constructors.Pair(wl',c'') -> +(match c'' with + Matita_datatypes_bool.True -> (Mk_word16((Matita_freescale_byte8.or_b8 (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X0)) wh'),wl')) + | Matita_datatypes_bool.False -> (Mk_word16(wh',wl'))) +) +) +) +;; + +let ror_w16_n = +let rec ror_w16_n = +(function w -> (function n -> +(match n with + Matita_nat_nat.O -> w + | Matita_nat_nat.S(n') -> (ror_w16_n (ror_w16 w) n')) +)) in ror_w16_n +;; + +let rcl_w16 = +(function w -> (function c -> +(match (Matita_freescale_byte8.rcl_b8 (w16l w) c) with + Matita_datatypes_constructors.Pair(wl',c') -> +(match (Matita_freescale_byte8.rcl_b8 (w16h w) c') with + Matita_datatypes_constructors.Pair(wh',c'') -> (Matita_datatypes_constructors.Pair((Mk_word16(wh',wl')),c''))) +) +)) +;; + +let shl_w16 = +(function w -> +(match (Matita_freescale_byte8.rcl_b8 (w16l w) Matita_datatypes_bool.False) with + Matita_datatypes_constructors.Pair(wl',c') -> +(match (Matita_freescale_byte8.rcl_b8 (w16h w) c') with + Matita_datatypes_constructors.Pair(wh',c'') -> (Matita_datatypes_constructors.Pair((Mk_word16(wh',wl')),c''))) +) +) +;; + +let rol_w16 = +(function w -> +(match (Matita_freescale_byte8.rcl_b8 (w16l w) Matita_datatypes_bool.False) with + Matita_datatypes_constructors.Pair(wl',c') -> +(match (Matita_freescale_byte8.rcl_b8 (w16h w) c') with + Matita_datatypes_constructors.Pair(wh',c'') -> +(match c'' with + Matita_datatypes_bool.True -> (Mk_word16(wh',(Matita_freescale_byte8.or_b8 (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1)) wl'))) + | Matita_datatypes_bool.False -> (Mk_word16(wh',wl'))) +) +) +) +;; + +let rol_w16_n = +let rec rol_w16_n = +(function w -> (function n -> +(match n with + Matita_nat_nat.O -> w + | Matita_nat_nat.S(n') -> (rol_w16_n (rol_w16 w) n')) +)) in rol_w16_n +;; + +let not_w16 = +(function w -> (Mk_word16((Matita_freescale_byte8.not_b8 (w16h w)),(Matita_freescale_byte8.not_b8 (w16l w))))) +;; + +let plus_w16 = +(function w1 -> (function w2 -> (function c -> +(match (Matita_freescale_byte8.plus_b8 (w16l w1) (w16l w2) c) with + Matita_datatypes_constructors.Pair(l,c') -> +(match (Matita_freescale_byte8.plus_b8 (w16h w1) (w16h w2) c') with + Matita_datatypes_constructors.Pair(h,c'') -> (Matita_datatypes_constructors.Pair((Mk_word16(h,l)),c''))) +) +))) +;; + +let plus_w16nc = +(function w1 -> (function w2 -> (Matita_datatypes_constructors.fst (plus_w16 w1 w2 Matita_datatypes_bool.False)))) +;; + +let plus_w16c = +(function w1 -> (function w2 -> (Matita_datatypes_constructors.snd (plus_w16 w1 w2 Matita_datatypes_bool.False)))) +;; + +let mSB_w16 = +(function w -> (Matita_freescale_exadecim.eq_ex Matita_freescale_exadecim.X8 (Matita_freescale_exadecim.and_ex Matita_freescale_exadecim.X8 (Matita_freescale_byte8.b8h (w16h w))))) +;; + +let nat_of_word16 = +(function w -> (Matita_nat_plus.plus (Matita_nat_times.times (Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S(Matita_nat_nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (Matita_freescale_byte8.nat_of_byte8 (w16h w))) (Matita_freescale_byte8.nat_of_byte8 (w16l w)))) +;; + +let word16_of_nat = +(function n -> (Mk_word16((Matita_freescale_byte8.byte8_of_nat (Matita_nat_div_and_mod.div n (Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S(Matita_nat_nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),(Matita_freescale_byte8.byte8_of_nat n)))) +;; + +let pred_w16 = +(function w -> +(match (Matita_freescale_byte8.eq_b8 (w16l w) (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))) with + Matita_datatypes_bool.True -> (Mk_word16((Matita_freescale_byte8.pred_b8 (w16h w)),(Matita_freescale_byte8.pred_b8 (w16l w)))) + | Matita_datatypes_bool.False -> (Mk_word16((w16h w),(Matita_freescale_byte8.pred_b8 (w16l w))))) +) +;; + +let succ_w16 = +(function w -> +(match (Matita_freescale_byte8.eq_b8 (w16l w) (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF))) with + Matita_datatypes_bool.True -> (Mk_word16((Matita_freescale_byte8.succ_b8 (w16h w)),(Matita_freescale_byte8.succ_b8 (w16l w)))) + | Matita_datatypes_bool.False -> (Mk_word16((w16h w),(Matita_freescale_byte8.succ_b8 (w16l w))))) +) +;; + +let compl_w16 = +(function w -> +(match (mSB_w16 w) with + Matita_datatypes_bool.True -> (succ_w16 (not_w16 w)) + | Matita_datatypes_bool.False -> (not_w16 (pred_w16 w))) +) +;; + +let mul_b8 = +(function b1 -> (function b2 -> +(match b1 with + Matita_freescale_byte8.Mk_byte8(b1h,b1l) -> +(match b2 with + Matita_freescale_byte8.Mk_byte8(b2h,b2l) -> +(match (Matita_freescale_byte8.mul_ex b1l b2l) with + Matita_freescale_byte8.Mk_byte8(t1_h,t1_l) -> +(match (Matita_freescale_byte8.mul_ex b1h b2l) with + Matita_freescale_byte8.Mk_byte8(t2_h,t2_l) -> +(match (Matita_freescale_byte8.mul_ex b2h b1l) with + Matita_freescale_byte8.Mk_byte8(t3_h,t3_l) -> +(match (Matita_freescale_byte8.mul_ex b1h b2h) with + Matita_freescale_byte8.Mk_byte8(t4_h,t4_l) -> (plus_w16nc (plus_w16nc (plus_w16nc (Mk_word16((Matita_freescale_byte8.Mk_byte8(t4_h,t4_l)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))) (Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,t3_h)),(Matita_freescale_byte8.Mk_byte8(t3_l,Matita_freescale_exadecim.X0))))) (Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,t2_h)),(Matita_freescale_byte8.Mk_byte8(t2_l,Matita_freescale_exadecim.X0))))) (Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(t1_h,t1_l)))))) +) +) +) +) +) +)) +;; + +let div_b8 = +(function w -> (function b -> +(match (Matita_freescale_byte8.eq_b8 b (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))) with + Matita_datatypes_bool.True -> (Matita_freescale_extra.TripleT((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(w16l w),Matita_datatypes_bool.True)) + | Matita_datatypes_bool.False -> +(match (eq_w16 w (Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))))) with + Matita_datatypes_bool.True -> (Matita_freescale_extra.TripleT((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),Matita_datatypes_bool.False)) + | Matita_datatypes_bool.False -> (let rec aux = +(function divd -> (function divs -> (function molt -> (function q -> (function c -> (let w' = (plus_w16nc divd (compl_w16 divs)) in +(match c with + Matita_nat_nat.O -> +(match (le_w16 divs divd) with + Matita_datatypes_bool.True -> (Matita_freescale_extra.TripleT((Matita_freescale_byte8.or_b8 molt q),(w16l w'),(Matita_freescale_extra.not_bool (Matita_freescale_byte8.eq_b8 (w16h w') (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))))) + | Matita_datatypes_bool.False -> (Matita_freescale_extra.TripleT(q,(w16l divd),(Matita_freescale_extra.not_bool (Matita_freescale_byte8.eq_b8 (w16h divd) (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))))))) + + | Matita_nat_nat.S(c') -> +(match (le_w16 divs divd) with + Matita_datatypes_bool.True -> (aux w' (ror_w16 divs) (Matita_freescale_byte8.ror_b8 molt) (Matita_freescale_byte8.or_b8 molt q) c') + | Matita_datatypes_bool.False -> (aux divd (ror_w16 divs) (Matita_freescale_byte8.ror_b8 molt) q c')) +) +)))))) in aux w (rol_w16_n (Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),b)) (Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S(Matita_nat_nat.O))))))))))))))) (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X0)) (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)) (Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S(Matita_nat_nat.O)))))))))))))))) +) +)) +;; + +let in_range = +(function x -> (function inf -> (function sup -> (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (le_w16 inf sup) (ge_w16 x inf)) (le_w16 x sup))))) +;; + +let forall_word16 = +(function p -> (Matita_freescale_byte8.forall_byte8 (function bh -> (Matita_freescale_byte8.forall_byte8 (function bl -> (p (Mk_word16(bh,bl)))))))) +;; +