module Term

import Data.Nat

import Misc

%default total

{-
  The type of terms is indexed by the size of the environment in which
  they are valid, that is, it is impossible to construct an ill-scoped term.
-}
public export
data Term : (_ : Index) -> Type where
  TType   : Term n                         -- The type of types (type in type)
  TDef    : Name -> Term n                 -- Axiomised term
  TLam    : Term n -> Term (S n) -> Term n -- Lambda abstraction (λ Type -> Scope)
  TPi     : Term n -> Term (S n) -> Term n -- Pi type            (∏ A    -> B a  )
  TApp    : Term n -> Term n -> Term n     -- Appliction
  TVar    : (n : Nat) -> LT n m -> Term m  -- Variable

public export
weaken : {p, q : _} -> LTE p q -> Term p -> Term q
weaken _ TType    = TType
weaken _ (TDef n) = TDef n
weaken p (TLam ty sc) = TLam (weaken p ty) (weaken (LTESucc p) sc)
weaken p (TPi  a  bx) = TLam (weaken p a ) (weaken (LTESucc p) bx)
weaken p (TApp f x) = TApp (weaken p f) (weaken p x)
{-
  Getting new index
  =================

    New index is 

      old + Δctx

    in this case

      r + (q - p)

    which since p <= q is equivalent to

      (r + q) - p


  Proving validity of new index
  =============================

              r <= p           => (+mono)
          r + q <= p + q       => (-mono)
    (r + q) - p <= (p + q) - p => (lteTransp -+)
    (r + q) - p <= q           ∎

-}
weaken {p = S p} {q = S q} (LTESucc p1) (TVar r p2') =
  case p2' of 
    LTESucc p2 => TVar (minus (r + q) p)
      (LTESucc (lteTransp (minusLteMonotone (plusLteMonotoneRight q r p p2)) Refl (minusPlus p)))