diff options
Diffstat (limited to 'src/Helium/Semantics/Axiomatic/Assertion.agda')
| -rw-r--r-- | src/Helium/Semantics/Axiomatic/Assertion.agda | 247 |
1 files changed, 132 insertions, 115 deletions
diff --git a/src/Helium/Semantics/Axiomatic/Assertion.agda b/src/Helium/Semantics/Axiomatic/Assertion.agda index ab786e5..505abd8 100644 --- a/src/Helium/Semantics/Axiomatic/Assertion.agda +++ b/src/Helium/Semantics/Axiomatic/Assertion.agda @@ -15,115 +15,39 @@ module Helium.Semantics.Axiomatic.Assertion open RawPseudocode rawPseudocode -open import Data.Bool as Bool using (Bool) +import Data.Bool as Bool open import Data.Empty.Polymorphic using (⊥) -open import Data.Fin as Fin using (suc) +open import Data.Fin using (suc) open import Data.Fin.Patterns open import Data.Nat using (ℕ; suc) import Data.Nat.Properties as ℕₚ -open import Data.Product using (∃; _×_; _,_; proj₁; proj₂) +open import Data.Product using (∃; _×_; _,_; uncurry) open import Data.Sum using (_⊎_) open import Data.Unit.Polymorphic using (⊤) -open import Data.Vec as Vec using (Vec; []; _∷_; _++_) -open import Data.Vec.Relation.Unary.All as All using (All; []; _∷_) -open import Function using (_$_) +open import Data.Vec as Vec using (Vec; []; _∷_; _++_; insert) +open import Data.Vec.Relation.Unary.All using (All; map) +import Data.Vec.Recursive as Vecᵣ +open import Function open import Helium.Data.Pseudocode.Core -open import Helium.Semantics.Axiomatic.Core rawPseudocode +open import Helium.Semantics.Core rawPseudocode open import Helium.Semantics.Axiomatic.Term rawPseudocode as Term using (Term) -open import Level using (_⊔_; Lift; lift; lower) renaming (suc to ℓsuc) +open import Level as L using (Lift; lift; lower) private variable t t′ : Type - m n o : ℕ + i j k m n o : ℕ Γ Δ Σ ts : Vec Type m -open Term.Term + ℓ = b₁ L.⊔ i₁ L.⊔ r₁ -data Assertion (Σ : Vec Type o) (Γ : Vec Type n) (Δ : Vec Type m) : Set (ℓsuc (b₁ ⊔ i₁ ⊔ r₁)) +open Term.Term -data Assertion Σ Γ Δ where +data Assertion (Σ : Vec Type o) (Γ : Vec Type n) (Δ : Vec Type m) : Set (L.suc ℓ) where all : Assertion Σ Γ (t ∷ Δ) → Assertion Σ Γ Δ some : Assertion Σ Γ (t ∷ Δ) → Assertion Σ Γ Δ pred : Term Σ Γ Δ bool → Assertion Σ Γ Δ - comb : ∀ {n} → (Vec (Set (b₁ ⊔ i₁ ⊔ r₁)) n → Set (b₁ ⊔ i₁ ⊔ r₁)) → Vec (Assertion Σ Γ Δ) n → Assertion Σ Γ Δ - -substVars : Assertion Σ Γ Δ → All (Term Σ ts Δ) Γ → Assertion Σ ts Δ -substVars (all P) ts = all (substVars P (Term.wknMeta′ ts)) -substVars (some P) ts = some (substVars P (Term.wknMeta′ ts)) -substVars (pred p) ts = pred (Term.substVars p ts) -substVars (comb f Ps) ts = comb f (helper Ps ts) - where - helper : ∀ {n m ts} → Vec (Assertion Σ _ Δ) n → All (Term {n = m} Σ ts Δ) Γ → Vec (Assertion Σ ts Δ) n - helper [] ts = [] - helper (P ∷ Ps) ts = substVars P ts ∷ helper Ps ts - -elimVar : Assertion Σ (t ∷ Γ) Δ → Term Σ Γ Δ t → Assertion Σ Γ Δ -elimVar (all P) t = all (elimVar P (Term.wknMeta t)) -elimVar (some P) t = some (elimVar P (Term.wknMeta t)) -elimVar (pred p) t = pred (Term.elimVar p t) -elimVar (comb f Ps) t = comb f (helper Ps t) - where - helper : ∀ {n} → Vec (Assertion Σ (_ ∷ Γ) Δ) n → Term Σ Γ Δ _ → Vec (Assertion Σ Γ Δ) n - helper [] t = [] - helper (P ∷ Ps) t = elimVar P t ∷ helper Ps t - -wknVar : Assertion Σ Γ Δ → Assertion Σ (t ∷ Γ) Δ -wknVar (all P) = all (wknVar P) -wknVar (some P) = some (wknVar P) -wknVar (pred p) = pred (Term.wknVar p) -wknVar (comb f Ps) = comb f (helper Ps) - where - helper : ∀ {n} → Vec (Assertion Σ Γ Δ) n → Vec (Assertion Σ (_ ∷ Γ) Δ) n - helper [] = [] - helper (P ∷ Ps) = wknVar P ∷ helper Ps - -wknVars : (ts : Vec Type n) → Assertion Σ Γ Δ → Assertion Σ (ts ++ Γ) Δ -wknVars τs (all P) = all (wknVars τs P) -wknVars τs (some P) = some (wknVars τs P) -wknVars τs (pred p) = pred (Term.wknVars τs p) -wknVars τs (comb f Ps) = comb f (helper Ps) - where - helper : ∀ {n} → Vec (Assertion Σ Γ Δ) n → Vec (Assertion Σ (τs ++ Γ) Δ) n - helper [] = [] - helper (P ∷ Ps) = wknVars τs P ∷ helper Ps - -addVars : Assertion Σ [] Δ → Assertion Σ Γ Δ -addVars (all P) = all (addVars P) -addVars (some P) = some (addVars P) -addVars (pred p) = pred (Term.addVars p) -addVars (comb f Ps) = comb f (helper Ps) - where - helper : ∀ {n} → Vec (Assertion Σ [] Δ) n → Vec (Assertion Σ Γ Δ) n - helper [] = [] - helper (P ∷ Ps) = addVars P ∷ helper Ps - -wknMetaAt : ∀ i → Assertion Σ Γ Δ → Assertion Σ Γ (Vec.insert Δ i t) -wknMetaAt i (all P) = all (wknMetaAt (suc i) P) -wknMetaAt i (some P) = some (wknMetaAt (suc i) P) -wknMetaAt i (pred p) = pred (Term.wknMetaAt i p) -wknMetaAt i (comb f Ps) = comb f (helper i Ps) - where - helper : ∀ {n} i → Vec (Assertion Σ Γ Δ) n → Vec (Assertion Σ Γ (Vec.insert Δ i _)) n - helper i [] = [] - helper i (P ∷ Ps) = wknMetaAt i P ∷ helper i Ps - --- NOTE: better to induct on P instead of ts? -wknMetas : (ts : Vec Type n) → Assertion Σ Γ Δ → Assertion Σ Γ (ts ++ Δ) -wknMetas [] P = P -wknMetas (_ ∷ ts) P = wknMetaAt 0F (wknMetas ts P) - -module _ (2≉0 : Term.2≉0) where - -- NOTE: better to induct on e here than in Term? - subst : Assertion Σ Γ Δ → {e : Code.Expression Σ Γ t} → Code.CanAssign Σ e → Term Σ Γ Δ t → Assertion Σ Γ Δ - subst (all P) e t = all (subst P e (Term.wknMeta t)) - subst (some P) e t = some (subst P e (Term.wknMeta t)) - subst (pred p) e t = pred (Term.subst 2≉0 p e t) - subst (comb f Ps) e t = comb f (helper Ps e t) - where - helper : ∀ {t n} → Vec (Assertion Σ Γ Δ) n → {e : Code.Expression Σ Γ t} → Code.CanAssign Σ e → Term Σ Γ Δ t → Vec (Assertion Σ Γ Δ) n - helper [] e t = [] - helper (P ∷ Ps) e t = subst P e t ∷ helper Ps e t + comb : (Set ℓ Vecᵣ.^ k → Set ℓ) → Vec (Assertion Σ Γ Δ) k → Assertion Σ Γ Δ module Construct where infixl 6 _∧_ @@ -136,38 +60,131 @@ module Construct where false = comb (λ _ → ⊥) [] _∧_ : Assertion Σ Γ Δ → Assertion Σ Γ Δ → Assertion Σ Γ Δ - P ∧ Q = comb (λ { (P ∷ Q ∷ []) → P × Q }) (P ∷ Q ∷ []) + P ∧ Q = comb (uncurry _×_) (P ∷ Q ∷ []) _∨_ : Assertion Σ Γ Δ → Assertion Σ Γ Δ → Assertion Σ Γ Δ - P ∨ Q = comb (λ { (P ∷ Q ∷ []) → P ⊎ Q }) (P ∷ Q ∷ []) + P ∨ Q = comb (uncurry _⊎_) (P ∷ Q ∷ []) equal : Term Σ Γ Δ t → Term Σ Γ Δ t → Assertion Σ Γ Δ - equal {t = bool} x y = pred Term.[ bool ][ x ≟ y ] - equal {t = int} x y = pred Term.[ int ][ x ≟ y ] - equal {t = fin n} x y = pred Term.[ fin ][ x ≟ y ] - equal {t = real} x y = pred Term.[ real ][ x ≟ y ] - equal {t = bit} x y = pred Term.[ bit ][ x ≟ y ] - equal {t = bits n} x y = pred Term.[ bits ][ x ≟ y ] - equal {t = tuple _ []} x y = true - equal {t = tuple _ (t ∷ ts)} x y = equal {t = t} (Term.func₁ proj₁ x) (Term.func₁ proj₁ y) ∧ equal (Term.func₁ proj₂ x) (Term.func₁ proj₂ y) - equal {t = array t 0} x y = true - equal {t = array t (suc n)} x y = all (equal {t = t} (index x) (index y)) + equal {t = bool} x y = pred (x ≟ y) + equal {t = int} x y = pred (x ≟ y) + equal {t = fin n} x y = pred (x ≟ y) + equal {t = real} x y = pred (x ≟ y) + equal {t = bit} x y = pred (x ≟ y) + equal {t = tuple []} x y = true + equal {t = tuple (t ∷ [])} x y = equal (head x) (head y) + equal {t = tuple (t ∷ t₁ ∷ ts)} x y = equal (head x) (head y) ∧ equal (tail x) (tail y) + equal {t = array t 0} x y = true + equal {t = array t (suc n)} x y = all (equal (index x) (index y)) where - index = λ v → Term.unbox (array t) $ - Term.func₁ proj₁ $ - Term.cut (array t) - (Term.cast (array t) (ℕₚ.+-comm 1 n) (Term.wknMeta v)) - (meta 0F) + index : Term Σ Γ Δ (array t (suc n)) → Term Σ Γ (fin (suc n) ∷ Δ) t + index t = unbox (slice (cast (ℕₚ.+-comm 1 _) (Term.Meta.weaken 0F t)) (meta 0F)) open Construct public -⟦_⟧ : Assertion Σ Γ Δ → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ Δ ⟧ₜ′ → Set (b₁ ⊔ i₁ ⊔ r₁) -⟦_⟧′ : Vec (Assertion Σ Γ Δ) n → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ Δ ⟧ₜ′ → Vec (Set (b₁ ⊔ i₁ ⊔ r₁)) n +module Var where + weaken : ∀ i → Assertion Σ Γ Δ → Assertion Σ (insert Γ i t) Δ + weaken i (all P) = all (weaken i P) + weaken i (some P) = some (weaken i P) + weaken i (pred p) = pred (Term.Var.weaken i p) + weaken i (comb f Ps) = comb f (helper i Ps) + where + helper : ∀ i → Vec (Assertion Σ Γ Δ) k → Vec (Assertion Σ (insert Γ i t) Δ) k + helper i [] = [] + helper i (P ∷ Ps) = weaken i P ∷ helper i Ps + + weakenAll : Assertion Σ [] Δ → Assertion Σ Γ Δ + weakenAll (all P) = all (weakenAll P) + weakenAll (some P) = some (weakenAll P) + weakenAll (pred p) = pred (Term.Var.weakenAll p) + weakenAll (comb f Ps) = comb f (helper Ps) + where + helper : Vec (Assertion Σ [] Δ) k → Vec (Assertion Σ Γ Δ) k + helper [] = [] + helper (P ∷ Ps) = weakenAll P ∷ helper Ps + + inject : ∀ (ts : Vec Type n) → Assertion Σ Γ Δ → Assertion Σ (Γ ++ ts) Δ + inject ts (all P) = all (inject ts P) + inject ts (some P) = some (inject ts P) + inject ts (pred p) = pred (Term.Var.inject ts p) + inject ts (comb f Ps) = comb f (helper ts Ps) + where + helper : ∀ (ts : Vec Type n) → Vec (Assertion Σ Γ Δ) k → Vec (Assertion Σ (Γ ++ ts) Δ) k + helper ts [] = [] + helper ts (P ∷ Ps) = inject ts P ∷ helper ts Ps + + raise : ∀ (ts : Vec Type n) → Assertion Σ Γ Δ → Assertion Σ (ts ++ Γ) Δ + raise ts (all P) = all (raise ts P) + raise ts (some P) = some (raise ts P) + raise ts (pred p) = pred (Term.Var.raise ts p) + raise ts (comb f Ps) = comb f (helper ts Ps) + where + helper : ∀ (ts : Vec Type n) → Vec (Assertion Σ Γ Δ) k → Vec (Assertion Σ (ts ++ Γ) Δ) k + helper ts [] = [] + helper ts (P ∷ Ps) = raise ts P ∷ helper ts Ps + + elim : ∀ i → Assertion Σ (insert Γ i t) Δ → Term Σ Γ Δ t → Assertion Σ Γ Δ + elim i (all P) e = all (elim i P (Term.Meta.weaken 0F e)) + elim i (some P) e = some (elim i P (Term.Meta.weaken 0F e)) + elim i (pred p) e = pred (Term.Var.elim i p e) + elim i (comb f Ps) e = comb f (helper i Ps e) + where + helper : ∀ i → Vec (Assertion Σ (insert Γ i t) Δ) k → Term Σ Γ Δ t → Vec (Assertion Σ Γ Δ) k + helper i [] e = [] + helper i (P ∷ Ps) e = elim i P e ∷ helper i Ps e + + elimAll : Assertion Σ Γ Δ → All (Term Σ ts Δ) Γ → Assertion Σ ts Δ + elimAll (all P) es = all (elimAll P (map (Term.Meta.weaken 0F) es)) + elimAll (some P) es = some (elimAll P (map (Term.Meta.weaken 0F) es)) + elimAll (pred p) es = pred (Term.Var.elimAll p es) + elimAll (comb f Ps) es = comb f (helper Ps es) + where + helper : Vec (Assertion Σ Γ Δ) n → All (Term Σ ts Δ) Γ → Vec (Assertion Σ ts Δ) n + helper [] es = [] + helper (P ∷ Ps) es = elimAll P es ∷ helper Ps es + +module Meta where + weaken : ∀ i → Assertion Σ Γ Δ → Assertion Σ Γ (insert Δ i t) + weaken i (all P) = all (weaken (suc i) P) + weaken i (some P) = some (weaken (suc i) P) + weaken i (pred p) = pred (Term.Meta.weaken i p) + weaken i (comb f Ps) = comb f (helper i Ps) + where + helper : ∀ i → Vec (Assertion Σ Γ Δ) k → Vec (Assertion Σ Γ (insert Δ i t)) k + helper i [] = [] + helper i (P ∷ Ps) = weaken i P ∷ helper i Ps + + elim : ∀ i → Assertion Σ Γ (insert Δ i t) → Term Σ Γ Δ t → Assertion Σ Γ Δ + elim i (all P) e = all (elim (suc i) P (Term.Meta.weaken 0F e)) + elim i (some P) e = some (elim (suc i) P (Term.Meta.weaken 0F e)) + elim i (pred p) e = pred (Term.Meta.elim i p e) + elim i (comb f Ps) e = comb f (helper i Ps e) + where + helper : ∀ i → Vec (Assertion Σ Γ (insert Δ i t)) k → Term Σ Γ Δ t → Vec (Assertion Σ Γ Δ) k + helper i [] e = [] + helper i (P ∷ Ps) e = elim i P e ∷ helper i Ps e + +subst : Assertion Σ Γ Δ → Reference Σ Γ t → Term Σ Γ Δ t → Assertion Σ Γ Δ +subst (all P) ref val = all (subst P ref (Term.Meta.weaken 0F val)) +subst (some P) ref val = some (subst P ref (Term.Meta.weaken 0F val)) +subst (pred p) ref val = pred (Term.subst p ref val) +subst (comb f Ps) ref val = comb f (helper Ps ref val) + where + helper : Vec (Assertion Σ Γ Δ) k → Reference Σ Γ t → Term Σ Γ Δ t → Vec (Assertion Σ Γ Δ) k + helper [] ref val = [] + helper (P ∷ Ps) ref val = subst P ref val ∷ Ps + + +module Semantics (2≉0 : 2≉0) where + module TS {i} {j} {k} = Term.Semantics {i} {j} {k} 2≉0 + + ⟦_⟧ : Assertion Σ Γ Δ → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ Δ ⟧ₜ′ → Set ℓ + ⟦_⟧′ : Vec (Assertion Σ Γ Δ) n → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ Δ ⟧ₜ′ → Vec (Set ℓ) n -⟦ all P ⟧ σ γ δ = ∀ x → ⟦ P ⟧ σ γ (x , δ) -⟦ some P ⟧ σ γ δ = ∃ λ x → ⟦ P ⟧ σ γ (x , δ) -⟦ pred p ⟧ σ γ δ = Lift (b₁ ⊔ i₁ ⊔ r₁) (Bool.T (lower (Term.⟦ p ⟧ σ γ δ))) -⟦ comb f Ps ⟧ σ γ δ = f (⟦ Ps ⟧′ σ γ δ) + ⟦_⟧ {Δ = Δ} (all P) σ γ δ = ∀ x → ⟦ P ⟧ σ γ (cons′ Δ x δ) + ⟦_⟧ {Δ = Δ} (some P) σ γ δ = ∃ λ x → ⟦ P ⟧ σ γ (cons′ Δ x δ) + ⟦ pred p ⟧ σ γ δ = Lift ℓ (Bool.T (lower (TS.⟦ p ⟧ σ γ δ))) + ⟦ comb f Ps ⟧ σ γ δ = f (Vecᵣ.fromVec (⟦ Ps ⟧′ σ γ δ)) -⟦ [] ⟧′ σ γ δ = [] -⟦ P ∷ Ps ⟧′ σ γ δ = ⟦ P ⟧ σ γ δ ∷ ⟦ Ps ⟧′ σ γ δ + ⟦ [] ⟧′ σ γ δ = [] + ⟦ P ∷ Ps ⟧′ σ γ δ = ⟦ P ⟧ σ γ δ ∷ ⟦ Ps ⟧′ σ γ δ |