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

git.iko.soy/Idris-dev

Totality checker tweaks

commit7142d7e5d1b05c60ac7a307737ffc26e83d9c008 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateWed 1 Feb 2012, 16:14 (15 years ago) parentb1e95cb

7 files changed+45−23

compare with master

unifiedsplit

lib/prelude/nat.idr+5−6 src/Core/Evaluate.hs+1−1 src/Idris/AbsSyntax.hs+1−1 src/Idris/Coverage.hs+29−13 src/Idris/ElabDecls.hs+6−2 src/Idris/IBC.hs+2 src/Idris/Parser.hs+1

lib/prelude/nat.idr+5−6

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

6868 (-) = minus

6969 (*) = mult

7070

71− fromInteger 0 = O

72− fromInteger n =

73− if (n > 0) then

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

75− else

76− O

71+ fromInteger = intToNat where

72+ %assert_total

73+ intToNat : Int -> Nat

74+ intToNat 0 = O

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

7776

7877--------------------------------------------------------------------------------

7978-- Division and modulus

src/Core/Evaluate.hs+1−1

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

532532 deriving (Show, Eq)

533533

534534instance Show Totality where

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

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

536536 show Unchecked = "not yet checked for totality"

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

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

src/Idris/AbsSyntax.hs+1−1

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

383383constraint = Constraint False Static

384384tacimpl = TacImp False Dynamic

385385

386−data FnOpt = Inlinable | TotalFn | TCGen

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

387387 deriving (Show, Eq)

388388{-!

389389deriving instance Binary FnOpt

src/Idris/Coverage.hs+29−13

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

198198 = do orders <- mapM ctot pats

199199 let order = sortBy cmpOrd $ concat orders

200200 let (errs, valid) = partitionEithers order

201− let lex = stripXX valid

201+ let lex = stripNoLT (stripXX valid)

202202 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

204205 checkDecreasing lex

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

206207 where

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

216217 dec [] = False

217218 dec (LexLT : _) = True

218219 dec (LexEQ : xs) = dec xs

219− dec (LexXX : _) = False

220+ dec (LexXX : xs) = False

220221

221222 stripXX [] = []

222223 stripXX v@(c : cs)

223224 = case span (==LexXX) c of

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

225226

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

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

229+

226230 ctot (lhs, rhs)

227231 | (_, args) <- unApply lhs

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

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

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

233237 = do ov <- chkOrd ords args v

234238 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

236240 chkOrd ords args ap@(App f a)

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

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

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

269273 case t of

270274 Unchecked -> case lookupDef Nothing n ctxt of

271275 [CaseOp _ _ pats _ _ _ _] ->

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

273− i <- getIState

274− case lookupCtxt Nothing n (idris_flags i) of

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

276− case t' of

277− Total _ -> return ()

278− e -> totalityError t'

279− else return ()

280− _ -> return ()

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 []

282+ else calcTotality path fc n pats

283+ if TotalFn `elem` opts

284+ then case t' of

285+ Total _ -> return ()

286+ e -> totalityError t'

287+ else return ()

281288 setTotality n t'

282289 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 ()

283299 return t'

284300 _ -> return $ Total []

285301 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

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

250250 ist <- get

251251-- let wf = wellFounded ist n sc

252− let tot = if pcover

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

253253 then Unchecked -- finish checking later

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

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

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

773773 elabData info s f d

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

775− elabClauses info f o n ps

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

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

777+ [fs] -> fs

778+ [] -> []

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

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

777781 where

778782 pinfo = let ds = concatMap declared ps

src/Idris/IBC.hs+2

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

694694 Inlinable -> putWord8 0

695695 TotalFn -> putWord8 1

696696 TCGen -> putWord8 2

697+ AssertTotal -> putWord8 3

697698 get

698699 = do i <- getWord8

699700 case i of

700701 0 -> return Inlinable

701702 1 -> return TotalFn

702703 2 -> return TCGen

704+ 3 -> return AssertTotal

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

704706

705707instance Binary Fixity where

src/Idris/Parser.hs+1

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

614614

615615pFnOpts :: IParser [FnOpt]

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

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

617618 <|> return []

618619

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