33baa44 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

More on errors; propagate line numbers

33baa44Edwin Brady15 years ago

src/Core/ProofState.hs+1−1

compare with master

unifiedsplit

@@ -308,7 +308,7 @@ solve ctxt env (Bind x (Guess ty val) sc)

308 -- unified = (uh, uns ++ [(x, val)]),

309 instances = instances ps \\ [x] })

310 return $ {- Bind x (Let ty val) sc -} instantiate val (pToV x sc)

311− | otherwise = fail $ "I see a hole in your solution. " ++ showEnv env val

311+ | otherwise = lift $ tfail $ IncompleteTerm val

312solve _ _ h = fail $ "Not a guess " ++ show h

313

314introTy :: Raw -> Maybe Name -> RunTactic

src/Idris/Coverage.hs+26−25

@@ -274,38 +274,39 @@ calcTotality path fc n pats

274checkTotality :: [Name] -> FC -> Name -> Idris Totality

275checkTotality path fc n

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

277− | otherwise

277+ | otherwise = do

278− = do t <- getTotality n

278+ t <- getTotality n

279− ctxt <- getContext

279+ ctxt <- getContext

280− case t of

281− Unchecked -> case lookupDef Nothing n ctxt of

282− [CaseOp _ _ pats _ _ _ _] ->

283− do i <- getIState

280+ i <- getIState

284− let opts = case lookupCtxt Nothing n (idris_flags i) of

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

285− [fs] -> fs

282+ [fs] -> fs

286− [] -> []

283+ [] -> []

284+ t' <- case t of

285+ Unchecked ->

286+ case lookupDef Nothing n ctxt of

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

287− t' <- if AssertTotal `elem` opts

288+ do t' <- if AssertTotal `elem` opts

288− then return $ Total []

289+ then return $ Total []

289− else calcTotality path fc n pats

290+ else calcTotality path fc n pats

290− if TotalFn `elem` opts

291− then case t' of

292− Total _ -> return ()

293− e -> totalityError t'

294− else return ()

295− setTotality n t'

291+ setTotality n t'

