{-# LANGUAGE CPP #-}
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.TypeChecking.Monad
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 ( bindParameters, fitsIn, forceSort)
import Agda.TypeChecking.Rules.Term ( isType_ )
import {-# SOURCE #-} Agda.TypeChecking.Rules.Decl (checkDecl)
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
-> Maybe (Ranged Induction)
-> Maybe HasEta
-> Maybe QName
-> [A.LamBinding]
-> A.Expr
-> [A.Field]
-> TCM ()
checkRecDef i name ind eta con ps contel fields =
traceCall (CheckRecDef (getRange name) (qnameName name) ps fields) $ do
reportSDoc "tc.rec" 10 $ vcat
[ text "checking record def" <+> prettyTCM name
, nest 2 $ text "ps =" <+> prettyList (map prettyAs ps)
, nest 2 $ text "contel =" <+> prettyA contel
, nest 2 $ text "fields =" <+> prettyA (map Constr fields)
]
t <- instantiateFull =<< typeOfConst name
bindParameters ps t $ \tel t0 -> do
reportSDoc "tc.rec" 15 $ text "checking fields"
contype <- workOnTypes $ instantiateFull =<< isType_ contel
reportSDoc "tc.rec" 20 $ vcat
[ text "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
text "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 $ text "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 $ map unArg 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 [ text "Agda doesn't like coinductive records with eta-equality."
, text "If you must, use pragma"
, text "{-# ETA" <+> prettyTCM name <+> text "#-}"
]
reportSDoc "tc.rec" 30 $ text "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
}
addConstant conName $
defaultDefn defaultArgInfo conName (telh `abstract` contype) $
Constructor
{ conPars = npars
, conArity = size fs
, conSrcCon = con
, conData = name
, conAbstr = Info.defAbstract conInfo
, conInd = conInduction
, conForced = []
, conErased = []
}
when (Info.defInstance i == InstanceDef) $ do
addNamedInstance conName name
_ <- fitsIn [] contype s
let info = setRelevance recordRelevance defaultArgInfo
addRecordVar = addContext ("", Dom info rect)
let m = qnameToMName name
modifyContext (map hideOrKeepInstance) $ addRecordVar $ do
reportSDoc "tc.rec.def" 10 $ sep
[ text "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
[ text "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
return ()
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 ai t) ftel2) (A.Field info x _ : fs) =
traceCall (CheckProjection (getRange info) x t) $ do
reportSDoc "tc.rec.proj" 5 $ sep
[ text "checking projection" <+> prettyTCM x
, nest 2 $ vcat
[ text "top =" <+> (inTopContext . prettyTCM =<< getContextTelescope)
, text "tel =" <+> (inTopContext . prettyTCM $ tel)
, text "ftel1 =" <+> prettyTCM ftel1
, text "t =" <+> prettyTCM t
, text "ftel2 =" <+> addContext ftel1 (underAbstraction_ ftel2 prettyTCM)
, text "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 ai t)
$ Abs (nameToArgName $ qnameName projname) EmptyTel)
(ftel2 `absApp` projcall ProjSystem) fs
reportSDoc "tc.rec.proj" 25 $ nest 2 $ text "finalt=" <+> do
inTopContext $ prettyTCM finalt
ifM (return (rel == Irrelevant) `and2M` do not . optIrrelevantProjections <$> pragmaOptions) recurse $ do
reportSDoc "tc.rec.proj" 10 $ sep
[ text "adding projection"
, nest 2 $ prettyTCM projname <+> text ":" <+> 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
, conPType = Just $ argFromDom $ fmap snd rt
, conPLazy = True }
conp = defaultArg $ ConP con cpi $
[ Arg ai' $ unnamed $ varP "x" | Dom 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 (\ (Dom ai (x,_)) -> Arg ai x) telList
}
reportSDoc "tc.rec.proj" 80 $ sep
[ text "adding projection"
, nest 2 $ prettyTCM projname <+> text (show clause)
]
reportSDoc "tc.rec.proj" 70 $ sep
[ text "adding projection"
, nest 2 $ prettyTCM projname <+> text (show (clausePats clause)) <+> text "=" <+>
inTopContext (addContext ftel (maybe (text "_|_") prettyTCM (clauseBody clause)))
]
reportSDoc "tc.rec.proj" 10 $ sep
[ text "adding projection"
, nest 2 $ prettyTCM (QNamed projname clause)
]
cc <- compileClauses Nothing [clause]
reportSDoc "tc.cc" 60 $ do
sep [ text "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
, funProjection = Just projection
, funMutual = Just []
, funTerminates = Just True
, funCopatternLHS = hasProjectionPatterns cc
})
{ defArgOccurrences = [StrictPos] }
computePolarity [projname]
when (Info.defInstance info == InstanceDef) $
addTypedInstance projname finalt
recurse
checkProjs ftel1 ftel2 (d : fs) = do
checkDecl d
checkProjs ftel1 ftel2 fs