module Quox.Syntax.Term.Tighten

import Quox.Syntax.Term.Base
import Quox.Syntax.Term.Subst
import public Quox.OPE
import Quox.No

%default total


export
Tighten Dim where
  tighten p (K e loc) = pure $ K e loc
  tighten p (B i loc) = B <$> tighten p i <*> pure loc

export
tightenScope : (forall m, n. OPE m n -> f n -> Maybe (f m)) ->
               {s : Nat} -> OPE m n -> Scoped s f n -> Maybe (Scoped s f m)
tightenScope f p (S names (Y body)) = SY names <$> f (keepN s p) body
tightenScope f p (S names (N body)) = S names . N <$> f p body

export
tightenDScope : {0 f : Nat -> Nat -> Type} ->
                (forall m, n, k. OPE m n -> f n k -> Maybe (f m k)) ->
                OPE m n -> Scoped s (f n) k -> Maybe (Scoped s (f m) k)
tightenDScope f p (S names (Y body)) = SY names <$> f p body
tightenDScope f p (S names (N body)) = S names . N <$> f p body


mutual
  private
  tightenT : OPE n1 n2 -> Term d n2 -> Maybe (Term d n1)
  tightenT p s =
    let Element s' _ = pushSubsts s in
    tightenT' p $ assert_smaller s s'

  private
  tightenE : OPE n1 n2 -> Elim d n2 -> Maybe (Elim d n1)
  tightenE p e =
    let Element e' _ = pushSubsts e in
    tightenE' p $ assert_smaller e e'

  private
  tightenT' : OPE n1 n2 -> (t : Term d n2) -> (0 nt : NotClo t) =>
              Maybe (Term d n1)
  tightenT' p (TYPE l loc) = pure $ TYPE l loc
  tightenT' p (Pi qty arg res loc) =
    Pi qty <$> tightenT p arg <*> tightenS p res <*> pure loc
  tightenT' p (Lam body loc) =
    Lam <$> tightenS p body <*> pure loc
  tightenT' p (Sig fst snd loc) =
    Sig <$> tightenT p fst <*> tightenS p snd <*> pure loc
  tightenT' p (Pair fst snd loc) =
    Pair <$> tightenT p fst <*> tightenT p snd <*> pure loc
  tightenT' p (Enum cases loc) =
    pure $ Enum cases loc
  tightenT' p (Tag tag loc) =
    pure $ Tag tag loc
  tightenT' p (Eq ty l r loc) =
    Eq <$> tightenDS p ty <*> tightenT p l <*> tightenT p r <*> pure loc
  tightenT' p (DLam body loc) =
    DLam <$> tightenDS p body <*> pure loc
  tightenT' p (Nat loc) =
    pure $ Nat loc
  tightenT' p (Zero loc) =
    pure $ Zero loc
  tightenT' p (Succ s loc) =
    Succ <$> tightenT p s <*> pure loc
  tightenT' p (BOX qty ty loc) =
    BOX qty <$> tightenT p ty <*> pure loc
  tightenT' p (Box val loc) =
    Box <$> tightenT p val <*> pure loc
  tightenT' p (E e) =
    assert_total $ E <$> tightenE p e

  private
  tightenE' : OPE n1 n2 -> (e : Elim d n2) -> (0 ne : NotClo e) =>
              Maybe (Elim d n1)
  tightenE' p (F x u loc) =
    pure $ F x u loc
  tightenE' p (B i loc) =
    B <$> tighten p i <*> pure loc
  tightenE' p (App fun arg loc) =
    App <$> tightenE p fun <*> tightenT p arg <*> pure loc
  tightenE' p (CasePair qty pair ret body loc) =
    CasePair qty <$> tightenE p pair
                 <*> tightenS p ret
                 <*> tightenS p body
                 <*> pure loc
  tightenE' p (CaseEnum qty tag ret arms loc) =
    CaseEnum qty <$> tightenE p tag
                 <*> tightenS p ret
                 <*> traverse (tightenT p) arms
                 <*> pure loc
  tightenE' p (CaseNat qty qtyIH nat ret zero succ loc) =
    CaseNat qty qtyIH
      <$> tightenE p nat
      <*> tightenS p ret
      <*> tightenT p zero
      <*> tightenS p succ
      <*> pure loc
  tightenE' p (CaseBox qty box ret body loc) =
    CaseBox qty <$> tightenE p box
                <*> tightenS p ret
                <*> tightenS p body
                <*> pure loc
  tightenE' p (DApp fun arg loc) =
    DApp <$> tightenE p fun <*> pure arg <*> pure loc
  tightenE' p (Ann tm ty loc) =
    Ann <$> tightenT p tm <*> tightenT p ty <*> pure loc
  tightenE' p (Coe ty q0 q1 val loc) =
    Coe <$> tightenDS p ty
        <*> pure q0 <*> pure q1
        <*> tightenT p val
        <*> pure loc
  tightenE' p (Comp ty q0 q1 val r zero one loc) =
    Comp <$> tightenT p ty
         <*> pure q0 <*> pure q1
         <*> tightenT p val
         <*> pure r
         <*> tightenDS p zero
         <*> tightenDS p one
         <*> pure loc
  tightenE' p (TypeCase ty ret arms def loc) =
    TypeCase <$> tightenE p ty
             <*> tightenT p ret
             <*> traverse (tightenS p) arms
             <*> tightenT p def
             <*> pure loc

  export
  tightenS : {s : Nat} -> OPE m n ->
             ScopeTermN s f n -> Maybe (ScopeTermN s f m)
  tightenS = assert_total $ tightenScope tightenT

  export
  tightenDS : OPE m n -> DScopeTermN s f n -> Maybe (DScopeTermN s f m)
  tightenDS = assert_total $ tightenDScope tightenT {f = \n, d => Term d n}

