Ty.hs

{-# LANGUAGE TypeFamilies, FlexibleContexts #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE OverloadedStrings, RecordWildCards, TupleSections #-}

module Toy.Language.Parser.Ty
( ty
, baseRT
) where

import Control.Monad
import Data.List.Extra
import Data.String
import Text.Megaparsec
import Text.Megaparsec.Char.Lexer

import Toy.Language.Syntax
import Toy.Language.Syntax.Terms.Sugar
import Toy.Language.Parser.Common
import Toy.Language.Parser.Util

ty :: ToyMonad e s m => m Ty
ty = TyArrow <$> try arrow
 <|> arrowLHS

arrowLHS :: ToyMonad e s m => m Ty
arrowLHS = parens ty <|> TyBase <$> baseRT

arrow :: ToyMonad e s m => m ArrowTy
arrow = do
  (piVarName, domTy) <- boundLHS <|> unboundLHS
  void $ lstring "->"
  codTy <- ty
  pure $ ArrowTy { .. }
  where
    unboundLHS = (Nothing,) <$> arrowLHS
    boundLHS = try $ parens $ do
      piVarName <- Just <$> varName <* lstring ":"
      domTy <- ty
      pure (piVarName, domTy)

baseRT :: ToyMonad e s m => m RefinedBaseTy
baseRT = try refinedTy <|> implicitTrue
  where
    implicitTrue = RefinedBaseTy <$> baseTy <*> pure trueRefinement
    refinedTy = do
      void $ lstring "{"
      void $ lstring "v"
      void $ lstring ":"
      baseType <- baseTy
      void $ lstring "|"
      baseTyRefinement <- Just <$> refinement
      void $ lstring "}"
      pure $ RefinedBaseTy { .. }

-- TODO support custom refinement vars
refinement :: ToyMonad e s m => m Refinement
refinement = Refinement "v" <$> atomicRefinement `sepBy1` lstring "&"

atomicRefinement :: ToyMonad e s m => m AtomicRefinement
atomicRefinement = do
  void $ lstring "v"
  (\op arg -> AR $ TBinOp () v op arg) <$> parseTable ops <*> args
  where
    ops = [ ("<=", BinOpLeq), ("<", BinOpLt), ("=", BinOpEq), ("/=", BinOpNEq), (">=", BinOpGeq), (">", BinOpGt) ]
    args = choice [ TInteger () <$> lexeme' decimal
                  , lstringSpace "len" >> TApp () "len" . TName ()  <$> varName
                  , TName () <$> varName
                  ]

baseTy :: ToyMonad e s m => m BaseTy
baseTy = parseTable [ (fromString str, bty)
                    | bty <- enumerate
                    , let str = tail $ show bty
                    ]