diff options
Diffstat (limited to 'src/Helium/Semantics/Axiomatic')
| -rw-r--r-- | src/Helium/Semantics/Axiomatic/Core.agda | 94 | ||||
| -rw-r--r-- | src/Helium/Semantics/Axiomatic/Term.agda | 322 |
2 files changed, 348 insertions, 68 deletions
diff --git a/src/Helium/Semantics/Axiomatic/Core.agda b/src/Helium/Semantics/Axiomatic/Core.agda index 176dbdd..de4f411 100644 --- a/src/Helium/Semantics/Axiomatic/Core.agda +++ b/src/Helium/Semantics/Axiomatic/Core.agda @@ -22,7 +22,7 @@ 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.Product as × using (_×_; _,_; uncurry) open import Data.Sum using (_⊎_) open import Data.Unit using (⊤) open import Data.Vec as Vec using (Vec; []; _∷_; _++_; lookup) @@ -45,79 +45,37 @@ private m n : ℕ Γ Δ Σ ts : Vec Type m -sizeOf : Type → Sliced → ℕ -sizeOf bool s = 0 -sizeOf int s = 0 -sizeOf (fin n) s = 0 -sizeOf real s = 0 -sizeOf bit s = 0 -sizeOf (bits n) s = Bool.if does (s ≟ˢ bits) then n else 0 -sizeOf (tuple _ []) s = 0 -sizeOf (tuple _ (t ∷ ts)) s = sizeOf t s ℕ.+ sizeOf (tuple _ ts) s -sizeOf (array t n) s = Bool.if does (s ≟ˢ array t) then n else sizeOf t s +⟦_⟧ₜ : Type → Set (b₁ ⊔ i₁ ⊔ r₁) +⟦_⟧ₜ′ : Vec Type n → Set (b₁ ⊔ i₁ ⊔ r₁) -allocateSpace : Vec Type n → Sliced → ℕ -allocateSpace [] s = 0 -allocateSpace (t ∷ ts) s = sizeOf t s ℕ.+ allocateSpace ts s +⟦ 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 -private - getSliced : ∀ {t} → True (sliced? t) → Sliced - getSliced t = ×.proj₁ (toWitness t) - - getCount : ∀ {t} → True (sliced? t) → ℕ - getCount t = ×.proj₁ (×.proj₂ (toWitness t)) - -data ⟦_；_⟧ₜ (counts : Sliced → ℕ) : (τ : Type) → Set (b₁ ⊔ i₁ ⊔ r₁) where - bool : Bool → ⟦ counts ； bool ⟧ₜ - int : ℤ → ⟦ counts ； int ⟧ₜ - fin : ∀ {n} → Fin n → ⟦ counts ； fin n ⟧ₜ - real : ℝ → ⟦ counts ； real ⟧ₜ - bit : Bit → ⟦ counts ； bit ⟧ₜ - bits : ∀ {n} → Vec (⟦ counts ； bit ⟧ₜ ⊎ Fin (counts bits)) n → ⟦ counts ； bits n ⟧ₜ - array : ∀ {t n} → Vec (⟦ counts ； t ⟧ₜ ⊎ Fin (counts (array t))) n → ⟦ counts ； array t n ⟧ₜ - tuple : ∀ {n ts} → All ⟦ counts ；_⟧ₜ ts → ⟦ counts ； tuple n ts ⟧ₜ - -Stack : (counts : Sliced → ℕ) → Vec Type n → Set (b₁ ⊔ i₁ ⊔ r₁) -Stack counts Γ = ⟦ counts ； tuple _ Γ ⟧ₜ - -Heap : (counts : Sliced → ℕ) → Set (b₁ ⊔ i₁ ⊔ r₁) -Heap counts = ∀ t → Vec ⟦ counts ； elemType t ⟧ₜ (counts t) - -record State (Γ : Vec Type n) : Set (b₁ ⊔ i₁ ⊔ r₁) where - private - counts = allocateSpace Γ - field - stack : Stack counts Γ - heap : Heap counts +⟦ [] ⟧ₜ′ = Lift (b₁ ⊔ i₁ ⊔ r₁) ⊤ +⟦ t ∷ ts ⟧ₜ′ = ⟦ t ⟧ₜ × ⟦ ts ⟧ₜ′ Transform : Vec Type m → Type → Set (b₁ ⊔ i₁ ⊔ r₁) -Transform ts t = ∀ counts → Heap counts → ⟦ counts ； tuple _ ts ⟧ₜ → ⟦ counts ； t ⟧ₜ +Transform ts t = ⟦ ts ⟧ₜ′ → ⟦ t ⟧ₜ Predicate : Vec Type m → Set (b₁ ⊔ i₁ ⊔ r₁) -Predicate ts = ∀ counts → ⟦ counts ； tuple _ ts ⟧ₜ → Bool - --- -- ⟦_⟧ₐ : ∀ {m Δ} → Assertion Σ Γ {m} Δ → State (Σ ++ Γ ++ Δ) → Set (b₁ ⊔ i₁ ⊔ r₁) --- -- ⟦_⟧ₐ = {!!} - --- -- module _ {o} {Σ : Vec Type o} where --- -- open Code Σ - --- -- 𝒦 : ∀ {n Γ m Δ t} → Literal t → Term Σ {n} Γ {m} Δ t --- -- 𝒦 = {!!} - --- -- ℰ : ∀ {n Γ m Δ t} → Expression {n} Γ t → Term Σ Γ {m} Δ t --- -- ℰ = {!!} +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 +-- 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)) []))) +-- 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) +-- 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 new file mode 100644 index 0000000..980b85a --- /dev/null +++ b/src/Helium/Semantics/Axiomatic/Term.agda @@ -0,0 +1,322 @@ +------------------------------------------------------------------------ +-- Agda Helium +-- +-- Definition of terms for use in assertions +------------------------------------------------------------------------ + +{-# OPTIONS --safe --without-K #-} + +open import Helium.Data.Pseudocode.Types using (RawPseudocode) + +module Helium.Semantics.Axiomatic.Term + {b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃} + (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.Fin.Patterns +open import Data.Nat as ℕ using (ℕ; suc) +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.Properties as Vecₚ +open import Data.Vec.Relation.Unary.All using (All; []; _∷_) +open import Function using (_∘_; _∘₂_; id) +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 +open import Relation.Nullary using (does; yes; no; ¬_) +open import Relation.Nullary.Decidable.Core using (True; toWitness) +open import Relation.Nullary.Negation using (contradiction) + +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′ + + +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 (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 (helper ts) + where + helper : ∀ {n ts} → All (Term Σ Γ Δ) {n} ts → All (Term Σ Γ (Vec.insert Δ i _)) ts + helper [] = [] + helper (t ∷ ts) = wknMetaAt i t ∷ helper ts + +wknMeta : Term Σ Γ Δ t → Term Σ Γ (t′ ∷ Δ) t +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 + +module _ {Σ : Vec Type o} (2≉0 : ¬ 2 ℝ′.×′ 1ℝ ℝ.≈ 0ℝ) where + open Code Σ + + 𝒦 : 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 (λ (x , xs , _) → xs Vec.∷ʳ x) (𝒦 (x ′x) ∷ 𝒦 (xs ′xs) ∷ []) + 𝒦 (x ′a) = func (λ (x , _) → Vec.replicate x) (𝒦 x ∷ []) + + ℰ : 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} () + + equal : HasEquality t → ⟦ t ⟧ₜ → ⟦ t ⟧ₜ → ⟦ bool ⟧ₜ + equal bool (lift x) (lift y) = lift (does (x Bool.≟ y)) + equal int (lift x) (lift y) = lift (does (x ≟ᶻ y)) + equal fin (lift x) (lift y) = lift (does (x Fin.≟ y)) + equal real (lift x) (lift y) = lift (does (x ≟ʳ y)) + equal bit (lift x) (lift y) = lift (does (x ≟ᵇ₁ y)) + equal bits [] [] = lift (Bool.true) + equal bits (x ∷ xs) (y ∷ ys) = lift (lower (equal bit x y) Bool.∧ lower (equal bits xs ys)) + + less : IsNumeric t → ⟦ t ⟧ₜ → ⟦ t ⟧ₜ → ⟦ bool ⟧ₜ + less int (lift x) (lift y) = lift (does (x <ᶻ? y)) + less real (lift x) (lift y) = lift (does (x <ʳ? y)) + + box : ∀ t → ⟦ elemType t ⟧ₜ → ⟦ asType t 1 ⟧ₜ + box bits x = x ∷ [] + box (array t) x = x ∷ [] + + unboxed : ∀ t → ⟦ asType t 1 ⟧ₜ → ⟦ elemType t ⟧ₜ + unboxed bits (x ∷ []) = x + unboxed (array t) (x ∷ []) = x + + casted : ∀ t {i j} → .(eq : i ≡ j) → ⟦ asType t i ⟧ₜ → ⟦ asType t j ⟧ₜ + casted bits {j = 0} eq [] = [] + casted bits {j = suc j} eq (x ∷ xs) = x ∷ casted bits (ℕₚ.suc-injective eq) xs + casted (array t) {j = 0} eq [] = [] + casted (array t) {j = suc j} eq (x ∷ xs) = x ∷ casted (array t) (ℕₚ.suc-injective eq) xs + + neg : IsNumeric t → ⟦ t ⟧ₜ → ⟦ t ⟧ₜ + neg int (lift x) = lift (ℤ.- x) + neg real (lift x) = lift (ℝ.- x) + + add : (isNum₁ : True (isNumeric? t₁)) → (isNum₂ : True (isNumeric? t₂)) → ⟦ t₁ ⟧ₜ → ⟦ t₂ ⟧ₜ → ⟦ combineNumeric t₁ t₂ {isNum₁} {isNum₂} ⟧ₜ + add {int} {int} _ _ (lift x) (lift y) = lift (x ℤ.+ y) + add {int} {real} _ _ (lift x) (lift y) = lift (x /1 ℝ.+ y) + add {real} {int} _ _ (lift x) (lift y) = lift (x ℝ.+ y /1) + add {real} {real} _ _ (lift x) (lift y) = lift (x ℝ.+ y) + + mul : (isNum₁ : True (isNumeric? t₁)) → (isNum₂ : True (isNumeric? t₂)) → ⟦ t₁ ⟧ₜ → ⟦ t₂ ⟧ₜ → ⟦ combineNumeric t₁ t₂ {isNum₁} {isNum₂} ⟧ₜ + mul {int} {int} _ _ (lift x) (lift y) = lift (x ℤ.* y) + mul {int} {real} _ _ (lift x) (lift y) = lift (x /1 ℝ.* y) + mul {real} {int} _ _ (lift x) (lift y) = lift (x ℝ.* y /1) + mul {real} {real} _ _ (lift x) (lift y) = lift (x ℝ.* y) + + pow : IsNumeric t → ⟦ t ⟧ₜ → ℕ → ⟦ t ⟧ₜ + pow int (lift x) y = lift (x ℤ′.^′ y) + pow real (lift x) y = lift (x ℝ′.^′ y) + + shift : ⟦ int ⟧ₜ → ℕ → ⟦ int ⟧ₜ + shift (lift x) n = lift (⌊ x /1 ℝ.* 2≉0 ℝ.⁻¹ ℝ′.^′ n ⌋) + + flatten : ∀ {ms : Vec ℕ n} → ⟦ Vec.map fin ms ⟧ₜ′ → All Fin ms + flatten {ms = []} _ = [] + flatten {ms = _ ∷ ms} (lift x , xs) = x ∷ flatten xs + + 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 y is 0 of result + join : ∀ t → ⟦ asType t m ⟧ₜ → ⟦ asType t n ⟧ₜ → ⟦ asType t (n ℕ.+ m) ⟧ₜ + join bits xs ys = ys ++ xs + join (array t) xs ys = ys ++ xs + + take : ∀ t i {j} → ⟦ asType t (i ℕ.+ j) ⟧ₜ → ⟦ asType t i ⟧ₜ + take bits i xs = Vec.take i xs + take (array t) i xs = Vec.take i xs + + drop : ∀ t i {j} → ⟦ asType t (i ℕ.+ j) ⟧ₜ → ⟦ asType t j ⟧ₜ + drop bits i xs = Vec.drop i xs + drop (array t) i xs = Vec.drop i xs + + -- 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 (lift i) = casted t eq (join t (join t high x) low) + where + reasoning = slicedSize _ m i + k = proj₁ reasoning + n≡i+k = sym (proj₂ (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 (proj₁ (proj₂ reasoning)) + + -- i of x is 0 of first + sliced : ∀ t {m n} → ⟦ asType t (n ℕ.+ m) ⟧ₜ → ⟦ fin (suc n) ⟧ₜ → ⟦ asType t m ∷ asType t n ∷ [] ⟧ₜ′ + sliced t {m} x (lift i) = middle , casted 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) (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)) + + helper : ∀ (e : 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 (_≟_ {hasEquality = hasEq} e e₁) eq = func (λ (x , y , _) → equal (toWitness hasEq) x y) (helper e (pull-0₂ eq) ∷ helper e₁ (pull-last eq) ∷ []) + helper (_<?_ {isNumeric = isNum} e e₁) eq = func (λ (x , y , _) → less (toWitness isNum) x y) (helper e (pull-0₂ eq) ∷ helper e₁ (pull-last eq) ∷ []) + helper (Code.inv e) eq = func (λ (lift b , _) → lift (Bool.not b)) (helper e eq ∷ []) + helper (e Code.&& e₁) eq = func (λ (lift b , lift b₁ , _) → lift (b Bool.∧ b₁)) (helper e (pull-0₂ eq) ∷ helper e₁ (pull-last eq) ∷ []) + helper (e Code.|| e₁) eq = func (λ (lift b , lift b₁ , _) → lift (b Bool.∨ b₁)) (helper e (pull-0₂ eq) ∷ helper e₁ (pull-last eq) ∷ []) + helper (Code.not e) eq = func (λ (xs , _) → Vec.map (lift ∘ 𝔹.¬_ ∘ lower) xs) (helper e eq ∷ []) + helper (e Code.and e₁) eq = func (λ (xs , ys , _) → Vec.zipWith (lift ∘₂ 𝔹._∧_ ) (Vec.map lower xs) (Vec.map lower ys)) (helper e (pull-0₂ eq) ∷ helper e₁ (pull-last eq) ∷ []) + helper (e Code.or e₁) eq = func (λ (xs , ys , _) → Vec.zipWith (lift ∘₂ 𝔹._∨_ ) (Vec.map lower xs) (Vec.map lower ys)) (helper e (pull-0₂ eq) ∷ helper e₁ (pull-last eq) ∷ []) + helper ([_] {t = t} e) eq = func (λ (x , _) → box t x) (helper e eq ∷ []) + helper (Code.unbox {t = t} e) eq = func (λ (x , _) → unboxed t x) (helper e eq ∷ []) + helper (Code.splice {t = t} e e₁ e₂) eq = func (λ (x , y , i , _) → spliced t x y i) (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 = func (λ (x , i , _) → sliced t x i) (helper e (pull-0₂ eq) ∷ helper e₁ (pull-last eq) ∷ []) + helper (Code.cast {t = t} i≡j e) eq = func (λ (x , _) → casted t i≡j x) (helper e eq ∷ []) + helper (-_ {isNumeric = isNum} e) eq = func (λ (x , _) → neg (toWitness isNum) x) (helper e eq ∷ []) + helper (_+_ {isNumeric₁ = isNum₁} {isNumeric₂ = isNum₂} e e₁) eq = func (λ (x , y , _) → add isNum₁ isNum₂ x y) (helper e (pull-0₂ eq) ∷ helper e₁ (pull-last eq) ∷ []) + helper (_*_ {isNumeric₁ = isNum₁} {isNumeric₂ = isNum₂} e e₁) eq = func (λ (x , y , _) → mul isNum₁ isNum₂ x y) (helper e (pull-0₂ eq) ∷ helper e₁ (pull-last eq) ∷ []) + helper (_^_ {isNumeric = isNum} e y) eq = func (λ (x , _) → pow (toWitness isNum) x y) (helper e eq ∷ []) + helper (e >> n) eq = func (λ (x , _) → shift x n) (helper e eq ∷ []) + helper (Code.rnd e) eq = func (λ (lift x , _) → lift ⌊ x ⌋) (helper e eq ∷ []) + helper (Code.fin f e) eq = func (λ (xs , _) → lift (f (flatten xs))) (helper e eq ∷ []) + helper (Code.asInt e) eq = func (λ (lift x , _) → lift (Fin.toℕ x ℤ′.×′ 1ℤ)) (helper e eq ∷ []) + helper Code.nil eq = func (λ args → _) [] + helper (Code.cons e e₁) eq = func (λ (x , xs , _) → x , xs) (helper e (pull-0₂ eq) ∷ helper e₁ (pull-last eq) ∷ []) + helper (Code.head e) eq = func (λ ((x , _) , _) → x) (helper e eq ∷ []) + helper (Code.tail e) eq = func (λ ((_ , xs) , _) → xs) (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) ∷ []) |