{-# LANGUAGE FlexibleContexts          #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# 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
  , 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, addNumTyCon

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

  ) where

import           Control.Monad (unless, void)
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.Types.Errors
import qualified Language.Fixpoint.Misc      as Misc
import           Language.Fixpoint.Smt.Types
import           Language.Fixpoint.Types hiding    (mapSort, fi, params, GInfo(..))
import qualified Language.Fixpoint.Types     as Types (GInfo(FI))
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
                     , PState -> HashSet Symbol
numTyCons   :: !(S.HashSet Symbol)
                     }

-- | 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
$cshowsPrec :: Int -> LayoutStack -> ShowS
showsPrec :: Int -> LayoutStack -> ShowS
$cshow :: LayoutStack -> String
show :: LayoutStack -> String
$cshowList :: [LayoutStack] -> ShowS
showList :: [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 = f (layoutStack 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 s e (m :: * -> *).
(TraversableStream s, 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 s e (m :: * -> *).
(TraversableStream s, 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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser () -> Parser (Parser ())
forall a. a -> StateT PState (Parsec Void String) a
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser () -> Parser (Parser ())
forall a. a -> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (() -> Parser ()
forall a. a -> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
    LayoutStack
_         -> Parser () -> Parser (Parser ())
forall a. a -> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (() -> Parser ()
forall a. a -> StateT PState (Parsec Void String) a
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> () -> Parser ()
forall a. a -> StateT PState (Parsec Void String) a
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> () -> Parser ()
forall a. a -> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    LayoutStack
_         -> () -> Parser ()
forall a. a -> StateT PState (Parsec Void String) a
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 :: forall a. Parser a -> Parser a
lexeme Parser a
p = do
  Parser ()
after <- Parser (Parser ())
guardLayout
  Parser a
p Parser a -> Parser () -> Parser a
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
spaces Parser a -> Parser () -> Parser a
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) 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 :: forall a. Parser a -> Parser (Located a)
locLexeme Parser a
p = do
  Parser ()
after <- Parser (Parser ())
guardLayout
  SourcePos
l1 <- StateT PState (Parsec Void String) SourcePos
forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
getSourcePos
  a
x <- Parser a
p
  SourcePos
l2 <- StateT PState (Parsec Void String) SourcePos
forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
getSourcePos
  Parser ()
spaces Parser () -> Parser () -> Parser ()
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
after
  Located a -> Parser (Located a)
forall a. a -> StateT PState (Parsec Void String) 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 :: forall a. Parser a -> Parser (Located a)
located Parser a
p = do
  SourcePos
l1 <- StateT PState (Parsec Void String) SourcePos
forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
getSourcePos
  a
x <- Parser a
p
  SourcePos
l2 <- StateT PState (Parsec Void String) SourcePos
forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
getSourcePos
  Located a -> Parser (Located a)
forall a. a -> StateT PState (Parsec Void String) 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 :: forall a. Parser a -> Parser [a]
indentedBlock Parser a
p =
      Parser ()
strictGuardLayout Parser () -> Parser () -> Parser ()
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser ()
setLayout Parser ()
-> StateT PState (Parsec Void String) [a]
-> StateT PState (Parsec Void String) [a]
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser a -> StateT PState (Parsec Void String) [a]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many (Parser a
p Parser a -> Parser () -> Parser a
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
popLayout) StateT PState (Parsec Void String) [a]
-> Parser () -> StateT PState (Parsec Void String) [a]
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) 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'.
  StateT PState (Parsec Void String) [a]
-> StateT PState (Parsec Void String) [a]
-> StateT PState (Parsec Void String) [a]
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [a] -> StateT PState (Parsec Void String) [a]
forall a. a -> StateT PState (Parsec Void String) 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 :: forall a. Parser a -> Parser a
indentedLine Parser a
p =
  Parser ()
setLayout Parser () -> Parser a -> Parser a
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser a
p Parser a -> Parser () -> Parser a
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
popLayout Parser a -> Parser () -> Parser a
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) 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 :: forall open close sep a.
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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) 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 :: 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 ()
resetLayout Parser () -> Parser open -> Parser open
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser open
open Parser open
-> StateT PState (Parsec Void String) [a]
-> StateT PState (Parsec Void String) [a]
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser a -> Parser sep -> StateT PState (Parsec Void String) [a]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepEndBy Parser a
p Parser sep
sep StateT PState (Parsec Void String) [a]
-> Parser close -> StateT PState (Parsec Void String) [a]
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser close
close StateT PState (Parsec Void String) [a]
-> Parser () -> StateT PState (Parsec Void String) [a]
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) 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 :: forall a. 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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
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 :: forall a. 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 =>
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
StateT PState (Parsec Void String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
alphaNumChar Parser Char -> Parser Char -> Parser Char
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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 =
  StateT PState (Parsec Void String) (Tokens String) -> Parser ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (StateT PState (Parsec Void String) (Tokens String) -> Parser ())
-> StateT PState (Parsec Void String) (Tokens String) -> Parser ()
forall a b. (a -> b) -> a -> b
$ StateT PState (Parsec Void String) (Tokens String)
-> StateT PState (Parsec Void String) (Tokens String)
forall a. Parser a -> Parser a
lexeme (StateT PState (Parsec Void String) (Tokens String)
-> StateT PState (Parsec Void String) (Tokens String)
forall a. Parser a -> Parser a
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 StateT PState (Parsec Void String) (Tokens String)
-> Parser () -> StateT PState (Parsec Void String) (Tokens String)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser Char -> Parser ()
forall a. StateT PState (Parsec Void String) a -> 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 a. Parser a -> Parser a
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser Char -> Parser ()
forall a. StateT PState (Parsec Void String) a -> 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 =
  StateT PState (Parsec Void String) (Tokens String) -> Parser ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (StateT PState (Parsec Void String) (Tokens String) -> Parser ())
-> StateT PState (Parsec Void String) (Tokens String) -> Parser ()
forall a b. (a -> b) -> a -> b
$ StateT PState (Parsec Void String) (Tokens String)
-> StateT PState (Parsec Void String) (Tokens String)
forall a. Parser a -> Parser a
lexeme (StateT PState (Parsec Void String) (Tokens String)
-> StateT PState (Parsec Void String) (Tokens String)
forall a. Parser a -> Parser a
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 StateT PState (Parsec Void String) (Tokens String)
-> Parser () -> StateT PState (Parsec Void String) (Tokens String)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser Char -> Parser ()
forall a. StateT PState (Parsec Void String) a -> 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 :: forall a. Parser a -> Parser a
parens   = Parser String
-> Parser String
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) 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 :: forall a. Parser a -> Parser a
brackets = Parser String
-> Parser String
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) 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 :: forall a. Parser a -> Parser a
angles   = Parser String
-> Parser String
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) 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 :: forall a. Parser a -> Parser a
braces   = Parser String
-> Parser String
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) 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 :: forall a. 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 a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
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)
-> StateT PState (Parsec Void String) (Located a)
forall a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
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 a. Parser a -> Parser a
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Char -> Parser Char
forall a. Parser a -> Parser a
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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 a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
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 a. a -> StateT PState (Parsec Void String) a
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 a. String -> StateT PState (Parsec Void String) a
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
StateT PState (Parsec Void String) (Token String)
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
StateT PState (Parsec Void String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
lowerChar Parser Char -> Parser Char -> Parser Char
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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
StateT PState (Parsec Void String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
letterChar Parser Char -> Parser Char -> Parser Char
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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 a. Parser a -> Parser a
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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr
falseP -- constant "false"
 Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"_|_" Parser () -> Parser Expr -> Parser Expr
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Expr -> Parser Expr
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
EBot) -- constant bottom, equivalent to "false"
 Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr -> Parser Expr
forall a. Parser a -> Parser a
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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr -> Parser Expr
forall a. Parser a -> Parser a
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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr -> Parser Expr
forall a. Parser a -> Parser a
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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr -> Parser Expr
forall a. Parser a -> Parser a
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 a. a -> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) Parser () -> Parser Expr -> Parser Expr
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr -> Parser Expr
forall a. Parser a -> Parser a
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 a b.
StateT PState (Parsec Void String) a
-> (a -> StateT PState (Parsec Void String) b)
-> StateT PState (Parsec Void String) b
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)
-> StateT PState (Parsec Void String) (Maybe Expr)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets PState -> Maybe Expr
empList
  case Maybe Expr
