92257c4 · Idris-dev · git.iko.soy

315 Just xs@(_:_) -> NS n xs

316 _ -> n

317

318+ -- if f is local, just do a simple_app

318 elab' (ina, g) tm@(PApp fc (PRef _ f) args')

319 elab' (ina, g) tm@(PApp fc (PRef _ f) args')

319 = do let args = {- case lookupCtxt f (inblock info) of

320 = do let args = {- case lookupCtxt f (inblock info) of

320 Just ps -> (map (pexp . (PRef fc)) ps ++ args')

321 Just ps -> (map (pexp . (PRef fc)) ps ++ args')

321 _ ->-} args'

322 _ ->-} args'

322-- newtm <- mkSpecialised ist fc f (map getTm args') tm

323-- newtm <- mkSpecialised ist fc f (map getTm args') tm

324+ env <- get_env

325+ if (f `elem` map fst env && length args' == 1)

326+ then -- simple app, as below

327+ do simple_app (elabE (ina, g) (PRef fc f))

328+ (elabE (True, g) (getTm (head args')))

329+ solve

330+ else

323− ivs <- get_instances

331+ do ivs <- get_instances

324− ps <- get_probs

332+ ps <- get_probs

325− -- HACK: we shouldn't resolve type classes if we're defining an instance

333+ -- HACK: we shouldn't resolve type classes if we're defining an instance

326− -- function or default definition.

334+ -- function or default definition.

327− let isinf = f == inferCon || tcname f

335+ let isinf = f == inferCon || tcname f

328− -- if f is a type class, we need to know its arguments so that

336+ -- if f is a type class, we need to know its arguments so that

329− -- we can unify with them

337+ -- we can unify with them

330− case lookupCtxt Nothing f (idris_classes ist) of

338+ case lookupCtxt Nothing f (idris_classes ist) of

331− [] -> return ()

339+ [] -> return ()

332− _ -> mapM_ setInjective (map getTm args')

340+ _ -> mapM_ setInjective (map getTm args')

333− ctxt <- get_context

341+ ctxt <- get_context

334− let guarded = isConName Nothing f ctxt

342+ let guarded = isConName Nothing f ctxt

335−-- when True

336− (ns, committed) <- tryWhen False

337− (do ns <- apply (Var f) (map isph args)

343+ ns <- apply (Var f) (map isph args)

338− return (ns, True))

339− (do apply_elab f (map (toElab (ina || not isinf, guarded)) args)

340− mkSpecialised ist fc f (map getTm args') tm

341− solve

342− return ([], False))

343− when committed $

344− do ptm <- get_term

344+ ptm <- get_term

345 g <- goal

346 let (ns', eargs) = unzip $

347 sortBy (\(_,x) (_,y) ->

348 compare (priority x) (priority y))

349 (zip ns args)

350− tryWhen False

351− (elabArgs (ina || not isinf, guarded)

350+ elabArgs (ina || not isinf, guarded)

352− [] False ns' (map (\x -> (lazyarg x, getTm x)) eargs))

351+ [] False ns' (map (\x -> (lazyarg x, getTm x)) eargs)

353− (elabArgs (ina || not isinf, guarded)

354− [] False (reverse ns')

355− (map (\x -> (lazyarg x, getTm x)) (reverse eargs)))

356 mkSpecialised ist fc f (map getTm args') tm

352 mkSpecialised ist fc f (map getTm args') tm

357 solve

353 solve

358− ptm <- get_term

354+ ptm <- get_term

359−-- elog (show ptm)

360− ivs' <- get_instances

355+ ivs' <- get_instances

361− ps' <- get_probs

356+ ps' <- get_probs

362 -- Attempt to resolve any type classes which have 'complete' types,

357 -- Attempt to resolve any type classes which have 'complete' types,

363 -- i.e. no holes in them

358 -- i.e. no holes in them

364− when (not pattern || (ina && not tcgen)) $

359+ when (not pattern || (ina && not tcgen)) $

365− mapM_ (\n -> do focus n

360+ mapM_ (\n -> do focus n

366− g <- goal

361+ g <- goal

367− env <- get_env

362+ env <- get_env

368− hs <- get_holes

363+ hs <- get_holes

369− if all (\n -> not (n `elem` hs)) (freeNames g)

364+ if all (\n -> not (n `elem` hs)) (freeNames g)

370− -- let insts = filter tcname $ map fst (ctxtAlist (tt_ctxt ist))

365+ -- let insts = filter tcname $ map fst (ctxtAlist (tt_ctxt ist))

371− then try (resolveTC 7 fn ist)

366+ then try (resolveTC 7 fn ist)

372− (movelast n)

367+ (movelast n)

373− else movelast n)

368+ else movelast n)

374− (ivs' \\ ivs)

369+ (ivs' \\ ivs)

375−-- ivs'

376 where tcArg (n, PConstraint _ _ Placeholder _) = True

370 where tcArg (n, PConstraint _ _ Placeholder _) = True

377 tcArg _ = False

371 tcArg _ = False

378

372

386

380

387 elab' ina@(_, a) (PApp fc f [arg])

381 elab' ina@(_, a) (PApp fc f [arg])

388 = erun fc $

382 = erun fc $

389− do ptm <- get_term

390− simple_app (elabE ina f) (elabE (True, a) (getTm arg))

383+ do simple_app (elabE ina f) (elabE (True, a) (getTm arg))

391 solve

384 solve

392 elab' ina Placeholder = do (h : hs) <- get_holes

385 elab' ina Placeholder = do (h : hs) <- get_holes

393 movelast h

386 movelast h