Sublogic.hs

{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./HasCASL/Sublogic.hs
Description :  HasCASL's sublogics
Copyright   :  (c) Sonja Groening, C. Maeder, and Uni Bremen 2002-2006
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  experimental
Portability :  portable

This module provides the sublogic functions (as required by Logic.hs) for
  HasCASL. The functions allow to compute the minimal sublogic needed by a
  given element, to check whether an item is part of a given sublogic, and --
  not yet -- to project an element into a given sublogic.
-}

module HasCASL.Sublogic
    ( -- * datatypes
      Sublogic (..)
    , Formulas (..)
    , Classes (..)
      -- * functions for SemiLatticeWithTop instance
    , topLogic
    , sublogic_max
      -- * combining sublogics restrictions
    , sublogic_min
    , sublogicUp
    , need_hol
      -- * further sublogic constants
    , bottom
    , noSubtypes
    , noClasses
    , totalFuns
    , caslLogic
      -- * functions for Logic instance

      -- ** sublogic to string converstion
    , sublogic_name
      -- ** list of all sublogics
    , sublogics_all
      -- ** checks if element is in given sublogic
    , in_basicSpec
    , in_sentence
    , in_symbItems
    , in_symbMapItems
    , in_env
    , in_morphism
    , in_symbol
      -- * computes the sublogic of a given element
    , sl_basicSpec
    , sl_sentence
    , sl_symbItems
    , sl_symbMapItems
    , sl_env
    , sl_morphism
    , sl_symbol
    ) where

import Data.Data
import qualified Data.Map as Map
import qualified Data.Set as Set

import Common.AS_Annotation
import Common.Id

import HasCASL.As
import HasCASL.AsUtils
import HasCASL.Le as Le
import HasCASL.Builtin
import HasCASL.FoldTerm

-- | formula kinds of HasCASL sublogics
data Formulas
    = Atomic  -- ^ atomic logic
    | Horn    -- ^ positive conditional logic
    | GHorn   -- ^ generalized positive conditional logic
    | FOL     -- ^ first-order logic
    | HOL     -- ^ higher-order logic
      deriving (Show, Eq, Ord, Typeable, Data)

data Classes = NoClasses | SimpleTypeClasses | ConstructorClasses
               deriving (Show, Eq, Ord, Typeable, Data)

-- | HasCASL sublogics
data Sublogic = Sublogic
    { has_sub :: Bool   -- ^ subsorting
    , has_part :: Bool  -- ^ partiality
    , has_eq :: Bool    -- ^ equality
    , has_pred :: Bool  -- ^ predicates
    , type_classes :: Classes
    , has_polymorphism :: Bool
    , has_type_constructors :: Bool
    , has_products :: Bool
    , which_logic :: Formulas
    } deriving (Show, Eq, Ord, Typeable, Data)

-- * special sublogic elements

-- | top element
topLogic :: Sublogic
topLogic = Sublogic
    { has_sub = True
    , has_part = True
    , has_eq = True
    , has_pred = True
    , type_classes = ConstructorClasses
    , has_polymorphism = True
    , has_type_constructors = True
    , has_products = True
    , which_logic = HOL
    }

-- | top sublogic without subtypes
noSubtypes :: Sublogic
noSubtypes = topLogic { has_sub = False }

-- | top sublogic without type classes
noClasses :: Sublogic
noClasses = topLogic { type_classes = NoClasses }

-- | top sublogic without partiality
totalFuns :: Sublogic
totalFuns = topLogic { has_part = False }

caslLogic :: Sublogic
caslLogic = noClasses
    { has_polymorphism = False
    , has_type_constructors = False
    , has_products = False
    , which_logic = FOL
    }

-- | bottom sublogic
bottom :: Sublogic
bottom = Sublogic
    { has_sub = False
    , has_part = False
    , has_eq = False
    , has_pred = False
    , type_classes = NoClasses
    , has_polymorphism = False
    , has_type_constructors = False
    , has_products = False
    , which_logic = Atomic
    }

