From 1fa638494da822209718f2db4f47d4ba5d538f49 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andr=C3=A9=20Videla?= Date: Mon, 31 Jul 2023 09:35:16 +0200 Subject: [PATCH] [ new ] Fixity access modifier (#3011) --- CHANGELOG.md | 1 + docs/source/tutorial/modules.rst | 12 ++++++ src/Idris/Desugar.idr | 58 +++++++++++++------------- src/Idris/Desugar/Mutual.idr | 4 +- src/Idris/Parser.idr | 17 ++++++-- src/Idris/Resugar.idr | 2 +- src/Idris/Syntax.idr | 66 ++++++++++++++++++++---------- src/Idris/Syntax/TTC.idr | 23 ++++++++--- src/Idris/Syntax/Traversals.idr | 4 +- tests/Main.idr | 2 +- tests/idris2/import009/Import.idr | 9 ++++ tests/idris2/import009/Infix.idr | 10 +++++ tests/idris2/import009/Prefix.idr | 12 ++++++ tests/idris2/import009/Resugar.idr | 5 +++ tests/idris2/import009/Test.idr | 22 ++++++++++ tests/idris2/import009/expected | 27 ++++++++++++ tests/idris2/import009/run | 6 +++ tests/idris2/warning004/Main0.idr | 7 ---- tests/idris2/warning004/expected | 36 +--------------- tests/idris2/warning004/run | 2 - 20 files changed, 219 insertions(+), 106 deletions(-) create mode 100644 tests/idris2/import009/Import.idr create mode 100644 tests/idris2/import009/Infix.idr create mode 100644 tests/idris2/import009/Prefix.idr create mode 100644 tests/idris2/import009/Resugar.idr create mode 100644 tests/idris2/import009/Test.idr create mode 100644 tests/idris2/import009/expected create mode 100755 tests/idris2/import009/run delete mode 100644 tests/idris2/warning004/Main0.idr diff --git a/CHANGELOG.md b/CHANGELOG.md index 2ae31906e..8d18f3096 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -16,6 +16,7 @@ * Rudimentary support for defining lazy functions (addressing issue [#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. * New fromTTImp, fromName, and fromDecls names for custom TTImp, Name, and Decls literals. diff --git a/docs/source/tutorial/modules.rst b/docs/source/tutorial/modules.rst index 0992fc555..29e8f93e7 100644 --- a/docs/source/tutorial/modules.rst +++ b/docs/source/tutorial/modules.rst @@ -162,6 +162,18 @@ For interfaces, the meanings are: - ``public export`` the interface name, method names and default definitions are exported +Meaning for fixity declarations +------------------------------- + +The modifiers differ slightly when applied to fixities. Un-labelled +fixities are exported rather than be private. There is no difference between +`public export` and `export`. In summary: + +- ``private`` means the fixity declaration is only visible within the file. + +- ``public export`` and ``export`` are the same and the fixity is exported. + The access modifier could also be eluded for the same effect. + Propagating Inner Module API's ------------------------------- diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr index 22b5fb8d1..499bac7dd 100644 --- a/src/Idris/Desugar.idr +++ b/src/Idris/Desugar.idr @@ -83,20 +83,27 @@ extendSyn newsyn ++ show (modDocstrings newsyn) ] - put Syn ({ infixes $= merge (infixes newsyn), - prefixes $= merge (prefixes newsyn), + -- Before we merge the two syntax environement, we remove the + -- private fixities from the one we are importing. + -- We keep the local private fixities since they are visible in the + -- current file. + let filteredFixities = removePrivate (fixities newsyn) + put Syn ({ fixities $= merge filteredFixities, ifaces $= merge (ifaces newsyn), modDocstrings $= mergeLeft (modDocstrings newsyn), modDocexports $= mergeLeft (modDocexports newsyn), defDocstrings $= merge (defDocstrings newsyn), bracketholes $= ((bracketholes newsyn) ++) } syn) + where + removePrivate : ANameMap FixityInfo -> ANameMap FixityInfo + removePrivate = fromList . filter ((/= Private) . vis . snd) . toList mkPrec : Fixity -> Nat -> OpPrec -mkPrec InfixL p = AssocL p -mkPrec InfixR p = AssocR p -mkPrec Infix p = NonAssoc p -mkPrec Prefix p = Prefix p +mkPrec InfixL = AssocL +mkPrec InfixR = AssocR +mkPrec Infix = NonAssoc +mkPrec Prefix = Prefix -- Check that an operator does not have any conflicting fixities in scope. -- Each operator can have its fixity defined multiple times across multiple @@ -110,8 +117,8 @@ checkConflictingFixities : {auto s : Ref Syn SyntaxInfo} -> checkConflictingFixities isPrefix exprFC opn = do syn <- get Syn let op = nameRoot opn - let foundFixities : List (Name, FC, Fixity, Nat) = lookupName (UN (Basic op)) (fixities syn) - let (pre, inf) = partition (\(_, _, fx, _) => fx == Prefix) foundFixities + let foundFixities : List (Name, FixityInfo) = lookupName (UN (Basic op)) (fixities syn) + let (pre, inf) = partition ((== Prefix) . fix . snd) foundFixities case (isPrefix, pre, inf) of -- If we do not find any fixity for this operator we check that it uses operator -- characters, if not, it must be a backticked expression. @@ -119,33 +126,33 @@ checkConflictingFixities isPrefix exprFC opn then throw (GenericMsg exprFC "Unknown operator '\{op}'") else pure (NonAssoc 1) -- Backticks are non associative by default - (True, ((fxName, _, fix, prec) :: _), _) => do + (True, ((fxName, fx) :: _), _) => do -- in the prefix case, remove conflicts with infix (-) let extraFixities = pre ++ (filter (\(nm, _) => not $ nameRoot nm == "-") inf) - unless (isCompatible fxName fix prec extraFixities) $ warnConflict fxName extraFixities - pure (mkPrec fix prec) + unless (isCompatible fx extraFixities) $ warnConflict fxName extraFixities + pure (mkPrec fx.fix fx.precedence) -- Could not find any prefix operator fixities, there may be infix ones (True, [] , _) => throw (GenericMsg exprFC $ "'\{op}' is not a prefix operator") - (False, _, ((fxName, _, fix, prec) :: _)) => do - -- in the infix case, remove conflicts with prefix (-) + (False, _, ((fxName, fx) :: _)) => do + -- In the infix case, remove conflicts with prefix (-) let extraFixities = (filter (\(nm, _) => not $ nm == UN (Basic "-")) pre) ++ inf - unless (isCompatible fxName fix prec extraFixities) $ warnConflict fxName extraFixities - pure (mkPrec fix prec) + unless (isCompatible fx extraFixities) $ warnConflict fxName extraFixities + pure (mkPrec fx.fix fx.precedence) -- Could not find any infix operator fixities, there may be prefix ones (False, _, []) => throw (GenericMsg exprFC $ "'\{op}' is not an infix operator") where - -- fixities are compatible with all others of the same name that share the same fixity and precedence - isCompatible : Name -> Fixity -> Nat -> (fixities : List (Name, FC, Fixity, Nat)) -> Bool - isCompatible opName fx prec fix - = all (\(nm, _, fx', prec') => fx' == fx && prec' == prec) fix + -- Fixities are compatible with all others of the same name that share the same fixity and precedence + isCompatible : FixityInfo -> (fixities : List (Name, FixityInfo)) -> Bool + isCompatible fx + = all (\fx' => fx.fix == fx'.fix && fx.precedence == fx'.precedence) . map snd -- Emits a warning using the fixity that we picked and the list of all conflicting fixities - warnConflict : (picked : Name) -> (conflicts : List (Name, FC, Fixity, Nat)) -> Core () + warnConflict : (picked : Name) -> (conflicts : List (Name, FixityInfo)) -> Core () warnConflict fxName all = recordWarning $ GenericWarn exprFC $ """ operator fixity is ambiguous, we are picking \{show fxName} out of : - \{unlines $ map (\(nm, _, _, fx) => " - \{show nm}, precedence level \{show fx}") $ toList all} + \{unlines $ map (\(nm, fx) => " - \{show nm}, precedence level \{show fx.precedence}") $ toList all} To remove this warning, use `%hide` with the fixity to remove For example: %hide \{show fxName} """ @@ -1096,7 +1103,7 @@ mutual mapDesugarPiInfo : List Name -> PiInfo PTerm -> Core (PiInfo RawImp) mapDesugarPiInfo ps = traverse (desugar AnyExpr ps) - desugarDecl ps (PFixity fc fix prec opName) + desugarDecl ps (PFixity fc vis fix prec opName) = do ctx <- get Ctxt -- We update the context of fixities by adding a namespaced fixity -- given by the current namespace and its fixity name. @@ -1105,12 +1112,7 @@ mutual let updatedNS = NS (mkNestedNamespace (Just ctx.currentNS) (show fix)) (UN $ Basic $ nameRoot opName) - -- Depending on the fixity we update the correct fixity context - case fix of - Prefix => - update Syn { prefixes $= addName updatedNS (fc, prec) } - _ => - update Syn { infixes $= addName updatedNS (fc, fix, prec) } + update Syn { fixities $= addName updatedNS (MkFixityInfo fc vis fix prec) } pure [] desugarDecl ps d@(PFail fc mmsg ds) = do -- save the state: the content of a failing block should be discarded diff --git a/src/Idris/Desugar/Mutual.idr b/src/Idris/Desugar/Mutual.idr index af5359ff4..b05449cee 100644 --- a/src/Idris/Desugar/Mutual.idr +++ b/src/Idris/Desugar/Mutual.idr @@ -29,7 +29,7 @@ getDecl AsType (PRecord fc doc vis mbtot (MkPRecord n ps _ _ _)) mkRecType : List (Name, RigCount, PiInfo PTerm, PTerm) -> PTerm mkRecType [] = PType fc mkRecType ((n, c, p, t) :: ts) = PPi fc c p (Just n) t (mkRecType ts) -getDecl AsType d@(PFixity _ _ _ _) = Just d +getDecl AsType d@(PFixity _ _ _ _ _) = Just d getDecl AsType d@(PDirective _ _) = Just d getDecl AsType d = Nothing @@ -37,7 +37,7 @@ getDecl AsDef (PClaim _ _ _ _ _) = Nothing getDecl AsDef d@(PData _ _ _ _ (MkPLater _ _ _)) = Just d getDecl AsDef (PInterface _ _ _ _ _ _ _ _ _) = Nothing getDecl AsDef d@(PRecord _ _ _ _ (MkPRecordLater _ _)) = Just d -getDecl AsDef (PFixity _ _ _ _) = Nothing +getDecl AsDef (PFixity _ _ _ _ _) = Nothing getDecl AsDef (PDirective _ _) = Nothing getDecl AsDef d = Just d diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index 8e47a2649..aa0facc0f 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -1054,14 +1054,24 @@ mutual visOption : OriginDesc -> Rule Visibility visOption fname = (decoratedKeyword fname "public" *> decoratedKeyword fname "export" $> Public) + -- If "public export" failed then we try to parse just "public" and emit an error message saying + -- the user should use "public export" + <|> (bounds (decoratedKeyword fname "public") >>= \x : WithBounds () + => the (Rule Visibility) (fatalLoc x.bounds + #""public" keyword by itself is not an export modifier, did you mean "public export"?"#)) <|> (decoratedKeyword fname "export" $> Export) <|> (decoratedKeyword fname "private" $> Private) -visibility : OriginDesc -> EmptyRule Visibility + +exportVisibility, visibility : OriginDesc -> EmptyRule Visibility visibility fname = visOption fname <|> pure Private +exportVisibility fname + = visOption fname + <|> pure Export + tyDecls : Rule Name -> String -> OriginDesc -> IndentInfo -> Rule (List1 PTypeDecl) tyDecls declName predoc fname indents = do bs <- do docns <- sepBy1 (decoratedSymbol fname ",") @@ -1801,13 +1811,14 @@ definition fname indents fixDecl : OriginDesc -> IndentInfo -> Rule (List PDecl) fixDecl fname indents - = do b <- bounds (do fixity <- decorate fname Keyword $ fix + = do vis <- exportVisibility fname + b <- bounds (do fixity <- decorate fname Keyword $ fix commit prec <- decorate fname Keyword $ intLit ops <- sepBy1 (decoratedSymbol fname ",") iOperator pure (fixity, prec, ops)) (fixity, prec, ops) <- pure b.val - pure (map (PFixity (boundToFC fname b) fixity (fromInteger prec)) (forget ops)) + pure (map (PFixity (boundToFC fname b) vis fixity (fromInteger prec)) (forget ops)) directiveDecl : OriginDesc -> IndentInfo -> Rule PDecl directiveDecl fname indents diff --git a/src/Idris/Resugar.idr b/src/Idris/Resugar.idr index ff481df28..33a72cabc 100644 --- a/src/Idris/Resugar.idr +++ b/src/Idris/Resugar.idr @@ -74,7 +74,7 @@ mkSectionL tm@(PLam fc rig info (PRef _ bd) ty syn <- get Syn let n = rawName kn let asOp = PSectionL fc opFC kn (unbracketApp x) - if not (null $ lookupName (UN $ Basic (nameRoot n)) (infixes syn)) + if not (null $ lookupName (UN $ Basic (nameRoot n)) (fixities syn)) then pure asOp else case dropNS n of DN str _ => pure $ ifThenElse (isOpUserName (Basic str)) asOp tm diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr index ff0423c9c..b0bc35ff1 100644 --- a/src/Idris/Syntax.idr +++ b/src/Idris/Syntax.idr @@ -46,6 +46,26 @@ Eq Fixity where Prefix == Prefix = True _ == _ = False +-- A record to hold all the information about a fixity +public export +record FixityInfo where + constructor MkFixityInfo + fc : FC + vis : Visibility + fix : Fixity + precedence : Nat + +export +Show FixityInfo where + show fx = "fc: \{show fx.fc}, visibility: \{show fx.vis}, fixity: \{show fx.fix}, precedence: \{show fx.precedence}" + +export +Eq FixityInfo where + x == y = x.fc == y.fc + && x.vis == y.vis + && x.fix == y.fix + && x.precedence == y.precedence + public export OpStr' : Type -> Type OpStr' nm = nm @@ -448,7 +468,7 @@ mutual PFail : FC -> Maybe String -> List (PDecl' nm) -> PDecl' nm PMutual : FC -> List (PDecl' nm) -> PDecl' nm - PFixity : FC -> Fixity -> Nat -> OpStr -> PDecl' nm + PFixity : FC -> Visibility -> Fixity -> Nat -> OpStr -> PDecl' nm PNamespace : FC -> Namespace -> List (PDecl' nm) -> PDecl' nm PTransform : FC -> String -> PTerm' nm -> PTerm' nm -> PDecl' nm PRunElabDecl : FC -> PTerm' nm -> PDecl' nm @@ -468,7 +488,7 @@ mutual getPDeclLoc (PRecord fc _ _ _ _) = fc getPDeclLoc (PMutual fc _) = fc getPDeclLoc (PFail fc _ _) = fc - getPDeclLoc (PFixity fc _ _ _) = fc + getPDeclLoc (PFixity fc _ _ _ _) = fc getPDeclLoc (PNamespace fc _ _) = fc getPDeclLoc (PTransform fc _ _ _) = fc getPDeclLoc (PRunElabDecl fc _) = fc @@ -885,14 +905,9 @@ record IFaceInfo where public export record SyntaxInfo where constructor MkSyntax - -- Keep infix/prefix, then we can define operators which are both - -- (most obviously, -) - ||| Infix operators as a map from their names to their fixity, + ||| Operators fixities as a map from their names to their fixity, ||| precedence, and the file context where that fixity was defined. - infixes : ANameMap (FC, Fixity, Nat) - ||| Prefix operators as a map from their names to their precedence - ||| and the file context where their fixity was defined. - prefixes : ANameMap (FC, Nat) + fixities : ANameMap FixityInfo -- info about modules saveMod : List ModuleIdent -- current module name modDocstrings : SortedMap ModuleIdent String @@ -911,8 +926,20 @@ record SyntaxInfo where holeNames : List String -- hole names in the file export -fixities : SyntaxInfo -> ANameMap (FC, Fixity, Nat) -fixities syn = merge (infixes syn) (ANameMap.fromList $ map (\(nm, fc, lv) => (nm, fc, Prefix, lv)) $ toList $ prefixes syn) +prefixes : SyntaxInfo -> ANameMap (FC, Nat) +prefixes = fromList + . map (\(name, fx)=> (name, fx.fc, fx.precedence)) + . filter ((== Prefix) . fix . snd) + . toList + . fixities + +export +infixes : SyntaxInfo -> ANameMap (FC, Fixity, Nat) +infixes = fromList + . map (\(nm, fx) => (nm, fx.fc, fx.fix, fx.precedence)) + . filter ((/= Prefix) . fix . snd) + . toList + . fixities HasNames IFaceInfo where full gam iface @@ -953,8 +980,7 @@ HasNames SyntaxInfo where export initSyntax : SyntaxInfo initSyntax - = MkSyntax initInfix - initPrefix + = MkSyntax initFixities [] empty empty @@ -969,13 +995,12 @@ initSyntax where - initInfix : ANameMap (FC, Fixity, Nat) - initInfix = addName (UN $ Basic "=") (EmptyFC, Infix, 0) empty - initPrefix : ANameMap (FC, Nat) - initPrefix = fromList - [ (UN $ Basic "-", (EmptyFC, 10)) - , (UN $ Basic "negate", (EmptyFC, 10)) -- for documentation purposes + initFixities : ANameMap FixityInfo + initFixities = fromList + [ (UN $ Basic "-", MkFixityInfo EmptyFC Export Prefix 10) + , (UN $ Basic "negate", MkFixityInfo EmptyFC Export Prefix 10) -- for documentation purposes + , (UN $ Basic "=", MkFixityInfo EmptyFC Export Infix 0) ] initDocStrings : ANameMap String @@ -1006,8 +1031,7 @@ addModDocInfo mi doc reexpts export removeFixity : {auto s : Ref Syn SyntaxInfo} -> Fixity -> Name -> Core () -removeFixity Prefix key = update Syn ({prefixes $= removeExact key }) -removeFixity _ key = update Syn ({infixes $= removeExact key }) +removeFixity _ key = update Syn ({fixities $= removeExact key }) export covering diff --git a/src/Idris/Syntax/TTC.idr b/src/Idris/Syntax/TTC.idr index 9643ebc3b..0ae8a2af3 100644 --- a/src/Idris/Syntax/TTC.idr +++ b/src/Idris/Syntax/TTC.idr @@ -81,11 +81,25 @@ TTC Import where nameAs <- fromBuf b pure (MkImport loc reexport path nameAs) +export +TTC FixityInfo where + toBuf b fx + = do toBuf b fx.fc + toBuf b fx.vis + toBuf b fx.fix + toBuf b fx.precedence + fromBuf b + = do fc <- fromBuf b + vis <- fromBuf b + fix <- fromBuf b + prec <- fromBuf b + pure $ MkFixityInfo fc vis fix prec + + export TTC SyntaxInfo where toBuf b syn - = do toBuf b (ANameMap.toList (infixes syn)) - toBuf b (ANameMap.toList (prefixes syn)) + = do toBuf b (ANameMap.toList (fixities syn)) toBuf b (filter (\n => elemBy (==) (fst n) (saveMod syn)) (SortedMap.toList $ modDocstrings syn)) toBuf b (filter (\n => elemBy (==) (fst n) (saveMod syn)) @@ -99,8 +113,7 @@ TTC SyntaxInfo where toBuf b (holeNames syn) fromBuf b - = do inf <- fromBuf b - pre <- fromBuf b + = do fix <- fromBuf b moddstr <- fromBuf b modexpts <- fromBuf b ifs <- fromBuf b @@ -108,7 +121,7 @@ TTC SyntaxInfo where bhs <- fromBuf b start <- fromBuf b hnames <- fromBuf b - pure $ MkSyntax (fromList inf) (fromList pre) + pure $ MkSyntax (fromList fix) [] (fromList moddstr) (fromList modexpts) [] (fromList ifs) empty (fromList defdstrs) diff --git a/src/Idris/Syntax/Traversals.idr b/src/Idris/Syntax/Traversals.idr index a1e7d4dde..de16afd48 100644 --- a/src/Idris/Syntax/Traversals.idr +++ b/src/Idris/Syntax/Traversals.idr @@ -265,7 +265,7 @@ mapPTermM f = goPTerm where pure $ PRecord fc doc v tot (MkPRecordLater n !(go4TupledPTerms nts)) goPDecl (PFail fc msg ps) = PFail fc msg <$> goPDecls ps goPDecl (PMutual fc ps) = PMutual fc <$> goPDecls ps - goPDecl p@(PFixity _ _ _ _) = pure p + goPDecl p@(PFixity _ _ _ _ _) = pure p goPDecl (PNamespace fc strs ps) = PNamespace fc strs <$> goPDecls ps goPDecl (PTransform fc n a b) = PTransform fc n <$> goPTerm a <*> goPTerm b goPDecl (PRunElabDecl fc a) = PRunElabDecl fc <$> goPTerm a @@ -534,7 +534,7 @@ mapPTerm f = goPTerm where = PRecord fc doc v tot (MkPRecordLater n (go4TupledPTerms nts)) goPDecl (PFail fc msg ps) = PFail fc msg $ goPDecl <$> ps goPDecl (PMutual fc ps) = PMutual fc $ goPDecl <$> ps - goPDecl p@(PFixity _ _ _ _) = p + goPDecl p@(PFixity _ _ _ _ _) = p goPDecl (PNamespace fc strs ps) = PNamespace fc strs $ goPDecl <$> ps goPDecl (PTransform fc n a b) = PTransform fc n (goPTerm a) (goPTerm b) goPDecl (PRunElabDecl fc a) = PRunElabDecl fc $ goPTerm a diff --git a/tests/Main.idr b/tests/Main.idr index ff6b3362f..d0338662c 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -272,7 +272,7 @@ idrisTests = MkTestPool "Misc" [] Nothing "eta001", -- Modules and imports "import001", "import002", "import003", "import004", "import005", "import006", - "import007", "import008", + "import007", "import008", "import009", -- Implicit laziness, lazy evaluation "lazy001", "lazy002", "lazy003", -- Namespace blocks diff --git a/tests/idris2/import009/Import.idr b/tests/idris2/import009/Import.idr new file mode 100644 index 000000000..d8c5fb18c --- /dev/null +++ b/tests/idris2/import009/Import.idr @@ -0,0 +1,9 @@ +module Import + +import Test + +(|>) : (s : HasComp x) => {0 a, b, c : x} -> a ~> b -> b ~> c -> a ~> c +a |> b = comp s a b + +(~:>) : Type -> Type -> Type +a ~:> b = Pair a b diff --git a/tests/idris2/import009/Infix.idr b/tests/idris2/import009/Infix.idr new file mode 100644 index 000000000..0bc02b2d5 --- /dev/null +++ b/tests/idris2/import009/Infix.idr @@ -0,0 +1,10 @@ +module Infix + +export +infix 6 !! + +(!!) : List a -> Nat -> Maybe a +[] !! _ = Nothing +(x :: _) !! Z = Just x +(_ :: xs) !! (S n) = xs !! n + diff --git a/tests/idris2/import009/Prefix.idr b/tests/idris2/import009/Prefix.idr new file mode 100644 index 000000000..4c0559cbd --- /dev/null +++ b/tests/idris2/import009/Prefix.idr @@ -0,0 +1,12 @@ +module Prefix + +private +prefix 5 !! + +export +(!!) : Type -> Type +(!!) = Not + +export +test : Either (!! a) (!! b) -> !! (a, b) +test f (x, y) = f (Left x) diff --git a/tests/idris2/import009/Resugar.idr b/tests/idris2/import009/Resugar.idr new file mode 100644 index 000000000..6968cdcb3 --- /dev/null +++ b/tests/idris2/import009/Resugar.idr @@ -0,0 +1,5 @@ +module Resugar + +import Prefix +import Infix + diff --git a/tests/idris2/import009/Test.idr b/tests/idris2/import009/Test.idr new file mode 100644 index 000000000..78aae7420 --- /dev/null +++ b/tests/idris2/import009/Test.idr @@ -0,0 +1,22 @@ +module Test + +private +infixr 5 ~:> + +public export +infixr 5 ~> +infixl 5 |> + +public export +record HasComp (x : Type) where + constructor MkComp + (~:>) : x -> x -> Type + comp : {0 a, b, c : x} -> a ~:> b -> b ~:> c -> a ~:> c + +public export +(~>) : (s : HasComp a) => a -> a -> Type +(~>) = (~:>) s + +export +typesHaveComp : HasComp Type +typesHaveComp = MkComp (\x, y => x -> y) (flip (.)) diff --git a/tests/idris2/import009/expected b/tests/idris2/import009/expected new file mode 100644 index 000000000..cda53b7a3 --- /dev/null +++ b/tests/idris2/import009/expected @@ -0,0 +1,27 @@ +1/1: Building Test (Test.idr) +2/2: Building Import (Import.idr) +Error: Unknown operator '~:>' + +Import:9:1--9:8 + 5 | (|>) : (s : HasComp x) => {0 a, b, c : x} -> a ~> b -> b ~> c -> a ~> c + 6 | a |> b = comp s a b + 7 | + 8 | (~:>) : Type -> Type -> Type + 9 | a ~:> b = Pair a b + ^^^^^^^ + +1/3: Building Prefix (Prefix.idr) +Error: While processing right hand side of test. When unifying: + Either ((!!) a) ((!!) b) +and: + Either a ?b -> Void +Mismatch between: Either ((!!) a) ((!!) b) and Either a ?b -> Void. + +Prefix:12:17--12:27 + 08 | (!!) = Not + 09 | + 10 | export + 11 | test : Either (!! a) (!! b) -> !! (a, b) + 12 | test f (x, y) = f (Left x) + ^^^^^^^^^^ + diff --git a/tests/idris2/import009/run b/tests/idris2/import009/run new file mode 100755 index 000000000..277a2e07c --- /dev/null +++ b/tests/idris2/import009/run @@ -0,0 +1,6 @@ +rm -rf build + +$1 --no-color --console-width 0 --no-banner --check Test.idr +$1 --no-color --console-width 0 --no-banner --check Import.idr + +$1 --no-color --console-width 0 --no-banner --check Resugar.idr diff --git a/tests/idris2/warning004/Main0.idr b/tests/idris2/warning004/Main0.idr deleted file mode 100644 index f55f8d8f6..000000000 --- a/tests/idris2/warning004/Main0.idr +++ /dev/null @@ -1,7 +0,0 @@ -module Main - -import Lib1 -import Lib2 - -main : IO () -main = printLn (10 %%% 10 %%% 1) diff --git a/tests/idris2/warning004/expected b/tests/idris2/warning004/expected index 2c5f4a7e0..b8541a483 100644 --- a/tests/idris2/warning004/expected +++ b/tests/idris2/warning004/expected @@ -1,36 +1,5 @@ -1/3: Building Lib1 (Lib1.idr) -2/3: Building Lib2 (Lib2.idr) -3/3: Building Main0 (Main0.idr) -Warning: operator fixity is ambiguous, we are picking Lib2.infixl.(%%%) out of : - - Lib2.infixl.(%%%), precedence level 5 - - Lib1.infixr.(%%%), precedence level 5 - -To remove this warning, use `%hide` with the fixity to remove -For example: %hide Lib2.infixl.(%%%) - -Main0:7:17--7:32 - 3 | import Lib1 - 4 | import Lib2 - 5 | - 6 | main : IO () - 7 | main = printLn (10 %%% 10 %%% 1) - ^^^^^^^^^^^^^^^ - -Warning: operator fixity is ambiguous, we are picking Lib2.infixl.(%%%) out of : - - Lib2.infixl.(%%%), precedence level 5 - - Lib1.infixr.(%%%), precedence level 5 - -To remove this warning, use `%hide` with the fixity to remove -For example: %hide Lib2.infixl.(%%%) - -Main0:7:24--7:32 - 3 | import Lib1 - 4 | import Lib2 - 5 | - 6 | main : IO () - 7 | main = printLn (10 %%% 10 %%% 1) - ^^^^^^^^ - +1/3: Building Lib2 (Lib2.idr) +2/3: Building Lib1 (Lib1.idr) 3/3: Building Main1 (Main1.idr) Warning: operator fixity is ambiguous, we are picking Lib2.infixl.(%%%) out of : - Lib2.infixl.(%%%), precedence level 5 @@ -63,4 +32,3 @@ Main1:7:24--7:32 ^^^^^^^^ 0 -0 diff --git a/tests/idris2/warning004/run b/tests/idris2/warning004/run index 30a82a74a..9f7c266f5 100755 --- a/tests/idris2/warning004/run +++ b/tests/idris2/warning004/run @@ -1,8 +1,6 @@ rm -rf ./build -$1 --no-color --console-width 0 --check Main0.idr $1 --no-color --console-width 0 --check Main1.idr -$1 --no-color --console-width 0 --exec main Main0.idr $1 --no-color --console-width 0 --exec main Main1.idr