{-# LANGUAGE DeriveDataTypeable #-}

{- |

Module : $Header$

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