Parser.hs

module Parser where

import Text.Parsec
import Math
import Control.Arrow
import Data.Char
import Head

ignore = many thingsToIgnore

thingsToIgnore = theorem <|> moduleInstance <|> extends <|> divisionLine <|> do{oneOf " \n"; return()}

divisionLine = do try $ do {string "--"; many (char '-'); char '\n'; ignore; return()}

variablesDeclaration = do try $ do string "VARIABLE"
                                   optional (char 'S')
                                   ws
                                   vs <- identifier `sepBy` try comma
                                   ignore
                                   return vs

theorem = do try $ do {string "THEOREM"; ws; manyTill anyChar (char '\n'); ignore; return()}
moduleInstance = do try $ do {string "INSTANCE"; ws; identifier; ignore; return()}
extends = do try $ do {string "EXTENDS"; ws; identifier `sepBy` try comma; ignore; return()}

identifier = many1 (oneOf (['a'..'z'] ++ ['A'..'Z'] ++ ['_'] ++ ['0'..'9']))
constant = do try $ do c <- oneOf ['A'..'Z']
                       cs <- many (oneOf (['a'..'z'] ++ ['A'..'Z'] ++ ['_'] ++ ['0'..'9']))
                       return (c:cs)

reserved = ",;.(){}\"/\\[]"
comma = do {ws; char ','; ws; return ()}
infOr = do {ws; string "\\/"; ws; return ()}
infAnd = do {ws; string "/\\"; ws; return ()}

parseTla :: FilePath -> IO (Either String (Module, [Definition]))
parseTla a = do f <- readFile a
                let e = parse specification "Error:" f
                return (left show e)

parseState s = parse action ("Error parsing " ++ s ++ ":") s
parseValue s = parse value ("Error parsing " ++ s ++ ":") s

parseTrace t = fmap resolveReferences (parse trace ("Error parsing " ++ t ++ ":") t)

resolveReferences :: [TraceState] -> [Action]
resolveReferences ts = resolveReferences' ts ts

