From 87eeb200ced275e33e488f49033e920907294426 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Sat, 4 May 2019 19:19:22 +0100 Subject: [PATCH] Add searchNames Can now search for expressions by trying constructors --- src/Core/AutoSearch.idr | 95 ++++++++++++++++++++++++++++++++++++++++- src/Core/Context.idr | 47 ++++++++++++++------ 2 files changed, 128 insertions(+), 14 deletions(-) diff --git a/src/Core/AutoSearch.idr b/src/Core/AutoSearch.idr index bc45acf..1337eb4 100644 --- a/src/Core/AutoSearch.idr +++ b/src/Core/AutoSearch.idr @@ -86,6 +86,53 @@ searchIfHole fc defaults (S depth) def top env locs arg | _ => throw (CantSolveGoal fc env top) pure () +successful : {auto c : Ref Ctxt Defs} -> + {auto u : Ref UST UState} -> + List (Core (NF vars)) -> + Core (List (Either Error (NF vars, Defs, UState))) +successful [] = pure [] +successful (elab :: elabs) + = do ust <- get UST + defs <- branch + catch (do -- Run the elaborator + res <- elab + -- Record post-elaborator state + ust' <- get UST + defs' <- get Ctxt + -- Reset to previous state and try the rest + put UST ust + put Ctxt defs + elabs' <- successful elabs + -- Record success, and the state we ended at + pure (Right (res, defs', ust') :: elabs')) + (\err => do put UST ust + put Ctxt defs + elabs' <- successful elabs + pure (Left err :: elabs')) + +exactlyOne : {auto c : Ref Ctxt Defs} -> + {auto u : Ref UST UState} -> + FC -> Env Term vars -> (topTy : Term vars) -> + List (Core (NF vars)) -> + Core (NF vars) +exactlyOne fc env top [elab] + = catch elab + (\err => case err of + CantSolveGoal _ _ _ => throw err + _ => throw (CantSolveGoal fc env top)) +exactlyOne fc env top all + = do elabs <- successful all + case rights elabs of + [(res, defs, ust)] => + do put UST ust + put Ctxt defs + commit + pure res + [] => throw (CantSolveGoal fc env top) + rs => do defs <- get Ctxt + empty <- clearDefs defs + rs' <- traverse (Normalise.quote empty env) (map fst rs) + throw (AmbiguousSearch fc env rs') searchLocal : {auto c : Ref Ctxt Defs} -> {auto u : Ref UST UState} -> @@ -109,13 +156,57 @@ searchLocal fc rigc defaults depth def top env locs ((ty, c) :: rest) target nf defs env candidate) (searchLocal fc rigc defaults depth def top env locs rest target) +searchName : {auto c : Ref Ctxt Defs} -> + {auto u : Ref UST UState} -> + FC -> RigCount -> + (defaults : Bool) -> (depth : Nat) -> + (defining : Name) -> (topTy : Term vars) -> + Env Term vars -> SearchEnv vars -> (target : NF vars) -> + (Name, GlobalDef) -> + Core (NF vars) +searchName fc rigc defaults depth def top env locs target (n, ndef) + = do defs <- get Ctxt + let ty = type ndef + let namety : NameType + = case definition ndef of + DCon tag arity => DataCon tag arity + TCon tag arity _ _ _ _ => TyCon tag arity + _ => Func + nty <- nf defs env (embed ty) + (args, appTy) <- mkArgs fc rigc env nty + ures <- unify InTerm fc env target appTy + let [] = constraints ures + | _ => throw (CantSolveGoal fc env top) + let candidate = applyInfo fc (Ref fc namety n) + (map (\i => (appInf i, metaApp i)) args) + traverse (searchIfHole fc defaults depth def top env locs) args + defs <- get Ctxt + nf defs env candidate + searchNames : {auto c : Ref Ctxt Defs} -> {auto u : Ref UST UState} -> FC -> RigCount -> (defaults : Bool) -> (depth : Nat) -> (defining : Name) -> (topTy : Term vars) -> - Env Term vars -> List Name -> + Env Term vars -> SearchEnv vars -> List Name -> (target : NF vars) -> Core (NF vars) +searchNames fc rigc defaults depth defining topty env locs [] target + = throw (CantSolveGoal fc env topty) +searchNames fc rigc defaults depth defining topty env locs (n :: ns) target + = do defs <- get Ctxt + visnsm <- traverse (visible (gamma defs) (currentNS defs)) (n :: ns) + let visns = mapMaybe id visnsm + exactlyOne fc env topty + (map (searchName fc rigc defaults depth defining topty env locs target) visns) + where + visible : Context GlobalDef -> + List String -> Name -> Core (Maybe (Name, GlobalDef)) + visible gam nspace n + = do Just def <- lookupCtxtExact n gam + | Nothing => pure Nothing + if visibleIn nspace n (visibility def) + then pure $ Just (n, def) + else pure $ Nothing -- Declared at the top searchType fc rigc defaults depth def top env locs (NBind nfc x (Pi c p ty) sc) @@ -137,7 +228,7 @@ searchType {vars} fc rigc defaults depth def top env locs target@(NTCon tfc tyn tryGroups [] = throw (CantSolveGoal fc env top) tryGroups (g :: gs) = handleUnify - (searchNames fc rigc defaults depth def top env g target) + (searchNames fc rigc defaults depth def top env locs g target) (\err => if ambig err || isNil gs then throw err else tryGroups gs) diff --git a/src/Core/Context.idr b/src/Core/Context.idr index 6463435..c8f87ed 100644 --- a/src/Core/Context.idr +++ b/src/Core/Context.idr @@ -572,6 +572,16 @@ export lookupTyName : Name -> Context GlobalDef -> Core (List (Name, Int, ClosedTerm)) lookupTyName = lookupNameBy type +-- private names are only visible in this namespace if their namespace +-- is the current namespace (or an outer one) +-- that is: given that most recent namespace is first in the list, +-- the namespace of 'n' is a suffix of nspace +export +visibleIn : (nspace : List String) -> Name -> Visibility -> Bool +visibleIn nspace (NS ns n) Private = isSuffixOf ns nspace +-- Public and Export names are always visible +visibleIn nspace n _ = True + export setFlag : {auto c : Ref Ctxt Defs} -> FC -> Name -> DefFlag -> Core () @@ -688,8 +698,14 @@ setDetermining fc tyn args export addHintFor : {auto c : Ref Ctxt Defs} -> FC -> Name -> Name -> Bool -> Core () -addHintFor fc tyn hintn direct +addHintFor fc tyn hintn_in direct = do defs <- get Ctxt + let hintn : Name + = case hintn_in of + Resolved i => hintn_in + _ => case getNameID hintn_in (gamma defs) of + Nothing => hintn_in + Just idx => Resolved idx Just (TCon t a ps dets cons hs) <- lookupDefExact tyn (gamma defs) | _ => throw (GenericMsg fc (show tyn ++ " is not a type constructor")) updateDef tyn (const (Just (TCon t a ps dets cons ((hintn, direct) :: hs)))) @@ -697,15 +713,27 @@ addHintFor fc tyn hintn direct export addGlobalHint : {auto c : Ref Ctxt Defs} -> Name -> Bool -> Core () -addGlobalHint hint isdef - = do d <- get Ctxt - put Ctxt (record { autoHints $= insert hint isdef } d) +addGlobalHint hintn_in isdef + = do defs <- get Ctxt + let hintn : Name + = case hintn_in of + Resolved i => hintn_in + _ => case getNameID hintn_in (gamma defs) of + Nothing => hintn_in + Just idx => Resolved idx + put Ctxt (record { autoHints $= insert hintn isdef } defs) export addOpenHint : {auto c : Ref Ctxt Defs} -> Name -> Core () -addOpenHint hint - = do d <- get Ctxt - put Ctxt (record { openHints $= insert hint () } d) +addOpenHint hintn_in + = do defs <- get Ctxt + let hintn : Name + = case hintn_in of + Resolved i => hintn_in + _ => case getNameID hintn_in (gamma defs) of + Nothing => hintn_in + Just idx => Resolved idx + put Ctxt (record { openHints $= insert hintn () } defs) -- Set the default namespace for new definitions export @@ -816,11 +844,6 @@ toFullNames tm = do Just gdef <- lookupCtxtExact (Resolved i) gam | Nothing => pure (Ref fc x (Resolved i)) pure (Ref fc x (fullname gdef)) --- = do let a = content gam --- arr <- get Arr --- Just gdef <- coreLift (readArray arr i) --- | Nothing => pure (Ref fc x (Resolved i)) --- pure (Ref fc x (fullname gdef)) full gam (Meta fc x y xs) = pure (Meta fc x y !(traverse (full gam) xs)) full gam (Bind fc x b scope)