{-# 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 (Int -> Formulas -> ShowS
[Formulas] -> ShowS
Formulas -> String
(Int -> Formulas -> ShowS)
-> (Formulas -> String) -> ([Formulas] -> ShowS) -> Show Formulas
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Formulas] -> ShowS
$cshowList :: [Formulas] -> ShowS
show :: Formulas -> String
$cshow :: Formulas -> String
showsPrec :: Int -> Formulas -> ShowS
$cshowsPrec :: Int -> Formulas -> ShowS
Show, Formulas -> Formulas -> Bool
(Formulas -> Formulas -> Bool)
-> (Formulas -> Formulas -> Bool) -> Eq Formulas
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Formulas -> Formulas -> Bool
$c/= :: Formulas -> Formulas -> Bool
== :: Formulas -> Formulas -> Bool
$c== :: Formulas -> Formulas -> Bool
Eq, Eq Formulas
Eq Formulas =>
(Formulas -> Formulas -> Ordering)
-> (Formulas -> Formulas -> Bool)
-> (Formulas -> Formulas -> Bool)
-> (Formulas -> Formulas -> Bool)
-> (Formulas -> Formulas -> Bool)
-> (Formulas -> Formulas -> Formulas)
-> (Formulas -> Formulas -> Formulas)
-> Ord Formulas
Formulas -> Formulas -> Bool
Formulas -> Formulas -> Ordering
Formulas -> Formulas -> Formulas
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Formulas -> Formulas -> Formulas
$cmin :: Formulas -> Formulas -> Formulas
max :: Formulas -> Formulas -> Formulas
$cmax :: Formulas -> Formulas -> Formulas
>= :: Formulas -> Formulas -> Bool
$c>= :: Formulas -> Formulas -> Bool
> :: Formulas -> Formulas -> Bool
$c> :: Formulas -> Formulas -> Bool
<= :: Formulas -> Formulas -> Bool
$c<= :: Formulas -> Formulas -> Bool
< :: Formulas -> Formulas -> Bool
$c< :: Formulas -> Formulas -> Bool
compare :: Formulas -> Formulas -> Ordering
$ccompare :: Formulas -> Formulas -> Ordering
$cp1Ord :: Eq Formulas
Ord, Typeable, Typeable Formulas
Constr
DataType
Typeable Formulas =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Formulas -> c Formulas)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Formulas)
-> (Formulas -> Constr)
-> (Formulas -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Formulas))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Formulas))
-> ((forall b. Data b => b -> b) -> Formulas -> Formulas)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Formulas -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Formulas -> r)
-> (forall u. (forall d. Data d => d -> u) -> Formulas -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Formulas -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Formulas -> m Formulas)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Formulas -> m Formulas)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Formulas -> m Formulas)
-> Data Formulas
Formulas -> Constr
Formulas -> DataType
(forall b. Data b => b -> b) -> Formulas -> Formulas
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Formulas -> c Formulas
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Formulas
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Formulas -> u
forall u. (forall d. Data d => d -> u) -> Formulas -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Formulas -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Formulas -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Formulas -> m Formulas
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Formulas -> m Formulas
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Formulas
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Formulas -> c Formulas
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Formulas)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Formulas)
$cHOL :: Constr
$cFOL :: Constr
$cGHorn :: Constr
$cHorn :: Constr
$cAtomic :: Constr
$tFormulas :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Formulas -> m Formulas
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Formulas -> m Formulas
gmapMp :: (forall d. Data d => d -> m d) -> Formulas -> m Formulas
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Formulas -> m Formulas
gmapM :: (forall d. Data d => d -> m d) -> Formulas -> m Formulas
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Formulas -> m Formulas
gmapQi :: Int -> (forall d. Data d => d -> u) -> Formulas -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Formulas -> u
gmapQ :: (forall d. Data d => d -> u) -> Formulas -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Formulas -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Formulas -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Formulas -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Formulas -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Formulas -> r
gmapT :: (forall b. Data b => b -> b) -> Formulas -> Formulas
$cgmapT :: (forall b. Data b => b -> b) -> Formulas -> Formulas
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Formulas)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Formulas)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Formulas)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Formulas)
dataTypeOf :: Formulas -> DataType
$cdataTypeOf :: Formulas -> DataType
toConstr :: Formulas -> Constr
$ctoConstr :: Formulas -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Formulas
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Formulas
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Formulas -> c Formulas
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Formulas -> c Formulas
$cp1Data :: Typeable Formulas
Data)

data Classes = NoClasses | SimpleTypeClasses | ConstructorClasses
               deriving (Int -> Classes -> ShowS
[Classes] -> ShowS
Classes -> String
(Int -> Classes -> ShowS)
-> (Classes -> String) -> ([Classes] -> ShowS) -> Show Classes
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Classes] -> ShowS
$cshowList :: [Classes] -> ShowS
show :: Classes -> String
$cshow :: Classes -> String
showsPrec :: Int -> Classes -> ShowS
$cshowsPrec :: Int -> Classes -> ShowS
Show, Classes -> Classes -> Bool
(Classes -> Classes -> Bool)
-> (Classes -> Classes -> Bool) -> Eq Classes
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Classes -> Classes -> Bool
$c/= :: Classes -> Classes -> Bool
== :: Classes -> Classes -> Bool
$c== :: Classes -> Classes -> Bool
Eq, Eq Classes
Eq Classes =>
(Classes -> Classes -> Ordering)
-> (Classes -> Classes -> Bool)
-> (Classes -> Classes -> Bool)
-> (Classes -> Classes -> Bool)
-> (Classes -> Classes -> Bool)
-> (Classes -> Classes -> Classes)
-> (Classes -> Classes -> Classes)
-> Ord Classes
Classes -> Classes -> Bool
Classes -> Classes -> Ordering
Classes -> Classes -> Classes
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Classes -> Classes -> Classes
$cmin :: Classes -> Classes -> Classes
max :: Classes -> Classes -> Classes
$cmax :: Classes -> Classes -> Classes
>= :: Classes -> Classes -> Bool
$c>= :: Classes -> Classes -> Bool
> :: Classes -> Classes -> Bool
$c> :: Classes -> Classes -> Bool
<= :: Classes -> Classes -> Bool
$c<= :: Classes -> Classes -> Bool
< :: Classes -> Classes -> Bool
$c< :: Classes -> Classes -> Bool
compare :: Classes -> Classes -> Ordering
$ccompare :: Classes -> Classes -> Ordering
$cp1Ord :: Eq Classes
Ord, Typeable, Typeable Classes
Constr
DataType
Typeable Classes =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Classes -> c Classes)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Classes)
-> (Classes -> Constr)
-> (Classes -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Classes))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Classes))
-> ((forall b. Data b => b -> b) -> Classes -> Classes)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Classes -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Classes -> r)
-> (forall u. (forall d. Data d => d -> u) -> Classes -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Classes -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Classes -> m Classes)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Classes -> m Classes)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Classes -> m Classes)
-> Data Classes
Classes -> Constr
Classes -> DataType
(forall b. Data b => b -> b) -> Classes -> Classes
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Classes -> c Classes
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Classes
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Classes -> u
forall u. (forall d. Data d => d -> u) -> Classes -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Classes -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Classes -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Classes -> m Classes
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Classes -> m Classes
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Classes
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Classes -> c Classes
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Classes)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Classes)
$cConstructorClasses :: Constr
$cSimpleTypeClasses :: Constr
$cNoClasses :: Constr
$tClasses :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Classes -> m Classes
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Classes -> m Classes
gmapMp :: (forall d. Data d => d -> m d) -> Classes -> m Classes
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Classes -> m Classes
gmapM :: (forall d. Data d => d -> m d) -> Classes -> m Classes
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Classes -> m Classes
gmapQi :: Int -> (forall d. Data d => d -> u) -> Classes -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Classes -> u
gmapQ :: (forall d. Data d => d -> u) -> Classes -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Classes -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Classes -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Classes -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Classes -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Classes -> r
gmapT :: (forall b. Data b => b -> b) -> Classes -> Classes
$cgmapT :: (forall b. Data b => b -> b) -> Classes -> Classes
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Classes)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Classes)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Classes)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Classes)
dataTypeOf :: Classes -> DataType
$cdataTypeOf :: Classes -> DataType
toConstr :: Classes -> Constr
$ctoConstr :: Classes -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Classes
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Classes
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Classes -> c Classes
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Classes -> c Classes
$cp1Data :: Typeable Classes
Data)

