{-# 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

  -- * Lexer to add new tokens
  , lexer

  -- * Some Important keyword and parsers
  , reserved, reservedOp
  , parens  , brackets, angles, braces
  , semi    , comma
  , colon   , dcolon
  , whiteSpace
  , blanks
  , pairP
  , stringLiteral

  -- * Parsing basic entities

  --   fTyConP  -- Type constructors
  , lowerIdP    -- Lower-case identifiers
  , upperIdP    -- Upper-case identifiers
  , infixIdP    -- String Haskell infix Id
  , symbolP     -- Arbitrary Symbols
  , constantP   -- (Integer) Constants
  , integer     -- Integer
  , bindP       -- Binder (lowerIdP <* colon)
  , sortP       -- Sort
  , mkQual      -- constructing qualifiers
  , infixSymbolP -- parse infix symbols 

  -- * 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

  -- * Some Combinators
  , condIdP     --  condIdP  :: [Char] -> (Text -> Bool) -> Parser Text

  -- * Add a Location to a parsed value
  , locParserP
  , locLowerIdP
  , locUpperIdP

  -- * Getting a Fresh Integer while parsing
  , freshIntP

  -- * Parsing Function
  , doParse'
  , parseFromFile
  , remainderP

  -- * Utilities
  , isSmall
  , isNotReserved

  , initPState, PState (..)

  , Fixity(..), Assoc(..), addOperatorP

  -- * For testing
  , expr0P
  , dataFieldP
  , dataCtorP
  , dataDeclP

  ) where

import qualified Data.HashMap.Strict         as M
import qualified Data.HashSet                as S
import qualified Data.Text                   as T
import           Data.Maybe                  (fromJust, fromMaybe)
import           Text.Parsec       hiding (State)
import           Text.Parsec.Expr
import qualified Text.Parsec.Token           as Token
-- import           Text.Printf                 (printf)
import           GHC.Generics                (Generic)

import qualified Data.Char                   as Char -- (isUpper, isLower)
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.Visitor   (foldSort, mapSort)
import           Language.Fixpoint.Types hiding    (mapSort)
import           Text.PrettyPrint.HughesPJ         (text, nest, vcat, (<+>))

import Control.Monad.State

type Parser = ParsecT String Integer (State PState)
type ParserT u a = ParsecT String u (State PState) a

data PState = PState { PState -> OpTable
fixityTable :: OpTable
                     , PState -> [Fixity]
fixityOps   :: [Fixity]
                     , PState -> Maybe Expr
empList     :: Maybe Expr
                     , PState -> Maybe (Expr -> Expr)
singList    :: Maybe (Expr -> Expr)}


--------------------------------------------------------------------


emptyDef :: Monad m => Token.GenLanguageDef String a m
emptyDef :: GenLanguageDef String a m
emptyDef    = LanguageDef :: forall s u (m :: * -> *).
String
-> String
-> String
-> Bool
-> ParsecT s u m Char
-> ParsecT s u m Char
-> ParsecT s u m Char
-> ParsecT s u m Char
-> [String]
-> [String]
-> Bool
-> GenLanguageDef s u m
Token.LanguageDef
               { commentStart :: String
Token.commentStart   = String
""
               , commentEnd :: String
Token.commentEnd     = String
""
               , commentLine :: String
Token.commentLine    = String
""
               , nestedComments :: Bool
Token.nestedComments = Bool
True
               , identStart :: ParsecT String a m Char
Token.identStart     = ParsecT String a m Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
lower ParsecT String a m Char
-> ParsecT String a m Char -> ParsecT String a m Char
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Char -> ParsecT String a m Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
'_'             -- letter <|> char '_'
               , identLetter :: ParsecT String a m Char
Token.identLetter    = (Char -> Bool) -> ParsecT String a m Char
forall s (m :: * -> *) u.
Stream s m Char =>
(Char -> Bool) -> ParsecT s u m Char
satisfy (Char -> HashSet Char -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet Char
symChars)  -- alphaNum <|> oneOf "_"
               , opStart :: ParsecT String a m Char
Token.opStart        = GenLanguageDef String a m -> ParsecT String a m Char
forall s u (m :: * -> *).
GenLanguageDef s u m -> ParsecT s u m Char
Token.opLetter GenLanguageDef String a m
forall (m :: * -> *) a. Monad m => GenLanguageDef String a m
emptyDef
               , opLetter :: ParsecT String a m Char
Token.opLetter       = String -> ParsecT String a m Char
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m Char
oneOf String
":!#$%&*+./<=>?@\\^|-~'"
               , reservedOpNames :: [String]
Token.reservedOpNames= []
               , reservedNames :: [String]
Token.reservedNames  = []
               , caseSensitive :: Bool
Token.caseSensitive  = Bool
True
               }

languageDef :: Monad m => Token.GenLanguageDef String a m
languageDef :: GenLanguageDef String a m
languageDef =
  GenLanguageDef String a m
forall (m :: * -> *) a. Monad m => GenLanguageDef String a m
emptyDef { commentStart :: String
Token.commentStart    = String
"/* "
           , commentEnd :: String
Token.commentEnd      = String
" */"
           , commentLine :: String
Token.commentLine     = String
"//"
           , identStart :: ParsecT String a m Char
Token.identStart      = ParsecT String a m Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
lower ParsecT String a m Char
-> ParsecT String a m Char -> ParsecT String a m Char
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Char -> ParsecT String a m Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
'_'
           , identLetter :: ParsecT String a m Char
Token.identLetter     = ParsecT String a m Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
alphaNum ParsecT String a m Char
-> ParsecT String a m Char -> ParsecT String a m Char
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String -> ParsecT String a m Char
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m Char
oneOf String
"_"
           , reservedNames :: [String]
Token.reservedNames   = HashSet String -> [String]
forall a. HashSet a -> [a]
S.toList HashSet String
reservedNames
           , reservedOpNames :: [String]
Token.reservedOpNames =          [String]
reservedOpNames
           }

reservedNames :: S.HashSet String
reservedNames :: HashSet String
reservedNames = [String] -> HashSet String
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList
  [ -- reserved words used in fixpoint
    String
"SAT"
  , String
"UNSAT"
  , String
"true"
  , String
"false"
  , String
"mod"
  , String
"data"
  , String
"Bexp"
  -- , "True"
  -- , "Int"
  , String
"import"
  , String
"if", String
"then", String
"else"
  , String
"func"
  , String
"autorewrite"
  , String
"rewrite"

  -- reserved words used in liquid haskell
  , String
"forall"
  , String
"coerce"
  , String
"exists"
  , String
"module"
  , String
"spec"
  , String
"where"
  , String
"decrease"
  , String
"lazyvar"
  , String
"LIQUID"
  , String
"lazy"
  , String
"local"
  , String
"assert"
  , String
"assume"
  , String
"automatic-instances"
  , String
"autosize"
  , String
"axiomatize"
  , String
"bound"
  , String
"class"
  , String
"data"
  , String
"define"
  , String
"defined"
  , String
"embed"
  , String
"expression"
  , String
"import"
  , String
"include"
  , String
"infix"
  , String
"infixl"
  , String
"infixr"
  , String
"inline"
  , String
"instance"
  , String
"invariant"
  , String
"measure"
  , String
"newtype"
  , String
"predicate"
  , String
"qualif"
  , String
"reflect"
  , String
"type"
  , String
"using"
  , String
"with"
  , String
"in"
  ]

reservedOpNames :: [String]
reservedOpNames :: [String]
reservedOpNames =
  [ String
"+", String
"-", String
"*", String
"/", String
"\\", String
":"
  , String
"<", String
">", String
"<=", String
">=", String
"=", String
"!=" , String
"/="
  , String
"mod", String
"and", String
"or"
  --, "is"
  , String
"&&", String
"||"
  , String
"~", String
"=>", String
"==>", String
"<=>"
  , String
"->"
  , String
":="
  , String
"&", String
"^", String
"<<", String
">>", String
"--"
  , String
"?", String
"Bexp"
  , String
"'"
  , String
"_|_"
  , String
"|"
  , String
"<:"
  , String
"|-"
  , String
"::"
  , String
"."
  ]

lexer :: Monad m => Token.GenTokenParser String u m
lexer :: GenTokenParser String u m
lexer = GenLanguageDef String u m -> GenTokenParser String u m
forall s (m :: * -> *) u.
Stream s m Char =>
GenLanguageDef s u m -> GenTokenParser s u m
Token.makeTokenParser GenLanguageDef String u m
forall (m :: * -> *) a. Monad m => GenLanguageDef String a m
languageDef


reserved :: String -> Parser ()
reserved :: String -> Parser ()
reserved      = GenTokenParser String Integer (State PState) -> String -> Parser ()
forall s u (m :: * -> *).
GenTokenParser s u m -> String -> ParsecT s u m ()
Token.reserved      GenTokenParser String Integer (State PState)
forall (m :: * -> *) u. Monad m => GenTokenParser String u m
lexer

reservedOp :: String -> Parser ()
reservedOp :: String -> Parser ()
reservedOp    = GenTokenParser String Integer (State PState) -> String -> Parser ()
forall s u (m :: * -> *).
GenTokenParser s u m -> String -> ParsecT s u m ()
Token.reservedOp    GenTokenParser String Integer (State PState)
forall (m :: * -> *) u. Monad m => GenTokenParser String u m
lexer

parens, brackets, angles, braces :: ParserT u a -> ParserT u a
parens :: ParserT u a -> ParserT u a
parens        = GenTokenParser String u (State PState)
-> forall a.
   ParsecT String u (State PState) a
   -> ParsecT String u (State PState) a
forall s u (m :: * -> *).
GenTokenParser s u m
-> forall a. ParsecT s u m a -> ParsecT s u m a
Token.parens        GenTokenParser String u (State PState)
forall (m :: * -> *) u. Monad m => GenTokenParser String u m
lexer
brackets :: ParserT u a -> ParserT u a
brackets      = GenTokenParser String u (State PState)
-> forall a.
   ParsecT String u (State PState) a
   -> ParsecT String u (State PState) a
forall s u (m :: * -> *).
GenTokenParser s u m
-> forall a. ParsecT s u m a -> ParsecT s u m a
Token.brackets      GenTokenParser String u (State PState)
forall (m :: * -> *) u. Monad m => GenTokenParser String u m
lexer
angles :: ParserT u a -> ParserT u a
angles        = GenTokenParser String u (State PState)
-> forall a.
   ParsecT String u (State PState) a
   -> ParsecT String u (State PState) a
forall s u (m :: * -> *).
GenTokenParser s u m
-> forall a. ParsecT s u m a -> ParsecT s u m a
Token.angles        GenTokenParser String u (State PState)
forall (m :: * -> *) u. Monad m => GenTokenParser String u m
lexer
braces :: ParserT u a -> ParserT u a
braces        = GenTokenParser String u (State PState)
-> forall a.
   ParsecT String u (State PState) a
   -> ParsecT String u (State PState) a
forall s u (m :: * -> *).
GenTokenParser s u m
-> forall a. ParsecT s u m a -> ParsecT s u m a
Token.braces        GenTokenParser String u (State PState)
forall (m :: * -> *) u. Monad m => GenTokenParser String u m
lexer

sbraces :: Parser a -> Parser a 
sbraces :: Parser a -> Parser a
sbraces Parser a
pp   = Parser a -> Parser a
forall u a. ParserT u a -> ParserT u a
braces (Parser a -> Parser a) -> Parser a -> Parser a
forall a b. (a -> b) -> a -> b
$ (Parser ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces Parser () -> Parser a -> Parser a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser a
pp Parser a -> Parser () -> Parser a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces)

semi, colon, comma, dot, stringLiteral :: Parser String
semi :: Parser String
semi          = GenTokenParser String Integer (State PState) -> Parser String
forall s u (m :: * -> *).
GenTokenParser s u m -> ParsecT s u m String
Token.semi          GenTokenParser String Integer (State PState)
forall (m :: * -> *) u. Monad m => GenTokenParser String u m
lexer
colon :: Parser String
colon         = GenTokenParser String Integer (State PState) -> Parser String
forall s u (m :: * -> *).
GenTokenParser s u m -> ParsecT s u m String
Token.colon         GenTokenParser String Integer (State PState)
forall (m :: * -> *) u. Monad m => GenTokenParser String u m
lexer
comma :: Parser String
comma         = GenTokenParser String Integer (State PState) -> Parser String
forall s u (m :: * -> *).
GenTokenParser s u m -> ParsecT s u m String
Token.comma         GenTokenParser String Integer (State PState)
forall (m :: * -> *) u. Monad m => GenTokenParser String u m
lexer
dot :: Parser String
dot           = GenTokenParser String Integer (State PState) -> Parser String
forall s u (m :: * -> *).
GenTokenParser s u m -> ParsecT s u m String
Token.dot           GenTokenParser String Integer (State PState)
forall (m :: * -> *) u. Monad m => GenTokenParser String u m
lexer
stringLiteral :: Parser String
stringLiteral = GenTokenParser String Integer (State PState) -> Parser String
forall s u (m :: * -> *).
GenTokenParser s u m -> ParsecT s u m String
Token.stringLiteral GenTokenParser String Integer (State PState)
forall (m :: * -> *) u. Monad m => GenTokenParser String u m
lexer

whiteSpace :: Parser ()
whiteSpace :: Parser ()
whiteSpace    = GenTokenParser String Integer (State PState) -> Parser ()
forall s u (m :: * -> *). GenTokenParser s u m -> ParsecT s u m ()
Token.whiteSpace    GenTokenParser String Integer (State PState)
forall (m :: * -> *) u. Monad m => GenTokenParser String u m
lexer

double :: Parser Double
double :: Parser Double
double        = GenTokenParser String Integer (State PState) -> Parser Double
forall s u (m :: * -> *).
GenTokenParser s u m -> ParsecT s u m Double
Token.float         GenTokenParser String Integer (State PState)
forall (m :: * -> *) u. Monad m => GenTokenParser String u m
lexer
-- integer       = Token.integer       lexer

-- identifier :: Parser String
-- identifier = Token.identifier lexer

-- TODO:AZ: pretty sure there is already a whitespace eater in parsec,
blanks :: Parser String
blanks :: Parser String
blanks  = ParsecT String Integer (State PState) Char -> Parser String
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ((Char -> Bool) -> ParsecT String Integer (State PState) Char
forall s (m :: * -> *) u.
Stream s m Char =>
(Char -> Bool) -> ParsecT s u m Char
satisfy (Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Char
' ', Char
'\t']))

-- | Integer
integer :: Parser Integer
integer :: Parser Integer
integer = GenTokenParser String Integer (State PState) -> Parser Integer
forall s u (m :: * -> *).
GenTokenParser s u m -> ParsecT s u m Integer
Token.natural GenTokenParser String Integer (State PState)
forall (m :: * -> *) u. Monad m => GenTokenParser String u m
lexer Parser Integer -> Parser () -> Parser Integer
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces

--  try (char '-' >> (negate <$> posInteger))
--       <|> posInteger
-- posInteger :: Parser Integer
-- posInteger = toI <$> (many1 digit <* spaces)
--  where
--    toI :: String -> Integer
--    toI = read

----------------------------------------------------------------
------------------------- Expressions --------------------------
----------------------------------------------------------------

locParserP :: Parser a -> Parser (Located a)
locParserP :: Parser a -> Parser (Located a)
locParserP Parser a
p = do SourcePos
l1 <- ParsecT String Integer (State PState) SourcePos
forall (m :: * -> *) s u. Monad m => ParsecT s u m SourcePos
getPosition
                  a
x  <- Parser a
p
                  SourcePos
l2 <- ParsecT String Integer (State PState) SourcePos
forall (m :: * -> *) s u. Monad m => ParsecT s u m SourcePos
getPosition
                  Located a -> Parser (Located a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Located a -> Parser (Located a))
-> Located a -> Parser (Located a)
forall a b. (a -> b) -> a -> b
$ SourcePos -> SourcePos -> a -> Located a
forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l1 SourcePos
l2 a
x


-- FIXME: we (LH) rely on this parser being dumb and *not* consuming trailing
-- whitespace, in order to avoid some parsers spanning multiple lines..

condIdP  :: Parser Char -> S.HashSet Char -> (String -> Bool) -> Parser Symbol
condIdP :: ParsecT String Integer (State PState) Char
-> HashSet Char -> (String -> Bool) -> Parser Symbol
condIdP ParsecT String Integer (State PState) Char
initP HashSet Char
okChars String -> Bool
p
  = do Char
c    <- ParsecT String Integer (State PState) Char
initP 
       String
cs   <- ParsecT String Integer (State PState) Char -> Parser String
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ((Char -> Bool) -> ParsecT String Integer (State PState) Char
forall s (m :: * -> *) u.
Stream s m Char =>
(Char -> Bool) -> ParsecT s u m Char
satisfy (Char -> HashSet Char -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet Char
okChars))
       Parser String
blanks
       let s :: String