e of
    Maybe Expr
Nothing -> String -> Parser Expr
forall a. String -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"No parsing support for empty lists"
    Just Expr
s  -> Expr -> Parser Expr
forall a. a -> StateT PState (Parsec Void String) a
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))
-> StateT PState (Parsec Void String) (Maybe (Expr -> Expr))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets PState -> Maybe (Expr -> Expr)
singList
  case Maybe (Expr -> Expr)
f of
    Maybe (Expr -> Expr)
Nothing -> String -> Parser Expr
forall a. String -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"No parsing support for singleton lists"
    Just Expr -> Expr
s  -> Expr -> Parser Expr
forall a. a -> StateT PState (Parsec Void String) a
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
       String
_ <- Parser String -> Parser String
forall a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try Parser String
dcolon Parser String -> Parser String -> Parser String
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser String
colon -- allow : or :: *and* allow following symbols
       Expr -> Sort -> Expr
ECst Expr
e (Sort -> Expr)
-> StateT PState (Parsec Void String) Sort -> Parser Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) Sort
sortP

fastIfP :: (Expr -> a -> a -> a) -> Parser a -> Parser a
fastIfP :: forall a. (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"
       Expr -> a -> a -> a
f Expr
p a
b1 (a -> a) -> Parser a -> Parser a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser a
bodyP

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 (StateT PState (Parsec Void String) Sort
-> Parser ()
-> StateT PState (Parsec Void String) Sort
-> Parser (Sort, Sort)
forall a z b. Parser a -> Parser z -> Parser b -> Parser (a, b)
pairP StateT PState (Parsec Void String) Sort
sortP (String -> Parser ()
reservedOp String
"~") StateT PState (Parsec Void String) Sort
sortP)
  Sort -> Sort -> Expr -> Expr
ECoerc Sort
s Sort
t (Expr -> Expr) -> Parser Expr -> Parser Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Expr
p



{-
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 a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try Parser Expr
funAppP
 Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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 = addOperator op (fixityTable s)
                    , fixityOps   = op:fixityOps s
                    }

-- | Add a new numeric FTyCon (symbol) to the parsing state.
addNumTyCon :: Symbol -> Parser ()
addNumTyCon :: Symbol -> Parser ()
addNumTyCon Symbol
tc = (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{ numTyCons = S.insert tc (numTyCons s) }

-- | Parses any of the known infix operators.
infixSymbolP :: Parser Symbol
infixSymbolP :: Parser Symbol
infixSymbolP = do
  [String]
ops <- (PState -> [String]) -> Parser [String]
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets PState -> [String]
infixOps
  [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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Symbol -> Parser Symbol
forall a. a -> StateT PState (Parsec Void String) a
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]) -> Parser [String]
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets PState -> [String]
infixOps
  [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 a b.
StateT PState (Parsec Void String) a
-> (a -> StateT PState (Parsec Void String) b)
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ (Loc SourcePos
l1 SourcePos
l2 String
_) -> LocSymbol -> Parser LocSymbol
forall a. a -> StateT PState (Parsec Void String) a
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 :: forall (parser :: * -> *) expr.
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
-> Parser (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 ()
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a. a -> StateT PState (Parsec Void String) a
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) (Parser (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 () -> Parser (Expr -> Expr) -> Parser (Expr -> Expr)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr) -> Parser (Expr -> Expr)
forall a. a -> StateT PState (Parsec Void String) a
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) (Parser (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 () -> Parser (Expr -> Expr) -> Parser (Expr -> Expr)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr) -> Parser (Expr -> Expr)
forall a. a -> StateT PState (Parsec Void String) a
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 b a. (b -> a -> b) -> b -> [a] -> b
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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr
exprFunP Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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 a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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 -> Parser (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 Parser (Expr -> Expr) -> Parser Expr -> Parser Expr
forall a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) a
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 a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
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 a. [a] -> 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 a. a -> StateT PState (Parsec Void String) a
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)


-- | Parser for literals of all sorts.
litP :: Parser Expr
litP :: Parser Expr
litP = do String -> Parser ()
reserved String
"lit"
          String
l <- Parser String
stringLiteral
          Constant -> Expr
ECon (Constant -> Expr) -> (Sort -> Constant) -> Sort -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Sort -> Constant
L (String -> Text
T.pack String
l) (Sort -> Expr)
-> StateT PState (Parsec Void String) Sort -> Parser Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) Sort
sortP

-- | Parser for lambda abstractions.
lamP :: Parser Expr
lamP :: Parser Expr
lamP
  = do String -> Parser ()
reservedOp String
"\\"
       Symbol
x <- Parser Symbol
symbolP
       String
_ <- Parser String
colon -- TODO: this should probably be reservedOp instead
       Sort
t <- StateT PState (Parsec Void String) Sort
sortP
       String -> Parser ()
reservedOp String
"->"
       (Symbol, Sort) -> Expr -> Expr
ELam (Symbol
x, Sort
t) (Expr -> Expr) -> Parser Expr -> Parser Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Expr
exprP

varSortP :: Parser Sort
varSortP :: StateT PState (Parsec Void String) Sort
varSortP  = Int -> Sort
FVar  (Int -> Sort)
-> StateT PState (Parsec Void String) Int
-> StateT PState (Parsec Void String) 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 :: StateT PState (Parsec Void String) Sort
funcSortP = StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) Sort
forall a. Parser a -> Parser a
parens (StateT PState (Parsec Void String) Sort
 -> StateT PState (Parsec Void String) Sort)
-> StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) 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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) a
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]
-> StateT PState (Parsec Void String) Sort
forall a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
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 a. Parser a -> Parser a
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 (StateT PState (Parsec Void String) Sort
-> Parser String -> StateT PState (Parsec Void String) [Sort]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy StateT PState (Parsec Void String) Sort
sortP Parser String
semi))
      StateT PState (Parsec Void String) [Sort]
-> StateT PState (Parsec Void String) [Sort]
-> StateT PState (Parsec Void String) [Sort]
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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 (StateT PState (Parsec Void String) Sort
-> Parser String -> StateT PState (Parsec Void String) [Sort]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy StateT PState (Parsec Void String) Sort
sortP Parser String
comma)

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

sortArgP :: Parser Sort
sortArgP :: StateT PState (Parsec Void String) Sort
sortArgP = StateT PState (Parsec Void String) [Sort]
-> StateT PState (Parsec Void String) Sort
sortP' ([Sort] -> StateT PState (Parsec Void String) [Sort]
forall a. a -> StateT PState (Parsec Void String) a
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]
-> StateT PState (Parsec Void String) Sort
sortP' StateT PState (Parsec Void String) [Sort]
appArgsP
   =  StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) Sort
forall a. Parser a -> Parser a
parens StateT PState (Parsec Void String) Sort
sortP -- parenthesised sort, starts with "("
  StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) Sort
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reserved String
"func" Parser ()
-> StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) Sort
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StateT PState (Parsec Void String) Sort
funcSortP) -- function sort, starts with "func"
  StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) Sort
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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 a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Sort -> Sort)
-> StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) Sort
forall a. Parser a -> Parser a
brackets StateT PState (Parsec Void String) Sort
sortP)
  StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) Sort
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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]
-> StateT PState (Parsec Void String) Sort
forall a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT PState (Parsec Void String) [Sort]
appArgsP)
  StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) Sort
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Sort -> [Sort] -> Sort
fApp   (Sort -> [Sort] -> Sort)
-> StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) ([Sort] -> Sort)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) Sort
tvarP   StateT PState (Parsec Void String) ([Sort] -> Sort)
-> StateT PState (Parsec Void String) [Sort]
-> StateT PState (Parsec Void String) Sort
forall a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT PState (Parsec Void String) [Sort]
appArgsP)

