Merge pull request #1597 from edwinb/expr-search

A couple of expression search improvements

src/Core/Context.idr

@@ -24,6 +24,7 @@ import Libraries.Data.StringMap
 import Libraries.Text.Distance.Levenshtein
 
 import System
+import System.Clock
 import System.Directory
 
 %default covering
@@ -1114,6 +1115,9 @@ record Defs where
      -- again
   timings : StringMap (Bool, Integer)
      -- ^ record of timings from logTimeRecord
+  timer : Maybe (Integer, String)
+     -- ^ for timing and checking timeouts; the maximum time after which a
+     -- timeout should be thrown
   warnings : List Warning
      -- ^ as yet unreported warnings
 
@@ -1159,6 +1163,7 @@ initDefs
            , userHoles = empty
            , peFailures = empty
            , timings = empty
+           , timer = Nothing
            , warnings = []
            }
 
@@ -2351,6 +2356,13 @@ setNFThreshold max
     = do defs <- get Ctxt
          put Ctxt (record { options->elabDirectives->nfThreshold = max } defs)
 
+export
+setSearchTimeout : {auto c : Ref Ctxt Defs} ->
+                   Integer -> Core ()
+setSearchTimeout t
+    = do defs <- get Ctxt
+         put Ctxt (record { options->session->searchTimeout = t } defs)
+
 export
 isLazyActive : {auto c : Ref Ctxt Defs} ->
                Core Bool
@@ -2582,3 +2594,48 @@ recordWarning w
     = do defs <- get Ctxt
          session <- getSession
          put Ctxt $ record { warnings $= (w ::) } defs
+
+export
+getTime : Core Integer
+getTime
+    = do clock <- coreLift (clockTime Process)
+         pure (seconds clock * nano + nanoseconds clock)
+  where
+    nano : Integer
+    nano = 1000000000
+
+-- A simple timeout mechanism. We can start a timer, clear it, or check
+-- whether too much time has passed and throw an exception if so
+
+||| Initialise the timer, setting the time in milliseconds after which a
+||| timeout should be thrown.
+||| Note: It's important to clear the timer when the operation that might
+||| timeout is complete, otherwise something else might throw a timeout
+||| error!
+export
+startTimer : {auto c : Ref Ctxt Defs} ->
+             Integer -> String -> Core ()
+startTimer tmax action
+    = do t <- getTime
+         defs <- get Ctxt
+         put Ctxt $ record { timer = Just (t + tmax * 1000000, action) } defs
+
+||| Clear the timer
+export
+clearTimer : {auto c : Ref Ctxt Defs} -> Core ()
+clearTimer
+    = do defs <- get Ctxt
+         put Ctxt $ record { timer = Nothing } defs
+
+||| If the timer was started more than t milliseconds ago, throw an exception
+export
+checkTimer : {auto c : Ref Ctxt Defs} ->
+             Core ()
+checkTimer
+    = do defs <- get Ctxt
+         let Just (max, action) = timer defs
+                | Nothing => pure ()
+         t <- getTime
+         if (t > max)
+            then throw (Timeout action)
+            else pure ()

src/Core/Core.idr

@@ -157,6 +157,7 @@ data Error : Type where
      ||| Contains list of specifiers for which foreign call cannot be resolved
      NoForeignCC : FC -> List String -> Error
      BadMultiline : FC -> String -> Error
+     Timeout : String -> Error
 
      InType : FC -> Name -> Error -> Error
      InCon : FC -> Name -> Error -> Error
@@ -332,6 +333,7 @@ Show Error where
   show (NoForeignCC fc specs) = show fc ++
        ":The given specifier " ++ show specs ++ " was not accepted by any available backend."
   show (BadMultiline fc str) = "Invalid multiline string: " ++ str
+  show (Timeout str) = "Timeout in " ++ str
 
   show (InType fc n err)
        = show fc ++ ":When elaborating type of " ++ show n ++ ":\n" ++
@@ -423,6 +425,7 @@ getErrorLoc (InternalError _) = Nothing
 getErrorLoc (UserError _) = Nothing
 getErrorLoc (NoForeignCC loc _) = Just loc
 getErrorLoc (BadMultiline loc _) = Just loc
+getErrorLoc (Timeout _) = Nothing
 getErrorLoc (InType _ _ err) = getErrorLoc err
 getErrorLoc (InCon _ _ err) = getErrorLoc err
 getErrorLoc (InLHS _ _ err) = getErrorLoc err

