{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE FlexibleContexts          #-}
{-# LANGUAGE UndecidableInstances      #-}
{-# LANGUAGE TupleSections             #-}
{-# LANGUAGE OverloadedStrings         #-}
{-# LANGUAGE DeriveDataTypeable        #-}
{-# LANGUAGE ScopedTypeVariables       #-}

module Language.Haskell.Liquid.Parse
  ( hsSpecificationP
  , specSpecificationP
  , singleSpecP
  , BPspec
  , Pspec(..)
  , parseSymbolToLogic
  , parseTest'
  )
  where

import           Control.Arrow                          (second)
import           Control.Monad
import           Control.Monad.Identity
import qualified Data.Foldable                          as F
import           Data.String
import           Data.Void
import           Prelude                                hiding (error)
import           Text.Megaparsec                        hiding (ParseError)
import           Text.Megaparsec.Char
import qualified Data.HashMap.Strict                    as M
import qualified Data.HashSet                           as S
import           Data.Data
import qualified Data.Maybe                             as Mb -- (isNothing, fromMaybe)
import           Data.Char                              (isSpace, isAlphaNum)
import           Data.List                              (foldl', partition)
import           GHC                                    (ModuleName, mkModuleName)
import qualified Text.PrettyPrint.HughesPJ              as PJ
import           Text.PrettyPrint.HughesPJ.Compat       ((<+>))
import           Language.Fixpoint.Types                hiding (panic, SVar, DDecl, DataDecl, DataCtor (..), Error, R, Predicate)
import           Language.Haskell.Liquid.GHC.Misc       hiding (getSourcePos)
import           Language.Haskell.Liquid.Types
-- import           Language.Haskell.Liquid.Types.Errors
import qualified Language.Fixpoint.Misc                 as Misc
import qualified Language.Haskell.Liquid.Misc           as Misc
import qualified Language.Haskell.Liquid.Measure        as Measure
import           Language.Fixpoint.Parse                hiding (defineP, dataDeclP, refBindP, refP, refDefP, parseTest')

import Control.Monad.State

-- import Debug.Trace

-- * Top-level parsing API

-- | Used to parse .hs and .lhs files (via ApiAnnotations).
hsSpecificationP :: ModuleName
                 -> [(SourcePos, String)]
                 -> [BPspec]
                 -> Either [Error] (ModName, Measure.BareSpec)
hsSpecificationP :: ModuleName
-> [(SourcePos, [Char])]
-> [BPspec]
-> Either [Error] (ModName, BareSpec)
hsSpecificationP ModuleName
modName [(SourcePos, [Char])]
specComments [BPspec]
specQuotes =
  case ([Error], [BPspec])
-> PState -> [(SourcePos, [Char])] -> ([Error], [BPspec])
go ([], []) PState
initPStateWithList [(SourcePos, [Char])]
specComments of
    ([], [BPspec]
specs) ->
      forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ ModName -> [BPspec] -> (ModName, BareSpec)
mkSpec (ModType -> ModuleName -> ModName
ModName ModType
SrcImport ModuleName
modName) ([BPspec]
specs forall a. [a] -> [a] -> [a]
++ [BPspec]
specQuotes)
    ([Error]
errors, [BPspec]
_) ->
      forall a b. a -> Either a b
Left [Error]
errors
  where
    go :: ([Error], [BPspec])   -- accumulated errors and parsed specs (in reverse order)
       -> PState                -- parser state (primarily infix operator priorities)
       -> [(SourcePos, String)] -- remaining unparsed spec comments
       -> ([Error], [BPspec])   -- final errors and parsed specs
    go :: ([Error], [BPspec])
-> PState -> [(SourcePos, [Char])] -> ([Error], [BPspec])
go ([Error]
errors, [BPspec]
specs) PState
_ []
      = (forall a. [a] -> [a]
reverse [Error]
errors, forall a. [a] -> [a]
reverse [BPspec]
specs)
    go ([Error]
errors, [BPspec]
specs) PState
pstate ((SourcePos
pos, [Char]
specComment):[(SourcePos, [Char])]
xs)
      = -- 'specP' parses a single spec comment, i.e., a single LH directive
        -- we allow a "block" of specs now
        case forall a.
PState
-> Parser a
-> SourcePos
-> [Char]
-> Either (ParseErrorBundle [Char] Void) (PState, a)
parseWithError PState
pstate (forall a. Parser a -> Parser [a]
block Parser BPspec
specP) SourcePos
pos [Char]
specComment of
          Left ParseErrorBundle [Char] Void
err'       -> ([Error], [BPspec])
-> PState -> [(SourcePos, [Char])] -> ([Error], [BPspec])
go (ParseErrorBundle [Char] Void -> [Error]
parseErrorBundleToErrors ParseErrorBundle [Char] Void
err' forall a. [a] -> [a] -> [a]
++ [Error]
errors, [BPspec]
specs) PState
pstate [(SourcePos, [Char])]
xs
          Right (PState
st,[BPspec]
spec) -> ([Error], [BPspec])
-> PState -> [(SourcePos, [Char])] -> ([Error], [BPspec])
go ([Error]
errors,[BPspec]
spec forall a. [a] -> [a] -> [a]
++ [BPspec]
specs) PState
st [(SourcePos, [Char])]
xs

initPStateWithList :: PState
initPStateWithList :: PState
initPStateWithList
  = (Maybe Expr -> PState
initPState Maybe Expr
composeFun)
               { empList :: Maybe Expr
empList    = forall a. a -> Maybe a
Just (Symbol -> Expr
EVar (Symbol
"GHC.Types.[]" :: Symbol))
               , singList :: Maybe (Expr -> Expr)
singList   = forall a. a -> Maybe a
Just (\Expr
e -> Expr -> Expr -> Expr
EApp (Expr -> Expr -> Expr
EApp (Symbol -> Expr
EVar (Symbol
"GHC.Types.:"  :: Symbol)) Expr
e) (Symbol -> Expr
EVar (Symbol
"GHC.Types.[]" :: Symbol)))
               }
  where composeFun :: Maybe Expr
composeFun = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Symbol -> Expr
EVar Symbol
functionComposisionSymbol

-- | Used to parse .spec files.
specSpecificationP  :: SourceName -> String -> Either (ParseErrorBundle String Void) (ModName, Measure.BareSpec)
--------------------------------------------------------------------------
specSpecificationP :: [Char]
-> [Char]
-> Either (ParseErrorBundle [Char] Void) (ModName, BareSpec)
specSpecificationP [Char]
f [Char]
s = forall a b l. (a -> b) -> Either l a -> Either l b
mapRight forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$  forall a.
PState
-> Parser a
-> SourcePos
-> [Char]
-> Either (ParseErrorBundle [Char] Void) (PState, a)
parseWithError PState
initPStateWithList (StateT PState (Parsec Void [Char]) (ModName, BareSpec)
specificationP forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* forall e s (m :: * -> *). MonadParsec e s m => m ()
eof) ([Char] -> SourcePos
initialPos [Char]
f) [Char]
s

-- | Parses a module spec.
--
-- A module spec is a module only containing spec constructs for Liquid Haskell,
-- and no "normal" Haskell code.
--
specificationP :: Parser (ModName, Measure.BareSpec)
specificationP :: StateT PState (Parsec Void [Char]) (ModName, BareSpec)
specificationP = do
  [Char] -> Parser ()
reserved [Char]
"module"
  [Char] -> Parser ()
reserved [Char]
"spec"
  Symbol
name   <- Parser Symbol
symbolP
  [Char] -> Parser ()
reserved [Char]
"where"
  [BPspec]
xs     <- forall a. Parser a -> Parser [a]
block Parser BPspec
specP
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ModName -> [BPspec] -> (ModName, BareSpec)
mkSpec (ModType -> ModuleName -> ModName
ModName ModType
SpecImport forall a b. (a -> b) -> a -> b
$ [Char] -> ModuleName
mkModuleName forall a b. (a -> b) -> a -> b
$ Symbol -> [Char]
symbolString Symbol
name) [BPspec]
xs

-- debugP = grabs (specP <* whiteSpace)

-------------------------------------------------------------------------------
singleSpecP :: SourcePos -> String -> Either (ParseErrorBundle String Void) BPspec
-------------------------------------------------------------------------------
singleSpecP :: SourcePos -> [Char] -> Either (ParseErrorBundle [Char] Void) BPspec
singleSpecP SourcePos
pos = forall a b l. (a -> b) -> Either l a -> Either l b
mapRight forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
PState
-> Parser a
-> SourcePos
-> [Char]
-> Either (ParseErrorBundle [Char] Void) (PState, a)
parseWithError PState
initPStateWithList Parser BPspec
specP SourcePos
pos

mapRight :: (a -> b) -> Either l a -> Either l b
mapRight :: forall a b l. (a -> b) -> Either l a -> Either l b
mapRight a -> b
f (Right a
x) = forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ a -> b
f a
x
mapRight a -> b
_ (Left l
x)  = forall a b. a -> Either a b
Left l
x

-- Note [PState in parser]
--
-- In the original parsec parser, 'PState' did not contain the supply counter.
-- The supply counter was separately initialised to 0 on every parser call, e.g.
-- in 'parseWithError'.
--
-- Now, the supply counter is a part of 'PState' and would normally be threaded
-- between subsequent parsing calls within s single file, as for example issued
-- by 'hsSpecificationP'. This threading seems correct to me (Andres). It sounds
-- like we would want to have the same behaviour of the counter whether we are
-- parsing several separate specs or a single combined spec.
--
-- However, I am getting one test failure due to the threading change, namely
-- Tests.Micro.class-laws-pos.FreeVar.hs, because in a unification call two
-- variables occurring in a binding position do not match. This seems like a bug
-- in the unifier. I'm nevertheless reproucing the "old" supply behaviour for
-- now. This should be revisited later. TODO.

-- | Entry point for parsers.
--
-- Resets the supply in the given state to 0, see Note [PState in parser].
-- Also resets the layout stack, as different spec comments in a file can
-- start at different columns, and we do not want layout info to carry
-- across different such comments.
--
parseWithError :: forall a. PState -> Parser a -> SourcePos -> String -> Either (ParseErrorBundle String Void) (PState, a)
parseWithError :: forall a.
PState
-> Parser a
-> SourcePos
-> [Char]
-> Either (ParseErrorBundle [Char] Void) (PState, a)
parseWithError PState
pstate Parser a
parser SourcePos
p [Char]
s =
  case forall a b. (a, b) -> b
snd (forall a. Identity a -> a
runIdentity (forall (m :: * -> *) e s a.
Monad m =>
ParsecT e s m a
-> State s e -> m (State s e, Either (ParseErrorBundle s e) a)
runParserT' (forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT Parser a
doParse PState
pstate{supply :: Integer
supply = Integer
0, layoutStack :: LayoutStack
layoutStack = LayoutStack
Empty}) forall {e}. State [Char] e
internalParserState)) of
    Left ParseErrorBundle [Char] Void
peb -> forall a b. a -> Either a b
Left ParseErrorBundle [Char] Void
peb
    Right (a
r, PState
st) -> forall a b. b -> Either a b
Right (PState
st, a
r)
  where
    doParse :: Parser a
    doParse :: Parser a
doParse = 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
    internalParserState :: State [Char] e
internalParserState =
      State
        { stateInput :: [Char]
stateInput = [Char]
s
        , stateOffset :: Int
stateOffset = Int
0
        , statePosState :: PosState [Char]
statePosState =
          PosState
            { pstateInput :: [Char]
pstateInput = [Char]
s
            , pstateOffset :: Int
pstateOffset = Int
0
            , pstateSourcePos :: SourcePos
pstateSourcePos = SourcePos
p
            , pstateTabWidth :: Pos
pstateTabWidth = Pos
defaultTabWidth
            , pstateLinePrefix :: [Char]
pstateLinePrefix = [Char]
""
            }
        , stateParseErrors :: [ParseError [Char] e]
stateParseErrors = []
        }

-- | Function to test parsers interactively.
parseTest' :: Show a => Parser a -> String -> IO ()
parseTest' :: forall a. Show a => Parser a -> [Char] -> IO ()
parseTest' Parser a
parser [Char]
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 PState
initPStateWithList) [Char]
input

parseErrorBundleToErrors :: ParseErrorBundle String Void -> [Error]
parseErrorBundleToErrors :: ParseErrorBundle [Char] Void -> [Error]
parseErrorBundleToErrors (ParseErrorBundle NonEmpty (ParseError [Char] Void)
errors PosState [Char]
posState) =
  let
    (NonEmpty (ParseError [Char] Void, SourcePos)
es, PosState [Char]
_) = 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 [Char] Void)
errors PosState [Char]
posState
  in
    (ParseError [Char] Void, SourcePos) -> Error
parseErrorError forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList NonEmpty (ParseError [Char] Void, SourcePos)
es

---------------------------------------------------------------------------
parseErrorError     :: (ParseError, SourcePos) -> Error
---------------------------------------------------------------------------
parseErrorError :: (ParseError [Char] Void, SourcePos) -> Error
parseErrorError (ParseError [Char] Void
e, SourcePos
pos) = forall t. SrcSpan -> Doc -> ParseError [Char] Void -> TError t
ErrParse SrcSpan
sp Doc
msg ParseError [Char] Void
e
  where
    sp :: SrcSpan
sp              = SourcePos -> SrcSpan
sourcePosSrcSpan SourcePos
pos
    msg :: Doc
msg             = Doc
"Error Parsing Specification from:" Doc -> Doc -> Doc
<+> [Char] -> Doc
PJ.text (SourcePos -> [Char]
sourceName SourcePos
pos)

--------------------------------------------------------------------------------
-- Parse to Logic  -------------------------------------------------------------
--------------------------------------------------------------------------------

parseSymbolToLogic :: SourceName -> String -> Either (ParseErrorBundle String Void) LogicMap
parseSymbolToLogic :: [Char] -> [Char] -> Either (ParseErrorBundle [Char] Void) LogicMap
parseSymbolToLogic [Char]
f = forall a b l. (a -> b) -> Either l a -> Either l b
mapRight forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
PState
-> Parser a
-> SourcePos
-> [Char]
-> Either (ParseErrorBundle [Char] Void) (PState, a)
parseWithError PState
initPStateWithList Parser LogicMap
toLogicP ([Char] -> SourcePos
initialPos [Char]
f)

toLogicP :: Parser LogicMap
toLogicP :: Parser LogicMap
toLogicP
  = [(LocSymbol, [Symbol], Expr)] -> LogicMap
toLogicMap forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many Parser (LocSymbol, [Symbol], Expr)
toLogicOneP

toLogicOneP :: Parser  (LocSymbol, [Symbol], Expr)
toLogicOneP :: Parser (LocSymbol, [Symbol], Expr)
toLogicOneP
  = do [Char] -> Parser ()
reserved [Char]
"define"
       (LocSymbol
x:[LocSymbol]
xs) <- forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some Parser LocSymbol
locSymbolP
       [Char] -> Parser ()
reservedOp [Char]
"="
       Expr
e      <- StateT PState (Parsec Void [Char]) Expr
exprP forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT PState (Parsec Void [Char]) Expr
predP
       forall (m :: * -> *) a. Monad m => a -> m a
return (LocSymbol
x, forall a. Located a -> a
val forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [LocSymbol]
xs, Expr
e)


defineP :: Parser (LocSymbol, Symbol)
defineP :: Parser (LocSymbol, Symbol)
defineP =
  (,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser LocSymbol
locBinderP forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* [Char] -> Parser ()
reservedOp [Char]
"=" forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Symbol
binderP

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

{- | [NOTE:BARETYPE-PARSE] Fundamentally, a type is of the form

      comp -> comp -> ... -> comp

So

  bt = comp
     | comp '->' bt

  comp = circle
       | '(' bt ')'

  circle = the ground component of a baretype, sans parens or "->" at the top level

Each 'comp' should have a variable to refer to it,
either a parser-assigned one or given explicitly. e.g.

  xs : [Int]

-}

data ParamComp = PC { ParamComp -> PcScope
_pci :: PcScope
                    , ParamComp -> RType BTyCon BTyVar RReft
_pct :: BareType }
                    deriving (Int -> ParamComp -> ShowS
[ParamComp] -> ShowS
ParamComp -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [ParamComp] -> ShowS
$cshowList :: [ParamComp] -> ShowS
show :: ParamComp -> [Char]
$cshow :: ParamComp -> [Char]
showsPrec :: Int -> ParamComp -> ShowS
$cshowsPrec :: Int -> ParamComp -> ShowS
Show)

data PcScope = PcImplicit Symbol
             | PcExplicit Symbol
             | PcNoSymbol
             deriving (PcScope -> PcScope -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PcScope -> PcScope -> Bool
$c/= :: PcScope -> PcScope -> Bool
== :: PcScope -> PcScope -> Bool
$c== :: PcScope -> PcScope -> Bool
Eq,Int -> PcScope -> ShowS
[PcScope] -> ShowS
PcScope -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [PcScope] -> ShowS
$cshowList :: [PcScope] -> ShowS
show :: PcScope -> [Char]
$cshow :: PcScope -> [Char]
showsPrec :: Int -> PcScope -> ShowS
$cshowsPrec :: Int -> PcScope -> ShowS
Show)

nullPC :: BareType -> ParamComp
nullPC :: RType BTyCon BTyVar RReft -> ParamComp
nullPC RType BTyCon BTyVar RReft
bt = PcScope -> RType BTyCon BTyVar RReft -> ParamComp
PC PcScope
PcNoSymbol RType BTyCon BTyVar RReft
bt

btP :: Parser ParamComp
btP :: Parser ParamComp
btP = do
  c :: ParamComp
c@(PC PcScope
sb RType BTyCon BTyVar RReft
_) <- Parser ParamComp
compP
  case PcScope
sb of
    PcScope
PcNoSymbol   -> forall (m :: * -> *) a. Monad m => a -> m a
return ParamComp
c
    PcImplicit Symbol
b -> ParamComp -> Symbol -> Parser ParamComp
parseFun ParamComp
c Symbol
b
    PcExplicit Symbol
b -> ParamComp -> Symbol -> Parser ParamComp
parseFun ParamComp
c Symbol
b
  forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"btP"
  where
    parseFun :: ParamComp -> Symbol -> Parser ParamComp
parseFun c :: ParamComp
c@(PC PcScope
sb RType BTyCon BTyVar RReft
t1) Symbol
sym  =
      (do
            [Char] -> Parser ()
reservedOp [Char]
"->"
            PC PcScope
_ RType BTyCon BTyVar RReft
t2 <- Parser ParamComp
btP
            forall (m :: * -> *) a. Monad m => a -> m a
return (PcScope -> RType BTyCon BTyVar RReft -> ParamComp
PC PcScope
sb (forall r c tv.
Monoid r =>
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
rFun Symbol
sym RType BTyCon BTyVar RReft
t1 RType BTyCon BTyVar RReft
t2)))
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
         (do
            [Char] -> Parser ()
reservedOp [Char]
"=>"
            PC PcScope
_ RType BTyCon BTyVar RReft
t2 <- Parser ParamComp
btP
            -- TODO:AZ return an error if s == PcExplicit
            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PcScope -> RType BTyCon BTyVar RReft -> ParamComp
PC PcScope
sb forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (forall r c tv.
Monoid r =>
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
rFun Symbol
dummySymbol) RType BTyCon BTyVar RReft
t2 (forall t t1. RType BTyCon t t1 -> [RType BTyCon t t1]
getClasses RType BTyCon BTyVar RReft
t1))
         forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
          (do
             LocSymbol
b <- Parser LocSymbol
locInfixSymbolP
             PC PcScope
_ RType BTyCon BTyVar RReft
t2 <- Parser ParamComp
btP
             forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PcScope -> RType BTyCon BTyVar RReft -> ParamComp
PC PcScope
sb forall a b. (a -> b) -> a -> b
$ forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp (LocSymbol -> BTyCon
mkBTyCon LocSymbol
b) [RType BTyCon BTyVar RReft
t1,RType BTyCon BTyVar RReft
t2] [] forall a. Monoid a => a
mempty)
         forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *) a. Monad m => a -> m a
return ParamComp
c


compP :: Parser ParamComp
compP :: Parser ParamComp
compP = Parser ParamComp
circleP forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall a. Parser a -> Parser a
parens Parser ParamComp
btP forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"compP"

circleP :: Parser ParamComp
circleP :: Parser ParamComp
circleP
  =  RType BTyCon BTyVar RReft -> ParamComp
nullPC forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Char] -> Parser ()
reserved [Char]
"forall" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
bareAllP)
 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser ParamComp
holePC                                 -- starts with '_'
 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser ParamComp
namedCircleP                           -- starts with lower
 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser ParamComp
bareTypeBracesP                        -- starts with '{'
 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser ParamComp
unnamedCircleP
 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser ParamComp
anglesCircleP                          -- starts with '<'
 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> RType BTyCon BTyVar RReft -> ParamComp
nullPC forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) b. Monad m => m (Reft -> b) -> m b
dummyP Parser (Reft -> RType BTyCon BTyVar RReft)
bbaseP               -- starts with '_' or '[' or '(' or lower or "'" or upper
 forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"circleP"

anglesCircleP :: Parser ParamComp
anglesCircleP :: Parser ParamComp
anglesCircleP
  = forall a. Parser a -> Parser a
angles forall a b. (a -> b) -> a -> b
$ do
      PC PcScope
sb RType BTyCon BTyVar RReft
t <- forall a. Parser a -> Parser a
parens Parser ParamComp
btP
      Predicate
p       <- Parser Predicate
monoPredicateP
      forall (m :: * -> *) a. Monad m => a -> m a
return   forall a b. (a -> b) -> a -> b
$ PcScope -> RType BTyCon BTyVar RReft -> ParamComp
PC PcScope
sb (RType BTyCon BTyVar RReft
t forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`strengthen` forall r. r -> Predicate -> UReft r
MkUReft forall a. Monoid a => a
mempty Predicate
p)

holePC :: Parser ParamComp
holePC :: Parser ParamComp
holePC = do
  RType BTyCon BTyVar RReft
h <- StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
holeP
  Symbol
b <- Parser Symbol
dummyBindP
  forall (m :: * -> *) a. Monad m => a -> m a
return (PcScope -> RType BTyCon BTyVar RReft -> ParamComp
PC (Symbol -> PcScope
PcImplicit Symbol
b) RType BTyCon BTyVar RReft
h)

namedCircleP :: Parser ParamComp
namedCircleP :: Parser ParamComp
namedCircleP = do
  LocSymbol
lb <- Parser LocSymbol
locLowerIdP
  do ()
_ <- [Char] -> Parser ()
reservedOp [Char]
":"
     let b :: Symbol
b = forall a. Located a -> a
val LocSymbol
lb
     PcScope -> RType BTyCon BTyVar RReft -> ParamComp
PC (Symbol -> PcScope
PcExplicit Symbol
b) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Symbol
-> StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
bareArgP Symbol
b
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do
      Symbol
b <- Parser Symbol
dummyBindP
      PcScope -> RType BTyCon BTyVar RReft -> ParamComp
PC (Symbol -> PcScope
PcImplicit Symbol
b) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) b. Monad m => m (Reft -> b) -> m b
dummyP (Symbol -> Parser (Reft -> RType BTyCon BTyVar RReft)
lowerIdTail (forall a. Located a -> a
val LocSymbol
lb))

unnamedCircleP :: Parser ParamComp
unnamedCircleP :: Parser ParamComp
unnamedCircleP = do
  LocSymbol
lb <- forall a. Parser a -> Parser (Located a)
located Parser Symbol
dummyBindP
  let b :: Symbol
b = forall a. Located a -> a
val LocSymbol
lb
  RType BTyCon BTyVar RReft
t1 <- Symbol
-> StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
bareArgP Symbol
b
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PcScope -> RType BTyCon BTyVar RReft -> ParamComp
PC (Symbol -> PcScope
PcImplicit Symbol
b) RType BTyCon BTyVar RReft
t1

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

-- | The top-level parser for "bare" refinement types. If refinements are
-- not supplied, then the default "top" refinement is used.

bareTypeP :: Parser BareType
bareTypeP :: StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
bareTypeP = do
  PC PcScope
_ RType BTyCon BTyVar RReft
v <- Parser ParamComp
btP
  forall (m :: * -> *) a. Monad m => a -> m a
return RType BTyCon BTyVar RReft
v

bareTypeBracesP :: Parser ParamComp
bareTypeBracesP :: Parser ParamComp
bareTypeBracesP = do
  Either ParamComp (RType BTyCon BTyVar RReft)
t <-  forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (forall a. Parser a -> Parser a
braces (
            forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (forall a b. b -> Either a b
Right forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
constraintP)
           forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
            (do
                    Symbol
x  <- Parser Symbol
symbolP
                    ()
_ <- [Char] -> Parser ()
reservedOp [Char]
":"
                    -- NOSUBST i  <- freshIntP
                    Reft -> RType BTyCon BTyVar RReft
t  <- Parser (Reft -> RType BTyCon BTyVar RReft)
bbaseP
                    [Char] -> Parser ()
reservedOp [Char]
"|"
                    Expr
ra <- StateT PState (Parsec Void [Char]) Expr
refasHoleP
                    -- xi is a unique var based on the name in x.
                    -- su replaces any use of x in the balance of the expression with the unique val
                    -- NOSUBST let xi = intSymbol x i
                    -- NOSUBST let su v = if v == x then xi else v
                    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ PcScope -> RType BTyCon BTyVar RReft -> ParamComp
PC (Symbol -> PcScope
PcExplicit Symbol
x) forall a b. (a -> b) -> a -> b
$ Reft -> RType BTyCon BTyVar RReft
t ((Symbol, Expr) -> Reft
Reft (Symbol
x, Expr
ra)) )
            )) 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 {b}.
StateT PState (Parsec Void [Char]) Expr
-> Parser (Either ParamComp b)
helper StateT PState (Parsec Void [Char]) Expr
holeOrPredsP) forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall {b}.
StateT PState (Parsec Void [Char]) Expr
-> Parser (Either ParamComp b)
helper StateT PState (Parsec Void [Char]) Expr
predP
  case Either ParamComp (RType BTyCon BTyVar RReft)
