{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}

{- |

Module : $Header$

Copyright : (c) Klaus Luettich, Uni Bremen 2002-2004

License : GPLv2 or higher, see LICENSE.txt

Maintainer : Christian.Maeder@dfki.de

Stability : provisional

Portability : portable

Coding out subsorting into unary predicates.

New concept for proving Ontologies.

generatedness via non-injective datatype constructors

(i.e. proper data constructors) is simply ignored

total functions my become partial because i.e. division is total

for a second non-zero argument but partial otherwise.

partial functions remain partial unless they fall to together

with an overloaded total function

-}

module Comorphisms.CASL2TopSort (CASL2TopSort (..)) where

import Data.Ord

import Data.Maybe

import Data.List

import Logic.Logic

import Logic.Comorphism

import Common.AS_Annotation

import Common.Id

import Common.ProofTree

import Common.Result

import qualified Common.Lib.Rel as Rel

import qualified Common.Lib.MapSet as MapSet

-- CASL

import CASL.Logic_CASL

import CASL.AS_Basic_CASL

import CASL.Fold

import CASL.Sign

import CASL.StaticAna (sortsOfArgs)

import CASL.Morphism

import CASL.Sublogic as SL

import qualified Data.Map as Map

import qualified Data.Set as Set

-- | The identity of the comorphism

data CASL2TopSort = CASL2TopSort deriving Show

instance Language CASL2TopSort where

language_name CASL2TopSort = "CASL2PCFOLTopSort"

instance Comorphism CASL2TopSort

CASL CASL_Sublogics

CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS

CASLSign

CASLMor

Symbol RawSymbol ProofTree

CASL CASL_Sublogics

CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS

CASLSign

CASLMor

Symbol RawSymbol ProofTree where

sourceLogic CASL2TopSort = CASL

sourceSublogic CASL2TopSort = SL.caslTop

{ sub_features = LocFilSub

, cons_features = emptyMapConsFeature }

targetLogic CASL2TopSort = CASL

mapSublogic CASL2TopSort sub =

if sub `isSubElem` sourceSublogic CASL2TopSort

then Just $

sub { sub_features = NoSub -- subsorting is coded out

, cons_features = NoSortGen -- special Sort_gen_ax is coded out

, which_logic = max Horn (which_logic sub)

, has_eq = True {- was in the original targetLogic

may be avoided through predications of sort-preds

with the result terms of functions instead of formulas like:

forall x : T . bot = x => a(x)

better: . a(bot) -}

, has_pred = True

, has_part = True }

{- subsorting is coded out and

special Sort_gen_ax are coded out -}

else Nothing

map_theory CASL2TopSort = mkTheoryMapping transSig transSen

map_morphism CASL2TopSort mor = do

let trSig = fmap fst . transSig

sigSour <- trSig $ msource mor

sigTarg <- trSig $ mtarget mor

return mor

{ msource = sigSour

, mtarget = sigTarg }

map_sentence CASL2TopSort = transSen

map_symbol CASL2TopSort _ = Set.singleton . id

has_model_expansion CASL2TopSort = True

data PredInfo = PredInfo { topSortPI :: SORT

, directSuperSortsPI :: Set.Set SORT

, predicatePI :: PRED_NAME

} deriving Show

type SubSortMap = Map.Map SORT PredInfo

generateSubSortMap :: Rel.Rel SORT -> PredMap -> SubSortMap

generateSubSortMap sortRels pMap =

let disAmbMap = Map.map disAmbPred

disAmbPred v = let pn = predicatePI v in

case dropWhile (`Set.member` MapSet.keysSet pMap)

$ pn : map (appendNumber (predicatePI v)) [1 ..] of

n : _ -> v { predicatePI = n }

[] -> error "generateSubSortMap"

mR = (Rel.flatSet .

Rel.partSet (\ x y -> Rel.member x y sortRels &&

Rel.member y x sortRels))

(Rel.mostRight sortRels)

toPredInfo k e =

let ts = case filter (flip (Rel.member k) sortRels)

