4751N/A{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}

4751N/A{- |

4751N/AModule : ./Comorphisms/SoftFOL2CommonLogic.hs

4751N/ADescription : Coding of SoftFOL into CommonLogic

4751N/ACopyright : (c) Eugen Kuksa and Uni Bremen 2011

4751N/ALicense : GPLv2 or higher, see LICENSE.txt

4751N/A

4751N/AMaintainer : eugenk@informatik.uni-bremen.de

4751N/AStability : experimental

4751N/APortability : non-portable (imports Logic.Logic)

6982N/A

6982N/AThe translating comorphism from SoftFOL to CommonLogic.

4751N/A-}

4751N/A

4751N/Amodule Comorphisms.SoftFOL2CommonLogic

4751N/A (

6982N/A SoftFOL2CommonLogic (..)

6982N/A )

6982N/A where

6982N/A

4751N/Aimport Data.Maybe (maybeToList)

4751N/A

4751N/Aimport Common.ProofTree

4751N/Aimport Common.Id

5061N/Aimport Common.Result

5821N/Aimport Common.Utils (concatMapM)

4751N/Aimport qualified Common.AS_Annotation as AS_Anno

4751N/Aimport qualified Common.DefaultMorphism as DefaultMorphism

4751N/Aimport qualified Common.Lib.Rel as Rel

4751N/A

4751N/Aimport Logic.Logic

4751N/Aimport Logic.Comorphism

4751N/A

4751N/Aimport qualified Data.Set as Set

4751N/Aimport qualified Data.Map as Map

4751N/A

4751N/A-- SoftFOL

4751N/Aimport qualified SoftFOL.Logic_SoftFOL as FOLLogic

4751N/Aimport qualified SoftFOL.Sign as FOLSign

4751N/A

4751N/A-- CommonLogic

4751N/Aimport CommonLogic.AS_CommonLogic

4751N/Aimport qualified CommonLogic.Logic_CommonLogic as ClLogic

4751N/Aimport qualified CommonLogic.Sign as ClSign

4751N/Aimport qualified CommonLogic.Symbol as ClSymbol

4751N/Aimport qualified CommonLogic.Morphism as ClMor

4751N/Aimport qualified CommonLogic.Sublogic as ClSL

4751N/A

4751N/A-- | lid of the morphism

4751N/Adata SoftFOL2CommonLogic = SoftFOL2CommonLogic deriving Show

4751N/A

4751N/Ainstance Language SoftFOL2CommonLogic where

4751N/A language_name SoftFOL2CommonLogic = "SoftFOL2CommonLogic"

4751N/A

4751N/Ainstance Comorphism SoftFOL2CommonLogic

4751N/A FOLLogic.SoftFOL -- lid domain

4751N/A () -- sublogics codomain

4751N/A [FOLSign.TPTP] -- Basic spec domain

4751N/A FOLSign.Sentence -- sentence domain

4751N/A () -- symbol items domain

4751N/A () -- symbol map items domain

4751N/A FOLSign.Sign -- signature domain

4751N/A FOLSign.SoftFOLMorphism -- morphism domain

4751N/A FOLSign.SFSymbol -- symbol domain

4751N/A () -- rawsymbol domain

4751N/A ProofTree -- proof tree codomain

4751N/A ClLogic.CommonLogic -- lid domain

4751N/A ClSL.CommonLogicSL -- sublogics codomain

4751N/A BASIC_SPEC -- Basic spec domain

4751N/A TEXT_META -- sentence domain

4751N/A SYMB_ITEMS -- symb_items

4751N/A SYMB_MAP_ITEMS -- symbol map items domain

4751N/A ClSign.Sign -- signature domain

4751N/A ClMor.Morphism -- morphism domain

4751N/A ClSymbol.Symbol -- symbol domain

4751N/A ClSymbol.Symbol -- rawsymbol domain

4751N/A ProofTree -- proof tree codomain

4751N/A where

