git.iko.soy/Idris-dev
on master help sign in
Rename Tactical to Elab
c3def79David Raymond Christiansen
libs/prelude/Language/Reflection/Elab.idrnew file+149
compare with master
unifiedsplit
@@ -0,0 +1,149 @@
1+module Language.Reflection.Elab
2+
3+import Builtins
4+import Prelude.Applicative
5+import Prelude.Functor
6+import Prelude.List
7+import Prelude.Maybe
8+import Prelude.Monad
9+import Language.Reflection
10+
11+data Arg : Type where
12+ Explicit : TTName -> Raw -> Arg
13+ Implicit : TTName -> Raw -> Arg
14+ Constraint : TTName -> Raw -> Arg
15+
16+data TyDecl : Type where
17+ Declare : TTName -> List Arg -> Raw -> TyDecl
18+
19+data FunClause : Type where
20+ MkFunClause : (lhs, rhs : Raw) -> FunClause
21+ MkImpossibleClause : (lhs : Raw) -> FunClause
22+
23+data FunDefn : Type where
24+ DefineFun : TTName -> List FunClause -> FunDefn
25+
26+abstract
27+data Elab : Type -> Type where
28+ -- obligatory control stuff
29+ prim__PureElab : a -> Elab a
30+ prim__BindElab : {a, b : Type} -> Elab a -> (a -> Elab b) -> Elab b
31+
32+ prim__Try : {a : Type} -> Elab a -> Elab a -> Elab a
33+ prim__Fail : {a : Type} -> List ErrorReportPart -> Elab a
34+
35+ prim__Env : Elab (List (TTName, Binder TT))
36+ prim__Goal : Elab (TTName, TT)
37+ prim__Holes : Elab (List TTName)
38+ prim__Guess : Elab (Maybe TT)
39+
40+ prim__SourceLocation : Elab SourceLocation
41+
42+ prim__Forget : TT -> Elab Raw
43+
44+ prim__Gensym : String -> Elab TTName
45+
46+ prim__Solve : Elab ()
47+ prim__Fill : Raw -> Elab ()
48+ prim__Focus : TTName -> Elab ()
49+ prim__Unfocus : TTName -> Elab ()
50+ prim__Attack : Elab ()
51+
52+ prim__Rewrite : Raw -> Elab ()
53+
54+ prim__Claim : TTName -> Raw -> Elab ()
55+ prim__Intro : Maybe TTName -> Elab ()
56+
57+ prim__DeclareType : TyDecl -> Elab ()
58+ prim__DefineFunction : FunDefn -> Elab ()
59+
60+ prim__Debug : {a : Type} -> Maybe String -> Elab a
61+
62+
63+-------------
64+-- Public API
65+-------------
66+%access public
67+
68+instance Functor Elab where
69+ map f t = prim__BindElab t (\x => prim__PureElab (f x))
70+
71+instance Applicative Elab where
72+ pure x = prim__PureElab x
73+ f <*> x = prim__BindElab f $ \g =>
74+ prim__BindElab x $ \y =>
75+ prim__PureElab $ g y
76+
77+instance Alternative Elab where
78+ empty = prim__Fail [TextPart "empty"]
79+ x <|> y = prim__Try x y
80+
81+instance Monad Elab where
82+ x >>= f = prim__BindElab x f
83+
84+fail : List ErrorReportPart -> Elab a
85+fail err = prim__Fail err
86+
87+getEnv : Elab (List (TTName, Binder TT))
88+getEnv = prim__Env
89+
90+getGoal : Elab (TTName, TT)
91+getGoal = prim__Goal
92+
93+getHoles : Elab (List TTName)
94+getHoles = prim__Holes
95+
96+getGuess : Elab (Maybe TT)
97+getGuess = prim__Guess
98+
99+forgetTypes : TT -> Elab Raw
100+forgetTypes tt = prim__Forget tt
101+
102+gensym : (hint : String) -> Elab TTName
103+gensym hint = prim__Gensym hint
104+
105+solve : Elab ()
106+solve = prim__Solve
107+
108+fill : Raw -> Elab ()
109+fill tm = prim__Fill tm
110+
111+focus : (hole : TTName) -> Elab ()
112+focus hole = prim__Focus hole
113+
114+unfocus : TTName -> Elab ()
115+unfocus hole = prim__Unfocus hole
116+
117+attack : Elab ()
118+attack = prim__Attack
119+
120+claim : TTName -> Raw -> Elab ()
121+claim n ty = prim__Claim n ty
122+
123+intro : Maybe TTName -> Elab ()
124+intro n = prim__Intro n
125+
126+||| Find out the present source context for the tactic script
127+getSourceLocation : Elab SourceLocation
128+getSourceLocation = prim__SourceLocation
129+
130+||| Attempt to solve the current goal with the source code location
131+sourceLocation : Elab ()
132+sourceLocation = do loc <- getSourceLocation
133+ fill (quote loc)
134+ solve
135+
136+rewriteWith : Raw -> Elab ()
137+rewriteWith rule = prim__Rewrite rule
138+
139+declareType : TyDecl -> Elab ()
140+declareType decl = prim__DeclareType decl
141+
142+defineFunction : FunDefn -> Elab ()
143+defineFunction defun = prim__DefineFunction defun
144+
145+debug : Elab a
146+debug = prim__Debug Nothing
147+
148+debugMessage : String -> Elab a
149+debugMessage msg = prim__Debug (Just msg)
libs/prelude/Language/Reflection/Tactical.idrdeleted−149
@@ -1,149 +0,0 @@
1−module Language.Reflection.Tactical
2−
3−import Builtins
4−import Prelude.Applicative
5−import Prelude.Functor
6−import Prelude.List
7−import Prelude.Maybe
8−import Prelude.Monad
9−import Language.Reflection
10−
11−data Arg : Type where
12− Explicit : TTName -> Raw -> Arg
13− Implicit : TTName -> Raw -> Arg
14− Constraint : TTName -> Raw -> Arg
15−
16−data TyDecl : Type where
17− Declare : TTName -> List Arg -> Raw -> TyDecl
18−
19−data FunClause : Type where
20− MkFunClause : (lhs, rhs : Raw) -> FunClause
21− MkImpossibleClause : (lhs : Raw) -> FunClause
22−
23−data FunDefn : Type where
24− DefineFun : TTName -> List FunClause -> FunDefn
25−
26−abstract
27−data Tactical : Type -> Type where
28− -- obligatory control stuff
29− prim__PureTactical : a -> Tactical a
30− prim__BindTactical : {a, b : Type} -> Tactical a -> (a -> Tactical b) -> Tactical b
31−
32− prim__Try : {a : Type} -> Tactical a -> Tactical a -> Tactical a
33− prim__Fail : {a : Type} -> List ErrorReportPart -> Tactical a
34−
35− prim__Env : Tactical (List (TTName, Binder TT))
36− prim__Goal : Tactical (TTName, TT)
37− prim__Holes : Tactical (List TTName)
38− prim__Guess : Tactical (Maybe TT)
39−
40− prim__SourceLocation : Tactical SourceLocation
41−
42− prim__Forget : TT -> Tactical Raw
43−
44− prim__Gensym : String -> Tactical TTName
45−
46− prim__Solve : Tactical ()
47− prim__Fill : Raw -> Tactical ()
48− prim__Focus : TTName -> Tactical ()
49− prim__Unfocus : TTName -> Tactical ()
50− prim__Attack : Tactical ()
51−
52− prim__Rewrite : Raw -> Tactical ()
53−
54− prim__Claim : TTName -> Raw -> Tactical ()
55− prim__Intro : Maybe TTName -> Tactical ()
56−
57− prim__DeclareType : TyDecl -> Tactical ()
58− prim__DefineFunction : FunDefn -> Tactical ()
59−
60− prim__Debug : {a : Type} -> Maybe String -> Tactical a
61−
62−
63−-------------
64−-- Public API
65−-------------
66−%access public
67−
68−instance Functor Tactical where
69− map f t = prim__BindTactical t (\x => prim__PureTactical (f x))
70−
71−instance Applicative Tactical where
72− pure x = prim__PureTactical x
73− f <*> x = prim__BindTactical f $ \g =>
74− prim__BindTactical x $ \y =>
75− prim__PureTactical $ g y
76−
77−instance Alternative Tactical where
78− empty = prim__Fail [TextPart "empty"]
79− x <|> y = prim__Try x y
80−
81−instance Monad Tactical where
82− x >>= f = prim__BindTactical x f
83−
84−fail : List ErrorReportPart -> Tactical a
85−fail err = prim__Fail err
86−
87−getEnv : Tactical (List (TTName, Binder TT))
88−getEnv = prim__Env
89−
90−getGoal : Tactical (TTName, TT)
91−getGoal = prim__Goal
92−
93−getHoles : Tactical (List TTName)
94−getHoles = prim__Holes
95−
96−getGuess : Tactical (Maybe TT)
97−getGuess = prim__Guess
98−
99−forgetTypes : TT -> Tactical Raw
100−forgetTypes tt = prim__Forget tt
101−
102−gensym : (hint : String) -> Tactical TTName
103−gensym hint = prim__Gensym hint
104−
105−solve : Tactical ()
106−solve = prim__Solve
107−
108−fill : Raw -> Tactical ()
109−fill tm = prim__Fill tm
110−
111−focus : (hole : TTName) -> Tactical ()
112−focus hole = prim__Focus hole
113−
114−unfocus : TTName -> Tactical ()
115−unfocus hole = prim__Unfocus hole
116−
117−attack : Tactical ()
118−attack = prim__Attack
119−
120−claim : TTName -> Raw -> Tactical ()
121−claim n ty = prim__Claim n ty
122−
123−intro : Maybe TTName -> Tactical ()
124−intro n = prim__Intro n
125−
126−||| Find out the present source context for the tactic script
127−getSourceLocation : Tactical SourceLocation
128−getSourceLocation = prim__SourceLocation
129−
130−||| Attempt to solve the current goal with the source code location
131−sourceLocation : Tactical ()
132−sourceLocation = do loc <- getSourceLocation
133− fill (quote loc)
134− solve
135−
136−rewriteWith : Raw -> Tactical ()
137−rewriteWith rule = prim__Rewrite rule
138−
139−declareType : TyDecl -> Tactical ()
140−declareType decl = prim__DeclareType decl
141−
142−defineFunction : FunDefn -> Tactical ()
143−defineFunction defun = prim__DefineFunction defun
144−
145−debug : Tactical a
146−debug = prim__Debug Nothing
147−
148−debugMessage : String -> Tactical a
149−debugMessage msg = prim__Debug (Just msg)
libs/prelude/prelude.ipkg+1−1
@@ -10,7 +10,7 @@ modules = Builtins, Prelude, IO,
10 Prelude.Foldable, Prelude.Traversable, Prelude.Bits, Prelude.Stream,
10 Prelude.Foldable, Prelude.Traversable, Prelude.Bits, Prelude.Stream,
11 Prelude.Uninhabited, Prelude.Pairs, Prelude.Providers,
11 Prelude.Uninhabited, Prelude.Pairs, Prelude.Providers,
12
12
13− Language.Reflection, Language.Reflection.Errors, Language.Reflection.Tactical,
13+ Language.Reflection, Language.Reflection.Errors, Language.Reflection.Elab,
14
14
15 Decidable.Equality
15 Decidable.Equality
16
16
src/Idris/AbsSyntax.hs+4−4
@@ -1011,7 +1011,7 @@ expandParams dec ps ns infs tm = en tm
1011 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
1011 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
1012 en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)
1012 en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)
1013 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
1013 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
1014− en (PRunTactics fc tm) = PRunTactics fc (en tm)
1014+ en (PRunElab fc tm) = PRunElab fc (en tm)
1015 en t = t
1015 en t = t
1016
1016
1017 nselem x [] = False
1017 nselem x [] = False
@@ -1485,7 +1485,7 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1485 imps top env (PHidden tm) = imps False env tm
1485 imps top env (PHidden tm) = imps False env tm
1486 imps top env (PUnifyLog tm) = imps False env tm
1486 imps top env (PUnifyLog tm) = imps False env tm
1487 imps top env (PNoImplicits tm) = imps False env tm
1487 imps top env (PNoImplicits tm) = imps False env tm
1488− imps top env (PRunTactics fc tm) = imps False env tm
1488+ imps top env (PRunElab fc tm) = imps False env tm
1489 imps top env _ = return ()
1489 imps top env _ = return ()
1490
1490
1491 pibind using [] sc = sc
1491 pibind using [] sc = sc
@@ -1612,7 +1612,7 @@ addImpl' inpat env infns imp_meths ist ptm
1612 ai qq env ds (PQuasiquote tm g) = PQuasiquote (ai True env ds tm)
1612 ai qq env ds (PQuasiquote tm g) = PQuasiquote (ai True env ds tm)
1613 (fmap (ai True env ds) g)
1613 (fmap (ai True env ds) g)
1614 ai qq env ds (PUnquote tm) = PUnquote (ai False env ds tm)
1614 ai qq env ds (PUnquote tm) = PUnquote (ai False env ds tm)
1615− ai qq env ds (PRunTactics fc tm) = PRunTactics fc (ai False env ds tm)
1615+ ai qq env ds (PRunElab fc tm) = PRunElab fc (ai False env ds tm)
1616 ai qq env ds tm = tm
1616 ai qq env ds tm = tm
1617
1617
1618 handleErr (Left err) = PElabError err
1618 handleErr (Left err) = PElabError err
@@ -2149,5 +2149,5 @@ mkUniqueNames env tm = evalState (mkUniq tm) (S.fromList env) where
2149 mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)
2149 mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)
2150 mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts)
2150 mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts)
2151 mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)
2151 mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)
2152− mkUniq (PRunTactics fc ts) = liftM (PRunTactics fc ) (mkUniq ts)
2152+ mkUniq (PRunElab fc ts) = liftM (PRunElab fc ) (mkUniq ts)
2153 mkUniq t = return t
2153 mkUniq t = return t
src/Idris/AbsSyntaxTree.hs+1−1
@@ -826,7 +826,7 @@ data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level langua
826 | PNoImplicits PTerm -- ^ never run implicit converions on the term
826 | PNoImplicits PTerm -- ^ never run implicit converions on the term
827 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
827 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
828 | PUnquote PTerm -- ^ ~Term
828 | PUnquote PTerm -- ^ ~Term
829− | PRunTactics FC PTerm -- ^ %runTactics tm - New-style proof script
829+ | PRunElab FC PTerm -- ^ %runElab tm - New-style proof script
830 deriving (Eq, Data, Typeable)
830 deriving (Eq, Data, Typeable)
831
831
832
832
src/Idris/DSL.hs+2−2
@@ -108,7 +108,7 @@ expandDo dsl (PDoBlock ds)
108 block b _ = PElabError (Msg "Invalid statement in do block")
108 block b _ = PElabError (Msg "Invalid statement in do block")
109
109
110expandDo dsl (PIdiom fc e) = expandDo dsl $ unIdiom (dsl_apply dsl) (dsl_pure dsl) fc e
110expandDo dsl (PIdiom fc e) = expandDo dsl $ unIdiom (dsl_apply dsl) (dsl_pure dsl) fc e
111−expandDo dsl (PRunTactics fc tm) = PRunTactics fc $ expandDo dsl tm
111+expandDo dsl (PRunElab fc tm) = PRunElab fc $ expandDo dsl tm
112expandDo dsl t = t
112expandDo dsl t = t
113
113
114-- | Replace DSL-bound variable in a term
114-- | Replace DSL-bound variable in a term
@@ -195,7 +195,7 @@ debind b tm = let (tm', (bs, _)) = runState (db' tm) ([], 0) in
195 db' (PDPair fc p l t r) = do l' <- db' l
195 db' (PDPair fc p l t r) = do l' <- db' l
196 r' <- db' r
196 r' <- db' r
197 return (PDPair fc p l' t r')
197 return (PDPair fc p l' t r')
198− db' (PRunTactics fc t) = fmap (PRunTactics fc) (db' t)
198+ db' (PRunElab fc t) = fmap (PRunElab fc) (db' t)
199 db' t = return t
199 db' t = return t
200
200
201 dbArg a = do t' <- db' (getTm a)
201 dbArg a = do t' <- db' (getTm a)
src/Idris/DeepSeq.hs+1−1
@@ -243,7 +243,7 @@ instance NFData PTerm where
243 rnf (PNoImplicits x1) = rnf x1 `seq` ()
243 rnf (PNoImplicits x1) = rnf x1 `seq` ()
244 rnf (PQuasiquote x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
244 rnf (PQuasiquote x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
245 rnf (PUnquote x1) = rnf x1 `seq` ()
245 rnf (PUnquote x1) = rnf x1 `seq` ()
246− rnf (PRunTactics x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
246+ rnf (PRunElab x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
247
247
248instance (NFData t) => NFData (PTactic' t) where
248instance (NFData t) => NFData (PTactic' t) where
249 rnf (Intro x1) = rnf x1 `seq` ()
249 rnf (Intro x1) = rnf x1 `seq` ()
src/Idris/ElabQuasiquote.hs+2−2
@@ -170,8 +170,8 @@ extractUnquotes n (PUnquote tm)
170 return (PRef (fileFC "(unquote)") n, [(n, tm)])
170 return (PRef (fileFC "(unquote)") n, [(n, tm)])
171 | otherwise = fmap (\(tm', ex) -> (PUnquote tm', ex)) $
171 | otherwise = fmap (\(tm', ex) -> (PUnquote tm', ex)) $
172 extractUnquotes (n-1) tm
172 extractUnquotes (n-1) tm
173−extractUnquotes n (PRunTactics fc tm)
173+extractUnquotes n (PRunElab fc tm)
174− = fmap (\(tm', ex) -> (PRunTactics fc tm', ex)) $ extractUnquotes n tm
174+ = fmap (\(tm', ex) -> (PRunElab fc tm', ex)) $ extractUnquotes n tm
175extractUnquotes n x = return (x, []) -- no subterms!
175extractUnquotes n x = return (x, []) -- no subterms!
176
176
177
177
src/Idris/ElabTerm.hs+6−6
@@ -220,7 +220,7 @@ goal_polymorphic =
220
220
221-- | Returns the set of declarations we need to add to complete the
221-- | Returns the set of declarations we need to add to complete the
222-- definition (most likely case blocks to elaborate) as well as
222-- definition (most likely case blocks to elaborate) as well as
223−-- declarations resulting from user tactic scripts (%runTactics)
223+-- declarations resulting from user tactic scripts (%runElab)
224elab :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->
224elab :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->
225 ElabD ()
225 ElabD ()
226elab ist info emode opts fn tm
226elab ist info emode opts fn tm
@@ -1107,11 +1107,11 @@ elab ist info emode opts fn tm
1107 delayElab $ do focus h
1107 delayElab $ do focus h
1108 dotterm
1108 dotterm
1109 elab' ina fc t
1109 elab' ina fc t
1110− elab' ina fc (PRunTactics fc' tm) =
1110+ elab' ina fc (PRunElab fc' tm) =
1111 do attack
1111 do attack
1112 n <- getNameFrom (sMN 0 "tacticScript")
1112 n <- getNameFrom (sMN 0 "tacticScript")
1113 n' <- getNameFrom (sMN 0 "tacticExpr")
1113 n' <- getNameFrom (sMN 0 "tacticExpr")
1114− let scriptTy = RApp (Var (sNS (sUN "Tactical") ["Tactical", "Reflection", "Language"])) (Var unitTy)
1114+ let scriptTy = RApp (Var (sNS (sUN "Elab") ["Elab", "Reflection", "Language"])) (Var unitTy)
1115 claim n scriptTy
1115 claim n scriptTy
1116 movelast n
1116 movelast n
1117 letbind n' scriptTy (Var n)
1117 letbind n' scriptTy (Var n)
@@ -1590,7 +1590,7 @@ case_ ind autoSolve ist fn tm = do
1590 when autoSolve solveAll
1590 when autoSolve solveAll
1591
1591
1592tacN :: String -> Name
1592tacN :: String -> Name
1593−tacN str = sNS (sUN str) ["Tactical", "Reflection", "Language"]
1593+tacN str = sNS (sUN str) ["Elab", "Reflection", "Language"]
1594
1594
1595runTactical :: FC -> Env -> Term -> ElabD ()
1595runTactical :: FC -> Env -> Term -> ElabD ()
1596runTactical fc env tm = do tm' <- eval tm
1596runTactical fc env tm = do tm' <- eval tm
@@ -1679,9 +1679,9 @@ runTactical fc env tm = do tm' <- eval tm
1679 = do errs' <- eval errs
1679 = do errs' <- eval errs
1680 parts <- reifyReportParts errs'
1680 parts <- reifyReportParts errs'
1681 lift . tfail $ ReflectionError [parts] (Msg "")
1681 lift . tfail $ ReflectionError [parts] (Msg "")
1682− | n == tacN "prim__PureTactical", [_a, tm] <- args
1682+ | n == tacN "prim__PureElab", [_a, tm] <- args
1683 = return tm
1683 = return tm
1684− | n == tacN "prim__BindTactical", [_a, _b, first, andThen] <- args
1684+ | n == tacN "prim__BindElab", [_a, _b, first, andThen] <- args
1685 = do first' <- eval first
1685 = do first' <- eval first
1686 res <- runTacTm first'
1686 res <- runTacTm first'
1687 next <- eval (App andThen res)
1687 next <- eval (App andThen res)
src/Idris/Error.hs+1−1
@@ -148,4 +148,4 @@ warnDisamb ist (PQuasiquote tm goal) = warnDisamb ist tm >>
148warnDisamb ist (PUnquote tm) = warnDisamb ist tm
148warnDisamb ist (PUnquote tm) = warnDisamb ist tm
149warnDisamb ist (PAs _ _ tm) = warnDisamb ist tm
149warnDisamb ist (PAs _ _ tm) = warnDisamb ist tm
150warnDisamb ist (PAppImpl tm _) = warnDisamb ist tm
150warnDisamb ist (PAppImpl tm _) = warnDisamb ist tm
151−warnDisamb ist (PRunTactics _ tm) = warnDisamb ist tm
151+warnDisamb ist (PRunElab _ tm) = warnDisamb ist tm
src/Idris/IBC.hs+4−4
@@ -1674,9 +1674,9 @@ instance Binary PTerm where
1674 put x2
1674 put x2
1675 PUniverse x1 -> do putWord8 38
1675 PUniverse x1 -> do putWord8 38
1676 put x1
1676 put x1
1677− PRunTactics x1 x2 -> do putWord8 39
1677+ PRunElab x1 x2 -> do putWord8 39
1678− put x1
1678+ put x1
1679− put x2
1679+ put x2
1680 PAs x1 x2 x3 -> do putWord8 40
1680 PAs x1 x2 x3 -> do putWord8 40
1681 put x1
1681 put x1
1682 put x2
1682 put x2
@@ -1809,7 +1809,7 @@ instance Binary PTerm where
1809 return (PUniverse x1)
1809 return (PUniverse x1)
1810 39 -> do x1 <- get
1810 39 -> do x1 <- get
1811 x2 <- get
1811 x2 <- get
1812− return (PRunTactics x1 x2)
1812+ return (PRunElab x1 x2)
1813 40 -> do x1 <- get
1813 40 -> do x1 <- get
1814 x2 <- get
1814 x2 <- get
1815 x3 <- get
1815 x3 <- get
src/Idris/IdrisDoc.hs+1−1
@@ -321,7 +321,7 @@ extractPTermNames (PCoerced p) = extract p
321extractPTermNames (PDisamb _ p) = extract p
321extractPTermNames (PDisamb _ p) = extract p
322extractPTermNames (PUnifyLog p) = extract p
322extractPTermNames (PUnifyLog p) = extract p
323extractPTermNames (PNoImplicits p) = extract p
323extractPTermNames (PNoImplicits p) = extract p
324−extractPTermNames (PRunTactics _ p) = extract p
324+extractPTermNames (PRunElab _ p) = extract p
325extractPTermNames _ = []
325extractPTermNames _ = []
326
326
327-- | Shorter name for extractPTermNames
327-- | Shorter name for extractPTermNames
src/Idris/ParseExpr.hs+9−9
@@ -221,7 +221,7 @@ InternalExpr ::=
221internalExpr :: SyntaxInfo -> IdrisParser PTerm
221internalExpr :: SyntaxInfo -> IdrisParser PTerm
222internalExpr syn =
222internalExpr syn =
223 unifyLog syn
223 unifyLog syn
224− <|> runTactics syn
224+ <|> runElab syn
225 <|> disamb syn
225 <|> disamb syn
226 <|> noImplicits syn
226 <|> noImplicits syn
227 <|> recordType syn
227 <|> recordType syn
@@ -498,16 +498,16 @@ unifyLog syn = do try (lchar '%' *> reserved "unifyLog")
498
498
499{- | Parses a new-style tactics expression
499{- | Parses a new-style tactics expression
500RunTactics ::=
500RunTactics ::=
501− '%' 'runTactics' SimpleExpr
501+ '%' 'runElab' SimpleExpr
502 ;
502 ;
503-}
503-}
504−runTactics :: SyntaxInfo -> IdrisParser PTerm
504+runElab :: SyntaxInfo -> IdrisParser PTerm
505−runTactics syn = do try (lchar '%' *> reserved "runTactics")
505+runElab syn = do try (lchar '%' *> reserved "runElab")
506− fc <- getFC
506+ fc <- getFC
507− tm <- simpleExpr syn
507+ tm <- simpleExpr syn
508− i <- get
508+ i <- get
509− return $ PRunTactics fc tm
509+ return $ PRunElab fc tm
510− <?> "new-style tactics expression"
510+ <?> "new-style tactics expression"
511
511
512{- | Parses a disambiguation expression
512{- | Parses a disambiguation expression
513Disamb ::=
513Disamb ::=
test/tactics001/Tactics.idr+4−4
@@ -1,6 +1,6 @@
1module Tactics
1module Tactics
2
2
3−import Language.Reflection.Tactical
3+import Language.Reflection.Elab
4
4
5import Data.Vect
5import Data.Vect
6
6
@@ -18,21 +18,21 @@ refl t x = RApp (RApp (Var (UN "Refl")) t) x
18plusZeroRightNeutralNew : (n : Nat) -> plus n 0 = n
18plusZeroRightNeutralNew : (n : Nat) -> plus n 0 = n
19plusZeroRightNeutralNew Z = Refl
19plusZeroRightNeutralNew Z = Refl
20plusZeroRightNeutralNew (S k) =
20plusZeroRightNeutralNew (S k) =
21− %runTactics (do rewriteWith `(sym $ plusZeroRightNeutralNew ~(Var "k"))
21+ %runElab (do rewriteWith `(sym $ plusZeroRightNeutralNew ~(Var "k"))
22 fill $ refl `(Nat : Type) `(S ~(Var (UN "k")))
22 fill $ refl `(Nat : Type) `(S ~(Var (UN "k")))
23 solve)
23 solve)
24
24
25plusSuccRightSuccNew : (j, k : Nat) -> plus j (S k) = S (plus j k)
25plusSuccRightSuccNew : (j, k : Nat) -> plus j (S k) = S (plus j k)
26plusSuccRightSuccNew Z k = Refl
26plusSuccRightSuccNew Z k = Refl
27plusSuccRightSuccNew (S j) k =
27plusSuccRightSuccNew (S j) k =
28− %runTactics (do rewriteWith `(sym $ plusSuccRightSuccNew ~(Var "j") ~(Var (UN "k")))
28+ %runElab (do rewriteWith `(sym $ plusSuccRightSuccNew ~(Var "j") ~(Var (UN "k")))
29 fill $ refl `(Nat : Type) `(S (S (plus ~(Var (UN "j")) ~(Var (UN "k")))))
29 fill $ refl `(Nat : Type) `(S (S (plus ~(Var (UN "j")) ~(Var (UN "k")))))
30 solve)
30 solve)
31
31
32-- Test that side effects in new tactics work
32-- Test that side effects in new tactics work
33
33
34mkDecl : ()
34mkDecl : ()
35−mkDecl = %runTactics (do declareType $ Declare (NS (UN "repUnit") ["Tactics"])
35+mkDecl = %runElab (do declareType $ Declare (NS (UN "repUnit") ["Tactics"])
36 [Implicit (UN "z") `(Nat)]
36 [Implicit (UN "z") `(Nat)]
37 `(Vect ~(Var (UN "z")) ())
37 `(Vect ~(Var (UN "z")) ())
38 fill `(() : ())
38 fill `(() : ())