{- |
Module      :  ./CASL/Kif2CASL.hs
Description :  Parser for SUMO (suggested upper merged ontology) .kif files
Copyright   :  (c) T.Mossakowski, C.Maeder and Uni Bremen 2006
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  portable

Parser for SUMO (suggested upper merged ontology) .kif files
-}

module CASL.Kif2CASL where

import Common.AS_Annotation
import Common.Id
import Common.Lexer
import Common.Parsec
import Common.ProofUtils
import Common.Token

import qualified Data.List as List
import qualified Data.Set as Set
import qualified Data.Map as Map

import qualified Text.PrettyPrint.HughesPJ as Doc
import Text.ParserCombinators.Parsec

import CASL.Kif
import CASL.AS_Basic_CASL
import CASL.Fold

-- | the universal sort
universe :: SORT
universe :: SORT
universe = String -> Range -> SORT
toId "U" Range
nullRange

llRange :: RangedLL -> Range
llRange :: RangedLL -> Range
llRange (RangedLL p :: SourcePos
p _ q :: SourcePos
q) = [Pos] -> Range
Range [SourcePos -> Pos
fromSourcePos SourcePos
p, SourcePos -> Pos
fromSourcePos SourcePos
q]

-- | translation of formulas
kif2CASLFormula :: RangedLL -> CASLFORMULA
kif2CASLFormula :: RangedLL -> CASLFORMULA
kif2CASLFormula rl :: RangedLL
rl@(RangedLL _ x :: ListOfList
x _) = let r :: Range
r = RangedLL -> Range
llRange RangedLL
rl in case ListOfList
x of
  List (pr :: RangedLL
pr@(RangedLL _ (Literal KToken p :: String
p) _) : phis :: [RangedLL]
phis) -> case (String
p, [RangedLL]
phis) of
    ("and", _) -> Junctor -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction Junctor
