2509N/A{- |

0N/AModule : $Header$

0N/ADescription : printing Isabelle entities

0N/ACopyright : (c) University of Cambridge, Cambridge, England

0N/A adaption (c) Till Mossakowski, Uni Bremen 2002-2006

0N/ALicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

0N/A

0N/AMaintainer : Christian.Maeder@dfki.de

0N/AStability : provisional

0N/APortability : portable

0N/A

0N/APrinting functions for Isabelle logic.

0N/A-}

0N/A

0N/Amodule Isabelle.IsaPrint

0N/A ( showBaseSig

0N/A , printIsaTheory

2362N/A , getAxioms

2362N/A , printNamedSen

2362N/A ) where

0N/A

2509N/Aimport Isabelle.IsaSign

0N/Aimport Isabelle.IsaConsts

0N/A

1178N/Aimport Common.AS_Annotation

0N/Aimport qualified Data.Map as Map

0N/Aimport Common.Doc hiding (bar)

0N/Aimport Common.DocUtils

0N/A

0N/Aimport Data.Char

0N/Aimport Data.List

0N/A

0N/AprintIsaTheory :: String -> String -> Sign -> [Named Sentence] -> Doc

0N/AprintIsaTheory tn _ sign sens = let

0N/A b = baseSig sign

0N/A bs = showBaseSig b

0N/A ld = "$HETS_LIB/Isabelle/"

0N/A use = text usesS <+> doubleQuotes (text $ ld ++ "prelude")

0N/A in text theoryS <+> text tn

0N/A $+$ text importsS <+> (if case b of

0N/A Main_thy -> False

0N/A HOLCF_thy -> False

0N/A _ -> True then doubleQuotes

0N/A $ text $ ld ++ bs else text bs)

0N/A $+$ use

0N/A $+$ text beginS

0N/A $++$ printTheoryBody sign sens

1178N/A $++$ text endS

0N/A

0N/AprintTheoryBody :: Sign -> [Named Sentence] -> Doc

0N/AprintTheoryBody sig sens =

0N/A let (axs, rest) =

0N/A getAxioms $ filter ( \ ns -> sentence ns /= mkSen true) sens

1178N/A (defs, rs) = getDefs rest

1178N/A (rdefs, ts) = getRecDefs rs

0N/A tNames = map senName $ ts ++ axs

0N/A in

0N/A callML "initialize" (brackets $ sepByCommas

1178N/A $ map (text . show . Quote) tNames) $++$

0N/A printSign sig $++$

0N/A (if null axs then empty else text axiomsS $+$

0N/A vsep (map printNamedSen axs)) $++$

1178N/A (if null defs then empty else text defsS $+$

0N/A vsep (map printNamedSen defs)) $++$

0N/A vsep (map printNamedSen rdefs) $++$

1178N/A vcat (map ( \ a -> text declareS <+> text (senName a)

1178N/A <+> brackets (text simpS))

0N/A $ filter ( \ a -> case sentence a of

0N/A b@Sentence{} -> isSimp b

0N/A _ -> False) axs) $++$

0N/A vsep (map ( \ t -> printNamedSen t $+$

1178N/A text (case sentence t of

0N/A Sentence { thmProof = Just s } -> s

0N/A _ -> oopsS)

0N/A $++$ callML "record" (text $ show $ Quote $ senName t)) ts)

0N/A $++$ printMonSign sig

0N/A

0N/AcallML :: String -> Doc -> Doc

0N/AcallML fun args =

0N/A text mlS <+> doubleQuotes (fsep [text ("Header." ++ fun), args])

0N/A

0N/Adata QuotedString = Quote String

0N/Ainstance Show QuotedString where

0N/A show (Quote s) = init . tail . show $ show s

0N/A

0N/AgetAxioms, getDefs, getRecDefs :: [Named Sentence] ->

0N/A ([Named Sentence], [Named Sentence])

0N/A

0N/AgetAxioms = partition ( \ s -> case sentence s of

0N/A Sentence {} -> isAxiom s

0N/A _ -> False)

0N/A

0N/AgetDefs = partition ( \ s -> case sentence s of

0N/A ConstDef {} -> True

1178N/A _ -> False)

1178N/A

1178N/AgetRecDefs = partition ( \ s -> case sentence s of

1178N/A RecDef {} -> True

0N/A _ -> False)