export Tighten (Elim d) where tighten p e = tightenE p e
export Tighten (Term d) where tighten p t = tightenT p t


mutual
  export
  dtightenT : OPE d1 d2 -> Term d2 n -> Maybe (Term d1 n)
  dtightenT p s =
    let Element s' _ = pushSubsts s in
    dtightenT' p $ assert_smaller s s'

  export
  dtightenE : OPE d1 d2 -> Elim d2 n -> Maybe (Elim d1 n)
  dtightenE p e =
    let Element e' _ = pushSubsts e in
    dtightenE' p $ assert_smaller e e'

  private
  dtightenT' : OPE d1 d2 -> (t : Term d2 n) -> (0 nt : NotClo t) =>
               Maybe (Term d1 n)
  dtightenT' p (TYPE l loc) =
    pure $ TYPE l loc
  dtightenT' p (Pi qty arg res loc) =
    Pi qty <$> dtightenT p arg <*> dtightenS p res <*> pure loc
  dtightenT' p (Lam body loc) =
    Lam <$> dtightenS p body <*> pure loc
  dtightenT' p (Sig fst snd loc) =
    Sig <$> dtightenT p fst <*> dtightenS p snd <*> pure loc
  dtightenT' p (Pair fst snd loc) =
    Pair <$> dtightenT p fst <*> dtightenT p snd <*> pure loc
  dtightenT' p (Enum cases loc) =
    pure $ Enum cases loc
  dtightenT' p (Tag tag loc) =
    pure $ Tag tag loc
  dtightenT' p (Eq ty l r loc) =
    Eq <$> dtightenDS p ty <*> dtightenT p l <*> dtightenT p r <*> pure loc
  dtightenT' p (DLam body loc) =
    DLam <$> dtightenDS p body <*> pure loc
  dtightenT' p (Nat loc) =
    pure $ Nat loc
  dtightenT' p (Zero loc) =
    pure $ Zero loc
  dtightenT' p (Succ s loc) =
    Succ <$> dtightenT p s <*> pure loc
  dtightenT' p (BOX qty ty loc) =
    BOX qty <$> dtightenT p ty <*> pure loc
  dtightenT' p (Box val loc) =
    Box <$> dtightenT p val <*> pure loc
  dtightenT' p (E e) =
    assert_total $ E <$> dtightenE p e

  export
  dtightenE' : OPE d1 d2 -> (e : Elim d2 n) -> (0 ne : NotClo e) =>
               Maybe (Elim d1 n)
  dtightenE' p (F x u loc) =
    pure $ F x u loc
  dtightenE' p (B i loc) =
    pure $ B i loc
  dtightenE' p (App fun arg loc) =
    App <$> dtightenE p fun <*> dtightenT p arg <*> pure loc
  dtightenE' p (CasePair qty pair ret body loc) =
    CasePair qty <$> dtightenE p pair
                 <*> dtightenS p ret
                 <*> dtightenS p body
                 <*> pure loc
  dtightenE' p (CaseEnum qty tag ret arms loc) =
    CaseEnum qty <$> dtightenE p tag
                 <*> dtightenS p ret
                 <*> traverse (dtightenT p) arms
                 <*> pure loc
  dtightenE' p (CaseNat qty qtyIH nat ret zero succ loc) =
    CaseNat qty qtyIH
      <$> dtightenE p nat
      <*> dtightenS p ret
      <*> dtightenT p zero
      <*> dtightenS p succ
      <*> pure loc
  dtightenE' p (CaseBox qty box ret body loc) =
    CaseBox qty <$> dtightenE p box
                <*> dtightenS p ret
                <*> dtightenS p body
                <*> pure loc
  dtightenE' p (DApp fun arg loc) =
    DApp <$> dtightenE p fun <*> tighten p arg <*> pure loc
  dtightenE' p (Ann tm ty loc) =
    Ann <$> dtightenT p tm <*> dtightenT p ty <*> pure loc
  dtightenE' p (Coe ty q0 q1 val loc) =
    [|Coe (dtightenDS p ty) (tighten p q0) (tighten p q1) (dtightenT p val)
          (pure loc)|]
  dtightenE' p (Comp ty q0 q1 val r zero one loc) =
    [|Comp (dtightenT p ty) (tighten p q0) (tighten p q1)
           (dtightenT p val) (tighten p r)
           (dtightenDS p zero) (dtightenDS p one) (pure loc)|]
  dtightenE' p (TypeCase ty ret arms def loc) =
    [|TypeCase (dtightenE p ty) (dtightenT p ret)
               (traverse (dtightenS p) arms) (dtightenT p def) (pure loc)|]

  export
  dtightenS : OPE d1 d2 -> ScopeTermN s d2 n -> Maybe (ScopeTermN s d1 n)
  dtightenS = assert_total $ tightenDScope dtightenT {f = Term}

  export
  dtightenDS : {s : Nat} -> OPE d1 d2 ->
               DScopeTermN s d2 n -> Maybe (DScopeTermN s d1 n)
  dtightenDS = assert_total $ tightenScope dtightenT


