git.iko.soy/Idris-dev
on master help sign in
Add "intro" tactic to new tactics
ee8fce0David Raymond Christiansen
libs/prelude/Language/Reflection/Tactical.idr+4
compare with master
unifiedsplit
@@ -33,6 +33,7 @@ data Tactical : Type -> Type where
33 prim__Attack : Tactical ()
33 prim__Attack : Tactical ()
34
34
35 prim__Claim : TTName -> Raw -> Tactical ()
35 prim__Claim : TTName -> Raw -> Tactical ()
36+ prim__Intro : Maybe TTName -> Tactical ()
36
37
37-------------
38-------------
38-- Public API
39-- Public API
@@ -93,3 +94,6 @@ attack = prim__Attack
93
94
94claim : TTName -> Raw -> Tactical ()
95claim : TTName -> Raw -> Tactical ()
95claim n ty = prim__Claim n ty
96claim 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 ()
1575 = do n' <- reifyTTName what
1575 = do n' <- reifyTTName what
1576 movelast n'
1576 movelast n'
1577 returnUnit
1577 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
1578 runTacTm x = lift . tfail . InternalMsg $ "tactical is not implemented for " ++ show x
1584 runTacTm x = lift . tfail . InternalMsg $ "tactical is not implemented for " ++ show x
1579
1585
1580-- Running tactics directly
1586-- Running tactics directly