Con ((RangedLL -> CASLFORMULA) -> [RangedLL] -> [CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map RangedLL -> CASLFORMULA
kif2CASLFormula [RangedLL]
phis) Range
r
    ("or", _) -> Junctor -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction Junctor
Dis ((RangedLL -> CASLFORMULA) -> [RangedLL] -> [CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map RangedLL -> CASLFORMULA
kif2CASLFormula [RangedLL]
phis) Range
r
    ("=>", [phi1 :: RangedLL
phi1, phi2 :: RangedLL
phi2]) ->
      CASLFORMULA -> Relation -> CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
Relation (RangedLL -> CASLFORMULA
kif2CASLFormula RangedLL
phi1) Relation
Implication (RangedLL -> CASLFORMULA
kif2CASLFormula RangedLL
phi2) Range
r
    ("<=>", [phi1 :: RangedLL
phi1, phi2 :: RangedLL
phi2]) ->
      CASLFORMULA -> Relation -> CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
Relation (RangedLL -> CASLFORMULA
kif2CASLFormula RangedLL
phi1) Relation
Equivalence (RangedLL -> CASLFORMULA
kif2CASLFormula RangedLL
phi2) Range
r
    ("not", [phi :: RangedLL
phi]) -> CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Range -> FORMULA f
Negation (RangedLL -> CASLFORMULA
kif2CASLFormula RangedLL
phi) Range
r
    ("True", []) -> Bool -> Range -> CASLFORMULA
forall f. Bool -> Range -> FORMULA f
Atom Bool
True Range
r
    ("False", []) -> Bool -> Range -> CASLFORMULA
forall f. Bool -> Range -> FORMULA f
Atom Bool
False Range
r
    ("exists", [RangedLL _ (List vl :: [RangedLL]
vl) _, phi :: RangedLL
phi]) ->
      QUANTIFIER -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
Existential ([RangedLL] -> [VAR_DECL]
kif2CASLvardeclList [RangedLL]
vl) (RangedLL -> CASLFORMULA
kif2CASLFormula RangedLL
phi)
      Range
r
    ("forall", [RangedLL _ (List vl :: [RangedLL]
vl) _, phi :: RangedLL
phi]) ->
      QUANTIFIER -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
Universal ([RangedLL] -> [VAR_DECL]
kif2CASLvardeclList [RangedLL]
vl) (RangedLL -> CASLFORMULA
kif2CASLFormula RangedLL
phi)
      Range
r
    ("equal", [t1 :: RangedLL
t1, t2 :: RangedLL
t2]) ->
      TERM () -> Equality -> TERM () -> Range -> CASLFORMULA
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
Equation (RangedLL -> TERM ()
kif2CASLTerm RangedLL
t1) Equality
Strong (RangedLL -> TERM ()
kif2CASLTerm RangedLL
t2) Range
r
    _ -> PRED_SYMB -> [TERM ()] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication (SORT -> PRED_SYMB
Pred_name (String -> Range -> SORT
toId String
p (Range -> SORT) -> Range -> SORT
forall a b. (a -> b) -> a -> b
$ RangedLL -> Range
llRange RangedLL
pr))
      ((RangedLL -> TERM ()) -> [RangedLL] -> [TERM ()]
forall a b. (a -> b) -> [a] -> [b]
map RangedLL -> TERM ()
kif2CASLTerm [RangedLL]
phis) Range
r
-- also translate 2nd order applications to 1st order, using holds predicate
  List l :: [RangedLL]
l -> PRED_SYMB -> [TERM ()] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication (SORT -> PRED_SYMB
Pred_name (String -> Range -> SORT
toId "holds" Range
r))
                  ((RangedLL -> TERM ()) -> [RangedLL] -> [TERM ()]
forall a b. (a -> b) -> [a] -> [b]
map RangedLL -> TERM ()
kif2CASLTerm [RangedLL]
l) Range
r
-- a variable in place of a formula; coerce from Booleans
  Literal k :: StringKind
k v :: String
v | StringKind -> [StringKind] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem StringKind
k [StringKind
QWord, StringKind
AtWord] ->
    TERM () -> Equality -> TERM () -> Range -> CASLFORMULA
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
Equation (Token -> TERM ()
forall f. Token -> TERM f
Mixfix_token (Token -> TERM ()) -> Token -> TERM ()
forall a b. (a -> b) -> a -> b
$ String -> Range -> Token
toVar String
v Range
r) Equality
Strong TERM ()
trueTerm Range
r
  _ -> String -> CASLFORMULA
forall a. HasCallStack => String -> a
error (String -> CASLFORMULA) -> String -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ "kif2CASLFormula : cannot translate " String -> String -> String
forall a. [a] -> [a] -> [a]
++ ListOfList -> String
forall a. Show a => a -> String
show ListOfList
x

trueTerm :: TERM ()
trueTerm :: TERM ()
trueTerm = Token -> TERM ()
forall f. Token -> TERM f
varOrConst (Token -> TERM ()) -> Token -> TERM ()
forall a b. (a -> b) -> a -> b
$ String -> Token
mkSimpleId "True"

falseTerm :: TERM ()
falseTerm :: TERM ()
falseTerm = Token -> TERM ()
forall f. Token -> TERM f
varOrConst (Token -> TERM ()) -> Token -> TERM ()
forall a b. (a -> b) -> a -> b
$ String -> Token
mkSimpleId "False"

toVar :: String -> Range -> Token
toVar :: String -> Range -> Token
toVar v :: String
v = String -> Range -> Token
toSId (String -> Range -> Token) -> String -> Range -> Token
forall a b. (a -> b) -> a -> b
$ 'v' Char -> String -> String
forall a. a -> [a] -> [a]
: String -> String
forall a. [a] -> [a]
tail String
v

toId :: String -> Range -> Id
toId :: String -> Range -> SORT
toId s :: String
s = Token -> SORT
simpleIdToId (Token -> SORT) -> (Range -> Token) -> Range -> SORT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Range -> Token
toSId String
s

-- | convert a string to a legal CASL identifier
toSId :: String -> Range -> Token
toSId :: String -> Range -> Token
toSId s :: String
s = String -> Range -> Token
Token (String -> Range -> Token) -> String -> Range -> Token
forall a b. (a -> b) -> a -> b
$ case Parsec String () () -> String -> String -> Either ParseError ()
forall s t a.
Stream s Identity t =>
Parsec s () a -> String -> s -> Either ParseError a
parse ([String] -> CharParser () String -> CharParser () String
forall st. [String] -> CharParser st String -> CharParser st String
reserved ([String]
casl_reserved_words
                                        [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
formula_words) CharParser () String
forall st. CharParser st String
scanAnyWords CharParser () String -> Parsec String () () -> Parsec String () ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parsec String () ()
forall s (m :: * -> *) t u.
(Stream s m t, Show t) =>
ParsecT s u m ()
eof)
             "Kif2CASL.toId" String
s of
    Left _ -> 'a' Char -> String -> String
forall a. a -> [a] -> [a]
: (Char -> String) -> String -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ( \ c :: Char
c -> '_' Char -> String -> String
forall a. a -> [a] -> [a]
: String -> Char -> Map Char String -> String
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault [Char
c] Char
c
                              (Char -> String -> Map Char String -> Map Char String
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert '_' "U" Map Char String
charMap)) String
s
    Right _ -> String
s

kif2CASLTerm :: RangedLL -> TERM ()
kif2CASLTerm :: RangedLL -> TERM ()
kif2CASLTerm rl :: RangedLL
rl@(RangedLL _ x :: ListOfList
x _) = let r :: Range
r = RangedLL -> Range
llRange RangedLL
rl in case ListOfList
x of
    Literal k :: StringKind
k v :: String
v | StringKind -> [StringKind] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem StringKind
k [StringKind
QWord, StringKind
AtWord] -> Token -> TERM ()
forall f. Token -> TERM f
Mixfix_token (Token -> TERM ()) -> Token -> TERM ()
forall a b. (a -> b) -> a -> b
$ String -> Range -> Token
toVar String
v Range
r
    Literal _ s :: String
s -> Token -> TERM ()
forall f. Token -> TERM f
varOrConst (Token -> TERM ()) -> Token -> TERM ()
forall a b. (a -> b) -> a -> b
$ String -> Range -> Token
toSId String
s Range
r
    -- a formula in place of a term; coerce to Booleans
    List (rf :: RangedLL
rf@(RangedLL _ (Literal _ f :: String
f) _) : args :: [RangedLL]
args) ->
      if String
f String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ["forall", "exists"] -- ,"and","or","=>","<=>","not"]
       then TERM () -> CASLFORMULA -> TERM () -> Range -> TERM ()
forall f. TERM f -> FORMULA f -> TERM f -> Range -> TERM f
Conditional TERM ()
trueTerm
         (RangedLL -> CASLFORMULA
kif2CASLFormula RangedLL
rl) TERM ()
falseTerm Range
r
        else OP_SYMB -> [TERM ()] -> Range -> TERM ()
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application (SORT -> OP_SYMB
Op_name (SORT -> OP_SYMB) -> SORT -> OP_SYMB
forall a b. (a -> b) -> a -> b
$ String -> Range -> SORT
toId String
f (Range -> SORT) -> Range -> SORT
forall a b. (a -> b) -> a -> b
$ RangedLL -> Range
llRange RangedLL
rf)
                 ((RangedLL -> TERM ()) -> [RangedLL] -> [TERM ()]
forall a b. (a -> b) -> [a] -> [b]
map RangedLL -> TERM ()
kif2CASLTerm [RangedLL]
args) Range
r
    _ -> String -> TERM ()
forall a. HasCallStack => String -> a
error (String -> TERM ()) -> String -> TERM ()
forall a b. (a -> b) -> a -> b
$ "kif2CASLTerm : cannot translate " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (RangedLL -> Doc
ppRangedLL RangedLL
rl)

-- | translation of variable declaration lists
kif2CASLvardeclList :: [RangedLL] -> [VAR_DECL]
kif2CASLvardeclList :: [RangedLL] -> [VAR_DECL]
kif2CASLvardeclList = (RangedLL -> VAR_DECL) -> [RangedLL] -> [VAR_DECL]
forall a b. (a -> b) -> [a] -> [b]
map RangedLL -> VAR_DECL
kif2CASLvardecl

-- | translation of variable declarations
kif2CASLvardecl :: RangedLL -> VAR_DECL
kif2CASLvardecl :: RangedLL -> VAR_DECL
kif2CASLvardecl rl :: RangedLL
rl@(RangedLL _ l :: ListOfList
l _) = let r :: Range
r = RangedLL -> Range
llRange RangedLL
rl in case ListOfList
l of
    Literal _ v :: String
v -> [Token] -> SORT -> Range -> VAR_DECL
Var_decl [String -> Range -> Token
toVar String
v Range
r] SORT
universe Range
r
    _ -> String -> VAR_DECL
forall a. HasCallStack => String -> a
error (String -> VAR_DECL) -> String -> VAR_DECL
forall a b. (a -> b) -> a -> b
$ "kif2CASLvardecl " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (ListOfList -> Doc
ppListOfList ListOfList
l)

-- | first pass of translation, just collecting the formulas
kif2CASLpass1 :: [RangedLL] -> [Annoted CASLFORMULA]
kif2CASLpass1 :: [RangedLL] -> [Annoted CASLFORMULA]
kif2CASLpass1 [] = []
kif2CASLpass1 (phi :: RangedLL
phi : rest :: [RangedLL]
rest) =
  (CASLFORMULA -> Annoted CASLFORMULA
forall a. a -> Annoted a
emptyAnno CASLFORMULA
phi') { r_annos :: [Annotation]
r_annos = [Annotation]
annos } Annoted CASLFORMULA
-> [Annoted CASLFORMULA] -> [Annoted CASLFORMULA]
forall a. a -> [a] -> [a]
: [RangedLL] -> [Annoted CASLFORMULA]
kif2CASLpass1 [RangedLL]
rest'
  where phi' :: CASLFORMULA
phi' = RangedLL -> CASLFORMULA
kif2CASLFormula RangedLL
phi
        (annos :: [Annotation]
annos, rest' :: [RangedLL]
rest') = [Annotation] -> [RangedLL] -> ([Annotation], [RangedLL])
skipComments [] [RangedLL]
rest

-- | check for comment
isKifComment :: ListOfList -> Bool
isKifComment :: ListOfList -> Bool
isKifComment (List (RangedLL _ (Literal KToken "documentation") _ : _)) = Bool
True
isKifComment _ = Bool
False

-- | convert comment to annotation
toAnno :: ListOfList -> Annotation
toAnno :: ListOfList -> Annotation
toAnno (List (_ : l :: [RangedLL]
l)) =
  Annote_word -> Annote_text -> Range -> Annotation
Unparsed_anno Annote_word
Comment_start
    ([String] -> Annote_text
Group_anno [Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
Doc.vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (RangedLL -> Doc) -> [RangedLL] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map RangedLL -> Doc
ppRangedLL [RangedLL]
l]) Range
nullRange
toAnno _ = String -> Annotation
forall a. HasCallStack => String -> a
error "Kif2CASL.toAnno: wrong format of comment"

-- | skip the first comments; they belong to the whole file
skipComments :: [Annotation] -> [RangedLL] -> ([Annotation], [RangedLL])
skipComments :: [Annotation] -> [RangedLL] -> ([Annotation], [RangedLL])
skipComments acc :: [Annotation]
acc [] = ([Annotation] -> [Annotation]
forall a. [a] -> [a]
reverse [Annotation]
acc, [])
skipComments acc :: [Annotation]
acc l :: [RangedLL]
l@(RangedLL _ x :: ListOfList
x _ : rest :: [RangedLL]
rest) =
  if ListOfList -> Bool
isKifComment ListOfList
x
   then [Annotation] -> [RangedLL] -> ([Annotation], [RangedLL])
skipComments (ListOfList -> Annotation
toAnno ListOfList
x Annotation -> [Annotation] -> [Annotation]
forall a. a -> [a] -> [a]
: [Annotation]
acc) [RangedLL]
rest
   else ([Annotation] -> [Annotation]
forall a. [a] -> [a]
reverse [Annotation]
acc, [RangedLL]
l)

data Predsym = Predsym Int PRED_NAME
                deriving (Predsym -> Predsym -> Bool
(Predsym -> Predsym -> Bool)
-> (Predsym -> Predsym -> Bool) -> Eq Predsym
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Predsym -> Predsym -> Bool
$c/= :: Predsym -> Predsym -> Bool
== :: Predsym -> Predsym -> Bool
$c== :: Predsym -> Predsym -> Bool
Eq, Eq Predsym
Eq Predsym =>
(Predsym -> Predsym -> Ordering)
-> (Predsym -> Predsym -> Bool)
-> (Predsym -> Predsym -> Bool)
-> (Predsym -> Predsym -> Bool)
-> (Predsym -> Predsym -> Bool)
-> (Predsym -> Predsym -> Predsym)
-> (Predsym -> Predsym -> Predsym)
-> Ord Predsym
Predsym -> Predsym -> Bool
Predsym -> Predsym -> Ordering
Predsym -> Predsym -> Predsym
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Predsym -> Predsym -> Predsym
$cmin :: Predsym -> Predsym -> Predsym
max :: Predsym -> Predsym -> Predsym
$cmax :: Predsym -> Predsym -> Predsym
>= :: Predsym -> Predsym -> Bool
$c>= :: Predsym -> Predsym -> Bool
> :: Predsym -> Predsym -> Bool
$c> :: Predsym -> Predsym -> Bool
<= :: Predsym -> Predsym -> Bool
$c<= :: Predsym -> Predsym -> Bool
< :: Predsym -> Predsym -> Bool
$c< :: Predsym -> Predsym -> Bool
compare :: Predsym -> Predsym -> Ordering
$ccompare :: Predsym -> Predsym -> Ordering
$cp1Ord :: Eq Predsym
Ord, Int -> Predsym -> String -> String
[Predsym] -> String -> String
Predsym -> String
(Int -> Predsym -> String -> String)
-> (Predsym -> String)
-> ([Predsym] -> String -> String)
-> Show Predsym
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [Predsym] -> String -> String
$cshowList :: [Predsym] -> String -> String
show :: Predsym -> String
$cshow :: Predsym -> String
showsPrec :: Int -> Predsym -> String -> String
$cshowsPrec :: Int -> Predsym -> String -> String
Show)

sameArity :: Predsym -> Predsym -> Bool
sameArity :: Predsym -> Predsym -> Bool
sameArity (Predsym m :: Int
m _) (Predsym n :: Int
n _) = Int
m Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n

getName :: Predsym -> PRED_NAME
getName :: Predsym -> SORT
getName (Predsym _ p :: SORT
p) = SORT
p

-- | collect all predicate symbols used in a formula
collectPreds :: CASLFORMULA -> Set.Set Predsym
collectPreds :: CASLFORMULA -> Set Predsym
collectPreds = Record () (Set Predsym) (Set Predsym) -> CASLFORMULA -> Set Predsym
forall f a b. Record f a b -> FORMULA f -> a
foldFormula
    ((() -> Set Predsym)
-> ([Set Predsym] -> Set Predsym)
-> Set Predsym
-> Record () (Set Predsym) (Set Predsym)
forall f a. (f -> a) -> ([a] -> a) -> a -> Record f a a
constRecord (String -> () -> Set Predsym
forall a. HasCallStack => String -> a
error "Kif2CASL.collectPreds") [Set Predsym] -> Set Predsym
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions Set Predsym
forall a. Set a
Set.empty)
    { foldPredication :: CASLFORMULA -> PRED_SYMB -> [Set Predsym] -> Range -> Set Predsym
foldPredication = \ _ p :: PRED_SYMB
p args :: [Set Predsym]
args _ -> Predsym -> Set Predsym -> Set Predsym
forall a. Ord a => a -> Set a -> Set a
Set.insert
               (Int -> SORT -> Predsym
Predsym ([Set Predsym] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Set Predsym]
args)
                        (case PRED_SYMB
p of
                          Pred_name pn :: SORT
pn -> SORT
pn
                          Qual_pred_name pn :: SORT
pn _ _ -> SORT
pn))
               ([Set Predsym] -> Set Predsym
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions [Set Predsym]
args) }

collectVars :: CASLFORMULA -> Set.Set Token
collectVars :: CASLFORMULA -> Set Token
collectVars = Record () (Set Token) (Set Token) -> CASLFORMULA -> Set Token
forall f a b. Record f a b -> FORMULA f -> a
foldFormula
    ((() -> Set Token)
-> ([Set Token] -> Set Token)
-> Set Token
-> Record () (Set Token) (Set Token)
forall f a. (f -> a) -> ([a] -> a) -> a -> Record f a a
constRecord (String -> () -> Set Token
forall a. HasCallStack => String -> a
error "Kif2CASL.collectVars") [Set Token] -> Set Token
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions Set Token
forall a. Set a
Set.empty)
    { foldMixfix_token :: TERM () -> Token -> Set Token
foldMixfix_token = (Token -> Set Token) -> TERM () -> Token -> Set Token
forall a b. a -> b -> a
const Token -> Set Token
forall a. a -> Set a
Set.singleton
    , foldQuantification :: CASLFORMULA
-> QUANTIFIER -> [VAR_DECL] -> Set Token -> Range -> Set Token
foldQuantification = \ _ _ vs :: [VAR_DECL]
vs rs :: Set Token
rs _ ->
        Set Token -> Set Token -> Set Token
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set Token
rs (Set Token -> Set Token)
-> ([Token] -> Set Token) -> [Token] -> Set Token
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Token] -> Set Token
forall a. Ord a => [a] -> Set a
Set.fromList
          ([Token] -> Set Token) -> [Token] -> Set Token
forall a b. (a -> b) -> a -> b
$ (VAR_DECL -> [Token]) -> [VAR_DECL] -> [Token]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ (Var_decl v :: [Token]
v _ _) -> [Token]
v) [VAR_DECL]
vs
    }

