7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maeder{- |

7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederModule : $Header$

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian MaederCopyright : (c) Klaus L�ttich, Uni Bremen 2002-2004

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder

b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiMaintainer : luettich@tzi.de

7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederStability : provisional

2ac1742771a267119f1d839054b5e45d0a468085Christian MaederPortability : portable

7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maeder

35597678f1c9da703de8d0b6b66ea63247ebe884Christian MaederCoding out subsorting into unary predicates.

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder New concept for proving Ontologies.

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder-}

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maedermodule Comorphisms.CASL2TopSort (CASL2TopSort(..)) where

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport Control.Exception (assert)

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport Data.Maybe

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maederimport Data.List

ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder

ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport Logic.Logic

4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maederimport Logic.Comorphism

8197d0be8b81692f311ad5ca34e125e2cf9eecb8Christian Maeder

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport Common.Id

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maederimport Common.Result

d42a01c4eb6892fe23ca9eff107bb29f4a229480Christian Maederimport qualified Data.Map as Map

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maederimport qualified Data.Set as Set

c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maederimport qualified Common.Lib.Rel as Rel

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maederimport Common.AS_Annotation

c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder-- CASL

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport CASL.Logic_CASL

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport CASL.AS_Basic_CASL

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maederimport CASL.Utils

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maederimport CASL.Sign

2ac1742771a267119f1d839054b5e45d0a468085Christian Maederimport CASL.Morphism

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport CASL.Sublogic as SL

2ac1742771a267119f1d839054b5e45d0a468085Christian Maederimport CASL.Inject (injName)

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder-- | The identity of the comorphism

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maederdata CASL2TopSort = CASL2TopSort deriving (Show)

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederinstance Language CASL2TopSort -- default definition is okay

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maederinstance Comorphism CASL2TopSort

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder CASL CASL_Sublogics

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder CASLSign

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder CASLMor

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder Symbol RawSymbol ()

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder CASL CASL_Sublogics

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder CASLSign

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder CASLMor

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Symbol RawSymbol () where

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder sourceLogic CASL2TopSort = CASL

ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder sourceSublogic CASL2TopSort = SL.top

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder { sub_features = LocFilSub,

ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder cons_features = SortGen { emptyMapping = True,

ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder onlyInjConstrs = True}

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder }

ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder targetLogic CASL2TopSort = CASL

d48085f765fca838c1d972d2123601997174583dChristian Maeder mapSublogic CASL2TopSort sub =

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder if sub `isSubElem` sourceSublogic CASL2TopSort

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder then Just $

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

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

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder , which_logic = max Horn (which_logic sub)

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder , has_eq = True -- was in the original targetLogic

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder -- may be avoided through predications of sort-preds

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder -- with the result terms of functions instead of formulas like:

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

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder -- better: . a(bot)

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder , has_pred = True}

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder -- subsorting is coded out and

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder -- special Sort_gen_ax are coded out

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder else Nothing

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder map_theory CASL2TopSort = mkTheoryMapping transSig transSen

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder map_morphism CASL2TopSort mor =

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder let rsigSour = trSig $ msource mor

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder rsigTarg = trSig $ mtarget mor

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder in case rsigSour of

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Result diags1 mrs ->

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder case rsigTarg of

5ba383b1607c20c57e14324e72cee2c789436d5fChristian Maeder Result diags2 mrt

ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder | isJust mrs && isJust mrt ->

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder Result (diags1++diags2) (Just

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder (mor { msource = fromJust mrs

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder , mtarget = fromJust mrt }))

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder | otherwise ->

7c35990c03276d1e675ea6f4ba38f47081620d77Christian Maeder (Result (diags1++diags2) Nothing)

7c35990c03276d1e675ea6f4ba38f47081620d77Christian Maeder where trSig sig = case transSig sig of

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder Result dias mr ->

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder Result dias (maybe Nothing

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder (Just . fst)

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder mr)

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder map_sentence CASL2TopSort = transSen

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder map_symbol CASL2TopSort = Set.singleton . id

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder

