2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina{- |

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinaModule : $Header$

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinaDescription : CASL signatures and local environments for basic analysis

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinaCopyright : (c) Christian Maeder and Uni Bremen 2002-2006

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinaLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinaMaintainer : Christian.Maeder@dfki.de

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinaStability : provisional

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinaPortability : portable

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinaCASL signatures also serve as local environments for the basic static analysis

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina-}

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinamodule CASL.Sign where

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaimport CASL.AS_Basic_CASL

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaimport CASL.ToDoc ()

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaimport qualified Data.Map as Map

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaimport qualified Data.Set as Set

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaimport qualified Common.Lib.Rel as Rel

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaimport qualified Common.Lib.State as State

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaimport Common.Keywords

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaimport Common.Id

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaimport Common.Result

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaimport Common.AS_Annotation

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaimport Common.GlobalAnnotations

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaimport Common.Doc

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaimport Common.DocUtils

c9aab1c04c399ca2d1abef74f6df22ced34983dcPavel Březina

d117004902c767d46430848b6ef1c11c3ad82835Pavel Březinaimport Data.List (isPrefixOf)

2a25713afc6beefb11a799903a43f695c5d7a4f9Adam Tkacimport Control.Monad (when, unless)

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina-- constants have empty argument lists

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinadata OpType = OpType {opKind :: OpKind, opArgs :: [SORT], opRes :: SORT}

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina deriving (Show, Eq, Ord)

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinadata PredType = PredType {predArgs :: [SORT]} deriving (Show, Eq, Ord)

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinatype OpMap = Map.Map Id (Set.Set OpType)

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

4f3a9d837a55b49448eca3c713c85a406207e523Simo Sorcedata SymbType = SortAsItemType

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina | OtherTypeKind String

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina | OpAsItemType OpType

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina -- since symbols do not speak about totality, the totality

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina -- information in OpType has to be ignored

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina | PredAsItemType PredType

4f3a9d837a55b49448eca3c713c85a406207e523Simo Sorce deriving (Show, Eq, Ord)

4f3a9d837a55b49448eca3c713c85a406207e523Simo Sorce

4f3a9d837a55b49448eca3c713c85a406207e523Simo Sorcedata Symbol = Symbol {symName :: Id, symbType :: SymbType}

4f3a9d837a55b49448eca3c713c85a406207e523Simo Sorce deriving (Show, Eq, Ord)

4f3a9d837a55b49448eca3c713c85a406207e523Simo Sorce

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinainstance GetRange Symbol where

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina getRange = getRange . symName

a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov

a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai KondrashovidToSortSymbol :: Id -> Symbol

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinaidToSortSymbol idt = Symbol idt SortAsItemType

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinaidToOpSymbol :: Id -> OpType -> Symbol

4f3a9d837a55b49448eca3c713c85a406207e523Simo SorceidToOpSymbol idt = Symbol idt . OpAsItemType

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinaidToPredSymbol :: Id -> PredType -> Symbol

a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai KondrashovidToPredSymbol idt = Symbol idt . PredAsItemType

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinadummy :: Sign f s -> a -> ()

4f3a9d837a55b49448eca3c713c85a406207e523Simo Sorcedummy _ _ = ()

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinadummyMin :: b -> c -> Result ()

4f3a9d837a55b49448eca3c713c85a406207e523Simo SorcedummyMin _ _ = return ()

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinatype CASLSign = Sign () ()

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina{- | the data type for the basic static analysis to accumulate variables,

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinasentences, symbols, diagnostics and annotations, that are removed or ignored

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinawhen looking at signatures from outside, i.e. during logic-independent

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaprocessing. -}

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinadata Sign f e = Sign

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina { sortSet :: Set.Set SORT

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina , emptySortSet :: Set.Set SORT

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina -- ^ a subset of the sort set of possibly empty sorts

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina , sortRel :: Rel.Rel SORT

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina , opMap :: OpMap

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina , assocOps :: OpMap -- ^ the subset of associative operators

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina , predMap :: Map.Map Id (Set.Set PredType)

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina , varMap :: Map.Map SIMPLE_ID SORT -- ^ temporary variables

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina , sentences :: [Named (FORMULA f)] -- ^ current sentences

710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina , declaredSymbols :: Set.Set Symbol -- ^ introduced or redeclared symbols

a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov , envDiags :: [Diagnosis] -- ^ diagnostics for basic spec

a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov , annoMap :: Map.Map Symbol (Set.Set Annotation) -- ^ annotated symbols

710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina , globAnnos :: GlobalAnnos -- ^ global annotations to use

710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina , extendedInfo :: e

710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina } deriving Show