data Opsym = Opsym Int OP_NAME
                deriving (Opsym -> Opsym -> Bool
(Opsym -> Opsym -> Bool) -> (Opsym -> Opsym -> Bool) -> Eq Opsym
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Opsym -> Opsym -> Bool
$c/= :: Opsym -> Opsym -> Bool
== :: Opsym -> Opsym -> Bool
$c== :: Opsym -> Opsym -> Bool
Eq, Eq Opsym
Eq Opsym =>
(Opsym -> Opsym -> Ordering)
-> (Opsym -> Opsym -> Bool)
-> (Opsym -> Opsym -> Bool)
-> (Opsym -> Opsym -> Bool)
-> (Opsym -> Opsym -> Bool)
-> (Opsym -> Opsym -> Opsym)
-> (Opsym -> Opsym -> Opsym)
-> Ord Opsym
Opsym -> Opsym -> Bool
Opsym -> Opsym -> Ordering
Opsym -> Opsym -> Opsym
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Opsym -> Opsym -> Opsym
$cmin :: Opsym -> Opsym -> Opsym
max :: Opsym -> Opsym -> Opsym
$cmax :: Opsym -> Opsym -> Opsym
>= :: Opsym -> Opsym -> Bool
$c>= :: Opsym -> Opsym -> Bool
> :: Opsym -> Opsym -> Bool
$c> :: Opsym -> Opsym -> Bool
<= :: Opsym -> Opsym -> Bool
$c<= :: Opsym -> Opsym -> Bool
< :: Opsym -> Opsym -> Bool
$c< :: Opsym -> Opsym -> Bool
compare :: Opsym -> Opsym -> Ordering
$ccompare :: Opsym -> Opsym -> Ordering
$cp1Ord :: Eq Opsym
Ord, Int -> Opsym -> String -> String
[Opsym] -> String -> String
Opsym -> String
(Int -> Opsym -> String -> String)
-> (Opsym -> String) -> ([Opsym] -> String -> String) -> Show Opsym
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [Opsym] -> String -> String
$cshowList :: [Opsym] -> String -> String
show :: Opsym -> String
$cshow :: Opsym -> String
showsPrec :: Int -> Opsym -> String -> String
$cshowsPrec :: Int -> Opsym -> String -> String
Show)