tvarP :: Parser Sort
tvarP :: StateT PState (Parsec Void String) 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
"@" StateT PState (Parsec Void String) (Tokens String)
-> StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) Sort
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StateT PState (Parsec Void String) Sort
varSortP)
  StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) Sort
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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 -> StateT PState (Parsec Void String) 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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FTycon -> StateT PState (Parsec Void String) FTycon
forall a. a -> StateT PState (Parsec Void String) a
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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FTycon -> StateT PState (Parsec Void String) FTycon
forall a. a -> StateT PState (Parsec Void String) a
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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FTycon -> StateT PState (Parsec Void String) FTycon
forall a. a -> StateT PState (Parsec Void String) a
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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FTycon -> StateT PState (Parsec Void String) FTycon
forall a. a -> StateT PState (Parsec Void String) a
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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FTycon -> StateT PState (Parsec Void String) FTycon
forall a. a -> StateT PState (Parsec Void String) a
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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FTycon -> StateT PState (Parsec Void String) FTycon
forall a. a -> StateT PState (Parsec Void String) a
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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FTycon -> StateT PState (Parsec Void String) FTycon
forall a. a -> StateT PState (Parsec Void String) a
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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (LocSymbol -> StateT PState (Parsec Void String) FTycon
mkFTycon          (LocSymbol -> StateT PState (Parsec Void String) FTycon)
-> Parser LocSymbol -> StateT PState (Parsec Void String) FTycon
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<  Parser LocSymbol
locUpperIdP)

mkFTycon :: LocSymbol -> Parser FTycon
mkFTycon :: LocSymbol -> StateT PState (Parsec Void String) FTycon
mkFTycon LocSymbol
locSymbol = do
  HashSet Symbol
