{-| Module : Idris.Elab.Data Description : Code to elaborate data structures. License : BSD3 Maintainer : The Idris Community. -} {-# LANGUAGE CPP, PatternGuards #-} module Idris.Elab.Data(elabData) where import Idris.AbsSyntax import Idris.ASTUtils import Idris.Core.Evaluate import Idris.Core.TT import Idris.Core.Typecheck import Idris.Delaborate import Idris.Docstrings import Idris.Elab.Rewrite import Idris.Elab.Type import Idris.Elab.Utils import Idris.Elab.Value import Idris.Error import Idris.Output (iWarn, sendHighlighting) import Util.Pretty #if (MIN_VERSION_base(4,11,0)) import Prelude hiding (id, (.), (<>)) #else import Prelude hiding (id, (.)) #endif import Control.Category import Control.Monad import Data.List import qualified Data.Set as S warnLC :: FC -> Name -> Idris () warnLC fc n = iWarn fc $ annName n <+> text "has a name which may be implicitly bound." <> line <> text "This is likely to lead to problems!" elabData :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm)-> [(Name, Docstring (Either Err PTerm))] -> FC -> DataOpts -> PData -> Idris () elabData info syn doc argDocs fc opts (PLaterdecl n nfc t_in) = do logElab 1 (show (fc, doc)) checkUndefined fc n when (implicitable (nsroot n)) $ warnLC fc n (cty, _, t, inacc) <- buildType info syn fc [] n t_in addIBC (IBCDef n) updateContext (addTyDecl n (TCon 0 0) cty) -- temporary, to check cons sendHighlighting $ S.fromList [(FC' nfc, AnnName n Nothing Nothing Nothing)] elabData info syn doc argDocs fc opts (PDatadecl n nfc t_in dcons) = do let codata = Codata `elem` opts logElab 1 (show fc) undef <- isUndefined fc n when (implicitable (nsroot n)) $ warnLC fc n (cty, ckind, t, inacc) <- buildType info syn fc [] n t_in -- if n is defined already, make sure it is just a type declaration -- with the same type we've just elaborated, and no constructors -- yet i <- getIState checkDefinedAs fc n cty i -- temporary, to check cons when undef $ updateContext (addTyDecl n (TCon 0 0) cty) let cnameinfo = cinfo info (map cname dcons) unique <- case getRetTy (normalise (tt_ctxt i) [] cty) of UType UniqueType -> return True UType _ -> return False TType _ -> return False rt -> tclift $ tfail (At fc (Elaborating "type constructor " n Nothing (Msg "Not a valid type constructor"))) cons <- mapM (elabCon cnameinfo syn n codata (getRetTy cty) ckind) dcons ttag <- getName ctxt <- getContext let params = findParams n (normalise ctxt [] cty) (map snd cons) logElab 2 $ "Parameters : " ++ show params addParamConstraints fc params cty cons i <- getIState -- TI contains information about mutually declared types - this will -- be updated when the mutual block is complete putIState (i { idris_datatypes = addDef n (TI (map fst cons) codata opts params [n] (any linearArg (map snd cons))) (idris_datatypes i) }) addIBC (IBCDef n) addIBC (IBCData n) checkDocs fc argDocs t doc' <- elabDocTerms info doc argDocs' <- mapM (\(n, d) -> do d' <- elabDocTerms info d return (n, d')) argDocs addDocStr n doc' argDocs' addIBC (IBCDoc n) let metainf = DataMI params addIBC (IBCMetaInformation n metainf) -- TMP HACK! Make this a data option updateContext (addDatatype (Data n ttag cty unique cons)) updateContext (setMetaInformation n metainf) mapM_ totcheck (zip (repeat fc) (map fst cons)) -- mapM_ (checkPositive n) cons -- if there's exactly one constructor, -- mark both the type and the constructor as detaggable case cons of [(cn,ct)] -> setDetaggable cn >> setDetaggable n >> addIBC (IBCOpt cn) >> addIBC (IBCOpt n) _ -> return () -- create a rewriting lemma when (n /= sUN "=") $ elabRewriteLemma info n cty -- Emit highlighting info sendHighlighting $ S.fromList $ [(FC' nfc, AnnName n Nothing Nothing Nothing)] ++ map (\(_, _, n, nfc, _, _, _) -> (FC' nfc, AnnName n Nothing Nothing Nothing)) dcons where checkDefinedAs fc n t i = let defined = tclift $ tfail (At fc (AlreadyDefined n)) ctxt = tt_ctxt i in case lookupDef n ctxt of [] -> return () [TyDecl _ ty] -> case converts ctxt [] t ty of OK () -> case lookupCtxtExact n (idris_datatypes i) of Nothing -> return () _ -> defined _ -> defined _ -> defined cname (_, _, n, _, _, _, _) = n -- Abuse of ElabInfo. -- TODO Contemplate whether the ElabInfo type needs modification. cinfo :: ElabInfo -> [Name] -> ElabInfo cinfo info ds = let newps = params info dsParams = map (\n -> (n, [])) ds newb = addAlist dsParams (inblock info) in info { params = newps, inblock = newb, liftname = id -- Is this appropriate? } elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool -> Type -> -- for unique kind checking Type -> -- data type's kind (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC, [Name]) -> Idris (Name, Type) elabCon info syn tn codata expkind dkind (doc, argDocs, n, nfc, t_in, fc, forcenames) = do checkUndefined fc n when (implicitable (nsroot n)) $ warnLC fc n logElab 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t_in (cty, ckind, t, inacc) <- buildType info syn fc [Constructor] n (if codata then mkLazy t_in else t_in) ctxt <- getContext let cty' = normalise ctxt [] cty checkUniqueKind ckind expkind -- Check that the constructor type is, in fact, a part of the family being defined tyIs n cty' -- Need to calculate forceability from the non-normalised type, -- because we might not be able to export the definitions which -- we're normalising which changes the forceability status! let force = if tn == sUN "Delayed" then [] -- TMP HACK! Totality checker needs this info else forceArgs ctxt tn cty logElab 5 $ show fc ++ ":Constructor " ++ show n ++ " elaborated : " ++ show t logElab 5 $ "Inaccessible args: " ++ show inacc logElab 5 $ "Forceable args: " ++ show force logElab 2 $ "---> " ++ show n ++ " : " ++ show cty -- Add to the context (this is temporary, so that later constructors -- can be indexed by it) updateContext (addTyDecl n (DCon 0 0 False) cty) addIBC (IBCDef n) checkDocs fc argDocs t doc' <- elabDocTerms info doc argDocs' <- mapM (\(n, d) -> do d' <- elabDocTerms info d return (n, d')) argDocs addDocStr n doc' argDocs' addIBC (IBCDoc n) fputState (opt_inaccessible . ist_optimisation n) inacc fputState (opt_forceable . ist_optimisation n) force addIBC (IBCOpt n) return (n, cty) where tyIs con (Bind n b sc) = tyIs con (substV (P Bound n Erased) sc) tyIs con t | (P Bound n' _, _) <- unApply t = if n' /= tn then tclift $ tfail (At fc (Elaborating "constructor " con Nothing (Msg ("Type level variable " ++ show n' ++ " is not " ++ show tn)))) else return () tyIs con t | (P _ n' _, _) <- unApply t = if n' /= tn then tclift $ tfail (At fc (Elaborating "constructor " con Nothing (Msg (show n' ++ " is not " ++ show tn)))) else return () tyIs con t = tclift $ tfail (At fc (Elaborating "constructor " con Nothing (Msg (show t ++ " is not " ++ show tn)))) mkLazy (PPi pl n nfc ty sc) = let ty' = if getTyName ty then PApp fc (PRef fc [] (sUN "Delayed")) [pexp (PRef fc [] (sUN "Infinite")), pexp ty] else ty in PPi pl n nfc ty' (mkLazy sc) mkLazy t = t getTyName (PApp _ (PRef _ _ n) _) = n == nsroot tn getTyName (PRef _ _ n) = n == nsroot tn getTyName _ = False -- if the constructor is a UniqueType, the datatype must be too -- (AnyType is fine, since that is checked for uniqueness too) -- if hte contructor is AnyType, the datatype must be at least AnyType checkUniqueKind (UType NullType) (UType NullType) = return () checkUniqueKind (UType NullType) _ = tclift $ tfail (At fc (UniqueKindError NullType n)) checkUniqueKind (UType UniqueType) (UType UniqueType) = return () checkUniqueKind (UType UniqueType) (UType AllTypes) = return () checkUniqueKind (UType UniqueType) _ = tclift $ tfail (At fc (UniqueKindError UniqueType n)) checkUniqueKind (UType AllTypes) (UType AllTypes) = return () checkUniqueKind (UType AllTypes) (UType UniqueType) = return () checkUniqueKind (UType AllTypes) _ = tclift $ tfail (At fc (UniqueKindError AllTypes n)) checkUniqueKind _ _ = return () forceArgs :: Context -> Name -> Type -> [Int] forceArgs ctxt tn ty = forceFrom 0 ty where -- for each argument, substitute in MN pos "FF" -- then when we look at the return type, if we see MN pos name -- constructor guarded, then 'pos' is a forceable position forceFrom :: Int -> Type -> [Int] forceFrom i (Bind n (Pi _ _ _ _) sc) = forceFrom (i + 1) (substV (P Ref (sMN i "FF") Erased) sc) forceFrom i sc -- Go under the top level type application -- We risk affecting erasure of more complex indices, so we'll only -- mark something forced if *everything* which appears in an index -- is forceable -- (FIXME: Actually the real risk is if we erase something a programmer -- definitely wants, which is particularly the case with 'views'. -- So perhaps we need a way of marking that in the source?) | (P _ ty _, args) <- unApply sc, ty == tn -- Must be the right top level type! = if null (concatMap (findNonForcePos True) args) then nub (concatMap findForcePos args) else [] forceFrom i sc = [] findForcePos (P _ (MN i ff) _) | ff == txt "FF" = [i] -- Only look under constructors in applications findForcePos ap@(App _ f a) | (P _ con _, args) <- unApply ap, isDConName con ctxt = nub $ concatMap findForcePos args findForcePos _ = [] findNonForcePos fok (P _ (MN i ff) _) | ff == txt "FF" = if fok then [] else [i] -- Look under non-constructors in applications for things which can't -- be forced findNonForcePos fok ap@(App _ f a) | (P _ con _, args) <- unApply ap = nub $ concatMap (findNonForcePos (fok && isConName con ctxt)) args findNonForcePos _ _ = [] addParamConstraints :: FC -> [Int] -> Type -> [(Name, Type)] -> Idris () addParamConstraints fc ps cty cons = case getRetTy cty of TType cvar -> mapM_ (addConConstraint ps cvar) (map getParamNames cons) _ -> return () where getParamNames (n, ty) = (ty, getPs ty) getPs (Bind n (Pi _ _ _ _) sc) = getPs (substV (P Ref n Erased) sc) getPs t | (f, args) <- unApply t = paramArgs 0 args paramArgs i (P _ n _ : args) | i `elem` ps = n : paramArgs (i + 1) args paramArgs i (_ : args) = paramArgs (i + 1) args paramArgs i [] = [] addConConstraint ps cvar (ty, pnames) = constraintTy ty where constraintTy (Bind n (Pi _ _ ty _) sc) = case getRetTy ty of TType avar -> do tit <- typeInType when (not tit) $ do ctxt <- getContext let tv = next_tvar ctxt let con = if n `elem` pnames then ULE avar cvar else ULT avar cvar addConstraints fc (tv, [con]) addIBC (IBCConstraint fc con) _ -> return () constraintTy t = return ()