0 | module Core.TT.Var

  2 | import Data.Fin

  3 | import Data.List

  4 | import Data.So

  5 | import Data.SnocList

  7 | import Core.Name.Scoped

  9 | import Libraries.Data.SnocList.HasLength

 10 | import Libraries.Data.SnocList.SizeOf

 12 | import Data.List.HasLength

 13 | import Data.DPair

 15 | import Libraries.Data.List.SizeOf

 17 | import Libraries.Data.Erased

 19 | %default total

 30 | public export

 31 | data IsVar : a -> Nat -> List a -> Type where

 32 |      First : IsVar n Z (n :: ns)

 33 |      Later : IsVar n i ns -> IsVar n (S i) (m :: ns)

 35 | %name IsVar idx

 42 | 0 Last : HasLength (S n) vs -> Exists (\ nm => IsVar nm n vs)

 43 | Last {vs = .(_)} (S Z) = Evidence _ First

 44 | Last {vs = .(_)} (S (S p)) = bimap id Later (Last (S p))

 47 | finIdx : {idx : _} -> (0 prf : IsVar x idx vars) ->

 48 |          Fin (length vars)

 49 | finIdx First = FZ

 50 | finIdx (Later l) = FS (finIdx l)

 55 | nameAt : {vars : List a} -> {idx : Nat} -> (0 p : IsVar n idx vars) -> a

 56 | nameAt {vars = n :: _} First = n

 57 | nameAt (Later p) = nameAt p

 61 | dropLater : IsVar nm (S idx) (n :: ns) -> IsVar nm idx ns

 62 | dropLater (Later p) = p

 65 | 0 mkIsVar : HasLength m inner -> IsVar nm m (inner ++ nm :: outer)

 66 | mkIsVar Z = First

 67 | mkIsVar (S x) = Later (mkIsVar x)

 70 | 0 mkIsVarChiply : HasLength m inner -> IsVar nm m (inner <>> nm :: outer)

 71 | mkIsVarChiply hl

 72 |   = rewrite chipsAsListAppend inner (nm :: outer) in

 73 |     rewrite sym $ plusZeroRightNeutral m in

 74 |     mkIsVar (hlChips hl Z)

 77 | public export

 78 | dropIsVar :

 79 |   (ns : List a) ->

 80 |   {idx : Nat} -> (0 p : IsVar name idx ns) ->

 81 |   List a

 82 | dropIsVar (_ :: xs) First = xs

 83 | dropIsVar (n :: xs) (Later p) = n :: dropIsVar xs p

 89 | 0 embedIsVar : IsVar x idx xs -> IsVar x idx (xs ++ outer)

 90 | embedIsVar First = First

 91 | embedIsVar (Later p) = Later (embedIsVar p)

 96 | 0 weakenIsVar : (s : SizeOf ns) -> IsVar x idx xs -> IsVar x (size s + idx) (ns ++ xs)

 97 | weakenIsVar (MkSizeOf Z Z) p =  p

 98 | weakenIsVar (MkSizeOf (S k) (S l)) p =  Later (weakenIsVar (MkSizeOf k l) p)

100 | 0 locateIsVarLT :

101 |   (s : SizeOf local) ->

102 |   So (idx < size s) ->

103 |   IsVar x idx (local ++ outer) ->

104 |   IsVar x idx local

105 | locateIsVarLT (MkSizeOf Z Z) so v = case v of

106 |   First impossible

107 |   Later v impossible

108 | locateIsVarLT (MkSizeOf (S k) (S l)) so v = case v of

109 |   First => First

110 |   Later v => Later (locateIsVarLT (MkSizeOf k l) so v)

112 | 0 locateIsVarGE :

113 |   (s : SizeOf local) ->

114 |   So (idx >= size s) ->

115 |   IsVar x idx (local ++ outer) ->

116 |   IsVar x (idx `minus` size s) outer

117 | locateIsVarGE (MkSizeOf Z Z) so v = rewrite minusZeroRight idx in v

118 | locateIsVarGE (MkSizeOf (S k) (S l)) so v = case v of

