module Agda.TypeChecking.Rules.Record where
import Prelude hiding (null)
import Control.Applicative hiding (empty)
import Control.Monad
import Data.Maybe
import qualified Data.Set as Set
import Agda.Interaction.Options
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, forceSort)
import Agda.TypeChecking.Rules.Term ( isType_ )
import Agda.TypeChecking.Rules.Decl (checkDecl)
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Utils.Size
#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 <- instantiateFull =<< isType_ contel
reportSDoc "tc.rec" 20 $ vcat
[ text "contype = " <+> prettyTCM contype ]
let TelV ftel _ = telView' contype
recordRelevance = minimum $ Irrelevant : (map getRelevance $ telToList ftel)
TelV idxTel s <- telView t0
unless (null idxTel) $ typeError $ ShouldBeASort t0
s <- forceSort s
reportSDoc "tc.rec" 20 $ do
gamma <- getContextTelescope
text "gamma = " <+> inTopContext (prettyTCM gamma)
rect <- El s . Def name . map Apply <$> getContextArgs
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 False) Specified eta
con = ConHead conName conInduction $ map unArg fs
reportSDoc "tc.rec" 30 $ text "record constructor is " <+> text (show con)
let npars = size tel
telh = fmap hideAndRelParams tel
escapeContext npars $ do
addConstant name $
defaultDefn defaultArgInfo name t $
Record
{ recPars = npars
, recClause = Nothing
, recConHead = con
, recNamedCon = hasNamedCon
, recFields = fs
, recTel = telh `abstract` ftel
, recAbstr = Info.defAbstract i
, recEtaEquality' = haveEta
, recInduction = indCo
, recRecursive = False
, recMutual = []
}
addConstant conName $
defaultDefn defaultArgInfo conName (telh `abstract` contype) $
Constructor
{ conPars = npars
, conSrcCon = con
, conData = name
, conAbstr = Info.defAbstract conInfo
, conInd = conInduction
, conErased = []
}
when (Info.defInstance i == InstanceDef) $ do
addNamedInstance conName name
contype `fitsIn` s
let info = setRelevance recordRelevance defaultArgInfo
addRecordVar = addContext' ("", 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
setDefaultModuleParameters m
checkRecordProjections m name hasNamedCon con tel' (raise 1 ftel) fields
return ()
checkRecordProjections ::
ModuleName -> QName -> Bool -> ConHead -> Telescope -> Telescope ->
[A.Declaration] -> TCM ()
checkRecordProjections m r hasNamedCon 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 =" <+> addContext ftel1 (underAbstraction_ ftel2 prettyTCM)
]
]
let finalt = telePi (replaceEmptyName "r" tel) t
projname = qualify m $ qnameName x
projcall o = Var 0 [Proj o projname]
rel = getRelevance ai
recurse = checkProjs (abstract ftel1 $ ExtendTel (Dom ai t)
$ Abs (nameToArgName $ qnameName projname) EmptyTel)
(ftel2 `absApp` projcall ProjSystem) 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
NonStrict -> id
Irrelevant -> DontCare
_ -> __IMPOSSIBLE__
let
telList = telToList tel
(_ptel,[rt]) = splitAt (size tel 1) telList
cpo = if hasNamedCon then ConOCon else ConORec
cpi = ConPatternInfo (Just cpo) (Just $ argFromDom $ fmap snd rt)
conp = defaultArg $ ConP con cpi $
[ Arg info $ unnamed $ varP "x" | Dom info _ <- telToList ftel ]
body = Just $ bodyMod $ var (size ftel2)
cltel = ftel
clause = Clause { clauseRange = getRange info
, clauseTel = killRange cltel
, namedClausePats = [Named Nothing <$> numberPatVars __IMPOSSIBLE__ (idP $ size ftel) conp]
, clauseBody = body
, clauseType = Just $ Arg ai t
, clauseCatchall = False
}
let projection = Projection
{ projProper = True
, projOrig = projname
, projFromType = defaultArg r
, projIndex = size tel
, projLams = ProjLams $ map (\ (Dom ai (x,_)) -> Arg ai x) telList
}
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 (addContext ftel (maybe (text "_|_") 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)
emptyFunction
{ funClauses = [clause]
, funCompiled = Just cc
, funProjection = Just projection
, funTerminates = Just True
, 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