
   0 | module Idris.IDEMode.Holes
   1 | 
   2 | import Core.Env
   3 | 
   4 | import Data.String
   5 | 
   6 | import Idris.Resugar
   7 | import Idris.Syntax
   8 | import Idris.Pretty
   9 | 
  10 | import Idris.IDEMode.Commands
  11 | 
  12 | %default covering
  13 | 
  14 | public export
  15 | record Premise where
  16 |   constructor MkHolePremise
  17 |   name         : Name
  18 |   type         : IPTerm
  19 |   multiplicity : RigCount
  20 |   isImplicit   : Bool
  21 | 
  22 | impBracket : Bool -> String -> String
  23 | impBracket False str = str
  24 | impBracket True str = "{" ++ str ++ "}"
  25 | 
  26 | export covering
  27 | Show Holes.Premise where
  28 |   show premise =
  29 |     " " ++ showCount premise.multiplicity ++ " "
  30 |     ++ impBracket premise.isImplicit (show premise.name ++ " : " ++ show premise.type)
  31 | 
  32 | prettyImpBracket : Bool -> Doc ann -> Doc ann
  33 | prettyImpBracket False = id
  34 | prettyImpBracket True = braces
  35 | 
  36 | export
  37 | prettyRigHole : RigCount -> Doc IdrisSyntax
  38 | prettyRigHole = elimSemi (keyword (pretty0 '0') <+> space)
  39 |                          (keyword (pretty0 '1') <+> space)
  40 |                          (const $ space <+> space)
  41 | 
  42 | export
  43 | Pretty IdrisSyntax Holes.Premise where
  44 |   pretty premise =
  45 |      prettyRigHole premise.multiplicity
  46 |      <+> prettyImpBracket premise.isImplicit (pretty0 premise.name <++> colon <++> pretty premise.type)
  47 | 
  48 | public export
  49 | record Data where
  50 |   constructor MkHoleData
  51 |   name : Name
  52 |   type : IPTerm
  53 |   context : List Holes.Premise
  54 | 
  55 | export
  56 | prettyHoles : List Holes.Data -> Doc IdrisSyntax
  57 | prettyHoles holes = case holes of
  58 |   []  => "No holes"
  59 |   [x] => "1 hole" <+> colon <++> prettyHole x
  60 |   xs  => vcat $ (pretty0 (show $ length xs) <++> "holes" <+> colon)
  61 |               :: map (indent 2 . prettyHole) xs
  62 | 
  63 |   where
  64 | 
  65 |    prettyHole : Holes.Data -> Doc IdrisSyntax
  66 |    prettyHole x = pretty0 x.name <++> colon <++> pretty x.type
  67 | 
  68 | 
  69 | ||| If input is a hole, return number of locals in scope at binding
  70 | ||| point
  71 | export
  72 | isHole : GlobalDef -> Maybe Nat
  73 | isHole def
  74 |     = case definition def of
  75 |            Hole locs _ => Just locs
  76 |            PMDef pi _ _ _ _ =>
  77 |                  case holeInfo pi of
  78 |                       NotHole => Nothing
  79 |                       SolvedHole n => Just n
  80 |            None => Just 0
  81 |            _ => Nothing
  82 | 
  83 | 
  84 | -- Bring these back into REPL.idr
  85 | showName : Name -> Bool
  86 | showName (UN Underscore) = False
  87 | showName (MN {}) = False
  88 | showName _ = True
  89 | 
  90 | export
  91 | extractHoleData : {vars : _} ->
  92 |                   {auto c : Ref Ctxt Defs} ->
  93 |                   {auto s : Ref Syn SyntaxInfo} ->
  94 |                   Defs -> Env Term vars -> Name -> Nat -> Term vars ->
  95 |                   Core Holes.Data
  96 | extractHoleData defs env fn (S args) (Bind fc x (Let _ c val ty) sc)
  97 |   = extractHoleData defs env fn args (subst val sc)
  98 | extractHoleData defs env fn (S args) (Bind fc x b sc)
  99 |   = do rest <- extractHoleData defs (b :: env) fn args sc
 100 |        let True = showName x
 101 |          | False => do log "ide-mode.hole" 10 $ "Not showing name: " ++ show x
 102 |                        pure rest
 103 |        log "ide-mode.hole" 10 $ "Showing name: " ++ show x
 104 |        ity <- resugar env !(normalise defs env (binderType b))
 105 |        let premise = MkHolePremise x ity (multiplicity b) (isImplicit b)
 106 |        pure $ { context $= (premise ::)  } rest
 107 | extractHoleData defs env fn args ty
 108 |   = do nty <- normalise defs env ty
 109 |        ity <- resugar env nty
 110 |        log "ide-mode.hole" 20 $
 111 |           "Return type: " ++ show !(toFullNames ty)
 112 |           ++ "\n  Evaluated to: " ++ show !(toFullNames nty)
 113 |           ++ "\n  Resugared to: " ++ show ity
 114 |        pure $ MkHoleData fn ity []
 115 | 
 116 | 
 117 | export
 118 | holeData : {vars : _} ->
 119 |            {auto c : Ref Ctxt Defs} ->
 120 |            {auto s : Ref Syn SyntaxInfo} ->
 121 |            Defs -> Env Term vars -> Name -> Nat -> Term vars ->
 122 |            Core Holes.Data
 123 | 
 124 | holeData gam env fn args ty
 125 |   = do hdata <- extractHoleData gam env fn args ty
 126 |        pp <- getPPrint
 127 |        pure $ if showImplicits pp
 128 |               then hdata
 129 |               else { context $= dropShadows } hdata
 130 |   where
 131 |     dropShadows : List Holes.Premise -> List Holes.Premise
 132 |     dropShadows [] = []
 133 |     dropShadows (premise :: rest)
 134 |         = if premise.name `elem` map name rest
 135 |              then            dropShadows rest
 136 |              else premise :: dropShadows rest
 137 | 
 138 | export
 139 | getUserHolesData :
 140 |   {auto c : Ref Ctxt Defs} ->
 141 |   {auto s : Ref Syn SyntaxInfo} ->
 142 |   Core (List Holes.Data)
 143 | getUserHolesData
 144 |     = do defs <- get Ctxt
 145 |          let ctxt = gamma defs
 146 |          ms  <- getUserHoles
 147 |          let globs = concat !(traverse (\n => lookupCtxtName n ctxt) ms)
 148 |          let holesWithArgs = mapMaybe (\(n, i, gdef) => do args <- isHole gdef
 149 |                                                            pure (n, gdef, args))
 150 |                                       globs
 151 |          traverse (\n_gdef_args =>
 152 |                      -- Inference can't deal with this for now :/
 153 |                      let (n, gdef, args) = the (Name, GlobalDef, Nat) n_gdef_args in
 154 |                      holeData defs Env.empty n args (type gdef))
 155 |                   holesWithArgs
 156 | 
 157 | export
 158 | showHole : {vars : _} ->
 159 |           {auto c : Ref Ctxt Defs} ->
 160 |           {auto s : Ref Syn SyntaxInfo} ->
 161 |           Defs -> Env Term vars -> Name -> Nat -> Term vars ->
 162 |           Core String
 163 | 
 164 | showHole defs env fn args ty
 165 |     = do hdata <- holeData defs env fn args ty
 166 |          case hdata.context of
 167 |            [] => pure $ show (hdata.name) ++ " : " ++ show hdata.type
 168 |            _  => pure $
 169 |               unlines (map show hdata.context)
 170 |               ++ "-------------------------------------\n"
 171 |               ++ nameRoot (hdata.name) ++ " : " ++ show hdata.type
 172 | 
 173 | export
 174 | prettyHole : {vars : _} ->
 175 |              {auto c : Ref Ctxt Defs} ->
 176 |              {auto s : Ref Syn SyntaxInfo} ->
 177 |              Defs -> Env Term vars -> Name -> Nat -> Term vars ->
 178 |              Core (Doc IdrisSyntax)
 179 | prettyHole defs env fn args ty
 180 |   = do hdata <- holeData defs env fn args ty
 181 |        case hdata.context of
 182 |          [] => pure $ pretty0 hdata.name <++> colon <++> pretty hdata.type
 183 |          _  => pure $ indent 1 (vsep $ map pretty hdata.context) <+> hardline
 184 |                   <+> (pretty0 $ replicate 30 '-') <+> hardline
 185 |                   <+> pretty0 (nameRoot $ hdata.name) <++> colon <++> pretty hdata.type
 186 | 
 187 | 
 188 | premiseIDE : Holes.Premise -> HolePremise
 189 | premiseIDE premise = IDE.MkHolePremise
 190 |   { name = " " ++ showCount premise.multiplicity ++ " "
 191 |                ++ (impBracket premise.isImplicit $
 192 |                   show premise.name)
 193 |   , type = show premise.type
 194 |   }
 195 | 
 196 | export
 197 | holeIDE : Holes.Data -> IDE.HoleData
 198 | holeIDE hole = IDE.MkHoleData
 199 |   { name = show hole.name
 200 |   , type = show hole.type
 201 |   , context = map premiseIDE hole.context
 202 |   }
 203 |