0N/A

0N/A------------------- Printing functions -------------------

0N/A

0N/AshowBaseSig :: BaseSig -> String

0N/AshowBaseSig = reverse . drop 4 . reverse . show

0N/A

1178N/AprintClass :: IsaClass -> Doc

0N/AprintClass (IsaClass x) = text x

1178N/A

1178N/AprintSort :: Sort -> Doc

1178N/AprintSort l = case l of

0N/A [c] -> printClass c

0N/A _ -> specBraces . hsep . punctuate comma $ map printClass l

1178N/A

1178N/Adata SynFlag = Quoted | Unquoted | Null

0N/A

0N/AdoubleColon :: Doc

0N/AdoubleColon = text "::"

1178N/A

0N/Abar :: [Doc] -> [Doc]

0N/Abar = punctuate $ space <> text "|"

0N/A

1178N/AprintType :: Typ -> Doc

0N/AprintType = printTyp Unquoted

0N/A

0N/AprintTyp :: SynFlag -> Typ -> Doc

1178N/AprintTyp a = fst . printTypeAux a

0N/A

0N/AprintTypeAux :: SynFlag -> Typ -> (Doc, Int)

0N/AprintTypeAux a t = case t of

1178N/A (TFree v s) -> (let d = text $ if isPrefixOf "\'" v || isPrefixOf "?\'" v

0N/A then v else '\'' : v

0N/A c = printSort s

0N/A in if null s then d else case a of

1178N/A Quoted -> d <> doubleColon <> if null $ tail s then c else doubleQuotes c

0N/A Unquoted -> d <> doubleColon <> c

0N/A Null -> d, 1000)

0N/A (TVar iv s) -> printTypeAux a $ TFree ("?\'" ++ unindexed iv) s

0N/A (Type name _ args) -> case args of

1178N/A [t1, t2] | elem name [prodS, sProdS, funS, cFunS, sSumS] ->

0N/A printTypeOp a name t1 t2

0N/A _ -> ((case args of

0N/A [] -> empty

0N/A [arg] -> let (d, i) = printTypeAux a arg in

1178N/A if i < 1000 then parens d else d

0N/A _ -> parens $ hsep $ punctuate comma $

0N/A map (fst . printTypeAux a) args)

0N/A <+> text name, 1000)

1178N/A

1178N/AprintTypeOp :: SynFlag -> TName -> Typ -> Typ -> (Doc, Int)

0N/AprintTypeOp x name r1 r2 =

0N/A let (d1, i1) = printTypeAux x r1

0N/A (d2, i2) = printTypeAux x r2

0N/A (l, r) = Map.findWithDefault (0 :: Int, 0 :: Int)

0N/A name $ Map.fromList

0N/A [ (funS, (1,0))

1178N/A , (cFunS, (1,0))

1178N/A , (sSumS, (11, 10))

0N/A , (prodS, (21, 20))

1178N/A , (sProdS, (21, 20))

1178N/A ]

0N/A d3 = if i1 < l then parens d1 else d1

1178N/A d4 = if i2 < r then parens d2 else d2

1178N/A in (d3 <+> text name <+> d4, r)

0N/A

1178N/Aand_docs :: [Doc] -> Doc

1178N/Aand_docs ds = vcat $ prepPunctuate (text andS <> space) ds

0N/A

0N/A-- | printing a named sentence

0N/AprintNamedSen :: Named Sentence -> Doc

0N/AprintNamedSen ns =

let s = sentence ns

lab = senName ns

b = isAxiom ns

d = printSentence s

in case s of

RecDef {} -> d

_ -> let dd = doubleQuotes d in

if isRefute s then text lemmaS <+> text lab <+> colon

<+> dd $+$ text refuteS

else if null lab then dd else fsep[ (case s of

ConstDef {} -> text $ lab ++ "_def"

Sentence {} ->

(if b then empty else text theoremS)

<+> text lab <+> (if b then text "[rule_format]" else empty)

_ -> error "printNamedSen") <+> colon, dd]

-- | sentence printing

printSentence :: Sentence -> Doc

printSentence s = case s of

RecDef kw xs -> text kw <+>

and_docs (map (vcat . map (doubleQuotes . printTerm)) xs)

_ -> printPlainTerm (not $ isRefute s) $ senTerm s

