[ fix #1193 ] Fine tune REPL's typesearch (#1196)

This commit is contained in:
G. Allais 2021-03-17 10:54:09 +00:00 committed by GitHub
parent 405c266b5e
commit 8f71aae705
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
3 changed files with 34 additions and 18 deletions

View File

@ -1379,6 +1379,7 @@ lookupDefTyExact = lookupExactBy (\g => (definition g, type g))
-- private names are only visible in this namespace if their namespace
-- is the current namespace (or an outer one)
-- that is: the namespace of 'n' is a parent of nspace
export
visibleIn : Namespace -> Name -> Visibility -> Bool
visibleIn nspace (NS ns n) Private = isParentOf ns nspace
-- Public and Export names are always visible
@ -1709,7 +1710,7 @@ setExternal fc tyn u
export
addHintFor : {auto c : Ref Ctxt Defs} ->
FC -> Name -> Name -> Bool -> Bool -> Core ()
FC -> Name -> Name -> Bool -> Bool -> Core ()
addHintFor fc tyn_in hintn_in direct loading
= do defs <- get Ctxt
tyn <- toFullNames tyn_in

View File

@ -574,6 +574,11 @@ data Term : List Name -> Type where
Term vars
TType : FC -> Term vars
export
isErased : Term vars -> Bool
isErased (Erased _ _) = True
isErased _ = False
export
getLoc : Term vars -> FC
getLoc (Local fc _ _ _) = fc

View File

@ -678,15 +678,22 @@ equivTypes : {auto c : Ref Ctxt Defs} ->
(ty1 : ClosedTerm) ->
(ty2 : ClosedTerm) ->
Core Bool
equivTypes ty1 ty2 = do defs <- get Ctxt
True <- pure (!(getArity defs [] ty1) == !(getArity defs [] ty2))
| False => pure False
_ <- newRef UST initUState
catch (do res <- unify inTerm replFC [] ty1 ty2
case res of
(MkUnifyResult _ _ _ NoLazy) => pure True
_ => pure False)
(\err => pure False)
equivTypes ty1 ty2 =
do let False = isErased ty1
| _ => pure False
logTerm "typesearch.equiv" 10 "Candidate: " ty1
defs <- get Ctxt
True <- pure (!(getArity defs [] ty1) == !(getArity defs [] ty2))
| False => pure False
_ <- newRef UST initUState
b <- catch
(do res <- unify inTerm replFC [] ty1 ty2
case res of
(MkUnifyResult [] _ [] NoLazy) => pure True
_ => pure False)
(\err => pure False)
when b $ logTerm "typesearch.equiv" 20 "Accepted: " ty1
pure b
||| Process a single `REPLCmd`
|||
@ -807,23 +814,26 @@ process (Exec ctm)
= execExp ctm
process Help
= pure RequestedHelp
process (TypeSearch searchTerm@(PPi _ _ _ _ _ _))
process (TypeSearch searchTerm)
= do defs <- branch
let curr = currentNS defs
let ctxt = gamma defs
rawTy <- desugar AnyExpr [] searchTerm
let bound = piBindNames replFC [] rawTy
(ty, _) <- elabTerm 0 InType [] (MkNested []) [] bound Nothing
ty' <- toResolvedNames ty
filteredDefs <- do names <- allNames ctxt
defs <- catMaybes <$> (traverse (flip lookupCtxtExact ctxt) names)
allDefs <- traverse (resolved ctxt) defs
(flip filterM) allDefs (\def => equivTypes def.type ty')
filteredDefs <-
do names <- allNames ctxt
defs <- traverse (flip lookupCtxtExact ctxt) names
let defs = flip mapMaybe defs $ \ md =>
do d <- md
guard (visibleIn curr (fullname d) (visibility d))
pure d
allDefs <- traverse (resolved ctxt) defs
filterM (\def => equivTypes def.type ty') allDefs
put Ctxt defs
doc <- traverse (docsOrSignature replFC) $ (.fullname) <$> filteredDefs
pure $ Printed $ vsep $ pretty <$> (intersperse "\n" $ join doc)
process (TypeSearch _)
= pure $ REPLError $ reflow "Could not parse input as a type signature."
process (Missing n)
= do defs <- get Ctxt
case !(lookupCtxtName n (gamma defs)) of