d4595617cf3503fb9f2650b3c1e8b338c62c4c91Christian MaederDescription : Translation from ExtModal to Ship
d4595617cf3503fb9f2650b3c1e8b338c62c4c91Christian MaederCopyright : (c) C. Maeder, DFKI GmbH 2012
d4595617cf3503fb9f2650b3c1e8b338c62c4c91Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
d4595617cf3503fb9f2650b3c1e8b338c62c4c91Christian MaederMaintainer : Christian.Maeder@dfki.de
d4595617cf3503fb9f2650b3c1e8b338c62c4c91Christian MaederStability : provisional
d4595617cf3503fb9f2650b3c1e8b338c62c4c91Christian MaederPortability : portable
65cbddb21125ea0e5192819e7abdda4723091bd7Christian MaedertransSid :: Token -> String
65cbddb21125ea0e5192819e7abdda4723091bd7Christian MaedertransSid = transString . show
65cbddb21125ea0e5192819e7abdda4723091bd7Christian MaedertransId :: Id -> String
65cbddb21125ea0e5192819e7abdda4723091bd7Christian MaedertransId = transString . show
65cbddb21125ea0e5192819e7abdda4723091bd7Christian MaedertoFoltl :: FORMULA EM_FORMULA -> Result Foltl
65cbddb21125ea0e5192819e7abdda4723091bd7Christian MaedertoFoltl = foldFormula foltlRec
65cbddb21125ea0e5192819e7abdda4723091bd7Christian MaederfoltlRec :: Record EM_FORMULA (Result Foltl) (Result Foltl)
65cbddb21125ea0e5192819e7abdda4723091bd7Christian MaederfoltlRec = (constRecord extModalToFoltlt (const $ fail "foltlRec1")
65cbddb21125ea0e5192819e7abdda4723091bd7Christian Maeder (fail "foltlRec2"))
65cbddb21125ea0e5192819e7abdda4723091bd7Christian Maeder { foldQuantification = \ _ q vs f _ -> if
65cbddb21125ea0e5192819e7abdda4723091bd7Christian Maeder q == Unique_existential then fail "Unique_existential not supported"
65cbddb21125ea0e5192819e7abdda4723091bd7Christian Maeder else fmap (PreOp $ QuantF
65cbddb21125ea0e5192819e7abdda4723091bd7Christian Maeder (if q == Universal then AllValuesFrom else SomeValuesFrom)
65cbddb21125ea0e5192819e7abdda4723091bd7Christian Maeder $ concatMap (\ (Var_decl l s _) -> map
65cbddb21125ea0e5192819e7abdda4723091bd7Christian Maeder (\ v -> AConcept (transSid v) . CName $ transId s) l) vs)
65cbddb21125ea0e5192819e7abdda4723091bd7Christian Maeder , foldJunction = \ _ j fs _ -> fmap (JoinedF
65cbddb21125ea0e5192819e7abdda4723091bd7Christian Maeder $ if j == Con then IntersectionOf else UnionOf) $ sequence fs
65cbddb21125ea0e5192819e7abdda4723091bd7Christian Maeder , foldRelation = \ _ mf1 r mf2 _ -> do
65cbddb21125ea0e5192819e7abdda4723091bd7Christian Maeder let i = BinOp f1 Impl f2
65cbddb21125ea0e5192819e7abdda4723091bd7Christian Maeder return $ if r == Equivalence then
65cbddb21125ea0e5192819e7abdda4723091bd7Christian Maeder JoinedF IntersectionOf [i, BinOp f2 Impl f1]
65cbddb21125ea0e5192819e7abdda4723091bd7Christian Maeder , foldNegation = \ _ f _ -> fmap (PreOp NotF) f
65cbddb21125ea0e5192819e7abdda4723091bd7Christian Maeder , foldAtom = \ _ b _ -> return $ if b then trueFoltl else falseFoltl
65cbddb21125ea0e5192819e7abdda4723091bd7Christian Maeder , foldPredication = \ (Predication ps as _) _ _ _ -> case as of
d4595617cf3503fb9f2650b3c1e8b338c62c4c91Christian Maeder n <- toNominal a
65cbddb21125ea0e5192819e7abdda4723091bd7Christian Maeder return . ABoxass . AConcept n . CName $ predSymToString ps
d4595617cf3503fb9f2650b3c1e8b338c62c4c91Christian Maeder [a1, a2] -> do
d4595617cf3503fb9f2650b3c1e8b338c62c4c91Christian Maeder n1 <- toNominal a1
d4595617cf3503fb9f2650b3c1e8b338c62c4c91Christian Maeder n2 <- toNominal a2
65cbddb21125ea0e5192819e7abdda4723091bd7Christian Maeder return . ABoxass . ARole n1 n2 . RName $ predSymToString ps
d4595617cf3503fb9f2650b3c1e8b338c62c4c91Christian Maeder _ -> fail "no concept or role"
65cbddb21125ea0e5192819e7abdda4723091bd7Christian Maeder , foldDefinedness = \ _ _ _ -> fail "foltlRec.Definedness"
65cbddb21125ea0e5192819e7abdda4723091bd7Christian Maeder , foldEquation = \ (Equation t1 _ t2 _) _ _ _ _ -> do
65cbddb21125ea0e5192819e7abdda4723091bd7Christian Maeder s1 <- toNominal t1
65cbddb21125ea0e5192819e7abdda4723091bd7Christian Maeder s2 <- toNominal t2
65cbddb21125ea0e5192819e7abdda4723091bd7Christian Maeder return . ABoxass $ AIndividual s1 Same s2
65cbddb21125ea0e5192819e7abdda4723091bd7Christian Maeder , foldMembership = \ (Membership t s _) _ _ _ -> do
65cbddb21125ea0e5192819e7abdda4723091bd7Christian Maeder n <- toNominal t
65cbddb21125ea0e5192819e7abdda4723091bd7Christian Maeder return . ABoxass . AConcept n . CName $ transId s
65cbddb21125ea0e5192819e7abdda4723091bd7Christian Maeder , foldQuantOp = \ _ _ _ _ -> fail "foltlRec.QuantOp"
65cbddb21125ea0e5192819e7abdda4723091bd7Christian Maeder , foldQuantPred = \ _ _ _ _ -> fail "foltlRec.QuantPred"
65cbddb21125ea0e5192819e7abdda4723091bd7Christian MaederextModalToFoltlt :: EM_FORMULA -> Result Foltl
65cbddb21125ea0e5192819e7abdda4723091bd7Christian MaederextModalToFoltlt emf = case emf of
65cbddb21125ea0e5192819e7abdda4723091bd7Christian Maeder PrefixForm p pf _ -> do
65cbddb21125ea0e5192819e7abdda4723091bd7Christian Maeder f <- toFoltl pf
65cbddb21125ea0e5192819e7abdda4723091bd7Christian Maeder NextY True -> return $ PreOp X f
65cbddb21125ea0e5192819e7abdda4723091bd7Christian Maeder StateQuantification True b -> return $ PreOp (if b then G else F) f
65cbddb21125ea0e5192819e7abdda4723091bd7Christian Maeder UntilSince True f1 f2 _ -> do
65cbddb21125ea0e5192819e7abdda4723091bd7Christian Maeder u1 <- toFoltl f1
65cbddb21125ea0e5192819e7abdda4723091bd7Christian Maeder u2 <- toFoltl f2
65cbddb21125ea0e5192819e7abdda4723091bd7Christian Maeder return $ BinOp u1 Until u2
65cbddb21125ea0e5192819e7abdda4723091bd7Christian Maeder _ -> fail "extModalToFoltl"
65cbddb21125ea0e5192819e7abdda4723091bd7Christian MaederpredSymToString :: PRED_SYMB -> String
65cbddb21125ea0e5192819e7abdda4723091bd7Christian MaederpredSymToString = transId . predSymbName
d4595617cf3503fb9f2650b3c1e8b338c62c4c91Christian MaedertoNominal :: TERM EM_FORMULA -> Result String
d4595617cf3503fb9f2650b3c1e8b338c62c4c91Christian MaedertoNominal trm = case trm of
d4595617cf3503fb9f2650b3c1e8b338c62c4c91Christian Maeder Qual_var v _ _ -> return . transString $ show v
d4595617cf3503fb9f2650b3c1e8b338c62c4c91Christian Maeder Sorted_term t _ _ -> toNominal t
d4595617cf3503fb9f2650b3c1e8b338c62c4c91Christian Maeder Cast t _ _ -> toNominal t
d4595617cf3503fb9f2650b3c1e8b338c62c4c91Christian Maeder _ -> fail "no nominal"