9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke{-# LANGUAGE MultiParamTypeClasses #-}

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke{- |

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaederModule : $Header$

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkeDescription : Sublogics for THF

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuCopyright : (c) Jonathan von Schroeder, DFKI Bremen 2012

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkeLicense : GPLv2 or higher, see LICENSE.txt

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkeMaintainer : Jonathan von Schroeder <j.von_schroeder@dfki.de>

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkeStability : experimental

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkePortability : non-portable (via Logic.Logic)

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaederSublogics for THF

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke-}

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkemodule THF.Sublogic where

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkeimport THF.As

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkeimport Logic.Logic hiding (join)

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkedata THFCoreSl = THF | THFP | THF0 deriving (Ord,Show,Eq)

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkedata THFSl = THFSl {

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke core :: THFCoreSl,

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder ext_ShortTypes :: Bool } deriving (Ord,Eq)

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder{-

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaederThe ShortTypes extension allows for unnamed unique types:

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder %With ShortTypes

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder thf(a_type,type,a : ($tType,$tType))

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder thf(b_type,type,b : $tType > a)

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder thf(test_const_type,type, test : b)

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder %Without ShortTypes

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder thf(a1_type,type,a1 : $tType)

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke thf(a2_type,type,a2 : $tType)

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke thf(b1_type,type,b1 : $tType)

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke thf(test_const_type,type, test : b1 > (a1,a2))

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkeNote: Types made of other, non-atomic types are not allowed i.e. the following

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkeis still not a legal type-definition:

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke thf(a_type,type, a: $tType > $tType)

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke thf(b_type,type, b: a > $tType)

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkeWithout this extension $tType may only be used to declare

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maederatomic types i.e.

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke thf(a_type,type, a : $tType)

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder-}

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maederinstance Show THFSl where

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke show sl = (show $ core sl) ++

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke (if ext_ShortTypes sl

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke then "_ST" else "")

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaederjoinCoreSl :: THFCoreSl -> THFCoreSl -> THFCoreSl

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkejoinCoreSl THF _ = THF

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaederjoinCoreSl _ THF = THF

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkejoinCoreSl THFP _ = THFP

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkejoinCoreSl _ THFP = THFP

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkejoinCoreSl _ _ = THF0

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maederjoin :: THFSl -> THFSl -> THFSl

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkejoin sl1 sl2 = THFSl {

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke core = joinCoreSl (core sl1) (core sl2),

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke ext_ShortTypes = (ext_ShortTypes sl1) ||

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder (ext_ShortTypes sl2) }

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartketHF0,tHFP,tHF :: THFSl

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartketHF0 = THFSl { core = THF0, ext_ShortTypes = False }

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartketHFP = THFSl { core = THFP, ext_ShortTypes = False }

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartketHF = THFSl { core = THF , ext_ShortTypes = False }

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartketHF0_ST,tHFP_ST,tHF_ST :: THFSl

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartketHF0_ST = tHF0 { ext_ShortTypes = True }

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartketHFP_ST = tHFP { ext_ShortTypes = True }

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartketHF_ST = tHF { ext_ShortTypes = True }

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkesublogics_all :: [THFSl]

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maedersublogics_all = [tHF0, tHF0_ST,

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder tHFP, tHFP_ST,

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke tHF, tHF_ST]

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkeinstance MinSublogic THFSl THFFormula where

a23e572c8f957cc051a1b0831abd6fe9380d45c7Christian Maeder minSublogic f = case f of

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder TF_THF_Logic_Formula f' -> join tHF0 $ minSublogic f'

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder TF_THF_Sequent s -> join tHF $ minSublogic s

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder T0F_THF_Typed_Const tc -> join tHF0 $ minSublogic tc -- fixme: Not in THF?

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maederinstance MinSublogic THFSl THFLogicFormula where

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder minSublogic f = case f of

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke TLF_THF_Binary_Formula b -> join tHF0 $ minSublogic b

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke TLF_THF_Unitary_Formula u -> join tHF0 $ minSublogic u

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke TLF_THF_Type_Formula tf -> join tHF $ minSublogic tf

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke TLF_THF_Sub_Type st -> join tHF $ minSublogic st

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkeinstance MinSublogic THFSl THFSequent where

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke minSublogic _ = tHF

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maederinstance MinSublogic THFSl THFTypedConst where

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder minSublogic c = case c of

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder T0TC_Typed_Const _ tp -> minSublogic tp

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder T0TC_THF_TypedConst_Par tp -> minSublogic tp

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkeinstance MinSublogic THFSl THFBinaryFormula where

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke minSublogic b = case b of

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke TBF_THF_Binary_Pair f1 c f2 -> join tHF0 (join (minSublogic f1)

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke (join (minSublogic c) (minSublogic f2)))

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder TBF_THF_Binary_Tuple bt -> join tHF0 $ minSublogic bt

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke TBF_THF_Binary_Type bt -> join tHF $ minSublogic bt

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkeinstance MinSublogic THFSl THFUnitaryFormula where

minSublogic u = case u of

TUF_THF_Quantified_Formula qf -> join tHF0 $ minSublogic qf

TUF_THF_Unary_Formula uc f -> join tHF0 $ join (minSublogic uc)

(minSublogic f)

TUF_THF_Atom a -> join tHF0 $ minSublogic a

TUF_THF_Tuple uts -> foldr join tHFP (map minSublogic uts)

TUF_THF_Conditional f1 f2 f3 -> join tHF $ join (minSublogic f1)

(join (minSublogic f2) (minSublogic f3))

TUF_THF_Logic_Formula_Par f -> join tHF0 $ minSublogic f

T0UF_THF_Abstraction vs u' -> join (foldr join tHF0

(map minSublogic vs)) $