$ Set.toList mR of

[x] -> x

_ -> error "CASL2TopSort.generateSubSortMap.toPredInfo"

in PredInfo { topSortPI = ts

, directSuperSortsPI = Set.difference e mR

, predicatePI = k }

initMap = Map.filterWithKey (\ k _ -> not $ Set.member k mR)

(Map.mapWithKey toPredInfo

(Rel.toMap (Rel.intransKernel sortRels)))

in disAmbMap initMap

{- | Finds Top-sort(s) and transforms for each top-sort all subsorts

into unary predicates. All predicates typed with subsorts are now

typed with the top-sort and axioms reflecting the typing are

generated. The operations are treated analogous. Axioms are

generated that each generated unary predicate must hold on at least

one element of the top-sort. -}

transSig :: Sign () e -> Result (Sign () e, [Named (FORMULA ())])

transSig sig = return

$ let sortRels = Rel.rmNullSets $ sortRel sig in

if Rel.nullKeys sortRels then (sig, []) else

let subSortMap = generateSubSortMap sortRels (predMap sig)

newOpMap = transOpMap sortRels subSortMap (opMap sig)

newAssOpMap0 = transOpMap sortRels subSortMap (assocOps sig)

axs = generateAxioms subSortMap (predMap sig) newOpMap

newPreds = foldr (\ pI -> MapSet.insert (predicatePI pI)

$ PredType [topSortPI pI])

MapSet.empty . Map.elems

newPredMap = MapSet.union (transPredMap subSortMap

$ predMap sig) $ newPreds subSortMap

in (sig

{ sortRel = Rel.fromKeysSet

$ Set.fromList (map topSortPI $ Map.elems subSortMap)

`Set.union` (sortSet sig `Set.difference` Map.keysSet subSortMap)

, opMap = newOpMap

, assocOps = interOpMapSet newAssOpMap0 newOpMap

, predMap = newPredMap

}, axs ++ symmetryAxioms subSortMap sortRels)

transPredMap :: SubSortMap -> PredMap -> PredMap

transPredMap subSortMap = MapSet.map transType

where transType t = t

{ predArgs = map (lkupTop subSortMap) $ predArgs t }

transOpMap :: Rel.Rel SORT -> SubSortMap -> OpMap -> OpMap

transOpMap sRel subSortMap = rmOrAddPartsMap True . MapSet.map transType

where

transType t =

let args = opArgs t

lkp = lkupTop subSortMap

newArgs = map lkp args

kd = opKind t

in -- make function partial if argument sorts are subsorts

t { opArgs = map lkp $ opArgs t

, opRes = lkp $ opRes t

, opKind = if kd == Total && and (zipWith

(\ a na -> a == na || Rel.member na a sRel)

args newArgs) then kd else Partial }

procOpMapping :: SubSortMap -> OP_NAME -> Set.Set OpType

-> [Named (FORMULA ())] -> [Named (FORMULA ())]

procOpMapping subSortMap opName =

(++) . Map.foldWithKey procProfMapOpMapping [] . mkProfMapOp subSortMap

where

procProfMapOpMapping :: [SORT] -> (OpKind, Set.Set [Maybe PRED_NAME])

-> [Named (FORMULA ())] -> [Named (FORMULA ())]

procProfMapOpMapping sl (kind, spl) = genArgRest

(genSenName "o" opName $ length sl) (genOpEquation kind opName) sl spl

mkSimpleQualPred :: PRED_NAME -> SORT -> PRED_SYMB

mkSimpleQualPred symS ts = mkQualPred symS $ Pred_type [ts] nullRange

symmetryAxioms :: SubSortMap -> Rel.Rel SORT -> [Named (FORMULA ())]

symmetryAxioms ssMap sortRels =

let symSets = Rel.sccOfClosure sortRels

toAxioms = concatMap