4751N/A sourceLogic SoftFOL2CommonLogic = FOLLogic.SoftFOL

4751N/A sourceSublogic SoftFOL2CommonLogic = ()

4751N/A targetLogic SoftFOL2CommonLogic = ClLogic.CommonLogic

4751N/A mapSublogic SoftFOL2CommonLogic = Just . mapSub

4751N/A map_theory SoftFOL2CommonLogic = mapTheory

4751N/A map_sentence SoftFOL2CommonLogic = mapSentence

4751N/A map_morphism SoftFOL2CommonLogic = mapMor

4751N/A

4751N/AmapSub :: () -> ClSL.CommonLogicSL

4751N/AmapSub _ = ClSL.folsl

4751N/A

4751N/AmapMor :: FOLSign.SoftFOLMorphism -> Result ClMor.Morphism

4751N/AmapMor mor =

4751N/A let src = mapSign $ DefaultMorphism.domOfDefaultMorphism mor

4751N/A tgt = mapSign $ DefaultMorphism.codOfDefaultMorphism mor

4751N/A pmp = Map.empty

4751N/A in return $ ClMor.Morphism src tgt pmp

4751N/A

5061N/AmapSentence :: FOLSign.Sign -> FOLSign.Sentence -> Result TEXT_META

4751N/AmapSentence = translate

4751N/A

4751N/AmapSign :: FOLSign.Sign -> ClSign.Sign

4751N/AmapSign sig =

4751N/A let items = Set.map (\ t -> mkId [t]) $ Set.fromList $ concat

4751N/A [ Map.keys $ FOLSign.sortMap sig

4751N/A , Map.keys $ FOLSign.funcMap sig

4751N/A , Map.keys $ FOLSign.predMap sig

4751N/A ]

4751N/A in ClSign.emptySig { ClSign.discourseNames = items }

4751N/A

4751N/A-- | translates SoftFOL-theories to CL-theories keeping their names

4751N/AmapTheory :: (FOLSign.Sign, [AS_Anno.Named FOLSign.Sentence])

4751N/A -> Result (ClSign.Sign, [AS_Anno.Named TEXT_META])

4751N/AmapTheory (srcSign, srcFormulas) = do

4751N/A trans_fs <- mapM (transSnd . senAndName) srcFormulas

4751N/A return (mapSign srcSign, signToTexts srcSign

4751N/A ++ map (uncurry AS_Anno.makeNamed) trans_fs)

4751N/A where senAndName :: AS_Anno.Named FOLSign.Sentence -> (String, FOLSign.Sentence)

4751N/A senAndName f = (AS_Anno.senAttr f, AS_Anno.sentence f)

4751N/A transSnd :: (String, FOLSign.Sentence) -> Result (String, TEXT_META)

4751N/A transSnd (s, f) = do

4751N/A tm <- translate srcSign f

4751N/A return (s, tm)

4751N/A

4751N/A-- translates a SoftFOL-theory to a CL-Text

4751N/Atranslate :: FOLSign.Sign -> FOLSign.Sentence -> Result TEXT_META

4751N/Atranslate s f = do

4751N/A sen <- trmToSen s f

4751N/A return $ emptyTextMeta { getText = Text [Sentence sen] nullRange }

4751N/A

4751N/AsignToTexts :: FOLSign.Sign -> [AS_Anno.Named TEXT_META]

4751N/AsignToTexts srcSign =

4751N/A let sr = sortRelText $ Rel.toMap $ FOLSign.sortRel srcSign

4751N/A fm = funcMapText $ FOLSign.funcMap srcSign

4751N/A pm = predMapText $ FOLSign.predMap srcSign

4751N/A in concat

4751N/A [ map (AS_Anno.makeNamed sortRelTrS) (maybeToList sr)

5821N/A , map (AS_Anno.makeNamed funcMapTrS) (maybeToList fm)

4751N/A , map (AS_Anno.makeNamed predMapTrS) (maybeToList pm)

4751N/A ]

4751N/A