t of
    Left ParamComp
l -> forall (m :: * -> *) a. Monad m => a -> m a
return ParamComp
l
    Right RType BTyCon BTyVar RReft
ct -> do
      PC PcScope
_sb RType BTyCon BTyVar RReft
tt <- Parser ParamComp
btP
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ RType BTyCon BTyVar RReft -> ParamComp
nullPC forall a b. (a -> b) -> a -> b
$ forall r c tv.
Monoid r =>
RType c tv r -> RType c tv r -> RType c tv r
rrTy RType BTyCon BTyVar RReft
ct RType BTyCon BTyVar RReft
tt
  where
    holeOrPredsP :: StateT PState (Parsec Void [Char]) Expr
holeOrPredsP
      = ([Char] -> Parser ()
reserved [Char]
"_" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return Expr
hole)
     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 (ListNE 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 StateT PState (Parsec Void [Char]) Expr
predP Parser [Char]
semi))
    helper :: StateT PState (Parsec Void [Char]) Expr
-> Parser (Either ParamComp b)
helper StateT PState (Parsec Void [Char]) Expr
p = forall a. Parser a -> Parser a
braces forall a b. (a -> b) -> a -> b
$ do
      RType BTyCon BTyVar RReft
t <- forall c tv r. r -> RType c tv r
RHole forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r. r -> UReft r
uTop forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, Expr) -> Reft
Reft forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol
"VV",) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void [Char]) Expr
p
      forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ RType BTyCon BTyVar RReft -> ParamComp
nullPC RType BTyCon BTyVar RReft
t)


bareArgP :: Symbol -> Parser BareType
bareArgP :: Symbol
-> StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
bareArgP Symbol
vvv
  =  Symbol
-> StateT PState (Parsec Void [Char]) Expr
-> Parser (Reft -> RType BTyCon BTyVar RReft)
-> StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
refDefP Symbol
vvv StateT PState (Parsec Void [Char]) Expr
refasHoleP Parser (Reft -> RType BTyCon BTyVar RReft)
bbaseP    -- starts with '{'
 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
holeP                            -- starts with '_'
 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *) b. Monad m => m (Reft -> b) -> m b
dummyP Parser (Reft -> RType BTyCon BTyVar RReft)
bbaseP
 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall a. Parser a -> Parser a
parens StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
bareTypeP                 -- starts with '('
                                      -- starts with '_', '[', '(', lower, upper
 forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"bareArgP"

bareAtomP :: (Parser Expr -> Parser (Reft -> BareType) -> Parser BareType)
          -> Parser BareType
bareAtomP :: (StateT PState (Parsec Void [Char]) Expr
 -> Parser (Reft -> RType BTyCon BTyVar RReft)
 -> StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft))
-> StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
bareAtomP StateT PState (Parsec Void [Char]) Expr
-> Parser (Reft -> RType BTyCon BTyVar RReft)
-> StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
ref
  =  StateT PState (Parsec Void [Char]) Expr
-> Parser (Reft -> RType BTyCon BTyVar RReft)
-> StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
ref StateT PState (Parsec Void [Char]) Expr
refasHoleP Parser (Reft -> RType BTyCon BTyVar RReft)
bbaseP
 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
holeP
 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *) b. Monad m => m (Reft -> b) -> m b
dummyP Parser (Reft -> RType BTyCon BTyVar RReft)
bbaseP
 forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"bareAtomP"

bareAtomBindP :: Parser BareType
bareAtomBindP :: StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
bareAtomBindP = (StateT PState (Parsec Void [Char]) Expr
 -> Parser (Reft -> RType BTyCon BTyVar RReft)
 -> StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft))
-> StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
bareAtomP StateT PState (Parsec Void [Char]) Expr
-> Parser (Reft -> RType BTyCon BTyVar RReft)
-> StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
refBindBindP


-- Either
--  { x : t | ra }
-- or
--  { ra }
refBindBindP :: Parser Expr
             -> Parser (Reft -> BareType)
             -> Parser BareType
refBindBindP :: StateT PState (Parsec Void [Char]) Expr
-> Parser (Reft -> RType BTyCon BTyVar RReft)
-> StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
refBindBindP StateT PState (Parsec Void [Char]) Expr
rp Parser (Reft -> RType BTyCon BTyVar RReft)
kindP'
  = forall a. Parser a -> Parser a
braces (
      (do
              Symbol
x  <- Parser Symbol
symbolP
              ()
_ <- [Char] -> Parser ()
reservedOp [Char]
":"
              -- NOSUBST i  <- freshIntP
              Reft -> RType BTyCon BTyVar RReft
t  <- Parser (Reft -> RType BTyCon BTyVar RReft)
kindP'
              [Char] -> Parser ()
reservedOp [Char]
"|"
              Expr
ra <- StateT PState (Parsec Void [Char]) Expr
rp
              -- xi is a unique var based on the name in x.
              -- su replaces any use of x in the balance of the expression with the unique val
              -- NOSUBST let xi = intSymbol x i
              -- NOSUBST let su v = if v == x then xi else v
              forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ {- substa su $ NOSUBST -} Reft -> RType BTyCon BTyVar RReft
t ((Symbol, Expr) -> Reft
Reft (Symbol
x, Expr
ra)) )
     forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (forall c tv r. r -> RType c tv r
RHole forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r. r -> UReft r
uTop forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, Expr) -> Reft
Reft forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol
"VV",) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void [Char]) Expr
rp)
     forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"refBindBindP"
   )


refDefP :: Symbol
        -> Parser Expr
        -> Parser (Reft -> BareType)
        -> Parser BareType
refDefP :: Symbol
-> StateT PState (Parsec Void [Char]) Expr
-> Parser (Reft -> RType BTyCon BTyVar RReft)
-> StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
refDefP Symbol
sym StateT PState (Parsec Void [Char]) Expr
rp Parser (Reft -> RType BTyCon BTyVar RReft)
kindP' = forall a. Parser a -> Parser a
braces forall a b. (a -> b) -> a -> b
$ do
  Symbol
x       <- Symbol -> Parser Symbol
optBindP Symbol
sym
  -- NOSUBST i       <- freshIntP
  Reft -> RType BTyCon BTyVar RReft
t       <- forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (Parser (Reft -> RType BTyCon BTyVar RReft)
kindP' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* [Char] -> Parser ()
reservedOp [Char]
"|") forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *) a. Monad m => a -> m a
return (forall c tv r. r -> RType c tv r
RHole forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r. r -> UReft r
uTop) forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"refDefP"
  Expr
ra      <- StateT PState (Parsec Void [Char]) Expr
rp
  -- xi is a unique var based on the name in x.
  -- su replaces any use of x in the balance of the expression with the unique val
  -- NOSUBST let xi   = intSymbol x i
  -- NOSUBST let su v = if v == x then xi else v
  forall (m :: * -> *) a. Monad m => a -> m a
return   forall a b. (a -> b) -> a -> b
$ {- substa su $ NOSUBST -} Reft -> RType BTyCon BTyVar RReft
t ((Symbol, Expr) -> Reft
Reft (Symbol
x, Expr
ra))
       -- substa su . t . Reft . (x,) <$> (rp <* spaces))
      --  <|> ((RHole . uTop . Reft . ("VV",)) <$> (rp <* spaces))

refP :: Parser (Reft -> BareType) -> Parser BareType
refP :: Parser (Reft -> RType BTyCon BTyVar RReft)
-> StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
refP = StateT PState (Parsec Void [Char]) Expr
-> Parser (Reft -> RType BTyCon BTyVar RReft)
-> StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
refBindBindP StateT PState (Parsec Void [Char]) Expr
refaP

relrefaP :: Parser RelExpr
relrefaP :: Parser RelExpr
relrefaP =
  forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (Expr -> RelExpr -> RelExpr
ERUnChecked forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void [Char]) Expr
refaP forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* [Char] -> Parser ()
reserved [Char]
":=>" forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser RelExpr
relrefaP)
    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 (Expr -> RelExpr -> RelExpr
ERChecked forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void [Char]) Expr
refaP forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* [Char] -> Parser ()
reserved [Char]
"!=>" forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser RelExpr
relrefaP)
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Expr -> RelExpr
ERBasic forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void [Char]) Expr
refaP

-- "sym :" or return the devault sym
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

holeP :: Parser BareType
holeP :: StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
holeP    = [Char] -> Parser ()
reserved [Char]
"_" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return (forall c tv r. r -> RType c tv r
RHole forall a b. (a -> b) -> a -> b
$ forall r. r -> UReft r
uTop forall a b. (a -> b) -> a -> b
$ (Symbol, Expr) -> Reft
Reft (Symbol
"VV", Expr
hole))

holeRefP :: Parser (Reft -> BareType)
holeRefP :: Parser (Reft -> RType BTyCon BTyVar RReft)
holeRefP = [Char] -> Parser ()
reserved [Char]
"_" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return (forall c tv r. r -> RType c tv r
RHole forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r. r -> UReft r
uTop)

-- NOPROP refasHoleP :: Parser Expr
-- NOPROP refasHoleP  = try refaP
-- NOPROP          <|> (reserved "_" >> return hole)

refasHoleP :: Parser Expr
refasHoleP :: StateT PState (Parsec Void [Char]) Expr
refasHoleP
  =  ([Char] -> Parser ()
reserved [Char]
"_" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return Expr
hole)
 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT PState (Parsec Void [Char]) Expr
refaP
 forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"refasHoleP"

bbaseP :: Parser (Reft -> BareType)
bbaseP :: Parser (Reft -> RType BTyCon BTyVar RReft)
bbaseP
  =  Parser (Reft -> RType BTyCon BTyVar RReft)
holeRefP  -- Starts with '_'
 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 forall tv r.
Maybe (RType BTyCon tv (UReft r))
-> [RTProp BTyCon tv (UReft r)] -> r -> RType BTyCon tv (UReft r)
bLst (forall a. Parser a -> Parser a
brackets (forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
bareTypeP)) forall tv r c.
(IsString tv, Monoid r) =>
Parser [Ref (RType c tv r) (RType BTyCon BTyVar RReft)]
predicatesP
 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 forall r.
(PPrint r, Reftable r, Reftable (RType BTyCon BTyVar (UReft r)),
 Reftable (RTProp BTyCon BTyVar (UReft r))) =>
[(Maybe Symbol, RType BTyCon BTyVar (UReft r))]
-> [RTProp BTyCon BTyVar (UReft r)]
-> r
-> RType BTyCon BTyVar (UReft r)
bTup (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 (Maybe Symbol, a)
maybeBind StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
bareTypeP) Parser [Char]
comma) forall tv r c.
(IsString tv, Monoid r) =>
Parser [Ref (RType c tv r) (RType BTyCon BTyVar RReft)]
predicatesP
 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 (Reft -> RType BTyCon BTyVar RReft)
parseHelper  -- starts with lower
 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *) a1 a2 a3 a4 r.
Monad m =>
(a1 -> a2 -> a3 -> a4 -> r) -> m a1 -> m a2 -> m a3 -> m a4 -> m r
liftM4 forall c tv r.
c
-> [RTProp c tv (UReft r)]
-> [RType c tv (UReft r)]
-> Predicate
-> r
-> RType c tv (UReft r)
bCon Parser BTyCon
bTyConP forall tv r c.
(IsString tv, Monoid r) =>
Parser [Ref (RType c tv r) (RType BTyCon BTyVar RReft)]
predicatesP (forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
bareTyArgP) Parser Predicate
mmonoPredicateP
           -- starts with "'" or upper case char
 forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"bbaseP"
 where
   parseHelper :: Parser (Reft -> RType BTyCon BTyVar RReft)
parseHelper = do
     Symbol
l <- Parser Symbol
lowerIdP
     Symbol -> Parser (Reft -> RType BTyCon BTyVar RReft)
lowerIdTail Symbol
l

maybeBind :: Parser a -> Parser (Maybe Symbol, a)
maybeBind :: forall a. Parser a -> Parser (Maybe Symbol, a)
maybeBind Parser a
parser = do {Maybe Symbol
bd <- forall {f :: * -> *} {e} {s} {a}.
MonadParsec e s f =>
f a -> f (Maybe a)
maybeP' Parser Symbol
bbindP; a
ty <- Parser a
parser ; forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Symbol
bd, a
ty)}
  where
    maybeP' :: f a -> f (Maybe a)
maybeP' f a
p = forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f a
p)
             forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing

lowerIdTail :: Symbol -> Parser (Reft -> BareType)
lowerIdTail :: Symbol -> Parser (Reft -> RType BTyCon BTyVar RReft)
lowerIdTail Symbol
l =
          forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (t :: * -> *) r tv c.
(Foldable t, PPrint r, Reftable r) =>
tv -> t (RType c tv (UReft r)) -> r -> RType c tv (UReft r)
bAppTy (Symbol -> BTyVar
bTyVar Symbol
l)) (forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
bareTyArgP)
      forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall tv r c. tv -> Predicate -> r -> RType c tv (UReft r)
bRVar (Symbol -> BTyVar
bTyVar Symbol
l)) Parser Predicate
monoPredicateP

bTyConP :: Parser BTyCon
bTyConP :: Parser BTyCon
bTyConP
  =  ([Char] -> Parser ()
reservedOp [Char]
"'" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (LocSymbol -> BTyCon
mkPromotedBTyCon forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser LocSymbol
locUpperIdP))
 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> LocSymbol -> BTyCon
mkBTyCon forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser LocSymbol
locUpperIdP
 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved [Char]
"*" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return (LocSymbol -> BTyCon
mkBTyCon (forall a. a -> Located a
dummyLoc forall a b. (a -> b) -> a -> b
$ forall a. Symbolic a => a -> Symbol
symbol ([Char]
"*" :: String))))
 forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"bTyConP"

mkPromotedBTyCon :: LocSymbol -> BTyCon
mkPromotedBTyCon :: LocSymbol -> BTyCon
mkPromotedBTyCon LocSymbol
x = LocSymbol -> Bool -> Bool -> BTyCon
BTyCon LocSymbol
x Bool
False Bool
True -- (consSym '\'' <$> x) False True

classBTyConP :: Parser BTyCon
classBTyConP :: Parser BTyCon
classBTyConP = LocSymbol -> BTyCon
mkClassBTyCon forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser LocSymbol
locUpperIdP

mkClassBTyCon :: LocSymbol -> BTyCon
mkClassBTyCon :: LocSymbol -> BTyCon
mkClassBTyCon LocSymbol
x = LocSymbol -> Bool -> Bool -> BTyCon
BTyCon LocSymbol
x Bool
True Bool
False

bbaseNoAppP :: Parser (Reft -> BareType)
bbaseNoAppP :: Parser (Reft -> RType BTyCon BTyVar RReft)
bbaseNoAppP
  =  Parser (Reft -> RType BTyCon BTyVar RReft)
holeRefP
 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 forall tv r.
Maybe (RType BTyCon tv (UReft r))
-> [RTProp BTyCon tv (UReft r)] -> r -> RType BTyCon tv (UReft r)
bLst (forall a. Parser a -> Parser a
brackets (forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
bareTypeP)) forall tv r c.
(IsString tv, Monoid r) =>
Parser [Ref (RType c tv r) (RType BTyCon BTyVar RReft)]
predicatesP
 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 forall r.
(PPrint r, Reftable r, Reftable (RType BTyCon BTyVar (UReft r)),
 Reftable (RTProp BTyCon BTyVar (UReft r))) =>
[(Maybe Symbol, RType BTyCon BTyVar (UReft r))]
-> [RTProp BTyCon BTyVar (UReft r)]
-> r
-> RType BTyCon BTyVar (UReft r)
bTup (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 (Maybe Symbol, a)
maybeBind StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
bareTypeP) Parser [Char]
comma) forall tv r c.
(IsString tv, Monoid r) =>
Parser [Ref (RType c tv r) (RType BTyCon BTyVar RReft)]
predicatesP
 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 (m :: * -> *) a1 a2 a3 a4 r.
Monad m =>
(a1 -> a2 -> a3 -> a4 -> r) -> m a1 -> m a2 -> m a3 -> m a4 -> m r
liftM4 forall c tv r.
c
-> [RTProp c tv (UReft r)]
-> [RType c tv (UReft r)]
-> Predicate
-> r
-> RType c tv (UReft r)
bCon Parser BTyCon
bTyConP forall tv r c.
(IsString tv, Monoid r) =>
Parser [Ref (RType c tv r) (RType BTyCon BTyVar RReft)]
predicatesP (forall (m :: * -> *) a. Monad m => a -> m a
return []) (forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Monoid a => a
mempty))
 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 forall tv r c. tv -> Predicate -> r -> RType c tv (UReft r)
bRVar (Symbol -> BTyVar
bTyVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Symbol
lowerIdP) Parser Predicate
monoPredicateP
 forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"bbaseNoAppP"

bareTyArgP :: Parser BareType
bareTyArgP :: StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
bareTyArgP
  =  (forall c tv r. Located Expr -> RType c tv r
RExprArg forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Expression a => a -> Expr
expr forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser (Located Integer)
locNatural)
 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
braces forall a b. (a -> b) -> a -> b
$ forall c tv r. Located Expr -> RType c tv r
RExprArg forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Parser a -> Parser (Located a)
located StateT PState (Parsec Void [Char]) 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 StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
bareAtomNoAppP
 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 StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
bareTypeP)
 forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"bareTyArgP"

bareAtomNoAppP :: Parser BareType
bareAtomNoAppP :: StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
bareAtomNoAppP
  =  Parser (Reft -> RType BTyCon BTyVar RReft)
-> StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
refP Parser (Reft -> RType BTyCon BTyVar RReft)
bbaseNoAppP
 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *) b. Monad m => m (Reft -> b) -> m b
dummyP Parser (Reft -> RType BTyCon BTyVar RReft)
bbaseNoAppP
 forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"bareAtomNoAppP"


constraintP :: Parser BareType
constraintP :: StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
constraintP
  = do [(LocSymbol, RType BTyCon BTyVar RReft)]
xts <- Parser [(LocSymbol, RType BTyCon BTyVar RReft)]
constraintEnvP
       RType BTyCon BTyVar RReft
t1  <- StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
bareTypeP
       [Char] -> Parser ()
reservedOp [Char]
"<:"
       forall c tv r. RTypeRep c tv r -> RType c tv r
