module DeducteamTalk where
open import Level renaming (zero to zeroL ; suc to sucL)
open import Function
open import Data.Empty
open import Data.Unit
open import Data.Bool
open import Data.Product
open import Data.Sum
open import Data.List
open import Data.Fin hiding (lift ; _+_)
open import Data.Nat
open import Relation.Binary.PropositionalEquality
open import Enum
data Desc {ℓ} : Set (sucL ℓ) where
`K : (S : Set ℓ) → Desc
`X : Desc
_`×_ _`+_ : (D₁ D₂ : Desc) → Desc
`σ : (E : Enum)(D : EnumT E → Desc) → Desc
`Σ `Π : (S : Set ℓ)(D : S → Desc) → Desc
⟦_⟧ : ∀{ℓ} → Desc {ℓ} → Set ℓ → Set ℓ
⟦ `K S ⟧ X = S
⟦ `X ⟧ X = X
⟦ D₁ `× D₂ ⟧ X = ⟦ D₁ ⟧ X × ⟦ D₂ ⟧ X
⟦ D₁ `+ D₂ ⟧ X = ⟦ D₁ ⟧ X ⊎ ⟦ D₂ ⟧ X
⟦ `σ E D ⟧ X = σ E (λ e → ⟦ D e ⟧ X)
⟦ `Σ S D ⟧ X = Σ[ s ∈ S ] ⟦ D s ⟧ X
⟦ `Π S D ⟧ X = (s : S) → ⟦ D s ⟧ X
infixr 30 _`×_
infixr 20 _`+_
pattern `ze` = zero
pattern `su` = suc zero
NatD : Desc {zeroL}
NatD = `σ 2 (λ { `ze` → `K ⊤
; `su` → `X
; (suc (suc ())) } )
pattern `nil` = zero
pattern `cons` = suc zero
ListD : Set → Desc {zeroL}
ListD A = `σ 2 (λ { `nil` → `K ⊤
; `cons` → `Σ A (λ _ → `X)
; (suc (suc ())) })
pattern `leaf` = zero
pattern `node` = suc zero
TreeD : Set → Set → Desc {zeroL}
TreeD A B = `σ 2 λ { `leaf` → `K A
; `node` → `K B `× `X `× `X
; (suc (suc ())) }
data μ {ℓ}(D : Desc {ℓ}) : Set ℓ where
⟨_⟩ : (xs : ⟦ D ⟧ (μ D)) → μ D
module Fold {ℓ}(D : Desc {ℓ}){X : Set ℓ}
(α : ⟦ D ⟧ X → X) where
mutual
foldD : μ D → X
foldD ⟨ xs ⟩ = α (mapFoldD D xs)
mapFoldD : (D' : Desc) → ⟦ D' ⟧ (μ D) → ⟦ D' ⟧ X
mapFoldD (`K S) s = s
mapFoldD `X xs = foldD xs
mapFoldD (D₁ `× D₂) (xs₁ , xs₂) = mapFoldD D₁ xs₁ , mapFoldD D₂ xs₂
mapFoldD (D₁ `+ D₂) (inj₁ xs₁) = inj₁ (mapFoldD D₁ xs₁)
mapFoldD (D₁ `+ D₂) (inj₂ xs₂) = inj₂ (mapFoldD D₂ xs₂)
mapFoldD (`σ E D') (k , xs) = k , mapFoldD (D' k) xs
mapFoldD (`Σ S D') (s , xs) = s , mapFoldD (D' s) xs
mapFoldD (`Π S D') xs s = mapFoldD (D' s) (xs s)
open Fold
postulate
□ : ∀{ℓ k}{X : Set ℓ} → (D : Desc {ℓ}) →
(P : X → Set k) → ⟦ D ⟧ X → Set k
induction : ∀{ℓ}{D : Desc {ℓ}}{P : μ D → Set} →
(α : ∀ xs → □ D P xs → P ⟨ xs ⟩) →
(xs : μ D) → P xs
Nat' : Set
Nat' = μ NatD
ze' : Nat'
ze' = ⟨ `ze` , tt ⟩
su' : Nat' → Nat'
su' n = ⟨ `su` , n ⟩
List' : Set → Set
List' A = μ (ListD A)
nil' : ∀{A} → List' A
nil' = ⟨ `nil` , tt ⟩
cons' : ∀{A} → A → List' A → List' A
cons' a xs = ⟨ `cons` , a , xs ⟩
Tree' : Set → Set → Set
Tree' A B = μ (TreeD A B)
leaf' : ∀{A B} → A → Tree' A B
leaf' a = ⟨ `leaf` , a ⟩
node' : ∀{A B} → B → Tree' A B → Tree' A B → Tree' A B
node' b l r = ⟨ `node` , b , l , r ⟩
pattern `K` = zero
pattern `X` = suc zero
pattern `×` = suc (suc zero)
pattern `+` = suc (suc (suc zero))
pattern `σ` = suc (suc (suc (suc zero)))
pattern `Σ` = suc (suc (suc (suc (suc zero))))
pattern `Π` = suc (suc (suc (suc (suc (suc zero)))))
DescD : ∀{ℓ} → Desc {sucL ℓ}
DescD {ℓ} = `σ 7 (λ { `K` → `K (Set ℓ)
; `X` → `K (Lift ⊤)
; `×` → `X `× `X
; `+` → `X `× `X
; `σ` → `Σ (Lift Enum) λ { (lift E) →
`Π (Lift (EnumT E)) (λ _ →
`X) }
; `Σ` → `Σ (Set ℓ) λ S →
`Π (Lift S) (λ _ →
`X)
; `Π` → `Σ (Set ℓ) λ S →
`Π (Lift S) (λ _ →
`X)
; (suc (suc (suc (suc (suc (suc (suc ()))))))) })
Desc' : ∀{ℓ} → Set (sucL ℓ)
Desc' = μ DescD
`K' : ∀{ℓ} → Set ℓ → Desc' {ℓ}
`K' S = ⟨ `K` , S ⟩
`X' : ∀{ℓ} → Desc' {ℓ}
`X' = ⟨ `X` , lift tt ⟩
_`×'_ : ∀{ℓ} → Desc' {ℓ} → Desc' {ℓ} → Desc' {ℓ}
D₁ `×' D₂ = ⟨ `×` , D₁ , D₂ ⟩
_`+'_ : ∀{ℓ} → Desc' {ℓ} → Desc' {ℓ} → Desc' {ℓ}
D₁ `+' D₂ = ⟨ `+` , D₁ , D₂ ⟩
`σ' : ∀{ℓ} → (E : Enum)(T : EnumT E → Desc' {ℓ}) → Desc' {ℓ}
`σ' E T = ⟨ `σ` , lift E , T ∘ lower ⟩
`Σ' : ∀{ℓ} → (S : Set ℓ) → (S → Desc' {ℓ}) → Desc' {ℓ}
`Σ' S D = ⟨ `Σ` , S , D ∘ lower ⟩
`Π' : ∀{ℓ} → (S : Set ℓ) → (S → Desc' {ℓ}) → Desc' {ℓ}
`Π' S D = ⟨ `Π` , S , D ∘ lower ⟩
postulate
fromDescD : ∀{ℓ} → Desc {ℓ} → Desc' {ℓ}
toDescD : ∀{ℓ} → Desc' {ℓ} → Desc {ℓ}
iso-from-to : ∀{ℓ} → ∀ (D : Desc' {ℓ}) →
fromDescD (toDescD D) ≡ D
iso-to-from : ∀{ℓ} → ∀ (D : Desc {ℓ}) →
toDescD (fromDescD D) ≡ D
data RTree (A : Set) : Set where
node : A → List (RTree A) → RTree A
⟦_⟧map : ∀ {ℓ}(D : Desc) → {X Y : Set ℓ} →
(f : X → Y) → ⟦ D ⟧ X → ⟦ D ⟧ Y
⟦ `K S ⟧map f s = s
⟦ `X ⟧map f x = f x
⟦ D₁ `× D₂ ⟧map f xs = Data.Product.map (⟦ D₁ ⟧map f) (⟦ D₂ ⟧map f) xs
⟦ D₁ `+ D₂ ⟧map f xs = Data.Sum.map (⟦ D₁ ⟧map f) (⟦ D₂ ⟧map f) xs
⟦ `σ E D ⟧map f xs = σmap (λ e xs → ⟦ D e ⟧map f xs) xs
⟦ `Σ S D ⟧map f xs = Data.Product.map id (λ {s} → ⟦ D s ⟧map f) xs
⟦ `Π S D ⟧map f xs s = ⟦ D s ⟧map f (xs s)
tDesc : Set₁
tDesc = Σ[ E ∈ Enum ] (EnumT E → Desc)
⌊_⌋ : tDesc → Desc {zeroL}
⌊ (E , D) ⌋ = `σ E D
μ⌊_⌋ : tDesc → Set
μ⌊_⌋ = μ ∘ ⌊_⌋
pattern `var` = zero
[_]D* : tDesc → Set → tDesc
[ (E , D) ]D* X = (suc E) , (λ { `var` → `K X
; (suc k) → D k })
[_]* : tDesc → Set → Set
[ D ]* X = μ⌊ [ D ]D* X ⌋
module Structure {D : tDesc} where
return : ∀ {X} → X → [ D ]* X
return x = ⟨ `var` , x ⟩
fmap : ∀{X Y} → (X → Y) → [ D ]* X → [ D ]* Y
fmap {X}{Y} f xs = foldD ⌊ [ D ]D* X ⌋ apply xs
where apply : ⟦ ⌊ [ D ]D* X ⌋ ⟧ ([ D ]* Y) → [ D ]* Y
apply (zero , x) = return (f x)
apply (suc k , ys) = ⟨ suc k , ys ⟩
join : ∀{X} → [ D ]* ([ D ]* X) → [ D ]* X
join {X} xs = foldD ⌊ [ D ]D* ([ D ]* X) ⌋ help xs
where help : ⟦ ⌊ [ D ]D* ([ D ]* X) ⌋ ⟧ ([ D ]* X) → [ D ]* X
help (zero , x) = x
help (suc k , xs) = ⟨ suc k , xs ⟩
bind : ∀{X Y} → [ D ]* X → (X → [ D ]* Y) → [ D ]* Y
bind {X}{Y} dxs f = join (fmap f dxs)
open Structure
module AExpr where
pattern `val` = zero
pattern `plus` = suc zero
pattern `times` = suc (suc zero)
AExpD : tDesc
AExpD = 3 ,
λ { `val` → `K ℕ
; `plus` → `X `× `X
; `times` → `X `× `X
; (suc (suc (suc ()))) }
AExp : Set → Set
AExp V = [ AExpD ]* V
var : ∀{V} → V → AExp V
var = return
val : ∀{V} → ℕ → AExp V
val n = ⟨ suc `val` , n ⟩
plus : ∀{V} → AExp V → AExp V → AExp V
plus e₁ e₂ = ⟨ suc `plus` , e₁ , e₂ ⟩
times : ∀{V} → AExp V → AExp V → AExp V
times e₁ e₂ = ⟨ suc `times` , e₁ , e₂ ⟩
substAExpr : ∀{V W} → AExp V → (V → AExp W) → AExp W
substAExpr = bind
evalAExpr : ∀{V} → (V → ℕ) → AExp V → ℕ
evalAExpr ρ tm = help (substAExpr tm (val ∘ ρ))
where α : ⟦ ⌊ [ AExpD ]D* ⊥ ⌋ ⟧ ℕ → ℕ
α (`var` , ())
α (suc `val` , n) = n
α (suc `plus` , m , n) = m + n
α (suc `times` , m , n) = m * n
α (suc (suc (suc (suc ()))) , _)
help : AExp ⊥ → ℕ
help = foldD ⌊ [ AExpD ]D* ⊥ ⌋ α
module Eff where
pattern `get` = zero
pattern `set` = suc zero
StateSig : Set → tDesc
StateSig S = 2 , λ { `get` → `Π S λ _ → `X
; `set` → `Σ S λ _ → `X
; (suc (suc ())) }
State : Set → Set → Set
State S A = [ StateSig S ]* A
pure : ∀{S A} → A → State S A
pure = return
_>>=_ : ∀{S A B} → State S A → (A → State S B) → State S B
_>>=_ = bind
get : ∀{S} → ⊤ → State S S
get tt = ⟨ suc `get` , (λ s → return s) ⟩
set : ∀{S} → S → State S ⊤
set s = ⟨ suc `set` , s , return tt ⟩
example : State ℕ ℕ
example =
get tt >>= λ n₁ →
set (n₁ + 3) >>= λ tt →
pure n₁
∂Desc : Desc {zeroL} → Set
∂Desc (`K S) = ⊤
∂Desc `X = ⊤
∂Desc (D₁ `× D₂) = ∂Desc D₁ × ∂Desc D₂
∂Desc (D₁ `+ D₂) = ∂Desc D₁ × ∂Desc D₂
∂Desc (`σ E D) = π E (λ e → ∂Desc (D e))
∂Desc _ = ⊥
∂ : (D : Desc) → ∂Desc D → Desc {zeroL}
∂ (`K S) ∂D = `K (Lift ⊥)
∂ `X ∂D = `K ⊤
∂ (D₁ `+ D₂) (∂D₁ , ∂D₂) = ∂ D₁ ∂D₁ `+ ∂ D₂ ∂D₂
∂ (D₁ `× D₂) (∂D₁ , ∂D₂) = (∂ D₁ ∂D₁ `× D₂) `+ (D₁ `× ∂ D₂ ∂D₂)
∂ (`σ E D) ∂D = `Σ (EnumT E) (λ e → ∂ (D e) (appπ ∂D e))
∂ (`Σ S D) ()
∂ (`Π S D) ()
data Context (D : Desc){q : ∂Desc D} : Set where
root : Context D
layer : ⟦ ∂ D q ⟧ (μ D) → Context D {q} → Context D
Zipper : (D : Desc){q : ∂Desc D} → Set
Zipper D {q} = Context D {q} × μ D
plug : (D : Desc){q : ∂Desc D} → Context D {q} → μ D → μ D
plug D root t = t
plug D {q} (layer x ctxt) t = plug D {_} ctxt ⟨ plugF D {q} x t ⟩
where plugF : ∀{X} → (D : Desc){q : ∂Desc D} → ⟦ ∂ D q ⟧ X → X → ⟦ D ⟧ X
plugF (`K S) (lift ())
plugF `X tt x = x
plugF (D₁ `+ D₂) {∂D₁ , ∂D₂} (inj₁ xs₁) x = inj₁ (plugF D₁ {∂D₁} xs₁ x)
plugF (D₁ `+ D₂) {∂D₁ , ∂D₂} (inj₂ xs₂) x = inj₂ (plugF D₂ {∂D₂} xs₂ x)
plugF (D₁ `× D₂) {∂D₁ , ∂D₂} (inj₁ (∂xs₁ , xs₂)) x = plugF D₁ {∂D₁} ∂xs₁ x , xs₂
plugF (D₁ `× D₂) {∂D₁ , ∂D₂} (inj₂ (xs₁ , ∂xs₂)) x = xs₁ , plugF D₂ {∂D₂} ∂xs₂ x
plugF (`σ E D) {∂D} (e , xs) x = e , (plugF (D e) {appπ ∂D e} xs x)
plugF (`Σ S D) {()} _ _
plugF (`Π S D) {()} _ _
module ZipperTree {A B : Set} where
CTree' : (A B : Set) → Set
CTree' A B = Context (TreeD A B)
nodeL' : B → Tree' A B → CTree' A B → CTree' A B
nodeL' b l r = layer (`node` , inj₂ (b , (inj₁ (tt , l)))) r
nodeR' : B → CTree' A B → Tree' A B → CTree' A B
nodeR' b l r = layer (`node` , inj₂ (b , (inj₂ (r , tt)))) l
module Example where
open ZipperTree
example : Tree' ⊤ ℕ
example =
node' 1
(node' 2
(leaf' tt)
(leaf' tt))
(node' 5
(node' 6
(node' 7
(leaf' tt)
(leaf' tt))
(leaf' tt))
(node' 3
(leaf' tt)
(leaf' tt)))
exampleZ : Zipper (TreeD ⊤ ℕ)
exampleZ = ( nodeL' 5
(node' 3
(leaf' tt)
(leaf' tt))
(nodeR' 1
root
(node' 2
(leaf' tt)
(leaf' tt))),
node' 6
(node' 7
(leaf' tt)
(leaf' tt))
(leaf' tt))
example' : Tree' ⊤ ℕ
example' = plug (TreeD ⊤ ℕ) (proj₁ exampleZ) (proj₂ exampleZ)
test : example ≡ example'
test = refl
open import IProp
postulate
map-id : ∀ {ℓ}{X : Set ℓ} → (D : Desc {ℓ}) →
(xs : ⟦ D ⟧ X) →
⊢ ⟦ D ⟧map id xs ≡ xs
map-∘ : ∀{ℓ}{X Y Z : Set ℓ} → (D : Desc {ℓ}) →
(xs : ⟦ D ⟧ X) → (f : Y → Z)(g : X → Y) →
⊢ ⟦ D ⟧map (f ∘ g) xs ≡ (⟦ D ⟧map f ∘ ⟦ D ⟧map g) xs
postulate
bind-left-id : {X Y : Set} → (D : tDesc)
(x : X)(f : X → [ D ]* Y) →
⊢ bind (return x) f ≡ f x
bind-right-id : {X : Set} → (D : tDesc)
(xs : [ D ]* X) →
⊢ bind xs return ≡ xs
bind-∘ : {X Y Z : Set} → (D : tDesc)
(xs : [ D ]* X)(g : X → [ D ]* Y)(f : Y → [ D ]* Z) →
⊢ bind (bind xs g) f ≡ bind xs ((λ xs → bind xs f) ∘ g)
record BSig : Set₁ where
field
Op : Set
Ar : Op → Set
Bi : ∀ {sh} → Ar sh → ℕ
module Terms (Σ : BSig) where
open BSig Σ
mutual
data Tm (n : ℕ) : Set where
`var : Fin n → Tm n
`op : (sh : Op)(Xs : (pos : Ar sh) → Scope[ Bi pos ] n) → Tm n
data Scope[_] (k : ℕ)(n : ℕ) : Set where
sc : Tm (k + n) → Scope[ k ] n
Strength : Set
Strength = {l m : ℕ} → (∀{l m} → (Fin l → Fin m) → Tm l → Tm m) →
Tm l ⊎ Fin m → Tm (m + l)
module Subst (Σ : BSig)
(str : Terms.Strength Σ) where
open BSig Σ
open Terms Σ
mutual
mapSc : ∀{k l m} →
(Fin l → Fin m) → Scope[ k ] l → Scope[ k ] m
mapSc {k} ρ (sc tm) = sc (mapTm (Data.Fin.lift k ρ) tm)
mapTm : ∀{l m} →
(Fin l → Fin m) → Tm l → Tm m
mapTm ρ (`var x) = `var (ρ x)
mapTm ρ (`op sh Xs) = `op sh λ pos → mapSc {Bi pos} ρ (Xs pos)
var : ∀{m} → Fin m → Tm m
var = `var
mutual
sub : ∀{m n} → (Fin m → Tm n) → Tm m → Tm n
sub ρ (`var x) = ρ x
sub ρ (`op sh Xs) = `op sh (λ pos → weaken {Bi pos} ρ (Xs pos))
weaken : ∀{k m n} → (Fin m → Tm n) → Scope[ k ] m → Scope[ k ] n
weaken {k}{m}{n} ρ (sc tm) = sc (sub (λ v → str {n}{k} mapTm (Data.Sum.map ρ id (monFin v))) tm)
where monFin : ∀{n m} → Fin (n + m) → Fin m ⊎ Fin n
monFin {zero} xs = inj₁ xs
monFin {suc m} zero = inj₂ zero
monFin {suc m} (suc xs) with monFin {m} xs
monFin {suc m} (suc xs) | inj₁ x = inj₁ x
monFin {suc m} (suc xs) | inj₂ y = inj₂ (suc y)
module LC where
Σλam : BSig
Σλam = record { Op = Bool
; Ar = λ { true → ⊤
; false → Bool }
; Bi = λ { {true} tt → 1
; {false} b → 0 } }
open Terms Σλam
λam : ℕ → Set
λam n = Tm n
app : ∀{n} → λam n → λam n → λam n
app f s = `op false (λ { true → sc f
; false → sc s })
abs : ∀{n} → λam (suc n) → λam n
abs b = `op true (λ { tt → sc b })
str : Terms.Strength Σλam
str {m = n} fmap (inj₁ tm) = fmap (raise n) tm
str fmap (inj₂ k) = `var (inject+ _ k)
open Subst Σλam str
substλ : ∀{m n} → λam m → (Fin m → λam n) → λam n
substλ tm ρ = sub ρ tm
tm1 : λam 0
tm1 = abs (var zero)
tm2 : λam 1
tm2 = abs (app (var (suc zero)) (var zero))
tm3 : λam 0
tm3 = substλ tm2 ρ
where ρ : Fin 1 → λam 0
ρ zero = tm1
ρ (suc ())
module Equation (Σ : BSig)(str : Terms.Strength Σ) where
open Terms Σ
open Subst Σ str
postulate
sub-left-id : {m n : ℕ} →
(x : Fin m)(f : Fin m → Tm n) →
⊢ sub f (var x) ≡ f x
sub-right-id : {m : ℕ} →
(xs : Tm m) →
⊢ sub var xs ≡ xs
sub-∘ : {l m n : ℕ} →
(xs : Tm l)(g : Fin l → Tm m)(f : Fin m → Tm n) →
⊢ sub f (sub g xs) ≡ sub ((sub f) ∘ g) xs
weaken-id : {k l : ℕ} →
(xs : Scope[ k ] l) →
⊢ weaken var xs ≡ xs
weaken-∘ : {k l m n : ℕ} →
(xs : Scope[ k ] l)(g : Fin l → Tm m)(f : Fin m → Tm n) →
⊢ weaken f (weaken g xs) ≡ weaken (sub f ∘ g) xs