Lines Matching defs:data
1211 fun Poly32Mod2_loop (i,(data,poly)) =
1213 then data
1215 val data =
1216 if Bitstring.bit(data,i)
1217 then (Bitstring.bits(Nat.-(L3.length data,1),i) data)
1220 (Bitstring.bits(Nat.-(i,1),0) data,
1222 else data
1224 Poly32Mod2_loop(Nat.-(i,1),(data,poly))
1227 fun Poly32Mod2 (data,poly) =
1231 (Nat.-(L3.length data,1),(data,BitsN.toBitstring poly))),32);
1747 val data = if rt_unknown then BitsN.fromNat(0,N) else X N t
1751 write'Mem N (data,x)
1755 val data =
1760 then write'X 32 (ExtendWord (32,32) (data,signed),t)
1761 else write'X 64 (ExtendWord (64,64) (data,signed),t)
1909 val data = if rt_unknown then BitsN.fromNat(0,N) else X N t
1916 write'Mem N (data,x)
1929 write'Mem N (data,x)
1935 val data = Mem N (address,(dbytes,acctype))
1938 then write'X N (data,t)
1939 else write'X 32 (BitsN.fromNat(BitsN.toNat data,32),t)
1962 val data =
1981 write'Mem N (data,x)
2000 val data = Mem N (address,(dbytes,acctype))
2003 then ( write'X 32 (BitsN.bits(63,32) data,t)
2004 ; write'X 32 (BitsN.bits(31,0) data,t2)
2006 else ( write'X 32 (BitsN.bits(31,0) data,t)
2007 ; write'X 32 (BitsN.bits(63,32) data,t2)
2031 val data =
2036 write'X 64 (ExtendWord (64,64) (data,signed),t)