nbe stuff

formalizations/guarded-cubical/Syntax/Nbe.agda

@@ -8,7 +8,6 @@ open import Cubical.Data.Sigma
 open import Syntax.IntensionalTerms
 open import Syntax.Types
 
-
 private
  variable
    Δ Γ Θ Z Δ' Γ' Θ' Z' : Ctx
@@ -22,12 +21,26 @@ private
    M M' M'' N N' : Comp Γ S
    E E' E'' F F' : EvCtx Γ S T
 
--- Part 1: define a presheaf semantics of contexts, i.e. every context
+-- Part 1: define a semantics of contexts, i.e. every context
 -- gets interpreted as an product of the Value presheaves
 ctx-sem : ∀ (Γ : Ctx) → (Ctx → Type (ℓ-suc ℓ-zero))
 ctx-sem [] Δ      = Unit*
 ctx-sem (A ∷ Γ) Δ = ctx-sem Γ Δ × Val Δ A
 
+data CompNF (Γ : Ctx) : (R : Ty) → Type (ℓ-suc ℓ-zero) where
+  errNF : CompNF Γ R
+  retNF : Val Γ R → CompNF Γ R
+  bindNF : Comp Γ R → CompNF (R ∷ Γ) S → CompNF Γ S
+  tickNF : CompNF Γ R → CompNF Γ R
+  neuNF : Comp Γ R → CompNF Γ R
+
+bindNF' : CompNF Γ R → CompNF (R ∷ Γ) S → CompNF Γ S
+bindNF' errNF K = errNF
+bindNF' (retNF x) K = {!K [ ids ,s x ]cnf!}
+bindNF' (bindNF x Mnf) K = {!!}
+bindNF' (tickNF Mnf) K = tickNF (bindNF' Mnf K)
+bindNF' (neuNF x) K = neuNF {!!}
+
 _[_]sem : ctx-sem Γ Δ → Subst Θ Δ → ctx-sem Γ Θ
 _[_]sem {Γ = []} tt* δ = tt*
 _[_]sem {Γ = x ∷ Γ} (γ~ , v) δ = (γ~ [ δ ]sem) , (v [ δ ]v)