export Tighten (\d => Term d n) where tighten p t = dtightenT p t
export Tighten (\d => Elim d n) where tighten p e = dtightenE p e


parameters {auto _ : Tighten f} {s : Nat}
  export
  squeeze : Scoped s f n -> (BContext s, Either (f (s + n)) (f n))
  squeeze (S ns (N t)) = (ns, Right t)
  squeeze (S ns (Y t)) = (ns, maybe (Left t) Right $ tightenN s t)

  export
  squeeze' : Scoped s f n -> Scoped s f n
  squeeze' t = let (ns, res) = squeeze t in S ns $ either Y N res

parameters {0 f : Nat -> Nat -> Type}
           {auto tt : Tighten (\d => f d n)} {s : Nat}
  export
  dsqueeze : Scoped s (\d => f d n) d ->
             (BContext s, Either (f (s + d) n) (f d n))
  dsqueeze = squeeze

  export
  dsqueeze' : Scoped s (\d => f d n) d -> Scoped s (\d => f d n) d
  dsqueeze' = squeeze'


-- versions of SY, etc, that try to tighten and use SN automatically

public export %inline
ST : Tighten f => {s : Nat} -> BContext s -> f (s + n) -> Scoped s f n
ST names body = squeeze' $ SY names body

public export %inline
DST : {s : Nat} -> BContext s -> Term (s + d) n -> DScopeTermN s d n
DST names body = dsqueeze' {f = Term} $ SY names body

