7142d7e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Totality checker tweaks

7142d7eEdwin Brady15 years ago

lib/prelude/nat.idr+5−6

compare with master

unifiedsplit

@@ -68,12 +68,11 @@ instance Num Nat where

68 (-) = minus

69 (*) = mult

71− fromInteger 0 = O

71+ fromInteger = intToNat where

72− fromInteger n =

72+ %assert_total

73− if (n > 0) then

73+ intToNat : Int -> Nat

74+ intToNat 0 = O

74− (S (fromInteger (n-1)))

75+ intToNat n = if (n > 0) then S (fromInteger (n-1)) else O

75− else

76− O

78--------------------------------------------------------------------------------

77--------------------------------------------------------------------------------

79-- Division and modulus

78-- Division and modulus

src/Core/Evaluate.hs+1−1

@@ -532,7 +532,7 @@ data PReason = Other [Name] | Itself | NotCovering | NotPositive | UseUndef Name

532 deriving (Show, Eq)

533

534instance Show Totality where

535− 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"

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

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

src/Idris/AbsSyntax.hs+1−1

@@ -383,7 +383,7 @@ expl = Exp False Dynamic

383constraint = Constraint False Static

384tacimpl = TacImp False Dynamic

385

386−data FnOpt = Inlinable | TotalFn | TCGen

386+data FnOpt = Inlinable | TotalFn | AssertTotal | TCGen

387 deriving (Show, Eq)