(\ s ->

let ts = lkupTop ssMap s

symS = lkupPred ssMap s

psy = mkSimpleQualPred symS ts

vd = mkVarDeclStr "x" ts

vt = toQualVar vd

in if ts == s then [] else

[makeNamed (show ts ++ "_symmetric_with_" ++ show symS)

$ mkForall [vd] $ mkPredication psy [vt]]

) . Set.toList

in concatMap toAxioms symSets

generateAxioms :: SubSortMap -> PredMap -> OpMap -> [Named (FORMULA ())]

generateAxioms subSortMap pMap oMap = hi_axs ++ p_axs ++ axs

where -- generate argument restrictions for operations

axs = Map.foldWithKey (procOpMapping subSortMap) []

$ MapSet.toMap oMap

p_axs =

-- generate argument restrictions for predicates

Map.foldWithKey (\ pName ->

(++) . Map.foldWithKey

(\ sl -> genArgRest

(genSenName "p" pName $ length sl)

(genPredication pName)

sl)

[] . mkProfMapPred subSortMap)

[] $ MapSet.toMap pMap

hi_axs =

{- generate subclass_of axioms derived from subsorts

and non-emptyness axioms -}

concatMap (\ prdInf ->

let ts = topSortPI prdInf

subS = predicatePI prdInf

set = directSuperSortsPI prdInf

supPreds = map (lkupPred subSortMap) $ Set.toList set

x = mkVarDeclStr "x" ts

mkPredf sS = mkPredication (mkSimpleQualPred sS ts)

[toQualVar x]

in makeNamed (show subS ++ "_non_empty")

(Quantification Existential [x] (mkPredf subS)

nullRange)

: map (\ supS ->

makeNamed (show subS ++ "_subclassOf_" ++ show supS)

$ mkForall [x]

$ mkImpl (mkPredf subS) $ mkPredf supS)

supPreds

) $ Map.elems subSortMap

mkProfMapPred :: SubSortMap -> Set.Set PredType

-> Map.Map [SORT] (Set.Set [Maybe PRED_NAME])

mkProfMapPred ssm = Set.fold seperate Map.empty

where seperate pt = MapSet.setInsert (pt2topSorts pt) (pt2preds pt)

pt2topSorts = map (lkupTop ssm) . predArgs

pt2preds = map (lkupPredM ssm) . predArgs

mkProfMapOp :: SubSortMap -> Set.Set OpType

-> Map.Map [SORT] (OpKind, Set.Set [Maybe PRED_NAME])

mkProfMapOp ssm = Set.fold seperate Map.empty

where seperate ot =

Map.insertWith (\ (k1, s1) (k2, s2) ->

(min k1 k2, Set.union s1 s2))

(pt2topSorts joinedList)

(fKind, Set.singleton $ pt2preds joinedList)

where joinedList = opSorts ot

fKind = opKind ot

pt2topSorts = map (lkupTop ssm)

pt2preds = map (lkupPredM ssm)

lkupTop :: SubSortMap -> SORT -> SORT

lkupTop ssm s = maybe s topSortPI (Map.lookup s ssm)

lkupPredM :: SubSortMap -> SORT -> Maybe PRED_NAME

lkupPredM ssm s = fmap predicatePI $ Map.lookup s ssm

lkupPred :: SubSortMap -> SORT -> PRED_NAME

lkupPred ssm = fromMaybe (error "CASL2TopSort.lkupPred") . lkupPredM ssm

genArgRest :: String -> ([VAR_DECL] -> FORMULA f)

{- ^ generates from a list of variables

either the predication or function equation -}

-> [SORT] -> Set.Set [Maybe PRED_NAME]

-> [Named (FORMULA f)] -> [Named (FORMULA f)]

genArgRest sen_name genProp sl spl fs =

let vars = genVars sl

mquant = genQuantification (genProp vars) vars spl

in maybe fs (\ quant -> makeNamed sen_name quant : fs) mquant

genPredication :: PRED_NAME -> [VAR_DECL] -> FORMULA f

genPredication pName vars =

genPredAppl pName (map (\ (Var_decl _ s _) -> s) vars) $ map toQualVar vars