{- the following are used to add a needed feature to a given
   sublogic via sublogic_max, i.e. (sublogic_max given needs_part)
   will force partiality in addition to what features given already
   has included -}

-- | minimal sublogic with partiality
need_part :: Sublogic
need_part = bottom { has_part = True }

-- | minimal sublogic with equality
need_eq :: Sublogic
need_eq = bottom { has_eq = True }

-- | minimal sublogic with predicates
need_pred :: Sublogic
need_pred = bottom { has_pred = True }

-- | minimal sublogic with subsorting
need_sub :: Sublogic
need_sub = need_pred { has_sub = True }

-- | minimal sublogic with polymorhism
need_polymorphism :: Sublogic
need_polymorphism = bottom { has_polymorphism = True }

-- | minimal sublogic with simple type classes
simpleTypeClasses :: Sublogic
simpleTypeClasses = need_polymorphism { type_classes = SimpleTypeClasses }

-- | minimal sublogic with constructor classes
constructorClasses :: Sublogic
constructorClasses = need_polymorphism { type_classes = ConstructorClasses }

-- | minimal sublogic with type constructors
need_type_constructors :: Sublogic
need_type_constructors = bottom { has_type_constructors = True,
                                  has_products = True }

need_product_type_constructor :: Sublogic
need_product_type_constructor = bottom { has_products = True }

need_horn :: Sublogic
need_horn = bottom { which_logic = Horn }

need_ghorn :: Sublogic
need_ghorn = bottom { which_logic = GHorn }

need_fol :: Sublogic
need_fol = bottom { which_logic = FOL }

need_hol :: Sublogic
need_hol = need_pred { which_logic = HOL }

-- | make sublogic consistent w.r.t. illegal combinations
sublogicUp :: Sublogic -> Sublogic
sublogicUp s' = let s = if has_type_constructors s'
                        then s' { has_products = True } else s'
                in if which_logic s == HOL || has_sub s then
                    s { has_pred = True } else s

-- | generate a list of all sublogics for HasCASL
sublogics_all :: [Sublogic]
sublogics_all = let bools = [False, True] in
    [ Sublogic
    { has_sub = sub
    , has_part = part
    , has_eq = eq
    , has_pred = pre
    , type_classes = tyCl
    , has_polymorphism = poly
    , has_type_constructors = tyCon
    , has_products = prods || tyCon
    , which_logic = logic
    }
    | (tyCl, poly) <- [(NoClasses, False), (NoClasses, True),
                       (SimpleTypeClasses, True), (ConstructorClasses, True)]
    , tyCon <- bools
    , prods <- bools
    , sub <- bools
    , part <- bools
    , eq <- bools
    , pre <- bools
    , logic <- [Atomic, Horn, GHorn, FOL, HOL]
    , pre || logic /= HOL && not sub
    ]

-- | conversion functions to String
formulas_name :: Bool -> Formulas -> String
formulas_name hasPred f = case f of
    HOL -> "HOL"
    FOL -> if hasPred then "FOL" else "FOAlg"
    _ -> case f of
         Atomic -> if hasPred then "Atom" else "Eq"
         _ -> (case f of
                GHorn -> ("G" ++)
                _ -> id) $ if hasPred then "Horn" else "Cond"

-- | the sublogic name as a singleton string list
sublogic_name :: Sublogic -> String
sublogic_name x =
     (if has_sub x then "Sub" else "")
  ++ (if has_part x then "P" else "")
  ++ (case type_classes x of
         NoClasses -> if has_polymorphism x then "Poly" else ""
         SimpleTypeClasses -> "TyCl"
         ConstructorClasses -> "CoCl")
  ++ (if has_type_constructors x then "TyCons" else "")
  ++ (if has_products x then "Prods" else "")
  ++ formulas_name (has_pred x) (which_logic x)
  ++ (if has_eq x then "=" else "")

-- * join functions
sublogic_join :: (Bool -> Bool -> Bool)
               -> (Classes -> Classes -> Classes)
               -> (Formulas -> Formulas -> Formulas)
               -> Sublogic -> Sublogic -> Sublogic
