instance Lattice Bool where
------------------------------------------------------------------------------
-- datatypes for CASL sublogics
------------------------------------------------------------------------------
data CASL_Formulas = Atomic -- ^ atomic logic
| Horn -- ^ positive conditional logic
| GHorn -- ^ generalized positive conditional logic
| FOL -- ^ first-order logic
data SubsortingFeatures = NoSub
data SortGenerationFeatures =
| SortGen { emptyMapping :: Bool
-- ^ Mapping of indexed sorts is empty
-- ^ only injective constructors
} deriving (Show, Eq, Ord)
joinSortGenFeature :: (Bool -> Bool -> Bool)
-> SortGenerationFeatures -> SortGenerationFeatures
-> SortGenerationFeatures
joinSortGenFeature f x y =
SortGen em_x ojc_x -> case y of
SortGen em_y ojc_y -> SortGen (f em_x em_y) (f ojc_x ojc_y)
{ 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
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
has_cons :: CASL_SL a -> Bool
has_cons sl = case cons_features sl of
-----------------------------------------------------------------------------
-- Special sublogics elements
-----------------------------------------------------------------------------
top :: Lattice a => CASL_SL a
top = (CASL_SL Sub True (SortGen False False) True True FOL ctop)
bottom :: Lattice a => CASL_SL a
bottom = (CASL_SL NoSub False (NoSortGen) False False Atomic bot)
-- 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
-- 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 }
-- minimal sublogics with sort generation constraints
need_cons :: Lattice a => CASL_SL a
{ cons_features = SortGen { emptyMapping = False
, onlyInjConstrs = False} }
need_e_cons :: Lattice a => CASL_SL a
{ cons_features = SortGen { emptyMapping = True
, onlyInjConstrs = False} }
need_s_cons :: Lattice a => CASL_SL a
{ cons_features = SortGen { emptyMapping = False
, onlyInjConstrs = True} }
need_se_cons :: Lattice a => CASL_SL a
{ 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_ghorn :: Lattice a => CASL_SL a
need_ghorn = bottom { which_logic = GHorn }
need_fol :: Lattice a => CASL_SL a
need_fol = bottom { which_logic = FOL }
-----------------------------------------------------------------------------
-- Functions to generate a list of all sublogics for CASL
-----------------------------------------------------------------------------
-- 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
| s_f <- [NoSub, LocFilSub, Sub]
, fo <- [FOL, GHorn, Horn, Atomic]
, c_f <- NoSortGen : [ SortGen m s | m <- bools, s <- bools]
------------------------------------------------------------------------------
-- Conversion functions (to String)
------------------------------------------------------------------------------
formulas_name :: Bool -> CASL_Formulas -> String
formulas_name True FOL = "FOL"
formulas_name False FOL = "FOAlg"
formulas_name True GHorn = "GHorn"
formulas_name False GHorn = "GCond"
formulas_name True Horn = "Horn"
formulas_name False Horn = "Cond"
formulas_name True Atomic = "Atom"
formulas_name False Atomic = "Eq"
sublogics_name :: (a -> String) -> CASL_SL a -> [String]
sublogics_name f x = [ f (ext_features x)
++ ( case sub_features x of
++ ( if (has_part x) then "P" else "")
then ( (if onlyInjConstrs (cons_features x)
++(if emptyMapping (cons_features x)
++ ( formulas_name (has_pred x) (which_logic x) )
++ ( if (has_eq x) then "=" else "")]
------------------------------------------------------------------------------
------------------------------------------------------------------------------
sublogics_join :: (Bool -> Bool -> Bool)
-> (SubsortingFeatures -> SubsortingFeatures
-> (SortGenerationFeatures -> SortGenerationFeatures
-> SortGenerationFeatures)
-> (CASL_Formulas -> CASL_Formulas -> CASL_Formulas)
-> 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
, which_logic = jF (which_logic a) (which_logic b)
sublogics_max :: Lattice a => CASL_SL a -> CASL_SL a
sublogics_max = sublogics_join max max (joinSortGenFeature min) max cjoin
------------------------------------------------------------------------------
------------------------------------------------------------------------------
-- compute sublogics from a list of sublogics
comp_list :: Lattice a => [CASL_SL a] -> CASL_SL a
comp_list l = foldl sublogics_max bottom l
-- 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
-- . 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 (p1:pl) f [] = (Nothing,p1):(mapMaybePos pl f [])
mapMaybePos (p1:pl) f (h:t) = let
(res,p1):(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
mapPos :: Int -> Range -> (a -> Maybe b) -> [a] -> ([b],Range)
mapPos c (Range p) f l = let
(res,pos) = (\(x,y) -> (catMaybes x,y))
$ unzip $ mapMaybePos (drop c p) f l
(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
--------------------------------------------------------------------------- -}
sl_form_level :: Lattice a => (f -> CASL_SL a)
-> (Bool, Bool) -> FORMULA f -> CASL_SL a
sl_form_level ff (isCompound, leftImp) phi =
Quantification q _ f _ ->
then sl_form_level ff (isCompound, leftImp) f
Conjunction l _ -> comp_list $ map (sl_form_level ff (True, leftImp)) l
Disjunction _ _ -> need_fol
Implication l1 l2 _ _ -> if leftImp then need_fol else
comp_list [sl_form_level ff (True, True) l1,
sl_form_level ff (True, False) l2,
else comp_list [sl_form_level ff (True, True) l1,
sl_form_level ff (True, True) l2,
Negation _ _ -> need_fol -- it won't get worse
Predication _ _ _ -> bottom
Definedness _ _ -> bottom
Existl_equation _ _ _ -> bottom
Strong_equation _ _ _ -> if leftImp then need_fol else need_horn
Membership _ _ _ -> bottom
Sort_gen_ax _ _ -> bottom
is_atomic_q :: QUANTIFIER -> Bool
is_atomic_q (Universal) = True
-- 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 = sl_form_level ff (False, False)
-- for the formula inside a subsort-defn
get_logic_sd :: Lattice a => (f -> CASL_SL a)
-> FORMULA f -> CASL_SL a
sublogics_max need_horn $ sl_form_level ff (False, False) f
{- get_logic_sd f = if (is_horn_p_a f) then need_horn else
if (is_ghorn_prem f) then need_ghorn else
------------------------------------------------------------------------------
-- 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)
-> 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) $ map item l
sl_basic_items :: Lattice a => (b -> 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 l _ -> comp_list $ map sl_datatype_decl
Sort_gen l _ -> sublogics_max need_cons
(comp_list $ map (sl_sig_items sf ff)
Var_items l _ -> comp_list $ map sl_var_decl l
Local_var_axioms d l _ -> sublogics_max
(comp_list $ map sl_var_decl d)
(comp_list $ map (sl_formula ff)
Axiom_items l _ -> comp_list $ map (sl_formula ff) $ map item l
Ext_BASIC_ITEMS b -> bf b
sl_sig_items :: Lattice a => (s -> CASL_SL a)
-> SIG_ITEMS s f -> CASL_SL a
sl_sig_items sf ff si = case si of
Sort_items l _ -> comp_list $ map (sl_sort_item ff) $ map item l
Op_items l _ -> comp_list $ map (sl_op_item ff) $ map item l
Pred_items l _ -> comp_list $ map (sl_pred_item ff) $ map item l
Datatype_items l _ -> comp_list $ map sl_datatype_decl $ map item l
-- 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)
(sl_formula ff $ item f))
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_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
sl_op_type :: Lattice a => OP_TYPE -> CASL_SL a
sl_op_type ot = case ot of
Op_type Partial _ _ _ -> need_part
sl_op_head :: Lattice a => OP_HEAD -> CASL_SL a
sl_op_head oh = case oh of
Op_head Partial _ _ _ -> need_part
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
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
sl_components :: Lattice a => COMPONENTS -> CASL_SL a
sl_components c = case c of
Cons_select Partial _ _ _ -> need_part
sl_var_decl :: Lattice a => VAR_DECL -> CASL_SL a
{- without subsorts casts are trivial and would not even require
need_part, but testing term_sort 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!
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
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
Conjunction l _ -> comp_list $ map (sl_form ff) l
Disjunction l _ -> comp_list $ map (sl_form ff) l
Implication f g _ _ -> sublogics_max (sl_form ff f) (sl_form ff g)
Equivalence f g _ -> sublogics_max (sl_form ff f) (sl_form ff g)
Negation f _ -> sl_form ff f
Predication _ l _ -> sublogics_max need_pred
(comp_list $ map (sl_term ff) l)
-- need_part is tested elsewhere (need_pred not required)
Definedness t _ -> sl_term ff t
Existl_equation t u _ -> comp_list [need_eq, sl_term ff t, sl_term ff u]
Strong_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
| null mapping && null otherConstrs -> need_se_cons
| null mapping && not (null otherConstrs) -> need_e_cons
| not (null mapping) && null otherConstrs -> need_s_cons
Qual_op_name n _ _ -> n /= injName) ops
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
sl_symb :: Lattice a => SYMB -> CASL_SL a
Qual_id _ t _ -> sl_type t
sl_type :: Lattice a => TYPE -> CASL_SL a
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_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
preds = if
Map.null $ predMap s then bottom else need_pred
partial = if any ( \ t -> opKind t == Partial) $
Set.toList in sublogics_max subs (sublogics_max preds partial)
sl_sentence :: Lattice a => (f -> CASL_SL a)
-> FORMULA f -> CASL_SL a
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
sl_optype :: Lattice a => OpType -> CASL_SL a
sl_optype k = sl_funkind $ opKind k
sl_funkind :: Lattice a => FunKind -> CASL_SL a
sl_funkind fk = case fk of
------------------------------------------------------------------------------
------------------------------------------------------------------------------
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)
return $ replaceAnnoted res 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
pr_annoted_dt :: CASL_SL s
-> (CASL_SL s -> a -> (Maybe a, [SORT]))
-> Annoted a -> (Maybe (Annoted a), [SORT])
let (res, lst) = f sl (item a)
return $ replaceAnnoted b a
-- keep an element if its computed sublogic is in the given sublogic
pr_check :: Lattice a => CASL_SL a -> (b -> CASL_SL a)
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 = \ (ExtFORMULA f) _ ->
Nothing -> error "pr_formula"
toCheck :: Lattice a => CASL_SL a
-> (CASL_SL a -> f -> Maybe (FORMULA f))
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)
fmap (foldFormula $ checkRecord l ff)
$ pr_check l (sl_formula $ toCheck l ff) f
pr_term :: Lattice a => (CASL_SL a -> f -> Maybe (FORMULA f))
-> CASL_SL a -> TERM f -> Maybe (TERM f)
fmap (foldTerm $ checkRecord l ff)
$ pr_check l (sl_term $ toCheck l ff) f
-- make full Annoted Sig_items out of a SORT list
pr_make_sorts :: [SORT] -> Annoted (BASIC_ITEMS b s f)
Annoted (Sig_items (Sort_items
[Annoted (Sort_decl s 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) =
res = map (pr_annoted_dt l $ pr_basic_items fb fs ff) s
items = catMaybes $ map fst res
toAdd = concat $ map snd res
ret = if (toAdd==[]) then
pr_make_sorts toAdd : items
-- returns a non-empty list of [SORT] if datatypes had to be removed
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
(res, lst) = pr_sig_items fs ff l s
(Just (Sig_items (fromJust res)), lst)
(res, pos) = mapPos 2 p (pr_annoted l pr_datatype_decl) d
lst = pr_lost_dt l (map item d)
(Just (Free_datatype res pos), lst)
tmp = map (pr_annoted_dt l $ pr_sig_items fs ff) s
res = catMaybes $ map fst tmp
lst = concat $ map snd tmp
(Just (Sort_gen res p), lst)
Var_items v p -> (Just (Var_items v p), [])
Local_var_axioms v f p ->
(res, pos) = mapPos (length v) p
(pr_annoted l $ pr_formula ff) f
(Just (Local_var_axioms v res pos), [])
(res, pos) = mapPos 0 p (pr_annoted l $ pr_formula ff) f
(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) =
(res, pos) = mapPos 1 p (pr_annoted l pr_alternative) a
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 ->
(res, pos) = mapPos 1 p (pr_components l) c
Just (Alt_construct Total n res pos)
Alt_construct Partial _ _ _ ->
pr_components :: CASL_SL a -> COMPONENTS -> Maybe COMPONENTS
pr_components l sel = case sel of
Cons_select Partial _ _ _ ->
-- 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
pr_symbol :: Lattice a => CASL_SL a -> Symbol -> Maybe Symbol
pr_symbol l s = pr_check l sl_symbol s
-- returns a non-empty list of [SORT] if datatypes had to be removed
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
(res, pos) = mapPos 1 p (pr_annoted l pr_sort_item) s
(Just (Sort_items res pos), [])
(res, pos) = mapPos 1 p (pr_annoted l $ pr_op_item ff) o
(Just (Op_items res pos), [])
(Just (Pred_items i p), [])
(res, pos) = mapPos 1 p (pr_annoted l pr_datatype_decl) d
lst = pr_lost_dt l (map item d)
(Just (Datatype_items 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
g <- pr_annoted l (pr_term ff) f
-- subsort declarations and definitions are reduced to simple
-- sort declarations if the sublogic disallows subsorting to
-- avoid loosing sorts in the projection
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) =
Just (Subsort_decl sl s p)
Just (Sort_decl (s:sl) nullRange)
pr_sort_item l (Subsort_defn s1 v s2 f p) =
Just (Subsort_defn s1 v s2 f p)
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
pr_symb_items l (Symb_items k s p) =
if (in_x l k sl_symb_kind) then
(res, pos) = mapPos 1 p (pr_symb l) s
Just (Symb_items k res pos)
pr_symb_map_items :: Lattice a => CASL_SL a -> SYMB_MAP_ITEMS
pr_symb_map_items l (Symb_map_items k s p) =
if (in_x l k sl_symb_kind) then
(res, pos) = mapPos 1 p (pr_symb_or_map l) s
Just (Symb_map_items k res pos)
pr_symb_or_map :: Lattice a => CASL_SL a -> SYMB_OR_MAP
pr_symb_or_map l (Symb s) =
Just (Symb (fromJust res))
pr_symb_or_map l (Symb_map s t p) =
if ((isJust a) && (isJust b)) then
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
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
m { msource = pr_sign l $ msource m
, mtarget = pr_sign l $ mtarget m
, fun_map = pr_fun_map l $ fun_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.emptypr_fun_map :: Lattice a => CASL_SL a -> Fun_map -> Fun_map
pr_fun_map_entry :: Lattice a => CASL_SL a -> (Id, OpType)
pr_fun_map_entry l (_, t) (_, b) =
if (has_part l) then True
else ((in_x l t sl_optype) && b == Partial)
-- compute a morphism that consists of the original signature
-- and the projected signature
pr_epsilon :: Ext f e m -> CASL_SL a -> Sign f e -> Morphism f e m
pr_epsilon extEm l s = embedMorphism extEm s $ pr_sign l s