fromRTypeRep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c tv r.
[(RTVar tv (RType c tv ()), r)]
-> [PVar (RType c tv ())]
-> [Symbol]
-> [RFInfo]
-> [r]
-> [RType c tv r]
-> RType c tv r
-> RTypeRep c tv r
RTypeRep [] []
                               ((forall a. Located a -> a
val forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(LocSymbol, RType BTyCon BTyVar RReft)]
xts) forall a. [a] -> [a] -> [a]
++ [Symbol
dummySymbol])
                               (forall a. Int -> a -> [a]
replicate (forall (t :: * -> *) a. Foldable t => t a -> Int
length [(LocSymbol, RType BTyCon BTyVar RReft)]
xts forall a. Num a => a -> a -> a
+ Int
1) RFInfo
defRFInfo)
                               (forall a. Int -> a -> [a]
replicate (forall (t :: * -> *) a. Foldable t => t a -> Int
length [(LocSymbol, RType BTyCon BTyVar RReft)]
xts forall a. Num a => a -> a -> a
+ Int
1) forall a. Monoid a => a
mempty)
                               ((forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(LocSymbol, RType BTyCon BTyVar RReft)]
xts) forall a. [a] -> [a] -> [a]
++ [RType BTyCon BTyVar RReft
t1]) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
bareTypeP

constraintEnvP :: Parser [(LocSymbol, BareType)]
constraintEnvP :: Parser [(LocSymbol, RType BTyCon BTyVar RReft)]
constraintEnvP
   =  forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (do [(LocSymbol, RType BTyCon BTyVar RReft)]
xts <- forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy Parser (LocSymbol, RType BTyCon BTyVar RReft)
tyBindNoLocP Parser [Char]
comma
              [Char] -> Parser ()
reservedOp [Char]
"|-"
              forall (m :: * -> *) a. Monad m => a -> m a
return [(LocSymbol, RType BTyCon BTyVar RReft)]
xts)
  forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *) a. Monad m => a -> m a
return []
  forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"constraintEnvP"

rrTy :: Monoid r => RType c tv r -> RType c tv r -> RType c tv r
rrTy :: forall r c tv.
Monoid r =>
RType c tv r -> RType c tv r -> RType c tv r
rrTy RType c tv r
ct = forall c tv r.
[(Symbol, RType c tv r)]
-> r -> Oblig -> RType c tv r -> RType c tv r
RRTy ([(Symbol, RType c tv r)]
xts forall a. [a] -> [a] -> [a]
++ [(Symbol
dummySymbol, RType c tv r
tr)]) forall a. Monoid a => a
mempty Oblig
OCons
  where
    tr :: RType c tv r
tr   = forall c tv r. RTypeRep c tv r -> RType c tv r
ty_res RTypeRep c tv r
trep
    xts :: [(Symbol, RType c tv r)]
xts  = forall a b. [a] -> [b] -> [(a, b)]
zip (forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds RTypeRep c tv r
trep) (forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args RTypeRep c tv r
trep)
    trep :: RTypeRep c tv r
trep = forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep RType c tv r
ct

--  "forall <z w> . TYPE"
-- or
--  "forall x y <z :: Nat, w :: Int> . TYPE"
bareAllP :: Parser BareType
bareAllP :: StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
bareAllP = do
  SourcePos
sp <- forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
getSourcePos
  [BTyVar]
as  <- Parser [BTyVar]
tyVarDefsP
  [PVar BSort]
ps  <- forall a. Parser a -> Parser a
angles StateT PState (Parsec Void [Char]) [PVar BSort]
inAngles
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *) a. Monad m => a -> m a
return []
  [Char]
_ <- Parser [Char]
dot
  RType BTyCon BTyVar RReft
t <- StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
bareTypeP
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall {r} {c} {tv}.
Monoid r =>
RTVU c tv -> RType c tv r -> RType c tv r
rAllT (forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (SourcePos
-> PVar BSort
-> RType BTyCon BTyVar RReft
-> RType BTyCon BTyVar RReft
rAllP SourcePos
sp) RType BTyCon BTyVar RReft
t [PVar BSort]
ps) (forall tv s. tv -> RTVar tv s
makeRTVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [BTyVar]
as)
  where
    rAllT :: RTVU c tv -> RType c tv r -> RType c tv r
rAllT RTVU c tv
a RType c tv r
t = forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVU c tv
a RType c tv r
t forall a. Monoid a => a
mempty
    inAngles :: StateT PState (Parsec Void [Char]) [PVar BSort]
inAngles  = forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try  (forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy  Parser (PVar BSort)
predVarDefP Parser [Char]
comma)

-- See #1907 for why we have to alpha-rename pvar binders
rAllP :: SourcePos -> PVar BSort -> BareType -> BareType
rAllP :: SourcePos
-> PVar BSort
-> RType BTyCon BTyVar RReft
-> RType BTyCon BTyVar RReft
rAllP SourcePos
sp PVar BSort
p RType BTyCon BTyVar RReft
t = forall c tv r. PVU c tv -> RType c tv r -> RType c tv r
RAllP PVar BSort
p' ({- F.tracepp "rAllP" $ -} PVar BSort
-> PVar BSort
-> RType BTyCon BTyVar RReft
-> RType BTyCon BTyVar RReft
substPVar PVar BSort
p PVar BSort
p' RType BTyCon BTyVar RReft
t)
  where
    p' :: PVar BSort
p'  = PVar BSort
p { pname :: Symbol
pname = Symbol
pn' }
    pn' :: Symbol
pn' = forall t. PVar t -> Symbol
pname PVar BSort
p forall a. Show a => Symbol -> a -> Symbol
`intSymbol` Int
lin forall a. Show a => Symbol -> a -> Symbol
`intSymbol` Int
col
    lin :: Int
lin = Pos -> Int
unPos (SourcePos -> Pos
sourceLine SourcePos
sp)
    col :: Int
col = Pos -> Int
unPos (SourcePos -> Pos
sourceColumn  SourcePos
sp)

tyVarDefsP :: Parser [BTyVar]
tyVarDefsP :: Parser [BTyVar]
tyVarDefsP
  = forall a. Parser a -> Parser a
parens (forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many (Symbol -> BTyVar
bTyVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Symbol
tyKindVarIdP))
 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many (Symbol -> BTyVar
bTyVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Symbol
tyVarIdP)
 forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"tyVarDefsP"

tyKindVarIdP :: Parser Symbol
tyKindVarIdP :: Parser Symbol
tyKindVarIdP = do
   Symbol
tv <- Parser Symbol
tyVarIdP
   do [Char] -> Parser ()
reservedOp [Char]
"::"; RType BTyCon BTyVar RReft
_ <- StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
kindP; forall (m :: * -> *) a. Monad m => a -> m a
return Symbol
tv forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *) a. Monad m => a -> m a
return Symbol
tv

kindP :: Parser BareType
kindP :: StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
kindP = StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
bareAtomBindP

predVarDefsP :: Parser [PVar BSort]
predVarDefsP :: StateT PState (Parsec Void [Char]) [PVar BSort]
predVarDefsP
  =  forall a. Parser a -> Parser a
angles (forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy1 Parser (PVar BSort)
predVarDefP Parser [Char]
comma)
 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *) a. Monad m => a -> m a
return []
 forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"predVarDefP"

predVarDefP :: Parser (PVar BSort)
predVarDefP :: Parser (PVar BSort)
predVarDefP
  = forall t t1. Symbol -> t -> [(Symbol, t1)] -> PVar t1
bPVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Symbol
predVarIdP forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Char] -> Parser ()
reservedOp [Char]
"::" forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser [(Symbol, BSort)]
propositionSortP

predVarIdP :: Parser Symbol
predVarIdP :: Parser Symbol
predVarIdP
  = forall a. Symbolic a => a -> Symbol
symbol forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Symbol
tyVarIdP

bPVar :: Symbol -> t -> [(Symbol, t1)] -> PVar t1
bPVar :: forall t t1. Symbol -> t -> [(Symbol, t1)] -> PVar t1
bPVar Symbol
p t
_ [(Symbol, t1)]
xts  = forall t.
Symbol -> PVKind t -> Symbol -> [(t, Symbol, Expr)] -> PVar t
PV Symbol
p (forall t. t -> PVKind t
PVProp t1
τ) Symbol
dummySymbol [(t1, Symbol, Expr)]
τxs
  where
    (Symbol
_, t1
τ) = forall {a}. [Char] -> [a] -> a
safeLast [Char]
"bPVar last" [(Symbol, t1)]
xts
    τxs :: [(t1, Symbol, Expr)]
τxs    = [ (t1
τ', Symbol
x, Symbol -> Expr
EVar Symbol
x) | (Symbol
x, t1
τ') <- forall a. [a] -> [a]
init [(Symbol, t1)]
xts ]
    safeLast :: [Char] -> [a] -> a
safeLast [Char]
_ xs :: [a]
xs@(a
_:[a]
_) = forall a. [a] -> a
last [a]
xs
    safeLast [Char]
msg [a]
_      = forall a. Maybe SrcSpan -> [Char] -> a
panic forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ [Char]
"safeLast with empty list " forall a. [a] -> [a] -> [a]
++ [Char]
msg

propositionSortP :: Parser [(Symbol, BSort)]
propositionSortP :: Parser [(Symbol, BSort)]
propositionSortP = forall a b. (a -> b) -> [a] -> [b]
map (forall b c a. (b -> c) -> (a, b) -> (a, c)
Misc.mapSnd forall c tv r. RType c tv r -> RType c tv ()
toRSort) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser [(Symbol, RType BTyCon BTyVar RReft)]
propositionTypeP

propositionTypeP :: Parser [(Symbol, BareType)]
propositionTypeP :: Parser [(Symbol, RType BTyCon BTyVar RReft)]
propositionTypeP = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. RType BTyCon BTyVar RReft
-> Either [Char] [(Symbol, RType BTyCon BTyVar RReft)]
mkPropositionType forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
bareTypeP

mkPropositionType :: BareType -> Either String [(Symbol, BareType)]
mkPropositionType :: RType BTyCon BTyVar RReft
-> Either [Char] [(Symbol, RType BTyCon BTyVar RReft)]
mkPropositionType RType BTyCon BTyVar RReft
t
  | Bool
isOk      = forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip (forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds RTypeRep BTyCon BTyVar RReft
tRep) (forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args RTypeRep BTyCon BTyVar RReft
tRep)
  | Bool
otherwise = forall a b. a -> Either a b
Left [Char]
mkErr
  where
    isOk :: Bool
isOk      = forall t t1. RType BTyCon t t1 -> Bool
isPropBareType (forall c tv r. RTypeRep c tv r -> RType c tv r
ty_res RTypeRep BTyCon BTyVar RReft
tRep)
    tRep :: RTypeRep BTyCon BTyVar RReft
tRep      = forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep RType BTyCon BTyVar RReft
t
    mkErr :: [Char]
mkErr     = [Char]
"Proposition type with non-Bool output: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
showpp RType BTyCon BTyVar RReft
t

xyP :: Parser x -> Parser a -> Parser y -> Parser (x, y)
xyP :: forall x a y. Parser x -> Parser a -> Parser y -> Parser (x, y)
xyP Parser x
lP Parser a
sepP Parser y
rP =
  (,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser x
lP forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser a
sepP forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser y
rP

dummyBindP :: Parser Symbol
dummyBindP :: Parser Symbol
dummyBindP = Symbol -> Integer -> Symbol
tempSymbol Symbol
"db" forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Integer
freshIntP

isPropBareType :: RType BTyCon t t1 -> Bool
isPropBareType :: forall t t1. RType BTyCon t t1 -> Bool
isPropBareType  = forall t t1. Symbol -> RType BTyCon t t1 -> Bool
isPrimBareType Symbol
boolConName

isPrimBareType :: Symbol -> RType BTyCon t t1 -> Bool
isPrimBareType :: forall t t1. Symbol -> RType BTyCon t t1 -> Bool
isPrimBareType Symbol
n (RApp BTyCon
tc [] [RTProp BTyCon t t1]
_ t1
_) = forall a. Located a -> a
val (BTyCon -> LocSymbol
btc_tc BTyCon
tc) forall a. Eq a => a -> a -> Bool
== Symbol
n
isPrimBareType Symbol
_ RType BTyCon t t1
_                = Bool
False

getClasses :: RType BTyCon t t1 -> [RType BTyCon t t1]
getClasses :: forall t t1. RType BTyCon t t1 -> [RType BTyCon t t1]
getClasses (RApp BTyCon
tc [RType BTyCon t t1]
ts [RTProp BTyCon t t1]
ps t1
r)
  | forall c. TyConable c => c -> Bool
isTuple BTyCon
tc
  = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall t t1. RType BTyCon t t1 -> [RType BTyCon t t1]
getClasses [RType BTyCon t t1]
ts
  | Bool
otherwise
  = [forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp (BTyCon
tc { btc_class :: Bool
btc_class = Bool
True }) [RType BTyCon t t1]
ts [RTProp BTyCon t t1]
ps t1
r]
getClasses RType BTyCon t t1
t
  = [RType BTyCon t t1
t]

dummyP ::  Monad m => m (Reft -> b) -> m b
dummyP :: forall (m :: * -> *) b. Monad m => m (Reft -> b) -> m b
dummyP m (Reft -> b)
fm
  = m (Reft -> b)
fm forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
`ap` forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Monoid a => a
dummyReft

symsP :: (IsString tv, Monoid r)
      => Parser [(Symbol, RType c tv r)]
symsP :: forall tv r c.
(IsString tv, Monoid r) =>
Parser [(Symbol, RType c tv r)]
symsP
  = do [Char] -> Parser ()
reservedOp [Char]
"\\"
       [Symbol]
ss <- forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many Parser Symbol
symbolP
       [Char] -> Parser ()
reservedOp [Char]
"->"
       forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ (, forall tv r c. (IsString tv, Monoid r) => RType c tv r
dummyRSort) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
ss
 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *) a. Monad m => a -> m a
return []
 forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"symsP"

dummyRSort :: (IsString tv, Monoid r) => RType c tv r
dummyRSort :: forall tv r c. (IsString tv, Monoid r) => RType c tv r
dummyRSort
  = forall c tv r. tv -> r -> RType c tv r
RVar tv
"dummy" forall a. Monoid a => a
mempty

predicatesP :: (IsString tv, Monoid r)
            => Parser [Ref (RType c tv r) BareType]
predicatesP :: forall tv r c.
(IsString tv, Monoid r) =>
Parser [Ref (RType c tv r) (RType BTyCon BTyVar RReft)]
predicatesP
   =  forall a. Parser a -> Parser a
angles (forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy1 forall tv r c.
(IsString tv, Monoid r) =>
Parser (Ref (RType c tv r) (RType BTyCon BTyVar RReft))
predicate1P Parser [Char]
comma)
  forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *) a. Monad m => a -> m a
return []
  forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"predicatesP"

predicate1P :: (IsString tv, Monoid r)
            => Parser (Ref (RType c tv r) BareType)
predicate1P :: forall tv r c.
(IsString tv, Monoid r) =>
Parser (Ref (RType c tv r) (RType BTyCon BTyVar RReft))
predicate1P
   =  forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall tv r c.
(IsString tv, Monoid r) =>
Parser [(Symbol, RType c tv r)]
symsP forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser (Reft -> RType BTyCon BTyVar RReft)
-> StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
refP Parser (Reft -> RType BTyCon BTyVar RReft)
bbaseP)
  forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (forall τ r c tv. [(Symbol, τ)] -> r -> Ref τ (RType c tv r)
rPropP [] forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r. Monoid r => Predicate -> UReft r
predUReft forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Predicate
monoPredicate1P)
  forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall a. Parser a -> Parser a
braces (forall τ c.
[((Symbol, τ), Symbol)] -> Expr -> Ref τ (RType c BTyVar RReft)
bRProp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {tv} {r} {c}.
(IsString tv, Monoid r) =>
StateT
  PState (Parsec Void [Char]) [((Symbol, RType c tv r), Symbol)]
symsP' forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT PState (Parsec Void [Char]) Expr
refaP)
  forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"predicate1P"
   where
    symsP' :: StateT
  PState (Parsec Void [Char]) [((Symbol, RType c tv r), Symbol)]
symsP'       = do [(Symbol, RType c tv r)]
ss    <- forall tv r c.
(IsString tv, Monoid r) =>
Parser [(Symbol, RType c tv r)]
symsP
                      [Symbol]
fs    <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Symbol -> Parser Symbol
refreshSym (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RType c tv r)]
ss)
                      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [(Symbol, RType c tv r)]
ss [Symbol]
fs
    refreshSym :: Symbol -> Parser Symbol
refreshSym Symbol
s = forall a. Show a => Symbol -> a -> Symbol
intSymbol Symbol
s forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Integer
freshIntP

mmonoPredicateP :: Parser Predicate
mmonoPredicateP :: Parser Predicate
mmonoPredicateP
   = forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (forall a. Parser a -> Parser a
angles forall a b. (a -> b) -> a -> b
$ forall a. Parser a -> Parser a
angles Parser Predicate
monoPredicate1P)
  forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Monoid a => a
mempty
  forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"mmonoPredicateP"

monoPredicateP :: Parser Predicate
monoPredicateP :: Parser Predicate
monoPredicateP
   = forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (forall a. Parser a -> Parser a
angles Parser Predicate
monoPredicate1P)
  forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Monoid a => a
mempty
  forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"monoPredicateP"

monoPredicate1P :: Parser Predicate
monoPredicate1P :: Parser Predicate
monoPredicate1P
   =  ([Char] -> Parser ()
reserved [Char]
"True" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Monoid a => a
mempty)
  forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (forall t. PVar t -> Predicate
pdVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Parser a -> Parser a
parens Parser (PVar [Char])
predVarUseP)
  forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (forall t. PVar t -> Predicate
pdVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>        Parser (PVar [Char])
predVarUseP)
  forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"monoPredicate1P"

predVarUseP :: Parser (PVar String)
predVarUseP :: Parser (PVar [Char])
predVarUseP
  = do (Symbol
p, ListNE Expr
xs) <- Parser (Symbol, ListNE Expr)
funArgsP
       forall (m :: * -> *) a. Monad m => a -> m a
return   forall a b. (a -> b) -> a -> b
$ forall t.
Symbol -> PVKind t -> Symbol -> [(t, Symbol, Expr)] -> PVar t
PV Symbol
p (forall t. t -> PVKind t
PVProp forall a. IsString a => a
dummyTyId) Symbol
dummySymbol [ (forall a. IsString a => a
dummyTyId, Symbol
dummySymbol, Expr
x) | Expr
x <- ListNE Expr
xs ]

funArgsP :: Parser (Symbol, [Expr])
funArgsP :: Parser (Symbol, ListNE Expr)
funArgsP  = forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try Parser (Symbol, ListNE Expr)
realP forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall {a}. StateT PState (Parsec Void [Char]) (Symbol, [a])
empP forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"funArgsP"
  where
    empP :: StateT PState (Parsec Void [Char]) (Symbol, [a])
empP  = (,[]) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Symbol
predVarIdP
    realP :: Parser (Symbol, ListNE Expr)
realP = do (EVar Symbol
lp, ListNE Expr
xs) <- Expr -> (Expr, ListNE Expr)
splitEApp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void [Char]) Expr
funAppP
               forall (m :: * -> *) a. Monad m => a -> m a
return (Symbol
lp, ListNE Expr
xs)

boundP :: Parser (Bound (Located BareType) Expr)
boundP :: Parser (Bound (Located (RType BTyCon BTyVar RReft)) Expr)
boundP = do
  LocSymbol
name   <- Parser LocSymbol
locUpperIdP
  [Char] -> Parser ()
reservedOp [Char]
"="
  [Located (RType BTyCon BTyVar RReft)]
vs      <- forall {r} {c}.
Monoid r =>
StateT PState (Parsec Void [Char]) [Located (RType c BTyVar r)]
bvsP
  [(LocSymbol, Located (RType BTyCon BTyVar RReft))]
params' <- forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many (forall a. Parser a -> Parser a
parens Parser (LocSymbol, Located (RType BTyCon BTyVar RReft))
tyBindP)
  [(LocSymbol, Located (RType BTyCon BTyVar RReft))]
args    <- StateT
  PState
  (Parsec Void [Char])
  [(LocSymbol, Located (RType BTyCon BTyVar RReft))]
bargsP
  forall t e.
LocSymbol
-> [t] -> [(LocSymbol, t)] -> [(LocSymbol, t)] -> e -> Bound t e
Bound LocSymbol
name [Located (RType BTyCon BTyVar RReft)]
vs [(LocSymbol, Located (RType BTyCon BTyVar RReft))]
params' [(LocSymbol, Located (RType BTyCon BTyVar RReft))]
args forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void [Char]) Expr
predP
 where
    bargsP :: StateT
  PState
  (Parsec Void [Char])
  [(LocSymbol, Located (RType BTyCon BTyVar RReft))]
bargsP =     ( do [Char] -> Parser ()
reservedOp [Char]
"\\"
                      [(LocSymbol, Located (RType BTyCon BTyVar RReft))]
xs <- forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many (forall a. Parser a -> Parser a
parens Parser (LocSymbol, Located (RType BTyCon BTyVar RReft))
tyBindP)
                      [Char] -> Parser ()
reservedOp  [Char]
"->"
                      forall (m :: * -> *) a. Monad m => a -> m a
return [(LocSymbol, Located (RType BTyCon BTyVar RReft))]
xs
                 )
           forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *) a. Monad m => a -> m a
return []
           forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"bargsP"
    bvsP :: StateT PState (Parsec Void [Char]) [Located (RType c BTyVar r)]
bvsP   =     ( do [Char] -> Parser ()
reserved [Char]
"forall"
                      [Located BTyVar]
xs <- forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Symbol -> BTyVar
bTyVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser LocSymbol
locSymbolP)
                      [Char] -> Parser ()
reservedOp  [Char]
"."
                      forall (m :: * -> *) a. Monad m => a -> m a
return (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall c tv r. tv -> r -> RType c tv r
`RVar` forall a. Monoid a => a
mempty) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Located BTyVar]
xs)
                 )
           forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *) a. Monad m => a -> m a
return []


infixGenP :: Assoc -> Parser ()
infixGenP :: Assoc -> Parser ()
infixGenP Assoc
assoc = do
   Maybe Int
p <- Parser (Maybe Int)
maybeDigit
   Symbol
s <- Parser Symbol
infixIdP -- TODO: Andres: infixIdP was defined as many (satisfy (`notElem` [' ', '.'])) which does not make sense at all
   -- Andres: going via Symbol seems unnecessary and wasteful here
   Fixity -> Parser ()
