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

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens Elkner{- |

c7e03d0708369f944b6f235057b39142a21599f2Mihai CodescuModule : ./Comorphisms/CASL2TopSort.hs

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

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt

c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu

c7e03d0708369f944b6f235057b39142a21599f2Mihai CodescuMaintainer : Christian.Maeder@dfki.de

c7e03d0708369f944b6f235057b39142a21599f2Mihai CodescuStability : provisional

c7e03d0708369f944b6f235057b39142a21599f2Mihai CodescuPortability : portable

c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu

90d7cac36f60438bd35124e3389b5bce6d114b46Christian MaederCoding out subsorting into unary predicates.

c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu New concept for proving Ontologies.

c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu

c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescugeneratedness via non-injective datatype constructors

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

c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu

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

c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescufor a second non-zero argument but partial otherwise.

d87ee0dd97c1e61947cf8522346c3126debcd8c1Christian Maeder

c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescupartial functions remain partial unless they fall to together

c208973c890b8f993297720fd0247bc7481d4304Christian Maederwith an overloaded total function

d90c545f128262b3ed863e447bc068ab2b9b2ff6Christian Maeder-}

55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder

d90c545f128262b3ed863e447bc068ab2b9b2ff6Christian Maedermodule Comorphisms.CASL2TopSort (CASL2TopSort (..)) where

d90c545f128262b3ed863e447bc068ab2b9b2ff6Christian Maeder

d90c545f128262b3ed863e447bc068ab2b9b2ff6Christian Maederimport Data.Ord

d90c545f128262b3ed863e447bc068ab2b9b2ff6Christian Maederimport Data.Maybe

d90c545f128262b3ed863e447bc068ab2b9b2ff6Christian Maederimport Data.List

d90c545f128262b3ed863e447bc068ab2b9b2ff6Christian Maeder

d90c545f128262b3ed863e447bc068ab2b9b2ff6Christian Maederimport Logic.Logic

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maederimport Logic.Comorphism

c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu

d90c545f128262b3ed863e447bc068ab2b9b2ff6Christian Maederimport Common.AS_Annotation

47e0312a5350da31881e35fe148233f9e252630fMihai Codescuimport Common.Id

fb891ddc67e73a126dfca1664396ec75068fd8cbMihai Codescuimport Common.ProofTree

2d00b580613fcdc777040a3f855e5cdbdac5d8dfChristian Maederimport Common.Result

d90c545f128262b3ed863e447bc068ab2b9b2ff6Christian Maederimport qualified Common.Lib.Rel as Rel

d90c545f128262b3ed863e447bc068ab2b9b2ff6Christian Maederimport qualified Common.Lib.MapSet as MapSet

96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescu

d90c545f128262b3ed863e447bc068ab2b9b2ff6Christian Maeder-- CASL

c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescuimport CASL.Logic_CASL

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maederimport CASL.AS_Basic_CASL

36f69d35e01d2d6b6bdc165b49661f2a80af8687Mihai Codescuimport CASL.Fold

4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maederimport CASL.Sign

4f3a84cb1b7e55ce38df8f4ac71d06b574b23cb1mscodescuimport CASL.StaticAna (sortsOfArgs)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport CASL.Morphism

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport CASL.Sublogic as SL

28f6b9a4625b910f79be69a4dd819bbbd6e3f7b9Till Mossakowski

4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maederimport qualified Data.Map as Map

36f69d35e01d2d6b6bdc165b49661f2a80af8687Mihai Codescuimport qualified Data.Set as Set

4f3a84cb1b7e55ce38df8f4ac71d06b574b23cb1mscodescu

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- | The identity of the comorphism

4f3a84cb1b7e55ce38df8f4ac71d06b574b23cb1mscodescudata CASL2TopSort = CASL2TopSort deriving Show

fb891ddc67e73a126dfca1664396ec75068fd8cbMihai Codescu

4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maederinstance Language CASL2TopSort where

fb891ddc67e73a126dfca1664396ec75068fd8cbMihai Codescu language_name CASL2TopSort = "CASL2PCFOLTopSort"

33bb9640c37582ebb80c4281e5467728944145aaMihai Codescu

47e0312a5350da31881e35fe148233f9e252630fMihai Codescuinstance Comorphism CASL2TopSort

4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder CASL CASL_Sublogics

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS

d11391a2447a2005329a95b5d770f24e62bf5b63Christian Maeder CASLSign

fb891ddc67e73a126dfca1664396ec75068fd8cbMihai Codescu CASLMor

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Symbol RawSymbol ProofTree

d87ee0dd97c1e61947cf8522346c3126debcd8c1Christian Maeder CASL CASL_Sublogics

d87ee0dd97c1e61947cf8522346c3126debcd8c1Christian Maeder CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS

