daab1a3 · Idris-dev · git.iko.soy

lib/Builtins.idr+2−2

compare with master

unifiedsplit

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

34trace_malloc : a -> a

35trace_malloc x = x -- compiled specially

36

37−abstract

37+abstract %assert_total -- need to pretend

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

39believe_me x = prim__believe_me _ _ x

40

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

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

42really_believe_me : a -> b

43really_believe_me x = prim__believe_me _ _ x

44

src/Idris/AbsSyntax.hs+3

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

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

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

86

87+clear_totcheck :: Idris ()

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

89+

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

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

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

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

89

92

src/Idris/Coverage.hs+5−5

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

313 -- typechecking decidable

314 case t' of

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

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

316+ p@(Partial _) ->

317−-- do setAccessibility n Frozen

317+ do setAccessibility n Frozen

318−-- addIBC (IBCAccess n Frozen)

318+ addIBC (IBCAccess n Frozen)

319−-- logLvl 5 $ "HIDDEN: "

319+ logLvl 5 $ "HIDDEN: "

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

320+ ++ show n ++ show p

321 _ -> return ()

322 return t'

323 _ -> 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

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

685 addIBC (IBCCG n)

686 _ -> return ()

687+ return ()

687 -- addIBC (IBCTotal n tot)

688 -- addIBC (IBCTotal n tot)

688 [] -> return ()

689 [] -> return ()

689 return ()

690 return ()

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

1495elabDecl' what info (PMutual f ps)

1496elabDecl' what info (PMutual f ps)

1496 = do mapM_ (elabDecl ETypes info) ps

1497 = do mapM_ (elabDecl ETypes info) ps

1497 mapM_ (elabDecl EDefns info) ps

1498 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+

1498elabDecl' what info (PParams f ns ps)

1505elabDecl' what info (PParams f ns ps)

1499 = do i <- getIState

1506 = do i <- getIState

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

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

src/Idris/Parser.hs+14−3

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

134 -- Now add all the declarations to the context

135 v <- verbose

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

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

137− elabDecls toplevel ds

140+ elabDecls toplevel (map toMutual ds)

138 i <- getIState

141 i <- getIState

139 -- simplify every definition do give the totality checker

142 -- simplify every definition do give the totality checker

140 -- a better chance

143 -- a better chance

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

144 -- build size change graph from simplified definitions

147 -- build size change graph from simplified definitions

145 iLOG "Totality checking"

148 iLOG "Totality checking"

146 i <- getIState

149 i <- getIState

147− mapM_ buildSCG (idris_totcheck i)

150+-- mapM_ buildSCG (idris_totcheck i)

148− mapM_ checkDeclTotality (idris_totcheck i)

151+-- mapM_ checkDeclTotality (idris_totcheck i)

149 iLOG ("Finished " ++ f)

152 iLOG ("Finished " ++ f)

150 ibcsd <- valIBCSubDir i

153 ibcsd <- valIBCSubDir i

151 iLOG "Universe checking"

154 iLOG "Universe checking"

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

166 namespaces [] ds = ds

169 namespaces [] ds = ds

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

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

168

171

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+

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

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

170addHides xs = do i <- getIState

181addHides xs = do i <- getIState

171 let defh = default_access i

182 let defh = default_access i