s = Char
cChar -> String -> String
forall a. a -> [a] -> [a]
:String
cs
       if String -> Bool
p String
s then Symbol -> Parser Symbol
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol String
s) else Parser Symbol
forall s u (m :: * -> *) a. ParsecT s u m a
parserZero

-- upperIdP :: Parser Symbol
-- upperIdP = do
--  c  <- upper
--  cs <- many (satisfy (`S.member` symChars))
--  blanks
--  return (symbol $ c:cs)
-- lowerIdP = do
  -- c  <- satisfy (\c -> isLower c || c == '_' )
  -- cs <- many (satisfy (`S.member` symChars))
  -- blanks
  -- return (symbol $ c:cs)

-- TODO:RJ we really _should_ just use the below, but we cannot,
-- because 'identifier' also chomps newlines which then make
-- it hard to parse stuff like: "measure foo :: a -> b \n foo x = y"
-- as the type parser thinks 'b \n foo` is a type. Sigh.
-- lowerIdP :: Parser Symbol
-- lowerIdP = symbol <$> (identifier <* blanks)

upperIdP :: Parser Symbol
upperIdP :: Parser Symbol
upperIdP  = ParsecT String Integer (State PState) Char
-> HashSet Char -> (String -> Bool) -> Parser Symbol
condIdP ParsecT String Integer (State PState) Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
upper                  HashSet Char
symChars (Bool -> String -> Bool
forall a b. a -> b -> a
const Bool
True)

lowerIdP :: Parser Symbol
lowerIdP :: Parser Symbol
lowerIdP  = ParsecT String Integer (State PState) Char
-> HashSet Char -> (String -> Bool) -> Parser Symbol
condIdP (ParsecT String Integer (State PState) Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
lower ParsecT String Integer (State PState) Char
-> ParsecT String Integer (State PState) Char
-> ParsecT String Integer (State PState) Char
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Char -> ParsecT String Integer (State PState) Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
'_')   HashSet Char
symChars String -> Bool
isNotReserved

symCharsP :: Parser Symbol
symCharsP :: Parser Symbol
symCharsP = ParsecT String Integer (State PState) Char
-> HashSet Char -> (String -> Bool) -> Parser Symbol
condIdP (ParsecT String Integer (State PState) Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
letter ParsecT String Integer (State PState) Char
-> ParsecT String Integer (State PState) Char
-> ParsecT String Integer (State PState) Char
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Char -> ParsecT String Integer (State PState) Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
'_')  HashSet Char
symChars String -> Bool
isNotReserved

isNotReserved :: String -> Bool
isNotReserved :: String -> Bool
isNotReserved String
s = Bool -> Bool
not (String
s String -> HashSet String -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet String
reservedNames)

-- (&&&) :: (a -> Bool) -> (a -> Bool) -> a -> Bool
-- f &&& g = \x -> f x && g x
-- | String Haskell infix Id
infixIdP :: Parser String
infixIdP :: Parser String
infixIdP = ParsecT String Integer (State PState) Char -> Parser String
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ((Char -> Bool) -> ParsecT String Integer (State PState) Char
forall s (m :: * -> *) u.
Stream s m Char =>
(Char -> Bool) -> ParsecT s u m Char
satisfy (Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Char
' ', Char
'.']))

isSmall :: Char -> Bool
isSmall :: Char -> Bool
isSmall Char
c = Char -> Bool
Char.isLower Char
c Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'_'

locSymbolP, locLowerIdP, locUpperIdP :: Parser LocSymbol
locLowerIdP :: Parser LocSymbol
locLowerIdP = Parser Symbol -> Parser LocSymbol
forall a. Parser a -> Parser (Located a)
locParserP Parser Symbol
lowerIdP
locUpperIdP :: Parser LocSymbol
locUpperIdP = Parser Symbol -> Parser LocSymbol
forall a. Parser a -> Parser (Located a)
locParserP Parser Symbol
upperIdP
locSymbolP :: Parser LocSymbol
locSymbolP  = Parser Symbol -> Parser LocSymbol
forall a. Parser a -> Parser (Located a)
locParserP Parser Symbol
symbolP

-- | Arbitrary Symbols
symbolP :: Parser Symbol
symbolP :: Parser Symbol
symbolP = Symbol -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (Symbol -> Symbol) -> Parser Symbol -> Parser Symbol
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Symbol
symCharsP

-- | (Integer) Constants
constantP :: Parser Constant
constantP :: Parser Constant
constantP =  Parser Constant -> Parser Constant
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try (Double -> Constant
R (Double -> Constant) -> Parser Double -> Parser Constant
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Double
double)
         Parser Constant -> Parser Constant -> Parser Constant
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Integer -> Constant
I (Integer -> Constant) -> Parser Integer -> Parser Constant
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Integer
integer


symconstP :: Parser SymConst
symconstP :: Parser SymConst
symconstP = Text -> SymConst
SL (Text -> SymConst) -> (String -> Text) -> String -> SymConst
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
T.pack (String -> SymConst) -> Parser String -> Parser SymConst
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser String
stringLiteral

expr0P :: Parser Expr
expr0P :: Parser Expr
expr0P
  =  Parser Expr
trueP
 Parser Expr -> Parser Expr -> Parser Expr
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser Expr
falseP
 Parser Expr -> Parser Expr -> Parser Expr
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Expr -> Expr -> Expr -> Expr) -> Parser Expr -> Parser Expr
forall a. (Expr -> a -> a -> a) -> Parser a -> Parser a
fastIfP Expr -> Expr -> Expr -> Expr
EIte Parser Expr
exprP
 Parser Expr -> Parser Expr -> Parser Expr
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser Expr -> Parser Expr
coerceP Parser Expr
exprP
 Parser Expr -> Parser Expr -> Parser Expr
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (SymConst -> Expr
ESym (SymConst -> Expr) -> Parser SymConst -> Parser Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser SymConst
symconstP)
 Parser Expr -> Parser Expr -> Parser Expr
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Constant -> Expr
ECon (Constant -> Expr) -> Parser Constant -> Parser Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Constant
constantP)
 Parser Expr -> Parser Expr -> Parser Expr
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (String -> Parser ()
reservedOp String
"_|_" Parser () -> Parser Expr -> Parser Expr
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Expr -> Parser Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
EBot)
 Parser Expr -> Parser Expr -> Parser Expr
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser Expr
lamP
 Parser Expr -> Parser Expr -> Parser Expr
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser Expr -> Parser Expr
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try Parser Expr
tupleP
  -- TODO:AZ get rid of these try, after the rest
 Parser Expr -> Parser Expr -> Parser Expr
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser Expr -> Parser Expr
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try (Parser Expr -> Parser Expr
forall u a. ParserT u a -> ParserT u a
parens Parser Expr
exprP)
 Parser Expr -> Parser Expr -> Parser Expr
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (String -> Parser ()
reserved String
"[]" Parser () -> Parser Expr -> Parser Expr
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Expr
emptyListP)
 Parser Expr -> Parser Expr -> Parser Expr
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser Expr -> Parser Expr
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try (Parser Expr -> Parser Expr
forall u a. ParserT u a -> ParserT u a
brackets Parser Expr
exprP Parser Expr -> (Expr -> Parser Expr) -> Parser Expr
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Expr -> Parser Expr
singletonListP) 
 Parser Expr -> Parser Expr -> Parser Expr
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser Expr -> Parser Expr
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try (Parser Expr -> Parser Expr
forall u a. ParserT u a -> ParserT u a
parens Parser Expr
exprCastP)
 Parser Expr -> Parser Expr -> Parser Expr
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Symbol -> Expr
charsExpr (Symbol -> Expr) -> Parser Symbol -> Parser Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Symbol
symCharsP)

emptyListP :: Parser Expr
emptyListP :: Parser Expr
emptyListP = do 
  Maybe Expr
e <- PState -> Maybe Expr
empList (PState -> Maybe Expr)
-> ParsecT String Integer (State PState) PState
-> ParsecT String Integer (State PState) (Maybe Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT String Integer (State PState) PState
forall s (m :: * -> *). MonadState s m => m s
get 
  case Maybe Expr
e of 
    Maybe Expr
Nothing -> String -> Parser Expr
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"No parsing support for empty lists"
    Just Expr
s  -> Expr -> Parser Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
s 

singletonListP :: Expr -> Parser Expr 
singletonListP :: Expr -> Parser Expr
singletonListP Expr
e = do 
  Maybe (Expr -> Expr)
f <- PState -> Maybe (Expr -> Expr)
singList (PState -> Maybe (Expr -> Expr))
-> ParsecT String Integer (State PState) PState
-> ParsecT String Integer (State PState) (Maybe (Expr -> Expr))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT String Integer (State PState) PState
forall s (m :: * -> *). MonadState s m => m s
get
  case Maybe (Expr -> Expr)
f of 
    Maybe (Expr -> Expr)
Nothing -> String -> Parser Expr
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"No parsing support for singleton lists"
    Just Expr -> Expr
s  -> Expr -> Parser Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Parser Expr) -> Expr -> Parser Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
s Expr
e 

exprCastP :: Parser Expr
exprCastP :: Parser Expr
exprCastP
  = do Expr
e  <- Parser Expr
exprP
       (Parser String -> Parser String
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try Parser String
dcolon) Parser String -> Parser String -> Parser String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser String
colon
       Sort
so <- Parser Sort
sortP
       Expr -> Parser Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Parser Expr) -> Expr -> Parser Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Sort -> Expr
ECst Expr
e Sort
so

charsExpr :: Symbol -> Expr
charsExpr :: Symbol -> Expr
charsExpr Symbol
cs
  | Char -> Bool
isSmall (Symbol -> Char
headSym Symbol
cs) = Symbol -> Expr
forall a. Expression a => a -> Expr
expr Symbol
cs
  | Bool
otherwise            = Symbol -> Expr
EVar Symbol
cs

fastIfP :: (Expr -> a -> a -> a) -> Parser a -> Parser a
fastIfP :: (Expr -> a -> a -> a) -> Parser a -> Parser a
fastIfP Expr -> a -> a -> a
f Parser a
bodyP
  = do String -> Parser ()
reserved String
"if"
       Expr
p <- Parser Expr
predP
       String -> Parser ()
reserved String
"then"
       a
b1 <- Parser a
bodyP
       String -> Parser ()
reserved String
"else"
       a
b2 <- Parser a
bodyP
       a -> Parser a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Parser a) -> a -> Parser a
forall a b. (a -> b) -> a -> b
$ Expr -> a -> a -> a
f Expr
p a
b1 a
b2

coerceP :: Parser Expr -> Parser Expr
coerceP :: Parser Expr -> Parser Expr
coerceP Parser Expr
p = do
  String -> Parser ()
reserved String
"coerce"
  (Sort
s, Sort
t) <- ParserT Integer (Sort, Sort) -> ParserT Integer (Sort, Sort)
forall u a. ParserT u a -> ParserT u a
parens (Parser Sort
-> Parser () -> Parser Sort -> ParserT Integer (Sort, Sort)
forall a z b. Parser a -> Parser z -> Parser b -> Parser (a, b)
pairP Parser Sort
sortP (String -> Parser ()
reservedOp String
"~") Parser Sort
sortP)
  Expr
e      <- Parser Expr
p
  Expr -> Parser Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Parser Expr) -> Expr -> Parser Expr
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Expr -> Expr
ECoerc Sort
s Sort
t Expr
e



{-
qmIfP f bodyP
  = parens $ do
      p  <- predP
      reserved "?"
      b1 <- bodyP
      colon
      b2 <- bodyP
      return $ f p b1 b2
-}

-- | Used as input to @Text.Parsec.Expr.buildExpressionParser@ to create @exprP@
expr1P :: Parser Expr
expr1P :: Parser Expr
expr1P
  =  Parser Expr -> Parser Expr
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try Parser Expr
funAppP
 Parser Expr -> Parser Expr -> Parser Expr
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser Expr
expr0P

-- | Expressions
exprP :: Parser Expr
exprP :: Parser Expr
exprP = (PState -> OpTable
fixityTable (PState -> OpTable)
-> ParsecT String Integer (State PState) PState
-> ParsecT String Integer (State PState) OpTable
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT String Integer (State PState) PState
forall s (m :: * -> *). MonadState s m => m s
get) ParsecT String Integer (State PState) OpTable
-> (OpTable -> Parser Expr) -> Parser Expr
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (OpTable -> Parser Expr -> Parser Expr
forall s (m :: * -> *) t u a.
Stream s m t =>
OperatorTable s u m a -> ParsecT s u m a -> ParsecT s u m a
`buildExpressionParser` Parser Expr
expr1P)

data Fixity
  = FInfix   {Fixity -> Maybe Int
fpred :: Maybe Int, Fixity -> String
fname :: String, Fixity -> Maybe (Expr -> Expr -> Expr)
fop2 :: Maybe (Expr -> Expr -> Expr), Fixity -> Assoc
fassoc :: Assoc}
  | FPrefix  {fpred :: Maybe Int, fname :: String, Fixity -> Maybe (Expr -> Expr)
fop1 :: Maybe (Expr -> Expr)}
  | FPostfix {fpred :: Maybe Int, fname :: String, fop1 :: Maybe (Expr -> Expr)}


-- Invariant : OpTable has 10 elements
type OpTable = OperatorTable String Integer (State PState) Expr

addOperatorP :: Fixity -> Parser ()
addOperatorP :: Fixity -> Parser ()
addOperatorP Fixity
op
  = (PState -> PState) -> Parser ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((PState -> PState) -> Parser ())
-> (PState -> PState) -> Parser ()
forall a b. (a -> b) -> a -> b
$ \PState
s -> PState
s{ fixityTable :: OpTable
fixityTable =  Fixity -> OpTable -> OpTable
addOperator Fixity
op (PState -> OpTable
fixityTable PState
s)
                    , fixityOps :: [Fixity]
fixityOps   =  Fixity
opFixity -> [Fixity] -> [Fixity]
forall a. a -> [a] -> [a]
:PState -> [Fixity]
fixityOps PState
s 
                    }

infixSymbolP :: Parser Symbol
infixSymbolP :: Parser Symbol
infixSymbolP = do 
  [String]
ops <- PState -> [String]
infixOps (PState -> [String])
-> ParsecT String Integer (State PState) PState
-> ParsecT String Integer (State PState) [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT String Integer (State PState) PState
forall s (m :: * -> *). MonadState s m => m s
get 
  [Parser Symbol] -> Parser Symbol
forall s (m :: * -> *) t u a.
Stream s m t =>
[ParsecT s u m a] -> ParsecT s u m a
choice (String -> Parser Symbol
reserved' (String -> Parser Symbol) -> [String] -> [Parser Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [String]
ops)
  where 
    infixOps :: PState -> [String]
infixOps PState
st = [String
s | FInfix Maybe Int
_ String
s Maybe (Expr -> Expr -> Expr)
_ Assoc
_ <- PState -> [Fixity]
fixityOps PState
st]
    reserved' :: String -> Parser Symbol
reserved' String
x = String -> Parser ()
reserved String
x Parser () -> Parser Symbol -> Parser Symbol
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Symbol -> Parser Symbol
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol String
x) 

addOperator :: Fixity -> OpTable -> OpTable
addOperator :: Fixity -> OpTable -> OpTable
addOperator (FInfix Maybe Int
p String
x Maybe (Expr -> Expr -> Expr)
f Assoc
assoc) OpTable
ops
 = Int
-> Operator String Integer (State PState) Expr
-> OpTable
-> OpTable
insertOperator (Maybe Int -> Int
makePrec Maybe Int
p) (ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
-> Assoc -> Operator String Integer (State PState) Expr
forall s u (m :: * -> *) a.
ParsecT s u m (a -> a -> a) -> Assoc -> Operator s u m a
Infix (String -> Parser ()
reservedOp String
x Parser ()
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Maybe (Expr -> Expr -> Expr) -> Expr -> Expr -> Expr
makeInfixFun String
x Maybe (Expr -> Expr -> Expr)
f)) Assoc
assoc) OpTable
ops
addOperator (FPrefix Maybe Int
p String
x Maybe (Expr -> Expr)
f) OpTable
ops
 = Int
-> Operator String Integer (State PState) Expr
-> OpTable
-> OpTable
insertOperator (Maybe Int -> Int
makePrec Maybe Int
p) (ParsecT String Integer (State PState) (Expr -> Expr)
-> Operator String Integer (State PState) Expr
forall s u (m :: * -> *) a.
ParsecT s u m (a -> a) -> Operator s u m a
Prefix (String -> Parser ()
reservedOp String
x Parser ()
-> ParsecT String Integer (State PState) (Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Maybe (Expr -> Expr) -> Expr -> Expr
makePrefixFun String
x Maybe (Expr -> Expr)
f))) OpTable
ops
addOperator (FPostfix Maybe Int
p String
x Maybe (Expr -> Expr)
f) OpTable
ops
 = Int