addOperatorP (Maybe Int
-> [Char] -> Maybe (Expr -> Expr -> Expr) -> Assoc -> Fixity
FInfix Maybe Int
p (Symbol -> [Char]
symbolString Symbol
s) forall a. Maybe a
Nothing Assoc
assoc)

infixP :: Parser ()
infixP :: Parser ()
infixP = Assoc -> Parser ()
infixGenP Assoc
AssocLeft

infixlP :: Parser ()
infixlP :: Parser ()
infixlP = Assoc -> Parser ()
infixGenP Assoc
AssocLeft

infixrP :: Parser ()
infixrP :: Parser ()
infixrP = Assoc -> Parser ()
infixGenP Assoc
AssocRight

maybeDigit :: Parser (Maybe Int)
maybeDigit :: Parser (Maybe Int)
maybeDigit
  = forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional (forall a. Parser a -> Parser a
lexeme (forall a. Read a => [Char] -> a
read 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 e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
digitChar))

------------------------------------------------------------------------
----------------------- Wrapped Constructors ---------------------------
------------------------------------------------------------------------

bRProp :: [((Symbol, τ), Symbol)]
       -> Expr -> Ref τ (RType c BTyVar (UReft Reft))
bRProp :: forall τ c.
[((Symbol, τ), Symbol)] -> Expr -> Ref τ (RType c BTyVar RReft)
bRProp []    Expr
_    = forall a. Maybe SrcSpan -> [Char] -> a
panic forall a. Maybe a
Nothing [Char]
"Parse.bRProp empty list"
bRProp [((Symbol, τ), Symbol)]
syms' Expr
epr  = forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, τ)]
ss forall a b. (a -> b) -> a -> b
$ forall tv r c. tv -> Predicate -> r -> RType c tv (UReft r)
bRVar (Symbol -> BTyVar
BTV Symbol
dummyName) forall a. Monoid a => a
mempty Reft
r
  where
    ([(Symbol, τ)]
ss, (Symbol
v, τ
_))  = (forall a. [a] -> [a]
init [(Symbol, τ)]
symsf, forall a. [a] -> a
last [(Symbol, τ)]
symsf)
    symsf :: [(Symbol, τ)]
symsf         = [(Symbol
y, τ
s) | ((Symbol
_, τ
s), Symbol
y) <- [((Symbol, τ), Symbol)]
syms']
    su :: Subst
su            = [(Symbol, Expr)] -> Subst
mkSubst [(Symbol
x, Symbol -> Expr
EVar Symbol
y) | ((Symbol
x, τ
_), Symbol
y) <- [((Symbol, τ), Symbol)]
syms']
    r :: Reft
r             = Subst
su forall a. Subable a => Subst -> a -> a
`subst` (Symbol, Expr) -> Reft
Reft (Symbol
v, Expr
epr)

bRVar :: tv -> Predicate -> r -> RType c tv (UReft r)
bRVar :: forall tv r c. tv -> Predicate -> r -> RType c tv (UReft r)
bRVar tv
α Predicate
p r
r = forall c tv r. tv -> r -> RType c tv r
RVar tv
α (forall r. r -> Predicate -> UReft r
MkUReft r
r Predicate
p)

bLst :: Maybe (RType BTyCon tv (UReft r))
     -> [RTProp BTyCon tv (UReft r)]
     -> r
     -> RType BTyCon tv (UReft r)
bLst :: forall tv r.
Maybe (RType BTyCon tv (UReft r))
-> [RTProp BTyCon tv (UReft r)] -> r -> RType BTyCon tv (UReft r)
bLst (Just RType BTyCon tv (UReft r)
t) [RTProp BTyCon tv (UReft r)]
rs r
r = forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp (LocSymbol -> BTyCon
mkBTyCon forall a b. (a -> b) -> a -> b
$ forall a. a -> Located a
dummyLoc Symbol
listConName) [RType BTyCon tv (UReft r)
t] [RTProp BTyCon tv (UReft r)]
rs (forall r. r -> UReft r
reftUReft r
r)
bLst Maybe (RType BTyCon tv (UReft r))
Nothing  [RTProp BTyCon tv (UReft r)]
rs r
r = forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp (LocSymbol -> BTyCon
mkBTyCon forall a b. (a -> b) -> a -> b
$ forall a. a -> Located a
dummyLoc Symbol
listConName) []  [RTProp BTyCon tv (UReft r)]
rs (forall r. r -> UReft r
reftUReft r
r)

bTup :: (PPrint r, Reftable r, Reftable (RType BTyCon BTyVar (UReft r)), Reftable (RTProp BTyCon BTyVar (UReft r)))
     => [(Maybe Symbol, RType BTyCon BTyVar (UReft r))]
     -> [RTProp BTyCon BTyVar (UReft r)]
     -> r
     -> RType BTyCon BTyVar (UReft r)
bTup :: forall r.
(PPrint r, Reftable r, Reftable (RType BTyCon BTyVar (UReft r)),
 Reftable (RTProp BTyCon BTyVar (UReft r))) =>
[(Maybe Symbol, RType BTyCon BTyVar (UReft r))]
-> [RTProp BTyCon BTyVar (UReft r)]
-> r
-> RType BTyCon BTyVar (UReft r)
bTup [(Maybe Symbol
_,RType BTyCon BTyVar (UReft r)
t)] [RTProp BTyCon BTyVar (UReft r)]
_ r
r
  | forall r. Reftable r => r -> Bool
isTauto r
r  = RType BTyCon BTyVar (UReft r)
t
  | Bool
otherwise  = RType BTyCon BTyVar (UReft r)
t forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`strengthen` forall r. r -> UReft r
reftUReft r
r
bTup [(Maybe Symbol, RType BTyCon BTyVar (UReft r))]
ts [RTProp BTyCon BTyVar (UReft r)]
rs r
r
  | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all forall a. Maybe a -> Bool
Mb.isNothing (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Maybe Symbol, RType BTyCon BTyVar (UReft r))]
ts) Bool -> Bool -> Bool
|| forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Maybe Symbol, RType BTyCon BTyVar (UReft r))]
ts forall a. Ord a => a -> a -> Bool
< Int
2
  = forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp (LocSymbol -> BTyCon
mkBTyCon forall a b. (a -> b) -> a -> b
$ forall a. a -> Located a
dummyLoc Symbol
tupConName) (forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Maybe Symbol, RType BTyCon BTyVar (UReft r))]
ts) [RTProp BTyCon BTyVar (UReft r)]
rs (forall r. r -> UReft r
reftUReft r
r)
  | Bool
otherwise
  = forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp (LocSymbol -> BTyCon
mkBTyCon forall a b. (a -> b) -> a -> b
$ forall a. a -> Located a
dummyLoc Symbol
tupConName) (forall r. Reftable r => r -> r
top forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Maybe Symbol, RType BTyCon BTyVar (UReft r))]
ts) forall {r2}.
Monoid r2 =>
[Ref (RType BTyCon BTyVar r2) (RType BTyCon BTyVar (UReft r))]
rs' (forall r. r -> UReft r
reftUReft r
r)
  where
    args :: [(Symbol, RType BTyCon BTyVar r2)]
args       = [(forall a. a -> Maybe a -> a
Mb.fromMaybe Symbol
dummySymbol Maybe Symbol
x, forall r1 r2 c tv. (r1 -> r2) -> RType c tv r1 -> RType c tv r2
mapReft forall a. Monoid a => a
mempty RType BTyCon BTyVar (UReft r)
t) | (Maybe Symbol
x,RType BTyCon BTyVar (UReft r)
t) <- [(Maybe Symbol, RType BTyCon BTyVar (UReft r))]
ts]
    makeProp :: Int -> Ref (RType BTyCon BTyVar r2) (RType BTyCon BTyVar (UReft r))
makeProp Int
i = forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp (forall a. Int -> [a] -> [a]
take Int
i forall {r2}. Monoid r2 => [(Symbol, RType BTyCon BTyVar r2)]
args) ((forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Maybe Symbol, RType BTyCon BTyVar (UReft r))]
ts)forall a. [a] -> Int -> a
!!Int
i)
    rs' :: [Ref (RType BTyCon BTyVar r2) (RType BTyCon BTyVar (UReft r))]
rs'        = forall {r2}.
Monoid r2 =>
Int -> Ref (RType BTyCon BTyVar r2) (RType BTyCon BTyVar (UReft r))
makeProp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
1..(forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Maybe Symbol, RType BTyCon BTyVar (UReft r))]
tsforall a. Num a => a -> a -> a
-Int
1)]


-- Temporarily restore this hack benchmarks/esop2013-submission/Array.hs fails
-- w/o it
-- TODO RApp Int [] [p] true should be syntactically different than RApp Int [] [] p
-- bCon b s [RProp _ (RHole r1)] [] _ r = RApp b [] [] $ r1 `meet` (MkUReft r mempty s)
bCon :: c
     -> [RTProp c tv (UReft r)]
     -> [RType c tv (UReft r)]
     -> Predicate
     -> r
     -> RType c tv (UReft r)
bCon :: forall c tv r.
c
-> [RTProp c tv (UReft r)]
-> [RType c tv (UReft r)]
-> Predicate
-> r
-> RType c tv (UReft r)
bCon c
b [RTProp c tv (UReft r)]
rs [RType c tv (UReft r)]
ts Predicate
p r
r = forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp c
b [RType c tv (UReft r)]
ts [RTProp c tv (UReft r)]
rs forall a b. (a -> b) -> a -> b
$ forall r. r -> Predicate -> UReft r
MkUReft r
r Predicate
p

bAppTy :: (Foldable t, PPrint r, Reftable r)
       => tv -> t (RType c tv (UReft r)) -> r -> RType c tv (UReft r)
bAppTy :: forall (t :: * -> *) r tv c.
(Foldable t, PPrint r, Reftable r) =>
tv -> t (RType c tv (UReft r)) -> r -> RType c tv (UReft r)
bAppTy tv
v t (RType c tv (UReft r))
ts r
r  = RType c tv (UReft r)
ts' forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`strengthen` forall r. r -> UReft r
reftUReft r
r
  where
    ts' :: RType c tv (UReft r)
ts'        = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\RType c tv (UReft r)
a RType c tv (UReft r)
b -> forall c tv r. RType c tv r -> RType c tv r -> r -> RType c tv r
RAppTy RType c tv (UReft r)
a RType c tv (UReft r)
b forall a. Monoid a => a
mempty) (forall c tv r. tv -> r -> RType c tv r
RVar tv
v forall a. Monoid a => a
mempty) t (RType c tv (UReft r))
ts

reftUReft :: r -> UReft r
reftUReft :: forall r. r -> UReft r
reftUReft r
r    = forall r. r -> Predicate -> UReft r
MkUReft r
r forall a. Monoid a => a
mempty

predUReft :: Monoid r => Predicate -> UReft r
predUReft :: forall r. Monoid r => Predicate -> UReft r
predUReft Predicate
p    = forall r. r -> Predicate -> UReft r
MkUReft forall a. Monoid a => a
dummyReft Predicate
p

dummyReft :: Monoid a => a
dummyReft :: forall a. Monoid a => a
dummyReft      = forall a. Monoid a => a
mempty

dummyTyId :: IsString a => a
dummyTyId :: forall a. IsString a => a
dummyTyId      = a
""

------------------------------------------------------------------
--------------------------- Measures -----------------------------
------------------------------------------------------------------

type BPspec = Pspec LocBareType LocSymbol

-- | The AST for a single parsed spec.
data Pspec ty ctor
  = Meas    (Measure ty ctor)                             -- ^ 'measure' definition
  | Assm    (LocSymbol, ty)                               -- ^ 'assume' signature (unchecked)
  | Asrt    (LocSymbol, ty)                               -- ^ 'assert' signature (checked)
  | LAsrt   (LocSymbol, ty)                               -- ^ 'local' assertion -- TODO RJ: what is this
  | Asrts   ([LocSymbol], (ty, Maybe [Located Expr]))     -- ^ TODO RJ: what is this
  | Impt    Symbol                                        -- ^ 'import' a specification module
  | DDecl   DataDecl                                      -- ^ refined 'data'    declaration
  | NTDecl  DataDecl                                      -- ^ refined 'newtype' declaration
  | Relational (LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr) -- ^ relational signature
  | AssmRel (LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr) -- ^ 'assume' relational signature
  | Class   (RClass ty)                                   -- ^ refined 'class' definition
  | CLaws   (RClass ty)                                   -- ^ 'class laws' definition
  | ILaws   (RILaws ty)
  | RInst   (RInstance ty)                                -- ^ refined 'instance' definition
  | Incl    FilePath                                      -- ^ 'include' a path -- TODO: deprecate
  | Invt    ty                                            -- ^ 'invariant' specification
  | Using  (ty, ty)                                       -- ^ 'using' declaration (for local invariants on a type)
  | Alias   (Located (RTAlias Symbol BareType))           -- ^ 'type' alias declaration
  | EAlias  (Located (RTAlias Symbol Expr))               -- ^ 'predicate' alias declaration
  | Embed   (LocSymbol, FTycon, TCArgs)                   -- ^ 'embed' declaration
  | Qualif  Qualifier                                     -- ^ 'qualif' definition
  | LVars   LocSymbol                                     -- ^ 'lazyvar' annotation, defer checks to *use* sites
  | Lazy    LocSymbol                                     -- ^ 'lazy' annotation, skip termination check on binder
  | Fail    LocSymbol                                     -- ^ 'fail' annotation, the binder should be unsafe
  | Rewrite LocSymbol                                     -- ^ 'rewrite' annotation, the binder generates a rewrite rule
  | Rewritewith (LocSymbol, [LocSymbol])                  -- ^ 'rewritewith' annotation, the first binder is using the rewrite rules of the second list,
  | Insts   (LocSymbol, Maybe Int)                        -- ^ 'auto-inst' or 'ple' annotation; use ple locally on binder
  | HMeas   LocSymbol                                     -- ^ 'measure' annotation; lift Haskell binder as measure
  | Reflect LocSymbol                                     -- ^ 'reflect' annotation; reflect Haskell binder as function in logic
  | Inline  LocSymbol                                     -- ^ 'inline' annotation;  inline (non-recursive) binder as an alias
  | Ignore  LocSymbol                                     -- ^ 'ignore' annotation; skip all checks inside this binder
  | ASize   LocSymbol                                     -- ^ 'autosize' annotation; automatically generate size metric for this type
  | HBound  LocSymbol                                     -- ^ 'bound' annotation; lift Haskell binder as an abstract-refinement "bound"
  | PBound  (Bound ty Expr)                               -- ^ 'bound' definition
  | Pragma  (Located String)                              -- ^ 'LIQUID' pragma, used to save configuration options in source files
  | CMeas   (Measure ty ())                               -- ^ 'class measure' definition
  | IMeas   (Measure ty ctor)                             -- ^ 'instance measure' definition
  | Varia   (LocSymbol, [Variance])                       -- ^ 'variance' annotations, marking type constructor params as co-, contra-, or in-variant
  | DSize   ([ty], LocSymbol)                             -- ^ 'data size' annotations, generating fancy termination metric
  | BFix    ()                                            -- ^ fixity annotation
  | Define  (LocSymbol, Symbol)                           -- ^ 'define' annotation for specifying aliases c.f. `include-CoreToLogic.lg`
  deriving (Pspec ty ctor -> DataType
Pspec ty ctor -> Constr
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall {ty} {ctor}.
(Data ty, Data ctor) =>
Typeable (Pspec ty ctor)
forall ty ctor. (Data ty, Data ctor) => Pspec ty ctor -> DataType
forall ty ctor. (Data ty, Data ctor) => Pspec ty ctor -> Constr
forall ty ctor.
(Data ty, Data ctor) =>
(forall b. Data b => b -> b) -> Pspec ty ctor -> Pspec ty ctor
forall ty ctor u.
(Data ty, Data ctor) =>
Int -> (forall d. Data d => d -> u) -> Pspec ty ctor -> u
forall ty ctor u.
(Data ty, Data ctor) =>
(forall d. Data d => d -> u) -> Pspec ty ctor -> [u]
forall ty ctor r r'.
(Data ty, Data ctor) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Pspec ty ctor -> r
forall ty ctor r r'.
(Data ty, Data ctor) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Pspec ty ctor -> r
forall ty ctor (m :: * -> *).
(Data ty, Data ctor, Monad m) =>
(forall d. Data d => d -> m d)
-> Pspec ty ctor -> m (Pspec ty ctor)
forall ty ctor (m :: * -> *).
(Data ty, Data ctor, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> Pspec ty ctor -> m (Pspec ty ctor)
forall ty ctor (c :: * -> *).
(Data ty, Data ctor) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Pspec ty ctor)
forall ty ctor (c :: * -> *).
(Data ty, Data ctor) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Pspec ty ctor -> c (Pspec ty ctor)
forall ty ctor (t :: * -> *) (c :: * -> *).
(Data ty, Data ctor, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Pspec ty ctor))
forall ty ctor (t :: * -> * -> *) (c :: * -> *).
(Data ty, Data ctor, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Pspec ty ctor))
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Pspec ty ctor)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Pspec ty ctor -> c (Pspec ty ctor)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Pspec ty ctor))
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> Pspec ty ctor -> m (Pspec ty ctor)
$cgmapMo :: forall ty ctor (m :: * -> *).
(Data ty, Data ctor, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> Pspec ty ctor -> m (Pspec ty ctor)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> Pspec ty ctor -> m (Pspec ty ctor)
$cgmapMp :: forall ty ctor (m :: * -> *).
(Data ty, Data ctor, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> Pspec ty ctor -> m (Pspec ty ctor)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> Pspec ty ctor -> m (Pspec ty ctor)
$cgmapM :: forall ty ctor (m :: * -> *).
(Data ty, Data ctor, Monad m) =>
(forall d. Data d => d -> m d)
-> Pspec ty ctor -> m (Pspec ty ctor)
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Pspec ty ctor -> u
$cgmapQi :: forall ty ctor u.
(Data ty, Data ctor) =>
Int -> (forall d. Data d => d -> u) -> Pspec ty ctor -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Pspec ty ctor -> [u]
$cgmapQ :: forall ty ctor u.
(Data ty, Data ctor) =>
(forall d. Data d => d -> u) -> Pspec ty ctor -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Pspec ty ctor -> r
$cgmapQr :: forall ty ctor r r'.
(Data ty, Data ctor) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Pspec ty ctor -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Pspec ty ctor -> r
$cgmapQl :: forall ty ctor r r'.
(Data ty, Data ctor) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Pspec ty ctor -> r
gmapT :: (forall b. Data b => b -> b) -> Pspec ty ctor -> Pspec ty ctor
$cgmapT :: forall ty ctor.
(Data ty, Data ctor) =>
(forall b. Data b => b -> b) -> Pspec ty ctor -> Pspec ty ctor
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Pspec ty ctor))
$cdataCast2 :: forall ty ctor (t :: * -> * -> *) (c :: * -> *).
(Data ty, Data ctor, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Pspec ty ctor))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Pspec ty ctor))
$cdataCast1 :: forall ty ctor (t :: * -> *) (c :: * -> *).
(Data ty, Data ctor, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Pspec ty ctor))
dataTypeOf :: Pspec ty ctor -> DataType
$cdataTypeOf :: forall ty ctor. (Data ty, Data ctor) => Pspec ty ctor -> DataType
toConstr :: Pspec ty ctor -> Constr
$ctoConstr :: forall ty ctor. (Data ty, Data ctor) => Pspec ty ctor -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Pspec ty ctor)
$cgunfold :: forall ty ctor (c :: * -> *).
(Data ty, Data ctor) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Pspec ty ctor)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Pspec ty ctor -> c (Pspec ty ctor)
$cgfoldl :: forall ty ctor (c :: * -> *).
(Data ty, Data ctor) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Pspec ty ctor -> c (Pspec ty ctor)
Data, Int -> Pspec ty ctor -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
forall ty ctor.
(PPrint ty, PPrint ctor, Show ty) =>
Int -> Pspec ty ctor -> ShowS
forall ty ctor.
(PPrint ty, PPrint ctor, Show ty) =>
[Pspec ty ctor] -> ShowS
forall ty ctor.
(PPrint ty, PPrint ctor, Show ty) =>
Pspec ty ctor -> [Char]
showList :: [Pspec ty ctor] -> ShowS
$cshowList :: forall ty ctor.
(PPrint ty, PPrint ctor, Show ty) =>
[Pspec ty ctor] -> ShowS
show :: Pspec ty ctor -> [Char]
$cshow :: forall ty ctor.
(PPrint ty, PPrint ctor, Show ty) =>
Pspec ty ctor -> [Char]
showsPrec :: Int -> Pspec ty ctor -> ShowS
$cshowsPrec :: forall ty ctor.
(PPrint ty, PPrint ctor, Show ty) =>
Int -> Pspec ty ctor -> ShowS
Show, Typeable)

instance (PPrint ty, PPrint ctor) => PPrint (Pspec ty ctor) where
  pprintTidy :: Tidy -> Pspec ty ctor -> Doc
pprintTidy = forall ty ctor.
(PPrint ty, PPrint ctor) =>
Tidy -> Pspec ty ctor -> Doc
ppPspec

splice :: PJ.Doc -> [PJ.Doc] -> PJ.Doc
splice :: Doc -> [Doc] -> Doc
splice Doc
sep = [Doc] -> Doc
PJ.hcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> [Doc]
PJ.punctuate Doc
sep

ppAsserts :: (PPrint t) => Tidy -> [LocSymbol] -> t -> Maybe [Located Expr] -> PJ.Doc
ppAsserts :: forall t.
PPrint t =>
Tidy -> [LocSymbol] -> t -> Maybe [Located Expr] -> Doc
ppAsserts Tidy
k [LocSymbol]
lxs t
t Maybe [Located Expr]
mles
  = [Doc] -> Doc
PJ.hcat [ Doc -> [Doc] -> Doc
splice Doc
", " (forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a. Located a -> a
val forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [LocSymbol]
lxs))
            , Doc
" :: "
            , forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k t
t
            , forall {f :: * -> *} {b}.
(PPrint (f b), Functor f) =>
Maybe (f (Located b)) -> Doc
ppLes Maybe [Located Expr]
mles
            ]
  where
    ppLes :: Maybe (f (Located b)) -> Doc
ppLes Maybe (f (Located b))
Nothing    = Doc
""
    ppLes (Just f (Located b)
les) = Doc
"/" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (forall a. Located a -> a
val forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (Located b)
les)

