0 | module TTImp.Interactive.CaseSplit

  2 | import Core.Env

  3 | import Core.Metadata

  4 | import Core.UnifyState

  5 | import Core.Value

  7 | import Idris.REPL.Opts

  8 | import Idris.Syntax

 10 | import TTImp.Elab

 11 | import TTImp.Elab.Check

 12 | import TTImp.ProcessDef

 13 | import TTImp.TTImp

 14 | import TTImp.TTImp.Functor

 15 | import TTImp.Unelab

 16 | import TTImp.Utils

 18 | %default covering

 24 | public export

 25 | data ClauseUpdate : Type where

 26 |      Valid : RawImp -> List (Name, RawImp) -> ClauseUpdate

 27 |      Impossible : RawImp -> ClauseUpdate

 28 |      Invalid : ClauseUpdate

 32 | Show ClauseUpdate where

 33 |   show (Valid lhs updates) = "Valid: " ++ show lhs ++ "\n" ++ "Updates: " ++ show updates

 34 |   show (Impossible lhs) = "Impossible: " ++ show lhs

 35 |   show Invalid = "Invalid"

 37 | public export

 38 | data SplitError : Type where

 39 |      NoValidSplit : SplitError -- None of the splits either type check, or fail

 40 |                                -- in a way which is valid as an 'impossible' case

 41 |      CantSplitThis : Name -> String -> SplitError -- Request to split was not on a splittable variable

 42 |      CantFindLHS : SplitError -- Can't find any clause to split

 45 | Show SplitError where

 46 |   show NoValidSplit = "No valid case splits"

 47 |   show (CantSplitThis n r) = "Can't split on " ++ show n ++ " (" ++ r ++ ")"

 48 |   show CantFindLHS = "No clause to split here"

 50 | public export

 51 | data SplitResult : Type -> Type where

 52 |      SplitFail : SplitError -> SplitResult a

 53 |      OK : a -> SplitResult a

 56 | Show a => Show (SplitResult a) where

 57 |   show (SplitFail err) = "Split error: " ++ show err

 58 |   show (OK res) = "OK: " ++ show res

 60 | findTyName : {vars : _} ->

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

 62 |              Defs -> Env Term vars -> Name -> Term vars ->

 63 |              Core (Maybe Name)

 64 | findTyName defs env n (Bind _ x b@(PVar _ c p ty) sc)

 65 |       -- Take the first one, which is the most recently bound

 66 |     = if n == x

 67 |          then do tynf <- nf defs env ty

 68 |                  case tynf of

 69 |                       NTCon _ tyn _ _ => pure $ Just tyn

 70 |                       _ => pure Nothing

 71 |          else findTyName defs (b :: env) n sc

 72 | findTyName defs env n (Bind _ x b sc) = findTyName defs (b :: env) n sc

 73 | findTyName _ _ _ _ = pure Nothing

 75 | getDefining : Term vars -> Maybe Name

 76 | getDefining (Bind _ _ _ sc) = getDefining sc

 77 | getDefining tm

 78 |     = case getFn tm of

 79 |            Ref _ _ fn => Just fn

 80 |            _ => Nothing

 84 | findCons : {auto c : Ref Ctxt Defs} ->

 85 |            Name -> ClosedTerm -> Core (SplitResult (Name, Name, List Name))

 86 | findCons n lhs

 87 |     = case getDefining lhs of

 88 |            Nothing => pure (SplitFail

 89 |                             (CantSplitThis n "Can't find function name on LHS"))

 90 |            Just fn =>

 91 |               do defs <- get Ctxt

 92 |                  case !(findTyName defs Env.empty n lhs) of

 93 |                       Nothing => pure (SplitFail (CantSplitThis n

 94 |                                          ("Can't find type of " ++ show n ++ " in LHS")))

 95 |                       Just tyn =>

 96 |                           do Just (TCon _ _ _ _ _ cons _) <-

 97 |                                       lookupDefExact tyn (gamma defs)

 98 |                                 | res => pure (SplitFail

 99 |                                             (CantSplitThis n

100 |                                                ("Not a type constructor " ++

101 |                                                   show res)))

