blob: d6bce606e4d227526a0850403be715d6f2d1f86d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
|
{-# OPTIONS --without-K --safe #-}
------------------------------------------------------------------------
-- 2.2 Values
module Wasm.Expression.Values where
open import Data.Char using (Char; toℕ)
open import Data.Empty using (⊥)
open import Data.Fin using (Fin)
open import Data.Nat using (ℕ; zero; suc; _^_; pred)
open import Wasm.Expression.Utilities using (BitWidth; 32Bit; 64Bit)
infix 8 +_ -_
------------------------------------------------------------------------
-- 2.2.1 Bytes
Byte : Set
Byte = Fin 256
------------------------------------------------------------------------
-- 2.2.2 Integers
UnsignedInteger : ℕ → Set
UnsignedInteger n = Fin (2 ^ n)
data SignedInteger : ℕ → Set where
+_ : ∀ {n} → Fin n → SignedInteger (suc n)
-[1+_] : ∀ {n} → Fin n → SignedInteger (suc n)
UninterpretedInteger : ℕ → Set
UninterpretedInteger = UnsignedInteger
------------------------------------------------------------------------
-- 2.2.3 Floating-Point
signif : BitWidth → ℕ
signif 32Bit = 23
signif 64Bit = 52
expon : BitWidth → ℕ
expon 32Bit = 8
expon 64Bit = 11
data FloatMag : BitWidth → Set where
nan : ∀ {w} → (n : Fin (pred (2 ^ (signif w)))) → FloatMag w
∞ : ∀ {w} → FloatMag w
normal : ∀ {w} → (e : Fin (pred (pred (2 ^ (expon w))))) → (t : Fin (2 ^ (signif w))) → FloatMag w
subnormal : ∀ {w} → (t : Fin (pred (2 ^ (signif w)))) → FloatMag w
zero : ∀ {w} → FloatMag w
data Float : BitWidth → Set where
+_ : ∀ {w} → FloatMag w → Float w
-_ : ∀ {w} → FloatMag w → Float w
------------------------------------------------------------------------
-- 2.2.4 Names
module _ where
open import Data.Bool using (Bool; true; false; if_then_else_)
open import Data.List using (List; []; _∷_; length; map; sum)
open import Data.Nat using (_≤ᵇ_; _<_; z≤n; s≤s)
open import Data.Nat.Properties using (≤-step)
open import Data.Product using (_×_; _,_; proj₂; map₂)
open import Data.String using (String; toList)
halfEven? : ℕ → Bool × ℕ
halfEven? zero = true , 0
halfEven? (suc zero) = false , 0
halfEven? (suc (suc n)) = map₂ suc (halfEven? n)
n≢0⇒halfEven?<n : ∀ n → proj₂ (halfEven? (suc n)) < (suc n)
n≢0⇒halfEven?<n zero = s≤s z≤n
n≢0⇒halfEven?<n (suc zero) = s≤s (n≢0⇒halfEven?<n zero)
n≢0⇒halfEven?<n (suc (suc n)) = s≤s (≤-step (n≢0⇒halfEven?<n n))
asBits : ℕ → List Bool
asBits n = All.wfRec <-wellFounded _ Pred helper n
where
open import Data.Nat.Induction using (<-wellFounded)
open import Data.Nat.Properties using (module ≤-Reasoning)
open import Induction.WellFounded using (WfRec; module All)
open import Relation.Binary.PropositionalEquality using (cong; inspect; [_])
open ≤-Reasoning
Pred : ℕ → Set
Pred n = List Bool
helper : ∀ n → WfRec _<_ Pred n → List Bool
helper zero rec = []
helper (suc n) rec with halfEven? (suc n) | inspect halfEven? (suc n)
... | true , m | [ m≡n+1/2 ] = false ∷ rec m (begin-strict
m ≡˘⟨ cong proj₂ m≡n+1/2 ⟩
proj₂ (halfEven? (suc n)) <⟨ n≢0⇒halfEven?<n n ⟩
suc n ∎)
... | false , m | [ m≡n/2 ] = true ∷ rec m (begin-strict
m ≡˘⟨ cong proj₂ m≡n/2 ⟩
proj₂ (halfEven? (suc n)) <⟨ n≢0⇒halfEven?<n n ⟩
suc n ∎)
utf8Bytes : Char → ℕ
utf8Bytes c with asBits (toℕ c)
... | bits = if length bits ≤ᵇ 7 then
1
else if length bits ≤ᵇ 11 then
2
else if length bits ≤ᵇ 16 then
3
else
4
byteLength : String → ℕ
byteLength s = sum (map utf8Bytes (toList s))
data Name : Set where
name : ∀ s → {len : byteLength s < 2 ^ 32} → Name
|
