


-- 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.DataType
       (
         module Pire.Parser.DataType

       )

       where



import Pire.Syntax.Telescope
import Pire.Syntax.Nm
import Pire.Syntax.Constructor


import Pire.Parser.Parser
import Pire.Parser.Basic
import Pire.Parser.Token
import Pire.Parser.Telescope




#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 Control.Applicative
#endif





-- MonadPlus
-- import Control.Monad
-- import Control.Monad.Error
-- 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)




-- ====================
-- data types





-- eg.
-- Zero
-- Succ of (Nat)
constructorDef :: (DeltaParsing m
                  , LookAheadParsing m
                  , MonadState PiState m
                  ) => m (ConstructorDef T.Text T.Text)
constructorDef = do
  pos <- position
  cname <- ide
  args <- option EmptyTele (reserved "of" >> telescope)


  -- old Unbound impl, using parsec's newPos...
  -- the task of the translation function now...

  -- return $ ConstructorDef (newPos
  --                          ""
  --                          (lineNum pos)
  --                          (columnNum pos)) cname args
  -- <?> "Constructor"


  return $ ConstructorDef pos cname args
  <?> "Constructor"







constructorDef_ :: (DeltaParsing m
                   -- , Fresh m
                   , LookAheadParsing m
                   , MonadState PiState m
                   ) => m (ConstructorDef T.Text T.Text)
constructorDef_ = do
    pos <- position
    (cname, ws) <- id_

    (maybeOf, args') <- option
                        (Nothing, EmptyTele)
                        ((,) <$> (Just <$> of_) <*> telescope_)

    -- hm - need this ?
    -- ws' <- sliced whiteSpace

    return $ ConstructorDef_ pos (Nm1_ cname ws) maybeOf args'
    <?> "Constructor"



-- exmpl: Logic.pi
-- data Void : Type where {}

-- but maybe should be more general even: allow for ws aware versions
-- of openBlock_, closeblock_, indentedBlock_ etc
-- to keep track of the braces (+ws)
-- to allow eg.
-- { constructorDef2 ; constructorDef2 }
-- ie. explicitly in braces, keeping braces + ws

-- noConstructorDef_ :: (DeltaParsing m
--                       -- , Fresh m
--                      , LookAheadParsing m
--                      , MonadState PiState m
--                      ) => m (ConstructorDef_ String)
-- noConstructorDef_ = do
--     bo <- braceOpen_
--     bc <- braceClose_
--     return $ NoConstructorDef_ bo bc
--     <?> "NoConstructor"


