idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-09-11 13:36:08 +03:00
Code Issues Projects Releases Wiki Activity

[ fix #1230 ] Better error messages for out-of-scope identifiers (#1233)

Browse Source
This commit is contained in:
G. Allais 2021-03-29 10:45:48 +01:00 committed by GitHub
parent ec77ad21ab
commit 238eb62da6
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
32 changed files with 339 additions and 73 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
idris2api.ipkg
View File

@ -106,6 +106,7 @@ modules =
Libraries.Data.DList,
Libraries.Data.IMaybe,
Libraries.Data.IntMap,
Libraries.Data.IOMatrix,
Libraries.Data.LengthMatch,
Libraries.Data.List.Extra,
Libraries.Data.List.Lazy,
@ -119,6 +120,7 @@ modules =
Libraries.Data.StringTrie,
Libraries.Text.Bounded,
Libraries.Text.Distance.Levenshtein,
Libraries.Text.Lexer,
Libraries.Text.Lexer.Core,
Libraries.Text.Lexer.Tokenizer,

93
src/Core/Context.idr
View File

@ -15,9 +15,12 @@ import Libraries.Utils.Binary
import Libraries.Data.IntMap
import Data.IOArray
import Data.List
import Data.List1
import Data.Maybe
import Data.Nat
import Libraries.Data.NameMap
import Libraries.Data.StringMap
import Libraries.Text.Distance.Levenshtein
import System
import System.Directory
@ -1069,6 +1072,54 @@ clearCtxt
resetElab : Options -> Options
resetElab = record { elabDirectives = defaultElab }
-- Find similar looking names in the context
getSimilarNames : {auto c : Ref Ctxt Defs} -> Name -> Core (List String)
getSimilarNames nm = case userNameRoot nm of
Nothing => pure []
Just str => if length str <= 1 then pure [] else
let threshold : Nat := max 1 (assert_total (divNat (length str) 3))
test : Name -> IO (Maybe Nat) := \ nm => do
let (Just str') = userNameRoot nm
| _ => pure Nothing
dist <- Levenshtein.compute str str'
pure (dist <$ guard (dist <= threshold))
in do defs <- get Ctxt
kept <- coreLift $ mapMaybeM test (resolvedAs (gamma defs))
let sorted = sortBy (\ x, y => compare (snd x) (snd y)) $ toList kept
let roots = mapMaybe (showNames nm str . fst) sorted
pure (nub roots)
where
showNames : Name -> String -> Name -> Maybe String
showNames target str nm = do
let root = nameRoot nm
let True = str == root | _ => pure root
let full = show nm
let True = str == full || show target == full | _ => pure full
Nothing
maybeMisspelling : {auto c : Ref Ctxt Defs} ->
Error -> Name -> Core a
maybeMisspelling err nm = do
candidates <- getSimilarNames nm
case candidates of
[] => throw err
(x::xs) => throw (MaybeMisspelling err (x ::: xs))
-- Throw an UndefinedName exception. But try to find similar names first.
export
undefinedName : {auto c : Ref Ctxt Defs} ->
FC -> Name -> Core a
undefinedName loc nm = maybeMisspelling (UndefinedName loc nm) nm
-- Throw a NoDeclaration exception. But try to find similar names first.
export
noDeclaration : {auto c : Ref Ctxt Defs} ->
FC -> Name -> Core a
noDeclaration loc nm = maybeMisspelling (NoDeclaration loc nm) nm
-- Get the canonical name of something that might have been aliased via
-- import as
export
@ -1077,7 +1128,7 @@ canonicalName : {auto c : Ref Ctxt Defs} ->
canonicalName fc n
= do defs <- get Ctxt
case !(lookupCtxtName n (gamma defs)) of
[] => throw (UndefinedName fc n)
[] => undefinedName fc n
[(n, _, _)] => pure n
ns => throw (AmbiguousName fc (map fst ns))
@ -1444,7 +1495,7 @@ setFlag : {auto c : Ref Ctxt Defs} ->
setFlag fc n fl
= do defs <- get Ctxt
Just def <- lookupCtxtExact n (gamma defs)
| Nothing => throw (UndefinedName fc n)
| Nothing => undefinedName fc n
let flags' = fl :: filter (/= fl) (flags def)
ignore $ addDef n (record { flags = flags' } def)
@ -1454,7 +1505,7 @@ setNameFlag : {auto c : Ref Ctxt Defs} ->
setNameFlag fc n fl
= do defs <- get Ctxt
[(n', i, def)] <- lookupCtxtName n (gamma defs)
| [] => throw (UndefinedName fc n)
| [] => undefinedName fc n
| res => throw (AmbiguousName fc (map fst res))
let flags' = fl :: filter (/= fl) (flags def)
ignore $ addDef (Resolved i) (record { flags = flags' } def)
@ -1465,7 +1516,7 @@ unsetFlag : {auto c : Ref Ctxt Defs} ->
unsetFlag fc n fl
= do defs <- get Ctxt
Just def <- lookupCtxtExact n (gamma defs)
| Nothing => throw (UndefinedName fc n)
| Nothing => undefinedName fc n
let flags' = filter (/= fl) (flags def)
ignore $ addDef n (record { flags = flags' } def)
@ -1475,7 +1526,7 @@ hasFlag : {auto c : Ref Ctxt Defs} ->
hasFlag fc n fl
= do defs <- get Ctxt
Just def <- lookupCtxtExact n (gamma defs)
| Nothing => throw (UndefinedName fc n)
| Nothing => undefinedName fc n
pure (fl `elem` flags def)
export
@ -1484,7 +1535,7 @@ setSizeChange : {auto c : Ref Ctxt Defs} ->
setSizeChange loc n sc
= do defs <- get Ctxt
Just def <- lookupCtxtExact n (gamma defs)
| Nothing => throw (UndefinedName loc n)
| Nothing => undefinedName loc n
ignore $ addDef n (record { sizeChange = sc } def)
export
@ -1493,7 +1544,7 @@ setTotality : {auto c : Ref Ctxt Defs} ->
setTotality loc n tot
= do defs <- get Ctxt
Just def <- lookupCtxtExact n (gamma defs)
| Nothing => throw (UndefinedName loc n)
| Nothing => undefinedName loc n
ignore $ addDef n (record { totality = tot } def)
export
@ -1502,7 +1553,7 @@ setCovering : {auto c : Ref Ctxt Defs} ->
setCovering loc n tot
= do defs <- get Ctxt
Just def <- lookupCtxtExact n (gamma defs)
| Nothing => throw (UndefinedName loc n)
| Nothing => undefinedName loc n
ignore $ addDef n (record { totality->isCovering = tot } def)
export
@ -1511,7 +1562,7 @@ setTerminating : {auto c : Ref Ctxt Defs} ->
setTerminating loc n tot
= do defs <- get Ctxt
Just def <- lookupCtxtExact n (gamma defs)
| Nothing => throw (UndefinedName loc n)
| Nothing => undefinedName loc n
ignore $ addDef n (record { totality->isTerminating = tot } def)
export
@ -1520,7 +1571,7 @@ getTotality : {auto c : Ref Ctxt Defs} ->
getTotality loc n
= do defs <- get Ctxt
Just def <- lookupCtxtExact n (gamma defs)
| Nothing => throw (UndefinedName loc n)
| Nothing => undefinedName loc n
pure $ totality def
export
@ -1529,7 +1580,7 @@ getSizeChange : {auto c : Ref Ctxt Defs} ->
getSizeChange loc n
= do defs <- get Ctxt
Just def <- lookupCtxtExact n (gamma defs)
| Nothing => throw (UndefinedName loc n)
| Nothing => undefinedName loc n
pure $ sizeChange def
export
@ -1538,7 +1589,7 @@ setVisibility : {auto c : Ref Ctxt Defs} ->
setVisibility fc n vis
= do defs <- get Ctxt
Just def <- lookupCtxtExact n (gamma defs)
| Nothing => throw (UndefinedName fc n)
| Nothing => undefinedName fc n
ignore $ addDef n (record { visibility = vis } def)
-- Set a name as Private that was previously visible (and, if 'everywhere' is
@ -1549,7 +1600,7 @@ hide : {auto c : Ref Ctxt Defs} ->
hide fc n
= do defs <- get Ctxt
[(nsn, _)] <- lookupCtxtName n (gamma defs)
| [] => throw (UndefinedName fc n)
| [] => undefinedName fc n
| res => throw (AmbiguousName fc (map fst res))
put Ctxt (record { gamma $= hideName nsn } defs)
@ -1559,7 +1610,7 @@ getVisibility : {auto c : Ref Ctxt Defs} ->
getVisibility fc n
= do defs <- get Ctxt
Just def <- lookupCtxtExact n (gamma defs)
| Nothing => throw (UndefinedName fc n)
| Nothing => undefinedName fc n
pure $ visibility def
public export
@ -1589,7 +1640,7 @@ getSearchData : {auto c : Ref Ctxt Defs} ->
getSearchData fc defaults target
= do defs <- get Ctxt
Just (TCon _ _ _ dets u _ _ _) <- lookupDefExact target (gamma defs)
| _ => throw (UndefinedName fc target)
| _ => undefinedName fc target
hs <- case lookup !(toFullNames target) (typeHints defs) of
Just hs => filterM (\x => notHidden x (gamma defs)) hs
Nothing => pure []
@ -1630,7 +1681,7 @@ setMutWith : {auto c : Ref Ctxt Defs} ->
setMutWith fc tn tns
= do defs <- get Ctxt
Just g <- lookupCtxtExact tn (gamma defs)
| _ => throw (UndefinedName fc tn)
| _ => undefinedName fc tn
let TCon t a ps dets u _ cons det = definition g
| _ => throw (GenericMsg fc (show (fullname g) ++ " is not a type constructor [setMutWith]"))
updateDef tn (const (Just (TCon t a ps dets u tns cons det)))
@ -1655,7 +1706,7 @@ setDetermining : {auto c : Ref Ctxt Defs} ->
setDetermining fc tyn args
= do defs <- get Ctxt
Just g <- lookupCtxtExact tyn (gamma defs)
| _ => throw (UndefinedName fc tyn)
| _ => undefinedName fc tyn
let TCon t a ps _ u cons ms det = definition g
| _ => throw (GenericMsg fc (show (fullname g) ++ " is not a type constructor [setDetermining]"))
apos <- getPos 0 args (type g)
@ -1679,7 +1730,7 @@ setDetags : {auto c : Ref Ctxt Defs} ->
setDetags fc tyn args
= do defs <- get Ctxt
Just g <- lookupCtxtExact tyn (gamma defs)
| _ => throw (UndefinedName fc tyn)
| _ => undefinedName fc tyn
let TCon t a ps det u cons ms _ = definition g
| _ => throw (GenericMsg fc (show (fullname g) ++ " is not a type constructor [setDetermining]"))
updateDef tyn (const (Just (TCon t a ps det u cons ms args)))
@ -1690,7 +1741,7 @@ setUniqueSearch : {auto c : Ref Ctxt Defs} ->
setUniqueSearch fc tyn u
= do defs <- get Ctxt
Just g <- lookupCtxtExact tyn (gamma defs)
| _ => throw (UndefinedName fc tyn)
| _ => undefinedName fc tyn
let TCon t a ps ds fl cons ms det = definition g
| _ => throw (GenericMsg fc (show (fullname g) ++ " is not a type constructor [setDetermining]"))
let fl' = record { uniqueAuto = u } fl
@ -1702,7 +1753,7 @@ setExternal : {auto c : Ref Ctxt Defs} ->
setExternal fc tyn u
= do defs <- get Ctxt
Just g <- lookupCtxtExact tyn (gamma defs)
| _ => throw (UndefinedName fc tyn)
| _ => undefinedName fc tyn
let TCon t a ps ds fl cons ms det = definition g
| _ => throw (GenericMsg fc (show (fullname g) ++ " is not a type constructor [setDetermining]"))
let fl' = record { external = u } fl
@ -2114,7 +2165,7 @@ checkUnambig : {auto c : Ref Ctxt Defs} ->
checkUnambig fc n
= do defs <- get Ctxt
case !(lookupDefName n (gamma defs)) of
[] => throw (UndefinedName fc n)
[] => undefinedName fc n
[(fulln, i, _)] => pure (Resolved i)
ns => throw (AmbiguousName fc (map fst ns))

10
src/Core/Core.idr
View File

@ -154,6 +154,8 @@ data Error : Type where
InLHS : FC -> Name -> Error -> Error
InRHS : FC -> Name -> Error -> Error
MaybeMisspelling : Error -> List1 String -> Error
public export
data Warning : Type where
UnreachableClause : {vars : _} ->
@ -189,7 +191,8 @@ Show Error where
case prob of
Left tm => assert_total (show tm) ++ " is not a valid impossible pattern because it typechecks"
Right err => "Not a valid impossible pattern:\n\t" ++ assert_total (show err)
show (UndefinedName fc x) = show fc ++ ":Undefined name " ++ show x
show (UndefinedName fc x)
= show fc ++ ":Undefined name " ++ show x
show (InvisibleName fc x (Just ns))
= show fc ++ ":Name " ++ show x ++ " is inaccessible since " ++
show ns ++ " is not explicitly imported"
@ -331,6 +334,10 @@ Show Error where
= show fc ++ ":When elaborating right hand side of " ++ show n ++ ":\n" ++
show err
show (MaybeMisspelling err ns)
= show err ++ "\nDid you mean" ++ case ns of
(n ::: []) => ": " ++ n ++ "?"
_ => " any of: " ++ showSep ", " (map show (forget ns)) ++ "?"
export
getErrorLoc : Error -> Maybe FC
getErrorLoc (Fatal err) = getErrorLoc err
@ -400,6 +407,7 @@ getErrorLoc (InType _ _ err) = getErrorLoc err
getErrorLoc (InCon _ _ err) = getErrorLoc err
getErrorLoc (InLHS _ _ err) = getErrorLoc err
getErrorLoc (InRHS _ _ err) = getErrorLoc err
getErrorLoc (MaybeMisspelling err _) = getErrorLoc err
export
getWarningLoc : Warning -> Maybe FC

2
src/Core/Coverage.idr
View File

@ -413,7 +413,7 @@ getNonCoveringRefs : {auto c : Ref Ctxt Defs} ->
getNonCoveringRefs fc n
= do defs <- get Ctxt
Just d <- lookupCtxtExact n (gamma defs)
| Nothing => throw (UndefinedName fc n)
| Nothing => undefinedName fc n
let ds = mapMaybe noAssert (toList (refersTo d))
let cases = filter isCase !(traverse toFullNames ds)

4
src/Core/GetType.idr
View File

@ -25,12 +25,12 @@ mutual
chk env (Ref fc nt n)
= do defs <- get Ctxt
Just ty <- lookupTyExact n (gamma defs)
| Nothing => throw (UndefinedName fc n)
| Nothing => undefinedName fc n
pure $ gnf env (embed ty)
chk env (Meta fc n i args)
= do defs <- get Ctxt
Just mty <- lookupTyExact (Resolved i) (gamma defs)
| Nothing => throw (UndefinedName fc n)
| Nothing => undefinedName fc n
chkMeta fc env !(nf defs env (embed mty)) args
chk env (Bind fc nm b sc)
= do bt <- chkBinder env b

10
src/Core/LinearCheck.idr
View File

@ -214,7 +214,7 @@ mutual
lcheck {vars} rig erase env (Meta fc n idx args)
= do defs <- get Ctxt
Just gdef <- lookupCtxtExact (Resolved idx) (gamma defs)
| _ => throw (UndefinedName fc n)
| _ => undefinedName fc n
let expand = branchZero
(case type gdef of
Erased _ _ => True -- defined elsewhere, need to expand
@ -344,7 +344,7 @@ mutual
fused ++ aused)
NApp _ (NRef _ n) _ =>
do Just _ <- lookupCtxtExact n (gamma defs)
| _ => throw (UndefinedName fc n)
| _ => undefinedName fc n
tfty <- getTerm gfty
throw (GenericMsg fc ("Linearity checking failed on " ++ show f' ++
" (" ++ show tfty ++ " not a function type)"))
@ -584,14 +584,14 @@ mutual
lcheckDef fc rig True env n
= do defs <- get Ctxt
Just def <- lookupCtxtExact n (gamma defs)
| Nothing => throw (UndefinedName fc n)
| Nothing => undefinedName fc n
pure (type def)
lcheckDef fc rig False env n
= do defs <- get Ctxt
let Just idx = getNameID n (gamma defs)
| Nothing => throw (UndefinedName fc n)
| Nothing => undefinedName fc n
Just def <- lookupCtxtExact (Resolved idx) (gamma defs)
| Nothing => throw (UndefinedName fc n)
| Nothing => undefinedName fc n
rigSafe (multiplicity def) rig
if linearChecked def
then pure (type def)

10
src/Core/Termination.idr
View File

@ -363,7 +363,7 @@ mutual
-- Under 'assert_total' we assume that all calls are fine, so leave
-- the size change list empty
= do Just gdef <- lookupCtxtExact fn_in (gamma defs)
| Nothing => throw (UndefinedName fc fn_in)
| Nothing => undefinedName fc fn_in
let fn = fullname gdef
log "totality.termination.sizechange" 10 $ "Looking under " ++ show !(toFullNames fn)
aSmaller <- resolved (gamma defs) (NS builtinNS (UN "assert_smaller"))
@ -415,7 +415,7 @@ calculateSizeChange loc n
= do log "totality.termination.sizechange" 5 $ "Calculating Size Change: " ++ show !(toFullNames n)
defs <- get Ctxt
Just def <- lookupCtxtExact n (gamma defs)
| Nothing => throw (UndefinedName loc n)
| Nothing => undefinedName loc n
getSC defs (definition def)
Arg : Type
@ -528,7 +528,7 @@ calcTerminating loc n
= do defs <- get Ctxt
log "totality.termination.calc" 7 $ "Calculating termination: " ++ show !(toFullNames n)
case !(lookupCtxtExact n (gamma defs)) of
Nothing => throw (UndefinedName loc n)
Nothing => undefinedName loc n
Just def =>
case !(totRefs defs (nub !(addCases defs (keys (refersTo def))))) of
IsTerminating =>
@ -662,7 +662,7 @@ calcPositive loc n
pure (t , dcons)
bad => pure (bad, dcons)
Just _ => throw (GenericMsg loc (show n ++ " not a data type"))
Nothing => throw (UndefinedName loc n)
Nothing => undefinedName loc n
-- Check whether a data type satisfies the strict positivity condition, and
-- record in the context
@ -690,7 +690,7 @@ checkTotal : {auto c : Ref Ctxt Defs} ->
checkTotal loc n_in
= do defs <- get Ctxt
let Just nidx = getNameID n_in (gamma defs)
| Nothing => throw (UndefinedName loc n_in)
| Nothing => undefinedName loc n_in
let n = Resolved nidx
tot <- getTotality loc n
log "totality" 5 $ "Checking totality: " ++ show !(toFullNames n)

10
src/Core/Unify.idr
View File

@ -248,7 +248,7 @@ postpone blockedMetas loc mode logstr env x y
checkDefined : Defs -> NF vars -> Core ()
checkDefined defs (NApp _ (NRef _ n) _)
= do Just _ <- lookupCtxtExact n (gamma defs)
| _ => throw (UndefinedName loc n)
| _ => undefinedName loc n
pure ()
checkDefined _ _ = pure ()
@ -757,7 +757,7 @@ mutual
unifyHoleApp swap mode loc env mname mref margs margs' tm@(NApp nfc (NMeta n i margs2) args2')
= do defs <- get Ctxt
Just mdef <- lookupCtxtExact (Resolved i) (gamma defs)
| Nothing => throw (UndefinedName nfc mname)
| Nothing => undefinedName nfc mname
let inv = isPatName n || invertible mdef
if inv
then unifyInvertible swap (lower mode) loc env mname mref margs margs' Nothing
@ -1323,7 +1323,7 @@ setInvertible : {auto c : Ref Ctxt Defs} ->
setInvertible fc n
= do defs <- get Ctxt
Just gdef <- lookupCtxtExact n (gamma defs)
| Nothing => throw (UndefinedName fc n)
| Nothing => undefinedName fc n
ignore $ addDef n (record { invertible = True } gdef)
public export
@ -1605,7 +1605,7 @@ checkDots
dotSolved <-
maybe (pure False)
(\n => do Just ndef <- lookupDefExact n (gamma defs)
| Nothing => throw (UndefinedName fc n)
| Nothing => undefinedName fc n
case ndef of
Hole _ _ => pure False
_ => pure True)
@ -1622,7 +1622,7 @@ checkDots
InternalError _ =>
do defs <- get Ctxt
Just dty <- lookupTyExact n (gamma defs)
| Nothing => throw (UndefinedName fc n)
| Nothing => undefinedName fc n
logTermNF "unify.constraint" 5 "Dot type" [] dty
-- Clear constraints so we don't report again
-- later

4
src/Idris/DocString.idr
View File

@ -69,7 +69,7 @@ getDocsForName fc n
= do syn <- get Syn
defs <- get Ctxt
all@(_ :: _) <- lookupCtxtName n (gamma defs)
| _ => throw (UndefinedName fc n)
| _ => undefinedName fc n
let ns@(_ :: _) = concatMap (\n => lookupName n (docstrings syn))
(map fst all)
| [] => pure ["No documentation for " ++ show n]
@ -162,7 +162,7 @@ getDocsForName fc n
showDoc (n, str)
= do defs <- get Ctxt
Just def <- lookupCtxtExact n (gamma defs)
| Nothing => throw (UndefinedName fc n)
| Nothing => undefinedName fc n
ty <- normaliseHoles defs [] (type def)
let doc = show !(aliasName n) ++ " : " ++ show !(resugar [] ty)
++ "\n" ++ addNL (indent str)

6
src/Idris/Elab/Implementation.idr
View File

@ -138,15 +138,15 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps named im
inames <- lookupCtxtName iname (gamma defs)
let [cndata] = concatMap (\n => lookupName n (ifaces syn))
(map fst inames)
| [] => throw (UndefinedName fc iname)
| [] => undefinedName fc iname
| ns => throw (AmbiguousName fc (map fst ns))
let cn : Name = fst cndata
let cdata : IFaceInfo = snd cndata
Just ity <- lookupTyExact cn (gamma defs)
| Nothing => throw (UndefinedName fc cn)
| Nothing => undefinedName fc cn
Just conty <- lookupTyExact (iconstructor cdata) (gamma defs)
| Nothing => throw (UndefinedName fc (iconstructor cdata))
| Nothing => undefinedName fc (iconstructor cdata)
let impsp = nub (concatMap findIBinds ps ++
concatMap findIBinds (map snd cons))

2
src/Idris/Elab/Interface.idr
View File

@ -357,7 +357,7 @@ elabInterface {vars} fc vis env nest constraints iname params dets mcon body
pure (record { name = n } mt)) meth_decls
defs <- get Ctxt
Just ty <- lookupTyExact ns_iname (gamma defs)
| Nothing => throw (UndefinedName fc iname)
| Nothing => undefinedName fc iname
let implParams = getImplParams ty
updateIfaceSyn ns_iname conName

16
src/Idris/Error.idr
View File

@ -15,7 +15,7 @@ import Idris.Pretty
import Parser.Source
import Data.List
import Data.List1
import Libraries.Data.List1 as Lib
import Libraries.Data.List.Extra
import Data.Maybe
import Data.Stream
@ -293,8 +293,8 @@ perror (AllFailed ts)
allUndefined : List (Maybe Name, Error) -> Maybe Error
allUndefined [] = Nothing
allUndefined [(_, UndefinedName loc e)] = Just (UndefinedName loc e)
allUndefined ((_, UndefinedName _ e) :: es) = allUndefined es
allUndefined [(_, err@(UndefinedName _ _))] = Just err
allUndefined ((_, err@(UndefinedName _ _)) :: es) = allUndefined es
allUndefined _ = Nothing
perror (RecordTypeNeeded fc _)
= pure $ errorDesc (reflow "Can't infer type for this record update.") <+> line <+> !(ploc fc)
@ -430,7 +430,7 @@ perror (UserError str) = pure $ errorDesc (pretty "Error" <+> colon) <++> pretty
perror (NoForeignCC fc) = do
let cgs = fst <$> availableCGs (options !(get Ctxt))
let res = vsep [ errorDesc (reflow "The given specifier was not accepted by any backend. Available backends" <+> colon)
, indent 2 (concatWith (\x,y => x <+> ", " <+> y) (map reflow cgs))
, indent 2 (concatWith (\ x, y => x <+> ", " <+> y) (map reflow cgs))
, reflow "Some backends have additional specifier rules, refer to their documentation."
] <+> line <+> !(ploc fc)
pure res
@ -453,6 +453,14 @@ perror (InRHS fc n err)
, !(perror err)
]
perror (MaybeMisspelling err ns) = pure $ !(perror err) <+> case ns of
(n ::: []) => reflow "Did you mean:" <++> pretty n <+> "?"
_ => let (xs, x) = Lib.unsnoc ns in
reflow "Did you mean any of:"
<++> concatWith (surround (comma <+> space)) (map pretty xs)
<+> comma <++> reflow "or" <++> pretty x <+> "?"
export
pwarning : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->

12
src/Idris/REPL.idr
View File

@ -385,7 +385,7 @@ processEdit (TypeAt line col name)
(_, Just (n, _, type)) => pure $ DisplayEdit $
pretty (nameRoot n) <++> colon <++> !(displayTerm defs type)
(Just globalDoc, Nothing) => pure $ DisplayEdit $ globalDoc
(Nothing, Nothing) => throw (UndefinedName replFC name)
(Nothing, Nothing) => undefinedName replFC name
processEdit (CaseSplit upd line col name)
= do let find = if col > 0
@ -673,7 +673,7 @@ docsOrSignature fc n
= do syn <- get Syn
defs <- get Ctxt
all@(_ :: _) <- lookupCtxtName n (gamma defs)
| _ => throw (UndefinedName fc n)
| _ => undefinedName fc n
let ns@(_ :: _) = concatMap (\n => lookupName n (docstrings syn))
(map fst all)
| [] => typeSummary defs
@ -770,7 +770,7 @@ process (Check (PRef fc (UN "it")))
process (Check (PRef fc fn))
= do defs <- get Ctxt
case !(lookupCtxtName fn (gamma defs)) of
[] => throw (UndefinedName fc fn)
[] => undefinedName fc fn
ts => do tys <- traverse (displayType defs) ts
pure (Printed $ vsep tys)
process (Check itm)
@ -787,7 +787,7 @@ process (Check itm)
process (PrintDef fn)
= do defs <- get Ctxt
case !(lookupCtxtName fn (gamma defs)) of
[] => throw (UndefinedName replFC fn)
[] => undefinedName replFC fn
ts => do defs <- traverse (displayPats defs) ts
pure (Printed $ vsep defs)
process Reload
@ -848,7 +848,7 @@ process (TypeSearch searchTerm)
process (Missing n)
= do defs <- get Ctxt
case !(lookupCtxtName n (gamma defs)) of
[] => throw (UndefinedName replFC n)
[] => undefinedName replFC n
ts => map Missed $ traverse (\fn =>
do tot <- getTotality replFC fn
the (Core MissedResult) $ case isCovering tot of
@ -863,7 +863,7 @@ process (Missing n)
process (Total n)
= do defs <- get Ctxt
case !(lookupCtxtName n (gamma defs)) of
[] => throw (UndefinedName replFC n)
[] => undefinedName replFC n
ts => map CheckedTotal $
traverse (\fn =>
do ignore $ checkTotal replFC fn

41
src/Libraries/Data/IOMatrix.idr Normal file
View File

@ -0,0 +1,41 @@
module Libraries.Data.IOMatrix
import Data.IOArray.Prims
export
record IOMatrix a where
constructor MkIOMatrix
maxWidth : Int
maxHeight : Int
content : ArrayData (Maybe a)
export
width : IOMatrix a -> Int
width = maxWidth
export
height : IOMatrix a -> Int
height = maxHeight
export
new : HasIO io => (width, height : Int) -> io (IOMatrix a)
new width height
= pure $ MkIOMatrix width height
!(primIO (prim__newArray (width * height) Nothing))
toPosition : IOMatrix a -> Int -> Int -> Maybe Int
toPosition (MkIOMatrix w h arr) i j
= do guard (not (i < 0 || j < 0 || i >= w || j >= h))
pure (i * h + j)
export
write : HasIO io => IOMatrix a -> Int -> Int -> a -> io Bool
write mat i j el = case toPosition mat i j of
Nothing => pure False
Just pos => True <$ primIO (prim__arraySet (content mat) pos (Just el))
export
read : HasIO io => IOMatrix a -> Int -> Int -> io (Maybe a)
read mat i j = case toPosition mat i j of
Nothing => pure Nothing
Just pos => primIO (prim__arrayGet (content mat) pos)

5
src/Libraries/Data/List/Extra.idr
View File

@ -1,9 +1,14 @@
module Libraries.Data.List.Extra
import Data.List
import Data.List1
%default total
export
minimum : Ord a => (xs : List a) -> {auto 0 _ : NonEmpty xs} -> a
minimum (x :: xs) = foldl min x xs
||| Fetches the element at a given position.
||| Returns `Nothing` if the position beyond the list's end.
public export

41
src/Libraries/Data/NameMap.idr
View File

@ -316,3 +316,44 @@ Semigroup v => Semigroup (NameMap v) where
export
(Semigroup v) => Monoid (NameMap v) where
neutral = empty
treeFilterByM : Monad m => (Key -> m Bool) -> Tree n v -> m (NameMap v)
treeFilterByM test = loop empty where
loop : NameMap v -> Tree _ v -> m (NameMap v)
loop acc (Leaf k v)
= do True <- test k | _ => pure acc
pure (insert k v acc)
loop acc (Branch2 t1 _ t2)
= do acc <- loop acc t1
loop acc t2
loop acc (Branch3 t1 _ t2 _ t3)
= do acc <- loop acc t1
acc <- loop acc t2
loop acc t3
export
filterByM : Monad m => (Name -> m Bool) -> NameMap v -> m (NameMap v)
filterByM test Empty = pure Empty
filterByM test (M _ t) = treeFilterByM test t
treeMapMaybeM : Monad m => (Key -> m (Maybe a)) -> Tree _ v -> m (NameMap a)
treeMapMaybeM test = loop empty where
loop : NameMap a -> Tree _ v -> m (NameMap a)
loop acc (Leaf k v)
= do Just a <- test k | _ => pure acc
pure (insert k a acc)
loop acc (Branch2 t1 _ t2)
= do acc <- loop acc t1
loop acc t2
loop acc (Branch3 t1 _ t2 _ t3)
= do acc <- loop acc t1
acc <- loop acc t2
loop acc t3
export
mapMaybeM : Monad m => (Name -> m (Maybe a)) -> NameMap v -> m (NameMap a)
mapMaybeM test Empty = pure Empty
mapMaybeM test (M _ t) = treeMapMaybeM test t

68
src/Libraries/Text/Distance/Levenshtein.idr Normal file
View File

@ -0,0 +1,68 @@
module Libraries.Text.Distance.Levenshtein
import Data.List
import Data.Maybe
import Data.Strings
import Libraries.Data.IOMatrix
import Libraries.Data.List.Extra
%default total
||| Self-evidently correct but O(3 ^ (min mn)) complexity
spec : String -> String -> Nat
spec a b = loop (fastUnpack a) (fastUnpack b) where
loop : List Char -> List Char -> Nat
loop [] ys = length ys -- deletions
loop xs [] = length xs -- insertions
loop (x :: xs) (y :: ys)
= if x == y then loop xs ys -- match
else 1 + minimum [ loop (x :: xs) ys -- insert y
, loop xs (y :: ys) -- delete x
, loop xs ys -- substitute y for x
]
||| Dynamic programming
export
compute : HasIO io => String -> String -> io Nat
compute a b = assert_total $ do
let w = strLength a
let h = strLength b
-- In mat[i][j], we store the distance between
-- * the suffix of a of size i
-- * the suffix of b of size j
-- So we need a matrix of size (|a|+1) * (|b|+1)
mat <- new (w+1) (h+1)
-- Whenever one of the two suffixes of interest is empty, the only
-- winning move is to:
-- * delete all of the first
-- * insert all of the second
-- i.e. the cost is the length of the non-zero suffix
for_ [0..w] $ \ i => write mat i 0 i -- deletions
for_ [0..h] $ \ j => write mat 0 j j -- insertions
-- We introduce a specialised `read` for ease of use
let get = \i, j => case !(read {io} mat i j) of
Nothing => idris_crash "INTERNAL ERROR: Badly initialised matrix"
Just n => pure n
-- We fill the matrix from the bottom up, using the same formula we used
-- in the specification's `loop`.
for_ [1..h] $ \ j => do
for_ [1..w] $ \ i => do
-- here we change Levenshtein slightly so that we may only substitute
-- alpha / numerical characters for similar ones. This avoids suggesting
-- "#" as a replacement for an out of scope "n".
let cost = let c = strIndex a (i-1)
d = strIndex b (j-1)
in if c == d then 0 else
if isAlpha c && isAlpha d then 1 else
if isDigit c && isDigit d then 1 else 2
write mat i j $
minimum [ 1 + !(get i (j-1)) -- insert y
, 1 + !(get (i-1) j) -- delete x
, cost + !(get (i-1) (j-1)) -- equal or substitute y for x
]
-- Once the matrix is fully filled, we can simply read the top right corner
integerToNat . cast <$> get w h

4
src/TTImp/Elab/App.idr
View File

@ -59,7 +59,7 @@ getNameType rigc env fc x
Nothing =>
do defs <- get Ctxt
[(pname, i, def)] <- lookupCtxtName x (gamma defs)
| [] => throw (UndefinedName fc x)
| [] => undefinedName fc x
| ns => throw (AmbiguousName fc (map fst ns))
checkVisibleNS fc !(getFullName pname) (visibility def)
rigSafe (multiplicity def) rigc
@ -91,7 +91,7 @@ getVarType rigc nest env fc x
let arglen = length argns
let n' = maybe x id nestn
case !(lookupCtxtExact n' (gamma defs)) of
Nothing => throw (UndefinedName fc n')
Nothing => undefinedName fc n'
Just ndef =>
let nt = case definition ndef of
PMDef _ _ _ _ _ => Func

2
src/TTImp/Elab/Term.idr
View File

@ -261,7 +261,7 @@ checkTerm rig elabinfo nest env (IWithUnambigNames fc ns rhs) exp
ctxt <- get Ctxt
rns <- lookupCtxtName n (gamma ctxt)
case rns of
[] => throw $ UndefinedName fc n
[] => undefinedName fc n
[rn] => insert nRoot rn <$> resolveNames fc ns
_ => throw $ AmbiguousName fc (map fst rns)

2
src/TTImp/Impossible.idr
View File

@ -135,7 +135,7 @@ mutual
gdefs <- lookupNameBy id n (gamma defs)
[(n', _, gdef)] <- dropNoMatch mty gdefs
| [] => throw (UndefinedName fc n)
| [] => undefinedName fc n
| ts => throw (AmbiguousName fc (map fst ts))
tynf <- nf defs [] (type gdef)
-- #899 we need to make sure that type & data constructors are marked

4
src/TTImp/Interactive/CaseSplit.idr
View File

@ -199,7 +199,7 @@ expandCon : {auto c : Ref Ctxt Defs} ->
expandCon fc usedvars con
= do defs <- get Ctxt
Just ty <- lookupTyExact con (gamma defs)
| Nothing => throw (UndefinedName fc con)
| Nothing => undefinedName fc con
pure (apply (IVar fc con)
(map (IBindVar fc)
!(getArgNames defs [] usedvars []
@ -402,7 +402,7 @@ getSplitsLHS fc envlen lhs_in n
trycases <- traverse (\c => newLHS fc envlen usedns n c rawlhs) cons
let Just idx = getNameID fn (gamma defs)
| Nothing => throw (UndefinedName fc fn)
| Nothing => undefinedName fc fn
cases <- traverse (mkCase idx rawlhs) trycases
pure (combine cases [])

4
src/TTImp/Interactive/ExprSearch.idr
View File

@ -811,7 +811,7 @@ search fc rig opts topty n_in
throw (InternalError $ "Not a hole: " ++ show n ++ " in " ++
show (map recname (recData opts)))
_ => do log "interaction.search" 10 $ show n_in ++ " not found"
throw (UndefinedName fc n_in)
undefinedName fc n_in
where
lookupHoleName : Name -> Context ->
Core (Maybe (Name, Int, GlobalDef))
@ -864,7 +864,7 @@ exprSearchOpts : {auto c : Ref Ctxt Defs} ->
exprSearchOpts opts fc n_in hints
= do defs <- get Ctxt
Just (n, idx, gdef) <- lookupHoleName n_in defs
| Nothing => throw (UndefinedName fc n_in)
| Nothing => undefinedName fc n_in
lhs <- findHoleLHS !(getFullName (Resolved idx))
log "interaction.search" 10 $ "LHS hole data " ++ show (n, lhs)
opts' <- if getRecData opts

2
src/TTImp/Interactive/GenerateDef.idr
View File

@ -219,7 +219,7 @@ makeDefFromType loc opts n envlen ty
(apply (IVar loc n) (pre_env ++ (map (IBindVar loc) argns)))
(IHole loc rhshole)
let Just nidx = getNameID n (gamma defs)
| Nothing => throw (UndefinedName loc n)
| Nothing => undefinedName loc n
cs' <- mkSplits loc opts nidx initcs
-- restore the global state, given that we've fiddled with it a lot!
put Ctxt defs

2
src/TTImp/ProcessDef.idr
View File

@ -823,7 +823,7 @@ processDef opts nest env fc n_in cs_in
= do n <- inCurrentNS n_in
defs <- get Ctxt
Just gdef <- lookupCtxtExact n (gamma defs)
| Nothing => throw (NoDeclaration fc n)
| Nothing => noDeclaration fc n
let None = definition gdef
| _ => throw (AlreadyDefined fc n)
let ty = type gdef

4
src/TTImp/ProcessType.idr
View File

@ -41,7 +41,7 @@ processFnOpt fc _ ndef TCInline
processFnOpt fc True ndef (Hint d)
= do defs <- get Ctxt
Just ty <- lookupTyExact ndef (gamma defs)
| Nothing => throw (UndefinedName fc ndef)
| Nothing => undefinedName fc ndef
target <- getRetTy defs !(nf defs [] ty)
addHintFor fc target ndef d False
processFnOpt fc _ ndef (Hint d)
@ -64,7 +64,7 @@ processFnOpt fc _ ndef Macro
processFnOpt fc _ ndef (SpecArgs ns)
= do defs <- get Ctxt
Just gdef <- lookupCtxtExact ndef (gamma defs)
| Nothing => throw (UndefinedName fc ndef)
| Nothing => undefinedName fc ndef
nty <- nf defs [] (type gdef)
ps <- getNamePos 0 nty
ddeps <- collectDDeps nty

8
src/Yaffle/REPL.idr
View File

@ -65,7 +65,7 @@ process (Check ttimp)
process (ProofSearch n_in)
= do defs <- get Ctxt
[(n, i, ty)] <- lookupTyName n_in (gamma defs)
| [] => throw (UndefinedName toplevelFC n_in)
| [] => undefinedName toplevelFC n_in
| ns => throw (AmbiguousName toplevelFC (map fst ns))
def <- search toplevelFC top False 1000 n ty []
defs <- get Ctxt
@ -75,7 +75,7 @@ process (ProofSearch n_in)
process (ExprSearch n_in)
= do defs <- get Ctxt
[(n, i, ty)] <- lookupTyName n_in (gamma defs)
| [] => throw (UndefinedName toplevelFC n_in)
| [] => undefinedName toplevelFC n_in
| ns => throw (AmbiguousName toplevelFC (map fst ns))
results <- exprSearchN toplevelFC 1 n []
traverse_ (\d => coreLift (printLn d)) results
@ -99,7 +99,7 @@ process (GenerateDef line name)
process (Missing n_in)
= do defs <- get Ctxt
case !(lookupCtxtName n_in (gamma defs)) of
[] => throw (UndefinedName emptyFC n_in)
[] => undefinedName emptyFC n_in
ts => do traverse_ (\fn =>
do tot <- getTotality emptyFC fn
the (Core ()) $ case isCovering tot of
@ -118,7 +118,7 @@ process (Missing n_in)
process (CheckTotal n)
= do defs <- get Ctxt
case !(lookupCtxtName n (gamma defs)) of
[] => throw (UndefinedName emptyFC n)
[] => undefinedName emptyFC n
ts => do traverse_ (\fn =>
do ignore $ checkTotal emptyFC fn
tot <- getTotality emptyFC fn

1
tests/Main.idr
View File

@ -68,6 +68,7 @@ idrisTestsError = MkTestPool []
["error001", "error002", "error003", "error004", "error005",
"error006", "error007", "error008", "error009", "error010",
"error011", "error012", "error013", "error014", "error015",
"error016",
-- Parse errors
"perror001", "perror002", "perror003", "perror004", "perror005",
"perror006", "perror007", "perror008"]

2
tests/idris2/basic041/expected
View File

@ -8,4 +8,4 @@ QDo.idr:27:10--27:11
26 | test = B.A.do
27 | 5
^
Did you mean any of: Main.A.B.>>, Prelude.Interfaces.>>, Main.MyDo.>>, >, >=>, or >>=?

9
tests/idris2/error016/Issue1230.idr Normal file
View File

@ -0,0 +1,9 @@
record R where
constructor MkR
field : Nat
myRec1 : R
myRec1 = MkR 3
mkRec2 : R
myRec2 = MkR 3

25
tests/idris2/error016/expected Normal file
View File

@ -0,0 +1,25 @@
1/1: Building Issue1230 (Issue1230.idr)
Error: No type declaration for Main.myRec2.
Issue1230.idr:9:1--9:15
5 | myRec1 : R
6 | myRec1 = MkR 3
7 |
8 | mkRec2 : R
9 | myRec2 = MkR 3
^^^^^^^^^^^^^^
Did you mean any of: mkRec2, or myRec1?
Main> Error: Undefined name nap.
(interactive):1:4--1:7
1 | :t nap
^^^
Did you mean: map?
Main> Error: Undefined name lentgh.
(interactive):1:4--1:10
1 | :t lentgh
^^^^^^
Did you mean: length?
Main>
Bye for now!

3
tests/idris2/error016/input Normal file
View File

@ -0,0 +1,3 @@
:t nap
:t lentgh
:q

4
tests/idris2/error016/run Executable file
View File

@ -0,0 +1,4 @@
$1 --no-color --console-width 0 --no-banner --check Issue1230.idr
$1 --no-color --console-width 0 --no-banner < input
rm -rf build/