idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-19 17:21:59 +03:00
Code Issues Projects Releases Wiki Activity

[ warning ] for incompatible visibilities on forward decls and definitions. (#3063)

Browse Source
This commit is contained in:
Adowrath 2023-10-25 12:24:43 +02:00 committed by GitHub
parent 305604d243
commit ea093ffaed
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
49 changed files with 401 additions and 112 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
CHANGELOG.md
View File

@ -17,6 +17,10 @@
[#1066](https://github.com/idris-lang/idris2/issues/1066)).
* `%hide` directives can now hide conflicting fixities from other modules.
* Fixity declarations can now be kept private with export modifiers.
* Forward-declarations whose visibility differ from their
actual definition now emit a warning, unless the definition
has no specified visibility
(addressing Issue [#1236](https://github.com/idris-lang/Idris2/issues/1236)).
* New `fromTTImp`, `fromName`, and `fromDecls` names for custom `TTImp`,
`Name`, and `Decls` literals.
* Call to `%macro`-functions do not require the `ElabReflection` extension.
@ -119,6 +123,9 @@
To avoid confusing tooling about which `.ipkg` to use, the
package file is under the newly added `ipkg` sub-directory.
* Added `Libraries.Data.WithDefault` to facilitate consistent use
of a default-if-unspecified value, currently for `private` visibility.
### Library changes
#### Prelude
@ -211,6 +218,8 @@
* Adds `infixOfBy` and `isInfixOfBy` into `Data.List`.
* Adds `WithDefault` into `Language.Reflection.TTImp`, mirroring compiler addition.
* Adds updating functions to `SortedMap` and `SortedDMap`.
* Adds `grouped` function to `Data.List` for splitting a list into equal-sized slices.

1
idris2api.ipkg
View File

@ -189,6 +189,7 @@ modules =
Libraries.Data.Tap,
Libraries.Data.UserNameMap,
Libraries.Data.Version,
Libraries.Data.WithDefault,
Libraries.System.File,
Libraries.System.File.Buffer,

48
libs/base/Language/Reflection/TTImp.idr
View File

@ -178,17 +178,42 @@ mutual
%name Clause cl
public export
data WithDefault : (a : Type) -> (def : a) -> Type where
DefaultedValue : WithDefault a def
SpecifiedValue : a -> WithDefault a def
export
specified : a -> WithDefault a def
specified = SpecifiedValue
export
defaulted : WithDefault a def
defaulted = DefaultedValue
export
collapseDefault : {def : a} -> WithDefault a def -> a
collapseDefault DefaultedValue = def
collapseDefault (SpecifiedValue a) = a
export
onWithDefault : (defHandler : Lazy b) -> (valHandler : a -> b) ->
WithDefault a def -> b
onWithDefault defHandler _ DefaultedValue = defHandler
onWithDefault _ valHandler (SpecifiedValue v) = valHandler v
public export
data Decl : Type where
IClaim : FC -> Count -> Visibility -> List FnOpt ->
ITy -> Decl
IData : FC -> Visibility -> Maybe TotalReq -> Data -> Decl
IData : FC -> WithDefault Visibility Private -> Maybe TotalReq -> Data -> Decl
IDef : FC -> Name -> (cls : List Clause) -> Decl
IParameters : FC -> (params : List (Name, Count, PiInfo TTImp, TTImp)) ->
(decls : List Decl) -> Decl
IRecord : FC ->
Maybe String -> -- nested namespace
Visibility -> Maybe TotalReq -> Record -> Decl
WithDefault Visibility Private ->
Maybe TotalReq -> Record -> Decl
INamespace : FC -> Namespace -> (decls : List Decl) -> Decl
ITransform : FC -> Name -> TTImp -> TTImp -> Decl
IRunElabDecl : FC -> TTImp -> Decl
@ -300,6 +325,25 @@ Eq DataOpt where
NoNewtype == NoNewtype = True
_ == _ = False
public export
Eq a => Eq (WithDefault a def) where
DefaultedValue == DefaultedValue = True
DefaultedValue == SpecifiedValue _ = False
SpecifiedValue _ == DefaultedValue = False
SpecifiedValue x == SpecifiedValue y = x == y
public export
Ord a => Ord (WithDefault a def) where
compare DefaultedValue DefaultedValue = EQ
compare DefaultedValue (SpecifiedValue _) = LT
compare (SpecifiedValue _) DefaultedValue = GT
compare (SpecifiedValue x) (SpecifiedValue y) = compare x y
public export
{def : a} -> (Show a) => Show (WithDefault a def) where
show (SpecifiedValue x) = show x
show DefaultedValue = show def
public export
Eq a => Eq (PiInfo a) where
ImplicitArg == ImplicitArg = True

9
src/Compiler/Common.idr
View File

@ -16,13 +16,14 @@ import Core.Directory
import Core.Options
import Core.TT
import Core.TTC
import Libraries.Data.IOArray
import Libraries.Utils.Scheme
import Data.List
import Data.List1
import Libraries.Data.NameMap
import Data.String as String
import Libraries.Data.NameMap
import Libraries.Data.IOArray
import Libraries.Data.WithDefault
import Libraries.Utils.Scheme
import Idris.Syntax
import Idris.Env
@ -151,7 +152,7 @@ getMinimalDef (Coded ns bin)
name <- fromBuf b
let def
= MkGlobalDef fc name (Erased fc Placeholder) [] [] [] [] mul
[] Public (MkTotality Unchecked IsCovering) False
[] (specified Public) (MkTotality Unchecked IsCovering) False
[] Nothing refsR False False True
None cdef Nothing [] Nothing
pure (def, Just (ns, bin))

7
src/Compiler/Inline.idr
View File

@ -14,11 +14,12 @@ import Core.Hash
import Core.Options
import Core.TT
import Libraries.Data.LengthMatch
import Data.Maybe
import Libraries.Data.NameMap
import Data.List
import Data.Vect
import Libraries.Data.LengthMatch
import Libraries.Data.NameMap
import Libraries.Data.WithDefault
%default covering
@ -561,7 +562,7 @@ addArityHash n
Just def <- lookupCtxtExact n (gamma defs) | Nothing => pure ()
let Just cexpr = compexpr def | Nothing => pure ()
let MkFun args _ = cexpr | _ => pure ()
case visibility def of
case collapseDefault $ visibility def of
Private => pure ()
_ => addHash (n, length args)

3
src/Compiler/Opts/InlineHeuristics.idr
View File

@ -4,6 +4,7 @@ import Compiler.CompileExpr
import Core.Context
import Core.Context.Log
import Data.Vect
import Libraries.Data.WithDefault
parameters (fn : Name)
isVar : CExp vars -> Bool
@ -55,7 +56,7 @@ inlineHeuristics fn = do
-- intervention by this function.
-- We could lift this public restriction if we checked that the source def was _either
-- public OR the destination was the same module as the source_.
let Public = gdef.visibility
let Public = collapseDefault $ gdef.visibility
| _ => pure ()
unless (NoInline `elem` gdef.flags) $ do
log "compiler.inline.heuristic" 25 $ "inlining heuristic decided to inline: " ++ show fn

6
src/Core/AutoSearch.idr
View File

@ -13,6 +13,8 @@ import Data.Either
import Data.List
import Data.Maybe
import Libraries.Data.WithDefault
%default covering
SearchEnv : List Name -> Type
@ -365,7 +367,7 @@ searchName : {vars : _} ->
searchName fc rigc defaults trying depth def top env target (n, ndef)
= do defs <- get Ctxt
when (not (visibleInAny (!getNS :: !getNestedNS)
(fullname ndef) (visibility ndef))) $
(fullname ndef) (collapseDefault $ visibility ndef))) $
throw (CantSolveGoal fc (gamma defs) [] top Nothing)
when (BlockedHint `elem` flags ndef) $
throw (CantSolveGoal fc (gamma defs) [] top Nothing)
@ -416,7 +418,7 @@ searchNames fc rigc defaults trying depth defining topty env ambig (n :: ns) tar
visible gam nspace n
= do Just def <- lookupCtxtExact n gam
| Nothing => pure Nothing
if visibleInAny nspace n (visibility def)
if visibleInAny nspace n (collapseDefault $ visibility def)
then pure $ Just (n, def)
else pure $ Nothing

16
src/Core/Binary/Prims.idr
View File

@ -15,6 +15,7 @@ import Libraries.Data.PosMap
import public Libraries.System.File.Meta as L -- Remove after release 0.7.0
import public Libraries.Utils.Binary
import public Libraries.Utils.String
import Libraries.Data.WithDefault
import System.Info
import System.File
@ -281,6 +282,21 @@ TTC a => TTC (Maybe a) where
pure (Just val)
_ => corrupt "Maybe"
export
TTC a => TTC (WithDefault a def) where
toBuf b def = onWithDefault
(tag 0)
(\v => do tag 1
toBuf b v)
def
fromBuf b
= case !getTag of
0 => pure defaulted
1 => do val <- fromBuf b
pure (specified val)
_ => corrupt "WithDefault"
export
(TTC a, TTC b) => TTC (Either a b) where
toBuf b (Left val)

17
src/Core/Context.idr
View File

@ -28,6 +28,7 @@ import Data.Nat
import Libraries.Data.NameMap
import Libraries.Data.StringMap
import Libraries.Data.UserNameMap
import Libraries.Data.WithDefault
import Libraries.Text.Distance.Levenshtein
import System.Clock
@ -319,11 +320,11 @@ commitCtxt ctxt
||| @rig quantity annotation
||| @vars local variables
||| @ty (closed) type
||| @vis Visibility
||| @vis Visibility, defaulting to private
||| @def actual definition
export
newDef : (fc : FC) -> (n : Name) -> (rig : RigCount) -> (vars : List Name) ->
(ty : ClosedTerm) -> (vis : Visibility) -> (def : Def) -> GlobalDef
(ty : ClosedTerm) -> (vis : WithDefault Visibility Private) -> (def : Def) -> GlobalDef
newDef fc n rig vars ty vis def
= MkGlobalDef
{ location = fc
@ -713,6 +714,7 @@ HasNames Warning where
full gam (UnreachableClause fc rho s) = UnreachableClause fc <$> full gam rho <*> full gam s
full gam (ShadowingGlobalDefs fc xs)
= ShadowingGlobalDefs fc <$> traverseList1 (traversePair (traverseList1 (full gam))) xs
full gam (IncompatibleVisibility fc x y n) = IncompatibleVisibility fc x y <$> full gam n
full gam w@(ShadowingLocalBindings _ _) = pure w
full gam (Deprecated fc x y) = Deprecated fc x <$> traverseOpt (traversePair (full gam)) y
full gam (GenericWarn fc x) = pure (GenericWarn fc x)
@ -721,6 +723,7 @@ HasNames Warning where
resolved gam (UnreachableClause fc rho s) = UnreachableClause fc <$> resolved gam rho <*> resolved gam s
resolved gam (ShadowingGlobalDefs fc xs)
= ShadowingGlobalDefs fc <$> traverseList1 (traversePair (traverseList1 (resolved gam))) xs
resolved gam (IncompatibleVisibility fc x y n) = IncompatibleVisibility fc x y <$> resolved gam n
resolved gam w@(ShadowingLocalBindings _ _) = pure w
resolved gam (Deprecated fc x y) = Deprecated fc x <$> traverseOpt (traversePair (resolved gam)) y
resolved gam (GenericWarn fc x) = pure (GenericWarn fc x)
@ -1132,7 +1135,7 @@ getSimilarNames nm = case show <$> userNameRoot nm of
| False => pure Nothing
Just def <- lookupCtxtExact nm (gamma defs)
| Nothing => pure Nothing -- should be impossible
pure (Just (visibility def, dist))
pure (Just (collapseDefault $ visibility def, dist))
kept <- NameMap.mapMaybeM @{CORE} test (resolvedAs (gamma defs))
pure $ Just (str, toList kept)
@ -1166,7 +1169,7 @@ showSimilarNames ns nm str kept
getVisibility : {auto c : Ref Ctxt Defs} ->
FC -> Name -> Core Visibility
FC -> Name -> Core (WithDefault Visibility Private)
getVisibility fc n
= do defs <- get Ctxt
Just def <- lookupCtxtExact n (gamma defs)
@ -1201,7 +1204,7 @@ ambiguousName : {auto c : Ref Ctxt Defs} -> FC
-> Name -> List Name
-> Core a
ambiguousName fc n ns = do
ns <- filterM (\x => pure $ !(getVisibility fc x) /= Private) ns
ns <- filterM (\x => pure $ !(collapseDefault <$> getVisibility fc x) /= Private) ns
case ns of
[] => undefinedName fc n
ns => throw $ AmbiguousName fc ns
@ -1329,7 +1332,7 @@ addBuiltin n ty tot op
, inferrable = []
, multiplicity = top
, localVars = []
, visibility = Public
, visibility = specified Public
, totality = tot
, isEscapeHatch = False
, flags = [Inline]
@ -1664,7 +1667,7 @@ setVisibility fc n vis
= do defs <- get Ctxt
Just def <- lookupCtxtExact n (gamma defs)
| Nothing => undefinedName fc n
ignore $ addDef n ({ visibility := vis } def)
ignore $ addDef n ({ visibility := specified vis } def)
public export
record SearchData where

3
src/Core/Context/Context.idr
View File

@ -14,6 +14,7 @@ import Libraries.Data.IntMap
import Libraries.Data.IOArray
import Libraries.Data.NameMap
import Libraries.Data.UserNameMap
import Libraries.Data.WithDefault
import Libraries.Utils.Binary
import Libraries.Utils.Scheme
@ -342,7 +343,7 @@ record GlobalDef where
inferrable : List Nat -- arguments which can be inferred from elsewhere in the type
multiplicity : RigCount
localVars : List Name -- environment name is defined in
visibility : Visibility
visibility : WithDefault Visibility Private
totality : Totality
isEscapeHatch : Bool
flags : List DefFlag

6
src/Core/Context/Data.idr
View File

@ -9,6 +9,8 @@ import Core.Normalise
import Data.List
import Data.Maybe
import Libraries.Data.WithDefault
%default covering
-- If a name appears more than once in an argument list, only the first is
@ -102,7 +104,7 @@ addData vars vis tidx (MkData (MkCon dfc tyn arity tycon) datacons)
log "declare.data.parameters" 20 $
"Positions of parameters for datatype" ++ show tyn ++
": [" ++ showSep ", " (map show paramPositions) ++ "]"
let tydef = newDef dfc tyn top vars tycon vis
let tydef = newDef dfc tyn top vars tycon (specified vis)
(TCon tag arity
paramPositions
allPos
@ -124,7 +126,7 @@ addData vars vis tidx (MkData (MkCon dfc tyn arity tycon) datacons)
Context -> Core Context
addDataConstructors tag [] gam = pure gam
addDataConstructors tag (MkCon fc n a ty :: cs) gam
= do let condef = newDef fc n top vars ty (conVisibility vis) (DCon tag a Nothing)
= do let condef = newDef fc n top vars ty (specified $ conVisibility vis) (DCon tag a Nothing)
-- Check 'n' is undefined
Nothing <- lookupCtxtExact n gam
| Just gdef => throw (AlreadyDefined fc n)

8
src/Core/Core.idr
View File

@ -66,6 +66,11 @@ data Warning : Type where
UnreachableClause : {vars : _} ->
FC -> Env Term vars -> Term vars -> Warning
ShadowingGlobalDefs : FC -> List1 (String, List1 Name) -> Warning
||| Soft-breaking change, make an error later.
||| @ original Originally declared visibility on forward decl
||| @ new Incompatible new visibility on actual declaration.
IncompatibleVisibility : FC -> (original : Visibility) ->
(new : Visibility) -> Name -> Warning
||| First FC is type
||| @ shadowed list of names which are shadowed,
||| where they originally appear
@ -204,6 +209,7 @@ Show Warning where
show (ParserWarning fc msg) = show fc ++ msg
show (UnreachableClause fc _ _) = show fc ++ ":Unreachable clause"
show (ShadowingGlobalDefs fc _) = show fc ++ ":Shadowing names"
show (IncompatibleVisibility fc _ _ _) = show fc ++ ":Incompatible Visibility"
show (ShadowingLocalBindings fc _) = show fc ++ ":Shadowing names"
show (Deprecated fc name _) = show fc ++ ":Deprecated " ++ name
show (GenericWarn fc msg) = show fc ++ msg
@ -395,6 +401,7 @@ getWarningLoc : Warning -> FC
getWarningLoc (ParserWarning fc _) = fc
getWarningLoc (UnreachableClause fc _ _) = fc
getWarningLoc (ShadowingGlobalDefs fc _) = fc
getWarningLoc (IncompatibleVisibility loc _ _ _) = loc
getWarningLoc (ShadowingLocalBindings fc _) = fc
getWarningLoc (Deprecated fc _ fcAndName) = fromMaybe fc (fst <$> fcAndName)
getWarningLoc (GenericWarn fc _) = fc
@ -483,6 +490,7 @@ killWarningLoc : Warning -> Warning
killWarningLoc (ParserWarning fc x) = ParserWarning emptyFC x
killWarningLoc (UnreachableClause fc x y) = UnreachableClause emptyFC x y
killWarningLoc (ShadowingGlobalDefs fc xs) = ShadowingGlobalDefs emptyFC xs
killWarningLoc (IncompatibleVisibility fc x y z) = IncompatibleVisibility emptyFC x y z
killWarningLoc (ShadowingLocalBindings fc xs) =
ShadowingLocalBindings emptyFC $ (\(n, _, _) => (n, emptyFC, emptyFC)) <$> xs
killWarningLoc (Deprecated fc x y) = Deprecated emptyFC x (map ((emptyFC,) . snd) y)

4
src/Core/Normalise/Eval.idr
View File

@ -15,6 +15,8 @@ import Data.Nat
import Data.String
import Data.Vect
import Libraries.Data.WithDefault
%default covering
-- A pair of a term and its normal form. This could be constructed either
@ -291,7 +293,7 @@ parameters (defs : Defs, topopts : EvalOpts)
let redok1 = evalAll topopts
let redok2 = reducibleInAny (currentNS defs :: nestedNS defs)
(fullname res)
(visibility res)
(collapseDefault $ visibility res)
-- want to shortcut that second check, if we're evaluating
-- everything, so don't let bind unless we need that log!
let redok = redok1 || redok2

23
src/Core/Reflect.idr
View File

@ -8,6 +8,8 @@ import Core.Normalise
import Core.TT
import Core.Value
import Libraries.Data.WithDefault
%default covering
public export
@ -292,6 +294,27 @@ Reflect a => Reflect (Maybe a) where
= do x' <- reflect fc defs lhs env x
appCon fc defs (preludetypes "Just") [Erased fc Placeholder, x']
export
Reify a => Reify (WithDefault a def) where
reify defs val@(NDCon _ n _ _ args)
= case (dropAllNS !(full (gamma defs) n), args) of
(UN (Basic "DefaultedValue"), _) => pure defaulted
(UN (Basic "SpecifiedValue"), [_, _, (_, x)])
=> do x' <- reify defs !(evalClosure defs x)
pure (specified x')
_ => cantReify val "WithDefault"
reify defs val = cantReify val "WithDefault"
export
Reflect a => Reflect (WithDefault a def) where
reflect fc defs lhs env def
= onWithDefault
(appCon fc defs (reflectionttimp "Default") [Erased fc Placeholder, Erased fc Placeholder])
(\x => do x' <- reflect fc defs lhs env x
appCon fc defs (reflectionttimp "Value") [Erased fc Placeholder, Erased fc Placeholder, x'])
def
export
(Reify a, Reify b) => Reify (a, b) where
reify defs val@(NDCon _ n _ _ [_, _, (_, x), (_, y)])

4
src/Core/SchemeEval/Compile.idr
View File

@ -24,6 +24,8 @@ import Data.List
import Libraries.Utils.Scheme
import System.Info
import Libraries.Data.WithDefault
schString : String -> String
schString s = concatMap okchar (unpack s)
where
@ -567,7 +569,7 @@ compileDef mode n_in
let redok = mode == EvalAll ||
reducibleInAny (currentNS defs :: nestedNS defs)
(fullname def)
(visibility def)
(collapseDefault $ visibility def)
-- 'n' is used in compileBody for generating names for readback,
-- and reading back resolved names is quicker because it's just
-- an integer

7
src/Core/TTC.idr
View File

@ -11,10 +11,11 @@ import Core.Name
import Core.Options
import Core.TT
import Libraries.Data.NameMap
import Libraries.Data.IOArray
import Data.Vect
import Libraries.Data.NameMap
import Libraries.Data.IOArray
import Libraries.Data.WithDefault
import Libraries.Utils.Binary
import Libraries.Utils.Scheme
@ -1149,7 +1150,7 @@ TTC GlobalDef where
mul vars vis
tot hatch fl refs refsR inv c True def cdef Nothing sc Nothing)
else pure (MkGlobalDef loc name (Erased loc Placeholder) [] [] [] []
mul [] Public unchecked False [] refs refsR
mul [] (specified Public) unchecked False [] refs refsR
False False True def cdef Nothing [] Nothing)
export

9
src/Core/UnifyState.idr
View File

@ -15,6 +15,7 @@ import Core.Value
import Data.List
import Libraries.Data.IntMap
import Libraries.Data.NameMap
import Libraries.Data.WithDefault
%default covering
@ -425,7 +426,7 @@ newMetaLets {vars} fc rig env n ty def nocyc lets
= do let hty = if lets then abstractFullEnvType fc env ty
else abstractEnvType fc env ty
let hole = { noCycles := nocyc }
(newDef fc n rig [] hty Public def)
(newDef fc n rig [] hty (specified Public) def)
log "unify.meta" 5 $ "Adding new meta " ++ show (n, fc, rig)
logTerm "unify.meta" 10 ("New meta type " ++ show n) hty
idx <- addDef n hole
@ -470,7 +471,7 @@ newConstant {vars} fc rig env tm ty constrs
= do let def = mkConstant fc env tm
let defty = abstractFullEnvType fc env ty
cn <- genName "postpone"
let guess = newDef fc cn rig [] defty Public
let guess = newDef fc cn rig [] defty (specified Public)
(Guess def (length env) constrs)
log "unify.constant" 5 $ "Adding new constant " ++ show (cn, fc, rig)
logTerm "unify.constant" 10 ("New constant type " ++ show cn) defty
@ -493,7 +494,7 @@ newSearch : {vars : _} ->
Env Term vars -> Name -> Term vars -> Core (Int, Term vars)
newSearch {vars} fc rig depth def env n ty
= do let hty = abstractEnvType fc env ty
let hole = newDef fc n rig [] hty Public (BySearch rig depth def)
let hole = newDef fc n rig [] hty (specified Public) (BySearch rig depth def)
log "unify.search" 10 $ "Adding new search " ++ show fc ++ " " ++ show n
logTermNF "unify.search" 10 "New search type" [] hty
idx <- addDef n hole
@ -514,7 +515,7 @@ newDelayed : {vars : _} ->
(ty : Term vars) -> Core (Int, Term vars)
newDelayed {vars} fc rig env n ty
= do let hty = abstractEnvType fc env ty
let hole = newDef fc n rig [] hty Public Delayed
let hole = newDef fc n rig [] hty (specified Public) Delayed
idx <- addDef n hole
log "unify.delay" 10 $ "Added delayed elaborator " ++ show (n, idx)
addHoleName fc n idx

5
src/Idris/Doc/Keywords.idr
View File

@ -137,6 +137,11 @@ visibility = vcat $
* `private` means that neither the declaration nor the definition will be
exported. This is the default and is the ideal setting for auxiliary
definitions.
""", "",
"""
If a forward-declaration for a definition exists, they cannot declare
incompatible visibility modifiers - they either have to match up or at most
one of the two can declare visibility.
"""]
ifthenelse : Doc IdrisDocAnn

10
src/Idris/Doc/String.idr
View File

@ -29,6 +29,7 @@ import Libraries.Data.SortedSet
import Libraries.Data.SortedMap
import Libraries.Data.StringMap as S
import Libraries.Data.String.Extra
import Libraries.Data.WithDefault
import public Libraries.Text.PrettyPrint.Prettyprinter
import public Libraries.Text.PrettyPrint.Prettyprinter.Util
@ -417,11 +418,12 @@ getDocsForName fc n config
| [ifacedata] => (Just "interface",) . pure <$> getIFaceDoc ifacedata
| _ => pure (Nothing, []) -- shouldn't happen, we've resolved ambiguity by now
case definition d of
PMDef _ _ _ _ _ => pure (Nothing, catMaybes [ showTotal (totality d)
, pure (showVisible (visibility d))])
PMDef _ _ _ _ _ => pure ( Nothing
, catMaybes [ showTotal (totality d)
, pure (showVisible (collapseDefault $ visibility d))])
TCon _ _ _ _ _ _ cons _ =>
do let tot = catMaybes [ showTotal (totality d)
, pure (showVisible (visibility d))]
, pure (showVisible (collapseDefault $ visibility d))]
cdocs <- traverse (getDConDoc <=< toFullNames) cons
cdoc <- case cdocs of
[] => pure (Just "data", [])
@ -697,7 +699,7 @@ getContents ns
visible defs n
= do Just def <- lookupCtxtExact n (gamma defs)
| Nothing => pure False
pure (visibility def /= Private)
pure (collapseDefault (visibility def) /= Private)
inNS : Name -> Bool
inNS (NS xns (UN _)) = ns `isParentOf` xns

21
src/Idris/Elab/Interface.idr
View File

@ -22,6 +22,7 @@ import TTImp.Utils
import Libraries.Data.ANameMap
import Libraries.Data.List.Extra
import Data.List
import Libraries.Data.WithDefault
%default covering
@ -104,11 +105,11 @@ mkDataTy fc ((n, (_, ty)) :: ps)
mkIfaceData : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
FC -> Visibility -> Env Term vars ->
FC -> WithDefault Visibility Private -> Env Term vars ->
List (Maybe Name, RigCount, RawImp) ->
Name -> Name -> List (Name, (RigCount, RawImp)) ->
List Name -> List (Name, RigCount, RawImp) -> Core ImpDecl
mkIfaceData {vars} ifc vis env constraints n conName ps dets meths
mkIfaceData {vars} ifc def_vis env constraints n conName ps dets meths
= let opts = if isNil dets
then [NoHints, UniqueSearch]
else [NoHints, UniqueSearch, SearchBy dets]
@ -119,7 +120,7 @@ mkIfaceData {vars} ifc vis env constraints n conName ps dets meths
con = MkImpTy vfc EmptyFC conName !(bindTypeNames ifc [] (pNames ++ map fst meths ++ vars) conty)
bound = pNames ++ map fst meths ++ vars in
pure $ IData vfc vis Nothing {- ?? -}
pure $ IData vfc def_vis Nothing {- ?? -}
$ MkImpData vfc n
(Just !(bindTypeNames ifc [] bound (mkDataTy vfc ps)))
opts [con]
@ -333,7 +334,7 @@ elabInterface : {vars : _} ->
{auto s : Ref Syn SyntaxInfo} ->
{auto m : Ref MD Metadata} ->
{auto o : Ref ROpts REPLOpts} ->
FC -> Visibility ->
FC -> WithDefault Visibility Private ->
Env Term vars -> NestedNames vars ->
(constraints : List (Maybe Name, RawImp)) ->
Name ->
@ -342,7 +343,7 @@ elabInterface : {vars : _} ->
(conName : Maybe (String, Name)) ->
List ImpDecl ->
Core ()
elabInterface {vars} ifc vis env nest constraints iname params dets mcon body
elabInterface {vars} ifc def_vis env nest constraints iname params dets mcon body
= do fullIName <- getFullName iname
ns_iname <- inCurrentNS fullIName
let conName_in = maybe (mkCon vfc fullIName) snd mcon
@ -396,7 +397,7 @@ elabInterface {vars} ifc vis env nest constraints iname params dets mcon body
consts <- traverse (getMethDecl env nest params meth_names . (top,)) constraints
log "elab.interface" 5 $ "Constraints: " ++ show consts
dt <- mkIfaceData vfc vis env consts iname conName params
dt <- mkIfaceData vfc def_vis env consts iname conName params
dets meths
log "elab.interface" 10 $ "Methods: " ++ show meths
log "elab.interface" 5 $ "Making interface data type " ++ show dt
@ -407,7 +408,8 @@ elabInterface {vars} ifc vis env nest constraints iname params dets mcon body
Core ()
elabMethods conName meth_names meth_sigs
= do -- Methods have same visibility as data declaration
fnsm <- traverse (getMethToplevel env vis iname conName
fnsm <- traverse (getMethToplevel env (collapseDefault def_vis)
iname conName
(map fst constraints)
meth_names
params) meth_sigs
@ -452,7 +454,7 @@ elabInterface {vars} ifc vis env nest constraints iname params dets mcon body
dty_imp <- bindTypeNames dfc [] (map name tydecls ++ vars) dty
log "elab.interface.default" 5 $ "Default method " ++ show dn ++ " : " ++ show dty_imp
let dtydecl = IClaim vdfc rig vis [] (MkImpTy EmptyFC EmptyFC dn dty_imp)
let dtydecl = IClaim vdfc rig (collapseDefault def_vis) [] (MkImpTy EmptyFC EmptyFC dn dty_imp)
processDecl [] nest env dtydecl
@ -516,7 +518,8 @@ elabInterface {vars} ifc vis env nest constraints iname params dets mcon body
Core ()
elabConstraintHints conName meth_names
= do let nconstraints = nameCons 0 constraints
chints <- traverse (getConstraintHint vfc env vis iname conName
chints <- traverse (getConstraintHint vfc env (collapseDefault def_vis)
iname conName
(map fst nconstraints)
meth_names
paramNames) nconstraints

9
src/Idris/Error.idr
View File

@ -33,6 +33,8 @@ Eq Warning where
ParserWarning fc1 x1 == ParserWarning fc2 x2 = fc1 == fc2 && x1 == x2
UnreachableClause fc1 rho1 s1 == UnreachableClause fc2 rho2 s2 = fc1 == fc2
ShadowingGlobalDefs fc1 xs1 == ShadowingGlobalDefs fc2 xs2 = fc1 == fc2 && xs1 == xs2
IncompatibleVisibility fc1 x1 y1 n1 == IncompatibleVisibility fc2 x2 y2 n2
= fc1 == fc2 && x1 == x2 && y1 == y2 && n1 == n2
Deprecated fc1 x1 y1 == Deprecated fc2 x2 y2 = fc1 == fc2 && x1 == x2 && y1 == y2
GenericWarn fc1 x1 == GenericWarn fc2 x2 = fc1 == fc2 && x1 == x2
_ == _ = False
@ -274,6 +276,13 @@ pwarningRaw (ShadowingGlobalDefs fc ns)
:: reflow "is shadowing"
:: punctuate comma (map pretty0 (forget ns))
pwarningRaw (IncompatibleVisibility fc vx vy n)
= pure $ warning (code (pretty0 (sugarName n))
<++> reflow "has been forward-declared with"
<++> keyword (pretty0 vx) <++> reflow "visibility, cannot change to"
<++> keyword (pretty0 vy) <+> reflow ". This will be an error in a later release.")
<+> line <+> !(ploc fc)
pwarningRaw (ShadowingLocalBindings fc ns)
= pure $ vcat
[ reflow "You may be unintentionally shadowing the following local bindings:"

3
src/Idris/Package.idr
View File

@ -26,6 +26,7 @@ import System.File
import Libraries.Data.SortedMap
import Libraries.Data.StringMap
import Libraries.Data.StringTrie
import Libraries.Data.WithDefault
import Libraries.Text.Parser
import Libraries.Utils.Path
import Libraries.Text.PrettyPrint.Prettyprinter.Render.String
@ -756,7 +757,7 @@ makeDoc pkg opts =
visible : GlobalDef -> Bool
visible def = case definition def of
(DCon _ _ _) => False
_ => (visibility def /= Private)
_ => (collapseDefault (visibility def) /= Private)
fileError : String -> FileError -> Core (List Error)
fileError filename err = pure [FileErr filename err]

17
src/Idris/Parser.idr
View File

@ -19,6 +19,7 @@ import Data.Nat
import Data.SnocList
import Data.String
import Libraries.Utils.String
import Libraries.Data.WithDefault
import Idris.Parser.Let
@ -1125,11 +1126,12 @@ visOption fname
<|> (decoratedKeyword fname "private" $> Private)
exportVisibility, visibility : OriginDesc -> EmptyRule Visibility
visibility : OriginDesc -> EmptyRule (WithDefault Visibility Private)
visibility fname
= visOption fname
<|> pure Private
= (specified <$> visOption fname)
<|> pure defaulted
exportVisibility : OriginDesc -> EmptyRule Visibility
exportVisibility fname
= visOption fname
<|> pure Export
@ -1327,11 +1329,11 @@ dataDeclBody fname indents
simpleData fname b n indents <|> gadtData fname col b n indents
-- a data declaration can have a visibility and an optional totality (#1404)
dataVisOpt : OriginDesc -> EmptyRule (Visibility, Maybe TotalReq)
dataVisOpt : OriginDesc -> EmptyRule (WithDefault Visibility Private, Maybe TotalReq)
dataVisOpt fname
= do { vis <- visOption fname ; mbtot <- optional (totalityOpt fname) ; pure (vis, mbtot) }
= do { vis <- visOption fname ; mbtot <- optional (totalityOpt fname) ; pure (specified vis, mbtot) }
<|> do { tot <- totalityOpt fname ; vis <- visibility fname ; pure (vis, Just tot) }
<|> pure (Private, Nothing)
<|> pure (defaulted, Nothing)
dataDecl : OriginDesc -> IndentInfo -> Rule PDecl
dataDecl fname indents
@ -1747,7 +1749,8 @@ recordParam fname indents
-- A record without a where is a forward declaration
recordBody : OriginDesc -> IndentInfo ->
String -> Visibility -> Maybe TotalReq ->
String -> WithDefault Visibility Private ->
Maybe TotalReq ->
Int ->
Name ->
List (Name, RigCount, PiInfo PTerm, PTerm) ->

5
src/Idris/REPL.idr
View File

@ -71,6 +71,7 @@ import Data.String
import Libraries.Data.List.Extra
import Libraries.Data.String.Extra
import Libraries.Data.Tap
import Libraries.Data.WithDefault
import Libraries.Text.PrettyPrint.Prettyprinter.Util
import Libraries.Utils.Path
import Libraries.System.Directory.Tree
@ -898,7 +899,7 @@ process (Eval itm)
let norm = replEval emode
evalResultName <- DN "it" <$> genName "evalResult"
ignore $ addDef evalResultName
$ newDef replFC evalResultName top [] ty Private
$ newDef replFC evalResultName top [] ty defaulted
$ PMDef defaultPI [] (STerm 0 ntm) (STerm 0 ntm) []
addToSave evalResultName
put ROpts ({ evalResultName := Just evalResultName } opts)
@ -989,7 +990,7 @@ process (TypeSearch searchTerm)
defs <- traverse (flip lookupCtxtExact ctxt) names
let defs = flip mapMaybe defs $ \ md =>
do d <- md
guard (visibleIn curr (fullname d) (visibility d))
guard (visibleIn curr (fullname d) (collapseDefault $ visibility d))
guard (isJust $ userNameRoot (fullname d))
pure d
allDefs <- traverse (resolved ctxt) defs

3
src/Idris/REPL/FuzzySearch.idr
View File

@ -17,6 +17,7 @@ import Data.Maybe
import Data.String
import Libraries.Data.List.Extra
import Libraries.Data.String.Extra
import Libraries.Data.WithDefault
%default covering
@ -49,7 +50,7 @@ fuzzySearch expr = do
defs <- traverse (flip lookupCtxtExact ctxt) names
let defs = flip mapMaybe defs $ \ md =>
do d <- md
guard (visibleIn curr (fullname d) (visibility d))
guard (visibleIn curr (fullname d) (collapseDefault $ visibility d))
guard (isJust $ userNameRoot (fullname d))
pure d
allDefs <- traverse (resolved ctxt) defs

9
src/Idris/Syntax.idr
View File

@ -22,6 +22,7 @@ import Libraries.Data.NameMap
import Libraries.Data.SortedMap
import Libraries.Data.String.Extra
import Libraries.Data.StringMap
import Libraries.Data.WithDefault
import Libraries.Text.PrettyPrint.Prettyprinter
import Parser.Lexer.Source
@ -428,14 +429,15 @@ mutual
data PDecl' : Type -> Type where
PClaim : FC -> RigCount -> Visibility -> List (PFnOpt' nm) -> PTypeDecl' nm -> PDecl' nm
PDef : FC -> List (PClause' nm) -> PDecl' nm
PData : FC -> (doc : String) -> Visibility -> Maybe TotalReq -> PDataDecl' nm -> PDecl' nm
PData : FC -> (doc : String) -> WithDefault Visibility Private ->
Maybe TotalReq -> PDataDecl' nm -> PDecl' nm
PParameters : FC ->
List (Name, RigCount, PiInfo (PTerm' nm), PTerm' nm) ->
List (PDecl' nm) -> PDecl' nm
PUsing : FC -> List (Maybe Name, PTerm' nm) ->
List (PDecl' nm) -> PDecl' nm
PInterface : FC ->
Visibility ->
WithDefault Visibility Private ->
(constraints : List (Maybe Name, PTerm' nm)) ->
Name ->
(doc : String) ->
@ -456,7 +458,8 @@ mutual
PDecl' nm
PRecord : FC ->
(doc : String) ->
Visibility -> Maybe TotalReq ->
WithDefault Visibility Private ->
Maybe TotalReq ->
PRecordDecl' nm ->
PDecl' nm

74
src/Libraries/Data/WithDefault.idr Normal file
View File

@ -0,0 +1,74 @@
module Libraries.Data.WithDefault
export
data WithDefault : (0 a : Type) -> (0 def : a) -> Type where
DefaultedValue : WithDefault a def
SpecifiedValue : a -> WithDefault a def
export
specified : a -> WithDefault a def
specified = SpecifiedValue
export
defaulted : WithDefault a def
defaulted = DefaultedValue
export
specifyValue : a -> WithDefault a def -> WithDefault a def
specifyValue v DefaultedValue = SpecifiedValue v
specifyValue _ v = v
export
replaceSpecified : WithDefault a def -> WithDefault a def'
replaceSpecified DefaultedValue = DefaultedValue
replaceSpecified (SpecifiedValue v) = SpecifiedValue v
export
collapseDefault : {def : a} -> WithDefault a def -> a
collapseDefault DefaultedValue = def
collapseDefault (SpecifiedValue v) = v
export
onWithDefault : (defHandler : Lazy b) ->
(valHandler : a -> b) ->
WithDefault a def ->
b
onWithDefault defHandler _ DefaultedValue = defHandler
onWithDefault _ valHandler (SpecifiedValue v) = valHandler v
export
collapseDefaults : Eq a =>
{def : a} ->
WithDefault a def ->
WithDefault a def ->
Either (a, a) a
collapseDefaults (SpecifiedValue x) (SpecifiedValue y) = if x /= y
then Left (x, y)
else Right x
collapseDefaults (SpecifiedValue x) DefaultedValue = Right x
collapseDefaults DefaultedValue (SpecifiedValue y) = Right y
collapseDefaults DefaultedValue DefaultedValue = Right def
export
isDefaulted : WithDefault a def -> Bool
isDefaulted DefaultedValue = True
isDefaulted _ = False
export
isSpecified : WithDefault a def -> Bool
isSpecified DefaultedValue = False
isSpecified _ = True
public export
Eq a => Eq (WithDefault a def) where
DefaultedValue == DefaultedValue = True
DefaultedValue == SpecifiedValue _ = False
SpecifiedValue _ == DefaultedValue = False
SpecifiedValue x == SpecifiedValue y = x == y
public export
Ord a => Ord (WithDefault a def) where
compare DefaultedValue DefaultedValue = EQ
compare DefaultedValue (SpecifiedValue _) = LT
compare (SpecifiedValue _) DefaultedValue = GT
compare (SpecifiedValue x) (SpecifiedValue y) = compare x y

3
src/TTImp/Elab/Ambiguity.idr
View File

@ -23,6 +23,7 @@ import Data.String
import Data.Vect
import Libraries.Data.UserNameMap
import Libraries.Data.WithDefault
%default covering
@ -85,7 +86,7 @@ expandAmbigName mode nest env orig args (IVar fc x) exp
| _ => pure True
if !(isVisible ns)
then pure $ visibleInAny (!getNS :: !getNestedNS) (NS ns x)
(visibility def)
(collapseDefault $ visibility def)
else pure False
-- If there's multiple alternatives and all else fails, resort to using

6
src/TTImp/Elab/App.idr
View File

@ -20,6 +20,8 @@ import TTImp.TTImp
import Data.List
import Data.Maybe
import Libraries.Data.WithDefault
%default covering
checkVisibleNS : {auto c : Ref Ctxt Defs} ->
@ -71,7 +73,7 @@ getNameType elabMode rigc env fc x
do defs <- get Ctxt
[(pname, i, def)] <- lookupCtxtName x (gamma defs)
| ns => ambiguousName fc x (map fst ns)
checkVisibleNS fc (fullname def) (visibility def)
checkVisibleNS fc (fullname def) (collapseDefault $ visibility def)
when (not $ onLHS elabMode) $
checkDeprecation fc def
rigSafe (multiplicity def) rigc
@ -126,7 +128,7 @@ getVarType elabMode rigc nest env fc x
tm = tmf fc nt
tyenv = useVars (getArgs tm)
(embed (type ndef)) in
do checkVisibleNS fc (fullname ndef) (visibility ndef)
do checkVisibleNS fc (fullname ndef) (collapseDefault $ visibility ndef)
logTerm "elab" 5 ("Type of " ++ show n') tyenv
logTerm "elab" 5 ("Expands to") tm
log "elab" 5 $ "Arg length " ++ show arglen

5
src/TTImp/Elab/Case.idr
View File

@ -26,6 +26,7 @@ import Data.List
import Data.Maybe
import Data.String
import Libraries.Data.NameMap
import Libraries.Data.WithDefault
%default covering
@ -192,9 +193,9 @@ caseBlock {vars} rigc elabinfo fc nest env opts scr scrtm scrty caseRig alts exp
let env = updateMults (linearUsed est) env
defs <- get Ctxt
parentDef <- lookupCtxtExact (Resolved (defining est)) (gamma defs)
let vis = case parentDef of
let vis = specified $ case parentDef of
Just gdef =>
if visibility gdef == Public
if collapseDefault (visibility gdef) == Public
then Public
else Private
Nothing => Public

7
src/TTImp/Elab/Check.idr
View File

@ -20,11 +20,12 @@ import Idris.Syntax
import TTImp.TTImp
import Data.Either
import Libraries.Data.IntMap
import Data.List
import Libraries.Data.NameMap
import Data.SnocList
import Libraries.Data.IntMap
import Libraries.Data.NameMap
import Libraries.Data.UserNameMap
import Libraries.Data.WithDefault
%default covering
@ -411,7 +412,7 @@ uniVar : {auto c : Ref Ctxt Defs} ->
FC -> Core Name
uniVar fc
= do n <- genName "u"
idx <- addDef n (newDef fc n erased [] (Erased fc Placeholder) Public None)
idx <- addDef n (newDef fc n erased [] (Erased fc Placeholder) (specified Public) None)
pure (Resolved idx)
export

7
src/TTImp/Elab/Local.idr
View File

@ -17,6 +17,7 @@ import TTImp.TTImp
import Libraries.Data.NameMap
import Data.List
import Libraries.Data.WithDefault
%default covering
@ -36,7 +37,7 @@ localHelper {vars} nest env nestdecls_in func
let f = defining est
defs <- get Ctxt
gdef <- lookupCtxtExact (Resolved (defining est)) (gamma defs)
let vis = maybe Public visibility gdef
let vis = maybe Public (collapseDefault . visibility) gdef
let mult = maybe linear GlobalDef.multiplicity gdef
-- If the parent function is public, the nested definitions need
@ -143,8 +144,8 @@ localHelper {vars} nest env nestdecls_in func
setPublic : ImpDecl -> ImpDecl
setPublic (IClaim fc c _ opts ty) = IClaim fc c Public opts ty
setPublic (IData fc _ mbt d) = IData fc Public mbt d
setPublic (IRecord fc c _ mbt r) = IRecord fc c Public mbt r
setPublic (IData fc _ mbt d) = IData fc (specified Public) mbt d
setPublic (IRecord fc c _ mbt r) = IRecord fc c (specified Public) mbt r
setPublic (IParameters fc ps decls)
= IParameters fc ps (map setPublic decls)
setPublic (INamespace fc ps decls)

4
src/TTImp/Interactive/Completion.idr
View File

@ -9,6 +9,8 @@ import Idris.Parser
import Data.String
import Libraries.Data.WithDefault
||| Completion tasks are varied:
||| are we trying to fill in a name, a REPL command, a pragma?
data Task
@ -55,7 +57,7 @@ nameCompletion pref = do
-- and it better be visible
Just def <- lookupCtxtExact nsn (gamma defs)
| Nothing => pure Nothing
let True = visibleIn cns nsn (visibility def)
let True = visibleIn cns nsn (collapseDefault $ visibility def)
| False => pure Nothing
pure (Just n)
pure (map show $ nub nms)

5
src/TTImp/Interactive/ExprSearch.idr
View File

@ -35,6 +35,7 @@ import TTImp.Utils
import Data.List
import Libraries.Data.Tap
import Libraries.Data.WithDefault
%default covering
@ -283,7 +284,7 @@ searchName fc rigc opts hints env target topty (n, ndef)
= do defs <- get Ctxt
checkTimer
let True = visibleInAny (!getNS :: !getNestedNS)
(fullname ndef) (visibility ndef)
(fullname ndef) (collapseDefault $ visibility ndef)
| _ => noResult
let ty = type ndef
let True = usableName (fullname ndef)
@ -365,7 +366,7 @@ searchNames fc rig opts hints env ty topty (n :: ns)
visible gam nspace n
= do Just def <- lookupCtxtExact n gam
| Nothing => pure Nothing
if visibleInAny nspace n (visibility def)
if visibleInAny nspace n (collapseDefault $ visibility def)
then pure (Just (n, def))
else pure Nothing

13
src/TTImp/Parser.idr
View File

@ -8,6 +8,7 @@ import TTImp.TTImp
import public Libraries.Text.Parser
import Data.List
import Data.List1
import Libraries.Data.WithDefault
topDecl : OriginDesc -> IndentInfo -> Rule ImpDecl
-- All the clauses get parsed as one-clause definitions. Collect any
@ -76,10 +77,10 @@ visOption
<|> do keyword "private"
pure Private
visibility : EmptyRule Visibility
visibility : EmptyRule (WithDefault Visibility Private)
visibility
= visOption
<|> pure Private
= (specified <$> visOption)
<|> pure defaulted
totalityOpt : Rule TotalReq
totalityOpt
@ -90,11 +91,11 @@ totalityOpt
<|> do keyword "covering"
pure CoveringOnly
dataVisOpt : EmptyRule (Visibility, Maybe TotalReq)
dataVisOpt : EmptyRule (WithDefault Visibility Private, Maybe TotalReq)
dataVisOpt
= do { vis <- visOption ; mbtot <- optional totalityOpt ; pure (vis, mbtot) }
= do { vis <- visOption ; mbtot <- optional totalityOpt ; pure (specified vis, mbtot) }
<|> do { tot <- totalityOpt ; vis <- visibility ; pure (vis, Just tot) }
<|> pure (Private, Nothing)
<|> pure (defaulted, Nothing)
fnOpt : Rule FnOpt
fnOpt = do x <- totalityOpt

3
src/TTImp/PartialEval.idr
View File

@ -23,6 +23,7 @@ import Protocol.Hex
import Data.List
import Libraries.Data.NameMap
import Libraries.Data.WithDefault
%default covering
@ -281,7 +282,7 @@ mkSpecDef {vars} fc gdef pename sargs fn stk
log "specialise.flags" 20 "Defining \{show pename} with flags: \{show defflags}"
peidx <- addDef pename
$ the (GlobalDef -> GlobalDef) { flags := defflags }
$ newDef fc pename top [] sty Public None
$ newDef fc pename top [] sty (specified Public) None
addToSave (Resolved peidx)
-- Reduce the function to be specialised, and reduce any name in

29
src/TTImp/ProcessData.idr
View File

@ -24,6 +24,7 @@ import TTImp.TTImp
import Data.DPair
import Data.List
import Libraries.Data.NameMap
import Libraries.Data.WithDefault
%default covering
@ -400,9 +401,9 @@ processData : {vars : _} ->
{auto o : Ref ROpts REPLOpts} ->
List ElabOpt -> NestedNames vars ->
Env Term vars -> FC ->
Visibility -> Maybe TotalReq ->
WithDefault Visibility Private -> Maybe TotalReq ->
ImpData -> Core ()
processData {vars} eopts nest env fc vis mbtot (MkImpLater dfc n_in ty_raw)
processData {vars} eopts nest env fc def_vis mbtot (MkImpLater dfc n_in ty_raw)
= do n <- inCurrentNS n_in
ty_raw <- bindTypeNames fc [] vars ty_raw
@ -424,7 +425,7 @@ processData {vars} eopts nest env fc vis mbtot (MkImpLater dfc n_in ty_raw)
arity <- getArity defs [] fullty
-- Add the type constructor as a placeholder
tidx <- addDef n (newDef fc n linear vars fullty vis
tidx <- addDef n (newDef fc n linear vars fullty def_vis
(TCon 0 arity [] [] defaultFlags [] [] Nothing))
addMutData (Resolved tidx)
defs <- get Ctxt
@ -434,13 +435,13 @@ processData {vars} eopts nest env fc vis mbtot (MkImpLater dfc n_in ty_raw)
addToSave n
log "declare.data" 10 $ "Saving from " ++ show n ++ ": " ++ show (keys (getMetas ty))
case vis of
case collapseDefault def_vis of
Private => pure ()
_ => do addHashWithNames n
addHashWithNames fullty
log "module.hash" 15 "Adding hash for data declaration with name \{show n}"
processData {vars} eopts nest env fc vis mbtot (MkImpData dfc n_in mty_raw opts cons_raw)
processData {vars} eopts nest env fc def_vis mbtot (MkImpData dfc n_in mty_raw opts cons_raw)
= do n <- inCurrentNS n_in
log "declare.data" 1 $ "Processing " ++ show n
@ -462,17 +463,23 @@ processData {vars} eopts nest env fc vis mbtot (MkImpData dfc n_in mty_raw opts
let metas = maybe empty fst mmetasfullty
let mfullty = map snd mmetasfullty
-- If n exists, check it's the same type as we have here, and is
-- a data constructor.
-- If n exists, check it's the same type as we have here, is
-- a type constructor, and has either the same visibility or we don't define one.
-- When looking up, note the data types which were undefined at the
-- point of declaration.
ndefm <- lookupCtxtExact n (gamma defs)
(mw, vis, fullty) <- the (Core (List Name, Visibility, ClosedTerm)) $ case ndefm of
Nothing => case mfullty of
Nothing => throw (GenericMsg fc "Missing telescope for data definition \{show n_in}")
Just fullty => pure ([], vis, fullty)
Just ndef =>
let vis = max (visibility ndef) vis in
Just fullty => pure ([], collapseDefault def_vis, fullty)
Just ndef => do
vis <- the (Core Visibility) $ case collapseDefaults ndef.visibility def_vis of
Right finalVis => pure finalVis
Left (oldVis, newVis) => do
-- TODO : In a later release, replace this with an error.
recordWarning (IncompatibleVisibility fc oldVis newVis n)
pure (max oldVis newVis)
case definition ndef of
TCon _ _ _ _ _ mw [] _ => case mfullty of
Nothing => pure (mw, vis, type ndef)
@ -490,7 +497,7 @@ processData {vars} eopts nest env fc vis mbtot (MkImpData dfc n_in mty_raw opts
-- Add the type constructor as a placeholder while checking
-- data constructors
tidx <- addDef n (newDef fc n linear vars fullty vis
tidx <- addDef n (newDef fc n linear vars fullty (specified vis)
(TCon 0 arity [] [] defaultFlags [] [] Nothing))
case vis of
Private => pure ()

17
src/TTImp/ProcessDef.idr
View File

@ -36,9 +36,10 @@ import TTImp.WithClause
import Data.Either
import Data.List
import Libraries.Data.NameMap
import Data.String
import Data.Maybe
import Libraries.Data.NameMap
import Libraries.Data.WithDefault
import Libraries.Text.PrettyPrint.Prettyprinter
%default covering
@ -587,7 +588,7 @@ checkClause {vars} mult vis totreq hashit n opts nest env
wname <- genWithName !(prettyName !(toFullNames (Resolved n)))
widx <- addDef wname ({flags $= (SetTotal totreq ::)}
(newDef vfc wname (if isErased mult then erased else top)
vars wtype vis None))
vars wtype (specified vis) None))
let toWarg : Maybe (PiInfo RawImp, Name) -> List (Maybe Name, RawImp)
:= flip maybe (\pn => [(Nothing, IVar vfc (snd pn))]) $
@ -940,12 +941,12 @@ lookupOrAddAlias eopts nest env fc n [cl@(PatClause _ lhs _)]
Just (str, kept) <- getSimilarNames n
| Nothing => pure []
-- only keep the ones that haven't been defined yet
decls <- for kept $ \ (cand, weight) => do
decls <- for kept $ \ (cand, vis, weight) => do
Just gdef <- lookupCtxtExact cand (gamma defs)
| Nothing => pure Nothing -- should be impossible
let None = definition gdef
| _ => pure Nothing
pure (Just (cand, weight))
pure (Just (cand, vis, weight))
pure $ showSimilarNames (currentNS defs) n str $ catMaybes decls
| (x :: xs) => throw (MaybeMisspelling (NoDeclaration fc n) (x ::: xs))
-- 3) declare an alias
@ -988,7 +989,7 @@ processDef opts nest env fc n_in cs_in
-- should include the definition (RHS) of anything that is public (available
-- at compile time for elaboration) _or_ inlined (dropped into destination definitions
-- during compilation).
let hashit = visibility gdef == Public || (Inline `elem` gdef.flags)
let hashit = (collapseDefault $ visibility gdef) == Public || (Inline `elem` gdef.flags)
let mult = if isErased (multiplicity gdef)
then erased
else linear
@ -999,7 +1000,7 @@ processDef opts nest env fc n_in cs_in
log "declare.def" 5 $ "Traversing clauses of " ++ show n ++ " with mult " ++ show mult
let treq = fromMaybe !getDefaultTotalityOption (findSetTotal (flags gdef))
cs <- withTotality treq $
traverse (checkClause mult (visibility gdef) treq
traverse (checkClause mult (collapseDefault $ visibility gdef) treq
hashit nidx opts nest env) cs_in
let pats = map toPats (rights cs)
@ -1026,11 +1027,11 @@ processDef opts nest env fc n_in cs_in
({ definition := PMDef pi cargs tree_ct tree_ct pats
} gdef)
when (visibility gdef == Public) $
when (collapseDefault (visibility gdef) == Public) $
do let rmetas = getMetas tree_ct
log "declare.def" 10 $ "Saving from " ++ show n ++ ": " ++ show (keys rmetas)
traverse_ addToSave (keys rmetas)
when (isUserName n && visibility gdef /= Private) $
when (isUserName n && collapseDefault (visibility gdef) /= Private) $
do let tymetas = getMetas (type gdef)
traverse_ addToSave (keys tymetas)
addToSave n

19
src/TTImp/ProcessRecord.idr
View File

@ -18,6 +18,8 @@ import TTImp.TTImp.Traversals
import TTImp.Unelab
import TTImp.Utils
import Libraries.Data.WithDefault
import Data.List
import Data.String
@ -43,13 +45,14 @@ elabRecord : {vars : _} ->
{auto o : Ref ROpts REPLOpts} ->
List ElabOpt -> FC -> Env Term vars ->
NestedNames vars -> Maybe String ->
Visibility -> Maybe TotalReq -> Name ->
WithDefault Visibility Private ->
Maybe TotalReq -> Name ->
(params : List (Name, RigCount, PiInfo RawImp, RawImp)) ->
(opts : List DataOpt) ->
(conName : Name) ->
List IField ->
Core ()
elabRecord {vars} eopts fc env nest newns vis mbtot tn_in params0 opts conName_in fields
elabRecord {vars} eopts fc env nest newns def_vis mbtot tn_in params0 opts conName_in fields
= do tn <- inCurrentNS tn_in
conName <- inCurrentNS conName_in
params <- preElabAsData tn
@ -145,7 +148,7 @@ elabRecord {vars} eopts fc env nest newns vis mbtot tn_in params0 opts conName_i
-- we don't use MkImpLater because users may have already declared the record ahead of time
let dt = MkImpData fc tn (Just dataTy) opts []
log "declare.record" 10 $ "Pre-declare record data type: \{show dt}"
processDecl [] nest env (IData fc vis mbtot dt)
processDecl [] nest env (IData fc def_vis mbtot dt)
defs <- get Ctxt
Just ty <- lookupTyExact tn (gamma defs)
| Nothing => throw (InternalError "Missing data type \{show tn}, despite having just declared it!")
@ -221,7 +224,7 @@ elabRecord {vars} eopts fc env nest newns vis mbtot tn_in params0 opts conName_i
!(bindTypeNames fc [] boundNames conty)
let dt = MkImpData fc tn Nothing opts [con]
log "declare.record" 5 $ "Record data type " ++ show dt
processDecl [] nest env (IData fc vis mbtot dt)
processDecl [] nest env (IData fc def_vis mbtot dt)
countExp : Term vs -> Nat
countExp (Bind _ _ (Pi _ _ Explicit _) sc) = S (countExp sc)
@ -245,7 +248,7 @@ elabRecord {vars} eopts fc env nest newns vis mbtot tn_in params0 opts conName_i
Core ()
elabGetters tn con params done upds tyenv (Bind bfc n b@(Pi _ rc imp ty_chk) sc)
= let rig = if isErased rc then erased else top
isVis = projVis vis
isVis = projVis (collapseDefault def_vis)
in if (n `elem` map fst params) || (n `elem` vars)
then elabGetters tn con params
(if imp == Explicit && not (n `elem` vars)
@ -339,7 +342,7 @@ processRecord : {vars : _} ->
{auto o : Ref ROpts REPLOpts} ->
List ElabOpt -> NestedNames vars ->
Env Term vars -> Maybe String ->
Visibility -> Maybe TotalReq ->
WithDefault Visibility Private -> Maybe TotalReq ->
ImpRecord -> Core ()
processRecord eopts nest env newns vis mbtot (MkImpRecord fc n ps opts cons fs)
= do elabRecord eopts fc env nest newns vis mbtot n ps opts cons fs
processRecord eopts nest env newns def_vis mbtot (MkImpRecord fc n ps opts cons fs)
= do elabRecord eopts fc env nest newns def_vis mbtot n ps opts cons fs

3
src/TTImp/ProcessType.idr
View File

@ -25,6 +25,7 @@ import Data.List1
import Data.String
import Libraries.Data.NameMap
import Libraries.Data.StringMap
import Libraries.Data.WithDefault
%default covering
@ -177,7 +178,7 @@ processType {vars} eopts nest env fc rig vis opts (MkImpTy tfc nameFC n_in ty_ra
({ eraseArgs := erased,
safeErase := dterased,
inferrable := infargs }
(newDef fc n rig vars fullty vis def))
(newDef fc n rig vars fullty (specified vis) def))
-- Flag it as checked, because we're going to check the clauses
-- from the top level.
-- But, if it's a case block, it'll be checked as part of the top

1
src/TTImp/Reflect.idr
View File

@ -8,6 +8,7 @@ import Core.TT
import Core.Value
import TTImp.TTImp
import Libraries.Data.WithDefault
%default covering

7
src/TTImp/TTImp.idr
View File

@ -14,6 +14,7 @@ import Data.List1
import Data.Maybe
import Libraries.Data.SortedSet
import Libraries.Data.WithDefault
%default covering
@ -450,14 +451,16 @@ mutual
data ImpDecl' : Type -> Type where
IClaim : FC -> RigCount -> Visibility -> List (FnOpt' nm) ->
ImpTy' nm -> ImpDecl' nm
IData : FC -> Visibility -> Maybe TotalReq -> ImpData' nm -> ImpDecl' nm
IData : FC -> WithDefault Visibility Private ->
Maybe TotalReq -> ImpData' nm -> ImpDecl' nm
IDef : FC -> Name -> List (ImpClause' nm) -> ImpDecl' nm
IParameters : FC ->
List (ImpParameter' nm) ->
List (ImpDecl' nm) -> ImpDecl' nm
IRecord : FC ->
Maybe String -> -- nested namespace
Visibility -> Maybe TotalReq ->
WithDefault Visibility Private ->
Maybe TotalReq ->
ImpRecord' nm -> ImpDecl' nm
IFail : FC -> Maybe String -> List (ImpDecl' nm) -> ImpDecl' nm
INamespace : FC -> Namespace -> List (ImpDecl' nm) -> ImpDecl' nm

2
src/TTImp/TTImp/TTC.idr
View File

@ -8,6 +8,8 @@ import Core.Context.TTC
import TTImp.TTImp
import Libraries.Data.WithDefault
%default covering
mutual

24
tests/idris2/error028/Issue1236.idr Normal file
View File

@ -0,0 +1,24 @@
module Issue1236
private
data Mismatched1 : Type
export
data Mismatched1 : Type where
public export
data Mismatched2 : Type
export
data Mismatched2 : Type where
export
data Aligned : Type
export
data Aligned : Type where
public export
data SpecifyOnce1 : Type
data SpecifyOnce1 : Type where
data SpecifyOnce2 : Type
public export
data SpecifyOnce2 : Type where

13
tests/idris2/error028/expected Normal file
View File

@ -0,0 +1,13 @@
1/1: Building Issue1236 (Issue1236.idr)
Warning: Issue1236.Mismatched1 has been forward-declared with private visibility, cannot change to export. This will be an error in a later release.
Issue1236:5:1--6:30
5 | export
6 | data Mismatched1 : Type where
Warning: Issue1236.Mismatched2 has been forward-declared with public export visibility, cannot change to export. This will be an error in a later release.
Issue1236:10:1--11:30
10 | export
11 | data Mismatched2 : Type where

3
tests/idris2/error028/run Normal file
View File

@ -0,0 +1,3 @@
rm -rf build
$1 --no-color --console-width 0 --check Issue1236.idr

2
tests/idris2/reflection/reflection004/refdecl.idr
View File

@ -21,7 +21,7 @@ mkPoint : (n : Nat) -> {auto gt : GT n 0} -> {auto lte : LTE n 4} -> Decl
mkPoint n
= let type = "Point" ++ show n ++ "D" in
let mkMainUN = NS (MkNS ["Main"]) . UN . Basic in
IRecord emptyFC Nothing Public Nothing
IRecord emptyFC Nothing (specified Public) Nothing
(MkRecord emptyFC (mkMainUN type) [] [] (mkMainUN ("Mk" ++ type))
(toList $ map (\axis => MkIField emptyFC MW ExplicitArg (UN (Field axis)) `(Double)) (axes n)))

2
tests/idris2/reflection/reflection014/refdecl.idr
View File

@ -7,7 +7,7 @@ fc = EmptyFC
mkEnum : (name : String) -> (cons : List String) -> Elab ()
mkEnum name cons =
let enumDecl = IData EmptyFC Public Nothing dat
let enumDecl = IData EmptyFC (specified Public) Nothing dat
in declare [enumDecl]
where enumName : Name
enumName = UN $ Basic name

2
tests/idris2/reflection/reflection024/src/TypeProviders.idr
View File

@ -22,7 +22,7 @@ declareRecordFromSimpleText lk textPath dataName consName = do
fs <- for fs $ \line => case words line of
[name, type] => pure (name, type)
_ => fail "Expected two strings in line in \{!errDesc}"
let dataDecl : Decl = IRecord EmptyFC Nothing Public Nothing $
let dataDecl : Decl = IRecord EmptyFC Nothing (specified Public) Nothing $
MkRecord EmptyFC dataName [] [] consName $
fs <&> \(name, type) => do
let (ns, n) = unsnoc $ split (== '.') type