sameOpArity :: Opsym -> Opsym -> Bool
sameOpArity :: Opsym -> Opsym -> Bool
sameOpArity (Opsym m :: Int
m _) (Opsym n :: Int
n _) = Int
m Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n

getOpName :: Opsym -> OP_NAME
getOpName :: Opsym -> SORT
getOpName (Opsym _ p :: SORT
p) = SORT
p

collectOps :: CASLFORMULA -> Set.Set Opsym
collectOps :: CASLFORMULA -> Set Opsym
collectOps = Record () (Set Opsym) (Set Opsym) -> CASLFORMULA -> Set Opsym
forall f a b. Record f a b -> FORMULA f -> a
foldFormula
    ((() -> Set Opsym)
-> ([Set Opsym] -> Set Opsym)
-> Set Opsym
-> Record () (Set Opsym) (Set Opsym)
forall f a. (f -> a) -> ([a] -> a) -> a -> Record f a a
constRecord (String -> () -> Set Opsym
forall a. HasCallStack => String -> a
error "Kif2CASL.collectConsts") [Set Opsym] -> Set Opsym
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions Set Opsym
forall a. Set a
Set.empty)
    { foldApplication :: TERM () -> OP_SYMB -> [Set Opsym] -> Range -> Set Opsym
foldApplication = \ _ o :: OP_SYMB
o l :: [Set Opsym]
l _ ->
          Opsym -> Set Opsym -> Set Opsym
forall a. Ord a => a -> Set a -> Set a
Set.insert (Int -> SORT -> Opsym
Opsym ([Set Opsym] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Set Opsym]
l) (case OP_SYMB
o of
            Op_name i :: SORT
i -> SORT
i
            Qual_op_name i :: SORT
i _ _ -> SORT
i) )
            ([Set Opsym] -> Set Opsym
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions [Set Opsym]
l) }