src/Core/Normalise.idr

@@ -291,6 +291,9 @@ parameters (defs : Defs, topopts : EvalOpts)
              -- want to shortcut that second check, if we're evaluating
              -- everything, so don't let bind unless we need that log!
              let redok = redok1 || redok2
+             checkTimer -- If we're going to time out anywhere, it'll be
+                        -- when evaluating something recursive, so this is a
+                        -- good place to check
              unless redok2 $ logC "eval.stuck" 5 $ do n' <- toFullNames n
                                                       pure $ "Stuck function: " ++ show n'
              if redok

src/Core/Options.idr

@@ -157,6 +157,8 @@ record Session where
   dumpanf : Maybe String -- file to output ANF definitions
   dumpvmcode : Maybe String -- file to output VM code definitions
   profile : Bool -- generate profiling information, if supported
+  searchTimeout : Integer -- maximum number of milliseconds to run
+                          -- expression/program search
   -- Warnings
   warningsAsErrors : Bool
   showShadowingWarning : Bool
@@ -210,7 +212,7 @@ export
 defaultSession : Session
 defaultSession = MkSessionOpts False False False Chez [] False defaultLogLevel
                                False False False Nothing Nothing
-                               Nothing Nothing False False True False
+                               Nothing Nothing False 1000 False True False
 
 export
 defaultElab : ElabDirectives

src/Idris/Desugar.idr

@@ -1010,6 +1010,7 @@ mutual
              AmbigDepth n => pure [IPragma [] (\nest, env => setAmbigLimit n)]
              AutoImplicitDepth n => pure [IPragma [] (\nest, env => setAutoImplicitLimit n)]
              NFMetavarThreshold n => pure [IPragma [] (\nest, env => setNFThreshold n)]
+             SearchTimeout n => pure [IPragma [] (\nest, env => setSearchTimeout n)]
              PairNames ty f s => pure [IPragma [] (\nest, env => setPair fc ty f s)]
              RewriteName eq rw => pure [IPragma [] (\nest, env => setRewrite fc eq rw)]
              PrimInteger n => pure [IPragma [] (\nest, env => setFromInteger n)]

src/Idris/Error.idr

@@ -467,6 +467,7 @@ perror (NoForeignCC fc specs) = do
                    ] <+> line <+> !(ploc fc)
     pure res
 perror (BadMultiline fc str) = pure $ errorDesc (reflow "While processing multi-line string" <+> dot <++> pretty str <+> dot) <+> line <+> !(ploc fc)
