add both typebind and autobind

src/Idris/Doc/Keywords.idr

@@ -467,17 +467,44 @@ autobindDoc = """
     allowing you to give a name to the left-hand-side of the operator and
     use it on the right-hand-side.
 
-    A typical example of an autobind operator is `(**)` the type constructor
-    for dependent pairs. It is used like this: `(x : Nat ** Vect x String)`
+    `autobind` differs from `typebind` in the syntax it allows and the way
+    it desugars. Delcaring an operator as `autobind infixr 0 =|>` allows
+    you to use it with the syntax `(x := e =|> f x)` or `(x : t := e =|> f x)`
 
-    If you declare a new operator to be autobind you can use it the same
-    way.
-
-    Start by defining `autobind infixr 1 =@`, and then you can use it
-    like so: `(n : Nat =@ f n)`.
+    You will need to use `autobind` instead of `typebind` whenever the
+    type of the lambda of the function called by the operator has a type
+    that is not equal to the argument given on the left side of the operator
 
     `autobind` only applies to `infixr` operators and cannot be used as
     operator sections.
+
+    `autobind` operators are desugared as a lambda:
+    `(x := expr =|> fn x)` -> `(expr =@ (\x : ? =|> fn x))`
+    `(x : ty := expr =|> fn x)` -> `(expr =@ (\x : ty =|> fn x))`
+  """
+typebindDoc : Doc IdrisDocAnn
+typebindDoc = """
+  Typebind
+
+    `typebind` is a modifier for operator precedence and fixity declaration.
+    It tells the parser that this operator behaves like a binding operator,
+    allowing you to give a name to the left-hand-side of the operator and
+    use it on the right-hand-side.
+
+    A typical example of a typebind operator is `(**)` the type constructor
+    for dependent pairs. It is used like this: `(x : Nat ** Vect x String)`
+
+    If you declare a new operator to be typebind you can use it the same
+    way.
+
+    Start by defining `typebind infixr 1 =@`, and then you can use it
+    like so: `(n : Nat =@ f n)` or `(n : Nat) =@ f n`
+
+    `typebind` only applies to `infixr` operators and cannot be used as
+    operator sections.
+
+    `typebind` operators are desugared as a lambda:
+    `(x : ty =@ fn x)` -> `(ty =@ (\x : ty =@ fn x))`
   """
 
 rewriteeq : Doc IdrisDocAnn
@@ -584,6 +611,7 @@ keywordsDoc =
   :: "else" ::= ifthenelse
   :: "forall" ::= forallquantifier
   :: "rewrite" ::= rewriteeq
+  :: "typebind" ::= autobindDoc
   :: "autobind" ::= autobindDoc
   :: "using" ::= ""
   :: "interface" ::= interfacemechanism

src/Idris/Parser.idr

@@ -331,15 +331,15 @@ mutual
   opBinderTypes fname indents boundName =
            do decoratedSymbol fname ":"
               ty <- typeExpr pdef fname indents
-              pure (BindType boundName ty)
+              decoratedSymbol fname ":="
+              exp <- expr pdef fname indents
+              pure (BindExplicitType boundName ty exp)
        <|> do decoratedSymbol fname ":="
               exp <- expr pdef fname indents
               pure (BindExpr boundName exp)
        <|> do decoratedSymbol fname ":"
               ty <- typeExpr pdef fname indents
-              decoratedSymbol fname ":="
-              exp <- expr pdef fname indents
-              pure (BindExplicitType boundName ty exp)
+              pure (BindType boundName ty)
 
   opBinder : OriginDesc -> IndentInfo -> Rule (OperatorLHSInfo PTerm)
   opBinder fname indents
@@ -1866,10 +1866,16 @@ definition fname indents
     = do nd <- bounds (clause 0 Nothing fname indents)
          pure (PDef (boundToFC fname nd) [nd.val])
 
+operatorBindingKeyword : EmptyRule BindingModifier
+operatorBindingKeyword
+  =   (keyword "autobind" >> pure Autobind)
+  <|> (keyword "typebind" >> pure Typebind)
+  <|> pure NotBinding
+
 fixDecl : OriginDesc -> IndentInfo -> Rule (List PDecl)
 fixDecl fname indents
     = do vis <- exportVisibility fname
