2f96f33 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Split between primitive tactics and UI

This allows the interface to be better than the underlying primitives.

commit2f96f3388f607f0f517927b5ccda9a8db4caff31 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateThu 19 Feb 2015, 11:29 (12 years ago) parenta0346b6

2 files changed+83−41

compare with master

unifiedsplit

libs/prelude/Language/Reflection/Tactical.idr+67−25 src/Idris/ElabTerm.hs+16−16

libs/prelude/Language/Reflection/Tactical.idr+67−25

@@ -8,46 +8,88 @@ import Prelude.Maybe

88import Prelude.Monad

99import Language.Reflection

1010

11+%access private

12+

1113data Tactical : Type -> Type where

1214 -- obligatory control stuff

13− PureTactical : a -> Tactical a

14− BindTactical : {a, b : Type} -> Tactical a -> (a -> Tactical b) -> Tactical b

15+ prim__PureTactical : a -> Tactical a

16+ prim__BindTactical : {a, b : Type} -> Tactical a -> (a -> Tactical b) -> Tactical b

1517

16− Try : {a : Type} -> Tactical a -> Tactical a -> Tactical a

17− Skip : Tactical ()

18− Fail : {a : Type} -> List ErrorReportPart -> Tactical a

18+ prim__Try : {a : Type} -> Tactical a -> Tactical a -> Tactical a

19+ prim__Fail : {a : Type} -> List ErrorReportPart -> Tactical a

1920

20− Env : Tactical (List (TTName, Binder TT))

21− Goal : Tactical (TTName, TT)

22− Holes : Tactical (List TTName)

23− Guess : Tactical (Maybe TT)

21+ prim__Env : Tactical (List (TTName, Binder TT))

22+ prim__Goal : Tactical (TTName, TT)

23+ prim__Holes : Tactical (List TTName)

24+ prim__Guess : Tactical (Maybe TT)

2425

25− Forget : TT -> Tactical Raw

26+ prim__Forget : TT -> Tactical Raw

2627

27− Gensym : String -> Tactical TTName

28+ prim__Gensym : String -> Tactical TTName

2829

29− Solve : Tactical ()

30− Fill : Raw -> Tactical ()

31− Focus : TTName -> Tactical ()

32− Unfocus : TTName -> Tactical ()

33− Attack : Tactical ()

30+ prim__Solve : Tactical ()

31+ prim__Fill : Raw -> Tactical ()

32+ prim__Focus : TTName -> Tactical ()

33+ prim__Unfocus : TTName -> Tactical ()

34+ prim__Attack : Tactical ()

3435

35− Claim : TTName -> Raw -> Tactical ()

36+ prim__Claim : TTName -> Raw -> Tactical ()

3637

38+-------------

39+-- Public API

40+-------------

41+%access public

3742

3843instance 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))

4045

4146instance Applicative Tactical where

42− pure x = PureTactical x

43− f <$> x = BindTactical f $ \g =>

44− BindTactical x $ \y =>

45− PureTactical $ g y

47+ pure x = prim__PureTactical x

48+ f <$> x = prim__BindTactical f $ \g =>

49+ prim__BindTactical x $ \y =>

50+ prim__PureTactical $ g y

4651

4752instance Alternative Tactical where

48− empty = Fail [TextPart "empty"]

49− x <|> y = Try x y

53+ empty = prim__Fail [TextPart "empty"]

54+ x <|> y = prim__Try x y

5055

5156instance 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

5393

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 ()

14761476 -- step, the output is the (reflected) term returned.

14771477 runTacTm :: Term -> ElabD Term

14781478 runTacTm (unApply -> tac@(P _ n _, args))

1479− | n == tacN "Solve", [] <- args

1479+ | n == tacN "prim__Solve", [] <- args

14801480 = do solve

14811481 returnUnit

1482− | n == tacN "Goal", [] <- args

1482+ | n == tacN "prim__Goal", [] <- args

