diff options
Diffstat (limited to 'src/Helium')
| -rw-r--r-- | src/Helium/Data/Pseudocode/Core.agda | 33 | ||||
| -rw-r--r-- | src/Helium/Semantics/Denotational/Core.agda | 39 |
2 files changed, 32 insertions, 40 deletions
diff --git a/src/Helium/Data/Pseudocode/Core.agda b/src/Helium/Data/Pseudocode/Core.agda index a63cc39..a50fb84 100644 --- a/src/Helium/Data/Pseudocode/Core.agda +++ b/src/Helium/Data/Pseudocode/Core.agda @@ -24,7 +24,6 @@ open import Relation.Unary using (Decidable) --- The set of types and boolean properties of them data Type : Set where - unit : Type bool : Type int : Type fin : (n : ℕ) → Type @@ -44,7 +43,6 @@ data HasEquality : Type → Set where bits : ∀ {n} → HasEquality (bits n) hasEquality? : Decidable HasEquality -hasEquality? unit = no (λ ()) hasEquality? bool = yes bool hasEquality? int = yes int hasEquality? (fin n) = yes fin @@ -58,7 +56,6 @@ data IsNumeric : Type → Set where real : IsNumeric real isNumeric? : Decidable IsNumeric -isNumeric? unit = no (λ ()) isNumeric? bool = no (λ ()) isNumeric? int = yes int isNumeric? real = yes real @@ -101,7 +98,7 @@ module Code {o} (Σ : Vec Type o) where data CanAssign {n} {Γ} : ∀ {t} → Expression {n} Γ t → Set canAssign? : ∀ {n Γ t} → Decidable (CanAssign {n} {Γ} {t}) canAssignAll? : ∀ {n Γ m ts} → Decidable {A = All (Expression {n} Γ) {m} ts} (All (CanAssign ∘ proj₂) ∘ (reduce (λ {x} e → x , e))) - data Statement {n} (Γ : Vec Type n) (ret : Type) : Set + data Statement {n} (Γ : Vec Type n) : Set data Function {n} (Γ : Vec Type n) (ret : Type) : Set data Procedure {n} (Γ : Vec Type n) : Set @@ -122,9 +119,9 @@ module Code {o} (Σ : Vec Type o) where inv : Expression Γ bool → Expression Γ bool _&&_ : Expression Γ bool → Expression Γ bool → Expression Γ bool _||_ : Expression Γ bool → Expression Γ bool → Expression Γ bool - not : ∀ {n} → Expression Γ (bits n) → Expression Γ (bits n) - _and_ : ∀ {n} → Expression Γ (bits n) → Expression Γ (bits n) → Expression Γ (bits n) - _or_ : ∀ {n} → Expression Γ (bits n) → Expression Γ (bits n) → Expression Γ (bits n) + not : ∀ {m} → Expression Γ (bits m) → Expression Γ (bits m) + _and_ : ∀ {m} → Expression Γ (bits m) → Expression Γ (bits m) → Expression Γ (bits m) + _or_ : ∀ {m} → Expression Γ (bits m) → Expression Γ (bits m) → Expression Γ (bits m) [_] : ∀ {t} → Expression Γ t → Expression Γ (array t 1) unbox : ∀ {t} → Expression Γ (array t 1) → Expression Γ t _∶_ : ∀ {m n t} → Expression Γ (asType t m) → Expression Γ (asType t n) → Expression Γ (asType t (n ℕ.+ m)) @@ -139,7 +136,7 @@ module Code {o} (Σ : Vec Type o) where rnd : Expression Γ real → Expression Γ int -- get : ℕ → Expression Γ int → Expression Γ bit fin : ∀ {k ms n} → (All (Fin) ms → Fin n) → Expression Γ (tuple k (map fin ms)) → Expression Γ (fin n) - asInt : ∀ {n} → Expression Γ (fin n) → Expression Γ int + asInt : ∀ {m} → Expression Γ (fin m) → Expression Γ int tup : ∀ {m ts} → All (Expression Γ) ts → Expression Γ (tuple m ts) call : ∀ {t m Δ} → Function Δ t → Expression Γ (tuple m Δ) → Expression Γ t if_then_else_ : ∀ {t} → Expression Γ bool → Expression Γ t → Expression Γ t → Expression Γ t @@ -194,21 +191,21 @@ module Code {o} (Σ : Vec Type o) where infixl 1 _∙_ _∙return_ infix 1 _∙end - data Statement Γ ret where - _∙_ : Statement Γ ret → Statement Γ ret → Statement Γ ret - skip : Statement Γ ret - _≔_ : ∀ {t} → (ref : Expression Γ t) → {canAssign : True (canAssign? ref)}→ Expression Γ t → Statement Γ ret - declare : ∀ {t} → Expression Γ t → Statement (t ∷ Γ) ret → Statement Γ ret - invoke : ∀ {m Δ} → Procedure Δ → Expression Γ (tuple m Δ) → Statement Γ ret - if_then_else_ : Expression Γ bool → Statement Γ ret → Statement Γ ret → Statement Γ ret - for : ∀ m → Statement (fin m ∷ Γ) ret → Statement Γ ret + data Statement Γ where + _∙_ : Statement Γ → Statement Γ → Statement Γ + skip : Statement Γ + _≔_ : ∀ {t} → (ref : Expression Γ t) → {canAssign : True (canAssign? ref)}→ Expression Γ t → Statement Γ + declare : ∀ {t} → Expression Γ t → Statement (t ∷ Γ) → Statement Γ + invoke : ∀ {m Δ} → Procedure Δ → Expression Γ (tuple m Δ) → Statement Γ + if_then_else_ : Expression Γ bool → Statement Γ → Statement Γ → Statement Γ + for : ∀ m → Statement (fin m ∷ Γ) → Statement Γ data Function Γ ret where - _∙return_ : Statement Γ ret → Expression Γ ret → Function Γ ret + _∙return_ : Statement Γ → Expression Γ ret → Function Γ ret declare : ∀ {t} → Expression Γ t → Function (t ∷ Γ) ret → Function Γ ret data Procedure Γ where - _∙end : Statement Γ unit → Procedure Γ + _∙end : Statement Γ → Procedure Γ declare : ∀ {t} → Expression Γ t → Procedure (t ∷ Γ) → Procedure Γ infixl 6 _<<_ diff --git a/src/Helium/Semantics/Denotational/Core.agda b/src/Helium/Semantics/Denotational/Core.agda index 6dd76b0..a644adb 100644 --- a/src/Helium/Semantics/Denotational/Core.agda +++ b/src/Helium/Semantics/Denotational/Core.agda @@ -37,7 +37,6 @@ open import Relation.Nullary using (does) open import Relation.Nullary.Decidable.Core using (True; False; toWitness; fromWitness) ⟦_⟧ₗ : Type → Level -⟦ unit ⟧ₗ = 0ℓ ⟦ bool ⟧ₗ = 0ℓ ⟦ int ⟧ₗ = i₁ ⟦ fin n ⟧ₗ = 0ℓ @@ -53,7 +52,6 @@ open import Relation.Nullary.Decidable.Core using (True; False; toWitness; fromW ⟦_⟧ₜ : ∀ t → Set ⟦ t ⟧ₗ ⟦_⟧ₜ′ : ∀ {n} ts → Set ⟦ tuple n ts ⟧ₗ -⟦ unit ⟧ₜ = ⊤ ⟦ bool ⟧ₜ = Bool ⟦ int ⟧ₜ = ℤ ⟦ fin n ⟧ₜ = Fin n @@ -62,7 +60,7 @@ open import Relation.Nullary.Decidable.Core using (True; False; toWitness; fromW ⟦ tuple n ts ⟧ₜ = ⟦ ts ⟧ₜ′ ⟦ array t n ⟧ₜ = Vec ⟦ t ⟧ₜ n -⟦ [] ⟧ₜ′ = ⟦ unit ⟧ₜ +⟦ [] ⟧ₜ′ = ⊤ ⟦ t ∷ [] ⟧ₜ′ = ⟦ t ⟧ₜ ⟦ t ∷ t′ ∷ ts ⟧ₜ′ = ⟦ t ⟧ₜ × ⟦ t′ ∷ ts ⟧ₜ′ @@ -177,7 +175,7 @@ pow real x n = x ℝ′.^′ n shiftr : 2 ℝ′.×′ 1ℝ ℝ.≉ 0ℝ → ⟦ int ⟧ₜ → ℕ → ⟦ int ⟧ₜ shiftr 2≉0 x n = ⌊ x /1 ℝ.* 2≉0 ℝ.⁻¹ ℝ′.^′ n ⌋ -module _ +module Expression {o} {Σ : Vec Type o} (2≉0 : 2 ℝ′.×′ 1ℝ ℝ.≉ 0ℝ) where @@ -185,7 +183,7 @@ module _ open Code Σ ⟦_⟧ᵉ : ∀ {n} {Γ : Vec Type n} {t} → Expression Γ t → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ Σ ⟧ₜ′ × ⟦ t ⟧ₜ - ⟦_⟧ˢ : ∀ {n} {Γ : Vec Type n} {ret} → Statement Γ ret → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ Σ ⟧ₜ′ × (⟦ Γ ⟧ₜ′ ⊎ ⟦ ret ⟧ₜ) + ⟦_⟧ˢ : ∀ {n} {Γ : Vec Type n} → Statement Γ → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ Σ ⟧ₜ′ × ⟦ Γ ⟧ₜ′ ⟦_⟧ᶠ : ∀ {n} {Γ : Vec Type n} {ret} → Function Γ ret → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ Σ ⟧ₜ′ × ⟦ ret ⟧ₜ ⟦_⟧ᵖ : ∀ {n} {Γ : Vec Type n} → Procedure Γ → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ Σ ⟧ₜ′ update : ∀ {n Γ t e} → CanAssign {n} {Γ} {t} e → ⟦ t ⟧ₜ → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ Σ ⟧ₜ′ × ⟦ Γ ⟧ₜ′ @@ -261,39 +259,36 @@ module _ Bool.if x then ⟦ e₁ ⟧ᵉ σ′ γ else ⟦ e₂ ⟧ᵉ σ′ γ ⟦ s ∙ s₁ ⟧ˢ σ γ = do - let σ′ , v = ⟦ s ⟧ˢ σ γ - S.[ ⟦ s ⟧ˢ σ′ , (λ v → σ′ , ret v) ] v - ⟦ skip ⟧ˢ σ γ = σ , next γ + let σ′ , γ′ = ⟦ s ⟧ˢ σ γ + ⟦ s ⟧ˢ σ′ γ′ + ⟦ skip ⟧ˢ σ γ = σ , γ ⟦ _≔_ ref {canAssign = canAssign} e ⟧ˢ σ γ = do let σ′ , v = ⟦ e ⟧ᵉ σ γ - let σ′′ , γ′ = update (toWitness canAssign) v σ′ γ - σ′′ , next γ′ + update (toWitness canAssign) v σ′ γ ⟦_⟧ˢ {Γ = Γ} (declare e s) σ γ = do let σ′ , x = ⟦ e ⟧ᵉ σ γ - let σ′′ , v = ⟦ s ⟧ˢ σ′ (tupCons Γ x γ) - σ′′ , S.map₁ (tupTail Γ) v + let σ′′ , γ′ = ⟦ s ⟧ˢ σ′ (tupCons Γ x γ) + σ′′ , tupTail Γ γ′ ⟦ invoke p e ⟧ˢ σ γ = do let σ′ , v = ⟦ e ⟧ᵉ σ γ - ⟦ p ⟧ᵖ σ′ v , next γ + ⟦ p ⟧ᵖ σ′ v , γ ⟦ if e then s₁ else s₂ ⟧ˢ σ γ = do let σ′ , x = ⟦ e ⟧ᵉ σ γ Bool.if x then ⟦ s₁ ⟧ˢ σ′ γ else ⟦ s₂ ⟧ˢ σ′ γ - ⟦_⟧ˢ {Γ = Γ} {ret = t} (for m s) σ γ = helper m ⟦ s ⟧ˢ σ γ + ⟦_⟧ˢ {Γ = Γ} (for m s) σ γ = helper m ⟦ s ⟧ˢ σ γ where - helper : ∀ m → (⟦ Σ ⟧ₜ′ → ⟦ fin m ∷ Γ ⟧ₜ′ → ⟦ Σ ⟧ₜ′ × (⟦ fin m ∷ Γ ⟧ₜ′ ⊎ ⟦ t ⟧ₜ)) → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ Σ ⟧ₜ′ × (⟦ Γ ⟧ₜ′ ⊎ ⟦ t ⟧ₜ) - helper zero s σ γ = σ , next γ + helper : ∀ m → (⟦ Σ ⟧ₜ′ → ⟦ fin m ∷ Γ ⟧ₜ′ → ⟦ Σ ⟧ₜ′ × ⟦ fin m ∷ Γ ⟧ₜ′) → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ Σ ⟧ₜ′ × ⟦ Γ ⟧ₜ′ + helper zero s σ γ = σ , γ helper (suc m) s σ γ with s σ (tupCons Γ zero γ) - ... | σ′ , ret v = σ′ , ret v - ... | σ′ , next γ′ = helper m s′ σ′ (tupTail Γ γ′) + ... | σ′ , γ′ = helper m s′ σ′ (tupTail Γ γ′) where - s′ : ⟦ Σ ⟧ₜ′ → ⟦ fin m ∷ Γ ⟧ₜ′ → ⟦ Σ ⟧ₜ′ × (⟦ fin m ∷ Γ ⟧ₜ′ ⊎ ⟦ t ⟧ₜ) + s′ : ⟦ Σ ⟧ₜ′ → ⟦ fin m ∷ Γ ⟧ₜ′ → ⟦ Σ ⟧ₜ′ × ⟦ fin m ∷ Γ ⟧ₜ′ s′ σ γ = - P.map₂ (S.map₁ (tupCons Γ (tupHead Γ γ) ∘′ (tupTail Γ))) + P.map₂ (tupCons Γ (tupHead Γ γ) ∘′ (tupTail Γ)) (s σ (tupCons Γ (suc (tupHead Γ γ)) (tupTail Γ γ))) ⟦ s ∙return e ⟧ᶠ σ γ with ⟦ s ⟧ˢ σ γ - ... | σ′ , ret v = σ′ , v - ... | σ′ , next γ′ = ⟦ e ⟧ᵉ σ′ γ′ + ... | σ′ , γ′ = ⟦ e ⟧ᵉ σ′ γ′ ⟦_⟧ᶠ {Γ = Γ} (declare e f) σ γ = do let σ′ , x = ⟦ e ⟧ᵉ σ γ ⟦ f ⟧ᶠ σ′ (tupCons Γ x γ) |