Sublogic.hs revision f6bb1e62e1d83b2c9279e3b54a2892887f1d4962
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederModule : $Header$
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederCopyright : (c) Sonja Groening, C. Maeder, and Uni Bremen 2002-2006
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederMaintainer : maeder@tzi.de
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederStability : experimental
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederPortability : portable
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederThis module provides the sublogic functions (as required by Logic.hs) for
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder HasCASL. The functions allow to compute the minimal sublogic needed by a
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder given element, to check whether an item is part of a given sublogic, and --
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder not yet -- to project an element into a given sublogic.
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder ( -- * datatypes
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , Formulas(..)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , Classes(..)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- * functions for SemiLatticeWithTop instance
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , sublogic_max
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- * combining sublogics restrictions
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , sublogic_min
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- * further sublogic constants
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- * functions for Logic instance
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- ** sublogic to string converstion
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , sublogic_name
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- ** list of all sublogics
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , sublogics_all
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- ** checks if element is in given sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , in_basicSpec
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , in_sentence
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , in_symbItems
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , in_symbMapItems
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , in_morphism
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- * computes the sublogic of a given element
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , sl_basicSpec
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , sl_sentence
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , sl_symbItems
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , sl_symbMapItems
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , sl_morphism
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederimport qualified Data.Map as Map
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederimport qualified Data.Set as Set
ba904a15082557e939db689fcfba0c68c9a4f740Christian Maeder-- | formula kinds of HasCASL sublogics
ba904a15082557e939db689fcfba0c68c9a4f740Christian Maeder = Atomic -- ^ atomic logic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder | Horn -- ^ positive conditional logic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder | GHorn -- ^ generalized positive conditional logic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder | FOL -- ^ first-order logic
ba904a15082557e939db689fcfba0c68c9a4f740Christian Maeder | HOL -- ^ higher-order logic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder deriving (Show, Eq, Ord)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederdata Classes = NoClasses | SimpleTypeClasses | ConstructorClasses
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder deriving (Show, Eq, Ord)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- | HasCASL sublogics
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederdata Sublogic = Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder { has_sub :: Bool -- ^ subsorting
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , has_part :: Bool -- ^ partiality
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , has_eq :: Bool -- ^ equality
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , has_pred :: Bool -- ^ predicates
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , type_classes :: Classes
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , has_polymorphism :: Bool
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , has_type_constructors :: Bool
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , which_logic :: Formulas
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder } deriving (Show, Eq)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- * special sublogic elements
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- | top element
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertopLogic :: Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertopLogic = Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder { has_sub = True
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , has_part = True
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , has_eq = True
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , has_pred = True
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , type_classes = ConstructorClasses
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , has_polymorphism = True
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , has_type_constructors = True
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , which_logic = HOL
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- | top sublogic without subtypes
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedernoSubtypes :: Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedernoSubtypes = topLogic { has_sub = False }
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- | top sublogic without type classes
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedernoClasses :: Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedernoClasses = topLogic { type_classes = NoClasses }
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- | top sublogic without partiality
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertotalFuns :: Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertotalFuns = topLogic { has_part = False }
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedercaslLogic :: Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedercaslLogic = noClasses
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder { has_polymorphism = False
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , has_type_constructors = False
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , which_logic = FOL
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- | bottom sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederbottom :: Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederbottom = Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder { has_sub = False
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , has_part = False
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , has_eq = False
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , has_pred = False
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , type_classes = NoClasses
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , has_polymorphism = False
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , has_type_constructors = False
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , which_logic = Atomic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder{- the following are used to add a needed feature to a given
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder sublogic via sublogic_max, i.e. (sublogic_max given needs_part)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder will force partiality in addition to what features given already
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder has included -}
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- | minimal sublogic with partiality
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederneed_part :: Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederneed_part = bottom { has_part = True }
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- | minimal sublogic with equality
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederneed_eq :: Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederneed_eq = bottom { has_eq = True }
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- | minimal sublogic with predicates
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederneed_pred :: Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederneed_pred = bottom { has_pred = True }
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- | minimal sublogic with subsorting
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederneed_sub :: Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederneed_sub = need_pred { has_sub = True }
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- | minimal sublogic with polymorhism
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederneed_polymorphism :: Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederneed_polymorphism = bottom { has_polymorphism = True }
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- | minimal sublogic with simple type classes
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedersimpleTypeClasses :: Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedersimpleTypeClasses = need_polymorphism { type_classes = SimpleTypeClasses }
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- | minimal sublogic with constructor classes
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederconstructorClasses :: Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederconstructorClasses = need_polymorphism { type_classes = ConstructorClasses }
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- | minimal sublogic with type constructors
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederneed_type_constructors :: Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederneed_type_constructors = bottom { has_type_constructors = True }
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederneed_horn :: Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederneed_horn = bottom { which_logic = Horn }
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederneed_ghorn :: Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederneed_ghorn = bottom { which_logic = GHorn }
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederneed_fol :: Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederneed_fol = bottom { which_logic = FOL }
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederneed_hol :: Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederneed_hol = need_pred { which_logic = HOL }
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- | make sublogic consistent w.r.t. illegal combinations
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedersublogicUp :: Sublogic -> Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedersublogicUp s =
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder if which_logic s /= HOL && has_sub s then s { has_pred = True } else s
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- | generate a list of all sublogics for HasCASL
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersublogics_all :: [Sublogic]
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersublogics_all = let bools = [False, True] in
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder { has_sub = sub
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , has_part = part
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , has_eq = eq
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , has_pred = pre
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , type_classes = tyCl
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , has_polymorphism = poly
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , has_type_constructors = tyCon
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , which_logic = logic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder | (tyCl, poly) <- [(NoClasses, False), (NoClasses, True),
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder (SimpleTypeClasses, True), (ConstructorClasses, True)]
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , tyCon <- bools
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , sub <- bools
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , part <- bools
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , eq <- bools
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , pre <- bools
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , logic <- [Atomic, Horn, GHorn, FOL, HOL]
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , pre || logic /= HOL && not sub
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- | conversion functions to String
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederformulas_name :: Bool -> Formulas -> String
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederformulas_name hasPred f = case f of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder FOL -> if hasPred then "FOL" else "FOAlg"
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder _ -> case f of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Atomic -> if hasPred then "Atom" else "Eq"
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder _ -> (case f of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder GHorn -> ("G" ++)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder _ -> id) $ if hasPred then "Horn" else "Cond"
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- | the sublogic name as a singleton string list
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersublogic_name :: Sublogic -> [String]
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersublogic_name x = [
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder (if has_sub x then "Sub" else "")
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder ++ (if has_part x then "P" else "")
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder ++ (case type_classes x of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder NoClasses -> if has_polymorphism x then "Poly" else ""
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder SimpleTypeClasses -> "TyCl"
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder ConstructorClasses -> "CoCl")
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder ++ (if has_type_constructors x then "TyCons" else "")
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder ++ formulas_name (has_pred x) (which_logic x)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder ++ (if has_eq x then "=" else "")]
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- * join functions
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersublogic_join :: (Bool -> Bool -> Bool)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -> (Classes -> Classes -> Classes)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -> (Formulas -> Formulas -> Formulas)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -> Sublogic -> Sublogic -> Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersublogic_join joinB joinC joinF a b = Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder { has_sub = joinB (has_sub a) $ has_sub b
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , has_part = joinB (has_part a) $ has_part b
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , has_eq = joinB (has_eq a) $ has_eq b
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , has_pred = joinB (has_pred a) $ has_pred b
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , type_classes = joinC (type_classes a) $ type_classes b
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , has_polymorphism = joinB (has_polymorphism a) $ has_polymorphism b
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , has_type_constructors =
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder joinB (has_type_constructors a) $ has_type_constructors b
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , which_logic = joinF (which_logic a) $ which_logic b
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersublogic_max :: Sublogic -> Sublogic -> Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersublogic_max = sublogic_join max max max
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersublogic_min :: Sublogic -> Sublogic -> Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersublogic_min = sublogic_join min min min
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- | compute union sublogic from a list of sublogics
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedercomp_list :: [Sublogic] -> Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedercomp_list l = foldl sublogic_max bottom l
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder------------------------------------------------------------------------------
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- Functions to analyse formulae
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder------------------------------------------------------------------------------
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder{- ---------------------------------------------------------------------------
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder These functions are based on Till Mossakowski's paper "Sublanguages of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder CASL", which is CoFI Note L-7. The functions implement an adaption of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder the reduced grammar given there for formulae in a specific expression
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder logic by, checking whether a formula would match the productions from the
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder grammar. Which function checks for which nonterminal from the paper is
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder given as a comment before each function.
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder They are adapted for HasCASL, especially HasCASLs abstract syntax (As.hs)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder--------------------------------------------------------------------------- -}
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- Atomic Logic (subsection 3.4 of the paper)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederisPredication :: Term -> Bool
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederisPredication = foldTerm FoldRec
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder { foldQualVar = \ _ _ -> True
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , foldQualOp = \ _ b (InstOpId i _ _) t _ ->
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder b /= Fun && not (elem (i, t) bList)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , foldApplTerm = \ _ b1 b2 _ -> b1 && b2
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , foldTupleTerm = \ _ bs _ -> and bs
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , foldTypedTerm = \ _ b q _ _ -> q /= InType && b
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , foldAsPattern = \ _ _ _ _ -> False
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , foldQuantifiedTerm = \ _ _ _ _ _ -> False
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , foldLambdaTerm = \ _ _ _ _ _ -> False
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , foldCaseTerm = \ _ _ _ _ -> False
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , foldLetTerm = \ _ _ _ _ _ -> False
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , foldResolvedMixTerm = \ _ i bs _ ->
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder not (elem i $ map fst bList) && and bs
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , foldTermToken = \ _ _ -> True
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , foldMixTypeTerm = \ _ q _ _ -> q /= InType
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , foldMixfixTerm = \ _ bs -> and bs
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , foldBracketTerm = \ _ _ bs _ -> and bs
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , foldProgEq = \ _ _ _ _ -> False
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- FORMULA, P-ATOM
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederis_atomic_t :: Term -> Bool
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederis_atomic_t term = case term of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder QuantifiedTerm q _ t _ | is_atomic_q q && is_atomic_t t -> True
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- P-Conjunction and ExEq
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder ApplTerm (QualOp Fun (InstOpId i _ _) t _) arg _
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder | (case arg of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder TupleTerm ts@[_, _] _ ->
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder i == andId && t == logType && and (map is_atomic_t ts)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder || i == exEq && t == eqType
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder _ -> False) || i == defId && t == defType
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder QualOp Fun (InstOpId i _ _) t _
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder | i == trueId && t == unitTypeScheme -> True
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder _ -> isPredication term
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederis_atomic_q :: Quantifier -> Bool
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederis_atomic_q q = case q of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Universal -> True
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- Positive Conditional Logic (subsection 3.2 in the paper)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederis_horn_t :: Term -> Bool
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederis_horn_t term = case term of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder QuantifiedTerm q _ f _ -> is_atomic_q q && is_horn_t f
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder ApplTerm (QualOp Fun (InstOpId i _ _) t _) (TupleTerm [t1, t2] _) _
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder | i == implId && t == logType && is_horn_p_conj t1 && is_horn_a t2
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder _ -> is_atomic_t term
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- P-CONJUNCTION
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederis_horn_p_conj :: Term -> Bool
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederis_horn_p_conj term = case term of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder ApplTerm (QualOp Fun (InstOpId i _ _) t _) (TupleTerm ts@[_, _] _) _
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder | i == andId && t == logType && and (map is_horn_a ts)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder _ -> is_atomic_t term
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederis_horn_a :: Term -> Bool
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederis_horn_a term = case term of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder QualOp Fun (InstOpId i _ _) t _
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder | i == trueId && t == unitTypeScheme -> True
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder ApplTerm (QualOp Fun (InstOpId i _ _) t _) arg _
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder | (case arg of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder TupleTerm [_, _] _ -> (i == exEq || i == eqId) && t == eqType
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder _ -> False) || i == defId && t == defType
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder _ -> is_atomic_t term
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederis_horn_p_a :: Term -> Bool
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederis_horn_p_a term = case term of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder QualOp Fun (InstOpId i _ _) t _
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder | i == trueId && t == unitTypeScheme -> True
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder ApplTerm (QualOp Fun (InstOpId i _ _) t _) arg _
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder | (case arg of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder TupleTerm [_, _] _ -> i == exEq && t == eqType
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder _ -> False) || i == defId && t == defType
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder _ -> is_atomic_t term
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- Generalized Positive Conditional Logic (subsection 3.3 of the paper)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- FORMULA, ATOM
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederis_ghorn_t :: Term -> Bool
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederis_ghorn_t term = case term of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder QuantifiedTerm q _ t _ -> is_atomic_q q && is_ghorn_t t
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder ApplTerm (QualOp Fun (InstOpId i _ _) t _) arg _
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder | (case arg of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder TupleTerm f@[f1, f2] _ ->
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder t == logType &&
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder (i == andId && (is_ghorn_c_conj f || is_ghorn_f_conj f)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder || i == implId && is_ghorn_prem f1 && is_ghorn_conc f2
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder || i == eqvId && is_ghorn_prem f1 && is_ghorn_prem f2)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder || t == eqType && (i == exEq || i == eqId)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder _ -> False) || t == defType && i == defId
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder _ -> is_atomic_t term
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- C-CONJUNCTION
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederis_ghorn_c_conj :: [Term] -> Bool
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederis_ghorn_c_conj = and . map is_ghorn_conc
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- F-CONJUNCTION
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederis_ghorn_f_conj :: [Term] -> Bool
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederis_ghorn_f_conj = and . map is_ghorn_t
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- P-CONJUNCTION
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederis_ghorn_p_conj :: [Term] -> Bool
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederis_ghorn_p_conj = and . map is_ghorn_prem
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederis_ghorn_prem :: Term -> Bool
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederis_ghorn_prem term = case term of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder ApplTerm (QualOp Fun (InstOpId i _ _) t _) (TupleTerm ts@[_, _] _) _ ->
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder i == andId && t == logType && is_ghorn_p_conj ts
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder _ -> is_horn_p_a term
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederis_ghorn_conc :: Term -> Bool
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederis_ghorn_conc term = case term of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder ApplTerm (QualOp Fun (InstOpId i _ _) t _) (TupleTerm ts@[_,_] _) _ ->
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder i == andId && t == logType && is_ghorn_c_conj ts
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder _ -> is_horn_a term
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederis_fol_t :: Term -> Bool
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederis_fol_t t = case t of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder LambdaTerm _ _ _ _ -> False
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder CaseTerm _ _ _ -> False
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder LetTerm _ _ _ _ -> False
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder no higher types (i.e. all types are basic, tuples, or tuple -> basic)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- | compute logic of a formula by checking all logics in turn
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederget_logic :: Term -> Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederget_logic t = if is_atomic_t t then bottom else
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder if is_horn_t t then need_horn else
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder if is_ghorn_t t then need_ghorn else
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder if is_fol_t t then need_fol else need_hol
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder------------------------------------------------------------------------------
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- Functions to compute minimal sublogic for a given element; these work
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- by recursing into all subelements
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder------------------------------------------------------------------------------
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_basicSpec :: BasicSpec -> Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_basicSpec (BasicSpec l) =
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder sublogicUp $ comp_list $ map (sl_basicItem . item) l
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_basicItem :: BasicItem -> Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_basicItem bIt = case bIt of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder SigItems l -> sl_sigItems l
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder ProgItems l _ -> comp_list $ map (sl_progEq . item) l
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder ClassItems _ l _ -> comp_list $ map (sl_classItem . item) l
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder GenVarItems l _ -> comp_list $ map sl_genVarDecl l
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder FreeDatatype l _ -> comp_list $ map (sl_datatypeDecl . item) l
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder GenItems l _ -> comp_list $ map (sl_sigItems . item) l
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder AxiomItems l m _ ->
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder comp_list $ map sl_genVarDecl l ++ map (sl_term . item) m
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Internal l _ -> comp_list $ map (sl_basicItem . item) l
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_sigItems :: SigItems -> Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_sigItems sIt = case sIt of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder TypeItems i l _ ->
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder comp_list $ sl_instance i : map (sl_typeItem . item) l
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder OpItems b l _ ->
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder comp_list $ sl_opBrand b : map (sl_opItem . item) l
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_opBrand :: OpBrand -> Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_opBrand o = case o of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Pred -> need_pred
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_instance :: Instance -> Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_instance i = case i of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Instance -> simpleTypeClasses
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_classItem :: ClassItem -> Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_classItem (ClassItem c l _) =
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder comp_list $ sl_classDecl c : map (sl_basicItem . item) l
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_classDecl :: ClassDecl -> Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_classDecl (ClassDecl _ k _) = case k of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder ClassKind _ -> simpleTypeClasses
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder FunKind _ _ _ _ -> constructorClasses
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- don't check the variance or kind of builtin type constructors
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_Variance :: Variance -> Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_Variance v = case v of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder InVar -> bottom
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder _ -> need_sub
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_AnyKind :: (a -> Sublogic) -> AnyKind a -> Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_AnyKind f k = case k of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder ClassKind i -> f i
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder FunKind v k1 k2 _ ->
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder comp_list [sl_Variance v, sl_AnyKind f k1, sl_AnyKind f k2]
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_Rawkind :: RawKind -> Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_Rawkind = sl_AnyKind (const bottom)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_kind :: Kind -> Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_kind = sl_AnyKind $
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder \ i -> if i == universeId then bottom else simpleTypeClasses
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_typeItem :: TypeItem -> Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_typeItem tyIt = case tyIt of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder TypeDecl l k _ -> comp_list $ sl_kind k : map sl_typePattern l
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder SubtypeDecl l _ _ -> comp_list $ need_sub : map sl_typePattern l
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder IsoDecl l _ -> comp_list $ need_sub : map sl_typePattern l
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder SubtypeDefn tp _ t term _ -> comp_list
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , sl_typePattern tp
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , sl_term $ item term ]
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder AliasType tp (Just k) ts _ -> comp_list
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , sl_typePattern tp
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , sl_typeScheme ts ]
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder AliasType tp Nothing ts _ ->
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder sublogic_max (sl_typePattern tp) $ sl_typeScheme ts
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Datatype dDecl -> sl_datatypeDecl dDecl
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_typePattern :: TypePattern -> Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_typePattern tp = case tp of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder TypePattern _ l _ -> comp_list $ map sl_typeArg l
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- non-empty args --> type constructor!
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder MixfixTypePattern l -> comp_list $ map sl_typePattern l
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder BracketTypePattern _ l _ -> comp_list $ map sl_typePattern l
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder TypePatternArg _ _ -> need_polymorphism
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_type :: Type -> Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_type = sl_BasicFun
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_Basictype :: Type -> Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_Basictype ty = case ty of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder TypeName _ k v -> sublogic_max
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder (if v /= 0 then need_polymorphism else bottom) $ sl_Rawkind k
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder KindedType t k _ -> sublogic_max (sl_Basictype t) $ sl_kind k
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder ExpandedType _ t -> sl_Basictype t
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder TypeAbs v t _ -> comp_list
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder [ need_type_constructors
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , sl_typeArg v
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , sl_Basictype t ]
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder BracketType Parens [t] _ -> sl_Basictype t
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder _ -> case getTypeAppl ty of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder (TypeName ide _ _, args) -> comp_list $
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder (if isArrow ide || ide == lazyTypeId then need_hol else
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder need_type_constructors) : map sl_Basictype args
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder (_, []) -> error "sl_Basictype"
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder (t, args) -> comp_list $ sl_Basictype t : map sl_Basictype args
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_BasicProd :: Type -> Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_BasicProd ty = case getTypeAppl ty of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder (TypeName ide _ _, tyArgs@(_:_:_)) | ide == productId (length tyArgs)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -> comp_list $ map sl_Basictype tyArgs
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder _ -> sl_Basictype ty
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_BasicFun :: Type -> Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_BasicFun ty = case getTypeAppl ty of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder (TypeName ide _ _, [arg, res]) | isArrow ide -> comp_list
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder [ if isPartialArrow ide then need_part else bottom
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , sl_BasicProd arg
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , sl_Basictype res ]
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder _ -> sl_Basictype ty
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- FOL, no higher types, all types are basic, tuples, or tuple -> basic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_typeScheme :: TypeScheme -> Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_typeScheme (TypeScheme l t _) = comp_list $ sl_type t : map sl_typeArg l
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_opItem :: OpItem -> Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_opItem o = case o of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder OpDecl l t m _ -> comp_list $
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder sl_typeScheme t : map sl_opId l ++ map sl_opAttr m
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder OpDefn i v ts p t _ -> comp_list $
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , sl_typeScheme ts
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , sl_partiality p
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder ] ++ map sl_varDecl (concat v)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_partiality :: Partiality -> Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_partiality p = case p of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Partial -> need_part
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Total -> bottom
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_opAttr :: OpAttr -> Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_opAttr a = case a of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder UnitOpAttr t _ -> sl_term t
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_datatypeDecl :: DatatypeDecl -> Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_datatypeDecl (DatatypeDecl t k l c _) = comp_list $
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder [ if null c then bottom else simpleTypeClasses
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , sl_typePattern t
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , sl_kind k ] ++ map (sl_alternative . item) l
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_alternative :: Alternative -> Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_alternative a = case a of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Constructor _ l p _ ->
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder comp_list $ sl_partiality p : map sl_component (concat l)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Subtype l _ -> comp_list $ need_sub : map sl_type l
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_component :: Component -> Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_component s = case s of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Selector _ p t _ _ -> sublogic_max (sl_partiality p) $ sl_type t
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder NoSelector t -> sl_type t
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_term :: Term -> Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_term t = sublogic_max (get_logic t) $ sl_t t
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_t :: Term -> Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_t trm = case trm of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder QualVar vd -> sl_varDecl vd
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder QualOp b i t _ -> comp_list
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder [ sl_opBrand b
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , sl_instOpId i
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , sl_typeScheme t ]
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder ApplTerm t1 t2 _ -> sublogic_max (sl_t t1) $ sl_t t2
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder TupleTerm l _ -> comp_list $ map sl_t l
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder TypedTerm t _ ty _ -> sublogic_max (sl_t t) $ sl_type ty
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder QuantifiedTerm _ l t _ -> comp_list $ sl_t t : map sl_genVarDecl l
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder LambdaTerm l p t _ ->
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder comp_list $ sl_partiality p : sl_t t : map sl_pattern l
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder CaseTerm t l _ -> comp_list $ sl_t t : map sl_progEq l ++ map sl_progEq l
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder LetTerm _ l t _ -> comp_list $ sl_t t : map sl_progEq l
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder MixTypeTerm _ t _ -> sl_type t
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder MixfixTerm l -> comp_list $ map sl_t l
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder BracketTerm _ l _ -> comp_list $ map sl_t l
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder AsPattern vd p2 _ -> sublogic_max (sl_varDecl vd) $ sl_pattern p2
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_pattern :: Pattern -> Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_pattern = sl_t
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_progEq :: ProgEq -> Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_progEq (ProgEq p t _) = sublogic_max (sl_pattern p) (sl_t t)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_varDecl :: VarDecl -> Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_varDecl (VarDecl _ t _ _) = sl_type t
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_varKind :: VarKind -> Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_varKind vk = case vk of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder VarKind k -> sl_kind k
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Downset t -> sublogic_max need_sub $ sl_type t
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_typeArg :: TypeArg -> Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_typeArg (TypeArg _ _ k _ _ _ _) =
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder sublogic_max need_polymorphism (sl_varKind k)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_genVarDecl :: GenVarDecl -> Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_genVarDecl g = case g of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder GenVarDecl v -> sl_varDecl v
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder GenTypeVarDecl v -> sl_typeArg v
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_opId :: OpId -> Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_opId (OpId _ l _) = comp_list $ map sl_typeArg l
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_instOpId :: InstOpId -> Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_instOpId (InstOpId i l _) = comp_list $
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder (if i == exEq || i == eqId then need_eq else bottom) : map sl_type l
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_symbItems :: SymbItems -> Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_symbItems (SymbItems k l _ _) = comp_list $ sl_symbKind k : map sl_symb l
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_symbMapItems :: SymbMapItems -> Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_symbMapItems (SymbMapItems k l _ _) =
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder comp_list $ sl_symbKind k : map sl_symbOrMap l
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_symbKind :: SymbKind -> Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_symbKind k = case k of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder SK_pred -> need_pred
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder SK_class -> simpleTypeClasses
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_symb :: Symb -> Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_symb s = case s of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Symb _ Nothing _ -> bottom
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Symb _ (Just l) _ -> sl_symbType l
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_symbType :: SymbType -> Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_symbType (SymbType t) = sl_typeScheme t
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_symbOrMap :: SymbOrMap -> Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_symbOrMap m = case m of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder SymbOrMap s Nothing _ -> sl_symb s
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder SymbOrMap s (Just t) _ -> sublogic_max (sl_symb s) $ sl_symb t
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder{- the maps have no influence since all sorts,ops,preds in them
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder must also appear in the signatures, so any features needed by
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder them will be included by just checking the signatures -}
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_env :: Env -> Sublogic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedersl_env e = sublogicUp $ comp_list $
(if Map.null $ classMap e then bottom else simpleTypeClasses)
: map sl_typeInfo (Map.elems $ typeMap e)
++ map sl_opInfos (Map.elems $ assumps e)
sublogic_max (if Set.null $ superTypes t then bottom else need_sub)