diff options
| author | Greg Brown <greg.brown@cl.cam.ac.uk> | 2022-01-07 09:59:41 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown@cl.cam.ac.uk> | 2022-01-07 09:59:41 +0000 |
| commit | 568792d2890028fbf7d011393b6516af27cc8b2f (patch) | |
| tree | 3a9f73f1990d127f85070ff0abde7812c135f016 /src/Helium/Data | |
| parent | 5052a3f5ddf5cc65bb5a19e644b01694ba34d0f5 (diff) | |
Rename ⟦_⟧ to float.
Diffstat (limited to 'src/Helium/Data')
| -rw-r--r-- | src/Helium/Data/Pseudocode.agda | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/src/Helium/Data/Pseudocode.agda b/src/Helium/Data/Pseudocode.agda index 7e6f6dc..f683193 100644 --- a/src/Helium/Data/Pseudocode.agda +++ b/src/Helium/Data/Pseudocode.agda @@ -73,7 +73,7 @@ record RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃ : Set (ℓsuc (b₁ field -- Arithmetic operations - ⟦_⟧ : ℤ → ℝ + float : ℤ → ℝ round : ℝ → ℤ _+ᶻ_ : Op₂ ℤ _+ʳ_ : Op₂ ℝ @@ -137,7 +137,7 @@ record RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃ : Set (ℓsuc (b₁ module divmod (≈ᶻ-trans : Transitive _≈ᶻ_) - (round∘⟦⟧ : ∀ x → x ≈ᶻ round ⟦ x ⟧) + (round∘float : ∀ x → x ≈ᶻ round (float x)) (round-cong : ∀ {x y} → x ≈ʳ y → round x ≈ᶻ round y) (0#-homo-round : round 0ℝ ≈ᶻ 0ℤ) where @@ -146,21 +146,21 @@ record RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃ : Set (ℓsuc (b₁ _div_ : ∀ (x y : ℤ) → .{≢0 : False (y ≟ᶻ 0ℤ)} → ℤ (x div y) {≢0} = - let f = (λ y≈0 → ≈ᶻ-trans (round∘⟦⟧ y) (≈ᶻ-trans (round-cong y≈0) 0#-homo-round)) in - round (⟦ x ⟧ *ʳ (⟦ y ⟧ ⁻¹) {map-False f ≢0}) + let f = (λ y≈0 → ≈ᶻ-trans (round∘float y) (≈ᶻ-trans (round-cong y≈0) 0#-homo-round)) in + round (float x *ʳ (float y ⁻¹) {map-False f ≢0}) _mod_ : ∀ (x y : ℤ) → .{≢0 : False (y ≟ᶻ 0ℤ)} → ℤ (x mod y) {≢0} = x +ᶻ -ᶻ y *ᶻ (x div y) {≢0} module 2^n≢0 (≈ᶻ-trans : Transitive _≈ᶻ_) - (round∘⟦⟧ : ∀ x → x ≈ᶻ round ⟦ x ⟧) + (round∘float : ∀ x → x ≈ᶻ round (float x)) (round-cong : ∀ {x y} → x ≈ʳ y → round x ≈ᶻ round y) (0#-homo-round : round 0ℝ ≈ᶻ 0ℤ) (2^n≢0 : ∀ n → False (2ℤ ^ᶻ n ≟ᶻ 0ℤ)) where - open divmod ≈ᶻ-trans round∘⟦⟧ round-cong 0#-homo-round public + open divmod ≈ᶻ-trans round∘float round-cong 0#-homo-round public _>>_ : ℤ → ℕ → ℤ x >> n = (x div (2ℤ ^ᶻ n)) {2^n≢0 n} @@ -170,14 +170,14 @@ record RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃ : Set (ℓsuc (b₁ module sliceᶻ (≈ᶻ-trans : Transitive _≈ᶻ_) - (round∘⟦⟧ : ∀ x → x ≈ᶻ round ⟦ x ⟧) + (round∘float : ∀ x → x ≈ᶻ round (float x)) (round-cong : ∀ {x y} → x ≈ʳ y → round x ≈ᶻ round y) (0#-homo-round : round 0ℝ ≈ᶻ 0ℤ) (2^n≢0 : ∀ n → False (2ℤ ^ᶻ n ≟ᶻ 0ℤ)) (*ᶻ-identityʳ : ∀ x → x *ᶻ 1ℤ ≈ᶻ x) where - open 2^n≢0 ≈ᶻ-trans round∘⟦⟧ round-cong 0#-homo-round 2^n≢0 public + open 2^n≢0 ≈ᶻ-trans round∘float round-cong 0#-homo-round 2^n≢0 public sliceᶻ : ∀ n i → ℤ → Bits (n ℕ-ℕ i) sliceᶻ zero zero z = [] |