module Core.Environment.Extension

import Core.Environment
import Core.Term.Thinned
import Core.Thinning

-- Definition ------------------------------------------------------------------

public export
data Extends : m `Thins` n -> Env n -> Env m -> Type where
  Id : Extends (id n) env env
  Drop : Extends thin env1 env2 -> Extends (drop thin) (env1 :< a) env2
  Keep : Extends thin env1 env2 -> Extends (keep thin) (env1 :< wkn a thin) (env2 :< a)

%name Extends ext

-- Composition -----------------------------------------------------------------

public export
(.) : Extends thin2 env3 env2 -> Extends thin1 env2 env1 -> Extends (thin2 . thin1) env3 env1
Id . ext1 =
  rewrite compLeftId thin1 in
  ext1
Drop {thin = thin2} ext2 . ext1 =
  rewrite compLeftDrop thin2 thin1 in
  Drop (ext2 . ext1)
Keep {thin = thin2} ext2 . Id =
  rewrite compRightId (keep thin2) in
  Keep ext2
Keep {thin = thin2} ext2 . Drop {thin = thin1} ext1 =
  rewrite compRightDrop thin2 thin1 in
  Drop (ext2 . ext1)
Keep {thin = thin2} ext2 . Keep {thin = thin1, a} ext1 =
  rewrite compKeep thin2 thin1 in
  rewrite wknHomo a thin1 thin2 in
  Keep (ext2 . ext1)