[ minor ] more magic for name generation

src/Algebra/ZeroOneOmega.idr

@@ -8,6 +8,8 @@ import Algebra.Preorder
 export
 data ZeroOneOmega = Rig0 | Rig1 | RigW
 
+%name ZeroOneOmega rig
+
 export
 Preorder ZeroOneOmega where
   Rig0 <=    _ = True

src/Core/Context/Context.idr

@@ -35,6 +35,7 @@ record PMDefInfo where
                  -- typically for inlinable metavariable solutions
   externalDecl : Bool -- declared in another module, which may affect how it
                       -- is compiled
+%name PMDefInfo pminfo
 
 export
 defaultPI : PMDefInfo
@@ -170,6 +171,7 @@ record Constructor where
   name : Name
   arity : Nat
   type : ClosedTerm
+%name Constructor cons
 
 public export
 data DataDef : Type where
@@ -181,6 +183,7 @@ data Clause : Type where
      MkClause : {vars : _} ->
                 (env : Env Term vars) ->
                 (lhs : Term vars) -> (rhs : Term vars) -> Clause
+%name Clause cl
 
 export
 covering
@@ -192,6 +195,8 @@ public export
 data NoMangleDirective : Type where
     CommonName : String -> NoMangleDirective
     BackendNames : List (String, String) -> NoMangleDirective
+%name NoMangleDirective dir
+
 
 public export
 data DefFlag
@@ -228,6 +233,7 @@ data DefFlag
          -- The nat represents which argument the function evaluates to
     | NoMangle NoMangleDirective
          -- use the user provided name directly (backend, name)
+%name DefFlag dflag
 
 export
 Eq DefFlag where

src/Core/TT.idr

@@ -870,7 +870,7 @@ data Term : List Name -> Type where
      TType : FC -> Name -> -- universe variable
              Term vars
 
-%name Term s, t, u
+%name Term t, u
 
 -- Remove/restore the given namespace from all Refs. This is to allow
 -- writing terms and case trees to disk without repeating the same namespace
@@ -1030,6 +1030,7 @@ interface Weaken tm where
 
 public export
 data Visibility = Private | Export | Public
+%name Visibility vis
 
 export
 Show Visibility where
@@ -1066,6 +1067,7 @@ Ord Visibility where
 
 public export
 data TotalReq = Total | CoveringOnly | PartialOK
+%name TotalReq treq
 
 export
 Eq TotalReq where

src/TTImp/TTImp.idr

@@ -44,6 +44,8 @@ Weaken NestedNames where
 public export
 data BindMode = PI RigCount | PATTERN | COVERAGE | NONE
 
+%name BindMode bm
+
 mutual
 
   public export
@@ -123,6 +125,8 @@ mutual
        -- with-disambiguation
        IWithUnambigNames : FC -> List (FC, Name) -> RawImp' nm -> RawImp' nm
 
+  %name RawImp' t, u
+
   public export
   IFieldUpdate : Type
   IFieldUpdate = IFieldUpdate' Name
@@ -131,6 +135,7 @@ mutual
   data IFieldUpdate' : Type -> Type where
        ISetField : (path : List String) -> RawImp' nm -> IFieldUpdate' nm
        ISetFieldApp : (path : List String) -> RawImp' nm -> IFieldUpdate' nm
+  %name IFieldUpdate' upd
 
   public export
   AltType : Type
@@ -141,6 +146,7 @@ mutual
        FirstSuccess : AltType' nm
        Unique : AltType' nm
        UniqueDefault : RawImp' nm -> AltType' nm
+  %name AltType' alt
 
   export
   covering
@@ -234,6 +240,7 @@ mutual
        Macro : FnOpt' nm
        SpecArgs : List Name -> FnOpt' nm
        NoMangle : Maybe NoMangleDirective -> FnOpt' nm
+  %name FnOpt' fopt
 
   public export
   isTotalityReq : FnOpt' nm -> Bool
