{-# 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 -> 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
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
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)
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)))
{-# 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"
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
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
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))
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
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
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
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"
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
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
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
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
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 (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
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
{-# 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
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))
{-# 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)
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 }
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"