desugar autobind properly

src/Idris/Desugar.idr

@@ -160,7 +160,7 @@ checkConflictingFixities isPrefix exprFC opn
 toTokList : {auto s : Ref Syn SyntaxInfo} ->
             {auto c : Ref Ctxt Defs} ->
             PTerm -> Core (List (Tok OpStr PTerm))
-toTokList (POp fc opFC opn l r)
+toTokList (POp fc opFC _ opn l r)
     = do precInfo <- checkConflictingFixities False fc opn
          rtoks <- toTokList r
          pure (Expr l :: Op fc opFC opn precInfo :: rtoks)
@@ -308,8 +308,16 @@ mutual
                      [apply (IVar fc (UN $ Basic "===")) [l', r'],
                       apply (IVar fc (UN $ Basic "~=~")) [l', r']]
   desugarB side ps (PBracketed fc e) = desugarB side ps e
-  desugarB side ps (POp fc opFC op l r)
+  -- desugarB side ps (PDPair fc opFC (PRef namefc n@(UN _)) ty r)
-      = do ts <- toTokList (POp fc opFC op l r)
+  --     = do ty' <- desugarB side ps ty
+  --          r' <- desugarB side ps r
+  --          pure $ apply (IVar opFC dpairname)
+  --                       [ty', ILam namefc top Explicit (Just n) ty' r']
+  desugarB side ps (POp fc opFC (Just nm) op l r)
+      = desugarB side ps (POp fc opFC Nothing op l
+                         $ PLam (virtualiseFC opFC) top Explicit nm (PImplicit opFC) r)
+  desugarB side ps (POp fc opFC Nothing op l r)
+      = do ts <- toTokList (POp fc opFC Nothing op l r)
            desugarTree side ps !(parseOps ts)
   desugarB side ps (PPrefixOp fc opFC op arg)
       = do ts <- toTokList (PPrefixOp fc opFC op arg)
@@ -322,12 +330,12 @@ mutual
                 [] =>
                     desugarB side ps
                         (PLam fc top Explicit (PRef fc (MN "arg" 0)) (PImplicit fc)
-                            (POp fc opFC op (PRef fc (MN "arg" 0)) arg))
+                            (POp fc opFC Nothing op (PRef fc (MN "arg" 0)) arg))
                 (prec :: _) => desugarB side ps (PPrefixOp fc opFC op arg)
   desugarB side ps (PSectionR fc opFC arg op)
       = desugarB side ps
           (PLam fc top Explicit (PRef fc (MN "arg" 0)) (PImplicit fc)
-              (POp fc opFC op arg (PRef fc (MN "arg" 0))))
+              (POp fc opFC Nothing op arg (PRef fc (MN "arg" 0))))
   desugarB side ps (PSearch fc depth) = pure $ ISearch fc depth
   desugarB side ps (PPrimVal fc (BI x))
       = case !fromIntegerName of

src/Idris/Parser.idr

@@ -325,15 +325,41 @@ mutual
         decoratedSymbol fname "]"
         pure (map (\ n => (boundToFC fname n, n.val)) $ forget ns)
 
-  opExpr : ParseOpts -> OriginDesc -> IndentInfo -> Rule PTerm
+  opBinder : OriginDesc -> IndentInfo -> Rule (PTerm, PTerm)
-  opExpr q fname indents
+  opBinder fname indents
+      = do loc <- bounds (do x <- UN . Basic <$> decoratedSimpleBinderName fname
+                             decoratedSymbol fname ":"
+                             ty <- typeExpr pdef fname indents
+                             pure (x, ty))
+           (nm, ty) <- pure loc.val
+           pure (PRef (boundToFC fname loc) nm, ty)
+
+
+  autobindOp : ParseOpts -> OriginDesc -> IndentInfo -> Rule PTerm
+  autobindOp q fname indents
+      = do bindRes <- bounds $ parens fname (opBinder fname indents)
+           (bindName, bindExpr) <- pure $ bindRes.val
+           continue indents
+           op <- bounds iOperator
+           e <- bounds (expr q fname indents)
+           pure (POp (boundToFC fname $ mergeBounds bindRes e)
+                     (boundToFC fname op)
+                     (Just $ bindName)
+                     op.val
+                     bindExpr
+                     e.val)
+
+  opExprBase : ParseOpts -> OriginDesc -> IndentInfo -> Rule PTerm
+  opExprBase q fname indents
       = do l <- bounds (appExpr q fname indents)
            (if eqOK q
-               then do r <- bounds (continue indents *> decoratedSymbol fname "=" *> opExpr q fname indents)
+               then do r <- bounds (continue indents
+                                *> decoratedSymbol fname "="
+                                *> opExprBase q fname indents)
                        pure $
                          let fc = boundToFC fname (mergeBounds l r)
                              opFC = virtualiseFC fc -- already been highlighted: we don't care
-                         in POp fc opFC (UN $ Basic "=") l.val r.val
+                         in POp fc opFC Nothing (UN $ Basic "=") l.val r.val
                else fail "= not allowed")
              <|>
              (do b <- bounds $ do
@@ -346,9 +372,13 @@ mutual
                  (op, r) <- pure b.val
                  let fc = boundToFC fname (mergeBounds l b)
                  let opFC = boundToFC fname op
-                 pure (POp fc opFC op.val l.val r))
+                 pure (POp fc opFC Nothing op.val l.val r))
                <|> pure l.val
 
