6d7da92 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #2378 from david-christiansen/wip/tactical

Latest Elab reflection updates

commit6d7da9261878f521c5747923ab6328425814cc22 authorDavid Christiansen <david@davidchristiansen.dk> dateMon 15 Jun 2015, 23:01 (11 years ago) parentecab241 ff60396

7 files changed+93−14

compare with master

unifiedsplit

libs/prelude/Language/Reflection/Elab.idr+46−4 src/Idris/Core/Elaborate.hs+7−2 src/Idris/Elab/Term.hs+13−3 src/Idris/Elab/Utils.hs−2 src/Idris/Reflection.hs+20 test/meta002/Tacs.idr+6−2 test/meta002/expected+1−1

libs/prelude/Language/Reflection/Elab.idr+46−4

@@ -7,6 +7,7 @@ module Language.Reflection.Elab

88import Builtins

99import Prelude.Applicative

10+import Prelude.Bool

1011import Prelude.Functor

1112import Prelude.List

1213import Prelude.Maybe

@@ -99,7 +100,8 @@ data Elab : Type -> Type where

99100

100101 prim__Solve : Elab ()

101102 prim__Fill : Raw -> Elab ()

102− prim__Apply : Raw -> Elab ()

103+ prim__Apply : Raw -> List (Bool, Int) -> Elab (List (TTName, TTName))

104+ prim__MatchApply : Raw -> List (Bool, Int) -> Elab (List (TTName, TTName))

103105 prim__Focus : TTName -> Elab ()

104106 prim__Unfocus : TTName -> Elab ()

105107 prim__Attack : Elab ()

@@ -217,9 +219,49 @@ namespace Tactics

217219 fill : Raw -> Elab ()

218220 fill tm = prim__Fill tm

219221

220− ||| Fill with unification

221− apply : Raw -> Elab ()

222− apply tm = prim__Apply tm

222+ ||| Attempt to apply an operator to fill the current hole,

223+ ||| potentially solving arugments by unification.

224+ |||

225+ ||| The return value is a list of pairs of names, one for each input

226+ ||| argument. The first projection of these pairs is the original

227+ ||| name of the argument, from the type declaration, and the second

228+ ||| projection is the hole into which it is placed.

229+ |||

230+ ||| Note that not all of the returned hole names still exist, as

231+ ||| they may have been solved.

232+ |||

233+ ||| @ op the term to apply

234+ |||

235+ ||| @ argSpec instructions for finding the arguments to the term,

236+ ||| where the Boolean states whether or not to attempt to solve

237+ ||| the argument and the Int gives the priority in which to do

238+ ||| so

239+ apply : (op : Raw) ->

240+ (argSpec : List (Bool, Int)) ->

241+ Elab (List (TTName, TTName))

242+ apply tm argSpec = prim__Apply tm argSpec

243+

244+ ||| Attempt to apply an operator to fill the current hole,

245+ ||| potentially solving arugments by matching.

246+ |||

247+ ||| The return value is a list of pairs of names, one for each input

248+ ||| argument. The first projection of these pairs is the original

249+ ||| name of the argument, from the type declaration, and the second

250+ ||| projection is the hole into which it is placed.

251+ |||

252+ ||| Note that not all of the returned hole names still exist, as

253+ ||| they may have been solved.

254+ |||

255+ ||| @ op the term to apply

256+ |||

257+ ||| @ argSpec instructions for finding the arguments to the term,

258+ ||| where the Boolean states whether or not to attempt to solve

259+ ||| the argument and the Int gives the priority in which to do

260+ ||| so

261+ matchApply : (op : Raw) ->

262+ (argSpec : List (Bool, Int)) ->

263+ Elab (List (TTName, TTName))

264+ matchApply tm argSpec = prim__Apply tm argSpec

223265

224266 ||| Move the focus to the specified hole

225267 |||

src/Idris/Core/Elaborate.hs+7−2

@@ -563,7 +563,12 @@ prepare_apply fn imps =

563563 rebind hs (App s f a) = App s (rebind hs f) (rebind hs a)

564564 rebind hs t = t

565565

566−apply, match_apply :: Raw -> [(Bool, Int)] -> Elab' aux [(Name, Name)]

566+-- | Apply an operator, solving some arguments by unification or matching.

567+apply, match_apply :: Raw -- ^ The operator to apply

568+ -> [(Bool, Int)] -- ^ For each argument, whether to

569+ -- attempt to solve it and the

570+ -- priority in which to do so

571+ -> Elab' aux [(Name, Name)]

567572apply = apply' fill

568573match_apply = apply' match_fill

569574

@@ -574,7 +579,7 @@ apply' fillt fn imps =

574579 -- (remove from unified list before calling end_unify)

575580 hs <- get_holes

576581 ES (p, a) s prev <- get

577− let dont = if null imps

582+ let dont = if null imps

578583 then head hs : dontunify p

579584 else getNonUnify (head hs : dontunify p) imps args

580585 let (n, hunis) = -- trace ("AVOID UNIFY: " ++ show (fn, dont)) $

src/Idris/Elab/Term.hs+13−3

@@ -1839,10 +1839,20 @@ runElabAction ist fc env tm ns = do tm' <- eval tm

18391839 = do raw' <- reifyRaw =<< eval raw

18401840 fill raw'

18411841 returnUnit

1842− | n == tacN "prim__Apply", [raw] <- args

1842+ | n == tacN "prim__Apply" || n == tacN "prim__MatchApply"

1843+ , [raw, argSpec] <- args

18431844 = do raw' <- reifyRaw =<< eval raw

