Merge pull request #266 from edwinb/vis-case-with

Propagate visibility appropriately to case/with

src/TTImp/Elab/Case.idr

@@ -184,6 +184,12 @@ caseBlock {vars} rigc elabinfo fc nest env scr scrtm scrty caseRig alts expected
          -- (esp. in the scrutinee!) are set to 0 in the case type
          let env = updateMults (linearUsed est) env
          defs <- get Ctxt
+         let vis = case !(lookupCtxtExact (Resolved (defining est)) (gamma defs)) of
+                        Just gdef =>
+                             if visibility gdef == Public
+                                then Public
+                                else Private
+                        Nothing => Public
 
          -- if the scrutinee is ones of the arguments in 'env' we should
          -- split on that, rather than adding it as a new argument
@@ -213,7 +219,7 @@ caseBlock {vars} rigc elabinfo fc nest env scr scrtm scrty caseRig alts expected
          -- the alternative of fixing up the environment
          when (not (isNil fullImps)) $ findImpsIn fc [] [] casefnty
          cidx <- addDef casen (newDef fc casen (if isErased rigc then erased else top)
-                                      [] casefnty Public None)
+                                      [] casefnty vis None)
          -- don't worry about totality of the case block; it'll be handled
          -- by the totality of the parent function
          setFlag fc (Resolved cidx) (SetTotal PartialOK)

src/TTImp/Elab/Local.idr

@@ -29,10 +29,20 @@ checkLocal : {vars : _} ->
              FC -> List ImpDecl -> (scope : RawImp) ->
              (expTy : Maybe (Glued vars)) ->
              Core (Term vars, Glued vars)
-checkLocal {vars} rig elabinfo nest env fc nestdecls scope expty
-    = do let defNames = definedInBlock [] nestdecls
-         est <- get EST
+checkLocal {vars} rig elabinfo nest env fc nestdecls_in scope expty
+    = do est <- get EST
          let f = defining est
+         defs <- get Ctxt
+         let vis = case !(lookupCtxtExact (Resolved (defining est)) (gamma defs)) of
+                        Just gdef => visibility gdef
+                        Nothing => Public
+         -- If the parent function is public, the nested definitions need
+         -- to be public too
+         let nestdecls =
+               if vis == Public
+                  then map setPublic nestdecls_in
+                  else nestdecls_in
+         let defNames = definedInBlock [] nestdecls
          names' <- traverse (applyEnv f)
                             (nub defNames) -- binding names must be unique
                                            -- fixes bug #115
@@ -101,6 +111,16 @@ checkLocal {vars} rig elabinfo nest env fc nestdecls scope expty
          = IData loc' vis (updateDataName nest d)
     updateName nest i = i
 
+    setPublic : ImpDecl -> ImpDecl
+    setPublic (IClaim fc c _ opts ty) = IClaim fc c Public opts ty
+    setPublic (IData fc _ d) = IData fc Public d
+    setPublic (IRecord fc c _ r) = IRecord fc c Public r
+    setPublic (IParameters fc ps decls)
+        = IParameters fc ps (map setPublic decls)
+    setPublic (INamespace fc ps decls)
+        = INamespace fc ps (map setPublic decls)
+    setPublic d = d
+
 getLocalTerm : {vars : _} ->
                {auto c : Ref Ctxt Defs} ->
                FC -> Env Term vars -> Term vars -> List Name ->

src/TTImp/Interactive/GenerateDef.idr

@@ -57,7 +57,7 @@ expandClause : {auto c : Ref Ctxt Defs} ->
 expandClause loc n c
     = do log 10 $ "Trying clause " ++ show c
          c <- uniqueRHS c
-         Right clause <- checkClause linear False n [] (MkNested []) [] c
+         Right clause <- checkClause linear Private False n [] (MkNested []) [] c
             | Left _ => pure [] -- TODO: impossible clause, do something
                                 -- appropriate
          let MkClause {vars} env lhs rhs = clause

