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