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

git.iko.soy/Idris-dev

on master help sign in

Improved termination check (gets ackermann now, but still no mutual recursive definitions)

7fb7decEdwin Brady15 years ago

src/Core/Evaluate.hs+14−9

compare with master

unifiedsplit

@@ -524,17 +524,22 @@ data Accessibility = Public | Frozen | Hidden

524

525data Totality = Total [Int] -- well-founded arguments

526 | Partial PReason

527+ | Unchecked

527 deriving Eq

528 deriving Eq

528

529

529data PReason = Other [Name] | Itself | NotCovering | NotPositive | UseUndef Name

530data PReason = Other [Name] | Itself | NotCovering | NotPositive | UseUndef Name

531+ | Mutual [Name]

530 deriving (Show, Eq)

532 deriving (Show, Eq)

531

533

532instance Show Totality where

534instance Show Totality where

533 show (Total args)= "Total, " ++ show args ++ " decreasing arguments"

535 show (Total args)= "Total, " ++ show args ++ " decreasing arguments"

536+ show Unchecked = "not yet checked for totality"

534− show (Partial Itself) = "not total as it is not well founded"

537+ show (Partial Itself) = "possibly not total as it is not well founded"

535 show (Partial NotCovering) = "not total as there are missing cases"

538 show (Partial NotCovering) = "not total as there are missing cases"

536 show (Partial NotPositive) = "not strictly positive"

539 show (Partial NotPositive) = "not strictly positive"

537− show (Partial (Other ns)) = "not total due to: " ++ showSep ", " (map show ns)

540+ show (Partial (Other ns)) = "possibly not total due to: " ++ showSep ", " (map show ns)

541+ show (Partial (Mutual ns)) = "possibly not total due to mutual recursive path " ++

542+ showSep " --> " (map show ns)

538

543

