Add searchNames

Can now search for expressions by trying constructors

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)

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
+addGlobalHint hintn_in isdef
-    = do d <- get Ctxt
+    = do defs <- get Ctxt
-         put Ctxt (record { autoHints $= insert hint isdef } d)
+         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
+addOpenHint hintn_in
-    = do d <- get Ctxt
+    = do defs <- get Ctxt
-         put Ctxt (record { openHints $= insert hint () } d)
+         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)