content: {-# 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
  
  
  