539{-!

544{-!

540deriving instance Binary Accessibility

545deriving instance Binary Accessibility

@@ -562,7 +567,7 @@ veval ctxt env t = evalState (eval ctxt emptyContext env t []) ()

562addToCtxt :: Name -> Term -> Type -> Context -> Context

567addToCtxt :: Name -> Term -> Type -> Context -> Context

563addToCtxt n tm ty uctxt

568addToCtxt n tm ty uctxt

564 = let ctxt = definitions uctxt

569 = let ctxt = definitions uctxt

565− ctxt' = addDef n (Function ty tm, Public, Total []) ctxt in

570+ ctxt' = addDef n (Function ty tm, Public, Unchecked) ctxt in

566 uctxt { definitions = ctxt' }

571 uctxt { definitions = ctxt' }

567

572

568setAccess :: Name -> Accessibility -> Context -> Context

573setAccess :: Name -> Accessibility -> Context -> Context

@@ -579,13 +584,13 @@ setTotal n t uctxt

579

584

580addCtxtDef :: Name -> Def -> Context -> Context

585addCtxtDef :: Name -> Def -> Context -> Context

581addCtxtDef n d c = let ctxt = definitions c

586addCtxtDef n d c = let ctxt = definitions c

582− ctxt' = addDef n (d, Public, Total []) ctxt in

587+ ctxt' = addDef n (d, Public, Unchecked) ctxt in

583 c { definitions = ctxt' }

588 c { definitions = ctxt' }

584

589

585addTyDecl :: Name -> Type -> Context -> Context

590addTyDecl :: Name -> Type -> Context -> Context

586addTyDecl n ty uctxt

591addTyDecl n ty uctxt

587 = let ctxt = definitions uctxt

592 = let ctxt = definitions uctxt

588− ctxt' = addDef n (TyDecl Ref ty, Public, Total []) ctxt in

593+ ctxt' = addDef n (TyDecl Ref ty, Public, Unchecked) ctxt in

589 uctxt { definitions = ctxt' }

594 uctxt { definitions = ctxt' }

590

595

591addDatatype :: Datatype Name -> Context -> Context

596addDatatype :: Datatype Name -> Context -> Context

@@ -593,14 +598,14 @@ addDatatype (Data n tag ty cons) uctxt

593 = let ctxt = definitions uctxt

598 = let ctxt = definitions uctxt

594 ty' = normalise uctxt [] ty

599 ty' = normalise uctxt [] ty

595 ctxt' = addCons 0 cons (addDef n

600 ctxt' = addCons 0 cons (addDef n

596− (TyDecl (TCon tag (arity ty')) ty, Public, Total []) ctxt) in

601+ (TyDecl (TCon tag (arity ty')) ty, Public, Unchecked) ctxt) in

597 uctxt { definitions = ctxt' }

602 uctxt { definitions = ctxt' }

598 where

603 where

599 addCons tag [] ctxt = ctxt

604 addCons tag [] ctxt = ctxt

600 addCons tag ((n, ty) : cons) ctxt

605 addCons tag ((n, ty) : cons) ctxt

601 = let ty' = normalise uctxt [] ty in

606 = let ty' = normalise uctxt [] ty in

602 addCons (tag+1) cons (addDef n

607 addCons (tag+1) cons (addDef n

603− (TyDecl (DCon tag (arity ty')) ty, Public, Total []) ctxt)

608+ (TyDecl (DCon tag (arity ty')) ty, Public, Unchecked) ctxt)

604

609

605addCasedef :: Name -> Bool -> Bool -> Bool -> [(Term, Term)] -> [(Term, Term)] ->

610addCasedef :: Name -> Bool -> Bool -> Bool -> [(Term, Term)] -> [(Term, Term)] ->

606 Type -> Context -> Context

611 Type -> Context -> Context

@@ -612,7 +617,7 @@ addCasedef n alwaysInline tcase covering ps psrt ty uctxt

612 (CaseDef args sc _, CaseDef args' sc' _) ->

617 (CaseDef args sc _, CaseDef args' sc' _) ->

613 let inl = alwaysInline in

618 let inl = alwaysInline in

614 addDef n (CaseOp inl ty ps args sc args' sc',

619 addDef n (CaseOp inl ty ps args sc args' sc',

615− Public, Total []) ctxt in

620+ Public, Unchecked) ctxt in

616 uctxt { definitions = ctxt' }

621 uctxt { definitions = ctxt' }

617 where simpl [] = []

622 where simpl [] = []

618 simpl ((l,r) : xs) = (l, simplify uctxt [] r) : simpl xs

623 simpl ((l,r) : xs) = (l, simplify uctxt [] r) : simpl xs

@@ -620,7 +625,7 @@ addCasedef n alwaysInline tcase covering ps psrt ty uctxt

620addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) -> Context -> Context

625addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) -> Context -> Context

621addOperator n ty a op uctxt

626addOperator n ty a op uctxt

622 = let ctxt = definitions uctxt

627 = let ctxt = definitions uctxt

623− ctxt' = addDef n (Operator ty a op, Public, Total []) ctxt in

628+ ctxt' = addDef n (Operator ty a op, Public, Unchecked) ctxt in

624 uctxt { definitions = ctxt' }

629 uctxt { definitions = ctxt' }

625

630

626tfst (a, _, _) = a

631tfst (a, _, _) = a

src/Idris/AbsSyntax.hs+12−1

@@ -46,6 +46,7 @@ data IState = IState { tt_ctxt :: Context,

46 idris_patdefs :: Ctxt [(Term, Term)], -- not exported

47 idris_flags :: Ctxt [FnOpt],

48 idris_callgraph :: Ctxt [Name],

49+ idris_totcheck :: [(FC, Name)],

49 idris_log :: String,

50 idris_log :: String,

50 idris_options :: IOption,

51 idris_options :: IOption,

51 idris_name :: Int,

52 idris_name :: Int,

@@ -92,7 +93,7 @@ data IBCWrite = IBCFix FixDecl

92idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

93idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

93 emptyContext emptyContext emptyContext emptyContext

94 emptyContext emptyContext emptyContext emptyContext

94 emptyContext emptyContext

95 emptyContext emptyContext

95− "" defaultOpts 6 [] [] [] [] [] [] [] []

96+ [] "" defaultOpts 6 [] [] [] [] [] [] [] []

96 Nothing Nothing Nothing [] [] [] Hidden [] Nothing

97 Nothing Nothing Nothing [] [] [] Hidden [] Nothing

98-- The monad for the main REPL - reading and processing files and updating

99-- The monad for the main REPL - reading and processing files and updating

@@ -117,6 +118,9 @@ addLib f = do i <- get; put (i { idris_libs = f : idris_libs i })

117addHdr :: String -> Idris ()

118addHdr :: String -> Idris ()

118addHdr f = do i <- get; put (i { idris_hdrs = f : idris_hdrs i })

119addHdr f = do i <- get; put (i { idris_hdrs = f : idris_hdrs i })

119

120

121+totcheck :: (FC, Name) -> Idris ()

122+totcheck n = do i <- get; put (i { idris_totcheck = n : idris_totcheck i })

123+

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

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

121setFlags n fs = do i <- get; put (i { idris_flags = addDef n fs (idris_flags i) })

125setFlags n fs = do i <- get; put (i { idris_flags = addDef n fs (idris_flags i) })

122

126

@@ -132,6 +136,13 @@ setTotality n a

132 let ctxt = setTotal n a (tt_ctxt i)

136 let ctxt = setTotal n a (tt_ctxt i)

133 put (i { tt_ctxt = ctxt })

137 put (i { tt_ctxt = ctxt })

134

138

139+getTotality :: Name -> Idris Totality

140+getTotality n

141+ = do i <- get

142+ case lookupTotal n (tt_ctxt i) of

143+ [t] -> return t

144+ _ -> return (Total [])

145+

135addToCG :: Name -> [Name] -> Idris ()

146addToCG :: Name -> [Name] -> Idris ()

136addToCG n ns = do i <- get

147addToCG n ns = do i <- get

137 put (i { idris_callgraph = addDef n ns (idris_callgraph i) })

148 put (i { idris_callgraph = addDef n ns (idris_callgraph i) })

src/Idris/Coverage.hs+108

@@ -8,8 +8,10 @@ import Core.CaseTree

9import Idris.AbsSyntax

10import Idris.Delaborate

11+import Idris.Error

12import Data.List

13import Data.List

14+import Data.Either

13import Debug.Trace

15import Debug.Trace

15-- Given a list of LHSs, generate a extra clauses which cover the remaining

17-- Given a list of LHSs, generate a extra clauses which cover the remaining

@@ -151,6 +153,9 @@ wellFounded i n sc = case wff [] sc of

151 chkArgs i ns (P _ n _ : xs) | n `elem` ns = i : chkArgs (i + 1) ns xs

153 chkArgs i ns (P _ n _ : xs) | n `elem` ns = i : chkArgs (i + 1) ns xs

152 chkArgs i ns (_ : xs) = chkArgs (i+1) ns xs

154 chkArgs i ns (_ : xs) = chkArgs (i+1) ns xs

153

155

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

157+-- and update the context accordingly

158+

154checkPositive :: Name -> (Name, Type) -> Idris ()

159checkPositive :: Name -> (Name, Type) -> Idris ()

155checkPositive n (cn, ty)

160checkPositive n (cn, ty)

156 = do let p = cp ty

161 = do let p = cp ty

@@ -170,3 +175,106 @@ checkPositive n (cn, ty)

170 = n /= n' && posArg sc

175 = n /= n' && posArg sc

171 posArg t = True

176 posArg t = True

172

177

178+-- Totality checking - check for structural recursion (no mutual definitions yet)

179+

180+data LexOrder = LexXX | LexEQ | LexLT

181+ deriving (Show, Eq, Ord)

182+

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

184+calcTotality path fc n pats

185+ = do orders <- mapM ctot pats

186+ let order = sortBy cmpOrd $ concat orders

187+ let (errs, valid) = partitionEithers order

188+ let lex = stripXX valid

189+ case errs of

190+ [] -> do logLvl 3 $ show n ++ ":\n" ++ showSep "\n" (map show lex)

191+ checkDecreasing lex

192+ (e : _) -> return e -- FIXME: should probably combine them

193+ where

194+ cmpOrd (Left _) (Left _) = EQ

195+ cmpOrd (Left _) (Right _) = LT

196+ cmpOrd (Right _) (Left _) = GT

197+ cmpOrd (Right x) (Right y) = compare x y

198+

199+ checkDecreasing [] = return (Total [])

200+ checkDecreasing (c : cs) | dec c = checkDecreasing cs

201+ | otherwise = return (Partial Itself)

202+

203+ dec [] = False

204+ dec (LexLT : _) = True

205+ dec (LexEQ : xs) = dec xs

206+ dec (LexXX : _) = False

207+

208+ stripXX [] = []

209+ stripXX v@(c : cs)

210+ = case span (==LexXX) c of

211+ (ns, rest) -> map (drop (length ns)) v

212+

213+ ctot (lhs, rhs)

214+ | (_, args) <- unApply lhs

215+ = do -- check lhs doesn't use any dodgy names

216+ lhsOK <- mapM (chkOrd [] []) args

217+ chkOrd (concat lhsOK) args rhs

218+

219+ chkOrd ords args (Bind n (Let t v) sc)

220+ = do ov <- chkOrd ords args v

221+ chkOrd ov args sc

222+ chkOrd ords args (Bind n b sc) = chkOrd ords args sc

223+ chkOrd ords args ap@(App f a)

224+ | (P _ fn _, args') <- unApply ap

225+ = if fn == n && length args == length args'

226+ then do orf <- chkOrd (Right (zipWith lexOrd args args') : ords) args f

227+ chkOrd orf args a

228+ else do orf <- chkOrd ords args f

229+ chkOrd orf args a

230+ | otherwise = do orf <- chkOrd ords args f

231+ chkOrd orf args a

232+ chkOrd ords args (P _ fn _)

233+ | n /= fn

234+ = do tf <- checkTotality (n : path) fc fn

235+ case tf of

236+ Total _ -> return ords

237+ p@(Partial (Mutual x)) -> return ((Left p) : ords)

238+ _ -> return (Left (Partial (Other [fn])) : ords)

239+ chkOrd ords args _ = return ords

240+

241+ lexOrd x y | x == y = LexEQ

242+ lexOrd f@(App _ _) x

243+ | (f', args) <- unApply f

244+ = let ords = map (\x' -> lexOrd x' x) args in

245+ if any (\o -> o == LexEQ || o == LexLT) ords

246+ then LexLT

247+ else LexXX

248+ lexOrd _ _ = LexXX

249+

250+checkTotality :: [Name] -> FC -> Name -> Idris Totality

251+checkTotality path fc n

252+ | n `elem` path = return (Partial (Mutual (n : path)))

253+ | otherwise

254+ = do t <- getTotality n

255+ ctxt <- getContext

256+ case t of

257+ Unchecked -> case lookupDef Nothing n ctxt of

258+ [CaseOp _ _ pats _ _ _ _] ->

259+ do t' <- calcTotality path fc n pats

260+ i <- getIState

261+ case lookupCtxt Nothing n (idris_flags i) of

262+ [fs] -> if TotalFn `elem` fs then

263+ case t' of

264+ Total _ -> return ()

265+ e -> totalityError t'

266+ else return ()

267+ _ -> return ()

268+ setTotality n t'

269+ addIBC (IBCTotal n t')

270+ return t'

271+ _ -> return $ Total []

272+ x -> return x

273+ where

274+ totalityError t = tclift $ tfail (At fc (Msg (show n ++ " is " ++ show t)))

275+

276+checkDeclTotality :: (FC, Name) -> Idris Totality

277+checkDeclTotality (fc, n)

278+ = do logLvl 2 $ "Checking " ++ show n ++ " for totality"

279+ checkTotality [] fc n

280+

src/Idris/ElabDecls.hs+12−11

@@ -234,17 +234,17 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

234 pdef' <- applyOpts pdef

235 let tree@(CaseDef _ sc _) = simpleCase tcase pcover pdef

236 ist <- get

237− let wf = wellFounded ist n sc

237+-- let wf = wellFounded ist n sc

238 let tot = if pcover

239− then wf

239+ then Unchecked -- finish checking later

240− else Partial NotCovering

240+ else Partial NotCovering -- already know it's not total

241− case lookupCtxt (namespace info) n (idris_flags ist) of

241+-- case lookupCtxt (namespace info) n (idris_flags ist) of

242− [fs] -> if TotalFn `elem` fs

242+-- [fs] -> if TotalFn `elem` fs

243− then case tot of

243+-- then case tot of

244− Total _ -> return ()

244+-- Total _ -> return ()

245− t -> tclift $ tfail (At fc (Msg (show n ++ " is " ++ show t)))

245+-- t -> tclift $ tfail (At fc (Msg (show n ++ " is " ++ show t)))

246− else return ()

246+-- else return ()

247− _ -> return ()

247+-- _ -> return ()

248 case tree of

249 CaseDef _ _ [] -> return ()

250 CaseDef _ _ xs -> mapM_ (\x ->

@@ -263,6 +263,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

263 tcase pcover pdef pdef' ty)

264 addIBC (IBCDef n)

265 setTotality n tot

266+ when (tot == Unchecked) $ totcheck (fc, n)

266 i <- get

267 i <- get

267 case lookupDef Nothing n (tt_ctxt i) of

268 case lookupDef Nothing n (tt_ctxt i) of

268 (CaseOp _ _ _ _ sc _ _ : _) ->

269 (CaseOp _ _ _ _ sc _ _ : _) ->

@@ -271,7 +272,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

271 addToCG n ns

272 addToCG n ns

272 addIBC (IBCCG n)

273 addIBC (IBCCG n)

273 _ -> return ()

274 _ -> return ()

274− addIBC (IBCTotal n tot)

275+-- addIBC (IBCTotal n tot)

275 [] -> return ()

276 [] -> return ()

276 where

277 where

277 debind (x, y) = (depat x, depat y)

278 debind (x, y) = (depat x, depat y)

src/Idris/IBC.hs+6

@@ -609,6 +609,8 @@ instance Binary PReason where

609 Itself -> putWord8 1

610 NotCovering -> putWord8 2

611 NotPositive -> putWord8 3

612+ Mutual x1 -> do putWord8 4

613+ put x1

612 get

614 get

613 = do i <- getWord8

615 = do i <- getWord8

614 case i of

616 case i of

@@ -617,6 +619,8 @@ instance Binary PReason where

617 1 -> return Itself

619 1 -> return Itself

618 2 -> return NotCovering

620 2 -> return NotCovering

619 3 -> return NotPositive

621 3 -> return NotPositive

622+ 4 -> do x1 <- get

623+ return (Mutual x1)

620 _ -> error "Corrupted binary data for PReason"

624 _ -> error "Corrupted binary data for PReason"

621

625

622instance Binary Totality where

626instance Binary Totality where

@@ -626,6 +630,7 @@ instance Binary Totality where

626 put x1

630 put x1

627 Partial x1 -> do putWord8 1

631 Partial x1 -> do putWord8 1

628 put x1

632 put x1

633+ Unchecked -> do putWord8 2

629 get

634 get

630 = do i <- getWord8

635 = do i <- getWord8

631 case i of

636 case i of

@@ -633,6 +638,7 @@ instance Binary Totality where

633 return (Total x1)

638 return (Total x1)

634 1 -> do x1 <- get

639 1 -> do x1 <- get

635 return (Partial x1)

640 return (Partial x1)

641+ 2 -> return Unchecked

636 _ -> error "Corrupted binary data for Totality"

642 _ -> error "Corrupted binary data for Totality"

637

643

638instance Binary IBCFile where

644instance Binary IBCFile where

src/Idris/Parser.hs+3

@@ -8,6 +8,7 @@ import Idris.Imports

8import Idris.Error

9import Idris.ElabDecls

10import Idris.ElabTerm

11+import Idris.Coverage

11import Idris.IBC

12import Idris.IBC

12import Idris.Unlit

13import Idris.Unlit

13import Paths_idris

14import Paths_idris

@@ -100,6 +101,8 @@ loadSource lidr f

100 v <- verbose

101 v <- verbose

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

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

102 mapM_ (elabDecl toplevel) ds

103 mapM_ (elabDecl toplevel) ds

104+ i <- get

105+ mapM_ checkDeclTotality (idris_totcheck i)

103 iLOG ("Finished " ++ f)

106 iLOG ("Finished " ++ f)

104 let ibc = dropExtension f ++ ".ibc"

107 let ibc = dropExtension f ++ ".ibc"

105 iucheck

108 iucheck

test/test010/expected+1−1

@@ -1 +1 @@

1−test010.idr:14:foo is not total due to: MkBad

1+test010.idr:14:foo is possibly not total due to: MkBad