-> Operator String Integer (State PState) Expr
-> OpTable
-> OpTable
insertOperator (Maybe Int -> Int
makePrec Maybe Int
p) (ParsecT String Integer (State PState) (Expr -> Expr)
-> Operator String Integer (State PState) Expr
forall s u (m :: * -> *) a.
ParsecT s u m (a -> a) -> Operator s u m a
Postfix (String -> Parser ()
reservedOp String
x Parser ()
-> ParsecT String Integer (State PState) (Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Maybe (Expr -> Expr) -> Expr -> Expr
makePrefixFun String
x Maybe (Expr -> Expr)
f))) OpTable
ops

makePrec :: Maybe Int -> Int
makePrec :: Maybe Int -> Int
makePrec = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
9

makeInfixFun :: String -> Maybe (Expr -> Expr -> Expr) -> Expr -> Expr -> Expr
makeInfixFun :: String -> Maybe (Expr -> Expr -> Expr) -> Expr -> Expr -> Expr
makeInfixFun String
x = (Expr -> Expr -> Expr)
-> Maybe (Expr -> Expr -> Expr) -> Expr -> Expr -> Expr
forall a. a -> Maybe a -> a
fromMaybe (\Expr
e1 Expr
e2 -> Expr -> Expr -> Expr
EApp (Expr -> Expr -> Expr
EApp (Symbol -> Expr
EVar (Symbol -> Expr) -> Symbol -> Expr
forall a b. (a -> b) -> a -> b
$ String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol String
x) Expr
e1) Expr
e2)

makePrefixFun :: String -> Maybe (Expr -> Expr) -> Expr -> Expr
makePrefixFun :: String -> Maybe (Expr -> Expr) -> Expr -> Expr
makePrefixFun String
x = (Expr -> Expr) -> Maybe (Expr -> Expr) -> Expr -> Expr
forall a. a -> Maybe a -> a
fromMaybe (Expr -> Expr -> Expr
EApp (Symbol -> Expr
EVar (Symbol -> Expr) -> Symbol -> Expr
forall a b. (a -> b) -> a -> b
$ String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol String
x))

insertOperator :: Int -> Operator String Integer (State PState) Expr -> OpTable -> OpTable
insertOperator :: Int
-> Operator String Integer (State PState) Expr
-> OpTable
-> OpTable
insertOperator Int
i Operator String Integer (State PState) Expr
op = Int -> OpTable -> OpTable
forall t. (Eq t, Num t) => t -> OpTable -> OpTable
go (Int
9 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
i) 
  where
    go :: t -> OpTable -> OpTable
go t
_ []         = Error -> OpTable
forall a. Error -> a
die (Error -> OpTable) -> Error -> OpTable
forall a b. (a -> b) -> a -> b
$ SrcSpan -> Doc -> Error
err SrcSpan
dummySpan (String -> Doc
text String
"insertOperator on empty ops")
    go t
0 ([Operator String Integer (State PState) Expr]
xs:OpTable
xss)   = ([Operator String Integer (State PState) Expr]
xs [Operator String Integer (State PState) Expr]
-> [Operator String Integer (State PState) Expr]
-> [Operator String Integer (State PState) Expr]
forall a. [a] -> [a] -> [a]
++ [Operator String Integer (State PState) Expr
op]) [Operator String Integer (State PState) Expr] -> OpTable -> OpTable
forall a. a -> [a] -> [a]
: OpTable
xss
    go t
i ([Operator String Integer (State PState) Expr]
xs:OpTable
xss)   = [Operator String Integer (State PState) Expr]
xs [Operator String Integer (State PState) Expr] -> OpTable -> OpTable
forall a. a -> [a] -> [a]
: t -> OpTable -> OpTable
go (t
i t -> t -> t
forall a. Num a => a -> a -> a
- t
1) OpTable
xss

initOpTable :: OpTable
initOpTable :: OpTable
initOpTable = Int -> [Operator String Integer (State PState) Expr] -> OpTable
forall a. Int -> a -> [a]
replicate Int
10 [] 

bops :: Maybe Expr -> OpTable
bops :: Maybe Expr -> OpTable
bops Maybe Expr
cmpFun = (OpTable -> Fixity -> OpTable) -> OpTable -> [Fixity] -> OpTable
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((Fixity -> OpTable -> OpTable) -> OpTable -> Fixity -> OpTable
forall a b c. (a -> b -> c) -> b -> a -> c
flip Fixity -> OpTable -> OpTable
addOperator) OpTable
initOpTable [Fixity]
buildinOps
  where
-- Build in Haskell ops https://www.haskell.org/onlinereport/decls.html#fixity
    buildinOps :: [Fixity]
buildinOps = [ Maybe Int -> String -> Maybe (Expr -> Expr) -> Fixity
FPrefix (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
9) String
"-"   ((Expr -> Expr) -> Maybe (Expr -> Expr)
forall a. a -> Maybe a
Just Expr -> Expr
ENeg)
                 , Maybe Int
-> String -> Maybe (Expr -> Expr -> Expr) -> Assoc -> Fixity
FInfix  (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
7) String
"*"   ((Expr -> Expr -> Expr) -> Maybe (Expr -> Expr -> Expr)
forall a. a -> Maybe a
Just ((Expr -> Expr -> Expr) -> Maybe (Expr -> Expr -> Expr))
-> (Expr -> Expr -> Expr) -> Maybe (Expr -> Expr -> Expr)
forall a b. (a -> b) -> a -> b
$ Bop -> Expr -> Expr -> Expr
EBin Bop
Times) Assoc
AssocLeft
                 , Maybe Int
-> String -> Maybe (Expr -> Expr -> Expr) -> Assoc -> Fixity
FInfix  (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
7) String
"/"   ((Expr -> Expr -> Expr) -> Maybe (Expr -> Expr -> Expr)
forall a. a -> Maybe a
Just ((Expr -> Expr -> Expr) -> Maybe (Expr -> Expr -> Expr))
-> (Expr -> Expr -> Expr) -> Maybe (Expr -> Expr -> Expr)
forall a b. (a -> b) -> a -> b
$ Bop -> Expr -> Expr -> Expr
EBin Bop
Div)   Assoc
AssocLeft
                 , Maybe Int
-> String -> Maybe (Expr -> Expr -> Expr) -> Assoc -> Fixity
FInfix  (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
6) String
"-"   ((Expr -> Expr -> Expr) -> Maybe (Expr -> Expr -> Expr)
forall a. a -> Maybe a
Just ((Expr -> Expr -> Expr) -> Maybe (Expr -> Expr -> Expr))
-> (Expr -> Expr -> Expr) -> Maybe (Expr -> Expr -> Expr)
forall a b. (a -> b) -> a -> b
$ Bop -> Expr -> Expr -> Expr
EBin Bop
Minus) Assoc
AssocLeft
                 , Maybe Int
-> String -> Maybe (Expr -> Expr -> Expr) -> Assoc -> Fixity
FInfix  (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
6) String
"+"   ((Expr -> Expr -> Expr) -> Maybe (Expr -> Expr -> Expr)
forall a. a -> Maybe a
Just ((Expr -> Expr -> Expr) -> Maybe (Expr -> Expr -> Expr))
-> (Expr -> Expr -> Expr) -> Maybe (Expr -> Expr -> Expr)
forall a b. (a -> b) -> a -> b
$ Bop -> Expr -> Expr -> Expr
EBin Bop
Plus)  Assoc
AssocLeft
                 , Maybe Int
-> String -> Maybe (Expr -> Expr -> Expr) -> Assoc -> Fixity
FInfix  (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
5) String
"mod" ((Expr -> Expr -> Expr) -> Maybe (Expr -> Expr -> Expr)
forall a. a -> Maybe a
Just ((Expr -> Expr -> Expr) -> Maybe (Expr -> Expr -> Expr))
-> (Expr -> Expr -> Expr) -> Maybe (Expr -> Expr -> Expr)
forall a b. (a -> b) -> a -> b
$ Bop -> Expr -> Expr -> Expr
EBin Bop
Mod)   Assoc
AssocLeft -- Haskell gives mod 7
                 , Maybe Int
-> String -> Maybe (Expr -> Expr -> Expr) -> Assoc -> Fixity
FInfix  (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
9) String
"."   Maybe (Expr -> Expr -> Expr)
applyCompose        Assoc
AssocRight
                 ]
    applyCompose :: Maybe (Expr -> Expr -> Expr)
applyCompose = (\Expr
f Expr
x Expr
y -> (Expr
f Expr -> [Expr] -> Expr
`eApps` [Expr
x,Expr
y])) (Expr -> Expr -> Expr -> Expr)
-> Maybe Expr -> Maybe (Expr -> Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Expr
cmpFun

-- | Function Applications
funAppP :: Parser Expr
funAppP :: Parser Expr
funAppP            =  Parser Expr
litP Parser Expr -> Parser Expr -> Parser Expr
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser Expr
exprFunP Parser Expr -> Parser Expr -> Parser Expr
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser Expr
simpleAppP
  where
    exprFunP :: Parser Expr
exprFunP = LocSymbol -> [Expr] -> Expr
mkEApp (LocSymbol -> [Expr] -> Expr)
-> Parser LocSymbol
-> ParsecT String Integer (State PState) ([Expr] -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser LocSymbol
funSymbolP ParsecT String Integer (State PState) ([Expr] -> Expr)
-> ParsecT String Integer (State PState) [Expr] -> Parser Expr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT String Integer (State PState) [Expr]
funRhsP
    funRhsP :: ParsecT String Integer (State PState) [Expr]
funRhsP  =  Parser Expr
-> Parser String -> ParsecT String Integer (State PState) [Expr]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy1 Parser Expr
expr0P Parser String
blanks
            ParsecT String Integer (State PState) [Expr]
-> ParsecT String Integer (State PState) [Expr]
-> ParsecT String Integer (State PState) [Expr]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT String Integer (State PState) [Expr]
-> ParsecT String Integer (State PState) [Expr]
forall u a. ParserT u a -> ParserT u a
parens ParsecT String Integer (State PState) [Expr]
innerP
    innerP :: ParsecT String Integer (State PState) [Expr]
innerP   = ParsecT String Integer (State PState) [Expr]
-> ParsecT String Integer (State PState) [Expr]
forall u a. ParserT u a -> ParserT u a
brackets (Parser Expr
-> Parser String -> ParsecT String Integer (State PState) [Expr]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy Parser Expr
exprP Parser String
semi)

    -- TODO:AZ the parens here should be superfluous, but it hits an infinite loop if removed
    simpleAppP :: Parser Expr
simpleAppP     = Expr -> Expr -> Expr
EApp (Expr -> Expr -> Expr)
-> Parser Expr
-> ParsecT String Integer (State PState) (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Expr -> Parser Expr
forall u a. ParserT u a -> ParserT u a
parens Parser Expr
exprP ParsecT String Integer (State PState) (Expr -> Expr)
-> Parser Expr -> Parser Expr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Expr -> Parser Expr
forall u a. ParserT u a -> ParserT u a
parens Parser Expr
exprP
    funSymbolP :: Parser LocSymbol
funSymbolP     = Parser Symbol -> Parser LocSymbol
forall a. Parser a -> Parser (Located a)
locParserP Parser Symbol
symbolP


tupleP :: Parser Expr
tupleP :: Parser Expr
tupleP = do
  let tp :: ParserT Integer (Expr, [Expr])
tp = ParserT Integer (Expr, [Expr]) -> ParserT Integer (Expr, [Expr])
forall u a. ParserT u a -> ParserT u a
parens (Parser Expr
-> Parser String
-> ParsecT String Integer (State PState) [Expr]
-> ParserT Integer (Expr, [Expr])
forall a z b. Parser a -> Parser z -> Parser b -> Parser (a, b)
pairP Parser Expr
exprP Parser String
comma (Parser Expr
-> Parser String -> ParsecT String Integer (State PState) [Expr]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy1 Parser Expr
exprP Parser String
comma))
  Loc SourcePos
l1 SourcePos
l2 (Expr
first, [Expr]
rest) <- ParserT Integer (Expr, [Expr]) -> Parser (Located (Expr, [Expr]))
forall a. Parser a -> Parser (Located a)
locParserP ParserT Integer (Expr, [Expr])
tp
  let cons :: Symbol
cons = String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String -> Symbol) -> String -> Symbol
forall a b. (a -> b) -> a -> b
$ String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> Char -> String
forall a. Int -> a -> [a]
replicate ([Expr] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
rest) Char
',' String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
  Expr -> Parser Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Parser Expr) -> Expr -> Parser Expr
forall a b. (a -> b) -> a -> b
$ LocSymbol -> [Expr] -> Expr
mkEApp (SourcePos -> SourcePos -> Symbol -> LocSymbol
forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l1 SourcePos
l2 Symbol
cons) (Expr
first Expr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
: [Expr]
rest)


-- TODO:AZ: The comment says BitVector literal, but it accepts any @Sort@
-- | BitVector literal: lit "#x00000001" (BitVec (Size32 obj))
litP :: Parser Expr
litP :: Parser Expr
litP = do String -> Parser ()
reserved String
"lit"
          String
l <- Parser String
stringLiteral
          Sort
t <- Parser Sort
sortP
          Expr -> Parser Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Parser Expr) -> Expr -> Parser Expr
forall a b. (a -> b) -> a -> b
$ Constant -> Expr
ECon (Constant -> Expr) -> Constant -> Expr
forall a b. (a -> b) -> a -> b
$ Text -> Sort -> Constant
L (String -> Text
T.pack String
l) Sort
t

-- parenBrackets :: Parser a -> Parser a
-- parenBrackets  = parens . brackets

-- eMinus     = EBin Minus (expr (0 :: Integer))
-- eCons x xs = EApp (dummyLoc consName) [x, xs]
-- eNil       = EVar nilName

lamP :: Parser Expr
lamP :: Parser Expr
lamP
  = do String -> Parser ()
reservedOp String
"\\"
       Symbol
x <- Parser Symbol
symbolP
       Parser String
colon
       Sort
t <- Parser Sort
sortP
       String -> Parser ()
reservedOp String
"->"
       Expr
e  <- Parser Expr
exprP
       Expr -> Parser Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Parser Expr) -> Expr -> Parser Expr
forall a b. (a -> b) -> a -> b
$ (Symbol, Sort) -> Expr -> Expr
ELam (Symbol
x, Sort
t) Expr
e

dcolon :: Parser String
dcolon :: Parser String
dcolon = String -> Parser String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string String
"::" Parser String -> Parser () -> Parser String
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces

varSortP :: Parser Sort
varSortP :: Parser Sort
varSortP  = Int -> Sort
FVar  (Int -> Sort)
-> ParsecT String Integer (State PState) Int -> Parser Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT String Integer (State PState) Int
-> ParsecT String Integer (State PState) Int
forall u a. ParserT u a -> ParserT u a
parens ParsecT String Integer (State PState) Int
intP

funcSortP :: Parser Sort
funcSortP :: Parser Sort
funcSortP = Parser Sort -> Parser Sort
forall u a. ParserT u a -> ParserT u a
parens (Parser Sort -> Parser Sort) -> Parser Sort -> Parser Sort
forall a b. (a -> b) -> a -> b
$ Int -> [Sort] -> Sort
mkFFunc (Int -> [Sort] -> Sort)
-> ParsecT String Integer (State PState) Int
-> ParsecT String Integer (State PState) ([Sort] -> Sort)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT String Integer (State PState) Int
intP ParsecT String Integer (State PState) ([Sort] -> Sort)
-> Parser String
-> ParsecT String Integer (State PState) ([Sort] -> Sort)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser String
comma ParsecT String Integer (State PState) ([Sort] -> Sort)
-> ParsecT String Integer (State PState) [Sort] -> Parser Sort
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT String Integer (State PState) [Sort]
sortsP

sortsP :: Parser [Sort]
sortsP :: ParsecT String Integer (State PState) [Sort]
sortsP = ParsecT String Integer (State PState) [Sort]
-> ParsecT String Integer (State PState) [Sort]
forall u a. ParserT u a -> ParserT u a
brackets (ParsecT String Integer (State PState) [Sort]
 -> ParsecT String Integer (State PState) [Sort])
-> ParsecT String Integer (State PState) [Sort]
-> ParsecT String Integer (State PState) [Sort]
forall a b. (a -> b) -> a -> b
$ Parser Sort
-> Parser String -> ParsecT String Integer (State PState) [Sort]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy Parser Sort
sortP Parser String
semi

-- | Sort
sortP    :: Parser Sort
sortP :: Parser Sort
sortP    = ParsecT String Integer (State PState) [Sort] -> Parser Sort
sortP' (Parser Sort
-> Parser String -> ParsecT String Integer (State PState) [Sort]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy Parser Sort
sortArgP Parser String
blanks)

sortArgP :: Parser Sort
sortArgP :: Parser Sort
sortArgP = ParsecT String Integer (State PState) [Sort] -> Parser Sort
sortP' ([Sort] -> ParsecT String Integer (State PState) [Sort]
forall (m :: * -> *) a. Monad m => a -> m a
return [])