nonEmpty :: Annoted (BASIC_ITEMS () () ()) -> Bool
nonEmpty :: Annoted (BASIC_ITEMS () () ()) -> Bool
nonEmpty bi :: Annoted (BASIC_ITEMS () () ())
bi = case Annoted (BASIC_ITEMS () () ()) -> BASIC_ITEMS () () ()
forall a. Annoted a -> a
item Annoted (BASIC_ITEMS () () ())
bi of
  Sig_items (Sort_items _ l :: [Annoted (SORT_ITEM ())]
l _) -> Bool -> Bool
not ([Annoted (SORT_ITEM ())] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Annoted (SORT_ITEM ())]
l)
  Sig_items (Op_items l :: [Annoted (OP_ITEM ())]
l _) -> Bool -> Bool
not ([Annoted (OP_ITEM ())] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Annoted (OP_ITEM ())]
l)
  Sig_items (Pred_items l :: [Annoted (PRED_ITEM ())]
l _) -> Bool -> Bool
not ([Annoted (PRED_ITEM ())] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Annoted (PRED_ITEM ())]
l)
  Var_items l :: [VAR_DECL]
l _ -> Bool -> Bool
not ([VAR_DECL] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [VAR_DECL]
l)
  Axiom_items l :: [Annoted CASLFORMULA]
