git.iko.soy/Idris-dev
on master help sign in
Prefer 'List' at the REPL

This makes it easier for beginners to try things without explaining 'with', disambiguation, etc. List is preferred only if there has been a "Can't disambiguate" error.

commit65b5c20d45d4a7e870a096098d918e809c7f3a9a authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 28 Jun 2015, 15:18 (11 years ago) parente3dcb11
2 files changed+12−4
compare with master
unifiedsplit
src/Idris/Elab/Value.hs+9−1 src/Idris/REPL.hs+3−3
src/Idris/Elab/Value.hs+9−1
@@ -1,6 +1,7 @@
11{-# LANGUAGE PatternGuards #-}
22{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
3−module Idris.Elab.Value(elabVal, elabValBind, elabDocTerms, elabExec) where
3+module Idris.Elab.Value(elabVal, elabValBind, elabDocTerms,
4+ elabExec, elabREPL) where
45
56import Idris.AbsSyntax
67import Idris.ASTUtils
@@ -130,3 +131,10 @@ elabExec fc tm = runtm (PAlternative FirstSuccess
130131 printtm t = PApp fc (PRef fc (sUN "printLn"))
131132 [pimp (sUN "ffi") (PRef fc (sUN "FFI_C")) False, pexp t]
132133
134+elabREPL :: ElabInfo -> ElabMode -> PTerm -> Idris (Term, Type)
135+elabREPL info aspat tm
136+ = idrisCatch (elabVal info aspat tm) catchAmbig
137+ where
138+ catchAmbig (CantResolveAlts _)
139+ = elabVal info aspat (PDisamb [[txt "List"]] tm)
140+ catchAmbig e = ierror e
src/Idris/REPL.hs+3−3
@@ -774,7 +774,7 @@ process fn (Eval t)
774774 = withErrorReflection $
775775 do logLvl 5 $ show t
776776 getIState >>= flip warnDisamb t
777− (tm, ty) <- elabVal recinfo ERHS t
777+ (tm, ty) <- elabREPL recinfo ERHS t
778778 ctxt <- getContext
779779 let tm' = perhapsForce $ normaliseAll ctxt [] tm
780780 let ty' = perhapsForce $ normaliseAll ctxt [] ty
@@ -931,7 +931,7 @@ process fn (Check (PRef _ n))
931931
932932
933933process fn (Check t)
934− = do (tm, ty) <- elabVal recinfo ERHS t
934+ = do (tm, ty) <- elabREPL recinfo ERHS t
935935 ctxt <- getContext
936936 ist <- getIState
937937 let ppo = ppOptionIst ist
@@ -943,7 +943,7 @@ process fn (Check t)
943943 (pprintDelab ist ty)
944944
945945process fn (Core t)
946− = do (tm, ty) <- elabVal recinfo ERHS t
946+ = do (tm, ty) <- elabREPL recinfo ERHS t
947947 iPrintTermWithType (pprintTT [] tm) (pprintTT [] ty)
948948
949949process fn (DocStr (Left n) w)