


-- for TokParsing, MonadicParsing
{-# LANGUAGE ConstraintKinds #-}


{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE CPP #-}







-- {-# OPTIONS_GHC -Wall #-}
-- {-# OPTIONS_GHC -fno-warn-unused-matches #-}
-- {-# OPTIONS_GHC -fno-warn-orphans #-}



-- {-# OPTIONS_GHC -fno-warn-missing-signatures #-}
-- {-# OPTIONS_GHC -fno-warn-unused-do-bind #-}

-- {-# OPTIONS_GHC -fno-warn-incomplete-patterns #-}
-- {-# OPTIONS_GHC -fno-warn-incomplete-uni-patterns #-}




--------------------------------------------------------------------
-- |
-- Copyright :  (c) Andreas Reuleaux 2015
-- License   :  BSD2
-- Maintainer:  Andreas Reuleaux <rx@a-rx.info>
-- Stability :  experimental
-- Portability: non-portable
--
-- This module is part of Pire's parser.
--------------------------------------------------------------------



module Pire.Parser.Telescope
       (
         module Pire.Parser.Telescope

       )

       where



import Pire.Syntax.Telescope
import Pire.Syntax.Nm
import Pire.Syntax.Eps
-- import Pire.Syntax.Token
-- import Pire.Syntax.Constructor
-- import Pire.Syntax.Decl
-- import Pire.Syntax.Modules
-- import Pire.Syntax.ConstructorNames
import Pire.Syntax.Wildcard
import Pire.Syntax.Expr

-- import Pire.Syntax.MkVisible
import Pire.Syntax.Binder


-- import Pire.Utils

import Pire.Parser.Parser
import Pire.Parser.Basic
import Pire.Parser.Token
import Pire.Parser.VarWildcard
import Pire.Parser.Expr
-- import Pire.Parser.Layout






import Control.Applicative

-- MonadPlus



-- import Control.Monad.Error
#ifdef MIN_VERSION_GLASGOW_HASKELL
#if MIN_VERSION_GLASGOW_HASKELL(7,10,3,0)
-- ghc >= 7.10.3
-- import Control.Monad.Except
#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 Control.Monad.Error
-- import Control.Monad
#endif



-- import Control.Monad.State
import Control.Monad.State.Strict


import Text.Parser.LookAhead


-- import Text.PrettyPrint (Doc)
-- import Text.PrettyPrint.HughesPJ (Doc)
-- import Text.PrettyPrint.ANSI.Leijen (Doc)




-- import qualified Data.Set as S



-- import qualified Data.Text as T (Text, pack)
import qualified Data.Text as T (Text)




-- examples, cf tests dir, lecture 4(?):
--  (m1:Nat)(m2:Nat)(Beautiful m1)(Beautiful m2)[n = plus m1 m2]
-- handled below as annot, (imp,) equal


telescope :: (TokenParsing m
             -- , Fresh m
             , LookAheadParsing m
             , DeltaParsing m
             , MonadState PiState m
             ) => m (Telescope T.Text T.Text)
telescope = do
  bindings <- telebindings
  return $ foldr id EmptyTele bindings where







telescope_ :: (TokenParsing m
              , LookAheadParsing m
              , DeltaParsing m
              , MonadState PiState m
              ) => m (Telescope T.Text T.Text)

-- -- for starters...
-- telescope_ = return EmptyTele


telescope_ = do
  -- bindings <- telebindings'
  -- let bindings' = [b | (o, b, c) <- bindings]
  -- return $ foldr id Empty' bindings' where
  bindings <- telebindings_
  -- let bindings' = [b | (o, b, c) <- bindings]
  return $ foldr id EmptyTele bindings where








telebindings :: (TokenParsing m
                , LookAheadParsing m
                , DeltaParsing m
                , MonadState PiState m)
                => m [Telescope T.Text T.Text -> Telescope T.Text T.Text]
telebindings = many teleBinding
  where
    annot = do

      (x,ty) <-    try ((,) <$> varOrWildcard      <*> (colon >> expr))
                <|>    ((,) <$> fresh wildcardName <*> expr)
      return (Cons RuntimeP x ty)



    imp = do
        v <- varOrWildcard
        _ <- colon
        t <- expr
        return (Cons ErasedP v t)

    equal = do
        v <- ide
        reservedOp "="
        t <- expr
        return (Constraint (V v) t)

    teleBinding =
      (    parens annot
       <|> try (brackets imp)
       <|> brackets equal) <?> "binding"



-- "  (m1{-m-}:{-d-}Nat{-N-})"


annot_ :: (TokenParsing m
          -- , Fresh m
          , LookAheadParsing m
          , DeltaParsing m
          , MonadState PiState m
          )=> m (Telescope T.Text T.Text -> Telescope T.Text T.Text)
annot_ = do

  -- ( x : T )
  -- ( _ : T )
  try (do
          po <- parenOpen_
          -- v <- varOrWildcard_
          (v, ws) <- varOrWildcard2_
          cln <- colon_
          ty <- expr_
          pc <- parenClose_
          return $ ConsInParens_ RuntimeP po (Nm1_ v ws) cln ty pc
      )
    <|>

    -- ( T ) -> ( _ [:] T )
    -- (Beautiful m2)
    (do
          po <- parenOpen_

          -- v <- fresh wildcardName
          i <- freshIdx
          -- let v = mkVisible wildcardName i
               

          -- PiP_ RuntimeP (Ann_ $ InferredAnnBnd_ (InvisibleBinder i) tyA) arr $ abstract1 nm $ tyB


          ty <- expr_
          pc <- parenClose_
          -- no colon, thus SimpleConsInParens_
          -- return $ ConsWildInParens_ RuntimeP po v ty pc
          return $ ConsWildInParens_ RuntimeP po (InvisibleBinder i)  ty pc
          
    )




-- "  [m1{-m-}:{-d-}Nat{-N-}]"


imp_ :: (TokenParsing m
        -- , Fresh m
        , LookAheadParsing m
        , DeltaParsing m
        , MonadState PiState m
        )=> m (Telescope T.Text T.Text -> Telescope T.Text T.Text)
imp_ = do
        bo <- bracketOpen_
        -- v <- varOrWildcard_
        (v, ws) <- varOrWildcard2_
        c <- colon_
        ty <- expr_
        bc <- bracketClose_
        return $ ConsInBrackets_ ErasedP bo (Nm1_ v ws) c ty bc




-- [n = plus m1 m2]
equal_ :: (TokenParsing m
        -- , Fresh m
          , LookAheadParsing m
        , DeltaParsing m
        , MonadState PiState m
        ) => m (Telescope T.Text T.Text -> Telescope T.Text T.Text)
equal_ = do
        bo <- bracketOpen_
        v <- var_
        e <- eq_
        t <- expr_
        bc <- bracketClose_
        return $ Constraint_ bo v e t bc






teleBinding_ :: (TokenParsing m
                -- , Fresh m
                , LookAheadParsing m
                , DeltaParsing m
                , MonadState PiState m
                ) => m (Telescope T.Text T.Text -> Telescope T.Text T.Text)
teleBinding_ =
  annot_
  <|> try imp_
  <|> equal_ <?> "binding"






telebindings_ :: (TokenParsing m
                 -- , Fresh m
                 , LookAheadParsing m
                 , DeltaParsing m
                 , MonadState PiState m)
                 => m [Telescope T.Text T.Text -> Telescope T.Text T.Text]
telebindings_ = many teleBinding_