@@ -57,6 +70,48 @@ reflect<-reify≡id {Γ = x ∷ Γ} γ~ = ΣPathP (cong reflect wkβ ∙ reflect
 -- Part 3: give a semantics of terms as "polymorphic transformations"
 -- These will all end up being natural but fortunately we don't need that.
 
+ev-sem' : EvCtx Γ R S → ∀ {Θ} → ctx-sem Γ Θ → CompNF Θ R → CompNF Θ S
+comp-sem' : Comp Γ R → ∀ {Θ} → ctx-sem Γ Θ → CompNF Θ R
+
+ev-sem' ∙E x M~ = M~
+ev-sem' (E ∘E E₁) x M~ = {!!}
+ev-sem' (∘IdL i) x M~ = {!!}
+ev-sem' (∘IdR i) x M~ = {!!}
+ev-sem' (∘Assoc i) x M~ = {!!}
+ev-sem' (E [ x₁ ]e) x M~ = {!!}
+ev-sem' (substId i) x M~ = {!!}
+ev-sem' (substAssoc i) x M~ = {!!}
+ev-sem' (∙substDist i) x M~ = {!!}
+ev-sem' (∘substDist i) x M~ = {!!}
+ev-sem' (bind N[x]) x M~ = {!!}
+ev-sem' (ret-η i) x M~ = {!!}
+ev-sem' (isSetEvCtx E E₁ x₁ y i i₁) x M~ = {!!}
+
+comp-sem' (E [ M ]∙) x = {!!}
+comp-sem' (plugId i) x = {!!}
+comp-sem' (plugAssoc i) x = {!!}
+comp-sem' (M [ x₁ ]c) x = {!!}
+comp-sem' (substId i) x = {!!}
+comp-sem' (substAssoc i) x = {!!}
+comp-sem' (substPlugDist i) x = {!!}
+comp-sem' err x = {!!}
+comp-sem' (strictness i) x = {!!}
+comp-sem' ret x = {!!}
+comp-sem' (ret-β i) x = {!!}
+comp-sem' app x = {!!}
+comp-sem' (fun-β i) x = {!!}
+comp-sem' (matchNat M M₁) x = {!!}
+comp-sem' (matchNatβz M M₁ i) x = {!!}
+comp-sem' (matchNatβs M M₁ V i) x = {!!}
+comp-sem' (matchNatη i) x = {!!}
+comp-sem' (matchDyn M M₁) x = {!!}
+comp-sem' (matchDynβn M M₁ V i) x = {!!}
+comp-sem' (matchDynβf M M₁ V i) x = {!!}
+comp-sem' (tick M) x = {!!}
+comp-sem' (tick-strictness i) x = {!!}
+comp-sem' (isSetComp M M₁ x₁ y i i₁) x = {!!}
+
+
 subst-sem : Subst Δ Γ → ∀ {Θ} → ctx-sem Δ Θ → ctx-sem Γ Θ
 val-sem : Val Γ R → ∀ {Θ} → ctx-sem Γ Θ → Val Θ R
 comp-sem : Comp Γ R → ∀ {Θ} → ctx-sem Γ Θ → Comp Θ R
@@ -69,28 +124,29 @@ subst-sem (γ ,s v) x = (subst-sem γ x) , (val-sem v x)
 subst-sem wk = fst
 
 -- these equations should essentially hold by refl
-subst-sem ([]η i) = {!!}
-subst-sem (∘IdL i) = {!!}
+subst-sem ([]η i) = λ _ → tt*
+subst-sem (∘IdL {γ = γ} i) = subst-sem γ
 subst-sem (∘IdR i) = {!!}
 subst-sem (∘Assoc i) = {!!}
-subst-sem (isSetSubst γ γ₁ x y i i₁) = {!!}
 subst-sem (wkβ i) = {!!}
 subst-sem (,sη i) = {!!}
+subst-sem (isSetSubst γ γ₁ x y i i₁) = {!!}
 
 val-sem (V [ γ ]v) x = val-sem V (subst-sem γ x)
 val-sem var x = x .snd
 val-sem zro x = zro [ !s ]v
 val-sem suc (_ , n) = suc [ !s ,s n ]v
 val-sem (lda M[x]) x = lda (comp-sem M[x] ((x [ wk ]sem) , var))
+
 val-sem injectN x = {!!}
 val-sem (injectArr V) x = {!!}
 val-sem (mapDyn V V₁) x = {!!}
 
 -- don't bother proving these until you have to
-val-sem (fun-η i) x = {!!}
 val-sem (varβ i) x = {!!}
 val-sem (substId i) x = {!!}
 val-sem (substAssoc i) x = {!!}
+val-sem (fun-η i) x = {!!}
 val-sem (isSetVal V V₁ x₁ y i i₁) x = {!!}
 
 comp-sem (E [ M ]∙) x = ev-sem E x (comp-sem M x)
@@ -114,6 +170,7 @@ comp-sem (substId i) x = {!!}
 comp-sem (substAssoc i) x = {!!}
 comp-sem (substPlugDist i) x = {!!}
 comp-sem (strictness i) x = {!!}
+
 comp-sem (ret-β i) x = {!!}
 comp-sem (fun-β i) x = {!!}
 comp-sem (matchNatβz M M₁ i) x = {!!}
@@ -128,13 +185,15 @@ ev-sem ∙E x M = M
 ev-sem (E ∘E E₁) x M = ev-sem E x (ev-sem E₁ x M)
 ev-sem (E [ γ ]e) x M = ev-sem E (subst-sem γ x) M
 ev-sem (bind K) x M = bind (comp-sem K ((x [ wk ]sem) , var)) [ M ]∙
+
 ev-sem (∘IdL i) x M = {!!}
 ev-sem (∘IdR i) x M = {!!}
 ev-sem (∘Assoc i) x M = {!!}
 ev-sem (substId i) x M = {!!}
 ev-sem (substAssoc i) x M = {!!}
-ev-sem (∙substDist i) x M = {!!}
+ev-sem (∙substDist i) x M = M
 ev-sem (∘substDist i) x M = {!!}
+
 ev-sem (ret-η i) x M = {!!}
 ev-sem (isSetEvCtx E E₁ x₁ y i i₁) x M = {!!}
 
@@ -152,7 +211,7 @@ subst-correct (γ ∘s γ') δ~ = sym ∘Assoc
   ∙ subst-correct γ _
 subst-correct !s δ~ = []η
 -- This is the naturality of ,s we discussed
-subst-correct (γ ,s x) δ~ = {!!}
+subst-correct (γ ,s v) δ~ = {!!}
 subst-correct wk δ~ = wkβ
 -- This all should follow by isSet stuff
 subst-correct (∘IdL i) δ~ = {!!}