c42673c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Highlight pattern vars

commitc42673c5d74bbbc2fbd69566eb39db8b5fa1f881 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateSun 10 May 2015, 21:00 (11 years ago) parent924f791

3 files changed+33−23

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+15−15 src/Idris/Elab/Term.hs+16−5 src/Idris/ParseOps.hs+2−3

src/Idris/AbsSyntax.hs+15−15

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

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

15201520 ai qq env ds (PRef fc f)

15211521 | 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 []

15231523 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 [])

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

15261526 = let lt' = ai qq env ds lt

15271527 rt' = ai qq env ds rt

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

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

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

15551555 PApp fc (PInferRef fc f) as'

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

1557− | f `elem` infns = ai qq env ds (PApp fc (PInferRef fc 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 ffc f) as)

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

15591559 = 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'

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

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

15631563 arity = getPArity ty in

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

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

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

16231623

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

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

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 ffc ds []

16261626 = case lookupDef f (tt_ctxt ist) of

16271627 [] -> Right $ PPatvar fc f

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

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

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

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

16321632-- 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

16341634 else Right $ PPatvar fc f

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

16361636 imp _ = True

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

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

16451645 vname _ = False

16461646

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

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

1649−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 ffc f) as

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

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

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

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

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

16541654 [] -> nh

16551655 x -> x

16561656 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)

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

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

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

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

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

16611661 alts -> Right $

16621662 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'))

16641664 (insertImpl ns as)) alts

16651665 where

16661666 -- 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

452452 trySeq' deferr (x : xs)

453453 = try' (do elab' ina fc x

454454 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)

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

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

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

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

472475 _ -> True

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

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

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

478+ if (tcname n && ina)

479+ then erun fc $

480+ do patvar n

481+ update_term liftPats

482+ highlightSource fc (AnnBoundName n False)

476483 else if (defined && not guarded)

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

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

479− (do patvar n; update_term liftPats)

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

486+ annot <- findHighlight n

487+ solve

488+ highlightSource fc annot)

489+ (do patvar n

490+ update_term liftPats

491+ highlightSource fc (AnnBoundName n False))

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

481493 [] -> False

482494 _ -> True

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

707719

708720 annot <- findHighlight f

709721 highlightSource ffc annot

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

711722

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

713724 [] fc False f

src/Idris/ParseOps.hs+2−3

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

7676-- | Backtick operator

7777backtick :: Operator IdrisParser PTerm

7878backtick = Infix (do indentPropHolds gtProp

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

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

8080 lchar '`'

8181 indentPropHolds gtProp

82− fc <- getFC

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

8483

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

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

8786nofixityoperator = Infix (do indentPropHolds gtProp

8887 op <- try operator

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

90−

89+

9190

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

9392 optional namespace