{- |

Module : $Header$

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 (..)

-- * class

, Lattice (..)

-- * predicates on CASL_SL

, has_sub

, has_cons

-- * functions for SemiLatticeWithTop instance

, top

, caslTop

, cFol

, sublogics_max

-- * functions for the creation of minimal sublogics

, bottom

, emptyMapConsFeature

, need_sub

, need_pred

, need_horn

, need_fol

-- * functions for Logic instance sublogic to string conversion

, sublogics_name

-- ** list of all sublogics

, sublogics_all

-- * computes the sublogic of a given element

, sl_sig_items

, sl_basic_spec

, sl_opkind

, sl_op_type

, sl_sentence

, 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.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 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

| FOL -- ^ first-order logic

| SOL -- ^ second-order logic

deriving (Show, Eq, Ord)

data SubsortingFeatures = NoSub

| LocFilSub

| Sub

deriving (Show, Eq, Ord)

data SortGenerationFeatures =

NoSortGen

| SortGen { emptyMapping :: Bool

-- ^ Mapping of indexed sorts is empty

, onlyInjConstrs :: Bool

-- ^ only constructors that are subsort injections

} deriving (Show, Eq, Ord)

joinSortGenFeature :: (Bool -> Bool -> Bool)

-> SortGenerationFeatures -> SortGenerationFeatures

-> SortGenerationFeatures

joinSortGenFeature f x y =

case x of

NoSortGen -> y

SortGen em_x ojc_x -> case y of

NoSortGen -> x

SortGen em_y ojc_y -> SortGen (f em_x em_y) (f ojc_x ojc_y)

data CASL_SL a = CASL_SL

{ sub_features :: SubsortingFeatures, -- ^ subsorting

has_part :: Bool, -- ^ partiality

cons_features :: SortGenerationFeatures, -- ^ sort generation constraints

has_eq :: Bool, -- ^ equality

has_pred :: Bool, -- ^ predicates

which_logic :: CASL_Formulas, -- ^ first order sublogics

has_empty_sorts :: Bool, -- ^ may sorts be empty

ext_features :: a -- ^ features of extension

} deriving (Show, Eq, Ord)

type CASL_Sublogics = CASL_SL ()

{- -----------------------

old selector functions

----------------------- -}

has_sub :: CASL_SL a -> Bool

has_sub sl = case sub_features sl of

NoSub -> False

_ -> True

has_cons :: CASL_SL a -> Bool

has_cons sl = case cons_features sl of

NoSortGen -> False

_ -> True

{- ---------------------------------------------------------------------------

Special sublogics elements

--------------------------------------------------------------------------- -}

-- top element

top :: Lattice a => CASL_SL a

top = CASL_SL Sub True (SortGen False False) True True SOL True ctop

caslTop :: Lattice a => CASL_SL a

caslTop = top

{ has_empty_sorts = False

, which_logic = FOL

}

cFol :: Lattice a => CASL_SL a

cFol = caslTop

{ sub_features = NoSub -- no subsorting

, has_part = False -- no partiality

}

-- bottom element

bottom :: Lattice a => CASL_SL a

bottom = CASL_SL NoSub False NoSortGen False False Atomic False bot

need_empty_sorts :: Lattice a => CASL_SL a

need_empty_sorts = bottom { has_empty_sorts = 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 = need_horn { sub_features = Sub }

need_sul :: Lattice a => CASL_SL a

need_sul = need_horn { sub_features = LocFilSub }

-- minimal sublogic with partiality

need_part :: Lattice a => CASL_SL a

need_part = bottom { has_part = True }

emptyMapConsFeature :: SortGenerationFeatures

emptyMapConsFeature = SortGen

{ emptyMapping = True

, onlyInjConstrs = False }

-- minimal sublogics with sort generation constraints

need_cons :: Lattice a => CASL_SL a

need_cons = bottom

{ cons_features = SortGen { emptyMapping = False

, onlyInjConstrs = False} }

need_e_cons :: Lattice a => CASL_SL a

need_e_cons = bottom

{ cons_features = emptyMapConsFeature }

need_s_cons :: Lattice a => CASL_SL a

need_s_cons = bottom

{ cons_features = SortGen { emptyMapping = False

, onlyInjConstrs = True} }

need_se_cons :: Lattice a => CASL_SL a

need_se_cons = bottom

{ cons_features = SortGen { emptyMapping = True

, onlyInjConstrs = True} }

-- minimal sublogic with equality

need_eq :: Lattice a => CASL_SL a

need_eq = bottom { has_eq = True }

-- minimal sublogic with predicates

need_pred :: Lattice a => CASL_SL a

need_pred = bottom { has_pred = True }

need_horn :: Lattice a => CASL_SL a

need_horn = bottom { which_logic = Horn }

need_fol :: Lattice a => CASL_SL a

need_fol = bottom { which_logic = 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 :: [a] -> [CASL_SL a]

sublogics_all l = let bools = [True, False] in

[ CASL_SL

{ sub_features = s_f

, ext_features = a

, has_part = pa_b

, cons_features = c_f

, has_eq = e_b

, has_pred = pr_b

, has_empty_sorts = es_b

, which_logic = fo

}

| s_f <- [NoSub, LocFilSub, Sub]

, pa_b <- bools

, pr_b <- bools

, e_b <- bools

, fo <- [SOL, FOL, GHorn, Horn, Atomic]

, es_b <- bools

, a <- l

, c_f <- NoSortGen : [ SortGen m s | m <- bools, s <- bools]

]

{- ----------------------------------------------------------------------------

Conversion functions (to String)

---------------------------------------------------------------------------- -}

formulas_name :: Bool -> CASL_Formulas -> String

formulas_name b f = case (b, f) of

(True, SOL) -> "SOL"

(False, SOL) -> "SOAlg"

(True, FOL) -> "FOL"

(False, FOL) -> "FOAlg"

(True, GHorn) -> "GHorn"

(False, GHorn) -> "GCond"

(True, Horn) -> "Horn"

(False, Horn) -> "Cond"

(True, Atomic) -> "Atom"

(False, Atomic) -> "Eq"

sublogics_name :: (a -> String) -> CASL_SL a -> String

sublogics_name f x = f (ext_features x)

++ (case sub_features x of

NoSub -> ""

LocFilSub -> "Sul"

Sub -> "Sub")

++ (if has_part x then "P" else "")

++ (if has_cons x

then (if onlyInjConstrs (cons_features x)

then "s" else "") ++

(if emptyMapping (cons_features x)

then "e" else "") ++ "C"

else "")

++ formulas_name (has_pred x) (which_logic x)

++ (if has_eq x then "=" else "")

++ if has_empty_sorts x then "E" else ""

{- ----------------------------------------------------------------------------

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 jB jS jC jF jE a b = CASL_SL

{ sub_features = jS (sub_features a) (sub_features b)

, ext_features = jE (ext_features a) (ext_features b)

, has_part = jB (has_part a) $ has_part b

, cons_features = jC (cons_features a) (cons_features b)

, has_eq = jB (has_eq a) $ has_eq b

, has_pred = jB (has_pred a) $ has_pred b

, has_empty_sorts = jB (has_empty_sorts a) $ has_empty_sorts b

, which_logic = jF (which_logic a) (which_logic b)

}

sublogics_max :: Lattice a => CASL_SL a -> CASL_SL a

-> CASL_SL a

sublogics_max = sublogics_join max max (joinSortGenFeature min) max cjoin

{- ----------------------------------------------------------------------------

Helper functions

---------------------------------------------------------------------------- -}

-- compute sublogics from a list of sublogics

comp_list :: Lattice a => [CASL_SL a] -> CASL_SL a

comp_list = foldl sublogics_max 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 [] _ _ = []

mapMaybePos (p1 : pl) f [] = (Nothing, p1) : mapMaybePos pl f []

mapMaybePos (p1 : pl) f (h : t) = let res = f h in

(if isJust res then ((res, p1) :) else id) $ mapMaybePos pl f 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 c (Range p) f l = let

(res, pos) = unzip $ mapMaybePos (drop c p) f l

in

(catMaybes res, Range (take c p ++ 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 ff (isCompound, leftImp) phi =

case phi of

Quantification q _ f _ ->

let ql = sl_form_level ff (isCompound, leftImp) f

in if is_atomic_q q then ql else max FOL ql

Junction j l _ -> maximum $ case j of

Con -> map (sl_form_level ff (True, leftImp)) l

Dis -> FOL : map (sl_form_level ff (False, False)) l

Relation l1 c l2 _ -> maximum $ sl_form_level ff (True, True) l1

: case c of

Equivalence -> [ sl_form_level ff (True, True) l2

, if leftImp then FOL else GHorn ]

_ -> [ sl_form_level ff (True, False) l2

, if leftImp then FOL else

if isCompound then GHorn else Horn ]

Negation f _ -> max FOL $ sl_form_level ff (False, False) f

Atom b _ -> if b then Atomic else FOL

Predication _ _ _ -> Atomic

Definedness _ _ -> Atomic

Equation _ e _ _ -> if e == Existl then Atomic else

if leftImp then FOL else Horn

Membership _ _ _ -> Atomic

Sort_gen_ax _ _ -> Atomic

QuantOp _ _ _ -> SOL -- it can't get worse

QuantPred _ _ _ -> SOL

ExtFORMULA f -> ff f

_ -> error "CASL.Sublogic.sl_form_level: illegal FORMULA type"

-- QUANTIFIER

is_atomic_q :: QUANTIFIER -> Bool

is_atomic_q Universal = True

is_atomic_q _ = 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 ff f = bottom

{ which_logic = sl_form_level (which_logic . ff) (False, False) 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 ff f = bottom

{ which_logic =

max Horn $ sl_form_level (which_logic . ff) (False, False) 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 bf sf ff (Basic_spec l) =

comp_list $ map (sl_basic_items bf sf ff . item) 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 bf sf ff bi = case bi of

Sig_items i -> sl_sig_items sf ff i

Free_datatype sk l _ -> needsEmptySorts sk

$ comp_list $ map (sl_datatype_decl . item) l

Sort_gen l _ -> sublogics_max need_cons

$ comp_list $ map (sl_sig_items sf ff . item) l

Var_items l _ -> comp_list $ map sl_var_decl l

Local_var_axioms d l _ -> comp_list

$ map sl_var_decl d ++ map (sl_formula ff . item) l

Axiom_items l _ -> comp_list $ map (sl_formula ff . item) l

Ext_BASIC_ITEMS b -> bf b

needsEmptySorts :: Lattice a => SortsKind -> CASL_SL a -> CASL_SL a

needsEmptySorts sk = case sk of

NonEmptySorts -> id

PossiblyEmptySorts -> sublogics_max 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 sf ff si = case si of

Sort_items sk l _ -> needsEmptySorts sk

$ comp_list $ map (sl_sort_item ff . item) l

Op_items l _ -> comp_list $ map (sl_op_item ff . item) l

Pred_items l _ -> comp_list $ map (sl_pred_item ff . item) l

Datatype_items sk l _ -> needsEmptySorts sk

$ comp_list $ map (sl_datatype_decl . item) l

Ext_SIG_ITEMS s -> sf 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 ff si = case si of

Subsort_decl _ _ _ -> need_sub

Subsort_defn _ _ _ f _ -> sublogics_max

(get_logic_sd ff $ item f)

(sublogics_max need_sub

(sl_formula ff $ item f))

Iso_decl _ _ -> need_sub

_ -> bottom

sl_op_item :: Lattice a => (f -> CASL_SL a)

-> OP_ITEM f -> CASL_SL a

sl_op_item ff oi = case oi of

Op_decl _ t l _ -> sublogics_max (sl_op_type t)

(comp_list $ map (sl_op_attr ff) l)

Op_defn _ h t _ -> sublogics_max (sl_op_head h)

(sl_term ff $ item t)

sl_op_attr :: Lattice a => (f -> CASL_SL a)

-> OP_ATTR f -> CASL_SL a

sl_op_attr ff oa = case oa of

Unit_op_attr t -> sl_term ff t

_ -> need_eq

sl_op_type :: Lattice a => OP_TYPE -> CASL_SL a

sl_op_type ot = case ot of

Op_type Partial _ _ _ -> need_part

_ -> bottom

sl_op_head :: Lattice a => OP_HEAD -> CASL_SL a

sl_op_head oh = case oh of

Op_head Partial _ _ _ -> need_part

_ -> bottom

sl_pred_item :: Lattice a => (f -> CASL_SL a)

-> PRED_ITEM f -> CASL_SL a

sl_pred_item ff i = case i of

Pred_decl _ _ _ -> need_pred

Pred_defn _ _ f _ -> sublogics_max need_pred (sl_formula ff $ item f)

sl_datatype_decl :: Lattice a => DATATYPE_DECL -> CASL_SL a

sl_datatype_decl (Datatype_decl _ l _) =

comp_list $ map (sl_alternative . item) l

sl_alternative :: Lattice a => ALTERNATIVE -> CASL_SL a

sl_alternative a = case a of

Alt_construct Total _ l _ -> comp_list $ map sl_components l

Alt_construct Partial _ _ _ -> need_part

Subsorts _ _ -> need_sub

sl_components :: Lattice a => COMPONENTS -> CASL_SL a

sl_components c = case c of

Cons_select Partial _ _ _ -> need_part

_ -> bottom

sl_var_decl :: Lattice a => VAR_DECL -> CASL_SL a

sl_var_decl _ = 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 -}

sl_term :: Lattice a => (f -> CASL_SL a) -> TERM f -> CASL_SL a

-- the subterms may make it worse than "need_part"

sl_term ff trm = case trm of

Cast t _ _ -> sublogics_max need_part $ sl_term ff t

-- check here also for the formula_level!

Conditional t f u _ ->

comp_list [sl_term ff t, sl_formula ff f, sl_term ff u]

Sorted_term t _ _ -> sl_term ff t

Application _ l _ -> comp_list $ map (sl_term ff) l

Qual_var _ _ _ -> bottom

_ -> error "CASL.Sublogic.sl_term"

sl_formula :: Lattice a => (f -> CASL_SL a)

-> FORMULA f -> CASL_SL a

sl_formula ff f = sublogics_max (get_logic ff f) (sl_form ff f)

sl_form :: Lattice a => (f -> CASL_SL a)

-> FORMULA f -> CASL_SL a

sl_form ff frm = case frm of

Quantification _ _ f _ -> sl_form ff f

Junction _ l _ -> comp_list $ map (sl_form ff) l

Relation f _ g _ -> sublogics_max (sl_form ff f) (sl_form ff g)

Negation f _ -> sl_form ff f

Atom _ _ -> bottom

Predication _ l _ -> comp_list $ need_pred : map (sl_term ff) l

-- need_part is tested elsewhere (need_pred not required)

Definedness t _ -> sl_term ff t

Equation t _ u _ -> comp_list [need_eq, sl_term ff t, sl_term ff u]

-- need_sub is tested elsewhere (need_pred not required)

Membership t _ _ -> sl_term ff t

Sort_gen_ax constraints _ -> case recover_Sort_gen_ax constraints of

(_, ops, m) -> case (m, filter (\ o -> case o of

Op_name _ -> True

Qual_op_name n _ _ ->

not (isInjName n)) ops) of

([], []) -> need_se_cons

([], _) -> need_e_cons

(_, []) -> need_s_cons

_ -> need_cons

QuantOp _ _ f -> sl_form ff f

QuantPred _ _ f -> sublogics_max need_pred $ sl_form ff f

ExtFORMULA f -> ff f

_ -> error "CASL.Sublogic.sl_form"

sl_symb_items :: Lattice a => SYMB_ITEMS -> CASL_SL a

sl_symb_items (Symb_items k l _) = sublogics_max (sl_symb_kind k)

(comp_list $ map sl_symb l)

sl_symb_kind :: Lattice a => SYMB_KIND -> CASL_SL a

sl_symb_kind pk = case pk of

Preds_kind -> need_pred

_ -> bottom

sl_symb :: Lattice a => SYMB -> CASL_SL a

sl_symb s = case s of

Symb_id _ -> bottom

Qual_id _ t _ -> sl_type t

sl_type :: Lattice a => TYPE -> CASL_SL a

sl_type ty = case ty of

O_type t -> sl_op_type t

P_type _ -> need_pred

_ -> bottom

sl_symb_map_items :: Lattice a => SYMB_MAP_ITEMS -> CASL_SL a

sl_symb_map_items (Symb_map_items k l _) = sublogics_max (sl_symb_kind k)

(comp_list $ map sl_symb_or_map l)

sl_symb_or_map :: Lattice a => SYMB_OR_MAP -> CASL_SL a

sl_symb_or_map syms = case syms of

Symb s -> sl_symb s

Symb_map s t _ -> sublogics_max (sl_symb s) (sl_symb t)

{- the maps have no influence since all sorts, ops, preds in them

must also appear in the signatures, so any features needed by

them will be included by just checking the signatures -}

sl_sign :: Lattice a => Sign f e -> CASL_SL a

sl_sign s =

let rel = sortRel s

subs | Rel.noPairs rel = bottom

| Rel.locallyFiltered rel = need_sul

| otherwise = need_sub

esorts = if Set.null $ emptySortSet s then bottom

else need_empty_sorts

preds = if MapSet.null $ predMap s then bottom else need_pred

partial = if any isPartial $ Set.toList

$ MapSet.elems $ opMap s then need_part else bottom

in comp_list [subs, esorts, preds, partial]

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

sl_sentence = sl_formula

sl_morphism :: Lattice a => Morphism f e m -> CASL_SL a

sl_morphism m = sublogics_max (sl_sign $ msource m) (sl_sign $ mtarget m)

sl_symbol :: Lattice a => Symbol -> CASL_SL a

sl_symbol (Symbol _ t) = sl_symbtype t

sl_symbtype :: Lattice a => SymbType -> CASL_SL a

sl_symbtype st = case st of

OpAsItemType t -> sl_optype t

PredAsItemType _ -> need_pred

_ -> bottom

sl_optype :: Lattice a => OpType -> CASL_SL a

sl_optype = sl_opkind . opKind

sl_opkind :: Lattice a => OpKind -> CASL_SL a

sl_opkind fk = case fk of

Partial -> need_part

_ -> bottom

{- ----------------------------------------------------------------------------

projection functions

---------------------------------------------------------------------------- -}

sl_in :: Lattice a => CASL_SL a -> CASL_SL a -> Bool

sl_in given new = sublogics_max given new == given

in_x :: Lattice a => CASL_SL a -> b -> (b -> CASL_SL a) -> Bool

in_x l x f = sl_in l (f 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 sl f a =

fmap (`replaceAnnoted` a) $ f sl (item 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 sl f a =

let (res, lst) = f sl (item a)

in (fmap (`replaceAnnoted` a) res

, 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 l f e = if in_x l e f then Just e else Nothing

checkRecord :: CASL_SL a -> (CASL_SL a -> f -> Maybe (FORMULA f))

-> Record f (FORMULA f) (TERM f)

checkRecord l ff = (mapRecord id)

{ foldExtFORMULA = \ o _ -> case o of

ExtFORMULA f -> fromMaybe (error "checkRecord") $ ff l f

_ -> error "checkRecord.foldExtFORMULA" }

toCheck :: Lattice a => CASL_SL a

-> (CASL_SL a -> f -> Maybe (FORMULA f))

-> f -> CASL_SL a

toCheck l ff = maybe top (const l) . ff l

pr_formula :: Lattice a => (CASL_SL a -> f -> Maybe (FORMULA f))

-> CASL_SL a -> FORMULA f -> Maybe (FORMULA f)

pr_formula ff l =

fmap (foldFormula $ checkRecord l ff)

. pr_check l (sl_formula $ toCheck l ff)

pr_term :: Lattice a => (CASL_SL a -> f -> Maybe (FORMULA f))

-> CASL_SL a -> TERM f -> Maybe (TERM f)

pr_term ff l =

fmap (foldTerm $ checkRecord l ff)

. pr_check l (sl_term $ toCheck l ff)

-- make full Annoted Sig_items out of a SORT list

pr_make_sorts :: [SORT] -> Annoted (BASIC_ITEMS b s f)

pr_make_sorts s =

Annoted (Sig_items (Sort_items NonEmptySorts

[Annoted (Sort_decl s nullRange) nullRange [] []]

nullRange))

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 fb fs ff l (Basic_spec s) =

let

res = map (pr_annoted_dt l $ pr_basic_items fb fs ff) s

items = mapMaybe fst res

toAdd = concatMap snd res

ret = if null toAdd then

items

else

pr_make_sorts toAdd : items

in

Basic_spec 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 fb fs ff l bi = case bi of

Sig_items s ->

let

(res, lst) = pr_sig_items fs ff l s

in

if isNothing res then

(Nothing, lst)

else

(Just (Sig_items (fromJust res)), lst)

Free_datatype sk d p ->

let

(res, pos) = mapPos 2 p (pr_annoted l pr_datatype_decl) d

lst = pr_lost_dt l (map item d)

in

if null res then

(Nothing, lst)

else

(Just (Free_datatype sk res pos), lst)

Sort_gen s p ->

if has_cons l then

let

tmp = map (pr_annoted_dt l $ pr_sig_items fs ff) s

res = mapMaybe fst tmp

lst = concatMap snd tmp

in

if null res then

(Nothing, lst)

else

(Just (Sort_gen res p), lst)

else

(Nothing, [])

Var_items v p -> (Just (Var_items v p), [])

Local_var_axioms v f p ->

let

(res, pos) = mapPos (length v) p

(pr_annoted l $ pr_formula ff) f

in

if null res then

(Nothing, [])

else

(Just (Local_var_axioms v res pos), [])

Axiom_items f p ->

let

(res, pos) = mapPos 0 p (pr_annoted l $ pr_formula ff) f

in

if null res then

(Nothing, [])

else

(Just (Axiom_items res pos), [])

Ext_BASIC_ITEMS b -> fb l b

pr_datatype_decl :: CASL_SL a -> DATATYPE_DECL -> Maybe DATATYPE_DECL

pr_datatype_decl l (Datatype_decl s a p) =

let

(res, pos) = mapPos 1 p (pr_annoted l pr_alternative) a

in

if null res then

Nothing

else

Just (Datatype_decl s res pos)

pr_alternative :: CASL_SL a -> ALTERNATIVE -> Maybe ALTERNATIVE

pr_alternative l alt = case alt of

Alt_construct Total n c p ->

let

(res, pos) = mapPos 1 p (pr_components l) c

in

if null res then

Nothing

else

Just (Alt_construct Total n res pos)

Alt_construct Partial _ _ _ ->

if has_part l then

Just alt

else

Nothing

Subsorts s p ->

if has_sub l then

Just (Subsorts s p)

else

Nothing

pr_components :: CASL_SL a -> COMPONENTS -> Maybe COMPONENTS

pr_components l sel = case sel of

Cons_select Partial _ _ _ ->

if has_part l then

Just sel

else

Nothing

_ -> Just 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 sl = concatMap (\ dt@(Datatype_decl s _ _) ->

case pr_datatype_decl sl dt of

Nothing -> [s]

_ -> [])

pr_symbol :: Lattice a => CASL_SL a -> Symbol -> Maybe Symbol

pr_symbol l = pr_check l 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 sf ff l si = case si of

Sort_items sk s p ->

let

(res, pos) = mapPos 1 p (pr_annoted l pr_sort_item) s

in

if null res then

(Nothing, [])

else

(Just (Sort_items sk res pos), [])

Op_items o p ->

let

(res, pos) = mapPos 1 p (pr_annoted l $ pr_op_item ff) o

in

if null res then

(Nothing, [])

else

(Just (Op_items res pos), [])

Pred_items i p ->

if has_pred l then

(Just (Pred_items i p), [])

else

(Nothing, [])

Datatype_items sk d p ->

let

(res, pos) = mapPos 1 p (pr_annoted l pr_datatype_decl) d

lst = pr_lost_dt l (map item d)

in

if null res then

(Nothing, lst)

else

(Just (Datatype_items sk res pos), lst)

Ext_SIG_ITEMS s -> sf l 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 ff l oi = case oi of

Op_defn o h f r -> do

g <- pr_annoted l (pr_term ff) f

return $ Op_defn o h g r

_ -> Just 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 _ (Sort_decl s p) = Just (Sort_decl s p)

pr_sort_item l (Subsort_decl sl s p) =

if has_sub l then

Just (Subsort_decl sl s p)

else

Just (Sort_decl (s : sl) nullRange)

pr_sort_item l (Subsort_defn s1 v s2 f p) =

if has_sub l then

Just (Subsort_defn s1 v s2 f p)

else

Just (Sort_decl [s1] nullRange)

pr_sort_item _ (Iso_decl s p) = Just (Iso_decl s p)

pr_symb_items :: Lattice a => CASL_SL a -> SYMB_ITEMS

-> Maybe SYMB_ITEMS

pr_symb_items l (Symb_items k s p) =

if in_x l k sl_symb_kind then

let

(res, pos) = mapPos 1 p (pr_symb l) s

in

if null res then

Nothing

else

Just (Symb_items k res pos)

else

Nothing

pr_symb_map_items :: Lattice a => CASL_SL a -> SYMB_MAP_ITEMS

-> Maybe SYMB_MAP_ITEMS

pr_symb_map_items l (Symb_map_items k s p) =

if in_x l k sl_symb_kind then

let

(res, pos) = mapPos 1 p (pr_symb_or_map l) s

in

if null res then

Nothing

else

Just (Symb_map_items k res pos)

else

Nothing

pr_symb_or_map :: Lattice a => CASL_SL a -> SYMB_OR_MAP

-> Maybe SYMB_OR_MAP

pr_symb_or_map l (Symb s) =

let

res = pr_symb l s

in

if isNothing res then

Nothing

else

Just (Symb (fromJust res))

pr_symb_or_map l (Symb_map s t p) =

let

a = pr_symb l s

b = pr_symb l t

in

if isJust a && isJust b then

Just (Symb_map s t p)

else

Nothing

pr_symb :: Lattice a => CASL_SL a -> SYMB -> Maybe SYMB

pr_symb _ (Symb_id i) = Just (Symb_id i)

pr_symb l (Qual_id i t p) =

if in_x l t sl_type then

Just (Qual_id i t p)

else

Nothing

pr_sign :: CASL_SL a -> Sign f e -> Sign f e

pr_sign _sl s = s -- do something here

pr_morphism :: Lattice a => CASL_SL a -> Morphism f e m

-> Morphism f e m

pr_morphism l m =

m { msource = pr_sign l $ msource m

, mtarget = pr_sign l $ mtarget m

, op_map = pr_op_map l $ op_map m

, pred_map = pr_pred_map l $ pred_map 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 l x = if has_pred l then x else Map.empty

pr_op_map :: Lattice a => CASL_SL a -> Op_map -> Op_map

pr_op_map = Map.filterWithKey . pr_op_map_entry

pr_op_map_entry :: Lattice a => CASL_SL a -> (Id, OpType) -> (Id, OpKind)

-> Bool

pr_op_map_entry l (_, t) (_, b) =

has_part l || in_x l t sl_optype && b == 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 extEm l s = embedMorphism extEm s $ pr_sign l s