\documentclass{beamer}
\usetheme{uucs}
%\usepackage[debug]{polytable}

%include colorcode.fmt
%include agda.fmt
%subst space = "\ "
%include beamer.fmt
%include spacing.fmt
\renewcommand\Keyword[1]{\textbf{\color{uuxgreen}{#1}}}

\barhs
\setlength{\coderulewidth}{1.5pt}
\setbeamercolor{alerted text}{fg=uuxgreen}
\colorlet{codecolor}{uuxred}
\renewcommand\hscodestyle{\small}
\newcommand\Constructor[1]{{\color{uuyblue}\Conid{#1}}}

\usepackage{cmbright}
\usepackage{pifont}

\title{Indexed fixed points}
\author{Andres L\"oh}
\institute{%
  Dept.\ of Information and Computing Sciences, Utrecht University\\%
  P.O.\ Box 80.089, 3508 TB Utrecht, The Netherlands\\%
  Web pages: \url{http://www.cs.uu.nl/wiki/Center}}
\date{GP meeting, 21 November 2008}

\newcommand\makeboxx[2]{%
  {%
  \setbox0\hbox{\(#1\)}%
  \makebox[\wd0]{#2}%
  }%
}
\newcommand\makebold[1]{%
  {\let\Varid\textbf #1}%
}
\newcommand\centercolumn[1]{%
  \aligncolumn{#1}{@@{}>{\hspre}c<{\hspost}@@{}}}
\newcommand\rightcolumn[1]{%
  \aligncolumn{#1}{@@{}>{\hspre}r<{\hspost}@@{}}}

\DeclareUnicodeCharacter{9312}{\ding{192}}
\DeclareUnicodeCharacter{9313}{\ding{193}}
\DeclareUnicodeCharacter{9314}{\ding{194}}
\DeclareUnicodeCharacter{9655}{\ensuremath{\rhd}}
\DeclareUnicodeCharacter{8788}{\ensuremath{\mathbin{\colon\!\!\!\!=}}}

\begin{document}
\frontmatter

\begin{frame}
  \titlepage
\end{frame}

\mainmatter

\begin{frame}{Fixed points}
%format * = "\mathord{\ast}"
%format -> = "\mathbin{\rightarrow}"
%format Fix_n
%format ? = "{\color{uuxgreen}\textbf{?}}"
%format => = "\mathbin{\makeboxx{" -> "}{$\only<1>{" -> "}\only<2->{" × "}$}}"
\saverestorecolumns
\only<1-2>{%
\begin{spec}
Fix₁   :  (*  ->  *) -> 
          *

Fix₂   :  (*  =>  * -> *) => 
          (*  =>  * -> *) ->
          *

Fix₃   :  (*  =>  *  =>  * -> *) => 
          (*  =>  *  =>  * -> *) =>
          (*  =>  *  =>  * -> *) ->
          *

Fix_n  :  ?
\end{spec}
}\only<3->{%
\restorecolumns
%format (EXP m (n)) = "\only<1-4>{{" m "^{" n "}}}\only<5->{{"( "\makebold{ " n "}" ^^ -> ^^ m )"}}"
%format (FOUR (x)) = "\only<1-3>{" ? "}\only<4->{" x "}"
%format IGNORE x = x
\begin{spec}
Fix₁   :  (EXP ((EXP * (1) -> *)) (1)) -> *
^

Fix₂   :  (EXP ((EXP * (2) -> *)) (2)) -> *
^
^

Fix₃   :  (EXP ((EXP * (3) -> *)) (3)) -> *
^         
^
^

Fix_n  :  (FOUR (IGNORE (EXP ((EXP * (n) -> *)) (n)) -> *))
\end{spec}
}%

How to generalize to arbitrary arities?

\uncover<2->{\alert<2>{① Uncurry}}
\uncover<3->{--- \alert<3-4>{② Simplify}}
\uncover<5->{--- \alert<5>{③ Index}}
\end{frame}

\resetsavecolumns

\begin{frame}{Agda vs.~Haskell}

%format FIN n = "{\makebold{" n "}}"
%format (EXP m (n)) = "{"( n ^^ -> ^^ m )"}"
\begin{spec}
Fix_n  :  (EXP ((EXP * (FIN n) -> *)) (FIN n)) -> *
\end{spec}

Agda:
%format FIN n = Fin ^^ n
\begin{spec}
Fix  :  (n : ℕ) -> (EXP ((EXP * (FIN n) -> *)) (FIN n)) -> *
\end{spec}

Haskell:
%format FIN n = "\alert{" * "}"
\begin{spec}
Fix  ::  (EXP ((EXP * (FIN n) -> *)) (FIN n)) -> *
\end{spec}
where |FIN n| is instantiated by a suitable index type.

\end{frame}

\begin{frame}{Adding projection}

Describes the complete family:
%format (FIN n) = "{\makebold{" n "}}"
\begin{spec}
Fix_n  :  (EXP ((EXP * (FIN n) -> *)) (FIN n)) -> *
\end{spec}
Projecting out one type:
\begin{spec}
Fix_n  :  (EXP ((EXP * (FIN n) -> *)) (FIN n)) -> (FIN n) -> *
\end{spec}
\pause
Agda:
%format (FIN n) = Fin ^^ n
\begin{spec}
Fix  :  (n : ℕ) ->  (EXP ((EXP * (FIN n) -> *)) (FIN n))
                    ^^^ ^^^ ^^^^ ^^^^ ^^^^   -> (FIN n) -> *
\end{spec}
Haskell:
%format (FIN n) = "\alert{" * "}"
\begin{spec}
Fix  ::  (EXP ((EXP * (FIN n) -> *)) (FIN n)) -> (FIN n) -> *
\end{spec}

\end{frame}

%if style == newcode
\begin{code}
module IndexFix where

open import Data.Bool
open import Data.Nat hiding (fold; _≟_)
open import Data.Sum
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Data.List renaming (map to lmap)
open import Data.Unit
open import Data.String using (String; _≟_)
open import Data.Empty
open import Data.Maybe
open import Data.Function
open import Category.Functor
open import Category.Monad
open import Data.Fin hiding (fold; _+_)
open import Data.Star hiding (map; fold; _>>=_)
                      renaming (ε to []; _◅_ to _∷_;
                                return to [_])
open import Relation.Binary
\end{code}
%endif

\begin{frame}{The universe}

%format Set1
%format I = "{\color{uuxred}\textbf{I}}"
%format K = "{\color{uuxred}\textbf{K}}"
%format _⊕_ = "{\char95{\color{uuxred}+}\char95}"
%format _⊗_ = "{\char95{\color{uuxred}×}\char95}"
%format _▷_ = "{\char95{\color{uuxred}▷}\char95}"
%format ⊕ = "\mathbin{\color{uuxred}+}"
%format ⊗ = "\mathbin{\color{uuxred}×}"
%format ▷ = "\mathbin{\color{uuxred}▷}"
%format FC = "{\color{uuxred}\Varid{FC}}"
%format C  = "{\color{uuxred}\Varid{C}}"
%format C₁ = "{\color{uuxred}\Varid{C₁}}"
%format C₂ = "{\color{uuxred}\Varid{C₂}}"
%if True
%format econst = "\Constructor{econst}"
%format eadd   = "\Constructor{eadd}"
%format emul   = "\Constructor{emul}"
%format evar   = "\Constructor{evar}"
%format elet   = "\Constructor{elet}"
%format vexpr  = "\Constructor{vexpr}"
%format vdecl  = "\Constructor{vdecl}"
%format vvar   = "\Constructor{vvar}"
%format inj₁   = "\Constructor{inj₁}"
%format inj₂   = "\Constructor{inj₂}"
%format ,      = "\mathpunct{\Constructor{,}}"
% format _,_    = "\Constructor{\char95{,}\char95}"
%format ≡-refl = "\Constructor{≡-refl}"
%format ≔      = "\Constructor{≔}"
%format ∙      = "\Constructor{∙}"
%format _≔_    = "\Constructor{\char95{≔}\char95}"
%format _∙_    = "\Constructor{\char95{∙}\char95}"
%format [      = "\Constructor{[\,}"
%format ]      = "\Constructor{]}"
%format ∷      = "\Constructor{∷}"
%format nothing = "\Constructor{nothing}"
%format just   = "\Constructor{just}"
%endif
\begin{joincode}
\onslide<1->%
\begin{code}
module Base (n : ℕ) where

  Ix = Fin n
\end{code}
\begin{spec}
^
\end{spec}
\onslide<2->%
\centercolumn{5}%
\rightcolumn{13}%
\begin{code}
  data Code : Set1 where
    I    :  Ix             -> Code
    K    :  Set            -> Code
    _⊕_  :  Code -> Code   -> Code
    _⊗_  :  Code -> Code   -> Code
    _▷_  :  Code -> Ix     -> Code
\end{code}
\begin{spec}
^
\end{spec}
\onslide<3->%
\centercolumn{6}%
\centercolumn{18}%
\centercolumn{23}%
\centercolumn{41}%
\begin{code}
  ⟦_⟧ : Code -> (Ix -> Set) -> Ix -> Set
  ⟦  I x      ⟧  ⟨_⟩  _  =  ⟨ x ⟩
  ⟦  K A      ⟧  _    _  =  A
  ⟦  C₁ ⊕ C₂  ⟧  ⟨_⟩  y  =  ⟦ C₁ ⟧ ⟨_⟩ y  ⊎  ⟦  C₂  ⟧ ⟨_⟩ y
  ⟦  C₁ ⊗ C₂  ⟧  ⟨_⟩  y  =  ⟦ C₁ ⟧ ⟨_⟩ y  ×  ⟦  C₂  ⟧ ⟨_⟩ y
  ⟦  C ▷ x    ⟧  ⟨_⟩  y  =  x ≡ y         ×  ⟦  C   ⟧ ⟨_⟩ y
\end{code}
\end{joincode}

\end{frame}

%if style == newcode
\begin{code}
  infixr 6 _⊗_
  infixr 4 _⊕_
  infix  5 _▷_
\end{code}
%endif

\begin{frame}{Generic map}

\centercolumn{6}%
\centercolumn{18}%
\centercolumn{23}%
\centercolumn{41}%
\begingroup
\colorlet{codecolor}{uuyblue}
\begin{spec}
  ⟦_⟧ : Code -> (Ix -> Set) -> Ix -> Set
  ⟦  I x      ⟧  ⟨_⟩  _  =  ⟨ x ⟩
  ⟦  K A      ⟧  _    _  =  A
  ⟦  C₁ ⊕ C₂  ⟧  ⟨_⟩  y  =  ⟦ C₁ ⟧ ⟨_⟩ y  ⊎  ⟦  C₂  ⟧ ⟨_⟩ y
  ⟦  C₁ ⊗ C₂  ⟧  ⟨_⟩  y  =  ⟦ C₁ ⟧ ⟨_⟩ y  ×  ⟦  C₂  ⟧ ⟨_⟩ y
  ⟦  C ▷ x    ⟧  ⟨_⟩  y  =  x ≡ y         ×  ⟦  C   ⟧ ⟨_⟩ y
\end{spec}
\endgroup
\centercolumn{10}
\begin{code}
  map :   {F G : Ix -> Set} {y : Ix} -> (C : Code) ->
          ({x : Ix} -> F x -> G x) -> ⟦ C ⟧ F y -> ⟦ C ⟧ G y
  map (  I x      )  f  y             =  f y
  map (  K _      )  f  y             =  y
  map (  C₁ ⊕ C₂  )  f  (inj₁ y₁)     =  inj₁ (map C₁ f y₁)
  map (  C₁ ⊕ C₂  )  f  (inj₂ y₂)     =  inj₂ (map C₂ f y₂)
  map (  C₁ ⊗ C₂  )  f  (y₁ , y₂)     =  map C₁ f y₁ , map C₂ f y₂
  map (  C ▷ x    )  f  (≡-refl , y)  =  ≡-refl , map C f y
\end{code}

\end{frame}

\begin{frame}{Embedding-projection}

Lets group everything required to allow generic programming
for a family of types in a record:
\begin{code}
  record Fam : Set1 where
    field
      FC    :  Code
      ⟨_⟩   :  Ix -> Set
      from  :  {x : Ix} -> ⟨ x ⟩ -> ⟦ FC ⟧ ⟨_⟩ x
      to    :  {x : Ix} -> ⟦ FC ⟧ ⟨_⟩ x -> ⟨ x ⟩
\end{code}

\pause
Boilerplate to write:
\begin{dingautolist}{192}
\item The |Code| for the family.
\item The interpretation function |⟨_⟩|.
\item Conversion functions |from| and |to|.
\end{dingautolist}

\end{frame}

\begin{frame}{ASTs}

\centercolumn{7}%
\centercolumn{8}%
\rightcolumn{18}%
\begin{code}
module AST where

  Var  :  Set
  Var  =  String

  mutual
    data Expr : Set where
      econst  :  ℕ             -> Expr
      eadd    :  Expr -> Expr  -> Expr
      emul    :  Expr -> Expr  -> Expr
      evar    :  Var           -> Expr
      elet    :  Decl -> Expr  -> Expr

    data Decl : Set where
      _≔_     :  Var -> Expr   -> Decl
      _∙_     :  Decl -> Decl  -> Decl
\end{code}
%if style == newcode
\begin{code}
  infixr 3 _≔_
  infixl 2 _∙_
\end{code}
%endif

\end{frame}

\begin{frame}{Instantiating |Fam| --- preliminaries}

\saverestorecolumns
\invisiblecomments

\begin{code}

  open Base 3

\end{code}
A view is not necessary, but nice to have:
\restorecolumns
\begin{code}
  expr  =  zero
  decl  =  suc zero
  var   =  suc (suc zero)

  data ViewAST : Ix -> Set where
    vexpr  :  ViewAST expr
    vdecl  :  ViewAST decl
    vvar   :  ViewAST var
  
  viewAST : (n : Ix) -> ViewAST n
  viewAST zero                  =  vexpr
  viewAST (suc zero)            =  vdecl
  viewAST (suc (suc zero))      =  vvar
  viewAST (suc (suc (suc ())))  --
\end{code}

\end{frame}

\resetsavecolumns

\begin{frame}{Instantiating |Fam| --- codes}

\centercolumn{10}%
%format FC = "{\color{uuxred}\Varid{FC}}"
%format ExprC = "{\color{uuxred}\Varid{ExprC}}"
%format DeclC = "{\color{uuxred}\Varid{DeclC}}"
%format VarC  = "{\color{uuxred}\Varid{DeclC}}"
%format ASTC  = "{\color{uuxred}\Varid{ASTC}}"
\begin{code}
  ExprC  :  Code
  ExprC  =  K ℕ                  -- |econst|
         ⊕  I expr  ⊗  I expr    -- |eadd|
         ⊕  I expr  ⊗  I expr    -- |emul|
         ⊕  I var                -- |evar|
         ⊕  I decl  ⊗  I expr    -- |elet|
  
  DeclC  :  Code
  DeclC  =  I var   ⊗  I expr    -- |_≔_|
         ⊕  I decl  ⊗  I decl    -- |_∙_|

  VarC   :  Code
  VarC   =  K String
  
  ASTC   :  Code
  ASTC   =  ExprC  ▷  expr
         ⊕  DeclC  ▷  decl
         ⊕  VarC   ▷  var
\end{code}

\end{frame}

\begin{frame}{Instantiating |Fam| -- interpretation}

\centercolumn{9}%
%format (. (x)) = "{\color{uuxsilver}\textbf{.}" x "}"
\begin{code}
  AST⟨_⟩ : Ix -> Set
  AST⟨  x      ⟩ with viewAST x
  AST⟨  (. _)  ⟩ | vexpr  =  Expr
  AST⟨  (. _)  ⟩ | vdecl  =  Decl
  AST⟨  (. _)  ⟩ | vvar   =  Var
\end{code}

\end{frame}

\begin{frame}{Instantiating |Fam| -- conversions}

\vspace*{-.5\baselineskip}%
\centercolumn{18}%
\begin{code}
  fromExpr : Expr -> ⟦ ExprC ⟧ AST⟨_⟩ expr
  fromExpr  (econst i       )  =  inj₁                    i
  fromExpr  (eadd   e₁  e₂  )  =  inj₂ (inj₁              (e₁  ,  e₂  )  )
  fromExpr  (emul   e₁  e₂  )  =  inj₂ (inj₂ (inj₁        (e₁  ,  e₂  )  ))
  fromExpr  (evar   v       )  =  inj₂ (inj₂ (inj₂ (inj₁  v              )))
  fromExpr  (elet   d   e   )  =  inj₂ (inj₂ (inj₂ (inj₂  (d   ,  e   )  )))
  
  fromDecl : Decl -> ⟦ DeclC ⟧ AST⟨_⟩ decl
  fromDecl  (v   ≔   e   )   =  inj₁  (v , e)
  fromDecl  (d₁  ∙   d₂  )   =  inj₂  (d₁ , d₂)

  fromVar : Var -> ⟦ VarC ⟧ AST⟨_⟩ var
  fromVar v = v
  
  fromAST : {x : Ix} -> AST⟨ x ⟩ -> ⟦ ASTC ⟧ AST⟨_⟩ x
  fromAST {x} v with viewAST x
  fromAST e  |  vexpr  =  inj₁          (≡-refl , fromExpr   e  ) 
  fromAST d  |  vdecl  =  inj₂ (inj₁    (≡-refl , fromDecl   d  ))
  fromAST v  |  vvar   =  inj₂ (inj₂    (≡-refl , fromVar    v  ))
\end{code}

\end{frame}

\begin{frame}{Instantiating |Fam| -- conversions}

\vspace*{-.5\baselineskip}%
\centercolumn{41}%
\begin{code}
  toExpr : ⟦ ExprC ⟧ AST⟨_⟩ expr -> Expr
  toExpr (inj₁                    i              )     =  econst i
  toExpr (inj₂ (inj₁              (e₁  ,  e₂  )  ))    =  eadd e₁ e₂
  toExpr (inj₂ (inj₂ (inj₁        (e₁  ,  e₂  )  )))   =  emul e₁ e₂
  toExpr (inj₂ (inj₂ (inj₂ (inj₁  v              ))))  =  evar v
  toExpr (inj₂ (inj₂ (inj₂ (inj₂  (d   ,  e   )  ))))  =  elet d e

  toDecl : ⟦ DeclC ⟧ AST⟨_⟩ decl -> Decl
  toDecl (inj₁  (v    ,  e   ))  =  v   ≔   e
  toDecl (inj₂  (d₁   ,  d₂  ))  =  d₁  ∙   d₂

  toVar : ⟦ VarC ⟧ AST⟨_⟩ var -> Var
  toVar v = v

  toAST : {x : Ix} -> ⟦ ASTC ⟧ AST⟨_⟩ x -> AST⟨ x ⟩
  toAST (inj₁        (≡-refl  ,    e  ))   =   toExpr e
  toAST (inj₂ (inj₁  (≡-refl  ,    d  )))  =   toDecl d
  toAST (inj₂ (inj₂  (≡-refl  ,    v  )))  =   toVar v
\end{code}

\end{frame}

\begin{frame}{Instantiating |Fam| -- finalization}

\begin{code}
  AST : Fam
  AST = record
          {  FC    =  ASTC
          ;  ⟨_⟩   =  AST⟨_⟩
          ;  from  =  fromAST
          ;  to    =  toAST
          }
\end{code}

\end{frame}

\begin{frame}{Generic fold -- algebras}

\centercolumn{10}%
\begin{code}
module Fold {n : ℕ} (F : Base.Fam n) where

  open Base n public
  open Fam F

  RawAlg : Code -> (F G : Ix -> Set) -> Ix -> Set
  RawAlg C F G y = ⟦ C ⟧ F y -> G y

  Alg : Code -> (F G : Ix -> Set) -> Ix -> Set
  Alg (  I x      )  F G y  =  F x -> G y
  Alg (  K A      )  F G y  =  A -> G y
  Alg (  C₁ ⊕ C₂  )  F G y  =  Alg C₁ F G y × Alg C₂ F G y
  Alg (  C₁ ⊗ C₂  )  F G y  =  Alg C₁ F (Alg C₂ F G) y
  Alg (  C ▷ x    )  F G y  =  Alg C F G x

  RawAlgebra   : (Ix -> Set) -> Set
  RawAlgebra  F  =  (x : Ix) -> RawAlg  FC F F x

  Algebra      : (Ix -> Set) -> Set
  Algebra     F  =  (x : Ix) -> Alg     FC F F x
\end{code}

\end{frame}

\begin{frame}{Generic fold -- relating algebras}

\vspace*{-.5\baselineskip}
\centercolumn{10}%
\begingroup
\colorlet{codecolor}{uuyblue}
\begin{spec}
  RawAlg : Code -> (F G : Ix -> Set) -> Ix -> Set
  RawAlg C F G y = ⟦ C ⟧ F y -> G y

  Alg : Code -> (F G : Ix -> Set) -> Ix -> Set
  Alg (  I x      )  F G y  =  F x -> G y
  Alg (  K A      )  F G y  =  A -> G y
  Alg (  C₁ ⊕ C₂  )  F G y  =  Alg C₁ F G y × Alg C₂ F G y
  Alg (  C₁ ⊗ C₂  )  F G y  =  Alg C₁ F (Alg C₂ F G) y
  Alg (  C ▷ x    )  F G y  =  Alg C F G x
\end{spec}
\endgroup

\vspace*{-\baselineskip}%

\centercolumn{12}%
\begin{code}
  apply :   (C : Code) {F G : Ix -> Set} {y : Ix} ->
            Alg C F G y -> RawAlg C F G y
  apply (  I x      )  a          y             =  a y
  apply (  K _      )  a          y             =  a y
  apply (  C₁ ⊕ C₂  )  (a₁ , a₂)  (inj₁ y₁)     =  apply C₁ a₁ y₁
  apply (  C₁ ⊕ C₂  )  (a₁ , a₂)  (inj₂ y₂)     =  apply C₂ a₂ y₂
  apply (  C₁ ⊗ C₂  )  a          (y₁ , y₂)     =  apply C₂ (apply C₁ a y₁) y₂
  apply (  C ▷ x    )  a          (≡-refl , y)  =  apply C a y
\end{code}

\end{frame}

\begin{frame}{Generic fold -- the function}

This unfortunately doesn't termination-check:
\saverestorecolumns
\begin{code}
  foldRaw   :  {y : Ix} {F : Ix -> Set} -> 
               RawAlgebra  F  ->  ⟨ y ⟩ -> F y

  foldRaw alg x = alg _ (map FC (foldRaw  alg) (from x))
\end{code}
\pause
\begingroup
\colorlet{codecolor}{uuyblue}
\begin{spec}
  apply :   (C : Code) {F G : Ix -> Set} {y : Ix} ->
            Alg C F G y -> RawAlg C F G y
\end{spec}
\endgroup
\restorecolumns
\begin{code}
  fold      :  {y : Ix} {F : Ix -> Set} ->
               Algebra     F  ->  ⟨ y ⟩ -> F y

  fold alg = foldRaw (\ x -> apply FC (alg x))
\end{code}

\end{frame}

\begin{frame}{Generic fold -- application}

Instantiating the |Fold| module to |AST|:
\begin{code}
module FoldExample where

  open AST
  open Fold  AST
  open Fam   AST

\end{code}
%if style == newcode
\begin{code}
  Env : Set
  Env = Var -> ℕ

  empty : Env
  empty _ = 0

  insert : Var -> ℕ -> Env -> Env
  insert x v env y with decToBool (x ≟ y)
  ... | true  = v
  ... | false = env y

  testInsert₁ : (insert "x" 2 empty) "x" ≡ 2
  testInsert₁ = ≡-refl

  testInsert₂ : (insert "x" 4 (insert "x" 2 empty)) "x" ≡ 4
  testInsert₂ = ≡-refl

  testInsert₃ : (insert "y" 4 (insert "x" 2 empty)) "x" ≡ 2
  testInsert₃ = ≡-refl
\end{code}
%endif

\end{frame}

\begin{frame}{Generic fold -- application}

\begin{code}
  Value : Ix -> Set
  Value x with viewAST x
  Value (. _)  | vexpr  =  Env -> ℕ
  Value (. _)  | vdecl  =  Env -> Env
  Value (. _)  | vvar   =  Var

  evalAlgebra : Algebra Value
  evalAlgebra _ =  
                   (  (\ i       env  ->  i                     )   ,   -- |econst|
                      (\ r₁  r₂  env  ->  r₁ env + r₂ env       )   ,   -- |eadd|
                      (\ r₁  r₂  env  ->  r₁ env * r₂ env       )   ,   -- |emul|
                      (\ v       env  ->  env v                 )   ,   -- |evar|
                      (\ f   r   env  ->  r (f env)             ))  ,   -- |elet|
                   (  (\ v   r   env  ->  insert v (r env) env  )   ,   -- |_≔_|
                      (\ f₁  f₂  env  ->  f₂ (f₁ env)           ))  ,   -- |_∙_|
                   (  (\ v            ->  v                     ))
\end{code}

\end{frame}

\begin{frame}{Generic fold -- call}

\begin{code}
  eval : Expr -> Value expr
  eval = fold {expr} {Value} evalAlgebra

  example : Expr
  example = elet  (  "x"  ≔  emul (econst 6) (econst 9) ∙
                     "y"  ≔  eadd (evar "x") (econst 2))
                  (eadd (evar "y") (evar "x"))

  testFold : eval example empty ≡ 110
  testFold = ≡-refl
\end{code}

\end{frame}

\begin{frame}{One-hole contexts}

\centercolumn{10}%
\centercolumn{27}%
\centercolumn{44}%
\begin{code}
module Zipper {n : ℕ} (F : Base.Fam n) where

  open Base n public
  open Fam F

  Ctx : Code -> Ix -> Ix -> Set
  Ctx (  I x      )  y z  =  x ≡ y
  Ctx (  K _      )  y z  =  ⊥
  Ctx (  C₁ ⊕ C₂  )  y z  =  Ctx C₁ y z    ⊎  Ctx C₂ y z
  Ctx (  C₁ ⊗ C₂  )  y z  =  Ctx C₁ y z    ×  ⟦ C₂ ⟧ ⟨_⟩ z
                          ⊎  ⟦ C₁ ⟧ ⟨_⟩ z  ×  Ctx C₂ y z
  Ctx (  C ▷ x    )  y z  =  x ≡ z × Ctx C y z
\end{code}

\end{frame}

\begin{frame}{From contexts to locations}

A path of contexts is the reflexive transitive closure
of the |Ctx| relation:
\onslide<1->
%format (REL x) = "\only<1>{" x ^^ -> ^^ x ^^ -> ^^ Set "}\only<2->{" Rel ^^ x "}"
\begingroup
\colorlet{codecolor}{uuyblue}
\begin{spec}
  Ctx : Code -> (REL Ix)
  
  Rel : Set -> Set1
  Rel A = A -> A -> Set
\end{spec}
\endgroup

\vspace*{-\baselineskip}

\onslide<3->
\begin{code}
  Ctxs : Rel Ix
  Ctxs = Star (Ctx FC)
\end{code}

\onslide<4->%
A location is a pair of a value and a path:
%{
%if True
%format _ = "\Constructor{\char95}"
%format , = "\Constructor{,}"
%endif
\begin{code}
  data Loc : Ix -> Set where
    _,_ : {x y : Ix} -> ⟨ x ⟩ -> Ctxs x y -> Loc y
\end{code}
%}
%if style == newcode
\begin{code}
  infixr 1 _,_
\end{code}
%endif

\end{frame}

\begin{frame}{Filling a hole}

\vspace*{-.5\baselineskip}%
\centercolumn{10}%
\centercolumn{27}%
\centercolumn{44}%
\begingroup
\colorlet{codecolor}{uuyblue}
\begin{spec}
  Ctx : Code -> Ix -> Ix -> Set
  Ctx (  I x      )  y z  =  x ≡ y
  Ctx (  K _      )  y z  =  ⊥
  Ctx (  C₁ ⊕ C₂  )  y z  =  Ctx C₁ y z    ⊎  Ctx C₂ y z
  Ctx (  C₁ ⊗ C₂  )  y z  =  Ctx C₁ y z    ×  ⟦ C₂ ⟧ ⟨_⟩ z
                          ⊎  ⟦ C₁ ⟧ ⟨_⟩ z  ×  Ctx C₂ y z
  Ctx (  C ▷ x    )  y z  =  x ≡ z × Ctx C y z
\end{spec}
\endgroup

\vspace*{-\baselineskip}%

\centercolumn{11}
\begin{code}
  fill :   (C : Code) {x y : Ix} -> 
           Ctx C x y -> ⟨ x ⟩ -> ⟦ C ⟧ ⟨_⟩ y
  fill (  I _      )   ≡-refl                 y   =  y
  fill (  K _      )   ()                     _ 
  fill (  C₁ ⊕ C₂  )   (inj₁ cy₁)             y₁  =  inj₁ (fill C₁ cy₁ y₁)
  fill (  C₁ ⊕ C₂  )   (inj₂ cy₂)             y₂  =  inj₂ (fill C₂ cy₂ y₂)
  fill (  C₁ ⊗ C₂  )   (inj₁ (cy₁ , y₂))      y₁  =  fill C₁ cy₁ y₁ , y₂
  fill (  C₁ ⊗ C₂  )   (inj₂ (y₁ , cy₂))      y₂  =  y₁ , fill C₂ cy₂ y₂
  fill (  C ▷ _    )   (≡-refl , cy)          y   =  ≡-refl , fill C cy y
\end{code}

\end{frame}

\begin{frame}{Navigating up}

\begin{code}
  open RawMonadPlus MaybeMonadPlus

  Nav : Set
  Nav = {x : Ix} -> Loc x -> Maybe (Loc x)

  up : Nav
  up (x , [])      =  ∅
  up (x , c ∷ cs)  =  return (to (fill FC c x) , cs)
\end{code}



\end{frame}

\begingroup
\setbeamertemplate{background}{}%
\begin{frame}{Navigating down}

\renewcommand{\hscodestyle}{\scriptsize}%
\hspace*{-1.8cm}%
\begin{minipage}{\linewidth}
\centercolumn{12}%
\centercolumn{39}%
\begin{code}
  first :   {A : Set} (C : Code) {y : Ix} ->
            ({x : Ix} -> ⟨ x ⟩ -> Ctx C x y -> A) ->
            ⟦ C ⟧ ⟨_⟩ y -> Maybe A
  first (  I _      ) k y             =  return (k y ≡-refl)
  first (  K _      ) k _             =  ∅
  first (  C₁ ⊕ C₂  ) k (inj₁ y₁)     =  first C₁  (\z cy₁  ->  k z (inj₁ cy₁)         )  y₁
  first (  C₁ ⊕ C₂  ) k (inj₂ y₂)     =  first C₂  (\z cy₂  ->  k z (inj₂ cy₂)         )  y₂
  first (  C₁ ⊗ C₂  ) k (y₁ , y₂)     =  first C₁  (\z cy₁  ->  k z (inj₁ (cy₁ , y₂))  )  y₁
                                      ∣  first C₂  (\z cy₂  ->  k z (inj₂ (y₁ , cy₂))  )  y₂
  first (  C ▷ _    ) k (≡-refl , y)  =  first C   (\z cy   ->  k z (≡-refl , cy)      )  y

  down : Nav
  down (x , cs) = first FC (\z c -> z , (c ∷ cs)) (from x) 
\end{code}
\end{minipage}

\end{frame}

\begin{frame}{Navigating right}

\renewcommand{\hscodestyle}{\scriptsize}%
\hspace*{-2.2cm}%
\begin{minipage}{\linewidth}
\centercolumn{11}
\centercolumn{47}
\begin{code}
  next :   {A : Set} (C : Code) {y : Ix} ->
           ({x : Ix} -> ⟨ x ⟩ -> Ctx C x y -> A) ->
           {x : Ix} -> Ctx C x y -> ⟨ x ⟩ -> Maybe A
  next (  I _      ) k ≡-refl             y   =  ∅
  next (  K _      ) k ()                 _
  next (  C₁ ⊕ C₂  ) k (inj₁ cy₁)         y₁  =  next   C₁  (\z cy₁′  -> k z (inj₁ cy₁′)                         ) cy₁  y₁
  next (  C₁ ⊕ C₂  ) k (inj₂ cy₂)         y₂  =  next   C₂  (\z cy₂′  -> k z (inj₂ cy₂′)                         ) cy₂  y₂
  next (  C₁ ⊗ C₂  ) k (inj₁ (cy₁ , y₂))  y₁  =  next   C₁  (\z cy₁′  -> k z (inj₁ (cy₁′            ,  y₂    ))  ) cy₁  y₁
                                              ∣  first  C₂  (\z cy₁′  -> k z (inj₂ (fill C₁ cy₁ y₁  ,  cy₁′  ))  )      y₂
  next (  C₁ ⊗ C₂  ) k (inj₂ (y₁ , cy₂))  y₂  =  next   C₂  (\z cy₂′  -> k z (inj₂ (y₁              ,  cy₂′  ))  ) cy₂  y₂
  next (  C ▷ _    ) k (≡-refl , cy)      y   =  next   C   (\z cy′   -> k z (≡-refl , cy′)                      ) cy   y

  right : Nav
  right (x ,  []        )  =  ∅
  right (x ,  (c ∷ cs)  )  =  next FC (\z c′ -> z , (c′ ∷ cs)) c x 
\end{code}
\end{minipage}

\end{frame}
\endgroup

\begin{frame}{Completing the navigation functions}

The functions |prev| and |left| are similar to |next| and |right|.
\begin{code}
  enter : {x : Ix} -> ⟨ x ⟩ -> Loc x
  enter x = x , []

  leave : {x : Ix} -> Loc x -> ⟨ x ⟩
  leave (x , [])        =  x
  leave (x , (c ∷ cs))  =  leave (to (fill FC c x) , cs)

  update : ((x : Ix) -> ⟨ x ⟩ -> ⟨ x ⟩) -> Nav
  update f (x , cs) = return (f _ x , cs)

  on :  {A : Set} -> ((x : Ix) -> ⟨ x ⟩ -> A) ->
        {x : Ix} -> Loc x -> A
  on f (x , cs) = f _ x
\end{code}

\end{frame}

\begin{frame}{Using the Zipper -- preparations}

\begin{code}
module ZipperExample where

  open AST
  open Zipper AST
  open Fam AST
  open FoldExample
  open RawMonadPlus MaybeMonadPlus
\end{code}

\end{frame}

\begin{frame}{Using the Zipper -- test}

\begin{code}
  source : Expr
  source = elet  ("x" ≔ emul (econst 6) (econst 9)) 
                 (eadd (evar "x") (evar "y"))

  callZipper : Maybe Expr
  callZipper =
    return (enter {expr} source) >>=
    down >>= down >>= right >>= update simp >>=
    return ∘ leave
      where  simp : (n : Ix) -> ⟨ n ⟩ -> ⟨ n ⟩
             simp n x with viewAST n
             simp (. _) e  |  vexpr  =  econst (eval e empty)
             simp (. _) d  |  vdecl  =  d
             simp (. _) v  |  vvar   =  v

  target = elet ("x" ≔ econst 54) (eadd (evar "x") (evar "y"))
  testZipper : callZipper ≡ just target
  testZipper = ≡-refl
\end{code}

\end{frame}

\end{document}