From 91cd436bce90fbcf863ecf4c1256bf4ef8769428 Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Mon, 21 Feb 2022 16:53:13 +0000 Subject: Generalise slice and join into cut and splice. --- src/Helium/Data/Pseudocode/Core.agda | 117 +++++++------ src/Helium/Semantics/Axiomatic/Core.agda | 245 ++++++++++++---------------- 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 _≟_ _>_ : 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 ) +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ℕ