{- |
Module : ./DFOL/Comorphism.hs
Description : Helper functions for the DFOL -> CASL translation
Copyright : (c) Kristina Sojakova, DFKI Bremen 2009
License : GPLv2 or higher, see LICENSE.txt
Maintainer : k.sojakova@jacobs-university.de
Stability : experimental
Portability : portable
-}
module DFOL.Comorphism where
import Common.Id
import Common.AS_Annotation
import qualified Common.Lib.MapSet as MapSet
import qualified Common.Lib.Rel as Rel
import Data.Maybe
import qualified Data.Set as Set
import qualified Data.Map as Map
import DFOL.Sign
import DFOL.AS_DFOL
import DFOL.Morphism
import DFOL.Symbol
import qualified CASL.Sign as CASL_Sign
import qualified CASL.AS_Basic_CASL as CASL_AS
import qualified CASL.Morphism as CASL_Morphism
-- shorthand notation
nr :: Range
nr = nullRange
-- the unique sort
sort :: CASL_AS.SORT
sort = mkId [Token "Sort" nr]
-- the special bot symbol
botTok :: Token
botTok = Token "Bot" nr
bot :: CASL_AS.CASLTERM
bot = CASL_AS.Application (CASL_AS.Qual_op_name (mkId [botTok])
(CASL_AS.Op_type CASL_AS.Total [] sort nr) nr) [] nr
-- constructing a FOL type of the specified arity
folType :: Int -> [CASL_AS.SORT]
folType n = replicate n sort
-- signature map
sigMap :: Sign -> CASL_Sign.CASLSign
sigMap sig =
foldr (sigMapH sig) caslSig2 symbols
where caslSig2 = (CASL_Sign.emptySign ())
, CASL_Sign.opMap = MapSet.insert (mkId [botTok])
(CASL_Sign.sortToOpType sort) MapSet.empty }
symbols = Set.toList $ getSymbols sig
sigMapH :: Sign -> NAME -> CASL_Sign.CASLSign -> CASL_Sign.CASLSign
sigMapH sig sym csig = case kind of
SortKind -> csig
{ CASL_Sign.predMap = insSym (predTy $ arity + 1) predis }
PredKind -> csig { CASL_Sign.predMap = insSym (predTy arity) predis }
FuncKind -> csig
{ CASL_Sign.opMap = MapSet.insert (mkId [sym])
(CASL_Sign.mkTotOpType (folType arity) sort)
$ CASL_Sign.opMap csig }
where predis = CASL_Sign.predMap csig
insSym = MapSet.insert (mkId [sym])
predTy = CASL_Sign.PredType . folType
Just kind = getSymbolKind sym sig
Just arity = getSymbolArity sym sig
-- generating axioms for a translated signature
generateAxioms :: Sign -> [Named CASL_AS.CASLFORMULA]
generateAxioms sig = predAx ++ funcAx ++ sortAx
where sorts = Set.toList $ getSymbolsByKind sig SortKind
funcs = Set.toList $ getSymbolsByKind sig FuncKind
preds = Set.toList $ getSymbolsByKind sig PredKind
sortAx = generateSortAxioms sig sorts
funcAx = generateFuncAxioms sig funcs
predAx = generatePredAxioms sig preds
-- generating axioms for translated predicate symbols
generatePredAxioms :: Sign -> [NAME] -> [Named CASL_AS.CASLFORMULA]
generatePredAxioms = concatMap . generatePredAxiomsH
generatePredAxiomsH :: Sign -> NAME -> [Named CASL_AS.CASLFORMULA]
generatePredAxiomsH sig p =
[makeNamed ("gen_pred_" ++ show p) formula | not $ null argNames]
where Just argNames = getArgumentNames p sig
Just argTypes = getArgumentTypes p sig
args = map makeVar argNames
formula = makeForall
argNames
(CASL_AS.mkNeg (makeTypeHyps argTypes args sig))
(CASL_AS.mkNeg (makePredication p args sig)))
-- generating axioms for translated function symbols
generateFuncAxioms :: Sign -> [NAME] -> [Named CASL_AS.CASLFORMULA]
generateFuncAxioms = concatMap . generateFuncAxiomsH
generateFuncAxiomsH :: Sign -> NAME -> [Named CASL_AS.CASLFORMULA]
generateFuncAxiomsH sig f =
if null argNames
then [makeNamed ("gen_func_1_" ++ show f) formula0]
else [makeNamed ("gen_func_1_" ++ show f) formula1,
makeNamed ("gen_func_2_" ++ show f) formula2]
where Just argNames = getArgumentNames f sig
Just argTypes = getArgumentTypes f sig
Just resultType = getReturnType f sig
args = map makeVar argNames
formula1 = makeForall
argNames
(CASL_AS.mkNeg (makeTypeHyps argTypes args sig))
(CASL_AS.mkStEq (makeApplication f args sig) bot))
formula2 = makeForall
argNames
(makeTypeHyps argTypes args sig)
(makeTypeHyp resultType
(makeApplication f args sig) sig))
formula0 = makeTypeHyp resultType (makeApplication f [] sig) sig
-- generating axioms for translated sort symbols
generateSortAxioms :: Sign -> [NAME] -> [Named CASL_AS.CASLFORMULA]
generateSortAxioms sig ss =
axioms1 ++ axioms2 ++ [axiom3] ++ axioms4
where axioms1 = concatMap (generateSortAxiomsH1 sig) ss
axioms2 = concatMap (generateSortAxiomsH2 sig) ss
axiom3 = generateSortAxiomsH3 sig ss
axioms4 = generateSortAxiomsH4 sig ss
generateSortAxiomsH1 :: Sign -> NAME -> [Named CASL_AS.CASLFORMULA]
generateSortAxiomsH1 sig s =
[makeNamed ("gen_sort_1_" ++ show s) formula | not $ null argNames]
where Just argNames = getArgumentNames s sig
Just argTypes = getArgumentTypes s sig
args = map makeVar argNames
elName = Token "gen_y" nr
el = makeVar elName
formula = makeForall
argNames
(CASL_AS.mkNeg (makeTypeHyps argTypes args sig))
(makeForall
[elName]
(makePredication s (args ++ [el]) sig))))
generateSortAxiomsH2 :: Sign -> NAME -> [Named CASL_AS.CASLFORMULA]
generateSortAxiomsH2 sig s =
if ar == 0
then [makeNamed ("gen_sort_2_" ++ show s) formula0]
else [makeNamed ("gen_sort_2_" ++ show s) formula1,
makeNamed ("gen_sort_3_" ++ show s) formula2]
where Just ar = getSymbolArity s sig
argNames1 = makeArgNames "x" ar
argNames2 = makeArgNames "y" ar
elName = Token "z" nr
args1 = map makeVar argNames1
args2 = map makeVar argNames2
el = makeVar elName
formula1 = makeForall
argNames1
$ CASL_AS.mkNeg $ makePredication s (args1 ++ [bot]) sig
formula2 = makeForall
(argNames1 ++ argNames2 ++ [elName])
[makePredication s (args1 ++ [el]) sig,
makePredication s (args2 ++ [el]) sig])
$ zipWith CASL_AS.mkStEq args1 args2
formula0 = CASL_AS.mkNeg $ makePredication s [bot] sig
generateSortAxiomsH3 :: Sign -> [NAME] -> Named CASL_AS.CASLFORMULA
generateSortAxiomsH3 sig ss =
makeNamed "gen_sort_4" formula
where elName = Token "y" nr
el = makeVar elName
ar s = fromJust $ getSymbolArity s sig
argNames s = makeArgNames "x" (ar s)
args s = map makeVar (argNames s)
formula = makeForall
[elName]
(CASL_AS.mkNeg (CASL_AS.mkStEq el bot))
(CASL_AS.disjunct $ map subformula ss))
subformula s = if ar s == 0
then makePredication s [el] sig
else makeExists
(argNames s)
$ makePredication s (args s ++ [el]) sig
generateSortAxiomsH4 :: Sign -> [NAME] -> [Named CASL_AS.CASLFORMULA]
generateSortAxiomsH4 sig ss =
map (generateSortAxiomsH4H sig) [ (s1, s2) | s1 <- ss, s2 <- ss, s1 < s2 ]
generateSortAxiomsH4H :: Sign -> (NAME, NAME) -> Named CASL_AS.CASLFORMULA
generateSortAxiomsH4H sig (s1, s2) =
makeNamed ("gen_sort_5_" ++ show s1 ++ "_" ++ show s2) formula
where Just ar1 = getSymbolArity s1 sig
Just ar2 = getSymbolArity s2 sig
argNames1 = makeArgNames "x" ar1
argNames2 = makeArgNames "y" ar2
elName = Token "z" nr
args1 = map makeVar argNames1
args2 = map makeVar argNames2
el = makeVar elName
formula = makeForall (argNames1 ++ argNames2 ++ [elName])
$ CASL_AS.mkImpl (makePredication s1 (args1 ++ [el]) sig)
$ CASL_AS.mkNeg $ makePredication s2 (args2 ++ [el]) sig
-- make argument names
makeArgNames :: String -> Int -> [NAME]
makeArgNames var n = map (\ i -> Token (var ++ "_" ++ show i) nr) [1 .. n]
-- make a variable
makeVar :: NAME -> CASL_AS.CASLTERM
makeVar var = CASL_AS.Qual_var var sort nr
-- make an application
makeApplication :: NAME -> [CASL_AS.CASLTERM] -> Sign -> CASL_AS.CASLTERM
makeApplication f as sig =
(mkId [f])
(CASL_AS.Op_type CASL_AS.Total (folType arity) sort nr)
nr)
as
nr
where Just arity = getSymbolArity f sig
-- make a predication
makePredication :: NAME -> [CASL_AS.CASLTERM] -> Sign -> CASL_AS.CASLFORMULA
makePredication p as sig =
(mkId [p])
(CASL_AS.Pred_type (folType arity1) nr)
nr)
as
nr
where Just kind = getSymbolKind p sig
Just arity = getSymbolArity p sig
arity1 = if kind == SortKind then arity + 1 else arity
-- make a universal quantification
makeForall :: [NAME] -> CASL_AS.CASLFORMULA -> CASL_AS.CASLFORMULA
makeForall vars = CASL_AS.mkForall [CASL_AS.Var_decl vars sort nr]
-- make an existential quantification
makeExists :: [NAME] -> CASL_AS.CASLFORMULA -> CASL_AS.CASLFORMULA
makeExists vars = CASL_AS.mkExist [CASL_AS.Var_decl vars sort nr]
-- make a type hypothesis
makeTypeHyp :: TYPE -> CASL_AS.CASLTERM -> Sign -> CASL_AS.CASLFORMULA
makeTypeHyp t term sig = makePredication s (args ++ [term]) sig
where Univ sortterm = t
(s, as) = termFlatForm sortterm
args = map (termTransl sig) as
-- make type hypotheses
makeTypeHyps :: [TYPE] -> [CASL_AS.CASLTERM]
-> Sign -> CASL_AS.CASLFORMULA
makeTypeHyps ts terms sig =
CASL_AS.conjunct $ map (\ (t, term) -> makeTypeHyp t term sig) $ zip ts terms
-- term translation
termTransl :: Sign -> TERM -> CASL_AS.CASLTERM
termTransl sig (Identifier x) = if not (isConstant x sig)
then CASL_AS.Qual_var x sort nr
else makeApplication x [] sig
termTransl sig t = makeApplication f (map (termTransl sig) as) sig
where (f, as) = termFlatForm t
-- signature translation
sigTransl :: Sign -> (CASL_Sign.CASLSign, [Named CASL_AS.CASLFORMULA])
sigTransl sig = (sigMap sig, generateAxioms sig)
-- theory translation
theoryTransl :: (Sign, [Named FORMULA]) ->
(CASL_Sign.CASLSign, [Named CASL_AS.CASLFORMULA])
theoryTransl (sig, fs) = (sigCASL, axCASL ++ fsCASL)
where (sigCASL, axCASL) = sigTransl sig
fsCASL = map (namedSenTransl sig) fs
-- morphism translation
morphTransl :: Morphism -> CASL_Morphism.CASLMor
morphTransl (Morphism sig1 sig2 sym_map) =
foldl (addSymbolTransl sig1) init_morph $ Map.toList sym_map
where init_morph = CASL_Morphism.Morphism
{ CASL_Morphism.msource = fst $ sigTransl sig1
, CASL_Morphism.mtarget = fst $ sigTransl sig2
, CASL_Morphism.extended_map = ()
}
addSymbolTransl :: Sign -> CASL_Morphism.CASLMor -> (NAME, NAME) ->
addSymbolTransl sig m (f, g) = case kind of
FuncKind -> let
f1 = (mkId [f], CASL_Sign.OpType CASL_AS.Partial (folType arity) sort)
g1 = (mkId [g], CASL_AS.Total)
in m {CASL_Morphism.op_map = Map.insert f1 g1
$ CASL_Morphism.op_map m}
PredKind -> let
f1 = (mkId [f], CASL_Sign.PredType (folType arity))
g1 = mkId [g]
in m {CASL_Morphism.pred_map = Map.insert f1 g1
SortKind -> let
f1 = (mkId [f], CASL_Sign.PredType (folType (arity + 1)))
g1 = mkId [g]
in m {CASL_Morphism.pred_map = Map.insert f1 g1
where Just kind = getSymbolKind f sig
Just arity = getSymbolArity f sig
makeTypesAndVars :: [DECL] -> ([TYPE], [NAME], [CASL_AS.CASLTERM])
makeTypesAndVars ds = let varNames = getVarsFromDecls ds in
( concatMap (\ (ns, t1) -> replicate (length ns) t1) ds
, varNames, map makeVar varNames)
-- sentence translation
senTransl :: Sign -> FORMULA -> CASL_AS.CASLFORMULA
senTransl sig frm = case frm of
T -> CASL_AS.trueForm
F -> CASL_AS.falseForm
Pred t -> makePredication p (map (termTransl sig) as) sig
where (p, as) = termFlatForm t
Equality t1 t2 -> CASL_AS.mkStEq (termTransl sig t1) (termTransl sig t2)
Negation f -> CASL_AS.mkNeg (senTransl sig f)
Conjunction fs -> CASL_AS.conjunct (map (senTransl sig) fs)
Disjunction fs -> CASL_AS.disjunct (map (senTransl sig) fs)
Implication f g -> CASL_AS.mkImpl (senTransl sig f) (senTransl sig g)
Equivalence f g -> CASL_AS.mkEqv (senTransl sig f) (senTransl sig g)
Forall ds f -> let (types, varNames, vars) = makeTypesAndVars ds in
makeForall varNames
(CASL_AS.mkImpl (makeTypeHyps types vars sig) (senTransl sig f))
Exists ds f -> let (types, varNames, vars) = makeTypesAndVars ds in
makeExists varNames
(CASL_AS.conjunct [makeTypeHyps types vars sig, senTransl sig f])
-- named sentence translation
namedSenTransl :: Sign -> Named FORMULA -> Named CASL_AS.CASLFORMULA
namedSenTransl sig nf = nf {sentence = senTransl sig $ sentence nf}
-- symbol translation
symbolTransl :: Sign -> Symbol -> Set.Set CASL_Sign.Symbol
symbolTransl sig sym =
Set.singleton $ CASL_Sign.Symbol (mkId [n])
$ case kind of
PredKind -> CASL_Sign.PredAsItemType
$ CASL_Sign.PredType (folType arity)
FuncKind -> CASL_Sign.OpAsItemType
$ CASL_Sign.mkTotOpType (folType arity) sort
SortKind -> CASL_Sign.PredAsItemType
$ CASL_Sign.PredType (folType (arity + 1))
where n = name sym
Just kind = getSymbolKind n sig
Just arity = getSymbolArity n sig