-- | HasCASL sublogics
data Sublogic = Sublogic
    { Sublogic -> Bool
has_sub :: Bool   -- ^ subsorting
    , Sublogic -> Bool
has_part :: Bool  -- ^ partiality
    , Sublogic -> Bool
has_eq :: Bool    -- ^ equality
    , Sublogic -> Bool
has_pred :: Bool  -- ^ predicates
    , Sublogic -> Classes
type_classes :: Classes
    , Sublogic -> Bool
has_polymorphism :: Bool
    , Sublogic -> Bool
has_type_constructors :: Bool
    , Sublogic -> Bool
has_products :: Bool
    , Sublogic -> Formulas
which_logic :: Formulas
    } deriving (Int -> Sublogic -> ShowS
[Sublogic] -> ShowS
Sublogic -> String
(Int -> Sublogic -> ShowS)
-> (Sublogic -> String) -> ([Sublogic] -> ShowS) -> Show Sublogic
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Sublogic] -> ShowS
$cshowList :: [Sublogic] -> ShowS
show :: Sublogic -> String
$cshow :: Sublogic -> String
showsPrec :: Int -> Sublogic -> ShowS
$cshowsPrec :: Int -> Sublogic -> ShowS
Show, Sublogic -> Sublogic -> Bool
(Sublogic -> Sublogic -> Bool)
-> (Sublogic -> Sublogic -> Bool) -> Eq Sublogic
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Sublogic -> Sublogic -> Bool
$c/= :: Sublogic -> Sublogic -> Bool
== :: Sublogic -> Sublogic -> Bool
$c== :: Sublogic -> Sublogic -> Bool
Eq, Eq Sublogic
Eq Sublogic =>
(Sublogic -> Sublogic -> Ordering)
-> (Sublogic -> Sublogic -> Bool)
-> (Sublogic -> Sublogic -> Bool)
-> (Sublogic -> Sublogic -> Bool)
-> (Sublogic -> Sublogic -> Bool)
-> (Sublogic -> Sublogic -> Sublogic)
-> (Sublogic -> Sublogic -> Sublogic)
-> Ord Sublogic
Sublogic -> Sublogic -> Bool
Sublogic -> Sublogic -> Ordering
Sublogic -> Sublogic -> Sublogic
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Sublogic -> Sublogic -> Sublogic
$cmin :: Sublogic -> Sublogic -> Sublogic
max :: Sublogic -> Sublogic -> Sublogic
$cmax :: Sublogic -> Sublogic -> Sublogic
>= :: Sublogic -> Sublogic -> Bool
$c>= :: Sublogic -> Sublogic -> Bool
> :: Sublogic -> Sublogic -> Bool
$c> :: Sublogic -> Sublogic -> Bool
<= :: Sublogic -> Sublogic -> Bool
$c<= :: Sublogic -> Sublogic -> Bool
< :: Sublogic -> Sublogic -> Bool
$c< :: Sublogic -> Sublogic -> Bool
compare :: Sublogic -> Sublogic -> Ordering
$ccompare :: Sublogic -> Sublogic -> Ordering
$cp1Ord :: Eq Sublogic
Ord, Typeable, Typeable Sublogic
Constr
DataType
Typeable Sublogic =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Sublogic -> c Sublogic)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Sublogic)
-> (Sublogic -> Constr)
-> (Sublogic -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Sublogic))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sublogic))
-> ((forall b. Data b => b -> b) -> Sublogic -> Sublogic)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Sublogic -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Sublogic -> r)
-> (forall u. (forall d. Data d => d -> u) -> Sublogic -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Sublogic -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Sublogic -> m Sublogic)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Sublogic -> m Sublogic)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Sublogic -> m Sublogic)
-> Data Sublogic
Sublogic -> Constr
Sublogic -> DataType
(forall b. Data b => b -> b) -> Sublogic -> Sublogic
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sublogic -> c Sublogic
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sublogic
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Sublogic -> u
forall u. (forall d. Data d => d -> u) -> Sublogic -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Sublogic -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Sublogic -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Sublogic -> m Sublogic
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Sublogic -> m Sublogic
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sublogic
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sublogic -> c Sublogic
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Sublogic)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sublogic)
$cSublogic :: Constr
$tSublogic :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Sublogic -> m Sublogic
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Sublogic -> m Sublogic
gmapMp :: (forall d. Data d => d -> m d) -> Sublogic -> m Sublogic
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Sublogic -> m Sublogic
gmapM :: (forall d. Data d => d -> m d) -> Sublogic -> m Sublogic
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Sublogic -> m Sublogic
gmapQi :: Int -> (forall d. Data d => d -> u) -> Sublogic -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Sublogic -> u
gmapQ :: (forall d. Data d => d -> u) -> Sublogic -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Sublogic -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Sublogic -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Sublogic -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Sublogic -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Sublogic -> r
gmapT :: (forall b. Data b => b -> b) -> Sublogic -> Sublogic
$cgmapT :: (forall b. Data b => b -> b) -> Sublogic -> Sublogic
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sublogic)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sublogic)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Sublogic)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Sublogic)
dataTypeOf :: Sublogic -> DataType
$cdataTypeOf :: Sublogic -> DataType
toConstr :: Sublogic -> Constr
$ctoConstr :: Sublogic -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sublogic
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sublogic
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sublogic -> c Sublogic
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sublogic -> c Sublogic
$cp1Data :: Typeable Sublogic
Data)

-- * special sublogic elements

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

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

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

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

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