840b2a6f37ec58f3281da16fafbc4121462c856aChristian Maederdata PredInfo = PredInfo { topSort_PI :: SORT

5ba383b1607c20c57e14324e72cee2c789436d5fChristian Maeder , directSuperSorts_PI :: Set.Set SORT

5ba383b1607c20c57e14324e72cee2c789436d5fChristian Maeder , predicate_PI :: PRED_NAME

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder } deriving (Show, Ord, Eq)

5ba383b1607c20c57e14324e72cee2c789436d5fChristian Maeder

5ba383b1607c20c57e14324e72cee2c789436d5fChristian Maedertype SubSortMap = Map.Map SORT PredInfo

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedergenerateSubSortMap :: Rel.Rel SORT

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder -> Map.Map Id (Set.Set PredType)

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder -> Result SubSortMap

2ac1742771a267119f1d839054b5e45d0a468085Christian MaedergenerateSubSortMap sortRels pMap =

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder let disAmbMap m = Map.map disAmbPred m

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder disAmbPred v = if (predicate_PI v) `Map.member` pMap

55ea7f4cb33abac6a8d539741e457cf686d1f26cChristian Maeder then disAmbPred' (1::Int) v'

2118d66b6aa3c90458925019c9b2fb986e2b2aabChristian Maeder else v

2118d66b6aa3c90458925019c9b2fb986e2b2aabChristian Maeder where v' = add "_s" v

2118d66b6aa3c90458925019c9b2fb986e2b2aabChristian Maeder disAmbPred' x v1 =

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder if (predicate_PI v1) `Map.member` pMap

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder then disAmbPred' (x+1) (add (show x) v')

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder else v1

d48085f765fca838c1d972d2123601997174583dChristian Maeder add s v1 = v1 {predicate_PI =

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder case predicate_PI v1 of

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder Id ts is ps ->

d48085f765fca838c1d972d2123601997174583dChristian Maeder assert (not (null ts))

d48085f765fca838c1d972d2123601997174583dChristian Maeder (Id (init ts ++

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder [(last ts) {tokStr =

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder tokStr (last ts)++s}

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder ]) is ps)

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder }

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder mR = (Rel.flatSet .

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

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder Rel.member y x sortRels))

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder (Rel.mostRight sortRels)

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder toPredInfo k e =

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder let ts = case filter (\pts -> Rel.member k pts sortRels)

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder $ Set.toList mR of

5ba383b1607c20c57e14324e72cee2c789436d5fChristian Maeder [x] -> x

5ba383b1607c20c57e14324e72cee2c789436d5fChristian Maeder _ -> error "CASL2TopSort.generateSubSortMap.toPredInfo"

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder in PredInfo { topSort_PI = ts

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder , directSuperSorts_PI = Set.difference e mR

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder , predicate_PI = k }

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

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder (Map.mapWithKey toPredInfo

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder (Rel.toMap (Rel.intransKernel sortRels)))

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder in return (disAmbMap initMap)

d93bbbec133697cc79d59f9d7cc8e97458976c15Christian Maeder

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder-- | Finds Top-sort(s) and transforms for each top-sort all subsorts

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder-- into unary predicates. All predicates typed with subsorts are now

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder-- typed with the top-sort and axioms reflecting the typing are

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder-- generated. The operations are treated analogous. Axioms are

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder-- generated that each generated unary predicate must hold on at least

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder-- one element of the top-sort.

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder

35597678f1c9da703de8d0b6b66ea63247ebe884Christian MaedertransSig :: Sign () e -> Result (Sign () e, [Named (FORMULA ())])