minSublogic u'

instance MinSublogic THFSl THFTypeFormula where

minSublogic tf = case tf of

TTF_THF_Type_Formula tf' tp -> join tHF $ join (minSublogic tf')

(minSublogic tp)

TTF_THF_Typed_Const _ tp -> join tHF $ minSublogic tp

instance MinSublogic THFSl THFSubType where

minSublogic _ = tHF

instance MinSublogic THFSl THFPairConnective where

minSublogic _ = tHF0

instance MinSublogic THFSl THFBinaryTuple where

minSublogic bt = case bt of

TBT_THF_Or_Formula ufs -> foldr join tHF0 $ map minSublogic ufs

TBT_THF_And_Formula ufs -> foldr join tHF0 $ map minSublogic ufs

TBT_THF_Apply_Formula ufs -> foldr join tHF0 $ map minSublogic ufs

instance MinSublogic THFSl THFBinaryType where

minSublogic bt = case bt of

TBT_THF_Mapping_Type uts ->

join (if hasTType uts then tHF0_ST else tHF0) $

foldr join tHF0

(map minSublogic uts)

TBT_THF_Xprod_Type uts ->

foldr join (if hasTType uts then tHFP_ST else tHFP)

(map minSublogic uts)

TBT_THF_Union_Type uts ->

foldr join (if hasTType uts then tHF_ST else tHF)

(map minSublogic uts)

T0BT_THF_Binary_Type_Par bt' -> minSublogic bt'

where hasTType uts = foldr (&&) False $

map (\ut -> case ut of

T0UT_THF_Binary_Type_Par bt' -> hasTTypeB bt'

T0UT_Defined_Type DT_tType -> True

_ -> False) uts

hasTTypeB bt' =

case bt' of

TBT_THF_Mapping_Type uts' -> hasTType uts'

TBT_THF_Xprod_Type uts' -> hasTType uts'

TBT_THF_Union_Type uts' -> hasTType uts'

T0BT_THF_Binary_Type_Par bt'' -> hasTTypeB bt''

--fixme: maybe we need to check TUT_THF_Unitary_Formula for ShortTypes

--fixme: how does this differ from THF?

instance MinSublogic THFSl THFQuantifiedFormula where

