module Agda.TypeChecking.Rules.Record where
import Control.Applicative
import Control.Monad.Trans
import Control.Monad.Reader
import qualified Agda.Utils.IO.Locale as LocIO
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.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 =
noMutualBlock $
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 = mnameFromList $ qnameToList name
hide (Arg _ x) = Arg Hidden x
htel = map hide $ telToList tel
rect = El s $ Def name $ reverse
[ Arg h (Var i [])
| (i, Arg h _) <- zip [0..] $ reverse $ telToList gamma
]
tel' = telFromList $ htel ++ [Arg NotHidden ("r", rect)]
extWithR ret = underAbstraction (Arg NotHidden rect) (Abs "r" ()) $ \_ -> ret
ext (Arg h (x, t)) = addCtx x (Arg h t)
let getName (A.Field _ h x _) = [(h, x)]
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)
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 (maybe name A.axiomName con)
tel' (raise 1 ftel) fields
addConstant name $ Defn name t0 (defaultDisplayForm name) 0
$ Record { recPars = 0
, recClause = Nothing
, recCon = A.axiomName <$> con
, recConType = contype
, recFields = concatMap getName fields
, recTel = ftel
, recAbstr = Info.defAbstract i
, recPolarity = []
, recArgOccurrences = []
}
case con of
Nothing -> return ()
Just (A.Axiom i c _) -> do
addConstant c $
Defn c contype (defaultDisplayForm name) 0 $
Constructor { conPars = 0
, conSrcCon = c
, conData = name
, conHsCode = Nothing
, conAbstr = Info.defAbstract i
, conInd = Inductive
}
verboseS "tc.rec.def" 20 $ liftIO . LocIO.print =<< getConstInfo c
Just _ -> __IMPOSSIBLE__
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 (Arg _ _) ftel2) (A.Field info h x 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
delta <- getContextTelescope
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 = telFromList $ take (size tel 1) $ telToList tel
hps = map (fmap $ VarP . fst) $ telToList ptel
conp = Arg NotHidden
$ ConP q $ zipWith Arg
(map argHiding (telToList ftel))
[ VarP "x" | _ <- [1..size ftel] ]
nobind 0 = id
nobind n = NoBind . nobind (n 1)
body = nobind (size tel 1)
$ nobind (size ftel1)
$ Bind . Abs "x"
$ nobind (size ftel2)
$ Body $ Var 0 []
cltel = ptel `abstract` ftel
clause = Clause { clauseRange = getRange info
, clauseTel = killRange cltel
, clausePerm = idP $ size ptel + size ftel
, clausePats = hps ++ [conp]
, clauseBody = body
}
escapeContext (size tel) $ do
addConstant projname $ Defn projname (killRange finalt) (defaultDisplayForm projname) 0
$ Function { funClauses = [clause]
, funDelayed = NotDelayed
, funInv = NotInjective
, funAbstr = ConcreteDef
, funPolarity = []
, funArgOccurrences = map (const Unused) hps ++ [Negative]
}
computePolarity projname
checkProjs (abstract ftel1 $ ExtendTel (Arg h t)
$ Abs (show $ qnameName projname) EmptyTel
) (absBody ftel2) fs
checkProjs ftel1 ftel2 (d : fs) = do
checkDecl d
checkProjs ftel1 ftel2 fs