module Quox.Typing

import public Quox.Syntax
import public Quox.Context
import public Quox.Definition

import Data.Nat
import public Data.SortedMap
import Control.Monad.Reader
import Control.Monad.State
import Generics.Derive

%hide TT.Name
%default total
%language ElabReflection

%default total


public export
data DContext : Nat -> Type where
  DNil  : DContext 0
  DBind : DContext d -> DContext (S d)
  DEq   : Dim d -> Dim d -> DContext d -> DContext d

public export
TContext : Nat -> Nat -> Type
TContext d = Context (Term d)

public export
QContext : Nat -> Type
QContext = Context' Qty

public export
QOutput : Nat -> Type
QOutput = QContext


public export
record TyContext (d, n : Nat) where
  constructor MkTyContext
  dctx : DContext d
  tctx : TContext d n
  qctx : QContext n

%name TyContext ctx


namespace TContext
  export
  pushD : TContext d n -> TContext (S d) n
  pushD tel = map (/// shift 1) tel


namespace TyContext
  export
  extendTy : Term d n -> Qty -> TyContext d n -> TyContext d (S n)
  extendTy s rho = {tctx $= (:< s), qctx $= (:< rho)}

  export
  extendDim : TyContext d n -> TyContext (S d) n
  extendDim = {dctx $= DBind, tctx $= pushD}

  export
  eqDim : Dim d -> Dim d -> TyContext d n -> TyContext d n
  eqDim p q = {dctx $= DEq p q}


namespace QOutput
  export
  (+) : QOutput n -> QOutput n -> QOutput n
  (+) = zipWith (+)

  export
  (*) : Qty -> QOutput n -> QOutput n
  (*) pi = map (pi *)

  export
  zero : {n : Nat} -> QOutput n
  zero = pure Zero


public export
CheckResult : Nat -> Type
CheckResult = QOutput

public export
record InferResult d n where
  constructor InfRes
  type : Term d n
  qout : QOutput n


public export
data EqMode = Equal | Sub
%runElab derive "EqMode" [Generic, Meta, Eq, Ord, DecEq, Show]


public export
data Error
= ExpectedTYPE (Term d n)
| ExpectedPi   (Term d n)
| BadUniverse  Universe Universe

| ClashT EqMode (Term d n) (Term d n)
| ClashU EqMode Universe Universe
| ClashQ        Qty      Qty
| NotInScope    Name