c42673c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Highlight pattern vars

c42673cDavid Raymond Christiansen11 years ago

src/Idris/AbsSyntax.hs+15−15

compare with master

unifiedsplit

@@ -1519,9 +1519,9 @@ addImpl' inpat env infns imp_meths ist ptm

1519 ai :: Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm

1520 ai qq env ds (PRef fc f)

1521 | f `elem` infns = PInferRef fc f

1522− | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat qq imp_meths ist fc f ds []

1522+ | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat qq imp_meths ist fc f fc ds []

1523 ai qq env ds (PHidden (PRef fc f))

1524− | not (f `elem` map fst env) = PHidden (handleErr $ aiFn inpat False qq imp_meths ist fc f ds [])

1524+ | not (f `elem` map fst env) = PHidden (handleErr $ aiFn inpat False qq imp_meths ist fc f fc ds [])

1525 ai qq env ds (PEq fc lt rt l r)

1526 = let lt' = ai qq env ds lt

1527 rt' = ai qq env ds rt

@@ -1553,11 +1553,11 @@ addImpl' inpat env infns imp_meths ist ptm

1553 ai qq env ds (PApp fc (PInferRef _ f) as)

1554 = let as' = map (fmap (ai qq env ds)) as in

1555 PApp fc (PInferRef fc f) as'

1556− ai qq env ds (PApp fc ftm@(PRef _ f) as)

1556+ ai qq env ds (PApp fc ftm@(PRef ffc f) as)

1557− | f `elem` infns = ai qq env ds (PApp fc (PInferRef fc f) as)

1557+ | f `elem` infns = ai qq env ds (PApp fc (PInferRef ffc f) as)

1558 | not (f `elem` map fst env)

1559 = let as' = map (fmap (ai qq env ds)) as in

1560− handleErr $ aiFn inpat False qq imp_meths ist fc f ds as'

1560+ handleErr $ aiFn inpat False qq imp_meths ist fc f ffc ds as'

1561 | Just (Just ty) <- lookup f env =

1562 let as' = map (fmap (ai qq env ds)) as

1563 arity = getPArity ty in

@@ -1621,8 +1621,8 @@ addImpl' inpat env infns imp_meths ist ptm

1621-- if in a pattern, and there are no arguments, and there's no possible

1622-- names with zero explicit arguments, don't add implicits.

1623

1624−aiFn :: Bool -> Bool -> Bool -> [Name] -> IState -> FC -> Name -> [[T.Text]] -> [PArg] -> Either Err PTerm

1624+aiFn :: Bool -> Bool -> Bool -> [Name] -> IState -> FC -> Name -> FC -> [[T.Text]] -> [PArg] -> Either Err PTerm

1625−aiFn inpat True qq imp_meths ist fc f ds []

1625+aiFn inpat True qq imp_meths ist fc f ffc ds []

1626 = case lookupDef f (tt_ctxt ist) of

1627 [] -> Right $ PPatvar fc f

1628 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in

@@ -1630,7 +1630,7 @@ aiFn inpat True qq imp_meths ist fc f ds []

1630 if (not (vname f) || tcname f

1631 || any (conCaf (tt_ctxt ist)) ialts)

1632-- any constructor alts || any allImp ialts))

1633− then aiFn inpat False qq imp_meths ist fc f ds [] -- use it as a constructor

1633+ then aiFn inpat False qq imp_meths ist fc f fc ds [] -- use it as a constructor

1634 else Right $ PPatvar fc f

1635 where imp (PExp _ _ _ _) = False

1636 imp _ = True

@@ -1644,9 +1644,9 @@ aiFn inpat True qq imp_meths ist fc f ds []

1644 vname (UN n) = True -- non qualified

1645 vname _ = False

1646

1647−aiFn inpat expat qq imp_meths ist fc f ds as

1647+aiFn inpat expat qq imp_meths ist fc f ffc ds as

1648− | f `elem` primNames = Right $ PApp fc (PRef fc f) as

1648+ | f `elem` primNames = Right $ PApp fc (PRef ffc f) as

1649−aiFn inpat expat qq imp_meths ist fc f ds as

1649+aiFn inpat expat qq imp_meths ist fc f ffc ds as

1650 -- This is where namespaces get resolved by adding PAlternative

1651 = do let ns = lookupCtxtName f (idris_implicits ist)

1652 let nh = filter (\(n, _) -> notHidden n) ns

@@ -1654,13 +1654,13 @@ aiFn inpat expat qq imp_meths ist fc f ds as

1654 [] -> nh

1655 x -> x

1656 case ns' of

