module Agda.TypeChecking.Rules.Record where
import Control.Applicative
import Data.Maybe
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Common
import Agda.Syntax.Internal as I
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.Compile
import Agda.TypeChecking.Rules.Data ( bindParameters, fitsIn )
import Agda.TypeChecking.Rules.Term ( isType_, ConvColor(..) )
import Agda.TypeChecking.Rules.Decl (checkDecl)
import Agda.Utils.Size
import Agda.Utils.Permutation
import Agda.Utils.Monad
import Agda.Interaction.Options
#include "undefined.h"
import Agda.Utils.Impossible
checkRecDef
:: Info.DefInfo
-> QName
-> Maybe (Ranged Induction)
-> Maybe A.QName
-> [A.LamBinding]
-> A.Expr
-> [A.Field]
-> TCM ()
checkRecDef i name ind 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 <- killRange <$> (instantiateFull =<< isType_ contel)
reportSDoc "tc.rec" 20 $ vcat
[ text "contype = " <+> prettyTCM contype ]
let TelV ftel _ = telView' contype
recordRelevance = minimum $ Irrelevant : (map getRelevance $ telToList ftel)
t0' <- normalise t0
s <- case ignoreSharing $ unEl t0' of
Sort s -> return s
_ -> typeError $ ShouldBeASort t0
gamma <- getContextTelescope
reportSDoc "tc.rec" 20 $ vcat
[ text "gamma = " <+> inTopContext (prettyTCM gamma) ]
let rect = El s $ Def name $ map Apply $ teleArgs gamma
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"
let getName :: A.Declaration -> [A.Arg QName]
getName (A.Field _ x arg) = [x <$ arg]
getName (A.ScopedDecl _ [f]) = getName f
getName _ = []
fs = concatMap (convColor . getName) fields
indCo = rangedThing <$> ind
conInduction = fromMaybe Inductive indCo
haveEta = conInduction == Inductive
con = ConHead conName conInduction $ map unArg fs
reportSDoc "tc.rec" 30 $ text "record constructor is " <+> text (show con)
addConstant name $ defaultDefn defaultArgInfo name t0
$ Record { recPars = 0
, recClause = Nothing
, recConHead = con
, recNamedCon = hasNamedCon
, recConType = contype
, recFields = fs
, recTel = ftel
, recAbstr = Info.defAbstract i
, recEtaEquality = haveEta
, recInduction = indCo
, recRecursive = False
, recMutual = []
}
addConstant conName $
defaultDefn defaultArgInfo conName contype $
Constructor { conPars = 0
, conSrcCon = con
, conData = name
, conAbstr = Info.defAbstract conInfo
, conInd = conInduction
}
addNamedInstance conName name
contype `fitsIn` s
let
m = qnameToMName name
htel = map hideAndRelParams $ telToList tel
info = setRelevance recordRelevance defaultArgInfo
tel' = telFromList $ htel ++ [Dom info ("r", rect)]
ext (Dom info (x, t)) = addCtx x (Dom info t)
ctx <- (reverse . map (setHiding Hidden) . take (size tel)) <$> getContext
reportSDoc "tc.rec" 80 $ sep
[ text "visibility-modified record telescope"
, nest 2 $ text "ctx =" <+> prettyTCM ctx
]
escapeContext (size tel) $ flip (foldr ext) ctx $
underAbstraction (Dom info rect) (Abs "" ()) $ \_ -> do
reportSDoc "tc.rec.def" 10 $ sep
[ text "record section:"
, nest 2 $ sep
[ prettyTCM m <+> (inTopContext . prettyTCM =<< getContextTelescope)
, fsep $ punctuate comma $ map (text . show . getName) fields
]
]
reportSDoc "tc.rec.def" 15 $ nest 2 $ vcat
[ text "field tel =" <+> escapeContext 1 (prettyTCM ftel)
]
addSection m
modifyContext (modifyContextEntries (setHiding Hidden)) $ do
underAbstraction (Dom info rect) (Abs "" ()) $ \_ -> do
withCurrentModule m $ do
tel' <- getContextTelescope
checkRecordProjections m name con tel' (raise 1 ftel) fields
return ()
checkRecordProjections ::
ModuleName -> QName -> ConHead -> Telescope -> Telescope ->
[A.Declaration] -> TCM ()
checkRecordProjections m r 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) = do
reportSDoc "tc.rec.proj" 5 $ sep
[ text "checking projection" <+> text (show x)
, nest 2 $ vcat
[ text "top =" <+> (inTopContext . prettyTCM =<< getContextTelescope)
, text "tel =" <+> (inTopContext . prettyTCM $ tel)
, text "ftel1 =" <+> prettyTCM ftel1
, text "t =" <+> prettyTCM t
, text "ftel2 =" <+> addCtxTel ftel1 (underAbstraction_ ftel2 prettyTCM)
]
]
let finalt = telePi (replaceEmptyName "r" tel) t
projname = qualify m $ qnameName x
projcall = Var 0 [Proj projname]
rel = getRelevance ai
recurse = checkProjs (abstract ftel1 $ ExtendTel (Dom ai t)
$ Abs (nameToArgName $ qnameName projname) EmptyTel)
(ftel2 `absApp` projcall) 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
Irrelevant -> DontCare
_ -> __IMPOSSIBLE__
let
(ptel,[rt]) = splitAt (size tel 1) $ telToList tel
projArgI = domInfo rt
cpi = ConPatternInfo (Just ConPRec) (Just $ argFromDom $ fmap snd rt)
conp = defaultArg $ ConP con cpi $
[ Arg info $ unnamed $ VarP "x" | Dom info _ <- telToList ftel ]
nobind 0 = id
nobind n = Bind . Abs "_" . nobind (n 1)
body = nobind (size ftel1)
$ Bind . Abs "x"
$ nobind (size ftel2)
$ Body $ bodyMod $ var (size ftel2)
cltel = ftel
clause = Clause { clauseRange = getRange info
, clauseTel = killRange cltel
, clausePerm = idP $ size ftel
, namedClausePats = [Named Nothing <$> conp]
, clauseBody = body
, clauseType = Just $ Arg ai t
}
let core = Lam projArgI $ Abs "r" $ bodyMod $ projcall
proj = teleNoAbs ptel core
projection = Projection
{ projProper = Just projname
, projFromType = r
, projIndex = size ptel + 1
, projDropPars = proj
, projArgInfo = projArgI
}
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 (addCtxTel ftel (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" 10 $ do
sep [ text "compiled clauses of " <+> prettyTCM projname
, nest 2 $ text (show cc)
]
escapeContext (size tel) $ do
addConstant projname $
(defaultDefn ai projname (killRange finalt)
Function { funClauses = [clause]
, funCompiled = Just cc
, funDelayed = NotDelayed
, funInv = NotInjective
, funAbstr = ConcreteDef
, funMutual = []
, funProjection = Just projection
, funStatic = False
, funCopy = False
, funTerminates = Just True
, funExtLam = Nothing
, funWith = Nothing
, funCopatternLHS = isCopatternLHS [clause]
})
{ defArgOccurrences = [StrictPos] }
computePolarity projname
recurse
checkProjs ftel1 ftel2 (d : fs) = do
checkDecl d
checkProjs ftel1 ftel2 fs