module Agda.TypeChecking.Rules.Def where
import Prelude hiding (mapM)
import Control.Arrow ((***))
import Control.Applicative
import Control.Monad.State hiding (forM, mapM)
import Control.Monad.Reader hiding (forM, mapM)
import Data.Function
import Data.List hiding (sort)
import Data.Maybe
import Data.Traversable
import qualified Data.Set as Set
import Agda.Syntax.Common
import qualified Agda.Syntax.Concrete as C
import Agda.Syntax.Concrete (exprFieldA)
import Agda.Syntax.Position
import qualified Agda.Syntax.Abstract as A
import qualified Agda.Syntax.Abstract.Views as A
import Agda.Syntax.Internal as I
import Agda.Syntax.Internal.Pattern as I
import qualified Agda.Syntax.Info as Info
import Agda.Syntax.Fixity
import Agda.Syntax.Translation.InternalToAbstract
import Agda.Syntax.Info
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import qualified Agda.TypeChecking.Monad.Benchmark as Bench
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Patterns.Abstract (expandPatternSynonyms)
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Free
import Agda.TypeChecking.CheckInternal (checkType)
import Agda.TypeChecking.With
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Injectivity
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.SizedTypes.Solve
import Agda.TypeChecking.RecordPatterns
import Agda.TypeChecking.CompiledClause (CompiledClauses(..))
import Agda.TypeChecking.CompiledClause.Compile
import Agda.TypeChecking.Primitive hiding (Nat)
import Agda.TypeChecking.Rules.Term ( checkExpr, inferExpr, inferExprForWith, checkDontExpandLast, checkTelescope )
import Agda.TypeChecking.Rules.LHS ( checkLeftHandSide, LHSResult(..), bindAsPatterns )
import Agda.TypeChecking.Rules.LHS.Problem ( AsBinding(..) )
import Agda.TypeChecking.Rules.Decl ( checkDecls )
import Agda.Utils.Except ( MonadError(catchError, throwError) )
import Agda.Utils.Lens
import Agda.Utils.Maybe ( whenNothing )
import Agda.Utils.Monad
import Agda.Utils.Permutation
import Agda.Utils.Size
import Agda.Utils.Functor
#include "undefined.h"
import Agda.Utils.Impossible
checkFunDef :: Delayed -> Info.DefInfo -> QName -> [A.Clause] -> TCM ()
checkFunDef delayed i name cs = do
t <- typeOfConst name
info <- flip setRelevance defaultArgInfo <$> relOfConst name
case isAlias cs t of
Just (e, mc, x) ->
traceCall (CheckFunDef (getRange i) (qnameName name) cs) $ do
whenM (isFrozen x) $ unfreezeMeta x
checkAlias t info delayed i name e mc
_ -> checkFunDef' t info delayed Nothing Nothing i name cs
ismacro <- isMacro . theDef <$> getConstInfo name
when (ismacro || Info.defMacro i == MacroDef) $ checkMacroType t
checkMacroType :: Type -> TCM ()
checkMacroType t = do
t' <- normalise t
TelV tel tr <- telView t'
let telList = telToList tel
resType = abstract (telFromList (drop (length telList 1) telList)) tr
expectedType <- el primAgdaTerm --> el (primAgdaTCM <#> primLevelZero <@> primUnit)
equalType resType expectedType
`catchError` \ _ -> typeError . GenericDocError =<< sep [ text "Result type of a macro must be"
, nest 2 $ prettyTCM expectedType ]
isAlias :: [A.Clause] -> Type -> Maybe (A.Expr, Maybe C.Expr, MetaId)
isAlias cs t =
case trivialClause cs of
Just (e, mc) | Just x <- isMeta (ignoreSharing $ unEl t) -> Just (e, mc, x)
_ -> Nothing
where
isMeta (MetaV x _) = Just x
isMeta _ = Nothing
trivialClause [A.Clause (A.LHS i (A.LHSHead f []) []) _ (A.RHS e mc) [] _] = Just (e, mc)
trivialClause _ = Nothing
checkAlias :: Type -> ArgInfo -> Delayed -> Info.DefInfo -> QName -> A.Expr -> Maybe C.Expr -> TCM ()
checkAlias t' ai delayed i name e mc = atClause name 0 (A.RHS e mc) $ do
reportSDoc "tc.def.alias" 10 $ text "checkAlias" <+> vcat
[ text (show name) <+> colon <+> prettyTCM t'
, text (show name) <+> equals <+> prettyTCM e
]
v <- applyRelevanceToContext (getRelevance ai) $ checkDontExpandLast e t'
let t = t'
reportSDoc "tc.def.alias" 20 $ text "checkAlias: finished checking"
solveSizeConstraints DontDefaultToInfty
v <- instantiateFull v
let bodyMod = case getRelevance ai of
Irrelevant -> dontCare
_ -> id
addConstant name $ defaultDefn ai name t
$ set funMacro (Info.defMacro i == MacroDef) $
emptyFunction
{ funClauses = [ Clause
{ clauseRange = getRange i
, clauseTel = EmptyTel
, namedClausePats = []
, clauseBody = Just $ bodyMod v
, clauseType = Just $ Arg ai t
, clauseCatchall = False
} ]
, funCompiled = Just $ Done [] $ bodyMod v
, funDelayed = delayed
, funAbstr = Info.defAbstract i
}
reportSDoc "tc.def.alias" 20 $ text "checkAlias: leaving"
checkFunDef' :: Type
-> ArgInfo
-> Delayed
-> Maybe ExtLamInfo
-> Maybe QName
-> Info.DefInfo
-> QName
-> [A.Clause]
-> TCM ()
checkFunDef' t ai delayed extlam with i name cs =
checkFunDefS t ai delayed extlam with i name Nothing cs
checkFunDefS :: Type
-> ArgInfo
-> Delayed
-> Maybe ExtLamInfo
-> Maybe QName
-> Info.DefInfo
-> QName
-> Maybe Substitution
-> [A.Clause]
-> TCM ()
checkFunDefS t ai delayed extlam with i name withSub cs =
traceCall (CheckFunDef (getRange i) (qnameName name) cs) $ do
reportSDoc "tc.def.fun" 10 $
sep [ text "checking body of" <+> prettyTCM name
, nest 2 $ text ":" <+> prettyTCM t
, nest 2 $ text "full type:" <+> (prettyTCM . defType =<< getConstInfo name)
]
reportSDoc "tc.def.fun" 70 $
sep $ [ text "clauses:" ] ++ map (nest 2 . text . show . A.deepUnscope) cs
cs <- return $ map A.lhsToSpine cs
reportSDoc "tc.def.fun" 70 $
sep $ [ text "spine clauses:" ] ++ map (nest 2 . text . show . A.deepUnscope) cs
cs <- traceCall NoHighlighting $ do
forM (zip cs [0..]) $ \ (c, clauseNo) -> do
atClause name clauseNo (A.clauseRHS c) $ do
c <- applyRelevanceToContext (argInfoRelevance ai) $ do
checkClause t withSub c
whenNothing extlam $ solveSizeConstraints DontDefaultToInfty
inTopContext $ addClauses name [c]
return c
reportSDoc "tc.def.fun" 70 $
sep $ [ text "checked clauses:" ] ++ map (nest 2 . text . show) cs
modifyFunClauses name (const [])
reportSDoc "tc.cc" 25 $ do
sep [ text "clauses before injectivity test"
, nest 2 $ prettyTCM $ map (QNamed name) cs
]
reportSDoc "tc.cc" 60 $ do
sep [ text "raw clauses: "
, nest 2 $ sep $ map (text . show . QNamed name) cs
]
cs <- instantiateFull cs
reportSLn "tc.inj.def" 20 $ "checkFunDef': checking injectivity..."
inv <- Bench.billTo [Bench.Injectivity] $
checkInjectivity name cs
reportSDoc "tc.cc" 15 $ do
sep [ text "clauses before compilation"
, nest 2 $ sep $ map (prettyTCM . QNamed name) cs
]
inTopContext $ addClauses name cs
fullType <- flip telePi t <$> getContextTelescope
cc <- Bench.billTo [Bench.Coverage] $
inTopContext $ compileClauses (Just (name, fullType)) cs
reportSDoc "tc.cc" 10 $ do
sep [ text "compiled clauses of" <+> prettyTCM name
, nest 2 $ text (show cc)
]
ismacro <- isMacro . theDef <$> getConstInfo name
inTopContext $ addConstant name =<< do
useTerPragma $ defaultDefn ai name fullType $
set funMacro (ismacro || Info.defMacro i == MacroDef) $
emptyFunction
{ funClauses = cs
, funCompiled = Just cc
, funDelayed = delayed
, funInv = inv
, funAbstr = Info.defAbstract i
, funExtLam = extlam
, funWith = with
, funCopatternLHS = isCopatternLHS cs
}
reportSDoc "tc.def.fun" 10 $ do
sep [ text "added " <+> prettyTCM name <+> text ":"
, nest 2 $ prettyTCM . defType =<< getConstInfo name
]
useTerPragma :: Definition -> TCM Definition
useTerPragma def@Defn{ defName = name, theDef = fun@Function{}} = do
tc <- asks envTerminationCheck
let terminates = case tc of
NonTerminating -> Just False
Terminating -> Just True
_ -> Nothing
reportSLn "tc.fundef" 30 $ unlines $
[ "funTerminates of " ++ show name ++ " set to " ++ show terminates
, " tc = " ++ show tc
]
return $ def { theDef = fun { funTerminates = terminates }}
useTerPragma def = return def
insertPatterns :: [A.Pattern] -> A.RHS -> A.RHS
insertPatterns pats (A.WithRHS aux es cs) = A.WithRHS aux es (map insertToClause cs)
where insertToClause (A.Clause (A.LHS i lhscore ps) dots rhs ds catchall)
= A.Clause (A.LHS i lhscore (pats ++ ps)) dots (insertPatterns pats rhs) ds catchall
insertPatterns pats (A.RewriteRHS qes rhs wh) = A.RewriteRHS qes (insertPatterns pats rhs) wh
insertPatterns pats rhs = rhs
data WithFunctionProblem
= NoWithFunction
| WithFunction
{ wfParentName :: QName
, wfName :: QName
, wfParentType :: Type
, wfBeforeTel :: Telescope
, wfAfterTel :: Telescope
, wfExprs :: [Term]
, wfExprTypes :: [EqualityView]
, wfRHSType :: Type
, wfParentPats :: [NamedArg DeBruijnPattern]
, wfParentParams :: Nat
, wfPermSplit :: Permutation
, wfPermParent :: Permutation
, wfPermFinal :: Permutation
, wfClauses :: [A.Clause]
}
checkClause
:: Type
-> Maybe Substitution
-> A.SpineClause
-> TCM Clause
checkClause t withSub c@(A.Clause (A.SpineLHS i x aps withPats) namedDots rhs0 wh catchall) = do
reportSDoc "tc.lhs.top" 30 $ text "Checking clause" $$ prettyA c
unless (null withPats) $
typeError $ UnexpectedWithPatterns withPats
traceCall (CheckClause t c) $ do
aps <- expandPatternSynonyms aps
cxtNames <- reverse . map (fst . unDom) <$> getContext
when (not $ null namedDots) $ reportSDoc "tc.lhs.top" 50 $
text "namedDots:" <+> vcat [ prettyTCM x <+> text "=" <+> prettyTCM v <+> text ":" <+> prettyTCM a | A.NamedDot x v a <- namedDots ]
bindAsPatterns [ AsB x v a | A.NamedDot x v a <- namedDots ] $
checkLeftHandSide (CheckPatternShadowing c) (Just x) aps t withSub $ \ lhsResult@(LHSResult npars delta ps trhs patSubst asb) -> do
t' <- case withSub of
Just{} -> return t
Nothing -> do
theta <- lookupSection (qnameModule x)
return $ abstract theta t
let rhs = updateRHS rhs0
updateRHS rhs@A.RHS{} = rhs
updateRHS rhs@A.AbsurdRHS{} = rhs
updateRHS (A.WithRHS q es cs) = A.WithRHS q es (map updateClause cs)
updateRHS (A.RewriteRHS qes rhs wh) = A.RewriteRHS qes (updateRHS rhs) wh
updateClause (A.Clause f dots rhs wh ca) = A.Clause f (applySubst patSubst dots) (updateRHS rhs) wh ca
(body, with) <- bindAsPatterns asb $ checkWhere wh $ checkRHS i x aps t' lhsResult rhs
inTopContext $ Bench.billTo [Bench.Typing, Bench.With] $ checkWithFunction cxtNames with
reportSDoc "tc.lhs.top" 10 $ escapeContext (size delta) $ vcat
[ text "Clause before translation:"
, nest 2 $ vcat
[ text "delta =" <+> prettyTCM delta
, text "ps =" <+> text (show ps)
, text "body =" <+> text (show body)
, text "body =" <+> maybe (text "_|_") prettyTCM body
]
]
rel <- asks envRelevance
let bodyMod body = case rel of
Irrelevant -> dontCare <$> body
_ -> body
return $
Clause { clauseRange = getRange i
, clauseTel = killRange delta
, namedClausePats = ps
, clauseBody = bodyMod body
, clauseType = Just trhs
, clauseCatchall = catchall
}
checkRHS
:: LHSInfo
-> QName
-> [NamedArg A.Pattern]
-> Type
-> LHSResult
-> A.RHS
-> TCM (Maybe Term, WithFunctionProblem)
checkRHS i x aps t lhsResult@(LHSResult _ delta ps trhs _ _asb) rhs0 = handleRHS rhs0
where
absurdPat = any (containsAbsurdPattern . namedArg) aps
handleRHS rhs =
case rhs of
A.RHS e _ -> Bench.billTo [Bench.Typing, Bench.CheckRHS] $ do
when absurdPat $ typeError $ AbsurdPatternRequiresNoRHS aps
v <- checkExpr e $ unArg trhs
return (Just v, NoWithFunction)
A.AbsurdRHS -> do
unless absurdPat $ typeError $ NoRHSRequiresAbsurdPattern aps
return (Nothing, NoWithFunction)
A.RewriteRHS [] rhs wh -> checkWhere wh $ handleRHS rhs
A.RewriteRHS ((qname,eq):qes) rhs wh -> do
st <- get
let recurse = do
st' <- get
let sameIP = (==) `on` (^.stInteractionPoints)
when (sameIP st st') $ put st
handleRHS $ A.RewriteRHS qes rhs wh
(proof, eqt) <- inferExpr eq
solveSizeConstraints DefaultToInfty
t' <- reduce =<< instantiateFull eqt
(eqt,rewriteType,rewriteFrom,rewriteTo) <- equalityView t' >>= \case
eqt@(EqualityType s _eq _level dom a b) -> return (eqt, El s (unArg dom), unArg a, unArg b)
OtherType{} -> typeError . GenericDocError =<< do
text "Cannot rewrite by equation of type" <+> prettyTCM t'
Con reflCon _ [] <- ignoreSharing <$> primRefl
let isReflProof = do
v <- reduce proof
case ignoreSharing v of
Con c _ [] | c == reflCon -> return True
_ -> return False
ifM isReflProof recurse $ do
let reflPat = A.ConP (ConPatInfo ConOCon patNoRange) (AmbQ [conName reflCon]) []
let isReflexive = tryConversion $ dontAssignMetas $
equalTerm rewriteType rewriteFrom rewriteTo
(pats, withExpr, withType) <- do
ifM isReflexive
(return ([ reflPat ], proof, OtherType t'))
(return ([ A.WildP patNoRange, reflPat ], proof, eqt))
let rhs' = insertPatterns pats rhs
(rhs'', outerWhere)
| null qes = (rhs', wh)
| otherwise = (A.RewriteRHS qes rhs' wh, [])
cs = [A.Clause (A.LHS i (A.LHSHead x (killRange aps)) pats) [] rhs'' outerWhere False]
checkWithRHS x qname t lhsResult [withExpr] [withType] cs
A.WithRHS aux es cs -> do
reportSDoc "tc.with.top" 15 $ vcat
[ text "TC.Rules.Def.checkclause reached A.WithRHS"
, sep $ prettyA aux : map (parens . prettyA) es
]
reportSDoc "tc.with.top" 20 $ do
nfv <- getCurrentModuleFreeVars
m <- currentModule
sep [ text "with function module:" <+>
prettyList (map prettyTCM $ mnameToList m)
, text $ "free variables: " ++ show nfv
]
(vs0, as) <- unzip <$> mapM inferExprForWith es
solveSizeConstraints DefaultToInfty
checkWithRHS x aux t lhsResult vs0 (map OtherType as) cs
checkWithRHS
:: QName
-> QName
-> Type
-> LHSResult
-> [Term]
-> [EqualityView]
-> [A.Clause]
-> TCM (Maybe Term, WithFunctionProblem)
checkWithRHS x aux t (LHSResult npars delta ps trhs _ _asb) vs0 as cs = Bench.billTo [Bench.Typing, Bench.With] $ do
let withArgs = withArguments vs0 as
perm = fromMaybe __IMPOSSIBLE__ $ dbPatPerm ps
(vs, as) <- normalise (vs0, as)
reportSDoc "tc.with.top" 25 $ escapeContext (size delta) $ vcat
[ text "delta =" <+> prettyTCM delta
]
reportSDoc "tc.with.top" 25 $ vcat
[ text "vs =" <+> prettyTCM vs
, text "as =" <+> prettyTCM as
, text "perm =" <+> text (show perm)
]
(delta1, delta2, perm', t', as, vs) <- return $
splitTelForWith delta (unArg trhs) as vs
let finalPerm = composeP perm' perm
reportSLn "tc.with.top" 75 $ "delta = " ++ show delta
reportSDoc "tc.with.top" 25 $ escapeContext (size delta) $ vcat
[ text "delta1 =" <+> prettyTCM delta1
, text "delta2 =" <+> addContext delta1 (prettyTCM delta2)
]
reportSDoc "tc.with.top" 25 $ vcat
[ text "perm' =" <+> text (show perm')
, text "fPerm =" <+> text (show finalPerm)
]
us <- getContextArgs
let n = size us
m = size delta
(us0, us1') = genericSplitAt (n m) us
(us1, us2) = genericSplitAt (size delta1) $ permute perm' us1'
v = Def aux $ map Apply $ us0 ++ us1 ++ map defaultArg withArgs ++ us2
addConstant aux =<< do
useTerPragma $ defaultDefn defaultArgInfo aux typeDontCare emptyFunction
reportSDoc "tc.with.top" 20 $
text " with arguments" <+> do escapeContext (size delta) $ addContext delta1 $ prettyList (map prettyTCM vs)
reportSDoc "tc.with.top" 20 $
text " types" <+> do escapeContext (size delta) $ addContext delta1 $ prettyList (map prettyTCM as)
reportSDoc "tc.with.top" 20 $
text "with function call" <+> prettyTCM v
reportSDoc "tc.with.top" 20 $
text " context" <+> (prettyTCM =<< getContextTelescope)
reportSDoc "tc.with.top" 20 $
text " delta" <+> do escapeContext (size delta) $ prettyTCM delta
reportSDoc "tc.with.top" 20 $
text " delta1" <+> do escapeContext (size delta) $ prettyTCM delta1
reportSDoc "tc.with.top" 20 $
text " delta2" <+> do escapeContext (size delta) $ addContext delta1 $ prettyTCM delta2
reportSDoc "tc.with.top" 20 $
text " body" <+> prettyTCM v
return (Just v, WithFunction x aux t delta1 delta2 vs as t' ps npars perm' perm finalPerm cs)
checkWithFunction :: [Name] -> WithFunctionProblem -> TCM ()
checkWithFunction _ NoWithFunction = return ()
checkWithFunction cxtNames (WithFunction f aux t delta1 delta2 vs as b qs npars perm' perm finalPerm cs) = do
let
withSub :: Substitution
withSub = liftS (size delta2) (wkS (countWithArgs as) idS) `composeS` renaming __IMPOSSIBLE__ (reverseP perm')
reportSDoc "tc.with.top" 10 $ vcat
[ text "checkWithFunction"
, nest 2 $ vcat
[ text "delta1 =" <+> prettyTCM delta1
, text "delta2 =" <+> addContext delta1 (prettyTCM delta2)
, text "t =" <+> prettyTCM t
, text "as =" <+> addContext delta1 (prettyTCM as)
, text "vs =" <+> do addContext delta1 $ prettyTCM vs
, text "b =" <+> do addContext delta1 $ addContext delta2 $ prettyTCM b
, text "qs =" <+> prettyList (map pretty qs)
, text "perm' =" <+> text (show perm')
, text "perm =" <+> text (show perm)
, text "fperm =" <+> text (show finalPerm)
, text "withSub=" <+> text (show withSub)
]
]
delta1 <- normalise delta1
(withFunType, n) <- withFunctionType delta1 vs as delta2 b
reportSDoc "tc.with.type" 10 $ sep [ text "with-function type:", nest 2 $ prettyTCM withFunType ]
reportSDoc "tc.with.type" 50 $ sep [ text "with-function type:", nest 2 $ pretty withFunType ]
setCurrentRange cs
(traceCall NoHighlighting $
checkType withFunType)
`catchError` \err -> case err of
TypeError s e -> do
put s
wt <- reify withFunType
enterClosure e $ do
traceCall (CheckWithFunctionType wt) . typeError
err -> throwError err
df <- makeGlobal =<< withDisplayForm f aux delta1 delta2 n qs perm' perm
reportSLn "tc.with.top" 20 "created with display form"
case dget df of
Display n ts dt ->
reportSDoc "tc.with.top" 20 $ text "Display" <+> fsep
[ text (show n)
, prettyList $ map prettyTCM ts
, prettyTCM dt
]
addConstant aux =<< do
useTerPragma $ (defaultDefn defaultArgInfo aux withFunType emptyFunction)
{ defDisplay = [df] }
reportSDoc "tc.with.top" 10 $ sep
[ text "added with function" <+> (prettyTCM aux) <+> text "of type"
, nest 2 $ prettyTCM withFunType
, nest 2 $ text "-|" <+> (prettyTCM =<< getContextTelescope)
]
reportSDoc "tc.with.top" 70 $ vcat
[ nest 2 $ text $ "raw with func. type = " ++ show withFunType
]
cs <- return $ map (A.lhsToSpine) cs
cs <- buildWithFunction cxtNames f aux t qs npars withSub finalPerm (size delta1) n cs
cs <- return $ map (A.spineToLhs) cs
checkFunDefS withFunType defaultArgInfo NotDelayed Nothing (Just f) info aux (Just withSub) cs
where
info = Info.mkDefInfo (nameConcrete $ qnameName aux) noFixity' PublicAccess ConcreteDef (getRange cs)
checkWhere
:: [A.Declaration]
-> TCM a
-> TCM a
checkWhere ds ret = loop ds
where
loop ds = case ds of
[] -> ret
[A.ScopedDecl scope ds] -> withScope_ scope $ loop ds
[A.Section _ m tel ds] -> newSection m tel $ do
local (\ e -> e { envCheckingWhere = True }) $ do
checkDecls ds
ret
_ -> __IMPOSSIBLE__
newSection :: ModuleName -> A.Telescope -> TCM a -> TCM a
newSection m tel cont = do
reportSDoc "tc.section" 10 $
text "checking section" <+> prettyTCM m <+> fsep (map prettyAs tel)
checkTelescope tel $ \ tel' -> do
reportSDoc "tc.section" 10 $
text "adding section:" <+> prettyTCM m <+> text (show (size tel'))
addSection m
reportSDoc "tc.section" 10 $ inTopContext $
nest 4 $ text "actual tele:" <+> do prettyTCM =<< lookupSection m
withCurrentModule m cont
containsAbsurdPattern :: A.Pattern -> Bool
containsAbsurdPattern p = case p of
A.AbsurdP _ -> True
A.VarP _ -> False
A.WildP _ -> False
A.DotP _ _ _ -> False
A.LitP _ -> False
A.AsP _ _ p -> containsAbsurdPattern p
A.ConP _ _ ps -> any (containsAbsurdPattern . namedArg) ps
A.RecP _ fs -> any (containsAbsurdPattern . (^. exprFieldA)) fs
A.ProjP{} -> False
A.DefP _ _ ps -> any (containsAbsurdPattern . namedArg) ps
A.PatternSynP _ _ _ -> __IMPOSSIBLE__
atClause :: QName -> Int -> A.RHS -> TCM a -> TCM a
atClause name i rhs = local $ \ e -> e { envClause = IPClause name i rhs }