sublogic_join joinB joinC joinF a b = Sublogic
    { has_sub = joinB (has_sub a) $ has_sub b
    , has_part = joinB (has_part a) $ has_part b
    , has_eq = joinB (has_eq a) $ has_eq b
    , has_pred = joinB (has_pred a) $ has_pred b
    , type_classes = joinC (type_classes a) $ type_classes b
    , has_polymorphism = joinB (has_polymorphism a) $ has_polymorphism b
    , has_type_constructors =
        joinB (has_type_constructors a) $ has_type_constructors b
    , has_products = has_products a || has_products b
                     || has_type_constructors a
                     || has_type_constructors b
    , which_logic = joinF (which_logic a) $ which_logic b
    }

sublogic_max :: Sublogic -> Sublogic -> Sublogic
sublogic_max = sublogic_join max max max

sublogic_min :: Sublogic -> Sublogic -> Sublogic
sublogic_min = sublogic_join min min min

-- | compute union sublogic from a list of sublogics
comp_list :: [Sublogic] -> Sublogic
comp_list = foldl sublogic_max bottom

-- Functions to analyse formulae

{- ---------------------------------------------------------------------------
   These functions are based on Till Mossakowski's paper "Sublanguages of
   CASL", which is CoFI Note L-7. The functions implement an adaption of
   the reduced grammar given there for formulae in a specific expression
   logic by, checking whether a formula would match the productions from the
   grammar. Which function checks for which nonterminal from the paper is
   given as a comment before each function.

   They are adapted for HasCASL, especially HasCASLs abstract syntax (As.hs)
--------------------------------------------------------------------------- -}

-- Atomic Logic (subsection 3.4 of the paper)

isPredication :: Term -> Bool
isPredication = foldTerm FoldRec
    { foldQualVar = \ _ _ -> True
    , foldQualOp = \ _ b (PolyId i _ _) t _ _ _ ->
                   b /= Fun && notElem (i, t) bList
    , foldApplTerm = \ _ b1 b2 _ -> b1 && b2
    , foldTupleTerm = \ _ bs _ -> and bs
    , foldTypedTerm = \ _ b q _ _ -> q /= InType && b
    , foldAsPattern = \ _ _ _ _ -> False
    , foldQuantifiedTerm = \ _ _ _ _ _ -> False
    , foldLambdaTerm = \ _ _ _ _ _ -> False
    , foldCaseTerm = \ _ _ _ _ -> False
    , foldLetTerm = \ _ _ _ _ _ -> False
    , foldResolvedMixTerm = \ _ i _ bs _ ->
          notElem i (map fst bList) && and bs
    , foldTermToken = \ _ _ -> True
    , foldMixTypeTerm = \ _ q _ _ -> q /= InType
    , foldMixfixTerm = const and
    , foldBracketTerm = \ _ _ bs _ -> and bs
    , foldProgEq = \ _ _ _ _ -> False
    }

-- FORMULA, P-ATOM
is_atomic_t :: Term -> Bool
is_atomic_t term = case term of
    QuantifiedTerm q _ t _ | is_atomic_q q && is_atomic_t t -> True
      -- P-Conjunction and ExEq
    ApplTerm (QualOp _ (PolyId i _ _) t _ _ _) arg _
      | (case arg of
        TupleTerm ts@[_, _] _ ->
            i == andId && t == logType && all is_atomic_t ts
            || i == exEq && t == eqType
        _ -> False) || i == defId && t == defType
        -> True
    QualOp _ (PolyId i _ _) t _ _ _
        | i == trueId && t == unitTypeScheme -> True
    _ -> isPredication term

-- QUANTIFIER
is_atomic_q :: Quantifier -> Bool
is_atomic_q q = case q of
    Universal -> True
    _ -> False

-- Positive Conditional Logic (subsection 3.2 in the paper)

