diff options
Diffstat (limited to 'src/Helium')
| -rw-r--r-- | src/Helium/Data/Pseudocode/Core.agda | 117 | ||||
| -rw-r--r-- | src/Helium/Semantics/Axiomatic/Core.agda | 245 | ||||
| -rw-r--r-- | src/Helium/Semantics/Denotational/Core.agda | 79 |
3 files changed, 213 insertions, 228 deletions
diff --git a/src/Helium/Data/Pseudocode/Core.agda b/src/Helium/Data/Pseudocode/Core.agda index 0e85c0d..9f0c12d 100644 --- a/src/Helium/Data/Pseudocode/Core.agda +++ b/src/Helium/Data/Pseudocode/Core.agda @@ -9,7 +9,8 @@ module Helium.Data.Pseudocode.Core where open import Data.Bool using (Bool; true; false) -open import Data.Fin using (Fin; #_) +open import Data.Fin as Fin using (Fin) +open import Data.Fin.Patterns open import Data.Nat as ℕ using (ℕ; zero; suc) open import Data.Nat.Properties using (+-comm) open import Data.Product using (∃; _,_; proj₂; uncurry) @@ -130,53 +131,55 @@ module Code {o} (Σ : Vec Type o) where infix 4 _≟_ _<?_ data Expression {n} Γ where - lit : ∀ {t} → Literal t → Expression Γ t - state : ∀ i → Expression Γ (lookup Σ i) - var : ∀ i → Expression Γ (lookup Γ i) - abort : ∀ {t} → Expression Γ (fin 0) → Expression Γ t - _≟_ : ∀ {t} {hasEquality : True (hasEquality? t)} → Expression Γ t → Expression Γ t → Expression Γ bool - _<?_ : ∀ {t} {isNumeric : True (isNumeric? t)} → Expression Γ t → Expression Γ t → Expression Γ bool - inv : Expression Γ bool → Expression Γ bool - _&&_ : Expression Γ bool → Expression Γ bool → Expression Γ bool - _||_ : Expression Γ bool → Expression Γ bool → Expression Γ bool - 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 Γ (elemType t) → Expression Γ (asType t 1) - unbox : ∀ {t} → Expression Γ (asType t 1) → Expression Γ (elemType t) - _∶_ : ∀ {m n t} → Expression Γ (asType t m) → Expression Γ (asType t n) → Expression Γ (asType t (n ℕ.+ m)) - slice : ∀ {i j t} → Expression Γ (asType t (i ℕ.+ j)) → Expression Γ (fin (suc i)) → Expression Γ (asType t j) - 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₂}) + lit : ∀ {t} → Literal t → Expression Γ t + state : ∀ i → Expression Γ (lookup Σ i) + var : ∀ i → Expression Γ (lookup Γ i) + abort : ∀ {t} → Expression Γ (fin 0) → Expression Γ t + _≟_ : ∀ {t} {hasEquality : True (hasEquality? t)} → Expression Γ t → Expression Γ t → Expression Γ bool + _<?_ : ∀ {t} {isNumeric : True (isNumeric? t)} → Expression Γ t → Expression Γ t → Expression Γ bool + inv : Expression Γ bool → Expression Γ bool + _&&_ : Expression Γ bool → Expression Γ bool → Expression Γ bool + _||_ : Expression Γ bool → Expression Γ bool → Expression Γ bool + 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 Γ (elemType t) → Expression Γ (asType t 1) + unbox : ∀ {t} → Expression Γ (asType t 1) → Expression Γ (elemType t) + splice : ∀ {m n t} → Expression Γ (asType t m) → Expression Γ (asType t n) → Expression Γ (fin (suc n)) → Expression Γ (asType t (n ℕ.+ m)) + 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₂}) -- _/_ : Expression Γ real → Expression Γ real → Expression Γ real - _^_ : ∀ {t} {isNumeric : True (isNumeric? t)} → Expression Γ t → ℕ → Expression Γ t - _>>_ : Expression Γ int → ℕ → Expression Γ int - rnd : Expression Γ real → Expression Γ int - fin : ∀ {k ms n} → (All (Fin) ms → Fin n) → Expression Γ (tuple k (map fin ms)) → Expression Γ (fin n) - asInt : ∀ {m} → Expression Γ (fin m) → Expression Γ int - tup : ∀ {m ts} → All (Expression Γ) ts → Expression Γ (tuple m ts) - head : ∀ {m t ts} → Expression Γ (tuple (suc m) (t ∷ ts)) → Expression Γ t - tail : ∀ {m t ts} → Expression Γ (tuple (suc m) (t ∷ ts)) → Expression Γ (tuple m ts) - call : ∀ {t m Δ} → Function Δ t → All (Expression Γ) {m} Δ → Expression Γ t + _^_ : ∀ {t} {isNumeric : True (isNumeric? t)} → Expression Γ t → ℕ → Expression Γ t + _>>_ : Expression Γ int → ℕ → Expression Γ int + rnd : Expression Γ real → Expression Γ int + fin : ∀ {k ms n} → (All (Fin) ms → Fin n) → Expression Γ (tuple k (map fin ms)) → Expression Γ (fin n) + asInt : ∀ {m} → Expression Γ (fin m) → Expression Γ int + tup : ∀ {m ts} → All (Expression Γ) ts → Expression Γ (tuple m ts) + head : ∀ {m t ts} → Expression Γ (tuple (suc m) (t ∷ ts)) → Expression Γ t + tail : ∀ {m t ts} → Expression Γ (tuple (suc m) (t ∷ ts)) → Expression Γ (tuple m ts) + call : ∀ {t m Δ} → Function Δ t → All (Expression Γ) {m} Δ → Expression Γ t if_then_else_ : ∀ {t} → Expression Γ bool → Expression Γ t → Expression Γ t → Expression Γ t data CanAssign {n} {Γ} where state : ∀ i → CanAssign (state i) var : ∀ i → CanAssign (var i) - abort : ∀ {t} {e : Expression Γ (fin 0)} → CanAssign (abort {t = t} e) - _∶_ : ∀ {m n t} {e₁ : Expression Γ (asType t m)} {e₂ : Expression Γ (asType t n)} → CanAssign e₁ → CanAssign e₂ → CanAssign (e₁ ∶ e₂) - [_] : ∀ {t} {e : Expression Γ (elemType t)} → CanAssign e → CanAssign ([_] {t = t} e) - unbox : ∀ {t} {e : Expression Γ (asType t 1)} → CanAssign e → CanAssign (unbox e) - slice : ∀ {i j t} {e₁ : Expression Γ (asType t (i ℕ.+ j))} → CanAssign e₁ → (e₂ : Expression Γ (fin (suc i))) → CanAssign (slice e₁ e₂) - cast : ∀ {i j t} {e : Expression Γ (asType t i)} .(eq : i ≡ j) → CanAssign e → CanAssign (cast eq e) - tup : ∀ {m ts} {es : All (Expression Γ) {m} ts} → All (CanAssign ∘ proj₂) (reduce (λ {x} e → x , e) es) → CanAssign (tup es) + abort : ∀ {t} e → CanAssign (abort {t = t} e) + [_] : ∀ {t e} → CanAssign e → CanAssign ([_] {t = t} e) + unbox : ∀ {t e} → CanAssign e → CanAssign (unbox {t = t} e) + splice : ∀ {m n t e₁ e₂} → CanAssign e₁ → CanAssign e₂ → ∀ e₃ → CanAssign (splice {m = m} {n} {t} e₁ e₂ e₃) + cut : ∀ {m n t e₁} → CanAssign e₁ → ∀ e₂ → CanAssign (cut {m = m} {n} {t} e₁ e₂) + cast : ∀ {i j t e} .(eq : i ≡ j) → CanAssign e → CanAssign (cast {t = t} eq e) + tup : ∀ {m ts es} → All (CanAssign ∘ proj₂) (reduce (λ {x} e → x , e) es) → CanAssign (tup {m = m} {ts} es) + head : ∀ {m t ts e} → CanAssign e → CanAssign (head {m = m} {t} {ts} e) + tail : ∀ {m t ts e} → CanAssign e → CanAssign (tail {m = m} {t} {ts} e) canAssign? (lit x) = no λ () canAssign? (state i) = yes (state i) canAssign? (var i) = yes (var i) - canAssign? (abort e) = yes abort + canAssign? (abort e) = yes (abort e) canAssign? (e ≟ e₁) = no λ () canAssign? (e <? e₁) = no λ () canAssign? (inv e) = no λ () @@ -187,8 +190,8 @@ module Code {o} (Σ : Vec Type o) where canAssign? (e or e₁) = no λ () canAssign? [ e ] = map′ [_] (λ { [ e ] → e }) (canAssign? e) canAssign? (unbox e) = map′ unbox (λ { (unbox e) → e }) (canAssign? e) - canAssign? (e ∶ e₁) = map′ (uncurry _∶_) (λ { (e ∶ e₁) → e , e₁ }) (canAssign? e ×-dec canAssign? e₁) - canAssign? (slice e e₁) = map′ (λ e → slice e e₁) (λ { (slice e e₁) → e }) (canAssign? e) + canAssign? (splice e e₁ e₂) = map′ (λ (e , e₁) → splice e e₁ e₂) (λ { (splice e e₁ _) → e , e₁ }) (canAssign? e ×-dec canAssign? e₁) + canAssign? (cut e e₁) = map′ (λ e → cut e e₁) (λ { (cut e e₁) → e }) (canAssign? e) canAssign? (cast eq e) = map′ (cast eq) (λ { (cast eq e) → e }) (canAssign? e) canAssign? (- e) = no λ () canAssign? (e + e₁) = no λ () @@ -200,8 +203,8 @@ module Code {o} (Σ : Vec Type o) where canAssign? (fin x e) = no λ () canAssign? (asInt e) = no λ () canAssign? (tup es) = map′ tup (λ { (tup es) → es }) (canAssignAll? es) - canAssign? (head e) = no λ () - canAssign? (tail e) = no λ () + canAssign? (head e) = map′ head (λ { (head e) → e }) (canAssign? e) + canAssign? (tail e) = map′ tail (λ { (tail e) → e }) (canAssign? e) canAssign? (call x e) = no λ () canAssign? (if e then e₁ else e₂) = no λ () @@ -210,23 +213,27 @@ module Code {o} (Σ : Vec Type o) where data AssignsState where state : ∀ i → AssignsState (state i) - _∶ˡ_ : ∀ {m n t e₁ e₂ a₁} → AssignsState a₁ → ∀ a₂ → AssignsState (_∶_ {m = m} {n} {t} {e₁} {e₂} a₁ a₂) - _∶ʳ_ : ∀ {m n t e₁ e₂} a₁ {a₂} → AssignsState a₂ → AssignsState (_∶_ {m = m} {n} {t} {e₁} {e₂} a₁ a₂) [_] : ∀ {t e a} → AssignsState a → AssignsState ([_] {t = t} {e} a) unbox : ∀ {t e a} → AssignsState a → AssignsState (unbox {t = t} {e} a) - slice : ∀ {i j t e₁ a} → AssignsState a → ∀ e₂ → AssignsState (slice {i = i} {j} {t} {e₁} a e₂) + spliceˡ : ∀ {m n t e₁ e₂ a₁} → AssignsState a₁ → ∀ a₂ e₃ → AssignsState (splice {m = m} {n} {t} {e₁} {e₂} a₁ a₂ e₃) + spliceʳ : ∀ {m n t e₁ e₂} a₁ {a₂} → AssignsState a₂ → ∀ e₃ → AssignsState (splice {m = m} {n} {t} {e₁} {e₂} a₁ a₂ e₃) + cut : ∀ {m n t e₁ a₁} → AssignsState a₁ → ∀ e₂ → AssignsState (cut {m = m} {n} {t} {e₁} a₁ e₂) cast : ∀ {i j t e} .(eq : i ≡ j) {a} → AssignsState a → AssignsState (cast {t = t} {e} eq a) tup : ∀ {m ts es as} → Any (AssignsState ∘ proj₂) (reduce (λ {x} a → x , a) as) → AssignsState (tup {m = m} {ts} {es} as) + head : ∀ {m t ts e a} → AssignsState a → AssignsState (head {m = m} {t} {ts} {e} a) + tail : ∀ {m t ts e a} → AssignsState a → AssignsState (tail {m = m} {t} {ts} {e} a) assignsState? (state i) = yes (state i) assignsState? (var i) = no λ () - assignsState? abort = no λ () - assignsState? (a ∶ a₁) = map′ [ (_∶ˡ a₁) , (a ∶ʳ_) ]′ (λ { (s ∶ˡ _) → inj₁ s ; (_ ∶ʳ s) → inj₂ s }) (assignsState? a ⊎-dec assignsState? a₁) + assignsState? (abort e) = no λ () assignsState? [ a ] = map′ [_] (λ { [ s ] → s }) (assignsState? a) assignsState? (unbox a) = map′ unbox (λ { (unbox s) → s }) (assignsState? a) - assignsState? (slice a e₂) = map′ (λ s → slice s e₂ ) (λ { (slice s _) → s }) (assignsState? a) + assignsState? (splice a₁ a₂ e₃) = map′ [ (λ a₁ → spliceˡ a₁ a₂ e₃) , (λ a₂ → spliceʳ a₁ a₂ e₃) ]′ (λ { (spliceˡ a₁ _ _) → inj₁ a₁ ; (spliceʳ _ a₂ _) → inj₂ a₂ }) (assignsState? a₁ ⊎-dec assignsState? a₂) + assignsState? (cut a e₂) = map′ (λ s → cut s e₂ ) (λ { (cut s _) → s }) (assignsState? a) assignsState? (cast eq a) = map′ (cast eq) (λ { (cast _ s) → s }) (assignsState? a) assignsState? (tup as) = map′ tup (λ { (tup ss) → ss }) (assignsStateAny? as) + assignsState? (head a) = map′ head (λ { (head s) → s }) (assignsState? a) + assignsState? (tail a) = map′ tail (λ { (tail s) → s }) (assignsState? a) assignsStateAny? {es = []} [] = no λ () assignsStateAny? {es = e ∷ es} (a ∷ as) = map′ [ here , there ]′ (λ { (here s) → inj₁ s ; (there ss) → inj₂ ss }) (assignsState? a ⊎-dec assignsStateAny? as) @@ -273,6 +280,12 @@ module Code {o} (Σ : Vec Type o) where infixl 6 _<<_ infixl 5 _-_ + _∶_ : ∀ {n Γ i j t} → Expression {n} Γ (asType t j) → Expression Γ (asType t i) → Expression Γ (asType t (i ℕ.+ j)) + e₁ ∶ e₂ = splice e₁ e₂ (lit (Fin.fromℕ _ ′f)) + + slice : ∀ {n Γ i j t} → Expression {n} Γ (asType t (i ℕ.+ j)) → Expression Γ (fin (suc i)) → Expression Γ (asType t j) + slice e₁ e₂ = head (cut e₁ e₂) + 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₂ @@ -288,8 +301,8 @@ module Code {o} (Σ : Vec Type o) where uint : ∀ {n Γ m} → Expression {n} Γ (bits m) → Expression Γ int uint {m = zero} x = lit (0 ′i) uint {m = suc m} x = - lit (2 ′i) * uint {m = m} (slice x (lit ((# 1) ′f))) + - ( if slice′ x (lit ((# 0) ′f)) ≟ lit ((true ∷ []) ′xs) + lit (2 ′i) * uint {m = m} (slice x (lit (1F ′f))) + + ( if slice′ x (lit (0F ′f)) ≟ lit ((true ∷ []) ′xs) then lit (1 ′i) else lit (0 ′i)) @@ -297,7 +310,7 @@ module Code {o} (Σ : Vec Type o) where sint {m = zero} x = lit (0 ′i) sint {m = suc zero} x = if x ≟ lit ((true ∷ []) ′xs) then - lit (1 ′i) else lit (0 ′i) sint {m = suc (suc m)} x = - lit (2 ′i) * sint (slice {i = 1} x (lit ((# 1) ′f))) + - ( if slice′ x (lit ((# 0) ′f)) ≟ lit ((true ∷ []) ′xs) + lit (2 ′i) * sint (slice {i = 1} x (lit (1F ′f))) + + ( if slice′ x (lit (0F ′f)) ≟ lit ((true ∷ []) ′xs) then lit (1 ′i) else lit (0 ′i)) diff --git a/src/Helium/Semantics/Axiomatic/Core.agda b/src/Helium/Semantics/Axiomatic/Core.agda index 92c67bb..176dbdd 100644 --- a/src/Helium/Semantics/Axiomatic/Core.agda +++ b/src/Helium/Semantics/Axiomatic/Core.agda @@ -16,153 +16,108 @@ module Helium.Semantics.Axiomatic.Core private open module C = RawPseudocode rawPseudocode -open import Data.Bool using (Bool; T) -open import Data.Fin as Fin using (zero; suc) -import Data.Fin.Properties as Finₚ --- open import Data.Nat as ℕ using (zero; suc) -import Data.Nat as ℕ +open import Data.Bool as Bool using (Bool) +open import Data.Fin as Fin using (Fin; zero; suc) +open import Data.Fin.Patterns +open import Data.Nat as ℕ using (ℕ; suc) +import Data.Nat.Induction as Natᵢ import Data.Nat.Properties as ℕₚ -open import Data.Product using (∃; _×_; _,_; <_,_>) +open import Data.Product as × using (_,_; uncurry) open import Data.Sum using (_⊎_) open import Data.Unit using (⊤) -open import Data.Vec using (Vec; _∷_; lookup) +open import Data.Vec as Vec using (Vec; []; _∷_; _++_; lookup) open import Data.Vec.Relation.Unary.All as All using (All; []; _∷_) -open import Function using (_$_) +open import Function using (_on_) open import Helium.Data.Pseudocode.Core -open import Helium.Semantics.Core rawPseudocode -open import Level using (_⊔_; Lift) -open import Relation.Binary.PropositionalEquality using (refl) -open import Relation.Nullary using (yes; no) -open import Relation.Unary using (Decidable; _⊆_) - -module _ {o} (Σ : Vec Type o) {n} (Γ : Vec Type n) where - data Term {m} (Δ : Vec Type m) : Type → Set (b₁ ⊔ i₁ ⊔ r₁) where - state : ∀ i → Term Δ (lookup Σ i) - var : ∀ i → Term Δ (lookup Γ i) - meta : ∀ i → Term Δ (lookup Δ i) - funct : ∀ {m ts t} → (⟦ tuple m ts ⟧ₜˡ → ⟦ t ⟧ₜˡ) → All (Term Δ) ts → Term Δ t - - infixl 7 _⇒_ - infixl 6 _∧_ - infixl 5 _∨_ - - data Assertion {m} (Δ : Vec Type m) : Set (b₁ ⊔ i₁ ⊔ r₁) where - _∧_ : Assertion Δ → Assertion Δ → Assertion Δ - _∨_ : Assertion Δ → Assertion Δ → Assertion Δ - _⇒_ : Assertion Δ → Assertion Δ → Assertion Δ - all : ∀ {t} → Assertion (t ∷ Δ) → Assertion Δ - some : ∀ {t} → Assertion (t ∷ Δ) → Assertion Δ - pred : ∀ {m ts} → (⟦ tuple m ts ⟧ₜˡ → Bool) → All (Term Δ) ts → Assertion Δ - -module _ {o} {Σ : Vec Type o} {n} {Γ : Vec Type n} {m} {Δ : Vec Type m} where - ⟦_⟧ : ∀ {t} → Term Σ Γ Δ t → ⟦ Σ ⟧ₜˡ′ → ⟦ Γ ⟧ₜˡ′ → ⟦ Δ ⟧ₜˡ′ → ⟦ t ⟧ₜˡ - ⟦_⟧′ : ∀ {n ts} → All (Term Σ Γ Δ) ts → ⟦ Σ ⟧ₜˡ′ → ⟦ Γ ⟧ₜˡ′ → ⟦ Δ ⟧ₜˡ′ → ⟦ tuple n ts ⟧ₜˡ - ⟦ state i ⟧ σ γ δ = fetchˡ Σ σ i - ⟦ var i ⟧ σ γ δ = fetchˡ Γ γ i - ⟦ meta i ⟧ σ γ δ = fetchˡ Δ δ i - ⟦ funct f ts ⟧ σ γ δ = f (⟦ ts ⟧′ σ γ δ) - - ⟦ [] ⟧′ σ γ δ = _ - ⟦ (t ∷ []) ⟧′ σ γ δ = ⟦ t ⟧ σ γ δ - ⟦ (t ∷ t′ ∷ ts) ⟧′ σ γ δ = ⟦ t ⟧ σ γ δ , ⟦ t′ ∷ ts ⟧′ σ γ δ - - termSubstState : ∀ {t} → Term Σ Γ Δ t → ∀ j → Term Σ Γ Δ (lookup Σ j) → Term Σ Γ Δ t - termSubstState (state i) j t′ with j Fin.≟ i - ... | yes refl = t′ - ... | no _ = state i - termSubstState (var i) j t′ = var i - termSubstState (meta i) j t′ = meta i - termSubstState (funct f ts) j t′ = funct f (helper ts) - where - helper : ∀ {n ts} → All (Term Σ Γ Δ) {n} ts → All (Term Σ Γ Δ) ts - helper [] = [] - helper (t ∷ ts) = termSubstState t j t′ ∷ helper ts - - termSubstVar : ∀ {t} → Term Σ Γ Δ t → ∀ j → Term Σ Γ Δ (lookup Γ j) → Term Σ Γ Δ t - termSubstVar (state i) j t′ = state i - termSubstVar (var i) j t′ with j Fin.≟ i - ... | yes refl = t′ - ... | no _ = var i - termSubstVar (meta i) j t′ = meta i - termSubstVar (funct f ts) j t′ = funct f (helper ts) - where - helper : ∀ {n ts} → All (Term Σ Γ Δ) {n} ts → All (Term Σ Γ Δ) ts - helper [] = [] - helper (t ∷ ts) = termSubstVar t j t′ ∷ helper ts - - termElimVar : ∀ {t t′} → Term Σ (t′ ∷ Γ) Δ t → Term Σ Γ Δ t′ → Term Σ Γ Δ t - termElimVar (state i) t′ = state i - termElimVar (var zero) t′ = t′ - termElimVar (var (suc i)) t′ = var i - termElimVar (meta i) t′ = meta i - termElimVar (funct f ts) t′ = funct f (helper ts) - where - helper : ∀ {n ts} → All (Term _ _ _) {n} ts → All (Term _ _ _) ts - helper [] = [] - helper (t ∷ ts) = termElimVar t t′ ∷ helper ts - - termWknVar : ∀ {t t′} → Term Σ Γ Δ t → Term Σ (t′ ∷ Γ) Δ t - termWknVar (state i) = state i - termWknVar (var i) = var (suc i) - termWknVar (meta i) = meta i - termWknVar (funct f ts) = funct f (helper ts) - where - helper : ∀ {n ts} → All (Term _ _ _) {n} ts → All (Term _ _ _) ts - helper [] = [] - helper (t ∷ ts) = termWknVar t ∷ helper ts - - termWknMeta : ∀ {t t′} → Term Σ Γ Δ t → Term Σ Γ (t′ ∷ Δ) t - termWknMeta (state i) = state i - termWknMeta (var i) = var i - termWknMeta (meta i) = meta (suc i) - termWknMeta (funct f ts) = funct f (helper ts) - where - helper : ∀ {n ts} → All (Term _ _ _) {n} ts → All (Term _ _ _) ts - helper [] = [] - helper (t ∷ ts) = termWknMeta t ∷ helper ts - -module _ {o} {Σ : Vec Type o} {n} {Γ : Vec Type n} where - infix 4 _∋[_] _⊨_ - - _∋[_] : ∀ {m Δ} → Assertion Σ Γ {m} Δ → ⟦ Σ ⟧ₜˡ′ × ⟦ Γ ⟧ₜˡ′ × ⟦ Δ ⟧ₜˡ′ → Set (b₁ ⊔ i₁ ⊔ r₁) - P ∧ Q ∋[ s ] = P ∋[ s ] × Q ∋[ s ] - P ∨ Q ∋[ s ] = P ∋[ s ] ⊎ Q ∋[ s ] - P ⇒ Q ∋[ s ] = P ∋[ s ] → Q ∋[ s ] - pred P ts ∋[ σ , γ , δ ] = Lift (b₁ ⊔ i₁ ⊔ r₁) $ T $ P (⟦ ts ⟧′ σ γ δ) - _∋[_] {Δ = Δ} (all P) (σ , γ , δ) = ∀ v → P ∋[ σ , γ , consˡ Δ v δ ] - _∋[_] {Δ = Δ} (some P) (σ , γ , δ) = ∃ λ v → P ∋[ σ , γ , consˡ Δ v δ ] - - _⊨_ : ∀ {m Δ} → ⟦ Σ ⟧ₜˡ′ × ⟦ Γ ⟧ₜˡ′ × ⟦ Δ ⟧ₜˡ′ → Assertion Σ Γ {m} Δ → Set (b₁ ⊔ i₁ ⊔ r₁) - s ⊨ P = P ∋[ s ] - - asstSubstState : ∀ {m Δ} → Assertion Σ Γ {m} Δ → ∀ j → Term Σ Γ Δ (lookup Σ j) → Assertion Σ Γ Δ - asstSubstState (P ∧ Q) j t = asstSubstState P j t ∧ asstSubstState Q j t - asstSubstState (P ∨ Q) j t = asstSubstState P j t ∨ asstSubstState Q j t - asstSubstState (P ⇒ Q) j t = asstSubstState P j t ⇒ asstSubstState Q j t - asstSubstState (all P) j t = all (asstSubstState P j (termWknMeta t)) - asstSubstState (some P) j t = some (asstSubstState P j (termWknMeta t)) - asstSubstState (pred p ts) j t = pred p (All.map (λ t′ → termSubstState t′ j t) ts) - - asstSubstVar : ∀ {m Δ} → Assertion Σ Γ {m} Δ → ∀ j → Term Σ Γ Δ (lookup Γ j) → Assertion Σ Γ Δ - asstSubstVar (P ∧ Q) j t = asstSubstVar P j t ∧ asstSubstVar Q j t - asstSubstVar (P ∨ Q) j t = asstSubstVar P j t ∨ asstSubstVar Q j t - asstSubstVar (P ⇒ Q) j t = asstSubstVar P j t ⇒ asstSubstVar Q j t - asstSubstVar (all P) j t = all (asstSubstVar P j (termWknMeta t)) - asstSubstVar (some P) j t = some (asstSubstVar P j (termWknMeta t)) - asstSubstVar (pred p ts) j t = pred p (All.map (λ t′ → termSubstVar t′ j t) ts) - - asstElimVar : ∀ {m Δ t′} → Assertion Σ (t′ ∷ Γ) {m} Δ → Term Σ Γ Δ t′ → Assertion Σ Γ Δ - asstElimVar (P ∧ Q) t = asstElimVar P t ∧ asstElimVar Q t - asstElimVar (P ∨ Q) t = asstElimVar P t ∨ asstElimVar Q t - asstElimVar (P ⇒ Q) t = asstElimVar P t ⇒ asstElimVar Q t - asstElimVar (all P) t = all (asstElimVar P (termWknMeta t)) - asstElimVar (some P) t = some (asstElimVar P (termWknMeta t)) - asstElimVar (pred p ts) t = pred p (All.map (λ t′ → termElimVar t′ t) ts) - -module _ {o} {Σ : Vec Type o} where - open Code Σ - - data HoareTriple {n Γ m Δ} : Assertion Σ {n} Γ {m} Δ → Statement Γ → Assertion Σ Γ Δ → Set (b₁ ⊔ i₁ ⊔ r₁) where - csqs : ∀ {P₁ P₂ Q₁ Q₂ : Assertion Σ Γ Δ} {s} → (_⊨ P₁) ⊆ (_⊨ P₂) → HoareTriple P₂ s Q₂ → (_⊨ Q₂) ⊆ (_⊨ Q₁) → HoareTriple P₁ s Q₁ - _∙_ : ∀ {P Q R s₁ s₂} → HoareTriple P s₁ Q → HoareTriple Q s₂ R → HoareTriple P (s₁ ∙ s₂) R - skip : ∀ {P} → HoareTriple P skip P +open import Helium.Data.Pseudocode.Properties +import Induction.WellFounded as Wf +open import Level using (_⊔_; Lift; lift) +import Relation.Binary.Construct.On as On +open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; cong₂) +open import Relation.Nullary using (Dec; does; yes; no) +open import Relation.Nullary.Decidable.Core using (True; toWitness; map′) +open import Relation.Nullary.Product using (_×-dec_) +open import Relation.Unary using (_⊆_) + +private + variable + t t′ : Type + m n : ℕ + Γ Δ Σ ts : Vec Type m + +sizeOf : Type → Sliced → ℕ +sizeOf bool s = 0 +sizeOf int s = 0 +sizeOf (fin n) s = 0 +sizeOf real s = 0 +sizeOf bit s = 0 +sizeOf (bits n) s = Bool.if does (s ≟ˢ bits) then n else 0 +sizeOf (tuple _ []) s = 0 +sizeOf (tuple _ (t ∷ ts)) s = sizeOf t s ℕ.+ sizeOf (tuple _ ts) s +sizeOf (array t n) s = Bool.if does (s ≟ˢ array t) then n else sizeOf t s + +allocateSpace : Vec Type n → Sliced → ℕ +allocateSpace [] s = 0 +allocateSpace (t ∷ ts) s = sizeOf t s ℕ.+ allocateSpace ts s + +private + getSliced : ∀ {t} → True (sliced? t) → Sliced + getSliced t = ×.proj₁ (toWitness t) + + getCount : ∀ {t} → True (sliced? t) → ℕ + getCount t = ×.proj₁ (×.proj₂ (toWitness t)) + +data ⟦_；_⟧ₜ (counts : Sliced → ℕ) : (τ : Type) → Set (b₁ ⊔ i₁ ⊔ r₁) where + bool : Bool → ⟦ counts ； bool ⟧ₜ + int : ℤ → ⟦ counts ； int ⟧ₜ + fin : ∀ {n} → Fin n → ⟦ counts ； fin n ⟧ₜ + real : ℝ → ⟦ counts ； real ⟧ₜ + bit : Bit → ⟦ counts ； bit ⟧ₜ + bits : ∀ {n} → Vec (⟦ counts ； bit ⟧ₜ ⊎ Fin (counts bits)) n → ⟦ counts ； bits n ⟧ₜ + array : ∀ {t n} → Vec (⟦ counts ； t ⟧ₜ ⊎ Fin (counts (array t))) n → ⟦ counts ； array t n ⟧ₜ + tuple : ∀ {n ts} → All ⟦ counts ；_⟧ₜ ts → ⟦ counts ； tuple n ts ⟧ₜ + +Stack : (counts : Sliced → ℕ) → Vec Type n → Set (b₁ ⊔ i₁ ⊔ r₁) +Stack counts Γ = ⟦ counts ； tuple _ Γ ⟧ₜ + +Heap : (counts : Sliced → ℕ) → Set (b₁ ⊔ i₁ ⊔ r₁) +Heap counts = ∀ t → Vec ⟦ counts ； elemType t ⟧ₜ (counts t) + +record State (Γ : Vec Type n) : Set (b₁ ⊔ i₁ ⊔ r₁) where + private + counts = allocateSpace Γ + field + stack : Stack counts Γ + heap : Heap counts + +Transform : Vec Type m → Type → Set (b₁ ⊔ i₁ ⊔ r₁) +Transform ts t = ∀ counts → Heap counts → ⟦ counts ； tuple _ ts ⟧ₜ → ⟦ counts ； t ⟧ₜ + +Predicate : Vec Type m → Set (b₁ ⊔ i₁ ⊔ r₁) +Predicate ts = ∀ counts → ⟦ counts ； tuple _ ts ⟧ₜ → Bool + +-- -- ⟦_⟧ₐ : ∀ {m Δ} → Assertion Σ Γ {m} Δ → State (Σ ++ Γ ++ Δ) → Set (b₁ ⊔ i₁ ⊔ r₁) +-- -- ⟦_⟧ₐ = {!!} + +-- -- module _ {o} {Σ : Vec Type o} where +-- -- open Code Σ + +-- -- 𝒦 : ∀ {n Γ m Δ t} → Literal t → Term Σ {n} Γ {m} Δ t +-- -- 𝒦 = {!!} + +-- -- ℰ : ∀ {n Γ m Δ t} → Expression {n} Γ t → Term Σ Γ {m} Δ t +-- -- ℰ = {!!} + +-- -- data HoareTriple {n Γ m Δ} : Assertion Σ {n} Γ {m} Δ → Statement Γ → Assertion Σ Γ Δ → Set (b₁ ⊔ i₁ ⊔ r₁) where +-- -- _∙_ : ∀ {P Q R s₁ s₂} → HoareTriple P s₁ Q → HoareTriple Q s₂ R → HoareTriple P (s₁ ∙ s₂) R +-- -- skip : ∀ {P} → HoareTriple P skip P + +-- -- assign : ∀ {P t ref canAssign e} → HoareTriple (asrtSubst P (toWitness canAssign) (ℰ e)) (_≔_ {t = t} ref {canAssign} e) P +-- -- declare : ∀ {t P Q e s} → HoareTriple (P ∧ equal (var 0F) (termWknVar (ℰ e))) s (asrtWknVar Q) → HoareTriple (asrtElimVar P (ℰ e)) (declare {t = t} e s) Q +-- -- invoke : ∀ {m ts P Q s e} → HoareTriple (assignMetas Δ ts (All.tabulate var) (asrtAddVars P)) s (asrtAddVars Q) → HoareTriple (assignMetas Δ ts (All.tabulate (λ i → ℰ (All.lookup i e))) (asrtAddVars P)) (invoke {m = m} {ts} (s ∙end) e) (asrtAddVars Q) +-- -- if : ∀ {P Q e s₁ s₂} → HoareTriple (P ∧ equal (ℰ e) (𝒦 (Bool.true ′b))) s₁ Q → HoareTriple (P ∧ equal (ℰ e) (𝒦 (Bool.false ′b))) s₂ Q → HoareTriple P (if e then s₁ else s₂) Q +-- -- for : ∀ {m} {I : Assertion Σ Γ (fin (suc m) ∷ Δ)} {s} → HoareTriple (some (asrtWknVar (asrtWknMetaAt 1F I) ∧ equal (meta 1F) (var 0F) ∧ equal (meta 0F) (func (λ { _ (lift x ∷ []) → lift (Fin.inject₁ x) }) (meta 1F ∷ [])))) s (some (asrtWknVar (asrtWknMetaAt 1F I) ∧ equal (meta 0F) (func (λ { _ (lift x ∷ []) → lift (Fin.suc x) }) (meta 1F ∷ [])))) → HoareTriple (some (I ∧ equal (meta 0F) (func (λ _ _ → lift 0F) []))) (for m s) (some (I ∧ equal (meta 0F) (func (λ _ _ → lift (Fin.fromℕ m)) []))) + +-- -- consequence : ∀ {P₁ P₂ Q₁ Q₂ s} → ⟦ P₁ ⟧ₐ ⊆ ⟦ P₂ ⟧ₐ → HoareTriple P₂ s Q₂ → ⟦ Q₂ ⟧ₐ ⊆ ⟦ Q₁ ⟧ₐ → HoareTriple P₁ s Q₁ +-- -- some : ∀ {t P Q s} → HoareTriple P s Q → HoareTriple (some {t = t} P) s (some Q) +-- -- frame : ∀ {P Q R s} → HoareTriple P s Q → HoareTriple (P * R) s (Q * R) diff --git a/src/Helium/Semantics/Denotational/Core.agda b/src/Helium/Semantics/Denotational/Core.agda index 474a60f..ff5a56d 100644 --- a/src/Helium/Semantics/Denotational/Core.agda +++ b/src/Helium/Semantics/Denotational/Core.agda @@ -111,8 +111,8 @@ comp real x y = does (x <ʳ? y) -- 0 of y is 0 of result join : ∀ t {m n} → ⟦ asType t m ⟧ₜ → ⟦ asType t n ⟧ₜ → ⟦ asType t (n ℕ.+ m) ⟧ₜ -join bits {m} x y = y VecF.++ x -join (array _) {m} x y = y Vec.++ x +join bits x y = y VecF.++ x +join (array _) x y = y Vec.++ x -- take from 0 take : ∀ t i {j} → ⟦ asType t (i ℕ.+ j) ⟧ₜ → ⟦ asType t i ⟧ₜ @@ -134,26 +134,39 @@ module _ where m≤n⇒m+k≡n ℕ.z≤n = _ , ≡.refl m≤n⇒m+k≡n (ℕ.s≤s m≤n) = P.dmap id (≡.cong suc) (m≤n⇒m+k≡n m≤n) - slicedSize : ∀ i j (off : Fin (suc i)) → P.∃ λ k → i ℕ.+ j ≡ Fin.toℕ off ℕ.+ (j ℕ.+ k) - slicedSize i j off = k , (begin - i ℕ.+ j ≡˘⟨ ≡.cong (ℕ._+ j) (P.proj₂ off+k≤i) ⟩ - (Fin.toℕ off ℕ.+ k) ℕ.+ j ≡⟨ ℕₚ.+-assoc (Fin.toℕ off) k j ⟩ - Fin.toℕ off ℕ.+ (k ℕ.+ j) ≡⟨ ≡.cong (Fin.toℕ off ℕ.+_) (ℕₚ.+-comm k j) ⟩ - Fin.toℕ off ℕ.+ (j ℕ.+ k) ∎) + slicedSize : ∀ n m (i : Fin (suc n)) → P.∃ λ k → n ℕ.+ m ≡ Fin.toℕ i ℕ.+ (m ℕ.+ k) × Fin.toℕ i ℕ.+ k ≡ n + slicedSize n m i = k , (begin + n ℕ.+ m ≡˘⟨ ≡.cong (ℕ._+ m) (P.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) ∎) , + P.proj₂ i+k≡n where open ≡-Reasoning - off+k≤i = m≤n⇒m+k≡n (ℕₚ.≤-pred (Finₚ.toℕ<n off)) - k = P.proj₁ off+k≤i + i+k≡n = m≤n⇒m+k≡n (ℕₚ.≤-pred (Finₚ.toℕ<n i)) + k = P.proj₁ i+k≡n - sliced : ∀ t {i j} → ⟦ asType t (i ℕ.+ j) ⟧ₜ → ⟦ fin (suc i) ⟧ₜ → ⟦ asType t j ⟧ₜ - sliced t {i} {j} x off = take t j (drop t (Fin.toℕ off) (casted t (P.proj₂ (slicedSize i j off)) x)) - -updateSliced : ∀ {a} {A : Set a} t {i j} → ⟦ asType t (i ℕ.+ j) ⟧ₜ → ⟦ fin (suc i) ⟧ₜ → ⟦ asType t j ⟧ₜ → (⟦ asType t (i ℕ.+ j) ⟧ₜ → A) → A -updateSliced t {i} {j} orig off v f = f (casted t (≡.sym eq) (join t (join t untaken v) dropped)) - where - eq = P.proj₂ (slicedSize i j off) - dropped = take t (Fin.toℕ off) (casted t eq orig) - untaken = drop t j (drop t (Fin.toℕ off) (casted t eq orig)) + -- 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 i = casted t eq (join t (join t high x) low) + where + reasoning = slicedSize _ m i + k = P.proj₁ reasoning + n≡i+k = ≡.sym (P.proj₂ (P.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 (P.proj₁ (P.proj₂ reasoning)) + + sliced : ∀ t {m n} → ⟦ asType t (n ℕ.+ m) ⟧ₜ → ⟦ fin (suc n) ⟧ₜ → ⟦ asType t m ∷ asType t n ∷ [] ⟧ₜ′ + sliced t {m} x i = middle , casted t i+k≡n (join t high low) + where + reasoning = slicedSize _ m i + k = P.proj₁ reasoning + i+k≡n = P.proj₂ (P.proj₂ reasoning) + eq = P.proj₁ (P.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)) box : ∀ t → ⟦ elemType t ⟧ₜ → ⟦ asType t 1 ⟧ₜ box bits v = v VecF.∷ VecF.[] @@ -214,8 +227,8 @@ module Expression ⟦ e or e₁ ⟧ᵉ σ γ = ⟦ e ⟧ᵉ σ γ Bits.∨ ⟦ e₁ ⟧ᵉ σ γ ⟦ [_] {t = t} e ⟧ᵉ σ γ = box t (⟦ e ⟧ᵉ σ γ) ⟦ unbox {t = t} e ⟧ᵉ σ γ = unboxed t (⟦ e ⟧ᵉ σ γ) - ⟦ _∶_ {t = t} e e₁ ⟧ᵉ σ γ = join t (⟦ e ⟧ᵉ σ γ) (⟦ e₁ ⟧ᵉ σ γ) - ⟦ slice {t = t} e e₁ ⟧ᵉ σ γ = sliced t (⟦ e ⟧ᵉ σ γ) (⟦ e₁ ⟧ᵉ σ γ) + ⟦ splice {t = t} e e₁ e₂ ⟧ᵉ σ γ = spliced t (⟦ e ⟧ᵉ σ γ) (⟦ e₁ ⟧ᵉ σ γ) (⟦ e₂ ⟧ᵉ σ γ) + ⟦ cut {t = t} e e₁ ⟧ᵉ σ γ = sliced t (⟦ e ⟧ᵉ σ γ) (⟦ e₁ ⟧ᵉ σ γ) ⟦ cast {t = t} eq e ⟧ᵉ σ γ = casted t eq (⟦ e ⟧ᵉ σ γ) ⟦ -_ {isNumeric = isNum} e ⟧ᵉ σ γ = neg (toWitness isNum) (⟦ e ⟧ᵉ σ γ) ⟦ _+_ {isNumeric₁ = isNum₁} {isNumeric₂ = isNum₂} e e₁ ⟧ᵉ σ γ = add isNum₁ isNum₂ (⟦ e ⟧ᵉ σ γ) (⟦ e₁ ⟧ᵉ σ γ) @@ -267,16 +280,20 @@ module Expression update (state i) v σ γ = updateAt Σ i v σ , γ update {Γ = Γ} (var i) v σ γ = σ , updateAt Γ i v γ - update abort v σ γ = σ , γ - update (_∶_ {m = m} {t = t} e e₁) v σ γ = do - let σ′ , γ′ = update e (sliced t v (Fin.fromℕ _)) σ γ - update e₁ (sliced t (casted t (ℕₚ.+-comm _ m) v) zero) σ′ γ′ + update (abort _) v σ γ = σ , γ update ([_] {t = t} e) v σ γ = update e (unboxed t v) σ γ update (unbox {t = t} e) v σ γ = update e (box t v) σ γ - update (slice {t = t} {e₁ = e₁} a e₂) v σ γ = updateSliced t (⟦ e₁ ⟧ᵉ σ γ) (⟦ e₂ ⟧ᵉ σ γ) v (λ v → update a v σ γ) + update (splice {m = m} {t = t} e e₁ e₂) v σ γ = do + let i = ⟦ e₂ ⟧ᵉ σ γ + let σ′ , γ′ = update e (P.proj₁ (sliced t v i)) σ γ + update e₁ (P.proj₂ (sliced t v i)) σ′ γ′ + update (cut {t = t} a e₂) v σ γ = do + let i = ⟦ e₂ ⟧ᵉ σ γ + update a (spliced t (P.proj₁ v) (P.proj₂ v) i) σ γ update (cast {t = t} eq e) v σ γ = update e (casted t (≡.sym eq) v) σ γ - update (tup {es = []} x) v σ γ = σ , γ - update (tup {es = _ ∷ []} (x ∷ [])) v σ γ = update x v σ γ - update (tup {es = _ ∷ _ ∷ _} (x ∷ xs)) (v , vs) σ γ = do - let σ′ , γ′ = update x v σ γ - update (tup xs) vs σ′ γ′ + update (tup {es = []} x) vs σ γ = σ , γ + update (tup {ts = _ ∷ ts} {es = _ ∷ _} (x ∷ xs)) vs σ γ = do + let σ′ , γ′ = update x (tupHead ts vs) σ γ + update (tup xs) (tupTail ts vs) σ′ γ′ + update (head {ts = ts} {e = e} a) v σ γ = update a (tupCons ts v (tupTail ts (⟦ e ⟧ᵉ σ γ))) σ γ + update (tail {ts = ts} {e = e} a) v σ γ = update a (tupCons ts (tupHead ts (⟦ e ⟧ᵉ σ γ)) v) σ γ |