7e78f0a · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Extend positivity check for mutual data types

7e78f0aEdwin Brady12 years ago

src/Idris/AbsSyntaxTree.hs+2−1

compare with master

unifiedsplit

@@ -884,7 +884,8 @@ deriving instance NFData OptInfo

884data TypeInfo = TI { con_names :: [Name],

885 codata :: Bool,

886 data_opts :: DataOpts,

887− param_pos :: [Int] }

887+ param_pos :: [Int],

888+ mutual_types :: [Name] }

888 deriving Show

889 deriving Show

889{-!

890{-!

890deriving instance Binary TypeInfo

891deriving instance Binary TypeInfo

src/Idris/Coverage.hs+19−9

@@ -211,7 +211,7 @@ genAll i args

211 let p = resugar (PApp fc (PRef fc n) (zipWith upd xs' xs))

212 let tyn = getTy n (tt_ctxt i)

213 case lookupCtxt tyn (idris_datatypes i) of

214− (TI ns _ _ _ : _) -> p : map (mkPat fc) (ns \\ [n])

214+ (TI ns _ _ _ _ : _) -> p : map (mkPat fc) (ns \\ [n])

215 _ -> [p]

216 ops fc n arg o = return Placeholder

217

@@ -265,19 +265,21 @@ checkAllCovering fc done top n | not (n `elem` done)

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

266checkAllCovering _ _ _ _ = return ()

267

268+-- Check if, in a given group of type declarations mut_ns,

268−-- Check if, in a given type n, the constructor cn : ty is strictly positive,

269+-- the constructor cn : ty is strictly positive,

269-- and update the context accordingly

270-- and update the context accordingly

270

271

271−checkPositive :: Name -> (Name, Type) -> Idris ()

272+checkPositive :: [Name] -> (Name, Type) -> Idris Totality

272−checkPositive n (cn, ty')

273+checkPositive mut_ns (cn, ty')

273 = do let ty = delazy ty'

274 = do let ty = delazy ty'

274 let p = cp ty

275 let p = cp ty

275 i <- getIState

276 i <- getIState

276 let tot = if p then Total (args ty) else Partial NotPositive

277 let tot = if p then Total (args ty) else Partial NotPositive

277 let ctxt' = setTotal cn tot (tt_ctxt i)

278 let ctxt' = setTotal cn tot (tt_ctxt i)

278 putIState (i { tt_ctxt = ctxt' })

279 putIState (i { tt_ctxt = ctxt' })

279− logLvl 5 $ "Constructor " ++ show cn ++ " is " ++ show tot

280+ logLvl 5 $ "Constructor " ++ show cn ++ " is " ++ show tot ++ " with " ++ show mut_ns

280 addIBC (IBCTotal cn tot)

281 addIBC (IBCTotal cn tot)

282+ return tot

281 where

283 where

282 args t = [0..length (getArgTys t)-1]

284 args t = [0..length (getArgTys t)-1]

283

285

@@ -286,7 +288,7 @@ checkPositive n (cn, ty')

286

288

287 posArg (Bind _ (Pi nty) sc)

289 posArg (Bind _ (Pi nty) sc)

288 | (P _ n' _, args) <- unApply nty

290 | (P _ n' _, args) <- unApply nty

289− = n /= n' && posArg sc

291+ = n' `notElem` mut_ns && posArg sc

290 posArg t = True

292 posArg t = True

291

293

292calcProd :: IState -> FC -> Name -> [([Name], Term, Term)] -> Idris Totality

294calcProd :: IState -> FC -> Name -> [([Name], Term, Term)] -> Idris Totality

@@ -335,7 +337,7 @@ calcProd i fc topn pats

335 cotype (DCon _ _) n ty

337 cotype (DCon _ _) n ty

336 | (P _ t _, _) <- unApply (getRetTy ty)

338 | (P _ t _, _) <- unApply (getRetTy ty)

337 = case lookupCtxt t (idris_datatypes i) of

339 = case lookupCtxt t (idris_datatypes i) of

338− [TI _ True _ _] -> True

340+ [TI _ True _ _ _] -> True

339 _ -> False

341 _ -> False

340 cotype nt n ty = False

342 cotype nt n ty = False

341

343

@@ -383,6 +385,14 @@ checkTotality path fc n

383 setTotality n t'

385 setTotality n t'

384 addIBC (IBCTotal n t')

386 addIBC (IBCTotal n t')

385 return t'

387 return t'

388+ [TyDecl (DCon _ _) ty] ->

389+ case unApply (getRetTy ty) of

390+ (P _ tyn _, _) -> do

391+ let ms = case lookupCtxt tyn (idris_datatypes i) of

392+ [TI _ _ _ _ xs@(_:_)] -> xs

393+ ts -> [tyn]

394+ checkPositive ms (n, ty)

395+ _-> return $ Total []

386 _ -> return $ Total []

396 _ -> return $ Total []

387 x -> return x

397 x -> return x

388 case t' of

398 case t' of

@@ -556,7 +566,7 @@ buildSCG' ist pats args = nub $ concatMap scgPat pats where

556

566

557 isInductive (P _ nty _) (P _ nty' _) =

567 isInductive (P _ nty _) (P _ nty' _) =

558 let co = case lookupCtxt nty (idris_datatypes ist) of

568 let co = case lookupCtxt nty (idris_datatypes ist) of

559− [TI _ x _ _] -> x

569+ [TI _ x _ _ _] -> x

560 _ -> False in

570 _ -> False in

561 nty == nty' && not co

571 nty == nty' && not co

562 isInductive _ _ = False

572 isInductive _ _ = False

@@ -639,7 +649,7 @@ checkMP ist i mp = if i > 0

639 = case lookupTotal f (tt_ctxt ist) of

649 = case lookupTotal f (tt_ctxt ist) of

640 [Total _] -> Unchecked -- okay so far

650 [Total _] -> Unchecked -- okay so far

641 [Partial _] -> Partial (Other [f])

651 [Partial _] -> Partial (Other [f])

642− x -> error (show x)

652+ x -> error $ "CAN'T HAPPEN: " ++ (show x)

643 | [TyDecl (TCon _ _) _] <- lookupDef f (tt_ctxt ist)

653 | [TyDecl (TCon _ _) _] <- lookupDef f (tt_ctxt ist)

644 = Total []

654 = Total []

645 tryPath desc path (e@(f, args) : es) arg

655 tryPath desc path (e@(f, args) : es) arg

src/Idris/DeepSeq.hs+1−1

@@ -290,7 +290,7 @@ instance NFData OptInfo where

290 = rnf x1 `seq` rnf x2 `seq` ()

291

292instance NFData TypeInfo where

293− rnf (TI x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

293+ rnf (TI x1 x2 x3 x4 x5) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

294

295instance (NFData t) => NFData (DSL' t) where

296 rnf (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9)

src/Idris/ElabDecls.hs+22−4

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

125 let (t, _) = unApply (getRetTy nty')

126 let corec = case t of

127 P _ rcty _ -> case lookupCtxt rcty (idris_datatypes i) of

128− [TI _ True _ _] -> True

128+ [TI _ True _ _ _] -> True

129 _ -> False

130 _ -> False

131 -- Productivity checking now via checking for guarded 'Delay'

@@ -256,8 +256,10 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

256 let as = map (const Nothing) (getArgTys cty)

257 let params = findParams (map snd cons)

258 logLvl 2 $ "Parameters : " ++ show params

259+ -- TI contains information about mutually declared types - this will

260+ -- be updated when the mutual block is complete

259 putIState (i { idris_datatypes =

261 putIState (i { idris_datatypes =

260− addDef n (TI (map fst cons) codata opts params)

262+ addDef n (TI (map fst cons) codata opts params [n])

261 (idris_datatypes i) })

263 (idris_datatypes i) })

262 addIBC (IBCDef n)

264 addIBC (IBCDef n)

263 addIBC (IBCData n)

265 addIBC (IBCData n)

@@ -269,7 +271,8 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

269 -- TMP HACK! Make this a data option

271 -- TMP HACK! Make this a data option

270 updateContext (addDatatype (Data n ttag cty cons))

272 updateContext (addDatatype (Data n ttag cty cons))

271 updateContext (setMetaInformation n metainf)

273 updateContext (setMetaInformation n metainf)

274+ mapM_ totcheck (zip (repeat fc) (map fst cons))

272− mapM_ (checkPositive n) cons

275+-- mapM_ (checkPositive n) cons

273

276

274 -- if there's exactly one constructor,

277 -- if there's exactly one constructor,

275 -- mark both the type and the constructor as detaggable

278 -- mark both the type and the constructor as detaggable

@@ -1617,7 +1620,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1617 rev <- case ret_fam of

1620 rev <- case ret_fam of

1618 P _ rfamn _ ->

1621 P _ rfamn _ ->

1619 case lookupCtxt rfamn (idris_datatypes i) of

1622 case lookupCtxt rfamn (idris_datatypes i) of

1620− [TI _ _ dopts _] ->

1623+ [TI _ _ dopts _ _] ->

1621 return (DataErrRev `elem` dopts)

1624 return (DataErrRev `elem` dopts)

1622 _ -> return False

1625 _ -> return False

1623 _ -> return False

1626 _ -> return False

@@ -2340,6 +2343,11 @@ elabDecl' what info (PMutual f ps)

2340 [p] -> elabDecl what info p

2343 [p] -> elabDecl what info p

2341 _ -> do mapM_ (elabDecl ETypes info) ps

2344 _ -> do mapM_ (elabDecl ETypes info) ps

2342 mapM_ (elabDecl EDefns info) ps

2345 mapM_ (elabDecl EDefns info) ps

2346+ -- record mutually defined data definitions

2347+ let datans = concatMap declared (filter isDataDecl ps)

2348+ mapM_ (setMutData datans) datans

2349+ iLOG $ "Rechecking for positivity " ++ show datans

2350+ mapM_ (\x -> do setTotality x Unchecked) datans

2343 -- Do totality checking after entire mutual block

2351 -- Do totality checking after entire mutual block

2344 i <- get

2352 i <- get

2345 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n

2353 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n

@@ -2348,6 +2356,16 @@ elabDecl' what info (PMutual f ps)

2348 mapM_ buildSCG (idris_totcheck i)

2356 mapM_ buildSCG (idris_totcheck i)

2349 mapM_ checkDeclTotality (idris_totcheck i)

2357 mapM_ checkDeclTotality (idris_totcheck i)

2350 clear_totcheck

2358 clear_totcheck

2359+ where isDataDecl (PData _ _ _ _ _ _) = True

2360+ isDataDecl _ = False

2361+

2362+ setMutData ns n

2363+ = do i <- getIState

2364+ case lookupCtxt n (idris_datatypes i) of

2365+ [x] -> do let x' = x { mutual_types = ns }

2366+ putIState $ i { idris_datatypes

2367+ = addDef n x' (idris_datatypes i) }

2368+ _ -> return ()

2351

2369

2352elabDecl' what info (PParams f ns ps)

2370elabDecl' what info (PParams f ns ps)

2353 = do i <- getIState

2371 = do i <- getIState

src/Idris/IBC.hs+8−6

@@ -30,7 +30,7 @@ import Codec.Compression.Zlib (compress)

30import Util.Zlib (decompressEither)

32ibcVersion :: Word8

33−ibcVersion = 73

33+ibcVersion = 74

35data IBCFile = IBCFile { ver :: Word8,

36 sourcefile :: FilePath,

@@ -2152,15 +2152,17 @@ instance Binary OptInfo where

2152 return (Optimise x1 x2)

2153

2154instance Binary TypeInfo where

2155− put (TI x1 x2 x3 x4) = do put x1

2155+ put (TI x1 x2 x3 x4 x5) = do put x1

2156− put x2

2156+ put x2

2157− put x3

2157+ put x3

2158− put x4

2158+ put x4

2159+ put x5

2159 get = do x1 <- get

2160 get = do x1 <- get

2160 x2 <- get

2161 x2 <- get

2161 x3 <- get

2162 x3 <- get

2162 x4 <- get

2163 x4 <- get

2164+ x5 <- get

2163− return (TI x1 x2 x3 x4)

2165+ return (TI x1 x2 x3 x4 x5)

2164

2166

2165instance Binary SynContext where

2167instance Binary SynContext where

2166 put x

2168 put x