-- FORMULA
is_horn_t :: Term -> Bool
is_horn_t term = case term of
    QuantifiedTerm q _ f _ -> is_atomic_q q && is_horn_t f
    ApplTerm (QualOp _ (PolyId i _ _) t _ _ _) (TupleTerm [t1, t2] _) _
        | i == implId && t == logType && is_horn_p_conj t1 && is_horn_a t2
          -> True
    _ -> is_atomic_t term

-- P-CONJUNCTION
is_horn_p_conj :: Term -> Bool
is_horn_p_conj term = case term of
    ApplTerm (QualOp _ (PolyId i _ _) t _ _ _) (TupleTerm ts@[_, _] _) _
        | i == andId && t == logType && all is_horn_a ts
          -> True
    _ -> is_atomic_t term

-- ATOM
is_horn_a :: Term -> Bool
is_horn_a term = case term of
    QualOp _ (PolyId i _ _) t _ _ _
        | i == trueId && t == unitTypeScheme -> True
    ApplTerm (QualOp _ (PolyId i _ _) t _ _ _) arg _
      | (case arg of
        TupleTerm [_, _] _ -> isEq i && t == eqType
        _ -> False) || i == defId && t == defType
        -> True
    _ -> is_atomic_t term

-- P-ATOM
is_horn_p_a :: Term -> Bool
is_horn_p_a term = case term of
    QualOp _ (PolyId i _ _) t _ _ _
        | i == trueId && t == unitTypeScheme -> True
    ApplTerm (QualOp _ (PolyId i _ _) t _ _ _) arg _
      | (case arg of
        TupleTerm [_, _] _ -> i == exEq && t == eqType
        _ -> False) || i == defId && t == defType
        -> True
    _ -> is_atomic_t term

-- Generalized Positive Conditional Logic (subsection 3.3 of the paper)

-- FORMULA, ATOM
is_ghorn_t :: Term -> Bool
is_ghorn_t term = case term of
    QuantifiedTerm q _ t _ -> is_atomic_q q && is_ghorn_t t
    ApplTerm (QualOp _ (PolyId i _ _) t _ _ _) arg _
        | (case arg of
          TupleTerm f@[f1, f2] _ ->
              t == logType &&
               (i == andId && (is_ghorn_c_conj f || is_ghorn_f_conj f)
                || i == implId && is_ghorn_prem f1 && is_ghorn_conc f2
                || i == eqvId && is_ghorn_prem f1 && is_ghorn_prem f2)
              || t == eqType && isEq i
          _ -> False) || t == defType && i == defId
          -> True
    _ -> is_atomic_t term

-- C-CONJUNCTION
is_ghorn_c_conj :: [Term] -> Bool
is_ghorn_c_conj = all is_ghorn_conc

-- F-CONJUNCTION
is_ghorn_f_conj :: [Term] -> Bool
is_ghorn_f_conj = all is_ghorn_t

-- P-CONJUNCTION
is_ghorn_p_conj :: [Term] -> Bool
is_ghorn_p_conj = all is_ghorn_prem

-- PREMISE
is_ghorn_prem :: Term -> Bool
is_ghorn_prem term = case term of
    ApplTerm (QualOp _ (PolyId i _ _) t _ _ _) (TupleTerm ts@[_, _] _) _ ->
        i == andId && t == logType && is_ghorn_p_conj ts
    _ -> is_horn_p_a term

-- CONCLUSION
is_ghorn_conc :: Term -> Bool
is_ghorn_conc term = case term of
    ApplTerm (QualOp _ (PolyId i _ _) t _ _ _) (TupleTerm ts@[_, _] _) _ ->
        i == andId && t == logType && is_ghorn_c_conj ts
    _ -> is_horn_a term

is_fol_t :: Term -> Bool
is_fol_t t = case t of
    LambdaTerm {} -> False
    CaseTerm {} -> False
    LetTerm {} -> False
    _ -> True
{- FOL:
  no lambda/let/case,
  no higher types (i.e. all types are basic, tuples, or tuple -> basic)
-}

-- | compute logic of a formula by checking all logics in turn
get_logic :: Term -> Sublogic
get_logic t
  | is_atomic_t t = bottom
  | is_horn_t t = need_horn
  | is_ghorn_t t = need_ghorn
  | is_fol_t t = need_fol
  | otherwise = need_hol

