{-# LANGUAGE CPP #-}
{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Rules.Record where
import Prelude hiding (null)
import Control.Applicative hiding (empty)
import Control.Monad
import Data.Maybe
import qualified Data.Set as Set
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.Syntax.Scope.Monad (freshAbstractQName)
import Agda.Syntax.Fixity
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Names
import Agda.TypeChecking.Primitive
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 qualified Agda.Utils.Pretty as P
import Agda.Utils.Size
#include "undefined.h"
import Agda.Utils.Impossible
checkRecDef
:: Info.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 -> [Arg QName]
getName (A.Field _ x arg) = [x <$ arg]
getName (A.ScopedDecl _ [f]) = getName f
getName _ = []
fs = concatMap getName fields
indCo = rangedThing <$> ind
conInduction = fromMaybe Inductive indCo
haveEta = maybe (Inferred NoEta) Specified eta
con = ConHead conName conInduction 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 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, Nothing)
, conForced = []
, conErased = []
}
when (Info.defInstance i == InstanceDef) $ do
addNamedInstance conName name
_ <- fitsIn uc [] contype s
let info = setRelevance recordRelevance defaultArgInfo
addRecordVar =
addRecordNameContext (setArgInfo info $ defaultDom rect)
let m = qnameToMName name
modifyContext (map 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 . getName) fields
]
]
reportSDoc "tc.rec.def" 15 $ nest 2 $ vcat
[ "field tel =" <+> escapeContext 1 (prettyTCM ftel)
]
addSection m
modifyContext (map hideOrKeepInstance) $ addRecordVar $ do
withCurrentModule m $ do
tel' <- getContextTelescope
setModuleCheckpoint m
checkRecordProjections m name hasNamedCon con tel' (raise 1 ftel) fields
escapeContext npars $ do
addCompositionForRecord name con tel fs ftel rect
return ()
addCompositionForRecord
:: QName
-> ConHead
-> Telescope
-> [Arg QName]
-> Telescope
-> Type
-> TCM ()
addCompositionForRecord name con tel fs ftel rect = do
compWays <- do
cxt <- getContextTelescope
escapeContext (size cxt) $
if null fs then Left . (,Just []) <$> defineCompData name con (abstract cxt tel) [] ftel rect []
else Right <$>
ifM (return (any (== Irrelevant) $ map getRelevance fs) `and2M` do not . optIrrelevantProjections <$> pragmaOptions)
(return emptyCompKit)
(defineCompKitR name (abstract cxt tel) ftel fs rect)
case compWays of
Right kit -> do
modifySignature $ updateDefinition name $ updateTheDef $ \ d ->
case d of
r@Record{} -> r { recComp = kit }
_ -> __IMPOSSIBLE__
Left y -> do
modifySignature $ updateDefinition (conName con) $ updateTheDef $ \ d ->
case d of
r@Constructor{} -> r { conComp = y }
_ -> __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
, clauseUnreachable = Just False
}
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
, clauseUnreachable = Just False
}
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)
]
]
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
(_ptel,[rt]) = splitAt (size tel - 1) telList
cpo = if hasNamedCon then PatOCon else PatORec
cpi = ConPatternInfo { conPRecord = Just cpo
, 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 = 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
, clauseUnreachable = Just False
}
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 (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
, funCopatternLHS = hasProjectionPatterns cc
})
{ defArgOccurrences = [StrictPos] }
computePolarity [projname]
when (Info.defInstance info == InstanceDef) $
addTypedInstance projname t
recurse
checkProjs ftel1 ftel2 (d : fs) = do
checkDecl d
checkProjs ftel1 ftel2 fs