From 69b82b0f568dd840f05f6aa9902ee6dcd5df5cad Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Tue, 8 Mar 2022 18:49:39 +0000 Subject: Migrate to agda-stdlib-2.0-dev. --- src/Helium/Algebra/Bundles.agda | 1 + src/Helium/Algebra/Decidable/Bundles.agda | 2 +- src/Helium/Algebra/Decidable/Construct/Pointwise.agda | 2 +- src/Helium/Algebra/Ordered/StrictTotal/Structures.agda | 5 ++++- src/Helium/Algebra/Structures.agda | 5 ++++- src/Helium/Data/Pseudocode/Manipulate.agda | 4 ++-- src/Helium/Instructions/Base.agda | 2 +- src/Helium/Semantics/Axiomatic/Core.agda | 14 -------------- src/Helium/Semantics/Axiomatic/Term.agda | 4 ++-- 9 files changed, 16 insertions(+), 23 deletions(-) (limited to 'src') diff --git a/src/Helium/Algebra/Bundles.agda b/src/Helium/Algebra/Bundles.agda index 1fa3634..c7ed8d0 100644 --- a/src/Helium/Algebra/Bundles.agda +++ b/src/Helium/Algebra/Bundles.agda @@ -10,6 +10,7 @@ module Helium.Algebra.Bundles where open import Algebra.Bundles +open import Algebra.Lattice.Bundles open import Algebra.Core open import Helium.Algebra.Core open import Helium.Algebra.Structures diff --git a/src/Helium/Algebra/Decidable/Bundles.agda b/src/Helium/Algebra/Decidable/Bundles.agda index e446706..c40de30 100644 --- a/src/Helium/Algebra/Decidable/Bundles.agda +++ b/src/Helium/Algebra/Decidable/Bundles.agda @@ -9,7 +9,7 @@ module Helium.Algebra.Decidable.Bundles where -open import Algebra.Bundles using (RawLattice) +open import Algebra.Lattice.Bundles using (RawLattice) open import Algebra.Core open import Helium.Algebra.Decidable.Structures open import Level using (suc; _⊔_) diff --git a/src/Helium/Algebra/Decidable/Construct/Pointwise.agda b/src/Helium/Algebra/Decidable/Construct/Pointwise.agda index 9f067ba..cccaa96 100644 --- a/src/Helium/Algebra/Decidable/Construct/Pointwise.agda +++ b/src/Helium/Algebra/Decidable/Construct/Pointwise.agda @@ -8,7 +8,7 @@ module Helium.Algebra.Decidable.Construct.Pointwise where -open import Algebra.Bundles using (RawLattice) +open import Algebra.Lattice.Bundles using (RawLattice) open import Algebra.Core open import Data.Nat using (ℕ) open import Data.Product using (_,_) diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Structures.agda b/src/Helium/Algebra/Ordered/StrictTotal/Structures.agda index 6f6b38d..b9db374 100644 --- a/src/Helium/Algebra/Ordered/StrictTotal/Structures.agda +++ b/src/Helium/Algebra/Ordered/StrictTotal/Structures.agda @@ -161,6 +161,7 @@ record IsAbelianGroup (∙ : Op₂ A) record IsRing (+ _*_ : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field +-isAbelianGroup : IsAbelianGroup + 0# -_ + -- FIXME: unroll definition *-isMonoid : NoOrder.IsMonoid _*_ 1# distrib : _*_ DistributesOver + zero : Zero 0# _*_ @@ -224,7 +225,9 @@ record IsRing (+ _*_ : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ₁ isRing : NoOrder.IsRing + _*_ -_ 0# 1# isRing = record { +-isAbelianGroup = IsAbelianGroup.Unordered.isAbelianGroup +-isAbelianGroup - ; *-isMonoid = *-isMonoid + ; *-cong = *-cong + ; *-assoc = *-assoc + ; *-identity = *-identity ; distrib = distrib ; zero = zero } diff --git a/src/Helium/Algebra/Structures.agda b/src/Helium/Algebra/Structures.agda index b64b4c7..f88ce59 100644 --- a/src/Helium/Algebra/Structures.agda +++ b/src/Helium/Algebra/Structures.agda @@ -72,6 +72,7 @@ record IsDivisionRing (_⁻¹ : AlmostOp₁ _≈_ 0#) : Set (a ⊔ ℓ) where field +-isAbelianGroup : IsAbelianGroup + 0# -_ + -- FIXME: unroll definition *-isAlmostGroup : IsAlmostGroup _*_ 0# 1# _⁻¹ distrib : _*_ DistributesOver + zero : Zero 0# _*_ @@ -126,7 +127,9 @@ record IsDivisionRing isRing : IsRing + _*_ -_ 0# 1# isRing = record { +-isAbelianGroup = +-isAbelianGroup - ; *-isMonoid = *-isMonoid + ; *-cong = *-cong + ; *-assoc = *-assoc + ; *-identity = *-identity ; distrib = distrib ; zero = zero } diff --git a/src/Helium/Data/Pseudocode/Manipulate.agda b/src/Helium/Data/Pseudocode/Manipulate.agda index 0ca5194..a5fe519 100644 --- a/src/Helium/Data/Pseudocode/Manipulate.agda +++ b/src/Helium/Data/Pseudocode/Manipulate.agda @@ -1240,10 +1240,10 @@ private e (Vec.allFin m) where - helper : ∀ {n m} k (f : ∀ {n : ℕ} e (i : Fin m) → ∃ λ e′ → callDepth e′ ℕ.≤ k ⊔ callDepth e) → ∀ e xs → callDepth (Vec.foldl (λ _ → Expression Γ ret) {n} (λ {n} e i → proj₁ (f {n} e i)) e xs) ℕ.≤ k ⊔ callDepth e + helper : ∀ {n m} k (f : ∀ e (i : Fin m) → ∃ λ e′ → callDepth e′ ℕ.≤ k ⊔ callDepth e) → ∀ e xs → callDepth (Vec.foldl′ {n = n} (λ e i → proj₁ (f e i)) e xs) ℕ.≤ k ⊔ callDepth e helper k f e [] = ℕₚ.m≤n⊔m k (callDepth e) helper k f e (x ∷ xs) = begin - callDepth (Vec.foldl _ (λ e i → proj₁ (f e i)) (proj₁ (f e x)) xs) + callDepth (Vec.foldl′ (λ e i → proj₁ (f e i)) (proj₁ (f e x)) xs) ≤⟨ helper k f (proj₁ (f e x)) xs ⟩ k ⊔ callDepth (proj₁ (f e x)) ≤⟨ ℕₚ.⊔-monoʳ-≤ k (proj₂ (f e x)) ⟩ diff --git a/src/Helium/Instructions/Base.agda b/src/Helium/Instructions/Base.agda index d157d5a..29e163d 100644 --- a/src/Helium/Instructions/Base.agda +++ b/src/Helium/Instructions/Base.agda @@ -130,7 +130,7 @@ LSL-C : ∀ {n} (shift : ℕ) → Function (bits n ∷ []) (tuple 2 (bits n ∷ LSL-C {n} shift = declare (var 0F ∶ lit ((Vec.replicate {n = (suc shift)} false) ′xs)) (skip ∙return tup ( slice (var 0F) (lit (zero ′f)) - ∷ unbox (slice (cast eq (var 0F)) (lit (Fin.inject+ shift (Fin.fromℕ n) ′f))) + ∷ unbox (slice (cast eq (var 0F)) (lit (((Fin.fromℕ n) Fin.↑ˡ shift) ′f))) ∷ [])) where eq = P.trans (ℕₚ.+-comm 1 (shift ℕ.+ n)) (P.cong (ℕ._+ 1) (ℕₚ.+-comm shift n)) diff --git a/src/Helium/Semantics/Axiomatic/Core.agda b/src/Helium/Semantics/Axiomatic/Core.agda index 3b7e8db..dd03a55 100644 --- a/src/Helium/Semantics/Axiomatic/Core.agda +++ b/src/Helium/Semantics/Axiomatic/Core.agda @@ -69,17 +69,3 @@ Transform ts t = ⟦ ts ⟧ₜ′ → ⟦ t ⟧ₜ Predicate : Vec Type m → Set (b₁ ⊔ i₁ ⊔ r₁) Predicate ts = ⟦ ts ⟧ₜ′ → Bool - --- 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/Axiomatic/Term.agda b/src/Helium/Semantics/Axiomatic/Term.agda index c7c2797..e9a3f4a 100644 --- a/src/Helium/Semantics/Axiomatic/Term.agda +++ b/src/Helium/Semantics/Axiomatic/Term.agda @@ -102,7 +102,7 @@ wknVar (func f ts) = func f (helper ts) wknVars : (ts : Vec Type n) → Term Σ Γ Δ t → Term Σ (ts ++ Γ) Δ t wknVars τs (state i) = state i -wknVars τs (var i) = castType (var (Fin.raise (Vec.length τs) i)) (Vecₚ.lookup-++ʳ τs _ i) +wknVars τs (var i) = castType (var (Vec.length τs Fin.↑ʳ i)) (Vecₚ.lookup-++ʳ τs _ i) wknVars τs (meta i) = meta i wknVars τs (func f ts) = func f (helper ts) where @@ -135,7 +135,7 @@ wknMeta = wknMetaAt 0F wknMetas : (ts : Vec Type n) → Term Σ Γ Δ t → Term Σ Γ (ts ++ Δ) t wknMetas τs (state i) = state i wknMetas τs (var i) = var i -wknMetas τs (meta i) = castType (meta (Fin.raise (Vec.length τs) i)) (Vecₚ.lookup-++ʳ τs _ i) +wknMetas τs (meta i) = castType (meta (Vec.length τs Fin.↑ʳ i)) (Vecₚ.lookup-++ʳ τs _ i) wknMetas τs (func f ts) = func f (helper ts) where helper : ∀ {n ts} → All (Term Σ Γ Δ) {n} ts → All (Term Σ Γ (τs ++ Δ)) ts -- cgit v1.2.3