+perror (Timeout str) = pure $ errorDesc (reflow "Timeout in" <++> pretty str)
 
 perror (InType fc n err)
     = pure $ hsep [ errorDesc (reflow "While processing type of" <++> code (pretty !(prettyName n))) <+> dot

src/Idris/Parser.idr

@@ -1166,6 +1166,10 @@ directive fname indents
          dpt <- decorate fname Keyword $ intLit
          atEnd indents
          pure (NFMetavarThreshold (fromInteger dpt))
+  <|> do decorate fname Keyword $ pragma "search_timeout"
+         t <- decorate fname Keyword $ intLit
+         atEnd indents
+         pure (SearchTimeout t)
   <|> do decorate fname Keyword $ pragma "pair"
          ty <- name
          f <- name

src/Idris/REPL.idr

@@ -451,7 +451,7 @@ processEdit (ExprSearch upd line name hints)
                   case holeInfo pi of
                        NotHole => pure $ EditError "Not a searchable hole"
                        SolvedHole locs =>
-                          do let (_ ** (env, tm')) = dropLamsTm locs [] tm
+                          do let (_ ** (env, tm')) = dropLamsTm locs [] !(normaliseHoles defs [] tm)
                              itm <- resugar env tm'
                              let itm' : PTerm = if brack then addBracket replFC itm else itm
                              if upd

src/Idris/Syntax.idr

@@ -267,6 +267,7 @@ mutual
        PrefixRecordProjections : Bool -> Directive
        AutoImplicitDepth : Nat -> Directive
        NFMetavarThreshold : Nat -> Directive
+       SearchTimeout : Integer -> Directive
 
   public export
   data PField : Type where

src/TTImp/Interactive/ExprSearch.idr

@@ -18,6 +18,7 @@ import Core.Env
 import Core.LinearCheck
 import Core.Metadata
 import Core.Normalise
+import Core.Options
 import Core.Unify
 import Core.TT
 import Core.Value
@@ -91,11 +92,14 @@ searchN : {auto c : Ref Ctxt Defs} ->
           {auto u : Ref UST UState} ->
           Nat -> Core (Search a) -> Core (List a, Core (Search a))
 searchN max s
-    = tryUnify
+    = do startTimer (searchTimeout !getSession) "expression search"
+         tryUnify
            (do res <- s
                xs <- count max res
+               clearTimer
                pure xs)
-         (pure ([], pure NoMore))
+           (do clearTimer
+               pure ([], pure NoMore))
   where
     count : Nat -> Search a -> Core (List a, Core (Search a))
     count k NoMore = pure ([], pure NoMore)
@@ -235,7 +239,12 @@ firstSuccess (elab :: elabs)
          catch (do Result res more <- elab
                       | NoMore => continue ust defs elabs
                    pure (Result res (continue ust defs (more :: elabs))))
-               (\err => continue ust defs elabs)
+               (\err =>
+                    case err of
+                         -- Give up on timeout, or we'll keep trying all the
+                         -- other branches.
+                         Timeout _ => noResult
+                         _ => continue ust defs elabs)
   where
     continue : UState -> Defs -> List (Core (Search a)) ->
                Core (Search a)
@@ -301,6 +310,7 @@ searchName : {vars : _} ->
              Core (Search (Term vars, ExprDefs))
 searchName fc rigc opts env target topty (n, ndef)
     = do defs <- get Ctxt
+         checkTimer
          let True = visibleInAny (!getNS :: !getNestedNS)
                                  (fullname ndef) (visibility ndef)
              | _ => noResult
@@ -371,6 +381,7 @@ searchNames fc rig opts env ty topty []
     = noResult
 searchNames fc rig opts env ty topty (n :: ns)
     = do defs <- get Ctxt
+         checkTimer
          vis <- traverse (visible (gamma defs) (currentNS defs :: nestedNS defs)) (n :: ns)
          let visns = mapMaybe id vis
          nfty <- nf defs env ty
@@ -470,6 +481,7 @@ searchLocalWith fc nofn rig opts env [] ty topty
     = noResult
 searchLocalWith {vars} fc nofn rig opts env ((p, pty) :: rest) ty topty
     = do defs <- get Ctxt
+         checkTimer
          nty <- nf defs env ty
          getSuccessful fc rig opts False env ty topty
                        [findPos defs p id !(nf defs env pty) nty,
@@ -792,6 +804,7 @@ searchHole : {auto c : Ref Ctxt Defs} ->
 searchHole fc rig opts n locs topty defs glob
     = do searchty <- normalise defs [] (type glob)
          logTerm "interaction.search" 10 "Normalised type" searchty
+         checkTimer
          searchType fc rig opts [] topty locs searchty
 
 -- Declared at the top
@@ -864,6 +877,13 @@ exprSearchOpts opts fc n_in hints
     = do defs <- get Ctxt
          Just (n, idx, gdef) <- lookupHoleName n_in defs
              | Nothing => undefinedName fc n_in
+         -- the REPL does this step, but doing it here too because
+         -- expression search might be invoked some other way
+         let Hole _ _ = definition gdef
+             | PMDef pi [] (STerm _ tm) _ _
+                 => do raw <- unelab [] !(toFullNames !(normaliseHoles defs [] tm))
+                       one raw
+             | _ => throw (GenericMsg fc "Name is already defined")
          lhs <- findHoleLHS !(getFullName (Resolved idx))
          log "interaction.search" 10 $ "LHS hole data " ++ show (n, lhs)
          opts' <- if getRecData opts
@@ -881,13 +901,24 @@ exprSearchOpts opts fc n_in hints
                                [res] => pure $ Just res
                                _ => pure Nothing
 
+exprSearch' : {auto c : Ref Ctxt Defs} ->
+              {auto m : Ref MD Metadata} ->
+              {auto u : Ref UST UState} ->
+              FC -> Name -> List Name ->
+              Core (Search RawImp)
+exprSearch' = exprSearchOpts (initSearchOpts True 5)
+
 export
 exprSearch : {auto c : Ref Ctxt Defs} ->
              {auto m : Ref MD Metadata} ->
              {auto u : Ref UST UState} ->
              FC -> Name -> List Name ->
              Core (Search RawImp)
-exprSearch = exprSearchOpts (initSearchOpts True 5)
+exprSearch fc n hints
+    = do startTimer (searchTimeout !getSession) "expression search"
+         res <- exprSearch' fc n hints
+         clearTimer
+         pure res
 
 export
 exprSearchN : {auto c : Ref Ctxt Defs} ->

tests/Main.idr

@@ -79,7 +79,7 @@ idrisTestsInteractive = MkTestPool "Interactive editing" [] Nothing
        "interactive021", "interactive022", "interactive023", "interactive024",
        "interactive025", "interactive026", "interactive027", "interactive028",
        "interactive029", "interactive030", "interactive031", "interactive032",
-       "interactive033"]
+       "interactive033", "interactive034", "interactive035"]
 
 idrisTestsInterface : TestPool
 idrisTestsInterface = MkTestPool "Interface" [] Nothing

tests/idris2/interactive034/expected

@@ -0,0 +1,3 @@
+1/1: Building timeout (timeout.idr)
+Main> tailIsNotSound contra (ConsIsSound headIsSound tailIsSound) = contra tailIsSound
+Main> Bye for now!

tests/idris2/interactive034/input

@@ -0,0 +1,2 @@
+:gd 54 tailIsNotSound
+:q

tests/idris2/interactive034/run

@@ -0,0 +1,3 @@
+$1 --no-color --console-width 0 --no-banner timeout.idr < input
+
+rm -rf build

tests/idris2/interactive034/timeout.idr

@@ -0,0 +1,56 @@
+import Data.List
+import Data.List.Elem
+
+%search_timeout 1000
+
+||| A Place has an ID and a number of tokens
+data Place : Type where
+  MkPlace : (i : Nat) -> (nTokens : Nat) -> Place
+
+||| A transition has a name
+data Transition : Type where
+  MkTransition : String -> Transition
+
+||| An Input links a Place and a Transition...
+data Input : Type where
+  MkInput : (from : Place) -> (to : Transition) -> Input
+
+-- Accessor functions for proof
+0 inputFrom : Input -> Place
+inputFrom (MkInput p t) = p
+
+0 inputTo : Input -> Transition
+inputTo (MkInput p t) = t
+
+data SoundInputFrom : Input -> List Place -> Type where
+  MkSoundInputFrom : (i : Input)
+                     -> (ps : List Place)
+                     -> (prf : Elem (inputFrom i) ps)
+                     -> SoundInputFrom i ps
+
+data SoundInputTo : Input -> List Transition -> Type where
+  MkSoundInputTo : (i : Input)
+                   -> (ts : List Transition)
+                   -> (prf : Elem (inputTo i) ts)
+                   -> SoundInputTo i ts
+
+data SoundInput : Input -> List Place -> List Transition -> Type where
+  MkSoundInput : (i : Input)
+                 -> (ps : List Place)
+                 -> (ts : List Transition)
+                 -> (fromOK : SoundInputFrom i ps)
+                 -> (toOK   : SoundInputTo   i ts)
+                 -> SoundInput i ps ts
+
+data AllInputsSound : List Input -> List Place -> List Transition -> Type where
+  NilInputsIsSound : AllInputsSound [] _ _
+  ConsIsSound : (headIsSound : SoundInput i ps ts)
+                -> (tailIsSound : AllInputsSound is ps ts)
+                -> AllInputsSound (i :: is) ps ts
+
+-- Searching here finds the right answer immediately, but then if we don't
+-- have a timeout, it takes ages to explore more non-solutions! So we cut off
+-- after a second
+tailIsNotSound : (contra : (AllInputsSound is ps ts -> Void))
+                 -> AllInputsSound (i :: is) ps ts
+                 -> Void

tests/idris2/interactive035/expected

@@ -0,0 +1,3 @@
+1/1: Building unify (unify.idr)
+Main> 4
+Main> Bye for now!

tests/idris2/interactive035/input

@@ -0,0 +1,2 @@
+:ps 7 vlength
+:q

tests/idris2/interactive035/run

@@ -0,0 +1,3 @@
+$1 --no-color --console-width 0 --no-banner unify.idr < input
+
+rm -rf build

tests/idris2/interactive035/unify.idr

@@ -0,0 +1,7 @@
+import Data.Vect
+
+data VectN : Type -> Type where
+     MkVectN : (n : Nat) -> Vect n a -> VectN a
+
+doSearch : Nat -> VectN Int
+doSearch n = MkVectN ?vlength [1,2,3,4]