88aa6d1 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Support mixed induction/coinduction with Inf type

88aa6d1Edwin Brady13 years ago

CHANGELOG+1

compare with master

unifiedsplit

@@ -22,6 +22,7 @@ New in 0.9.12:

22* Updated 'effects' library

23* New :apropos command at REPL to search documentation, names, and types

24* Unification errors are now slightly more informative

25+* Support mixed induction/coinduction with 'Inf' type

26New in 0.9.11:

27New in 0.9.11:

27--------------

28--------------

libs/prelude/Prelude/Bool.idr+1−1

@@ -16,7 +16,7 @@ boolElim False t e = e

16||| Defines a predicate on Bool which guarantees that the value is true.

17data so : Bool -> Type where oh : so True

19−-- Syntaxtic sugar for boolean elimination.

19+-- Syntactic sugar for boolean elimination.

20syntax if [test] then [t] else [e] = boolElim test (Delay t) (Delay e)

22-- Boolean Operator Precedence

src/Idris/Core/Unify.hs+14−8

@@ -96,7 +96,8 @@ match_unify ctxt env topx topy inj holes from =

96 un names x y

97 | OK True <- convEq' ctxt holes x y = do sc 1; return []

98 | otherwise = do UI s f <- get

99− let r = recoverable x y

99+ let r = recoverable (normalise ctxt env x)

100+ (normalise ctxt env y)

100 let err = cantUnify from r

101 let err = cantUnify from r

101 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

102 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

102 if (not r) then lift $ tfail err

103 if (not r) then lift $ tfail err

@@ -110,7 +111,8 @@ match_unify ctxt env topx topy inj holes from =

110 uB bnames (Lam tx) (Lam ty) = un bnames tx ty

111 uB bnames (Lam tx) (Lam ty) = un bnames tx ty

111 uB bnames (Pi tx) (Pi ty) = un bnames tx ty

112 uB bnames (Pi tx) (Pi ty) = un bnames tx ty

112 uB bnames x y = do UI s f <- get

113 uB bnames x y = do UI s f <- get

113− let r = recoverable (binderTy x) (binderTy y)

114+ let r = recoverable (normalise ctxt env (binderTy x))

115+ (normalise ctxt env (binderTy y))

114 let err = cantUnify from r topx topy

116 let err = cantUnify from r topx topy

115 (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)

117 (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)

116 (errEnv env) s

118 (errEnv env) s

@@ -124,7 +126,8 @@ match_unify ctxt env topx topy inj holes from =

124 put (UI (s+i) f)

126 put (UI (s+i) f)

125

127

126 unifyFail x y = do UI s f <- get

128 unifyFail x y = do UI s f <- get

127− let r = recoverable x y

129+ let r = recoverable (normalise ctxt env x)

130+ (normalise ctxt env y)

128 let err = cantUnify from r

131 let err = cantUnify from r

129 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

132 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

130 put (UI s ((x, y, env, err, from, Match) : f))

133 put (UI s ((x, y, env, err, from, Match) : f))

@@ -377,7 +380,8 @@ unify ctxt env topx topy inj holes from =

377 un' fn bnames x y

380 un' fn bnames x y

378 | OK True <- convEq' ctxt holes x y = do sc 1; return []

381 | OK True <- convEq' ctxt holes x y = do sc 1; return []

379 | otherwise = do UI s f <- get

382 | otherwise = do UI s f <- get

380− let r = recoverable x y

383+ let r = recoverable (normalise ctxt env x)

384+ (normalise ctxt env y)

381 let err = cantUnify from r

385 let err = cantUnify from r

382 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

386 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

383 if (not r) then lift $ tfail err

387 if (not r) then lift $ tfail err

@@ -477,7 +481,7 @@ unify ctxt env topx topy inj holes from =

477 unifyTmpFail :: Term -> Term -> StateT UInfo TC [(Name, TT Name)]

481 unifyTmpFail :: Term -> Term -> StateT UInfo TC [(Name, TT Name)]

478 unifyTmpFail x y

482 unifyTmpFail x y

479 = do UI s f <- get

483 = do UI s f <- get

480− let r = recoverable x y

484+ let r = recoverable (normalise ctxt env x) (normalise ctxt env y)