4751N/A-- creates one-sentence-phrases: forall x. (subSort x) => (superSort x)

4751N/AsortRelText :: Map.Map FOLSign.SPIdentifier (Set.Set FOLSign.SPIdentifier)

4751N/A -> Maybe TEXT_META

4751N/AsortRelText m =

4751N/A let ps = Map.foldWithKey (\ subSrt set phrs ->

4751N/A Set.fold (\ superSrt phrs2 ->

4751N/A Sentence (Quant_sent Universal [Name xName]

4751N/A (Bool_sent (BinOp Implication

4751N/A (predicateNames subSrt [xName])

4751N/A (predicateNames superSrt [xName])

4751N/A ) nullRange) nullRange)

4751N/A : phrs2) [] set

4751N/A ++ phrs) [] m

4751N/A in if null ps

4751N/A then Nothing

4751N/A else Just $ emptyTextMeta { getText = Named_text (mkSimpleId sortRelTrS)

(Text ps nullRange) nullRange

}

typesWithIndv :: [Token] -> [(Token, NAME)] -- (type, individual)

typesWithIndv args =

foldr (\ (a, i) resArg -> (a, indv a i) : resArg) [] $ zip args [0 ..]

{- creates one-sentence-phrases:

forall x y z. (if (and (T1 x) (T2 y) (T3 z)) (T4 f[x,y,z])) -}

funcMapText :: Map.Map Token (Set.Set ([Token], Token)) -> Maybe TEXT_META

funcMapText m =

let ps = Map.foldWithKey (\ f set phrs ->

Set.fold (\ (args, res) phrs2 ->

let argsAndNames = typesWithIndv args

in Sentence (

if null args

then predicateNames res [f]

else

Quant_sent Universal

(map (Name . snd) argsAndNames) (

Bool_sent (BinOp Implication

(Bool_sent (Junction Conjunction $

map (\ (p, x) -> predicateNames p [x]) argsAndNames

) nullRange)

(Atom_sent (Atom

(Name_term res)

[Term_seq $ Funct_term (Name_term f) (

map (Term_seq . Name_term . snd) argsAndNames

) nullRange]

) nullRange)

) nullRange

) nullRange)

: phrs2) [] set

++ phrs) [] m

in if null ps

then Nothing

else Just $ emptyTextMeta { getText = Named_text (mkSimpleId funcMapTrS)

(Text ps nullRange) nullRange

}

{- creates one-sentence-phrases:

forall x y z. (P[x,y,z]) => (and (T1 x) (T2 y) (T3 z)) -}

predMapText :: Map.Map Token (Set.Set [Token]) -> Maybe TEXT_META

predMapText m =

let ps = Map.foldWithKey (\ prd set phrs ->

Set.fold (\ args phrs2 ->

let argsAndNames = typesWithIndv args

in Sentence (Quant_sent Universal

(map (Name . snd) argsAndNames) (

Bool_sent (BinOp Implication

(predicateNames prd (map snd argsAndNames))

(Bool_sent (Junction Conjunction $

map (\ (p, x) -> predicateNames p [x]) argsAndNames

) nullRange)

) nullRange

) nullRange)

: phrs2) [] set

++ phrs) [] m

in if null ps

then Nothing

else Just $ emptyTextMeta { getText = Named_text

(mkSimpleId predMapTrS)

(Text ps nullRange)

nullRange

}

trmToSen :: FOLSign.Sign -> FOLSign.SPTerm -> Result SENTENCE

trmToSen s t = case t of

FOLSign.SPQuantTerm qsym vl f -> quantTrm s qsym vl f

FOLSign.SPComplexTerm sym args -> case sym of

FOLSign.SPEqual -> case args of

[x, y] -> toEquation (x, y)

l@(_ : _ : _) -> do

eqs <- mapM toEquation $ zip l $ tail l

return $ Bool_sent (Junction Conjunction eqs) nullRange

x -> fail $ "equation needs at least two arguments, but found: " ++ show x

