-- Parse and typecheck TPTP clauses, stopping at include-clauses.

{-# LANGUAGE BangPatterns, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, TypeOperators, TypeFamilies, CPP, DeriveFunctor #-}
{-# OPTIONS_GHC -funfolding-use-threshold=1000 #-}
module Jukebox.TPTP.Parse.Core where

#include "errors.h"
import Jukebox.TPTP.Parsec
import Control.Applicative
import Control.Monad
import qualified Data.Map.Strict as Map
import Data.Map(Map)
import Data.List
import Jukebox.TPTP.Print
import Jukebox.Name
import qualified Data.Set as Set
import Data.Int
import Jukebox.Utils
import Data.Symbol

import Jukebox.TPTP.Lexer hiding
  (Pos, Error, Include, Var, Type, Not, ForAll,
   Exists, And, Or, Type, Implies, Follows, Xor, Nand, Nor,
   Rational, Real, NegatedConjecture, Question,
   Axiom, Hypothesis, Definition, Assumption, Lemma, Theorem, NegatedConjecture,
   Conjecture, Question,
   keyword, defined, kind)
import qualified Jukebox.TPTP.Lexer as L
import qualified Jukebox.Form as Form
import Jukebox.Form hiding (tag, kind, newFunction, TypeOf(..), run)
import qualified Jukebox.Name as Name

-- The parser monad

data ParseState =
  MkState (Maybe String)           -- filename
          ![Input Form]            -- problem being constructed, inputs are in reverse order
          !(Map Symbol Type)       -- types in scope
          !(Map Symbol [Function]) -- functions in scope
          !(Map Symbol Variable)   -- variables in scope, for CNF
          !Int64                   -- unique supply
type Parser = Parsec ParsecState
type ParsecState = UserState ParseState TokenStream

-- An include-clause.
data IncludeStatement = Include String (Maybe [Tag]) deriving Int -> IncludeStatement -> ShowS
[IncludeStatement] -> ShowS
IncludeStatement -> String
(Int -> IncludeStatement -> ShowS)
-> (IncludeStatement -> String)
-> ([IncludeStatement] -> ShowS)
-> Show IncludeStatement
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [IncludeStatement] -> ShowS
$cshowList :: [IncludeStatement] -> ShowS
show :: IncludeStatement -> String
$cshow :: IncludeStatement -> String
showsPrec :: Int -> IncludeStatement -> ShowS
$cshowsPrec :: Int -> IncludeStatement -> ShowS
Show

-- The initial parser state.
initialState :: Maybe String -> ParseState
initialState :: Maybe String -> ParseState
initialState Maybe String
mfile =
  Maybe String
-> [Name] -> Map Symbol Type -> Map Symbol [Function] -> ParseState
initialStateFrom Maybe String
mfile []
    ([(Symbol, Type)] -> Map Symbol Type
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(String -> Symbol
intern (Name -> String
forall a. Show a => a -> String
show (Type -> Name
forall a. Named a => a -> Name
name Type
ty)), Type
ty) | Type
ty <- [Type
intType, Type
ratType, Type
realType]])
    ([(Symbol, [Function])] -> Map Symbol [Function]
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
       [ (String -> Symbol
intern String
fun,
          [FixedName -> Maybe String -> Name
Fixed (Symbol -> Symbol -> FixedName
Overloaded (String -> Symbol
intern String
fun) (String -> Symbol
intern (Name -> String
forall a. Show a => a -> String
show (Type -> Name
forall a. Named a => a -> Name
name Type
kind)))) Maybe String
forall a. Maybe a
Nothing Name -> FunType -> Function
forall a b. a -> b -> a ::: b
::: FunType
ty
          | (Type
kind, FunType
ty) <- [(Type, FunType)]
tys ])
       | (String
fun, [(Type, FunType)]
tys) <- [(String, [(Type, FunType)])]
funs ])
   where
     overloads :: (Type -> b) -> [(Type, b)]
overloads Type -> b
f = [(Type
ty, Type -> b
f Type
ty) | Type
ty <- [Type
intType, Type
ratType, Type
realType, Type
indType]]
     fun :: [a] -> (Type -> b) -> [(a, [(Type, b)])]
fun [a]
xs Type -> b
f = [(a
x, (Type -> b) -> [(Type, b)]
forall b. (Type -> b) -> [(Type, b)]
overloads Type -> b
f) | a
x <- [a]
xs]

     funs :: [(String, [(Type, FunType)])]
funs =
       [String] -> (Type -> FunType) -> [(String, [(Type, FunType)])]
forall a b. [a] -> (Type -> b) -> [(a, [(Type, b)])]
fun [String
"$less", String
"$lesseq", String
"$greater", String
"$greatereq"]
         (\Type
ty -> [Type] -> Type -> FunType
FunType [Type
ty, Type
ty] Type
O) [(String, [(Type, FunType)])]
-> [(String, [(Type, FunType)])] -> [(String, [(Type, FunType)])]
forall a. [a] -> [a] -> [a]
++
       [String] -> (Type -> FunType) -> [(String, [(Type, FunType)])]
forall a b. [a] -> (Type -> b) -> [(a, [(Type, b)])]
fun [String
"$is_int", String
"$is_rat"]
         (\Type
ty -> [Type] -> Type -> FunType
FunType [Type
ty] Type
O) [(String, [(Type, FunType)])]
-> [(String, [(Type, FunType)])] -> [(String, [(Type, FunType)])]
forall a. [a] -> [a] -> [a]
++
       [String] -> (Type -> FunType) -> [(String, [(Type, FunType)])]
forall a b. [a] -> (Type -> b) -> [(a, [(Type, b)])]
fun [String
"$uminus", String
"$floor", String
"$ceiling", String
"$truncate", String
"$round"]
         (\Type
ty -> [Type] -> Type -> FunType
FunType [Type
ty] Type
ty) [(String, [(Type, FunType)])]
-> [(String, [(Type, FunType)])] -> [(String, [(Type, FunType)])]
forall a. [a] -> [a] -> [a]
++
       [String] -> (Type -> FunType) -> [(String, [(Type, FunType)])]
forall a b. [a] -> (Type -> b) -> [(a, [(Type, b)])]
fun [String
"$sum", String
"$difference", String
"$product",
            String
"$quotient_e", String
"$quotient_t", String
"$quotient_f",
            String
"$remainder_e", String
"$remainder_t", String
"$remainder_f"]
         (\Type
ty -> [Type] -> Type -> FunType
FunType [Type
ty, Type
ty] Type
ty) [(String, [(Type, FunType)])]
-> [(String, [(Type, FunType)])] -> [(String, [(Type, FunType)])]
forall a. [a] -> [a] -> [a]
++
       [(String
"$quotient",
         [(Type
ty, [Type] -> Type -> FunType
FunType [Type
ty, Type
ty] Type
ty) | Type
ty <- [Type
ratType, Type
realType]])] [(String, [(Type, FunType)])]
-> [(String, [(Type, FunType)])] -> [(String, [(Type, FunType)])]
forall a. [a] -> [a] -> [a]
++
       [String] -> (Type -> FunType) -> [(String, [(Type, FunType)])]
forall a b. [a] -> (Type -> b) -> [(a, [(Type, b)])]
fun [String
"$to_int"]  (\Type
ty -> [Type] -> Type -> FunType
FunType [Type
ty] Type
intType) [(String, [(Type, FunType)])]
-> [(String, [(Type, FunType)])] -> [(String, [(Type, FunType)])]
forall a. [a] -> [a] -> [a]
++
       [String] -> (Type -> FunType) -> [(String, [(Type, FunType)])]
forall a b. [a] -> (Type -> b) -> [(a, [(Type, b)])]
fun [String
"$to_rat"]  (\Type
ty -> [Type] -> Type -> FunType
FunType [Type
ty] Type
ratType) [(String, [(Type, FunType)])]
-> [(String, [(Type, FunType)])] -> [(String, [(Type, FunType)])]
forall a. [a] -> [a] -> [a]
++
       [String] -> (Type -> FunType) -> [(String, [(Type, FunType)])]
forall a b. [a] -> (Type -> b) -> [(a, [(Type, b)])]
fun [String
"$to_real"] (\Type
ty -> [Type] -> Type -> FunType
FunType [Type
ty] Type
realType)

initialStateFrom :: Maybe String -> [Name] -> Map Symbol Type -> Map Symbol [Function] -> ParseState
initialStateFrom :: Maybe String
-> [Name] -> Map Symbol Type -> Map Symbol [Function] -> ParseState
initialStateFrom Maybe String
mfile [Name]
xs Map Symbol Type
tys Map Symbol [Function]
fs = Maybe String
-> [Input Form]
-> Map Symbol Type
-> Map Symbol [Function]
-> Map Symbol Variable
-> Int64
-> ParseState
MkState Maybe String
mfile [] Map Symbol Type
tys Map Symbol [Function]
fs Map Symbol Variable
forall k a. Map k a
Map.empty Int64
n
  where
    n :: Int64
n = [Int64] -> Int64
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (Int64
0Int64 -> [Int64] -> [Int64]
forall a. a -> [a] -> [a]
:[Int64 -> Int64
forall a. Enum a => a -> a
succ Int64
m | Unique Int64
m Symbol
_ Maybe String
_ Renamer
_ <- [Name]
xs])

instance Stream TokenStream Token where
  primToken :: TokenStream
-> (TokenStream -> Token -> c) -> c -> (String -> c) -> c
primToken (At Pos
_ (Cons Token
Eof TokenStream
_)) TokenStream -> Token -> c
_ok c
err String -> c
_fatal = c
err
  primToken (At Pos
_ (Cons Token
L.Error TokenStream
_)) TokenStream -> Token -> c
_ok c
_err String -> c
fatal = String -> c
fatal String
"Lexical error"
  primToken (At Pos
_ (Cons Token
t TokenStream
ts)) TokenStream -> Token -> c
ok c
_err String -> c
_fatal = TokenStream -> Token -> c
ok TokenStream
ts Token
t
  type Position TokenStream = TokenStream
  position :: TokenStream -> Position TokenStream
position = TokenStream -> Position TokenStream
forall a. a -> a
id

-- The main parsing function.
data ParseResult a =
    ParseFailed Location [String]
  | ParseSucceeded a
  | ParseStalled Location FilePath (String -> ParseResult a)
  deriving a -> ParseResult b -> ParseResult a
(a -> b) -> ParseResult a -> ParseResult b
(forall a b. (a -> b) -> ParseResult a -> ParseResult b)
-> (forall a b. a -> ParseResult b -> ParseResult a)
-> Functor ParseResult
forall a b. a -> ParseResult b -> ParseResult a
forall a b. (a -> b) -> ParseResult a -> ParseResult b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> ParseResult b -> ParseResult a
$c<$ :: forall a b. a -> ParseResult b -> ParseResult a
fmap :: (a -> b) -> ParseResult a -> ParseResult b
$cfmap :: forall a b. (a -> b) -> ParseResult a -> ParseResult b
Functor

instance Applicative ParseResult where
  pure :: a -> ParseResult a
pure = a -> ParseResult a
forall (m :: * -> *) a. Monad m => a -> m a
return
  <*> :: ParseResult (a -> b) -> ParseResult a -> ParseResult b
(<*>) = ((a -> b) -> a -> b)
-> ParseResult (a -> b) -> ParseResult a -> ParseResult b
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
($)

instance Monad ParseResult where
  return :: a -> ParseResult a
return = a -> ParseResult a
forall a. a -> ParseResult a
ParseSucceeded
  ParseFailed Location
loc [String]
err >>= :: ParseResult a -> (a -> ParseResult b) -> ParseResult b
>>= a -> ParseResult b
_ = Location -> [String] -> ParseResult b
forall a. Location -> [String] -> ParseResult a
ParseFailed Location
loc [String]
err
  ParseSucceeded a
x >>= a -> ParseResult b
f = a -> ParseResult b
f a
x
  ParseStalled Location
loc String
name String -> ParseResult a
k >>= a -> ParseResult b
f =
    Location -> String -> (String -> ParseResult b) -> ParseResult b
forall a.
Location -> String -> (String -> ParseResult a) -> ParseResult a
ParseStalled Location
loc String
name (\String
xs -> String -> ParseResult a
k String
xs ParseResult a -> (a -> ParseResult b) -> ParseResult b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> ParseResult b
f)

data Location = Location FilePath Integer Integer
instance Show Location where
  show :: Location -> String
show (Location String
file Integer
row Integer
col) =
    String
file String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" (line " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
row String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", column " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
col String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"

makeLocation :: FilePath -> L.Pos -> Location
makeLocation :: String -> Pos -> Location
makeLocation String
file (L.Pos Word
row Word
col) =
  String -> Integer -> Integer -> Location
Location String
file (Word -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word
row) (Word -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word
col)

parseProblem :: FilePath -> String -> ParseResult [Input Form]
parseProblem :: String -> String -> ParseResult [Input Form]
parseProblem String
name String
contents = ParseState -> String -> String -> ParseResult [Input Form]
parseProblemFrom (Maybe String -> ParseState
initialState (String -> Maybe String
forall a. a -> Maybe a
Just String
name)) String
name String
contents

parseProblemFrom :: ParseState -> FilePath -> String -> ParseResult [Input Form]
parseProblemFrom :: ParseState -> String -> String -> ParseResult [Input Form]
parseProblemFrom ParseState
state String
name String
contents =
  (ParseState -> [Input Form])
-> ParseResult ParseState -> ParseResult [Input Form]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ParseState -> [Input Form]
finalise (ParseResult ParseState -> ParseResult [Input Form])
-> ParseResult ParseState -> ParseResult [Input Form]
forall a b. (a -> b) -> a -> b
$
    Maybe [String] -> String -> ParsecState -> ParseResult ParseState
aux Maybe [String]
forall a. Maybe a
Nothing String
name (ParseState -> TokenStream -> ParsecState
forall state stream. state -> stream -> UserState state stream
UserState ParseState
state (String -> TokenStream
scan String
contents))
  where
    aux :: Maybe [Tag] -> FilePath -> ParsecState -> ParseResult ParseState
    aux :: Maybe [String] -> String -> ParsecState -> ParseResult ParseState
aux Maybe [String]
tags String
name ParsecState
state =
      case (Position ParsecState -> [String])
-> Parsec ParsecState (Maybe IncludeStatement)
-> ParsecState
-> (Position ParsecState, Either [String] (Maybe IncludeStatement))
forall a c b.
Stream a c =>
(Position a -> [String])
-> Parsec a b -> a -> (Position a, Either [String] b)
run ParsecState -> [String]
Position ParsecState -> [String]
report ((String -> Bool) -> Parsec ParsecState (Maybe IncludeStatement)
section (Maybe [String] -> String -> Bool
included Maybe [String]
tags)) ParsecState
state of
        (UserState{userStream = At pos _}, Left [String]
err) ->
          Location -> [String] -> ParseResult ParseState
forall a. Location -> [String] -> ParseResult a
ParseFailed (String -> Pos -> Location
makeLocation String
name Pos
pos) [String]
err
        (UserState{userState = state'}, Right Maybe IncludeStatement
Nothing) ->
          ParseState -> ParseResult ParseState
forall (m :: * -> *) a. Monad m => a -> m a
return ParseState
state'
        (UserState state (input'@(At pos _)),
         Right (Just (Include String
name' Maybe [String]
tags'))) ->
          Location
-> String
-> (String -> ParseResult ParseState)
-> ParseResult ParseState
forall a.
Location -> String -> (String -> ParseResult a) -> ParseResult a
ParseStalled (String -> Pos -> Location
makeLocation String
name Pos
pos) String
name' ((String -> ParseResult ParseState) -> ParseResult ParseState)
-> (String -> ParseResult ParseState) -> ParseResult ParseState
forall a b. (a -> b) -> a -> b
$ \String
input -> do
            ParseState
state' <- Maybe [String] -> String -> ParsecState -> ParseResult ParseState
aux (Maybe [String]
tags Maybe [String] -> Maybe [String] -> Maybe [String]
`merge` Maybe [String]
tags') String
name' (ParseState -> TokenStream -> ParsecState
forall state stream. state -> stream -> UserState state stream
UserState ParseState
state (String -> TokenStream
scan String
input))
            Maybe [String] -> String -> ParsecState -> ParseResult ParseState
aux Maybe [String]
tags String
name (ParseState -> TokenStream -> ParsecState
forall state stream. state -> stream -> UserState state stream
UserState ParseState
state' TokenStream
input')

    report :: ParsecState -> [String]
    report :: ParsecState -> [String]
report UserState{userStream :: forall state stream. UserState state stream -> stream
userStream = At Pos
_ (Cons Token
Eof TokenStream
_)} =
      [String
"Unexpected end of file"]
    report UserState{userStream :: forall state stream. UserState state stream -> stream
userStream = At Pos
_ (Cons Token
L.Error TokenStream
_)} =
      [String
"Lexical error"]
    report UserState{userStream :: forall state stream. UserState state stream -> stream
userStream = At Pos
_ (Cons Token
t TokenStream
_)} =
      [String
"Unexpected " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Token -> String
forall a. Show a => a -> String
show Token
t]

    included :: Maybe [Tag] -> Tag -> Bool
    included :: Maybe [String] -> String -> Bool
included Maybe [String]
Nothing String
_ = Bool
True
    included (Just [String]
xs) String
x = String
x String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
xs

    merge :: Maybe [Tag] -> Maybe [Tag] -> Maybe [Tag]
    merge :: Maybe [String] -> Maybe [String] -> Maybe [String]
merge Maybe [String]
Nothing Maybe [String]
x = Maybe [String]
x
    merge Maybe [String]
x Maybe [String]
Nothing = Maybe [String]
x
    merge (Just [String]
xs) (Just [String]
ys) = [String] -> Maybe [String]
forall a. a -> Maybe a
Just ([String]
xs [String] -> [String] -> [String]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` [String]
ys)

    finalise :: ParseState -> Problem Form
    finalise :: ParseState -> [Input Form]
finalise (MkState Maybe String
_ [Input Form]
p Map Symbol Type
_ Map Symbol [Function]
_ Map Symbol Variable
_ Int64
_) = [Input Form] -> [Input Form]
forall a. Symbolic a => a -> a
check ([Input Form] -> [Input Form]
forall a. [a] -> [a]
reverse [Input Form]
p)

-- Wee function for testing.
testParser :: Parser a -> String -> Either [String] a
testParser :: Parser a -> String -> Either [String] a
testParser Parser a
p String
s = (ParsecState, Either [String] a) -> Either [String] a
forall a b. (a, b) -> b
snd ((Position ParsecState -> [String])
-> Parser a
-> ParsecState
-> (Position ParsecState, Either [String] a)
forall a c b.
Stream a c =>
(Position a -> [String])
-> Parsec a b -> a -> (Position a, Either [String] b)
run ([String] -> ParsecState -> [String]
forall a b. a -> b -> a
const []) Parser a
p (ParseState -> TokenStream -> ParsecState
forall state stream. state -> stream -> UserState state stream
UserState (Maybe String -> ParseState
initialState Maybe String
forall a. Maybe a
Nothing) (String -> TokenStream
scan String
s)))

-- Primitive parsers.

{-# INLINE keyword' #-}
keyword' :: (Keyword -> Bool) -> Parsec a Token
keyword' Keyword -> Bool
p = (Token -> Bool) -> Parsec a Token
forall a b. Stream a b => (b -> Bool) -> Parsec a b
satisfy Token -> Bool
p'
  where p' :: Token -> Bool
p' Atom { keyword :: Token -> Keyword
L.keyword = Keyword
k } = Keyword -> Bool
p Keyword
k
        p' Token
_ = Bool
False
{-# INLINE keyword #-}
keyword :: Keyword -> Parsec a Token
keyword Keyword
k = (Keyword -> Bool) -> Parsec a Token
forall a. Stream a Token => (Keyword -> Bool) -> Parsec a Token
keyword' (Keyword -> Keyword -> Bool
forall a. Eq a => a -> a -> Bool
== Keyword
k) Parsec a Token -> String -> Parsec a Token
forall a b. Parsec a b -> String -> Parsec a b
<?> String
"'" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Keyword -> String
forall a. Show a => a -> String
show Keyword
k String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"'"
{-# INLINE punct' #-}
punct' :: (Punct -> Bool) -> Parsec a Token
punct' Punct -> Bool
p = (Token -> Bool) -> Parsec a Token
forall a b. Stream a b => (b -> Bool) -> Parsec a b
satisfy Token -> Bool
p'
  where p' :: Token -> Bool
p' Punct { kind :: Token -> Punct
L.kind = Punct
k } = Punct -> Bool
p Punct
k
        p' Token
_ = Bool
False
{-# INLINE punct #-}
punct :: Punct -> Parsec a Token
punct Punct
k = (Punct -> Bool) -> Parsec a Token
forall a. Stream a Token => (Punct -> Bool) -> Parsec a Token
punct' (Punct -> Punct -> Bool
forall a. Eq a => a -> a -> Bool
== Punct
k) Parsec a Token -> String -> Parsec a Token
forall a b. Parsec a b -> String -> Parsec a b
<?> String
"'" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Punct -> String
forall a. Show a => a -> String
show Punct
k String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"'"
{-# INLINE operator #-}
operator :: (Punct -> Bool) -> Parsec a Token
operator Punct -> Bool
q = (Punct -> Bool) -> Parsec a Token
forall a. Stream a Token => (Punct -> Bool) -> Parsec a Token
punct' (\Punct
x -> Punct -> Bool
p Punct
x Bool -> Bool -> Bool
&& Punct -> Bool
q Punct
x) Parsec a Token -> String -> Parsec a Token
forall a b. Parsec a b -> String -> Parsec a b
<?> String
"operator"
  where
    p :: Punct -> Bool
p Punct
Dot = Bool
True
    p Punct
Colon = Bool
True
    p Punct
Times = Bool
True
    p Punct
Plus = Bool
True
    p Punct
FunArrow = Bool
True
    p (Other Symbol
_) = Bool
True
    p Punct
_ = Bool
False
{-# INLINE defined' #-}
defined' :: (Defined -> Bool) -> Parsec a Defined
defined' Defined -> Bool
p = (Token -> Defined) -> Parsec a Token -> Parsec a Defined
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Token -> Defined
L.defined ((Token -> Bool) -> Parsec a Token
forall a b. Stream a b => (b -> Bool) -> Parsec a b
satisfy Token -> Bool
p')
  where p' :: Token -> Bool
p' Defined { defined :: Token -> Defined
L.defined = Defined
d } = Defined -> Bool
p Defined
d
        p' Token
_ = Bool
False
{-# INLINE defined #-}
defined :: Defined -> Parsec a Defined
defined Defined
k = (Defined -> Bool) -> Parsec a Defined
forall a. Stream a Token => (Defined -> Bool) -> Parsec a Defined
defined' (Defined -> Defined -> Bool
forall a. Eq a => a -> a -> Bool
== Defined
k) Parsec a Defined -> String -> Parsec a Defined
forall a b. Parsec a b -> String -> Parsec a b
<?> String
"'" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Defined -> String
forall a. Show a => a -> String
show Defined
k String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"'"
{-# INLINE variable #-}
variable :: Parsec ParsecState Symbol
variable = (Token -> Symbol)
-> Parsec ParsecState Token -> Parsec ParsecState Symbol
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Token -> Symbol
tokenName ((Token -> Bool) -> Parsec ParsecState Token
forall a b. Stream a b => (b -> Bool) -> Parsec a b
satisfy Token -> Bool
p) Parsec ParsecState Symbol -> String -> Parsec ParsecState Symbol
forall a b. Parsec a b -> String -> Parsec a b
<?> String
"variable"
  where p :: Token -> Bool
p L.Var{} = Bool
True
        p Token
_ = Bool
False
{-# INLINE number #-}
number :: Parsec ParsecState Integer
number = (Token -> Integer)
-> Parsec ParsecState Token -> Parsec ParsecState Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Token -> Integer
value ((Token -> Bool) -> Parsec ParsecState Token
forall a b. Stream a b => (b -> Bool) -> Parsec a b
satisfy Token -> Bool
p) Parsec ParsecState Integer -> String -> Parsec ParsecState Integer
forall a b. Parsec a b -> String -> Parsec a b
<?> String
"number"
  where p :: Token -> Bool
p Number{} = Bool
True
        p Token
_ = Bool
False
{-# INLINE ratNumber #-}
ratNumber :: Parsec ParsecState Rational
ratNumber = (Token -> Rational)
-> Parsec ParsecState Token -> Parsec ParsecState Rational
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Token -> Rational
ratValue ((Token -> Bool) -> Parsec ParsecState Token
forall a b. Stream a b => (b -> Bool) -> Parsec a b
satisfy Token -> Bool
p)
  where p :: Token -> Bool
p L.Rational{} = Bool
True
        p Token
_ = Bool
False
{-# INLINE realNumber #-}
realNumber :: Parsec ParsecState Rational
realNumber = (Token -> Rational)
-> Parsec ParsecState Token -> Parsec ParsecState Rational
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Token -> Rational
ratValue ((Token -> Bool) -> Parsec ParsecState Token
forall a b. Stream a b => (b -> Bool) -> Parsec a b
satisfy Token -> Bool
p)
  where p :: Token -> Bool
p L.Real{} = Bool
True
        p Token
_ = Bool
False
{-# INLINE atom #-}
atom :: Parsec ParsecState Symbol
atom = (Token -> Symbol)
-> Parsec ParsecState Token -> Parsec ParsecState Symbol
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Token -> Symbol
tokenName ((Keyword -> Bool) -> Parsec ParsecState Token
forall a. Stream a Token => (Keyword -> Bool) -> Parsec a Token
keyword' (Bool -> Keyword -> Bool
forall a b. a -> b -> a
const Bool
True)) Parsec ParsecState Symbol -> String -> Parsec ParsecState Symbol
forall a b. Parsec a b -> String -> Parsec a b
<?> String
"atom"

-- Combinators.

parens, bracks :: Parser a -> Parser a
{-# INLINE parens #-}
parens :: Parser a -> Parser a
parens Parser a
p = Parsec ParsecState Token
-> Parsec ParsecState Token -> Parser a -> Parser a
forall a b c d.
Parsec a b -> Parsec a c -> Parsec a d -> Parsec a d
between (Punct -> Parsec ParsecState Token
forall a. Stream a Token => Punct -> Parsec a Token
punct Punct
LParen) (Punct -> Parsec ParsecState Token
forall a. Stream a Token => Punct -> Parsec a Token
punct Punct
RParen) Parser a
p
{-# INLINE bracks #-}
bracks :: Parser a -> Parser a
bracks Parser a
p = Parsec ParsecState Token
-> Parsec ParsecState Token -> Parser a -> Parser a
forall a b c d.
Parsec a b -> Parsec a c -> Parsec a d -> Parsec a d
between (Punct -> Parsec ParsecState Token
forall a. Stream a Token => Punct -> Parsec a Token
punct Punct
LBrack) (Punct -> Parsec ParsecState Token
forall a. Stream a Token => Punct -> Parsec a Token
punct Punct
RBrack) Parser a
p

-- Build an expression parser from a binary-connective parser
-- and a leaf parser.
binExpr :: Parser a -> Parser (a -> a -> Parser a) -> Parser a
binExpr :: Parser a -> Parser (a -> a -> Parser a) -> Parser a
binExpr Parser a
leaf Parser (a -> a -> Parser a)
op = do
  a
lhs <- Parser a
leaf
  do { a -> a -> Parser a
f <- Parser (a -> a -> Parser a)
op; a
rhs <- Parser a -> Parser (a -> a -> Parser a) -> Parser a
forall a. Parser a -> Parser (a -> a -> Parser a) -> Parser a
binExpr Parser a
leaf Parser (a -> a -> Parser a)
op; a -> a -> Parser a
f a
lhs a
rhs } Parser a -> Parser a -> Parser a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> a -> Parser a
forall (m :: * -> *) a. Monad m => a -> m a
return a
lhs

-- Parsing clauses.

-- Parse as many things as possible until EOF or an include statement.
section :: (Tag -> Bool) -> Parser (Maybe IncludeStatement)
section :: (String -> Bool) -> Parsec ParsecState (Maybe IncludeStatement)
section String -> Bool
included = Parsec ParsecState () -> Parsec ParsecState ()
forall a b. Parsec a b -> Parsec a ()
skipMany ((String -> Bool) -> Parsec ParsecState ()
input String -> Bool
included) Parsec ParsecState ()
-> Parsec ParsecState (Maybe IncludeStatement)
-> Parsec ParsecState (Maybe IncludeStatement)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ((IncludeStatement -> Maybe IncludeStatement)
-> Parsec ParsecState IncludeStatement
-> Parsec ParsecState (Maybe IncludeStatement)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap IncludeStatement -> Maybe IncludeStatement
forall a. a -> Maybe a
Just Parsec ParsecState IncludeStatement
include Parsec ParsecState (Maybe IncludeStatement)
-> Parsec ParsecState (Maybe IncludeStatement)
-> Parsec ParsecState (Maybe IncludeStatement)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Parsec ParsecState ()
forall a b. Stream a b => Parsec a ()
eof Parsec ParsecState ()
-> Parsec ParsecState (Maybe IncludeStatement)
-> Parsec ParsecState (Maybe IncludeStatement)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe IncludeStatement
-> Parsec ParsecState (Maybe IncludeStatement)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe IncludeStatement
forall a. Maybe a
Nothing))

-- A single non-include clause.
input :: (Tag -> Bool) -> Parser ()
input :: (String -> Bool) -> Parsec ParsecState ()
input String -> Bool
included = Keyword
-> (String -> Parsec ParsecState ()) -> Parsec ParsecState ()
declaration Keyword
Cnf (Parsec ParsecState Form -> String -> Parsec ParsecState ()
formulaIn Parsec ParsecState Form
cnf) Parsec ParsecState ()
-> Parsec ParsecState () -> Parsec ParsecState ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
                 Keyword
-> (String -> Parsec ParsecState ()) -> Parsec ParsecState ()
declaration Keyword
Fof (Parsec ParsecState Form -> String -> Parsec ParsecState ()
formulaIn Parsec ParsecState Form
fof) Parsec ParsecState ()
-> Parsec ParsecState () -> Parsec ParsecState ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
                 Keyword
-> (String -> Parsec ParsecState ()) -> Parsec ParsecState ()
declaration Keyword
Tff (\String
tag -> Parsec ParsecState Form -> String -> Parsec ParsecState ()
formulaIn Parsec ParsecState Form
tff String
tag Parsec ParsecState ()
-> Parsec ParsecState () -> Parsec ParsecState ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parsec ParsecState ()
typeDeclaration) Parsec ParsecState ()
-> Parsec ParsecState () -> Parsec ParsecState ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
                 Keyword
-> (String -> Parsec ParsecState ()) -> Parsec ParsecState ()
declaration Keyword
Tcf (\String
tag -> Parsec ParsecState Form -> String -> Parsec ParsecState ()
formulaIn Parsec ParsecState Form
tff String
tag Parsec ParsecState ()
-> Parsec ParsecState () -> Parsec ParsecState ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parsec ParsecState ()
typeDeclaration)
  where {-# INLINE declaration #-}
        declaration :: Keyword
-> (String -> Parsec ParsecState ()) -> Parsec ParsecState ()
declaration Keyword
k String -> Parsec ParsecState ()
m = do
          Keyword -> Parsec ParsecState Token
forall a. Stream a Token => Keyword -> Parsec a Token
keyword Keyword
k
          Parsec ParsecState () -> Parsec ParsecState ()
forall a. Parser a -> Parser a
parens (Parsec ParsecState () -> Parsec ParsecState ())
-> Parsec ParsecState () -> Parsec ParsecState ()
forall a b. (a -> b) -> a -> b
$ do
            String
t <- Parser String
tag
            Punct -> Parsec ParsecState Token
forall a. Stream a Token => Punct -> Parsec a Token
punct Punct
Comma
            -- Don't bother typechecking clauses that we are not
            -- supposed to include in the problem (seems in the
            -- spirit of TPTP's include mechanism)
            if String -> Bool
included String
t then String -> Parsec ParsecState ()
m String
t else Parsec ParsecState ()
balancedParens
          Punct -> Parsec ParsecState Token
forall a. Stream a Token => Punct -> Parsec a Token
punct Punct
Dot
          () -> Parsec ParsecState ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        formulaIn :: Parsec ParsecState Form -> String -> Parsec ParsecState ()
formulaIn Parsec ParsecState Form
lang String
tag = do
          String -> Form -> Input Form
k <- Parser (String -> Form -> Input Form)
kind
          Punct -> Parsec ParsecState Token
forall a. Stream a Token => Punct -> Parsec a Token
punct Punct
Comma
          Form
form <- Parsec ParsecState Form
lang
          Input Form -> Parsec ParsecState ()
newFormula (String -> Form -> Input Form
k String
tag Form
form)
        balancedParens :: Parsec ParsecState ()
balancedParens = Parsec ParsecState () -> Parsec ParsecState ()
forall a b. Parsec a b -> Parsec a ()
skipMany (Parsec ParsecState () -> Parsec ParsecState ()
forall a. Parser a -> Parser a
parens Parsec ParsecState ()
balancedParens Parsec ParsecState ()
-> Parsec ParsecState () -> Parsec ParsecState ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ((Token -> Bool) -> Parsec ParsecState Token
forall a b. Stream a b => (b -> Bool) -> Parsec a b
satisfy Token -> Bool
p Parsec ParsecState Token
-> Parsec ParsecState () -> Parsec ParsecState ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> () -> Parsec ParsecState ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()))
        p :: Token -> Bool
p Punct{kind :: Token -> Punct
L.kind=Punct
LParen} = Bool
False
        p Punct{kind :: Token -> Punct
L.kind=Punct
RParen} = Bool
False
        p Token
_ = Bool
True

-- A TPTP kind.
kind :: Parser (Tag -> Form -> Input Form)
kind :: Parser (String -> Form -> Input Form)
kind = do
  MkState Maybe String
mfile [Input Form]
_ Map Symbol Type
_ Map Symbol [Function]
_ Map Symbol Variable
_ Int64
_ <- Parsec ParsecState ParseState
forall state a. Parsec (UserState state a) state
getState
  UserState ParseState
_ (At (L.Pos Word
n Word
_) Contents
_) <- Parsec ParsecState ParsecState
forall a b. Stream a b => Parsec a (Position a)
getPosition
  let
    general :: Keyword -> Kind -> Parser (String -> Form -> Input Form)
general Keyword
k Kind
kind = Keyword -> Parsec ParsecState Token
forall a. Stream a Token => Keyword -> Parsec a Token
keyword Keyword
k Parsec ParsecState Token
-> Parser (String -> Form -> Input Form)
-> Parser (String -> Form -> Input Form)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (String -> Form -> Input Form)
-> Parser (String -> Form -> Input Form)
forall (m :: * -> *) a. Monad m => a -> m a
return (Kind -> String -> Form -> Input Form
mk Kind
kind)
    axiom :: Keyword -> AxKind -> Parser (String -> Form -> Input Form)
axiom Keyword
t AxKind
kind = Keyword -> Kind -> Parser (String -> Form -> Input Form)
general Keyword
t (AxKind -> Kind
Form.Ax AxKind
kind)
    conjecture :: Keyword -> ConjKind -> Parser (String -> Form -> Input Form)
conjecture Keyword
t ConjKind
kind = Keyword -> Kind -> Parser (String -> Form -> Input Form)
general Keyword
t (ConjKind -> Kind
Form.Conj ConjKind
kind)
    mk :: Kind -> String -> Form -> Input Form
mk Kind
kind String
tag Form
form =
      Input :: forall a. String -> Kind -> InputSource -> a -> Input a
Input { tag :: String
Form.tag = String
tag,
              kind :: Kind
Form.kind = Kind
kind,
              what :: Form
Form.what = Form
form,
              source :: InputSource
Form.source =
                case Maybe String
mfile of
                  Maybe String
Nothing -> InputSource
Form.Unknown
                  Just String
file -> String -> Int -> InputSource
FromFile String
file (Word -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word
n) }
  Keyword -> AxKind -> Parser (String -> Form -> Input Form)
axiom Keyword
L.Axiom AxKind
Axiom Parser (String -> Form -> Input Form)
-> Parser (String -> Form -> Input Form)
-> Parser (String -> Form -> Input Form)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
    Keyword -> AxKind -> Parser (String -> Form -> Input Form)
axiom Keyword
L.Hypothesis AxKind
Hypothesis Parser (String -> Form -> Input Form)
-> Parser (String -> Form -> Input Form)
-> Parser (String -> Form -> Input Form)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
    Keyword -> AxKind -> Parser (String -> Form -> Input Form)
axiom Keyword
L.Definition AxKind
Definition Parser (String -> Form -> Input Form)
-> Parser (String -> Form -> Input Form)
-> Parser (String -> Form -> Input Form)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
    Keyword -> AxKind -> Parser (String -> Form -> Input Form)
axiom Keyword
L.Assumption AxKind
Assumption Parser (String -> Form -> Input Form)
-> Parser (String -> Form -> Input Form)
-> Parser (String -> Form -> Input Form)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
    Keyword -> AxKind -> Parser (String -> Form -> Input Form)
axiom Keyword
L.Lemma AxKind
Lemma Parser (String -> Form -> Input Form)
-> Parser (String -> Form -> Input Form)
-> Parser (String -> Form -> Input Form)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
    Keyword -> AxKind -> Parser (String -> Form -> Input Form)
axiom Keyword
L.Theorem AxKind
TheoremKind Parser (String -> Form -> Input Form)
-> Parser (String -> Form -> Input Form)
-> Parser (String -> Form -> Input Form)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
    Keyword -> AxKind -> Parser (String -> Form -> Input Form)
axiom Keyword
L.NegatedConjecture AxKind
NegatedConjecture Parser (String -> Form -> Input Form)
-> Parser (String -> Form -> Input Form)
-> Parser (String -> Form -> Input Form)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
    Keyword -> ConjKind -> Parser (String -> Form -> Input Form)
conjecture Keyword
L.Conjecture ConjKind
Conjecture Parser (String -> Form -> Input Form)
-> Parser (String -> Form -> Input Form)
-> Parser (String -> Form -> Input Form)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
    Keyword -> ConjKind -> Parser (String -> Form -> Input Form)
conjecture Keyword
L.Question ConjKind
Question

-- A formula name.
tag :: Parser Tag
tag :: Parser String
tag = (Symbol -> String) -> Parsec ParsecState Symbol -> Parser String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Symbol -> String
unintern Parsec ParsecState Symbol
atom Parser String -> Parser String -> Parser String
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Integer -> String) -> Parsec ParsecState Integer -> Parser String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Integer -> String
forall a. Show a => a -> String
show Parsec ParsecState Integer
number Parser String -> String -> Parser String
forall a b. Parsec a b -> String -> Parsec a b
<?> String
"clause name"

-- An include declaration.
include :: Parser IncludeStatement
include :: Parsec ParsecState IncludeStatement
include = do
  Keyword -> Parsec ParsecState Token
forall a. Stream a Token => Keyword -> Parsec a Token
keyword Keyword
L.Include
  IncludeStatement
res <- Parsec ParsecState IncludeStatement
-> Parsec ParsecState IncludeStatement
forall a. Parser a -> Parser a
parens (Parsec ParsecState IncludeStatement
 -> Parsec ParsecState IncludeStatement)
-> Parsec ParsecState IncludeStatement
-> Parsec ParsecState IncludeStatement
forall a b. (a -> b) -> a -> b
$ do
    Symbol
name <- Parsec ParsecState Symbol
atom Parsec ParsecState Symbol -> String -> Parsec ParsecState Symbol
forall a b. Parsec a b -> String -> Parsec a b
<?> String
"quoted filename"
    Maybe [String]
clauses <- do { Punct -> Parsec ParsecState Token
forall a. Stream a Token => Punct -> Parsec a Token
punct Punct
Comma
                  ; ([String] -> Maybe [String])
-> Parsec ParsecState [String]
-> Parsec ParsecState (Maybe [String])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [String] -> Maybe [String]
forall a. a -> Maybe a
Just (Parsec ParsecState [String] -> Parsec ParsecState [String]
forall a. Parser a -> Parser a
bracks (Parser String
-> Parsec ParsecState Token -> Parsec ParsecState [String]
forall a b c. Parsec a b -> Parsec a c -> Parsec a [b]
sepBy1 Parser String
tag (Punct -> Parsec ParsecState Token
forall a. Stream a Token => Punct -> Parsec a Token
punct Punct
Comma))) } Parsec ParsecState (Maybe [String])
-> Parsec ParsecState (Maybe [String])
-> Parsec ParsecState (Maybe [String])
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Maybe [String] -> Parsec ParsecState (Maybe [String])
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe [String]
forall a. Maybe a
Nothing
    IncludeStatement -> Parsec ParsecState IncludeStatement
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Maybe [String] -> IncludeStatement
Include (Symbol -> String
unintern Symbol
name) Maybe [String]
clauses)
  Punct -> Parsec ParsecState Token
forall a. Stream a Token => Punct -> Parsec a Token
punct Punct
Dot
  IncludeStatement -> Parsec ParsecState IncludeStatement
forall (m :: * -> *) a. Monad m => a -> m a
return IncludeStatement
res

-- Inserting types, functions and clauses.

newFormula :: Input Form -> Parser ()
newFormula :: Input Form -> Parsec ParsecState ()
newFormula Input Form
input = do
  MkState Maybe String
mfile [Input Form]
p Map Symbol Type
t Map Symbol [Function]
f Map Symbol Variable
v Int64
n <- Parsec ParsecState ParseState
forall state a. Parsec (UserState state a) state
getState
  ParseState -> Parsec ParsecState ()
forall state a. state -> Parsec (UserState state a) ()
putState (Maybe String
-> [Input Form]
-> Map Symbol Type
-> Map Symbol [Function]
-> Map Symbol Variable
-> Int64
-> ParseState
MkState Maybe String
mfile (Input Form
inputInput Form -> [Input Form] -> [Input Form]
forall a. a -> [a] -> [a]
:[Input Form]
p) Map Symbol Type
t Map Symbol [Function]
f Map Symbol Variable
v Int64
n)
  
newFunction :: Symbol -> FunType -> Parser Function
newFunction :: Symbol -> FunType -> Parser Function
newFunction Symbol
name FunType
ty = do
  [Function]
fs <- FunType -> Symbol -> Parser [Function]
lookupFunction FunType
ty Symbol
name
  case [ Function
f | Function
f <- [Function]
fs, Function -> FunType
forall a b. (a ::: b) -> b
rhs Function
f FunType -> FunType -> Bool
forall a. Eq a => a -> a -> Bool
== FunType
ty ] of
    [] ->
      String -> Parser Function
forall a c b. Stream a c => String -> Parsec a b
fatalError (String -> Parser Function) -> String -> Parser Function
forall a b. (a -> b) -> a -> b
$ String
"Constant " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Symbol -> String
unintern Symbol
name String -> ShowS
forall a. [a] -> [a] -> [a]
++
                   String
" was declared to have type " String -> ShowS
forall a. [a] -> [a] -> [a]
++ FunType -> String
forall a. Pretty a => a -> String
prettyShow FunType
ty String -> ShowS
forall a. [a] -> [a] -> [a]
++
                   String
" but already has type " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [FunType] -> String
showTypes ((Function -> FunType) -> [Function] -> [FunType]
forall a b. (a -> b) -> [a] -> [b]
map Function -> FunType
forall a b. (a ::: b) -> b
rhs [Function]
fs)
    (Function
f:[Function]
_) -> Function -> Parser Function
forall (m :: * -> *) a. Monad m => a -> m a
return Function
f

showTypes :: [FunType] -> String
showTypes :: [FunType] -> String
showTypes = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
" and " ([String] -> String)
-> ([FunType] -> [String]) -> [FunType] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FunType -> String) -> [FunType] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map FunType -> String
forall a. Pretty a => a -> String
prettyShow

{-# INLINE applyFunction #-}
applyFunction :: Symbol -> [Term] -> Type -> Parser Term
applyFunction :: Symbol -> [Term] -> Type -> Parser Term
applyFunction Symbol
name [Term]
args Type
res = do
  [Function]
fs <- FunType -> Symbol -> Parser [Function]
lookupFunction ([Type] -> Type -> FunType
FunType (Int -> Type -> [Type]
forall a. Int -> a -> [a]
replicate ([Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
args) Type
indType) Type
res) Symbol
name
  case [ Function
f | Function
f <- [Function]
fs, Function -> [Type]
funArgs Function
f [Type] -> [Type] -> Bool
forall a. Eq a => a -> a -> Bool
== (Term -> Type) -> [Term] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Type
forall a. Typed a => a -> Type
typ [Term]
args ] of
    [] -> [Function] -> [Term] -> Parser Term
forall a c b. Stream a c => [Function] -> [Term] -> Parsec a b
typeError [Function]
fs [Term]
args
    (Function
f:[Function]
_) -> Term -> Parser Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Function
f Function -> [Term] -> Term
:@: [Term]
args)

{-# NOINLINE typeError #-}
typeError :: [Function] -> [Term] -> Parsec a b
typeError fs :: [Function]
fs@(f :: Function
f@(Name
x ::: FunType
_):[Function]
_) [Term]
args' = do
    let plural :: a -> p -> p -> p
plural a
1 p
x p
_ = p
x 
        plural a
_ p
_ p
y = p
y
        lengths :: [Int]
lengths = [Int] -> [Int]
forall a. Ord a => [a] -> [a]
usort ((Function -> Int) -> [Function] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map ([Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Type] -> Int) -> (Function -> [Type]) -> Function -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Function -> [Type]
funArgs) [Function]
fs)
    String -> Parsec a b
forall a c b. Stream a c => String -> Parsec a b
fatalError (String -> Parsec a b) -> String -> Parsec a b
forall a b. (a -> b) -> a -> b
$ String
"Type mismatch in term '" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Pretty a => a -> String
prettyShow (Term -> Term
forall a. Symbolic a => a -> a
prettyNames (Function
f Function -> [Term] -> Term
:@: [Term]
args')) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"': " String -> ShowS
forall a. [a] -> [a] -> [a]
++
                 String
"Constant " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Pretty a => a -> String
prettyShow Name
x String -> ShowS
forall a. [a] -> [a] -> [a]
++
                 if [Int] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
lengths Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 Bool -> Bool -> Bool
&& [Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
args' Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Int]
lengths then
                   String
" has arity " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([Int] -> Int
forall a. [a] -> a
head [Int]
lengths) String -> ShowS
forall a. [a] -> [a] -> [a]
++
                   String
" but was applied to " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
args') String -> ShowS
forall a. [a] -> [a] -> [a]
++
                   Int -> String -> ShowS
forall a p. (Eq a, Num a) => a -> p -> p -> p
plural ([Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
args') String
" argument" String
" arguments"
                 else
                   String
" has type " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [FunType] -> String
showTypes ((Function -> FunType) -> [Function] -> [FunType]
forall a b. (a -> b) -> [a] -> [b]
map Function -> FunType
forall a b. (a ::: b) -> b
rhs [Function]
fs) String -> ShowS
forall a. [a] -> [a] -> [a]
++
                   String
" but was applied to " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String -> ShowS
forall a p. (Eq a, Num a) => a -> p -> p -> p
plural ([Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
args') String
"an argument" String
"arguments" String -> ShowS
forall a. [a] -> [a] -> [a]
++
                   String
" of type " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " ((Term -> String) -> [Term] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Type -> String
forall a. Pretty a => a -> String
prettyShow (Type -> String) -> (Term -> Type) -> Term -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Type
forall a. Typed a => a -> Type
typ) [Term]
args')

{-# INLINE lookupType #-}
lookupType :: Symbol -> Parser Type
lookupType :: Symbol -> Parser Type
lookupType Symbol
xs = do
  MkState Maybe String
mfile [Input Form]
p Map Symbol Type
t Map Symbol [Function]
f Map Symbol Variable
v Int64
n <- Parsec ParsecState ParseState
forall state a. Parsec (UserState state a) state
getState
  case Symbol -> Map Symbol Type -> Maybe Type
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Symbol
xs Map Symbol Type
t of
    Maybe Type
Nothing -> do
      let ty :: Type
ty = Name -> Type
Type (Symbol -> Name
forall a. Named a => a -> Name
name Symbol
xs)
      ParseState -> Parsec ParsecState ()
forall state a. state -> Parsec (UserState state a) ()
putState (Maybe String
-> [Input Form]
-> Map Symbol Type
-> Map Symbol [Function]
-> Map Symbol Variable
-> Int64
-> ParseState
MkState Maybe String
mfile [Input Form]
p (Symbol -> Type -> Map Symbol Type -> Map Symbol Type
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Symbol
xs Type
ty Map Symbol Type
t) Map Symbol [Function]
f Map Symbol Variable
v Int64
n)
      Type -> Parser Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty
    Just Type
ty -> Type -> Parser Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty

{-# INLINE lookupFunction #-}
lookupFunction :: FunType -> Symbol -> Parser [Name ::: FunType]
lookupFunction :: FunType -> Symbol -> Parser [Function]
lookupFunction FunType
def Symbol
x = do
  MkState Maybe String
mfile [Input Form]
p Map Symbol Type
t Map Symbol [Function]
f Map Symbol Variable
v Int64
n <- Parsec ParsecState ParseState
forall state a. Parsec (UserState state a) state
getState
  case Symbol -> Map Symbol [Function] -> Maybe [Function]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Symbol
x Map Symbol [Function]
f of
    Maybe [Function]
Nothing -> do
      let decl :: Function
decl = Symbol -> Name
forall a. Named a => a -> Name
name Symbol
x Name -> FunType -> Function
forall a b. a -> b -> a ::: b
::: FunType
def
      ParseState -> Parsec ParsecState ()
forall state a. state -> Parsec (UserState state a) ()
putState (Maybe String
-> [Input Form]
-> Map Symbol Type
-> Map Symbol [Function]
-> Map Symbol Variable
-> Int64
-> ParseState
MkState Maybe String
mfile [Input Form]
p Map Symbol Type
t (Symbol
-> [Function] -> Map Symbol [Function] -> Map Symbol [Function]
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Symbol
x [Function
decl] Map Symbol [Function]
f) Map Symbol Variable
v Int64
n)
      [Function] -> Parser [Function]
forall (m :: * -> *) a. Monad m => a -> m a
return [Function
decl]
    Just [Function]
fs -> [Function] -> Parser [Function]
forall (m :: * -> *) a. Monad m => a -> m a
return [Function]
fs

getFunctions :: Parser (Map Symbol [Function])
getFunctions :: Parser (Map Symbol [Function])
getFunctions = do
  MkState Maybe String
_ [Input Form]
_ Map Symbol Type
_ Map Symbol [Function]
f Map Symbol Variable
_ Int64
_ <- Parsec ParsecState ParseState
forall state a. Parsec (UserState state a) state
getState
  Map Symbol [Function] -> Parser (Map Symbol [Function])
forall (m :: * -> *) a. Monad m => a -> m a
return Map Symbol [Function]
f

-- Parsing formulae.

cnf, tff, fof :: Parser Form
cnf :: Parsec ParsecState Form
cnf = do
  MkState Maybe String
mfile [Input Form]
p Map Symbol Type
t Map Symbol [Function]
f Map Symbol Variable
_ Int64
n <- Parsec ParsecState ParseState
forall state a. Parsec (UserState state a) state
getState
  ParseState -> Parsec ParsecState ()
forall state a. state -> Parsec (UserState state a) ()
putState (Maybe String
-> [Input Form]
-> Map Symbol Type
-> Map Symbol [Function]
-> Map Symbol Variable
-> Int64
-> ParseState
MkState Maybe String
mfile [Input Form]
p Map Symbol Type
t Map Symbol [Function]
f Map Symbol Variable
forall k a. Map k a
Map.empty Int64
n)
  Form
form <- Mode -> Map Symbol Variable -> Parsec ParsecState Form
forall a. TermLike a => Mode -> Map Symbol Variable -> Parser a
formula Mode
NoQuantification __
  Form -> Parsec ParsecState Form
forall (m :: * -> *) a. Monad m => a -> m a
return (Form -> Form
closeForm Form
form)
tff :: Parsec ParsecState Form
tff = Mode -> Map Symbol Variable -> Parsec ParsecState Form
forall a. TermLike a => Mode -> Map Symbol Variable -> Parser a
formula Mode
Typed Map Symbol Variable
forall k a. Map k a
Map.empty
fof :: Parsec ParsecState Form
fof = Mode -> Map Symbol Variable -> Parsec ParsecState Form
forall a. TermLike a => Mode -> Map Symbol Variable -> Parser a
formula Mode
Untyped Map Symbol Variable
forall k a. Map k a
Map.empty

-- We cannot always know whether what we are parsing is a formula or a
-- term, since we don't have lookahead. For example, p(x) might be a
-- formula, but in p(x)=y, p(x) is a term.
--
-- To deal with this, we introduce the Thing datatype.
-- A thing is either a term or a formula, or a literal that we don't know
-- if it should be a term or a formula. Instead of a separate formula-parser
-- and term-parser we have a combined thing-parser.
data Thing = Apply !Symbol ![Term]
           | Term !Term
           | Formula !Form

instance Show Thing where
  show :: Thing -> String
show (Apply Symbol
f []) = Symbol -> String
unintern Symbol
f
  show (Apply Symbol
f [Term]
args) =
    Symbol -> String
unintern Symbol
f String -> ShowS
forall a. [a] -> [a] -> [a]
++
      case [Term]
args of
        [] -> String
""
        [Term]
args -> [Term] -> String
forall a. Pretty a => a -> String
prettyShow [Term]
args
  show (Term Term
t) = Term -> String
forall a. Pretty a => a -> String
prettyShow Term
t
  show (Formula Form
f) = Form -> String
forall a. Pretty a => a -> String
prettyShow Form
f

-- However, often we do know whether we want a formula or a term,
-- and there it's best to use a specialised parser (not least because
-- the error messages are better). For that reason, our parser is
-- parametrised on the type of thing you want to parse. We have two
-- main parsers:
--   * 'term' parses a term or predicate
--   * 'formula' parses an arbitrary expression
-- You can instantiate 'term' for Term, Form or Thing; in each case
-- you get an appropriate parser. You can instantiate 'formula' for
-- Form or Thing.

-- Types for which a term f(...) is a valid literal. These are the types on
-- which you can use 'term'.
class TermLike a where
  -- Convert from a Thing.
  fromThing :: Thing -> Parser a
  -- Parse a variable occurrence as a term on its own, if that's allowed.
  var :: Mode -> Map Symbol Variable -> Parser a
  -- Parse the input as a formula, if that's allowed.
  parseFormula :: Parser Form -> Parser a
  -- A parser for this type.
  parser :: Mode -> Map Symbol Variable -> Parser a

data Mode = Typed | Untyped | NoQuantification

instance TermLike Form where
  {-# INLINE fromThing #-}
  fromThing :: Thing -> Parsec ParsecState Form
fromThing (Apply Symbol
x [Term]
xs) = (Term -> Form) -> Parser Term -> Parsec ParsecState Form
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Literal -> Form
Literal (Literal -> Form) -> (Term -> Literal) -> Term -> Form
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Atomic -> Literal
forall a. a -> Signed a
Pos (Atomic -> Literal) -> (Term -> Atomic) -> Term -> Literal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Atomic
Tru) (Symbol -> [Term] -> Type -> Parser Term
applyFunction Symbol
x [Term]
xs Type
O)
  fromThing (Term Term
_) = Parsec ParsecState Form
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  fromThing (Formula Form
f) = Form -> Parsec ParsecState Form
forall (m :: * -> *) a. Monad m => a -> m a
return Form
f
  -- A variable itself is not a valid formula.
  var :: Mode -> Map Symbol Variable -> Parsec ParsecState Form
var Mode
_ Map Symbol Variable
_ = Parsec ParsecState Form
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  parseFormula :: Parsec ParsecState Form -> Parsec ParsecState Form
parseFormula = Parsec ParsecState Form -> Parsec ParsecState Form
forall a. a -> a
id
  parser :: Mode -> Map Symbol Variable -> Parsec ParsecState Form
parser = Mode -> Map Symbol Variable -> Parsec ParsecState Form
forall a. TermLike a => Mode -> Map Symbol Variable -> Parser a
formula

instance TermLike Term where
  {-# INLINE fromThing #-}
  fromThing :: Thing -> Parser Term
fromThing (Apply Symbol
x [Term]
xs) = Symbol -> [Term] -> Type -> Parser Term
applyFunction Symbol
x [Term]
xs Type
indType
  fromThing (Term Term
t) = Term -> Parser Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t
  fromThing (Formula Form
_) = Parser Term
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  parseFormula :: Parsec ParsecState Form -> Parser Term
parseFormula Parsec ParsecState Form
_ = Parser Term
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  parser :: Mode -> Map Symbol Variable -> Parser Term
parser = Mode -> Map Symbol Variable -> Parser Term
forall a. TermLike a => Mode -> Map Symbol Variable -> Parser a
term

  {-# INLINE var #-}
  var :: Mode -> Map Symbol Variable -> Parser Term
var Mode
NoQuantification Map Symbol Variable
_ = do
    Symbol
x <- Parsec ParsecState Symbol
variable
    MkState Maybe String
mfile [Input Form]
p Map Symbol Type
t Map Symbol [Function]
f Map Symbol Variable
ctx Int64
n <- Parsec ParsecState ParseState
forall state a. Parsec (UserState state a) state
getState
    case Symbol -> Map Symbol Variable -> Maybe Variable
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Symbol
x Map Symbol Variable
ctx of
      Just Variable
v -> Term -> Parser Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Variable -> Term
Var Variable
v)
      Maybe Variable
Nothing -> do
        let v :: Variable
v = Int64 -> Symbol -> Maybe String -> Renamer -> Name
Unique (Int64
nInt64 -> Int64 -> Int64
forall a. Num a => a -> a -> a
+Int64
1) Symbol
x Maybe String
forall a. Maybe a
Nothing Renamer
defaultRenamer Name -> Type -> Variable
forall a b. a -> b -> a ::: b
::: Type
indType
        ParseState -> Parsec ParsecState ()
forall state a. state -> Parsec (UserState state a) ()
putState (Maybe String
-> [Input Form]
-> Map Symbol Type
-> Map Symbol [Function]
-> Map Symbol Variable
-> Int64
-> ParseState
MkState Maybe String
mfile [Input Form]
p Map Symbol Type
t Map Symbol [Function]
f (Symbol -> Variable -> Map Symbol Variable -> Map Symbol Variable
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Symbol
x Variable
v Map Symbol Variable
ctx) (Int64
nInt64 -> Int64 -> Int64
forall a. Num a => a -> a -> a
+Int64
1))
        Term -> Parser Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Variable -> Term
Var Variable
v)
  var Mode
_ Map Symbol Variable
ctx = do
    Symbol
x <- Parsec ParsecState Symbol
variable
    case Symbol -> Map Symbol Variable -> Maybe Variable
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Symbol
x Map Symbol Variable
ctx of
      Just Variable
v -> Term -> Parser Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Variable -> Term
Var Variable
v)
      Maybe Variable
Nothing -> String -> Parser Term
forall a c b. Stream a c => String -> Parsec a b
fatalError (String -> Parser Term) -> String -> Parser Term
forall a b. (a -> b) -> a -> b
$ String
"unbound variable " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Symbol -> String
unintern Symbol
x

instance TermLike Thing where
  fromThing :: Thing -> Parser Thing
fromThing = Thing -> Parser Thing
forall (m :: * -> *) a. Monad m => a -> m a
return
  var :: Mode -> Map Symbol Variable -> Parser Thing
var Mode
mode Map Symbol Variable
ctx = (Term -> Thing) -> Parser Term -> Parser Thing
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> Thing
Term (Mode -> Map Symbol Variable -> Parser Term
forall a. TermLike a => Mode -> Map Symbol Variable -> Parser a
var Mode
mode Map Symbol Variable
ctx)
  parseFormula :: Parsec ParsecState Form -> Parser Thing
parseFormula = (Form -> Thing) -> Parsec ParsecState Form -> Parser Thing
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Form -> Thing
Formula
  parser :: Mode -> Map Symbol Variable -> Parser Thing
parser = Mode -> Map Symbol Variable -> Parser Thing
forall a. TermLike a => Mode -> Map Symbol Variable -> Parser a
formula

-- An atomic expression.
{-# INLINEABLE atomic #-}
atomic :: TermLike a => Mode -> Map Symbol Variable -> Parser a
atomic :: Mode -> Map Symbol Variable -> Parser a
atomic Mode
mode Map Symbol Variable
ctx = Parser a
function Parser a -> Parser a -> Parser a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Mode -> Map Symbol Variable -> Parser a
forall a. TermLike a => Mode -> Map Symbol Variable -> Parser a
var Mode
mode Map Symbol Variable
ctx Parser a -> Parser a -> Parser a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser a
num Parser a -> Parser a -> Parser a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser a -> Parser a
forall a. Parser a -> Parser a
parens (Mode -> Map Symbol Variable -> Parser a
forall a. TermLike a => Mode -> Map Symbol Variable -> Parser a
parser Mode
mode Map Symbol Variable
ctx)
  where
    {-# INLINE function #-}
    function :: Parser a
function = do
      Symbol
x <- Parsec ParsecState Symbol
atom
      [Term]
args <- Parser [Term] -> Parser [Term]
forall a. Parser a -> Parser a
parens (Parser Term -> Parsec ParsecState Token -> Parser [Term]
forall a b c. Parsec a b -> Parsec a c -> Parsec a [b]
sepBy1 (Mode -> Map Symbol Variable -> Parser Term
forall a. TermLike a => Mode -> Map Symbol Variable -> Parser a
term Mode
mode Map Symbol Variable
ctx) (Punct -> Parsec ParsecState Token
forall a. Stream a Token => Punct -> Parsec a Token
punct Punct
Comma)) Parser [Term] -> Parser [Term] -> Parser [Term]
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Term] -> Parser [Term]
forall (m :: * -> *) a. Monad m => a -> m a
return []
      Thing -> Parser a
forall a. TermLike a => Thing -> Parser a
fromThing (Symbol -> [Term] -> Thing
Apply Symbol
x [Term]
args)

    {-# INLINE num #-}
    num :: Parser a
num = (Parser a
int Parser a -> Parser a -> Parser a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser a
rat Parser a -> Parser a -> Parser a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser a
real)

    {-# INLINE int #-}
    int :: Parser a
int = do
      Integer
n <- Parsec ParsecState Integer
number
      FixedName -> Type -> Parser a
forall a. TermLike a => FixedName -> Type -> Parser a
constant (Integer -> FixedName
Integer Integer
n) Type
intType

    {-# INLINE rat #-}
    rat :: Parser a
rat = do
      Rational
x <- Parsec ParsecState Rational
ratNumber
      FixedName -> Type -> Parser a
forall a. TermLike a => FixedName -> Type -> Parser a
constant (Rational -> FixedName
Rational Rational
x) Type
ratType

    {-# INLINE real #-}
    real :: Parser a
real = do
      Rational
x <- Parsec ParsecState Rational
realNumber
      FixedName -> Type -> Parser a
forall a. TermLike a => FixedName -> Type -> Parser a
constant (Rational -> FixedName
Real Rational
x) Type
realType

    {-# INLINE constant #-}
    constant :: FixedName -> Type -> Parser a
constant FixedName
x Type
ty =
      Thing -> Parser a
forall a. TermLike a => Thing -> Parser a
fromThing (Term -> Thing
Term ((FixedName -> Maybe String -> Name
Fixed FixedName
x Maybe String
forall a. Maybe a
Nothing Name -> FunType -> Function
forall a b. a -> b -> a ::: b
::: [Type] -> Type -> FunType
FunType [] Type
ty) Function -> [Term] -> Term
:@: []))

unary :: TermLike a => Mode -> Map Symbol Variable -> Parser a
unary :: Mode -> Map Symbol Variable -> Parser a
unary Mode
mode Map Symbol Variable
ctx =
  Parser a
forall a. TermLike a => Parser a
prefix Parser a -> Parser a -> Parser a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do
    Thing
t <- Mode -> Map Symbol Variable -> Parser Thing
forall a. TermLike a => Mode -> Map Symbol Variable -> Parser a
atomic Mode
mode Map Symbol Variable
ctx :: Parser Thing
    Thing -> Parser a
forall a. TermLike a => Thing -> Parser a
maybePostfix Thing
t
  where
    prefix :: TermLike a => Parser a
    prefix :: Parser a
prefix = do
      Symbol
p <- Parsec ParsecState Symbol
prefixOperator
      Term
arg <- Parser Term
forall a. TermLike a => Parser a
prefix Parser Term -> Parser Term -> Parser Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Mode -> Map Symbol Variable -> Parser Term
forall a. TermLike a => Mode -> Map Symbol Variable -> Parser a
atomic Mode
mode Map Symbol Variable
ctx :: Parser Term
      Thing -> Parser a
forall a. TermLike a => Thing -> Parser a
fromThing (Symbol -> [Term] -> Thing
Apply Symbol
p [Term
arg])
    maybePostfix, postfix :: TermLike a => Thing -> Parser a
    maybePostfix :: Thing -> Parser a
maybePostfix Thing
t = Thing -> Parser a
forall a. TermLike a => Thing -> Parser a
postfix Thing
t Parser a -> Parser a -> Parser a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Thing -> Parser a
forall a. TermLike a => Thing -> Parser a
fromThing Thing
t
    postfix :: Thing -> Parser a
postfix Thing
t = do
      Symbol
p <- Parsec ParsecState Symbol
postfixOperator
      Term
arg <- Thing -> Parser Term
forall a. TermLike a => Thing -> Parser a
fromThing Thing
t :: Parser Term
      Thing -> Parser a
forall a. TermLike a => Thing -> Parser a
maybePostfix (Symbol -> [Term] -> Thing
Apply Symbol
p [Term
arg])

term :: TermLike a => Mode -> Map Symbol Variable -> Parser a
term :: Mode -> Map Symbol Variable -> Parser a
term Mode
mode Map Symbol Variable
ctx = do
  Thing
t <- Mode -> Map Symbol Variable -> Parser Thing
forall a. TermLike a => Mode -> Map Symbol Variable -> Parser a
unary Mode
mode Map Symbol Variable
ctx :: Parser Thing
  let
    binop :: Parser a
binop = do
      Symbol
p <- Parsec ParsecState Symbol
infixOperator
      Term
lhs <- Thing -> Parser Term
forall a. TermLike a => Thing -> Parser a
fromThing Thing
t :: Parser Term
      Term
rhs <- Mode -> Map Symbol Variable -> Parser Term
forall a. TermLike a => Mode -> Map Symbol Variable -> Parser a
unary Mode
mode Map Symbol Variable
ctx :: Parser Term
      Thing -> Parser a
forall a. TermLike a => Thing -> Parser a
fromThing (Symbol -> [Term] -> Thing
Apply Symbol
p [Term
lhs, Term
rhs])
  Parser a
binop Parser a -> Parser a -> Parser a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Thing -> Parser a
forall a. TermLike a => Thing -> Parser a
fromThing Thing
t

postfixOperator :: Parser Symbol
postfixOperator :: Parsec ParsecState Symbol
postfixOperator = do
  Map Symbol [Function]
funcs <- Parser (Map Symbol [Function])
getFunctions
  Punct Punct
p <- (Punct -> Bool) -> Parsec ParsecState Token
forall a. Stream a Token => (Punct -> Bool) -> Parsec a Token
operator (Map Symbol [Function] -> Punct -> Bool
isPostfix Map Symbol [Function]
funcs)
  Symbol -> Parsec ParsecState Symbol
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Symbol
intern (Char
'_'Char -> ShowS
forall a. a -> [a] -> [a]
:Punct -> String
forall a. Show a => a -> String
show Punct
p))

prefixOperator :: Parser Symbol
prefixOperator :: Parsec ParsecState Symbol
prefixOperator = do
  Map Symbol [Function]
funcs <- Parser (Map Symbol [Function])
getFunctions
  Punct Punct
p <- (Punct -> Bool) -> Parsec ParsecState Token
forall a. Stream a Token => (Punct -> Bool) -> Parsec a Token
operator (Bool -> Bool
not (Bool -> Bool) -> (Punct -> Bool) -> Punct -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Symbol [Function] -> Punct -> Bool
isPostfix Map Symbol [Function]
funcs)
  Symbol -> Parsec ParsecState Symbol
forall (m :: * -> *) a. Monad m => a -> m a
return (Punct -> Symbol
showPunct Punct
p)

infixOperator :: Parser Symbol
infixOperator :: Parsec ParsecState Symbol
infixOperator = Parsec ParsecState Symbol
prefixOperator -- we don't syntactically distinguish them

isPostfix :: Map Symbol [Function] -> Punct -> Bool
isPostfix :: Map Symbol [Function] -> Punct -> Bool
isPostfix Map Symbol [Function]
ctx Punct
p = String -> Symbol
intern (Char
'_'Char -> ShowS
forall a. a -> [a] -> [a]
:Punct -> String
forall a. Show a => a -> String
show Punct
p) Symbol -> Map Symbol [Function] -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.member` Map Symbol [Function]
ctx

literal, unitary, quantified, formula ::
  TermLike a => Mode -> Map Symbol Variable -> Parser a
{-# INLINE literal #-}
literal :: Mode -> Map Symbol Variable -> Parser a
literal Mode
mode Map Symbol Variable
ctx = Parser a
true Parser a -> Parser a -> Parser a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser a
false Parser a -> Parser a -> Parser a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser a
binary Parser a -> String -> Parser a
forall a b. Parsec a b -> String -> Parsec a b
<?> String
"literal"
  where {-# INLINE true #-}
        true :: Parser a
true = Parsec ParsecState Form -> Parser a
forall a. TermLike a => Parsec ParsecState Form -> Parser a
parseFormula (Parsec ParsecState Form -> Parser a)
-> Parsec ParsecState Form -> Parser a
forall a b. (a -> b) -> a -> b
$ do { Defined -> Parsec ParsecState Defined
forall a. Stream a Token => Defined -> Parsec a Defined
defined Defined
DTrue; Form -> Parsec ParsecState Form
forall (m :: * -> *) a. Monad m => a -> m a
return ([Form] -> Form
And []) }
        {-# INLINE false #-}
        false :: Parser a
false = Parsec ParsecState Form -> Parser a
forall a. TermLike a => Parsec ParsecState Form -> Parser a
parseFormula (Parsec ParsecState Form -> Parser a)
-> Parsec ParsecState Form -> Parser a
forall a b. (a -> b) -> a -> b
$ do { Defined -> Parsec ParsecState Defined
forall a. Stream a Token => Defined -> Parsec a Defined
defined Defined
DFalse; Form -> Parsec ParsecState Form
forall (m :: * -> *) a. Monad m => a -> m a
return ([Form] -> Form
Or []) }
        binary :: Parser a
binary = do
          Thing
x <- Mode -> Map Symbol Variable -> Parser Thing
forall a. TermLike a => Mode -> Map Symbol Variable -> Parser a
term Mode
mode Map Symbol Variable
ctx :: Parser Thing
          let {-# INLINE f #-}
              f :: Punct -> (Atomic -> Literal) -> Parser a
f Punct
p Atomic -> Literal
sign = Parsec ParsecState Form -> Parser a
forall a. TermLike a => Parsec ParsecState Form -> Parser a
parseFormula (Parsec ParsecState Form -> Parser a)
-> Parsec ParsecState Form -> Parser a
forall a b. (a -> b) -> a -> b
$ do
               Punct -> Parsec ParsecState Token
forall a. Stream a Token => Punct -> Parsec a Token
punct Punct
p
               Term
lhs <- Thing -> Parser Term
forall a. TermLike a => Thing -> Parser a
fromThing Thing
x :: Parser Term
               Term
rhs <- Mode -> Map Symbol Variable -> Parser Term
forall a. TermLike a => Mode -> Map Symbol Variable -> Parser a
term Mode
mode Map Symbol Variable
ctx :: Parser Term
               let form :: Form
form = Literal -> Form
Literal (Literal -> Form) -> (Atomic -> Literal) -> Atomic -> Form
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Atomic -> Literal
sign (Atomic -> Form) -> Atomic -> Form
forall a b. (a -> b) -> a -> b
$ Term
lhs Term -> Term -> Atomic
:=: Term
rhs
               Bool -> Parsec ParsecState () -> Parsec ParsecState ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Term -> Type
forall a. Typed a => a -> Type
typ Term
lhs Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
/= Term -> Type
forall a. Typed a => a -> Type
typ Term
rhs) (Parsec ParsecState () -> Parsec ParsecState ())
-> Parsec ParsecState () -> Parsec ParsecState ()
forall a b. (a -> b) -> a -> b
$
                 String -> Parsec ParsecState ()
forall a c b. Stream a c => String -> Parsec a b
fatalError (String -> Parsec ParsecState ())
-> String -> Parsec ParsecState ()
forall a b. (a -> b) -> a -> b
$ String
"Type mismatch in equality '" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Form -> String
forall a. Pretty a => a -> String
prettyShow (Form -> Form
forall a. Symbolic a => a -> a
prettyNames Form
form) String -> ShowS
forall a. [a] -> [a] -> [a]
++
                              String
"': left hand side has type " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Pretty a => a -> String
prettyShow (Term -> Type
forall a. Typed a => a -> Type
typ Term
lhs) String -> ShowS
forall a. [a] -> [a] -> [a]
++
                              String
" but right hand side has type " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Pretty a => a -> String
prettyShow (Term -> Type
forall a. Typed a => a -> Type
typ Term
rhs)
               Bool -> Parsec ParsecState () -> Parsec ParsecState ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Term -> Type
forall a. Typed a => a -> Type
typ Term
lhs Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
O) (Parsec ParsecState () -> Parsec ParsecState ())
-> Parsec ParsecState () -> Parsec ParsecState ()
forall a b. (a -> b) -> a -> b
$
                 String -> Parsec ParsecState ()
forall a c b. Stream a c => String -> Parsec a b
fatalError (String -> Parsec ParsecState ())
-> String -> Parsec ParsecState ()
forall a b. (a -> b) -> a -> b
$ String
"Type error in equality '" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Form -> String
forall a. Pretty a => a -> String
prettyShow (Form -> Form
forall a. Symbolic a => a -> a
prettyNames Form
form) String -> ShowS
forall a. [a] -> [a] -> [a]
++
                 String
"': can't use equality on predicate (use <=> or <~> instead)"
               Form -> Parsec ParsecState Form
forall (m :: * -> *) a. Monad m => a -> m a
return Form
form
          Punct -> (Atomic -> Literal) -> Parser a
f Punct
Eq Atomic -> Literal
forall a. a -> Signed a
Pos Parser a -> Parser a -> Parser a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Punct -> (Atomic -> Literal) -> Parser a
f Punct
Neq Atomic -> Literal
forall a. a -> Signed a
Neg Parser a -> Parser a -> Parser a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Thing -> Parser a
forall a. TermLike a => Thing -> Parser a
fromThing Thing
x

{-# INLINEABLE unitary #-}
unitary :: Mode -> Map Symbol Variable -> Parser a
unitary Mode
mode Map Symbol Variable
ctx = Parser a
negation Parser a -> Parser a -> Parser a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Mode -> Map Symbol Variable -> Parser a
forall a. TermLike a => Mode -> Map Symbol Variable -> Parser a
quantified Mode
mode Map Symbol Variable
ctx Parser a -> Parser a -> Parser a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Mode -> Map Symbol Variable -> Parser a
forall a. TermLike a => Mode -> Map Symbol Variable -> Parser a
literal Mode
mode Map Symbol Variable
ctx
  where {-# INLINE negation #-}
        negation :: Parser a
negation = Parsec ParsecState Form -> Parser a
forall a. TermLike a => Parsec ParsecState Form -> Parser a
parseFormula (Parsec ParsecState Form -> Parser a)
-> Parsec ParsecState Form -> Parser a
forall a b. (a -> b) -> a -> b
$ do
          Punct -> Parsec ParsecState Token
forall a. Stream a Token => Punct -> Parsec a Token
punct Punct
L.Not
          (Form -> Form)
-> Parsec ParsecState Form -> Parsec ParsecState Form
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Form -> Form
Not (Parsec ParsecState Form -> Parsec ParsecState Form)
-> Parsec ParsecState Form -> Parsec ParsecState Form
forall a b. (a -> b) -> a -> b
$ Mode -> Map Symbol Variable -> Parsec ParsecState Form
forall a. TermLike a => Mode -> Map Symbol Variable -> Parser a
unitary Mode
mode Map Symbol Variable
ctx

{-# INLINE quantified #-}
quantified :: Mode -> Map Symbol Variable -> Parser a
quantified Mode
mode Map Symbol Variable
ctx = Parsec ParsecState Form -> Parser a
forall a. TermLike a => Parsec ParsecState Form -> Parser a
parseFormula (Parsec ParsecState Form -> Parser a)
-> Parsec ParsecState Form -> Parser a
forall a b. (a -> b) -> a -> b
$ do
  Bind Form -> Form
q <- (Punct -> Parsec ParsecState Token
forall a. Stream a Token => Punct -> Parsec a Token
punct Punct
L.ForAll Parsec ParsecState Token
-> Parsec ParsecState (Bind Form -> Form)
-> Parsec ParsecState (Bind Form -> Form)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Bind Form -> Form) -> Parsec ParsecState (Bind Form -> Form)
forall (m :: * -> *) a. Monad m => a -> m a
return Bind Form -> Form
ForAll) Parsec ParsecState (Bind Form -> Form)
-> Parsec ParsecState (Bind Form -> Form)
-> Parsec ParsecState (Bind Form -> Form)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
       (Punct -> Parsec ParsecState Token
forall a. Stream a Token => Punct -> Parsec a Token
punct Punct
L.Exists Parsec ParsecState Token
-> Parsec ParsecState (Bind Form -> Form)
-> Parsec ParsecState (Bind Form -> Form)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Bind Form -> Form) -> Parsec ParsecState (Bind Form -> Form)
forall (m :: * -> *) a. Monad m => a -> m a
return Bind Form -> Form
Exists)
  [Variable]
vars <- Parser [Variable] -> Parser [Variable]
forall a. Parser a -> Parser a
bracks (Parsec ParsecState Variable
-> Parsec ParsecState Token -> Parser [Variable]
forall a b c. Parsec a b -> Parsec a c -> Parsec a [b]
sepBy1 (Mode -> Parsec ParsecState Variable
binder Mode
mode) (Punct -> Parsec ParsecState Token
forall a. Stream a Token => Punct -> Parsec a Token
punct Punct
Comma))
  let ctx' :: Map Symbol Variable
ctx' = (Map Symbol Variable -> Variable -> Map Symbol Variable)
-> Map Symbol Variable -> [Variable] -> Map Symbol Variable
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\Map Symbol Variable
m Variable
v -> Symbol -> Variable -> Map Symbol Variable -> Map Symbol Variable
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (String -> Symbol
intern (Name -> String
forall a. Named a => a -> String
Name.base (Variable -> Name
forall a. Named a => a -> Name
Name.name Variable
v))) Variable
v Map Symbol Variable
m) Map Symbol Variable
ctx [Variable]
vars
  Punct -> Parsec ParsecState Token
forall a. Stream a Token => Punct -> Parsec a Token
punct Punct
Colon
  Form
rest <- Mode -> Map Symbol Variable -> Parsec ParsecState Form
forall a. TermLike a => Mode -> Map Symbol Variable -> Parser a
unitary Mode
mode Map Symbol Variable
ctx' :: Parser Form
  Form -> Parsec ParsecState Form
forall (m :: * -> *) a. Monad m => a -> m a
return (Bind Form -> Form
q (Set Variable -> Form -> Bind Form
forall a. Set Variable -> a -> Bind a
Bind ([Variable] -> Set Variable
forall a. Ord a => [a] -> Set a
Set.fromList [Variable]
vars) Form
rest))

-- A general formula.
{-# INLINEABLE formula #-}
formula :: Mode -> Map Symbol Variable -> Parser a
formula Mode
mode Map Symbol Variable
ctx = do
  Thing
x <- Mode -> Map Symbol Variable -> Parser Thing
forall a. TermLike a => Mode -> Map Symbol Variable -> Parser a
unitary Mode
mode Map Symbol Variable
ctx :: Parser Thing
  let binop :: ([a] -> t) -> a -> a -> t
binop [a] -> t
op a
t a
u = [a] -> t
op [a
t, a
u]
      {-# INLINE connective #-}
      connective :: Punct -> (Form -> Form -> Form) -> Parser a
connective Punct
p Form -> Form -> Form
op = Parsec ParsecState Form -> Parser a
forall a. TermLike a => Parsec ParsecState Form -> Parser a
parseFormula (Parsec ParsecState Form -> Parser a)
-> Parsec ParsecState Form -> Parser a
forall a b. (a -> b) -> a -> b
$ do
        Punct -> Parsec ParsecState Token
forall a. Stream a Token => Punct -> Parsec a Token
punct Punct
p
        Form
lhs <- Thing -> Parsec ParsecState Form
forall a. TermLike a => Thing -> Parser a
fromThing Thing
x
        Form
rhs <- Mode -> Map Symbol Variable -> Parsec ParsecState Form
forall a. TermLike a => Mode -> Map Symbol Variable -> Parser a
formula Mode
mode Map Symbol Variable
ctx :: Parser Form
        Form -> Parsec ParsecState Form
forall (m :: * -> *) a. Monad m => a -> m a
return (Form -> Form -> Form
op Form
lhs Form
rhs)
  Punct -> (Form -> Form -> Form) -> Parser a
connective Punct
L.And (([Form] -> Form) -> Form -> Form -> Form
forall a t. ([a] -> t) -> a -> a -> t
binop [Form] -> Form
And) Parser a -> Parser a -> Parser a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Punct -> (Form -> Form -> Form) -> Parser a
connective Punct
L.Or (([Form] -> Form) -> Form -> Form -> Form
forall a t. ([a] -> t) -> a -> a -> t
binop [Form] -> Form
Or) Parser a -> Parser a -> Parser a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
   Punct -> (Form -> Form -> Form) -> Parser a
connective Punct
Iff Form -> Form -> Form
Equiv Parser a -> Parser a -> Parser a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
   Punct -> (Form -> Form -> Form) -> Parser a
connective Punct
L.Implies (Connective -> Form -> Form -> Form
Connective Connective
Implies) Parser a -> Parser a -> Parser a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
   Punct -> (Form -> Form -> Form) -> Parser a
connective Punct
L.Follows (Connective -> Form -> Form -> Form
Connective Connective
Follows) Parser a -> Parser a -> Parser a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
   Punct -> (Form -> Form -> Form) -> Parser a
connective Punct
L.Xor (Connective -> Form -> Form -> Form
Connective Connective
Xor) Parser a -> Parser a -> Parser a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
   Punct -> (Form -> Form -> Form) -> Parser a
connective Punct
L.Nor (Connective -> Form -> Form -> Form
Connective Connective
Nor) Parser a -> Parser a -> Parser a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
   Punct -> (Form -> Form -> Form) -> Parser a
connective Punct
L.Nand (Connective -> Form -> Form -> Form
Connective Connective
Nand) Parser a -> Parser a -> Parser a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
   Thing -> Parser a
forall a. TermLike a => Thing -> Parser a
fromThing Thing
x

binder :: Mode -> Parser Variable
binder :: Mode -> Parsec ParsecState Variable
binder Mode
NoQuantification =
  String -> Parsec ParsecState Variable
forall a c b. Stream a c => String -> Parsec a b
fatalError String
"Used a quantifier in a CNF clause"
binder Mode
mode = do
  Symbol
x <- Parsec ParsecState Symbol
variable
  Type
ty <- do { Punct -> Parsec ParsecState Token
forall a. Stream a Token => Punct -> Parsec a Token
punct Punct
Colon;
             case Mode
mode of {
               Mode
Typed -> () -> Parsec ParsecState ()
forall (m :: * -> *) a. Monad m => a -> m a
return ();
               Mode
Untyped ->
                 String -> Parsec ParsecState ()
forall a c b. Stream a c => String -> Parsec a b
fatalError String
"Used a typed quantification in an untyped formula" };
             Parser Type
type_ } Parser Type -> Parser Type -> Parser Type
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Type -> Parser Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
indType
  MkState Maybe String
mfile [Input Form]
p Map Symbol Type
t Map Symbol [Function]
f Map Symbol Variable
v Int64
n <- Parsec ParsecState ParseState
forall state a. Parsec (UserState state a) state
getState
  ParseState -> Parsec ParsecState ()
forall state a. state -> Parsec (UserState state a) ()
putState (Maybe String
-> [Input Form]
-> Map Symbol Type
-> Map Symbol [Function]
-> Map Symbol Variable
-> Int64
-> ParseState
MkState Maybe String
mfile [Input Form]
p Map Symbol Type
t Map Symbol [Function]
f Map Symbol Variable
v (Int64
nInt64 -> Int64 -> Int64
forall a. Num a => a -> a -> a
+Int64
1))
  Variable -> Parsec ParsecState Variable
forall (m :: * -> *) a. Monad m => a -> m a
return (Int64 -> Symbol -> Maybe String -> Renamer -> Name
Unique Int64
n Symbol
x Maybe String
forall a. Maybe a
Nothing Renamer
defaultRenamer Name -> Type -> Variable
forall a b. a -> b -> a ::: b
::: Type
ty)

-- Parse a type
type_ :: Parser Type
type_ :: Parser Type
type_ =
  do { Symbol
x <- Parsec ParsecState Symbol
atom; Symbol -> Parser Type
lookupType Symbol
x } Parser Type -> Parser Type -> Parser Type
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
  do { Defined -> Parsec ParsecState Defined
forall a. Stream a Token => Defined -> Parsec a Defined
defined Defined
DI; Type -> Parser Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
indType }

-- A little data type to help with parsing types.
data Type_ = TType | Fun [Type] Type | Prod [Type]

prod :: Type_ -> Type_ -> Parser Type_
prod :: Type_ -> Type_ -> Parser Type_
prod (Prod [Type]
tys) (Prod [Type]
tys2) | Bool -> Bool
not (Type
O Type -> [Type] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Type]
tys [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
tys2) = Type_ -> Parser Type_
forall (m :: * -> *) a. Monad m => a -> m a
return (Type_ -> Parser Type_) -> Type_ -> Parser Type_
forall a b. (a -> b) -> a -> b
$ [Type] -> Type_
Prod ([Type]
tys [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
tys2)
prod Type_
_ Type_
_ = String -> Parser Type_
forall a c b. Stream a c => String -> Parsec a b
fatalError String
"invalid type"

arrow :: Type_ -> Type_ -> Parser Type_
arrow :: Type_ -> Type_ -> Parser Type_
arrow (Prod [Type]
ts) (Prod [Type
x]) = Type_ -> Parser Type_
forall (m :: * -> *) a. Monad m => a -> m a
return (Type_ -> Parser Type_) -> Type_ -> Parser Type_
forall a b. (a -> b) -> a -> b
$ [Type] -> Type -> Type_
Fun [Type]
ts Type
x
arrow Type_
_ Type_
_ = String -> Parser Type_
forall a c b. Stream a c => String -> Parsec a b
fatalError String
"invalid type"

leaf :: Parser Type_
leaf :: Parser Type_
leaf = do { Defined -> Parsec ParsecState Defined
forall a. Stream a Token => Defined -> Parsec a Defined
defined Defined
DTType; Type_ -> Parser Type_
forall (m :: * -> *) a. Monad m => a -> m a
return Type_
TType } Parser Type_ -> Parser Type_ -> Parser Type_
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
       do { Defined -> Parsec ParsecState Defined
forall a. Stream a Token => Defined -> Parsec a Defined
defined Defined
DO; Type_ -> Parser Type_
forall (m :: * -> *) a. Monad m => a -> m a
return ([Type] -> Type_
Prod [Type
O]) } Parser Type_ -> Parser Type_ -> Parser Type_
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
       do { Type
ty <- Parser Type
type_; Type_ -> Parser Type_
forall (m :: * -> *) a. Monad m => a -> m a
return ([Type] -> Type_
Prod [Type
ty]) } Parser Type_ -> Parser Type_ -> Parser Type_
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
       Parser Type_ -> Parser Type_
forall a. Parser a -> Parser a
parens Parser Type_
compoundType

compoundType :: Parser Type_
compoundType :: Parser Type_
compoundType = Parser Type_
leaf Parser Type_
-> Parser (Type_ -> Type_ -> Parser Type_) -> Parser Type_
forall a. Parser a -> Parser (a -> a -> Parser a) -> Parser a
`binExpr` (Punct -> Parsec ParsecState Token
forall a. Stream a Token => Punct -> Parsec a Token
punct Punct
Times Parsec ParsecState Token
-> Parser (Type_ -> Type_ -> Parser Type_)
-> Parser (Type_ -> Type_ -> Parser Type_)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Type_ -> Type_ -> Parser Type_)
-> Parser (Type_ -> Type_ -> Parser Type_)
forall (m :: * -> *) a. Monad m => a -> m a
return Type_ -> Type_ -> Parser Type_
prod)
                    Parser Type_
-> Parser (Type_ -> Type_ -> Parser Type_) -> Parser Type_
forall a. Parser a -> Parser (a -> a -> Parser a) -> Parser a
`binExpr` (Punct -> Parsec ParsecState Token
forall a. Stream a Token => Punct -> Parsec a Token
punct Punct
FunArrow Parsec ParsecState Token
-> Parser (Type_ -> Type_ -> Parser Type_)
-> Parser (Type_ -> Type_ -> Parser Type_)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Type_ -> Type_ -> Parser Type_)
-> Parser (Type_ -> Type_ -> Parser Type_)
forall (m :: * -> *) a. Monad m => a -> m a
return Type_ -> Type_ -> Parser Type_
arrow)

typeDeclaration :: Parser ()
typeDeclaration :: Parsec ParsecState ()
typeDeclaration = do
  Keyword -> Parsec ParsecState Token
forall a. Stream a Token => Keyword -> Parsec a Token
keyword Keyword
L.Type
  Punct -> Parsec ParsecState Token
forall a. Stream a Token => Punct -> Parsec a Token
punct Punct
Comma
  let manyParens :: Parsec ParsecState a -> Parsec ParsecState a
manyParens Parsec ParsecState a
p = Parsec ParsecState a -> Parsec ParsecState a
forall a. Parser a -> Parser a
parens (Parsec ParsecState a -> Parsec ParsecState a
manyParens Parsec ParsecState a
p) Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parsec ParsecState a
p
  Parsec ParsecState () -> Parsec ParsecState ()
forall a. Parser a -> Parser a
manyParens (Parsec ParsecState () -> Parsec ParsecState ())
-> Parsec ParsecState () -> Parsec ParsecState ()
forall a b. (a -> b) -> a -> b
$ do
    Symbol
name <- Parsec ParsecState Symbol
atom
    Punct -> Parsec ParsecState Token
forall a. Stream a Token => Punct -> Parsec a Token
punct Punct
Colon
    Type_
res <- Parser Type_
compoundType
    case Type_
res of
      Type_
TType -> () -> Parsec ParsecState ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      Fun [Type]
args Type
res -> do { Symbol -> FunType -> Parser Function
newFunction Symbol
name ([Type] -> Type -> FunType
FunType [Type]
args Type
res); () -> Parsec ParsecState ()
forall (m :: * -> *) a. Monad m => a -> m a
return () }
      Prod [Type
res] -> do { Symbol -> FunType -> Parser Function
newFunction Symbol
name ([Type] -> Type -> FunType
FunType [] Type
res); () -> Parsec ParsecState ()
forall (m :: * -> *) a. Monad m => a -> m a
return () }
      Type_
_ -> String -> Parsec ParsecState ()
forall a c b. Stream a c => String -> Parsec a b
fatalError String
"invalid type"