d87ee0dd97c1e61947cf8522346c3126debcd8c1Christian Maeder CASLSign

4f3a84cb1b7e55ce38df8f4ac71d06b574b23cb1mscodescu CASLMor

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Symbol RawSymbol ProofTree where

28f6b9a4625b910f79be69a4dd819bbbd6e3f7b9Till Mossakowski sourceLogic CASL2TopSort = CASL

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder sourceSublogic CASL2TopSort = SL.caslTop

90d7cac36f60438bd35124e3389b5bce6d114b46Christian Maeder { sub_features = LocFilSub

d90c545f128262b3ed863e447bc068ab2b9b2ff6Christian Maeder , cons_features = emptyMapConsFeature }

d90c545f128262b3ed863e447bc068ab2b9b2ff6Christian Maeder targetLogic CASL2TopSort = CASL

d90c545f128262b3ed863e447bc068ab2b9b2ff6Christian Maeder mapSublogic CASL2TopSort sub =

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder if sub `isSubElem` sourceSublogic CASL2TopSort

d90c545f128262b3ed863e447bc068ab2b9b2ff6Christian Maeder then Just $

d90c545f128262b3ed863e447bc068ab2b9b2ff6Christian Maeder sub { sub_features = NoSub -- subsorting is coded out

d90c545f128262b3ed863e447bc068ab2b9b2ff6Christian Maeder , cons_features = NoSortGen -- special Sort_gen_ax is coded out

d90c545f128262b3ed863e447bc068ab2b9b2ff6Christian Maeder , which_logic = max Horn (which_logic sub)

d90c545f128262b3ed863e447bc068ab2b9b2ff6Christian Maeder , has_eq = True {- was in the original targetLogic

d90c545f128262b3ed863e447bc068ab2b9b2ff6Christian Maeder may be avoided through predications of sort-preds

d90c545f128262b3ed863e447bc068ab2b9b2ff6Christian Maeder with the result terms of functions instead of formulas like:

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

36f69d35e01d2d6b6bdc165b49661f2a80af8687Mihai Codescu better: . a(bot) -}

36f69d35e01d2d6b6bdc165b49661f2a80af8687Mihai Codescu , has_pred = True

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder , has_part = True }

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder {- subsorting is coded out and

c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu special Sort_gen_ax are coded out -}

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder else Nothing

d90c545f128262b3ed863e447bc068ab2b9b2ff6Christian Maeder

d90c545f128262b3ed863e447bc068ab2b9b2ff6Christian Maeder map_theory CASL2TopSort = mkTheoryMapping transSig transSen

c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu map_morphism CASL2TopSort mor = do

d90c545f128262b3ed863e447bc068ab2b9b2ff6Christian Maeder let trSig = fmap fst . transSig

d90c545f128262b3ed863e447bc068ab2b9b2ff6Christian Maeder sigSour <- trSig $ msource mor

d90c545f128262b3ed863e447bc068ab2b9b2ff6Christian Maeder sigTarg <- trSig $ mtarget mor

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder return mor

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder { msource = sigSour

c1d06b3018b34ede2b3fb6c7fe2ad28cd5ce5b68Christian Maeder , mtarget = sigTarg }

d90c545f128262b3ed863e447bc068ab2b9b2ff6Christian Maeder map_sentence CASL2TopSort = transSen

36f69d35e01d2d6b6bdc165b49661f2a80af8687Mihai Codescu map_symbol CASL2TopSort _ = Set.singleton . id

96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescu has_model_expansion CASL2TopSort = True

96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescu

d90c545f128262b3ed863e447bc068ab2b9b2ff6Christian Maederdata PredInfo = PredInfo { topSortPI :: SORT

d90c545f128262b3ed863e447bc068ab2b9b2ff6Christian Maeder , directSuperSortsPI :: Set.Set SORT

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder , predicatePI :: PRED_NAME

12368e292c1abf7eaf975f20ee30ef7820ac5dd5Christian Maeder } deriving Show

d90c545f128262b3ed863e447bc068ab2b9b2ff6Christian Maeder

d90c545f128262b3ed863e447bc068ab2b9b2ff6Christian Maedertype SubSortMap = Map.Map SORT PredInfo

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergenerateSubSortMap :: Rel.Rel SORT -> PredMap -> SubSortMap

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergenerateSubSortMap sortRels pMap =

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let disAmbMap = Map.map disAmbPred

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder disAmbPred v = let pn = predicatePI v in

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder case dropWhile (`Set.member` MapSet.keysSet pMap)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder $ pn : map (\x -> appendString (predicatePI v) $ show x)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder [1::Int ..] of

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder n : _ -> v { predicatePI = n }

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder [] -> error "generateSubSortMap"

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder mR = (Rel.flatSet .

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Rel.partSet (\ x y -> Rel.member x y sortRels &&

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder 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]