nums  <- (PState -> HashSet Symbol)
-> StateT PState (Parsec Void String) (HashSet Symbol)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets PState -> HashSet Symbol
numTyCons
  FTycon -> StateT PState (Parsec Void String) FTycon
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return (LocSymbol -> Bool -> Bool -> FTycon
symbolNumInfoFTyCon LocSymbol
locSymbol (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
locSymbol Symbol -> HashSet Symbol -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet Symbol
nums) Bool
False)


--------------------------------------------------------------------------------
-- | 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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr
falseP -- constant "false"
      Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"??" Parser () -> Parser Expr -> Parser Expr
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Expr
makeUniquePGrad)
      Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr
kvarPredP
      Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr -> Parser Expr
forall a. Parser a -> Parser a
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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"?" Parser () -> Parser Expr -> Parser Expr
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Expr
exprP)
      Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr -> Parser Expr
forall a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try Parser Expr
funAppP
      Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"&&" Parser () -> Parser Expr -> Parser Expr
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"||" Parser () -> Parser Expr -> Parser Expr
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
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 s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
getSourcePos
       Expr -> Parser Expr
forall a. a -> StateT PState (Parsec Void String) a
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Expr -> Parser Expr
forall a. a -> StateT PState (Parsec Void String) a
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Expr -> Parser Expr
forall a. a -> StateT PState (Parsec Void String) a
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 a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
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 = [ [Parser (Expr -> Expr)
-> Operator (StateT PState (Parsec Void String)) Expr
forall (m :: * -> *) a. m (a -> a) -> Operator m a
Prefix (String -> Parser ()
reservedOp String
"~"    Parser () -> Parser (Expr -> Expr) -> Parser (Expr -> Expr)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr) -> Parser (Expr -> Expr)
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr -> Expr
PNot)]
           , [Parser (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 () -> Parser (Expr -> Expr) -> Parser (Expr -> Expr)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr) -> Parser (Expr -> Expr)
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr -> Expr
PNot)]
           , [Parser (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 ()
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr -> Expr -> Expr
pGAnd)]
           , [Parser (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 ()
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return (\Expr
x Expr
y -> [Expr] -> Expr
POr [Expr
x,Expr
y]))]
           , [Parser (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 ()
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr -> Expr -> Expr
PImp)]
           , [Parser (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 ()
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr -> Expr -> Expr
PImp)]
           , [Parser (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 ()
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr -> Expr -> Expr
PIff)]
           , [Parser (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 ()
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr -> Expr -> Expr
PIff)]
           , [Parser (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 ()
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr -> Expr -> Expr
pNotIff)]
           , [Parser (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 ()
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr -> Expr -> Expr
pNotIff)]
           ]

pNotIff :: Expr -> Expr -> Expr
pNotIff :: Expr -> Expr -> Expr
pNotIff Expr
x Expr
y = Expr -> Expr
PNot (Expr -> Expr -> Expr
PIff Expr
x Expr
y)

-- | 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)
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr)
forall a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser (Expr -> Expr -> Expr)
brelP Parser (Expr -> Expr) -> Parser Expr -> Parser Expr
forall a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
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 :: Parser (Expr -> Expr -> Expr)
brelP =  (String -> Parser ()
reservedOp String
"==" Parser ()
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Eq))
     Parser (Expr -> Expr -> Expr)
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"="  Parser ()
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Eq))
     Parser (Expr -> Expr -> Expr)
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"~~" Parser ()
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Ueq))
     Parser (Expr -> Expr -> Expr)
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"!=" Parser ()
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Ne))
     Parser (Expr -> Expr -> Expr)
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"/=" Parser ()
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Ne))
     Parser (Expr -> Expr -> Expr)
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"!~" Parser ()
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Une))
     Parser (Expr -> Expr -> Expr)
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"<"  Parser ()
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Lt))
     Parser (Expr -> Expr -> Expr)
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"<=" Parser ()
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Le))
     Parser (Expr -> Expr -> Expr)
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
">"  Parser ()
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Gt))
     Parser (Expr -> Expr -> Expr)
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
">=" Parser ()
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a. a -> StateT PState (Parsec Void String) a
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 a. Parser a -> Parser a
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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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 :: forall a.
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
spaces
      a -> Parser a
forall a. a -> StateT PState (Parsec Void String) 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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) a
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 a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try Parser Symbol
bindP Parser Symbol -> Parser Symbol -> Parser Symbol
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Symbol -> Parser Symbol
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return Symbol
x

