{-# LANGUAGE FlexibleContexts          #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE TupleSections             #-}
{-# LANGUAGE TypeSynonymInstances      #-}
{-# LANGUAGE UndecidableInstances      #-}
{-# LANGUAGE DeriveGeneric             #-}
{-# LANGUAGE OverloadedStrings         #-}

module Language.Fixpoint.Parse (

  -- * Top Level Class for Parseable Values
    Inputable (..)

  -- * Top Level Class for Parseable Values
  , Parser

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

  -- * Parsing basic entities

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

  -- * Parsing recursive entities
  , exprP       -- Expressions
  , predP       -- Refinement Predicates
  , funAppP     -- Function Applications
  , qualifierP  -- Qualifiers
  , refaP       -- Refa
  , refP        -- (Sorted) Refinements
  , refDefP     -- (Sorted) Refinements with default binder
  , refBindP    -- (Sorted) Refinements with configurable sub-parsers
  , bvSortP     -- Bit-Vector Sort
  , defineP     -- function definition equations (PLE)
  , matchP      -- measure definition equations (PLE)

  -- * Layout
  , indentedBlock
  , indentedLine
  , indentedOrExplicitBlock
  , explicitBlock
  , explicitCommaBlock
  , block
  , spaces
  , setLayout
  , popLayout

  -- * Raw identifiers
  , condIdR

  -- * Lexemes and lexemes with location
  , lexeme
  , located
  , locLexeme
  , locLowerIdP
  , locUpperIdP

  -- * Getting a Fresh Integer while parsing
  , freshIntP

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

  -- * Utilities
  , isSmall
  , isNotReserved

  , initPState, PState (..)

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

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

  ) where

import           Control.Monad.Combinators.Expr
import qualified Data.IntMap.Strict          as IM
import qualified Data.HashMap.Strict         as M
import qualified Data.HashSet                as S
import           Data.List                   (foldl')
import           Data.List.NonEmpty          (NonEmpty(..))
import qualified Data.Text                   as T
import qualified Data.Text.IO                as T
import           Data.Maybe                  (fromJust, fromMaybe)
import           Data.Void
import           Text.Megaparsec             hiding (State, ParseError)
import           Text.Megaparsec.Char
import qualified Text.Megaparsec.Char.Lexer  as L
import           GHC.Generics                (Generic)

import qualified Data.Char                   as Char
import           Language.Fixpoint.Smt.Bitvector
import           Language.Fixpoint.Types.Errors
import qualified Language.Fixpoint.Misc      as Misc
import           Language.Fixpoint.Smt.Types
import           Language.Fixpoint.Types hiding    (mapSort)
import           Text.PrettyPrint.HughesPJ         (text, vcat, (<+>), Doc)

import Control.Monad.State

-- import Debug.Trace

-- Note [Parser monad]
--
-- For reference,
--
-- in *parsec*, the base monad transformer is
--
-- ParsecT s u m a
--
-- where
--
--   s   is the input stream type
--   u   is the user state type
--   m   is the underlying monad
--   a   is the return type
--
-- whereas in *megaparsec*, the base monad transformer is
--
-- ParsecT e s m a
--
-- where
--
--   e   is the custom data component for errors
--   s   is the input stream type
--   m   is the underlying monad
--   a   is the return type
--
-- The Liquid Haskell parser tracks state in 'PState', primarily
-- for operator fixities.
--
-- The old Liquid Haskell parser did not use parsec's "user state"
-- functionality for 'PState', but instead wrapped a state monad
-- in a parsec monad. We do the same thing for megaparsec.
--
-- However, user state was still used for an additional 'Integer'
-- as a unique supply. We incorporate this in the 'PState'.
--
-- Furthermore, we have to decide whether the state in the parser
-- should be "backtracking" or not. "Backtracking" state resets when
-- the parser backtracks, and thus only contains state modifications
-- performed by successful parses. On the other hand, non-backtracking
-- state would contain all modifications made during the parsing
-- process and allow us to observe unsuccessful attempts.
--
-- It turns out that:
--
-- - parsec's old built-in user state is backtracking
-- - using @StateT s (ParsecT ...)@ is backtracking
-- - using @ParsecT ... (StateT s ...)@ is non-backtracking
--
-- We want all our state to be backtracking.
--
-- Note that this is in deviation from what the old LH parser did,
-- but I think that was plainly wrong.

type Parser = StateT PState (Parsec Void String)

-- | The parser state.
--
-- We keep track of the fixities of infix operators.
--
-- We also keep track of whether empty list and singleton lists
-- syntax is allowed (and how they are to be interpreted, if they
-- are).
--
-- We also keep track of an integer counter that can be used to
-- supply unique integers during the parsing process.
--
-- Finally, we keep track of the layout stack.
--
data PState = PState { PState -> OpTable
fixityTable :: OpTable
                     , PState -> [Fixity]
fixityOps   :: [Fixity]
                     , PState -> Maybe Expr
empList     :: Maybe Expr
                     , PState -> Maybe (Expr -> Expr)
singList    :: Maybe (Expr -> Expr)
                     , PState -> Integer
supply      :: !Integer
                     , PState -> LayoutStack
layoutStack :: LayoutStack
                     }

-- | The layout stack tracks columns at which layout blocks
-- have started.
--
data LayoutStack =
    Empty -- ^ no layout info
  | Reset LayoutStack -- ^ in a block not using layout
  | At Pos LayoutStack -- ^ in a block at the given column
  | After Pos LayoutStack -- ^ past a block at the given column
  deriving Int -> LayoutStack -> ShowS
[LayoutStack] -> ShowS
LayoutStack -> String
(Int -> LayoutStack -> ShowS)
-> (LayoutStack -> String)
-> ([LayoutStack] -> ShowS)
-> Show LayoutStack
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [LayoutStack] -> ShowS
$cshowList :: [LayoutStack] -> ShowS
show :: LayoutStack -> String
$cshow :: LayoutStack -> String
showsPrec :: Int -> LayoutStack -> ShowS
$cshowsPrec :: Int -> LayoutStack -> ShowS
Show

-- | Pop the topmost element from the stack.
popLayoutStack :: LayoutStack -> LayoutStack
popLayoutStack :: LayoutStack -> LayoutStack
popLayoutStack LayoutStack
Empty       = String -> LayoutStack
forall a. HasCallStack => String -> a
error String
"unbalanced layout stack"
popLayoutStack (Reset LayoutStack
s)   = LayoutStack
s
popLayoutStack (At Pos
_ LayoutStack
s)    = LayoutStack
s
popLayoutStack (After Pos
_ LayoutStack
s) = LayoutStack
s

-- | Modify the layout stack using the given function.
modifyLayoutStack :: (LayoutStack -> LayoutStack) -> Parser ()
modifyLayoutStack :: (LayoutStack -> LayoutStack) -> Parser ()
modifyLayoutStack LayoutStack -> LayoutStack
f =
  (PState -> PState) -> Parser ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\ PState
s -> PState
s { layoutStack :: LayoutStack
layoutStack = LayoutStack -> LayoutStack
f (PState -> LayoutStack
layoutStack PState
s) })

-- | Start a new layout block at the current indentation level.
setLayout :: Parser ()
setLayout :: Parser ()
setLayout = do
  Pos
i <- StateT PState (Parsec Void String) Pos
forall e s (m :: * -> *). MonadParsec e s m => m Pos
L.indentLevel
  -- traceShow ("setLayout", i) $ pure ()
  (LayoutStack -> LayoutStack) -> Parser ()
modifyLayoutStack (Pos -> LayoutStack -> LayoutStack
At Pos
i)

-- | Temporarily reset the layout information, because we enter
-- a block with explicit separators.
--
resetLayout :: Parser ()
resetLayout :: Parser ()
resetLayout = do
  -- traceShow ("resetLayout") $ pure ()
  (LayoutStack -> LayoutStack) -> Parser ()
modifyLayoutStack LayoutStack -> LayoutStack
Reset

-- | Remove the topmost element from the layout stack.
popLayout :: Parser ()
popLayout :: Parser ()
popLayout = do
  -- traceShow ("popLayout") $ pure ()
  (LayoutStack -> LayoutStack) -> Parser ()
modifyLayoutStack LayoutStack -> LayoutStack
popLayoutStack

-- | Consumes all whitespace, including LH comments.
--
-- Should not be used directly, but primarily via 'lexeme'.
--
-- The only "valid" use case for spaces is in top-level parsing
-- function, to consume initial spaces.
--
spaces :: Parser ()
spaces :: Parser ()
spaces =
  Parser () -> Parser () -> Parser () -> Parser ()
forall e s (m :: * -> *).
MonadParsec e s m =>
m () -> m () -> m () -> m ()
L.space
    Parser ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space1
    Parser ()
lhLineComment
    Parser ()
lhBlockComment

-- | Verify that the current indentation level is in the given
-- relation to the provided reference level, otherwise fail.
--
-- This is a variant of 'indentGuard' provided by megaparsec,
-- only that it does not consume whitespace.
--
guardIndentLevel :: Ordering -> Pos -> Parser ()
guardIndentLevel :: Ordering -> Pos -> Parser ()
guardIndentLevel Ordering
ord Pos
ref = do
  Pos
actual <- StateT PState (Parsec Void String) Pos
forall e s (m :: * -> *). MonadParsec e s m => m Pos
L.indentLevel
  -- traceShow ("guardIndentLevel", actual, ord, ref) $ pure ()
  Bool -> Parser () -> Parser ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Pos -> Pos -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Pos
actual Pos
ref Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
ord)
    (Ordering -> Pos -> Pos -> Parser ()
forall e s (m :: * -> *) a.
MonadParsec e s m =>
Ordering -> Pos -> Pos -> m a
L.incorrectIndent Ordering
ord Pos
ref Pos
actual)

-- | Checks the current indentation level with respect to the
-- current layout stack. May fail. Returns the parser to run
-- after the next token.
--
-- This function is intended to be used within a layout block
-- to check whether the next token is valid within the current
-- block.
--
guardLayout :: Parser (Parser ())
guardLayout :: Parser (Parser ())
guardLayout = do
  LayoutStack
stack <- (PState -> LayoutStack)
-> StateT PState (Parsec Void String) LayoutStack
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets PState -> LayoutStack
layoutStack
  -- traceShow ("guardLayout", stack) $ pure ()
  case LayoutStack
stack of
    At Pos
i LayoutStack
s    -> Ordering -> Pos -> Parser ()
guardIndentLevel Ordering
EQ Pos
i Parser () -> Parser (Parser ()) -> Parser (Parser ())
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser () -> Parser (Parser ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((LayoutStack -> LayoutStack) -> Parser ()
modifyLayoutStack (LayoutStack -> LayoutStack -> LayoutStack
forall a b. a -> b -> a
const (Pos -> LayoutStack -> LayoutStack
After Pos
i (Pos -> LayoutStack -> LayoutStack
At Pos
i LayoutStack
s))))
      -- Note: above, we must really set the stack to 'After i (At i s)' explicitly.
      -- Otherwise, repeated calls to 'guardLayout' at the same column could push
      -- multiple 'After' entries on the stack.
    After Pos
i LayoutStack
_ -> Ordering -> Pos -> Parser ()
guardIndentLevel Ordering
GT Pos
i Parser () -> Parser (Parser ()) -> Parser (Parser ())
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser () -> Parser (Parser ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (() -> Parser ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
    LayoutStack
_         -> Parser () -> Parser (Parser ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (() -> Parser ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())

-- | Checks the current indentation level with respect to the
-- current layout stack. The current indentation level must
-- be strictly greater than the one of the surrounding block.
-- May fail.
--
-- This function is intended to be used before we establish
-- a new, nested, layout block, which should be indented further
-- than the surrounding blocks.
--
strictGuardLayout :: Parser ()
strictGuardLayout :: Parser ()
strictGuardLayout = do
  LayoutStack
stack <- (PState -> LayoutStack)
-> StateT PState (Parsec Void String) LayoutStack
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets PState -> LayoutStack
layoutStack
  -- traceShow ("strictGuardLayout", stack) $ pure ()
  case LayoutStack
stack of
    At Pos
i LayoutStack
_    -> Ordering -> Pos -> Parser ()
guardIndentLevel Ordering
GT Pos
i Parser () -> Parser () -> Parser ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> () -> Parser ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    After Pos
i LayoutStack
_ -> Ordering -> Pos -> Parser ()
guardIndentLevel Ordering
GT Pos
i Parser () -> Parser () -> Parser ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> () -> Parser ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    LayoutStack
_         -> () -> Parser ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()


-- | Indentation-aware lexeme parser. Before parsing, establishes
-- whether we are in a position permitted by the layout stack.
-- After the token, consume whitespace and potentially change state.
--
lexeme :: Parser a -> Parser a
lexeme :: Parser a -> Parser a
lexeme Parser a
p = do
  Parser ()
after <- Parser (Parser ())
guardLayout
  Parser a
p Parser a -> Parser () -> Parser a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
spaces Parser a -> Parser () -> Parser a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
after

-- | Indentation-aware located lexeme parser.
--
-- This is defined in such a way that it determines the actual source range
-- covered by the identifier. I.e., it consumes additional whitespace in the
-- end, but that is not part of the source range reported for the identifier.
--
locLexeme :: Parser a -> Parser (Located a)
locLexeme :: Parser a -> Parser (Located a)
locLexeme Parser a
p = do
  Parser ()
after <- Parser (Parser ())
guardLayout
  SourcePos
l1 <- StateT PState (Parsec Void String) SourcePos
forall e s (m :: * -> *). MonadParsec e s m => m SourcePos
getSourcePos
  a
x <- Parser a
p
  SourcePos
l2 <- StateT PState (Parsec Void String) SourcePos
forall e s (m :: * -> *). MonadParsec e s m => m SourcePos
getSourcePos
  Parser ()
spaces Parser () -> Parser () -> Parser ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
after
  Located a -> Parser (Located a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SourcePos -> SourcePos -> a -> Located a
forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l1 SourcePos
l2 a
x)

-- | Make a parser location-aware.
--
-- This is at the cost of an imprecise span because we still
-- consume spaces in the end first.
--
located :: Parser a -> Parser (Located a)
located :: Parser a -> Parser (Located a)
located Parser a
p = do
  SourcePos
l1 <- StateT PState (Parsec Void String) SourcePos
forall e s (m :: * -> *). MonadParsec e s m => m SourcePos
getSourcePos
  a
x <- Parser a
p
  SourcePos
l2 <- StateT PState (Parsec Void String) SourcePos
forall e s (m :: * -> *). MonadParsec e s m => m SourcePos
getSourcePos
  Located a -> Parser (Located a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SourcePos -> SourcePos -> a -> Located a
forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l1 SourcePos
l2 a
x)

-- | Parse a block delimited by layout.
-- The block must be indented more than the surrounding blocks,
-- otherwise we return an empty list.
--
-- Assumes that the parser for items does not accept the empty string.
--
indentedBlock :: Parser a -> Parser [a]
indentedBlock :: Parser a -> Parser [a]
indentedBlock Parser a
p =
      Parser ()
strictGuardLayout Parser () -> Parser () -> Parser ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser ()
setLayout Parser () -> Parser [a] -> Parser [a]
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser a -> Parser [a]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many (Parser a
p Parser a -> Parser () -> Parser a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
popLayout) Parser [a] -> Parser () -> Parser [a]
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
popLayout
      -- We have to pop after every p, because the first successful
      -- token moves from 'At' to 'After'. We have to pop at the end,
      -- because we want to remove 'At'.
  Parser [a] -> Parser [a] -> Parser [a]
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [a] -> Parser [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
      -- We need to have a fallback with the empty list, because if the
      -- layout check fails, we still want to accept this as an empty block.

-- | Parse a single line that may be continued via layout.
indentedLine :: Parser a -> Parser a
indentedLine :: Parser a -> Parser a
indentedLine Parser a
p =
  Parser ()
setLayout Parser () -> Parser a -> Parser a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser a
p Parser a -> Parser () -> Parser a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
popLayout Parser a -> Parser () -> Parser a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
popLayout
  -- We have to pop twice, because the first successful token
  -- moves from 'At' to 'After', so we have to remove both.

-- | Parse a block of items which can be delimited either via
-- layout or via explicit delimiters as specified.
--
-- Assumes that the parser for items does not accept the empty string.
--
indentedOrExplicitBlock :: Parser open -> Parser close -> Parser sep -> Parser a -> Parser [a]
indentedOrExplicitBlock :: Parser open -> Parser close -> Parser sep -> Parser a -> Parser [a]
indentedOrExplicitBlock Parser open
open Parser close
close Parser sep
sep Parser a
p =
      Parser open -> Parser close -> Parser sep -> Parser a -> Parser [a]
forall open close sep a.
Parser open -> Parser close -> Parser sep -> Parser a -> Parser [a]
explicitBlock Parser open
open Parser close
close Parser sep
sep Parser a
p
  Parser [a] -> Parser [a] -> Parser [a]
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([[a]] -> [a]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[a]] -> [a])
-> StateT PState (Parsec Void String) [[a]] -> Parser [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser [a] -> StateT PState (Parsec Void String) [[a]]
forall a. Parser a -> Parser [a]
indentedBlock (Parser a -> Parser sep -> Parser [a]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepEndBy1 Parser a
p Parser sep
sep))

-- | Parse a block of items that are delimited via explicit delimiters.
-- Layout is disabled/reset for the scope of this block.
--
explicitBlock :: Parser open -> Parser close -> Parser sep -> Parser a -> Parser [a]
explicitBlock :: Parser open -> Parser close -> Parser sep -> Parser a -> Parser [a]
explicitBlock Parser open
open Parser close
close Parser sep
sep Parser a
p =
  Parser ()
resetLayout Parser () -> Parser open -> Parser open
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser open
open Parser open -> Parser [a] -> Parser [a]
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser a -> Parser sep -> Parser [a]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepEndBy Parser a
p Parser sep
sep Parser [a] -> Parser close -> Parser [a]
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser close
close Parser [a] -> Parser () -> Parser [a]
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
popLayout

-- | Symbolic lexeme. Stands on its own.
sym :: String -> Parser String
sym :: String -> Parser String
sym String
x =
  Parser String -> Parser String
forall a. Parser a -> Parser a
lexeme (Tokens String -> StateT PState (Parsec Void String) (Tokens String)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string String
Tokens String
x)

-- | Located variant of 'sym'.
locSym :: String -> Parser (Located String)
locSym :: String -> Parser (Located String)
locSym String
x =
  Parser String -> Parser (Located String)
forall a. Parser a -> Parser (Located a)
locLexeme (Tokens String -> StateT PState (Parsec Void String) (Tokens String)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string String
Tokens String
x)

semi, comma, colon, dcolon, dot :: Parser String
semi :: Parser String
semi   = String -> Parser String
sym String
";"
comma :: Parser String
comma  = String -> Parser String
sym String
","
colon :: Parser String
colon  = String -> Parser String
sym String
":" -- Note: not a reserved symbol; use with care
dcolon :: Parser String
dcolon = String -> Parser String
sym String
"::" -- Note: not a reserved symbol; use with care
dot :: Parser String
dot    = String -> Parser String
sym String
"." -- Note: not a reserved symbol; use with care

-- | Parses a block via layout or explicit braces and semicolons.
--
-- Assumes that the parser for items does not accept the empty string.
--
-- However, even in layouted mode, we are allowing semicolons to
-- separate block contents. We also allow semicolons at the beginning,
-- end, and multiple subsequent semicolons, so the resulting parser
-- provides the illusion of allowing empty items.
--
block :: Parser a -> Parser [a]
block :: Parser a -> Parser [a]
block =
  Parser [String]
-> Parser String -> Parser [String] -> Parser a -> Parser [a]
forall open close sep a.
Parser open -> Parser close -> Parser sep -> Parser a -> Parser [a]
indentedOrExplicitBlock (String -> Parser String
sym String
"{" Parser String -> Parser [String] -> Parser [String]
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser String -> Parser [String]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many Parser String
semi) (String -> Parser String
sym String
"}") (Parser String -> Parser [String]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some Parser String
semi)

-- | Parses a block with explicit braces and commas as separator.
-- Used for record constructors in datatypes.
--
explicitCommaBlock :: Parser a -> Parser [a]
explicitCommaBlock :: Parser a -> Parser [a]
explicitCommaBlock =
  Parser String
-> Parser String -> Parser String -> Parser a -> Parser [a]
forall open close sep a.
Parser open -> Parser close -> Parser sep -> Parser a -> Parser [a]
explicitBlock (String -> Parser String
sym String
"{") (String -> Parser String
sym String
"}") Parser String
comma

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

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"
  ]

-- TODO: This is currently unused.
--
-- The only place where this is used in the original parsec code is in the
-- Text.Parsec.Token.operator parser.
--
_reservedOpNames :: [String]
_reservedOpNames :: [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 = Token.makeTokenParser languageDef
-}

-- | Consumes a line comment.
lhLineComment :: Parser ()
lhLineComment :: Parser ()
lhLineComment =
  Tokens String -> Parser ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Tokens s -> m ()
L.skipLineComment Tokens String
"// "

-- | Consumes a block comment.
lhBlockComment :: Parser ()
lhBlockComment :: Parser ()
lhBlockComment =
  Tokens String -> Tokens String -> Parser ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Tokens s -> Tokens s -> m ()
L.skipBlockComment Tokens String
"/* " Tokens String
"*/"

-- | Parser that consumes a single char within an identifier (not start of identifier).
identLetter :: Parser Char
identLetter :: Parser Char
identLetter =
  Parser Char
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
alphaNumChar Parser Char -> Parser Char -> Parser Char
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Token String] -> StateT PState (Parsec Void String) (Token String)
forall (f :: * -> *) e s (m :: * -> *).
(Foldable f, MonadParsec e s m) =>
f (Token s) -> m (Token s)
oneOf (String
"_" :: String)

-- | Parser that consumes a single char within an operator (not start of operator).
opLetter :: Parser Char
opLetter :: Parser Char
opLetter =
  [Token String] -> StateT PState (Parsec Void String) (Token String)
forall (f :: * -> *) e s (m :: * -> *).
(Foldable f, MonadParsec e s m) =>
f (Token s) -> m (Token s)
oneOf (String
":!#$%&*+./<=>?@\\^|-~'" :: String)

-- | Parser that consumes the given reserved word.
--
-- The input token cannot be longer than the given name.
--
-- NOTE: we currently don't double-check that the reserved word is in the
-- list of reserved words.
--
reserved :: String -> Parser ()
reserved :: String -> Parser ()
reserved String
x =
  Parser String -> Parser ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Parser String -> Parser ()) -> Parser String -> Parser ()
forall a b. (a -> b) -> a -> b
$ Parser String -> Parser String
forall a. Parser a -> Parser a
lexeme (Parser String -> Parser String
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (Tokens String -> StateT PState (Parsec Void String) (Tokens String)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string String
Tokens String
x Parser String -> Parser () -> Parser String
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser Char -> Parser ()
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m ()
notFollowedBy Parser Char
identLetter))

locReserved :: String -> Parser (Located String)
locReserved :: String -> Parser (Located String)
locReserved String
x =
  Parser String -> Parser (Located String)
forall a. Parser a -> Parser (Located a)
locLexeme (Parser String -> Parser String
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (Tokens String -> StateT PState (Parsec Void String) (Tokens String)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string String
Tokens String
x Parser String -> Parser () -> Parser String
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser Char -> Parser ()
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m ()
notFollowedBy Parser Char
identLetter))

-- | Parser that consumes the given reserved operator.
--
-- The input token cannot be longer than the given name.
--
-- NOTE: we currently don't double-check that the reserved operator is in the
-- list of reserved operators.
--
reservedOp :: String -> Parser ()
reservedOp :: String -> Parser ()
reservedOp String
x =
  Parser String -> Parser ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Parser String -> Parser ()) -> Parser String -> Parser ()
forall a b. (a -> b) -> a -> b
$ Parser String -> Parser String
forall a. Parser a -> Parser a
lexeme (Parser String -> Parser String
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (Tokens String -> StateT PState (Parsec Void String) (Tokens String)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string String
Tokens String
x Parser String -> Parser () -> Parser String
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser Char -> Parser ()
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m ()
notFollowedBy Parser Char
opLetter))

-- | Parser that consumes the given symbol.
--
-- The difference with 'reservedOp' is that the given symbol is seen
-- as a token of its own, so the next character that follows does not
-- matter.
--
-- symbol :: String -> Parser String
-- symbol x =
--   L.symbol spaces (string x)

parens, brackets, angles, braces :: Parser a -> Parser a
parens :: Parser a -> Parser a
parens   = Parser String -> Parser String -> Parser a -> Parser a
forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
between (String -> Parser String
sym String
"(") (String -> Parser String
sym String
")")
brackets :: Parser a -> Parser a
brackets = Parser String -> Parser String -> Parser a -> Parser a
forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
between (String -> Parser String
sym String
"[") (String -> Parser String
sym String
"]")
angles :: Parser a -> Parser a
angles   = Parser String -> Parser String -> Parser a -> Parser a
forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
between (String -> Parser String
sym String
"<") (String -> Parser String
sym String
">")
braces :: Parser a -> Parser a
braces   = Parser String -> Parser String -> Parser a -> Parser a
forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
between (String -> Parser String
sym String
"{") (String -> Parser String
sym String
"}")

locParens :: Parser a -> Parser (Located a)
locParens :: Parser a -> Parser (Located a)
locParens Parser a
p =
  (\ (Loc SourcePos
l1 SourcePos
_ String
_) a
a (Loc SourcePos
_ SourcePos
l2 String
_) -> SourcePos -> SourcePos -> a -> Located a
forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l1 SourcePos
l2 a
a) (Located String -> a -> Located String -> Located a)
-> Parser (Located String)
-> StateT
     PState (Parsec Void String) (a -> Located String -> Located a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> Parser (Located String)
locSym String
"(" StateT
  PState (Parsec Void String) (a -> Located String -> Located a)
-> Parser a
-> StateT PState (Parsec Void String) (Located String -> Located a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser a
p StateT PState (Parsec Void String) (Located String -> Located a)
-> Parser (Located String) -> Parser (Located a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> String -> Parser (Located String)
locSym String
")"

-- | Parses a string literal as a lexeme. This is based on megaparsec's
-- 'charLiteral' parser, which claims to handle all the single-character
-- escapes defined by the Haskell grammar.
--
stringLiteral :: Parser String
stringLiteral :: Parser String
stringLiteral =
  Parser String -> Parser String
forall a. Parser a -> Parser a
lexeme Parser String
stringR Parser String -> String -> Parser String
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"string literal"

locStringLiteral :: Parser (Located String)
locStringLiteral :: Parser (Located String)
locStringLiteral =
  Parser String -> Parser (Located String)
forall a. Parser a -> Parser (Located a)
locLexeme Parser String
stringR Parser (Located String) -> String -> Parser (Located String)
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"string literal"

stringR :: Parser String
stringR :: Parser String
stringR =
  Token String -> StateT PState (Parsec Void String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token String
'\"' Parser Char -> Parser String -> Parser String
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Char -> Parser Char -> Parser String
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
manyTill Parser Char
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m Char
L.charLiteral (Token String -> StateT PState (Parsec Void String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token String
'\"')

-- | Consumes a float literal lexeme.
double :: Parser Double
double :: Parser Double
double = Parser Double -> Parser Double
forall a. Parser a -> Parser a
lexeme Parser Double
forall e s (m :: * -> *) a.
(MonadParsec e s m, Token s ~ Char, RealFloat a) =>
m a
L.float Parser Double -> String -> Parser Double
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"float literal"

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

-- | Consumes a natural number literal lexeme, which can be
-- in decimal, octal and hexadecimal representation.
--
-- This does not parse negative integers. Unary minus is available
-- as an operator in the expression language.
--
natural :: Parser Integer
natural :: Parser Integer
natural =
  Parser Integer -> Parser Integer
forall a. Parser a -> Parser a
lexeme Parser Integer
naturalR Parser Integer -> String -> Parser Integer
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"nat literal"

locNatural :: Parser (Located Integer)
locNatural :: Parser (Located Integer)
locNatural =
  Parser Integer -> Parser (Located Integer)
forall a. Parser a -> Parser (Located a)
locLexeme Parser Integer
naturalR Parser (Located Integer) -> String -> Parser (Located Integer)
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"nat literal"

naturalR :: Parser Integer
naturalR :: Parser Integer
naturalR =
      Parser Char -> Parser Char
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (Token String -> StateT PState (Parsec Void String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token String
'0' Parser Char -> Parser Char -> Parser Char
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Token String -> StateT PState (Parsec Void String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char' Char
Token String
'x') Parser Char -> Parser Integer -> Parser Integer
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Integer
forall e s (m :: * -> *) a.
(MonadParsec e s m, Token s ~ Char, Num a) =>
m a
L.hexadecimal
  Parser Integer -> Parser Integer -> Parser Integer
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Char -> Parser Char
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (Token String -> StateT PState (Parsec Void String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token String
'0' Parser Char -> Parser Char -> Parser Char
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Token String -> StateT PState (Parsec Void String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char' Char
Token String
'o') Parser Char -> Parser Integer -> Parser Integer
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Integer
forall e s (m :: * -> *) a.
(MonadParsec e s m, Token s ~ Char, Num a) =>
m a
L.octal
  Parser Integer -> Parser Integer -> Parser Integer
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Integer
forall e s (m :: * -> *) a.
(MonadParsec e s m, Token s ~ Char, Num a) =>
m a
L.decimal

-- | Raw (non-whitespace) parser for an identifier adhering to certain conditions.
--
-- The arguments are as follows, in order:
--
-- * the parser for the initial character,
-- * a predicate indicating which subsequent characters are ok,
-- * a check for the entire identifier to be applied in the end,
-- * an error message to display if the final check fails.
--
condIdR :: Parser Char -> (Char -> Bool) -> (String -> Bool) -> String -> Parser Symbol
condIdR :: Parser Char
-> (Char -> Bool) -> (String -> Bool) -> String -> Parser Symbol
condIdR Parser Char
initial Char -> Bool
okChars String -> Bool
condition String
msg = do
  String
s <- (:) (Char -> ShowS)
-> Parser Char -> StateT PState (Parsec Void String) ShowS
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Char
initial StateT PState (Parsec Void String) ShowS
-> Parser String -> Parser String
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe String
-> (Token String -> Bool)
-> StateT PState (Parsec Void String) (Tokens String)
forall e s (m :: * -> *).
MonadParsec e s m =>
Maybe String -> (Token s -> Bool) -> m (Tokens s)
takeWhileP Maybe String
forall a. Maybe a
Nothing Char -> Bool
Token String -> Bool
okChars
  if String -> Bool
condition String
s
    then Symbol -> Parser Symbol
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol String
s)
    else String -> Parser Symbol
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
msg String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> ShowS
forall a. Show a => a -> String
show String
s)

-- TODO: The use of the following parsers is unsystematic.

-- | Raw parser for an identifier starting with an uppercase letter.
--
-- See Note [symChars].
--
upperIdR :: Parser Symbol
upperIdR :: Parser Symbol
upperIdR =
  Parser Char
-> (Char -> Bool) -> (String -> Bool) -> String -> Parser Symbol
condIdR Parser Char
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
upperChar (Char -> HashSet Char -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet Char
symChars) (Bool -> String -> Bool
forall a b. a -> b -> a
const Bool
True) String
"unexpected"

-- | Raw parser for an identifier starting with a lowercase letter.
--
-- See Note [symChars].
--
lowerIdR :: Parser Symbol
lowerIdR :: Parser Symbol
lowerIdR =
  Parser Char
-> (Char -> Bool) -> (String -> Bool) -> String -> Parser Symbol
condIdR (Parser Char
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
lowerChar Parser Char -> Parser Char -> Parser Char
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Token String -> StateT PState (Parsec Void String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token String
'_') (Char -> HashSet Char -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet Char
symChars) String -> Bool
isNotReserved String
"unexpected reserved word"

-- | Raw parser for an identifier starting with any letter.
--
-- See Note [symChars].
--
symbolR :: Parser Symbol
symbolR :: Parser Symbol
symbolR =
  Parser Char
-> (Char -> Bool) -> (String -> Bool) -> String -> Parser Symbol
condIdR (Parser Char
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
letterChar Parser Char -> Parser Char -> Parser Char
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Token String -> StateT PState (Parsec Void String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token String
'_') (Char -> HashSet Char -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet Char
symChars) String -> Bool
isNotReserved String
"unexpected reserved word"

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)

-- | Predicate version to check if the characer is a valid initial
-- character for 'lowerIdR'.
--
-- TODO: What is this needed for?
--
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
'_'

-- Note [symChars].
--
-- The parser 'symChars' is very permissive. In particular, we allow
-- dots (for qualified names), and characters such as @$@ to be able
-- to refer to identifiers as they occur in e.g. GHC Core.

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

-- | Lexeme version of 'upperIdR'.
--
upperIdP :: Parser Symbol
upperIdP :: Parser Symbol
upperIdP  =
  Parser Symbol -> Parser Symbol
forall a. Parser a -> Parser a
lexeme Parser Symbol
upperIdR Parser Symbol -> String -> Parser Symbol
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"upperIdP"

-- | Lexeme version of 'lowerIdR'.
--
lowerIdP :: Parser Symbol
lowerIdP :: Parser Symbol
lowerIdP  =
  Parser Symbol -> Parser Symbol
forall a. Parser a -> Parser a
lexeme Parser Symbol
lowerIdR Parser Symbol -> String -> Parser Symbol
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"lowerIdP"

-- | Unconstrained identifier, lower- or uppercase.
--
-- Must not be a reserved word.
--
-- Lexeme version of 'symbolR'.
--
symbolP :: Parser Symbol
symbolP :: Parser Symbol
symbolP =
  Parser Symbol -> Parser Symbol
forall a. Parser a -> Parser a
lexeme Parser Symbol
symbolR Parser Symbol -> String -> Parser Symbol
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"identifier"

-- The following are located versions of the lexeme identifier parsers.

locSymbolP, locLowerIdP, locUpperIdP :: Parser LocSymbol
locLowerIdP :: Parser LocSymbol
locLowerIdP = Parser Symbol -> Parser LocSymbol
forall a. Parser a -> Parser (Located a)
locLexeme Parser Symbol
lowerIdR
locUpperIdP :: Parser LocSymbol
locUpperIdP = Parser Symbol -> Parser LocSymbol
forall a. Parser a -> Parser (Located a)
locLexeme Parser Symbol
upperIdR
locSymbolP :: Parser LocSymbol
locSymbolP  = Parser Symbol -> Parser LocSymbol
forall a. Parser a -> Parser (Located a)
locLexeme Parser Symbol
symbolR

-- | Parser for literal numeric constants: floats or integers without sign.
constantP :: Parser Constant
constantP :: Parser Constant
constantP =
     Parser Constant -> Parser Constant
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> 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)   -- float literal
 Parser Constant -> Parser Constant -> Parser Constant
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Integer -> Constant
I (Integer -> Constant) -> Parser Integer -> Parser Constant
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Integer
natural        -- nat literal

-- | Parser for literal string contants.
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

-- | Parser for "atomic" expressions.
--
-- This parser is reused by Liquid Haskell.
--
expr0P :: Parser Expr
expr0P :: Parser Expr
expr0P
  =  Parser Expr
trueP -- constant "true"
 Parser Expr -> Parser Expr -> Parser Expr
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr
falseP -- constant "false"
 Parser Expr -> Parser Expr -> Parser Expr
forall (f :: * -> *) a. Alternative f => f a -> f a -> f 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 -- "if-then-else", starts with "if"
 Parser Expr -> Parser Expr -> Parser Expr
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr -> Parser Expr
coerceP Parser Expr
exprP -- coercion, starts with "coerce"
 Parser Expr -> Parser Expr -> Parser Expr
forall (f :: * -> *) a. Alternative f => f a -> f a -> f 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) -- string literal, starts with double-quote
 Parser Expr -> Parser Expr -> Parser Expr
forall (f :: * -> *) a. Alternative f => f a -> f a -> f 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) -- numeric literal, starts with a digit
 Parser Expr -> Parser Expr -> Parser Expr
forall (f :: * -> *) a. Alternative f => f a -> f a -> f 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) -- constant bottom, equivalent to "false"
 Parser Expr -> Parser Expr -> Parser Expr
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr
lamP -- lambda abstraction, starts with backslash
 Parser Expr -> Parser Expr -> Parser Expr
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr -> Parser Expr
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try Parser Expr
tupleP -- tuple expressions, starts with "("
 Parser Expr -> Parser Expr -> Parser Expr
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr -> Parser Expr
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (Parser Expr -> Parser Expr
forall a. Parser a -> Parser a
parens Parser Expr
exprP) -- parenthesised expression, starts with "("
 Parser Expr -> Parser Expr -> Parser Expr
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr -> Parser Expr
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (Parser Expr -> Parser Expr
forall a. Parser a -> Parser a
parens Parser Expr
exprCastP) -- explicit type annotation, starts with "(", TODO: should be an operator rather than require parentheses?
 Parser Expr -> Parser Expr -> Parser Expr
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Symbol -> Expr
EVar (Symbol -> Expr) -> Parser Symbol -> Parser Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Symbol
symbolP -- identifier, starts with any letter or underscore
 Parser Expr -> Parser Expr -> Parser Expr
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr -> Parser Expr
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (Parser () -> Parser ()
forall a. Parser a -> Parser a
brackets (() -> Parser ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) Parser () -> Parser Expr -> Parser Expr
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Expr
emptyListP) -- empty list, start with "["
 Parser Expr -> Parser Expr -> Parser Expr
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr -> Parser Expr
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (Parser Expr -> Parser Expr
forall a. Parser a -> Parser 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) -- singleton list, starts with "["
 --
 -- Note:
 --
 -- In the parsers above, it is important that *all* parsers starting with "("
 -- are prefixed with "try". This is because expr0P itself is chained with
 -- additional parsers in funAppP ...

emptyListP :: Parser Expr
emptyListP :: Parser Expr
emptyListP = do
  Maybe Expr
e <- PState -> Maybe Expr
empList (PState -> Maybe Expr)
-> StateT PState (Parsec Void String) PState
-> StateT PState (Parsec Void String) (Maybe Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) 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))
-> StateT PState (Parsec Void String) PState
-> StateT PState (Parsec Void String) (Maybe (Expr -> Expr))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) 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

-- | Parser for an explicitly type-annotated expression.
exprCastP :: Parser Expr
exprCastP :: Parser Expr
exprCastP
  = do Expr
e  <- Parser Expr
exprP
       Parser String -> Parser String
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try Parser String
dcolon Parser String -> Parser String -> Parser String
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser String
colon -- allow : or :: *and* allow following symbols
       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

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) <- Parser (Sort, Sort) -> Parser (Sort, Sort)
forall a. Parser a -> Parser a
parens (Parser Sort -> Parser () -> Parser Sort -> Parser (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
-}

-- | Parser for atomic expressions plus function applications.
--
-- Base parser used in 'exprP' which adds in other operators.
--
expr1P :: Parser Expr
expr1P :: Parser Expr
expr1P
  =  Parser Expr -> Parser Expr
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try Parser Expr
funAppP
 Parser Expr -> Parser Expr -> Parser Expr
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr
expr0P

-- | Expressions
exprP :: Parser Expr
exprP :: Parser Expr
exprP =
  do
    OpTable
table <- (PState -> OpTable) -> StateT PState (Parsec Void String) OpTable
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets PState -> OpTable
fixityTable
    Parser Expr
-> [[Operator (StateT PState (Parsec Void String)) Expr]]
-> Parser Expr
forall (m :: * -> *) a.
MonadPlus m =>
m a -> [[Operator m a]] -> m a
makeExprParser Parser Expr
expr1P (OpTable -> [[Operator (StateT PState (Parsec Void String)) Expr]]
flattenOpTable OpTable
table)

data Assoc = AssocNone | AssocLeft | AssocRight

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)}


-- | An OpTable stores operators by their fixity.
--
-- Fixity levels range from 9 (highest) to 0 (lowest).
type OpTable = IM.IntMap [Operator Parser Expr] -- [[Operator Parser Expr]]

-- | Transform an operator table to the form expected by 'makeExprParser',
-- which wants operators sorted by decreasing priority.
--
flattenOpTable :: OpTable -> [[Operator Parser Expr]]
flattenOpTable :: OpTable -> [[Operator (StateT PState (Parsec Void String)) Expr]]
flattenOpTable =
  ((Int, [Operator (StateT PState (Parsec Void String)) Expr])
-> [Operator (StateT PState (Parsec Void String)) Expr]
forall a b. (a, b) -> b
snd ((Int, [Operator (StateT PState (Parsec Void String)) Expr])
 -> [Operator (StateT PState (Parsec Void String)) Expr])
-> [(Int, [Operator (StateT PState (Parsec Void String)) Expr])]
-> [[Operator (StateT PState (Parsec Void String)) Expr]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) ([(Int, [Operator (StateT PState (Parsec Void String)) Expr])]
 -> [[Operator (StateT PState (Parsec Void String)) Expr]])
-> (OpTable
    -> [(Int, [Operator (StateT PState (Parsec Void String)) Expr])])
-> OpTable
-> [[Operator (StateT PState (Parsec Void String)) Expr]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> OpTable
-> [(Int, [Operator (StateT PState (Parsec Void String)) Expr])]
forall a. IntMap a -> [(Int, a)]
IM.toDescList

-- | Add an operator to the parsing state.
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
                    }

-- | Parses any of the known infix operators.
infixSymbolP :: Parser Symbol
infixSymbolP :: Parser Symbol
infixSymbolP = do
  [String]
ops <- PState -> [String]
infixOps (PState -> [String])
-> StateT PState (Parsec Void String) PState -> Parser [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) PState
forall s (m :: * -> *). MonadState s m => m s
get
  [Parser Symbol] -> Parser Symbol
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> 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)

-- | Located version of 'infixSymbolP'.
locInfixSymbolP :: Parser (Located Symbol)
locInfixSymbolP :: Parser LocSymbol
locInfixSymbolP = do
  [String]
ops <- PState -> [String]
infixOps (PState -> [String])
-> StateT PState (Parsec Void String) PState -> Parser [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) PState
forall s (m :: * -> *). MonadState s m => m s
get
  [Parser LocSymbol] -> Parser LocSymbol
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
choice (String -> Parser LocSymbol
reserved' (String -> Parser LocSymbol) -> [String] -> [Parser LocSymbol]
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 LocSymbol
reserved' String
x = String -> Parser (Located String)
locReserved String
x Parser (Located String)
-> (Located String -> Parser LocSymbol) -> Parser LocSymbol
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ (Loc SourcePos
l1 SourcePos
l2 String
_) -> LocSymbol -> Parser LocSymbol
forall (m :: * -> *) a. Monad m => a -> m a
return (SourcePos -> SourcePos -> Symbol -> LocSymbol
forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l1 SourcePos
l2 (String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol String
x))

-- | Helper function that turns an associativity into the right constructor for 'Operator'.
mkInfix :: Assoc -> parser (expr -> expr -> expr) -> Operator parser expr
mkInfix :: Assoc -> parser (expr -> expr -> expr) -> Operator parser expr
mkInfix Assoc
AssocLeft  = parser (expr -> expr -> expr) -> Operator parser expr
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixL
mkInfix Assoc
AssocRight = parser (expr -> expr -> expr) -> Operator parser expr
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixR
mkInfix Assoc
AssocNone  = parser (expr -> expr -> expr) -> Operator parser expr
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixN

-- | Add the given operator to the operator table.
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 (StateT PState (Parsec Void String)) Expr
-> OpTable
-> OpTable
insertOperator (Maybe Int -> Int
makePrec Maybe Int
p) (Assoc
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> Operator (StateT PState (Parsec Void String)) Expr
forall (parser :: * -> *) expr.
Assoc -> parser (expr -> expr -> expr) -> Operator parser expr
mkInfix Assoc
assoc (String -> Parser ()
reservedOp String
x Parser ()
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (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))) OpTable
ops
addOperator (FPrefix Maybe Int
p String
x Maybe (Expr -> Expr)
f) OpTable
ops
 = Int
-> Operator (StateT PState (Parsec Void String)) Expr
-> OpTable
-> OpTable
insertOperator (Maybe Int -> Int
makePrec Maybe Int
p) (StateT PState (Parsec Void String) (Expr -> Expr)
-> Operator (StateT PState (Parsec Void String)) Expr
forall (m :: * -> *) a. m (a -> a) -> Operator m a
Prefix (String -> Parser ()
reservedOp String
x Parser ()
-> StateT PState (Parsec Void String) (Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr) -> StateT PState (Parsec Void String) (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 (StateT PState (Parsec Void String)) Expr
-> OpTable
-> OpTable
insertOperator (Maybe Int -> Int
makePrec Maybe Int
p) (StateT PState (Parsec Void String) (Expr -> Expr)
-> Operator (StateT PState (Parsec Void String)) Expr
forall (m :: * -> *) a. m (a -> a) -> Operator m a
Postfix (String -> Parser ()
reservedOp String
x Parser ()
-> StateT PState (Parsec Void String) (Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr) -> StateT PState (Parsec Void String) (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

-- | Helper function for computing the priority of an operator.
--
-- If no explicit priority is given, a priority of 9 is assumed.
--
makePrec :: Maybe Int -> Int
makePrec :: 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))

-- | Add an operator at the given priority to the operator table.
insertOperator :: Int -> Operator Parser Expr -> OpTable -> OpTable
insertOperator :: Int
-> Operator (StateT PState (Parsec Void String)) Expr
-> OpTable
-> OpTable
insertOperator Int
i Operator (StateT PState (Parsec Void String)) Expr
op = (Maybe [Operator (StateT PState (Parsec Void String)) Expr]
 -> Maybe [Operator (StateT PState (Parsec Void String)) Expr])
-> Int -> OpTable -> OpTable
forall a. (Maybe a -> Maybe a) -> Int -> IntMap a -> IntMap a
IM.alter ([Operator (StateT PState (Parsec Void String)) Expr]
-> Maybe [Operator (StateT PState (Parsec Void String)) Expr]
forall a. a -> Maybe a
Just ([Operator (StateT PState (Parsec Void String)) Expr]
 -> Maybe [Operator (StateT PState (Parsec Void String)) Expr])
-> (Maybe [Operator (StateT PState (Parsec Void String)) Expr]
    -> [Operator (StateT PState (Parsec Void String)) Expr])
-> Maybe [Operator (StateT PState (Parsec Void String)) Expr]
-> Maybe [Operator (StateT PState (Parsec Void String)) Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Operator (StateT PState (Parsec Void String)) Expr
op Operator (StateT PState (Parsec Void String)) Expr
-> [Operator (StateT PState (Parsec Void String)) Expr]
-> [Operator (StateT PState (Parsec Void String)) Expr]
forall a. a -> [a] -> [a]
:) ([Operator (StateT PState (Parsec Void String)) Expr]
 -> [Operator (StateT PState (Parsec Void String)) Expr])
-> (Maybe [Operator (StateT PState (Parsec Void String)) Expr]
    -> [Operator (StateT PState (Parsec Void String)) Expr])
-> Maybe [Operator (StateT PState (Parsec Void String)) Expr]
-> [Operator (StateT PState (Parsec Void String)) Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Operator (StateT PState (Parsec Void String)) Expr]
-> Maybe [Operator (StateT PState (Parsec Void String)) Expr]
-> [Operator (StateT PState (Parsec Void String)) Expr]
forall a. a -> Maybe a -> a
fromMaybe []) Int
i

-- | The initial (empty) operator table.
initOpTable :: OpTable
initOpTable :: OpTable
initOpTable = OpTable
forall a. IntMap a
IM.empty

-- | Built-in operator table, parameterised over the composition function.
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]
builtinOps
  where
    -- Built-in Haskell operators, see https://www.haskell.org/onlinereport/decls.html#fixity
    builtinOps :: [Fixity]
    builtinOps :: [Fixity]
builtinOps = [ 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 :: 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

-- | Parser for function applications.
--
-- Andres, TODO: Why is this so complicated?
--
funAppP :: Parser Expr
funAppP :: Parser Expr
funAppP            =  Parser Expr
litP Parser Expr -> Parser Expr -> Parser Expr
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr
exprFunP Parser Expr -> Parser Expr -> Parser Expr
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr
simpleAppP
  where
    exprFunP :: Parser Expr
exprFunP = LocSymbol -> [Expr] -> Expr
mkEApp (LocSymbol -> [Expr] -> Expr)
-> Parser LocSymbol
-> StateT PState (Parsec Void String) ([Expr] -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser LocSymbol
funSymbolP StateT PState (Parsec Void String) ([Expr] -> Expr)
-> StateT PState (Parsec Void String) [Expr] -> Parser Expr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT PState (Parsec Void String) [Expr]
funRhsP
    funRhsP :: StateT PState (Parsec Void String) [Expr]
funRhsP  =  Parser Expr -> StateT PState (Parsec Void String) [Expr]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some Parser Expr
expr0P
            StateT PState (Parsec Void String) [Expr]
-> StateT PState (Parsec Void String) [Expr]
-> StateT PState (Parsec Void String) [Expr]
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT PState (Parsec Void String) [Expr]
-> StateT PState (Parsec Void String) [Expr]
forall a. Parser a -> Parser a
parens StateT PState (Parsec Void String) [Expr]
innerP
    innerP :: StateT PState (Parsec Void String) [Expr]
innerP   = StateT PState (Parsec Void String) [Expr]
-> StateT PState (Parsec Void String) [Expr]
forall a. Parser a -> Parser a
brackets (Parser Expr
-> Parser String -> StateT PState (Parsec Void String) [Expr]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> 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 -> StateT PState (Parsec Void String) (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Expr -> Parser Expr
forall a. Parser a -> Parser a
parens Parser Expr
exprP StateT PState (Parsec Void String) (Expr -> Expr)
-> Parser Expr -> Parser Expr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Expr -> Parser Expr
forall a. Parser a -> Parser a
parens Parser Expr
exprP
    funSymbolP :: Parser LocSymbol
funSymbolP     = Parser LocSymbol
locSymbolP

-- | Parser for tuple expressions (two or more components).
tupleP :: Parser Expr
tupleP :: Parser Expr
tupleP = do
  Loc SourcePos
l1 SourcePos
l2 (Expr
first, [Expr]
rest) <- Parser (Expr, [Expr]) -> Parser (Located (Expr, [Expr]))
forall a. Parser a -> Parser (Located a)
locParens ((,) (Expr -> [Expr] -> (Expr, [Expr]))
-> Parser Expr
-> StateT PState (Parsec Void String) ([Expr] -> (Expr, [Expr]))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Expr
exprP StateT PState (Parsec Void String) ([Expr] -> (Expr, [Expr]))
-> Parser String
-> StateT PState (Parsec Void String) ([Expr] -> (Expr, [Expr]))
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser String
comma StateT PState (Parsec Void String) ([Expr] -> (Expr, [Expr]))
-> StateT PState (Parsec Void String) [Expr]
-> Parser (Expr, [Expr])
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Expr
-> Parser String -> StateT PState (Parsec Void String) [Expr]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy1 Parser Expr
exprP Parser String
comma) -- at least two components necessary
  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 -> ShowS
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 -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")" -- stored in prefix form
  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

-- | Parser for lambda abstractions.
lamP :: Parser Expr
lamP :: Parser Expr
lamP
  = do String -> Parser ()
reservedOp String
"\\"
       Symbol
x <- Parser Symbol
symbolP
       Parser String
colon -- TODO: this should probably be reservedOp instead
       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

varSortP :: Parser Sort
varSortP :: Parser Sort
varSortP  = Int -> Sort
FVar  (Int -> Sort)
-> StateT PState (Parsec Void String) Int -> Parser Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) Int
-> StateT PState (Parsec Void String) Int
forall a. Parser a -> Parser a
parens StateT PState (Parsec Void String) Int
intP

-- | Parser for function sorts without the "func" keyword.
funcSortP :: Parser Sort
funcSortP :: Parser Sort
funcSortP = Parser Sort -> Parser Sort
forall a. Parser a -> Parser a
parens (Parser Sort -> Parser Sort) -> Parser Sort -> Parser Sort
forall a b. (a -> b) -> a -> b
$ Int -> [Sort] -> Sort
mkFFunc (Int -> [Sort] -> Sort)
-> StateT PState (Parsec Void String) Int
-> StateT PState (Parsec Void String) ([Sort] -> Sort)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) Int
intP StateT PState (Parsec Void String) ([Sort] -> Sort)
-> Parser String
-> StateT PState (Parsec Void String) ([Sort] -> Sort)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser String
comma StateT PState (Parsec Void String) ([Sort] -> Sort)
-> StateT PState (Parsec Void String) [Sort] -> Parser Sort
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT PState (Parsec Void String) [Sort]
sortsP

sortsP :: Parser [Sort]
sortsP :: StateT PState (Parsec Void String) [Sort]
sortsP = StateT PState (Parsec Void String) [Sort]
-> StateT PState (Parsec Void String) [Sort]
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (StateT PState (Parsec Void String) [Sort]
-> StateT PState (Parsec Void String) [Sort]
forall a. Parser a -> Parser a
brackets (Parser Sort
-> Parser String -> StateT PState (Parsec Void String) [Sort]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy Parser Sort
sortP Parser String
semi)) 
      StateT PState (Parsec Void String) [Sort]
-> StateT PState (Parsec Void String) [Sort]
-> StateT PState (Parsec Void String) [Sort]
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (StateT PState (Parsec Void String) [Sort]
-> StateT PState (Parsec Void String) [Sort]
forall a. Parser a -> Parser a
brackets (Parser Sort
-> Parser String -> StateT PState (Parsec Void String) [Sort]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy Parser Sort
sortP Parser String
comma)) 

-- | Parser for sorts (types).
sortP    :: Parser Sort
sortP :: Parser Sort
sortP    = StateT PState (Parsec Void String) [Sort] -> Parser Sort
sortP' (Parser Sort -> StateT PState (Parsec Void String) [Sort]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many Parser Sort
sortArgP)

sortArgP :: Parser Sort
sortArgP :: Parser Sort
sortArgP = StateT PState (Parsec Void String) [Sort] -> Parser Sort
sortP' ([Sort] -> StateT PState (Parsec Void String) [Sort]
forall (m :: * -> *) a. Monad m => a -> m a
return [])

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

-- | Parser for sorts, parameterised over the parser for arguments.
--
-- TODO, Andres: document the parameter better.
--
sortP' :: Parser [Sort] -> Parser Sort
sortP' :: StateT PState (Parsec Void String) [Sort] -> Parser Sort
sortP' StateT PState (Parsec Void String) [Sort]
appArgsP
   =  Parser Sort -> Parser Sort
forall a. Parser a -> Parser a
parens Parser Sort
sortP -- parenthesised sort, starts with "("
  Parser Sort -> Parser Sort -> Parser Sort
forall (f :: * -> *) a. Alternative f => f a -> f a -> f 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) -- function sort, starts with "func"
  Parser Sort -> Parser Sort -> Parser Sort
forall (f :: * -> *) a. Alternative f => f a -> f a -> f 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 (f :: * -> *) a. Applicative f => a -> f a
pure (Sort -> Sort) -> Parser Sort -> Parser Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Sort -> Parser Sort
forall a. Parser a -> Parser a
brackets Parser Sort
sortP)
  -- <|> bvSortP -- Andres: this looks unreachable, as it starts with "("
  Parser Sort -> Parser Sort -> Parser Sort
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (FTycon -> [Sort] -> Sort
fAppTC (FTycon -> [Sort] -> Sort)
-> StateT PState (Parsec Void String) FTycon
-> StateT PState (Parsec Void String) ([Sort] -> Sort)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) FTycon
fTyConP StateT PState (Parsec Void String) ([Sort] -> Sort)
-> StateT PState (Parsec Void String) [Sort] -> Parser Sort
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT PState (Parsec Void String) [Sort]
appArgsP)
  Parser Sort -> Parser Sort -> Parser Sort
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Sort -> [Sort] -> Sort
fApp   (Sort -> [Sort] -> Sort)
-> Parser Sort
-> StateT PState (Parsec Void String) ([Sort] -> Sort)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Sort
tvarP   StateT PState (Parsec Void String) ([Sort] -> Sort)
-> StateT PState (Parsec Void String) [Sort] -> Parser Sort
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT PState (Parsec Void String) [Sort]
appArgsP)

tvarP :: Parser Sort
tvarP :: Parser Sort
tvarP
   =  (Tokens String -> StateT PState (Parsec Void String) (Tokens String)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string Tokens 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 (f :: * -> *) a. Alternative f => f a -> f a -> f 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 :: StateT PState (Parsec Void String) FTycon
fTyConP
  =   (String -> Parser ()
reserved String
"int"     Parser ()
-> StateT PState (Parsec Void String) FTycon
-> StateT PState (Parsec Void String) FTycon
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FTycon -> StateT PState (Parsec Void String) FTycon
forall (m :: * -> *) a. Monad m => a -> m a
return FTycon
intFTyCon)
  StateT PState (Parsec Void String) FTycon
-> StateT PState (Parsec Void String) FTycon
-> StateT PState (Parsec Void String) FTycon
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reserved String
"Integer" Parser ()
-> StateT PState (Parsec Void String) FTycon
-> StateT PState (Parsec Void String) FTycon
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FTycon -> StateT PState (Parsec Void String) FTycon
forall (m :: * -> *) a. Monad m => a -> m a
return FTycon
intFTyCon)
  StateT PState (Parsec Void String) FTycon
-> StateT PState (Parsec Void String) FTycon
-> StateT PState (Parsec Void String) FTycon
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reserved String
"Int"     Parser ()
-> StateT PState (Parsec Void String) FTycon
-> StateT PState (Parsec Void String) FTycon
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FTycon -> StateT PState (Parsec Void String) FTycon
forall (m :: * -> *) a. Monad m => a -> m a
return FTycon
intFTyCon)
  -- <|> (reserved "int"     >> return intFTyCon) -- TODO:AZ duplicate?
  StateT PState (Parsec Void String) FTycon
-> StateT PState (Parsec Void String) FTycon
-> StateT PState (Parsec Void String) FTycon
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reserved String
"real"    Parser ()
-> StateT PState (Parsec Void String) FTycon
-> StateT PState (Parsec Void String) FTycon
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FTycon -> StateT PState (Parsec Void String) FTycon
forall (m :: * -> *) a. Monad m => a -> m a
return FTycon
realFTyCon)
  StateT PState (Parsec Void String) FTycon
-> StateT PState (Parsec Void String) FTycon
-> StateT PState (Parsec Void String) FTycon
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reserved String
"bool"    Parser ()
-> StateT PState (Parsec Void String) FTycon
-> StateT PState (Parsec Void String) FTycon
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FTycon -> StateT PState (Parsec Void String) FTycon
forall (m :: * -> *) a. Monad m => a -> m a
return FTycon
boolFTyCon)
  StateT PState (Parsec Void String) FTycon
