git.iko.soy/Idris-dev
on master help sign in
Add proof search to Elab
9b94995David Raymond Christiansen
libs/prelude/Language/Reflection/Elab.idr+12
compare with master
unifiedsplit
@@ -115,6 +115,7 @@ data Elab : Type -> Type where
115 prim__AddInstance : TTName -> TTName -> Elab ()
115 prim__AddInstance : TTName -> TTName -> Elab ()
116
116
117 prim__ResolveTC : TTName -> Elab ()
117 prim__ResolveTC : TTName -> Elab ()
118+ prim__Search : Int -> List TTName -> Elab ()
118 prim__RecursiveElab : Raw -> Elab () -> Elab (TT, TT)
119 prim__RecursiveElab : Raw -> Elab () -> Elab (TT, TT)
119
120
120 prim__Debug : {a : Type} -> Maybe String -> Elab a
121 prim__Debug : {a : Type} -> Maybe String -> Elab a
@@ -312,6 +313,17 @@ namespace Tactics
312 resolveTC : (fn : TTName) -> Elab ()
313 resolveTC : (fn : TTName) -> Elab ()
313 resolveTC fn = prim__ResolveTC fn
314 resolveTC fn = prim__ResolveTC fn
314
315
316+ ||| Use Idris's internal proof search.
317+ search : Elab ()
318+ search = prim__Search 100 []
319+
320+ ||| Use Idris's internal proof search, with more control.
321+ |||
322+ ||| @ depth the search depth
323+ ||| @ hints additional names to try
324+ search' : (depth : Int) -> (hints : List TTName) -> Elab ()
325+ search' depth hints = prim__Search depth hints
326+
315 ||| Halt elaboration, dumping the internal state for inspection.
327 ||| Halt elaboration, dumping the internal state for inspection.
316 |||
328 |||
317 ||| This is intended for elaboration script developers, not for
329 ||| This is intended for elaboration script developers, not for
src/Idris/Elab/Term.hs+13
@@ -1929,6 +1929,19 @@ runTactical ist fc env tm = do tm' <- eval tm
1929 fn <- reifyTTName fn
1929 fn <- reifyTTName fn
1930 resolveTC False True 100 g fn ist
1930 resolveTC False True 100 g fn ist
1931 returnUnit
1931 returnUnit
1932+ | n == tacN "prim__Search", [depth, hints] <- args
1933+ = do d <- eval depth
1934+ hints' <- eval hints
1935+ case (d, unList hints') of
1936+ (Constant (I i), Just hs) ->
1937+ do actualHints <- mapM reifyTTName hs
1938+ unifyProblems
1939+ let psElab = elab ist toplevel ERHS [] (sMN 0 "tac")
1940+ proofSearch True True False False i psElab Nothing (sMN 0 "search ") actualHints ist
1941+ returnUnit
1942+ (Constant (I _), Nothing ) ->
1943+ lift . tfail . InternalMsg $ "Not a list: " ++ show hints'
1944+ (_, _) -> lift . tfail . InternalMsg $ "Can't reify int " ++ show d
1932 | n == tacN "prim__RecursiveElab", [goal, script] <- args
1945 | n == tacN "prim__RecursiveElab", [goal, script] <- args
1933 = do goal' <- reifyRaw goal
1946 = do goal' <- reifyRaw goal
1934 ctxt <- get_context
1947 ctxt <- get_context