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.Substitute
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
#include "../../undefined.h"
import Agda.Utils.Impossible
checkRecDef :: Info.DefInfo -> QName -> Maybe A.QName ->
[A.LamBinding] -> A.Expr -> [A.Constructor] -> TCM ()
checkRecDef i name 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 argRelevance $ telToList ftel)
t0' <- normalise t0
s <- case unEl t0' of
Sort s -> return s
_ -> typeError $ ShouldBeASort t0
gamma <- getContextTelescope
let m = qnameToMName name
htel = map hideAndRelParams $ telToList tel
rect = El s $ Def name $ reverse
[ Arg h r (Var i [])
| (i, Arg h r _) <- zip [0..] $ reverse $ telToList gamma
]
telh' h = telFromList $ htel ++ [Arg h recordRelevance ("r", rect)]
tel' = telh' NotHidden
telIFS = telh' Instance
extWithRH h ret = underAbstraction (Arg h recordRelevance rect) (Abs "" ()) $ \_ -> ret
extWithR = extWithRH NotHidden
ext (Arg h r (x, t)) = addCtx x (Arg h r t)
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 _ = []
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
, recPolarity = []
, recArgOccurrences = []
}
addConstant conName $
Defn Relevant conName contype (defaultDisplayForm conName) 0 noCompiledRep $
Constructor { conPars = 0
, conSrcCon = conName
, conData = name
, conAbstr = Info.defAbstract conInfo
, conInd = Inductive
}
let dummy = Var 0 []
telePi ftel (El s dummy) `fitsIn` s
ctx <- (reverse . map hide . take (size tel)) <$> getContext
escapeContext (size tel) $ flip (foldr ext) ctx $ extWithR $ 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
computePolarity name
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 _ ftel2) (A.Field info x (Arg h rel t) : fs) = do
reportSDoc "tc.rec.proj" 5 $ sep
[ text "checking projection"
, nest 2 $ vcat
[ text "top =" <+> (inContext [] . prettyTCM =<< getContextTelescope)
, text "ftel1 =" <+> prettyTCM ftel1
, text "ftel2 =" <+> addCtxTel ftel1 (underAbstraction_ ftel2 prettyTCM)
, text "t =" <+> prettyTCM t
]
]
t <- isType_ t
let finalt = telePi tel t
projname = qualify m $ qnameName x
reportSDoc "tc.rec.proj" 10 $ sep
[ text "adding projection"
, nest 2 $ prettyTCM projname <+> text ":" <+> inContext [] (prettyTCM finalt)
]
let
(ptel,[rt]) = splitAt (size tel 1) $ telToList tel
conp = defaultArg
$ ConP q (Just (fmap snd rt))
$ zipWith3 Arg
(map argHiding (telToList ftel))
(map argRelevance (telToList ftel))
[ VarP "x" | _ <- [1..size ftel] ]
nobind 0 = id
nobind n = Bind . Abs "_" . nobind (n 1)
body = nobind (size ftel1)
$ Bind . Abs "x"
$ nobind (size ftel2)
$ Body $ Var (size ftel2) []
cltel = ftel
clause = Clause { clauseRange = getRange info
, clauseTel = killRange cltel
, clausePerm = idP $ size ftel
, clausePats = [conp]
, clauseBody = body
}
cc <- compileClauses False [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) (defaultDisplayForm projname) 0 noCompiledRep
$ Function { funClauses = [clause]
, funCompiled = cc
, funDelayed = NotDelayed
, funInv = NotInjective
, funAbstr = ConcreteDef
, funPolarity = []
, funArgOccurrences = [Negative]
, funProjection = Just (r, size ptel + 1)
, funStatic = False
}
computePolarity projname
checkProjs (abstract ftel1 $ ExtendTel (Arg h rel t)
$ Abs (show $ qnameName projname) EmptyTel
) (absBody ftel2) fs
checkProjs ftel1 ftel2 (d : fs) = do
checkDecl d
checkProjs ftel1 ftel2 fs