9546bd4 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Ignore accessibility when rechecking

access rules (private/public) only relevant during elaboration

commit9546bd4531b25363b400df1a7e44fc75550854bd authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 16 Mar 2015, 17:38 (12 years ago) parent426d052

2 files changed+10−4

compare with master

unifiedsplit

src/Idris/Core/Evaluate.hs+6−3 src/Idris/Core/Typecheck.hs+4−1

src/Idris/Core/Evaluate.hs+6−3

@@ -9,7 +9,7 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,

99 addToCtxt, setAccess, setTotal, setMetaInformation, addCtxtDef, addTyDecl,

1010 addDatatype, addCasedef, simplifyCasedef, addOperator,

1111 lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,

12− lookupP, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,

12+ lookupP, lookupP_all, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,

1313 mapDefCtxt,

1414 lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict, isDConName, canBeDConName, isTConName, isConName, isFnName,

1515 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,

@@ -1007,7 +1007,10 @@ isTCDict n ctxt

10071007 _ -> False

10081008

10091009lookupP :: Name -> Context -> [Term]

1010−lookupP n ctxt

1010+lookupP = lookupP_all False

1011+

1012+lookupP_all :: Bool -> Name -> Context -> [Term]

1013+lookupP_all all n ctxt

10111014 = do def <- lookupCtxt n (definitions ctxt)

10121015 p <- case def of

10131016 (Function ty tm, a, _, _) -> return (P Ref n ty, a)

@@ -1015,7 +1018,7 @@ lookupP n ctxt

10151018 (CaseOp _ ty _ _ _ _, a, _, _) -> return (P Ref n ty, a)

10161019 (Operator ty _ _, a, _, _) -> return (P Ref n ty, a)

10171020 case snd p of

1018− Hidden -> []

1021+ Hidden -> if all then return (fst p) else []

10191022 _ -> return (fst p)

10201023

10211024lookupDefExact :: Name -> Context -> Maybe Def

src/Idris/Core/Typecheck.hs+4−1

@@ -81,7 +81,10 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

8181 Env -> Raw -> StateT UCs TC (Term, Type)

8282 chk u env (Var n)

8383 | Just (i, ty) <- lookupTyEnv n env = return (P Bound n ty, ty)

84− | (P nt n' ty : _) <- lookupP n ctxt = return (P nt n' ty, ty)

84+ -- If we're elaborating, we don't want the private names; if we're

85+ -- checking an already elaborated term, we do

86+ | (P nt n' ty : _) <- lookupP_all (not holes) n ctxt

87+ = return (P nt n' ty, ty)

8588 | otherwise = do lift $ tfail $ NoSuchVariable n

8689 chk u env ap@(RApp f a)

8790 = do (fv, fty) <- chk u env f