liquid-fixpoint-8.10.7: src/Language/Fixpoint/Parse.hs
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE OverloadedStrings #-}
module Language.Fixpoint.Parse (
-- * Top Level Class for Parseable Values
Inputable (..)
-- * Top Level Class for Parseable Values
, Parser
-- * Some Important keyword and parsers
, reserved, reservedOp
, locReserved
, parens , brackets, angles, braces
, semi , comma
, colon , dcolon
, dot
, pairP
, stringLiteral
, locStringLiteral
-- * Parsing basic entities
-- fTyConP -- Type constructors
, lowerIdP -- Lower-case identifiers
, upperIdP -- Upper-case identifiers
-- , infixIdP -- String Haskell infix Id
, symbolP -- Arbitrary Symbols
, locSymbolP
, constantP -- (Integer) Constants
, natural -- Non-negative integer
, locNatural
, bindP -- Binder (lowerIdP <* colon)
, sortP -- Sort
, mkQual -- constructing qualifiers
, infixSymbolP -- parse infix symbols
, locInfixSymbolP
-- * Parsing recursive entities
, exprP -- Expressions
, predP -- Refinement Predicates
, funAppP -- Function Applications
, qualifierP -- Qualifiers
, refaP -- Refa
, refP -- (Sorted) Refinements
, refDefP -- (Sorted) Refinements with default binder
, refBindP -- (Sorted) Refinements with configurable sub-parsers
, bvSortP -- Bit-Vector Sort
, defineP -- function definition equations (PLE)
, matchP -- measure definition equations (PLE)
-- * Layout
, indentedBlock
, indentedLine
, indentedOrExplicitBlock
, explicitBlock
, explicitCommaBlock
, block
, spaces
, setLayout
, popLayout
-- * Raw identifiers
, condIdR
-- * Lexemes and lexemes with location
, lexeme
, located
, locLexeme
, locLowerIdP
, locUpperIdP
-- * Getting a Fresh Integer while parsing
, freshIntP
-- * Parsing Function
, doParse'
, parseTest'
, parseFromFile
, parseFromStdIn
, remainderP
-- * Utilities
, isSmall
, isNotReserved
, initPState, PState (..)
, LayoutStack(..)
, Fixity(..), Assoc(..), addOperatorP
-- * For testing
, expr0P
, dataFieldP
, dataCtorP
, dataDeclP
) where
import Control.Monad.Combinators.Expr
import qualified Data.IntMap.Strict as IM
import qualified Data.HashMap.Strict as M
import qualified Data.HashSet as S
import Data.List (foldl')
import Data.List.NonEmpty (NonEmpty(..))
import qualified Data.Text as T
import qualified Data.Text.IO as T
import Data.Maybe (fromJust, fromMaybe)
import Data.Void
import Text.Megaparsec hiding (State, ParseError)
import Text.Megaparsec.Char
import qualified Text.Megaparsec.Char.Lexer as L
import GHC.Generics (Generic)
import qualified Data.Char as Char
import Language.Fixpoint.Smt.Bitvector
import Language.Fixpoint.Types.Errors
import qualified Language.Fixpoint.Misc as Misc
import Language.Fixpoint.Smt.Types
import Language.Fixpoint.Types hiding (mapSort)
import Text.PrettyPrint.HughesPJ (text, vcat, (<+>), Doc)
import Control.Monad.State
-- import Debug.Trace
-- Note [Parser monad]
--
-- For reference,
--
-- in *parsec*, the base monad transformer is
--
-- ParsecT s u m a
--
-- where
--
-- s is the input stream type
-- u is the user state type
-- m is the underlying monad
-- a is the return type
--
-- whereas in *megaparsec*, the base monad transformer is
--
-- ParsecT e s m a
--
-- where
--
-- e is the custom data component for errors
-- s is the input stream type
-- m is the underlying monad
-- a is the return type
--
-- The Liquid Haskell parser tracks state in 'PState', primarily
-- for operator fixities.
--
-- The old Liquid Haskell parser did not use parsec's "user state"
-- functionality for 'PState', but instead wrapped a state monad
-- in a parsec monad. We do the same thing for megaparsec.
--
-- However, user state was still used for an additional 'Integer'
-- as a unique supply. We incorporate this in the 'PState'.
--
-- Furthermore, we have to decide whether the state in the parser
-- should be "backtracking" or not. "Backtracking" state resets when
-- the parser backtracks, and thus only contains state modifications
-- performed by successful parses. On the other hand, non-backtracking
-- state would contain all modifications made during the parsing
-- process and allow us to observe unsuccessful attempts.
--
-- It turns out that:
--
-- - parsec's old built-in user state is backtracking
-- - using @StateT s (ParsecT ...)@ is backtracking
-- - using @ParsecT ... (StateT s ...)@ is non-backtracking
--
-- We want all our state to be backtracking.
--
-- Note that this is in deviation from what the old LH parser did,
-- but I think that was plainly wrong.
type Parser = StateT PState (Parsec Void String)
-- | The parser state.
--
-- We keep track of the fixities of infix operators.
--
-- We also keep track of whether empty list and singleton lists
-- syntax is allowed (and how they are to be interpreted, if they
-- are).
--
-- We also keep track of an integer counter that can be used to
-- supply unique integers during the parsing process.
--
-- Finally, we keep track of the layout stack.
--
data PState = PState { fixityTable :: OpTable
, fixityOps :: [Fixity]
, empList :: Maybe Expr
, singList :: Maybe (Expr -> Expr)
, supply :: !Integer
, layoutStack :: LayoutStack
}
-- | The layout stack tracks columns at which layout blocks
-- have started.
--
data LayoutStack =
Empty -- ^ no layout info
| Reset LayoutStack -- ^ in a block not using layout
| At Pos LayoutStack -- ^ in a block at the given column
| After Pos LayoutStack -- ^ past a block at the given column
deriving Show
-- | Pop the topmost element from the stack.
popLayoutStack :: LayoutStack -> LayoutStack
popLayoutStack Empty = error "unbalanced layout stack"
popLayoutStack (Reset s) = s
popLayoutStack (At _ s) = s
popLayoutStack (After _ s) = s
-- | Modify the layout stack using the given function.
modifyLayoutStack :: (LayoutStack -> LayoutStack) -> Parser ()
modifyLayoutStack f =
modify (\ s -> s { layoutStack = f (layoutStack s) })
-- | Start a new layout block at the current indentation level.
setLayout :: Parser ()
setLayout = do
i <- L.indentLevel
-- traceShow ("setLayout", i) $ pure ()
modifyLayoutStack (At i)
-- | Temporarily reset the layout information, because we enter
-- a block with explicit separators.
--
resetLayout :: Parser ()
resetLayout = do
-- traceShow ("resetLayout") $ pure ()
modifyLayoutStack Reset
-- | Remove the topmost element from the layout stack.
popLayout :: Parser ()
popLayout = do
-- traceShow ("popLayout") $ pure ()
modifyLayoutStack popLayoutStack
-- | Consumes all whitespace, including LH comments.
--
-- Should not be used directly, but primarily via 'lexeme'.
--
-- The only "valid" use case for spaces is in top-level parsing
-- function, to consume initial spaces.
--
spaces :: Parser ()
spaces =
L.space
space1
lhLineComment
lhBlockComment
-- | Verify that the current indentation level is in the given
-- relation to the provided reference level, otherwise fail.
--
-- This is a variant of 'indentGuard' provided by megaparsec,
-- only that it does not consume whitespace.
--
guardIndentLevel :: Ordering -> Pos -> Parser ()
guardIndentLevel ord ref = do
actual <- L.indentLevel
-- traceShow ("guardIndentLevel", actual, ord, ref) $ pure ()
unless (compare actual ref == ord)
(L.incorrectIndent ord ref actual)
-- | Checks the current indentation level with respect to the
-- current layout stack. May fail. Returns the parser to run
-- after the next token.
--
-- This function is intended to be used within a layout block
-- to check whether the next token is valid within the current
-- block.
--
guardLayout :: Parser (Parser ())
guardLayout = do
stack <- gets layoutStack
-- traceShow ("guardLayout", stack) $ pure ()
case stack of
At i s -> guardIndentLevel EQ i *> pure (modifyLayoutStack (const (After i (At i s))))
-- Note: above, we must really set the stack to 'After i (At i s)' explicitly.
-- Otherwise, repeated calls to 'guardLayout' at the same column could push
-- multiple 'After' entries on the stack.
After i _ -> guardIndentLevel GT i *> pure (pure ())
_ -> pure (pure ())
-- | Checks the current indentation level with respect to the
-- current layout stack. The current indentation level must
-- be strictly greater than the one of the surrounding block.
-- May fail.
--
-- This function is intended to be used before we establish
-- a new, nested, layout block, which should be indented further
-- than the surrounding blocks.
--
strictGuardLayout :: Parser ()
strictGuardLayout = do
stack <- gets layoutStack
-- traceShow ("strictGuardLayout", stack) $ pure ()
case stack of
At i _ -> guardIndentLevel GT i *> pure ()
After i _ -> guardIndentLevel GT i *> pure ()
_ -> pure ()
-- | Indentation-aware lexeme parser. Before parsing, establishes
-- whether we are in a position permitted by the layout stack.
-- After the token, consume whitespace and potentially change state.
--
lexeme :: Parser a -> Parser a
lexeme p = do
after <- guardLayout
p <* spaces <* after
-- | Indentation-aware located lexeme parser.
--
-- This is defined in such a way that it determines the actual source range
-- covered by the identifier. I.e., it consumes additional whitespace in the
-- end, but that is not part of the source range reported for the identifier.
--
locLexeme :: Parser a -> Parser (Located a)
locLexeme p = do
after <- guardLayout
l1 <- getSourcePos
x <- p
l2 <- getSourcePos
spaces <* after
pure (Loc l1 l2 x)
-- | Make a parser location-aware.
--
-- This is at the cost of an imprecise span because we still
-- consume spaces in the end first.
--
located :: Parser a -> Parser (Located a)
located p = do
l1 <- getSourcePos
x <- p
l2 <- getSourcePos
pure (Loc l1 l2 x)
-- | Parse a block delimited by layout.
-- The block must be indented more than the surrounding blocks,
-- otherwise we return an empty list.
--
-- Assumes that the parser for items does not accept the empty string.
--
indentedBlock :: Parser a -> Parser [a]
indentedBlock p =
strictGuardLayout *> setLayout *> many (p <* popLayout) <* popLayout
-- We have to pop after every p, because the first successful
-- token moves from 'At' to 'After'. We have to pop at the end,
-- because we want to remove 'At'.
<|> pure []
-- We need to have a fallback with the empty list, because if the
-- layout check fails, we still want to accept this as an empty block.
-- | Parse a single line that may be continued via layout.
indentedLine :: Parser a -> Parser a
indentedLine p =
setLayout *> p <* popLayout <* popLayout
-- We have to pop twice, because the first successful token
-- moves from 'At' to 'After', so we have to remove both.
-- | Parse a block of items which can be delimited either via
-- layout or via explicit delimiters as specified.
--
-- Assumes that the parser for items does not accept the empty string.
--
indentedOrExplicitBlock :: Parser open -> Parser close -> Parser sep -> Parser a -> Parser [a]
indentedOrExplicitBlock open close sep p =
explicitBlock open close sep p
<|> (concat <$> indentedBlock (sepEndBy1 p sep))
-- | Parse a block of items that are delimited via explicit delimiters.
-- Layout is disabled/reset for the scope of this block.
--
explicitBlock :: Parser open -> Parser close -> Parser sep -> Parser a -> Parser [a]
explicitBlock open close sep p =
resetLayout *> open *> sepEndBy p sep <* close <* popLayout
-- | Symbolic lexeme. Stands on its own.
sym :: String -> Parser String
sym x =
lexeme (string x)
-- | Located variant of 'sym'.
locSym :: String -> Parser (Located String)
locSym x =
locLexeme (string x)
semi, comma, colon, dcolon, dot :: Parser String
semi = sym ";"
comma = sym ","
colon = sym ":" -- Note: not a reserved symbol; use with care
dcolon = sym "::" -- Note: not a reserved symbol; use with care
dot = sym "." -- Note: not a reserved symbol; use with care
-- | Parses a block via layout or explicit braces and semicolons.
--
-- Assumes that the parser for items does not accept the empty string.
--
-- However, even in layouted mode, we are allowing semicolons to
-- separate block contents. We also allow semicolons at the beginning,
-- end, and multiple subsequent semicolons, so the resulting parser
-- provides the illusion of allowing empty items.
--
block :: Parser a -> Parser [a]
block =
indentedOrExplicitBlock (sym "{" *> many semi) (sym "}") (some semi)
-- | Parses a block with explicit braces and commas as separator.
-- Used for record constructors in datatypes.
--
explicitCommaBlock :: Parser a -> Parser [a]
explicitCommaBlock =
explicitBlock (sym "{") (sym "}") comma
--------------------------------------------------------------------
reservedNames :: S.HashSet String
reservedNames = S.fromList
[ -- reserved words used in fixpoint
"SAT"
, "UNSAT"
, "true"
, "false"
, "mod"
, "data"
, "Bexp"
-- , "True"
-- , "Int"
, "import"
, "if", "then", "else"
, "func"
, "autorewrite"
, "rewrite"
-- reserved words used in liquid haskell
, "forall"
, "coerce"
, "exists"
, "module"
, "spec"
, "where"
, "decrease"
, "lazyvar"
, "LIQUID"
, "lazy"
, "local"
, "assert"
, "assume"
, "automatic-instances"
, "autosize"
, "axiomatize"
, "bound"
, "class"
, "data"
, "define"
, "defined"
, "embed"
, "expression"
, "import"
, "include"
, "infix"
, "infixl"
, "infixr"
, "inline"
, "instance"
, "invariant"
, "measure"
, "newtype"
, "predicate"
, "qualif"
, "reflect"
, "type"
, "using"
, "with"
, "in"
]
-- TODO: This is currently unused.
--
-- The only place where this is used in the original parsec code is in the
-- Text.Parsec.Token.operator parser.
--
_reservedOpNames :: [String]
_reservedOpNames =
[ "+", "-", "*", "/", "\\", ":"
, "<", ">", "<=", ">=", "=", "!=" , "/="
, "mod", "and", "or"
--, "is"
, "&&", "||"
, "~", "=>", "==>", "<=>"
, "->"
, ":="
, "&", "^", "<<", ">>", "--"
, "?", "Bexp"
, "'"
, "_|_"
, "|"
, "<:"
, "|-"
, "::"
, "."
]
{-
lexer :: Monad m => Token.GenTokenParser String u m
lexer = Token.makeTokenParser languageDef
-}
-- | Consumes a line comment.
lhLineComment :: Parser ()
lhLineComment =
L.skipLineComment "// "
-- | Consumes a block comment.
lhBlockComment :: Parser ()
lhBlockComment =
L.skipBlockComment "/* " "*/"
-- | Parser that consumes a single char within an identifier (not start of identifier).
identLetter :: Parser Char
identLetter =
alphaNumChar <|> oneOf ("_" :: String)
-- | Parser that consumes a single char within an operator (not start of operator).
opLetter :: Parser Char
opLetter =
oneOf (":!#$%&*+./<=>?@\\^|-~'" :: String)
-- | Parser that consumes the given reserved word.
--
-- The input token cannot be longer than the given name.
--
-- NOTE: we currently don't double-check that the reserved word is in the
-- list of reserved words.
--
reserved :: String -> Parser ()
reserved x =
void $ lexeme (try (string x <* notFollowedBy identLetter))
locReserved :: String -> Parser (Located String)
locReserved x =
locLexeme (try (string x <* notFollowedBy identLetter))
-- | Parser that consumes the given reserved operator.
--
-- The input token cannot be longer than the given name.
--
-- NOTE: we currently don't double-check that the reserved operator is in the
-- list of reserved operators.
--
reservedOp :: String -> Parser ()
reservedOp x =
void $ lexeme (try (string x <* notFollowedBy opLetter))
-- | Parser that consumes the given symbol.
--
-- The difference with 'reservedOp' is that the given symbol is seen
-- as a token of its own, so the next character that follows does not
-- matter.
--
-- symbol :: String -> Parser String
-- symbol x =
-- L.symbol spaces (string x)
parens, brackets, angles, braces :: Parser a -> Parser a
parens = between (sym "(") (sym ")")
brackets = between (sym "[") (sym "]")
angles = between (sym "<") (sym ">")
braces = between (sym "{") (sym "}")
locParens :: Parser a -> Parser (Located a)
locParens p =
(\ (Loc l1 _ _) a (Loc _ l2 _) -> Loc l1 l2 a) <$> locSym "(" <*> p <*> locSym ")"
-- | Parses a string literal as a lexeme. This is based on megaparsec's
-- 'charLiteral' parser, which claims to handle all the single-character
-- escapes defined by the Haskell grammar.
--
stringLiteral :: Parser String
stringLiteral =
lexeme stringR <?> "string literal"
locStringLiteral :: Parser (Located String)
locStringLiteral =
locLexeme stringR <?> "string literal"
stringR :: Parser String
stringR =
char '\"' *> manyTill L.charLiteral (char '\"')
-- | Consumes a float literal lexeme.
double :: Parser Double
double = lexeme L.float <?> "float literal"
-- identifier :: Parser String
-- identifier = Token.identifier lexer
-- | Consumes a natural number literal lexeme, which can be
-- in decimal, octal and hexadecimal representation.
--
-- This does not parse negative integers. Unary minus is available
-- as an operator in the expression language.
--
natural :: Parser Integer
natural =
lexeme naturalR <?> "nat literal"
locNatural :: Parser (Located Integer)
locNatural =
locLexeme naturalR <?> "nat literal"
naturalR :: Parser Integer
naturalR =
try (char '0' *> char' 'x') *> L.hexadecimal
<|> try (char '0' *> char' 'o') *> L.octal
<|> L.decimal
-- | Raw (non-whitespace) parser for an identifier adhering to certain conditions.
--
-- The arguments are as follows, in order:
--
-- * the parser for the initial character,
-- * a predicate indicating which subsequent characters are ok,
-- * a check for the entire identifier to be applied in the end,
-- * an error message to display if the final check fails.
--
condIdR :: Parser Char -> (Char -> Bool) -> (String -> Bool) -> String -> Parser Symbol
condIdR initial okChars condition msg = do
s <- (:) <$> initial <*> takeWhileP Nothing okChars
if condition s
then pure (symbol s)
else fail (msg <> " " <> show s)
-- TODO: The use of the following parsers is unsystematic.
-- | Raw parser for an identifier starting with an uppercase letter.
--
-- See Note [symChars].
--
upperIdR :: Parser Symbol
upperIdR =
condIdR upperChar (`S.member` symChars) (const True) "unexpected"
-- | Raw parser for an identifier starting with a lowercase letter.
--
-- See Note [symChars].
--
lowerIdR :: Parser Symbol
lowerIdR =
condIdR (lowerChar <|> char '_') (`S.member` symChars) isNotReserved "unexpected reserved word"
-- | Raw parser for an identifier starting with any letter.
--
-- See Note [symChars].
--
symbolR :: Parser Symbol
symbolR =
condIdR (letterChar <|> char '_') (`S.member` symChars) isNotReserved "unexpected reserved word"
isNotReserved :: String -> Bool
isNotReserved s = not (s `S.member` reservedNames)
-- | Predicate version to check if the characer is a valid initial
-- character for 'lowerIdR'.
--
-- TODO: What is this needed for?
--
isSmall :: Char -> Bool
isSmall c = Char.isLower c || c == '_'
-- Note [symChars].
--
-- The parser 'symChars' is very permissive. In particular, we allow
-- dots (for qualified names), and characters such as @$@ to be able
-- to refer to identifiers as they occur in e.g. GHC Core.
----------------------------------------------------------------
------------------------- Expressions --------------------------
----------------------------------------------------------------
-- | Lexeme version of 'upperIdR'.
--
upperIdP :: Parser Symbol
upperIdP =
lexeme upperIdR <?> "upperIdP"
-- | Lexeme version of 'lowerIdR'.
--
lowerIdP :: Parser Symbol
lowerIdP =
lexeme lowerIdR <?> "lowerIdP"
-- | Unconstrained identifier, lower- or uppercase.
--
-- Must not be a reserved word.
--
-- Lexeme version of 'symbolR'.
--
symbolP :: Parser Symbol
symbolP =
lexeme symbolR <?> "identifier"
-- The following are located versions of the lexeme identifier parsers.
locSymbolP, locLowerIdP, locUpperIdP :: Parser LocSymbol
locLowerIdP = locLexeme lowerIdR
locUpperIdP = locLexeme upperIdR
locSymbolP = locLexeme symbolR
-- | Parser for literal numeric constants: floats or integers without sign.
constantP :: Parser Constant
constantP =
try (R <$> double) -- float literal
<|> I <$> natural -- nat literal
-- | Parser for literal string contants.
symconstP :: Parser SymConst
symconstP = SL . T.pack <$> stringLiteral
-- | Parser for "atomic" expressions.
--
-- This parser is reused by Liquid Haskell.
--
expr0P :: Parser Expr
expr0P
= trueP -- constant "true"
<|> falseP -- constant "false"
<|> fastIfP EIte exprP -- "if-then-else", starts with "if"
<|> coerceP exprP -- coercion, starts with "coerce"
<|> (ESym <$> symconstP) -- string literal, starts with double-quote
<|> (ECon <$> constantP) -- numeric literal, starts with a digit
<|> (reservedOp "_|_" >> return EBot) -- constant bottom, equivalent to "false"
<|> lamP -- lambda abstraction, starts with backslash
<|> try tupleP -- tuple expressions, starts with "("
<|> try (parens exprP) -- parenthesised expression, starts with "("
<|> try (parens exprCastP) -- explicit type annotation, starts with "(", TODO: should be an operator rather than require parentheses?
<|> EVar <$> symbolP -- identifier, starts with any letter or underscore
<|> try (brackets (pure ()) >> emptyListP) -- empty list, start with "["
<|> try (brackets exprP >>= singletonListP) -- singleton list, starts with "["
--
-- Note:
--
-- In the parsers above, it is important that *all* parsers starting with "("
-- are prefixed with "try". This is because expr0P itself is chained with
-- additional parsers in funAppP ...
emptyListP :: Parser Expr
emptyListP = do
e <- empList <$> get
case e of
Nothing -> fail "No parsing support for empty lists"
Just s -> return s
singletonListP :: Expr -> Parser Expr
singletonListP e = do
f <- singList <$> get
case f of
Nothing -> fail "No parsing support for singleton lists"
Just s -> return $ s e
-- | Parser for an explicitly type-annotated expression.
exprCastP :: Parser Expr
exprCastP
= do e <- exprP
try dcolon <|> colon -- allow : or :: *and* allow following symbols
so <- sortP
return $ ECst e so
fastIfP :: (Expr -> a -> a -> a) -> Parser a -> Parser a
fastIfP f bodyP
= do reserved "if"
p <- predP
reserved "then"
b1 <- bodyP
reserved "else"
b2 <- bodyP
return $ f p b1 b2
coerceP :: Parser Expr -> Parser Expr
coerceP p = do
reserved "coerce"
(s, t) <- parens (pairP sortP (reservedOp "~") sortP)
e <- p
return $ ECoerc s t e
{-
qmIfP f bodyP
= parens $ do
p <- predP
reserved "?"
b1 <- bodyP
colon
b2 <- bodyP
return $ f p b1 b2
-}
-- | Parser for atomic expressions plus function applications.
--
-- Base parser used in 'exprP' which adds in other operators.
--
expr1P :: Parser Expr
expr1P
= try funAppP
<|> expr0P
-- | Expressions
exprP :: Parser Expr
exprP =
do
table <- gets fixityTable
makeExprParser expr1P (flattenOpTable table)
data Assoc = AssocNone | AssocLeft | AssocRight
data Fixity
= FInfix {fpred :: Maybe Int, fname :: String, fop2 :: Maybe (Expr -> Expr -> Expr), fassoc :: Assoc}
| FPrefix {fpred :: Maybe Int, fname :: String, fop1 :: Maybe (Expr -> Expr)}
| FPostfix {fpred :: Maybe Int, fname :: String, fop1 :: Maybe (Expr -> Expr)}
-- | An OpTable stores operators by their fixity.
--
-- Fixity levels range from 9 (highest) to 0 (lowest).
type OpTable = IM.IntMap [Operator Parser Expr] -- [[Operator Parser Expr]]
-- | Transform an operator table to the form expected by 'makeExprParser',
-- which wants operators sorted by decreasing priority.
--
flattenOpTable :: OpTable -> [[Operator Parser Expr]]
flattenOpTable =
(snd <$>) <$> IM.toDescList
-- | Add an operator to the parsing state.
addOperatorP :: Fixity -> Parser ()
addOperatorP op
= modify $ \s -> s{ fixityTable = addOperator op (fixityTable s)
, fixityOps = op:fixityOps s
}
-- | Parses any of the known infix operators.
infixSymbolP :: Parser Symbol
infixSymbolP = do
ops <- infixOps <$> get
choice (reserved' <$> ops)
where
infixOps st = [s | FInfix _ s _ _ <- fixityOps st]
reserved' x = reserved x >> return (symbol x)
-- | Located version of 'infixSymbolP'.
locInfixSymbolP :: Parser (Located Symbol)
locInfixSymbolP = do
ops <- infixOps <$> get
choice (reserved' <$> ops)
where
infixOps st = [s | FInfix _ s _ _ <- fixityOps st]
reserved' x = locReserved x >>= \ (Loc l1 l2 _) -> return (Loc l1 l2 (symbol x))
-- | Helper function that turns an associativity into the right constructor for 'Operator'.
mkInfix :: Assoc -> parser (expr -> expr -> expr) -> Operator parser expr
mkInfix AssocLeft = InfixL
mkInfix AssocRight = InfixR
mkInfix AssocNone = InfixN
-- | Add the given operator to the operator table.
addOperator :: Fixity -> OpTable -> OpTable
addOperator (FInfix p x f assoc) ops
= insertOperator (makePrec p) (mkInfix assoc (reservedOp x >> return (makeInfixFun x f))) ops
addOperator (FPrefix p x f) ops
= insertOperator (makePrec p) (Prefix (reservedOp x >> return (makePrefixFun x f))) ops
addOperator (FPostfix p x f) ops
= insertOperator (makePrec p) (Postfix (reservedOp x >> return (makePrefixFun x f))) ops
-- | Helper function for computing the priority of an operator.
--
-- If no explicit priority is given, a priority of 9 is assumed.
--
makePrec :: Maybe Int -> Int
makePrec = fromMaybe 9
makeInfixFun :: String -> Maybe (Expr -> Expr -> Expr) -> Expr -> Expr -> Expr
makeInfixFun x = fromMaybe (\e1 e2 -> EApp (EApp (EVar $ symbol x) e1) e2)
makePrefixFun :: String -> Maybe (Expr -> Expr) -> Expr -> Expr
makePrefixFun x = fromMaybe (EApp (EVar $ symbol x))
-- | Add an operator at the given priority to the operator table.
insertOperator :: Int -> Operator Parser Expr -> OpTable -> OpTable
insertOperator i op = IM.alter (Just . (op :) . fromMaybe []) i
-- | The initial (empty) operator table.
initOpTable :: OpTable
initOpTable = IM.empty
-- | Built-in operator table, parameterised over the composition function.
bops :: Maybe Expr -> OpTable
bops cmpFun = foldl' (flip addOperator) initOpTable builtinOps
where
-- Built-in Haskell operators, see https://www.haskell.org/onlinereport/decls.html#fixity
builtinOps :: [Fixity]
builtinOps = [ FPrefix (Just 9) "-" (Just ENeg)
, FInfix (Just 7) "*" (Just $ EBin Times) AssocLeft
, FInfix (Just 7) "/" (Just $ EBin Div) AssocLeft
, FInfix (Just 6) "-" (Just $ EBin Minus) AssocLeft
, FInfix (Just 6) "+" (Just $ EBin Plus) AssocLeft
, FInfix (Just 5) "mod" (Just $ EBin Mod) AssocLeft -- Haskell gives mod 7
, FInfix (Just 9) "." applyCompose AssocRight
]
applyCompose :: Maybe (Expr -> Expr -> Expr)
applyCompose = (\f x y -> (f `eApps` [x,y])) <$> cmpFun
-- | Parser for function applications.
--
-- Andres, TODO: Why is this so complicated?
--
funAppP :: Parser Expr
funAppP = litP <|> exprFunP <|> simpleAppP
where
exprFunP = mkEApp <$> funSymbolP <*> funRhsP
funRhsP = some expr0P
<|> parens innerP
innerP = brackets (sepBy exprP semi)
-- TODO:AZ the parens here should be superfluous, but it hits an infinite loop if removed
simpleAppP = EApp <$> parens exprP <*> parens exprP
funSymbolP = locSymbolP
-- | Parser for tuple expressions (two or more components).
tupleP :: Parser Expr
tupleP = do
Loc l1 l2 (first, rest) <- locParens ((,) <$> exprP <* comma <*> sepBy1 exprP comma) -- at least two components necessary
let cons = symbol $ "(" ++ replicate (length rest) ',' ++ ")" -- stored in prefix form
return $ mkEApp (Loc l1 l2 cons) (first : rest)
-- TODO:AZ: The comment says BitVector literal, but it accepts any @Sort@
-- | BitVector literal: lit "#x00000001" (BitVec (Size32 obj))
litP :: Parser Expr
litP = do reserved "lit"
l <- stringLiteral
t <- sortP
return $ ECon $ L (T.pack l) t
-- | Parser for lambda abstractions.
lamP :: Parser Expr
lamP
= do reservedOp "\\"
x <- symbolP
colon -- TODO: this should probably be reservedOp instead
t <- sortP
reservedOp "->"
e <- exprP
return $ ELam (x, t) e
varSortP :: Parser Sort
varSortP = FVar <$> parens intP
-- | Parser for function sorts without the "func" keyword.
funcSortP :: Parser Sort
funcSortP = parens $ mkFFunc <$> intP <* comma <*> sortsP
sortsP :: Parser [Sort]
sortsP = try (brackets (sepBy sortP semi))
<|> (brackets (sepBy sortP comma))
-- | Parser for sorts (types).
sortP :: Parser Sort
sortP = sortP' (many sortArgP)
sortArgP :: Parser Sort
sortArgP = sortP' (return [])
{-
sortFunP :: Parser Sort
sortFunP
= try (string "@" >> varSortP)
<|> (fTyconSort <$> fTyConP)
-}
-- | Parser for sorts, parameterised over the parser for arguments.
--
-- TODO, Andres: document the parameter better.
--
sortP' :: Parser [Sort] -> Parser Sort
sortP' appArgsP
= parens sortP -- parenthesised sort, starts with "("
<|> (reserved "func" >> funcSortP) -- function sort, starts with "func"
<|> (fAppTC listFTyCon . pure <$> brackets sortP)
-- <|> bvSortP -- Andres: this looks unreachable, as it starts with "("
<|> (fAppTC <$> fTyConP <*> appArgsP)
<|> (fApp <$> tvarP <*> appArgsP)
tvarP :: Parser Sort
tvarP
= (string "@" >> varSortP)
<|> (FObj . symbol <$> lowerIdP)
fTyConP :: Parser FTycon
fTyConP
= (reserved "int" >> return intFTyCon)
<|> (reserved "Integer" >> return intFTyCon)
<|> (reserved "Int" >> return intFTyCon)
-- <|> (reserved "int" >> return intFTyCon) -- TODO:AZ duplicate?
<|> (reserved "real" >> return realFTyCon)
<|> (reserved "bool" >> return boolFTyCon)
<|> (reserved "num" >> return numFTyCon)
<|> (reserved "Str" >> return strFTyCon)
<|> (symbolFTycon <$> locUpperIdP)
-- | Bit-Vector Sort
bvSortP :: Parser Sort
bvSortP = mkSort <$> (bvSizeP "Size32" S32 <|> bvSizeP "Size64" S64)
where
bvSizeP ss s = do
parens (reserved "BitVec" >> reserved ss)
return s
--------------------------------------------------------------------------------
-- | Predicates ----------------------------------------------------------------
--------------------------------------------------------------------------------
-- | Parser for "atomic" predicates.
--
-- This parser is reused by Liquid Haskell.
--
pred0P :: Parser Expr
pred0P = trueP -- constant "true"
<|> falseP -- constant "false"
<|> (reservedOp "??" >> makeUniquePGrad)
<|> kvarPredP
<|> fastIfP pIte predP -- "if-then-else", starts with "if"
<|> try predrP -- binary relation, starts with anything that an expr can start with
<|> (parens predP) -- parenthesised predicate, starts with "("
<|> (reservedOp "?" *> exprP)
<|> try funAppP
<|> EVar <$> symbolP -- identifier, starts with any letter or underscore
<|> (reservedOp "&&" >> pGAnds <$> predsP) -- built-in prefix and
<|> (reservedOp "||" >> POr <$> predsP) -- built-in prefix or
makeUniquePGrad :: Parser Expr
makeUniquePGrad
= do uniquePos <- getSourcePos
return $ PGrad (KV $ symbol $ show uniquePos) mempty (srcGradInfo uniquePos) mempty
-- qmP = reserved "?" <|> reserved "Bexp"
-- | Parser for the reserved constant "true".
trueP :: Parser Expr
trueP = reserved "true" >> return PTrue
-- | Parser for the reserved constant "false".
falseP :: Parser Expr
falseP = reserved "false" >> return PFalse
kvarPredP :: Parser Expr
kvarPredP = PKVar <$> kvarP <*> substP
kvarP :: Parser KVar
kvarP = KV <$> lexeme (char '$' *> symbolR)
substP :: Parser Subst
substP = mkSubst <$> many (brackets $ pairP symbolP aP exprP)
where
aP = reservedOp ":="
-- | Parses a semicolon-separated bracketed list of predicates.
--
-- Used as the argument of the prefix-versions of conjunction and
-- disjunction.
--
predsP :: Parser [Expr]
predsP = brackets $ sepBy predP semi
-- | Parses a predicate.
--
-- Unlike for expressions, there is a built-in operator list.
--
predP :: Parser Expr
predP = makeExprParser pred0P lops
where
lops = [ [Prefix (reservedOp "~" >> return PNot)]
, [Prefix (reserved "not" >> return PNot)]
, [InfixR (reservedOp "&&" >> return pGAnd)]
, [InfixR (reservedOp "||" >> return (\x y -> POr [x,y]))]
, [InfixR (reservedOp "=>" >> return PImp)]
, [InfixR (reservedOp "==>" >> return PImp)]
, [InfixR (reservedOp "=" >> return PIff)]
, [InfixR (reservedOp "<=>" >> return PIff)]]
-- | Parses a relation predicate.
--
-- Binary relations connect expressions and predicates.
--
predrP :: Parser Expr
predrP =
(\ e1 r e2 -> r e1 e2) <$> exprP <*> brelP <*> exprP
-- | Parses a relation symbol.
--
-- There is a built-in table of available relations.
--
brelP :: Parser (Expr -> Expr -> Expr)
brelP = (reservedOp "==" >> return (PAtom Eq))
<|> (reservedOp "=" >> return (PAtom Eq))
<|> (reservedOp "~~" >> return (PAtom Ueq))
<|> (reservedOp "!=" >> return (PAtom Ne))
<|> (reservedOp "/=" >> return (PAtom Ne))
<|> (reservedOp "!~" >> return (PAtom Une))
<|> (reservedOp "<" >> return (PAtom Lt))
<|> (reservedOp "<=" >> return (PAtom Le))
<|> (reservedOp ">" >> return (PAtom Gt))
<|> (reservedOp ">=" >> return (PAtom Ge))
--------------------------------------------------------------------------------
-- | BareTypes -----------------------------------------------------------------
--------------------------------------------------------------------------------
-- | Refa
refaP :: Parser Expr
refaP = try (pAnd <$> brackets (sepBy predP semi))
<|> predP
-- | (Sorted) Refinements with configurable sub-parsers
refBindP :: Parser Symbol -> Parser Expr -> Parser (Reft -> a) -> Parser a
refBindP bp rp kindP
= braces $ do
x <- bp
t <- kindP
reservedOp "|"
ra <- rp <* spaces
return $ t (Reft (x, ra))
-- bindP = symbol <$> (lowerIdP <* colon)
-- | Binder (lowerIdP <* colon)
bindP :: Parser Symbol
bindP = symbolP <* colon
optBindP :: Symbol -> Parser Symbol
optBindP x = try bindP <|> return x
-- | (Sorted) Refinements
refP :: Parser (Reft -> a) -> Parser a
refP = refBindP bindP refaP
-- | (Sorted) Refinements with default binder
refDefP :: Symbol -> Parser Expr -> Parser (Reft -> a) -> Parser a
refDefP x = refBindP (optBindP x)
--------------------------------------------------------------------------------
-- | Parsing Data Declarations -------------------------------------------------
--------------------------------------------------------------------------------
dataFieldP :: Parser DataField
dataFieldP = DField <$> locSymbolP <* colon <*> sortP
dataCtorP :: Parser DataCtor
dataCtorP = DCtor <$> locSymbolP
<*> braces (sepBy dataFieldP comma)
dataDeclP :: Parser DataDecl
dataDeclP = DDecl <$> fTyConP <*> intP <* reservedOp "="
<*> brackets (many (reservedOp "|" *> dataCtorP))
--------------------------------------------------------------------------------
-- | Parsing Qualifiers --------------------------------------------------------
--------------------------------------------------------------------------------
-- | Qualifiers
qualifierP :: Parser Sort -> Parser Qualifier
qualifierP tP = do
pos <- getSourcePos
n <- upperIdP
params <- parens $ sepBy1 (qualParamP tP) comma
_ <- colon
body <- predP
return $ mkQual n params body pos
qualParamP :: Parser Sort -> Parser QualParam
qualParamP tP = do
x <- symbolP
pat <- qualPatP
_ <- colon
t <- tP
return $ QP x pat t
qualPatP :: Parser QualPattern
qualPatP
= (reserved "as" >> qualStrPatP)
<|> return PatNone
qualStrPatP :: Parser QualPattern
qualStrPatP
= (PatExact <$> symbolP)
<|> parens ( (uncurry PatPrefix <$> pairP symbolP dot qpVarP)
<|> (uncurry PatSuffix <$> pairP qpVarP dot symbolP) )
qpVarP :: Parser Int
qpVarP = char '$' *> intP
symBindP :: Parser a -> Parser (Symbol, a)
symBindP = pairP symbolP colon
pairP :: Parser a -> Parser z -> Parser b -> Parser (a, b)
pairP xP sepP yP = (,) <$> xP <* sepP <*> yP
---------------------------------------------------------------------
-- | Axioms for Symbolic Evaluation ---------------------------------
---------------------------------------------------------------------
autoRewriteP :: Parser AutoRewrite
autoRewriteP = do
args <- sepBy sortedReftP spaces
_ <- spaces
_ <- reserved "="
_ <- spaces
(lhs, rhs) <- braces $
pairP exprP (reserved "=") exprP
return $ AutoRewrite args lhs rhs
defineP :: Parser Equation
defineP = do
name <- symbolP
params <- parens $ sepBy (symBindP sortP) comma
sort <- colon *> sortP
body <- reserved "=" *> braces (
if sort == boolSort then predP else exprP
)
return $ mkEquation name params body sort
matchP :: Parser Rewrite
matchP = SMeasure <$> symbolP <*> symbolP <*> many symbolP <*> (reserved "=" >> exprP)
pairsP :: Parser a -> Parser b -> Parser [(a, b)]
pairsP aP bP = brackets $ sepBy1 (pairP aP (reserved ":") bP) semi
---------------------------------------------------------------------
-- | Parsing Constraints (.fq files) --------------------------------
---------------------------------------------------------------------
-- Entities in Query File
data Def a
= Srt !Sort
| Cst !(SubC a)
| Wfc !(WfC a)
| Con !Symbol !Sort
| Dis !Symbol !Sort
| Qul !Qualifier
| Kut !KVar
| Pack !KVar !Int
| IBind !Int !Symbol !SortedReft
| EBind !Int !Symbol !Sort
| Opt !String
| Def !Equation
| Mat !Rewrite
| Expand ![(Int,Bool)]
| Adt !DataDecl
| AutoRW !Int !AutoRewrite
| RWMap ![(Int,Int)]
deriving (Show, Generic)
-- Sol of solbind
-- Dep of FixConstraint.dep
fInfoOptP :: Parser (FInfoWithOpts ())
fInfoOptP = do ps <- many defP
return $ FIO (defsFInfo ps) [s | Opt s <- ps]
fInfoP :: Parser (FInfo ())
fInfoP = defsFInfo <$> {- SCC "many-defP" #-} many defP
defP :: Parser (Def ())
defP = Srt <$> (reserved "sort" >> colon >> sortP)
<|> Cst <$> (reserved "constraint" >> colon >> {- SCC "subCP" #-} subCP)
<|> Wfc <$> (reserved "wf" >> colon >> {- SCC "wfCP" #-} wfCP)
<|> Con <$> (reserved "constant" >> symbolP) <*> (colon >> sortP)
<|> Dis <$> (reserved "distinct" >> symbolP) <*> (colon >> sortP)
<|> Pack <$> (reserved "pack" >> kvarP) <*> (colon >> intP)
<|> Qul <$> (reserved "qualif" >> qualifierP sortP)
<|> Kut <$> (reserved "cut" >> kvarP)
<|> EBind <$> (reserved "ebind" >> intP) <*> symbolP <*> (colon >> braces sortP)
<|> IBind <$> (reserved "bind" >> intP) <*> symbolP <*> (colon >> sortedReftP)
<|> Opt <$> (reserved "fixpoint" >> stringLiteral)
<|> Def <$> (reserved "define" >> defineP)
<|> Mat <$> (reserved "match" >> matchP)
<|> Expand <$> (reserved "expand" >> pairsP intP boolP)
<|> Adt <$> (reserved "data" >> dataDeclP)
<|> AutoRW <$> (reserved "autorewrite" >> intP) <*> autoRewriteP
<|> RWMap <$> (reserved "rewrite" >> pairsP intP intP)
sortedReftP :: Parser SortedReft
sortedReftP = refP (RR <$> (sortP <* spaces))
wfCP :: Parser (WfC ())
wfCP = do reserved "env"
env <- envP
reserved "reft"
r <- sortedReftP
let [w] = wfC env r ()
return w
subCP :: Parser (SubC ())
subCP = do pos <- getSourcePos
reserved "env"
env <- envP
reserved "lhs"
lhs <- sortedReftP
reserved "rhs"
rhs <- sortedReftP
reserved "id"
i <- natural <* spaces
tag <- tagP
pos' <- getSourcePos
return $ subC' env lhs rhs i tag pos pos'
subC' :: IBindEnv
-> SortedReft
-> SortedReft
-> Integer
-> Tag
-> SourcePos
-> SourcePos
-> SubC ()
subC' env lhs rhs i tag l l'
= case cs of
[c] -> c
_ -> die $ err sp $ "RHS without single conjunct at" <+> pprint l'
where
cs = subC env lhs rhs (Just i) tag ()
sp = SS l l'
tagP :: Parser [Int]
tagP = reserved "tag" >> spaces >> brackets (sepBy intP semi)
envP :: Parser IBindEnv
envP = do binds <- brackets $ sepBy (intP <* spaces) semi
return $ insertsIBindEnv binds emptyIBindEnv
intP :: Parser Int
intP = fromInteger <$> natural
boolP :: Parser Bool
boolP = (reserved "True" >> return True)
<|> (reserved "False" >> return False)
defsFInfo :: [Def a] -> FInfo a
defsFInfo defs = {- SCC "defsFI" #-} FI cm ws bs ebs lts dts kts qs binfo adts mempty mempty ae
where
cm = Misc.safeFromList
"defs-cm" [(cid c, c) | Cst c <- defs]
ws = Misc.safeFromList
"defs-ws" [(i, w) | Wfc w <- defs, let i = Misc.thd3 (wrft w)]
bs = bindEnvFromList $ exBinds ++ [(n,x,r) | IBind n x r <- defs]
ebs = [ n | (n,_,_) <- exBinds]
exBinds = [(n, x, RR t mempty) | EBind n x t <- defs]
lts = fromListSEnv [(x, t) | Con x t <- defs]
dts = fromListSEnv [(x, t) | Dis x t <- defs]
kts = KS $ S.fromList [k | Kut k <- defs]
qs = [q | Qul q <- defs]
binfo = mempty
expand = M.fromList [(fromIntegral i, f)| Expand fs <- defs, (i,f) <- fs]
eqs = [e | Def e <- defs]
rews = [r | Mat r <- defs]
autoRWs = M.fromList [(arId , s) | AutoRW arId s <- defs]
rwEntries = [(i, f) | RWMap fs <- defs, (i,f) <- fs]
rwMap = foldl insert (M.fromList []) rwEntries
where
insert map (cid, arId) =
case M.lookup arId autoRWs of
Just rewrite ->
M.insertWith (++) (fromIntegral cid) [rewrite] map
Nothing ->
map
cid = fromJust . sid
ae = AEnv eqs rews expand rwMap
adts = [d | Adt d <- defs]
-- msg = show $ "#Lits = " ++ (show $ length consts)
---------------------------------------------------------------------
-- | Interacting with Fixpoint --------------------------------------
---------------------------------------------------------------------
fixResultP :: Parser a -> Parser (FixResult a)
fixResultP pp
= (reserved "SAT" >> return (Safe mempty))
<|> (reserved "UNSAT" >> Unsafe mempty <$> brackets (sepBy pp comma))
<|> (reserved "CRASH" >> crashP pp)
crashP :: Parser a -> Parser (FixResult a)
crashP pp = do
i <- pp
msg <- takeWhileP Nothing (const True) -- consume the rest of the input
return $ Crash [i] msg
predSolP :: Parser Expr
predSolP = parens (predP <* (comma >> iQualP))
iQualP :: Parser [Symbol]
iQualP = upperIdP >> parens (sepBy symbolP comma)
solution1P :: Parser (KVar, Expr)
solution1P = do
reserved "solution:"
k <- kvP
reservedOp ":="
ps <- brackets $ sepBy predSolP semi
return (k, simplify $ PAnd ps)
where
kvP = try kvarP <|> (KV <$> symbolP)
solutionP :: Parser (M.HashMap KVar Expr)
solutionP = M.fromList <$> sepBy solution1P spaces
solutionFileP :: Parser (FixResult Integer, M.HashMap KVar Expr)
solutionFileP = (,) <$> fixResultP natural <*> solutionP
--------------------------------------------------------------------------------
-- | Parse via the given parser, and obtain the rest of the input
-- as well as the final source position.
--
remainderP :: Parser a -> Parser (a, String, SourcePos)
remainderP p
= do res <- p
str <- getInput
pos <- getSourcePos
return (res, str, pos)
-- | Initial parser state.
initPState :: Maybe Expr -> PState
initPState cmpFun = PState { fixityTable = bops cmpFun
, empList = Nothing
, singList = Nothing
, fixityOps = []
, supply = 0
, layoutStack = Empty
}
-- | Entry point for parsing, for testing.
--
-- Take the top-level parser, the source file name, and the input as a string.
-- Fails with an exception on a parse error.
--
doParse' :: Parser a -> SourceName -> String -> a
doParse' parser fileName input =
case runParser (evalStateT (spaces *> parser <* eof) (initPState Nothing)) fileName input of
Left peb@(ParseErrorBundle errors posState) -> -- parse errors; we extract the first error from the error bundle
let
((_, pos) :| _, _) = attachSourcePos errorOffset errors posState
in
die $ err (SS pos pos) (dErr peb)
Right r -> r -- successful parse with no remaining input
where
-- Turns the multiline error string from megaparsec into a pretty-printable Doc.
dErr :: ParseErrorBundle String Void -> Doc
dErr e = vcat (map text (lines (errorBundlePretty e)))
-- | Function to test parsers interactively.
parseTest' :: Show a => Parser a -> String -> IO ()
parseTest' parser input =
parseTest (evalStateT parser (initPState Nothing)) input
-- errorSpan :: ParseError -> SrcSpan
-- errorSpan e = SS l l where l = errorPos e
parseFromFile :: Parser b -> SourceName -> IO b
parseFromFile p f = doParse' p f <$> readFile f
parseFromStdIn :: Parser a -> IO a
parseFromStdIn p = doParse' p "stdin" . T.unpack <$> T.getContents
-- | Obtain a fresh integer during the parsing process.
freshIntP :: Parser Integer
freshIntP = do n <- gets supply
modify (\ s -> s{supply = n + 1})
return n
---------------------------------------------------------------------
-- Standalone SMTLIB2 commands --------------------------------------
---------------------------------------------------------------------
commandsP :: Parser [Command]
commandsP = sepBy commandP semi
commandP :: Parser Command
commandP
= (reserved "var" >> cmdVarP)
<|> (reserved "push" >> return Push)
<|> (reserved "pop" >> return Pop)
<|> (reserved "check" >> return CheckSat)
<|> (reserved "assert" >> (Assert Nothing <$> predP))
<|> (reserved "distinct" >> (Distinct <$> brackets (sepBy exprP comma)))
cmdVarP :: Parser Command
cmdVarP = error "UNIMPLEMENTED: cmdVarP"
-- do
-- x <- bindP
-- t <- sortP
-- return $ Declare x [] t
---------------------------------------------------------------------
-- Bundling Parsers into a Typeclass --------------------------------
---------------------------------------------------------------------
class Inputable a where
rr :: String -> a
rr' :: String -> String -> a
rr' _ = rr
rr = rr' ""
instance Inputable Symbol where
rr' = doParse' symbolP
instance Inputable Constant where
rr' = doParse' constantP
instance Inputable Expr where
rr' = doParse' exprP
instance Inputable (FixResult Integer) where
rr' = doParse' $ fixResultP natural
instance Inputable (FixResult Integer, FixSolution) where
rr' = doParse' solutionFileP
instance Inputable (FInfo ()) where
rr' = {- SCC "fInfoP" #-} doParse' fInfoP
instance Inputable (FInfoWithOpts ()) where
rr' = {- SCC "fInfoWithOptsP" #-} doParse' fInfoOptP
instance Inputable Command where
rr' = doParse' commandP
instance Inputable [Command] where
rr' = doParse' commandsP
{-
---------------------------------------------------------------
--------------------------- Testing ---------------------------
---------------------------------------------------------------
-- A few tricky predicates for parsing
-- myTest1 = "((((v >= 56320) && (v <= 57343)) => (((numchars a o ((i - o) + 1)) == (1 + (numchars a o ((i - o) - 1)))) && (((numchars a o (i - (o -1))) >= 0) && (((i - o) - 1) >= 0)))) && ((not (((v >= 56320) && (v <= 57343)))) => (((numchars a o ((i - o) + 1)) == (1 + (numchars a o (i - o)))) && ((numchars a o (i - o)) >= 0))))"
--
-- myTest2 = "len x = len y - 1"
-- myTest3 = "len x y z = len a b c - 1"
-- myTest4 = "len x y z = len a b (c - 1)"
-- myTest5 = "x >= -1"
-- myTest6 = "(bLength v) = if n > 0 then n else 0"
-- myTest7 = "(bLength v) = (if n > 0 then n else 0)"
-- myTest8 = "(bLength v) = (n > 0 ? n : 0)"
sa = "0"
sb = "x"
sc = "(x0 + y0 + z0) "
sd = "(x+ y * 1)"
se = "_|_ "
sf = "(1 + x + _|_)"
sg = "f(x,y,z)"
sh = "(f((x+1), (y * a * b - 1), _|_))"
si = "(2 + f((x+1), (y * a * b - 1), _|_))"
s0 = "true"
s1 = "false"
s2 = "v > 0"
s3 = "(0 < v && v < 100)"
s4 = "(x < v && v < y+10 && v < z)"
s6 = "[(v > 0)]"
s6' = "x"
s7' = "(x <=> y)"
s8' = "(x <=> a = b)"
s9' = "(x <=> (a <= b && b < c))"
s7 = "{ v: Int | [(v > 0)] }"
s8 = "x:{ v: Int | v > 0 } -> {v : Int | v >= x}"
s9 = "v = x+y"
s10 = "{v: Int | v = x + y}"
s11 = "x:{v:Int | true } -> {v:Int | true }"
s12 = "y : {v:Int | true } -> {v:Int | v = x }"
s13 = "x:{v:Int | true } -> y:{v:Int | true} -> {v:Int | v = x + y}"
s14 = "x:{v:a | true} -> y:{v:b | true } -> {v:a | (x < v && v < y) }"
s15 = "x:Int -> Bool"
s16 = "x:Int -> y:Int -> {v:Int | v = x + y}"
s17 = "a"
s18 = "x:a -> Bool"
s20 = "forall a . x:Int -> Bool"
s21 = "x:{v : GHC.Prim.Int# | true } -> {v : Int | true }"
r0 = (rr s0) :: Pred
r0' = (rr s0) :: [Refa]
r1 = (rr s1) :: [Refa]
e1, e2 :: Expr
e1 = rr "(k_1 + k_2)"
e2 = rr "k_1"
o1, o2, o3 :: FixResult Integer
o1 = rr "SAT "
o2 = rr "UNSAT [1, 2, 9,10]"
o3 = rr "UNSAT []"
-- sol1 = doParse solution1P "solution: k_5 := [0 <= VV_int]"
-- sol2 = doParse solution1P "solution: k_4 := [(0 <= VV_int)]"
b0, b1, b2, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13 :: BareType
b0 = rr "Int"
b1 = rr "x:{v:Int | true } -> y:{v:Int | true} -> {v:Int | v = x + y}"
b2 = rr "x:{v:Int | true } -> y:{v:Int | true} -> {v:Int | v = x - y}"
b4 = rr "forall a . x : a -> Bool"
b5 = rr "Int -> Int -> Int"
b6 = rr "(Int -> Int) -> Int"
b7 = rr "({v: Int | v > 10} -> Int) -> Int"
b8 = rr "(x:Int -> {v: Int | v > x}) -> {v: Int | v > 10}"
b9 = rr "x:Int -> {v: Int | v > x} -> {v: Int | v > 10}"
b10 = rr "[Int]"
b11 = rr "x:[Int] -> {v: Int | v > 10}"
b12 = rr "[Int] -> String"
b13 = rr "x:(Int, [Bool]) -> [(String, String)]"
-- b3 :: BareType
-- b3 = rr "x:Int -> y:Int -> {v:Bool | ((v is True) <=> x = y)}"
m1 = ["len :: [a] -> Int", "len (Nil) = 0", "len (Cons x xs) = 1 + len(xs)"]
m2 = ["tog :: LL a -> Int", "tog (Nil) = 100", "tog (Cons y ys) = 200"]
me1, me2 :: Measure.Measure BareType Symbol
me1 = (rr $ intercalate "\n" m1)
me2 = (rr $ intercalate "\n" m2)
-}