ppPspec :: (PPrint t, PPrint c) => Tidy -> Pspec t c -> PJ.Doc
ppPspec :: forall ty ctor.
(PPrint ty, PPrint ctor) =>
Tidy -> Pspec ty ctor -> Doc
ppPspec Tidy
k (Meas Measure t c
m)
  = Doc
"measure" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Measure t c
m
ppPspec Tidy
k (Assm (LocSymbol
lx, t
t))
  = Doc
"assume"  Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (forall a. Located a -> a
val LocSymbol
lx) Doc -> Doc -> Doc
<+> Doc
"::" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k t
t
ppPspec Tidy
k (Asrt (LocSymbol
lx, t
t))
  = Doc
"assert"  Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (forall a. Located a -> a
val LocSymbol
lx) Doc -> Doc -> Doc
<+> Doc
"::" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k t
t
ppPspec Tidy
k (LAsrt (LocSymbol
lx, t
t))
  = Doc
"local assert"  Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (forall a. Located a -> a
val LocSymbol
lx) Doc -> Doc -> Doc
<+> Doc
"::" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k t
t
ppPspec Tidy
k (Asrts ([LocSymbol]
lxs, (t
t, Maybe [Located Expr]
les)))
  = forall t.
PPrint t =>
Tidy -> [LocSymbol] -> t -> Maybe [Located Expr] -> Doc
ppAsserts Tidy
k [LocSymbol]
lxs t
t Maybe [Located Expr]
les
ppPspec Tidy
k (Impt  Symbol
x)
  = Doc
"import" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Symbol
x
ppPspec Tidy
k (DDecl DataDecl
d)
  = forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k DataDecl
d
ppPspec Tidy
k (NTDecl DataDecl
d)
  = Doc
"newtype" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k DataDecl
d
ppPspec Tidy
_ (Incl [Char]
f)
  = Doc
"include" Doc -> Doc -> Doc
<+> Doc
"<" Doc -> Doc -> Doc
PJ.<> [Char] -> Doc
PJ.text [Char]
f Doc -> Doc -> Doc
PJ.<> Doc
">"
ppPspec Tidy
k (Invt t
t)
  = Doc
"invariant" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k t
t
ppPspec Tidy
k (Using (t
t1, t
t2))
  = Doc
"using" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k t
t1 Doc -> Doc -> Doc
<+> Doc
"as" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k t
t2
ppPspec Tidy
k (Alias   (Loc SourcePos
_ SourcePos
_ RTAlias Symbol (RType BTyCon BTyVar RReft)
rta))
  = Doc
"type" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k RTAlias Symbol (RType BTyCon BTyVar RReft)
rta
ppPspec Tidy
k (EAlias  (Loc SourcePos
_ SourcePos
_ RTAlias Symbol Expr
rte))
  = Doc
"predicate" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k RTAlias Symbol Expr
rte
ppPspec Tidy
k (Embed   (LocSymbol
lx, FTycon
tc, TCArgs
NoArgs))
  = Doc
"embed" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (forall a. Located a -> a
val LocSymbol
lx)         Doc -> Doc -> Doc
<+> Doc
"as" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k FTycon
tc
ppPspec Tidy
k (Embed   (LocSymbol
lx, FTycon
tc, TCArgs
WithArgs))
  = Doc
"embed" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (forall a. Located a -> a
val LocSymbol
lx) Doc -> Doc -> Doc
<+> Doc
"*" Doc -> Doc -> Doc
<+> Doc
"as" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k FTycon
tc
ppPspec Tidy
k (Qualif  Qualifier
q)
  = forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Qualifier
q
ppPspec Tidy
k (LVars   LocSymbol
lx)
  = Doc
"lazyvar" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (forall a. Located a -> a
val LocSymbol
lx)
ppPspec Tidy
k (Lazy   LocSymbol
lx)
  = Doc
"lazy" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (forall a. Located a -> a
val LocSymbol
lx)
ppPspec Tidy
k (Rewrite   LocSymbol
lx)
  = Doc
"rewrite" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (forall a. Located a -> a
val LocSymbol
lx)
ppPspec Tidy
k (Rewritewith (LocSymbol
lx, [LocSymbol]
lxs))
  = Doc
"rewriteWith" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (forall a. Located a -> a
val LocSymbol
lx) Doc -> Doc -> Doc
<+> [Doc] -> Doc
PJ.hsep (forall a b. (a -> b) -> [a] -> [b]
map forall {a}. PPrint a => Located a -> Doc
go [LocSymbol]
lxs)
  where
    go :: Located a -> Doc
go Located a
s = forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k forall a b. (a -> b) -> a -> b
$ forall a. Located a -> a
val Located a
s
ppPspec Tidy
k (Fail   LocSymbol
lx)
  = Doc
"fail" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (forall a. Located a -> a
val LocSymbol
lx)
ppPspec Tidy
k (Insts   (LocSymbol
lx, Maybe Int
mbN))
  = Doc
"automatic-instances" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (forall a. Located a -> a
val LocSymbol
lx) Doc -> Doc -> Doc
<+> forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
"" ((Doc
"with" Doc -> Doc -> Doc
<+>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k) Maybe Int
mbN
ppPspec Tidy
k (HMeas   LocSymbol
lx)
  = Doc
"measure" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (forall a. Located a -> a
val LocSymbol
lx)
ppPspec Tidy
k (Reflect LocSymbol
lx)
  = Doc
"reflect" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (forall a. Located a -> a
val LocSymbol
lx)
ppPspec Tidy
k (Inline  LocSymbol
lx)
  = Doc
"inline" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (forall a. Located a -> a
val LocSymbol
lx)
ppPspec Tidy
k (Ignore  LocSymbol
lx)
  = Doc
"ignore" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (forall a. Located a -> a
val LocSymbol
lx)
ppPspec Tidy
k (HBound  LocSymbol
lx)
  = Doc
"bound" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (forall a. Located a -> a
val LocSymbol
lx)
ppPspec Tidy
k (ASize   LocSymbol
lx)
  = Doc
"autosize" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (forall a. Located a -> a
val LocSymbol
lx)
ppPspec Tidy
k (PBound  Bound t Expr
bnd)
  = forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Bound t Expr
bnd
ppPspec Tidy
_ (Pragma  (Loc SourcePos
_ SourcePos
_ [Char]
s))
  = Doc
"LIQUID" Doc -> Doc -> Doc
<+> [Char] -> Doc
PJ.text [Char]
s
ppPspec Tidy
k (CMeas   Measure t ()
m)
  = Doc
"class measure" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Measure t ()
m
ppPspec Tidy
k (IMeas   Measure t c
m)
  = Doc
"instance  measure" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Measure t c
m
ppPspec Tidy
k (Class   RClass t
cls)
  = forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k RClass t
cls
ppPspec Tidy
k (CLaws  RClass t
cls)
  = forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k RClass t
cls
ppPspec Tidy
k (RInst   RInstance t
inst)
  = forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k RInstance t
inst
ppPspec Tidy
k (Varia   (LocSymbol
lx, [Variance]
vs))
  = Doc
"data variance" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (forall a. Located a -> a
val LocSymbol
lx) Doc -> Doc -> Doc
<+> Doc -> [Doc] -> Doc
splice Doc
" " (forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Variance]
vs)
ppPspec Tidy
k (DSize   ([t]
ds, LocSymbol
ss))
  = Doc
"data size" Doc -> Doc -> Doc
<+> Doc -> [Doc] -> Doc
splice Doc
" " (forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [t]
ds) Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (forall a. Located a -> a
val LocSymbol
ss)
ppPspec Tidy
_ (BFix    ()
_)           --
  = Doc
"fixity"
ppPspec Tidy
k (Define  (LocSymbol
lx, Symbol
y))
  = Doc
"define" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (forall a. Located a -> a
val LocSymbol
lx) Doc -> Doc -> Doc
<+> Doc
"=" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Symbol
y
ppPspec Tidy
_ ILaws{}
  = Doc
"TBD-INSTANCE-LAWS"
ppPspec Tidy
k (Relational (LocSymbol
lxl, LocSymbol
lxr, t
tl, t
tr, RelExpr
q, RelExpr
p))
  = Doc
"relational"
        Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (forall a. Located a -> a
val LocSymbol
lxl) Doc -> Doc -> Doc
<+> Doc
"::" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k t
tl Doc -> Doc -> Doc
<+> Doc
"~"
        Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (forall a. Located a -> a
val LocSymbol
lxr) Doc -> Doc -> Doc
<+> Doc
"::" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k t
tr Doc -> Doc -> Doc
<+> Doc
"|"
        Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k RelExpr
q Doc -> Doc -> Doc
<+> Doc
"=>" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k RelExpr
p
ppPspec Tidy
k (AssmRel (LocSymbol
lxl, LocSymbol
lxr, t
tl, t
tr, RelExpr
q, RelExpr
p))
  = Doc
"assume relational"
        Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (forall a. Located a -> a
val LocSymbol
lxl) Doc -> Doc -> Doc
<+> Doc
"::" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k t
tl Doc -> Doc -> Doc
<+> Doc
"~"
        Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (forall a. Located a -> a
val LocSymbol
lxr) Doc -> Doc -> Doc
<+> Doc
"::" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k t
tr Doc -> Doc -> Doc
<+> Doc
"|"
        Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k RelExpr
q Doc -> Doc -> Doc
<+> Doc
"=>" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k RelExpr
p


-- | For debugging
{-instance Show (Pspec a b) where
  show (Meas   _) = "Meas"
  show (Assm   _) = "Assm"
  show (Asrt   _) = "Asrt"
  show (LAsrt  _) = "LAsrt"
  show (Asrts  _) = "Asrts"
  show (Impt   _) = "Impt"
  shcl  _) = "DDecl"
  show (NTDecl _) = "NTDecl"
  show (Incl   _) = "Incl"
  show (Invt   _) = "Invt"
  show (Using _) = "Using"
  show (Alias  _) = "Alias"
  show (EAlias _) = "EAlias"
  show (Embed  _) = "Embed"
  show (Qualif _) = "Qualif"
  show (Decr   _) = "Decr"
  show (LVars  _) = "LVars"
  show (Lazy   _) = "Lazy"
  -- show (Axiom  _) = "Axiom"
  show (Insts  _) = "Insts"
  show (Reflect _) = "Reflect"
  show (HMeas  _) = "HMeas"
  show (HBound _) = "HBound"
  show (Inline _) = "Inline"
  show (Pragma _) = "Pragma"
  show (CMeas  _) = "CMeas"
  show (IMeas  _) = "IMeas"
  show (Class  _) = "Class"
  show (Varia  _) = "Varia"
  show (PBound _) = "Bound"
  show (RInst  _) = "RInst"
  show (ASize  _) = "ASize"
  show (BFix   _) = "BFix"
  show (Define _) = "Define"-}

qualifySpec :: Symbol -> Spec ty bndr -> Spec ty bndr
qualifySpec :: forall ty bndr. Symbol -> Spec ty bndr -> Spec ty bndr
qualifySpec Symbol
name Spec ty bndr
sp = Spec ty bndr
sp { sigs :: [(LocSymbol, ty)]
sigs      = [ (LocSymbol -> LocSymbol
tx LocSymbol
x, ty
t)  | (LocSymbol
x, ty
t)  <- forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
sigs Spec ty bndr
sp]
                         -- , asmSigs   = [ (tx x, t)  | (x, t)  <- asmSigs sp]
                         }
  where
    tx :: Located Symbol -> Located Symbol
    tx :: LocSymbol -> LocSymbol
tx = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Symbol -> Symbol -> Symbol
qualifySymbol Symbol
name)

-- | Turns a list of parsed specifications into a "bare spec".
--
-- This is primarily a rearrangement, as the bare spec is a record containing
-- different kinds of spec directives in different positions, whereas the input
-- list is a mixed list.
--
-- In addition, the sigs of the spec (these are asserted/checked LH type
-- signatues) are being qualified, i.e., the binding occurrences are prefixed
-- with the module name.
--
-- Andres: It is unfortunately totally unclear to me what the justification
-- for the qualification is, and in particular, why it is being done for
-- the asserted signatures only. My trust is not exactly improved by the
-- commented out line in 'qualifySpec'.
--
mkSpec :: ModName -> [BPspec] -> (ModName, Measure.Spec LocBareType LocSymbol)
mkSpec :: ModName -> [BPspec] -> (ModName, BareSpec)
mkSpec ModName
name [BPspec]
xs         = (ModName
name,) forall a b. (a -> b) -> a -> b
$ forall ty bndr. Symbol -> Spec ty bndr -> Spec ty bndr
qualifySpec (forall a. Symbolic a => a -> Symbol
symbol ModName
name) Measure.Spec
  { measures :: [Measure (Located (RType BTyCon BTyVar RReft)) LocSymbol]
Measure.measures   = [Measure (Located (RType BTyCon BTyVar RReft)) LocSymbol
m | Meas   Measure (Located (RType BTyCon BTyVar RReft)) LocSymbol
m <- [BPspec]
xs]
  , asmSigs :: [(LocSymbol, Located (RType BTyCon BTyVar RReft))]
Measure.asmSigs    = [(LocSymbol, Located (RType BTyCon BTyVar RReft))
a | Assm   (LocSymbol, Located (RType BTyCon BTyVar RReft))
a <- [BPspec]
xs]
  , sigs :: [(LocSymbol, Located (RType BTyCon BTyVar RReft))]
Measure.sigs       = [(LocSymbol, Located (RType BTyCon BTyVar RReft))
a | Asrt   (LocSymbol, Located (RType BTyCon BTyVar RReft))
a <- [BPspec]
xs]
                      forall a. [a] -> [a] -> [a]
++ [(LocSymbol
y, Located (RType BTyCon BTyVar RReft)
t) | Asrts ([LocSymbol]
ys, (Located (RType BTyCon BTyVar RReft)
t, Maybe [Located Expr]
_)) <- [BPspec]
xs, LocSymbol
y <- [LocSymbol]
ys]
  , localSigs :: [(LocSymbol, Located (RType BTyCon BTyVar RReft))]
Measure.localSigs  = []
  , reflSigs :: [(LocSymbol, Located (RType BTyCon BTyVar RReft))]
Measure.reflSigs   = []
  , impSigs :: [(Symbol, Sort)]
Measure.impSigs    = []
  , expSigs :: [(Symbol, Sort)]
Measure.expSigs    = []
  , invariants :: [(Maybe LocSymbol, Located (RType BTyCon BTyVar RReft))]
Measure.invariants = [(forall a. Maybe a
Nothing, Located (RType BTyCon BTyVar RReft)
t) | Invt   Located (RType BTyCon BTyVar RReft)
t <- [BPspec]
xs]
  , ialiases :: [(Located (RType BTyCon BTyVar RReft),
  Located (RType BTyCon BTyVar RReft))]
Measure.ialiases   = [(Located (RType BTyCon BTyVar RReft),
 Located (RType BTyCon BTyVar RReft))
t | Using (Located (RType BTyCon BTyVar RReft),
 Located (RType BTyCon BTyVar RReft))
t <- [BPspec]
xs]
  , imports :: [Symbol]
Measure.imports    = [Symbol
i | Impt   Symbol
i <- [BPspec]
xs]
  , dataDecls :: [DataDecl]
Measure.dataDecls  = [DataDecl
d | DDecl  DataDecl
d <- [BPspec]
xs] forall a. [a] -> [a] -> [a]
++ [DataDecl
d | NTDecl DataDecl
d <- [BPspec]
xs]
  , newtyDecls :: [DataDecl]
Measure.newtyDecls = [DataDecl
d | NTDecl DataDecl
d <- [BPspec]
xs]
  , includes :: [[Char]]
Measure.includes   = [[Char]
q | Incl   [Char]
q <- [BPspec]
xs]
  , aliases :: [Located (RTAlias Symbol (RType BTyCon BTyVar RReft))]
Measure.aliases    = [Located (RTAlias Symbol (RType BTyCon BTyVar RReft))
a | Alias  Located (RTAlias Symbol (RType BTyCon BTyVar RReft))
a <- [BPspec]
xs]
  , ealiases :: [Located (RTAlias Symbol Expr)]
Measure.ealiases   = [Located (RTAlias Symbol Expr)
e | EAlias Located (RTAlias Symbol Expr)
e <- [BPspec]
xs]
  , embeds :: TCEmb LocSymbol
Measure.embeds     = forall a. (Eq a, Hashable a) => [(a, (Sort, TCArgs))] -> TCEmb a
tceFromList [(LocSymbol
c, (FTycon -> Sort
fTyconSort FTycon
tc, TCArgs
a)) | Embed (LocSymbol
c, FTycon
tc, TCArgs
a) <- [BPspec]
xs]
  , qualifiers :: [Qualifier]
Measure.qualifiers = [Qualifier
q | Qualif Qualifier
q <- [BPspec]
xs]
  , lvars :: HashSet LocSymbol
Measure.lvars      = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [LocSymbol
d | LVars LocSymbol
d  <- [BPspec]
xs]
  , autois :: HashMap LocSymbol (Maybe Int)
Measure.autois     = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(LocSymbol, Maybe Int)
s | Insts (LocSymbol, Maybe Int)
s <- [BPspec]
xs]
  , pragmas :: [Located [Char]]
Measure.pragmas    = [Located [Char]
s | Pragma Located [Char]
s <- [BPspec]
xs]
  , cmeasures :: [Measure (Located (RType BTyCon BTyVar RReft)) ()]
Measure.cmeasures  = [Measure (Located (RType BTyCon BTyVar RReft)) ()
m | CMeas  Measure (Located (RType BTyCon BTyVar RReft)) ()
m <- [BPspec]
xs]
  , imeasures :: [Measure (Located (RType BTyCon BTyVar RReft)) LocSymbol]
Measure.imeasures  = [Measure (Located (RType BTyCon BTyVar RReft)) LocSymbol
m | IMeas  Measure (Located (RType BTyCon BTyVar RReft)) LocSymbol
m <- [BPspec]
xs]
  , classes :: [RClass (Located (RType BTyCon BTyVar RReft))]
Measure.classes    = [RClass (Located (RType BTyCon BTyVar RReft))
c | Class  RClass (Located (RType BTyCon BTyVar RReft))
c <- [BPspec]
xs]
  , relational :: [(LocSymbol, LocSymbol, Located (RType BTyCon BTyVar RReft),
  Located (RType BTyCon BTyVar RReft), RelExpr, RelExpr)]
Measure.relational = [(LocSymbol, LocSymbol, Located (RType BTyCon BTyVar RReft),
 Located (RType BTyCon BTyVar RReft), RelExpr, RelExpr)
r | Relational (LocSymbol, LocSymbol, Located (RType BTyCon BTyVar RReft),
 Located (RType BTyCon BTyVar RReft), RelExpr, RelExpr)
r <- [BPspec]
xs]
  , asmRel :: [(LocSymbol, LocSymbol, Located (RType BTyCon BTyVar RReft),
  Located (RType BTyCon BTyVar RReft), RelExpr, RelExpr)]
Measure.asmRel     = [(LocSymbol, LocSymbol, Located (RType BTyCon BTyVar RReft),
 Located (RType BTyCon BTyVar RReft), RelExpr, RelExpr)
r | AssmRel (LocSymbol, LocSymbol, Located (RType BTyCon BTyVar RReft),
 Located (RType BTyCon BTyVar RReft), RelExpr, RelExpr)
r <- [BPspec]
xs]
  , claws :: [RClass (Located (RType BTyCon BTyVar RReft))]
Measure.claws      = [RClass (Located (RType BTyCon BTyVar RReft))
c | CLaws  RClass (Located (RType BTyCon BTyVar RReft))
c <- [BPspec]
xs]
  , dvariance :: [(LocSymbol, [Variance])]
Measure.dvariance  = [(LocSymbol, [Variance])
v | Varia  (LocSymbol, [Variance])
v <- [BPspec]
xs]
  , dsize :: [([Located (RType BTyCon BTyVar RReft)], LocSymbol)]
Measure.dsize      = [([Located (RType BTyCon BTyVar RReft)], LocSymbol)
v | DSize  ([Located (RType BTyCon BTyVar RReft)], LocSymbol)
v <- [BPspec]
xs]
  , rinstance :: [RInstance (Located (RType BTyCon BTyVar RReft))]
Measure.rinstance  = [RInstance (Located (RType BTyCon BTyVar RReft))
i | RInst  RInstance (Located (RType BTyCon BTyVar RReft))
i <- [BPspec]
xs]
  , ilaws :: [RILaws (Located (RType BTyCon BTyVar RReft))]
Measure.ilaws      = [RILaws (Located (RType BTyCon BTyVar RReft))
i | ILaws  RILaws (Located (RType BTyCon BTyVar RReft))
i <- [BPspec]
xs]
  , termexprs :: [(LocSymbol, [Located Expr])]
Measure.termexprs  = [(LocSymbol
y, [Located Expr]
es) | Asrts ([LocSymbol]
ys, (Located (RType BTyCon BTyVar RReft)
_, Just [Located Expr]
es)) <- [BPspec]
xs, LocSymbol
y <- [LocSymbol]
ys]
  , lazy :: HashSet LocSymbol
Measure.lazy       = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [LocSymbol
s | Lazy   LocSymbol
s <- [BPspec]
xs]
  , fails :: HashSet LocSymbol
Measure.fails      = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [LocSymbol
s | Fail   LocSymbol
s <- [BPspec]
xs]
  , rewrites :: HashSet LocSymbol
Measure.rewrites   = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [LocSymbol
s | Rewrite LocSymbol
s <- [BPspec]
xs]
  , rewriteWith :: HashMap LocSymbol [LocSymbol]
Measure.rewriteWith = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(LocSymbol, [LocSymbol])
s | Rewritewith (LocSymbol, [LocSymbol])
s <- [BPspec]
xs]
  , bounds :: RRBEnv (Located (RType BTyCon BTyVar RReft))
Measure.bounds     = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(forall t e. Bound t e -> LocSymbol
bname Bound (Located (RType BTyCon BTyVar RReft)) Expr
i, Bound (Located (RType BTyCon BTyVar RReft)) Expr
i) | PBound Bound (Located (RType BTyCon BTyVar RReft)) Expr
i <- [BPspec]
xs]
  , reflects :: HashSet LocSymbol
Measure.reflects   = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [LocSymbol
s | Reflect LocSymbol
s <- [BPspec]
xs]
  , hmeas :: HashSet LocSymbol
