From b8d81b768e9bfbaace919cfc92235a7c612d4315 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andr=C3=A9=20Videla?= Date: Wed, 18 Oct 2023 13:04:42 +0100 Subject: [PATCH] add autobind keyword --- src/Core/Binary.idr | 2 +- src/Idris/Desugar.idr | 4 ++-- src/Idris/Desugar/Mutual.idr | 4 ++-- src/Idris/Parser.idr | 3 ++- src/Idris/Syntax.idr | 14 ++++++++------ src/Idris/Syntax/TTC.idr | 4 +++- src/Idris/Syntax/Traversals.idr | 4 ++-- tests/idris2/operators/operators001/Test.idr | 2 +- 8 files changed, 21 insertions(+), 16 deletions(-) diff --git a/src/Core/Binary.idr b/src/Core/Binary.idr index bd9a4e4ce..6f985cde4 100644 --- a/src/Core/Binary.idr +++ b/src/Core/Binary.idr @@ -29,7 +29,7 @@ import public Libraries.Utils.Binary ||| version number if you're changing the version more than once in the same day. export ttcVersion : Int -ttcVersion = 2023_09_08_00 +ttcVersion = 2023_11_12_00 export checkTTCVersion : String -> Int -> Int -> Core () diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr index f9196dd34..d512552ab 100644 --- a/src/Idris/Desugar.idr +++ b/src/Idris/Desugar.idr @@ -1109,7 +1109,7 @@ mutual NS ns (DN str (MN ("__mk" ++ str) 0)) mkConName n = DN (show n) (MN ("__mk" ++ show n) 0) - desugarDecl ps (PFixity fc vis fix prec opName) + desugarDecl ps (PFixity fc vis binding 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. @@ -1118,7 +1118,7 @@ mutual let updatedNS = NS (mkNestedNamespace (Just ctx.currentNS) (show fix)) (UN $ Basic $ nameRoot opName) - update Syn { fixities $= addName updatedNS (MkFixityInfo fc vis fix prec) } + update Syn { fixities $= addName updatedNS (MkFixityInfo fc vis binding 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 b05449cee..c13ca8c41 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 545da2e70..8d47e5890 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -1828,13 +1828,14 @@ definition fname indents fixDecl : OriginDesc -> IndentInfo -> Rule (List PDecl) fixDecl fname indents = do vis <- exportVisibility fname + binding <- map isJust (optional (keyword "autobind")) 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) vis fixity (fromInteger prec)) (forget ops)) + pure (map (PFixity (boundToFC fname b) vis binding fixity (fromInteger prec)) (forget ops)) directiveDecl : OriginDesc -> IndentInfo -> Rule PDecl directiveDecl fname indents diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr index ed365477c..6a77dc490 100644 --- a/src/Idris/Syntax.idr +++ b/src/Idris/Syntax.idr @@ -53,17 +53,19 @@ record FixityInfo where constructor MkFixityInfo fc : FC vis : Visibility + isAutobind : Bool 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}" + show fx = "fc: \{show fx.fc}, visibility: \{show fx.vis}, isAutobind: \{show fx.isAutobind}, fixity: \{show fx.fix}, precedence: \{show fx.precedence}" export Eq FixityInfo where x == y = x.fc == y.fc && x.vis == y.vis + && x.isAutobind == y.isAutobind && x.fix == y.fix && x.precedence == y.precedence @@ -470,7 +472,7 @@ mutual PFail : FC -> Maybe String -> List (PDecl' nm) -> PDecl' nm PMutual : FC -> List (PDecl' nm) -> PDecl' nm - PFixity : FC -> Visibility -> Fixity -> Nat -> OpStr -> PDecl' nm + PFixity : FC -> Visibility -> (isAutobind : Bool) -> 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 @@ -489,7 +491,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 @@ -999,9 +1001,9 @@ initSyntax 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) + [ (UN $ Basic "-", MkFixityInfo EmptyFC Export False Prefix 10) + , (UN $ Basic "negate", MkFixityInfo EmptyFC Export False Prefix 10) -- for documentation purposes + , (UN $ Basic "=", MkFixityInfo EmptyFC Export False Infix 0) ] initDocStrings : ANameMap String diff --git a/src/Idris/Syntax/TTC.idr b/src/Idris/Syntax/TTC.idr index 0ae8a2af3..47e1b63ad 100644 --- a/src/Idris/Syntax/TTC.idr +++ b/src/Idris/Syntax/TTC.idr @@ -86,14 +86,16 @@ TTC FixityInfo where toBuf b fx = do toBuf b fx.fc toBuf b fx.vis + toBuf b fx.isAutobind toBuf b fx.fix toBuf b fx.precedence fromBuf b = do fc <- fromBuf b vis <- fromBuf b + isAutobind <- fromBuf b fix <- fromBuf b prec <- fromBuf b - pure $ MkFixityInfo fc vis fix prec + pure $ MkFixityInfo fc vis isAutobind fix prec export diff --git a/src/Idris/Syntax/Traversals.idr b/src/Idris/Syntax/Traversals.idr index 9db5d8fa2..fd390ceea 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 @@ -533,7 +533,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/idris2/operators/operators001/Test.idr b/tests/idris2/operators/operators001/Test.idr index c113aa3d8..053dd0f1e 100644 --- a/tests/idris2/operators/operators001/Test.idr +++ b/tests/idris2/operators/operators001/Test.idr @@ -1,6 +1,6 @@ autobind infixr 0 =@ -(=@) : (a : Type) -> (a -> Type) -> Type +0 (=@) : (a : Type) -> (a -> Type) -> Type (=@) a f = (1 x : a) -> f x