diff --git a/idris2.ipkg b/idris2.ipkg index 96a47ba31..ccb37e788 100644 --- a/idris2.ipkg +++ b/idris2.ipkg @@ -71,6 +71,7 @@ modules = Idris.IDEMode.Parser, Idris.IDEMode.REPL, Idris.IDEMode.TokenLine, + Idris.IDEMode.Holes, Idris.ModTree, Idris.Package, Idris.Parser, diff --git a/src/Idris/IDEMode/Holes.idr b/src/Idris/IDEMode/Holes.idr new file mode 100644 index 000000000..f6fbeec17 --- /dev/null +++ b/src/Idris/IDEMode/Holes.idr @@ -0,0 +1,146 @@ +module Idris.IDEMode.Holes + +import Core.Env + +import Idris.Resugar +import Idris.Syntax + +import Idris.IDEMode.Commands + +public export +record HolePremise where + constructor MkHolePremise + name : Name + type : PTerm + multiplicity : RigCount + isImplicit : Bool + + +public export +record HoleData where + constructor MkHoleData + name : Name + type : PTerm + context : List HolePremise + +||| If input is a hole, return number of locals in scope at binding +||| point +export +isHole : GlobalDef -> Maybe Nat +isHole def + = case definition def of + Hole locs _ => Just locs + PMDef pi _ _ _ _ => + case holeInfo pi of + NotHole => Nothing + SolvedHole n => Just n + None => Just 0 + _ => Nothing + + + +-- Bring these back into REPL.idr +showName : Name -> Bool +showName (UN "_") = False +showName (MN _ _) = False +showName _ = True + +showCount : RigCount -> String +showCount = elimSemi + " 0 " + " 1 " + (const " ") + +impBracket : Bool -> String -> String +impBracket False str = str +impBracket True str = "{" ++ str ++ "}" + +tidy : Name -> String +tidy (MN n _) = n +tidy n = show n + +export +extractHoleData : {vars : _} -> + {auto c : Ref Ctxt Defs} -> + {auto s : Ref Syn SyntaxInfo} -> + Defs -> Env Term vars -> Name -> Nat -> Term vars -> + Core HoleData +extractHoleData defs env fn (S args) (Bind fc x (Let c val ty) sc) + = extractHoleData defs env fn args (subst val sc) +extractHoleData defs env fn (S args) (Bind fc x b sc) + = do rest <- extractHoleData defs (b :: env) fn args sc + let True = showName x + | False => pure rest + ity <- resugar env !(normalise defs env (binderType b)) + let premise = MkHolePremise x ity (multiplicity b) (implicitBind b) + pure $ record { context $= (premise ::) } rest + where + implicitBind : Binder (Term vars) -> Bool + implicitBind (Pi _ Explicit _) = False + implicitBind (Pi _ _ _) = True + implicitBind (Lam _ Explicit _) = False + implicitBind (Lam _ _ _) = True + implicitBind _ = False + +extractHoleData defs env fn args ty + = do ity <- resugar env !(normaliseHoles defs env ty) + pure $ MkHoleData fn ity [] + + +export +holeData : {vars : _} -> + {auto c : Ref Ctxt Defs} -> + {auto s : Ref Syn SyntaxInfo} -> + Defs -> Env Term vars -> Name -> Nat -> Term vars -> + Core HoleData + +holeData gam env fn args ty + = do hdata <- extractHoleData gam env fn args ty + pp <- getPPrint + pure $ if showImplicits pp + then hdata + else record { context $= dropShadows } hdata + where + dropShadows : List HolePremise -> List HolePremise + dropShadows [] = [] + dropShadows (premise :: rest) + = if premise.name `elem` map name rest + then dropShadows rest + else premise :: dropShadows rest + + +export +showHole : {vars : _} -> + {auto c : Ref Ctxt Defs} -> + {auto s : Ref Syn SyntaxInfo} -> + Defs -> Env Term vars -> Name -> Nat -> Term vars -> + Core String +showHole defs env fn args ty + = do hdata <- holeData defs env fn args ty + case hdata.context of + [] => pure $ show (hdata.name) ++ " : " ++ show hdata.type + _ => pure $ concat + (map (\premise => showCount premise.multiplicity + ++ (impBracket premise.isImplicit $ + tidy premise.name ++ " : " ++ (show premise.type) ++ "\n" ) + ) hdata.context) + ++ "-------------------------------------\n" + ++ nameRoot (hdata.name) ++ " : " ++ show hdata.type + +sexpPremise : HolePremise -> SExp +sexpPremise premise = + SExpList [StringAtom $ showCount premise.multiplicity + ++ (impBracket premise.isImplicit $ + tidy premise.name) + ,StringAtom $ show premise.type + ,SExpList [] -- TODO: metadata + ] + +export +sexpHole : HoleData -> SExp +sexpHole hole = SExpList + [ StringAtom (show hole.name) + , SExpList $ map sexpPremise hole.context -- Premises + , SExpList [ StringAtom $ show hole.type -- Conclusion + , SExpList[]] -- TODO: Highlighting information + ] diff --git a/src/Idris/IDEMode/REPL.idr b/src/Idris/IDEMode/REPL.idr index 84924527f..7084c715c 100644 --- a/src/Idris/IDEMode/REPL.idr +++ b/src/Idris/IDEMode/REPL.idr @@ -261,9 +261,6 @@ SExpable REPLOpt where toSExp (CG str) = SExpList [ SymbolAtom "cg", toSExp str ] -sexpName : Name -> SExp -sexpName n = SExpList [ StringAtom (show n), SExpList [], SExpList [StringAtom "?", SExpList[]]] - displayIDEResult : {auto c : Ref Ctxt Defs} -> {auto u : Ref UST UState} -> {auto s : Ref Syn SyntaxInfo} -> @@ -317,14 +314,8 @@ displayIDEResult outf i (REPL $ CheckedTotal xs) = printIDEResult outf i $ StringAtom $ showSep "\n" $ map (\ (fn, tot) => (show fn ++ " is " ++ show tot)) xs -displayIDEResult outf i (REPL $ FoundHoles []) - = printIDEResult outf i $ SExpList [] -displayIDEResult outf i (REPL $ FoundHoles xs) - = printIDEResult outf i $ holesSexp - where - holesSexp : SExp - holesSexp = SExpList $ map sexpName xs - +displayIDEResult outf i (REPL $ FoundHoles holes) + = printIDEResult outf i $ SExpList $ map sexpHole holes displayIDEResult outf i (REPL $ LogLevelSet k) = printIDEResult outf i $ StringAtom $ "Set loglevel to " ++ show k diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr index 9ddd82a7d..5f17a203c 100644 --- a/src/Idris/REPL.idr +++ b/src/Idris/REPL.idr @@ -26,6 +26,7 @@ import Idris.Error import Idris.IDEMode.CaseSplit import Idris.IDEMode.Commands import Idris.IDEMode.MakeClause +import Idris.IDEMode.Holes import Idris.ModTree import Idris.Parser import Idris.Resugar @@ -76,82 +77,6 @@ showInfo (n, idx, d) coreLift $ putStrLn $ "Size change: " ++ showSep ", " scinfo -isHole : GlobalDef -> Maybe Nat -isHole def - = case definition def of - Hole locs _ => Just locs - PMDef pi _ _ _ _ => - case holeInfo pi of - NotHole => Nothing - SolvedHole n => Just n - _ => Nothing - -showCount : RigCount -> String -showCount = elimSemi - " 0 " - " 1 " - (const " ") - -impBracket : Bool -> String -> String -impBracket False str = str -impBracket True str = "{" ++ str ++ "}" - -showName : Name -> Bool -showName (UN "_") = False -showName (MN _ _) = False -showName _ = True - -tidy : Name -> String -tidy (MN n _) = n -tidy n = show n - -showEnv : {vars : _} -> - {auto c : Ref Ctxt Defs} -> - {auto s : Ref Syn SyntaxInfo} -> - Defs -> Env Term vars -> Name -> Nat -> Term vars -> - Core (List (Name, String), String) -showEnv defs env fn (S args) (Bind fc x (Let c val ty) sc) - = showEnv defs env fn args (subst val sc) -showEnv defs env fn (S args) (Bind fc x b sc) - = do ity <- resugar env !(normalise defs env (binderType b)) - let pre = if showName x - then REPL.showCount (multiplicity b) ++ - impBracket (implicitBind b) (tidy x ++ " : " ++ show ity) ++ "\n" - else "" - (envstr, ret) <- showEnv defs (b :: env) fn args sc - pure ((x, pre) :: envstr, ret) - where - implicitBind : Binder (Term vars) -> Bool - implicitBind (Pi _ Explicit _) = False - implicitBind (Pi _ _ _) = True - implicitBind (Lam _ Explicit _) = False - implicitBind (Lam _ _ _) = True - implicitBind _ = False -showEnv defs env fn args ty - = do ity <- resugar env !(normalise defs env ty) - pure ([], "-------------------------------------\n" ++ - nameRoot fn ++ " : " ++ show ity) - -showHole : {vars : _} -> - {auto c : Ref Ctxt Defs} -> - {auto s : Ref Syn SyntaxInfo} -> - Defs -> Env Term vars -> Name -> Nat -> Term vars -> - Core String -showHole gam env fn args ty - = do (envs, ret) <- showEnv gam env fn args ty - pp <- getPPrint - let envs' = if showImplicits pp - then envs - else dropShadows envs - pure (concat (map snd envs') ++ ret) - where - dropShadows : List (Name, a) -> List (Name, a) - dropShadows [] = [] - dropShadows ((n, ty) :: ns) - = if n `elem` map fst ns - then dropShadows ns - else (n, ty) :: dropShadows ns - displayType : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> Defs -> (Name, Int, GlobalDef) -> @@ -494,7 +419,7 @@ data REPLResult : Type where ProofFound : PTerm -> REPLResult Missed : List MissedResult -> REPLResult CheckedTotal : List (Name, Totality) -> REPLResult - FoundHoles : List Name -> REPLResult + FoundHoles : List HoleData -> REPLResult OptionsSet : List REPLOpt -> REPLResult LogLevelSet : Nat -> REPLResult VersionIs : Version -> REPLResult @@ -702,8 +627,21 @@ process (SetLog lvl) = do setLogLevel lvl pure $ LogLevelSet lvl process Metavars - = do ms <- getUserHoles - pure $ FoundHoles ms + = do defs <- get Ctxt + let ctxt = gamma defs + ms <- getUserHoles + let globs = concat !(traverse (\n => lookupCtxtName n ctxt) ms) + let holesWithArgs = mapMaybe (\(n, i, gdef) => do args <- isHole gdef + pure (n, gdef, args)) + globs + hData <- the (Core $ List HoleData) $ + traverse (\n_gdef_args => + -- Inference can't deal with this for now :/ + let (n, gdef, args) = the (Name, GlobalDef, Nat) n_gdef_args in + holeData defs [] n args (type gdef)) + holesWithArgs + pure $ FoundHoles hData + process (Editing cmd) = do ppopts <- getPPrint -- Since we're working in a local environment, don't do the usual @@ -860,9 +798,9 @@ mutual displayResult (Missed cases) = printResult $ showSep "\n" $ map handleMissing cases displayResult (CheckedTotal xs) = printResult $ showSep "\n" $ map (\ (fn, tot) => (show fn ++ " is " ++ show tot)) xs displayResult (FoundHoles []) = printResult $ "No holes" - displayResult (FoundHoles [x]) = printResult $ "1 hole: " ++ show x + displayResult (FoundHoles [x]) = printResult $ "1 hole: " ++ show x.name displayResult (FoundHoles xs) = printResult $ show (length xs) ++ " holes: " ++ - showSep ", " (map show xs) + showSep ", " (map (show . name) xs) displayResult (LogLevelSet k) = printResult $ "Set loglevel to " ++ show k displayResult (VersionIs x) = printResult $ showVersion True x displayResult (RequestedHelp) = printResult displayHelp diff --git a/tests/typedd-book/chapter01/expected b/tests/typedd-book/chapter01/expected index 8b8af5a54..b2671889e 100644 --- a/tests/typedd-book/chapter01/expected +++ b/tests/typedd-book/chapter01/expected @@ -3,6 +3,5 @@ 3/5: Building HelloHole (HelloHole.idr) 4/5: Building HoleFix (HoleFix.idr) 5/5: Building All (All.idr) -Main> ------------------------------------- -convert : Char -> String +Main> Main.convert : Char -> String Main> Bye for now!