Sign.hs revision 4e14c1bc2b97679b84c6ad996fa11c273b74ea02
7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maeder{- |
7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederModule : $Header$
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian MaederDescription : CASL signatures and local environments for basic analysis
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2002-2006
7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
b4fbc96e05117839ca409f5f20f97b3ac872d1edTill Mossakowski
7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederMaintainer : Christian.Maeder@dfki.de
7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederStability : provisional
08faa81d4dd8409cd923b334064f64f802ecc33dChristian MaederPortability : portable
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder
08faa81d4dd8409cd923b334064f64f802ecc33dChristian MaederCASL signatures also serve as local environments for the basic static analysis
08faa81d4dd8409cd923b334064f64f802ecc33dChristian Maeder-}
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder
08faa81d4dd8409cd923b334064f64f802ecc33dChristian Maedermodule CASL.Sign where
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederimport CASL.AS_Basic_CASL
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport CASL.Fold
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport CASL.ToDoc ()
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport qualified Data.Map as Map
f71a8dcf94fd9eb3c9800e16dcdc5e5ff74e5c22Christian Maederimport qualified Data.Set as Set
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport qualified Common.Lib.MapSet as MapSet
7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maederimport qualified Common.Lib.Rel as Rel
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maederimport qualified Common.Lib.State as State
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maederimport Common.Keywords
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport Common.Id
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport Common.Result
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport Common.AS_Annotation
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport Common.GlobalAnnotations
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport Common.Prec (mkPrecIntMap, PrecMap)
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport Common.Doc
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport Common.DocUtils
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport Data.Maybe (fromMaybe)
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport Data.List (isPrefixOf)
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport Control.Monad (when, unless)
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder-- constants have empty argument lists
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maederdata OpType = OpType {opKind :: OpKind, opArgs :: [SORT], opRes :: SORT}
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder deriving (Show, Eq, Ord)
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder-- | result sort added to argument sorts
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian MaederopSorts :: OpType -> [SORT]
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian MaederopSorts o = opRes o : opArgs o
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian MaedermkTotOpType :: [SORT] -> SORT -> OpType
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian MaedermkTotOpType = OpType Total
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian MaedersortToOpType :: SORT -> OpType
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian MaedersortToOpType = mkTotOpType []
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian MaederisSingleArgOp :: OpType -> Bool
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian MaederisSingleArgOp = isSingle . opArgs
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maederdata PredType = PredType {predArgs :: [SORT]} deriving (Show, Eq, Ord)
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian MaedersortToPredType :: SORT -> PredType
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian MaedersortToPredType s = PredType [s]
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian MaederisBinPredType :: PredType -> Bool
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian MaederisBinPredType (PredType l) = case l of
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder [_, _] -> True
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder _ -> False
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maedertype OpMap = MapSet.MapSet OP_NAME OpType
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maedertype PredMap = MapSet.MapSet PRED_NAME PredType
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maedertype AnnoMap = MapSet.MapSet Symbol Annotation
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maederdata SymbType = SortAsItemType
7feac39f792f587cffdc8b63b0e7c5a7d2de292eChristian Maeder | SubsortAsItemType SORT -- special symbols for xml output
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder | OpAsItemType OpType
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder {- since symbols do not speak about totality, the totality
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder information in OpType has to be ignored -}
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder | PredAsItemType PredType
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder deriving (Show, Eq, Ord)
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedersymbolKind :: SymbType -> SYMB_KIND
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedersymbolKind t = case t of
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder OpAsItemType _ -> Ops_kind
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder PredAsItemType _ -> Preds_kind
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder _ -> Sorts_kind
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederdata Symbol = Symbol {symName :: Id, symbType :: SymbType}
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder deriving (Show, Eq, Ord)
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederinstance GetRange Symbol where
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder getRange = getRange . symName
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder rangeSpan = rangeSpan . symName
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederidToSortSymbol :: Id -> Symbol
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederidToSortSymbol idt = Symbol idt SortAsItemType
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederidToOpSymbol :: Id -> OpType -> Symbol
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederidToOpSymbol idt = Symbol idt . OpAsItemType
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederidToPredSymbol :: Id -> PredType -> Symbol
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederidToPredSymbol idt = Symbol idt . PredAsItemType
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederdummy :: Sign f s -> a -> ()
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederdummy _ _ = ()
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederdummyMin :: b -> c -> Result ()
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian MaederdummyMin _ _ = return ()
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maedertype CASLSign = Sign () ()
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder{- | the data type for the basic static analysis to accumulate variables,
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maedersentences, symbols, diagnostics and annotations, that are removed or ignored
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maederwhen looking at signatures from outside, i.e. during logic-independent
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederprocessing. -}
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maederdata Sign f e = Sign
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder { sortRel :: Rel.Rel SORT
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder -- ^ every sort is a subsort of itself
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder , emptySortSet :: Set.Set SORT
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder -- ^ a subset of the sort set of possibly empty sorts
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder , opMap :: OpMap
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder , assocOps :: OpMap -- ^ the subset of associative operators
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder , predMap :: PredMap
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder , varMap :: Map.Map SIMPLE_ID SORT -- ^ temporary variables
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder , sentences :: [Named (FORMULA f)] -- ^ current sentences
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder , declaredSymbols :: Set.Set Symbol -- ^ introduced or redeclared symbols
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder , envDiags :: [Diagnosis] -- ^ diagnostics for basic spec
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder , annoMap :: AnnoMap -- ^ annotated symbols
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder , globAnnos :: GlobalAnnos -- ^ global annotations to use
, extendedInfo :: e
} deriving Show
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
, 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 = 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 -> 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)
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 :: 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
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]
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
-- | 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