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

git.iko.soy/Idris-dev

Support mixed induction/coinduction with Inf type

Update totality checker so that it checks for 'Delay LazyCodata' being guarded by constructors/lambdas only, allowing mixed inductive/coinductive definitions.

commit88aa6d13ea6635d278f1381c57ea6cca99c6b368 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 22 Mar 2014, 17:46 (13 years ago) parent85852c2

7 files changed+56−38

compare with master

unifiedsplit

CHANGELOG+1 libs/prelude/Prelude/Bool.idr+1−1 src/Idris/Core/Unify.hs+14−8 src/Idris/Coverage.hs+34−25 src/Idris/ElabDecls.hs+4−2 test/error003/expected+1−1 test/reg007/expected+1−1

CHANGELOG+1

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

2222* Updated 'effects' library

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

2424* Unification errors are now slightly more informative

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

2526

2627New in 0.9.11:

2728--------------

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

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

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

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

1818

19−-- Syntaxtic sugar for boolean elimination.

19+-- Syntactic sugar for boolean elimination.

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

2121

2222-- Boolean Operator Precedence

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

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

9696 un names x y

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

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

100101 let err = cantUnify from r

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

102103 if (not r) then lift $ tfail err

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

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

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

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

114116 let err = cantUnify from r topx topy

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

116118 (errEnv env) s

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

124126 put (UI (s+i) f)

125127

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

128131 let err = cantUnify from r

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

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

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

377380 un' fn bnames x y

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

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

381385 let err = cantUnify from r

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

383387 if (not r) then lift $ tfail err

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

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

478482 unifyTmpFail x y

479483 = do UI s f <- get

480− let r = recoverable x y

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

481485 let err = cantUnify from r

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

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

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

485489

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

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

489493 let err = cantUnify from r

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

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

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

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

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

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

511516 let err = cantUnify from r topx topy

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

513518 (errEnv env) s

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

577582-- more work may help.

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

579584-- rethink overloading properly...

585+-- ASSUMPTION: inputs are in normal form

580586

581587recoverable t@(App _ _) _

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

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

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

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

599605recoverable 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

601607recoverable (App f a) (App f' a')

602608 = recoverable f f' -- && recoverable a a'

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

src/Idris/Coverage.hs+34−25

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

256256

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

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

260260

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

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

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

292292 _ -> False

293293 cotype nt n ty = False

294294

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

296− -> Idris Totality

297−calcTotality path fc n pats

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+

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

300+calcTotality fc n pats

298301 = do i <- getIState

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

300303 [fs] -> fs

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

329332 [CaseOp _ _ _ _ pats _] ->

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

331334 then return $ Total []

332− else calcTotality path fc n pats

335+ else calcTotality fc n pats

333336 setTotality n t'

334337 addIBC (IBCTotal n t')

335338 return t'

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

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

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

403406

404−delazy t@(App f a)

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

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

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

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

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

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

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

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

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

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

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

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

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

413−delazy t = t

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

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

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

417+delazy' all t = t

414418

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

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

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

418422 rhs' = delazy rhs

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

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

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

421425

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

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

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

424428 -- that it is total.

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

426430 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" = []

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

428− = mkChange n args pargs ++

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

430− findCalls (App f a) pvs pargs

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

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

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

434− findCalls (Bind n _ e) pvs pargs

435− = findCalls e (n : pvs) pargs

436− findCalls (P _ f _ ) pvs pargs

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

437+ mkChange n args pargs ++

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

439+ findCalls guarded (App f a) pvs pargs

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

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

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

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

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

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

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

438− findCalls _ _ _ = []

447+ findCalls _ _ _ _ = []

439448

440449 expandToArity n args

441450 = 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

116116 [TI _ True _ _] -> True

117117 _ -> False

118118 _ -> False

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

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

120121 let usety = if norm then nty' else nty

121122 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

127128 addDocStr n doc argDocs

128129 addIBC (IBCDoc n)

129130 addIBC (IBCFlags n opts')

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

131− addIBC (IBCCoercion n)

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

132+ addIBC (IBCCoercion n)

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

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

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

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

882883 mkLazy t = t

883884

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

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

885887 getTyName _ = False

886888

887889

test/error003/expected+1−1

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

11ErrorReflection.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 @@

11reg007.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:

33Can't unify

44 n = lala

55with