-- | (Sorted) Refinements
refP :: Parser (Reft -> a) -> Parser a
refP :: forall a. 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 :: forall a. 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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser String
colon StateT PState (Parsec Void String) (Sort -> DataField)
-> StateT PState (Parsec Void String) Sort -> Parser DataField
forall a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT PState (Parsec Void String) 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 a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
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 a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) a
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 a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser DataCtor
dataCtorP))

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

-- | Qualifiers
qualifierP :: Parser Sort -> Parser Qualifier
qualifierP :: StateT PState (Parsec Void String) Sort -> Parser Qualifier
qualifierP StateT PState (Parsec Void String) Sort
tP = do
  SourcePos
pos    <- StateT PState (Parsec Void String) SourcePos
forall s e (m :: * -> *).
(TraversableStream s, 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 (StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) QualParam
qualParamP StateT PState (Parsec Void String) Sort
tP) Parser String
comma
  String
_      <- Parser String
colon
  Expr
body   <- Parser Expr
predP
  Qualifier -> Parser Qualifier
forall a. a -> StateT PState (Parsec Void String) a
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 :: StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) QualParam
qualParamP StateT PState (Parsec Void String) Sort
tP = do
  Symbol
x     <- Parser Symbol
symbolP
  QualPattern
pat   <- Parser QualPattern
qualPatP
  String
_     <- Parser String
colon
  Symbol -> QualPattern -> Sort -> QualParam
QP Symbol
x QualPattern
pat (Sort -> QualParam)
-> StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) QualParam
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) Sort
tP

qualPatP :: Parser QualPattern
qualPatP :: Parser QualPattern
qualPatP
   =  (String -> Parser ()
reserved String
"as" Parser () -> Parser QualPattern -> Parser QualPattern
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser QualPattern
qualStrPatP)
  Parser QualPattern -> Parser QualPattern -> Parser QualPattern
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> QualPattern -> Parser QualPattern
forall a. a -> StateT PState (Parsec Void String) a
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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
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 :: forall a. 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 :: forall a z b. 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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) a
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 -> StateT PState (Parsec Void String) (a, b)
forall a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) 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 a. a -> StateT PState (Parsec Void String) a
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 (StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) (Symbol, Sort)
forall a. Parser a -> Parser (Symbol, a)
symBindP StateT PState (Parsec Void String) Sort
sortP) Parser String
comma
  Sort
sort   <- Parser String
colon        Parser String
-> StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) Sort
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT PState (Parsec Void String) Sort
sortP
  Expr
body   <- String -> Parser ()
reserved String
"=" Parser () -> Parser Expr -> Parser Expr
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
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 a. a -> StateT PState (Parsec Void String) a
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 a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
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 a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
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 a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (String -> Parser ()
reserved String
"=" Parser () -> Parser Expr -> Parser Expr
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Expr
exprP)

pairsP :: Parser a -> Parser b -> Parser [(a, b)]
pairsP :: forall a b. 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]
sepBy (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 !a
  | EBind !Int !Symbol !Sort !a
  | 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, Show a) => Int -> Def a -> ShowS
forall a. (Fixpoint a, Show a) => [Def a] -> ShowS
forall a. (Fixpoint a, Show a) => Def a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. (Fixpoint a, Show a) => Int -> Def a -> ShowS
showsPrec :: Int -> Def a -> ShowS
$cshow :: forall a. (Fixpoint a, Show a) => Def a -> String
show :: Def a -> String
$cshowList :: forall a. (Fixpoint a, Show a) => [Def a] -> ShowS
showList :: [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
$cfrom :: forall a x. Def a -> Rep (Def a) x
from :: forall x. Def a -> Rep (Def a) x
$cto :: forall a x. Rep (Def a) x -> Def a
to :: forall x. Rep (Def a) x -> Def a
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 a. a -> StateT PState (Parsec Void String) a
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 ())
-> StateT PState (Parsec Void String) 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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser String
colon Parser String
-> StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) Sort
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StateT PState (Parsec Void String) Sort
sortP)
    StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Symbol
symbolP) StateT PState (Parsec Void String) (Sort -> Def ())
-> StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) (Def ())
forall a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Parser String
colon Parser String
-> StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) Sort
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StateT PState (Parsec Void String) Sort
sortP)
    StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Symbol
symbolP) StateT PState (Parsec Void String) (Sort -> Def ())
-> StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) (Def ())
forall a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Parser String
colon Parser String
-> StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) Sort
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StateT PState (Parsec Void String) Sort
sortP)
    StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
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 a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StateT PState (Parsec Void String) Sort -> Parser Qualifier
qualifierP StateT PState (Parsec Void String) Sort
sortP)
    StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Int -> Symbol -> Sort -> () -> Def ()
