daab1a3 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Partially defined names should not reduce at compile-time

This has been the spec for a long time, but wasn't implemented fully since the totality checker wasn't strong enough to find some obviously total things. This is now switched on --- functions are checked for totality after every mutual block, or every individual function (if not mutual).

commitdaab1a3e9fe9614f141b2172f0f2bae9f4b5680b authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 17 Sep 2013, 12:39 (13 years ago) parent3a8d9db

5 files changed+31−10

compare with master

unifiedsplit

lib/Builtins.idr+2−2 src/Idris/AbsSyntax.hs+3 src/Idris/Coverage.hs+5−5 src/Idris/ElabDecls.hs+7 src/Idris/Parser.hs+14−3

lib/Builtins.idr+2−2

@@ -34,11 +34,11 @@ malloc size x = x -- compiled specially

3434trace_malloc : a -> a

3535trace_malloc x = x -- compiled specially

3636

37−abstract

37+abstract %assert_total -- need to pretend

3838believe_me : a -> b -- compiled specially as id, use with care!

3939believe_me x = prim__believe_me _ _ x

4040

41−public -- reduces at compile time, use with extreme care!

41+public %assert_total -- reduces at compile time, use with extreme care!

4242really_believe_me : a -> b

4343really_believe_me x = prim__believe_me _ _ x

4444

src/Idris/AbsSyntax.hs+3

@@ -84,6 +84,9 @@ addTrans t = do i <- getIState

8484totcheck :: (FC, Name) -> Idris ()

8585totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }

8686

87+clear_totcheck :: Idris ()

88+clear_totcheck = do i <- getIState; putIState $ i { idris_totcheck = [] }

89+

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

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

8992

src/Idris/Coverage.hs+5−5

@@ -313,11 +313,11 @@ checkTotality path fc n

313313 -- typechecking decidable

314314 case t' of

315315-- FIXME: Put this back when we can handle mutually recursive things

316−-- p@(Partial _) ->

317−-- do setAccessibility n Frozen

318−-- addIBC (IBCAccess n Frozen)

319−-- logLvl 5 $ "HIDDEN: "

320−-- ++ show n ++ show p

316+ p@(Partial _) ->

317+ do setAccessibility n Frozen

318+ addIBC (IBCAccess n Frozen)

319+ logLvl 5 $ "HIDDEN: "

320+ ++ show n ++ show p

321321 _ -> return ()

322322 return t'

323323 _ -> return $ Total []

src/Idris/ElabDecls.hs+7

@@ -684,6 +684,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

684684 addToCalledG n (nub (map fst calls)) -- plus names in type!

685685 addIBC (IBCCG n)

686686 _ -> return ()

687+ return ()

687688 -- addIBC (IBCTotal n tot)

688689 [] -> return ()

689690 return ()

@@ -1495,6 +1496,12 @@ elabDecl' what info d@(PClauses f o n ps)

14951496elabDecl' what info (PMutual f ps)

14961497 = do mapM_ (elabDecl ETypes info) ps

14971498 mapM_ (elabDecl EDefns info) ps

1499+ -- Do totality checking after entire mutual block

1500+ i <- get

1501+ mapM_ buildSCG (idris_totcheck i)

1502+ mapM_ checkDeclTotality (idris_totcheck i)

1503+ clear_totcheck

1504+

14981505elabDecl' what info (PParams f ns ps)

14991506 = do i <- getIState

15001507 iLOG $ "Expanding params block with " ++ show ns ++ " decls " ++

src/Idris/Parser.hs+14−3

@@ -134,7 +134,10 @@ loadSource lidr f

134134 -- Now add all the declarations to the context

135135 v <- verbose

136136 when v $ iputStrLn $ "Type checking " ++ f

137− elabDecls toplevel ds

137+ -- we totality check after every Mutual block, so if

138+ -- anything is a single definition, wrap it in a

139+ -- mutual block on its own

140+ elabDecls toplevel (map toMutual ds)

138141 i <- getIState

139142 -- simplify every definition do give the totality checker

140143 -- a better chance

@@ -144,8 +147,8 @@ loadSource lidr f

144147 -- build size change graph from simplified definitions

145148 iLOG "Totality checking"

146149 i <- getIState

147− mapM_ buildSCG (idris_totcheck i)

148− mapM_ checkDeclTotality (idris_totcheck i)

150+-- mapM_ buildSCG (idris_totcheck i)

151+-- mapM_ checkDeclTotality (idris_totcheck i)

149152 iLOG ("Finished " ++ f)

150153 ibcsd <- valIBCSubDir i

151154 iLOG "Universe checking"

@@ -166,6 +169,14 @@ loadSource lidr f

166169 namespaces [] ds = ds

167170 namespaces (x:xs) ds = [PNamespace x (namespaces xs ds)]

168171

172+ toMutual m@(PMutual _ d) = m

173+ toMutual x = let r = PMutual (FC "single mutual" 0) [x] in

174+ case x of

175+ PClauses _ _ _ _ -> r

176+ PClass _ _ _ _ _ _ _ -> r

177+ PInstance _ _ _ _ _ _ _ _ -> r

178+ _ -> x

179+

169180addHides :: [(Name, Maybe Accessibility)] -> Idris ()

170181addHides xs = do i <- getIState

171182 let defh = default_access i