eval loop

src/GeneralizedPolynomial.agda

@@ -3,110 +3,78 @@
 module GeneralizedPolynomial where
 
 open import Data.Sum using (_⊎_; inj₁; inj₂)
-open import Data.Product using (_×_; _,_)
+open import Data.Product using (_×_; ∃-syntax; _,_)
 open import Relation.Binary.PropositionalEquality
-    using (_≡_; refl; cong)
-open import Function using (_∘_; id)
-open import Data.Unit using (⊤; tt)
-open import Data.Empty using (⊥)
+    using (_≡_; refl; ≢-sym)
+open import Data.Nat
+  using (ℕ; suc; _<_; _≤_; _⊔_; _+_; s≤s; z≤n; _≟_; _≤?_)
+open import Data.Nat.Properties
+  using (≤-reflexive; ≤-trans; ≤-step; n≤1+n; ≤∧≢⇒<; ≤-pred)
+open import Relation.Nullary using (¬_; yes; no)
 
-infixl 6 _⊕_
-infixl 7 _⊗_
-infixl 8 _⊙_
-
-data Polynomial : Set₁ where
-    I    : Polynomial
-    K    : Set → Polynomial
-    _⊗_ : Polynomial → Polynomial → Polynomial
-    _⊕_ : Polynomial → Polynomial → Polynomial
-    μ_   : Polynomial → Polynomial
-    ν_   : Polynomial → Polynomial
+private module ℕExtra where
+  n≤n⊔m : {n m : ℕ} → n ≤ n ⊔ m
+  n≤n⊔m {0}     {m}     = z≤n
+  n≤n⊔m {suc n} {0}     = ≤-reflexive refl
+  n≤n⊔m {suc n} {suc m} = s≤s n≤n⊔m
 
-𝟙 : Polynomial
-𝟙 = K ⊤
+  m≤n⊔m : {n m : ℕ} → m ≤ n ⊔ m
+  m≤n⊔m {0}     {m}     = ≤-reflexive refl
+  m≤n⊔m {suc n} {0}     = z≤n
+  m≤n⊔m {suc n} {suc m} = s≤s m≤n⊔m
 
-𝟘 : Polynomial
-𝟘 = K ⊥
 
-_⊙_ : Polynomial → Polynomial → Polynomial
-I        ⊙ G = G
-K x      ⊙ G = K x
-(L ⊗ R) ⊙ G = L ⊙ G ⊗ R ⊙ G
-(L ⊕ R) ⊙ G = L ⊙ G ⊕ R ⊙ G
-(μ F)    ⊙ G = μ F
-(ν F)    ⊙ G = ν F
+open ℕExtra
 
+infixl 6 _⊕_
+infixl 7 _⊗_
 
--- Fix F
--- F ⊙ F ⊙ ⋯ ⊙ F ⊙ F x
--- F ⊙ F ⊙ ⋯ ⊙ F (F x)
--- ⋯
--- F (F ⋯ (F (F x)) ⋯)
+data Polynomial : ℕ → Set₁ where
+    I_  : {n : ℕ} → (m : ℕ) → {m < n} → Polynomial n
+    K_  : {n : ℕ} → Set → Polynomial n
+    _⊗_ : {n m : ℕ} → Polynomial n → Polynomial m → Polynomial (n ⊔ m)
+    _⊕_ : {n m : ℕ} → Polynomial n → Polynomial m → Polynomial (n ⊔ m)
+    μ_  : {n : ℕ} → Polynomial (suc n) → Polynomial n
+    ν_  : {n : ℕ} → Polynomial (suc n) → Polynomial n
+
+
+data Context : ℕ → Set₁ where
+  ∅   : Context 0
+  _,[_]_ : {n m : ℕ} → Context n → (m ≤ n) → Polynomial m → Context (suc n)
+
+-- I i means to lookup the i-th position in the context from the context
+-- ∅ , a , b , c , d
+--     3   2   1   0
+lookup : {n : ℕ} → Context n → (m : ℕ) → {m < n} → ∃[ p ] Polynomial p × p < n
+lookup (ctx ,[ m≤n ] X) 0       {p}     = _ , X , s≤s m≤n
+lookup (ctx ,[ _   ] _) (suc m) {s≤s p} with lookup ctx m {p}
+... | p , X , p<n = p , X , ≤-step p<n
+
+-- ∅ , a , b , c , d (4)
+-- wk to 2
+-- ∅ , a , b
+-- A = I 0 ⊕ I 1
+-- B = I 0
+-- A ⊗ B
+weaken : ∀ {n m : ℕ} → (m ≤ n) → Context n → Context m
+weaken {0} {0} z≤z ∅ = ∅
+weaken {n} {m} m≤n ctx@(rest ,[ _ ] _) with n ≟ m
+... | yes refl = ctx
+... | no  n≢m  = weaken (≤-pred (≤∧≢⇒< m≤n (≢-sym n≢m))) rest
 
 mutual
