Replace wordSem$word_sh with asmSem$word_shift

Neither of these constants exist in these locations. There is a wordLang$word_sh:

val word_sh_def = Define `
  word_sh sh (w:'a word) n =
    if n <> 0 /\ n ≥ dimindex (:'a) then NONE else
      case sh of
      | Lsl => SOME (w << n)
      | Lsr => SOME (w >>> n)
      | Asr => SOME (w >> n)
      | Ror => SOME (word_ror w n)`;

and a stackLang$word_shift:

val word_shift_def = Define `
  word_shift (:'a) =
    (* this could be defined as LOG 2 (dimindex(:'a)) - 3, but I want
       to be sure that LOG doesn't unnecessarily end up in the
       generated CakeML code *)
    if dimindex (:'a) = 32 then 2 else 3:num`;

In addition, there is a wordLang$shift:

val shift_def = Define `
  shift (:'a) = if dimindex (:'a) = 32 then 2 else 3n`;

I will soon submit a PR moving a shift constant to backend_common and dropping the definitions of the others.

CakeML / cakeml

Replace wordSem$word_sh with asmSem$word_shift #171