?prevdifflink? - Blame
|
{-# LANGUAGE FlexibleContexts #-} {-# OPTIONS_GHC -Wall #-} ------------------------------------------------------------------------------- {- | Module : Language.Step.Parser Description : Proof step parser. Copyright : (c) Paulo Silva License : LGPL Maintainer : paufil@di.uminho.pt Stability : experimental Portability : portable -} ------------------------------------------------------------------------------- module Language.Step.Parser ( parser, parseStep ) where import Control.GalcError import Control.Monad.Error import qualified Language.Combinator.Parser as C import qualified Language.R.Parser as R import Language.Step.Syntax import Text.ParserCombinators.Parsec import Text.ParserCombinators.Parsec.Language import qualified Text.ParserCombinators.Parsec.Token as P ------------------------------------------------------------------------------- type StepParser = Parser Step ------------------------------------------------------------------------------- lexer :: P.TokenParser st lexer = P.makeTokenParser $ emptyDef { P.reservedNames = steps } ------------------------------------------------------------------------------- reserved :: String -> CharParser st () reserved = P.reserved lexer whiteSpace :: CharParser st () whiteSpace = P.whiteSpace lexer parens :: CharParser st Step -> CharParser st Step parens = P.parens lexer ------------------------------------------------------------------------------- parser :: MonadError GalcError m => String -> m Step parser = either2error (ParsingError . show) . parse mainStepParser "" ------------------------------------------------------------------------------- mainStepParser :: StepParser mainStepParser = do whiteSpace t <- parseStep eof return t ------------------------------------------------------------------------------- parseStep :: StepParser parseStep = parens parseStep <|> parseCombin <|> parseIndirectUp <|> parseIndirectLow <|> parseIndirectEnd <|> parseLeft <|> parseQed <|> parseRight <|> parseSeqc ------------------------------------------------------------------------------- parseCombin :: StepParser parseCombin = do comb <- C.parseComb return $ Comb comb ------------------------------------------------------------------------------- parseIndirectUp :: StepParser parseIndirectUp = do try (do reserved "indirect" reserved "up") r <- R.parseR return $ Indirect (Right r) ------------------------------------------------------------------------------- parseIndirectLow :: StepParser parseIndirectLow = do try (do reserved "indirect" reserved "low") r <- R.parseR return $ Indirect (Left r) ------------------------------------------------------------------------------- parseIndirectEnd :: StepParser parseIndirectEnd = do try (do reserved "indirect" reserved "end") return IndirectEnd ------------------------------------------------------------------------------- parseLeft :: StepParser parseLeft = do reserved "left" return LeftP ------------------------------------------------------------------------------- parseQed :: StepParser parseQed = do reserved "qed" return Qed ------------------------------------------------------------------------------- parseRight :: StepParser parseRight = do reserved "right" return RightP ------------------------------------------------------------------------------- parseSeqc :: StepParser parseSeqc = do reserved "seqc" s1 <- parseStep s2 <- parseStep return $ SeqC s1 s2 ------------------------------------------------------------------------------- |