Merge pull request #521 from edwinb/search-unpacking

Look at intermediate results in program search

CHANGELOG.md

@@ -58,7 +58,7 @@ exposes the function `mainWithCodegens` that takes a list of codegens. The
 feature in documented [here](https://idris2.readthedocs.io/en/latest/backends/custom.html).
 * New code generators `node` and `javascript`.
 
-REPL changes:
+REPL/IDE mode changes:
 
 * Implemented `:module` command, to load a module during a REPL session.
 * Implemented `:doc`, which displays documentation for a name.
@@ -71,6 +71,8 @@ REPL changes:
   next type correct implementation
   + Correspondingly, added the IDE mode command `generate-def-next` (which takes
     no arguments)
+* Improved program search to allow deconstructing intermediate values, and in
+  simple cases, the result of recursive calls.
 
 Changes since Idris 2 v0.1.0
 ----------------------------

src/Idris/REPL.idr

@@ -296,7 +296,7 @@ addMadeCase lit wapp line content
 nextProofSearch : {auto c : Ref Ctxt Defs} ->
                   {auto u : Ref UST UState} ->
                   {auto o : Ref ROpts REPLOpts} ->
-                  Core (Maybe (Name, ClosedTerm))
+                  Core (Maybe (Name, RawImp))
 nextProofSearch
     = do opts <- get ROpts
          let Just (n, res) = psResult opts
@@ -326,12 +326,17 @@ nextGenDef reject
               Z => pure (Just (line, res))
               S k => nextGenDef k
 
-dropLams : {vars : _} ->
-           Nat -> Env Term vars -> Term vars ->
-           (vars' ** (Env Term vars', Term vars'))
-dropLams Z env tm = (_ ** (env, tm))
-dropLams (S k) env (Bind _ _ b sc) = dropLams k (b :: env) sc
-dropLams _ env tm = (_ ** (env, tm))
+dropLams : Nat -> RawImp -> RawImp
+dropLams Z tm = tm
+dropLams (S k) (ILam _ _ _ _ _ sc) = dropLams k sc
+dropLams _ tm = tm
+
+dropLamsTm : {vars : _} ->
+             Nat -> Env Term vars -> Term vars ->
+             (vars' ** (Env Term vars', Term vars'))
+dropLamsTm Z env tm = (_ ** (env, tm))
+dropLamsTm (S k) env (Bind _ _ b sc) = dropLamsTm k (b :: env) sc
+dropLamsTm _ env tm = (_ ** (env, tm))
 
 processEdit : {auto c : Ref Ctxt Defs} ->
               {auto u : Ref UST UState} ->
@@ -380,11 +385,10 @@ processEdit (ExprSearch upd line name hints)
                      ropts <- get ROpts
                      put ROpts (record { psResult = Just (name, searchtm) } ropts)
                      defs <- get Ctxt
-                     Just (_, tm) <- nextProofSearch
+                     Just (_, restm) <- nextProofSearch
                           | Nothing => pure $ EditError "No search results"
-                     restm <- normaliseHoles defs [] tm
-                     let (_ ** (env, tm')) = dropLams locs [] restm
-                     itm <- resugar env tm'
+                     let tm' = dropLams locs restm
+                     itm <- pterm tm'
                      let res = show (the PTerm (if brack
                                                    then addBracket replFC itm
                                                    else itm))
@@ -395,7 +399,7 @@ processEdit (ExprSearch upd line name hints)
                   case holeInfo pi of
                        NotHole => pure $ EditError "Not a searchable hole"
                        SolvedHole locs =>
-                          do let (_ ** (env, tm')) = dropLams locs [] tm
+                          do let (_ ** (env, tm')) = dropLamsTm locs [] tm
                              itm <- resugar env tm'
                              let res = show (the PTerm (if brack
                                                 then addBracket replFC itm
@@ -408,14 +412,13 @@ processEdit (ExprSearch upd line name hints)
 processEdit ExprSearchNext
     = do defs <- get Ctxt
          syn <- get Syn
-         Just (name, tm) <- nextProofSearch
+         Just (name, restm) <- nextProofSearch
               | Nothing => pure $ EditError "No more results"
          [(n, nidx, Hole locs _)] <- lookupDefName name (gamma defs)
               | _ => pure $ EditError "Not a searchable hole"
          let brack = elemBy (\x, y => dropNS x == dropNS y) name (bracketholes syn)
-         restm <- normaliseHoles defs [] tm
-         let (_ ** (env, tm')) = dropLams locs [] restm
-         itm <- resugar env tm'
+         let tm' = dropLams locs restm
+         itm <- pterm tm'
          let res = show (the PTerm (if brack
                                        then addBracket replFC itm
                                        else itm))

src/Idris/REPLOpts.idr

@@ -29,7 +29,7 @@ record REPLOpts where
   errorLine : Maybe Int
   idemode : OutputMode
   currentElabSource : String
-  psResult : Maybe (Name, Core (Search ClosedTerm)) -- last proof search continuation (and name)
+  psResult : Maybe (Name, Core (Search RawImp)) -- last proof search continuation (and name)
   gdResult : Maybe (Int, Core (Search (FC, List ImpClause))) -- last generate def continuation (and line number)
   -- TODO: Move extraCodegens from here, it doesn't belong, but there's nowhere
   -- better to stick it now.

src/Idris/Resugar.idr

@@ -200,7 +200,7 @@ mutual
            imp <- showImplicits
            arg' <- if imp then toPTerm tyPrec arg
                           else pure (PImplicit fc)
-           sc' <- toPTerm p sc
+           sc' <- toPTerm startPrec sc
            pt' <- traverse (toPTerm argPrec) pt
            bracket p startPrec (PLam fc rig pt' (PRef fc n) arg' sc')
   toPTerm p (ILet fc rig n ty val sc)
@@ -211,6 +211,12 @@ mutual
            sc' <- toPTerm startPrec sc
            bracket p startPrec (PLet fc rig (PRef fc n)
                                      ty' val' sc' [])
+  toPTerm p (ICase fc sc scty [PatClause _ lhs rhs])
+      = do sc' <- toPTerm startPrec sc
+           lhs' <- toPTerm startPrec lhs
+           rhs' <- toPTerm startPrec rhs
+           bracket p startPrec
+                   (PLet fc top lhs' (PImplicit fc) sc' rhs' [])
   toPTerm p (ICase fc sc scty alts)
       = do sc' <- toPTerm startPrec sc
            alts' <- traverse toPClause alts

src/TTImp/Interactive/CaseSplit.idr

@@ -133,8 +133,13 @@ defaultNames = ["x", "y", "z", "w", "v", "s", "t", "u"]
 
 export
 getArgName : {auto c : Ref Ctxt Defs} ->
-             Defs -> Name -> List Name -> NF vars -> Core String
-getArgName defs x allvars ty
+             Defs -> Name ->
+             List Name -> -- explicitly bound names (possibly coming later),
+                          -- so we don't invent a default
+                          -- name that duplicates it
+             List Name -> -- names bound so far
+             NF vars -> Core String
+getArgName defs x bound allvars ty
     = do defnames <- findNames ty
          pure $ getName x defnames allvars
   where
@@ -145,13 +150,17 @@ getArgName defs x allvars ty
              then pure (Just t)
              else lookupName n ts
 
+    notBound : String -> Bool
+    notBound x = not $ UN x `elem` bound
+
     findNames : NF vars -> Core (List String)
-    findNames (NBind _ x (Pi _ _ _) _) = pure ["f", "g"]
+    findNames (NBind _ x (Pi _ _ _) _)
+        = pure (filter notBound ["f", "g"])
     findNames (NTCon _ n _ _ _)
         = case !(lookupName n (NameMap.toList (namedirectives defs))) of
-               Nothing => pure defaultNames
-               Just ns => pure ns
-    findNames ty = pure defaultNames
+               Nothing => pure (filter notBound defaultNames)
+               Just ns => pure (filter notBound ns)
+    findNames ty = pure (filter notBound defaultNames)
 
     getName : Name -> List String -> List Name -> String
     getName (UN n) defs used = unique (n :: defs) (n :: defs) 0 used
@@ -159,20 +168,27 @@ getArgName defs x allvars ty
 
 export
 getArgNames : {auto c : Ref Ctxt Defs} ->
-              Defs -> List Name -> Env Term vars -> NF vars ->
+              Defs -> List Name -> List Name -> Env Term vars -> NF vars ->
               Core (List String)
-getArgNames defs allvars env (NBind fc x (Pi _ p ty) sc)
+getArgNames defs bound allvars env nf@(NBind fc x (Pi _ p ty) sc)
     = do ns <- case p of
-                    Explicit => pure [!(getArgName defs x allvars ty)]
+                    Explicit => pure [!(getArgName defs x bound allvars ty)]
                     _ => pure []
          sc' <- sc defs (toClosure defaultOpts env (Erased fc False))
-         pure $ ns ++ !(getArgNames defs (map UN ns ++ allvars) env sc')
-getArgNames defs allvars env val = pure []
+         pure $ ns ++ !(getArgNames defs bound (map UN ns ++ allvars) env sc')
+getArgNames defs bound allvars env val = pure []
+
+export
+explicitlyBound : Defs -> NF [] -> Core (List Name)
+explicitlyBound defs (NBind fc x (Pi _ _ _) sc)
+    = pure $ x :: !(explicitlyBound defs
+                    !(sc defs (toClosure defaultOpts [] (Erased fc False))))
+explicitlyBound defs _ = pure []
 
 export
 getEnvArgNames : {auto c : Ref Ctxt Defs} ->
                  Defs -> Nat -> NF [] -> Core (List String)
-getEnvArgNames defs Z sc = getArgNames defs [] [] sc
+getEnvArgNames defs Z sc = getArgNames defs !(explicitlyBound defs sc) [] [] sc
 getEnvArgNames defs (S k) (NBind fc n _ sc)
     = getEnvArgNames defs k !(sc defs (toClosure defaultOpts [] (Erased fc False)))
 getEnvArgNames defs n ty = pure []
@@ -185,7 +201,7 @@ expandCon fc usedvars con
               | Nothing => throw (UndefinedName fc con)
          pure (apply (IVar fc con)
                 (map (IBindVar fc)
-                     !(getArgNames defs usedvars []
+                     !(getArgNames defs [] usedvars []
                                    !(nf defs [] ty))))
 
 updateArg : {auto c : Ref Ctxt Defs} ->

src/TTImp/Interactive/ExprSearch.idr

@@ -21,7 +21,10 @@ import Core.Unify
 import Core.TT
 import Core.Value
 
+import TTImp.Elab.Check
 import TTImp.Interactive.CaseSplit
+import TTImp.TTImp
+import TTImp.Unelab
 import TTImp.Utils
 
 import Data.Bool.Extra
@@ -32,17 +35,16 @@ import Data.List
 
 -- Data for building recursive calls - the function name, and the structure
 -- of the LHS. Only recursive calls with a different structure are okay.
+public export -- to keep Idris2-boot happy!
 record RecData where
   constructor MkRecData
+  {vars : List Name}
   recname : Name -- resolved name
   lhsapp : Term vars
 
-record SearchOpts where
-  constructor MkSearchOpts
-  holesOK : Bool
-  recOK : Bool
-  depth : Nat
-  inArg : Bool
+-- Additional definitions required to support the result
+ExprDefs : Type
+ExprDefs = List ImpDecl
 
 export
 data Search : Type -> Type where
@@ -135,13 +137,37 @@ nextResult s
                   Result r next => pure (Just (r, next)))
          (pure Nothing)
 
+public export
+record SearchOpts where
+  constructor MkSearchOpts
+  holesOK : Bool -- add a hole on getting stuck, rather than an error
+  getRecData : Bool -- update the LHS data
+  recData : Maybe RecData -- LHS, to help build recursive calls
+  depth : Nat -- maximum search depth
+  inArg : Bool -- in an argument (not top level). Here, try recursive calls
+               -- before constructors, otherwise try recursive calls last
+  inUnwrap : Bool
+  ltor : Bool -- case split left to right
+              -- (right to left is good for auxiliary definitions, because
+              -- then we split on the new pattern first)
+  mustSplit : Bool -- must begin with a case split (in a case helper)
+  doneSplit : Bool -- definitely under a case split
+  genExpr : Maybe (SearchOpts -> Name -> Nat -> ClosedTerm ->
+                   Core (Search (FC, List ImpClause)))
+
+export
+initSearchOpts : (rec : Bool) -> (maxDepth : Nat) -> SearchOpts
+initSearchOpts rec depth
+    = MkSearchOpts False rec Nothing depth
+                   False False True False False
+                   Nothing
+
 search : {auto c : Ref Ctxt Defs} ->
          {auto m : Ref MD Metadata} ->
          {auto u : Ref UST UState} ->
          FC -> RigCount ->
-         SearchOpts -> Maybe RecData ->
-         ClosedTerm ->
-         Name -> Core (Search ClosedTerm)
+         SearchOpts -> ClosedTerm ->
+         Name -> Core (Search (ClosedTerm, ExprDefs))
 
 getAllEnv : {vars : _} ->
             FC -> (done : List Name) ->
@@ -150,21 +176,28 @@ getAllEnv : {vars : _} ->
 getAllEnv fc done [] = []
 getAllEnv {vars = v :: vs} fc done (b :: env)
    = let rest = getAllEnv fc (done ++ [v]) env
-         MkVar p = weakenVar done {inner = v :: vs} First in
-         (Local fc Nothing _ p,
-           rewrite appendAssociative done [v] vs in
-              weakenNs (done ++ [v]) (binderType b)) ::
-                   rewrite appendAssociative done [v] vs in rest
+         MkVar p = weakenVar done {inner = v :: vs} First
+         usable = usableName v in
+         if usable
+            then (Local fc Nothing _ p,
+                     rewrite appendAssociative done [v] vs in
+                        weakenNs (done ++ [v]) (binderType b)) ::
+                             rewrite appendAssociative done [v] vs in rest
+            else rewrite appendAssociative done [v] vs in rest
+  where
+    usableName : Name -> Bool
+    usableName (UN _) = True
+    usableName _ = False
 
 -- Search recursively, but only if the given name wasn't solved by unification
 searchIfHole : {vars : _} ->
                {auto c : Ref Ctxt Defs} ->
                {auto m : Ref MD Metadata} ->
                {auto u : Ref UST UState} ->
-               FC -> SearchOpts -> Maybe RecData -> ClosedTerm ->
+               FC -> SearchOpts -> ClosedTerm ->
                Env Term vars -> ArgInfo vars ->
-               Core (Search (Term vars))
-searchIfHole fc opts defining topty env arg
+               Core (Search (Term vars, ExprDefs))
+searchIfHole fc opts topty env arg
     = case depth opts of
            Z => noResult
            S k =>
@@ -174,16 +207,17 @@ searchIfHole fc opts defining topty env arg
                  Just gdef <- lookupCtxtExact (Resolved hole) (gamma defs)
                       | Nothing => noResult
                  let Hole _ _ = definition gdef
-                      | _ => one !(normaliseHoles defs env (metaApp arg))
+                      | _ => one (!(normaliseHoles defs env (metaApp arg)), [])
                                 -- already solved
                  res <- search fc rig (record { depth = k,
                                                 inArg = True } opts)
-                               defining topty (Resolved hole)
+                               topty (Resolved hole)
                  -- When we solve an argument, we're also building a lambda
                  -- expression for its environment, so we need to apply it to
                  -- the current environment to use it as an argument.
-                 traverse (\tm => pure !(normaliseHoles defs env
-                                         (applyTo fc (embed tm) env))) res
+                 traverse (\(tm, ds) =>
+                    pure (!(normaliseHoles defs env
+                             (applyTo fc (embed tm) env)), ds)) res
 
 explicit : ArgInfo vars -> Bool
 explicit ai
@@ -211,6 +245,7 @@ firstSuccess (elab :: elabs)
              put Ctxt defs
              firstSuccess elabs
 
+-- Take the first successful result of the two given searches
 export
 trySearch : {auto c : Ref Ctxt Defs} ->
             {auto u : Ref UST UState} ->
@@ -240,18 +275,19 @@ combine f (Result x nextx) (Result y nexty)
 mkCandidates : {vars : _} ->
                {auto c : Ref Ctxt Defs} ->
                {auto u : Ref UST UState} ->
-               FC -> Term vars -> List (Search (Term vars)) ->
-               Core (Search (Term vars))
+               FC -> Term vars -> ExprDefs ->
+               List (Search (Term vars, ExprDefs)) ->
+               Core (Search (Term vars, ExprDefs))
 -- out of arguments, we have a candidate
-mkCandidates fc f [] = one f
+mkCandidates fc f ds [] = one (f, ds)
 -- argument has run out of ideas, we're stuck
-mkCandidates fc f (NoMore :: argss) = noResult
+mkCandidates fc f ds (NoMore :: argss) = noResult
 -- make a candidate from 'f arg' applied to the rest of the arguments
-mkCandidates fc f (Result arg next :: argss)
+mkCandidates fc f ds (Result (arg, ds') next :: argss)
     = firstSuccess
-           [mkCandidates fc (App fc f arg) argss,
+           [mkCandidates fc (App fc f arg) (ds ++ ds') argss,
             do next' <- next
-               mkCandidates fc f (next' :: argss)]
+               mkCandidates fc f ds (next' :: argss)]
 
 -- Apply the name to arguments and see if the result unifies with the target
 -- type, then try to automatically solve any holes which were generated.
@@ -262,8 +298,9 @@ searchName : {vars : _} ->
              {auto u : Ref UST UState} ->
              FC -> RigCount -> SearchOpts ->
              Env Term vars -> NF vars -> ClosedTerm ->
-             Maybe RecData -> (Name, GlobalDef) -> Core (Search (Term vars))
-searchName fc rigc opts env target topty defining (n, ndef)
+             (Name, GlobalDef) ->
+             Core (Search (Term vars, ExprDefs))
+searchName fc rigc opts env target topty (n, ndef)
     = do defs <- get Ctxt
          let True = visibleInAny (!getNS :: !getNestedNS)
                                  (fullname ndef) (visibility ndef)
@@ -285,11 +322,11 @@ searchName fc rigc opts env target topty defining (n, ndef)
          let [] = constraints ures
              | _ => noResult
          -- Search the explicit arguments first, they may resolve other holes
-         traverse (searchIfHole fc opts defining topty env)
+         traverse (searchIfHole fc opts topty env)
                   (filter explicit args)
-         args' <- traverse (searchIfHole fc opts defining topty env)
+         args' <- traverse (searchIfHole fc opts topty env)
                            args
-         mkCandidates fc (Ref fc namety n) args'
+         mkCandidates fc (Ref fc namety n) [] args'
   where
     -- we can only use the name in a search result if it's a user writable
     -- name (so, no recursive with blocks or case blocks, for example)
@@ -305,10 +342,9 @@ getSuccessful : {vars : _} ->
                 {auto u : Ref UST UState} ->
                 FC -> RigCount -> SearchOpts -> Bool ->
                 Env Term vars -> Term vars -> ClosedTerm ->
-                Maybe RecData ->
-                List (Core (Search (Term vars))) ->
-                Core (Search (Term vars))
-getSuccessful {vars} fc rig opts mkHole env ty topty defining all
+                List (Core (Search (Term vars, ExprDefs))) ->
+                Core (Search (Term vars, ExprDefs))
+getSuccessful {vars} fc rig opts mkHole env ty topty all
     = do res <- firstSuccess all
          case res of
               NoMore => -- If no successful search, make a hole
@@ -316,12 +352,12 @@ getSuccessful {vars} fc rig opts mkHole env ty topty defining all
                    then do defs <- get Ctxt
                            let base = maybe "arg"
                                             (\r => nameRoot (recname r) ++ "_rhs")
-                                            defining
+                                            (recData opts)
                            hn <- uniqueName defs (map nameRoot vars) base
                            (idx, tm) <- newMeta fc rig env (UN hn) ty
                                                 (Hole (length env) (holeInit False))
                                                 False
-                           one tm
+                           one (tm, [])
                    else noResult
               r => pure r
 
@@ -331,17 +367,17 @@ searchNames : {vars : _} ->
               {auto u : Ref UST UState} ->
               FC -> RigCount -> SearchOpts -> Env Term vars ->
               Term vars -> ClosedTerm ->
-              Maybe RecData -> List Name -> Core (Search (Term vars))
-searchNames fc rig opts env ty topty defining []
+              List Name -> Core (Search (Term vars, ExprDefs))
+searchNames fc rig opts env ty topty []
     = noResult
-searchNames fc rig opts env ty topty defining (n :: ns)
+searchNames fc rig opts env ty topty (n :: ns)
     = do defs <- get Ctxt
          vis <- traverse (visible (gamma defs) (currentNS defs :: nestedNS defs)) (n :: ns)
          let visns = mapMaybe id vis
          nfty <- nf defs env ty
          logTerm 10 ("Searching " ++ show (map fst visns) ++ " for ") ty
-         getSuccessful fc rig opts False env ty topty defining
-            (map (searchName fc rig opts env nfty topty defining) visns)
+         getSuccessful fc rig opts False env ty topty
+            (map (searchName fc rig opts env nfty topty) visns)
   where
     visible : Context -> List (List String) -> Name ->
               Core (Maybe (Name, GlobalDef))
@@ -358,19 +394,17 @@ tryRecursive : {vars : _} ->
                {auto u : Ref UST UState} ->
                FC -> RigCount -> SearchOpts ->
                Env Term vars -> Term vars -> ClosedTerm ->
-               Maybe RecData -> Core (Search (Term vars))
-tryRecursive fc rig opts env ty topty Nothing
-    = noResult
-tryRecursive fc rig opts env ty topty (Just rdata)
+               RecData -> Core (Search (Term vars, ExprDefs))
+tryRecursive fc rig opts env ty topty rdata
     = do defs <- get Ctxt
          case !(lookupCtxtExact (recname rdata) (gamma defs)) of
               Nothing => noResult
               Just def =>
-                do res <- searchName fc rig opts env !(nf defs env ty)
-                                     topty Nothing
-                                     (recname rdata, def)
+                do res <- searchName fc rig (record { recData = Nothing } opts)
+                                     env !(nf defs env ty)
+                                     topty (recname rdata, def)
                    defs <- get Ctxt
-                   filterS (structDiff (lhsapp rdata)) res
+                   filterS (structDiffTm (lhsapp rdata)) res
   where
     mutual
       -- A fairly simple superficialy syntactic check to make sure that
@@ -415,6 +449,9 @@ tryRecursive fc rig opts env ty topty (Just rdata)
                (f', args') = getFnArgs tm' in
                appsDiff f f' args args'
 
+      structDiffTm : Term vs -> (Term vs', ExprDefs) -> Bool
+      structDiffTm tm (tm', _) = structDiff tm tm'
+
 -- A local is usable as long as its type isn't a hole
 usableLocal : FC -> Env Term vars -> NF vars -> Bool
 usableLocal loc env (NApp _ (NMeta _ _ _) args) = False
@@ -424,25 +461,26 @@ searchLocalWith : {vars : _} ->
                   {auto c : Ref Ctxt Defs} ->
                   {auto m : Ref MD Metadata} ->
                   {auto u : Ref UST UState} ->
-                  FC -> RigCount -> SearchOpts -> Env Term vars ->
+                  FC -> Bool ->
+                  RigCount -> SearchOpts -> Env Term vars ->
                   List (Term vars, Term vars) ->
-                  Term vars -> ClosedTerm -> Maybe RecData ->
-                  Core (Search (Term vars))
-searchLocalWith fc rig opts env [] ty topty defining
+                  Term vars -> ClosedTerm ->
+                  Core (Search (Term vars, ExprDefs))
+searchLocalWith fc nofn rig opts env [] ty topty
     = noResult
-searchLocalWith {vars} fc rig opts env ((p, pty) :: rest) ty topty defining
+searchLocalWith {vars} fc nofn rig opts env ((p, pty) :: rest) ty topty
     = do defs <- get Ctxt
          nty <- nf defs env ty
-         getSuccessful fc rig opts False env ty topty defining
+         getSuccessful fc rig opts False env ty topty
                        [findPos defs p id !(nf defs env pty) nty,
-                        searchLocalWith fc rig opts env rest ty
-                                        topty defining]
+                        searchLocalWith fc nofn rig opts env rest ty
+                                        topty]
   where
     findDirect : Defs -> Term vars ->
                  (Term vars -> Term vars) ->
                  NF vars -> -- local variable's type
                  NF vars -> -- type we're looking for
-                 Core (Search (Term vars))
+                 Core (Search (Term vars, ExprDefs))
     findDirect defs prf f nty ty
         = do (args, appTy) <- mkArgs fc rig env nty
              -- We can only use a local variable if it's not an unsolved
@@ -450,23 +488,25 @@ searchLocalWith {vars} fc rig opts env ((p, pty) :: rest) ty topty defining
              if usableLocal fc env nty
                 then
                   tryUnify -- try with no arguments first
-                    (do ures <- unify inTerm fc env ty nty
+                    (do when (not (isNil args) && nofn) $
+                             throw (InternalError "Must apply function")
+                        ures <- unify inTerm fc env ty nty
                         let [] = constraints ures
                             | _ => throw (InternalError "Can't use directly")
-                        mkCandidates fc (f prf) [])
+                        mkCandidates fc (f prf) [] [])
                     (do ures <- unify inTerm fc env ty appTy
                         let [] = constraints ures
                             | _ => noResult
-                        args' <- traverse (searchIfHole fc opts defining topty env)
+                        args' <- traverse (searchIfHole fc opts topty env)
                                           args
-                        mkCandidates fc (f prf) args')
+                        mkCandidates fc (f prf) [] args')
                 else noResult
 
     findPos : Defs -> Term vars ->
               (Term vars -> Term vars) ->
-              NF vars -> NF vars -> Core (Search (Term vars))
+              NF vars -> NF vars -> Core (Search (Term vars, ExprDefs))
     findPos defs prf f x@(NTCon pfc pn _ _ [xty, yty]) target
-        = getSuccessful fc rig opts False env ty topty defining
+        = getSuccessful fc rig opts False env ty topty
               [findDirect defs prf f x target,
                  (do fname <- maybe (throw (InternalError "No fst"))
                                     pure
@@ -478,7 +518,7 @@ searchLocalWith {vars} fc rig opts env ((p, pty) :: rest) ty topty defining
                         then do empty <- clearDefs defs
                                 xtytm <- quote empty env xty
                                 ytytm <- quote empty env yty
-                                getSuccessful fc rig opts False env ty topty defining
+                                getSuccessful fc rig opts False env ty topty
                                   [(do xtynf <- evalClosure defs xty
                                        findPos defs prf
                                          (\arg => apply fc (Ref fc Func fname)
@@ -502,39 +542,198 @@ searchLocal : {vars : _} ->
               {auto u : Ref UST UState} ->
               FC -> RigCount -> SearchOpts ->
               Env Term vars -> Term vars -> ClosedTerm ->
-              Maybe RecData -> Core (Search (Term vars))
-searchLocal fc rig opts env ty topty defining
+              Core (Search (Term vars, ExprDefs))
+searchLocal fc rig opts env ty topty
+    = -- Reverse the environment so we try the patterns left to right.
+      -- This heuristic is just so arguments appear the same order in
+      -- recursive calls
+      searchLocalWith fc False rig opts env (reverse (getAllEnv fc [] env))
+                      ty topty
+
+makeHelper : {vars : _} ->
+             {auto c : Ref Ctxt Defs} ->
+             {auto m : Ref MD Metadata} ->
+             {auto u : Ref UST UState} ->
+             FC -> RigCount -> SearchOpts ->
+             Env Term vars ->
+             Term vars -> Term vars -> Search (Term vars, ExprDefs) ->
+             Core (Search (Term vars, ExprDefs))
+makeHelper fc rig opts env letty targetty NoMore
+    = pure NoMore
+makeHelper fc rig opts env letty targetty (Result (locapp, ds) next)
+    = do let S depth' = depth opts
+             | Z => noResult
+         logTerm 10 "Local app" locapp
+         let Just gendef = genExpr opts
+             | Nothing => noResult
+         defs <- get Ctxt
+         intn <- genVarName "cval"
+         helpern_in <- genCaseName "search"
+         helpern <- inCurrentNS helpern_in
+         let env' = Lam top Explicit letty :: env
+         scopeMeta <- metaVar fc top env' helpern
+                             (weaken {n = intn} targetty)
+         let scope = toApp scopeMeta
+         updateDef helpern (const (Just None))
+         -- Apply the intermediate result to the helper function we're
+         -- about to generate.
+         let def = App fc (Bind fc intn (Lam top Explicit letty) scope)
+                          locapp
+
+         logTermNF 10 "Binding def" env def
+         defs <- get Ctxt
+         Just ty <- lookupTyExact helpern (gamma defs)
+             | Nothing => throw (InternalError "Can't happen")
+         logTermNF 10 "Type of scope name" [] ty
+
+         -- Generate a definition for the helper, but with more restrictions.
+         -- Always take the first result, to avoid blowing up search space.
+         -- Go right to left on variable split, to get the variable we just
+         -- added first.
+         -- There must be at least one case split.
+         ((helper :: _), nextdef) <- 
+                    searchN 1 $ gendef (record { getRecData = False,
+                                                 inUnwrap = True,
+                                                 depth = depth',
+                                                 ltor = False,
+                                                 mustSplit = True } opts)
+                                       helpern 0 ty
+              | _ => do log 10 "No results"
+                        noResult
+         
+         let helperdef = IDef fc helpern (snd helper)
+         log 10 $ "Def: " ++ show helperdef
+         pure (Result (def, helperdef :: ds) -- plus helper
+                      (do next' <- next
+                          makeHelper fc rig opts env letty targetty next'))
+  where
+    -- convert a metavar application (as created by 'metaVar') to a normal 
+    -- application (as required by a case block)
+    toApp : forall vars . Term vars -> Term vars
+    toApp (Meta fc n i args) = apply fc (Ref fc Func (Resolved i)) args
+    toApp tm = tm
+
+
+tryIntermediateWith : {vars : _} ->
+                      {auto c : Ref Ctxt Defs} ->
+                      {auto m : Ref MD Metadata} ->
+                      {auto u : Ref UST UState} ->
+                      FC -> RigCount -> SearchOpts ->
+                      Env Term vars -> List (Term vars, Term vars) ->
+                      Term vars -> ClosedTerm ->
+                      Core (Search (Term vars, ExprDefs))
+tryIntermediateWith fc rig opts env [] ty topty = noResult
+tryIntermediateWith fc rig opts env ((p, pty) :: rest) ty topty
     = do defs <- get Ctxt
-         -- Reverse the environment so we try the patterns left to right.
-         -- This heuristic is just so arguments appear the same order in
-         -- recursive calls
-         searchLocalWith fc rig opts env (reverse (getAllEnv fc [] env))
-                         ty topty defining
+         getSuccessful fc rig opts False env ty topty
+                       [applyLocal defs p !(nf defs env pty) ty,
+                        tryIntermediateWith fc rig opts env rest ty
+                                            topty]
+  where
+    matchable : Defs -> NF vars -> Core Bool
+    matchable defs (NBind fc x (Pi _ _ _) sc)
+        = matchable defs !(sc defs (toClosure defaultOpts env
+                                              (Erased fc False)))
+    matchable defs (NTCon _ _ _ _ _) = pure True
+    matchable _ _ = pure False
+
+    applyLocal : Defs -> Term vars ->
+                 NF vars -> Term vars -> Core (Search (Term vars, ExprDefs))
+    applyLocal defs tm locty@(NBind _ x (Pi _ _ _) sc) targetty
+        = -- If the local has a function type, and the return type is
+          -- something we can pattern match on (so, NTCon) then apply it,
+          -- let bind the result, and try to generate a definition for
+          -- the scope of the let binding
+          do True <- matchable defs 
+                           !(sc defs (toClosure defaultOpts env 
+                                                (Erased fc False)))
+                 | False => noResult
+             intnty <- genVarName "cty"
+             letty <- metaVar fc erased env intnty (TType fc)
+             let opts' = record { inUnwrap = True } opts
+             locsearch <- searchLocalWith fc True rig opts' env [(p, pty)]
+                                          letty topty
+             makeHelper fc rig opts env letty targetty locsearch
+    applyLocal defs tm _ _ = noResult
+
+-- Try to make progress by applying a local variable or the recursive
+-- definition to an argument, then making a helper function to complete
+-- the job
+tryIntermediate : {vars : _} ->
+                  {auto c : Ref Ctxt Defs} ->
+                  {auto m : Ref MD Metadata} ->
+                  {auto u : Ref UST UState} ->
+                  FC -> RigCount -> SearchOpts ->
+                  Env Term vars -> Term vars -> ClosedTerm ->
+                  Core (Search (Term vars, ExprDefs))
+tryIntermediate fc rig opts env ty topty
+    = tryIntermediateWith fc rig opts env (reverse (getAllEnv fc [] env))
+                          ty topty
+
+-- Try making a recursive call and unpacking the result. Only do this if
+-- the return type is a single constructor data type, otherwise it massively
+-- increases the search space, and the intention is for unpacking
+-- things like dependent pairs and singleton types before proceeding.
+tryIntermediateRec : {vars : _} ->
+                     {auto c : Ref Ctxt Defs} ->
+                     {auto m : Ref MD Metadata} ->
+                     {auto u : Ref UST UState} ->
+                     FC -> RigCount -> SearchOpts ->
+                     Env Term vars -> 
+                     Term vars -> ClosedTerm ->
+                     Maybe RecData -> Core (Search (Term vars, ExprDefs))
+tryIntermediateRec fc rig opts env ty topty Nothing = noResult
+tryIntermediateRec fc rig opts env ty topty (Just rd)
+    = do defs <- get Ctxt
+         Just rty <- lookupTyExact (recname rd) (gamma defs)
+              | Nothing => noResult
+         True <- isSingleCon defs !(nf defs [] rty)
+              | _ => noResult
+         intnty <- genVarName "cty"
+         letty <- metaVar fc erased env intnty (TType fc)
+         let opts' = record { inUnwrap = True,
+                              recData = Nothing } opts
+         logTerm 10 "Trying recursive search for" ty
+         log 10 $ show !(toFullNames (recname rd))
+         logTerm 10 "LHS" !(toFullNames (lhsapp rd))
+         recsearch <- tryRecursive fc rig opts' env letty topty rd
+         makeHelper fc rig opts' env letty ty recsearch
+  where
+    isSingleCon : Defs -> NF [] -> Core Bool
+    isSingleCon defs (NBind fc x (Pi _ _ _) sc)
+        = isSingleCon defs !(sc defs (toClosure defaultOpts []
+                                              (Erased fc False)))
+    isSingleCon defs (NTCon _ n _ _ _)
+        = do Just (TCon _ _ _ _ _ _ [con] _) <- lookupDefExact n (gamma defs)
+                  | _ => pure False
+             pure True
+    isSingleCon _ _ = pure False
 
 searchType : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->
              {auto m : Ref MD Metadata} ->
              {auto u : Ref UST UState} ->
-             FC -> RigCount -> SearchOpts -> Env Term vars -> Maybe RecData ->
+             FC -> RigCount -> SearchOpts -> Env Term vars ->
              ClosedTerm ->
-             Nat -> Term vars -> Core (Search (Term vars))
-searchType fc rig opts env defining topty (S k) (Bind bfc n (Pi c info ty) sc)
+             Nat -> Term vars -> Core (Search (Term vars, ExprDefs))
+searchType fc rig opts env topty (S k) (Bind bfc n (Pi c info ty) sc)
     = do let env' : Env Term (n :: _) = Pi c info ty :: env
          log 10 $ "Introduced lambda, search for " ++ show sc
-         scVal <- searchType fc rig opts env' defining topty k sc
-         pure (map (Bind bfc n (Lam c info ty)) scVal)
-searchType {vars} fc rig opts env defining topty Z (Bind bfc n (Pi c info ty) sc)
+         scVal <- searchType fc rig opts env' topty k sc
+         pure (map (\ (sc, ds) => (Bind bfc n (Lam c info ty) sc, ds)) scVal)
+searchType {vars} fc rig opts env topty Z (Bind bfc n (Pi c info ty) sc)
     = -- try a local before creating a lambda...
-      getSuccessful fc rig opts False env ty topty defining
-           [searchLocal fc rig opts env (Bind bfc n (Pi c info ty) sc) topty defining,
+      getSuccessful fc rig opts False env ty topty
+           [searchLocal fc rig opts env (Bind bfc n (Pi c info ty) sc) topty,
             (do defs <- get Ctxt
-                let n' = UN !(getArgName defs n vars !(nf defs env ty))
+                let n' = UN !(getArgName defs n [] vars !(nf defs env ty))
                 let env' : Env Term (n' :: _) = Pi c info ty :: env
                 let sc' = renameTop n' sc
                 log 10 $ "Introduced lambda, search for " ++ show sc'
-                scVal <- searchType fc rig opts env' defining topty Z sc'
-                pure (map (Bind bfc n' (Lam c info ty)) scVal))]
-searchType fc rig opts env defining topty _ ty
+                scVal <- searchType fc rig opts env' topty Z sc'
+                pure (map (\ (sc, ds) =>
+                             (Bind bfc n' (Lam c info ty) sc, ds)) scVal))]
+searchType fc rig opts env topty _ ty
     = case getFnArgs ty of
            (Ref rfc (TyCon t ar) n, args) =>
                 do defs <- get Ctxt
@@ -548,53 +747,68 @@ searchType fc rig opts env defining topty _ ty
                              log 10 $ "Hints found for " ++ show n ++ " "
                                          ++ show allHints
                              let tries =
-                                   [searchLocal fc rig opts env ty topty defining,
-                                    searchNames fc rig opts env ty topty defining allHints]
+                                   [searchLocal fc rig opts env ty topty,
+                                    searchNames fc rig opts env ty topty allHints]
                              let tryRec =
-                                   if recOK opts
-                                      then [tryRecursive fc rig opts env ty topty defining]
+                                   case recData opts of
+                                        Nothing => []
+                                        Just rd => [tryRecursive fc rig opts env ty topty rd]
+                             let tryIntRec = 
+                                   if doneSplit opts
+                                      then [tryIntermediateRec fc rig opts env ty topty (recData opts)]
                                       else []
+                             let tryInt = if not (inUnwrap opts)
+                                             then [tryIntermediate fc rig opts env ty topty]
+                                             else []
                              -- if we're in an argument, try the recursive call
                              -- first. We're more likely to want that than nested
                              -- constructors.
                              let allns : List _
                                      = if inArg opts
-                                          then tryRec ++ tries
-                                          else tries ++ tryRec
-                             getSuccessful fc rig opts True env ty topty defining allns
+                                          then tryRec ++ tryInt ++ tries
+                                          else tryInt ++ tries ++ tryRec ++ tryIntRec
+                             getSuccessful fc rig opts True env ty topty allns
                      else noResult
            _ => do logTerm 10 "Searching locals only at" ty
-                   getSuccessful fc rig opts True env ty topty defining
-                       ([searchLocal fc rig opts env ty topty defining]
-                         ++ if recOK opts
-                               then [tryRecursive fc rig opts env ty topty defining]
-                               else [])
+                   let tryInt = if not (inUnwrap opts)
+                                   then [tryIntermediate fc rig opts env ty topty]
+                                   else []
+                   let tryIntRec = if inArg opts || not (doneSplit opts)
+                                      then []
+                                      else [tryIntermediateRec fc rig opts env ty topty (recData opts)]
+                   getSuccessful fc rig opts True env ty topty
+                           (tryInt ++ [searchLocal fc rig opts env ty topty]
+                             ++ case recData opts of
+                                     Nothing => []
+                                     Just rd => [tryRecursive fc rig opts env ty topty rd]
+                             ++ tryIntRec)
 
 searchHole : {auto c : Ref Ctxt Defs} ->
              {auto m : Ref MD Metadata} ->
              {auto u : Ref UST UState} ->
-             FC -> RigCount -> SearchOpts -> Maybe RecData -> Name ->
+             FC -> RigCount -> SearchOpts -> Name ->
              Nat -> ClosedTerm ->
-             Defs -> GlobalDef -> Core (Search ClosedTerm)
-searchHole fc rig opts defining n locs topty defs glob
+             Defs -> GlobalDef -> Core (Search (ClosedTerm, ExprDefs))
+searchHole fc rig opts n locs topty defs glob
     = do searchty <- normalise defs [] (type glob)
          logTerm 10 "Normalised type" searchty
-         searchType fc rig opts [] defining topty locs searchty
+         searchType fc rig opts [] topty locs searchty
 
 -- Declared at the top
-search fc rig opts defining topty n_in
+search fc rig opts topty n_in
     = do defs <- get Ctxt
          case !(lookupHoleName n_in (gamma defs)) of
               Just (n, i, gdef) =>
                    -- The definition should be 'BySearch' at this stage,
                    -- if it's arising from an auto implicit
                    case definition gdef of
-                        Hole locs _ => searchHole fc rig opts defining n locs topty defs gdef
-                        BySearch _ _ _ => searchHole fc rig opts defining n
+                        Hole locs _ => searchHole fc rig opts n locs topty defs gdef
+                        BySearch _ _ _ => searchHole fc rig opts n
                                                    !(getArity defs [] (type gdef))
                                                    topty defs gdef
                         _ => do log 10 $ show n_in ++ " not a hole"
-                                throw (InternalError $ "Not a hole: " ++ show n ++ " in " ++ show (map recname defining))
+                                throw (InternalError $ "Not a hole: " ++ show n ++ " in " ++
+                                        show (map recname (recData opts)))
               _ => do log 10 $ show n_in ++ " not found"
                       throw (UndefinedName fc n_in)
   where
@@ -611,7 +825,7 @@ getLHSData : Defs -> Maybe ClosedTerm -> Core (Maybe RecData)
 getLHSData defs Nothing = pure Nothing
 getLHSData defs (Just tm) = pure $ getLHS !(normaliseHoles defs [] tm)
   where
-    getLHS : Term vars -> Maybe RecData
+    getLHS : {vars : _} -> Term vars -> Maybe RecData
     getLHS (Bind _ _ (PVar _ _ _) sc) = getLHS sc
     getLHS (Bind _ _ (PLet _ _ _) sc) = getLHS sc
     getLHS sc
@@ -620,29 +834,41 @@ getLHSData defs (Just tm) = pure $ getLHS !(normaliseHoles defs [] tm)
                _ => Nothing
 
 firstLinearOK : {auto c : Ref Ctxt Defs} ->
+                {auto m : Ref MD Metadata} ->
                 {auto u : Ref UST UState} ->
-                FC -> Search ClosedTerm -> Core (Search ClosedTerm)
+                FC -> Search (ClosedTerm, ExprDefs) ->
+                Core (Search RawImp)
 firstLinearOK fc NoMore = noResult
-firstLinearOK fc (Result t next)
-    = tryUnify
-            (do linearCheck fc linear False [] t
-                pure (Result t (firstLinearOK fc !next)))
-            (do next' <- next
-                firstLinearOK fc next')
+firstLinearOK fc (Result (t, ds) next)
+    = handleUnify
+            (do when (not (isNil ds)) $
+                   traverse_ (processDecl [InCase] (MkNested []) []) ds
+                linearCheck fc linear False [] t
+                defs <- get Ctxt
+                nft <- normaliseHoles defs [] t
+                raw <- unelab [] !(toFullNames nft)
+                pure (Result raw (firstLinearOK fc !next)))
+            (\err =>
+                do next' <- next
+                   firstLinearOK fc next')
 
 export
-exprSearch : {auto c : Ref Ctxt Defs} ->
-             {auto m : Ref MD Metadata} ->
-             {auto u : Ref UST UState} ->
-             FC -> Name -> List Name -> Core (Search ClosedTerm)
-exprSearch fc n_in hints
+exprSearchOpts : {auto c : Ref Ctxt Defs} ->
+                 {auto m : Ref MD Metadata} ->
+                 {auto u : Ref UST UState} ->
+                 SearchOpts -> FC -> Name -> List Name ->
+                 Core (Search RawImp)
+exprSearchOpts opts fc n_in hints
     = do defs <- get Ctxt
          Just (n, idx, gdef) <- lookupHoleName n_in defs
              | Nothing => throw (UndefinedName fc n_in)
          lhs <- findHoleLHS !(getFullName (Resolved idx))
          log 10 $ "LHS hole data " ++ show (n, lhs)
-         res <- search fc (multiplicity gdef) (MkSearchOpts False True 5 False)
-                       !(getLHSData defs lhs) (type gdef) n
+         opts' <- if getRecData opts
+                     then do d <- getLHSData defs lhs
+                             pure (record { recData = d } opts)
+                     else pure opts
+         res <- search fc (multiplicity gdef) opts' (type gdef) n
          firstLinearOK fc res
   where
     lookupHoleName : Name -> Defs -> Core (Maybe (Name, Int, GlobalDef))
@@ -653,11 +879,20 @@ exprSearch fc n_in hints
                                [res] => pure $ Just res
                                _ => pure Nothing
 
+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)
+
 export
 exprSearchN : {auto c : Ref Ctxt Defs} ->
               {auto m : Ref MD Metadata} ->
               {auto u : Ref UST UState} ->
-              FC -> Nat -> Name -> List Name -> Core (List ClosedTerm)
+              FC -> Nat -> Name -> List Name ->
+              Core (List RawImp)
 exprSearchN fc max n hints
     = do (res, _) <- searchN max (exprSearch fc n hints)
          pure res

src/TTImp/Interactive/GenerateDef.idr

@@ -52,9 +52,9 @@ uniqueRHS c = pure c
 expandClause : {auto c : Ref Ctxt Defs} ->
                {auto m : Ref MD Metadata} ->
                {auto u : Ref UST UState} ->
-               FC -> Int -> ImpClause ->
+               FC -> SearchOpts -> Int -> ImpClause ->
                Core (Search (List ImpClause))
-expandClause loc n c
+expandClause loc opts n c
     = do c <- uniqueRHS c
          Right clause <- checkClause linear Private False n [] (MkNested []) [] c
             | Left err => noResult -- TODO: impossible clause, do something
@@ -67,15 +67,11 @@ expandClause loc n c
          Just (Hole locs _) <- lookupDefExact (Resolved fn) (gamma defs)
             | _ => throw (GenericMsg loc "No searchable hole on RHS")
          log 10 $ "Expression search for " ++ show (i, fn)
-         rhs' <- exprSearch loc (Resolved fn) []
+         rhs' <- exprSearchOpts opts loc (Resolved fn) []
          traverse (\rhs' =>
-            do defs <- get Ctxt
-               rhsnf <- normaliseHoles defs [] rhs'
-               let (_ ** (env', rhsenv)) = dropLams locs [] rhsnf
-
-               rhsraw <- unelab env' rhsenv
+            do let rhsraw = dropLams locs rhs'
                logTermNF 5 "Got clause" env lhs
-               logTermNF 5 "        = " env' rhsenv
+               log 5 $ "        = " ++ show rhsraw
                pure [updateRHS c rhsraw]) rhs'
   where
     updateRHS : ImpClause -> RawImp -> ImpClause
@@ -84,12 +80,10 @@ expandClause loc n c
     updateRHS (WithClause fc lhs wval flags cs) rhs = WithClause fc lhs wval flags cs
     updateRHS (ImpossibleClause fc lhs) _ = ImpossibleClause fc lhs
 
-    dropLams : {vars : _} ->
-               Nat -> Env Term vars -> Term vars ->
-               (vars' ** (Env Term vars', Term vars'))
-    dropLams Z env tm = (_ ** (env, tm))
-    dropLams (S k) env (Bind _ _ b sc) = dropLams k (b :: env) sc
-    dropLams _ env tm = (_ ** (env, tm))
+    dropLams : Nat -> RawImp -> RawImp
+    dropLams Z tm = tm
+    dropLams (S k) (ILam _ _ _ _ _ sc) = dropLams k sc
+    dropLams _ tm = tm
 
 splittableNames : RawImp -> List Name
 splittableNames (IApp _ f (IBindVar _ n))
@@ -139,15 +133,18 @@ trySplit loc lhsraw lhs rhs n
 generateSplits : {auto m : Ref MD Metadata} ->
                  {auto c : Ref Ctxt Defs} ->
                  {auto u : Ref UST UState} ->
-                 FC -> Int -> ImpClause ->
+                 FC -> SearchOpts -> Int -> ImpClause ->
                  Core (List (Name, List ImpClause))
-generateSplits loc fn (ImpossibleClause fc lhs) = pure []
-generateSplits loc fn (WithClause fc lhs wval flags cs) = pure []
-generateSplits {c} {m} {u} loc fn (PatClause fc lhs rhs)
+generateSplits loc opts fn (ImpossibleClause fc lhs) = pure []
+generateSplits loc opts fn (WithClause fc lhs wval flags cs) = pure []
+generateSplits loc opts fn (PatClause fc lhs rhs)
     = do (lhstm, _) <-
                 elabTerm fn (InLHS linear) [] (MkNested []) []
                          (IBindHere loc PATTERN lhs) Nothing
-         traverse (trySplit fc lhs lhstm rhs) (splittableNames lhs)
+         let splitnames =
+                 if ltor opts then splittableNames lhs
+                              else reverse (splittableNames lhs)
+         traverse (trySplit fc lhs lhstm rhs) splitnames
 
 collectClauses : {auto c : Ref Ctxt Defs} ->
                  {auto u : Ref UST UState} ->
@@ -162,31 +159,68 @@ mutual
   tryAllSplits : {auto c : Ref Ctxt Defs} ->
                  {auto m : Ref MD Metadata} ->
                  {auto u : Ref UST UState} ->
-                 FC -> Int ->
+                 FC -> SearchOpts -> Int ->
                  List (Name, List ImpClause) ->
                  Core (Search (List ImpClause))
-  tryAllSplits loc n [] = noResult
-  tryAllSplits loc n ((x, []) :: rest)
-      = tryAllSplits loc n rest
-  tryAllSplits loc n ((x, cs) :: rest)
+  tryAllSplits loc opts n [] = noResult
+  tryAllSplits loc opts n ((x, []) :: rest)
+      = tryAllSplits loc opts n rest
+  tryAllSplits loc opts n ((x, cs) :: rest)
       = do log 5 $ "Splitting on " ++ show x
-           trySearch (do cs' <- traverse (mkSplits loc n) cs
+           trySearch (do cs' <- traverse (mkSplits loc opts n) cs
                          collectClauses cs')
-                     (tryAllSplits loc n rest)
+                     (tryAllSplits loc opts n rest)
 
   mkSplits : {auto c : Ref Ctxt Defs} ->
              {auto m : Ref MD Metadata} ->
              {auto u : Ref UST UState} ->
-             FC -> Int -> ImpClause ->
+             FC -> SearchOpts -> Int -> ImpClause ->
              Core (Search (List ImpClause))
   -- If the clause works, use it. Otherwise, split on one of the splittable
   -- variables and try all of the resulting clauses
-  mkSplits loc n c
+  mkSplits loc opts n c
       = trySearch
-          (expandClause loc n c)
-          (do cs <- generateSplits loc n c
+          (if mustSplit opts
+              then noResult
+              else expandClause loc opts n c)
+          (do cs <- generateSplits loc opts n c
               log 5 $ "Splits: " ++ show cs
-              tryAllSplits loc n cs)
+              tryAllSplits loc (record { mustSplit = False,
+                                         doneSplit = True } opts) n cs)
+
+export
+makeDefFromType : {auto c : Ref Ctxt Defs} ->
+                  {auto m : Ref MD Metadata} ->
+                  {auto u : Ref UST UState} ->
+                  FC -> 
+                  SearchOpts ->
+                  Name -> -- function name to generate
+                  Nat -> -- number of arguments
+                  ClosedTerm -> -- type of function
+                  Core (Search (FC, List ImpClause))
+makeDefFromType loc opts n envlen ty
+    = tryUnify
+         (do defs <- branch
+             meta <- get MD
+             ust <- get UST
+             argns <- getEnvArgNames defs envlen !(nf defs [] ty)
+             -- Need to add implicit patterns for the outer environment.
+             -- We won't try splitting on these
+             let pre_env = replicate envlen (Implicit loc True)
+
+             rhshole <- uniqueName defs [] (fnName False n ++ "_rhs")
+             let initcs = PatClause loc
+                                (apply (IVar loc n) (pre_env ++ (map (IBindVar loc) argns)))
+                                (IHole loc rhshole)
+             let Just nidx = getNameID n (gamma defs)
+                 | Nothing => throw (UndefinedName loc n)
+             cs' <- mkSplits loc opts nidx initcs
+             -- restore the global state, given that we've fiddled with it a lot!
+             put Ctxt defs
+             put MD meta
+             put UST ust
+             pure (map (\c => (loc, c)) cs'))
+         noResult
 
 export
 makeDef : {auto c : Ref Ctxt Defs} ->
@@ -199,28 +233,9 @@ makeDef p n
             | Nothing => noResult
          n <- getFullName nidx
          logTerm 5 ("Searching for " ++ show n) ty
-         tryUnify
-           (do defs <- branch
-               meta <- get MD
-               ust <- get UST
-               argns <- getEnvArgNames defs envlen !(nf defs [] ty)
-               -- Need to add implicit patterns for the outer environment.
-               -- We won't try splitting on these
-               let pre_env = replicate envlen (Implicit loc True)
-
-               rhshole <- uniqueName defs [] (fnName False n ++ "_rhs")
-               let initcs = PatClause loc
-                                  (apply (IVar loc n) (pre_env ++ (map (IBindVar loc) argns)))
-                                  (IHole loc rhshole)
-               let Just nidx = getNameID n (gamma defs)
-                   | Nothing => throw (UndefinedName loc n)
-               cs' <- mkSplits loc nidx initcs
-               -- restore the global state, given that we've fiddled with it a lot!
-               put Ctxt defs
-               put MD meta
-               put UST ust
-               pure (map (\c => (loc, c)) cs'))
-           noResult
+         let opts = record { genExpr = Just (makeDefFromType loc) }
+                           (initSearchOpts True 5)
+         makeDefFromType loc opts n envlen ty
 
 -- Given a clause, return the bindable names, and the ones that were used in
 -- the rhs

src/Yaffle/REPL.idr

@@ -77,9 +77,7 @@ process (ExprSearch n_in)
               | [] => throw (UndefinedName toplevelFC n_in)
               | ns => throw (AmbiguousName toplevelFC (map fst ns))
          results <- exprSearchN toplevelFC 1 n []
-         defs <- get Ctxt
-         defnfs <- traverse (normaliseHoles defs []) results
-         traverse_ (\d => coreLift (printLn !(toFullNames d))) defnfs
+         traverse_ (\d => coreLift (printLn d)) results
          pure True
 process (GenerateDef line name)
     = do defs <- get Ctxt

tests/Main.idr

@@ -57,7 +57,8 @@ idrisTests
        "interactive001", "interactive002", "interactive003", "interactive004",
        "interactive005", "interactive006", "interactive007", "interactive008",
        "interactive009", "interactive010", "interactive011", "interactive012",
-       "interactive013", "interactive014", "interactive015",
+       "interactive013", "interactive014", "interactive015", "interactive016",
+       "interactive017",
        -- Interfaces
        "interface001", "interface002", "interface003", "interface004",
        "interface005", "interface006", "interface007", "interface008",

tests/idris2/basic016/expected

@@ -1,6 +1,6 @@
 1/1: Building Eta (Eta.idr)
 Eta.idr:14:10--14:14:While processing right hand side of etaBad at Eta.idr:14:1--15:1:
-When unifying \x => (\y => (MkTest ?_ ?_)) = \x => (\y => (MkTest ?_ ?_)) and MkTest = \x => (\y => (MkTest ?_ ?_))
+When unifying \x => \y => MkTest ?_ ?_ = \x => \y => MkTest ?_ ?_ and MkTest = \x => \y => MkTest ?_ ?_
 Mismatch between:
 	Nat
 and
@@ -11,7 +11,7 @@ at:
 
 1/1: Building Eta2 (Eta2.idr)
 Eta2.idr:2:8--2:12:While processing right hand side of test at Eta2.idr:2:1--4:1:
-When unifying \x => (S ?_) = \x => (S ?_) and S = \x => (S ?_)
+When unifying \x => S ?_ = \x => S ?_ and S = \x => S ?_
 Mismatch between:
 	a
 and
@@ -21,7 +21,7 @@ at:
 	       ^^^^
 
 Eta2.idr:5:44--5:48:While processing right hand side of test2 at Eta2.idr:5:1--6:1:
-When unifying \x => (S ?_) = \x => (S ?_) and S = \x => (S ?_)
+When unifying \x => S ?_ = \x => S ?_ and S = \x => S ?_
 Mismatch between:
 	a
 and

tests/idris2/basic019/expected

@@ -4,5 +4,5 @@ Main> Prelude.elem : Eq a => a -> List a -> Bool
 elem x [] = False
 elem x (y :: ys) = (x == y) || Delay (elem x ys)
 Main> PrimIO.io_bind : (1 _ : IO a) -> (1 _ : (a -> IO b)) -> IO b
-io_bind (MkIO fn) k = MkIO (\1 w => (case fn w of { MkIORes x' w' => case k x' of { MkIO res => res w' } }))
+io_bind (MkIO fn) k = MkIO (\1 w => let MkIORes x' w' = fn w in let MkIO res = k x' in res w')
 Main> Bye for now!

tests/idris2/basic023/expected

@@ -3,7 +3,7 @@ Main> Main.Dict : (a -> a -> Bool) -> Type -> Type
 Main> Main.MkDict : (eq : (a -> a -> Bool)) -> List (a, b) -> Dict eq b
 Main> Main.lookup : (a -> a -> Bool) -> a -> List (a, b) -> Maybe b
 Main> Main.lookupK : (eq : (a -> a -> Bool)) -> a -> Dict eq b -> Maybe b
-Main> MkDict (\{arg:0} => (\{arg:1} => (intToBool (prim__eq_Int arg arg)))) [(0, "foo"), (1, "bar")]
+Main> MkDict (\{arg:0} => \{arg:1} => intToBool (prim__eq_Int arg arg)) [(0, "foo"), (1, "bar")]
 Main> Just "bar"
 Main> Nothing
 Main> Bye for now!

tests/idris2/interactive009/expected

@@ -5,13 +5,13 @@ Main>               (True # d) => ?now_4
 Main>  0 m : Type -> Type
  1 d : Door Open
    x : Integer
- 0 r : Res Bool (\r => (Door (if r then Open else Closed)))
+ 0 r : Res Bool (\r => Door (if r then Open else Closed))
 -------------------------------------
 now_2 : Use Many m ()
 Main>  0 m : Type -> Type
  1 d : Door Closed
    x : Integer
- 0 r : Res Bool (\r => (Door (if r then Open else Closed)))
+ 0 r : Res Bool (\r => Door (if r then Open else Closed))
 -------------------------------------
 now_3 : Use Many m ()
 Main> Bye for now!

tests/idris2/interactive011/expected

@@ -1,6 +1,6 @@
 1/1: Building IEdit (IEdit.idr)
-Main> natElim p x f 0 = x
-natElim p x f (S k) = f k (natElim p x f k)
+Main> natElim p y f 0 = y
+natElim p y f (S k) = f k (natElim p y f k)
 Main> f k (natElim2 p x f k)
 Main> listElim p mnil mcons [] = mnil
 listElim p mnil mcons (x :: xs) = mcons x xs (listElim p mnil mcons xs)

tests/idris2/interactive016/Cont.idr

@@ -0,0 +1,11 @@
+data Cont : (r : Type) -> (a : Type) -> Type where
+     MkCont : ((k : a -> r) -> r) -> Cont r a
+
+data ContT : (r : Type) -> (m : Type -> Type) -> (a : Type) -> Type where
+     MkContT : ((k : a -> m r) -> m r) -> ContT r m a
+
+cbind : Cont r a -> (a -> Cont r b) -> Cont r b
+
+ctbind : ContT r m a -> (a -> ContT r m b) -> ContT r m b
+
+callCC : ((a -> ContT r m b) -> ContT r m a) -> ContT r m a

tests/idris2/interactive016/expected

@@ -0,0 +1,5 @@
+1/1: Building Cont (Cont.idr)
+Main> cbind (MkCont g) f = MkCont (\k => g (\x => let MkCont f1 = f x in f1 k))
+Main> ctbind (MkContT g) f = MkContT (\k => g (\x => let MkContT f1 = f x in f1 k))
+Main> callCC f = MkContT (\k => let MkContT g = f (\x => MkContT (\g => k x)) in g k)
+Main> Bye for now!

tests/idris2/interactive016/input

@@ -0,0 +1,4 @@
+:gd 7 cbind
+:gd 9 ctbind
+:gd 11 callCC
+:q

tests/idris2/interactive016/run

@@ -0,0 +1,3 @@
+$1 --no-banner Cont.idr < input
+
+rm -rf build

tests/idris2/interactive017/RLE.idr

@@ -0,0 +1,95 @@
+module RLE
+
+import Decidable.Equality
+
+rep : Nat -> a -> List a
+
+data RunLength : List a -> Type where
+     Empty : RunLength []
+     Run : (n : Nat) -> (x : a) -> (rest : RunLength more) ->
+           RunLength (rep n x ++ more)
+
+data Singleton : a -> Type where
+     Val : (x : a) -> Singleton x
+
+uncompress : RunLength xs -> Singleton xs
+
+
+
+
+
+
+
+
+
+
+
+
+{-
+
+rle : DecEq a => (xs : List a) -> RLE xs
+rle [] = Empty
+rle (x :: xs) with (rle xs)
+  rle (x :: []) | Empty = Run 1 x Empty
+  rle (x :: (rep n y ++ more)) | (Run n y comp) with (decEq x y)
+    rle (y :: (rep n y ++ more)) | (Run n y comp) | (Yes Refl)
+        = Run (S n) y comp
+    rle (x :: (rep n y ++ more)) | (Run n y comp) | (No contra)
+        = Run 1 x $ Run n y comp
+
+data Singleton : a -> Type where
+     Val : (x : a) -> Singleton x
+
+uncompress : RLE xs -> Singleton xs
+
+-- uncompress Empty = Val []
+-- uncompress (Run n x comp)
+--     = let Val rec = uncompress comp in
+--           Val (rep n x ++ rec)
+
+uncompressHelp : (x : a) -> RLE more -> (n : Nat) -> Singleton more -> Singleton (rep n x ++ more)
+uncompressHelp x comp n (Val _) = Val (rep n x ++ more)
+
+uncompress' : RLE xs -> Singleton xs
+uncompress' Empty = Val []
+uncompress' (Run n x comp)
+    = let rec = uncompress' comp in
+          uncompressHelp x comp n rec
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+{-
+rle [] = Empty
+rle (x :: xs) with (rle xs)
+  rle (x :: []) | Empty = Run 1 x Empty
+  rle (x :: (rep n y ++ more)) | (Run n y comp) with (decEq x y)
+    rle (y :: (rep n y ++ more)) | (Run n y comp) | (Yes Refl)
+        = Run (S n) y comp
+    rle (x :: (rep n y ++ more)) | (Run n y comp) | (No contra)
+        = Run 1 x $ Run n y comp
+
+uncompress Empty = Val []
+uncompress (Run n x comp)
+   = let Val uncomp = uncompress comp in
+         Val (rep n x ++ uncomp)
+-}
+-}

tests/idris2/interactive017/expected

@@ -0,0 +1,4 @@
+1/1: Building RLE (RLE.idr)
+RLE> uncompress Empty = Val []
+uncompress (Run n x rest) = let Val ys = uncompress rest in Val (rep n x ++ ys)
+RLE> Bye for now!

tests/idris2/interactive017/input

@@ -0,0 +1,2 @@
+:gd 15 uncompress
+:q

tests/idris2/interactive017/run

@@ -0,0 +1,3 @@
+$1 --no-banner RLE.idr < input
+
+rm -rf build

tests/idris2/literate006/expected

@@ -5,13 +5,13 @@ Main> >               (True # d) => ?now_4
 Main>  0 m : Type -> Type
  1 d : Door Open
    x : Integer
- 0 r : Res Bool (\r => (Door (if r then Open else Closed)))
+ 0 r : Res Bool (\r => Door (if r then Open else Closed))
 -------------------------------------
 now_2 : Use Many m ()
 Main>  0 m : Type -> Type
  1 d : Door Closed
    x : Integer
- 0 r : Res Bool (\r => (Door (if r then Open else Closed)))
+ 0 r : Res Bool (\r => Door (if r then Open else Closed))
 -------------------------------------
 now_3 : Use Many m ()
 Main> Bye for now!

tests/idris2/literate008/expected

@@ -1,6 +1,6 @@
 1/1: Building IEdit (IEdit.lidr)
-Main> > natElim p x f 0 = x
-> natElim p x f (S k) = f k (natElim p x f k)
+Main> > natElim p y f 0 = y
+> natElim p y f (S k) = f k (natElim p y f k)
 Main> f k (natElim2 p x f k)
 Main> > listElim p mnil mcons [] = mnil
 > listElim p mnil mcons (x :: xs) = mcons x xs (listElim p mnil mcons xs)

tests/idris2/pkg005/expected

@@ -1,7 +1,7 @@
 1/1: Building Foo (Foo.idr)
 Foo> Foo.hi : IO String
-Foo> MkIO (\1 w => (MkIORes "Hi!" w))
+Foo> MkIO (\1 w => MkIORes "Hi!" w)
 Foo> Bye for now!
 Foo> Foo.hi : IO String
-Foo> MkIO (\1 w => (MkIORes "Hi!" w))
+Foo> MkIO (\1 w => MkIORes "Hi!" w)
 Foo> Bye for now!