ae4be75 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Well founded recursion check

commitae4be752c38c00499cba748c11d2d68212b161e3 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateSat 21 Jan 2012, 20:57 (15 years ago) parentfb3160e

6 files changed+178−28

compare with master

unifiedsplit

src/Core/Evaluate.hs+50−22 src/Idris/AbsSyntax.hs+8−1 src/Idris/Coverage.hs+54 src/Idris/ElabDecls.hs+16−1 src/Idris/IBC.hs+47−4 src/Idris/REPL.hs+3

src/Core/Evaluate.hs+50−22

@@ -3,11 +3,12 @@

44module Core.Evaluate(normalise, normaliseC, normaliseAll,

55 simplify, specialise, hnf,

6− Def(..), Accessibility(..),

6+ Def(..), Accessibility(..), Totality(..), PReason(..),

77 Context, initContext, ctxtAlist, uconstraints, next_tvar,

8− addToCtxt, setAccess, addCtxtDef, addTyDecl, addDatatype,

8+ addToCtxt, setAccess, setTotal, addCtxtDef, addTyDecl, addDatatype,

99 addCasedef, addOperator,

10− lookupTy, lookupP, lookupDef, lookupVal, lookupTyEnv, isConName,

10+ lookupTy, lookupP, lookupDef, lookupVal, lookupTotal,

11+ lookupTyEnv, isConName,

1112 Value(..)) where

1213

1314import Debug.Trace

@@ -470,42 +471,63 @@ instance Binary (a -> b) where

470471

471472data Accessibility = Public | Frozen | Hidden

472473 deriving (Show, Eq)

474+

475+data Totality = Total | Partial PReason

476+ deriving (Show, Eq)

477+

478+data PReason = Other [Name] | Itself | NotCovering | NotPositive

479+ deriving (Show, Eq)

480+

473481{-!

474482deriving instance Binary Accessibility

475483!-}

476484

485+{-!

486+deriving instance Binary Totality

487+!-}

488+

489+{-!

490+deriving instance Binary PReason

491+!-}

492+

477493data Context = MkContext { uconstraints :: [UConstraint],

478494 next_tvar :: Int,

479− definitions :: Ctxt (Def, Accessibility) }

495+ definitions :: Ctxt (Def, Accessibility, Totality) }

480496

481497initContext = MkContext [] 0 emptyContext

482498

483499ctxtAlist :: Context -> [(Name, Def)]

484−ctxtAlist ctxt = map (\(n, (d, a)) -> (n, d)) $ toAlist (definitions ctxt)

500+ctxtAlist ctxt = map (\(n, (d, a, t)) -> (n, d)) $ toAlist (definitions ctxt)

485501

486502veval ctxt env t = evalState (eval ctxt emptyContext env t []) ()

487503

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

489505addToCtxt n tm ty uctxt

490506 = let ctxt = definitions uctxt

491− ctxt' = addDef n (Function ty tm, Public) ctxt in

507+ ctxt' = addDef n (Function ty tm, Public, Total) ctxt in

