diff --git a/docs/source/typedd/typedd.rst b/docs/source/typedd/typedd.rst index a0943d7c8..beae79f55 100644 --- a/docs/source/typedd/typedd.rst +++ b/docs/source/typedd/typedd.rst @@ -312,6 +312,9 @@ In ``ArithCmd.idr``, update ``DivBy`` and ``import Data.Strings`` as above. Also since export rules are per-namespace now, rather than per-file, you need to export ``(>>=)`` from the namespaces ``CommandDo`` and ``ConsoleDo``. +In ``ArithCmdDo.idr``, since ``(>>=)`` is ``export``, ``Command`` and ``ConsoleIO`` +also have to be ``export``. + In ``StreamFail.idr``, add a ``partial`` annotation to ``labelWith``. Chapter 12 @@ -322,6 +325,9 @@ Also the ``(>>=)`` operators need to be set as ``export`` since they are in thei own namespaces, and in ``getRandom``, ``DivBy`` needs to take additional arguments ``div`` and ``rem``. +In ``ArithState.idr``, since ``(>>=)`` is ``export``, ``Command`` and ``ConsoleIO`` +also have to be ``export``. + Chapter 13 ---------- diff --git a/libs/base/Control/App.idr b/libs/base/Control/App.idr index a0c21e6a2..25aae13b9 100644 --- a/libs/base/Control/App.idr +++ b/libs/base/Control/App.idr @@ -58,11 +58,9 @@ data App1Res : Usage -> Type -> Type where PrimApp : Type -> Type PrimApp a = (1 x : %World) -> AppRes a -export prim_app_pure : a -> PrimApp a prim_app_pure x = \w => MkAppRes x w -export prim_app_bind : (1 act : PrimApp a) -> (1 k : a -> PrimApp b) -> PrimApp b prim_app_bind fn k w = let MkAppRes x' w' = fn w in k x' w' diff --git a/libs/base/System/Clock.idr b/libs/base/System/Clock.idr index 7994b7c3a..e4f3f8336 100644 --- a/libs/base/System/Clock.idr +++ b/libs/base/System/Clock.idr @@ -69,6 +69,7 @@ data OSClock : Type where [external] ||| Note: Back-ends are required to implement UTC, monotonic time, CPU time ||| in current process/thread, and time duration; the rest are optional. +export data ClockTypeMandatory = Mandatory | Optional diff --git a/libs/contrib/System/Path.idr b/libs/contrib/System/Path.idr index 10bfce426..4bb5662c9 100644 --- a/libs/contrib/System/Path.idr +++ b/libs/contrib/System/Path.idr @@ -146,7 +146,6 @@ pathTokenMap = toTokenMap $ , (some $ non $ oneOf "/\\:?", PTText) ] -export lexPath : String -> List PathToken lexPath str = let (tokens, _, _, _) = lex pathTokenMap str in map TokenData.tok tokens diff --git a/libs/contrib/Text/Lexer/Core.idr b/libs/contrib/Text/Lexer/Core.idr index 48f8a3dbd..d75e65fef 100644 --- a/libs/contrib/Text/Lexer/Core.idr +++ b/libs/contrib/Text/Lexer/Core.idr @@ -101,7 +101,6 @@ strIndex (MkStrLen str len) i mkStr : String -> StrLen mkStr str = MkStrLen str (length str) -export strTail : Nat -> StrLen -> StrLen strTail start (MkStrLen str len) = MkStrLen (substr start len str) (minus len start) diff --git a/src/Algebra/ZeroOneOmega.idr b/src/Algebra/ZeroOneOmega.idr index 8ea753b98..29fb00108 100644 --- a/src/Algebra/ZeroOneOmega.idr +++ b/src/Algebra/ZeroOneOmega.idr @@ -8,6 +8,7 @@ import Algebra.Preorder export data ZeroOneOmega = Rig0 | Rig1 | RigW +export Preorder ZeroOneOmega where Rig0 <= _ = True Rig1 <= Rig1 = True diff --git a/src/Idris/Error.idr b/src/Idris/Error.idr index 5b054fd4b..f2a9dba3b 100644 --- a/src/Idris/Error.idr +++ b/src/Idris/Error.idr @@ -195,8 +195,8 @@ perror (SolvedNamedHole _ env h tm) = pure $ "Named hole " ++ show h ++ " has been solved by unification\n" ++ "Result: " ++ !(pshow env tm) perror (VisibilityError fc vx x vy y) - = pure $ show vx ++ " " ++ sugarName x ++ - " cannot refer to " ++ show vy ++ " " ++ sugarName y + = pure $ show vx ++ " " ++ sugarName !(toFullNames x) ++ + " cannot refer to " ++ show vy ++ " " ++ sugarName !(toFullNames y) perror (NonLinearPattern _ n) = pure $ "Non linear pattern " ++ sugarName n perror (BadPattern _ n) = pure $ "Pattern not allowed here: " ++ show n perror (NoDeclaration _ n) = pure $ "No type declaration for " ++ show n diff --git a/src/TTImp/Elab/Case.idr b/src/TTImp/Elab/Case.idr index b1705bb17..9c18e555c 100644 --- a/src/TTImp/Elab/Case.idr +++ b/src/TTImp/Elab/Case.idr @@ -208,7 +208,7 @@ caseBlock {vars} rigc elabinfo fc nest env scr scrtm scrty caseRig alts expected -- the alternative of fixing up the environment when (not (isNil fullImps)) $ findImpsIn fc [] [] casefnty cidx <- addDef casen (newDef fc casen (if isErased rigc then erased else top) - [] casefnty Private None) + [] casefnty Public None) -- don't worry about totality of the case block; it'll be handled -- by the totality of the parent function setFlag fc (Resolved cidx) (SetTotal PartialOK) diff --git a/src/TTImp/ProcessData.idr b/src/TTImp/ProcessData.idr index c19415c5c..adaac8291 100644 --- a/src/TTImp/ProcessData.idr +++ b/src/TTImp/ProcessData.idr @@ -14,6 +14,7 @@ import TTImp.Elab.Check import TTImp.Elab.Utils import TTImp.Elab import TTImp.TTImp +import TTImp.Utils import Data.List import Data.NameMap @@ -110,6 +111,12 @@ checkCon {vars} opts nest env vis tn_in tn (MkImpTy fc cn_in ty_raw) Public => do addHashWithNames cn addHashWithNames fullty _ => pure () + + -- Check name visibility: unless it's a private name, any names in + -- the type must be greater than private + when (vis /= Private) $ + traverse_ (checkRefVisibility fc cn vis Private) + (keys (getRefs (UN "") fullty)) pure (MkCon fc cn !(getArity defs [] fullty) fullty) conName : Constructor -> Name @@ -280,6 +287,12 @@ processData {vars} eopts nest env fc vis (MkImpLater dfc n_in ty_raw) Private => pure () _ => do addHashWithNames n addHashWithNames fullty + + -- Check name visibility: unless it's a private name, any names in + -- the type must be greater than private + when (vis /= Private) $ + traverse_ (checkRefVisibility fc n vis Private) + (keys (getRefs (UN "") fullty)) pure () processData {vars} eopts nest env fc vis (MkImpData dfc n_in ty_raw opts cons_raw) diff --git a/src/TTImp/ProcessRecord.idr b/src/TTImp/ProcessRecord.idr index c0ba0c65e..6edc98ceb 100644 --- a/src/TTImp/ProcessRecord.idr +++ b/src/TTImp/ProcessRecord.idr @@ -24,6 +24,11 @@ mkDataTy fc [] = IType fc mkDataTy fc ((n, c, p, ty) :: ps) = IPi fc c p (Just n) ty (mkDataTy fc ps) +-- Projections are only visible if the record is public export +projVis : Visibility -> Visibility +projVis Public = Public +projVis _ = Private + elabRecord : {vars : _} -> {auto c : Ref Ctxt Defs} -> {auto m : Ref MD Metadata} -> @@ -148,7 +153,7 @@ elabRecord {vars} eopts fc env nest newns vis tn params conName_in fields processDecl [] nest env (IClaim fc (if isErased rc then erased - else top) vis [Inline] (MkImpTy fc projNameNS projTy)) + else top) (projVis vis) [Inline] (MkImpTy fc projNameNS projTy)) -- Define the LHS and RHS let lhs_exp diff --git a/src/TTImp/ProcessType.idr b/src/TTImp/ProcessType.idr index 81ef8315d..fa8689ddc 100644 --- a/src/TTImp/ProcessType.idr +++ b/src/TTImp/ProcessType.idr @@ -15,6 +15,7 @@ import TTImp.Elab.Check import TTImp.Elab.Utils import TTImp.Elab import TTImp.TTImp +import TTImp.Utils import Data.List import Data.NameMap @@ -271,10 +272,15 @@ processType {vars} eopts nest env fc rig vis opts (MkImpTy tfc n_in ty_raw) (IBindHere fc (PI erased) ty_raw) (gType fc) logTermNF 3 ("Type of " ++ show n) [] (abstractFullEnvType tfc env ty) - -- TODO: Check name visibility def <- initDef n env ty opts let fullty = abstractFullEnvType tfc env ty + -- Check name visibility: unless it's a private name, any names in + -- the type must be greater than private + when (vis /= Private) $ + traverse_ (checkRefVisibility fc n vis Private) + (keys (getRefs (UN "") fullty)) + (erased, dterased) <- findErased fullty defs <- get Ctxt empty <- clearDefs defs @@ -298,7 +304,6 @@ processType {vars} eopts nest env fc rig vis opts (MkImpTy tfc n_in ty_raw) addTyDecl fc (Resolved idx) env ty -- for definition generation addNameType fc (Resolved idx) env ty -- for looking up types - traverse_ addToSave (keys (getMetas ty)) addToSave n log 10 $ "Saving from " ++ show n ++ ": " ++ show (keys (getMetas ty)) diff --git a/src/TTImp/Utils.idr b/src/TTImp/Utils.idr index e8a533cfc..20edcebe6 100644 --- a/src/TTImp/Utils.idr +++ b/src/TTImp/Utils.idr @@ -286,3 +286,16 @@ uniqueName defs used n next str = let (n, i) = nameNum str in n ++ "_" ++ show (i + 1) + +export +checkRefVisibility : {auto c : Ref Ctxt Defs} -> + FC -> Name -> + Visibility -> -- Visibility of the name + Visibility -> -- Minimum visibility of references + Name -> Core () +checkRefVisibility fc fn vis min ref + = do defs <- get Ctxt + Just gdef <- lookupCtxtExact ref (gamma defs) + | Nothing => pure () + when (visibility gdef <= min) $ + throw (VisibilityError fc vis fn (visibility gdef) ref) diff --git a/src/Utils/Path.idr b/src/Utils/Path.idr index d9f4664fe..61118fed9 100644 --- a/src/Utils/Path.idr +++ b/src/Utils/Path.idr @@ -146,7 +146,6 @@ pathTokenMap = toTokenMap $ , (some $ non $ oneOf "/\\:?", PTText) ] -export lexPath : String -> List PathToken lexPath str = let (tokens, _, _, _) = lex pathTokenMap str in map TokenData.tok tokens diff --git a/tests/idris2/basic003/Ambig2.idr b/tests/idris2/basic003/Ambig2.idr index 48b8b36c8..eda9e9721 100644 --- a/tests/idris2/basic003/Ambig2.idr +++ b/tests/idris2/basic003/Ambig2.idr @@ -1,9 +1,13 @@ infixr 5 :: +export data List a = Nil | (::) a (List a) +export data Nat = Z | S Nat +export data Vect : Type -> Type where +export data Set : Type -> Type where namespace Vect diff --git a/tests/idris2/basic003/expected b/tests/idris2/basic003/expected index 2d1dc35ba..ac42e64df 100644 --- a/tests/idris2/basic003/expected +++ b/tests/idris2/basic003/expected @@ -1,7 +1,7 @@ 1/1: Building Ambig1 (Ambig1.idr) Main> Bye for now! 1/1: Building Ambig2 (Ambig2.idr) -Ambig2.idr:22:21--22:28:While processing right hand side of keepUnique at Ambig2.idr:22:1--24:1: +Ambig2.idr:26:21--26:28:While processing right hand side of keepUnique at Ambig2.idr:26:1--28:1: Ambiguous elaboration. Possible correct results: Main.Set.toList ?arg Main.Vect.toList ?arg diff --git a/tests/idris2/perf004/bigdpair.idr b/tests/idris2/perf004/bigdpair.idr index 23f2ce834..b5167bbc4 100644 --- a/tests/idris2/perf004/bigdpair.idr +++ b/tests/idris2/perf004/bigdpair.idr @@ -11,6 +11,7 @@ bigEx (S k) = ((2 ** [0,0]), bigEx k) data VWrap : Type -> Type where MkVWrap : (0 n : Nat) -> Vect n a -> VWrap a +export MkBig' : Nat -> Type MkBig' Z = Int MkBig' (S k) = (VWrap Int, MkBig' k) diff --git a/tests/idris2/real002/Control/App.idr b/tests/idris2/real002/Control/App.idr index f8faae069..f420419df 100644 --- a/tests/idris2/real002/Control/App.idr +++ b/tests/idris2/real002/Control/App.idr @@ -81,11 +81,9 @@ data App1Res : Usage -> Type -> Type where PrimApp : Type -> Type PrimApp a = (1 x : %World) -> AppRes a -export prim_app_pure : a -> PrimApp a prim_app_pure x = \w => MkAppRes x w -export prim_app_bind : (1 act : PrimApp a) -> (1 k : a -> PrimApp b) -> PrimApp b prim_app_bind fn k w = let MkAppRes x' w' = fn w in k x' w' diff --git a/tests/idris2/reg008/Vending.idr b/tests/idris2/reg008/Vending.idr index ef1fac040..ca73dd7e9 100644 --- a/tests/idris2/reg008/Vending.idr +++ b/tests/idris2/reg008/Vending.idr @@ -16,6 +16,7 @@ strToInput x = if all isDigit (unpack x) then Just (REFILL (stringToNatOrZ x)) else Nothing +export data MachineCmd : Type -> VendState -> VendState -> Type where @@ -35,6 +36,7 @@ data MachineCmd : Type -> (a -> MachineCmd b state2 state3) -> MachineCmd b state1 state3 +export data MachineIO : VendState -> Type where Do : {state1 : _} -> MachineCmd a state1 state2 -> diff --git a/tests/ttimp/basic005/Ambig.yaff b/tests/ttimp/basic005/Ambig.yaff index d3e521b8e..ac2959719 100644 --- a/tests/ttimp/basic005/Ambig.yaff +++ b/tests/ttimp/basic005/Ambig.yaff @@ -1,3 +1,4 @@ +public export data Nat : Type where Z : Nat S : Nat -> Nat diff --git a/tests/ttimp/basic006/Ambig.yaff b/tests/ttimp/basic006/Ambig.yaff index e7a5562bc..b1c51c16c 100644 --- a/tests/ttimp/basic006/Ambig.yaff +++ b/tests/ttimp/basic006/Ambig.yaff @@ -1,3 +1,4 @@ +public export data Nat : Type where Z : Nat S : Nat -> Nat diff --git a/tests/typedd-book/chapter11/ArithCmdDo.idr b/tests/typedd-book/chapter11/ArithCmdDo.idr index db71f5b1a..5956d0af7 100644 --- a/tests/typedd-book/chapter11/ArithCmdDo.idr +++ b/tests/typedd-book/chapter11/ArithCmdDo.idr @@ -4,6 +4,7 @@ import System -- %default total +export data Command : Type -> Type where PutStr : String -> Command () GetLine : Command String @@ -11,6 +12,7 @@ data Command : Type -> Type where Pure : ty -> Command ty Bind : Command a -> (a -> Command b) -> Command b +export data ConsoleIO : Type -> Type where Quit : a -> ConsoleIO a Do : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b diff --git a/tests/typedd-book/chapter12/ArithState.idr b/tests/typedd-book/chapter12/ArithState.idr index 5066d353f..a01325037 100644 --- a/tests/typedd-book/chapter12/ArithState.idr +++ b/tests/typedd-book/chapter12/ArithState.idr @@ -32,6 +32,7 @@ addCorrect = record { score.correct $= (+1), setDifficulty : Int -> GameState -> GameState setDifficulty newDiff state = record { difficulty = newDiff } state +export data Command : Type -> Type where PutStr : String -> Command () GetLine : Command String @@ -43,6 +44,7 @@ data Command : Type -> Type where Pure : ty -> Command ty Bind : Command a -> (a -> Command b) -> Command b +export data ConsoleIO : Type -> Type where Quit : a -> ConsoleIO a Do : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b diff --git a/tests/typedd-book/chapter13/StackIO.idr b/tests/typedd-book/chapter13/StackIO.idr index 598b0d623..fc6095ebf 100644 --- a/tests/typedd-book/chapter13/StackIO.idr +++ b/tests/typedd-book/chapter13/StackIO.idr @@ -1,5 +1,6 @@ import Data.Vect +export data StackCmd : Type -> Nat -> Nat -> Type where Push : Integer -> StackCmd () height (S height) Pop : StackCmd Integer (S height) height @@ -35,6 +36,7 @@ testAdd = do Push 10 val2 <- Pop PutStr (show (val1 + val2) ++ "\n") +export data StackIO : Nat -> Type where Do : StackCmd a height1 height2 -> (a -> Inf (StackIO height2)) -> StackIO height1 diff --git a/tests/typedd-book/chapter13/Vending.idr b/tests/typedd-book/chapter13/Vending.idr index 53ec601cf..e8e704f63 100644 --- a/tests/typedd-book/chapter13/Vending.idr +++ b/tests/typedd-book/chapter13/Vending.idr @@ -16,6 +16,7 @@ strToInput x = if all isDigit (unpack x) then Just (REFILL (stringToNatOrZ x)) else Nothing +export data MachineCmd : Type -> VendState -> VendState -> Type where @@ -35,6 +36,7 @@ data MachineCmd : Type -> (a -> MachineCmd b state2 state3) -> MachineCmd b state1 state3 +export data MachineIO : VendState -> Type where Do : {state1 : _} -> MachineCmd a state1 state2 -> diff --git a/tests/typedd-book/chapter14/Hangman.idr b/tests/typedd-book/chapter14/Hangman.idr index 986e3b234..266746f74 100644 --- a/tests/typedd-book/chapter14/Hangman.idr +++ b/tests/typedd-book/chapter14/Hangman.idr @@ -6,6 +6,7 @@ import Decidable.Equality %default total +public export data GameState : Type where NotRunning : GameState Running : (guesses : Nat) -> (letters : Nat) -> GameState @@ -15,6 +16,7 @@ letters str = nub (map toUpper (unpack str)) data GuessResult = Correct | Incorrect +export data GameCmd : (ty : Type) -> GameState -> (ty -> GameState) -> Type where NewGame : (word : String) -> GameCmd () NotRunning (const (Running 6 (length (letters word))))