ff60396 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Make apply match internal behaviour

The second argument to apply is no longer ignored. This means that we can now make use of Idris's features for solving implicits.

commitff603967cc453d6e5b01b979024b7dea148d1b84 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateMon 15 Jun 2015, 11:57 (11 years ago) parent6df52fa

6 files changed+93−12

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/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/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