Measure.hmeas      = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [LocSymbol
s | HMeas  LocSymbol
s <- [BPspec]
xs]
  , inlines :: HashSet LocSymbol
Measure.inlines    = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [LocSymbol
s | Inline LocSymbol
s <- [BPspec]
xs]
  , ignores :: HashSet LocSymbol
Measure.ignores    = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [LocSymbol
s | Ignore LocSymbol
s <- [BPspec]
xs]
  , autosize :: HashSet LocSymbol
Measure.autosize   = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [LocSymbol
s | ASize  LocSymbol
s <- [BPspec]
xs]
  , hbounds :: HashSet LocSymbol
Measure.hbounds    = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [LocSymbol
s | HBound LocSymbol
s <- [BPspec]
xs]
  , defs :: HashMap LocSymbol Symbol
Measure.defs       = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(LocSymbol, Symbol)
d | Define (LocSymbol, Symbol)
d <- [BPspec]
xs]
  , axeqs :: [Equation]
Measure.axeqs      = []
  }

-- | Parse a single top level liquid specification
specP :: Parser BPspec
specP :: Parser BPspec
specP
  =     [Char] -> Parser BPspec -> Parser BPspec
fallbackSpecP [Char]
"assume"
    (([Char] -> Parser ()
reserved [Char]
"relational" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall ty ctor.
(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr) -> Pspec ty ctor
AssmRel Parser
  (LocSymbol, LocSymbol, Located (RType BTyCon BTyVar RReft),
   Located (RType BTyCon BTyVar RReft), RelExpr, RelExpr)
relationalP)
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>                           forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall ty ctor. (LocSymbol, ty) -> Pspec ty ctor
Assm   Parser (LocSymbol, Located (RType BTyCon BTyVar RReft))
tyBindP  )
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> Parser BPspec -> Parser BPspec
fallbackSpecP [Char]
"assert"      (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall ty ctor. (LocSymbol, ty) -> Pspec ty ctor
Asrt    Parser (LocSymbol, Located (RType BTyCon BTyVar RReft))
tyBindP  )
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> Parser BPspec -> Parser BPspec
fallbackSpecP [Char]
"autosize"    (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall ty ctor. LocSymbol -> Pspec ty ctor
ASize   Parser LocSymbol
asizeP   )
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved [Char]
"local"         forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall ty ctor. (LocSymbol, ty) -> Pspec ty ctor
LAsrt   Parser (LocSymbol, Located (RType BTyCon BTyVar RReft))
tyBindP  )

    -- TODO: These next two are synonyms, kill one
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> Parser BPspec -> Parser BPspec
fallbackSpecP [Char]
"axiomatize"  (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall ty ctor. LocSymbol -> Pspec ty ctor
Reflect Parser LocSymbol
axiomP   )
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> Parser BPspec -> Parser BPspec
fallbackSpecP [Char]
"reflect"     (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall ty ctor. LocSymbol -> Pspec ty ctor
Reflect Parser LocSymbol
axiomP   )

    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> Parser BPspec -> Parser BPspec
fallbackSpecP [Char]
"measure"    Parser BPspec
hmeasureP

    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> Parser BPspec -> Parser BPspec
fallbackSpecP [Char]
"define"      (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall ty ctor. (LocSymbol, Symbol) -> Pspec ty ctor
Define  Parser (LocSymbol, Symbol)
defineP  )
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved [Char]
"infixl"        forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall ty ctor. () -> Pspec ty ctor
BFix    Parser ()
infixlP  )
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved [Char]
"infixr"        forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall ty ctor. () -> Pspec ty ctor
BFix    Parser ()
infixrP  )
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved [Char]
"infix"         forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall ty ctor. () -> Pspec ty ctor
BFix    Parser ()
infixP   )
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> Parser BPspec -> Parser BPspec
fallbackSpecP [Char]
"inline"      (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall ty ctor. LocSymbol -> Pspec ty ctor
Inline  Parser LocSymbol
inlineP  )
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> Parser BPspec -> Parser BPspec
fallbackSpecP [Char]
"ignore"      (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall ty ctor. LocSymbol -> Pspec ty ctor
Ignore  Parser LocSymbol
inlineP  )

    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> Parser BPspec -> Parser BPspec
fallbackSpecP [Char]
"bound"       (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall ty ctor. Bound ty Expr -> Pspec ty ctor
PBound  Parser (Bound (Located (RType BTyCon BTyVar RReft)) Expr)
boundP
                                 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall ty ctor. LocSymbol -> Pspec ty ctor
HBound  Parser LocSymbol
hboundP  )
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved [Char]
"class"
         forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (([Char] -> Parser ()
reserved [Char]
"measure"  forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall ty ctor. Measure ty () -> Pspec ty ctor
CMeas  Parser (Measure (Located (RType BTyCon BTyVar RReft)) ())
cMeasureP )
         forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved [Char]
"laws"     forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall ty ctor. RClass ty -> Pspec ty ctor
CLaws  Parser (RClass (Located (RType BTyCon BTyVar RReft)))
classP)
         forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall ty ctor. RClass ty -> Pspec ty ctor
Class  Parser (RClass (Located (RType BTyCon BTyVar RReft)))
classP                            ))
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved [Char]
"instance"
         forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (([Char] -> Parser ()
reserved [Char]
"measure"  forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall ty ctor. Measure ty ctor -> Pspec ty ctor
IMeas  Parser (Measure (Located (RType BTyCon BTyVar RReft)) LocSymbol)
iMeasureP )
         forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved [Char]
"laws"     forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall ty ctor. RILaws ty -> Pspec ty ctor
ILaws Parser (RILaws (Located (RType BTyCon BTyVar RReft)))
instanceLawP)
         forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall ty ctor. RInstance ty -> Pspec ty ctor
RInst  Parser (RInstance (Located (RType BTyCon BTyVar RReft)))
instanceP ))

    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved [Char]
"import"        forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall ty ctor. Symbol -> Pspec ty ctor
Impt   Parser Symbol
symbolP   )

    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved [Char]
"data"
        forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (([Char] -> Parser ()
reserved [Char]
"variance"  forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall ty ctor. (LocSymbol, [Variance]) -> Pspec ty ctor
Varia  Parser (LocSymbol, [Variance])
datavarianceP)
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved [Char]
"size"      forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall ty ctor. ([ty], LocSymbol) -> Pspec ty ctor
DSize  Parser ([Located (RType BTyCon BTyVar RReft)], LocSymbol)
dsizeP)
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall ty ctor. DataDecl -> Pspec ty ctor
DDecl  Parser DataDecl
dataDeclP ))
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved [Char]
"newtype"       forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall ty ctor. DataDecl -> Pspec ty ctor
NTDecl Parser DataDecl
dataDeclP )
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved [Char]
"relational"    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall ty ctor.
(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr) -> Pspec ty ctor
Relational Parser
  (LocSymbol, LocSymbol, Located (RType BTyCon BTyVar RReft),
   Located (RType BTyCon BTyVar RReft), RelExpr, RelExpr)
relationalP )
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved [Char]
"include"       forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall ty ctor. [Char] -> Pspec ty ctor
Incl   Parser [Char]
filePathP )
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> Parser BPspec -> Parser BPspec
fallbackSpecP [Char]
"invariant"   (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall ty ctor. ty -> Pspec ty ctor
Invt   Parser (Located (RType BTyCon BTyVar RReft))
invariantP)
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved [Char]
"using"          forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall ty ctor. (ty, ty) -> Pspec ty ctor
Using Parser
  (Located (RType BTyCon BTyVar RReft),
   Located (RType BTyCon BTyVar RReft))
invaliasP )
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved [Char]
"type"          forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall ty ctor.
Located (RTAlias Symbol (RType BTyCon BTyVar RReft))
-> Pspec ty ctor
Alias  Parser (Located (RTAlias Symbol (RType BTyCon BTyVar RReft)))
aliasP    )

    -- TODO: Next two are basically synonyms
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> Parser BPspec -> Parser BPspec
fallbackSpecP [Char]
"predicate"   (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall ty ctor. Located (RTAlias Symbol Expr) -> Pspec ty ctor
EAlias Parser (Located (RTAlias Symbol Expr))
ealiasP   )
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> Parser BPspec -> Parser BPspec
fallbackSpecP [Char]
"expression"  (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall ty ctor. Located (RTAlias Symbol Expr) -> Pspec ty ctor
EAlias Parser (Located (RTAlias Symbol Expr))
ealiasP   )

    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> Parser BPspec -> Parser BPspec
fallbackSpecP [Char]
"embed"       (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall ty ctor. (LocSymbol, FTycon, TCArgs) -> Pspec ty ctor
Embed  Parser (LocSymbol, FTycon, TCArgs)
embedP    )
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> Parser BPspec -> Parser BPspec
fallbackSpecP [Char]
"qualif"      (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall ty ctor. Qualifier -> Pspec ty ctor
Qualif (Parser Sort -> Parser Qualifier
qualifierP Parser Sort
sortP))
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved [Char]
"lazyvar"       forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall ty ctor. LocSymbol -> Pspec ty ctor
LVars  Parser LocSymbol
lazyVarP  )

    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved [Char]
"lazy"          forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall ty ctor. LocSymbol -> Pspec ty ctor
Lazy   Parser LocSymbol
lazyVarP  )
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved [Char]
"rewrite"       forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall ty ctor. LocSymbol -> Pspec ty ctor
Rewrite   Parser LocSymbol
rewriteVarP )
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved [Char]
"rewriteWith"   forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall ty ctor. (LocSymbol, [LocSymbol]) -> Pspec ty ctor
Rewritewith   Parser (LocSymbol, [LocSymbol])
rewriteWithP )
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved [Char]
"fail"          forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall ty ctor. LocSymbol -> Pspec ty ctor
Fail   Parser LocSymbol
failVarP  )
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved [Char]
"ple"           forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall ty ctor. (LocSymbol, Maybe Int) -> Pspec ty ctor
Insts Parser (LocSymbol, Maybe Int)
autoinstP  )
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved [Char]
"automatic-instances" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall ty ctor. (LocSymbol, Maybe Int) -> Pspec ty ctor
Insts Parser (LocSymbol, Maybe Int)
autoinstP  )
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved [Char]
"LIQUID"        forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall ty ctor. Located [Char] -> Pspec ty ctor
Pragma Parser (Located [Char])
pragmaP   )
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved [Char]
"liquid"        forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall ty ctor. Located [Char] -> Pspec ty ctor
Pragma Parser (Located [Char])
pragmaP   )
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> {- DEFAULT -}                forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall ty ctor.
([LocSymbol], (ty, Maybe [Located Expr])) -> Pspec ty ctor
Asrts  Parser
  ([LocSymbol],
   (Located (RType BTyCon BTyVar RReft), Maybe [Located Expr]))
tyBindsP
    forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"specP"

-- | Try the given parser on the tail after matching the reserved word, and if
-- it fails fall back to parsing it as a haskell signature for a function with
-- the same name.
fallbackSpecP :: String -> Parser BPspec -> Parser BPspec
fallbackSpecP :: [Char] -> Parser BPspec -> Parser BPspec
fallbackSpecP [Char]
kw Parser BPspec
p = do
  (Loc SourcePos
l1 SourcePos
l2 [Char]
_) <- [Char] -> Parser (Located [Char])
locReserved [Char]
kw
  Parser BPspec
p forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall ty ctor.
([LocSymbol], (ty, Maybe [Located Expr])) -> Pspec ty ctor
Asrts (LocSymbol
-> Parser
     ([LocSymbol],
      (Located (RType BTyCon BTyVar RReft), Maybe [Located Expr]))
tyBindsRemP (forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l1 SourcePos
l2 (forall a. Symbolic a => a -> Symbol
symbol [Char]
kw)) )

-- | Same as tyBindsP, except the single initial symbol has already been matched
tyBindsRemP :: LocSymbol -> Parser ([LocSymbol], (Located BareType, Maybe [Located Expr]))
tyBindsRemP :: LocSymbol
-> Parser
     ([LocSymbol],
      (Located (RType BTyCon BTyVar RReft), Maybe [Located Expr]))
tyBindsRemP LocSymbol
sym = do
  [Char] -> Parser ()
reservedOp [Char]
"::"
  (Located (RType BTyCon BTyVar RReft), Maybe [Located Expr])
tb <- Parser (Located (RType BTyCon BTyVar RReft), Maybe [Located Expr])
termBareTypeP
  forall (m :: * -> *) a. Monad m => a -> m a
return ([LocSymbol
sym],(Located (RType BTyCon BTyVar RReft), Maybe [Located Expr])
tb)

pragmaP :: Parser (Located String)
pragmaP :: Parser (Located [Char])
pragmaP = Parser (Located [Char])
locStringLiteral

autoinstP :: Parser (LocSymbol, Maybe Int)
autoinstP :: Parser (LocSymbol, Maybe Int)
autoinstP = do LocSymbol
x <- Parser LocSymbol
locBinderP
               Maybe Integer
i <- forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional ([Char] -> Parser ()
reserved [Char]
"with" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Integer
natural)
               forall (m :: * -> *) a. Monad m => a -> m a
return (LocSymbol
x, forall a b. (Integral a, Num b) => a -> b
fromIntegral forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Integer
i)

lazyVarP :: Parser LocSymbol
lazyVarP :: Parser LocSymbol
lazyVarP = Parser LocSymbol
locBinderP


rewriteVarP :: Parser LocSymbol
rewriteVarP :: Parser LocSymbol
rewriteVarP = Parser LocSymbol
locBinderP

rewriteWithP :: Parser (LocSymbol, [LocSymbol])
rewriteWithP :: Parser (LocSymbol, [LocSymbol])
rewriteWithP = (,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser LocSymbol
locBinderP forall (f :: * -> *) a b. Applicative f => 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]
sepBy1 Parser LocSymbol
locBinderP Parser [Char]
comma)

failVarP :: Parser LocSymbol
failVarP :: Parser LocSymbol
failVarP = Parser LocSymbol
locBinderP

axiomP :: Parser LocSymbol
axiomP :: Parser LocSymbol
axiomP = Parser LocSymbol
locBinderP

hboundP :: Parser LocSymbol
hboundP :: Parser LocSymbol
hboundP = Parser LocSymbol
locBinderP

inlineP :: Parser LocSymbol
inlineP :: Parser LocSymbol
inlineP = Parser LocSymbol
locBinderP

asizeP :: Parser LocSymbol
asizeP :: Parser LocSymbol
asizeP = Parser LocSymbol
locBinderP

filePathP     :: Parser FilePath
filePathP :: Parser [Char]
filePathP     = forall a. Parser a -> Parser a
angles forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some Parser Char
pathCharP
  where
    pathCharP :: Parser Char
    pathCharP :: Parser Char
pathCharP = forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
choice forall a b. (a -> b) -> a -> b
$ forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Char]
pathChars

    pathChars :: [Char]
    pathChars :: [Char]
pathChars = [Char
'a'..Char
'z'] forall a. [a] -> [a] -> [a]
++ [Char
'A'..Char
'Z'] forall a. [a] -> [a] -> [a]
++ [Char
'0'..Char
'9'] forall a. [a] -> [a] -> [a]
++ [Char
'.', Char
'/']

datavarianceP :: Parser (Located Symbol, [Variance])
datavarianceP :: Parser (LocSymbol, [Variance])
datavarianceP = forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (,) Parser LocSymbol
locUpperIdP (forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many Parser Variance
varianceP)

dsizeP :: Parser ([Located BareType], Located Symbol)
dsizeP :: Parser ([Located (RType BTyCon BTyVar RReft)], LocSymbol)
dsizeP = forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (,) (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 (Located a)
located StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
genBareTypeP) Parser [Char]
comma) Parser LocSymbol
locBinderP


varianceP :: Parser Variance
varianceP :: Parser Variance
varianceP = ([Char] -> Parser ()
reserved [Char]
"bivariant"     forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return Variance
Bivariant)
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved [Char]
"invariant"     forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return Variance
Invariant)
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved [Char]
"covariant"     forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return Variance
Covariant)
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved [Char]
"contravariant" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return Variance
Contravariant)
        forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"Invalid variance annotation\t Use one of bivariant, invariant, covariant, contravariant"

tyBindsP :: Parser ([LocSymbol], (Located BareType, Maybe [Located Expr]))
tyBindsP :: Parser
  ([LocSymbol],
   (Located (RType BTyCon BTyVar RReft), Maybe [Located Expr]))
tyBindsP =
  forall x a y. Parser x -> Parser a -> Parser y -> Parser (x, y)
xyP (forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy1 Parser LocSymbol
locBinderP Parser [Char]
comma) ([Char] -> Parser ()
reservedOp [Char]
"::") Parser (Located (RType BTyCon BTyVar RReft), Maybe [Located Expr])
termBareTypeP

tyBindNoLocP :: Parser (LocSymbol, BareType)
tyBindNoLocP :: Parser (LocSymbol, RType BTyCon BTyVar RReft)
tyBindNoLocP = forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second forall a. Located a -> a
val forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser (LocSymbol, Located (RType BTyCon BTyVar RReft))
tyBindP

-- | Parses a type signature as it occurs in "assume" and "assert" directives.
tyBindP :: Parser (LocSymbol, Located BareType)
tyBindP :: Parser (LocSymbol, Located (RType BTyCon BTyVar RReft))
tyBindP =
  (,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser LocSymbol
locBinderP forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* [Char] -> Parser ()
reservedOp [Char]
"::" forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Parser a -> Parser (Located a)
located StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
genBareTypeP

termBareTypeP :: Parser (Located BareType, Maybe [Located Expr])
termBareTypeP :: Parser (Located (RType BTyCon BTyVar RReft), Maybe [Located Expr])
termBareTypeP = do
  Located (RType BTyCon BTyVar RReft)
t <- forall a. Parser a -> Parser (Located a)
located StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
genBareTypeP
  Located (RType BTyCon BTyVar RReft)
-> Parser
     (Located (RType BTyCon BTyVar RReft), Maybe [Located Expr])
termTypeP Located (RType BTyCon BTyVar RReft)
t forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *) a. Monad m => a -> m a
return (Located (RType BTyCon BTyVar RReft)
t, forall a. Maybe a
Nothing)

termTypeP :: Located BareType ->Parser (Located BareType, Maybe [Located Expr])
termTypeP :: Located (RType BTyCon BTyVar RReft)
-> Parser
     (Located (RType BTyCon BTyVar RReft), Maybe [Located Expr])
termTypeP Located (RType BTyCon BTyVar RReft)
t
  = do
       [Char] -> Parser ()
reservedOp [Char]
"/"
       [Located Expr]
es <- 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. Parser a -> Parser (Located a)
located StateT PState (Parsec Void [Char]) Expr
exprP) Parser [Char]
comma
       forall (m :: * -> *) a. Monad m => a -> m a
return (Located (RType BTyCon BTyVar RReft)
t, forall a. a -> Maybe a
Just [Located Expr]
es)

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

invariantP :: Parser (Located BareType)
invariantP :: Parser (Located (RType BTyCon BTyVar RReft))
invariantP = forall a. Parser a -> Parser (Located a)
located StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
genBareTypeP

invaliasP :: Parser (Located BareType, Located BareType)
invaliasP :: Parser
  (Located (RType BTyCon BTyVar RReft),
   Located (RType BTyCon BTyVar RReft))
invaliasP
  = do Located (RType BTyCon BTyVar RReft)
t  <- forall a. Parser a -> Parser (Located a)
located StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
genBareTypeP
       [Char] -> Parser ()
reserved [Char]
"as"
       Located (RType BTyCon BTyVar RReft)
ta <- forall a. Parser a -> Parser (Located a)
located StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
genBareTypeP
       forall (m :: * -> *) a. Monad m => a -> m a
return (Located (RType BTyCon BTyVar RReft)
t, Located (RType BTyCon BTyVar RReft)
ta)

genBareTypeP :: Parser BareType
genBareTypeP :: StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
genBareTypeP = StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
bareTypeP

embedP :: Parser (Located Symbol, FTycon, TCArgs)
embedP :: Parser (LocSymbol, FTycon, TCArgs)
embedP = do
  LocSymbol
x <- Parser LocSymbol
locUpperIdP
  TCArgs
a <- forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try ([Char] -> Parser ()
reserved [Char]
"*" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return TCArgs
WithArgs) forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *) a. Monad m => a -> m a
return TCArgs
NoArgs -- TODO: reserved "*" looks suspicious
  ()
_ <- [Char] -> Parser ()
reserved [Char]
"as"
  FTycon
t <- Parser FTycon
fTyConP
  forall (m :: * -> *) a. Monad m => a -> m a
return (LocSymbol
x, FTycon
t, TCArgs
a)
  --  = xyP locUpperIdP symbolTCArgs (reserved "as") fTyConP


aliasP :: Parser (Located (RTAlias Symbol BareType))
aliasP :: Parser (Located (RTAlias Symbol (RType BTyCon BTyVar RReft)))
aliasP  = forall tv ty.
(Symbol -> tv) -> Parser ty -> Parser (Located (RTAlias tv ty))
rtAliasP forall a. a -> a
id     StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
bareTypeP forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"aliasP"

ealiasP :: Parser (Located (RTAlias Symbol Expr))
ealiasP :: Parser (Located (RTAlias Symbol Expr))
ealiasP = forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (forall tv ty.
(Symbol -> tv) -> Parser ty -> Parser (Located (RTAlias tv ty))
rtAliasP forall a. Symbolic a => a -> Symbol
symbol StateT PState (Parsec Void [Char]) Expr
predP)
      forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall tv ty.
(Symbol -> tv) -> Parser ty -> Parser (Located (RTAlias tv ty))
rtAliasP forall a. Symbolic a => a -> Symbol
symbol StateT PState (Parsec Void [Char]) Expr
exprP
      forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"ealiasP"

-- | Parser for a LH type synonym.
rtAliasP :: (Symbol -> tv) -> Parser ty -> Parser (Located (RTAlias tv ty))
rtAliasP :: forall tv ty.
(Symbol -> tv) -> Parser ty -> Parser (Located (RTAlias tv ty))
rtAliasP Symbol -> tv
f Parser ty
bodyP
  = do SourcePos
pos  <- forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
getSourcePos
       Symbol
name <- Parser Symbol
upperIdP
       [Symbol]
