From ced6134f79e6162fd104b260623fcfddf9f72ed9 Mon Sep 17 00:00:00 2001 From: Ohad Kammar Date: Mon, 25 May 2020 07:13:12 +0100 Subject: [PATCH] Refactor hole information extracting functions into a new submodule Introduce a new data structure for IDE-related hole data Separate hole printing from informationextraction --- idris2.ipkg | 1 + src/Idris/IDEMode/Holes.idr | 123 ++++++++++++++++++++++++++++++++++++ src/Idris/IDEMode/REPL.idr | 20 ++++-- src/Idris/REPL.idr | 76 +--------------------- 4 files changed, 140 insertions(+), 80 deletions(-) create mode 100644 src/Idris/IDEMode/Holes.idr diff --git a/idris2.ipkg b/idris2.ipkg index 54b6c23d0..952743481 100644 --- a/idris2.ipkg +++ b/idris2.ipkg @@ -70,6 +70,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..d3bc6b1d3 --- /dev/null +++ b/src/Idris/IDEMode/Holes.idr @@ -0,0 +1,123 @@ +module Idris.IDEMode.Holes + +import Core.Env + +import Idris.Resugar +import Idris.Syntax + +record HolePremise where + constructor MkHolePremise + name : Name + type : PTerm + multiplicity : RigCount + isImplicit : Bool + + +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 + _ => 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 !(normalise 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 record { context $= dropShadows } hdata + else 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 + pure $ concat + (map (\hole => showCount hole.multiplicity + ++ (impBracket hole.isImplicit $ + tidy hole.name ++ " : " ++ (show hole.type) ++ "\n" ) + ) hdata.context) + ++ "-------------------------------------\n" + ++ nameRoot (hdata.name) ++ " : " ++ show hdata.type + + diff --git a/src/Idris/IDEMode/REPL.idr b/src/Idris/IDEMode/REPL.idr index 84924527f..7e99ffa94 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} -> @@ -320,10 +317,21 @@ displayIDEResult outf i (REPL $ CheckedTotal xs) displayIDEResult outf i (REPL $ FoundHoles []) = printIDEResult outf i $ SExpList [] displayIDEResult outf i (REPL $ FoundHoles xs) - = printIDEResult outf i $ holesSexp + = printIDEResult outf i $ !holesSexp where - holesSexp : SExp - holesSexp = SExpList $ map sexpName xs + sexpName : + Name -> Core SExp + sexpName n = do + pure $ SExpList + [ StringAtom (show n) + , SExpList [] -- Premises + , SExpList [ StringAtom "?" -- Conclusion + , SExpList[]] -- TODO: Highlighting information + ] + + holesSexp : Core SExp + holesSexp = pure $ SExpList !( traverse sexpName xs ) + displayIDEResult outf i (REPL $ LogLevelSet k) = printIDEResult outf i diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr index 745533417..c912ff01a 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,81 +77,8 @@ 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 +-- Put the printing of holes back here displayType : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} ->