+  opExpr : ParseOpts -> OriginDesc -> IndentInfo -> Rule PTerm
+  opExpr q fname indents = opExprBase q fname indents
+                       <|> autobindOp q fname indents
+
   dpairType : OriginDesc -> WithBounds t -> IndentInfo -> Rule PTerm
   dpairType fname start indents
       = do loc <- bounds (do x <- UN . Basic <$> decoratedSimpleBinderName fname
@@ -981,6 +1011,7 @@ mutual
     <|> defaultImplicitPi fname indents
     <|> forall_ fname indents
     <|> implicitPi fname indents
+    <|> autobindOp pdef fname indents
     <|> explicitPi fname indents
     <|> lam fname indents
 

src/Idris/Pretty.idr

@@ -332,7 +332,11 @@ mutual
     prettyPrec d (PDotted _ p) = dot <+> prettyPrec d p
     prettyPrec d (PImplicit _) = "_"
     prettyPrec d (PInfer _) = annotate Hole $ "?"
-    prettyPrec d (POp _ _ op x y) =
+    prettyPrec d (POp _ _ (Just ab) op left right) =
+        group $ parens (pretty ab <++> ":" <++> pretty left)
+           <++> prettyOp op
+           <++> pretty right
+    prettyPrec d (POp _ _ Nothing op x y) =
       parenthesise (d >= App) $
         group $ pretty x
            <++> prettyOp op

src/Idris/Resugar.idr

@@ -46,7 +46,7 @@ mkOp tm@(PApp fc (PApp _ (PRef opFC kn) x) y)
        -- to know if the name is an operator or not, it's enough to check
        -- that the fixity context contains the name `(++)`
        let rootName = UN (Basic (nameRoot raw))
-       let asOp = POp fc opFC kn (unbracketApp x) (unbracketApp y)
+       let asOp = POp fc opFC Nothing kn (unbracketApp x) (unbracketApp y)
        if not (null (lookupName rootName (infixes syn)))
          then pure asOp
          else case dropNS raw of
@@ -590,8 +590,8 @@ cleanPTerm ptm
     cleanNode : IPTerm -> Core IPTerm
     cleanNode (PRef fc nm)    =
       PRef fc <$> cleanKindedName nm
-    cleanNode (POp fc opFC op x y) =
+    cleanNode (POp fc opFC abi op x y) =
-      (\ op => POp fc opFC op x y) <$> cleanKindedName op
+      (\ op => POp fc opFC abi op x y) <$> cleanKindedName op
     cleanNode (PPrefixOp fc opFC op x) =
       (\ op => PPrefixOp fc opFC op x) <$> cleanKindedName op
     cleanNode (PSectionL fc opFC op x) =

src/Idris/Syntax.idr

@@ -138,7 +138,10 @@ mutual
 
        -- Operators
 
-       POp : (full, opFC : FC) -> OpStr' nm -> PTerm' nm -> PTerm' nm -> PTerm' nm
+       POp : (full, opFC : FC) ->
+             -- If the operator is autobind, we expect a pterm for the bound name
+             (isAutobind : Maybe (PTerm' nm)) ->
+             OpStr' nm -> PTerm' nm -> PTerm' nm -> PTerm' nm
        PPrefixOp : (full, opFC : FC) -> OpStr' nm -> PTerm' nm -> PTerm' nm
        PSectionL : (full, opFC : FC) -> OpStr' nm -> PTerm' nm -> PTerm' nm
        PSectionR : (full, opFC : FC) -> PTerm' nm -> OpStr' nm -> PTerm' nm
@@ -204,7 +207,7 @@ mutual
   getPTermLoc (PDotted fc _) = fc
   getPTermLoc (PImplicit fc) = fc
   getPTermLoc (PInfer fc) = fc
-  getPTermLoc (POp fc _ _ _ _) = fc
+  getPTermLoc (POp fc _ _ _ _ _) = fc
   getPTermLoc (PPrefixOp fc _ _ _) = fc
   getPTermLoc (PSectionL fc _ _ _) = fc
   getPTermLoc (PSectionR fc _ _ _) = fc
@@ -808,7 +811,9 @@ parameters {0 nm : Type} (toName : nm -> Name)
   showPTermPrec d (PDotted _ p) = "." ++ showPTermPrec d p
   showPTermPrec _ (PImplicit _) = "_"
   showPTermPrec _ (PInfer _) = "?"
-  showPTermPrec d (POp _ _ op x y) = showPTermPrec d x ++ " " ++ showOpPrec d op ++ " " ++ showPTermPrec d y
+  showPTermPrec d (POp _ _ Nothing op x y) = showPTermPrec d x ++ " " ++ showOpPrec d op ++ " " ++ showPTermPrec d y
+  showPTermPrec d (POp _ _ (Just nm) op x y)
+        = "(" ++ showPTermPrec d nm ++ " : " ++ showPTermPrec d x ++ " " ++ showOpPrec d op ++ " " ++ showPTermPrec d y ++ ")"
   showPTermPrec d (PPrefixOp _ _ op x) = showOpPrec d op ++ showPTermPrec d x
   showPTermPrec d (PSectionL _ _ op x) = "(" ++ showOpPrec d op ++ " " ++ showPTermPrec d x ++ ")"
   showPTermPrec d (PSectionR _ _ x op) = "(" ++ showPTermPrec d x ++ " " ++ showOpPrec d op ++ ")"

src/Idris/Syntax/Traversals.idr

@@ -99,9 +99,12 @@ mapPTermM f = goPTerm where
       >>= f
     goPTerm t@(PImplicit _) = f t
     goPTerm t@(PInfer _) = f t
-    goPTerm (POp fc opFC x y z) =
+    goPTerm (POp fc opFC autobindInfo x y z) =
-      POp fc opFC x <$> goPTerm y
+      POp fc opFC
-                    <*> goPTerm z
+          <$> traverseOpt f autobindInfo
+          <*> pure x
+          <*> goPTerm y
+          <*> goPTerm z
       >>= f
     goPTerm (PPrefixOp fc opFC x y) =
       PPrefixOp fc opFC x <$> goPTerm y
@@ -434,8 +437,8 @@ mapPTerm f = goPTerm where
       = f $ PDotted fc $ goPTerm x
     goPTerm t@(PImplicit _) = f t
     goPTerm t@(PInfer _) = f t
-    goPTerm (POp fc opFC x y z)
+    goPTerm (POp fc opFC autoBindInfo opName y z)
-      = f $ POp fc opFC x (goPTerm y) (goPTerm z)
+      = f $ POp fc opFC (map f autoBindInfo) opName (goPTerm y) (goPTerm z)
     goPTerm (PPrefixOp fc opFC x y)
       = f $ PPrefixOp fc opFC x $ goPTerm y
     goPTerm (PSectionL fc opFC x y)
@@ -618,7 +621,7 @@ substFC fc = mapPTerm $ \case
   PDotted _ x => PDotted fc x
   PImplicit _ => PImplicit fc
   PInfer _ => PInfer fc
-  POp _ _ x y z => POp fc fc x y z
+  POp _ _ ab nm l r => POp fc fc ab nm l r
   PPrefixOp _ _ x y => PPrefixOp fc fc x y
   PSectionL _ _ x y => PSectionL fc fc x y
   PSectionR _ _ x y => PSectionR fc fc x y

src/Idris/Syntax/Views.idr

@@ -26,7 +26,8 @@ getFnArgs embed fts = go fts [] where
   go (PAutoApp fc f t) = go f . (Auto fc t ::)
   go (PNamedApp fc f n t) = go f . (Named fc n t ::)
   go (PBracketed fc f) = go f
-  go (POp fc opFC op l r) = (PRef opFC op,) . (Explicit fc l ::) . (Explicit fc r ::)
+  -- we don't care about the binder info here
+  go (POp fc opFC _ op l r) = (PRef opFC op,) . (Explicit fc l ::) . (Explicit fc r ::)
   go (PEq fc l r) = (PRef fc $ embed eqName,) . (Explicit fc l ::) . (Explicit fc r ::)
   -- ambiguous, picking the type constructor here
   go (PPair fc l r) = (PRef fc $ embed pairname,) . (Explicit fc l ::) . (Explicit fc r ::)

tests/idris2/operators/operators001/Test.idr

@@ -1,6 +1,14 @@
 
+
 autobind infixr 0 =@
 
 0 (=@) : (a : Type) -> (a -> Type) -> Type
 (=@) a f = (1 x : a) -> f x
 
+
+data S : {ty : Type} -> (x : ty) -> Type where
+  MkS : (x : ty) =@ S x
+  -- same as
+  -- MkS : (1 x : ty) -> S x
+
+