[ IDE ] intro command (#2502)

docs/source/implementation/ide-protocol.rst

@@ -173,6 +173,10 @@ New in Version 2 of the protocol are:
   ``(:proof-search-next)``
     Replace the previous proof search result with the next proof search result.
 
+  ``(:intro LINE NAME)``
+    Returns the non-empty list of valid saturated constructors that can be used in the hole
+    at line ``LINE`` named ``NAME``.
+
 Possible Replies
 ----------------
 

idris2api.ipkg

@@ -281,6 +281,7 @@ modules =
     TTImp.Interactive.CaseSplit,
     TTImp.Interactive.ExprSearch,
     TTImp.Interactive.GenerateDef,
+    TTImp.Interactive.Intro,
     TTImp.Interactive.MakeLemma,
 
     Yaffle.Main,

src/Core/Env.idr

@@ -17,7 +17,6 @@ export
 extend : (x : Name) -> Binder (tm vars) -> Env tm vars -> Env tm (x :: vars)
 extend x = (::) {x}
 
-
 export
 length : Env tm xs -> Nat
 length [] = 0

src/Core/TT.idr

@@ -53,6 +53,10 @@ export
 defaultKindedName : Name -> KindedName
 defaultKindedName nm = MkKindedName Nothing nm nm
 
+export
+funKindedName : Name -> KindedName
+funKindedName nm = MkKindedName (Just Func) nm nm
+
 export
 Show KindedName where show = show . rawName
 

src/Idris/IDEMode/REPL.idr

@@ -177,6 +177,10 @@ process (AddClause l n)
 process (AddMissing l n)
     = do todoCmd "add-missing"
          pure $ REPL $ Edited $ DisplayEdit emptyDoc
+process (Intro l h) =
+   do replWrap $ Idris.REPL.process
+               $ Editing
+               $ Intro False (fromInteger l) (UN $ Basic h) {- hole name -}
 process (Refine l h expr) =
    do let Right (_, _, e) = runParser (Virtual Interactive) Nothing expr aPTerm
         | Left err => pure $ REPL $ REPLError (pretty0 $ show err)
@@ -377,6 +381,8 @@ displayIDEResult outf i (REPL $ Edited (DisplayEdit xs))
   = printIDEResult outf i $ AString $ show xs
 displayIDEResult outf i (REPL $ Edited (EditError x))
   = printIDEError outf i x
+displayIDEResult outf i (REPL $ Edited (MadeIntro is))
+  = printIDEResult outf i $ AnIntroList is
 displayIDEResult outf i (REPL $ Edited (MadeLemma lit name pty pappstr))
   = printIDEResult outf i $ AMetaVarLemma $ MkMetaVarLemma
       { application = pappstr

src/Idris/Parser.idr

@@ -2361,6 +2361,7 @@ parserCommandsForHelp =
   , editLineNameArgCmd (ParseREPLCmd ["ml", "makelemma"]) MakeLemma "Make lemma for term <n> defined on line <l>"
   , editLineNameArgCmd (ParseREPLCmd ["mc", "makecase"]) MakeCase "Make case on term <n> defined on line <l>"
   , editLineNameArgCmd (ParseREPLCmd ["mw", "makewith"]) MakeWith "Add with expression on term <n> defined on line <l>"
+  , editLineNameArgCmd (ParseREPLCmd ["intro"]) Intro "Introduce unambiguous constructor in hole <n> defined on line <l>"
   , editLineNamePTermArgCmd (ParseREPLCmd ["refine"]) Refine "Refine hole <h> with identifier <n> on line <l> and column <c>"
   , editLineNameCSVArgCmd (ParseREPLCmd ["ps", "proofsearch"]) ExprSearch "Search for a proof"
   , noArgCmd (ParseREPLCmd ["psnext"]) (Editing ExprSearchNext) "Show next proof"

src/Idris/REPL.idr

@@ -52,6 +52,7 @@ import TTImp.Elab.Local
 import TTImp.Interactive.CaseSplit
 import TTImp.Interactive.ExprSearch
 import TTImp.Interactive.GenerateDef
+import TTImp.Interactive.Intro
 import TTImp.Interactive.MakeLemma
 import TTImp.TTImp
 import TTImp.Unelab
@@ -487,6 +488,27 @@ processEdit (AddClause upd line name)
          if upd
             then updateFile (addClause c (integerToNat (cast line)))
             else pure $ DisplayEdit (pretty0 c)
+processEdit (Intro upd line hole)
+    = do defs <- get Ctxt
+         -- Grab the hole's definition (and check it is not a solved hole)
+         [(h, hidx, hgdef)] <- lookupCtxtName hole (gamma defs)
+           | _ => pure $ EditError ("Could not find hole named" <++> pretty0 hole)
+         let Hole args _ = definition hgdef
+           | _ => pure $ EditError (pretty0 hole <++> "is not a refinable hole")
+         let (lhsCtxt ** (env, htyInLhsCtxt)) = underPis (cast args) [] (type hgdef)
+
+         (iintrod :: iintrods) <- intro hidx hole env htyInLhsCtxt
+           | [] => pure $ EditError "Don't know what to do."
+         pintrods <- traverseList1 pterm (iintrod ::: iintrods)
+         syn <- get Syn
+         let brack = elemBy (\x, y => dropNS x == dropNS y) hole (bracketholes syn)
+         let introds = map (show . pretty . ifThenElse brack (addBracket replFC) id) pintrods
+
+         if upd
+            then case introds of
+                   introd ::: [] => updateFile (proofSearch hole introd (integerToNat (cast (line - 1))))
+                   _ => pure $ EditError "Don't know what to do"
+            else pure $ MadeIntro introds
 processEdit (Refine upd line hole e)
     = do defs <- get Ctxt
          -- First we grab the hole's definition (and check it is not a solved hole)
@@ -1238,6 +1260,7 @@ mutual
     = printResult $ pretty0 (relit lit (show name ++ " : " ++ show pty ++ "\n") ++ pappstr)
   displayResult (Edited (MadeWith lit wapp)) = printResult $ pretty0 $ showSep "\n" (map (relit lit) wapp)
   displayResult (Edited (MadeCase lit cstr)) = printResult $ pretty0 $ showSep "\n" (map (relit lit) cstr)
+  displayResult (Edited (MadeIntro is)) = printResult $ pretty0 $ showSep "\n" (toList is)
   displayResult (OptionsSet opts) = printResult (vsep (pretty0 <$> opts))
 
   -- do not use a catchall so that we are warned when a new constructor is added

src/Idris/REPL/Common.idr

@@ -200,6 +200,7 @@ data EditResult : Type where
   MadeLemma : Maybe String -> Name -> IPTerm -> String -> EditResult
   MadeWith : Maybe String -> List String -> EditResult
   MadeCase : Maybe String -> List String -> EditResult
+  MadeIntro : List1 String -> EditResult
 
 public export
 data MissedResult : Type where

src/Idris/Resugar.idr

@@ -180,29 +180,33 @@ mutual
       "rangeFromThenTo" => pure $ PRange fc (unbracket l) (Just $ unbracket m) (unbracket r)
       _ => Nothing
   sugarAppM (PApp fc (PApp _ (PRef opFC (MkKindedName nt (NS ns nm) rn)) l) r) =
-    if builtinNS == ns
-       then case nameRoot nm of
-         "Pair"   => pure $ PPair fc (unbracket l) (unbracket r)
-         "MkPair" => pure $ PPair fc (unbracket l) (unbracket r)
-         "DPair"  => case unbracket r of
-            PLam _ _ _ n _ r' => pure $ PDPair fc opFC n (unbracket l) (unbracket r')
-            _                 => Nothing
-         "Equal"  => pure $ PEq fc (unbracket l) (unbracket r)
-         "==="    => pure $ PEq fc (unbracket l) (unbracket r)
-         "~=~"    => pure $ PEq fc (unbracket l) (unbracket r)
-         _        => Nothing
-       else case nameRoot nm of
-              "::" => case sugarApp (unbracket r) of
-                PList fc nilFC xs => pure $ PList fc nilFC ((opFC, unbracketApp l) :: xs)
-                _           => Nothing
-              ":<" => case sugarApp (unbracket l) of
-                        PSnocList fc nilFC xs => pure $ PSnocList fc nilFC
-                                                  (xs :< (opFC, unbracketApp r))
-                        _                     => Nothing
-              "rangeFromTo" => pure $ PRange fc (unbracket l) Nothing (unbracket r)
-              "rangeFromThen" => pure $ PRangeStream fc (unbracket l) (Just $ unbracket r)
-
-              _    => Nothing
+    if builtinNS == ns then
+      case nameRoot nm of
+        "Pair"   => pure $ PPair fc (unbracket l) (unbracket r)
+        "MkPair" => pure $ PPair fc (unbracket l) (unbracket r)
+        "DPair"  => case unbracket r of
+          PLam _ _ _ n _ r' => pure $ PDPair fc opFC n (unbracket l) (unbracket r')
+          _                 => Nothing
+        "Equal"  => pure $ PEq fc (unbracket l) (unbracket r)
+        "==="    => pure $ PEq fc (unbracket l) (unbracket r)
+        "~=~"    => pure $ PEq fc (unbracket l) (unbracket r)
+        _        => Nothing
+    else if dpairNS == ns then
+      case nameRoot nm of
+        "MkDPair" => pure $ PDPair fc opFC (unbracket l) (PImplicit opFC) (unbracket r)
+        _                 => Nothing
+    else
+      case nameRoot nm of
+        "::" => case sugarApp (unbracket r) of
+          PList fc nilFC xs => pure $ PList fc nilFC ((opFC, unbracketApp l) :: xs)
+          _ => Nothing
+        ":<" => case sugarApp (unbracket l) of
+          PSnocList fc nilFC xs => pure $ PSnocList fc nilFC
+                                            (xs :< (opFC, unbracketApp r))
+          _ => Nothing
+        "rangeFromTo" => pure $ PRange fc (unbracket l) Nothing (unbracket r)
+        "rangeFromThen" => pure $ PRangeStream fc (unbracket l) (Just $ unbracket r)
+        _    => Nothing
   sugarAppM tm =
   -- refolding natural numbers if the expression is a constant
     let Nothing = extractNat 0 tm

