| Line No. | Rev | Author | Line |
|---|---|---|---|
| 1 | 7 | paulosilva | |
| 2 | {-# LANGUAGE FlexibleContexts #-} | ||
| 3 | {-# OPTIONS_GHC -Wall #-} | ||
| 4 | |||
| 5 | ------------------------------------------------------------------------------- | ||
| 6 | |||
| 7 | {- | | ||
| 8 | Module : Language.Step.Parser | ||
| 9 | Description : Proof step parser. | ||
| 10 | Copyright : (c) Paulo Silva | ||
| 11 | License : LGPL | ||
| 12 | |||
| 13 | Maintainer : paufil@di.uminho.pt | ||
| 14 | Stability : experimental | ||
| 15 | Portability : portable | ||
| 16 | |||
| 17 | -} | ||
| 18 | |||
| 19 | ------------------------------------------------------------------------------- | ||
| 20 | |||
| 21 | module Language.Step.Parser ( | ||
| 22 | parser, | ||
| 23 | parseStep | ||
| 24 | ) where | ||
| 25 | |||
| 26 | import Control.GalcError | ||
| 27 | import Control.Monad.Error | ||
| 28 | import qualified Language.Combinator.Parser as C | ||
| 29 | import qualified Language.R.Parser as R | ||
| 30 | import Language.Step.Syntax | ||
| 31 | import Text.ParserCombinators.Parsec | ||
| 32 | import Text.ParserCombinators.Parsec.Language | ||
| 33 | import qualified Text.ParserCombinators.Parsec.Token as P | ||
| 34 | |||
| 35 | ------------------------------------------------------------------------------- | ||
| 36 | |||
| 37 | type StepParser = Parser Step | ||
| 38 | |||
| 39 | ------------------------------------------------------------------------------- | ||
| 40 | |||
| 41 | lexer :: P.TokenParser st | ||
| 42 | lexer = P.makeTokenParser $ emptyDef { P.reservedNames = steps } | ||
| 43 | |||
| 44 | ------------------------------------------------------------------------------- | ||
| 45 | |||
| 46 | reserved :: String -> CharParser st () | ||
| 47 | reserved = P.reserved lexer | ||
| 48 | |||
| 49 | whiteSpace :: CharParser st () | ||
| 50 | whiteSpace = P.whiteSpace lexer | ||
| 51 | |||
| 52 | parens :: CharParser st Step -> CharParser st Step | ||
| 53 | parens = P.parens lexer | ||
| 54 | |||
| 55 | ------------------------------------------------------------------------------- | ||
| 56 | |||
| 57 | parser :: MonadError GalcError m => String -> m Step | ||
| 58 | parser = either2error (ParsingError . show) . parse mainStepParser "" | ||
| 59 | |||
| 60 | ------------------------------------------------------------------------------- | ||
| 61 | |||
| 62 | mainStepParser :: StepParser | ||
| 63 | mainStepParser = do | ||
| 64 | whiteSpace | ||
| 65 | t <- parseStep | ||
| 66 | eof | ||
| 67 | return t | ||
| 68 | |||
| 69 | ------------------------------------------------------------------------------- | ||
| 70 | |||
| 71 | parseStep :: StepParser | ||
| 72 | parseStep = | ||
| 73 | parens parseStep <|> | ||
| 74 | parseCombin <|> | ||
| 75 | parseIndirectUp <|> | ||
| 76 | parseIndirectLow <|> | ||
| 77 | parseIndirectEnd <|> | ||
| 78 | parseLeft <|> | ||
| 79 | parseQed <|> | ||
| 80 | parseRight <|> | ||
| 81 | parseSeqc | ||
| 82 | |||
| 83 | ------------------------------------------------------------------------------- | ||
| 84 | |||
| 85 | parseCombin :: StepParser | ||
| 86 | parseCombin = do | ||
| 87 | comb <- C.parseComb | ||
| 88 | return $ Comb comb | ||
| 89 | |||
| 90 | ------------------------------------------------------------------------------- | ||
| 91 | |||
| 92 | parseIndirectUp :: StepParser | ||
| 93 | parseIndirectUp = do | ||
| 94 | try (do reserved "indirect" | ||
| 95 | reserved "up") | ||
| 96 | r <- R.parseR | ||
| 97 | return $ Indirect (Right r) | ||
| 98 | |||
| 99 | ------------------------------------------------------------------------------- | ||
| 100 | |||
| 101 | parseIndirectLow :: StepParser | ||
| 102 | parseIndirectLow = do | ||
| 103 | try (do reserved "indirect" | ||
| 104 | reserved "low") | ||
| 105 | r <- R.parseR | ||
| 106 | return $ Indirect (Left r) | ||
| 107 | |||
| 108 | ------------------------------------------------------------------------------- | ||
| 109 | |||
| 110 | parseIndirectEnd :: StepParser | ||
| 111 | parseIndirectEnd = do | ||
| 112 | try (do reserved "indirect" | ||
| 113 | reserved "end") | ||
| 114 | return IndirectEnd | ||
| 115 | |||
| 116 | ------------------------------------------------------------------------------- | ||
| 117 | |||
| 118 | parseLeft :: StepParser | ||
| 119 | parseLeft = do | ||
| 120 | reserved "left" | ||
| 121 | return LeftP | ||
| 122 | |||
| 123 | ------------------------------------------------------------------------------- | ||
| 124 | |||
| 125 | parseQed :: StepParser | ||
| 126 | parseQed = do | ||
| 127 | reserved "qed" | ||
| 128 | return Qed | ||
| 129 | |||
| 130 | ------------------------------------------------------------------------------- | ||
| 131 | |||
| 132 | parseRight :: StepParser | ||
| 133 | parseRight = do | ||
| 134 | reserved "right" | ||
| 135 | return RightP | ||
| 136 | |||
| 137 | ------------------------------------------------------------------------------- | ||
| 138 | |||
| 139 | parseSeqc :: StepParser | ||
| 140 | parseSeqc = do | ||
| 141 | reserved "seqc" | ||
| 142 | s1 <- parseStep | ||
| 143 | s2 <- parseStep | ||
| 144 | return $ SeqC s1 s2 | ||
| 145 | |||
| 146 | ------------------------------------------------------------------------------- |