f281f3c · Idris-dev · git.iko.soy

615-- elab' (_, _, inty) (PRef fc f)

616-- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty

617-- = lift $ tfail (Msg "Typecase is not allowed")

618− elab' ec _ tm@(PRef fc hl n)

618+ elab' ec fc' tm@(PRef fc hls n)

619 | pattern && not reflection && not (e_qq ec) && not (e_intype ec)

620 && isTConName n (tt_ctxt ist)

621 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)

628 guarded = e_guarded ec

629 inty = e_intype ec

630 ctxt <- get_context

631+ env <- get_env

631

632

633+ -- If the name is defined, globally or locally, elaborate it

634+ -- as a reference, otherwise it might end up as a pattern var.

632 let defined = case lookupTy n ctxt of

635 let defined = case lookupTy n ctxt of

636+ [] -> case lookupTyEnv n env of

637+ Just _ -> True

633− [] -> False

638+ _ -> False

634 _ -> True

639 _ -> True

640+

635− -- this is to stop us resolve interfaces recursively

641+ -- this is to stop us resolving interfaces recursively

636− -- trace (show (n, guarded)) $

637 if (tcname n && ina && not intransform)

642 if (tcname n && ina && not intransform)

638 then erun fc $

643 then erun fc $

639 do patvar n

644 do patvar n

640 update_term liftPats

645 update_term liftPats

641 highlightSource fc (AnnBoundName n False)

646 highlightSource fc (AnnBoundName n False)

642− else if defined

647+ else if defined -- finally, ordinary PRef elaboration

643− then do apply (Var n) []

648+ then elabRef ec fc' fc hls n tm

644− annot <- findHighlight n

645− solve

646− highlightSource fc annot

647 else try (do apply (Var n) []

649 else try (do apply (Var n) []

648 annot <- findHighlight n

650 annot <- findHighlight n

649 solve

651 solve

664 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)

666 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)

665 | pattern && not reflection && not (e_qq ina) && e_nomatching ina

667 | pattern && not reflection && not (e_qq ina) && e_nomatching ina

666 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)

668 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)

667− | otherwise =

669+ | otherwise = elabRef ina fc' fc hls n tm

668− do fty <- get_type (Var n) -- check for implicits

669− ctxt <- get_context

670− env <- get_env

671− let a' = insertScopedImps fc (normalise ctxt env fty) []

672− if null a'

673− then erun fc $

674− do apply (Var n) []

675− hilite <- findHighlight n

676− solve

677− mapM_ (uncurry highlightSource) $

678− (fc, hilite) : map (\f -> (f, hilite)) hls

679− else elab' ina fc' (PApp fc tm [])

680 elab' ina _ (PLam _ _ _ _ PImpossible) = lift . tfail . Msg $ "Only pattern-matching lambdas can be impossible"

670 elab' ina _ (PLam _ _ _ _ PImpossible) = lift . tfail . Msg $ "Only pattern-matching lambdas can be impossible"

681 elab' ina _ (PLam fc n nfc Placeholder sc)

671 elab' ina _ (PLam fc n nfc Placeholder sc)

682 = do -- if n is a type constructor name, this makes no sense...

672 = do -- if n is a type constructor name, this makes no sense...

1512 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))

1502 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))

1513 fullApp x = x

1503 fullApp x = x

1514

1504

1515− insertScopedImps fc (Bind n (Pi _ im@(Just i) _ _) sc) xs

1505+ insertScopedImps fc ty@(Bind n (Pi _ im@(Just i) _ _) sc) xs

1516 | tcimplementation i && not (toplevel_imp i)

1506 | tcimplementation i && not (toplevel_imp i)

1517 = pimp n (PResolveTC fc) True : insertScopedImps fc sc xs

1507 = pimp n (PResolveTC fc) True : insertScopedImps fc sc xs

1518 | not (toplevel_imp i)

1508 | not (toplevel_imp i)

1519 = pimp n Placeholder True : insertScopedImps fc sc xs

1509 = pimp n Placeholder True : insertScopedImps fc sc xs

1520 insertScopedImps fc (Bind n (Pi _ _ _ _) sc) (x : xs)

1510 insertScopedImps fc (Bind n (Pi _ _ _ _) sc) (x : xs)

1521 = x : insertScopedImps fc sc xs

1511 = x : insertScopedImps fc sc xs

1522− insertScopedImps _ _ xs = xs

1512+ insertScopedImps _ ty xs = xs

1523

1513

1524 insertImpLam ina t =

1514 insertImpLam ina t =

1525 do ty <- goal

1515 do ty <- goal

1528 addLam ty' t

1518 addLam ty' t

1529 where

1519 where

1530 -- just one level at a time

1520 -- just one level at a time

1531− addLam (Bind n (Pi _ (Just _) _ _) sc) t =

1521+ addLam goal@(Bind n (Pi _ (Just _) _ _) sc) t =

1532 do impn <- unique_hole n -- (sMN 0 "scoped_imp")

1522 do impn <- unique_hole n -- (sMN 0 "scoped_imp")

1533− if e_isfn ina -- apply to an implicit immediately

1534− then return (PApp emptyFC

1535− (PLam emptyFC impn NoFC Placeholder t)

1536− [pexp Placeholder])

1537− else return (PLam emptyFC impn NoFC Placeholder t)

1523+ return (PLam emptyFC impn NoFC Placeholder t)

1538 addLam _ t = return t

1524 addLam _ t = return t

1539

1525

1540 insertCoerce ina t@(PCase _ _ _) = return t

1526 insertCoerce ina t@(PCase _ _ _) = return t

1559 addImplBound ist (map fstEnv env)

1545 addImplBound ist (map fstEnv env)

1560 (PApp fc (PRef fc [] n) [pexp (PCoerced t)])

1546 (PApp fc (PRef fc [] n) [pexp (PCoerced t)])

1561

1547

1548+ elabRef :: ElabCtxt -> Maybe FC -> FC -> [FC] -> Name -> PTerm -> ElabD ()

1549+ elabRef ina fc' fc hls n tm =

1550+ do fty <- get_type (Var n) -- check for implicits

1551+ ctxt <- get_context

1552+ env <- get_env

1553+ let a' = insertScopedImps fc (normalise ctxt env fty) []

1554+ if null a'

1555+ then erun fc $

1556+ do apply (Var n) []

1557+ hilite <- findHighlight n

1558+ solve

1559+ mapM_ (uncurry highlightSource) $

1560+ (fc, hilite) : map (\f -> (f, hilite)) hls

1561+ else elab' ina fc' (PApp fc tm [])

1562+

1562 -- | Elaborate the arguments to a function

1563 -- | Elaborate the arguments to a function

1563 elabArgs :: IState -- ^ The current Idris state

1564 elabArgs :: IState -- ^ The current Idris state

1564 -> ElabCtxt -- ^ (in an argument, guarded, in a type, in a qquote)

1565 -> ElabCtxt -- ^ (in an argument, guarded, in a type, in a qquote)