{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./CASL/Sublogic.hs
Description :  sublogic analysis for CASL
Copyright   :  (c) Pascal Schmidt, C. Maeder, and Uni Bremen 2002-2006
License     :  GPLv2 or higher, see LICENSE.txt

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

Sublogic analysis for CASL

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

module CASL.Sublogic
    ( -- * types
      CASL_Sublogics
    , CASL_SL (..)
    , CASL_Formulas (..)
    , SubsortingFeatures (..)
    , SortGenerationFeatures (..)
    , SortGenTotality (..)
    -- * class
    , Lattice (..)
    -- * predicates on CASL_SL
    , has_sub
    , has_cons
    -- * functions for SemiLatticeWithTop instance
    , mkTop
    , top
    , caslTop
    , cFol
    , fol
    , cPrenex
    , sublogics_max
    , comp_list
    -- * functions for the creation of minimal sublogics
    , bottom
    , mkBot
    , emptyMapConsFeature
    , need_sub
    , need_pred
    , need_horn
    , need_fol
    , updExtFeature
    -- * functions for Logic instance sublogic to string conversion
    , sublogics_name
    , parseSL
    , parseBool
    -- ** list of all sublogics
    , sublogics_all
    , sDims
    -- * computes the sublogic of a given element
    , sl_sig_items
    , sl_basic_spec
    , sl_opkind
    , sl_op_type
    , sl_op_item
    , sl_pred_item
    , sl_sentence
    , sl_term
    , sl_symb_items
    , sl_symb_map_items
    , sl_sign
    , sl_morphism
    , sl_symbol
    -- * projects an element into a given sublogic
    , pr_basic_spec
    , pr_symb_items
    , pr_symb_map_items
    , pr_sign
    , pr_morphism
    , pr_epsilon
    , pr_symbol
    ) where

import Data.Data
import Data.List
import Data.Maybe
import qualified Data.Map as Map
import qualified Data.Set as Set

import qualified Common.Lib.MapSet as MapSet
import qualified Common.Lib.Rel as Rel
import Common.Id
import Common.AS_Annotation
import Common.Lattice

import Control.Monad

import CASL.AS_Basic_CASL
import CASL.Sign
import CASL.Morphism
import CASL.Fold

{- ----------------------------------------------------------------------------
datatypes for CASL sublogics
---------------------------------------------------------------------------- -}

data CASL_Formulas = Atomic  -- ^ atomic logic
                   | Horn    -- ^ positive conditional logic
                   | GHorn   -- ^ generalized positive conditional logic
                   | Prenex  -- ^ formulas in prenex normal form
                   | FOL     -- ^ first-order logic
                   | SOL     -- ^ second-order logic
                   deriving (Int -> CASL_Formulas -> ShowS
[CASL_Formulas] -> ShowS
CASL_Formulas -> String
(Int -> CASL_Formulas -> ShowS)
-> (CASL_Formulas -> String)
-> ([CASL_Formulas] -> ShowS)
-> Show CASL_Formulas
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CASL_Formulas] -> ShowS
$cshowList :: [CASL_Formulas] -> ShowS
show :: CASL_Formulas -> String
$cshow :: CASL_Formulas -> String
showsPrec :: Int -> CASL_Formulas -> ShowS
$cshowsPrec :: Int -> CASL_Formulas -> ShowS
Show, CASL_Formulas -> CASL_Formulas -> Bool
(CASL_Formulas -> CASL_Formulas -> Bool)
-> (CASL_Formulas -> CASL_Formulas -> Bool) -> Eq CASL_Formulas
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CASL_Formulas -> CASL_Formulas -> Bool
$c/= :: CASL_Formulas -> CASL_Formulas -> Bool
== :: CASL_Formulas -> CASL_Formulas -> Bool
$c== :: CASL_Formulas -> CASL_Formulas -> Bool
Eq, Eq CASL_Formulas
Eq CASL_Formulas =>
(CASL_Formulas -> CASL_Formulas -> Ordering)
-> (CASL_Formulas -> CASL_Formulas -> Bool)
-> (CASL_Formulas -> CASL_Formulas -> Bool)
-> (CASL_Formulas -> CASL_Formulas -> Bool)
-> (CASL_Formulas -> CASL_Formulas -> Bool)
-> (CASL_Formulas -> CASL_Formulas -> CASL_Formulas)
-> (CASL_Formulas -> CASL_Formulas -> CASL_Formulas)
-> Ord CASL_Formulas
CASL_Formulas -> CASL_Formulas -> Bool
CASL_Formulas -> CASL_Formulas -> Ordering
CASL_Formulas -> CASL_Formulas -> CASL_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 :: CASL_Formulas -> CASL_Formulas -> CASL_Formulas
$cmin :: CASL_Formulas -> CASL_Formulas -> CASL_Formulas
max :: CASL_Formulas -> CASL_Formulas -> CASL_Formulas
$cmax :: CASL_Formulas -> CASL_Formulas -> CASL_Formulas
>= :: CASL_Formulas -> CASL_Formulas -> Bool
$c>= :: CASL_Formulas -> CASL_Formulas -> Bool
> :: CASL_Formulas -> CASL_Formulas -> Bool
$c> :: CASL_Formulas -> CASL_Formulas -> Bool
<= :: CASL_Formulas -> CASL_Formulas -> Bool
$c<= :: CASL_Formulas -> CASL_Formulas -> Bool
< :: CASL_Formulas -> CASL_Formulas -> Bool
$c< :: CASL_Formulas -> CASL_Formulas -> Bool
compare :: CASL_Formulas -> CASL_Formulas -> Ordering
$ccompare :: CASL_Formulas -> CASL_Formulas -> Ordering
$cp1Ord :: Eq CASL_Formulas
Ord, Typeable, Typeable CASL_Formulas
Constr
DataType
Typeable CASL_Formulas =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> CASL_Formulas -> c CASL_Formulas)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c CASL_Formulas)
-> (CASL_Formulas -> Constr)
-> (CASL_Formulas -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c CASL_Formulas))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c CASL_Formulas))
-> ((forall b. Data b => b -> b) -> CASL_Formulas -> CASL_Formulas)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> CASL_Formulas -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> CASL_Formulas -> r)
-> (forall u. (forall d. Data d => d -> u) -> CASL_Formulas -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> CASL_Formulas -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> CASL_Formulas -> m CASL_Formulas)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> CASL_Formulas -> m CASL_Formulas)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> CASL_Formulas -> m CASL_Formulas)
-> Data CASL_Formulas
CASL_Formulas -> Constr
CASL_Formulas -> DataType
(forall b. Data b => b -> b) -> CASL_Formulas -> CASL_Formulas
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CASL_Formulas -> c CASL_Formulas
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CASL_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) -> CASL_Formulas -> u
forall u. (forall d. Data d => d -> u) -> CASL_Formulas -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CASL_Formulas -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CASL_Formulas -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> CASL_Formulas -> m CASL_Formulas
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CASL_Formulas -> m CASL_Formulas
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CASL_Formulas
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CASL_Formulas -> c CASL_Formulas
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c CASL_Formulas)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c CASL_Formulas)
$cSOL :: Constr
$cFOL :: Constr
$cPrenex :: Constr
$cGHorn :: Constr
$cHorn :: Constr
$cAtomic :: Constr
$tCASL_Formulas :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> CASL_Formulas -> m CASL_Formulas
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CASL_Formulas -> m CASL_Formulas
gmapMp :: (forall d. Data d => d -> m d) -> CASL_Formulas -> m CASL_Formulas
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CASL_Formulas -> m CASL_Formulas
gmapM :: (forall d. Data d => d -> m d) -> CASL_Formulas -> m CASL_Formulas
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> CASL_Formulas -> m CASL_Formulas
gmapQi :: Int -> (forall d. Data d => d -> u) -> CASL_Formulas -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> CASL_Formulas -> u
gmapQ :: (forall d. Data d => d -> u) -> CASL_Formulas -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> CASL_Formulas -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CASL_Formulas -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CASL_Formulas -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CASL_Formulas -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CASL_Formulas -> r
gmapT :: (forall b. Data b => b -> b) -> CASL_Formulas -> CASL_Formulas
$cgmapT :: (forall b. Data b => b -> b) -> CASL_Formulas -> CASL_Formulas
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c CASL_Formulas)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c CASL_Formulas)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c CASL_Formulas)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c CASL_Formulas)
dataTypeOf :: CASL_Formulas -> DataType
$cdataTypeOf :: CASL_Formulas -> DataType
toConstr :: CASL_Formulas -> Constr
$ctoConstr :: CASL_Formulas -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CASL_Formulas
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CASL_Formulas
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CASL_Formulas -> c CASL_Formulas
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CASL_Formulas -> c CASL_Formulas
$cp1Data :: Typeable CASL_Formulas
Data)

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

-- sets availability of strongly persistently liberal encoding of partiality
data SortGenTotality = SomePartial -- ^ partial constructors in gen constraints
                    | OnlyTotal -- ^ no partial constructors
                    | OnlyFree -- ^ only free types; no partial cons possible
                    deriving (SortGenTotality -> SortGenTotality -> Bool
(SortGenTotality -> SortGenTotality -> Bool)
-> (SortGenTotality -> SortGenTotality -> Bool)
-> Eq SortGenTotality
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SortGenTotality -> SortGenTotality -> Bool
$c/= :: SortGenTotality -> SortGenTotality -> Bool
== :: SortGenTotality -> SortGenTotality -> Bool
$c== :: SortGenTotality -> SortGenTotality -> Bool
Eq, Eq SortGenTotality
Eq SortGenTotality =>
(SortGenTotality -> SortGenTotality -> Ordering)
-> (SortGenTotality -> SortGenTotality -> Bool)
-> (SortGenTotality -> SortGenTotality -> Bool)
-> (SortGenTotality -> SortGenTotality -> Bool)
-> (SortGenTotality -> SortGenTotality -> Bool)
-> (SortGenTotality -> SortGenTotality -> SortGenTotality)
-> (SortGenTotality -> SortGenTotality -> SortGenTotality)
-> Ord SortGenTotality
SortGenTotality -> SortGenTotality -> Bool
SortGenTotality -> SortGenTotality -> Ordering
SortGenTotality -> SortGenTotality -> SortGenTotality
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 :: SortGenTotality -> SortGenTotality -> SortGenTotality
$cmin :: SortGenTotality -> SortGenTotality -> SortGenTotality
max :: SortGenTotality -> SortGenTotality -> SortGenTotality
$cmax :: SortGenTotality -> SortGenTotality -> SortGenTotality
>= :: SortGenTotality -> SortGenTotality -> Bool
$c>= :: SortGenTotality -> SortGenTotality -> Bool
> :: SortGenTotality -> SortGenTotality -> Bool
$c> :: SortGenTotality -> SortGenTotality -> Bool
<= :: SortGenTotality -> SortGenTotality -> Bool
$c<= :: SortGenTotality -> SortGenTotality -> Bool
< :: SortGenTotality -> SortGenTotality -> Bool
$c< :: SortGenTotality -> SortGenTotality -> Bool
compare :: SortGenTotality -> SortGenTotality -> Ordering
$ccompare :: SortGenTotality -> SortGenTotality -> Ordering
$cp1Ord :: Eq SortGenTotality
Ord, Typeable, Typeable SortGenTotality
Constr
DataType
Typeable SortGenTotality =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> SortGenTotality -> c SortGenTotality)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c SortGenTotality)
-> (SortGenTotality -> Constr)
-> (SortGenTotality -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c SortGenTotality))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c SortGenTotality))
-> ((forall b. Data b => b -> b)
    -> SortGenTotality -> SortGenTotality)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> SortGenTotality -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> SortGenTotality -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> SortGenTotality -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> SortGenTotality -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> SortGenTotality -> m SortGenTotality)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> SortGenTotality -> m SortGenTotality)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> SortGenTotality -> m SortGenTotality)
-> Data SortGenTotality
SortGenTotality -> Constr
SortGenTotality -> DataType
(forall b. Data b => b -> b) -> SortGenTotality -> SortGenTotality
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SortGenTotality -> c SortGenTotality
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SortGenTotality
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) -> SortGenTotality -> u
forall u. (forall d. Data d => d -> u) -> SortGenTotality -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SortGenTotality -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SortGenTotality -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> SortGenTotality -> m SortGenTotality
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> SortGenTotality -> m SortGenTotality
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SortGenTotality
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SortGenTotality -> c SortGenTotality
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SortGenTotality)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SortGenTotality)
$cOnlyFree :: Constr
$cOnlyTotal :: Constr
$cSomePartial :: Constr
$tSortGenTotality :: DataType
gmapMo :: (forall d. Data d => d -> m d)
-> SortGenTotality -> m SortGenTotality
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> SortGenTotality -> m SortGenTotality
gmapMp :: (forall d. Data d => d -> m d)
-> SortGenTotality -> m SortGenTotality
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> SortGenTotality -> m SortGenTotality
gmapM :: (forall d. Data d => d -> m d)
-> SortGenTotality -> m SortGenTotality
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> SortGenTotality -> m SortGenTotality
gmapQi :: Int -> (forall d. Data d => d -> u) -> SortGenTotality -> u
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> SortGenTotality -> u
gmapQ :: (forall d. Data d => d -> u) -> SortGenTotality -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> SortGenTotality -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SortGenTotality -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SortGenTotality -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SortGenTotality -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SortGenTotality -> r
gmapT :: (forall b. Data b => b -> b) -> SortGenTotality -> SortGenTotality
$cgmapT :: (forall b. Data b => b -> b) -> SortGenTotality -> SortGenTotality
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SortGenTotality)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SortGenTotality)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c SortGenTotality)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SortGenTotality)
dataTypeOf :: SortGenTotality -> DataType
$cdataTypeOf :: SortGenTotality -> DataType
toConstr :: SortGenTotality -> Constr
$ctoConstr :: SortGenTotality -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SortGenTotality
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SortGenTotality
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SortGenTotality -> c SortGenTotality
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SortGenTotality -> c SortGenTotality
$cp1Data :: Typeable SortGenTotality
Data)

instance Show SortGenTotality where
  show :: SortGenTotality -> String
show SomePartial = ""
  show OnlyTotal = "t"
  show OnlyFree = "f"

data SortGenerationFeatures =
          NoSortGen
        | SortGen { SortGenerationFeatures -> Bool
emptyMapping :: Bool
                    -- ^ Mapping of indexed sorts is empty
                  , SortGenerationFeatures -> Bool
onlyInjConstrs :: Bool
                    -- ^ only constructors that are subsort injections
                  , SortGenerationFeatures -> SortGenTotality
totality :: SortGenTotality
                    -- ^ how total constructors are
                  } deriving (Int -> SortGenerationFeatures -> ShowS
[SortGenerationFeatures] -> ShowS
SortGenerationFeatures -> String
(Int -> SortGenerationFeatures -> ShowS)
-> (SortGenerationFeatures -> String)
-> ([SortGenerationFeatures] -> ShowS)
-> Show SortGenerationFeatures
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SortGenerationFeatures] -> ShowS
$cshowList :: [SortGenerationFeatures] -> ShowS
show :: SortGenerationFeatures -> String
$cshow :: SortGenerationFeatures -> String
showsPrec :: Int -> SortGenerationFeatures -> ShowS
$cshowsPrec :: Int -> SortGenerationFeatures -> ShowS
Show, SortGenerationFeatures -> SortGenerationFeatures -> Bool
(SortGenerationFeatures -> SortGenerationFeatures -> Bool)
-> (SortGenerationFeatures -> SortGenerationFeatures -> Bool)
-> Eq SortGenerationFeatures
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SortGenerationFeatures -> SortGenerationFeatures -> Bool
$c/= :: SortGenerationFeatures -> SortGenerationFeatures -> Bool
== :: SortGenerationFeatures -> SortGenerationFeatures -> Bool
$c== :: SortGenerationFeatures -> SortGenerationFeatures -> Bool
Eq, Eq SortGenerationFeatures
Eq SortGenerationFeatures =>
(SortGenerationFeatures -> SortGenerationFeatures -> Ordering)
-> (SortGenerationFeatures -> SortGenerationFeatures -> Bool)
-> (SortGenerationFeatures -> SortGenerationFeatures -> Bool)
-> (SortGenerationFeatures -> SortGenerationFeatures -> Bool)
-> (SortGenerationFeatures -> SortGenerationFeatures -> Bool)
-> (SortGenerationFeatures
    -> SortGenerationFeatures -> SortGenerationFeatures)
-> (SortGenerationFeatures
    -> SortGenerationFeatures -> SortGenerationFeatures)
-> Ord SortGenerationFeatures
SortGenerationFeatures -> SortGenerationFeatures -> Bool
SortGenerationFeatures -> SortGenerationFeatures -> Ordering
SortGenerationFeatures
-> SortGenerationFeatures -> SortGenerationFeatures
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 :: SortGenerationFeatures
-> SortGenerationFeatures -> SortGenerationFeatures
$cmin :: SortGenerationFeatures
-> SortGenerationFeatures -> SortGenerationFeatures
max :: SortGenerationFeatures
-> SortGenerationFeatures -> SortGenerationFeatures
$cmax :: SortGenerationFeatures
-> SortGenerationFeatures -> SortGenerationFeatures
>= :: SortGenerationFeatures -> SortGenerationFeatures -> Bool
$c>= :: SortGenerationFeatures -> SortGenerationFeatures -> Bool
> :: SortGenerationFeatures -> SortGenerationFeatures -> Bool
$c> :: SortGenerationFeatures -> SortGenerationFeatures -> Bool
<= :: SortGenerationFeatures -> SortGenerationFeatures -> Bool
$c<= :: SortGenerationFeatures -> SortGenerationFeatures -> Bool
< :: SortGenerationFeatures -> SortGenerationFeatures -> Bool
$c< :: SortGenerationFeatures -> SortGenerationFeatures -> Bool
compare :: SortGenerationFeatures -> SortGenerationFeatures -> Ordering
$ccompare :: SortGenerationFeatures -> SortGenerationFeatures -> Ordering
$cp1Ord :: Eq SortGenerationFeatures
Ord, Typeable, Typeable SortGenerationFeatures
Constr
DataType
Typeable SortGenerationFeatures =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g)
 -> SortGenerationFeatures
 -> c SortGenerationFeatures)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c SortGenerationFeatures)
-> (SortGenerationFeatures -> Constr)
-> (SortGenerationFeatures -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c SortGenerationFeatures))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c SortGenerationFeatures))
-> ((forall b. Data b => b -> b)
    -> SortGenerationFeatures -> SortGenerationFeatures)
-> (forall r r'.
    (r -> r' -> r)
    -> r
    -> (forall d. Data d => d -> r')
    -> SortGenerationFeatures
    -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r
    -> (forall d. Data d => d -> r')
    -> SortGenerationFeatures
    -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> SortGenerationFeatures -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> SortGenerationFeatures -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> SortGenerationFeatures -> m SortGenerationFeatures)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> SortGenerationFeatures -> m SortGenerationFeatures)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> SortGenerationFeatures -> m SortGenerationFeatures)
-> Data SortGenerationFeatures
SortGenerationFeatures -> Constr
SortGenerationFeatures -> DataType
(forall b. Data b => b -> b)
-> SortGenerationFeatures -> SortGenerationFeatures
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> SortGenerationFeatures
-> c SortGenerationFeatures
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SortGenerationFeatures
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) -> SortGenerationFeatures -> u
forall u.
(forall d. Data d => d -> u) -> SortGenerationFeatures -> [u]
forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> SortGenerationFeatures
-> r
forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> SortGenerationFeatures
-> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> SortGenerationFeatures -> m SortGenerationFeatures
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> SortGenerationFeatures -> m SortGenerationFeatures
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SortGenerationFeatures
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> SortGenerationFeatures
-> c SortGenerationFeatures
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SortGenerationFeatures)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SortGenerationFeatures)
$cSortGen :: Constr
$cNoSortGen :: Constr
$tSortGenerationFeatures :: DataType
gmapMo :: (forall d. Data d => d -> m d)
-> SortGenerationFeatures -> m SortGenerationFeatures
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> SortGenerationFeatures -> m SortGenerationFeatures
gmapMp :: (forall d. Data d => d -> m d)
-> SortGenerationFeatures -> m SortGenerationFeatures
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> SortGenerationFeatures -> m SortGenerationFeatures
gmapM :: (forall d. Data d => d -> m d)
-> SortGenerationFeatures -> m SortGenerationFeatures
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> SortGenerationFeatures -> m SortGenerationFeatures
gmapQi :: Int -> (forall d. Data d => d -> u) -> SortGenerationFeatures -> u
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> SortGenerationFeatures -> u
gmapQ :: (forall d. Data d => d -> u) -> SortGenerationFeatures -> [u]
$cgmapQ :: forall u.
(forall d. Data d => d -> u) -> SortGenerationFeatures -> [u]
gmapQr :: (r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> SortGenerationFeatures
-> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> SortGenerationFeatures
-> r
gmapQl :: (r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> SortGenerationFeatures
-> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> SortGenerationFeatures
-> r
gmapT :: (forall b. Data b => b -> b)
-> SortGenerationFeatures -> SortGenerationFeatures
$cgmapT :: (forall b. Data b => b -> b)
-> SortGenerationFeatures -> SortGenerationFeatures
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SortGenerationFeatures)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SortGenerationFeatures)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c SortGenerationFeatures)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SortGenerationFeatures)
dataTypeOf :: SortGenerationFeatures -> DataType
$cdataTypeOf :: SortGenerationFeatures -> DataType
toConstr :: SortGenerationFeatures -> Constr
$ctoConstr :: SortGenerationFeatures -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SortGenerationFeatures
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SortGenerationFeatures
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> SortGenerationFeatures
-> c SortGenerationFeatures
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> SortGenerationFeatures
-> c SortGenerationFeatures
$cp1Data :: Typeable SortGenerationFeatures
Data)

joinSortGenFeature :: (Bool -> Bool -> Bool)
                   -> (SortGenTotality -> SortGenTotality -> SortGenTotality)
                   -> SortGenerationFeatures -> SortGenerationFeatures
                   -> SortGenerationFeatures
joinSortGenFeature :: (Bool -> Bool -> Bool)
-> (SortGenTotality -> SortGenTotality -> SortGenTotality)
-> SortGenerationFeatures
-> SortGenerationFeatures
-> SortGenerationFeatures
joinSortGenFeature f :: Bool -> Bool -> Bool
f g :: SortGenTotality -> SortGenTotality -> SortGenTotality
g x :: SortGenerationFeatures
x y :: SortGenerationFeatures
y =
    case SortGenerationFeatures
x of
      NoSortGen -> SortGenerationFeatures
y
      SortGen em_x :: Bool
em_x ojc_x :: Bool
ojc_x tc_x :: SortGenTotality
tc_x -> case SortGenerationFeatures
y of
          NoSortGen -> SortGenerationFeatures
x
          SortGen em_y :: Bool
em_y ojc_y :: Bool
ojc_y tc_y :: SortGenTotality
tc_y ->
            Bool -> Bool -> SortGenTotality -> SortGenerationFeatures
SortGen (Bool -> Bool -> Bool
f Bool
em_x Bool
em_y) (Bool -> Bool -> Bool
f Bool
ojc_x Bool
ojc_y) (SortGenTotality -> SortGenTotality -> SortGenTotality
g SortGenTotality
tc_x SortGenTotality
tc_y)