FOLSign.SPTrue -> return clTrue

FOLSign.SPFalse -> return clFalse

FOLSign.SPOr -> do

sens <- mapM (trmToSen s) args

return $ Bool_sent (Junction Disjunction sens) nullRange

FOLSign.SPAnd -> do

sens <- mapM (trmToSen s) args

return $ Bool_sent (Junction Conjunction sens) nullRange

FOLSign.SPNot -> case args of

[x] -> do

sen <- trmToSen s x

return $ Bool_sent (Negation sen) nullRange

_ -> fail $

"negation can only be applied to a single argument, but found: "

++ show t

FOLSign.SPImplies -> case args of

[x, y] -> do

sen1 <- trmToSen s x

sen2 <- trmToSen s y

return $ Bool_sent (BinOp Implication sen1 sen2) nullRange

_ -> fail $

"implication can only be applied to two arguments, but found: "

++ show t

FOLSign.SPImplied -> case args of

[x, y] -> do

sen1 <- trmToSen s x

sen2 <- trmToSen s y

return $ Bool_sent (BinOp Implication sen2 sen1) nullRange

_ -> fail $

"implication can only be applied to two arguments, but found: "

++ show t

FOLSign.SPEquiv -> case args of

[x, y] -> do

sen1 <- trmToSen s x

sen2 <- trmToSen s y

return $ Bool_sent (BinOp Biconditional sen1 sen2) nullRange

_ -> fail $

"equivalence can only be applied to two arguments, but found: "

++ show t

_ -> predicateSPTerms (symToTerm sym) args

-- | converts SPEquation to a CL-Equation

toEquation :: (FOLSign.SPTerm, FOLSign.SPTerm) -> Result SENTENCE

toEquation (x, y) = do

trmx <- trmToTerm x

trmy <- trmToTerm y

return $ Atom_sent (Equation trmx trmy) nullRange

predicateSPTerms :: TERM -> [FOLSign.SPTerm] -> Result SENTENCE

predicateSPTerms t args = do

tseqs <- mapM trmToTermSeq args

return $ Atom_sent (Atom t tseqs) nullRange

predicateNames :: NAME -> [NAME] -> SENTENCE

predicateNames p xs =

Atom_sent (Atom (Name_term p) (map (Term_seq . Name_term) xs)) nullRange

predicateTerm :: NAME -> TERM -> SENTENCE

predicateTerm p xs = Atom_sent (Atom (Name_term p) [Term_seq xs]) nullRange

{- Converts a quantified FOL-term to a CL-Quant_sent. Quantifier arguments

contain only the inner-most arguments of the SoftFOL Quantifier in order to

convert sentences like

@forall s(Y1), t(u(Y2)) . Y1 /= Y2@

to

@forall Y1, Y2 . S(Y1) & T(u(Y2)) & U(Y2) => Y1 /= Y2@

where S, T and U are the types that Y1, u(Y2) and Y2 must have

in order to apply functions/predicates s, t and u to them (defined in

funcMap and predMap). -}

quantTrm :: FOLSign.Sign -> FOLSign.SPQuantSym

-> [FOLSign.SPTerm] -> FOLSign.SPTerm -> Result SENTENCE

quantTrm sig qsymm vs f = do

let functions_quant = filter (not . isNullary) vs

let trans_vs = concatMap trmToNameSeq vs

trans_f <- if null functions_quant

then trmToSen sig f

else do

sen1 <- typeSentence sig functions_quant

sen2 <- trmToSen sig f

return $ Bool_sent (BinOp Implication sen1 sen2) nullRange

quantifier <- case qsymm of

FOLSign.SPForall -> return Universal

FOLSign.SPExists -> return Existential

_ -> fail "custom quantifiers not allowed"

return $ Quant_sent quantifier trans_vs trans_f nullRange

typeSentence :: FOLSign.Sign -> [FOLSign.SPTerm] -> Result SENTENCE

typeSentence sig vs = case vs of

