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.CompiledClause
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.Constructor ->
[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 fields
]
t <- instantiateFull =<< typeOfConst name
bindParameters ps t $ \tel t0 -> do
t0' <- normalise t0
s <- case unEl t0' of
Sort s -> return s
_ -> typeError $ ShouldBeASort t0
gamma <- getContextTelescope
let m = qnameToMName name
htel = map hide $ telToList tel
rect = El s $ Def name $ reverse
[ Arg h r (Var i [])
| (i, Arg h r _) <- zip [0..] $ reverse $ telToList gamma
]
tel' = telFromList $ htel ++ [defaultArg ("r", rect)]
extWithR ret = underAbstraction (defaultArg rect) (Abs "r" ()) $ \_ -> ret
ext (Arg h r (x, t)) = addCtx x (Arg h r t)
let getName :: A.Declaration -> [Arg QName]
getName (A.Field _ x arg) = [fmap (const x) arg]
getName (A.ScopedDecl _ [f]) = getName f
getName _ = []
ctx <- (reverse . map hide . take (size tel)) <$> getContext
contype <- killRange <$> (instantiateFull =<< isType_ contel)
let TelV ftel _ = telView' contype
let contype = telePi ftel (raise (size ftel) rect)
(hasNamedCon, conName, conInfo) <- case con of
Just (A.Axiom i c _) -> return (True, c, i)
Just _ -> __IMPOSSIBLE__
Nothing -> do
m <- killRange <$> currentModule
c <- qualify m <$> freshName_ "recCon-NOT-PRINTED"
return (False, c, i)
addConstant name $ Defn name t0 (defaultDisplayForm name) 0
$ 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 conName contype (defaultDisplayForm conName) 0 $
Constructor { conPars = 0
, conSrcCon = conName
, conData = name
, conHsCode = Nothing
, conAbstr = Info.defAbstract conInfo
, conInd = Inductive
}
escapeContext (size tel) $ flip (foldr ext) ctx $ extWithR $ do
reportSDoc "tc.rec.def" 10 $ sep
[ text "record section:"
, nest 2 $ sep
[ prettyTCM m <+> (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 conName tel' (raise 1 ftel) fields
let dummy = Var 0 []
telePi ftel (El s dummy) `fitsIn` s
computePolarity name
return ()
checkRecordProjections ::
ModuleName -> QName -> Telescope -> Telescope ->
[A.Declaration] -> TCM ()
checkRecordProjections m 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 =" <+> (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 ":" <+> prettyTCM finalt
]
let
(ptel,[rt]) = splitAt (size tel 1) $ telToList tel
hps = map (fmap $ VarP . fst) $ ptel
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 tel 1)
$ nobind (size ftel1)
$ Bind . Abs "x"
$ nobind (size ftel2)
$ Body $ Var (size ftel2) []
cltel = (telFromList ptel) `abstract` ftel
clause = Clause { clauseRange = getRange info
, clauseTel = killRange cltel
, clausePerm = idP $ size ptel + size ftel
, clausePats = hps ++ [conp]
, clauseBody = body
}
clause2 = Clauses Nothing clause
escapeContext (size tel) $ do
addConstant projname $ Defn projname (killRange finalt) (defaultDisplayForm projname) 0
$ Function { funClauses = [clause2]
, funCompiled = compileClauses [clause2]
, funDelayed = NotDelayed
, funInv = NotInjective
, funAbstr = ConcreteDef
, funPolarity = []
, funArgOccurrences = map (const Unused) hps ++ [Negative]
}
computePolarity projname
checkProjs (abstract ftel1 $ ExtendTel (Arg h Relevant t)
$ Abs (show $ qnameName projname) EmptyTel
) (absBody ftel2) fs
checkProjs ftel1 ftel2 (d : fs) = do
checkDecl d
checkProjs ftel1 ftel2 fs