{-
sortFunP :: Parser Sort
sortFunP
   =  try (string "@" >> varSortP)
  <|> (fTyconSort <$> fTyConP)
-}

sortP' :: Parser [Sort] -> Parser Sort
sortP' :: ParsecT String Integer (State PState) [Sort] -> Parser Sort
sortP' ParsecT String Integer (State PState) [Sort]
appArgsP
   =  Parser Sort -> Parser Sort
forall u a. ParserT u a -> ParserT u a
parens Parser Sort
sortP
  Parser Sort -> Parser Sort -> Parser Sort
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (String -> Parser ()
reserved String
"func" Parser () -> Parser Sort -> Parser Sort
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Sort
funcSortP)
  Parser Sort -> Parser Sort -> Parser Sort
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (FTycon -> [Sort] -> Sort
fAppTC FTycon
listFTyCon ([Sort] -> Sort) -> (Sort -> [Sort]) -> Sort -> Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sort -> [Sort]
forall a. a -> [a]
single (Sort -> Sort) -> Parser Sort -> Parser Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Sort -> Parser Sort
forall u a. ParserT u a -> ParserT u a
brackets Parser Sort
sortP)
  Parser Sort -> Parser Sort -> Parser Sort
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser Sort
bvSortP
  Parser Sort -> Parser Sort -> Parser Sort
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (FTycon -> [Sort] -> Sort
fAppTC (FTycon -> [Sort] -> Sort)
-> ParsecT String Integer (State PState) FTycon
-> ParsecT String Integer (State PState) ([Sort] -> Sort)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT String Integer (State PState) FTycon
fTyConP ParsecT String Integer (State PState) ([Sort] -> Sort)
-> ParsecT String Integer (State PState) [Sort] -> Parser Sort
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT String Integer (State PState) [Sort]
appArgsP)
  Parser Sort -> Parser Sort -> Parser Sort
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Sort -> [Sort] -> Sort
fApp   (Sort -> [Sort] -> Sort)
-> Parser Sort
-> ParsecT String Integer (State PState) ([Sort] -> Sort)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Sort
tvarP   ParsecT String Integer (State PState) ([Sort] -> Sort)
-> ParsecT String Integer (State PState) [Sort] -> Parser Sort
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT String Integer (State PState) [Sort]
appArgsP)

single :: a -> [a]
single :: a -> [a]
single a
x = [a
x]

tvarP :: Parser Sort
tvarP :: Parser Sort
tvarP
   =  (String -> Parser String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string String
"@" Parser String -> Parser Sort -> Parser Sort
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Sort
varSortP)
  Parser Sort -> Parser Sort -> Parser Sort
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Symbol -> Sort
FObj (Symbol -> Sort) -> (Symbol -> Symbol) -> Symbol -> Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (Symbol -> Sort) -> Parser Symbol -> Parser Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Symbol
lowerIdP)


fTyConP :: Parser FTycon
fTyConP :: ParsecT String Integer (State PState) FTycon
fTyConP
  =   (String -> Parser ()
reserved String
"int"     Parser ()
-> ParsecT String Integer (State PState) FTycon
-> ParsecT String Integer (State PState) FTycon
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FTycon -> ParsecT String Integer (State PState) FTycon
forall (m :: * -> *) a. Monad m => a -> m a
return FTycon
intFTyCon)
  ParsecT String Integer (State PState) FTycon
-> ParsecT String Integer (State PState) FTycon
-> ParsecT String Integer (State PState) FTycon
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (String -> Parser ()
reserved String
"Integer" Parser ()
-> ParsecT String Integer (State PState) FTycon
-> ParsecT String Integer (State PState) FTycon
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FTycon -> ParsecT String Integer (State PState) FTycon
forall (m :: * -> *) a. Monad m => a -> m a
return FTycon
intFTyCon)
  ParsecT String Integer (State PState) FTycon
-> ParsecT String Integer (State PState) FTycon
-> ParsecT String Integer (State PState) FTycon
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (String -> Parser ()
reserved String
"Int"     Parser ()
-> ParsecT String Integer (State PState) FTycon
-> ParsecT String Integer (State PState) FTycon
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FTycon -> ParsecT String Integer (State PState) FTycon
forall (m :: * -> *) a. Monad m => a -> m a
return FTycon
intFTyCon)
  -- <|> (reserved "int"     >> return intFTyCon) -- TODO:AZ duplicate?
  ParsecT String Integer (State PState) FTycon
-> ParsecT String Integer (State PState) FTycon
-> ParsecT String Integer (State PState) FTycon
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (String -> Parser ()
reserved String
"real"    Parser ()
-> ParsecT String Integer (State PState) FTycon
-> ParsecT String Integer (State PState) FTycon
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FTycon -> ParsecT String Integer (State PState) FTycon
forall (m :: * -> *) a. Monad m => a -> m a
return FTycon
realFTyCon)
  ParsecT String Integer (State PState) FTycon
-> ParsecT String Integer (State PState) FTycon
-> ParsecT String Integer (State PState) FTycon
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (String -> Parser ()
reserved String
"bool"    Parser ()
-> ParsecT String Integer (State PState) FTycon
-> ParsecT String Integer (State PState) FTycon
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FTycon -> ParsecT String Integer (State PState) FTycon
forall (m :: * -> *) a. Monad m => a -> m a
return FTycon
boolFTyCon)
  ParsecT String Integer (State PState) FTycon
-> ParsecT String Integer (State PState) FTycon
-> ParsecT String Integer (State PState) FTycon
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (String -> Parser ()
reserved String
"num"     Parser ()
-> ParsecT String Integer (State PState) FTycon
-> ParsecT String Integer (State PState) FTycon
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FTycon -> ParsecT String Integer (State PState) FTycon
forall (m :: * -> *) a. Monad m => a -> m a
return FTycon
numFTyCon)
  ParsecT String Integer (State PState) FTycon
-> ParsecT String Integer (State PState) FTycon
-> ParsecT String Integer (State PState) FTycon
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (String -> Parser ()
reserved String
"Str"     Parser ()
-> ParsecT String Integer (State PState) FTycon
-> ParsecT String Integer (State PState) FTycon
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FTycon -> ParsecT String Integer (State PState) FTycon
forall (m :: * -> *) a. Monad m => a -> m a
return FTycon
strFTyCon)
  ParsecT String Integer (State PState) FTycon
-> ParsecT String Integer (State PState) FTycon
-> ParsecT String Integer (State PState) FTycon
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (LocSymbol -> FTycon
symbolFTycon      (LocSymbol -> FTycon)
-> Parser LocSymbol -> ParsecT String Integer (State PState) FTycon
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser LocSymbol
locUpperIdP)

-- | Bit-Vector Sort
bvSortP :: Parser Sort
bvSortP :: Parser Sort
bvSortP = BvSize -> Sort
mkSort (BvSize -> Sort)
-> ParsecT String Integer (State PState) BvSize -> Parser Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> BvSize -> ParsecT String Integer (State PState) BvSize
forall b. String -> b -> ParsecT String Integer (State PState) b
bvSizeP String
"Size32" BvSize
S32 ParsecT String Integer (State PState) BvSize
-> ParsecT String Integer (State PState) BvSize
-> ParsecT String Integer (State PState) BvSize
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String -> BvSize -> ParsecT String Integer (State PState) BvSize
forall b. String -> b -> ParsecT String Integer (State PState) b
bvSizeP String
"Size64" BvSize
S64)
  where
    bvSizeP :: String -> b -> ParsecT String Integer (State PState) b
bvSizeP String
ss b
s = do
      Parser () -> Parser ()
forall u a. ParserT u a -> ParserT u a
parens (String -> Parser ()
reserved String
"BitVec" Parser () -> Parser () -> Parser ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> Parser ()
reserved String
ss)
      b -> ParsecT String Integer (State PState) b
forall (m :: * -> *) a. Monad m => a -> m a
return b
s


--------------------------------------------------------------------------------
-- | Predicates ----------------------------------------------------------------
--------------------------------------------------------------------------------

pred0P :: Parser Expr
pred0P :: Parser Expr
pred0P =  Parser Expr
trueP
      Parser Expr -> Parser Expr -> Parser Expr
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser Expr
falseP
      Parser Expr -> Parser Expr -> Parser Expr
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (String -> Parser ()
reservedOp String
"??" Parser () -> Parser Expr -> Parser Expr
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Expr
makeUniquePGrad)
      Parser Expr -> Parser Expr -> Parser Expr
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser Expr
kvarPredP
      Parser Expr -> Parser Expr -> Parser Expr
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ((Expr -> Expr -> Expr -> Expr) -> Parser Expr -> Parser Expr
forall a. (Expr -> a -> a -> a) -> Parser a -> Parser a
fastIfP Expr -> Expr -> Expr -> Expr
pIte Parser Expr
predP)
      Parser Expr -> Parser Expr -> Parser Expr
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser Expr -> Parser Expr
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try Parser Expr
predrP
      Parser Expr -> Parser Expr -> Parser Expr
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Parser Expr -> Parser Expr
forall u a. ParserT u a -> ParserT u a
parens Parser Expr
predP)
      Parser Expr -> Parser Expr -> Parser Expr
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (String -> Parser ()
reservedOp String
"?" Parser () -> Parser Expr -> Parser Expr
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Expr
exprP)
      Parser Expr -> Parser Expr -> Parser Expr
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser Expr -> Parser Expr
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try Parser Expr
funAppP
      Parser Expr -> Parser Expr -> Parser Expr
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Symbol -> Expr
forall a. Symbolic a => a -> Expr
eVar (Symbol -> Expr) -> Parser Symbol -> Parser Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Symbol
symbolP)
      Parser Expr -> Parser Expr -> Parser Expr
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (String -> Parser ()
reservedOp String
"&&" Parser () -> Parser Expr -> Parser Expr
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [Expr] -> Expr
pGAnds ([Expr] -> Expr)
-> ParsecT String Integer (State PState) [Expr] -> Parser Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT String Integer (State PState) [Expr]
predsP)
      Parser Expr -> Parser Expr -> Parser Expr
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (String -> Parser ()
reservedOp String
"||" Parser () -> Parser Expr -> Parser Expr
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [Expr] -> Expr
POr  ([Expr] -> Expr)
-> ParsecT String Integer (State PState) [Expr] -> Parser Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT String Integer (State PState) [Expr]
predsP)

makeUniquePGrad :: Parser Expr
makeUniquePGrad :: Parser Expr
makeUniquePGrad
  = do SourcePos
uniquePos <- ParsecT String Integer (State PState) SourcePos
forall (m :: * -> *) s u. Monad m => ParsecT s u m SourcePos
getPosition
       Expr -> Parser Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Parser Expr) -> Expr -> Parser Expr
forall a b. (a -> b) -> a -> b
$ KVar -> Subst -> GradInfo -> Expr -> Expr
PGrad (Symbol -> KVar
KV (Symbol -> KVar) -> Symbol -> KVar
forall a b. (a -> b) -> a -> b
$ String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String -> Symbol) -> String -> Symbol
forall a b. (a -> b) -> a -> b
$ SourcePos -> String
forall a. Show a => a -> String
show SourcePos
uniquePos) Subst
forall a. Monoid a => a
mempty (SourcePos -> GradInfo
srcGradInfo SourcePos
uniquePos) Expr
forall a. Monoid a => a
mempty

-- qmP    = reserved "?" <|> reserved "Bexp"

trueP, falseP :: Parser Expr
trueP :: Parser Expr
trueP  = String -> Parser ()
reserved String
"true"  Parser () -> Parser Expr -> Parser Expr
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Expr -> Parser Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
PTrue
falseP :: Parser Expr
falseP = String -> Parser ()
reserved String
"false" Parser () -> Parser Expr -> Parser Expr
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Expr -> Parser Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
PFalse

kvarPredP :: Parser Expr
kvarPredP :: Parser Expr
kvarPredP = KVar -> Subst -> Expr
PKVar (KVar -> Subst -> Expr)
-> ParsecT String Integer (State PState) KVar
-> ParsecT String Integer (State PState) (Subst -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT String Integer (State PState) KVar
kvarP ParsecT String Integer (State PState) (Subst -> Expr)
-> ParsecT String Integer (State PState) Subst -> Parser Expr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT String Integer (State PState) Subst
substP

kvarP :: Parser KVar
kvarP :: ParsecT String Integer (State PState) KVar
kvarP = Symbol -> KVar
KV (Symbol -> KVar)
-> Parser Symbol -> ParsecT String Integer (State PState) KVar
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Char -> ParsecT String Integer (State PState) Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
'$' ParsecT String Integer (State PState) Char
-> Parser Symbol -> Parser Symbol
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Symbol
symbolP Parser Symbol -> Parser () -> Parser Symbol
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces)

substP :: Parser Subst
substP :: ParsecT String Integer (State PState) Subst
substP = [(Symbol, Expr)] -> Subst
mkSubst ([(Symbol, Expr)] -> Subst)
-> ParsecT String Integer (State PState) [(Symbol, Expr)]
-> ParsecT String Integer (State PState) Subst
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT String Integer (State PState) (Symbol, Expr)
-> ParsecT String Integer (State PState) [(Symbol, Expr)]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many (ParsecT String Integer (State PState) (Symbol, Expr)
-> ParsecT String Integer (State PState) (Symbol, Expr)
forall u a. ParserT u a -> ParserT u a
brackets (ParsecT String Integer (State PState) (Symbol, Expr)
 -> ParsecT String Integer (State PState) (Symbol, Expr))
-> ParsecT String Integer (State PState) (Symbol, Expr)
-> ParsecT String Integer (State PState) (Symbol, Expr)
forall a b. (a -> b) -> a -> b
$ Parser Symbol
-> Parser ()
-> Parser Expr
-> ParsecT String Integer (State PState) (Symbol, Expr)
forall a z b. Parser a -> Parser z -> Parser b -> Parser (a, b)
pairP Parser Symbol
symbolP Parser ()
aP Parser Expr
exprP)
  where
    aP :: Parser ()
aP = String -> Parser ()
reservedOp String
":="

predsP :: Parser [Expr]
predsP :: ParsecT String Integer (State PState) [Expr]
predsP = ParsecT String Integer (State PState) [Expr]
-> ParsecT String Integer (State PState) [Expr]
forall u a. ParserT u a -> ParserT u a
brackets (ParsecT String Integer (State PState) [Expr]
 -> ParsecT String Integer (State PState) [Expr])
-> ParsecT String Integer (State PState) [Expr]
-> ParsecT String Integer (State PState) [Expr]
forall a b. (a -> b) -> a -> b
$ Parser Expr
-> Parser String -> ParsecT String Integer (State PState) [Expr]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy Parser Expr
predP Parser String
semi

predP  :: Parser Expr
predP :: Parser Expr
predP  = OpTable -> Parser Expr -> Parser Expr
forall s (m :: * -> *) t u a.
Stream s m t =>
OperatorTable s u m a -> ParsecT s u m a -> ParsecT s u m a
buildExpressionParser OpTable
lops Parser Expr
pred0P
  where
    lops :: OpTable