args <- forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many Parser Symbol
aliasIdP
       [Char] -> Parser ()
reservedOp [Char]
"="
       ty
body <- Parser ty
bodyP
       SourcePos
posE <- forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
getSourcePos
       let ([Symbol]
tArgs, [Symbol]
vArgs) = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Char -> Bool
isSmall forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Char
headSym) [Symbol]
args
       forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
pos SourcePos
posE (forall x a. Symbol -> [x] -> [Symbol] -> a -> RTAlias x a
RTA Symbol
name (Symbol -> tv
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
tArgs) [Symbol]
vArgs ty
body)

hmeasureP :: Parser BPspec
hmeasureP :: Parser BPspec
hmeasureP = do
  Parser ()
setLayout
  LocSymbol
b <- Parser LocSymbol
locBinderP
  (do [Char] -> Parser ()
reservedOp [Char]
"::"
      Located (RType BTyCon BTyVar RReft)
ty <- forall a. Parser a -> Parser (Located a)
located StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
genBareTypeP
      Parser ()
popLayout forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
popLayout
      [Def (Located (RType BTyCon BTyVar RReft)) LocSymbol]
eqns <- forall a. Parser a -> Parser [a]
block forall a b. (a -> b) -> a -> b
$ forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try forall a b. (a -> b) -> a -> b
$ Parser Body
-> StateT
     PState
     (Parsec Void [Char])
     (Def (Located (RType BTyCon BTyVar RReft)) LocSymbol)
measureDefP (Parser Body
rawBodyP forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Located (RType BTyCon BTyVar RReft) -> Parser Body
tyBodyP Located (RType BTyCon BTyVar RReft)
ty)
      forall (m :: * -> *) a. Monad m => a -> m a
return (forall ty ctor. Measure ty ctor -> Pspec ty ctor
Meas forall a b. (a -> b) -> a -> b
$ forall ty bndr.
LocSymbol
-> ty
-> [Def ty bndr]
-> MeasureKind
-> UnSortedExprs
-> Measure ty bndr
Measure.mkM LocSymbol
b Located (RType BTyCon BTyVar RReft)
ty [Def (Located (RType BTyCon BTyVar RReft)) LocSymbol]
eqns MeasureKind
MsMeasure forall a. Monoid a => a
mempty))
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Parser ()
popLayout forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
popLayout forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return (forall ty ctor. LocSymbol -> Pspec ty ctor
HMeas LocSymbol
b))

measureP :: Parser (Measure (Located BareType) LocSymbol)
measureP :: Parser (Measure (Located (RType BTyCon BTyVar RReft)) LocSymbol)
measureP = do
  (LocSymbol
x, Located (RType BTyCon BTyVar RReft)
ty) <- forall a. Parser a -> Parser a
indentedLine Parser (LocSymbol, Located (RType BTyCon BTyVar RReft))
tyBindP
  Maybe [Char]
_ <- forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional Parser [Char]
semi
  [Def (Located (RType BTyCon BTyVar RReft)) LocSymbol]
eqns    <- forall a. Parser a -> Parser [a]
block forall a b. (a -> b) -> a -> b
$ Parser Body
-> StateT
     PState
     (Parsec Void [Char])
     (Def (Located (RType BTyCon BTyVar RReft)) LocSymbol)
measureDefP (Parser Body
rawBodyP forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Located (RType BTyCon BTyVar RReft) -> Parser Body
tyBodyP Located (RType BTyCon BTyVar RReft)
ty)
  forall (m :: * -> *) a. Monad m => a -> m a
return   forall a b. (a -> b) -> a -> b
$ forall ty bndr.
LocSymbol
-> ty
-> [Def ty bndr]
-> MeasureKind
-> UnSortedExprs
-> Measure ty bndr
Measure.mkM LocSymbol
x Located (RType BTyCon BTyVar RReft)
ty [Def (Located (RType BTyCon BTyVar RReft)) LocSymbol]
eqns MeasureKind
MsMeasure forall a. Monoid a => a
mempty

-- | class measure
cMeasureP :: Parser (Measure (Located BareType) ())
cMeasureP :: Parser (Measure (Located (RType BTyCon BTyVar RReft)) ())
cMeasureP
  = do (LocSymbol
x, Located (RType BTyCon BTyVar RReft)
ty) <- Parser (LocSymbol, Located (RType BTyCon BTyVar RReft))
tyBindP
       forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty bndr.
LocSymbol
-> ty
-> [Def ty bndr]
-> MeasureKind
-> UnSortedExprs
-> Measure ty bndr
Measure.mkM LocSymbol
x Located (RType BTyCon BTyVar RReft)
ty [] MeasureKind
MsClass forall a. Monoid a => a
mempty

iMeasureP :: Parser (Measure (Located BareType) LocSymbol)
iMeasureP :: Parser (Measure (Located (RType BTyCon BTyVar RReft)) LocSymbol)
iMeasureP = Parser (Measure (Located (RType BTyCon BTyVar RReft)) LocSymbol)
measureP


oneClassArg :: Parser [Located BareType]
oneClassArg :: Parser [Located (RType BTyCon BTyVar RReft)]
oneClassArg
  = forall {a}. a -> [a]
sing forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Parser a -> Parser (Located a)
located (forall {r} {c} {tv}. Monoid r => c -> [tv] -> RType c tv r
rit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser BTyCon
classBTyConP forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall a b. (a -> b) -> [a] -> [b]
map forall a. Located a -> a
val forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void [Char]) [Located BTyVar]
classParams))
  where
    rit :: c -> [tv] -> RType c tv r
rit c
t [tv]
as    = forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp c
t ((forall c tv r. tv -> r -> RType c tv r
`RVar` forall a. Monoid a => a
mempty) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [tv]
as) [] forall a. Monoid a => a
mempty
    classParams :: StateT PState (Parsec Void [Char]) [Located BTyVar]
classParams =  ([Char] -> Parser ()
reserved [Char]
"where" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return [])
               forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ((:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Symbol -> BTyVar
bTyVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser LocSymbol
locLowerIdP) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT PState (Parsec Void [Char]) [Located BTyVar]
classParams)
    sing :: a -> [a]
sing a
x      = [a
x]


superP :: Parser (Located BareType)
superP :: Parser (Located (RType BTyCon BTyVar RReft))
superP = forall a. Parser a -> Parser (Located a)
located (forall a. a -> a
toRCls forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
bareAtomBindP)
  where toRCls :: p -> p
toRCls p
x = p
x

instanceLawP :: Parser (RILaws (Located BareType))
instanceLawP :: Parser (RILaws (Located (RType BTyCon BTyVar RReft)))
instanceLawP
  = do SourcePos
l1   <- forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
getSourcePos
       [Located (RType BTyCon BTyVar RReft)]
sups <- Parser [Located (RType BTyCon BTyVar RReft)]
supersP
       BTyCon
c    <- Parser BTyCon
classBTyConP
       [Located (RType BTyCon BTyVar RReft)]
tvs  <- forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
manyTill (forall a. Parser a -> Parser (Located a)
located StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
bareTypeP) (forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try forall a b. (a -> b) -> a -> b
$ [Char] -> Parser ()
reserved [Char]
"where")
       [(LocSymbol, LocSymbol)]
ms   <- forall a. Parser a -> Parser [a]
block Parser (LocSymbol, LocSymbol)
eqBinderP
       SourcePos
l2   <- 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
$ forall ty.
BTyCon
-> [ty]
-> [ty]
-> [(LocSymbol, LocSymbol)]
-> Located ()
-> RILaws ty
RIL BTyCon
c [Located (RType BTyCon BTyVar RReft)]
sups [Located (RType BTyCon BTyVar RReft)]
tvs [(LocSymbol, LocSymbol)]
ms (forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l1 SourcePos
l2 ())
  where
    supersP :: Parser [Located (RType BTyCon BTyVar RReft)]
supersP  = forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try ((forall a. Parser a -> Parser a
parens (Parser (Located (RType BTyCon BTyVar RReft))
superP forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
`sepBy1` Parser [Char]
comma) forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (f :: * -> *) a. Applicative f => a -> f a
pure Parser (Located (RType BTyCon BTyVar RReft))
superP)
                       forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* [Char] -> Parser ()
reservedOp [Char]
"=>")
               forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *) a. Monad m => a -> m a
return []

    eqBinderP :: Parser (LocSymbol, LocSymbol)
eqBinderP = forall x a y. Parser x -> Parser a -> Parser y -> Parser (x, y)
xyP Parser LocSymbol
xP ([Char] -> Parser ()
reservedOp [Char]
"=") Parser LocSymbol
xP

    xP :: Parser LocSymbol
xP = Parser LocSymbol
locBinderP

instanceP :: Parser (RInstance (Located BareType))
instanceP :: Parser (RInstance (Located (RType BTyCon BTyVar RReft)))
instanceP
  = do [Located (RType BTyCon BTyVar RReft)]
_    <- Parser [Located (RType BTyCon BTyVar RReft)]
supersP
       BTyCon
c    <- Parser BTyCon
classBTyConP
       [Located (RType BTyCon BTyVar RReft)]
tvs  <- forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try Parser [Located (RType BTyCon BTyVar RReft)]
oneClassArg forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
manyTill Parser (Located (RType BTyCon BTyVar RReft))
iargsP (forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try forall a b. (a -> b) -> a -> b
$ [Char] -> Parser ()
reserved [Char]
"where")
       [(LocSymbol, RISig (Located (RType BTyCon BTyVar RReft)))]
ms   <- forall a. Parser a -> Parser [a]
block Parser (LocSymbol, RISig (Located (RType BTyCon BTyVar RReft)))
riMethodSigP
       forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. BTyCon -> [t] -> [(LocSymbol, RISig t)] -> RInstance t
RI BTyCon
c [Located (RType BTyCon BTyVar RReft)]
tvs [(LocSymbol, RISig (Located (RType BTyCon BTyVar RReft)))]
ms
  where
    supersP :: Parser [Located (RType BTyCon BTyVar RReft)]
supersP  = forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try ((forall a. Parser a -> Parser a
parens (Parser (Located (RType BTyCon BTyVar RReft))
superP forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
`sepBy1` Parser [Char]
comma) forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (f :: * -> *) a. Applicative f => a -> f a
pure Parser (Located (RType BTyCon BTyVar RReft))
superP)
                       forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* [Char] -> Parser ()
reservedOp [Char]
"=>")
               forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *) a. Monad m => a -> m a
return []

    iargsP :: Parser (Located (RType BTyCon BTyVar RReft))
iargsP   =   (forall {r} {tv} {c}. Monoid r => tv -> Located (RType c tv r)
mkVar forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> BTyVar
bTyVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Symbol
tyVarIdP)
            forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall a. Parser a -> Parser a
parens (forall a. Parser a -> Parser (Located a)
located StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
bareTypeP)


    mkVar :: tv -> Located (RType c tv r)
mkVar tv
v  = forall a. a -> Located a
dummyLoc forall a b. (a -> b) -> a -> b
$ forall c tv r. tv -> r -> RType c tv r
RVar tv
v forall a. Monoid a => a
mempty


riMethodSigP :: Parser (LocSymbol, RISig (Located BareType))
riMethodSigP :: Parser (LocSymbol, RISig (Located (RType BTyCon BTyVar RReft)))
riMethodSigP
  = forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (do [Char] -> Parser ()
reserved [Char]
"assume"
            (LocSymbol
x, Located (RType BTyCon BTyVar RReft)
t) <- Parser (LocSymbol, Located (RType BTyCon BTyVar RReft))
tyBindP
            forall (m :: * -> *) a. Monad m => a -> m a
return (LocSymbol
x, forall t. t -> RISig t
RIAssumed Located (RType BTyCon BTyVar RReft)
t) )
 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do (LocSymbol
x, Located (RType BTyCon BTyVar RReft)
t) <- Parser (LocSymbol, Located (RType BTyCon BTyVar RReft))
tyBindP
        forall (m :: * -> *) a. Monad m => a -> m a
return (LocSymbol
x, forall t. t -> RISig t
RISig Located (RType BTyCon BTyVar RReft)
t)
 forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"riMethodSigP"

classP :: Parser (RClass (Located BareType))
classP :: Parser (RClass (Located (RType BTyCon BTyVar RReft)))
classP
  = do [Located (RType BTyCon BTyVar RReft)]
sups <- Parser [Located (RType BTyCon BTyVar RReft)]
supersP
       BTyCon
c    <- Parser BTyCon
classBTyConP
       [BTyVar]
tvs  <- forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
manyTill (Symbol -> BTyVar
bTyVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Symbol
tyVarIdP) (forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try forall a b. (a -> b) -> a -> b
$ [Char] -> Parser ()
reserved [Char]
"where")
       [(LocSymbol, Located (RType BTyCon BTyVar RReft))]
ms   <- forall a. Parser a -> Parser [a]
block Parser (LocSymbol, Located (RType BTyCon BTyVar RReft))
tyBindP -- <|> sepBy tyBindP semi
       forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty.
BTyCon -> [ty] -> [BTyVar] -> [(LocSymbol, ty)] -> RClass ty
RClass BTyCon
c [Located (RType BTyCon BTyVar RReft)]
sups [BTyVar]
tvs [(LocSymbol, Located (RType BTyCon BTyVar RReft))]
ms
  where
    supersP :: Parser [Located (RType BTyCon BTyVar RReft)]
supersP  = forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try ((forall a. Parser a -> Parser a
parens (Parser (Located (RType BTyCon BTyVar RReft))
superP forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
`sepBy1` Parser [Char]
comma) forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (f :: * -> *) a. Applicative f => a -> f a
pure Parser (Located (RType BTyCon BTyVar RReft))
superP)
                       forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* [Char] -> Parser ()
reservedOp [Char]
"=>")
               forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *) a. Monad m => a -> m a
return []

rawBodyP :: Parser Body
rawBodyP :: Parser Body
rawBodyP
  = forall a. Parser a -> Parser a
braces forall a b. (a -> b) -> a -> b
$ do
      Symbol
v <- Parser Symbol
symbolP
      [Char] -> Parser ()
reservedOp [Char]
"|"
      Symbol -> Expr -> Body
R Symbol
v forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void [Char]) Expr
predP

tyBodyP :: Located BareType -> Parser Body
tyBodyP :: Located (RType BTyCon BTyVar RReft) -> Parser Body
tyBodyP Located (RType BTyCon BTyVar RReft)
ty
  = case forall {c} {tv} {r}. RType c tv r -> Maybe (RType c tv r)
outTy (forall a. Located a -> a
val Located (RType BTyCon BTyVar RReft)
ty) of
      Just RType BTyCon BTyVar RReft
bt | forall t t1. RType BTyCon t t1 -> Bool
isPropBareType RType BTyCon BTyVar RReft
bt
                -> Expr -> Body
P forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void [Char]) Expr
predP
      Maybe (RType BTyCon BTyVar RReft)
_         -> Expr -> Body
E forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void [Char]) Expr
exprP
    where outTy :: RType c tv r -> Maybe (RType c tv r)
outTy (RAllT RTVU c tv
_ RType c tv r
t r
_)    = RType c tv r -> Maybe (RType c tv r)
outTy RType c tv r
t
          outTy (RAllP PVU c tv
_ RType c tv r
t)      = RType c tv r -> Maybe (RType c tv r)
outTy RType c tv r
t
          outTy (RFun Symbol
_ RFInfo
_ RType c tv r
_ RType c tv r
t r
_) = forall a. a -> Maybe a
Just RType c tv r
t
          outTy RType c tv r
_                = forall a. Maybe a
Nothing

locUpperOrInfixIdP :: Parser (Located Symbol)
locUpperOrInfixIdP :: Parser LocSymbol
locUpperOrInfixIdP = Parser LocSymbol
locUpperIdP' forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser LocSymbol
locInfixCondIdP

locBinderP :: Parser (Located Symbol)
locBinderP :: Parser LocSymbol
locBinderP =
  forall a. Parser a -> Parser (Located a)
located Parser Symbol
binderP -- TODO

-- | LHS of the thing being defined
--
-- TODO, Andres: this is still very broken
--
{-
binderP :: Parser Symbol
binderP    = pwr    <$> parens (idP bad)
         <|> symbol <$> idP badc
  where
    idP p  = takeWhile1P Nothing (not . p)
    badc c = (c == ':') || (c == ',') || bad c
    bad c  = isSpace c || c `elem` ("(,)[]" :: String)
    pwr s  = symbol $ "(" `mappend` s `mappend` ")"
-}
binderP :: Parser Symbol
binderP :: Parser Symbol
binderP =
      forall a. Symbolic a => a -> Symbol
symbol forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\ Text
x -> Text
"(" forall a. Semigroup a => a -> a -> a
<> Text
x forall a. Semigroup a => a -> a -> a
<> Text
")") forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Text
symbolText forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Parser a -> Parser a
parens Parser Symbol
infixBinderIdP
  forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Symbol
binderIdP
  -- Note: It is important that we do *not* use the LH/fixpoint reserved words here,
  -- because, for example, we must be able to use "assert" as an identifier.
  --
  -- TODO, Andres: I have no idea why we make the parens part of the symbol here.
  -- But I'm reproducing this behaviour for now, as it is backed up via a few tests.

measureDefP :: Parser Body -> Parser (Def (Located BareType) LocSymbol)
measureDefP :: Parser Body
-> StateT
     PState
     (Parsec Void [Char])
     (Def (Located (RType BTyCon BTyVar RReft)) LocSymbol)
measureDefP Parser Body
bodyP
  = do LocSymbol
mname   <- Parser LocSymbol
locSymbolP
       (LocSymbol
c, [LocSymbol]
xs) <- Parser (LocSymbol, [LocSymbol])
measurePatP
       [Char] -> Parser ()
reservedOp [Char]
"="
       Body
body    <- Parser Body
bodyP
       let xs' :: [Symbol]
xs'  = forall a. Symbolic a => a -> Symbol
symbol forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Located a -> a
val forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [LocSymbol]
xs
       forall (m :: * -> *) a. Monad m => a -> m a
return   forall a b. (a -> b) -> a -> b
$ forall ty ctor.
LocSymbol
-> ctor -> Maybe ty -> [(Symbol, Maybe ty)] -> Body -> Def ty ctor
Def LocSymbol
mname (forall a. Symbolic a => a -> Symbol
symbol forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LocSymbol
c) forall a. Maybe a
Nothing ((, forall a. Maybe a
Nothing) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
xs') Body
body

measurePatP :: Parser (LocSymbol, [LocSymbol])
measurePatP :: Parser (LocSymbol, [LocSymbol])
measurePatP
  =  forall a. Parser a -> Parser a
parens (forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try Parser (LocSymbol, [LocSymbol])
conPatP 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. IsString a => Parser (Located a, [LocSymbol])
consPatP forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall a t. IsString a => Parser (Located a, [t])
nilPatP forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser (LocSymbol, [LocSymbol])
tupPatP)
 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall t. Parser (LocSymbol, [t])
nullaryConPatP
 forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"measurePatP"

tupPatP :: Parser (Located Symbol, [Located Symbol])
tupPatP :: Parser (LocSymbol, [LocSymbol])
tupPatP  = forall (t :: * -> *) a. Foldable t => t a -> (LocSymbol, t a)
mkTupPat  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy1 Parser LocSymbol
locLowerIdP Parser [Char]
comma

conPatP :: Parser (Located Symbol, [Located Symbol])
conPatP :: Parser (LocSymbol, [LocSymbol])
conPatP  = (,)       forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser LocSymbol
dataConNameP forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many Parser LocSymbol
locLowerIdP

consPatP :: IsString a
         => Parser (Located a, [Located Symbol])
consPatP :: forall a. IsString a => Parser (Located a, [LocSymbol])
consPatP = forall a t1 t. IsString a => t1 -> t -> t1 -> (Located a, [t1])
mkConsPat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser LocSymbol
locLowerIdP  forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Char] -> Parser ()
reservedOp [Char]
":" forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser LocSymbol
locLowerIdP

nilPatP :: IsString a
        => Parser (Located a, [t])
nilPatP :: forall a t. IsString a => Parser (Located a, [t])
nilPatP  = forall a t t1. IsString a => t -> (Located a, [t1])
mkNilPat  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Parser a -> Parser a
brackets (forall (f :: * -> *) a. Applicative f => a -> f a
pure ())

nullaryConPatP :: Parser (Located Symbol, [t])
nullaryConPatP :: forall t. Parser (LocSymbol, [t])
nullaryConPatP = forall a t. IsString a => Parser (Located a, [t])
nilPatP forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ((,[]) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser LocSymbol
dataConNameP)
                 forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"nullaryConPatP"

mkTupPat :: Foldable t => t a -> (Located Symbol, t a)
mkTupPat :: forall (t :: * -> *) a. Foldable t => t a -> (LocSymbol, t a)
mkTupPat t a
zs     = (Int -> LocSymbol
tupDataCon (forall (t :: * -> *) a. Foldable t => t a -> Int
length t a
zs), t a
zs)

mkNilPat :: IsString a => t -> (Located a, [t1])
mkNilPat :: forall a t t1. IsString a => t -> (Located a, [t1])
mkNilPat t
_      = (forall a. a -> Located a
dummyLoc a
"[]", []    )

mkConsPat :: IsString a => t1 -> t -> t1 -> (Located a, [t1])
mkConsPat :: forall a t1 t. IsString a => t1 -> t -> t1 -> (Located a, [t1])
mkConsPat t1
x t
_ t1
y = (forall a. a -> Located a
dummyLoc a
":" , [t1
x, t1
y])

tupDataCon :: Int -> Located Symbol
tupDataCon :: Int -> LocSymbol
tupDataCon Int
n    = forall a. a -> Located a
dummyLoc forall a b. (a -> b) -> a -> b
$ forall a. Symbolic a => a -> Symbol
symbol forall a b. (a -> b) -> a -> b
$ [Char]
"(" forall a. Semigroup a => a -> a -> a
<> forall a. Int -> a -> [a]
replicate (Int
n forall a. Num a => a -> a -> a
- Int
1) Char
',' forall a. Semigroup a => a -> a -> a
<> [Char]
")"


-------------------------------------------------------------------------------
--------------------------------- Predicates ----------------------------------
-------------------------------------------------------------------------------

dataConFieldsP :: Parser [(Symbol, BareType)]
dataConFieldsP :: Parser [(Symbol, RType BTyCon BTyVar RReft)]
dataConFieldsP
   =  forall a. Parser a -> Parser [a]
