7537cc4 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Change totality checking and inlining

This solves a problem caused by inlining for totality checking, but not elsewhere. For example, the following passes totality checking because x is inlined: foo = let x = diverging in 42 If we then assume it's safe to evaluate all parts of foo because it's total, as the partial evaluator does, the compiler ends up in a loop. So, the totality checked version and the stored version really need to be the same, which this patch does. We still need to do some controlled unfolding so that interface dictionaries work correctly (controlled using the 'Unfold' flag on a function), and to spot definitions which preserve guardedness of productive definitions.

commit7537cc415ee2b26c8b76063e86a0a1ce95981aee authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 17 Nov 2016, 13:37 (10 years ago) parent4057b48

17 files changed+269−79

compare with master

unifiedsplit

libs/prelude/Builtins.idr+2−1 libs/prelude/Prelude/Show.idr+2−2 libs/prelude/Prelude/Strings.idr+2−2 src/Idris/AbsSyntax.hs+7 src/Idris/AbsSyntaxTree.hs+9−2 src/Idris/Core/Elaborate.hs+1−1 src/Idris/Core/Evaluate.hs+64−42 src/Idris/Core/ProofState.hs+4−4 src/Idris/Core/Typecheck.hs+2−2 src/Idris/Coverage.hs+62−2 src/Idris/Elab/Clause.hs+83−7 src/Idris/Elab/Implementation.hs+10−1 src/Idris/Elab/Term.hs+4−4 src/Idris/Elab/Type.hs+1−1 src/Idris/IBC.hs+13−4 test/totality013/expected+2−3 test/totality015/totality015.idr+1−1

libs/prelude/Builtins.idr+2−1

@@ -160,7 +160,8 @@ par : Lazy a -> a -- Doesn't actually do anything yet. Maybe a 'Par a' type

160160par (Delay x) = x

161161

162162||| Assert to the totality checker that y is always structurally smaller than

163−||| x (which is typically a pattern argument)

163+||| x (which is typically a pattern argument, and *must* be in normal form

164+||| for this to work)

164165||| @ x the larger value (typically a pattern argument)

165166||| @ y the smaller value (typically an argument to a recursive call)

166167assert_smaller : (x : a) -> (y : b) -> b

libs/prelude/Prelude/Show.idr+2−2

@@ -46,7 +46,7 @@ interface Show ty where

4646 ||| @ x the value to convert

4747 partial

4848 show : (x : ty) -> String

49− show = showPrec Open

49+ show x = showPrec Open x -- Eta expand to help totality checker

5050

5151 ||| Convert a value to its `String` representation in a certain precedence

5252 ||| context.

@@ -63,7 +63,7 @@ interface Show ty where

6363 ||| @ x the value to convert

6464 partial

6565 showPrec : (d : Prec) -> (x : ty) -> String

66− showPrec _ = show

66+ showPrec _ x = show x

6767

6868||| Surround a `String` with parentheses depending on a condition.

6969|||

libs/prelude/Prelude/Strings.idr+2−2

@@ -328,7 +328,7 @@ toLower : String -> String

328328toLower x with (strM x)

329329 toLower "" | StrNil = ""

330330 toLower (strCons c cs) | (StrCons c cs) =

331− strCons (toLower c) (toLower (assert_smaller (strCons c cs) cs))

331+ strCons (toLower c) (toLower (assert_smaller (prim__strCons c cs) cs))

332332

333333||| Uppercases all characters in the string.

334334|||

@@ -339,7 +339,7 @@ toUpper : String -> String

339339toUpper x with (strM x)

340340 toUpper "" | StrNil = ""

341341 toUpper (strCons c cs) | (StrCons c cs) =

342− strCons (toUpper c) (toUpper (assert_smaller (strCons c cs) cs ))

342+ strCons (toUpper c) (toUpper (assert_smaller (prim__strCons c cs) cs ))

343343

344344--------------------------------------------------------------------------------

345345-- Predicates

src/Idris/AbsSyntax.hs+7

@@ -208,6 +208,13 @@ clear_totcheck = do i <- getIState; putIState $ i { idris_totcheck = [] }

208208setFlags :: Name -> [FnOpt] -> Idris ()

209209setFlags n fs = do i <- getIState; putIState $ i { idris_flags = addDef n fs (idris_flags i) }

210210

211+addFnOpt :: Name -> FnOpt -> Idris ()

212+addFnOpt n f = do i <- getIState

213+ let fls = case lookupCtxtExact n (idris_flags i) of

214+ Nothing -> []

215+ Just x -> x

216+ setFlags n (f : fls)

217+

211218setFnInfo :: Name -> FnInfo -> Idris ()

212219setFnInfo n fs = do i <- getIState; putIState $ i { idris_fninfo = addDef n fs (idris_fninfo i) }

213220

src/Idris/AbsSyntaxTree.hs+9−2

@@ -361,7 +361,7 @@ data IBCWrite = IBCFix FixDecl

361361 | IBCMetaInformation Name MetaInformation

362362 | IBCTotal Name Totality

363363 | IBCInjective Name Injectivity

364− | IBCFlags Name [FnOpt]

364+ | IBCFlags Name

365365 | IBCFnInfo Name FnInfo

366366 | IBCTrans Name (Term, Term)

367367 | IBCErrRev (Term, Term)

@@ -636,7 +636,8 @@ tacimpl t = TacImp [] Dynamic t

636636