lops = [ [ParsecT String Integer (State PState) (Expr -> Expr)
-> Operator String Integer (State PState) Expr
forall s u (m :: * -> *) a.
ParsecT s u m (a -> a) -> Operator s u m a
Prefix (String -> Parser ()
reservedOp String
"~"    Parser ()
-> ParsecT String Integer (State PState) (Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Expr -> Expr
PNot)]
           , [ParsecT String Integer (State PState) (Expr -> Expr)
-> Operator String Integer (State PState) Expr
forall s u (m :: * -> *) a.
ParsecT s u m (a -> a) -> Operator s u m a
Prefix (String -> Parser ()
reservedOp String
"not " Parser ()
-> ParsecT String Integer (State PState) (Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Expr -> Expr
PNot)]
           , [ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
-> Assoc -> Operator String Integer (State PState) Expr
forall s u (m :: * -> *) a.
ParsecT s u m (a -> a -> a) -> Assoc -> Operator s u m a
Infix  (String -> Parser ()
reservedOp String
"&&"   Parser ()
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Expr -> Expr -> Expr
pGAnd) Assoc
AssocRight]
           , [ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
-> Assoc -> Operator String Integer (State PState) Expr
forall s u (m :: * -> *) a.
ParsecT s u m (a -> a -> a) -> Assoc -> Operator s u m a
Infix  (String -> Parser ()
reservedOp String
"||"   Parser ()
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (\Expr
x Expr
y -> [Expr] -> Expr
POr  [Expr
x,Expr
y])) Assoc
AssocRight]
           , [ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
-> Assoc -> Operator String Integer (State PState) Expr
forall s u (m :: * -> *) a.
ParsecT s u m (a -> a -> a) -> Assoc -> Operator s u m a
Infix  (String -> Parser ()
reservedOp String
"=>"   Parser ()
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Expr -> Expr -> Expr
PImp) Assoc
AssocRight]
           , [ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
-> Assoc -> Operator String Integer (State PState) Expr
forall s u (m :: * -> *) a.
ParsecT s u m (a -> a -> a) -> Assoc -> Operator s u m a
Infix  (String -> Parser ()
reservedOp String
"==>"  Parser ()
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Expr -> Expr -> Expr
PImp) Assoc
AssocRight]
           , [ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
-> Assoc -> Operator String Integer (State PState) Expr
forall s u (m :: * -> *) a.
ParsecT s u m (a -> a -> a) -> Assoc -> Operator s u m a
Infix  (String -> Parser ()
reservedOp String
"<=>"  Parser ()
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Expr -> Expr -> Expr
PIff) Assoc
AssocRight]]

predrP :: Parser Expr
predrP :: Parser Expr
predrP = do Expr
e1    <- Parser Expr
exprP
            Expr -> Expr -> Expr
r     <- ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
brelP
            Expr
e2    <- Parser Expr
exprP
            Expr -> Parser Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Parser Expr) -> Expr -> Parser Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
r Expr
e1 Expr
e2

brelP ::  Parser (Expr -> Expr -> Expr)
brelP :: ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
brelP =  (String -> Parser ()
reservedOp String
"==" Parser ()
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Eq))
     ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (String -> Parser ()
reservedOp String
"="  Parser ()
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Eq))
     ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (String -> Parser ()
reservedOp String
"~~" Parser ()
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Ueq))
     ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (String -> Parser ()
reservedOp String
"!=" Parser ()
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Ne))
     ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (String -> Parser ()
reservedOp String
"/=" Parser ()
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Ne))
     ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (String -> Parser ()
reservedOp String
"!~" Parser ()
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Une))
     ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (String -> Parser ()
reservedOp String
"<"  Parser ()
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Lt))
     ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (String -> Parser ()
reservedOp String
"<=" Parser ()
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Le))
     ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (String -> Parser ()
reservedOp String
">"  Parser ()
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Gt))
     ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (String -> Parser ()
reservedOp String
">=" Parser ()
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> ParsecT String Integer (State PState) (Expr -> Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Ge))

--------------------------------------------------------------------------------
-- | BareTypes -----------------------------------------------------------------
--------------------------------------------------------------------------------

-- | Refa
refaP :: Parser Expr
refaP :: Parser Expr
refaP =  Parser Expr -> Parser Expr
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try ([Expr] -> Expr
pAnd ([Expr] -> Expr)
-> ParsecT String Integer (State PState) [Expr] -> Parser Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT String Integer (State PState) [Expr]
-> ParsecT String Integer (State PState) [Expr]
forall u a. ParserT u a -> ParserT u a
brackets (Parser Expr
-> Parser String -> ParsecT String Integer (State PState) [Expr]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy Parser Expr
predP Parser String
semi))
     Parser Expr -> Parser Expr -> Parser Expr
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser Expr
predP


-- | (Sorted) Refinements with configurable sub-parsers
refBindP :: Parser Symbol -> Parser Expr -> Parser (Reft -> a) -> Parser a
refBindP :: Parser Symbol -> Parser Expr -> Parser (Reft -> a) -> Parser a
refBindP Parser Symbol
bp Parser Expr
rp Parser (Reft -> a)
kindP
  = Parser a -> Parser a
forall u a. ParserT u a -> ParserT u a
braces (Parser a -> Parser a) -> Parser a -> Parser a
forall a b. (a -> b) -> a -> b
$ do
      Symbol
x  <- Parser Symbol
bp
      Reft -> a
t  <- Parser (Reft -> a)
kindP
      String -> Parser ()
reservedOp String
"|"
      Expr
ra <- Parser Expr
rp Parser Expr -> Parser () -> Parser Expr
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
      a -> Parser a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Parser a) -> a -> Parser a
forall a b. (a -> b) -> a -> b
$ Reft -> a
t ((Symbol, Expr) -> Reft
Reft (Symbol
x, Expr
ra))


-- bindP      = symbol    <$> (lowerIdP <* colon)
-- | Binder (lowerIdP <* colon)
bindP :: Parser Symbol
bindP :: Parser Symbol
bindP = Parser Symbol
symbolP Parser Symbol -> Parser String -> Parser Symbol
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser String
colon

optBindP :: Symbol -> Parser Symbol
optBindP :: Symbol -> Parser Symbol
optBindP Symbol
x = Parser Symbol -> Parser Symbol
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try Parser Symbol
bindP Parser Symbol -> Parser Symbol -> Parser Symbol
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Symbol -> Parser Symbol
forall (m :: * -> *) a. Monad m => a -> m a
return Symbol
x

-- | (Sorted) Refinements
refP :: Parser (Reft -> a) -> Parser a
refP :: Parser (Reft -> a) -> Parser a
refP       = Parser Symbol -> Parser Expr -> Parser (Reft -> a) -> Parser a
forall a.
Parser Symbol -> Parser Expr -> Parser (Reft -> a) -> Parser a
refBindP Parser Symbol
bindP Parser Expr
refaP

-- | (Sorted) Refinements with default binder
refDefP :: Symbol -> Parser Expr -> Parser (Reft -> a) -> Parser a
refDefP :: Symbol -> Parser Expr -> Parser (Reft -> a) -> Parser a
refDefP Symbol
x  = Parser Symbol -> Parser Expr -> Parser (Reft -> a) -> Parser a
forall a.
Parser Symbol -> Parser Expr -> Parser (Reft -> a) -> Parser a
refBindP (Symbol -> Parser Symbol
optBindP Symbol
x)

--------------------------------------------------------------------------------
-- | Parsing Data Declarations -------------------------------------------------
--------------------------------------------------------------------------------

dataFieldP :: Parser DataField
dataFieldP :: Parser DataField
dataFieldP = LocSymbol -> Sort -> DataField
DField (LocSymbol -> Sort -> DataField)
-> Parser LocSymbol
-> ParsecT String Integer (State PState) (Sort -> DataField)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser LocSymbol
locSymbolP ParsecT String Integer (State PState) (Sort -> DataField)
-> Parser String
-> ParsecT String Integer (State PState) (Sort -> DataField)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser String
colon ParsecT String Integer (State PState) (Sort -> DataField)
-> Parser Sort -> Parser DataField
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Sort
sortP

dataCtorP :: Parser DataCtor
dataCtorP :: Parser DataCtor
dataCtorP  = LocSymbol -> [DataField] -> DataCtor
DCtor (LocSymbol -> [DataField] -> DataCtor)
-> Parser LocSymbol
-> ParsecT String Integer (State PState) ([DataField] -> DataCtor)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser LocSymbol
locSymbolP
                   ParsecT String Integer (State PState) ([DataField] -> DataCtor)
-> ParsecT String Integer (State PState) [DataField]
-> Parser DataCtor
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT String Integer (State PState) [DataField]
-> ParsecT String Integer (State PState) [DataField]
forall u a. ParserT u a -> ParserT u a
braces (Parser DataField
-> Parser String
-> ParsecT String Integer (State PState) [DataField]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy Parser DataField
dataFieldP Parser String
comma)

dataDeclP :: Parser DataDecl
dataDeclP :: Parser DataDecl
dataDeclP  = FTycon -> Int -> [DataCtor] -> DataDecl
DDecl (FTycon -> Int -> [DataCtor] -> DataDecl)
-> ParsecT String Integer (State PState) FTycon
-> ParsecT
     String Integer (State PState) (Int -> [DataCtor] -> DataDecl)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT String Integer (State PState) FTycon
fTyConP ParsecT
  String Integer (State PState) (Int -> [DataCtor] -> DataDecl)
-> ParsecT String Integer (State PState) Int
-> ParsecT String Integer (State PState) ([DataCtor] -> DataDecl)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT String Integer (State PState) Int
intP ParsecT String Integer (State PState) ([DataCtor] -> DataDecl)
-> Parser ()
-> ParsecT String Integer (State PState) ([DataCtor] -> DataDecl)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* String -> Parser ()
reservedOp String
"="
                   ParsecT String Integer (State PState) ([DataCtor] -> DataDecl)
-> ParsecT String Integer (State PState) [DataCtor]
-> Parser DataDecl
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT String Integer (State PState) [DataCtor]
-> ParsecT String Integer (State PState) [DataCtor]
forall u a. ParserT u a -> ParserT u a
brackets (Parser DataCtor -> ParsecT String Integer (State PState) [DataCtor]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many (String -> Parser ()
reservedOp String
"|" Parser () -> Parser DataCtor -> Parser DataCtor
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser DataCtor
dataCtorP))

--------------------------------------------------------------------------------
-- | Parsing Qualifiers --------------------------------------------------------
--------------------------------------------------------------------------------

-- | Qualifiers
qualifierP :: Parser Sort -> Parser Qualifier
qualifierP :: Parser Sort -> Parser Qualifier
qualifierP Parser Sort
tP = do
  SourcePos
pos    <- ParsecT String Integer (State PState) SourcePos
forall (m :: * -> *) s u. Monad m => ParsecT s u m SourcePos
getPosition
  Symbol
n      <- Parser Symbol
upperIdP
  [QualParam]
params <- ParserT Integer [QualParam] -> ParserT Integer [QualParam]
forall u a. ParserT u a -> ParserT u a
parens (ParserT Integer [QualParam] -> ParserT Integer [QualParam])
-> ParserT Integer [QualParam] -> ParserT Integer [QualParam]
forall a b. (a -> b) -> a -> b
$ ParsecT String Integer (State PState) QualParam
-> Parser String -> ParserT Integer [QualParam]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy1 (Parser Sort -> ParsecT String Integer (State PState) QualParam
qualParamP Parser Sort
tP) Parser String
comma
  String
_      <- Parser String
colon
  Expr
body   <- Parser Expr
predP
  Qualifier -> Parser Qualifier
forall (m :: * -> *) a. Monad m => a -> m a
return  (Qualifier -> Parser Qualifier) -> Qualifier -> Parser Qualifier
forall a b. (a -> b) -> a -> b
$ Symbol -> [QualParam] -> Expr -> SourcePos -> Qualifier
mkQual Symbol
n [QualParam]
params Expr
body SourcePos
pos

qualParamP :: Parser Sort -> Parser QualParam 
qualParamP :: Parser Sort -> ParsecT String Integer (State PState) QualParam
qualParamP Parser Sort
tP = do 
  Symbol
x     <- Parser Symbol
symbolP 
  QualPattern
pat   <- Parser QualPattern
qualPatP 
  String
_     <- Parser String
colon 
  Sort
t     <- Parser Sort
tP 
  QualParam -> ParsecT String Integer (State PState) QualParam
forall (m :: * -> *) a. Monad m => a -> m a
return (QualParam -> ParsecT String Integer (State PState) QualParam)
-> QualParam -> ParsecT String Integer (State PState) QualParam
forall a b. (a -> b) -> a -> b
$ Symbol -> QualPattern -> Sort -> QualParam
QP Symbol
x QualPattern
pat Sort
t 

qualPatP :: Parser QualPattern
qualPatP :: Parser QualPattern
qualPatP 
   =  (String -> Parser ()
reserved String
"as" Parser () -> Parser QualPattern -> Parser QualPattern
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser QualPattern
qualStrPatP)
  Parser QualPattern -> Parser QualPattern -> Parser QualPattern
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> QualPattern -> Parser QualPattern
forall (m :: * -> *) a. Monad m => a -> m a
return QualPattern
PatNone 

qualStrPatP :: Parser QualPattern
qualStrPatP :: Parser QualPattern
qualStrPatP 
   = (Symbol -> QualPattern
PatExact (Symbol -> QualPattern) -> Parser Symbol -> Parser QualPattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Symbol
symbolP)
  Parser QualPattern -> Parser QualPattern -> Parser QualPattern
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser QualPattern -> Parser QualPattern
forall u a. ParserT u a -> ParserT u a
parens (    ((Symbol -> Int -> QualPattern) -> (Symbol, Int) -> QualPattern
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Symbol -> Int -> QualPattern
PatPrefix ((Symbol, Int) -> QualPattern)
-> ParsecT String Integer (State PState) (Symbol, Int)
-> Parser QualPattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Symbol
-> Parser String
-> ParsecT String Integer (State PState) Int
-> ParsecT String Integer (State PState) (Symbol, Int)
forall a z b. Parser a -> Parser z -> Parser b -> Parser (a, b)
pairP Parser Symbol
symbolP Parser String
dot ParsecT String Integer (State PState) Int
qpVarP)
              Parser QualPattern -> Parser QualPattern -> Parser QualPattern
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ((Int -> Symbol -> QualPattern) -> (Int, Symbol) -> QualPattern
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Int -> Symbol -> QualPattern
PatSuffix ((Int, Symbol) -> QualPattern)
-> ParsecT String Integer (State PState) (Int, Symbol)
-> Parser QualPattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT String Integer (State PState) Int
-> Parser String
-> Parser Symbol
-> ParsecT String Integer (State PState) (Int, Symbol)
forall a z b. Parser a -> Parser z -> Parser b -> Parser (a, b)
pairP ParsecT String Integer (State PState) Int
qpVarP  Parser String
dot Parser Symbol
symbolP) )


qpVarP :: Parser Int
qpVarP :: ParsecT String Integer (State PState) Int
qpVarP = Char -> ParsecT String Integer (State PState) Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
'$' ParsecT String Integer (State PState) Char
-> ParsecT String Integer (State PState) Int
-> ParsecT String Integer (State PState) Int
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT String Integer (State PState) Int
intP 

symBindP :: Parser a -> Parser (Symbol, a)
symBindP :: Parser a -> Parser (Symbol, a)
symBindP = Parser Symbol -> Parser String -> Parser a -> Parser (Symbol, a)
forall a z b. Parser a -> Parser z -> Parser b -> Parser (a, b)
pairP Parser Symbol
symbolP Parser String
colon