data CASL_SL a = CASL_SL
    { CASL_SL a -> SubsortingFeatures
sub_features :: SubsortingFeatures, -- ^ subsorting
      CASL_SL a -> Bool
has_part :: Bool,  -- ^ partiality
      CASL_SL a -> SortGenerationFeatures
cons_features :: SortGenerationFeatures, -- ^ sort generation constraints
      CASL_SL a -> Bool
has_eq :: Bool,    -- ^ equality
      CASL_SL a -> Bool
has_pred :: Bool,  -- ^ predicates
      CASL_SL a -> CASL_Formulas
which_logic :: CASL_Formulas, -- ^ first order sublogics
      CASL_SL a -> Bool
has_empty_sorts :: Bool, -- ^ may sorts be empty
      CASL_SL a -> a
ext_features :: a  -- ^ features of extension
    } deriving (Int -> CASL_SL a -> ShowS
[CASL_SL a] -> ShowS
CASL_SL a -> String
(Int -> CASL_SL a -> ShowS)
-> (CASL_SL a -> String)
-> ([CASL_SL a] -> ShowS)
-> Show (CASL_SL a)
forall a. Show a => Int -> CASL_SL a -> ShowS
forall a. Show a => [CASL_SL a] -> ShowS
forall a. Show a => CASL_SL a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CASL_SL a] -> ShowS
$cshowList :: forall a. Show a => [CASL_SL a] -> ShowS
show :: CASL_SL a -> String
$cshow :: forall a. Show a => CASL_SL a -> String
showsPrec :: Int -> CASL_SL a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> CASL_SL a -> ShowS
Show, CASL_SL a -> CASL_SL a -> Bool
(CASL_SL a -> CASL_SL a -> Bool)
-> (CASL_SL a -> CASL_SL a -> Bool) -> Eq (CASL_SL a)
forall a. Eq a => CASL_SL a -> CASL_SL a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CASL_SL a -> CASL_SL a -> Bool
$c/= :: forall a. Eq a => CASL_SL a -> CASL_SL a -> Bool
== :: CASL_SL a -> CASL_SL a -> Bool
$c== :: forall a. Eq a => CASL_SL a -> CASL_SL a -> Bool
Eq, Eq (CASL_SL a)
Eq (CASL_SL a) =>
(CASL_SL a -> CASL_SL a -> Ordering)
-> (CASL_SL a -> CASL_SL a -> Bool)
-> (CASL_SL a -> CASL_SL a -> Bool)
-> (CASL_SL a -> CASL_SL a -> Bool)
-> (CASL_SL a -> CASL_SL a -> Bool)
-> (CASL_SL a -> CASL_SL a -> CASL_SL a)
-> (CASL_SL a -> CASL_SL a -> CASL_SL a)
-> Ord (CASL_SL a)
CASL_SL a -> CASL_SL a -> Bool
CASL_SL a -> CASL_SL a -> Ordering
CASL_SL a -> CASL_SL a -> CASL_SL a
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
forall a. Ord a => Eq (CASL_SL a)
forall a. Ord a => CASL_SL a -> CASL_SL a -> Bool
forall a. Ord a => CASL_SL a -> CASL_SL a -> Ordering
forall a. Ord a => CASL_SL a -> CASL_SL a -> CASL_SL a
min :: CASL_SL a -> CASL_SL a -> CASL_SL a
$cmin :: forall a. Ord a => CASL_SL a -> CASL_SL a -> CASL_SL a
max :: CASL_SL a -> CASL_SL a -> CASL_SL a
$cmax :: forall a. Ord a => CASL_SL a -> CASL_SL a -> CASL_SL a
>= :: CASL_SL a -> CASL_SL a -> Bool
$c>= :: forall a. Ord a => CASL_SL a -> CASL_SL a -> Bool
> :: CASL_SL a -> CASL_SL a -> Bool
$c> :: forall a. Ord a => CASL_SL a -> CASL_SL a -> Bool
<= :: CASL_SL a -> CASL_SL a -> Bool
$c<= :: forall a. Ord a => CASL_SL a -> CASL_SL a -> Bool
< :: CASL_SL a -> CASL_SL a -> Bool
$c< :: forall a. Ord a => CASL_SL a -> CASL_SL a -> Bool
compare :: CASL_SL a -> CASL_SL a -> Ordering
$ccompare :: forall a. Ord a => CASL_SL a -> CASL_SL a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (CASL_SL a)
Ord, Typeable, Typeable (CASL_SL a)
Constr
DataType
Typeable (CASL_SL a) =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> CASL_SL a -> c (CASL_SL a))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (CASL_SL a))
-> (CASL_SL a -> Constr)
-> (CASL_SL a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (CASL_SL a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (CASL_SL a)))
-> ((forall b. Data b => b -> b) -> CASL_SL a -> CASL_SL a)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> CASL_SL a -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> CASL_SL a -> r)
-> (forall u. (forall d. Data d => d -> u) -> CASL_SL a -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> CASL_SL a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> CASL_SL a -> m (CASL_SL a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> CASL_SL a -> m (CASL_SL a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> CASL_SL a -> m (CASL_SL a))
-> Data (CASL_SL a)
CASL_SL a -> Constr
CASL_SL a -> DataType
(forall d. Data d => c (t d)) -> Maybe (c (CASL_SL a))
(forall b. Data b => b -> b) -> CASL_SL a -> CASL_SL a
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CASL_SL a -> c (CASL_SL a)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (CASL_SL a)
forall a. Data a => Typeable (CASL_SL a)
forall a. Data a => CASL_SL a -> Constr
forall a. Data a => CASL_SL a -> DataType
forall a.
Data a =>
(forall b. Data b => b -> b) -> CASL_SL a -> CASL_SL a
forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> CASL_SL a -> u
forall a u.
Data a =>
(forall d. Data d => d -> u) -> CASL_SL a -> [u]
forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CASL_SL a -> r
forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CASL_SL a -> r
forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> CASL_SL a -> m (CASL_SL a)
forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> CASL_SL a -> m (CASL_SL a)
forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (CASL_SL a)
forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CASL_SL a -> c (CASL_SL a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (CASL_SL a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (CASL_SL a))
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) -> CASL_SL a -> u
forall u. (forall d. Data d => d -> u) -> CASL_SL a -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CASL_SL a -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CASL_SL a -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> CASL_SL a -> m (CASL_SL a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CASL_SL a -> m (CASL_SL a)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (CASL_SL a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CASL_SL a -> c (CASL_SL a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (CASL_SL a))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (CASL_SL a))
$cCASL_SL :: Constr
$tCASL_SL :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> CASL_SL a -> m (CASL_SL a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> CASL_SL a -> m (CASL_SL a)
gmapMp :: (forall d. Data d => d -> m d) -> CASL_SL a -> m (CASL_SL a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> CASL_SL a -> m (CASL_SL a)
gmapM :: (forall d. Data d => d -> m d) -> CASL_SL a -> m (CASL_SL a)
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> CASL_SL a -> m (CASL_SL a)
gmapQi :: Int -> (forall d. Data d => d -> u) -> CASL_SL a -> u
$cgmapQi :: forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> CASL_SL a -> u
gmapQ :: (forall d. Data d => d -> u) -> CASL_SL a -> [u]
$cgmapQ :: forall a u.
Data a =>
(forall d. Data d => d -> u) -> CASL_SL a -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CASL_SL a -> r
$cgmapQr :: forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CASL_SL a -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CASL_SL a -> r
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CASL_SL a -> r
gmapT :: (forall b. Data b => b -> b) -> CASL_SL a -> CASL_SL a
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b) -> CASL_SL a -> CASL_SL a
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (CASL_SL a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (CASL_SL a))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (CASL_SL a))
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (CASL_SL a))
dataTypeOf :: CASL_SL a -> DataType
$cdataTypeOf :: forall a. Data a => CASL_SL a -> DataType
toConstr :: CASL_SL a -> Constr
$ctoConstr :: forall a. Data a => CASL_SL a -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (CASL_SL a)
$cgunfold :: forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (CASL_SL a)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CASL_SL a -> c (CASL_SL a)
$cgfoldl :: forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CASL_SL a -> c (CASL_SL a)
$cp1Data :: forall a. Data a => Typeable (CASL_SL a)
Data)

updExtFeature :: (a -> a) -> CASL_SL a -> CASL_SL a
updExtFeature :: (a -> a) -> CASL_SL a -> CASL_SL a
updExtFeature f :: a -> a
f s :: CASL_SL a
s = CASL_SL a
s { ext_features :: a
ext_features = a -> a
f (a -> a) -> a -> a
forall a b. (a -> b) -> a -> b
$ CASL_SL a -> a
forall a. CASL_SL a -> a
ext_features CASL_SL a
s }

type CASL_Sublogics = CASL_SL ()

{- -----------------------
old selector functions
----------------------- -}

has_sub :: CASL_SL a -> Bool
has_sub :: CASL_SL a -> Bool
has_sub sl :: CASL_SL a
sl = case CASL_SL a -> SubsortingFeatures
forall a. CASL_SL a -> SubsortingFeatures
sub_features CASL_SL a
sl of
             NoSub -> Bool
False
             _ -> Bool
True

has_cons :: CASL_SL a -> Bool
has_cons :: CASL_SL a -> Bool
has_cons sl :: CASL_SL a
sl = case CASL_SL a -> SortGenerationFeatures
forall a. CASL_SL a -> SortGenerationFeatures
cons_features CASL_SL a
sl of
              NoSortGen -> Bool
False
              _ -> Bool
True
{- ---------------------------------------------------------------------------
Special sublogics elements
--------------------------------------------------------------------------- -}

-- top element
mkTop :: a -> CASL_SL a
mkTop :: a -> CASL_SL a
mkTop = SubsortingFeatures
-> Bool
-> SortGenerationFeatures
-> Bool
-> Bool
-> CASL_Formulas
-> Bool
-> a
-> CASL_SL a
forall a.
SubsortingFeatures
-> Bool
-> SortGenerationFeatures
-> Bool
-> Bool
-> CASL_Formulas
-> Bool
-> a
-> CASL_SL a
CASL_SL SubsortingFeatures
Sub Bool
True (Bool -> Bool -> SortGenTotality -> SortGenerationFeatures
SortGen Bool
False Bool
False SortGenTotality
SomePartial) Bool
True Bool
True CASL_Formulas
SOL Bool
True

top :: Lattice a => CASL_SL a
top :: CASL_SL a
top = a -> CASL_SL a
forall a. a -> CASL_SL a
mkTop a
forall l. Lattice l => l
ctop

caslTop :: Lattice a => CASL_SL a
caslTop :: CASL_SL a
caslTop = CASL_SL a
forall a. Lattice a => CASL_SL a
top
  { has_empty_sorts :: Bool
has_empty_sorts = Bool
False
  , which_logic :: CASL_Formulas
which_logic = CASL_Formulas
FOL
  }

cFol :: Lattice a => CASL_SL a
cFol :: CASL_SL a
cFol = CASL_SL a
forall a. Lattice a => CASL_SL a
caslTop
  { sub_features :: SubsortingFeatures
sub_features = SubsortingFeatures
NoSub -- no subsorting
  , has_part :: Bool
has_part = Bool
False -- no partiality
  }

fol :: Lattice a => CASL_SL a
fol :: CASL_SL a
fol = CASL_SL a
forall a. Lattice a => CASL_SL a
caslTop
  { sub_features :: SubsortingFeatures
sub_features = SubsortingFeatures
NoSub -- no subsorting
  , has_part :: Bool
has_part = Bool
False -- no partiality
  , cons_features :: SortGenerationFeatures
cons_features = SortGenerationFeatures
NoSortGen -- no sort generation constraints 
  }

cPrenex :: Lattice a => CASL_SL a
cPrenex :: CASL_SL a
cPrenex = CASL_SL a
forall a. Lattice a => CASL_SL a
cFol {which_logic :: CASL_Formulas
which_logic = CASL_Formulas
Prenex}

mkBot :: a -> CASL_SL a
mkBot :: a -> CASL_SL a
mkBot = SubsortingFeatures
-> Bool
-> SortGenerationFeatures
-> Bool
-> Bool
-> CASL_Formulas
-> Bool
-> a
-> CASL_SL a
forall a.
SubsortingFeatures
-> Bool
-> SortGenerationFeatures
-> Bool
-> Bool
-> CASL_Formulas
-> Bool
-> a
-> CASL_SL a
CASL_SL SubsortingFeatures
NoSub Bool
False SortGenerationFeatures
NoSortGen Bool
False Bool
False CASL_Formulas
Atomic Bool
False

-- bottom element
bottom :: Lattice a => CASL_SL a
bottom :: CASL_SL a
bottom = a -> CASL_SL a
forall a. a -> CASL_SL a
mkBot a
forall l. Lattice l => l
bot

need_empty_sorts :: Lattice a => CASL_SL a
need_empty_sorts :: CASL_SL a
need_empty_sorts = CASL_SL a
forall a. Lattice a => CASL_SL a
bottom { has_empty_sorts :: Bool
has_empty_sorts = Bool
True }

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

-- minimal sublogics with subsorting
need_sub :: Lattice a => CASL_SL a
need_sub :: CASL_SL a
need_sub = CASL_SL a
forall a. Lattice a => CASL_SL a
need_horn { sub_features :: SubsortingFeatures
sub_features = SubsortingFeatures
Sub }

need_sul :: Lattice a => CASL_SL a
need_sul :: CASL_SL a
need_sul = CASL_SL a
forall a. Lattice a => CASL_SL a
need_horn { sub_features :: SubsortingFeatures
sub_features = SubsortingFeatures
LocFilSub }

-- minimal sublogic with partiality
need_part :: Lattice a => CASL_SL a
need_part :: CASL_SL a
need_part = CASL_SL a
forall a. Lattice a => CASL_SL a
bottom { has_part :: Bool
has_part = Bool
True }

emptyMapConsFeature :: SortGenerationFeatures
emptyMapConsFeature :: SortGenerationFeatures
emptyMapConsFeature = SortGen :: Bool -> Bool -> SortGenTotality -> SortGenerationFeatures
SortGen
  { emptyMapping :: Bool
emptyMapping = Bool
True
  , onlyInjConstrs :: Bool
onlyInjConstrs = Bool
False
  , totality :: SortGenTotality
totality = SortGenTotality
SomePartial}

-- minimal sublogics with sort generation constraints
need_cons :: Lattice a => Bool -> Bool -> SortGenTotality -> CASL_SL a
need_cons :: Bool -> Bool -> SortGenTotality -> CASL_SL a
need_cons em :: Bool
em ojc :: Bool
ojc tc :: SortGenTotality
tc = CASL_SL a
forall a. Lattice a => CASL_SL a
bottom
    { cons_features :: SortGenerationFeatures
cons_features = Bool -> Bool -> SortGenTotality -> SortGenerationFeatures
SortGen Bool
em Bool
ojc SortGenTotality
tc }

-- minimal sublogic with equality
need_eq :: Lattice a => CASL_SL a
need_eq :: CASL_SL a
need_eq = CASL_SL a
forall a. Lattice a => CASL_SL a
bottom { has_eq :: Bool
has_eq = Bool
True }

-- minimal sublogic with predicates
need_pred :: Lattice a => CASL_SL a
need_pred :: CASL_SL a
need_pred = CASL_SL a
forall a. Lattice a => CASL_SL a
bottom { has_pred :: Bool
has_pred = Bool
True }

need_horn :: Lattice a => CASL_SL a
need_horn :: CASL_SL a
need_horn = CASL_SL a
forall a. Lattice a => CASL_SL a
bottom { which_logic :: CASL_Formulas
which_logic = CASL_Formulas
Horn }

need_fol :: Lattice a => CASL_SL a
need_fol :: CASL_SL a
need_fol = CASL_SL a
forall a. Lattice a => CASL_SL a
bottom { which_logic :: CASL_Formulas
which_logic = CASL_Formulas
FOL }

{- ---------------------------------------------------------------------------
Functions to generate a list of all sublogics for CASL
--------------------------------------------------------------------------- -}

{- all elements
create a list of all CASL sublogics by generating all possible
feature combinations and then filtering illegal ones out -}
sublogics_all :: Lattice a => [a] -> [CASL_SL a]
sublogics_all :: [a] -> [CASL_SL a]
sublogics_all l :: [a]
l = CASL_SL a
forall a. Lattice a => CASL_SL a
bottom CASL_SL a -> [CASL_SL a] -> [CASL_SL a]
forall a. a -> [a] -> [a]
: (a -> CASL_SL a) -> [a] -> [CASL_SL a]
forall a b. (a -> b) -> [a] -> [b]
map a -> CASL_SL a
forall a. a -> CASL_SL a
mkBot [a]
l [CASL_SL a] -> [CASL_SL a] -> [CASL_SL a]
forall a. [a] -> [a] -> [a]
++ [[CASL_SL a]] -> [CASL_SL a]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[a]] -> [[CASL_SL a]]
forall a. Lattice a => [[a]] -> [[CASL_SL a]]
sDims [])
 [CASL_SL a] -> [CASL_SL a] -> [CASL_SL a]
forall a. [a] -> [a] -> [a]
++ let subPAtom :: CASL_SL a
subPAtom = (CASL_SL a -> CASL_SL a -> CASL_SL a
forall a. Lattice a => CASL_SL a -> CASL_SL a -> CASL_SL a
sublogics_max CASL_SL a
forall a. Lattice a => CASL_SL a
need_part CASL_SL a
forall a. Lattice a => CASL_SL a
need_pred) { sub_features :: SubsortingFeatures
sub_features = SubsortingFeatures
Sub } in
    [ CASL_SL a -> CASL_SL a -> CASL_SL a
forall a. Lattice a => CASL_SL a -> CASL_SL a -> CASL_SL a
sublogics_max CASL_SL a
forall a. Lattice a => CASL_SL a
need_fol CASL_SL a
forall a. Lattice a => CASL_SL a
need_eq
    , [CASL_SL a] -> CASL_SL a
forall a. Lattice a => [CASL_SL a] -> CASL_SL a
comp_list [CASL_SL a
subPAtom, CASL_SL a
forall a. Lattice a => CASL_SL a
need_horn, CASL_SL a
forall a. Lattice a => CASL_SL a
need_eq]
    , CASL_SL a
subPAtom
    , CASL_SL a -> CASL_SL a -> CASL_SL a
forall a. Lattice a => CASL_SL a -> CASL_SL a -> CASL_SL a
sublogics_max CASL_SL a
subPAtom (Bool -> Bool -> SortGenTotality -> CASL_SL a
forall a. Lattice a => Bool -> Bool -> SortGenTotality -> CASL_SL a
need_cons Bool
False Bool
False SortGenTotality
SomePartial)
    , CASL_SL a
forall a. Lattice a => CASL_SL a
cFol, CASL_SL a
forall a. Lattice a => CASL_SL a
caslTop, CASL_SL a
forall a. Lattice a => CASL_SL a
top]

sDims :: Lattice a => [[a]] -> [[CASL_SL a]]
sDims :: [[a]] -> [[CASL_SL a]]
sDims l :: [[a]]
l = let
  t :: Bool
t = Bool
True
  b :: CASL_SL a
b = CASL_SL a
forall a. Lattice a => CASL_SL a
bottom
  bools :: [Bool]
bools = [Bool
True, Bool
False]
  in
  ([a] -> [CASL_SL a]) -> [[a]] -> [[CASL_SL a]]
forall a b. (a -> b) -> [a] -> [b]
map ((a -> CASL_SL a) -> [a] -> [CASL_SL a]
forall a b. (a -> b) -> [a] -> [b]
map a -> CASL_SL a
forall a. a -> CASL_SL a
mkBot) [[a]]
l [[CASL_SL a]] -> [[CASL_SL a]] -> [[CASL_SL a]]
forall a. [a] -> [a] -> [a]
++
  [ [ CASL_SL a
b { sub_features :: SubsortingFeatures
sub_features = SubsortingFeatures
s_f } | SubsortingFeatures
s_f <- [SubsortingFeatures
LocFilSub, SubsortingFeatures
Sub]]
  , [CASL_SL a
b { has_part :: Bool
has_part = Bool
t } ]
  , [CASL_SL a
b { cons_features :: SortGenerationFeatures
cons_features = SortGenerationFeatures
c_f } | 
    SortGenerationFeatures
c_f <- [ Bool -> Bool -> SortGenTotality -> SortGenerationFeatures
SortGen Bool
m Bool
s SortGenTotality
tc | 
      Bool
m <- [Bool]
bools, Bool
s <- [Bool]
bools, SortGenTotality
tc <- [ SortGenTotality
OnlyFree, SortGenTotality
OnlyTotal,  SortGenTotality
SomePartial ]]]
  , [CASL_SL a
b { has_eq :: Bool
has_eq = Bool
t } ]
  , [CASL_SL a
b { has_pred :: Bool
has_pred = Bool
t } ]
  , [CASL_SL a
b { has_empty_sorts :: Bool
has_empty_sorts = Bool
t } ]
  , [CASL_SL a
b { which_logic :: CASL_Formulas
which_logic = CASL_Formulas
fo } | CASL_Formulas
fo <- [CASL_Formulas] -> [CASL_Formulas]
forall a. [a] -> [a]
reverse [CASL_Formulas
SOL, CASL_Formulas
FOL, CASL_Formulas
Prenex, CASL_Formulas
GHorn, CASL_Formulas
Horn]]]

{- ----------------------------------------------------------------------------
Conversion functions (to String)
---------------------------------------------------------------------------- -}

formulas_name :: Bool -> CASL_Formulas -> String
formulas_name :: Bool -> CASL_Formulas -> String
formulas_name b :: Bool
b f :: CASL_Formulas
f = let Just s :: String
s = (Bool, CASL_Formulas)
-> [((Bool, CASL_Formulas), String)] -> Maybe String
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (Bool
b, CASL_Formulas
f) [((Bool, CASL_Formulas), String)]
nameList in String
s

nameList :: [((Bool, CASL_Formulas), String)]
nameList :: [((Bool, CASL_Formulas), String)]
nameList =
  [ ((Bool
True, CASL_Formulas
SOL), "SOL")
  , ((Bool
False, CASL_Formulas
SOL), "SOAlg")
  , ((Bool
True, CASL_Formulas
FOL), "FOL")
  , ((Bool
False, CASL_Formulas
FOL), "FOAlg")
  , ((Bool
True, CASL_Formulas
Prenex), "Prenex")
  , ((Bool
False,CASL_Formulas
Prenex), "PrenexAlg")
  , ((Bool
True, CASL_Formulas
GHorn), "GHorn")
  , ((Bool
False, CASL_Formulas
GHorn), "GCond")
  , ((Bool
True, CASL_Formulas
Horn), "Horn")
  , ((Bool
False, CASL_Formulas
Horn), "Cond")
  , ((Bool
True, CASL_Formulas
Atomic), "Atom")
  , ((Bool
False, CASL_Formulas
Atomic), "Eq")]

sublogics_name :: (a -> String) -> CASL_SL a -> String
sublogics_name :: (a -> String) -> CASL_SL a -> String
sublogics_name f :: a -> String
f x :: CASL_SL a
x = a -> String
f (CASL_SL a -> a
forall a. CASL_SL a -> a
ext_features CASL_SL a
x)
                    String -> ShowS
forall a. [a] -> [a] -> [a]
++ (case CASL_SL a -> SubsortingFeatures
forall a. CASL_SL a -> SubsortingFeatures
sub_features CASL_SL a
x of
                         NoSub -> ""
                         LocFilSub -> "Sul"
                         Sub -> "Sub")
                    String -> ShowS
forall a. [a] -> [a] -> [a]
++ (if CASL_SL a -> Bool
forall a. CASL_SL a -> Bool
has_part CASL_SL a
x then "P" else "")
                    String -> ShowS
forall a. [a] -> [a] -> [a]
++ (if CASL_SL a -> Bool
forall a. CASL_SL a -> Bool
has_cons CASL_SL a
x
                        then (if SortGenerationFeatures -> Bool
onlyInjConstrs (CASL_SL a -> SortGenerationFeatures
forall a. CASL_SL a -> SortGenerationFeatures
cons_features CASL_SL a
x)
                              then "s" else "") String -> ShowS
forall a. [a] -> [a] -> [a]
++
                             (if SortGenerationFeatures -> Bool
emptyMapping (CASL_SL a -> SortGenerationFeatures
forall a. CASL_SL a -> SortGenerationFeatures
cons_features CASL_SL a
x)
                              then "e" else "") String -> ShowS
forall a. [a] -> [a] -> [a]
++
                             ((SortGenTotality -> String
forall a. Show a => a -> String
show(SortGenTotality -> String)
-> (CASL_SL a -> SortGenTotality) -> CASL_SL a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.SortGenerationFeatures -> SortGenTotality
totality(SortGenerationFeatures -> SortGenTotality)
-> (CASL_SL a -> SortGenerationFeatures)
-> CASL_SL a
-> SortGenTotality
forall b c a. (b -> c) -> (a -> b) -> a -> c
.CASL_SL a -> SortGenerationFeatures
forall a. CASL_SL a -> SortGenerationFeatures
cons_features) CASL_SL a
x) String -> ShowS
forall a. [a] -> [a] -> [a]
++ "C"
                         else "")
                    String -> ShowS
