From 9cef0fa6915e02897a134b93a389feb866efac1b Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Sun, 22 Dec 2024 16:56:29 -0600
Subject: [PATCH] wip

---
 src/AOP/NBE.agda            | 26 +++++++++++++++---
 src/AOP/palindromes.agda    | 53 +++++++++++++++++++++++++++++++++++++
 src/ThesisWork/EMSpace.agda | 11 ++++----
 3 files changed, 82 insertions(+), 8 deletions(-)
 create mode 100644 src/AOP/palindromes.agda

diff --git a/src/AOP/NBE.agda b/src/AOP/NBE.agda
index c9013fd..982c6ec 100644
--- a/src/AOP/NBE.agda
+++ b/src/AOP/NBE.agda
@@ -45,11 +45,15 @@ _ = ≈-trans add-zero add-zero
 
 -- phase 1: evaluation
 eval : SNat → ℕ
-eval x = {!!}
+eval zero = 0
+eval one = 1
+eval (add x y) = (eval x) + (eval y)
 
 -- phase 2: reification
 reify : ℕ → SNat
-reify n = {!!}
+reify zero = zero
+reify (suc zero) = one
+reify (2+ n) = add one (add one (reify n))
 
 -- optimisation is just composition! hurray!
 optimise : SNat → SNat
@@ -57,4 +61,20 @@ optimise x = reify (eval x)
 
 -- phase 3: correctness
 correct : ∀ x → optimise x ≈ x
-correct x = {!!}
+correct zero = ≈-refl
+correct one = ≈-refl
+correct (add x y) = ≈-trans (lemma x y) (≈-cong (correct x) (correct y)) where
+  lemma : ∀ (x y : SNat) → optimise (add x y) ≈ add (optimise x) (optimise y)
+  lemma zero y = ≈-sym add-zero
+  lemma one zero = ≈-trans (≈-sym add-zero) (≈-sym add-one)
+  lemma one one = ≈-cong ≈-refl (≈-trans add-one add-zero)
+  lemma one (add x y) = {!   !}
+    -- optimize (add one (add x y))
+    -- add (optimize one) (add (optimize x) (optimize y))
+    -- add (optimize one) (optimize (add x y))
+  lemma (add x y) z = {!   !}
+    -- optimise (add (add x y) z) 
+    -- add (add x y) z
+    -- add (add x y) (optimise z)
+    -- add (add (optimize x) (optimize y)) (optimise z)
+    -- add (optimise (add x y)) (optimise z)
diff --git a/src/AOP/palindromes.agda b/src/AOP/palindromes.agda
new file mode 100644
index 0000000..fe29c25
--- /dev/null
+++ b/src/AOP/palindromes.agda
@@ -0,0 +1,53 @@
+open import Data.Nat
+open import Data.Nat.Properties
+open import Relation.Binary.PropositionalEquality hiding ([_])
+open ≡-Reasoning
+
+infixr 5 _∷_
+
+data Vec (A : Set) : ℕ → Set where 
+    [] : Vec A 0
+    _∷_ : ∀{n} → A → Vec A n → Vec A (suc n)
+
+snoc : ∀{A : Set}{n} → Vec A n → A → Vec A (suc n)
+snoc [] x = x ∷ []
+snoc (x₁ ∷ xs) x = x₁ ∷ snoc xs x
+
+rev : ∀{A : Set}{n} → Vec A n → Vec A n
+rev [] = []
+rev (x ∷ xs) = snoc (rev xs) x
+
+tail : ∀{A : Set}{n} → Vec A (suc n) → Vec A n
+tail (x ∷ xs) = xs
+
+init : ∀{A : Set}{n} → Vec A (suc n) → Vec A n
+init (x ∷ []) = []
+init (x ∷ x₁ ∷ xs) = x ∷ init (x₁ ∷ xs)
+
+last : ∀{A : Set}{n} → Vec A (suc n) → A
+last (x ∷ []) = x
+last (x ∷ x₁ ∷ xs) = last (x₁ ∷ xs)
+
+module _(X : Set) where
+  data IsPalindrome : {n : ℕ} → Vec X n → Set where
+    empty : IsPalindrome []
+    one   : ∀{x} → IsPalindrome (x ∷ [])
+    more  : ∀{n}{x}{xs : Vec X n} → IsPalindrome xs → IsPalindrome (snoc (x ∷ xs) x)
+
+  proof₁ : ∀{n}{xs : Vec X n} → IsPalindrome xs → rev xs ≡ xs
+  proof₁ empty = refl
+  proof₁ one = refl
+  proof₁ {n} (more {x = x} {xs} p) = helper where
+    helper2 : ∀ {x} {xs} → rev (snoc xs x) ≡ x ∷ xs
+    helper2 {x} {[]} = refl
+    helper2 {x} {y ∷ xs} = {!   !}
+    -- rev (snoc xs x) ≡⟨ {!   !} ⟩ x ∷ rev xs ≡⟨ cong (x ∷_) (proof₁ p) ⟩ x ∷ xs ∎
+    helper =
+      snoc (rev (snoc xs x)) x ≡⟨ cong (λ z → snoc z x) helper2 ⟩
+      snoc (x ∷ xs) x ≡⟨ refl ⟩
+      x ∷ snoc xs x ∎
+ 
+  proof₂ : ∀{n}{xs : Vec X n} → rev xs ≡ xs → IsPalindrome xs
+  proof₂ {n} {[]} x = empty 
+  proof₂ {n} {a ∷ []} refl = one  
+  proof₂ {n} {a ∷ b ∷ xs} p = let IH = proof₂ p in {!   !} 
\ No newline at end of file
diff --git a/src/ThesisWork/EMSpace.agda b/src/ThesisWork/EMSpace.agda
index bd7025a..787ee28 100644
--- a/src/ThesisWork/EMSpace.agda
+++ b/src/ThesisWork/EMSpace.agda
@@ -40,10 +40,10 @@ module _ where
   test : S¹ ≃ K[ ℤGroup ,1]
   test = isoToEquiv (iso f g {!   !} {!   !}) where
     loop^_ : ℤ → S¹-base ≡ S¹-base
-    loop^ pos (suc n) = (loop^ (pos n)) ∙ S¹-loop
-    loop^ pos zero = refl
-    loop^ negsuc zero = sym S¹-loop
-    loop^ negsuc (suc n) = (loop^ (negsuc n)) ∙ sym S¹-loop
+    -- loop^ pos (suc n) = (loop^ (pos n)) ∙ S¹-loop
+    -- loop^ pos zero = refl
+    -- loop^ negsuc zero = sym S¹-loop
+    -- loop^ negsuc (suc n) = (loop^ (negsuc n)) ∙ sym S¹-loop
 
     Code1 : S¹ → Type
     Code1 S¹-base = ℤ
@@ -117,11 +117,12 @@ module _ (G : Group ℓ) where
     CodesFunc : ⟨ G ⟩ → ⟨ G ⟩ ≃ ⟨ G ⟩
     CodesFunc g = {!   !}
 
-    Codes' : K1 G → hSet ℓ
+    Codes' : K[ G ,1] → hSet ℓ
     Codes' base = ⟨ G ⟩ , is-set
     Codes' (loop x i) = ⟨ G ⟩ , is-set
     Codes' (loop-1g i i₁) = {!   !}
     Codes' (loop-∙ x y i i₁) = {!   !}
+    Codes' x = ?
 
   module _ where
     _ : (x y : ⟨ G ⟩) → subst {! λ x → Codes x .snd  !} {!   !} {!   !} ≡ {!   !}