296− addIBC (IBCTotal n t')

292+ addIBC (IBCTotal n t')

297− -- if it's not total, it can't reduce, to keep

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

298− -- typechecking decidable

294+ -- typechecking decidable

299− case t' of

295+ case t' of

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

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

301-- p@(Partial _) ->

297-- p@(Partial _) ->

302-- do setAccessibility n Frozen

298-- do setAccessibility n Frozen

303-- addIBC (IBCAccess n Frozen)

299-- addIBC (IBCAccess n Frozen)

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

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

305 _ -> return ()

301 _ -> return ()

306− return t'

302+ return t'

307− _ -> return $ Total []

303+ _ -> return $ Total []

308 x -> return x

304 x -> return x

305+ if TotalFn `elem` opts

306+ then case t' of

307+ Total _ -> return t'

308+ e -> totalityError t'

309+ else return t'

309 where

310 where

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

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

311

312

src/Idris/Delaborate.hs+9−6

@@ -19,17 +19,20 @@ delab' ist tm fullname = de [] tm

19 un = FC "(val)" 0

21 de env (App f a) = deFn env f [a]

22− de env (V i) | i < length env = PRef un (env!!i)

22+ de env (V i) | i < length env = PRef un (snd (env!!i))

23 | otherwise = PRef un (UN ("v" ++ show i ++ ""))

24 de env (P _ n _) | n == unitTy = PTrue un

25 | n == unitCon = PTrue un

26 | n == falseTy = PFalse un

27+ | Just n' <- lookup n env = PRef un n'

27 | otherwise = PRef un (dens n)

28 | otherwise = PRef un (dens n)

28− de env (Bind n (Lam ty) sc) = PLam n (de env ty) (de (n:env) sc)

29+ de env (Bind n (Lam ty) sc) = PLam n (de env ty) (de ((n,n):env) sc)

29− de env (Bind n (Pi ty) sc) = PPi expl n (de env ty) (de (n:env) sc)

30+ de env (Bind n (Pi ty) sc) = PPi expl n (de env ty) (de ((n,n):env) sc)

30 de env (Bind n (Let ty val) sc)

31 de env (Bind n (Let ty val) sc)

31− = PLet n (de env ty) (de env val) (de (n:env) sc)

32+ = PLet n (de env ty) (de env val) (de ((n,n):env) sc)

33+ de env (Bind n (Hole ty) sc) = de ((n, UN "[__]"):env) sc

34+ de env (Bind n (Guess ty val) sc) = de ((n, UN "[__]"):env) sc

32− de env (Bind n _ sc) = de (n:env) sc

35+ de env (Bind n _ sc) = de ((n,n):env) sc

33 de env (Constant i) = PConstant i

36 de env (Constant i) = PConstant i

34 de env Erased = Placeholder

37 de env Erased = Placeholder

35 de env (Set i) = PSet

38 de env (Set i) = PSet

@@ -76,7 +79,7 @@ pshow i (NotInjective p x y) = "Can't verify injectivity of " ++ show (delab i p

76 show (delab i y)

79 show (delab i y)

77pshow i (CantResolve c) = "Can't resolve type class " ++ show (delab i c)

80pshow i (CantResolve c) = "Can't resolve type class " ++ show (delab i c)

78pshow i (NoSuchVariable n) = "No such variable " ++ show n

81pshow i (NoSuchVariable n) = "No such variable " ++ show n

79−pshow i (IncompleteTerm t) = "Incomplete term " ++ show t

82+pshow i (IncompleteTerm t) = "Incomplete term " ++ show (delab i t)

80pshow i UniverseError = "Universe inconsistency"

83pshow i UniverseError = "Universe inconsistency"

81pshow i ProgramLineComment = "Program line next to comment"

84pshow i ProgramLineComment = "Program line next to comment"

82pshow i (At f e) = show f ++ ":" ++ pshow i e

85pshow i (At f e) = show f ++ ":" ++ pshow i e

src/Idris/ElabDecls.hs+8−6

@@ -28,7 +28,9 @@ import Debug.Trace

29recheckC ctxt fc env t

30 = do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...)

31− (tm, ty, cs) <- tclift $ recheck ctxt env (forget t) t

31+ (tm, ty, cs) <- tclift $ case recheck ctxt env (forget t) t of

32+ Error e -> tfail (At fc e)

33+ OK x -> return x

32 addConstraints fc cs

34 addConstraints fc cs

33 return (tm, ty)

35 return (tm, ty)

@@ -283,8 +285,8 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

283 tcase pcover pdef pdef' ty)

285 tcase pcover pdef pdef' ty)

284 addIBC (IBCDef n)

286 addIBC (IBCDef n)

285 setTotality n tot

287 setTotality n tot

286− if (tot == Unchecked) then totcheck (fc, n)

288+ totcheck (fc, n)

287− else addIBC (IBCTotal n tot)

289+ when (tot /= Unchecked) $ addIBC (IBCTotal n tot)

288 i <- get

290 i <- get

289 case lookupDef Nothing n (tt_ctxt i) of

291 case lookupDef Nothing n (tt_ctxt i) of

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

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

@@ -320,7 +322,7 @@ elabVal info aspat tm_in

320 logLvl 3 ("Value: " ++ show tm')

322 logLvl 3 ("Value: " ++ show tm')

321 let vtm = getInferTerm tm'

323 let vtm = getInferTerm tm'

322 logLvl 2 (show vtm)

324 logLvl 2 (show vtm)

323− recheckC ctxt (FC "prompt" 0) [] vtm

325+ recheckC ctxt (FC "(input)" 0) [] vtm

324

326

325-- checks if the clause is a possible left hand side. Returns the term if

327-- checks if the clause is a possible left hand side. Returns the term if

326-- possible, otherwise Nothing.

328-- possible, otherwise Nothing.

@@ -381,7 +383,7 @@ elabClause info tcgen (PClause fc fname lhs_in withs rhs_in whereblock)

381 tclift $ elaborate ctxt (MN 0 "patRHS") clhsty []

383 tclift $ elaborate ctxt (MN 0 "patRHS") clhsty []

382 (do pbinds lhs_tm

384 (do pbinds lhs_tm

383 (_, _, is) <- erun fc (build i info False fname rhs)

385 (_, _, is) <- erun fc (build i info False fname rhs)

384− psolve lhs_tm

386+ erun fc $ psolve lhs_tm

385 tt <- get_term

387 tt <- get_term

386 let (tm, ds) = runState (collectDeferred tt) []

388 let (tm, ds) = runState (collectDeferred tt) []

387 return (tm, ds, is))

389 return (tm, ds, is))

@@ -436,7 +438,7 @@ elabClause info tcgen (PWith fc fname lhs_in withs wval_in withblock)

436 (do pbinds lhs_tm

438 (do pbinds lhs_tm

437 -- TODO: may want where here - see winfo abpve

439 -- TODO: may want where here - see winfo abpve

438 (_', d, is) <- erun fc (build i info False fname (infTerm wval))

440 (_', d, is) <- erun fc (build i info False fname (infTerm wval))

439− psolve lhs_tm

441+ erun fc $ psolve lhs_tm

440 tt <- get_term

442 tt <- get_term

441 return (tt, d, is))

443 return (tt, d, is))

442 def' <- checkDef fc defer

444 def' <- checkDef fc defer

test/test002/expected+1−1

@@ -1 +1 @@

1−test002.idr:7:Universe inconsistency

1+test002.idr:5:Universe inconsistency

test/test010/expected+1−1

@@ -1 +1 @@

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

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

tutorial/examples/theorems.idr+4

@@ -12,6 +12,10 @@ disjoint n p = replace {P = disjointTy} p ()

12 disjointTy O = ()

13 disjointTy (S k) = _|_

15+total acyclic : (n : Nat) -> n = S n -> _|_

16+acyclic O p = disjoint _ p

17+acyclic (S k) p = acyclic k _ -- (succInjective _ _ p)

18+

15empty1 : _|_

19empty1 : _|_

16empty1 = hd [] where

20empty1 = hd [] where

17 hd : List a -> a

21 hd : List a -> a