-- | bottom sublogic
bottom :: Sublogic
bottom :: Sublogic
bottom = Sublogic :: Bool
-> Bool
-> Bool
-> Bool
-> Classes
-> Bool
-> Bool
-> Bool
-> Formulas
-> Sublogic
Sublogic
    { has_sub :: Bool
has_sub = Bool
False
    , has_part :: Bool
has_part = Bool
False
    , has_eq :: Bool
has_eq = Bool
False
    , has_pred :: Bool
has_pred = Bool
False
    , type_classes :: Classes
type_classes = Classes
NoClasses
    , has_polymorphism :: Bool
has_polymorphism = Bool
False
    , has_type_constructors :: Bool
has_type_constructors = Bool
False
    , has_products :: Bool
has_products = Bool
False
    , which_logic :: Formulas
which_logic = Formulas
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 :: Sublogic
need_part = Sublogic
bottom { has_part :: Bool
has_part = Bool
True }

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

sublogic_max :: Sublogic -> Sublogic -> Sublogic
sublogic_max :: Sublogic -> Sublogic -> Sublogic
sublogic_max = (Bool -> Bool -> Bool)
-> (Classes -> Classes -> Classes)
-> (Formulas -> Formulas -> Formulas)
-> Sublogic
-> Sublogic
-> Sublogic
sublogic_join Bool -> Bool -> Bool
forall a. Ord a => a -> a -> a
max Classes -> Classes -> Classes
forall a. Ord a => a -> a -> a
max Formulas -> Formulas -> Formulas
forall a. Ord a => a -> a -> a
max

sublogic_min :: Sublogic -> Sublogic -> Sublogic
sublogic_min :: Sublogic -> Sublogic -> Sublogic
sublogic_min = (Bool -> Bool -> Bool)
-> (Classes -> Classes -> Classes)
-> (Formulas -> Formulas -> Formulas)
-> Sublogic
-> Sublogic
-> Sublogic
sublogic_join Bool -> Bool -> Bool
forall a. Ord a => a -> a -> a
min Classes -> Classes -> Classes
forall a. Ord a => a -> a -> a
min Formulas -> Formulas -> Formulas
forall a. Ord a => a -> a -> a
min

-- | compute union sublogic from a list of sublogics
comp_list :: [Sublogic] -> Sublogic
comp_list :: [Sublogic] -> Sublogic
comp_list = (Sublogic -> Sublogic -> Sublogic)
-> Sublogic -> [Sublogic] -> Sublogic
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Sublogic -> Sublogic -> Sublogic
sublogic_max Sublogic
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 :: Term -> Bool
isPredication = FoldRec Bool Bool -> Term -> Bool
forall a b. FoldRec a b -> Term -> a
foldTerm FoldRec :: forall a b.
(Term -> VarDecl -> a)
-> (Term
    -> OpBrand
    -> PolyId
    -> TypeScheme
    -> [Type]
    -> InstKind
    -> Range
    -> a)
-> (Term -> a -> a -> Range -> a)
-> (Term -> [a] -> Range -> a)
-> (Term -> a -> TypeQual -> Type -> Range -> a)
-> (Term -> VarDecl -> a -> Range -> a)
-> (Term -> Quantifier -> [GenVarDecl] -> a -> Range -> a)
-> (Term -> [a] -> Partiality -> a -> Range -> a)
-> (Term -> a -> [b] -> Range -> a)
-> (Term -> LetBrand -> [b] -> a -> Range -> a)
-> (Term -> Id -> [Type] -> [a] -> Range -> a)
-> (Term -> Token -> a)
-> (Term -> TypeQual -> Type -> Range -> a)
-> (Term -> [a] -> a)
-> (Term -> BracketKind -> [a] -> Range -> a)
-> (ProgEq -> a -> a -> Range -> b)
-> FoldRec a b
FoldRec
    { foldQualVar :: Term -> VarDecl -> Bool
foldQualVar = \ _ _ -> Bool
True
    , foldQualOp :: Term
-> OpBrand
-> PolyId
-> TypeScheme
-> [Type]
-> InstKind
-> Range
-> Bool
foldQualOp = \ _ b :: OpBrand
b (PolyId i :: Id
i _ _) t :: TypeScheme
t _ _ _ ->
                   OpBrand
b OpBrand -> OpBrand -> Bool
forall a. Eq a => a -> a -> Bool
/= OpBrand
Fun Bool -> Bool -> Bool
&& (Id, TypeScheme) -> [(Id, TypeScheme)] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem (Id
i, TypeScheme
t) [(Id, TypeScheme)]
bList
    , foldApplTerm :: Term -> Bool -> Bool -> Range -> Bool
foldApplTerm = \ _ b1 :: Bool
b1 b2 :: Bool
b2 _ -> Bool
b1 Bool -> Bool -> Bool
&& Bool
b2
    , foldTupleTerm :: Term -> [Bool] -> Range -> Bool
foldTupleTerm = \ _ bs :: [Bool]
bs _ -> [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
bs
    , foldTypedTerm :: Term -> Bool -> TypeQual -> Type -> Range -> Bool
foldTypedTerm = \ _ b :: Bool
b q :: TypeQual
q _ _ -> TypeQual
q TypeQual -> TypeQual -> Bool
forall a. Eq a => a -> a -> Bool
/= TypeQual
InType Bool -> Bool -> Bool
&& Bool
b
    , foldAsPattern :: Term -> VarDecl -> Bool -> Range -> Bool
foldAsPattern = \ _ _ _ _ -> Bool
False
    , foldQuantifiedTerm :: Term -> Quantifier -> [GenVarDecl] -> Bool -> Range -> Bool
foldQuantifiedTerm = \ _ _ _ _ _ -> Bool
False
    , foldLambdaTerm :: Term -> [Bool] -> Partiality -> Bool -> Range -> Bool
foldLambdaTerm = \ _ _ _ _ _ -> Bool
False
    , foldCaseTerm :: Term -> Bool -> [Bool] -> Range -> Bool
foldCaseTerm = \ _ _ _ _ -> Bool
False
    , foldLetTerm :: Term -> LetBrand -> [Bool] -> Bool -> Range -> Bool
foldLetTerm = \ _ _ _ _ _ -> Bool
False
    , foldResolvedMixTerm :: Term -> Id -> [Type] -> [Bool] -> Range -> Bool
foldResolvedMixTerm = \ _ i :: Id
i _ bs :: [Bool]
bs _ ->
          Id -> [Id] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem Id
i (((Id, TypeScheme) -> Id) -> [(Id, TypeScheme)] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map (Id, TypeScheme) -> Id
forall a b. (a, b) -> a
fst [(Id, TypeScheme)]
bList) Bool -> Bool -> Bool
&& [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
bs
    , foldTermToken :: Term -> Token -> Bool
foldTermToken = \ _ _ -> Bool
True
    , foldMixTypeTerm :: Term -> TypeQual -> Type -> Range -> Bool
foldMixTypeTerm = \ _ q :: TypeQual
q _ _ -> TypeQual
q TypeQual -> TypeQual -> Bool
forall a. Eq a => a -> a -> Bool
/= TypeQual
InType
    , foldMixfixTerm :: Term -> [Bool] -> Bool
foldMixfixTerm = ([Bool] -> Bool) -> Term -> [Bool] -> Bool
forall a b. a -> b -> a
const [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and
    , foldBracketTerm :: Term -> BracketKind -> [Bool] -> Range -> Bool
foldBracketTerm = \ _ _ bs :: [Bool]
bs _ -> [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
bs
    , foldProgEq :: ProgEq -> Bool -> Bool -> Range -> Bool
foldProgEq = \ _ _ _ _ -> Bool
False
    }

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

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

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

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

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

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

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

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

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

-- C-CONJUNCTION
is_ghorn_c_conj :: [Term] -> Bool
is_ghorn_c_conj :: [Term] -> Bool
is_ghorn_c_conj = (Term -> Bool) -> [Term] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Term -> Bool
is_ghorn_conc

-- F-CONJUNCTION
is_ghorn_f_conj :: [Term] -> Bool
is_ghorn_f_conj :: [Term] -> Bool
is_ghorn_f_conj = (Term -> Bool) -> [Term] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Term -> Bool
is_ghorn_t

-- P-CONJUNCTION
is_ghorn_p_conj :: [Term] -> Bool
is_ghorn_p_conj :: [Term] -> Bool
is_ghorn_p_conj = (Term -> Bool) -> [Term] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Term -> Bool
is_ghorn_prem

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

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

is_fol_t :: Term -> Bool
is_fol_t :: Term -> Bool
is_fol_t t :: Term
t = case Term
t of
    LambdaTerm {} -> Bool
False
    CaseTerm {} -> Bool
False
    LetTerm {} -> Bool
False
    _ -> Bool
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 :: Term -> Sublogic
get_logic t :: Term
t
  | Term -> Bool
is_atomic_t Term
t = Sublogic
bottom
  | Term -> Bool
is_horn_t Term
t = Sublogic
need_horn
  | Term -> Bool
is_ghorn_t Term
t = Sublogic
need_ghorn
  | Term -> Bool
is_fol_t Term
t = Sublogic
need_fol
  | Bool
otherwise = Sublogic
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 -> Sublogic
sl_basicSpec (BasicSpec l :: [Annoted BasicItem]
l) =
    Sublogic -> Sublogic
sublogicUp (Sublogic -> Sublogic) -> Sublogic -> Sublogic
forall a b. (a -> b) -> a -> b
$ [Sublogic] -> Sublogic
comp_list ([Sublogic] -> Sublogic) -> [Sublogic] -> Sublogic
forall a b. (a -> b) -> a -> b
$ (Annoted BasicItem -> Sublogic)
-> [Annoted BasicItem] -> [Sublogic]
forall a b. (a -> b) -> [a] -> [b]
map (BasicItem -> Sublogic
sl_basicItem (BasicItem -> Sublogic)
-> (Annoted BasicItem -> BasicItem)
-> Annoted BasicItem
-> Sublogic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted BasicItem -> BasicItem
forall a. Annoted a -> a
item) [Annoted BasicItem]
l

sl_basicItem :: BasicItem -> Sublogic
sl_basicItem :: BasicItem -> Sublogic
sl_basicItem bIt :: BasicItem
bIt = case BasicItem
bIt of
    SigItems l :: SigItems
l -> SigItems -> Sublogic
sl_sigItems SigItems
l
    ProgItems l :: [Annoted ProgEq]
l _ -> [Sublogic] -> Sublogic
comp_list ([Sublogic] -> Sublogic) -> [Sublogic] -> Sublogic
forall a b. (a -> b) -> a -> b
$ (Annoted ProgEq -> Sublogic) -> [Annoted ProgEq] -> [Sublogic]
forall a b. (a -> b) -> [a] -> [b]
map (ProgEq -> Sublogic
sl_progEq (ProgEq -> Sublogic)
-> (Annoted ProgEq -> ProgEq) -> Annoted ProgEq -> Sublogic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted ProgEq -> ProgEq
forall a. Annoted a -> a
item) [Annoted ProgEq]
l
    ClassItems _ l :: [Annoted ClassItem]
l _ -> [Sublogic] -> Sublogic
comp_list ([Sublogic] -> Sublogic) -> [Sublogic] -> Sublogic
forall a b. (a -> b) -> a -> b
$ (Annoted ClassItem -> Sublogic)
-> [Annoted ClassItem] -> [Sublogic]
forall a b. (a -> b) -> [a] -> [b]
map (ClassItem -> Sublogic
sl_classItem (ClassItem -> Sublogic)
-> (Annoted ClassItem -> ClassItem)
-> Annoted ClassItem
-> Sublogic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted ClassItem -> ClassItem
forall a. Annoted a -> a
item) [Annoted ClassItem]
l
    GenVarItems l :: [GenVarDecl]
l _ -> [Sublogic] -> Sublogic
comp_list ([Sublogic] -> Sublogic) -> [Sublogic] -> Sublogic
forall a b. (a -> b) -> a -> b
$ (GenVarDecl -> Sublogic) -> [GenVarDecl] -> [Sublogic]
forall a b. (a -> b) -> [a] -> [b]
map GenVarDecl -> Sublogic
sl_genVarDecl [GenVarDecl]
l
    FreeDatatype l :: [Annoted DatatypeDecl]
l _ -> [Sublogic] -> Sublogic
comp_list ([Sublogic] -> Sublogic) -> [Sublogic] -> Sublogic
forall a b. (a -> b) -> a -> b
$ (Annoted DatatypeDecl -> Sublogic)
-> [Annoted DatatypeDecl] -> [Sublogic]
forall a b. (a -> b) -> [a] -> [b]
map (DatatypeDecl -> Sublogic
sl_datatypeDecl (DatatypeDecl -> Sublogic)
-> (Annoted DatatypeDecl -> DatatypeDecl)
-> Annoted DatatypeDecl
-> Sublogic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted DatatypeDecl -> DatatypeDecl
forall a. Annoted a -> a
item) [Annoted DatatypeDecl]
l
    GenItems l :: [Annoted SigItems]
l _ -> [Sublogic] -> Sublogic
comp_list ([Sublogic] -> Sublogic) -> [Sublogic] -> Sublogic
forall a b. (a -> b) -> a -> b
$ (Annoted SigItems -> Sublogic) -> [Annoted SigItems] -> [Sublogic]
forall a b. (a -> b) -> [a] -> [b]
map (SigItems -> Sublogic
sl_sigItems (SigItems -> Sublogic)
-> (Annoted SigItems -> SigItems) -> Annoted SigItems -> Sublogic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted SigItems -> SigItems
forall a. Annoted a -> a
item) [Annoted SigItems]
l
    AxiomItems l :: [GenVarDecl]
l m :: [Annoted Term]
m _ ->
        [Sublogic] -> Sublogic
comp_list ([Sublogic] -> Sublogic) -> [Sublogic] -> Sublogic
forall a b. (a -> b) -> a -> b
$ (GenVarDecl -> Sublogic) -> [GenVarDecl] -> [Sublogic]
forall a b. (a -> b) -> [a] -> [b]
map GenVarDecl -> Sublogic
sl_genVarDecl [GenVarDecl]
l [Sublogic] -> [Sublogic] -> [Sublogic]
forall a. [a] -> [a] -> [a]
++ (Annoted Term -> Sublogic) -> [Annoted Term] -> [Sublogic]
forall a b. (a -> b) -> [a] -> [b]
map (Term -> Sublogic
sl_term (Term -> Sublogic)
-> (Annoted Term -> Term) -> Annoted Term -> Sublogic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted Term -> Term
forall a. Annoted a -> a
item) [Annoted Term]
m
    Internal l :: [Annoted BasicItem]
l _ -> [Sublogic] -> Sublogic
comp_list ([Sublogic] -> Sublogic) -> [Sublogic] -> Sublogic
forall a b. (a -> b) -> a -> b
$ (Annoted BasicItem -> Sublogic)
-> [Annoted BasicItem] -> [Sublogic]
forall a b. (a -> b) -> [a] -> [b]
map (BasicItem -> Sublogic
sl_basicItem (BasicItem -> Sublogic)
-> (Annoted BasicItem -> BasicItem)
-> Annoted BasicItem
-> Sublogic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted BasicItem -> BasicItem
forall a. Annoted a -> a
item) [Annoted BasicItem]
l

sl_sigItems :: SigItems -> Sublogic
sl_sigItems :: SigItems -> Sublogic
sl_sigItems sIt :: SigItems
sIt = case SigItems
sIt of
    TypeItems i :: Instance
i l :: [Annoted TypeItem]
l _ ->
        [Sublogic] -> Sublogic
comp_list ([Sublogic] -> Sublogic) -> [Sublogic] -> Sublogic
forall a b. (a -> b) -> a -> b
$ Instance -> Sublogic
sl_instance Instance
i Sublogic -> [Sublogic] -> [Sublogic]
forall a. a -> [a] -> [a]
: (Annoted TypeItem -> Sublogic) -> [Annoted TypeItem] -> [Sublogic]
forall a b. (a -> b) -> [a] -> [b]
map (TypeItem -> Sublogic
sl_typeItem (TypeItem -> Sublogic)
-> (Annoted TypeItem -> TypeItem) -> Annoted TypeItem -> Sublogic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted TypeItem -> TypeItem
forall a. Annoted a -> a
item) [Annoted TypeItem]
l
    OpItems b :: OpBrand
b l :: [Annoted OpItem]
l _ ->
        [Sublogic] -> Sublogic
comp_list ([Sublogic] -> Sublogic) -> [Sublogic] -> Sublogic
forall a b. (a -> b) -> a -> b
$ OpBrand -> Sublogic
sl_opBrand OpBrand
b Sublogic -> [Sublogic] -> [Sublogic]
forall a. a -> [a] -> [a]
: (Annoted OpItem -> Sublogic) -> [Annoted OpItem] -> [Sublogic]
forall a b. (a -> b) -> [a] -> [b]
map (OpItem -> Sublogic
sl_opItem (OpItem -> Sublogic)
-> (Annoted OpItem -> OpItem) -> Annoted OpItem -> Sublogic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted OpItem -> OpItem
forall a. Annoted a -> a
item) [Annoted OpItem]
l

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

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

sl_classItem :: ClassItem -> Sublogic
sl_classItem :: ClassItem -> Sublogic
sl_classItem (ClassItem c :: ClassDecl
c l :: [Annoted BasicItem]
l _) =
    [Sublogic] -> Sublogic
comp_list ([Sublogic] -> Sublogic) -> [Sublogic] -> Sublogic
forall a b. (a -> b) -> a -> b
$ ClassDecl -> Sublogic
sl_classDecl ClassDecl
c Sublogic -> [Sublogic] -> [Sublogic]
forall a. a -> [a] -> [a]
: (Annoted BasicItem -> Sublogic)
-> [Annoted BasicItem] -> [Sublogic]
forall a b. (a -> b) -> [a] -> [b]
map (BasicItem -> Sublogic
sl_basicItem (BasicItem -> Sublogic)
-> (Annoted BasicItem -> BasicItem)
-> Annoted BasicItem
-> Sublogic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted BasicItem -> BasicItem
forall a. Annoted a -> a
item) [Annoted BasicItem]
l

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

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

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

sl_Rawkind :: RawKind -> Sublogic
sl_Rawkind :: RawKind -> Sublogic
sl_Rawkind = (() -> Sublogic) -> RawKind -> Sublogic
forall a. (a -> Sublogic) -> AnyKind a -> Sublogic
sl_AnyKind (Sublogic -> () -> Sublogic
forall a b. a -> b -> a
const Sublogic
bottom)

sl_kind :: Kind -> Sublogic
sl_kind :: Kind -> Sublogic
sl_kind = (Id -> Sublogic) -> Kind -> Sublogic
forall a. (a -> Sublogic) -> AnyKind a -> Sublogic
sl_AnyKind ((Id -> Sublogic) -> Kind -> Sublogic)
-> (Id -> Sublogic) -> Kind -> Sublogic
forall a b. (a -> b) -> a -> b
$
          \ i :: Id
i -> if Id
i Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
universeId then Sublogic
bottom else Sublogic
simpleTypeClasses

sl_typeItem :: TypeItem -> Sublogic
sl_typeItem :: TypeItem -> Sublogic
sl_typeItem tyIt :: TypeItem
tyIt = case TypeItem
tyIt of
    TypeDecl l :: [TypePattern]
l k :: Kind
k _ -> [Sublogic] -> Sublogic
comp_list ([Sublogic] -> Sublogic) -> [Sublogic] -> Sublogic
forall a b. (a -> b) -> a -> b
$ Kind -> Sublogic
sl_kind Kind
k Sublogic -> [Sublogic] -> [Sublogic]
forall a. a -> [a] -> [a]
: (TypePattern -> Sublogic) -> [TypePattern] -> [Sublogic]
forall a b. (a -> b) -> [a] -> [b]
map TypePattern -> Sublogic
sl_typePattern [TypePattern]
l
    SubtypeDecl l :: [TypePattern]
l _ _ -> [Sublogic] -> Sublogic
comp_list ([Sublogic] -> Sublogic) -> [Sublogic] -> Sublogic
forall a b. (a -> b) -> a -> b
$ Sublogic
need_sub Sublogic -> [Sublogic] -> [Sublogic]
forall a. a -> [a] -> [a]
: (TypePattern -> Sublogic) -> [TypePattern] -> [Sublogic]
forall a b. (a -> b) -> [a] -> [b]
map TypePattern -> Sublogic
sl_typePattern [TypePattern]
l
    IsoDecl l :: [TypePattern]
l _ -> [Sublogic] -> Sublogic
comp_list ([Sublogic] -> Sublogic) -> [Sublogic] -> Sublogic
forall a b. (a -> b) -> a -> b
$ Sublogic
need_sub Sublogic -> [Sublogic] -> [Sublogic]
forall a. a -> [a] -> [a]
: (TypePattern -> Sublogic) -> [TypePattern] -> [Sublogic]
forall a b. (a -> b) -> [a] -> [b]
map TypePattern -> Sublogic
sl_typePattern [TypePattern]
l
    SubtypeDefn tp :: TypePattern
tp _ t :: Type
t term :: Annoted Term
term _ -> [Sublogic] -> Sublogic
comp_list
        [ Sublogic
need_sub
        , TypePattern -> Sublogic
sl_typePattern TypePattern
tp
        , Type -> Sublogic
sl_type Type
t
        , Term -> Sublogic
sl_term (Term -> Sublogic) -> Term -> Sublogic
forall a b. (a -> b) -> a -> b
$ Annoted Term -> Term
forall a. Annoted a -> a
item Annoted Term
term ]
    AliasType tp :: TypePattern
tp (Just k :: Kind
k) ts :: TypeScheme
ts _ -> [Sublogic] -> Sublogic
comp_list
        [ Kind -> Sublogic
sl_kind Kind
k
        , TypePattern -> Sublogic
sl_typePattern TypePattern
tp
        , TypeScheme -> Sublogic
sl_typeScheme TypeScheme
ts ]
    AliasType tp :: TypePattern
tp Nothing ts :: TypeScheme
ts _ ->
        Sublogic -> Sublogic -> Sublogic
sublogic_max (TypePattern -> Sublogic
sl_typePattern TypePattern
tp) (Sublogic -> Sublogic) -> Sublogic -> Sublogic
forall a b. (a -> b) -> a -> b
$ TypeScheme -> Sublogic
sl_typeScheme TypeScheme
ts
    Datatype dDecl :: DatatypeDecl
dDecl -> DatatypeDecl -> Sublogic
sl_datatypeDecl DatatypeDecl
dDecl

sl_typePattern :: TypePattern -> Sublogic
sl_typePattern :: TypePattern -> Sublogic
sl_typePattern tp :: TypePattern
tp = case TypePattern
tp of
    TypePattern _ l :: [TypeArg]
l _ -> [Sublogic] -> Sublogic
comp_list ([Sublogic] -> Sublogic) -> [Sublogic] -> Sublogic
forall a b. (a -> b) -> a -> b
$ (TypeArg -> Sublogic) -> [TypeArg] -> [Sublogic]
forall a b. (a -> b) -> [a] -> [b]
map TypeArg -> Sublogic
sl_typeArg [TypeArg]
l
    -- non-empty args --> type constructor!
    MixfixTypePattern l :: [TypePattern]
l -> [Sublogic] -> Sublogic
comp_list ([Sublogic] -> Sublogic) -> [Sublogic] -> Sublogic
forall a b. (a -> b) -> a -> b
$ (TypePattern -> Sublogic) -> [TypePattern] -> [Sublogic]
forall a b. (a -> b) -> [a] -> [b]
map TypePattern -> Sublogic
sl_typePattern [TypePattern]
l
    BracketTypePattern _ l :: [TypePattern]
l _ -> [Sublogic] -> Sublogic
comp_list ([Sublogic] -> Sublogic) -> [Sublogic] -> Sublogic
forall a b. (a -> b) -> a -> b
$ (TypePattern -> Sublogic) -> [TypePattern] -> [Sublogic]
forall a b. (a -> b) -> [a] -> [b]
map TypePattern -> Sublogic
sl_typePattern [TypePattern]
l
    TypePatternArg _ _ -> Sublogic
need_polymorphism
    _ -> Sublogic
bottom

sl_type :: Type -> Sublogic
sl_type :: Type -> Sublogic
sl_type = Type -> Sublogic
sl_BasicFun

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

sl_BasicProd :: Type -> Sublogic
sl_BasicProd :: Type -> Sublogic
sl_BasicProd ty :: Type
ty = case Type -> (Type, [Type])
getTypeAppl Type
ty of
    (TypeName ide :: Id
ide _ _, tyArgs :: [Type]
tyArgs@(_ : _ : _))
        | Id -> Int -> Bool
isProductIdWithArgs Id
ide (Int -> Bool) -> Int -> Bool
forall a b. (a -> b) -> a -> b
$ [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
tyArgs
        -> [Sublogic] -> Sublogic
comp_list ([Sublogic] -> Sublogic) -> [Sublogic] -> Sublogic
forall a b. (a -> b) -> a -> b
$ (Type -> Sublogic) -> [Type] -> [Sublogic]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Sublogic
sl_Basictype [Type]
tyArgs
    _ -> Type -> Sublogic
sl_Basictype Type
ty

isAnyUnitType :: Type -> Bool
isAnyUnitType :: Type -> Bool
isAnyUnitType ty :: Type
ty = case Type
ty of
  BracketType Parens [] _ -> Bool
True
  TypeToken t :: Token
t -> Token -> String
tokStr Token
t String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
unitTypeS
  _ -> Type
ty Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
unitType

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

-- FOL, no higher types, all types are basic, tuples, or tuple -> basic
sl_typeScheme :: TypeScheme -> Sublogic
sl_typeScheme :: TypeScheme -> Sublogic
sl_typeScheme (TypeScheme l :: [TypeArg]
l t :: Type
t _) = [Sublogic] -> Sublogic
comp_list ([Sublogic] -> Sublogic) -> [Sublogic] -> Sublogic
forall a b. (a -> b) -> a -> b
$ Type -> Sublogic
sl_type Type
t Sublogic -> [Sublogic] -> [Sublogic]
forall a. a -> [a] -> [a]
: (TypeArg -> Sublogic) -> [TypeArg] -> [Sublogic]
forall a b. (a -> b) -> [a] -> [b]
map TypeArg -> Sublogic
sl_typeArg [TypeArg]
l

sl_opItem :: OpItem -> Sublogic
sl_opItem :: OpItem -> Sublogic
sl_opItem o :: OpItem
o = case OpItem
o of
    OpDecl l :: [PolyId]
l t :: TypeScheme
t m :: [OpAttr]
m _ -> [Sublogic] -> Sublogic
comp_list ([Sublogic] -> Sublogic) -> [Sublogic] -> Sublogic
forall a b. (a -> b) -> a -> b
$
        TypeScheme -> Sublogic
sl_typeScheme TypeScheme
t Sublogic -> [Sublogic] -> [Sublogic]
forall a. a -> [a] -> [a]
: (PolyId -> Sublogic) -> [PolyId] -> [Sublogic]
forall a b. (a -> b) -> [a] -> [b]
map PolyId -> Sublogic
sl_opId [PolyId]
l [Sublogic] -> [Sublogic] -> [Sublogic]
forall a. [a] -> [a] -> [a]
++ (OpAttr -> Sublogic) -> [OpAttr] -> [Sublogic]
forall a b. (a -> b) -> [a] -> [b]
map OpAttr -> Sublogic
sl_opAttr [OpAttr]
m
    OpDefn i :: PolyId
i v :: [[VarDecl]]
v ts :: TypeScheme
ts t :: Term
t _ -> [Sublogic] -> Sublogic
comp_list ([Sublogic] -> Sublogic) -> [Sublogic] -> Sublogic
forall a b. (a -> b) -> a -> b
$
        [ PolyId -> Sublogic
sl_opId PolyId
i
        , TypeScheme -> Sublogic
sl_typeScheme TypeScheme
ts
        , Term -> Sublogic
sl_term Term
t
        ] [Sublogic] -> [Sublogic] -> [Sublogic]
forall a. [a] -> [a] -> [a]
++ (VarDecl -> Sublogic) -> [VarDecl] -> [Sublogic]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl -> Sublogic
sl_varDecl ([[VarDecl]] -> [VarDecl]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[VarDecl]]
v)

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

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

sl_datatypeDecl :: DatatypeDecl -> Sublogic
sl_datatypeDecl :: DatatypeDecl -> Sublogic
sl_datatypeDecl (DatatypeDecl t :: TypePattern
t k :: Kind
k l :: [Annoted Alternative]
l c :: [Id]
c _) = [Sublogic] -> Sublogic
comp_list ([Sublogic] -> Sublogic) -> [Sublogic] -> Sublogic
forall a b. (a -> b) -> a -> b
$
    [ if [Id] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Id]
c then Sublogic
bottom else Sublogic
simpleTypeClasses
    , TypePattern -> Sublogic
sl_typePattern TypePattern
t
    , Kind -> Sublogic
sl_kind Kind
k ] [Sublogic] -> [Sublogic] -> [Sublogic]
forall a. [a] -> [a] -> [a]
++ (Annoted Alternative -> Sublogic)
-> [Annoted Alternative] -> [Sublogic]
forall a b. (a -> b) -> [a] -> [b]
map (Alternative -> Sublogic
sl_alternative (Alternative -> Sublogic)
-> (Annoted Alternative -> Alternative)
-> Annoted Alternative
-> Sublogic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted Alternative -> Alternative
forall a. Annoted a -> a
item) [Annoted Alternative]
l

sl_alternative :: Alternative -> Sublogic
sl_alternative :: Alternative -> Sublogic
sl_alternative a :: Alternative
a = case Alternative
a of
    Constructor _ l :: [[Component]]
l p :: Partiality
p _ ->
        [Sublogic] -> Sublogic
comp_list ([Sublogic] -> Sublogic) -> [Sublogic] -> Sublogic
forall a b. (a -> b) -> a -> b
$ Partiality -> Sublogic
sl_partiality Partiality
p Sublogic -> [Sublogic] -> [Sublogic]
forall a. a -> [a] -> [a]
: (Component -> Sublogic) -> [Component] -> [Sublogic]
forall a b. (a -> b) -> [a] -> [b]
map Component -> Sublogic
sl_component ([[Component]] -> [Component]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Component]]
l)
    Subtype l :: [Type]
l _ -> [Sublogic] -> Sublogic
comp_list ([Sublogic] -> Sublogic) -> [Sublogic] -> Sublogic
forall a b. (a -> b) -> a -> b
$ Sublogic
need_sub Sublogic -> [Sublogic] -> [Sublogic]
forall a. a -> [a] -> [a]
: (Type -> Sublogic) -> [Type] -> [Sublogic]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Sublogic
sl_type [Type]
l

sl_component :: Component -> Sublogic
sl_component :: Component -> Sublogic
sl_component s :: Component
s = case Component
s of
    Selector _ p :: Partiality
p t :: Type
t _ _ -> Sublogic -> Sublogic -> Sublogic
sublogic_max (Partiality -> Sublogic
sl_partiality Partiality
p) (Sublogic -> Sublogic) -> Sublogic -> Sublogic
forall a b. (a -> b) -> a -> b
$ Type -> Sublogic
sl_type Type
t
    NoSelector t :: Type
t -> Type -> Sublogic
sl_type Type
t

sl_term :: Term -> Sublogic
sl_term :: Term -> Sublogic
sl_term t :: Term
t = Sublogic -> Sublogic -> Sublogic
sublogic_max (Term -> Sublogic
get_logic Term
t) (Sublogic -> Sublogic) -> Sublogic -> Sublogic
forall a b. (a -> b) -> a -> b
$ Term -> Sublogic
sl_t Term
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 :: Term -> Sublogic
sl_t trm :: Term
trm = case Term
trm of
    QualVar vd :: VarDecl
vd -> VarDecl -> Sublogic
sl_varDecl VarDecl
vd
    QualOp b :: OpBrand
b i :: PolyId
i@(PolyId ri :: Id
ri _ _) t :: TypeScheme
t _ _ _ ->
        if Id -> [Id] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Id
ri ([Id] -> Bool) -> [Id] -> Bool
forall a b. (a -> b) -> a -> b
$ ((Id, TypeScheme) -> Id) -> [(Id, TypeScheme)] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map (Id, TypeScheme) -> Id
forall a b. (a, b) -> a
fst [(Id, TypeScheme)]
bList then PolyId -> Sublogic
sl_opId PolyId
i else
        [Sublogic] -> Sublogic
comp_list
        [ OpBrand -> Sublogic
sl_opBrand OpBrand
b
        , PolyId -> Sublogic
sl_opId PolyId
i
        , TypeScheme -> Sublogic
sl_typeScheme TypeScheme
t ]
    ApplTerm t1 :: Term
t1 t2 :: Term
t2 _ -> case Term -> Maybe (Id, TypeScheme, [Term])
getAppl Term
trm of
      Just (i :: Id
i, _, arg :: [Term]
arg) | Id -> [Id] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Id
i ([Id] -> Bool) -> [Id] -> Bool
forall a b. (a -> b) -> a -> b
$ ((Id, TypeScheme) -> Id) -> [(Id, TypeScheme)] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map (Id, TypeScheme) -> Id
forall a b. (a, b) -> a
fst [(Id, TypeScheme)]
bList -> [Sublogic] -> Sublogic
comp_list ((Term -> Sublogic) -> [Term] -> [Sublogic]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Sublogic
sl_t [Term]
arg)
      _ -> Sublogic -> Sublogic -> Sublogic
sublogic_max (Term -> Sublogic
sl_t Term
t1) (Sublogic -> Sublogic) -> Sublogic -> Sublogic
forall a b. (a -> b) -> a -> b
$ Term -> Sublogic
sl_t Term
t2
    TupleTerm l :: [Term]
l _ -> [Sublogic] -> Sublogic
comp_list ([Sublogic] -> Sublogic) -> [Sublogic] -> Sublogic
forall a b. (a -> b) -> a -> b
$ (Term -> Sublogic) -> [Term] -> [Sublogic]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Sublogic
sl_t [Term]
l
    TypedTerm t :: Term
t _ ty :: Type
ty _ -> Sublogic -> Sublogic -> Sublogic
sublogic_max (Term -> Sublogic
sl_t Term
t) (Sublogic -> Sublogic) -> Sublogic -> Sublogic
forall a b. (a -> b) -> a -> b
$ Type -> Sublogic
sl_type Type
ty
    QuantifiedTerm _ l :: [GenVarDecl]
l t :: Term
t _ -> [Sublogic] -> Sublogic
comp_list ([Sublogic] -> Sublogic) -> [Sublogic] -> Sublogic
forall a b. (a -> b) -> a -> b
$ Term -> Sublogic
sl_t Term
t Sublogic -> [Sublogic] -> [Sublogic]
forall a. a -> [a] -> [a]
: (GenVarDecl -> Sublogic) -> [GenVarDecl] -> [Sublogic]
forall a b. (a -> b) -> [a] -> [b]
map GenVarDecl -> Sublogic
sl_genVarDecl [GenVarDecl]
l
    LambdaTerm l :: [Term]
l p :: Partiality
p t :: Term
t _ ->
        [Sublogic] -> Sublogic
comp_list ([Sublogic] -> Sublogic) -> [Sublogic] -> Sublogic
forall a b. (a -> b) -> a -> b
$ Partiality -> Sublogic
sl_partiality Partiality
p Sublogic -> [Sublogic] -> [Sublogic]
forall a. a -> [a] -> [a]
: Term -> Sublogic
sl_t Term
t Sublogic -> [Sublogic] -> [Sublogic]
forall a. a -> [a] -> [a]
: (Term -> Sublogic) -> [Term] -> [Sublogic]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Sublogic
sl_t [Term]
l
    CaseTerm t :: Term
t l :: [ProgEq]
l _ -> [Sublogic] -> Sublogic
comp_list ([Sublogic] -> Sublogic) -> [Sublogic] -> Sublogic
forall a b. (a -> b) -> a -> b
$ Term -> Sublogic
sl_t Term
t Sublogic -> [Sublogic] -> [Sublogic]
forall a. a -> [a] -> [a]
: (ProgEq -> Sublogic) -> [ProgEq] -> [Sublogic]
forall a b. (a -> b) -> [a] -> [b]
map ProgEq -> Sublogic
sl_progEq [ProgEq]
l [Sublogic] -> [Sublogic] -> [Sublogic]
forall a. [a] -> [a] -> [a]
++ (ProgEq -> Sublogic) -> [ProgEq] -> [Sublogic]
forall a b. (a -> b) -> [a] -> [b]
map ProgEq -> Sublogic
sl_progEq [ProgEq]
l
    LetTerm _ l :: [ProgEq]
l t :: Term
t _ -> [Sublogic] -> Sublogic
comp_list ([Sublogic] -> Sublogic) -> [Sublogic] -> Sublogic
forall a b. (a -> b) -> a -> b
$ Term -> Sublogic
sl_t Term
t Sublogic -> [Sublogic] -> [Sublogic]
forall a. a -> [a] -> [a]
: (ProgEq -> Sublogic) -> [ProgEq] -> [Sublogic]
forall a b. (a -> b) -> [a] -> [b]
map ProgEq -> Sublogic
sl_progEq [ProgEq]
l
    MixTypeTerm _ t :: Type
t _ -> Type -> Sublogic
sl_type Type
t
    MixfixTerm l :: [Term]
l -> [Sublogic] -> Sublogic
comp_list ([Sublogic] -> Sublogic) -> [Sublogic] -> Sublogic
forall a b. (a -> b) -> a -> b
$ (Term -> Sublogic) -> [Term] -> [Sublogic]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Sublogic
sl_t [Term]
l
    BracketTerm _ l :: [Term]
l _ -> [Sublogic] -> Sublogic
comp_list ([Sublogic] -> Sublogic) -> [Sublogic] -> Sublogic
forall a b. (a -> b) -> a -> b
$ (Term -> Sublogic) -> [Term] -> [Sublogic]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Sublogic
sl_t [Term]
l
    AsPattern vd :: VarDecl
vd p2 :: Term
p2 _ -> Sublogic -> Sublogic -> Sublogic
sublogic_max (VarDecl -> Sublogic
sl_varDecl VarDecl
vd) (Sublogic -> Sublogic) -> Sublogic -> Sublogic
forall a b. (a -> b) -> a -> b
$ Term -> Sublogic
sl_t Term
p2
    _ -> Sublogic
bottom

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

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

sl_varKind :: VarKind -> Sublogic
sl_varKind :: VarKind -> Sublogic
sl_varKind vk :: VarKind
vk = case VarKind
vk of
   VarKind k :: Kind
k -> Kind -> Sublogic
sl_kind Kind
k
   Downset t :: Type
t -> Sublogic -> Sublogic -> Sublogic
sublogic_max Sublogic
need_sub (Sublogic -> Sublogic) -> Sublogic -> Sublogic
forall a b. (a -> b) -> a -> b
$ Type -> Sublogic
sl_type Type
t
   _ -> Sublogic
bottom

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

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

isEq :: Id -> Bool
isEq :: Id -> Bool
isEq = (Id -> [Id] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Id
exEq, Id
eqId])

sl_opId :: PolyId -> Sublogic
sl_opId :: PolyId -> Sublogic
sl_opId (PolyId i :: Id
i tys :: [TypeArg]
tys _)
  | Id -> Bool
isEq Id
i = Sublogic
need_eq
  | Id -> [Id] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Id
i [Id
botId, Id
defId, Id
resId] = Sublogic
need_part
  | Id -> [Id] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Id
i ([Id] -> Bool) -> [Id] -> Bool
forall a b. (a -> b) -> a -> b
$ ((Id, TypeScheme) -> Id) -> [(Id, TypeScheme)] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map (Id, TypeScheme) -> Id
forall a b. (a, b) -> a
fst [(Id, TypeScheme)]
bList = Sublogic
bottom
  | Bool
otherwise = [Sublogic] -> Sublogic
comp_list ([Sublogic] -> Sublogic) -> [Sublogic] -> Sublogic
forall a b. (a -> b) -> a -> b
$ (TypeArg -> Sublogic) -> [TypeArg] -> [Sublogic]
forall a b. (a -> b) -> [a] -> [b]
map TypeArg -> Sublogic
sl_typeArg [TypeArg]
tys

sl_symbItems :: SymbItems -> Sublogic
sl_symbItems :: SymbItems -> Sublogic
sl_symbItems (SymbItems k :: SymbKind
k l :: [Symb]
l _ _) = [Sublogic] -> Sublogic
comp_list ([Sublogic] -> Sublogic) -> [Sublogic] -> Sublogic
forall a b. (a -> b) -> a -> b
$ SymbKind -> Sublogic
sl_symbKind SymbKind
k Sublogic -> [Sublogic] -> [Sublogic]
forall a. a -> [a] -> [a]
: (Symb -> Sublogic) -> [Symb] -> [Sublogic]
forall a b. (a -> b) -> [a] -> [b]
map Symb -> Sublogic
sl_symb [Symb]
l

sl_symbMapItems :: SymbMapItems -> Sublogic
sl_symbMapItems :: SymbMapItems -> Sublogic
sl_symbMapItems (SymbMapItems k :: SymbKind
k l :: [SymbOrMap]
l _ _) =
    [Sublogic] -> Sublogic
comp_list ([Sublogic] -> Sublogic) -> [Sublogic] -> Sublogic
forall a b. (a -> b) -> a -> b
$ SymbKind -> Sublogic
sl_symbKind SymbKind
k Sublogic -> [Sublogic] -> [Sublogic]
forall a. a -> [a] -> [a]
: (SymbOrMap -> Sublogic) -> [SymbOrMap] -> [Sublogic]
forall a b. (a -> b) -> [a] -> [b]
map SymbOrMap -> Sublogic
sl_symbOrMap [SymbOrMap]
l

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

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

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

sl_symbOrMap :: SymbOrMap -> Sublogic
sl_symbOrMap :: SymbOrMap -> Sublogic
sl_symbOrMap m :: SymbOrMap
m = case SymbOrMap
m of
    SymbOrMap s :: Symb
s Nothing _ -> Symb -> Sublogic
sl_symb Symb
s
    SymbOrMap s :: Symb
s (Just t :: Symb
t) _ -> Sublogic -> Sublogic -> Sublogic
sublogic_max (Symb -> Sublogic
sl_symb Symb
s) (Sublogic -> Sublogic) -> Sublogic -> Sublogic
forall a b. (a -> b) -> a -> b
$ Symb -> Sublogic
sl_symb 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 :: Env -> Sublogic
sl_env e :: Env
e = Sublogic -> Sublogic
sublogicUp (Sublogic -> Sublogic) -> Sublogic -> Sublogic
forall a b. (a -> b) -> a -> b
$ [Sublogic] -> Sublogic
comp_list ([Sublogic] -> Sublogic) -> [Sublogic] -> Sublogic
forall a b. (a -> b) -> a -> b
$
    (if Map Id ClassInfo -> Bool
forall k a. Map k a -> Bool
Map.null (Map Id ClassInfo -> Bool) -> Map Id ClassInfo -> Bool
forall a b. (a -> b) -> a -> b
$ Env -> Map Id ClassInfo
classMap Env
e then Sublogic
bottom else Sublogic
simpleTypeClasses)
    Sublogic -> [Sublogic] -> [Sublogic]
forall a. a -> [a] -> [a]
: (TypeInfo -> Sublogic) -> [TypeInfo] -> [Sublogic]
forall a b. (a -> b) -> [a] -> [b]
map TypeInfo -> Sublogic
sl_typeInfo (Map Id TypeInfo -> [TypeInfo]
forall k a. Map k a -> [a]
Map.elems (Map Id TypeInfo -> [TypeInfo]) -> Map Id TypeInfo -> [TypeInfo]
forall a b. (a -> b) -> a -> b
$ Env -> Map Id TypeInfo
typeMap Env
e)
    [Sublogic] -> [Sublogic] -> [Sublogic]
forall a. [a] -> [a] -> [a]
++ (Set OpInfo -> Sublogic) -> [Set OpInfo] -> [Sublogic]
forall a b. (a -> b) -> [a] -> [b]
map Set OpInfo -> Sublogic
sl_opInfos (Map Id (Set OpInfo) -> [Set OpInfo]
forall k a. Map k a -> [a]
Map.elems (Map Id (Set OpInfo) -> [Set OpInfo])
-> Map Id (Set OpInfo) -> [Set OpInfo]
forall a b. (a -> b) -> a -> b
$ Env -> Map Id (Set OpInfo)
assumps Env
e)

sl_typeInfo :: TypeInfo -> Sublogic
sl_typeInfo :: TypeInfo -> Sublogic
sl_typeInfo t :: TypeInfo
t =
    Sublogic -> Sublogic -> Sublogic
sublogic_max (if Set Id -> Bool
forall a. Set a -> Bool
Set.null (Set Id -> Bool) -> Set Id -> Bool
forall a b. (a -> b) -> a -> b
$ TypeInfo -> Set Id
superTypes TypeInfo
t then Sublogic
bottom else Sublogic
need_sub)
    (Sublogic -> Sublogic) -> Sublogic -> Sublogic
forall a b. (a -> b) -> a -> b
$ TypeDefn -> Sublogic
sl_typeDefn (TypeDefn -> Sublogic) -> TypeDefn -> Sublogic
forall a b. (a -> b) -> a -> b
$ TypeInfo -> TypeDefn
typeDefn TypeInfo
t

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

sl_dataEntry :: DataEntry -> Sublogic
sl_dataEntry :: DataEntry -> Sublogic
sl_dataEntry (DataEntry _ _ _ l :: [TypeArg]
l _ m :: Set AltDefn
m) =
    [Sublogic] -> Sublogic
comp_list ([Sublogic] -> Sublogic) -> [Sublogic] -> Sublogic
forall a b. (a -> b) -> a -> b
$ (TypeArg -> Sublogic) -> [TypeArg] -> [Sublogic]
forall a b. (a -> b) -> [a] -> [b]
map TypeArg -> Sublogic
sl_typeArg [TypeArg]
l [Sublogic] -> [Sublogic] -> [Sublogic]
forall a. [a] -> [a] -> [a]
++ (AltDefn -> Sublogic) -> [AltDefn] -> [Sublogic]
forall a b. (a -> b) -> [a] -> [b]
map AltDefn -> Sublogic
sl_altDefn (Set AltDefn -> [AltDefn]
forall a. Set a -> [a]
Set.toList Set AltDefn
m)

sl_opInfos :: Set.Set OpInfo -> Sublogic
sl_opInfos :: Set OpInfo -> Sublogic
sl_opInfos = [Sublogic] -> Sublogic
comp_list ([Sublogic] -> Sublogic)
-> (Set OpInfo -> [Sublogic]) -> Set OpInfo -> Sublogic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (OpInfo -> Sublogic) -> [OpInfo] -> [Sublogic]
forall a b. (a -> b) -> [a] -> [b]
map OpInfo -> Sublogic
sl_opInfo ([OpInfo] -> [Sublogic])
-> (Set OpInfo -> [OpInfo]) -> Set OpInfo -> [Sublogic]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set OpInfo -> [OpInfo]
forall a. Set a -> [a]
Set.toList

sl_opInfo :: OpInfo -> Sublogic
sl_opInfo :: OpInfo -> Sublogic
sl_opInfo o :: OpInfo
o = [Sublogic] -> Sublogic
comp_list ([Sublogic] -> Sublogic) -> [Sublogic] -> Sublogic
forall a b. (a -> b) -> a -> b
$ TypeScheme -> Sublogic
sl_typeScheme (OpInfo -> TypeScheme
opType OpInfo
o) Sublogic -> [Sublogic] -> [Sublogic]
forall a. a -> [a] -> [a]
: OpDefn -> Sublogic
sl_opDefn (OpInfo -> OpDefn
opDefn OpInfo
o)
              Sublogic -> [Sublogic] -> [Sublogic]
forall a. a -> [a] -> [a]
: (OpAttr -> Sublogic) -> [OpAttr] -> [Sublogic]
forall a b. (a -> b) -> [a] -> [b]
map OpAttr -> Sublogic
sl_opAttr (Set OpAttr -> [OpAttr]
forall a. Set a -> [a]
Set.toList (Set OpAttr -> [OpAttr]) -> Set OpAttr -> [OpAttr]
forall a b. (a -> b) -> a -> b
$ OpInfo -> Set OpAttr
opAttrs OpInfo
o)

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

sl_constrInfo :: ConstrInfo -> Sublogic
sl_constrInfo :: ConstrInfo -> Sublogic
sl_constrInfo = TypeScheme -> Sublogic
sl_typeScheme (TypeScheme -> Sublogic)
-> (ConstrInfo -> TypeScheme) -> ConstrInfo -> Sublogic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConstrInfo -> TypeScheme
Le.constrType

sl_sentence :: Sentence -> Sublogic
sl_sentence :: Sentence -> Sublogic
sl_sentence s :: Sentence
s = Sublogic -> Sublogic
sublogicUp (Sublogic -> Sublogic) -> Sublogic -> Sublogic
forall a b. (a -> b) -> a -> b
$ case Sentence
s of
    Formula t :: Term
t -> Term -> Sublogic
sl_term Term
t
    ProgEqSen _ ts :: TypeScheme
ts pq :: ProgEq
pq -> Sublogic -> Sublogic -> Sublogic
sublogic_max (TypeScheme -> Sublogic
sl_typeScheme TypeScheme
ts) (Sublogic -> Sublogic) -> Sublogic -> Sublogic
forall a b. (a -> b) -> a -> b
$ ProgEq -> Sublogic
sl_progEq ProgEq
pq
    DatatypeSen l :: [DataEntry]
l -> [Sublogic] -> Sublogic
comp_list ([Sublogic] -> Sublogic) -> [Sublogic] -> Sublogic
forall a b. (a -> b) -> a -> b
$ (DataEntry -> Sublogic) -> [DataEntry] -> [Sublogic]
forall a b. (a -> b) -> [a] -> [b]
map DataEntry -> Sublogic
sl_dataEntry [DataEntry]
l

{- a missing constructor identifier also indicates subtyping
but checking super types is enough for subtype detection -}
sl_altDefn :: AltDefn -> Sublogic
sl_altDefn :: AltDefn -> Sublogic
sl_altDefn (Construct _ l :: [Type]
l p :: Partiality
p m :: [[Selector]]
m) = [Sublogic] -> Sublogic
comp_list ([Sublogic] -> Sublogic) -> [Sublogic] -> Sublogic
forall a b. (a -> b) -> a -> b
$ Partiality -> Sublogic
sl_partiality Partiality
p Sublogic -> [Sublogic] -> [Sublogic]
forall a. a -> [a] -> [a]
:
    (Type -> Sublogic) -> [Type] -> [Sublogic]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Sublogic
sl_type [Type]
l [Sublogic] -> [Sublogic] -> [Sublogic]
forall a. [a] -> [a] -> [a]
++ (Selector -> Sublogic) -> [Selector] -> [Sublogic]
forall a b. (a -> b) -> [a] -> [b]
map Selector -> Sublogic
sl_selector ([[Selector]] -> [Selector]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Selector]]
m)

