df41e3d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Give a bit more context for error messages

That is, say what part of what is being elaborated at the time. Still todo, better rendering of generated names like decorated names in where blocks, generated function types in classes and instances etc.

commitdf41e3d397c0e8401b98a2e7b7b047ba4df8f910 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 10 Sep 2013, 14:54 (13 years ago) parente8f4bb1

11 files changed+49−19

compare with master

unifiedsplit

src/Core/Elaborate.hs+10−1 src/Core/Evaluate.hs+3 src/Core/TT.hs+2 src/Idris/Delaborate.hs+2 src/Idris/ElabDecls.hs+19−11 test/reg003/expected+6−3 test/reg010/expected+2−1 test/test020/expected+1 test/test030/expected+2−1 tutorial/examples/bmain.idr+1−1 tutorial/examples/btree.idr+1−1

src/Core/Elaborate.hs+10−1

@@ -59,6 +59,15 @@ loadState = do (ES p s e) <- get

5959 Just st -> put st

6060 _ -> fail "Nothing to undo"

6161

62+errAt :: String -> Name -> Elab' aux a -> Elab' aux a

63+errAt thing n elab = do s <- get

64+ case runStateT elab s of

65+ OK (a, s') -> do put s'

66+ return a

67+ Error (At f e) ->

68+ lift $ Error (At f (Elaborating thing n e))

69+ Error e -> lift $ Error (Elaborating thing n e)

70+

6271erun :: FC -> Elab' aux a -> Elab' aux a

6372erun f elab = do s <- get

6473 case runStateT elab s of

@@ -263,7 +272,7 @@ regret = processTactic' Regret

263272compute :: Elab' aux ()

264273compute = processTactic' Compute

265274

266−computeLet :: Name -> Elab' aux ()

275+computeLet :: Name -> Elab' aux ()

267276computeLet n = processTactic' (ComputeLet n)

268277

269278simplify :: Elab' aux ()

src/Core/Evaluate.hs+3

@@ -554,8 +554,11 @@ instance Show Def where

554554 show (Operator ty _ _) = "Operator: " ++ show ty

555555 show (CaseOp (CaseInfo inlc inlr) ty ps_in ps cd)

556556 = let (ns, sc) = cases_compiletime cd

557+ (ns_t, sc_t) = cases_totcheck cd

557558 (ns', sc') = cases_runtime cd in

558559 "Case: " ++ show ty ++ " " ++ show ps ++ "\n" ++

560+ "TOTALITY CHECK TIME:\n\n" ++

561+ show ns_t ++ " " ++ show sc_t ++ "\n\n" ++

559562 "COMPILE TIME:\n\n" ++

560563 show ns ++ " " ++ show sc ++ "\n\n" ++

561564 "RUN TIME:\n\n" ++

src/Core/TT.hs+2

@@ -78,6 +78,7 @@ data Err = Msg String

7878 | ProofSearchFail Err

7979 | NoRewriting Term

8080 | At FC Err

81+ | Elaborating String Name Err

8182 | ProviderError String

8283 deriving Eq

8384

@@ -98,6 +99,7 @@ instance Sized Err where

9899 size UniverseError = 1

99100 size ProgramLineComment = 1

100101 size (At fc err) = size fc + size err

102+ size (Elaborating _ n err) = size err

101103 size (ProviderError msg) = length msg

102104 size _ = 1

103105

src/Idris/Delaborate.hs+2

@@ -153,6 +153,8 @@ pshow i (AlreadyDefined n) = show n ++ " is already defined"

153153pshow i (ProofSearchFail e) = pshow i e

154154pshow i (NoRewriting tm) = "rewrite did not change type " ++ show (delab i tm)

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

156+pshow i (Elaborating s n e) = "When elaborating " ++ s ++

157+ showbasic n ++ ":\n" ++ pshow i e

156158pshow i (ProviderError msg) = "Type provider error: " ++ msg

157159

158160showSc i [] = ""

src/Idris/ElabDecls.hs+19−11

@@ -57,8 +57,9 @@ elabType info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in

5757 ty' <- implicit syn n ty'

5858 let ty = addImpl i ty'

5959 logLvl 2 $ show n ++ " type " ++ showImp Nothing True False ty

60− ((tyT, defer, is), log) <- tclift $ elaborate ctxt n (TType (UVal 0)) []

61− (erun fc (build i info False n ty))

60+ ((tyT, defer, is), log) <-

61+ tclift $ elaborate ctxt n (TType (UVal 0)) []

62+ (errAt "type of " n (erun fc (build i info False n ty)))

6263 ds <- checkDef fc defer

6364 addDeferred ds

6465 mapM_ (elabCaseBlock info) is

@@ -139,8 +140,9 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)

139140 i <- getIState

140141 t_in <- implicit syn n t_in

141142 let t = addImpl i t_in

