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

git.iko.soy/Idris-dev

Extend positivity check for mutual data types

Needs a make lib_clean

commit7e78f0acea696a4ebd4a652c16fe5aef3bdf9457 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 28 May 2014, 23:00 (12 years ago) parent00793ac

5 files changed+52−21

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+2−1 src/Idris/Coverage.hs+19−9 src/Idris/DeepSeq.hs+1−1 src/Idris/ElabDecls.hs+22−4 src/Idris/IBC.hs+8−6

src/Idris/AbsSyntaxTree.hs+2−1

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

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

885885 codata :: Bool,

886886 data_opts :: DataOpts,

887− param_pos :: [Int] }

887+ param_pos :: [Int],

888+ mutual_types :: [Name] }

888889 deriving Show

889890{-!

890891deriving instance Binary TypeInfo

src/Idris/Coverage.hs+19−9

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

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

212212 let tyn = getTy n (tt_ctxt i)

213213 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])

215215 _ -> [p]

216216 ops fc n arg o = return Placeholder

217217

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

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

266266checkAllCovering _ _ _ _ = return ()

267267

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

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

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

269270-- and update the context accordingly

270271

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

272−checkPositive n (cn, ty')

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

273+checkPositive mut_ns (cn, ty')

273274 = do let ty = delazy ty'

274275 let p = cp ty

275276 i <- getIState

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

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

278279 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

280281 addIBC (IBCTotal cn tot)

282+ return tot

281283 where

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

283285

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

286288

287289 posArg (Bind _ (Pi nty) sc)

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

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

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

290292 posArg t = True

291293

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

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

335337 cotype (DCon _ _) n ty

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

337339 = case lookupCtxt t (idris_datatypes i) of

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

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

339341 _ -> False

340342 cotype nt n ty = False

341343

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

383385 setTotality n t'

384386 addIBC (IBCTotal n t')

385387 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 []

386396 _ -> return $ Total []

387397 x -> return x

388398 case t' of

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

556566

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

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

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

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

560570 _ -> False in

561571 nty == nty' && not co

562572 isInductive _ _ = False

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

639649 = case lookupTotal f (tt_ctxt ist) of

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

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

642− x -> error (show x)

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

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

644654 = Total []

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

src/Idris/DeepSeq.hs+1−1

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

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

291291

292292instance 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` ()

294294

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

296296 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

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

126126 let corec = case t of

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

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

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

129129 _ -> False

130130 _ -> False

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

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

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

257257 let params = findParams (map snd cons)

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

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

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

259261 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])

261263 (idris_datatypes i) })

262264 addIBC (IBCDef n)

263265 addIBC (IBCData n)

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

269271 -- TMP HACK! Make this a data option

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

271273 updateContext (setMetaInformation n metainf)

272− mapM_ (checkPositive n) cons

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

275+-- mapM_ (checkPositive n) cons

273276

274277 -- if there's exactly one constructor,

275278 -- 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)

16171620 rev <- case ret_fam of

16181621 P _ rfamn _ ->

16191622 case lookupCtxt rfamn (idris_datatypes i) of

1620− [TI _ _ dopts _] ->

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

16211624 return (DataErrRev `elem` dopts)

16221625 _ -> return False

16231626 _ -> return False

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

23402343 [p] -> elabDecl what info p

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

23422345 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

23432351 -- Do totality checking after entire mutual block

23442352 i <- get

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

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

23482356 mapM_ buildSCG (idris_totcheck i)

23492357 mapM_ checkDeclTotality (idris_totcheck i)

23502358 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 ()

23512369

23522370elabDecl' what info (PParams f ns ps)

23532371 = do i <- getIState

src/Idris/IBC.hs+8−6

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

3030import Util.Zlib (decompressEither)

3131

3232ibcVersion :: Word8

33−ibcVersion = 73

33+ibcVersion = 74

3434

3535data IBCFile = IBCFile { ver :: Word8,

3636 sourcefile :: FilePath,

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

21522152 return (Optimise x1 x2)

21532153

21542154instance Binary TypeInfo where

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

2156− put x2

2157− put x3

2158− put x4

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

2156+ put x2

2157+ put x3

2158+ put x4

2159+ put x5

21592160 get = do x1 <- get

21602161 x2 <- get

21612162 x3 <- get

21622163 x4 <- get

2163− return (TI x1 x2 x3 x4)

2164+ x5 <- get

2165+ return (TI x1 x2 x3 x4 x5)

21642166

21652167instance Binary SynContext where

21662168 put x