-- | print plain term

printTerm :: Term -> Doc

printTerm = printPlainTerm True

printPlainTerm :: Bool -> Term -> Doc

printPlainTerm b = fst . printTrm b

-- | print parens but leave a space if doc starts or ends with a bar

parensForTerm :: Doc -> Doc

parensForTerm d =

let s = show d

b = '|'

in parens $ if null s then d

else (if head s == b then (space <>) else id)

((if last s == b then (<> space) else id) d)

printParenTerm :: Bool -> Int -> Term -> Doc

printParenTerm b i t = case printTrm b t of

(d, j) -> if j < i then parensForTerm d else d

flatTuplex :: [Term] -> Continuity -> [Term]

flatTuplex cs c = case cs of

[] -> cs

_ -> case last cs of

Tuplex rs@(_ : _ : _) d | d == c -> init cs ++ flatTuplex rs d

_ -> cs

printMixfixAppl :: Bool -> Continuity -> Term -> [Term] -> (Doc, Int)

printMixfixAppl b c f args = case f of

Const (VName n (Just (AltSyntax s is i))) _ -> let l = length is in

case compare l $ length args of

EQ -> if b || n == cNot || isPrefixOf "op " n then

(fsep $ replaceUnderlines s

$ zipWith (printParenTerm b) is args, i)

else printApp b c f args

LT -> let (fargs, rargs) = splitAt l args

(d, p) = printMixfixAppl b c f fargs

e = if p < maxPrio - 1 then parensForTerm d else d

in printDocApp b c e rargs

GT -> printApp b c f args

Const vn _ | new vn `elem` [allS, exS, ex1S] -> case args of

[Abs v t _] -> (fsep [text (new vn) <+> printPlainTerm False v

<> text "."

, printPlainTerm b t], lowPrio)

_ -> printApp b c f args

App g a d | c == d -> printMixfixAppl b c g (a : args)

_ -> printApp b c f args

-- | print the term using the alternative syntax (if True)

printTrm :: Bool -> Term -> (Doc, Int)

printTrm b trm = case trm of

Const vn ty -> let

dvn = text $ new vn

nvn = case ty of

_ | ty == noType -> dvn

_ -> parens $ dvn <+> doubleColon <+> printType ty

in case altSyn vn of

Nothing -> (nvn, maxPrio)

Just (AltSyntax s is i) -> if b && null is then

(fsep $ replaceUnderlines s [], i) else (nvn, maxPrio)

Free vn -> (text $ new vn, maxPrio)

Abs v t c -> ((text $ case c of

NotCont -> "%"

IsCont -> "LAM") <+> printPlainTerm False v <> text "."

<+> printPlainTerm b t, lowPrio)

If i t e c -> let d = fsep [printPlainTerm b i,

text "then" <+> printPlainTerm b t,

text "else" <+> printPlainTerm b e]

in case c of

NotCont -> (text "if" <+> d, lowPrio)

IsCont -> (text "If" <+> d <+> text "fi", maxPrio)

Case e ps -> (text "case" <+> printPlainTerm b e <+> text "of"

$+$ vcat (bar $ map (\ (p, t) ->

fsep [ printPlainTerm b p <+> text "=>"

, printParenTerm b (lowPrio + 1) t]) ps), lowPrio)

Let es i -> (fsep [text "let" <+>

vcat (punctuate semi $

map (\ (p, t) -> fsep [ printPlainTerm b p <+> text "="

, printPlainTerm b t]) es)

, text "in" <+> printPlainTerm b i], lowPrio)

IsaEq t1 t2 -> (fsep [ printParenTerm b (isaEqPrio + 1) t1 <+> text "=="

, printParenTerm b isaEqPrio t2], isaEqPrio)

Tuplex cs c -> ((case c of

NotCont -> parensForTerm

IsCont -> \ d -> text "<" <+> d <+> text ">") $

sepByCommas (map (printPlainTerm b) $ flatTuplex cs c)

, maxPrio)

App f a c -> printMixfixAppl b c f [a]

printApp :: Bool -> Continuity -> Term -> [Term] -> (Doc, Int)

printApp b c t l = case l of

[] -> printTrm b t

_ -> printDocApp b c (printParenTerm b (maxPrio - 1) t) l

