7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder{- |

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederModule : $Header$

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederDescription : CASL signatures and local environments for basic analysis

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2002-2006

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederMaintainer : Christian.Maeder@dfki.de

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederStability : provisional

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederPortability : portable

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederCASL signatures also serve as local environments for the basic static analysis

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder-}

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maedermodule CASL.Sign where

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maederimport CASL.AS_Basic_CASL

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maederimport CASL.ToDoc ()

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maederimport qualified Data.Map as Map

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maederimport qualified Data.Set as Set

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maederimport qualified Common.Lib.Rel as Rel

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maederimport qualified Common.Lib.State as State

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maederimport Common.Keywords

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maederimport Common.Id

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maederimport Common.Result

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maederimport Common.AS_Annotation

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maederimport Common.GlobalAnnotations

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maederimport Common.Doc

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maederimport Common.DocUtils

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maederimport Data.List (isPrefixOf)

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maederimport Control.Monad (when, unless)

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder-- constants have empty argument lists

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maederdata OpType = OpType {opKind :: OpKind, opArgs :: [SORT], opRes :: SORT}

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder deriving (Show, Eq, Ord)

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maederdata PredType = PredType {predArgs :: [SORT]} deriving (Show, Eq, Ord)

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maedertype OpMap = Map.Map Id (Set.Set OpType)

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maederdata SymbType = SortAsItemType

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder | OtherTypeKind String

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder | OpAsItemType OpType

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder -- since symbols do not speak about totality, the totality

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder -- information in OpType has to be ignored

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder | PredAsItemType PredType

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder deriving (Show, Eq, Ord)

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maederdata Symbol = Symbol {symName :: Id, symbType :: SymbType}

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder deriving (Show, Eq, Ord)

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maederinstance GetRange Symbol where

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder getRange = getRange . symName

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederidToSortSymbol :: Id -> Symbol

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederidToSortSymbol idt = Symbol idt SortAsItemType

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederidToOpSymbol :: Id -> OpType -> Symbol

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederidToOpSymbol idt = Symbol idt . OpAsItemType

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederidToPredSymbol :: Id -> PredType -> Symbol

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederidToPredSymbol idt = Symbol idt . PredAsItemType

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maederdummy :: Sign f s -> a -> ()

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maederdummy _ _ = ()

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederdummyMin :: b -> c -> Result ()

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederdummyMin _ _ = return ()

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maedertype CASLSign = Sign () ()

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maederdata Sign f e = Sign

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder { sortSet :: Set.Set SORT

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder , emptySortSet :: Set.Set SORT

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder -- a subset of the sort set of possibly empty sorts

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder , sortRel :: Rel.Rel SORT

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder , opMap :: OpMap

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder , assocOps :: OpMap

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder , predMap :: Map.Map Id (Set.Set PredType)

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder , varMap :: Map.Map SIMPLE_ID SORT

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder , sentences :: [Named (FORMULA f)]

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder , declaredSymbols :: Set.Set Symbol

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder , envDiags :: [Diagnosis]

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder , annoMap :: Map.Map Symbol (Set.Set Annotation)

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder , globAnnos :: GlobalAnnos

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder , extendedInfo :: e

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder } deriving Show

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder-- better ignore assoc flags for equality

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maederinstance Eq e => Eq (Sign f e) where

45ad02e03fb913ba373d8fdcfe50244be3df31eaChristian Maeder e1 == e2 =

ee31a8a5f5d786472f2b5dfb271b38e6d401fa35Christian Maeder sortSet e1 == sortSet e2 &&

b7413fd7a18b060775364d271c3e706c07227b13Christian Maeder emptySortSet e1 == emptySortSet e2 &&

b7413fd7a18b060775364d271c3e706c07227b13Christian Maeder sortRel e1 == sortRel e2 &&

b7413fd7a18b060775364d271c3e706c07227b13Christian Maeder opMap e1 == opMap e2 &&

b7413fd7a18b060775364d271c3e706c07227b13Christian Maeder predMap e1 == predMap e2 &&

b7413fd7a18b060775364d271c3e706c07227b13Christian Maeder extendedInfo e1 == extendedInfo e2