1844− apply raw' []

1845− returnUnit

1845+ argSpec' <- reifyList (reifyPair reifyBool reifyInt) argSpec

1846+ let op = if n == tacN "prim__Apply"

1847+ then apply

1848+ else match_apply

1849+ ns <- op raw' argSpec'

1850+ fmap fst . checkClosed $

1851+ rawList (rawPairTy (Var $ reflm "TTName") (Var $ reflm "TTName"))

1852+ [ rawPair (Var $ reflm "TTName", Var $ reflm "TTName")

1853+ (reflectName n1, reflectName n2)

1854+ | (n1, n2) <- ns

1855+ ]

18461856 | n == tacN "prim__Gensym", [hint] <- args

18471857 = do hintStr <- eval hint

18481858 case hintStr of

src/Idris/Elab/Utils.hs−2

@@ -66,8 +66,6 @@ inaccessibleImps _ _ _ = []

6666

6767-- | Get the list of (index, name) of inaccessible arguments from the type.

6868inaccessibleArgs :: Int -> PTerm -> [(Int, Name)]

69−inaccessibleArgs i (PPi (Imp _ _ _ _) n _ Placeholder t)

70− = (i,n) : inaccessibleArgs (i+1) t -- unbound implicit

7169inaccessibleArgs i (PPi plicity n _ ty t)

7270 | InaccessibleArg `elem` pargopts plicity

7371 = (i,n) : inaccessibleArgs (i+1) t -- an .{erased : Implicit}

src/Idris/Reflection.hs+20

@@ -116,6 +116,26 @@ reifyApp ist t [errs]

116116 | t == reflm "Fail" = fmap TFail (reifyReportParts errs)

117117reifyApp _ f args = fail ("Unknown tactic " ++ show (f, args)) -- shouldn't happen

118118

119+reifyBool :: Term -> ElabD Bool

120+reifyBool (P _ n _) | n == sNS (sUN "True") ["Bool", "Prelude"] = return True

121+ | n == sNS (sUN "False") ["Bool", "Prelude"] = return False

122+reifyBool tm = fail $ "Not a Boolean: " ++ show tm

123+

124+reifyInt :: Term -> ElabD Int

125+reifyInt (Constant (I i)) = return i

126+reifyInt tm = fail $ "Not an Int: " ++ show tm

127+

128+reifyPair :: (Term -> ElabD a) -> (Term -> ElabD b) -> Term -> ElabD (a, b)

129+reifyPair left right (App _ (App _ (App _ (App _ (P _ n _) _) _) x) y)

130+ | n == pairCon = liftM2 (,) (left x) (right y)

131+reifyPair left right tm = fail $ "Not a pair: " ++ show tm

132+

133+reifyList :: (Term -> ElabD a) -> Term -> ElabD [a]

134+reifyList getElt lst =

135+ case unList lst of

136+ Nothing -> fail "Couldn't reify a list"

137+ Just xs -> mapM getElt xs

138+

119139reifyReportParts :: Term -> ElabD [ErrorReportPart]

120140reifyReportParts errs =

121141 case unList errs of

test/meta002/Tacs.idr+6−2

@@ -181,7 +181,7 @@ namespace STLC

181181 mkIx : Fin n -> Elab ()

182182 mkIx FZ = do envH <- mkEnvH

183183 tH <- mkTyH

184− apply `(Z {t=~(Var tH)} {env=~(Var envH)})

184+ apply `(Z {t=~(Var tH)} {env=~(Var envH)}) []

185185 solve

186186 mkIx (FS i) = do envH <- mkEnvH

187187 tH <- mkTyH

@@ -189,7 +189,7 @@ namespace STLC

189189 argH <- gensym "arg"

190190 claim argH `(Ix ~(Var envH) ~(Var tH))

191191 unfocus argH

192− apply `(S {env=~(Var envH)} {t=~(Var tH)} {t'=~(Var vH)} ~(Var argH))

192+ apply `(S {env=~(Var envH)} {t=~(Var tH)} {t'=~(Var vH)} ~(Var argH)) []

193193 solve

194194 focus argH

195195 mkIx i

@@ -203,6 +203,7 @@ namespace STLC

203203 apply `(Lam {env=~(Var envH)}

204204 {t=~(Var tH)} {t'=~(Var tH')}

205205 ~(Var bodyH))

206+ []

206207

207208 solve

208209 focus bodyH

@@ -219,6 +220,7 @@ namespace STLC

219220 apply `(App {env=~(Var envH)}

220221 {t=~(Var tH)} {t'=~(Var tH')}

221222 ~(Var fH) ~(Var argH))

223+ []

222224 solve

223225 focus fH

224226 mkTerm xs tm

@@ -230,11 +232,13 @@ namespace STLC

230232 claim ixH `(Ix ~(Var envH) ~(Var tH))

231233 unfocus ixH

232234 apply `(Var {env=~(Var envH)} {t=~(Var tH)} ~(Var ixH))

235+ []

233236 solve

234237 focus ixH

235238 mkIx i

236239 mkTerm xs UnitCon = do envH <- mkEnvH

237240 apply `(UnitCon {env=~(Var envH)})

241+ []

238242 solve

239243 testElab : Sigma Ty (Tm [])

240244 testElab = %runElab (elaborateSTLC (App (Lam "x" UnitCon) UnitCon))

test/meta002/expected+1−1

@@ -1,3 +1,3 @@

1−Tacs.idr:247:15:

1+Tacs.idr:251:15:

22When checking right hand side of testElab3:

33Unifying ty and ARR ty t would lead to infinite value