2495a079ef0be260bc66490fe9e9ff7e2e6497f1yoshikiDescription : Parser for SUMO (suggested upper merged ontology) .kif files
a99c5d4cc3cab6a62b04d52000dbc22ce1fa2d94coarCopyright : (c) T.Mossakowski, C.Maeder and Uni Bremen 2006
2495a079ef0be260bc66490fe9e9ff7e2e6497f1yoshikiLicense : GPLv2 or higher, see LICENSE.txt
031b91a62d25106ae69d4693475c79618dd5e884fieldingMaintainer : Christian.Maeder@dfki.de
031b91a62d25106ae69d4693475c79618dd5e884fieldingStability : provisional
031b91a62d25106ae69d4693475c79618dd5e884fieldingPortability : portable
031b91a62d25106ae69d4693475c79618dd5e884fieldingParser for SUMO (suggested upper merged ontology) .kif files
d5d794fc2f4cc9ca6d6da17cfa2cdcd8d244bacdndimport qualified Data.List as List
d5d794fc2f4cc9ca6d6da17cfa2cdcd8d244bacdndimport qualified Data.Set as Set
2495a079ef0be260bc66490fe9e9ff7e2e6497f1yoshikiimport qualified Data.Map as Map
208651a016b098f4fa1f6279559f104d70f1632dtakashiimport qualified Text.PrettyPrint.HughesPJ as Doc
208651a016b098f4fa1f6279559f104d70f1632dtakashi-- | the universal sort
208651a016b098f4fa1f6279559f104d70f1632dtakashiuniverse :: SORT
2495a079ef0be260bc66490fe9e9ff7e2e6497f1yoshikiuniverse = toId "U" nullRange
208651a016b098f4fa1f6279559f104d70f1632dtakashillRange :: RangedLL -> Range
208651a016b098f4fa1f6279559f104d70f1632dtakashillRange (RangedLL p _ q) = Range [fromSourcePos p, fromSourcePos q]
208651a016b098f4fa1f6279559f104d70f1632dtakashi-- | translation of formulas
208651a016b098f4fa1f6279559f104d70f1632dtakashikif2CASLFormula :: RangedLL -> CASLFORMULA
208651a016b098f4fa1f6279559f104d70f1632dtakashikif2CASLFormula rl@(RangedLL _ x _) = let r = llRange rl in case x of
208651a016b098f4fa1f6279559f104d70f1632dtakashi List (pr@(RangedLL _ (Literal KToken p) _) : phis) -> case (p, phis) of
2495a079ef0be260bc66490fe9e9ff7e2e6497f1yoshiki ("and", _) -> Junction Con (map kif2CASLFormula phis) r
2495a079ef0be260bc66490fe9e9ff7e2e6497f1yoshiki ("or", _) -> Junction Dis (map kif2CASLFormula phis) r
208651a016b098f4fa1f6279559f104d70f1632dtakashi ("=>", [phi1, phi2]) ->
208651a016b098f4fa1f6279559f104d70f1632dtakashi Relation (kif2CASLFormula phi1) Implication (kif2CASLFormula phi2) r
208651a016b098f4fa1f6279559f104d70f1632dtakashi ("<=>", [phi1, phi2]) ->
208651a016b098f4fa1f6279559f104d70f1632dtakashi Relation (kif2CASLFormula phi1) Equivalence (kif2CASLFormula phi2) r
9b37d999ede3b016119e3042f774a139ed3cd2bakawai ("not", [phi]) -> Negation (kif2CASLFormula phi) r
208651a016b098f4fa1f6279559f104d70f1632dtakashi ("True", []) -> Atom True r
208651a016b098f4fa1f6279559f104d70f1632dtakashi ("False", []) -> Atom False r
208651a016b098f4fa1f6279559f104d70f1632dtakashi ("exists", [RangedLL _ (List vl) _, phi]) ->
9b37d999ede3b016119e3042f774a139ed3cd2bakawai Quantification Existential (kif2CASLvardeclList vl) (kif2CASLFormula phi)
2495a079ef0be260bc66490fe9e9ff7e2e6497f1yoshiki ("forall", [RangedLL _ (List vl) _, phi]) ->
2495a079ef0be260bc66490fe9e9ff7e2e6497f1yoshiki Quantification Universal (kif2CASLvardeclList vl) (kif2CASLFormula phi)
2495a079ef0be260bc66490fe9e9ff7e2e6497f1yoshiki ("equal", [t1, t2]) ->
208651a016b098f4fa1f6279559f104d70f1632dtakashi Equation (kif2CASLTerm t1) Strong (kif2CASLTerm t2) r
c70d1c1ea5807b57db0a06ae4f01495bab2c630bkawai _ -> Predication (Pred_name (toId p $ llRange pr))
208651a016b098f4fa1f6279559f104d70f1632dtakashi (map kif2CASLTerm phis) r
208651a016b098f4fa1f6279559f104d70f1632dtakashi-- also translate 2nd order applications to 1st order, using holds predicate
208651a016b098f4fa1f6279559f104d70f1632dtakashi List l -> Predication (Pred_name (toId "holds" r))
208651a016b098f4fa1f6279559f104d70f1632dtakashi (map kif2CASLTerm l) r
208651a016b098f4fa1f6279559f104d70f1632dtakashi-- a variable in place of a formula; coerce from Booleans
c70d1c1ea5807b57db0a06ae4f01495bab2c630bkawai Literal k v | elem k [QWord, AtWord] ->
208651a016b098f4fa1f6279559f104d70f1632dtakashi Equation (Mixfix_token $ toVar v r) Strong trueTerm r
208651a016b098f4fa1f6279559f104d70f1632dtakashi _ -> error $ "kif2CASLFormula : cannot translate " ++ show x
208651a016b098f4fa1f6279559f104d70f1632dtakashitrueTerm :: TERM ()
208651a016b098f4fa1f6279559f104d70f1632dtakashitrueTerm = varOrConst $ mkSimpleId "True"
208651a016b098f4fa1f6279559f104d70f1632dtakashifalseTerm :: TERM ()
208651a016b098f4fa1f6279559f104d70f1632dtakashifalseTerm = varOrConst $ mkSimpleId "False"
c70d1c1ea5807b57db0a06ae4f01495bab2c630bkawaitoVar :: String -> Range -> Token
c70d1c1ea5807b57db0a06ae4f01495bab2c630bkawaitoVar v = toSId $ 'v' : tail v
c70d1c1ea5807b57db0a06ae4f01495bab2c630bkawaitoId :: String -> Range -> Id
c70d1c1ea5807b57db0a06ae4f01495bab2c630bkawaitoId s = simpleIdToId . toSId s
208651a016b098f4fa1f6279559f104d70f1632dtakashi-- | convert a string to a legal CASL identifier
208651a016b098f4fa1f6279559f104d70f1632dtakashitoSId :: String -> Range -> Token
208651a016b098f4fa1f6279559f104d70f1632dtakashitoSId s = Token $ case parse (reserved (casl_reserved_words
208651a016b098f4fa1f6279559f104d70f1632dtakashi ++ formula_words) scanAnyWords >> eof)
c70d1c1ea5807b57db0a06ae4f01495bab2c630bkawai Left _ -> 'a' : concatMap ( \ c -> '_' : Map.findWithDefault [c] c
c70d1c1ea5807b57db0a06ae4f01495bab2c630bkawai (Map.insert '_' "U" charMap)) s
c70d1c1ea5807b57db0a06ae4f01495bab2c630bkawai Right _ -> s
2495a079ef0be260bc66490fe9e9ff7e2e6497f1yoshikikif2CASLTerm :: RangedLL -> TERM ()
208651a016b098f4fa1f6279559f104d70f1632dtakashikif2CASLTerm rl@(RangedLL _ x _) = let r = llRange rl in case x of
4968dbef150b4e1c59621e1e181ece60c4df550cyoshiki Literal k v | elem k [QWord, AtWord] -> Mixfix_token $ toVar v r
4968dbef150b4e1c59621e1e181ece60c4df550cyoshiki Literal _ s -> varOrConst $ toSId s r
9dca5c120b818e1c51dbbb6c658d95a9f91b524cyoshiki -- a formula in place of a term; coerce to Booleans
9dca5c120b818e1c51dbbb6c658d95a9f91b524cyoshiki List (rf@(RangedLL _ (Literal _ f) _) : args) ->
2495a079ef0be260bc66490fe9e9ff7e2e6497f1yoshiki if f `elem` ["forall", "exists"] -- ,"and","or","=>","<=>","not"]
2495a079ef0be260bc66490fe9e9ff7e2e6497f1yoshiki then Conditional trueTerm
2495a079ef0be260bc66490fe9e9ff7e2e6497f1yoshiki (kif2CASLFormula rl) falseTerm r
208651a016b098f4fa1f6279559f104d70f1632dtakashi else Application (Op_name $ toId f $ llRange rf)
208651a016b098f4fa1f6279559f104d70f1632dtakashi (map kif2CASLTerm args) r
2495a079ef0be260bc66490fe9e9ff7e2e6497f1yoshiki _ -> error $ "kif2CASLTerm : cannot translate " ++ show (ppRangedLL rl)
208651a016b098f4fa1f6279559f104d70f1632dtakashi-- | translation of variable declaration lists
4968dbef150b4e1c59621e1e181ece60c4df550cyoshikikif2CASLvardeclList :: [RangedLL] -> [VAR_DECL]
208651a016b098f4fa1f6279559f104d70f1632dtakashikif2CASLvardeclList = map kif2CASLvardecl
208651a016b098f4fa1f6279559f104d70f1632dtakashi-- | translation of variable declarations
4968dbef150b4e1c59621e1e181ece60c4df550cyoshikikif2CASLvardecl :: RangedLL -> VAR_DECL
4968dbef150b4e1c59621e1e181ece60c4df550cyoshikikif2CASLvardecl rl@(RangedLL _ l _) = let r = llRange rl in case l of
2495a079ef0be260bc66490fe9e9ff7e2e6497f1yoshiki Literal _ v -> Var_decl [toVar v r] universe r
208651a016b098f4fa1f6279559f104d70f1632dtakashi _ -> error $ "kif2CASLvardecl " ++ show (ppListOfList l)
2495a079ef0be260bc66490fe9e9ff7e2e6497f1yoshiki-- | first pass of translation, just collecting the formulas
208651a016b098f4fa1f6279559f104d70f1632dtakashikif2CASLpass1 :: [RangedLL] -> [Annoted CASLFORMULA]
208651a016b098f4fa1f6279559f104d70f1632dtakashikif2CASLpass1 [] = []
208651a016b098f4fa1f6279559f104d70f1632dtakashikif2CASLpass1 (phi : rest) =
208651a016b098f4fa1f6279559f104d70f1632dtakashi (emptyAnno phi') { r_annos = annos } : kif2CASLpass1 rest'
208651a016b098f4fa1f6279559f104d70f1632dtakashi where phi' = kif2CASLFormula phi
2495a079ef0be260bc66490fe9e9ff7e2e6497f1yoshiki (annos, rest') = skipComments [] rest
2b1ca4f3e09956e86d7f7c5b44f2c6f5351d54dbyoshiki-- | check for comment
208651a016b098f4fa1f6279559f104d70f1632dtakashiisKifComment :: ListOfList -> Bool
208651a016b098f4fa1f6279559f104d70f1632dtakashiisKifComment (List (RangedLL _ (Literal KToken "documentation") _ : _)) = True
2b1ca4f3e09956e86d7f7c5b44f2c6f5351d54dbyoshikiisKifComment _ = False
208651a016b098f4fa1f6279559f104d70f1632dtakashi-- | convert comment to annotation
208651a016b098f4fa1f6279559f104d70f1632dtakashitoAnno :: ListOfList -> Annotation
208651a016b098f4fa1f6279559f104d70f1632dtakashitoAnno (List (_ : l)) =
208651a016b098f4fa1f6279559f104d70f1632dtakashi Unparsed_anno Comment_start
2b1ca4f3e09956e86d7f7c5b44f2c6f5351d54dbyoshiki (Group_anno [show $ Doc.vcat $ map ppRangedLL l]) nullRange
208651a016b098f4fa1f6279559f104d70f1632dtakashitoAnno _ = error "Kif2CASL.toAnno: wrong format of comment"
2495a079ef0be260bc66490fe9e9ff7e2e6497f1yoshiki-- | skip the first comments; they belong to the whole file
208651a016b098f4fa1f6279559f104d70f1632dtakashiskipComments :: [Annotation] -> [RangedLL] -> ([Annotation], [RangedLL])
07ab565873bfd241828a89261b1260c448a0799eyoshikiskipComments acc [] = (reverse acc, [])
208651a016b098f4fa1f6279559f104d70f1632dtakashiskipComments acc l@(RangedLL _ x _ : rest) =
208651a016b098f4fa1f6279559f104d70f1632dtakashi if isKifComment x
07ab565873bfd241828a89261b1260c448a0799eyoshiki then skipComments (toAnno x : acc) rest
208651a016b098f4fa1f6279559f104d70f1632dtakashi else (reverse acc, l)
07ab565873bfd241828a89261b1260c448a0799eyoshikidata Predsym = Predsym Int PRED_NAME
07ab565873bfd241828a89261b1260c448a0799eyoshiki deriving (Eq, Ord, Show)
07ab565873bfd241828a89261b1260c448a0799eyoshikisameArity :: Predsym -> Predsym -> Bool
07ab565873bfd241828a89261b1260c448a0799eyoshikisameArity (Predsym m _) (Predsym n _) = m == n
07ab565873bfd241828a89261b1260c448a0799eyoshikigetName :: Predsym -> PRED_NAME
07ab565873bfd241828a89261b1260c448a0799eyoshikigetName (Predsym _ p) = p
2495a079ef0be260bc66490fe9e9ff7e2e6497f1yoshiki-- | collect all predicate symbols used in a formula
2495a079ef0be260bc66490fe9e9ff7e2e6497f1yoshikicollectPreds :: CASLFORMULA -> Set.Set Predsym
2495a079ef0be260bc66490fe9e9ff7e2e6497f1yoshikicollectPreds = foldFormula
2495a079ef0be260bc66490fe9e9ff7e2e6497f1yoshiki (constRecord (error "Kif2CASL.collectPreds") Set.unions Set.empty)
208651a016b098f4fa1f6279559f104d70f1632dtakashi { foldPredication = \ _ p args _ -> Set.insert
4968dbef150b4e1c59621e1e181ece60c4df550cyoshiki (Predsym (length args)
9dca5c120b818e1c51dbbb6c658d95a9f91b524cyoshiki Pred_name pn -> pn
9dca5c120b818e1c51dbbb6c658d95a9f91b524cyoshiki Qual_pred_name pn _ _ -> pn))
2495a079ef0be260bc66490fe9e9ff7e2e6497f1yoshikicollectVars :: CASLFORMULA -> Set.Set Token
208651a016b098f4fa1f6279559f104d70f1632dtakashicollectVars = foldFormula
208651a016b098f4fa1f6279559f104d70f1632dtakashi (constRecord (error "Kif2CASL.collectVars") Set.unions Set.empty)
208651a016b098f4fa1f6279559f104d70f1632dtakashi { foldMixfix_token = const Set.singleton
208651a016b098f4fa1f6279559f104d70f1632dtakashi , foldQuantification = \ _ _ vs rs _ ->
208651a016b098f4fa1f6279559f104d70f1632dtakashi $ concatMap (\ (Var_decl v _ _) -> v) vs
4968dbef150b4e1c59621e1e181ece60c4df550cyoshikidata Opsym = Opsym Int OP_NAME
4968dbef150b4e1c59621e1e181ece60c4df550cyoshiki deriving (Eq, Ord, Show)
2495a079ef0be260bc66490fe9e9ff7e2e6497f1yoshikisameOpArity :: Opsym -> Opsym -> Bool
2495a079ef0be260bc66490fe9e9ff7e2e6497f1yoshikisameOpArity (Opsym m _) (Opsym n _) = m == n
2495a079ef0be260bc66490fe9e9ff7e2e6497f1yoshikigetOpName :: Opsym -> OP_NAME
2495a079ef0be260bc66490fe9e9ff7e2e6497f1yoshikigetOpName (Opsym _ p) = p
208651a016b098f4fa1f6279559f104d70f1632dtakashicollectOps :: CASLFORMULA -> Set.Set Opsym
4968dbef150b4e1c59621e1e181ece60c4df550cyoshikicollectOps = foldFormula
4968dbef150b4e1c59621e1e181ece60c4df550cyoshiki (constRecord (error "Kif2CASL.collectConsts") Set.unions Set.empty)
9dca5c120b818e1c51dbbb6c658d95a9f91b524cyoshiki { foldApplication = \ _ o l _ ->
9dca5c120b818e1c51dbbb6c658d95a9f91b524cyoshiki Set.insert (Opsym (length l) (case o of
9dca5c120b818e1c51dbbb6c658d95a9f91b524cyoshiki Op_name i -> i
2495a079ef0be260bc66490fe9e9ff7e2e6497f1yoshiki Qual_op_name i _ _ -> i) )
208651a016b098f4fa1f6279559f104d70f1632dtakashinonEmpty :: Annoted (BASIC_ITEMS () () ()) -> Bool
208651a016b098f4fa1f6279559f104d70f1632dtakashinonEmpty bi = case item bi of
208651a016b098f4fa1f6279559f104d70f1632dtakashi Sig_items (Sort_items _ l _) -> not (null l)
208651a016b098f4fa1f6279559f104d70f1632dtakashi Sig_items (Op_items l _) -> not (null l)
208651a016b098f4fa1f6279559f104d70f1632dtakashi Sig_items (Pred_items l _) -> not (null l)
208651a016b098f4fa1f6279559f104d70f1632dtakashi Var_items l _ -> not (null l)
208651a016b098f4fa1f6279559f104d70f1632dtakashi Axiom_items l _ -> not (null l)
4968dbef150b4e1c59621e1e181ece60c4df550cyoshiki-- | main translation function
2495a079ef0be260bc66490fe9e9ff7e2e6497f1yoshikikif2CASL :: [RangedLL] -> BASIC_SPEC () () ()
208651a016b098f4fa1f6279559f104d70f1632dtakashikif2CASL l = Basic_spec $ filter nonEmpty
208651a016b098f4fa1f6279559f104d70f1632dtakashi [(emptyAnno sorts) { l_annos = ans },
208651a016b098f4fa1f6279559f104d70f1632dtakashi emptyAnno ops, emptyAnno preds,
2495a079ef0be260bc66490fe9e9ff7e2e6497f1yoshiki emptyAnno vars, emptyAnno axs]
208651a016b098f4fa1f6279559f104d70f1632dtakashi where (ans, rest) = skipComments [] l
208651a016b098f4fa1f6279559f104d70f1632dtakashi phis = kif2CASLpass1 rest
208651a016b098f4fa1f6279559f104d70f1632dtakashi axs = Axiom_items phis nullRange
208651a016b098f4fa1f6279559f104d70f1632dtakashi preds = Sig_items $ Pred_items preddecls nullRange
2b1ca4f3e09956e86d7f7c5b44f2c6f5351d54dbyoshiki predsyms = Set.toList $ Set.unions $ map (collectPreds . item) phis
208651a016b098f4fa1f6279559f104d70f1632dtakashi preddecls = map (emptyAnno . mkPreddecl)
208651a016b098f4fa1f6279559f104d70f1632dtakashi $ List.groupBy sameArity predsyms
2495a079ef0be260bc66490fe9e9ff7e2e6497f1yoshiki mkPreddecl [] = error "kif2CASL: this cannot happen"
208651a016b098f4fa1f6279559f104d70f1632dtakashi mkPreddecl psyms@(Predsym arity _ : _) =
208651a016b098f4fa1f6279559f104d70f1632dtakashi Pred_decl (map getName psyms)
208651a016b098f4fa1f6279559f104d70f1632dtakashi (Pred_type (replicate arity universe) nullRange)
2495a079ef0be260bc66490fe9e9ff7e2e6497f1yoshiki Sig_items $ Sort_items NonEmptySorts [emptyAnno sortdecl] nullRange
2495a079ef0be260bc66490fe9e9ff7e2e6497f1yoshiki sortdecl = Sort_decl [universe] nullRange
2495a079ef0be260bc66490fe9e9ff7e2e6497f1yoshiki ops = Sig_items $ Op_items opdecls nullRange
208651a016b098f4fa1f6279559f104d70f1632dtakashi opsyms = Set.toList $ Set.unions $ map (collectOps . item) phis
208651a016b098f4fa1f6279559f104d70f1632dtakashi opdecls = map (emptyAnno . mkOpdecl) (List.groupBy sameOpArity opsyms)
2495a079ef0be260bc66490fe9e9ff7e2e6497f1yoshiki mkOpdecl [] = error "kif2CASL: this cannot happen"
2495a079ef0be260bc66490fe9e9ff7e2e6497f1yoshiki mkOpdecl opsms@(Opsym arity _ : _) =
2495a079ef0be260bc66490fe9e9ff7e2e6497f1yoshiki Op_decl (map getOpName opsms)
208651a016b098f4fa1f6279559f104d70f1632dtakashi (Op_type Total (replicate arity universe) universe nullRange)
208651a016b098f4fa1f6279559f104d70f1632dtakashi [] nullRange
2495a079ef0be260bc66490fe9e9ff7e2e6497f1yoshiki usedVars = Set.toList $ Set.unions $ map (collectVars . item) phis
2495a079ef0be260bc66490fe9e9ff7e2e6497f1yoshiki vars = Var_items (if null usedVars then []
2495a079ef0be260bc66490fe9e9ff7e2e6497f1yoshiki else [Var_decl usedVars universe nullRange])