printDocApp :: Bool -> Continuity -> Doc -> [Term] -> (Doc, Int)

printDocApp b c d l =

(fsep $ (case c of

NotCont -> id

IsCont -> punctuate $ text " $")

$ d : map (printParenTerm b maxPrio) l

, maxPrio - 1)

replaceUnderlines :: String -> [Doc] -> [Doc]

replaceUnderlines str l = case str of

"" -> []

'\'': r@(q : s) -> if q `elem` "_/'()"

then cons (text [q]) $ replaceUnderlines s l

else cons (text "'") $ replaceUnderlines r l

'_' : r -> case l of

h : t -> cons h $ replaceUnderlines r t

_ -> error "replaceUnderlines"

'/' : ' ' : r -> empty : replaceUnderlines r l

q : r -> if q `elem` "()/" then replaceUnderlines r l

else cons (text [q]) $ replaceUnderlines r l

where

cons :: Doc -> [Doc] -> [Doc]

cons d r = case r of

[] -> [d]

h : t -> let

b = '|'

hs = show h

ds = show d

hhs = head hs

lds = last ds

in if null hs || null ds then (d <> h) : t else

if hhs == b && lds == '('

|| last ds == b && hhs == ')' then (d <+> h) : t

else (d <> h) : t

-- end of term printing

printClassrel :: Classrel -> Doc

printClassrel = vcat . map ( \ (t, cl) -> case cl of

Nothing -> empty

Just x -> text axclassS <+> printClass t <+> text "<" <+>

printSort x) . Map.toList

printMonArities :: String -> Arities -> Doc

printMonArities tn = vcat . map ( \ (t, cl) ->

vcat $ map (printThMorp tn t) cl) . Map.toList

printThMorp :: String -> TName -> (IsaClass, [(Typ, Sort)]) -> Doc

printThMorp tn t xs = case xs of

(IsaClass "Monad", _) ->

if (isSuffixOf "_mh" tn) || (isSuffixOf "_mhc" tn)

then printMInstance tn t

else error "IsaPrint, printInstance: monads not supported"

_ -> empty

printArities :: String -> Arities -> Doc

printArities tn = vcat . map ( \ (t, cl) ->

vcat $ map (printInstance tn t) cl) . Map.toList

printInstance :: String -> TName -> (IsaClass, [(Typ, Sort)]) -> Doc

printInstance _ t xs = case xs of

(IsaClass "Monad", _) -> empty

_ -> printNInstance t xs

printMInstance :: String -> TName -> Doc

printMInstance tn t = let nM = text (t ++ "_tm")

nM2 = text (t ++ "_tm2")

in prnThymorph nM "MonadType" tn t [("MonadType.M","'a")] []

$+$ text "t_instantiate MonadOps mapping" <+> nM

$+$ text "renames:" <+>

brackMapList (\x -> t ++ "_" ++ x)

[("MonadOpEta.eta","eta"),("MonadOpBind.bind","bind")]

$+$ text "without_syntax"

$++$ text "defs "

$+$ text (t ++ "_eta_def:") <+> doubleQuotes

(text (t ++ "_eta") <+> text "==" <+> text ("return_" ++ t))

$+$ text (t ++ "_bind_def:") <+> doubleQuotes

(text (t ++ "_bind") <+> text "==" <+> text ("mbind_" ++ t))

$++$ lunitLemma t

$+$ runitLemma t

$+$ assocLemma t

$+$ etaInjLemma t

$++$ prnThymorph nM2 "MonadAxms" tn t [("MonadType.M","'a")]

[("MonadOpEta.eta",(t ++ "_eta")),("MonadOpBind.bind",(t ++ "_bind"))]

$+$ text "t_instantiate Monad mapping" <+> nM2

$+$ text "renames:" <+>

brackMapList (\x -> t ++ "_" ++ x)

[("Monad.kapp","kapp"),

("Monad.lift","lift"),

("Monad.lift","lift"),

("Monad.mapF","mapF"),

("Monad.bind'","bind'"),

("Monad.joinM","joinM"),

("Monad.kapp2","kapp2"),

("Monad.kapp3","kapp3"),

("Monad.lift2","lift2"),

("Monad.lift3","lift3")]

$+$ text "without_syntax"

$++$ text " "

where

lunitLemma w = text "lemma" <+> text (w ++ "_lunit:")