-> StateT PState (Parsec Void String) FTycon
-> StateT PState (Parsec Void String) FTycon
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reserved String
"num"     Parser ()
-> StateT PState (Parsec Void String) FTycon
-> StateT PState (Parsec Void String) FTycon
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FTycon -> StateT PState (Parsec Void String) FTycon
forall (m :: * -> *) a. Monad m => a -> m a
return FTycon
numFTyCon)
  StateT PState (Parsec Void String) FTycon
-> StateT PState (Parsec Void String) FTycon
-> StateT PState (Parsec Void String) FTycon
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reserved String
"Str"     Parser ()
-> StateT PState (Parsec Void String) FTycon
-> StateT PState (Parsec Void String) FTycon
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FTycon -> StateT PState (Parsec Void String) FTycon
forall (m :: * -> *) a. Monad m => a -> m a
return FTycon
strFTyCon)
  StateT PState (Parsec Void String) FTycon
-> StateT PState (Parsec Void String) FTycon
-> StateT PState (Parsec Void String) FTycon
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (LocSymbol -> FTycon
symbolFTycon      (LocSymbol -> FTycon)
-> Parser LocSymbol -> StateT PState (Parsec Void String) 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)
-> StateT PState (Parsec Void String) BvSize -> Parser Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> BvSize -> StateT PState (Parsec Void String) BvSize
forall b. String -> b -> StateT PState (Parsec Void String) b
bvSizeP String
"Size32" BvSize
S32 StateT PState (Parsec Void String) BvSize
-> StateT PState (Parsec Void String) BvSize
-> StateT PState (Parsec Void String) BvSize
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> BvSize -> StateT PState (Parsec Void String) BvSize
forall b. String -> b -> StateT PState (Parsec Void String) b
bvSizeP String
"Size64" BvSize
S64)
  where
    bvSizeP :: String -> b -> StateT PState (Parsec Void String) b