{- Functions to compute minimal sublogic for a given element; these work
by recursing into all subelements -}

sl_basicSpec :: BasicSpec -> Sublogic
sl_basicSpec (BasicSpec l) =
    sublogicUp $ comp_list $ map (sl_basicItem . item) l

sl_basicItem :: BasicItem -> Sublogic
sl_basicItem bIt = case bIt of
    SigItems l -> sl_sigItems l
    ProgItems l _ -> comp_list $ map (sl_progEq . item) l
    ClassItems _ l _ -> comp_list $ map (sl_classItem . item) l
    GenVarItems l _ -> comp_list $ map sl_genVarDecl l
    FreeDatatype l _ -> comp_list $ map (sl_datatypeDecl . item) l
    GenItems l _ -> comp_list $ map (sl_sigItems . item) l
    AxiomItems l m _ ->
        comp_list $ map sl_genVarDecl l ++ map (sl_term . item) m
    Internal l _ -> comp_list $ map (sl_basicItem . item) l

sl_sigItems :: SigItems -> Sublogic
sl_sigItems sIt = case sIt of
    TypeItems i l _ ->
        comp_list $ sl_instance i : map (sl_typeItem . item) l
    OpItems b l _ ->
        comp_list $ sl_opBrand b : map (sl_opItem . item) l

sl_opBrand :: OpBrand -> Sublogic
sl_opBrand o = case o of
    Pred -> need_pred
    _ -> bottom

sl_instance :: Instance -> Sublogic
sl_instance i = case i of
    Instance -> simpleTypeClasses
    _ -> bottom

sl_classItem :: ClassItem -> Sublogic
sl_classItem (ClassItem c l _) =
    comp_list $ sl_classDecl c : map (sl_basicItem . item) l

sl_classDecl :: ClassDecl -> Sublogic
sl_classDecl (ClassDecl _ k _) = case k of
    ClassKind _ -> simpleTypeClasses
    FunKind {} -> constructorClasses

-- don't check the variance or kind of builtin type constructors
sl_Variance :: Variance -> Sublogic
sl_Variance v = case v of
    NonVar -> bottom
    _ -> need_sub

sl_AnyKind :: (a -> Sublogic) -> AnyKind a -> Sublogic
sl_AnyKind f k = case k of
   ClassKind i -> f i
   FunKind v k1 k2 _ ->
       comp_list [sl_Variance v, sl_AnyKind f k1, sl_AnyKind f k2]

sl_Rawkind :: RawKind -> Sublogic
sl_Rawkind = sl_AnyKind (const bottom)

sl_kind :: Kind -> Sublogic
sl_kind = sl_AnyKind $
          \ i -> if i == universeId then bottom else simpleTypeClasses

sl_typeItem :: TypeItem -> Sublogic
sl_typeItem tyIt = case tyIt of
    TypeDecl l k _ -> comp_list $ sl_kind k : map sl_typePattern l
    SubtypeDecl l _ _ -> comp_list $ need_sub : map sl_typePattern l
    IsoDecl l _ -> comp_list $ need_sub : map sl_typePattern l
    SubtypeDefn tp _ t term _ -> comp_list
        [ need_sub
        , sl_typePattern tp
        , sl_type t
        , sl_term $ item term ]
    AliasType tp (Just k) ts _ -> comp_list
        [ sl_kind k
        , sl_typePattern tp
        , sl_typeScheme ts ]
    AliasType tp Nothing ts _ ->
        sublogic_max (sl_typePattern tp) $ sl_typeScheme ts
    Datatype dDecl -> sl_datatypeDecl dDecl

sl_typePattern :: TypePattern -> Sublogic
sl_typePattern tp = case tp of
    TypePattern _ l _ -> comp_list $ map sl_typeArg l
    -- non-empty args --> type constructor!
    MixfixTypePattern l -> comp_list $ map sl_typePattern l
    BracketTypePattern _ l _ -> comp_list $ map sl_typePattern l
    TypePatternArg _ _ -> need_polymorphism
    _ -> bottom

