Add local hints (basic version)

This gives us the ability to define and use implementations locally, in
where clauses/local let bindings, as well as flag local definitions as
hints.
It's not yet quite equivalent to global hints, however, since it translated
the hint to a local let binding, which doesn't reduce, so if something
relies on the reduction behaviour of the hint, it won't work. This
refinement is coming later

src/Core/Context.idr

@@ -936,6 +936,8 @@ record Defs where
   openHints : NameMap ()
      -- ^ currently open global hints; just for the rest of this module (not exported)
      -- and prioritised
+  localHints : NameMap ()
+     -- ^ Hints defined in the current environment
   saveTypeHints : List (Name, Name, Bool)
      -- We don't look up anything in here, it's merely for saving out to TTC.
      -- We save the hints in the 'GlobalDef' itself for faster lookup.
@@ -988,7 +990,7 @@ initDefs : Core Defs
 initDefs
     = do gam <- initCtxt
          pure (MkDefs gam [] mainNS [] defaults empty 100
-                      empty empty empty [] [] empty []
+                      empty empty empty empty [] [] empty []
                       empty 5381 [] [] [] [] [] empty empty empty empty [])
 
 -- Reset the context, except for the options
@@ -1658,6 +1660,14 @@ addGlobalHint hintn_in isdef
          put Ctxt (record { autoHints $= insert hintn isdef,
                             saveAutoHints $= ((hintn, isdef) ::) } defs)
 
+export
+addLocalHint : {auto c : Ref Ctxt Defs} ->
+               Name -> Core ()
+addLocalHint hintn_in
+    = do defs <- get Ctxt
+         hintn <- toResolvedNames hintn_in
+         put Ctxt (record { localHints $= insert hintn () } defs)
+
 export
 addOpenHint : {auto c : Ref Ctxt Defs} -> Name -> Core ()
 addOpenHint hintn_in

src/Core/Options/Log.idr

@@ -116,7 +116,7 @@ defaultLogLevel = singleton [] 0
 
 export
 insertLogLevel : LogLevel -> LogLevels -> LogLevels
-insertLogLevel (MkLogLevel ps n) = insert ps n
+insertLogLevel (MkLogLevel ps n) = insertWith ps (maybe n (max n))
 
 ----------------------------------------------------------------------------------
 -- CHECKING WHETHER TO LOG

src/Core/UnifyState.idr

@@ -479,7 +479,7 @@ newSearch {vars} fc rig depth def env n ty
     = do let hty = abstractEnvType fc env ty
          let hole = newDef fc n rig [] hty Public (BySearch rig depth def)
          log "unify.search" 10 $ "Adding new search " ++ show fc ++ " " ++ show n
-         logTermNF "unify.search" 10 "New search type" env ty
+         logTermNF "unify.search" 10 "New search type" [] hty
          idx <- addDef n hole
          addGuessName fc n idx
          pure (idx, Meta fc n idx envArgs)

src/Idris/Desugar.idr

@@ -721,7 +721,7 @@ mutual
       expandConstraint (Nothing, p)
           = map (\x => (Nothing, x)) (pairToCons p)
 
