0 | ||| A segment is a compositional fragment of a telescope.
  1 | ||| A key difference is that segments are right-nested, whereas
  2 | ||| telescopes are left nested.
  3 | ||| So telescopes are convenient for well-bracketing dependencies,
  4 | ||| but segments are convenient for processing telescopes from left
  5 | ||| to right.
  6 | |||
  7 | ||| As with telescopes, indexing segments by their length (hopefully)
  8 | ||| helps the type-checker infer stuff.
  9 | module Data.Telescope.Segment
 10 |
 11 | import Data.Telescope.Telescope
 12 |
 13 | import Syntax.PreorderReasoning
 14 | import Data.Fin
 15 | import Data.Nat
 16 | import Data.DPair
 17 |
 18 | %default total
 19 |
 20 | ||| A segment is a compositional fragment of a telescope, indexed by
 21 | ||| the segment's length.
 22 | public export
 23 | data Segment : (n : Nat) -> Left.Telescope k -> Type where
 24 |   Nil  : Segment 0 gamma
 25 |   (::) : (ty : TypeIn gamma) -> (delta : Segment n (gamma -. ty)) -> Segment (S n) gamma
 26 |
 27 | ||| A segment of size `n` indexed by `gamma` can be seen as the tabulation of a
 28 | ||| function that turns environments for `gamma` into telescopes of size `n`.
 29 | public export
 30 | tabulate : (n : Nat) -> (Left.Environment gamma -> Left.Telescope n) -> Segment n gamma
 31 | tabulate Z tel = []
 32 | tabulate (S n) tel = (sigma :: tabulate n (uncurry delta)) where
 33 |
 34 |   sigma : TypeIn gamma
 35 |   sigma env = fst (uncons (tel env))
 36 |
 37 |   delta : (env : Environment gamma) -> sigma env -> Left.Telescope n
 38 |   delta env v with (uncons (tel env))
 39 |     delta env v | (sig ** delt ** _) = delt v
 40 |
 41 | ||| Any telescope is a segment in the empty telescope. It amounts to looking
 42 | ||| at it left-to-right instead of right-to-left.
 43 | public export
 44 | fromTelescope : {k : Nat} -> Left.Telescope k -> Segment k []
 45 | fromTelescope gamma = tabulate _ (const gamma)
 46 |
 47 | ||| Conversely, a segment of size `n` in telescope `gamma` can be seen as a function
 48 | ||| from environments for `gamma` to telescopes of size `n`.
 49 | public export
 50 | untabulate : {n : Nat} -> Segment n gamma -> (Left.Environment gamma -> Left.Telescope n)
 51 | untabulate []            _   = []
 52 | untabulate (ty :: delta) env = cons (ty env) (untabulate delta . (\ v => (env ** v)))
 53 |
 54 | ||| Any segment in the empty telescope correspond to a telescope.
 55 | public export
 56 | toTelescope : {k : Nat} -> Segment k [] -> Left.Telescope k
 57 | toTelescope seg = untabulate seg ()
 58 |
 59 | %name Segment delta,delta',delta1,delta2
 60 |
 61 | export infixl 3 |++, :++
 62 |
 63 | ||| This lemma comes up all the time when mixing induction on Nat with
 64 | ||| indexing modulo addition.  An alternative is to use something like
 65 | ||| frex.
 66 | succLemma : (lft, rgt : Nat) -> lft + (S rgt) = S (lft + rgt)
 67 | succLemma x y = Calc $
 68 |   |~ x + (1 + y)
 69 |   ~~ (x + 1)+ y  ...(plusAssociative x 1 y)
 70 |   ~~ (1 + x)+ y  ...(cong (+y) $ plusCommutative x 1)
 71 |   ~~ 1 + (x + y) ...(sym $ plusAssociative 1 x y)
 72 |
 73 | -- Should go somehwere in stdlib
 74 | public export
 75 | keep : (0 prf : a ~=~ b) -> a ~=~ b
 76 | keep Refl = Refl
 77 |
 78 | -- Keeping the `Nat` argument relevant, should (hopefully) only
 79 | -- case-split on it and not the environment unnecessarily, allowing us
 80 | -- to calculate, so long as we know the 'shape' of the Segment.
 81 | --
 82 | -- This should work in theory, I don't think it actually works for
 83 | -- Idris at the moment.  Might work in Agda?
 84 |
 85 | ||| Segments act on telescope from the right.
 86 | public export
 87 | (|++) : (gamma : Left.Telescope k) -> {n : Nat} -> (delta : Segment n gamma) -> Left.Telescope (n + k)
 88 | (|++)  gamma {n = 0} delta  = gamma
 89 | (|++)  gamma {n=S n} (ty :: delta) = rewrite sym $ succLemma n k in
 90 |                                        gamma -. ty |++ delta
 91 |
 92 | ||| Segments form a kind of an indexed monoid w.r.t. the action `(|++)`
 93 | public export
 94 | (++) : {gamma : Left.Telescope k}
 95 |     -> {n : Nat}
 96 |     -> (lft : Segment n  gamma         )
 97 |     -> (rgt : Segment m (gamma |++ lft))
 98 |     -> Segment (n + m) gamma
 99 | (++) {n = 0  } delta       rgt = rgt