minSublogic qf = case qf of

TQF_THF_Quantified_Formula qf' vs u -> join (minSublogic u) $

join (minSublogic qf')

(foldr join tHF0

(map minSublogic vs))

T0QF_THF_Quantified_Var qf' vs u -> join (minSublogic u) $

join (minSublogic qf')

(foldr join tHF0

(map minSublogic vs))

--note: T0QF_THF_Quantified_Var in THF0 is pretty much the same as

-- TQF_THF_Quantified_Formula in THF (cf. As.hs 190 ff.)

-- Maybe we should merge the two constructors?

T0QF_THF_Quantified_Novar qf' u -> join (minSublogic qf')

(minSublogic u)

-- fixme: not in THF?!?

instance MinSublogic THFSl THFUnaryConnective where

minSublogic uc = case uc of

Negation -> tHF0

PiForAll -> tHF

SigmaExists -> tHF

instance MinSublogic THFSl THFAtom where

minSublogic a = case a of

TA_Term _ -> tHF

TA_THF_Conn_Term conn ->

case conn of

TCT_THF_Pair_Connective pc -> join tHF $ minSublogic pc

TCT_Assoc_Connective _ -> tHF0

TCT_THF_Unary_Connective uc -> join tHF0 $ minSublogic uc

T0CT_THF_Quantifier qf -> join tHF0 $ minSublogic qf

TA_Defined_Type df -> join tHF $ minSublogic df

TA_Defined_Plain_Formula _ -> tHF

TA_System_Type _ -> tHF

TA_System_Atomic_Formula _ -> tHF

T0A_Constant _ -> tHF0

T0A_Defined_Constant _ -> tHF0

T0A_System_Constant _ -> tHF0

T0A_Variable _ -> tHF0

-- fixme: how do these in THF0 differ from THF?

instance MinSublogic THFSl THFVariable where

minSublogic v = case v of

TV_THF_Typed_Variable _ t -> join tHF0 $ minSublogic t

_ -> tHF0

instance MinSublogic THFSl THFQuantifier where

minSublogic qf = case qf of

T0Q_PiForAll -> tHF0

T0Q_SigmaExists -> tHF0

_ -> tHF

instance MinSublogic THFSl Quantifier where

minSublogic _ = tHF0

instance MinSublogic THFSl THFTopLevelType where

minSublogic tp = case tp of

TTLT_THF_Logic_Formula f -> join tHF $ minSublogic f

--fixme: maybe we need to check for ShortTypes extension?

T0TLT_Constant _ -> tHF0

T0TLT_Variable _ -> tHF0

T0TLT_Defined_Type df -> join tHF0 $ minSublogic df

T0TLT_System_Type _ -> tHF0

T0TLT_THF_Binary_Type bt -> join tHF0 $ minSublogic bt

--fixme: how do all these THF0 types differ from THF?

instance MinSublogic THFSl THFTypeableFormula where

minSublogic tf = case tf of

TTyF_THF_Atom a -> join tHF $ minSublogic a

TTyF_THF_Tuple ts -> foldr join tHFP $ map minSublogic ts

TTyF_THF_Logic_Formula f -> join tHF $ minSublogic f

instance MinSublogic THFSl DefinedType where

minSublogic df = case df of

DT_oType -> tHF0

DT_o -> tHF0

DT_iType -> tHF0

DT_i -> tHF0

DT_tType -> tHF0

DT_real -> tHF

DT_rat -> tHF

DT_int -> tHF

instance MinSublogic THFSl THFUnitaryType where

minSublogic ut = case ut of

TUT_THF_Unitary_Formula f -> join tHF $ minSublogic f

T0UT_Constant _ -> tHF0

T0UT_Variable _ -> tHF0

T0UT_Defined_Type df -> join tHF0 $ minSublogic df

T0UT_System_Type _ -> tHF0

T0UT_THF_Binary_Type_Par bt -> join tHF0 $ minSublogic bt

--fixme: how do all these THF0 types differ from THF?