bvSizeP String
ss b
s = do
      Parser () -> Parser ()
forall a. Parser a -> Parser 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 -> StateT PState (Parsec Void String) b
forall (m :: * -> *) a. Monad m => a -> m a
return b
s


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

-- | Parser for "atomic" predicates.
--
-- This parser is reused by Liquid Haskell.
--
pred0P :: Parser Expr
pred0P :: Parser Expr
pred0P =  Parser Expr
trueP -- constant "true"
      Parser Expr -> Parser Expr -> Parser Expr
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr
falseP -- constant "false"
      Parser Expr -> Parser Expr -> Parser Expr
forall (f :: * -> *) a. Alternative f => f a -> f a -> f 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 (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr
kvarPredP
      Parser Expr -> Parser Expr -> Parser Expr
forall (f :: * -> *) a. Alternative f => f a -> f a -> f 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 -- "if-then-else", starts with "if"
      Parser Expr -> Parser Expr -> Parser Expr
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr -> Parser Expr
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try Parser Expr
predrP -- binary relation, starts with anything that an expr can start with
      Parser Expr -> Parser Expr -> Parser Expr
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Parser Expr -> Parser Expr
forall a. Parser a -> Parser a
parens Parser Expr
predP) -- parenthesised predicate, starts with "("
      Parser Expr -> Parser Expr -> Parser Expr
