calculus/Calculus/Lambda/Omega/Explicit/Read.hs

   1 {-# LANGUAGE FlexibleContexts #-}
   2 {-# LANGUAGE NoImplicitPrelude #-}
   3 {-# LANGUAGE OverloadedStrings #-}
   4 {-# LANGUAGE Rank2Types #-}
   5 {-# LANGUAGE TupleSections #-}
   6 {-# OPTIONS_GHC -fno-warn-tabs #-}
   7 module Calculus.Lambda.Omega.Explicit.Read where
   8
   9 import Control.Applicative (Alternative(..), Applicative(..), (<$>), (<$))
  10 import qualified Control.Applicative as Applicative
  11 import Control.Monad
  12 import Data.Bool
  13 import Data.Char (Char)
  14 import qualified Data.Char as Char
  15 import Data.Either (Either(..))
  16 import Data.Eq (Eq(..))
  17 import Data.Foldable (Foldable(..))
  18 import Data.Function (($), (.), flip)
  19 import qualified Data.List as List
  20 import Data.Maybe (Maybe(..))
  21 import Data.Maybe (catMaybes)
  22 import Data.Text (Text)
  23 import Data.String (String)
  24 import qualified Data.Text as Text
  25 import Text.Parsec ((<?>))
  26 import qualified Text.Parsec as R
  27 import Text.Show (Show(..))
  28
  29 -- import Debug.Trace
  30
  31 import Calculus.Abstraction.DeBruijn.Generalized
  32 import Calculus.Lambda.Omega.Explicit
  33
  34 -- * Type 'Lexer'
  35 type Lexer s m a
  36  =  R.Stream  s m Char
  37  => R.ParsecT s Lexer_State m a
  38 type Lexer_State = ()
  39
  40 -- ** Type 'Token'
  41 -- | A lexed token.
  42 data Token
  43  =   Token_Arrow
  44  |   Token_Type_0
  45  |   Token_Equal
  46  |   Token_Colon
  47  |   Token_Lambda
  48  |   Token_Name Text
  49  |   Token_Paren_Close
  50  |   Token_Paren_Open
  51  |   Token_Pi
  52  deriving (Eq, Show)
  53
  54 -- | A lexed token with location information attached
  55 data Lexed_Token
  56  =   Lexed_Token Token R.SourcePos
  57  deriving (Show)
  58
  59 -- | Remove location information from a 'Lexed_Token'
  60 lexed_token :: Lexed_Token -> Token
  61 lexed_token (Lexed_Token tok _) = tok
  62
  63 lex
  64  :: R.Stream s m Char
  65  => Lexer s m a
  66  -> s -> m (Either R.ParseError a)
  67 lex l = R.runParserT l () ""
  68
  69 lex_all :: Lexer s m [Lexed_Token]
  70 lex_all =
  71         catMaybes
  72          <$> R.many lex_token_or_whitespace
  73          <*  R.eof
  74
  75 -- | Lex either one token or some whitespace
  76 lex_token_or_whitespace :: Lexer s m (Maybe Lexed_Token)
  77 lex_token_or_whitespace =
  78         (<|>)
  79          (Nothing <$  R.try lex_whitespace)
  80          (Just    <$> lex_token)
  81
  82 lex_whitespace :: Lexer s m ()
  83 lex_whitespace =
  84         R.choice
  85          [ () <$ Applicative.some R.space
  86          , lex_comment_block
  87          , lex_comment_line
  88          ]
  89
  90 -- | Lex a @{- ... -}@ comment (perhaps nested).
  91 lex_comment_block :: Lexer s m ()
  92 lex_comment_block = R.try (R.string "{-") *> lex_comment_body
  93
  94 -- | Lex a block comment, without the opening.
  95 lex_comment_body :: Lexer s m ()
  96 lex_comment_body =
  97         R.choice
  98          [ lex_comment_block     *> lex_comment_body
  99          , R.try (R.string "-}") *> return ()
 100          , R.anyChar             *> lex_comment_body
 101          ]
 102
 103 lex_comment_line :: Lexer s m ()
 104 lex_comment_line =
 105   R.try (R.string "--")
 106   *> R.manyTill R.anyChar (R.eof <|> (() <$ R.newline))
 107   *> return ()
 108
 109 lex_token :: Lexer s m Lexed_Token
 110 lex_token =
 111         Lexed_Token
 112          <$> R.choice
 113           [ lex_symbol
 114           , lex_word
 115           -- , Token_Int . fromInteger <$> R.natural R.haskell
 116           ]
 117          <*> R.getPosition
 118
 119 -- | Lex one non-alphanumeric token
 120 lex_symbol :: Lexer s m Token
 121 lex_symbol = R.choice
 122   [ Token_Arrow       <$  (R.try (R.string "->") <|> R.string "→")
 123   , Token_Colon       <$  R.char ':'
 124   , Token_Equal       <$  R.char '='
 125   , Token_Lambda      <$  (R.char '\\' <|> R.char 'λ')
 126   , Token_Type_0      <$  R.char '*'
 127   , Token_Paren_Close <$  R.char ')'
 128   , Token_Paren_Open  <$  R.char '('
 129   , Token_Pi          <$  (R.string "\\/" <|> R.string "Π" <|> R.string "∀")
 130   ]
 131
 132 lex_word :: Lexer s m Token
 133 lex_word = tokenify <$> lex_name
 134         where
 135         tokenify name = Token_Name (Text.pack name)
 136
 137 lex_name :: Lexer s m String
 138 lex_name = (:)
 139          <$> (R.letter <|> R.char '_')
 140          <*> (R.many (R.alphaNum <|> R.char '_'))
 141
 142 -- * Type 'Parser'
 143 type Parser m a
 144  =  R.Stream  [Lexed_Token] m Lexed_Token
 145  => R.ParsecT [Lexed_Token] Parser_State m a
 146 type Parser_State = ()
 147
 148 read
 149  :: (R.Stream s m Char, Monad m)
 150  => Parser m a -> s -> m (Either R.ParseError a)
 151 read p s = do
 152         toks <- lex lex_all s
 153         case toks of
 154          Left err -> return $ Left err
 155          Right ts -> parse p ts
 156
 157 parse
 158  :: R.Stream [Lexed_Token] m Lexed_Token
 159  => Parser m a
 160  -> [Lexed_Token]
 161  -> m (Either R.ParseError a)
 162 parse p = R.runParserT (p <* R.eof) () ""
 163
 164 -- | Like 'R.updatePosChar' but working on 'Lexed_Token'.
 165 updatePosToken
 166  :: R.SourcePos   -- ^ position of the current token
 167  -> Lexed_Token   -- ^ current token
 168  -> [Lexed_Token] -- ^ remaining tokens
 169  -> R.SourcePos   -- ^ position of the next token
 170 updatePosToken pos _ [] = pos
 171 updatePosToken _   _ (Lexed_Token _ pos : _) = pos
 172
 173 -- | Parse a nullary token.
 174 parse_token
 175  :: Token -> Parser m ()
 176 parse_token t =
 177         R.tokenPrim
 178          show updatePosToken
 179          (guard . (t ==) . lexed_token)
 180
 181 -- | Parse an unary token.
 182 parse_token_1
 183  :: (Token -> Maybe a)
 184  -> Parser m a
 185 parse_token_1 untoken =
 186         R.tokenPrim
 187          show updatePosToken
 188          (untoken . lexed_token)
 189
 190 -- | 'parse_term' @::=@ 'parse_term_abst' @|@ 'parse_type_abst'
 191 parse_term :: Parser m (Term Var_Name)
 192 parse_term =
 193         R.try parse_term_abst
 194          <|> parse_type_abst
 195          <?> "term"
 196
 197 parse_sort :: Parser m (Type Var_Name)
 198 parse_sort =
 199         Type_Sort . (Type_Level_0,)
 200          <$  parse_token Token_Type_0
 201          <*> R.option Type_Morphism_Mono
 202                  (parse_token_1 $ \tok -> case tok of
 203                          Token_Name "m" -> Just Type_Morphism_Mono
 204                          Token_Name "p" -> Just Type_Morphism_Poly
 205                          _              -> Nothing)
 206          <?> "sort"
 207
 208 parse_var_name :: Parser m Var_Name
 209 parse_var_name =
 210         parse_token_1 (\tok ->
 211                 case tok of
 212                  Token_Name "_" -> Nothing
 213                  Token_Name n   -> Just n
 214                  _              -> Nothing)
 215          <?> "variable-name"
 216
 217 parse_var_def :: Parser m Var_Name
 218 parse_var_def =
 219         parse_token_1 (\tok ->
 220                 case tok of
 221                  Token_Name "_" -> Just ""
 222                  Token_Name n   -> Just n
 223                  _              -> Nothing)
 224          <?> "variable-definition"
 225
 226 parse_var :: Parser m (Term Var_Name)
 227 parse_var =
 228         TeTy_Var
 229          <$> parse_var_name
 230          <?> "variable"
 231
 232 -- | 'parse_app' @::=@ 'parse_atom'@+@
 233 parse_app :: Parser m (Term Var_Name)
 234 parse_app =
 235         List.foldl1 TeTy_App
 236          <$> R.many1 (R.try parse_atom)
 237          <?> "application"
 238
 239 -- | 'parse_atom' @::=@ 'parse_sort' @|@ 'parse_var' @|@ @"("@ 'parse_term @")"@
 240 parse_atom :: Parser m (Term Var_Name)
 241 parse_atom =
 242         R.try parse_sort
 243          <|> R.try parse_var
 244          <|> R.between
 245                  (parse_token Token_Paren_Open)
 246                  (parse_token Token_Paren_Close)
 247                  parse_term
 248          <?> "atom"
 249
 250 -- | 'parse_term_abst' @::=@ @"\"@ 'parse_term_abst_decl'@+@ @"->"@ 'parse_term'
 251 parse_term_abst :: Parser m (Term Var_Name)
 252 parse_term_abst =
 253         (flip $ foldr (\(x, f_in) t ->
 254                 Term_Abst (Suggest x) f_in ((x =?) `abstract` t)))
 255          <$  parse_token Token_Lambda
 256          <*> R.many1 parse_term_abst_decl
 257          <*  parse_token Token_Arrow
 258          <*> parse_term
 259          <?> "term_abst"
 260
 261 -- | 'parse_term_abst_decl' @::=@ @"("@ 'parse_var_def' @":"@ 'parse_type' @")"@
 262 parse_term_abst_decl :: Parser m (Var_Name, Type Var_Name)
 263 parse_term_abst_decl =
 264         (,)
 265          <$  parse_token Token_Paren_Open
 266          <*> parse_var_def
 267          <*  parse_token Token_Colon
 268          <*> parse_type
 269          <*  parse_token Token_Paren_Close
 270          <?> "term_abst_decl"
 271
 272 -- | 'parse_type_abst_decl' @::=@ @"("@ @(@ 'parse_var_def' @":"@ @)?@ 'parse_type' @")"@
 273 parse_type_abst_decl :: Parser m (Var_Name, Type Var_Name)
 274 parse_type_abst_decl =
 275         (,)
 276          <$  parse_token Token_Paren_Open
 277          <*> R.option "" (R.try parse_var_def <* parse_token Token_Colon)
 278          <*> parse_type
 279          <*  parse_token Token_Paren_Close
 280          <?> "type_abst_decl"
 281
 282 -- | 'parse_type_abst' @::=@ @(@ 'parse_app' @|@ 'parse_type_abst_decl' @)@ @"->"@ 'parse_type_abst' @|@ 'parse_app'
 283 parse_type_abst :: Parser m (Term Var_Name)
 284 parse_type_abst =
 285         (R.try
 286                 ((\(x, f_in) f_out ->
 287                         Type_Abst (Suggest x) f_in ((x =?) `abstract` f_out))
 288                  <$> (
 289                          (R.try (("",) <$> parse_app))
 290                         <|>
 291                          (R.option () (parse_token Token_Pi)
 292                                  *> parse_type_abst_decl)
 293                  )
 294                  <*  parse_token Token_Arrow
 295                  <*> parse_type_abst))
 296          <|> parse_app
 297          <?> "type_abst"
 298
 299 -- | 'parse_type' @::=@ 'parse_term'
 300 parse_type :: Parser m (Term Var_Name)
 301 parse_type =
 302         parse_term <?> "type"
 303
 304 parse_let_or_term :: Parser m (Either (Var_Name, Maybe (Type Var_Name), Term Var_Name) (Term Var_Name))
 305 parse_let_or_term =
 306         R.option
 307          Right
 308          (R.try ((\name args maybe_ty te ->
 309                 Left
 310                  ( name
 311                  , (\ty -> foldr (\(x, x_ty) t ->
 312                         Type_Abst (Suggest x) x_ty ((x =?) `abstract` t)) ty args
 313                          ) <$> maybe_ty
 314                         , foldr (\(x, x_ty) t ->
 315                                 Term_Abst (Suggest x) x_ty ((x =?) `abstract` t)) te args
 316                  )
 317                 )<$> parse_var_name
 318                  <*> R.many parse_term_abst_decl
 319                  <*> (<|>)
 320                          (R.try (Just
 321                                  <$  parse_token Token_Colon
 322                                  <*> parse_type))
 323                          (pure Nothing)
 324                  <* parse_token Token_Equal
 325          ))
 326          <*> parse_term
 327
 328 -- | 'parse_let' @::=@ 'parse_var_name' @(@'parse_term_abst_decl'@)*@ @"="@ 'parse_term'
 329 parse_let :: Parser m (Var_Name, Maybe (Type Var_Name), Term Var_Name)
 330 parse_let =
 331         (\name args maybe_ty te ->
 332                 ( name
 333                 , (\ty -> foldr (\(x, x_ty) t ->
 334                         Type_Abst (Suggest x) x_ty ((x =?) `abstract` t)) ty args
 335                  ) <$> maybe_ty
 336                 , foldr (\(x, x_ty) t ->
 337                         Term_Abst (Suggest x) x_ty ((x =?) `abstract` t)) te args
 338                 )
 339         )<$> parse_var_name
 340          <*> R.many parse_term_abst_decl
 341          <*> (<|>)
 342                  (R.try (Just
 343                          <$  parse_token Token_Colon
 344                          <*> parse_type))
 345                  (pure Nothing)
 346          <*  parse_token Token_Equal
 347          <*> parse_term
 348          <?> "let"
 349
 350 -- | 'parse_assume' @::=@ 'parse_var_name' @":"@ 'parse_type'
 351 parse_assume :: Parser m (Var_Name, Type Var_Name)
 352 parse_assume =
 353         (,)
 354          <$> parse_var_name
 355          <*  parse_token Token_Colon
 356          <*> parse_type
 357          <?> "axiom"
 358
 359 parse_command
 360  :: R.Stream  s m Char
 361  => R.ParsecT s () m (String, String)
 362 parse_command =
 363         (,)
 364          <$> (R.option "" (R.try (
 365                         R.char ':'
 366                          *> R.many (R.satisfy Char.isLetter <|> R.char '_')
 367                          <* (R.option () $ void $ R.many (void $ R.char ' '))
 368                          )))
 369          <*> R.many (R.try (
 370                 (<|>)
 371                          (R.try R.newline <* R.lookAhead (R.char ' ' <|> R.char '\t'))
 372                          (R.satisfy is_horizontal)
 373          ))
 374         where
 375                 is_horizontal c = case c of {'\n' -> False; '\r' -> False; _ -> True}
 376
 377 parse_commands
 378  :: R.Stream  s m Char
 379  => R.ParsecT s () m [(String, String)]
 380 parse_commands =
 381         R.many $ do
 382                 _ <- R.many $ do
 383                         _ <- R.many (R.satisfy is_horizontal_space)
 384                         R.newline
 385                 (c, s) <- parse_command
 386                 _ <- R.many1 $ do
 387                         _ <- R.try (R.many (R.satisfy is_horizontal_space))
 388                         R.newline
 389                 return (c,s)
 390         where
 391         is_horizontal_space c = case c of {' ' -> True; '\t' -> True; _ -> False}
 392