git.iko.soy/Idris-dev
on master help sign in
Split between primitive tactics and UI
2f96f33David Raymond Christiansen
libs/prelude/Language/Reflection/Tactical.idr+67−25
compare with master
unifiedsplit
@@ -8,46 +8,88 @@ import Prelude.Maybe
8import Prelude.Monad
8import Prelude.Monad
9import Language.Reflection
9import Language.Reflection
10
10
11+%access private
12+
11data Tactical : Type -> Type where
13data Tactical : Type -> Type where
12 -- obligatory control stuff
14 -- obligatory control stuff
13− PureTactical : a -> Tactical a
15+ prim__PureTactical : a -> Tactical a
14− BindTactical : {a, b : Type} -> Tactical a -> (a -> Tactical b) -> Tactical b
16+ prim__BindTactical : {a, b : Type} -> Tactical a -> (a -> Tactical b) -> Tactical b
15
17
16− Try : {a : Type} -> Tactical a -> Tactical a -> Tactical a
18+ prim__Try : {a : Type} -> Tactical a -> Tactical a -> Tactical a
17− Skip : Tactical ()
18− Fail : {a : Type} -> List ErrorReportPart -> Tactical a
19+ prim__Fail : {a : Type} -> List ErrorReportPart -> Tactical a
19
20
20− Env : Tactical (List (TTName, Binder TT))
21+ prim__Env : Tactical (List (TTName, Binder TT))
21− Goal : Tactical (TTName, TT)
22+ prim__Goal : Tactical (TTName, TT)
22− Holes : Tactical (List TTName)
23+ prim__Holes : Tactical (List TTName)
23− Guess : Tactical (Maybe TT)
24+ prim__Guess : Tactical (Maybe TT)
24
25
25− Forget : TT -> Tactical Raw
26+ prim__Forget : TT -> Tactical Raw
26
27
27− Gensym : String -> Tactical TTName
28+ prim__Gensym : String -> Tactical TTName
28
29
29− Solve : Tactical ()
30+ prim__Solve : Tactical ()
30− Fill : Raw -> Tactical ()
31+ prim__Fill : Raw -> Tactical ()
31− Focus : TTName -> Tactical ()
32+ prim__Focus : TTName -> Tactical ()
32− Unfocus : TTName -> Tactical ()
33+ prim__Unfocus : TTName -> Tactical ()
33− Attack : Tactical ()
34+ prim__Attack : Tactical ()
34
35
35− Claim : TTName -> Raw -> Tactical ()
36+ prim__Claim : TTName -> Raw -> Tactical ()
36
37
38+-------------
39+-- Public API
40+-------------
41+%access public
37
42
38instance Functor Tactical where
43instance Functor Tactical where
39− map f t = BindTactical t (\x => PureTactical (f x))
44+ map f t = prim__BindTactical t (\x => prim__PureTactical (f x))
40
45
41instance Applicative Tactical where
46instance Applicative Tactical where
42− pure x = PureTactical x
47+ pure x = prim__PureTactical x
43− f <$> x = BindTactical f $ \g =>
48+ f <$> x = prim__BindTactical f $ \g =>
44− BindTactical x $ \y =>
49+ prim__BindTactical x $ \y =>
45− PureTactical $ g y
50+ prim__PureTactical $ g y
46
51
47instance Alternative Tactical where
52instance Alternative Tactical where
48− empty = Fail [TextPart "empty"]
53+ empty = prim__Fail [TextPart "empty"]
49− x <|> y = Try x y
54+ x <|> y = prim__Try x y
50
55
51instance Monad Tactical where
56instance Monad Tactical where
52− x >>= f = BindTactical x f
57+ x >>= f = prim__BindTactical x f
58+
59+fail : List ErrorReportPart -> Tactical a
60+fail err = prim__Fail err
61+
62+getEnv : Tactical (List (TTName, Binder TT))
63+getEnv = prim__Env
64+
65+getGoal : Tactical (TTName, TT)
66+getGoal = prim__Goal
67+
68+getHoles : Tactical (List TTName)
69+getHoles = prim__Holes
70+getGuess : Tactical (Maybe TT)
71+getGuess = prim__Guess
72+
73+forgetTypes : TT -> Tactical Raw
74+forgetTypes tt = prim__Forget tt
75+
76+gensym : (hint : String) -> Tactical TTName
77+gensym hint = prim__Gensym hint
78+
79+solve : Tactical ()
80+solve = prim__Solve
81+
82+fill : Raw -> Tactical ()
83+fill tm = prim__Fill tm
84+
85+focus : (hole : TTName) -> Tactical ()
86+focus hole = prim__Focus hole
87+
88+unfocus : TTName -> Tactical ()
89+unfocus hole = prim__Unfocus hole
90+
91+attack : Tactical ()
92+attack = prim__Attack
53
93
94+claim : TTName -> Raw -> Tactical ()
95+claim n ty = prim__Claim n ty
src/Idris/ElabTerm.hs+16−16
@@ -1476,20 +1476,20 @@ runTactical ctxt env tm = runTacTm (eval tm) >> return ()
1476 -- step, the output is the (reflected) term returned.
1476 -- step, the output is the (reflected) term returned.
1477 runTacTm :: Term -> ElabD Term
1477 runTacTm :: Term -> ElabD Term
1478 runTacTm (unApply -> tac@(P _ n _, args))
1478 runTacTm (unApply -> tac@(P _ n _, args))
1479− | n == tacN "Solve", [] <- args
1479+ | n == tacN "prim__Solve", [] <- args
1480 = do solve
1480 = do solve
1481 returnUnit
1481 returnUnit
1482− | n == tacN "Goal", [] <- args
1482+ | n == tacN "prim__Goal", [] <- args
1483 = do (h:_) <- get_holes
1483 = do (h:_) <- get_holes
1484 t <- goal
1484 t <- goal
1485 fmap fst . get_type_val $
1485 fmap fst . get_type_val $
1486 rawPair (Var (reflm "TTName"), Var (reflm "TT"))
1486 rawPair (Var (reflm "TTName"), Var (reflm "TT"))
1487 (reflectName h, reflect t)
1487 (reflectName h, reflect t)
1488− | n == tacN "Holes", [] <- args
1488+ | n == tacN "prim__Holes", [] <- args
1489 = do hs <- get_holes
1489 = do hs <- get_holes
1490 fmap fst . get_type_val $
1490 fmap fst . get_type_val $
1491 mkList (Var $ reflm "TTName") (map reflectName hs)
1491 mkList (Var $ reflm "TTName") (map reflectName hs)
1492− | n == tacN "Guess", [] <- args
1492+ | n == tacN "prim__Guess", [] <- args
1493 = do ok <- is_guess
1493 = do ok <- is_guess
1494 if ok
1494 if ok
1495 then do guess <- fmap forget get_guess
1495 then do guess <- fmap forget get_guess
@@ -1500,46 +1500,46 @@ runTactical ctxt env tm = runTacTm (eval tm) >> return ()
1500 else fmap fst . get_type_val $
1500 else fmap fst . get_type_val $
1501 RApp (Var (sNS (sUN "Nothing") ["Maybe", "Prelude"]))
1501 RApp (Var (sNS (sUN "Nothing") ["Maybe", "Prelude"]))
1502 (Var (reflm "TT"))
1502 (Var (reflm "TT"))
1503− | n == tacN "Env", [] <- args
1503+ | n == tacN "prim__Env", [] <- args
1504 = do env <- get_env
1504 = do env <- get_env
1505 fmap fst . get_type_val $ reflectEnv env
1505 fmap fst . get_type_val $ reflectEnv env
1506− | n == tacN "Fail", [_a, errs] <- args
1506+ | n == tacN "prim__Fail", [_a, errs] <- args
1507 = do parts <- reifyReportParts (eval errs)
1507 = do parts <- reifyReportParts (eval errs)
1508 lift . tfail $ ReflectionError [parts] (Msg "")
1508 lift . tfail $ ReflectionError [parts] (Msg "")
1509− | n == tacN "PureTactical", [_a, tm] <- args
1509+ | n == tacN "prim__PureTactical", [_a, tm] <- args
1510 = return tm
1510 = return tm
1511− | n == tacN "BindTactical", [_a, _b, first, andThen] <- args
1511+ | n == tacN "prim__BindTactical", [_a, _b, first, andThen] <- args
1512 = do let first' = eval first
1512 = do let first' = eval first
1513 res <- runTacTm first'
1513 res <- runTacTm first'
1514 let next = eval (App andThen res)
1514 let next = eval (App andThen res)
1515 runTacTm next
1515 runTacTm next
1516− | n == tacN "Try", [_a, first, alt] <- args
1516+ | n == tacN "prim__Try", [_a, first, alt] <- args
1517 = do let first' = eval first
1517 = do let first' = eval first
1518 let alt' = eval alt
1518 let alt' = eval alt
1519 try' (runTacTm first') (runTacTm alt') True
1519 try' (runTacTm first') (runTacTm alt') True
1520− | n == tacN "Fill", [raw] <- args
1520+ | n == tacN "prim__Fill", [raw] <- args
1521 = do raw' <- reifyRaw raw
1521 = do raw' <- reifyRaw raw
1522 apply raw' []
1522 apply raw' []
1523 returnUnit
1523 returnUnit
1524− | n == tacN "Gensym", [eval -> Constant (Str hint)] <- args
1524+ | n == tacN "prim__Gensym", [eval -> Constant (Str hint)] <- args
1525 = do n <- getNameFrom (sMN 0 hint)
1525 = do n <- getNameFrom (sMN 0 hint)
1526 fmap fst $ get_type_val (reflectName n)
1526 fmap fst $ get_type_val (reflectName n)
1527− | n == tacN "Claim", [n, ty] <- args
1527+ | n == tacN "prim__Claim", [n, ty] <- args
1528 = do n' <- reifyTTName n
1528 = do n' <- reifyTTName n
1529 ty' <- reifyRaw ty
1529 ty' <- reifyRaw ty
1530 claim n' ty'
1530 claim n' ty'
1531 returnUnit
1531 returnUnit
1532− | n == tacN "Forget", [tt] <- args
1532+ | n == tacN "prim__Forget", [tt] <- args
1533 = do tt' <- reifyTT tt
1533 = do tt' <- reifyTT tt
1534 fmap fst . get_type_val $ reflect tt'
1534 fmap fst . get_type_val $ reflect tt'
1535− | n == tacN "Attack", [] <- args
1535+ | n == tacN "prim__Attack", [] <- args
1536 = do attack
1536 = do attack
1537 returnUnit
1537 returnUnit
1538− | n == tacN "Focus", [what] <- args
1538+ | n == tacN "prim__Focus", [what] <- args
1539 = do n' <- reifyTTName what
1539 = do n' <- reifyTTName what
1540 focus n'
1540 focus n'
1541 returnUnit
1541 returnUnit
1542− | n == tacN "Unfocus", [what] <- args
1542+ | n == tacN "prim__Unfocus", [what] <- args
1543 = do n' <- reifyTTName what
1543 = do n' <- reifyTTName what
1544 movelast n'
1544 movelast n'
1545 returnUnit
1545 returnUnit