forall (f :: * -> *) a. Alternative f => f a -> f a -> f 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 (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr -> Parser Expr
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try Parser Expr
funAppP
      Parser Expr -> Parser Expr -> Parser Expr
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Symbol -> Expr
EVar (Symbol -> Expr) -> Parser Symbol -> Parser Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Symbol
symbolP -- identifier, starts with any letter or underscore
      Parser Expr -> Parser Expr -> Parser Expr
forall (f :: * -> *) a. Alternative f => f a -> f a -> f 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)
-> StateT PState (Parsec Void String) [Expr] -> Parser Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) [Expr]
predsP) -- built-in prefix and
      Parser Expr -> Parser Expr -> Parser Expr
forall (f :: * -> *) a. Alternative f => f a -> f a -> f 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)
-> StateT PState (Parsec Void String) [Expr] -> Parser Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) [Expr]
predsP) -- built-in prefix or

makeUniquePGrad :: Parser Expr
makeUniquePGrad :: Parser Expr
makeUniquePGrad
  = do SourcePos
uniquePos <- StateT PState (Parsec Void String) SourcePos
forall e s (m :: * -> *). MonadParsec e s m => m SourcePos
getSourcePos
       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"

-- | Parser for the reserved constant "true".
trueP :: 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

-- | Parser for the reserved constant "false".
falseP :: Parser Expr
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)
-> StateT PState (Parsec Void String) KVar
-> StateT PState (Parsec Void String) (Subst -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) KVar
kvarP StateT PState (Parsec Void String) (Subst -> Expr)
-> StateT PState (Parsec Void String) Subst -> Parser Expr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT PState (Parsec Void String) Subst
substP