102 |                              pure (OK (fn, !(toFullNames tyn),

103 |                                            !(traverse toFullNames $ fromMaybe [] cons)))

105 | findAllVars : Term vars -> List Name

106 | findAllVars (Bind _ x (PVar {}) sc)

107 |     = x :: findAllVars sc

108 | findAllVars (Bind _ x (Let {}) sc)

109 |     = x :: findAllVars sc

110 | findAllVars (Bind _ x (PLet {}) sc)

111 |     = x :: findAllVars sc

113 | findAllVars t = toList (dropNS <$> getDefining t)

116 | explicitlyBound : Defs -> ClosedNF -> Core (List Name)

117 | explicitlyBound defs (NBind fc x (Pi {}) sc)

118 |     = pure $ x :: !(explicitlyBound defs

119 |                     !(sc defs (toClosure defaultOpts Env.empty (Erased fc Placeholder))))

120 | explicitlyBound defs _ = pure []

123 | getEnvArgNames : {auto c : Ref Ctxt Defs} ->

124 |                  Defs -> Nat -> ClosedNF -> Core (List String)

125 | getEnvArgNames defs Z sc = getArgNames defs !(explicitlyBound defs sc) [] Env.empty sc

126 | getEnvArgNames defs (S k) (NBind fc n _ sc)

127 |     = getEnvArgNames defs k !(sc defs (toClosure defaultOpts Env.empty (Erased fc Placeholder)))

128 | getEnvArgNames defs n ty = pure []

130 | expandCon : {auto c : Ref Ctxt Defs} ->

131 |             FC -> List Name -> Name -> Core RawImp

132 | expandCon fc usedvars con

133 |     = do defs <- get Ctxt

134 |          Just ty <- lookupTyExact con (gamma defs)

135 |               | Nothing => undefinedName fc con

136 |          pure (apply (IVar fc con)

137 |                 (map (IBindVar fc . UN . Basic)

138 |                      !(getArgNames defs [] usedvars Env.empty

139 |                                    !(nf defs Env.empty ty))))

141 | updateArg : {auto c : Ref Ctxt Defs} ->

142 |             List Name -> -- all the variable names

143 |             (var : Name) -> (con : Name) ->

144 |             RawImp -> Core RawImp

145 | updateArg allvars var con (IVar fc n)

146 |     = if n `elem` allvars

147 |          then if n == var

148 |                  then expandCon fc (filter (/= n) allvars) con

149 |                  else pure $ Implicit fc True

150 |          else pure $ IVar fc n

151 | updateArg allvars var con (IApp fc f a)

152 |     = pure $ IApp fc !(updateArg allvars var con f)

153 |                      !(updateArg allvars var con a)

154 | updateArg allvars var con (IWithApp fc f a)

155 |     = pure $ IWithApp fc !(updateArg allvars var con f)

156 |                          !(updateArg allvars var con a)

157 | updateArg allvars var con (IAutoApp fc f a)

158 |     = pure $ IAutoApp fc !(updateArg allvars var con f)

159 |                          !(updateArg allvars var con a)

160 | updateArg allvars var con (INamedApp fc f n a)

161 |     = pure $ INamedApp fc !(updateArg allvars var con f) n

162 |                           !(updateArg allvars var con a)

163 | updateArg allvars var con (IAs fc nameFC s n p)

164 |     = updateArg allvars var con p

165 | updateArg allvars var con tm = pure $ Implicit (getFC tm) True

167 | update : {auto c : Ref Ctxt Defs} ->

168 |          List Name -> -- all the variable names

169 |          (var : Name) -> (con : Name) ->

170 |          Arg -> Core Arg

171 | update allvars var con (Explicit fc arg)

172 |     = pure $ Explicit fc !(updateArg allvars var con arg)

173 | update allvars var con (Auto fc arg)

174 |     = pure $ Auto fc !(updateArg allvars var con arg)