forall a. [a] -> [a] -> [a]
++ Bool -> CASL_Formulas -> String
formulas_name (CASL_SL a -> Bool
forall a. CASL_SL a -> Bool
has_pred CASL_SL a
x) (CASL_SL a -> CASL_Formulas
forall a. CASL_SL a -> CASL_Formulas
which_logic CASL_SL a
x)
                    String -> ShowS
forall a. [a] -> [a] -> [a]
++ (if CASL_SL a -> Bool
forall a. CASL_SL a -> Bool
has_eq CASL_SL a
x then "=" else "")
                    String -> ShowS
forall a. [a] -> [a] -> [a]
++ if CASL_SL a -> Bool
forall a. CASL_SL a -> Bool
has_empty_sorts CASL_SL a
x then "E" else ""

parseBool :: String -> String -> (Bool, String)
parseBool :: String -> String -> (Bool, String)
parseBool p :: String
p s :: String
s = case String -> String -> Maybe String
forall a. Eq a => [a] -> [a] -> Maybe [a]
stripPrefix String
p String
s of
        Just r :: String
r -> (Bool
True, String
r)
        Nothing -> (Bool
False, String
s)

parseSL :: (String -> Maybe (a, String)) -> String -> Maybe (CASL_SL a)
parseSL :: (String -> Maybe (a, String)) -> String -> Maybe (CASL_SL a)
parseSL f :: String -> Maybe (a, String)
f s0 :: String
s0 = do
  (a :: a
a, s1 :: String
s1) <- String -> Maybe (a, String)
f String
s0
  (sub :: SubsortingFeatures
sub, s2 :: String
s2) <- case String -> String -> Maybe String
forall a. Eq a => [a] -> [a] -> Maybe [a]
stripPrefix "Su" String
s1 of
    Just r :: String
r -> case String
r of
      c :: Char
c : t :: String
t -> case Char
c of
        'l' -> (SubsortingFeatures, String) -> Maybe (SubsortingFeatures, String)
forall a. a -> Maybe a
Just (SubsortingFeatures
LocFilSub, String
t)
        'b' -> (SubsortingFeatures, String) -> Maybe (SubsortingFeatures, String)
forall a. a -> Maybe a
Just (SubsortingFeatures
Sub, String
t)
        _ -> Maybe (SubsortingFeatures, String)
forall a. Maybe a
Nothing
      "" -> Maybe (SubsortingFeatures, String)
forall a. Maybe a
Nothing
    Nothing -> (SubsortingFeatures, String) -> Maybe (SubsortingFeatures, String)
forall a. a -> Maybe a
Just (SubsortingFeatures
NoSub, String
s1)
  let (pa :: Bool
pa, s3 :: String
s3) = String -> String -> (Bool, String)
parseBool "P" String
s2
      (c :: SortGenerationFeatures
c, s4 :: String
s4) = String -> (SortGenerationFeatures, String)
parseCons String
s3
  ((pr :: Bool
pr, l :: CASL_Formulas
l), s5 :: String
s5) <- String -> Maybe ((Bool, CASL_Formulas), String)
parseForm String
s4
  let (eq :: Bool
eq, s6 :: String
s6) = String -> String -> (Bool, String)
parseBool "=" String
s5
      (es :: Bool
es, s7 :: String
s7) = String -> String -> (Bool, String)
parseBool "E" String
s6
  Bool -> Maybe () -> Maybe ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
s7) Maybe ()
forall a. Maybe a
Nothing
  CASL_SL a -> Maybe (CASL_SL a)
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> CASL_SL a
forall a. a -> CASL_SL a
mkBot a
a)
    { sub_features :: SubsortingFeatures
sub_features = SubsortingFeatures
sub
    , has_part :: Bool
has_part = Bool
pa
    , cons_features :: SortGenerationFeatures
cons_features = SortGenerationFeatures
c
    , has_pred :: Bool
has_pred = Bool
pr
    , which_logic :: CASL_Formulas
which_logic = CASL_Formulas
l
    , has_eq :: Bool
has_eq = Bool
eq
    , has_empty_sorts :: Bool
has_empty_sorts = Bool
es }

parseForm :: String -> Maybe ((Bool, CASL_Formulas), String)
parseForm :: String -> Maybe ((Bool, CASL_Formulas), String)
parseForm s :: String
s = (((Bool, CASL_Formulas), String)
 -> Maybe ((Bool, CASL_Formulas), String)
 -> Maybe ((Bool, CASL_Formulas), String))
-> Maybe ((Bool, CASL_Formulas), String)
-> [((Bool, CASL_Formulas), String)]
-> Maybe ((Bool, CASL_Formulas), String)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (q :: (Bool, CASL_Formulas)
q, p :: String
p) m :: Maybe ((Bool, CASL_Formulas), String)
m -> case Maybe ((Bool, CASL_Formulas), String)
m of
  Just _ -> Maybe ((Bool, CASL_Formulas), String)
m
  Nothing -> case String -> String -> Maybe String
forall a. Eq a => [a] -> [a] -> Maybe [a]
stripPrefix String
p String
s of
    Just r :: String
r -> ((Bool, CASL_Formulas), String)
-> Maybe ((Bool, CASL_Formulas), String)
forall a. a -> Maybe a
Just ((Bool, CASL_Formulas)
q, String
r)
    Nothing -> Maybe ((Bool, CASL_Formulas), String)
m) Maybe ((Bool, CASL_Formulas), String)
forall a. Maybe a
Nothing [((Bool, CASL_Formulas), String)]
nameList

parseCons :: String -> (SortGenerationFeatures, String)
parseCons :: String -> (SortGenerationFeatures, String)
parseCons s :: String
s = let (ojc :: Bool
ojc, s1 :: String
s1) = String -> String -> (Bool, String)
parseBool "s" String
s in
              let (em :: Bool
em, s2 :: String
s2) = String -> String -> (Bool, String)
parseBool "e" String
s1 in
              let (ofr :: Bool
ofr, s3 :: String
s3) = String -> String -> (Bool, String)
parseBool "f" String
s2 in
              let (oto :: Bool
oto, s4 :: String
s4) = String -> String -> (Bool, String)
parseBool "t" String
s3 in
              let tc :: SortGenTotality
tc = if Bool
ofr
                          then SortGenTotality
OnlyFree
                          else if Bool
oto then SortGenTotality
OnlyTotal else SortGenTotality
SomePartial
              in
              let (sgc :: Bool
sgc, s5 :: String
s5) = String -> String -> (Bool, String)
parseBool "C" String
s4 in
              if Bool -> Bool
not Bool
sgc Bool -> Bool -> Bool
|| String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf "ond" String
s5
                 then (SortGenerationFeatures
NoSortGen, String
s)
                 else ((Bool -> Bool -> SortGenTotality -> SortGenerationFeatures
SortGen Bool
ojc Bool
em SortGenTotality
tc), String
s5)


{- ----------------------------------------------------------------------------
join or max functions
---------------------------------------------------------------------------- -}

sublogics_join :: (Bool -> Bool -> Bool)
               -> (SubsortingFeatures -> SubsortingFeatures
                   -> SubsortingFeatures)
               -> (SortGenerationFeatures -> SortGenerationFeatures
                   -> SortGenerationFeatures)
               -> (CASL_Formulas -> CASL_Formulas -> CASL_Formulas)
               -> (a -> a -> a)
               -> CASL_SL a -> CASL_SL a -> CASL_SL a
sublogics_join :: (Bool -> Bool -> Bool)
-> (SubsortingFeatures -> SubsortingFeatures -> SubsortingFeatures)
-> (SortGenerationFeatures
    -> SortGenerationFeatures -> SortGenerationFeatures)
-> (CASL_Formulas -> CASL_Formulas -> CASL_Formulas)
-> (a -> a -> a)
-> CASL_SL a
-> CASL_SL a
-> CASL_SL a
sublogics_join jB :: Bool -> Bool -> Bool
jB jS :: SubsortingFeatures -> SubsortingFeatures -> SubsortingFeatures
jS jC :: SortGenerationFeatures
-> SortGenerationFeatures -> SortGenerationFeatures
jC jF :: CASL_Formulas -> CASL_Formulas -> CASL_Formulas
jF jE :: a -> a -> a
jE a :: CASL_SL a
a b :: CASL_SL a
b = CASL_SL :: forall a.
SubsortingFeatures
-> Bool
-> SortGenerationFeatures
-> Bool
-> Bool
-> CASL_Formulas
-> Bool
-> a
-> CASL_SL a
CASL_SL
    { sub_features :: SubsortingFeatures
sub_features = SubsortingFeatures -> SubsortingFeatures -> SubsortingFeatures
jS (CASL_SL a -> SubsortingFeatures
forall a. CASL_SL a -> SubsortingFeatures
sub_features CASL_SL a
a) (CASL_SL a -> SubsortingFeatures
forall a. CASL_SL a -> SubsortingFeatures
sub_features CASL_SL a
b)
    , ext_features :: a
ext_features = a -> a -> a
jE (CASL_SL a -> a
forall a. CASL_SL a -> a
ext_features CASL_SL a
a) (CASL_SL a -> a
forall a. CASL_SL a -> a
ext_features CASL_SL a
b)
    , has_part :: Bool
has_part = Bool -> Bool -> Bool
jB (CASL_SL a -> Bool
forall a. CASL_SL a -> Bool
has_part CASL_SL a
a) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ CASL_SL a -> Bool
forall a. CASL_SL a -> Bool
has_part CASL_SL a
b
    , cons_features :: SortGenerationFeatures
cons_features = SortGenerationFeatures
-> SortGenerationFeatures -> SortGenerationFeatures
jC (CASL_SL a -> SortGenerationFeatures
forall a. CASL_SL a -> SortGenerationFeatures
cons_features CASL_SL a
a) (CASL_SL a -> SortGenerationFeatures
forall a. CASL_SL a -> SortGenerationFeatures
cons_features CASL_SL a
b)
    , has_eq :: Bool
has_eq = Bool -> Bool -> Bool
jB (CASL_SL a -> Bool
forall a. CASL_SL a -> Bool
has_eq CASL_SL a
a) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ CASL_SL a -> Bool
forall a. CASL_SL a -> Bool
has_eq CASL_SL a
b
    , has_pred :: Bool
has_pred = Bool -> Bool -> Bool
jB (CASL_SL a -> Bool
forall a. CASL_SL a -> Bool
has_pred CASL_SL a
a) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ CASL_SL a -> Bool
forall a. CASL_SL a -> Bool
has_pred CASL_SL a
b
    , has_empty_sorts :: Bool
has_empty_sorts = Bool -> Bool -> Bool
jB (CASL_SL a -> Bool
forall a. CASL_SL a -> Bool
has_empty_sorts CASL_SL a
a) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ CASL_SL a -> Bool
forall a. CASL_SL a -> Bool
has_empty_sorts CASL_SL a
b
    , which_logic :: CASL_Formulas
which_logic = CASL_Formulas -> CASL_Formulas -> CASL_Formulas
jF (CASL_SL a -> CASL_Formulas
forall a. CASL_SL a -> CASL_Formulas
which_logic CASL_SL a
a) (CASL_SL a -> CASL_Formulas
forall a. CASL_SL a -> CASL_Formulas
which_logic CASL_SL a
b)
    }

sublogics_max :: Lattice a => CASL_SL a -> CASL_SL a
              -> CASL_SL a
sublogics_max :: CASL_SL a -> CASL_SL a -> CASL_SL a
sublogics_max = (Bool -> Bool -> Bool)
-> (SubsortingFeatures -> SubsortingFeatures -> SubsortingFeatures)
-> (SortGenerationFeatures
    -> SortGenerationFeatures -> SortGenerationFeatures)
-> (CASL_Formulas -> CASL_Formulas -> CASL_Formulas)
-> (a -> a -> a)
-> CASL_SL a
-> CASL_SL a
-> CASL_SL a
forall a.
(Bool -> Bool -> Bool)
-> (SubsortingFeatures -> SubsortingFeatures -> SubsortingFeatures)
-> (SortGenerationFeatures
    -> SortGenerationFeatures -> SortGenerationFeatures)
-> (CASL_Formulas -> CASL_Formulas -> CASL_Formulas)
-> (a -> a -> a)
-> CASL_SL a
-> CASL_SL a
-> CASL_SL a
sublogics_join Bool -> Bool -> Bool
forall a. Ord a => a -> a -> a
max SubsortingFeatures -> SubsortingFeatures -> SubsortingFeatures
forall a. Ord a => a -> a -> a
max ((Bool -> Bool -> Bool)
-> (SortGenTotality -> SortGenTotality -> SortGenTotality)
-> SortGenerationFeatures
-> SortGenerationFeatures
-> SortGenerationFeatures
joinSortGenFeature Bool -> Bool -> Bool
forall a. Ord a => a -> a -> a
min SortGenTotality -> SortGenTotality -> SortGenTotality
forall a. Ord a => a -> a -> a
min) CASL_Formulas -> CASL_Formulas -> CASL_Formulas
forall a. Ord a => a -> a -> a
max a -> a -> a
forall l. Lattice l => l -> l -> l
cjoin

{- ----------------------------------------------------------------------------
Helper functions
---------------------------------------------------------------------------- -}

-- compute sublogics from a list of sublogics
comp_list :: Lattice a => [CASL_SL a] -> CASL_SL a
comp_list :: [CASL_SL a] -> CASL_SL a
comp_list = (CASL_SL a -> CASL_SL a -> CASL_SL a)
-> CASL_SL a -> [CASL_SL a] -> CASL_SL a
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl CASL_SL a -> CASL_SL a -> CASL_SL a
forall a. Lattice a => CASL_SL a -> CASL_SL a -> CASL_SL a
sublogics_max CASL_SL a
forall a. Lattice a => CASL_SL a
bottom

{- map a function returning Maybe over a list of arguments
. a list of Pos is maintained by removing an element if the
function f returns Nothing on the corresponding element of
the argument list
. leftover elements in the Pos list after the argument
list is exhausted are appended at the end with Nothing
as a substitute for f's result -}
mapMaybePos :: [Pos] -> (a -> Maybe b) -> [a] -> [(Maybe b, Pos)]
mapMaybePos :: [Pos] -> (a -> Maybe b) -> [a] -> [(Maybe b, Pos)]
mapMaybePos [] _ _ = []
mapMaybePos (p1 :: Pos
p1 : pl :: [Pos]
pl) f :: a -> Maybe b
f [] = (Maybe b
forall a. Maybe a
Nothing, Pos
p1) (Maybe b, Pos) -> [(Maybe b, Pos)] -> [(Maybe b, Pos)]
forall a. a -> [a] -> [a]
: [Pos] -> (a -> Maybe b) -> [a] -> [(Maybe b, Pos)]
forall a b. [Pos] -> (a -> Maybe b) -> [a] -> [(Maybe b, Pos)]
mapMaybePos [Pos]
pl a -> Maybe b
f []
mapMaybePos (p1 :: Pos
p1 : pl :: [Pos]
pl) f :: a -> Maybe b
f (h :: a
h : t :: [a]
t) = let res :: Maybe b
res = a -> Maybe b
f a
h in
  (if Maybe b -> Bool
forall a. Maybe a -> Bool
isJust Maybe b
res then ((Maybe b
res, Pos
p1) (Maybe b, Pos) -> [(Maybe b, Pos)] -> [(Maybe b, Pos)]
forall a. a -> [a] -> [a]
:) else [(Maybe b, Pos)] -> [(Maybe b, Pos)]
forall a. a -> a
id) ([(Maybe b, Pos)] -> [(Maybe b, Pos)])
-> [(Maybe b, Pos)] -> [(Maybe b, Pos)]
forall a b. (a -> b) -> a -> b
$ [Pos] -> (a -> Maybe b) -> [a] -> [(Maybe b, Pos)]
forall a b. [Pos] -> (a -> Maybe b) -> [a] -> [(Maybe b, Pos)]
mapMaybePos [Pos]
pl a -> Maybe b
f [a]
t

{- map with partial function f on Maybe type
will remove elements from given Pos list for elements of [a]
where f returns Nothing
given number of elements from the beginning of Range are always
kept -}
mapPos :: Int -> Range -> (a -> Maybe b) -> [a] -> ([b], Range)
mapPos :: Int -> Range -> (a -> Maybe b) -> [a] -> ([b], Range)
mapPos c :: Int
c (Range p :: [Pos]
p) f :: a -> Maybe b
f l :: [a]
l = let
                   (res :: [Maybe b]
res, pos :: [Pos]
pos) = [(Maybe b, Pos)] -> ([Maybe b], [Pos])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(Maybe b, Pos)] -> ([Maybe b], [Pos]))
-> [(Maybe b, Pos)] -> ([Maybe b], [Pos])
forall a b. (a -> b) -> a -> b
$ [Pos] -> (a -> Maybe b) -> [a] -> [(Maybe b, Pos)]
forall a b. [Pos] -> (a -> Maybe b) -> [a] -> [(Maybe b, Pos)]
mapMaybePos (Int -> [Pos] -> [Pos]
forall a. Int -> [a] -> [a]
drop Int
c [Pos]
p) a -> Maybe b
f [a]
l
                 in
                   ([Maybe b] -> [b]
forall a. [Maybe a] -> [a]
catMaybes [Maybe b]
res, [Pos] -> Range
Range (Int -> [Pos] -> [Pos]
forall a. Int -> [a] -> [a]
take Int
c [Pos]
p [Pos] -> [Pos] -> [Pos]
forall a. [a] -> [a] -> [a]
++ [Pos]
pos))

{- ----------------------------------------------------------------------------
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.
--------------------------------------------------------------------------- -}

sl_form_level :: (f -> CASL_Formulas)
              -> (Bool, Bool) -> FORMULA f -> CASL_Formulas
sl_form_level :: (f -> CASL_Formulas) -> (Bool, Bool) -> FORMULA f -> CASL_Formulas
sl_form_level ff :: f -> CASL_Formulas
ff (isCompound :: Bool
isCompound, leftImp :: Bool
leftImp) phi :: FORMULA f
phi = let
     subl :: CASL_Formulas
subl = (f -> CASL_Formulas) -> (Bool, Bool) -> FORMULA f -> CASL_Formulas
forall f.
(f -> CASL_Formulas) -> (Bool, Bool) -> FORMULA f -> CASL_Formulas
sl_form_level_aux f -> CASL_Formulas
ff (Bool
isCompound, Bool
leftImp) FORMULA f
phi
  in if CASL_Formulas
subl CASL_Formulas -> CASL_Formulas -> Bool
forall a. Eq a => a -> a -> Bool
== CASL_Formulas
FOL 
      then if Bool -> (f -> CASL_Formulas) -> FORMULA f -> Bool
forall f. Bool -> (f -> CASL_Formulas) -> FORMULA f -> Bool
testPrenex Bool
True f -> CASL_Formulas
ff FORMULA f
phi then CASL_Formulas
Prenex
                                  else CASL_Formulas
FOL
      else CASL_Formulas
subl 

sl_form_level_aux :: (f -> CASL_Formulas)
              -> (Bool, Bool) -> FORMULA f -> CASL_Formulas
sl_form_level_aux :: (f -> CASL_Formulas) -> (Bool, Bool) -> FORMULA f -> CASL_Formulas
sl_form_level_aux ff :: f -> CASL_Formulas
ff (isCompound :: Bool
isCompound, leftImp :: Bool
leftImp) phi :: FORMULA f
phi =
 case FORMULA f
phi of
   Quantification q :: QUANTIFIER
q _ f :: FORMULA f
f _ ->
       let ql :: CASL_Formulas
ql = (f -> CASL_Formulas) -> (Bool, Bool) -> FORMULA f -> CASL_Formulas
forall f.
(f -> CASL_Formulas) -> (Bool, Bool) -> FORMULA f -> CASL_Formulas
sl_form_level_aux f -> CASL_Formulas
ff (Bool
isCompound, Bool
leftImp) FORMULA f
f
       in if QUANTIFIER -> Bool
is_atomic_q QUANTIFIER
q then CASL_Formulas
ql else CASL_Formulas -> CASL_Formulas -> CASL_Formulas
forall a. Ord a => a -> a -> a
max CASL_Formulas
FOL CASL_Formulas
ql
   Junction j :: Junctor
j l :: [FORMULA f]
l _ -> [CASL_Formulas] -> CASL_Formulas
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([CASL_Formulas] -> CASL_Formulas)
-> [CASL_Formulas] -> CASL_Formulas
forall a b. (a -> b) -> a -> b
$ case Junctor
j of
      Con -> CASL_Formulas
FOL CASL_Formulas -> [CASL_Formulas] -> [CASL_Formulas]
forall a. a -> [a] -> [a]
: (FORMULA f -> CASL_Formulas) -> [FORMULA f] -> [CASL_Formulas]
forall a b. (a -> b) -> [a] -> [b]
map ((f -> CASL_Formulas) -> (Bool, Bool) -> FORMULA f -> CASL_Formulas
forall f.
(f -> CASL_Formulas) -> (Bool, Bool) -> FORMULA f -> CASL_Formulas
sl_form_level_aux f -> CASL_Formulas
ff (Bool
True, Bool
leftImp)) [FORMULA f]
l
      Dis -> CASL_Formulas
FOL CASL_Formulas -> [CASL_Formulas] -> [CASL_Formulas]
forall a. a -> [a] -> [a]
: (FORMULA f -> CASL_Formulas) -> [FORMULA f] -> [CASL_Formulas]
forall a b. (a -> b) -> [a] -> [b]
map ((f -> CASL_Formulas) -> (Bool, Bool) -> FORMULA f -> CASL_Formulas
forall f.
(f -> CASL_Formulas) -> (Bool, Bool) -> FORMULA f -> CASL_Formulas
sl_form_level_aux f -> CASL_Formulas
ff (Bool
False, Bool
False)) [FORMULA f]
l
   Relation l1 :: FORMULA f
l1 c :: Relation
c l2 :: FORMULA f
l2 _ -> [CASL_Formulas] -> CASL_Formulas
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([CASL_Formulas] -> CASL_Formulas)
-> [CASL_Formulas] -> CASL_Formulas
forall a b. (a -> b) -> a -> b
$ (f -> CASL_Formulas) -> (Bool, Bool) -> FORMULA f -> CASL_Formulas
forall f.
(f -> CASL_Formulas) -> (Bool, Bool) -> FORMULA f -> CASL_Formulas
sl_form_level_aux f -> CASL_Formulas
ff (Bool
True, Bool
True) FORMULA f
l1
     CASL_Formulas -> [CASL_Formulas] -> [CASL_Formulas]
forall a. a -> [a] -> [a]
: case Relation
c of
         Equivalence -> [ (f -> CASL_Formulas) -> (Bool, Bool) -> FORMULA f -> CASL_Formulas
forall f.
(f -> CASL_Formulas) -> (Bool, Bool) -> FORMULA f -> CASL_Formulas
sl_form_level_aux f -> CASL_Formulas
ff (Bool
True, Bool
True) FORMULA f
l2
                        , if Bool
leftImp then CASL_Formulas
FOL else CASL_Formulas
GHorn ]
         _ -> [ (f -> CASL_Formulas) -> (Bool, Bool) -> FORMULA f -> CASL_Formulas
forall f.
(f -> CASL_Formulas) -> (Bool, Bool) -> FORMULA f -> CASL_Formulas
sl_form_level_aux f -> CASL_Formulas
ff (Bool
True, Bool
False) FORMULA f
l2
              , if Bool
leftImp then CASL_Formulas
FOL else
                    if Bool
isCompound then CASL_Formulas
GHorn else CASL_Formulas
Horn ]
   Negation f :: FORMULA f
