module Agda.TypeChecking.Rules.Record where
import Control.Applicative
import Control.Monad
import Data.Maybe
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern
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_ )
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 Bool
-> Maybe QName
-> [A.LamBinding]
-> A.Expr
-> [A.Field]
-> TCM ()
checkRecDef i name ind eta 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"
etaenabled <- etaEnabled
let getName :: A.Declaration -> [Arg QName]
getName (A.Field _ x arg) = [x <$ arg]
getName (A.ScopedDecl _ [f]) = getName f
getName _ = []
fs = concatMap getName fields
indCo = rangedThing <$> ind
conInduction = fromMaybe Inductive indCo
haveEta = maybe (Inferred $ conInduction == Inductive && etaenabled) Specified eta
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
}
when (Info.defInstance i == InstanceDef) $ do
addNamedInstance conName name
contype `fitsIn` s
let info = setRelevance recordRelevance defaultArgInfo
addRecordVar = addCtxString "" $ Dom info rect
let m = qnameToMName name
modifyContext (modifyContextEntries hideOrKeepInstance) $ addRecordVar $ 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 hideOrKeepInstance) $ addRecordVar $ 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) =
traceCall (CheckProjection (getRange info) x t) $ 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
, namedClausePats = [Named Nothing <$> numberPatVars (idP $ size ftel) conp]
, clauseBody = body
, clauseType = Just $ Arg ai t
, clauseCatchall = False
}
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
, funTreeless = Nothing
, funDelayed = NotDelayed
, funInv = NotInjective
, funAbstr = ConcreteDef
, funMutual = []
, funProjection = Just projection
, funSmashable = True
, funStatic = False
, funInline = False
, funTerminates = Just True
, funExtLam = Nothing
, funWith = Nothing
, funCopatternLHS = isCopatternLHS [clause]
})
{ defArgOccurrences = [StrictPos] }
computePolarity projname
when (Info.defInstance info == InstanceDef) $
addTypedInstance projname finalt
recurse
checkProjs ftel1 ftel2 (d : fs) = do
checkDecl d
checkProjs ftel1 ftel2 fs