sl_type :: Type -> Sublogic
sl_type = sl_BasicFun

sl_Basictype :: Type -> Sublogic
sl_Basictype ty = case getTypeAppl ty of
 (TypeName tid _ _, _) | isProductId tid -> need_product_type_constructor
 _ -> case ty of
    TypeName _ k v -> sublogic_max
        (if v /= 0 then need_polymorphism else bottom) $ sl_Rawkind k
    KindedType t k _ -> comp_list $ sl_Basictype t : map sl_kind (Set.toList k)
    ExpandedType _ t -> sl_Basictype t
    TypeAbs v t _ -> comp_list
        [ need_type_constructors
        , sl_typeArg v
        , sl_Basictype t ]
    BracketType Parens [t] _ -> sl_Basictype t
    _ -> case getTypeAppl ty of
         (TypeName ide _ _, args) -> comp_list $
            (if isArrow ide || ide == lazyTypeId then need_hol else
                need_type_constructors) : map sl_Basictype args
         (_, []) -> bottom
         (t, args) -> comp_list $ sl_Basictype t : map sl_Basictype args

sl_BasicProd :: Type -> Sublogic
sl_BasicProd ty = case getTypeAppl ty of
    (TypeName ide _ _, tyArgs@(_ : _ : _))
        | isProductIdWithArgs ide $ length tyArgs
        -> comp_list $ map sl_Basictype tyArgs
    _ -> sl_Basictype ty

isAnyUnitType :: Type -> Bool
isAnyUnitType ty = case ty of
  BracketType Parens [] _ -> True
  TypeToken t -> tokStr t == unitTypeS
  _ -> ty == unitType

sl_BasicFun :: Type -> Sublogic
sl_BasicFun ty = case getTypeAppl ty of
    (TypeName ide _ _, [arg, res]) | isArrow ide -> comp_list
        [ if isPartialArrow ide then
              if isAnyUnitType res then need_pred else need_part
          else bottom
        , sl_BasicProd arg
        , sl_Basictype res ]
    _ -> sl_Basictype ty

-- FOL, no higher types, all types are basic, tuples, or tuple -> basic
sl_typeScheme :: TypeScheme -> Sublogic
sl_typeScheme (TypeScheme l t _) = comp_list $ sl_type t : map sl_typeArg l

sl_opItem :: OpItem -> Sublogic
sl_opItem o = case o of
    OpDecl l t m _ -> comp_list $
        sl_typeScheme t : map sl_opId l ++ map sl_opAttr m
    OpDefn i v ts t _ -> comp_list $
        [ sl_opId i
        , sl_typeScheme ts
        , sl_term t
        ] ++ map sl_varDecl (concat v)

sl_partiality :: Partiality -> Sublogic
sl_partiality p = case p of
    Partial -> need_part
    Total -> bottom

sl_opAttr :: OpAttr -> Sublogic
sl_opAttr a = case a of
    UnitOpAttr t _ -> sl_term t
    _ -> need_eq

sl_datatypeDecl :: DatatypeDecl -> Sublogic
sl_datatypeDecl (DatatypeDecl t k l c _) = comp_list $
    [ if null c then bottom else simpleTypeClasses
    , sl_typePattern t
    , sl_kind k ] ++ map (sl_alternative . item) l

sl_alternative :: Alternative -> Sublogic
sl_alternative a = case a of
    Constructor _ l p _ ->
        comp_list $ sl_partiality p : map sl_component (concat l)
    Subtype l _ -> comp_list $ need_sub : map sl_type l

sl_component :: Component -> Sublogic
sl_component s = case s of
    Selector _ p t _ _ -> sublogic_max (sl_partiality p) $ sl_type t
    NoSelector t -> sl_type t

sl_term :: Term -> Sublogic
sl_term t = sublogic_max (get_logic t) $ sl_t t