f _ -> CASL_Formulas -> CASL_Formulas -> CASL_Formulas
forall a. Ord a => a -> a -> a
max CASL_Formulas
FOL (CASL_Formulas -> CASL_Formulas) -> CASL_Formulas -> CASL_Formulas
forall a b. (a -> b) -> a -> b
$ (f -> CASL_Formulas) -> (Bool, Bool) -> FORMULA f -> CASL_Formulas
forall f.
(f -> CASL_Formulas) -> (Bool, Bool) -> FORMULA f -> CASL_Formulas
sl_form_level_aux f -> CASL_Formulas
ff (Bool
False, Bool
False) FORMULA f
f
   Atom b :: Bool
b _ -> if Bool
b then CASL_Formulas
Atomic else CASL_Formulas
FOL
   Equation _ e :: Equality
e _ _
     | Equality
e Equality -> Equality -> Bool
forall a. Eq a => a -> a -> Bool
== Equality
Existl -> CASL_Formulas
Atomic
     | Bool
leftImp -> CASL_Formulas
FOL
     | Bool
otherwise -> CASL_Formulas
Horn
   QuantOp {} -> CASL_Formulas
SOL  -- it can't get worse
   QuantPred {} -> CASL_Formulas
SOL
   ExtFORMULA f :: f
f -> f -> CASL_Formulas
ff f
f
   _ -> CASL_Formulas
Atomic

testPrenex :: Bool -> (f -> CASL_Formulas) -> FORMULA f -> Bool
testPrenex :: Bool -> (f -> CASL_Formulas) -> FORMULA f -> Bool
testPrenex topQ :: Bool
topQ ff :: f -> CASL_Formulas
ff phi :: FORMULA f
phi = 
  case FORMULA f
phi of 
    Quantification _ _ phi' :: FORMULA f
phi' _ -> if Bool
topQ then Bool -> (f -> CASL_Formulas) -> FORMULA f -> Bool
forall f. Bool -> (f -> CASL_Formulas) -> FORMULA f -> Bool
testPrenex Bool
True f -> CASL_Formulas
ff FORMULA f
phi' else Bool
False
    Junction _ l :: [FORMULA f]
l _ -> (Bool -> FORMULA f -> Bool) -> Bool -> [FORMULA f] -> Bool
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\b :: Bool
b x :: FORMULA f
x -> Bool
b Bool -> Bool -> Bool
&& Bool -> (f -> CASL_Formulas) -> FORMULA f -> Bool
forall f. Bool -> (f -> CASL_Formulas) -> FORMULA f -> Bool
testPrenex Bool
False f -> CASL_Formulas
ff FORMULA f
x) Bool
True [FORMULA f]
l
    Relation l1 :: FORMULA f
l1 _ l2 :: FORMULA f
l2 _ -> Bool -> (f -> CASL_Formulas) -> FORMULA f -> Bool
forall f. Bool -> (f -> CASL_Formulas) -> FORMULA f -> Bool
testPrenex Bool
False f -> CASL_Formulas
ff FORMULA f
l1 Bool -> Bool -> Bool
&& Bool -> (f -> CASL_Formulas) -> FORMULA f -> Bool
forall f. Bool -> (f -> CASL_Formulas) -> FORMULA f -> Bool
testPrenex Bool
False f -> CASL_Formulas
ff FORMULA f
l2
    Negation f :: FORMULA f
f _ -> Bool -> (f -> CASL_Formulas) -> FORMULA f -> Bool
forall f. Bool -> (f -> CASL_Formulas) -> FORMULA f -> Bool
testPrenex Bool
False f -> CASL_Formulas
ff FORMULA f
f
    Atom _ _ -> Bool
True
    Equation _ _ _ _ -> Bool
True 
    QuantOp {} -> String -> Bool
forall a. HasCallStack => String -> a
error "should not get quant ops in FOL"
    QuantPred {} -> String -> Bool
forall a. HasCallStack => String -> a
error "should not get quant preds in FOL"
    ExtFORMULA f :: f
f -> if f -> CASL_Formulas
ff f
f CASL_Formulas -> CASL_Formulas -> Bool
forall a. Eq a => a -> a -> Bool
== CASL_Formulas
Prenex then Bool
True else Bool
False
    _ -> Bool
True 
    

-- QUANTIFIER
is_atomic_q :: QUANTIFIER -> Bool
is_atomic_q :: QUANTIFIER -> Bool
is_atomic_q Universal = Bool
True
is_atomic_q _ = Bool
False

-- compute logic of a formula by checking all logics in turn
get_logic :: Lattice a => (f -> CASL_SL a)
          -> FORMULA f -> CASL_SL a
get_logic :: (f -> CASL_SL a) -> FORMULA f -> CASL_SL a
get_logic ff :: f -> CASL_SL a
ff f :: FORMULA f
f = CASL_SL a
forall a. Lattice a => CASL_SL a
bottom
  { which_logic :: CASL_Formulas
which_logic = (f -> CASL_Formulas) -> (Bool, Bool) -> FORMULA f -> CASL_Formulas
forall f.
(f -> CASL_Formulas) -> (Bool, Bool) -> FORMULA f -> CASL_Formulas
sl_form_level (CASL_SL a -> CASL_Formulas
forall a. CASL_SL a -> CASL_Formulas
which_logic (CASL_SL a -> CASL_Formulas)
-> (f -> CASL_SL a) -> f -> CASL_Formulas
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f -> CASL_SL a
ff) (Bool
False, Bool
False) FORMULA f
f }

-- for the formula inside a subsort-defn
get_logic_sd :: Lattice a => (f -> CASL_SL a)
             -> FORMULA f -> CASL_SL a
get_logic_sd :: (f -> CASL_SL a) -> FORMULA f -> CASL_SL a
get_logic_sd ff :: f -> CASL_SL a
ff f :: FORMULA f
f = CASL_SL a
forall a. Lattice a => CASL_SL a
bottom
  { which_logic :: CASL_Formulas
which_logic =
    CASL_Formulas -> CASL_Formulas -> CASL_Formulas
forall a. Ord a => a -> a -> a
max CASL_Formulas
Horn (CASL_Formulas -> CASL_Formulas) -> CASL_Formulas -> CASL_Formulas
forall a b. (a -> b) -> a -> b
$ (f -> CASL_Formulas) -> (Bool, Bool) -> FORMULA f -> CASL_Formulas
forall f.
(f -> CASL_Formulas) -> (Bool, Bool) -> FORMULA f -> CASL_Formulas
sl_form_level (CASL_SL a -> CASL_Formulas
forall a. CASL_SL a -> CASL_Formulas
which_logic (CASL_SL a -> CASL_Formulas)
-> (f -> CASL_SL a) -> f -> CASL_Formulas
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f -> CASL_SL a
ff) (Bool
False, Bool
False) FORMULA f
f }

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

sl_basic_spec :: Lattice a => (b -> CASL_SL a)
              -> (s -> CASL_SL a)
              -> (f -> CASL_SL a)
              -> BASIC_SPEC b s f -> CASL_SL a
sl_basic_spec :: (b -> CASL_SL a)
-> (s -> CASL_SL a)
-> (f -> CASL_SL a)
-> BASIC_SPEC b s f
-> CASL_SL a
sl_basic_spec bf :: b -> CASL_SL a
bf sf :: s -> CASL_SL a
sf ff :: f -> CASL_SL a
ff (Basic_spec l :: [Annoted (BASIC_ITEMS b s f)]
l) =
    [CASL_SL a] -> CASL_SL a
forall a. Lattice a => [CASL_SL a] -> CASL_SL a
comp_list ([CASL_SL a] -> CASL_SL a) -> [CASL_SL a] -> CASL_SL a
forall a b. (a -> b) -> a -> b
$ (Annoted (BASIC_ITEMS b s f) -> CASL_SL a)
-> [Annoted (BASIC_ITEMS b s f)] -> [CASL_SL a]
forall a b. (a -> b) -> [a] -> [b]
map ((b -> CASL_SL a)
-> (s -> CASL_SL a)
-> (f -> CASL_SL a)
-> BASIC_ITEMS b s f
-> CASL_SL a
forall a b s f.
Lattice a =>
(b -> CASL_SL a)
-> (s -> CASL_SL a)
-> (f -> CASL_SL a)
-> BASIC_ITEMS b s f
-> CASL_SL a
sl_basic_items b -> CASL_SL a
bf s -> CASL_SL a
sf f -> CASL_SL a
ff (BASIC_ITEMS b s f -> CASL_SL a)
-> (Annoted (BASIC_ITEMS b s f) -> BASIC_ITEMS b s f)
-> Annoted (BASIC_ITEMS b s f)
-> CASL_SL a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted (BASIC_ITEMS b s f) -> BASIC_ITEMS b s f
forall a. Annoted a -> a
item) [Annoted (BASIC_ITEMS b s f)]
l
sl_basic_items :: Lattice a => (b -> CASL_SL a)
              -> (s -> CASL_SL a)
              -> (f -> CASL_SL a)
              -> BASIC_ITEMS b s f -> CASL_SL a
sl_basic_items :: (b -> CASL_SL a)
-> (s -> CASL_SL a)
-> (f -> CASL_SL a)
-> BASIC_ITEMS b s f
-> CASL_SL a
sl_basic_items bf :: b -> CASL_SL a
bf sf :: s -> CASL_SL a
sf ff :: f -> CASL_SL a
ff bi :: BASIC_ITEMS b s f
bi = case BASIC_ITEMS b s f
bi of
    Sig_items i :: SIG_ITEMS s f
i -> (s -> CASL_SL a) -> (f -> CASL_SL a) -> SIG_ITEMS s f -> CASL_SL a
forall a s f.
Lattice a =>
(s -> CASL_SL a) -> (f -> CASL_SL a) -> SIG_ITEMS s f -> CASL_SL a
sl_sig_items s -> CASL_SL a
sf f -> CASL_SL a
ff SIG_ITEMS s f
i
    Free_datatype sk :: SortsKind
sk l :: [Annoted DATATYPE_DECL]
l _ -> CASL_SL a -> CASL_SL a -> CASL_SL a
forall a. Lattice a => CASL_SL a -> CASL_SL a -> CASL_SL a
sublogics_max (Bool -> Bool -> SortGenTotality -> CASL_SL a
forall a. Lattice a => Bool -> Bool -> SortGenTotality -> CASL_SL a
need_cons Bool
True Bool
True SortGenTotality
OnlyFree)
        (CASL_SL a -> CASL_SL a) -> CASL_SL a -> CASL_SL a
forall a b. (a -> b) -> a -> b
$ SortsKind -> CASL_SL a -> CASL_SL a
forall a. Lattice a => SortsKind -> CASL_SL a -> CASL_SL a
needsEmptySorts SortsKind
sk (CASL_SL a -> CASL_SL a) -> CASL_SL a -> CASL_SL a
forall a b. (a -> b) -> a -> b
$ [CASL_SL a] -> CASL_SL a
forall a. Lattice a => [CASL_SL a] -> CASL_SL a
comp_list ([CASL_SL a] -> CASL_SL a) -> [CASL_SL a] -> CASL_SL a
forall a b. (a -> b) -> a -> b
$ (Annoted DATATYPE_DECL -> CASL_SL a)
-> [Annoted DATATYPE_DECL] -> [CASL_SL a]
forall a b. (a -> b) -> [a] -> [b]
map (DATATYPE_DECL -> CASL_SL a
forall a. Lattice a => DATATYPE_DECL -> CASL_SL a
sl_datatype_decl (DATATYPE_DECL -> CASL_SL a)
-> (Annoted DATATYPE_DECL -> DATATYPE_DECL)
-> Annoted DATATYPE_DECL
-> CASL_SL a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted DATATYPE_DECL -> DATATYPE_DECL
forall a. Annoted a -> a
item) [Annoted DATATYPE_DECL]
l
    Sort_gen l :: [Annoted (SIG_ITEMS s f)]
l _ -> CASL_SL a -> CASL_SL a -> CASL_SL a
forall a. Lattice a => CASL_SL a -> CASL_SL a -> CASL_SL a
sublogics_max (Bool -> Bool -> SortGenTotality -> CASL_SL a
forall a. Lattice a => Bool -> Bool -> SortGenTotality -> CASL_SL a
need_cons Bool
True Bool
True SortGenTotality
OnlyTotal)
        (CASL_SL a -> CASL_SL a) -> CASL_SL a -> CASL_SL a
forall a b. (a -> b) -> a -> b
$ [CASL_SL a] -> CASL_SL a
forall a. Lattice a => [CASL_SL a] -> CASL_SL a
comp_list ([CASL_SL a] -> CASL_SL a) -> [CASL_SL a] -> CASL_SL a
forall a b. (a -> b) -> a -> b
$ (Annoted (SIG_ITEMS s f) -> CASL_SL a)
-> [Annoted (SIG_ITEMS s f)] -> [CASL_SL a]
forall a b. (a -> b) -> [a] -> [b]
map ((s -> CASL_SL a) -> (f -> CASL_SL a) -> SIG_ITEMS s f -> CASL_SL a
forall a s f.
Lattice a =>
(s -> CASL_SL a) -> (f -> CASL_SL a) -> SIG_ITEMS s f -> CASL_SL a
sl_sig_items s -> CASL_SL a
sf f -> CASL_SL a
ff (SIG_ITEMS s f -> CASL_SL a)
-> (Annoted (SIG_ITEMS s f) -> SIG_ITEMS s f)
-> Annoted (SIG_ITEMS s f)
-> CASL_SL a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted (SIG_ITEMS s f) -> SIG_ITEMS s f
forall a. Annoted a -> a
item) [Annoted (SIG_ITEMS s f)]
l
    Var_items l :: [VAR_DECL]
l _ -> [CASL_SL a] -> CASL_SL a
forall a. Lattice a => [CASL_SL a] -> CASL_SL a
comp_list ([CASL_SL a] -> CASL_SL a) -> [CASL_SL a] -> CASL_SL a
forall a b. (a -> b) -> a -> b
$ (VAR_DECL -> CASL_SL a) -> [VAR_DECL] -> [CASL_SL a]
forall a b. (a -> b) -> [a] -> [b]
map VAR_DECL -> CASL_SL a
forall a. Lattice a => VAR_DECL -> CASL_SL a
sl_var_decl [VAR_DECL]
l
    Local_var_axioms d :: [VAR_DECL]
d l :: [Annoted (FORMULA f)]
l _ -> [CASL_SL a] -> CASL_SL a
forall a. Lattice a => [CASL_SL a] -> CASL_SL a
comp_list
        ([CASL_SL a] -> CASL_SL a) -> [CASL_SL a] -> CASL_SL a
forall a b. (a -> b) -> a -> b
$ (VAR_DECL -> CASL_SL a) -> [VAR_DECL] -> [CASL_SL a]
forall a b. (a -> b) -> [a] -> [b]
map VAR_DECL -> CASL_SL a
forall a. Lattice a => VAR_DECL -> CASL_SL a
sl_var_decl [VAR_DECL]
d [CASL_SL a] -> [CASL_SL a] -> [CASL_SL a]
forall a. [a] -> [a] -> [a]
++ (Annoted (FORMULA f) -> CASL_SL a)
-> [Annoted (FORMULA f)] -> [CASL_SL a]
forall a b. (a -> b) -> [a] -> [b]
map ((f -> CASL_SL a) -> FORMULA f -> CASL_SL a
forall a f. Lattice a => (f -> CASL_SL a) -> FORMULA f -> CASL_SL a
sl_formula f -> CASL_SL a
ff (FORMULA f -> CASL_SL a)
-> (Annoted (FORMULA f) -> FORMULA f)
-> Annoted (FORMULA f)
-> CASL_SL a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted (FORMULA f) -> FORMULA f
forall a. Annoted a -> a
item) [Annoted (FORMULA f)]
l
    Axiom_items l :: [Annoted (FORMULA f)]
l _ -> [CASL_SL a] -> CASL_SL a
forall a. Lattice a => [CASL_SL a] -> CASL_SL a
comp_list ([CASL_SL a] -> CASL_SL a) -> [CASL_SL a] -> CASL_SL a
forall a b. (a -> b) -> a -> b
$ (Annoted (FORMULA f) -> CASL_SL a)
-> [Annoted (FORMULA f)] -> [CASL_SL a]
forall a b. (a -> b) -> [a] -> [b]
map ((f -> CASL_SL a) -> FORMULA f -> CASL_SL a
forall a f. Lattice a => (f -> CASL_SL a) -> FORMULA f -> CASL_SL a
sl_formula f -> CASL_SL a
ff (FORMULA f -> CASL_SL a)
-> (Annoted (FORMULA f) -> FORMULA f)
-> Annoted (FORMULA f)
-> CASL_SL a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted (FORMULA f) -> FORMULA f
forall a. Annoted a -> a
item) [Annoted (FORMULA f)]
l
    Ext_BASIC_ITEMS b :: b
b -> b -> CASL_SL a
bf b
b

needsEmptySorts :: Lattice a => SortsKind -> CASL_SL a -> CASL_SL a
needsEmptySorts :: SortsKind -> CASL_SL a -> CASL_SL a
needsEmptySorts sk :: SortsKind
sk = case SortsKind
sk of
    NonEmptySorts -> CASL_SL a -> CASL_SL a
forall a. a -> a
id
    PossiblyEmptySorts -> CASL_SL a -> CASL_SL a -> CASL_SL a
forall a. Lattice a => CASL_SL a -> CASL_SL a -> CASL_SL a
sublogics_max CASL_SL a
forall a. Lattice a => CASL_SL a
need_empty_sorts

sl_sig_items :: Lattice a => (s -> CASL_SL a)
              -> (f -> CASL_SL a)
              -> SIG_ITEMS s f -> CASL_SL a
sl_sig_items :: (s -> CASL_SL a) -> (f -> CASL_SL a) -> SIG_ITEMS s f -> CASL_SL a
sl_sig_items sf :: s -> CASL_SL a
sf ff :: f -> CASL_SL a
ff si :: SIG_ITEMS s f
si = case SIG_ITEMS s f
si of
    Sort_items sk :: SortsKind
sk l :: [Annoted (SORT_ITEM f)]
l _ -> SortsKind -> CASL_SL a -> CASL_SL a
forall a. Lattice a => SortsKind -> CASL_SL a -> CASL_SL a
needsEmptySorts SortsKind
sk
          (CASL_SL a -> CASL_SL a) -> CASL_SL a -> CASL_SL a
forall a b. (a -> b) -> a -> b
$ [CASL_SL a] -> CASL_SL a
forall a. Lattice a => [CASL_SL a] -> CASL_SL a
comp_list ([CASL_SL a] -> CASL_SL a) -> [CASL_SL a] -> CASL_SL a
forall a b. (a -> b) -> a -> b
$ (Annoted (SORT_ITEM f) -> CASL_SL a)
-> [Annoted (SORT_ITEM f)] -> [CASL_SL a]
forall a b. (a -> b) -> [a] -> [b]
map ((f -> CASL_SL a) -> SORT_ITEM f -> CASL_SL a
forall a f.
Lattice a =>
(f -> CASL_SL a) -> SORT_ITEM f -> CASL_SL a
sl_sort_item f -> CASL_SL a
ff (SORT_ITEM f -> CASL_SL a)
-> (Annoted (SORT_ITEM f) -> SORT_ITEM f)
-> Annoted (SORT_ITEM f)
-> CASL_SL a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted (SORT_ITEM f) -> SORT_ITEM f
forall a. Annoted a -> a
item) [Annoted (SORT_ITEM f)]
l
    Op_items l :: [Annoted (OP_ITEM f)]
l _ -> [CASL_SL a] -> CASL_SL a
forall a. Lattice a => [CASL_SL a] -> CASL_SL a
comp_list ([CASL_SL a] -> CASL_SL a) -> [CASL_SL a] -> CASL_SL a
forall a b. (a -> b) -> a -> b
$ (Annoted (OP_ITEM f) -> CASL_SL a)
-> [Annoted (OP_ITEM f)] -> [CASL_SL a]
forall a b. (a -> b) -> [a] -> [b]
map ((f -> CASL_SL a) -> OP_ITEM f -> CASL_SL a
forall a f. Lattice a => (f -> CASL_SL a) -> OP_ITEM f -> CASL_SL a
sl_op_item f -> CASL_SL a
ff (OP_ITEM f -> CASL_SL a)
-> (Annoted (OP_ITEM f) -> OP_ITEM f)
-> Annoted (OP_ITEM f)
-> CASL_SL a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted (OP_ITEM f) -> OP_ITEM f
forall a. Annoted a -> a
item) [Annoted (OP_ITEM f)]
l
    Pred_items l :: [Annoted (PRED_ITEM f)]
l _ -> [CASL_SL a] -> CASL_SL a
forall a. Lattice a => [CASL_SL a] -> CASL_SL a
comp_list ([CASL_SL a] -> CASL_SL a) -> [CASL_SL a] -> CASL_SL a
forall a b. (a -> b) -> a -> b
$ (Annoted (PRED_ITEM f) -> CASL_SL a)
-> [Annoted (PRED_ITEM f)] -> [CASL_SL a]
forall a b. (a -> b) -> [a] -> [b]
map ((f -> CASL_SL a) -> PRED_ITEM f -> CASL_SL a
forall a f.
Lattice a =>
(f -> CASL_SL a) -> PRED_ITEM f -> CASL_SL a
sl_pred_item f -> CASL_SL a
ff (PRED_ITEM f -> CASL_SL a)
-> (Annoted (PRED_ITEM f) -> PRED_ITEM f)
-> Annoted (PRED_ITEM f)
-> CASL_SL a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted (PRED_ITEM f) -> PRED_ITEM f
forall a. Annoted a -> a
item) [Annoted (PRED_ITEM f)]
l
    Datatype_items sk :: SortsKind
sk l :: [Annoted DATATYPE_DECL]
l _ -> SortsKind -> CASL_SL a -> CASL_SL a
forall a. Lattice a => SortsKind -> CASL_SL a -> CASL_SL a
needsEmptySorts SortsKind
sk
          (CASL_SL a -> CASL_SL a) -> CASL_SL a -> CASL_SL a
forall a b. (a -> b) -> a -> b
$ [CASL_SL a] -> CASL_SL a
forall a. Lattice a => [CASL_SL a] -> CASL_SL a
comp_list ([CASL_SL a] -> CASL_SL a) -> [CASL_SL a] -> CASL_SL a
forall a b. (a -> b) -> a -> b
$ (Annoted DATATYPE_DECL -> CASL_SL a)
-> [Annoted DATATYPE_DECL] -> [CASL_SL a]
forall a b. (a -> b) -> [a] -> [b]
map (DATATYPE_DECL -> CASL_SL a
forall a. Lattice a => DATATYPE_DECL -> CASL_SL a
sl_datatype_decl (DATATYPE_DECL -> CASL_SL a)
-> (Annoted DATATYPE_DECL -> DATATYPE_DECL)
-> Annoted DATATYPE_DECL
-> CASL_SL a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted DATATYPE_DECL -> DATATYPE_DECL
forall a. Annoted a -> a
item) [Annoted DATATYPE_DECL]
l
    Ext_SIG_ITEMS s :: s
s -> s -> CASL_SL a
sf s
s

{- Subsort_defn needs to compute the expression logic needed seperately
because the expressiveness allowed in the formula may be different
from more general formulae in the same expression logic -}
sl_sort_item :: Lattice a => (f -> CASL_SL a)
             -> SORT_ITEM f -> CASL_SL a
sl_sort_item :: (f -> CASL_SL a) -> SORT_ITEM f -> CASL_SL a
sl_sort_item ff :: f -> CASL_SL a
ff si :: SORT_ITEM f
si = case SORT_ITEM f
si of
    Subsort_decl {} -> CASL_SL a
