{-# 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
data ParseState =
MkState (Maybe String)
![Input Form]
!(Map Symbol Type)
!(Map Symbol [Function])
!(Map Symbol Variable)
!Int64
type Parser = Parsec ParsecState
type ParsecState = UserState ParseState TokenStream
data IncludeStatement = Include String (Maybe [Tag]) deriving Int -> IncludeStatement -> ShowS
[IncludeStatement] -> ShowS
IncludeStatement -> Tag
(Int -> IncludeStatement -> ShowS)
-> (IncludeStatement -> Tag)
-> ([IncludeStatement] -> ShowS)
-> Show IncludeStatement
forall a.
(Int -> a -> ShowS) -> (a -> Tag) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> IncludeStatement -> ShowS
showsPrec :: Int -> IncludeStatement -> ShowS
$cshow :: IncludeStatement -> Tag
show :: IncludeStatement -> Tag
$cshowList :: [IncludeStatement] -> ShowS
showList :: [IncludeStatement] -> ShowS
Show
initialState :: Maybe String -> ParseState
initialState :: Maybe Tag -> ParseState
initialState Maybe Tag
mfile =
Maybe Tag
-> [Name] -> Map Symbol Type -> Map Symbol [Function] -> ParseState
initialStateFrom Maybe Tag
mfile []
([(Symbol, Type)] -> Map Symbol Type
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Tag -> Symbol
intern (Name -> Tag
forall a. Show a => a -> Tag
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
[ (Tag -> Symbol
intern Tag
fun,
[FixedName -> Maybe Tag -> Name
Fixed (Symbol -> Symbol -> FixedName
Overloaded (Tag -> Symbol
intern Tag
fun) (Tag -> Symbol
intern (Name -> Tag
forall a. Show a => a -> Tag
show (Type -> Name
forall a. Named a => a -> Name
name Type
kind)))) Maybe Tag
forall a. Maybe a
Nothing Name -> FunType -> Function
forall a b. a -> b -> a ::: b
::: FunType
ty
| (Type
kind, FunType
ty) <- [(Type, FunType)]
tys ])
| (Tag
fun, [(Type, FunType)]
tys) <- [(Tag, [(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 :: [(Tag, [(Type, FunType)])]
funs =
[Tag] -> (Type -> FunType) -> [(Tag, [(Type, FunType)])]
forall {a} {b}. [a] -> (Type -> b) -> [(a, [(Type, b)])]
fun [Tag
"$less", Tag
"$lesseq", Tag
"$greater", Tag
"$greatereq"]
(\Type
ty -> [Type] -> Type -> FunType
FunType [Type
ty, Type
ty] Type
O) [(Tag, [(Type, FunType)])]
-> [(Tag, [(Type, FunType)])] -> [(Tag, [(Type, FunType)])]
forall a. [a] -> [a] -> [a]
++
[Tag] -> (Type -> FunType) -> [(Tag, [(Type, FunType)])]
forall {a} {b}. [a] -> (Type -> b) -> [(a, [(Type, b)])]
fun [Tag
"$is_int", Tag
"$is_rat"]
(\Type
ty -> [Type] -> Type -> FunType
FunType [Type
ty] Type
O) [(Tag, [(Type, FunType)])]
-> [(Tag, [(Type, FunType)])] -> [(Tag, [(Type, FunType)])]
forall a. [a] -> [a] -> [a]
++
[Tag] -> (Type -> FunType) -> [(Tag, [(Type, FunType)])]
forall {a} {b}. [a] -> (Type -> b) -> [(a, [(Type, b)])]
fun [Tag
"$uminus", Tag
"$floor", Tag
"$ceiling", Tag
"$truncate", Tag
"$round"]
(\Type
ty -> [Type] -> Type -> FunType
FunType [Type
ty] Type
ty) [(Tag, [(Type, FunType)])]
-> [(Tag, [(Type, FunType)])] -> [(Tag, [(Type, FunType)])]
forall a. [a] -> [a] -> [a]
++
[Tag] -> (Type -> FunType) -> [(Tag, [(Type, FunType)])]
forall {a} {b}. [a] -> (Type -> b) -> [(a, [(Type, b)])]
fun [Tag
"$sum", Tag
"$difference", Tag
"$product",
Tag
"$quotient_e", Tag
"$quotient_t", Tag
"$quotient_f",
Tag
"$remainder_e", Tag
"$remainder_t", Tag
"$remainder_f"]
(\Type
ty -> [Type] -> Type -> FunType
FunType [Type
ty, Type
ty] Type
ty) [(Tag, [(Type, FunType)])]
-> [(Tag, [(Type, FunType)])] -> [(Tag, [(Type, FunType)])]
forall a. [a] -> [a] -> [a]
++
[(Tag
"$quotient",
[(Type
ty, [Type] -> Type -> FunType
FunType [Type
ty, Type
ty] Type
ty) | Type
ty <- [Type
ratType, Type
realType]])] [(Tag, [(Type, FunType)])]
-> [(Tag, [(Type, FunType)])] -> [(Tag, [(Type, FunType)])]
forall a. [a] -> [a] -> [a]
++
[Tag] -> (Type -> FunType) -> [(Tag, [(Type, FunType)])]
forall {a} {b}. [a] -> (Type -> b) -> [(a, [(Type, b)])]
fun [Tag
"$to_int"] (\Type
ty -> [Type] -> Type -> FunType
FunType [Type
ty] Type
intType) [(Tag, [(Type, FunType)])]
-> [(Tag, [(Type, FunType)])] -> [(Tag, [(Type, FunType)])]
forall a. [a] -> [a] -> [a]
++
[Tag] -> (Type -> FunType) -> [(Tag, [(Type, FunType)])]
forall {a} {b}. [a] -> (Type -> b) -> [(a, [(Type, b)])]
fun [Tag
"$to_rat"] (\Type
ty -> [Type] -> Type -> FunType
FunType [Type
ty] Type
ratType) [(Tag, [(Type, FunType)])]
-> [(Tag, [(Type, FunType)])] -> [(Tag, [(Type, FunType)])]
forall a. [a] -> [a] -> [a]
++
[Tag] -> (Type -> FunType) -> [(Tag, [(Type, FunType)])]
forall {a} {b}. [a] -> (Type -> b) -> [(a, [(Type, b)])]
fun [Tag
"$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 Tag
-> [Name] -> Map Symbol Type -> Map Symbol [Function] -> ParseState
initialStateFrom Maybe Tag
mfile [Name]
xs Map Symbol Type
tys Map Symbol [Function]
fs = Maybe Tag
-> Problem Form
-> Map Symbol Type
-> Map Symbol [Function]
-> Map Symbol Variable
-> Int64
-> ParseState
MkState Maybe Tag
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 a. Ord a => [a] -> a
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 Tag
_ Renamer
_ <- [Name]
xs])
instance Stream TokenStream Token where
primToken :: forall c.
TokenStream -> (TokenStream -> Token -> c) -> c -> (Tag -> c) -> c
primToken (At Pos
_ (Cons Token
Eof TokenStream
_)) TokenStream -> Token -> c
_ok c
err Tag -> c
_fatal = c
err
primToken (At Pos
_ (Cons Token
L.Error TokenStream
_)) TokenStream -> Token -> c
_ok c
_err Tag -> c
fatal = Tag -> c
fatal Tag
"Lexical error"
primToken (At Pos
_ (Cons Token
t TokenStream
ts)) TokenStream -> Token -> c
ok c
_err Tag -> c
_fatal = TokenStream -> Token -> c
ok TokenStream
ts Token
t
type Position TokenStream = TokenStream
position :: TokenStream -> Position TokenStream
position = TokenStream -> TokenStream
TokenStream -> Position TokenStream
forall a. a -> a
id
data ParseResult a =
ParseFailed Location [String]
| ParseSucceeded a
| ParseStalled Location FilePath (String -> ParseResult a)
deriving (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
$cfmap :: forall a b. (a -> b) -> ParseResult a -> ParseResult b
fmap :: forall a b. (a -> b) -> ParseResult a -> ParseResult b
$c<$ :: forall a b. a -> ParseResult b -> ParseResult a
<$ :: forall a b. a -> ParseResult b -> ParseResult a
Functor
instance Applicative ParseResult where
pure :: forall a. a -> ParseResult a
pure = a -> ParseResult a
forall a. a -> ParseResult a
forall (m :: * -> *) a. Monad m => a -> m a
return
<*> :: forall a b. 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 :: forall a. a -> ParseResult a
return = a -> ParseResult a
forall a. a -> ParseResult a
ParseSucceeded
ParseFailed Location
loc [Tag]
err >>= :: forall a b. ParseResult a -> (a -> ParseResult b) -> ParseResult b
>>= a -> ParseResult b
_ = Location -> [Tag] -> ParseResult b
forall a. Location -> [Tag] -> ParseResult a
ParseFailed Location
loc [Tag]
err
ParseSucceeded a
x >>= a -> ParseResult b
f = a -> ParseResult b
f a
x
ParseStalled Location
loc Tag
name Tag -> ParseResult a
k >>= a -> ParseResult b
f =
Location -> Tag -> (Tag -> ParseResult b) -> ParseResult b
forall a.
Location -> Tag -> (Tag -> ParseResult a) -> ParseResult a
ParseStalled Location
loc Tag
name (\Tag
xs -> Tag -> ParseResult a
k Tag
xs ParseResult a -> (a -> ParseResult b) -> ParseResult b
forall a b. 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 -> Tag
show (Location Tag
file Integer
row Integer
col) =
Tag
file Tag -> ShowS
forall a. [a] -> [a] -> [a]
++ Tag
" (line " Tag -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> Tag
forall a. Show a => a -> Tag
show Integer
row Tag -> ShowS
forall a. [a] -> [a] -> [a]
++ Tag
", column " Tag -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> Tag
forall a. Show a => a -> Tag
show Integer
col Tag -> ShowS
forall a. [a] -> [a] -> [a]
++ Tag
")"
makeLocation :: FilePath -> L.Pos -> Location
makeLocation :: Tag -> Pos -> Location
makeLocation Tag
file (L.Pos Word
row Word
col) =
Tag -> Integer -> Integer -> Location
Location Tag
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 :: Tag -> Tag -> ParseResult (Problem Form)
parseProblem Tag
name Tag
contents = ParseState -> Tag -> Tag -> ParseResult (Problem Form)
parseProblemFrom (Maybe Tag -> ParseState
initialState (Tag -> Maybe Tag
forall a. a -> Maybe a
Just Tag
name)) Tag
name Tag
contents
parseProblemFrom :: ParseState -> FilePath -> String -> ParseResult [Input Form]
parseProblemFrom :: ParseState -> Tag -> Tag -> ParseResult (Problem Form)
parseProblemFrom ParseState
state Tag
name Tag
contents =
(ParseState -> Problem Form)
-> ParseResult ParseState -> ParseResult (Problem Form)
forall a b. (a -> b) -> ParseResult a -> ParseResult b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ParseState -> Problem Form
finalise (ParseResult ParseState -> ParseResult (Problem Form))
-> ParseResult ParseState -> ParseResult (Problem Form)
forall a b. (a -> b) -> a -> b
$
Maybe [Tag] -> Tag -> ParsecState -> ParseResult ParseState
aux Maybe [Tag]
forall a. Maybe a
Nothing Tag
name (ParseState -> TokenStream -> ParsecState
forall state stream. state -> stream -> UserState state stream
UserState ParseState
state (Tag -> TokenStream
scan Tag
contents))
where
aux :: Maybe [Tag] -> FilePath -> ParsecState -> ParseResult ParseState
aux :: Maybe [Tag] -> Tag -> ParsecState -> ParseResult ParseState
aux Maybe [Tag]
tags Tag
name ParsecState
state =
case (Position ParsecState -> [Tag])
-> Parsec ParsecState (Maybe IncludeStatement)
-> ParsecState
-> (Position ParsecState, Either [Tag] (Maybe IncludeStatement))
forall a c b.
Stream a c =>
(Position a -> [Tag])
-> Parsec a b -> a -> (Position a, Either [Tag] b)
run ParsecState -> [Tag]
Position ParsecState -> [Tag]
report ((Tag -> Bool) -> Parsec ParsecState (Maybe IncludeStatement)
section (Maybe [Tag] -> Tag -> Bool
included Maybe [Tag]
tags)) ParsecState
state of
(UserState{userStream :: forall state stream. UserState state stream -> stream
userStream = At Pos
pos Contents
_}, Left [Tag]
err) ->
Location -> [Tag] -> ParseResult ParseState
forall a. Location -> [Tag] -> ParseResult a
ParseFailed (Tag -> Pos -> Location
makeLocation Tag
name Pos
pos) [Tag]
err
(UserState{userState :: forall state stream. UserState state stream -> state
userState = ParseState
state'}, Right Maybe IncludeStatement
Nothing) ->
ParseState -> ParseResult ParseState
forall a. a -> ParseResult a
forall (m :: * -> *) a. Monad m => a -> m a
return ParseState
state'
(UserState ParseState
state (input' :: TokenStream
input'@(At Pos
pos Contents
_)),
Right (Just (Include Tag
name' Maybe [Tag]
tags'))) ->
Location
-> Tag -> (Tag -> ParseResult ParseState) -> ParseResult ParseState
forall a.
Location -> Tag -> (Tag -> ParseResult a) -> ParseResult a
ParseStalled (Tag -> Pos -> Location
makeLocation Tag
name Pos
pos) Tag
name' ((Tag -> ParseResult ParseState) -> ParseResult ParseState)
-> (Tag -> ParseResult ParseState) -> ParseResult ParseState
forall a b. (a -> b) -> a -> b
$ \Tag
input -> do
ParseState
state' <- Maybe [Tag] -> Tag -> ParsecState -> ParseResult ParseState
aux (Maybe [Tag]
tags Maybe [Tag] -> Maybe [Tag] -> Maybe [Tag]
`merge` Maybe [Tag]
tags') Tag
name' (ParseState -> TokenStream -> ParsecState
forall state stream. state -> stream -> UserState state stream
UserState ParseState
state (Tag -> TokenStream
scan Tag
input))
Maybe [Tag] -> Tag -> ParsecState -> ParseResult ParseState
aux Maybe [Tag]
tags Tag
name (ParseState -> TokenStream -> ParsecState
forall state stream. state -> stream -> UserState state stream
UserState ParseState
state' TokenStream
input')
report :: ParsecState -> [String]
report :: ParsecState -> [Tag]
report UserState{userStream :: forall state stream. UserState state stream -> stream
userStream = At Pos
_ (Cons Token
Eof TokenStream
_)} =
[Tag
"Unexpected end of file"]
report UserState{userStream :: forall state stream. UserState state stream -> stream
userStream = At Pos
_ (Cons Token
L.Error TokenStream
_)} =
[Tag
"Lexical error"]
report UserState{userStream :: forall state stream. UserState state stream -> stream
userStream = At Pos
_ (Cons Token
t TokenStream
_)} =
[Tag
"Unexpected " Tag -> ShowS
forall a. [a] -> [a] -> [a]
++ Token -> Tag
forall a. Show a => a -> Tag
show Token
t]
included :: Maybe [Tag] -> Tag -> Bool
included :: Maybe [Tag] -> Tag -> Bool
included Maybe [Tag]
Nothing Tag
_ = Bool
True
included (Just [Tag]
xs) Tag
x = Tag
x Tag -> [Tag] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Tag]
xs
merge :: Maybe [Tag] -> Maybe [Tag] -> Maybe [Tag]
merge :: Maybe [Tag] -> Maybe [Tag] -> Maybe [Tag]
merge Maybe [Tag]
Nothing Maybe [Tag]
x = Maybe [Tag]
x
merge Maybe [Tag]
x Maybe [Tag]
Nothing = Maybe [Tag]
x
merge (Just [Tag]
xs) (Just [Tag]
ys) = [Tag] -> Maybe [Tag]
forall a. a -> Maybe a
Just ([Tag]
xs [Tag] -> [Tag] -> [Tag]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` [Tag]
ys)
finalise :: ParseState -> Problem Form
finalise :: ParseState -> Problem Form
finalise (MkState Maybe Tag
_ Problem Form
p Map Symbol Type
_ Map Symbol [Function]
_ Map Symbol Variable
_ Int64
_) = Problem Form -> Problem Form
forall a. Symbolic a => a -> a
check (Problem Form -> Problem Form
forall a. [a] -> [a]
reverse Problem Form
p)
testParser :: Parser a -> String -> Either [String] a
testParser :: forall a. Parser a -> Tag -> Either [Tag] a
testParser Parser a
p Tag
s = (ParsecState, Either [Tag] a) -> Either [Tag] a
forall a b. (a, b) -> b
snd ((Position ParsecState -> [Tag])
-> Parser a
-> ParsecState
-> (Position ParsecState, Either [Tag] a)
forall a c b.
Stream a c =>
(Position a -> [Tag])
-> Parsec a b -> a -> (Position a, Either [Tag] b)
run ([Tag] -> ParsecState -> [Tag]
forall a b. a -> b -> a
const []) Parser a
p (ParseState -> TokenStream -> ParsecState
forall state stream. state -> stream -> UserState state stream
UserState (Maybe Tag -> ParseState
initialState Maybe Tag
forall a. Maybe a
Nothing) (Tag -> TokenStream
scan Tag
s)))
{-# 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 -> Tag -> Parsec a Token
forall a b. Parsec a b -> Tag -> Parsec a b
<?> Tag
"'" Tag -> ShowS
forall a. [a] -> [a] -> [a]
++ Keyword -> Tag
forall a. Show a => a -> Tag
show Keyword
k Tag -> ShowS
forall a. [a] -> [a] -> [a]
++ Tag
"'"
{-# 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 -> Tag -> Parsec a Token
forall a b. Parsec a b -> Tag -> Parsec a b
<?> Tag
"'" Tag -> ShowS
forall a. [a] -> [a] -> [a]
++ Punct -> Tag
forall a. Show a => a -> Tag
show Punct
k Tag -> ShowS
forall a. [a] -> [a] -> [a]
++ Tag
"'"
{-# 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 -> Tag -> Parsec a Token
forall a b. Parsec a b -> Tag -> Parsec a b
<?> Tag
"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 a b. (a -> b) -> Parsec a a -> Parsec a b
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 -> Tag -> Parsec a Defined
forall a b. Parsec a b -> Tag -> Parsec a b
<?> Tag
"'" Tag -> ShowS
forall a. [a] -> [a] -> [a]
++ Defined -> Tag
forall a. Show a => a -> Tag
show Defined
k Tag -> ShowS
forall a. [a] -> [a] -> [a]
++ Tag
"'"
{-# INLINE variable #-}
variable :: Parsec ParsecState Symbol
variable = (Token -> Symbol)
-> Parsec ParsecState Token -> Parsec ParsecState Symbol
forall a b.
(a -> b) -> Parsec ParsecState a -> Parsec ParsecState b
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 -> Tag -> Parsec ParsecState Symbol
forall a b. Parsec a b -> Tag -> Parsec a b
<?> Tag
"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 a b.
(a -> b) -> Parsec ParsecState a -> Parsec ParsecState b
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 -> Tag -> Parsec ParsecState Integer
forall a b. Parsec a b -> Tag -> Parsec a b
<?> Tag
"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 a b.
(a -> b) -> Parsec ParsecState a -> Parsec ParsecState b
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 a b.
(a -> b) -> Parsec ParsecState a -> Parsec ParsecState b
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 a b.
(a -> b) -> Parsec ParsecState a -> Parsec ParsecState b
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 -> Tag -> Parsec ParsecState Symbol
forall a b. Parsec a b -> Tag -> Parsec a b
<?> Tag
"atom"
parens, bracks :: Parser a -> Parser a
{-# INLINE parens #-}
parens :: forall a. 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 :: forall a. 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
binExpr :: Parser a -> Parser (a -> a -> Parser a) -> Parser a
binExpr :: forall a. 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 a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> a -> Parser a
forall a. a -> Parsec ParsecState a
forall (m :: * -> *) a. Monad m => a -> m a
return a
lhs
section :: (Tag -> Bool) -> Parser (Maybe IncludeStatement)
section :: (Tag -> Bool) -> Parsec ParsecState (Maybe IncludeStatement)
section Tag -> Bool
included = Parsec ParsecState () -> Parsec ParsecState ()
forall a b. Parsec a b -> Parsec a ()
skipMany ((Tag -> Bool) -> Parsec ParsecState ()
input Tag -> Bool
included) Parsec ParsecState ()
-> Parsec ParsecState (Maybe IncludeStatement)
-> Parsec ParsecState (Maybe IncludeStatement)
forall a b.
Parsec ParsecState a
-> Parsec ParsecState b -> Parsec ParsecState b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ((IncludeStatement -> Maybe IncludeStatement)
-> Parsec ParsecState IncludeStatement
-> Parsec ParsecState (Maybe IncludeStatement)
forall a b.
(a -> b) -> Parsec ParsecState a -> Parsec ParsecState b
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 a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState a
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 a b.
Parsec ParsecState a
-> Parsec ParsecState b -> Parsec ParsecState b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe IncludeStatement
-> Parsec ParsecState (Maybe IncludeStatement)
forall a. a -> Parsec ParsecState a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe IncludeStatement
forall a. Maybe a
Nothing))
input :: (Tag -> Bool) -> Parser ()
input :: (Tag -> Bool) -> Parsec ParsecState ()
input Tag -> Bool
included = Keyword -> (Tag -> Parsec ParsecState ()) -> Parsec ParsecState ()
declaration Keyword
Cnf (Parsec ParsecState Form -> Tag -> Parsec ParsecState ()
formulaIn Parsec ParsecState Form
cnf) Parsec ParsecState ()
-> Parsec ParsecState () -> Parsec ParsecState ()
forall a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
Keyword -> (Tag -> Parsec ParsecState ()) -> Parsec ParsecState ()
declaration Keyword
Fof (Parsec ParsecState Form -> Tag -> Parsec ParsecState ()
formulaIn Parsec ParsecState Form
fof) Parsec ParsecState ()
-> Parsec ParsecState () -> Parsec ParsecState ()
forall a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
Keyword -> (Tag -> Parsec ParsecState ()) -> Parsec ParsecState ()
declaration Keyword
Tff (\Tag
tag -> Parsec ParsecState Form -> Tag -> Parsec ParsecState ()
formulaIn Parsec ParsecState Form
tff Tag
tag Parsec ParsecState ()
-> Parsec ParsecState () -> Parsec ParsecState ()
forall a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parsec ParsecState ()
typeDeclaration) Parsec ParsecState ()
-> Parsec ParsecState () -> Parsec ParsecState ()
forall a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
Keyword -> (Tag -> Parsec ParsecState ()) -> Parsec ParsecState ()
declaration Keyword
Tcf (\Tag
tag -> Parsec ParsecState Form -> Tag -> Parsec ParsecState ()
formulaIn Parsec ParsecState Form
tff Tag
tag Parsec ParsecState ()
-> Parsec ParsecState () -> Parsec ParsecState ()
forall a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parsec ParsecState ()
typeDeclaration)
where {-# INLINE declaration #-}
declaration :: Keyword -> (Tag -> Parsec ParsecState ()) -> Parsec ParsecState ()
declaration Keyword
k Tag -> 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
Tag
t <- Parser Tag
tag
Punct -> Parsec ParsecState Token
forall {a}. Stream a Token => Punct -> Parsec a Token
punct Punct
Comma
if Tag -> Bool
included Tag
t then Tag -> Parsec ParsecState ()
m Tag
t else Parsec ParsecState ()
balancedParens
Punct -> Parsec ParsecState Token
forall {a}. Stream a Token => Punct -> Parsec a Token
punct Punct
Dot
() -> Parsec ParsecState ()
forall a. a -> Parsec ParsecState a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
formulaIn :: Parsec ParsecState Form -> Tag -> Parsec ParsecState ()
formulaIn Parsec ParsecState Form
lang Tag
tag = do
Tag -> Form -> Input Form
k <- Parser (Tag -> 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 (Tag -> Form -> Input Form
k Tag
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 a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState a
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 a b.
Parsec ParsecState a
-> Parsec ParsecState b -> Parsec ParsecState b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> () -> Parsec ParsecState ()
forall a. a -> Parsec ParsecState a
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
kind :: Parser (Tag -> Form -> Input Form)
kind :: Parser (Tag -> Form -> Input Form)
kind = do
MkState Maybe Tag
mfile Problem 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
Parsec ParsecState (Position ParsecState)
forall a b. Stream a b => Parsec a (Position a)
getPosition
let
general :: Keyword -> Kind -> Parser (Tag -> 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 (Tag -> Form -> Input Form)
-> Parser (Tag -> Form -> Input Form)
forall a b.
Parsec ParsecState a
-> Parsec ParsecState b -> Parsec ParsecState b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Tag -> Form -> Input Form) -> Parser (Tag -> Form -> Input Form)
forall a. a -> Parsec ParsecState a
forall (m :: * -> *) a. Monad m => a -> m a
return (Kind -> Tag -> Form -> Input Form
mk Kind
kind)
axiom :: Keyword -> AxKind -> Parser (Tag -> Form -> Input Form)
axiom Keyword
t AxKind
kind = Keyword -> Kind -> Parser (Tag -> Form -> Input Form)
general Keyword
t (AxKind -> Kind
Form.Ax AxKind
kind)
conjecture :: Keyword -> ConjKind -> Parser (Tag -> Form -> Input Form)
conjecture Keyword
t ConjKind
kind = Keyword -> Kind -> Parser (Tag -> Form -> Input Form)
general Keyword
t (ConjKind -> Kind
Form.Conj ConjKind
kind)
mk :: Kind -> Tag -> Form -> Input Form
mk Kind
kind Tag
tag Form
form =
Input { tag :: Tag
Form.tag = Tag
tag,
kind :: Kind
Form.kind = Kind
kind,
what :: Form
Form.what = Form
form,
source :: InputSource
Form.source =
case Maybe Tag
mfile of
Maybe Tag
Nothing -> InputSource
Form.Unknown
Just Tag
file -> Tag -> Int -> InputSource
FromFile Tag
file (Word -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word
n) }
Keyword -> AxKind -> Parser (Tag -> Form -> Input Form)
axiom Keyword
L.Axiom AxKind
Axiom Parser (Tag -> Form -> Input Form)
-> Parser (Tag -> Form -> Input Form)
-> Parser (Tag -> Form -> Input Form)
forall a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
Keyword -> AxKind -> Parser (Tag -> Form -> Input Form)
axiom Keyword
L.Hypothesis AxKind
Hypothesis Parser (Tag -> Form -> Input Form)
-> Parser (Tag -> Form -> Input Form)
-> Parser (Tag -> Form -> Input Form)
forall a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
Keyword -> AxKind -> Parser (Tag -> Form -> Input Form)
axiom Keyword
L.Definition AxKind
Definition Parser (Tag -> Form -> Input Form)
-> Parser (Tag -> Form -> Input Form)
-> Parser (Tag -> Form -> Input Form)
forall a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
Keyword -> AxKind -> Parser (Tag -> Form -> Input Form)
axiom Keyword
L.Assumption AxKind
Assumption Parser (Tag -> Form -> Input Form)
-> Parser (Tag -> Form -> Input Form)
-> Parser (Tag -> Form -> Input Form)
forall a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
Keyword -> AxKind -> Parser (Tag -> Form -> Input Form)
axiom Keyword
L.Lemma AxKind
Lemma Parser (Tag -> Form -> Input Form)
-> Parser (Tag -> Form -> Input Form)
-> Parser (Tag -> Form -> Input Form)
forall a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
Keyword -> AxKind -> Parser (Tag -> Form -> Input Form)
axiom Keyword
L.Theorem AxKind
TheoremKind Parser (Tag -> Form -> Input Form)
-> Parser (Tag -> Form -> Input Form)
-> Parser (Tag -> Form -> Input Form)
forall a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
Keyword -> AxKind -> Parser (Tag -> Form -> Input Form)
axiom Keyword
L.NegatedConjecture AxKind
NegatedConjecture Parser (Tag -> Form -> Input Form)
-> Parser (Tag -> Form -> Input Form)
-> Parser (Tag -> Form -> Input Form)
forall a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
Keyword -> ConjKind -> Parser (Tag -> Form -> Input Form)
conjecture Keyword
L.Conjecture ConjKind
Conjecture Parser (Tag -> Form -> Input Form)
-> Parser (Tag -> Form -> Input Form)
-> Parser (Tag -> Form -> Input Form)
forall a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
Keyword -> ConjKind -> Parser (Tag -> Form -> Input Form)
conjecture Keyword
L.Question ConjKind
Question
tag :: Parser Tag
tag :: Parser Tag
tag = (Symbol -> Tag) -> Parsec ParsecState Symbol -> Parser Tag
forall a b.
(a -> b) -> Parsec ParsecState a -> Parsec ParsecState b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Symbol -> Tag
unintern Parsec ParsecState Symbol
atom Parser Tag -> Parser Tag -> Parser Tag
forall a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Integer -> Tag) -> Parsec ParsecState Integer -> Parser Tag
forall a b.
(a -> b) -> Parsec ParsecState a -> Parsec ParsecState b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Integer -> Tag
forall a. Show a => a -> Tag
show Parsec ParsecState Integer
number Parser Tag -> Tag -> Parser Tag
forall a b. Parsec a b -> Tag -> Parsec a b
<?> Tag
"clause name"
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 -> Tag -> Parsec ParsecState Symbol
forall a b. Parsec a b -> Tag -> Parsec a b
<?> Tag
"quoted filename"
Maybe [Tag]
clauses <- do { Punct -> Parsec ParsecState Token
forall {a}. Stream a Token => Punct -> Parsec a Token
punct Punct
Comma
; ([Tag] -> Maybe [Tag])
-> Parsec ParsecState [Tag] -> Parsec ParsecState (Maybe [Tag])
forall a b.
(a -> b) -> Parsec ParsecState a -> Parsec ParsecState b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Tag] -> Maybe [Tag]
forall a. a -> Maybe a
Just (Parsec ParsecState [Tag] -> Parsec ParsecState [Tag]
forall a. Parser a -> Parser a
bracks (Parser Tag -> Parsec ParsecState Token -> Parsec ParsecState [Tag]
forall a b c. Parsec a b -> Parsec a c -> Parsec a [b]
sepBy1 Parser Tag
tag (Punct -> Parsec ParsecState Token
forall {a}. Stream a Token => Punct -> Parsec a Token
punct Punct
Comma))) } Parsec ParsecState (Maybe [Tag])
-> Parsec ParsecState (Maybe [Tag])
-> Parsec ParsecState (Maybe [Tag])
forall a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Maybe [Tag] -> Parsec ParsecState (Maybe [Tag])
forall a. a -> Parsec ParsecState a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe [Tag]
forall a. Maybe a
Nothing
IncludeStatement -> Parsec ParsecState IncludeStatement
forall a. a -> Parsec ParsecState a
forall (m :: * -> *) a. Monad m => a -> m a
return (Tag -> Maybe [Tag] -> IncludeStatement
Include (Symbol -> Tag
unintern Symbol
name) Maybe [Tag]
clauses)
Punct -> Parsec ParsecState Token
forall {a}. Stream a Token => Punct -> Parsec a Token
punct Punct
Dot
IncludeStatement -> Parsec ParsecState IncludeStatement
forall a. a -> Parsec ParsecState a
forall (m :: * -> *) a. Monad m => a -> m a
return IncludeStatement
res
newFormula :: Input Form -> Parser ()
newFormula :: Input Form -> Parsec ParsecState ()
newFormula Input Form
input = do
MkState Maybe Tag
mfile Problem 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 Tag
-> Problem Form
-> Map Symbol Type
-> Map Symbol [Function]
-> Map Symbol Variable
-> Int64
-> ParseState
MkState Maybe Tag
mfile (Input Form
inputInput Form -> Problem Form -> Problem Form
forall a. a -> [a] -> [a]
:Problem 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
[] ->
Tag -> Parser Function
forall a c b. Stream a c => Tag -> Parsec a b
fatalError (Tag -> Parser Function) -> Tag -> Parser Function
forall a b. (a -> b) -> a -> b
$ Tag
"Constant " Tag -> ShowS
forall a. [a] -> [a] -> [a]
++ Symbol -> Tag
unintern Symbol
name Tag -> ShowS
forall a. [a] -> [a] -> [a]
++
Tag
" was declared to have type " Tag -> ShowS
forall a. [a] -> [a] -> [a]
++ FunType -> Tag
forall a. Pretty a => a -> Tag
prettyShow FunType
ty Tag -> ShowS
forall a. [a] -> [a] -> [a]
++
Tag
" but already has type " Tag -> ShowS
forall a. [a] -> [a] -> [a]
++ [FunType] -> Tag
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 a. a -> Parsec ParsecState a
forall (m :: * -> *) a. Monad m => a -> m a
return Function
f
showTypes :: [FunType] -> String
showTypes :: [FunType] -> Tag
showTypes = Tag -> [Tag] -> Tag
forall a. [a] -> [[a]] -> [a]
intercalate Tag
" and " ([Tag] -> Tag) -> ([FunType] -> [Tag]) -> [FunType] -> Tag
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FunType -> Tag) -> [FunType] -> [Tag]
forall a b. (a -> b) -> [a] -> [b]
map FunType -> Tag
forall a. Pretty a => a -> Tag
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 a. [a] -> 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 a. a -> Parsec ParsecState a
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 a. [a] -> 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)
Tag -> Parsec a b
forall a c b. Stream a c => Tag -> Parsec a b
fatalError (Tag -> Parsec a b) -> Tag -> Parsec a b
forall a b. (a -> b) -> a -> b
$ Tag
"Type mismatch in term '" Tag -> ShowS
forall a. [a] -> [a] -> [a]
++ Term -> Tag
forall a. Pretty a => a -> Tag
prettyShow (Term -> Term
forall a. Symbolic a => a -> a
prettyNames (Function
f Function -> [Term] -> Term
:@: [Term]
args')) Tag -> ShowS
forall a. [a] -> [a] -> [a]
++ Tag
"': " Tag -> ShowS
forall a. [a] -> [a] -> [a]
++
Tag
"Constant " Tag -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> Tag
forall a. Pretty a => a -> Tag
prettyShow Name
x Tag -> ShowS
forall a. [a] -> [a] -> [a]
++
if [Int] -> Int
forall a. [a] -> 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 a. [a] -> 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
Tag
" has arity " Tag -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> Tag
forall a. Show a => a -> Tag
show ([Int] -> Int
forall a. HasCallStack => [a] -> a
head [Int]
lengths) Tag -> ShowS
forall a. [a] -> [a] -> [a]
++
Tag
" but was applied to " Tag -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> Tag
forall a. Show a => a -> Tag
show ([Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
args') Tag -> ShowS
forall a. [a] -> [a] -> [a]
++
Int -> Tag -> ShowS
forall {a} {p}. (Eq a, Num a) => a -> p -> p -> p
plural ([Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
args') Tag
" argument" Tag
" arguments"
else
Tag
" has type " Tag -> ShowS
forall a. [a] -> [a] -> [a]
++ [FunType] -> Tag
showTypes ((Function -> FunType) -> [Function] -> [FunType]
forall a b. (a -> b) -> [a] -> [b]
map Function -> FunType
forall a b. (a ::: b) -> b
rhs [Function]
fs) Tag -> ShowS
forall a. [a] -> [a] -> [a]
++
Tag
" but was applied to " Tag -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> Tag -> ShowS
forall {a} {p}. (Eq a, Num a) => a -> p -> p -> p
plural ([Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
args') Tag
"an argument" Tag
"arguments" Tag -> ShowS
forall a. [a] -> [a] -> [a]
++
Tag
" of type " Tag -> ShowS
forall a. [a] -> [a] -> [a]
++ Tag -> [Tag] -> Tag
forall a. [a] -> [[a]] -> [a]
intercalate Tag
", " ((Term -> Tag) -> [Term] -> [Tag]
forall a b. (a -> b) -> [a] -> [b]
map (Type -> Tag
forall a. Pretty a => a -> Tag
prettyShow (Type -> Tag) -> (Term -> Type) -> Term -> Tag
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 Tag
mfile Problem 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 Tag
-> Problem Form
-> Map Symbol Type
-> Map Symbol [Function]
-> Map Symbol Variable
-> Int64
-> ParseState
MkState Maybe Tag
mfile Problem 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 a. a -> Parsec ParsecState a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty
Just Type
ty -> Type -> Parser Type
forall a. a -> Parsec ParsecState a
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 Tag
mfile Problem 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 Tag
-> Problem Form
-> Map Symbol Type
-> Map Symbol [Function]
-> Map Symbol Variable
-> Int64
-> ParseState
MkState Maybe Tag
mfile Problem 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 a. a -> Parsec ParsecState a
forall (m :: * -> *) a. Monad m => a -> m a
return [Function
decl]
Just [Function]
fs -> [Function] -> Parser [Function]
forall a. a -> Parsec ParsecState a
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 Tag
_ Problem 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 a. a -> Parsec ParsecState a
forall (m :: * -> *) a. Monad m => a -> m a
return Map Symbol [Function]
f
cnf, tff, fof :: Parser Form
cnf :: Parsec ParsecState Form
cnf = do
MkState Maybe Tag
mfile Problem 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 Tag
-> Problem Form
-> Map Symbol Type
-> Map Symbol [Function]
-> Map Symbol Variable
-> Int64
-> ParseState
MkState Maybe Tag
mfile Problem 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 a. a -> Parsec ParsecState a
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
data Thing = Apply !Symbol ![Term]
| Term !Term
| Formula !Form
instance Show Thing where
show :: Thing -> Tag
show (Apply Symbol
f []) = Symbol -> Tag
unintern Symbol
f
show (Apply Symbol
f [Term]
args) =
Symbol -> Tag
unintern Symbol
f Tag -> ShowS
forall a. [a] -> [a] -> [a]
++
case [Term]
args of
[] -> Tag
""
[Term]
args -> [Term] -> Tag
forall a. Pretty a => a -> Tag
prettyShow [Term]
args
show (Term Term
t) = Term -> Tag
forall a. Pretty a => a -> Tag
prettyShow Term
t
show (Formula Form
f) = Form -> Tag
forall a. Pretty a => a -> Tag
prettyShow Form
f
class TermLike a where
fromThing :: Thing -> Parser a
var :: Mode -> Map Symbol Variable -> Parser a
parseFormula :: Parser Form -> Parser a
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 a b.
(a -> b) -> Parsec ParsecState a -> Parsec ParsecState b
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 a. Parsec ParsecState a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
fromThing (Formula Form
f) = Form -> Parsec ParsecState Form
forall a. a -> Parsec ParsecState a
forall (m :: * -> *) a. Monad m => a -> m a
return Form
f
var :: Mode -> Map Symbol Variable -> Parsec ParsecState Form
var Mode
_ Map Symbol Variable
_ = Parsec ParsecState Form
forall a. Parsec ParsecState a
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 a. a -> Parsec ParsecState a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t
fromThing (Formula Form
_) = Parser Term
forall a. Parsec ParsecState a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
parseFormula :: Parsec ParsecState Form -> Parser Term
parseFormula Parsec ParsecState Form
_ = Parser Term
forall a. Parsec ParsecState a
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 Tag
mfile Problem 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 a. a -> Parsec ParsecState a
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 Tag -> Renamer -> Name
Unique (Int64
nInt64 -> Int64 -> Int64
forall a. Num a => a -> a -> a
+Int64
1) Symbol
x Maybe Tag
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 Tag
-> Problem Form
-> Map Symbol Type
-> Map Symbol [Function]
-> Map Symbol Variable
-> Int64
-> ParseState
MkState Maybe Tag
mfile Problem 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 a. a -> Parsec ParsecState a
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 a. a -> Parsec ParsecState a
forall (m :: * -> *) a. Monad m => a -> m a
return (Variable -> Term
Var Variable
v)
Maybe Variable
Nothing -> Tag -> Parser Term
forall a c b. Stream a c => Tag -> Parsec a b
fatalError (Tag -> Parser Term) -> Tag -> Parser Term
forall a b. (a -> b) -> a -> b
$ Tag
"unbound variable " Tag -> ShowS
forall a. [a] -> [a] -> [a]
++ Symbol -> Tag
unintern Symbol
x
instance TermLike Thing where
fromThing :: Thing -> Parser Thing
fromThing = Thing -> Parser Thing
forall a. a -> Parsec ParsecState a
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 a b.
(a -> b) -> Parsec ParsecState a -> Parsec ParsecState b
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 a b.
(a -> b) -> Parsec ParsecState a -> Parsec ParsecState b
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
{-# INLINEABLE atomic #-}
atomic :: TermLike a => Mode -> Map Symbol Variable -> Parser a
atomic :: forall a. TermLike a => Mode -> Map Symbol Variable -> Parser a
atomic Mode
mode Map Symbol Variable
ctx = Parsec ParsecState a
function Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState a
forall a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Mode -> Map Symbol Variable -> Parsec ParsecState a
forall a. TermLike a => Mode -> Map Symbol Variable -> Parser a
var Mode
mode Map Symbol Variable
ctx Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState a
forall a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parsec ParsecState a
num Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState a
forall a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parsec ParsecState a -> Parsec ParsecState a
forall a. Parser a -> Parser a
parens (Mode -> Map Symbol Variable -> Parsec ParsecState a
forall a. TermLike a => Mode -> Map Symbol Variable -> Parser a
parser Mode
mode Map Symbol Variable
ctx)
where
{-# INLINE function #-}
function :: Parsec ParsecState 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 a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Term] -> Parser [Term]
forall a. a -> Parsec ParsecState a
forall (m :: * -> *) a. Monad m => a -> m a
return []
Thing -> Parsec ParsecState a
forall a. TermLike a => Thing -> Parser a
fromThing (Symbol -> [Term] -> Thing
Apply Symbol
x [Term]
args)
{-# INLINE num #-}
num :: Parsec ParsecState a
num = (Parsec ParsecState a
int Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState a
forall a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parsec ParsecState a
rat Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState a
forall a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parsec ParsecState a
real)
{-# INLINE int #-}
int :: Parsec ParsecState a
int = do
Integer
n <- Parsec ParsecState Integer
number
FixedName -> Type -> Parsec ParsecState a
forall {a}. TermLike a => FixedName -> Type -> Parser a
constant (Integer -> FixedName
Integer Integer
n) Type
intType
{-# INLINE rat #-}
rat :: Parsec ParsecState a
rat = do
Rational
x <- Parsec ParsecState Rational
ratNumber
FixedName -> Type -> Parsec ParsecState a
forall {a}. TermLike a => FixedName -> Type -> Parser a
constant (Rational -> FixedName
Rational Rational
x) Type
ratType
{-# INLINE real #-}
real :: Parsec ParsecState a
real = do
Rational
x <- Parsec ParsecState Rational
realNumber
FixedName -> Type -> Parsec ParsecState 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 Tag -> Name
Fixed FixedName
x Maybe Tag
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 :: forall a. TermLike a => 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 a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState 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 :: forall a. TermLike a => 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 a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState a
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 :: forall a. TermLike a => 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 a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState 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 :: forall a. TermLike a => 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 :: forall a. TermLike a => 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 a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState 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 a. a -> Parsec ParsecState a
forall (m :: * -> *) a. Monad m => a -> m a
return (Tag -> Symbol
intern (Char
'_'Char -> ShowS
forall a. a -> [a] -> [a]
:Punct -> Tag
forall a. Show a => a -> Tag
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 a. a -> Parsec ParsecState a
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
isPostfix :: Map Symbol [Function] -> Punct -> Bool
isPostfix :: Map Symbol [Function] -> Punct -> Bool
isPostfix Map Symbol [Function]
ctx Punct
p = Tag -> Symbol
intern (Char
'_'Char -> ShowS
forall a. a -> [a] -> [a]
:Punct -> Tag
forall a. Show a => a -> Tag
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 :: forall a. TermLike a => Mode -> Map Symbol Variable -> Parser a
literal Mode
mode Map Symbol Variable
ctx = Parser a
true Parser a -> Parser a -> Parser a
forall a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser a
false Parser a -> Parser a -> Parser a
forall a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser a
binary Parser a -> Tag -> Parser a
forall a b. Parsec a b -> Tag -> Parsec a b
<?> Tag
"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 a. a -> Parsec ParsecState a
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 a. a -> Parsec ParsecState a
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
$
Tag -> Parsec ParsecState ()
forall a c b. Stream a c => Tag -> Parsec a b
fatalError (Tag -> Parsec ParsecState ()) -> Tag -> Parsec ParsecState ()
forall a b. (a -> b) -> a -> b
$ Tag
"Type mismatch in equality '" Tag -> ShowS
forall a. [a] -> [a] -> [a]
++ Form -> Tag
forall a. Pretty a => a -> Tag
prettyShow (Form -> Form
forall a. Symbolic a => a -> a
prettyNames Form
form) Tag -> ShowS
forall a. [a] -> [a] -> [a]
++
Tag
"': left hand side has type " Tag -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> Tag
forall a. Pretty a => a -> Tag
prettyShow (Term -> Type
forall a. Typed a => a -> Type
typ Term
lhs) Tag -> ShowS
forall a. [a] -> [a] -> [a]
++
Tag
" but right hand side has type " Tag -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> Tag
forall a. Pretty a => a -> Tag
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
$
Tag -> Parsec ParsecState ()
forall a c b. Stream a c => Tag -> Parsec a b
fatalError (Tag -> Parsec ParsecState ()) -> Tag -> Parsec ParsecState ()
forall a b. (a -> b) -> a -> b
$ Tag
"Type error in equality '" Tag -> ShowS
forall a. [a] -> [a] -> [a]
++ Form -> Tag
forall a. Pretty a => a -> Tag
prettyShow (Form -> Form
forall a. Symbolic a => a -> a
prettyNames Form
form) Tag -> ShowS
forall a. [a] -> [a] -> [a]
++
Tag
"': can't use equality on predicate (use <=> or <~> instead)"
Form -> Parsec ParsecState Form
forall a. a -> Parsec ParsecState a
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 a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState 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 a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState 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 :: forall a. TermLike a => Mode -> Map Symbol Variable -> Parser a
unitary Mode
mode Map Symbol Variable
ctx = Parser a
negation Parser a -> Parser a -> Parser a
forall a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState 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 a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState 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 a b.
(a -> b) -> Parsec ParsecState a -> Parsec ParsecState b
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 :: forall a. TermLike a => 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 a b.
Parsec ParsecState a
-> Parsec ParsecState b -> Parsec ParsecState b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Bind Form -> Form) -> Parsec ParsecState (Bind Form -> Form)
forall a. a -> Parsec ParsecState a
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 a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState a
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 a b.
Parsec ParsecState a
-> Parsec ParsecState b -> Parsec ParsecState b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Bind Form -> Form) -> Parsec ParsecState (Bind Form -> Form)
forall a. a -> Parsec ParsecState a
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 b a. (b -> a -> b) -> b -> [a] -> b
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 (Tag -> Symbol
intern (Name -> Tag
forall a. Named a => a -> Tag
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 a. a -> Parsec ParsecState a
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))
{-# INLINEABLE formula #-}
formula :: forall a. TermLike a => 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 a. a -> Parsec ParsecState a
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 a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState 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 a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState 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 a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState 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 a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState 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 a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState 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 a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState 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 a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState 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 a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState 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 =
Tag -> Parsec ParsecState Variable
forall a c b. Stream a c => Tag -> Parsec a b
fatalError Tag
"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 a. a -> Parsec ParsecState a
forall (m :: * -> *) a. Monad m => a -> m a
return ();
Mode
Untyped ->
Tag -> Parsec ParsecState ()
forall a c b. Stream a c => Tag -> Parsec a b
fatalError Tag
"Used a typed quantification in an untyped formula" };
Parser Type
type_ } Parser Type -> Parser Type -> Parser Type
forall a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Type -> Parser Type
forall a. a -> Parsec ParsecState a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
indType
MkState Maybe Tag
mfile Problem 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 Tag
-> Problem Form
-> Map Symbol Type
-> Map Symbol [Function]
-> Map Symbol Variable
-> Int64
-> ParseState
MkState Maybe Tag
mfile Problem 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 a. a -> Parsec ParsecState a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int64 -> Symbol -> Maybe Tag -> Renamer -> Name
Unique Int64
n Symbol
x Maybe Tag
forall a. Maybe a
Nothing Renamer
defaultRenamer Name -> Type -> Variable
forall a b. a -> b -> a ::: b
::: Type
ty)
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 a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState a
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 a. a -> Parsec ParsecState a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
indType }
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 a. Eq a => a -> [a] -> 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 a. a -> Parsec ParsecState a
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_
_ = Tag -> Parser Type_
forall a c b. Stream a c => Tag -> Parsec a b
fatalError Tag
"invalid type"
arrow :: Type_ -> Type_ -> Parser Type_
arrow :: Type_ -> Type_ -> Parser Type_
arrow (Prod [Type]
ts) (Prod [Type
x]) = Type_ -> Parser Type_
forall a. a -> Parsec ParsecState a
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_
_ = Tag -> Parser Type_
forall a c b. Stream a c => Tag -> Parsec a b
fatalError Tag
"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 a. a -> Parsec ParsecState a
forall (m :: * -> *) a. Monad m => a -> m a
return Type_
TType } Parser Type_ -> Parser Type_ -> Parser Type_
forall a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState a
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 a. a -> Parsec ParsecState a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Type] -> Type_
Prod [Type
O]) } Parser Type_ -> Parser Type_ -> Parser Type_
forall a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
do { Type
ty <- Parser Type
type_; Type_ -> Parser Type_
forall a. a -> Parsec ParsecState a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Type] -> Type_
Prod [Type
ty]) } Parser Type_ -> Parser Type_ -> Parser Type_
forall a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState a
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 a b.
Parsec ParsecState a
-> Parsec ParsecState b -> Parsec ParsecState b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Type_ -> Type_ -> Parser Type_)
-> Parser (Type_ -> Type_ -> Parser Type_)
forall a. a -> Parsec ParsecState a
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 a b.
Parsec ParsecState a
-> Parsec ParsecState b -> Parsec ParsecState b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Type_ -> Type_ -> Parser Type_)
-> Parser (Type_ -> Type_ -> Parser Type_)
forall a. a -> Parsec ParsecState a
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 a.
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 a. a -> Parsec ParsecState a
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 a. a -> Parsec ParsecState a
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 a. a -> Parsec ParsecState a
forall (m :: * -> *) a. Monad m => a -> m a
return () }
Type_
_ -> Tag -> Parsec ParsecState ()
forall a c b. Stream a c => Tag -> Parsec a b
fatalError Tag
"invalid type"