pairP :: Parser a -> Parser z -> Parser b -> Parser (a, b)
pairP :: Parser a -> Parser z -> Parser b -> Parser (a, b)
pairP Parser a
xP Parser z
sepP Parser b
yP = (,) (a -> b -> (a, b))
-> Parser a -> ParsecT String Integer (State PState) (b -> (a, b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser a
xP ParsecT String Integer (State PState) (b -> (a, b))
-> Parser z -> ParsecT String Integer (State PState) (b -> (a, b))
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser z
sepP ParsecT String Integer (State PState) (b -> (a, b))
-> Parser b -> Parser (a, b)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser b
yP

---------------------------------------------------------------------
-- | Axioms for Symbolic Evaluation ---------------------------------
---------------------------------------------------------------------

autoRewriteP :: Parser AutoRewrite
autoRewriteP :: Parser AutoRewrite
autoRewriteP = do
  [SortedReft]
args       <- ParsecT String Integer (State PState) SortedReft
-> Parser () -> ParsecT String Integer (State PState) [SortedReft]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy ParsecT String Integer (State PState) SortedReft
sortedReftP Parser ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
  ()
_          <- Parser ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
  ()
_          <- String -> Parser ()
reserved String
"="
  ()
_          <- Parser ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
  (Expr
lhs, Expr
rhs) <- ParserT Integer (Expr, Expr) -> ParserT Integer (Expr, Expr)
forall u a. ParserT u a -> ParserT u a
braces (ParserT Integer (Expr, Expr) -> ParserT Integer (Expr, Expr))
-> ParserT Integer (Expr, Expr) -> ParserT Integer (Expr, Expr)
forall a b. (a -> b) -> a -> b
$
      Parser Expr
-> Parser () -> Parser Expr -> ParserT Integer (Expr, Expr)
forall a z b. Parser a -> Parser z -> Parser b -> Parser (a, b)
pairP Parser Expr
exprP (String -> Parser ()
reserved String
"=") Parser Expr
exprP
  AutoRewrite -> Parser AutoRewrite
forall (m :: * -> *) a. Monad m => a -> m a
return (AutoRewrite -> Parser AutoRewrite)
-> AutoRewrite -> Parser AutoRewrite
forall a b. (a -> b) -> a -> b
$ [SortedReft] -> Expr -> Expr -> AutoRewrite
AutoRewrite [SortedReft]
args Expr
lhs Expr
rhs


defineP :: Parser Equation
defineP :: Parser Equation
defineP = do
  Symbol
name   <- Parser Symbol
symbolP
  [(Symbol, Sort)]
params <- ParserT Integer [(Symbol, Sort)]
-> ParserT Integer [(Symbol, Sort)]
forall u a. ParserT u a -> ParserT u a
parens        (ParserT Integer [(Symbol, Sort)]
 -> ParserT Integer [(Symbol, Sort)])
-> ParserT Integer [(Symbol, Sort)]
-> ParserT Integer [(Symbol, Sort)]
forall a b. (a -> b) -> a -> b
$ ParsecT String Integer (State PState) (Symbol, Sort)
-> Parser String -> ParserT Integer [(Symbol, Sort)]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy (Parser Sort -> ParsecT String Integer (State PState) (Symbol, Sort)
forall a. Parser a -> Parser (Symbol, a)
symBindP Parser Sort
sortP) Parser String
comma
  Sort
sort   <- Parser String
colon        Parser String -> Parser Sort -> Parser Sort
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Sort
sortP
  Expr
body   <- String -> Parser ()
reserved String
"=" Parser () -> Parser Expr -> Parser Expr
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Expr -> Parser Expr
forall a. Parser a -> Parser a
sbraces (
              if Sort
sort Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
boolSort then Parser Expr
predP else Parser Expr
exprP
               )
  Equation -> Parser Equation
forall (m :: * -> *) a. Monad m => a -> m a
return  (Equation -> Parser Equation) -> Equation -> Parser Equation
forall a b. (a -> b) -> a -> b
$ Symbol -> [(Symbol, Sort)] -> Expr -> Sort -> Equation
mkEquation Symbol
name [(Symbol, Sort)]
params Expr
body Sort
sort

matchP :: Parser Rewrite
matchP :: Parser Rewrite
matchP = Symbol -> Symbol -> [Symbol] -> Expr -> Rewrite
SMeasure (Symbol -> Symbol -> [Symbol] -> Expr -> Rewrite)
-> Parser Symbol
-> ParsecT
     String
     Integer
     (State PState)
     (Symbol -> [Symbol] -> Expr -> Rewrite)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Symbol
symbolP ParsecT
  String
  Integer
  (State PState)
  (Symbol -> [Symbol] -> Expr -> Rewrite)
-> Parser Symbol
-> ParsecT
     String Integer (State PState) ([Symbol] -> Expr -> Rewrite)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Symbol
symbolP ParsecT String Integer (State PState) ([Symbol] -> Expr -> Rewrite)
-> ParsecT String Integer (State PState) [Symbol]
-> ParsecT String Integer (State PState) (Expr -> Rewrite)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Symbol -> ParsecT String Integer (State PState) [Symbol]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many Parser Symbol
symbolP ParsecT String Integer (State PState) (Expr -> Rewrite)
-> Parser Expr -> Parser Rewrite
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (String -> Parser ()
reserved String
"=" Parser () -> Parser Expr -> Parser Expr
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Expr
exprP)

pairsP :: Parser a -> Parser b -> Parser [(a, b)]
pairsP :: Parser a -> Parser b -> Parser [(a, b)]
pairsP Parser a
aP Parser b
bP = Parser [(a, b)] -> Parser [(a, b)]
forall u a. ParserT u a -> ParserT u a
brackets (Parser [(a, b)] -> Parser [(a, b)])
-> Parser [(a, b)] -> Parser [(a, b)]
forall a b. (a -> b) -> a -> b
$ ParsecT String Integer (State PState) (a, b)
-> Parser String -> Parser [(a, b)]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy1 (Parser a
-> Parser ()
-> Parser b
-> ParsecT String Integer (State PState) (a, b)
forall a z b. Parser a -> Parser z -> Parser b -> Parser (a, b)
pairP Parser a
aP (String -> Parser ()
reserved String
":") Parser b
bP) Parser String
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 (Int -> Def a -> String -> String
[Def a] -> String -> String
Def a -> String
(Int -> Def a -> String -> String)
-> (Def a -> String)
-> ([Def a] -> String -> String)
-> Show (Def a)
forall a. Fixpoint a => Int -> Def a -> String -> String
forall a. Fixpoint a => [Def a] -> String -> String
forall a. Fixpoint a => Def a -> String
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [Def a] -> String -> String
$cshowList :: forall a. Fixpoint a => [Def a] -> String -> String
show :: Def a -> String
$cshow :: forall a. Fixpoint a => Def a -> String
showsPrec :: Int -> Def a -> String -> String
$cshowsPrec :: forall a. Fixpoint a => Int -> Def a -> String -> String
Show, (forall x. Def a -> Rep (Def a) x)
-> (forall x. Rep (Def a) x -> Def a) -> Generic (Def a)
forall x. Rep (Def a) x -> Def a
forall x. Def a -> Rep (Def a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Def a) x -> Def a
forall a x. Def a -> Rep (Def a) x
$cto :: forall a x. Rep (Def a) x -> Def a
$cfrom :: forall a x. Def a -> Rep (Def a) x
Generic)
  --  Sol of solbind
  --  Dep of FixConstraint.dep

fInfoOptP :: Parser (FInfoWithOpts ())
fInfoOptP :: Parser (FInfoWithOpts ())
fInfoOptP = do [Def ()]
ps <- ParsecT String Integer (State PState) (Def ())
-> ParsecT String Integer (State PState) [Def ()]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ParsecT String Integer (State PState) (Def ())
defP
               FInfoWithOpts () -> Parser (FInfoWithOpts ())
forall (m :: * -> *) a. Monad m => a -> m a
return (FInfoWithOpts () -> Parser (FInfoWithOpts ()))
-> FInfoWithOpts () -> Parser (FInfoWithOpts ())
forall a b. (a -> b) -> a -> b
$ FInfo () -> [String] -> FInfoWithOpts ()
forall a. FInfo a -> [String] -> FInfoWithOpts a
FIO ([Def ()] -> FInfo ()
forall a. [Def a] -> FInfo a
defsFInfo [Def ()]
ps) [String
s | Opt String
s <- [Def ()]
ps]

fInfoP :: Parser (FInfo ())
fInfoP :: Parser (FInfo ())
fInfoP = [Def ()] -> FInfo ()
forall a. [Def a] -> FInfo a
defsFInfo ([Def ()] -> FInfo ())
-> ParsecT String Integer (State PState) [Def ()]
-> Parser (FInfo ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> {-# SCC "many-defP" #-} ParsecT String Integer (State PState) (Def ())
-> ParsecT String Integer (State PState) [Def ()]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ParsecT String Integer (State PState) (Def ())
defP

defP :: Parser (Def ())
defP :: ParsecT String Integer (State PState) (Def ())
defP =  Sort -> Def ()
forall a. Sort -> Def a
Srt   (Sort -> Def ())
-> Parser Sort -> ParsecT String Integer (State PState) (Def ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"sort"         Parser () -> Parser String -> Parser String
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser String
colon Parser String -> Parser Sort -> Parser Sort
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Sort
sortP)
    ParsecT String Integer (State PState) (Def ())
-> ParsecT String Integer (State PState) (Def ())
-> ParsecT String Integer (State PState) (Def ())
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SubC () -> Def ()
forall a. SubC a -> Def a
Cst   (SubC () -> Def ())
-> ParsecT String Integer (State PState) (SubC ())
-> ParsecT String Integer (State PState) (Def ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"constraint"   Parser () -> Parser String -> Parser String
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser String
colon Parser String
-> ParsecT String Integer (State PState) (SubC ())
-> ParsecT String Integer (State PState) (SubC ())
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> {-# SCC "subCP" #-} ParsecT String Integer (State PState) (SubC ())
subCP)
    ParsecT String Integer (State PState) (Def ())
-> ParsecT String Integer (State PState) (Def ())
-> ParsecT String Integer (State PState) (Def ())
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> WfC () -> Def ()
forall a. WfC a -> Def a
Wfc   (WfC () -> Def ())
-> ParsecT String Integer (State PState) (WfC ())
-> ParsecT String Integer (State PState) (Def ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"wf"           Parser () -> Parser String -> Parser String
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser String
colon Parser String
-> ParsecT String Integer (State PState) (WfC ())
-> ParsecT String Integer (State PState) (WfC ())
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> {-# SCC "wfCP"  #-} ParsecT String Integer (State PState) (WfC ())
wfCP)
    ParsecT String Integer (State PState) (Def ())
-> ParsecT String Integer (State PState) (Def ())
-> ParsecT String Integer (State PState) (Def ())
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Symbol -> Sort -> Def ()
forall a. Symbol -> Sort -> Def a
Con   (Symbol -> Sort -> Def ())
-> Parser Symbol
-> ParsecT String Integer (State PState) (Sort -> Def ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"constant"     Parser () -> Parser Symbol -> Parser Symbol
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Symbol
symbolP) ParsecT String Integer (State PState) (Sort -> Def ())
-> Parser Sort -> ParsecT String Integer (State PState) (Def ())
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Parser String
colon Parser String -> Parser Sort -> Parser Sort
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Sort
sortP)
    ParsecT String Integer (State PState) (Def ())
-> ParsecT String Integer (State PState) (Def ())
-> ParsecT String Integer (State PState) (Def ())
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Symbol -> Sort -> Def ()
forall a. Symbol -> Sort -> Def a
Dis   (Symbol -> Sort -> Def ())
-> Parser Symbol
-> ParsecT String Integer (State PState) (Sort -> Def ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"distinct"     Parser () -> Parser Symbol -> Parser Symbol
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Symbol
symbolP) ParsecT String Integer (State PState) (Sort -> Def ())
-> Parser Sort -> ParsecT String Integer (State PState) (Def ())
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Parser String
colon Parser String -> Parser Sort -> Parser Sort
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Sort
sortP)
    ParsecT String Integer (State PState) (Def ())
-> ParsecT String Integer (State PState) (Def ())
-> ParsecT String Integer (State PState) (Def ())
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> KVar -> Int -> Def ()
forall a. KVar -> Int -> Def a
Pack  (KVar -> Int -> Def ())
-> ParsecT String Integer (State PState) KVar
-> ParsecT String Integer (State PState) (Int -> Def ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"pack"         Parser ()
-> ParsecT String Integer (State PState) KVar
-> ParsecT String Integer (State PState) KVar
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ParsecT String Integer (State PState) KVar
kvarP)   ParsecT String Integer (State PState) (Int -> Def ())
-> ParsecT String Integer (State PState) Int
-> ParsecT String Integer (State PState) (Def ())
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Parser String
colon Parser String
-> ParsecT String Integer (State PState) Int
-> ParsecT String Integer (State PState) Int
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ParsecT String Integer (State PState) Int
intP)
    ParsecT String Integer (State PState) (Def ())
-> ParsecT String Integer (State PState) (Def ())
-> ParsecT String Integer (State PState) (Def ())
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Qualifier -> Def ()
forall a. Qualifier -> Def a
Qul   (Qualifier -> Def ())
-> Parser Qualifier
-> ParsecT String Integer (State PState) (Def ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"qualif"       Parser () -> Parser Qualifier -> Parser Qualifier
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Sort -> Parser Qualifier
qualifierP Parser Sort
sortP)
    ParsecT String Integer (State PState) (Def ())
-> ParsecT String Integer (State PState) (Def ())
-> ParsecT String Integer (State PState) (Def ())
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> KVar -> Def ()
forall a. KVar -> Def a
Kut   (KVar -> Def ())
-> ParsecT String Integer (State PState) KVar
-> ParsecT String Integer (State PState) (Def ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"cut"          Parser ()
-> ParsecT String Integer (State PState) KVar
-> ParsecT String Integer (State PState) KVar
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ParsecT String Integer (State PState) KVar
kvarP)
    ParsecT String Integer (State PState) (Def ())
-> ParsecT String Integer (State PState) (Def ())
-> ParsecT String Integer (State PState) (Def ())
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Int -> Symbol -> Sort -> Def ()
forall a. Int -> Symbol -> Sort -> Def a
EBind (Int -> Symbol -> Sort -> Def ())
-> ParsecT String Integer (State PState) Int
-> ParsecT String Integer (State PState) (Symbol -> Sort -> Def ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"ebind"        Parser ()
-> ParsecT String Integer (State PState) Int
-> ParsecT String Integer (State PState) Int
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ParsecT String Integer (State PState) Int
intP) ParsecT String Integer (State PState) (Symbol -> Sort -> Def ())
-> Parser Symbol
-> ParsecT String Integer (State PState) (Sort -> Def ())
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Symbol
symbolP ParsecT String Integer (State PState) (Sort -> Def ())
-> Parser Sort -> ParsecT String Integer (State PState) (Def ())
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Parser String
colon Parser String -> Parser Sort -> Parser Sort
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Sort -> Parser Sort
forall u a. ParserT u a -> ParserT u a
braces Parser Sort
sortP)
    ParsecT String Integer (State PState) (Def ())
-> ParsecT String Integer (State PState) (Def ())
-> ParsecT String Integer (State PState) (Def ())
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Int -> Symbol -> SortedReft -> Def ()
forall a. Int -> Symbol -> SortedReft -> Def a
IBind (Int -> Symbol -> SortedReft -> Def ())
-> ParsecT String Integer (State PState) Int
-> ParsecT
     String Integer (State PState) (Symbol -> SortedReft -> Def ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"bind"         Parser ()
-> ParsecT String Integer (State PState) Int
-> ParsecT String Integer (State PState) Int
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ParsecT String Integer (State PState) Int
intP) ParsecT
  String Integer (State PState) (Symbol -> SortedReft -> Def ())
-> Parser Symbol
-> ParsecT String Integer (State PState) (SortedReft -> Def ())
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Symbol
symbolP ParsecT String Integer (State PState) (SortedReft -> Def ())
-> ParsecT String Integer (State PState) SortedReft
-> ParsecT String Integer (State PState) (Def ())
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Parser String
colon Parser String
-> ParsecT String Integer (State PState) SortedReft
-> ParsecT String Integer (State PState) SortedReft
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ParsecT String Integer (State PState) SortedReft
sortedReftP)
    ParsecT String Integer (State PState) (Def ())
-> ParsecT String Integer (State PState) (Def ())
-> ParsecT String Integer (State PState) (Def ())
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String -> Def ()
forall a. String -> Def a
Opt    (String -> Def ())
-> Parser String -> ParsecT String Integer (State PState) (Def ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"fixpoint"    Parser () -> Parser String -> Parser String
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser String
stringLiteral)
    ParsecT String Integer (State PState) (Def ())
-> ParsecT String Integer (State PState) (Def ())
-> ParsecT String Integer (State PState) (Def ())
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Equation -> Def ()
forall a. Equation -> Def a
Def    (Equation -> Def ())
-> Parser Equation
-> ParsecT String Integer (State PState) (Def ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"define"      Parser () -> Parser Equation -> Parser Equation
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Equation
defineP)
    ParsecT String Integer (State PState) (Def ())
-> ParsecT String Integer (State PState) (Def ())
-> ParsecT String Integer (State PState) (Def ())
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Rewrite -> Def ()
forall a. Rewrite -> Def a
Mat    (Rewrite -> Def ())
-> Parser Rewrite -> ParsecT String Integer (State PState) (Def ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"match"       Parser () -> Parser Rewrite -> Parser Rewrite
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Rewrite
matchP)
    ParsecT String Integer (State PState) (Def ())
-> ParsecT String Integer (State PState) (Def ())
-> ParsecT String Integer (State PState) (Def ())
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [(Int, Bool)] -> Def ()
forall a. [(Int, Bool)] -> Def a
Expand ([(Int, Bool)] -> Def ())
-> ParsecT String Integer (State PState) [(Int, Bool)]
-> ParsecT String Integer (State PState) (Def ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"expand"      Parser ()
-> ParsecT String Integer (State PState) [(Int, Bool)]
-> ParsecT String Integer (State PState) [(Int, Bool)]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ParsecT String Integer (State PState) Int
-> Parser Bool
-> ParsecT String Integer (State PState) [(Int, Bool)]
forall a b. Parser a -> Parser b -> Parser [(a, b)]
pairsP ParsecT String Integer (State PState) Int
intP Parser Bool
boolP)
    ParsecT String Integer (State PState) (Def ())
-> ParsecT String Integer (State PState) (Def ())
-> ParsecT String Integer (State PState) (Def ())
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> DataDecl -> Def ()
forall a. DataDecl -> Def a
Adt    (DataDecl -> Def ())
-> Parser DataDecl
-> ParsecT String Integer (State PState) (Def ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"data"        Parser () -> Parser DataDecl -> Parser DataDecl
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser DataDecl
dataDeclP)
    ParsecT String Integer (State PState) (Def ())
-> ParsecT String Integer (State PState) (Def ())
-> ParsecT String Integer (State PState) (Def ())
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Int -> AutoRewrite -> Def ()
forall a. Int -> AutoRewrite -> Def a
AutoRW (Int -> AutoRewrite -> Def ())
-> ParsecT String Integer (State PState) Int
-> ParsecT String Integer (State PState) (AutoRewrite -> Def ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"autorewrite" Parser ()
-> ParsecT String Integer (State PState) Int
-> ParsecT String Integer (State PState) Int
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ParsecT String Integer (State PState) Int
intP) ParsecT String Integer (State PState) (AutoRewrite -> Def ())
-> Parser AutoRewrite
-> ParsecT String Integer (State PState) (Def ())
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser AutoRewrite
autoRewriteP
    ParsecT String Integer (State PState) (Def ())
-> ParsecT String Integer (State PState) (Def ())
-> ParsecT String Integer (State PState) (Def ())
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [(Int, Int)] -> Def ()
forall a. [(Int, Int)] -> Def a
RWMap  ([(Int, Int)] -> Def ())
-> ParsecT String Integer (State PState) [(Int, Int)]
-> ParsecT String Integer (State PState) (Def ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"rewrite"     Parser ()
-> ParsecT String Integer (State PState) [(Int, Int)]
-> ParsecT String Integer (State PState) [(Int, Int)]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ParsecT String Integer (State PState) Int
-> ParsecT String Integer (State PState) Int
-> ParsecT String Integer (State PState) [(Int, Int)]
forall a b. Parser a -> Parser b -> Parser [(a, b)]
pairsP ParsecT String Integer (State PState) Int
intP ParsecT String Integer (State PState) Int
intP)


sortedReftP :: Parser SortedReft
sortedReftP :: ParsecT String Integer (State PState) SortedReft
sortedReftP = Parser (Reft -> SortedReft)
-> ParsecT String Integer (State PState) SortedReft
forall a. Parser (Reft -> a) -> Parser a
refP (Sort -> Reft -> SortedReft
RR (Sort -> Reft -> SortedReft)
-> Parser Sort -> Parser (Reft -> SortedReft)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Parser Sort
sortP Parser Sort -> Parser () -> Parser Sort
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces))