d93bbbec133697cc79d59f9d7cc8e97458976c15Christian MaedertransSig sig

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder | Rel.null (sortRel sig) =

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder Result [Diag Hint (

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder "CASL2TopSort.transSig: Signature is unchanged (no subsorting present)"

8dcc70ff9afdfe4aff258676718677a4d7076fd0Christian Maeder ) nullRange] (Just (sig,[]))

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder | otherwise =

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder case generateSubSortMap (sortRel sig) (predMap sig) of

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder Result dias m_subSortMap ->

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder maybe (Result dias Nothing)

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder (\ subSortMap -> -- trace (show subSortMap) $

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder let (dias2,newPredMap) =

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder Map.mapAccum (\ds (un,ds1) -> (ds++ds1,un)) [] $

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder Map.unionWithKey repError

d48085f765fca838c1d972d2123601997174583dChristian Maeder (transPredMap subSortMap (predMap sig))

d48085f765fca838c1d972d2123601997174583dChristian Maeder (newPreds subSortMap)

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder (Result dias3 maxioms) =

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder generateAxioms subSortMap (predMap sig) (opMap sig)

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder dias' = dias ++ dias2 ++ dias3

d93bbbec133697cc79d59f9d7cc8e97458976c15Christian Maeder in maybe (Result dias' Nothing)

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder (\axs -> Result dias' $ Just $

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder (sig { sortSet =

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder Set.fromList (map topSort_PI

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder (Map.elems subSortMap))

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder `Set.union`

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder (sortSet sig `Set.difference`

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder Map.keysSet subSortMap)

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder , sortRel = Rel.empty

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder , opMap = transOpMap subSortMap (opMap sig)

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder , assocOps= transOpMap subSortMap (assocOps sig)

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder , predMap = newPredMap

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder },axs ++ symmetryAxioms subSortMap (sortRel sig)))

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder maxioms)

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder m_subSortMap

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder where

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder repError k (v1,d1) (v2,d2) =

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder (Set.union v1 v2,

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder (Diag Warning

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder ("CASL2TopSort.transSig: generating "++

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder "overloading: Predicate "++show k++

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder " gets additional type(s): "++show v2) nullRange)

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder :d1++d2 )

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder newPreds mp =

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder foldr (\ pI nm -> Map.insert (predicate_PI pI)

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder (Set.singleton

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder (PredType [topSort_PI pI]),[]) nm)

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder Map.empty (Map.elems mp)

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaedertransPredMap :: SubSortMap -> Map.Map PRED_NAME (Set.Set PredType)

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder -> Map.Map PRED_NAME (Set.Set PredType, [Diagnosis])

2ac1742771a267119f1d839054b5e45d0a468085Christian MaedertransPredMap subSortMap = Map.map (\s -> (Set.map transType s,[]))

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder where transType t = t { predArgs = map (\s -> maybe s topSort_PI

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder (Map.lookup s subSortMap))

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder (predArgs t)}

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaedertransOpMap :: SubSortMap -> Map.Map OP_NAME (Set.Set OpType)

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder -> Map.Map OP_NAME (Set.Set OpType)

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaedertransOpMap subSortMap = Map.map (tidySet . Set.map transType)

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder where tidySet s = Set.fold joinPartial s s

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder where joinPartial t@(OpType {opKind = Partial})

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder | t {opKind = Total} `Set.member` s = Set.delete t

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder | otherwise = id

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder joinPartial _ = id

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder transType t =

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder t { opArgs = map lkp (opArgs t)

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder , opRes = lkp (opRes t)}

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder lkp = (\s -> maybe s topSort_PI (Map.lookup s subSortMap))

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder

5ba383b1607c20c57e14324e72cee2c789436d5fChristian MaederprocOpMapping :: SubSortMap

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder -> OP_NAME -> Set.Set OpType

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder -> Result [Named (FORMULA ())] -> Result [Named (FORMULA ())]

2ac1742771a267119f1d839054b5e45d0a468085Christian MaederprocOpMapping subSortMap opName set r@(Result ds1 mal) =

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder case mkProfMapOp opName subSortMap set of

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder Result ds2 (Just profMap) ->

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder -- trace (show profMap)

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder (maybe r

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder (\al ->

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder Result (ds1++ds2)

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder (Just (al ++ Map.foldWithKey

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder procProfMapOpMapping

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder [] profMap))) mal)

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder Result ds2 Nothing -> Result (ds1++ds2) Nothing

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder where

27912d626bf179b82fcb337077e5cd9653bb71cfChristian Maeder procProfMapOpMapping :: [SORT] -> (FunKind,Set.Set [Maybe PRED_NAME])

27912d626bf179b82fcb337077e5cd9653bb71cfChristian Maeder -> [Named (FORMULA ())] -> [Named (FORMULA ())]

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder procProfMapOpMapping sl (kind,spl) =

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder genArgRest

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder (genSenName "o" opName (length sl))

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder (genOpEquation kind opName)

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder sl spl

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder

5ba383b1607c20c57e14324e72cee2c789436d5fChristian MaedersymmetryAxioms :: SubSortMap -> Rel.Rel SORT -> [Named (FORMULA ())]

5ba383b1607c20c57e14324e72cee2c789436d5fChristian MaedersymmetryAxioms ssMap sortRels =

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder let symSets = Rel.sccOfClosure sortRels

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder mR = Rel.mostRight sortRels

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder symTopSorts symSet = not (Set.null (Set.intersection mR symSet))

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder xVar = mkSimpleId "x"

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder updateLabel ts symS [sen] =

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder reName ( \ s -> show ts ++ s ++ show symS) sen

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder updateLabel _ _ _ = error "CASL2TopSort.symmetryAxioms"

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder toAxioms symSet =

d48085f765fca838c1d972d2123601997174583dChristian Maeder [updateLabel ts symS (inlineAxioms CASL

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder "sort ts pred symS:ts\n\

ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder \forall xVar : ts\n\

7c35990c03276d1e675ea6f4ba38f47081620d77Christian Maeder \. symS(xVar) %(_symmetric_with_)%")

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder | s<-(Set.toList(Set.difference symSet mR)),

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder let ts = lkupTop ssMap s,

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder let symS = fromJust (lkupPRED_NAME ssMap s)]

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder in concatMap toAxioms (filter symTopSorts symSets)

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian MaedergenerateAxioms :: SubSortMap -> Map.Map PRED_NAME (Set.Set PredType)

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder -> Map.Map OP_NAME (Set.Set OpType)

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder -> Result [Named (FORMULA ())]

35597678f1c9da703de8d0b6b66ea63247ebe884Christian MaedergenerateAxioms subSortMap pMap oMap =

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder -- generate argument restrictions for operations

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder case Map.foldWithKey (procOpMapping subSortMap) (return []) oMap of

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Result dias m_opAxs -> maybe (Result dias Nothing)

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder (\axs -> -- trace (show dias) $

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder Result dias

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder (Just (reverse hi_axs ++

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder reverse p_axs ++

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder reverse axs)))

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder m_opAxs

9fb0db7f56cbb44c3df49552c04afc881267b84eChristian Maeder where p_axs =

840b2a6f37ec58f3281da16fafbc4121462c856aChristian Maeder -- generate argument restrictions for predicates

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder Map.foldWithKey (\ pName set al ->

bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder case mkProfMapPred subSortMap set of

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder profMap ->

bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder -- trace (show profMap)

bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder (al ++ Map.foldWithKey

bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder (\sl -> genArgRest

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder (genSenName "p" pName (length sl))

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder (genPredication pName)

bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder sl)

840b2a6f37ec58f3281da16fafbc4121462c856aChristian Maeder [] profMap))

bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder [] pMap

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder hi_axs =

bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder -- generate subclass_of axioms derived from subsorts

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder -- and non-emptyness axioms

9fb0db7f56cbb44c3df49552c04afc881267b84eChristian Maeder Map.fold (\ (PredInfo { topSort_PI = ts

9fb0db7f56cbb44c3df49552c04afc881267b84eChristian Maeder , predicate_PI = subS

9fb0db7f56cbb44c3df49552c04afc881267b84eChristian Maeder , directSuperSorts_PI = set

9fb0db7f56cbb44c3df49552c04afc881267b84eChristian Maeder }) al ->

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder let supPreds =

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder map (\ s ->

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder maybe (error ("CASL2TopSort: genAxioms:"++

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder " impossible happend: "++show s))

predicate_PI (Map.lookup s subSortMap))

(Set.toList set)

x = mkSimpleId "x"

in al ++ zipWith ( \ sen supS ->

reName ( \ s -> show subS ++ s

++ show supS) sen)

(concat [inlineAxioms CASL

"sort ts\n\

\pred subS,supS: ts\n\

\ forall x : ts . subS(x) =>\n\

\ supS(x) %(_subclassOf_)%"|supS<-supPreds]

) supPreds ++

map ( \ sen -> reName (show subS ++) sen)

(concat [inlineAxioms CASL

"sort ts\n\

\pred subS: ts \n\

\. exists x:ts . \n\

\ subS(x) %(_non_empty)%"])

) [] subSortMap

mkProfMapPred :: SubSortMap -> Set.Set PredType

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

mkProfMapPred ssm = Set.fold seperate Map.empty

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

pt2topSorts = map (lkupTop ssm) . predArgs

pt2preds = map (lkupPRED_NAME ssm) . predArgs

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

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

mkProfMapOp opName ssm = Set.fold seperate (return Map.empty)

where seperate ot r@(Result dias mmap) =

maybe r

(\ mp -> Result dias'

(Just

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

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

(pt2topSorts joinedList)

(fKind,

Set.singleton (pt2preds joinedList))

mp)))

mmap

where joinedList = opArgs ot ++ [opRes ot]

fKind = opKind ot

dias' = if fKind == Partial

then dias ++

[Diag Warning

("Please, check if operation \""++

show opName ++

"\" is still partial as intended,\

\ since a joining of types could\

\ have made it total!!")

nullRange]

else dias

pt2topSorts = map (lkupTop ssm)

pt2preds = map (lkupPRED_NAME ssm)

lkupTop :: SubSortMap -> SORT -> SORT

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

lkupPRED_NAME :: SubSortMap -> SORT -> Maybe PRED_NAME

lkupPRED_NAME ssm s =

maybe Nothing (Just . predicate_PI) (Map.lookup s ssm)

genArgRest :: String

-> ([SORT] -> [TERM f] -> 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 sl (map toSortTerm vars))

vars spl

in

maybe fs ( \ quant -> mapNamed (const quant) (makeNamed "" sen_name)

: fs) mquant

-- | generate a predication with qualified pred name

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

genPredication pName sl ts =

Predication (Qual_pred_name pName

(Pred_type sl nullRange) nullRange)

ts

nullRange

genOpEquation :: FunKind -> OP_NAME -> [SORT] -> [TERM f] -> FORMULA f

genOpEquation kind opName sl terms =

Strong_equation sortedFunTerm resTerm nullRange

where sortedFunTerm =

Sorted_term (Application

(Qual_op_name opName

opType nullRange)

argTerms

nullRange)

resSort

nullRange

opType = case kind of

Partial -> Op_type Partial argSorts resSort nullRange

Total -> Op_type Total argSorts resSort nullRange

argTerms = init terms

resTerm = last terms

argSorts = init sl

resSort = last sl

genVars :: [SORT] -> [TERM f]

genVars = zipWith toVarTerm varSymbs

where varSymbs = map mkSimpleId

(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

-> [TERM f] -- ^ Qual_vars

-> (Set.Set [Maybe PRED_NAME])

-> Maybe (FORMULA f)

genQuantification prop vars spl =

-- trace (show vds) $

maybe Nothing (\dis ->

Just (Quantification Universal vds

(Implication prop

dis

True nullRange) nullRange))

(genDisjunction vars spl)

where vds = reverse (foldl toVarDecl [] vars)

-- toVarDecl :: [VAR_DECL] -> TERM f -> [VAR_DECL]

toVarDecl [] (Qual_var n s _) = [Var_decl [n] s nullRange]

toVarDecl xxs@((Var_decl l s1 _):xs) (Qual_var n s _)

| s1 == s = Var_decl (l++[n]) s1 nullRange:xs

| otherwise = Var_decl [n] s nullRange:xxs

toVarDecl _ _ =

error "CASL2TopSort.toVarDecl: can only handle Qual_var"

genDisjunction :: [TERM f] -- ^ Qual_vars

-> (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 (Disjunction disjs nullRange)

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

genConjunction acc pns

| null conjs = acc

| otherwise = (Conjunction (reverse conjs) nullRange):acc

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

-- genPred :: TERM f -> PRED_NAME -> FORMULA f

genPred acc (v@(Qual_var _ s _),mpn) =

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

genPred _ _ =

error "CASL2TopSort.genPred: can only handle Qual_var"

partitionArity :: Int -> Set.Set PredType -> Map.Map Int [PredType]

partitionArity arity set

| arity == 1 = Map.insert arity (Set.toList set) Map.empty

| otherwise = case Set.partition

(\ x -> length (predArgs x) == arity) set of

(tt,ff) -> Map.insert arity (Set.toList tt)

(partitionArity (arity-1) ff)

combineTypes :: SubSortMap -> Map.Map Int [PredType]

-> Map.Map Int [Map.Map SORT (Set.Set SORT)]

combineTypes subSortMap =

Map.mapWithKey (\ arity types ->

foldr (\ t sl -> zipWith ins (predArgs t) sl)

(replicate arity Map.empty) types)

where ins so mp = maybe mp

(\v -> Rel.setInsert (topSort_PI v) so mp)

(Map.lookup so subSortMap)

-- | 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 :: (Show f) => Sign f e -> FORMULA f -> Result (FORMULA f)

transSen sig f

| Rel.null (sortRel sig) =

Result [Diag Hint (

"CASL2TopSort.transSen: Sentence is unchanged (no subsorting present)"

) nullRange] (Just f)

| otherwise =

case (generateSubSortMap (sortRel sig)

(predMap sig)) of

Result d Nothing -> Result d Nothing

Result d (Just ssm) ->

case mapSen ssm f of

Result d2 jf -> Result (d++d2) jf

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

mapSen ssMap f =

case f of

Sort_gen_ax cs _ ->

genEitherAxiom ssMap cs

_ -> return $ mapSen1 ssMap f

mapSen1 :: SubSortMap -> FORMULA f -> FORMULA f

mapSen1 subSortMap f =

case f of

Conjunction fl pl -> Conjunction (map (mapSen1 subSortMap) fl) pl

Disjunction fl pl -> Disjunction (map (mapSen1 subSortMap) fl) pl

Implication f1 f2 b pl ->

Implication (mapSen1 subSortMap f1) (mapSen1 subSortMap f2) b pl

Equivalence f1 f2 pl ->

Equivalence (mapSen1 subSortMap f1) (mapSen1 subSortMap f2) pl

Negation f1 pl -> Negation (mapSen1 subSortMap f1) pl

tr@(True_atom _) -> tr

fa@(False_atom _) -> fa

Quantification q vdl f1 pl ->

Quantification q (map updateVarDecls vdl) (mapSen1 subSortMap f1) pl

Membership t s pl ->

let t' = mapTerm subSortMap t

in maybe (Membership t' s pl)

(\pn -> genPredication pn [lkupTop subSortMap s]

[t'])

(lkupPRED_NAME subSortMap s)

Existl_equation t1 t2 pl ->

Existl_equation (mapTerm subSortMap t1) (mapTerm subSortMap t2) pl

Strong_equation t1 t2 pl ->

Strong_equation (mapTerm subSortMap t1) (mapTerm subSortMap t2) pl

Definedness t pl ->

Definedness (mapTerm subSortMap t) pl

Predication psy tl pl ->

Predication (updatePRED_SYMB psy) (map (mapTerm subSortMap) tl) pl

ExtFORMULA f1 -> ExtFORMULA f1 -- ExtFORMULA stays as it is

_ ->

error "CASL2TopSort.mapSen1"

where updateVarDecls (Var_decl vl s pl) =

Var_decl vl (lkupTop subSortMap 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 (lkupTop subSortMap) sl) pl') pl

mapTerm :: SubSortMap -> TERM f -> TERM f

mapTerm ssMap t =

case t of

Qual_var v s pl -> Qual_var v (lTop s) pl

Application osy tl pl ->

Application (updateOP_SYMB osy) (map (mapTerm ssMap) tl) pl

Sorted_term t1 s pl ->

Sorted_term (mapTerm ssMap t1) (lTop s) pl

-- casts are discarded due to missing subsorting

Cast t1 _ _ -> mapTerm ssMap t1

Conditional t1 f t2 pl ->

Conditional (mapTerm ssMap t1) (mapSen1 ssMap f) (mapTerm ssMap t2) pl

_ ->

error "CASL2TopSort.mapTerm"

where lTop = lkupTop ssMap

updateOP_SYMB (Op_name _) =

error "CASL2TopSort.mapTerm: got untyped application"

updateOP_SYMB (Qual_op_name on ot pl) =

Qual_op_name on (updateOP_TYPE ot) pl

updateOP_TYPE (Op_type fk sl s pl) =

Op_type fk (map lTop sl) (lTop s) pl

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

[] -> Result [Diag Error

"No injective operation found" nullRange]

Nothing

[xs@(x:_)] -> Result [] (Just (genQuant x (genImpl xs)))

xs@((x:_):_) ->

Result [] (Just (genQuant x (Conjunction

(map genImpl xs) nullRange)))

_ -> error "CASL2TopSort.genEitherAxiom.groupedInjOps"

else Result [Diag Error

("CASL2TopSort: Cannot handle \

\datatype constructors; only subsort \

\embeddings are allowed with free and \

\generated types!") nullRange] Nothing

isInjOp ops =

case ops of

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

Qual_op_name on _ _ -> on == injName

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 x1 x2 = compare (resultSort x1) (resultSort x2)

sameTarget x1 x2 = compTarget x1 x2 == EQ

lTop = lkupTop ssMap

varName = mkSimpleId "x"

mkVarTerm qon =

Sorted_term (Qual_var varName s nullRange) s nullRange

where s = lTop (resultSort qon)

mkVarDecl qon =

Var_decl [varName] (lTop (resultSort qon)) nullRange

genQuant qon f = Quantification Universal [mkVarDecl qon] f nullRange

genImpl [] = error "No OP_SYMB found"

genImpl xs@(x:_) =

assert (lTop (resultSort x) == lTop (argSort x))

(if (resultSort x) == lTop (resultSort x)

then genDisj xs

else Implication (genProp x) (genDisj xs) True nullRange)

genProp qon = genPredication (lPredName (resultSort qon))

[lTop (resultSort qon)]

[mkVarTerm qon]

lPredName s = maybe (error ("CASL2TopSort.genEitherAxiom: \

\No PRED_NAME for \""++show s

++"\" found!"))

id

(lkupPRED_NAME ssMap s)

genDisj qons = Disjunction (map genPred qons) nullRange

genPred qon = genPredication (lPredName (argSort qon))

[lTop (resultSort qon)]

[mkVarTerm qon]