module Agda.TypeChecking.Rules.Record where
import Control.Applicative
import Control.Monad.Trans
import Control.Monad.Reader
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Position
import qualified Agda.Syntax.Info as Info
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin ( primIrrAxiom )
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Reduce
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_ )
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 Induction -> Maybe A.QName ->
[A.LamBinding] -> A.Expr -> [A.Field] -> TCM ()
checkRecDef i name ind con ps contel fields =
traceCall (CheckRecDef (getRange i) (qnameName name) ps fields) $ do
reportSDoc "tc.rec" 10 $ vcat
[ text "checking record def" <+> prettyTCM name
, nest 2 $ text "ps =" <+> prettyList (map prettyA 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)
let TelV ftel _ = telView' contype
recordRelevance = minimum $ Irrelevant : (map domRelevance $ telToList ftel)
t0' <- normalise t0
s <- case ignoreSharing $ unEl t0' of
Sort s -> return s
_ -> typeError $ ShouldBeASort t0
gamma <- getContextTelescope
let rect = El s $ Def name $ 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"
return (False, c, i)
reportSDoc "tc.rec" 15 $ text "adding record type to signature"
let getName :: A.Declaration -> [Arg QName]
getName (A.Field _ x arg) = [fmap (const x) arg]
getName (A.ScopedDecl _ [f]) = getName f
getName _ = []
indCo = maybe Inductive id ind
addConstant name $ Defn Relevant name t0 [] [] (defaultDisplayForm name) 0 noCompiledRep
$ Record { recPars = 0
, recClause = Nothing
, recCon = conName
, recNamedCon = hasNamedCon
, recConType = contype
, recFields = concatMap getName fields
, recTel = ftel
, recAbstr = Info.defAbstract i
, recEtaEquality = True
, recInduction = indCo
, recRecursive = False
, recMutual = []
}
addConstant conName $
Defn Relevant conName contype [] [] (defaultDisplayForm conName) 0 noCompiledRep $
Constructor { conPars = 0
, conSrcCon = conName
, conData = name
, conAbstr = Info.defAbstract conInfo
, conInd = indCo
}
let dummy = var 0
telePi ftel (El s dummy) `fitsIn` s
ctx <- (reverse . map (mapDomHiding $ const Hidden) . take (size tel)) <$> getContext
let
m = qnameToMName name
htel = map hideAndRelParams $ telToList tel
tel' = telFromList $ htel ++ [Dom NotHidden recordRelevance ("r", rect)]
ext (Dom h r (x, t)) = addCtx x (Dom h r t)
escapeContext (size tel) $ flip (foldr ext) ctx $
underAbstraction (Dom NotHidden recordRelevance rect) (Abs "" ()) $ \_ -> do
reportSDoc "tc.rec.def" 10 $ sep
[ text "record section:"
, nest 2 $ sep
[ prettyTCM m <+> (inContext [] . 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 (size tel')
withCurrentModule m $
checkRecordProjections m name conName tel' (raise 1 ftel) fields
return ()
checkRecordProjections ::
ModuleName -> QName -> QName -> Telescope -> Telescope ->
[A.Declaration] -> TCM ()
checkRecordProjections m r q tel ftel fs = 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 h rel 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 =" <+> (inContext [] . prettyTCM =<< getContextTelescope)
, text "tel =" <+> prettyTCM tel
, text "ftel1 =" <+> prettyTCM ftel1
, text "t =" <+> prettyTCM t
, text "ftel2 =" <+> addCtxTel ftel1 (underAbstraction_ ftel2 prettyTCM)
]
]
let finalt = telePi tel t
projname = qualify m $ qnameName x
projcall = Def projname [defaultArg $ var 0]
recurse = checkProjs (abstract ftel1 $ ExtendTel (Dom h rel t)
$ Abs (show $ qnameName projname) EmptyTel)
(ftel2 `absApp` projcall) fs
reportSDoc "tc.rec.proj" 25 $ nest 2 $ text "finalt=" <+> 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 ":" <+> inContext [] (prettyTCM finalt)
]
bodyMod <- do
case rel of
Relevant -> return $ \ n x -> x
Irrelevant -> return $ \ n x -> DontCare x
_ -> __IMPOSSIBLE__
let
(ptel,[rt]) = splitAt (size tel 1) $ telToList tel
conp = defaultArg
$ ConP q (Just (argFromDom $ fmap snd rt))
[ Arg h r (VarP "x") | Dom h r _ <- telToList ftel ]
nobind 0 = id
nobind n = Bind . Abs "_" . nobind (n 1)
body = nobind (size ftel1)
$ Bind . Abs "x"
$ nobind (size ftel2)
$ Body $ bodyMod (size ftel) $ Var (size ftel2) []
cltel = ftel
clause = Clause { clauseRange = getRange info
, clauseTel = killRange cltel
, clausePerm = idP $ size ftel
, clausePats = [conp]
, clauseBody = body
}
reportSDoc "tc.rec.proj" 20 $ sep
[ text "adding projection"
, nest 2 $ prettyTCM projname <+> text (show clause)
]
reportSDoc "tc.rec.proj" 10 $ sep
[ text "adding projection"
, nest 2 $ prettyTCM projname <+> text (show (clausePats clause)) <+> text "=" <+>
inContext [] (addCtxTel ftel (prettyTCM (clauseBody 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 $ Defn rel projname (killRange finalt) [] [StrictPos] (defaultDisplayForm projname) 0 noCompiledRep
$ Function { funClauses = [clause]
, funCompiled = cc
, funDelayed = NotDelayed
, funInv = NotInjective
, funAbstr = ConcreteDef
, funMutual = []
, funProjection = Just (r, size ptel + 1)
, funStatic = False
, funCopy = False
, funTerminates = Just True
}
computePolarity projname
recurse
checkProjs ftel1 ftel2 (d : fs) = do
checkDecl d
checkProjs ftel1 ftel2 fs