sl_selector :: Selector -> Sublogic
sl_selector :: Selector -> Sublogic
sl_selector (Select _ t :: Type
t p :: Partiality
p) = Sublogic -> Sublogic -> Sublogic
sublogic_max (Type -> Sublogic
sl_type Type
t) (Sublogic -> Sublogic) -> Sublogic -> Sublogic
forall a b. (a -> b) -> a -> b
$ Partiality -> Sublogic
sl_partiality Partiality
p

sl_morphism :: Morphism -> Sublogic
sl_morphism :: Morphism -> Sublogic
sl_morphism m :: Morphism
m = Sublogic -> Sublogic -> Sublogic
sublogic_max (Env -> Sublogic
sl_env (Env -> Sublogic) -> Env -> Sublogic
forall a b. (a -> b) -> a -> b
$ Morphism -> Env
msource Morphism
m) (Sublogic -> Sublogic) -> Sublogic -> Sublogic
forall a b. (a -> b) -> a -> b
$ Env -> Sublogic
sl_env (Env -> Sublogic) -> Env -> Sublogic
forall a b. (a -> b) -> a -> b
$ Morphism -> Env
mtarget Morphism
m

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

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

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

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

in_basicSpec :: Sublogic -> BasicSpec -> Bool
in_basicSpec :: Sublogic -> BasicSpec -> Bool
in_basicSpec l :: Sublogic
l x :: BasicSpec
x = Sublogic -> BasicSpec -> (BasicSpec -> Sublogic) -> Bool
forall a. Sublogic -> a -> (a -> Sublogic) -> Bool
in_x Sublogic
l BasicSpec
x BasicSpec -> Sublogic
sl_basicSpec