1657− [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc (isImpName f f')) (insertImpl ns as)

1657+ [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef ffc (isImpName f f')) (insertImpl ns as)

1658 [] -> if f `elem` (map fst (idris_metavars ist))

1659− then Right $ PApp fc (PRef fc f) as

1659+ then Right $ PApp fc (PRef ffc f) as

1660− else Right $ mkPApp fc (length as) (PRef fc f) as

1660+ else Right $ mkPApp fc (length as) (PRef ffc f) as

1661 alts -> Right $

1662 PAlternative True $

1663− map (\(f', ns) -> mkPApp fc (length ns) (PRef fc (isImpName f f'))

1663+ map (\(f', ns) -> mkPApp fc (length ns) (PRef ffc (isImpName f f'))

1664 (insertImpl ns as)) alts

1665 where

1666 -- if the name is in imp_meths, we should actually refer to the bound

src/Idris/Elab/Term.hs+16−5

@@ -452,7 +452,10 @@ elab ist info emode opts fn tm

452 trySeq' deferr (x : xs)

453 = try' (do elab' ina fc x

454 solveAutos ist fn False) (trySeq' deferr xs) True

455− elab' ina _ (PPatvar fc n) | bindfree = do patvar n; update_term liftPats

455+ elab' ina _ (PPatvar fc n) | bindfree

456+ = do patvar n

457+ update_term liftPats

458+ highlightSource fc (AnnBoundName n False)

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

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

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

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

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

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

@@ -472,11 +475,20 @@ elab ist info emode opts fn tm

472 _ -> True

475 _ -> True

473 -- this is to stop us resolve type classes recursively

476 -- this is to stop us resolve type classes recursively

474 -- trace (show (n, guarded)) $

477 -- trace (show (n, guarded)) $

478+ if (tcname n && ina)

479+ then erun fc $

480+ do patvar n

475− if (tcname n && ina) then erun fc $ do patvar n; update_term liftPats

481+ update_term liftPats

482+ highlightSource fc (AnnBoundName n False)

476 else if (defined && not guarded)

483 else if (defined && not guarded)

477 then do apply (Var n) []; solve

484 then do apply (Var n) []; solve

478− else try (do apply (Var n) []; solve)

485+ else try (do apply (Var n) []

486+ annot <- findHighlight n

487+ solve

488+ highlightSource fc annot)

489+ (do patvar n

479− (do patvar n; update_term liftPats)

490+ update_term liftPats

491+ highlightSource fc (AnnBoundName n False))

480 where inparamBlock n = case lookupCtxtName n (inblock info) of

492 where inparamBlock n = case lookupCtxtName n (inblock info) of

481 [] -> False

493 [] -> False

482 _ -> True

494 _ -> True

@@ -707,7 +719,6 @@ elab ist info emode opts fn tm

707

719

708 annot <- findHighlight f

720 annot <- findHighlight f

709 highlightSource ffc annot

721 highlightSource ffc annot

710− trace ("highlighting " ++ show f ++ " at " ++ show ffc ++ " as " ++ show annot) $ return ()

711

722

712 elabArgs ist (ina { e_inarg = e_inarg ina || not isinf })

723 elabArgs ist (ina { e_inarg = e_inarg ina || not isinf })

713 [] fc False f

724 [] fc False f

src/Idris/ParseOps.hs+2−3

@@ -76,10 +76,9 @@ prefix name f = Prefix (do reservedOp name

76-- | Backtick operator

77backtick :: Operator IdrisParser PTerm

78backtick = Infix (do indentPropHolds gtProp

79− lchar '`'; n <- fst <$> fnName

79+ lchar '`'; (n, fc) <- fnName

80 lchar '`'

81 indentPropHolds gtProp

82− fc <- getFC

83 return (\x y -> PApp fc (PRef fc n) [pexp x, pexp y])) AssocNone

82 return (\x y -> PApp fc (PRef fc n) [pexp x, pexp y])) AssocNone

85-- | Operator without fixity (throws an error)

84-- | Operator without fixity (throws an error)

@@ -87,7 +86,7 @@ nofixityoperator :: Operator IdrisParser PTerm

87nofixityoperator = Infix (do indentPropHolds gtProp

86nofixityoperator = Infix (do indentPropHolds gtProp

88 op <- try operator

87 op <- try operator

89 unexpected $ "Operator without known fixity: " ++ op) AssocNone

88 unexpected $ "Operator without known fixity: " ++ op) AssocNone

90−

89+

92{- | Parses an operator in function position i.e. enclosed by `()', with an

91{- | Parses an operator in function position i.e. enclosed by `()', with an

93 optional namespace

92 optional namespace