idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-18 00:31:57 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #498 from edwinb/search-stuff

Browse Source 
More search improvements
This commit is contained in:
Edwin Brady 2020-07-27 14:14:59 +01:00 committed by GitHub
commit 3a0a566607
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
15 changed files with 354 additions and 123 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
CHANGELOG.md
View File

@ -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
----------------------------

4
src/Idris/IDEMode/Commands.idr
View File

@ -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])

6
src/Idris/IDEMode/REPL.idr
View File

@ -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)))
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)

11
src/Idris/Parser.idr
View File

@ -1710,17 +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)
<|> do replCmd ["gdnext"]
pure GenerateDefNext
<|> do replCmd ["ml", "makelemma"]
upd <- option False (do symbol "!"; pure True)
line <- intLit

128
src/Idris/REPL.idr
View File

@ -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 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,33 +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 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 Just (fc, cs) <- makeDef (\p, n => onLine (line - 1) p) n'
| Nothing => pure $ EditError $ "Can't find a definition for " ++ show n'
Just srcLine <- getSourceLine line
| Nothing => pure (EditError "Source line not found")
let (markM, srcLineUnlit) = isLitLine srcLine
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
@ -540,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)

16
src/Idris/REPLOpts.idr
View File

@ -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 ()

4
src/Idris/Syntax.idr
View File

@ -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
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

140
src/TTImp/Interactive/ExprSearch.idr
View File

