module CC.Term.Raw

import CC.Name
import CC.Term

import Data.DPair
import Data.List1

import Text.Bounded

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

public export
data RawTerm : Type

public export
record RawBinding where
  constructor Of
  name : Maybe Name
  bound : RawTerm

data RawTerm where
  Bounded : WithBounds RawTerm -> RawTerm

  Var : (n : Name) -> RawTerm

  Let : Name -> Maybe RawTerm -> RawTerm -> RawTerm -> RawTerm

  Set : RawTerm

  Pi : RawBinding -> RawTerm -> RawTerm
  Abs : (n : Maybe Name) -> RawTerm -> RawTerm
  App : RawTerm -> RawTerm -> RawTerm

%name RawBinding bind
%name RawTerm t, u

-- Error Type ------------------------------------------------------------------

export
data NameError : Type -> Type where
  Ok : ty -> NameError ty
  Err : List1 Name -> NameError ty

export
Functor NameError where
  map f (Ok v) = Ok (f v)
  map f (Err errs) = Err errs

export
Applicative NameError where
  pure = Ok

  Ok f <*> Ok v = Ok (f v)
  Ok f <*> Err ys = Err ys
  Err xs <*> Ok v = Err xs
  Err xs <*> Err ys = Err (xs ++ ys)

export
runNameError : NameError ty -> Either (List1 Name) ty
runNameError (Ok x) = Right x
runNameError (Err xs) = Left xs

-- Translation -----------------------------------------------------------------

export
lookup : (ctx : Context) -> (n : Name) -> NameError $ Subset Nat (\k => IsVar k n ctx)
lookup [<] n = Err (n ::: [])
lookup (ctx :< m) n =
  case decEquiv n m of
    Yes eq => Ok (Element 0 (Here eq))
    No _ => map (\p => Element (S p.fst) (There p.snd)) (lookup ctx n)