
   0 | ||| The telescope data structures.
   1 | |||
   2 | ||| Indexing telescopes by their length (hopefully) helps inform the
   3 | ||| type-checker during inference.
   4 | module Data.Telescope.Telescope
   5 | 
   6 | import Data.DPair
   7 | import Data.Nat
   8 | import Data.Fin
   9 | 
  10 | %default total
  11 | 
  12 | public export
  13 | plusAcc : Nat -> Nat -> Nat
  14 | plusAcc Z n = n
  15 | plusAcc (S m) n = plusAcc m (S n)
  16 | 
  17 | export
  18 | plusAccIsPlus : (m, n : Nat) -> (m + n) === plusAcc m n
  19 | plusAccIsPlus Z n = Refl
  20 | plusAccIsPlus (S m) n =
  21 |   rewrite plusSuccRightSucc m n in
  22 |   plusAccIsPlus m (S n)
  23 | 
  24 | public export
  25 | plusAccZeroRightNeutral : (m : Nat) -> plusAcc m 0 === m
  26 | plusAccZeroRightNeutral m =
  27 |   rewrite sym (plusAccIsPlus m 0) in
  28 |   rewrite plusZeroRightNeutral m in
  29 |   Refl
  30 | 
  31 | 
  32 | export infixl 4 -.
  33 | export typebind infixr 0 .-
  34 | 
  35 | namespace Left
  36 | 
  37 |   mutual
  38 |     ||| A left-nested sequence of dependent types
  39 |     public export
  40 |     data Telescope : (k : Nat) -> Type where
  41 |       Nil  : Telescope 0
  42 |       (-.) : (gamma : Left.Telescope k) -> (ty : TypeIn gamma) -> Telescope (S k)
  43 | 
  44 |     ||| A type with dependencies in the given context
  45 |     public export
  46 |     TypeIn : Left.Telescope k -> Type
  47 |     TypeIn gamma = (env : Environment gamma) -> Type
  48 | 
  49 |     ||| A tuple of values of each type in the telescope
  50 |     public export
  51 |     Environment : Left.Telescope k -> Type
  52 |     Environment [] = ()
  53 |     Environment (gamma -. ty) = (env : Environment gamma ** ty env)
  54 | 
  55 |   export
  56 |   weakenTypeIn : TypeIn gamma -> TypeIn (gamma -. sigma)
  57 |   weakenTypeIn ty env = ty (fst env)
  58 | 
  59 |   public export
  60 |   uncons : (gamma : Telescope (S k)) ->
  61 |            (ty : Type
  62 |             ** delta : (ty -> Telescope k)
  63 |             ** (v : ty) -> Environment (delta v) -> Environment gamma)
  64 |   uncons ([] -. ty) = (ty () ** const [] ** \ v, _ => (() ** v))
  65 |   uncons (gamma@(_ -. _) -. ty) =
  66 |     let (sigma ** delta ** left) = uncons gamma in
  67 |     (sigma ** (\ v => delta v -. (\ env => ty (left v env)))
  68 |            ** (\ v, (env ** w) => (left v env ** w)))
  69 | 
  70 |   export autobind infixr 0 \++
  71 | 
  72 |   public export
  73 |   (\++) : {n : Nat} -> (gamma : Left.Telescope m) -> (Environment gamma -> Left.Telescope n) ->
  74 |          Telescope (plusAcc n m)
  75 |   (\++) {n = Z} gamma delta = gamma
  76 |   (\++) {n = S n} gamma delta = (env <- gamma -. sigma) \++ uncurry theta env where
  77 | 
  78 |     sigma : Environment gamma -> Type
  79 |     sigma env = fst (uncons (delta env))
  80 | 
  81 |     theta : (env : Environment gamma) -> sigma env -> Telescope n
  82 |     theta env val with (uncons (delta env))
  83 |       theta env val | (sig ** omega ** _) = omega val
  84 | 
  85 |   public export
  86 |   cons : {k : Nat} -> (ty : Type) -> (ty -> Left.Telescope k) -> Left.Telescope (S k)
  87 |   cons sigma gamma =
  88 |     rewrite plusCommutative 1 k in
  89 |     rewrite plusAccIsPlus k 1 in
  90 |     (env <- [] -. const sigma) \++ gamma (snd env)
  91 | 
  92 |   ||| A position between the variables of a telescope, counting from the _end_:
  93 |   ||| Telescope:   Nil -. ty1 -. ... -. tyn
  94 |   ||| Positions: ^k    ^k-1   ^k-2   ^1     ^0
  95 |   public export
  96 |   Position : {k : Nat} -> Telescope k -> Type
  97 |   Position {k} _ = Fin (S k)
  98 | 
  99 |   ||| The position at the beginning of the telescope
 100 |   public export
 101 |   start : {k : Nat} -> (gamma : Telescope k) -> Position gamma
 102 |   start {k} gamma = last
 103 | 
 104 | namespace Right
 105 | 
 106 |   mutual
 107 |     ||| A right-nested sequence of dependent types
 108 |     public export
 109 |     data Telescope : (k : Nat) -> Type where
 110 |       Nil  : Telescope 0
 111 |       (.-) : (ty : Type) -> (gamma : ty -> Right.Telescope k) -> Telescope (S k)
 112 | 
 113 |     ||| A tuple of values of each type in the telescope
 114 |     public export
 115 |     Environment : Right.Telescope k -> Type
 116 |     Environment [] = ()
 117 |     Environment (ty .- gamma) = (v : ty ** Environment (gamma v))
 118 | 
 119 |   export
 120 |   empty : (0 gamma : Right.Telescope Z) -> Environment gamma
 121 |   empty {gamma = []} = ()
 122 | 
 123 |   export
 124 |   snoc : (gamma : Right.Telescope k) -> (Environment gamma -> Type) -> Right.Telescope (S k)
 125 |   snoc [] tau   = (v : tau ()) .- const [] v
 126 |   snoc (sigma .- gamma) tau = (v : sigma) .- snoc (gamma v) (\ env => tau (v ** env))
 127 | 
 128 |   export
 129 |   unsnoc : {k : Nat} -> (gamma : Right.Telescope (S k)) ->
 130 |            (delta : Right.Telescope k
 131 |             ** sigma : (Environment delta -> Type)
 132 |             ** (env : Environment delta) -> sigma env -> Environment gamma)
 133 |   unsnoc {k = Z} (sigma .- gamma) = ([] ** const sigma ** \ (), v => (v ** empty (gamma v)))
 134 |   unsnoc {k = S k} (sigma .- gamma)
 135 |     = ((x : sigma) .- delta x ** uncurry tau ** \ (v ** env) => transp v env) where
 136 | 
 137 |     delta : sigma -> Right.Telescope k
 138 |     delta v = fst (unsnoc (gamma v))
 139 | 
 140 |     tau : (v : sigma) -> Environment (delta v) -> Type
 141 |     tau v = fst (snd (unsnoc (gamma v)))
 142 | 
 143 |     transp : (v : sigma) -> (env : Environment (delta v)) -> tau v env -> Environment ((x : sigma) .- gamma x)
 144 |     transp v env w = (v ** (snd (snd (unsnoc (gamma v))) env w))
 145 | 
 146 |   export autobind infixr 0 ++/
 147 | 
 148 |   export
 149 |   (++/) : (gamma : Right.Telescope m) -> (Environment gamma -> Right.Telescope n) -> Right.Telescope (m + n)
 150 |   [] ++/ delta = delta ()
 151 |   (sigma .- gamma) ++/ delta = (v : sigma) .- (env <- gamma v) ++/ delta (v ** env)
 152 | 
 153 |   export
 154 |   split : (gamma : Right.Telescope m) -> (delta : Environment gamma -> Right.Telescope n) ->
 155 |           Environment ((env <- gamma) ++/ delta env) ->
 156 |           (env : Environment gamma ** Environment (delta env))
 157 |   split [] delta env = (() ** env)
 158 |   split (sigma .- gamma) delta (v ** env) =
 159 |     let (env1 ** env2) = split (gamma v) (\env => delta (v ** env)) env in
 160 |     ((v ** env1) ** env2)
 161 | 
 162 | namespace Tree
 163 | 
 164 |   export infixl 4 ><
 165 | 
 166 |   mutual
 167 |     ||| A tree of dependent types
 168 |     public export
 169 |     data Telescope : (k : Nat) -> Type where
 170 |       Nil  : Telescope 0
 171 |       Elt  : Type -> Telescope 1
 172 |       (><) : (gamma : Tree.Telescope m) ->
 173 |              (delta : Tree.Environment gamma -> Tree.Telescope n) ->
 174 |               Telescope (m + n)
 175 | 
 176 |     ||| A tuple of values of each type in the telescope
 177 |     public export
 178 |     Environment : Tree.Telescope k -> Type
 179 |     Environment [] = ()
 180 |     Environment (Elt t) = t
 181 |     Environment (gamma >< delta) = (env : Environment gamma ** Environment (delta env))
 182 | 
 183 |   export
 184 |   concat : (gamma : Tree.Telescope k) -> (delta : Right.Telescope k ** Environment delta -> Environment gamma)
 185 |   concat Nil = ([] ** id)
 186 |   concat (Elt t) = ((x : t) .- const [] x ** fst)
 187 |   concat (gamma >< delta) =
 188 |     let (thetaL ** transpL) = concat gamma in
 189 |     (((envL <- thetaL) ++/ fst (concat (delta (transpL envL))))
 190 |     ** \ env =>
 191 |          let (env1 ** env2) = split thetaL (\ envL => fst (concat (delta (transpL envL)))) env in
 192 |          (transpL env1 ** snd (concat (delta (transpL env1))) env2)
 193 |     )
 194 | 
 195 | export autobind infixr 0 <++>
 196 | 
 197 | public export
 198 | (<++>) : (gamma : Left.Telescope m) -> (Environment gamma -> Right.Telescope n) -> Right.Telescope (plusAcc m n)
 199 | [] <++> delta = delta ()
 200 | (gamma -. sigma ) <++> delta = (env <- gamma) <++> (v : sigma env) .- delta (env ** v)
 201 | 
 202 | export autobind infixr 0 >++<
 203 | 
 204 | (>++<) : {m, n : Nat} -> (gamma : Right.Telescope m) -> (Environment gamma -> Left.Telescope n) ->
 205 |          Left.Telescope (plusAcc m n)
 206 | [] >++< delta = delta ()
 207 | gamma@(_ .- _) >++< delta =
 208 |   let (gamma ** sigma ** transp) = unsnoc gamma in
 209 |   (env <- gamma) >++< cons (sigma env) (\ v => delta (transp env v))
 210 | 
 211 | export
 212 | leftToRight : Left.Telescope m -> Right.Telescope m
 213 | leftToRight gamma = rewrite sym (plusAccZeroRightNeutral m) in (env <- gamma) <++> const [] env
 214 | 
 215 | export
 216 | rightToLeft : {m : Nat} -> Right.Telescope m -> Left.Telescope m
 217 | rightToLeft gamma = rewrite sym (plusAccZeroRightNeutral m) in (env <- gamma) >++< const [] env
 218 |