-- Parse little bits of TPTP, e.g. a prelude for a particular tool.

{-# LANGUAGE CPP, OverloadedStrings #-}
module Jukebox.TPTP.ParseSnippet where

import Jukebox.TPTP.Parse.Core as TPTP.Parse.Core
import Jukebox.TPTP.Parsec as TPTP.Parsec
import Jukebox.TPTP.Lexer
import Jukebox.Name
import Jukebox.Form hiding (run_)
import qualified Data.Map.Strict as Map
import Data.List
#if __GLASGOW_HASKELL__ < 710
import Control.Applicative
#endif
import Data.Symbol

tff, cnf :: [(String, Type)] -> [(String, Function)] -> String -> Form
tff :: [(String, Type)] -> [(String, Function)] -> String -> Form
tff = Parser Form
-> [(String, Type)] -> [(String, Function)] -> String -> Form
forall a.
Symbolic a =>
Parser a -> [(String, Type)] -> [(String, Function)] -> String -> a
form Parser Form
TPTP.Parse.Core.tff
cnf :: [(String, Type)] -> [(String, Function)] -> String -> Form
cnf = Parser Form
-> [(String, Type)] -> [(String, Function)] -> String -> Form
forall a.
Symbolic a =>
Parser a -> [(String, Type)] -> [(String, Function)] -> String -> a
form Parser Form
TPTP.Parse.Core.cnf

form :: Symbolic a => Parser a -> [(String, Type)] -> [(String, Function)] -> String -> a
form :: Parser a -> [(String, Type)] -> [(String, Function)] -> String -> a
form Parser a
parser [(String, Type)]
types0 [(String, Function)]
funs0 String
str =
  case Parser a -> ParsecState -> Result (Position ParsecState) a
forall a c b.
Stream a c =>
Parsec a b -> a -> Result (Position a) b
run_ (Parser a
parser Parser a -> Parsec ParsecState () -> Parser a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parsec ParsecState ()
forall a b. Stream a b => Parsec a ()
eof)
            (ParseState -> TokenStream -> ParsecState
forall state stream. state -> stream -> UserState state stream
UserState (Maybe String
-> [Input Form]
-> Map Symbol Type
-> Map Symbol [Function]
-> Map Symbol Variable
-> Int64
-> ParseState
MkState Maybe String
forall a. Maybe a
Nothing [] (Symbol -> Map Symbol Type -> Map Symbol Type
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete Symbol
"$i" Map Symbol Type
types) Map Symbol [Function]
funs Map Symbol Variable
forall k a. Map k a
Map.empty Int64
0) (String -> TokenStream
scan String
str)) of
    Ok (UserState (MkState _ _ types' funs' _ _) (At _ (Cons Eof _))) a
res
      | Symbol -> Type -> Map Symbol Type -> Map Symbol Type
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Symbol
"$i" Type
indType Map Symbol Type
types Map Symbol Type -> Map Symbol Type -> Bool
forall a. Eq a => a -> a -> Bool
/=
        Symbol -> Type -> Map Symbol Type -> Map Symbol Type
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Symbol
"$i" Type
indType Map Symbol Type
types' ->
        String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
"ParseSnippet: type implicitly defined: " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                [Type] -> String
forall a. Show a => a -> String
show (((Symbol, Type) -> Type) -> [(Symbol, Type)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol, Type) -> Type
forall a b. (a, b) -> b
snd (Map Symbol Type -> [(Symbol, Type)]
forall k a. Map k a -> [(k, a)]
Map.toList Map Symbol Type
types' [(Symbol, Type)] -> [(Symbol, Type)] -> [(Symbol, Type)]
forall a. Eq a => [a] -> [a] -> [a]
\\ Map Symbol Type -> [(Symbol, Type)]
forall k a. Map k a -> [(k, a)]
Map.toList Map Symbol Type
types))
      | Map Symbol [Function]
funs Map Symbol [Function] -> Map Symbol [Function] -> Bool
forall a. Eq a => a -> a -> Bool
/= Map Symbol [Function]
funs' ->
        String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
"ParseSnippet: function implicitly defined: " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                [[Function]] -> String
forall a. Show a => a -> String
show (((Symbol, [Function]) -> [Function])
-> [(Symbol, [Function])] -> [[Function]]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol, [Function]) -> [Function]
forall a b. (a, b) -> b
snd (Map Symbol [Function] -> [(Symbol, [Function])]
forall k a. Map k a -> [(k, a)]
Map.toList Map Symbol [Function]
funs' [(Symbol, [Function])]
-> [(Symbol, [Function])] -> [(Symbol, [Function])]
forall a. Eq a => [a] -> [a] -> [a]
\\ Map Symbol [Function] -> [(Symbol, [Function])]
forall k a. Map k a -> [(k, a)]
Map.toList Map Symbol [Function]
funs))
      | Bool
