ff60396 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Make apply match internal behaviour

ff60396David Raymond Christiansen11 years ago

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

compare with master

unifiedsplit

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

8import Builtins

9import Prelude.Applicative

10+import Prelude.Bool

10import Prelude.Functor

11import Prelude.Functor

11import Prelude.List

12import Prelude.List

12import Prelude.Maybe

13import Prelude.Maybe

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

100

100 prim__Solve : Elab ()

101 prim__Solve : Elab ()

101 prim__Fill : Raw -> Elab ()

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

103 prim__Focus : TTName -> Elab ()

105 prim__Focus : TTName -> Elab ()

104 prim__Unfocus : TTName -> Elab ()

106 prim__Unfocus : TTName -> Elab ()

105 prim__Attack : Elab ()

107 prim__Attack : Elab ()

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

217 fill : Raw -> Elab ()

219 fill : Raw -> Elab ()

218 fill tm = prim__Fill tm

220 fill tm = prim__Fill tm

219

221

220− ||| Fill with unification

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

221− apply : Raw -> Elab ()

239+ apply : (op : Raw) ->

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

241+ Elab (List (TTName, TTName))

222− apply tm = prim__Apply tm

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

223

265

224 ||| Move the focus to the specified hole

266 ||| Move the focus to the specified hole

225 |||

267 |||

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

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

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

564 rebind hs t = t

565

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

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

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

567apply = apply' fill

572apply = apply' fill

568match_apply = apply' match_fill

573match_apply = apply' match_fill

569

574

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

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

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

575 hs <- get_holes

580 hs <- get_holes

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

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

577− let dont = if null imps

582+ let dont = if null imps

578 then head hs : dontunify p

583 then head hs : dontunify p

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

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

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

585 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

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

1840 fill raw'

1841 returnUnit

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

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

1843+ , [raw, argSpec] <- args

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

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

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

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

1844− apply raw' []

1847+ then apply

1845− returnUnit

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+ ]

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

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

1847 = do hintStr <- eval hint

1857 = do hintStr <- eval hint

1848 case hintStr of

1858 case hintStr of

src/Idris/Reflection.hs+20

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

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

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

118

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+

119reifyReportParts :: Term -> ElabD [ErrorReportPart]

139reifyReportParts :: Term -> ElabD [ErrorReportPart]

120reifyReportParts errs =

140reifyReportParts errs =

121 case unList errs of

141 case unList errs of

test/meta002/Tacs.idr+6−2

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

181 mkIx : Fin n -> Elab ()

182 mkIx FZ = do envH <- mkEnvH

183 tH <- mkTyH

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

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

185 solve

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

187 tH <- mkTyH

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

189 argH <- gensym "arg"

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

191 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)) []

193 solve

194 focus argH

195 mkIx i

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

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

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

205 ~(Var bodyH))

206+ []

206

207

207 solve

208 solve

208 focus bodyH

209 focus bodyH

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

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

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

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

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

221 ~(Var fH) ~(Var argH))

222 ~(Var fH) ~(Var argH))

223+ []

222 solve

224 solve

223 focus fH

225 focus fH

224 mkTerm xs tm

226 mkTerm xs tm

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

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

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

231 unfocus ixH

233 unfocus ixH

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

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

235+ []

233 solve

236 solve

234 focus ixH

237 focus ixH

235 mkIx i

238 mkIx i

236 mkTerm xs UnitCon = do envH <- mkEnvH

239 mkTerm xs UnitCon = do envH <- mkEnvH

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

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

241+ []

238 solve

242 solve

239 testElab : Sigma Ty (Tm [])

243 testElab : Sigma Ty (Tm [])

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

244 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:

2When checking right hand side of testElab3:

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