explicitCommaBlock Parser (Symbol, RType BTyCon BTyVar RReft)
predTypeDDP -- braces (sepBy predTypeDDP comma)
  forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many Parser (Symbol, RType BTyCon BTyVar RReft)
dataConFieldP
  forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"dataConFieldP"

dataConFieldP :: Parser (Symbol, BareType)
dataConFieldP :: Parser (Symbol, RType BTyCon BTyVar RReft)
dataConFieldP
   =  forall a. Parser a -> Parser a
parens (forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try Parser (Symbol, RType BTyCon BTyVar RReft)
predTypeDDP forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser (Symbol, RType BTyCon BTyVar RReft)
dbTypeP)
  forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser (Symbol, RType BTyCon BTyVar RReft)
dbTyArgP -- unparenthesised constructor fields must be "atomic"
  forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"dataConFieldP"
  where
    dbTypeP :: Parser (Symbol, RType BTyCon BTyVar RReft)
dbTypeP = (,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Symbol
dummyBindP forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
bareTypeP
    dbTyArgP :: Parser (Symbol, RType BTyCon BTyVar RReft)
dbTyArgP = (,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Symbol
dummyBindP forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
bareTyArgP

predTypeDDP :: Parser (Symbol, BareType)
predTypeDDP :: Parser (Symbol, RType BTyCon BTyVar RReft)
predTypeDDP = (,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Symbol
bbindP forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
bareTypeP

bbindP   :: Parser Symbol
bbindP :: Parser Symbol
bbindP   = Parser Symbol
lowerIdP forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* [Char] -> Parser ()
reservedOp [Char]
"::"

dataConP :: [Symbol] -> Parser DataCtor
dataConP :: [Symbol] -> Parser DataCtor
dataConP [Symbol]
as = do
  LocSymbol
x   <- Parser LocSymbol
dataConNameP
  [(Symbol, RType BTyCon BTyVar RReft)]
xts <- Parser [(Symbol, RType BTyCon BTyVar RReft)]
dataConFieldsP
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ LocSymbol
-> [Symbol]
-> [RType BTyCon BTyVar RReft]
-> [(Symbol, RType BTyCon BTyVar RReft)]
-> Maybe (RType BTyCon BTyVar RReft)
-> DataCtor
DataCtor LocSymbol
x [Symbol]
as [] [(Symbol, RType BTyCon BTyVar RReft)]
xts forall a. Maybe a
Nothing

adtDataConP :: [Symbol] -> Parser DataCtor
adtDataConP :: [Symbol] -> Parser DataCtor
adtDataConP [Symbol]
as = do
  LocSymbol
x     <- Parser LocSymbol
dataConNameP
  [Char] -> Parser ()
reservedOp [Char]
"::"
  RTypeRep BTyCon BTyVar RReft
tr    <- forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
bareTypeP
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ LocSymbol
-> [Symbol]
-> [RType BTyCon BTyVar RReft]
-> [(Symbol, RType BTyCon BTyVar RReft)]
-> Maybe (RType BTyCon BTyVar RReft)
-> DataCtor
DataCtor LocSymbol
x (forall a c r. Symbolic a => [Symbol] -> RTypeRep c a r -> [Symbol]
tRepVars [Symbol]
as RTypeRep BTyCon BTyVar RReft
tr) [] (forall c tv r. RTypeRep c tv r -> [(Symbol, RType c tv r)]
tRepFields RTypeRep BTyCon BTyVar RReft
tr) (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall c tv r. RTypeRep c tv r -> RType c tv r
ty_res RTypeRep BTyCon BTyVar RReft
tr)

tRepVars :: Symbolic a => [Symbol] -> RTypeRep c a r -> [Symbol]
tRepVars :: forall a c r. Symbolic a => [Symbol] -> RTypeRep c a r -> [Symbol]
tRepVars [Symbol]
as RTypeRep c a r
tr = case forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall c tv r. RTypeRep c tv r -> [(RTVar tv (RType c tv ()), r)]
ty_vars RTypeRep c a r
tr of
  [] -> [Symbol]
as
  [RTVar a (RType c a ())]
vs -> forall a. Symbolic a => a -> Symbol
symbol forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall tv s. RTVar tv s -> tv
ty_var_value forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTVar a (RType c a ())]
vs

tRepFields :: RTypeRep c tv r -> [(Symbol, RType c tv r)]
tRepFields :: forall c tv r. RTypeRep c tv r -> [(Symbol, RType c tv r)]
tRepFields RTypeRep c tv r
tr = forall a b. [a] -> [b] -> [(a, b)]
zip (forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds RTypeRep c tv r
tr) (forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args RTypeRep c tv r
tr)

-- TODO: fix Located
dataConNameP :: Parser (Located Symbol)
dataConNameP :: Parser LocSymbol
dataConNameP
  =  forall a. Parser a -> Parser (Located a)
located
 (   forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try Parser Symbol
upperIdP
 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall {a}. (Symbolic a, Semigroup a, IsString a) => a -> Symbol
pwr forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Parser a -> Parser a
parens (forall {e} {s} {m :: * -> *}.
MonadParsec e s m =>
(Token s -> Bool) -> m (Tokens s)
idP Char -> Bool
bad)
 forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"dataConNameP"
 )
  where
     idP :: (Token s -> Bool) -> m (Tokens s)
idP Token s -> Bool
p  = forall e s (m :: * -> *).
MonadParsec e s m =>
Maybe [Char] -> (Token s -> Bool) -> m (Tokens s)
takeWhile1P forall a. Maybe a
Nothing (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Token s -> Bool
p)
     bad :: Char -> Bool
bad Char
c  = Char -> Bool
isSpace Char
c Bool -> Bool -> Bool
|| Char
c forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ([Char]
"(,)" :: String)
     pwr :: a -> Symbol
pwr a
s  = forall a. Symbolic a => a -> Symbol
symbol forall a b. (a -> b) -> a -> b
$ a
"(" forall a. Semigroup a => a -> a -> a
<> a
s forall a. Semigroup a => a -> a -> a
<> a
")"

dataSizeP :: Parser (Maybe SizeFun)
dataSizeP :: Parser (Maybe SizeFun)
dataSizeP
  = forall a. Parser a -> Parser a
brackets (forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocSymbol -> SizeFun
SymSizeFun forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser LocSymbol
locLowerIdP)
  forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing

relationalP :: Parser (LocSymbol, LocSymbol, LocBareType, LocBareType, RelExpr, RelExpr)
relationalP :: Parser
  (LocSymbol, LocSymbol, Located (RType BTyCon BTyVar RReft),
   Located (RType BTyCon BTyVar RReft), RelExpr, RelExpr)
relationalP = do
   LocSymbol
x <- Parser LocSymbol
locBinderP
   [Char] -> Parser ()
reserved [Char]
"~"
   LocSymbol
y <- Parser LocSymbol
locBinderP
   [Char] -> Parser ()
reserved [Char]
"::"
   forall a. Parser a -> Parser a
braces forall a b. (a -> b) -> a -> b
$ do
    Located (RType BTyCon BTyVar RReft)
tx <- forall a. Parser a -> Parser (Located a)
located StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
genBareTypeP
    [Char] -> Parser ()
reserved [Char]
"~"
    Located (RType BTyCon BTyVar RReft)
ty <- forall a. Parser a -> Parser (Located a)
located StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
genBareTypeP
    [Char] -> Parser ()
reserved [Char]
"|"
    RelExpr
assm <- forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (Parser RelExpr
relrefaP forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* [Char] -> Parser ()
reserved [Char]
"|-") forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> RelExpr
ERBasic Expr
PTrue)
    RelExpr
ex <- Parser RelExpr
relrefaP
    forall (m :: * -> *) a. Monad m => a -> m a
return (LocSymbol
x,LocSymbol
y,Located (RType BTyCon BTyVar RReft)
tx,Located (RType BTyCon BTyVar RReft)
ty,RelExpr
assm,RelExpr
ex)

dataDeclP :: Parser DataDecl
dataDeclP :: Parser DataDecl
dataDeclP = do
  SourcePos
pos <- forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
getSourcePos
  LocSymbol
x   <- Parser LocSymbol
locUpperOrInfixIdP
  Maybe SizeFun
fsize <- Parser (Maybe SizeFun)
dataSizeP
  SourcePos -> LocSymbol -> Maybe SizeFun -> Parser DataDecl
dataDeclBodyP SourcePos
pos LocSymbol
x Maybe SizeFun
fsize forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *) a. Monad m => a -> m a
return (LocSymbol -> SourcePos -> Maybe SizeFun -> DataDecl
emptyDecl LocSymbol
x SourcePos
pos Maybe SizeFun
fsize)

emptyDecl :: LocSymbol -> SourcePos -> Maybe SizeFun -> DataDecl
emptyDecl :: LocSymbol -> SourcePos -> Maybe SizeFun -> DataDecl
emptyDecl LocSymbol
x SourcePos
pos fsize :: Maybe SizeFun
fsize@(Just SizeFun
_)
  = DataName
-> [Symbol]
-> [PVar BSort]
-> Maybe [DataCtor]
-> SourcePos
-> Maybe SizeFun
-> Maybe (RType BTyCon BTyVar RReft)
-> DataDeclKind
-> DataDecl
DataDecl (LocSymbol -> DataName
DnName LocSymbol
x) [] [] forall a. Maybe a
Nothing SourcePos
pos Maybe SizeFun
fsize forall a. Maybe a
Nothing DataDeclKind
DataUser
emptyDecl LocSymbol
x SourcePos
pos Maybe SizeFun
_
  = forall a. UserError -> a
uError (forall t. SrcSpan -> Doc -> Doc -> TError t
ErrBadData (SourcePos -> SrcSpan
sourcePosSrcSpan SourcePos
pos) (forall a. PPrint a => a -> Doc
pprint (forall a. Located a -> a
val LocSymbol
x)) forall a. IsString a => a
msg)
  where
    msg :: a
msg = a
"You should specify either a default [size] or one or more fields in the data declaration"

dataDeclBodyP :: SourcePos -> LocSymbol -> Maybe SizeFun -> Parser DataDecl
dataDeclBodyP :: SourcePos -> LocSymbol -> Maybe SizeFun -> Parser DataDecl
dataDeclBodyP SourcePos
pos LocSymbol
x Maybe SizeFun
fsize = do
  Bool
vanilla    <- forall (t :: * -> *) a. Foldable t => t a -> Bool
null forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many Parser LocSymbol
locUpperIdP
  [Symbol]
as         <- forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many Parser Symbol
noWhere -- TODO: check this again
  [PVar BSort]
ps         <- StateT PState (Parsec Void [Char]) [PVar BSort]
predVarDefsP
  (Maybe (RType BTyCon BTyVar RReft)
pTy, [DataCtor]
dcs) <- [Symbol] -> Parser (Maybe (RType BTyCon BTyVar RReft), [DataCtor])
dataCtorsP [Symbol]
as
  let dn :: DataName
dn      = SourcePos -> LocSymbol -> Bool -> [DataCtor] -> DataName
dataDeclName SourcePos
pos LocSymbol
x Bool
vanilla [DataCtor]
dcs
  forall (m :: * -> *) a. Monad m => a -> m a
return      forall a b. (a -> b) -> a -> b
$ DataName
-> [Symbol]
-> [PVar BSort]
-> Maybe [DataCtor]
-> SourcePos
-> Maybe SizeFun
-> Maybe (RType BTyCon BTyVar RReft)
-> DataDeclKind
-> DataDecl
DataDecl DataName
dn [Symbol]
as [PVar BSort]
ps (forall a. a -> Maybe a
Just [DataCtor]
dcs) SourcePos
pos Maybe SizeFun
fsize Maybe (RType BTyCon BTyVar RReft)
pTy DataDeclKind
DataUser

dataDeclName :: SourcePos -> LocSymbol -> Bool -> [DataCtor] -> DataName
dataDeclName :: SourcePos -> LocSymbol -> Bool -> [DataCtor] -> DataName
dataDeclName SourcePos
_ LocSymbol
x Bool
True  [DataCtor]
_     = LocSymbol -> DataName
DnName LocSymbol
x               -- vanilla data    declaration
dataDeclName SourcePos
_ LocSymbol
_ Bool
False (DataCtor
d:[DataCtor]
_) = LocSymbol -> DataName
DnCon  (DataCtor -> LocSymbol
dcName DataCtor
d)      -- family instance declaration
dataDeclName SourcePos
p LocSymbol
x Bool
_  [DataCtor]
_        = forall a. UserError -> a
uError (forall t. SrcSpan -> Doc -> Doc -> TError t
ErrBadData (SourcePos -> SrcSpan
sourcePosSrcSpan SourcePos
p) (forall a. PPrint a => a -> Doc
pprint (forall a. Located a -> a
val LocSymbol
x)) forall a. IsString a => a
msg)
  where
    msg :: a
msg                  = a
"You should specify at least one data constructor for a family instance"

-- | Parse the constructors of a datatype, allowing both classic and GADT-style syntax.
--
-- Note that as of 2020-10-14, we changed the syntax of GADT-style datatype declarations
-- to match Haskell more closely and parse all constructors in a layout-sensitive block,
-- whereas before we required them to be separated by @|@.
--
dataCtorsP :: [Symbol] -> Parser (Maybe BareType, [DataCtor])
dataCtorsP :: [Symbol] -> Parser (Maybe (RType BTyCon BTyVar RReft), [DataCtor])
dataCtorsP [Symbol]
as = do
  (Maybe (RType BTyCon BTyVar RReft)
pTy, [DataCtor]
dcs) <-     ([Char] -> Parser ()
reservedOp [Char]
"="     forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ((forall a. Maybe a
Nothing, ) 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 ([Symbol] -> Parser DataCtor
dataConP    [Symbol]
as) ([Char] -> Parser ()
reservedOp [Char]
"|")))
                forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved   [Char]
"where" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ((forall a. Maybe a
Nothing, ) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>                 forall a. Parser a -> Parser [a]
block ([Symbol] -> Parser DataCtor
adtDataConP [Symbol]
as)                 ))
                forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>                        ((,)         forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser (Maybe (RType BTyCon BTyVar RReft))
dataPropTyP forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Parser a -> Parser [a]
block ([Symbol] -> Parser DataCtor
adtDataConP [Symbol]
as)                  )
  forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (RType BTyCon BTyVar RReft)
pTy, forall b a. Ord b => (a -> b) -> [a] -> [a]
Misc.sortOn (forall a. Located a -> a
val forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCtor -> LocSymbol
dcName) [DataCtor]
dcs)

noWhere :: Parser Symbol
noWhere :: Parser Symbol
noWhere =
  forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try forall a b. (a -> b) -> a -> b
$ do
  Symbol
s <- Parser Symbol
tyVarIdP
  forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Symbol
s forall a. Eq a => a -> a -> Bool
/= Symbol
"where")
  forall (m :: * -> *) a. Monad m => a -> m a
return Symbol
s

dataPropTyP :: Parser (Maybe BareType)
dataPropTyP :: Parser (Maybe (RType BTyCon BTyVar RReft))
dataPropTyP = forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
between ([Char] -> Parser ()
reservedOp [Char]
"::") ([Char] -> Parser ()
reserved [Char]
"where") StateT PState (Parsec Void [Char]) (RType BTyCon BTyVar RReft)
bareTypeP

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

fTyConP :: Parser FTycon
fTyConP :: Parser FTycon
fTyConP
  =   ([Char] -> Parser ()
reserved [Char]
"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
<|> ([Char] -> Parser ()
reserved [Char]
"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
<|> ([Char] -> Parser ()
reserved [Char]
"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
<|> ([Char] -> Parser ()
reserved [Char]
"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
<|> ([Char] -> Parser ()
reserved [Char]
"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
<|> (LocSymbol -> FTycon
symbolFTycon      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser LocSymbol
locUpperIdP)
  forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"fTyConP"

---------------------------------------------------------------------
-- Identifiers ------------------------------------------------------
---------------------------------------------------------------------

-- Andres, TODO: Fix all the rules for identifiers. This was limited to all lowercase letters before.
tyVarIdR :: Parser Symbol
tyVarIdR :: Parser Symbol
tyVarIdR =
  Parser Char
-> (Char -> Bool) -> ([Char] -> Bool) -> [Char] -> 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
'_') Char -> Bool
isAlphaNum [Char] -> Bool
isNotReserved [Char]
"unexpected reserved name"

tyVarIdP :: Parser Symbol
tyVarIdP :: Parser Symbol
tyVarIdP =
  forall a. Parser a -> Parser a
lexeme Parser Symbol
tyVarIdR

aliasIdR :: Parser Symbol
aliasIdR :: Parser Symbol
aliasIdR =
  Parser Char
-> (Char -> Bool) -> ([Char] -> Bool) -> [Char] -> 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
'_') Char -> Bool
isAlphaNum (forall a b. a -> b -> a
const Bool
True) [Char]
"unexpected"

aliasIdP :: Parser Symbol
aliasIdP :: Parser Symbol
aliasIdP =
  forall a. Parser a -> Parser a
lexeme Parser Symbol
aliasIdR

-- | Andres, TODO: This must be liberal with respect to reserved words (LH reserved words are
-- not Haskell reserved words, and we want to redefine all sorts of internal stuff).
--
-- Also, this currently accepts qualified names by allowing '.' ...
-- Moreover, it seems that it is currently allowed to use qualified symbolic names in
-- unparenthesised form. Oh, the parser is also used for reflect, where apparently
-- symbolic names appear in unqualified and unparenthesised form.
-- Furthermore, : is explicitly excluded because a : can directly, without whitespace,
-- follow a binder ...
--
binderIdR :: Parser Symbol
binderIdR :: Parser Symbol
binderIdR =
  Parser Char
-> (Char -> Bool) -> ([Char] -> Bool) -> [Char] -> 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 (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *).
MonadParsec e s m =>
(Token s -> Bool) -> m (Token s)
satisfy Char -> Bool
isHaskellOpStartChar) (\ Char
c -> Char -> Bool
isAlphaNum Char
c Bool -> Bool -> Bool
|| Char -> Bool
isHaskellOpStartChar Char
c Bool -> Bool -> Bool
|| Char
c forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ([Char]
"_'" :: String)) (forall a b. a -> b -> a
const Bool
True) [Char]
"unexpected"

binderIdP :: Parser Symbol
binderIdP :: Parser Symbol
binderIdP =
  forall a. Parser a -> Parser a
lexeme Parser Symbol
binderIdR

infixBinderIdR :: Parser Symbol
infixBinderIdR :: Parser Symbol
infixBinderIdR =
  Parser Char
-> (Char -> Bool) -> ([Char] -> Bool) -> [Char] -> 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 (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *).
MonadParsec e s m =>
(Token s -> Bool) -> m (Token s)
satisfy Char -> Bool
isHaskellOpChar) (\ Char
c -> Char -> Bool
isAlphaNum Char
c Bool -> Bool -> Bool
|| Char -> Bool
isHaskellOpChar Char
c Bool -> Bool -> Bool
|| Char
c forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ([Char]
"_'" :: String)) (forall a b. a -> b -> a
const Bool
True) [Char]
"unexpected"

infixBinderIdP :: Parser Symbol
infixBinderIdP :: Parser Symbol
infixBinderIdP =
  forall a. Parser a -> Parser a
lexeme Parser Symbol
infixBinderIdR

upperIdR' :: Parser Symbol
upperIdR' :: Parser Symbol
upperIdR' =
  Parser Char
-> (Char -> Bool) -> ([Char] -> Bool) -> [Char] -> Parser Symbol
condIdR forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
upperChar (\ Char
c -> Char -> Bool
isAlphaNum Char
c Bool -> Bool -> Bool
|| Char
c forall a. Eq a => a -> a -> Bool
== Char
'\'') (forall a b. a -> b -> a
const Bool
True) [Char]
"unexpected"

locUpperIdP' :: Parser (Located Symbol)
locUpperIdP' :: Parser LocSymbol
locUpperIdP' =
  forall a. Parser a -> Parser (Located a)
locLexeme Parser Symbol
upperIdR'

-- Andres, TODO: This used to force a colon at the end. Also, it used to not
-- allow colons in the middle. Finally, it should probably exclude all reserved
-- operators. I'm just excluding :: because I'm pretty sure that would be
-- undesired.
--
infixCondIdR :: Parser Symbol
infixCondIdR :: Parser Symbol
infixCondIdR =
  Parser Char
-> (Char -> Bool) -> ([Char] -> Bool) -> [Char] -> Parser Symbol
condIdR (forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
':') Char -> Bool
isHaskellOpChar (forall a. Eq a => a -> a -> Bool
/= [Char]
"::") [Char]
"unexpected double colon"

-- Andres, TODO: This used to be completely ad-hoc. It's still not good though.
infixIdR :: Parser Symbol
infixIdR :: Parser Symbol
infixIdR =
  Parser Char
-> (Char -> Bool) -> ([Char] -> Bool) -> [Char] -> Parser Symbol
condIdR (forall e s (m :: * -> *).
MonadParsec e s m =>
(Token s -> Bool) -> m (Token s)
satisfy Char -> Bool
isHaskellOpChar) Char -> Bool
isHaskellOpChar (forall a. Eq a => a -> a -> Bool
/= [Char]
"::") [Char]
"unexpected double colon"

infixIdP :: Parser Symbol
infixIdP :: Parser Symbol
infixIdP =
  forall a. Parser a -> Parser a
lexeme Parser Symbol
infixIdR

{-
infixVarIdR :: Parser Symbol
infixVarIdR =
  condIdR (satisfy isHaskellOpStartChar) isHaskellOpChar (const True)

infixVarIdP :: Parser Symbol
infixVarIdP =
  lexeme infixVarIdR
-}

isHaskellOpChar :: Char -> Bool
isHaskellOpChar :: Char -> Bool
isHaskellOpChar Char
c
  = Char
c forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ([Char]
":!#$%&*+./<=>?@\\^|~-" :: String)

isHaskellOpStartChar :: Char -> Bool
isHaskellOpStartChar :: Char -> Bool
isHaskellOpStartChar Char
c
  = Char
c forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ([Char]
"!#$%&*+./<=>?@\\^|~-" :: String)

locInfixCondIdP :: Parser (Located Symbol)
locInfixCondIdP :: Parser LocSymbol
locInfixCondIdP =
  forall a. Parser a -> Parser (Located a)
locLexeme Parser Symbol
infixCondIdR