l _ -> Bool -> Bool
not ([Annoted CASLFORMULA] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Annoted CASLFORMULA]
l)
  _ -> Bool
True

-- | main translation function
kif2CASL :: [RangedLL] -> BASIC_SPEC () () ()
kif2CASL :: [RangedLL] -> BASIC_SPEC () () ()
kif2CASL l :: [RangedLL]
l = [Annoted (BASIC_ITEMS () () ())] -> BASIC_SPEC () () ()
forall b s f. [Annoted (BASIC_ITEMS b s f)] -> BASIC_SPEC b s f
Basic_spec ([Annoted (BASIC_ITEMS () () ())] -> BASIC_SPEC () () ())
-> [Annoted (BASIC_ITEMS () () ())] -> BASIC_SPEC () () ()
forall a b. (a -> b) -> a -> b
$ (Annoted (BASIC_ITEMS () () ()) -> Bool)
-> [Annoted (BASIC_ITEMS () () ())]
-> [Annoted (BASIC_ITEMS () () ())]
forall a. (a -> Bool) -> [a] -> [a]
filter Annoted (BASIC_ITEMS () () ()) -> Bool
nonEmpty
                           [(BASIC_ITEMS () () () -> Annoted (BASIC_ITEMS () () ())
forall a. a -> Annoted a
emptyAnno BASIC_ITEMS () () ()
forall b s f. BASIC_ITEMS b s f
sorts) { l_annos :: [Annotation]
l_annos = [Annotation]
ans },
                            BASIC_ITEMS () () () -> Annoted (BASIC_ITEMS () () ())
forall a. a -> Annoted a
emptyAnno BASIC_ITEMS () () ()
forall b s f. BASIC_ITEMS b s f
ops, BASIC_ITEMS () () () -> Annoted (BASIC_ITEMS () () ())
forall a. a -> Annoted a
emptyAnno BASIC_ITEMS () () ()
forall b s f. BASIC_ITEMS b s f
preds,
                            BASIC_ITEMS () () () -> Annoted (BASIC_ITEMS () () ())
forall a. a -> Annoted a
emptyAnno BASIC_ITEMS () () ()
forall b s f. BASIC_ITEMS b s f
vars, BASIC_ITEMS () () () -> Annoted (BASIC_ITEMS () () ())
forall a. a -> Annoted a
emptyAnno BASIC_ITEMS () () ()
forall b s. BASIC_ITEMS b s ()
axs]
  where (ans :: [Annotation]
ans, rest :: [RangedLL]
rest) = [Annotation] -> [RangedLL] -> ([Annotation], [RangedLL])
skipComments [] [RangedLL]
l
        phis :: [Annoted CASLFORMULA]