100 | (++) {n = S n} (ty :: lft) rgt = ty :: lft ++ rewrite succLemma n k in
101 |                                               rgt
102 | -- This monoid does act on telescopes:
103 | export
104 | actSegmentAssociative : (gamma : Left.Telescope k)
105 |                      -> (lft : Segment n gamma)
106 |                      -> (rgt : Segment m (gamma |++ lft))
107 |                      -> (gamma |++ (lft ++ rgt)) ~=~ ((gamma |++ lft) |++ rgt)
108 | actSegmentAssociative gamma {n = 0}   []          rgt = Refl
109 | actSegmentAssociative gamma {n = S n} (ty :: lft) rgt =
110 |   let rgt' : Segment {k = n + (S k)} m (gamma -. ty |++ lft)
111 |       rgt' = rewrite succLemma n k in
112 |              rgt
113 |       rgt_eq_rgt' : rgt ~=~ rgt'
114 |       rgt_eq_rgt' = rewrite succLemma n k in
115 |                     Refl
116 |   in
117 |   rewrite sym $ succLemma (n + m) k in
118 |   rewrite sym $ succLemma n       k in keep $ Calc $
119 |   |~ ((gamma -. ty) |++ (lft ++ rgt'))
120 |   ~~ ((gamma -. ty |++  lft) |++ rgt')
121 |           ...(actSegmentAssociative (gamma -. ty) lft rgt')
122 |
123 | public export
124 | weaken : {0 gamma : Left.Telescope k}
125 |       -> {delta : Segment n gamma} -> (sy : TypeIn gamma)
126 |       -> TypeIn (gamma |++ delta)
127 | weaken           {delta = []         } sy = sy
128 | weaken {n = S n} {delta = ty :: delta} sy = rewrite sym $ succLemma n k in
129 |                                             weaken (weakenTypeIn sy)
130 |
131 | public export
132 | projection : {0 gamma : Left.Telescope k}
133 |           -> {n : Nat}
134 |           -> {0 delta : Segment n gamma}
135 |           -> Environment (gamma |++ delta)
136 |           -> Environment gamma
137 | projection {n = 0  } {delta = []         } env = env
138 | projection {n = S n} {delta = ty :: delta} env
139 |   = let (env' ** _) = projection {n} {delta}
140 |                     $ rewrite succLemma n k in env
141 |     in env'
142 |
143 | export infixl 4 .=
144 |
145 | public export
146 | data Environment : (env : Left.Environment gamma)
147 |                 -> (delta : Segment n gamma) -> Type where
148 |   Empty : Environment env []
149 |   (.=) : {0 gamma : Left.Telescope k} -> {0 ty : TypeIn gamma}
150 |       -> {0 env   : Left.Environment gamma}
151 |       -> {0 delta : Segment n (gamma -. ty)}
152 |
153 |       -> (x : ty env) -> (xs : Segment.Environment (env ** x) delta)
154 |       -> Environment env (ty :: delta)
155 |
156 | public export
157 | (:++) : {0 gamma : Left.Telescope k} -> {0 delta : Segment n gamma}
158 |      -> (env : Left.Environment gamma)
159 |      -> (ext : Segment.Environment env delta)
160 |      ->        Left.Environment (gamma |++ delta)
161 | (:++) env Empty = env
162 | (:++) {n = S n} env (x .= xs) = rewrite sym $ succLemma n k in
163 |                                 (env ** x) :++ xs
164 |
165 | -- This is too nasty for now, leave to later
166 | {-
167 | public export
168 | break : {0 k : Nat} -> (gamma : Telescope k') -> (pos : Position gamma)
169 |      -> {auto 0 ford : k' = cast pos + k } -> Telescope k
170 | break gamma          FZ      {ford = Refl} = gamma
171 | break []            (FS pos) {ford = _   } impossible
172 | break {k' = S k'} (gamma -. ty) (FS pos) {ford} = break gamma pos
173 |   {ford = Calc $
174 |    |~ k'
175 |    ~~ cast pos + k ...(succInjective _ _ ford)}
176 |
177 | -- Should go into Data.Fin
178 | export
179 | lastIsLast : {n : Nat} -> cast (last {n}) = n
180 | lastIsLast {n = 0  } = Refl
181 | lastIsLast {n = S n} = rewrite lastIsLast {n} in
182 |                        Refl
183 |
184 | public export
185 | finComplement : {n : Nat} -> (i : Fin n) -> Fin n
186 | finComplement FZ = last
187 | finComplement (FS i) = weaken (finComplement i)
188 |
189 | export
190 | castNaturality : (i : Fin n) -> finToNat (weaken i) ~=~ finToNat i
191 | castNaturality  FZ    = Refl
192 | castNaturality (FS i) = rewrite castNaturality i in
193 |                         Refl
194 |
195 | export
196 | finComplementSpec : (i : Fin (S n)) -> cast i + cast (finComplement i) = n
197 | finComplementSpec FZ = keep lastIsLast
198 | finComplementSpec {n = .(S n)} (FS i@ FZ   ) = rewrite castNaturality (finComplement i) in
199 |                                                rewrite finComplementSpec i in
200 |                                                Refl
201 | finComplementSpec {n = .(S n)} (FS i@(FS _)) = rewrite castNaturality (finComplement i) in
202 |                                                rewrite finComplementSpec i in
203 |                                                Refl
204 |
205 | complementLastZero : (n : Nat) -> finComplement (last {n}) = FZ
206 | complementLastZero n = finToNatInjective _ _ $ plusLeftCancel n _ _ $ Calc $
207 |    let n' : Nat
208 |        n' = cast $ finComplement $ last {n} in
209 |    |~ n + n'
210 |    ~~ (finToNat $ last {n})  + n'
211 |                     ...(cong (+n') $ sym $ lastIsLast {n})
212 |    ~~ n             ...(finComplementSpec $ last {n})
213 |    ~~ n         + 0 ...(sym $ plusZeroRightNeutral n)
214 |
215 | public export
216 | breakOnto : {0 k,k' : Nat} -> (gamma : Telescope k) -> (pos : Position gamma)
217 |          -> (delta : Segment n gamma)
218 |          -> {auto 0 ford1 : k' === (finToNat $ finComplement pos) }
219 |          -> {default
220 |                -- disgusting, sorry
221 |                (replace {p = \u => k = finToNat pos + u}
222 |                         (sym ford1)
223 |                         (sym $ finComplementSpec pos))
224 |              0 ford2 : (k === ((finToNat pos) + k')) }
225 |          -> Segment (cast pos + n)
226 |                     (break {k = k'}
227 |                            gamma pos
228 |                            {ford = ford2})
229 | breakOnto gamma          FZ      delta {ford1 = Refl} {ford2} =
230 |                          rewrite sym ford2 in
231 |                          delta
232 | breakOnto (gamma -. ty) (FS pos) delta {ford1 = Refl} {ford2} =
233 |                          rewrite sym $ succLemma (cast pos) n in
234 |                          rewrite castNaturality (finComplement pos) in
235 |                          breakOnto gamma pos (ty :: delta)
236 |
237 | uip : (prf1, prf2 : x ~=~ y) -> prf1 ~=~ prf2
238 | uip Refl Refl = Refl
239 |
240 | export
241 | breakStartEmpty : (gamma : Telescope k')
242 |                -> {auto 0 ford1 : k = 0}
243 |                -> {auto 0 ford2 : k' = finToNat (start gamma) + k}
244 |                -> break {k} {k'} gamma (start gamma) {ford = ford2}
245 |                 ~=~ Telescope.Nil
246 | breakStartEmpty [] {ford1 = Refl} {ford2 = Refl}            = Refl
247 | breakStartEmpty {k} {k' = S k'} {ford1} {ford2} (gamma -. ty) =
248 |                 -- Yuck!
249 |                 let 0 u : (k' = finToNat (start gamma) + k)
250 |                     u = succInjective _ _ ford2
251 |                     v : break {k} {k'} gamma (start gamma) {ford = u}
252 |                         ~=~ Telescope.Nil
253 |                     v = breakStartEmpty {k} {k'} gamma {ford2 = u}
254 |                 in replace {p = \z =>
255 |                              Equal {a = Telescope k} {b = Telescope 0}
256 |                                    (break {k'} {k} gamma (start gamma)
257 |                                           {ford = z})
258 |                                           []
259 |                         }
260 |                         (uip u _)
261 |                         (keep v)
262 |
263 |
264 |
265 | public export
266 | projection : {0 gamma : Telescope k} -> (pos : Position gamma) -> (env : Environment gamma)
267 |           -> Environment (break {k = cast (finComplement pos)} gamma pos
268 |                                 {ford = sym $ finComplementSpec pos})
269 | projection FZ env = rewrite finComplementSpec $ FZ {k} in
270 |                     env
271 | projection {gamma = []} (FS pos) Empty impossible
272 | projection {k = S k} {gamma = gamma -. ty} (FS pos) (env ** x) =
273 |   rewrite castNaturality (finComplement pos) in
274 |   projection {k} pos env
275 | -}
276 |