14831483 = do (h:_) <- get_holes

14841484 t <- goal

14851485 fmap fst . get_type_val $

14861486 rawPair (Var (reflm "TTName"), Var (reflm "TT"))

14871487 (reflectName h, reflect t)

1488− | n == tacN "Holes", [] <- args

1488+ | n == tacN "prim__Holes", [] <- args

14891489 = do hs <- get_holes

14901490 fmap fst . get_type_val $

14911491 mkList (Var $ reflm "TTName") (map reflectName hs)

1492− | n == tacN "Guess", [] <- args

1492+ | n == tacN "prim__Guess", [] <- args

14931493 = do ok <- is_guess

14941494 if ok

14951495 then do guess <- fmap forget get_guess

@@ -1500,46 +1500,46 @@ runTactical ctxt env tm = runTacTm (eval tm) >> return ()

15001500 else fmap fst . get_type_val $

15011501 RApp (Var (sNS (sUN "Nothing") ["Maybe", "Prelude"]))

15021502 (Var (reflm "TT"))

1503− | n == tacN "Env", [] <- args

1503+ | n == tacN "prim__Env", [] <- args

15041504 = do env <- get_env

15051505 fmap fst . get_type_val $ reflectEnv env

1506− | n == tacN "Fail", [_a, errs] <- args

1506+ | n == tacN "prim__Fail", [_a, errs] <- args

15071507 = do parts <- reifyReportParts (eval errs)

15081508 lift . tfail $ ReflectionError [parts] (Msg "")

1509− | n == tacN "PureTactical", [_a, tm] <- args

1509+ | n == tacN "prim__PureTactical", [_a, tm] <- args

15101510 = return tm

1511− | n == tacN "BindTactical", [_a, _b, first, andThen] <- args

1511+ | n == tacN "prim__BindTactical", [_a, _b, first, andThen] <- args

15121512 = do let first' = eval first

15131513 res <- runTacTm first'

15141514 let next = eval (App andThen res)

15151515 runTacTm next

1516− | n == tacN "Try", [_a, first, alt] <- args

1516+ | n == tacN "prim__Try", [_a, first, alt] <- args

15171517 = do let first' = eval first

15181518 let alt' = eval alt

15191519 try' (runTacTm first') (runTacTm alt') True

1520− | n == tacN "Fill", [raw] <- args

1520+ | n == tacN "prim__Fill", [raw] <- args

15211521 = do raw' <- reifyRaw raw

15221522 apply raw' []

15231523 returnUnit

1524− | n == tacN "Gensym", [eval -> Constant (Str hint)] <- args

1524+ | n == tacN "prim__Gensym", [eval -> Constant (Str hint)] <- args

15251525 = do n <- getNameFrom (sMN 0 hint)

15261526 fmap fst $ get_type_val (reflectName n)

1527− | n == tacN "Claim", [n, ty] <- args

1527+ | n == tacN "prim__Claim", [n, ty] <- args

15281528 = do n' <- reifyTTName n

15291529 ty' <- reifyRaw ty

15301530 claim n' ty'

15311531 returnUnit

1532− | n == tacN "Forget", [tt] <- args

1532+ | n == tacN "prim__Forget", [tt] <- args

15331533 = do tt' <- reifyTT tt

15341534 fmap fst . get_type_val $ reflect tt'

1535− | n == tacN "Attack", [] <- args

1535+ | n == tacN "prim__Attack", [] <- args

15361536 = do attack

15371537 returnUnit

1538− | n == tacN "Focus", [what] <- args

1538+ | n == tacN "prim__Focus", [what] <- args

15391539 = do n' <- reifyTTName what

15401540 focus n'

15411541 returnUnit

1542− | n == tacN "Unfocus", [what] <- args

1542+ | n == tacN "prim__Unfocus", [what] <- args

15431543 = do n' <- reifyTTName what

15441544 movelast n'

15451545 returnUnit