@ -42,6 +42,7 @@ record SearchOpts where
holesOK : Bool
recOK : Bool
depth : Nat
inArg : Bool
export
data Search : Type -> Type where
@ -62,6 +63,10 @@ export
one : a -> Core (Search a)
one res = pure $ Result res (pure NoMore)
export
noResult : Core (Search a)
noResult = pure NoMore
export
traverse : (a -> Core b) -> Search a -> Core (Search b)
traverse f NoMore = pure NoMore
@ -80,6 +85,35 @@ filterS p (Result r next)
then pure $ Result r fnext
else fnext
export
searchN : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
Nat -> Core (Search a) -> Core (List a)
searchN max s
= tryUnify
(do res <- s
xs <- count max res
pure xs)
(pure [])
where
count : Nat -> Search a -> Core (List a)
count k NoMore = pure []
count Z _ = pure []
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} ->
{auto u : Ref UST UState} ->
@ -111,17 +145,18 @@ searchIfHole : {vars : _} ->
Core (Search (Term vars))
searchIfHole fc opts defining topty env arg
= case depth opts of
Z => pure NoMore
Z => noResult
S k =>
do let hole = holeID arg
let rig = argRig arg
defs <- get Ctxt
Just gdef <- lookupCtxtExact (Resolved hole) (gamma defs)
| Nothing => pure NoMore
| Nothing => noResult
let Hole _ _ = definition gdef
| _ => one !(normaliseHoles defs env (metaApp arg))
-- already solved
res <- search fc rig (record { depth = k} opts)
res <- search fc rig (record { depth = k,
inArg = True } opts)
defining 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
@ -137,9 +172,9 @@ explicit ai
firstSuccess : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
List (Core (Search (Term vars))) ->
Core (Search (Term vars))
firstSuccess [] = pure NoMore
List (Core (Search a)) ->
Core (Search a)
firstSuccess [] = noResult
firstSuccess (elab :: elabs)
= do ust <- get UST
defs <- get Ctxt
@ -148,13 +183,39 @@ firstSuccess (elab :: elabs)
pure (Result res (continue ust defs (more :: elabs))))
(\err => continue ust defs elabs)
where
continue : UState -> Defs -> List (Core (Search (Term vars))) ->
Core (Search (Term vars))
continue : UState -> Defs -> List (Core (Search a)) ->
Core (Search a)
continue ust defs elabs
= do put UST ust
put Ctxt defs
firstSuccess elabs
export
trySearch : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
Core (Search a) ->
Core (Search a) ->
Core (Search a)
trySearch s1 s2 = firstSuccess [s1, s2]
export
combine : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
(a -> b -> t) -> Search a -> Search b -> Core (Search t)
combine f NoMore y = pure NoMore
combine f (Result x next) NoMore = pure NoMore
combine f (Result x nextx) (Result y nexty)
= pure $ Result (f x y) $
(do nexty' <- nexty
combine f !(one x) nexty')
`trySearch`
((do nextx' <- nextx
combine f nextx' !(one y))
`trySearch`
(do nextx' <- nextx
nexty' <- nexty
combine f nextx' nexty'))
mkCandidates : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
@ -163,7 +224,7 @@ mkCandidates : {vars : _} ->
-- out of arguments, we have a candidate
mkCandidates fc f [] = one f
-- argument has run out of ideas, we're stuck
mkCandidates fc f (NoMore :: argss) = pure NoMore
mkCandidates fc f (NoMore :: argss) = noResult
-- make a candidate from 'f arg' applied to the rest of the arguments
mkCandidates fc f (Result arg next :: argss)
= firstSuccess
@ -185,7 +246,7 @@ searchName fc rigc opts env target topty defining (n, ndef)
= do defs <- get Ctxt
let True = visibleInAny (!getNS :: !getNestedNS)
(fullname ndef) (visibility ndef)
| _ => pure NoMore
| _ => noResult
let ty = type ndef
let namety : NameType
= case definition ndef of
@ -199,7 +260,7 @@ searchName fc rigc opts env target topty defining (n, ndef)
logNF 10 "App type" env appTy
ures <- unify inSearch fc env target appTy
let [] = constraints ures
| _ => pure NoMore
| _ => noResult
-- Search the explicit arguments first, they may resolve other holes
traverse (searchIfHole fc opts defining topty env)
(filter explicit args)
@ -230,7 +291,7 @@ getSuccessful {vars} fc rig opts mkHole env ty topty defining all
(Hole (length env) (holeInit False))
False
one tm
else pure NoMore
else noResult
r => pure r
searchNames : {vars : _} ->
@ -241,7 +302,7 @@ searchNames : {vars : _} ->
Term vars -> ClosedTerm ->
Maybe RecData -> List Name -> Core (Search (Term vars))
searchNames fc rig opts env ty topty defining []
= pure NoMore
= noResult
searchNames fc rig opts env ty topty defining (n :: ns)
= do defs <- get Ctxt
vis <- traverse (visible (gamma defs) (currentNS defs :: nestedNS defs)) (n :: ns)
@ -268,11 +329,11 @@ tryRecursive : {vars : _} ->
Env Term vars -> Term vars -> ClosedTerm ->
Maybe RecData -> Core (Search (Term vars))
tryRecursive fc rig opts env ty topty Nothing
= pure NoMore
= noResult
tryRecursive fc rig opts env ty topty (Just rdata)
= do defs <- get Ctxt
case !(lookupCtxtExact (recname rdata) (gamma defs)) of
Nothing => pure NoMore
Nothing => noResult
Just def =>
do res <- searchName fc rig opts env !(nf defs env ty)
topty Nothing
@ -337,7 +398,7 @@ searchLocalWith : {vars : _} ->
Term vars -> ClosedTerm -> Maybe RecData ->
Core (Search (Term vars))
searchLocalWith fc rig opts env [] ty topty defining
= pure NoMore
= noResult
searchLocalWith {vars} fc rig opts env ((p, pty) :: rest) ty topty defining
= do defs <- get Ctxt
nty <- nf defs env ty
@ -364,11 +425,11 @@ searchLocalWith {vars} fc rig opts env ((p, pty) :: rest) ty topty defining
mkCandidates fc (f prf) [])
(do ures <- unify inTerm fc env ty appTy
let [] = constraints ures
| _ => pure NoMore
| _ => noResult
args' <- traverse (searchIfHole fc opts defining topty env)
args
mkCandidates fc (f prf) args')
else pure NoMore
else noResult
findPos : Defs -> Term vars ->
(Term vars -> Term vars) ->
@ -401,7 +462,7 @@ searchLocalWith {vars} fc rig opts env ((p, pty) :: rest) ty topty defining
ytytm,
f arg])
ytynf target)]
else pure NoMore)]
else noResult)]
findPos defs prf f nty target = findDirect defs prf f nty target
searchLocal : {vars : _} ->
@ -455,14 +516,22 @@ searchType fc rig opts env defining topty _ ty
-- Then try a recursive call
log 10 $ "Hints found for " ++ show n ++ " "
++ show allHints
getSuccessful fc rig opts True env ty topty defining
([searchLocal fc rig opts env ty topty defining,
searchNames fc rig opts env ty topty defining
allHints]
++ if recOK opts
then [tryRecursive fc rig opts env ty topty defining]
else [])
else pure NoMore
let tries =
[searchLocal fc rig opts env ty topty defining,
searchNames fc rig opts env ty topty defining allHints]
let tryRec =
if recOK opts
then [tryRecursive fc rig opts env ty topty defining]
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
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]
@ -522,7 +591,7 @@ getLHSData defs (Just tm) = pure $ getLHS !(normaliseHoles defs [] tm)
firstLinearOK : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
FC -> Search ClosedTerm -> Core (Search ClosedTerm)
firstLinearOK fc NoMore = pure NoMore
firstLinearOK fc NoMore = noResult
firstLinearOK fc (Result t next)
= tryUnify
(do linearCheck fc linear False [] t
@ -541,7 +610,7 @@ exprSearch fc n_in hints
| 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)
res <- search fc (multiplicity gdef) (MkSearchOpts False True 5 False)
!(getLHSData defs lhs) (type gdef) n
firstLinearOK fc res
where
@ -559,15 +628,4 @@ exprSearchN : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
FC -> Nat -> Name -> List Name -> Core (List ClosedTerm)
exprSearchN fc max n hints
= tryUnify
(do foo <- getNextEntry
res <- exprSearch fc n hints
xs <- count max res
pure xs)
(pure [])
where
count : Nat -> Search a -> Core (List a)
count k NoMore = pure []
count Z _ = pure []
count (S Z) (Result a next) = pure [a]
count (S k) (Result a next) = pure $ a :: !(count k !next)
= searchN max (exprSearch fc n hints)