-         binding <- map isJust (optional (keyword "autobind"))
+         binding <- operatorBindingKeyword
          b <- bounds (do fixity <- decorate fname Keyword $ fix
                          commit
                          prec <- decorate fname Keyword $ intLit

src/Idris/Syntax.idr

@@ -47,25 +47,42 @@ Eq Fixity where
   Prefix == Prefix = True
   _ == _ = False
 
+
+public export
+data BindingModifier = NotBinding | Autobind | Typebind
+
+export
+Eq BindingModifier where
+  NotBinding == NotBinding = True
+  Autobind == Autobind = True
+  Typebind == Typebind = True
+  _ == _ = False
+
+export
+Show BindingModifier where
+  show NotBinding = "not binding"
+  show Typebind = "typebind"
+  show Autobind = "autobind"
+
 -- A record to hold all the information about a fixity
 public export
 record FixityInfo where
   constructor MkFixityInfo
   fc : FC
   vis : Visibility
-  isAutobind : Bool
+  bindingInfo : BindingModifier
   fix : Fixity
   precedence : Nat
 
 export
 Show FixityInfo where
-  show fx = "fc: \{show fx.fc}, visibility: \{show fx.vis}, isAutobind: \{show fx.isAutobind}, fixity: \{show fx.fix}, precedence: \{show fx.precedence}"
+  show fx = "fc: \{show fx.fc}, visibility: \{show fx.vis}, binding: \{show fx.bindingInfo}, 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.bindingInfo == y.bindingInfo
         && x.fix == y.fix
         && x.precedence == y.precedence
 
@@ -507,7 +524,7 @@ mutual
        PFail : FC -> Maybe String -> List (PDecl' nm) -> PDecl' nm
 
        PMutual : FC -> List (PDecl' nm) -> PDecl' nm
-       PFixity : FC -> Visibility -> (isAutobind : Bool) -> Fixity -> Nat -> OpStr -> PDecl' nm
+       PFixity : FC -> Visibility -> BindingModifier -> 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
@@ -1043,9 +1060,9 @@ initSyntax
 
     initFixities : ANameMap FixityInfo
     initFixities = fromList
-      [ (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)
+      [ (UN $ Basic "-", MkFixityInfo EmptyFC Export NotBinding Prefix 10)
+      , (UN $ Basic "negate", MkFixityInfo EmptyFC Export NotBinding Prefix 10) -- for documentation purposes
+      , (UN $ Basic "=", MkFixityInfo EmptyFC Export NotBinding Infix 0)
       ]
 
     initDocStrings : ANameMap String

src/Idris/Syntax/TTC.idr

@@ -81,21 +81,33 @@ TTC Import where
          nameAs <- fromBuf b
          pure (MkImport loc reexport path nameAs)
 
+export
+TTC BindingModifier where
+  toBuf b NotBinding = tag 0
+  toBuf b Typebind = tag 1
+  toBuf b Autobind = tag 2
+  fromBuf b
+      = case !getTag of
+             0 => pure NotBinding
+             1 => pure Typebind
+             2 => pure Autobind
+             _ => corrupt "binding"
+
 export
 TTC FixityInfo where
   toBuf b fx
       = do toBuf b fx.fc
            toBuf b fx.vis
-           toBuf b fx.isAutobind
+           toBuf b fx.bindingInfo
            toBuf b fx.fix
            toBuf b fx.precedence
   fromBuf b
       = do fc <- fromBuf b
            vis <- fromBuf b
-           isAutobind <- fromBuf b
+           binding <- fromBuf b
            fix <- fromBuf b
            prec <- fromBuf b
-           pure $ MkFixityInfo fc vis isAutobind fix prec
+           pure $ MkFixityInfo fc vis binding fix prec
 
 
 export

src/Parser/Lexer/Source.idr

@@ -245,7 +245,7 @@ keywords : List String
 keywords = ["data", "module", "where", "let", "in", "do", "record",
             "auto", "default", "implicit", "failing", "mutual", "namespace",
             "parameters", "with", "proof", "impossible", "case", "of",
-            "if", "then", "else", "forall", "rewrite", "autobind",
+            "if", "then", "else", "forall", "rewrite", "typebind", "autobind",
             "using", "interface", "implementation", "open", "import",
             "public", "export", "private"] ++
             fixityKeywords ++

tests/idris2/operators/operators001/Test.idr

@@ -10,8 +10,6 @@ typebind infixr 0 =@
 
 data S : {ty : Type} -> (x : ty) -> Type where
   MkS : (x : ty) =@ S x
-  -- same as
-  -- MkS : (1 x : ty) -> S x
 
 typebind infixr 0 *>