module Total.Syntax

import public Data.List
import public Data.List.Quantifiers
import public Data.SnocList
import public Data.SnocList.Quantifiers
import public Total.Term
import public Total.Term.CoDebruijn

infixr 20 ~>*
infixl 9 .~, .*

public export
data Len : SnocList a -> Type where
  Z : Len [<]
  S : Len sx -> Len (sx :< x)

%name Len k

export
lenToNat : Len sx -> Nat
lenToNat Z = 0
lenToNat (S k) = S (lenToNat k)

public export
(~>*) : SnocList Ty -> Ty -> Ty
tys ~>* ty = foldr (~>) ty tys

public export
0 Fun : (sx : SnocList a) -> (a -> Type) -> Type -> Type
Fun [<] p ret = ret
Fun (sx :< x) p ret = Fun sx p (p x -> ret)

after : Len sx -> (r -> s) -> Fun sx p r -> Fun sx p s
after Z f = f
after (S k) f = after k (f .)

before : Len sx -> (forall x. p x -> q x) -> Fun sx q ret -> Fun sx p ret
before Z f = id
before (S k) f = before k f . after k (. f)

export
lit : Nat -> FullTerm N ctx
lit 0 = Zero `Over` Empty
lit (S n) = suc (lit n)

absHelper :
  Len tys ->
  Fun tys (flip Elem (ctx ++ tys)) (FullTerm ty (ctx ++ tys)) ->
  FullTerm (tys ~>* ty) ctx
absHelper Z x = x
absHelper (S k) x =
  absHelper k $
  after k (\f => CoDebruijn.abs (f SnocList.Elem.Here)) $
  before k SnocList.Elem.There x

export
abs' :
  Len tys ->
  Fun tys (flip FullTerm (ctx ++ tys)) (FullTerm ty (ctx ++ tys)) ->
  FullTerm (tys ~>* ty) ctx
abs' k = absHelper k . before k var

export
app' :
  {tys : SnocList Ty} ->
  FullTerm (tys ~>* ty) ctx ->
  All (flip FullTerm ctx) tys ->
  FullTerm ty ctx
app' t [<] = t
app' t (us :< u) = app (app' t us) u

-- export
-- compose :
--   {ty, ty' : Ty} ->
--   (t : FullTerm (ty' ~> ty'') ctx) ->
--   (u : FullTerm (ty ~> ty') ctx) ->
--   Len u.support =>
--   Covering Covers t.thin u.thin ->
--   CoTerm (ty ~> ty'') ctx
-- compose (t `Over` thin1) (u `Over` thin2) cover =
--   Abs
--     (MakeBound
--       (App
--         (MakePair
--           (t `Over` Drop thin1)
--           (App
--             (MakePair
--               (u `Over` Drop id)
--               (Var `Over` Keep empty)
--               (DropKeep (coverIdLeft empty)))
--            `Over` Keep thin2)
--           (DropKeep cover)))
--       (Keep Empty))

-- export
-- (.~) :
--   Len ctx =>
--   {ty, ty' : Ty} ->
--   CoTerm (ty' ~> ty'') ctx ->
--   CoTerm (ty ~> ty') ctx ->
--   CoTerm (ty ~> ty'') ctx
-- t .~ u = compose (t `Over` id) (u `Over` id) (coverIdLeft id)

export
(.) :
  {ty, ty' : Ty} ->
  FullTerm (ty' ~> ty'') ctx ->
  FullTerm (ty ~> ty') ctx ->
  FullTerm (ty ~> ty'') ctx
t . u = abs' (S Z) (\x => app (drop t) (app (drop u) x))

export
(.*) :
  {ty : Ty} ->
  {tys : SnocList Ty} ->
  FullTerm (ty ~> ty') ctx ->
  FullTerm (tys ~>* ty) ctx ->
  FullTerm (tys ~>* ty') ctx
(.*) {tys = [<]} t u = app t u
(.*) {tys = tys :< ty''} t u = abs' (S Z) (\f => drop t . f) .*  u

export
lift : FullTerm ty [<] -> FullTerm ty ctx
lift t = wkn t Empty

export
id : FullTerm (ty ~> ty) [<]
id = Abs Var `Over` Empty