module Total.Term.CoDebruijn

import public Data.SnocList.Elem
import public Thinning
import Syntax.PreorderReasoning
import Total.Term

%prefix_record_projections off

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

public export
data FullTerm : Ty -> SnocList Ty -> Type where
  Var : FullTerm ty [<ty]
  Const : FullTerm ty' ctx -> FullTerm (ty ~> ty') ctx
  Abs : FullTerm ty' (ctx :< ty) -> FullTerm (ty ~> ty') ctx
  App : {ty : Ty} -> Pair (FullTerm (ty ~> ty')) (FullTerm ty) ctx -> FullTerm ty' ctx
  Zero : FullTerm N [<]
  Suc : FullTerm N ctx -> FullTerm N ctx
  Rec : Pair (FullTerm N) (Pair (FullTerm ty) (FullTerm (ty ~> ty))) ctx -> FullTerm ty ctx

%name FullTerm t, u, v

public export
CoTerm : Ty -> SnocList Ty -> Type
CoTerm ty ctx = Thinned (FullTerm ty) ctx

-- Smart Constructors ----------------------------------------------------------

public export
var : Elem ty ctx -> CoTerm ty ctx
var i = Var `Over` Point i

public export
abs : CoTerm ty' (ctx :< ty) -> CoTerm (ty ~> ty') ctx
abs (t `Over` Id) = Abs t `Over` Id
abs (t `Over` Empty) = Const t `Over` Empty
abs (t `Over` Drop thin) = Const t `Over` thin
abs (t `Over` Keep thin) = Abs t `Over` thin

public export
app : {ty : Ty} -> CoTerm (ty ~> ty') ctx -> CoTerm ty ctx -> CoTerm ty' ctx
app t u = map App (MkPair t u)

public export
zero : CoTerm N ctx
zero = Zero `Over` Empty

public export
suc : CoTerm N ctx -> CoTerm N ctx
suc = map Suc

public export
rec : CoTerm N ctx -> CoTerm ty ctx -> CoTerm (ty ~> ty) ctx -> CoTerm ty ctx
rec t u v = map Rec $ MkPair t (MkPair u v)

-- Raw Interfaces --------------------------------------------------------------

export
Point Ty CoTerm where
  point = var

export
Weaken Ty CoTerm where
  wkn = Thinning.wkn
  drop = Thinning.drop

export PointWeaken Ty CoTerm where

-- Substitution Operation ------------------------------------------------------

public export
subst : CoTerm ty ctx -> Subst CoTerm ctx ctx' -> CoTerm ty ctx'
public export
subst' : FullTerm ty ctx -> Subst CoTerm ctx ctx' -> CoTerm ty ctx'

subst (t `Over` thin) sub = subst' t (restrict sub thin)

subst' Var sub = index sub Here
subst' (Const t) sub = abs (drop $ subst' t sub)
subst' (Abs t) sub = abs (subst' t $ lift sub)
subst' (App (MakePair t u _)) sub = app (subst t sub) (subst u sub)
subst' Zero sub = zero
subst' (Suc t) sub = suc (subst' t sub)
subst' (Rec (MakePair t (MakePair u v _ `Over` thin) _)) sub =
  rec (subst t sub) (subst u (restrict sub thin)) (subst v (restrict sub thin))

-- Initiality ------------------------------------------------------------------

toTerm' : FullTerm ty ctx -> ctx `Thins` ctx' -> Term ty ctx'
toTerm' Var thin = Var (index thin Here)
toTerm' (Const t) thin = Abs (toTerm' t (Drop thin))
toTerm' (Abs t) thin = Abs (toTerm' t (Keep thin))
toTerm' (App (MakePair (t `Over` thin1) (u `Over` thin2) _)) thin =
  App (toTerm' t (thin . thin1)) (toTerm' u (thin . thin2))
toTerm' Zero thin = Zero
toTerm' (Suc t) thin = Suc (toTerm' t thin)
toTerm'
  (Rec
    (MakePair
      (t `Over` thin1)
      (MakePair (u `Over` thin2) (v `Over` thin3) _ `Over` thin') _))
  thin =
  Rec
    (toTerm' t (thin . thin1))
    (toTerm' u ((thin . thin') . thin2))
    (toTerm' v ((thin . thin') . thin3))

export
toTerm : CoTerm ty ctx -> Term ty ctx
toTerm (t `Over` thin) = toTerm' t thin

export
fromTerm : Term ty ctx -> CoTerm ty ctx
fromTerm (Var i) = var i
fromTerm (Abs t) = abs (fromTerm t)
fromTerm (App t u) = app (fromTerm t) (fromTerm u)
fromTerm Zero = zero
fromTerm (Suc t) = suc (fromTerm t)
fromTerm (Rec t u v) = rec (fromTerm t) (fromTerm u) (fromTerm v)

