implement binding application

Author: andrevidela

libs/prelude/Prelude/Interfaces.idr

@@ -551,6 +551,9 @@ sequence : Applicative f => Traversable t => t (f a) -> f (t a)
 sequence = traverse id
 
 ||| Like `traverse` but with the arguments flipped.
+||| You can call this function using binding syntax.
+||| Instead of writing `for xs (\x => f x)` you can write
+||| `for (x := xs) ; f x`
 %inline %tcinline public export
 for : Applicative f => Traversable t => t a -> (a -> f b) -> f (t b)
 for = flip traverse

src/Compiler/Common.idr

@@ -156,7 +156,7 @@ getMinimalDef (Coded ns bin)
              = MkGlobalDef fc name (Erased fc Placeholder) NatSet.empty NatSet.empty NatSet.empty NatSet.empty mul
                            Scope.empty (specified Public) (MkTotality Unchecked IsCovering) False
                            [] Nothing refsR False False True
-                           None cdef Nothing [] Nothing
+                           None cdef Nothing [] Nothing NotBinding
          pure (def, Just (ns, bin))
 
 -- ||| Recursively get all calls in a function definition

src/Core/Binary.idr

@@ -30,7 +30,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 = 2025_08_08_00
+ttcVersion = 2025_08_14_00
 
 export
 checkTTCVersion : String -> Int -> Int -> Core ()

src/Core/Context.idr

@@ -10,6 +10,7 @@ import public Core.Name
 import        Core.Options
 import public Core.Options.Log
 import public Core.TT
+import public Core.WithData
 
 import Libraries.Utils.Binary
 import Libraries.Utils.Path
@@ -325,10 +326,11 @@ commitCtxt ctxt
 ||| @vis  Visibility, defaulting to private
 ||| @def  actual definition
 export
-newDef : (fc : FC) -> (n : Name) -> (rig : RigCount) -> (vars : Scope) ->
+newDef : {default NotBinding bind : BindingModifier} ->
+         (fc : FC) -> (n : Name) -> (rig : RigCount) -> (vars : Scope) ->
          (ty : ClosedTerm) -> (vis : WithDefault Visibility Private) -> (def : Def) -> GlobalDef
 newDef fc n rig vars ty vis def
-    = MkGlobalDef
+  = MkGlobalDef
         { location = fc
         , fullname = n
         , type = ty
@@ -352,6 +354,7 @@ newDef fc n rig vars ty vis def
         , namedcompexpr = Nothing
         , sizeChange = []
         , schemeExpr = Nothing
+        , bindingMode = bind
         }
 
 -- Rewrite rules, applied after type checking, for runtime code only
@@ -1368,6 +1371,7 @@ addBuiltin n ty tot op
          , namedcompexpr = Nothing
          , sizeChange = []
          , schemeExpr = Nothing
+         , bindingMode = NotBinding
          }
 
 export

src/Core/Context/Context.idr

@@ -177,7 +177,7 @@ Show Def where
 
 public export
 Constructor' : Type -> Type
-Constructor' = AddFC . WithName . WithArity
+Constructor' = AddFC . WithName . WithArity . AddMetadata Bind'
 
 public export
 Constructor : Type
@@ -331,6 +331,7 @@ record GlobalDef where
   namedcompexpr : Maybe NamedDef
   sizeChange : List SCCall
   schemeExpr : Maybe (SchemeMode, SchemeObj Write)
+  bindingMode : BindingModifier
 
 export
 getDefNameType : GlobalDef -> NameType

src/Core/Context/Data.idr

@@ -101,7 +101,7 @@ addData vars vis tidx (MkData con datacons)
          log "declare.data.parameters" 20 $
             "Positions of parameters for datatype" ++ show tyName ++
             ": " ++ show paramPositions
-         let tydef = newDef con.fc tyName top vars con.val (specified vis)
+         let tydef = newDef {bind = con.bind} con.fc tyName top vars con.val (specified vis)
                             (TCon con.arity
                                   paramPositions
                                   allPos
@@ -120,7 +120,7 @@ addData vars vis tidx (MkData con datacons)
     addDataConstructors tag [] gam = pure gam
     addDataConstructors tag (con :: cs) gam
         = do let conName = con.name.val
-             let condef = newDef con.fc conName top vars con.val (specified $ conVisibility vis) (DCon tag con.arity Nothing)
+             let condef = newDef {bind = con.bind} con.fc conName top vars con.val (specified $ conVisibility vis) (DCon tag con.arity Nothing)
              -- Check 'n' is undefined
              Nothing <- lookupCtxtExact conName gam
                  | Just gdef => throw (AlreadyDefined con.fc conName)

src/Core/Core.idr

@@ -890,6 +890,14 @@ namespace Binder
   traverse f (PLet fc c val ty) = pure $ PLet fc c !(f val) !(f ty)
   traverse f (PVTy fc c ty) = pure $ PVTy fc c !(f ty)
 
+namespace BindingInfo
+  export
+  traverse : (a -> Core b) -> BindingInfo a -> Core (BindingInfo b)
+  traverse f (BindType name type) = BindType <$> f name <*> f type
+  traverse f (BindExpr name expr) = BindExpr <$> f name <*> f expr
+  traverse f (BindExplicitType name type expr)
+    = BindExplicitType <$> f name <*> f type <*> f expr
+
 export
 mapTermM : ({vars : _} -> Term vars -> Core (Term vars)) ->
            ({vars : _} -> Term vars -> Core (Term vars))

src/Core/FC.idr

@@ -230,3 +230,4 @@ Pretty Void FC where
   pretty (MkVirtualFC ident startPos endPos) = byShow ident <+> colon
                  <+> prettyPos startPos <+> pretty "--"
                  <+> prettyPos endPos
+

src/Core/Name/Namespace.idr

@@ -304,3 +304,7 @@ dpairNS = mkNamespace "Builtin.DPair"
 export
 natNS : Namespace
 natNS = mkNamespace "Data.Nat"
+
+export
+allQuantifiersNS : Namespace
+allQuantifiersNS = mkNamespace "Data.List.Quantifiers.All"

src/Core/Options/Log.idr

@@ -106,6 +106,7 @@ knownTopics = [
     ("elab.as", Nothing),
     ("elab.bindnames", Nothing),
     ("elab.binder", Nothing),
+    ("elab.bindApp", Just "Elaborating binding application"),
     ("elab.case", Nothing),
     ("elab.def.local", Nothing),
     ("elab.delay", Nothing),