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

git.iko.soy/Idris-dev

on master help sign in

Comment editing

6c682f3Edwin Brady11 years ago

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

compare with master

unifiedsplit

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

740

741-------

742

743−-- Frozen => doesn't reduce

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

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

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

745

747

746data Accessibility = Hidden | Public | Frozen | Private

748data Accessibility = Hidden | Public | Frozen | Private

747 deriving (Eq, Ord)

749 deriving (Eq, Ord)

src/Idris/Coverage.hs+10−4

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

442 _ -> []

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

444 t <- checkTotality [] fc n

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

446+ Just (n, a) -> a

447+ _ -> Public

445 case t of

448 case t of

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

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

447− -- typechecking decidable

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

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

454+ setAccessibility n newacc

449− addIBC (IBCAccess n Frozen)

455+ addIBC (IBCAccess n newacc)

450− logCoverage 5 $ "HIDDEN: "

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

451 ++ show n ++ show p

457 ++ show n ++ show p

452 _ -> return ()

458 _ -> return ()

453 return t

459 return t