[] -> return clTrue

[v] -> typeSentence1 sig v -- v = f(x,y,z)

_ -> do

sens <- mapM (typeSentence1 sig) vs

return $ Bool_sent (Junction Conjunction sens) nullRange

typeSentence1 :: FOLSign.Sign -> FOLSign.SPTerm -> Result SENTENCE

typeSentence1 sig v = case v of

FOLSign.SPComplexTerm _ [] ->

fail "bug (typeSentence1): nullary functions should not occur here"

FOLSign.SPComplexTerm sym args -> typeSentenceGetTypes sig (symToName sym) args

FOLSign.SPQuantTerm {} ->

fail "quantification not allowed in bound variable list"

typeSentenceGetTypes :: FOLSign.Sign -> FOLSign.SPIdentifier -> [FOLSign.SPTerm]

-> Result SENTENCE

typeSentenceGetTypes sig symN args =

case Map.lookup symN $ FOLSign.funcMap sig of

Nothing -> case Map.lookup symN $ FOLSign.predMap sig of

Nothing -> case Map.lookup symN $ FOLSign.sortMap sig of

Nothing -> fail $ "symbol has no type: " ++ show symN

Just _ -> typeSentencesSort args symN

Just ts -> typeSentencesDisjPred sig args $ Set.elems ts

Just ts -> typeSentencesDisjFunc sig args $ Set.elems ts

typeSentencesSort :: [FOLSign.SPTerm] -> FOLSign.SPIdentifier

-> Result SENTENCE

typeSentencesSort args srt = case args of

[] -> fail $ "no arguments for sort " ++ show srt

[arg] -> do

funtrm <- trmToFunctTrm arg

return $ predicateTerm srt funtrm

_ -> do

sens <- mapM (\ arg -> do

funtrm <- trmToFunctTrm arg

return $ predicateTerm srt funtrm

) args

return $ Bool_sent (Junction Conjunction sens) nullRange

typeSentencesDisjPred :: FOLSign.Sign -> [FOLSign.SPTerm]

-> [[FOLSign.SPIdentifier]]

-> Result SENTENCE

typeSentencesDisjPred sig args typeSet = case typeSet of

[t] -> tsdp1 t

_ -> do

sens <- mapM tsdp1 typeSet

return $ Bool_sent (Junction Disjunction sens) nullRange

where tsdp1 :: [FOLSign.SPIdentifier] -> Result SENTENCE

tsdp1 t = do

sens <- mapM (\ (arg, argType) -> case arg of

FOLSign.SPComplexTerm _ [] ->

return $ predicateNames argType [trmToName arg]

FOLSign.SPComplexTerm _ _ ->

typeSentence1 sig arg

FOLSign.SPQuantTerm {} ->

fail "quantification not allowed in quantifier-argument list"

) $ zip args t

return $ Bool_sent (Junction Conjunction sens) nullRange

typeSentencesDisjFunc :: FOLSign.Sign -> [FOLSign.SPTerm]

-> [([FOLSign.SPIdentifier], FOLSign.SPIdentifier)]

-> Result SENTENCE

typeSentencesDisjFunc sig args typeSet = case typeSet of

[t] -> tsdf1 t

_ -> do

sens <- mapM tsdf1 typeSet

return $ Bool_sent (Junction Disjunction sens) nullRange

where tsdf1 :: ([FOLSign.SPIdentifier], FOLSign.SPIdentifier) -> Result SENTENCE

tsdf1 (t, resType) = do

sens <- concatMapM (\ (arg, argType) -> case arg of

FOLSign.SPComplexTerm _ [] ->

return [predicateNames argType [trmToName arg]]

FOLSign.SPComplexTerm _ _ -> do

funtrm <- trmToFunctTrm arg

typsen <- typeSentence1 sig arg

return [predicateTerm resType funtrm, typsen]

FOLSign.SPQuantTerm {} ->

fail "quantification not allowed in quantifier-argument list"

) $ zip args t

