{- |
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