kvarP :: Parser KVar
kvarP :: StateT PState (Parsec Void String) KVar
kvarP = Symbol -> KVar
KV (Symbol -> KVar)
-> Parser Symbol -> StateT PState (Parsec Void String) KVar
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Symbol -> Parser Symbol
forall a. Parser a -> Parser a
lexeme (Token String -> StateT PState (Parsec Void String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token String
'$' Parser Char -> Parser Symbol -> Parser Symbol
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Symbol
symbolR)

substP :: Parser Subst
substP :: StateT PState (Parsec Void String) Subst
substP = [(Symbol, Expr)] -> Subst
mkSubst ([(Symbol, Expr)] -> Subst)
-> StateT PState (Parsec Void String) [(Symbol, Expr)]
-> StateT PState (Parsec Void String) Subst
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) (Symbol, Expr)
-> StateT PState (Parsec Void String) [(Symbol, Expr)]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many (StateT PState (Parsec Void String) (Symbol, Expr)
-> StateT PState (Parsec Void String) (Symbol, Expr)
forall a. Parser a -> Parser a
brackets (StateT PState (Parsec Void String) (Symbol, Expr)
 -> StateT PState (Parsec Void String) (Symbol, Expr))
-> StateT PState (Parsec Void String) (Symbol, Expr)
-> StateT PState (Parsec Void String) (Symbol, Expr)
forall a b. (a -> b) -> a -> b
$ Parser Symbol
-> Parser ()
-> Parser Expr
-> StateT PState (Parsec Void String) (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
":="

-- | Parses a semicolon-separated bracketed list of predicates.
--
-- Used as the argument of the prefix-versions of conjunction and
-- disjunction.
--
predsP :: Parser [Expr]
predsP :: StateT PState (Parsec Void String) [Expr]
predsP = StateT PState (Parsec Void String) [Expr]
-> StateT PState (Parsec Void String) [Expr]
forall a. Parser a -> Parser a
brackets (StateT PState (Parsec Void String) [Expr]
 -> StateT PState (Parsec Void String) [Expr])
-> StateT PState (Parsec Void String) [Expr]
-> StateT PState (Parsec Void String) [Expr]
forall a b. (a -> b) -> a -> b
$ Parser Expr
-> Parser String -> StateT PState (Parsec Void String) [Expr]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy Parser Expr
predP Parser String
semi

-- | Parses a predicate.
--
-- Unlike for expressions, there is a built-in operator list.
--
predP  :: Parser Expr
predP :: Parser Expr
predP  = Parser Expr
-> [[Operator (StateT PState (Parsec Void String)) Expr]]
-> Parser Expr
forall (m :: * -> *) a.
MonadPlus m =>
m a -> [[Operator m a]] -> m a
makeExprParser Parser Expr
pred0P [[Operator (StateT PState (Parsec Void String)) Expr]]
lops
  where
    lops :: [[Operator (StateT PState (Parsec Void String)) Expr]]
lops = [ [StateT PState (Parsec Void String) (Expr -> Expr)
-> Operator (StateT PState (Parsec Void String)) Expr
forall (m :: * -> *) a. m (a -> a) -> Operator m a
Prefix (String -> Parser ()
reservedOp String
"~"    Parser ()
-> StateT PState (Parsec Void String) (Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr) -> StateT PState (Parsec Void String) (Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Expr -> Expr
PNot)]
           , [StateT PState (Parsec Void String) (Expr -> Expr)
-> Operator (StateT PState (Parsec Void String)) Expr
forall (m :: * -> *) a. m (a -> a) -> Operator m a
Prefix (String -> Parser ()
reserved   String
"not"  Parser ()
-> StateT PState (Parsec Void String) (Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr) -> StateT PState (Parsec Void String) (Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Expr -> Expr
PNot)]
           , [StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> Operator (StateT PState (Parsec Void String)) Expr
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixR (String -> Parser ()
reservedOp String
"&&"   Parser ()
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Expr -> Expr -> Expr
pGAnd)]
           , [StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> Operator (StateT PState (Parsec Void String)) Expr
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixR (String -> Parser ()
reservedOp String
"||"   Parser ()
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (\Expr
x Expr
y -> [Expr] -> Expr
POr [Expr
x,Expr
y]))]
           , [StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> Operator (StateT PState (Parsec Void String)) Expr
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixR (String -> Parser ()
reservedOp String
"=>"   Parser ()
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Expr -> Expr -> Expr
PImp)]
           , [StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> Operator (StateT PState (Parsec Void String)) Expr
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixR (String -> Parser ()
reservedOp String
"==>"  Parser ()
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Expr -> Expr -> Expr
PImp)]
           , [StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> Operator (StateT PState (Parsec Void String)) Expr
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixR (String -> Parser ()
reservedOp String
"="    Parser ()
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Expr -> Expr -> Expr
PIff)]
           , [StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> Operator (StateT PState (Parsec Void String)) Expr
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixR (String -> Parser ()
reservedOp String
"<=>"  Parser ()
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Expr -> Expr -> Expr
PIff)]]

-- | Parses a relation predicate.
--
-- Binary relations connect expressions and predicates.
--
predrP :: Parser Expr
predrP :: Parser Expr
predrP =
  (\ Expr
e1 Expr -> Expr -> Expr
r Expr
e2 -> Expr -> Expr -> Expr
r Expr
e1 Expr
e2) (Expr -> (Expr -> Expr -> Expr) -> Expr -> Expr)
-> Parser Expr
-> StateT
     PState
     (Parsec Void String)
     ((Expr -> Expr -> Expr) -> Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Expr
exprP StateT
  PState
  (Parsec Void String)
  ((Expr -> Expr -> Expr) -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
brelP StateT PState (Parsec Void String) (Expr -> Expr)
-> Parser Expr -> Parser Expr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Expr
exprP

-- | Parses a relation symbol.
--
-- There is a built-in table of available relations.
--
brelP ::  Parser (Expr -> Expr -> Expr)
brelP :: StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
brelP =  (String -> Parser ()
reservedOp String
"==" Parser ()
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Eq))
     StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"="  Parser ()
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Eq))
     StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"~~" Parser ()
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Ueq))
     StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"!=" Parser ()
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Ne))
     StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"/=" Parser ()
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Ne))
     StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"!~" Parser ()
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Une))
     StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"<"  Parser ()
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Lt))
     StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"<=" Parser ()
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Le))
     StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
