idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-09-21 02:07:25 +03:00
Code Issues Projects Releases Wiki Activity

Allow multiple results from generate-defs

Browse Source 
Return a 'Search' rather than a single definition. Also, change the
order of search in expressions so that we look at recursive calls
earlier when under a constructor - the assumption being that this is
more likely than nested constructors.
This commit is contained in:
Edwin Brady 2020-07-27 12:04:39 +01:00
parent c860e5e690
commit f8ef44f1b0
7 changed files with 167 additions and 87 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -170,7 +170,7 @@ process (ExprSearch l n hs all)
= replWrap $ Idris.REPL.process (Editing (ExprSearch False (fromInteger l) (UN n) = replWrap $ Idris.REPL.process (Editing (ExprSearch False (fromInteger l) (UN n)
(map UN hs) all)) (map UN hs) all))
process (GenerateDef l n) process (GenerateDef l n)
= replWrap $ Idris.REPL.process (Editing (GenerateDef False (fromInteger l) (UN n))) = replWrap $ Idris.REPL.process (Editing (GenerateDef False (fromInteger l) (UN n) False))
process (MakeLemma l n) process (MakeLemma l n)
= replWrap $ Idris.REPL.process (Editing (MakeLemma False (fromInteger l) (UN n))) = replWrap $ Idris.REPL.process (Editing (MakeLemma False (fromInteger l) (UN n)))
process (MakeCase l n) process (MakeCase l n)

7
src/Idris/Parser.idr
View File

@ -1720,7 +1720,12 @@ editCmd
upd <- option False (do symbol "!"; pure True) upd <- option False (do symbol "!"; pure True)
line <- intLit line <- intLit
n <- name n <- name
pure (GenerateDef upd (fromInteger line) n) 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)
<|> do replCmd ["ml", "makelemma"] <|> do replCmd ["ml", "makelemma"]
upd <- option False (do symbol "!"; pure True) upd <- option False (do symbol "!"; pure True)
line <- intLit line <- intLit

28
src/Idris/REPL.idr
View File

