wip app

src/Idris/Desugar.idr

@@ -431,6 +431,8 @@ mutual
   desugarB side ps (PMultiline fc hashtag indent lines)
       = pure $ maybeIApp fc !fromStringName !(expandString side ps fc hashtag !(trimMultiline fc indent lines))
 
+  desugarB side ps (PBindingApp fc expr name bound body)
+      = ?undefined
   -- We only add `fromString` if we are looking at a plain string literal.
   -- Interpolated string literals don't have a `fromString` call since they
   -- are always concatenated with other strings and therefore can never use

src/Idris/Parser.idr

@@ -346,6 +346,15 @@ mutual
       = do boundName <- bounds (UN . Basic <$> decoratedSimpleBinderName fname)
            opBinderTypes fname indents boundName
 
+  bindingExpr : ParseOpts -> OriginDesc -> IndentInfo -> Rule PTerm
+  bindingExpr q fname indents
+      = do leader <- expr pdef fname indents
+           binder <- bounds $ parens fname (opBinder fname indents)
+           decoratedSymbol fname "|"
+           body <- expr pdef fname indents
+           ?whui
+    <|> autobindOp q fname indents
+
   autobindOp : ParseOpts -> OriginDesc -> IndentInfo -> Rule PTerm
   autobindOp q fname indents
       = do binder <- bounds $ parens fname (opBinder fname indents)
@@ -416,6 +425,19 @@ mutual
                         (PImplicit (boundToFC fname (mergeBounds start rest)))
                         rest.val)
 
+--   bindingExpr : OriginDesc -> IndentInfo -> Rule PTerm
+--   bindingExpr fname indents = do
+--     fn <- expr pdef fname indents
+--     bn <- bounds (do symbol "("
+--                      bname <- UN . Basic <$> decoratedSimpleBinderName fname
+--                      symbol ":"
+--                      bexpr <- expr pdef fname indents
+--                      symbol ")"
+--                      pure (bname, bexpr))
+--     decoratedSymbol fname "|"
+--     body <- expr pdef fname indents
+--     ?end
+
   bracketedExpr : OriginDesc -> WithBounds t -> IndentInfo -> Rule PTerm
   bracketedExpr fname s indents
       -- left section. This may also be a prefix operator, but we'll sort

src/Idris/Pretty.idr

@@ -354,6 +354,9 @@ mutual
     prettyPrec d (PSectionR _ _ x op) = parens (pretty x <++> prettyOp op)
     prettyPrec d (PEq fc l r) = parenthesise (d > startPrec) $ prettyPrec Equal l <++> equals <++> prettyPrec Equal r
     prettyPrec d (PBracketed _ tm) = parens (pretty tm)
+    prettyPrec d (PBindingApp _ expr name bound body)
+      = parenthesise (d > startPrec) $ prettyPrec d expr <++>
+        parens (prettyBinder name <++> ":" <++> pretty bound) <++>  "|" <++> prettyPrec d body
     prettyPrec d (PString _ _ xs) = parenthesise (d > startPrec) $ hsep $ punctuate "++" (prettyPStr <$> xs)
     prettyPrec d (PMultiline _ _ indent xs) =
       "multiline" <++>

src/Idris/Syntax.idr

@@ -108,6 +108,7 @@ mutual
        PBracketed : FC -> PTerm' nm -> PTerm' nm
 
        -- Syntactic sugar