forall a. Lattice a => CASL_SL a
need_sul
    Subsort_defn _ _ _ f :: Annoted (FORMULA f)
f _ -> CASL_SL a -> CASL_SL a -> CASL_SL a
forall a. Lattice a => CASL_SL a -> CASL_SL a -> CASL_SL a
sublogics_max
                                        ((f -> CASL_SL a) -> FORMULA f -> CASL_SL a
forall a f. Lattice a => (f -> CASL_SL a) -> FORMULA f -> CASL_SL a
get_logic_sd f -> CASL_SL a
ff (FORMULA f -> CASL_SL a) -> FORMULA f -> CASL_SL a
forall a b. (a -> b) -> a -> b
$ Annoted (FORMULA f) -> FORMULA f
forall a. Annoted a -> a
item Annoted (FORMULA f)
f)
                                        (CASL_SL a -> CASL_SL a -> CASL_SL a
forall a. Lattice a => CASL_SL a -> CASL_SL a -> CASL_SL a
sublogics_max CASL_SL a
forall a. Lattice a => CASL_SL a
need_sul
                                        ((f -> CASL_SL a) -> FORMULA f -> CASL_SL a
forall a f. Lattice a => (f -> CASL_SL a) -> FORMULA f -> CASL_SL a
sl_formula f -> CASL_SL a
ff (FORMULA f -> CASL_SL a) -> FORMULA f -> CASL_SL a
forall a b. (a -> b) -> a -> b
$ Annoted (FORMULA f) -> FORMULA f
forall a. Annoted a -> a
item Annoted (FORMULA f)
f))
    Iso_decl _ _ -> CASL_SL a
forall a. Lattice a => CASL_SL a
need_sul
    _ -> CASL_SL a
forall a. Lattice a => CASL_SL a
bottom

sl_op_item :: Lattice a => (f -> CASL_SL a)
           -> OP_ITEM f -> CASL_SL a
sl_op_item :: (f -> CASL_SL a) -> OP_ITEM f -> CASL_SL a
sl_op_item ff :: f -> CASL_SL a
ff oi :: OP_ITEM f
oi = case OP_ITEM f
oi of
    Op_decl _ t :: OP_TYPE
t l :: [OP_ATTR f]
l _ -> CASL_SL a -> CASL_SL a -> CASL_SL a
forall a. Lattice a => CASL_SL a -> CASL_SL a -> CASL_SL a
sublogics_max (OP_TYPE -> CASL_SL a
forall a. Lattice a => OP_TYPE -> CASL_SL a
sl_op_type OP_TYPE
t)
                               ([CASL_SL a] -> CASL_SL a
forall a. Lattice a => [CASL_SL a] -> CASL_SL a
comp_list ([CASL_SL a] -> CASL_SL a) -> [CASL_SL a] -> CASL_SL a
forall a b. (a -> b) -> a -> b
$ (OP_ATTR f -> CASL_SL a) -> [OP_ATTR f] -> [CASL_SL a]
forall a b. (a -> b) -> [a] -> [b]
map ((f -> CASL_SL a) -> OP_ATTR f -> CASL_SL a
forall a f. Lattice a => (f -> CASL_SL a) -> OP_ATTR f -> CASL_SL a
sl_op_attr f -> CASL_SL a
ff) [OP_ATTR f]
l)
    Op_defn _ h :: OP_HEAD
h t :: Annoted (TERM f)
t _ -> CASL_SL a -> CASL_SL a -> CASL_SL a
forall a. Lattice a => CASL_SL a -> CASL_SL a -> CASL_SL a
sublogics_max (OP_HEAD -> CASL_SL a
forall a. Lattice a => OP_HEAD -> CASL_SL a
sl_op_head OP_HEAD
h)
                                             ((f -> CASL_SL a) -> TERM f -> CASL_SL a
forall a f. Lattice a => (f -> CASL_SL a) -> TERM f -> CASL_SL a
sl_term f -> CASL_SL a
ff (TERM f -> CASL_SL a) -> TERM f -> CASL_SL a
forall a b. (a -> b) -> a -> b
$ Annoted (TERM f) -> TERM f
forall a. Annoted a -> a
item Annoted (TERM f)
t)

sl_op_attr :: Lattice a => (f -> CASL_SL a)
           -> OP_ATTR f -> CASL_SL a
sl_op_attr :: (f -> CASL_SL a) -> OP_ATTR f -> CASL_SL a
sl_op_attr ff :: f -> CASL_SL a
ff oa :: OP_ATTR f
oa = case OP_ATTR f
oa of
    Unit_op_attr t :: TERM f
t -> (f -> CASL_SL a) -> TERM f -> CASL_SL a
forall a f. Lattice a => (f -> CASL_SL a) -> TERM f -> CASL_SL a
sl_term f -> CASL_SL a
ff TERM f
t
    _ -> CASL_SL a
forall a. Lattice a => CASL_SL a
need_eq

sl_op_type :: Lattice a => OP_TYPE -> CASL_SL a
sl_op_type :: OP_TYPE -> CASL_SL a
sl_op_type ot :: OP_TYPE
ot = case OP_TYPE
ot of
    Op_type Partial _ _ _ -> CASL_SL a
forall a. Lattice a => CASL_SL a
need_part
    _ -> CASL_SL a
forall a. Lattice a => CASL_SL a
bottom

sl_op_head :: Lattice a => OP_HEAD -> CASL_SL a
sl_op_head :: OP_HEAD -> CASL_SL a
sl_op_head oh :: OP_HEAD
oh = case OP_HEAD
oh of
    Op_head Partial _ _ _ -> CASL_SL a
forall a. Lattice a => CASL_SL a
need_part
    _ -> CASL_SL a
forall a. Lattice a => CASL_SL a
bottom

sl_pred_item :: Lattice a => (f -> CASL_SL a)
             -> PRED_ITEM f -> CASL_SL a
sl_pred_item :: (f -> CASL_SL a) -> PRED_ITEM f -> CASL_SL a
sl_pred_item ff :: f -> CASL_SL a
ff i :: PRED_ITEM f
i = case PRED_ITEM f
i of
    Pred_decl {} -> CASL_SL a
forall a. Lattice a => CASL_SL a
need_pred
    Pred_defn _ _ f :: Annoted (FORMULA f)
f _ -> CASL_SL a -> CASL_SL a -> CASL_SL a
forall a. Lattice a => CASL_SL a -> CASL_SL a -> CASL_SL a
sublogics_max CASL_SL a
forall a. Lattice a => CASL_SL a
need_pred ((f -> CASL_SL a) -> FORMULA f -> CASL_SL a
forall a f. Lattice a => (f -> CASL_SL a) -> FORMULA f -> CASL_SL a
sl_formula f -> CASL_SL a
ff (FORMULA f -> CASL_SL a) -> FORMULA f -> CASL_SL a
forall a b. (a -> b) -> a -> b
$ Annoted (FORMULA f) -> FORMULA f
forall a. Annoted a -> a
item Annoted (FORMULA f)
f)

sl_datatype_decl :: Lattice a => DATATYPE_DECL -> CASL_SL a
sl_datatype_decl :: DATATYPE_DECL -> CASL_SL a
sl_datatype_decl (Datatype_decl _ l :: [Annoted ALTERNATIVE]
l _) =
    [CASL_SL a] -> CASL_SL a
forall a. Lattice a => [CASL_SL a] -> CASL_SL a
comp_list ([CASL_SL a] -> CASL_SL a) -> [CASL_SL a] -> CASL_SL a
forall a b. (a -> b) -> a -> b
$ (Annoted ALTERNATIVE -> CASL_SL a)
-> [Annoted ALTERNATIVE] -> [CASL_SL a]
forall a b. (a -> b) -> [a] -> [b]
map (ALTERNATIVE -> CASL_SL a
forall a. Lattice a => ALTERNATIVE -> CASL_SL a
sl_alternative (ALTERNATIVE -> CASL_SL a)
-> (Annoted ALTERNATIVE -> ALTERNATIVE)
-> Annoted ALTERNATIVE
-> CASL_SL a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted ALTERNATIVE -> ALTERNATIVE
forall a. Annoted a -> a
item) [Annoted ALTERNATIVE]
l

sl_alternative :: Lattice a => ALTERNATIVE -> CASL_SL a
sl_alternative :: ALTERNATIVE -> CASL_SL a
sl_alternative a :: ALTERNATIVE
a = case ALTERNATIVE
a of
    Alt_construct Total _ l :: [COMPONENTS]
l _ -> [CASL_SL a] -> CASL_SL a
forall a. Lattice a => [CASL_SL a] -> CASL_SL a
comp_list ([CASL_SL a] -> CASL_SL a) -> [CASL_SL a] -> CASL_SL a
forall a b. (a -> b) -> a -> b
$ (COMPONENTS -> CASL_SL a) -> [COMPONENTS] -> [CASL_SL a]
forall a b. (a -> b) -> [a] -> [b]
map COMPONENTS -> CASL_SL a
forall a. Lattice a => COMPONENTS -> CASL_SL a
sl_components [COMPONENTS]
l
    Alt_construct Partial _ _ _ -> CASL_SL a
forall a. Lattice a => CASL_SL a
need_part
    Subsorts _ _ -> CASL_SL a
forall a. Lattice a => CASL_SL a
need_sul

sl_components :: Lattice a => COMPONENTS -> CASL_SL a
sl_components :: COMPONENTS -> CASL_SL a
sl_components c :: COMPONENTS
c = case COMPONENTS
c of
    Cons_select Partial _ _ _ -> CASL_SL a
forall a. Lattice a => CASL_SL a
need_part
    _ -> CASL_SL a
forall a. Lattice a => CASL_SL a
bottom

sl_var_decl :: Lattice a => VAR_DECL -> CASL_SL a
sl_var_decl :: VAR_DECL -> CASL_SL a
sl_var_decl _ = CASL_SL a
forall a. Lattice a => CASL_SL a
bottom

{- without subsorts casts are trivial and would not even require
   need_part, but testing sortOfTerm is not save for formulas in basic specs
   that are only parsed (and resolved) but not enriched with sorts -}

slRecord :: Lattice a => (f -> CASL_SL a) -> Record f (CASL_SL a) (CASL_SL a)
slRecord :: (f -> CASL_SL a) -> Record f (CASL_SL a) (CASL_SL a)
slRecord ff :: f -> CASL_SL a
ff = ((f -> CASL_SL a)
-> ([CASL_SL a] -> CASL_SL a)
-> CASL_SL a
-> Record f (CASL_SL a) (CASL_SL a)
forall f a. (f -> a) -> ([a] -> a) -> a -> Record f a a
constRecord f -> CASL_SL a
ff [CASL_SL a] -> CASL_SL a
forall a. Lattice a => [CASL_SL a] -> CASL_SL a
comp_list CASL_SL a
forall a. Lattice a => CASL_SL a
bottom)
  { foldPredication :: FORMULA f -> PRED_SYMB -> [CASL_SL a] -> Range -> CASL_SL a
foldPredication = \ _ _ l :: [CASL_SL a]
l _ -> [CASL_SL a] -> CASL_SL a
forall a. Lattice a => [CASL_SL a] -> CASL_SL a
comp_list ([CASL_SL a] -> CASL_SL a) -> [CASL_SL a] -> CASL_SL a
forall a b. (a -> b) -> a -> b
$ CASL_SL a
forall a. Lattice a => CASL_SL a
need_pred CASL_SL a -> [CASL_SL a] -> [CASL_SL a]
forall a. a -> [a] -> [a]
: [CASL_SL a]
l
  , foldEquation :: FORMULA f
-> CASL_SL a -> Equality -> CASL_SL a -> Range -> CASL_SL a
foldEquation = \ _ t :: CASL_SL a
t _ u :: CASL_SL a
u _ -> [CASL_SL a] -> CASL_SL a
forall a. Lattice a => [CASL_SL a] -> CASL_SL a
comp_list [CASL_SL a
forall a. Lattice a => CASL_SL a
need_eq, CASL_SL a
t, CASL_SL a
u]
  , foldSort_gen_ax :: FORMULA f -> [Constraint] -> Bool -> CASL_SL a
foldSort_gen_ax = \ _ constraints :: [Constraint]
constraints isFree :: Bool
isFree ->
      case [Constraint] -> ([SORT], [OP_SYMB], [(SORT, SORT)])
recover_Sort_gen_ax [Constraint]
constraints of
      (_, ops :: [OP_SYMB]
ops, m :: [(SORT, SORT)]
m) -> let
        ojc :: Bool
ojc = (OP_SYMB -> Bool) -> [OP_SYMB] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all OP_SYMB -> Bool
isInjOp [OP_SYMB]
ops
        tc :: SortGenTotality
tc = if Bool
isFree
                then SortGenTotality
OnlyFree
                else if (OP_SYMB -> Bool) -> [OP_SYMB] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all OP_SYMB -> Bool
isTotalOp [OP_SYMB]
ops
                        then SortGenTotality
OnlyTotal
                        else SortGenTotality
SomePartial
        in Bool -> Bool -> SortGenTotality -> CASL_SL a
forall a. Lattice a => Bool -> Bool -> SortGenTotality -> CASL_SL a
need_cons ([(SORT, SORT)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(SORT, SORT)]
m) Bool
ojc SortGenTotality
tc where
          isInjOp :: OP_SYMB -> Bool
isInjOp (Qual_op_name n :: SORT
n _ _) = SORT -> Bool
isInjName SORT
n
          isInjOp _ = Bool
False
          isTotalOp :: OP_SYMB -> Bool
isTotalOp (Qual_op_name _ (Op_type Total _ _ _) _) = Bool
True
          isTotalOp _ = Bool
False
  , foldQuantPred :: FORMULA f -> SORT -> PRED_TYPE -> CASL_SL a -> CASL_SL a
foldQuantPred = \ _ _ _ f :: CASL_SL a
f -> CASL_SL a -> CASL_SL a -> CASL_SL a
forall a. Lattice a => CASL_SL a -> CASL_SL a -> CASL_SL a
sublogics_max CASL_SL a
forall a. Lattice a => CASL_SL a
need_pred CASL_SL a
f
  , foldCast :: TERM f -> CASL_SL a -> SORT -> Range -> CASL_SL a
foldCast = \ _ t :: CASL_SL a
t _ _ -> CASL_SL a -> CASL_SL a -> CASL_SL a
forall a. Lattice a => CASL_SL a -> CASL_SL a -> CASL_SL a
sublogics_max CASL_SL a
forall a. Lattice a => CASL_SL a
need_part CASL_SL a
t
  }

sl_term :: Lattice a => (f -> CASL_SL a) -> TERM f -> CASL_SL a
sl_term :: (f -> CASL_SL a) -> TERM f -> CASL_SL a
sl_term = Record f (CASL_SL a) (CASL_SL a) -> TERM f -> CASL_SL a
forall f a b. Record f a b -> TERM f -> b
foldTerm (Record f (CASL_SL a) (CASL_SL a) -> TERM f -> CASL_SL a)
-> ((f -> CASL_SL a) -> Record f (CASL_SL a) (CASL_SL a))
-> (f -> CASL_SL a)
-> TERM f
-> CASL_SL a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f -> CASL_SL a) -> Record f (CASL_SL a) (CASL_SL a)
forall a f.
Lattice a =>
(f -> CASL_SL a) -> Record f (CASL_SL a) (CASL_SL a)
slRecord

sl_formula :: Lattice a => (f -> CASL_SL a)
           -> FORMULA f -> CASL_SL a
sl_formula :: (f -> CASL_SL a) -> FORMULA f -> CASL_SL a
sl_formula ff :: f -> CASL_SL a
ff f :: FORMULA f
f = CASL_SL a -> CASL_SL a -> CASL_SL a
forall a. Lattice a => CASL_SL a -> CASL_SL a -> CASL_SL a
sublogics_max ((f -> CASL_SL a) -> FORMULA f -> CASL_SL a
forall a f. Lattice a => (f -> CASL_SL a) -> FORMULA f -> CASL_SL a
get_logic f -> CASL_SL a
ff FORMULA f
f) ((f -> CASL_SL a) -> FORMULA f -> CASL_SL a
forall a f. Lattice a => (f -> CASL_SL a) -> FORMULA f -> CASL_SL a
sl_form f -> CASL_SL a
ff FORMULA f
f)

sl_form :: Lattice a => (f -> CASL_SL a)
        -> FORMULA f -> CASL_SL a
sl_form :: (f -> CASL_SL a) -> FORMULA f -> CASL_SL a
sl_form = Record f (CASL_SL a) (CASL_SL a) -> FORMULA f -> CASL_SL a
forall f a b. Record f a b -> FORMULA f -> a
foldFormula (Record f (CASL_SL a) (CASL_SL a) -> FORMULA f -> CASL_SL a)
-> ((f -> CASL_SL a) -> Record f (CASL_SL a) (CASL_SL a))
-> (f -> CASL_SL a)
-> FORMULA f
-> CASL_SL a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f -> CASL_SL a) -> Record f (CASL_SL a) (CASL_SL a)
forall a f.
Lattice a =>
(f -> CASL_SL a) -> Record f (CASL_SL a) (CASL_SL a)
slRecord

sl_symb_items :: Lattice a => SYMB_ITEMS -> CASL_SL a
sl_symb_items :: SYMB_ITEMS -> CASL_SL a
sl_symb_items (Symb_items k :: SYMB_KIND
k l :: [SYMB]
l _) = CASL_SL a -> CASL_SL a -> CASL_SL a
forall a. Lattice a => CASL_SL a -> CASL_SL a -> CASL_SL a
sublogics_max (SYMB_KIND -> CASL_SL a
forall a. Lattice a => SYMB_KIND -> CASL_SL a
sl_symb_kind SYMB_KIND
k)
                                   ([CASL_SL a] -> CASL_SL a
forall a. Lattice a => [CASL_SL a] -> CASL_SL a
comp_list ([CASL_SL a] -> CASL_SL a) -> [CASL_SL a] -> CASL_SL a
forall a b. (a -> b) -> a -> b
$ (SYMB -> CASL_SL a) -> [SYMB] -> [CASL_SL a]
forall a b. (a -> b) -> [a] -> [b]
map SYMB -> CASL_SL a
forall a. Lattice a => SYMB -> CASL_SL a
sl_symb [SYMB]
l)

sl_symb_kind :: Lattice a => SYMB_KIND -> CASL_SL a
sl_symb_kind :: SYMB_KIND -> CASL_SL a
sl_symb_kind pk :: SYMB_KIND
pk = case SYMB_KIND
pk of
    Preds_kind -> CASL_SL a
forall a. Lattice a => CASL_SL a
need_pred
    _ -> CASL_SL a
forall a. Lattice a => CASL_SL a
bottom

sl_symb :: Lattice a => SYMB -> CASL_SL a
sl_symb :: SYMB -> CASL_SL a
sl_symb s :: SYMB
s = case SYMB
s of
    Symb_id _ -> CASL_SL a
forall a. Lattice a => CASL_SL a
bottom
    Qual_id _ t :: TYPE
t _ -> TYPE -> CASL_SL a
forall a. Lattice a => TYPE -> CASL_SL a
sl_type TYPE
t

sl_type :: Lattice a => TYPE -> CASL_SL a
sl_type :: TYPE -> CASL_SL a
sl_type ty :: TYPE
ty = case TYPE
ty of
    O_type t :: OP_TYPE
t -> OP_TYPE -> CASL_SL a
forall a. Lattice a => OP_TYPE -> CASL_SL a
sl_op_type OP_TYPE
t
    P_type _ -> CASL_SL a
forall a. Lattice a => CASL_SL a
need_pred
    _ -> CASL_SL a
forall a. Lattice a => CASL_SL a
bottom

sl_symb_map_items :: Lattice a => SYMB_MAP_ITEMS -> CASL_SL a
sl_symb_map_items :: SYMB_MAP_ITEMS -> CASL_SL a
sl_symb_map_items (Symb_map_items k :: SYMB_KIND
k l :: [SYMB_OR_MAP]
l _) = CASL_SL a -> CASL_SL a -> CASL_SL a
forall a. Lattice a => CASL_SL a -> CASL_SL a -> CASL_SL a
sublogics_max (SYMB_KIND -> CASL_SL a
forall a. Lattice a => SYMB_KIND -> CASL_SL a
sl_symb_kind SYMB_KIND
k)
                                          ([CASL_SL a] -> CASL_SL a
forall a. Lattice a => [CASL_SL a] -> CASL_SL a
comp_list ([CASL_SL a] -> CASL_SL a) -> [CASL_SL a] -> CASL_SL a
forall a b. (a -> b) -> a -> b
$ (SYMB_OR_MAP -> CASL_SL a) -> [SYMB_OR_MAP] -> [CASL_SL a]
forall a b. (a -> b) -> [a] -> [b]
map SYMB_OR_MAP -> CASL_SL a
forall a. Lattice a => SYMB_OR_MAP -> CASL_SL a
sl_symb_or_map [SYMB_OR_MAP]
l)

sl_symb_or_map :: Lattice a => SYMB_OR_MAP -> CASL_SL a
sl_symb_or_map :: SYMB_OR_MAP -> CASL_SL a
sl_symb_or_map syms :: SYMB_OR_MAP
syms = case SYMB_OR_MAP
syms of
    Symb s :: SYMB
s -> SYMB -> CASL_SL a
forall a. Lattice a => SYMB -> CASL_SL a
sl_symb SYMB
s
    Symb_map s :: SYMB
