[ upstream ] Support Name in IBindVar

spcfox · spcfox · commit aa33af1c292a · 2025-03-25T22:11:44.000+03:00
diff --git a/src/Derive/Abs.idr b/src/Derive/Abs.idr
@@ -28,7 +28,7 @@ absImplDef abs impl = def impl [patClause (var impl) (appNames "MkAbs" [abs])]
 
 parameters (nms : List Name)
   abs : BoundArg 1 Explicit -> TTImp
-  abs (BA _ [x] _)  = `(abs ~(varStr x))
+  abs (BA _ [x] _)  = `(abs ~(var x))
 
   export
   absDef : Name -> Con n vs -> Decl
diff --git a/src/Derive/Eq.idr b/src/Derive/Eq.idr
@@ -127,7 +127,7 @@ rhs (sx :< x) = foldr (\e,acc => `(~(e) && ~(acc))) x sx
 
 parameters (nms : List Name)
   arg : BoundArg 2 Regular -> TTImp
-  arg (BA g [x,y] _) = assertIfRec nms g.type `(~(varStr x) == ~(varStr y))
+  arg (BA g [x,y] _) = assertIfRec nms g.type `(~(var x) == ~(var y))
 
   ||| Generates pattern match clauses for the constructors of
   ||| the given data type. `fun` is the name of the function we implement.
diff --git a/src/Derive/Fractional.idr b/src/Derive/Fractional.idr
@@ -35,10 +35,10 @@ fractionalImplDef d r i =
   def i [patClause (var i) (appNames "MkFractional" [d, r])]
 
 div : BoundArg 2 Explicit -> TTImp
-div (BA arg [x,y] _)  = `(~(varStr x) / ~(varStr y))
+div (BA arg [x,y] _)  = `(~(var x) / ~(var y))
 
 recip : BoundArg 1 Explicit -> TTImp
-recip (BA arg [x] _)  = `(recip ~(varStr x))
+recip (BA arg [x] _)  = `(recip ~(var x))
 
 export
 divDef : Name -> Con n vs -> Decl
diff --git a/src/Derive/Integral.idr b/src/Derive/Integral.idr
@@ -29,10 +29,10 @@ intImplDef d m impl =
 
 parameters (nms : List Name)
   div : BoundArg 2 Explicit -> TTImp
-  div (BA arg [x,y] _)  = `(div ~(varStr x) ~(varStr y))
+  div (BA arg [x,y] _)  = `(div ~(var x) ~(var y))
 
   mod : BoundArg 2 Explicit -> TTImp
-  mod (BA arg [x,y] _)  = `(mod ~(varStr x) ~(varStr y))
+  mod (BA arg [x,y] _)  = `(mod ~(var x) ~(var y))
 
   export
   divDef : Name -> Con n vs -> Decl
diff --git a/src/Derive/Neg.idr b/src/Derive/Neg.idr
@@ -35,10 +35,10 @@ negImplDef neg min impl =
   def impl [patClause (var impl) (appNames "MkNeg" [neg, min])]
 
 minus : BoundArg 2 Explicit -> TTImp
-minus (BA arg [x,y] _)  = `(~(varStr x) - ~(varStr y))
+minus (BA arg [x,y] _)  = `(~(var x) - ~(var y))
 
 neg : BoundArg 1 Explicit -> TTImp
-neg (BA arg [x] _)  = `(negate ~(varStr x))
+neg (BA arg [x] _)  = `(negate ~(var x))
 
 export
 minusDef : Name -> Con n vs -> Decl
diff --git a/src/Derive/Num.idr b/src/Derive/Num.idr
@@ -41,10 +41,10 @@ numImplDef p m fi impl =
   def impl [patClause (var impl) (appNames "MkNum" [p,m,fi])]
 
 plus : BoundArg 2 Explicit -> TTImp
-plus (BA arg [x,y] _)  = `(~(varStr x) + ~(varStr y))
+plus (BA arg [x,y] _)  = `(~(var x) + ~(var y))
 
 mult : BoundArg 2 Explicit -> TTImp
-mult (BA arg [x,y] _)  = `(~(varStr x) * ~(varStr y))
+mult (BA arg [x,y] _)  = `(~(var x) * ~(var y))
 
 fromInt : BoundArg 0 Explicit -> TTImp
 fromInt _ = `(fromInteger n)
diff --git a/src/Derive/Ord.idr b/src/Derive/Ord.idr
@@ -55,7 +55,7 @@ catchAll ci fun ti =
 
 parameters (nms : List Name)
   arg : BoundArg 2 Regular -> TTImp
-  arg (BA g [x,y] _) = assertIfRec nms g.type `(compare ~(varStr x) ~(varStr y))
+  arg (BA g [x,y] _) = assertIfRec nms g.type `(compare ~(var x) ~(var y))
 
   ||| Generates pattern match clauses for the constructors of
   ||| the given data type. `fun` is the name of the function we implement.
diff --git a/src/Derive/Pretty.idr b/src/Derive/Pretty.idr
@@ -53,7 +53,7 @@ parameters (nms : List Name)
   -- pretty printing a single, explicit, unnamed constructor argument
   arg : BoundArg 1 Explicit -> TTImp
   arg (BA (MkArg M0 _ _ _) _   _) = `(pretty US)
-  arg (BA (MkArg _  _ _ t) [x] _) = assertIfRec nms t `(prettyArg ~(varStr x))
+  arg (BA (MkArg _  _ _ t) [x] _) = assertIfRec nms t `(prettyArg ~(var x))
 
   -- prettying a constructor plus its arguments
   rhs : Name -> SnocList TTImp -> TTImp
@@ -65,7 +65,7 @@ parameters (nms : List Name)
     let nm := (argName a).namePrim
      in case a.count of
        M0 => `(prettyField ~(nm) US)
-       _  => assertIfRec nms a.type `(prettyField ~(nm) ~(varStr x))
+       _  => assertIfRec nms a.type `(prettyField ~(nm) ~(var x))
 
   -- prettying a constructor plus its named arguments
   nrhs : Name -> SnocList TTImp -> TTImp
diff --git a/src/Derive/Semigroup.idr b/src/Derive/Semigroup.idr
@@ -33,7 +33,7 @@ semigroupImplDef f i =
   def i [patClause (var i) (var "MkSemigroup" `app` var f)]
 
 app : BoundArg 2 Explicit -> TTImp
-app (BA _ [x,y] _) = `(~(varStr x) <+> ~(varStr y))
+app (BA _ [x,y] _) = `(~(var x) <+> ~(var y))
 
 appClause : Name -> Con n vs -> Clause
 appClause f = mapArgs2 explicit (\x,y => `(~(var f) ~(x) ~(y))) app
diff --git a/src/Derive/Show.idr b/src/Derive/Show.idr
@@ -72,7 +72,7 @@ parameters (nms : List Name)
   -- showing a single, explicit, unnamed constructor argument
   arg : BoundArg 1 Explicit -> TTImp
   arg (BA (MkArg M0 _ _ _) _   _) = primVal (Str " _")
-  arg (BA (MkArg _  _ _ t) [x] _) = assertIfRec nms t `(showArg ~(varStr x))
+  arg (BA (MkArg _  _ _ t) [x] _) = assertIfRec nms t `(showArg ~(var x))
 
   -- showing a constructor plus its arguments
   rhs : Name -> SnocList TTImp -> TTImp
@@ -86,7 +86,7 @@ parameters (nms : List Name)
      in case a.count of
        M0 => `(MkPair ~(nm) "_")
        _  =>
-         let shown := assertIfRec nms a.type `(show ~(varStr x))
+         let shown := assertIfRec nms a.type `(show ~(var x))
           in `(MkPair ~(nm) ~(shown))
 
   -- showing a constructor plus its named arguments
diff --git a/src/Doc/Generic1.md b/src/Doc/Generic1.md
@@ -233,13 +233,13 @@ name and generated list of fresh argument names in a tuple:
 ||| to be used in pattern match declarations
 public export
 ConNames : Type
-ConNames = (Name, List String, List TTImp)
+ConNames = (Name, List Name, List TTImp)
 
 private
 conNames : (c : Con n vs) -> ConNames
 conNames c =
   let ns   := toList $ freshNames "x" c.arty
-      vars := map varStr ns
+      vars := map var ns
    in (c.name, ns, vars)
 
 export
@@ -259,13 +259,7 @@ toClauses cs =
   -- determine on its own that the above list of clauses is covering.
   -- we therefore append an explicit `impossible` clause.
   [impossibleClause $ mkSOP1 (length cs) implicitTrue]
-```
-
-A quick note about function `nameStr`: Idris does not accept
-the machine-generated names of unnamed arguments in pattern matches.
-The function `nameStr` converts such names to similar user-defined names.
 
-```idris
 private
 genericDecl : TypeInfo -> List Decl
 genericDecl ti =
diff --git a/src/Doc/Generic3.md b/src/Doc/Generic3.md
@@ -24,7 +24,7 @@ export
 paramConNames : ParamCon n -> ConNames
 paramConNames c =
   let ns   := toList $ freshNames "x" (count isExplicit c.args)
-      vars := map varStr ns
+      vars := map var ns
    in (c.name, ns, vars)
 
 export
diff --git a/src/Doc/Generic4.md b/src/Doc/Generic4.md
@@ -95,7 +95,7 @@ private
 conNames : ParamCon n -> ConNames
 conNames c =
   let ns   := toList $ freshNames "x" (count isExplicit c.args)
-      vars := map varStr ns
+      vars := map var ns
    in (c.name, ns, vars)
 
 export
diff --git a/src/Doc/Generic7.md b/src/Doc/Generic7.md
@@ -72,7 +72,7 @@ do using elaborator reflection:
 ```idris
 private
 ConNames : Type
-ConNames = (Name, List String, List TTImp)
+ConNames = (Name, List Name, List TTImp)
 
 export
 mkGeneric : Name
@@ -126,7 +126,7 @@ zipWithIndex as = run 0 as
 conNames : ParamCon n -> ConNames
 conNames c =
   let ns   := toList $ freshNames "x" (count isExplicit c.args)
-      vars := map varStr ns
+      vars := map var ns
    in (c.name, ns, vars)
 
 ||| Derives a `Generic` implementation for the given data type
diff --git a/src/Language/Reflection/Derive.idr b/src/Language/Reflection/Derive.idr
@@ -66,7 +66,7 @@ public export
 record BoundArg (n : Nat) (p : Arg -> Type) where
   constructor BA
   arg  : Arg
-  vars : Vect n String
+  vars : Vect n Name
   prf  : p arg
 
 public export
@@ -83,13 +83,13 @@ boundArgs :
      {0 p : Arg -> Type}
   -> (f : (a : Arg) -> Maybe (p a))
   -> Vect n Arg
-  -> Vect k (Vect n String)
+  -> Vect k (Vect n Name)
   -> SnocList (BoundArg k p)
 boundArgs f = go Lin
   where
     go :  SnocList (BoundArg k p)
        -> Vect m Arg
-       -> Vect k (Vect m String)
+       -> Vect k (Vect m Name)
        -> SnocList (BoundArg k p)
     go sx (x :: xs) ns =
       let (y, ys) := split ns
diff --git a/src/Language/Reflection/Syntax.idr b/src/Language/Reflection/Syntax.idr
@@ -139,14 +139,14 @@ varStr = var . fromString
 |||
 ||| This is an alias for `IBindVar EmptyFC`.
 public export %inline
-bindVar : String -> TTImp
+bindVar : Name -> TTImp
 bindVar = IBindVar EmptyFC
 
 ||| Bind a named value to a variable. This uses `nameStr` for
 ||| the variable's name.
 public export %inline
 (.bindVar) : Named a => a -> TTImp
-x.bindVar = bindVar x.nameStr
+x.bindVar = bindVar x.getName
 
 ||| Implicit value bound if unsolved
 |||
@@ -248,7 +248,7 @@ appNames fun = appAll fun . map var
 ||| Example: bindAll "MkPair" ["a","b"]
 |||          is the same as `(MkPair a b)
 public export %inline
-bindAll : (fun : Name) -> (args : List String) -> TTImp
+bindAll : (fun : Name) -> (args : List Name) -> TTImp
 bindAll fun = appAll fun . map bindVar
 
 ||| Alias for `IBindHere EmptyFC`
diff --git a/src/Language/Reflection/Types.idr b/src/Language/Reflection/Types.idr
@@ -28,13 +28,13 @@ Res = Either String
 ||| names. This function provides a pure way to do so without having
 ||| to run this in the `Elab` monad.
 export
-freshNames : String -> (n : Nat) -> Vect n String
+freshNames : String -> (n : Nat) -> Vect n Name
 freshNames s = go 0
 
   where
-    go : Nat -> (k : Nat) -> Vect k String
+    go : Nat -> (k : Nat) -> Vect k Name
     go m 0     = []
-    go m (S k) = (s ++ show m) :: go (S m) k
+    go m (S k) = (UN $ Basic $ s ++ show m) :: go (S m) k
 
 public export
 implicits : Foldable t => t Name -> List Arg
@@ -195,11 +195,11 @@ isConstant c = all isErased c.args
 ||| This is useful for implementing functions which pattern match on a
 ||| data constructor.
 export
-bindCon : (c : Con n vs) -> Vect c.arty String -> TTImp
+bindCon : (c : Con n vs) -> Vect c.arty Name -> TTImp
 bindCon c ns = go c.nameVar (map piInfo c.args) ns
 
   where
-    go : TTImp -> Vect k (PiInfo TTImp) -> Vect k String -> TTImp
+    go : TTImp -> Vect k (PiInfo TTImp) -> Vect k Name -> TTImp
     go t []                  []        = t
     go t (ExplicitArg :: xs) (n :: ns) = go (t `app` bindVar n) xs ns
     go t (_           :: xs) (n :: ns) = go t xs ns
