summaryrefslogtreecommitdiff
path: root/src/Helium/Semantics
diff options
context:
space:
mode:
authorGreg Brown <greg.brown@cl.cam.ac.uk>2022-04-18 15:05:24 +0100
committerGreg Brown <greg.brown@cl.cam.ac.uk>2022-04-18 15:21:38 +0100
commit00a0ce9082b4cc1389815defcc806efd4a9b80f4 (patch)
treeaebdc99b954be177571697fc743ee75841c98b2e /src/Helium/Semantics
parent24845ef25e12864711552ebc75a1f54903bee50c (diff)
Do a big refactor.
- Replace the decidable predicates on expressions and statements with separate data types. - Reorganise the Hoare logic semantics to remove unnecessary definitions. - Make liberal use of modules to group related definitions together. - Unify the types for denotational and Hoare logic semantics. - Make bits an abstraction of array types.
Diffstat (limited to 'src/Helium/Semantics')
-rw-r--r--src/Helium/Semantics/Axiomatic.agda47
-rw-r--r--src/Helium/Semantics/Axiomatic/Assertion.agda247
-rw-r--r--src/Helium/Semantics/Axiomatic/Core.agda85
-rw-r--r--src/Helium/Semantics/Axiomatic/Term.agda873
-rw-r--r--src/Helium/Semantics/Axiomatic/Triple.agda61
-rw-r--r--src/Helium/Semantics/Core.agda209
-rw-r--r--src/Helium/Semantics/Denotational/Core.agda416
7 files changed, 1062 insertions, 876 deletions
diff --git a/src/Helium/Semantics/Axiomatic.agda b/src/Helium/Semantics/Axiomatic.agda
index 2fa3db1..02e2a69 100644
--- a/src/Helium/Semantics/Axiomatic.agda
+++ b/src/Helium/Semantics/Axiomatic.agda
@@ -17,31 +17,38 @@ open import Helium.Data.Pseudocode.Algebra.Properties pseudocode
open import Data.Nat using (ℕ)
import Data.Unit
-open import Data.Vec using (Vec)
open import Function using (_∘_)
-open import Helium.Data.Pseudocode.Core
-import Helium.Semantics.Axiomatic.Core rawPseudocode as Core
-import Helium.Semantics.Axiomatic.Assertion rawPseudocode as Assertion
-import Helium.Semantics.Axiomatic.Term rawPseudocode as Term
-import Helium.Semantics.Axiomatic.Triple rawPseudocode as Triple
+import Helium.Semantics.Core rawPseudocode as Core′
+import Helium.Semantics.Axiomatic.Term rawPseudocode as Term′
+import Helium.Semantics.Axiomatic.Assertion rawPseudocode as Assertion′
-open Assertion.Construct public
-open Assertion.Assertion public
+private
+ proof-2≉0 : Core′.2≉0
+ proof-2≉0 = ℝ.<⇒≉ (ℝ.n≢0∧x>0⇒n×x>0 2 (ℝ.≤∧≉⇒< ℝ.0≤1 (ℝ.1≉0 ∘ ℝ.Eq.sym))) ∘ ℝ.Eq.sym
-open Assertion public
- using (Assertion)
+module Core where
+ open Core′ public hiding (shift)
-open Term.Term public
-open Term public
- using (Term)
+ shift : ℤ → ℕ → ℤ
+ shift = Core′.shift proof-2≉0
+
+open Core public using (⟦_⟧ₜ; ⟦_⟧ₜ′; Κ[_]_; 2≉0)
-2≉0 : 2 ℝ.× 1ℝ ℝ.≉ 0ℝ
-2≉0 = ℝ.<⇒≉ (ℝ.n≢0∧x>0⇒n×x>0 2 (ℝ.≤∧≉⇒< ℝ.0≤1 (ℝ.1≉0 ∘ ℝ.Eq.sym))) ∘ ℝ.Eq.sym
+module Term where
+ open Term′ public hiding (module Semantics)
+ module Semantics {i} {j} {k} where
+ open Term′.Semantics {i} {j} {k} proof-2≉0 public
-HoareTriple : ∀ {o} {Σ : Vec Type o} {n} {Γ : Vec Type n} {m} {Δ : Vec Type m} → Assertion Σ Γ Δ → Code.Statement Σ Γ → Assertion Σ Γ Δ → Set _
-HoareTriple = Triple.HoareTriple 2≉0
+open Term public using (Term; ↓_) hiding (module Term)
+open Term.Term public
+
+module Assertion where
+ open Assertion′ public hiding (module Semantics)
+ module Semantics where
+ open Assertion′.Semantics proof-2≉0 public
-ℰ : ∀ {o} {Σ : Vec Type o} {n} {Γ : Vec Type n} {m} {Δ : Vec Type m} {t : Type} → Code.Expression Σ Γ t → Term Σ Γ Δ t
-ℰ = Term.ℰ 2≉0
+open Assertion public using (Assertion) hiding (module Assertion)
+open Assertion.Assertion public
+open Assertion.Construct public
-open Triple.HoareTriple 2≉0 public
+open import Helium.Semantics.Axiomatic.Triple rawPseudocode proof-2≉0 public
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 ⟧′ σ γ δ
diff --git a/src/Helium/Semantics/Axiomatic/Core.agda b/src/Helium/Semantics/Axiomatic/Core.agda
deleted file mode 100644
index a65a6d0..0000000
--- a/src/Helium/Semantics/Axiomatic/Core.agda
+++ /dev/null
@@ -1,85 +0,0 @@
-------------------------------------------------------------------------
--- Agda Helium
---
--- Base definitions for the axiomatic semantics
-------------------------------------------------------------------------
-
-{-# OPTIONS --safe --without-K #-}
-
-open import Helium.Data.Pseudocode.Algebra using (RawPseudocode)
-
-module Helium.Semantics.Axiomatic.Core
- {b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃}
- (rawPseudocode : RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃)
- where
-
-private
- open module C = RawPseudocode rawPseudocode
-
-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 as × using (_×_; _,_; uncurry)
-open import Data.Sum using (_⊎_)
-open import Data.Unit using (⊤)
-open import Data.Vec as Vec using (Vec; []; _∷_; _++_; lookup)
-open import Data.Vec.Relation.Unary.All as All using (All; []; _∷_)
-open import Function using (_on_)
-open import Helium.Data.Pseudocode.Core
-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
-
-⟦_⟧ₜ : Type → Set (b₁ ⊔ i₁ ⊔ r₁)
-⟦_⟧ₜ′ : Vec Type n → Set (b₁ ⊔ i₁ ⊔ r₁)
-
-⟦ bool ⟧ₜ = Lift (b₁ ⊔ i₁ ⊔ r₁) Bool
-⟦ int ⟧ₜ = Lift (b₁ ⊔ r₁) ℤ
-⟦ fin n ⟧ₜ = Lift (b₁ ⊔ i₁ ⊔ r₁) (Fin n)
-⟦ real ⟧ₜ = Lift (b₁ ⊔ i₁) ℝ
-⟦ bit ⟧ₜ = Lift (i₁ ⊔ r₁) Bit
-⟦ bits n ⟧ₜ = Vec ⟦ bit ⟧ₜ n
-⟦ tuple n ts ⟧ₜ = ⟦ ts ⟧ₜ′
-⟦ array t n ⟧ₜ = Vec ⟦ t ⟧ₜ n
-
-⟦ [] ⟧ₜ′ = Lift (b₁ ⊔ i₁ ⊔ r₁) ⊤
-⟦ t ∷ ts ⟧ₜ′ = ⟦ t ⟧ₜ × ⟦ ts ⟧ₜ′
-
-fetch : ∀ i → ⟦ Γ ⟧ₜ′ → ⟦ lookup Γ i ⟧ₜ
-fetch {Γ = _ ∷ _} 0F (x , _) = x
-fetch {Γ = _ ∷ _} (suc i) (_ , xs) = fetch i xs
-
-Transform : Vec Type m → Type → Set (b₁ ⊔ i₁ ⊔ r₁)
-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 c9ddd02..08eac5f 100644
--- a/src/Helium/Semantics/Axiomatic/Term.agda
+++ b/src/Helium/Semantics/Axiomatic/Term.agda
@@ -13,373 +13,530 @@ module Helium.Semantics.Axiomatic.Term
(rawPseudocode : RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃)
where
+
open RawPseudocode rawPseudocode
import Data.Bool as Bool
-open import Data.Fin as Fin using (Fin; suc)
-import Data.Fin.Properties as Finₚ
+open import Data.Empty using (⊥-elim)
+open import Data.Fin as Fin using (Fin; suc; punchOut)
open import Data.Fin.Patterns
-open import Data.Nat as ℕ using (ℕ; suc)
+import Data.Integer as 𝕀
+import Data.Fin.Properties as Finₚ
+open import Data.Nat as ℕ using (ℕ; suc; _≤_; z≤n; s≤s; _⊔_)
import Data.Nat.Properties as ℕₚ
-open import Data.Product using (∃; _×_; _,_; proj₁; proj₂; uncurry; dmap)
-open import Data.Vec as Vec using (Vec; []; _∷_; _++_; lookup)
-import Data.Vec.Functional as VecF
+open import Data.Product using (∃; _,_; dmap)
+open import Data.Vec as Vec using (Vec; []; _∷_; _++_; lookup; insert; remove; map; zipWith; take; drop)
import Data.Vec.Properties as Vecₚ
+open import Data.Vec.Recursive as Vecᵣ using (2+_)
open import Data.Vec.Relation.Unary.All as All using (All; []; _∷_)
-open import Function using (_∘_; _∘₂_; id; flip)
+open import Function
open import Helium.Data.Pseudocode.Core
-import Helium.Data.Pseudocode.Manipulate as M
-open import Helium.Semantics.Axiomatic.Core rawPseudocode
-open import Level using (_⊔_; lift; lower)
-open import Relation.Binary.PropositionalEquality hiding ([_]) renaming (subst to ≡-subst)
-open import Relation.Nullary using (¬_; does; yes; no)
-open import Relation.Nullary.Decidable.Core using (True; toWitness)
-open import Relation.Nullary.Negation using (contradiction)
+open import Helium.Data.Pseudocode.Manipulate hiding (module Cast)
+open import Helium.Semantics.Core rawPseudocode
+open import Level as L using (lift; lower)
+open import Relation.Binary.PropositionalEquality hiding (subst)
+open import Relation.Nullary using (does; yes; no)
private
variable
- t t′ t₁ t₂ : Type
- m n o : ℕ
- Γ Δ Σ ts : Vec Type m
-
-data Term (Σ : Vec Type o) (Γ : Vec Type n) (Δ : Vec Type m) : Type → Set (b₁ ⊔ i₁ ⊔ r₁) where
- state : ∀ i → Term Σ Γ Δ (lookup Σ i)
- var : ∀ i → Term Σ Γ Δ (lookup Γ i)
- meta : ∀ i → Term Σ Γ Δ (lookup Δ i)
- func : Transform ts t → All (Term Σ Γ Δ) ts → Term Σ Γ Δ t
-
-castType : Term Σ Γ Δ t → t ≡ t′ → Term Σ Γ Δ t′
-castType (state i) refl = state i
-castType (var i) refl = var i
-castType (meta i) refl = meta i
-castType (func f ts) eq = func (≡-subst (Transform _) eq f) ts
-
-substState : Term Σ Γ Δ t → ∀ i → Term Σ Γ Δ (lookup Σ i) → Term Σ Γ Δ t
-substState (state i) j t′ with i Fin.≟ j
-... | yes refl = t′
-... | no _ = state i
-substState (var i) j t′ = var i
-substState (meta i) j t′ = meta i
-substState (func f ts) j t′ = func f (helper ts j t′)
- where
- helper : ∀ {n ts} → All (Term Σ Γ Δ) {n} ts → ∀ i → Term Σ Γ Δ (lookup Σ i) → All (Term Σ Γ Δ) ts
- helper [] i t′ = []
- helper (t ∷ ts) i t′ = substState t i t′ ∷ helper ts i t′
-
-substVar : Term Σ Γ Δ t → ∀ i → Term Σ Γ Δ (lookup Γ i) → Term Σ Γ Δ t
-substVar (state i) j t′ = state i
-substVar (var i) j t′ with i Fin.≟ j
-... | yes refl = t′
-... | no _ = var i
-substVar (meta i) j t′ = meta i
-substVar (func f ts) j t′ = func f (helper ts j t′)
- where
- helper : ∀ {n ts} → All (Term Σ Γ Δ) {n} ts → ∀ i → Term Σ Γ Δ (lookup Γ i) → All (Term Σ Γ Δ) ts
- helper [] i t′ = []
- helper (t ∷ ts) i t′ = substVar t i t′ ∷ helper ts i t′
-
-substVars : Term Σ Γ Δ t → All (Term Σ ts Δ) Γ → Term Σ ts Δ t
-substVars (state i) ts = state i
-substVars (var i) ts = All.lookup i ts
-substVars (meta i) ts = meta i
-substVars (func f ts′) ts = func f (helper ts′ ts)
- where
- helper : ∀ {ts ts′} → All (Term Σ Γ Δ) {n} ts → All (Term {n = m} Σ ts′ Δ) Γ → All (Term Σ ts′ Δ) ts
- helper [] ts = []
- helper (t ∷ ts′) ts = substVars t ts ∷ helper ts′ ts
-
-elimVar : Term Σ (t′ ∷ Γ) Δ t → Term Σ Γ Δ t′ → Term Σ Γ Δ t
-elimVar (state i) t′ = state i
-elimVar (var 0F) t′ = t′
-elimVar (var (suc i)) t′ = var i
-elimVar (meta i) t′ = meta i
-elimVar (func f ts) t′ = func f (helper ts t′)
- where
- helper : ∀ {n ts} → All (Term Σ (_ ∷ Γ) Δ) {n} ts → Term Σ Γ Δ _ → All (Term Σ Γ Δ) ts
- helper [] t′ = []
- helper (t ∷ ts) t′ = elimVar t t′ ∷ helper ts t′
-
-wknVar : Term Σ Γ Δ t → Term Σ (t′ ∷ Γ) Δ t
-wknVar (state i) = state i
-wknVar (var i) = var (suc i)
-wknVar (meta i) = meta i
-wknVar (func f ts) = func f (helper ts)
- where
- helper : ∀ {n ts} → All (Term Σ Γ Δ) {n} ts → All (Term Σ (_ ∷ Γ) Δ) ts
- helper [] = []
- helper (t ∷ ts) = wknVar t ∷ 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 (meta i) = meta i
-wknVars τs (func f ts) = func f (helper ts)
- where
- helper : ∀ {n ts} → All (Term Σ Γ Δ) {n} ts → All (Term Σ (τs ++ Γ) Δ) ts
- helper [] = []
- helper (t ∷ ts) = wknVars τs t ∷ helper ts
-
-addVars : Term Σ [] Δ t → Term Σ Γ Δ t
-addVars (state i) = state i
-addVars (meta i) = meta i
-addVars (func f ts) = func f (helper ts)
- where
- helper : ∀ {n ts} → All (Term Σ [] Δ) {n} ts → All (Term Σ Γ Δ) ts
- helper [] = []
- helper (t ∷ ts) = addVars t ∷ helper ts
-
-wknMetaAt : ∀ i → Term Σ Γ Δ t → Term Σ Γ (Vec.insert Δ i t′) t
-wknMetaAt′ : ∀ i → All (Term Σ Γ Δ) ts → All (Term Σ Γ (Vec.insert Δ i t′)) ts
-
-wknMetaAt i (state j) = state j
-wknMetaAt i (var j) = var j
-wknMetaAt i (meta j) = castType (meta (Fin.punchIn i j)) (Vecₚ.insert-punchIn _ i _ j)
-wknMetaAt i (func f ts) = func f (wknMetaAt′ i ts)
-
-wknMetaAt′ i [] = []
-wknMetaAt′ i (t ∷ ts) = wknMetaAt i t ∷ wknMetaAt′ i ts
-
-wknMeta : Term Σ Γ Δ t → Term Σ Γ (t′ ∷ Δ) t
-wknMeta = wknMetaAt 0F
-
-wknMeta′ : All (Term Σ Γ Δ) ts → All (Term Σ Γ (t′ ∷ Δ)) ts
-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 (func f ts) = func f (helper ts)
- where
- helper : ∀ {n ts} → All (Term Σ Γ Δ) {n} ts → All (Term Σ Γ (τs ++ Δ)) ts
- helper [] = []
- helper (t ∷ ts) = wknMetas τs t ∷ helper ts
-
-func₀ : ⟦ t ⟧ₜ → Term Σ Γ Δ t
-func₀ f = func (λ _ → f) []
-
-func₁ : (⟦ t ⟧ₜ → ⟦ t′ ⟧ₜ) → Term Σ Γ Δ t → Term Σ Γ Δ t′
-func₁ f t = func (λ (x , _) → f x) (t ∷ [])
-
-func₂ : (⟦ t₁ ⟧ₜ → ⟦ t₂ ⟧ₜ → ⟦ t′ ⟧ₜ) → Term Σ Γ Δ t₁ → Term Σ Γ Δ t₂ → Term Σ Γ Δ t′
-func₂ f t₁ t₂ = func (λ (x , y , _) → f x y) (t₁ ∷ t₂ ∷ [])
-
-[_][_≟_] : HasEquality t → Term Σ Γ Δ t → Term Σ Γ Δ t → Term Σ Γ Δ bool
-[ bool ][ t ≟ t′ ] = func₂ (λ (lift x) (lift y) → lift (does (x Bool.≟ y))) t t′
-[ int ][ t ≟ t′ ] = func₂ (λ (lift x) (lift y) → lift (does (x ≟ᶻ y))) t t′
-[ fin ][ t ≟ t′ ] = func₂ (λ (lift x) (lift y) → lift (does (x Fin.≟ y))) t t′
-[ real ][ t ≟ t′ ] = func₂ (λ (lift x) (lift y) → lift (does (x ≟ʳ y))) t t′
-[ bit ][ t ≟ t′ ] = func₂ (λ (lift x) (lift y) → lift (does (x ≟ᵇ₁ y))) t t′
-[ bits ][ t ≟ t′ ] = func₂ (λ xs ys → lift (does (VecF.fromVec (Vec.map lower xs) ≟ᵇ VecF.fromVec (Vec.map lower ys)))) t t′
-
-[_][_<?_] : IsNumeric t → Term Σ Γ Δ t → Term Σ Γ Δ t → Term Σ Γ Δ bool
-[ int ][ t <? t′ ] = func₂ (λ (lift x) (lift y) → lift (does (x <ᶻ? y))) t t′
-[ real ][ t <? t′ ] = func₂ (λ (lift x) (lift y) → lift (does (x <ʳ? y))) t t′
-
-[_][_] : ∀ t → Term Σ Γ Δ (elemType t) → Term Σ Γ Δ (asType t 1)
-[ bits ][ t ] = func₁ (_∷ []) t
-[ array τ ][ t ] = func₁ (_∷ []) t
-
-unbox : ∀ t → Term Σ Γ Δ (asType t 1) → Term Σ Γ Δ (elemType t)
-unbox bits = func₁ Vec.head
-unbox (array t) = func₁ Vec.head
-
-castV : ∀ {a} {A : Set a} {m n} → .(eq : m ≡ n) → Vec A m → Vec A n
-castV {n = 0} eq [] = []
-castV {n = suc n} eq (x ∷ xs) = x ∷ castV (ℕₚ.suc-injective eq) xs
-
-cast′ : ∀ t → .(eq : m ≡ n) → ⟦ asType t m ⟧ₜ → ⟦ asType t n ⟧ₜ
-cast′ bits eq = castV eq
-cast′ (array τ) eq = castV eq
-
-cast : ∀ t → .(eq : m ≡ n) → Term Σ Γ Δ (asType t m) → Term Σ Γ Δ (asType t n)
-cast τ eq = func₁ (cast′ τ eq)
-
-[_][-_] : IsNumeric t → Term Σ Γ Δ t → Term Σ Γ Δ t
-[ int ][- t ] = func₁ (lift ∘ ℤ.-_ ∘ lower) t
-[ real ][- t ] = func₁ (lift ∘ ℝ.-_ ∘ lower) t
-
-[_,_,_,_][_+_] : ∀ t₁ t₂ → (isNum₁ : True (isNumeric? t₁)) → (isNum₂ : True (isNumeric? t₂)) → Term Σ Γ Δ t₁ → Term Σ Γ Δ t₂ → Term Σ Γ Δ (combineNumeric t₁ t₂ isNum₁ isNum₂)
-[ int , int , _ , _ ][ t + t′ ] = func₂ (λ (lift x) (lift y) → lift (x ℤ.+ y)) t t′
-[ int , real , _ , _ ][ t + t′ ] = func₂ (λ (lift x) (lift y) → lift (x /1 ℝ.+ y)) t t′
-[ real , int , _ , _ ][ t + t′ ] = func₂ (λ (lift x) (lift y) → lift (x ℝ.+ y /1)) t t′
-[ real , real , _ , _ ][ t + t′ ] = func₂ (λ (lift x) (lift y) → lift (x ℝ.+ y)) t t′
-
-[_,_,_,_][_*_] : ∀ t₁ t₂ → (isNum₁ : True (isNumeric? t₁)) → (isNum₂ : True (isNumeric? t₂)) → Term Σ Γ Δ t₁ → Term Σ Γ Δ t₂ → Term Σ Γ Δ (combineNumeric t₁ t₂ isNum₁ isNum₂)
-[ int , int , _ , _ ][ t * t′ ] = func₂ (λ (lift x) (lift y) → lift (x ℤ.* y)) t t′
-[ int , real , _ , _ ][ t * t′ ] = func₂ (λ (lift x) (lift y) → lift (x /1 ℝ.* y)) t t′
-[ real , int , _ , _ ][ t * t′ ] = func₂ (λ (lift x) (lift y) → lift (x ℝ.* y /1)) t t′
-[ real , real , _ , _ ][ t * t′ ] = func₂ (λ (lift x) (lift y) → lift (x ℝ.* y)) t t′
-
-[_][_^_] : IsNumeric t → Term Σ Γ Δ t → ℕ → Term Σ Γ Δ t
-[ int ][ t ^ n ] = func₁ (lift ∘ (ℤ′._^′ n) ∘ lower) t
-[ real ][ t ^ n ] = func₁ (lift ∘ (ℝ′._^′ n) ∘ lower) t
-
-2≉0 : Set _
-2≉0 = ¬ 2 ℝ′.×′ 1ℝ ℝ.≈ 0ℝ
-
-[_][_>>_] : 2≉0 → Term Σ Γ Δ int → ℕ → Term Σ Γ Δ int
-[ 2≉0 ][ t >> n ] = func₁ (lift ∘ ⌊_⌋ ∘ (ℝ._* 2≉0 ℝ.⁻¹ ℝ′.^′ n) ∘ _/1 ∘ lower) t
-
--- 0 of y is 0 of result
-join′ : ∀ t → ⟦ asType t m ⟧ₜ → ⟦ asType t n ⟧ₜ → ⟦ asType t (n ℕ.+ m) ⟧ₜ
-join′ bits = flip _++_
-join′ (array t) = flip _++_
-
-take′ : ∀ t m {n} → ⟦ asType t (m ℕ.+ n) ⟧ₜ → ⟦ asType t m ⟧ₜ
-take′ bits m = Vec.take m
-take′ (array t) m = Vec.take m
-
-drop′ : ∀ t m {n} → ⟦ asType t (m ℕ.+ n) ⟧ₜ → ⟦ asType t n ⟧ₜ
-drop′ bits m = Vec.drop m
-drop′ (array t) m = Vec.drop m
-
-private
- m≤n⇒m+k≡n : ∀ {m n} → m ℕ.≤ n → ∃ λ k → m ℕ.+ k ≡ n
- m≤n⇒m+k≡n ℕ.z≤n = _ , refl
- m≤n⇒m+k≡n (ℕ.s≤s m≤n) = dmap id (cong suc) (m≤n⇒m+k≡n m≤n)
-
- slicedSize : ∀ n m (i : Fin (suc n)) → ∃ λ k → n ℕ.+ m ≡ Fin.toℕ i ℕ.+ (m ℕ.+ k) × Fin.toℕ i ℕ.+ k ≡ n
- slicedSize n m i = k , (begin
- n ℕ.+ m ≡˘⟨ cong (ℕ._+ m) (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) ∎) ,
- proj₂ i+k≡n
- where
- open ≡-Reasoning
- i+k≡n = m≤n⇒m+k≡n (ℕₚ.≤-pred (Finₚ.toℕ<n i))
- k = proj₁ i+k≡n
-
--- 0 of x is i of result
-splice′ : ∀ t → ⟦ asType t m ⟧ₜ → ⟦ asType t n ⟧ₜ → ⟦ fin (suc n) ⟧ₜ → ⟦ asType t (n ℕ.+ m) ⟧ₜ
-splice′ {m = m} t x y (lift i) = cast′ t eq (join′ t (join′ t high x) low)
+ t t′ t₁ t₂ : Type
+ i j k m n o : ℕ
+ Γ Δ Σ ts : Vec Type m
+
+ ℓ = b₁ L.⊔ i₁ L.⊔ r₁
+
+ punchOut-insert : ∀ {a} {A : Set a} (xs : Vec A n) {i j} (i≢j : i ≢ j) x → lookup xs (punchOut i≢j) ≡ lookup (insert xs i x) j
+ punchOut-insert xs {i} {j} i≢j x = begin
+ lookup xs (punchOut i≢j) ≡˘⟨ cong (flip lookup (punchOut i≢j)) (Vecₚ.remove-insert xs i x) ⟩
+ lookup (remove (insert xs i x) i) (punchOut i≢j) ≡⟨ Vecₚ.remove-punchOut (insert xs i x) i≢j ⟩
+ lookup (insert xs i x) j ∎
+ where open ≡-Reasoning
+
+ open ℕₚ.≤-Reasoning
+
+ ⨆[_]_ : ∀ n → ℕ Vecᵣ.^ n → ℕ
+ ⨆[_]_ = Vecᵣ.foldl (const ℕ) 0 id (const (flip ℕ._⊔_))
+
+ ⨆-step : ∀ m x xs → ⨆[ 2+ m ] (x , xs) ≡ x ⊔ ⨆[ suc m ] xs
+ ⨆-step 0 x xs = refl
+ ⨆-step (suc m) x (y , xs) = begin-equality
+ ⨆[ 2+ suc m ] (x , y , xs) ≡⟨ ⨆-step m (x ⊔ y) xs ⟩
+ x ⊔ y ⊔ ⨆[ suc m ] xs ≡⟨ ℕₚ.⊔-assoc x y _ ⟩
+ x ⊔ (y ⊔ ⨆[ suc m ] xs) ≡˘⟨ cong (_ ⊔_) (⨆-step m y xs) ⟩
+ x ⊔ ⨆[ 2+ m ] (y , xs) ∎
+
+ lookup-⨆-≤ : ∀ i (xs : ℕ Vecᵣ.^ n) → Vecᵣ.lookup i xs ≤ ⨆[ n ] xs
+ lookup-⨆-≤ {1} 0F x = ℕₚ.≤-refl
+ lookup-⨆-≤ {2+ n} 0F (x , xs) = begin
+ x ≤⟨ ℕₚ.m≤m⊔n x _ ⟩
+ x ⊔ ⨆[ suc n ] xs ≡˘⟨ ⨆-step n x xs ⟩
+ ⨆[ 2+ n ] (x , xs) ∎
+ lookup-⨆-≤ {2+ n} (suc i) (x , xs) = begin
+ Vecᵣ.lookup i xs ≤⟨ lookup-⨆-≤ i xs ⟩
+ ⨆[ suc n ] xs ≤⟨ ℕₚ.m≤n⊔m x _ ⟩
+ x ⊔ ⨆[ suc n ] xs ≡˘⟨ ⨆-step n x xs ⟩
+ ⨆[ 2+ n ] (x , xs) ∎
+
+data Term (Σ : Vec Type i) (Γ : Vec Type j) (Δ : Vec Type k) : Type → Set ℓ where
+ lit : ⟦ t ⟧ₜ → Term Σ Γ Δ t
+ state : ∀ i → Term Σ Γ Δ (lookup Σ i)
+ var : ∀ i → Term Σ Γ Δ (lookup Γ i)
+ meta : ∀ i → Term Σ Γ Δ (lookup Δ i)
+ _≟_ : ⦃ HasEquality t ⦄ → Term Σ Γ Δ t → Term Σ Γ Δ t → Term Σ Γ Δ bool
+ _<?_ : ⦃ Ordered t ⦄ → Term Σ Γ Δ t → Term Σ Γ Δ t → Term Σ Γ Δ bool
+ inv : Term Σ Γ Δ bool → Term Σ Γ Δ bool
+ _&&_ : Term Σ Γ Δ bool → Term Σ Γ Δ bool → Term Σ Γ Δ bool
+ _||_ : Term Σ Γ Δ bool → Term Σ Γ Δ bool → Term Σ Γ Δ bool
+ not : Term Σ Γ Δ (bits n) → Term Σ Γ Δ (bits n)
+ _and_ : Term Σ Γ Δ (bits n) → Term Σ Γ Δ (bits n) → Term Σ Γ Δ (bits n)
+ _or_ : Term Σ Γ Δ (bits n) → Term Σ Γ Δ (bits n) → Term Σ Γ Δ (bits n)
+ [_] : Term Σ Γ Δ t → Term Σ Γ Δ (array t 1)
+ unbox : Term Σ Γ Δ (array t 1) → Term Σ Γ Δ t
+ merge : Term Σ Γ Δ (array t m) → Term Σ Γ Δ (array t n) → Term Σ Γ Δ (fin (suc n)) → Term Σ Γ Δ (array t (n ℕ.+ m))
+ slice : Term Σ Γ Δ (array t (n ℕ.+ m)) → Term Σ Γ Δ (fin (suc n)) → Term Σ Γ Δ (array t m)
+ cut : Term Σ Γ Δ (array t (n ℕ.+ m)) → Term Σ Γ Δ (fin (suc n)) → Term Σ Γ Δ (array t n)
+ cast : .(eq : m ≡ n) → Term Σ Γ Δ (array t m) → Term Σ Γ Δ (array t n)
+ -_ : ⦃ IsNumeric t ⦄ → Term Σ Γ Δ t → Term Σ Γ Δ t
+ _+_ : ⦃ isNum₁ : IsNumeric t₁ ⦄ → ⦃ isNum₂ : IsNumeric t₂ ⦄ → Term Σ Γ Δ t₁ → Term Σ Γ Δ t₂ → Term Σ Γ Δ (isNum₁ +ᵗ isNum₂)
+ _*_ : ⦃ isNum₁ : IsNumeric t₁ ⦄ → ⦃ isNum₂ : IsNumeric t₂ ⦄ → Term Σ Γ Δ t₁ → Term Σ Γ Δ t₂ → Term Σ Γ Δ (isNum₁ +ᵗ isNum₂)
+ _^_ : ⦃ IsNumeric t ⦄ → Term Σ Γ Δ t → ℕ → Term Σ Γ Δ t
+ _>>_ : Term Σ Γ Δ int → (n : ℕ) → Term Σ Γ Δ int
+ rnd : Term Σ Γ Δ real → Term Σ Γ Δ int
+ fin : ∀ {ms} (f : literalTypes (map fin ms) → Fin n) → Term Σ Γ Δ (tuple {n = o} (map fin ms)) → Term Σ Γ Δ (fin n)
+ asInt : Term Σ Γ Δ (fin n) → Term Σ Γ Δ int
+ nil : Term Σ Γ Δ (tuple [])
+ cons : Term Σ Γ Δ t → Term Σ Γ Δ (tuple ts) → Term Σ Γ Δ (tuple (t ∷ ts))
+ head : Term Σ Γ Δ (tuple (t ∷ ts)) → Term Σ Γ Δ t
+ tail : Term Σ Γ Δ (tuple (t ∷ ts)) → Term Σ Γ Δ (tuple ts)
+ if_then_else_ : Term Σ Γ Δ bool → Term Σ Γ Δ t → Term Σ Γ Δ t → Term Σ Γ Δ t
+
+↓_ : Expression Σ Γ t → Term Σ Γ Δ t
+↓ e = go (Flatten.expr e) (Flatten.expr-depth e)
where
- reasoning = slicedSize _ m i
- k = proj₁ reasoning
- n≡i+k = sym (proj₂ (proj₂ reasoning))
- low = take′ t (Fin.toℕ i) (cast′ t n≡i+k y)
- high = drop′ t (Fin.toℕ i) (cast′ t n≡i+k y)
- eq = sym (proj₁ (proj₂ reasoning))
-
-splice : ∀ t → Term Σ Γ Δ (asType t m) → Term Σ Γ Δ (asType t n) → Term Σ Γ Δ (fin (suc n)) → Term Σ Γ Δ (asType t (n ℕ.+ m))
-splice τ t₁ t₂ t′ = func (λ (x , y , i , _) → splice′ τ x y i) (t₁ ∷ t₂ ∷ t′ ∷ [])
-
--- i of x is 0 of first
-cut′ : ∀ t → ⟦ asType t (n ℕ.+ m) ⟧ₜ → ⟦ fin (suc n) ⟧ₜ → ⟦ asType t m ∷ asType t n ∷ [] ⟧ₜ′
-cut′ {m = m} t x (lift i) = middle , cast′ t i+k≡n (join′ t high low) , _
- where
- reasoning = slicedSize _ m i
- k = proj₁ reasoning
- i+k≡n = proj₂ (proj₂ reasoning)
- eq = proj₁ (proj₂ reasoning)
- low = take′ t (Fin.toℕ i) (cast′ t eq x)
- middle = take′ t m (drop′ t (Fin.toℕ i) (cast′ t eq x))
- high = drop′ t m (drop′ t (Fin.toℕ i) (cast′ t eq x))
-
-cut : ∀ t → Term Σ Γ Δ (asType t (n ℕ.+ m)) → Term Σ Γ Δ (fin (suc n)) → Term Σ Γ Δ (tuple _ (asType t m ∷ asType t n ∷ []))
-cut τ t t′ = func₂ (cut′ τ) t t′
-
-flatten : ∀ {ms : Vec ℕ n} → ⟦ Vec.map fin ms ⟧ₜ′ → All Fin ms
-flatten {ms = []} _ = []
-flatten {ms = _ ∷ ms} (lift x , xs) = x ∷ flatten xs
-
-𝒦 : Literal t → Term Σ Γ Δ t
-𝒦 (x ′b) = func₀ (lift x)
-𝒦 (x ′i) = func₀ (lift (x ℤ′.×′ 1ℤ))
-𝒦 (x ′f) = func₀ (lift x)
-𝒦 (x ′r) = func₀ (lift (x ℝ′.×′ 1ℝ))
-𝒦 (x ′x) = func₀ (lift (Bool.if x then 1𝔹 else 0𝔹))
-𝒦 ([] ′xs) = func₀ []
-𝒦 ((x ∷ xs) ′xs) = func₂ (flip Vec._∷ʳ_) (𝒦 (x ′x)) (𝒦 (xs ′xs))
-𝒦 (x ′a) = func₁ Vec.replicate (𝒦 x)
-
-module _ (2≉0 : 2≉0) where
- ℰ : Code.Expression Σ Γ t → Term Σ Γ Δ t
- ℰ e = (uncurry helper) (M.elimFunctions e)
- where
- 1+m⊔n≡1+k : ∀ m n → ∃ λ k → suc m ℕ.⊔ n ≡ suc k
- 1+m⊔n≡1+k m 0 = m , refl
- 1+m⊔n≡1+k m (suc n) = m ℕ.⊔ n , refl
-
- pull-0₂ : ∀ {x y} → x ℕ.⊔ y ≡ 0 → x ≡ 0
- pull-0₂ {0} {0} refl = refl
- pull-0₂ {0} {suc y} ()
-
- pull-0₃ : ∀ {x y z} → x ℕ.⊔ y ℕ.⊔ z ≡ 0 → x ≡ 0
- pull-0₃ {0} {0} {0} refl = refl
- pull-0₃ {0} {suc y} {0} ()
- pull-0₃ {suc x} {0} {0} ()
- pull-0₃ {suc x} {0} {suc z} ()
-
- pull-1₃ : ∀ x {y z} → x ℕ.⊔ y ℕ.⊔ z ≡ 0 → y ≡ 0
- pull-1₃ 0 {0} {0} refl = refl
- pull-1₃ 0 {suc y} {0} ()
- pull-1₃ (suc x) {0} {0} ()
- pull-1₃ (suc x) {0} {suc z} ()
-
- pull-last : ∀ {x y} → x ℕ.⊔ y ≡ 0 → y ≡ 0
- pull-last {0} {0} refl = refl
- pull-last {suc x} {0} ()
-
- helper : ∀ (e : Code.Expression Σ Γ t) → M.callDepth e ≡ 0 → Term Σ Γ Δ t
- helper (Code.lit x) eq = 𝒦 x
- helper (Code.state i) eq = state i
- helper (Code.var i) eq = var i
- helper (Code.abort e) eq = func₁ (λ ()) (helper e eq)
- helper (Code._≟_ {hasEquality = hasEq} e e₁) eq = [ toWitness hasEq ][ helper e (pull-0₂ eq) ≟ helper e₁ (pull-last eq) ]
- helper (Code._<?_ {isNumeric = isNum} e e₁) eq = [ toWitness isNum ][ helper e (pull-0₂ eq) <? helper e₁ (pull-last eq) ]
- helper (Code.inv e) eq = func₁ (lift ∘ Bool.not ∘ lower) (helper e eq)
- helper (e Code.&& e₁) eq = func₂ (λ (lift x) (lift y) → lift (x Bool.∧ y)) (helper e (pull-0₂ eq)) (helper e₁ (pull-last eq))
- helper (e Code.|| e₁) eq = func₂ (λ (lift x) (lift y) → lift (x Bool.∨ y)) (helper e (pull-0₂ eq)) (helper e₁ (pull-last eq))
- helper (Code.not e) eq = func₁ (Vec.map (lift ∘ 𝔹.¬_ ∘ lower)) (helper e eq)
- helper (e Code.and e₁) eq = func₂ (λ xs ys → Vec.zipWith (λ (lift x) (lift y) → lift (x 𝔹.∧ y)) xs ys) (helper e (pull-0₂ eq)) (helper e₁ (pull-last eq))
- helper (e Code.or e₁) eq = func₂ (λ xs ys → Vec.zipWith (λ (lift x) (lift y) → lift (x 𝔹.∨ y)) xs ys) (helper e (pull-0₂ eq)) (helper e₁ (pull-last eq))
- helper (Code.[_] {t = t} e) eq = [ t ][ helper e eq ]
- helper (Code.unbox {t = t} e) eq = unbox t (helper e eq)
- helper (Code.splice {t = t} e e₁ e₂) eq = splice t (helper e (pull-0₃ eq)) (helper e₁ (pull-1₃ (M.callDepth e) eq)) (helper e₂ (pull-last eq))
- helper (Code.cut {t = t} e e₁) eq = cut t (helper e (pull-0₂ eq)) (helper e₁ (pull-last eq))
- helper (Code.cast {t = t} i≡j e) eq = cast t i≡j (helper e eq)
- helper (Code.-_ {isNumeric = isNum} e) eq = [ toWitness isNum ][- helper e eq ]
- helper (Code._+_ {isNumeric₁ = isNum₁} {isNumeric₂ = isNum₂} e e₁) eq = [ _ , _ , isNum₁ , isNum₂ ][ helper e (pull-0₂ eq) + helper e₁ (pull-last eq) ]
- helper (Code._*_ {isNumeric₁ = isNum₁} {isNumeric₂ = isNum₂} e e₁) eq = [ _ , _ , isNum₁ , isNum₂ ][ helper e (pull-0₂ eq) * helper e₁ (pull-last eq) ]
- helper (Code._^_ {isNumeric = isNum} e y) eq = [ toWitness isNum ][ helper e eq ^ y ]
- helper (e Code.>> n) eq = [ 2≉0 ][ helper e eq >> n ]
- helper (Code.rnd e) eq = func₁ (lift ∘ ⌊_⌋ ∘ lower) (helper e eq)
- helper (Code.fin f e) eq = func₁ (lift ∘ f ∘ flatten) (helper e eq)
- helper (Code.asInt e) eq = func₁ (lift ∘ (ℤ′._×′ 1ℤ) ∘ Fin.toℕ ∘ lower) (helper e eq)
- helper Code.nil eq = func₀ _
- helper (Code.cons e e₁) eq = func₂ _,_ (helper e (pull-0₂ eq)) (helper e₁ (pull-last eq))
- helper (Code.head e) eq = func₁ proj₁ (helper e eq)
- helper (Code.tail e) eq = func₁ proj₂ (helper e eq)
- helper (Code.call f es) eq = contradiction (trans (sym eq) (proj₂ (1+m⊔n≡1+k (M.funCallDepth f) (M.callDepth′ es)))) ℕₚ.0≢1+n
- helper (Code.if e then e₁ else e₂) eq = func (λ (lift b , x , x₁ , _) → Bool.if b then x else x₁) (helper e (pull-0₃ eq) ∷ helper e₁ (pull-1₃ (M.callDepth e) eq) ∷ helper e₂ (pull-last eq) ∷ [])
-
- ℰ′ : All (Code.Expression Σ Γ) ts → All (Term Σ Γ Δ) ts
- ℰ′ [] = []
- ℰ′ (e ∷ es) = ℰ e ∷ ℰ′ es
-
- subst : Term Σ Γ Δ t → {e : Code.Expression Σ Γ t′} → Code.CanAssign Σ e → Term Σ Γ Δ t′ → Term Σ Γ Δ t
- subst t (Code.state i) t′ = substState t i t′
- subst t (Code.var i) t′ = substVar t i t′
- subst t (Code.abort e) t′ = func₁ (λ ()) (ℰ e)
- subst t (Code.[_] {t = τ} ref) t′ = subst t ref (unbox τ t′)
- subst t (Code.unbox {t = τ} ref) t′ = subst t ref [ τ ][ t′ ]
- subst t (Code.splice {t = τ} ref ref₁ e₃) t′ = subst (subst t ref (func₁ proj₁ (cut τ t′ (ℰ e₃)))) ref₁ (func₁ (proj₁ ∘ proj₂) (cut τ t′ (ℰ e₃)))
- subst t (Code.cut {t = τ} ref e₂) t′ = subst t ref (splice τ (func₁ proj₁ t′) (func₁ (proj₁ ∘ proj₂) t′) (ℰ e₂))
- subst t (Code.cast {t = τ} eq ref) t′ = subst t ref (cast τ (sym eq) t′)
- subst t Code.nil t′ = t
- subst t (Code.cons ref ref₁) t′ = subst (subst t ref (func₁ proj₁ t′)) ref₁ (func₁ proj₂ t′)
- subst t (Code.head {e = e} ref) t′ = subst t ref (func₂ _,_ t′ (func₁ proj₂ (ℰ e)))
- subst t (Code.tail {t = τ} {e = e} ref) t′ = subst t ref (func₂ {t₁ = τ} _,_ (func₁ proj₁ (ℰ e)) t′)
-
-⟦_⟧ : Term Σ Γ Δ t → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ Δ ⟧ₜ′ → ⟦ t ⟧ₜ
-⟦_⟧′ : ∀ {ts} → All (Term Σ Γ Δ) {n} ts → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ Δ ⟧ₜ′ → ⟦ ts ⟧ₜ′
-
-⟦ state i ⟧ σ γ δ = fetch i σ
-⟦ var i ⟧ σ γ δ = fetch i γ
-⟦ meta i ⟧ σ γ δ = fetch i δ
-⟦ func f ts ⟧ σ γ δ = f (⟦ ts ⟧′ σ γ δ)
-
-⟦ [] ⟧′ σ γ δ = _
-⟦ t ∷ ts ⟧′ σ γ δ = ⟦ t ⟧ σ γ δ , ⟦ ts ⟧′ σ γ δ
+ ⊔-inj : ∀ i xs → ⨆[ n ] xs ≡ 0 → Vecᵣ.lookup i xs ≡ 0
+ ⊔-inj i xs eq = ℕₚ.n≤0⇒n≡0 (ℕₚ.≤-trans (lookup-⨆-≤ i xs) (ℕₚ.≤-reflexive eq))
+
+ go : ∀ (e : Expression Σ Γ t) → CallDepth.expr e ≡ 0 → Term Σ Γ Δ t
+ go (lit {t} x) ≡0 = lit (Κ[ t ] x)
+ go (state i) ≡0 = state i
+ go (var i) ≡0 = var i
+ go (e ≟ e₁) ≡0 = go e (⊔-inj 0F (CallDepth.expr e , CallDepth.expr e₁) ≡0) ≟ go e₁ (⊔-inj 1F (CallDepth.expr e , CallDepth.expr e₁) ≡0)
+ go (e <? e₁) ≡0 = go e (⊔-inj 0F (CallDepth.expr e , CallDepth.expr e₁) ≡0) <? go e₁ (⊔-inj 1F (CallDepth.expr e , CallDepth.expr e₁) ≡0)
+ go (inv e) ≡0 = inv (go e ≡0)
+ go (e && e₁) ≡0 = go e (⊔-inj 0F (CallDepth.expr e , CallDepth.expr e₁) ≡0) && go e₁ (⊔-inj 1F (CallDepth.expr e , CallDepth.expr e₁) ≡0)
+ go (e || e₁) ≡0 = go e (⊔-inj 0F (CallDepth.expr e , CallDepth.expr e₁) ≡0) || go e₁ (⊔-inj 1F (CallDepth.expr e , CallDepth.expr e₁) ≡0)
+ go (not e) ≡0 = not (go e ≡0)
+ go (e and e₁) ≡0 = go e (⊔-inj 0F (CallDepth.expr e , CallDepth.expr e₁) ≡0) and go e₁ (⊔-inj 1F (CallDepth.expr e , CallDepth.expr e₁) ≡0)
+ go (e or e₁) ≡0 = go e (⊔-inj 0F (CallDepth.expr e , CallDepth.expr e₁) ≡0) or go e₁ (⊔-inj 1F (CallDepth.expr e , CallDepth.expr e₁) ≡0)
+ go [ e ] ≡0 = [ go e ≡0 ]
+ go (unbox e) ≡0 = unbox (go e ≡0)
+ go (merge e e₁ e₂) ≡0 = merge (go e (⊔-inj 0F (CallDepth.expr e , CallDepth.expr e₁ , CallDepth.expr e₂) ≡0)) (go e₁ (⊔-inj 1F (CallDepth.expr e , CallDepth.expr e₁ , CallDepth.expr e₂) ≡0)) (go e₂ (⊔-inj 2F (CallDepth.expr e , CallDepth.expr e₁ , CallDepth.expr e₂) ≡0))
+ go (slice e e₁) ≡0 = slice (go e (⊔-inj 0F (CallDepth.expr e , CallDepth.expr e₁) ≡0)) (go e₁ (⊔-inj 1F (CallDepth.expr e , CallDepth.expr e₁) ≡0))
+ go (cut e e₁) ≡0 = cut (go e (⊔-inj 0F (CallDepth.expr e , CallDepth.expr e₁) ≡0)) (go e₁ (⊔-inj 1F (CallDepth.expr e , CallDepth.expr e₁) ≡0))
+ go (cast eq e) ≡0 = cast eq (go e ≡0)
+ go (- e) ≡0 = - go e ≡0
+ go (e + e₁) ≡0 = go e (⊔-inj 0F (CallDepth.expr e , CallDepth.expr e₁) ≡0) + go e₁ (⊔-inj 1F (CallDepth.expr e , CallDepth.expr e₁) ≡0)
+ go (e * e₁) ≡0 = go e (⊔-inj 0F (CallDepth.expr e , CallDepth.expr e₁) ≡0) * go e₁ (⊔-inj 1F (CallDepth.expr e , CallDepth.expr e₁) ≡0)
+ go (e ^ x) ≡0 = go e ≡0 ^ x
+ go (e >> n) ≡0 = go e ≡0 >> n
+ go (rnd e) ≡0 = rnd (go e ≡0)
+ go (fin f e) ≡0 = fin f (go e ≡0)
+ go (asInt e) ≡0 = asInt (go e ≡0)
+ go nil ≡0 = nil
+ go (cons e e₁) ≡0 = cons (go e (⊔-inj 0F (CallDepth.expr e , CallDepth.expr e₁) ≡0)) (go e₁ (⊔-inj 1F (CallDepth.expr e , CallDepth.expr e₁) ≡0))
+ go (head e) ≡0 = head (go e ≡0)
+ go (tail e) ≡0 = tail (go e ≡0)
+ go (call f es) ≡0 = ⊥-elim (ℕₚ.>⇒≢ (CallDepth.call>0 f es) ≡0)
+ go (if e then e₁ else e₂) ≡0 = if go e (⊔-inj 0F (CallDepth.expr e , CallDepth.expr e₁ , CallDepth.expr e₂) ≡0) then go e₁ (⊔-inj 1F (CallDepth.expr e , CallDepth.expr e₁ , CallDepth.expr e₂) ≡0) else go e₂ (⊔-inj 2F (CallDepth.expr e , CallDepth.expr e₁ , CallDepth.expr e₂) ≡0)
+
+module Cast where
+ type : t ≡ t′ → Term Σ Γ Δ t → Term Σ Γ Δ t′
+ type refl = id
+
+module State where
+ subst : ∀ i → Term Σ Γ Δ t → Term Σ Γ Δ (lookup Σ i) → Term Σ Γ Δ t
+ subst i (lit x) e′ = lit x
+ subst i (state j) e′ with i Fin.≟ j
+ ... | yes refl = e′
+ ... | no i≢j = state j
+ subst i (var j) e′ = var j
+ subst i (meta j) e′ = meta j
+ subst i (e ≟ e₁) e′ = subst i e e′ ≟ subst i e₁ e′
+ subst i (e <? e₁) e′ = subst i e e′ <? subst i e₁ e′
+ subst i (inv e) e′ = inv (subst i e e′)
+ subst i (e && e₁) e′ = subst i e e′ && subst i e₁ e′
+ subst i (e || e₁) e′ = subst i e e′ || subst i e₁ e′
+ subst i (not e) e′ = not (subst i e e′)
+ subst i (e and e₁) e′ = subst i e e′ and subst i e₁ e′
+ subst i (e or e₁) e′ = subst i e e′ or subst i e₁ e′
+ subst i [ e ] e′ = [ subst i e e′ ]
+ subst i (unbox e) e′ = unbox (subst i e e′)
+ subst i (merge e e₁ e₂) e′ = merge (subst i e e′) (subst i e₁ e′) (subst i e₂ e′)
+ subst i (slice e e₁) e′ = slice (subst i e e′) (subst i e₁ e′)
+ subst i (cut e e₁) e′ = cut (subst i e e′) (subst i e₁ e′)
+ subst i (cast eq e) e′ = cast eq (subst i e e′)
+ subst i (- e) e′ = - subst i e e′
+ subst i (e + e₁) e′ = subst i e e′ + subst i e₁ e′
+ subst i (e * e₁) e′ = subst i e e′ * subst i e₁ e′
+ subst i (e ^ x) e′ = subst i e e′ ^ x
+ subst i (e >> n) e′ = subst i e e′ >> n
+ subst i (rnd e) e′ = rnd (subst i e e′)
+ subst i (fin f e) e′ = fin f (subst i e e′)
+ subst i (asInt e) e′ = asInt (subst i e e′)
+ subst i nil e′ = nil
+ subst i (cons e e₁) e′ = cons (subst i e e′) (subst i e₁ e′)
+ subst i (head e) e′ = head (subst i e e′)
+ subst i (tail e) e′ = tail (subst i e e′)
+ subst i (if e then e₁ else e₂) e′ = if subst i e e′ then subst i e₁ e′ else subst i e₂ e′
+
+module Var {Γ : Vec Type o} where
+ weaken : ∀ i → Term Σ Γ Δ t → Term Σ (insert Γ i t′) Δ t
+ weaken i (lit x) = lit x
+ weaken i (state j) = state j
+ weaken i (var j) = Cast.type (Vecₚ.insert-punchIn _ i _ j) (var (Fin.punchIn i j))
+ weaken i (meta j) = meta j
+ weaken i (e ≟ e₁) = weaken i e ≟ weaken i e₁
+ weaken i (e <? e₁) = weaken i e <? weaken i e₁
+ weaken i (inv e) = inv (weaken i e)
+ weaken i (e && e₁) = weaken i e && weaken i e₁
+ weaken i (e || e₁) = weaken i e || weaken i e₁
+ weaken i (not e) = not (weaken i e)
+ weaken i (e and e₁) = weaken i e and weaken i e₁
+ weaken i (e or e₁) = weaken i e or weaken i e₁
+ weaken i [ e ] = [ weaken i e ]
+ weaken i (unbox e) = unbox (weaken i e)
+ weaken i (merge e e₁ e₂) = merge (weaken i e) (weaken i e₁) (weaken i e₂)
+ weaken i (slice e e₁) = slice (weaken i e) (weaken i e₁)
+ weaken i (cut e e₁) = cut (weaken i e) (weaken i e₁)
+ weaken i (cast eq e) = cast eq (weaken i e)
+ weaken i (- e) = - weaken i e
+ weaken i (e + e₁) = weaken i e + weaken i e₁
+ weaken i (e * e₁) = weaken i e * weaken i e₁
+ weaken i (e ^ x) = weaken i e ^ x
+ weaken i (e >> n) = weaken i e >> n
+ weaken i (rnd e) = rnd (weaken i e)
+ weaken i (fin f e) = fin f (weaken i e)
+ weaken i (asInt e) = asInt (weaken i e)
+ weaken i nil = nil
+ weaken i (cons e e₁) = cons (weaken i e) (weaken i e₁)
+ weaken i (head e) = head (weaken i e)
+ weaken i (tail e) = tail (weaken i e)
+ weaken i (if e then e₁ else e₂) = if weaken i e then weaken i e₁ else weaken i e₂
+
+ weakenAll : Term Σ [] Δ t → Term Σ Γ Δ t
+ weakenAll (lit x) = lit x
+ weakenAll (state j) = state j
+ weakenAll (meta j) = meta j
+ weakenAll (e ≟ e₁) = weakenAll e ≟ weakenAll e₁
+ weakenAll (e <? e₁) = weakenAll e <? weakenAll e₁
+ weakenAll (inv e) = inv (weakenAll e)
+ weakenAll (e && e₁) = weakenAll e && weakenAll e₁
+ weakenAll (e || e₁) = weakenAll e || weakenAll e₁
+ weakenAll (not e) = not (weakenAll e)
+ weakenAll (e and e₁) = weakenAll e and weakenAll e₁
+ weakenAll (e or e₁) = weakenAll e or weakenAll e₁
+ weakenAll [ e ] = [ weakenAll e ]
+ weakenAll (unbox e) = unbox (weakenAll e)
+ weakenAll (merge e e₁ e₂) = merge (weakenAll e) (weakenAll e₁) (weakenAll e₂)
+ weakenAll (slice e e₁) = slice (weakenAll e) (weakenAll e₁)
+ weakenAll (cut e e₁) = cut (weakenAll e) (weakenAll e₁)
+ weakenAll (cast eq e) = cast eq (weakenAll e)
+ weakenAll (- e) = - weakenAll e
+ weakenAll (e + e₁) = weakenAll e + weakenAll e₁
+ weakenAll (e * e₁) = weakenAll e * weakenAll e₁
+ weakenAll (e ^ x) = weakenAll e ^ x
+ weakenAll (e >> n) = weakenAll e >> n
+ weakenAll (rnd e) = rnd (weakenAll e)
+ weakenAll (fin f e) = fin f (weakenAll e)
+ weakenAll (asInt e) = asInt (weakenAll e)
+ weakenAll nil = nil
+ weakenAll (cons e e₁) = cons (weakenAll e) (weakenAll e₁)
+ weakenAll (head e) = head (weakenAll e)
+ weakenAll (tail e) = tail (weakenAll e)
+ weakenAll (if e then e₁ else e₂) = if weakenAll e then weakenAll e₁ else weakenAll e₂
+
+ inject : ∀ (ts : Vec Type n) → Term Σ Γ Δ t → Term Σ (Γ ++ ts) Δ t
+ inject ts (lit x) = lit x
+ inject ts (state j) = state j
+ inject ts (var j) = Cast.type (Vecₚ.lookup-++ˡ Γ ts j) (var (Fin.inject+ _ j))
+ inject ts (meta j) = meta j
+ inject ts (e ≟ e₁) = inject ts e ≟ inject ts e₁
+ inject ts (e <? e₁) = inject ts e <? inject ts e₁
+ inject ts (inv e) = inv (inject ts e)
+ inject ts (e && e₁) = inject ts e && inject ts e₁
+ inject ts (e || e₁) = inject ts e || inject ts e₁
+ inject ts (not e) = not (inject ts e)
+ inject ts (e and e₁) = inject ts e and inject ts e₁
+ inject ts (e or e₁) = inject ts e or inject ts e₁
+ inject ts [ e ] = [ inject ts e ]
+ inject ts (unbox e) = unbox (inject ts e)
+ inject ts (merge e e₁ e₂) = merge (inject ts e) (inject ts e₁) (inject ts e₂)
+ inject ts (slice e e₁) = slice (inject ts e) (inject ts e₁)
+ inject ts (cut e e₁) = cut (inject ts e) (inject ts e₁)
+ inject ts (cast eq e) = cast eq (inject ts e)
+ inject ts (- e) = - inject ts e
+ inject ts (e + e₁) = inject ts e + inject ts e₁
+ inject ts (e * e₁) = inject ts e * inject ts e₁
+ inject ts (e ^ x) = inject ts e ^ x
+ inject ts (e >> n) = inject ts e >> n
+ inject ts (rnd e) = rnd (inject ts e)
+ inject ts (fin f e) = fin f (inject ts e)
+ inject ts (asInt e) = asInt (inject ts e)
+ inject ts nil = nil
+ inject ts (cons e e₁) = cons (inject ts e) (inject ts e₁)
+ inject ts (head e) = head (inject ts e)
+ inject ts (tail e) = tail (inject ts e)
+ inject ts (if e then e₁ else e₂) = if inject ts e then inject ts e₁ else inject ts e₂
+
+ raise : ∀ (ts : Vec Type n) → Term Σ Γ Δ t → Term Σ (ts ++ Γ) Δ t
+ raise ts (lit x) = lit x
+ raise ts (state j) = state j
+ raise ts (var j) = Cast.type (Vecₚ.lookup-++ʳ ts Γ j) (var (Fin.raise _ j))
+ raise ts (meta j) = meta j
+ raise ts (e ≟ e₁) = raise ts e ≟ raise ts e₁
+ raise ts (e <? e₁) = raise ts e <? raise ts e₁
+ raise ts (inv e) = inv (raise ts e)
+ raise ts (e && e₁) = raise ts e && raise ts e₁
+ raise ts (e || e₁) = raise ts e || raise ts e₁
+ raise ts (not e) = not (raise ts e)
+ raise ts (e and e₁) = raise ts e and raise ts e₁
+ raise ts (e or e₁) = raise ts e or raise ts e₁
+ raise ts [ e ] = [ raise ts e ]
+ raise ts (unbox e) = unbox (raise ts e)
+ raise ts (merge e e₁ e₂) = merge (raise ts e) (raise ts e₁) (raise ts e₂)
+ raise ts (slice e e₁) = slice (raise ts e) (raise ts e₁)
+ raise ts (cut e e₁) = cut (raise ts e) (raise ts e₁)
+ raise ts (cast eq e) = cast eq (raise ts e)
+ raise ts (- e) = - raise ts e
+ raise ts (e + e₁) = raise ts e + raise ts e₁
+ raise ts (e * e₁) = raise ts e * raise ts e₁
+ raise ts (e ^ x) = raise ts e ^ x
+ raise ts (e >> n) = raise ts e >> n
+ raise ts (rnd e) = rnd (raise ts e)
+ raise ts (fin f e) = fin f (raise ts e)
+ raise ts (asInt e) = asInt (raise ts e)
+ raise ts nil = nil
+ raise ts (cons e e₁) = cons (raise ts e) (raise ts e₁)
+ raise ts (head e) = head (raise ts e)
+ raise ts (tail e) = tail (raise ts e)
+ raise ts (if e then e₁ else e₂) = if raise ts e then raise ts e₁ else raise ts e₂
+
+ elim : ∀ i → Term Σ (insert Γ i t′) Δ t → Term Σ Γ Δ t′ → Term Σ Γ Δ t
+ elim i (lit x) e′ = lit x
+ elim i (state j) e′ = state j
+ elim i (var j) e′ with i Fin.≟ j
+ ... | yes refl = Cast.type (sym (Vecₚ.insert-lookup Γ i _)) e′
+ ... | no i≢j = Cast.type (punchOut-insert Γ i≢j _) (var (Fin.punchOut i≢j))
+ elim i (meta j) e′ = meta j
+ elim i (e ≟ e₁) e′ = elim i e e′ ≟ elim i e₁ e′
+ elim i (e <? e₁) e′ = elim i e e′ <? elim i e₁ e′
+ elim i (inv e) e′ = inv (elim i e e′)
+ elim i (e && e₁) e′ = elim i e e′ && elim i e₁ e′
+ elim i (e || e₁) e′ = elim i e e′ || elim i e₁ e′
+ elim i (not e) e′ = not (elim i e e′)
+ elim i (e and e₁) e′ = elim i e e′ and elim i e₁ e′
+ elim i (e or e₁) e′ = elim i e e′ or elim i e₁ e′
+ elim i [ e ] e′ = [ elim i e e′ ]
+ elim i (unbox e) e′ = unbox (elim i e e′)
+ elim i (merge e e₁ e₂) e′ = merge (elim i e e′) (elim i e₁ e′) (elim i e₂ e′)
+ elim i (slice e e₁) e′ = slice (elim i e e′) (elim i e₁ e′)
+ elim i (cut e e₁) e′ = cut (elim i e e′) (elim i e₁ e′)
+ elim i (cast eq e) e′ = cast eq (elim i e e′)
+ elim i (- e) e′ = - elim i e e′
+ elim i (e + e₁) e′ = elim i e e′ + elim i e₁ e′
+ elim i (e * e₁) e′ = elim i e e′ * elim i e₁ e′
+ elim i (e ^ x) e′ = elim i e e′ ^ x
+ elim i (e >> n) e′ = elim i e e′ >> n
+ elim i (rnd e) e′ = rnd (elim i e e′)
+ elim i (fin f e) e′ = fin f (elim i e e′)
+ elim i (asInt e) e′ = asInt (elim i e e′)
+ elim i nil e′ = nil
+ elim i (cons e e₁) e′ = cons (elim i e e′) (elim i e₁ e′)
+ elim i (head e) e′ = head (elim i e e′)
+ elim i (tail e) e′ = tail (elim i e e′)
+ elim i (if e then e₁ else e₂) e′ = if elim i e e′ then elim i e₁ e′ else elim i e₂ e′
+
+ elimAll : Term Σ Γ Δ t → All (Term Σ ts Δ) Γ → Term Σ ts Δ t
+ elimAll (lit x) es = lit x
+ elimAll (state j) es = state j
+ elimAll (var j) es = All.lookup j es
+ elimAll (meta j) es = meta j
+ elimAll (e ≟ e₁) es = elimAll e es ≟ elimAll e₁ es
+ elimAll (e <? e₁) es = elimAll e es <? elimAll e₁ es
+ elimAll (inv e) es = inv (elimAll e es)
+ elimAll (e && e₁) es = elimAll e es && elimAll e₁ es
+ elimAll (e || e₁) es = elimAll e es || elimAll e₁ es
+ elimAll (not e) es = not (elimAll e es)
+ elimAll (e and e₁) es = elimAll e es and elimAll e₁ es
+ elimAll (e or e₁) es = elimAll e es or elimAll e₁ es
+ elimAll [ e ] es = [ elimAll e es ]
+ elimAll (unbox e) es = unbox (elimAll e es)
+ elimAll (merge e e₁ e₂) es = merge (elimAll e es) (elimAll e₁ es) (elimAll e₂ es)
+ elimAll (slice e e₁) es = slice (elimAll e es) (elimAll e₁ es)
+ elimAll (cut e e₁) es = cut (elimAll e es) (elimAll e₁ es)
+ elimAll (cast eq e) es = cast eq (elimAll e es)
+ elimAll (- e) es = - elimAll e es
+ elimAll (e + e₁) es = elimAll e es + elimAll e₁ es
+ elimAll (e * e₁) es = elimAll e es * elimAll e₁ es
+ elimAll (e ^ x) es = elimAll e es ^ x
+ elimAll (e >> n) es = elimAll e es >> n
+ elimAll (rnd e) es = rnd (elimAll e es)
+ elimAll (fin f e) es = fin f (elimAll e es)
+ elimAll (asInt e) es = asInt (elimAll e es)
+ elimAll nil es = nil
+ elimAll (cons e e₁) es = cons (elimAll e es) (elimAll e₁ es)
+ elimAll (head e) es = head (elimAll e es)
+ elimAll (tail e) es = tail (elimAll e es)
+ elimAll (if e then e₁ else e₂) es = if elimAll e es then elimAll e₁ es else elimAll e₂ es
+
+ subst : ∀ i → Term Σ Γ Δ t → Term Σ Γ Δ (lookup Γ i) → Term Σ Γ Δ t
+ subst i (lit x) e′ = lit x
+ subst i (state j) e′ = state j
+ subst i (var j) e′ with i Fin.≟ j
+ ... | yes refl = e′
+ ... | no i≢j = var j
+ subst i (meta j) e′ = meta j
+ subst i (e ≟ e₁) e′ = subst i e e′ ≟ subst i e₁ e′
+ subst i (e <? e₁) e′ = subst i e e′ <? subst i e₁ e′
+ subst i (inv e) e′ = inv (subst i e e′)
+ subst i (e && e₁) e′ = subst i e e′ && subst i e₁ e′
+ subst i (e || e₁) e′ = subst i e e′ || subst i e₁ e′
+ subst i (not e) e′ = not (subst i e e′)
+ subst i (e and e₁) e′ = subst i e e′ and subst i e₁ e′
+ subst i (e or e₁) e′ = subst i e e′ or subst i e₁ e′
+ subst i [ e ] e′ = [ subst i e e′ ]
+ subst i (unbox e) e′ = unbox (subst i e e′)
+ subst i (merge e e₁ e₂) e′ = merge (subst i e e′) (subst i e₁ e′) (subst i e₂ e′)
+ subst i (slice e e₁) e′ = slice (subst i e e′) (subst i e₁ e′)
+ subst i (cut e e₁) e′ = cut (subst i e e′) (subst i e₁ e′)
+ subst i (cast eq e) e′ = cast eq (subst i e e′)
+ subst i (- e) e′ = - subst i e e′
+ subst i (e + e₁) e′ = subst i e e′ + subst i e₁ e′
+ subst i (e * e₁) e′ = subst i e e′ * subst i e₁ e′
+ subst i (e ^ x) e′ = subst i e e′ ^ x
+ subst i (e >> n) e′ = subst i e e′ >> n
+ subst i (rnd e) e′ = rnd (subst i e e′)
+ subst i (fin f e) e′ = fin f (subst i e e′)
+ subst i (asInt e) e′ = asInt (subst i e e′)
+ subst i nil e′ = nil
+ subst i (cons e e₁) e′ = cons (subst i e e′) (subst i e₁ e′)
+ subst i (head e) e′ = head (subst i e e′)
+ subst i (tail e) e′ = tail (subst i e e′)
+ subst i (if e then e₁ else e₂) e′ = if subst i e e′ then subst i e₁ e′ else subst i e₂ e′
+
+module Meta {Δ : Vec Type o} where
+ weaken : ∀ i → Term Σ Γ Δ t → Term Σ Γ (insert Δ i t′) t
+ weaken i (lit x) = lit x
+ weaken i (state j) = state j
+ weaken i (var j) = var j
+ weaken i (meta j) = Cast.type (Vecₚ.insert-punchIn _ i _ j) (meta (Fin.punchIn i j))
+ weaken i (e ≟ e₁) = weaken i e ≟ weaken i e₁
+ weaken i (e <? e₁) = weaken i e <? weaken i e₁
+ weaken i (inv e) = inv (weaken i e)
+ weaken i (e && e₁) = weaken i e && weaken i e₁
+ weaken i (e || e₁) = weaken i e || weaken i e₁
+ weaken i (not e) = not (weaken i e)
+ weaken i (e and e₁) = weaken i e and weaken i e₁
+ weaken i (e or e₁) = weaken i e or weaken i e₁
+ weaken i [ e ] = [ weaken i e ]
+ weaken i (unbox e) = unbox (weaken i e)
+ weaken i (merge e e₁ e₂) = merge (weaken i e) (weaken i e₁) (weaken i e₂)
+ weaken i (slice e e₁) = slice (weaken i e) (weaken i e₁)
+ weaken i (cut e e₁) = cut (weaken i e) (weaken i e₁)
+ weaken i (cast eq e) = cast eq (weaken i e)
+ weaken i (- e) = - weaken i e
+ weaken i (e + e₁) = weaken i e + weaken i e₁
+ weaken i (e * e₁) = weaken i e * weaken i e₁
+ weaken i (e ^ x) = weaken i e ^ x
+ weaken i (e >> n) = weaken i e >> n
+ weaken i (rnd e) = rnd (weaken i e)
+ weaken i (fin f e) = fin f (weaken i e)
+ weaken i (asInt e) = asInt (weaken i e)
+ weaken i nil = nil
+ weaken i (cons e e₁) = cons (weaken i e) (weaken i e₁)
+ weaken i (head e) = head (weaken i e)
+ weaken i (tail e) = tail (weaken i e)
+ weaken i (if e then e₁ else e₂) = if weaken i e then weaken i e₁ else weaken i e₂
+
+ elim : ∀ i → Term Σ Γ (insert Δ i t′) t → Term Σ Γ Δ t′ → Term Σ Γ Δ t
+ elim i (lit x) e′ = lit x
+ elim i (state j) e′ = state j
+ elim i (var j) e′ = var j
+ elim i (meta j) e′ with i Fin.≟ j
+ ... | yes refl = Cast.type (sym (Vecₚ.insert-lookup Δ i _)) e′
+ ... | no i≢j = Cast.type (punchOut-insert Δ i≢j _) (meta (Fin.punchOut i≢j))
+ elim i (e ≟ e₁) e′ = elim i e e′ ≟ elim i e₁ e′
+ elim i (e <? e₁) e′ = elim i e e′ <? elim i e₁ e′
+ elim i (inv e) e′ = inv (elim i e e′)
+ elim i (e && e₁) e′ = elim i e e′ && elim i e₁ e′
+ elim i (e || e₁) e′ = elim i e e′ || elim i e₁ e′
+ elim i (not e) e′ = not (elim i e e′)
+ elim i (e and e₁) e′ = elim i e e′ and elim i e₁ e′
+ elim i (e or e₁) e′ = elim i e e′ or elim i e₁ e′
+ elim i [ e ] e′ = [ elim i e e′ ]
+ elim i (unbox e) e′ = unbox (elim i e e′)
+ elim i (merge e e₁ e₂) e′ = merge (elim i e e′) (elim i e₁ e′) (elim i e₂ e′)
+ elim i (slice e e₁) e′ = slice (elim i e e′) (elim i e₁ e′)
+ elim i (cut e e₁) e′ = cut (elim i e e′) (elim i e₁ e′)
+ elim i (cast eq e) e′ = cast eq (elim i e e′)
+ elim i (- e) e′ = - elim i e e′
+ elim i (e + e₁) e′ = elim i e e′ + elim i e₁ e′
+ elim i (e * e₁) e′ = elim i e e′ * elim i e₁ e′
+ elim i (e ^ x) e′ = elim i e e′ ^ x
+ elim i (e >> n) e′ = elim i e e′ >> n
+ elim i (rnd e) e′ = rnd (elim i e e′)
+ elim i (fin f e) e′ = fin f (elim i e e′)
+ elim i (asInt e) e′ = asInt (elim i e e′)
+ elim i nil e′ = nil
+ elim i (cons e e₁) e′ = cons (elim i e e′) (elim i e₁ e′)
+ elim i (head e) e′ = head (elim i e e′)
+ elim i (tail e) e′ = tail (elim i e e′)
+ elim i (if e then e₁ else e₂) e′ = if elim i e e′ then elim i e₁ e′ else elim i e₂ e′
+
+subst : Term Σ Γ Δ t → Reference Σ Γ t′ → Term Σ Γ Δ t′ → Term Σ Γ Δ t
+subst e (state i) val = State.subst i e val
+subst e (var i) val = Var.subst i e val
+subst e [ ref ] val = subst e ref (unbox val)
+subst e (unbox ref) val = subst e ref [ val ]
+subst e (merge ref ref₁ x) val = subst (subst e ref (slice val (↓ x))) ref₁ (cut val (↓ x))
+subst e (slice ref x) val = subst e ref (merge val (↓ ! cut ref x) (↓ x))
+subst e (cut ref x) val = subst e ref (merge (↓ ! slice ref x) val (↓ x))
+subst e (cast eq ref) val = subst e ref (cast (sym eq) val)
+subst e nil val = e
+subst e (cons ref ref₁) val = subst (subst e ref (head val)) ref₁ (tail val)
+subst e (head ref) val = subst e ref (cons val (↓ ! tail ref))
+subst e (tail ref) val = subst e ref (cons (↓ ! head ref) val)
+
+module Semantics (2≉0 : 2≉0) {Σ : Vec Type i} {Γ : Vec Type j} {Δ : Vec Type k} where
+ ⟦_⟧ : Term Σ Γ Δ t → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ Δ ⟧ₜ′ → ⟦ t ⟧ₜ
+ ⟦ lit x ⟧ σ γ δ = x
+ ⟦ state i ⟧ σ γ δ = fetch i Σ σ
+ ⟦ var i ⟧ σ γ δ = fetch i Γ γ
+ ⟦ meta i ⟧ σ γ δ = fetch i Δ δ
+ ⟦ e ≟ e₁ ⟧ σ γ δ = (lift ∘₂ does ∘₂ ≈-dec) (⟦ e ⟧ σ γ δ) (⟦ e₁ ⟧ σ γ δ)
+ ⟦ e <? e₁ ⟧ σ γ δ = (lift ∘₂ does ∘₂ <-dec) (⟦ e ⟧ σ γ δ) (⟦ e₁ ⟧ σ γ δ)
+ ⟦ inv e ⟧ σ γ δ = lift ∘ Bool.not ∘ lower $ ⟦ e ⟧ σ γ δ
+ ⟦ e && e₁ ⟧ σ γ δ = (lift ∘₂ Bool._∧_ on lower) (⟦ e ⟧ σ γ δ) (⟦ e₁ ⟧ σ γ δ)
+ ⟦ e || e₁ ⟧ σ γ δ = (lift ∘₂ Bool._∨_ on lower) (⟦ e ⟧ σ γ δ) (⟦ e₁ ⟧ σ γ δ)
+ ⟦ not e ⟧ σ γ δ = map (lift ∘ 𝔹.¬_ ∘ lower) (⟦ e ⟧ σ γ δ)
+ ⟦ e and e₁ ⟧ σ γ δ = zipWith (lift ∘₂ 𝔹._∧_ on lower) (⟦ e ⟧ σ γ δ) (⟦ e₁ ⟧ σ γ δ)
+ ⟦ e or e₁ ⟧ σ γ δ = zipWith (lift ∘₂ 𝔹._∨_ on lower) (⟦ e ⟧ σ γ δ) (⟦ e₁ ⟧ σ γ δ)
+ ⟦ [ e ] ⟧ σ γ δ = ⟦ e ⟧ σ γ δ ∷ []
+ ⟦ unbox e ⟧ σ γ δ = Vec.head (⟦ e ⟧ σ γ δ)
+ ⟦ merge e e₁ e₂ ⟧ σ γ δ = mergeVec (⟦ e ⟧ σ γ δ) (⟦ e₁ ⟧ σ γ δ) (lower (⟦ e₂ ⟧ σ γ δ))
+ ⟦ slice e e₁ ⟧ σ γ δ = sliceVec (⟦ e ⟧ σ γ δ) (lower (⟦ e₁ ⟧ σ γ δ))
+ ⟦ cut e e₁ ⟧ σ γ δ = cutVec (⟦ e ⟧ σ γ δ) (lower (⟦ e₁ ⟧ σ γ δ))
+ ⟦ cast eq e ⟧ σ γ δ = castVec eq (⟦ e ⟧ σ γ δ)
+ ⟦ - e ⟧ σ γ δ = neg (⟦ e ⟧ σ γ δ)
+ ⟦ e + e₁ ⟧ σ γ δ = add (⟦ e ⟧ σ γ δ) (⟦ e₁ ⟧ σ γ δ)
+ ⟦ e * e₁ ⟧ σ γ δ = mul (⟦ e ⟧ σ γ δ) (⟦ e₁ ⟧ σ γ δ)
+ ⟦ e ^ x ⟧ σ γ δ = pow (⟦ e ⟧ σ γ δ) x
+ ⟦ e >> n ⟧ σ γ δ = lift ∘ flip (shift 2≉0) n ∘ lower $ ⟦ e ⟧ σ γ δ
+ ⟦ rnd e ⟧ σ γ δ = lift ∘ ⌊_⌋ ∘ lower $ ⟦ e ⟧ σ γ δ
+ ⟦ fin {ms = ms} f e ⟧ σ γ δ = lift ∘ f ∘ lowerFin ms $ ⟦ e ⟧ σ γ δ
+ ⟦ asInt e ⟧ σ γ δ = lift ∘ 𝕀⇒ℤ ∘ 𝕀.+_ ∘ Fin.toℕ ∘ lower $ ⟦ e ⟧ σ γ δ
+ ⟦ nil ⟧ σ γ δ = _
+ ⟦ cons {ts = ts} e e₁ ⟧ σ γ δ = cons′ ts (⟦ e ⟧ σ γ δ) (⟦ e₁ ⟧ σ γ δ)
+ ⟦ head {ts = ts} e ⟧ σ γ δ = head′ ts (⟦ e ⟧ σ γ δ)
+ ⟦ tail {ts = ts} e ⟧ σ γ δ = tail′ ts (⟦ e ⟧ σ γ δ)
+ ⟦ if e then e₁ else e₂ ⟧ σ γ δ = Bool.if lower (⟦ e ⟧ σ γ δ) then ⟦ e₁ ⟧ σ γ δ else ⟦ e₂ ⟧ σ γ δ
diff --git a/src/Helium/Semantics/Axiomatic/Triple.agda b/src/Helium/Semantics/Axiomatic/Triple.agda
index 23a487e..8c6b45a 100644
--- a/src/Helium/Semantics/Axiomatic/Triple.agda
+++ b/src/Helium/Semantics/Axiomatic/Triple.agda
@@ -7,40 +7,61 @@
{-# OPTIONS --safe --without-K #-}
open import Helium.Data.Pseudocode.Algebra using (RawPseudocode)
+import Helium.Semantics.Core as Core
module Helium.Semantics.Axiomatic.Triple
{b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃}
(rawPseudocode : RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃)
+ (2≉0 : Core.2≉0 rawPseudocode)
where
private
open module C = RawPseudocode rawPseudocode
import Data.Bool as Bool
-import Data.Fin as Fin
+open import Data.Fin using (fromℕ; suc; inject₁)
open import Data.Fin.Patterns
-open import Data.Nat using (suc)
+open import Data.Nat using (ℕ; suc)
open import Data.Vec using (Vec; _∷_)
+open import Data.Vec.Relation.Unary.All as All using (All)
open import Function using (_∘_)
open import Helium.Data.Pseudocode.Core
open import Helium.Semantics.Axiomatic.Assertion rawPseudocode as Asrt
-open import Helium.Semantics.Axiomatic.Term rawPseudocode as Term using (var; meta; func₀; func₁; 𝒦; ℰ; ℰ′)
+open import Helium.Semantics.Axiomatic.Term rawPseudocode as Term using (↓_)
open import Level using (_⊔_; lift; lower) renaming (suc to ℓsuc)
open import Relation.Nullary.Decidable.Core using (toWitness)
-open import Relation.Unary using (_⊆′_)
-
-module _ (2≉0 : Term.2≉0) {o} {Σ : Vec Type o} where
- open Code Σ
- data HoareTriple {n} {Γ : Vec Type n} {m} {Δ : Vec Type m} : Assertion Σ Γ Δ → Statement Γ → Assertion Σ Γ Δ → Set (ℓsuc (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 (subst 2≉0 P (toWitness canAssign) (ℰ 2≉0 e)) (_≔_ {t = t} ref {canAssign} e) P
- declare : ∀ {t P Q e s} → HoareTriple (P ∧ equal (var 0F) (Term.wknVar (ℰ 2≉0 e))) s (Asrt.wknVar Q) → HoareTriple (Asrt.elimVar P (ℰ 2≉0 e)) (declare {t = t} e s) Q
- invoke : ∀ {m ts P Q s es} → HoareTriple P s (Asrt.addVars Q) → HoareTriple (Asrt.substVars P (ℰ′ 2≉0 es)) (invoke {m = m} {ts} (s ∙end) es) (Asrt.addVars Q)
- if : ∀ {P Q e s} → HoareTriple (P ∧ equal (ℰ 2≉0 e) (𝒦 (Bool.true ′b))) s Q → HoareTriple (P ∧ equal (ℰ 2≉0 e) (𝒦 (Bool.false ′b))) skip Q → HoareTriple P (if e then s) Q
- if-else : ∀ {P Q e s₁ s₂} → HoareTriple (P ∧ equal (ℰ 2≉0 e) (𝒦 (Bool.true ′b))) s₁ Q → HoareTriple (P ∧ equal (ℰ 2≉0 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 (Asrt.wknVar (Asrt.wknMetaAt 1F I) ∧ equal (meta 1F) (var 0F) ∧ equal (meta 0F) (func₁ (lift ∘ Fin.inject₁ ∘ lower) (meta 1F)))) s (some (Asrt.wknVar (Asrt.wknMetaAt 1F I) ∧ equal (meta 0F) (func₁ (lift ∘ Fin.suc ∘ lower) (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)
+
+open Term.Term
+open Semantics 2≉0
+
+private
+ variable
+ i j k m n : ℕ
+ t : Type
+ Σ Γ Δ ts : Vec Type n
+ P Q R S : Assertion Σ Γ Δ
+ ref : Reference Σ Γ t
+ e val : Expression Σ Γ t
+ es : All (Expression Σ Γ) ts
+ s s₁ s₂ : Statement Σ Γ
+
+ ℓ = b₁ ⊔ i₁ ⊔ r₁
+
+infix 4 _⊆_
+record _⊆_ (P : Assertion Σ Γ Δ) (Q : Assertion Σ Γ Δ) : Set ℓ where
+ constructor arr
+ field
+ implies : ∀ σ γ δ → ⟦ P ⟧ σ γ δ → ⟦ Q ⟧ σ γ δ
+
+open _⊆_ public
+
+data HoareTriple {Σ : Vec Type i} {Γ : Vec Type j} {Δ : Vec Type k} : Assertion Σ Γ Δ → Statement Σ Γ → Assertion Σ Γ Δ → Set (ℓsuc (b₁ ⊔ i₁ ⊔ r₁)) where
+ seq : ∀ Q → HoareTriple P s Q → HoareTriple Q s₁ R → HoareTriple P (s ∙ s₁) R
+ skip : P ⊆ Q → HoareTriple P skip Q
+ assign : subst P ref (↓ val) ⊆ Q → HoareTriple P (ref ≔ val) Q
+ declare : HoareTriple (Var.weaken 0F P ∧ equal (var 0F) (Term.Var.weaken 0F (↓ e))) s (Var.weaken 0F Q) → HoareTriple P (declare e s) Q
+ invoke : ∀ (Q R : Assertion Σ ts Δ) → P ⊆ Var.elimAll Q (All.map ↓_ es) → HoareTriple Q s R → Var.inject Γ R ⊆ Var.raise ts S → HoareTriple P (invoke (s ∙end) es) S
+ if : HoareTriple (P ∧ pred (↓ e)) s Q → P ∧ pred (↓ inv e) ⊆ Q → HoareTriple P (if e then s) Q
+ if-else : HoareTriple (P ∧ pred (↓ e)) s Q → HoareTriple (P ∧ pred (↓ inv e)) s Q → HoareTriple P (if e then s) Q
+ for : ∀ (I : Assertion _ _ (fin _ ∷ _)) → P ⊆ Meta.elim 0F I (↓ lit 0F) → HoareTriple {Δ = fin _ ∷ Δ} (Var.weaken 0F (Meta.elim 1F (Meta.weaken 0F I) (fin inject₁ (cons (meta 0F) nil)))) s (Var.weaken 0F (Meta.elim 1F (Meta.weaken 0F I) (fin suc (cons (meta 0F) nil)))) → Meta.elim 0F I (↓ lit (fromℕ m)) ⊆ Q → HoareTriple P (for m s) Q
+ some : HoareTriple P s Q → HoareTriple (some P) s (some Q)
diff --git a/src/Helium/Semantics/Core.agda b/src/Helium/Semantics/Core.agda
new file mode 100644
index 0000000..688f6f6
--- /dev/null
+++ b/src/Helium/Semantics/Core.agda
@@ -0,0 +1,209 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Base definitions for semantics
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --without-K #-}
+
+open import Helium.Data.Pseudocode.Algebra using (RawPseudocode)
+
+module Helium.Semantics.Core
+ {b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃}
+ (rawPseudocode : RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃)
+ where
+
+private
+ open module C = RawPseudocode rawPseudocode
+
+open import Algebra.Core using (Op₁)
+open import Data.Bool as Bool using (Bool)
+open import Data.Fin as Fin using (Fin; zero; suc)
+open import Data.Fin.Patterns
+import Data.Fin.Properties as Finₚ
+open import Data.Integer as 𝕀 using () renaming (ℤ to 𝕀)
+open import Data.Nat as ℕ using (ℕ; suc)
+import Data.Nat.Properties as ℕₚ
+open import Data.Product as × using (_×_; _,_)
+open import Data.Sign using (Sign)
+open import Data.Unit using (⊤)
+open import Data.Vec as Vec using (Vec; []; _∷_; _++_; lookup; map; take; drop)
+open import Data.Vec.Relation.Binary.Pointwise.Extensional using (Pointwise; decidable)
+open import Data.Vec.Relation.Unary.All as All using (All; []; _∷_)
+open import Function
+open import Helium.Data.Pseudocode.Core
+open import Level hiding (suc)
+open import Relation.Binary
+import Relation.Binary.Construct.On as On
+open import Relation.Binary.PropositionalEquality
+open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Decidable.Core using (map′)
+
+private
+ variable
+ a : Level
+ A : Set a
+ t t′ t₁ t₂ : Type
+ m n : ℕ
+ Γ Δ Σ ts : Vec Type m
+
+ ℓ = b₁ ⊔ i₁ ⊔ r₁
+ ℓ₁ = ℓ ⊔ b₂ ⊔ i₂ ⊔ r₂
+ ℓ₂ = i₁ ⊔ i₃ ⊔ r₁ ⊔ r₃
+
+ Sign⇒- : Sign → Op₁ A → Op₁ A
+ Sign⇒- Sign.+ f = id
+ Sign⇒- Sign.- f = f
+
+open ℕₚ.≤-Reasoning
+
+𝕀⇒ℤ : 𝕀 → ℤ
+𝕀⇒ℤ z = Sign⇒- (𝕀.sign z) ℤ.-_ (𝕀.∣ z ∣ ℤ′.×′ 1ℤ)
+
+𝕀⇒ℝ : 𝕀 → ℝ
+𝕀⇒ℝ z = Sign⇒- (𝕀.sign z) ℝ.-_ (𝕀.∣ z ∣ ℝ′.×′ 1ℝ)
+
+castVec : .(eq : m ≡ n) → Vec A m → Vec A n
+castVec {m = .0} {0} eq [] = []
+castVec {m = .suc m} {suc n} eq (x ∷ xs) = x ∷ castVec (ℕₚ.suc-injective eq) xs
+
+⟦_⟧ₜ : Type → Set ℓ
+⟦_⟧ₜ′ : Vec Type n → Set ℓ
+
+⟦ bool ⟧ₜ = Lift ℓ Bool
+⟦ int ⟧ₜ = Lift ℓ ℤ
+⟦ fin n ⟧ₜ = Lift ℓ (Fin n)
+⟦ real ⟧ₜ = Lift ℓ ℝ
+⟦ bit ⟧ₜ = Lift ℓ Bit
+⟦ tuple ts ⟧ₜ = ⟦ ts ⟧ₜ′
+⟦ array t n ⟧ₜ = Vec ⟦ t ⟧ₜ n
+
+⟦ [] ⟧ₜ′ = Lift ℓ ⊤
+⟦ t ∷ [] ⟧ₜ′ = ⟦ t ⟧ₜ
+⟦ t ∷ t₁ ∷ ts ⟧ₜ′ = ⟦ t ⟧ₜ × ⟦ t₁ ∷ ts ⟧ₜ′
+
+fetch : ∀ (i : Fin n) Γ → ⟦ Γ ⟧ₜ′ → ⟦ lookup Γ i ⟧ₜ
+fetch 0F (t ∷ []) x = x
+fetch 0F (t ∷ t₁ ∷ Γ) (x , xs) = x
+fetch (suc i) (t ∷ t₁ ∷ Γ) (x , xs) = fetch i (t₁ ∷ Γ) xs
+
+updateAt : ∀ (i : Fin n) Γ → ⟦ lookup Γ i ⟧ₜ → ⟦ Γ ⟧ₜ′ → ⟦ Γ ⟧ₜ′
+updateAt 0F (t ∷ []) v x = v
+updateAt 0F (t ∷ t₁ ∷ Γ) v (x , xs) = v , xs
+updateAt (suc i) (t ∷ t₁ ∷ Γ) v (x , xs) = x , updateAt i (t₁ ∷ Γ) v xs
+
+cons′ : ∀ (ts : Vec Type n) → ⟦ t ⟧ₜ → ⟦ tuple ts ⟧ₜ → ⟦ tuple (t ∷ ts) ⟧ₜ
+cons′ [] x xs = x
+cons′ (_ ∷ _) x xs = x , xs
+
+head′ : ∀ (ts : Vec Type n) → ⟦ tuple (t ∷ ts) ⟧ₜ → ⟦ t ⟧ₜ
+head′ [] x = x
+head′ (_ ∷ _) (x , xs) = x
+
+tail′ : ∀ (ts : Vec Type n) → ⟦ tuple (t ∷ ts) ⟧ₜ → ⟦ tuple ts ⟧ₜ
+tail′ [] x = _
+tail′ (_ ∷ _) (x , xs) = xs
+
+_≈_ : ⦃ HasEquality t ⦄ → Rel ⟦ t ⟧ₜ ℓ₁
+_≈_ ⦃ bool ⦄ = Lift ℓ₁ ∘₂ _≡_ on lower
+_≈_ ⦃ int ⦄ = Lift ℓ₁ ∘₂ ℤ._≈_ on lower
+_≈_ ⦃ fin ⦄ = Lift ℓ₁ ∘₂ _≡_ on lower
+_≈_ ⦃ real ⦄ = Lift ℓ₁ ∘₂ ℝ._≈_ on lower
+_≈_ ⦃ bit ⦄ = Lift ℓ₁ ∘₂ 𝔹._≈_ on lower
+_≈_ ⦃ array ⦄ = Pointwise _≈_
+
+_<_ : ⦃ Ordered t ⦄ → Rel ⟦ t ⟧ₜ ℓ₂
+_<_ ⦃ int ⦄ = Lift ℓ₂ ∘₂ ℤ._<_ on lower
+_<_ ⦃ fin ⦄ = Lift ℓ₂ ∘₂ Fin._<_ on lower
+_<_ ⦃ real ⦄ = Lift ℓ₂ ∘₂ ℝ._<_ on lower
+
+≈-dec : ⦃ hasEq : HasEquality t ⦄ → Decidable (_≈_ ⦃ hasEq ⦄)
+≈-dec ⦃ bool ⦄ = map′ lift lower ∘₂ On.decidable lower _≡_ Bool._≟_
+≈-dec ⦃ int ⦄ = map′ lift lower ∘₂ On.decidable lower ℤ._≈_ _≟ᶻ_
+≈-dec ⦃ fin ⦄ = map′ lift lower ∘₂ On.decidable lower _≡_ Fin._≟_
+≈-dec ⦃ real ⦄ = map′ lift lower ∘₂ On.decidable lower ℝ._≈_ _≟ʳ_
+≈-dec ⦃ bit ⦄ = map′ lift lower ∘₂ On.decidable lower 𝔹._≈_ _≟ᵇ₁_
+≈-dec ⦃ array ⦄ = decidable ≈-dec
+
+<-dec : ⦃ ordered : Ordered t ⦄ → Decidable (_<_ ⦃ ordered ⦄)
+<-dec ⦃ int ⦄ = map′ lift lower ∘₂ On.decidable lower ℤ._<_ _<ᶻ?_
+<-dec ⦃ fin ⦄ = map′ lift lower ∘₂ On.decidable lower Fin._<_ Fin._<?_
+<-dec ⦃ real ⦄ = map′ lift lower ∘₂ On.decidable lower ℝ._<_ _<ʳ?_
+
+Κ[_]_ : ∀ t → literalType t → ⟦ t ⟧ₜ
+Κ[ bool ] x = lift x
+Κ[ int ] x = lift (𝕀⇒ℤ x)
+Κ[ fin n ] x = lift x
+Κ[ real ] x = lift (𝕀⇒ℝ x)
+Κ[ bit ] x = lift (Bool.if x then 1𝔹 else 0𝔹)
+Κ[ tuple [] ] x = _
+Κ[ tuple (t ∷ []) ] x = Κ[ t ] x
+Κ[ tuple (t ∷ t₁ ∷ ts) ] (x , xs) = Κ[ t ] x , Κ[ tuple (t₁ ∷ ts) ] xs
+Κ[ array t n ] x = map Κ[ t ]_ x
+
+2≉0 : Set _
+2≉0 = ¬ 2 ℝ′.×′ 1ℝ ℝ.≈ 0ℝ
+
+neg : ⦃ IsNumeric t ⦄ → Op₁ ⟦ t ⟧ₜ
+neg ⦃ int ⦄ = lift ∘ ℤ.-_ ∘ lower
+neg ⦃ real ⦄ = lift ∘ ℝ.-_ ∘ lower
+
+add : ⦃ isNum₁ : IsNumeric t₁ ⦄ → ⦃ isNum₂ : IsNumeric t₂ ⦄ → ⟦ t₁ ⟧ₜ → ⟦ t₂ ⟧ₜ → ⟦ isNum₁ +ᵗ isNum₂ ⟧ₜ
+add ⦃ int ⦄ ⦃ int ⦄ x y = lift (lower x ℤ.+ lower y)
+add ⦃ int ⦄ ⦃ real ⦄ x y = lift (lower x /1 ℝ.+ lower y)
+add ⦃ real ⦄ ⦃ int ⦄ x y = lift (lower x ℝ.+ lower y /1)
+add ⦃ real ⦄ ⦃ real ⦄ x y = lift (lower x ℝ.+ lower y)
+
+mul : ⦃ isNum₁ : IsNumeric t₁ ⦄ → ⦃ isNum₂ : IsNumeric t₂ ⦄ → ⟦ t₁ ⟧ₜ → ⟦ t₂ ⟧ₜ → ⟦ isNum₁ +ᵗ isNum₂ ⟧ₜ
+mul ⦃ int ⦄ ⦃ int ⦄ x y = lift (lower x ℤ.* lower y)
+mul ⦃ int ⦄ ⦃ real ⦄ x y = lift (lower x /1 ℝ.* lower y)
+mul ⦃ real ⦄ ⦃ int ⦄ x y = lift (lower x ℝ.* lower y /1)
+mul ⦃ real ⦄ ⦃ real ⦄ x y = lift (lower x ℝ.* lower y)
+
+pow : ⦃ IsNumeric t ⦄ → ⟦ t ⟧ₜ → ℕ → ⟦ t ⟧ₜ
+pow ⦃ int ⦄ = lift ∘₂ ℤ′._^′_ ∘ lower
+pow ⦃ real ⦄ = lift ∘₂ ℝ′._^′_ ∘ lower
+
+shift : 2≉0 → ℤ → ℕ → ℤ
+shift 2≉0 z n = ⌊ z /1 ℝ.* 2≉0 ℝ.⁻¹ ℝ′.^′ n ⌋
+
+lowerFin : ∀ (ms : Vec ℕ n) → ⟦ tuple (map fin ms) ⟧ₜ → literalTypes (map fin ms)
+lowerFin [] _ = _
+lowerFin (_ ∷ []) x = lower x
+lowerFin (_ ∷ m₁ ∷ ms) (x , xs) = lower x , lowerFin (m₁ ∷ ms) xs
+
+mergeVec : Vec A m → Vec A n → Fin (suc n) → Vec A (n ℕ.+ m)
+mergeVec {m = m} {n} xs ys i = castVec eq (low ++ xs ++ high)
+ where
+ i′ = Fin.toℕ i
+ ys′ = castVec (sym (ℕₚ.m+[n∸m]≡n (ℕ.≤-pred (Finₚ.toℕ<n i)))) ys
+ low = take i′ ys′
+ high = drop i′ ys′
+ eq = begin-equality
+ i′ ℕ.+ (m ℕ.+ (n ℕ.∸ i′)) ≡⟨ ℕₚ.+-comm i′ _ ⟩
+ m ℕ.+ (n ℕ.∸ i′) ℕ.+ i′ ≡⟨ ℕₚ.+-assoc m _ _ ⟩
+ m ℕ.+ (n ℕ.∸ i′ ℕ.+ i′) ≡⟨ cong (m ℕ.+_) (ℕₚ.m∸n+n≡m (ℕ.≤-pred (Finₚ.toℕ<n i))) ⟩
+ m ℕ.+ n ≡⟨ ℕₚ.+-comm m n ⟩
+ n ℕ.+ m ∎
+
+sliceVec : Vec A (n ℕ.+ m) → Fin (suc n) → Vec A m
+sliceVec {n = n} {m} xs i = take m (drop i′ (castVec eq xs))
+ where
+ i′ = Fin.toℕ i
+ eq = sym $ begin-equality
+ i′ ℕ.+ (m ℕ.+ (n ℕ.∸ i′)) ≡⟨ ℕₚ.+-comm i′ _ ⟩
+ m ℕ.+ (n ℕ.∸ i′) ℕ.+ i′ ≡⟨ ℕₚ.+-assoc m _ _ ⟩
+ m ℕ.+ (n ℕ.∸ i′ ℕ.+ i′) ≡⟨ cong (m ℕ.+_) (ℕₚ.m∸n+n≡m (ℕ.≤-pred (Finₚ.toℕ<n i))) ⟩
+ m ℕ.+ n ≡⟨ ℕₚ.+-comm m n ⟩
+ n ℕ.+ m ∎
+
+cutVec : Vec A (n ℕ.+ m) → Fin (suc n) → Vec A n
+cutVec {n = n} {m} xs i = castVec (ℕₚ.m+[n∸m]≡n (ℕ.≤-pred (Finₚ.toℕ<n i))) (take i′ (castVec eq xs) ++ drop m (drop i′ (castVec eq xs)))
+ where
+ i′ = Fin.toℕ i
+ eq = sym $ begin-equality
+ i′ ℕ.+ (m ℕ.+ (n ℕ.∸ i′)) ≡⟨ ℕₚ.+-comm i′ _ ⟩
+ m ℕ.+ (n ℕ.∸ i′) ℕ.+ i′ ≡⟨ ℕₚ.+-assoc m _ _ ⟩
+ m ℕ.+ (n ℕ.∸ i′ ℕ.+ i′) ≡⟨ cong (m ℕ.+_) (ℕₚ.m∸n+n≡m (ℕ.≤-pred (Finₚ.toℕ<n i))) ⟩
+ m ℕ.+ n ≡⟨ ℕₚ.+-comm m n ⟩
+ n ℕ.+ m ∎
diff --git a/src/Helium/Semantics/Denotational/Core.agda b/src/Helium/Semantics/Denotational/Core.agda
index 07c71bd..c015cbc 100644
--- a/src/Helium/Semantics/Denotational/Core.agda
+++ b/src/Helium/Semantics/Denotational/Core.agda
@@ -16,284 +16,144 @@ module Helium.Semantics.Denotational.Core
private
open module C = RawPseudocode rawPseudocode
-open import Data.Bool as Bool using (Bool; true; false)
-open import Data.Fin as Fin using (Fin; zero; suc)
-import Data.Fin.Properties as Finₚ
-open import Data.Nat as ℕ using (ℕ; zero; suc)
-import Data.Nat.Properties as ℕₚ
-open import Data.Product as P using (_×_; _,_)
-open import Data.Sum as S using (_⊎_) renaming (inj₁ to next; inj₂ to ret)
-open import Data.Unit using (⊤)
-open import Data.Vec as Vec using (Vec; []; _∷_)
+import Data.Bool as Bool
+open import Data.Empty using (⊥-elim)
+import Data.Fin as Fin
+import Data.Integer as 𝕀
+open import Data.Nat using (ℕ)
+open import Data.Product using (_×_; _,_; proj₁; proj₂; <_,_>; uncurry)
+open import Data.Vec as Vec using (Vec; []; _∷_; map; zipWith)
open import Data.Vec.Relation.Unary.All using (All; []; _∷_)
-import Data.Vec.Functional as VecF
-open import Function using (case_of_; _∘′_; id)
+open import Function
open import Helium.Data.Pseudocode.Core
-import Induction as I
-import Induction.WellFounded as Wf
-open import Level using (Level; _⊔_; 0ℓ)
-open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; module ≡-Reasoning)
-open import Relation.Nullary using (does) renaming (¬_ to ¬′_)
-open import Relation.Nullary.Decidable.Core using (True; False; toWitness; fromWitness)
+open import Helium.Semantics.Core rawPseudocode
+open import Level
+open import Relation.Binary.PropositionalEquality using (sym)
+open import Relation.Nullary using (does)
-⟦_⟧ₗ : Type → Level
-⟦ bool ⟧ₗ = 0ℓ
-⟦ int ⟧ₗ = i₁
-⟦ fin n ⟧ₗ = 0ℓ
-⟦ real ⟧ₗ = r₁
-⟦ bit ⟧ₗ = b₁
-⟦ bits n ⟧ₗ = b₁
-⟦ tuple n ts ⟧ₗ = helper ts
- where
- helper : ∀ {n} → Vec Type n → Level
- helper [] = 0ℓ
- helper (t ∷ ts) = ⟦ t ⟧ₗ ⊔ helper ts
-⟦ array t n ⟧ₗ = ⟦ t ⟧ₗ
-
-⟦_⟧ₜ : ∀ t → Set ⟦ t ⟧ₗ
-⟦_⟧ₜ′ : ∀ {n} ts → Set ⟦ tuple n ts ⟧ₗ
-
-⟦ bool ⟧ₜ = Bool
-⟦ int ⟧ₜ = ℤ
-⟦ fin n ⟧ₜ = Fin n
-⟦ real ⟧ₜ = ℝ
-⟦ bit ⟧ₜ = Bit
-⟦ bits n ⟧ₜ = Bits n
-⟦ tuple n ts ⟧ₜ = ⟦ ts ⟧ₜ′
-⟦ array t n ⟧ₜ = Vec ⟦ t ⟧ₜ n
-
-⟦ [] ⟧ₜ′ = ⊤
-⟦ t ∷ [] ⟧ₜ′ = ⟦ t ⟧ₜ
-⟦ t ∷ t′ ∷ ts ⟧ₜ′ = ⟦ t ⟧ₜ × ⟦ t′ ∷ ts ⟧ₜ′
-
--- The case for bitvectors looks odd so that the right-most bit is bit 0.
-𝒦 : ∀ {t} → Literal t → ⟦ t ⟧ₜ
-𝒦 (x ′b) = x
-𝒦 (x ′i) = x ℤ′.×′ 1ℤ
-𝒦 (x ′f) = x
-𝒦 (x ′r) = x ℝ′.×′ 1ℝ
-𝒦 (x ′x) = Bool.if x then 1𝔹 else 0𝔹
-𝒦 (xs ′xs) = Vec.foldl Bits (λ bs b → (Bool.if b then 1𝔹 else 0𝔹) VecF.∷ bs) VecF.[] xs
-𝒦 (x ′a) = Vec.replicate (𝒦 x)
-
-fetch : ∀ {n} ts → ⟦ tuple n ts ⟧ₜ → ∀ i → ⟦ Vec.lookup ts i ⟧ₜ
-fetch (_ ∷ []) x zero = x
-fetch (_ ∷ _ ∷ _) (x , xs) zero = x
-fetch (_ ∷ t ∷ ts) (x , xs) (suc i) = fetch (t ∷ ts) xs i
-
-updateAt : ∀ {n} ts i → ⟦ Vec.lookup ts i ⟧ₜ → ⟦ tuple n ts ⟧ₜ → ⟦ tuple n ts ⟧ₜ
-updateAt (_ ∷ []) zero v _ = v
-updateAt (_ ∷ _ ∷ _) zero v (_ , xs) = v , xs
-updateAt (_ ∷ t ∷ ts) (suc i) v (x , xs) = x , updateAt (t ∷ ts) i v xs
-
-tupCons : ∀ {n t} ts → ⟦ t ⟧ₜ → ⟦ tuple n ts ⟧ₜ → ⟦ tuple _ (t ∷ ts) ⟧ₜ
-tupCons [] x xs = x
-tupCons (t ∷ ts) x xs = x , xs
-
-tupHead : ∀ {n t} ts → ⟦ tuple (suc n) (t ∷ ts) ⟧ₜ → ⟦ t ⟧ₜ
-tupHead {t = t} ts xs = fetch (t ∷ ts) xs zero
-
-tupTail : ∀ {n t} ts → ⟦ tuple _ (t ∷ ts) ⟧ₜ → ⟦ tuple n ts ⟧ₜ
-tupTail [] x = _
-tupTail (_ ∷ _) (x , xs) = xs
-
-equal : ∀ {t} → HasEquality t → ⟦ t ⟧ₜ → ⟦ t ⟧ₜ → Bool
-equal bool x y = does (x Bool.≟ y)
-equal int x y = does (x ≟ᶻ y)
-equal fin x y = does (x Fin.≟ y)
-equal real x y = does (x ≟ʳ y)
-equal bit x y = does (x ≟ᵇ₁ y)
-equal bits x y = does (x ≟ᵇ y)
-
-comp : ∀ {t} → IsNumeric t → ⟦ t ⟧ₜ → ⟦ t ⟧ₜ → Bool
-comp int x y = does (x <ᶻ? y)
-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 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 ⟧ₜ
-take bits i x = VecF.take i x
-take (array _) i x = Vec.take i x
-
--- drop from 0
-drop : ∀ t i {j} → ⟦ asType t (i ℕ.+ j) ⟧ₜ → ⟦ asType t j ⟧ₜ
-drop bits i x = VecF.drop i x
-drop (array _) i x = Vec.drop i x
-
-casted : ∀ t {i j} → .(eq : i ≡ j) → ⟦ asType t i ⟧ₜ → ⟦ asType t j ⟧ₜ
-casted bits eq x = x ∘′ Fin.cast (≡.sym eq)
-casted (array _) {j = zero} eq [] = []
-casted (array t) {j = suc _} eq (x ∷ y) = x ∷ casted (array t) (ℕₚ.suc-injective eq) y
-
-module _ where
- m≤n⇒m+k≡n : ∀ {m n} → m ℕ.≤ n → P.∃ λ k → m ℕ.+ k ≡ n
- 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 : ∀ 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
- i+k≡n = m≤n⇒m+k≡n (ℕₚ.≤-pred (Finₚ.toℕ<n i))
- k = P.proj₁ i+k≡n
-
- -- 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.[]
-box (array t) v = v ∷ []
-
-unboxed : ∀ t → ⟦ asType t 1 ⟧ₜ → ⟦ elemType t ⟧ₜ
-unboxed bits v = v (Fin.zero)
-unboxed (array t) (v ∷ []) = v
-
-neg : ∀ {t} → IsNumeric t → ⟦ t ⟧ₜ → ⟦ t ⟧ₜ
-neg int x = ℤ.- x
-neg real x = ℝ.- x
-
-add : ∀ {t₁ t₂} (isNum₁ : True (isNumeric? t₁)) (isNum₂ : True (isNumeric? t₂)) → ⟦ t₁ ⟧ₜ → ⟦ t₂ ⟧ₜ → ⟦ combineNumeric t₁ t₂ isNum₁ isNum₂ ⟧ₜ
-add {t₁ = int} {t₂ = int} _ _ x y = x ℤ.+ y
-add {t₁ = int} {t₂ = real} _ _ x y = x /1 ℝ.+ y
-add {t₁ = real} {t₂ = int} _ _ x y = x ℝ.+ y /1
-add {t₁ = real} {t₂ = real} _ _ x y = x ℝ.+ y
-
-mul : ∀ {t₁ t₂} (isNum₁ : True (isNumeric? t₁)) (isNum₂ : True (isNumeric? t₂)) → ⟦ t₁ ⟧ₜ → ⟦ t₂ ⟧ₜ → ⟦ combineNumeric t₁ t₂ isNum₁ isNum₂ ⟧ₜ
-mul {t₁ = int} {t₂ = int} _ _ x y = x ℤ.* y
-mul {t₁ = int} {t₂ = real} _ _ x y = x /1 ℝ.* y
-mul {t₁ = real} {t₂ = int} _ _ x y = x ℝ.* y /1
-mul {t₁ = real} {t₂ = real} _ _ x y = x ℝ.* y
-
-pow : ∀ {t} → IsNumeric t → ⟦ t ⟧ₜ → ℕ → ⟦ t ⟧ₜ
-pow int x n = x ℤ′.^′ n
-pow real x n = x ℝ′.^′ n
-
-shiftr : ¬′ 2 ℝ′.×′ 1ℝ ℝ.≈ 0ℝ → ⟦ int ⟧ₜ → ℕ → ⟦ int ⟧ₜ
-shiftr 2≉0 x n = ⌊ x /1 ℝ.* 2≉0 ℝ.⁻¹ ℝ′.^′ n ⌋
-
-module Expression
- {o} {Σ : Vec Type o}
- (2≉0 : ¬′ 2 ℝ′.×′ 1ℝ ℝ.≈ 0ℝ)
- where
-
- open Code Σ
-
- ⟦_⟧ᵉ : ∀ {n} {Γ : Vec Type n} {t} → Expression Γ t → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ t ⟧ₜ
- ⟦_⟧ˢ : ∀ {n} {Γ : Vec Type n} → Statement Γ → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ Σ ⟧ₜ′ × ⟦ Γ ⟧ₜ′
- ⟦_⟧ᶠ : ∀ {n} {Γ : Vec Type n} {ret} → Function Γ ret → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ ret ⟧ₜ
- ⟦_⟧ᵖ : ∀ {n} {Γ : Vec Type n} → Procedure Γ → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ Σ ⟧ₜ′
- ⟦_⟧ᵉ′ : ∀ {n} {Γ : Vec Type n} {m ts} → All (Expression Γ) ts → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ tuple m ts ⟧ₜ
- update : ∀ {n Γ t e} → CanAssign {n} {Γ} {t} e → ⟦ t ⟧ₜ → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ Σ ⟧ₜ′ × ⟦ Γ ⟧ₜ′
-
- ⟦ lit x ⟧ᵉ σ γ = 𝒦 x
- ⟦ state i ⟧ᵉ σ γ = fetch Σ σ i
- ⟦_⟧ᵉ {Γ = Γ} (var i) σ γ = fetch Γ γ i
- ⟦ abort e ⟧ᵉ σ γ = case ⟦ e ⟧ᵉ σ γ of λ ()
- ⟦ _≟_ {hasEquality = hasEq} e e₁ ⟧ᵉ σ γ = equal (toWitness hasEq) (⟦ e ⟧ᵉ σ γ) (⟦ e₁ ⟧ᵉ σ γ)
- ⟦ _<?_ {isNumeric = isNum} e e₁ ⟧ᵉ σ γ = comp (toWitness isNum) (⟦ e ⟧ᵉ σ γ) (⟦ e₁ ⟧ᵉ σ γ)
- ⟦ inv e ⟧ᵉ σ γ = Bool.not (⟦ e ⟧ᵉ σ γ)
- ⟦ e && e₁ ⟧ᵉ σ γ = Bool.if ⟦ e ⟧ᵉ σ γ then ⟦ e₁ ⟧ᵉ σ γ else false
- ⟦ e || e₁ ⟧ᵉ σ γ = Bool.if ⟦ e ⟧ᵉ σ γ then true else ⟦ e₁ ⟧ᵉ σ γ
- ⟦ not e ⟧ᵉ σ γ = Bits.¬_ (⟦ e ⟧ᵉ σ γ)
- ⟦ e and e₁ ⟧ᵉ σ γ = ⟦ e ⟧ᵉ σ γ Bits.∧ ⟦ e₁ ⟧ᵉ σ γ
- ⟦ e or e₁ ⟧ᵉ σ γ = ⟦ e ⟧ᵉ σ γ Bits.∨ ⟦ e₁ ⟧ᵉ σ γ
- ⟦ [_] {t = t} e ⟧ᵉ σ γ = box t (⟦ e ⟧ᵉ σ γ)
- ⟦ unbox {t = t} e ⟧ᵉ σ γ = unboxed t (⟦ 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₁ ⟧ᵉ σ γ)
- ⟦ _*_ {isNumeric₁ = isNum₁} {isNumeric₂ = isNum₂} e e₁ ⟧ᵉ σ γ = mul isNum₁ isNum₂ (⟦ e ⟧ᵉ σ γ) (⟦ e₁ ⟧ᵉ σ γ)
- -- ⟦ e / e₁ ⟧ᵉ σ γ = {!!}
- ⟦ _^_ {isNumeric = isNum} e n ⟧ᵉ σ γ = pow (toWitness isNum) (⟦ e ⟧ᵉ σ γ) n
- ⟦ _>>_ e n ⟧ᵉ σ γ = shiftr 2≉0 (⟦ e ⟧ᵉ σ γ) n
- ⟦ rnd e ⟧ᵉ σ γ = ⌊ ⟦ e ⟧ᵉ σ γ ⌋
- ⟦ fin x e ⟧ᵉ σ γ = apply x (⟦ e ⟧ᵉ σ γ)
- where
- apply : ∀ {k ms n} → (All Fin ms → Fin n) → ⟦ Vec.map {n = k} fin ms ⟧ₜ′ → ⟦ fin n ⟧ₜ
- apply {zero} {[]} f xs = f []
- apply {suc k} {_ ∷ ms} f xs =
- apply (λ x → f (tupHead (Vec.map fin ms) xs ∷ x)) (tupTail (Vec.map fin ms) xs)
- ⟦ asInt e ⟧ᵉ σ γ = Fin.toℕ (⟦ e ⟧ᵉ σ γ) ℤ′.×′ 1ℤ
- ⟦ nil ⟧ᵉ σ γ = _
- ⟦ cons {ts = ts} e e₁ ⟧ᵉ σ γ = tupCons ts (⟦ e ⟧ᵉ σ γ) (⟦ e₁ ⟧ᵉ σ γ)
- ⟦ head {ts = ts} e ⟧ᵉ σ γ = tupHead ts (⟦ e ⟧ᵉ σ γ)
- ⟦ tail {ts = ts} e ⟧ᵉ σ γ = tupTail ts (⟦ e ⟧ᵉ σ γ)
- ⟦ call f e ⟧ᵉ σ γ = ⟦ f ⟧ᶠ σ (⟦ e ⟧ᵉ′ σ γ)
- ⟦ if e then e₁ else e₂ ⟧ᵉ σ γ = Bool.if ⟦ e ⟧ᵉ σ γ then ⟦ e₁ ⟧ᵉ σ γ else ⟦ e₂ ⟧ᵉ σ γ
-
- ⟦ [] ⟧ᵉ′ σ γ = _
- ⟦ e ∷ [] ⟧ᵉ′ σ γ = ⟦ e ⟧ᵉ σ γ
- ⟦ e ∷ e′ ∷ es ⟧ᵉ′ σ γ = ⟦ e ⟧ᵉ σ γ , ⟦ e′ ∷ es ⟧ᵉ′ σ γ
-
- ⟦ s ∙ s₁ ⟧ˢ σ γ = P.uncurry ⟦ s ⟧ˢ (⟦ s ⟧ˢ σ γ)
- ⟦ skip ⟧ˢ σ γ = σ , γ
- ⟦ _≔_ ref {canAssign = canAssign} e ⟧ˢ σ γ = update (toWitness canAssign) (⟦ e ⟧ᵉ σ γ) σ γ
- ⟦_⟧ˢ {Γ = Γ} (declare e s) σ γ = P.map₂ (tupTail Γ) (⟦ s ⟧ˢ σ (tupCons Γ (⟦ e ⟧ᵉ σ γ) γ))
- ⟦ invoke p e ⟧ˢ σ γ = ⟦ p ⟧ᵖ σ (⟦ e ⟧ᵉ′ σ γ) , γ
- ⟦ if e then s₁ ⟧ˢ σ γ = Bool.if ⟦ e ⟧ᵉ σ γ then ⟦ s₁ ⟧ˢ σ γ else (σ , γ)
- ⟦ if e then s₁ else s₂ ⟧ˢ σ γ = Bool.if ⟦ e ⟧ᵉ σ γ then ⟦ s₁ ⟧ˢ σ γ else ⟦ s₂ ⟧ˢ σ γ
- ⟦_⟧ˢ {Γ = Γ} (for m s) σ γ = helper m ⟦ s ⟧ˢ σ γ
- where
- helper : ∀ m → (⟦ Σ ⟧ₜ′ → ⟦ fin m ∷ Γ ⟧ₜ′ → ⟦ Σ ⟧ₜ′ × ⟦ fin m ∷ Γ ⟧ₜ′) → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ Σ ⟧ₜ′ × ⟦ Γ ⟧ₜ′
- helper zero s σ γ = σ , γ
- helper (suc m) s σ γ = P.uncurry (helper m s′) (P.map₂ (tupTail Γ) (s σ (tupCons Γ zero γ)))
- where
- s′ : ⟦ Σ ⟧ₜ′ → ⟦ fin m ∷ Γ ⟧ₜ′ → ⟦ Σ ⟧ₜ′ × ⟦ fin m ∷ Γ ⟧ₜ′
- s′ σ γ =
- P.map₂ (tupCons Γ (tupHead Γ γ) ∘′ (tupTail Γ))
- (s σ (tupCons Γ (suc (tupHead Γ γ)) (tupTail Γ γ)))
-
- ⟦ s ∙return e ⟧ᶠ σ γ = P.uncurry ⟦ e ⟧ᵉ (⟦ s ⟧ˢ σ γ)
- ⟦_⟧ᶠ {Γ = Γ} (declare e f) σ γ = ⟦ f ⟧ᶠ σ (tupCons Γ (⟦ e ⟧ᵉ σ γ) γ)
-
- ⟦ s ∙end ⟧ᵖ σ γ = P.proj₁ (⟦ s ⟧ˢ σ γ)
-
- update (state i) v σ γ = updateAt Σ i v σ , γ
- update {Γ = Γ} (var i) v σ γ = σ , updateAt Γ i v γ
- 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 (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 nil v σ γ = σ , γ
- update (cons {ts = ts} e e₁) vs σ γ = do
- let σ′ , γ′ = update e (tupHead ts vs) σ γ
- update e₁ (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) σ γ
+private
+ variable
+ n : ℕ
+ t : Type
+ Σ Γ ts : Vec Type n
+
+
+module Semantics (2≉0 : 2≉0) where
+ expr : Expression Σ Γ t → ⟦ Σ ⟧ₜ′ × ⟦ Γ ⟧ₜ′ → ⟦ t ⟧ₜ
+ exprs : All (Expression Σ Γ) ts → ⟦ Σ ⟧ₜ′ × ⟦ Γ ⟧ₜ′ → ⟦ ts ⟧ₜ′
+ ref : Reference Σ Γ t → ⟦ Σ ⟧ₜ′ × ⟦ Γ ⟧ₜ′ → ⟦ t ⟧ₜ
+ locRef : LocalReference Σ Γ t → ⟦ Σ ⟧ₜ′ × ⟦ Γ ⟧ₜ′ → ⟦ t ⟧ₜ
+ assign : Reference Σ Γ t → ⟦ t ⟧ₜ → ⟦ Σ ⟧ₜ′ × ⟦ Γ ⟧ₜ′ → ⟦ Σ ⟧ₜ′ × ⟦ Γ ⟧ₜ′ → ⟦ Σ ⟧ₜ′ × ⟦ Γ ⟧ₜ′
+ locAssign : LocalReference Σ Γ t → ⟦ t ⟧ₜ → ⟦ Σ ⟧ₜ′ × ⟦ Γ ⟧ₜ′ → ⟦ Σ ⟧ₜ′ × ⟦ Γ ⟧ₜ′ → ⟦ Γ ⟧ₜ′
+ stmt : Statement Σ Γ → ⟦ Σ ⟧ₜ′ × ⟦ Γ ⟧ₜ′ → ⟦ Σ ⟧ₜ′ × ⟦ Γ ⟧ₜ′
+ locStmt : LocalStatement Σ Γ → ⟦ Σ ⟧ₜ′ × ⟦ Γ ⟧ₜ′ → ⟦ Γ ⟧ₜ′
+ fun : Function Σ Γ t → ⟦ Σ ⟧ₜ′ × ⟦ Γ ⟧ₜ′ → ⟦ t ⟧ₜ
+ proc : Procedure Σ Γ → ⟦ Σ ⟧ₜ′ × ⟦ Γ ⟧ₜ′ → ⟦ Σ ⟧ₜ′
+
+ expr (lit {t = t} x) = const (Κ[ t ] x)
+ expr {Σ = Σ} (state i) = fetch i Σ ∘ proj₁
+ expr {Γ = Γ} (var i) = fetch i Γ ∘ proj₂
+ expr (e ≟ e₁) = lift ∘ does ∘ uncurry ≈-dec ∘ < expr e , expr e₁ >
+ expr (e <? e₁) = lift ∘ does ∘ uncurry <-dec ∘ < expr e , expr e₁ >
+ expr (inv e) = lift ∘ Bool.not ∘ lower ∘ expr e
+ expr (e && e₁) = lift ∘ uncurry (Bool._∧_ on lower) ∘ < expr e , expr e₁ >
+ expr (e || e₁) = lift ∘ uncurry (Bool._∨_ on lower) ∘ < expr e , expr e₁ >
+ expr (not e) = map (lift ∘ 𝔹.¬_ ∘ lower) ∘ expr e
+ expr (e and e₁) = uncurry (zipWith (lift ∘₂ 𝔹._∧_ on lower)) ∘ < expr e , expr e₁ >
+ expr (e or e₁) = uncurry (zipWith (lift ∘₂ 𝔹._∨_ on lower)) ∘ < expr e , expr e₁ >
+ expr [ e ] = (_∷ []) ∘ expr e
+ expr (unbox e) = Vec.head ∘ expr e
+ expr (merge e e₁ e₂) = uncurry (uncurry mergeVec) ∘ < < expr e , expr e₁ > , lower ∘ expr e₂ >
+ expr (slice e e₁) = uncurry sliceVec ∘ < expr e , lower ∘ expr e₁ >
+ expr (cut e e₁) = uncurry cutVec ∘ < expr e , lower ∘ expr e₁ >
+ expr (cast eq e) = castVec eq ∘ expr e
+ expr (- e) = neg ∘ expr e
+ expr (e + e₁) = uncurry add ∘ < expr e , expr e₁ >
+ expr (e * e₁) = uncurry mul ∘ < expr e , expr e₁ >
+ expr (e ^ x) = flip pow x ∘ expr e
+ expr (e >> n) = lift ∘ flip (shift 2≉0) n ∘ lower ∘ expr e
+ expr (rnd e) = lift ∘ ⌊_⌋ ∘ lower ∘ expr e
+ expr (fin {ms = ms} f e) = lift ∘ f ∘ lowerFin ms ∘ expr e
+ expr (asInt e) = lift ∘ 𝕀⇒ℤ ∘ 𝕀.+_ ∘ Fin.toℕ ∘ lower ∘ expr e
+ expr nil = const _
+ expr (cons {ts = ts} e e₁) = uncurry (cons′ ts) ∘ < expr e , expr e₁ >
+ expr (head {ts = ts} e) = head′ ts ∘ expr e
+ expr (tail {ts = ts} e) = tail′ ts ∘ expr e
+ expr (call f es) = fun f ∘ < proj₁ , exprs es >
+ expr (if e then e₁ else e₂) = uncurry (uncurry Bool.if_then_else_) ∘ < < lower ∘ expr e , expr e₁ > , expr e₂ >
+
+ exprs [] = const _
+ exprs (e ∷ []) = expr e
+ exprs (e ∷ e₁ ∷ es) = < expr e , exprs (e₁ ∷ es) >
+
+ ref {Σ = Σ} (state i) = fetch i Σ ∘ proj₁
+ ref {Γ = Γ} (var i) = fetch i Γ ∘ proj₂
+ ref [ r ] = (_∷ []) ∘ ref r
+ ref (unbox r) = Vec.head ∘ ref r
+ ref (merge r r₁ e) = uncurry (uncurry mergeVec) ∘ < < ref r , ref r₁ > , lower ∘ expr e >
+ ref (slice r e) = uncurry sliceVec ∘ < ref r , lower ∘ expr e >
+ ref (cut r e) = uncurry cutVec ∘ < ref r , lower ∘ expr e >
+ ref (cast eq r) = castVec eq ∘ ref r
+ ref nil = const _
+ ref (cons {ts = ts} r r₁) = uncurry (cons′ ts) ∘ < ref r , ref r₁ >
+ ref (head {ts = ts} r) = head′ ts ∘ ref r
+ ref (tail {ts = ts} r) = tail′ ts ∘ ref r
+
+ locRef {Γ = Γ} (var i) = fetch i Γ ∘ proj₂
+ locRef [ r ] = (_∷ []) ∘ locRef r
+ locRef (unbox r) = Vec.head ∘ locRef r
+ locRef (merge r r₁ e) = uncurry (uncurry mergeVec) ∘ < < locRef r , locRef r₁ > , lower ∘ expr e >
+ locRef (slice r e) = uncurry sliceVec ∘ < locRef r , lower ∘ expr e >
+ locRef (cut r e) = uncurry cutVec ∘ < locRef r , lower ∘ expr e >
+ locRef (cast eq r) = castVec eq ∘ locRef r
+ locRef nil = const _
+ locRef (cons {ts = ts} r r₁) = uncurry (cons′ ts) ∘ < locRef r , locRef r₁ >
+ locRef (head {ts = ts} r) = head′ ts ∘ locRef r
+ locRef (tail {ts = ts} r) = tail′ ts ∘ locRef r
+
+ assign {Σ = Σ} (state i) val σ,γ = < updateAt i Σ val ∘ proj₁ , proj₂ >
+ assign {Γ = Γ} (var i) val σ,γ = < proj₁ , updateAt i Γ val ∘ proj₂ >
+ assign [ r ] val σ,γ = assign r (Vec.head val) σ,γ
+ assign (unbox r) val σ,γ = assign r (val ∷ []) σ,γ
+ assign (merge r r₁ e) val σ,γ = assign r₁ (cutVec val (lower (expr e σ,γ))) σ,γ ∘ assign r (sliceVec val (lower (expr e σ,γ))) σ,γ
+ assign (slice r e) val σ,γ = assign r (mergeVec val (cutVec (ref r σ,γ) (lower (expr e σ,γ))) (lower (expr e σ,γ))) σ,γ
+ assign (cut r e) val σ,γ = assign r (mergeVec (sliceVec (ref r σ,γ) (lower (expr e σ,γ))) val (lower (expr e σ,γ))) σ,γ
+ assign (cast eq r) val σ,γ = assign r (castVec (sym eq) val) σ,γ
+ assign nil val σ,γ = id
+ assign (cons {ts = ts} r r₁) val σ,γ = assign r₁ (tail′ ts val) σ,γ ∘ assign r (head′ ts val) σ,γ
+ assign (head {ts = ts} r) val σ,γ = assign r (cons′ ts val (ref (tail r) σ,γ)) σ,γ
+ assign (tail {ts = ts} r) val σ,γ = assign r (cons′ ts (ref (head r) σ,γ) val) σ,γ
+
+ locAssign {Γ = Γ} (var i) val σ,γ = updateAt i Γ val ∘ proj₂
+ locAssign [ r ] val σ,γ = locAssign r (Vec.head val) σ,γ
+ locAssign (unbox r) val σ,γ = locAssign r (val ∷ []) σ,γ
+ locAssign (merge r r₁ e) val σ,γ = locAssign r₁ (cutVec val (lower (expr e σ,γ))) σ,γ ∘ < proj₁ , locAssign r (sliceVec val (lower (expr e σ,γ))) σ,γ >
+ locAssign (slice r e) val σ,γ = locAssign r (mergeVec val (cutVec (locRef r σ,γ) (lower (expr e σ,γ))) (lower (expr e σ,γ))) σ,γ
+ locAssign (cut r e) val σ,γ = locAssign r (mergeVec (sliceVec (locRef r σ,γ) (lower (expr e σ,γ))) val (lower (expr e σ,γ))) σ,γ
+ locAssign (cast eq r) val σ,γ = locAssign r (castVec (sym eq) val) σ,γ
+ locAssign nil val σ,γ = proj₂
+ locAssign (cons {ts = ts} r r₁) val σ,γ = locAssign r₁ (tail′ ts val) σ,γ ∘ < proj₁ , locAssign r (head′ ts val) σ,γ >
+ locAssign (head {ts = ts} r) val σ,γ = locAssign r (cons′ ts val (locRef (tail r) σ,γ)) σ,γ
+ locAssign (tail {ts = ts} r) val σ,γ = locAssign r (cons′ ts (locRef (head r) σ,γ) val) σ,γ
+
+ stmt (s ∙ s₁) = stmt s₁ ∘ stmt s
+ stmt skip = id
+ stmt (ref ≔ val) = uncurry (uncurry (assign ref)) ∘ < < expr val , id > , id >
+ stmt {Γ = Γ} (declare e s) = < proj₁ , tail′ Γ ∘ proj₂ > ∘ stmt s ∘ < proj₁ , uncurry (cons′ Γ) ∘ < expr e , proj₂ > >
+ stmt (invoke p es) = < proc p ∘ < proj₁ , exprs es > , proj₂ >
+ stmt (if e then s) = uncurry (uncurry Bool.if_then_else_) ∘ < < lower ∘ expr e , stmt s > , id >
+ stmt (if e then s else s₁) = uncurry (uncurry Bool.if_then_else_) ∘ < < lower ∘ expr e , stmt s > , stmt s₁ >
+ stmt {Γ = Γ} (for m s) = Vec.foldl _ (flip λ i → (< proj₁ , tail′ Γ ∘ proj₂ > ∘ stmt s ∘ < proj₁ , cons′ Γ (lift i) ∘ proj₂ >) ∘_) id (Vec.allFin m)
+
+ locStmt (s ∙ s₁) = locStmt s₁ ∘ < proj₁ , locStmt s >
+ locStmt skip = proj₂
+ locStmt (ref ≔ val) = uncurry (uncurry (locAssign ref)) ∘ < < expr val , id > , id >
+ locStmt {Γ = Γ} (declare e s) = tail′ Γ ∘ locStmt s ∘ < proj₁ , uncurry (cons′ Γ) ∘ < expr e , proj₂ > >
+ locStmt (if e then s) = uncurry (uncurry Bool.if_then_else_) ∘ < < lower ∘ expr e , locStmt s > , proj₂ >
+ locStmt (if e then s else s₁) = uncurry (uncurry Bool.if_then_else_) ∘ < < lower ∘ expr e , locStmt s > , locStmt s₁ >
+ locStmt {Γ = Γ} (for m s) = proj₂ ∘ Vec.foldl _ (flip λ i → (< proj₁ , tail′ Γ ∘ locStmt s > ∘ < proj₁ , cons′ Γ (lift i) ∘ proj₂ >) ∘_) id (Vec.allFin m)
+
+ fun {Γ = Γ} (declare e f) = fun f ∘ < proj₁ , uncurry (cons′ Γ) ∘ < expr e , proj₂ > >
+ fun (s ∙return e) = expr e ∘ < proj₁ , locStmt s >
+
+ proc (s ∙end) = proj₁ ∘ stmt s
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-30 07:56:57 +0000