637637data FnOpt = Inlinable -- ^ always evaluate when simplifying

638638 | TotalFn | PartialFn | CoveringFn

639− | Coinductive | AssertTotal

639+ | AllGuarded -- ^ all delayed arguments guaranteed guarded by constructors

640+ | AssertTotal

640641

641642 -- | interface dictionary, eval only when a function

642643 -- argument, and further evaluation results.

@@ -649,6 +650,12 @@ data FnOpt = Inlinable -- ^ always evaluate when simplifying

649650 | ErrorReverse -- ^ attempt to reverse normalise before showing in error

650651 | Reflection -- ^ a reflecting function, compile-time only

651652 | Specialise [(Name, Maybe Int)] -- ^ specialise it, freeze these names

653+ | UnfoldIface Name [Name]

654+ -- ^ Unfold given interface name in the definition, the

655+ -- top level methods, and anything which has

656+ -- the interface name as an argument. This is to unfold

657+ -- things for termination checking, as interfaces will otherwise

658+ -- cause problems

652659 | Constructor -- ^ Data constructor type

653660 | AutoHint -- ^ use in auto implicit search

654661 | PEGenerated -- ^ generated by partial evaluator

src/Idris/Core/Elaborate.hs+1−1

@@ -697,7 +697,7 @@ apply_elab n args =

697697 do ty <- get_type (Var n)

698698 ctxt <- get_context

699699 env <- get_env

700− claims <- doClaims (hnf ctxt env ty) args []

700+ claims <- doClaims (normalise ctxt env ty) args []

701701 prep_fill n (map fst claims)

702702 let eclaims = sortBy (\ (_, x) (_,y) -> priOrder x y) claims

703703 elabClaims [] False claims

src/Idris/Core/Evaluate.hs+64−42

@@ -11,7 +11,7 @@ Maintainer : The Idris Community.

1111

1212module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,

1313 normaliseAll, normaliseBlocking, toValue, quoteTerm,

14− rt_simplify, simplify, specialise, hnf, convEq, convEq',

14+ rt_simplify, simplify, specialise, unfold, convEq, convEq',

1515 Def(..), CaseInfo(..), CaseDefs(..),

1616 Accessibility(..), Injectivity, Totality(..), PReason(..), MetaInformation(..),

1717 Context, initContext, ctxtAlist, next_tvar,