in_sentence :: Sublogic -> Sentence -> Bool
in_sentence :: Sublogic -> Sentence -> Bool
in_sentence l :: Sublogic
l x :: Sentence
x = Sublogic -> Sentence -> (Sentence -> Sublogic) -> Bool
forall a. Sublogic -> a -> (a -> Sublogic) -> Bool
in_x Sublogic
l Sentence
x Sentence -> Sublogic
sl_sentence

in_symbItems :: Sublogic -> SymbItems -> Bool
in_symbItems :: Sublogic -> SymbItems -> Bool
in_symbItems l :: Sublogic
l x :: SymbItems
x = Sublogic -> SymbItems -> (SymbItems -> Sublogic) -> Bool
forall a. Sublogic -> a -> (a -> Sublogic) -> Bool
in_x Sublogic
l SymbItems
x SymbItems -> Sublogic
sl_symbItems

in_symbMapItems :: Sublogic -> SymbMapItems -> Bool
in_symbMapItems :: Sublogic -> SymbMapItems -> Bool
in_symbMapItems l :: Sublogic
l x :: SymbMapItems
x = Sublogic -> SymbMapItems -> (SymbMapItems -> Sublogic) -> Bool
forall a. Sublogic -> a -> (a -> Sublogic) -> Bool
in_x Sublogic
l SymbMapItems
x SymbMapItems -> Sublogic
sl_symbMapItems

in_env :: Sublogic -> Env -> Bool
in_env :: Sublogic -> Env -> Bool
in_env l :: Sublogic
l x :: Env
x = Sublogic -> Env -> (Env -> Sublogic) -> Bool
forall a. Sublogic -> a -> (a -> Sublogic) -> Bool
in_x Sublogic
l Env
x Env -> Sublogic
sl_env

in_morphism :: Sublogic -> Morphism -> Bool
in_morphism :: Sublogic -> Morphism -> Bool
in_morphism l :: Sublogic
l x :: Morphism
x = Sublogic -> Morphism -> (Morphism -> Sublogic) -> Bool
forall a. Sublogic -> a -> (a -> Sublogic) -> Bool
in_x Sublogic
l Morphism
x Morphism -> Sublogic
sl_morphism

in_symbol :: Sublogic -> Symbol -> Bool
in_symbol :: Sublogic -> Symbol -> Bool
in_symbol l :: Sublogic
l x :: Symbol
x = Sublogic -> Symbol -> (Symbol -> Sublogic) -> Bool
forall a. Sublogic -> a -> (a -> Sublogic) -> Bool
in_x Sublogic
l Symbol
x Symbol -> Sublogic
sl_symbol