s t :: SYMB
t _ -> CASL_SL a -> CASL_SL a -> CASL_SL a
forall a. Lattice a => CASL_SL a -> CASL_SL a -> CASL_SL a
sublogics_max (SYMB -> CASL_SL a
forall a. Lattice a => SYMB -> CASL_SL a
sl_symb SYMB
s) (SYMB -> CASL_SL a
forall a. Lattice a => SYMB -> CASL_SL a
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_sign :: Lattice a => (e -> CASL_SL a) -> Sign f e -> CASL_SL a
sl_sign :: (e -> CASL_SL a) -> Sign f e -> CASL_SL a
sl_sign f :: e -> CASL_SL a
f s :: Sign f e
s =
    let rel :: Rel SORT
rel = Sign f e -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel Sign f e
s
        subs :: CASL_SL a
subs | Rel SORT -> Bool
forall a. Ord a => Rel a -> Bool
Rel.noPairs Rel SORT
rel = CASL_SL a
forall a. Lattice a => CASL_SL a
bottom
             | Rel SORT -> Bool
forall a. Ord a => Rel a -> Bool
Rel.locallyFiltered Rel SORT
rel = CASL_SL a
forall a. Lattice a => CASL_SL a
need_sul
             | Bool
otherwise = CASL_SL a
forall a. Lattice a => CASL_SL a
need_sub
        esorts :: CASL_SL a
esorts = if Set SORT -> Bool
forall a. Set a -> Bool
Set.null (Set SORT -> Bool) -> Set SORT -> Bool
forall a b. (a -> b) -> a -> b
$ Sign f e -> Set SORT
forall f e. Sign f e -> Set SORT
emptySortSet Sign f e
s then CASL_SL a
forall a. Lattice a => CASL_SL a
bottom
                 else CASL_SL a
forall a. Lattice a => CASL_SL a
need_empty_sorts
        preds :: CASL_SL a
preds = if MapSet SORT PredType -> Bool
forall a b. MapSet a b -> Bool
MapSet.null (MapSet SORT PredType -> Bool) -> MapSet SORT PredType -> Bool
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet SORT PredType
forall f e. Sign f e -> MapSet SORT PredType
predMap Sign f e
s then CASL_SL a
forall a. Lattice a => CASL_SL a
bottom else CASL_SL a
forall a. Lattice a => CASL_SL a
need_pred
        partial :: CASL_SL a
partial = if (OpType -> Bool) -> [OpType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any OpType -> Bool
isPartial ([OpType] -> Bool) -> [OpType] -> Bool
forall a b. (a -> b) -> a -> b
$ Set OpType -> [OpType]
forall a. Set a -> [a]
Set.toList
                  (Set OpType -> [OpType]) -> Set OpType -> [OpType]
forall a b. (a -> b) -> a -> b
$ MapSet SORT OpType -> Set OpType
forall b a. Ord b => MapSet a b -> Set b
MapSet.elems (MapSet SORT OpType -> Set OpType)
-> MapSet SORT OpType -> Set OpType
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet SORT OpType
forall f e. Sign f e -> MapSet SORT OpType
opMap Sign f e
s then CASL_SL a
forall a. Lattice a => CASL_SL a
need_part else CASL_SL a
forall a. Lattice a => CASL_SL a
bottom
        in [CASL_SL a] -> CASL_SL a
forall a. Lattice a => [CASL_SL a] -> CASL_SL a
comp_list [CASL_SL a
subs, CASL_SL a
esorts, CASL_SL a
preds, CASL_SL a
partial, e -> CASL_SL a
f (e -> CASL_SL a) -> e -> CASL_SL a
forall a b. (a -> b) -> a -> b
$ Sign f e -> e
forall f e. Sign f e -> e
extendedInfo Sign f e
s]

sl_sentence :: Lattice a => (f -> CASL_SL a) -> FORMULA f -> CASL_SL a
sl_sentence :: (f -> CASL_SL a) -> FORMULA f -> CASL_SL a
sl_sentence = (f -> CASL_SL a) -> FORMULA f -> CASL_SL a
forall a f. Lattice a => (f -> CASL_SL a) -> FORMULA f -> CASL_SL a
sl_formula

sl_morphism :: Lattice a => (e -> CASL_SL a) -> Morphism f e m -> CASL_SL a
sl_morphism :: (e -> CASL_SL a) -> Morphism f e m -> CASL_SL a
sl_morphism f :: e -> CASL_SL a
f m :: Morphism f e m
m = CASL_SL a -> CASL_SL a -> CASL_SL a
forall a. Lattice a => CASL_SL a -> CASL_SL a -> CASL_SL a
sublogics_max ((e -> CASL_SL a) -> Sign f e -> CASL_SL a
forall a e f.
Lattice a =>
(e -> CASL_SL a) -> Sign f e -> CASL_SL a
sl_sign e -> CASL_SL a
f (Sign f e -> CASL_SL a) -> Sign f e -> CASL_SL a
forall a b. (a -> b) -> a -> b
$ Morphism f e m -> Sign f e
forall f e m. Morphism f e m -> Sign f e
msource Morphism f e m
m) ((e -> CASL_SL a) -> Sign f e -> CASL_SL a
forall a e f.
Lattice a =>
(e -> CASL_SL a) -> Sign f e -> CASL_SL a
sl_sign e -> CASL_SL a
f (Sign f e -> CASL_SL a) -> Sign f e -> CASL_SL a
forall a b. (a -> b) -> a -> b
$ Morphism f e m -> Sign f e
forall f e m. Morphism f e m -> Sign f e
mtarget Morphism f e m
m)

sl_symbol :: Lattice a => Symbol -> CASL_SL a
sl_symbol :: Symbol -> CASL_SL a
sl_symbol (Symbol _ t :: SymbType
t) = SymbType -> CASL_SL a
forall a. Lattice a => SymbType -> CASL_SL a
sl_symbtype SymbType
t

sl_symbtype :: Lattice a => SymbType -> CASL_SL a
sl_symbtype :: SymbType -> CASL_SL a
sl_symbtype st :: SymbType
st = case SymbType
st of
    OpAsItemType t :: OpType
t -> OpType -> CASL_SL a
forall a. Lattice a => OpType -> CASL_SL a
sl_optype OpType
t
    PredAsItemType _ -> CASL_SL a
forall a. Lattice a => CASL_SL a
need_pred
    _ -> CASL_SL a
forall a. Lattice a => CASL_SL a
bottom

sl_optype :: Lattice a => OpType -> CASL_SL a
sl_optype :: OpType -> CASL_SL a
sl_optype = OpKind -> CASL_SL a
forall a. Lattice a => OpKind -> CASL_SL a
sl_opkind (OpKind -> CASL_SL a) -> (OpType -> OpKind) -> OpType -> CASL_SL a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OpType -> OpKind
opKind

sl_opkind :: Lattice a => OpKind -> CASL_SL a
sl_opkind :: OpKind -> CASL_SL a
sl_opkind fk :: OpKind
fk = case OpKind
fk of
    Partial -> CASL_SL a
forall a. Lattice a => CASL_SL a
need_part
    _ -> CASL_SL a
forall a. Lattice a => CASL_SL a
bottom

{- ----------------------------------------------------------------------------
projection functions
---------------------------------------------------------------------------- -}

sl_in :: Lattice a => CASL_SL a -> CASL_SL a -> Bool
sl_in :: CASL_SL a -> CASL_SL a -> Bool
sl_in given :: CASL_SL a
given new :: CASL_SL a
new = CASL_SL a -> CASL_SL a -> CASL_SL a
forall a. Lattice a => CASL_SL a -> CASL_SL a -> CASL_SL a
sublogics_max CASL_SL a
given CASL_SL a
new CASL_SL a -> CASL_SL a -> Bool
forall a. Eq a => a -> a -> Bool
== CASL_SL a
given

in_x :: Lattice a => CASL_SL a -> b -> (b -> CASL_SL a) -> Bool
in_x :: CASL_SL a -> b -> (b -> CASL_SL a) -> Bool
in_x l :: CASL_SL a
l x :: b
x f :: b -> CASL_SL a
f = CASL_SL a -> CASL_SL a -> Bool
forall a. Lattice a => CASL_SL a -> CASL_SL a -> Bool
sl_in CASL_SL a
l (b -> CASL_SL a
f b
x)

-- process Annoted type like simple type, simply keep all annos
pr_annoted :: CASL_SL s -> (CASL_SL s -> a -> Maybe a)
              -> Annoted a -> Maybe (Annoted a)
pr_annoted :: CASL_SL s
-> (CASL_SL s -> a -> Maybe a) -> Annoted a -> Maybe (Annoted a)
pr_annoted sl :: CASL_SL s
sl f :: CASL_SL s -> a -> Maybe a
f a :: Annoted a
a =
  (a -> Annoted a) -> Maybe a -> Maybe (Annoted a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (a -> Annoted a -> Annoted a
forall b a. b -> Annoted a -> Annoted b
`replaceAnnoted` Annoted a
a) (Maybe a -> Maybe (Annoted a)) -> Maybe a -> Maybe (Annoted a)
forall a b. (a -> b) -> a -> b
$ CASL_SL s -> a -> Maybe a
f CASL_SL s
sl (Annoted a -> a
forall a. Annoted a -> a
item Annoted a
a)

{- project annoted type, by-producing a [SORT]
used for projecting datatypes: sometimes it is necessary to
introduce a SORT_DEFN for a datatype that was erased
completely, for example by only having partial constructors
and partiality forbidden in the desired sublogic - the sort
name may however still be needed for formulas because it can
appear there like in (forall x,y:Datatype . x=x), a formula
that does not use partiality (does not use any constructor
or selector) -}
pr_annoted_dt :: CASL_SL s
              -> (CASL_SL s -> a -> (Maybe a, [SORT]))
              -> Annoted a -> (Maybe (Annoted a), [SORT])
pr_annoted_dt :: CASL_SL s
-> (CASL_SL s -> a -> (Maybe a, [SORT]))
-> Annoted a
-> (Maybe (Annoted a), [SORT])
pr_annoted_dt sl :: CASL_SL s
sl f :: CASL_SL s -> a -> (Maybe a, [SORT])
f a :: Annoted a
a =
    let (res :: Maybe a
res, lst :: [SORT]
lst) = CASL_SL s -> a -> (Maybe a, [SORT])
f CASL_SL s
sl (Annoted a -> a
forall a. Annoted a -> a
item Annoted a
a)
    in ((a -> Annoted a) -> Maybe a -> Maybe (Annoted a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (a -> Annoted a -> Annoted a
forall b a. b -> Annoted a -> Annoted b
`replaceAnnoted` Annoted a
a) Maybe a
res
       , [SORT]
lst)

-- keep an element if its computed sublogic is in the given sublogic
pr_check :: Lattice a => CASL_SL a -> (b -> CASL_SL a)
         -> b -> Maybe b
pr_check :: CASL_SL a -> (b -> CASL_SL a) -> b -> Maybe b
pr_check l :: CASL_SL a
l f :: b -> CASL_SL a
f e :: b
e = if CASL_SL a -> b -> (b -> CASL_SL a) -> Bool
forall a b. Lattice a => CASL_SL a -> b -> (b -> CASL_SL a) -> Bool
in_x CASL_SL a
l b
e b -> CASL_SL a
f then b -> Maybe b
forall a. a -> Maybe a
Just b
e else Maybe b
forall a. Maybe a
Nothing

checkRecord :: CASL_SL a -> (CASL_SL a -> f -> Maybe (FORMULA f))
            -> Record f (FORMULA f) (TERM f)
checkRecord :: CASL_SL a
-> (CASL_SL a -> f -> Maybe (FORMULA f))
-> Record f (FORMULA f) (TERM f)
checkRecord l :: CASL_SL a
l ff :: CASL_SL a -> f -> Maybe (FORMULA f)
ff = ((f -> f) -> Record f (FORMULA f) (TERM f)
forall f g. (f -> g) -> Record f (FORMULA g) (TERM g)
mapRecord f -> f
forall a. a -> a
id)
          { foldExtFORMULA :: FORMULA f -> f -> FORMULA f
foldExtFORMULA = \ o :: FORMULA f
o _ -> case FORMULA f
o of
              ExtFORMULA f :: f
f -> FORMULA f -> Maybe (FORMULA f) -> FORMULA f
forall a. a -> Maybe a -> a
fromMaybe (String -> FORMULA f
forall a. HasCallStack => String -> a
error "checkRecord") (Maybe (FORMULA f) -> FORMULA f) -> Maybe (FORMULA f) -> FORMULA f
forall a b. (a -> b) -> a -> b
$ CASL_SL a -> f -> Maybe (FORMULA f)
ff CASL_SL a
l f
f
              _ -> String -> FORMULA f
forall a. HasCallStack => String -> a
error "checkRecord.foldExtFORMULA" }

toCheck :: Lattice a => CASL_SL a
        -> (CASL_SL a -> f -> Maybe (FORMULA f))
        -> f -> CASL_SL a
toCheck :: CASL_SL a
-> (CASL_SL a -> f -> Maybe (FORMULA f)) -> f -> CASL_SL a
toCheck l :: CASL_SL a
l ff :: CASL_SL a -> f -> Maybe (FORMULA f)
ff = CASL_SL a
-> (FORMULA f -> CASL_SL a) -> Maybe (FORMULA f) -> CASL_SL a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe CASL_SL a
forall a. Lattice a => CASL_SL a
top (CASL_SL a -> FORMULA f -> CASL_SL a
forall a b. a -> b -> a
const CASL_SL a
l) (Maybe (FORMULA f) -> CASL_SL a)
-> (f -> Maybe (FORMULA f)) -> f -> CASL_SL a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CASL_SL a -> f -> Maybe (FORMULA f)
ff CASL_SL a
l

pr_formula :: Lattice a => (CASL_SL a -> f -> Maybe (FORMULA f))
           -> CASL_SL a -> FORMULA f -> Maybe (FORMULA f)
pr_formula :: (CASL_SL a -> f -> Maybe (FORMULA f))
-> CASL_SL a -> FORMULA f -> Maybe (FORMULA f)
pr_formula ff :: CASL_SL a -> f -> Maybe (FORMULA f)
ff l :: CASL_SL a
l =
    (FORMULA f -> FORMULA f) -> Maybe (FORMULA f) -> Maybe (FORMULA f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Record f (FORMULA f) (TERM f) -> FORMULA f -> FORMULA f
forall f a b. Record f a b -> FORMULA f -> a
foldFormula (Record f (FORMULA f) (TERM f) -> FORMULA f -> FORMULA f)
-> Record f (FORMULA f) (TERM f) -> FORMULA f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ CASL_SL a
-> (CASL_SL a -> f -> Maybe (FORMULA f))
-> Record f (FORMULA f) (TERM f)
forall a f.
CASL_SL a
-> (CASL_SL a -> f -> Maybe (FORMULA f))
-> Record f (FORMULA f) (TERM f)
checkRecord CASL_SL a
l CASL_SL a -> f -> Maybe (FORMULA f)
ff)
    (Maybe (FORMULA f) -> Maybe (FORMULA f))
-> (FORMULA f -> Maybe (FORMULA f))
-> FORMULA f
-> Maybe (FORMULA f)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CASL_SL a
-> (FORMULA f -> CASL_SL a) -> FORMULA f -> Maybe (FORMULA f)
forall a b.
Lattice a =>
CASL_SL a -> (b -> CASL_SL a) -> b -> Maybe b
pr_check CASL_SL a
l ((f -> CASL_SL a) -> FORMULA f -> CASL_SL a
forall a f. Lattice a => (f -> CASL_SL a) -> FORMULA f -> CASL_SL a
sl_formula ((f -> CASL_SL a) -> FORMULA f -> CASL_SL a)
-> (f -> CASL_SL a) -> FORMULA f -> CASL_SL a
forall a b. (a -> b) -> a -> b
$ CASL_SL a
-> (CASL_SL a -> f -> Maybe (FORMULA f)) -> f -> CASL_SL a
forall a f.
Lattice a =>
CASL_SL a
-> (CASL_SL a -> f -> Maybe (FORMULA f)) -> f -> CASL_SL a
toCheck CASL_SL a
l CASL_SL a -> f -> Maybe (FORMULA f)
ff)

pr_term :: Lattice a => (CASL_SL a -> f -> Maybe (FORMULA f))
        -> CASL_SL a -> TERM f -> Maybe (TERM f)
pr_term :: (CASL_SL a -> f -> Maybe (FORMULA f))
-> CASL_SL a -> TERM f -> Maybe (TERM f)
pr_term ff :: CASL_SL a -> f -> Maybe (FORMULA f)
ff l :: CASL_SL a
l =
    (TERM f -> TERM f) -> Maybe (TERM f) -> Maybe (TERM f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Record f (FORMULA f) (TERM f) -> TERM f -> TERM f
forall f a b. Record f a b -> TERM f -> b
foldTerm (Record f (FORMULA f) (TERM f) -> TERM f -> TERM f)
-> Record f (FORMULA f) (TERM f) -> TERM f -> TERM f
forall a b. (a -> b) -> a -> b
$ CASL_SL a
-> (CASL_SL a -> f -> Maybe (FORMULA f))
-> Record f (FORMULA f) (TERM f)
forall a f.
CASL_SL a
-> (CASL_SL a -> f -> Maybe (FORMULA f))
-> Record f (FORMULA f) (TERM f)
checkRecord CASL_SL a
l CASL_SL a -> f -> Maybe (FORMULA f)
ff)
    (Maybe (TERM f) -> Maybe (TERM f))
-> (TERM f -> Maybe (TERM f)) -> TERM f -> Maybe (TERM f)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CASL_SL a -> (TERM f -> CASL_SL a) -> TERM f -> Maybe (TERM f)
forall a b.
Lattice a =>
CASL_SL a -> (b -> CASL_SL a) -> b -> Maybe b
pr_check CASL_SL a
l ((f -> CASL_SL a) -> TERM f -> CASL_SL a
forall a f. Lattice a => (f -> CASL_SL a) -> TERM f -> CASL_SL a
sl_term ((f -> CASL_SL a) -> TERM f -> CASL_SL a)
-> (f -> CASL_SL a) -> TERM f -> CASL_SL a
forall a b. (a -> b) -> a -> b
$ CASL_SL a
-> (CASL_SL a -> f -> Maybe (FORMULA f)) -> f -> CASL_SL a
forall a f.
Lattice a =>
CASL_SL a
-> (CASL_SL a -> f -> Maybe (FORMULA f)) -> f -> CASL_SL a
toCheck CASL_SL a
l CASL_SL a -> f -> Maybe (FORMULA f)
ff)

-- make full Annoted Sig_items out of a SORT list
pr_make_sorts :: [SORT] -> Annoted (BASIC_ITEMS b s f)
pr_make_sorts :: [SORT] -> Annoted (BASIC_ITEMS b s f)
pr_make_sorts s :: [SORT]
s =
  BASIC_ITEMS b s f
-> Range
-> [Annotation]
-> [Annotation]
-> Annoted (BASIC_ITEMS b s f)
forall a. a -> Range -> [Annotation] -> [Annotation] -> Annoted a
Annoted (SIG_ITEMS s f -> BASIC_ITEMS b s f
forall b s f. SIG_ITEMS s f -> BASIC_ITEMS b s f
Sig_items (SortsKind -> [Annoted (SORT_ITEM f)] -> Range -> SIG_ITEMS s f
forall s f.
SortsKind -> [Annoted (SORT_ITEM f)] -> Range -> SIG_ITEMS s f
Sort_items SortsKind
NonEmptySorts
             [SORT_ITEM f
-> Range -> [Annotation] -> [Annotation] -> Annoted (SORT_ITEM f)
forall a. a -> Range -> [Annotation] -> [Annotation] -> Annoted a
Annoted ([SORT] -> Range -> SORT_ITEM f
forall f. [SORT] -> Range -> SORT_ITEM f
Sort_decl [SORT]
s Range
nullRange) Range
nullRange [] []]
             Range
nullRange))
          Range
nullRange [] []

{- when processing BASIC_SPEC, add a Sort_decl in front for sorts
defined by DATATYPE_DECLs that had to be removed completely,
otherwise formulas might be broken by the missing sorts, thus
breaking the projection -}
pr_basic_spec :: Lattice a =>
                 (CASL_SL a -> b -> (Maybe (BASIC_ITEMS b s f), [SORT]))
              -> (CASL_SL a -> s -> (Maybe (SIG_ITEMS s f), [SORT]))
              -> (CASL_SL a -> f -> Maybe (FORMULA f))
              -> CASL_SL a -> BASIC_SPEC b s f -> BASIC_SPEC b s f
pr_basic_spec :: (CASL_SL a -> b -> (Maybe (BASIC_ITEMS b s f), [SORT]))
-> (CASL_SL a -> s -> (Maybe (SIG_ITEMS s f), [SORT]))
-> (CASL_SL a -> f -> Maybe (FORMULA f))
-> CASL_SL a
-> BASIC_SPEC b s f
-> BASIC_SPEC b s f
pr_basic_spec fb :: CASL_SL a -> b -> (Maybe (BASIC_ITEMS b s f), [SORT])
fb fs :: CASL_SL a -> s -> (Maybe (SIG_ITEMS s f), [SORT])
fs ff :: CASL_SL a -> f -> Maybe (FORMULA f)
ff l :: CASL_SL a
l (Basic_spec s :: [Annoted (BASIC_ITEMS b s f)]
s) =
  let
    res :: [(Maybe (Annoted (BASIC_ITEMS b s f)), [SORT])]
res = (Annoted (BASIC_ITEMS b s f)
 -> (Maybe (Annoted (BASIC_ITEMS b s f)), [SORT]))
-> [Annoted (BASIC_ITEMS b s f)]
-> [(Maybe (Annoted (BASIC_ITEMS b s f)), [SORT])]
forall a b. (a -> b) -> [a] -> [b]
map (CASL_SL a
-> (CASL_SL a
    -> BASIC_ITEMS b s f -> (Maybe (BASIC_ITEMS b s f), [SORT]))
-> Annoted (BASIC_ITEMS b s f)
-> (Maybe (Annoted (BASIC_ITEMS b s f)), [SORT])
forall s a.
CASL_SL s
-> (CASL_SL s -> a -> (Maybe a, [SORT]))
-> Annoted a
-> (Maybe (Annoted a), [SORT])
pr_annoted_dt CASL_SL a
l ((CASL_SL a
  -> BASIC_ITEMS b s f -> (Maybe (BASIC_ITEMS b s f), [SORT]))
 -> Annoted (BASIC_ITEMS b s f)
 -> (Maybe (Annoted (BASIC_ITEMS b s f)), [SORT]))
-> (CASL_SL a
    -> BASIC_ITEMS b s f -> (Maybe (BASIC_ITEMS b s f), [SORT]))
-> Annoted (BASIC_ITEMS b s f)
-> (Maybe (Annoted (BASIC_ITEMS b s f)), [SORT])
forall a b. (a -> b) -> a -> b
$ (CASL_SL a -> b -> (Maybe (BASIC_ITEMS b s f), [SORT]))
-> (CASL_SL a -> s -> (Maybe (SIG_ITEMS s f), [SORT]))
-> (CASL_SL a -> f -> Maybe (FORMULA f))
-> CASL_SL a
-> BASIC_ITEMS b s f
-> (Maybe (BASIC_ITEMS b s f), [SORT])
forall a b s f.
Lattice a =>
(CASL_SL a -> b -> (Maybe (BASIC_ITEMS b s f), [SORT]))
-> (CASL_SL a -> s -> (Maybe (SIG_ITEMS s f), [SORT]))
-> (CASL_SL a -> f -> Maybe (FORMULA f))
-> CASL_SL a
-> BASIC_ITEMS b s f
-> (Maybe (BASIC_ITEMS b s f), [SORT])
pr_basic_items CASL_SL a -> b -> (Maybe (BASIC_ITEMS b s f), [SORT])
fb CASL_SL a -> s -> (Maybe (SIG_ITEMS s f), [SORT])
fs CASL_SL a -> f -> Maybe (FORMULA f)
ff) [Annoted (BASIC_ITEMS b s f)]
s
    items :: [Annoted (BASIC_ITEMS b s f)]
items = ((Maybe (Annoted (BASIC_ITEMS b s f)), [SORT])
 -> Maybe (Annoted (BASIC_ITEMS b s f)))
-> [(Maybe (Annoted (BASIC_ITEMS b s f)), [SORT])]
-> [Annoted (BASIC_ITEMS b s f)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Maybe (Annoted (BASIC_ITEMS b s f)), [SORT])
-> Maybe (Annoted (BASIC_ITEMS b s f))
forall a b. (a, b) -> a
fst [(Maybe (Annoted (BASIC_ITEMS b s f)), [SORT])]
res
    toAdd :: [SORT]
toAdd = ((Maybe (Annoted (BASIC_ITEMS b s f)), [SORT]) -> [SORT])
-> [(Maybe (Annoted (BASIC_ITEMS b s f)), [SORT])] -> [SORT]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Maybe (Annoted (BASIC_ITEMS b s f)), [SORT]) -> [SORT]
forall a b. (a, b) -> b
snd [(Maybe (Annoted (BASIC_ITEMS b s f)), [SORT])]
res
    ret :: [Annoted (BASIC_ITEMS b s f)]
ret = if [SORT] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SORT]
toAdd then
              [Annoted (BASIC_ITEMS b s f)]
items
            else
              [SORT] -> Annoted (BASIC_ITEMS b s f)
forall b s f. [SORT] -> Annoted (BASIC_ITEMS b s f)
pr_make_sorts [SORT]
toAdd Annoted (BASIC_ITEMS b s f)
-> [Annoted (BASIC_ITEMS b s f)] -> [Annoted (BASIC_ITEMS b s f)]
forall a. a -> [a] -> [a]
: [Annoted (BASIC_ITEMS b s f)]
items
  in
    [Annoted (BASIC_ITEMS b s f)] -> BASIC_SPEC b s f
forall b s f. [Annoted (BASIC_ITEMS b s f)] -> BASIC_SPEC b s f
Basic_spec [Annoted (BASIC_ITEMS b s f)]
ret

{- returns a non-empty list of [SORT] if datatypes had to be removed
completely -}
pr_basic_items :: Lattice a =>
    (CASL_SL a -> b -> (Maybe (BASIC_ITEMS b s f), [SORT]))
    -> (CASL_SL a -> s -> (Maybe (SIG_ITEMS s f), [SORT]))
    -> (CASL_SL a -> f -> Maybe (FORMULA f))
    -> CASL_SL a -> BASIC_ITEMS b s f
    -> (Maybe (BASIC_ITEMS b s f), [SORT])
pr_basic_items :: (CASL_SL a -> b -> (Maybe (BASIC_ITEMS b s f), [SORT]))
-> (CASL_SL a -> s -> (Maybe (SIG_ITEMS s f), [SORT]))
-> (CASL_SL a -> f -> Maybe (FORMULA f))
-> CASL_SL a
-> BASIC_ITEMS b s f
-> (Maybe (BASIC_ITEMS b s f), [SORT])
pr_basic_items fb :: CASL_SL a -> b -> (Maybe (BASIC_ITEMS b s f), [SORT])
fb fs :: CASL_SL a -> s -> (Maybe (SIG_ITEMS s f), [SORT])
fs ff :: CASL_SL a -> f -> Maybe (FORMULA f)
ff l :: CASL_SL a
l bi :: BASIC_ITEMS b s f
bi = case BASIC_ITEMS b s f
bi of
    Sig_items s :: SIG_ITEMS s f
s ->
               let
                 (res :: Maybe (SIG_ITEMS s f)
res, lst :: [SORT]
lst) = (CASL_SL a -> s -> (Maybe (SIG_ITEMS s f), [SORT]))
-> (CASL_SL a -> f -> Maybe (FORMULA f))
-> CASL_SL a
-> SIG_ITEMS s f
-> (Maybe (SIG_ITEMS s f), [SORT])
forall a s f.
Lattice a =>
(CASL_SL a -> s -> (Maybe (SIG_ITEMS s f), [SORT]))
-> (CASL_SL a -> f -> Maybe (FORMULA f))
-> CASL_SL a
-> SIG_ITEMS s f
-> (Maybe (SIG_ITEMS s f), [SORT])
pr_sig_items CASL_SL a -> s -> (Maybe (SIG_ITEMS s f), [SORT])
fs CASL_SL a -> f -> Maybe (FORMULA f)
ff CASL_SL a
l SIG_ITEMS s f
s
               in
                 if Maybe (SIG_ITEMS s f) -> Bool
forall a. Maybe a -> Bool
isNothing Maybe (SIG_ITEMS s f)
res then
                   (Maybe (BASIC_ITEMS b s f)
forall a. Maybe a
Nothing, [SORT]
lst)
                 else
                   (BASIC_ITEMS b s f -> Maybe (BASIC_ITEMS b s f)
forall a. a -> Maybe a
Just (SIG_ITEMS s f -> BASIC_ITEMS b s f
forall b s f. SIG_ITEMS s f -> BASIC_ITEMS b s f
Sig_items (Maybe (SIG_ITEMS s f) -> SIG_ITEMS s f
forall a. HasCallStack => Maybe a -> a
fromJust Maybe (SIG_ITEMS s f)
res)), [SORT]
lst)
    Free_datatype sk :: SortsKind
sk d :: [Annoted DATATYPE_DECL]
d p :: Range
p ->
               let
                 (res :: [Annoted DATATYPE_DECL]
res, pos :: Range
pos) = Int
-> Range
-> (Annoted DATATYPE_DECL -> Maybe (Annoted DATATYPE_DECL))
-> [Annoted DATATYPE_DECL]
-> ([Annoted DATATYPE_DECL], Range)
forall a b. Int -> Range -> (a -> Maybe b) -> [a] -> ([b], Range)
mapPos 2 Range
p (CASL_SL a
-> (CASL_SL a -> DATATYPE_DECL -> Maybe DATATYPE_DECL)
-> Annoted DATATYPE_DECL
-> Maybe (Annoted DATATYPE_DECL)
forall s a.
CASL_SL s
-> (CASL_SL s -> a -> Maybe a) -> Annoted a -> Maybe (Annoted a)
pr_annoted CASL_SL a
l CASL_SL a -> DATATYPE_DECL -> Maybe DATATYPE_DECL
forall a. CASL_SL a -> DATATYPE_DECL -> Maybe DATATYPE_DECL
pr_datatype_decl) [Annoted DATATYPE_DECL]
d
                 lst :: [SORT]
lst = CASL_SL a -> [DATATYPE_DECL] -> [SORT]
forall a. CASL_SL a -> [DATATYPE_DECL] -> [SORT]
pr_lost_dt CASL_SL a
l ((Annoted DATATYPE_DECL -> DATATYPE_DECL)
-> [Annoted DATATYPE_DECL] -> [DATATYPE_DECL]
forall a b. (a -> b) -> [a] -> [b]
map Annoted DATATYPE_DECL -> DATATYPE_DECL
forall a. Annoted a -> a
item [Annoted DATATYPE_DECL]
d)
               in
                 if [Annoted DATATYPE_DECL] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Annoted DATATYPE_DECL]
res then
                   (Maybe (BASIC_ITEMS b s f)
forall a. Maybe a
Nothing, [SORT]
lst)
                 else
                   (BASIC_ITEMS b s f -> Maybe (BASIC_ITEMS b s f)
forall a. a -> Maybe a
Just (SortsKind -> [Annoted DATATYPE_DECL] -> Range -> BASIC_ITEMS b s f
forall b s f.
SortsKind -> [Annoted DATATYPE_DECL] -> Range -> BASIC_ITEMS b s f
Free_datatype SortsKind
sk [Annoted DATATYPE_DECL]
res Range
pos), [SORT]
lst)
    Sort_gen s :: [Annoted (SIG_ITEMS s f)]
s p :: Range
p ->
               if CASL_SL a -> Bool
forall a. CASL_SL a -> Bool
has_cons CASL_SL a
l then
                 let
                   tmp :: [(Maybe (Annoted (SIG_ITEMS s f)), [SORT])]
tmp = (Annoted (SIG_ITEMS s f)
 -> (Maybe (Annoted (SIG_ITEMS s f)), [SORT]))
-> [Annoted (SIG_ITEMS s f)]
-> [(Maybe (Annoted (SIG_ITEMS s f)), [SORT])]
forall a b. (a -> b) -> [a] -> [b]
map (CASL_SL a
-> (CASL_SL a -> SIG_ITEMS s f -> (Maybe (SIG_ITEMS s f), [SORT]))
-> Annoted (SIG_ITEMS s f)
-> (Maybe (Annoted (SIG_ITEMS s f)), [SORT])
forall s a.
CASL_SL s
-> (CASL_SL s -> a -> (Maybe a, [SORT]))
-> Annoted a
-> (Maybe (Annoted a), [SORT])
pr_annoted_dt CASL_SL a
l ((CASL_SL a -> SIG_ITEMS s f -> (Maybe (SIG_ITEMS s f), [SORT]))
 -> Annoted (SIG_ITEMS s f)
 -> (Maybe (Annoted (SIG_ITEMS s f)), [SORT]))
-> (CASL_SL a -> SIG_ITEMS s f -> (Maybe (SIG_ITEMS s f), [SORT]))
-> Annoted (SIG_ITEMS s f)
-> (Maybe (Annoted (SIG_ITEMS s f)), [SORT])
forall a b. (a -> b) -> a -> b
$ (CASL_SL a -> s -> (Maybe (SIG_ITEMS s f), [SORT]))
-> (CASL_SL a -> f -> Maybe (FORMULA f))
-> CASL_SL a
-> SIG_ITEMS s f
-> (Maybe (SIG_ITEMS s f), [SORT])
forall a s f.
Lattice a =>
(CASL_SL a -> s -> (Maybe (SIG_ITEMS s f), [SORT]))
-> (CASL_SL a -> f -> Maybe (FORMULA f))
-> CASL_SL a
-> SIG_ITEMS s f
-> (Maybe (SIG_ITEMS s f), [SORT])
pr_sig_items CASL_SL a -> s -> (Maybe (SIG_ITEMS s f), [SORT])
fs CASL_SL a -> f -> Maybe (FORMULA f)
ff) [Annoted (SIG_ITEMS s f)]
s
                   res :: [Annoted (SIG_ITEMS s f)]
res = ((Maybe (Annoted (SIG_ITEMS s f)), [SORT])
 -> Maybe (Annoted (SIG_ITEMS s f)))
-> [(Maybe (Annoted (SIG_ITEMS s f)), [SORT])]
-> [Annoted (SIG_ITEMS s f)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Maybe (Annoted (SIG_ITEMS s f)), [SORT])
-> Maybe (Annoted (SIG_ITEMS s f))
forall a b. (a, b) -> a
fst [(Maybe (Annoted (SIG_ITEMS s f)), [SORT])]
tmp
                   lst :: [SORT]
lst = ((Maybe (Annoted (SIG_ITEMS s f)), [SORT]) -> [SORT])
-> [(Maybe (Annoted (SIG_ITEMS s f)), [SORT])] -> [SORT]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Maybe (Annoted (SIG_ITEMS s f)), [SORT]) -> [SORT]
forall a b. (a, b) -> b
snd [(Maybe (Annoted (SIG_ITEMS s f)), [SORT])]
tmp
                 in
                   if [Annoted (SIG_ITEMS s f)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Annoted (SIG_ITEMS s f)]
