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

git.iko.soy/Idris-dev

More on errors; propagate line numbers

commit33baa44c76f81c8bd6a16896e020807f3f0752ad authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateThu 2 Feb 2012, 12:14 (15 years ago) parented72247

7 files changed+50−40

compare with master

unifiedsplit

src/Core/ProofState.hs+1−1 src/Idris/Coverage.hs+26−25 src/Idris/Delaborate.hs+9−6 src/Idris/ElabDecls.hs+8−6 test/test002/expected+1−1 test/test010/expected+1−1 tutorial/examples/theorems.idr+4

src/Core/ProofState.hs+1−1

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

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

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

310310 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

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

313313

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

src/Idris/Coverage.hs+26−25

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

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

275275checkTotality path fc n

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

277− | otherwise

278− = do t <- getTotality n

279− ctxt <- getContext

280− case t of

281− Unchecked -> case lookupDef Nothing n ctxt of

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

283− do i <- getIState

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

285− [fs] -> fs

286− [] -> []

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

288− then return $ Total []

289− 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'

296− addIBC (IBCTotal n t')

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

298− -- typechecking decidable

299− case t' of

277+ | otherwise = do

278+ t <- getTotality n

279+ ctxt <- getContext

280+ i <- getIState

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

282+ [fs] -> fs

283+ [] -> []

284+ t' <- case t of

285+ Unchecked ->

286+ case lookupDef Nothing n ctxt of

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

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

289+ then return $ Total []

290+ else calcTotality path fc n pats

291+ setTotality n t'

292+ addIBC (IBCTotal n t')

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

294+ -- typechecking decidable

295+ case t' of

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

301297-- p@(Partial _) ->

302298-- do setAccessibility n Frozen

303299-- addIBC (IBCAccess n Frozen)

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

305301 _ -> return ()

306− return t'

307− _ -> return $ Total []

302+ return t'

303+ _ -> return $ Total []

308304 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'

309310 where

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

311312

src/Idris/Delaborate.hs+9−6

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

1919 un = FC "(val)" 0

2020

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

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

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

2525 | n == unitCon = PTrue un

2626 | n == falseTy = PFalse un

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

2728 | 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 (Pi ty) sc) = PPi expl 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)

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

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

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

32− de env (Bind n _ sc) = 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

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

3336 de env (Constant i) = PConstant i

3437 de env Erased = Placeholder

3538 de env (Set i) = PSet

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

7679 show (delab i y)

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

7881pshow 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)

8083pshow i UniverseError = "Universe inconsistency"

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

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

src/Idris/ElabDecls.hs+8−6

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

2828

2929recheckC ctxt fc env t

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

3234 addConstraints fc cs

3335 return (tm, ty)

3436

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

283285 tcase pcover pdef pdef' ty)

284286 addIBC (IBCDef n)

285287 setTotality n tot

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

287− else addIBC (IBCTotal n tot)

288+ totcheck (fc, n)

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

288290 i <- get

289291 case lookupDef Nothing n (tt_ctxt i) of

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

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

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

321323 let vtm = getInferTerm tm'

322324 logLvl 2 (show vtm)

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

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

324326

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

326328-- possible, otherwise Nothing.

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

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

382384 (do pbinds lhs_tm

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

384− psolve lhs_tm

386+ erun fc $ psolve lhs_tm

385387 tt <- get_term

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

387389 return (tm, ds, is))

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

436438 (do pbinds lhs_tm

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

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

439− psolve lhs_tm

441+ erun fc $ psolve lhs_tm

440442 tt <- get_term

441443 return (tt, d, is))

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

1212 disjointTy O = ()

1313 disjointTy (S k) = _|_

1414

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

16+acyclic O p = disjoint _ p

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

18+

1519empty1 : _|_

1620empty1 = hd [] where

1721 hd : List a -> a