git.iko.soy/Idris-dev
on master help sign in
Add "intro" tactic to new tactics
commitee8fce0b8a52c445e3c09d279064e843ad15da64 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateSun 22 Feb 2015, 19:57 (12 years ago) parentf327f18
2 files changed+10
compare with master
unifiedsplit
libs/prelude/Language/Reflection/Tactical.idr+4 src/Idris/ElabTerm.hs+6
libs/prelude/Language/Reflection/Tactical.idr+4
@@ -33,6 +33,7 @@ data Tactical : Type -> Type where
3333 prim__Attack : Tactical ()
3434
3535 prim__Claim : TTName -> Raw -> Tactical ()
36+ prim__Intro : Maybe TTName -> Tactical ()
3637
3738-------------
3839-- Public API
@@ -93,3 +94,6 @@ attack = prim__Attack
9394
9495claim : TTName -> Raw -> Tactical ()
9596claim n ty = prim__Claim n ty
97+
98+intro : Maybe TTName -> Tactical ()
99+intro n = prim__Intro n
src/Idris/ElabTerm.hs+6
@@ -1575,6 +1575,12 @@ runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()
15751575 = do n' <- reifyTTName what
15761576 movelast n'
15771577 returnUnit
1578+ | n == tacN "prim__Intro", [mn] <- args
1579+ = do n <- case fromTTMaybe mn of
1580+ Nothing -> return Nothing
1581+ Just name -> fmap Just $ reifyTTName name
1582+ intro n
1583+ returnUnit
15781584 runTacTm x = lift . tfail . InternalMsg $ "tactical is not implemented for " ++ show x
15791585
15801586-- Running tactics directly