388{-!

389deriving instance Binary FnOpt

src/Idris/Coverage.hs+29−13

@@ -198,9 +198,10 @@ calcTotality path fc n pats

198 = do orders <- mapM ctot pats

199 let order = sortBy cmpOrd $ concat orders

200 let (errs, valid) = partitionEithers order

201− let lex = stripXX valid

201+ let lex = stripNoLT (stripXX valid)

202 case errs of

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

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

204+ logLvl 10 $ show pats

204 checkDecreasing lex

205 checkDecreasing lex

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

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

206 where

207 where

@@ -216,13 +217,16 @@ calcTotality path fc n pats

216 dec [] = False

217 dec [] = False

217 dec (LexLT : _) = True

218 dec (LexLT : _) = True

218 dec (LexEQ : xs) = dec xs

219 dec (LexEQ : xs) = dec xs

219− dec (LexXX : _) = False

220+ dec (LexXX : xs) = False

220

221

221 stripXX [] = []

222 stripXX [] = []

222 stripXX v@(c : cs)

223 stripXX v@(c : cs)

223 = case span (==LexXX) c of

224 = case span (==LexXX) c of

224 (ns, rest) -> map (drop (length ns)) v

225 (ns, rest) -> map (drop (length ns)) v

225

226

227+ -- argument positions which are never LT are no use to us

228+ stripNoLT xs = transpose (filter (any (==LexLT)) (transpose xs))

229+

226 ctot (lhs, rhs)

230 ctot (lhs, rhs)

227 | (_, args) <- unApply lhs

231 | (_, args) <- unApply lhs

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

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

@@ -232,7 +236,7 @@ calcTotality path fc n pats

232 chkOrd ords args (Bind n (Let t v) sc)

236 chkOrd ords args (Bind n (Let t v) sc)

233 = do ov <- chkOrd ords args v

237 = do ov <- chkOrd ords args v

234 chkOrd ov args sc

238 chkOrd ov args sc

235− chkOrd ords args (Bind n b sc) = chkOrd ords args sc

239+ chkOrd ords args (Bind n b sc) = chkOrd ords (args ++ [P Ref n Erased]) sc

236 chkOrd ords args ap@(App f a)

240 chkOrd ords args ap@(App f a)

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

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

238 = if fn == n && length args == length args'

242 = if fn == n && length args == length args'

@@ -269,17 +273,29 @@ checkTotality path fc n

269 case t of

273 case t of

270 Unchecked -> case lookupDef Nothing n ctxt of

274 Unchecked -> case lookupDef Nothing n ctxt of

271 [CaseOp _ _ pats _ _ _ _] ->

275 [CaseOp _ _ pats _ _ _ _] ->

276+ do i <- getIState

277+ let opts = case lookupCtxt Nothing n (idris_flags i) of

278+ [fs] -> fs

279+ [] -> []

280+ t' <- if AssertTotal `elem` opts

281+ then return $ Total []

272− do t' <- calcTotality path fc n pats

282+ else calcTotality path fc n pats

273− i <- getIState

274− case lookupCtxt Nothing n (idris_flags i) of

275− [fs] -> if TotalFn `elem` fs then

283+ if TotalFn `elem` opts

276− case t' of

284+ then case t' of

277− Total _ -> return ()

285+ Total _ -> return ()

278− e -> totalityError t'

286+ e -> totalityError t'

279− else return ()

280− _ -> return ()

287+ else return ()

281 setTotality n t'

288 setTotality n t'

282 addIBC (IBCTotal n t')

289 addIBC (IBCTotal n t')

290+ -- if it's not total, it can't reduce, to keep

291+ -- typechecking decidable

292+ case t' of

293+-- FIXME: Put this back when we can handle mutually recursive things

294+-- p@(Partial _) ->

295+-- do setAccessibility n Frozen

296+-- addIBC (IBCAccess n Frozen)

297+-- iputStrLn $ "HIDDEN: " ++ show n ++ show p

298+ _ -> return ()

283 return t'

299 return t'

284 _ -> return $ Total []

300 _ -> return $ Total []

285 x -> return x

301 x -> return x

src/Idris/ElabDecls.hs+6−2

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

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

250 ist <- get

251-- let wf = wellFounded ist n sc

252− let tot = if pcover

252+ let tot = if pcover || AssertTotal `elem` opts

253 then Unchecked -- finish checking later

254 else Partial NotCovering -- already know it's not total

255-- case lookupCtxt (namespace info) n (idris_flags ist) of

@@ -772,7 +772,11 @@ elabDecl' info (PTy s f o n ty) = do iLOG $ "Elaborating type decl " ++ show

772elabDecl' info (PData s f d) = do iLOG $ "Elaborating " ++ show (d_name d)

773 elabData info s f d

774elabDecl' info d@(PClauses f o n ps) = do iLOG $ "Elaborating clause " ++ show n

775+ i <- get -- get the type options too

776+ let o' = case lookupCtxt Nothing n (idris_flags i) of

777+ [fs] -> fs

778+ [] -> []

775− elabClauses info f o n ps

779+ elabClauses info f (o ++ o') n ps

776elabDecl' info (PParams f ns ps) = mapM_ (elabDecl' pinfo) ps

780elabDecl' info (PParams f ns ps) = mapM_ (elabDecl' pinfo) ps

777 where

781 where

778 pinfo = let ds = concatMap declared ps

782 pinfo = let ds = concatMap declared ps

src/Idris/IBC.hs+2

@@ -694,12 +694,14 @@ instance Binary FnOpt where

694 Inlinable -> putWord8 0

695 TotalFn -> putWord8 1

696 TCGen -> putWord8 2

697+ AssertTotal -> putWord8 3

697 get

698 get

698 = do i <- getWord8

699 = do i <- getWord8

699 case i of

700 case i of

700 0 -> return Inlinable

701 0 -> return Inlinable

701 1 -> return TotalFn

702 1 -> return TotalFn

702 2 -> return TCGen

703 2 -> return TCGen

704+ 3 -> return AssertTotal

703 _ -> error "Corrupted binary data for FnOpt"

705 _ -> error "Corrupted binary data for FnOpt"

704

706

705instance Binary Fixity where

707instance Binary Fixity where

src/Idris/Parser.hs+1

@@ -614,6 +614,7 @@ pAccessibility

614

615pFnOpts :: IParser [FnOpt]

616pFnOpts = do reserved "total"; xs <- pFnOpts; return (TotalFn : xs)

617+ <|> do lchar '%'; reserved "assert_total"; xs <- pFnOpts; return (AssertTotal : xs)

617 <|> return []

618 <|> return []

618

619

619addAcc :: Name -> Maybe Accessibility -> IParser ()

620addAcc :: Name -> Maybe Accessibility -> IParser ()