-- * functions for the creation of minimal sublogics
-- * functions for Logic instance sublogic to string conversion
-- ** list of all sublogics
-- * computes the sublogic of a given element
-- * projects an element into a given sublogic
{- ----------------------------------------------------------------------------
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
data SubsortingFeatures = NoSub
data SortGenerationFeatures =
| SortGen { emptyMapping :: Bool
-- ^ Mapping of indexed sorts is empty
-- ^ only constructors that are subsort injections
} 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
has_empty_sorts :: Bool, -- ^ may sorts be empty
ext_features :: a -- ^ features of extension
} deriving (Show, Eq, Ord)
updExtFeature :: (a -> a) -> CASL_SL a -> CASL_SL a
updExtFeature f s = s { ext_features = f $ ext_features s }
type CASL_Sublogics = CASL_SL ()
{- -----------------------
----------------------- -}
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
--------------------------------------------------------------------------- -}
mkTop = CASL_SL Sub True (SortGen False False) True True SOL True
top :: Lattice a => CASL_SL a
caslTop :: Lattice a => CASL_SL a
{ has_empty_sorts = False
cFol :: Lattice a => CASL_SL a
{ sub_features = NoSub -- no subsorting
, has_part = False -- no partiality
mkBot = CASL_SL NoSub False NoSortGen False False Atomic False
bottom :: Lattice a => CASL_SL a
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
-- 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
, onlyInjConstrs = False }
-- 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 = emptyMapConsFeature }
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_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 :: Lattice a => [a] -> [CASL_SL a]
sublogics_all l = bottom : map mkBot l ++ concat (sDims [])
++ let subPAtom = (sublogics_max need_part need_pred) { sub_features = Sub } in
[ sublogics_max need_fol need_eq
, comp_list [subPAtom, need_horn, need_eq]
, sublogics_max subPAtom need_cons
sDims :: Lattice a => [[a]] -> [[CASL_SL a]]
[ [ b { sub_features = s_f } | s_f <- [LocFilSub, Sub]]
, [b { cons_features = c_f } | c_f <- [ SortGen m s | m <- bools, s <- bools]]
, [b { has_empty_sorts = t } ]
, [b { which_logic = fo } | fo <- reverse [SOL, FOL, GHorn, Horn]]]
{- ----------------------------------------------------------------------------
Conversion functions (to String)
---------------------------------------------------------------------------- -}
formulas_name :: Bool -> CASL_Formulas -> String
formulas_name b f = let Just s = lookup (b, f) nameList in s
nameList :: [((Bool, CASL_Formulas), String)]
, ((False, SOL), "SOAlg")
, ((False, FOL), "FOAlg")
, ((True, GHorn), "GHorn")
, ((False, GHorn), "GCond")
, ((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
++ (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 "")
++ if has_empty_sorts x then "E" else ""
parseBool :: String -> String -> (Bool, String)
parseBool p s = case stripPrefix p s of
parseSL :: (String -> Maybe (a, String)) -> String -> Maybe (CASL_SL a)
(sub, s2) <- case stripPrefix "Su" s1 of
'l' -> Just (LocFilSub, t)
Nothing -> Just (NoSub, s1)
let (pa, s3) = parseBool "P" s2
((pr, l), s5) <- parseForm s4
let (eq, s6) = parseBool "=" s5
(es, s7) = parseBool "E" s6
parseForm :: String -> Maybe ((Bool, CASL_Formulas), String)
parseForm s = foldr (\ (q, p) m -> case m of
Nothing -> case stripPrefix p s of
Nothing -> m) Nothing nameList
parseCons :: String -> (SortGenerationFeatures, String)
parseCons s = case stripPrefix "seC" s of
Just r -> (SortGen True True, r)
Nothing -> case stripPrefix "sC" s of
Just r -> (SortGen False True, r)
Nothing -> case stripPrefix "eC" s of
Just r -> (SortGen True False, r)
Nothing -> case stripPrefix "C" s of
Just r | not $ isPrefixOf "ond" r -> (SortGen False False, r)
{- ----------------------------------------------------------------------------
---------------------------------------------------------------------------- -}
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
, 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
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 = 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
. 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 = 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]
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) = unzip $ mapMaybePos (drop c p) f l
(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
--------------------------------------------------------------------------- -}
sl_form_level :: (f -> CASL_Formulas)
-> (Bool, Bool) -> FORMULA f -> CASL_Formulas
sl_form_level ff (isCompound, leftImp) phi =
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
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
QuantOp {} -> SOL -- it can't get worse
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
{ 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
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)
-> 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)
-> 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_se_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
PossiblyEmptySorts -> sublogics_max need_empty_sorts
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 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
{- 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_sul
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 . 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
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 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 ff = (constRecord ff comp_list bottom)
{ foldPredication = \ _ _ l _ -> comp_list $ need_pred : l
, foldEquation = \ _ t _ u _ -> comp_list [need_eq, t, u]
, foldSort_gen_ax = \ _ constraints _ ->
case recover_Sort_gen_ax constraints of
(_, ops, m) -> case (m, filter (\ o -> case o of
not (isInjName n)) ops) of
, foldQuantPred = \ _ _ _ f -> sublogics_max need_pred f
, foldCast = \ _ t _ _ -> sublogics_max need_part t
sl_term :: Lattice a => (f -> CASL_SL a) -> TERM f -> CASL_SL a
sl_term = foldTerm . slRecord
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 = foldFormula . slRecord
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 => (e -> CASL_SL a) -> Sign f e -> CASL_SL a
esorts = if
Set.null $ emptySortSet s then bottom
preds = if
MapSet.null $ predMap s then bottom else need_pred
in comp_list [subs, esorts, preds, partial, f $ extendedInfo s]
sl_sentence :: Lattice a => (f -> CASL_SL a) -> FORMULA f -> CASL_SL a
sl_morphism :: Lattice a => (e -> CASL_SL a) -> Morphism f e m -> CASL_SL a
sl_morphism f m = sublogics_max (sl_sign f $ msource m) (sl_sign f $ 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 = sl_opkind . opKind
sl_opkind :: Lattice a => OpKind -> CASL_SL a
sl_opkind 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)
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
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)
in (fmap (`replaceAnnoted` a) res
-- 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 = \ o _ -> case o of
ExtFORMULA f -> fromMaybe (error "checkRecord") $ ff l f
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)
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)
-- 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 NonEmptySorts
[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
toAdd = concatMap snd res
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 sk res pos), lst)
tmp = map (pr_annoted_dt l $ pr_sig_items fs ff) s
(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 = pr_check l sl_symbol
{- 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 sk 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 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
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 -}
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) =
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) =
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
, 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.emptypr_op_map :: Lattice a => CASL_SL a -> Op_map -> Op_map
pr_op_map_entry :: Lattice a => CASL_SL a -> (Id, OpType) -> (Id, OpKind)
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