6c682f3 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Comment editing

commit6c682f3902110e970c01c1cbd2963e39869fd4d6 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 14 Feb 2016, 12:35 (11 years ago) parentfdfd99e

2 files changed+14−6

unifiedsplit

src/Idris/Core/Evaluate.hs+4−2

@@ -740,8 +740,10 @@ instance Show Def where

740740

741741-------

742742

743−-- Frozen => doesn't reduce

744−-- Hidden => doesn't reduce and invisible to type checker

743+-- Hidden => Programs can't access the name at all

744+-- Public => Programs can access the name and use at will

745+-- Frozen => Programs can access the name, which doesn't reduce

746+-- Private => Programs can't access the name, doesn't reduce internally

745747

746748data Accessibility = Hidden | Public | Frozen | Private

747749 deriving (Eq, Ord)

src/Idris/Coverage.hs+10−4

@@ -442,12 +442,18 @@ checkDeclTotality (fc, n)

442442 _ -> []

443443 when (CoveringFn `elem` opts) $ checkAllCovering fc [] n n

444444 t <- checkTotality [] fc n

445+ let acc = case lookupDefAccExact n False (tt_ctxt i) of

446+ Just (n, a) -> a

447+ _ -> Public

445448 case t of

446449 -- if it's not total, it can't reduce, to keep

447− -- typechecking decidable

448− p@(Partial _) -> do setAccessibility n Frozen

449− addIBC (IBCAccess n Frozen)

450− logCoverage 5 $ "HIDDEN: "

450+ -- typechecking decidable.

451+ -- So if it's currently public export, set it as

452+ -- export instead.

453+ p@(Partial _) -> do let newacc = max Frozen acc

454+ setAccessibility n newacc

455+ addIBC (IBCAccess n newacc)

456+ logCoverage 5 $ "Set to " ++ show newacc ++ ":"

451457 ++ show n ++ show p

452458 _ -> return ()

453459 return t