


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

-- for impOrExpVar
{-# LANGUAGE TupleSections #-}


{-# LANGUAGE FlexibleContexts #-}


{-# LANGUAGE OverloadedStrings #-}





-- ghc opts / calm down ghc-mod


-- {-# 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.Nat where


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


import Pire.Syntax.Ex
import Pire.Syntax.Ws
import Pire.Syntax.Expr

import qualified Data.Text as T (pack)

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




-- originally desugaring of nats in the parser...

-- commented out in PIRE!!!
{-
  natenc :: TokParsing m => m  Tm
  natenc =
    do n <- natural
       return $ encode n
     where encode 0 = DCon "Zero" [] natty
           encode n = DCon "Succ" [Arg RuntimeP (encode (n-1))] natty
           natty    = Annot $ Just (TCon "Nat" [])
 -}



-- commented out in PIRE!!!
-- think about where to put the ws:
-- as part of the DCName' or of the Annot' ?
-- for now on the (top most) DCName'
{-
  natenc_ :: (TokParsing m
             , DeltaParsing m
             ) => m  Tm_
  natenc_ = do
    n <- runUnspaced natural
    ws <- sliced whiteSpace
    -- return $ (\(DCon_ n'  args (Annot_ m _)) ->
    --             DCon_ n'  args (Annot_ m $ Ws $ txt ws )) $ encode n
    return $ (\(DCon_ (DCName_ n' _)  args annot) ->
                DCon_ (DCName_ n' $ Ws $ txt ws)  args annot) $ encode n
      where
        -- encode 0 = DCon_ "Zero" [] natty
        encode 0 = DCon_ (DCName_ "Zero" $ Ws "") [] natty
        -- encode n = DCon_ "Succ" [Arg_ Runtime (encode (n-1))] natty
        encode n = DCon_ (DCName_ "Succ" $ Ws "")
                   [Arg_ RuntimeP (encode (n-1))] natty
        natty    = Annot_ (Just (TCon_ (TCName_ "Nat" $ Ws "") [])) $ Ws ""
 -}






-- ... but don't want implicit desugaring while parsing
nat :: TokParsing m => m Ex
nat =
  do n <- natural
     return $ Nat n





nat_ :: (TokenParsing m
         , Monad m
         , DeltaParsing m
         , MonadState PiState m
         )
        => m Ex
nat_ = do
  n <- runUnspaced natural
  ws <- sliced whiteSpace
  return $ Nat_ n (T.pack $ show n) (Ws $ txt ws)




