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

git.iko.soy/Idris-dev

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

commit7fb7decd40d0227590b79bdfb8c91c764a57414d authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 31 Jan 2012, 19:07 (15 years ago) parent486b176

7 files changed+156−22

compare with master

unifiedsplit

src/Core/Evaluate.hs+14−9 src/Idris/AbsSyntax.hs+12−1 src/Idris/Coverage.hs+108 src/Idris/ElabDecls.hs+12−11 src/Idris/IBC.hs+6 src/Idris/Parser.hs+3 test/test010/expected+1−1

src/Core/Evaluate.hs+14−9

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

524524

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

526526 | Partial PReason

527+ | Unchecked

527528 deriving Eq

528529

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

531+ | Mutual [Name]

530532 deriving (Show, Eq)

531533

532534instance Show Totality where

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

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

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

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

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

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

538543

539544{-!

540545deriving instance Binary Accessibility

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

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

563568addToCtxt n tm ty uctxt

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

566571 uctxt { definitions = ctxt' }

567572

568573setAccess :: Name -> Accessibility -> Context -> Context

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

579584

580585addCtxtDef :: Name -> Def -> Context -> Context

581586addCtxtDef 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

583588 c { definitions = ctxt' }

584589

585590addTyDecl :: Name -> Type -> Context -> Context

586591addTyDecl n ty uctxt

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

589594 uctxt { definitions = ctxt' }

590595

591596addDatatype :: Datatype Name -> Context -> Context

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

593598 = let ctxt = definitions uctxt

594599 ty' = normalise uctxt [] ty

595600 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

597602 uctxt { definitions = ctxt' }

598603 where

599604 addCons tag [] ctxt = ctxt

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

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

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

604609

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

606611 Type -> Context -> Context

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

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

613618 let inl = alwaysInline in

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

615− Public, Total []) ctxt in

620+ Public, Unchecked) ctxt in

616621 uctxt { definitions = ctxt' }

617622 where simpl [] = []

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

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

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

621626addOperator n ty a op uctxt

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

624629 uctxt { definitions = ctxt' }

625630

626631tfst (a, _, _) = a

src/Idris/AbsSyntax.hs+12−1

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

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

4747 idris_flags :: Ctxt [FnOpt],

4848 idris_callgraph :: Ctxt [Name],

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

4950 idris_log :: String,

5051 idris_options :: IOption,

5152 idris_name :: Int,

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

9293idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

9394 emptyContext emptyContext emptyContext emptyContext

9495 emptyContext emptyContext

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

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

9697 Nothing Nothing Nothing [] [] [] Hidden [] Nothing

9798

9899-- 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 })

117118addHdr :: String -> Idris ()

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

119120

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

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

123+

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

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

122126

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

132136 let ctxt = setTotal n a (tt_ctxt i)

133137 put (i { tt_ctxt = ctxt })

134138

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+

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

136147addToCG n ns = do i <- get

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

src/Idris/Coverage.hs+108

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

99import Idris.AbsSyntax

1010import Idris.Delaborate

11+import Idris.Error

1112

1213import Data.List

14+import Data.Either

1315import Debug.Trace

1416

1517-- 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

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

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

153155

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

157+-- and update the context accordingly

158+

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

155160checkPositive n (cn, ty)

156161 = do let p = cp ty

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

170175 = n /= n' && posArg sc

171176 posArg t = True

172177

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

234234 pdef' <- applyOpts pdef

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

236236 ist <- get

237− let wf = wellFounded ist n sc

237+-- let wf = wellFounded ist n sc

238238 let tot = if pcover

239− then wf

240− else Partial NotCovering

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

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

243− then case tot of

244− Total _ -> return ()

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

246− else return ()

247− _ -> return ()

239+ then Unchecked -- finish checking later

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

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

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

243+-- then case tot of

244+-- Total _ -> return ()

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

246+-- else return ()

247+-- _ -> return ()

248248 case tree of

249249 CaseDef _ _ [] -> return ()

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

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

263263 tcase pcover pdef pdef' ty)

264264 addIBC (IBCDef n)

265265 setTotality n tot

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

266267 i <- get

267268 case lookupDef Nothing n (tt_ctxt i) of

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

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

271272 addToCG n ns

272273 addIBC (IBCCG n)

273274 _ -> return ()

274− addIBC (IBCTotal n tot)

275+-- addIBC (IBCTotal n tot)

275276 [] -> return ()

276277 where

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

src/Idris/IBC.hs+6

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

609609 Itself -> putWord8 1

610610 NotCovering -> putWord8 2

611611 NotPositive -> putWord8 3

612+ Mutual x1 -> do putWord8 4

613+ put x1

612614 get

613615 = do i <- getWord8

614616 case i of

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

617619 1 -> return Itself

618620 2 -> return NotCovering

619621 3 -> return NotPositive

622+ 4 -> do x1 <- get

623+ return (Mutual x1)

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

621625

622626instance Binary Totality where

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

626630 put x1

627631 Partial x1 -> do putWord8 1

628632 put x1

633+ Unchecked -> do putWord8 2

629634 get

630635 = do i <- getWord8

631636 case i of

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

633638 return (Total x1)

634639 1 -> do x1 <- get

635640 return (Partial x1)

641+ 2 -> return Unchecked

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

637643

638644instance Binary IBCFile where

src/Idris/Parser.hs+3

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

88import Idris.Error

99import Idris.ElabDecls

1010import Idris.ElabTerm

11+import Idris.Coverage

1112import Idris.IBC

1213import Idris.Unlit

1314import Paths_idris

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

100101 v <- verbose

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

102103 mapM_ (elabDecl toplevel) ds

104+ i <- get

105+ mapM_ checkDeclTotality (idris_totcheck i)

103106 iLOG ("Finished " ++ f)

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

105108 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