7379170a0860790f2739e07fffe3d6ec85264566Pavel Březina

710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina-- better ignore assoc flags for equality

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinainstance Eq e => Eq (Sign f e) where

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina a == b = compare a {extendedInfo = ()} b {extendedInfo = ()} == EQ

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina && extendedInfo a == extendedInfo b

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinainstance Ord e => Ord (Sign f e) where

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina compare a b = compare

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (sortSet a, emptySortSet a, sortRel a, opMap a, predMap a, extendedInfo a)

b3ca35780617b2e5a7637f9888b089e8e26a4e8cPavel Březina (sortSet b, emptySortSet b, sortRel b, opMap b, predMap b, extendedInfo b)

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinaemptySign :: e -> Sign f e

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinaemptySign e = Sign

5ff1c3c5a12930692cb6284d14f7fda3a974af8ePavel Březina { sortSet = Set.empty

b0abb3bfdfd95951a23c9fc223c735805ffd2969Pavel Březina , emptySortSet = Set.empty

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina , sortRel = Rel.empty

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina , opMap = Map.empty

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina , assocOps = Map.empty

c9aab1c04c399ca2d1abef74f6df22ced34983dcPavel Březina , predMap = Map.empty

b0abb3bfdfd95951a23c9fc223c735805ffd2969Pavel Březina , varMap = Map.empty

c9aab1c04c399ca2d1abef74f6df22ced34983dcPavel Březina , sentences = []

b0abb3bfdfd95951a23c9fc223c735805ffd2969Pavel Březina , declaredSymbols = Set.empty

c9aab1c04c399ca2d1abef74f6df22ced34983dcPavel Březina , envDiags = []

55fdd0d28e7c88f333ad78183b0ba37a1da34160Pavel Březina , annoMap = Map.empty

a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov , globAnnos = emptyGlobalAnnos

a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov , extendedInfo = e }

55fdd0d28e7c88f333ad78183b0ba37a1da34160Pavel Březina

b0abb3bfdfd95951a23c9fc223c735805ffd2969Pavel Březinaclass SignExtension e where

b0abb3bfdfd95951a23c9fc223c735805ffd2969Pavel Březina isSubSignExtension :: e -> e -> Bool

c9aab1c04c399ca2d1abef74f6df22ced34983dcPavel Březina symOfExtension :: e -> Set.Set Symbol

c9aab1c04c399ca2d1abef74f6df22ced34983dcPavel Březina symOfExtension _ = Set.empty

c9aab1c04c399ca2d1abef74f6df22ced34983dcPavel Březina

c9aab1c04c399ca2d1abef74f6df22ced34983dcPavel Březinainstance SignExtension () where

55fdd0d28e7c88f333ad78183b0ba37a1da34160Pavel Březina isSubSignExtension _ _ = True

a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov

a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov-- | proper subsorts (possibly excluding input sort)

c9aab1c04c399ca2d1abef74f6df22ced34983dcPavel BřezinasubsortsOf :: SORT -> Sign f e -> Set.Set SORT

c9aab1c04c399ca2d1abef74f6df22ced34983dcPavel BřezinasubsortsOf s e = Rel.predecessors (sortRel e) s

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

b0abb3bfdfd95951a23c9fc223c735805ffd2969Pavel Březina-- | proper supersorts (possibly excluding input sort)

7379170a0860790f2739e07fffe3d6ec85264566Pavel BřezinasupersortsOf :: SORT -> Sign f e -> Set.Set SORT