492508 uctxt { definitions = ctxt' }

493509

494510setAccess :: Name -> Accessibility -> Context -> Context

495511setAccess n a uctxt

496512 = let ctxt = definitions uctxt

497− ctxt' = updateDef n (\ (d, _) -> (d, a)) ctxt in

513+ ctxt' = updateDef n (\ (d, _, t) -> (d, a, t)) ctxt in

514+ uctxt { definitions = ctxt' }

515+

516+setTotal :: Name -> Totality -> Context -> Context

517+setTotal n t uctxt

518+ = let ctxt = definitions uctxt

519+ ctxt' = updateDef n (\ (d, a, _) -> (d, a, t)) ctxt in

498520 uctxt { definitions = ctxt' }

499521

500522addCtxtDef :: Name -> Def -> Context -> Context

501523addCtxtDef n d c = let ctxt = definitions c

502− ctxt' = addDef n (d, Public) ctxt in

524+ ctxt' = addDef n (d, Public, Total) ctxt in

503525 c { definitions = ctxt' }

504526

505527addTyDecl :: Name -> Type -> Context -> Context

506528addTyDecl n ty uctxt

507529 = let ctxt = definitions uctxt

508− ctxt' = addDef n (TyDecl Ref ty, Public) ctxt in

530+ ctxt' = addDef n (TyDecl Ref ty, Public, Total) ctxt in

509531 uctxt { definitions = ctxt' }

510532

511533addDatatype :: Datatype Name -> Context -> Context

@@ -513,14 +535,14 @@ addDatatype (Data n tag ty cons) uctxt

513535 = let ctxt = definitions uctxt

514536 ty' = normalise uctxt [] ty

515537 ctxt' = addCons 0 cons (addDef n

516− (TyDecl (TCon tag (arity ty')) ty, Public) ctxt) in

538+ (TyDecl (TCon tag (arity ty')) ty, Public, Total) ctxt) in

517539 uctxt { definitions = ctxt' }

518540 where

519541 addCons tag [] ctxt = ctxt

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

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

522544 addCons (tag+1) cons (addDef n

523− (TyDecl (DCon tag (arity ty')) ty, Public) ctxt)

545+ (TyDecl (DCon tag (arity ty')) ty, Public, Total) ctxt)

524546

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

526548 Type -> Context -> Context

@@ -532,7 +554,7 @@ addCasedef n alwaysInline tcase covering ps psrt ty uctxt

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

533555 let inl = alwaysInline in

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

535− Public) ctxt in

557+ Public, Total) ctxt in

536558 uctxt { definitions = ctxt' }

537559 where simpl [] = []

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

@@ -540,13 +562,15 @@ addCasedef n alwaysInline tcase covering ps psrt ty uctxt

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

541563addOperator n ty a op uctxt

542564 = let ctxt = definitions uctxt

543− ctxt' = addDef n (Operator ty a op, Public) ctxt in

565+ ctxt' = addDef n (Operator ty a op, Public, Total) ctxt in

544566 uctxt { definitions = ctxt' }

545567

568+tfst (a, _, _) = a

569+

546570lookupTy :: Maybe [String] -> Name -> Context -> [Type]

547571lookupTy root n ctxt

548572 = do def <- lookupCtxt root n (definitions ctxt)

549− case fst def of

573+ case tfst def of

550574 (Function ty _) -> return ty

551575 (TyDecl _ ty) -> return ty

552576 (Operator ty _ _) -> return ty

@@ -555,7 +579,7 @@ lookupTy root n ctxt

555579isConName :: Maybe [String] -> Name -> Context -> Bool

556580isConName root n ctxt

557581 = or $ do def <- lookupCtxt root n (definitions ctxt)

558− case fst def of

582+ case tfst def of

559583 (TyDecl (DCon _ _) _) -> return True

560584 (TyDecl (TCon _ _) _) -> return True

561585 _ -> return False

@@ -564,26 +588,30 @@ lookupP :: Maybe [String] -> Name -> Context -> [Term]

564588lookupP root n ctxt

565589 = do def <- lookupCtxt root n (definitions ctxt)

566590 p <- case def of

567− (Function ty tm, a) -> return (P Ref n ty, a)

568− (TyDecl nt ty, a) -> return (P nt n ty, a)

569− (CaseOp _ ty _ _ _ _ _, a) -> return (P Ref n ty, a)

570− (Operator ty _ _, a) -> return (P Ref n ty, a)

591+ (Function ty tm, a, _) -> return (P Ref n ty, a)

592+ (TyDecl nt ty, a, _) -> return (P nt n ty, a)

593+ (CaseOp _ ty _ _ _ _ _, a, _) -> return (P Ref n ty, a)

594+ (Operator ty _ _, a, _) -> return (P Ref n ty, a)

571595 case snd p of

572596 Hidden -> []

573597 _ -> return (fst p)

574598

575599lookupDef :: Maybe [String] -> Name -> Context -> [Def]

576−lookupDef root n ctxt = map fst $ lookupCtxt root n (definitions ctxt)

600+lookupDef root n ctxt = map tfst $ lookupCtxt root n (definitions ctxt)

577601

578602lookupDefAcc :: Maybe [String] -> Name -> Bool -> Context -> [(Def, Accessibility)]

579603lookupDefAcc root n mkpublic ctxt

580604 = map mkp $ lookupCtxt root n (definitions ctxt)

581− where mkp (d, a) = if mkpublic then (d, Public) else (d, a)

605+ where mkp (d, a, _) = if mkpublic then (d, Public) else (d, a)

606+

607+lookupTotal :: Name -> Context -> [Totality]

608+lookupTotal n ctxt = map mkt $ lookupCtxt Nothing n (definitions ctxt)

609+ where mkt (d, a, t) = t

582610

583611lookupVal :: Maybe [String] -> Name -> Context -> [Value]

584612lookupVal root n ctxt

585613 = do def <- lookupCtxt root n (definitions ctxt)

586− case fst def of

614+ case tfst def of

587615 (Function _ htm) -> return (veval ctxt [] htm)

588616 (TyDecl nt ty) -> return (VP nt n (veval ctxt [] ty))

589617

src/Idris/AbsSyntax.hs+8−1

@@ -81,6 +81,7 @@ data IBCWrite = IBCFix FixDecl

8181 | IBCLib String

8282 | IBCHeader String

8383 | IBCAccess Name Accessibility

84+ | IBCTotal Name Totality

8485 | IBCDef Name -- i.e. main context

8586 deriving Show

8687

@@ -117,6 +118,12 @@ setAccessibility n a

117118 let ctxt = setAccess n a (tt_ctxt i)

118119 put (i { tt_ctxt = ctxt })

119120

121+setTotality :: Name -> Totality -> Idris ()

122+setTotality n a

123+ = do i <- get

124+ let ctxt = setTotal n a (tt_ctxt i)

125+ put (i { tt_ctxt = ctxt })

126+

120127addIBC :: IBCWrite -> Idris ()

121128addIBC ibc@(IBCDef n)

122129 = do i <- get

@@ -349,7 +356,7 @@ impl = Imp False Dynamic

349356expl = Exp False Dynamic

350357constraint = Constraint False Static

351358

352−data FnOpt = Inlinable | Partial | Abstract | Private | TCGen

359+data FnOpt = Inlinable | Abstract | Private | TCGen

353360 deriving (Show, Eq)

354361

355362type FnOpts = [FnOpt]

src/Idris/Coverage.hs+54

@@ -4,6 +4,8 @@ module Idris.Coverage where

55import Core.TT

66import Core.Evaluate

7+import Core.CaseTree

79import Idris.AbsSyntax

810import Idris.Delaborate

911

@@ -95,3 +97,55 @@ genAll i args = concatMap otherPats (nub args)

9597

9698upd p' p = p { getTm = p' }

9799

100+-- recursive calls are well-founded if one of their argument positions is

101+-- always decreasing.

102+

103+-- If we encounter a non-total name, we'll fail

104+

105+wellFounded :: IState -> Name -> SC -> Either [Name] Bool

106+wellFounded i n sc = case wff [] sc of

107+ RightOK smaller_args ->

108+ -- is there a number in every list?

109+ -- trace (show (n, smaller_args)) $

110+ case smaller_args of

111+ [] -> Right True

112+ (x : xs) -> let args = foldl intersect x xs in

113+ Right $ not (null args)

114+ LeftErr x -> Left x

115+ where

116+ wff :: [Name] -> SC -> EitherErr [Name] [[Int]]

117+ wff ns (Case n as) = do is <- mapM (wffC ns) as

118+ return $ concat is

119+ where wffC ns (ConCase _ i ns' sc) = wff (ns ++ ns') sc

120+ wffC ns (ConstCase _ sc) = wff ns sc

121+ wffC ns (DefaultCase sc) = wff ns sc

122+ wff ns (STerm t) = argPos ns t

123+ wff ns _ = return []

124+

125+ checkOK n' = case lookupTotal n' (tt_ctxt i) of

126+ [Partial _] -> LeftErr [n']

127+ [Total] -> RightOK ()

128+ x -> RightOK ()

129+-- checkOK n = RightOK ()

130+

131+ argPos ns ap@(App f' a')

132+ | (P _ f _, args) <- unApply ap

133+ = if f == n then

134+ do aa <- argPos ns a'

135+ return $ chkArgs 0 ns args : aa

136+ else do checkOK f

137+ argPos ns a'

138+ argPos ns (App f a) = do f' <- argPos ns f

139+ a' <- argPos ns a

140+ return (f' ++ a')

141+ argPos ns (Bind n (Let t v) sc) = do v' <- argPos ns v

142+ sc' <- argPos ns sc

143+ return (v' ++ sc')

144+ argPos ns (Bind n _ sc) = argPos ns sc

145+ argPos ns _ = return []

146+

147+ chkArgs i ns [] = []

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

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

150+

151+

src/Idris/ElabDecls.hs+16−1

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

128128 return False)

129129 else return False

130130 pdef' <- applyOpts pdef

131− let tree = simpleCase tcase pcover pdef

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

132+ ist <- get

133+ let wf = wellFounded ist n sc

134+ tot <- if pcover

135+ then case wf of

136+ Left ns -> do logLvl 2 $ show n ++ " not well founded due to "

137+ ++ show ns

138+ return $ Partial (Other ns)

139+ Right False -> do logLvl 2 $ show n ++ " not well founded"

140+ return $ Partial Itself

141+ Right True -> do logLvl 2 $ show n ++ " well founded"

142+ return Total

143+ else do logLvl 2 $ show n ++ " does not cover all cases"

144+ return $ Partial NotCovering

132145 case tree of

133146 CaseDef _ _ [] -> return ()

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

@@ -146,6 +159,8 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

146159 [ty] -> do updateContext (addCasedef n (inlinable opts)

147160 tcase pcover pdef pdef' ty)

148161 addIBC (IBCDef n)

162+ setTotality n tot

163+ addIBC (IBCTotal n tot)

149164 [] -> return ()

150165 where

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

src/Idris/IBC.hs+47−4

@@ -22,7 +22,7 @@ import System.Directory

2222import Paths_idris

2323

2424ibcVersion :: Word8

25−ibcVersion = 10

25+ibcVersion = 14

2626

2727data IBCFile = IBCFile { ver :: Word8,

2828 sourcefile :: FilePath,

@@ -40,13 +40,14 @@ data IBCFile = IBCFile { ver :: Word8,

4040 ibc_libs :: [String],

4141 ibc_hdrs :: [String],

4242 ibc_access :: [(Name, Accessibility)],

43+ ibc_total :: [(Name, Totality)],

4344 ibc_defs :: [(Name, Def)] }

4445{-!

4546deriving instance Binary IBCFile

4647!-}

4748

4849initIBC :: IBCFile

49−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

50+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

5051

5152loadIBC :: FilePath -> Idris ()

5253loadIBC fp = do iLOG $ "Loading ibc " ++ fp

@@ -106,6 +107,7 @@ ibc i (IBCDef n) f = case lookupDef Nothing n (tt_ctxt i) of

106107 [v] -> return f { ibc_defs = (n,v) : ibc_defs f }

107108 _ -> fail "IBC write failed"

108109ibc i (IBCAccess n a) f = return f { ibc_access = (n,a) : ibc_access f }

110+ibc i (IBCTotal n a) f = return f { ibc_total = (n,a) : ibc_total f }

109111

110112process :: IBCFile -> FilePath -> Idris ()

111113process i fn

@@ -131,6 +133,7 @@ process i fn

131133 pHdrs (ibc_hdrs i)

132134 pDefs (ibc_defs i)

133135 pAccess (ibc_access i)

136+ pTotal (ibc_total i)

134137

135138timestampOlder :: FilePath -> FilePath -> IO ()

136139timestampOlder src ibc = do srct <- getModificationTime src

@@ -231,6 +234,12 @@ pAccess ds = mapM_ (\ (n, a) ->

231234 putIState (i { tt_ctxt = setAccess n a (tt_ctxt i) }))

232235 ds

233236

237+pTotal :: [(Name, Totality)] -> Idris ()

238+pTotal ds = mapM_ (\ (n, a) ->

239+ do i <- getIState

240+ putIState (i { tt_ctxt = setTotal n a (tt_ctxt i) }))

241+ ds

242+

234243----- Generated by 'derive'

235244

236245

@@ -580,8 +589,40 @@ instance Binary Accessibility where

580589 2 -> return Hidden

581590 _ -> error "Corrupted binary data for Accessibility"

582591

592+instance Binary PReason where

593+ put x

594+ = case x of

595+ Other x1 -> do putWord8 0

596+ put x1

597+ Itself -> putWord8 1

598+ NotCovering -> putWord8 2

599+ NotPositive -> putWord8 3

600+ get

601+ = do i <- getWord8

602+ case i of

603+ 0 -> do x1 <- get

604+ return (Other x1)

605+ 1 -> return Itself

606+ 2 -> return NotCovering

607+ 3 -> return NotPositive

608+ _ -> error "Corrupted binary data for PReason"

609+

610+instance Binary Totality where

611+ put x

612+ = case x of

613+ Total -> putWord8 0

614+ Partial x1 -> do putWord8 1

615+ put x1

616+ get

617+ = do i <- getWord8

618+ case i of

619+ 0 -> return Total

620+ 1 -> do x1 <- get

621+ return (Partial x1)

622+ _ -> error "Corrupted binary data for Totality"

623+

583624instance Binary IBCFile where

584− put (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17)

625+ put (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18)

585626 = do put x1

586627 put x2

587628 put x3

@@ -599,6 +640,7 @@ instance Binary IBCFile where

599640 put x15

600641 put x16

601642 put x17

643+ put x18

602644 get

603645 = do x1 <- get

604646 if x1 == ibcVersion then

@@ -618,7 +660,8 @@ instance Binary IBCFile where

618660 x15 <- get

619661 x16 <- get

620662 x17 <- get

621− return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17)

663+ x18 <- get

664+ return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18)

622665 else return (initIBC { ver = x1 })

623666

624667instance Binary Fixity where

src/Idris/REPL.hs+3

@@ -176,6 +176,9 @@ process fn (Defn n) = do i <- get

176176 [] -> return ()

177177 [d] -> do iputStrLn "Original definiton:\n"

178178 mapM_ (printCase i) d

179+ case lookupTotal n (tt_ctxt i) of

180+ [t] -> iputStrLn (show t)

181+ _ -> return ()

179182 where printCase i (lhs, rhs) = do liftIO $ putStr $ showImp True (delab i lhs)

180183 liftIO $ putStr " = "

181184 liftIO $ putStrLn $ showImp True (delab i rhs)