Copyright	(c) Jonathan von Schroeder DFKI Bremen 2012
License	GPLv2 or higher, see LICENSE.txt
Maintainer	Jonathan von Schroeder <jonathan.von_schroeder@dfki.de>
Stability	experimental
Portability	non-portable (via Logic.Logic)
Safe Haskell	None

THF.Sublogic

Description

Sublogics for THF

Documentation

data THFCoreSl Source #

Constructors

THF
THFP
THF0

Instances

Instances details

Eq THFCoreSl Source #
Instance details Defined in THF.Sublogic Methods (==) :: THFCoreSl -> THFCoreSl -> Bool (/=) :: THFCoreSl -> THFCoreSl -> Bool
Data THFCoreSl Source #
Instance details Defined in THF.Sublogic Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THFCoreSl -> c THFCoreSl gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THFCoreSl toConstr :: THFCoreSl -> Constr dataTypeOf :: THFCoreSl -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c THFCoreSl) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THFCoreSl) gmapT :: (forall b. Data b => b -> b) -> THFCoreSl -> THFCoreSl gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THFCoreSl -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THFCoreSl -> r gmapQ :: (forall d. Data d => d -> u) -> THFCoreSl -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THFCoreSl -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THFCoreSl -> m THFCoreSl gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THFCoreSl -> m THFCoreSl gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THFCoreSl -> m THFCoreSl
Ord THFCoreSl Source #
Instance details Defined in THF.Sublogic Methods compare :: THFCoreSl -> THFCoreSl -> Ordering (<) :: THFCoreSl -> THFCoreSl -> Bool (<=) :: THFCoreSl -> THFCoreSl -> Bool (>) :: THFCoreSl -> THFCoreSl -> Bool (>=) :: THFCoreSl -> THFCoreSl -> Bool max :: THFCoreSl -> THFCoreSl -> THFCoreSl min :: THFCoreSl -> THFCoreSl -> THFCoreSl
Show THFCoreSl Source #
Instance details Defined in THF.Sublogic Methods showsPrec :: Int -> THFCoreSl -> ShowS show :: THFCoreSl -> String showList :: [THFCoreSl] -> ShowS
Generic THFCoreSl
Instance details Defined in THF.ATC_THF Associated Types type Rep THFCoreSl :: Type -> Type Methods from :: THFCoreSl -> Rep THFCoreSl x to :: Rep THFCoreSl x -> THFCoreSl
FromJSON THFCoreSl
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser THFCoreSl parseJSONList :: Value -> Parser [THFCoreSl]
ToJSON THFCoreSl
Instance details Defined in THF.ATC_THF Methods toJSON :: THFCoreSl -> Value toEncoding :: THFCoreSl -> Encoding toJSONList :: [THFCoreSl] -> Value toEncodingList :: [THFCoreSl] -> Encoding
ShATermConvertible THFCoreSl
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> THFCoreSl -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [THFCoreSl] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, THFCoreSl) fromShATermList' :: Int -> ATermTable -> (ATermTable, [THFCoreSl])
type Rep THFCoreSl
Instance details Defined in THF.ATC_THF type Rep THFCoreSl = D1 ('MetaData "THFCoreSl" "THF.Sublogic" "main" 'False) (C1 ('MetaCons "THF" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "THFP" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "THF0" 'PrefixI 'False) (U1 :: Type -> Type)))

data THFSl Source #

Constructors

THFSl
Fields core :: THFCoreSl ext_Poly :: Bool

Instances

Instances details

Eq THFSl Source #
Instance details Defined in THF.Sublogic Methods (==) :: THFSl -> THFSl -> Bool (/=) :: THFSl -> THFSl -> Bool
Data THFSl Source #
Instance details Defined in THF.Sublogic Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THFSl -> c THFSl gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THFSl toConstr :: THFSl -> Constr dataTypeOf :: THFSl -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c THFSl) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THFSl) gmapT :: (forall b. Data b => b -> b) -> THFSl -> THFSl gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THFSl -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THFSl -> r gmapQ :: (forall d. Data d => d -> u) -> THFSl -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THFSl -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THFSl -> m THFSl gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THFSl -> m THFSl gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THFSl -> m THFSl
Ord THFSl Source #
Instance details Defined in THF.Sublogic Methods compare :: THFSl -> THFSl -> Ordering (<) :: THFSl -> THFSl -> Bool (<=) :: THFSl -> THFSl -> Bool (>) :: THFSl -> THFSl -> Bool (>=) :: THFSl -> THFSl -> Bool max :: THFSl -> THFSl -> THFSl min :: THFSl -> THFSl -> THFSl
Show THFSl Source #
Instance details Defined in THF.Sublogic Methods showsPrec :: Int -> THFSl -> ShowS show :: THFSl -> String showList :: [THFSl] -> ShowS
Generic THFSl
Instance details Defined in THF.ATC_THF Associated Types type Rep THFSl :: Type -> Type Methods from :: THFSl -> Rep THFSl x to :: Rep THFSl x -> THFSl
FromJSON THFSl
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser THFSl parseJSONList :: Value -> Parser [THFSl]
ToJSON THFSl
Instance details Defined in THF.ATC_THF Methods toJSON :: THFSl -> Value toEncoding :: THFSl -> Encoding toJSONList :: [THFSl] -> Value toEncodingList :: [THFSl] -> Encoding
ShATermConvertible THFSl
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> THFSl -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [THFSl] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, THFSl) fromShATermList' :: Int -> ATermTable -> (ATermTable, [THFSl])
SublogicName THFSl Source #
Instance details Defined in THF.Logic_THF Methods sublogicName :: THFSl -> String Source #
SemiLatticeWithTop THFSl Source #
Instance details Defined in THF.Logic_THF Methods lub :: THFSl -> THFSl -> THFSl Source # top :: THFSl Source #
ProjectSublogicM THFSl () Source #
Instance details Defined in THF.Logic_THF Methods projectSublogicM :: THFSl -> () -> Maybe () Source #
ProjectSublogicM THFSl SymbolTHF Source #
Instance details Defined in THF.Logic_THF Methods projectSublogicM :: THFSl -> SymbolTHF -> Maybe SymbolTHF Source #
ProjectSublogic THFSl BasicSpecTHF Source #
Instance details Defined in THF.Logic_THF Methods projectSublogic :: THFSl -> BasicSpecTHF -> BasicSpecTHF Source #
ProjectSublogic THFSl SignTHF Source #
Instance details Defined in THF.Logic_THF Methods projectSublogic :: THFSl -> SignTHF -> SignTHF Source #
ProjectSublogic THFSl MorphismTHF Source #
Instance details Defined in THF.Logic_THF Methods projectSublogic :: THFSl -> MorphismTHF -> MorphismTHF Source #
MinSublogic THFSl () Source #
Instance details Defined in THF.Logic_THF Methods minSublogic :: () -> THFSl Source #
MinSublogic THFSl DefinedType Source #
Instance details Defined in THF.Sublogic Methods minSublogic :: DefinedType -> THFSl Source #
MinSublogic THFSl THFUnaryConnective Source #
Instance details Defined in THF.Sublogic Methods minSublogic :: THFUnaryConnective -> THFSl Source #
MinSublogic THFSl THFPairConnective Source #
Instance details Defined in THF.Sublogic Methods minSublogic :: THFPairConnective -> THFSl Source #
MinSublogic THFSl Quantifier Source #
Instance details Defined in THF.Sublogic Methods minSublogic :: Quantifier -> THFSl Source #
MinSublogic THFSl THFQuantifier Source #
Instance details Defined in THF.Sublogic Methods minSublogic :: THFQuantifier -> THFSl Source #
MinSublogic THFSl THFSequent Source #
Instance details Defined in THF.Sublogic Methods minSublogic :: THFSequent -> THFSl Source #
MinSublogic THFSl THFAtom Source #
Instance details Defined in THF.Sublogic Methods minSublogic :: THFAtom -> THFSl Source #
MinSublogic THFSl THFBinaryType Source #
Instance details Defined in THF.Sublogic Methods minSublogic :: THFBinaryType -> THFSl Source #
MinSublogic THFSl THFUnitaryType Source #
Instance details Defined in THF.Sublogic Methods minSublogic :: THFUnitaryType -> THFSl Source #
MinSublogic THFSl THFTopLevelType Source #
Instance details Defined in THF.Sublogic Methods minSublogic :: THFTopLevelType -> THFSl Source #
MinSublogic THFSl THFSubType Source #
Instance details Defined in THF.Sublogic Methods minSublogic :: THFSubType -> THFSl Source #
MinSublogic THFSl THFTypeableFormula Source #
Instance details Defined in THF.Sublogic Methods minSublogic :: THFTypeableFormula -> THFSl Source #
MinSublogic THFSl THFTypeFormula Source #
Instance details Defined in THF.Sublogic Methods minSublogic :: THFTypeFormula -> THFSl Source #
MinSublogic THFSl THFTypedConst Source #
Instance details Defined in THF.Sublogic Methods minSublogic :: THFTypedConst -> THFSl Source #
MinSublogic THFSl THFVariable Source #
Instance details Defined in THF.Sublogic Methods minSublogic :: THFVariable -> THFSl Source #
MinSublogic THFSl THFQuantifiedFormula Source #
Instance details Defined in THF.Sublogic Methods minSublogic :: THFQuantifiedFormula -> THFSl Source #
MinSublogic THFSl THFUnitaryFormula Source #
Instance details Defined in THF.Sublogic Methods minSublogic :: THFUnitaryFormula -> THFSl Source #
MinSublogic THFSl THFBinaryTuple Source #
Instance details Defined in THF.Sublogic Methods minSublogic :: THFBinaryTuple -> THFSl Source #
MinSublogic THFSl THFBinaryFormula Source #
Instance details Defined in THF.Sublogic Methods minSublogic :: THFBinaryFormula -> THFSl Source #
MinSublogic THFSl THFLogicFormula Source #
Instance details Defined in THF.Sublogic Methods minSublogic :: THFLogicFormula -> THFSl Source #
MinSublogic THFSl THFFormula Source #
Instance details Defined in THF.Sublogic Methods minSublogic :: THFFormula -> THFSl Source #
MinSublogic THFSl Kind Source #
Instance details Defined in THF.Logic_THF Methods minSublogic :: Kind -> THFSl Source #
MinSublogic THFSl Type Source #
Instance details Defined in THF.Logic_THF Methods minSublogic :: Type -> THFSl Source #
MinSublogic THFSl SymbolTHF Source #
Instance details Defined in THF.Logic_THF Methods minSublogic :: SymbolTHF -> THFSl Source #
MinSublogic THFSl BasicSpecTHF Source #
Instance details Defined in THF.Logic_THF Methods minSublogic :: BasicSpecTHF -> THFSl Source #
MinSublogic THFSl SignTHF Source #
Instance details Defined in THF.Logic_THF Methods minSublogic :: SignTHF -> THFSl Source #
MinSublogic THFSl MorphismTHF Source #
Instance details Defined in THF.Logic_THF Methods minSublogic :: MorphismTHF -> THFSl Source #
Logic THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source #
Instance details Defined in THF.Logic_THF Methods parse_basic_sen :: THF -> Maybe (BasicSpecTHF -> AParser st THFFormula) Source # stability :: THF -> Stability Source # data_logic :: THF -> Maybe AnyLogic Source # top_sublogic :: THF -> THFSl Source # all_sublogics :: THF -> [THFSl] Source # bottomSublogic :: THF -> Maybe THFSl Source # sublogicDimensions :: THF -> [[THFSl]] Source # parseSublogic :: THF -> String -> Maybe THFSl Source # proj_sublogic_epsilon :: THF -> THFSl -> SignTHF -> MorphismTHF Source # provers :: THF -> [Prover SignTHF THFFormula MorphismTHF THFSl ProofTree] Source # default_prover :: THF -> String Source # cons_checkers :: THF -> [ConsChecker SignTHF THFFormula THFSl MorphismTHF ProofTree] Source # conservativityCheck :: THF -> [ConservativityChecker SignTHF THFFormula MorphismTHF] Source # empty_proof_tree :: THF -> ProofTree Source # syntaxTable :: THF -> SignTHF -> Maybe SyntaxTable Source # omdoc_metatheory :: THF -> Maybe OMCD Source # export_symToOmdoc :: THF -> NameMap SymbolTHF -> SymbolTHF -> String -> Result TCElement Source # export_senToOmdoc :: THF -> NameMap SymbolTHF -> THFFormula -> Result TCorOMElement Source # export_theoryToOmdoc :: THF -> SigMap SymbolTHF -> SignTHF -> [Named THFFormula] -> Result [TCElement] Source # omdocToSym :: THF -> SigMapI SymbolTHF -> TCElement -> String -> Result SymbolTHF Source # omdocToSen :: THF -> SigMapI SymbolTHF -> TCElement -> String -> Result (Maybe (Named THFFormula)) Source # addOMadtToTheory :: THF -> SigMapI SymbolTHF -> (SignTHF, [Named THFFormula]) -> [[OmdADT]] -> Result (SignTHF, [Named THFFormula]) Source # addOmdocToTheory :: THF -> SigMapI SymbolTHF -> (SignTHF, [Named THFFormula]) -> [TCElement] -> Result (SignTHF, [Named THFFormula]) Source # sublogicOfTheo :: THF -> (SignTHF, [THFFormula]) -> THFSl Source #
Comorphism THFP_P2THFP THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source #
Instance details Defined in Comorphisms.THFP_P2THFP Methods sourceLogic :: THFP_P2THFP -> THF Source # sourceSublogic :: THFP_P2THFP -> THFSl Source # sourceSublogicLossy :: THFP_P2THFP -> THFSl Source # minSourceTheory :: THFP_P2THFP -> Maybe (LibName, String) Source # targetLogic :: THFP_P2THFP -> THF Source # mapSublogic :: THFP_P2THFP -> THFSl -> Maybe THFSl Source # map_theory :: THFP_P2THFP -> (SignTHF, [Named THFFormula]) -> Result (SignTHF, [Named THFFormula]) Source # mapMarkedTheory :: THFP_P2THFP -> (SignTHF, [Named THFFormula]) -> Result (SignTHF, [Named THFFormula]) Source # map_morphism :: THFP_P2THFP -> MorphismTHF -> Result MorphismTHF Source # map_sentence :: THFP_P2THFP -> SignTHF -> THFFormula -> Result THFFormula Source # map_symbol :: THFP_P2THFP -> SignTHF -> SymbolTHF -> Set SymbolTHF Source # extractModel :: THFP_P2THFP -> SignTHF -> ProofTree -> Result (SignTHF, [Named THFFormula]) Source # is_model_transportable :: THFP_P2THFP -> Bool Source # has_model_expansion :: THFP_P2THFP -> Bool Source # is_weakly_amalgamable :: THFP_P2THFP -> Bool Source # constituents :: THFP_P2THFP -> [String] Source # isInclusionComorphism :: THFP_P2THFP -> Bool Source # rps :: THFP_P2THFP -> Bool Source # eps :: THFP_P2THFP -> Bool Source # isGTC :: THFP_P2THFP -> Bool Source #
Comorphism THFP_P2HasCASL THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.THFP_P2HasCASL Methods sourceLogic :: THFP_P2HasCASL -> THF Source # sourceSublogic :: THFP_P2HasCASL -> THFSl Source # sourceSublogicLossy :: THFP_P2HasCASL -> THFSl Source # minSourceTheory :: THFP_P2HasCASL -> Maybe (LibName, String) Source # targetLogic :: THFP_P2HasCASL -> HasCASL Source # mapSublogic :: THFP_P2HasCASL -> THFSl -> Maybe Sublogic Source # map_theory :: THFP_P2HasCASL -> (SignTHF, [Named THFFormula]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: THFP_P2HasCASL -> (SignTHF, [Named THFFormula]) -> Result (Env, [Named Sentence]) Source # map_morphism :: THFP_P2HasCASL -> MorphismTHF -> Result Morphism Source # map_sentence :: THFP_P2HasCASL -> SignTHF -> THFFormula -> Result Sentence Source # map_symbol :: THFP_P2HasCASL -> SignTHF -> SymbolTHF -> Set Symbol Source # extractModel :: THFP_P2HasCASL -> SignTHF -> () -> Result (SignTHF, [Named THFFormula]) Source # is_model_transportable :: THFP_P2HasCASL -> Bool Source # has_model_expansion :: THFP_P2HasCASL -> Bool Source # is_weakly_amalgamable :: THFP_P2HasCASL -> Bool Source # constituents :: THFP_P2HasCASL -> [String] Source # isInclusionComorphism :: THFP_P2HasCASL -> Bool Source # rps :: THFP_P2HasCASL -> Bool Source # eps :: THFP_P2HasCASL -> Bool Source # isGTC :: THFP_P2HasCASL -> Bool Source #
Comorphism THFP2THF0 THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source #
Instance details Defined in Comorphisms.THFP2THF0 Methods sourceLogic :: THFP2THF0 -> THF Source # sourceSublogic :: THFP2THF0 -> THFSl Source # sourceSublogicLossy :: THFP2THF0 -> THFSl Source # minSourceTheory :: THFP2THF0 -> Maybe (LibName, String) Source # targetLogic :: THFP2THF0 -> THF Source # mapSublogic :: THFP2THF0 -> THFSl -> Maybe THFSl Source # map_theory :: THFP2THF0 -> (SignTHF, [Named THFFormula]) -> Result (SignTHF, [Named THFFormula]) Source # mapMarkedTheory :: THFP2THF0 -> (SignTHF, [Named THFFormula]) -> Result (SignTHF, [Named THFFormula]) Source # map_morphism :: THFP2THF0 -> MorphismTHF -> Result MorphismTHF Source # map_sentence :: THFP2THF0 -> SignTHF -> THFFormula -> Result THFFormula Source # map_symbol :: THFP2THF0 -> SignTHF -> SymbolTHF -> Set SymbolTHF Source # extractModel :: THFP2THF0 -> SignTHF -> ProofTree -> Result (SignTHF, [Named THFFormula]) Source # is_model_transportable :: THFP2THF0 -> Bool Source # has_model_expansion :: THFP2THF0 -> Bool Source # is_weakly_amalgamable :: THFP2THF0 -> Bool Source # constituents :: THFP2THF0 -> [String] Source # isInclusionComorphism :: THFP2THF0 -> Bool Source # rps :: THFP2THF0 -> Bool Source # eps :: THFP2THF0 -> Bool Source # isGTC :: THFP2THF0 -> Bool Source #
Comorphism HasCASL2THFP_P HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source #
Instance details Defined in Comorphisms.HasCASL2THFP_P Methods sourceLogic :: HasCASL2THFP_P -> HasCASL Source # sourceSublogic :: HasCASL2THFP_P -> Sublogic Source # sourceSublogicLossy :: HasCASL2THFP_P -> Sublogic Source # minSourceTheory :: HasCASL2THFP_P -> Maybe (LibName, String) Source # targetLogic :: HasCASL2THFP_P -> THF Source # mapSublogic :: HasCASL2THFP_P -> Sublogic -> Maybe THFSl Source # map_theory :: HasCASL2THFP_P -> (Env, [Named Sentence]) -> Result (SignTHF, [Named THFFormula]) Source # mapMarkedTheory :: HasCASL2THFP_P -> (Env, [Named Sentence]) -> Result (SignTHF, [Named THFFormula]) Source # map_morphism :: HasCASL2THFP_P -> Morphism -> Result MorphismTHF Source # map_sentence :: HasCASL2THFP_P -> Env -> Sentence -> Result THFFormula Source # map_symbol :: HasCASL2THFP_P -> Env -> Symbol -> Set SymbolTHF Source # extractModel :: HasCASL2THFP_P -> Env -> ProofTree -> Result (Env, [Named Sentence]) Source # is_model_transportable :: HasCASL2THFP_P -> Bool Source # has_model_expansion :: HasCASL2THFP_P -> Bool Source # is_weakly_amalgamable :: HasCASL2THFP_P -> Bool Source # constituents :: HasCASL2THFP_P -> [String] Source # isInclusionComorphism :: HasCASL2THFP_P -> Bool Source # rps :: HasCASL2THFP_P -> Bool Source # eps :: HasCASL2THFP_P -> Bool Source # isGTC :: HasCASL2THFP_P -> Bool Source #
type Rep THFSl
Instance details Defined in THF.ATC_THF type Rep THFSl = D1 ('MetaData "THFSl" "THF.Sublogic" "main" 'False) (C1 ('MetaCons "THFSl" 'PrefixI 'True) (S1 ('MetaSel ('Just "core") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFCoreSl) :*: S1 ('MetaSel ('Just "ext_Poly") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))

joinCoreSl :: THFCoreSl -> THFCoreSl -> THFCoreSl Source #

joinSL :: THFSl -> THFSl -> THFSl Source #

tHF0 :: THFSl Source #

tHFP :: THFSl Source #

tHF :: THFSl Source #

tHF0_P :: THFSl Source #

tHFP_P :: THFSl Source #

tHF_P :: THFSl Source #

sublogics_all :: [THFSl] Source #