{- typed in- or as-terms would also indicate subtyping
but we rely on the subtypes in the signature -}
sl_t :: Term -> Sublogic
sl_t trm = case trm of
    QualVar vd -> sl_varDecl vd
    QualOp b i@(PolyId ri _ _) t _ _ _ ->
        if elem ri $ map fst bList then sl_opId i else
        comp_list
        [ sl_opBrand b
        , sl_opId i
        , sl_typeScheme t ]
    ApplTerm t1 t2 _ -> case getAppl trm of
      Just (i, _, arg) | elem i $ map fst bList -> comp_list (map sl_t arg)
      _ -> sublogic_max (sl_t t1) $ sl_t t2
    TupleTerm l _ -> comp_list $ map sl_t l
    TypedTerm t _ ty _ -> sublogic_max (sl_t t) $ sl_type ty
    QuantifiedTerm _ l t _ -> comp_list $ sl_t t : map sl_genVarDecl l
    LambdaTerm l p t _ ->
        comp_list $ sl_partiality p : sl_t t : map sl_t l
    CaseTerm t l _ -> comp_list $ sl_t t : map sl_progEq l ++ map sl_progEq l
    LetTerm _ l t _ -> comp_list $ sl_t t : map sl_progEq l
    MixTypeTerm _ t _ -> sl_type t
    MixfixTerm l -> comp_list $ map sl_t l
    BracketTerm _ l _ -> comp_list $ map sl_t l
    AsPattern vd p2 _ -> sublogic_max (sl_varDecl vd) $ sl_t p2
    _ -> bottom

sl_progEq :: ProgEq -> Sublogic
sl_progEq (ProgEq p t _) = sublogic_max (sl_t p) (sl_t t)

sl_varDecl :: VarDecl -> Sublogic
sl_varDecl (VarDecl _ t _ _) = sl_type t

sl_varKind :: VarKind -> Sublogic
sl_varKind vk = case vk of
   VarKind k -> sl_kind k
   Downset t -> sublogic_max need_sub $ sl_type t
   _ -> bottom

sl_typeArg :: TypeArg -> Sublogic
sl_typeArg (TypeArg _ _ k _ _ _ _) =
    sublogic_max need_polymorphism (sl_varKind k)

sl_genVarDecl :: GenVarDecl -> Sublogic
sl_genVarDecl g = case g of
    GenVarDecl v -> sl_varDecl v
    GenTypeVarDecl v -> sl_typeArg v

isEq :: Id -> Bool
isEq = (`elem` [exEq, eqId])

sl_opId :: PolyId -> Sublogic
sl_opId (PolyId i tys _)
  | isEq i = need_eq
  | elem i [botId, defId, resId] = need_part
  | elem i $ map fst bList = bottom
  | otherwise = comp_list $ map sl_typeArg tys

sl_symbItems :: SymbItems -> Sublogic
sl_symbItems (SymbItems k l _ _) = comp_list $ sl_symbKind k : map sl_symb l

sl_symbMapItems :: SymbMapItems -> Sublogic
sl_symbMapItems (SymbMapItems k l _ _) =
    comp_list $ sl_symbKind k : map sl_symbOrMap l

sl_symbKind :: SymbKind -> Sublogic
sl_symbKind k = case k of
    SyKpred -> need_pred
    SyKclass -> simpleTypeClasses
    _ -> bottom

sl_symb :: Symb -> Sublogic
sl_symb s = case s of
    Symb _ Nothing _ -> bottom
    Symb _ (Just l) _ -> sl_symbType l

sl_symbType :: SymbType -> Sublogic
sl_symbType (SymbType t) = sl_typeScheme t

sl_symbOrMap :: SymbOrMap -> Sublogic
sl_symbOrMap m = case m of
    SymbOrMap s Nothing _ -> sl_symb s
    SymbOrMap s (Just t) _ -> sublogic_max (sl_symb s) $ sl_symb t

{- the maps have no influence since all sorts,ops,preds in them
   must also appear in the signatures, so any features needed by
   them will be included by just checking the signatures -}

