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

{-# OPTIONS_GHC -Wno-name-shadowing #-}

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.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
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [LayoutStack] -> ShowS
$cshowList :: [LayoutStack] -> ShowS
show :: LayoutStack -> String
$cshow :: LayoutStack -> String
showsPrec :: Int -> LayoutStack -> ShowS
$cshowsPrec :: Int -> LayoutStack -> ShowS
Show

-- | Pop the topmost element from the stack.
popLayoutStack :: LayoutStack -> LayoutStack
popLayoutStack :: LayoutStack -> LayoutStack
popLayoutStack LayoutStack
Empty       = 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 =
  forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\ PState
s -> PState
s { layoutStack :: LayoutStack
layoutStack = LayoutStack -> LayoutStack
f (PState -> LayoutStack
layoutStack PState
s) })

-- | Start a new layout block at the current indentation level.
setLayout :: Parser ()
setLayout :: Parser ()
setLayout = do
  Pos
i <- 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 =
  forall e s (m :: * -> *).
MonadParsec e s m =>
m () -> m () -> m () -> m ()
L.space
    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 <- forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m Pos
L.indentLevel
  -- traceShow ("guardIndentLevel", actual, ord, ref) $ pure ()
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Ord a => a -> a -> Ordering
compare Pos
actual Pos
ref forall a. Eq a => a -> a -> Bool
== Ordering
ord)
    (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 <- 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 forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (f :: * -> *) a. Applicative f => a -> f a
pure ((LayoutStack -> LayoutStack) -> Parser ()
modifyLayoutStack (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 forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
    LayoutStack
_         -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (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 <- 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 forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    After Pos
i LayoutStack
_ -> Ordering -> Pos -> Parser ()
guardIndentLevel Ordering
GT Pos
i forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    LayoutStack
_         -> 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 forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
spaces 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 <- forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
getSourcePos
  a
x <- Parser a
p
  SourcePos
l2 <- forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
getSourcePos
  Parser ()
spaces forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
after
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (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 <- forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
getSourcePos
  a
x <- Parser a
p
  SourcePos
l2 <- forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
getSourcePos
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (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 forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser ()
setLayout forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many (Parser a
p forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
popLayout) 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'.
  forall (f :: * -> *) a. Alternative f => f a -> f a -> f 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 forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser a
p forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
popLayout 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 =
      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
  forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Parser a -> Parser [a]
indentedBlock (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 forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser open
open forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepEndBy Parser a
p Parser sep
sep forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser close
close 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 =
  forall a. Parser a -> Parser a
lexeme (forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string String
x)

-- | Located variant of 'sym'.
locSym :: String -> Parser (Located String)
locSym :: String -> Parser (Located String)
locSym String
x =
  forall a. Parser a -> Parser (Located a)
locLexeme (forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string 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 =
  forall open close sep a.
Parser open -> Parser close -> Parser sep -> Parser a -> Parser [a]
indentedOrExplicitBlock (String -> Parser String
sym String
"{" forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many Parser String
semi) (String -> Parser String
sym 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 =
  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 = 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 =
  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 =
  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 =
  forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
alphaNumChar forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> 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 =
  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 =
  forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ forall a. Parser a -> Parser a
lexeme (forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string String
x forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* 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 =
  forall a. Parser a -> Parser (Located a)
locLexeme (forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string String
x forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* 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 =
  forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ forall a. Parser a -> Parser a
lexeme (forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string String
x forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* 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   = 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 = 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   = 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   = 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
_) -> forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l1 SourcePos
l2 a
a) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> Parser (Located String)
locSym String
"(" forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser a
p 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 =
  forall a. Parser a -> Parser a
lexeme Parser String
stringR 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 =
  forall a. Parser a -> Parser (Located a)
locLexeme Parser String
stringR forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"string literal"

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

-- | Consumes a float literal lexeme.
double :: Parser Double
double :: Parser Double
double = forall a. Parser a -> Parser a
lexeme forall e s (m :: * -> *) a.
(MonadParsec e s m, Token s ~ Char, RealFloat a) =>
m a
L.float 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 =
  forall a. Parser a -> Parser a
lexeme Parser Integer
naturalR 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 =
  forall a. Parser a -> Parser (Located a)
locLexeme Parser Integer
naturalR forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"nat literal"

naturalR :: Parser Integer
naturalR :: Parser Integer
naturalR =
      forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
'0' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char' Char
'x') forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall e s (m :: * -> *) a.
(MonadParsec e s m, Token s ~ Char, Num a) =>
m a
L.hexadecimal
  forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
'0' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char' Char
'o') forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall e s (m :: * -> *) a.
(MonadParsec e s m, Token s ~ Char, Num a) =>
m a
L.octal
  forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> 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 <- (:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Char
initial forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall e s (m :: * -> *).
MonadParsec e s m =>
Maybe String -> (Token s -> Bool) -> m (Tokens s)
takeWhileP forall a. Maybe a
Nothing Char -> Bool
okChars
  if String -> Bool
condition String
s
    then forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Symbolic a => a -> Symbol
symbol String
s)
    else forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
msg forall a. Semigroup a => a -> a -> a
<> String
" " forall a. Semigroup a => a -> a -> a
<> 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 forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
upperChar (forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet Char
symChars) (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 (forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
lowerChar forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
'_') (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 (forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
letterChar forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
'_') (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 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 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  =
  forall a. Parser a -> Parser a
lexeme Parser Symbol
upperIdR 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  =
  forall a. Parser a -> Parser a
lexeme Parser Symbol
lowerIdR 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 =
  forall a. Parser a -> Parser a
lexeme Parser Symbol
symbolR 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 = forall a. Parser a -> Parser (Located a)
locLexeme Parser Symbol
lowerIdR
locUpperIdP :: Parser LocSymbol
locUpperIdP = forall a. Parser a -> Parser (Located a)
locLexeme Parser Symbol
upperIdR
locSymbolP :: Parser LocSymbol
locSymbolP  = 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 =
     forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (Double -> Constant
R forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Double
double)   -- float literal
 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Integer -> Constant
I 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
T.pack 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"
 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr
falseP -- constant "false"
 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> 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"
 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr -> Parser Expr
coerceP Parser Expr
exprP -- coercion, starts with "coerce"
 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (SymConst -> Expr
ESym forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser SymConst
symconstP) -- string literal, starts with double-quote
 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Constant -> Expr
ECon forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Constant
constantP) -- numeric literal, starts with a digit
 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"_|_" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return Expr
EBot) -- constant bottom, equivalent to "false"
 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr
lamP -- lambda abstraction, starts with backslash
 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try Parser Expr
tupleP -- tuple expressions, starts with "("
 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (forall a. Parser a -> Parser a
parens Parser Expr
exprP) -- parenthesised expression, starts with "("
 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (forall a. Parser a -> Parser a
parens Parser Expr
exprCastP) -- explicit type annotation, starts with "(", TODO: should be an operator rather than require parentheses?
 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Symbol -> Expr
EVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Symbol
symbolP -- identifier, starts with any letter or underscore
 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (forall a. Parser a -> Parser a
brackets (forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Expr
emptyListP) -- empty list, start with "["
 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (forall a. Parser a -> Parser a
brackets Parser Expr
exprP 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 <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets PState -> Maybe Expr
empList
  case Maybe Expr
e of
    Maybe Expr
Nothing -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"No parsing support for empty lists"
    Just Expr
s  -> 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 <- 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 -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"No parsing support for singleton lists"
    Just Expr -> Expr
s  -> forall (m :: * -> *) a. Monad m => a -> m a
return 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
_ <- forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try Parser String
dcolon 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser 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 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) <- forall a. Parser a -> Parser a
parens (forall a z b. Parser a -> Parser z -> Parser b -> Parser (a, b)
pairP Parser Sort
sortP (String -> Parser ()
reservedOp String
"~") Parser Sort
sortP)
  Sort -> Sort -> Expr -> Expr
ECoerc Sort
s Sort
t 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
  =  forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try Parser Expr
funAppP
 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 <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets PState -> OpTable
fixityTable
    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 =
  (forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. IntMap a -> [(Int, a)]
IM.toDescList

-- | Add an operator to the parsing state.
addOperatorP :: Fixity -> Parser ()
addOperatorP :: Fixity -> Parser ()
addOperatorP Fixity
op
  = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \PState
s -> PState
s{ fixityTable :: OpTable
fixityTable = Fixity -> OpTable -> OpTable
addOperator Fixity
op (PState -> OpTable
fixityTable PState
s)
                    , fixityOps :: [Fixity]
fixityOps   = Fixity
opforall a. a -> [a] -> [a]
:PState -> [Fixity]
fixityOps PState
s
                    }

-- | Add a new numeric FTyCon (symbol) to the parsing state.
addNumTyCon :: Symbol -> Parser ()
addNumTyCon :: Symbol -> Parser ()
addNumTyCon Symbol
tc = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \PState
s -> PState
s{ numTyCons :: HashSet Symbol
numTyCons = forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
S.insert Symbol
tc (PState -> HashSet Symbol
numTyCons PState
s) }

-- | Parses any of the known infix operators.
infixSymbolP :: Parser Symbol
infixSymbolP :: Parser Symbol
infixSymbolP = do
  [String]
ops <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets PState -> [String]
infixOps
  forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
choice (String -> Parser Symbol
reserved' 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 forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Symbolic a => a -> Symbol
symbol String
x)

-- | Located version of 'infixSymbolP'.
locInfixSymbolP :: Parser (Located Symbol)
locInfixSymbolP :: Parser LocSymbol
locInfixSymbolP = do
  [String]
ops <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets PState -> [String]
infixOps
  forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
choice (String -> Parser LocSymbol
reserved' 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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ (Loc SourcePos
l1 SourcePos
l2 String
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l1 SourcePos
l2 (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  = forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixL
mkInfix Assoc
AssocRight = forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixR
mkInfix Assoc
AssocNone  = 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) (forall (parser :: * -> *) expr.
Assoc -> parser (expr -> expr -> expr) -> Operator parser expr
mkInfix Assoc
assoc (String -> Parser ()
reservedOp String
x forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> 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) (forall (m :: * -> *) a. m (a -> a) -> Operator m a
Prefix (String -> Parser ()
reservedOp String
x forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> 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) (forall (m :: * -> *) a. m (a -> a) -> Operator m a
Postfix (String -> Parser ()
reservedOp String
x forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> 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 = 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 = forall a. a -> Maybe a -> a
fromMaybe (\Expr
e1 Expr
e2 -> Expr -> Expr -> Expr
EApp (Expr -> Expr -> Expr
EApp (Symbol -> Expr
EVar forall a b. (a -> b) -> a -> b
$ 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 = forall a. a -> Maybe a -> a
fromMaybe (Expr -> Expr -> Expr
EApp (Symbol -> Expr
EVar forall a b. (a -> b) -> a -> b
$ 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 = forall a. (Maybe a -> Maybe a) -> Int -> IntMap a -> IntMap a
IM.alter (forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Operator (StateT PState (Parsec Void String)) Expr
op forall a. a -> [a] -> [a]
:) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a -> a
fromMaybe []) Int
i

-- | The initial (empty) operator table.
initOpTable :: OpTable
initOpTable :: OpTable
initOpTable = 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 = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (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 (forall a. a -> Maybe a
Just Int
9) String
"-"   (forall a. a -> Maybe a
Just Expr -> Expr
ENeg)
                 , Maybe Int
-> String -> Maybe (Expr -> Expr -> Expr) -> Assoc -> Fixity
FInfix  (forall a. a -> Maybe a
Just Int
7) String
"*"   (forall a. a -> Maybe a
Just 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  (forall a. a -> Maybe a
Just Int
7) String
"/"   (forall a. a -> Maybe a
Just 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  (forall a. a -> Maybe a
Just Int
6) String
"-"   (forall a. a -> Maybe a
Just 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  (forall a. a -> Maybe a
Just Int
6) String
"+"   (forall a. a -> Maybe a
Just 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  (forall a. a -> Maybe a
Just Int
5) String
"mod" (forall a. a -> Maybe a
Just 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  (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]) 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 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr
exprFunP forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr
simpleAppP
  where
    exprFunP :: Parser Expr
exprFunP = LocSymbol -> [Expr] -> Expr
mkEApp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser LocSymbol
funSymbolP 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  =  forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some Parser Expr
expr0P
            forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall a. Parser a -> Parser a
parens StateT PState (Parsec Void String) [Expr]
innerP
    innerP :: StateT PState (Parsec Void String) [Expr]
innerP   = forall a. Parser a -> Parser a
brackets (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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Parser a -> Parser a
parens Parser Expr
exprP forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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) <- forall a. Parser a -> Parser (Located a)
locParens ((,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Expr
exprP forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser String
comma forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 = forall a. Symbolic a => a -> Symbol
symbol forall a b. (a -> b) -> a -> b
$ String
"(" forall a. [a] -> [a] -> [a]
++ forall a. Int -> a -> [a]
replicate (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
rest) Char
',' forall a. [a] -> [a] -> [a]
++ String
")" -- stored in prefix form
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ LocSymbol -> [Expr] -> Expr
mkEApp (forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l1 SourcePos
l2 Symbol
cons) (Expr
first 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Sort -> Constant
L (String -> Text
T.pack String
l) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser 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 <- Parser Sort
sortP
       String -> Parser ()
reservedOp String
"->"
       (Symbol, Sort) -> Expr -> Expr
ELam (Symbol
x, Sort
t) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Expr
exprP

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

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

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

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

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

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


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

mkFTycon :: LocSymbol -> Parser FTycon
mkFTycon :: LocSymbol -> Parser FTycon
mkFTycon LocSymbol
locSym = do
  HashSet Symbol
nums  <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets PState -> HashSet Symbol
numTyCons
  forall (m :: * -> *) a. Monad m => a -> m a
return (LocSymbol -> Bool -> Bool -> FTycon
symbolNumInfoFTyCon LocSymbol
locSym (forall a. Located a -> a
val LocSymbol
locSym 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"
      forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr
falseP -- constant "false"
      forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"??" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Expr
makeUniquePGrad)
      forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr
kvarPredP
      forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> 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"
      forall (f :: * -> *) a. Alternative f => f a -> f a -> f 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
      forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall a. Parser a -> Parser a
parens Parser Expr
predP -- parenthesised predicate, starts with "("
      forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"?" forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Expr
exprP)
      forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try Parser Expr
funAppP
      forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Symbol -> Expr
EVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Symbol
symbolP -- identifier, starts with any letter or underscore
      forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"&&" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [Expr] -> Expr
pGAnds forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) [Expr]
predsP) -- built-in prefix and
      forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"||" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [Expr] -> Expr
POr  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 <- forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
getSourcePos
       forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ KVar -> Subst -> GradInfo -> Expr -> Expr
PGrad (Symbol -> KVar
KV forall a b. (a -> b) -> a -> b
$ forall a. Symbolic a => a -> Symbol
symbol forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show SourcePos
uniquePos) forall a. Monoid a => a
mempty (SourcePos -> GradInfo
srcGradInfo SourcePos
uniquePos) 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"  forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> 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" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return Expr
PFalse

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

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

substP :: Parser Subst
substP :: Parser Subst
substP = [(Symbol, Expr)] -> Subst
mkSubst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many (forall a. Parser a -> Parser a
brackets forall a b. (a -> b) -> a -> b
$ 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 = forall a. Parser a -> Parser a
brackets forall a b. (a -> b) -> a -> b
$ 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  = 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 = [ [forall (m :: * -> *) a. m (a -> a) -> Operator m a
Prefix (String -> Parser ()
reservedOp String
"~"    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return Expr -> Expr
PNot)]
           , [forall (m :: * -> *) a. m (a -> a) -> Operator m a
Prefix (String -> Parser ()
reserved   String
"not"  forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return Expr -> Expr
PNot)]
           , [forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixR (String -> Parser ()
reservedOp String
"&&"   forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return Expr -> Expr -> Expr
pGAnd)]
           , [forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixR (String -> Parser ()
reservedOp String
"||"   forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return (\Expr
x Expr
y -> [Expr] -> Expr
POr [Expr
x,Expr
y]))]
           , [forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixR (String -> Parser ()
reservedOp String
"=>"   forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return Expr -> Expr -> Expr
PImp)]
           , [forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixR (String -> Parser ()
reservedOp String
"==>"  forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return Expr -> Expr -> Expr
PImp)]
           , [forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixR (String -> Parser ()
reservedOp String
"="    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return Expr -> Expr -> Expr
PIff)]
           , [forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixR (String -> Parser ()
reservedOp String
"<=>"  forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return Expr -> Expr -> Expr
PIff)]
           , [forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixR (String -> Parser ()
reservedOp String
"!="   forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return Expr -> Expr -> Expr
pNotIff)]
           , [forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixR (String -> Parser ()
reservedOp String
"/="   forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> 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) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Expr
exprP forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser (Expr -> Expr -> Expr)
brelP 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
"==" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Eq))
     forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"="  forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Eq))
     forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"~~" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Ueq))
     forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"!=" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Ne))
     forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"/=" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Ne))
     forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"!~" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Une))
     forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"<"  forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Lt))
     forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"<=" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Le))
     forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
">"  forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Gt))
     forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
">=" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> 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 =  forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try ([Expr] -> Expr
pAnd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Parser a -> Parser a
brackets (forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy Parser Expr
predP Parser String
semi))
     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
  = forall a. Parser a -> Parser a
braces 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 forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
spaces
      forall (m :: * -> *) a. Monad m => a -> m a
return 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 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 = forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try Parser Symbol
bindP forall (f :: * -> *) a. Alternative f => f a -> f a -> f 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       = 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  = 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser LocSymbol
locSymbolP forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser String
colon forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Sort
sortP

dataCtorP :: Parser DataCtor
dataCtorP :: Parser DataCtor
dataCtorP  = LocSymbol -> [DataField] -> DataCtor
DCtor forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser LocSymbol
locSymbolP
                   forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Parser a -> Parser a
braces (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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser FTycon
fTyConP forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Int
intP forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* String -> Parser ()
reservedOp String
"="
                   forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Parser a -> Parser a
brackets (forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many (String -> Parser ()
reservedOp String
"|" forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser DataCtor
dataCtorP))

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

-- | Qualifiers
qualifierP :: Parser Sort -> Parser Qualifier
qualifierP :: Parser Sort -> Parser Qualifier
qualifierP Parser Sort
tP = do
  SourcePos
pos    <- forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
getSourcePos
  Symbol
n      <- Parser Symbol
upperIdP
  [QualParam]
params <- forall a. Parser a -> Parser a
parens forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy1 (Parser Sort -> Parser QualParam
qualParamP Parser Sort
tP) Parser String
comma
  String
_      <- Parser String
colon
  Expr
body   <- Parser Expr
predP
  forall (m :: * -> *) a. Monad m => a -> m a
return  forall a b. (a -> b) -> a -> b
$ Symbol -> [QualParam] -> Expr -> SourcePos -> Qualifier
mkQual Symbol
n [QualParam]
params Expr
body SourcePos
pos

qualParamP :: Parser Sort -> Parser QualParam
qualParamP :: Parser Sort -> Parser QualParam
qualParamP Parser 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Sort
tP

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

qualStrPatP :: Parser QualPattern
qualStrPatP :: Parser QualPattern
qualStrPatP
   = (Symbol -> QualPattern
PatExact forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Symbol
symbolP)
  forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall a. Parser a -> Parser a
parens (    (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Symbol -> Int -> QualPattern
PatPrefix forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a z b. Parser a -> Parser z -> Parser b -> Parser (a, b)
pairP Parser Symbol
symbolP Parser String
dot Parser Int
qpVarP)
              forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Int -> Symbol -> QualPattern
PatSuffix forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a z b. Parser a -> Parser z -> Parser b -> Parser (a, b)
pairP Parser Int
qpVarP  Parser String
dot Parser Symbol
symbolP) )


qpVarP :: Parser Int
qpVarP :: Parser Int
qpVarP = forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
'$' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Int
intP

symBindP :: Parser a -> Parser (Symbol, a)
symBindP :: forall a. Parser a -> Parser (Symbol, a)
symBindP = 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 = (,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser a
xP forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser z
sepP 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       <- forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy Parser SortedReft
sortedReftP Parser ()
spaces
  ()
_          <- Parser ()
spaces
  ()
_          <- String -> Parser ()
reserved String
"="
  ()
_          <- Parser ()
spaces
  (Expr
lhs, Expr
rhs) <- forall a. Parser a -> Parser a
braces forall a b. (a -> b) -> a -> b
$
      forall a z b. Parser a -> Parser z -> Parser b -> Parser (a, b)
pairP Parser Expr
exprP (String -> Parser ()
reserved String
"=") Parser Expr
exprP
  forall (m :: * -> *) a. Monad m => a -> m a
return 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 <- forall a. Parser a -> Parser a
parens        forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy (forall a. Parser a -> Parser (Symbol, a)
symBindP Parser Sort
sortP) Parser String
comma
  Sort
sort   <- Parser String
colon        forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Sort
sortP
  Expr
body   <- String -> Parser ()
reserved String
"=" forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall a. Parser a -> Parser a
braces (
              if Sort
sort forall a. Eq a => a -> a -> Bool
== Sort
boolSort then Parser Expr
predP else Parser Expr
exprP
               )
  forall (m :: * -> *) a. Monad m => a -> m a
return  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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Symbol
symbolP forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Symbol
symbolP forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many Parser Symbol
symbolP forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (String -> Parser ()
reserved String
"=" 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 = forall a. Parser a -> Parser a
brackets forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy (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
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
showList :: [Def a] -> ShowS
$cshowList :: forall a. (Fixpoint a, Show a) => [Def a] -> ShowS
show :: Def a -> String
$cshow :: forall a. (Fixpoint a, Show a) => Def a -> String
showsPrec :: Int -> Def a -> ShowS
$cshowsPrec :: forall a. (Fixpoint a, Show a) => Int -> Def a -> ShowS
Show, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Def a) x -> Def a
forall a x. Def a -> Rep (Def a) x
$cto :: forall a x. Rep (Def a) x -> Def a
$cfrom :: forall a x. Def a -> Rep (Def a) x
Generic)
  --  Sol of solbind
  --  Dep of FixConstraint.dep

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

fInfoP :: Parser (FInfo ())
fInfoP :: Parser (FInfo ())
fInfoP = forall a. [Def a] -> FInfo a
defsFInfo forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> {- SCC "many-defP" -} forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many Parser (Def ())
defP

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


sortedReftP :: Parser SortedReft
sortedReftP :: Parser SortedReft
sortedReftP = forall a. Parser (Reft -> a) -> Parser a
refP (Sort -> Reft -> SortedReft
RR forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Parser Sort
sortP 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 <- Parser SortedReft
sortedReftP
          case forall a. Fixpoint a => IBindEnv -> SortedReft -> a -> [WfC a]
wfC IBindEnv
env SortedReft
r () of
            [WfC ()
w]   -> forall (m :: * -> *) a. Monad m => a -> m a
return WfC ()
w
            []    -> forall a. HasCallStack => String -> a
error String
"Unexpected empty list in wfCP"
            WfC ()
_:WfC ()
_:[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 <- 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 <- Parser SortedReft
sortedReftP
           String -> Parser ()
reserved String
"rhs"
           SortedReft
rhs <- Parser SortedReft
sortedReftP
           String -> Parser ()
reserved String
"id"
           Integer
i   <- Parser Integer
natural 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 ()]
_   -> forall a. Error -> a
die forall a b. (a -> b) -> a -> b
$ SrcSpan -> Doc -> Error
err SrcSpan
sp forall a b. (a -> b) -> a -> b
$ Doc
"RHS without single conjunct at" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint SourcePos
l'
    where
       cs :: [SubC ()]
cs = forall a.
IBindEnv
-> SortedReft
-> SortedReft
-> Maybe Integer
-> [Int]
-> a
-> [SubC a]
subC IBindEnv
env SortedReft
lhs SortedReft
rhs (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" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
spaces forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall a. Parser a -> Parser a
brackets (forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy Parser Int
intP Parser String
semi)

envP  :: Parser IBindEnv
envP :: Parser IBindEnv
envP  = do [Int]
binds <- forall a. Parser a -> Parser a
brackets forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy (Parser Int
intP forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
spaces) Parser String
semi
           forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Int] -> IBindEnv -> IBindEnv
insertsIBindEnv [Int]
binds IBindEnv
emptyIBindEnv

intP :: Parser Int
intP :: Parser Int
intP = forall a. Num a => Integer -> a
fromInteger 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" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True)
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reserved String
"False" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> 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" -} 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 forall a. Monoid a => a
binfo [DataDecl]
adts forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty AxiomEnv
ae
  where
    cm :: HashMap Integer (SubC a)
cm         = forall k v.
(HasCallStack, Eq k, Hashable k, Show k) =>
String -> [(k, v)] -> HashMap k v
Misc.safeFromList
                   String
"defs-cm"        [(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         = 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 = forall a b c. (a, b, c) -> c
Misc.thd3 (forall a. WfC a -> (Symbol, Sort, KVar)
wrft WfC a
w)]
    bs :: BindEnv a
bs         = forall a. [(Int, (Symbol, SortedReft, a))] -> BindEnv a
bindEnvFromList  forall a b. (a -> b) -> a -> b
$ [(Int, (Symbol, SortedReft, a))]
exBinds 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 forall a. Monoid a => a
mempty, a
a)) | EBind Int
n Symbol
x Sort
t a
a <- [Def a]
defs]
    lts :: SEnv Sort
lts        = forall a. [(Symbol, a)] -> SEnv a
fromListSEnv       [(Symbol
x, Sort
t)             | Con Symbol
x Sort
t     <- [Def a]
defs]
    dts :: SEnv Sort
dts        = 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 forall a b. (a -> b) -> a -> b
$ 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      = forall a. Monoid a => a
mempty
    expand :: HashMap k Bool
expand     = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList         [(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    = 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      = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' forall {k} {a}.
(Hashable k, Integral a, Num k) =>
HashMap k [AutoRewrite] -> (a, Int) -> HashMap k [AutoRewrite]
insert (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 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 ->
                         forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> k -> v -> HashMap k v -> HashMap k v
M.insertWith forall a. [a] -> [a] -> [a]
(++) (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        = forall a. HasCallStack => Maybe a -> a
fromJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall {k}. (Hashable k, Num k) => HashMap k Bool
expand 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"   forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Stats -> FixResult a
Safe forall a. Monoid a => a
mempty))
 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reserved String
"UNSAT" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall a. Stats -> [a] -> FixResult a
Unsafe forall a. Monoid a => a
mempty forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Parser a -> Parser a
brackets (forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy Parser a
pp Parser String
comma))
 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reserved String
"CRASH" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> 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 <- forall e s (m :: * -> *).
MonadParsec e s m =>
Maybe String -> (Token s -> Bool) -> m (Tokens s)
takeWhileP forall a. Maybe a
Nothing (forall a b. a -> b -> a
const Bool
True) -- consume the rest of the input
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [(a, Maybe String)] -> String -> FixResult a
Crash [(a
i, forall a. Maybe a
Nothing)] String
msg

predSolP :: Parser Expr
predSolP :: Parser Expr
predSolP = forall a. Parser a -> Parser a
parens (Parser Expr
predP  forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* (Parser String
comma 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 forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall a. Parser a -> Parser a
parens (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  <- Parser KVar
kvP
  String -> Parser ()
reservedOp String
":="
  [Expr]
ps <- forall a. Parser a -> Parser a
brackets forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy Parser Expr
predSolP Parser String
semi
  forall (m :: * -> *) a. Monad m => a -> m a
return (KVar
k, forall a. Fixpoint a => a -> a
simplify forall a b. (a -> b) -> a -> b
$ [Expr] -> Expr
PAnd [Expr]
ps)
  where
    kvP :: Parser KVar
kvP = forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try Parser KVar
kvarP forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Symbol -> KVar
KV forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Symbol
symbolP)

solutionP :: Parser (M.HashMap KVar Expr)
solutionP :: Parser FixSolution
solutionP = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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, FixSolution)
solutionFileP = (,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Parser a -> Parser (FixResult a)
fixResultP Parser Integer
natural forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser FixSolution
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 <- forall e s (m :: * -> *). MonadParsec e s m => m s
getInput
       SourcePos
pos <- forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
getSourcePos
       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     = forall a. Maybe a
Nothing
                           , singList :: Maybe (Expr -> Expr)
singList    = forall a. Maybe a
Nothing
                           , fixityOps :: [Fixity]
fixityOps   = []
                           , supply :: Integer
supply      = Integer
0
                           , layoutStack :: LayoutStack
layoutStack = LayoutStack
Empty
                           , numTyCons :: HashSet Symbol
numTyCons   = 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 forall e s a.
Parsec e s a -> String -> s -> Either (ParseErrorBundle s e) a
runParser (forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (Parser ()
spaces forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser a
parser forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* forall e s (m :: * -> *). MonadParsec e s m => m ()
eof) (Maybe Expr -> PState
initPState 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
_) = forall (t :: * -> *) s a.
(Traversable t, TraversableStream s) =>
(a -> Int) -> t a -> PosState s -> (t (a, SourcePos), PosState s)
attachSourcePos forall s e. ParseError s e -> Int
errorOffset NonEmpty (ParseError String Void)
errors PosState String
posState
      in
        forall a. Error -> a
die 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 (forall a b. (a -> b) -> [a] -> [b]
map String -> Doc
text (String -> [String]
lines (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 =
  forall e a s.
(ShowErrorComponent e, Show a, VisualStream s,
 TraversableStream s) =>
Parsec e s a -> s -> IO ()
parseTest (forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT Parser a
parser (Maybe Expr -> PState
initPState 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 = forall a. Parser a -> String -> String -> a
doParse' Parser b
p String
f 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 = forall a. Parser a -> String -> String -> a
doParse' Parser a
p String
"stdin" forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
T.unpack 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 <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets PState -> Integer
supply
               forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\ PState
s -> PState
s{supply :: Integer
supply = Integer
n forall a. Num a => a -> a -> a
+ Integer
1})
               forall (m :: * -> *) a. Monad m => a -> m a
return Integer
n

---------------------------------------------------------------------
-- Standalone SMTLIB2 commands --------------------------------------
---------------------------------------------------------------------
commandsP :: Parser [Command]
commandsP :: Parser [Command]
commandsP = forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy Parser Command
commandP Parser String
semi

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

cmdVarP :: Parser Command
cmdVarP :: Parser Command
cmdVarP = 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
_ = forall a. Inputable a => String -> a
rr
  rr    = forall a. Inputable a => String -> String -> a
rr' String
""

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

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

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

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

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

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

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

instance Inputable Command where
  rr' :: String -> String -> Command
rr' = forall a. Parser a -> String -> String -> a
doParse' Parser Command
commandP

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