0 | module TTImp.Elab.Ambiguity

  2 | import Core.Env

  3 | import Core.Metadata

  4 | import Core.Unify

  5 | import Core.Value

  7 | import Idris.REPL.Opts

  8 | import Idris.Syntax

 10 | import TTImp.Elab.Check

 11 | import TTImp.Elab.Delayed

 12 | import TTImp.TTImp

 14 | import Data.String

 15 | import Data.Vect

 17 | import Libraries.Data.UserNameMap

 18 | import Libraries.Data.WithDefault

 20 | %default covering

 23 | expandAmbigName : {vars : _} ->

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

 25 |                   {auto e : Ref EST (EState vars)} ->

 26 |                   ElabMode -> NestedNames vars -> Env Term vars -> RawImp ->

 27 |                   List (FC, Maybe (Maybe Name), RawImp) ->

 28 |                   RawImp -> Maybe (Glued vars) -> Core RawImp

 29 | expandAmbigName (InLHS _) nest env orig args (IBindVar fc n) exp

 30 |     = do est <- get EST

 31 |          if n `elem` lhsPatVars est

 32 |             then pure $ IMustUnify fc NonLinearVar orig

 33 |             else pure $ orig

 34 | expandAmbigName mode nest env orig args (IVar fc x) exp

 35 |    = case lookup x (names nest) of

 36 |           Just _ => do log "elab.ambiguous" 20 $ "Nested " ++ show x

 37 |                        pure orig

 38 |           Nothing => do

 39 |              defs <- get Ctxt

 40 |              case defined x env of

 41 |                   Just _ =>

 42 |                     if isNil args || notLHS mode

 43 |                        then do log "elab.ambiguous" 20 $ "Defined in env " ++ show x

 44 |                                pure $ orig

 45 |                        else pure $ IMustUnify fc VarApplied orig

 46 |                   Nothing =>

 47 |                      do est <- get EST

 48 |                         primNs <- getPrimNames

 49 |                         let prims = primNamesToList primNs

 50 |                         let primApp = isPrimName prims x

 51 |                         case lookupUN (userNameRoot x) (unambiguousNames est) of

 52 |                           Just xr => do

 53 |                             log "elab.ambiguous" 50 $ "unambiguous: " ++ show (fst xr)

 54 |                             pure $ mkAlt primApp est xr

 55 |                           Nothing => do

 56 |                             ns <- lookupCtxtName x (gamma defs)

 57 |                             ns' <- filterM visible ns

 58 |                             case ns' of

 59 |                                [] => do log "elab.ambiguous" 50 $ "Failed to find " ++ show orig

 60 |                                         pure orig

 61 |                                [nalt] =>

 62 |                                      do log "elab.ambiguous" 40 $ "Only one " ++ show (fst nalt)

 63 |                                         pure $ mkAlt primApp est nalt

 64 |                                nalts =>

 65 |                                      do log "elab.ambiguous" 10 $

 66 |                                           "Ambiguous: " ++ joinBy ", " (map (show . fst) nalts)

 67 |                                         pure $ IAlternative fc

 68 |                                                       (uniqType x args primNs)

 69 |                                                       (map (mkAlt primApp est) nalts)

 70 |   where

 71 |     lookupUN : Maybe UserName -> UserNameMap a -> Maybe a

 72 |     lookupUN Nothing _ = Nothing

 73 |     lookupUN (Just n) sm = lookup n sm

 75 |     visible : (Name, Int, GlobalDef) -> Core Bool

 76 |     visible (n, i, def)

 77 |         = do let NS ns x = fullname def

 78 |                  | _ => pure True

 79 |              if !(isVisible ns)

 80 |                 then pure $ visibleInAny (!getNS :: !getNestedNS) (NS ns x)

 81 |                                          (collapseDefault $ visibility def)

 82 |                 else pure False

 84 |     -- If there's multiple alternatives and all else fails, resort to using

 85 |     -- the primitive directly

 86 |     -- The order of the arguments have a big effect on case-tree size

 87 |     uniqType : Name -> List (FC, Maybe (Maybe Name), RawImp) -> PrimNames -> AltType

 88 |     uniqType n [(_, _, IPrimVal fc (BI x))] (MkPrimNs (Just fi) _ _ _ _ _ _)

 89 |         = UniqueDefault (IPrimVal fc (BI x))

 90 |     uniqType n [(_, _, IPrimVal fc (Str x))] (MkPrimNs _ (Just si) _ _ _ _ _)

 91 |         = UniqueDefault (IPrimVal fc (Str x))

 92 |     uniqType n [(_, _, IPrimVal fc (Ch x))] (MkPrimNs _ _ (Just ci) _ _ _ _)

 93 |         = UniqueDefault (IPrimVal fc (Ch x))

 94 |     uniqType n [(_, _, IPrimVal fc (Db x))] (MkPrimNs _ _ _ (Just di) _ _ _)

 95 |         = UniqueDefault (IPrimVal fc (Db x))

 96 |     uniqType n [(_, _, IQuote fc tm)] (MkPrimNs _ _ _ _ (Just dt) _ _)

 97 |         = UniqueDefault (IQuote fc tm)

 98 |         {-

104 |     uniqType _ _ _ = Unique

106 |     buildAlt : RawImp -> List (FC, Maybe (Maybe Name), RawImp) ->

107 |                RawImp

108 |     buildAlt f [] = f

109 |     buildAlt f ((fc', Nothing, a) :: as)

110 |         = buildAlt (IApp fc' f a) as

111 |     buildAlt f ((fc', Just Nothing, a) :: as)

112 |         = buildAlt (IAutoApp fc' f a) as

113 |     buildAlt f ((fc', Just (Just i), a) :: as)

114 |         = buildAlt (INamedApp fc' f i a) as

116 |     -- If it's not a constructor application, dot it

117 |     wrapDot : Bool -> EState vars ->

118 |               ElabMode -> Name -> List RawImp -> Def -> RawImp -> RawImp

119 |     wrapDot _ _ _ _ _ (DCon {}) tm = tm

120 |     wrapDot _ _ _ _ _ (TCon {}) tm = tm

121 |     -- Leave primitive applications alone, because they'll be inlined

122 |     -- before compiling the case tree

123 |     wrapDot prim est (InLHS _) n' [arg] _ tm

124 |        = if n' == Resolved (defining est) || prim

125 |             then tm

126 |             else IMustUnify fc NotConstructor tm

127 |     wrapDot prim est (InLHS _) n' _ _ tm

128 |        = if n' == Resolved (defining est)

129 |             then tm

130 |             else IMustUnify fc NotConstructor tm

131 |     wrapDot _ _ _ _ _ _ tm = tm

133 |     notLHS : ElabMode -> Bool

134 |     notLHS (InLHS _) = False

135 |     notLHS _ = True

137 |     mkTerm : Bool -> EState vars -> Name -> GlobalDef -> RawImp

138 |     mkTerm prim est n def

139 |         = if (Context.Macro `elem` flags def) && notLHS mode

140 |              then alternativeFirstSuccess $ reverse $

141 |                     allSplits args <&> \(macroArgs, extArgs) =>

142 |                       (IRunElab fc False $ ICoerced fc $ IVar fc n `buildAlt` macroArgs) `buildAlt` extArgs

143 |              else wrapDot prim est mode n (map (snd . snd) args)

144 |                     (definition def) (buildAlt (IVar fc n) args)

145 |       where

146 |         -- All splits of the original list starting from the (empty, full) finishing with (full, empty)

147 |         allSplits : (l : List a) -> Vect (S $ length l) (List a, List a)

148 |         allSplits []           = [([], [])]

149 |         allSplits full@(x::xs) = ([], full) :: (mapFst (x::) <$> allSplits xs)

151 |         alternativeFirstSuccess : forall n. Vect (S n) RawImp -> RawImp

152 |         alternativeFirstSuccess [x] = x

153 |         alternativeFirstSuccess xs  = IAlternative fc FirstSuccess $ toList xs

155 |     mkAlt : Bool -> EState vars -> (Name, Int, GlobalDef) -> RawImp

156 |     mkAlt prim est (fullname, i, gdef)

157 |         = mkTerm prim est (Resolved i) gdef

159 | expandAmbigName mode nest env orig args (IApp fc f a) exp

160 |     = expandAmbigName mode nest env orig

161 |                       ((fc, Nothing, a) :: args) f exp

162 | expandAmbigName mode nest env orig args (INamedApp fc f n a) exp

163 |     = expandAmbigName mode nest env orig

164 |                       ((fc, Just (Just n), a) :: args) f exp

165 | expandAmbigName mode nest env orig args (IAutoApp fc f a) exp

166 |     = expandAmbigName mode nest env orig

167 |                       ((fc, Just Nothing, a) :: args) f exp

168 | expandAmbigName elabmode nest env orig args tm exp

169 |     = do log "elab.ambiguous" 50 $ "No ambiguity " ++ show orig

170 |          pure orig

172 | stripDelay : NF vars -> NF vars

173 | stripDelay (NDelayed fc r t) = stripDelay t

174 | stripDelay tm = tm

176 | data TypeMatch = Concrete | Poly | NoMatch

178 | Show TypeMatch where

179 |   show Concrete = "Concrete"

180 |   show Poly = "Poly"

181 |   show NoMatch = "NoMatch"

184 |   mightMatchD : {auto c : Ref Ctxt Defs} ->

185 |                 {vars : _} ->

186 |                 Defs -> NF vars -> ClosedNF -> Core TypeMatch

187 |   mightMatchD defs l r

188 |       = mightMatch defs (stripDelay l) (stripDelay r)

190 |   mightMatchArg : {auto c : Ref Ctxt Defs} ->

191 |                   {vars : _} ->

192 |                   Defs ->

193 |                   Closure vars -> ClosedClosure ->

194 |                   Core Bool

195 |   mightMatchArg defs l r

196 |       = pure $ case !(mightMatchD defs !(evalClosure defs l) !(evalClosure defs r)) of

197 |              NoMatch => False

198 |              _ => True

200 |   mightMatchArgs : {auto c : Ref Ctxt Defs} ->

201 |                    {vars : _} ->

202 |                    Defs ->

203 |                    Scopeable (Closure vars) -> Scopeable ClosedClosure ->

204 |                    Core Bool

205 |   mightMatchArgs defs [] [] = pure True

206 |   mightMatchArgs defs (x :: xs) (y :: ys)

207 |       = do amatch <- mightMatchArg defs x y

208 |            if amatch

209 |               then mightMatchArgs defs xs ys

210 |               else pure False

211 |   mightMatchArgs _ _ _ = pure False

213 |   mightMatch : {auto c : Ref Ctxt Defs} ->

214 |                {vars : _} ->

215 |                Defs -> NF vars -> ClosedNF -> Core TypeMatch

216 |   mightMatch defs target (NBind fc n (Pi {}) sc)

217 |       = mightMatchD defs target !(sc defs (toClosure defaultOpts Env.empty (Erased fc Placeholder)))

218 |   mightMatch defs (NBind {}) (NBind {}) = pure Poly -- lambdas might match

219 |   mightMatch defs (NTCon _ n a args) (NTCon _ n' a' args')

220 |       = if n == n'

221 |            then do amatch <- mightMatchArgs defs (map snd args) (map snd args')

222 |                    if amatch then pure Concrete else pure NoMatch

223 |            else pure NoMatch

224 |   mightMatch defs (NDCon _ n t a args) (NDCon _ n' t' a' args')

225 |       = if t == t'

226 |            then do amatch <- mightMatchArgs defs (map snd args) (map snd args')

227 |                    if amatch then pure Concrete else pure NoMatch

228 |            else pure NoMatch

229 |   mightMatch defs (NPrimVal _ x) (NPrimVal _ y)

230 |       = if x == y then pure Concrete else pure NoMatch

231 |   mightMatch defs (NType {}) (NType {}) = pure Concrete

232 |   mightMatch defs (NApp {}) _ = pure Poly

233 |   mightMatch defs (NErased {}) _ = pure Poly

234 |   mightMatch defs _ (NApp {}) = pure Poly

235 |   mightMatch defs _ (NErased {}) = pure Poly

236 |   mightMatch _ _ _ = pure NoMatch

239 | couldBeName : {auto c : Ref Ctxt Defs} ->

240 |               {vars : _} ->

241 |               Defs -> NF vars -> Name -> Core TypeMatch

242 | couldBeName defs target n

243 |     = case !(lookupTyExact n (gamma defs)) of

244 |            Nothing => pure Poly -- could be a local name, don't rule it out

245 |            Just ty => mightMatchD defs target !(nf defs Env.empty ty)

247 | couldBeFn : {auto c : Ref Ctxt Defs} ->

248 |             {vars : _} ->

249 |             Defs -> NF vars -> RawImp -> Core TypeMatch

250 | couldBeFn defs ty (IVar _ n) = couldBeName defs ty n

251 | couldBeFn defs ty (IAlternative {}) = pure Concrete

252 | couldBeFn defs ty _ = pure Poly

258 | couldBe : {auto c : Ref Ctxt Defs} ->

259 |           {vars : _} ->

260 |           Defs -> NF vars -> RawImp -> Core (Maybe (Bool, RawImp))

261 | couldBe {vars} defs ty@(NTCon _ n _ _) app

262 |    = case !(couldBeFn {vars} defs ty (getFn app)) of

263 |           Concrete => pure $ Just (True, app)

264 |           Poly => pure $ Just (False, app)

265 |           NoMatch => pure Nothing

266 | couldBe {vars} defs ty@(NPrimVal {}) app

267 |    = case !(couldBeFn {vars} defs ty (getFn app)) of

268 |           Concrete => pure $ Just (True, app)

269 |           Poly => pure $ Just (False, app)

270 |           NoMatch => pure Nothing

271 | couldBe {vars} defs ty@(NType {}) app

272 |    = case !(couldBeFn {vars} defs ty (getFn app)) of

273 |           Concrete => pure $ Just (True, app)

274 |           Poly => pure $ Just (False, app)

275 |           NoMatch => pure Nothing

276 | couldBe defs ty app = pure $ Just (False, app)

279 | notOverloadable : Defs -> (Bool, RawImp) -> Core Bool

280 | notOverloadable defs (True, fn) = pure True

281 | notOverloadable defs (concrete, fn) = notOverloadableFn (getFn fn)

282 |   where

283 |     notOverloadableFn : RawImp -> Core Bool

284 |     notOverloadableFn (IVar _ n)

285 |         = do Just gdef <- lookupCtxtExact n (gamma defs)

286 |                   | Nothing => pure True

287 |              pure False -- If the name exists, and doesn't have a concrete type

288 |                         -- but another possibility does, remove it from the set

289 |                         -- no matter what

290 |                         -- (TODO: Consider whether %allow_overloads should exist)

291 |                         -- (not (Overloadable `elem` flags gdef))

292 |     notOverloadableFn _ = pure True

294 | filterCore : (a -> Core Bool) -> List a -> Core (List a)

295 | filterCore f [] = pure []

296 | filterCore f (x :: xs)

297 |     = do p <- f x

298 |          xs' <- filterCore f xs

299 |          if p then pure (x :: xs')

300 |               else pure xs'

302 | pruneByType : {vars : _} ->

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

304 |               Env Term vars -> NF vars -> List RawImp ->

305 |               Core (List RawImp)

306 | pruneByType env target alts

307 |     = do defs <- get Ctxt

308 |          matches_in <- traverse (couldBe defs (stripDelay target)) alts

309 |          let matches = mapMaybe id matches_in

310 |          logNF "elab.prune" 10 "Prune by" env target

311 |          log "elab.prune" 10 (show matches)

312 |          res <- if any Builtin.fst matches

313 |                 -- if there's any concrete matches, drop the non-concrete

314 |                 -- matches marked as '%allow_overloads' from the possible set

315 |                    then do keep <- filterCore (notOverloadable defs) matches

316 |                            log "elab.prune" 10 $ "Keep " ++ show keep

317 |                            pure (map snd keep)

318 |                    else pure (map snd matches)

319 |          if isNil res

320 |             then pure alts -- if none of them work, better to show all the errors

321 |             else pure res

323 | checkAmbigDepth : {auto c : Ref Ctxt Defs} ->

324 |                   {auto e : Ref EST (EState vars)} ->

325 |                   FC -> ElabInfo -> Core ()

326 | checkAmbigDepth fc info

327 |     = do max <- getAmbigLimit

328 |          let ambs = ambigTries info

329 |          when (length ambs > max) $

330 |            do est <- get EST

331 |               throw (AmbiguityTooDeep fc (Resolved (defining est)) ambs)

333 | getName : RawImp -> Maybe Name

334 | getName (IVar _ n) = Just n

335 | getName (IApp _ f _) = getName f

336 | getName (INamedApp _ f _ _) = getName f

337 | getName (IAutoApp _ f _) = getName f

338 | getName _ = Nothing

341 | addAmbig : List alts -> Maybe Name -> ElabInfo -> ElabInfo

342 | addAmbig _ Nothing = id

343 | addAmbig [] _ = id

344 | addAmbig [_] _ = id

345 | addAmbig _ (Just n) = { ambigTries $= (n ::) }

348 | checkAlternative : {vars : _} ->

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

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

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

352 |                    {auto e : Ref EST (EState vars)} ->

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

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

355 |                    RigCount -> ElabInfo ->

356 |                    NestedNames vars -> Env Term vars ->

357 |                    FC -> AltType -> List RawImp -> Maybe (Glued vars) ->

358 |                    Core (Term vars, Glued vars)

359 | checkAlternative rig elabinfo nest env fc (UniqueDefault def) alts mexpected

360 |     = do checkAmbigDepth fc elabinfo

361 |          expected <- maybe (do nm <- genName "altTy"

362 |                                u <- uniVar fc

363 |                                ty <- metaVar fc erased env nm (TType fc u)

364 |                                pure (gnf env ty))

365 |                            pure mexpected

366 |          let solvemode = case elabMode elabinfo of

367 |                               InLHS c => inLHS

368 |                               _ => inTerm

369 |          delayOnFailure fc rig env (Just expected) ambiguous Ambiguity $

370 |              \delayed =>

371 |                do solveConstraints solvemode Normal

372 |                   exp <- getTerm expected

374 |                   -- We can't just use the old NF on the second attempt,

375 |                   -- because we might know more now, so recalculate it

376 |                   let exp' = if delayed

377 |                                 then gnf env exp

378 |                                 else expected

380 |                   logGlueNF "elab.ambiguous" 5 (fastConcat

381 |                     [ "Ambiguous elaboration at ", show fc, ":\n"

382 |                     , unlines (map (("  " ++) . show) alts)

383 |                     , "With default. Target type "

384 |                     ]) env exp'

385 |                   alts' <- pruneByType env !(getNF exp') alts

386 |                   log "elab.prune" 5 $

387 |                     "Pruned " ++ show (minus (length alts) (length alts')) ++ " alts."

388 |                     ++ " Kept:\n" ++ unlines (map show alts')

390 |                   if delayed -- use the default if there's still ambiguity

391 |                      then try

392 |                             (exactlyOne' False fc env

393 |                                 (map (\t =>

394 |                                    (getName t,

395 |                                     checkImp rig (addAmbig alts' (getName t) elabinfo)

396 |                                              nest env t

397 |                                              (Just exp'))) alts'))

398 |                             (do log "elab.ambiguous" 5 "All failed, running default"

399 |                                 checkImp rig (addAmbig alts' (getName def) elabinfo)

400 |                                              nest env def (Just exp'))

401 |                      else exactlyOne' True fc env

402 |                            (map (\t =>

403 |                              (getName t,

404 |                               checkImp rig (addAmbig alts' (getName t) elabinfo)

405 |                                        nest env t (Just exp')))

406 |                               alts')

407 | checkAlternative rig elabinfo nest env fc uniq alts mexpected

408 |     = do checkAmbigDepth fc elabinfo

409 |          alts' <- maybe (Core.pure [])

410 |                         (\exp => pruneByType env !(getNF exp) alts) mexpected

411 |          case alts' of

412 |            [alt] => checkImp rig elabinfo nest env alt mexpected

413 |            _ =>

414 |              do expected <- maybe (do nm <- genName "altTy"

415 |                                       u <- uniVar fc

416 |                                       ty <- metaVar fc erased env nm (TType fc u)

417 |                                       pure (gnf env ty))

418 |                                   pure mexpected

419 |                 let solvemode = case elabMode elabinfo of

420 |                                       InLHS c => inLHS

421 |                                       _ => inTerm

422 |                 delayOnFailure fc rig env (Just expected) ambiguous Ambiguity $

423 |                      \delayed =>

424 |                        do exp <- getTerm expected

426 |                           -- We can't just use the old NF on the second attempt,

427 |                           -- because we might know more now, so recalculate it

428 |                           let exp' = if delayed

429 |                                         then gnf env exp

430 |                                         else expected

432 |                           alts' <- pruneByType env !(getNF exp') alts

434 |                           logGlueNF "elab.ambiguous" 5 (fastConcat

435 |                               [ "Ambiguous elaboration"

436 |                               , " (kept ", show (length alts'), " out of "

437 |                               , show (length alts), " candidates)"

438 |                               , " (", if delayed then "" else "not ", "delayed)"

439 |                               , " at ", show fc, ":\n"

440 |                               , unlines (map show alts')

441 |                               , "Target type "

442 |                               ]) env exp'

443 |                           let tryall = case uniq of

444 |                                             FirstSuccess => anyOne fc

445 |                                             _ => exactlyOne' (not delayed) fc env

446 |                           tryall (map (\t =>

447 |                               (getName t,

448 |                                do res <- checkImp rig (addAmbig alts' (getName t) elabinfo)

449 |                                                   nest env t (Just exp')

450 |                                   -- Do it twice for interface resolution;

451 |                                   -- first pass gets the determining argument

452 |                                   -- (maybe rethink this, there should be a better

453 |                                   -- way that allows one pass)

454 |                                   solveConstraints solvemode Normal

455 |                                   solveConstraints solvemode Normal

456 |                                   log "elab.ambiguous" 10 $ show (getName t) ++ " success"

457 |                                   logTermNF "elab.ambiguous" 10 "Result" env (fst res)

458 |                                   pure res)) alts')