forall a. Int -> Symbol -> Sort -> a -> 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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
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 a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Symbol
symbolP StateT PState (Parsec Void String) (Sort -> () -> Def ())
-> StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) (() -> Def ())
forall a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Parser String
colon Parser String
-> StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) Sort
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) Sort
forall a. Parser a -> Parser a
braces StateT PState (Parsec Void String) Sort
sortP) StateT PState (Parsec Void String) (() -> Def ())
-> Parser () -> StateT PState (Parsec Void String) (Def ())
forall a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> () -> Parser ()
forall a. a -> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Int -> Symbol -> SortedReft -> () -> Def ()
forall a. Int -> Symbol -> SortedReft -> a -> 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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
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 a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
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 a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
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 ())
-> Parser () -> StateT PState (Parsec Void String) (Def ())
forall a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> () -> Parser ()
forall a. a -> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
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 a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
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)
-> StateT PState (Parsec Void String) Sort
-> Parser (Reft -> SortedReft)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (StateT PState (Parsec Void String) Sort
sortP StateT PState (Parsec Void String) Sort
-> Parser () -> StateT PState (Parsec Void String) Sort
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) a
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
          case IBindEnv -> SortedReft -> () -> [WfC ()]
forall a. Fixpoint a => IBindEnv -> SortedReft -> a -> [WfC a]
wfC IBindEnv
env SortedReft
r () of
            [WfC ()
w]   -> WfC () -> StateT PState (Parsec Void String) (WfC ())
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return WfC ()
w
            []    -> String -> StateT PState (Parsec Void String) (WfC ())
forall a. HasCallStack => String -> a
error String
"Unexpected empty list in wfCP"
            WfC ()
_:WfC ()
_:[WfC ()]
_ -> String -> StateT PState (Parsec Void String) (WfC ())
forall a. HasCallStack => String -> a
error String
"Expected a single element list in wfCP"

subCP :: Parser (SubC ())
subCP :: StateT PState (Parsec Void String) (SubC ())
subCP = do SourcePos
pos <- StateT PState (Parsec Void String) SourcePos
forall s e (m :: * -> *).
(TraversableStream s, 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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
spaces
           [Int]
tag <- Parser [Int]
tagP
           IBindEnv
-> SortedReft
-> SortedReft
-> Integer
-> [Int]
-> SourcePos
-> SourcePos
-> SubC ()
subC' IBindEnv
env SortedReft
lhs SortedReft
rhs Integer
i [Int]
tag SourcePos
pos (SourcePos -> SubC ())
-> StateT PState (Parsec Void String) SourcePos
-> StateT PState (Parsec Void String) (SubC ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) SourcePos
forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
getSourcePos

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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
spaces Parser () -> Parser [Int] -> Parser [Int]
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
spaces) Parser String
semi
           IBindEnv -> Parser IBindEnv
forall a. a -> StateT PState (Parsec Void String) a
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> Parser Bool
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True)
    Parser Bool -> Parser Bool -> Parser Bool
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reserved String
"False" Parser () -> Parser Bool -> Parser Bool
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> Parser Bool
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False)

defsFInfo :: [Def a] -> FInfo a
defsFInfo :: forall a. [Def a] -> FInfo a
defsFInfo [Def a]
defs = {- SCC "defsFI" -} HashMap Integer (SubC a)
-> HashMap KVar (WfC a)
-> BindEnv a
-> [Int]
-> SEnv Sort
-> SEnv Sort
-> Kuts
-> [Qualifier]
-> HashMap Int a
-> [DataDecl]
-> HOInfo
-> [Triggered Expr]
-> AxiomEnv
-> GInfo SubC a
forall (c :: * -> *) a.
HashMap Integer (c a)
-> HashMap KVar (WfC a)
-> BindEnv a
-> [Int]
-> SEnv Sort
-> SEnv Sort
-> Kuts
-> [Qualifier]
-> HashMap Int a
-> [DataDecl]
-> HOInfo
-> [Triggered Expr]
-> AxiomEnv
-> GInfo c a
Types.FI HashMap Integer (SubC a)
cm HashMap KVar (WfC a)
ws BindEnv a
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 a
bs         = [(Int, (Symbol, SortedReft, a))] -> BindEnv a
forall a. [(Int, (Symbol, SortedReft, a))] -> BindEnv a
bindEnvFromList  ([(Int, (Symbol, SortedReft, a))] -> BindEnv a)
-> [(Int, (Symbol, SortedReft, a))] -> BindEnv a
forall a b. (a -> b) -> a -> b
$ [(Int, (Symbol, SortedReft, a))]
exBinds [(Int, (Symbol, SortedReft, a))]
-> [(Int, (Symbol, SortedReft, a))]
-> [(Int, (Symbol, SortedReft, a))]
forall a. [a] -> [a] -> [a]
++ [(Int
n,(Symbol
x,SortedReft
r,a
a)) | IBind Int
n Symbol
x SortedReft
r a
a <- [Def a]
defs]
    ebs :: [Int]