+       PBindingApp : FC -> (expr : PTerm' nm) -> (boundName : Name) -> (boundExpr, body : PTerm' nm) -> PTerm' nm
        PString : FC -> (hashtag : Nat) -> List (PStr' nm) -> PTerm' nm
        PMultiline : FC -> (hashtag : Nat) -> (indent : Nat) -> List (List (PStr' nm)) -> PTerm' nm
        PDoBlock : FC -> Maybe Namespace -> List (PDo' nm) -> PTerm' nm
@@ -172,6 +173,7 @@ mutual
   getPTermLoc (PSectionR fc _ _ _) = fc
   getPTermLoc (PEq fc _ _) = fc
   getPTermLoc (PBracketed fc _) = fc
+  getPTermLoc (PBindingApp fc _ _ _ _) = fc
   getPTermLoc (PString fc _ _) = fc
   getPTermLoc (PMultiline fc _ _ _) = fc
   getPTermLoc (PDoBlock fc _ _) = fc
@@ -783,6 +785,8 @@ parameters {0 nm : Type} (toName : nm -> Name)
   showPTermPrec d (PSectionR _ _ x op) = "(" ++ showPTermPrec d x ++ " " ++ showOpPrec d op ++ ")"
   showPTermPrec d (PEq fc l r) = showPTermPrec d l ++ " = " ++ showPTermPrec d r
   showPTermPrec d (PBracketed _ tm) = "(" ++ showPTermPrec d tm ++ ")"
+  showPTermPrec d (PBindingApp _ expr name bound body)
+        = showPTermPrec d expr ++ " (" ++ show name ++ " : " ++ showPTermPrec d bound ++ ") | " ++ showPTermPrec d body
   showPTermPrec d (PString _ _ xs) = join " ++ " $ showPStr <$> xs
   showPTermPrec d (PMultiline _ _ indent xs) = "multiline (" ++ (join " ++ " $ showPStr <$> concat xs) ++ ")"
   showPTermPrec d (PDoBlock _ ns ds)

src/Idris/Syntax/Traversals.idr

@@ -140,6 +140,13 @@ mapPTermM f = goPTerm where
     goPTerm (PBracketed fc x) =
       PBracketed fc <$> goPTerm x
       >>= f
+    goPTerm (PBindingApp fc expr name bound body) =
+     pure (PBindingApp fc)
+       <*> goPTerm expr
+       <*> pure name
+       <*> goPTerm bound
+       <*> goPTerm body
+       >>= f
     goPTerm (PString fc x ys) =
       PString fc x <$> goPStrings ys
       >>= f
@@ -466,6 +473,8 @@ mapPTerm f = goPTerm where
       = f $ PEq fc (goPTerm x) (goPTerm y)
     goPTerm (PBracketed fc x)
       = f $ PBracketed fc $ goPTerm x
+    goPTerm (PBindingApp fc expr name bound body)
+      = f $ PBindingApp fc (goPTerm expr) name (goPTerm bound) (goPTerm body)
     goPTerm (PString fc x ys)
       = f $ PString fc x $ goPStr <$> ys
     goPTerm (PMultiline fc x y zs)
@@ -644,6 +653,7 @@ substFC fc = mapPTerm $ \case
   PSectionR _ _ x y => PSectionR fc fc x y
   PEq _ x y => PEq fc x y
   PBracketed _ x => PBracketed fc x
+  PBindingApp _ expr name bound body => PBindingApp fc expr name bound body
   PString _ x ys => PString fc x ys
   PMultiline _ x y zs => PMultiline fc x y zs
   PDoBlock _ x xs => PDoBlock fc x xs

src/TTImp/ProcessFnOpt.idr

@@ -65,6 +65,10 @@ processFnOpt fc _ ndef (Totality tot)
     = setFlag fc ndef (SetTotal tot)
 processFnOpt fc _ ndef Macro
     = setFlag fc ndef Macro
+processFnOpt fc _ ndef Typebind
+    = ?dunno2
+processFnOpt fc _ ndef Autobind
+    = ?dunno
 processFnOpt fc _ ndef (SpecArgs ns)
     = do defs <- get Ctxt
          Just gdef <- lookupCtxtExact ndef (gamma defs)

src/TTImp/Reflect.idr

@@ -679,6 +679,8 @@ mutual
         = do r' <- reflect fc defs lhs env r
              appCon fc defs (reflectionttimp "Totality") [r']
     reflect fc defs lhs env Macro = getCon fc defs (reflectionttimp "Macro")
+    reflect fc defs lhs env Typebind = getCon fc defs (reflectionttimp "Typebind")
+    reflect fc defs lhs env Autobind = getCon fc defs (reflectionttimp "Autobind")
     reflect fc defs lhs env (SpecArgs r)
         = do r' <- reflect fc defs lhs env r
              appCon fc defs (reflectionttimp "SpecArgs") [r']

src/TTImp/TTImp.idr

@@ -90,6 +90,13 @@ mutual
        IUpdate : FC -> List (IFieldUpdate' nm) -> RawImp' nm -> RawImp' nm
 
        IApp : FC -> RawImp' nm -> RawImp' nm -> RawImp' nm
+       -- Binding application is eventually converted to regular application, just like `let`
+       -- It is kept separate in TTImp for multiple reasons:
+       -- 1. We need to wait for `processFN` to check if the application is binding or not
+       -- 2. We can reconstruct the intended expression in error messages if it's incorrectly used.
+       -- 3. A function name can be overloaded and one of them could be binding while the other isn't
+       IBindingApp : FC -> (expr : RawImp' nm) -> (name : Name) ->
+                     (bound, body : RawImp' nm) -> RawImp' nm
        IAutoApp : FC -> RawImp' nm -> RawImp' nm -> RawImp' nm
        INamedApp : FC -> RawImp' nm -> Name -> RawImp' nm -> RawImp' nm
        IWithApp : FC -> RawImp' nm -> RawImp' nm -> RawImp' nm
@@ -250,6 +257,8 @@ mutual
        Totality : TotalReq -> FnOpt' nm
        Macro : FnOpt' nm
        SpecArgs : List Name -> FnOpt' nm
+       Typebind : FnOpt' nm
+       Autobind : FnOpt' nm
   %name FnOpt' fopt
 
   public export
@@ -276,6 +285,8 @@ mutual
     show (Totality PartialOK) = "partial"
     show Macro = "%macro"
     show (SpecArgs ns) = "%spec " ++ showSep " " (map show ns)
+    show Typebind = "typebind"
+    show Autobind = "autobind"
 
   export
   Eq FnOpt where
@@ -292,6 +303,8 @@ mutual
     (Totality tot_lhs) == (Totality tot_rhs) = tot_lhs == tot_rhs
     Macro == Macro = True
     (SpecArgs ns) == (SpecArgs ns') = ns == ns'
+    Typebind == Typebind = True
+    Autobind == Autobind = True
     _ == _ = False
 
   public export

src/TTImp/TTImp/Functor.idr

@@ -126,6 +126,8 @@ mutual
     map f (Totality tot) = Totality tot
     map f Macro = Macro
     map f (SpecArgs ns) = SpecArgs ns
+    map f Autobind = Autobind
+    map f Typebind = Typebind
 
   export
   Functor ImpTy' where

src/TTImp/TTImp/TTC.idr

@@ -345,6 +345,8 @@ mutual
     toBuf b Unsafe = tag 13
     toBuf b Deprecate = tag 14
     toBuf b (ForeignExport cs) = do tag 15; toBuf b cs
+    toBuf b Typebind = tag 16
+    toBuf b Autobind = tag 17
 
     fromBuf b
         = case !getTag of
@@ -364,6 +366,8 @@ mutual
                13 => pure Unsafe
                14 => pure Deprecate
                15 => do cs <- fromBuf b; pure (ForeignExport cs)
+               16 => pure Typebind
+               17 => pure Autobind
                _ => corrupt "FnOpt"
 
   export

src/TTImp/TTImp/Traversals.idr

@@ -43,6 +43,8 @@ parameters (f : RawImp' nm -> RawImp' nm)
   mapFnOpt Invertible = Invertible
   mapFnOpt (Totality treq) = Totality treq
   mapFnOpt Macro = Macro
+  mapFnOpt Typebind = Typebind
+  mapFnOpt Autobind = Autobind
   mapFnOpt (SpecArgs ns) = SpecArgs ns
 
   export