wfCP :: Parser (WfC ())
wfCP :: ParsecT String Integer (State PState) (WfC ())
wfCP = do String -> Parser ()
reserved String
"env"
          IBindEnv
env <- Parser IBindEnv
envP
          String -> Parser ()
reserved String
"reft"
          SortedReft
r   <- ParsecT String Integer (State PState) SortedReft
sortedReftP
          let [WfC ()
w] = IBindEnv -> SortedReft -> () -> [WfC ()]
forall a. Fixpoint a => IBindEnv -> SortedReft -> a -> [WfC a]
wfC IBindEnv
env SortedReft
r ()
          WfC () -> ParsecT String Integer (State PState) (WfC ())
forall (m :: * -> *) a. Monad m => a -> m a
return WfC ()
w

subCP :: Parser (SubC ())
subCP :: ParsecT String Integer (State PState) (SubC ())
subCP = do SourcePos
pos <- ParsecT String Integer (State PState) SourcePos
forall (m :: * -> *) s u. Monad m => ParsecT s u m SourcePos
getPosition
           String -> Parser ()
reserved String
"env"
           IBindEnv
env <- Parser IBindEnv
envP
           String -> Parser ()
reserved String
"lhs"
           SortedReft
lhs <- ParsecT String Integer (State PState) SortedReft
sortedReftP
           String -> Parser ()
reserved String
"rhs"
           SortedReft
rhs <- ParsecT String Integer (State PState) SortedReft
sortedReftP
           String -> Parser ()
reserved String
"id"
           Integer
i   <- Parser Integer
integer Parser Integer -> Parser () -> Parser Integer
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
           [Int]
tag <- Parser [Int]
tagP
           SourcePos
pos' <- ParsecT String Integer (State PState) SourcePos
forall (m :: * -> *) s u. Monad m => ParsecT s u m SourcePos
getPosition
           SubC () -> ParsecT String Integer (State PState) (SubC ())
forall (m :: * -> *) a. Monad m => a -> m a
return (SubC () -> ParsecT String Integer (State PState) (SubC ()))
-> SubC () -> ParsecT String Integer (State PState) (SubC ())
forall a b. (a -> b) -> a -> b
$ IBindEnv
-> SortedReft
-> SortedReft
-> Integer
-> [Int]
-> SourcePos
-> SourcePos
-> SubC ()
subC' IBindEnv
env SortedReft
lhs SortedReft
rhs Integer
i [Int]
tag SourcePos
pos SourcePos
pos'

subC' :: IBindEnv
      -> SortedReft
      -> SortedReft
      -> Integer
      -> Tag
      -> SourcePos
      -> SourcePos
      -> SubC ()
subC' :: IBindEnv
-> SortedReft
-> SortedReft
-> Integer
-> [Int]
-> SourcePos
-> SourcePos
-> SubC ()
subC' IBindEnv
env SortedReft
lhs SortedReft
rhs Integer
i [Int]
tag SourcePos
l SourcePos
l'
  = case [SubC ()]
cs of
      [SubC ()
c] -> SubC ()
c
      [SubC ()]
_   -> Error -> SubC ()
forall a. Error -> a
die (Error -> SubC ()) -> Error -> SubC ()
forall a b. (a -> b) -> a -> b
$ SrcSpan -> Doc -> Error
err SrcSpan
sp (Doc -> Error) -> Doc -> Error
forall a b. (a -> b) -> a -> b
$ Doc
"RHS without single conjunct at" Doc -> Doc -> Doc
<+> SourcePos -> Doc
forall a. PPrint a => a -> Doc
pprint SourcePos
l'
    where
       cs :: [SubC ()]
cs = IBindEnv
-> SortedReft
-> SortedReft
-> Maybe Integer
-> [Int]
-> ()
-> [SubC ()]
forall a.
IBindEnv
-> SortedReft
-> SortedReft
-> Maybe Integer
-> [Int]
-> a
-> [SubC a]
subC IBindEnv
env SortedReft
lhs SortedReft
rhs (Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
i) [Int]
tag ()
       sp :: SrcSpan
sp = SourcePos -> SourcePos -> SrcSpan
SS SourcePos
l SourcePos
l'


tagP  :: Parser [Int]
tagP :: Parser [Int]
tagP  = String -> Parser ()
reserved String
"tag" Parser () -> Parser () -> Parser ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces Parser () -> Parser [Int] -> Parser [Int]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser [Int] -> Parser [Int]
forall u a. ParserT u a -> ParserT u a
brackets (ParsecT String Integer (State PState) Int
-> Parser String -> Parser [Int]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy ParsecT String Integer (State PState) Int
intP Parser String
semi)

envP  :: Parser IBindEnv
envP :: Parser IBindEnv
envP  = do [Int]
binds <- Parser [Int] -> Parser [Int]
forall u a. ParserT u a -> ParserT u a
brackets (Parser [Int] -> Parser [Int]) -> Parser [Int] -> Parser [Int]
forall a b. (a -> b) -> a -> b
$ ParsecT String Integer (State PState) Int
-> Parser String -> Parser [Int]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy (ParsecT String Integer (State PState) Int
intP ParsecT String Integer (State PState) Int
-> Parser () -> ParsecT String Integer (State PState) Int
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces) Parser String
semi
           IBindEnv -> Parser IBindEnv
forall (m :: * -> *) a. Monad m => a -> m a
return (IBindEnv -> Parser IBindEnv) -> IBindEnv -> Parser IBindEnv
forall a b. (a -> b) -> a -> b
$ [Int] -> IBindEnv -> IBindEnv
insertsIBindEnv [Int]
binds IBindEnv
emptyIBindEnv

intP :: Parser Int
intP :: ParsecT String Integer (State PState) Int
intP = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int)
-> Parser Integer -> ParsecT String Integer (State PState) Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Integer
integer

boolP :: Parser Bool
boolP :: Parser Bool
boolP = (String -> Parser ()
reserved String
"True" Parser () -> Parser Bool -> Parser Bool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> Parser Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True)
    Parser Bool -> Parser Bool -> Parser Bool
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (String -> Parser ()
reserved String
"False" Parser () -> Parser Bool -> Parser Bool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> Parser Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False)