return $ Bool_sent (Junction Conjunction sens) nullRange

trmToName :: FOLSign.SPTerm -> NAME

trmToName t = case t of

FOLSign.SPComplexTerm sym _ -> symToName sym

x -> error $ "quantification not convertible to a name: " ++ show x

{- converts an @SPTerm@ to @[NAME_OR_SEQMARK]@ as an argument for a quantifier

using only the inner-most arguments -}

trmToNameSeq :: FOLSign.SPTerm -> [NAME_OR_SEQMARK]

trmToNameSeq t = case t of

FOLSign.SPComplexTerm sym [] -> [Name $ symToName sym]

FOLSign.SPComplexTerm _ args -> concatMap trmToNameSeq args

FOLSign.SPQuantTerm {} ->

error "quantification not allowed in quantifier-argument list"

-- converts an SPTerm to a TERM, i.e. for the arguments of an equation

trmToTerm :: FOLSign.SPTerm -> Result TERM

trmToTerm t = case t of

FOLSign.SPQuantTerm {} -> fail "quantification not allowed for a term"

FOLSign.SPComplexTerm _ [] -> return $ Name_term $ trmToName t

FOLSign.SPComplexTerm _ _ -> trmToFunctTrm t

-- Converts an SPTerm to TERM_SEQ as an argument for a quantifier

trmToTermSeq :: FOLSign.SPTerm -> Result TERM_SEQ

trmToTermSeq t = case t of

FOLSign.SPComplexTerm _ _ -> do

tseq <- trmToTerm t

return $ Term_seq tseq

FOLSign.SPQuantTerm {} ->

fail "quantification not allowed in argument list"

trmToFunctTrm :: FOLSign.SPTerm -> Result TERM

trmToFunctTrm t = case t of

FOLSign.SPComplexTerm sym args ->

if null args

then return $ symToTerm sym

else do

tseq <- mapM trmToTermSeq args

return $ Funct_term (symToTerm sym) tseq nullRange

FOLSign.SPQuantTerm {} ->

fail "quantification not allowed in quantifier-argument list"

-- | converts a custom symbol to a NAME, used in

symToName :: FOLSign.SPSymbol -> NAME

symToName s = case s of

FOLSign.SPCustomSymbol i -> i

FOLSign.SPID -> idName

FOLSign.SPDiv -> divName

FOLSign.SPComp -> compName

FOLSign.SPSum -> sumName

FOLSign.SPConv -> convName

x -> error $ "symbol not convertible to a name: " ++ show x

symToTerm :: FOLSign.SPSymbol -> TERM

symToTerm s = Name_term $ symToName s

isNullary :: FOLSign.SPTerm -> Bool

isNullary t = case t of

FOLSign.SPComplexTerm _ [] -> True

_ -> False

-- representation for true in CL

clTrue :: SENTENCE -- forall x. x=x

clTrue = Quant_sent Universal [Name xName]

(Atom_sent (Equation (Name_term xName) (Name_term xName)) nullRange

) nullRange

-- representation for false in CL

clFalse :: SENTENCE

clFalse = Bool_sent (Negation clTrue) nullRange

-- creates an individual-name out of a NAME by appending "_i" to it

indv :: NAME -> Int -> NAME

indv n i = mkSimpleId (tokStr n ++ "_item_" ++ show i)

-- simple names

xName :: NAME

xName = mkSimpleId "x"

idName :: NAME

idName = mkSimpleId "ID"

divName :: NAME

divName = mkSimpleId "DIV"

compName :: NAME

compName = mkSimpleId "COMP"

sumName :: NAME

sumName = mkSimpleId "SUM"

convName :: NAME

convName = mkSimpleId "CONV"

-- Text-Names

sortRelTrS :: String

sortRelTrS = "SoftFOL_SubsortRelations"

funcMapTrS :: String

funcMapTrS = "SoftFOL_FunctionMaps"

predMapTrS :: String

predMapTrS = "SoftFOL_PredicateMaps"