add autobind keyword

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 ()

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

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
 

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

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

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

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

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