<+> doubleQuotes (text (w ++ "_bind")

<+> parens (text (w ++ "_eta x"))

<+> parens (text $ "t::'a => 'b " ++ w)

<+> text "=" <+> text "t x")

$+$ text "sorry "

runitLemma w = text "lemma" <+> text (w ++ "_runit:")

<+> doubleQuotes (text (w ++ "_bind")

<+> parens (text $ "t::'a " ++ w) <+> text (w ++ "_eta")

<+> text "=" <+> text "t")

$+$ text "sorry "

assocLemma w = text "lemma" <+> text (w ++ "_assoc:")

<+> doubleQuotes ((text $ w ++ "_bind")

<+> parens ((text $ w ++ "_bind")

<+> parens (text $ "s::'a " ++ w) <+> text "t") <+> text "u"

<+> text "=" <+> text (w ++ "_bind s")

<+> parens ((text "%x.") <+>

(text $ w ++ "_bind") <+> text "(t x) u"))

$+$ text "sorry "

etaInjLemma w = text "lemma" <+> text (w ++ "_eta_inj:")

<+> doubleQuotes (parens (text $ w ++ "_eta::'a => 'a " ++ w)

<+> text "x"

<+> text "=" <+> (text $ w ++ "_eta y")

<+> text "==>" <+> text "x = y")

$+$ text "sorry "

prnThymorph :: Doc -> String -> String -> TName ->

[(String,String)] -> [(String,String)] -> Doc

prnThymorph nm xn tn t ts ws = let tArrow = text ("-" ++ "->")

in (text "thymorph" <+> nm <+> colon <+>

text xn <+> tArrow <+> text tn)

$+$ text " maps" <+> (brackets $

hcat [parens $ (doubleQuotes (text b <+> text a) <+>

text "|->" <+> doubleQuotes (text b <+> (text $ tn ++ "." ++ t))) |

(a,b) <- ts])

$+$ brackMapList (\j -> tn ++ "." ++ j) ws

brackMapList :: (String -> String) -> [(String,String)] -> Doc

brackMapList f ws = (brackets $

hsep $ punctuate comma [parens $ (doubleQuotes (text a)

<+> text "|->" <+> doubleQuotes (text $ f b)) | (a,b) <- ws])

printNInstance :: TName -> (IsaClass, [(Typ, Sort)]) -> Doc

printNInstance t (IsaClass x, xs) = let

ys = map snd xs

in (case t of

"tr" -> printNInst "lift" [holType]

"dInt" -> printNInst "lift" [holType]

_ -> printNInst t ys)

<+> (text x)

$+$ text (if x == "Eq" then "sorry"

else "by intro_classes")

printNInst :: TName -> [Sort] -> Doc

printNInst t xs = text instanceS <+> text t <>

doubleColon <> (case xs of

[] -> empty

_ -> parens $ hsep $ punctuate comma $

map (doubleQuotes . printSort) xs)

-- filter out types that are given in the domain table

printTypeDecls :: DomainTab -> Arities -> Doc

printTypeDecls odt ars =

let dt = Map.fromList $ map (\ (t, _) -> (typeId t, []))

$ concat odt

in vcat $ map printTycon $ Map.toList

$ Map.difference ars dt

printTycon :: (TName, [(IsaClass, [(Typ, Sort)])]) -> Doc