710472d946f6c337a095699dfd79134fa8b9eab9Pavel BřezinasupersortsOf s e = Rel.succs (sortRel e) s

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinatoOP_TYPE :: OpType -> OP_TYPE

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinatoOP_TYPE OpType { opArgs = args, opRes = res, opKind = k } =

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina Op_type k args res nullRange

b0abb3bfdfd95951a23c9fc223c735805ffd2969Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinatoPRED_TYPE :: PredType -> PRED_TYPE

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinatoPRED_TYPE PredType { predArgs = args } = Pred_type args nullRange

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinatoOpType :: OP_TYPE -> OpType

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinatoOpType (Op_type k args r _) = OpType k args r

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinatoPredType :: PRED_TYPE -> PredType

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinatoPredType (Pred_type args _) = PredType args

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinainstance Pretty OpType where

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina pretty = pretty . toOP_TYPE

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinainstance Pretty PredType where

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina pretty = pretty . toPRED_TYPE

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinainstance (Show f, Pretty e) => Pretty (Sign f e) where

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina pretty = printSign pretty

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

b0abb3bfdfd95951a23c9fc223c735805ffd2969Pavel Březinainstance Pretty Symbol where

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina pretty sy = let n = pretty (symName sy) in

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina case symbType sy of

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina SortAsItemType -> n

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina OtherTypeKind s -> text s <+> n

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

b0abb3bfdfd95951a23c9fc223c735805ffd2969Pavel Březina case predArgs pt of

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina [_] -> text predS <+> p

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina _ -> p

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina OpAsItemType ot -> let o = n <+> colon <> pretty ot in

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina case opArgs ot of

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina [] | opKind ot == Total -> text opS <+> o

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina _ -> o

b3ca35780617b2e5a7637f9888b089e8e26a4e8cPavel Březina

d38ffc9c92daeb62de7d28c409bdaeff98f82775Pavel Březinainstance Pretty SymbType where

76db25eab9010a33657f35e5afc8477c996df7a3Pavel Březina pretty st = case st of

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina OpAsItemType ot -> pretty ot

d38ffc9c92daeb62de7d28c409bdaeff98f82775Pavel Březina PredAsItemType pt -> space <> pretty pt

710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina _ -> empty

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinaprintSign :: (e -> Doc) -> Sign f e -> Doc

4f3a9d837a55b49448eca3c713c85a406207e523Simo SorceprintSign fE s = let

4f3a9d837a55b49448eca3c713c85a406207e523Simo Sorce printRel (supersort, subsorts) =

46d3d2c731e8c7e138462e5b60a39a279dc77d81Pavel Březina ppWithCommas (Set.toList subsorts) <+> text lessS <+>

46d3d2c731e8c7e138462e5b60a39a279dc77d81Pavel Březina idDoc supersort

46d3d2c731e8c7e138462e5b60a39a279dc77d81Pavel Březina esorts = emptySortSet s

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina srel = sortRel s

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina cs = Rel.sccOfClosure $ Rel.transClosure srel

b0abb3bfdfd95951a23c9fc223c735805ffd2969Pavel Březina nsorts = Set.difference (sortSet s) esorts in