-    ⟦_⟧ : Polynomial → Set → Set
-    ⟦ I      ⟧ x = x
-    ⟦ K k    ⟧ x = k
-    ⟦ L ⊗ R ⟧ x = ⟦ L ⟧ x × ⟦ R ⟧ x
-    ⟦ L ⊕ R ⟧ x = ⟦ L ⟧ x ⊎ ⟦ R ⟧ x
-    ⟦ μ F    ⟧ x = LeastFixpoint F
-    ⟦ ν F    ⟧ x = GreatestFixpoint F
-
-    data LeastFixpoint (F : Polynomial) : Set where
-        μ⟨_⟩ : ⟦ F ⟧ (LeastFixpoint F)  → LeastFixpoint F
-
-    record GreatestFixpoint (F : Polynomial) : Set where
-        coinductive
-        field rest : ⟦ F ⟧ (GreatestFixpoint F)
-
-
-⟦F⊙G⟧≡⟦F⟧∙⟦G⟧ : (F G : Polynomial) → ⟦ F ⊙ G ⟧ ≡ ⟦ F ⟧ ∘ ⟦ G ⟧
-⟦F⊙G⟧≡⟦F⟧∙⟦G⟧ I        G = refl
-⟦F⊙G⟧≡⟦F⟧∙⟦G⟧ (K k)    G = refl
-⟦F⊙G⟧≡⟦F⟧∙⟦G⟧ (L ⊗ R) G rewrite ⟦F⊙G⟧≡⟦F⟧∙⟦G⟧ L G
-                          rewrite ⟦F⊙G⟧≡⟦F⟧∙⟦G⟧ R G
-                          = refl
-⟦F⊙G⟧≡⟦F⟧∙⟦G⟧ (L ⊕ R) G rewrite ⟦F⊙G⟧≡⟦F⟧∙⟦G⟧ L G
-                          rewrite ⟦F⊙G⟧≡⟦F⟧∙⟦G⟧ R G
-                          = refl
-⟦F⊙G⟧≡⟦F⟧∙⟦G⟧ (μ F)    G = refl
-⟦F⊙G⟧≡⟦F⟧∙⟦G⟧ (ν F)    G = refl
-
-infixl 10 ∂_
-
-∂_ : Polynomial → Polynomial
-∂ I        = 𝟙
-∂ K k      = 𝟘
-∂ (L ⊗ R) = ∂ L ⊗ R ⊕ L ⊗ ∂ R
-∂ (L ⊕ R) = ∂ L ⊕ ∂ R
-∂ (μ P)    = inner ⊗ {!   !}
-    where inner = ∂ P ⊙ μ P
-∂ (ν P)    = {!   !}
-
-private module List where
-
-    ListF : Set → Polynomial
-    ListF A = μ (𝟙 ⊕ K A ⊗ I)
-
-    List : Set → Set
-    List A = ⟦ ListF A ⟧ ⊤
-
-    infixr 3 _∷_
-    pattern []       = μ⟨ inj₁ tt ⟩
-    pattern _∷_ x xs = μ⟨ inj₂ (x , xs) ⟩
-
-    map : ∀ {A B} → (A → B) → List A → List B
-    map f []       = []
-    map f (x ∷ xs) = f x ∷ map f xs
-
-    open import Data.Nat
-
-    _ : List ℕ
-    _ = 2 ∷ 1 ∷ 0 ∷ []
-
-
-    ListZipper : Set → Set
-    ListZipper A = ⟦ ∂ (ListF A) ⟧ ⊥
-
-    t : ∀ {A} → ListZipper A → A
-    t x = {!   !}
+  eval : {n : ℕ} → Polynomial n → Context n → Set
+  eval ((I m) {m<n}) ctx with lookup ctx m {m<n}
+  ... | p , X , s≤s p<n = eval X (weaken (≤-trans p<n (n≤1+n _)) ctx)
+  eval (K x)         ctx = x
+  eval (L ⊗ R)       ctx = eval L (weaken n≤n⊔m ctx) × eval R (weaken m≤n⊔m ctx)
+  eval (L ⊕ R)       ctx = eval L (weaken n≤n⊔m ctx) ⊎ eval R (weaken m≤n⊔m ctx)
+  eval (μ P)         ctx = LeastFixpoint P ctx
+  eval (ν P)         ctx = GreatestFixpoint P ctx
+
+  data LeastFixpoint {n : ℕ} (P : Polynomial (suc n)) (ctx : Context n) : Set where
+    μ⟨_⟩ : eval P (ctx ,[ ≤-reflexive refl ] (μ P)) → LeastFixpoint P ctx
+
+  record GreatestFixpoint {n : ℕ} (P : Polynomial (suc n)) (ctx : Context n) : Set where
+    coinductive
+    field rest : eval P (ctx ,[ ≤-reflexive refl ] (ν P))