481 let err = cantUnify from r

485 let err = cantUnify from r

482 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

486 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

483 put (UI s ((topx, topy, env, err, from, Unify) : f))

487 put (UI s ((topx, topy, env, err, from, Unify) : f))

@@ -485,7 +489,7 @@ unify ctxt env topx topy inj holes from =

485

489

486 -- shortcut failure, if we *know* nothing can fix it

490 -- shortcut failure, if we *know* nothing can fix it

487 unifyFail x y = do UI s f <- get

491 unifyFail x y = do UI s f <- get

488− let r = recoverable x y

492+ let r = recoverable (normalise ctxt env x) (normalise ctxt env y)

489 let err = cantUnify from r

493 let err = cantUnify from r

490 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

494 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

491 put (UI s ((topx, topy, env, err, from, Unify) : f))

495 put (UI s ((topx, topy, env, err, from, Unify) : f))

@@ -507,7 +511,8 @@ unify ctxt env topx topy inj holes from =

507 uB bnames (Hole tx) (Hole ty) = un' False bnames tx ty

511 uB bnames (Hole tx) (Hole ty) = un' False bnames tx ty

508 uB bnames (PVar tx) (PVar ty) = un' False bnames tx ty

512 uB bnames (PVar tx) (PVar ty) = un' False bnames tx ty

509 uB bnames x y = do UI s f <- get

513 uB bnames x y = do UI s f <- get

510− let r = recoverable (binderTy x) (binderTy y)

514+ let r = recoverable (normalise ctxt env (binderTy x))

515+ (normalise ctxt env (binderTy y))

511 let err = cantUnify from r topx topy

516 let err = cantUnify from r topx topy

512 (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)

517 (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)

513 (errEnv env) s

518 (errEnv env) s

@@ -577,6 +582,7 @@ envPos x i ((y, _) : ys) | x == y = i

577-- more work may help.

582-- more work may help.

578-- FIXME: Depending on how overloading gets used, this may cause problems. Better

583-- FIXME: Depending on how overloading gets used, this may cause problems. Better

579-- rethink overloading properly...

584-- rethink overloading properly...

585+-- ASSUMPTION: inputs are in normal form

580

586

581recoverable t@(App _ _) _

587recoverable t@(App _ _) _

582 | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy" = False

588 | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy" = False

@@ -597,7 +603,7 @@ recoverable (P (TCon _ _) x _) (P (DCon _ _) y _) = False

597recoverable p@(Constant _) (App f a) = recoverable p f

603recoverable p@(Constant _) (App f a) = recoverable p f

598recoverable (App f a) p@(Constant _) = recoverable f p

604recoverable (App f a) p@(Constant _) = recoverable f p

599recoverable p@(P _ n _) (App f a) = recoverable p f

605recoverable p@(P _ n _) (App f a) = recoverable p f

600−-- recoverable (App f a) p@(P _ _ _) = recoverable f p

606+recoverable (App f a) p@(P _ _ _) = recoverable f p

601recoverable (App f a) (App f' a')

607recoverable (App f a) (App f' a')

602 = recoverable f f' -- && recoverable a a'

608 = recoverable f f' -- && recoverable a a'

603recoverable f (Bind _ (Pi _) sc)

609recoverable f (Bind _ (Pi _) sc)

src/Idris/Coverage.hs+34−25

@@ -256,7 +256,7 @@ calcProd i fc topn pats

256

257 prodRec :: Name -> [Name] -> ([Name], Term, Term) -> Idris Bool

258 prodRec n done _ | n `elem` done = return True

259− prodRec n done (_, _, tm) = prod n done False (delazy tm)

