From 0cc54ff145adee29f42b5a970d9104a8cc598fd2 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Wed, 10 Jun 2020 12:41:02 +0100 Subject: [PATCH 1/3] Propagate visibility appropriately to case/with If a function is public export, the local definitions also need to be public export for it to reduce properly. But if they're not, we don't want them exported or they might affect the module hash and cause unnecessary rebuilds. --- src/TTImp/Elab/Case.idr | 8 +++++++- src/TTImp/Elab/Local.idr | 26 +++++++++++++++++++++++--- src/TTImp/Interactive/GenerateDef.idr | 2 +- src/TTImp/ProcessDef.idr | 13 +++++++------ tests/idris2/coverage010/expected | 2 +- 5 files changed, 39 insertions(+), 12 deletions(-) diff --git a/src/TTImp/Elab/Case.idr b/src/TTImp/Elab/Case.idr index ec7e3e17bb..7290b99034 100644 --- a/src/TTImp/Elab/Case.idr +++ b/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) diff --git a/src/TTImp/Elab/Local.idr b/src/TTImp/Elab/Local.idr index affded18e4..675cfc23bf 100644 --- a/src/TTImp/Elab/Local.idr +++ b/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 -> diff --git a/src/TTImp/Interactive/GenerateDef.idr b/src/TTImp/Interactive/GenerateDef.idr index 343a7b6c56..cc09c1834a 100644 --- a/src/TTImp/Interactive/GenerateDef.idr +++ b/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 diff --git a/src/TTImp/ProcessDef.idr b/src/TTImp/ProcessDef.idr index da6c383132..939103c75a 100644 --- a/src/TTImp/ProcessDef.idr +++ b/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)) <- diff --git a/tests/idris2/coverage010/expected b/tests/idris2/coverage010/expected index 42d1b5123b..c2660961c6 100644 --- a/tests/idris2/coverage010/expected +++ b/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 2081(287) From c07876d1a304f8fb11d3d9dc904ae102b0d41cac Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Wed, 10 Jun 2020 12:53:18 +0100 Subject: [PATCH 2/3] Fix clashing test output --- tests/idris2/coverage010/expected | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/idris2/coverage010/expected b/tests/idris2/coverage010/expected index c2660961c6..b1bc356484 100644 --- a/tests/idris2/coverage010/expected +++ b/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 2081(287) + Calls non covering function Main.case block in 2071(287) From df3449f44b4dcf12c6f39b14b8d280680ada533c Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Wed, 10 Jun 2020 13:08:50 +0100 Subject: [PATCH 3/3] Fix the other clashing test output I don't understand the difference here - there's probably a commit I hadn't merged earlier that affected the name generation. --- tests/idris2/coverage008/expected | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/idris2/coverage008/expected b/tests/idris2/coverage008/expected index 77b301b2d9..76fe3b30a9 100644 --- a/tests/idris2/coverage008/expected +++ b/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!