res then
                     (Maybe (BASIC_ITEMS b s f)
forall a. Maybe a
Nothing, [SORT]
lst)
                   else
                     (BASIC_ITEMS b s f -> Maybe (BASIC_ITEMS b s f)
forall a. a -> Maybe a
Just ([Annoted (SIG_ITEMS s f)] -> Range -> BASIC_ITEMS b s f
forall b s f.
[Annoted (SIG_ITEMS s f)] -> Range -> BASIC_ITEMS b s f
Sort_gen [Annoted (SIG_ITEMS s f)]
res Range
p), [SORT]
lst)
               else
                 (Maybe (BASIC_ITEMS b s f)
forall a. Maybe a
Nothing, [])
    Var_items v :: [VAR_DECL]
v p :: Range
p -> (BASIC_ITEMS b s f -> Maybe (BASIC_ITEMS b s f)
forall a. a -> Maybe a
Just ([VAR_DECL] -> Range -> BASIC_ITEMS b s f
forall b s f. [VAR_DECL] -> Range -> BASIC_ITEMS b s f
Var_items [VAR_DECL]
v Range
p), [])
    Local_var_axioms v :: [VAR_DECL]
v f :: [Annoted (FORMULA f)]
f p :: Range
p ->
               let
                 (res :: [Annoted (FORMULA f)]
res, pos :: Range
pos) = Int
-> Range
-> (Annoted (FORMULA f) -> Maybe (Annoted (FORMULA f)))
-> [Annoted (FORMULA f)]
-> ([Annoted (FORMULA f)], Range)
forall a b. Int -> Range -> (a -> Maybe b) -> [a] -> ([b], Range)
mapPos ([VAR_DECL] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [VAR_DECL]
v) Range
p
                              (CASL_SL a
-> (CASL_SL a -> FORMULA f -> Maybe (FORMULA f))
-> Annoted (FORMULA f)
-> Maybe (Annoted (FORMULA f))
forall s a.
CASL_SL s
-> (CASL_SL s -> a -> Maybe a) -> Annoted a -> Maybe (Annoted a)
pr_annoted CASL_SL a
l ((CASL_SL a -> FORMULA f -> Maybe (FORMULA f))
 -> Annoted (FORMULA f) -> Maybe (Annoted (FORMULA f)))
-> (CASL_SL a -> FORMULA f -> Maybe (FORMULA f))
-> Annoted (FORMULA f)
-> Maybe (Annoted (FORMULA f))
forall a b. (a -> b) -> a -> b
$ (CASL_SL a -> f -> Maybe (FORMULA f))
-> CASL_SL a -> FORMULA f -> Maybe (FORMULA f)
forall a f.
Lattice a =>
(CASL_SL a -> f -> Maybe (FORMULA f))
-> CASL_SL a -> FORMULA f -> Maybe (FORMULA f)
pr_formula CASL_SL a -> f -> Maybe (FORMULA f)
ff) [Annoted (FORMULA f)]
f
               in
                 if [Annoted (FORMULA f)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Annoted (FORMULA f)]
res then
                   (Maybe (BASIC_ITEMS b s f)
forall a. Maybe a
Nothing, [])
                 else
                   (BASIC_ITEMS b s f -> Maybe (BASIC_ITEMS b s f)
forall a. a -> Maybe a
Just ([VAR_DECL] -> [Annoted (FORMULA f)] -> Range -> BASIC_ITEMS b s f
forall b s f.
[VAR_DECL] -> [Annoted (FORMULA f)] -> Range -> BASIC_ITEMS b s f
Local_var_axioms [VAR_DECL]
v [Annoted (FORMULA f)]
res Range
pos), [])
    Axiom_items f :: [Annoted (FORMULA f)]
f p :: Range
p ->
               let
                 (res :: [Annoted (FORMULA f)]
res, pos :: Range
pos) = Int
-> Range
-> (Annoted (FORMULA f) -> Maybe (Annoted (FORMULA f)))
-> [Annoted (FORMULA f)]
-> ([Annoted (FORMULA f)], Range)
forall a b. Int -> Range -> (a -> Maybe b) -> [a] -> ([b], Range)
mapPos 0 Range
p (CASL_SL a
-> (CASL_SL a -> FORMULA f -> Maybe (FORMULA f))
-> Annoted (FORMULA f)
-> Maybe (Annoted (FORMULA f))
forall s a.
CASL_SL s
-> (CASL_SL s -> a -> Maybe a) -> Annoted a -> Maybe (Annoted a)
pr_annoted CASL_SL a
l ((CASL_SL a -> FORMULA f -> Maybe (FORMULA f))
 -> Annoted (FORMULA f) -> Maybe (Annoted (FORMULA f)))
-> (CASL_SL a -> FORMULA f -> Maybe (FORMULA f))
-> Annoted (FORMULA f)
-> Maybe (Annoted (FORMULA f))
forall a b. (a -> b) -> a -> b
$ (CASL_SL a -> f -> Maybe (FORMULA f))
-> CASL_SL a -> FORMULA f -> Maybe (FORMULA f)
forall a f.
Lattice a =>
(CASL_SL a -> f -> Maybe (FORMULA f))
-> CASL_SL a -> FORMULA f -> Maybe (FORMULA f)
pr_formula CASL_SL a -> f -> Maybe (FORMULA f)
ff) [Annoted (FORMULA f)]
f
               in
                 if [Annoted (FORMULA f)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Annoted (FORMULA f)]
res then
                   (Maybe (BASIC_ITEMS b s f)
forall a. Maybe a
Nothing, [])
                 else
                   (BASIC_ITEMS b s f -> Maybe (BASIC_ITEMS b s f)
forall a. a -> Maybe a
Just ([Annoted (FORMULA f)] -> Range -> BASIC_ITEMS b s f
forall b s f. [Annoted (FORMULA f)] -> Range -> BASIC_ITEMS b s f
Axiom_items [Annoted (FORMULA f)]
res Range
pos), [])
    Ext_BASIC_ITEMS b :: b
b -> CASL_SL a -> b -> (Maybe (BASIC_ITEMS b s f), [SORT])
fb CASL_SL a
l b
b

pr_datatype_decl :: CASL_SL a -> DATATYPE_DECL -> Maybe DATATYPE_DECL
pr_datatype_decl :: CASL_SL a -> DATATYPE_DECL -> Maybe DATATYPE_DECL
pr_datatype_decl l :: CASL_SL a
l (Datatype_decl s :: SORT
s a :: [Annoted ALTERNATIVE]
a p :: Range
p) =
                 let
                   (res :: [Annoted ALTERNATIVE]
res, pos :: Range
pos) = Int
-> Range
-> (Annoted ALTERNATIVE -> Maybe (Annoted ALTERNATIVE))
-> [Annoted ALTERNATIVE]
-> ([Annoted ALTERNATIVE], Range)
forall a b. Int -> Range -> (a -> Maybe b) -> [a] -> ([b], Range)
mapPos 1 Range
p (CASL_SL a
-> (CASL_SL a -> ALTERNATIVE -> Maybe ALTERNATIVE)
-> Annoted ALTERNATIVE
-> Maybe (Annoted ALTERNATIVE)
forall s a.
CASL_SL s
-> (CASL_SL s -> a -> Maybe a) -> Annoted a -> Maybe (Annoted a)
pr_annoted CASL_SL a
l CASL_SL a -> ALTERNATIVE -> Maybe ALTERNATIVE
forall a. CASL_SL a -> ALTERNATIVE -> Maybe ALTERNATIVE
pr_alternative) [Annoted ALTERNATIVE]
a
                 in
                   if [Annoted ALTERNATIVE] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Annoted ALTERNATIVE]
res then
                     Maybe DATATYPE_DECL
forall a. Maybe a
Nothing
                   else
                     DATATYPE_DECL -> Maybe DATATYPE_DECL
forall a. a -> Maybe a
Just (SORT -> [Annoted ALTERNATIVE] -> Range -> DATATYPE_DECL
Datatype_decl SORT
s [Annoted ALTERNATIVE]
res Range
pos)

pr_alternative :: CASL_SL a -> ALTERNATIVE -> Maybe ALTERNATIVE
pr_alternative :: CASL_SL a -> ALTERNATIVE -> Maybe ALTERNATIVE
pr_alternative l :: CASL_SL a
l alt :: ALTERNATIVE
alt = case ALTERNATIVE
alt of
    Alt_construct Total n :: SORT
n c :: [COMPONENTS]
c p :: Range
p ->
               let
                 (res :: [COMPONENTS]
res, pos :: Range
pos) = Int
-> Range
-> (COMPONENTS -> Maybe COMPONENTS)
-> [COMPONENTS]
-> ([COMPONENTS], Range)
forall a b. Int -> Range -> (a -> Maybe b) -> [a] -> ([b], Range)
mapPos 1 Range
p (CASL_SL a -> COMPONENTS -> Maybe COMPONENTS
forall a. CASL_SL a -> COMPONENTS -> Maybe COMPONENTS
pr_components CASL_SL a
l) [COMPONENTS]
c
               in
                 if [COMPONENTS] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [COMPONENTS]
res then
                   Maybe ALTERNATIVE
forall a. Maybe a
Nothing
                 else
                   ALTERNATIVE -> Maybe ALTERNATIVE
forall a. a -> Maybe a
Just (OpKind -> SORT -> [COMPONENTS] -> Range -> ALTERNATIVE
Alt_construct OpKind
Total SORT
n [COMPONENTS]
res Range
pos)
    Alt_construct Partial _ _ _ ->
             if CASL_SL a -> Bool
forall a. CASL_SL a -> Bool
has_part CASL_SL a
l then
               ALTERNATIVE -> Maybe ALTERNATIVE
forall a. a -> Maybe a
Just ALTERNATIVE
alt
             else
               Maybe ALTERNATIVE
forall a. Maybe a
Nothing
    Subsorts s :: [SORT]
s p :: Range
p ->
               if CASL_SL a -> Bool
forall a. CASL_SL a -> Bool
has_sub CASL_SL a
l then
                 ALTERNATIVE -> Maybe ALTERNATIVE
forall a. a -> Maybe a
Just ([SORT] -> Range -> ALTERNATIVE
Subsorts [SORT]
s Range
p)
               else
                 Maybe ALTERNATIVE
forall a. Maybe a
Nothing

pr_components :: CASL_SL a -> COMPONENTS -> Maybe COMPONENTS
pr_components :: CASL_SL a -> COMPONENTS -> Maybe COMPONENTS
pr_components l :: CASL_SL a
l sel :: COMPONENTS
sel = case COMPONENTS
sel of
    Cons_select Partial _ _ _ ->
              if CASL_SL a -> Bool
forall a. CASL_SL a -> Bool
has_part CASL_SL a
l then
                COMPONENTS -> Maybe COMPONENTS
forall a. a -> Maybe a
Just COMPONENTS
sel
              else
                Maybe COMPONENTS
forall a. Maybe a
Nothing
    _ -> COMPONENTS -> Maybe COMPONENTS
forall a. a -> Maybe a
Just COMPONENTS
sel

{- takes a list of datatype declarations and checks whether a
whole declaration is invalid in the given sublogic - if this
is the case, the sort that would be declared by the type is
added to a list of SORT that is emitted -}
pr_lost_dt :: CASL_SL a -> [DATATYPE_DECL] -> [SORT]
pr_lost_dt :: CASL_SL a -> [DATATYPE_DECL] -> [SORT]
pr_lost_dt sl :: CASL_SL a
sl = (DATATYPE_DECL -> [SORT]) -> [DATATYPE_DECL] -> [SORT]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ dt :: DATATYPE_DECL
dt@(Datatype_decl s :: SORT
s _ _) ->
                     case CASL_SL a -> DATATYPE_DECL -> Maybe DATATYPE_DECL
forall a. CASL_SL a -> DATATYPE_DECL -> Maybe DATATYPE_DECL
pr_datatype_decl CASL_SL a
sl DATATYPE_DECL
dt of
                       Nothing -> [SORT
s]
                       _ -> [])

pr_symbol :: Lattice a => CASL_SL a -> Symbol -> Maybe Symbol
pr_symbol :: CASL_SL a -> Symbol -> Maybe Symbol
pr_symbol l :: CASL_SL a
l = CASL_SL a -> (Symbol -> CASL_SL a) -> Symbol -> Maybe Symbol
forall a b.
Lattice a =>
CASL_SL a -> (b -> CASL_SL a) -> b -> Maybe b
pr_check CASL_SL a
l Symbol -> CASL_SL a
forall a. Lattice a => Symbol -> CASL_SL a
sl_symbol

{- returns a non-empty list of [SORT] if datatypes had to be removed
completely -}
pr_sig_items :: Lattice a =>
    (CASL_SL a -> s -> (Maybe (SIG_ITEMS s f), [SORT]))
    -> (CASL_SL a -> f -> Maybe (FORMULA f))
    -> CASL_SL a -> SIG_ITEMS s f -> (Maybe (SIG_ITEMS s f), [SORT])
pr_sig_items :: (CASL_SL a -> s -> (Maybe (SIG_ITEMS s f), [SORT]))
-> (CASL_SL a -> f -> Maybe (FORMULA f))
-> CASL_SL a
-> SIG_ITEMS s f
-> (Maybe (SIG_ITEMS s f), [SORT])
pr_sig_items sf :: CASL_SL a -> s -> (Maybe (SIG_ITEMS s f), [SORT])
sf ff :: CASL_SL a -> f -> Maybe (FORMULA f)
ff l :: CASL_SL a
l si :: SIG_ITEMS s f
si = case SIG_ITEMS s f
si of
    Sort_items sk :: SortsKind
sk s :: [Annoted (SORT_ITEM f)]
s p :: Range
p ->
             let
               (res :: [Annoted (SORT_ITEM f)]
res, pos :: Range
pos) = Int
-> Range
-> (Annoted (SORT_ITEM f) -> Maybe (Annoted (SORT_ITEM f)))
-> [Annoted (SORT_ITEM f)]
-> ([Annoted (SORT_ITEM f)], Range)
forall a b. Int -> Range -> (a -> Maybe b) -> [a] -> ([b], Range)
mapPos 1 Range
p (CASL_SL a
-> (CASL_SL a -> SORT_ITEM f -> Maybe (SORT_ITEM f))
-> Annoted (SORT_ITEM f)
-> Maybe (Annoted (SORT_ITEM f))
forall s a.
CASL_SL s
-> (CASL_SL s -> a -> Maybe a) -> Annoted a -> Maybe (Annoted a)
pr_annoted CASL_SL a
l CASL_SL a -> SORT_ITEM f -> Maybe (SORT_ITEM f)
forall a f. CASL_SL a -> SORT_ITEM f -> Maybe (SORT_ITEM f)
pr_sort_item) [Annoted (SORT_ITEM f)]
s
             in
               if [Annoted (SORT_ITEM f)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Annoted (SORT_ITEM f)]
