git.iko.soy/Idris-dev
on master help sign in
'compute' rather than whnf on disambiguation

It turns out that when we have deeply nested constructors, we end up computing an awful lot so we should do it all in advance. Otherwise, things slow down more than they should.

commit25eea964c229f5e6f1ca3282b7f7c47181c909ff authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 28 Nov 2016, 19:59 (10 years ago) parent8dc243f
2 files changed+11−11
compare with master
unifiedsplit
src/Idris/Elab/Term.hs+2−2 test/error005/expected+9−9
src/Idris/Elab/Term.hs+2−2
@@ -500,11 +500,11 @@ elab ist info emode opts fn tm
500500 showHd x = getNameFrom (sMN 0 "_") -- We probably should do something better than this here
501501
502502 doPrune as =
503− do whnf_compute -- to get 'Delayed' if it's there
503+ do compute -- to get 'Delayed' if it's there
504504 ty <- goal
505505 ctxt <- get_context
506506 env <- get_env
507− let ty' = whnf ctxt env (unDelay ty)
507+ let ty' = unDelay ty
508508 let (tc, _) = unApply ty'
509509 return $ pruneByType eimpossible env tc ty' ist as
510510
test/error005/expected+9−9
@@ -2,8 +2,8 @@ error005.idr:13:1:When checking right hand side of two with expected type
22 Fin 2
33
44When checking argument prf to function Data.Fin.fromInteger:
5− When using 2 as a literal for a Fin (fromIntegerNat 2)
6− 2 is not strictly less than fromIntegerNat 2
5+ When using 2 as a literal for a Fin 2
6+ 2 is not strictly less than 2
77error005.idr:16:1:When checking right hand side of hahaha with expected type
88 Fin n
99
@@ -14,18 +14,18 @@ error005.idr:22:1:When checking right hand side of notOk with expected type
1414 Fin (plus 2 n)
1515
1616When checking argument prf to function Data.Fin.fromInteger:
17− When using 2 as a literal for a Fin (plus (fromIntegerNat 2) n)
18− 2 is not strictly less than plus (fromIntegerNat 2) n
17+ When using 2 as a literal for a Fin (S (S n))
18+ 2 is not strictly less than S (S n)
1919error005.idr:23:24:When checking right hand side of b0rken with expected type
2020 Fin 3
2121
2222When checking argument prf to function Data.Fin.fromInteger:
23− When using n as a literal for a Fin (fromIntegerNat 3)
24− Could not show that n is less than fromIntegerNat 3 because n is
25− a bound variable instead of a constant Integer
23+ When using n as a literal for a Fin 3
24+ Could not show that n is less than 3 because n is a bound
25+ variable instead of a constant Integer
2626error005.idr:28:1:When checking right hand side of x with expected type
2727 Fin 4
2828
2929When checking argument prf to function Data.Fin.fromInteger:
30− When using 5 as a literal for a Fin (fromIntegerNat 4)
31− 5 is not strictly less than fromIntegerNat 4
30+ When using 5 as a literal for a Fin 4
31+ 5 is not strictly less than 4