From 77c53a45613a8f56e029f7ce9f747dcf23d93300 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andr=C3=A9=20Videla?= Date: Mon, 25 Aug 2025 14:26:15 +0100 Subject: [PATCH 1/8] implement binding application --- docs/source/reference/binding-application.rst | 172 +++++++++++++ libs/contrib/Text/Parser.idr | 2 +- src/Compiler/Common.idr | 2 +- src/Core/Binary.idr | 2 +- src/Core/Context.idr | 8 +- src/Core/Context/Context.idr | 3 +- src/Core/Context/Data.idr | 4 +- src/Core/Core.idr | 8 + src/Core/FC.idr | 1 + src/Core/Name/Namespace.idr | 1 + src/Core/Options/Log.idr | 1 + src/Core/Reflect.idr | 8 + src/Core/TT.idr | 85 ++++--- src/Core/TTC.idr | 34 ++- src/Core/WithData.idr | 18 +- src/Idris/Desugar.idr | 46 ++-- src/Idris/Elab/Implementation.idr | 6 +- src/Idris/Elab/Interface.idr | 16 +- src/Idris/Parser.idr | 225 ++++++++++-------- src/Idris/Pretty.idr | 7 +- src/Idris/REPL.idr | 2 +- src/Idris/Resugar.idr | 20 +- src/Idris/Syntax.idr | 42 ++-- src/Idris/Syntax/TTC.idr | 12 - src/Idris/Syntax/Traversals.idr | 21 +- src/Libraries/Data/WithData.idr | 5 +- src/TTImp/BindImplicits.idr | 2 +- src/TTImp/Elab/BindingApp.idr | 74 ++++++ src/TTImp/Elab/Local.idr | 19 +- src/TTImp/Elab/Term.idr | 3 + src/TTImp/Parser.idr | 30 +-- src/TTImp/ProcessData.idr | 61 ++--- src/TTImp/ProcessDef.idr | 5 +- src/TTImp/ProcessFnOpt.idr | 6 + src/TTImp/ProcessRecord.idr | 50 ++-- src/TTImp/ProcessType.idr | 2 +- src/TTImp/Reflect.idr | 39 ++- src/TTImp/TTImp.idr | 60 +++-- src/TTImp/TTImp/Functor.idr | 5 + src/TTImp/TTImp/TTC.idr | 9 +- src/TTImp/TTImp/Traversals.idr | 2 + src/TTImp/Utils.idr | 9 +- tests/idris2/basic/binding001/Test.idr | 50 ++++ tests/idris2/basic/binding001/expected | 12 + tests/idris2/basic/binding001/run | 4 + tests/idris2/basic/binding002/Test.idr | 21 ++ tests/idris2/basic/binding002/expected | 1 + tests/idris2/basic/binding002/run | 3 + tests/idris2/operators/operators002/Test.idr | 4 +- 49 files changed, 871 insertions(+), 351 deletions(-) create mode 100644 docs/source/reference/binding-application.rst create mode 100644 src/TTImp/Elab/BindingApp.idr create mode 100644 tests/idris2/basic/binding001/Test.idr create mode 100644 tests/idris2/basic/binding001/expected create mode 100755 tests/idris2/basic/binding001/run create mode 100644 tests/idris2/basic/binding002/Test.idr create mode 100644 tests/idris2/basic/binding002/expected create mode 100755 tests/idris2/basic/binding002/run diff --git a/docs/source/reference/binding-application.rst b/docs/source/reference/binding-application.rst new file mode 100644 index 00000000000..c8a584e5eb1 --- /dev/null +++ b/docs/source/reference/binding-application.rst @@ -0,0 +1,172 @@ + +.. _binding: + +********* +Binding Application +********* + +Binding application allows to overload the syntax of function application to better express the +semantics of dependent types. Take for example the mathematical notation for Sigma-types: +:math:`\Sigma x \in \mathbb{N} . Fin\ x` it binds the variable ``x`` and makes it available in the +scope after the dot. Another example is the mathematical notation for ``forall``: +:math:`\forall x \in \mathbb{N} | p x` it states that for all values ``x`` in the set of natural +number, the property ``p`` holds. + +Without any additional syntactic help those two types are only expressible using a lambda: + +.. code-block:: idris + record Sigma (a : Type) (p : a -> Type) where + fst : a + snd : p fst + + record Pi (a : Type) (p : a -> Type) where + fn : (x : a) -> p x + + sigmaExample : Sigma Nat (\n => Vect n Int) + + piExample : Pi Nat (\n => Vect n Int) + + +Ideally, instead of relying on a lambda, we would like to write something closer to the original +mathematical notation, binding application allows the following syntax: + +.. code-block:: idris + sigmaExample' : Sigma (n : Nat) | Vect n Int + + piExample' : Pi (n : Nat) | Vect n Int + +Binding Types +============= + +The first way to use binding application is to bind a type to a name. If +we take our ``Sigma`` example again it means that we need to tell the compiler that the type +constructor can be used with binding syntax. We do this by annotating the type declaration with +the ``typebind`` keyword. + + +.. code-block:: idris + typebind + record Sigma (a : Type) (p : a -> Type) where + constructor MkSigma + fst : a + snd : p fst + + +The type constructor can now be called with this syntax: ``Sigma (n : Nat) | Vect n Int``. And it reads +"Sigma ``n`` of type ``Nat`` such that ``Vect n Int``. This reading is appropriated from the +mathematical notation :math:`\forall x \in \mathbb{N} | p x` which reads the same. +We can also annotate functions with the same keyword, for example the following alias is allowed: + +.. code-block:: idris + typebind + ∃ : (a : Type) -> (p : a -> Type) -> Type + ∃ = Sigma + +In the implementation of this function we've used the ``Sigma`` type-constructor without any binding +syntax. That is because marking something as binding does not stop them from using them with regular +function application, for example the following is allowed: + +.. code-block:: idris + -- binding syntax from our alias + s1 : ∃ (n : Nat) | Fin n + s1 = ... + + -- pointfree notation is allowed + s2 : Sigma Nat Fin + s2 = ... + + s3 : (Nat -> Type) -> Type + s3 = Sigma Nat -- partial application is allowed + + +We've seen that you can annotate functions and type constructors, you can also annotate data-constructors. For example, to annotate a record constructor add the keyword before the `constructor` keyword: + +.. code-block:: idris + record Container where + typebind + constructor MkCont + goal : Type + solution : goal -> Type + + ListCont : Container + ListCont = MkCont (n : Nat) | Fin n + +You can also annotate constructors for data: + +.. code-block:: idris + data Desc : Type where + -- normal constructors + One : Desc + Ind : Desc -> Desc + + -- binding data constructor + typebind + Sig : (s : Type) -> (s -> Desc) -> Desc + +Binding application is a desugaring that takes an input of the form ``expr1 (name : type) | expr2`` +and maps it to a program ``expr1 type (\name : Type => expr2)``. Binding application will disambiguate +between binding and non-binding calls for example, the following works: + +.. code-block:: idris + namespace E1 + export + record Exists (a : Type) (p : a -> Type) where + + namespace E2 + export typebind + record Exists (a : Type) (p : a -> Type) where + + ok : Exists (n : Nat) | Vect n a + + +The compiler will automatically pick ``Exists`` from ``E2`` because the other one is not marked as +binding. However, when using regular function application, the call must be disambiguated: + +.. code-block:: idris + failing + noOK : Exists Nat Fin + + unambiguous : E1.Exists Nat Fin + + + +Binding Arbitrary Values +======================== + +Sometimes, we still want to using binding application syntax, but we are not binding a type. In those +cases you want to use the ``autobind`` feature to infer the type of the value being bound. The keyword +works in the same places as the ``typebind`` keyword, that is: + +On type constructors + +.. code-block:: idris + autobind + record StringProp : (str : String) -> (String -> Type) -> Type where + + autobind + data MaybeProp : (m : Maybe a) -> (a -> Type) -> Type where + +On data constructor: + +.. code-block:: idris + +on functions: + +.. code-block:: idris + autobind + for : (List a) -> (a -> IO ()) -> IO () + for ls fn = traverse fn ls >> pure () + + +Instead of using ``:`` as a separator, we use ``<-`` and so the last function can be used this way: + +.. code-block:: idris + main : IO () + main = for (x <- ['a' .. 'z']) | + putCharLn x + +The desguaring works in a similar way except that the type of the argument in the lambda has to be +inferred. ``expr1 (name <- expr2) | expr3`` desugars to ``expr1 expr2 (\name : ? => expr3)``. + +Like typebind, you can use regular function application and partial application with ``autobind`` +definitions. diff --git a/libs/contrib/Text/Parser.idr b/libs/contrib/Text/Parser.idr index f9fbb561b3b..515f6f06861 100644 --- a/libs/contrib/Text/Parser.idr +++ b/libs/contrib/Text/Parser.idr @@ -1,7 +1,7 @@ module Text.Parser import Data.Bool -import public Data.Nat +import Data.Nat import public Data.List1 import public Text.Parser.Core diff --git a/src/Compiler/Common.idr b/src/Compiler/Common.idr index 0bf03acc1aa..254d01e4e9f 100644 --- a/src/Compiler/Common.idr +++ b/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 diff --git a/src/Core/Binary.idr b/src/Core/Binary.idr index c24195d06dd..f3124c44484 100644 --- a/src/Core/Binary.idr +++ b/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_16_00 +ttcVersion = 2025_08_20_00 export checkTTCVersion : String -> Int -> Int -> Core () diff --git a/src/Core/Context.idr b/src/Core/Context.idr index 5d8fe0ebebf..32a46b1dd99 100644 --- a/src/Core/Context.idr +++ b/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 @@ -1372,6 +1375,7 @@ addBuiltin n ty tot op , namedcompexpr = Nothing , sizeChange = [] , schemeExpr = Nothing + , bindingMode = NotBinding } export diff --git a/src/Core/Context/Context.idr b/src/Core/Context/Context.idr index 14dc62a92a6..26b4172e067 100644 --- a/src/Core/Context/Context.idr +++ b/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 diff --git a/src/Core/Context/Data.idr b/src/Core/Context/Data.idr index 371f3bec284..3445db30618 100644 --- a/src/Core/Context/Data.idr +++ b/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) diff --git a/src/Core/Core.idr b/src/Core/Core.idr index 7cd9924e68d..44e52f869a4 100644 --- a/src/Core/Core.idr +++ b/src/Core/Core.idr @@ -896,6 +896,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)) diff --git a/src/Core/FC.idr b/src/Core/FC.idr index 4e3e704b233..b495ab2dbee 100644 --- a/src/Core/FC.idr +++ b/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 + diff --git a/src/Core/Name/Namespace.idr b/src/Core/Name/Namespace.idr index 7e683b5ef0b..3706eae943c 100644 --- a/src/Core/Name/Namespace.idr +++ b/src/Core/Name/Namespace.idr @@ -304,3 +304,4 @@ dpairNS = mkNamespace "Builtin.DPair" export natNS : Namespace natNS = mkNamespace "Data.Nat" + diff --git a/src/Core/Options/Log.idr b/src/Core/Options/Log.idr index db188cc67e6..ae3dc61140f 100644 --- a/src/Core/Options/Log.idr +++ b/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), diff --git a/src/Core/Reflect.idr b/src/Core/Reflect.idr index 6f4782d40fd..e1556bbbfa3 100644 --- a/src/Core/Reflect.idr +++ b/src/Core/Reflect.idr @@ -10,6 +10,7 @@ import Core.TT import Core.Value import Libraries.Data.WithDefault +import Libraries.Data.WithData %default covering @@ -885,6 +886,13 @@ Reflect a => Reflect (WithFC a) where val' <- reflect fc defs lhs env value.val appCon fc defs (reflectiontt "MkFCVal") [Erased fc Placeholder, loc', val'] +export +Reflect BindingModifier where + reflect fc defs lhs env NotBinding = getCon fc defs (reflectiontt "NotBinding") + reflect fc defs lhs env Autobind = getCon fc defs (reflectiontt "Autobind") + reflect fc defs lhs env Typebind = getCon fc defs (reflectiontt "Typebind") + + {- -- Reflection of well typed terms: We don't reify terms because that involves -- type checking, but we can reflect them diff --git a/src/Core/TT.idr b/src/Core/TT.idr index 621d9067f44..0a29d10f9c0 100644 --- a/src/Core/TT.idr +++ b/src/Core/TT.idr @@ -196,61 +196,84 @@ Eq FixityInfo where public export data FixityDeclarationInfo = UndeclaredFixity | DeclaredFixity FixityInfo --- Left-hand-side information for operators, carries autobind information --- an operator can either be --- - not autobind, a regular operator --- - binding types, such that `(nm : ty) =@ fn nm` desugars into `(=@) ty (\(nm : ty) => fn nm)` --- - binding expressing with an inferred type such that --- `(nm := exp) =@ fn nm` desugars into `(=@) exp (\(nm : ?) => fn nm)` --- - binding both types and expression such that --- `(nm : ty := exp) =@ fn nm` desugars into `(=@) exp (\(nm : ty) => fn nm)` +-- Binding information for binding application and binding operators +-- A binder can either +-- - bind types `(t : a)` +-- - bind expressions with an inferred type such that `(x := v)` +-- - bind an expression with an explicit type annotation `(x : a := v)` public export -data OperatorLHSInfo : tm -> Type where - -- Traditional operator wihtout binding, carries the lhs - NoBinder : (lhs : tm) -> OperatorLHSInfo tm - -- (nm : ty) =@ fn x - BindType : (name : tm) -> (ty : tm) -> OperatorLHSInfo tm - -- (nm := exp) =@ fn nm - BindExpr : (name : tm) -> (expr : tm) -> OperatorLHSInfo tm - -- (nm : ty := exp) =@ fn nm - BindExplicitType : (name : tm) -> (type, expr : tm) -> OperatorLHSInfo tm +data BindingInfo : (tm : Type) -> Type where + -- (name : type) + BindType : (name : tm) -> (type : tm) -> BindingInfo tm + -- (name := expr) + BindExpr : (name : tm) -> (expr : tm) -> BindingInfo tm + -- (name : type := expr) + BindExplicitType : (name : tm) -> (type, expr : tm) -> BindingInfo tm + export -Show (OperatorLHSInfo tm) where - show (NoBinder lhs) = "regular" +Show (BindingInfo tm) where show (BindType name ty) = "type-binding (typebind)" show (BindExpr name expr) = "automatically-binding (autobind)" show (BindExplicitType name type expr) = "automatically-binding (autobind)" -%name OperatorLHSInfo opInfo +%name BindingInfo opInfo export -Functor OperatorLHSInfo where - map f (NoBinder lhs) = NoBinder $ f lhs +Functor BindingInfo where map f (BindType nm lhs) = BindType (f nm) (f lhs) map f (BindExpr nm lhs) = BindExpr (f nm) (f lhs) map f (BindExplicitType nm ty lhs) = BindExplicitType (f nm) (f ty) (f lhs) +||| Left-hand-side of a binary operator. Could be either a term or a binder +public export +data OperatorLHSInfo tm = + NoBinder tm | LHSBinder (BindingInfo tm) + +export +Show (OperatorLHSInfo tm) where + show (NoBinder lhs) = "regular" + show (LHSBinder bd) = show bd + +export +Functor OperatorLHSInfo where + map f (NoBinder x) = NoBinder (f x) + map f (LHSBinder bd) = LHSBinder (map f bd) + +export +(.getBoundName) : BindingInfo tm -> tm +(.getBoundName) (BindExpr n _) = n +(.getBoundName) (BindType n _) = n +(.getBoundName) (BindExplicitType n _ _) = n + +export +(.getBoundExpr) : BindingInfo tm -> tm +(.getBoundExpr) (BindExpr _ t) = t +(.getBoundExpr) (BindType _ t) = t +(.getBoundExpr) (BindExplicitType _ _ t) = t + +export +(.getBindingMode) : BindingInfo tm -> BindingModifier +(.getBindingMode) (BindType name ty) = Typebind +(.getBindingMode) (BindExpr name expr) = Autobind +(.getBindingMode) (BindExplicitType name type expr) = Autobind + export (.getLhs) : OperatorLHSInfo tm -> tm (.getLhs) (NoBinder lhs) = lhs -(.getLhs) (BindExpr _ lhs) = lhs -(.getLhs) (BindType _ lhs) = lhs -(.getLhs) (BindExplicitType _ _ lhs) = lhs +(.getLhs) (LHSBinder lhs) = lhs.getBoundExpr export (.getBoundPat) : OperatorLHSInfo tm -> Maybe tm (.getBoundPat) (NoBinder lhs) = Nothing -(.getBoundPat) (BindType name ty) = Just name -(.getBoundPat) (BindExpr name expr) = Just name -(.getBoundPat) (BindExplicitType name type expr) = Just name +(.getBoundPat) (LHSBinder $ BindType name ty) = Just name +(.getBoundPat) (LHSBinder $ BindExpr name expr) = Just name +(.getBoundPat) (LHSBinder $ BindExplicitType name type expr) = Just name export (.getBinder) : OperatorLHSInfo tm -> BindingModifier (.getBinder) (NoBinder lhs) = NotBinding -(.getBinder) (BindType name ty) = Typebind -(.getBinder) (BindExpr name expr) = Autobind -(.getBinder) (BindExplicitType name type expr) = Autobind +(.getBinder) (LHSBinder lhs) = lhs.getBindingMode public export data TotalReq = Total | CoveringOnly | PartialOK diff --git a/src/Core/TTC.idr b/src/Core/TTC.idr index 2bdb08a04ac..eb4d5f90ac6 100644 --- a/src/Core/TTC.idr +++ b/src/Core/TTC.idr @@ -13,11 +13,14 @@ import Core.TT import Data.IOArray import Data.List1 +import Data.List.Quantifiers import Data.Vect +import Decidable.Equality import Libraries.Data.NameMap import Libraries.Data.NatSet import Libraries.Data.SparseMatrix import Libraries.Data.WithDefault +import Libraries.Data.WithData import Libraries.Utils.Binary import Libraries.Utils.Scheme @@ -80,6 +83,31 @@ TTC FC where _ => corrupt "FC" export +TTC BindingModifier where + toBuf NotBinding = tag 0 + toBuf Autobind = tag 1 + toBuf Typebind = tag 2 + + fromBuf + = case !getTag of + 0 => pure NotBinding + 1 => pure Autobind + 2 => pure Typebind + _ => corrupt "BindingModifier" + +export +TTC a => TTC (BindingInfo a) where + toBuf (BindType name type) = tag 0 >> toBuf name >> toBuf type + toBuf (BindExpr name expr) = tag 1 >> toBuf name >> toBuf expr + toBuf (BindExplicitType name type expr) = tag 2 >> toBuf name >> toBuf expr + + fromBuf + = case !getTag of + 0 => BindType <$> fromBuf <*> fromBuf + 1 => BindExpr <$> fromBuf <*> fromBuf + 2 => BindExplicitType <$> fromBuf <*> fromBuf <*> fromBuf + _ => corrupt "BindingInfo" +export TTC Name where -- for efficiency reasons we do not encode UserName separately -- hence the nested pattern matches on UN (Basic/Hole/Field) @@ -1156,6 +1184,7 @@ TTC GlobalDef where toBuf (invertible gdef) toBuf (noCycles gdef) toBuf (sizeChange gdef) + toBuf (bindingMode gdef) fromBuf = do cdef <- fromBuf @@ -1178,12 +1207,13 @@ TTC GlobalDef where inv <- fromBuf c <- fromBuf sc <- fromBuf + bm <- fromBuf pure (MkGlobalDef loc name ty eargs seargs specargs iargs mul vars vis - tot hatch fl refs refsR inv c True def cdef Nothing sc Nothing) + tot hatch fl refs refsR inv c True def cdef Nothing sc Nothing bm) else pure (MkGlobalDef loc name (Erased loc Placeholder) NatSet.empty NatSet.empty NatSet.empty NatSet.empty mul Scope.empty (specified Public) unchecked False [] refs refsR - False False True def cdef Nothing [] Nothing) + False False True def cdef Nothing [] Nothing NotBinding) export TTC Transform where diff --git a/src/Core/WithData.idr b/src/Core/WithData.idr index e296175a8fb..d62115b3887 100644 --- a/src/Core/WithData.idr +++ b/src/Core/WithData.idr @@ -109,6 +109,11 @@ setFC : {n : Nat} -> WithData fields a -> WithData fields a setFC fc = WithData.set "fc" fc @{inRange} +||| Attach binding and file context information to a type +public export +FCBind : Type -> Type +FCBind = AddMetadata Bind' . AddMetadata FC' + ||| A wrapper for a value with a file context. public export MkFCVal : FC -> ty -> WithFC ty @@ -180,8 +185,8 @@ Name' = "name" :-: WithFC Name ||| Extract the name out of the metadata. export (.name) : {n : Nat} -> - (inRange : NameInRange "name" fields === Just (n, WithFC Name)) => - WithData fields a -> WithFC Name + (inRange : NameInRange "name" fields === Just (n, nm)) => + WithData fields a -> nm (.name) = WithData.get "name" @{inRange} ||| Extract the name out of the metadata. @@ -199,20 +204,19 @@ WithName = AddMetadata Name' ||| the "tyname" label containing a `WithFC Name` for metadata records. Typically used for type names. public export TyName' : KeyVal -TyName' = "tyname" :-: WithFC Name +TyName' = "tyname" :-: FCBind Name ||| Extract the "tyname" value from the metadata record export (.tyName) : {n : Nat} -> - (inRange : NameInRange "tyname" fields === Just (n, WithFC Name)) => - WithData fields a -> WithFC Name + (inRange : NameInRange "tyname" fields === Just (n, FCBind Name)) => + WithData fields a -> FCBind Name (.tyName) = WithData.get "tyname" @{inRange} - ||| Attach documentation, binding and location information to a type public export DocBindFC : Type -> Type -DocBindFC = WithData [ Doc', Bind', FC' ] +DocBindFC = AddMetadata Doc' . AddMetadata Bind' . AddMetadata FC' ||| the "mname" label containing a `Maybe (WithFC Name)` for metadata records public export diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr index 39436940244..530696eef38 100644 --- a/src/Idris/Desugar.idr +++ b/src/Idris/Desugar.idr @@ -33,6 +33,7 @@ import TTImp.BindImplicits import TTImp.Parser import TTImp.ProcessType import TTImp.TTImp +import TTImp.TTImp.Functor import TTImp.Utils import Libraries.Data.IMaybe @@ -187,9 +188,9 @@ checkConflictingBinding opName foundFixity use_site rhs isCompatible UndeclaredFixity (NoBinder lhs) = True isCompatible UndeclaredFixity _ = False isCompatible (DeclaredFixity fixInfo) (NoBinder lhs) = fixInfo.bindingInfo == NotBinding - isCompatible (DeclaredFixity fixInfo) (BindType name ty) = fixInfo.bindingInfo == Typebind - isCompatible (DeclaredFixity fixInfo) (BindExpr name expr) = fixInfo.bindingInfo == Autobind - isCompatible (DeclaredFixity fixInfo) (BindExplicitType name type expr) + isCompatible (DeclaredFixity fixInfo) (LHSBinder $ BindType name ty) = fixInfo.bindingInfo == Typebind + isCompatible (DeclaredFixity fixInfo) (LHSBinder $ BindExpr name expr) = fixInfo.bindingInfo == Autobind + isCompatible (DeclaredFixity fixInfo) (LHSBinder $ BindExplicitType name type expr) = fixInfo.bindingInfo == Autobind keepCompatibleBinding : BindingModifier -> (Name, GlobalDef) -> Core Bool @@ -400,6 +401,9 @@ mutual = pure $ IAutoApp fc !(desugarB side ps x) !(desugarB side ps y) desugarB side ps (PWithApp fc x y) = pure $ IWithApp fc !(desugarB side ps x) !(desugarB side ps y) + desugarB side ps (PBindingApp nm bind scope) + = pure $ IBindingApp nm !(traverse (traverse (desugarB side ps)) bind) + !(traverse (desugarB side ps) scope) desugarB side ps (PNamedApp fc x argn y) = pure $ INamedApp fc !(desugarB side ps x) argn !(desugarB side ps y) desugarB side ps (PDelayed fc r ty) @@ -844,20 +848,20 @@ mutual r' <- desugarTree side ps r pure (PApp loc (PApp loc (PRef opFC op.toName) l') r') -- (x : ty) =@ f x ==>> (=@) ty (\x : ty => f x) - desugarTree side ps (Infix loc opFC (op, Just (BindType pat lhs)) l r) + desugarTree side ps (Infix loc opFC (op, Just (LHSBinder $ BindType pat lhs)) l r) = do l' <- desugarTree side ps l body <- desugarTree side ps r pure $ PApp loc (PApp loc (PRef opFC op.toName) l') (PLam loc top Explicit pat l' body) -- (x := exp) =@ f x ==>> (=@) exp (\x : ? => f x) - desugarTree side ps (Infix loc opFC (op, Just (BindExpr pat lhs)) l r) + desugarTree side ps (Infix loc opFC (op, Just (LHSBinder $ BindExpr pat lhs)) l r) = do l' <- desugarTree side ps l body <- desugarTree side ps r pure $ PApp loc (PApp loc (PRef opFC op.toName) l') (PLam loc top Explicit pat (PInfer opFC) body) -- (x : ty := exp) =@ f x ==>> (=@) exp (\x : ty => f x) - desugarTree side ps (Infix loc opFC (op, Just (BindExplicitType pat ty expr)) l r) + desugarTree side ps (Infix loc opFC (op, Just (LHSBinder $ BindExplicitType pat ty expr)) l r) = do l' <- desugarTree side ps l body <- desugarTree side ps r pure $ PApp loc (PApp loc (PRef opFC op.toName) l') @@ -901,12 +905,12 @@ mutual {auto u : Ref UST UState} -> {auto m : Ref MD Metadata} -> {auto o : Ref ROpts REPLOpts} -> - List Name -> PTypeDecl -> Core (List ImpTy) + List Name -> AddMetadata Bind' PTypeDecl -> Core (List ImpTy) desugarType ps pty@(MkWithData _ $ MkPTy names d ty) = flip Core.traverse (forget names) $ \(doc, n) : (String, WithFC Name) => do addDocString n.val (d ++ doc) syn <- get Syn - pure $ Mk [pty.fc, n] !(bindTypeNames pty.fc (usingImpl syn) + pure $ Mk [pty.fc, NotBinding :+ n] !(bindTypeNames pty.fc (usingImpl syn) ps !(desugar AnyExpr ps ty)) -- Attempt to get the function name from a function pattern. For example, @@ -994,7 +998,7 @@ mutual List Name -> (doc : String) -> PDataDecl -> Core ImpData desugarData ps doc (MkPData fc n tycon opts datacons) - = do addDocString n doc + = do addDocString n.val doc syn <- get Syn mm <- traverse (desugarType ps) datacons pure $ MkImpData fc n @@ -1004,7 +1008,7 @@ mutual opts (concat mm) desugarData ps doc (MkPLater fc n tycon) - = do addDocString n doc + = do addDocString n.val doc syn <- get Syn pure $ MkImpLater fc n !(bindTypeNames fc (usingImpl syn) ps !(desugar AnyExpr ps tycon)) @@ -1023,7 +1027,7 @@ mutual syn <- get Syn p' <- traverse (desugar AnyExpr ps) field.val.info ty' <- bindTypeNames field.fc (usingImpl syn) ps !(desugar AnyExpr ps field.val.boundType) - pure (Mk [field.fc, field.rig, n] (MkPiBindData p' ty')) + pure (Mk [field.fc, field.rig, AddDef (AddDef n)] (MkPiBindData p' ty')) where toRF : Name -> Name @@ -1141,7 +1145,7 @@ mutual $ for (map (boundType . val) paramList) $ findUniqueBindableNames pp.fc True (ps ++ paramNames) [] - let paramsb = map {f = List1} (map {f = WithData _} (mapType (doBind pnames))) params' + let paramsb = map {f = List1} (WithData.map (mapType (doBind pnames))) params' pure [IParameters pp.fc paramsb (concat pds')] where getArgs : Either (List1 PlainBinder) @@ -1150,12 +1154,12 @@ mutual getArgs (Left params) = traverseList1 (\ty => do ty' <- desugar AnyExpr ps ty.val - pure (Mk [top, ty.name] (MkPiBindData Explicit ty'))) params + pure (Mk [top, AddDef (AddDef ty.name)] (MkPiBindData Explicit ty'))) params getArgs (Right params) = join <$> traverseList1 (\(MkPBinder info (MkBasicMultiBinder rig n ntm)) => do tm' <- desugar AnyExpr ps ntm i' <- traverse (desugar AnyExpr ps) info - let allbinders = map (\nn => Mk [rig, nn] (MkPiBindData i' tm')) n + let allbinders = map (\nn => Mk [rig, AddDef (AddDef nn)] (MkPiBindData i' tm')) n pure allbinders) params desugarDecl ps use@(MkWithData _ $ PUsing uimpls uds) @@ -1262,12 +1266,12 @@ mutual mkRecType (MkPBinder p (MkBasicMultiBinder c (n ::: x :: xs) t) :: ts) = PPi rec.fc c p (Just n.val) t (mkRecType (MkPBinder p (MkBasicMultiBinder c (x ::: xs) t) :: ts)) desugarDecl ps rec@(MkWithData _ $ PRecord doc vis mbtot (MkPRecord tn params opts conname_in fields)) - = do addDocString tn doc + = do addDocString tn.val doc params' : List ImpParameter <- map concat $ for params $ \ (MkPBinder info (MkBasicMultiBinder rig names tm)) => do tm' <- desugar AnyExpr ps tm p' <- mapDesugarPiInfo ps info - let allBinders = map (\nm => Mk [rig, nm] (MkPiBindData p' tm')) (forget names) + let allBinders = map (\nm => Mk [rig, AddDef (AddDef nm)] (MkPiBindData p' tm')) (forget names) pure allBinders let fnames : List Name = concatMap getfname fields let paramNames : List Name = concatMap (map val . forget . names . bind) params @@ -1280,13 +1284,15 @@ mutual else [] let paramsb : List ImpParameter = map (map $ mapType $ doBind bnames) params' - let recName = nameRoot tn + let recName = nameRoot tn.val fields' : List (List IField) <- for fields (desugarField (ps ++ fnames ++ paramNames) (mkNamespace recName)) - let conname : Name = maybe (mkConName tn) val conname_in - whenJust (get "doc" <$> conname_in) (addDocString conname) + let conname : DocBindFC Name := fromMaybe (MkDef (mkConName tn.val)) conname_in + whenJust (get "doc" <$> conname_in) (addDocString conname.val) pure [IRecord rec.fc (Just recName) - vis mbtot (Mk [rec.fc] $ MkImpRecord (Mk [NoFC tn] paramsb) (Mk [NoFC conname, opts] (concat fields')))] + vis mbtot + (Mk [rec.fc] $ MkImpRecord (Mk [tn] paramsb) + (Mk [conname.drop, opts] (concat fields')))] where getfname : PField -> List Name getfname x = map val x.names diff --git a/src/Idris/Elab/Implementation.idr b/src/Idris/Elab/Implementation.idr index 11776ee212d..f5f1ba6f95d 100644 --- a/src/Idris/Elab/Implementation.idr +++ b/src/Idris/Elab/Implementation.idr @@ -55,7 +55,7 @@ bindConstraints fc p ((n, ty) :: rest) sc bindImpls : List (AddFC (ImpParameter' RawImp)) -> RawImp -> RawImp bindImpls [] ty = ty bindImpls (binder :: rest) sc - = IPi binder.fc binder.rig binder.val.info (Just binder.nameVal) binder.val.boundType (bindImpls rest sc) + = IPi binder.fc binder.rig binder.val.info (Just binder.name.val) binder.val.boundType (bindImpls rest sc) addDefaults : FC -> Name -> (params : List (Name, RawImp)) -> -- parameters have been specialised, use them! @@ -188,7 +188,7 @@ elabImplementation {vars} ifc vis opts_in pass env nest is cons iname ps named i let impTy = doBind paramBinds initTy let impTyDecl - = IClaim (MkFCVal vfc $ MkIClaimData top vis opts (Mk [EmptyFC, NoFC impName] impTy)) + = IClaim (MkFCVal vfc $ MkIClaimData top vis opts (Mk [EmptyFC, MkDef impName] impTy)) log "elab.implementation" 5 $ "Implementation type: " ++ show impTy @@ -475,7 +475,7 @@ elabImplementation {vars} ifc vis opts_in pass env nest is cons iname ps named i = do let opts = if isJust $ findTotality opts_in then opts_in else maybe opts_in (\t => Totality t :: opts_in) treq - IClaim $ MkFCVal vfc $ MkIClaimData c vis opts $ Mk [EmptyFC, NoFC n] mty + IClaim $ MkFCVal vfc $ MkIClaimData c vis opts $ Mk [EmptyFC, MkDef n] mty -- Given the method type (result of topMethType) return the mapping from -- top level method name to current implementation's method name diff --git a/src/Idris/Elab/Interface.idr b/src/Idris/Elab/Interface.idr index 15960fc9f62..0c68b73e701 100644 --- a/src/Idris/Elab/Interface.idr +++ b/src/Idris/Elab/Interface.idr @@ -59,14 +59,14 @@ getSig : ImpDecl -> Maybe Signature getSig (IClaim (MkWithData _ $ MkIClaimData c _ opts ty)) = Just $ MkSignature { count = c , flags = opts - , name = ty.tyName + , name = ty.tyName.drop , isData = False , type = namePis 0 ty.val } getSig (IData _ _ _ (MkImpLater fc n ty)) = Just $ MkSignature { count = erased , flags = [Invertible] - , name = NoFC n + , name = NoFC n.val , isData = True , type = namePis 0 ty } @@ -106,11 +106,11 @@ mkIfaceData {vars} ifc def_vis env constraints n conName ps dets meths conty = mkTy vfc Implicit (map jname ps) $ mkTy vfc AutoImplicit (map bhere constraints) $ mkTy vfc Explicit (map bname meths) retty - con = Mk [vfc, NoFC conName] !(bindTypeNames ifc [] (pNames ++ map fst meths ++ toList vars) conty) + con = Mk [vfc, MkDef conName] !(bindTypeNames ifc [] (pNames ++ map fst meths ++ toList vars) conty) bound = pNames ++ map fst meths ++ toList vars in pure $ IData vfc def_vis Nothing {- ?? -} - $ MkImpData vfc n + $ MkImpData vfc (MkDef n) -- Interface definiton aren't binding (Just !(bindTypeNames ifc [] bound (mkDataTy vfc ps))) opts [con] where @@ -174,7 +174,7 @@ getMethToplevel {vars} env vis iname cname allmeths bindNames params (mname, sig cn <- traverse inCurrentNS sig.name let tydecl = IClaim (MkFCVal vfc $ MkIClaimData sig.count vis (if sig.isData then [Inline, Invertible] else [Inline]) - (Mk [vfc, cn] ty_imp)) + (Mk [vfc, NotBinding :+ cn] ty_imp)) let conapp = apply (IVar vfc cname) (map (IBindVar EmptyFC) bindNames) let lhs = INamedApp vfc @@ -226,7 +226,7 @@ getConstraintHint {vars} fc env vis iname cname constraints meths params (cn, co (UN (Basic $ "__" ++ show iname ++ "_" ++ show con)) let tydecl = IClaim (MkFCVal fc $ MkIClaimData top vis [Inline, Hint False] - (Mk [EmptyFC, NoFC hintname] ty_imp)) + (Mk [EmptyFC, MkDef hintname] ty_imp)) let conapp = apply (impsBind (IVar fc cname) constraints) (map (const (Implicit fc True)) meths) @@ -291,7 +291,7 @@ elabInterface : {vars : _} -> Name -> (params : List (Name, (RigCount, RawImp))) -> (dets : Maybe (List1 Name)) -> - (conName : Maybe (WithDoc $ AddFC Name)) -> + (conName : Maybe (DocBindFC Name)) -> List ImpDecl -> Core () elabInterface {vars} ifc def_vis env nest constraints iname params dets mcon body @@ -407,7 +407,7 @@ elabInterface {vars} ifc def_vis env nest constraints iname params dets mcon bod let dtydecl = IClaim $ MkFCVal vdfc $ MkIClaimData rig (collapseDefault def_vis) [] - $ Mk [EmptyFC, NoFC dn] dty_imp + $ Mk [EmptyFC, MkDef dn] dty_imp processDecl [] nest env dtydecl diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index f72d1b768e9..3407a278d79 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -2,6 +2,7 @@ module Idris.Parser import Core.Options import Core.Metadata +import Core.WithData import Idris.Syntax import Idris.Syntax.Traversals import public Parser.Source @@ -181,50 +182,77 @@ iOperator = OpSymbols <$> operator <|> Backticked <$> (symbol "`" *> name <* symbol "`") + + data ArgType = UnnamedExpArg PTerm | UnnamedAutoArg PTerm | NamedArg Name PTerm | WithArg PTerm -argTerm : ArgType -> PTerm -argTerm (UnnamedExpArg t) = t -argTerm (UnnamedAutoArg t) = t -argTerm (NamedArg _ t) = t -argTerm (WithArg t) = t - -export -debugString : OriginDesc -> Rule PTerm -debugString fname = do - di <- bounds debugInfo - pure $ PPrimVal (boundToFC fname di) $ Str $ case di.val of - DebugLoc => - let bnds = di.bounds in - joinBy ", " - [ "File \{show fname}" - , "line \{show (startLine bnds)}" - , "characters \{show (startCol bnds)}\{ - ifThenElse (startLine bnds == endLine bnds) - ("-\{show (endCol bnds)}") - "" - }" - ] - DebugFile => "\{show fname}" - DebugLine => "\{show (startLine di.bounds)}" - DebugCol => "\{show (startCol di.bounds)}" +parameters {auto fname : OriginDesc} + export + debugString : Rule PTerm + debugString = do + di <- bounds debugInfo + pure $ PPrimVal (boundToFC fname di) $ Str $ case di.val of + DebugLoc => + let bnds = di.bounds in + joinBy ", " + [ "File \{show fname}" + , "line \{show (startLine bnds)}" + , "characters \{show (startCol bnds)}\{ + ifThenElse (startLine bnds == endLine bnds) + ("-\{show (endCol bnds)}") + "" + }" + ] + DebugFile => "\{show fname}" + DebugLine => "\{show (startLine di.bounds)}" + DebugCol => "\{show (startCol di.bounds)}" + + totalityOpt : Rule TotalReq + totalityOpt + = (decoratedKeyword fname "partial" $> PartialOK) + <|> (decoratedKeyword fname "total" $> Total) + <|> (decoratedKeyword fname "covering" $> CoveringOnly) + + operatorBindingOption : Rule BindingModifier + operatorBindingOption + = (decoratedKeyword fname "autobind" >> pure Autobind) + <|> (decoratedKeyword fname "typebind" >> pure Typebind) -totalityOpt : OriginDesc -> Rule TotalReq -totalityOpt fname - = (decoratedKeyword fname "partial" $> PartialOK) - <|> (decoratedKeyword fname "total" $> Total) - <|> (decoratedKeyword fname "covering" $> CoveringOnly) + operatorBindingKeyword : EmptyRule BindingModifier + operatorBindingKeyword + = operatorBindingOption <|> pure NotBinding -fnOpt : OriginDesc -> Rule PFnOpt -fnOpt fname - = do x <- totalityOpt fname - pure $ IFnOpt (Totality x) + fnOpt : Rule PFnOpt + fnOpt = do x <- totalityOpt + pure $ IFnOpt (Totality x) + <|> IFnOpt <$> Binding <$> operatorBindingOption mutual + ||| A binder with only one name and one type + ||| BNF: + ||| plainBinder := name ':' typeExpr + plainBinder : (fname : OriginDesc) => (indents : IndentInfo) => Rule PlainBinder + plainBinder = do name <- fcBounds (decoratedSimpleBinderUName fname) + decoratedSymbol fname ":" + ty <- typeExpr pdef fname indents + pure $ Mk [name] ty + + ||| A binder with multiple names and one type + ||| BNF: + ||| basicMultiBinder := name (, name)* ':' typeExpr + basicMultiBinder : (fname : OriginDesc) => (indents : IndentInfo) => Rule BasicMultiBinder + basicMultiBinder + = do rig <- multiplicity fname + names <- sepBy1 (decoratedSymbol fname ",") + $ fcBounds (decoratedSimpleBinderUName fname) + decoratedSymbol fname ":" + ty <- typeExpr pdef fname indents + pure $ MkBasicMultiBinder rig names ty + appExpr : ParseOpts -> OriginDesc -> IndentInfo -> Rule PTerm appExpr q fname indents = case_ fname indents @@ -233,6 +261,7 @@ mutual <|> lazy fname indents <|> if_ fname indents <|> with_ fname indents + <|> bindingApp fname indents <|> do b <- bounds (MkPair <$> simpleExpr fname indents <*> many (argExpr q fname indents)) (f, args) <- pure b.val pure (applyExpImp (start b) (end b) f (concat args)) @@ -264,12 +293,12 @@ mutual t => pure [UnnamedExpArg t] <|> do continue indents braceArgs fname indents - <|> if withOK q - then do continue indents - decoratedSymbol fname "|" - arg <- expr ({withOK := False} q) fname indents - pure [WithArg arg] - else fail "| not allowed here" + <|> do let True = withOK q + | False => fail "| not allowed here" + continue indents + decoratedSymbol fname "|" + arg <- expr ({withOK := False} q) fname indents + pure [WithArg arg] where underscore : FC -> ArgType underscore fc = NamedArg (UN Underscore) (PImplicit fc) @@ -294,7 +323,7 @@ mutual pure $ if isNil list then [underscore fc] else matchAny - pure $ matchAny ++ list + pure (matchAny ++ list) <|> do decoratedSymbol fname "@{" commit @@ -328,7 +357,7 @@ mutual -- The different kinds of operator bindings `x : ty` for typebind -- x <- e and x : ty <- e for autobind - opBinderTypes : OriginDesc -> IndentInfo -> WithBounds PTerm -> Rule (OperatorLHSInfo PTerm) + opBinderTypes : OriginDesc -> IndentInfo -> WithBounds PTerm -> Rule (BindingInfo PTerm) opBinderTypes fname indents boundName = do decoratedSymbol fname ":" ty <- typeExpr pdef fname indents @@ -342,11 +371,21 @@ mutual ty <- typeExpr pdef fname indents pure (BindType boundName.val ty) - opBinder : OriginDesc -> IndentInfo -> Rule (OperatorLHSInfo PTerm) + opBinder : OriginDesc -> IndentInfo -> Rule (BindingInfo PTerm) opBinder fname indents = do boundName <- bounds (expr plhs fname indents) opBinderTypes fname indents boundName + ||| parse binding application + ||| bindingApp := simpleExpr binderInfo "|" expr + bindingApp : OriginDesc -> IndentInfo -> Rule PTerm + bindingApp fname indents + = do fn <- fcBounds (decoratedSimpleBinderUName fname) + bind <- fcBounds (parens fname (opBinder fname indents)) + decoratedSymbol fname "|" + scope <- fcBounds (typeExpr pdef fname indents) + pure $ PBindingApp fn bind scope + autobindOp : ParseOpts -> OriginDesc -> IndentInfo -> Rule PTerm autobindOp q fname indents = do b <- fcBounds $ do @@ -356,7 +395,7 @@ mutual commit e <- expr q fname indents pure (binder, op, e) - pure (POp b.fc (fst b.val) (fst (snd b.val)) (snd (snd b.val))) + pure (POp b.fc (map LHSBinder $ fst b.val) (fst (snd b.val)) (snd (snd b.val))) opExprBase : ParseOpts -> OriginDesc -> IndentInfo -> Rule PTerm opExprBase q fname indents @@ -579,7 +618,7 @@ mutual pure $ case projs of [] => root _ => PPostfixApp (boundToFC fname b) root projs - <|> debugString fname + <|> debugString {fname} <|> do b <- bounds (forget <$> some (bounds postfixProj)) pure $ let projs = map (\ proj => (boundToFC fname proj, proj.val)) b.val in PPostfixAppPartial (boundToFC fname b) projs @@ -1165,7 +1204,6 @@ mutual Use "%export" instead """ - visOption : OriginDesc -> Rule Visibility visOption fname = (decoratedKeyword fname "public" *> decoratedKeyword fname "export" $> Public) @@ -1178,36 +1216,14 @@ visOption fname <|> (decoratedKeyword fname "private" $> Private) +parseDefault : Rule a -> EmptyRule (WithDefault a e) +parseDefault p = (specified <$> p) <|> pure defaulted + visibility : OriginDesc -> EmptyRule (WithDefault Visibility Private) -visibility fname - = (specified <$> visOption fname) - <|> pure defaulted +visibility fname = parseDefault (visOption fname) exportVisibility : OriginDesc -> EmptyRule (WithDefault Visibility Export) -exportVisibility fname - = (specified <$> visOption fname) - <|> pure defaulted - -||| A binder with only one name and one type -||| BNF: -||| plainBinder := name ':' typeExpr -plainBinder : (fname : OriginDesc) => (indents : IndentInfo) => Rule PlainBinder -plainBinder = do name <- fcBounds (decoratedSimpleBinderUName fname) - decoratedSymbol fname ":" - ty <- typeExpr pdef fname indents - pure $ Mk [name] ty - -||| A binder with multiple names and one type -||| BNF: -||| basicMultiBinder := name (, name)* ':' typeExpr -basicMultiBinder : (fname : OriginDesc) => (indents : IndentInfo) => Rule BasicMultiBinder -basicMultiBinder - = do rig <- multiplicity fname - names <- sepBy1 (decoratedSymbol fname ",") - $ fcBounds (decoratedSimpleBinderUName fname) - decoratedSymbol fname ":" - ty <- typeExpr pdef fname indents - pure $ MkBasicMultiBinder rig names ty +exportVisibility fname = parseDefault (visOption fname) tyDecls : Rule Name -> String -> OriginDesc -> IndentInfo -> Rule PTypeDecl tyDecls declName predoc fname indents @@ -1343,20 +1359,20 @@ simpleCon fname ret indents pure b.withFC simpleData : OriginDesc -> WithBounds t -> - WithBounds Name -> IndentInfo -> Rule PDataDecl + FCBind Name -> IndentInfo -> Rule PDataDecl simpleData fname start tyName indents = do b <- bounds (do params <- many (bounds $ decorate fname Bound name) tyend <- bounds (decoratedSymbol fname "=") mustWork $ do let tyfc = boundToFC fname (mergeBounds start tyend) - let tyCon = PRef (boundToFC fname tyName) tyName.val + let tyCon = PRef tyName.fc tyName.val let toPRef = \ t => PRef (boundToFC fname t) t.val let conRetTy = papply tyfc tyCon (map toPRef params) cons <- sepBy1 (decoratedSymbol fname "|") (simpleCon fname conRetTy indents) pure (params, tyfc, forget cons)) (params, tyfc, cons) <- pure b.val - pure (MkPData (boundToFC fname (mergeBounds start b)) tyName.val - (Just (mkTyConType fname tyfc params)) [] cons) + pure (MkPData (boundToFC fname (mergeBounds start b)) tyName + (Just (mkTyConType fname tyfc params)) [] (map (NotBinding :+) cons)) dataOpt : OriginDesc -> Rule DataOpt dataOpt fname @@ -1376,7 +1392,7 @@ dataOpts fname = option [] $ do decoratedSymbol fname "]" pure (forget opts) -dataBody : OriginDesc -> Int -> WithBounds t -> Name -> IndentInfo -> Maybe PTerm -> +dataBody : OriginDesc -> Int -> WithBounds t -> FCBind Name -> IndentInfo -> Maybe PTerm -> EmptyRule PDataDecl dataBody fname mincol start n indents ty = do ty <- maybe (fail "Telescope is not optional in forward declaration") pure ty @@ -1384,34 +1400,38 @@ dataBody fname mincol start n indents ty pure (MkPLater (boundToFC fname start) n ty) <|> do b <- bounds (do (mustWork $ decoratedKeyword fname "where") opts <- dataOpts fname + bind <- operatorBindingKeyword cs <- blockAfter mincol (tyDecls (mustWork $ decoratedDataConstructorName fname) "" fname) - pure (opts, cs)) - (opts, cs) <- pure b.val + pure (opts, map (bind :+) cs)) + (opts, cs) <- pure (the (Pair ? ?) b.val) pure (MkPData (boundToFC fname (mergeBounds start b)) n ty opts cs) gadtData : OriginDesc -> Int -> WithBounds t -> - WithBounds Name -> IndentInfo -> EmptyRule PDataDecl + FCBind Name -> IndentInfo -> EmptyRule PDataDecl gadtData fname mincol start tyName indents = do ty <- optional $ do decoratedSymbol fname ":" commit typeExpr pdef fname indents - dataBody fname mincol start tyName.val indents ty + dataBody fname mincol start tyName indents ty dataDeclBody : OriginDesc -> IndentInfo -> Rule PDataDecl dataDeclBody fname indents - = do b <- bounds (do col <- column - decoratedKeyword fname "data" - n <- mustWork (bounds $ decoratedDataTypeName fname) - pure (col, n)) + = do b <- bounds $ do + col <- column + bind <- operatorBindingKeyword {fname} + decoratedKeyword fname "data" + n <- mustWork (fcBounds $ decoratedDataTypeName fname) + pure (col, bind :+ n) + let _ = the (WithBounds (Int, FCBind Name)) b (col, n) <- pure b.val simpleData fname b n indents <|> gadtData fname col b n indents -- a data declaration can have a visibility and an optional totality (#1404) dataVisOpt : OriginDesc -> EmptyRule (WithDefault Visibility Private, Maybe TotalReq) dataVisOpt fname - = do { vis <- visOption fname ; mbtot <- optional (totalityOpt fname) ; pure (specified vis, mbtot) } - <|> do { tot <- totalityOpt fname ; vis <- visibility fname ; pure (vis, Just tot) } + = do { vis <- visOption fname ; mbtot <- optional totalityOpt ; pure (specified vis, mbtot) } + <|> do { tot <- totalityOpt ; vis <- visibility fname ; pure (vis, Just tot) } <|> pure (defaulted, Nothing) dataDecl : (fname : OriginDesc) => (indents : IndentInfo) => Rule PDeclNoFC @@ -1561,7 +1581,7 @@ directive atEnd indents pure (Extension e) <|> do decoratedPragma fname "default" - tot <- totalityOpt fname + tot <- totalityOpt atEnd indents pure (DefaultTotality tot) @@ -1650,7 +1670,7 @@ visOpt : OriginDesc -> Rule (Either Visibility PFnOpt) visOpt fname = do vis <- visOption fname pure (Left vis) - <|> do tot <- fnOpt fname + <|> do tot <- fnOpt pure (Right tot) <|> do opt <- fnDirectOpt fname pure (Right opt) @@ -1664,12 +1684,13 @@ getVisibility (Just vis) (Left x :: xs) = fatalError "Multiple visibility modifiers" getVisibility v (_ :: xs) = getVisibility v xs -recordConstructor : OriginDesc -> Rule (WithDoc $ AddFC Name) +recordConstructor : OriginDesc -> Rule (DocBindFC Name) recordConstructor fname = do doc <- optDocumentation fname + binding <- operatorBindingKeyword {fname} decorate fname Keyword $ exactIdent "constructor" n <- fcBounds $ mustWork $ decoratedDataConstructorName fname - pure (doc :+ n) + pure (doc :+ binding :+ n) autoImplicitField : OriginDesc -> IndentInfo -> Rule (PiInfo t) autoImplicitField fname _ = AutoImplicit <$ decoratedKeyword fname "auto" @@ -1713,7 +1734,8 @@ implBinds fname indents namedImpl = concatMap (map adjust) <$> go where piInfo <- bounds $ option Implicit $ defImplicitField fname indents when (not namedImpl && isDefaultImplicit piInfo.val) $ fatalLoc piInfo.bounds "Default implicits are allowed only for named implementations" - ns <- map (\case (MkBasicMultiBinder rig names type) => map (\nm => Mk [rig, nm] (MkPiBindData piInfo.val type)) (forget names)) + ns <- map (\case (MkBasicMultiBinder rig names type) => + map (\nm => Mk [rig, "" :+ NotBinding :+ nm] (MkPiBindData piInfo.val type)) (forget names)) (pibindListName fname indents) let ns = the (List (ImpParameter' PTerm)) ns commitSymbol fname "}" @@ -1805,10 +1827,11 @@ parameters {auto fname : OriginDesc} {auto indents : IndentInfo} visOpts <- many (visOpt fname) vis <- getVisibility Nothing visOpts let opts = mapMaybe getRight visOpts + bind <- operatorBindingKeyword rig <- multiplicity fname cls <- tyDecls (decorate fname Function name) doc fname indents - pure $ MkPClaim rig vis opts cls + pure $ MkPClaim rig vis opts (bind :+ cls) -- A Single binder with multiple names @@ -1839,12 +1862,12 @@ parameters {auto fname : OriginDesc} {auto indents : IndentInfo} recordBody : String -> WithDefault Visibility Private -> Maybe TotalReq -> Int -> - Name -> + FCBind Name -> List PBinder -> EmptyRule PDeclNoFC recordBody doc vis mbtot col n params = do atEndIndent indents - pure (PRecord doc vis mbtot (MkPRecordLater n params)) + pure (PRecord doc vis mbtot (MkPRecordLater n params)) -- TODO: MkPRecordLater takes WithFC Name <|> do mustWork $ decoratedKeyword fname "where" opts <- dataOpts fname dcflds <- blockWithOptHeaderAfter col @@ -1857,11 +1880,12 @@ parameters {auto fname : OriginDesc} {auto indents : IndentInfo} recordDecl = do doc <- optDocumentation fname (vis,mbtot) <- dataVisOpt fname + binding <- operatorBindingKeyword {fname} col <- column decoratedKeyword fname "record" - n <- mustWork (decoratedDataTypeName fname) + n <- fcBounds $ mustWork (decoratedDataTypeName fname) paramss <- many (continue indents >> recordParam) - recordBody doc vis mbtot col n paramss + recordBody doc vis mbtot col (binding :+ n) paramss ||| Parameter blocks ||| BNF: @@ -1892,11 +1916,6 @@ parameters {auto fname : OriginDesc} {auto indents : IndentInfo} = do nd <- clause 0 Nothing fname indents pure (PDef (singleton nd)) - operatorBindingKeyword : EmptyRule BindingModifier - operatorBindingKeyword - = (decoratedKeyword fname "autobind" >> pure Autobind) - <|> (decoratedKeyword fname "typebind" >> pure Typebind) - <|> pure NotBinding fixDecl : Rule PDecl fixDecl diff --git a/src/Idris/Pretty.idr b/src/Idris/Pretty.idr index 293ad9b9ce8..1abbab86b7b 100644 --- a/src/Idris/Pretty.idr +++ b/src/Idris/Pretty.idr @@ -337,6 +337,7 @@ mutual prettyPrec d (PForce _ tm) = parenthesise (d > startPrec) $ "Force" <++> prettyPrec appPrec tm prettyPrec d (PAutoApp _ f a) = parenthesise (d > startPrec) $ group $ prettyPrec leftAppPrec f <++> "@" <+> braces (pretty a) + prettyPrec d (PBindingApp fn bind scope) = ?TODO2 prettyPrec d (PNamedApp _ f n (PRef _ a)) = parenthesise (d > startPrec) $ group $ if n == rawName a @@ -360,15 +361,15 @@ mutual prettyPrec d (PDotted _ p) = dot <+> prettyPrec d p prettyPrec d (PImplicit _) = "_" prettyPrec d (PInfer _) = annotate Hole $ "?" - prettyPrec d (POp _ (MkWithData _ $ BindType nm left) op right) = + prettyPrec d (POp _ (MkWithData _ $ LHSBinder $ BindType nm left) op right) = group $ parens (prettyPrec d nm <++> ":" <++> pretty left) <++> prettyOp op.val.toName <++> pretty right - prettyPrec d (POp _ (MkWithData _ $ BindExpr nm left) op right) = + prettyPrec d (POp _ (MkWithData _ $ LHSBinder $ BindExpr nm left) op right) = group $ parens (prettyPrec d nm <++> "<-" <++> pretty left) <++> prettyOp op.val.toName <++> pretty right - prettyPrec d (POp _ (MkWithData _ $ BindExplicitType nm ty left) op right) = + prettyPrec d (POp _ (MkWithData _ $ LHSBinder $ BindExplicitType nm ty left) op right) = group $ parens (prettyPrec d nm <++> ":" <++> pretty ty <++> "<-" <++> pretty left) <++> prettyOp op.val.toName <++> pretty right diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr index 4a929787d91..4616d15395e 100644 --- a/src/Idris/REPL.idr +++ b/src/Idris/REPL.idr @@ -408,7 +408,7 @@ getItDecls let it = UN $ Basic "it" in pure [ IClaim (MkFCVal replFC $ MkIClaimData top Private [] - $ Mk [replFC, NoFC it] (Implicit replFC False)) + $ Mk [replFC, MkDef it] (Implicit replFC False)) , IDef replFC it [PatClause replFC (IVar replFC it) (IVar replFC n)]] ||| Produce the elaboration of a PTerm, along with its inferred type diff --git a/src/Idris/Resugar.idr b/src/Idris/Resugar.idr index 2918a5eda95..8d18d808b88 100644 --- a/src/Idris/Resugar.idr +++ b/src/Idris/Resugar.idr @@ -20,6 +20,7 @@ import Data.Maybe import Data.String import Libraries.Data.StringMap import Libraries.Data.ANameMap +import Libraries.Data.WithData %default covering @@ -359,6 +360,10 @@ mutual = do arg' <- toPTerm startPrec arg fn' <- toPTerm startPrec fn bracket p appPrec (PWithApp fc fn' arg') + toPTerm p (IBindingApp fn bind arg) + = pure $ PBindingApp fn + !(traverse (traverse (toPTerm p)) bind) + !(traverse (toPTerm p) arg) toPTerm p (INamedApp fc fn n arg) = do arg' <- toPTerm startPrec arg app <- toPTermApp fn [(fc, Just (Just n), arg')] @@ -472,9 +477,9 @@ mutual toPTypeDecl : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> - ImpTy' KindedName -> Core (PTypeDecl' KindedName) + ImpTy' KindedName -> Core (AddMetadata Bind' (PTypeDecl' KindedName)) toPTypeDecl impTy - = pure (MkFCVal impTy.fc $ MkPTy (pure ("", impTy.tyName)) "" !(toPTerm startPrec impTy.val)) + = pure $ Mk [impTy.tyName.bind, impTy.fc] (MkPTy (pure ("", drop $ impTy.tyName)) "" !(toPTerm startPrec impTy.val)) toPData : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> @@ -490,7 +495,7 @@ mutual IField' KindedName -> Core (PField' KindedName) toPField field = do bind' <- traverse (toPTerm startPrec) field.val - pure (Mk [field.fc , "", field.rig, [field.name]] bind') + pure (Mk [field.fc , "", field.rig, [field.name.drop.drop]] bind') toPFnOpt : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> @@ -505,7 +510,8 @@ mutual ImpDecl' KindedName -> Core (Maybe (PDecl' KindedName)) toPDecl (IClaim (MkWithData fc $ MkIClaimData rig vis opts ty)) = do opts' <- traverse toPFnOpt opts - pure (Just (MkWithData fc $ PClaim (MkPClaim rig vis opts' !(toPTypeDecl ty)))) + newTy <- toPTypeDecl ty + pure (Just (MkWithData fc $ PClaim (MkPClaim rig vis opts' newTy))) toPDecl (IData fc vis mbtot d) = pure (Just (MkFCVal fc $ PData "" vis mbtot !(toPData d))) toPDecl (IDef fc n cs) @@ -516,17 +522,17 @@ mutual traverseList1 (\binder => do info' <- traverse (toPTerm startPrec) binder.val.info type' <- toPTerm startPrec binder.val.boundType - pure (MkFullBinder info' binder.rig binder.name type')) ps + pure (MkFullBinder info' binder.rig binder.name.drop.drop type')) ps pure (Just (MkFCVal fc (PParameters (Right args) (catMaybes ds')))) toPDecl (IRecord fc _ vis mbtot (MkWithData _ $ MkImpRecord header body)) = do ps' <- traverse (traverse (traverse (toPTerm startPrec))) header.val fs' <- traverse toPField body.val pure (Just (MkFCVal fc $ PRecord "" vis mbtot - (MkPRecord header.name.val (map toBinder ps') body.opts (Just (AddDef body.name)) fs'))) + (MkPRecord header.tyName (map toBinder ps') body.opts (Just (AddDef body.tyName)) fs'))) where toBinder : ImpParameter' (PTerm' KindedName) -> PBinder' KindedName toBinder binder - = MkFullBinder binder.val.info binder.rig binder.name binder.val.boundType + = MkFullBinder binder.val.info binder.rig binder.name.drop.drop binder.val.boundType toPDecl (IFail fc msg ds) = do ds' <- traverse toPDecl ds diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr index 3a5c3f1f26b..9a48d7a3a14 100644 --- a/src/Idris/Syntax.idr +++ b/src/Idris/Syntax.idr @@ -7,6 +7,7 @@ import public Core.FC import public Core.Normalise import public Core.Options import public Core.TT +import public Core.WithData import TTImp.TTImp @@ -23,6 +24,7 @@ import Libraries.Data.NameMap import Libraries.Data.String.Extra import Libraries.Data.StringMap import Libraries.Data.WithDefault +import public Libraries.Data.WithData import Libraries.Text.PrettyPrint.Prettyprinter import Parser.Lexer.Source @@ -96,9 +98,11 @@ mutual -- Direct (more or less) translations to RawImp PRef : FC -> nm -> PTerm' nm + -- Pi-types with an arbitrary complex binder NewPi : WithFC (PBinderScope' nm) -> PTerm' nm Forall : WithFC (List1 (WithFC Name), PTerm' nm) -> PTerm' nm + -- Simple pi-types, translates directly into IPi, this should be replaced in favor of `NewPi` PPi : FC -> RigCount -> PiInfo (PTerm' nm) -> Maybe Name -> (argTy : PTerm' nm) -> (retTy : PTerm' nm) -> PTerm' nm PLam : FC -> RigCount -> PiInfo (PTerm' nm) -> (pat : PTerm' nm) -> @@ -112,6 +116,7 @@ mutual PApp : FC -> PTerm' nm -> PTerm' nm -> PTerm' nm PWithApp : FC -> PTerm' nm -> PTerm' nm -> PTerm' nm PNamedApp : FC -> PTerm' nm -> Name -> PTerm' nm -> PTerm' nm + PBindingApp : (function : WithFC Name) -> (binder : WithFC (BindingInfo (PTerm' nm))) -> (scope : WithFC (PTerm' nm)) -> PTerm' nm PAutoApp : FC -> PTerm' nm -> PTerm' nm -> PTerm' nm PDelayed : FC -> LazyReason -> PTerm' nm -> PTerm' nm @@ -188,6 +193,7 @@ mutual getPTermLoc (PWithApp fc _ _) = fc getPTermLoc (PAutoApp fc _ _) = fc getPTermLoc (PNamedApp fc _ _ _) = fc + getPTermLoc (PBindingApp s _ w) = fromMaybe EmptyFC (mergeFC s.fc w.fc) getPTermLoc (PDelayed fc _ _) = fc getPTermLoc (PDelay fc _) = fc getPTermLoc (PForce fc _) = fc @@ -376,23 +382,23 @@ mutual public export data PDataDecl' : Type -> Type where - MkPData : FC -> (tyname : Name) -> + MkPData : FC -> (tyname : FCBind Name) -> -- if we have already declared the type earlier using `MkPLater`, -- we are allowed to leave the telescope out here (tycon : Maybe (PTerm' nm)) -> (opts : List DataOpt) -> - (datacons : List (PTypeDecl' nm)) -> PDataDecl' nm - MkPLater : FC -> (tyname : Name) -> (tycon : PTerm' nm) -> PDataDecl' nm + (datacons : List (AddMetadata Bind' (PTypeDecl' nm))) -> PDataDecl' nm + MkPLater : FC -> (tyname : FCBind Name) -> (tycon : PTerm' nm) -> PDataDecl' nm public export data PRecordDecl' : Type -> Type where - MkPRecord : (tyname : Name) -> + MkPRecord : (tyname : FCBind Name) -> (params : List (PBinder' nm)) -> (opts : List DataOpt) -> - (conName : Maybe (WithDoc $ AddFC Name)) -> + (conName : Maybe (DocBindFC Name)) -> (decls : List (PField' nm)) -> PRecordDecl' nm - MkPRecordLater : (tyname : Name) -> + MkPRecordLater : (tyname : FCBind Name) -> (params : List (PBinder' nm)) -> PRecordDecl' nm @@ -523,7 +529,7 @@ mutual qty : RigCount vis : Visibility opts : List (PFnOpt' nm) - type : PTypeDecl' nm + type : AddMetadata Bind' (PTypeDecl' nm) public export record PFixityData where @@ -551,11 +557,11 @@ mutual List (PDecl' nm) -> PDeclNoFC' nm PInterface : WithDefault Visibility Private -> (constraints : List (Maybe Name, PTerm' nm)) -> - Name -> - (doc : String) -> + (typeName : Name) -> -- Those two should be merged into + (doc : String) -> -- WithData [Doc', FC'] Name (params : List (BasicMultiBinder' nm)) -> (det : Maybe (List1 Name)) -> - (conName : Maybe (WithDoc $ AddFC Name)) -> + (conName : Maybe (DocBindFC Name)) -> List (PDecl' nm) -> PDeclNoFC' nm PImplementation : Visibility -> List PFnOpt -> Pass -> @@ -616,13 +622,13 @@ isPDef _ = Nothing definedInData : PDataDecl -> List Name -definedInData (MkPData _ n _ _ cons) = n :: concatMap (.nameList) cons -definedInData (MkPLater _ n _) = [n] +definedInData (MkPData _ n _ _ cons) = n.val :: concatMap ((.nameList) . drop) cons +definedInData (MkPLater _ n _) = [n.val] export definedIn : List PDeclNoFC -> List Name definedIn [] = [] -definedIn (PClaim claim :: ds) = claim.type.nameList ++ definedIn ds +definedIn (PClaim claim :: ds) = claim.type.drop.nameList ++ definedIn ds definedIn (PData _ _ _ d :: ds) = definedInData d ++ definedIn ds definedIn (PParameters _ pds :: ds) = definedIn (map val pds) ++ definedIn ds definedIn (PUsing _ pds :: ds) = definedIn (map val pds) ++ definedIn ds @@ -913,6 +919,8 @@ parameters {0 nm : Type} (toName : nm -> Name) else showPTermPrec d f ++ " {" ++ showPrec d n ++ " = " ++ showPrec d (toName a) ++ "}" showPTermPrec d (PNamedApp _ f n a) = showPTermPrec d f ++ " {" ++ showPrec d n ++ " = " ++ showPTermPrec d a ++ "}" + showPTermPrec d (PBindingApp fn bind scope) + = ?TODO1 showPTermPrec _ (PSearch {}) = "%search" showPTermPrec d (PQuote _ tm) = "`(" ++ showPTermPrec d tm ++ ")" showPTermPrec d (PQuoteName _ n) = "`{" ++ showPrec d n ++ "}" @@ -928,11 +936,11 @@ parameters {0 nm : Type} (toName : nm -> Name) showPTermPrec _ (PInfer _) = "?" showPTermPrec d (POp _ (MkWithData _ $ NoBinder left) op right) = showPTermPrec d left ++ " " ++ showOpPrec d op.val ++ " " ++ showPTermPrec d right - showPTermPrec d (POp _ (MkWithData _ $ BindType nm left) op right) + showPTermPrec d (POp _ (MkWithData _ $ LHSBinder $ BindType nm left) op right) = "(" ++ showPTermPrec d nm ++ " : " ++ showPTermPrec d left ++ " " ++ showOpPrec d op.val ++ " " ++ showPTermPrec d right ++ ")" - showPTermPrec d (POp _ (MkWithData _ $ BindExpr nm left) op right) + showPTermPrec d (POp _ (MkWithData _ $ LHSBinder $ BindExpr nm left) op right) = "(" ++ showPTermPrec d nm ++ " := " ++ showPTermPrec d left ++ " " ++ showOpPrec d op.val ++ " " ++ showPTermPrec d right ++ ")" - showPTermPrec d (POp _ (MkWithData _ $ BindExplicitType nm ty left) op right) + showPTermPrec d (POp _ (MkWithData _ $ LHSBinder $ BindExplicitType nm ty left) op right) = "(" ++ showPTermPrec d nm ++ " : " ++ showPTermPrec d ty ++ ":=" ++ showPTermPrec d left ++ " " ++ showOpPrec d op.val ++ " " ++ showPTermPrec d right ++ ")" showPTermPrec d (PPrefixOp _ op x) = showOpPrec d op.val ++ showPTermPrec d x showPTermPrec d (PSectionL _ op x) = "(" ++ showOpPrec d op.val ++ " " ++ showPTermPrec d x ++ ")" @@ -1191,7 +1199,7 @@ Show PClause where export covering Show PClaimData where - show (MkPClaim rig _ _ sig) = showCount rig ++ show sig + show (MkPClaim rig _ _ sig) = showCount rig ++ show sig.drop -- TODO: finish writing this instance export diff --git a/src/Idris/Syntax/TTC.idr b/src/Idris/Syntax/TTC.idr index dcd7a0a748f..8802e7288e7 100644 --- a/src/Idris/Syntax/TTC.idr +++ b/src/Idris/Syntax/TTC.idr @@ -66,18 +66,6 @@ TTC Import where nameAs <- fromBuf pure (MkImport loc reexport path nameAs) -export -TTC BindingModifier where - toBuf NotBinding = tag 0 - toBuf Typebind = tag 1 - toBuf Autobind = tag 2 - fromBuf - = case !getTag of - 0 => pure NotBinding - 1 => pure Typebind - 2 => pure Autobind - _ => corrupt "binding" - export TTC FixityInfo where toBuf fx diff --git a/src/Idris/Syntax/Traversals.idr b/src/Idris/Syntax/Traversals.idr index 9452593426d..59c5cbe6c82 100644 --- a/src/Idris/Syntax/Traversals.idr +++ b/src/Idris/Syntax/Traversals.idr @@ -64,6 +64,10 @@ mapPTermM f = goPTerm where PAutoApp fc <$> goPTerm x <*> goPTerm y >>= f + goPTerm (PBindingApp fn bind scope) = + PBindingApp fn <$> traverse goBinderInfo bind + <*> traverse goPTerm scope + >>= f goPTerm (PNamedApp fc x n y) = PNamedApp fc <$> goPTerm x <*> pure n @@ -192,12 +196,16 @@ mapPTermM f = goPTerm where PWithUnambigNames fc ns <$> goPTerm rhs >>= f + export + goBinderInfo : BindingInfo (PTerm' nm) -> Core (BindingInfo (PTerm' nm)) + goBinderInfo (BindType name ty) = BindType <$> goPTerm name <*> goPTerm ty + goBinderInfo (BindExpr name expr) = BindExpr <$> goPTerm name <*> goPTerm expr + goBinderInfo (BindExplicitType name type expr) + = BindExplicitType <$> goPTerm name <*> goPTerm type <*> goPTerm expr + goOpBinder : OperatorLHSInfo (PTerm' nm) -> Core (OperatorLHSInfo (PTerm' nm)) goOpBinder (NoBinder lhs) = NoBinder <$> goPTerm lhs - goOpBinder (BindType name ty) = BindType <$> goPTerm name <*> goPTerm ty - goOpBinder (BindExpr name expr) = BindExpr <$> goPTerm name <*> goPTerm expr - goOpBinder (BindExplicitType name type expr) - = BindExplicitType <$> goPTerm name <*> goPTerm type <*> goPTerm expr + goOpBinder (LHSBinder lhs) = LHSBinder <$> goBinderInfo lhs goPFieldUpdate : PFieldUpdate' nm -> Core (PFieldUpdate' nm) goPFieldUpdate (PSetField p t) = PSetField p <$> goPTerm t @@ -314,7 +322,7 @@ mapPTermM f = goPTerm where goPDataDecl (MkPData fc n t opts tdecls) = MkPData fc n <$> goMPTerm t <*> pure opts - <*> goPTypeDecls tdecls + <*> traverse (traverse goPTypeDecl) tdecls goPDataDecl (MkPLater fc n t) = MkPLater fc n <$> goPTerm t goPiInfo : PiInfo (PTerm' nm) -> Core (PiInfo (PTerm' nm)) @@ -432,6 +440,8 @@ mapPTerm f = goPTerm where = f $ PWithApp fc (goPTerm x) (goPTerm y) goPTerm (PAutoApp fc x y) = f $ PAutoApp fc (goPTerm x) (goPTerm y) + goPTerm (PBindingApp x bind y) + = f $ PBindingApp x (map (map goPTerm) bind) (map goPTerm y) goPTerm (PNamedApp fc x n y) = f $ PNamedApp fc (goPTerm x) n (goPTerm y) goPTerm (PDelayed fc x y) @@ -631,6 +641,7 @@ substFC fc = mapPTerm $ \case PUpdate _ xs => PUpdate fc xs PApp _ x y => PApp fc x y PWithApp _ x y => PWithApp fc x y + PBindingApp x n y => PBindingApp x n y PNamedApp _ x n y => PNamedApp fc x n y PAutoApp _ x y => PAutoApp fc x y PDelayed _ x y => PDelayed fc x y diff --git a/src/Libraries/Data/WithData.idr b/src/Libraries/Data/WithData.idr index dafd5849ee4..d6da6ad30a3 100644 --- a/src/Libraries/Data/WithData.idr +++ b/src/Libraries/Data/WithData.idr @@ -196,10 +196,9 @@ export (.drop) : WithData (l :: ls) a -> WithData ls a (.drop) = {metadata $= Record.tail } -||| WithData is functiorial in its payload export -Functor (WithData md) where - map f x = MkWithData x.metadata (f x.val) +map : (a -> b) -> WithData md a -> WithData md b +map f = {val $= f} ------------------------------------------------------------------------------------------------ -- Default fields for records diff --git a/src/TTImp/BindImplicits.idr b/src/TTImp/BindImplicits.idr index ebaa748644f..36151703937 100644 --- a/src/TTImp/BindImplicits.idr +++ b/src/TTImp/BindImplicits.idr @@ -170,7 +170,7 @@ addUsing uimpls tm export bindTypeNames : {auto c : Ref Ctxt Defs} -> FC -> List (Maybe Name, RawImp) -> - List Name -> RawImp-> Core RawImp + List Name -> RawImp -> Core RawImp bindTypeNames fc uimpls env tm = if !isUnboundImplicits then do ns <- findUniqueBindableNames fc True env [] tm diff --git a/src/TTImp/Elab/BindingApp.idr b/src/TTImp/Elab/BindingApp.idr new file mode 100644 index 00000000000..ea4523fc4dc --- /dev/null +++ b/src/TTImp/Elab/BindingApp.idr @@ -0,0 +1,74 @@ +module TTImp.Elab.BindingApp + +import Core.Core +import Core.Context +import Core.Env +import Core.FC +import Core.Unify +import Core.Metadata +import Core.Name +import Core.Normalise + +import TTImp.Elab.Check +import TTImp.Elab.App +import TTImp.TTImp + +import Idris.REPL.Opts +import Idris.Syntax + +keepBinding : BindingModifier -> List GlobalDef -> List GlobalDef +keepBinding mode = filter (\x => x.bindingMode == mode) + +parameters (originalName : WithFC Name) {auto c : Ref Ctxt Defs} + checkUnique : List GlobalDef -> Core GlobalDef + checkUnique [ def ] = pure def + checkUnique [] = throw $ UndefinedName originalName.fc originalName.val + checkUnique defs = throw $ AmbiguousName originalName.fc (map fullname defs) + + typecheckCandidates : List GlobalDef -> Core (List GlobalDef) + typecheckCandidates xs = pure xs -- todo + + checkBinding : (mode : BindingModifier) -> (candidates : List GlobalDef) -> Core GlobalDef + checkBinding mode candidates = do + log "elab.bindApp" 10 $ "Potential candidates for binding identifer : \{show (map fullname candidates)}" + log "elab.bindApp" 10 $ "Checking if candidates have binding \{show mode}" + let bindingCandidates = keepBinding mode candidates + log "elab.bindApp" 10 $ "Final list of binding identifers : \{show (map fullname bindingCandidates)}" + wellTypedCandidates <- typecheckCandidates bindingCandidates + checkUnique bindingCandidates + +typeForBinder : BindingInfo RawImp -> FC -> RawImp +typeForBinder (BindType name type) = const type +typeForBinder (BindExpr name expr) = flip Implicit False +typeForBinder (BindExplicitType name type expr) = const type + + +buildLam : BindingInfo RawImp -> Maybe Name +buildLam (BindType (IVar _ name) type) = Just name +buildLam (BindExpr (IVar _ name) expr) = Just name +buildLam (BindExplicitType (IVar _ name) type expr) = Just name +buildLam _ = Nothing + +export +checkBindingApplication : {vars : _} -> + {auto c : Ref Ctxt Defs} -> + {auto m : Ref MD Metadata} -> + {auto u : Ref UST UState} -> + {auto e : Ref EST (EState vars)} -> + {auto s : Ref Syn SyntaxInfo} -> + {auto o : Ref ROpts REPLOpts} -> + RigCount -> ElabInfo -> + NestedNames vars -> Env Term vars -> + WithFC Name -> WithFC (BindingInfo RawImp) -> WithFC RawImp -> + Maybe (Glued vars) -> + Core (Term vars, Glued vars) +checkBindingApplication rig info nest env nm bind scope exp = do + ctx <- get Ctxt + log "elab.bindApp" 10 $ "checking if \{show nm.val} is binding" + defs <- lookupCtxtName nm.val (gamma ctx) + firstArg <- checkBinding nm bind.val.getBindingMode (map (snd . snd) defs) + let lam = ILam scope.fc top Explicit (buildLam bind.val) (typeForBinder bind.val bind.fc) scope.val + let fc = fromMaybe EmptyFC (mergeFC nm.fc scope.fc) + log "elab.bindApp" 10 $ "generating function \{show lam}" + checkApp rig info nest env fc (IVar nm.fc nm.val) [ bind.val.getBoundExpr, lam ] [] [] exp + diff --git a/src/TTImp/Elab/Local.idr b/src/TTImp/Elab/Local.idr index d38fdb8766c..c17b60da462 100644 --- a/src/TTImp/Elab/Local.idr +++ b/src/TTImp/Elab/Local.idr @@ -95,19 +95,12 @@ localHelper {vars} nest env nestdecls_in func \fc, nt => applyToFull fc (Ref fc nt (Resolved n')) env)) - -- Update the names in the declarations to the new 'nested' names. - -- When we encounter the names in elaboration, we'll update to an - -- application of the nested name. - updateTyName : NestedNames vars -> ImpTy -> ImpTy - updateTyName nest ty - = update "tyname" (map (mapNestedName nest)) ty - updateDataName : NestedNames vars -> ImpData -> ImpData updateDataName nest (MkImpData loc' n tycons dopts dcons) - = MkImpData loc' (mapNestedName nest n) tycons dopts - (map (updateTyName nest) dcons) + = MkImpData loc' (map (mapNestedName nest) n) tycons dopts + (map (update "tyname" (WithData.map (mapNestedName nest))) dcons) updateDataName nest (MkImpLater loc' n tycons) - = MkImpLater loc' (mapNestedName nest n) tycons + = MkImpLater loc' (map (mapNestedName nest) n) tycons updateFieldName : NestedNames vars -> IField -> IField updateFieldName nest field @@ -115,8 +108,8 @@ localHelper {vars} nest env nestdecls_in func updateRecordName : NestedNames vars -> ImpRecordData Name -> ImpRecordData Name updateRecordName nest (MkImpRecord header body) - = let updatedTyName = (update "name" (map (mapNestedName nest)) header) - updatedConName = (update "name" (map (mapNestedName nest)) body) + = let updatedTyName = (update "tyname" (map (mapNestedName nest)) header) + updatedConName = (update "tyname" (map (mapNestedName nest)) body) updatedParameters = (map (map (updateFieldName nest)) updatedConName) in MkImpRecord updatedTyName updatedParameters @@ -126,7 +119,7 @@ localHelper {vars} nest env nestdecls_in func updateName : NestedNames vars -> ImpDecl -> ImpDecl updateName nest (IClaim claim) - = IClaim $ map {type $= updateTyName nest} claim + = IClaim $ map {type $= update "tyname" (map (mapNestedName nest))} claim updateName nest (IDef loc' n cs) = IDef loc' (mapNestedName nest n) cs updateName nest (IData loc' vis mbt d) diff --git a/src/TTImp/Elab/Term.idr b/src/TTImp/Elab/Term.idr index ef5440287ca..b23a447ee4e 100644 --- a/src/TTImp/Elab/Term.idr +++ b/src/TTImp/Elab/Term.idr @@ -18,6 +18,7 @@ import TTImp.Elab.Ambiguity import TTImp.Elab.App import TTImp.Elab.As import TTImp.Elab.Binders +import TTImp.Elab.BindingApp import TTImp.Elab.Case import TTImp.Elab.Check import TTImp.Elab.Dot @@ -160,6 +161,8 @@ checkTerm rig elabinfo nest env (IAutoApp fc fn arg) exp = checkApp rig elabinfo nest env fc fn [] [arg] [] exp checkTerm rig elabinfo nest env (IWithApp fc fn arg) exp = throw (GenericMsg fc "with application not implemented yet") +checkTerm rig elabinfo nest env (IBindingApp fn bind arg) exp + = checkBindingApplication rig elabinfo nest env fn bind arg exp checkTerm rig elabinfo nest env (INamedApp fc fn nm arg) exp = checkApp rig elabinfo nest env fc fn [] [] [(nm, arg)] exp checkTerm rig elabinfo nest env (ISearch fc depth) (Just gexpty) diff --git a/src/TTImp/Parser.idr b/src/TTImp/Parser.idr index bb04411a525..b450f15c1df 100644 --- a/src/TTImp/Parser.idr +++ b/src/TTImp/Parser.idr @@ -2,6 +2,7 @@ module TTImp.Parser import Core.Context import Core.TT +import Core.WithData import Parser.Source import TTImp.TTImp @@ -263,7 +264,7 @@ mutual pibindListName : OriginDesc -> FilePos -> IndentInfo -> - Rule (List (WithRig $ WithName RawImp)) + Rule (List (WithRig $ AddMetadata ("name" :-: DocBindFC Name) RawImp)) pibindListName fname start indents = do rigc <- multiplicity ns <- sepBy1 (symbol ",") (withFC userName) @@ -271,20 +272,20 @@ mutual ty <- expr fname indents atEnd indents rig <- getMult rigc - pure (map (\n => Mk [rig, n] ty) (forget ns)) + pure (map (\n => Mk [rig, AddDef $ AddDef n] ty) (forget ns)) <|> forget <$> sepBy1 (symbol ",") (do rigc <- multiplicity n <- withFC name symbol ":" ty <- expr fname indents rig <- getMult rigc - pure (Mk [rig, n] ty)) + pure (Mk [rig, AddDef $ AddDef n] ty)) pibindList : OriginDesc -> FilePos -> IndentInfo -> Rule (List (WithRig $ WithMName RawImp)) pibindList fname start indents = do params <- pibindListName fname start indents - pure $ map (\ty => Mk [ty.rig, Just ty.name] ty.val) params + pure $ map (\ty => Mk [ty.rig, Just ty.name.drop.drop] ty.val) params autoImplicitPi : OriginDesc -> IndentInfo -> Rule RawImp @@ -502,13 +503,12 @@ tyDecl : OriginDesc -> IndentInfo -> Rule ImpTy tyDecl fname indents = do start <- location n <- withFC name - nameEnd <- location symbol ":" ty <- expr fname indents end <- location atEnd indents let fc = MkFC fname start end - pure (Mk [fc, n] ty) + pure (Mk [fc, AddDef n] ty) mutual parseRHS : (withArgs : Nat) -> @@ -535,7 +535,7 @@ mutual ws <- nonEmptyBlock (clause (S withArgs) fname) end <- location let fc = MkFC fname start end - pure (MkPair !(getFn lhs) $ WithClause fc lhs rig wval prf [] (forget $ map snd ws)) + pure $ MkPair !(getFn lhs) $ WithClause fc lhs rig wval prf [] (forget $ map snd ws) <|> do keyword "impossible" atEnd indents @@ -606,7 +606,7 @@ dataDecl fname indents opts <- dataOpts cs <- block (tyDecl fname) end <- location - pure (MkImpData (MkFC fname start end) n (Just ty) opts cs) + pure (MkImpData (MkFC fname start end) (MkDef n) (Just ty) opts cs) recordParam : OriginDesc -> IndentInfo -> Rule (List (ImpParameter' RawImp)) recordParam fname indents @@ -626,9 +626,9 @@ recordParam fname indents <|> pure Implicit) params <- pibindListName fname start indents symbol "}" - pure (map (map (MkPiBindData info)) params) + pure (map (map (MkPiBindData Explicit)) params) <|> do n <- withFC name - pure [ Mk [top, n] (MkPiBindData Explicit (Implicit n.fc False)) ] + pure [ Mk [top, AddDef $ AddDef n] (MkPiBindData Explicit (Implicit n.fc False)) ] fieldDecl : OriginDesc -> IndentInfo -> Rule (List IField) fieldDecl fname indents @@ -649,8 +649,9 @@ fieldDecl fname indents symbol ":" ty <- expr fname indents end <- location - pure (map (\n => Mk [MkFC fname start end, linear, n] - (MkPiBindData p ty)) (forget ns)) + pure (map (\n : WithFC Name => + Mk [MkFC fname start end, linear, AddDef (AddDef n)] + (MkPiBindData p ty)) (forget ns)) recordDecl : OriginDesc -> IndentInfo -> Rule ImpDecl recordDecl fname indents @@ -670,7 +671,7 @@ recordDecl fname indents end <- location pure (let fc = MkFC fname start end in IRecord fc Nothing vis mbtot - (Mk [fc] $ MkImpRecord (Mk [n] params) (Mk [dc, opts] (concat flds)))) + (Mk [fc] $ MkImpRecord (Mk [AddDef n] params) (Mk [AddDef dc, opts] (concat flds)))) namespaceDecl : Rule Namespace namespaceDecl @@ -740,7 +741,8 @@ topDecl fname indents rig <- getMult m claim <- tyDecl fname indents end <- location - pure (IClaim (MkFCVal (MkFC fname start end) $ MkIClaimData rig vis opts claim)) + pure (IClaim (MkFCVal (MkFC fname start end) $ MkIClaimData rig vis opts + (claim))) <|> recordDecl fname indents <|> directive fname indents <|> definition fname indents diff --git a/src/TTImp/ProcessData.idr b/src/TTImp/ProcessData.idr index b0f6d3d7947..09c2a9558ee 100644 --- a/src/TTImp/ProcessData.idr +++ b/src/TTImp/ProcessData.idr @@ -93,14 +93,16 @@ checkCon : {vars : _} -> {auto o : Ref ROpts REPLOpts} -> List ElabOpt -> NestedNames vars -> Env Term vars -> Visibility -> (orig : Name) -> (resolved : Name) -> - ImpTy -> Core Constructor + (nameType : ImpTy) -> + Core Constructor checkCon {vars} opts nest env vis tn_in tn ty_raw - = do let cn_in = ty_raw.tyName + = do cn' <- traverse inCurrentNS ty_raw.tyName + let cn = cn'.val let fc = ty_raw.fc - cn <- inCurrentNS cn_in.val let ty_raw = updateNS tn_in tn ty_raw.val log "declare.data.constructor" 5 $ "Checking constructor type " ++ show cn ++ " : " ++ show ty_raw log "declare.data.constructor" 10 $ "Updated " ++ show (tn_in, tn) + log "declare.data.constructor" 10 $ "Binding info: " ++ show cn'.bind defs <- get Ctxt -- Check 'cn' is undefined @@ -108,7 +110,7 @@ checkCon {vars} opts nest env vis tn_in tn ty_raw | Just gdef => throw (AlreadyDefined fc cn) u <- uniVar fc ty <- - wrapErrorC opts (InCon cn_in) $ + wrapErrorC opts (InCon cn'.drop) $ checkTerm !(resolveName cn) InType opts nest env (IBindHere fc (PI erased) ty_raw) (gType fc u) @@ -127,7 +129,7 @@ checkCon {vars} opts nest env vis tn_in tn ty_raw addHashWithNames fullty log "module.hash" 15 "Adding hash for data constructor: \{show cn}" _ => pure () - pure (Mk [fc, NoFC cn, !(getArity defs Env.empty fullty)] fullty) + pure (Mk [fc, cn'.drop, !(getArity defs Env.empty fullty), cn'.bind] fullty) -- Get the indices of the constructor type (with non-constructor parts erased) getIndexPats : {auto c : Ref Ctxt Defs} -> @@ -408,7 +410,7 @@ processData : {vars : _} -> WithDefault Visibility Private -> Maybe TotalReq -> ImpData -> Core () processData {vars} eopts nest env fc def_vis mbtot (MkImpLater dfc n_in ty_raw) - = do n <- inCurrentNS n_in + = do n <- inCurrentNS n_in.val ty_raw <- bindTypeNames fc [] (toList vars) ty_raw defs <- get Ctxt @@ -429,7 +431,7 @@ processData {vars} eopts nest env fc def_vis mbtot (MkImpLater dfc n_in ty_raw) arity <- getArity defs Env.empty fullty -- Add the type constructor as a placeholder - tidx <- addDef n (newDef fc n top vars fullty def_vis + tidx <- addDef n (newDef {bind = n_in.bind} fc n top vars fullty def_vis (TCon arity NatSet.empty NatSet.empty defaultFlags [] Nothing Nothing)) addMutData (Resolved tidx) defs <- get Ctxt @@ -450,9 +452,10 @@ processData {vars} eopts nest env fc def_vis mbtot (MkImpLater dfc n_in ty_raw) setFlag fc n (SetTotal tot) processData {vars} eopts nest env fc def_vis mbtot (MkImpData dfc n_in mty_raw opts cons_raw) - = do n <- inCurrentNS n_in + = do typeName' <- traverse inCurrentNS n_in + let typeName = typeName'.val - log "declare.data" 1 $ "Processing " ++ show n + log "declare.data" 1 $ "Processing " ++ show typeName defs <- get Ctxt mmetasfullty <- flip traverseOpt mty_raw $ \ ty_raw => do @@ -460,11 +463,11 @@ processData {vars} eopts nest env fc def_vis mbtot (MkImpData dfc n_in mty_raw o u <- uniVar fc (ty, _) <- - wrapErrorC eopts (InCon $ MkFCVal fc n) $ - elabTerm !(resolveName n) InType eopts nest env + wrapErrorC eopts (InCon $ MkFCVal fc typeName) $ -- check if we can inherit the location from n_in + elabTerm !(resolveName typeName) InType eopts nest env (IBindHere fc (PI erased) ty_raw) (Just (gType dfc u)) - checkIsType fc n env !(nf defs env ty) + checkIsType fc typeName env !(nf defs env ty) pure (keys (getMetas ty), abstractEnvType dfc env ty) @@ -476,24 +479,24 @@ processData {vars} eopts nest env fc def_vis mbtot (MkImpData dfc n_in mty_raw o -- or we don't define them. -- When looking up, note the data types which were undefined at the -- point of declaration. - ndefm <- lookupCtxtExact n (gamma defs) + ndefm <- lookupCtxtExact typeName (gamma defs) (mw, vis, tot, fullty) <- the (Core (List Name, Visibility, Maybe TotalReq, ClosedTerm)) $ case ndefm of Nothing => case mfullty of - Nothing => throw (GenericMsg fc "Missing telescope for data definition \{show n_in}") + Nothing => throw (GenericMsg fc "Missing telescope for data definition \{show n_in.val}") Just fullty => pure ([], collapseDefault def_vis, mbtot, fullty) Just ndef => do vis <- the (Core Visibility) $ case collapseDefaults ndef.visibility def_vis of Right finalVis => pure finalVis Left (oldVis, newVis) => do -- TODO : In a later release, at least after 0.7.0, replace this with an error. - recordWarning (IncompatibleVisibility fc oldVis newVis n) + recordWarning (IncompatibleVisibility fc oldVis newVis typeName) pure (max oldVis newVis) let declTot = findSetTotal $ ndef.flags tot <- case (mbtot, declTot) of (Just oldTot, Just newTot) => do when (oldTot /= newTot) $ throw $ GenericMsgSol fc - "Data \{show n_in} has been forward-declared with totality `\{show oldTot}`, cannot change to `\{show newTot}`" + "Data \{show n_in.val} has been forward-declared with totality `\{show oldTot}`, cannot change to `\{show newTot}`" "Possible solutions" [ "Use the same totality modifiers" , "Remove the totality modifier from the declaration" @@ -511,28 +514,30 @@ processData {vars} eopts nest env fc def_vis mbtot (MkImpData dfc n_in mty_raw o else do logTermNF "declare.data" 1 "Previous" Env.empty (type ndef) logTermNF "declare.data" 1 "Now" Env.empty fullty throw (CantConvert fc (gamma defs) Env.empty (type ndef) fullty) - _ => throw (AlreadyDefined fc n) + _ => throw (AlreadyDefined fc typeName) - logTermNF "declare.data" 5 ("data " ++ show n) Env.empty fullty + logTermNF "declare.data" 5 ("data " ++ show typeName) Env.empty fullty arity <- getArity defs Env.empty fullty -- Add the type constructor as a placeholder while checking -- data constructors - tidx <- addDef n (newDef fc n linear vars fullty (specified vis) + tidx <- addDef typeName (newDef {bind = n_in.bind} fc typeName linear vars fullty (specified vis) (TCon arity NatSet.empty NatSet.empty defaultFlags [] Nothing Nothing)) case vis of Private => pure () - _ => do addHashWithNames n + _ => do addHashWithNames typeName addHashWithNames fullty - log "module.hash" 15 "Adding hash for data declaration with name \{show n}" + log "module.hash" 15 "Adding hash for data declaration with name \{show typeName}" + -- Constructors are private if the data type as a whole is -- export let cvis = if vis == Export then Private else vis - cons <- traverse (checkCon eopts nest env cvis n_in (Resolved tidx)) cons_raw + cons <- traverse (checkCon eopts nest env cvis n_in.val (Resolved tidx)) + (cons_raw) - let ddef = MkData (Mk [dfc, NoFC n, arity] fullty) cons + let ddef = MkData (Mk [dfc, typeName'.drop , arity, n_in.bind] fullty) cons ignore $ addData vars vis tidx ddef -- Flag data type as a newtype, if possible (See `findNewtype` for criteria). @@ -545,7 +550,7 @@ processData {vars} eopts nest env fc def_vis mbtot (MkImpData dfc n_in mty_raw o -- point it was declared, and every data type undefined right now defs <- get Ctxt let mutWith = nub (mw ++ mutData defs) - log "declare.data" 3 $ show n ++ " defined in a mutual block with " ++ show mw + log "declare.data" 3 $ show typeName ++ " defined in a mutual block with " ++ show mw setMutWith fc (Resolved tidx) mw traverse_ (processDataOpt fc (Resolved tidx)) opts @@ -555,9 +560,9 @@ processData {vars} eopts nest env fc def_vis mbtot (MkImpData dfc n_in mty_raw o setDetags fc (Resolved tidx) detags traverse_ addToSave metas - addToSave n + addToSave typeName log "declare.data" 10 $ - "Saving from " ++ show n ++ ": " ++ show metas + "Saving from " ++ show typeName ++ ": " ++ show metas let connames = map (.name.val) cons unless (NoHints `elem` opts) $ @@ -568,5 +573,5 @@ processData {vars} eopts nest env fc def_vis mbtot (MkImpData dfc n_in mty_raw o -- #1404 whenJust tot $ \ tot => do - log "declare.data" 5 $ "setting totality flag for \{show n} and its constructors" - for_ (n :: map (.name.val) cons) $ \ n => setFlag fc n (SetTotal tot) + log "declare.data" 5 $ "setting totality flag for \{show typeName} and its constructors" + for_ (typeName :: map (.name.val) cons) $ \ n => setFlag fc n (SetTotal tot) diff --git a/src/TTImp/ProcessDef.idr b/src/TTImp/ProcessDef.idr index 9ad9cdc32b4..4d16d25a928 100644 --- a/src/TTImp/ProcessDef.idr +++ b/src/TTImp/ProcessDef.idr @@ -913,7 +913,8 @@ lookupOrAddAlias : {vars : _} -> {auto s : Ref Syn SyntaxInfo} -> {auto o : Ref ROpts REPLOpts} -> List ElabOpt -> NestedNames vars -> Env Term vars -> FC -> - Name -> List ImpClause -> Core (Maybe GlobalDef) + Name -> -- mightbe worth changing to WithFC + List ImpClause -> Core (Maybe GlobalDef) lookupOrAddAlias eopts nest env fc n [cl@(PatClause _ lhs _)] = do defs <- get Ctxt log "declare.def.alias" 20 $ "Looking at \{show cl}" @@ -944,7 +945,7 @@ lookupOrAddAlias eopts nest env fc n [cl@(PatClause _ lhs _)] log "declare.def" 5 "Not a misspelling: go ahead and declare it!" processType eopts nest env fc top Public [] -- See #3409 - $ Mk [fc, MkFCVal fc n] $ holeyType (map snd args) + $ Mk [fc, Mk [NotBinding, fc] n] $ holeyType (map snd args) defs <- get Ctxt lookupCtxtExact n (gamma defs) diff --git a/src/TTImp/ProcessFnOpt.idr b/src/TTImp/ProcessFnOpt.idr index ec3491a8872..53e1ca81b91 100644 --- a/src/TTImp/ProcessFnOpt.idr +++ b/src/TTImp/ProcessFnOpt.idr @@ -77,6 +77,12 @@ processFnOpt fc _ ndef (Totality tot) setFlag fc ndef (SetTotal tot) processFnOpt fc _ ndef Macro = setFlag fc ndef Macro +processFnOpt fc _ ndef (Binding b) + = do defs <- get Ctxt + Just def <- lookupCtxtExact ndef (gamma defs) + | Nothing => undefinedName fc ndef + let dx : GlobalDef = { bindingMode := b } def + ignore $ addDef ndef dx processFnOpt fc _ ndef (SpecArgs ns) = do defs <- get Ctxt Just gdef <- lookupCtxtExact ndef (gamma defs) diff --git a/src/TTImp/ProcessRecord.idr b/src/TTImp/ProcessRecord.idr index d569aff2346..54ee74ee1d7 100644 --- a/src/TTImp/ProcessRecord.idr +++ b/src/TTImp/ProcessRecord.idr @@ -6,6 +6,7 @@ import Core.Core import Core.Env import Core.Metadata import Core.UnifyState +import Core.WithData import Idris.REPL.Opts import Idris.Syntax @@ -47,19 +48,21 @@ elabRecord : {vars : _} -> NestedNames vars -> Maybe String -> WithDefault Visibility Private -> Maybe TotalReq -> - (tyName : Name) -> - (params : List ImpParameter) -> + (tyName : FCBind Name) -> + (params : List (ImpParameter' RawImp)) -> (opts : List DataOpt) -> - (conName : Name) -> + (conName : FCBind Name) -> List IField -> Core () elabRecord {vars} eopts fc env nest newns def_vis mbtot tn_in params0 opts conName_in fields - = do tn <- inCurrentNS tn_in - conName <- inCurrentNS conName_in + = do tn <- traverse inCurrentNS tn_in + conName <- traverse inCurrentNS conName_in params <- preElabAsData tn log "declare.record.parameters" 100 $ unlines ("New list of parameters:" :: map ((" " ++) . displayParam) params) elabAsData tn conName params + let conName = conName.val -- we don't need the binding information after this point + let tn = tn.val defs <- get Ctxt Just conty <- lookupTyExact conName (gamma defs) | Nothing => throw (InternalError ("Adding " ++ show tn ++ "failed")) @@ -96,13 +99,13 @@ elabRecord {vars} eopts fc env nest newns def_vis mbtot tn_in params0 opts conNa -> (AddFC $ WithRig $ WithMName (PiBindData RawImp)) -- Record type parameters are implicit in the constructor -- and projections - jname binder = Mk [EmptyFC, erased, Just binder.name] $ {info := Implicit} binder.val + jname binder = Mk [EmptyFC, erased, Just binder.name.drop.drop] $ {info := Implicit} binder.val fname : IField -> Name fname field = field.name.val farg : IField -> AddFC (WithRig $ WithMName (PiBindData RawImp)) - farg field = Mk [virtualiseFC field.fc, field.rig, Just field.name] field.val + farg field = Mk [virtualiseFC field.fc, field.rig, Just field.name.drop.drop] field.val mkTy : List (AddFC $ WithRig $ WithMName (PiBindData RawImp)) -> RawImp -> RawImp mkTy [] ret = ret @@ -139,15 +142,16 @@ elabRecord {vars} eopts fc env nest newns def_vis mbtot tn_in params0 opts conNa -- otherwise `a` will be bound as a field rather than a parameter! -- We pre-elaborate the datatype, thus resolving all the missing bindings, -- and return the new list of parameters - preElabAsData : (tn : Name) -> -- fully qualified name of the record type + preElabAsData : (tn : FCBind Name) -> -- fully qualified name of the record type Core (List ImpParameter) -- New telescope of parameters, including missing bindings - preElabAsData tn + preElabAsData tn' = do let fc = virtualiseFC fc + let tn = tn'.val let dataTy = IBindHere fc (PI erased) !(bindTypeNames fc [] (toList vars) (mkDataTy fc params0)) defs <- get Ctxt -- Create a forward declaration if none exists when (isNothing !(lookupTyExact tn (gamma defs))) $ do - let dt = MkImpLater fc tn dataTy + let dt = MkImpLater fc tn' dataTy log "declare.record" 10 $ "Pre-declare record data type: \{show dt}" processDecl [] nest env (IData fc def_vis mbtot dt) defs <- get Ctxt @@ -158,7 +162,7 @@ elabRecord {vars} eopts fc env nest newns def_vis mbtot tn_in params0 opts conNa ty <- unelabNest (NoSugar True) !nestDrop tyenv ty log "declare.record.parameters" 30 "Unelaborated type: \{show ty}" params <- getParameters [<] ty - addMissingNames ([<] <>< map (\x => x.name) params0 ) params [] + addMissingNames ([<] <>< map (.name) params0 ) params [] where @@ -171,7 +175,7 @@ elabRecord {vars} eopts fc env nest newns def_vis mbtot tn_in params0 opts conNa dropLeadingPis [] ty env = do unless (null vars) $ logC "declare.record.parameters" 60 $ pure $ unlines - [ "We elaborated \{show tn} in a non-empty local context." + [ "We elaborated \{show tn'.val} in a non-empty local context." , " Dropped: \{show vars}" , " Remaining type: \{show !(toFullNames ty)}" ] @@ -191,7 +195,7 @@ elabRecord {vars} eopts fc env nest newns def_vis mbtot tn_in params0 opts conNa getParameters acc ty = throw (InternalError "Malformed record type \{show ty}") addMissingNames : - SnocList (WithFC Name) -> + SnocList (DocBindFC Name) -> SnocList (WithRig $ WithMName $ PiBindData RawImp) -> List ImpParameter -> -- accumulator Core (List ImpParameter) @@ -201,7 +205,7 @@ elabRecord {vars} eopts fc env nest newns def_vis mbtot tn_in params0 opts conNa = do tele <- flip Core.traverseSnocList tele $ \ rest => case rest.mName of Nothing => throw (InternalError "Some names have disappeared?! \{show rest.val}") - Just nm => pure (Mk [rest.rig, nm] rest.val) -- (nm, rest) + Just nm => pure (Mk [rest.rig, AddDef (AddDef nm)] rest.val) -- (nm, rest) unless (null tele) $ log "declare.record.parameters" 50 $ unlines ( "Decided to bind the following extra parameters:" @@ -212,16 +216,16 @@ elabRecord {vars} eopts fc env nest newns def_vis mbtot tn_in params0 opts conNa = throw (InternalError "Some arguments have disappeared") - elabAsData : (tn : Name) -> -- fully qualified name of the record type - (conName : Name) -> -- fully qualified name of the record type constructor + elabAsData : (tyName : FCBind Name) -> -- fully qualified name of the record type + (conName : FCBind Name) -> -- fully qualified name of the record type constructor (params : List ImpParameter) -> -- telescope of parameters Core () - elabAsData tn cname params + elabAsData tn conName params = do let fc = virtualiseFC fc let conty = mkTy (paramTelescope params) $ - mkTy (map farg fields) (recTy tn params) + mkTy (map farg fields) (recTy tn.val params) let boundNames = paramNames params ++ map fname fields ++ (toList vars) - let con = Mk [virtualiseFC fc, NoFC cname] + let con = Mk [virtualiseFC fc, conName] !(bindTypeNames fc [] boundNames conty) let dt = MkImpData fc tn Nothing opts [con] log "declare.record" 5 $ "Record data type " ++ show dt @@ -250,7 +254,7 @@ elabRecord {vars} eopts fc env nest newns def_vis mbtot tn_in params0 opts conNa elabGetters tn con params done upds tyenv (Bind bfc n b@(Pi _ rc imp ty_chk) sc) = let rig = if isErased rc then erased else top isVis = projVis (collapseDefault def_vis) - paramNames = map (\x => x.name.val) params + paramNames = map (.name.val) params in if (n `elem` paramNames) || (n `elem` vars) then elabGetters tn con params (if imp == Explicit && not (n `elem` vars) @@ -273,8 +277,8 @@ elabRecord {vars} eopts fc env nest newns def_vis mbtot tn_in params0 opts conNa mkTy (paramTelescope params) $ IPi bfc top Explicit (Just rname) (recTy tn params) ty' let fc' = virtualiseFC fc - let mkProjClaim = \ nm => - let ty = Mk [fc', MkFCVal fc' nm] projTy + let mkProjClaim = \ nm => -- This nm ought to be WithFC Name + let ty = Mk [fc', Mk [NotBinding, fc'] nm] projTy in IClaim (MkFCVal bfc (MkIClaimData rig isVis [Inline] ty)) log "declare.record.projection.claim" 5 $ @@ -354,4 +358,4 @@ processRecord : {vars : _} -> WithDefault Visibility Private -> Maybe TotalReq -> ImpRecord -> Core () processRecord eopts nest env newns def_vis mbtot rec@(MkWithData _ $ MkImpRecord header body) - = elabRecord eopts rec.fc env nest newns def_vis mbtot header.name.val header.val body.opts body.name.val body.val + = elabRecord eopts rec.fc env nest newns def_vis mbtot header.tyName header.val body.opts body.tyName body.val diff --git a/src/TTImp/ProcessType.idr b/src/TTImp/ProcessType.idr index b709a6607ac..43e345cf0a0 100644 --- a/src/TTImp/ProcessType.idr +++ b/src/TTImp/ProcessType.idr @@ -157,7 +157,7 @@ processType {vars} eopts nest env fc rig vis opts ty_raw addNameLoc typeName.fc n log "declare.type" 1 $ "Processing " ++ show n - log "declare.type" 5 $ unwords ["Checking type decl:", show rig, show n, ":", show ty_raw] + log "declare.type" 5 $ unwords ["Checking type decl:", show rig, show n, ":", show ty_raw.val] idx <- resolveName n -- Check 'n' is undefined diff --git a/src/TTImp/Reflect.idr b/src/TTImp/Reflect.idr index a2562e13a70..d4616527410 100644 --- a/src/TTImp/Reflect.idr +++ b/src/TTImp/Reflect.idr @@ -6,6 +6,7 @@ import Core.Normalise import Core.Reflect import Core.TT import Core.Value +import Core.WithData import TTImp.TTImp import Libraries.Data.WithDefault @@ -86,7 +87,6 @@ Reflect DotReason where reflect fc defs lhs env UnderAppliedCon = getCon fc defs (reflectionttimp "UnderAppliedCon") - mutual export Reify RawImp where @@ -261,6 +261,16 @@ mutual _ => cantReify val "IFieldUpdate" reify defs val = cantReify val "IFieldUpdate" + export + Reify BindingModifier where + reify defs val@(NDCon _ n _ _ args) + = case (dropAllNS !(full (gamma defs) n), args) of + (UN (Basic "NotBinding"), _) => pure NotBinding + (UN (Basic "Typebind"), _) => pure Typebind + (UN (Basic "Autobind"), _) => pure Autobind + _ => cantReify val "BindingModifier" + reify defs val = cantReify val "BindingModifier" + export Reify AltType where reify defs val@(NDCon _ n _ _ args) @@ -314,9 +324,9 @@ mutual = case (dropAllNS !(full (gamma defs) n), map snd args) of (UN (Basic "MkTy"), [w, y, z]) => do fc' <- reify defs !(evalClosure defs w) - name' <- the (Core (WithFC Name)) (reify defs !(evalClosure defs y)) + name' <- reify defs !(evalClosure defs y) term' <- reify defs !(evalClosure defs z) - pure (Mk [fc', name'] term') + pure (Mk [fc', MkDef name'] term') _ => cantReify val "ITy" reify defs val = cantReify val "ITy" @@ -344,12 +354,12 @@ mutual x' <- reify defs !(evalClosure defs x) y' <- reify defs !(evalClosure defs y) z' <- reify defs !(evalClosure defs z) - pure (MkImpData v' w' x' y' z') + pure (MkImpData v' (MkDef w') x' y' z') (UN (Basic "MkLater"), [x,y,z]) => do x' <- reify defs !(evalClosure defs x) y' <- reify defs !(evalClosure defs y) z' <- reify defs !(evalClosure defs z) - pure (MkImpLater x' y' z') + pure (MkImpLater x' (MkDef y') z') _ => cantReify val "Data" reify defs val = cantReify val "Data" @@ -363,7 +373,7 @@ mutual info <- reify defs !(evalClosure defs x) name <- reify defs !(evalClosure defs y) type <- reify defs !(evalClosure defs z) - pure (Mk [fc, rig, NoFC name] (MkPiBindData info type)) + pure (Mk [fc, rig, MkDef name] (MkPiBindData info type)) _ => cantReify val "IField" reify defs val = cantReify val "IField" @@ -378,8 +388,8 @@ mutual opts <- reify defs !(evalClosure defs y) conName <- reify defs !(evalClosure defs z) fields <- reify defs !(evalClosure defs a) - pure (Mk [fc] $ MkImpRecord (Mk [NoFC tyName] (map fromOldParams params)) - (Mk [NoFC conName, opts] fields)) + pure (Mk [fc] $ MkImpRecord (Mk [MkDef tyName] (map fromOldParams params)) + (Mk [MkDef conName, opts] fields)) _ => cantReify val "Record" reify defs val = cantReify val "Record" @@ -538,6 +548,8 @@ mutual f' <- reflect fc defs lhs env f a' <- reflect fc defs lhs env a appCon fc defs (reflectionttimp "IApp") [fc', f', a'] + reflect fc defs lhs env (IBindingApp tfc f a) + = ?TODOReflect3 reflect fc defs lhs env (IAutoApp tfc f a) = do fc' <- reflect fc defs lhs env tfc f' <- reflect fc defs lhs env f @@ -693,12 +705,13 @@ mutual reflect fc defs lhs env (SpecArgs r) = do r' <- reflect fc defs lhs env r appCon fc defs (reflectionttimp "SpecArgs") [r'] + reflect fc defs lhs env (Binding r) = ?add export Reflect ImpTy where reflect fc defs lhs env ty = do w' <- reflect fc defs lhs env ty.fc - x' <- reflect fc defs lhs env ty.tyName + x' <- reflect fc defs lhs env ty.tyName.drop z' <- reflect fc defs lhs env ty.val appCon fc defs (reflectionttimp "MkTy") [w', x', z'] @@ -716,14 +729,14 @@ mutual Reflect ImpData where reflect fc defs lhs env (MkImpData v w x y z) = do v' <- reflect fc defs lhs env v - w' <- reflect fc defs lhs env w + w' <- reflect fc defs lhs env w.val x' <- reflect fc defs lhs env x y' <- reflect fc defs lhs env y z' <- reflect fc defs lhs env z appCon fc defs (reflectionttimp "MkData") [v', w', x', y', z'] reflect fc defs lhs env (MkImpLater x y z) = do x' <- reflect fc defs lhs env x - y' <- reflect fc defs lhs env y + y' <- reflect fc defs lhs env y.val z' <- reflect fc defs lhs env z appCon fc defs (reflectionttimp "MkLater") [x', y', z'] @@ -740,10 +753,10 @@ mutual Reflect ImpRecord where reflect fc defs lhs env r@(MkWithData _ $ MkImpRecord header body) = do v' <- reflect fc defs lhs env r.fc - w' <- reflect fc defs lhs env header.name.val + w' <- reflect fc defs lhs env header.tyName.val x' <- reflect fc defs lhs env (map toOldParams header.val) y' <- reflect fc defs lhs env body.opts - z' <- reflect fc defs lhs env body.name.val + z' <- reflect fc defs lhs env body.tyName.val a' <- reflect fc defs lhs env body.val appCon fc defs (reflectionttimp "MkRecord") [v', w', x', y', z', a'] diff --git a/src/TTImp/TTImp.idr b/src/TTImp/TTImp.idr index e5f5dcc22b5..7ccd12f92e6 100644 --- a/src/TTImp/TTImp.idr +++ b/src/TTImp/TTImp.idr @@ -8,6 +8,7 @@ import Core.Options import Core.Options.Log import Core.TT import Core.Value +import public Core.WithData import Data.List import public Data.List1 @@ -96,6 +97,8 @@ mutual 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 + IBindingApp : (fn : WithFC Name) -> (bound : WithFC (BindingInfo (RawImp' nm))) -> + (scope : WithFC (RawImp' nm)) -> RawImp' nm ISearch : FC -> (depth : Nat) -> RawImp' nm IAlternative : FC -> AltType' nm -> List (RawImp' nm) -> RawImp' nm @@ -191,6 +194,14 @@ mutual = "(" ++ show f ++ " [" ++ show a ++ "])" show (IWithApp fc f a) = "(" ++ show f ++ " | " ++ show a ++ ")" + show (IBindingApp nm binder scope) + = case binder.val of + (BindType name type) => + "\{show nm.val} (\{show name} : \{show type}) | \{show scope.val}" + (BindExpr name expr) => + "\{show nm.val} (\{show name} := \{show expr}) | \{show scope.val}" + (BindExplicitType name type expr) => + "\{show nm.val} (\{show name} : \{show type} := \{show expr}) | \{show scope.val}" show (ISearch fc d) = "%search" show (IAlternative fc ty alts) @@ -253,6 +264,8 @@ mutual Totality : TotalReq -> FnOpt' nm Macro : FnOpt' nm SpecArgs : List Name -> FnOpt' nm + Binding : BindingModifier -> FnOpt' nm + %name FnOpt' fopt public export @@ -288,6 +301,7 @@ mutual show (Totality PartialOK) = "partial" show Macro = "%macro" show (SpecArgs ns) = "%spec " ++ showSep " " (map show ns) + show (Binding b) = show b export Eq FnOpt where @@ -325,13 +339,13 @@ mutual public export data ImpData' : Type -> Type where - MkImpData : FC -> (n : Name) -> + MkImpData : FC -> (tyName : FCBind Name) -> -- if we have already declared the type using `MkImpLater`, -- we are allowed to leave the telescope out here. (tycon : Maybe (RawImp' nm)) -> (opts : List DataOpt) -> (datacons : List (ImpTy' nm)) -> ImpData' nm - MkImpLater : FC -> (n : Name) -> (tycon : RawImp' nm) -> ImpData' nm + MkImpLater : FC -> (n : FCBind Name) -> (tycon : RawImp' nm) -> ImpData' nm %name ImpData' dat @@ -339,11 +353,11 @@ mutual covering Show nm => Show (ImpData' nm) where show (MkImpData fc n (Just tycon) _ cons) - = "(%data " ++ show n ++ " " ++ show tycon ++ " " ++ show cons ++ ")" + = "(%data " ++ show n.val ++ " " ++ show tycon ++ " " ++ show (map val cons) ++ ")" show (MkImpData fc n Nothing _ cons) - = "(%data " ++ show n ++ " " ++ show cons ++ ")" + = "(%data " ++ show n.val ++ " " ++ show (map val cons) ++ ")" show (MkImpLater fc n tycon) - = "(%datadecl " ++ show n ++ " " ++ show tycon ++ ")" + = "(%datadecl " ++ show n.val ++ " " ++ show tycon ++ ")" public export IField : Type @@ -359,7 +373,7 @@ mutual public export ImpParameter' : Type -> Type - ImpParameter' nm = WithRig $ WithName $ PiBindData nm + ImpParameter' nm = WithRig $ AddMetadata ("name" :-: DocBindFC Name) $ PiBindData nm -- old datatype for ImpParameter, used for elabreflection compatibility public export @@ -372,11 +386,7 @@ mutual public export fromOldParams : OldParameters' nm -> ImpParameter' (RawImp' nm) - fromOldParams (nm, rig, info,type) = Mk [rig, NoFC nm] (MkPiBindData info type) - - export - Show nm => Show (ImpParameter' nm) where - show x = "\{show x.rig}\{show x.name.val} \{show x.val.boundType}" + fromOldParams (nm, rig, info,type) = Mk [rig, MkDef nm] (MkPiBindData info type) public export 0 ImpRecord : Type @@ -384,11 +394,11 @@ mutual public export 0 DataHeader : Type -> Type -- the name is the type constructor's name - DataHeader nm = WithName $ List (ImpParameter' (RawImp' nm)) + DataHeader nm = AddMetadata TyName' $ List (ImpParameter' (RawImp' nm)) public export 0 RecordBody : Type -> Type -- The name is the data constructor's name - RecordBody nm = WithName $ WithOpts $ List (IField' nm) + RecordBody nm = AddMetadata TyName' $ WithOpts $ List (IField' nm) ||| A record is defined by its header containing the name and parameters, and its body ||| containing the constructor name, options, and a list of fields @@ -401,15 +411,15 @@ mutual export covering Show nm => Show (IField' nm) where - show f@(MkWithData _ (MkPiBindData Explicit ty)) = show f.name.val ++ " : " ++ show ty - show f@(MkWithData _ ty) = "{" ++ show f.name.val ++ " : " ++ show ty.boundType ++ "}" + show f@(MkWithData _ (MkPiBindData Explicit ty)) = show {ty = Name} f.name.val ++ " : " ++ show ty + show f@(MkWithData _ ty) = "{" ++ show {ty = Name} f.name.val ++ " : " ++ show ty.boundType ++ "}" export covering Show nm => Show (ImpRecordData nm) where show (MkImpRecord header body) - = "record " ++ show header.name.val ++ " " ++ show header.val ++ - " " ++ show body.name.val ++ "\n\t" ++ + = "record " ++ show header.tyName.val ++ " " ++ show header.val ++ + " " ++ show body.tyName.val ++ "\n\t" ++ showSep "\n\t" (map show body.val) ++ "\n" public export @@ -495,11 +505,16 @@ mutual %name ImpDecl' decl + export + covering + Show nm => Show (ImpParameter' nm) where + show params = "\{show params.rig} \{show params.val.info} \{show params.val.boundType}" + export covering Show nm => Show (ImpDecl' nm) where show (IClaim (MkWithData _ $ MkIClaimData c _ opts ty)) - = show opts ++ " " ++ show c ++ " " ++ show ty + = show opts ++ " " ++ show c ++ " " ++ show ty.val show (IData _ _ _ d) = show d show (IDef _ n cs) = "(%def " ++ show n ++ " " ++ show cs ++ ")" show (IParameters _ ps ds) @@ -825,13 +840,13 @@ definedInBlock ns decls = defName ns acc (IClaim c) = insert (expandNS ns (getName c.val.type)) acc defName ns acc (IDef _ nm _) = insert (expandNS ns nm) acc defName ns acc (IData _ _ _ (MkImpData _ n _ _ cons)) - = foldl (flip insert) acc $ expandNS ns n :: map (expandNS ns . getName) cons - defName ns acc (IData _ _ _ (MkImpLater _ n _)) = insert (expandNS ns n) acc + = foldl (flip insert) acc $ expandNS ns n.val :: map (expandNS ns . getName) cons + defName ns acc (IData _ _ _ (MkImpLater _ n _)) = insert (expandNS ns n.val) acc defName ns acc (IParameters _ _ pds) = foldl (defName ns) acc pds defName ns acc (IFail _ _ nds) = foldl (defName ns) acc nds defName ns acc (INamespace _ n nds) = foldl (defName (ns <.> n)) acc nds defName ns acc (IRecord _ fldns _ _ rec) - = foldl (flip insert) acc $ expandNS ns rec.val.body.name.val :: all + = foldl (flip insert) acc $ expandNS ns rec.val.body.tyName.val :: all where fldns' : Namespace fldns' = maybe ns (\ f => ns <.> mkNamespace f) fldns @@ -854,7 +869,7 @@ definedInBlock ns decls = -- inside the parameter block) -- so let's just declare all of them and some may go unused. all : List Name - all = expandNS ns rec.val.header.name.val :: map (expandNS fldns') (fnsRF ++ fnsUN) + all = expandNS ns rec.val.header.tyName.val :: map (expandNS fldns') (fnsRF ++ fnsUN) defName ns acc (IPragma _ pns _) = foldl (flip insert) acc $ map (expandNS ns) pns defName _ acc _ = acc @@ -883,6 +898,7 @@ getFC (IApp x _ _) = x getFC (INamedApp x _ _ _) = x getFC (IAutoApp x _ _) = x getFC (IWithApp x _ _) = x +getFC (IBindingApp x _ y) = fromMaybe EmptyFC (mergeFC x.fc y.fc) getFC (ISearch x _) = x getFC (IAlternative x _ _) = x getFC (IRewrite x _ _) = x diff --git a/src/TTImp/TTImp/Functor.idr b/src/TTImp/TTImp/Functor.idr index 8baaf30baf3..1925f61242d 100644 --- a/src/TTImp/TTImp/Functor.idr +++ b/src/TTImp/TTImp/Functor.idr @@ -3,6 +3,8 @@ module TTImp.TTImp.Functor import Core.TT import Core.WithData import TTImp.TTImp +import Core.FC + %default covering @@ -33,6 +35,8 @@ mutual = INamedApp fc (map f fn) nm (map f t) map f (IWithApp fc fn t) = IWithApp fc (map f fn) (map f t) + map f (IBindingApp fn bn sc) + = IBindingApp fn (map (map (map f)) bn) (map (map f) sc) map f (ISearch fc n) = ISearch fc n map f (IAlternative fc alt ts) @@ -132,6 +136,7 @@ mutual map f (Totality tot) = Totality tot map f Macro = Macro map f (SpecArgs ns) = SpecArgs ns + map f (Binding b) = Binding b export Functor ImpData' where diff --git a/src/TTImp/TTImp/TTC.idr b/src/TTImp/TTImp/TTC.idr index 439fef12caa..d87761b94fe 100644 --- a/src/TTImp/TTImp/TTC.idr +++ b/src/TTImp/TTImp/TTC.idr @@ -48,7 +48,6 @@ mutual = do tag 12; toBuf fc; toBuf x; toBuf y toBuf (ICoerced fc y) = do tag 13; toBuf fc; toBuf y - toBuf (IBindHere fc m y) = do tag 14; toBuf fc; toBuf m; toBuf y toBuf (IBindVar fc y) @@ -92,6 +91,9 @@ mutual = do tag 30; toBuf fc; toBuf ns; toBuf rhs toBuf (IAutoApp fc fn arg) = do tag 31; toBuf fc; toBuf fn; toBuf arg + toBuf (IBindingApp fn bind arg) + = do tag 32; toBuf fn; toBuf bind; toBuf arg + fromBuf = case !getTag of @@ -186,6 +188,10 @@ mutual 31 => do fc <- fromBuf; fn <- fromBuf arg <- fromBuf pure (IAutoApp fc fn arg) + 32 => do fn <- fromBuf + bind <- fromBuf + arg <- fromBuf + pure (IBindingApp fn bind arg) _ => corrupt "RawImp" export @@ -327,6 +333,7 @@ mutual toBuf Unsafe = tag 13 toBuf Deprecate = tag 14 toBuf (ForeignExport cs) = do tag 15; toBuf cs + toBuf (Binding b) = do tag 16 ; toBuf b fromBuf = case !getTag of diff --git a/src/TTImp/TTImp/Traversals.idr b/src/TTImp/TTImp/Traversals.idr index 79aca98148b..b2bbc69d17e 100644 --- a/src/TTImp/TTImp/Traversals.idr +++ b/src/TTImp/TTImp/Traversals.idr @@ -41,6 +41,7 @@ parameters (f : RawImp' nm -> RawImp' nm) mapFnOpt (Totality treq) = Totality treq mapFnOpt Macro = Macro mapFnOpt (SpecArgs ns) = SpecArgs ns + mapFnOpt (Binding b) = Binding b export mapImpData : ImpData' nm -> ImpData' nm @@ -98,6 +99,7 @@ parameters (f : RawImp' nm -> RawImp' nm) mapTTImp (IAutoApp fc t u) = f $ IAutoApp fc (mapTTImp t) (mapTTImp u) mapTTImp (INamedApp fc t n u) = f $ INamedApp fc (mapTTImp t) n (mapTTImp u) mapTTImp (IWithApp fc t u) = f $ IWithApp fc (mapTTImp t) (mapTTImp u) + mapTTImp (IBindingApp fn b s) = assert_total $ f $ IBindingApp fn (map (map mapTTImp) b) (map mapTTImp s) mapTTImp (ISearch fc depth) = f $ ISearch fc depth mapTTImp (IAlternative fc alt ts) = f $ IAlternative fc (mapAltType alt) (assert_total map mapTTImp ts) mapTTImp (IRewrite fc t u) = f $ IRewrite fc (mapTTImp t) (mapTTImp u) diff --git a/src/TTImp/Utils.idr b/src/TTImp/Utils.idr index 1319417ccae..df30cba2c1d 100644 --- a/src/TTImp/Utils.idr +++ b/src/TTImp/Utils.idr @@ -100,6 +100,8 @@ findBindableNames arg env used (IAutoApp fc fn av) = findBindableNames False env used fn ++ findBindableNames True env used av findBindableNames arg env used (IWithApp fc fn av) = findBindableNames False env used fn ++ findBindableNames True env used av +findBindableNames arg env used (IBindingApp fn bound scope) + = findBindableNames False env used bound.val.getBoundExpr findBindableNames arg env used (IAs fc _ _ nm@(UN (Basic n)) pat) = (nm, UN $ Basic $ genUniqueStr used n) :: findBindableNames arg env used pat findBindableNames arg env used (IAs fc _ _ n pat) @@ -149,6 +151,11 @@ findBindableNamesQuot env used (IAutoApp fc x y) = findBindableNamesQuot env used ![x, y] findBindableNamesQuot env used (IWithApp fc x y) = findBindableNamesQuot env used ![x, y] +findBindableNamesQuot env used (IBindingApp x bind z) + = case bind.val of + (BindType _ ty) => findBindableNamesQuot env used ![ty, z.val] + (BindExpr _ expr) => findBindableNamesQuot env used ![expr, z.val] + (BindExplicitType _ ty expr) => findBindableNamesQuot env used ![ty, expr, z.val] findBindableNamesQuot env used (IRewrite fc x y) = findBindableNamesQuot env used ![x, y] findBindableNamesQuot env used (ICoerced fc x) @@ -479,7 +486,7 @@ mutual substLocDecl : FC -> ImpDecl -> ImpDecl substLocDecl fc' (IClaim (MkWithData _ $ MkIClaimData r vis opts td)) - = IClaim (MkFCVal fc' $ MkIClaimData r vis opts (map (substLoc fc') (set "fc" fc' td))) + = IClaim (Mk [fc'] $ MkIClaimData r vis opts (map (substLoc fc') (set "fc" fc' td))) substLocDecl fc' (IDef fc n cs) = IDef fc' n (map (substLocClause fc') cs) substLocDecl fc' (IData fc vis mbtot d) diff --git a/tests/idris2/basic/binding001/Test.idr b/tests/idris2/basic/binding001/Test.idr new file mode 100644 index 00000000000..6f660555cdb --- /dev/null +++ b/tests/idris2/basic/binding001/Test.idr @@ -0,0 +1,50 @@ + +import Data.Vect + +record Container where + typebind constructor MkCont + base : Type + fibre : base -> Type + +%hide Prelude.(&&) + +export +typebind +Exists : (t : Type) -> (t -> Type) -> Type +Exists = DPair + +ListCont : Container +ListCont = MkCont (n : Nat) | Fin n + +val2 : Exists Nat (\n => Vect n Nat) +val2 = (4 ** [0,1,2,3]) + +typebind +record Σ (t : Type) (s : t -> Type) where + constructor (&&) + π1 : t + π2 : s π1 + +(=>>) : (t : Type) -> (t -> Type) -> Type +(=>>) a b = (x : a) -> b x + +private typebind infixr 0 =>> + +autobind +loop : Applicative f => Foldable t => t a -> (a -> f b) -> f () +loop = Prelude.for_ + +val : Exists (n : Nat) | Vect n Nat +val = (4 ** [0,1,2,3]) + +main : IO () +main = loop (x <- [0 .. 10]) | + printLn x + +sigmaPi : Σ (ty : Type) | (x : ty) =>> Type +sigmaPi = (Type && List) + +nestedSigma : Σ (ty : Type) | Σ (n : Nat) | Vect n ty +nestedSigma = (String && 2 && ["hello", "world"]) + + diff --git a/tests/idris2/basic/binding001/expected b/tests/idris2/basic/binding001/expected new file mode 100644 index 00000000000..76b3a984d2f --- /dev/null +++ b/tests/idris2/basic/binding001/expected @@ -0,0 +1,12 @@ +1/1: Building Test (Test.idr) +0 +1 +2 +3 +4 +5 +6 +7 +8 +9 +10 diff --git a/tests/idris2/basic/binding001/run b/tests/idris2/basic/binding001/run new file mode 100755 index 00000000000..0d3c0452e07 --- /dev/null +++ b/tests/idris2/basic/binding001/run @@ -0,0 +1,4 @@ +. ../../../testutils.sh + +check Test.idr +run Test.idr diff --git a/tests/idris2/basic/binding002/Test.idr b/tests/idris2/basic/binding002/Test.idr new file mode 100644 index 00000000000..d721360bde2 --- /dev/null +++ b/tests/idris2/basic/binding002/Test.idr @@ -0,0 +1,21 @@ + +import Data.Vect + +record Container where + typebind constructor MkCont + base : Type + fibre : base -> Type + +typebind +record Sigma (a : Type) (b : a -> Type) where + constructor (*) + p1 : a + p2 : b p1 + +record Morphism (c1, c2 : Container) where + constructor MkMor + cont : (x : c1.base) -> Sigma (y : c2.base) | c2.fibre y -> c1.fibre x + +fwd : Morphism a b -> a.base -> b.base +fwd (MkMor c) x = p1 (c x) + diff --git a/tests/idris2/basic/binding002/expected b/tests/idris2/basic/binding002/expected new file mode 100644 index 00000000000..31e5db7f32c --- /dev/null +++ b/tests/idris2/basic/binding002/expected @@ -0,0 +1 @@ +1/1: Building Test (Test.idr) diff --git a/tests/idris2/basic/binding002/run b/tests/idris2/basic/binding002/run new file mode 100755 index 00000000000..d35387bb391 --- /dev/null +++ b/tests/idris2/basic/binding002/run @@ -0,0 +1,3 @@ +. ../../../testutils.sh + +check Test.idr diff --git a/tests/idris2/operators/operators002/Test.idr b/tests/idris2/operators/operators002/Test.idr index 901e7dda885..f7be6fe5455 100644 --- a/tests/idris2/operators/operators002/Test.idr +++ b/tests/idris2/operators/operators002/Test.idr @@ -32,7 +32,7 @@ MyLet : (val) -> (val -> rest) -> rest MyLet arg fn = fn arg program : Nat -program = (n := 3) `MyLet` 2 + n +program = (n <- 3) `MyLet` 2 + n program2 : Nat -program2 = (n : Nat := 3) `MyLet` 2 + n +program2 = (n : Nat <- 3) `MyLet` 2 + n From 6b7773e6e6f8ca012f7d7b91705719eb714a2054 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andr=C3=A9=20Videla?= Date: Mon, 25 Aug 2025 16:23:05 +0100 Subject: [PATCH 2/8] fix reflection --- src/TTImp/Reflect.idr | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/TTImp/Reflect.idr b/src/TTImp/Reflect.idr index d4616527410..704fd1b10ca 100644 --- a/src/TTImp/Reflect.idr +++ b/src/TTImp/Reflect.idr @@ -324,9 +324,9 @@ mutual = case (dropAllNS !(full (gamma defs) n), map snd args) of (UN (Basic "MkTy"), [w, y, z]) => do fc' <- reify defs !(evalClosure defs w) - name' <- reify defs !(evalClosure defs y) + name' <- the (Core (WithFC Name)) (reify defs !(evalClosure defs y)) term' <- reify defs !(evalClosure defs z) - pure (Mk [fc', MkDef name'] term') + pure (Mk [fc', AddDef name'] term') _ => cantReify val "ITy" reify defs val = cantReify val "ITy" From 592435b174bb98c11e5f03b86a8c18048c331ddc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andr=C3=A9=20Videla?= Date: Tue, 26 Aug 2025 14:54:25 +0100 Subject: [PATCH 3/8] add basic test for errors --- tests/idris2/basic/binding003/Test.idr | 4 ++++ tests/idris2/basic/binding003/Test2.idr | 12 ++++++++++++ tests/idris2/basic/binding003/Test3.idr | 10 ++++++++++ tests/idris2/basic/binding003/Test4.idr | 4 ++++ tests/idris2/basic/binding003/expected | 8 ++++++++ tests/idris2/basic/binding003/run | 6 ++++++ 6 files changed, 44 insertions(+) create mode 100644 tests/idris2/basic/binding003/Test.idr create mode 100644 tests/idris2/basic/binding003/Test2.idr create mode 100644 tests/idris2/basic/binding003/Test3.idr create mode 100644 tests/idris2/basic/binding003/Test4.idr create mode 100644 tests/idris2/basic/binding003/expected create mode 100755 tests/idris2/basic/binding003/run diff --git a/tests/idris2/basic/binding003/Test.idr b/tests/idris2/basic/binding003/Test.idr new file mode 100644 index 00000000000..e8535b727c5 --- /dev/null +++ b/tests/idris2/basic/binding003/Test.idr @@ -0,0 +1,4 @@ + +autobind +Sigma : (ty : Type) -> (ty -> Type) -> Type + diff --git a/tests/idris2/basic/binding003/Test2.idr b/tests/idris2/basic/binding003/Test2.idr new file mode 100644 index 00000000000..bccc986bc67 --- /dev/null +++ b/tests/idris2/basic/binding003/Test2.idr @@ -0,0 +1,12 @@ +import Data.Fin + + +typebind +record Sigma (ty : Type) (sy : ty -> Type) where + constructor S + p1 : ty + p2 : sy p1 + + +List : Type -> Type +List a = Sigma (n <- Nat) | Fin n -> a diff --git a/tests/idris2/basic/binding003/Test3.idr b/tests/idris2/basic/binding003/Test3.idr new file mode 100644 index 00000000000..12a83bdcf9a --- /dev/null +++ b/tests/idris2/basic/binding003/Test3.idr @@ -0,0 +1,10 @@ + + +autobind +for : List a -> (a -> IO ()) -> IO () + +range : List Nat +range = [1 .. 10] + +main : IO () +main = for (x : range) | printLn x diff --git a/tests/idris2/basic/binding003/Test4.idr b/tests/idris2/basic/binding003/Test4.idr new file mode 100644 index 00000000000..f1a4dcd8f27 --- /dev/null +++ b/tests/idris2/basic/binding003/Test4.idr @@ -0,0 +1,4 @@ + + +typebind +for : List a -> (a -> IO ()) -> IO () diff --git a/tests/idris2/basic/binding003/expected b/tests/idris2/basic/binding003/expected new file mode 100644 index 00000000000..d026d829c8d --- /dev/null +++ b/tests/idris2/basic/binding003/expected @@ -0,0 +1,8 @@ +1/1: Building Test (Test.idr) +SHould warn about declaring typebind instead of autobind +1/1: Building Test2 (Test2.idr) +Shouwl warn about autobind instead of typebind +1/1: Building Test3 (Test3.idr) +should warn about using typebind insteaf of autobind +1/1: Building Test4 (Test4.idr) +should warn about declaring auto instead of typebind diff --git a/tests/idris2/basic/binding003/run b/tests/idris2/basic/binding003/run new file mode 100755 index 00000000000..510e708d59b --- /dev/null +++ b/tests/idris2/basic/binding003/run @@ -0,0 +1,6 @@ +. ../../../testutils.sh + +check Test.idr +check Test2.idr +check Test3.idr +check Test4.idr From a7b404eab43e65e2b67f7cd30f752ed2d2d93530 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andr=C3=A9=20Videla?= Date: Tue, 26 Aug 2025 17:13:18 +0100 Subject: [PATCH 4/8] add basic support for error messages during misuse --- src/Core/Context.idr | 5 ++- src/Core/Core.idr | 12 ++++++- src/Idris/Error.idr | 20 +++++++++-- src/TTImp/Elab/BindingApp.idr | 48 ++++++++++++++++++-------- tests/idris2/basic/binding003/expected | 32 ++++++++++++++--- 5 files changed, 95 insertions(+), 22 deletions(-) diff --git a/src/Core/Context.idr b/src/Core/Context.idr index 32a46b1dd99..d5a150f2cdf 100644 --- a/src/Core/Context.idr +++ b/src/Core/Context.idr @@ -836,6 +836,8 @@ HasNames Error where full gam (OperatorBindingMismatch {print} fc expected actual (Right opName) rhs candidates) = OperatorBindingMismatch {print} fc expected actual <$> (Right <$> full gam opName) <*> pure rhs <*> pure candidates + full gam (BindingApplicationMismatch fc used bind others) + = BindingApplicationMismatch fc used <$> traverse (full gam) bind <*> traverse (full gam) others resolved gam (Fatal err) = Fatal <$> resolved gam err resolved _ (CantConvert fc gam rho s t) @@ -934,7 +936,8 @@ HasNames Error where resolved gam (OperatorBindingMismatch {print} fc expected actual (Right opName) rhs candidates) = OperatorBindingMismatch {print} fc expected actual <$> (Right <$> resolved gam opName) <*> pure rhs <*> pure candidates - + resolved gam (BindingApplicationMismatch fc used bind others) + = BindingApplicationMismatch fc used <$> traverse (resolved gam) bind <*> traverse (resolved gam) others export HasNames Totality where full gam (MkTotality t c) = pure $ MkTotality !(full gam t) !(full gam c) diff --git a/src/Core/Core.idr b/src/Core/Core.idr index 44e52f869a4..effc15d7b18 100644 --- a/src/Core/Core.idr +++ b/src/Core/Core.idr @@ -176,6 +176,12 @@ data Error : Type where FC -> (expectedFixity : FixityDeclarationInfo) -> (use_site : OperatorLHSInfo a) -> -- left: backticked, right: op symbolds (opName : Either Name Name) -> (rhs : a) -> (candidates : List String) -> Error + BindingApplicationMismatch : + FC -> + (bindingUsed : BindingModifier) -> + (bindingCandidates : List Name) -> + (nonBindingCandidates : List Name) -> + Error TTCError : TTCErrorMsg -> Error FileErr : String -> FileError -> Error CantFindPackage : String -> Error @@ -415,6 +421,8 @@ Show Error where show (OperatorBindingMismatch fc UndeclaredFixity actual opName rhs _) = show fc ++ ": Operator " ++ show opName ++ " has no declared fixity" ++ " but used as a " ++ show actual ++ " operator" + show (BindingApplicationMismatch fc used binding notBinding) + = show fc ++ ": Application used \{show used} syntax but no such function exists" export getWarningLoc : Warning -> FC @@ -506,6 +514,7 @@ getErrorLoc (InRHS _ _ err) = getErrorLoc err getErrorLoc (MaybeMisspelling err _) = getErrorLoc err getErrorLoc (WarningAsError warn) = Just (getWarningLoc warn) getErrorLoc (OperatorBindingMismatch loc _ _ _ _ _) = Just loc +getErrorLoc (BindingApplicationMismatch loc _ _ _) = Just loc export killWarningLoc : Warning -> Warning @@ -597,7 +606,8 @@ killErrorLoc (MaybeMisspelling err xs) = MaybeMisspelling (killErrorLoc err) xs killErrorLoc (WarningAsError wrn) = WarningAsError (killWarningLoc wrn) killErrorLoc (OperatorBindingMismatch {print} fc expected actual opName rhs candidates) = OperatorBindingMismatch {print} emptyFC expected actual opName rhs candidates - +killErrorLoc (BindingApplicationMismatch _ a b c) + = BindingApplicationMismatch emptyFC a b c -- Core is a wrapper around IO that is specialised for efficiency. export diff --git a/src/Idris/Error.idr b/src/Idris/Error.idr index 49ae5089c56..01b225b3835 100644 --- a/src/Idris/Error.idr +++ b/src/Idris/Error.idr @@ -627,7 +627,7 @@ perrorRaw (GenericMsgSol fc header solutionHeader solutions) <+> indent 1 (vsep (map (\s => "-" <++> pretty0 s) solutions)) perrorRaw (OperatorBindingMismatch fc {print=p} expected actual opName rhs candidates) = pure $ "Operator" <++> pretty0 !(getFullName (fromEither opName)) <++> "is" - <++> printBindingInfo expected-- .bindingInfo + <++> printBindingInfo expected <++> "operator, but is used as" <++> printBindingModifier actual.getBinder <++> "operator." <+> line <+> !(ploc fc) @@ -702,7 +702,23 @@ perrorRaw (OperatorBindingMismatch fc {print=p} expected actual opName rhs candi printBindingInfo : FixityDeclarationInfo -> Doc IdrisAnn printBindingInfo UndeclaredFixity = "a regular" printBindingInfo (DeclaredFixity x) = printBindingModifier x.bindingInfo - +perrorRaw (BindingApplicationMismatch fc used bind others) + = pure $ errorDesc $ reflow "Using \{show used} syntax but no function in scope is marked \{show used}" + <+> line + <+> !(ploc fc) + <+> line + <+> footer bind others + where + footer : List Name -> List Name -> Doc IdrisAnn + footer [] [] = reflow "There are no functions in scope that could match the current situation" + footer [] (x :: xs) = + reflow "Did you mean any of:" + <++> concatWith (surround (comma <+> space)) (map (code . pretty0) xs) + <+> comma <++> "or" <++> code (pretty0 x) <+> "?" + footer (x :: xs) ns1 = + reflow "Did you mean any of:" + <++> concatWith (surround (comma <+> space)) (map (code . pretty0) xs) + <+> comma <++> "or" <++> code (pretty0 x) <+> "?" perrorRaw (TTCError msg) = pure $ errorDesc (reflow "Error in TTC file" <+> colon <++> byShow msg) diff --git a/src/TTImp/Elab/BindingApp.idr b/src/TTImp/Elab/BindingApp.idr index ea4523fc4dc..f95ced4e78a 100644 --- a/src/TTImp/Elab/BindingApp.idr +++ b/src/TTImp/Elab/BindingApp.idr @@ -9,6 +9,8 @@ import Core.Metadata import Core.Name import Core.Normalise +import Data.List + import TTImp.Elab.Check import TTImp.Elab.App import TTImp.TTImp @@ -16,26 +18,44 @@ import TTImp.TTImp import Idris.REPL.Opts import Idris.Syntax -keepBinding : BindingModifier -> List GlobalDef -> List GlobalDef -keepBinding mode = filter (\x => x.bindingMode == mode) -parameters (originalName : WithFC Name) {auto c : Ref Ctxt Defs} - checkUnique : List GlobalDef -> Core GlobalDef - checkUnique [ def ] = pure def - checkUnique [] = throw $ UndefinedName originalName.fc originalName.val - checkUnique defs = throw $ AmbiguousName originalName.fc (map fullname defs) + +record BindingModes (a : Type) where + constructor MkBindingModes + everythingMatches : List a + bindingDoesNotMatch : List a + notBinding : List a + +keepBinding : BindingModifier -> List GlobalDef -> BindingModes GlobalDef +keepBinding mode = foldl sortBinding (MkBindingModes [] [] []) + where + sortBinding : BindingModes GlobalDef -> GlobalDef -> BindingModes GlobalDef + sortBinding modes def = if def.bindingMode == mode + then {everythingMatches $= (def ::)} modes + else if def.bindingMode == NotBinding + then {notBinding $= (def ::)} modes + else {bindingDoesNotMatch $= (def ::)} modes + + +parameters (originalName : WithFC Name) (mode : BindingModifier) {auto c : Ref Ctxt Defs} + checkUnique : BindingModes GlobalDef -> Core GlobalDef + checkUnique (MkBindingModes [ def ] _ _ ) = pure def + checkUnique (MkBindingModes [] may others) = do + coreLift $ putStrLn (show $ map fullname others) + throw $ BindingApplicationMismatch originalName.fc mode (map fullname may) (map fullname others) + checkUnique (MkBindingModes defs _ _) = throw $ AmbiguousName originalName.fc (map fullname defs) typecheckCandidates : List GlobalDef -> Core (List GlobalDef) - typecheckCandidates xs = pure xs -- todo + typecheckCandidates xs = pure xs -- todo: emit errors when the type doesn't match - checkBinding : (mode : BindingModifier) -> (candidates : List GlobalDef) -> Core GlobalDef - checkBinding mode candidates = do + checkBinding : (candidates : List GlobalDef) -> Core GlobalDef + checkBinding candidates = do log "elab.bindApp" 10 $ "Potential candidates for binding identifer : \{show (map fullname candidates)}" log "elab.bindApp" 10 $ "Checking if candidates have binding \{show mode}" - let bindingCandidates = keepBinding mode candidates - log "elab.bindApp" 10 $ "Final list of binding identifers : \{show (map fullname bindingCandidates)}" - wellTypedCandidates <- typecheckCandidates bindingCandidates - checkUnique bindingCandidates + let candidates = keepBinding mode candidates + log "elab.bindApp" 10 $ "Final list of binding identifers : \{show (map fullname candidates.everythingMatches)}" + -- wellTypedCandidates <- typecheckCandidates bindingCandidates + checkUnique candidates typeForBinder : BindingInfo RawImp -> FC -> RawImp typeForBinder (BindType name type) = const type diff --git a/tests/idris2/basic/binding003/expected b/tests/idris2/basic/binding003/expected index d026d829c8d..1cbe22e76fc 100644 --- a/tests/idris2/basic/binding003/expected +++ b/tests/idris2/basic/binding003/expected @@ -1,8 +1,32 @@ 1/1: Building Test (Test.idr) -SHould warn about declaring typebind instead of autobind +Should warn about declaring typebind instead of autobind 1/1: Building Test2 (Test2.idr) -Shouwl warn about autobind instead of typebind +[] +Error: While processing right hand side of List. Using autobind syntax but no function in scope is marked autobind + +Test2:12:10--12:15 + 08 | p2 : sy p1 + 09 | + 10 | + 11 | List : Type -> Type + 12 | List a = Sigma (n <- Nat) | Fin n -> a + ^^^^^ + +Did you mean to write: `Sigma (x : range)` using `Sigma` from module `Test3` on line 6? 1/1: Building Test3 (Test3.idr) -should warn about using typebind insteaf of autobind +[Prelude.Interfaces.for] +Error: While processing right hand side of main. Using typebind syntax but no function in scope is marked typebind + +Test3:10:8--10:11 + 06 | range : List Nat + 07 | range = [1 .. 10] + 08 | + 09 | main : IO () + 10 | main = for (x : range) | printLn x + ^^^ + +Possible fixes : +- Use autobind syntax `for (x <- range)` using `Test3.for` +- Use regular syntax `for range` using `Prelude.for` 1/1: Building Test4 (Test4.idr) -should warn about declaring auto instead of typebind +Should warn about declaring autobind instead of typebind From 1003b836e8c11c5bb8ec1f24976b636bfe3bf70a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andr=C3=A9=20Videla?= Date: Sun, 31 Aug 2025 20:39:47 +0100 Subject: [PATCH 5/8] fix binding symbol --- src/TTImp/TTImp.idr | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/TTImp/TTImp.idr b/src/TTImp/TTImp.idr index 7ccd12f92e6..eb65422d099 100644 --- a/src/TTImp/TTImp.idr +++ b/src/TTImp/TTImp.idr @@ -199,9 +199,9 @@ mutual (BindType name type) => "\{show nm.val} (\{show name} : \{show type}) | \{show scope.val}" (BindExpr name expr) => - "\{show nm.val} (\{show name} := \{show expr}) | \{show scope.val}" + "\{show nm.val} (\{show name} <- \{show expr}) | \{show scope.val}" (BindExplicitType name type expr) => - "\{show nm.val} (\{show name} : \{show type} := \{show expr}) | \{show scope.val}" + "\{show nm.val} (\{show name} : \{show type} <- \{show expr}) | \{show scope.val}" show (ISearch fc d) = "%search" show (IAlternative fc ty alts) From f2356f47187b5e225732ddb52c2dc9cc880f2310 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andr=C3=A9=20Videla?= Date: Mon, 1 Sep 2025 00:50:05 +0100 Subject: [PATCH 6/8] move documentation out of PTypeDeclData --- src/Core/TT.idr | 8 +++---- src/Idris/Desugar.idr | 4 ++-- src/Idris/Parser.idr | 37 +++++++++++++++++++-------------- src/Idris/Resugar.idr | 2 +- src/Idris/Syntax.idr | 3 +-- src/Idris/Syntax/Traversals.idr | 4 ++-- src/TTImp/Elab/BindingApp.idr | 9 +++++--- 7 files changed, 37 insertions(+), 30 deletions(-) diff --git a/src/Core/TT.idr b/src/Core/TT.idr index 0a29d10f9c0..14b80f2d2a4 100644 --- a/src/Core/TT.idr +++ b/src/Core/TT.idr @@ -199,15 +199,15 @@ data FixityDeclarationInfo = UndeclaredFixity | DeclaredFixity FixityInfo -- Binding information for binding application and binding operators -- A binder can either -- - bind types `(t : a)` --- - bind expressions with an inferred type such that `(x := v)` --- - bind an expression with an explicit type annotation `(x : a := v)` +-- - bind expressions with an inferred type such that `(x <- v)` +-- - bind an expression with an explicit type annotation `(x : a <- v)` public export data BindingInfo : (tm : Type) -> Type where -- (name : type) BindType : (name : tm) -> (type : tm) -> BindingInfo tm - -- (name := expr) + -- (name <- expr) BindExpr : (name : tm) -> (expr : tm) -> BindingInfo tm - -- (name : type := expr) + -- (name : type <- expr) BindExplicitType : (name : tm) -> (type, expr : tm) -> BindingInfo tm diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr index 530696eef38..21665d29b6a 100644 --- a/src/Idris/Desugar.idr +++ b/src/Idris/Desugar.idr @@ -906,9 +906,9 @@ mutual {auto m : Ref MD Metadata} -> {auto o : Ref ROpts REPLOpts} -> List Name -> AddMetadata Bind' PTypeDecl -> Core (List ImpTy) - desugarType ps pty@(MkWithData _ $ MkPTy names d ty) + desugarType ps pty@(MkWithData _ $ MkPTy names ty) = flip Core.traverse (forget names) $ \(doc, n) : (String, WithFC Name) => - do addDocString n.val (d ++ doc) + do addDocString n.val (pty.doc ++ doc) syn <- get Syn pure $ Mk [pty.fc, NotBinding :+ n] !(bindTypeNames pty.fc (usingImpl syn) ps !(desugar AnyExpr ps ty)) diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index 3407a278d79..544659f79f6 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -1225,17 +1225,23 @@ visibility fname = parseDefault (visOption fname) exportVisibility : OriginDesc -> EmptyRule (WithDefault Visibility Export) exportVisibility fname = parseDefault (visOption fname) -tyDecls : Rule Name -> String -> OriginDesc -> IndentInfo -> Rule PTypeDecl -tyDecls declName predoc fname indents - = do bs <- bounds $ do - docns <- sepBy1 (decoratedSymbol fname ",") - [| (optDocumentation fname, fcBounds declName) |] - b <- bounds $ decoratedSymbol fname ":" - mustWorkBecause b.bounds "Expected a type declaration" $ do - ty <- the (Rule PTerm) (typeExpr pdef fname indents) - pure $ MkPTy docns predoc ty +tyDeclsData : Rule Name -> OriginDesc -> IndentInfo -> Rule (PTypeDeclData' Name) +tyDeclsData declName fname indents + = do + docns <- sepBy1 (decoratedSymbol fname ",") + [| (optDocumentation fname, fcBounds declName) |] + b <- bounds $ decoratedSymbol fname ":" + ty <- mustWorkBecause b.bounds "Expected a type declaration" $ + the (Rule PTerm) (typeExpr pdef fname indents) + pure $ MkPTy docns ty + +tyDecls : Rule Name -> OriginDesc -> IndentInfo -> Rule PTypeDecl +tyDecls declName fname indents + = do doc <- optDocumentation fname + decl <- fcBounds (tyDeclsData declName fname indents) atEnd indents - pure $ bs.withFC + pure (doc :+ decl) + withFlags : OriginDesc -> EmptyRule (List WithFlag) withFlags fname @@ -1353,10 +1359,10 @@ simpleCon fname ret indents let conType = the (Maybe PTerm) (mkDataConType ret (concat (map distribData params))) fromMaybe (fatalError "Named arguments not allowed in ADT constructors") - (pure . MkPTy (singleton ("", cname)) cdoc <$> conType) + (pure . MkPTy (singleton ("", cname)) <$> conType) ) atEnd indents - pure b.withFC + pure ("" :+ b.withFC) simpleData : OriginDesc -> WithBounds t -> FCBind Name -> IndentInfo -> Rule PDataDecl @@ -1401,7 +1407,7 @@ dataBody fname mincol start n indents ty <|> do b <- bounds (do (mustWork $ decoratedKeyword fname "where") opts <- dataOpts fname bind <- operatorBindingKeyword - cs <- blockAfter mincol (tyDecls (mustWork $ decoratedDataConstructorName fname) "" fname) + cs <- blockAfter mincol (tyDecls (mustWork $ decoratedDataConstructorName fname) fname) pure (opts, map (bind :+) cs)) (opts, cs) <- pure (the (Pair ? ?) b.val) pure (MkPData (boundToFC fname (mergeBounds start b)) n ty opts cs) @@ -1827,10 +1833,9 @@ parameters {auto fname : OriginDesc} {auto indents : IndentInfo} visOpts <- many (visOpt fname) vis <- getVisibility Nothing visOpts let opts = mapMaybe getRight visOpts - bind <- operatorBindingKeyword + bind <- operatorBindingKeyword rig <- multiplicity fname - cls <- tyDecls (decorate fname Function name) - doc fname indents + cls <- tyDecls (decorate fname Function name) fname indents pure $ MkPClaim rig vis opts (bind :+ cls) diff --git a/src/Idris/Resugar.idr b/src/Idris/Resugar.idr index 8d18d808b88..dd7f81e6a59 100644 --- a/src/Idris/Resugar.idr +++ b/src/Idris/Resugar.idr @@ -479,7 +479,7 @@ mutual {auto s : Ref Syn SyntaxInfo} -> ImpTy' KindedName -> Core (AddMetadata Bind' (PTypeDecl' KindedName)) toPTypeDecl impTy - = pure $ Mk [impTy.tyName.bind, impTy.fc] (MkPTy (pure ("", drop $ impTy.tyName)) "" !(toPTerm startPrec impTy.val)) + = pure $ Mk [impTy.tyName.bind, "", impTy.fc] (MkPTy (pure ("", drop $ impTy.tyName)) !(toPTerm startPrec impTy.val)) toPData : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr index 9a48d7a3a14..0a76f8eb80c 100644 --- a/src/Idris/Syntax.idr +++ b/src/Idris/Syntax.idr @@ -365,12 +365,11 @@ mutual -- List of names and their associated documentation -- If no documentation is provided the first projection is `""` names : List1 (String, WithFC Name) - doc: String type : PTerm' nm -- probably need `WithFC` here to fix #3408 public export PTypeDecl' : Type -> Type - PTypeDecl' nm = WithFC (PTypeDeclData' nm) + PTypeDecl' nm = WithData [Doc', FC'] (PTypeDeclData' nm) export (.nameList) : PTypeDecl' nm -> List Name diff --git a/src/Idris/Syntax/Traversals.idr b/src/Idris/Syntax/Traversals.idr index 59c5cbe6c82..914e4f4e978 100644 --- a/src/Idris/Syntax/Traversals.idr +++ b/src/Idris/Syntax/Traversals.idr @@ -316,7 +316,7 @@ mapPTermM f = goPTerm where goPDecl p@(PBuiltin {}) = pure p goPTypeDecl : PTypeDeclData' nm -> Core (PTypeDeclData' nm) - goPTypeDecl (MkPTy n d t) = MkPTy n d <$> goPTerm t + goPTypeDecl (MkPTy n t) = MkPTy n <$> goPTerm t goPDataDecl : PDataDecl' nm -> Core (PDataDecl' nm) goPDataDecl (MkPData fc n t opts tdecls) = @@ -591,7 +591,7 @@ mapPTerm f = goPTerm where = MkBasicMultiBinder rig names (goPTerm type) goPTypeDecl : PTypeDeclData' nm -> PTypeDeclData' nm - goPTypeDecl (MkPTy n d t) = MkPTy n d $ goPTerm t + goPTypeDecl (MkPTy n t) = MkPTy n $ goPTerm t goPDataDecl : PDataDecl' nm -> PDataDecl' nm goPDataDecl (MkPData fc n t opts tdecls) diff --git a/src/TTImp/Elab/BindingApp.idr b/src/TTImp/Elab/BindingApp.idr index f95ced4e78a..e21800a916e 100644 --- a/src/TTImp/Elab/BindingApp.idr +++ b/src/TTImp/Elab/BindingApp.idr @@ -22,8 +22,11 @@ import Idris.Syntax record BindingModes (a : Type) where constructor MkBindingModes + -- Definition where the binding matches everythingMatches : List a + -- Definitions that are binding but not the correct type of binding bindingDoesNotMatch : List a + -- Definitions that are binding at all notBinding : List a keepBinding : BindingModifier -> List GlobalDef -> BindingModes GlobalDef @@ -46,7 +49,7 @@ parameters (originalName : WithFC Name) (mode : BindingModifier) {auto c : Ref C checkUnique (MkBindingModes defs _ _) = throw $ AmbiguousName originalName.fc (map fullname defs) typecheckCandidates : List GlobalDef -> Core (List GlobalDef) - typecheckCandidates xs = pure xs -- todo: emit errors when the type doesn't match + typecheckCandidates xs = pure xs -- todo: filter definitions with the wrong type checkBinding : (candidates : List GlobalDef) -> Core GlobalDef checkBinding candidates = do @@ -54,8 +57,8 @@ parameters (originalName : WithFC Name) (mode : BindingModifier) {auto c : Ref C log "elab.bindApp" 10 $ "Checking if candidates have binding \{show mode}" let candidates = keepBinding mode candidates log "elab.bindApp" 10 $ "Final list of binding identifers : \{show (map fullname candidates.everythingMatches)}" - -- wellTypedCandidates <- typecheckCandidates bindingCandidates - checkUnique candidates + wellTypedCandidates <- typecheckCandidates candidates.everythingMatches + checkUnique ({everythingMatches := wellTypedCandidates} candidates) typeForBinder : BindingInfo RawImp -> FC -> RawImp typeForBinder (BindType name type) = const type From 3e060318b33df4d546e3552e0df114704bfa1747 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andr=C3=A9=20Videla?= Date: Mon, 1 Sep 2025 00:59:08 +0100 Subject: [PATCH 7/8] attach documentation to field name --- src/Idris/Desugar.idr | 6 +++--- src/Idris/Parser.idr | 6 +++--- src/Idris/Resugar.idr | 2 +- src/Idris/Syntax.idr | 4 ++-- 4 files changed, 9 insertions(+), 9 deletions(-) diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr index 21665d29b6a..756f29f2bfd 100644 --- a/src/Idris/Desugar.idr +++ b/src/Idris/Desugar.idr @@ -907,10 +907,10 @@ mutual {auto o : Ref ROpts REPLOpts} -> List Name -> AddMetadata Bind' PTypeDecl -> Core (List ImpTy) desugarType ps pty@(MkWithData _ $ MkPTy names ty) - = flip Core.traverse (forget names) $ \(doc, n) : (String, WithFC Name) => - do addDocString n.val (pty.doc ++ doc) + = flip Core.traverse (forget names) $ \n : (WithDoc (WithFC Name)) => + do addDocString n.val (pty.doc ++ n.doc) syn <- get Syn - pure $ Mk [pty.fc, NotBinding :+ n] !(bindTypeNames pty.fc (usingImpl syn) + pure $ Mk [pty.fc, NotBinding :+ n.drop] !(bindTypeNames pty.fc (usingImpl syn) ps !(desugar AnyExpr ps ty)) -- Attempt to get the function name from a function pattern. For example, diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index 544659f79f6..6900a1d9953 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -1229,7 +1229,7 @@ tyDeclsData : Rule Name -> OriginDesc -> IndentInfo -> Rule (PTypeDeclData' Name tyDeclsData declName fname indents = do docns <- sepBy1 (decoratedSymbol fname ",") - [| (optDocumentation fname, fcBounds declName) |] + [| (optDocumentation fname :+ fcBounds declName) |] b <- bounds $ decoratedSymbol fname ":" ty <- mustWorkBecause b.bounds "Expected a type declaration" $ the (Rule PTerm) (typeExpr pdef fname indents) @@ -1355,11 +1355,11 @@ simpleCon fname ret indents = do b <- bounds (do cdoc <- optDocumentation fname cname <- fcBounds $ decoratedDataConstructorName fname params <- the (EmptyRule $ List $ WithFC $ List ArgType) - $ many (fcBounds $ argExpr plhs fname indents) + $ many (fcBounds $ argExpr plhs fname indents) let conType = the (Maybe PTerm) (mkDataConType ret (concat (map distribData params))) fromMaybe (fatalError "Named arguments not allowed in ADT constructors") - (pure . MkPTy (singleton ("", cname)) <$> conType) + (pure . MkPTy (singleton ("" :+ cname)) <$> conType) ) atEnd indents pure ("" :+ b.withFC) diff --git a/src/Idris/Resugar.idr b/src/Idris/Resugar.idr index dd7f81e6a59..5aa4c123c09 100644 --- a/src/Idris/Resugar.idr +++ b/src/Idris/Resugar.idr @@ -479,7 +479,7 @@ mutual {auto s : Ref Syn SyntaxInfo} -> ImpTy' KindedName -> Core (AddMetadata Bind' (PTypeDecl' KindedName)) toPTypeDecl impTy - = pure $ Mk [impTy.tyName.bind, "", impTy.fc] (MkPTy (pure ("", drop $ impTy.tyName)) !(toPTerm startPrec impTy.val)) + = pure $ Mk [impTy.tyName.bind, "", impTy.fc] (MkPTy (pure ("" :+ drop impTy.tyName)) !(toPTerm startPrec impTy.val)) toPData : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr index 0a76f8eb80c..f98dab91910 100644 --- a/src/Idris/Syntax.idr +++ b/src/Idris/Syntax.idr @@ -364,7 +364,7 @@ mutual constructor MkPTy -- List of names and their associated documentation -- If no documentation is provided the first projection is `""` - names : List1 (String, WithFC Name) + names : List1 (WithDoc $ WithFC Name) type : PTerm' nm -- probably need `WithFC` here to fix #3408 public export @@ -373,7 +373,7 @@ mutual export (.nameList) : PTypeDecl' nm -> List Name - (.nameList) = forget . map (val . snd) . names . val + (.nameList) = forget . map val . names . val public export PDataDecl : Type From 48de3f4289ac0a5713cd1057a25e1ac081b4dbfc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andr=C3=A9=20Videla?= Date: Mon, 1 Sep 2025 01:06:53 +0100 Subject: [PATCH 8/8] change how we parse record fields --- src/Idris/Parser.idr | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index 6900a1d9953..945e892c68b 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -1235,12 +1235,13 @@ tyDeclsData declName fname indents the (Rule PTerm) (typeExpr pdef fname indents) pure $ MkPTy docns ty -tyDecls : Rule Name -> OriginDesc -> IndentInfo -> Rule PTypeDecl +tyDecls : Rule Name -> OriginDesc -> IndentInfo -> Rule (AddMetadata Bind' PTypeDecl) tyDecls declName fname indents = do doc <- optDocumentation fname + bind <- operatorBindingKeyword decl <- fcBounds (tyDeclsData declName fname indents) atEnd indents - pure (doc :+ decl) + pure (bind :+ doc :+ decl) withFlags : OriginDesc -> EmptyRule (List WithFlag) @@ -1406,9 +1407,8 @@ dataBody fname mincol start n indents ty pure (MkPLater (boundToFC fname start) n ty) <|> do b <- bounds (do (mustWork $ decoratedKeyword fname "where") opts <- dataOpts fname - bind <- operatorBindingKeyword cs <- blockAfter mincol (tyDecls (mustWork $ decoratedDataConstructorName fname) fname) - pure (opts, map (bind :+) cs)) + pure (opts, cs)) (opts, cs) <- pure (the (Pair ? ?) b.val) pure (MkPData (boundToFC fname (mergeBounds start b)) n ty opts cs) @@ -1833,10 +1833,9 @@ parameters {auto fname : OriginDesc} {auto indents : IndentInfo} visOpts <- many (visOpt fname) vis <- getVisibility Nothing visOpts let opts = mapMaybe getRight visOpts - bind <- operatorBindingKeyword rig <- multiplicity fname cls <- tyDecls (decorate fname Function name) fname indents - pure $ MkPClaim rig vis opts (bind :+ cls) + pure $ MkPClaim rig vis opts cls -- A Single binder with multiple names