res then
                 (Maybe (SIG_ITEMS s f)
forall a. Maybe a
Nothing, [])
               else
                 (SIG_ITEMS s f -> Maybe (SIG_ITEMS s f)
forall a. a -> Maybe a
Just (SortsKind -> [Annoted (SORT_ITEM f)] -> Range -> SIG_ITEMS s f
forall s f.
SortsKind -> [Annoted (SORT_ITEM f)] -> Range -> SIG_ITEMS s f
Sort_items SortsKind
sk [Annoted (SORT_ITEM f)]
res Range
pos), [])
    Op_items o :: [Annoted (OP_ITEM f)]
o p :: Range
p ->
             let
               (res :: [Annoted (OP_ITEM f)]
res, pos :: Range
pos) = Int
-> Range
-> (Annoted (OP_ITEM f) -> Maybe (Annoted (OP_ITEM f)))
-> [Annoted (OP_ITEM f)]
-> ([Annoted (OP_ITEM f)], Range)
forall a b. Int -> Range -> (a -> Maybe b) -> [a] -> ([b], Range)
mapPos 1 Range
p (CASL_SL a
-> (CASL_SL a -> OP_ITEM f -> Maybe (OP_ITEM f))
-> Annoted (OP_ITEM f)
-> Maybe (Annoted (OP_ITEM f))
forall s a.
CASL_SL s
-> (CASL_SL s -> a -> Maybe a) -> Annoted a -> Maybe (Annoted a)
pr_annoted CASL_SL a
l ((CASL_SL a -> OP_ITEM f -> Maybe (OP_ITEM f))
 -> Annoted (OP_ITEM f) -> Maybe (Annoted (OP_ITEM f)))
-> (CASL_SL a -> OP_ITEM f -> Maybe (OP_ITEM f))
-> Annoted (OP_ITEM f)
-> Maybe (Annoted (OP_ITEM f))
forall a b. (a -> b) -> a -> b
$ (CASL_SL a -> f -> Maybe (FORMULA f))
-> CASL_SL a -> OP_ITEM f -> Maybe (OP_ITEM f)
forall a f.
Lattice a =>
(CASL_SL a -> f -> Maybe (FORMULA f))
-> CASL_SL a -> OP_ITEM f -> Maybe (OP_ITEM f)
pr_op_item CASL_SL a -> f -> Maybe (FORMULA f)
ff) [Annoted (OP_ITEM f)]
o
             in
               if [Annoted (OP_ITEM f)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Annoted (OP_ITEM f)]
res then
                 (Maybe (SIG_ITEMS s f)
forall a. Maybe a
Nothing, [])
               else
                 (SIG_ITEMS s f -> Maybe (SIG_ITEMS s f)
forall a. a -> Maybe a
Just ([Annoted (OP_ITEM f)] -> Range -> SIG_ITEMS s f
forall s f. [Annoted (OP_ITEM f)] -> Range -> SIG_ITEMS s f
Op_items [Annoted (OP_ITEM f)]
res Range
pos), [])
    Pred_items i :: [Annoted (PRED_ITEM f)]
i p :: Range
p ->
             if CASL_SL a -> Bool
forall a. CASL_SL a -> Bool
has_pred CASL_SL a
l then
               (SIG_ITEMS s f -> Maybe (SIG_ITEMS s f)
forall a. a -> Maybe a
Just ([Annoted (PRED_ITEM f)] -> Range -> SIG_ITEMS s f
forall s f. [Annoted (PRED_ITEM f)] -> Range -> SIG_ITEMS s f
Pred_items [Annoted (PRED_ITEM f)]
i Range
p), [])
             else
               (Maybe (SIG_ITEMS s f)
forall a. Maybe a
Nothing, [])
    Datatype_items sk :: SortsKind
sk d :: [Annoted DATATYPE_DECL]
d p :: Range
p ->
             let
               (res :: [Annoted DATATYPE_DECL]
res, pos :: Range
pos) = Int
-> Range
-> (Annoted DATATYPE_DECL -> Maybe (Annoted DATATYPE_DECL))
-> [Annoted DATATYPE_DECL]
-> ([Annoted DATATYPE_DECL], Range)
forall a b. Int -> Range -> (a -> Maybe b) -> [a] -> ([b], Range)
mapPos 1 Range
p (CASL_SL a
-> (CASL_SL a -> DATATYPE_DECL -> Maybe DATATYPE_DECL)
-> Annoted DATATYPE_DECL
-> Maybe (Annoted DATATYPE_DECL)
forall s a.
CASL_SL s
-> (CASL_SL s -> a -> Maybe a) -> Annoted a -> Maybe (Annoted a)
pr_annoted CASL_SL a
l CASL_SL a -> DATATYPE_DECL -> Maybe DATATYPE_DECL
forall a. CASL_SL a -> DATATYPE_DECL -> Maybe DATATYPE_DECL
pr_datatype_decl) [Annoted DATATYPE_DECL]
d
               lst :: [SORT]
lst = CASL_SL a -> [DATATYPE_DECL] -> [SORT]
forall a. CASL_SL a -> [DATATYPE_DECL] -> [SORT]
pr_lost_dt CASL_SL a
l ((Annoted DATATYPE_DECL -> DATATYPE_DECL)
-> [Annoted DATATYPE_DECL] -> [DATATYPE_DECL]
forall a b. (a -> b) -> [a] -> [b]
map Annoted DATATYPE_DECL -> DATATYPE_DECL
forall a. Annoted a -> a
item [Annoted DATATYPE_DECL]
d)
             in
               if [Annoted DATATYPE_DECL] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Annoted DATATYPE_DECL]
res then
                 (Maybe (SIG_ITEMS s f)
forall a. Maybe a
Nothing, [SORT]
lst)
               else
                 (SIG_ITEMS s f -> Maybe (SIG_ITEMS s f)
forall a. a -> Maybe a
Just (SortsKind -> [Annoted DATATYPE_DECL] -> Range -> SIG_ITEMS s f
forall s f.
SortsKind -> [Annoted DATATYPE_DECL] -> Range -> SIG_ITEMS s f
Datatype_items SortsKind
sk [Annoted DATATYPE_DECL]
res Range
pos), [SORT]
lst)
    Ext_SIG_ITEMS s :: s
s -> CASL_SL a -> s -> (Maybe (SIG_ITEMS s f), [SORT])
sf CASL_SL a
l s
s

pr_op_item :: Lattice a => (CASL_SL a -> f -> Maybe (FORMULA f))
           -> CASL_SL a -> OP_ITEM f -> Maybe (OP_ITEM f)
pr_op_item :: (CASL_SL a -> f -> Maybe (FORMULA f))
-> CASL_SL a -> OP_ITEM f -> Maybe (OP_ITEM f)
pr_op_item ff :: CASL_SL a -> f -> Maybe (FORMULA f)
ff l :: CASL_SL a
l oi :: OP_ITEM f
oi = case OP_ITEM f
oi of
      Op_defn o :: SORT
o h :: OP_HEAD
h f :: Annoted (TERM f)
f r :: Range
r -> do
        Annoted (TERM f)
g <- CASL_SL a
-> (CASL_SL a -> TERM f -> Maybe (TERM f))
-> Annoted (TERM f)
-> Maybe (Annoted (TERM f))
forall s a.
CASL_SL s
-> (CASL_SL s -> a -> Maybe a) -> Annoted a -> Maybe (Annoted a)
pr_annoted CASL_SL a
l ((CASL_SL a -> f -> Maybe (FORMULA f))
-> CASL_SL a -> TERM f -> Maybe (TERM f)
forall a f.
Lattice a =>
(CASL_SL a -> f -> Maybe (FORMULA f))
-> CASL_SL a -> TERM f -> Maybe (TERM f)
pr_term CASL_SL a -> f -> Maybe (FORMULA f)
ff) Annoted (TERM f)
f
        OP_ITEM f -> Maybe (OP_ITEM f)
forall (m :: * -> *) a. Monad m => a -> m a
return (OP_ITEM f -> Maybe (OP_ITEM f)) -> OP_ITEM f -> Maybe (OP_ITEM f)
forall a b. (a -> b) -> a -> b
$ SORT -> OP_HEAD -> Annoted (TERM f) -> Range -> OP_ITEM f
forall f. SORT -> OP_HEAD -> Annoted (TERM f) -> Range -> OP_ITEM f
Op_defn SORT
o OP_HEAD
h Annoted (TERM f)
g Range
r
      _ -> OP_ITEM f -> Maybe (OP_ITEM f)
forall a. a -> Maybe a
Just OP_ITEM f
oi

{- subsort declarations and definitions are reduced to simple
sort declarations if the sublogic disallows subsorting to
avoid loosing sorts in the projection -}
pr_sort_item :: CASL_SL a -> SORT_ITEM f -> Maybe (SORT_ITEM f)
pr_sort_item :: CASL_SL a -> SORT_ITEM f -> Maybe (SORT_ITEM f)
pr_sort_item _ (Sort_decl s :: [SORT]
s p :: Range
p) = SORT_ITEM f -> Maybe (SORT_ITEM f)
forall a. a -> Maybe a
Just ([SORT] -> Range -> SORT_ITEM f
forall f. [SORT] -> Range -> SORT_ITEM f
Sort_decl [SORT]
s Range
p)
pr_sort_item l :: CASL_SL a
l (Subsort_decl sl :: [SORT]
sl s :: SORT
s p :: Range
p) =
             SORT_ITEM f -> Maybe (SORT_ITEM f)
forall a. a -> Maybe a
Just (SORT_ITEM f -> Maybe (SORT_ITEM f))
-> SORT_ITEM f -> Maybe (SORT_ITEM f)
forall a b. (a -> b) -> a -> b
$ if CASL_SL a -> Bool
forall a. CASL_SL a -> Bool
has_sub CASL_SL a
l then [SORT] -> SORT -> Range -> SORT_ITEM f
forall f. [SORT] -> SORT -> Range -> SORT_ITEM f
Subsort_decl [SORT]
sl SORT
s Range
p
                    else [SORT] -> Range -> SORT_ITEM f
forall f. [SORT] -> Range -> SORT_ITEM f
Sort_decl (SORT
s SORT -> [SORT] -> [SORT]
forall a. a -> [a] -> [a]
: [SORT]
sl) Range
nullRange
pr_sort_item l :: CASL_SL a
l (Subsort_defn s1 :: SORT
s1 v :: VAR
v s2 :: SORT
s2 f :: Annoted (FORMULA f)
f p :: Range
p) =
             SORT_ITEM f -> Maybe (SORT_ITEM f)
forall a. a -> Maybe a
Just (SORT_ITEM f -> Maybe (SORT_ITEM f))
-> SORT_ITEM f -> Maybe (SORT_ITEM f)
forall a b. (a -> b) -> a -> b
$ if CASL_SL a -> Bool
forall a. CASL_SL a -> Bool
has_sub CASL_SL a
l then SORT -> VAR -> SORT -> Annoted (FORMULA f) -> Range -> SORT_ITEM f
forall f.
SORT -> VAR -> SORT -> Annoted (FORMULA f) -> Range -> SORT_ITEM f
Subsort_defn SORT
s1 VAR
v SORT
s2 Annoted (FORMULA f)
f Range
p
                    else [SORT] -> Range -> SORT_ITEM f
forall f. [SORT] -> Range -> SORT_ITEM f
Sort_decl [SORT
s1] Range
nullRange
pr_sort_item _ (Iso_decl s :: [SORT]
s p :: Range
p) = SORT_ITEM f -> Maybe (SORT_ITEM f)
forall a. a -> Maybe a
Just ([SORT] -> Range -> SORT_ITEM f
forall f. [SORT] -> Range -> SORT_ITEM f
Iso_decl [SORT]
s Range
p)

pr_symb_items :: Lattice a => CASL_SL a -> SYMB_ITEMS
              -> Maybe SYMB_ITEMS
pr_symb_items :: CASL_SL a -> SYMB_ITEMS -> Maybe SYMB_ITEMS
pr_symb_items l :: CASL_SL a
l (Symb_items k :: SYMB_KIND
k s :: [SYMB]
s p :: Range
p) =
              if CASL_SL a -> SYMB_KIND -> (SYMB_KIND -> CASL_SL a) -> Bool
forall a b. Lattice a => CASL_SL a -> b -> (b -> CASL_SL a) -> Bool
in_x CASL_SL a
l SYMB_KIND
k SYMB_KIND -> CASL_SL a
forall a. Lattice a => SYMB_KIND -> CASL_SL a
sl_symb_kind then
                let
                  (res :: [SYMB]
res, pos :: Range
pos) = Int -> Range -> (SYMB -> Maybe SYMB) -> [SYMB] -> ([SYMB], Range)
forall a b. Int -> Range -> (a -> Maybe b) -> [a] -> ([b], Range)
mapPos 1 Range
p (CASL_SL a -> SYMB -> Maybe SYMB
forall a. Lattice a => CASL_SL a -> SYMB -> Maybe SYMB
pr_symb CASL_SL a
l) [SYMB]
s
                in
                  if [SYMB] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SYMB]
res then
                    Maybe SYMB_ITEMS
forall a. Maybe a
Nothing
                  else
                    SYMB_ITEMS -> Maybe SYMB_ITEMS
forall a. a -> Maybe a
Just (SYMB_KIND -> [SYMB] -> Range -> SYMB_ITEMS
Symb_items SYMB_KIND
k [SYMB]
res Range
pos)
              else
                Maybe SYMB_ITEMS
forall a. Maybe a
Nothing

pr_symb_map_items :: Lattice a => CASL_SL a -> SYMB_MAP_ITEMS
                  -> Maybe SYMB_MAP_ITEMS
pr_symb_map_items :: CASL_SL a -> SYMB_MAP_ITEMS -> Maybe SYMB_MAP_ITEMS
pr_symb_map_items l :: CASL_SL a
l (Symb_map_items k :: SYMB_KIND
k s :: [SYMB_OR_MAP]
s p :: Range
p) =
                  if CASL_SL a -> SYMB_KIND -> (SYMB_KIND -> CASL_SL a) -> Bool
forall a b. Lattice a => CASL_SL a -> b -> (b -> CASL_SL a) -> Bool
in_x CASL_SL a
l SYMB_KIND
k SYMB_KIND -> CASL_SL a
forall a. Lattice a => SYMB_KIND -> CASL_SL a
sl_symb_kind then
                    let
                      (res :: [SYMB_OR_MAP]
res, pos :: Range
pos) = Int
-> Range
-> (SYMB_OR_MAP -> Maybe SYMB_OR_MAP)
-> [SYMB_OR_MAP]
-> ([SYMB_OR_MAP], Range)
forall a b. Int -> Range -> (a -> Maybe b) -> [a] -> ([b], Range)
mapPos 1 Range
p (CASL_SL a -> SYMB_OR_MAP -> Maybe SYMB_OR_MAP
forall a.
Lattice a =>
CASL_SL a -> SYMB_OR_MAP -> Maybe SYMB_OR_MAP
pr_symb_or_map CASL_SL a
l) [SYMB_OR_MAP]
s
                    in
                      if [SYMB_OR_MAP] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SYMB_OR_MAP]
res then
                        Maybe SYMB_MAP_ITEMS
forall a. Maybe a
Nothing
                      else
                        SYMB_MAP_ITEMS -> Maybe SYMB_MAP_ITEMS
forall a. a -> Maybe a
Just (SYMB_KIND -> [SYMB_OR_MAP] -> Range -> SYMB_MAP_ITEMS
Symb_map_items SYMB_KIND
k [SYMB_OR_MAP]
res Range
pos)
                  else
                    Maybe SYMB_MAP_ITEMS
forall a. Maybe a
Nothing

pr_symb_or_map :: Lattice a => CASL_SL a -> SYMB_OR_MAP
               -> Maybe SYMB_OR_MAP
pr_symb_or_map :: CASL_SL a -> SYMB_OR_MAP -> Maybe SYMB_OR_MAP
pr_symb_or_map l :: CASL_SL a
l (Symb s :: SYMB
s) =
               let
                 res :: Maybe SYMB
res = CASL_SL a -> SYMB -> Maybe SYMB
forall a. Lattice a => CASL_SL a -> SYMB -> Maybe SYMB
pr_symb CASL_SL a
l SYMB
s
               in
                 if Maybe SYMB -> Bool
forall a. Maybe a -> Bool
isNothing Maybe SYMB
res then
                   Maybe SYMB_OR_MAP
forall a. Maybe a
Nothing
                 else
                   SYMB_OR_MAP -> Maybe SYMB_OR_MAP
forall a. a -> Maybe a
Just (SYMB -> SYMB_OR_MAP
Symb (Maybe SYMB -> SYMB
forall a. HasCallStack => Maybe a -> a
fromJust Maybe SYMB
res))
pr_symb_or_map l :: CASL_SL a
l (Symb_map s :: SYMB
s t :: SYMB
t p :: Range
p) =
               let
                 a :: Maybe SYMB
a = CASL_SL a -> SYMB -> Maybe SYMB
forall a. Lattice a => CASL_SL a -> SYMB -> Maybe SYMB
pr_symb CASL_SL a
l SYMB
s
                 b :: Maybe SYMB
b = CASL_SL a -> SYMB -> Maybe SYMB
forall a. Lattice a => CASL_SL a -> SYMB -> Maybe SYMB
pr_symb CASL_SL a
l SYMB
t
               in
                 if Maybe SYMB -> Bool
forall a. Maybe a -> Bool
isJust Maybe SYMB
a Bool -> Bool -> Bool
&& Maybe SYMB -> Bool
forall a. Maybe a -> Bool
isJust Maybe SYMB
b then
                   SYMB_OR_MAP -> Maybe SYMB_OR_MAP
forall a. a -> Maybe a
Just (SYMB -> SYMB -> Range -> SYMB_OR_MAP
Symb_map SYMB
s SYMB
t Range
p)
                 else
                   Maybe SYMB_OR_MAP
forall a. Maybe a
Nothing

pr_symb :: Lattice a => CASL_SL a -> SYMB -> Maybe SYMB
pr_symb :: CASL_SL a -> SYMB -> Maybe SYMB
pr_symb _ (Symb_id i :: SORT
i) = SYMB -> Maybe SYMB
forall a. a -> Maybe a
Just (SORT -> SYMB
Symb_id SORT
i)
pr_symb l :: CASL_SL a
l (Qual_id i :: SORT
i t :: TYPE
t p :: Range
p) =
        if CASL_SL a -> TYPE -> (TYPE -> CASL_SL a) -> Bool
forall a b. Lattice a => CASL_SL a -> b -> (b -> CASL_SL a) -> Bool
in_x CASL_SL a
l TYPE
t TYPE -> CASL_SL a
forall a. Lattice a => TYPE -> CASL_SL a
sl_type then
          SYMB -> Maybe SYMB
forall a. a -> Maybe a
Just (SORT -> TYPE -> Range -> SYMB
Qual_id SORT
i TYPE
t Range
p)
        else
          Maybe SYMB
forall a. Maybe a
Nothing

pr_sign :: CASL_SL a -> Sign f e -> Sign f e
pr_sign :: CASL_SL a -> Sign f e -> Sign f e
pr_sign _sl :: CASL_SL a
_sl s :: Sign f e
s = Sign f e
s -- do something here

pr_morphism :: Lattice a => CASL_SL a -> Morphism f e m
            -> Morphism f e m
pr_morphism :: CASL_SL a -> Morphism f e m -> Morphism f e m
pr_morphism l :: CASL_SL a
l m :: Morphism f e m
m =
     Morphism f e m
m { msource :: Sign f e
msource = CASL_SL a -> Sign f e -> Sign f e
forall a f e. CASL_SL a -> Sign f e -> Sign f e
pr_sign CASL_SL a
l (Sign f e -> Sign f e) -> Sign f e -> Sign f e
forall a b. (a -> b) -> a -> b
$ Morphism f e m -> Sign f e
forall f e m. Morphism f e m -> Sign f e
msource Morphism f e m
m
       , mtarget :: Sign f e
mtarget = CASL_SL a -> Sign f e -> Sign f e
forall a f e. CASL_SL a -> Sign f e -> Sign f e
pr_sign CASL_SL a
l (Sign f e -> Sign f e) -> Sign f e -> Sign f e
forall a b. (a -> b) -> a -> b
$ Morphism f e m -> Sign f e
forall f e m. Morphism f e m -> Sign f e
mtarget Morphism f e m
m
       , op_map :: Op_map
op_map = CASL_SL a -> Op_map -> Op_map
forall a. Lattice a => CASL_SL a -> Op_map -> Op_map
pr_op_map CASL_SL a
l (Op_map -> Op_map) -> Op_map -> Op_map
forall a b. (a -> b) -> a -> b
$ Morphism f e m -> Op_map
forall f e m. Morphism f e m -> Op_map
op_map Morphism f e m
m
       , pred_map :: Pred_map
pred_map = CASL_SL a -> Pred_map -> Pred_map
forall a. CASL_SL a -> Pred_map -> Pred_map
pr_pred_map CASL_SL a
l (Pred_map -> Pred_map) -> Pred_map -> Pred_map
forall a b. (a -> b) -> a -> b
$ Morphism f e m -> Pred_map
forall f e m. Morphism f e m -> Pred_map
pred_map Morphism f e m
m }

{- predicates only rely on the has_pred feature, so the map
can be kept or removed as a whole -}
pr_pred_map :: CASL_SL a -> Pred_map -> Pred_map
pr_pred_map :: CASL_SL a -> Pred_map -> Pred_map
pr_pred_map l :: CASL_SL a
l x :: Pred_map
x = if CASL_SL a -> Bool
forall a. CASL_SL a -> Bool
has_pred CASL_SL a
l then Pred_map
x else Pred_map
forall k a. Map k a
Map.empty

pr_op_map :: Lattice a => CASL_SL a -> Op_map -> Op_map
pr_op_map :: CASL_SL a -> Op_map -> Op_map
pr_op_map = ((SORT, OpType) -> (SORT, OpKind) -> Bool) -> Op_map -> Op_map
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (((SORT, OpType) -> (SORT, OpKind) -> Bool) -> Op_map -> Op_map)
-> (CASL_SL a -> (SORT, OpType) -> (SORT, OpKind) -> Bool)
-> CASL_SL a
-> Op_map
-> Op_map
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CASL_SL a -> (SORT, OpType) -> (SORT, OpKind) -> Bool
forall a.
Lattice a =>
CASL_SL a -> (SORT, OpType) -> (SORT, OpKind) -> Bool
pr_op_map_entry

pr_op_map_entry :: Lattice a => CASL_SL a -> (Id, OpType) -> (Id, OpKind)
    -> Bool
pr_op_map_entry :: CASL_SL a -> (SORT, OpType) -> (SORT, OpKind) -> Bool
pr_op_map_entry l :: CASL_SL a
l (_, t :: OpType
t) (_, b :: OpKind
b) =
    CASL_SL a -> Bool
forall a. CASL_SL a -> Bool
has_part CASL_SL a
l Bool -> Bool -> Bool
|| CASL_SL a -> OpType -> (OpType -> CASL_SL a) -> Bool
forall a b. Lattice a => CASL_SL a -> b -> (b -> CASL_SL a) -> Bool
in_x CASL_SL a
l OpType
t OpType -> CASL_SL a
forall a. Lattice a => OpType -> CASL_SL a
sl_optype Bool -> Bool -> Bool
&& OpKind
b OpKind -> OpKind -> Bool
forall a. Eq a => a -> a -> Bool
== OpKind
Partial

{- compute a morphism that consists of the original signature
and the projected signature -}
pr_epsilon :: m -> CASL_SL a -> Sign f e -> Morphism f e m
pr_epsilon :: m -> CASL_SL a -> Sign f e -> Morphism f e m
pr_epsilon extEm :: m
extEm l :: CASL_SL a
l s :: Sign f e
s = m -> Sign f e -> Sign f e -> Morphism f e m
forall m f e. m -> Sign f e -> Sign f e -> Morphism f e m
embedMorphism m
extEm Sign f e
s (Sign f e -> Morphism f e m) -> Sign f e -> Morphism f e m
forall a b. (a -> b) -> a -> b
$ CASL_SL a -> Sign f e -> Sign f e
forall a f e. CASL_SL a -> Sign f e -> Sign f e
pr_sign CASL_SL a
l Sign f e
s