78
src/TTImp/Interactive/GenerateDef.idr
View File

@ -53,12 +53,12 @@ expandClause : {auto c : Ref Ctxt Defs} ->
{auto m : Ref MD Metadata} ->
{auto u : Ref UST UState} ->
FC -> Int -> ImpClause ->
Core (List ImpClause)
Core (Search (List ImpClause))
expandClause loc n c
= do c <- uniqueRHS c
Right clause <- checkClause linear Private False n [] (MkNested []) [] c
| Left err => pure [] -- TODO: impossible clause, do something
-- appropriate
| Left err => noResult -- TODO: impossible clause, do something
-- appropriate
let MkClause {vars} env lhs rhs = clause
let Meta _ i fn _ = getFn rhs
@ -67,16 +67,16 @@ 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' :: _) <- exprSearchN loc 1 (Resolved fn) []
| _ => throw (GenericMsg loc "No result found for search on RHS")
defs <- get Ctxt
rhsnf <- normaliseHoles defs [] rhs'
let (_ ** (env', rhsenv)) = dropLams locs [] rhsnf
rhs' <- exprSearch loc (Resolved fn) []
traverse (\rhs' =>
do defs <- get Ctxt
rhsnf <- normaliseHoles defs [] rhs'
let (_ ** (env', rhsenv)) = dropLams locs [] rhsnf
rhsraw <- unelab env' rhsenv
logTermNF 5 "Got clause" env lhs
logTermNF 5 " = " env' rhsenv
pure [updateRHS c rhsraw]
rhsraw <- unelab env' rhsenv
logTermNF 5 "Got clause" env lhs
logTermNF 5 " = " env' rhsenv
pure [updateRHS c rhsraw]) rhs'
where
updateRHS : ImpClause -> RawImp -> ImpClause
updateRHS (PatClause fc lhs _) rhs = PatClause fc lhs rhs
@ -149,46 +149,54 @@ generateSplits {c} {m} {u} loc fn (PatClause fc lhs rhs)
(IBindHere loc PATTERN lhs) Nothing
traverse (trySplit fc lhs lhstm rhs) (splittableNames lhs)
collectClauses : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
List (Search (List ImpClause)) ->
Core (Search (List ImpClause))
collectClauses [] = one []
collectClauses (x :: xs)
= do xs' <- collectClauses xs
combine (++) x xs'
mutual
tryAllSplits : {auto c : Ref Ctxt Defs} ->
{auto m : Ref MD Metadata} ->
{auto u : Ref UST UState} ->
FC -> Int -> Error ->
FC -> Int ->
List (Name, List ImpClause) ->
Core (List ImpClause)
tryAllSplits loc n err [] = throw err
tryAllSplits loc n err ((x, []) :: rest)
= tryAllSplits loc n err rest
tryAllSplits loc n err ((x, cs) :: rest)
Core (Search (List ImpClause))
tryAllSplits loc n [] = noResult
tryAllSplits loc n ((x, []) :: rest)
= tryAllSplits loc n rest
tryAllSplits loc n ((x, cs) :: rest)
= do log 5 $ "Splitting on " ++ show x
tryUnify (do cs' <- traverse (mkSplits loc n) cs
pure (concat cs'))
(tryAllSplits loc n err rest)
trySearch (do cs' <- traverse (mkSplits loc n) cs
collectClauses cs')
(tryAllSplits loc n rest)
mkSplits : {auto c : Ref Ctxt Defs} ->
{auto m : Ref MD Metadata} ->
{auto u : Ref UST UState} ->
FC -> Int -> ImpClause ->
Core (List 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
= handleUnify
= trySearch
(expandClause loc n c)
(\err =>
do cs <- generateSplits loc n c
log 5 $ "Splits: " ++ show cs
tryAllSplits loc n err cs)
(do cs <- generateSplits loc n c
log 5 $ "Splits: " ++ show cs
tryAllSplits loc n cs)
export
makeDef : {auto c : Ref Ctxt Defs} ->
{auto m : Ref MD Metadata} ->
{auto u : Ref UST UState} ->
(FC -> (Name, Nat, ClosedTerm) -> Bool) ->
Name -> Core (Maybe (FC, List ImpClause))
Name -> Core (Search (FC, List ImpClause))
makeDef p n
= do Just (loc, nidx, envlen, ty) <- findTyDeclAt p
| Nothing => pure Nothing
| Nothing => noResult
n <- getFullName nidx
logTerm 5 ("Searching for " ++ show n) ty
tryUnify
@ -211,5 +219,13 @@ makeDef p n
put Ctxt defs
put MD meta
put UST ust
pure (Just (loc, cs')))
(pure Nothing)
pure (map (\c => (loc, c)) cs'))
noResult
export
makeDefN : {auto c : Ref Ctxt Defs} ->
{auto m : Ref MD Metadata} ->
{auto u : Ref UST UState} ->
(FC -> (Name, Nat, ClosedTerm) -> Bool) ->
Nat -> Name -> Core (List (FC, List ImpClause))
makeDefN p max n = searchN max (makeDef p n)

6
src/Yaffle/REPL.idr
View File

@ -89,9 +89,9 @@ process (GenerateDef line name)
case !(lookupDefExact n' (gamma defs)) of
Just None =>
catch
(do Just (fc, cs) <- logTime "Generation" $
makeDef (\p, n => onLine line p) n'
| Nothing => coreLift (putStrLn "Failed")
(do ((fc, cs) :: _) <- logTime "Generation" $
makeDefN (\p, n => onLine line p) 1 n'
| _ => coreLift (putStrLn "Failed")
coreLift $ putStrLn (show cs))
(\err => coreLift $ putStrLn $ "Can't find a definition for " ++ show n')
Just _ => coreLift $ putStrLn "Already defined"

2
tests/Main.idr
View File

@ -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",

17
tests/idris2/interactive015/IEdit.idr Normal file
View File

@ -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

33
tests/idris2/interactive015/expected Normal file
View File

@ -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!

21
tests/idris2/interactive015/input Normal file
View File

@ -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

3
tests/idris2/interactive015/run Executable file
View File

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