b7413fd7a18b060775364d271c3e706c07227b13Christian Maeder

b7413fd7a18b060775364d271c3e706c07227b13Christian MaederemptySign :: e -> Sign f e

b7413fd7a18b060775364d271c3e706c07227b13Christian MaederemptySign e = Sign

b7413fd7a18b060775364d271c3e706c07227b13Christian Maeder { sortSet = Set.empty

b7413fd7a18b060775364d271c3e706c07227b13Christian Maeder , emptySortSet = Set.empty

b7413fd7a18b060775364d271c3e706c07227b13Christian Maeder , sortRel = Rel.empty

b7413fd7a18b060775364d271c3e706c07227b13Christian Maeder , opMap = Map.empty

b7413fd7a18b060775364d271c3e706c07227b13Christian Maeder , assocOps = Map.empty

b7413fd7a18b060775364d271c3e706c07227b13Christian Maeder , predMap = Map.empty

b7413fd7a18b060775364d271c3e706c07227b13Christian Maeder , varMap = Map.empty

b7413fd7a18b060775364d271c3e706c07227b13Christian Maeder , sentences = []

b7413fd7a18b060775364d271c3e706c07227b13Christian Maeder , declaredSymbols = Set.empty

b7413fd7a18b060775364d271c3e706c07227b13Christian Maeder , envDiags = []

b7413fd7a18b060775364d271c3e706c07227b13Christian Maeder , annoMap = Map.empty

b7413fd7a18b060775364d271c3e706c07227b13Christian Maeder , globAnnos = emptyGlobalAnnos

b7413fd7a18b060775364d271c3e706c07227b13Christian Maeder , extendedInfo = e }

b7413fd7a18b060775364d271c3e706c07227b13Christian Maeder

class SignExtension e where

isSubSignExtension :: e -> e -> Bool

instance SignExtension () where

isSubSignExtension _ _ = True

-- | proper subsorts (possibly excluding input sort)

subsortsOf :: SORT -> Sign f e -> Set.Set SORT

subsortsOf s e = Rel.predecessors (sortRel e) s

-- | proper supersorts (possibly excluding input sort)

supersortsOf :: SORT -> Sign f e -> Set.Set SORT

supersortsOf s e = Rel.succs (sortRel e) s

toOP_TYPE :: OpType -> OP_TYPE

toOP_TYPE OpType { opArgs = args, opRes = res, opKind = k } =

Op_type k args res nullRange

toPRED_TYPE :: PredType -> PRED_TYPE

toPRED_TYPE PredType { predArgs = args } = Pred_type args nullRange

toOpType :: OP_TYPE -> OpType

toOpType (Op_type k args r _) = OpType k args r

toPredType :: PRED_TYPE -> PredType

toPredType (Pred_type args _) = PredType args

instance Pretty OpType where

pretty = pretty . toOP_TYPE

instance Pretty PredType where

pretty = pretty . toPRED_TYPE

instance (Show f, Pretty e) => Pretty (Sign f e) where

pretty = printSign pretty

instance Pretty Symbol where

pretty sy = let n = pretty (symName sy) in

case symbType sy of

SortAsItemType -> n

OtherTypeKind s -> text s <+> n

PredAsItemType pt -> let p = n <+> colon <+> pretty pt in

case predArgs pt of

[_] -> text predS <+> p

_ -> p

OpAsItemType ot -> let o = n <+> colon <> pretty ot in

case opArgs ot of

[] | opKind ot == Total -> text opS <+> o

_ -> o

instance Pretty SymbType where

pretty st = case st of

OpAsItemType ot -> pretty ot

PredAsItemType pt -> space <> pretty pt

_ -> empty

printSign :: (e -> Doc) -> Sign f e -> Doc

printSign fE s = let

printRel (supersort, subsorts) =

ppWithCommas (Set.toList subsorts) <+> text lessS <+>

idDoc supersort

esorts = emptySortSet s

nsorts = Set.difference (sortSet s) esorts in

(if Set.null nsorts then empty else text (sortS++sS) <+>

sepByCommas (map idDoc (Set.toList nsorts))) $+$

