Migrate to agda-stdlib-2.0-dev.axiomatic

11 files changed, 34 insertions, 25 deletions

diff --git a/agda-helium.agda-lib b/agda-helium.agda-lib
index bec951d..91efa04 100644
--- a/agda-helium.agda-lib
+++ b/agda-helium.agda-lib
@@ -1,3 +1,3 @@
 name: agda-helium-0.1
-depend: standard-library-1.7.1
+depend: standard-library-2.0
 include: src
diff --git a/guix.scm b/guix.scm
index 6e3e28c..e5e8d80 100644
--- a/guix.scm
+++ b/guix.scm
@@ -8,6 +8,22 @@
              (yellowsquid build-system agda))
 (define %source-dir (dirname (current-filename)))
 
+;; NOTE: still a dev build
+(define agda-stdlib-2.0-dev
+  (package
+    (inherit agda-stdlib-1.7.1)
+    (name "agda-stdlib")
+    (version "2.0")
+    (home-page "https://github.com/agda/agda-stdlib")
+    (source (origin
+              (method git-fetch)
+              (uri (git-reference (url home-page)
+                                  (commit "a9e97a33e2796d9ce4f8ed6da5a927ae33daf0b1")))
+              (file-name (git-file-name name version))
+              (sha256
+               (base32
+                "0m5f0x8jygvl9ackqpxxjx70kb2jb2qv6irj5wzxx8bd9q423m85"))))))
+
 (define-public agda-helium
   (package
     (name "agda-helium")
@@ -17,7 +33,7 @@
                         #:recursive? #t
                         #:select? (git-predicate %source-dir)))
     (build-system agda-build-system)
-    (inputs (list agda-stdlib-1.7.1))
+    (inputs (list agda-stdlib-2.0-dev))
     (synopsis "Semantics of the Arm M-profile Vector Extension (MVE) in Agda")
     (description "")
     (license license:expat)))
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