bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder{- |

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian MaederModule : $Header$

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederCopyright : (c) Pascal Schmidt, Christiantian Maeder, and Uni Bremen 2002-2003

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt

b4fbc96e05117839ca409f5f20f97b3ac872d1edTill Mossakowski

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederMaintainer : hets@tzi.de

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederStability : experimental

f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederPortability : portable

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder This module provides the sublogic functions (as required by Logic.hs) for

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder HasCASL. The functions allow to compute the minimal sublogics needed by a

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder given element, to check whether an item is part of a given sublogic, and --

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder not yet -- to project an element into a given sublogic.

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder-}

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maedermodule HasCASL.Sublogic ( -- * datatypes

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder HasCASL_Sublogics(..),

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder HasCASL_Formulas(..),

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder -- * functions for LatticeWithTop instance

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder top,

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder sublogics_max,

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder sublogics_min,

33a5d53a412ba0a4e5847f7538d6da2e22bd116cChristian Maeder

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder -- * functions for Logic instance

e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maeder

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder -- * sublogic to string converstion

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder sublogics_name,

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder -- * list of all sublogics

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder sublogics_all,

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder -- * checks if element is in given sublogic

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder in_basicSpec,

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder in_sentence,

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder in_symbItems,

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder in_symbMapItems,

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder in_env,

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder in_morphism,

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder in_symbol,

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder -- * computes the sublogic of a given element

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder sl_basicSpec,

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder sl_sentence,

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder sl_symbItems,

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder sl_symbMapItems,

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder sl_env,

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder sl_morphism,

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder sl_symbol,

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder ) where

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maederimport Data.Maybe

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maederimport qualified Common.Lib.Map as Map

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maederimport Common.AS_Annotation

b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maederimport HasCASL.As

ebcaad207cafc89eeb49d431f40de2ef4c48411cChristian Maederimport HasCASL.Le

b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maederimport HasCASL.Morphism

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederimport HasCASL.Builtin

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder

b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder------------------------------------------------------------------------------

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder-- | Datatypes for HasCASL sublogics

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder------------------------------------------------------------------------------

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederdata HasCASL_Formulas = Atomic -- atomic logic

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder | Horn -- positive conditional logic

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder | GHorn -- generalized positive conditional logic

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder | FOL -- first-order logic

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder | HOL -- higher-order logic

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder deriving (Show,Ord,Eq)

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederdata HasCASL_Sublogics = HasCASL_SL

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder { has_sub :: Bool, -- subsorting

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder has_part :: Bool, -- partiality

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder has_eq :: Bool, -- equality

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder has_pred :: Bool, -- predicates

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder has_ho :: Bool, -- higher order

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder has_type_classes :: Bool,

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder has_polymorphism :: Bool,

dfa74d066ea0f00a70276aedecc624c6b3c86deaChristian Maeder has_type_constructors :: Bool,

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder which_logic::HasCASL_Formulas

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder } deriving (Show,Ord,Eq)

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder-----------------------------------------------------------------------------

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder-- Special sublogics elements

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder-----------------------------------------------------------------------------

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder-- top element

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder--

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maedertop :: HasCASL_Sublogics

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maedertop = (HasCASL_SL True True True True True True True True HOL)

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder-- bottom element

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder--

3c62e6ef442caf092adcbecf6fccd957dcd72689Christian Maederbottom :: HasCASL_Sublogics

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederbottom = (HasCASL_SL False False False False False False False False Atomic)

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder-- the following are used to add a needed feature to a given

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder-- sublogic via sublogics_max, i.e. (sublogics_max given needs_part)

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder-- will force partiality in addition to what features given already

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder-- has included

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder-- minimal sublogic with subsorting

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder--

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederneed_sub :: HasCASL_Sublogics

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maederneed_sub = bottom { has_sub = True }

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- minimal sublogic with partiality

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder--

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederneed_part :: HasCASL_Sublogics

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederneed_part = bottom { has_part = True }

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder

836e72a3c413366ba9801726f3b249c7791cb9caChristian Maeder-- minimal sublogic with equality

