git.iko.soy/Idris-dev
on master help sign in
Add proof search to Elab
commit9b949951935e0f79e5edfcd763640a4488f8ebca authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateTue 26 May 2015, 15:37 (11 years ago) parent0689f2b
2 files changed+25
compare with master
unifiedsplit
libs/prelude/Language/Reflection/Elab.idr+12 src/Idris/Elab/Term.hs+13
libs/prelude/Language/Reflection/Elab.idr+12
@@ -115,6 +115,7 @@ data Elab : Type -> Type where
115115 prim__AddInstance : TTName -> TTName -> Elab ()
116116
117117 prim__ResolveTC : TTName -> Elab ()
118+ prim__Search : Int -> List TTName -> Elab ()
118119 prim__RecursiveElab : Raw -> Elab () -> Elab (TT, TT)
119120
120121 prim__Debug : {a : Type} -> Maybe String -> Elab a
@@ -312,6 +313,17 @@ namespace Tactics
312313 resolveTC : (fn : TTName) -> Elab ()
313314 resolveTC fn = prim__ResolveTC fn
314315
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+
315327 ||| Halt elaboration, dumping the internal state for inspection.
316328 |||
317329 ||| 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
19291929 fn <- reifyTTName fn
19301930 resolveTC False True 100 g fn ist
19311931 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
19321945 | n == tacN "prim__RecursiveElab", [goal, script] <- args
19331946 = do goal' <- reifyRaw goal
19341947 ctxt <- get_context