{- |

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 = toId "U" nullRange

llRange :: RangedLL -> Range

llRange (RangedLL p _ q) = Range [fromSourcePos p, fromSourcePos q]

-- | translation of formulas

kif2CASLFormula :: RangedLL -> CASLFORMULA

kif2CASLFormula rl@(RangedLL _ x _) = let r = llRange rl in case x of

List (pr@(RangedLL _ (Literal KToken p) _) : phis) -> case (p, phis) of

("and", _) -> Junction Con (map kif2CASLFormula phis) r

("or", _) -> Junction Dis (map kif2CASLFormula phis) r

("=>", [phi1, phi2]) ->

Relation (kif2CASLFormula phi1) Implication (kif2CASLFormula phi2) r

("<=>", [phi1, phi2]) ->

Relation (kif2CASLFormula phi1) Equivalence (kif2CASLFormula phi2) r

("not", [phi]) -> Negation (kif2CASLFormula phi) r

("True", []) -> Atom True r

("False", []) -> Atom False r

("exists", [RangedLL _ (List vl) _, phi]) ->

Quantification Existential (kif2CASLvardeclList vl) (kif2CASLFormula phi)

r

("forall", [RangedLL _ (List vl) _, phi]) ->

Quantification Universal (kif2CASLvardeclList vl) (kif2CASLFormula phi)

r

("equal", [t1, t2]) ->

Equation (kif2CASLTerm t1) Strong (kif2CASLTerm t2) r

_ -> Predication (Pred_name (toId p $ llRange pr))

(map kif2CASLTerm phis) r

-- also translate 2nd order applications to 1st order, using holds predicate

List l -> Predication (Pred_name (toId "holds" r))

(map kif2CASLTerm l) r

-- a variable in place of a formula; coerce from Booleans

Literal k v | elem k [QWord, AtWord] ->

Equation (Mixfix_token $ toVar v r) Strong trueTerm r

_ -> error $ "kif2CASLFormula : cannot translate " ++ show x

trueTerm :: TERM ()

trueTerm = varOrConst $ mkSimpleId "True"

falseTerm :: TERM ()

falseTerm = varOrConst $ mkSimpleId "False"

toVar :: String -> Range -> Token

toVar v = toSId $ 'v' : tail v

toId :: String -> Range -> Id

toId s = simpleIdToId . toSId s

-- | convert a string to a legal CASL identifier

toSId :: String -> Range -> Token

toSId s = Token $ case parse (reserved (casl_reserved_words

++ formula_words) scanAnyWords >> eof)

"Kif2CASL.toId" s of

Left _ -> 'a' : concatMap ( \ c -> '_' : Map.findWithDefault [c] c

(Map.insert '_' "U" charMap)) s

Right _ -> s

kif2CASLTerm :: RangedLL -> TERM ()

kif2CASLTerm rl@(RangedLL _ x _) = let r = llRange rl in case x of

Literal k v | elem k [QWord, AtWord] -> Mixfix_token $ toVar v r

Literal _ s -> varOrConst $ toSId s r

-- a formula in place of a term; coerce to Booleans

List (rf@(RangedLL _ (Literal _ f) _) : args) ->

if f `elem` ["forall", "exists"] -- ,"and","or","=>","<=>","not"]

then Conditional trueTerm

(kif2CASLFormula rl) falseTerm r

else Application (Op_name $ toId f $ llRange rf)

(map kif2CASLTerm args) r

_ -> error $ "kif2CASLTerm : cannot translate " ++ show (ppRangedLL rl)

-- | translation of variable declaration lists

kif2CASLvardeclList :: [RangedLL] -> [VAR_DECL]

kif2CASLvardeclList = map kif2CASLvardecl

-- | translation of variable declarations

kif2CASLvardecl :: RangedLL -> VAR_DECL

kif2CASLvardecl rl@(RangedLL _ l _) = let r = llRange rl in case l of

Literal _ v -> Var_decl [toVar v r] universe r

_ -> error $ "kif2CASLvardecl " ++ show (ppListOfList l)

-- | first pass of translation, just collecting the formulas

kif2CASLpass1 :: [RangedLL] -> [Annoted CASLFORMULA]

kif2CASLpass1 [] = []

kif2CASLpass1 (phi : rest) =

