bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder{- |

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederModule : $Header$

81d182b21020b815887e9057959228546cf61b6bChristian MaederDescription : Definition of signatures for the Edinburgh

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder Logical Framework

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederCopyright : (c) Kristina Sojakova, DFKI Bremen 2009

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maeder

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederMaintainer : k.sojakova@jacobs-university.de

fbb66ee3e170624835b99f7aa91980753cb5b472Christian MaederStability : experimental

f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederPortability : portable

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder-}

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maedermodule LF.Sign

0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder ( Var

0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder , NAME

0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder , MODULE

0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder , BASE

0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder , Symbol (..)

0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder , EXP (..)

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder , DECL

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder , DEF (..)

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder , Sign (..)

ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder , emptySig

ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder , addDef

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder , getAllSyms

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder , getDeclaredSyms

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder , getDefinedSyms

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder , getLocalSyms

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder , isConstant

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder , isDeclaredSym

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder , isDefinedSym

33a5d53a412ba0a4e5847f7538d6da2e22bd116cChristian Maeder , isLocalSym

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder , getSymType

e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maeder , getSymValue

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder , recForm

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder , printSymbol

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder , printExp

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder ) where

0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder

0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maederimport Common.Doc

0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maederimport Common.DocUtils

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maederimport Common.Keywords

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowskiimport Data.Maybe

2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maederimport qualified Data.List as List

b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maederimport qualified Data.Set as Set

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederimport qualified Data.Map as Map

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowskitype Var = String

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maedertype NAME = String

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maedertype MODULE = String

2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maedertype BASE = String

2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederdata Symbol = Symbol

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder { symBase :: BASE

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder , symModule :: MODULE

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder , symName :: NAME

2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder } deriving (Ord, Show)

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederdata EXP = Type

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder | Var Var

2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder | Const Symbol

0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder | Appl EXP [EXP]

0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder | Func [EXP] EXP

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder | Pi [DECL] EXP

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder | Lamb [DECL] EXP

2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder deriving (Ord, Show)

2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder

c44c23429c72f3a709e22a18f2ed6f05fc8cc765Christian Maedertype DECL = (Var,EXP)

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maederdata DEF = Def

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder { getSym :: Symbol

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder , getType :: EXP

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder , getValue :: Maybe EXP

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

2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder

2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maederdata Sign = Sign

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder { sigBase :: BASE

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder , sigModule :: MODULE

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder , getDefs :: [DEF]

2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder }

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder deriving (Show, Ord)

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder

0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian MaederemptySig :: Sign

0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian MaederemptySig = Sign "" "" []

3c62e6ef442caf092adcbecf6fccd957dcd72689Christian Maeder

2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaederaddDef :: DEF -> Sign -> Sign

2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaederaddDef d (Sign b m ds) = Sign b m $ ds ++ [d]

2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder

2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder-- get the set of all symbols

715ffaf874309df081d1e1cd8e05073fc1227729Christian MaedergetAllSyms :: Sign -> Set.Set Symbol

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaedergetAllSyms (Sign _ _ ds) = Set.fromList $ map getSym ds

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder-- checks if the symbol is defined or declared in the signature

0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian MaederisConstant :: Symbol -> Sign -> Bool

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian MaederisConstant s sig = Set.member s $ getAllSyms sig

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder

2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder-- get the set of declared symbols

f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian MaedergetDeclaredSyms :: Sign -> Set.Set Symbol

715ffaf874309df081d1e1cd8e05073fc1227729Christian MaedergetDeclaredSyms (Sign _ _ ds) =

0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder Set.fromList $ map getSym $ filter (\ d -> isNothing $ getValue d) ds

89dc77946055c0e4cb4671c4a74c3dcd55ed41a1Christian Maeder

2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder-- checks if the symbol is declared in the signature

36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederisDeclaredSym :: Symbol -> Sign -> Bool

2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaederisDeclaredSym s sig = Set.member s $ getDeclaredSyms sig

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder

836e72a3c413366ba9801726f3b249c7791cb9caChristian Maeder-- get the set of declared symbols

836e72a3c413366ba9801726f3b249c7791cb9caChristian MaedergetDefinedSyms :: Sign -> Set.Set Symbol

89dc77946055c0e4cb4671c4a74c3dcd55ed41a1Christian MaedergetDefinedSyms (Sign _ _ ds) =

2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder Set.fromList $ map getSym $ filter (\ d -> isJust $ getValue d) ds

2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- checks if the symbol is defined in the signature

149e43c4a2705a86a0e5fa301ba849fdf19db32eChristian MaederisDefinedSym :: Symbol -> Sign -> Bool

2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaederisDefinedSym s sig = Set.member s $ getDefinedSyms sig

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder-- get the set of symbols not included from other signatures

2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaedergetLocalSyms :: Sign -> Set.Set Symbol

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaedergetLocalSyms sig = Set.filter (\ s -> isLocalSym s sig) $ getAllSyms sig

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder-- checks if the symbol is local to the signature

89dc77946055c0e4cb4671c4a74c3dcd55ed41a1Christian MaederisLocalSym :: Symbol -> Sign -> Bool

2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaederisLocalSym s sig =

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder and [sigBase sig == symBase s, sigModule sig == symModule s]

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

d48085f765fca838c1d972d2123601997174583dChristian Maeder-- returns the type/kind for the given symbol

797f811e57952d59e73b8cd03b667eef276db972Christian MaedergetSymType :: Symbol -> Sign -> Maybe EXP

89dc77946055c0e4cb4671c4a74c3dcd55ed41a1Christian MaedergetSymType sym sig =

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder let res = List.find (\ d -> getSym d == sym) $ getDefs sig

3daa82a175c7cfabf22455aa77c4beda327404e4Christian Maeder in case res of

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Nothing -> Nothing

3daa82a175c7cfabf22455aa77c4beda327404e4Christian Maeder Just (Def _ t _) -> Just t

3daa82a175c7cfabf22455aa77c4beda327404e4Christian Maeder

3daa82a175c7cfabf22455aa77c4beda327404e4Christian Maeder-- returns the value for the given symbol, if it exists

3daa82a175c7cfabf22455aa77c4beda327404e4Christian MaedergetSymValue :: Symbol -> Sign -> Maybe EXP

36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedergetSymValue sym sig =

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder let res = List.find (\ d -> getSym d == sym) $ getDefs sig

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder in case res of

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder Nothing -> Nothing

89dc77946055c0e4cb4671c4a74c3dcd55ed41a1Christian Maeder Just (Def _ _ v) -> v

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder

149e43c4a2705a86a0e5fa301ba849fdf19db32eChristian Maeder-- pretty printing

2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maederinstance Pretty Sign where

1738d16957389457347bee85075d3d33d002158fChristian Maeder pretty = printSig

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian MaederprintSig :: Sign -> Doc

2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaederprintSig sig = vcat $ map (printDef sig) $ getDefs sig

89dc77946055c0e4cb4671c4a74c3dcd55ed41a1Christian Maeder

2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaederprintDef :: Sign -> DEF -> Doc

304c84f22dd78f7979efd81b8fc38c8d2197ed39Christian MaederprintDef sig (Def s t v) =

304c84f22dd78f7979efd81b8fc38c8d2197ed39Christian Maeder fsep

304c84f22dd78f7979efd81b8fc38c8d2197ed39Christian Maeder [ printSymbol sig s

304c84f22dd78f7979efd81b8fc38c8d2197ed39Christian Maeder , text "::" <+> printExp sig t

304c84f22dd78f7979efd81b8fc38c8d2197ed39Christian Maeder , case v of

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder Nothing -> empty

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder Just val -> text "=" <+> printExp sig val

e215ca0377dc79c9bcfb105157ecc4b958bec67bChristian Maeder ]

e215ca0377dc79c9bcfb105157ecc4b958bec67bChristian Maeder

e215ca0377dc79c9bcfb105157ecc4b958bec67bChristian MaederprintSymbol :: Sign -> Symbol -> Doc

e215ca0377dc79c9bcfb105157ecc4b958bec67bChristian MaederprintSymbol sig s =

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder if (isLocalSym s sig)

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder then text $ symName s

2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder else text (symModule s) <> text sigDelimS <> text (symName s)

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian MaederprintExp :: Sign -> EXP -> Doc

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederprintExp _ Type = text "type"

2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaederprintExp sig (Const s) = printSymbol sig s

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian MaederprintExp _ (Var n) = text n

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian MaederprintExp sig (Appl e es) =

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder let f = printExpWithPrec sig (precAppl + 1) e

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder as = map (printExpWithPrec sig precAppl) es

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder in hsep (f:as)

printExp sig (Func es e) =

let as = map (printExpWithPrec sig precFunc) es

val = printExpWithPrec sig (precFunc + 1) e

in hsep $ punctuate (text "-> ") (as ++ [val])

printExp sig (Pi ds e) = sep [braces $ printDecls sig ds, printExp sig e]

printExp sig (Lamb ds e) = sep [brackets $ printDecls sig ds, printExp sig e]

printExpWithPrec :: Sign -> Int -> EXP -> Doc

printExpWithPrec sig i e =

if prec e >= i

then parens $ printExp sig e

else printExp sig e

prec :: EXP -> Int

prec Type = 0

prec Const {} = 0

prec Var {} = 0

prec Appl {} = 1

prec Func {} = 2

prec Pi {} = 3

prec Lamb {} = 3

precFunc, precAppl :: Int

precFunc = 2

precAppl = 1

printDecls :: Sign -> [DECL] -> Doc

printDecls sig xs = sep $ punctuate comma $ map (printDecl sig) xs

printDecl :: Sign -> DECL -> Doc

printDecl sig (n,e) = sep [text n, colon <+> printExp sig e]

{- converts the expression into a form where each construct takes

exactly one argument -}

recForm :: EXP -> EXP

recForm (Appl f []) = recForm f

recForm (Appl f as) = Appl (recForm $ Appl f $ init as) $ [recForm $ last as]

recForm (Func [] a) = recForm a

recForm (Func (t:ts) a) = Func [recForm t] $ recForm $ Func ts a

recForm (Pi [] t) = recForm t

recForm (Pi ((n,t):ds) a) =

Pi [(n,recForm t)] $ recForm $ Pi ds a

recForm (Lamb [] t) = recForm t

recForm (Lamb ((n,t):ds) a) =

Lamb [(n,recForm t)] $ recForm $ Lamb ds a

recForm t = t

{- modifies the given name until it is different from each of the names

in the input set -}

getNewName :: Var -> Set.Set Var -> Var

getNewName var names = getNewNameH var names var 0

getNewNameH :: Var -> Set.Set Var -> Var -> Int -> Var

getNewNameH var names root i =

if (Set.notMember var names)

then var

else let newVar = root ++ (show i)

in getNewNameH newVar names root $ i+1

-- returns a set of free Variables used within an expression

getFreeVars :: EXP -> Set.Set Var

getFreeVars e = getFreeVarsH $ recForm e

getFreeVarsH :: EXP -> Set.Set Var

getFreeVarsH Type = Set.empty

getFreeVarsH (Const _) = Set.empty

getFreeVarsH (Var x) = Set.singleton x

getFreeVarsH (Appl f [a]) =

Set.union (getFreeVarsH f) (getFreeVarsH a)

getFreeVarsH (Func [t] v) =

Set.union (getFreeVarsH t) (getFreeVarsH v)

getFreeVarsH (Pi [(n,t)] a) =

Set.delete n $ Set.union (getFreeVarsH t) (getFreeVarsH a)

getFreeVarsH (Lamb [(n,t)] a) =

Set.delete n $ Set.union (getFreeVarsH t) (getFreeVarsH a)

getFreeVarsH _ = Set.empty

{- Variable renamings:

- the first argument specifies the desired Variable renamings

- the second argument specifies the set of Variables which cannot

be used as new Variable names -}

rename :: Map.Map Var Var -> Set.Set Var -> EXP -> EXP

rename m s e = renameH m s (recForm e)

renameH :: Map.Map Var Var -> Set.Set Var -> EXP -> EXP

renameH _ _ Type = Type

renameH _ _ (Const n) = Const n

renameH m _ (Var n) = Var $ Map.findWithDefault n n m

renameH m s (Appl f [a]) = Appl (rename m s f) [rename m s a]

renameH m s (Func [t] u) = Func [rename m s t] (rename m s u)

renameH m s (Pi [(x,t)] a) =

let t1 = rename m s t

x1 = getNewName x s

a1 = rename (Map.insert x x1 m) (Set.insert x1 s) a

in Pi [(x1,t1)] a1

renameH m s (Lamb [(x,t)] a) =

let t1 = rename m s t

x1 = getNewName x s

a1 = rename (Map.insert x x1 m) (Set.insert x1 s) a

in Lamb [(x1,t1)] a1

renameH _ _ t = t

-- equality

instance Eq Sign where

sig1 == sig2 = eqSig sig1 sig2

instance Eq Symbol where

s1 == s2 = eqSym s1 s2

instance Eq EXP where

e1 == e2 = eqExp (recForm e1) (recForm e2)

eqSig :: Sign -> Sign -> Bool

eqSig (Sign _ m1 d1) (Sign _ m2 d2) = (m1,d1) == (m2,d2)

eqSym :: Symbol -> Symbol -> Bool

eqSym (Symbol _ m1 n1) (Symbol _ m2 n2) = (m1,n1) == (m2,n2)

eqExp :: EXP -> EXP -> Bool

eqExp Type Type = True

eqExp (Const x1) (Const x2) = x1 == x2

eqExp (Var x1) (Var x2) = x1 == x2

eqExp (Appl f1 [a1]) (Appl f2 [a2]) = and [f1 == f2, a1 == a2]

eqExp (Func [t1] s1) (Func [t2] s2) = and [t1 == t2, s1 == s2]

eqExp (Pi [(n1,t1)] s1) (Pi [(n2,t2)] s2) =

let vars = Set.delete n1 $ getFreeVars s1

vars1 = Set.delete n2 $ getFreeVars s2

in if (vars1 /= vars)

then False

else let s3 = rename (Map.singleton n2 n1) (Set.insert n1 vars) s2

in and [t1 == t2, s1 == s3]

eqExp (Lamb [(n1,t1)] s1) (Lamb [(n2,t2)] s2) =

let vars = Set.delete n1 $ getFreeVars s1

vars1 = Set.delete n2 $ getFreeVars s2

in if (vars1 /= vars)

then False

else let s3 = rename (Map.singleton n2 n1) (Set.insert n1 vars) s2

in and [t1 == t2, s1 == s3]

eqExp _ _ = False