836e72a3c413366ba9801726f3b249c7791cb9caChristian Maeder--

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederneed_eq :: HasCASL_Sublogics

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederneed_eq = bottom { has_eq = True }

149e43c4a2705a86a0e5fa301ba849fdf19db32eChristian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- minimal sublogic with predicates

149e43c4a2705a86a0e5fa301ba849fdf19db32eChristian Maeder--

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederneed_pred :: HasCASL_Sublogics

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederneed_pred = bottom { has_pred = True }

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder-- minimal sublogic with higher order

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder--

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederneed_ho :: HasCASL_Sublogics

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederneed_ho = bottom { has_ho = True }

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder-- minimal sublogic with type classes

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder--

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederneed_type_classes :: HasCASL_Sublogics

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederneed_type_classes = bottom { has_type_classes = True }

797f811e57952d59e73b8cd03b667eef276db972Christian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- minimal sublogic with polymorhism

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder--

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederneed_polymorphism :: HasCASL_Sublogics

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederneed_polymorphism = bottom { has_polymorphism = True }

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- minimal sublogic with type constructors

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder--

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederneed_type_constructors :: HasCASL_Sublogics

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederneed_type_constructors = bottom { has_type_constructors = True }

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maederneed_horn :: HasCASL_Sublogics

149e43c4a2705a86a0e5fa301ba849fdf19db32eChristian Maederneed_horn = bottom { which_logic = Horn }

149e43c4a2705a86a0e5fa301ba849fdf19db32eChristian Maeder

1738d16957389457347bee85075d3d33d002158fChristian Maederneed_ghorn :: HasCASL_Sublogics

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederneed_ghorn = bottom { which_logic = GHorn }

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder

33a5d53a412ba0a4e5847f7538d6da2e22bd116cChristian Maederneed_fol :: HasCASL_Sublogics

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederneed_fol = bottom { which_logic = FOL }

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederneed_hol :: HasCASL_Sublogics

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederneed_hol = bottom { which_logic = HOL }

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder

b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder-----------------------------------------------------------------------------

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder-- Functions to generate a list of all sublogics for HasCASL

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder-----------------------------------------------------------------------------

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maedersublogics_all :: [HasCASL_Sublogics]

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maedersublogics_all = [HasCASL_SL {has_sub = sub,

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder has_part = part,

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder has_eq = eq,

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder has_pred = pre,

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder has_ho = ho,

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder has_type_classes = tyCl,

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder has_polymorphism = poly,

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder has_type_constructors = tyCon,

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder which_logic = logic}

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder | sub <- [False,True],

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder part <- [False,True],

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder eq <- [False,True],

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder pre <- [False,True],

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder ho <- [False,True],

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder tyCl <- [False,True],

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder poly <- [False,True],

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder tyCon <- [False,True],

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder logic <- [Atomic, Horn, GHorn, FOL, HOL] ]

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder------------------------------------------------------------------------------

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder-- Conversion functions (to String)

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder------------------------------------------------------------------------------

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder-- "formulas_name :: has_pred -> has_ho -> which_logic -> String"

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederformulas_name :: Bool -> Bool -> HasCASL_Formulas -> String

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maederformulas_name True True HOL = "HOL"

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maederformulas_name True False HOL = "HOL" -- ?!

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maederformulas_name False True HOL = "HOL"

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maederformulas_name False False HOL = "HOL" -- ?!

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maederformulas_name True True FOL = "HOL" -- ?!

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maederformulas_name True False FOL = "FOL"

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederformulas_name False True FOL = "HO-FOAlg" -- ?!

formulas_name False False FOL = "FOAlg"

formulas_name True True GHorn = "HO-GHorn"

formulas_name True False GHorn = "GHorn"

formulas_name False True GHorn = "HO-GCond"

formulas_name False False GHorn = "GCond"

formulas_name True True Horn = "HO-Horn"

formulas_name True False Horn = "Horn"

formulas_name False True Horn = "HO-Cond"

formulas_name False False Horn = "Cond"

formulas_name True True Atomic = "HO-Atom"

formulas_name True False Atomic = "Atom"

formulas_name False True Atomic = "HO-Eq"