(emptyAnno phi') { r_annos = annos } : kif2CASLpass1 rest'

where phi' = kif2CASLFormula phi

(annos, rest') = skipComments [] rest

-- | check for comment

isKifComment :: ListOfList -> Bool

isKifComment (List (RangedLL _ (Literal KToken "documentation") _ : _)) = True

isKifComment _ = False

-- | convert comment to annotation

toAnno :: ListOfList -> Annotation

toAnno (List (_ : l)) =

Unparsed_anno Comment_start

(Group_anno [show $ Doc.vcat $ map ppRangedLL l]) nullRange

toAnno _ = error "Kif2CASL.toAnno: wrong format of comment"

-- | skip the first comments; they belong to the whole file

skipComments :: [Annotation] -> [RangedLL] -> ([Annotation], [RangedLL])

skipComments acc [] = (reverse acc, [])

skipComments acc l@(RangedLL _ x _ : rest) =

if isKifComment x

then skipComments (toAnno x : acc) rest

else (reverse acc, l)

data Predsym = Predsym Int PRED_NAME

deriving (Eq, Ord, Show)

sameArity :: Predsym -> Predsym -> Bool

sameArity (Predsym m _) (Predsym n _) = m == n

getName :: Predsym -> PRED_NAME

getName (Predsym _ p) = p

-- | collect all predicate symbols used in a formula

collectPreds :: CASLFORMULA -> Set.Set Predsym

collectPreds = foldFormula

(constRecord (error "Kif2CASL.collectPreds") Set.unions Set.empty)

{ foldPredication = \ _ p args _ -> Set.insert

(Predsym (length args)

(case p of

Pred_name pn -> pn

Qual_pred_name pn _ _ -> pn))

(Set.unions args) }

collectVars :: CASLFORMULA -> Set.Set Token

collectVars = foldFormula

(constRecord (error "Kif2CASL.collectVars") Set.unions Set.empty)

{ foldMixfix_token = const Set.singleton

, foldQuantification = \ _ _ vs rs _ ->

Set.difference rs . Set.fromList

$ concatMap (\ (Var_decl v _ _) -> v) vs

}

data Opsym = Opsym Int OP_NAME

deriving (Eq, Ord, Show)

sameOpArity :: Opsym -> Opsym -> Bool

sameOpArity (Opsym m _) (Opsym n _) = m == n

getOpName :: Opsym -> OP_NAME

getOpName (Opsym _ p) = p

collectOps :: CASLFORMULA -> Set.Set Opsym

collectOps = foldFormula

(constRecord (error "Kif2CASL.collectConsts") Set.unions Set.empty)

{ foldApplication = \ _ o l _ ->

Set.insert (Opsym (length l) (case o of

Op_name i -> i

Qual_op_name i _ _ -> i) )

(Set.unions l) }

nonEmpty :: Annoted (BASIC_ITEMS () () ()) -> Bool

nonEmpty bi = case item bi of

Sig_items (Sort_items _ l _) -> not (null l)

Sig_items (Op_items l _) -> not (null l)

Sig_items (Pred_items l _) -> not (null l)

Var_items l _ -> not (null l)

Axiom_items l _ -> not (null l)

_ -> True

-- | main translation function

kif2CASL :: [RangedLL] -> BASIC_SPEC () () ()

kif2CASL l = Basic_spec $ filter nonEmpty

[(emptyAnno sorts) { l_annos = ans },

emptyAnno ops, emptyAnno preds,

emptyAnno vars, emptyAnno axs]

where (ans, rest) = skipComments [] l

phis = kif2CASLpass1 rest

axs = Axiom_items phis nullRange

preds = Sig_items $ Pred_items preddecls nullRange

predsyms = Set.toList $ Set.unions $ map (collectPreds . item) phis

preddecls = map (emptyAnno . mkPreddecl)

$ List.groupBy sameArity predsyms

mkPreddecl [] = error "kif2CASL: this cannot happen"

mkPreddecl psyms@(Predsym arity _ : _) =

Pred_decl (map getName psyms)

(Pred_type (replicate arity universe) nullRange)

nullRange

sorts =

Sig_items $ Sort_items NonEmptySorts [emptyAnno sortdecl] nullRange

sortdecl = Sort_decl [universe] nullRange

ops = Sig_items $ Op_items opdecls nullRange

opsyms = Set.toList $ Set.unions $ map (collectOps . item) phis

opdecls = map (emptyAnno . mkOpdecl) (List.groupBy sameOpArity opsyms)

mkOpdecl [] = error "kif2CASL: this cannot happen"

mkOpdecl opsms@(Opsym arity _ : _) =

Op_decl (map getOpName opsms)

(Op_type Total (replicate arity universe) universe nullRange)

[] nullRange

usedVars = Set.toList $ Set.unions $ map (collectVars . item) phis

vars = Var_items (if null usedVars then []

else [Var_decl usedVars universe nullRange])

nullRange