-  desugarDecl ps (PImplementation fc vis fnopts pass is cons tn params impname nusing body)
+  desugarDecl ps (PImplementation fc vis fnopts pass is cons tn params impln nusing body)
       = do opts <- traverse (desugarFnOpt ps) fnopts
            is' <- traverse (\ (n,c,tm) => do tm' <- desugar AnyExpr ps tm
                                              pure (n, c, tm')) is
@@ -747,11 +747,20 @@ mutual
            body' <- maybe (pure Nothing)
                           (\b => do b' <- traverse (desugarDecl ps) b
                                     pure (Just (concat b'))) body
-           pure [IPragma (maybe [] (\n => [n]) impname)
+           -- calculate the name of the interface, if it's not explicitly
+           -- given.
+           let impname = maybe (mkImplName fc tn paramsb) id impln
+
+           pure [IPragma [impname]
                          (\nest, env =>
                              elabImplementation fc vis opts pass env nest isb consb
-                                                tn paramsb impname nusing
+                                                tn paramsb (isNamed impln)
+                                                impname nusing
                                                 body')]
+    where
+      isNamed : Maybe a -> Bool
+      isNamed Nothing = False
+      isNamed (Just _) = True
 
   desugarDecl ps (PRecord fc doc vis tn params conname_in fields)
       = do addDocString tn doc

src/Idris/Elab/Implementation.idr

@@ -34,8 +34,9 @@ replaceSep = pack . map toForward . unpack
     toForward '\\' = '/'
     toForward x = x
 
-mkImpl : FC -> Name -> List RawImp -> Name
-mkImpl fc n ps
+export
+mkImplName : FC -> Name -> List RawImp -> Name
+mkImplName fc n ps
     = DN (show n ++ " implementation at " ++ replaceSep (show fc))
          (UN ("__Impl_" ++ show n ++ "_" ++
           showSep "_" (map show ps)))
@@ -110,13 +111,14 @@ elabImplementation : {vars : _} ->
                      (constraints : List (Maybe Name, RawImp)) ->
                      Name ->
                      (ps : List RawImp) ->
-                     (implName : Maybe Name) ->
+                     (namedimpl : Bool) ->
+                     (implName : Name) ->
                      (nusing : List Name) ->
                      Maybe (List ImpDecl) ->
                      Core ()
 -- TODO: Refactor all these steps into separate functions
-elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nusing mbody
-    = do let impName_in = maybe (mkImpl fc iname ps) id impln
+elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps named impName_in nusing mbody
+    = do -- let impName_in = maybe (mkImplName fc iname ps) id impln
          -- If we're in a nested block, update the name
          let impName_nest = case lookup impName_in (names nest) of
                                  Just (Just n', _) => n'
@@ -157,8 +159,9 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
          -- given when using named implementations
          --    (cs : Constraints) -> Impl params
          -- Don't make it a hint if it's a named implementation
-         let opts = maybe ([Inline, Hint True])
-                          (const ([Inline])) impln
+         let opts = if named
+                       then [Inline]
+                       else [Inline, Hint True]
 
          let initTy = bindImpls fc is $ bindConstraints fc AutoImplicit cons
                          (apply (IVar fc iname) ps)
@@ -223,7 +226,9 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
 
                -- If it's a named implementation, add it as a global hint while
                -- elaborating the record and bodies
-               maybe (pure ()) (\x => addOpenHint impName) impln
+               if named
+                  then addOpenHint impName
+                  else pure ()
 
                -- Make sure we don't use this name to solve parent constraints
                -- when elaborating the record, or we'll end up in a cycle!
@@ -334,7 +339,7 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
     methName n
         = DN (show n)
              (UN (show n ++ "_" ++ show iname ++ "_" ++
-                     maybe "" show impln ++ "_" ++
+                     (if named then show impName_in else "") ++
                      showSep "_" (map show ps)))
 
     applyCon : Name -> Name -> Core (Name, RawImp)

src/TTImp/Elab/App.idr

@@ -198,7 +198,7 @@ mutual
                    est <- get EST
                    lim <- getAutoImplicitLimit
                    metaval <- searchVar fc argRig lim (Resolved (defining est))
-                                        env nm metaty
+                                        env nest nm metaty
                    let fntm = App fc tm metaval
                    fnty <- sc defs (toClosure defaultOpts env metaval)
                    checkAppWith rig elabinfo nest env fc

src/TTImp/Elab/Check.idr

@@ -407,10 +407,60 @@ searchVar : {vars : _} ->
             {auto c : Ref Ctxt Defs} ->
             {auto u : Ref UST UState} ->
             FC -> RigCount -> Nat -> Name ->
-            Env Term vars -> Name -> Term vars -> Core (Term vars)
-searchVar fc rig depth def env n ty
-    = do (_, tm) <- newSearch fc rig depth def env n ty
-         pure tm
+            Env Term vars -> NestedNames vars -> Name -> Term vars -> Core (Term vars)
+searchVar fc rig depth def env nest n ty
+    = do defs <- get Ctxt
+         (vars' ** (bind, env')) <- envHints (keys (localHints defs)) env
+         -- Initial the search with an environment which binds the applied
+         -- local hints
+         (_, tm) <- newSearch fc rig depth def env' n
+                              (weakenNs (mkSizeOf vars') ty)
+         pure (bind tm)
+  where
+    useVars : {vars : _} ->
+              List (Term vars) -> Term vars -> Term vars
+    useVars [] sc = sc
+    useVars (a :: as) (Bind bfc n (Pi fc c _ ty) sc)
+         = Bind bfc n (Let fc c a ty) (useVars (map weaken as) sc)
+    useVars as (Bind bfc n (Let fc c v ty) sc)
+         = Bind bfc n (Let fc c v ty) (useVars (map weaken as) sc)
+    useVars _ sc = sc -- Can't happen?
+
+    find : Name -> List (Name, (Maybe Name, b)) -> Maybe (Maybe Name, b)
+    find x [] = Nothing
+    find x ((n, t) :: xs)
+       = if x == n
+            then Just t
+            else case t of
+                      (Nothing, _) => find x xs
+                      (Just n', _) => if x == n'
+                                         then Just t
+                                         else find x xs
+
+    envHints : List Name -> Env Term vars ->
+               Core (vars' ** (Term (vars' ++ vars) -> Term vars, Env Term (vars' ++ vars)))
+    envHints [] env = pure ([] ** (id, env))
+    envHints (n :: ns) env
+        = do (vs ** (f, env')) <- envHints ns env
+             let Just (nestn, argns, tmf) = find !(toFullNames n) (names nest)
+                 | Nothing => pure (vs ** (f, env'))
+             let n' = maybe n id nestn
+             defs <- get Ctxt
+             Just ndef <- lookupCtxtExact n' (gamma defs)
+                 | Nothing => pure (vs ** (f, env'))
+             let nt = case definition ndef of
+                           PMDef _ _ _ _ _ => Func
+                           DCon t a _ => DataCon t a
+                           TCon t a _ _ _ _ _ _ => TyCon t a
+                           _ => Func
+             let app = tmf fc nt
+             let tyenv = useVars (getArgs app) (embed (type ndef))
+             let binder = Let fc top (weakenNs (mkSizeOf vs) app)
+                                     (weakenNs (mkSizeOf vs) tyenv)
+             varn <- toFullNames n'
+             pure ((varn :: vs) **
+                    (\t => f (Bind fc varn binder t),
+                       binder :: env'))
 
 -- Elaboration info (passed to recursive calls)
 public export

src/TTImp/Elab/Local.idr

@@ -15,6 +15,7 @@ import TTImp.Elab.Check
 import TTImp.Elab.Utils
 import TTImp.TTImp
 
+import Data.NameMap
 import Data.List
 
 %default covering
@@ -55,10 +56,18 @@ checkLocal {vars} rig elabinfo nest env fc nestdecls_in scope expty
          ust <- get UST
          let olddelayed = delayedElab ust
          put UST (record { delayedElab = [] } ust)
+         defs <- get Ctxt
+         -- store the local hints, so we can reset them after we've elaborated
+         -- everything
+         let oldhints = localHints defs
          traverse (processDecl [] nest' env') (map (updateName nest') nestdecls)
          ust <- get UST
          put UST (record { delayedElab = olddelayed } ust)
-         check rig elabinfo nest' env scope expty
+         defs <- get Ctxt
+         res <- check rig elabinfo nest' env scope expty
+         defs <- get Ctxt
+         put Ctxt (record { localHints = oldhints } defs)
+         pure res
   where
     -- For the local definitions, don't allow access to linear things
     -- unless they're explicitly passed.

src/TTImp/Elab/Term.idr

@@ -164,14 +164,14 @@ checkTerm rig elabinfo nest env (ISearch fc depth) (Just gexpty)
     = do est <- get EST
          nm <- genName "search"
          expty <- getTerm gexpty
-         sval <- searchVar fc rig depth (Resolved (defining est)) env nm expty
+         sval <- searchVar fc rig depth (Resolved (defining est)) env nest nm expty
          pure (sval, gexpty)
 checkTerm rig elabinfo nest env (ISearch fc depth) Nothing
     = do est <- get EST
          nmty <- genName "searchTy"
          ty <- metaVar fc erased env nmty (TType fc)
          nm <- genName "search"
-         sval <- searchVar fc rig depth (Resolved (defining est)) env nm ty
+         sval <- searchVar fc rig depth (Resolved (defining est)) env nest nm ty
          pure (sval, gnf env ty)
 checkTerm rig elabinfo nest env (IAlternative fc uniq alts) exp
     = checkAlternative rig elabinfo nest env fc uniq alts exp

src/TTImp/ProcessType.idr

@@ -32,30 +32,35 @@ getRetTy defs ty
              "Can only add hints for concrete return types")
 
 processFnOpt : {auto c : Ref Ctxt Defs} ->
-               FC -> Name -> FnOpt -> Core ()
-processFnOpt fc ndef Inline
+               FC -> Nat -> Name -> FnOpt -> Core ()
+processFnOpt fc _ ndef Inline
     = setFlag fc ndef Inline
-processFnOpt fc ndef TCInline
+processFnOpt fc _ ndef TCInline
     = setFlag fc ndef TCInline
-processFnOpt fc ndef (Hint d)
+processFnOpt fc Z ndef (Hint d)
     = do defs <- get Ctxt
          Just ty <- lookupTyExact ndef (gamma defs)
               | Nothing => throw (UndefinedName fc ndef)
          target <- getRetTy defs !(nf defs [] ty)
          addHintFor fc target ndef d False
-processFnOpt fc ndef (GlobalHint a)
+processFnOpt fc _ ndef (Hint d)
+    = do log "elab" 5 $ "Adding local hint " ++ show !(toFullNames ndef)
+         addLocalHint ndef
+processFnOpt fc Z ndef (GlobalHint a)
     = addGlobalHint ndef a
-processFnOpt fc ndef ExternFn
+processFnOpt fc _ ndef (GlobalHint a)
+    = throw (GenericMsg fc "%globalhint is not valid in local definitions")
+processFnOpt fc _ ndef ExternFn
     = setFlag fc ndef Inline -- if externally defined, inline when compiling
-processFnOpt fc ndef (ForeignFn _)
+processFnOpt fc _ ndef (ForeignFn _)
     = setFlag fc ndef Inline -- if externally defined, inline when compiling
-processFnOpt fc ndef Invertible
+processFnOpt fc _ ndef Invertible
     = setFlag fc ndef Invertible
-processFnOpt fc ndef (Totality tot)
+processFnOpt fc _ ndef (Totality tot)
     = setFlag fc ndef (SetTotal tot)
-processFnOpt fc ndef Macro
+processFnOpt fc _ ndef Macro
     = setFlag fc ndef Macro
-processFnOpt fc ndef (SpecArgs ns)
+processFnOpt fc _ ndef (SpecArgs ns)
     = do defs <- get Ctxt
          Just gdef <- lookupCtxtExact ndef (gamma defs)
               | Nothing => throw (UndefinedName fc ndef)
@@ -296,7 +301,7 @@ processType {vars} eopts nest env fc rig vis opts (MkImpTy tfc n_in ty_raw)
 
          log "declare.type" 2 $ "Setting options for " ++ show n ++ ": " ++ show opts
          let name = Resolved idx
-         traverse (processFnOpt fc name) opts
+         traverse (processFnOpt fc (length env) name) opts
          -- If no function-specific totality pragma has been used, attach the default totality
          unless (any isTotalityReq opts) $
            setFlag fc name (SetTotal !getDefaultTotalityOption)

tests/idris2/interface018/LocalInterface.idr

@@ -0,0 +1,9 @@
+interface Add a where
+  add : a -> a
+
+testAdd : Nat -> Nat -> Nat
+testAdd x y = add x
+  where
+    Add Nat where
+      add Z = y
+      add (S k) = add k

tests/idris2/interface018/expected

@@ -0,0 +1 @@
+1/1: Building LocalInterface (LocalInterface.idr)

tests/idris2/interface018/run

@@ -0,0 +1,3 @@
+$1 --no-color --console-width 0 LocalInterface.idr --check
+
+rm -rf build

tests/idris2/interface019/LocalHints.idr

@@ -0,0 +1,48 @@
+data Foo : Type where [noHints]
+  A : Foo
+  B : Foo
+  
+findA : {auto foo : Foo} -> String
+findA {foo = A} = "Found an A"
+findA {foo = _} = "Failed to find an A"
+
+Baz : String -> Type
+Baz s = s = "Found an A" 
+
+baz : (s : String ** Baz s)
+baz = let %hint arg : Foo
+          arg = A
+      in (findA ** Refl)
+
+interface Gnu where
+  constructor MkGnu
+  hasFoo : Foo
+  
+findB : Gnu => String
+findB = case hasFoo of
+  B => "Found a B"
+  _ => "Failed to find a B"
+
+Bar : String -> Type
+Bar s = s = "Found a B" 
+
+bar : (s : String ** Bar s)
+bar = let %hint arg : Gnu
+          arg = MkGnu B
+      in (findB ** Refl)
+
+interface Gnat a where
+  constructor MkGnat
+  makeFoo : a -> Foo
+
+record More where
+  constructor MkMore
+  0 Ty : Type
+
+%unbound_implicits off
+bug : forall a . a -> (s : String ** Bar s)
+bug {a} x = let M : More
+                M = MkMore a
+                %hint arg : Gnat (Ty M)
+                arg = MkGnat (const B)
+            in (findB ** Refl)

tests/idris2/interface019/expected

@@ -0,0 +1 @@
+1/1: Building LocalHints (LocalHints.idr)

tests/idris2/interface019/run

@@ -0,0 +1,3 @@
+$1 --no-color --console-width 0 LocalHints.idr --check
+
+rm -rf build