">"  Parser ()
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Gt))
     StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
">=" Parser ()
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (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 e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try ([Expr] -> Expr
pAnd ([Expr] -> Expr)
-> StateT PState (Parsec Void String) [Expr] -> Parser Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) [Expr]
-> StateT PState (Parsec Void String) [Expr]
forall a. Parser a -> Parser a
brackets (Parser Expr
-> Parser String -> StateT PState (Parsec Void String) [Expr]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy Parser Expr
predP Parser String
semi))
     Parser Expr -> Parser Expr -> Parser Expr
forall (f :: * -> *) a. Alternative f => f a -> f a -> f 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 a. Parser a -> Parser 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 ()
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 e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try Parser Symbol
bindP Parser Symbol -> Parser Symbol -> Parser Symbol
forall (f :: * -> *) a. Alternative f => f a -> f a -> f 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
-> StateT PState (Parsec Void String) (Sort -> DataField)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser LocSymbol
locSymbolP StateT PState (Parsec Void String) (Sort -> DataField)
-> Parser String
-> StateT PState (Parsec Void String) (Sort -> DataField)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser String
colon StateT PState (Parsec Void String) (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
-> StateT PState (Parsec Void String) ([DataField] -> DataCtor)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser LocSymbol
locSymbolP
                   StateT PState (Parsec Void String) ([DataField] -> DataCtor)
-> StateT PState (Parsec Void String) [DataField]
-> Parser DataCtor
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT PState (Parsec Void String) [DataField]
-> StateT PState (Parsec Void String) [DataField]
forall a. Parser a -> Parser a
braces (Parser DataField
-> Parser String -> StateT PState (Parsec Void String) [DataField]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> 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)
-> StateT PState (Parsec Void String) FTycon
-> StateT
     PState (Parsec Void String) (Int -> [DataCtor] -> DataDecl)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) FTycon
fTyConP StateT PState (Parsec Void String) (Int -> [DataCtor] -> DataDecl)
-> StateT PState (Parsec Void String) Int
-> StateT PState (Parsec Void String) ([DataCtor] -> DataDecl)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT PState (Parsec Void String) Int
intP StateT PState (Parsec Void String) ([DataCtor] -> DataDecl)
-> Parser ()
-> StateT PState (Parsec Void String) ([DataCtor] -> DataDecl)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* String -> Parser ()
reservedOp String
"="
                   StateT PState (Parsec Void String) ([DataCtor] -> DataDecl)
-> StateT PState (Parsec Void String) [DataCtor] -> Parser DataDecl
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT PState (Parsec Void String) [DataCtor]
-> StateT PState (Parsec Void String) [DataCtor]
forall a. Parser a -> Parser a
brackets (Parser DataCtor -> StateT PState (Parsec Void String) [DataCtor]
forall (m :: * -> *) a. MonadPlus m => m a -> 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    <- StateT PState (Parsec Void String) SourcePos
forall e s (m :: * -> *). MonadParsec e s m => m SourcePos
getSourcePos
  Symbol
n      <- Parser Symbol
upperIdP
  [QualParam]
params <- Parser [QualParam] -> Parser [QualParam]
forall a. Parser a -> Parser a
parens (Parser [QualParam] -> Parser [QualParam])
-> Parser [QualParam] -> Parser [QualParam]
forall a b. (a -> b) -> a -> b
$ StateT PState (Parsec Void String) QualParam
-> Parser String -> Parser [QualParam]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy1 (Parser Sort -> StateT PState (Parsec Void String) 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 -> StateT PState (Parsec Void String) 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 -> StateT PState (Parsec Void String) QualParam
forall (m :: * -> *) a. Monad m => a -> m a
return (QualParam -> StateT PState (Parsec Void String) QualParam)
-> QualParam -> StateT PState (Parsec Void String) 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 (f :: * -> *) a. Alternative f => f a -> f a -> f 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 (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser QualPattern -> Parser QualPattern
forall a. Parser a -> Parser 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)
-> StateT PState (Parsec Void String) (Symbol, Int)
-> Parser QualPattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Symbol
-> Parser String
-> StateT PState (Parsec Void String) Int
-> StateT PState (Parsec Void String) (Symbol, Int)
forall a z b. Parser a -> Parser z -> Parser b -> Parser (a, b)
pairP Parser Symbol
symbolP Parser String
dot StateT PState (Parsec Void String) Int
qpVarP)
              Parser QualPattern -> Parser QualPattern -> Parser QualPattern
forall (f :: * -> *) a. Alternative f => f a -> f a -> f 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)
-> StateT PState (Parsec Void String) (Int, Symbol)
-> Parser QualPattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) Int
-> Parser String
-> Parser Symbol
-> StateT PState (Parsec Void String) (Int, Symbol)
forall a z b. Parser a -> Parser z -> Parser b -> Parser (a, b)
pairP StateT PState (Parsec Void String) Int
qpVarP  Parser String
dot Parser Symbol
symbolP) )


