{-# LANGUAGE DeriveDataTypeable #-}

{- |

Module : ./CASL/Sign.hs

Description : CASL signatures and local environments for basic analysis

Copyright : (c) Christian Maeder and Uni Bremen 2002-2006

License : GPLv2 or higher, see LICENSE.txt

Maintainer : Christian.Maeder@dfki.de

Stability : provisional

Portability : portable

CASL signatures also serve as local environments for the basic static analysis

-}

module CASL.Sign where

import CASL.AS_Basic_CASL

import CASL.Fold

import CASL.ToDoc ()

import qualified Data.Map as Map

import qualified Data.Set as Set

import qualified Common.Lib.MapSet as MapSet

import qualified Common.Lib.Rel as Rel

import qualified Common.Lib.State as State

import Common.Keywords

import Common.Id

import Common.Result

import Common.AS_Annotation

import Common.GlobalAnnotations

import Common.Prec (mkPrecIntMap, PrecMap)

import Common.Doc

import Common.DocUtils

import Data.Data

import Data.Maybe (fromMaybe)

import Data.List (isPrefixOf)

import Control.Monad (when, unless)

-- constants have empty argument lists

data OpType = OpType {opKind :: OpKind, opArgs :: [SORT], opRes :: SORT}

deriving (Show, Eq, Ord, Typeable, Data)

-- | result sort added to argument sorts

opSorts :: OpType -> [SORT]

opSorts o = opRes o : opArgs o

mkTotOpType :: [SORT] -> SORT -> OpType

mkTotOpType = OpType Total

sortToOpType :: SORT -> OpType

sortToOpType = mkTotOpType []

isSingleArgOp :: OpType -> Bool

isSingleArgOp = isSingle . opArgs

data PredType = PredType {predArgs :: [SORT]} deriving (Show, Eq, Ord, Typeable, Data)

sortToPredType :: SORT -> PredType

sortToPredType s = PredType [s]

isBinPredType :: PredType -> Bool

isBinPredType (PredType l) = case l of

[_, _] -> True

_ -> False

type OpMap = MapSet.MapSet OP_NAME OpType

type PredMap = MapSet.MapSet PRED_NAME PredType

type AnnoMap = MapSet.MapSet Symbol Annotation

data SymbType = SortAsItemType

| SubsortAsItemType SORT -- special symbols for xml output

| OpAsItemType OpType

{- since symbols do not speak about totality, the totality

information in OpType has to be ignored -}

| PredAsItemType PredType

deriving (Show, Eq, Ord, Typeable, Data)

symbolKind :: SymbType -> SYMB_KIND

symbolKind t = case t of

OpAsItemType _ -> Ops_kind

PredAsItemType _ -> Preds_kind

_ -> Sorts_kind

data Symbol = Symbol {symName :: Id, symbType :: SymbType}

deriving (Show, Eq, Ord, Typeable, Data)

instance GetRange Symbol where

getRange = getRange . symName

rangeSpan = rangeSpan . symName

idToSortSymbol :: Id -> Symbol

idToSortSymbol idt = Symbol idt SortAsItemType

idToOpSymbol :: Id -> OpType -> Symbol

idToOpSymbol idt = Symbol idt . OpAsItemType

idToPredSymbol :: Id -> PredType -> Symbol

idToPredSymbol idt = Symbol idt . PredAsItemType

type CASLSign = Sign () ()

{- | the data type for the basic static analysis to accumulate variables,

sentences, symbols, diagnostics and annotations, that are removed or ignored

when looking at signatures from outside, i.e. during logic-independent

processing. -}

data Sign f e = Sign

{ sortRel :: Rel.Rel SORT

-- ^ every sort is a subsort of itself

, revSortRel :: Maybe (Rel.Rel SORT)

-- ^ reverse sort relation for more efficient lookup of subsorts

, emptySortSet :: Set.Set SORT

-- ^ a subset of the sort set of possibly empty sorts

, opMap :: OpMap

, assocOps :: OpMap -- ^ the subset of associative operators

, predMap :: PredMap

, varMap :: Map.Map SIMPLE_ID SORT -- ^ temporary variables

, sentences :: [Named (FORMULA f)] -- ^ current sentences

, declaredSymbols :: Set.Set Symbol -- ^ introduced or redeclared symbols

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

, annoMap :: AnnoMap -- ^ annotated symbols

, globAnnos :: GlobalAnnos -- ^ global annotations to use

, extendedInfo :: e

} deriving (Show, Typeable, Data)

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

sortSet = Rel.keysSet . sortRel

-- better ignore assoc flags for equality

instance Eq e => Eq (Sign f e) where

a == b = compare a {extendedInfo = ()} b {extendedInfo = ()} == EQ

&& extendedInfo a == extendedInfo b

instance Ord e => Ord (Sign f e) where

compare a b = compare

(emptySortSet a, sortRel a, opMap a, predMap a, extendedInfo a)

(emptySortSet b, sortRel b, opMap b, predMap b, extendedInfo b)

emptySign :: e -> Sign f e

emptySign e = Sign

{ sortRel = Rel.empty

, revSortRel = Nothing

, emptySortSet = Set.empty

, opMap = MapSet.empty

, assocOps = MapSet.empty

, predMap = MapSet.empty

, varMap = Map.empty

, sentences = []

, declaredSymbols = Set.empty

, envDiags = []

, annoMap = MapSet.empty

, globAnnos = emptyGlobalAnnos

, extendedInfo = e }

embedSign :: e -> Sign f1 e1 -> Sign f e

embedSign e sign = (emptySign e)

{ sortRel = sortRel sign

, opMap = opMap sign

, assocOps = assocOps sign

, predMap = predMap sign }

mapForm :: f -> FORMULA f1 -> FORMULA f

mapForm c = foldFormula $ mapRecord (const c)

mapFORMULA :: FORMULA f1 -> FORMULA f

mapFORMULA = mapForm $ error "CASL.mapFORMULA"

embedTheory :: (FORMULA f1 -> FORMULA f) -> e

-> (Sign f1 e1, [Named (FORMULA f1)])

-> (Sign f e, [Named (FORMULA f)])

embedTheory f e (sign, sens) =

(embedSign e sign, map (mapNamed f) sens)

embedCASLTheory :: e -> (Sign f1 e1, [Named (FORMULA f1)])

-> (Sign f e, [Named (FORMULA f)])

embedCASLTheory = embedTheory mapFORMULA

getSyntaxTable :: Sign f e -> (PrecMap, AssocMap)

getSyntaxTable sig = let gannos = globAnnos sig

in (mkPrecIntMap $ prec_annos gannos, assoc_annos gannos)

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 = case revSortRel e of

Nothing -> Rel.predecessors (sortRel e) s

Just r -> Rel.succs r s

setRevSortRel :: Sign f e -> Sign f e

setRevSortRel s = s { revSortRel = Just . Rel.transpose $ sortRel 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 -> keyword sortS <+> n

SubsortAsItemType s -> keyword sortS <+> n <+> less <+> pretty s

PredAsItemType pt -> keyword predS <+> n <+> colon <+> pretty pt

OpAsItemType ot -> keyword opS <+> n <+> colon <> pretty ot

eqAndSubsorts :: Bool -> Rel.Rel SORT -> ([[SORT]], [(SORT, [SORT])])

eqAndSubsorts groupSubsorts srel = let

cs = Rel.sccOfClosure srel

in ( filter ((> 1) . length) $ map Set.toList cs

, Map.toList . Map.map Set.toList . Rel.toMap . Rel.rmNullSets

. (if groupSubsorts then Rel.transpose else id)

. Rel.transReduce . Rel.irreflex $ Rel.collaps cs srel)

singleAndRelatedSorts :: Rel.Rel SORT -> ([SORT], [[SORT]])

singleAndRelatedSorts srel = let

ss = Rel.keysSet srel

rs = Rel.sccOfClosure

. Rel.transClosure . Rel.union srel $ Rel.transpose srel

is = Set.difference ss $ Set.unions rs

in (Set.toList is, map Set.toList rs)

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

printSign fE s = let

printRel (supersort, subsorts) =

ppWithCommas subsorts <+> text lessS <+>

idDoc supersort

esorts = emptySortSet s

srel = sortRel s

(es, ss) = eqAndSubsorts True srel

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.noPairs srel then empty

else text (sortS ++ sS) <+>

fsep (punctuate semi $

map (fsep . punctuate (space <> equals) . map pretty) es

++ map printRel ss))

$+$ printSetMap (text opS) empty (MapSet.toMap $ opMap s)

$+$ printSetMap (text predS) space (MapSet.toMap $ predMap s)

$+$ fE (extendedInfo s)

-- working with Sign

closeSortRel :: Sign f e -> Sign f e

closeSortRel s =

s { sortRel = Rel.transClosure $ sortRel s }

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

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

-- op kinds of op types

setOpKind :: OpKind -> OpType -> OpType

setOpKind k o = o { opKind = k }

mkPartial :: OpType -> OpType

mkPartial = setOpKind Partial

mkTotal :: OpType -> OpType

mkTotal = setOpKind Total

isTotal :: OpType -> Bool

isTotal = (== Total) . opKind

isPartial :: OpType -> Bool

isPartial = not . isTotal

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 isTotal s

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

rmOrAddPartsMap :: Bool -> OpMap -> OpMap

rmOrAddPartsMap b = MapSet.mapSet (rmOrAddParts b)

diffMapSet :: PredMap -> PredMap -> PredMap

diffMapSet = MapSet.difference

diffOpMapSet :: OpMap -> OpMap -> OpMap

diffOpMapSet m = MapSet.difference m . rmOrAddPartsMap False

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

{ emptySortSet = Set.difference s

$ nonEmptySortSet a `Set.difference` nonEmptySortSet b

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

. Rel.transReduce $ sortRel b

, opMap = opMap a `diffOpMapSet` opMap b

, assocOps = assocOps a `diffOpMapSet` assocOps b

, predMap = predMap a `diffMapSet` predMap b

, annoMap = annoMap a `MapSet.difference` annoMap b

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

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

is not transitive! -}

addOpMapSet :: OpMap -> OpMap -> OpMap

addOpMapSet m = rmOrAddPartsMap True . MapSet.union m

addMapSet :: PredMap -> PredMap -> PredMap

addMapSet = MapSet.union

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

{ 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 = MapSet.union (predMap a) $ predMap b

, annoMap = MapSet.union (annoMap a) $ annoMap b

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

uniteCASLSign :: CASLSign -> CASLSign -> CASLSign

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

interRel :: (Show a, Ord a) => Rel.Rel a -> Rel.Rel a -> Rel.Rel a

interRel a =

Rel.fromSet

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

interOpMapSet :: OpMap -> OpMap -> OpMap

interOpMapSet m = rmOrAddPartsMap True

. MapSet.intersection (rmOrAddPartsMap False m) . rmOrAddPartsMap False

interMapSet :: PredMap -> PredMap -> PredMap

interMapSet = MapSet.intersection

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

{ 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 = MapSet.intersection (annoMap a) $ annoMap b

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

isSubOpMap :: OpMap -> OpMap -> Bool

isSubOpMap m = Map.isSubmapOfBy (\ s t -> MapSet.setAll

(\ e -> Set.member e t || isPartial e && Set.member (mkTotal e) t)

s) (MapSet.toMap m) . MapSet.toMap

isSubMap :: PredMap -> PredMap -> Bool

isSubMap = MapSet.isSubmapOf

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

isSubSig isSubExt a b =

Rel.isSubrelOf (sortRel a) (sortRel b)

-- ignore empty sort sorts

&& isSubOpMap (opMap a) (opMap b)

-- ignore associativity properties!

&& isSubMap (predMap a) (predMap b)

&& isSubExt (extendedInfo a) (extendedInfo b)

mapSetToList :: MapSet.MapSet a b -> [(a, b)]

mapSetToList = MapSet.toPairList

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 = MapSet.update (Set.union v) s $ annoMap e }

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

addSymbol s = do

e <- State.get

State.put $ addSymbToDeclSymbs e s

addSymbToDeclSymbs :: Sign e f -> Symbol -> Sign e f

addSymbToDeclSymbs cs sy =

cs { declaredSymbols = Set.insert sy $ declaredSymbols cs }

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

addSort sk a s = do

e <- State.get

let r = sortRel e

em = emptySortSet e

known = Rel.memberKey s r

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

else do

State.put e { sortRel = Rel.insertKey s r }

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.insertDiffPair super sub)

$ Rel.insertDiffPair 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

addDiags $ if Rel.path sub super r

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

else [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

addDiags $ if Rel.path sub super r

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

else [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]

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

checkWithMap s1 s2 m i = if Map.member i m then alsoWarning s1 s2 i else []

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

checkWithOtherMap s1 s2 = checkWithMap s1 s2 . MapSet.toMap

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 = MapSet.insert

type VarSet = Set.Set (VAR, SORT)

{- | extract the sort and free variables from an analysed term. The input

signature for free variables is (currently only) used for statements in the

VSE logic. The conversion for boolean terms to formulas is only used for FPL.

-}

class TermExtension f where

freeVarsOfExt :: Sign f e -> f -> VarSet

freeVarsOfExt _ = const Set.empty

optTermSort :: f -> Maybe SORT

optTermSort = const Nothing

sortOfTerm :: f -> SORT

sortOfTerm = fromMaybe (genName "unknown") . optTermSort

termToFormula :: TERM f -> Result (FORMULA f)

termToFormula = const $ Result [] Nothing

instance TermExtension ()

instance TermExtension f => TermExtension (TERM f) where

optTermSort = optSortOfTerm optTermSort

optSortOfTerm :: (f -> Maybe SORT) -> TERM f -> Maybe SORT

optSortOfTerm f term = case term of

Qual_var _ ty _ -> Just ty

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

Sorted_term _ ty _ -> Just ty

Cast _ ty _ -> Just ty

Conditional t1 _ _ _ -> optSortOfTerm f t1

ExtTERM t -> f t

_ -> Nothing

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

mkSortGenName :: [SORT] -> String

mkSortGenName sl = "ga_generated_" ++ showSepList (showString "_") showId sl ""

{- | The sort generation constraint is given a generated name,

built from the sort list -}

toSortGenNamed :: FORMULA f -> [SORT] -> Named (FORMULA f)

toSortGenNamed f sl = makeNamed (mkSortGenName sl) f

getConstructors :: [Named (FORMULA f)] -> Set.Set (Id, OpType)

getConstructors = foldr (\ f s -> case sentence f of

Sort_gen_ax cs _ -> let

(_, ops, _) = recover_Sort_gen_ax cs

in foldr ( \ o -> case o of

Qual_op_name i t _ ->

Set.insert (i, mkPartial $ toOpType t)

_ -> id)

s ops

_ -> s) Set.empty

-- | adds a symbol to a given signature

addSymbToSign :: Sign e f -> Symbol -> Result (Sign e f)

addSymbToSign sig sy =

let addSort' cs s =

cs { sortRel = Rel.insertKey s $ sortRel cs }

addToMap' m n t = MapSet.insert n t m

addOp' cs n ot = cs { opMap = addToMap' (opMap cs) n ot }

addPred' cs n pt = cs { predMap = addToMap' (predMap cs) n pt }

in do

let sig' = addSymbToDeclSymbs sig sy

n = symName sy

case symbType sy of

SortAsItemType -> return $ addSort' sig' n

SubsortAsItemType _ -> return sig

PredAsItemType pt -> return $ addPred' sig' n pt

OpAsItemType ot -> return $ addOp' sig' n ot

-- The function below belong in a different file. But I put them here for now.

-- dual of a quantifier

dualQuant :: QUANTIFIER -> QUANTIFIER

dualQuant q = case q of

Universal -> Existential

Existential -> Universal

Unique_existential -> error "unique existential quantifier has no dual" -- should not get here