df41e3d · Idris-dev · git.iko.soy

src/Core/Elaborate.hs+10−1

compare with master

unifiedsplit

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

59 Just st -> put st

60 _ -> fail "Nothing to undo"

61

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+

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

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

63erun f elab = do s <- get

72erun f elab = do s <- get

64 case runStateT elab s of

73 case runStateT elab s of

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

263compute :: Elab' aux ()

272compute :: Elab' aux ()

264compute = processTactic' Compute

273compute = processTactic' Compute

265

274

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

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

267computeLet n = processTactic' (ComputeLet n)

276computeLet n = processTactic' (ComputeLet n)

268

277

269simplify :: Elab' aux ()

278simplify :: Elab' aux ()

src/Core/Evaluate.hs+3

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

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

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

556 = let (ns, sc) = cases_compiletime cd

557+ (ns_t, sc_t) = cases_totcheck cd

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

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

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

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

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

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

559 "COMPILE TIME:\n\n" ++

562 "COMPILE TIME:\n\n" ++

560 show ns ++ " " ++ show sc ++ "\n\n" ++

563 show ns ++ " " ++ show sc ++ "\n\n" ++

561 "RUN TIME:\n\n" ++

564 "RUN TIME:\n\n" ++

src/Core/TT.hs+2

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

78 | ProofSearchFail Err

79 | NoRewriting Term

80 | At FC Err

81+ | Elaborating String Name Err

81 | ProviderError String

82 | ProviderError String

82 deriving Eq

83 deriving Eq

83

84

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

98 size UniverseError = 1

99 size UniverseError = 1

99 size ProgramLineComment = 1

100 size ProgramLineComment = 1

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

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

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

101 size (ProviderError msg) = length msg

103 size (ProviderError msg) = length msg

102 size _ = 1

104 size _ = 1

103

105

src/Idris/Delaborate.hs+2

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

153pshow i (ProofSearchFail e) = pshow i e

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

155pshow 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

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

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

157

159

158showSc i [] = ""

160showSc 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

57 ty' <- implicit syn n ty'

58 let ty = addImpl i ty'

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

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

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

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

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

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

62 ds <- checkDef fc defer

63 ds <- checkDef fc defer

63 addDeferred ds

64 addDeferred ds

64 mapM_ (elabCaseBlock info) is

65 mapM_ (elabCaseBlock info) is

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

139 i <- getIState

140 i <- getIState

140 t_in <- implicit syn n t_in

141 t_in <- implicit syn n t_in

141 let t = addImpl i t_in

142 let t = addImpl i t_in

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

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

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

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

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

144 def' <- checkDef fc defer

146 def' <- checkDef fc defer

145 addDeferredTyCon def'

147 addDeferredTyCon def'

146 mapM_ (elabCaseBlock info) is

148 mapM_ (elabCaseBlock info) is

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

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

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

485 let t = addImpl i t_in

487 let t = addImpl i t_in

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

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

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

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

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

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

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

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

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

490 def' <- checkDef fc defer

493 def' <- checkDef fc defer

491 addDeferred def'

494 addDeferred def'

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

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

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

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

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

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

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

806+ (errAt "left hand side of " fname

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

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

804 let lhs_tm = orderPats (getInferTerm lhs')

808 let lhs_tm = orderPats (getInferTerm lhs')

805 let lhs_ty = getInferType lhs'

809 let lhs_ty = getInferType lhs'

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

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

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

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

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

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

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

837 (do pbinds lhs_tm

841 (do pbinds lhs_tm

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

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

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

844+ errAt "right hand side of " fname

839− erun fc $ psolve lhs_tm

845+ (erun fc $ psolve lhs_tm)

840 tt <- get_term

846 tt <- get_term

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

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

842 return (tm, ds, is))

848 return (tm, ds, is))

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

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

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

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

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

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

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

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

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

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

938 let lhs_tm = orderPats (getInferTerm lhs')

945 let lhs_tm = orderPats (getInferTerm lhs')

939 let lhs_ty = getInferType lhs'

946 let lhs_ty = getInferType lhs'

940 let ret_ty = getRetTy lhs_ty

947 let ret_ty = getRetTy lhs_ty

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

950 (bindTyArgs PVTy bargs infP) []

957 (bindTyArgs PVTy bargs infP) []

951 (do pbinds lhs_tm

958 (do pbinds lhs_tm

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

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

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

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

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

954 erun fc $ psolve lhs_tm

962 erun fc $ psolve lhs_tm

955 tt <- get_term

963 tt <- get_term

956 return (tt, d, is))

964 return (tt, d, is))

test/reg003/expected+6−3

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

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

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

2+No such variable OddList

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

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

4+No such variable EvenList

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

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

6+No such variable EvenList

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

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

test/reg010/expected+2−1

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

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

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

2+Can't unify P x with P y

2

3

3Specifically:

4Specifically:

4 Can't unify P x with P y

5 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:

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

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

2

3

3Specifically:

4Specifically:

test/test030/expected+2−1

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

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

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

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

2

3

3Specifically:

4Specifically:

4 Can't unify Just x with Nothing

5 Can't unify Just x with Nothing

tutorial/examples/bmain.idr+1−1

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

4

5main : IO ()

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

7− print (toList t)

7+ print (btree.toList t)

8

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)

10

11toList : BTree a -> List a

12toList 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)

14

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

16toTree [] = Leaf