-- | generate a predication with qualified pred name

genPredAppl :: PRED_NAME -> [SORT] -> [TERM f] -> FORMULA f

genPredAppl pName sl terms = Predication (Qual_pred_name pName

(Pred_type sl nullRange) nullRange) terms nullRange

genOpEquation :: OpKind -> OP_NAME -> [VAR_DECL] -> FORMULA f

genOpEquation kind opName vars = case vars of

resV@(Var_decl _ s _) : argVs -> mkStEq opTerm resTerm

where opTerm = mkAppl (mkQualOp opName opType) argTerms

opType = Op_type kind argSorts s nullRange

argSorts = sortsOfArgs argVs

resTerm = toQualVar resV

argTerms = map toQualVar argVs

_ -> error "CASL2TopSort.genOpEquation: no result variable"

genVars :: [SORT] -> [VAR_DECL]

genVars = zipWith mkVarDeclStr varSymbs

where varSymbs =

map (: []) "xyzuwv" ++ map (\ i -> 'v' : show i) [(1 :: Int) ..]

genSenName :: Show a => String -> a -> Int -> String

genSenName suff symbName arity =

"arg_rest_" ++ show symbName ++ '_' : suff ++ '_' : show arity

genQuantification :: FORMULA f {- ^ either the predication or

function equation -}

-> [VAR_DECL] -- ^ Qual_vars

-> Set.Set [Maybe PRED_NAME]

-> Maybe (FORMULA f)

genQuantification prop vars spl = do

dis <- genDisjunction vars spl

return $ mkForall vars $ mkImpl prop dis

genDisjunction :: [VAR_DECL] -> Set.Set [Maybe PRED_NAME] -> Maybe (FORMULA f)

genDisjunction vars spn

| Set.size spn == 1 =

case disjs of

[] -> Nothing

[x] -> Just x

_ -> error "CASL2TopSort.genDisjunction: this cannot happen"

| null disjs = Nothing

| otherwise = Just (disjunct disjs)

where disjs = foldl genConjunction [] (Set.toList spn)

genConjunction acc pns

| null conjs = acc

| otherwise = conjunct (reverse conjs) : acc

where conjs = foldl genPred [] (zip vars pns)

genPred acc (v, mpn) = maybe acc

(\ pn -> genPredication pn [v] : acc) mpn

{- | Each membership test of a subsort is transformed to a predication

of the corresponding unary predicate. Variables quantified over a

subsort yield a premise to the quantified formula that the

corresponding predicate holds. All typings are adjusted according

to the subsortmap and sort generation constraints are translated to

disjointness axioms. -}

transSen :: Sign f e -> FORMULA f -> Result (FORMULA f)

transSen sig f = let sortRels = Rel.rmNullSets $ sortRel sig in

if Rel.noPairs sortRels then return f else do

let ssm = generateSubSortMap sortRels (predMap sig)

newOpMap = transOpMap sortRels ssm (opMap sig)

mapSen ssm newOpMap f

mapSen :: SubSortMap -> OpMap -> FORMULA f -> Result (FORMULA f)

mapSen ssMap opM f =

case f of

Sort_gen_ax cs _ ->

genEitherAxiom ssMap cs

_ -> return $ foldFormula (mapRec ssMap opM) f

mapRec :: SubSortMap -> OpMap -> Record f (FORMULA f) (TERM f)

mapRec ssM opM = (mapRecord id)

{ foldQuantification = \ _ q vdl ->

Quantification q (map updateVarDecls vdl) . relativize q vdl

, foldMembership = \ _ t s pl -> maybe (Membership t s pl)

(\ pn -> genPredAppl pn [lTop s] [t]) $ lPred s

, foldPredication = \ _ -> Predication . updatePRED_SYMB

, foldQual_var = \ _ v -> Qual_var v . lTop

, foldApplication = \ _ -> Application . updateOP_SYMB

, foldSorted_term = \ _ t1 -> Sorted_term t1 . lTop

-- casts are discarded due to missing subsorting

, foldCast = \ _ t1 _ _ -> t1 }