phis = [RangedLL] -> [Annoted CASLFORMULA]
kif2CASLpass1 [RangedLL]
rest
        axs :: BASIC_ITEMS b s ()
axs = [Annoted CASLFORMULA] -> Range -> BASIC_ITEMS b s ()
forall b s f. [Annoted (FORMULA f)] -> Range -> BASIC_ITEMS b s f
Axiom_items [Annoted CASLFORMULA]
phis Range
nullRange
        preds :: BASIC_ITEMS b s f
preds = SIG_ITEMS s f -> BASIC_ITEMS b s f
forall b s f. SIG_ITEMS s f -> BASIC_ITEMS b s f
Sig_items (SIG_ITEMS s f -> BASIC_ITEMS b s f)
-> SIG_ITEMS s f -> BASIC_ITEMS b s f
forall a b. (a -> b) -> a -> b
$ [Annoted (PRED_ITEM f)] -> Range -> SIG_ITEMS s f
forall s f. [Annoted (PRED_ITEM f)] -> Range -> SIG_ITEMS s f
Pred_items [Annoted (PRED_ITEM f)]
forall f. [Annoted (PRED_ITEM f)]
preddecls Range
nullRange
        predsyms :: [Predsym]
predsyms = Set Predsym -> [Predsym]
forall a. Set a -> [a]
Set.toList (Set Predsym -> [Predsym]) -> Set Predsym -> [Predsym]
forall a b. (a -> b) -> a -> b
$ [Set Predsym] -> Set Predsym
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set Predsym] -> Set Predsym) -> [Set Predsym] -> Set Predsym
forall a b. (a -> b) -> a -> b
$ (Annoted CASLFORMULA -> Set Predsym)
-> [Annoted CASLFORMULA] -> [Set Predsym]
forall a b. (a -> b) -> [a] -> [b]
map (CASLFORMULA -> Set Predsym
collectPreds (CASLFORMULA -> Set Predsym)
-> (Annoted CASLFORMULA -> CASLFORMULA)
-> Annoted CASLFORMULA
-> Set Predsym
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted CASLFORMULA -> CASLFORMULA
forall a. Annoted a -> a
item) [Annoted CASLFORMULA]
phis
        preddecls :: [Annoted (PRED_ITEM f)]
preddecls = ([Predsym] -> Annoted (PRED_ITEM f))
-> [[Predsym]] -> [Annoted (PRED_ITEM f)]
forall a b. (a -> b) -> [a] -> [b]
map (PRED_ITEM f -> Annoted (PRED_ITEM f)
forall a. a -> Annoted a
emptyAnno (PRED_ITEM f -> Annoted (PRED_ITEM f))
-> ([Predsym] -> PRED_ITEM f) -> [Predsym] -> Annoted (PRED_ITEM f)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Predsym] -> PRED_ITEM f
forall f. [Predsym] -> PRED_ITEM f
mkPreddecl)
          ([[Predsym]] -> [Annoted (PRED_ITEM f)])
-> [[Predsym]] -> [Annoted (PRED_ITEM f)]
forall a b. (a -> b) -> a -> b
$ (Predsym -> Predsym -> Bool) -> [Predsym] -> [[Predsym]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
List.groupBy Predsym -> Predsym -> Bool
sameArity [Predsym]
predsyms
        mkPreddecl :: [Predsym] -> PRED_ITEM f
mkPreddecl [] = String -> PRED_ITEM f
forall a. HasCallStack => String -> a
error "kif2CASL: this cannot happen"
        mkPreddecl psyms :: [Predsym]
psyms@(Predsym arity :: Int
arity _ : _) =
            [SORT] -> PRED_TYPE -> Range -> PRED_ITEM f
forall f. [SORT] -> PRED_TYPE -> Range -> PRED_ITEM f
Pred_decl ((Predsym -> SORT) -> [Predsym] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map Predsym -> SORT
getName [Predsym]
psyms)
              ([SORT] -> Range -> PRED_TYPE
Pred_type (Int -> SORT -> [SORT]
forall a. Int -> a -> [a]
replicate Int
arity SORT
universe) Range
nullRange)
              Range
nullRange
        sorts :: BASIC_ITEMS b s f
sorts =
            SIG_ITEMS s f -> BASIC_ITEMS b s f
forall b s f. SIG_ITEMS s f -> BASIC_ITEMS b s f
Sig_items (SIG_ITEMS s f -> BASIC_ITEMS b s f)
-> SIG_ITEMS s f -> BASIC_ITEMS b s f
forall a b. (a -> b) -> a -> b
$ SortsKind -> [Annoted (SORT_ITEM f)] -> Range -> SIG_ITEMS s f
forall s f.
SortsKind -> [Annoted (SORT_ITEM f)] -> Range -> SIG_ITEMS s f
Sort_items SortsKind
NonEmptySorts [SORT_ITEM f -> Annoted (SORT_ITEM f)
forall a. a -> Annoted a
emptyAnno SORT_ITEM f
forall f. SORT_ITEM f
sortdecl] Range
nullRange
        sortdecl :: SORT_ITEM f
sortdecl = [SORT] -> Range -> SORT_ITEM f
forall f. [SORT] -> Range -> SORT_ITEM f
Sort_decl [SORT
universe] Range
nullRange
        ops :: BASIC_ITEMS b s f
ops = SIG_ITEMS s f -> BASIC_ITEMS b s f
forall b s f. SIG_ITEMS s f -> BASIC_ITEMS b s f
Sig_items (SIG_ITEMS s f -> BASIC_ITEMS b s f)
-> SIG_ITEMS s f -> BASIC_ITEMS b s f
forall a b. (a -> b) -> a -> b
$ [Annoted (OP_ITEM f)] -> Range -> SIG_ITEMS s f
forall s f. [Annoted (OP_ITEM f)] -> Range -> SIG_ITEMS s f
Op_items [Annoted (OP_ITEM f)]
forall f. [Annoted (OP_ITEM f)]
opdecls Range
nullRange
        opsyms :: [Opsym]
opsyms = Set Opsym -> [Opsym]
forall a. Set a -> [a]
Set.toList (Set Opsym -> [Opsym]) -> Set Opsym -> [Opsym]
forall a b. (a -> b) -> a -> b
$ [Set Opsym] -> Set Opsym
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set Opsym] -> Set Opsym) -> [Set Opsym] -> Set Opsym
forall a b. (a -> b) -> a -> b
$ (Annoted CASLFORMULA -> Set Opsym)
-> [Annoted CASLFORMULA] -> [Set Opsym]
forall a b. (a -> b) -> [a] -> [b]
map (CASLFORMULA -> Set Opsym
collectOps (CASLFORMULA -> Set Opsym)
-> (Annoted CASLFORMULA -> CASLFORMULA)
-> Annoted CASLFORMULA
-> Set Opsym
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted CASLFORMULA -> CASLFORMULA
forall a. Annoted a -> a
item) [Annoted CASLFORMULA]
phis
        opdecls :: [Annoted (OP_ITEM f)]
