working/0.2/HSLScript.sml

246     (transfer (s1,s0) (dst::dstL, src::srcL) =
247        transfer (twrite s1 dst (tread s0 src), s0) (dstL, srcL))`;
250   (!dst src.tdecode hs (TLDR dst src) =
251       twrite hs (inR dst) (tread hs (inE src))) /\
252   (!dst src.tdecode hs (TSTR dst src) =
253       twrite hs (inE dst) (tread hs (inR src))) /\
254   (tdecode hs (TMOV dst src) =
255       twrite hs (inR dst) (tread hs (roc_2_exp src))) /\
256   (tdecode hs (TADD dst src1 src2) =
257       twrite hs (inR dst) (tread hs (roc_2_exp src1) + tread hs (roc_2_exp src2))) /\
258   (tdecode hs (TSUB dst src1 src2) =
259       twrite hs (inR dst) (tread hs (roc_2_exp src1) - tread hs (roc_2_exp src2))) /\
260   (tdecode hs (TRSB dst src1 src2) =
261       twrite hs (inR dst) (tread hs (roc_2_exp src2) - tread hs (roc_2_exp src1))) /\
262   (tdecode hs (TMUL dst src1 src2_reg) =
263       twrite hs (inR dst) (tread hs (roc_2_exp src1) * tread hs (roc_2_exp src2_reg))) /\
264   (tdecode hs (TAND dst src1 src2) =
265       twrite hs (inR dst) (tread hs (roc_2_exp src1) && tread hs (roc_2_exp src2))) /\
266   (tdecode hs (TORR dst src1 src2) =
267       twrite hs (inR dst) (tread hs (roc_2_exp src1) !! tread hs (roc_2_exp src2))) /\
268   (tdecode hs (TEOR dst src1 src2) =
269       twrite hs (inR dst) (tread hs (roc_2_exp src1) ?? tread hs (roc_2_exp src2))) /\
270   (tdecode hs (TLSL dst src2_reg src2_num) =
271       twrite hs (inR dst) (tread hs (roc_2_exp src2_reg) << w2n src2_num)) /\
272   (tdecode hs (TLSR dst src2_reg src2_num) =
273       twrite hs (inR dst) (tread hs (roc_2_exp src2_reg) >>> w2n src2_num)) /\
274   (tdecode hs (TASR dst src2_reg src2_num) =
275       twrite hs (inR dst) (tread hs (roc_2_exp src2_reg) >> w2n src2_num)) /\
276   (tdecode hs (TROR dst src2_reg src2_num) =
277       twrite hs (inR dst) (tread hs (roc_2_exp src2_reg) #>> w2n src2_num))