qpVarP :: Parser Int
qpVarP :: StateT PState (Parsec Void String) Int
qpVarP = Token String -> StateT PState (Parsec Void String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token String
'$' Parser Char
-> StateT PState (Parsec Void String) Int
-> StateT PState (Parsec Void String) Int
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT PState (Parsec Void String) 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 -> StateT PState (Parsec Void String) (b -> (a, b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser a
xP StateT PState (Parsec Void String) (b -> (a, b))
-> Parser z -> StateT PState (Parsec Void String) (b -> (a, b))
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser z
sepP StateT PState (Parsec Void String) (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       <- StateT PState (Parsec Void String) SortedReft
-> Parser () -> StateT PState (Parsec Void String) [SortedReft]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy StateT PState (Parsec Void String) SortedReft
sortedReftP Parser ()
spaces
  ()
_          <- Parser ()
spaces
  ()
_          <- String -> Parser ()
reserved String
"="
  ()
_          <- Parser ()
spaces
  (Expr
lhs, Expr
rhs) <- Parser (Expr, Expr) -> Parser (Expr, Expr)
forall a. Parser a -> Parser a
braces (Parser (Expr, Expr) -> Parser (Expr, Expr))
-> Parser (Expr, Expr) -> Parser (Expr, Expr)
forall a b. (a -> b) -> a -> b
$
      Parser Expr -> Parser () -> Parser Expr -> Parser (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 <- Parser [(Symbol, Sort)] -> Parser [(Symbol, Sort)]
forall a. Parser a -> Parser a
parens        (Parser [(Symbol, Sort)] -> Parser [(Symbol, Sort)])
-> Parser [(Symbol, Sort)] -> Parser [(Symbol, Sort)]
forall a b. (a -> b) -> a -> b
$ StateT PState (Parsec Void String) (Symbol, Sort)
-> Parser String -> Parser [(Symbol, Sort)]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy (Parser Sort -> StateT PState (Parsec Void String) (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
braces (
              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
-> StateT
     PState (Parsec Void String) (Symbol -> [Symbol] -> Expr -> Rewrite)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Symbol
symbolP StateT
  PState (Parsec Void String) (Symbol -> [Symbol] -> Expr -> Rewrite)
-> Parser Symbol
-> StateT PState (Parsec Void String) ([Symbol] -> Expr -> Rewrite)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Symbol
symbolP StateT PState (Parsec Void String) ([Symbol] -> Expr -> Rewrite)
-> StateT PState (Parsec Void String) [Symbol]
-> StateT PState (Parsec Void String) (Expr -> Rewrite)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Symbol -> StateT PState (Parsec Void String) [Symbol]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many Parser Symbol
symbolP StateT PState (Parsec Void String) (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 a. Parser a -> Parser a
brackets (Parser [(a, b)] -> Parser [(a, b)])
-> Parser [(a, b)] -> Parser [(a, b)]
forall a b. (a -> b) -> a -> b
$ StateT PState (Parsec Void String) (a, b)
-> Parser String -> Parser [(a, b)]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy1 (Parser a
-> Parser ()
-> Parser b
-> StateT PState (Parsec Void String) (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 -> ShowS
[Def a] -> ShowS
Def a -> String
(Int -> Def a -> ShowS)
-> (Def a -> String) -> ([Def a] -> ShowS) -> Show (Def a)
forall a. Fixpoint a => Int -> Def a -> ShowS
forall a. Fixpoint a => [Def a] -> ShowS
forall a. Fixpoint a => Def a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Def a] -> ShowS
$cshowList :: forall a. Fixpoint a => [Def a] -> ShowS
show :: Def a -> String
$cshow :: forall a. Fixpoint a => Def a -> String
showsPrec :: Int -> Def a -> ShowS
$cshowsPrec :: forall a. Fixpoint a => Int -> Def a -> ShowS
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 <- StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) [Def ()]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many StateT PState (Parsec Void String) (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 ())
-> StateT PState (Parsec Void String) [Def ()] -> Parser (FInfo ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> {- SCC "many-defP" #-} StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) [Def ()]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many StateT PState (Parsec Void String) (Def ())
defP

defP :: Parser (Def ())
defP :: StateT PState (Parsec Void String) (Def ())
defP =  Sort -> Def ()
forall a. Sort -> Def a
Srt   (Sort -> Def ())
-> Parser Sort -> StateT PState (Parsec Void String) (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)
    StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SubC () -> Def ()
forall a. SubC a -> Def a
Cst   (SubC () -> Def ())
-> StateT PState (Parsec Void String) (SubC ())
-> StateT PState (Parsec Void String) (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
-> StateT PState (Parsec Void String) (SubC ())
-> StateT PState (Parsec Void String) (SubC ())
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> {- SCC "subCP" #-} StateT PState (Parsec Void String) (SubC ())
subCP)
    StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> WfC () -> Def ()
forall a. WfC a -> Def a
Wfc   (WfC () -> Def ())
-> StateT PState (Parsec Void String) (WfC ())
-> StateT PState (Parsec Void String) (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
-> StateT PState (Parsec Void String) (WfC ())
-> StateT PState (Parsec Void String) (WfC ())
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> {- SCC "wfCP"  #-} StateT PState (Parsec Void String) (WfC ())
wfCP)
    StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Symbol -> Sort -> Def ()
forall a. Symbol -> Sort -> Def a
Con   (Symbol -> Sort -> Def ())
-> Parser Symbol
-> StateT PState (Parsec Void String) (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) StateT PState (Parsec Void String) (Sort -> Def ())
-> Parser Sort -> StateT PState (Parsec Void String) (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)
    StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Symbol -> Sort -> Def ()
forall a. Symbol -> Sort -> Def a
Dis   (Symbol -> Sort -> Def ())
-> Parser Symbol
-> StateT PState (Parsec Void String) (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) StateT PState (Parsec Void String) (Sort -> Def ())
-> Parser Sort -> StateT PState (Parsec Void String) (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)
    StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> KVar -> Int -> Def ()
forall a. KVar -> Int -> Def a
Pack  (KVar -> Int -> Def ())
-> StateT PState (Parsec Void String) KVar
-> StateT PState (Parsec Void String) (Int -> Def ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"pack"         Parser ()
-> StateT PState (Parsec Void String) KVar
-> StateT PState (Parsec Void String) KVar
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StateT PState (Parsec Void String) KVar
kvarP)   StateT PState (Parsec Void String) (Int -> Def ())
-> StateT PState (Parsec Void String) Int
-> StateT PState (Parsec Void String) (Def ())
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Parser String
colon Parser String
-> StateT PState (Parsec Void String) Int
-> StateT PState (Parsec Void String) Int
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StateT PState (Parsec Void String) Int
intP)
    StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Qualifier -> Def ()
forall a. Qualifier -> Def a
Qul   (Qualifier -> Def ())
-> Parser Qualifier -> StateT PState (Parsec Void String) (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)
    StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> KVar -> Def ()
forall a. KVar -> Def a
Kut   (KVar -> Def ())
-> StateT PState (Parsec Void String) KVar
-> StateT PState (Parsec Void String) (Def ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"cut"          Parser ()
-> StateT PState (Parsec Void String) KVar
-> StateT PState (Parsec Void String) KVar
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StateT PState (Parsec Void String) KVar
kvarP)
    StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Int -> Symbol -> Sort -> Def ()
forall a. Int -> Symbol -> Sort -> Def a
EBind (Int -> Symbol -> Sort -> Def ())
-> StateT PState (Parsec Void String) Int
-> StateT PState (Parsec Void String) (Symbol -> Sort -> Def ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"ebind"        Parser ()
-> StateT PState (Parsec Void String) Int
-> StateT PState (Parsec Void String) Int
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StateT PState (Parsec Void String) Int
intP) StateT PState (Parsec Void String) (Symbol -> Sort -> Def ())
-> Parser Symbol
-> StateT PState (Parsec Void String) (Sort -> Def ())
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Symbol
symbolP StateT PState (Parsec Void String) (Sort -> Def ())
-> Parser Sort -> StateT PState (Parsec Void String) (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 a. Parser a -> Parser a
braces Parser Sort
sortP)
    StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Int -> Symbol -> SortedReft -> Def ()
forall a. Int -> Symbol -> SortedReft -> Def a
IBind (Int -> Symbol -> SortedReft -> Def ())
-> StateT PState (Parsec Void String) Int
-> StateT
     PState (Parsec Void String) (Symbol -> SortedReft -> Def ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"bind"         Parser ()
-> StateT PState (Parsec Void String) Int
-> StateT PState (Parsec Void String) Int
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StateT PState (Parsec Void String) Int
intP) StateT PState (Parsec Void String) (Symbol -> SortedReft -> Def ())
-> Parser Symbol
-> StateT PState (Parsec Void String) (SortedReft -> Def ())
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Symbol
symbolP StateT PState (Parsec Void String) (SortedReft -> Def ())
-> StateT PState (Parsec Void String) SortedReft
-> StateT PState (Parsec Void String) (Def ())
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Parser String
colon Parser String
-> StateT PState (Parsec Void String) SortedReft
-> StateT PState (Parsec Void String) SortedReft
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StateT PState (Parsec Void String) SortedReft
sortedReftP)
    StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> Def ()
forall a. String -> Def a
Opt    (String -> Def ())
-> Parser String -> StateT PState (Parsec Void String) (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)
    StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Equation -> Def ()
forall a. Equation -> Def a
Def    (Equation -> Def ())
-> Parser Equation -> StateT PState (Parsec Void String) (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)
    StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Rewrite -> Def ()
forall a. Rewrite -> Def a
Mat    (Rewrite -> Def ())
-> Parser Rewrite -> StateT PState (Parsec Void String) (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)
    StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [(Int, Bool)] -> Def ()
forall a. [(Int, Bool)] -> Def a
Expand ([(Int, Bool)] -> Def ())
-> StateT PState (Parsec Void String) [(Int, Bool)]
-> StateT PState (Parsec Void String) (Def ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"expand"      Parser ()
-> StateT PState (Parsec Void String) [(Int, Bool)]
-> StateT PState (Parsec Void String) [(Int, Bool)]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StateT PState (Parsec Void String) Int
-> Parser Bool -> StateT PState (Parsec Void String) [(Int, Bool)]
forall a b. Parser a -> Parser b -> Parser [(a, b)]
pairsP StateT PState (Parsec Void String) Int
intP Parser Bool
boolP)
    StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> DataDecl -> Def ()
forall a. DataDecl -> Def a
Adt    (DataDecl -> Def ())
-> Parser DataDecl -> StateT PState (Parsec Void String) (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)
    StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Int -> AutoRewrite -> Def ()
forall a. Int -> AutoRewrite -> Def a
AutoRW (Int -> AutoRewrite -> Def ())
-> StateT PState (Parsec Void String) Int
-> StateT PState (Parsec Void String) (AutoRewrite -> Def ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"autorewrite" Parser ()
-> StateT PState (Parsec Void String) Int
-> StateT PState (Parsec Void String) Int
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StateT PState (Parsec Void String) Int
intP) StateT PState (Parsec Void String) (AutoRewrite -> Def ())
-> Parser AutoRewrite
-> StateT PState (Parsec Void String) (Def ())
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser AutoRewrite
autoRewriteP
    StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [(Int, Int)] -> Def ()
forall a. [(Int, Int)] -> Def a
RWMap  ([(Int, Int)] -> Def ())
-> StateT PState (Parsec Void String) [(Int, Int)]
-> StateT PState (Parsec Void String) (Def ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"rewrite"     Parser ()
-> StateT PState (Parsec Void String) [(Int, Int)]
-> StateT PState (Parsec Void String) [(Int, Int)]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StateT PState (Parsec Void String) Int
-> StateT PState (Parsec Void String) Int
-> StateT PState (Parsec Void String) [(Int, Int)]
forall a b. Parser a -> Parser b -> Parser [(a, b)]
pairsP StateT PState (Parsec Void String) Int
intP StateT PState (Parsec Void String) Int
intP)


sortedReftP :: Parser SortedReft
sortedReftP :: StateT PState (Parsec Void String) SortedReft
sortedReftP = Parser (Reft -> SortedReft)
-> StateT PState (Parsec Void String) 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 ()
spaces))

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

subCP :: Parser (SubC ())
subCP :: StateT PState (Parsec Void String) (SubC ())
subCP = do SourcePos
pos <- StateT PState (Parsec Void String) SourcePos
forall e s (m :: * -> *). MonadParsec e s m => m SourcePos
getSourcePos
           String -> Parser ()
reserved String
"env"
           IBindEnv
env <- Parser IBindEnv
envP
           String -> Parser ()
reserved String
"lhs"
           SortedReft
lhs <- StateT PState (Parsec Void String) SortedReft
sortedReftP
           String -> Parser ()
reserved String
"rhs"
           SortedReft
rhs <- StateT PState (Parsec Void String) SortedReft
sortedReftP
           String -> Parser ()
reserved String
"id"
           Integer
i   <- Parser Integer
natural Parser Integer -> Parser () -> Parser Integer
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
spaces
           [Int]
tag <- Parser [Int]
tagP
           SourcePos
pos' <- StateT PState (Parsec Void String) SourcePos
forall e s (m :: * -> *). MonadParsec e s m => m SourcePos
getSourcePos
           SubC () -> StateT PState (Parsec Void String) (SubC ())
forall (m :: * -> *) a. Monad m => a -> m a
return (SubC () -> StateT PState (Parsec Void String) (SubC ()))
-> SubC () -> StateT PState (Parsec Void String) (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 ()
spaces Parser () -> Parser [Int] -> Parser [Int]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser [Int] -> Parser [Int]
forall a. Parser a -> Parser a
brackets (StateT PState (Parsec Void String) Int
-> Parser String -> Parser [Int]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy StateT PState (Parsec Void String) Int
intP Parser String
semi)

envP  :: Parser IBindEnv
envP :: Parser IBindEnv
envP  = do [Int]
binds <- Parser [Int] -> Parser [Int]
forall a. Parser a -> Parser a
brackets (Parser [Int] -> Parser [Int]) -> Parser [Int] -> Parser [Int]
forall a b. (a -> b) -> a -> b
$ StateT PState (Parsec Void String) Int
-> Parser String -> Parser [Int]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy (StateT PState (Parsec Void String) Int
intP StateT PState (Parsec Void String) Int
-> Parser () -> StateT PState (Parsec Void String) Int
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
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 :: StateT PState (Parsec Void String) Int
intP = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int)
-> Parser Integer -> StateT PState (Parsec Void String) Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Integer
natural

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 (f :: * -> *) a. Alternative f => f a -> f a -> f 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.
(HasCallStack, 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.
(HasCallStack, 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. HasCallStack => 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 (f :: * -> *) a. Alternative f => f a -> f a -> f 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)
-> StateT PState (Parsec Void String) [a] -> Parser (FixResult a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) [a]
-> StateT PState (Parsec Void String) [a]
forall a. Parser a -> Parser a
brackets (Parser a -> Parser String -> StateT PState (Parsec Void String) [a]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy Parser a
pp Parser String
comma))
 Parser (FixResult a)
-> Parser (FixResult a) -> Parser (FixResult a)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f 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 <- Maybe String
-> (Token String -> Bool)
-> StateT PState (Parsec Void String) (Tokens String)
forall e s (m :: * -> *).
MonadParsec e s m =>
Maybe String -> (Token s -> Bool) -> m (Tokens s)
takeWhileP Maybe String
forall a. Maybe a
Nothing (Bool -> Char -> Bool
forall a b. a -> b -> a
const Bool
True) -- consume the rest of the input
  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 a. Parser a -> Parser a
parens (Parser Expr
predP  Parser Expr
-> StateT PState (Parsec Void String) [Symbol] -> Parser Expr
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* (Parser String
comma Parser String
-> StateT PState (Parsec Void String) [Symbol]
-> StateT PState (Parsec Void String) [Symbol]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StateT PState (Parsec Void String) [Symbol]
iQualP))

iQualP :: Parser [Symbol]
iQualP :: StateT PState (Parsec Void String) [Symbol]
iQualP = Parser Symbol
upperIdP Parser Symbol
-> StateT PState (Parsec Void String) [Symbol]
-> StateT PState (Parsec Void String) [Symbol]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StateT PState (Parsec Void String) [Symbol]
-> StateT PState (Parsec Void String) [Symbol]
forall a. Parser a -> Parser a
parens (Parser Symbol
-> Parser String -> StateT PState (Parsec Void String) [Symbol]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> 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  <- StateT PState (Parsec Void String) KVar
kvP
  String -> Parser ()
reservedOp String
":="
  [Expr]
ps <- StateT PState (Parsec Void String) [Expr]
-> StateT PState (Parsec Void String) [Expr]
forall a. Parser a -> Parser a
brackets (StateT PState (Parsec Void String) [Expr]
 -> StateT PState (Parsec Void String) [Expr])
-> StateT PState (Parsec Void String) [Expr]
-> StateT PState (Parsec Void String) [Expr]
forall a b. (a -> b) -> a -> b
$ Parser Expr
-> Parser String -> StateT PState (Parsec Void String) [Expr]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> 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 :: StateT PState (Parsec Void String) KVar
kvP = StateT PState (Parsec Void String) KVar
-> StateT PState (Parsec Void String) KVar
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try StateT PState (Parsec Void String) KVar
kvarP StateT PState (Parsec Void String) KVar
-> StateT PState (Parsec Void String) KVar
-> StateT PState (Parsec Void String) KVar
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Symbol -> KVar
KV (Symbol -> KVar)
-> Parser Symbol -> StateT PState (Parsec Void String) 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)
-> StateT PState (Parsec Void String) [(KVar, Expr)]
-> Parser (HashMap KVar Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser (KVar, Expr)
-> Parser () -> StateT PState (Parsec Void String) [(KVar, Expr)]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy Parser (KVar, Expr)
solution1P Parser ()
spaces

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))
-> StateT PState (Parsec Void String) (FixResult Integer)
-> StateT
     PState
     (Parsec Void String)
     (HashMap KVar Expr -> (FixResult Integer, HashMap KVar Expr))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Integer
-> StateT PState (Parsec Void String) (FixResult Integer)
forall a. Parser a -> Parser (FixResult a)
fixResultP Parser Integer
natural StateT
  PState
  (Parsec Void String)
  (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

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

-- | Parse via the given parser, and obtain the rest of the input
-- as well as the final source position.
--
remainderP :: Parser a -> Parser (a, String, SourcePos)
remainderP :: Parser a -> Parser (a, String, SourcePos)
remainderP Parser a
p
  = do a
res <- Parser a
p
       String
str <- Parser String
forall e s (m :: * -> *). MonadParsec e s m => m s
getInput
       SourcePos
pos <- StateT PState (Parsec Void String) SourcePos
forall e s (m :: * -> *). MonadParsec e s m => m SourcePos
getSourcePos
       (a, String, SourcePos) -> Parser (a, String, SourcePos)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
res, String
str, SourcePos
pos)

-- | Initial parser state.
initPState :: Maybe Expr -> PState
initPState :: Maybe Expr -> PState
initPState Maybe Expr
cmpFun = PState :: OpTable
-> [Fixity]
-> Maybe Expr
-> Maybe (Expr -> Expr)
-> Integer
-> LayoutStack
-> 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   = []
                           , supply :: Integer
supply      = Integer
0
                           , layoutStack :: LayoutStack
layoutStack = LayoutStack
Empty
                           }

-- | Entry point for parsing, for testing.
--
-- Take the top-level parser, the source file name, and the input as a string.
-- Fails with an exception on a parse error.
--
doParse' :: Parser a -> SourceName -> String -> a
doParse' :: Parser a -> String -> String -> a
doParse' Parser a
parser String
fileName String
input =
  case Parsec Void String a
-> String -> String -> Either (ParseErrorBundle String Void) a
forall e s a.
Parsec e s a -> String -> s -> Either (ParseErrorBundle s e) a
runParser (Parser a -> PState -> Parsec Void String a
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (Parser ()
spaces Parser () -> Parser a -> Parser a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser a
parser Parser a -> Parser () -> Parser a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
forall e s (m :: * -> *). MonadParsec e s m => m ()
eof) (Maybe Expr -> PState
initPState Maybe Expr
forall a. Maybe a
Nothing)) String
fileName String
input of
    Left peb :: ParseErrorBundle String Void
peb@(ParseErrorBundle NonEmpty (ParseError String Void)
errors PosState String
posState) -> -- parse errors; we extract the first error from the error bundle
      let
        ((ParseError String Void
_, SourcePos
pos) :| [(ParseError String Void, SourcePos)]
_, PosState String
_) = (ParseError String Void -> Int)
-> NonEmpty (ParseError String Void)
-> PosState String
-> (NonEmpty (ParseError String Void, SourcePos), PosState String)
forall (t :: * -> *) s a.
(Traversable t, Stream s) =>
(a -> Int) -> t a -> PosState s -> (t (a, SourcePos), PosState s)
attachSourcePos ParseError String Void -> Int
forall s e. ParseError s e -> Int
errorOffset NonEmpty (ParseError String Void)
errors PosState String
posState
      in
        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
pos SourcePos
pos) (ParseErrorBundle String Void -> Doc
dErr ParseErrorBundle String Void
peb)
    Right a
r -> a
r -- successful parse with no remaining input
  where
    -- Turns the multiline error string from megaparsec into a pretty-printable Doc.
    dErr :: ParseErrorBundle String Void -> Doc
    dErr :: ParseErrorBundle String Void -> Doc
dErr ParseErrorBundle String Void
e = [Doc] -> Doc
vcat ((String -> Doc) -> [String] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map String -> Doc
text (String -> [String]
lines (ParseErrorBundle String Void -> String
forall s e.
(Stream s, ShowErrorComponent e) =>
ParseErrorBundle s e -> String
errorBundlePretty ParseErrorBundle String Void
e)))

-- | Function to test parsers interactively.
parseTest' :: Show a => Parser a -> String -> IO ()
parseTest' :: Parser a -> String -> IO ()
parseTest' Parser a
parser String
input =
  Parsec Void String a -> String -> IO ()
forall e a s.
(ShowErrorComponent e, Show a, Stream s) =>
Parsec e s a -> s -> IO ()
parseTest (Parser a -> PState -> Parsec Void String a
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT Parser a
parser (Maybe Expr -> PState
initPState Maybe Expr
forall a. Maybe a
Nothing)) String
input

-- errorSpan :: ParseError -> SrcSpan
-- errorSpan e = SS l l where l = errorPos 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

parseFromStdIn :: Parser a -> IO a
parseFromStdIn :: Parser a -> IO a
parseFromStdIn Parser a
p = Parser a -> String -> String -> a
forall a. Parser a -> String -> String -> a
doParse' Parser a
p String
"stdin" (String -> a) -> (Text -> String) -> Text -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
T.unpack (Text -> a) -> IO Text -> IO a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO Text
T.getContents

-- | Obtain a fresh integer during the parsing process.
freshIntP :: Parser Integer
freshIntP :: Parser Integer
freshIntP = do Integer
n <- (PState -> Integer) -> Parser Integer
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets PState -> Integer
supply
               (PState -> PState) -> Parser ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\ PState
s -> PState
s{supply :: Integer
supply = Integer
n 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 = StateT PState (Parsec Void String) Command
-> Parser String -> Parser [Command]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy StateT PState (Parsec Void String) Command
commandP Parser String
semi

commandP :: Parser Command
commandP :: StateT PState (Parsec Void String) Command
commandP
  =  (String -> Parser ()
reserved String
"var"      Parser ()
-> StateT PState (Parsec Void String) Command
-> StateT PState (Parsec Void String) Command
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StateT PState (Parsec Void String) Command
cmdVarP)
 StateT PState (Parsec Void String) Command
-> StateT PState (Parsec Void String) Command
-> StateT PState (Parsec Void String) Command
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reserved String
"push"     Parser ()
-> StateT PState (Parsec Void String) Command
-> StateT PState (Parsec Void String) Command
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Command -> StateT PState (Parsec Void String) Command
forall (m :: * -> *) a. Monad m => a -> m a
return Command
Push)
 StateT PState (Parsec Void String) Command
-> StateT PState (Parsec Void String) Command
-> StateT PState (Parsec Void String) Command
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reserved String
"pop"      Parser ()
-> StateT PState (Parsec Void String) Command
-> StateT PState (Parsec Void String) Command
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Command -> StateT PState (Parsec Void String) Command
forall (m :: * -> *) a. Monad m => a -> m a
return Command
Pop)
 StateT PState (Parsec Void String) Command
-> StateT PState (Parsec Void String) Command
-> StateT PState (Parsec Void String) Command
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reserved String
"check"    Parser ()
-> StateT PState (Parsec Void String) Command
-> StateT PState (Parsec Void String) Command
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Command -> StateT PState (Parsec Void String) Command
forall (m :: * -> *) a. Monad m => a -> m a
return Command
CheckSat)
 StateT PState (Parsec Void String) Command
-> StateT PState (Parsec Void String) Command
-> StateT PState (Parsec Void String) Command
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reserved String
"assert"   Parser ()
-> StateT PState (Parsec Void String) Command
-> StateT PState (Parsec Void String) 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 -> StateT PState (Parsec Void String) Command
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Expr
predP))
 StateT PState (Parsec Void String) Command
-> StateT PState (Parsec Void String) Command
-> StateT PState (Parsec Void String) Command
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reserved String
"distinct" Parser ()
-> StateT PState (Parsec Void String) Command
-> StateT PState (Parsec Void String) Command
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ([Expr] -> Command
Distinct ([Expr] -> Command)
-> StateT PState (Parsec Void String) [Expr]
-> StateT PState (Parsec Void String) Command
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) [Expr]
-> StateT PState (Parsec Void String) [Expr]
forall a. Parser a -> Parser a
brackets (Parser Expr
-> Parser String -> StateT PState (Parsec Void String) [Expr]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy Parser Expr
exprP Parser String
comma)))

cmdVarP :: Parser Command
cmdVarP :: StateT PState (Parsec Void String) Command
cmdVarP = String -> StateT PState (Parsec Void String) Command
forall a. HasCallStack => 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' = StateT PState (Parsec Void String) (FixResult Integer)
-> String -> String -> FixResult Integer
forall a. Parser a -> String -> String -> a
doParse' (StateT PState (Parsec Void String) (FixResult Integer)
 -> String -> String -> FixResult Integer)
-> StateT PState (Parsec Void String) (FixResult Integer)
-> String
-> String
-> FixResult Integer
forall a b. (a -> b) -> a -> b
$ Parser Integer
-> StateT PState (Parsec Void String) (FixResult Integer)
forall a. Parser a -> Parser (FixResult a)
fixResultP Parser Integer
natural

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' = StateT PState (Parsec Void String) Command
-> String -> String -> Command
forall a. Parser a -> String -> String -> a
doParse' StateT PState (Parsec Void String) 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)
-}