




{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveTraversable #-}

{-# LANGUAGE DataKinds #-}

{-# LANGUAGE CPP #-}

--------------------------------------------------------------------
-- |
-- Copyright :  (c) Andreas Reuleaux 2015
-- License   :  BSD2
-- Maintainer:  Andreas Reuleaux <rx@a-rx.info>
-- Stability :  experimental
-- Portability: non-portable
--
-- This module provides Pire's syntax,
-- ie. Pire's flavour of Pi-forall syntax: telescopes
--------------------------------------------------------------------




module Pire.Syntax.Telescope where




#ifdef MIN_VERSION_GLASGOW_HASKELL
#if MIN_VERSION_GLASGOW_HASKELL(7,10,3,0)
-- ghc >= 7.10.3
#else
-- older ghc versions, but MIN_VERSION_GLASGOW_HASKELL defined
#endif
#else
-- MIN_VERSION_GLASGOW_HASKELL not even defined yet (ghc <= 7.8.x)
import Data.Foldable
import Data.Traversable
import Control.Applicative
#endif



import Pire.Syntax.Token
import Pire.Syntax.Nm
import Pire.Syntax.Expr
import Pire.Syntax.Eps


import Data.Bifoldable
import Data.Bifunctor
import Data.Bitraversable


import Pire.Syntax.Binder


-- -------------
-- -- * Telescopes
-- -------------
-- -- | A telescope is like a first class context. It binds each name
-- -- in the rest of the telescope.  For example
-- --     Delta = x:* , y:x, y = w, empty

data Telescope t a =
  EmptyTele
  | Cons Eps t (Expr t a) (Telescope t a)


  | ConsInParens_    Eps (Token 'ParenOpenTy t)   (Nm1 t) (Token 'ColonTy t) (Expr t a) (Token 'ParenCloseTy t) (Telescope t a)

    -- no colon (and no ws to keep)
    --    | ConsWildInParens_  Eps (Token ParenOpenTy t)  t (Expr t a) (Token ParenCloseTy t) (Telescope t a)
  | ConsWildInParens_  Eps (Token 'ParenOpenTy t) (Binder t) (Expr t a) (Token 'ParenCloseTy t) (Telescope t a)

  | ConsInBrackets_    Eps (Token 'BracketOpenTy t) (Nm1 t) (Token 'ColonTy t) (Expr t a) (Token 'BracketCloseTy t) (Telescope t a)



  | Constraint (Expr t a) (Expr t a) (Telescope t a)


    -- need this as well - cf. equal_
    -- should keep = as well
  | Constraint_ (Token 'BracketOpenTy t) (Expr t a) (Token 'EqualTy t) (Expr t a) (Token 'BracketCloseTy t) (Telescope t a)

  deriving (Eq,Ord,Show,Functor,Foldable,Traversable)





instance Bifunctor Telescope where
  bimap = bimapDefault

instance Bifoldable Telescope where
  bifoldMap = bifoldMapDefault


-- (silence $ runExceptT $ getModules_ ["samples"] "M") >>= return . (\m -> fromRight' $ (ezipper $ Mod m) >>= lineColumn 6 5 >>= focus) . last . fromRight'
-- _decls mm

instance Bitraversable Telescope where
  {-# INLINE bitraverse #-}
  bitraverse f g = bt where

    bt EmptyTele = pure EmptyTele

    bt (Cons eps tt ex tele) = Cons <$> pure eps <*> f tt <*> bitraverseExpr f g ex <*> bt tele


    bt (ConsInParens_ eps po nm colon ex pc tele) =
      ConsInParens_ <$> pure eps <*> traverse f po <*> traverse f nm <*> traverse f colon <*> bitraverseExpr f g ex <*> traverse f pc <*> bt tele

      
    -- bt (ConsWildInParens_ eps po tt ex pc tele) =
    --   ConsWildInParens_ <$> pure eps <*> traverse f po <*> f tt <*> bitraverseExpr f g ex <*> traverse f pc <*> bt tele
      
    bt (ConsWildInParens_ eps po tt ex pc tele) =
      ConsWildInParens_ <$> pure eps <*> traverse f po <*> traverse f tt <*> bitraverseExpr f g ex <*> traverse f pc <*> bt tele



    bt (ConsInBrackets_ eps bo nm colon ex bc tele) =
      ConsInBrackets_ <$> pure eps <*> traverse f bo <*> traverse f nm <*> traverse f colon <*> bitraverseExpr f g ex <*> traverse f bc <*> bt tele
  
    
    bt (Constraint ex ty tele) =
      Constraint <$> bitraverseExpr f g ex <*> bitraverseExpr f g ty <*> bt tele
    

    bt (Constraint_ bo ex eq ty bc tele) =
      Constraint_ <$> traverse f bo <*> bitraverseExpr f g ex <*> traverse f eq <*> bitraverseExpr f g ty <*> traverse f bc <*> bt tele
  


bitraverseTele :: Applicative f => (a -> f c) -> (b -> f d) -> Telescope a b -> f (Telescope c d)
bitraverseTele = bitraverse