formulas_name False False Atomic = "Eq"

sublogics_name :: HasCASL_Sublogics -> [String]

sublogics_name x = [

( if (has_sub x) then "Sub" else "")

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

++ ( if (has_type_classes x) then "TyCl" else "")

++ ( if (has_polymorphism x) then "Poly" else "")

++ ( if (has_type_constructors x) then "TyCons" else "")

++ ( formulas_name (has_pred x) (has_ho x) (which_logic x) )

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

------------------------------------------------------------------------------

-- min/join and max/meet functions

------------------------------------------------------------------------------

formulas_max :: HasCASL_Formulas -> HasCASL_Formulas -> HasCASL_Formulas

formulas_max x y = if (x<y) then y else x

formulas_min :: HasCASL_Formulas -> HasCASL_Formulas -> HasCASL_Formulas

formulas_min x y = if (x<y) then x else y

sublogics_max :: HasCASL_Sublogics -> HasCASL_Sublogics -> HasCASL_Sublogics

sublogics_max a b = HasCASL_SL

(has_sub a || has_sub b)

(has_part a || has_part b)

(has_eq a || has_eq b)

(has_pred a || has_pred b)

(has_ho a || has_ho b)

(has_type_classes a || has_type_classes b)

(has_polymorphism a || has_polymorphism b)

(has_type_constructors a || has_type_constructors b)

(formulas_max (which_logic a) (which_logic b))

sublogics_min :: HasCASL_Sublogics -> HasCASL_Sublogics -> HasCASL_Sublogics

sublogics_min a b = HasCASL_SL

(has_sub a && has_sub b)

(has_part a && has_part b)

(has_eq a && has_eq b)

(has_pred a && has_pred b)

(has_ho a && has_ho b)

(has_type_classes a && has_type_classes b)

(has_polymorphism a && has_polymorphism b)

(has_type_constructors a && has_type_constructors b)

(formulas_min (which_logic a) (which_logic b))

------------------------------------------------------------------------------

-- Helper functions

------------------------------------------------------------------------------

-- compute sublogics from a list of sublogics

--

comp_list :: [HasCASL_Sublogics] -> HasCASL_Sublogics

comp_list l = foldl sublogics_max bottom l

------------------------------------------------------------------------------

-- Functions to analyse formulae

------------------------------------------------------------------------------

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

These functions are based on Till Mossakowski's paper "Sublanguages of

CASL", which is CoFI Note L-7. The functions implement an adaption of

the reduced grammar given there for formulae in a specific expression

logic by, checking whether a formula would match the productions from the

grammar. Which function checks for which nonterminal from the paper is

given as a comment before each function.

They are adapted for HasCASL, especially HasCASLs abstract syntax (As.hs)

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

-- Atomic Logic (subsection 3.4 of the paper)

-- FORMULA, P-ATOM

--

is_atomic_t :: Term -> Bool

is_atomic_t (QuantifiedTerm q _ t _) = (is_atomic_q q) && (is_atomic_t t)

is_atomic_t (ApplTerm (QualOp Fun (InstOpId i _ _) t _) (TupleTerm ts _) _) =

-- P-Conjunction and ExEq

(((i == andId)

&& (and $ map is_atomic_t ts))

|| (i == exEq))

&& (t == logType)

&& (not (null ts))

is_atomic_t (QualOp Fun (InstOpId i _ _) t _) =

(i == trueId)

&& (t == logType)

--is_atomic_t (Predication _ _ _) = True

is_atomic_t (ApplTerm (QualOp Fun (InstOpId i _ _) t _) _ _) =

(i == defId)

&& (t == logType)

is_atomic_t _ = False

-- QUANTIFIER

--

is_atomic_q :: Quantifier -> Bool

is_atomic_q (Universal) = True

is_atomic_q _ = False

-- Positive Conditional Logic (subsection 3.2 in the paper)

-- FORMULA

--

is_horn_t :: Term -> Bool

is_horn_t (QuantifiedTerm q _ f _) =

(is_atomic_q q)

&& (is_horn_t f)

is_horn_t (ApplTerm (QualOp Fun (InstOpId i _ _) t _) (TupleTerm f _) _) =

(i == implId)

&& (t == logType)

&& (is_horn_p_conj (head f))

&& (is_horn_a (last f))

is_horn_t _ = False

-- P-CONJUNCTION

--

is_horn_p_conj :: Term -> Bool

is_horn_p_conj (ApplTerm (QualOp Fun (InstOpId i _ _) t _) (TupleTerm ts _) _) =

(i == andId)

&& (t == logType)

&& (not (null ts))

&& (and $ map is_horn_a ts)

is_horn_p_conj _ = False

-- ATOM

--

is_horn_a :: Term -> Bool

is_horn_a (QualOp Fun (InstOpId i _ _) t _) =

(i == trueId)

&& (t == logType)

-- is_horn_a (Predication _ _ _) = True

is_horn_a (ApplTerm (QualOp Fun (InstOpId i _ _) t _) _ _) =

((i == defId)

|| (i == exEq)

|| (i == eqId))

&& (t == logType)

--is_horn_a (Membership _ _ _) = True

is_horn_a _ = False

-- P-ATOM

--

is_horn_p_a :: Term -> Bool

is_horn_p_a (QualOp Fun (InstOpId i _ _) t _) =

(i == trueId)

&& (t == logType)

-- is_horn_p_a (Predication _ _ _) = True

is_horn_p_a (ApplTerm (QualOp Fun (InstOpId i _ _) t _) _ _) =

((i == defId)

|| (i == exEq))

&& (t == logType)

-- is_horn_p_a (Membership _ _ _) = True

is_horn_p_a _ = False

-- Generalized Positive Conditional Logic (subsection 3.3 of the paper)

-- FORMULA, ATOM

--

is_ghorn_t :: Term -> Bool

is_ghorn_t (QuantifiedTerm q _ t _) = (is_atomic_q q) && (is_ghorn_t t)

is_ghorn_t (ApplTerm (QualOp Fun (InstOpId i _ _) t _) (TupleTerm f _) _) =

(t == logType)

&& (((i == andId) && (not (null f)) && ((is_ghorn_c_conj f) || (is_ghorn_f_conj f)))

||

((i == implId) && (is_ghorn_prem (head f)) && (is_ghorn_conc (last f)))

||

((i == eqvId) && (is_ghorn_prem (head f)) && (is_ghorn_prem (last f))))

is_ghorn_t (QualOp Fun (InstOpId i _ _) t _) =

(i == trueId)

&& (t == logType)

-- is_ghorn_t (Predication _ _ _) = True

is_ghorn_t (ApplTerm (QualOp Fun (InstOpId i _ _) t _) _ _) =

((i == defId)

|| (i == exEq)

|| (i == eqId))

&& (t == logType)

-- is_ghorn_t (Membership _ _ _) = True

is_ghorn_t _ = False

-- C-CONJUNCTION

--

is_ghorn_c_conj :: [Term] -> Bool

is_ghorn_c_conj t = (not(null t)) && (and ((map is_ghorn_conc) t))

-- F-CONJUNCTION

--

is_ghorn_f_conj :: [Term] -> Bool

is_ghorn_f_conj t = (not(null t)) && (and ((map is_ghorn_t) t))

-- P-CONJUNCTION

--

is_ghorn_p_conj :: [Term] -> Bool

is_ghorn_p_conj t = (not(null t)) && (and (map is_ghorn_prem t))

-- PREMISE

--

is_ghorn_prem :: Term -> Bool

is_ghorn_prem (ApplTerm (QualOp Fun (InstOpId i _ _) t _) (TupleTerm ts _) _) =

(i == andId)

&& (t == logType)

&& (not (null ts))

&& (is_ghorn_p_conj ts)

is_ghorn_prem x = is_horn_p_a x

-- CONCLUSION

--

is_ghorn_conc :: Term -> Bool

is_ghorn_conc (ApplTerm (QualOp Fun (InstOpId i _ _) t _) (TupleTerm ts _) _) =

(i == andId)

&& (t == logType)

&& (not (null ts))

&& (is_ghorn_c_conj ts)

is_ghorn_conc x = is_horn_a x

is_fol_t :: Term -> Bool

is_fol_t _ = False

{- FOL:

no lambda/let/case,

no higher types (i.e. all types are basic, tuples, or tuple -> basic)

-}

-- compute logic of a formula by checking all logics in turn

--

get_logic :: Term -> HasCASL_Sublogics

get_logic t = if (is_atomic_t t) then bottom else

if (is_horn_t t) then need_horn else

if (is_ghorn_t t) then need_ghorn else

if (is_fol_t t) then need_fol else

need_hol

------------------------------------------------------------------------------

-- Functions to compute minimal sublogic for a given element; these work

-- by recursing into all subelements

------------------------------------------------------------------------------

sl_basicSpec :: BasicSpec -> HasCASL_Sublogics

sl_basicSpec (BasicSpec l) = comp_list $ map sl_basicItem

$ map item l

sl_basicItem :: BasicItem -> HasCASL_Sublogics

sl_basicItem (SigItems l) = sl_sigItems l

sl_basicItem (ProgItems l _) = comp_list $ map sl_progEq

$ map item l

sl_basicItem (ClassItems _ l _) = sublogics_max need_type_classes

(comp_list $ map sl_classItem

$ map item l)

sl_basicItem (GenVarItems l _) = comp_list $ map sl_genVarDecl l

sl_basicItem (FreeDatatype l _) = comp_list $ map sl_datatypeDecl

$ map item l

sl_basicItem (GenItems l _) = (comp_list $ map sl_sigItems

$ map item l)

sl_basicItem (AxiomItems l m _) = sublogics_max

(comp_list $ map sl_genVarDecl l)

(comp_list $ map sl_term

$ map item m)

sl_basicItem (Internal l _) = comp_list $ map sl_basicItem

$ map item l

sl_sigItems :: SigItems -> HasCASL_Sublogics

sl_sigItems (TypeItems i l _) = sublogics_max (sl_instance i)

(comp_list $ map sl_typeItem

$ map item l)

sl_sigItems (OpItems b l _) = sublogics_max (sl_opBrand b)

(comp_list $ map sl_opItem

$ map item l)

sl_opBrand :: OpBrand -> HasCASL_Sublogics

sl_opBrand (Pred) = need_pred

sl_opBrand _ = bottom

sl_instance :: Instance -> HasCASL_Sublogics

sl_instance (Instance) = need_type_classes

sl_instance _ = bottom

sl_classItem :: ClassItem -> HasCASL_Sublogics

sl_classItem (ClassItem _ l _) = comp_list $ map sl_basicItem

$ map item l

sl_typeItem :: TypeItem -> HasCASL_Sublogics

sl_typeItem (TypeDecl l _ _) = comp_list $ map sl_typePattern l

sl_typeItem (SubtypeDecl l _ _) = sublogics_max need_sub

(comp_list $ map sl_typePattern l)

sl_typeItem (IsoDecl l _) = sublogics_max need_sub

(comp_list $ map sl_typePattern l)

sl_typeItem (SubtypeDefn tp _ t term _) =

comp_list [need_sub,

(sl_typePattern tp),

(sl_type t),

(sl_term (item term))]

sl_typeItem (AliasType tp _ ts _) = sublogics_max (sl_typePattern tp)

(sl_typeScheme ts)

sl_typeItem (Datatype dDecl) = sl_datatypeDecl dDecl

sl_typePattern :: TypePattern -> HasCASL_Sublogics

sl_typePattern (TypePattern _ l _) = comp_list $ map sl_typeArg l

-- non-empty args --> type constructor!

sl_typePattern (MixfixTypePattern l) = comp_list $ map sl_typePattern l

sl_typePattern (BracketTypePattern _ l _) = comp_list $ map sl_typePattern l

sl_typePattern (TypePatternArg _ _) = need_polymorphism

sl_typePattern _ = bottom

sl_type :: Type -> HasCASL_Sublogics

sl_type (TypeName _ _ v) = if v /= 0 then need_polymorphism else bottom

sl_type (TypeAppl t1 t2) = comp_list [need_type_constructors,

(sl_type t1), (sl_type t2)]

sl_type (BracketType _ l _) = comp_list $ map sl_type l

sl_type (KindedType t _ _) = sl_type t

sl_type (ExpandedType _ t) = sl_type t

sl_type (MixfixType l) = comp_list $ map sl_type l

sl_type (LazyType t _) = sl_type t

sl_type (ProductType l _) = comp_list $ map sl_type l

sl_type (FunType t1 a t2 _) =

comp_list [need_ho, (sl_type t1), (sl_arrow a), (sl_type t2)]

sl_type (TypeToken _) = bottom

{- FOL:

no higher types (i.e. all types are basic, tuples, or tuple -> basic)

-}

sl_arrow :: Arrow -> HasCASL_Sublogics

sl_arrow (PFunArr) = need_part

sl_arrow (PContFunArr) = need_part

sl_arrow _ = bottom

sl_typeScheme :: TypeScheme -> HasCASL_Sublogics

sl_typeScheme (TypeScheme l (p :=> t) _) =

comp_list ((comp_list $ map sl_typeArg l) :

(comp_list $ map sl_pred p) :

case unalias t of

FunType t1 a t2 _ -> [(sl_type t1), (sl_arrow a), (sl_type t2)]

_ -> [sl_type t])

sl_pred :: Pred -> HasCASL_Sublogics

sl_pred (IsIn _ l) = sublogics_max need_type_classes

(comp_list $ map sl_type l)

sl_opItem :: OpItem -> HasCASL_Sublogics

sl_opItem (OpDecl l t m _) =

comp_list [(comp_list $ map sl_opId l),

(sl_typeScheme t),

(comp_list $ map sl_opAttr m)]

sl_opItem (OpDefn i v ts p t _) =

comp_list [(sl_opId i),

(comp_list $ map sl_varDecl (concat v)),

(sl_typeScheme ts),

(sl_partiality p),

(sl_term t)]

sl_partiality :: Partiality -> HasCASL_Sublogics

sl_partiality (Partial) = need_part

sl_partiality _ = bottom

sl_opAttr :: OpAttr -> HasCASL_Sublogics

sl_opAttr (UnitOpAttr t _) = sl_term t

sl_opAttr _ = need_eq

sl_datatypeDecl :: DatatypeDecl -> HasCASL_Sublogics

sl_datatypeDecl (DatatypeDecl t _ l c _) =

if (null c) then sublogics_max (sl_typePattern t)

(comp_list $ map sl_alternative

$ map item l)

else comp_list [need_type_classes,

(sl_typePattern t),

(comp_list $ map sl_alternative $ map item l)]

sl_alternative :: Alternative -> HasCASL_Sublogics

sl_alternative (Constructor _ l p _) =

comp_list [(sl_partiality p),

(comp_list $ map sl_component (concat l))]

sl_alternative (Subtype l _) = sublogics_max need_sub

(comp_list $ map sl_type l)

sl_component :: Component -> HasCASL_Sublogics

sl_component (Selector _ p t _ _) =

sublogics_max (sl_partiality p) (sl_type t)

sl_component (NoSelector t) = sl_type t

sl_term :: Term -> HasCASL_Sublogics

sl_term t = sublogics_max (get_logic t) (sl_t t)

sl_t :: Term -> HasCASL_Sublogics

sl_t (QualVar vd) = sl_varDecl vd

sl_t (QualOp b i t _) =

comp_list [(sl_opBrand b),

(sl_instOpId i),

(sl_typeScheme t)]

--sl_t (ResolvedMixTerm _ l _) = comp_list $ map sl_t l

sl_t (ApplTerm t1 t2 _) = sublogics_max (sl_t t1) (sl_t t2)

sl_t (TupleTerm l _) = comp_list $ map sl_t l

sl_t (TypedTerm t _ ty _) = sublogics_max (sl_t t) (sl_type ty)

sl_t (QuantifiedTerm _ l t _) = sublogics_max (sl_t t)

(comp_list $ map sl_genVarDecl l)

sl_t (LambdaTerm l p t _) =

comp_list [(comp_list $ map sl_pattern l),

(sl_partiality p),

(sl_t t)]

sl_t (CaseTerm t l _) = sublogics_max (sl_t t)

(comp_list $ map sl_progEq l)

sl_t (LetTerm _ l t _) = sublogics_max (sl_t t)

(comp_list $ map sl_progEq l)

sl_t (MixTypeTerm _ t _) = sl_type t

sl_t (MixfixTerm l) = comp_list $ map sl_t l

sl_t (BracketTerm _ l _) = comp_list $ map sl_t l

sl_t (AsPattern vd p2 _) = sublogics_max (sl_varDecl vd) (sl_pattern p2)

sl_t _ = bottom

sl_pattern :: Pattern -> HasCASL_Sublogics

sl_pattern = sl_t

sl_progEq :: ProgEq -> HasCASL_Sublogics

sl_progEq (ProgEq p t _) = sublogics_max (sl_pattern p) (sl_t t)

sl_varDecl :: VarDecl -> HasCASL_Sublogics

sl_varDecl (VarDecl _ t _ _) = sl_type t

sl_typeArg :: TypeArg -> HasCASL_Sublogics

sl_typeArg (TypeArg _ _ _ _) = need_polymorphism

sl_genVarDecl :: GenVarDecl -> HasCASL_Sublogics

sl_genVarDecl (GenVarDecl v) = sl_varDecl v

sl_genVarDecl (GenTypeVarDecl _) = need_polymorphism

sl_opId :: OpId -> HasCASL_Sublogics

sl_opId (OpId _ l _) = comp_list $ map sl_typeArg l

sl_instOpId :: InstOpId -> HasCASL_Sublogics

sl_instOpId (InstOpId i l _) =

if ((i == exEq) || (i == eqId))

then sublogics_max need_eq (comp_list $ map sl_type l)

else comp_list $ map sl_type l

sl_symbItems :: SymbItems -> HasCASL_Sublogics

sl_symbItems (SymbItems k l _ _) = sublogics_max (sl_symbKind k)

(comp_list $ map sl_symb l)

sl_symbMapItems :: SymbMapItems -> HasCASL_Sublogics

sl_symbMapItems (SymbMapItems k l _ _) = sublogics_max (sl_symbKind k)

(comp_list $ map sl_symbOrMap l)

sl_symbKind :: SymbKind -> HasCASL_Sublogics

sl_symbKind (SK_pred) = need_pred

sl_symbKind (SK_class) = need_type_classes

sl_symbKind _ = bottom

sl_symb :: Symb -> HasCASL_Sublogics

sl_symb (Symb _ Nothing _) = bottom

sl_symb (Symb _ (Just l) _) = sl_symbType l

sl_symbType :: SymbType -> HasCASL_Sublogics

sl_symbType (SymbType t) = sl_typeScheme t

sl_symbOrMap :: SymbOrMap -> HasCASL_Sublogics

sl_symbOrMap (SymbOrMap s Nothing _) = sl_symb s

sl_symbOrMap (SymbOrMap s (Just 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_env :: Env -> HasCASL_Sublogics

sl_env e =

let classes = if Map.isEmpty $ classMap e

then bottom else need_type_classes

types = comp_list $ map sl_typeInfo (Map.elems (typeMap e))

ops = comp_list $ map sl_opInfos (Map.elems (assumps e))

in comp_list [classes, types, ops]

sl_typeInfo :: TypeInfo -> HasCASL_Sublogics

sl_typeInfo t = sublogics_max (comp_list $ map sl_type (superTypes t))

(sl_typeDefn (typeDefn t))

sl_typeDefn :: TypeDefn -> HasCASL_Sublogics

sl_typeDefn (Supertype _ ts t) =

sublogics_max (sl_typeScheme ts) (sl_term t)

sl_typeDefn (DatatypeDefn de) = sl_dataEntry de

sl_typeDefn (AliasTypeDefn t) = sl_typeScheme t

sl_typeDefn (TypeVarDefn) = need_polymorphism

sl_typeDefn _ = bottom

sl_dataEntry :: DataEntry -> HasCASL_Sublogics

sl_dataEntry (DataEntry _ _ _ l m) =

sublogics_max (comp_list $ map sl_typeArg l)

(comp_list $ map sl_altDefn m)

sl_opInfos :: OpInfos -> HasCASL_Sublogics

sl_opInfos o = comp_list $ map sl_opInfo (opInfos o)

sl_opInfo :: OpInfo -> HasCASL_Sublogics

sl_opInfo o = comp_list [(sl_typeScheme (opType o)),

(comp_list $ map sl_opAttr (opAttrs o)),

(sl_opDefn (opDefn o))]

sl_opDefn :: OpDefn -> HasCASL_Sublogics

sl_opDefn (NoOpDefn b) = sl_opBrand b

sl_opDefn (SelectData l _) = comp_list $ map sl_constrInfo l

sl_opDefn (Definition b t) =

sublogics_max (sl_opBrand b) (sl_term t)

sl_opDefn _ = bottom

sl_constrInfo :: ConstrInfo -> HasCASL_Sublogics

sl_constrInfo c = sl_typeScheme (constrType c)

sl_sentence :: Sentence -> HasCASL_Sublogics

sl_sentence (Formula t) = sl_term t

sl_sentence (ProgEqSen _ ts pq) =

sublogics_max (sl_typeScheme ts) (sl_progEq pq)

sl_sentence (DatatypeSen l) = comp_list $ map sl_dataEntry l

sl_altDefn :: AltDefn -> HasCASL_Sublogics

sl_altDefn (Construct _ l p m) =

comp_list [(comp_list $ map sl_type l),

(sl_partiality p),

(comp_list $ map sl_selector $ concat m)]

sl_selector :: Selector -> HasCASL_Sublogics

sl_selector (Select _ t p) = sublogics_max (sl_type t)

(sl_partiality p)

sl_morphism :: Morphism -> HasCASL_Sublogics

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

sl_symbol :: Symbol -> HasCASL_Sublogics

sl_symbol (Symbol _ t e) =

sublogics_max (sl_symbolType t) (sl_env e)

sl_symbolType :: SymbolType -> HasCASL_Sublogics

sl_symbolType (OpAsItemType t) = sl_typeScheme t

sl_symbolType (ClassAsItemType _) = need_type_classes

sl_symbolType _ = bottom

------------------------------------------------------------------------------

-- comparison functions

------------------------------------------------------------------------------

-- negated implication

--

nimpl :: Bool -> Bool -> Bool

nimpl True _ = True

nimpl False False = True

nimpl False True = False

-- check if a "new" sublogic is contained in/equal to a given

-- sublogic

--

sl_in :: HasCASL_Sublogics -> HasCASL_Sublogics -> Bool

sl_in given new = (nimpl (has_sub given) (has_sub new)) &&

(nimpl (has_part given) (has_part new)) &&

(nimpl (has_eq given) (has_eq new)) &&

(nimpl (has_pred given) (has_pred new)) &&

(nimpl (has_polymorphism given)

(has_polymorphism new)) &&

(nimpl (has_ho given) (has_ho new)) &&

(nimpl (has_type_classes given)

(has_type_classes new)) &&

(nimpl (has_type_constructors given)

(has_type_constructors new)) &&

((which_logic given) >= (which_logic new))

in_x :: HasCASL_Sublogics -> a -> (a -> HasCASL_Sublogics) -> Bool

in_x l x f = sl_in l (f x)

in_basicSpec :: HasCASL_Sublogics -> BasicSpec -> Bool

in_basicSpec l x = in_x l x sl_basicSpec

in_sentence :: HasCASL_Sublogics -> Sentence -> Bool

in_sentence l x = in_x l x sl_sentence

in_symbItems :: HasCASL_Sublogics -> SymbItems -> Bool

in_symbItems l x = in_x l x sl_symbItems

in_symbMapItems :: HasCASL_Sublogics -> SymbMapItems -> Bool

in_symbMapItems l x = in_x l x sl_symbMapItems

in_env :: HasCASL_Sublogics -> Env -> Bool

in_env l x = in_x l x sl_env

in_morphism :: HasCASL_Sublogics -> Morphism -> Bool

in_morphism l x = in_x l x sl_morphism

in_symbol :: HasCASL_Sublogics -> Symbol -> Bool

in_symbol l x = in_x l x sl_symbol