sl_env :: Env -> Sublogic
sl_env e = sublogicUp $ comp_list $
    (if Map.null $ classMap e then bottom else simpleTypeClasses)
    : map sl_typeInfo (Map.elems $ typeMap e)
    ++ map sl_opInfos (Map.elems $ assumps e)

sl_typeInfo :: TypeInfo -> Sublogic
sl_typeInfo t =
    sublogic_max (if Set.null $ superTypes t then bottom else need_sub)
    $ sl_typeDefn $ typeDefn t

sl_typeDefn :: TypeDefn -> Sublogic
sl_typeDefn d = case d of
    DatatypeDefn de -> sl_dataEntry de
    AliasTypeDefn t -> sl_type t
    _ -> bottom

sl_dataEntry :: DataEntry -> Sublogic
sl_dataEntry (DataEntry _ _ _ l _ m) =
    comp_list $ map sl_typeArg l ++ map sl_altDefn (Set.toList m)

sl_opInfos :: Set.Set OpInfo -> Sublogic
sl_opInfos = comp_list . map sl_opInfo . Set.toList

sl_opInfo :: OpInfo -> Sublogic
sl_opInfo o = comp_list $ sl_typeScheme (opType o) : sl_opDefn (opDefn o)
              : map sl_opAttr (Set.toList $ opAttrs o)

sl_opDefn :: OpDefn -> Sublogic
sl_opDefn o = case o of
    NoOpDefn b -> sl_opBrand b
    SelectData l _ -> comp_list $ map sl_constrInfo $ Set.toList l
    Definition b t -> sublogic_max (sl_opBrand b) $ sl_term t
    _ -> bottom

sl_constrInfo :: ConstrInfo -> Sublogic
sl_constrInfo = sl_typeScheme . Le.constrType

sl_sentence :: Sentence -> Sublogic
sl_sentence s = sublogicUp $ case s of
    Formula t -> sl_term t
    ProgEqSen _ ts pq -> sublogic_max (sl_typeScheme ts) $ sl_progEq pq
    DatatypeSen l -> comp_list $ map sl_dataEntry l

{- a missing constructor identifier also indicates subtyping
but checking super types is enough for subtype detection -}
sl_altDefn :: AltDefn -> Sublogic
sl_altDefn (Construct _ l p m) = comp_list $ sl_partiality p :
    map sl_type l ++ map sl_selector (concat m)

sl_selector :: Selector -> Sublogic
sl_selector (Select _ t p) = sublogic_max (sl_type t) $ sl_partiality p

sl_morphism :: Morphism -> Sublogic
sl_morphism m = sublogic_max (sl_env $ msource m) $ sl_env $ mtarget m

sl_symbol :: Symbol -> Sublogic
sl_symbol (Symbol _ t) = sl_symbolType t

sl_symbolType :: SymbolType -> Sublogic
sl_symbolType s = case s of
    OpAsItemType t -> sl_typeScheme t
    ClassAsItemType _ -> simpleTypeClasses
    _ -> bottom

-- | check if the second sublogic is contained in the first sublogic
sl_in :: Sublogic -> Sublogic -> Bool
sl_in given new = sublogic_max given new == given

in_x :: Sublogic -> a -> (a -> Sublogic) -> Bool
in_x l x f = sl_in l (f x)

in_basicSpec :: Sublogic -> BasicSpec -> Bool
in_basicSpec l x = in_x l x sl_basicSpec

in_sentence :: Sublogic -> Sentence -> Bool
in_sentence l x = in_x l x sl_sentence

in_symbItems :: Sublogic -> SymbItems -> Bool
in_symbItems l x = in_x l x sl_symbItems

in_symbMapItems :: Sublogic -> SymbMapItems -> Bool
in_symbMapItems l x = in_x l x sl_symbMapItems

in_env :: Sublogic -> Env -> Bool
in_env l x = in_x l x sl_env

in_morphism :: Sublogic -> Morphism -> Bool
in_morphism l x = in_x l x sl_morphism

in_symbol :: Sublogic -> Symbol -> Bool
in_symbol l x = in_x l x sl_symbol