opdecls = ([Opsym] -> Annoted (OP_ITEM f))
-> [[Opsym]] -> [Annoted (OP_ITEM f)]
forall a b. (a -> b) -> [a] -> [b]
map (OP_ITEM f -> Annoted (OP_ITEM f)
forall a. a -> Annoted a
emptyAnno (OP_ITEM f -> Annoted (OP_ITEM f))
-> ([Opsym] -> OP_ITEM f) -> [Opsym] -> Annoted (OP_ITEM f)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Opsym] -> OP_ITEM f
forall f. [Opsym] -> OP_ITEM f
mkOpdecl) ((Opsym -> Opsym -> Bool) -> [Opsym] -> [[Opsym]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
List.groupBy Opsym -> Opsym -> Bool
sameOpArity [Opsym]
opsyms)
        mkOpdecl :: [Opsym] -> OP_ITEM f
mkOpdecl [] = String -> OP_ITEM f
forall a. HasCallStack => String -> a
error "kif2CASL: this cannot happen"
        mkOpdecl opsms :: [Opsym]
opsms@(Opsym arity :: Int
arity _ : _) =
           [SORT] -> OP_TYPE -> [OP_ATTR f] -> Range -> OP_ITEM f
forall f. [SORT] -> OP_TYPE -> [OP_ATTR f] -> Range -> OP_ITEM f
Op_decl ((Opsym -> SORT) -> [Opsym] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map Opsym -> SORT
getOpName [Opsym]
opsms)
             (OpKind -> [SORT] -> SORT -> Range -> OP_TYPE
Op_type OpKind
Total (Int -> SORT -> [SORT]
forall a. Int -> a -> [a]
replicate Int
arity SORT
universe) SORT
universe Range
nullRange)
                   [] Range
nullRange
        usedVars :: [Token]
usedVars = Set Token -> [Token]
forall a. Set a -> [a]
Set.toList (Set Token -> [Token]) -> Set Token -> [Token]
forall a b. (a -> b) -> a -> b
$ [Set Token] -> Set Token
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set Token] -> Set Token) -> [Set Token] -> Set Token
forall a b. (a -> b) -> a -> b
$ (Annoted CASLFORMULA -> Set Token)
-> [Annoted CASLFORMULA] -> [Set Token]
forall a b. (a -> b) -> [a] -> [b]
map (CASLFORMULA -> Set Token
collectVars (CASLFORMULA -> Set Token)
-> (Annoted CASLFORMULA -> CASLFORMULA)
-> Annoted CASLFORMULA
-> Set Token
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted CASLFORMULA -> CASLFORMULA
forall a. Annoted a -> a
item) [Annoted CASLFORMULA]
phis
        vars :: BASIC_ITEMS b s f
vars = [VAR_DECL] -> Range -> BASIC_ITEMS b s f
forall b s f. [VAR_DECL] -> Range -> BASIC_ITEMS b s f
Var_items (if [Token] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Token]
usedVars then []
                           else [[Token] -> SORT -> Range -> VAR_DECL
Var_decl [Token]
usedVars SORT
universe Range
nullRange])
                         Range
nullRange