119 |   Later v => locateIsVarGE (MkSizeOf k l) so v

122 | locateIsVar : {idx : Nat} -> (s : SizeOf local) ->

123 |   (0 p : IsVar x idx (local ++ outer)) ->

124 |   Either (Erased (IsVar x idx local))

125 |          (Erased (IsVar x (idx `minus` size s) outer))

126 | locateIsVar s p = case choose (idx < size s) of

127 |   Left so => Left (MkErased (locateIsVarLT s so p))

128 |   Right so => Right (MkErased (locateIsVarGE s so p))

136 | public export

137 | record Var {0 a : Type} (vars : List a) where

138 |   constructor MkVar

139 |   {varIdx : Nat}

140 |   {0 varNm : a}

141 |   0 varPrf : IsVar varNm varIdx vars

143 | namespace Var

145 |   export

146 |   first : Var (n :: ns)

147 |   first = MkVar First

149 |   export

150 |   later : Var ns -> Var (n :: ns)

151 |   later (MkVar p) = MkVar (Later p)

153 |   export

154 |   isLater : Var (n :: vs) -> Maybe (Var vs)

155 |   isLater (MkVar First) = Nothing

156 |   isLater (MkVar (Later p)) = Just (MkVar p)

158 |   export

159 |   last : SizeOf vs -> Maybe (Var vs)

160 |   last (MkSizeOf Z p) = Nothing

161 |   last (MkSizeOf (S n) p) = Just (MkVar (snd $ Last p))

164 | mkVar : SizeOf inner -> Var (inner ++ nm :: outer)

165 | mkVar (MkSizeOf s p) = MkVar (mkIsVar p)

168 | mkVarChiply : SizeOf inner -> Var (inner <>> nm :: outer)

169 | mkVarChiply (MkSizeOf s p) = MkVar (mkIsVarChiply p)

173 | allVars : (vars : Scope) -> List (Var vars)

174 | allVars = go [<] where

176 |   go : SizeOf local -> (vs : Scope) -> List (Var (local <>> vs))

177 |   go s [] = []

178 |   go s (v :: vs) = mkVarChiply s :: go (s :< v) vs

181 | Eq (Var xs) where

182 |   v == w = varIdx v == varIdx w

185 | Show (Var ns) where

186 |   show v = show (varIdx v)

191 | public export

192 | record NVar {0 a : Type} (nm : a) (vars : List a) where

193 |   constructor MkNVar

194 |   {nvarIdx : Nat}

195 |   0 nvarPrf : IsVar nm nvarIdx vars

197 | namespace NVar

199 |   export

200 |   first : NVar n (n :: ns)

201 |   first = MkNVar First

203 |   export

204 |   later : NVar nm ns -> NVar nm (n :: ns)

205 |   later (MkNVar p) = MkNVar (Later p)

207 |   export

208 |   isLater : NVar nm (n :: ns) -> Maybe (NVar nm ns)

209 |   isLater (MkNVar First) = Nothing

210 |   isLater (MkNVar (Later p)) = Just (MkNVar p)

213 | forgetName : NVar nm vars -> Var vars

214 | forgetName (MkNVar p) = MkVar p

217 | recoverName : (v : Var vars) -> NVar (varNm v) vars

218 | recoverName (MkVar p) = MkNVar p

221 | mkNVar : SizeOf inner -> NVar nm (inner ++ nm :: outer)

222 | mkNVar (MkSizeOf s p) = MkNVar (mkIsVar p)

225 | mkNVarChiply : SizeOf inner -> NVar nm (inner <>> nm :: outer)

226 | mkNVarChiply (MkSizeOf s p) = MkNVar (mkIsVarChiply p)

229 | locateNVar : SizeOf local -> NVar nm (local ++ outer) ->

230 |              Either (NVar nm local) (NVar nm outer)

231 | locateNVar s (MkNVar p) = case locateIsVar s p of

232 |   Left p => Left (MkNVar (runErased p))

233 |   Right p => Right (MkNVar (runErased p))

235 | public export