defsFInfo :: [Def a] -> FInfo a
defsFInfo :: [Def a] -> FInfo a
defsFInfo [Def a]
defs = {-# SCC "defsFI" #-} HashMap Integer (SubC a)
-> HashMap KVar (WfC a)
-> BindEnv
-> [Int]
-> SEnv Sort
-> SEnv Sort
-> Kuts
-> [Qualifier]
-> HashMap Int a
-> [DataDecl]
-> HOInfo
-> [Triggered Expr]
-> AxiomEnv
-> FInfo a
forall (c :: * -> *) a.
HashMap Integer (c a)
-> HashMap KVar (WfC a)
-> BindEnv
-> [Int]
-> SEnv Sort
-> SEnv Sort
-> Kuts
-> [Qualifier]
-> HashMap Int a
-> [DataDecl]
-> HOInfo
-> [Triggered Expr]
-> AxiomEnv
-> GInfo c a
FI HashMap Integer (SubC a)
cm HashMap KVar (WfC a)
ws BindEnv
bs [Int]
ebs SEnv Sort
lts SEnv Sort
dts Kuts
kts [Qualifier]
qs HashMap Int a
forall a. Monoid a => a
binfo [DataDecl]
adts HOInfo
forall a. Monoid a => a
mempty [Triggered Expr]
forall a. Monoid a => a
mempty AxiomEnv
ae
  where
    cm :: HashMap Integer (SubC a)
cm         = String -> [(Integer, SubC a)] -> HashMap Integer (SubC a)
forall k v.
(?callStack::CallStack, Eq k, Hashable k, Show k) =>
String -> [(k, v)] -> HashMap k v
Misc.safeFromList 
                   String
"defs-cm"        [(SubC a -> Integer
forall (c :: * -> *) a. TaggedC c a => c a -> Integer
cid SubC a
c, SubC a
c)         | Cst SubC a
c       <- [Def a]
defs]
    ws :: HashMap KVar (WfC a)
ws         = String -> [(KVar, WfC a)] -> HashMap KVar (WfC a)
forall k v.
(?callStack::CallStack, Eq k, Hashable k, Show k) =>
String -> [(k, v)] -> HashMap k v
Misc.safeFromList 
                   String
"defs-ws"        [(KVar
i, WfC a
w)              | Wfc WfC a
w    <- [Def a]
defs, let i :: KVar
i = (Symbol, Sort, KVar) -> KVar
forall a b c. (a, b, c) -> c
Misc.thd3 (WfC a -> (Symbol, Sort, KVar)
forall a. WfC a -> (Symbol, Sort, KVar)
wrft WfC a
w)]
    bs :: BindEnv
bs         = [(Int, Symbol, SortedReft)] -> BindEnv
bindEnvFromList  ([(Int, Symbol, SortedReft)] -> BindEnv)
-> [(Int, Symbol, SortedReft)] -> BindEnv
forall a b. (a -> b) -> a -> b
$ [(Int, Symbol, SortedReft)]
exBinds [(Int, Symbol, SortedReft)]
-> [(Int, Symbol, SortedReft)] -> [(Int, Symbol, SortedReft)]
forall a. [a] -> [a] -> [a]
++ [(Int
n,Symbol
x,SortedReft
r)  | IBind Int
n Symbol
x SortedReft
r <- [Def a]
defs] 
    ebs :: [Int]
ebs        =                    [ Int
n                  | (Int
n,Symbol
_,SortedReft
_) <- [(Int, Symbol, SortedReft)]
exBinds] 
    exBinds :: [(Int, Symbol, SortedReft)]
exBinds    =                    [(Int
n, Symbol
x, Sort -> Reft -> SortedReft
RR Sort
t Reft
forall a. Monoid a => a
mempty) | EBind Int
n Symbol
x Sort
t <- [Def a]
defs]
    lts :: SEnv Sort
lts        = [(Symbol, Sort)] -> SEnv Sort
forall a. [(Symbol, a)] -> SEnv a
fromListSEnv       [(Symbol
x, Sort
t)             | Con Symbol
x Sort
t     <- [Def a]
defs]
    dts :: SEnv Sort
dts        = [(Symbol, Sort)] -> SEnv Sort
forall a. [(Symbol, a)] -> SEnv a
fromListSEnv       [(Symbol
x, Sort
t)             | Dis Symbol
x Sort
t     <- [Def a]
defs]
    kts :: Kuts
kts        = HashSet KVar -> Kuts
KS (HashSet KVar -> Kuts) -> HashSet KVar -> Kuts
forall a b. (a -> b) -> a -> b
$ [KVar] -> HashSet KVar
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList    [KVar
k                  | Kut KVar
k       <- [Def a]
defs]
    qs :: [Qualifier]
qs         =                    [Qualifier
q                  | Qul Qualifier
q       <- [Def a]
defs]
    binfo :: a
binfo      = a
forall a. Monoid a => a
mempty
    expand :: HashMap k Bool
expand     = [(k, Bool)] -> HashMap k Bool
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList         [(Int -> k
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i, Bool
f)| Expand [(Int, Bool)]
fs   <- [Def a]
defs, (Int
i,Bool
f) <- [(Int, Bool)]
fs]
    eqs :: [Equation]
eqs        =                    [Equation
e                  | Def Equation
e       <- [Def a]
defs]
    rews :: [Rewrite]
rews       =                    [Rewrite
r                  | Mat Rewrite
r       <- [Def a]
defs]
    autoRWs :: HashMap Int AutoRewrite
autoRWs    = [(Int, AutoRewrite)] -> HashMap Int AutoRewrite
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList         [(Int
arId , AutoRewrite
s)         | AutoRW Int
arId AutoRewrite
s <- [Def a]
defs]
    rwEntries :: [(Int, Int)]
rwEntries  =                    [(Int
i, Int
f)             | RWMap [(Int, Int)]
fs   <- [Def a]
defs, (Int
i,Int
f) <- [(Int, Int)]
fs]
    rwMap :: HashMap k [AutoRewrite]
rwMap      = (HashMap k [AutoRewrite] -> (Int, Int) -> HashMap k [AutoRewrite])
-> HashMap k [AutoRewrite]
-> [(Int, Int)]
-> HashMap k [AutoRewrite]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl HashMap k [AutoRewrite] -> (Int, Int) -> HashMap k [AutoRewrite]
forall k a.
(Hashable k, Integral a, Num k, Eq k) =>
HashMap k [AutoRewrite] -> (a, Int) -> HashMap k [AutoRewrite]
insert ([(k, [AutoRewrite])] -> HashMap k [AutoRewrite]
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList []) [(Int, Int)]
rwEntries
                 where
                   insert :: HashMap k [AutoRewrite] -> (a, Int) -> HashMap k [AutoRewrite]
insert HashMap k [AutoRewrite]
map (a
cid, Int
arId) =
                     case Int -> HashMap Int AutoRewrite -> Maybe AutoRewrite
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Int
arId HashMap Int AutoRewrite
autoRWs of
                       Just AutoRewrite
rewrite ->
                         ([AutoRewrite] -> [AutoRewrite] -> [AutoRewrite])
-> k
-> [AutoRewrite]
-> HashMap k [AutoRewrite]
-> HashMap k [AutoRewrite]
forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> k -> v -> HashMap k v -> HashMap k v
M.insertWith [AutoRewrite] -> [AutoRewrite] -> [AutoRewrite]
forall a. [a] -> [a] -> [a]
(++) (a -> k
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
cid) [AutoRewrite
rewrite] HashMap k [AutoRewrite]
map
                       Maybe AutoRewrite
Nothing ->
                         HashMap k [AutoRewrite]
map
    cid :: c a -> Integer
cid        = Maybe Integer -> Integer
forall a. (?callStack::CallStack) => Maybe a -> a
fromJust (Maybe Integer -> Integer)
-> (c a -> Maybe Integer) -> c a -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. c a -> Maybe Integer
forall (c :: * -> *) a. TaggedC c a => c a -> Maybe Integer
sid
    ae :: AxiomEnv
ae         = [Equation]
-> [Rewrite]
-> HashMap Integer Bool
-> HashMap Integer [AutoRewrite]
-> AxiomEnv
AEnv [Equation]
eqs [Rewrite]
rews HashMap Integer Bool
forall k. (Eq k, Hashable k, Num k) => HashMap k Bool
expand HashMap Integer [AutoRewrite]
forall k. (Hashable k, Num k, Eq k) => HashMap k [AutoRewrite]
rwMap
    adts :: [DataDecl]
adts       =                    [DataDecl
d                  | Adt DataDecl
d       <- [Def a]
defs]
    -- msg    = show $ "#Lits = " ++ (show $ length consts)

---------------------------------------------------------------------
-- | Interacting with Fixpoint --------------------------------------
---------------------------------------------------------------------

fixResultP :: Parser a -> Parser (FixResult a)
fixResultP :: Parser a -> Parser (FixResult a)
fixResultP Parser a
pp
  =  (String -> Parser ()
reserved String
"SAT"   Parser () -> Parser (FixResult a) -> Parser (FixResult a)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FixResult a -> Parser (FixResult a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Stats -> FixResult a
forall a. Stats -> FixResult a
Safe Stats
forall a. Monoid a => a
mempty))
 Parser (FixResult a)
-> Parser (FixResult a) -> Parser (FixResult a)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (String -> Parser ()
reserved String
"UNSAT" Parser () -> Parser (FixResult a) -> Parser (FixResult a)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Stats -> [a] -> FixResult a
forall a. Stats -> [a] -> FixResult a
Unsafe Stats
forall a. Monoid a => a
mempty ([a] -> FixResult a)
-> ParsecT String Integer (State PState) [a]
-> Parser (FixResult a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT String Integer (State PState) [a]
-> ParsecT String Integer (State PState) [a]
forall u a. ParserT u a -> ParserT u a
brackets (Parser a
-> Parser String -> ParsecT String Integer (State PState) [a]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy Parser a
pp Parser String
comma))
 Parser (FixResult a)
-> Parser (FixResult a) -> Parser (FixResult a)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (String -> Parser ()
reserved String
"CRASH" Parser () -> Parser (FixResult a) -> Parser (FixResult a)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser a -> Parser (FixResult a)
forall a. Parser a -> Parser (FixResult a)
crashP Parser a
pp)

crashP :: Parser a -> Parser (FixResult a)
crashP :: Parser a -> Parser (FixResult a)
crashP Parser a
pp = do
  a
i   <- Parser a
pp
  String
msg <- ParsecT String Integer (State PState) Char -> Parser String
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ParsecT String Integer (State PState) Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
anyChar
  FixResult a -> Parser (FixResult a)
forall (m :: * -> *) a. Monad m => a -> m a
return (FixResult a -> Parser (FixResult a))
-> FixResult a -> Parser (FixResult a)
forall a b. (a -> b) -> a -> b
$ [a] -> String -> FixResult a
forall a. [a] -> String -> FixResult a
Crash [a
i] String
msg

predSolP :: Parser Expr
predSolP :: Parser Expr
predSolP = Parser Expr -> Parser Expr
forall u a. ParserT u a -> ParserT u a
parens (Parser Expr
predP  Parser Expr
-> ParsecT String Integer (State PState) [Symbol] -> Parser Expr
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* (Parser String
comma Parser String
-> ParsecT String Integer (State PState) [Symbol]
-> ParsecT String Integer (State PState) [Symbol]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ParsecT String Integer (State PState) [Symbol]
iQualP))

iQualP :: Parser [Symbol]
iQualP :: ParsecT String Integer (State PState) [Symbol]
iQualP = Parser Symbol
upperIdP Parser Symbol
-> ParsecT String Integer (State PState) [Symbol]
-> ParsecT String Integer (State PState) [Symbol]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ParsecT String Integer (State PState) [Symbol]
-> ParsecT String Integer (State PState) [Symbol]
forall u a. ParserT u a -> ParserT u a
parens (Parser Symbol
-> Parser String -> ParsecT String Integer (State PState) [Symbol]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy Parser Symbol
symbolP Parser String
comma)

solution1P :: Parser (KVar, Expr)
solution1P :: Parser (KVar, Expr)
solution1P = do
  String -> Parser ()
reserved String
"solution:"
  KVar
k  <- ParsecT String Integer (State PState) KVar
kvP
  String -> Parser ()
reservedOp String
":="
  [Expr]
ps <- ParsecT String Integer (State PState) [Expr]
-> ParsecT String Integer (State PState) [Expr]
forall u a. ParserT u a -> ParserT u a
brackets (ParsecT String Integer (State PState) [Expr]
 -> ParsecT String Integer (State PState) [Expr])
-> ParsecT String Integer (State PState) [Expr]
-> ParsecT String Integer (State PState) [Expr]
forall a b. (a -> b) -> a -> b
$ Parser Expr
-> Parser String -> ParsecT String Integer (State PState) [Expr]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy Parser Expr
predSolP Parser String
semi
  (KVar, Expr) -> Parser (KVar, Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (KVar
k, Expr -> Expr
forall a. Fixpoint a => a -> a
simplify (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ [Expr] -> Expr
PAnd [Expr]
ps)
  where
    kvP :: ParsecT String Integer (State PState) KVar
kvP = ParsecT String Integer (State PState) KVar
-> ParsecT String Integer (State PState) KVar
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try ParsecT String Integer (State PState) KVar
kvarP ParsecT String Integer (State PState) KVar
-> ParsecT String Integer (State PState) KVar
-> ParsecT String Integer (State PState) KVar
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Symbol -> KVar
KV (Symbol -> KVar)
-> Parser Symbol -> ParsecT String Integer (State PState) KVar
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Symbol
symbolP)

solutionP :: Parser (M.HashMap KVar Expr)
solutionP :: Parser (HashMap KVar Expr)
solutionP = [(KVar, Expr)] -> HashMap KVar Expr
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList ([(KVar, Expr)] -> HashMap KVar Expr)
-> ParsecT String Integer (State PState) [(KVar, Expr)]
-> Parser (HashMap KVar Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser (KVar, Expr)
-> Parser ()
-> ParsecT String Integer (State PState) [(KVar, Expr)]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy Parser (KVar, Expr)
solution1P Parser ()
whiteSpace

solutionFileP :: Parser (FixResult Integer, M.HashMap KVar Expr)
solutionFileP :: Parser (FixResult Integer, HashMap KVar Expr)
solutionFileP = (,) (FixResult Integer
 -> HashMap KVar Expr -> (FixResult Integer, HashMap KVar Expr))
-> ParsecT String Integer (State PState) (FixResult Integer)
-> ParsecT
     String
     Integer
     (State PState)
     (HashMap KVar Expr -> (FixResult Integer, HashMap KVar Expr))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Integer
-> ParsecT String Integer (State PState) (FixResult Integer)
forall a. Parser a -> Parser (FixResult a)
fixResultP Parser Integer
integer ParsecT
  String
  Integer
  (State PState)
  (HashMap KVar Expr -> (FixResult Integer, HashMap KVar Expr))
-> Parser (HashMap KVar Expr)
-> Parser (FixResult Integer, HashMap KVar Expr)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser (HashMap KVar Expr)
solutionP

--------------------------------------------------------------------------------
remainderP :: Parser a -> Parser (a, String, SourcePos)
remainderP :: Parser a -> Parser (a, String, SourcePos)
remainderP Parser a
p
  = do a
res <- Parser a
p
       String
str <- Parser String
forall (m :: * -> *) s u. Monad m => ParsecT s u m s
getInput
       SourcePos
pos <- ParsecT String Integer (State PState) SourcePos
forall (m :: * -> *) s u. Monad m => ParsecT s u m SourcePos
getPosition
       (a, String, SourcePos) -> Parser (a, String, SourcePos)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
res, String
str, SourcePos
pos)


initPState :: Maybe Expr -> PState
initPState :: Maybe Expr -> PState
initPState Maybe Expr
cmpFun = PState :: OpTable -> [Fixity] -> Maybe Expr -> Maybe (Expr -> Expr) -> PState
PState { fixityTable :: OpTable
fixityTable = Maybe Expr -> OpTable
bops Maybe Expr
cmpFun
                           , empList :: Maybe Expr
empList     = Maybe Expr
forall a. Maybe a
Nothing
                           , singList :: Maybe (Expr -> Expr)
singList    = Maybe (Expr -> Expr)
forall a. Maybe a
Nothing
                           , fixityOps :: [Fixity]
fixityOps   = [] 
                           }

doParse' :: Parser a -> SourceName -> String -> a
doParse' :: Parser a -> String -> String -> a
doParse' Parser a
parser String
f String
s
  = case State PState (Either ParseError (a, String, SourcePos))
-> PState -> Either ParseError (a, String, SourcePos)
forall s a. State s a -> s -> a
evalState (ParsecT String Integer (State PState) (a, String, SourcePos)
-> Integer
-> String
-> String
-> State PState (Either ParseError (a, String, SourcePos))
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> u -> String -> s -> m (Either ParseError a)
runParserT (Parser a
-> ParsecT String Integer (State PState) (a, String, SourcePos)
forall a. Parser a -> Parser (a, String, SourcePos)
remainderP (Parser ()
whiteSpace Parser () -> Parser a -> Parser a
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser a
parser)) Integer
0 String
f String
s) (PState -> Either ParseError (a, String, SourcePos))
-> PState -> Either ParseError (a, String, SourcePos)
forall a b. (a -> b) -> a -> b
$ Maybe Expr -> PState
initPState Maybe Expr
forall a. Maybe a
Nothing of
      Left ParseError
e            -> Error -> a
forall a. Error -> a
die (Error -> a) -> Error -> a
forall a b. (a -> b) -> a -> b
$ SrcSpan -> Doc -> Error
err (ParseError -> SrcSpan
errorSpan ParseError
e) (ParseError -> Doc
forall a. Show a => a -> Doc
dErr ParseError
e)
      Right (a
r, String
"", SourcePos
_)  -> a
r
      Right (a
_, String
r, SourcePos
l)   -> Error -> a
forall a. Error -> a
die (Error -> a) -> Error -> a
forall a b. (a -> b) -> a -> b
$ SrcSpan -> Doc -> Error
err (SourcePos -> SourcePos -> SrcSpan
SS SourcePos
l SourcePos
l) (String -> Doc
dRem String
r)
    where
      dErr :: a -> Doc
dErr a
e = [Doc] -> Doc
vcat [ Doc
"parseError"        Doc -> Doc -> Doc
<+> a -> Doc
forall a. Show a => a -> Doc
Misc.tshow a
e
                    , Doc
"when parsing from" Doc -> Doc -> Doc
<+> String -> Doc
text String
f ]
      dRem :: String -> Doc
dRem String
r = [Doc] -> Doc
vcat [ Doc
"doParse has leftover"
                    , Int -> Doc -> Doc
nest Int
4 (String -> Doc
text String
r)
                    , Doc
"when parsing from" Doc -> Doc -> Doc
<+> String -> Doc
text String
f ]


errorSpan :: ParseError -> SrcSpan
errorSpan :: ParseError -> SrcSpan
errorSpan ParseError
e = SourcePos -> SourcePos -> SrcSpan
SS SourcePos
l SourcePos
l where l :: SourcePos
l = ParseError -> SourcePos
errorPos ParseError
e

parseFromFile :: Parser b -> SourceName -> IO b
parseFromFile :: Parser b -> String -> IO b
parseFromFile Parser b
p String
f = Parser b -> String -> String -> b
forall a. Parser a -> String -> String -> a
doParse' Parser b
p String
f (String -> b) -> IO String -> IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> IO String
readFile String
f

freshIntP :: Parser Integer
freshIntP :: Parser Integer
freshIntP = do Integer
n <- Parser Integer
forall (m :: * -> *) s u. Monad m => ParsecT s u m u
getState
               (Integer -> Integer) -> Parser ()
forall (m :: * -> *) u s. Monad m => (u -> u) -> ParsecT s u m ()
updateState (Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1)
               Integer -> Parser Integer
forall (m :: * -> *) a. Monad m => a -> m a
return Integer
n

---------------------------------------------------------------------
-- Standalone SMTLIB2 commands --------------------------------------
---------------------------------------------------------------------
commandsP :: Parser [Command]
commandsP :: Parser [Command]
commandsP = ParsecT String Integer (State PState) Command
-> Parser String -> Parser [Command]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy ParsecT String Integer (State PState) Command
commandP Parser String
semi

commandP :: Parser Command
commandP :: ParsecT String Integer (State PState) Command
commandP
  =  (String -> Parser ()
reserved String
"var"      Parser ()
-> ParsecT String Integer (State PState) Command
-> ParsecT String Integer (State PState) Command
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ParsecT String Integer (State PState) Command
cmdVarP)
 ParsecT String Integer (State PState) Command
-> ParsecT String Integer (State PState) Command
-> ParsecT String Integer (State PState) Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (String -> Parser ()
reserved String
"push"     Parser ()
-> ParsecT String Integer (State PState) Command
-> ParsecT String Integer (State PState) Command
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Command -> ParsecT String Integer (State PState) Command
forall (m :: * -> *) a. Monad m => a -> m a
return Command
Push)
 ParsecT String Integer (State PState) Command
-> ParsecT String Integer (State PState) Command
-> ParsecT String Integer (State PState) Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (String -> Parser ()
reserved String
"pop"      Parser ()
-> ParsecT String Integer (State PState) Command
-> ParsecT String Integer (State PState) Command
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Command -> ParsecT String Integer (State PState) Command
forall (m :: * -> *) a. Monad m => a -> m a
return Command
Pop)
 ParsecT String Integer (State PState) Command
-> ParsecT String Integer (State PState) Command
-> ParsecT String Integer (State PState) Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (String -> Parser ()
reserved String
"check"    Parser ()
-> ParsecT String Integer (State PState) Command
-> ParsecT String Integer (State PState) Command
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Command -> ParsecT String Integer (State PState) Command
forall (m :: * -> *) a. Monad m => a -> m a
return Command
CheckSat)
 ParsecT String Integer (State PState) Command
-> ParsecT String Integer (State PState) Command
-> ParsecT String Integer (State PState) Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (String -> Parser ()
reserved String
"assert"   Parser ()
-> ParsecT String Integer (State PState) Command
-> ParsecT String Integer (State PState) Command
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Maybe Int -> Expr -> Command
Assert Maybe Int
forall a. Maybe a
Nothing (Expr -> Command)
-> Parser Expr -> ParsecT String Integer (State PState) Command
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Expr
predP))
 ParsecT String Integer (State PState) Command
-> ParsecT String Integer (State PState) Command
-> ParsecT String Integer (State PState) Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (String -> Parser ()
reserved String
"distinct" Parser ()
-> ParsecT String Integer (State PState) Command
-> ParsecT String Integer (State PState) Command
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ([Expr] -> Command
Distinct ([Expr] -> Command)
-> ParsecT String Integer (State PState) [Expr]
-> ParsecT String Integer (State PState) Command
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT String Integer (State PState) [Expr]
-> ParsecT String Integer (State PState) [Expr]
forall u a. ParserT u a -> ParserT u a
brackets (Parser Expr
-> Parser String -> ParsecT String Integer (State PState) [Expr]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy Parser Expr
exprP Parser String
comma)))

cmdVarP :: Parser Command
cmdVarP :: ParsecT String Integer (State PState) Command
cmdVarP = String -> ParsecT String Integer (State PState) Command
forall a. (?callStack::CallStack) => String -> a
error String
"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' String
_ = String -> a
forall a. Inputable a => String -> a
rr
  rr    = String -> String -> a
forall a. Inputable a => String -> String -> a
rr' String
""

instance Inputable Symbol where
  rr' :: String -> String -> Symbol
rr' = Parser Symbol -> String -> String -> Symbol
forall a. Parser a -> String -> String -> a
doParse' Parser Symbol
symbolP

instance Inputable Constant where
  rr' :: String -> String -> Constant
rr' = Parser Constant -> String -> String -> Constant
forall a. Parser a -> String -> String -> a
doParse' Parser Constant
constantP

instance Inputable Expr where
  rr' :: String -> String -> Expr
rr' = Parser Expr -> String -> String -> Expr
forall a. Parser a -> String -> String -> a
doParse' Parser Expr
exprP

instance Inputable (FixResult Integer) where
  rr' :: String -> String -> FixResult Integer
rr' = ParsecT String Integer (State PState) (FixResult Integer)
-> String -> String -> FixResult Integer
forall a. Parser a -> String -> String -> a
doParse' (ParsecT String Integer (State PState) (FixResult Integer)
 -> String -> String -> FixResult Integer)
-> ParsecT String Integer (State PState) (FixResult Integer)
-> String
-> String
-> FixResult Integer
forall a b. (a -> b) -> a -> b
$ Parser Integer
-> ParsecT String Integer (State PState) (FixResult Integer)
forall a. Parser a -> Parser (FixResult a)
fixResultP Parser Integer
integer

instance Inputable (FixResult Integer, FixSolution) where
  rr' :: String -> String -> (FixResult Integer, HashMap KVar Expr)
rr' = Parser (FixResult Integer, HashMap KVar Expr)
-> String -> String -> (FixResult Integer, HashMap KVar Expr)
forall a. Parser a -> String -> String -> a
doParse' Parser (FixResult Integer, HashMap KVar Expr)
solutionFileP

instance Inputable (FInfo ()) where
  rr' :: String -> String -> FInfo ()
rr' = {-# SCC "fInfoP" #-} Parser (FInfo ()) -> String -> String -> FInfo ()
forall a. Parser a -> String -> String -> a
doParse' Parser (FInfo ())
fInfoP

instance Inputable (FInfoWithOpts ()) where
  rr' :: String -> String -> FInfoWithOpts ()
rr' = {-# SCC "fInfoWithOptsP" #-} Parser (FInfoWithOpts ()) -> String -> String -> FInfoWithOpts ()
forall a. Parser a -> String -> String -> a
doParse' Parser (FInfoWithOpts ())
fInfoOptP

instance Inputable Command where
  rr' :: String -> String -> Command
rr' = ParsecT String Integer (State PState) Command
-> String -> String -> Command
forall a. Parser a -> String -> String -> a
doParse' ParsecT String Integer (State PState) Command
commandP

instance Inputable [Command] where
  rr' :: String -> String -> [Command]
rr' = Parser [Command] -> String -> String -> [Command]
forall a. Parser a -> String -> String -> a
doParse' Parser [Command]
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)
-}