{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Rules.Record where
import Prelude hiding (null)
import Control.Monad
import Data.Maybe
import Agda.Interaction.Options
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern
import Agda.Syntax.Position
import qualified Agda.Syntax.Info as Info
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Primitive
import Agda.TypeChecking.Rewriting.Confluence
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Positivity.Occurrence
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Polarity
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.CompiledClause (hasProjectionPatterns)
import Agda.TypeChecking.CompiledClause.Compile
import Agda.TypeChecking.Rules.Data ( getGeneralizedParameters, bindGeneralizedParameters, bindParameters, fitsIn, forceSort,
defineCompData, defineTranspOrHCompForFields )
import Agda.TypeChecking.Rules.Term ( isType_ )
import {-# SOURCE #-} Agda.TypeChecking.Rules.Decl (checkDecl)
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Utils.POMonoid
import qualified Agda.Utils.Pretty as P
import Agda.Utils.Size
import Agda.Utils.Impossible
checkRecDef
:: A.DefInfo
-> QName
-> UniverseCheck
-> Maybe (Ranged Induction)
-> Maybe HasEta
-> Maybe QName
-> A.DataDefParams
-> A.Expr
-> [A.Field]
-> TCM ()
checkRecDef i name uc ind eta con (A.DataDefParams gpars ps) contel fields =
traceCall (CheckRecDef (getRange name) name ps fields) $ do
reportSDoc "tc.rec" 10 $ vcat
[ "checking record def" <+> prettyTCM name
, nest 2 $ "ps =" <+> prettyList (map prettyA ps)
, nest 2 $ "contel =" <+> prettyA contel
, nest 2 $ "fields =" <+> prettyA (map Constr fields)
]
def <- instantiateDef =<< getConstInfo name
t <- instantiateFull $ defType def
let npars =
case theDef def of
DataOrRecSig n -> n
_ -> __IMPOSSIBLE__
parNames <- getGeneralizedParameters gpars name
bindGeneralizedParameters parNames t $ \ gtel t0 ->
bindParameters (npars - length parNames) ps t0 $ \ ptel t0 -> do
let tel = abstract gtel ptel
reportSDoc "tc.rec" 15 $ "checking fields"
contype <- workOnTypes $ instantiateFull =<< isType_ contel
reportSDoc "tc.rec" 20 $ vcat
[ "contype = " <+> prettyTCM contype ]
let TelV ftel _ = telView' contype
TelV idxTel s <- telView t0
unless (null idxTel) $ typeError $ ShouldBeASort t0
s <- forceSort s
reportSDoc "tc.rec" 20 $ do
gamma <- getContextTelescope
"gamma = " <+> inTopContext (prettyTCM gamma)
rect <- El s . Def name . map Apply <$> getContextArgs
let contype = telePi_ ftel (raise (size ftel) rect)
(hasNamedCon, conName, conInfo) <- case con of
Just c -> return (True, c, i)
Nothing -> do
m <- killRange <$> currentModule
c <- qualify m <$> freshName_ ("recCon-NOT-PRINTED" :: String)
return (False, c, i)
reportSDoc "tc.rec" 15 $ "adding record type to signature"
etaenabled <- etaEnabled
let getName :: A.Declaration -> [Dom QName]
getName (A.Field _ x arg) = [x <$ domFromArg arg]
getName (A.ScopedDecl _ [f]) = getName f
getName _ = []
setTactic dom f = f { domTactic = domTactic dom }
fs = zipWith setTactic (telToList ftel) $ concatMap getName fields
indCo = rangedThing <$> ind
conInduction = fromMaybe Inductive indCo
haveEta = maybe (Inferred NoEta) Specified eta
con = ConHead conName conInduction $ map argFromDom fs
recordRelevance
| eta == Just NoEta = Relevant
| conInduction == CoInductive = Relevant
| otherwise = minimum $ Irrelevant : (map getRelevance $ telToList ftel)
when (conInduction == CoInductive && theEtaEquality haveEta == YesEta) $ do
typeError . GenericDocError =<< do
sep [ "Agda doesn't like coinductive records with eta-equality."
, "If you must, use pragma"
, "{-# ETA" <+> prettyTCM name <+> "#-}"
]
reportSDoc "tc.rec" 30 $ "record constructor is " <+> prettyTCM con
let npars = size tel
telh = fmap hideAndRelParams tel
escapeContext __IMPOSSIBLE__ npars $ do
addConstant name $
defaultDefn defaultArgInfo name t $
Record
{ recPars = npars
, recClause = Nothing
, recConHead = con
, recNamedCon = hasNamedCon
, recFields = fs
, recTel = telh `abstract` ftel
, recAbstr = Info.defAbstract i
, recEtaEquality' = haveEta
, recInduction = indCo
, recMutual = Nothing
, recComp = emptyCompKit
}
addConstant conName $
defaultDefn defaultArgInfo conName (telh `abstract` contype) $
Constructor
{ conPars = npars
, conArity = size fs
, conSrcCon = con
, conData = name
, conAbstr = Info.defAbstract conInfo
, conInd = conInduction
, conComp = emptyCompKit
, conProj = Nothing
, conForced = []
, conErased = Nothing
}
case Info.defInstance i of
InstanceDef r -> setCurrentRange r $ do
addTypedInstance conName contype
NotInstanceDef -> pure ()
_ <- fitsIn uc [] contype s
let info = setRelevance recordRelevance defaultArgInfo
addRecordVar =
addRecordNameContext (setArgInfo info $ defaultDom rect)
let m = qnameToMName name
modifyContextInfo hideOrKeepInstance $ addRecordVar $ do
reportSDoc "tc.rec.def" 10 $ sep
[ "record section:"
, nest 2 $ sep
[ prettyTCM m <+> (inTopContext . prettyTCM =<< getContextTelescope)
, fsep $ punctuate comma $ map (return . P.pretty . map argFromDom . getName) fields
]
]
reportSDoc "tc.rec.def" 15 $ nest 2 $ vcat
[ "field tel =" <+> escapeContext __IMPOSSIBLE__ 1 (prettyTCM ftel)
]
addSection m
modifyContextInfo hideOrKeepInstance $ addRecordVar $ do
withCurrentModule m $ do
tel' <- getContextTelescope
setModuleCheckpoint m
checkRecordProjections m name hasNamedCon con tel' (raise 1 ftel) fields
escapeContext __IMPOSSIBLE__ npars $ do
addCompositionForRecord name con tel (map argFromDom fs) ftel rect
whenM (optConfluenceCheck <$> pragmaOptions) $ forM_ fs $ \f -> do
cls <- defClauses <$> getConstInfo (unDom f)
forM (zip cls [0..]) $ \(cl,i) ->
checkConfluenceOfClause (unDom f) i cl
return ()
addCompositionForRecord
:: QName
-> ConHead
-> Telescope
-> [Arg QName]
-> Telescope
-> Type
-> TCM ()
addCompositionForRecord name con tel fs ftel rect = do
cxt <- getContextTelescope
inTopContext $ do
if null fs then do
kit <- defineCompData name con (abstract cxt tel) [] ftel rect []
modifySignature $ updateDefinition (conName con) $ updateTheDef $ \case
r@Constructor{} -> r { conComp = kit, conProj = Just [] }
_ -> __IMPOSSIBLE__
else do
kit <- ifM (return (any isIrrelevant fs)
`and2M` do not . optIrrelevantProjections <$> pragmaOptions)
(return emptyCompKit)
(defineCompKitR name (abstract cxt tel) ftel fs rect)
modifySignature $ updateDefinition name $ updateTheDef $ \case
r@Record{} -> r { recComp = kit }
_ -> __IMPOSSIBLE__
defineCompKitR ::
QName
-> Telescope
-> Telescope
-> [Arg QName]
-> Type
-> TCM CompKit
defineCompKitR name params fsT fns rect = do
required <- mapM getTerm'
[ builtinInterval
, builtinIZero
, builtinIOne
, builtinIMin
, builtinIMax
, builtinINeg
, builtinPOr
, builtinItIsOne
]
reportSDoc "tc.rec.cxt" 30 $ prettyTCM params
reportSDoc "tc.rec.cxt" 30 $ prettyTCM fsT
reportSDoc "tc.rec.cxt" 30 $ pretty rect
if not $ all isJust required then return $ emptyCompKit else do
transp <- whenDefined [builtinTrans] (defineTranspOrHCompR DoTransp name params fsT fns rect)
hcomp <- whenDefined [builtinTrans,builtinHComp] (defineTranspOrHCompR DoHComp name params fsT fns rect)
return $ CompKit
{ nameOfTransp = transp
, nameOfHComp = hcomp
}
where
whenDefined xs m = do
xs <- mapM getTerm' xs
if all isJust xs then m else return Nothing
defineTranspOrHCompR ::
TranspOrHComp
-> QName
-> Telescope
-> Telescope
-> [Arg QName]
-> Type
-> TCM (Maybe QName)
defineTranspOrHCompR cmd name params fsT fns rect = do
let project = (\ t fn -> t `applyE` [Proj ProjSystem fn])
stuff <- fmap fst <$> defineTranspOrHCompForFields cmd Nothing project name params fsT fns rect
caseMaybe stuff (return Nothing) $ \ (theName, gamma, rtype, clause_types, bodies) -> do
c' <- do
io <- primIOne
Just io_name <- getBuiltinName' builtinIOne
one <- primItIsOne
tInterval <- elInf primInterval
let
(ix,rhs) =
case cmd of
DoTransp -> (1,Var 0 [])
DoHComp -> (2,Var 1 [] `apply` [argN io, setRelevance Irrelevant $ argN one])
p = ConP (ConHead io_name Inductive [])
(noConPatternInfo { conPType = Just (Arg defaultArgInfo tInterval)
, conPFallThrough = True })
[]
s = singletonS ix p
pats :: [NamedArg DeBruijnPattern]
pats = s `applySubst` teleNamedArgs gamma
t :: Type
t = s `applyPatSubst` rtype
gamma' :: Telescope
gamma' = unflattenTel (ns0 ++ ns1) $ s `applyPatSubst` (g0 ++ g1)
where
(g0,_:g1) = splitAt (size gamma - 1 - ix) $ flattenTel gamma
(ns0,_:ns1) = splitAt (size gamma - 1 - ix) $ teleNames gamma
c = Clause { clauseTel = gamma'
, clauseType = Just $ argN t
, namedClausePats = pats
, clauseFullRange = noRange
, clauseLHSRange = noRange
, clauseCatchall = False
, clauseBody = Just $ rhs
, clauseRecursive = Just False
, clauseUnreachable = Just False
, clauseEllipsis = NoEllipsis
}
reportSDoc "trans.rec.face" 17 $ text $ show c
return c
cs <- flip mapM (zip3 fns clause_types bodies) $ \ (fname, clause_ty, body) -> do
let
pats = teleNamedArgs gamma ++ [defaultNamedArg $ ProjP ProjSystem $ unArg fname]
c = Clause { clauseTel = gamma
, clauseType = Just $ argN (unDom clause_ty)
, namedClausePats = pats
, clauseFullRange = noRange
, clauseLHSRange = noRange
, clauseCatchall = False
, clauseBody = Just body
, clauseRecursive = Nothing
, clauseUnreachable = Just False
, clauseEllipsis = NoEllipsis
}
reportSDoc "trans.rec" 17 $ text $ show c
reportSDoc "trans.rec" 16 $ text "type =" <+> text (show (clauseType c))
reportSDoc "trans.rec" 15 $ prettyTCM $ abstract gamma (unDom clause_ty)
reportSDoc "trans.rec" 10 $ text "body =" <+> prettyTCM (abstract gamma body)
return c
addClauses theName $ c' : cs
reportSDoc "trans.rec" 15 $ text $ "compiling clauses for " ++ show theName
(mst, _, cc) <- inTopContext (compileClauses Nothing cs)
whenJust mst $ setSplitTree theName
setCompiledClauses theName cc
reportSDoc "trans.rec" 15 $ text $ "compiled"
return $ Just theName
checkRecordProjections ::
ModuleName -> QName -> Bool -> ConHead -> Telescope -> Telescope ->
[A.Declaration] -> TCM ()
checkRecordProjections m r hasNamedCon con tel ftel fs = do
checkProjs EmptyTel ftel fs
where
checkProjs :: Telescope -> Telescope -> [A.Declaration] -> TCM ()
checkProjs _ _ [] = return ()
checkProjs ftel1 ftel2 (A.ScopedDecl scope fs' : fs) =
setScope scope >> checkProjs ftel1 ftel2 (fs' ++ fs)
checkProjs ftel1 (ExtendTel (dom@Dom{domInfo = ai,unDom = t}) ftel2) (A.Field info x _ : fs) =
traceCall (CheckProjection (getRange info) x t) $ do
reportSDoc "tc.rec.proj" 5 $ sep
[ "checking projection" <+> prettyTCM x
, nest 2 $ vcat
[ "top =" <+> (inTopContext . prettyTCM =<< getContextTelescope)
, "tel =" <+> (inTopContext . prettyTCM $ tel)
, "ftel1 =" <+> prettyTCM ftel1
, "t =" <+> prettyTCM t
, "ftel2 =" <+> addContext ftel1 (underAbstraction_ ftel2 prettyTCM)
, "abstr =" <+> (text . show) (Info.defAbstract info)
, "quant =" <+> (text . show) (getQuantity ai)
, "coh =" <+> (text . show) (getCohesion ai)
]
]
if hasLeftAdjoint (getCohesion ai)
then unless (getCohesion ai == Continuous)
__IMPOSSIBLE__
else genericError $ "Cannot have record fields with modality " ++ show (getCohesion ai)
let finalt = telePi (replaceEmptyName "r" tel) t
projname = qualify m $ qnameName x
projcall o = Var 0 [Proj o projname]
rel = getRelevance ai
recurse = checkProjs (abstract ftel1 $ ExtendTel dom
$ Abs (nameToArgName $ qnameName projname) EmptyTel)
(ftel2 `absApp` projcall ProjSystem) fs
reportSDoc "tc.rec.proj" 25 $ nest 2 $ "finalt=" <+> do
inTopContext $ prettyTCM finalt
do
reportSDoc "tc.rec.proj" 10 $ sep
[ "adding projection"
, nest 2 $ prettyTCM projname <+> ":" <+> inTopContext (prettyTCM finalt)
]
let bodyMod = case rel of
Relevant -> id
NonStrict -> id
Irrelevant -> dontCare
let
telList = telToList tel
(ptelList,[rt]) = splitAt (size tel - 1) telList
ptel = telFromList ptelList
cpo = if hasNamedCon then PatOCon else PatORec
cpi = ConPatternInfo { conPInfo = PatternInfo cpo []
, conPRecord = True
, conPFallThrough = False
, conPType = Just $ argFromDom $ fmap snd rt
, conPLazy = True }
conp = defaultArg $ ConP con cpi $
[ Arg ai' $ unnamed $ varP ("x" :: String)
| Dom{domInfo = ai'} <- telToList ftel
]
body = Just $ bodyMod $ var (size ftel2)
cltel = ptel `abstract` ftel
clause = Clause { clauseLHSRange = getRange info
, clauseFullRange = getRange info
, clauseTel = killRange cltel
, namedClausePats = [Named Nothing <$> numberPatVars __IMPOSSIBLE__ (idP $ size ftel) conp]
, clauseBody = body
, clauseType = Just $ Arg ai t
, clauseCatchall = False
, clauseRecursive = Just False
, clauseUnreachable = Just False
, clauseEllipsis = NoEllipsis
}
let projection = Projection
{ projProper = Just r
, projOrig = projname
, projFromType = defaultArg r
, projIndex = size tel
, projLams = ProjLams $ map (argFromDom . fmap fst) telList
}
reportSDoc "tc.rec.proj" 80 $ sep
[ "adding projection"
, nest 2 $ prettyTCM projname <+> text (show clause)
]
reportSDoc "tc.rec.proj" 70 $ sep
[ "adding projection"
, nest 2 $ prettyTCM projname <+> text (show (clausePats clause)) <+> "=" <+>
inTopContext (addContext ftel (maybe "_|_" prettyTCM (clauseBody clause)))
]
reportSDoc "tc.rec.proj" 10 $ sep
[ "adding projection"
, nest 2 $ prettyTCM (QNamed projname clause)
]
(mst, _, cc) <- compileClauses Nothing [clause]
reportSDoc "tc.cc" 60 $ do
sep [ "compiled clauses of " <+> prettyTCM projname
, nest 2 $ text (show cc)
]
escapeContext __IMPOSSIBLE__ (size tel) $ do
addConstant projname $
(defaultDefn ai projname (killRange finalt)
emptyFunction
{ funClauses = [clause]
, funCompiled = Just cc
, funSplitTree = mst
, funProjection = Just projection
, funMutual = Just []
, funTerminates = Just True
})
{ defArgOccurrences = [StrictPos]
, defCopatternLHS = hasProjectionPatterns cc
}
computePolarity [projname]
case Info.defInstance info of
InstanceDef _r -> addTypedInstance projname t
NotInstanceDef -> pure ()
recurse
checkProjs ftel1 ftel2 (d : fs) = do
checkDecl d
checkProjs ftel1 ftel2 fs