From 071d37197aa8ec10f19a553788222b04e5a5f5f8 Mon Sep 17 00:00:00 2001 From: "G. Allais" Date: Fri, 27 May 2022 10:54:34 +0100 Subject: [PATCH] [ IDE ] intro command (#2502) --- docs/source/implementation/ide-protocol.rst | 4 + idris2api.ipkg | 1 + src/Core/Env.idr | 1 - src/Core/TT.idr | 4 + src/Idris/IDEMode/REPL.idr | 6 ++ src/Idris/Parser.idr | 1 + src/Idris/REPL.idr | 23 ++++++ src/Idris/REPL/Common.idr | 1 + src/Idris/Resugar.idr | 50 +++++++------ src/Idris/Syntax.idr | 1 + src/Protocol/IDE/Command.idr | 8 +- src/Protocol/IDE/Result.idr | 14 ++-- src/Protocol/SExp.idr | 11 +++ src/TTImp/Interactive/CaseSplit.idr | 64 ---------------- src/TTImp/Interactive/ExprSearch.idr | 1 - src/TTImp/Interactive/Intro.idr | 83 +++++++++++++++++++++ src/TTImp/Utils.idr | 68 +++++++++++++++++ 17 files changed, 245 insertions(+), 96 deletions(-) create mode 100644 src/TTImp/Interactive/Intro.idr diff --git a/docs/source/implementation/ide-protocol.rst b/docs/source/implementation/ide-protocol.rst index 6c8700875..ab56e2e0b 100644 --- a/docs/source/implementation/ide-protocol.rst +++ b/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 ---------------- diff --git a/idris2api.ipkg b/idris2api.ipkg index a876d26f4..6bbec7061 100644 --- a/idris2api.ipkg +++ b/idris2api.ipkg @@ -281,6 +281,7 @@ modules = TTImp.Interactive.CaseSplit, TTImp.Interactive.ExprSearch, TTImp.Interactive.GenerateDef, + TTImp.Interactive.Intro, TTImp.Interactive.MakeLemma, Yaffle.Main, diff --git a/src/Core/Env.idr b/src/Core/Env.idr index c616ce919..0b689a238 100644 --- a/src/Core/Env.idr +++ b/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 diff --git a/src/Core/TT.idr b/src/Core/TT.idr index ac5a9f673..7f4210b15 100644 --- a/src/Core/TT.idr +++ b/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 diff --git a/src/Idris/IDEMode/REPL.idr b/src/Idris/IDEMode/REPL.idr index bd0ab4cf2..37a362a5f 100644 --- a/src/Idris/IDEMode/REPL.idr +++ b/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 diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index bcfb40786..64abcb7a2 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -2361,6 +2361,7 @@ parserCommandsForHelp = , editLineNameArgCmd (ParseREPLCmd ["ml", "makelemma"]) MakeLemma "Make lemma for term defined on line " , editLineNameArgCmd (ParseREPLCmd ["mc", "makecase"]) MakeCase "Make case on term defined on line " , editLineNameArgCmd (ParseREPLCmd ["mw", "makewith"]) MakeWith "Add with expression on term defined on line " + , editLineNameArgCmd (ParseREPLCmd ["intro"]) Intro "Introduce unambiguous constructor in hole defined on line " , editLineNamePTermArgCmd (ParseREPLCmd ["refine"]) Refine "Refine hole with identifier on line and column " , editLineNameCSVArgCmd (ParseREPLCmd ["ps", "proofsearch"]) ExprSearch "Search for a proof" , noArgCmd (ParseREPLCmd ["psnext"]) (Editing ExprSearchNext) "Show next proof" diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr index 3165e13ed..b3f69bb04 100644 --- a/src/Idris/REPL.idr +++ b/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 diff --git a/src/Idris/REPL/Common.idr b/src/Idris/REPL/Common.idr index a98c483a4..6dc921cc5 100644 --- a/src/Idris/REPL/Common.idr +++ b/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 diff --git a/src/Idris/Resugar.idr b/src/Idris/Resugar.idr index b02538993..72a1317bd 100644 --- a/src/Idris/Resugar.idr +++ b/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 diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr index 24204caca..a9435d978 100644 --- a/src/Idris/Syntax.idr +++ b/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 diff --git a/src/Protocol/IDE/Command.idr b/src/Protocol/IDE/Command.idr index 391804302..ac537a030 100644 --- a/src/Protocol/IDE/Command.idr +++ b/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 diff --git a/src/Protocol/IDE/Result.idr b/src/Protocol/IDE/Result.idr index 58146410f..ab4d0d0ab 100644 --- a/src/Protocol/IDE/Result.idr +++ b/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 diff --git a/src/Protocol/SExp.idr b/src/Protocol/SExp.idr index 696e18b10..d684353eb 100644 --- a/src/Protocol/SExp.idr +++ b/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 [] diff --git a/src/TTImp/Interactive/CaseSplit.idr b/src/TTImp/Interactive/CaseSplit.idr index 89494aa6d..fdac038af 100644 --- a/src/TTImp/Interactive/CaseSplit.idr +++ b/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) diff --git a/src/TTImp/Interactive/ExprSearch.idr b/src/TTImp/Interactive/ExprSearch.idr index 7a152157d..7e661500c 100644 --- a/src/TTImp/Interactive/ExprSearch.idr +++ b/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 diff --git a/src/TTImp/Interactive/Intro.idr b/src/TTImp/Interactive/Intro.idr new file mode 100644 index 000000000..57973f0dc --- /dev/null +++ b/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 [] diff --git a/src/TTImp/Utils.idr b/src/TTImp/Utils.idr index 716c5666c..43002fb20 100644 --- a/src/TTImp/Utils.idr +++ b/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 []