(if Set.null esorts then empty else text (esortS++sS) <+>

sepByCommas (map idDoc (Set.toList esorts))) $+$

(if Rel.null (sortRel s) then empty

else text (sortS++sS) <+>

(fsep $ punctuate semi $ map printRel $ Map.toList

$ Rel.toMap $ Rel.transpose $ sortRel s))

$+$ printSetMap (text opS) empty (opMap s)

$+$ printSetMap (text predS) space (predMap s)

$+$ fE (extendedInfo s)

-- working with Sign

irreflexClosure :: Ord a => Rel.Rel a -> Rel.Rel a

irreflexClosure = Rel.irreflex . Rel.transClosure

closeSortRel :: Sign f e -> Sign f e

closeSortRel s =

s { sortRel = irreflexClosure $ sortRel s }

diffSig :: (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e

diffSig dif a b = let s = sortSet a `Set.difference` sortSet b in

closeSortRel a

{ sortSet = s

, emptySortSet = Set.difference s

$ nonEmptySortSet a `Set.difference` nonEmptySortSet b

, sortRel = Rel.difference (sortRel a) $ sortRel b

, opMap = opMap a `diffOpMapSet` opMap b

, assocOps = assocOps a `diffOpMapSet` assocOps b

, predMap = predMap a `diffMapSet` predMap b

, annoMap = annoMap a `diffMapSet` annoMap b

, extendedInfo = dif (extendedInfo a) $ extendedInfo b }

-- transClosure needed: {a < b < c} - {a < c; b}

-- is not transitive!

diffOpMapSet :: OpMap -> OpMap -> OpMap

diffOpMapSet m = diffMapSet m . Map.map (rmOrAddParts False)

diffMapSet :: (Ord a, Ord b) => Map.Map a (Set.Set b)

-> Map.Map a (Set.Set b) -> Map.Map a (Set.Set b)

diffMapSet = Map.differenceWith

(\ s t -> let d = Set.difference s t in

if Set.null d then Nothing else Just d)

addMapSet :: (Ord a, Ord b) => Map.Map a (Set.Set b) -> Map.Map a (Set.Set b)

-> Map.Map a (Set.Set b)

addMapSet = Map.unionWith Set.union

mkPartial :: OpType -> OpType

mkPartial o = o { opKind = Partial }

mkTotal :: OpType -> OpType

mkTotal o = o { opKind = Total }

makePartial :: Set.Set OpType -> Set.Set OpType

makePartial = Set.mapMonotonic mkPartial

-- | remove (True) or add (False) partial op if it is included as total

rmOrAddParts :: Bool -> Set.Set OpType -> Set.Set OpType

rmOrAddParts b s =

let t = makePartial $ Set.filter ((== Total) . opKind) s

in (if b then Set.difference else Set.union) s t

addOpMapSet :: OpMap -> OpMap -> OpMap

addOpMapSet m = Map.map (rmOrAddParts True). addMapSet m

interMapSet :: (Ord a, Ord b) => Map.Map a (Set.Set b) -> Map.Map a (Set.Set b)

-> Map.Map a (Set.Set b)

interMapSet m =

Map.filter (not . Set.null) . Map.intersectionWith Set.intersection m

interOpMapSet :: OpMap -> OpMap -> OpMap

interOpMapSet m = Map.filter (not . Set.null)

. Map.intersectionWith

(\ s t -> rmOrAddParts True $ Set.intersection (rmOrAddParts False s)

$ rmOrAddParts False t) m

uniteCASLSign :: Sign () () -> Sign () () -> Sign () ()

uniteCASLSign = addSig (\_ _ -> ())

nonEmptySortSet :: Sign f e -> Set.Set Id

nonEmptySortSet s = Set.difference (sortSet s) $ emptySortSet s

addSig :: (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e

addSig ad a b = let s = sortSet a `Set.union` sortSet b in

closeSortRel a

{ sortSet = s

, emptySortSet = Set.difference s

$ nonEmptySortSet a `Set.union` nonEmptySortSet b

, sortRel = Rel.union (sortRel a) $ sortRel b

, opMap = addOpMapSet (opMap a) $ opMap b

, assocOps = addOpMapSet (assocOps a) $ assocOps b

, predMap = addMapSet (predMap a) $ predMap b

, annoMap = addMapSet (annoMap a) $ annoMap b

, extendedInfo = ad (extendedInfo a) $ extendedInfo b }

interRel :: Ord a => Rel.Rel a -> Rel.Rel a -> Rel.Rel a

interRel a = Rel.fromSet

. Set.intersection (Rel.toSet a) . Rel.toSet

interSig :: (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e

interSig ef a b = let s = sortSet a `Set.intersection` sortSet b in

closeSortRel a

{ sortSet = s

, emptySortSet = Set.difference s

$ nonEmptySortSet a `Set.intersection` nonEmptySortSet b

, sortRel = interRel (sortRel a) $ sortRel b

, opMap = interOpMapSet (opMap a) $ opMap b

, assocOps = interOpMapSet (assocOps a) $ assocOps b

, predMap = interMapSet (predMap a) $ predMap b

, annoMap = interMapSet (annoMap a) $ annoMap b

, extendedInfo = ef (extendedInfo a) $ extendedInfo b }

isEmptySig :: (e -> Bool) -> Sign f e -> Bool

isEmptySig ie s =

Set.null (sortSet s) &&

Rel.null (sortRel s) &&

Map.null (opMap s) &&

Map.null (predMap s) && ie (extendedInfo s)

isSubMapSet :: (Ord a, Ord b) => Map.Map a (Set.Set b) -> Map.Map a (Set.Set b)

-> Bool

isSubMapSet = Map.isSubmapOfBy Set.isSubsetOf

isSubOpMap :: OpMap -> OpMap -> Bool

isSubOpMap = Map.isSubmapOfBy $ \ s t ->

Set.fold ( \ e r -> r && (Set.member e t || case opKind e of

Partial -> Set.member (mkTotal e) t

Total -> False)) True s

isSubSig :: (e -> e -> Bool) -> Sign f e -> Sign f e -> Bool

isSubSig isSubExt a b = Set.isSubsetOf (sortSet a) (sortSet b)

&& Rel.isSubrelOf (sortRel a) (sortRel b)

-- ignore empty sort sorts

&& isSubOpMap (opMap a) (opMap b)

-- ignore associativity properties!

&& isSubMapSet (predMap a) (predMap b)

&& isSubExt (extendedInfo a) (extendedInfo b)

addDiags :: [Diagnosis] -> State.State (Sign f e) ()

addDiags ds = do

e <- State.get

State.put e { envDiags = reverse ds ++ envDiags e }

addAnnoSet :: Annoted a -> Symbol -> State.State (Sign f e) ()

addAnnoSet a s = do

addSymbol s

let v = Set.union (Set.fromList $ l_annos a) $ Set.fromList $ r_annos a

unless (Set.null v) $ do

e <- State.get

State.put e { annoMap = Map.insertWith Set.union s v $ annoMap e }

addSymbol :: Symbol -> State.State (Sign f e) ()

addSymbol s = do

e <- State.get

State.put e { declaredSymbols = Set.insert s $ declaredSymbols e }

addSort :: SortsKind -> Annoted a -> SORT -> State.State (Sign f e) ()

addSort sk a s = do

e <- State.get

let m = sortSet e

em = emptySortSet e

known = Set.member s m

if known then addDiags [mkDiag Hint "redeclared sort" s]

else do

State.put e { sortSet = Set.insert s m }

addDiags $ checkNamePrefix s

case sk of

NonEmptySorts -> when (Set.member s em) $ do

e2 <- State.get

State.put e2 { emptySortSet = Set.delete s em }

addDiags [mkDiag Warning "redeclared sort as non-empty" s]

PossiblyEmptySorts -> if known then

addDiags [mkDiag Warning "non-empty sort remains non-empty" s]

else do

e2 <- State.get

State.put e2 { emptySortSet = Set.insert s em }

addAnnoSet a $ Symbol s SortAsItemType

hasSort :: Sign f e -> SORT -> [Diagnosis]

hasSort e s =

[ mkDiag Error "unknown sort" s

| not $ Set.member s $ sortSet e ]

checkSorts :: [SORT] -> State.State (Sign f e) ()

checkSorts s = do

e <- State.get

addDiags $ concatMap (hasSort e) s

addSubsort :: SORT -> SORT -> State.State (Sign f e) ()

addSubsort = addSubsortOrIso True

addSubsortOrIso :: Bool -> SORT -> SORT -> State.State (Sign f e) ()

addSubsortOrIso b super sub = do

when b $ checkSorts [super, sub]

e <- State.get

let r = sortRel e

State.put e { sortRel = (if b then id else Rel.insert super sub)

$ Rel.insert sub super r }

let p = posOfId sub

rel = " '" ++

showDoc sub (if b then " < " else " = ") ++ showDoc super "'"

if super == sub then addDiags [mkDiag Warning "void reflexive subsort" sub]

else if b then

if Rel.path super sub r then

if Rel.path sub super r

then addDiags [Diag Warning ("sorts are isomorphic" ++ rel) p]

else addDiags [Diag Warning ("added subsort cycle by" ++ rel) p]

else when (Rel.path sub super r)

$ addDiags [Diag Hint ("redeclared subsort" ++ rel) p]

else if Rel.path super sub r then

if Rel.path sub super r

then addDiags [Diag Hint ("redeclared isomoprhic sorts" ++ rel) p]

else addDiags [Diag Warning ("subsort '" ++

showDoc super "' made isomorphic by" ++ rel) $ posOfId super]

else when (Rel.path sub super r)

$ addDiags [Diag Warning ("subsort '" ++

showDoc sub "' made isomorphic by" ++ rel) p]

closeSubsortRel :: State.State (Sign f e) ()

closeSubsortRel=

do e <- State.get

State.put e { sortRel = Rel.transClosure $ sortRel e }

checkNamePrefix :: Id -> [Diagnosis]

checkNamePrefix i =

[ mkDiag Warning "identifier may conflict with generated names" i

| isPrefixOf genNamePrefix $ showId i ""]

alsoWarning :: String -> String -> Id -> [Diagnosis]

alsoWarning new old i = let is = ' ' : showId i "'" in

[Diag Warning ("new '" ++ new ++ is ++ " is also known as '" ++ old ++ is)

$ posOfId i]

checkWithOtherMap :: String -> String -> Map.Map Id a -> Id -> [Diagnosis]

checkWithOtherMap s1 s2 m i =

case Map.lookup i m of

Nothing -> []

Just _ -> alsoWarning s1 s2 i

addVars :: VAR_DECL -> State.State (Sign f e) ()

addVars (Var_decl vs s _) = do

checkSorts [s]

mapM_ (addVar s) vs

addVar :: SORT -> SIMPLE_ID -> State.State (Sign f e) ()

addVar s v =

do e <- State.get

let m = varMap e

i = simpleIdToId v

ds = case Map.lookup v m of

Just _ -> [mkDiag Hint "known variable shadowed" v]

Nothing -> []

State.put e { varMap = Map.insert v s m }

addDiags $ ds ++ checkWithOtherMap varS opS (opMap e) i

++ checkWithOtherMap varS predS (predMap e) i

++ checkNamePrefix i

addOpTo :: Id -> OpType -> OpMap -> OpMap

addOpTo k v m =

let l = Map.findWithDefault Set.empty k m

in Map.insert k (Set.insert v l) m

-- | extract the sort from an analysed term

sortOfTerm :: TERM f -> SORT

sortOfTerm t = case t of

Qual_var _ ty _ -> ty

Application (Qual_op_name _ ot _) _ _ -> res_OP_TYPE ot

Sorted_term _ ty _ -> ty

Cast _ ty _ -> ty

Conditional t1 _ _ _ -> sortOfTerm t1

_ -> genName "unknown"

-- | create binding if variables are non-null

mkForall :: [VAR_DECL] -> FORMULA f -> Range -> FORMULA f

mkForall vl f ps = if null vl then f else Quantification Universal vl f ps

-- | convert a singleton variable declaration into a qualified variable

toQualVar :: VAR_DECL -> TERM f

toQualVar (Var_decl v s ps) =

if isSingle v then Qual_var (head v) s ps else error "toQualVar"