diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Helium/Data/Pseudocode/Core.agda | 18 | ||||
| -rw-r--r-- | src/Helium/Semantics/Axiomatic/Term.agda | 333 | ||||
| -rw-r--r-- | src/Helium/Semantics/Denotational/Core.agda | 16 |
3 files changed, 201 insertions, 166 deletions
diff --git a/src/Helium/Data/Pseudocode/Core.agda b/src/Helium/Data/Pseudocode/Core.agda index a229e8a..86bbffd 100644 --- a/src/Helium/Data/Pseudocode/Core.agda +++ b/src/Helium/Data/Pseudocode/Core.agda @@ -43,7 +43,7 @@ data HasEquality : Type → Set where fin : ∀ {n} → HasEquality (fin n) real : HasEquality real bit : HasEquality bit - bits : ∀ {n} → HasEquality (bits n) + bits : ∀ n → HasEquality (bits n) hasEquality? : Decidable HasEquality hasEquality? bool = yes bool @@ -51,7 +51,7 @@ hasEquality? int = yes int hasEquality? (fin n) = yes fin hasEquality? real = yes real hasEquality? bit = yes bit -hasEquality? (bits n) = yes bits +hasEquality? (bits n) = yes (bits n) hasEquality? (tuple n x) = no (λ ()) hasEquality? (array t n) = no (λ ()) @@ -69,10 +69,10 @@ isNumeric? (bits n) = no (λ ()) isNumeric? (tuple n x) = no (λ ()) isNumeric? (array t n) = no (λ ()) -combineNumeric : ∀ t₁ t₂ → {isNumeric₁ : True (isNumeric? t₁)} → {isNumeric₂ : True (isNumeric? t₂)} → Type -combineNumeric int int = int -combineNumeric int real = real -combineNumeric real _ = real +combineNumeric : ∀ t₁ t₂ → (isNumeric₁ : True (isNumeric? t₁)) → (isNumeric₂ : True (isNumeric? t₂)) → Type +combineNumeric int int _ _ = int +combineNumeric int real _ _ = real +combineNumeric real _ _ _ = real data Sliced : Set where bits : Sliced @@ -147,8 +147,8 @@ module Code {o} (Σ : Vec Type o) where cut : ∀ {m n t} → Expression Γ (asType t (n ℕ.+ m)) → Expression Γ (fin (suc n)) → Expression Γ (tuple 2 (asType t m ∷ asType t n ∷ [])) cast : ∀ {i j t} → .(eq : i ≡ j) → Expression Γ (asType t i) → Expression Γ (asType t j) -_ : ∀ {t} {isNumeric : True (isNumeric? t)} → Expression Γ t → Expression Γ t - _+_ : ∀ {t₁ t₂} {isNumeric₁ : True (isNumeric? t₁)} {isNumeric₂ : True (isNumeric? t₂)} → Expression Γ t₁ → Expression Γ t₂ → Expression Γ (combineNumeric t₁ t₂ {isNumeric₁} {isNumeric₂}) - _*_ : ∀ {t₁ t₂} {isNumeric₁ : True (isNumeric? t₁)} {isNumeric₂ : True (isNumeric? t₂)} → Expression Γ t₁ → Expression Γ t₂ → Expression Γ (combineNumeric t₁ t₂ {isNumeric₁} {isNumeric₂}) + _+_ : ∀ {t₁ t₂} {isNumeric₁ : True (isNumeric? t₁)} {isNumeric₂ : True (isNumeric? t₂)} → Expression Γ t₁ → Expression Γ t₂ → Expression Γ (combineNumeric t₁ t₂ isNumeric₁ isNumeric₂) + _*_ : ∀ {t₁ t₂} {isNumeric₁ : True (isNumeric? t₁)} {isNumeric₂ : True (isNumeric? t₂)} → Expression Γ t₁ → Expression Γ t₂ → Expression Γ (combineNumeric t₁ t₂ isNumeric₁ isNumeric₂) -- _/_ : Expression Γ real → Expression Γ real → Expression Γ real _^_ : ∀ {t} {isNumeric : True (isNumeric? t)} → Expression Γ t → ℕ → Expression Γ t _>>_ : Expression Γ int → ℕ → Expression Γ int @@ -312,7 +312,7 @@ module Code {o} (Σ : Vec Type o) where slice′ : ∀ {n Γ i j t} → Expression {n} Γ (asType t (i ℕ.+ j)) → Expression Γ (fin (suc j)) → Expression Γ (asType t i) slice′ {i = i} e₁ e₂ = slice (cast (+-comm i _) e₁) e₂ - _-_ : ∀ {n Γ t₁ t₂} {isNumeric₁ : True (isNumeric? t₁)} {isNumeric₂ : True (isNumeric? t₂)} → Expression {n} Γ t₁ → Expression Γ t₂ → Expression Γ (combineNumeric t₁ t₂ {isNumeric₁} {isNumeric₂}) + _-_ : ∀ {n Γ t₁ t₂} {isNumeric₁ : True (isNumeric? t₁)} {isNumeric₂ : True (isNumeric? t₂)} → Expression {n} Γ t₁ → Expression Γ t₂ → Expression Γ (combineNumeric t₁ t₂ isNumeric₁ isNumeric₂) _-_ {isNumeric₂ = isNumeric₂} x y = x + (-_ {isNumeric = isNumeric₂} y) _<<_ : ∀ {n Γ} → Expression {n} Γ int → ℕ → Expression Γ int diff --git a/src/Helium/Semantics/Axiomatic/Term.agda b/src/Helium/Semantics/Axiomatic/Term.agda index 980b85a..1ccef89 100644 --- a/src/Helium/Semantics/Axiomatic/Term.agda +++ b/src/Helium/Semantics/Axiomatic/Term.agda @@ -23,14 +23,15 @@ open import Data.Nat as ℕ using (ℕ; suc) import Data.Nat.Properties as ℕₚ open import Data.Product using (∃; _×_; _,_; proj₁; proj₂; uncurry; dmap) open import Data.Vec as Vec using (Vec; []; _∷_; _++_; lookup) +import Data.Vec.Functional as VecF import Data.Vec.Properties as Vecₚ open import Data.Vec.Relation.Unary.All using (All; []; _∷_) -open import Function using (_∘_; _∘₂_; id) +open import Function using (_∘_; _∘₂_; id; flip) open import Helium.Data.Pseudocode.Core import Helium.Data.Pseudocode.Manipulate as M open import Helium.Semantics.Axiomatic.Core rawPseudocode open import Level using (_⊔_; lift; lower) -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality hiding ([_]) renaming (subst to ≡-subst) open import Relation.Nullary using (does; yes; no; ¬_) open import Relation.Nullary.Decidable.Core using (True; toWitness) open import Relation.Nullary.Negation using (contradiction) @@ -51,7 +52,7 @@ castType : Term Σ Γ Δ t → t ≡ t′ → Term Σ Γ Δ t′ castType (state i) refl = state i castType (var i) refl = var i castType (meta i) refl = meta i -castType (func f ts) eq = func (subst (Transform _) eq f) ts +castType (func f ts) eq = func (≡-subst (Transform _) eq f) ts substState : Term Σ Γ Δ t → ∀ i → Term Σ Γ Δ (lookup Σ i) → Term Σ Γ Δ t substState (state i) j t′ with i Fin.≟ j @@ -141,20 +142,147 @@ wknMetas τs (func f ts) = func f (helper ts) helper [] = [] helper (t ∷ ts) = wknMetas τs t ∷ helper ts -module _ {Σ : Vec Type o} (2≉0 : ¬ 2 ℝ′.×′ 1ℝ ℝ.≈ 0ℝ) where - open Code Σ +func₀ : ⟦ t ⟧ₜ → Term Σ Γ Δ t +func₀ f = func (λ _ → f) [] - 𝒦 : Literal t → Term Σ Γ Δ t - 𝒦 (x ′b) = func (λ _ → lift x) [] - 𝒦 (x ′i) = func (λ _ → lift (x ℤ′.×′ 1ℤ)) [] - 𝒦 (x ′f) = func (λ _ → lift x) [] - 𝒦 (x ′r) = func (λ _ → lift (x ℝ′.×′ 1ℝ)) [] - 𝒦 (x ′x) = func (λ _ → lift (Bool.if x then 1𝔹 else 0𝔹)) [] - 𝒦 ([] ′xs) = func (λ _ → []) [] - 𝒦 ((x ∷ xs) ′xs) = func (λ (x , xs , _) → xs Vec.∷ʳ x) (𝒦 (x ′x) ∷ 𝒦 (xs ′xs) ∷ []) - 𝒦 (x ′a) = func (λ (x , _) → Vec.replicate x) (𝒦 x ∷ []) +func₁ : (⟦ t ⟧ₜ → ⟦ t′ ⟧ₜ) → Term Σ Γ Δ t → Term Σ Γ Δ t′ +func₁ f t = func (λ (x , _) → f x) (t ∷ []) - ℰ : Expression Γ t → Term Σ Γ Δ t +func₂ : (⟦ t₁ ⟧ₜ → ⟦ t₂ ⟧ₜ → ⟦ t′ ⟧ₜ) → Term Σ Γ Δ t₁ → Term Σ Γ Δ t₂ → Term Σ Γ Δ t′ +func₂ f t₁ t₂ = func (λ (x , y , _) → f x y) (t₁ ∷ t₂ ∷ []) + +[_][_≟_] : HasEquality t → Term Σ Γ Δ t → Term Σ Γ Δ t → Term Σ Γ Δ bool +[ bool ][ t ≟ t′ ] = func₂ (λ (lift x) (lift y) → lift (does (x Bool.≟ y))) t t′ +[ int ][ t ≟ t′ ] = func₂ (λ (lift x) (lift y) → lift (does (x ≟ᶻ y))) t t′ +[ fin ][ t ≟ t′ ] = func₂ (λ (lift x) (lift y) → lift (does (x Fin.≟ y))) t t′ +[ real ][ t ≟ t′ ] = func₂ (λ (lift x) (lift y) → lift (does (x ≟ʳ y))) t t′ +[ bit ][ t ≟ t′ ] = func₂ (λ (lift x) (lift y) → lift (does (x ≟ᵇ₁ y))) t t′ +[ bits n ][ t ≟ t′ ] = func₂ (λ xs ys → lift (does (VecF.fromVec (Vec.map lower xs) ≟ᵇ VecF.fromVec (Vec.map lower ys)))) t t′ + +[_][_<?_] : IsNumeric t → Term Σ Γ Δ t → Term Σ Γ Δ t → Term Σ Γ Δ bool +[ int ][ t <? t′ ] = func₂ (λ (lift x) (lift y) → lift (does (x <ᶻ? y))) t t′ +[ real ][ t <? t′ ] = func₂ (λ (lift x) (lift y) → lift (does (x <ʳ? y))) t t′ + +[_][_] : ∀ t → Term Σ Γ Δ (elemType t) → Term Σ Γ Δ (asType t 1) +[ bits ][ t ] = func₁ (_∷ []) t +[ array τ ][ t ] = func₁ (_∷ []) t + +unbox : ∀ t → Term Σ Γ Δ (asType t 1) → Term Σ Γ Δ (elemType t) +unbox bits = func₁ Vec.head +unbox (array t) = func₁ Vec.head + +castV : ∀ {a} {A : Set a} {m n} → .(eq : m ≡ n) → Vec A m → Vec A n +castV {n = 0} eq [] = [] +castV {n = suc n} eq (x ∷ xs) = x ∷ castV (ℕₚ.suc-injective eq) xs + +cast′ : ∀ t → .(eq : m ≡ n) → ⟦ asType t m ⟧ₜ → ⟦ asType t n ⟧ₜ +cast′ bits eq = castV eq +cast′ (array τ) eq = castV eq + +cast : ∀ t → .(eq : m ≡ n) → Term Σ Γ Δ (asType t m) → Term Σ Γ Δ (asType t n) +cast τ eq = func₁ (cast′ τ eq) + +[_][-_] : IsNumeric t → Term Σ Γ Δ t → Term Σ Γ Δ t +[ int ][- t ] = func₁ (lift ∘ ℤ.-_ ∘ lower) t +[ real ][- t ] = func₁ (lift ∘ ℝ.-_ ∘ lower) t + +[_,_,_,_][_+_] : ∀ t₁ t₂ → (isNum₁ : True (isNumeric? t₁)) → (isNum₂ : True (isNumeric? t₂)) → Term Σ Γ Δ t₁ → Term Σ Γ Δ t₂ → Term Σ Γ Δ (combineNumeric t₁ t₂ isNum₁ isNum₂) +[ int , int , _ , _ ][ t + t′ ] = func₂ (λ (lift x) (lift y) → lift (x ℤ.+ y)) t t′ +[ int , real , _ , _ ][ t + t′ ] = func₂ (λ (lift x) (lift y) → lift (x /1 ℝ.+ y)) t t′ +[ real , int , _ , _ ][ t + t′ ] = func₂ (λ (lift x) (lift y) → lift (x ℝ.+ y /1)) t t′ +[ real , real , _ , _ ][ t + t′ ] = func₂ (λ (lift x) (lift y) → lift (x ℝ.+ y)) t t′ + +[_,_,_,_][_*_] : ∀ t₁ t₂ → (isNum₁ : True (isNumeric? t₁)) → (isNum₂ : True (isNumeric? t₂)) → Term Σ Γ Δ t₁ → Term Σ Γ Δ t₂ → Term Σ Γ Δ (combineNumeric t₁ t₂ isNum₁ isNum₂) +[ int , int , _ , _ ][ t * t′ ] = func₂ (λ (lift x) (lift y) → lift (x ℤ.* y)) t t′ +[ int , real , _ , _ ][ t * t′ ] = func₂ (λ (lift x) (lift y) → lift (x /1 ℝ.* y)) t t′ +[ real , int , _ , _ ][ t * t′ ] = func₂ (λ (lift x) (lift y) → lift (x ℝ.* y /1)) t t′ +[ real , real , _ , _ ][ t * t′ ] = func₂ (λ (lift x) (lift y) → lift (x ℝ.* y)) t t′ + +[_][_^_] : IsNumeric t → Term Σ Γ Δ t → ℕ → Term Σ Γ Δ t +[ int ][ t ^ n ] = func₁ (lift ∘ (ℤ′._^′ n) ∘ lower) t +[ real ][ t ^ n ] = func₁ (lift ∘ (ℝ′._^′ n) ∘ lower) t + +2≉0 : Set _ +2≉0 = ¬ 2 ℝ′.×′ 1ℝ ℝ.≈ 0ℝ + +[_][_>>_] : 2≉0 → Term Σ Γ Δ int → ℕ → Term Σ Γ Δ int +[ 2≉0 ][ t >> n ] = func₁ (lift ∘ ⌊_⌋ ∘ (ℝ._* 2≉0 ℝ.⁻¹ ℝ′.^′ n) ∘ _/1 ∘ lower) t + +-- 0 of y is 0 of result +join′ : ∀ t → ⟦ asType t m ⟧ₜ → ⟦ asType t n ⟧ₜ → ⟦ asType t (n ℕ.+ m) ⟧ₜ +join′ bits = flip _++_ +join′ (array t) = flip _++_ + +take′ : ∀ t m {n} → ⟦ asType t (m ℕ.+ n) ⟧ₜ → ⟦ asType t m ⟧ₜ +take′ bits m = Vec.take m +take′ (array t) m = Vec.take m + +drop′ : ∀ t m {n} → ⟦ asType t (m ℕ.+ n) ⟧ₜ → ⟦ asType t n ⟧ₜ +drop′ bits m = Vec.drop m +drop′ (array t) m = Vec.drop m + +private + m≤n⇒m+k≡n : ∀ {m n} → m ℕ.≤ n → ∃ λ k → m ℕ.+ k ≡ n + m≤n⇒m+k≡n ℕ.z≤n = _ , refl + m≤n⇒m+k≡n (ℕ.s≤s m≤n) = dmap id (cong suc) (m≤n⇒m+k≡n m≤n) + + slicedSize : ∀ n m (i : Fin (suc n)) → ∃ λ k → n ℕ.+ m ≡ Fin.toℕ i ℕ.+ (m ℕ.+ k) × Fin.toℕ i ℕ.+ k ≡ n + slicedSize n m i = k , (begin + n ℕ.+ m ≡˘⟨ cong (ℕ._+ m) (proj₂ i+k≡n) ⟩ + (Fin.toℕ i ℕ.+ k) ℕ.+ m ≡⟨ ℕₚ.+-assoc (Fin.toℕ i) k m ⟩ + Fin.toℕ i ℕ.+ (k ℕ.+ m) ≡⟨ cong (Fin.toℕ i ℕ.+_) (ℕₚ.+-comm k m) ⟩ + Fin.toℕ i ℕ.+ (m ℕ.+ k) ∎) , + proj₂ i+k≡n + where + open ≡-Reasoning + i+k≡n = m≤n⇒m+k≡n (ℕₚ.≤-pred (Finₚ.toℕ<n i)) + k = proj₁ i+k≡n + +-- 0 of x is i of result +splice′ : ∀ t → ⟦ asType t m ⟧ₜ → ⟦ asType t n ⟧ₜ → ⟦ fin (suc n) ⟧ₜ → ⟦ asType t (n ℕ.+ m) ⟧ₜ +splice′ {m = m} t x y (lift i) = cast′ t eq (join′ t (join′ t high x) low) + where + reasoning = slicedSize _ m i + k = proj₁ reasoning + n≡i+k = sym (proj₂ (proj₂ reasoning)) + low = take′ t (Fin.toℕ i) (cast′ t n≡i+k y) + high = drop′ t (Fin.toℕ i) (cast′ t n≡i+k y) + eq = sym (proj₁ (proj₂ reasoning)) + +splice : ∀ t → Term Σ Γ Δ (asType t m) → Term Σ Γ Δ (asType t n) → Term Σ Γ Δ (fin (suc n)) → Term Σ Γ Δ (asType t (n ℕ.+ m)) +splice τ t₁ t₂ t′ = func (λ (x , y , i , _) → splice′ τ x y i) (t₁ ∷ t₂ ∷ t′ ∷ []) + +-- i of x is 0 of first +cut′ : ∀ t → ⟦ asType t (n ℕ.+ m) ⟧ₜ → ⟦ fin (suc n) ⟧ₜ → ⟦ asType t m ∷ asType t n ∷ [] ⟧ₜ′ +cut′ {m = m} t x (lift i) = middle , cast′ t i+k≡n (join′ t high low) , _ + where + reasoning = slicedSize _ m i + k = proj₁ reasoning + i+k≡n = proj₂ (proj₂ reasoning) + eq = proj₁ (proj₂ reasoning) + low = take′ t (Fin.toℕ i) (cast′ t eq x) + middle = take′ t m (drop′ t (Fin.toℕ i) (cast′ t eq x)) + high = drop′ t m (drop′ t (Fin.toℕ i) (cast′ t eq x)) + +cut : ∀ t → Term Σ Γ Δ (asType t (n ℕ.+ m)) → Term Σ Γ Δ (fin (suc n)) → Term Σ Γ Δ (tuple _ (asType t m ∷ asType t n ∷ [])) +cut τ t t′ = func₂ (cut′ τ) t t′ + +flatten : ∀ {ms : Vec ℕ n} → ⟦ Vec.map fin ms ⟧ₜ′ → All Fin ms +flatten {ms = []} _ = [] +flatten {ms = _ ∷ ms} (lift x , xs) = x ∷ flatten xs + +𝒦 : Literal t → Term Σ Γ Δ t +𝒦 (x ′b) = func₀ (lift x) +𝒦 (x ′i) = func₀ (lift (x ℤ′.×′ 1ℤ)) +𝒦 (x ′f) = func₀ (lift x) +𝒦 (x ′r) = func₀ (lift (x ℝ′.×′ 1ℝ)) +𝒦 (x ′x) = func₀ (lift (Bool.if x then 1𝔹 else 0𝔹)) +𝒦 ([] ′xs) = func₀ [] +𝒦 ((x ∷ xs) ′xs) = func₂ (flip Vec._∷ʳ_) (𝒦 (x ′x)) (𝒦 (xs ′xs)) +𝒦 (x ′a) = func₁ Vec.replicate (𝒦 x) + +module _ (2≉0 : 2≉0) where + ℰ : Code.Expression Σ Γ t → Term Σ Γ Δ t ℰ e = (uncurry helper) (M.elimFunctions e) where 1+m⊔n≡1+k : ∀ m n → ∃ λ k → suc m ℕ.⊔ n ≡ suc k @@ -181,142 +309,49 @@ module _ {Σ : Vec Type o} (2≉0 : ¬ 2 ℝ′.×′ 1ℝ ℝ.≈ 0ℝ) where pull-last {0} {0} refl = refl pull-last {suc x} {0} () - equal : HasEquality t → ⟦ t ⟧ₜ → ⟦ t ⟧ₜ → ⟦ bool ⟧ₜ - equal bool (lift x) (lift y) = lift (does (x Bool.≟ y)) - equal int (lift x) (lift y) = lift (does (x ≟ᶻ y)) - equal fin (lift x) (lift y) = lift (does (x Fin.≟ y)) - equal real (lift x) (lift y) = lift (does (x ≟ʳ y)) - equal bit (lift x) (lift y) = lift (does (x ≟ᵇ₁ y)) - equal bits [] [] = lift (Bool.true) - equal bits (x ∷ xs) (y ∷ ys) = lift (lower (equal bit x y) Bool.∧ lower (equal bits xs ys)) - - less : IsNumeric t → ⟦ t ⟧ₜ → ⟦ t ⟧ₜ → ⟦ bool ⟧ₜ - less int (lift x) (lift y) = lift (does (x <ᶻ? y)) - less real (lift x) (lift y) = lift (does (x <ʳ? y)) - - box : ∀ t → ⟦ elemType t ⟧ₜ → ⟦ asType t 1 ⟧ₜ - box bits x = x ∷ [] - box (array t) x = x ∷ [] - - unboxed : ∀ t → ⟦ asType t 1 ⟧ₜ → ⟦ elemType t ⟧ₜ - unboxed bits (x ∷ []) = x - unboxed (array t) (x ∷ []) = x - - casted : ∀ t {i j} → .(eq : i ≡ j) → ⟦ asType t i ⟧ₜ → ⟦ asType t j ⟧ₜ - casted bits {j = 0} eq [] = [] - casted bits {j = suc j} eq (x ∷ xs) = x ∷ casted bits (ℕₚ.suc-injective eq) xs - casted (array t) {j = 0} eq [] = [] - casted (array t) {j = suc j} eq (x ∷ xs) = x ∷ casted (array t) (ℕₚ.suc-injective eq) xs - - neg : IsNumeric t → ⟦ t ⟧ₜ → ⟦ t ⟧ₜ - neg int (lift x) = lift (ℤ.- x) - neg real (lift x) = lift (ℝ.- x) - - add : (isNum₁ : True (isNumeric? t₁)) → (isNum₂ : True (isNumeric? t₂)) → ⟦ t₁ ⟧ₜ → ⟦ t₂ ⟧ₜ → ⟦ combineNumeric t₁ t₂ {isNum₁} {isNum₂} ⟧ₜ - add {int} {int} _ _ (lift x) (lift y) = lift (x ℤ.+ y) - add {int} {real} _ _ (lift x) (lift y) = lift (x /1 ℝ.+ y) - add {real} {int} _ _ (lift x) (lift y) = lift (x ℝ.+ y /1) - add {real} {real} _ _ (lift x) (lift y) = lift (x ℝ.+ y) - - mul : (isNum₁ : True (isNumeric? t₁)) → (isNum₂ : True (isNumeric? t₂)) → ⟦ t₁ ⟧ₜ → ⟦ t₂ ⟧ₜ → ⟦ combineNumeric t₁ t₂ {isNum₁} {isNum₂} ⟧ₜ - mul {int} {int} _ _ (lift x) (lift y) = lift (x ℤ.* y) - mul {int} {real} _ _ (lift x) (lift y) = lift (x /1 ℝ.* y) - mul {real} {int} _ _ (lift x) (lift y) = lift (x ℝ.* y /1) - mul {real} {real} _ _ (lift x) (lift y) = lift (x ℝ.* y) - - pow : IsNumeric t → ⟦ t ⟧ₜ → ℕ → ⟦ t ⟧ₜ - pow int (lift x) y = lift (x ℤ′.^′ y) - pow real (lift x) y = lift (x ℝ′.^′ y) - - shift : ⟦ int ⟧ₜ → ℕ → ⟦ int ⟧ₜ - shift (lift x) n = lift (⌊ x /1 ℝ.* 2≉0 ℝ.⁻¹ ℝ′.^′ n ⌋) - - flatten : ∀ {ms : Vec ℕ n} → ⟦ Vec.map fin ms ⟧ₜ′ → All Fin ms - flatten {ms = []} _ = [] - flatten {ms = _ ∷ ms} (lift x , xs) = x ∷ flatten xs - - private - m≤n⇒m+k≡n : ∀ {m n} → m ℕ.≤ n → ∃ λ k → m ℕ.+ k ≡ n - m≤n⇒m+k≡n ℕ.z≤n = _ , refl - m≤n⇒m+k≡n (ℕ.s≤s m≤n) = dmap id (cong suc) (m≤n⇒m+k≡n m≤n) - - slicedSize : ∀ n m (i : Fin (suc n)) → ∃ λ k → n ℕ.+ m ≡ Fin.toℕ i ℕ.+ (m ℕ.+ k) × Fin.toℕ i ℕ.+ k ≡ n - slicedSize n m i = k , (begin - n ℕ.+ m ≡˘⟨ cong (ℕ._+ m) (proj₂ i+k≡n) ⟩ - (Fin.toℕ i ℕ.+ k) ℕ.+ m ≡⟨ ℕₚ.+-assoc (Fin.toℕ i) k m ⟩ - Fin.toℕ i ℕ.+ (k ℕ.+ m) ≡⟨ cong (Fin.toℕ i ℕ.+_) (ℕₚ.+-comm k m) ⟩ - Fin.toℕ i ℕ.+ (m ℕ.+ k) ∎) , - proj₂ i+k≡n - where - open ≡-Reasoning - i+k≡n = m≤n⇒m+k≡n (ℕₚ.≤-pred (Finₚ.toℕ<n i)) - k = proj₁ i+k≡n - - -- 0 of y is 0 of result - join : ∀ t → ⟦ asType t m ⟧ₜ → ⟦ asType t n ⟧ₜ → ⟦ asType t (n ℕ.+ m) ⟧ₜ - join bits xs ys = ys ++ xs - join (array t) xs ys = ys ++ xs - - take : ∀ t i {j} → ⟦ asType t (i ℕ.+ j) ⟧ₜ → ⟦ asType t i ⟧ₜ - take bits i xs = Vec.take i xs - take (array t) i xs = Vec.take i xs - - drop : ∀ t i {j} → ⟦ asType t (i ℕ.+ j) ⟧ₜ → ⟦ asType t j ⟧ₜ - drop bits i xs = Vec.drop i xs - drop (array t) i xs = Vec.drop i xs - - -- 0 of x is i of result - spliced : ∀ t {m n} → ⟦ asType t m ⟧ₜ → ⟦ asType t n ⟧ₜ → ⟦ fin (suc n) ⟧ₜ → ⟦ asType t (n ℕ.+ m) ⟧ₜ - spliced t {m} x y (lift i) = casted t eq (join t (join t high x) low) - where - reasoning = slicedSize _ m i - k = proj₁ reasoning - n≡i+k = sym (proj₂ (proj₂ reasoning)) - low = take t (Fin.toℕ i) (casted t n≡i+k y) - high = drop t (Fin.toℕ i) (casted t n≡i+k y) - eq = sym (proj₁ (proj₂ reasoning)) - - -- i of x is 0 of first - sliced : ∀ t {m n} → ⟦ asType t (n ℕ.+ m) ⟧ₜ → ⟦ fin (suc n) ⟧ₜ → ⟦ asType t m ∷ asType t n ∷ [] ⟧ₜ′ - sliced t {m} x (lift i) = middle , casted t i+k≡n (join t high low) , _ - where - reasoning = slicedSize _ m i - k = proj₁ reasoning - i+k≡n = proj₂ (proj₂ reasoning) - eq = proj₁ (proj₂ reasoning) - low = take t (Fin.toℕ i) (casted t eq x) - middle = take t m (drop t (Fin.toℕ i) (casted t eq x)) - high = drop t m (drop t (Fin.toℕ i) (casted t eq x)) - - helper : ∀ (e : Expression Γ t) → M.callDepth e ≡ 0 → Term Σ Γ Δ t + helper : ∀ (e : Code.Expression Σ Γ t) → M.callDepth e ≡ 0 → Term Σ Γ Δ t helper (Code.lit x) eq = 𝒦 x helper (Code.state i) eq = state i helper (Code.var i) eq = var i - helper (Code.abort e) eq = func (λ ()) (helper e eq ∷ []) - helper (_≟_ {hasEquality = hasEq} e e₁) eq = func (λ (x , y , _) → equal (toWitness hasEq) x y) (helper e (pull-0₂ eq) ∷ helper e₁ (pull-last eq) ∷ []) - helper (_<?_ {isNumeric = isNum} e e₁) eq = func (λ (x , y , _) → less (toWitness isNum) x y) (helper e (pull-0₂ eq) ∷ helper e₁ (pull-last eq) ∷ []) - helper (Code.inv e) eq = func (λ (lift b , _) → lift (Bool.not b)) (helper e eq ∷ []) - helper (e Code.&& e₁) eq = func (λ (lift b , lift b₁ , _) → lift (b Bool.∧ b₁)) (helper e (pull-0₂ eq) ∷ helper e₁ (pull-last eq) ∷ []) - helper (e Code.|| e₁) eq = func (λ (lift b , lift b₁ , _) → lift (b Bool.∨ b₁)) (helper e (pull-0₂ eq) ∷ helper e₁ (pull-last eq) ∷ []) - helper (Code.not e) eq = func (λ (xs , _) → Vec.map (lift ∘ 𝔹.¬_ ∘ lower) xs) (helper e eq ∷ []) - helper (e Code.and e₁) eq = func (λ (xs , ys , _) → Vec.zipWith (lift ∘₂ 𝔹._∧_ ) (Vec.map lower xs) (Vec.map lower ys)) (helper e (pull-0₂ eq) ∷ helper e₁ (pull-last eq) ∷ []) - helper (e Code.or e₁) eq = func (λ (xs , ys , _) → Vec.zipWith (lift ∘₂ 𝔹._∨_ ) (Vec.map lower xs) (Vec.map lower ys)) (helper e (pull-0₂ eq) ∷ helper e₁ (pull-last eq) ∷ []) - helper ([_] {t = t} e) eq = func (λ (x , _) → box t x) (helper e eq ∷ []) - helper (Code.unbox {t = t} e) eq = func (λ (x , _) → unboxed t x) (helper e eq ∷ []) - helper (Code.splice {t = t} e e₁ e₂) eq = func (λ (x , y , i , _) → spliced t x y i) (helper e (pull-0₃ eq) ∷ helper e₁ (pull-1₃ (M.callDepth e) eq) ∷ helper e₂ (pull-last eq) ∷ []) - helper (Code.cut {t = t} e e₁) eq = func (λ (x , i , _) → sliced t x i) (helper e (pull-0₂ eq) ∷ helper e₁ (pull-last eq) ∷ []) - helper (Code.cast {t = t} i≡j e) eq = func (λ (x , _) → casted t i≡j x) (helper e eq ∷ []) - helper (-_ {isNumeric = isNum} e) eq = func (λ (x , _) → neg (toWitness isNum) x) (helper e eq ∷ []) - helper (_+_ {isNumeric₁ = isNum₁} {isNumeric₂ = isNum₂} e e₁) eq = func (λ (x , y , _) → add isNum₁ isNum₂ x y) (helper e (pull-0₂ eq) ∷ helper e₁ (pull-last eq) ∷ []) - helper (_*_ {isNumeric₁ = isNum₁} {isNumeric₂ = isNum₂} e e₁) eq = func (λ (x , y , _) → mul isNum₁ isNum₂ x y) (helper e (pull-0₂ eq) ∷ helper e₁ (pull-last eq) ∷ []) - helper (_^_ {isNumeric = isNum} e y) eq = func (λ (x , _) → pow (toWitness isNum) x y) (helper e eq ∷ []) - helper (e >> n) eq = func (λ (x , _) → shift x n) (helper e eq ∷ []) - helper (Code.rnd e) eq = func (λ (lift x , _) → lift ⌊ x ⌋) (helper e eq ∷ []) - helper (Code.fin f e) eq = func (λ (xs , _) → lift (f (flatten xs))) (helper e eq ∷ []) - helper (Code.asInt e) eq = func (λ (lift x , _) → lift (Fin.toℕ x ℤ′.×′ 1ℤ)) (helper e eq ∷ []) - helper Code.nil eq = func (λ args → _) [] - helper (Code.cons e e₁) eq = func (λ (x , xs , _) → x , xs) (helper e (pull-0₂ eq) ∷ helper e₁ (pull-last eq) ∷ []) - helper (Code.head e) eq = func (λ ((x , _) , _) → x) (helper e eq ∷ []) - helper (Code.tail e) eq = func (λ ((_ , xs) , _) → xs) (helper e eq ∷ []) + helper (Code.abort e) eq = func₁ (λ ()) (helper e eq) + helper (Code._≟_ {hasEquality = hasEq} e e₁) eq = [ toWitness hasEq ][ helper e (pull-0₂ eq) ≟ helper e₁ (pull-last eq) ] + helper (Code._<?_ {isNumeric = isNum} e e₁) eq = [ toWitness isNum ][ helper e (pull-0₂ eq) <? helper e₁ (pull-last eq) ] + helper (Code.inv e) eq = func₁ (lift ∘ Bool.not ∘ lower) (helper e eq) + helper (e Code.&& e₁) eq = func₂ (λ (lift x) (lift y) → lift (x Bool.∧ y)) (helper e (pull-0₂ eq)) (helper e₁ (pull-last eq)) + helper (e Code.|| e₁) eq = func₂ (λ (lift x) (lift y) → lift (x Bool.∨ y)) (helper e (pull-0₂ eq)) (helper e₁ (pull-last eq)) + helper (Code.not e) eq = func₁ (Vec.map (lift ∘ 𝔹.¬_ ∘ lower)) (helper e eq) + helper (e Code.and e₁) eq = func₂ (λ xs ys → Vec.zipWith (λ (lift x) (lift y) → lift (x 𝔹.∧ y)) xs ys) (helper e (pull-0₂ eq)) (helper e₁ (pull-last eq)) + helper (e Code.or e₁) eq = func₂ (λ xs ys → Vec.zipWith (λ (lift x) (lift y) → lift (x 𝔹.∨ y)) xs ys) (helper e (pull-0₂ eq)) (helper e₁ (pull-last eq)) + helper (Code.[_] {t = t} e) eq = [ t ][ helper e eq ] + helper (Code.unbox {t = t} e) eq = unbox t (helper e eq) + helper (Code.splice {t = t} e e₁ e₂) eq = splice t (helper e (pull-0₃ eq)) (helper e₁ (pull-1₃ (M.callDepth e) eq)) (helper e₂ (pull-last eq)) + helper (Code.cut {t = t} e e₁) eq = cut t (helper e (pull-0₂ eq)) (helper e₁ (pull-last eq)) + helper (Code.cast {t = t} i≡j e) eq = cast t i≡j (helper e eq) + helper (Code.-_ {isNumeric = isNum} e) eq = [ toWitness isNum ][- helper e eq ] + helper (Code._+_ {isNumeric₁ = isNum₁} {isNumeric₂ = isNum₂} e e₁) eq = [ _ , _ , isNum₁ , isNum₂ ][ helper e (pull-0₂ eq) + helper e₁ (pull-last eq) ] + helper (Code._*_ {isNumeric₁ = isNum₁} {isNumeric₂ = isNum₂} e e₁) eq = [ _ , _ , isNum₁ , isNum₂ ][ helper e (pull-0₂ eq) * helper e₁ (pull-last eq) ] + helper (Code._^_ {isNumeric = isNum} e y) eq = [ toWitness isNum ][ helper e eq ^ y ] + helper (e Code.>> n) eq = [ 2≉0 ][ helper e eq >> n ] + helper (Code.rnd e) eq = func₁ (lift ∘ ⌊_⌋ ∘ lower) (helper e eq) + helper (Code.fin f e) eq = func₁ (lift ∘ f ∘ flatten) (helper e eq) + helper (Code.asInt e) eq = func₁ (lift ∘ (ℤ′._×′ 1ℤ) ∘ Fin.toℕ ∘ lower) (helper e eq) + helper Code.nil eq = func₀ _ + helper (Code.cons e e₁) eq = func₂ _,_ (helper e (pull-0₂ eq)) (helper e₁ (pull-last eq)) + helper (Code.head e) eq = func₁ proj₁ (helper e eq) + helper (Code.tail e) eq = func₁ proj₂ (helper e eq) helper (Code.call f es) eq = contradiction (trans (sym eq) (proj₂ (1+m⊔n≡1+k (M.funCallDepth f) (M.callDepth′ es)))) ℕₚ.0≢1+n helper (Code.if e then e₁ else e₂) eq = func (λ (lift b , x , x₁ , _) → Bool.if b then x else x₁) (helper e (pull-0₃ eq) ∷ helper e₁ (pull-1₃ (M.callDepth e) eq) ∷ helper e₂ (pull-last eq) ∷ []) + + subst : Term Σ Γ Δ t → {e : Code.Expression Σ Γ t′} → Code.CanAssign Σ e → Term Σ Γ Δ t′ → Term Σ Γ Δ t + subst t (Code.state i) t′ = substState t i t′ + subst t (Code.var i) t′ = substVar t i t′ + subst t (Code.abort e) t′ = func₁ (λ ()) (ℰ e) + subst t (Code.[_] {t = τ} ref) t′ = subst t ref (unbox τ t′) + subst t (Code.unbox {t = τ} ref) t′ = subst t ref [ τ ][ t′ ] + subst t (Code.splice {t = τ} ref ref₁ e₃) t′ = subst (subst t ref (func₁ proj₁ (cut τ t′ (ℰ e₃)))) ref₁ (func₁ (proj₁ ∘ proj₂) (cut τ t′ (ℰ e₃))) + subst t (Code.cut {t = τ} ref e₂) t′ = subst t ref (splice τ (func₁ proj₁ t′) (func₁ (proj₁ ∘ proj₂) t′) (ℰ e₂)) + subst t (Code.cast {t = τ} eq ref) t′ = subst t ref (cast τ (sym eq) t′) + subst t Code.nil t′ = t + subst t (Code.cons ref ref₁) t′ = subst (subst t ref (func₁ proj₁ t′)) ref₁ (func₁ proj₂ t′) + subst t (Code.head {e = e} ref) t′ = subst t ref (func₂ _,_ t′ (func₁ proj₂ (ℰ e))) + subst t (Code.tail {t = τ} {e = e} ref) t′ = subst t ref (func₂ {t₁ = τ} _,_ (func₁ proj₁ (ℰ e)) t′) diff --git a/src/Helium/Semantics/Denotational/Core.agda b/src/Helium/Semantics/Denotational/Core.agda index e605439..ec2a374 100644 --- a/src/Helium/Semantics/Denotational/Core.agda +++ b/src/Helium/Semantics/Denotational/Core.agda @@ -98,12 +98,12 @@ tupTail [] x = _ tupTail (_ ∷ _) (x , xs) = xs equal : ∀ {t} → HasEquality t → ⟦ t ⟧ₜ → ⟦ t ⟧ₜ → Bool -equal bool x y = does (x Bool.≟ y) -equal int x y = does (x ≟ᶻ y) -equal fin x y = does (x Fin.≟ y) -equal real x y = does (x ≟ʳ y) -equal bit x y = does (x ≟ᵇ₁ y) -equal bits x y = does (x ≟ᵇ y) +equal bool x y = does (x Bool.≟ y) +equal int x y = does (x ≟ᶻ y) +equal fin x y = does (x Fin.≟ y) +equal real x y = does (x ≟ʳ y) +equal bit x y = does (x ≟ᵇ₁ y) +equal (bits _) x y = does (x ≟ᵇ y) comp : ∀ {t} → IsNumeric t → ⟦ t ⟧ₜ → ⟦ t ⟧ₜ → Bool comp int x y = does (x <ᶻ? y) @@ -180,13 +180,13 @@ neg : ∀ {t} → IsNumeric t → ⟦ t ⟧ₜ → ⟦ t ⟧ₜ neg int x = ℤ.- x neg real x = ℝ.- x -add : ∀ {t₁ t₂} (isNum₁ : True (isNumeric? t₁)) (isNum₂ : True (isNumeric? t₂)) → ⟦ t₁ ⟧ₜ → ⟦ t₂ ⟧ₜ → ⟦ combineNumeric t₁ t₂ {isNum₁} {isNum₂} ⟧ₜ +add : ∀ {t₁ t₂} (isNum₁ : True (isNumeric? t₁)) (isNum₂ : True (isNumeric? t₂)) → ⟦ t₁ ⟧ₜ → ⟦ t₂ ⟧ₜ → ⟦ combineNumeric t₁ t₂ isNum₁ isNum₂ ⟧ₜ add {t₁ = int} {t₂ = int} _ _ x y = x ℤ.+ y add {t₁ = int} {t₂ = real} _ _ x y = x /1 ℝ.+ y add {t₁ = real} {t₂ = int} _ _ x y = x ℝ.+ y /1 add {t₁ = real} {t₂ = real} _ _ x y = x ℝ.+ y -mul : ∀ {t₁ t₂} (isNum₁ : True (isNumeric? t₁)) (isNum₂ : True (isNumeric? t₂)) → ⟦ t₁ ⟧ₜ → ⟦ t₂ ⟧ₜ → ⟦ combineNumeric t₁ t₂ {isNum₁} {isNum₂} ⟧ₜ +mul : ∀ {t₁ t₂} (isNum₁ : True (isNumeric? t₁)) (isNum₂ : True (isNumeric? t₂)) → ⟦ t₁ ⟧ₜ → ⟦ t₂ ⟧ₜ → ⟦ combineNumeric t₁ t₂ isNum₁ isNum₂ ⟧ₜ mul {t₁ = int} {t₂ = int} _ _ x y = x ℤ.* y mul {t₁ = int} {t₂ = real} _ _ x y = x /1 ℝ.* y mul {t₁ = real} {t₂ = int} _ _ x y = x ℝ.* y /1 |