src/Idris/Syntax.idr

@@ -600,6 +600,7 @@ data EditCmd : Type where
      CaseSplit : Bool -> Int -> Int -> Name -> EditCmd
      AddClause : Bool -> Int -> Name -> EditCmd
      Refine : Bool -> Int -> (hole : Name) -> (expr : PTerm) -> EditCmd
+     Intro : Bool -> Int -> (hole : Name) -> EditCmd
      ExprSearch : Bool -> Int -> Name -> List Name -> EditCmd
      ExprSearchNext : EditCmd
      GenerateDef : Bool -> Int -> Name -> Nat -> EditCmd

src/Protocol/IDE/Command.idr

@@ -30,7 +30,8 @@ data IDECommand
      | AddClause Integer String
      -- deprecated: | AddProofClause
      | AddMissing Integer String
-     | Refine Integer String String
+     | Intro Integer String -- line, hole name
+     | Refine Integer String String -- line, hole name, expression
      | ExprSearch Integer String Hints Bool
      | ExprSearchNext
      | GenerateDef Integer String
@@ -84,6 +85,8 @@ getIDECommand (SExpList [SymbolAtom "add-missing", IntegerAtom line, StringAtom
     = Just $ AddMissing line n
 getIDECommand (SExpList [SymbolAtom "proof-search", IntegerAtom l, StringAtom n])
     = Just $ ExprSearch l n (MkHints []) False
+getIDECommand (SExpList [SymbolAtom "intro", IntegerAtom l, StringAtom h])
+    = Just $ Intro l h
 getIDECommand (SExpList [SymbolAtom "refine", IntegerAtom l, StringAtom h, StringAtom n])
     = Just $ Refine l h n
 getIDECommand (SExpList [SymbolAtom "proof-search", IntegerAtom l, StringAtom n, hs])
@@ -156,7 +159,8 @@ putIDECommand (NameAt cmd (Just (line, col))) = (SExpList [SymbolAtom "name-at",
 putIDECommand (CaseSplit line col n)          = (SExpList [SymbolAtom "case-split", IntegerAtom line, IntegerAtom col, StringAtom n])
 putIDECommand (AddClause line n)              = (SExpList [SymbolAtom "add-clause", IntegerAtom line, StringAtom n])
 putIDECommand (AddMissing line n)             = (SExpList [SymbolAtom "add-missing", IntegerAtom line, StringAtom n])
-putIDECommand (Refine line hole name)  = (SExpList [SymbolAtom "refine", IntegerAtom line, StringAtom hole, StringAtom name])
+putIDECommand (Intro line hole)               = (SExpList [SymbolAtom "intro", IntegerAtom line, StringAtom hole])
+putIDECommand (Refine line hole name)         = (SExpList [SymbolAtom "refine", IntegerAtom line, StringAtom hole, StringAtom name])
 putIDECommand (ExprSearch line n hints mode)  = (SExpList [SymbolAtom "proof-search", IntegerAtom line, StringAtom n, toSExp hints, getMode mode])
   where
   getMode : Bool -> SExp

src/Protocol/IDE/Result.idr

@@ -5,6 +5,7 @@ import Protocol.SExp
 import Protocol.IDE.Holes
 import Protocol.IDE.FileContext
 
+import Data.List1
 import Data.Maybe
 
 %default total
@@ -60,7 +61,7 @@ record MetaVarLemma where
 
 export
 SExpable MetaVarLemma where
-  toSExp mvl =  SExpList [ SymbolAtom "metavariable-lemma"
+  toSExp mvl = SExpList [ SymbolAtom "metavariable-lemma"
              , SExpList [ SymbolAtom "replace-metavariable", StringAtom mvl.application ]
              , SExpList [ SymbolAtom "definition-type", StringAtom mvl.lemma ]
              ]
@@ -68,9 +69,9 @@ SExpable MetaVarLemma where
 export
 FromSExpable MetaVarLemma where
   fromSExp (SExpList [ SymbolAtom "metavariable-lemma"
-             , SExpList [ SymbolAtom "replace-metavariable", StringAtom application ]
-             , SExpList [ SymbolAtom "definition-type", StringAtom lemma ]
-             ]) = Just $ MkMetaVarLemma {application, lemma}
+            , SExpList [ SymbolAtom "replace-metavariable", StringAtom application ]
+            , SExpList [ SymbolAtom "definition-type", StringAtom lemma ]
+            ]) = Just $ MkMetaVarLemma {application, lemma}
   fromSExp _ = Nothing
 
 public export
@@ -110,6 +111,7 @@ data Result =
   | AHoleList (List HoleData)
   | ANameList (List String)
   | AnOptionList (List REPLOption)
+  | AnIntroList (List1 String)
 
 export
 SExpable Result where
@@ -121,7 +123,7 @@ SExpable Result where
   toSExp (AHoleList holes) = toSExp holes
   toSExp (ANameList names) = SExpList (map SymbolAtom names)
   toSExp (AnOptionList opts) = toSExp opts
-
+  toSExp (AnIntroList iss) = toSExp iss
 
 -- This code is not efficient. Usually the client knows what kind of
 -- result to expect based on the request it issued.
@@ -143,4 +145,6 @@ FromSExpable Result where
     | Just nl => pure $ ANameList nl
   let Nothing = fromSExp sexp
     | Just optl => pure $ AnOptionList optl
+  let Nothing = fromSExp sexp
+    | Just optl => pure $ AnIntroList optl
   Nothing

src/Protocol/SExp.idr

@@ -1,6 +1,7 @@
 module Protocol.SExp
 
 import Data.List
+import Data.List1
 
 %default total
 
@@ -112,6 +113,16 @@ FromSExpable a => FromSExpable (List a) where
   fromSExp (SExpList sexps) = traverse fromSExp sexps
   fromSExp _ = Nothing
 
+export
+SExpable a => SExpable (List1 a) where
+  toSExp xs
+      = SExpList (map toSExp (toList xs))
+
+export
+FromSExpable a => FromSExpable (List1 a) where
+  fromSExp (SExpList (sexp :: sexps)) = traverse fromSExp (sexp ::: sexps)
+  fromSExp _ = Nothing
+
 export
 SExpable a => SExpable (Maybe a) where
   toSExp Nothing = SExpList []

src/TTImp/Interactive/CaseSplit.idr

@@ -121,70 +121,6 @@ findAllVars (Bind _ x (PLet _ _ _ _) sc)
     = x :: findAllVars sc
 findAllVars _ = []
 
-unique : List String -> List String -> Int -> List Name -> String
-unique [] supply suff usedns = unique supply supply (suff + 1) usedns
-unique (str :: next) supply suff usedns
-    = let var = mkVarN str suff in
-          if UN (Basic var) `elem` usedns
-             then unique next supply suff usedns
-             else var
-  where
-    mkVarN : String -> Int -> String
-    mkVarN x 0 = x
-    mkVarN x i = x ++ show i
-
-defaultNames : List String
-defaultNames = ["x", "y", "z", "w", "v", "s", "t", "u"]
-
-export
-getArgName : {vars : _} ->
-             {auto c : Ref Ctxt Defs} ->
-             Defs -> Name ->
-             List Name -> -- explicitly bound names (possibly coming later),
-                          -- so we don't invent a default
-                          -- name that duplicates it
-             List Name -> -- names bound so far
-             NF vars -> Core String
-getArgName defs x bound allvars ty
-    = do defnames <- findNames ty
-         pure $ getName x defnames allvars
-  where
-    lookupName : Name -> List (Name, a) -> Core (Maybe a)
-    lookupName n [] = pure Nothing
-    lookupName n ((n', t) :: ts)
-        = if !(getFullName n) == !(getFullName n')
-             then pure (Just t)
-             else lookupName n ts
-
-    notBound : String -> Bool
-    notBound x = not $ UN (Basic x) `elem` bound
-
-    findNames : NF vars -> Core (List String)
-    findNames (NBind _ x (Pi _ _ _ _) _)
-        = pure (filter notBound ["f", "g"])
-    findNames (NTCon _ n _ _ _)
-        = case !(lookupName n (NameMap.toList (namedirectives defs))) of
-               Nothing => pure (filter notBound defaultNames)
-               Just ns => pure (filter notBound ns)
-    findNames ty = pure (filter notBound defaultNames)
-
-    getName : Name -> List String -> List Name -> String
-    getName (UN (Basic n)) defs used = unique (n :: defs) (n :: defs) 0 used
-    getName _ defs used = unique defs defs 0 used
-
-export
-getArgNames : {vars : _} ->
-              {auto c : Ref Ctxt Defs} ->
-              Defs -> List Name -> List Name -> Env Term vars -> NF vars ->
-              Core (List String)
-getArgNames defs bound allvars env (NBind fc x (Pi _ _ p ty) sc)
-    = do ns <- case p of
-                    Explicit => pure [!(getArgName defs x bound allvars !(evalClosure defs ty))]
-                    _ => pure []
-         sc' <- sc defs (toClosure defaultOpts env (Erased fc False))
-         pure $ ns ++ !(getArgNames defs bound (map (UN . Basic) ns ++ allvars) env sc')
-getArgNames defs bound allvars env val = pure []
-
 export
 explicitlyBound : Defs -> NF [] -> Core (List Name)
 explicitlyBound defs (NBind fc x (Pi _ _ _ _) sc)

src/TTImp/Interactive/ExprSearch.idr

@@ -27,7 +27,6 @@ import Idris.REPL.Opts
 import Idris.Syntax
 
 import TTImp.Elab.Check
-import TTImp.Interactive.CaseSplit
 import TTImp.TTImp
 import TTImp.TTImp.Functor
 import TTImp.Unelab

src/TTImp/Interactive/Intro.idr

@@ -0,0 +1,83 @@
+module TTImp.Interactive.Intro
+
+import Core.Core
+import Core.Context
+import Core.Env
+import Core.Metadata
+import Core.TT
+import Core.TT.Views
+import Core.Unify
+
+import Idris.Desugar
+import Idris.REPL.Opts
+import Idris.Resugar
+import Idris.Syntax
+
+import TTImp.Elab
+import TTImp.Elab.Check
+import TTImp.TTImp
+import TTImp.Unelab
+import TTImp.Utils
+
+%default covering
+
+parameters
+  {lhsCtxt : _ }
+  {auto c : Ref Ctxt Defs}
+  {auto s : Ref Syn SyntaxInfo}
+  {auto m : Ref MD Metadata}
+  {auto u : Ref UST UState}
+  {auto r : Ref ROpts REPLOpts}
+  (hidx : Int)
+  (hole : Name)
+  (env : Env Term lhsCtxt)
+
+  introLam : Name -> RigCount -> Term lhsCtxt -> Core IRawImp
+  introLam x rig ty = do
+    ty <- unelab env ty
+    defs <- get Ctxt
+    new_hole <- uniqueHoleName defs [] (nameRoot hole)
+    let iintrod = ILam replFC rig Explicit (Just x) ty (IHole replFC new_hole)
+    pure iintrod
+
+  introCon : Name -> Term lhsCtxt -> Core (List IRawImp)
+  introCon n ty = do
+    defs <- get Ctxt
+    ust <- get UST
+    Just gdef <- lookupCtxtExact n (gamma defs)
+      | _ => pure []
+    -- for now we only handle types with a unique constructor
+    let TCon _ _ _ _ _ _ cs _ = definition gdef
+      | _ => pure []
+    let gty = gnf env ty
+    ics <- for cs $ \ cons => do
+      Just gdef <- lookupCtxtExact cons (gamma defs)
+        | _ => pure Nothing
+      let nargs = lengthExplicitPi $ fst $ snd $ underPis (-1) [] (type gdef)
+      new_hole_names <- uniqueHoleNames defs nargs (nameRoot hole)
+      let new_holes = PHole replFC True <$> new_hole_names
+      let pcons = papply replFC (PRef replFC cons) new_holes
+      res <- catch
+        (do -- We're desugaring it to the corresponding TTImp
+            icons <- desugar AnyExpr lhsCtxt pcons
+            ccons <- checkTerm hidx {-is this correct?-} InExpr [] (MkNested []) env icons gty
+            newdefs <- get Ctxt
+            ncons <- normaliseHoles newdefs env ccons
+            icons <- unelab env ncons
+            pure (Just icons))
+        (\ _ => pure Nothing)
+      put Ctxt defs -- reset the context, we don't want any updates
+      put UST ust
+      pure res
+    pure (catMaybes ics)
+
+  export
+  intro : Term lhsCtxt -> Core (List IRawImp)
+  -- structural cases
+  intro (Bind _ x (Let _ _ ty val) sc) = toList <$> intro (subst val sc)
+  intro (TDelayed _ _ t) = intro t
+  -- interesting ones
+  intro (Bind _ x (Pi _ rig Explicit ty) _) = pure <$> introLam x rig ty
+  intro t = case getFnArgs t of
+    (Ref _ (TyCon _ ar) n, _) => introCon n t
+    _ => pure []

src/TTImp/Utils.idr

@@ -3,6 +3,8 @@ module TTImp.Utils
 import Core.Context
 import Core.Options
 import Core.TT
+import Core.Env
+import Core.Value
 import TTImp.TTImp
 
 import Data.List
@@ -11,6 +13,7 @@ import Data.String
 
 import Idris.Syntax
 
+import Libraries.Data.NameMap
 import Libraries.Utils.String
 
 %default covering
@@ -542,3 +545,68 @@ uniqueHoleNames defs = go [] where
   go acc (S n) hole = do
     hole' <- uniqueHoleName defs acc hole
     go (hole' :: acc) n hole'
+
+unique : List String -> List String -> Int -> List Name -> String
+unique [] supply suff usedns = unique supply supply (suff + 1) usedns
+unique (str :: next) supply suff usedns
+    = let var = mkVarN str suff in
+          if UN (Basic var) `elem` usedns
+             then unique next supply suff usedns
+             else var
+  where
+    mkVarN : String -> Int -> String
+    mkVarN x 0 = x
+    mkVarN x i = x ++ show i
+
+
+export
+getArgName : {vars : _} ->
+             {auto c : Ref Ctxt Defs} ->
+             Defs -> Name ->
+             List Name -> -- explicitly bound names (possibly coming later),
+                          -- so we don't invent a default
+                          -- name that duplicates it
+             List Name -> -- names bound so far
+             NF vars -> Core String
+getArgName defs x bound allvars ty
+    = do defnames <- findNames ty
+         pure $ getName x defnames allvars
+  where
+    lookupName : Name -> List (Name, a) -> Core (Maybe a)
+    lookupName n [] = pure Nothing
+    lookupName n ((n', t) :: ts)
+        = if !(getFullName n) == !(getFullName n')
+             then pure (Just t)
+             else lookupName n ts
+
+    notBound : String -> Bool
+    notBound x = not $ UN (Basic x) `elem` bound
+
+    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 _ _ _)
+        = case !(lookupName n (NameMap.toList (namedirectives defs))) of
+               Nothing => pure (filter notBound defaultNames)
+               Just ns => pure (filter notBound ns)
+    findNames ty = pure (filter notBound defaultNames)
+
+    getName : Name -> List String -> List Name -> String
+    getName (UN (Basic n)) defs used = unique (n :: defs) (n :: defs) 0 used
+    getName _ defs used = unique defs defs 0 used
+
+export
+getArgNames : {vars : _} ->
+              {auto c : Ref Ctxt Defs} ->
+              Defs -> List Name -> List Name -> Env Term vars -> NF vars ->
+              Core (List String)
+getArgNames defs bound allvars env (NBind fc x (Pi _ _ p ty) sc)
+    = do ns <- case p of
+                    Explicit => pure [!(getArgName defs x bound allvars !(evalClosure defs ty))]
+                    _ => pure []
+         sc' <- sc defs (toClosure defaultOpts env (Erased fc False))
+         pure $ ns ++ !(getArgNames defs bound (map (UN . Basic) ns ++ allvars) env sc')
+getArgNames defs bound allvars env val = pure []