175 | update allvars var con (Named fc n arg)

176 |     = pure $ Named fc n !(updateArg allvars var con arg)

181 | newLHS : {auto c : Ref Ctxt Defs} ->

182 |          FC ->

183 |          Nat -> -- previous environment length; leave these alone

184 |          List Name -> -- all the variable names

185 |          (var : Name) -> (con : Name) ->

186 |          RawImp -> Core RawImp

187 | newLHS fc envlen allvars var con tm

188 |     = do let (f, args) = getFnArgs tm []

189 |          let keep = map (const (Explicit fc (Implicit fc True)))

190 |                         (mapMaybe isExplicit $ take envlen args)

191 |          let ups = drop envlen args

192 |          ups' <- traverse (update allvars var con) ups

193 |          pure $ apply f (keep ++ ups')

195 | record Updates where

196 |   constructor MkUpdates

197 |   namemap : List (Name, Name)

198 |   updates : List (Name, RawImp)

200 | data UPD : Type where

202 | recordUpdate : {auto u : Ref UPD Updates} ->

203 |                FC -> Name -> RawImp -> Core ()

204 | recordUpdate fc n tm

205 |     = do u <- get UPD

206 |          let nupdates = mapSnd (IVar fc) <$> namemap u

207 |          put UPD ({ updates $= ((n, substNames [] nupdates tm) ::) } u)

209 | findUpdates : {auto u : Ref UPD Updates} ->

210 |               Defs -> RawImp -> RawImp -> Core ()

211 | findUpdates defs (IVar fc n) (IVar _ n')

212 |     = case !(lookupTyExact n' (gamma defs)) of

213 |            Just _ => recordUpdate fc n (IVar fc n')

214 |            Nothing =>

215 |               do u <- get UPD

216 |                  case lookup n' (namemap u) of

217 |                       Nothing => put UPD ({ namemap $= ((n', n) ::) } u)

218 |                       Just nm => put UPD ({ updates $= ((n, IVar fc nm) ::) } u)

219 | findUpdates defs (IVar fc n) tm = recordUpdate fc n tm

220 | findUpdates defs (IApp _ f a) (IApp _ f' a')

221 |     = do findUpdates defs f f'

222 |          findUpdates defs a a'

223 | findUpdates defs (IAutoApp _ f a) (IAutoApp _ f' a')

224 |     = do findUpdates defs f f'

225 |          findUpdates defs a a'

226 | findUpdates defs (IAutoApp _ f a) f'

227 |     = findUpdates defs f f'

228 | findUpdates defs f (IAutoApp _ f' a)

229 |     = findUpdates defs f f'

230 | findUpdates defs (INamedApp _ f _ a) (INamedApp _ f' _ a')

231 |     = do findUpdates defs f f'

232 |          findUpdates defs a a'

233 | findUpdates defs (INamedApp _ f _ a) f' = findUpdates defs f f'

234 | findUpdates defs f (INamedApp _ f' _ a) = findUpdates defs f f'

235 | findUpdates defs (IAs _ _ _ _ f) f' = findUpdates defs f f'

236 | findUpdates defs f (IAs _ _ _ _ f') = findUpdates defs f f'

237 | findUpdates _ _ _ = pure ()

239 | getUpdates : Defs -> RawImp -> RawImp -> Core (List (Name, RawImp))

240 | getUpdates defs orig updated

241 |     = do u <- newRef UPD (MkUpdates [] [])

242 |          findUpdates defs orig updated

243 |          pure (updates !(get UPD))

245 | mkCase : {auto c : Ref Ctxt Defs} ->

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

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

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

249 |          Int -> RawImp -> RawImp -> Core ClauseUpdate

250 | mkCase {c} {u} fn orig lhs_raw

251 |     = do m <- newRef MD (initMetadata $ Virtual Interactive)

252 |          defs <- get Ctxt

253 |          ust <- get UST

254 |          catch

255 |            (do

256 |                -- Fixes Issue #74. The problem is that if the function is defined in a sub module,

257 |                -- then the current namespace (accessed by calling getNS) differs from the function

258 |                -- namespace, therefore it is not considered visible by TTImp.Elab.App.checkVisibleNS

259 |                -- FIXME: Causes issue #1385

260 |                setAllPublic True

262 |                -- Use 'Rig0' since it might be a type level function, or it might

263 |                -- be an erased name in a case block (which will be bound elsewhere

264 |                -- once split and turned into a pattern)

265 |                (lhs, _) <- elabTerm {c} {m} {u}

266 |                                     fn (InLHS erased) [] (MkNested [])

267 |                                     Env.empty (IBindHere (getFC lhs_raw) PATTERN lhs_raw)

268 |                                     Nothing

269 |                -- Revert all public back to false

270 |                setAllPublic False

271 |                put Ctxt defs -- reset the context, we don't want any updates

272 |                put UST ust

273 |                lhs' <- map (map rawName) $ unelabNoSugar Env.empty lhs

275 |                log "interaction.casesplit" 3 $ "Original LHS: " ++ show orig

276 |                log "interaction.casesplit" 3 $ "New LHS: " ++ show lhs'

278 |                pure (Valid lhs' !(getUpdates defs orig lhs')))

279 |            (\err =>

280 |                do put Ctxt defs

281 |                   put UST ust

282 |                   case err of

283 |                        WhenUnifying _ gam env l r err

284 |                          => do let defs = { gamma := gam } defs

285 |                                if !(impossibleOK defs !(nf defs env l)

286 |                                                       !(nf defs env r))

287 |                                   then pure (Impossible lhs_raw)

288 |                                   else pure Invalid

289 |                        _ => pure Invalid)

291 | substLets : {vars : _} ->

292 |             Term vars -> Term vars

293 | substLets (Bind _ n (Let _ c val ty) sc) = substLets (subst val sc)

294 | substLets (Bind _ n (PLet _ c val ty) sc) = substLets (subst val sc)

295 | substLets (Bind fc n b sc) = Bind fc n b (substLets sc)

296 | substLets tm = tm

298 | combine : List ClauseUpdate -> List ClauseUpdate ->

299 |           SplitResult (List ClauseUpdate)

300 | combine [] [] = SplitFail NoValidSplit

301 | combine [] acc = OK (reverse acc)

302 | combine (Invalid :: xs) acc = combine xs acc

303 | combine (x :: xs) acc = combine xs (x :: acc)

306 | getSplitsLHS : {auto c : Ref Ctxt Defs} ->

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

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

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

310 |                FC -> Nat -> ClosedTerm -> Name ->

311 |                Core (SplitResult (List ClauseUpdate))

312 | getSplitsLHS fc envlen lhs_in n

313 |     = do let lhs = substLets lhs_in

314 |          logTerm "interaction.casesplit" 3 "Splitting" lhs_in

315 |          let usedns = findAllVars lhs_in

317 |          defs <- get Ctxt

319 |          OK (fn, tyn, cons) <- findCons n lhs

320 |             | SplitFail err => pure (SplitFail err)

322 |          rawlhs <- map (map rawName) $ unelabNoSugar Env.empty lhs

323 |          trycases <- traverse (\c => newLHS fc envlen usedns n c rawlhs) cons

325 |          let Just idx = getNameID fn (gamma defs)

326 |              | Nothing => undefinedName fc fn

327 |          cases <- traverse (mkCase idx rawlhs) trycases

328 |          log "interaction.casesplit" 3 $ "Found cases: " ++ show cases

330 |          pure (combine cases [])

333 | getSplits : {auto c : Ref Ctxt Defs} ->

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

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

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

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

338 |             (NonEmptyFC -> ClosedTerm -> Bool) -> Name ->

339 |             Core (SplitResult (List ClauseUpdate))

340 | getSplits p n

341 |     = do Just (loc, envlen, lhs_in) <- findLHSAt p

342 |               | Nothing => pure (SplitFail CantFindLHS)

343 |          getSplitsLHS (justFC loc) envlen lhs_in n