Symbols and signature morphisms for the CASL logic
type SymbolMap =
Map.Map Symbol Symbol
data RawSymbol = ASymbol Symbol | AKindedSymb SYMB_KIND Id
instance GetRange RawSymbol where
AKindedSymb _ i -> getRange i
type RawSymbolSet =
Set.Set RawSymbol
type RawSymbolMap =
Map.Map RawSymbol RawSymbol
-- always use the partial profile as key!
type Op_map =
Map.Map (Id, OpType) (Id, OpKind)
type Pred_map =
Map.Map (Id, PredType) Id
data Morphism f e m = Morphism
data DefMorExt e = DefMorExt deriving (Show, Eq)
emptyMorExt :: DefMorExt e
instance Pretty (DefMorExt e) where
type CASLMor = Morphism () () ()
isInclusionMorphism :: (m -> Bool) -> Morphism f e m -> Bool
isInclusionMorphism f m = f (extended_map m) &&
Map.null (sort_map m)
&&
Map.null (pred_map m) && isInclOpMap (op_map m)
mapSort :: Sort_map -> SORT -> SORT
mapOpType :: Sort_map -> OpType -> OpType
mapOpType sorts t = if
Map.null sorts then t else
t { opArgs = map (mapSort sorts) $ opArgs t
, opRes = mapSort sorts $ opRes t }
mapOpTypeK :: Sort_map -> OpKind -> OpType -> OpType
mapOpTypeK sorts k = makeTotal k . mapOpType sorts
makeTotal :: OpKind -> OpType -> OpType
makeTotal fk t = case fk of
Total -> t { opKind = Total }
mapOpSym :: Sort_map -> Op_map -> (Id, OpType) -> (Id, OpType)
mapOpSym sMap oMap (i, ot) = let mot = mapOpType sMap ot in
Just (j, k) -> (j, makeTotal k mot)
-- | Check if two OpTypes are equal modulo totality or partiality
compatibleOpTypes :: OpType -> OpType -> Bool
compatibleOpTypes ot1 ot2 = opArgs ot1 == opArgs ot2 && opRes ot1 == opRes ot2
mapPredType :: Sort_map -> PredType -> PredType
mapPredType sorts t = if
Map.null sorts then t else
t { predArgs = map (mapSort sorts) $ predArgs t }
mapPredSym :: Sort_map -> Pred_map -> (Id, PredType) -> (Id, PredType)
mapPredSym sMap oMap (i, pt) =
embedMorphism :: m -> Sign f e -> Sign f e -> Morphism f e m
embedMorphism extEm a b = Morphism
symbTypeToKind :: SymbType -> SYMB_KIND
symbTypeToKind st = case st of
OpAsItemType _ -> Ops_kind
PredAsItemType _ -> Preds_kind
SortAsItemType -> Sorts_kind
OtherTypeKind s -> OtherKinds s
symbolToRaw :: Symbol -> RawSymbol
idToRaw :: Id -> RawSymbol
idToRaw = AKindedSymb Implicit
rawSymName :: RawSymbol -> Id
rawSymName rs = case rs of
ASymbol sym -> symName sym
symOf :: Sign f e -> SymbolSet
sorts =
Set.map idToSortSymbol $ sortSet sigma
concatMap (\ (i, ts) -> map ( \ t -> idToOpSymbol i t) $
Set.toList ts)
concatMap (\ (i, ts) -> map ( \ t -> idToPredSymbol i t)
checkSymbList :: [SYMB_OR_MAP] -> [Diagnosis]
checkSymbList l = case l of
Symb (Symb_id a) : Symb (Qual_id b t _) : r -> mkDiag Warning
("profile '" ++ showDoc t "' does not apply to '"
++ showId a "' but only to") b : checkSymbList r
statSymbMapItems :: [SYMB_MAP_ITEMS] -> Result RawSymbolMap
let st (Symb_map_items kind l _) = do
appendDiags $ checkSymbList l
fmap concat $ mapM (symbOrMapToRaw kind) l
insertRsys m1 (rsy1, rsy2) = case
Map.lookup rsy1 m1 of
Just rsy3 -> if rsy2 == rsy3 then return m1 else
plain_error m1 ("Symbol " ++ showDoc rsy1 " mapped twice to "
++ showDoc rsy2 " and " ++ showDoc rsy3 "") nullRange
symbOrMapToRaw :: SYMB_KIND -> SYMB_OR_MAP -> Result [(RawSymbol, RawSymbol)]
appendDiags $ case (s, t) of
(Symb_id a, Symb_id b) | a == b ->
[mkDiag Hint "unneeded identical mapping of" a]
let mkS = AKindedSymb Sorts_kind
(Qual_id _ t1 _, Qual_id _ t2 _) -> case (t1, t2) of
(O_type (Op_type _ args1 res1 _), O_type (Op_type _ args2 res2 _))
| length args1 == length args2 -> -- ignore partiality
return $ (w, x) : (mkS res1, mkS res2)
: zipWith (\ s1 s2 -> (mkS s1, mkS s2)) args1 args2
(P_type (Pred_type args1 _), P_type (Pred_type args2 _))
| length args1 == length args2 ->
: zipWith (\ s1 s2 -> (mkS s1, mkS s2)) args1 args2
(O_type (Op_type _ [] res1 _), A_type s2) ->
return [(w, x), (mkS res1, mkS s2)]
(A_type s1, O_type (Op_type _ [] res2 _)) ->
return [(w, x), (mkS s1, mkS res2)]
(A_type s1, A_type s2) ->
return [(w, x), (mkS s1, mkS s2)]
_ -> fail $ "profiles '" ++ showDoc t1 "' and '"
++ showDoc t2 "' do not match"
statSymbItems :: [SYMB_ITEMS] -> Result [RawSymbol]
let st (Symb_items kind l _) = do
appendDiags $ checkSymbList $ map Symb l
in fmap concat (mapM st sl)
symbToRaw :: SYMB_KIND -> SYMB -> Result RawSymbol
symbToRaw k si = case si of
Symb_id idt -> return $ AKindedSymb k idt
Qual_id idt t _ -> typedSymbKindToRaw k idt t
typedSymbKindToRaw :: SYMB_KIND -> Id -> TYPE -> Result RawSymbol
typedSymbKindToRaw k idt t = let
err = plain_error (AKindedSymb Implicit idt)
(showDoc idt ":" ++ showDoc t
"does not have kind" ++ showDoc k "") nullRange
aSymb = ASymbol $ case t of
O_type ot -> idToOpSymbol idt $ toOpType ot
P_type pt -> idToPredSymbol idt $ toPredType pt
-- in case of ambiguity, return a constant function type
-- this deviates from the CASL summary !!!
let ot = OpType {opKind = Total, opArgs = [], opRes = s}
appendDiags [mkDiag Warning "qualify name as pred or op" idt]
A_type s -> return $ ASymbol $
let pt = PredType {predArgs = [s]}
symbMapToMorphism :: m -> Sign f e -> Sign f e
-> SymbolMap -> Result (Morphism f e m)
symbMapToMorphism extEm sigma1 sigma2 smap = let
case
Map.lookup Symbol {symName = s, symbType = SortAsItemType} smap
of Just sym -> let t = symName sym in if s == t then m else
mapOp i ots m =
Set.fold (insOp i) m ots
case
Map.lookup Symbol {symName = i, symbType = OpAsItemType ot} smap
of Just sym -> let j = symName sym in case symbType sym of
OpAsItemType oty -> let k = opKind oty in
if j == i && opKind ot == k then m
mapPred i pts m =
Set.fold (insPred i) m pts
case
Map.lookup Symbol {symName = i, symbType = PredAsItemType pt} smap
of Just sym -> let j = symName sym in case symbType sym of
PredAsItemType _ -> if i == j then m else
Map.insert (i, pt) j m
in return (embedMorphism extEm sigma1 sigma2)
morphismToSymbMap :: Morphism f e m -> SymbolMap
morphismToSymbMap = morphismToSymbMapAux False
morphismToSymbMapAux :: Bool -> Morphism f e m -> SymbolMap
morphismToSymbMapAux b mor = let
(\ s -> let t = mapSort sorts s in
if b && s == t then id else
( \ t -> let (j, k) = mapOpSym sorts ops (i, t) in
if b && i == j && opKind k == opKind t then id else
( \ t -> let (j, k) = mapPredSym sorts preds (i, t) in
if b && i == j then id else
Map.insert (idToPredSymbol i t) $ idToPredSymbol j k)
in foldr
Map.union sortSymMap [opSymMap, predSymMap]
matches :: Symbol -> RawSymbol -> Bool
matches x@(Symbol idt k) rs = case rs of
AKindedSymb rk di -> let res = idt == di in case (k, rk) of
(SortAsItemType, Sorts_kind) -> res
(OpAsItemType _, Ops_kind) -> res
(PredAsItemType _, Preds_kind) -> res
idMor :: m -> Sign f e -> Morphism f e m
idMor extEm sigma = embedMorphism extEm sigma sigma
composeM :: (Eq e, Eq f) => (m -> m -> Result m)
-> Morphism f e m -> Morphism f e m -> Result (Morphism f e m)
composeM comp mor1 mor2 = if mtarget mor1 == msource mor2 then do
let sMap1 = sort_map mor1
let j = mapSort sMap2 (mapSort sMap1 i) in
oMap = if
Map.null oMap2 then oMap1 else
let (ni, nt) = mapOpSym sMap2 oMap2 $
mapOpSym sMap1 oMap1 (i, ot)
in assert (mapOpTypeK sMap k ot == nt) $
if i == ni && opKind ot == k then id else
pMap = if
Map.null pMap2 then pMap1 else
let (ni, nt) = mapPredSym sMap2 pMap2 $
mapPredSym sMap1 pMap1 (i, pt)
in assert (mapPredType sMap pt == nt) $
if i == ni then id else
Map.insert (i, pt) ni) m t)
extComp <- comp (extended_map mor1) $ extended_map mor2
let emb = embedMorphism extComp src tar
else fail "target of first and source of second morphism are different"
legalSign :: Sign f e -> Bool
where sorts = sortSet sigma
legalOpType t = legalSort (opRes t)
&& all legalSort (opArgs t)
legalPredType = all legalSort . predArgs
-- | the image of a signature morphism
imageOfMorphism :: Morphism f e m -> Sign f e
{ sortSet = msorts $ sortSet src
, sortRel =
Rel.map ms $ sortRel src
, emptySortSet = msorts $ emptySortSet src
, opMap = inducedOpMap sm om $ opMap src
, assocOps = inducedOpMap sm om $ assocOps src
, predMap = inducedPredMap sm (pred_map mor) $ predMap src }
inducedOpMap :: Sort_map -> Op_map -> OpMap -> OpMap
let (j, nt) = mapOpSym sm fm (i, ot)
inducedPredMap :: Sort_map -> Pred_map ->
Map.Map Id (
Set.Set PredType)
let (j, nt) = mapPredSym sm pm (i, ot)
legalMor :: Morphism f e m -> Bool
&& isSubOpMap (inducedOpMap sm (op_map mor) $ opMap s1) (opMap s2)
&& isSubMapSet (inducedPredMap sm (pred_map mor) $ predMap s1) (predMap s2)
isInclOpMap :: Op_map -> Bool
isInclOpMap = all (\ ((i, _), (j, k)) -> i == j && k == Total) .
Map.toListidOrInclMorphism :: (e -> e -> Bool) -> Morphism f e m -> Morphism f e m
idOrInclMorphism isSubExt m =
in if isSubSig isSubExt tar src then m
else let diffOpMap = diffMapSet (opMap src) $ opMap tar in
map (\ t -> ((i, t), (i, Total)))
sigInclusion :: (Pretty f, Pretty e)
=> m -- ^ computed extended morphism
-> (e -> e -> Bool) -- ^ subsignature test of extensions
-> (e -> e -> e) -- ^ difference of signature extensions
-> Sign f e -> Sign f e -> Result (Morphism f e m)
sigInclusion extEm isSubExt diffExt sigma1 sigma2 =
if isSubSig isSubExt sigma1 sigma2 then
return $ idOrInclMorphism isSubExt $ embedMorphism extEm sigma1 sigma2
("Attempt to construct inclusion between non-subsignatures:\n"
++ showDoc (diffSig diffExt sigma1 sigma2) "") nullRange] Nothing
addSigM :: Monad m => (e -> e -> m e) -> Sign f e -> Sign f e -> m (Sign f e)
e <- f (extendedInfo a) $ extendedInfo b
return $ addSig (const $ const e) a b
morphismUnion :: (m -> m -> m) -- ^ join morphism extensions
-> (e -> e -> e) -- ^ join signature extensions
-> Morphism f e m -> Morphism f e m -> Result (Morphism f e m)
morphismUnion uniteM addSigExt =
morphismUnionM uniteM (\ e -> return . addSigExt e)
morphismUnionM :: (m -> m -> m) -- ^ join morphism extensions
-> (e -> e -> Result e) -- ^ join signature extensions
-> Morphism f e m -> Morphism f e m -> Result (Morphism f e m)
-- consider identity mappings but filter them eventually
morphismUnionM uniteM addSigExt mor1 mor2 =
let smap1 = sort_map mor1
uo1 = foldr delOp (opMap s1) $
Map.keys omap1
uo2 = foldr delOp (opMap s2) $
Map.keys omap2
up1 = foldr delPred (predMap s1) $
Map.keys pmap1
up2 = foldr delPred (predMap s2) $
Map.keys pmap2
(sds, smap) = foldr ( \ (i, j) (ds, m) -> case
Map.lookup i m of
Just k -> if j == k then (ds, m) else
("incompatible mapping of sort " ++ showId i " to "
++ showId j " and " ++ showId k "")
nullRange : ds, m)) ([], smap1)
(ods, omap) = foldr ( \ (isc@(i, ot), jsc@(j, t)) (ds, m) ->
Just (k, p) -> if j == k then if p == t then (ds, m)
("incompatible mapping of op " ++ showId i ":"
++ showDoc ot { opKind = t } " to "
++ showId j " and " ++ showId k "") nullRange : ds, m))
( \ (a, s) -> map ( \ ot -> ((a, mkPartial ot),
(pds, pmap) = foldr ( \ (isc@(i, pt), j) (ds, m) ->
Just k -> if j == k then (ds, m) else
("incompatible mapping of pred " ++ showId i ":"
++ showDoc pt " to " ++ showId j " and "
++ showId k "") nullRange : ds, m)) (ods, pmap1)
s3 <- addSigM addSigExt s1 s2
s4 <- addSigM addSigExt (mtarget mor1) $ mtarget mor2
(embedMorphism (uniteM (extended_map mor1) $ extended_map mor2) s3 s4)
(\ (i, ot) (j, k) -> i /= j || k == Total &&
Set.member ot
isSortInjective :: Morphism f e m -> Bool
let ss = sortSet $ msource m
-- morphism extension m is not considered here
isInjective :: Morphism f e m -> Bool
isInjective m = isSortInjective m && let
in sumSize os == sumSize (inducedOpMap sm (op_map m) os)
&& sumSize ps == sumSize (inducedPredMap sm (pred_map m) ps)
instance Pretty RawSymbol where
pretty rsym = case rsym of
AKindedSymb k i -> pretty k <+> pretty i
printMorphism :: (f -> Doc) -> (e -> Doc) -> (m -> Doc) -> Morphism f e m
printMorphism fF fE fM mor =
prSig s = specBraces (space <> printSign fF fE s)
in if isInclusionMorphism (const True) mor then
if isSubSig (\ _ _ -> True) tar src then
fsep [text "identity morphism over", srcD]
[ text "inclusion morphism of", srcD
[ pretty (morphismToSymbMapAux True mor)
$+$ fM (extended_map mor)
, colon <+> srcD, mapsto <+> prSig tar ]
instance (Pretty e, Pretty f, Pretty m) =>
Pretty (Morphism f e m) where
pretty = printMorphism pretty pretty pretty