5cb8ec3 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Be more careful with implicit FCs

This stops implict args from being highlighted on top of their functions sometimes.

commit5cb8ec3e0513140ec0c87c4d93204469973c6f0c authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateMon 11 May 2015, 10:47 (11 years ago) parent73b666b

2 files changed+6−6

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+3−3 src/Idris/Elab/Term.hs+3−3

src/Idris/AbsSyntax.hs+3−3

@@ -1628,14 +1628,14 @@ addImpl' inpat env infns imp_meths ist ptm

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

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

16301630 = case lookupDef f (tt_ctxt ist) of

1631− [] -> Right $ PPatvar fc f

1631+ [] -> Right $ PPatvar ffc f

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

16331633 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $

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

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

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

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

1638− else Right $ PPatvar fc f

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

1638+ else Right $ PPatvar ffc f

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

16401640 imp _ = True

16411641-- allImp [] = False

src/Idris/Elab/Term.hs+3−3

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

499499 bindable (NS _ _) = False

500500 bindable (UN xs) = True

501501 bindable n = implicitable n

502− elab' ina _ f@(PInferRef fc n) = elab' ina (Just fc) (PApp fc f [])

502+ elab' ina _ f@(PInferRef fc n) = elab' ina (Just fc) (PApp NoFC f [])

503503 elab' ina fc' tm@(PRef fc n)

504504 | pattern && not reflection && not (e_qq ina) && not (e_intype ina)

505505 && isTConName n (tt_ctxt ist)

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

861861 setInjective (PApp _ (PRef _ n) _) = setinj n

862862 setInjective _ = return ()

863863

864− elab' ina _ tm@(PApp fc f [arg]) =

864+ elab' ina _ tm@(PApp fc f [arg]) =

865865 erun fc $

866866 do simple_app (not $ headRef f)

867− (elabE (ina { e_isfn = True }) (Just fc) f)

867+ (elabE (ina { e_isfn = True }) (Just fc) f)

868868 (elabE (ina { e_inarg = True }) (Just fc) (getTm arg))

869869 (show tm)

870870 solve