236 | dropNVar : {ns : List a} -> NVar nm ns -> List a

237 | dropNVar (MkNVar p) = dropIsVar ns p

243 | isDeBruijn : Nat -> (vars : List Name) -> Maybe (Var vars)

244 | isDeBruijn Z (_ :: _) = pure first

245 | isDeBruijn (S k) (_ :: vs) = later <$> isDeBruijn k vs

246 | isDeBruijn _ _ = Nothing

249 | isNVar : (n : Name) -> (ns : List Name) -> Maybe (NVar n ns)

250 | isNVar n [] = Nothing

251 | isNVar n (m :: ms)

252 |     = case nameEq n m of

253 |            Nothing   => map later (isNVar n ms)

254 |            Just Refl => pure (MkNVar First)

257 | isVar : (n : Name) -> (ns : List Name) -> Maybe (Var ns)

258 | isVar n ns = forgetName <$> isNVar n ns

261 | locateVar : SizeOf local -> Var (local ++ outer) ->

262 |             Either (Var local) (Var outer)

263 | locateVar s v  = bimap forgetName forgetName

264 |   $ locateNVar s (recoverName v)

270 | weakenNVar : SizeOf ns -> NVar name outer -> NVar name (ns ++ outer)

271 | weakenNVar s (MkNVar {nvarIdx} p)

272 |   = MkNVar {nvarIdx = plus (size s) nvarIdx} (weakenIsVar s p)

275 | embedNVar : NVar name ns -> NVar name (ns ++ outer)

276 | embedNVar (MkNVar p) = MkNVar (embedIsVar p)

279 | insertNVar : SizeOf local ->

280 |              NVar nm (local ++ outer) ->

281 |              NVar nm (local ++ n :: outer)

282 | insertNVar p v = case locateNVar p v of

283 |   Left v => embedNVar v

284 |   Right v => weakenNVar p (later v)

287 | insertNVarChiply : SizeOf local ->

288 |   NVar nm (local <>> outer) ->

289 |   NVar nm (local <>> n :: outer)

290 | insertNVarChiply p v

291 |   = rewrite chipsAsListAppend local (n :: outer) in

292 |     insertNVar (p <>> zero)

293 |   $ replace {p = NVar nm} (chipsAsListAppend local outer) v

296 | insertNVarNames : GenWeakenable (NVar name)

297 | insertNVarNames p q v = case locateNVar p v of

298 |   Left v => embedNVar v

299 |   Right v =>

300 |     rewrite appendAssociative local ns outer in

301 |     weakenNVar (p + q) v

305 | removeNVar : SizeOf local ->

306 |          NVar nm (local ++ n :: outer) ->

307 |   Maybe (NVar nm (local ++      outer))

308 | removeNVar s var = case locateNVar s var of

309 |   Left v => pure (embedNVar v)

310 |   Right v => weakenNVar s <$> isLater v

313 | insertVar : SizeOf local ->

314 |   Var (local ++ outer) ->

315 |   Var (local ++ n :: outer)

316 | insertVar p v = forgetName $ insertNVar p (recoverName v)

318 | weakenVar : SizeOf ns -> Var outer -> Var (ns ++ outer)

319 | weakenVar p v = forgetName $ weakenNVar p (recoverName v)

321 | insertVarNames : GenWeakenable Var

322 | insertVarNames p q v = forgetName $ insertNVarNames p q (recoverName v)

326 | removeVar : SizeOf local ->

327 |          Var (local ++ n :: outer) ->

328 |   Maybe (Var (local ++      outer))

329 | removeVar s var = forgetName <$> removeNVar s (recoverName var)

335 | strengthenIsVar : {n : Nat} -> (s : SizeOf inner) ->

336 |   (0 p : IsVar x n (inner ++ vars)) ->

337 |   Maybe (Erased (IsVar x (n `minus` size s) vars))

338 | strengthenIsVar s p = case locateIsVar s p of

339 |   Left _ => Nothing

340 |   Right p => pure p

342 | strengthenVar : SizeOf inner ->

