0 | module TTImp.Interactive.GenerateDef

  4 | import Core.Env

  5 | import Core.Metadata

  6 | import Core.Unify

  7 | import Core.Value

  9 | import Idris.REPL.Opts

 10 | import Idris.Syntax

 11 | import Parser.Lexer.Source

 13 | import TTImp.Elab

 14 | import TTImp.Elab.Check

 15 | import TTImp.Interactive.CaseSplit

 16 | import TTImp.Interactive.ExprSearch

 17 | import TTImp.ProcessDecls

 18 | import TTImp.ProcessDef

 19 | import TTImp.TTImp

 20 | import TTImp.Utils

 22 | import Libraries.Data.Tap

 24 | %default covering

 26 | fnName : Bool -> Name -> String

 27 | fnName lhs (UN (Basic n))

 28 |     = if isIdentNormal n then n

 29 |       else if lhs then "(" ++ n ++ ")"

 30 |       else "op"

 31 | fnName lhs (NS _ n) = fnName lhs n

 32 | fnName lhs (DN s _) = s

 33 | fnName lhs n = nameRoot n

 36 | uniqueRHS : {auto c : Ref Ctxt Defs} ->

 37 |             {auto s : Ref Syn SyntaxInfo} ->

 38 |             ImpClause -> Core ImpClause

 39 | uniqueRHS (PatClause fc lhs rhs)

 40 |     = pure $ PatClause fc lhs !(mkUniqueName rhs)

 41 |   where

 42 |     mkUniqueName : RawImp -> Core RawImp

 43 |     mkUniqueName (IHole fc' rhsn)

 44 |         = do defs <- get Ctxt

 45 |              rhsn' <- uniqueHoleName defs [] rhsn

 46 |              pure (IHole fc' rhsn')

 47 |     mkUniqueName tm = pure tm -- it'll be a hole, but this is needed for covering

 48 | uniqueRHS c = pure c

 50 | expandClause : {auto c : Ref Ctxt Defs} ->

 51 |                {auto m : Ref MD Metadata} ->

 52 |                {auto u : Ref UST UState} ->

 53 |                {auto s : Ref Syn SyntaxInfo} ->

 54 |                {auto o : Ref ROpts REPLOpts} ->

 55 |                FC -> SearchOpts -> Int -> ImpClause ->

 56 |                Core (Search (List ImpClause))

 57 | expandClause loc opts n c

 58 |     = do c <- uniqueRHS c

 59 |          Right clause <- checkClause linear Private PartialOK False n [] (MkNested []) Env.empty c

 60 |             | Left err => noResult -- TODO: impossible clause, do something

 61 |                                    -- appropriate

 63 |          let MkClause {vars} env lhs rhs = clause

 64 |          let Meta _ i fn _ = getFn rhs

 65 |             | _ => throw (GenericMsg loc "No searchable hole on RHS")

 66 |          defs <- get Ctxt

 67 |          Just (Hole locs _) <- lookupDefExact (Resolved fn) (gamma defs)

 68 |             | _ => throw (GenericMsg loc "No searchable hole on RHS")

 69 |          log "interaction.generate" 10 $ "Expression search for " ++ show (i, fn)

 70 |          rhs' <- exprSearchOpts opts loc (Resolved fn) []

 71 |          traverse (\rhs' =>

 72 |             do let rhsraw = dropLams locs rhs'

 73 |                logTermNF "interaction.generate" 5 "Got clause" env lhs

 74 |                log "interaction.generate" 5 $ "        = " ++ show rhsraw

 75 |                pure [updateRHS c rhsraw]) rhs'

 76 |   where

 77 |     updateRHS : ImpClause -> RawImp -> ImpClause

 78 |     updateRHS (PatClause fc lhs _) rhs = PatClause fc lhs rhs

 79 |     -- 'with' won't happen, include for completeness

 80 |     updateRHS (WithClause fc lhs rig wval prf flags cs) rhs

 81 |       = WithClause fc lhs rig wval prf flags cs

 82 |     updateRHS (ImpossibleClause fc lhs) _ = ImpossibleClause fc lhs

 84 |     dropLams : Nat -> RawImp -> RawImp

 85 |     dropLams Z tm = tm

 86 |     dropLams (S k) (ILam _ _ _ _ _ sc) = dropLams k sc

 87 |     dropLams _ tm = tm

 89 | splittableNames : RawImp -> List Name

 90 | splittableNames (IApp _ f (IBindVar _ n))

 91 |     = splittableNames f ++ [n]

 92 | splittableNames (IApp _ f _)

 93 |     = splittableNames f

 94 | splittableNames (IWithApp _ f (IBindVar _ n))

 95 |     = splittableNames f ++ [n]

 96 | splittableNames (IWithApp _ f _)

 97 |     = splittableNames f

 98 | splittableNames (IAutoApp _ f _)

 99 |     = splittableNames f

100 | splittableNames (INamedApp _ f _ _)

101 |     = splittableNames f

102 | splittableNames _ = []

104 | trySplit : {auto c : Ref Ctxt Defs} ->

105 |            {auto u : Ref UST UState} ->

106 |            {auto s : Ref Syn SyntaxInfo} ->

107 |            {auto o : Ref ROpts REPLOpts} ->

108 |            FC -> RawImp -> ClosedTerm -> RawImp -> Name ->

109 |            Core (Name, List ImpClause)

110 | trySplit loc lhsraw lhs rhs n

111 |     = do OK updates <- getSplitsLHS loc 0 lhs n

112 |             | _ => pure (n, [])

113 |          pure (n, map (\ups => PatClause loc (updateLHS ups lhsraw) rhs)

114 |                       (mapMaybe valid updates))

115 |   where

116 |     valid : ClauseUpdate -> Maybe (List (Name, RawImp))

117 |     valid (Valid lhs' ups) = Just ups

118 |     valid _ = Nothing

120 |     fixNames : RawImp -> RawImp

121 |     fixNames (IVar loc' n@(UN (Basic {}))) = IBindVar loc' n

122 |     fixNames (IVar loc' (MN {})) = Implicit loc' True

123 |     fixNames (IApp loc' f a) = IApp loc' (fixNames f) (fixNames a)

124 |     fixNames (IAutoApp loc' f a) = IAutoApp loc' (fixNames f) (fixNames a)

125 |     fixNames (INamedApp loc' f t a) = INamedApp loc' (fixNames f) t (fixNames a)

126 |     fixNames tm = tm

128 |     updateLHS : List (Name, RawImp) -> RawImp -> RawImp

129 |     updateLHS ups (IVar loc' n)

130 |         = case lookup n ups of

131 |                Nothing => IVar loc' n

132 |                Just tm => fixNames tm

133 |     updateLHS ups (IBindVar loc' n)

134 |         = case lookup n ups of

135 |                Nothing => IBindVar loc' n

136 |                Just tm => fixNames tm

137 |     updateLHS ups (IApp loc' f a) = IApp loc' (updateLHS ups f) (updateLHS ups a)

138 |     updateLHS ups (IAutoApp loc' f a) = IAutoApp loc' (updateLHS ups f) (updateLHS ups a)

139 |     updateLHS ups (INamedApp loc' f t a)

140 |         = INamedApp loc' (updateLHS ups f) t (updateLHS ups a)

141 |     updateLHS ups tm = tm

143 | generateSplits : {auto m : Ref MD Metadata} ->

144 |                  {auto c : Ref Ctxt Defs} ->

145 |                  {auto u : Ref UST UState} ->

146 |                  {auto s : Ref Syn SyntaxInfo} ->

147 |                  {auto o : Ref ROpts REPLOpts} ->

148 |                  FC -> SearchOpts -> Int -> ImpClause ->

149 |                  Core (List (Name, List ImpClause))

150 | generateSplits loc opts fn (ImpossibleClause fc lhs) = pure []

151 | generateSplits loc opts fn (WithClause fc lhs rig wval prf flags cs) = pure []

152 | generateSplits loc opts fn (PatClause fc lhs rhs)

153 |     = do (lhstm, _) <-

154 |                 elabTerm fn (InLHS linear) [] (MkNested []) Env.empty

155 |                          (IBindHere loc PATTERN lhs) Nothing

156 |          let splitnames =

157 |                  if ltor opts then splittableNames lhs

158 |                               else reverse (splittableNames lhs)

159 |          traverse (trySplit fc lhs lhstm rhs) splitnames

161 | collectClauses : {auto c : Ref Ctxt Defs} ->

162 |                  {auto u : Ref UST UState} ->

163 |                  List (Search (List ImpClause)) ->

164 |                  Core (Search (List ImpClause))

165 | collectClauses [] = one []

166 | collectClauses (x :: xs)

167 |     = do xs' <- collectClauses xs

168 |          combine (++) x xs'

171 |   tryAllSplits : {auto c : Ref Ctxt Defs} ->

172 |                  {auto m : Ref MD Metadata} ->

173 |                  {auto u : Ref UST UState} ->

174 |                  {auto s : Ref Syn SyntaxInfo} ->

175 |                  {auto o : Ref ROpts REPLOpts} ->

176 |                  FC -> SearchOpts -> Int ->

177 |                  List (Name, List ImpClause) ->

178 |                  Core (Search (List ImpClause))

179 |   tryAllSplits loc opts n [] = noResult

180 |   tryAllSplits loc opts n ((x, []) :: rest)

181 |       = tryAllSplits loc opts n rest

182 |   tryAllSplits loc opts n ((x, cs) :: rest)

183 |       = do log "interaction.generate" 5 $ "Splitting on " ++ show x

184 |            trySearch (do cs' <- traverse (mkSplits loc opts n) cs

185 |                          collectClauses cs')

186 |                      (tryAllSplits loc opts n rest)

188 |   mkSplits : {auto c : Ref Ctxt Defs} ->

189 |              {auto m : Ref MD Metadata} ->

190 |              {auto u : Ref UST UState} ->

191 |              {auto s : Ref Syn SyntaxInfo} ->

192 |              {auto o : Ref ROpts REPLOpts} ->

193 |              FC -> SearchOpts -> Int -> ImpClause ->

194 |              Core (Search (List ImpClause))

195 |   -- If the clause works, use it. Otherwise, split on one of the splittable

196 |   -- variables and try all of the resulting clauses

197 |   mkSplits loc opts n c

198 |       = trySearch

199 |           (if mustSplit opts

200 |               then noResult

201 |               else expandClause loc opts n c)

202 |           (do cs <- generateSplits loc opts n c

203 |               log "interaction.generate" 5 $ "Splits: " ++ show cs

204 |               tryAllSplits loc ({ mustSplit := False,

205 |                                   doneSplit := True } opts) n cs)

208 | makeDefFromType : {auto c : Ref Ctxt Defs} ->

209 |                   {auto m : Ref MD Metadata} ->

210 |                   {auto u : Ref UST UState} ->

211 |                   {auto s : Ref Syn SyntaxInfo} ->

212 |                   {auto o : Ref ROpts REPLOpts} ->

213 |                   FC ->

214 |                   SearchOpts ->

215 |                   Name -> -- function name to generate

216 |                   Nat -> -- number of arguments

217 |                   ClosedTerm -> -- type of function

218 |                   Core (Search (FC, List ImpClause))

219 | makeDefFromType loc opts n envlen ty

220 |     = tryUnify

221 |          (do defs <- branch

222 |              meta <- get MD

223 |              ust <- get UST

224 |              argns <- getEnvArgNames defs envlen !(nf defs Env.empty ty)

225 |              -- Need to add implicit patterns for the outer environment.

226 |              -- We won't try splitting on these

227 |              let pre_env = replicate envlen (Implicit loc True)

229 |              rhshole <- uniqueHoleName defs [] (fnName False n ++ "_rhs")

230 |              let initcs = PatClause loc

231 |                                 (apply (IVar loc n) (pre_env ++ (map (IBindVar loc . UN . Basic) argns)))

232 |                                 (IHole loc rhshole)

233 |              let Just nidx = getNameID n (gamma defs)

234 |                  | Nothing => undefinedName loc n

235 |              cs' <- mkSplits loc opts nidx initcs

236 |              -- restore the global state, given that we've fiddled with it a lot!

237 |              put Ctxt defs

238 |              put MD meta

239 |              put UST ust

240 |              pure (map (\c => (loc, c)) cs'))

241 |          noResult

244 | makeDef : {auto c : Ref Ctxt Defs} ->

245 |           {auto m : Ref MD Metadata} ->

246 |           {auto u : Ref UST UState} ->

247 |           {auto s : Ref Syn SyntaxInfo} ->

248 |           {auto o : Ref ROpts REPLOpts} ->

249 |           (NonEmptyFC -> (Name, Nat, ClosedTerm) -> Bool) ->

250 |           Name -> Core (Search (FC, List ImpClause))

251 | makeDef p n

252 |     = do Just (loc, nidx, envlen, ty) <- findTyDeclAt p

253 |             | Nothing => noResult

254 |          n <- getFullName nidx

255 |          logTerm "interaction.generate" 5 ("Searching for " ++ show n) ty

256 |          let opts = { genExpr := Just (makeDefFromType (justFC loc)) }

257 |                            (initSearchOpts True 5)

258 |          makeDefFromType (justFC loc) opts n envlen ty

262 | bindableUsed : ImpClause -> Maybe (List Name, List Name)

263 | bindableUsed (PatClause fc lhs rhs)

264 |     = let lhsns = findIBindVars lhs

265 |           rhsns = findAllNames [] rhs in

266 |           Just (lhsns, filter (\x => x `elem` lhsns) rhsns)

267 | bindableUsed _ = Nothing

269 | propBindableUsed : List ImpClause -> Double

270 | propBindableUsed def

271 |     = let (b, u) = getProp def in

272 |           if b == Z

273 |              then 1.0

274 |              else the Double (cast u) / the Double (cast b)

275 |   where

276 |     getProp : List ImpClause -> (Nat, Nat)

277 |     getProp [] = (0, 0)

278 |     getProp (c :: xs)

279 |         = let (b, u) = getProp xs in

280 |               case bindableUsed c of

281 |                    Nothing => (b, u)

282 |                    Just (b', u') => (b + length (nub b'), u + length (nub u'))

289 | mostUsed : List ImpClause -> List ImpClause -> Ordering

290 | mostUsed def1 def2 = compare (propBindableUsed def2) (propBindableUsed def1)

293 | makeDefSort : {auto c : Ref Ctxt Defs} ->

294 |               {auto m : Ref MD Metadata} ->

295 |               {auto u : Ref UST UState} ->

296 |               {auto s : Ref Syn SyntaxInfo} ->

297 |               {auto o : Ref ROpts REPLOpts} ->

298 |               (NonEmptyFC -> (Name, Nat, ClosedTerm) -> Bool) ->

299 |               Nat -> (List ImpClause -> List ImpClause -> Ordering) ->

300 |               Name -> Core (Search (FC, List ImpClause))

301 | makeDefSort p max ord n

302 |     = searchSort max (makeDef p n) (\x, y => ord (snd x) (snd y))

305 | makeDefN : {auto c : Ref Ctxt Defs} ->

306 |            {auto m : Ref MD Metadata} ->

307 |            {auto u : Ref UST UState} ->

308 |            {auto s : Ref Syn SyntaxInfo} ->

309 |            {auto o : Ref ROpts REPLOpts} ->

310 |            (NonEmptyFC -> (Name, Nat, ClosedTerm) -> Bool) ->

311 |            Nat -> Name -> Core (List (FC, List ImpClause))

312 | makeDefN p max n

313 |     = do (res, _) <- searchN max (makeDef p n)

314 |          pure res