(* This code extends 'std_prelude'. *)

val word_add = 
  (fn v1 => 
    (fn v2 => 
      let val x = (v1 + v2) 
      in (x mod 4294967296) 
      end )) ;

val word_mul = 
  (fn v1 => 
    (fn v2 => 
      let val x = (v1 * v2) 
      in (x mod 4294967296) 
      end )) ;

val word_add_1 = 
  (fn v1 => 
    (fn v2 => 
      let val x = (v1 + v2) 
      in (x mod 65536) 
      end )) ;

val word_mul_1 = 
  (fn v1 => 
    (fn v2 => 
      let val x = (v1 * v2) 
      in (x mod 65536) 
      end )) ;

val word_add_2 = 
  (fn v1 => 
    (fn v2 => 
      let val x = (v1 + v2) 
      in (x mod 256) 
      end )) ;

val word_mul_2 = 
  (fn v1 => 
    (fn v2 => 
      let val x = (v1 * v2) 
      in (x mod 256) 
      end )) ;

fun BITWISE v1 = 
  (fn v2 => 
    (fn v3 => 
      (fn v4 => 
        (if (v1 <= 0) 
        then 0 
        else (((((BITWISE (v1 - 1)) v2) v3) v4) + ((SBIT ((v2 ((BIT (v1 - 1)) v3)) ((BIT (v1 - 1)) v4))) (v1 - 1))))))) ;

val word_xor = 
  (fn v4 => 
    (fn v3 => 
      let val x = ((((BITWISE 32) 
      (fn v2 => 
        (fn v1 => ((v2 = v1) = false)))) v4) v3) 
      in (x mod 4294967296) 
      end )) ;

val word_xor_1 = 
  (fn v4 => 
    (fn v3 => 
      let val x = ((((BITWISE 8) 
      (fn v2 => 
        (fn v1 => ((v2 = v1) = false)))) v4) v3) 
      in (x mod 256) 
      end )) ;

val word_xor_2 = 
  (fn v4 => 
    (fn v3 => 
      let val x = ((((BITWISE 16) 
      (fn v2 => 
        (fn v1 => ((v2 = v1) = false)))) v4) v3) 
      in (x mod 65536) 
      end )) ;

val word_or = 
  (fn v4 => 
    (fn v3 => 
      let val x = ((((BITWISE 32) 
      (fn v2 => 
        (fn v1 => (v2 orelse v1)))) v4) v3) 
      in (x mod 4294967296) 
      end )) ;

val word_or_1 = 
  (fn v4 => 
    (fn v3 => 
      let val x = ((((BITWISE 16) 
      (fn v2 => 
        (fn v1 => (v2 orelse v1)))) v4) v3) 
      in (x mod 65536) 
      end )) ;

val word_and = 
  (fn v4 => 
    (fn v3 => 
      let val x = ((((BITWISE 32) 
      (fn v2 => 
        (fn v1 => (v2 andalso v1)))) v4) v3) 
      in (x mod 4294967296) 
      end )) ;

val word_lsl = 
  (fn v1 => 
    (fn v2 => ((word_mul 
      let val x = ((EXP 2) v2) 
      in (x mod 4294967296) 
      end ) v1))) ;

val word_lsl_1 = 
  (fn v1 => 
    (fn v2 => ((word_mul_1 
      let val x = ((EXP 2) v2) 
      in (x mod 65536) 
      end ) v1))) ;

val word_lsl_2 = 
  (fn v1 => 
    (fn v2 => ((word_mul_2 
      let val x = ((EXP 2) v2) 
      in (x mod 256) 
      end ) v1))) ;

val word_lsr = 
  (fn v2 => 
    (fn v1 => 
      let val x = (v2 div ((EXP 2) v1)) 
      in (x mod 4294967296) 
      end )) ;

val word_lsr_1 = 
  (fn v2 => 
    (fn v1 => 
      let val x = (v2 div ((EXP 2) v1)) 
      in (x mod 65536) 
      end )) ;

val word_lsr_2 = 
  (fn v2 => 
    (fn v1 => 
      let val x = (v2 div ((EXP 2) v1)) 
      in (x mod 256) 
      end )) ;

val word_msb = 
  (fn v1 => ((BIT 31) v1)) ;

val word_msb_1 = 
  (fn v1 => ((BIT 15) v1)) ;

val word_msb_2 = 
  (fn v1 => ((BIT 7) v1)) ;

val word_lsb = 
  (fn v1 => (((v1 mod 2) <= 0) = false)) ;

val word_lsb_1 = 
  (fn v1 => (((v1 mod 2) <= 0) = false)) ;

val word_lsb_2 = 
  (fn v1 => (((v1 mod 2) <= 0) = false)) ;

val word_asr = 
  (fn v2 => 
    (fn v1 => 
      (if (word_msb v2) 
      then ((word_or 
        let val x = 
        let val k = (4294967296 - ((EXP 2) 
        let val k = (32 - ((MIN v1) 32)) 
        in 
          (if (k < 0) 
          then 0 
          else k) 
        end )) 
        in 
          (if (k < 0) 
          then 0 
          else k) 
        end 
        in (x mod 4294967296) 
        end ) ((word_lsr v2) v1)) 
      else ((word_lsr v2) v1)))) ;

val word_asr_1 = 
  (fn v2 => 
    (fn v1 => 
      (if (word_msb_1 v2) 
      then ((word_or_1 
        let val x = 
        let val k = (65536 - ((EXP 2) 
        let val k = (16 - ((MIN v1) 16)) 
        in 
          (if (k < 0) 
          then 0 
          else k) 
        end )) 
        in 
          (if (k < 0) 
          then 0 
          else k) 
        end 
        in (x mod 65536) 
        end ) ((word_lsr_1 v2) v1)) 
      else ((word_lsr_1 v2) v1)))) ;

val word_sub = 
  (fn v1 => 
    (fn v2 => ((word_add v1) 
      let val x = 
      let val k = (4294967296 - v2) 
      in 
        (if (k < 0) 
        then 0 
        else k) 
      end 
      in (x mod 4294967296) 
      end ))) ;

val word_sub_1 = 
  (fn v1 => 
    (fn v2 => ((word_add_1 v1) 
      let val x = 
      let val k = (65536 - v2) 
      in 
        (if (k < 0) 
        then 0 
        else k) 
      end 
      in (x mod 65536) 
      end ))) ;

val word_sub_2 = 
  (fn v1 => 
    (fn v2 => ((word_add_2 v1) 
      let val x = 
      let val k = (256 - v2) 
      in 
        (if (k < 0) 
        then 0 
        else k) 
      end 
      in (x mod 256) 
      end ))) ;

val word_bits = 
  (fn v1 => 
    (fn v2 => 
      (fn v3 => 
        let val x = (((BITS ((MIN v1) 31)) v2) v3) 
        in (x mod 4294967296) 
        end ))) ;

val word_ror = 
  (fn v3 => 
    (fn v2 => 
      let val v1 = (v2 mod 32) 
      in ((word_or (((word_bits 31) v1) v3)) ((word_lsl (((word_bits 
        let val k = (v1 - 1) 
        in 
          (if (k < 0) 
          then 0 
          else k) 
        end ) 0) v3)) 
        let val k = (32 - v1) 
        in 
          (if (k < 0) 
          then 0 
          else k) 
        end )) 
      end )) ;

val word_rol = 
  (fn v2 => 
    (fn v1 => ((word_ror v2) 
      let val k = (32 - (v1 mod 32)) 
      in 
        (if (k < 0) 
        then 0 
        else k) 
      end ))) ;