-- Properties ------------------------------------------------------------------

-- Weakening

export
FullWeaken Ty CoTerm where
  dropIsWkn (t `Over` thin) = ?dropIsWkn_rhs

  wknCong = ?wknCong_rhs

  wknId = ?wknId_rhs

  wknHomo = ?wknHomo_rhs

-- -- wknToTerm' :
-- --   (t : FullTerm ty ctx) ->
-- --   (thin : ctx `Thins` ctx') ->
-- --   (thin' : ctx' `Thins` ctx''') ->
-- --   wkn (toTerm' t thin) thin' = toTerm' t (thin' . thin)
-- -- wknToTerm' Var thin thin' = cong Var (indexHomo thin' thin Here)
-- -- wknToTerm' (Abs (MakeBound t (Drop Empty))) thin thin' =
-- --   cong Abs (wknToTerm' t (Drop thin) (Keep thin'))
-- -- wknToTerm' (Abs (MakeBound t (Keep Empty))) thin thin' =
-- --   cong Abs (wknToTerm' t (Keep thin) (Keep thin'))
-- -- wknToTerm' (App (MakePair (t `Over` thin1) (u `Over` thin2) _)) thin thin' =
-- --   rewrite sym $ assoc thin' thin thin1 in
-- --   rewrite sym $ assoc thin' thin thin2 in
-- --   cong2 App (wknToTerm' t (thin . thin1) thin') (wknToTerm' u (thin . thin2) thin')
-- -- wknToTerm' Zero thin thin' = Refl
-- -- wknToTerm' (Suc t) thin thin' = cong Suc (wknToTerm' t thin thin')
-- -- wknToTerm'
-- --   (Rec
-- --     (MakePair
-- --       (t `Over` thin1)
-- --       (MakePair (u `Over` thin2) (v `Over` thin3) _ `Over` thin'') _))
-- --   thin
-- --   thin' =
-- --   rewrite sym $ assoc thin' thin thin1 in
-- --   rewrite sym $ assoc (thin' . thin) thin'' thin2 in
-- --   rewrite sym $ assoc thin'  thin (thin'' . thin2) in
-- --   rewrite sym $ assoc thin thin'' thin2 in
-- --   rewrite sym $ assoc (thin' . thin) thin'' thin3 in
-- --   rewrite sym $ assoc thin'  thin (thin'' . thin3) in
-- --   rewrite sym $ assoc thin thin'' thin3 in
-- --   cong3 Rec
-- --     (wknToTerm' t (thin . thin1) thin')
-- --     (wknToTerm' u (thin . (thin'' . thin2)) thin')
-- --     (wknToTerm' v (thin . (thin'' . thin3)) thin')

-- -- export
-- -- wknToTerm :
-- --   (t : CoTerm ty ctx) ->
-- --   (thin : ctx `Thins` ctx') ->
-- --   wkn (toTerm t) thin = toTerm (wkn t thin)
-- -- wknToTerm (t `Over` thin') thin = wknToTerm' t thin' thin

-- -- export
-- -- toTermVar : Len ctx => (i : Elem ty ctx) -> toTerm (var i) = Var i
-- -- toTermVar i = cong Var $ indexPoint i

-- -- export
-- -- toTermApp :
-- --   (t : CoTerm (ty ~> ty') ctx) ->
-- --   (u : CoTerm ty ctx) ->
-- --   toTerm (app t u) = App (toTerm t) (toTerm u)
-- -- toTermApp (t `Over` thin1) (u `Over` thin2) =
-- --   cong2 App
-- --     (cong (toTerm' t) $ irrelevantEq $ triangleCorrect (coprod thin1 thin2).left)
-- --     (cong (toTerm' u) $ irrelevantEq $ triangleCorrect (coprod thin1 thin2).right)

-- -- indexShift :
-- --   (sub : Subst CoTerm ctx ctx') ->
-- --   (i : Elem ty ctx) ->
-- --   index (shift sub) i = drop (index sub i)
-- -- indexShift (sub :< t) Here = Refl
-- -- indexShift (sub :< t) (There i) = indexShift sub i

-- -- indexBase : (thin : [<ty] `Thins` ctx') -> index (Base thin) Here = Var `Over` thin
-- -- indexBase (Drop thin) = trans (indexShift (Base thin) Here) (cong drop (indexBase thin))
-- -- indexBase (Keep thin) = irrelevantEq $ cong ((Var `Over`) . Keep) $ emptyUnique empty thin

-- -- restrictShift :
-- --   (sub : Subst CoTerm ctx' ctx'') ->
-- --   (thin : ctx `Thins` ctx') ->
-- --   restrict (shift sub) thin = shift (restrict sub thin)
-- -- restrictShift [<] Empty = Refl
-- -- restrictShift (sub :< t) (Drop thin) = restrictShift sub thin
-- -- restrictShift (sub :< t) (Keep thin) = cong (:< drop t) (restrictShift sub thin)

-- -- restrictBase :
-- --   (thin2 : ctx' `Thins` ctx'') ->
-- --   (thin1 : ctx `Thins` ctx') ->
-- --   CoDebruijn.restrict (Base thin2) thin1 = Base (thin2 . thin1)
-- -- restrictBase Empty Empty = Refl
-- -- restrictBase (Drop thin2) thin1 =
-- --   trans
-- --     (restrictShift (Base thin2) thin1)
-- --     (cong shift $ restrictBase thin2 thin1)
-- -- restrictBase (Keep thin2) (Drop thin1) =
-- --   trans
-- --     (restrictShift (Base thin2) thin1)
-- --     (cong shift $ restrictBase thin2 thin1)
-- -- restrictBase (Keep thin2) (Keep thin1) =
-- --   cong (:< (Var `Over` point Here)) $
-- --   trans
-- --     (restrictShift (Base thin2) thin1)
-- --     (cong shift $ restrictBase thin2 thin1)

-- substBase :
--   (t : FullTerm ty ctx) ->
--   (thin : ctx `Thins` ctx') ->
--   subst' t (Base thin) = t `Over` thin
-- -- substBase Var thin = indexBase thin
-- -- substBase (Abs (MakeBound t (Drop Empty))) thin =
-- --   Calc $
-- --     |~ map Abs (MkBound (S Z) (subst' t (shift $ Base thin)))
-- --     ~~ map Abs (MkBound (S Z) (t `Over` Drop thin))
-- --       ...(cong (map Abs . MkBound (S Z)) $ substBase t (Drop thin))
-- --     ~~ map Abs (MakeBound t (Drop Empty) `Over` thin)
-- --       ...(Refl)
-- --     ~~ (Abs (MakeBound t (Drop Empty)) `Over` thin)
-- --       ...(Refl)
-- -- substBase (Abs (MakeBound t (Keep Empty))) thin =
-- --   Calc $
-- --     |~ map Abs (MkBound (S Z) (subst' t (lift $ Base thin)))
-- --     ~~ map Abs (MkBound (S Z) (t `Over` Keep thin))
-- --       ...(cong (map Abs . MkBound (S Z)) $ substBase t (Keep thin))
-- --     ~~ map Abs (MakeBound t (Keep Empty) `Over` thin)
-- --       ...(Refl)
-- --     ~~ (Abs (MakeBound t (Keep Empty)) `Over` thin)
-- --       ...(Refl)
-- -- substBase (App (MakePair (t `Over` thin1) (u `Over` thin2) cover)) thin =
-- --   rewrite restrictBase thin thin1 in
-- --   rewrite restrictBase thin thin2 in
-- --   rewrite substBase t (thin . thin1) in
-- --   rewrite substBase u (thin . thin2) in
-- --   rewrite coprodEta thin cover in
-- --   Refl
-- -- substBase Zero thin = cong (Zero `Over`) $ irrelevantEq $ emptyUnique empty thin
-- -- substBase (Suc t) thin = cong (map Suc) $ substBase t thin
-- -- substBase
-- --   (Rec (MakePair
-- --       (t `Over` thin1)
-- --       (MakePair
-- --         (u `Over` thin2)
-- --         (v `Over` thin3)
-- --         cover'
-- --       `Over` thin')
-- --       cover))
-- --   thin =
-- --   rewrite restrictBase thin thin1 in
-- --   rewrite restrictBase thin thin' in
-- --   rewrite restrictBase (thin . thin') thin2 in
-- --   rewrite restrictBase (thin . thin') thin3 in
-- --   rewrite substBase t (thin . thin1) in
-- --   rewrite substBase u ((thin . thin') . thin2) in
-- --   rewrite substBase v ((thin . thin') . thin3) in
-- --   rewrite coprodEta (thin . thin') cover' in
-- --   rewrite coprodEta thin cover in
-- --   Refl

-- export
-- substId : (t : CoTerm ty ctx) -> subst t (Base Id) = t
-- substId (t `Over` thin) =
--   Calc $
--     |~ subst' t (restrict (Base Id) thin)
--     ~~ subst' t (Base (Id . thin))        ...(cong (subst' t) $ restrictBase Id thin)
--     ~~ subst' t (Base thin)               ...(Refl)
--     ~~ (t `Over` thin)                    ...(substBase t thin)