@@ -315,64 +315,58 @@ elab ist info pattern tcgen fn tm
315315 Just xs@(_:_) -> NS n xs
316316 _ -> n
317317
318+ -- if f is local, just do a simple_app
318319 elab' (ina, g) tm@(PApp fc (PRef _ f) args')
319320 = do let args = {- case lookupCtxt f (inblock info) of
320321 Just ps -> (map (pexp . (PRef fc)) ps ++ args')
321322 _ ->-} args'
322323-- newtm <- mkSpecialised ist fc f (map getTm args') tm
323− ivs <- get_instances
324− ps <- get_probs
325− -- HACK: we shouldn't resolve type classes if we're defining an instance
326− -- function or default definition.
327− let isinf = f == inferCon || tcname f
328− -- if f is a type class, we need to know its arguments so that
329− -- we can unify with them
330− case lookupCtxt Nothing f (idris_classes ist) of
331− [] -> return ()
332− _ -> mapM_ setInjective (map getTm args')
333− ctxt <- get_context
334− let guarded = isConName Nothing f ctxt
335−-- when True
336− (ns, committed) <- tryWhen False
337− (do 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
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
331+ do ivs <- get_instances
332+ ps <- get_probs
333+ -- HACK: we shouldn't resolve type classes if we're defining an instance
334+ -- function or default definition.
335+ let isinf = f == inferCon || tcname f
336+ -- if f is a type class, we need to know its arguments so that
337+ -- we can unify with them
338+ case lookupCtxt Nothing f (idris_classes ist) of
339+ [] -> return ()
340+ _ -> mapM_ setInjective (map getTm args')
341+ ctxt <- get_context
342+ let guarded = isConName Nothing f ctxt
343+ ns <- apply (Var f) (map isph args)
344+ ptm <- get_term
345345 g <- goal
346346 let (ns', eargs) = unzip $
347347 sortBy (\(_,x) (_,y) ->
348348 compare (priority x) (priority y))
349349 (zip ns args)
350− tryWhen False
351− (elabArgs (ina || not isinf, guarded)
352− [] 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)))
350+ elabArgs (ina || not isinf, guarded)
351+ [] False ns' (map (\x -> (lazyarg x, getTm x)) eargs)
356352 mkSpecialised ist fc f (map getTm args') tm
357353 solve
358− ptm <- get_term
359−-- elog (show ptm)
360− ivs' <- get_instances
361− ps' <- get_probs
354+ ptm <- get_term
355+ ivs' <- get_instances
356+ ps' <- get_probs
362357 -- Attempt to resolve any type classes which have 'complete' types,
363358 -- i.e. no holes in them
364− when (not pattern || (ina && not tcgen)) $
365− mapM_ (\n -> do focus n
366− g <- goal
367− env <- get_env
368− hs <- get_holes
369− if all (\n -> not (n `elem` hs)) (freeNames g)
370− -- let insts = filter tcname $ map fst (ctxtAlist (tt_ctxt ist))
371− then try (resolveTC 7 fn ist)
372− (movelast n)
373− else movelast n)
374− (ivs' \\ ivs)
375−-- ivs'
359+ when (not pattern || (ina && not tcgen)) $
360+ mapM_ (\n -> do focus n
361+ g <- goal
362+ env <- get_env
363+ hs <- get_holes
364+ if all (\n -> not (n `elem` hs)) (freeNames g)
365+ -- let insts = filter tcname $ map fst (ctxtAlist (tt_ctxt ist))
366+ then try (resolveTC 7 fn ist)
367+ (movelast n)
368+ else movelast n)
369+ (ivs' \\ ivs)
376370 where tcArg (n, PConstraint _ _ Placeholder _) = True
377371 tcArg _ = False
378372
@@ -386,8 +380,7 @@ elab ist info pattern tcgen fn tm
386380
387381 elab' ina@(_, a) (PApp fc f [arg])
388382 = 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))
391384 solve
392385 elab' ina Placeholder = do (h : hs) <- get_holes
393386 movelast h