From df635cf8d7b56a070d845114fd62d38d0500e760 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Mon, 27 Jul 2020 13:45:10 +0100 Subject: [PATCH] Add :psnext and :gdnext at the REPL These continue the search from :ps and :gd next respectively, giving the next search result until there are no more results. Correspondingly, added ':proof-search-next' and ':generate-def-next' in IDE mode, which continue the search from the previous ':proof-search' and ':generate-def' respectively. --- CHANGELOG.md | 8 ++ src/Idris/IDEMode/Commands.idr | 4 + src/Idris/IDEMode/REPL.idr | 8 +- src/Idris/Parser.idr | 18 ++-- src/Idris/REPL.idr | 140 +++++++++++++++++--------- src/Idris/REPLOpts.idr | 16 ++- src/Idris/Syntax.idr | 6 +- src/TTImp/Interactive/ExprSearch.idr | 15 ++- tests/Main.idr | 2 +- tests/idris2/interactive015/IEdit.idr | 17 ++++ tests/idris2/interactive015/expected | 33 ++++++ tests/idris2/interactive015/input | 21 ++++ tests/idris2/interactive015/run | 3 + 13 files changed, 221 insertions(+), 70 deletions(-) create mode 100644 tests/idris2/interactive015/IEdit.idr create mode 100644 tests/idris2/interactive015/expected create mode 100644 tests/idris2/interactive015/input create mode 100755 tests/idris2/interactive015/run diff --git a/CHANGELOG.md b/CHANGELOG.md index bedf9e2fe..76040f1db 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -63,6 +63,14 @@ REPL changes: * Implemented `:module` command, to load a module during a REPL session. * Implemented `:doc`, which displays documentation for a name. * Implemented `:browse`, which lists the names exported by a namespace. +* Added `:psnext`, which continues the previous proof search, looking for the + next type correct expression + + Correspondingly, added the IDE mode command `proof-search-next` (which takes + no arguments) +* Added `:gdnext`, which continues the previous program search, looking for the + next type correct implementation + + Correspondingly, added the IDE mode command `generate-def-next` (which takes + no arguments) Changes since Idris 2 v0.1.0 ---------------------------- diff --git a/src/Idris/IDEMode/Commands.idr b/src/Idris/IDEMode/Commands.idr index ebccc8097..f00348072 100644 --- a/src/Idris/IDEMode/Commands.idr +++ b/src/Idris/IDEMode/Commands.idr @@ -29,7 +29,9 @@ data IDECommand -- deprecated: | AddProofClause | AddMissing Integer String | ExprSearch Integer String (List String) Bool + | ExprSearchNext | GenerateDef Integer String + | GenerateDefNext | MakeLemma Integer String | MakeCase Integer String | MakeWith Integer String @@ -150,7 +152,9 @@ putIDECommand (ExprSearch line n exprs mode) = (SExpList [SymbolAtom "proof-sea getMode : Bool -> SExp getMode True = SymbolAtom "all" getMode False = SymbolAtom "other" +putIDECommand ExprSearchNext = SymbolAtom "proof-search--next" putIDECommand (GenerateDef line n) = (SExpList [SymbolAtom "generate-def", IntegerAtom line, StringAtom n]) +putIDECommand GenerateDefNext = SymbolAtom "generate-def-next" putIDECommand (MakeLemma line n) = (SExpList [SymbolAtom "make-lemma", IntegerAtom line, StringAtom n]) putIDECommand (MakeCase line n) = (SExpList [SymbolAtom "make-case", IntegerAtom line, StringAtom n]) putIDECommand (MakeWith line n) = (SExpList [SymbolAtom "make-with", IntegerAtom line, StringAtom n]) diff --git a/src/Idris/IDEMode/REPL.idr b/src/Idris/IDEMode/REPL.idr index c332e659e..63fd57add 100644 --- a/src/Idris/IDEMode/REPL.idr +++ b/src/Idris/IDEMode/REPL.idr @@ -168,9 +168,13 @@ process (AddMissing l n) pure $ REPL $ Edited $ DisplayEdit [] process (ExprSearch l n hs all) = replWrap $ Idris.REPL.process (Editing (ExprSearch False (fromInteger l) (UN n) - (map UN hs) all)) + (map UN hs))) +process ExprSearchNext + = replWrap $ Idris.REPL.process (Editing ExprSearchNext) process (GenerateDef l n) - = replWrap $ Idris.REPL.process (Editing (GenerateDef False (fromInteger l) (UN n) False)) + = replWrap $ Idris.REPL.process (Editing (GenerateDef False (fromInteger l) (UN n))) +process GenerateDefNext + = replWrap $ Idris.REPL.process (Editing GenerateDefNext) process (MakeLemma l n) = replWrap $ Idris.REPL.process (Editing (MakeLemma False (fromInteger l) (UN n))) process (MakeCase l n) diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index 577d6f263..7cabd8fd9 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -1710,22 +1710,16 @@ editCmd upd <- option False (do symbol "!"; pure True) line <- intLit n <- name - pure (ExprSearch upd (fromInteger line) n [] False) - <|> do replCmd ["psall"] - upd <- option False (do symbol "!"; pure True) - line <- intLit - n <- name - pure (ExprSearch upd (fromInteger line) n [] True) + pure (ExprSearch upd (fromInteger line) n []) + <|> do replCmd ["psnext"] + pure ExprSearchNext <|> do replCmd ["gd"] upd <- option False (do symbol "!"; pure True) line <- intLit n <- name - pure (GenerateDef upd (fromInteger line) n False) - <|> do replCmd ["gdall"] - upd <- option False (do symbol "!"; pure True) - line <- intLit - n <- name - pure (GenerateDef upd (fromInteger line) n True) + pure (GenerateDef upd (fromInteger line) n) + <|> do replCmd ["gdnext"] + pure GenerateDefNext <|> do replCmd ["ml", "makelemma"] upd <- option False (do symbol "!"; pure True) line <- intLit diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr index 87a5e3661..72dd699ea 100644 --- a/src/Idris/REPL.idr +++ b/src/Idris/REPL.idr @@ -293,6 +293,43 @@ addMadeCase lit wapp line content addW (S k) acc (x :: xs) = addW k (x :: acc) xs addW (S k) acc [] = reverse acc +nextProofSearch : {auto c : Ref Ctxt Defs} -> + {auto u : Ref UST UState} -> + {auto o : Ref ROpts REPLOpts} -> + Core (Maybe (Name, ClosedTerm)) +nextProofSearch + = do opts <- get ROpts + let Just (n, res) = psResult opts + | Nothing => pure Nothing + Just (res, next) <- nextResult res + | Nothing => + do put ROpts (record { psResult = Nothing } opts) + pure Nothing + put ROpts (record { psResult = Just (n, next) } opts) + pure (Just (n, res)) + +nextGenDef : {auto c : Ref Ctxt Defs} -> + {auto u : Ref UST UState} -> + {auto o : Ref ROpts REPLOpts} -> + Core (Maybe (Int, (FC, List ImpClause))) +nextGenDef + = do opts <- get ROpts + let Just (line, res) = gdResult opts + | Nothing => pure Nothing + Just (res, next) <- nextResult res + | Nothing => + do put ROpts (record { gdResult = Nothing } opts) + pure Nothing + put ROpts (record { gdResult = Just (line, next) } opts) + pure (Just (line, res)) + +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)) + processEdit : {auto c : Ref Ctxt Defs} -> {auto u : Ref UST UState} -> {auto s : Ref Syn SyntaxInfo} -> @@ -330,30 +367,27 @@ processEdit (AddClause upd line name) if upd then updateFile (addClause c (integerToNat (cast line))) else pure $ DisplayEdit [c] -processEdit (ExprSearch upd line name hints all) +processEdit (ExprSearch upd line name hints) = do defs <- get Ctxt syn <- get Syn let brack = elemBy (\x, y => dropNS x == dropNS y) name (bracketholes syn) case !(lookupDefName name (gamma defs)) of [(n, nidx, Hole locs _)] => - do tms <- exprSearchN replFC (if all then 20 else 1) name [] + do let searchtm = exprSearch replFC name [] + ropts <- get ROpts + put ROpts (record { psResult = Just (name, searchtm) } ropts) defs <- get Ctxt - restms <- traverse (normaliseHoles defs []) tms - itms <- the (Core (List PTerm)) - (traverse (\tm => - do let (_ ** (env, tm')) = dropLams locs [] tm - resugar env tm') restms) - if all - then pure $ DisplayEdit (map show itms) - else case itms of - [] => pure $ EditError "No search results" - (x :: xs) => - let res = show (the PTerm (if brack - then addBracket replFC x - else x)) in - if upd - then updateFile (proofSearch name res (integerToNat (cast (line - 1)))) - else pure $ DisplayEdit [res] + Just (_, tm) <- nextProofSearch + | Nothing => pure $ EditError "No search results" + restm <- normaliseHoles defs [] tm + let (_ ** (env, tm')) = dropLams locs [] restm + itm <- resugar env tm' + let res = show (the PTerm (if brack + then addBracket replFC itm + else itm)) + if upd + then updateFile (proofSearch name res (integerToNat (cast (line - 1)))) + else pure $ DisplayEdit [res] [(n, nidx, PMDef pi [] (STerm _ tm) _ _)] => case holeInfo pi of NotHole => pure $ EditError "Not a searchable hole" @@ -368,43 +402,52 @@ processEdit (ExprSearch upd line name hints all) else pure $ DisplayEdit [res] [] => pure $ EditError $ "Unknown name " ++ show name _ => pure $ EditError "Not a searchable hole" - where - 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)) -processEdit (GenerateDef upd line name all) +processEdit ExprSearchNext + = do defs <- get Ctxt + syn <- get Syn + Just (name, tm) <- 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 res = show (the PTerm (if brack + then addBracket replFC itm + else itm)) + pure $ DisplayEdit [res] + +processEdit (GenerateDef upd line name) = do defs <- get Ctxt Just (_, n', _, _) <- findTyDeclAt (\p, n => onLine (line - 1) p) | Nothing => pure (EditError ("Can't find declaration for " ++ show name ++ " on line " ++ show line)) case !(lookupDefExact n' (gamma defs)) of Just None => - handleUnify - (do progs <- makeDefN (\p, n => onLine (line - 1) p) - (if all then 20 else 1) - n' - Just srcLine <- getSourceLine line - | Nothing => pure (EditError "Source line not found") - let (markM, srcLineUnlit) = isLitLine srcLine - if all - then do ls <- traverse (\ (fc, cs) => - do let l : Nat = integerToNat (cast (snd (startPos fc))) - res <- traverse (printClause markM l) cs - pure (res ++ ["----"])) progs - pure $ DisplayEdit (concat ls) - else case progs of - [] => pure (EditError "No search results") - ((fc, cs) :: _) => - do let l : Nat = integerToNat (cast (snd (startPos fc))) - ls <- traverse (printClause markM l) cs - if upd - then updateFile (addClause (unlines ls) (integerToNat (cast line))) - else pure $ DisplayEdit ls) - (\err => pure $ EditError $ "Can't find a definition for " ++ show n' ++ ": " ++ show err) + do let searchdef = makeDef (\p, n => onLine (line - 1) p) n' + ropts <- get ROpts + put ROpts (record { gdResult = Just (line, searchdef) } ropts) + Just (_, (fc, cs)) <- nextGenDef + | Nothing => pure (EditError "No search results") + let l : Nat = integerToNat (cast (snd (startPos fc))) + Just srcLine <- getSourceLine line + | Nothing => pure (EditError "Source line not found") + let (markM, srcLineUnlit) = isLitLine srcLine + ls <- traverse (printClause markM l) cs + if upd + then updateFile (addClause (unlines ls) (integerToNat (cast line))) + else pure $ DisplayEdit ls Just _ => pure $ EditError "Already defined" Nothing => pure $ EditError $ "Can't find declaration for " ++ show name +processEdit GenerateDefNext + = do Just (line, (fc, cs)) <- nextGenDef + | Nothing => pure (EditError "No more results") + let l : Nat = integerToNat (cast (snd (startPos fc))) + Just srcLine <- getSourceLine line + | Nothing => pure (EditError "Source line not found") + let (markM, srcLineUnlit) = isLitLine srcLine + ls <- traverse (printClause markM l) cs + pure $ DisplayEdit ls processEdit (MakeLemma upd line name) = do defs <- get Ctxt syn <- get Syn @@ -550,6 +593,7 @@ loadMainFile f errs <- logTime "Build deps" $ buildDeps f updateErrorLine errs setSource res + resetProofState case errs of [] => pure (FileLoaded f) _ => pure (ErrorsBuildingFile f errs) diff --git a/src/Idris/REPLOpts.idr b/src/Idris/REPLOpts.idr index b0df2dc07..513162009 100644 --- a/src/Idris/REPLOpts.idr +++ b/src/Idris/REPLOpts.idr @@ -3,6 +3,8 @@ module Idris.REPLOpts import Compiler.Common import Idris.Syntax import Parser.Unlit +import TTImp.Interactive.ExprSearch +import TTImp.TTImp import Data.List import Data.Strings @@ -27,15 +29,17 @@ record REPLOpts where errorLine : Maybe Int idemode : OutputMode currentElabSource : String + psResult : Maybe (Name, Core (Search ClosedTerm)) -- 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. extraCodegens : List (String, Codegen) - export defaultOpts : Maybe String -> OutputMode -> List (String, Codegen) -> REPLOpts defaultOpts fname outmode cgs - = MkREPLOpts False NormaliseAll fname (litStyle fname) "" "vim" Nothing outmode "" cgs + = MkREPLOpts False NormaliseAll fname (litStyle fname) "" "vim" + Nothing outmode "" Nothing Nothing cgs where litStyle : Maybe String -> Maybe LiterateStyle litStyle Nothing = Nothing @@ -72,6 +76,14 @@ setMainFile src litStyle Nothing = Nothing litStyle (Just fn) = isLitFile fn +export +resetProofState : {auto o : Ref ROpts REPLOpts} -> + Core () +resetProofState + = do opts <- get ROpts + put ROpts (record { psResult = Nothing, + gdResult = Nothing } opts) + export setSource : {auto o : Ref ROpts REPLOpts} -> String -> Core () diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr index 84da61c5a..3fbaeaccc 100644 --- a/src/Idris/Syntax.idr +++ b/src/Idris/Syntax.idr @@ -384,8 +384,10 @@ data EditCmd : Type where TypeAt : Int -> Int -> Name -> EditCmd CaseSplit : Bool -> Int -> Int -> Name -> EditCmd AddClause : Bool -> Int -> Name -> EditCmd - ExprSearch : Bool -> Int -> Name -> List Name -> Bool -> EditCmd - GenerateDef : Bool -> Int -> Name -> Bool -> EditCmd + ExprSearch : Bool -> Int -> Name -> List Name -> EditCmd + ExprSearchNext : EditCmd + GenerateDef : Bool -> Int -> Name -> EditCmd + GenerateDefNext : EditCmd MakeLemma : Bool -> Int -> Name -> EditCmd MakeCase : Bool -> Int -> Name -> EditCmd MakeWith : Bool -> Int -> Name -> EditCmd diff --git a/src/TTImp/Interactive/ExprSearch.idr b/src/TTImp/Interactive/ExprSearch.idr index 0d6b08a6c..1409cbbe8 100644 --- a/src/TTImp/Interactive/ExprSearch.idr +++ b/src/TTImp/Interactive/ExprSearch.idr @@ -87,13 +87,11 @@ filterS p (Result r next) export searchN : {auto c : Ref Ctxt Defs} -> - {auto m : Ref MD Metadata} -> {auto u : Ref UST UState} -> Nat -> Core (Search a) -> Core (List a) searchN max s = tryUnify - (do foo <- getNextEntry - res <- s + (do res <- s xs <- count max res pure xs) (pure []) @@ -104,6 +102,17 @@ searchN max s count (S Z) (Result a next) = pure [a] count (S k) (Result a next) = pure $ a :: !(count k !next) +export +nextResult : {auto c : Ref Ctxt Defs} -> + {auto u : Ref UST UState} -> + Core (Search a) -> Core (Maybe (a, Core (Search a))) +nextResult s + = tryUnify + (do res <- s + case res of + NoMore => pure Nothing + Result r next => pure (Just (r, next))) + (pure Nothing) search : {auto c : Ref Ctxt Defs} -> {auto m : Ref MD Metadata} -> diff --git a/tests/Main.idr b/tests/Main.idr index 70b70d47c..d0f4a300f 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -57,7 +57,7 @@ idrisTests "interactive001", "interactive002", "interactive003", "interactive004", "interactive005", "interactive006", "interactive007", "interactive008", "interactive009", "interactive010", "interactive011", "interactive012", - "interactive013", "interactive014", + "interactive013", "interactive014", "interactive015", -- Interfaces "interface001", "interface002", "interface003", "interface004", "interface005", "interface006", "interface007", "interface008", diff --git a/tests/idris2/interactive015/IEdit.idr b/tests/idris2/interactive015/IEdit.idr new file mode 100644 index 000000000..64ff35659 --- /dev/null +++ b/tests/idris2/interactive015/IEdit.idr @@ -0,0 +1,17 @@ +data Vect : Nat -> Type -> Type where + Nil : Vect Z a + (::) : a -> Vect k a -> Vect (S k) a + +%name Vect xs, ys, zs + +my_cong : forall f . (x : a) -> (y : a) -> x = y -> f x = f y + +append : Vect n a -> Vect m a -> Vect (n + m) a + +lappend : (1 _ : List a) -> (1 _ : List a) -> List a + +lappend1 : List a -> List a -> List a + +lappend2 : List a -> List a -> List a +lappend2 [] ys = ?lappend2_rhs_1 +lappend2 (x :: xs) ys = ?lappend2_rhs_2 diff --git a/tests/idris2/interactive015/expected b/tests/idris2/interactive015/expected new file mode 100644 index 000000000..017ac55b5 --- /dev/null +++ b/tests/idris2/interactive015/expected @@ -0,0 +1,33 @@ +1/1: Building IEdit (IEdit.idr) +Main> my_cong x x Refl = Refl +Main> No more results +Main> append [] ys = ys +append (x :: xs) ys = x :: append xs ys +Main> append [] ys = ys +append (x :: xs) [] = x :: append xs [] +append (x :: xs) (y :: ys) = x :: append xs (x :: ys) +Main> lappend [] ys = ys +lappend (x :: xs) ys = x :: lappend xs ys +Main> lappend [] ys = ys +lappend (x :: xs) ys = x :: lappend ys xs +Main> lappend [] ys = ys +lappend (x :: xs) ys = lappend xs (x :: ys) +Main> lappend1 xs ys = ys +Main> lappend1 xs ys = xs +Main> lappend1 xs ys = [] +Main> lappend1 [] ys = ys +lappend1 (x :: xs) ys = xs +Main> lappend1 [] ys = ys +lappend1 (x :: xs) ys = ys +Main> lappend1 [] ys = ys +lappend1 (x :: xs) ys = [] +Main> lappend1 [] ys = ys +lappend1 (x :: xs) ys = x :: lappend1 xs xs +Main> lappend1 [] ys = ys +lappend1 (x :: xs) ys = x :: lappend1 xs ys +Main> ys +Main> [] +Main> lappend2 ys ys +Main> lappend2 ys [] +Main> lappend2 [] ys +Main> Bye for now! diff --git a/tests/idris2/interactive015/input b/tests/idris2/interactive015/input new file mode 100644 index 000000000..a0b11b195 --- /dev/null +++ b/tests/idris2/interactive015/input @@ -0,0 +1,21 @@ +:gd 7 my_cong +:gdnext +:gd 9 append +:gdnext +:gd 11 lappend +:gdnext +:gdnext +:gd 13 lappend1 +:gdnext +:gdnext +:gdnext +:gdnext +:gdnext +:gdnext +:gdnext +:ps 16 lappend2_rhs_1 +:psnext +:psnext +:psnext +:psnext +:q diff --git a/tests/idris2/interactive015/run b/tests/idris2/interactive015/run new file mode 100755 index 000000000..95e2e7edc --- /dev/null +++ b/tests/idris2/interactive015/run @@ -0,0 +1,3 @@ +$1 --no-banner IEdit.idr < input + +rm -rf build