142− ((t', defer, is), log) <- tclift $ elaborate ctxt n (TType (UVal 0)) []

143− (erun fc (build i info False n t))

143+ ((t', defer, is), log) <-

144+ tclift $ elaborate ctxt n (TType (UVal 0)) []

145+ (errAt "data declaration " n (erun fc (build i info False n t)))

144146 def' <- checkDef fc defer

145147 addDeferredTyCon def'

146148 mapM_ (elabCaseBlock info) is

@@ -484,8 +486,9 @@ elabCon info syn tn codata (doc, n, t_in, fc)

484486 t_in <- implicit syn n (if codata then mkLazy t_in else t_in)

485487 let t = addImpl i t_in

486488 logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ showImp Nothing True False t

487− ((t', defer, is), log) <- tclift $ elaborate ctxt n (TType (UVal 0)) []

488− (erun fc (build i info False n t))

489+ ((t', defer, is), log) <-

490+ tclift $ elaborate ctxt n (TType (UVal 0)) []

491+ (errAt "constructor " n (erun fc (build i info False n t)))

489492 logLvl 2 $ "Rechecking " ++ show t'

490493 def' <- checkDef fc defer

491494 addDeferred def'

@@ -800,7 +803,8 @@ elabClause info tcgen (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

800803 logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show (fn_ty, fn_is))

801804 ((lhs', dlhs, []), _) <-

802805 tclift $ elaborate ctxt (MN 0 "patLHS") infP []

803− (erun fc (buildTC i info True tcgen fname (infTerm lhs)))

806+ (errAt "left hand side of " fname

807+ (erun fc (buildTC i info True tcgen fname (infTerm lhs))))

804808 let lhs_tm = orderPats (getInferTerm lhs')

805809 let lhs_ty = getInferType lhs'

806810 logLvl 3 ("Elaborated: " ++ show lhs_tm)

@@ -835,8 +839,10 @@ elabClause info tcgen (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

835839 ((rhs', defer, is), _) <-

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

837841 (do pbinds lhs_tm

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

839− erun fc $ psolve lhs_tm

842+ (_, _, is) <- errAt "right hand side of " fname

843+ (erun fc (build i info False fname rhs))

844+ errAt "right hand side of " fname

845+ (erun fc $ psolve lhs_tm)

840846 tt <- get_term

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

842848 return (tm, ds, is))

@@ -934,7 +940,8 @@ elabClause info tcgen (_, PWith fc fname lhs_in withs wval_in withblock)

934940 logLvl 5 ("LHS: " ++ showImp Nothing True False lhs)

935941 ((lhs', dlhs, []), _) <-

936942 tclift $ elaborate ctxt (MN 0 "patLHS") infP []

937− (erun fc (buildTC i info True tcgen fname (infTerm lhs)))

943+ (errAt "left hand side of with in " fname

944+ (erun fc (buildTC i info True tcgen fname (infTerm lhs))) )

938945 let lhs_tm = orderPats (getInferTerm lhs')

939946 let lhs_ty = getInferType lhs'

940947 let ret_ty = getRetTy lhs_ty

@@ -950,7 +957,8 @@ elabClause info tcgen (_, PWith fc fname lhs_in withs wval_in withblock)

950957 (bindTyArgs PVTy bargs infP) []

951958 (do pbinds lhs_tm

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

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

960+ (_', d, is) <- errAt "with value in " fname

961+ (erun fc (build i info False fname (infTerm wval)))

954962 erun fc $ psolve lhs_tm

955963 tt <- get_term

956964 return (tt, d, is))

test/reg003/expected+6−3

@@ -1,4 +1,7 @@

1−reg003a.idr:4:No such variable OddList

2−reg003a.idr:7:No such variable EvenList

3−reg003a.idr:10:No such variable EvenList

1+reg003a.idr:4:When elaborating constructor ECons:

2+No such variable OddList

3+reg003a.idr:7:When elaborating constructor OCons:

4+No such variable EvenList

5+reg003a.idr:10:When elaborating type of test:

6+No such variable EvenList

47reg003a.idr:10:No type declaration for test

test/reg010/expected+2−1

@@ -1,4 +1,5 @@

1−reg010.idr:5:Can't unify P x with P y

1+reg010.idr:5:When elaborating right hand side of usubst.unsafeSubst:

2+Can't unify P x with P y

34Specifically:

45 Can't unify P x with P y

test/test020/expected+1

@@ -1,3 +1,4 @@

1+When elaborating right hand side of Main.foo:

12test020a.idr:16:Can't unify Vect n a with List a

34Specifically:

test/test030/expected+2−1

@@ -1,4 +1,5 @@

1−test030a.idr:12:Can't unify IsJust (Just x) with IsJust (prove (getProof x))

1+test030a.idr:12:When elaborating right hand side of test030.testReflect1:

2+Can't unify IsJust (Just x) with IsJust (prove (getProof x))

34Specifically:

45 Can't unify Just x with Nothing

tutorial/examples/bmain.idr+1−1

@@ -4,5 +4,5 @@ import btree

55main : IO ()

66main = do let t = toTree [1,8,2,7,9,3]

7− print (toList t)

7+ print (btree.toList t)

tutorial/examples/btree.idr+1−1

@@ -10,7 +10,7 @@ insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)

1010

1111toList : BTree a -> List a

1212toList Leaf = []

13−toList (Node l v r) = toList l ++ (v :: toList r)

13+toList (Node l v r) = btree.toList l ++ (v :: btree.toList r)

1414

1515toTree : Ord a => List a -> BTree a

1616toTree [] = Leaf