@@ -298,6 +305,8 @@ mutual
   data ImpTy' : Type -> Type where
        MkImpTy : FC -> (nameFC : FC) -> (n : Name) -> (ty : RawImp' nm) -> ImpTy' nm
 
+  %name ImpTy' ty
+
   export
   covering
   Show nm => Show (ImpTy' nm) where
@@ -310,6 +319,7 @@ mutual
        UniqueSearch : DataOpt -- auto implicit search must check result is unique
        External : DataOpt -- implemented externally
        NoNewtype : DataOpt -- don't apply newtype optimisation
+  %name DataOpt dopt
 
   export
   Eq DataOpt where
@@ -331,6 +341,8 @@ mutual
                    (datacons : List (ImpTy' nm)) -> ImpData' nm
        MkImpLater : FC -> (n : Name) -> (tycon : RawImp' nm) -> ImpData' nm
 
+  %name ImpData' dat
+
   export
   covering
   Show nm => Show (ImpData' nm) where
@@ -349,6 +361,8 @@ mutual
        MkIField : FC -> RigCount -> PiInfo (RawImp' nm) -> Name -> RawImp' nm ->
                   IField' nm
 
+  %name IField' fld
+
   public export
   ImpParameter : Type
   ImpParameter = ImpParameter' Name
@@ -370,6 +384,8 @@ mutual
                      (fields : List (IField' nm)) ->
                      ImpRecord' nm
 
+  %name ImpRecord' rec
+
   export
   covering
   Show nm => Show (IField' nm) where
@@ -410,6 +426,8 @@ mutual
                     List (ImpClause' nm) -> ImpClause' nm
        ImpossibleClause : FC -> (lhs : RawImp' nm) -> ImpClause' nm
 
+  %name ImpClause' cl
+
   export
   covering
   Show nm => Show (ImpClause' nm) where
@@ -453,6 +471,8 @@ mutual
        ILog : Maybe (List String, Nat) -> ImpDecl' nm
        IBuiltin : FC -> BuiltinType -> Name -> ImpDecl' nm
 
+  %name ImpDecl' decl
+
   export
   covering
   Show nm => Show (ImpDecl' nm) where
@@ -882,6 +902,7 @@ data Arg' nm
    = Explicit FC (RawImp' nm)
    | Auto     FC (RawImp' nm)
    | Named    FC Name (RawImp' nm)
+%name Arg' arg
 
 public export
 Arg : Type

src/TTImp/Utils.idr

@@ -585,18 +585,35 @@ getArgName defs x bound allvars ty
     defaultNames : List String
     defaultNames = ["x", "y", "z", "w", "v", "s", "t", "u"]
 
-    findNames : NF vars -> Core (List String)
-    findNames (NBind _ x (Pi _ _ _ _) _)
-        = pure (filter notBound ["f", "g"])
-    findNames (NTCon _ n _ _ _)
-        = pure $ filter notBound
-        $ case !(lookupName n (NameMap.toList (namedirectives defs))) of
-               Nothing => defaultNames
-               Just ns => ns
-    findNames (NPrimVal fc c) = do
-          let defaultPos = ["m", "n", "p", "q"]
-          let defaultInts = ["i", "j", "k", "l"]
-          pure $ filter notBound $ case c of
+    namesFor : Name -> Core (Maybe (List String))
+    namesFor n = lookupName n (NameMap.toList (namedirectives defs))
+
+    findNamesM : NF vars -> Core (Maybe (List String))
+    findNamesM (NBind _ x (Pi _ _ _ _) _)
+        = pure (Just ["f", "g"])
+    findNamesM (NTCon _ n _ d [(_, v)]) = do
+          case dropNS !(full (gamma defs) n) of
+            UN (Basic "List") =>
+              do nf <- evalClosure defs v
+                 case !(findNamesM nf) of
+                   Nothing => namesFor n
+                   Just ns => pure (Just (map (++ "s") ns))
+            UN (Basic "Maybe") =>
+              do nf <- evalClosure defs v
+                 case !(findNamesM nf) of
+                   Nothing => namesFor n
+                   Just ns => pure (Just (map ("m" ++) ns))
+            UN (Basic "SnocList") =>
+              do nf <- evalClosure defs v
+                 case !(findNamesM nf) of
+                   Nothing => namesFor n
+                   Just ns => pure (Just (map ("s" ++) ns))
+            _ => namesFor n
+    findNamesM (NTCon _ n _ _ _) = namesFor n
+    findNamesM (NPrimVal fc c) = do
+          let defaultPos = Just ["m", "n", "p", "q"]
+          let defaultInts = Just ["i", "j", "k", "l"]
+          pure $ map (filter notBound) $ case c of
             PrT IntType => defaultInts
             PrT Int8Type => defaultInts
             PrT Int16Type => defaultInts
@@ -607,12 +624,15 @@ getArgName defs x bound allvars ty
             PrT Bits16Type => defaultPos
             PrT Bits32Type => defaultPos
             PrT Bits64Type => defaultPos
-            PrT StringType => ["str"]
-            PrT CharType => ["c","d"]
-            PrT DoubleType => ["dbl"]
-            PrT WorldType => ["wrld", "w"]
-            _ => defaultNames -- impossible
-    findNames ty = pure (filter notBound defaultNames)
+            PrT StringType => Just ["str"]
+            PrT CharType => Just ["c","d"]
+            PrT DoubleType => Just ["dbl"]
+            PrT WorldType => Just ["wrld", "w"]
+            _ => Nothing -- impossible
+    findNamesM ty = pure Nothing
+
+    findNames : NF vars -> Core (List String)
+    findNames nf = pure $ filter notBound $ fromMaybe defaultNames !(findNamesM nf)
 
     getName : Name -> List String -> List Name -> String
     getName (UN (Basic n)) defs used = unique (n :: defs) (n :: defs) 0 used