resolveReferences' :: [TraceState] -> [TraceState] -> [Action]
resolveReferences' _ [] = []
resolveReferences' ts (Act a:ss) = a : resolveReferences' ts ss
resolveReferences' ts (StepRef i:ss) = let a = case ts !! i of
                                             (Act a') -> a'
                                             _ -> error("Reference to reference")
                                       in a: resolveReferences' ts ss

data TraceState = Act Action | StepRef Int

-- trace :: Either ParseError TraceState
trace = do many1 $ traceStep

traceStep = do try $ do string "State "
                        _ <- many digit
                        string ": <"
                        _ <- manyTill anyChar (try (char '>'))
                        ignore
                        a <- action
                        ignore
                        return (Act a)
            <|> do string "Back to state "
                   digits <- many1 digit
                   let n = foldl (\x d -> 10 * x + (digitToInt d)) 0 digits
                   string ": <"
                   _ <- manyTill anyChar (try (char '>'))
                   ignore
                   return (StepRef (n-1))


specification = do (n, d) <- moduleHeader
                   ws
                   ds <- many definition
                   ws
                   many $ char '='
                   ignore
                   many comment
                   eof
                   return (Module n d, ds)

moduleHeader = do many (char '-')
                  string " MODULE "
                  name <- identifier
                  ws
                  divisionLine
                  documentation <- many comment
                  ignore
                  return (name, documentation)

comment = do try $ do string "(*"
             c <- anyChar `manyTill` (do try $ string "*)")
             ignore
             return c
          <|>
          do try $ do string "\\* "
             c <- anyChar `manyTill` char '\n'
             ignore
             return c

declaration = do try $ do string "CONSTANT"
                          optional (char 'S')
                          ws
                          cs <- constant `sepBy` try comma
                          ignore
                          return cs

parameters = identifier `sepBy` comma

call = do try $ do i <- identifier
                   char '('
                   ws
                   ps <- value `sepBy` comma
                   char ')'
                   ignore
                   return (i, ps)
       <|>
       do try $ do i <- identifier
                   ws
                   return (i, [])

defSignature = do try $ do i <- identifier
                           char '('
                           ws
                           ps <- parameters
                           char ')'
                           ignore
                           return (i, ps)
       <|>
       do try $ do i <- identifier
                   ws
                   return (i, [])

definition = do {Comment <$> comment;}
             <|>
             do try $ do {Constants <$> declaration;}
             <|>
             do try $ do {Variables <$> variablesDeclaration;}
             <|>
             do try $ do (i, ps) <- defSignature
                         ws
                         string "=="
                         ws
                         ValueDefinition i ps <$> value
             <|>
             do try $ do (i, ps) <- defSignature
                         string "=="
                         ws
                         doc <- many comment
                         a <- action
                         ignore
                         return (ActionDefinition i ps doc a)

orAction = do string "\\/"
              ws
              a <- action
              ws
              return a

andAction = do string "/\\"
               ws
               a <- action
               ws
               return a

action =  do try $ do string "IF"
                      ws
                      p <- predicate
                      string "THEN"
                      ws
                      at <- action
                      string "ELSE"
                      ws
                      af <- action
                      return (ActionIf p at af)
         <|>
         do {Condition <$> predicate;}
         <|>
         do {p <- primed; char '='; ws; Primed p <$> value;}
         <|>
         do string "UNCHANGED"
            ws
            string "<<"
            vs <- identifier `sepBy` comma
            string ">>"
            ws
            return (Unchanged vs)
         <|>
         do {(i, ps) <- call; return (ActionCall i ps)}
         <|>
         do try $ do {ws; as <- many1 andAction; return (ActionAnd as)}
         <|>
         do try $ do {ws; as <- many1 orAction; return (ActionOr as)}
         <|>
         do try $ do string "\\E"
                     ws
                     i <- identifier
                     ws
                     string "\\in"
                     ws
                     v <- value
                     char ':'
                     ws
                     as <- action `sepBy` infOr
                     return (Exists i v (ActionOr as))
         <|>
         do try $ do string "\\A"
                     ws
                     i <- identifier
                     ws
                     string "\\in"
                     ws
                     v <- value
                     char ':'
                     ws
                     a <- action
                     return (ForAll i v a)


predicate = do try $ do char '('
                        ws
                        ps <- atomPredicate `sepBy` infAnd
                        char ')'
                        ws
                        return (And ps)
           <|>
           do try $ do char '('
                       ws
                       ps <- atomPredicate `sepBy` infOr
                       char ')'
                       ws
                       return (Or ps)
           <|> atomPredicate

atomPredicate = do try $ do v1 <- value
                            char '='
                            ws
                            Equality v1 <$> value
                <|>
                do try $ do v1 <- value
                            char '#'
                            ws
                            Inequality v1 <$> value
                <|>
                do try $ do v1 <- value
                            char '>'
                            ws
                            Gt v1 <$> value
                <|>
                do try $ do v1 <- value
                            char '<'
                            ws
                            Lt v1 <$> value
                <|>
                do try $ do v1 <- value
                            string ">="
                            ws
                            Gte v1 <$> value
                <|>
                do try $ do v1 <- value
                            string "<="
                            ws
                            Lte v1 <$> value
                <|>
                do try $ do v1 <- value
                            string "\\in"
                            ws
                            RecordBelonging v1 <$> value
                <|>
                do try $ do v1 <- value
                            string "\\notin"
                            ws
                            v2 <- value
                            RecordNotBelonging v1 <$> value
                <|>
                do try $ do string "\\A"
                            ws
                            (i, v, p) <- inFilter
                            return (PForAll i v p)

predicateConditionCall = do try $ do i <- identifier
                                     return (ConditionCall i [])

inFilter = do i <- identifier
              ws
              string "\\in"
              ws
              v <- value
              char ':'
              ws
              p <- predicate
              return (i, v, p)

mapping = do try $ do ws
                      i <- identifier
                      ws
                      string "\\in"
                      ws
                      a <- value
                      ws
                      string "|->"
                      ws
                      v <- value
                      ws
                      return (All i a, v)
          <|>
          do ws
             i <- identifier
             ws
             string "|->"
             ws
             v <- value
             ws
             return (Key (Str i), v)

primed = do try $ do i <- identifier
                     char '\''
                     ws
                     return i

value = do try $ do string "Cardinality("
                    ws
                    s <- set
                    char ')'
                    ws
                    return (Cardinality s)
        <|>
        do {l <- lit; return (Lit l)}
        <|>
        do {caseStatement;}
        <|>
        do try $ do {n1 <- Math.number; string ".."; n2 <- Math.number; ws; return (Range n1 n2)}
        <|>
        do {record;}
        <|>
        do try $ do {i <- identifier; char '['; k <- identifier; char ']'; ws; return (Index (Ref i) (Ref k))}
        <|>
        do try $ do {i <- identifier; char '['; k <- literal; char ']'; ws; return (Index (Ref i) k)}
        <|>
        do {set;}
        <|>
        do try $ do {n1 <- Math.number; string ".."; n2 <- Math.number; ws; return (Range n1 n2)}
        <|>
        do try $ do {e <- arithmeticExpression; ws; return (e)}

set = do try $ do {s1 <- atomSet; string "\\cup"; ws; s2 <- set; ws; return (Union s1 s2)}
      <|>
      atomSet

atomSet = do try $ do char '{'
                      ws
                      vs <- value `sepBy` try comma
                      char '}'
                      ws
                      return (Set vs)
          <|>
          do try $ do char '{'
                      (i, v, p) <- inFilter
                      char '}'
                      ws
                      return (Filtered i v p)
          <|>
          do {e <- arithmeticExpression; ws; return (e)}

caseMatch = do try $ do string "OTHER"
                        ws
                        string "->"
                        ws
                        v <- value
                        ws
                        return (DefaultMatch v)
           <|>
           do p <- try $ predicate <|> predicateConditionCall
              ws
              string "->"
              ws
              v <- value
              ws
              return (Match p v)

caseStatement = do try $ do string "CASE"
                            ws
                            cs <- caseMatch `sepBy` try (do {ws; string "[]"; ws})
                            ws
                            return (Case cs)

record = do try $ do char '['
                     ms <- mapping `sepBy` try comma
                     char ']'
                     ws
                     return (Record ms)
        <|>
        do try $ do string "SetAsFun({"
                    ws
                    ts <- tuple `sepBy` try comma
                    ws
                    string "})"
                    ws
                    return (Record (map (\(Tuple [k, v]) -> (Key k, Lit v)) ts))
        <|>
        do try $ do char '('
                    ms <- recEntry `sepBy` try (string "@@ ")
                    char ')'
                    ws
                    return (Record ms)
         <|>
         do char '['
            i <- identifier
            ws
            string "EXCEPT"
            ws
            string "!["
            k <- identifier
            char ']'
            ws
            char '='
            ws
            v <- value
            char ']'
            ws
            return (Except i [(Ref k, v)])

recEntry = do try $ do l <- lit
                       ws
                       string ":>"
                       ws
                       v <- value
                       ws
                       return (Key l, v)

tuple = do try $ do {string "<<"; vs <- lit `sepBy` try comma; string ">>"; ws; return (Tuple vs)}

lit = do try $ do stringLiteral
      <|>
      do try $ do numberLiteral
      <|>
      do try $ do {string "TRUE"; return (Boolean True)}
      <|>
      do try $ do {string "FALSE"; return (Boolean False)}
      <|>
      tuple

stringLiteral =  do try $ do {char '\"'; cs <- many1 (noneOf reserved); char '\"'; ws; return (Str cs)}
literal = do try $ do {s <- stringLiteral; return (Lit s)}

arithmeticExpression = Math.build