343 |   Var (inner ++ vars) -> Maybe (Var vars)

344 | strengthenVar s (MkVar p)

345 |   = do MkErased p <- strengthenIsVar s p

346 |        pure (MkVar p)

348 | strengthenNVar : SizeOf inner ->

349 |   NVar x (inner ++ vars) -> Maybe (NVar x vars)

350 | strengthenNVar s (MkNVar p)

351 |   = do MkErased p <- strengthenIsVar s p

352 |        pure (MkNVar p)

357 | 0 lookup :

358 |   CompatibleVars xs ys ->

359 |   {idx : Nat} ->

360 |   (0 p : IsVar {a} name idx xs) ->

361 |   a

362 | lookup Pre p = name

363 | lookup (Ext {m} x) First = m

364 | lookup (Ext x) (Later p) = lookup x p

366 | 0 compatIsVar :

367 |   (ns : CompatibleVars xs ys) ->

368 |   {idx : Nat} -> (0 p : IsVar name idx xs) ->

369 |   IsVar (lookup ns p) idx ys

370 | compatIsVar Pre p = p

371 | compatIsVar (Ext {n} x) First = First

372 | compatIsVar (Ext {n} x) (Later p) = Later (compatIsVar x p)

374 | compatVar : CompatibleVars xs ys -> Var xs -> Var ys

375 | compatVar prf (MkVar p) = MkVar (compatIsVar prf p)

381 | thinIsVar : {idx : Nat} -> (0 p : IsVar name idx xs) ->

382 |   Thin xs ys -> Var ys

383 | thinIsVar p Refl = MkVar p

384 | thinIsVar p (Drop th) = later (thinIsVar p th)

385 | thinIsVar First (Keep th) = first

386 | thinIsVar (Later p) (Keep th) = later (thinIsVar p th)

389 | shrinkIsVar : {idx : Nat} -> (0 p : IsVar name idx xs) ->

390 |   Thin ys xs -> Maybe (Var ys)

391 | shrinkIsVar prf Refl = Just (MkVar prf)

392 | shrinkIsVar First (Drop p) = Nothing

393 | shrinkIsVar (Later x) (Drop p) = shrinkIsVar x p

394 | shrinkIsVar First (Keep p) = Just first

395 | shrinkIsVar (Later x) (Keep p) = later <$> shrinkIsVar x p

402 | 0 FreelyEmbeddableIsVar : FreelyEmbeddable (IsVar x k)

403 | FreelyEmbeddableIsVar = MkFreelyEmbeddable embedIsVar

406 | GenWeaken (Var {a = Name}) where

407 |   genWeakenNs = insertVarNames

411 | WeakenVar : Weaken (Var {a = Name})

412 | WeakenVar = GenWeakenWeakens

415 | Strengthen (Var {a = Name}) where

416 |   strengthenNs = strengthenVar

419 | FreelyEmbeddable (Var {a = Name}) where

420 |   embed (MkVar p) = MkVar (embedIsVar p)

423 | IsScoped (Var {a = Name}) where

424 |   compatNs = compatVar

426 |   thin (MkVar p) = thinIsVar p

427 |   shrink (MkVar p) = shrinkIsVar p

430 | GenWeaken (NVar {a = Name} nm) where

431 |   genWeakenNs = insertNVarNames

435 | WeakenNVar : Weaken (NVar {a = Name} nm)

436 | WeakenNVar = GenWeakenWeakens

439 | Strengthen (NVar {a = Name} nm) where

440 |   strengthenNs = strengthenNVar

443 | FreelyEmbeddable (NVar {a = Name} nm) where

444 |   embed (MkNVar p) = MkNVar (embedIsVar p)

451 | shiftUnderNs : SizeOf {a = Name} inner ->

452 |                {idx : _} ->

453 |                (0 p : IsVar n idx (x :: inner ++ outer)) ->

454 |                NVar n (inner ++ x :: outer)

455 | shiftUnderNs s First = weakenNs s (MkNVar First)

456 | shiftUnderNs s (Later p) = insertNVar s (MkNVar p)