259+ prodRec n done (_, _, tm) = prod n done False (delazy' True tm)

260

261 prod :: Name -> [Name] -> Bool -> Term -> Idris Bool

262 prod n done ok ap@(App _ _)

@@ -292,9 +292,12 @@ calcProd i fc topn pats

292 _ -> False

293 cotype nt n ty = False

294

295+-- Calculate the totality of a function from its patterns.

296+-- Either follow the size change graph (if inductive) or check for

297+-- productivity (if coinductive)

298+

295−calcTotality :: [Name] -> FC -> Name -> [([Name], Term, Term)]

299+calcTotality :: FC -> Name -> [([Name], Term, Term)] -> Idris Totality

296− -> Idris Totality

297−calcTotality path fc n pats

300+calcTotality fc n pats

298 = do i <- getIState

301 = do i <- getIState

299 let opts = case lookupCtxt n (idris_flags i) of

302 let opts = case lookupCtxt n (idris_flags i) of

300 [fs] -> fs

303 [fs] -> fs

@@ -329,7 +332,7 @@ checkTotality path fc n

329 [CaseOp _ _ _ _ pats _] ->

332 [CaseOp _ _ _ _ pats _] ->

330 do t' <- if AssertTotal `elem` opts

333 do t' <- if AssertTotal `elem` opts

331 then return $ Total []

334 then return $ Total []

332− else calcTotality path fc n pats

335+ else calcTotality fc n pats

333 setTotality n t'

336 setTotality n t'

334 addIBC (IBCTotal n t')

337 addIBC (IBCTotal n t')

335 return t'

338 return t'

@@ -401,41 +404,47 @@ buildSCG (_, n) = do

401 [] -> logLvl 5 $ "Could not build SCG for " ++ show n ++ "\n"

404 [] -> logLvl 5 $ "Could not build SCG for " ++ show n ++ "\n"

402 x -> error $ "buildSCG: " ++ show (n, x)

405 x -> error $ "buildSCG: " ++ show (n, x)

403

406

407+delazy = delazy' False -- not lazy codata

404−delazy t@(App f a)

408+delazy' all t@(App f a)

405− | (P _ (UN l) _, [_, _, arg]) <- unApply t,

406− l == txt "Force" = delazy arg

407 | (P _ (UN l) _, [_, _, arg]) <- unApply t,

409 | (P _ (UN l) _, [_, _, arg]) <- unApply t,

410+ l == txt "Force" = delazy' all arg

411+ | (P _ (UN l) _, [P _ (UN lty) _, _, arg]) <- unApply t,

408− l == txt "Delay" = delazy arg

412+ l == txt "Delay" && (all || lty == txt "LazyEval") = delazy arg

409 | (P _ (UN l) _, [_, arg]) <- unApply t,

413 | (P _ (UN l) _, [_, arg]) <- unApply t,

410− l == txt "Lazy'" = delazy arg

414+ l == txt "Lazy'" = delazy' all arg

411−delazy (App f a) = App (delazy f) (delazy a)

415+delazy' all (App f a) = App (delazy' all f) (delazy' all a)

412−delazy (Bind n b sc) = Bind n (fmap delazy b) (delazy sc)

416+delazy' all (Bind n b sc) = Bind n (fmap (delazy' all) b) (delazy' all sc)

413−delazy t = t

417+delazy' all t = t

414

418

415buildSCG' :: IState -> [(Term, Term)] -> [Name] -> [SCGEntry]

419buildSCG' :: IState -> [(Term, Term)] -> [Name] -> [SCGEntry]

416buildSCG' ist pats args = nub $ concatMap scgPat pats where

420buildSCG' ist pats args = nub $ concatMap scgPat pats where

417 scgPat (lhs, rhs) = let lhs' = delazy lhs

421 scgPat (lhs, rhs) = let lhs' = delazy lhs

418 rhs' = delazy rhs

422 rhs' = delazy rhs

419 (f, pargs) = unApply (dePat lhs') in

423 (f, pargs) = unApply (dePat lhs') in

420− findCalls (dePat rhs') (patvars lhs') pargs

424+ findCalls True (dePat rhs') (patvars lhs') pargs

421

425

422− findCalls ap@(App f a) pvs pargs

426+ findCalls guarded ap@(App f a) pvs pargs

423 -- under a call to "assert_total", don't do any checking, just believe

427 -- under a call to "assert_total", don't do any checking, just believe

424 -- that it is total.

428 -- that it is total.

425 | (P _ (UN at) _, [_, _]) <- unApply ap,

429 | (P _ (UN at) _, [_, _]) <- unApply ap,

426 at == txt "assert_total" = []

430 at == txt "assert_total" = []

431+ -- under a call to "Delay LazyCodata", don't do any checking as long

432+ -- as the call is guarded

433+ | (P _ (UN del) _, [_,_,_]) <- unApply ap,

434+ guarded && del == txt "Delay" = []

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

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

436+ = let nguarded = isConName n (tt_ctxt ist) in

428− = mkChange n args pargs ++

437+ mkChange n args pargs ++

429− concatMap (\x -> findCalls x pvs pargs) args

438+ concatMap (\x -> findCalls nguarded x pvs pargs) args

430− findCalls (App f a) pvs pargs

439+ findCalls guarded (App f a) pvs pargs

431− = findCalls f pvs pargs ++ findCalls a pvs pargs

440+ = findCalls False f pvs pargs ++ findCalls False a pvs pargs

432− findCalls (Bind n (Let t v) e) pvs pargs

441+ findCalls guarded (Bind n (Let t v) e) pvs pargs

433− = findCalls v pvs pargs ++ findCalls e (n : pvs) pargs

442+ = findCalls False v pvs pargs ++ findCalls guarded e (n : pvs) pargs

434− findCalls (Bind n _ e) pvs pargs

443+ findCalls guarded (Bind n _ e) pvs pargs

435− = findCalls e (n : pvs) pargs

444+ = findCalls guarded e (n : pvs) pargs

436− findCalls (P _ f _ ) pvs pargs

445+ findCalls guarded (P _ f _ ) pvs pargs

437 | not (f `elem` pvs) = [(f, [])]

446 | not (f `elem` pvs) = [(f, [])]

438− findCalls _ _ _ = []

447+ findCalls _ _ _ _ = []

439

448

440 expandToArity n args

449 expandToArity n args

441 = case lookupTy n (tt_ctxt ist) of

450 = case lookupTy n (tt_ctxt ist) of

src/Idris/ElabDecls.hs+4−2

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

116 [TI _ True _ _] -> True

117 _ -> False

118 _ -> False

119+ -- Productivity checking now via checking for guarded 'Delay'

119 let opts' = if corec then (Coinductive : opts) else opts

120 let opts' = if corec then (Coinductive : opts) else opts

120 let usety = if norm then nty' else nty

121 let usety = if norm then nty' else nty

121 ds <- checkDef fc [(n, (-1, Nothing, usety))]

122 ds <- checkDef fc [(n, (-1, Nothing, usety))]

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

127 addDocStr n doc argDocs

128 addDocStr n doc argDocs

128 addIBC (IBCDoc n)

129 addIBC (IBCDoc n)

129 addIBC (IBCFlags n opts')

130 addIBC (IBCFlags n opts')

130− when (Implicit `elem` opts) $ do addCoercion n

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

131− addIBC (IBCCoercion n)

132+ addIBC (IBCCoercion n)

132 -- If the function is declared as an error handler and the language

133 -- If the function is declared as an error handler and the language

133 -- extension is enabled, then add it to the list of error handlers.

134 -- extension is enabled, then add it to the list of error handlers.

134 errorReflection <- fmap (elem ErrorReflection . idris_language_extensions) getIState

135 errorReflection <- fmap (elem ErrorReflection . idris_language_extensions) getIState

@@ -882,6 +883,7 @@ elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)

882 mkLazy t = t

883 mkLazy t = t

883

884

884 getTyName (PApp _ (PRef _ n) _) = n == nsroot tn

885 getTyName (PApp _ (PRef _ n) _) = n == nsroot tn

886+ getTyName (PRef _ n) = n == nsroot tn

885 getTyName _ = False

887 getTyName _ = False

886

888

887

889

test/error003/expected+1−1

@@ -1,2 +1,2 @@

1ErrorReflection.idr:67:5:When elaborating right hand side of bad:

2−DSL type error: (t'(504) => t'(504)) doesn't match ()

2+DSL type error: (t(503) => t'(504)) doesn't match ()

test/reg007/expected+1−1

@@ -1,5 +1,5 @@

1reg007.lidr:8:1:A.n is already defined

2−reg007.lidr:12:9:When elaborating right hand side of hurrah:

2+reg007.lidr:12:11:When elaborating right hand side of hurrah:

3Can't unify

4 n = lala

5with