public export %inline
PiT : (qty : Qty) -> (x : BindName) ->
      (arg : Term d n) -> (res : Term d (S n)) -> (loc : Loc) -> Term d n
PiT {qty, x, arg, res, loc} = Pi {qty, arg, res = ST [< x] res, loc}

public export %inline
LamT : (x : BindName) -> (body : Term d (S n)) -> (loc : Loc) -> Term d n
LamT {x, body, loc} = Lam {body = ST [< x] body, loc}

public export %inline
SigT : (x : BindName) -> (fst : Term d n) ->
       (snd : Term d (S n)) -> (loc : Loc) -> Term d n
SigT {x, fst, snd, loc} = Sig {fst, snd = ST [< x] snd, loc}

public export %inline
EqT : (i : BindName) -> (ty : Term (S d) n) ->
      (l, r : Term d n) -> (loc : Loc) -> Term d n
EqT {i, ty, l, r, loc} = Eq {ty = DST [< i] ty, l, r, loc}

public export %inline
DLamT : (i : BindName) -> (body : Term (S d) n) -> (loc : Loc) -> Term d n
DLamT {i, body, loc} = DLam {body = DST [< i] body, loc}

public export %inline
CoeT : (i : BindName) -> (ty : Term (S d) n) ->
       (p, q : Dim d) -> (val : Term d n) -> (loc : Loc) -> Elim d n
CoeT {i, ty, p, q, val, loc} = Coe {ty = DST [< i] ty, p, q, val, loc}

public export %inline
typeCase1T : Elim d n -> Term d n ->
             (k : TyConKind) -> BContext (arity k) -> Term d (arity k + n) ->
             (loc : Loc) ->
             {default (Nat loc) def : Term d n} ->
             Elim d n
typeCase1T ty ret k ns body loc {def} =
  typeCase ty ret [(k ** ST ns body)] def loc


public export %inline
CompH' : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
         (r : Dim d) -> (zero, one : DScopeTerm d n) -> (loc : Loc) -> Elim d n
CompH' {ty, p, q, val, r, zero, one, loc} =
  let ty' = DST ty.names $ ty.term // (B VZ ty.name.loc ::: shift 2) in
  Comp {
    ty = dsub1 ty q, p, q,
    val = E $ Coe ty p q val val.loc, r,
    zero = DST zero.names $ E $
      Coe ty' (B VZ zero.loc) (weakD 1 q) zero.term zero.loc,
    one = DST one.names $ E $
      Coe ty' (B VZ one.loc) (weakD 1 q) one.term one.loc,
    loc
  }

||| heterogeneous composition, using Comp and Coe (and subst)
|||
||| comp [i ⇒ A] @p @q s @r { 0 j ⇒ t₀; 1 j ⇒ t₁ }
||| ≔
||| comp [A‹q/i›] @p @q (coe [i ⇒ A] @p @q s) @r {
|||   0 j ⇒ coe [i ⇒ A] @j @q t₀;
|||   1 j ⇒ coe [i ⇒ A] @j @q t₁
||| }
public export %inline
CompH : (i : BindName) -> (ty : Term (S d) n) ->
        (p, q : Dim d) -> (val : Term d n) -> (r : Dim d) ->
        (j0 : BindName) -> (zero : Term (S d) n) ->
        (j1 : BindName) -> (one : Term (S d) n) ->
        (loc : Loc) ->
        Elim d n
CompH {i, ty, p, q, val, r, j0, zero, j1, one, loc} =
  CompH' {ty = DST [< i] ty, p, q, val, r,
          zero = DST [< j0] zero, one = DST [< j1] one, loc}