otherwise -> (Type -> Type) -> a -> a
forall a. Symbolic a => (Type -> Type) -> a -> a
mapType Type -> Type
elimI a
res
    Ok{} -> String -> a
forall a. HasCallStack => String -> a
error String
"ParseSnippet: lexical error"
    TPTP.Parsec.Error Position ParsecState
_ String
msg -> String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
"ParseSnippet: parse error: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
msg
    Expected Position ParsecState
_ [String]
exp -> String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
"ParseSnippet: parse error: expected " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall a. Show a => a -> String
show [String]
exp

  where
    funs :: Map Symbol [Function]
funs = (String -> Symbol)
-> Map String [Function] -> Map Symbol [Function]
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys String -> Symbol
intern (Map String [Function] -> Map Symbol [Function])
-> Map String [Function] -> Map Symbol [Function]
forall a b. (a -> b) -> a -> b
$ [(String, [Function])] -> Map String [Function]
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(String, [Function])] -> Map String [Function])
-> [(String, [Function])] -> Map String [Function]
forall a b. (a -> b) -> a -> b
$ ((String, Function) -> (String, [Function]))
-> [(String, Function)] -> [(String, [Function])]
forall a b. (a -> b) -> [a] -> [b]
map ((Type -> Type) -> (String, Function) -> (String, [Function])
forall a a.
(Type -> Type) -> (a, a ::: FunType) -> (a, [a ::: FunType])
mapFunType Type -> Type
introI) [(String, Function)]
funs0
    types :: Map Symbol Type
types = (String -> Symbol) -> Map String Type -> Map Symbol Type
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys String -> Symbol
intern (Map String Type -> Map Symbol Type)
-> Map String Type -> Map Symbol Type
forall a b. (a -> b) -> a -> b
$ [(String, Type)] -> Map String Type
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(String, Type)]
types0

    mapFunType :: (Type -> Type) -> (a, a ::: FunType) -> (a, [a ::: FunType])
mapFunType Type -> Type
f (a
xs, a
name ::: FunType [Type]
args Type
res) =
      (a
xs, [a
name a -> FunType -> a ::: FunType
forall a b. a -> b -> a ::: b
::: [Type] -> Type -> FunType
FunType ((Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Type
f [Type]
args) (Type -> Type
f Type
res)])

    elimI :: Type -> Type
elimI =
      case Symbol -> Map Symbol Type -> Maybe Type
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Symbol
"$i" Map Symbol Type
types of
        Maybe Type
Nothing -> Type -> Type
forall a. a -> a
id
        Just Type
i ->
          \Type
ty -> if Type
ty Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
indType then Type
i else Type
ty
    introI :: Type -> Type
introI =
      case Symbol -> Map Symbol Type -> Maybe Type
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Symbol
"$i" Map Symbol Type
types of
        Maybe Type
Nothing -> Type -> Type
forall a. a -> a
id
        Just Type
i ->
          \Type
ty -> if Type
ty Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
i then Type
indType else Type
ty