1509d1723d39124f840c214327e698aff3b3f683Pavel Březina (if Set.null nsorts then empty else text (sortS ++ sS) <+>

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

1509d1723d39124f840c214327e698aff3b3f683Pavel Březina (if Set.null esorts then empty else text (esortS ++ sS) <+>

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina sepByCommas (map idDoc (Set.toList esorts))) $+$

46d3d2c731e8c7e138462e5b60a39a279dc77d81Pavel Březina (if Rel.null srel then empty

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina else text (sortS ++ sS) <+>

710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina fsep (punctuate semi $

41ef946f3f74a46b9e26118116e4811e259b30efPavel Březina map (fsep . punctuate (space <> equals) . map pretty)

46d3d2c731e8c7e138462e5b60a39a279dc77d81Pavel Březina (filter ((> 1) . length) $ map Set.toList cs)

a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov ++ map printRel (Map.toList

46d3d2c731e8c7e138462e5b60a39a279dc77d81Pavel Březina $ Rel.toMap $ Rel.transpose $ Rel.transReduce $ Rel.irreflex

41ef946f3f74a46b9e26118116e4811e259b30efPavel Březina $ Rel.collaps cs srel)))

41ef946f3f74a46b9e26118116e4811e259b30efPavel Březina $+$ printSetMap (text opS) empty (opMap s)

4f3a9d837a55b49448eca3c713c85a406207e523Simo Sorce $+$ printSetMap (text predS) space (predMap s)

4f3a9d837a55b49448eca3c713c85a406207e523Simo Sorce $+$ fE (extendedInfo s)

4f3a9d837a55b49448eca3c713c85a406207e523Simo Sorce

04b3ab7658985af749460010123bbe37eccf50edPavel Březina-- working with Sign

b510d909cbe8d8216b60ee070730dd5c41294303Pavel Březina

b510d909cbe8d8216b60ee070730dd5c41294303Pavel BřezinairreflexClosure :: Ord a => Rel.Rel a -> Rel.Rel a

a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai KondrashovirreflexClosure = Rel.irreflex . Rel.transClosure

a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov

b510d909cbe8d8216b60ee070730dd5c41294303Pavel BřezinacloseSortRel :: Sign f e -> Sign f e

b510d909cbe8d8216b60ee070730dd5c41294303Pavel BřezinacloseSortRel s =

b510d909cbe8d8216b60ee070730dd5c41294303Pavel Březina s { sortRel = irreflexClosure $ sortRel s }

b510d909cbe8d8216b60ee070730dd5c41294303Pavel Březina

a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai KondrashovdiffSig :: (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e

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

b510d909cbe8d8216b60ee070730dd5c41294303Pavel Březina closeSortRel a

b510d909cbe8d8216b60ee070730dd5c41294303Pavel Březina { sortSet = s

a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov , emptySortSet = Set.difference s

a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov $ nonEmptySortSet a `Set.difference` nonEmptySortSet b

04b3ab7658985af749460010123bbe37eccf50edPavel Březina , sortRel = Rel.difference (sortRel a) $ sortRel b

04b3ab7658985af749460010123bbe37eccf50edPavel Březina , opMap = opMap a `diffOpMapSet` opMap b

04b3ab7658985af749460010123bbe37eccf50edPavel Březina , assocOps = assocOps a `diffOpMapSet` assocOps b

04b3ab7658985af749460010123bbe37eccf50edPavel Březina , predMap = predMap a `diffMapSet` predMap b

46d3d2c731e8c7e138462e5b60a39a279dc77d81Pavel Březina , annoMap = annoMap a `diffMapSet` annoMap b

4f3a9d837a55b49448eca3c713c85a406207e523Simo Sorce , extendedInfo = dif (extendedInfo a) $ extendedInfo b }

46d3d2c731e8c7e138462e5b60a39a279dc77d81Pavel Březina -- transClosure needed: {a < b < c} - {a < c; b}

a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov -- is not transitive!

46d3d2c731e8c7e138462e5b60a39a279dc77d81Pavel Březina

b0abb3bfdfd95951a23c9fc223c735805ffd2969Pavel BřezinadiffOpMapSet :: OpMap -> OpMap -> OpMap

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinadiffOpMapSet m = diffMapSet m . Map.map (rmOrAddParts False)

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

15d41c8f28259061e39715acdbbbaea778b6ecc8Pavel BřezinadiffMapSet :: (Ord a, Ord b) => Map.Map a (Set.Set b)

15d41c8f28259061e39715acdbbbaea778b6ecc8Pavel Březina -> Map.Map a (Set.Set b) -> Map.Map a (Set.Set b)

15d41c8f28259061e39715acdbbbaea778b6ecc8Pavel BřezinadiffMapSet = Map.differenceWith

15d41c8f28259061e39715acdbbbaea778b6ecc8Pavel Březina (\ s t -> let d = Set.difference s t in

15d41c8f28259061e39715acdbbbaea778b6ecc8Pavel Březina if Set.null d then Nothing else Just d)

15d41c8f28259061e39715acdbbbaea778b6ecc8Pavel Březina

15d41c8f28259061e39715acdbbbaea778b6ecc8Pavel BřezinaaddMapSet :: (Ord a, Ord b) => Map.Map a (Set.Set b) -> Map.Map a (Set.Set b)

15d41c8f28259061e39715acdbbbaea778b6ecc8Pavel Březina -> Map.Map a (Set.Set b)

b3ca35780617b2e5a7637f9888b089e8e26a4e8cPavel BřezinaaddMapSet = Map.unionWith Set.union

b3ca35780617b2e5a7637f9888b089e8e26a4e8cPavel Březina

b3ca35780617b2e5a7637f9888b089e8e26a4e8cPavel BřezinamkPartial :: OpType -> OpType

d38ffc9c92daeb62de7d28c409bdaeff98f82775Pavel BřezinamkPartial o = o { opKind = Partial }

d38ffc9c92daeb62de7d28c409bdaeff98f82775Pavel Březina

d38ffc9c92daeb62de7d28c409bdaeff98f82775Pavel BřezinamkTotal :: OpType -> OpType

d38ffc9c92daeb62de7d28c409bdaeff98f82775Pavel BřezinamkTotal o = o { opKind = Total }

d38ffc9c92daeb62de7d28c409bdaeff98f82775Pavel Březina

b3ca35780617b2e5a7637f9888b089e8e26a4e8cPavel BřezinamakePartial :: Set.Set OpType -> Set.Set OpType

d38ffc9c92daeb62de7d28c409bdaeff98f82775Pavel BřezinamakePartial = Set.mapMonotonic mkPartial

d38ffc9c92daeb62de7d28c409bdaeff98f82775Pavel Březina

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

d38ffc9c92daeb62de7d28c409bdaeff98f82775Pavel BřezinarmOrAddParts :: Bool -> Set.Set OpType -> Set.Set OpType

b3ca35780617b2e5a7637f9888b089e8e26a4e8cPavel BřezinarmOrAddParts b s =

d38ffc9c92daeb62de7d28c409bdaeff98f82775Pavel Březina let t = makePartial $ Set.filter ((== Total) . opKind) s

d38ffc9c92daeb62de7d28c409bdaeff98f82775Pavel Březina in (if b then Set.difference else Set.union) s t

b3ca35780617b2e5a7637f9888b089e8e26a4e8cPavel Březina

d38ffc9c92daeb62de7d28c409bdaeff98f82775Pavel BřezinaaddOpMapSet :: OpMap -> OpMap -> OpMap

b3ca35780617b2e5a7637f9888b089e8e26a4e8cPavel BřezinaaddOpMapSet m = Map.map (rmOrAddParts True) . addMapSet m

d38ffc9c92daeb62de7d28c409bdaeff98f82775Pavel Březina

d38ffc9c92daeb62de7d28c409bdaeff98f82775Pavel BřezinainterMapSet :: (Ord a, Ord b) => Map.Map a (Set.Set b) -> Map.Map a (Set.Set b)

d38ffc9c92daeb62de7d28c409bdaeff98f82775Pavel Březina -> Map.Map a (Set.Set b)

d38ffc9c92daeb62de7d28c409bdaeff98f82775Pavel BřezinainterMapSet m =

b3ca35780617b2e5a7637f9888b089e8e26a4e8cPavel Březina Map.filter (not . Set.null) . Map.intersectionWith Set.intersection m

b3ca35780617b2e5a7637f9888b089e8e26a4e8cPavel Březina

d38ffc9c92daeb62de7d28c409bdaeff98f82775Pavel BřezinainterOpMapSet :: OpMap -> OpMap -> OpMap

46d3d2c731e8c7e138462e5b60a39a279dc77d81Pavel BřezinainterOpMapSet m = Map.filter (not . Set.null)

b3ca35780617b2e5a7637f9888b089e8e26a4e8cPavel Březina . Map.intersectionWith

b3ca35780617b2e5a7637f9888b089e8e26a4e8cPavel Březina (\ s t -> rmOrAddParts True $ Set.intersection (rmOrAddParts False s)

46d3d2c731e8c7e138462e5b60a39a279dc77d81Pavel Březina $ rmOrAddParts False t) m

46d3d2c731e8c7e138462e5b60a39a279dc77d81Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinauniteCASLSign :: Sign () () -> Sign () () -> Sign () ()

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinauniteCASLSign = addSig (\ _ _ -> ())

b3ca35780617b2e5a7637f9888b089e8e26a4e8cPavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinanonEmptySortSet :: Sign f e -> Set.Set Id

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinanonEmptySortSet s = Set.difference (sortSet s) $ emptySortSet s

710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina

c47e9d522f0d87259e5074ea643daaa3dfcb8d92Pavel BřezinaaddSig :: (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e

76db25eab9010a33657f35e5afc8477c996df7a3Pavel BřezinaaddSig ad a b = let s = sortSet a `Set.union` sortSet b in

710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina closeSortRel a

c47e9d522f0d87259e5074ea643daaa3dfcb8d92Pavel Březina { sortSet = s

710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina , emptySortSet = Set.difference s

710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina $ nonEmptySortSet a `Set.union` nonEmptySortSet b

76db25eab9010a33657f35e5afc8477c996df7a3Pavel Březina , sortRel = Rel.union (sortRel a) $ sortRel b

c47e9d522f0d87259e5074ea643daaa3dfcb8d92Pavel Březina , opMap = addOpMapSet (opMap a) $ opMap b

c47e9d522f0d87259e5074ea643daaa3dfcb8d92Pavel Březina , assocOps = addOpMapSet (assocOps a) $ assocOps b

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina , predMap = addMapSet (predMap a) $ predMap b

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina , annoMap = addMapSet (annoMap a) $ annoMap b

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina , extendedInfo = ad (extendedInfo a) $ extendedInfo b }

04b3ab7658985af749460010123bbe37eccf50edPavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinainterRel :: Ord a => Rel.Rel a -> Rel.Rel a -> Rel.Rel a

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinainterRel a = Rel.fromSet

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina . Set.intersection (Rel.toSet a) . Rel.toSet

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinainterSig :: (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinainterSig ef a b = let s = sortSet a `Set.intersection` sortSet b in

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina closeSortRel a

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina { sortSet = s

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina , emptySortSet = Set.difference s

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina $ nonEmptySortSet a `Set.intersection` nonEmptySortSet b

c47e9d522f0d87259e5074ea643daaa3dfcb8d92Pavel Březina , sortRel = interRel (sortRel a) $ sortRel b

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina , opMap = interOpMapSet (opMap a) $ opMap b

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina , assocOps = interOpMapSet (assocOps a) $ assocOps b

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina , predMap = interMapSet (predMap a) $ predMap b

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina , annoMap = interMapSet (annoMap a) $ annoMap b

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina , 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 -> (&& (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"

mkImpl :: FORMULA f -> FORMULA f -> FORMULA f

mkImpl f f' = Implication f f' True nullRange

mkExEq :: TERM f -> TERM f -> FORMULA f

mkExEq f f' = Existl_equation f f' nullRange

mkStEq :: TERM f -> TERM f -> FORMULA f

mkStEq u v = Strong_equation u v nullRange

mkEqv :: FORMULA f -> FORMULA f -> FORMULA f

mkEqv u v = Equivalence u v nullRange

mkAppl :: OP_SYMB -> [TERM f] -> TERM f

mkAppl op_symb fs = Application op_symb fs nullRange

-- | turn sorted variable into variable delcaration

mkVarDecl :: VAR -> SORT -> VAR_DECL

mkVarDecl v s = Var_decl [v] s nullRange

-- | turn sorted variable into term

mkVarTerm :: VAR -> SORT -> TERM f

mkVarTerm v = toQualVar . mkVarDecl v

-- | optimized conjunction

conjunct :: [FORMULA f] -> FORMULA f

conjunct fs = case fs of

[] -> True_atom nullRange

[phi] -> phi

_ -> Conjunction fs nullRange

mkVarDeclStr :: String -> SORT -> VAR_DECL

mkVarDeclStr = mkVarDecl . mkSimpleId

mkAxName :: String -> SORT -> SORT -> String

mkAxName str s s' = "ga_" ++ str ++ "_" ++ show s ++ "_to_" ++ show s'

mkAxNameSingle :: String -> SORT -> String

mkAxNameSingle str s = "ga_" ++ str ++ "_" ++ show s