@@ -45,10 +45,10 @@ data EvalState = ES { limited :: [(Name, Int)],

4545type Eval a = State EvalState a

4646

4747data EvalOpt = Spec

48− | HNF

49− | Simplify

48+ | Simplify Bool -- ^ whether to expand lets or not

5049 | AtREPL

5150 | RunTT

51+ | Unfold

5252 deriving (Show, Eq)

5353

5454initEval = ES [] 0 False

@@ -131,10 +131,7 @@ specialise ctxt env limits t

131131 (tm, limited st)

132132

133133-- | Like normalise, but we only reduce functions that are marked as okay to

134−-- inline (and probably shouldn't reduce lets?)

135−-- 20130908: now only used to reduce for totality checking. Inlining should

136−-- be done elsewhere.

137−

134+-- inline, and lets

138135simplify :: Context -> Env -> TT Name -> TT Name

139136simplify ctxt env t

140137 = evalState (do val <- eval False ctxt [(sUN "lazy", 0),

@@ -146,7 +143,23 @@ simplify ctxt env t

146143 (sUN "prim__syntactic_eq", 0),

147144 (sUN "fork", 0)]

148145 (map finalEntry env) (finalise t)

149− [Simplify]

146+ [Simplify True]

147+ quote 0 val) initEval

148+

149+-- | Like simplify, but we only reduce functions that are marked as okay to

150+-- inline, and don't reduce lets

151+inline :: Context -> Env -> TT Name -> TT Name

152+inline ctxt env t

153+ = evalState (do val <- eval False ctxt [(sUN "lazy", 0),

154+ (sUN "force", 0),

155+ (sUN "Force", 0),

156+ (sUN "assert_smaller", 0),

157+ (sUN "assert_total", 0),

158+ (sUN "par", 0),

159+ (sUN "prim__syntactic_eq", 0),

160+ (sUN "fork", 0)]

161+ (map finalEntry env) (finalise t)

162+ [Simplify False]

150163 quote 0 val) initEval

151164

152165-- | Simplify for run-time (i.e. basic inlining)

@@ -162,12 +175,19 @@ rt_simplify ctxt env t

162175 [RunTT]

163176 quote 0 val) initEval

164177

165−-- | Reduce a term to head normal form

166−hnf :: Context -> Env -> TT Name -> TT Name

167−hnf ctxt env t

168− = evalState (do val <- eval False ctxt []

169− (map finalEntry env)

170− (finalise t) [HNF]

178+-- | Unfold the given names in a term, the given number of times in a stack.

179+-- Preserves 'let'.

180+-- This is primarily to support inlining of the given names, and can also

181+-- help with partial evaluation by allowing a rescursive definition to be

182+-- unfolded once only.

183+-- Specifically used to unfold definitions using interfaces before going to

184+-- the totality checker (otherwise mutually recursive definitions in

185+-- implementations will not work...)

186+unfold :: Context -> Env -> [(Name, Int)] -> TT Name -> TT Name

187+unfold ctxt env ns t

188+ = evalState (do val <- eval False ctxt ns

189+ (map finalEntry env) (finalise t)

190+ [Unfold]

171191 quote 0 val) initEval

172192

173193

@@ -187,22 +207,25 @@ unbindEnv (_:bs) (Bind n b sc) = unbindEnv bs sc

187207unbindEnv env tm = error "Impossible case occurred: couldn't unbind env."

188208

189209usable :: Bool -- specialising

210+ -> Bool -- unfolding only

190211 -> Int -- Reduction depth limit (when simplifying/at REPL)

191212 -> Name -> [(Name, Int)] -> Eval (Bool, [(Name, Int)])

192213-- usable _ _ ns@((MN 0 "STOP", _) : _) = return (False, ns)

193−usable False depthlimit n [] = return (True, [])

194−usable True depthlimit n ns

214+usable False uf depthlimit n [] = return (True, [])

215+usable True uf depthlimit n ns

195216 = do ES ls num b <- get

196217 if b then return (False, ns)

197218 else case lookup n ls of

198219 Just 0 -> return (False, ns)

199220 Just i -> return (True, ns)

200221 _ -> return (False, ns)

201−usable False depthlimit n ns

222+usable False uf depthlimit n ns

202223 = case lookup n ns of

203224 Just 0 -> return (False, ns)

204225 Just i -> return $ (True, (n, abs (i-1)) : filter (\ (n', _) -> n/=n') ns)

205− _ -> return $ (True, (n, depthlimit) : filter (\ (n', _) -> n/=n') ns)

226+ _ -> return $ if uf

227+ then (False, ns)

228+ else (True, (n, depthlimit) : filter (\ (n', _) -> n/=n') ns)

206229

207230

208231fnCount :: Int -> Name -> Eval ()

@@ -231,10 +254,11 @@ eval :: Bool -> Context -> [(Name, Int)] -> Env -> TT Name ->

231254 [EvalOpt] -> Eval Value

232255eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

233256 spec = Spec `elem` opts

234− simpl = Simplify `elem` opts

257+ simpl = Simplify True `elem` opts || Simplify False `elem` opts

258+ simpl_inline = Simplify False `elem` opts

235259 runtime = RunTT `elem` opts

236260 atRepl = AtREPL `elem` opts

237− hnf = HNF `elem` opts

261+ unfold = Unfold `elem` opts

238262

239263 -- returns 'True' if the function should block

240264 -- normal evaluation should return false

@@ -243,7 +267,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

243267 = if always then False

244268 else not (inl || dict) || elem n stk

245269 | simpl

246− = (not (inl || dict) || elem n stk)

270+ = (not inl || elem n stk)

247271 || (n == sUN "prim__syntactic_eq")

248272 | otherwise = False

249273

@@ -254,21 +278,21 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

254278 ev ntimes stk top env (P _ n ty)

255279 | Just (Let t v) <- lookup n genv = ev ntimes stk top env v

256280 ev ntimes_in stk top env (P Ref n ty)

257− | not top && hnf = liftM (VP Ref n) (ev ntimes stk top env ty)

258− | otherwise

259281 = do let limit = if simpl then 100 else 10000

260− (u, ntimes) <- usable spec limit n ntimes_in

261− let red = u && (tcReducible n ctxt || spec || atRepl || runtime

282+ (u, ntimes) <- usable spec unfold limit n ntimes_in

283+ let red = u && (tcReducible n ctxt || spec || atRepl

284+ || runtime || unfold

262285 || sUN "assert_total" `elem` stk)

263286 if red then

264− do let val = lookupDefAcc n (spec || atRepl || runtime) ctxt

287+ do let val = lookupDefAcc n (spec || unfold || atRepl || runtime) ctxt

265288 case val of

266289 [(Function _ tm, Public)] ->

267290 ev ntimes (n:stk) True env tm

268291 [(TyDecl nt ty, _)] -> do vty <- ev ntimes stk True env ty

269292 return $ VP nt n vty

270293 [(CaseOp ci _ _ _ _ cd, acc)]

271− | (acc == Public || acc == Hidden || sUN "assert_total" `elem` stk) &&

294+ | (acc == Public || acc == Hidden) &&

295+-- || sUN "assert_total" `elem` stk) &&

272296 null (fst (cases_totcheck cd)) -> -- unoptimised version

273297 let (ns, tree) = getCases cd in

274298 if blockSimplify ci n stk

@@ -281,12 +305,12 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

281305 _ -> liftM (VP Ref n) (ev ntimes stk top env ty)

282306 else liftM (VP Ref n) (ev ntimes stk top env ty)

283307 ev ntimes stk top env (P nt n ty)

284− = liftM (VP nt n) (ev ntimes stk top env ty)

308+ = liftM (VP nt n) (ev ntimes stk top env ty)

285309 ev ntimes stk top env (V i)

286− | i < length env && i >= 0 = return $ snd (env !! i)

287− | otherwise = return $ VV i

310+ | i < length env && i >= 0 = return $ snd (env !! i)

311+ | otherwise = return $ VV i

288312 ev ntimes stk top env (Bind n (Let t v) sc)

289− | not runtime || occurrences n sc < 2

313+ | (not (runtime || simpl_inline || unfold)) || occurrences n sc < 2

290314 = do v' <- ev ntimes stk top env v --(finalise v)

291315 sc' <- ev ntimes stk top ((n, v') : env) sc

292316 wknV (-1) sc'

@@ -315,7 +339,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

315339 -- block reduction immediately under codata (and not forced)

316340 ev ntimes stk top env

317341 (App _ (App _ (App _ d@(P _ (UN dly) _) l@(P _ (UN lco) _)) t) arg)

318− | dly == txt "Delay" && lco == txt "Infinite" && not simpl

342+ | dly == txt "Delay" && lco == txt "Infinite" && not (unfold || simpl)

319343 = do let (f, _) = unApply arg

320344 let ntimes' = case f of

321345 P _ fn _ -> (fn, 0) : ntimes

@@ -330,7 +354,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

330354 -- Treat "assert_total" specially, as long as it's defined!

331355 ev ntimes stk top env (App _ (App _ (P _ n@(UN at) _) _) arg)

332356 | [(CaseOp _ _ _ _ _ _, _)] <- lookupDefAcc n (spec || atRepl || runtime) ctxt,

333− at == txt "assert_total" && not simpl

357+ at == txt "assert_total" && not (simpl || unfold)

334358 = ev ntimes (n : stk) top env arg

335359 ev ntimes stk top env (App _ f a)

336360 = do f' <- ev ntimes stk False env f

@@ -377,16 +401,13 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

377401 app <- apply ntimes stk top env a' as

378402 wknV 1 app

379403 apply ntimes_in stk top env f@(VP Ref n ty) args

380− | not top && hnf = case args of

381− [] -> return f

382− _ -> return $ unload env f args

383− | otherwise

384404 = do let limit = if simpl then 100 else 10000

385− (u, ntimes) <- usable spec limit n ntimes_in

386− let red = u && (tcReducible n ctxt || spec || atRepl || runtime

405+ (u, ntimes) <- usable spec unfold limit n ntimes_in

406+ let red = u && (tcReducible n ctxt || spec || atRepl

407+ || unfold || runtime

387408 || sUN "assert_total" `elem` stk)

388409 if red then

389− do let val = lookupDefAcc n (spec || atRepl || runtime) ctxt

410+ do let val = lookupDefAcc n (spec || unfold || atRepl || runtime) ctxt

390411 case val of

391412 [(CaseOp ci _ _ _ _ cd, acc)]

392413 | acc == Public || acc == Hidden ->

@@ -975,7 +996,8 @@ simplifyCasedef n ei uctxt

975996 pdef = map debind ps_in'

976997 CaseDef args sc _ <- simpleCase False (STerm Erased) False CompileTime emptyFC [] atys pdef ei

977998 return $ addDef n (CaseOp ci

978− ty atys ps_in' ps (cd { cases_totcheck = (args, sc) }),

999+ ty atys ps_in' ps (cd { cases_totcheck = (args, sc),

1000+ cases_compiletime = (args, sc) }),

9791001 inj, acc, tot, metainf) ctxt

9801002

9811003 _ -> return ctxt

@@ -989,7 +1011,7 @@ simplifyCasedef n ei uctxt

9891011 (vs, x', y')

9901012 debind (Left x) = let (vs, x') = depat [] x in

9911013 (vs, x', Impossible)

992− simpl (Right (x, y)) = Right (x, simplify uctxt [] y)

1014+ simpl (Right (x, y)) = Right (x, y) -- inline uctxt [] y)

9931015 simpl t = t

9941016

9951017addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) ->

src/Idris/Core/ProofState.hs+4−4

@@ -651,7 +651,7 @@ introTy ty mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

651651 Nothing -> x

652652 let t' = case t of

653653 x@(Bind y (Pi _ s _) _) -> x

654− _ -> hnf ctxt env t

654+ _ -> normalise ctxt env t

655655 (tyv, tyt) <- lift $ check ctxt env ty

656656-- ns <- lift $ unify ctxt env tyv t'

657657 case t' of

@@ -668,7 +668,7 @@ intro :: Maybe Name -> RunTactic

668668intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

669669 do let t' = case t of

670670 x@(Bind y (Pi _ s _) _) -> x

671− _ -> hnf ctxt env t

671+ _ -> normalise ctxt env t

672672 case t' of

673673 Bind y (Pi _ s _) t ->

674674 let n = case mn of

@@ -825,7 +825,7 @@ patbind :: Name -> RunTactic

825825patbind n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

826826 do let t' = case t of

827827 x@(Bind y (PVTy s) t) -> x

828− _ -> hnf ctxt env t

828+ _ -> normalise ctxt env t

829829 case t' of

830830 Bind y (PVTy s) t -> let t' = updsubst y (P Bound n s) t in

831831 return $ Bind n (PVar s) (Bind x (Hole t') (P Bound x t'))

@@ -839,7 +839,7 @@ compute ctxt env t = return t

839839

840840hnf_compute :: RunTactic

841841hnf_compute ctxt env (Bind x (Hole ty) sc) =

842− do let ty' = hnf ctxt env ty in

842+ do let ty' = normalise ctxt env ty in

843843-- trace ("HNF " ++ show (ty, ty')) $

844844 return $ Bind x (Hole ty') sc

845845hnf_compute ctxt env t = return t

src/Idris/Core/Typecheck.hs+2−2

@@ -116,7 +116,7 @@ check' holes tcns ctxt env top = chk (TType (UVar tcns (-5))) Nothing env top wh

116116 let fty' = case uniqueBinders (map fst env) (finalise fty) of

117117 ty@(Bind x (Pi i s k) t) -> ty

118118 _ -> uniqueBinders (map fst env)

119− $ case hnf ctxt env fty of

119+ $ case normalise ctxt env fty of

120120 ty@(Bind x (Pi i s k) t) -> ty

121121 _ -> normalise ctxt env fty

122122 case fty' of

@@ -138,7 +138,7 @@ check' holes tcns ctxt env top = chk (TType (UVar tcns (-5))) Nothing env top wh

138138 let fty' = case uniqueBinders (map fst env) (finalise fty) of

139139 ty@(Bind x (Pi i s k) t) -> ty

140140 _ -> uniqueBinders (map fst env)

141− $ case hnf ctxt env fty of

141+ $ case normalise ctxt env fty of

142142 ty@(Bind x (Pi i s k) t) -> ty

143143 _ -> normalise ctxt env fty

144144 (av, aty) <- chk u Nothing env a

src/Idris/Coverage.hs+62−2

@@ -372,6 +372,58 @@ checkAllCovering fc done top n | not (n `elem` done)

372372 x -> return () -- stop if total

373373checkAllCovering _ _ _ _ = return ()

374374

375+-- | Check whether all 'Inf' arguments to the name end up guaranteed to be

376+-- guarded by constructors (conservatively... maybe this can do better later).

377+-- Essentially, all it does is check that every branch is a constructor application

378+-- with no other function applications.

379+--

380+-- If so, set the 'AllGuarded' flag which can be used by the productivity check

381+checkIfGuarded :: Name -> Idris ()

382+checkIfGuarded n

383+ = do i <- get

384+ let ctxt = tt_ctxt i

385+ case lookupDefExact n ctxt of

386+ Just (CaseOp _ ty _ _ _ cases) ->

387+ let gnames = fst (cases_compiletime cases) in

388+ if allGuarded gnames i (snd (cases_compiletime cases))

389+ then -- trace (show (n, gnames, ty, cases_compiletime cases)) $

390+ addFnOpt n AllGuarded

391+ else return ()

392+ _ -> return ()

393+ where

394+ guard n ist = isConName n (tt_ctxt ist) || guardFlag n ist

395+ guardFlag n ist = case lookupCtxtExact n (idris_flags ist) of

396+ Nothing -> False

397+ Just fs -> AllGuarded `elem` fs

398+

399+ -- Top level thing always needs to be a constructor application if

400+ -- the delayed things are going to be definitely guarded by this definition

401+ allGuarded names i (STerm t)

402+ | (P _ fn _, args) <- unApply t,

403+ guard fn i

404+ = and (map (guardedTerm names i) args)

405+ | otherwise = False

406+ allGuarded names i (ProjCase _ alts) = and (map (guardedAlt names i) alts)

407+ allGuarded names i (Case _ _ alts) = and (map (guardedAlt names i) alts)

408+ allGuarded names i _ = True

409+

410+ guardedTerm names i (P _ v _) = v `elem` names || guard v i

411+ guardedTerm names i (Bind n (Let t v) sc)

412+ = guardedTerm names i v && guardedTerm names i sc

413+ guardedTerm names i (Bind n b sc) = False

414+ guardedTerm names i ap@(App _ _ _)

415+ | (P _ fn _, args) <- unApply ap,

416+ guard fn i || fn `elem` names

417+ = and (map (guardedTerm names i) args)

418+ guardedTerm names i (App _ f a) = False

419+ guardedTerm names i tm = True

420+

421+ guardedAlt names i (ConCase _ _ _ t) = allGuarded names i t

422+ guardedAlt names i (FnCase _ _ t) = allGuarded names i t

423+ guardedAlt names i (ConstCase _ t) = allGuarded names i t

424+ guardedAlt names i (SucCase _ t) = allGuarded names i t

425+ guardedAlt names i (DefaultCase t) = allGuarded names i t

426+

375427-- | Check if, in a given group of type declarations mut_ns, the

376428-- constructor cn : ty is strictly positive, and update the context

377429-- accordingly

@@ -605,7 +657,7 @@ buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where

605657 = findCalls cases Delayed arg pvs pargs

606658 | (P _ n _, args) <- unApply ap,

607659 Delayed <- guarded,

608− isConName n (tt_ctxt ist)

660+ isConName n (tt_ctxt ist) || allGuarded n ist

609661 = -- Still under a 'Delay' and constructor guarded, so check

610662 -- just the arguments to the constructor, remaining Delayed

611663 concatMap (\x -> findCalls cases guarded x pvs pargs) args

@@ -637,6 +689,7 @@ buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where

637689 = let nguarded = case guarded of

638690 Unguarded -> Unguarded

639691 x -> if isConName n (tt_ctxt ist)

692+ || allGuarded n ist

640693 then Guarded

641694 else Unguarded in

642695 mkChange n args pargs ++

@@ -647,7 +700,10 @@ buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where

647700 = findCalls cases Unguarded f pvs pargs ++ findCalls cases Unguarded a pvs pargs

648701 findCalls cases guarded (Bind n (Let t v) e) pvs pargs

649702 = findCalls cases Unguarded t pvs pargs ++

650− findCalls cases Unguarded v pvs pargs ++ findCalls cases guarded e (n : pvs) pargs

703+ findCalls cases Unguarded v pvs pargs ++

704+ -- Substitute in the scope since this might reveal some useful

705+ -- structure

706+ findCalls cases guarded (substV v e) pvs pargs

651707 findCalls cases guarded (Bind n t e) pvs pargs

652708 = findCalls cases Unguarded (binderTy t) pvs pargs ++

653709 findCalls cases guarded e (n : pvs) pargs

@@ -757,6 +813,10 @@ buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where

757813 patvars (Bind x (PVar _) sc) = x : patvars sc

758814 patvars _ = []

759815

816+ allGuarded n ist = case lookupCtxtExact n (idris_flags ist) of

817+ Nothing -> False

818+ Just fs -> AllGuarded `elem` fs

819+

760820checkSizeChange :: Name -> Idris Totality

761821checkSizeChange n = do

762822 ist <- getIState

src/Idris/Elab/Clause.hs+83−7

@@ -277,6 +277,10 @@ elabClauses info' fc opts n_in cs =

277277 -- all called functions, and fail if any of them are also

278278 -- 'Partial NotCovering'

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

280+ -- Add the 'AllGuarded' flag if it's guaranteed that every

281+ -- 'Inf' argument will be guarded by constructors in the result

282+ -- (allows productivity check to go under this function)

283+ checkIfGuarded n

280284 where

281285 noMatch i cs tm = all (\x -> case trim_matchClause i (delab' i x True True) tm of

282286 Right _ -> False

@@ -546,6 +550,34 @@ findUnique ctxt env (Bind n b sc)

546550 else findUnique ctxt ((n, b) : env) sc

547551findUnique _ _ _ = []

548552

553+getUnfolds (UnfoldIface n ns : _) = Just (n, ns)

554+getUnfolds (_ : xs) = getUnfolds xs

555+getUnfolds [] = Nothing

556+

557+-- Unfold the given name, interface methdods, and any function which uses it as

558+-- an argument directly. This is specifically for finding applications of

559+-- interface dictionaries and inlining them both for totality checking and for

560+-- a small performance gain.

561+getNamesToUnfold :: Name -> [Name] -> Term -> [Name]

562+getNamesToUnfold iname ms tm = nub $ iname : getNames Nothing tm ++ ms

563+ where

564+ getNames under fn@(App _ _ _)

565+ | (f, args) <- unApply fn

566+ = let under' = case f of

567+ P _ fn _ -> Just fn

568+ _ -> Nothing

569+ in

570+ getNames under f ++ concatMap (getNames under') args

571+ getNames (Just under) (P _ ref _)

572+ = if ref == iname then [under] else []

573+ getNames under (Bind n (Let t v) sc)

574+ = getNames Nothing t ++

575+ getNames Nothing v ++

576+ getNames Nothing sc

577+ getNames under (Bind n b sc) = getNames Nothing (binderTy b) ++

578+ getNames Nothing sc

579+ getNames _ _ = []

580+

549581-- | Return the elaborated LHS/RHS, and the original LHS with implicits added

550582elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->

551583 Idris (Either Term (Term, Term), PTerm)

@@ -684,7 +716,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

684716 logElab 2 $ "RHS: " ++ show (map fst newargs_all) ++ " " ++ showTmImpls rhs

685717 ctxt <- getContext -- new context with where block added

686718 logElab 5 "STARTING CHECK"

687− ((rhs', defer, holes, is, probs, ctxt', newDecls, highlights, newGName), _) <-

719+ ((rhsElab, defer, holes, is, probs, ctxt', newDecls, highlights, newGName), _) <-

688720 tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patRHS") clhsty initEState

689721 (do pbinds ist lhs_tm

690722 -- proof search can use explicitly written names

@@ -713,7 +745,20 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

713745 when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_,_) -> (x,y)) probs)

714746

715747 logElab 5 "DONE CHECK"

716− logElab 4 $ "---> " ++ show rhs'

748+ logElab 3 $ "---> " ++ show rhsElab

749+ ctxt <- getContext

750+

751+ let rhs' = case getUnfolds opts of

752+ Just (n, ms) ->

753+ let ns = getNamesToUnfold n ms rhsElab in

754+ unfold ctxt [] (map (\n -> (n, 1)) ns) rhsElab

755+ _ -> rhsElab

756+

757+ when (not (null (getUnfolds opts))) $

758+ logElab 1 $ "----- " ++ show (getUnfolds opts) ++

759+ "\nUnfolded " ++ show rhsElab ++ "\n" ++

760+ "to " ++ show rhs'

761+

717762 when (not (null defer)) $ logElab 1 $ "DEFERRED " ++

718763 show (map (\ (n, (_,_,t,_)) -> (n, t)) defer)

719764

@@ -880,7 +925,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

880925 let wval = rhs_trans info $ addImplBound i (map fst bargs) wval_in

881926 logElab 5 ("Checking " ++ showTmImpls wval)

882927 -- Elaborate wval in this context

883− ((wval', defer, is, ctxt', newDecls, highlights, newGName), _) <-

928+ ((wvalElab, defer, is, ctxt', newDecls, highlights, newGName), _) <-

884929 tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "withRHS")

885930 (bindTyArgs PVTy bargs infP) initEState

886931 (do pbinds i lhs_tm

@@ -902,7 +947,20 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

902947 let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, True))) def'

903948 addDeferred def''

904949 mapM_ (elabCaseBlock info opts) is

950+

951+ let wval' = case getUnfolds opts of

952+ Just (n, ms) ->

953+ let ns = getNamesToUnfold n ms wvalElab in

954+ unfold ctxt [] (map (\n -> (n, 1)) ns) wvalElab

955+ _ -> wvalElab

956+

905957 logElab 5 ("Checked wval " ++ show wval')

958+

959+ when (not (null (getUnfolds opts))) $

960+ logElab 1 $ "----- " ++ show (getUnfolds opts) ++

961+ "\nUnfolded wval " ++ show wvalElab ++ "\n" ++

962+ "to " ++ show wval'

963+

906964

907965 ctxt <- getContext

908966 (cwval, cwvalty) <- recheckC (constraintNS info) fc id [] (getInferTerm wval')

@@ -973,9 +1031,13 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

9731031 wb <- mapM (mkAuxC mpn wname lhs (map fst bargs_pre) (map fst bargs_post))

9741032 withblock

9751033 logElab 3 ("with block " ++ show wb)

976− -- propagate totality assertion to the new definitions

977− setFlags wname [Inlinable]

978− when (AssertTotal `elem` opts) $ setFlags wname [Inlinable, AssertTotal]

1034+ -- propagate totality assertion and unfold flags to the new definitions

1035+ let uflags = case getUnfolds opts of

1036+ Just (n, ns) -> [UnfoldIface n ns]

1037+ _ -> []

1038+ setFlags wname ([Inlinable] ++ uflags)

1039+ when (AssertTotal `elem` opts) $

1040+ setFlags wname ([Inlinable, AssertTotal] ++ uflags)

9791041 i <- getIState

9801042 let rhstrans' = updateWithTerm i mpn wname lhs (map fst bargs_pre) (map fst (bargs_post))

9811043 . rhs_trans info

@@ -995,7 +1057,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

9951057 logElab 5 ("New RHS " ++ showTmImpls rhs)

9961058 ctxt <- getContext -- New context with block added

9971059 i <- getIState

998− ((rhs', defer, is, ctxt', newDecls, highlights, newGName), _) <-

1060+ ((rhsElab, defer, is, ctxt', newDecls, highlights, newGName), _) <-

9991061 tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "wpatRHS") clhsty initEState

10001062 (do pbinds i lhs_tm

10011063 setNextName

@@ -1005,9 +1067,23 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

10051067 tt <- get_term

10061068 return (tt, d, is, ctxt', newDecls, highlights, newGName))

10071069 setContext ctxt'

1070+

10081071 processTacticDecls info newDecls

10091072 sendHighlighting highlights

10101073 updateIState $ \i -> i { idris_name = newGName }

1074+

1075+ ctxt <- getContext

1076+ let rhs' = case getUnfolds opts of

1077+ Just (n, ms) ->

1078+ let ns = getNamesToUnfold n ms rhsElab in

1079+ unfold ctxt [] (map (\n -> (n, 1)) ns) rhsElab

1080+ _ -> rhsElab

1081+

1082+ when (not (null (getUnfolds opts))) $

1083+ logElab 3 $ "----- " ++ show (getUnfolds opts) ++

1084+ "\nUnfolded with RHS " ++ show rhsElab ++ "\n" ++

1085+ "to " ++ show rhs'

1086+

10111087

10121088 def' <- checkDef info fc iderr True defer

10131089 let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, True))) def'

src/Idris/Elab/Implementation.hs+10−1

@@ -148,11 +148,14 @@ elabImplementation info syn doc argDocs what fc cs parents acc opts n nfc ps pex

148148 (decorate ns iname n,

149149 op, coninsert cs pextra t', t'))

150150 (interface_methods ci)

151+

151152 logElab 5 (show (mtys, (iimpps ++ ips)))

152153 logElab 5 ("Before defaults: " ++ show ds ++ "\n" ++ show (map fst (interface_methods ci)))

153154 let ds_defs = insertDefaults ist iname (interface_defaults ci) ns ds

154155 logElab 3 ("After defaults: " ++ show ds_defs ++ "\n")

155− let ds' = reorderDefs (map fst (interface_methods ci)) ds_defs

156+

157+ let ds' = map (addUnfold iname (map fst (interface_methods ci))) $

158+ reorderDefs (map fst (interface_methods ci)) ds_defs

156159 logElab 1 ("Reordered: " ++ show ds' ++ "\n")

157160

158161 mapM_ (warnMissing ds' ns iname) (map fst (interface_methods ci))

@@ -220,6 +223,12 @@ elabImplementation info syn doc argDocs what fc cs parents acc opts n nfc ps pex

220223 [PConstant NoFC (AType (ATInt ITNative))] -> True

221224 _ -> False

222225

226+ addUnfold iname ms (PTy doc docs syn fc opts n fc' tm)

227+ = PTy doc docs syn fc (UnfoldIface iname ms : opts) n fc' tm

228+ addUnfold iname ms (PClauses fc opts n cs)

229+ = PClauses fc (UnfoldIface iname ms : opts) n cs

230+ addUnfold iname ms dec = dec

231+

223232 mkiname n' ns ps' expn' =

224233 case expn' of

225234 Nothing -> case ns of

src/Idris/Elab/Term.hs+4−4

@@ -387,7 +387,7 @@ elab ist info emode opts fn tm

387387 highlightSource fc' (AnnConst c)

388388 elab' ina fc (PQuote r) = do fill r; solve

389389 elab' ina _ (PTrue fc _) =

390− do hnf_compute

390+ do compute

391391 g <- goal

392392 case g of

393393 TType _ -> elab' ina (Just fc) (PRef fc [] unitTy)

@@ -421,7 +421,7 @@ elab ist info emode opts fn tm

421421 pexp l, pexp r]))

422422

423423 elab' ina _ (PPair fc hls _ l r)

424− = do hnf_compute

424+ = do compute

425425 g <- goal

426426 let (tc, _) = unApply g

427427 case g of

@@ -444,7 +444,7 @@ elab ist info emode opts fn tm

444444 IsType -> asType

445445 IsTerm -> asValue

446446 TypeOrTerm ->

447− do hnf_compute

447+ do compute

448448 g <- goal

449449 case g of

450450 TType _ -> asType

@@ -2634,7 +2634,7 @@ runTac autoSolve ist perhapsFC fn tac

26342634 (value, _) <- get_type_val (Var letn)

26352635 ctxt <- get_context

26362636 env <- get_env

2637− let value' = hnf ctxt env value

2637+ let value' = normalise ctxt env value

26382638 runTac autoSolve ist perhapsFC fn (Exact $ PQuote (reflect value'))

26392639 runT (Fill v) = do attack -- let x = fill x in ...

26402640 tyn <- getNameFrom (sMN 0 "letty")

src/Idris/Elab/Type.hs+1−1

@@ -210,7 +210,7 @@ elabType' norm info syn doc argDocs fc opts n nfc ty' = {- let ty' = piBind (par

210210 return (n, d')) argDocs

211211 addDocStr n doc' argDocs'

212212 addIBC (IBCDoc n)

213− addIBC (IBCFlags n opts')

213+ addIBC (IBCFlags n)

214214 fputState (opt_inaccessible . ist_optimisation n) inacc

215215 addIBC (IBCOpt n)

216216 when (Implicit `elem` opts') $ do addCoercion n

src/Idris/IBC.hs+13−4

@@ -47,7 +47,7 @@ import System.Directory

4747import System.FilePath

4848

4949ibcVersion :: Word16

50−ibcVersion = 151

50+ibcVersion = 152

5151

5252-- | When IBC is being loaded - we'll load different things (and omit

5353-- different structures/definitions) depending on which phase we're in.

@@ -313,7 +313,10 @@ ibc i (IBCCG n) f = case lookupCtxtExact n (idris_callgraph i) of

313313 _ -> ifail "IBC write failed"

314314ibc i (IBCCoercion n) f = return f { ibc_coercions = n : ibc_coercions f }

315315ibc i (IBCAccess n a) f = return f { ibc_access = (n,a) : ibc_access f }

316−ibc i (IBCFlags n a) f = return f { ibc_flags = (n,a) : ibc_flags f }

316+ibc i (IBCFlags n) f

317+ = case lookupCtxtExact n (idris_flags i) of

318+ Just a -> return f { ibc_flags = (n,a): ibc_flags f }

319+ _ -> ifail "IBC write failed"

317320ibc i (IBCFnInfo n a) f = return f { ibc_fninfo = (n,a) : ibc_fninfo f }

318321ibc i (IBCTotal n a) f = return f { ibc_total = (n,a) : ibc_total f }

319322ibc i (IBCInjective n a) f = return f { ibc_injective = (n,a) : ibc_injective f }

@@ -1208,7 +1211,7 @@ instance Binary FnOpt where

12081211 AssertTotal -> putWord8 3

12091212 Specialise x -> do putWord8 4

12101213 put x

1211− Coinductive -> putWord8 5

1214+ AllGuarded -> putWord8 5

12121215 PartialFn -> putWord8 6

12131216 Implicit -> putWord8 7

12141217 Reflection -> putWord8 8

@@ -1223,6 +1226,9 @@ instance Binary FnOpt where

12231226 PEGenerated -> putWord8 16

12241227 StaticFn -> putWord8 17

12251228 OverlappingDictionary -> putWord8 18

1229+ UnfoldIface x ns -> do putWord8 19

1230+ put x

1231+ put ns

12261232 get

12271233 = do i <- getWord8

12281234 case i of

@@ -1232,7 +1238,7 @@ instance Binary FnOpt where

12321238 3 -> return AssertTotal

12331239 4 -> do x <- get

12341240 return (Specialise x)

1235− 5 -> return Coinductive

1241+ 5 -> return AllGuarded

12361242 6 -> return PartialFn

12371243 7 -> return Implicit

12381244 8 -> return Reflection

@@ -1247,6 +1253,9 @@ instance Binary FnOpt where

12471253 16 -> return PEGenerated

12481254 17 -> return StaticFn

12491255 18 -> return OverlappingDictionary

1256+ 19 -> do x <- get

1257+ ns <- get

1258+ return (UnfoldIface x ns)

12501259 _ -> error "Corrupted binary data for FnOpt"

12511260

12521261instance Binary Fixity where

test/totality013/expected+2−3

@@ -1,4 +1,3 @@

11totality013a.idr:5:3:

2−Main.foo is possibly not total due to recursive path Main.mtot --> Main.mtot --> Main.mtot --> Main.mtot

3−totality013a.idr:9:3:

4−Main.mtot is possibly not total due to recursive path Main.mtot --> Main.mtot --> Main.mtot

2+Main.foo is possibly not total due to recursive path Main.foo --> Main.mtot --> Main.mtot --> Main.mtot

3+totality013a.idr:9:3:Main.mtot is possibly not total due to: Main.foo

test/totality015/totality015.idr+1−1

@@ -12,7 +12,7 @@ data ConsoleIO : Type -> Type where

1212 Do : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b

1313

1414(>>=) : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b

15−(>>=) = Do

15+(>>=) = Do

1616

1717data Fuel = Dry | More (Lazy Fuel)

1818