ebs        =                    [ Int
n                  | (Int
n,(Symbol, SortedReft, a)
_) <- [(Int, (Symbol, SortedReft, a))]
exBinds]
    exBinds :: [(Int, (Symbol, SortedReft, a))]
exBinds    =                    [(Int
n, (Symbol
x, Sort -> Reft -> SortedReft
RR Sort
t Reft
forall a. Monoid a => a
mempty, a
a)) | EBind Int
n Symbol
x Sort
t a
a <- [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 b a. (b -> a -> b) -> b -> [a] -> b
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) =>
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}. (Hashable k, Num k) => HashMap k Bool
expand HashMap Integer [AutoRewrite]
forall {k}. (Hashable k, Num 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 :: forall a. Parser a -> Parser (FixResult a)
fixResultP Parser a
pp
  =  (String -> Parser ()
reserved String
"SAT"   Parser ()
-> StateT PState (Parsec Void String) (FixResult a)
-> StateT PState (Parsec Void String) (FixResult a)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FixResult a -> StateT PState (Parsec Void String) (FixResult a)
forall a. a -> StateT PState (Parsec Void String) 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))
 StateT PState (Parsec Void String) (FixResult a)
-> StateT PState (Parsec Void String) (FixResult a)
-> StateT PState (Parsec Void String) (FixResult a)
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reserved String
"UNSAT" Parser ()
-> StateT PState (Parsec Void String) (FixResult a)
-> StateT PState (Parsec Void String) (FixResult a)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
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]
-> StateT PState (Parsec Void String) (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))
 StateT PState (Parsec Void String) (FixResult a)
-> StateT PState (Parsec Void String) (FixResult a)
-> StateT PState (Parsec Void String) (FixResult a)
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reserved String
"CRASH" Parser ()
-> StateT PState (Parsec Void String) (FixResult a)
-> StateT PState (Parsec Void String) (FixResult a)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser a -> StateT PState (Parsec Void String) (FixResult a)
forall a. Parser a -> Parser (FixResult a)
crashP Parser a
pp)

crashP :: Parser a -> Parser (FixResult a)
crashP :: forall a. 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 -> Token String -> Bool
forall a b. a -> b -> a
const Bool
True) -- consume the rest of the input
  FixResult a -> Parser (FixResult a)
forall a. a -> StateT PState (Parsec Void String) 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, Maybe String)] -> String -> FixResult a
forall a. [(a, Maybe String)] -> String -> FixResult a
Crash [(a
i, Maybe String
forall a. Maybe a
Nothing)] 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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) a
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
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 a. a -> StateT PState (Parsec Void String) a
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 a. Parser a -> Parser a
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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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 a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
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 :: forall a. 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 s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
getSourcePos
       (a, String, SourcePos) -> Parser (a, String, SourcePos)
forall a. a -> StateT PState (Parsec Void String) a
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 { 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
                           , numTyCons :: HashSet Symbol
numTyCons   = HashSet Symbol
forall a. HashSet a
S.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' :: forall a. 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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser a
parser Parser a -> Parser () -> Parser a
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) 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, TraversableStream 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.
(VisualStream s, TraversableStream 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' :: forall a. Show a => Parser a -> String -> IO ()
parseTest' Parser a
parser String
input =
  Parsec Void String a -> String -> IO ()
forall e a s.
(ShowErrorComponent e, Show a, VisualStream s,
 TraversableStream 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 :: forall b. 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 :: forall a. 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 = n + 1})
               Integer -> Parser Integer
forall a. a -> StateT PState (Parsec Void String) a
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Command -> StateT PState (Parsec Void String) Command
forall a. a -> StateT PState (Parsec Void String) a
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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Command -> StateT PState (Parsec Void String) Command
forall a. a -> StateT PState (Parsec Void String) a
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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Command -> StateT PState (Parsec Void String) Command
forall a. a -> StateT PState (Parsec Void String) a
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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
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)
-}