1	import Base
2	import ../../../../spec/lib/numeric.bend as NM
3	
4	# All bits are represented explicitly: no Nat holds a full-width integer.
5	def zero() -> Word(64n):
6	  Word.zero(64n)
7	
8	def inc(w: Word(64n)) -> Word(64n):
9	  Word.inc(64n, w)
10	
11	def add(a: Word(64n), b: Word(64n)) -> Word(64n):
12	  Word.add(64n, a, b)
13	
14	def neg(w: Word(64n)) -> Word(64n):
15	  Word.inc(64n, Word.not(64n, w))
16	
17	def last(n: Nat, w: Word(n)) -> Bool:
18	  match n:
19	    case 0n:
20	      False{}
21	    case 1n+0n:
22	      match w:
23	        case WCon{b, tail}:
24	          b
25	    case 1n+1n+p:
26	      match w:
27	        case WCon{b, tail}:
28	          last(1n+p, tail)
29	
30	def is_zero(n: Nat, w: Word(n)) -> Bool:
31	  match n:
32	    case 0n:
33	      True{}
34	    case 1n+p:
35	      match w:
36	        case WCon{b, tail}:
37	          Bool.not(b) && is_zero(p, tail)
38	
39	def signed_order(a: Word(64n), b: Word(64n), sa: Bool, sb: Bool) -> Bool:
40	  match sa sb:
41	    case True{} False{}:
42	      True{}
43	    case False{} True{}:
44	      False{}
45	    case x y:
46	      Cmp.is_le(Word.cmp(64n, a, b))
47	
48	def le(+a: Word(64n), +b: Word(64n)) -> Bool:
49	  signed_order(a, b, last(64n, a), last(64n, b))
50	
51	def bit_u32(b: Bool) -> U32:
52	  match b:
53	    case False{}:
54	      0
55	    case True{}:
56	      1
57	
58	type Division<-n: Nat> is Data:
59	  Div{quotient: Word(n), remainder: U32}
60	
61	def digit_result(p: Nat, q: Word(p), r: U32, subtract: Bool) -> Division<1n+p>:
62	  match subtract:
63	    case False{}:
64	      Div{WCon{False{}, q}, r}
65	    case True{}:
66	      Div{WCon{True{}, q}, U32.sub(r, 1000000)}
67	
68	def digit_compare(p: Nat, q: Word(p), +r: U32) -> Division<1n+p>:
69	  digit_result(p, q, r, U32.is_ge(r, 1000000))
70	
71	def digit(p: Nat, b: Bool, prior: Division<p>) -> Division<1n+p>:
72	  Div{q, r} = prior
73	  digit_compare(p, q, U32.add(U32.mul(r, 2), bit_u32(b)))
74	
75	# Binary long division, processing the most significant bit first. The partial
76	# remainder stays below 1,000,000; the next candidate fits in U32 (<2,000,000).
77	def div_million(+n: Nat, w: Word(n)) -> Division<n>:
78	  match n:
79	    case 0n:
80	      Div{WNil{}, 0}
81	    case 1n+p:
82	      match w:
83	        case WCon{b, tail}:
84	          digit(p, b, div_million(p, tail))
85	
86	def quotient(r: Division<64n>) -> Word(64n):
87	  Div{q, rem} = r
88	  q
89	
90	def unsigned_milliseconds(w: Word(64n)) -> Word(64n):
91	  quotient(div_million(64n, w))
92	
93	def signed_milliseconds(w: Word(64n), negative: Bool) -> Word(64n):
94	  match negative:
95	    case False{}:
96	      unsigned_milliseconds(w)
97	    case True{}:
98	      neg(unsigned_milliseconds(neg(w)))
99	
100	def milliseconds(+w: Word(64n)) -> Word(64n):
101	  signed_milliseconds(w, last(64n, w))
102	
103	# Exact limb boundary used by the host bridge; limbs themselves are primitive U32.
104	def join(n: Nat, +m: Nat, a: Word(n), b: Word(m)) -> Word(Nat.add(n, m)):
105	  NM.join(n, m, a, b)
106	
107	type Parts<-n: Nat, -m: Nat> is Data:
108	  Split{low: Word(n), high: Word(m)}
109	
110	def split_cons(-n: Nat, -m: Nat, h: Bool, parts: Parts<n, m>) -> Parts<1n+n, m>:
111	  Split{low, high} = parts
112	  Split{WCon{h, low}, high}
113	
114	def split(n: Nat, +m: Nat, w: Word(Nat.add(n, m))) -> Parts<n, m>:
115	  match n:
116	    case 0n:
117	      Split{WNil{}, w}
118	    case 1n+p:
119	      match w:
120	        case WCon{h, tail}:
121	          split_cons(p, m, h, split(p, m, tail))
122	
123	def pack(low: U32, high: U32) -> Word(64n):
124	  NM.pack(low, high)
125	
126	def limbs(parts: Parts<32n, 32n>) -> U32 & U32:
127	  Split{lo, hi} = parts
128	  (U32{lo}, U32{hi})
129	
130	def unpack(w: Word(64n)) -> U32 & U32:
131	  limbs(split(32n, 32n, w))