printTycon (t, arity') =

let arity = if null arity' then

error "IsaPrint.printTycon"

else length (snd $ head arity') in

if t == "tr" || t == "dInt" || t == "bool" || t == "int"

then empty else

text typedeclS <+>

(if arity > 0

then parens $ hsep $ punctuate comma

$ map (text . ("'a"++) . show) [1..arity]

else empty) <+> text t

-- | show alternative syntax (computed by comorphisms)

printAlt :: VName -> Doc

printAlt (VName _ altV) = case altV of

Nothing -> empty

Just (AltSyntax s is i) -> parens $ doubleQuotes (text s)

<+> if null is then empty else text (show is) <+>

if i == maxPrio then empty else text (show i)

instance Pretty Sign where

pretty = printSign

-- | a dummy constant table with wrong types

constructors :: DomainTab -> ConstTab

constructors = Map.fromList . map (\ v -> (v, noType))

. concatMap (map fst . snd) . concat

printMonSign :: Sign -> Doc

printMonSign sig = let ars = arities $ tsig sig

in

printMonArities (theoryName sig) ars

printSign :: Sign -> Doc

printSign sig = let dt = domainTab sig

ars = arities $ tsig sig

in

printAbbrs (abbrs $ tsig sig) $++$

printTypeDecls dt ars $++$

printClassrel (classrel $ tsig sig) $++$

printDomainDefs dt $++$

printConstTab (Map.difference (constTab sig)

$ constructors dt) $++$

(if showLemmas sig then showCaseLemmata (domainTab sig) else empty) $++$

printArities (theoryName sig) ars

where

printAbbrs tab = if Map.null tab then empty else text typesS

$+$ vcat (map printAbbr $ Map.toList tab)

printAbbr (n, (vs, t)) = (case vs of

[] -> empty

[x] -> text ("\'" ++ x)

_ -> parens $ hsep $ punctuate comma $

map (\x -> text $ "\'" ++ x) vs)

<+> (text $ n) <+> equals <+> (doubleQuotes $ printType t)

printConstTab tab = if Map.null tab then empty else text constsS

$+$ vcat (map printConst $ Map.toList tab)

printConst (vn, t) = text (new vn) <+> doubleColon <+>

doubleQuotes (printType t) <+> printAlt vn

isDomain = case baseSig sig of

HOLCF_thy -> True

HsHOLCF_thy -> True

MHsHOLCF_thy -> True

_ -> False

printDomainDefs dtDefs = vcat $ map printDomainDef dtDefs

printDomainDef dts = if null dts then empty else

text (if isDomain then domainS else datatypeS)

<+> and_docs (map printDomain dts)

printDomain (t, ops) =

printTyp (if isDomain then Quoted else Null) t <+> equals <+>

hsep (bar $ map printDOp ops)

printDOp (vn, args) = let opname = new vn in

text opname <+> hsep (map (printDOpArg opname)

$ zip args [1 :: Int .. ])

<+> printAlt vn

printDOpArg o (a, i) = let

d = case a of

TFree _ _ -> printTyp Null a

_ -> doubleQuotes $ printTyp Null a

in if isDomain then

parens $ text "lazy" <+>

text (o ++ "_" ++ show i) <> doubleColon <> d

else d

showCaseLemmata dtDefs = text (concat $ map showCaseLemmata1 dtDefs)

showCaseLemmata1 dts = concat $ map showCaseLemma dts

showCaseLemma (_, []) = ""

showCaseLemma (tyCons, (c:cons)) =

let cs = "case caseVar of" ++ sp

sc b = showCons b c ++ (concat $ map ((" | " ++)

. (showCons b)) cons)

clSome = sc True

cl = sc False

showCons b ((VName {new=cName}), args) =

let pat = cName ++ (concat $ map ((sp ++) . showArg) args)

++ sp ++ "=>" ++ sp

term = showCaseTerm cName args

in

if b then pat ++ "Some" ++ sp ++ lb ++ term ++ rb ++ "\n"

else pat ++ term ++ "\n"

showCaseTerm name args = if null name then sa

else [toLower (head name)] ++ sa

where sa = (concat $ map ((sp ++) . showArg) args)

showArg (TFree [] _) = "varName"

showArg (TFree (n:ns) _) = [toLower n] ++ ns

showArg (TVar v s) = showArg (TFree (unindexed v) s)

showArg (Type [] _ _) = "varName"

showArg (Type m@(n:ns) _ s) =

if m == "typeAppl" || m == "fun" || m == "*"

then concat $ map showArg s

else [toLower n] ++ ns

showName (TFree v _) = v

showName (TVar v _) = unindexed v

showName (Type n _ _) = n

proof = "apply (case_tac caseVar)\napply (auto)\ndone\n"

in

"lemma" ++ sp ++ "case_" ++ showName tyCons ++ "_SomeProm" ++ sp

++ "[simp]:\"" ++ sp ++ lb ++ cs ++ clSome ++ rb ++ sp

++ "=\n" ++ "Some" ++ sp ++ lb ++ cs ++ cl ++ rb ++ "\"\n"

++ proof

instance Pretty Sentence where

pretty = printSentence

sp :: String

sp = " "

rb :: String

rb = ")"

lb :: String

lb = "("