ea37d7c468ca9accf7a8222e8bb0f78cfb6684286879547f50d10e376e53f5aa.tri (1292B)
1 -- Pure binary64 implementation; trusted internal helpers. 2 !import native_math as N 3 !export both 4 !export choose 5 !export either 6 !export head 7 !export lazy 8 !export node 9 !export not 10 !export roundL 11 !export shiftL 12 !export tail 13 !export triage 14 !export width 15 !export xor 16 17 triage leaf stem fork = t (t leaf stem) fork 18 choose yes no value = triage no (_ : yes) (_ _ : yes) value 19 lazy yes no value = choose yes no value t 20 head value = triage t (_ : t) (a _ : a) value 21 tail value = triage t (_ : t) (_ b : b) value 22 both a b = choose b t a 23 either a b = choose (t t) b a 24 not value = choose t (t t) value 25 xor a b = choose (not b) b a 26 node bit rest = choose (t bit rest) (choose t (t bit rest) (N.zero rest)) bit 27 width xs = triage 0 (_ : 0) (_ rest : N.successor (width rest)) xs 28 shiftL k x = shiftWalk k x t 29 shiftWalk k x sticky = lazy (_ : t x sticky) 30 (_ : triage (t t sticky) (_ : t t sticky) 31 (bit rest : shiftWalk (N.predecessor k) rest (either sticky bit)) x) (N.zero k) 32 roundL k x = lazy (_ : t x t) (_ : roundWalk k x t) (N.zero k) 33 roundWalk k x sticky = triage (t t sticky) (_ : t t sticky) 34 (bit rest : lazy 35 (_ : t (choose (N.successor rest) rest (both bit (either sticky (N.odd rest)))) (either sticky bit)) 36 (_ : roundWalk (N.predecessor k) rest (either sticky bit)) (N.equal k 1)) x