src/TTImp/ProcessDef.idr

@@ -352,10 +352,10 @@ checkClause : {vars : _} ->
               {auto c : Ref Ctxt Defs} ->
               {auto m : Ref MD Metadata} ->
               {auto u : Ref UST UState} ->
-              (mult : RigCount) -> (hashit : Bool) ->
+              (mult : RigCount) -> (vis : Visibility) -> (hashit : Bool) ->
               Int -> List ElabOpt -> NestedNames vars -> Env Term vars ->
               ImpClause -> Core (Either RawImp Clause)
-checkClause mult hashit n opts nest env (ImpossibleClause fc lhs)
+checkClause mult vis hashit n opts nest env (ImpossibleClause fc lhs)
     = do lhs_raw <- lhsInCurrentNS nest lhs
          handleUnify
            (do autoimp <- isUnboundImplicits
@@ -380,7 +380,7 @@ checkClause mult hashit n opts nest env (ImpossibleClause fc lhs)
                            if !(impossibleErrOK defs err)
                               then pure (Left lhs_raw)
                               else throw (ValidCase fc env (Right err)))
-checkClause {vars} mult hashit n opts nest env (PatClause fc lhs_in rhs)
+checkClause {vars} mult vis hashit n opts nest env (PatClause fc lhs_in rhs)
     = do (_, (vars'  ** (sub', env', nest', lhstm', lhsty'))) <-
              checkLHS False mult hashit n opts nest env fc lhs_in
          let rhsMode = if isErased mult then InType else InExpr
@@ -405,7 +405,7 @@ checkClause {vars} mult hashit n opts nest env (PatClause fc lhs_in rhs)
 
          pure (Right (MkClause env' lhstm' rhstm))
 -- TODO: (to decide) With is complicated. Move this into its own module?
-checkClause {vars} mult hashit n opts nest env (WithClause fc lhs_in wval_raw flags cs)
+checkClause {vars} mult vis hashit n opts nest env (WithClause fc lhs_in wval_raw flags cs)
     = do (lhs, (vars'  ** (sub', env', nest', lhspat, reqty))) <-
              checkLHS False mult hashit n opts nest env fc lhs_in
          let wmode
@@ -468,7 +468,7 @@ checkClause {vars} mult hashit n opts nest env (WithClause fc lhs_in wval_raw fl
 
          wname <- genWithName n
          widx <- addDef wname (newDef fc wname (if isErased mult then erased else top)
-                                      vars wtype Private None)
+                                      vars wtype vis None)
          let rhs_in = apply (IVar fc wname)
                         (map (IVar fc) envns ++
                          map (maybe wval_raw (\pn => IVar fc (snd pn))) wargNames)
@@ -696,7 +696,8 @@ processDef opts nest env fc n_in cs_in
                        then erased
                        else linear
          nidx <- resolveName n
-         cs <- traverse (checkClause mult hashit nidx opts nest env) cs_in
+         cs <- traverse (checkClause mult (visibility gdef)
+                                     hashit nidx opts nest env) cs_in
          let pats = map toPats (rights cs)
 
          (cargs ** (tree_ct, unreachable)) <-

tests/idris2/coverage008/expected

@@ -1,6 +1,6 @@
 1/1: Building wcov (wcov.idr)
 Main> Main.tfoo is total
 Main> Main.wfoo is total
-Main> Main.wbar is not covering due to call to function Main.with block in 1376
+Main> Main.wbar is not covering due to call to function Main.with block in 1372
 Main> Main.wbar1 is total
 Main> Bye for now!

tests/idris2/coverage010/expected

@@ -1,3 +1,3 @@
 1/1: Building casetot (casetot.idr)
 casetot.idr:12:1--13:1:main is not covering:
-	Calls non covering function Main.case block in 2087(287)
+	Calls non covering function Main.case block in 2071(287)