@ -336,7 +336,7 @@ processEdit (ExprSearch upd line name hints all)
let brack = elemBy (\x, y => dropNS x == dropNS y) name (bracketholes syn) let brack = elemBy (\x, y => dropNS x == dropNS y) name (bracketholes syn)
case !(lookupDefName name (gamma defs)) of case !(lookupDefName name (gamma defs)) of
[(n, nidx, Hole locs _)] => [(n, nidx, Hole locs _)] =>
do tms <- exprSearchN replFC 1 name [] do tms <- exprSearchN replFC (if all then 20 else 1) name []
defs <- get Ctxt defs <- get Ctxt
restms <- traverse (normaliseHoles defs []) tms restms <- traverse (normaliseHoles defs []) tms
itms <- the (Core (List PTerm)) itms <- the (Core (List PTerm))
@ -375,23 +375,33 @@ processEdit (ExprSearch upd line name hints all)
dropLams Z env tm = (_ ** (env, tm)) dropLams Z env tm = (_ ** (env, tm))
dropLams (S k) env (Bind _ _ b sc) = dropLams k (b :: env) sc dropLams (S k) env (Bind _ _ b sc) = dropLams k (b :: env) sc
dropLams _ env tm = (_ ** (env, tm)) dropLams _ env tm = (_ ** (env, tm))
processEdit (GenerateDef upd line name) processEdit (GenerateDef upd line name all)
= do defs <- get Ctxt = do defs <- get Ctxt
Just (_, n', _, _) <- findTyDeclAt (\p, n => onLine (line - 1) p) Just (_, n', _, _) <- findTyDeclAt (\p, n => onLine (line - 1) p)
| Nothing => pure (EditError ("Can't find declaration for " ++ show name ++ " on line " ++ show line)) | Nothing => pure (EditError ("Can't find declaration for " ++ show name ++ " on line " ++ show line))
case !(lookupDefExact n' (gamma defs)) of case !(lookupDefExact n' (gamma defs)) of
Just None => Just None =>
handleUnify handleUnify
(do Just (fc, cs) <- makeDef (\p, n => onLine (line - 1) p) n' (do progs <- makeDefN (\p, n => onLine (line - 1) p)
| Nothing => pure $ EditError $ "Can't find a definition for " ++ show n' (if all then 20 else 1)
n'
Just srcLine <- getSourceLine line Just srcLine <- getSourceLine line
| Nothing => pure (EditError "Source line not found") | Nothing => pure (EditError "Source line not found")
let (markM, srcLineUnlit) = isLitLine srcLine let (markM, srcLineUnlit) = isLitLine srcLine
let l : Nat = integerToNat (cast (snd (startPos fc))) if all
ls <- traverse (printClause markM l) cs then do ls <- traverse (\ (fc, cs) =>
if upd do let l : Nat = integerToNat (cast (snd (startPos fc)))
then updateFile (addClause (unlines ls) (integerToNat (cast line))) res <- traverse (printClause markM l) cs
else pure $ DisplayEdit ls) 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) (\err => pure $ EditError $ "Can't find a definition for " ++ show n' ++ ": " ++ show err)
Just _ => pure $ EditError "Already defined" Just _ => pure $ EditError "Already defined"
Nothing => pure $ EditError $ "Can't find declaration for " ++ show name Nothing => pure $ EditError $ "Can't find declaration for " ++ show name

2
src/Idris/Syntax.idr
View File

@ -385,7 +385,7 @@ data EditCmd : Type where
CaseSplit : Bool -> Int -> Int -> Name -> EditCmd CaseSplit : Bool -> Int -> Int -> Name -> EditCmd
AddClause : Bool -> Int -> Name -> EditCmd AddClause : Bool -> Int -> Name -> EditCmd
ExprSearch : Bool -> Int -> Name -> List Name -> Bool -> EditCmd ExprSearch : Bool -> Int -> Name -> List Name -> Bool -> EditCmd
GenerateDef : Bool -> Int -> Name -> EditCmd GenerateDef : Bool -> Int -> Name -> Bool -> EditCmd
MakeLemma : Bool -> Int -> Name -> EditCmd MakeLemma : Bool -> Int -> Name -> EditCmd
MakeCase : Bool -> Int -> Name -> EditCmd MakeCase : Bool -> Int -> Name -> EditCmd
MakeWith : Bool -> Int -> Name -> EditCmd MakeWith : Bool -> Int -> Name -> EditCmd

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

@ -42,6 +42,7 @@ record SearchOpts where
holesOK : Bool holesOK : Bool
recOK : Bool recOK : Bool
depth : Nat depth : Nat
inArg : Bool
export export
data Search : Type -> Type where data Search : Type -> Type where
@ -62,6 +63,10 @@ export
one : a -> Core (Search a) one : a -> Core (Search a)
one res = pure $ Result res (pure NoMore) one res = pure $ Result res (pure NoMore)
export
noResult : Core (Search a)
noResult = pure NoMore
export export
traverse : (a -> Core b) -> Search a -> Core (Search b) traverse : (a -> Core b) -> Search a -> Core (Search b)
traverse f NoMore = pure NoMore traverse f NoMore = pure NoMore
@ -80,6 +85,26 @@ filterS p (Result r next)
then pure $ Result r fnext then pure $ Result r fnext
else fnext else fnext
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
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)
search : {auto c : Ref Ctxt Defs} -> search : {auto c : Ref Ctxt Defs} ->
{auto m : Ref MD Metadata} -> {auto m : Ref MD Metadata} ->
{auto u : Ref UST UState} -> {auto u : Ref UST UState} ->
@ -111,17 +136,18 @@ searchIfHole : {vars : _} ->
Core (Search (Term vars)) Core (Search (Term vars))
searchIfHole fc opts defining topty env arg searchIfHole fc opts defining topty env arg
= case depth opts of = case depth opts of
Z => pure NoMore Z => noResult
S k => S k =>
do let hole = holeID arg do let hole = holeID arg
let rig = argRig arg let rig = argRig arg
defs <- get Ctxt defs <- get Ctxt
Just gdef <- lookupCtxtExact (Resolved hole) (gamma defs) Just gdef <- lookupCtxtExact (Resolved hole) (gamma defs)
| Nothing => pure NoMore | Nothing => noResult
let Hole _ _ = definition gdef let Hole _ _ = definition gdef
| _ => one !(normaliseHoles defs env (metaApp arg)) | _ => one !(normaliseHoles defs env (metaApp arg))
-- already solved -- already solved
res <- search fc rig (record { depth = k} opts) res <- search fc rig (record { depth = k,
inArg = True } opts)
defining topty (Resolved hole) defining topty (Resolved hole)
-- When we solve an argument, we're also building a lambda -- When we solve an argument, we're also building a lambda
-- expression for its environment, so we need to apply it to -- expression for its environment, so we need to apply it to
@ -137,9 +163,9 @@ explicit ai
firstSuccess : {auto c : Ref Ctxt Defs} -> firstSuccess : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} -> {auto u : Ref UST UState} ->
List (Core (Search (Term vars))) -> List (Core (Search a)) ->
Core (Search (Term vars)) Core (Search a)
firstSuccess [] = pure NoMore firstSuccess [] = noResult
firstSuccess (elab :: elabs) firstSuccess (elab :: elabs)
= do ust <- get UST = do ust <- get UST
defs <- get Ctxt defs <- get Ctxt
@ -148,13 +174,39 @@ firstSuccess (elab :: elabs)
pure (Result res (continue ust defs (more :: elabs)))) pure (Result res (continue ust defs (more :: elabs))))
(\err => continue ust defs elabs) (\err => continue ust defs elabs)
where where
continue : UState -> Defs -> List (Core (Search (Term vars))) -> continue : UState -> Defs -> List (Core (Search a)) ->
Core (Search (Term vars)) Core (Search a)
continue ust defs elabs continue ust defs elabs
= do put UST ust = do put UST ust
put Ctxt defs put Ctxt defs
firstSuccess elabs 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 : _} -> mkCandidates : {vars : _} ->
{auto c : Ref Ctxt Defs} -> {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} -> {auto u : Ref UST UState} ->
@ -163,7 +215,7 @@ mkCandidates : {vars : _} ->
-- out of arguments, we have a candidate -- out of arguments, we have a candidate
mkCandidates fc f [] = one f mkCandidates fc f [] = one f
-- argument has run out of ideas, we're stuck -- 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 -- make a candidate from 'f arg' applied to the rest of the arguments
mkCandidates fc f (Result arg next :: argss) mkCandidates fc f (Result arg next :: argss)
= firstSuccess = firstSuccess
@ -185,7 +237,7 @@ searchName fc rigc opts env target topty defining (n, ndef)
= do defs <- get Ctxt = do defs <- get Ctxt
let True = visibleInAny (!getNS :: !getNestedNS) let True = visibleInAny (!getNS :: !getNestedNS)
(fullname ndef) (visibility ndef) (fullname ndef) (visibility ndef)
| _ => pure NoMore | _ => noResult
let ty = type ndef let ty = type ndef
let namety : NameType let namety : NameType
= case definition ndef of = case definition ndef of
@ -199,7 +251,7 @@ searchName fc rigc opts env target topty defining (n, ndef)
logNF 10 "App type" env appTy logNF 10 "App type" env appTy
ures <- unify inSearch fc env target appTy ures <- unify inSearch fc env target appTy
let [] = constraints ures let [] = constraints ures
| _ => pure NoMore | _ => noResult
-- Search the explicit arguments first, they may resolve other holes -- Search the explicit arguments first, they may resolve other holes
traverse (searchIfHole fc opts defining topty env) traverse (searchIfHole fc opts defining topty env)
(filter explicit args) (filter explicit args)
@ -230,7 +282,7 @@ getSuccessful {vars} fc rig opts mkHole env ty topty defining all
(Hole (length env) (holeInit False)) (Hole (length env) (holeInit False))
False False
one tm one tm
else pure NoMore else noResult
r => pure r r => pure r
searchNames : {vars : _} -> searchNames : {vars : _} ->
@ -241,7 +293,7 @@ searchNames : {vars : _} ->
Term vars -> ClosedTerm -> Term vars -> ClosedTerm ->
Maybe RecData -> List Name -> Core (Search (Term vars)) Maybe RecData -> List Name -> Core (Search (Term vars))
searchNames fc rig opts env ty topty defining [] searchNames fc rig opts env ty topty defining []
= pure NoMore = noResult
searchNames fc rig opts env ty topty defining (n :: ns) searchNames fc rig opts env ty topty defining (n :: ns)
= do defs <- get Ctxt = do defs <- get Ctxt
vis <- traverse (visible (gamma defs) (currentNS defs :: nestedNS defs)) (n :: ns) vis <- traverse (visible (gamma defs) (currentNS defs :: nestedNS defs)) (n :: ns)
@ -268,11 +320,11 @@ tryRecursive : {vars : _} ->
Env Term vars -> Term vars -> ClosedTerm -> Env Term vars -> Term vars -> ClosedTerm ->
Maybe RecData -> Core (Search (Term vars)) Maybe RecData -> Core (Search (Term vars))
tryRecursive fc rig opts env ty topty Nothing tryRecursive fc rig opts env ty topty Nothing
= pure NoMore = noResult
tryRecursive fc rig opts env ty topty (Just rdata) tryRecursive fc rig opts env ty topty (Just rdata)
= do defs <- get Ctxt = do defs <- get Ctxt
case !(lookupCtxtExact (recname rdata) (gamma defs)) of case !(lookupCtxtExact (recname rdata) (gamma defs)) of
Nothing => pure NoMore Nothing => noResult
Just def => Just def =>
do res <- searchName fc rig opts env !(nf defs env ty) do res <- searchName fc rig opts env !(nf defs env ty)
topty Nothing topty Nothing
@ -337,7 +389,7 @@ searchLocalWith : {vars : _} ->
Term vars -> ClosedTerm -> Maybe RecData -> Term vars -> ClosedTerm -> Maybe RecData ->
Core (Search (Term vars)) Core (Search (Term vars))
searchLocalWith fc rig opts env [] ty topty defining searchLocalWith fc rig opts env [] ty topty defining
= pure NoMore = noResult
searchLocalWith {vars} fc rig opts env ((p, pty) :: rest) ty topty defining searchLocalWith {vars} fc rig opts env ((p, pty) :: rest) ty topty defining
= do defs <- get Ctxt = do defs <- get Ctxt
nty <- nf defs env ty nty <- nf defs env ty
@ -364,11 +416,11 @@ searchLocalWith {vars} fc rig opts env ((p, pty) :: rest) ty topty defining
mkCandidates fc (f prf) []) mkCandidates fc (f prf) [])
(do ures <- unify inTerm fc env ty appTy (do ures <- unify inTerm fc env ty appTy
let [] = constraints ures let [] = constraints ures
| _ => pure NoMore | _ => noResult
args' <- traverse (searchIfHole fc opts defining topty env) args' <- traverse (searchIfHole fc opts defining topty env)
args args
mkCandidates fc (f prf) args') mkCandidates fc (f prf) args')
else pure NoMore else noResult
findPos : Defs -> Term vars -> findPos : Defs -> Term vars ->
(Term vars -> Term vars) -> (Term vars -> Term vars) ->
@ -401,7 +453,7 @@ searchLocalWith {vars} fc rig opts env ((p, pty) :: rest) ty topty defining
ytytm, ytytm,
f arg]) f arg])
ytynf target)] ytynf target)]
else pure NoMore)] else noResult)]
findPos defs prf f nty target = findDirect defs prf f nty target findPos defs prf f nty target = findDirect defs prf f nty target
searchLocal : {vars : _} -> searchLocal : {vars : _} ->
@ -455,14 +507,22 @@ searchType fc rig opts env defining topty _ ty
-- Then try a recursive call -- Then try a recursive call
log 10 $ "Hints found for " ++ show n ++ " " log 10 $ "Hints found for " ++ show n ++ " "
++ show allHints ++ show allHints
getSuccessful fc rig opts True env ty topty defining let tries =
([searchLocal fc rig opts env ty topty defining, [searchLocal fc rig opts env ty topty defining,
searchNames fc rig opts env ty topty defining searchNames fc rig opts env ty topty defining allHints]
allHints] let tryRec =
++ if recOK opts if recOK opts
then [tryRecursive fc rig opts env ty topty defining] then [tryRecursive fc rig opts env ty topty defining]
else []) else []
else pure NoMore -- 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 _ => do logTerm 10 "Searching locals only at" ty
getSuccessful fc rig opts True env ty topty defining getSuccessful fc rig opts True env ty topty defining
([searchLocal fc rig opts env ty topty defining] ([searchLocal fc rig opts env ty topty defining]
@ -522,7 +582,7 @@ getLHSData defs (Just tm) = pure $ getLHS !(normaliseHoles defs [] tm)
firstLinearOK : {auto c : Ref Ctxt Defs} -> firstLinearOK : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} -> {auto u : Ref UST UState} ->
FC -> Search ClosedTerm -> Core (Search ClosedTerm) FC -> Search ClosedTerm -> Core (Search ClosedTerm)
firstLinearOK fc NoMore = pure NoMore firstLinearOK fc NoMore = noResult
firstLinearOK fc (Result t next) firstLinearOK fc (Result t next)
= tryUnify = tryUnify
(do linearCheck fc linear False [] t (do linearCheck fc linear False [] t
@ -541,7 +601,7 @@ exprSearch fc n_in hints
| Nothing => throw (UndefinedName fc n_in) | Nothing => throw (UndefinedName fc n_in)
lhs <- findHoleLHS !(getFullName (Resolved idx)) lhs <- findHoleLHS !(getFullName (Resolved idx))
log 10 $ "LHS hole data " ++ show (n, lhs) 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 !(getLHSData defs lhs) (type gdef) n
firstLinearOK fc res firstLinearOK fc res
where where
@ -559,15 +619,4 @@ exprSearchN : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} -> {auto u : Ref UST UState} ->
FC -> Nat -> Name -> List Name -> Core (List ClosedTerm) FC -> Nat -> Name -> List Name -> Core (List ClosedTerm)
exprSearchN fc max n hints exprSearchN fc max n hints
= tryUnify = searchN max (exprSearch fc n hints)
(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)

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

@ -53,12 +53,12 @@ expandClause : {auto c : Ref Ctxt Defs} ->
{auto m : Ref MD Metadata} -> {auto m : Ref MD Metadata} ->
{auto u : Ref UST UState} -> {auto u : Ref UST UState} ->
FC -> Int -> ImpClause -> FC -> Int -> ImpClause ->
Core (List ImpClause) Core (Search (List ImpClause))
expandClause loc n c expandClause loc n c
= do c <- uniqueRHS c = do c <- uniqueRHS c
Right clause <- checkClause linear Private False n [] (MkNested []) [] c Right clause <- checkClause linear Private False n [] (MkNested []) [] c
| Left err => pure [] -- TODO: impossible clause, do something | Left err => noResult -- TODO: impossible clause, do something
-- appropriate -- appropriate
let MkClause {vars} env lhs rhs = clause let MkClause {vars} env lhs rhs = clause
let Meta _ i fn _ = getFn rhs let Meta _ i fn _ = getFn rhs
@ -67,16 +67,16 @@ expandClause loc n c
Just (Hole locs _) <- lookupDefExact (Resolved fn) (gamma defs) Just (Hole locs _) <- lookupDefExact (Resolved fn) (gamma defs)
| _ => throw (GenericMsg loc "No searchable hole on RHS") | _ => throw (GenericMsg loc "No searchable hole on RHS")
log 10 $ "Expression search for " ++ show (i, fn) log 10 $ "Expression search for " ++ show (i, fn)
(rhs' :: _) <- exprSearchN loc 1 (Resolved fn) [] rhs' <- exprSearch loc (Resolved fn) []
| _ => throw (GenericMsg loc "No result found for search on RHS") traverse (\rhs' =>
defs <- get Ctxt do defs <- get Ctxt
rhsnf <- normaliseHoles defs [] rhs' rhsnf <- normaliseHoles defs [] rhs'
let (_ ** (env', rhsenv)) = dropLams locs [] rhsnf let (_ ** (env', rhsenv)) = dropLams locs [] rhsnf
rhsraw <- unelab env' rhsenv rhsraw <- unelab env' rhsenv
logTermNF 5 "Got clause" env lhs logTermNF 5 "Got clause" env lhs
logTermNF 5 " = " env' rhsenv logTermNF 5 " = " env' rhsenv
pure [updateRHS c rhsraw] pure [updateRHS c rhsraw]) rhs'
where where
updateRHS : ImpClause -> RawImp -> ImpClause updateRHS : ImpClause -> RawImp -> ImpClause
updateRHS (PatClause fc lhs _) rhs = PatClause fc lhs rhs 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 (IBindHere loc PATTERN lhs) Nothing
traverse (trySplit fc lhs lhstm rhs) (splittableNames lhs) 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 mutual
tryAllSplits : {auto c : Ref Ctxt Defs} -> tryAllSplits : {auto c : Ref Ctxt Defs} ->
{auto m : Ref MD Metadata} -> {auto m : Ref MD Metadata} ->
{auto u : Ref UST UState} -> {auto u : Ref UST UState} ->
FC -> Int -> Error -> FC -> Int ->
List (Name, List ImpClause) -> List (Name, List ImpClause) ->
Core (List ImpClause) Core (Search (List ImpClause))
tryAllSplits loc n err [] = throw err tryAllSplits loc n [] = noResult
tryAllSplits loc n err ((x, []) :: rest) tryAllSplits loc n ((x, []) :: rest)
= tryAllSplits loc n err rest = tryAllSplits loc n rest
tryAllSplits loc n err ((x, cs) :: rest) tryAllSplits loc n ((x, cs) :: rest)
= do log 5 $ "Splitting on " ++ show x = do log 5 $ "Splitting on " ++ show x
tryUnify (do cs' <- traverse (mkSplits loc n) cs trySearch (do cs' <- traverse (mkSplits loc n) cs
pure (concat cs')) collectClauses cs')
(tryAllSplits loc n err rest) (tryAllSplits loc n rest)
mkSplits : {auto c : Ref Ctxt Defs} -> mkSplits : {auto c : Ref Ctxt Defs} ->
{auto m : Ref MD Metadata} -> {auto m : Ref MD Metadata} ->
{auto u : Ref UST UState} -> {auto u : Ref UST UState} ->
FC -> Int -> ImpClause -> FC -> Int -> ImpClause ->
Core (List ImpClause) Core (Search (List ImpClause))
-- If the clause works, use it. Otherwise, split on one of the splittable -- If the clause works, use it. Otherwise, split on one of the splittable
-- variables and try all of the resulting clauses -- variables and try all of the resulting clauses
mkSplits loc n c mkSplits loc n c
= handleUnify = trySearch
(expandClause loc n c) (expandClause loc n c)
(\err => (do cs <- generateSplits loc n c
do cs <- generateSplits loc n c log 5 $ "Splits: " ++ show cs
log 5 $ "Splits: " ++ show cs tryAllSplits loc n cs)
tryAllSplits loc n err cs)
export export
makeDef : {auto c : Ref Ctxt Defs} -> makeDef : {auto c : Ref Ctxt Defs} ->
{auto m : Ref MD Metadata} -> {auto m : Ref MD Metadata} ->
{auto u : Ref UST UState} -> {auto u : Ref UST UState} ->
(FC -> (Name, Nat, ClosedTerm) -> Bool) -> (FC -> (Name, Nat, ClosedTerm) -> Bool) ->
Name -> Core (Maybe (FC, List ImpClause)) Name -> Core (Search (FC, List ImpClause))
makeDef p n makeDef p n
= do Just (loc, nidx, envlen, ty) <- findTyDeclAt p = do Just (loc, nidx, envlen, ty) <- findTyDeclAt p
| Nothing => pure Nothing | Nothing => noResult
n <- getFullName nidx n <- getFullName nidx
logTerm 5 ("Searching for " ++ show n) ty logTerm 5 ("Searching for " ++ show n) ty
tryUnify tryUnify
@ -211,5 +219,13 @@ makeDef p n
put Ctxt defs put Ctxt defs
put MD meta put MD meta
put UST ust put UST ust
pure (Just (loc, cs'))) pure (map (\c => (loc, c)) cs'))
(pure Nothing) 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 case !(lookupDefExact n' (gamma defs)) of
Just None => Just None =>
catch catch
(do Just (fc, cs) <- logTime "Generation" $ (do ((fc, cs) :: _) <- logTime "Generation" $
makeDef (\p, n => onLine line p) n' makeDefN (\p, n => onLine line p) 1 n'
| Nothing => coreLift (putStrLn "Failed") | _ => coreLift (putStrLn "Failed")
coreLift $ putStrLn (show cs)) coreLift $ putStrLn (show cs))
(\err => coreLift $ putStrLn $ "Can't find a definition for " ++ show n') (\err => coreLift $ putStrLn $ "Can't find a definition for " ++ show n')
Just _ => coreLift $ putStrLn "Already defined" Just _ => coreLift $ putStrLn "Already defined"