where lTop = lkupTop ssM

lPred = lkupPredM ssM

updateOP_SYMB (Op_name _) =

error "CASL2TopSort.mapTerm: got untyped application"

updateOP_SYMB (Qual_op_name on ot pl) =

Qual_op_name on (updateOP_TYPE on ot) pl

updateOP_TYPE on (Op_type _ sl s pl) =

let args = map lTop sl

res = lTop s

t1 = toOpType $ Op_type Total args res pl

ts = MapSet.lookup on opM

nK = if Set.member t1 ts then Total else Partial

in Op_type nK args res pl

updateVarDecls (Var_decl vl s pl) =

Var_decl vl (lTop s) pl

updatePRED_SYMB (Pred_name _) =

error "CASL2TopSort.mapSen: got untyped predication"

updatePRED_SYMB (Qual_pred_name pn (Pred_type sl pl') pl) =

Qual_pred_name pn

(Pred_type (map lTop sl) pl') pl

-- relativize quantifiers using predicates coding sorts

relativize q vdl f1 = let vPs = mkVarPreds vdl in

if null vdl then f1

else case q of -- universal? then use implication

Universal -> mkImpl vPs f1

-- existential or unique-existential? then use conjuction

_ -> conjunct [vPs, f1]

mkVarPreds = conjunct . map mkVarPred

mkVarPred (Var_decl vs s _) = conjunct $ foldr (mkVarPred1 s) [] vs

mkVarPred1 s v = case lPred s of

-- no subsort? then no relativization

Nothing -> id

Just p1 -> (genPredication p1 [mkVarDecl v $ lTop s] :)

genEitherAxiom :: SubSortMap -> [Constraint] -> Result (FORMULA f)

genEitherAxiom ssMap =

genConjunction . (\ (_, osl, _) -> osl) . recover_Sort_gen_ax

where genConjunction osl =

let (injOps, constrs) = partition isInjOp osl

groupedInjOps = groupBy sameTarget $ sortBy compTarget injOps

in if null constrs

then case groupedInjOps of

[] -> fatal_error "No injective operation found" nullRange

[xs@(x : _)] -> return $ genQuant x $ genImpl xs

((x : _) : _) -> return $ genQuant x

$ conjunct $ map genImpl groupedInjOps

_ -> error "CASL2TopSort.genEitherAxiom.groupedInjOps"

else Result [mkDiag Hint

"ignoring generating constructors"

constrs]

$ Just trueForm

isInjOp ops =

case ops of

Op_name _ -> error "CASL2TopSort.genEitherAxiom.isInjObj"

Qual_op_name on _ _ -> isInjName on

resultSort (Qual_op_name _ (Op_type _ _ t _) _) = t

resultSort _ = error "CASL2TopSort.genEitherAxiom.resultSort"

argSort (Qual_op_name _ (Op_type _ [x] _ _) _) = x

argSort _ = error "CASL2TopSort.genEitherAxiom.argSort"

compTarget = comparing resultSort

sameTarget x1 x2 = compTarget x1 x2 == EQ

lTop = lkupTop ssMap

mkXVarDecl = mkVarDeclStr "x" . lTop . resultSort

genQuant qon = mkForall [mkXVarDecl qon]

genImpl xs = case xs of

x : _ -> let

rSrt = resultSort x

ltSrt = lTop rSrt

disjs = genDisj xs

in if ltSrt == lTop (argSort x) then

if rSrt == ltSrt then disjs else mkImpl (genProp x) disjs

else error "CASL2TopSort.genEitherAxiom.genImpl"

_ -> error "CASL2TopSort.genEitherAxiom.genImpl No OP_SYMB found"

genProp qon =

genPredication (lPredName $ resultSort qon) [mkXVarDecl qon]

lPredName = lkupPred ssMap

genDisj qons = disjunct (map genPred qons)

genPred qon =

genPredication (lPredName $ argSort qon) [mkXVarDecl qon]