1	import Base
2	import ./decode_data.bend as D
3	
4	type Checked is Data:
5	  Value{value:U32}
6	  Invalid{}
7	def shifted(count:Nat,value:U32) -> U32:
8	  match count:
9	    case 0n: value
10	    case 1n+rest: shifted(rest,U32.mul(value,2))
11	def finite_checked(valid:Bool,value:U32,exponent:U32) -> Checked:
12	  match valid:
13	    case True{}:Value{shifted(U32.to_nat(U32.sub(exponent,1074)),value)}
14	    case False{}:Invalid{}
15	def finite(negative:Bool,high:U32,+low:U32,+exponent:U32) -> Checked:
16	  match negative high low:
17	    case False{} 0 0:Value{0}
18	    case False{} 0 n:finite_checked(U32.is_ge(exponent,1074) && U32.is_le(exponent,1105) && U32.is_le(exponent,U32.add(1074,U32.sub(31,U32.from_nat(U32.log2(n))))),n,exponent)
19	    case _ _ _:Invalid{}
20	def normalized(value:D.Numeric) -> Checked:
21	  match value:
22	    case D.Finite{negative,high,low,exponent}:finite(negative,high,low,exponent)
23	    case _:Invalid{}
24	def signed(valid:Bool,magnitude:Nat) -> Checked:
25	  match valid:
26	    case True{}:Value{U32.from_nat(magnitude)}
27	    case False{}:Invalid{}
28	def checked(raw:D.Raw) -> Checked:
29	  match raw:
30	    case D.Number{value}:Value{value}
31	    case D.SignedInteger{negative,+magnitude}:signed((Bool.not(negative) || Nat.is_eq(magnitude,0n)) && Nat.is_le(magnitude,4294967295n),magnitude)
32	    case D.Float{value}:normalized(D.float_numeric(F32.bits(value)))
33	    case D.Binary64{high,low}:normalized(D.binary_numeric(high,low))
34	    case _:Invalid{}