5330e8a · Idris-dev · git.iko.soy

libs/base/Language/Reflection/Utils.idr+5−3

compare with master

unifiedsplit

@@ -257,14 +257,16 @@ forget tm = fe [] tm

257 LT => Nothing

258 GT => atIndex xs (n-1)

259

260− %assert_total

261 fe : List TTName -> TT -> Maybe Raw

260 fe : List TTName -> TT -> Maybe Raw

262 fe env (P _ n _) = Just $ Var n

261 fe env (P _ n _) = Just $ Var n

263− fe env (V i) = map Var (atIndex env i)

262+ fe env (V i) = [| Var (atIndex env i) |]

264− fe env (Bind n b sc) = [| RBind (pure n) (traverse (fe env) b) (fe (n::env) sc) |]

263+ fe env (Bind n b sc) = [| RBind (pure n)

264+ (assert_total $ traverse (fe env) b)

265+ (fe (n::env) sc) |]

265 fe env (App f a) = [| RApp (fe env f) (fe env a) |]

266 fe env (App f a) = [| RApp (fe env f) (fe env a) |]

266 fe env (TConst c) = Just $ RConstant c

267 fe env (TConst c) = Just $ RConstant c

267 fe env (TType i) = Just RType

268 fe env (TType i) = Just RType

269+ fe env (UType uni) = Just (RUType uni)

268 fe env Erased = Just $ RConstant Forgot

270 fe env Erased = Just $ RConstant Forgot

269

271

270instance Show Raw where

272instance Show Raw where

libs/prelude/Language/Reflection/Elab.idr+7−23

@@ -120,14 +120,12 @@ data Elab : Type -> Type where

120 prim__SourceLocation : Elab SourceLocation

121 prim__Namespace : Elab (List String)

122

123− prim__Forget : TT -> Elab Raw

124−

125 prim__Gensym : String -> Elab TTName

123 prim__Gensym : String -> Elab TTName

126

124

127 prim__Solve : Elab ()

125 prim__Solve : Elab ()

128 prim__Fill : Raw -> Elab ()

126 prim__Fill : Raw -> Elab ()

129− prim__Apply : Raw -> List (Bool, Int) -> Elab (List (TTName, TTName))

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

130− prim__MatchApply : Raw -> List (Bool, Int) -> Elab (List (TTName, TTName))

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

131 prim__Focus : TTName -> Elab ()

129 prim__Focus : TTName -> Elab ()

132 prim__Unfocus : TTName -> Elab ()

130 prim__Unfocus : TTName -> Elab ()

133 prim__Attack : Elab ()

131 prim__Attack : Elab ()

@@ -187,7 +185,7 @@ namespace Tactics

187 ||| Halt elaboration with an error

185 ||| Halt elaboration with an error

188 fail : List ErrorReportPart -> Elab a

186 fail : List ErrorReportPart -> Elab a

189 fail err = prim__Fail err

187 fail err = prim__Fail err

190−

188+

191 ||| Look up the lexical binding at the focused hole. Fails if no holes are present.

189 ||| Look up the lexical binding at the focused hole. Fails if no holes are present.

192 getEnv : Elab (List (TTName, Binder TT))

190 getEnv : Elab (List (TTName, Binder TT))

193 getEnv = prim__Env

191 getEnv = prim__Env

@@ -237,16 +235,6 @@ namespace Tactics

237 check : (env : List (TTName, Binder TT)) -> (tm : Raw) -> Elab (TT, TT)

235 check : (env : List (TTName, Binder TT)) -> (tm : Raw) -> Elab (TT, TT)

238 check env tm = prim__Check env tm

236 check env tm = prim__Check env tm

239

237

240− ||| Convert a type-annotated reflected term to its untyped

241− ||| equivalent.

242− forgetTypes : TT -> Elab Raw

243− forgetTypes tt = prim__Forget tt

244−

245− ||| Get the goal type as a Raw term. Fails if there are no holes.

246− goalType : Elab Raw

247− goalType = do g <- getGoal

248− forgetTypes (snd g)

249−

250

238

251 ||| Generate a unique name based on some hint.

239 ||| Generate a unique name based on some hint.

252 |||

240 |||

@@ -281,10 +269,8 @@ namespace Tactics

281 ||| where the Boolean states whether or not to attempt to solve

269 ||| where the Boolean states whether or not to attempt to solve

282 ||| the argument and the Int gives the priority in which to do

270 ||| the argument and the Int gives the priority in which to do

283 ||| so

271 ||| so

284− apply : (op : Raw) ->

285− (argSpec : List (Bool, Int)) ->

272+ apply : (op : Raw) -> (argSpec : List Bool) -> Elab (List TTName)

286− Elab (List (TTName, TTName))

287− apply tm argSpec = prim__Apply tm argSpec

273+ apply tm argSpec = map snd <$> prim__Apply tm argSpec

288

274

289 ||| Attempt to apply an operator to fill the current hole,

275 ||| Attempt to apply an operator to fill the current hole,

290 ||| potentially solving arugments by matching.

276 ||| potentially solving arugments by matching.

@@ -303,10 +289,8 @@ namespace Tactics

303 ||| where the Boolean states whether or not to attempt to solve

289 ||| where the Boolean states whether or not to attempt to solve

304 ||| the argument and the Int gives the priority in which to do

290 ||| the argument and the Int gives the priority in which to do

305 ||| so

291 ||| so

306− matchApply : (op : Raw) ->

292+ matchApply : (op : Raw) -> (argSpec : List Bool) -> Elab (List TTName)

307− (argSpec : List (Bool, Int)) ->

308− Elab (List (TTName, TTName))

309− matchApply tm argSpec = prim__Apply tm argSpec

293+ matchApply tm argSpec = map snd <$> prim__Apply tm argSpec

310

294

311 ||| Move the focus to the specified hole. Fails if the hole does not

295 ||| Move the focus to the specified hole. Fails if the hole does not

312 ||| exist.

296 ||| exist.

libs/pruviloj/Pruviloj/Core.idr+33−5

@@ -17,6 +17,34 @@ skip = pure ()

17try : Alternative f => f a -> f ()

18try tac = ignore tac <|> pure ()

19

20+||| Remove type information from a `TT` term, in a context. Fails if

21+||| de Bruijn indices are out of scope.

22+forget' : List TTName -> TT -> Elab Raw

23+forget' env (P nt n tm) = pure (Var n)

24+forget' env (V x) = Var <$> getName x env

25+ where getName : Int -> List a -> Elab a

26+ getName _ [] = fail [TextPart "Scope error when forget'ting types"]

27+ getName i (n::ns) = if i <= 0 then pure n else getName (i-1) ns

28+forget' env (Bind n b tm) =

29+ [| (RBind n)

30+ (assert_total $ traverse (forget' env) b)

31+ (forget' (n::env) tm) |]

32+forget' env (App tm tm') = [| RApp (forget' env tm) (forget' env tm') |]

33+forget' env (TConst c) = pure (RConstant c)

34+forget' env Erased = pure (RConstant Forgot)

35+forget' env (TType uexp) = pure RType

36+forget' env (UType uni) = pure (RUType uni)

37+

38+||| Remove type information from a `TT` term. Fails if de Bruijn

39+||| indices are out of scope.

40+forget : TT -> Elab Raw

41+forget tm = forget' [] tm

42+

43+||| Get the goal type as a Raw term. Fails if there are no holes.

44+goalType : Elab Raw

45+goalType = do g <- getGoal

46+ forget (snd g)

47+

20||| Solve the goal using the most recent applicable hypothesis

48||| Solve the goal using the most recent applicable hypothesis

21hypothesis : Elab ()

49hypothesis : Elab ()

22hypothesis =

50hypothesis =

@@ -155,7 +183,7 @@ inferType tac =

155 _ => fail [TextPart "Not infer"]

183 _ => fail [TextPart "Not infer"]

156 where

184 where

157 startInfer : Elab ()

185 startInfer : Elab ()

158− startInfer = do [_, (_, tmH)] <- apply (Var `{MkInfer}) [(True, 0), (False, 1)]

186+ startInfer = do [_, tmH] <- apply (Var `{MkInfer}) [True, False]

159 | err => fail [TextPart "Type inference failure"]

187 | err => fail [TextPart "Type inference failure"]

160 solve

188 solve

161 focus tmH

189 focus tmH

@@ -181,15 +209,15 @@ andThen first after =

181||| @ tm the term to apply to some number of goals

209||| @ tm the term to apply to some number of goals

182refine : (tm : Raw) -> Elab (List TTName)

210refine : (tm : Raw) -> Elab (List TTName)

183refine tm =

211refine tm =

184− do ty <- (snd <$> check !getEnv tm) >>= forgetTypes

212+ do ty <- (snd <$> check !getEnv tm) >>= forget

185 g <- goalType

213 g <- goalType

186

214

187 -- we don't care about negative results because it'll just fail anyway

215 -- we don't care about negative results because it'll just fail anyway

188 let argCount = minus (countPi ty) (countPi g)

216 let argCount = minus (countPi ty) (countPi g)

189− newHoles <- apply tm (replicate argCount (True, 0))

217+ newHoles <- apply tm (replicate argCount True)

190 solve

218 solve

191 actualHoles <- getHoles

219 actualHoles <- getHoles

192− return (filter (flip elem actualHoles) (map snd newHoles))

220+ return (filter (flip elem actualHoles) newHoles)

193

221

194 where countPi : Raw -> Nat

222 where countPi : Raw -> Nat

195 countPi (RBind _ (Pi _ _) body) = S (countPi body)

223 countPi (RBind _ (Pi _ _) body) = S (countPi body)

@@ -206,7 +234,7 @@ both tm n1 n2 =

206 remember n2 B; apply `(snd {a=~A} {b=~B} ~tm) []; solve

234 remember n2 B; apply `(snd {a=~A} {b=~B} ~tm) []; solve

207 where

235 where

208 isPairTy : TT -> Elab (Raw, Raw)

236 isPairTy : TT -> Elab (Raw, Raw)

209− isPairTy `((~A, ~B) : Type) = [| MkPair (forgetTypes A) (forgetTypes B) |]

237+ isPairTy `((~A, ~B) : Type) = [| MkPair (forget A) (forget B) |]

210 isPairTy tm = fail [TermPart tm, TextPart "is not a pair"]

238 isPairTy tm = fail [TermPart tm, TextPart "is not a pair"]

211

239

212||| Let-bind all results of completely destructuring nested tuples.

240||| Let-bind all results of completely destructuring nested tuples.

libs/pruviloj/Pruviloj/Derive/Eliminators.idr+17−17

@@ -65,12 +65,12 @@ mkIh info motiveName recArg argty fam =

65 for_ {b=()} argArgs $ \(n, b) =>

66 forall n (getBinderTy b)

67 let argTm : Raw = mkApp (Var recArg) (map (Var . fst) argArgs)

68− argTmTy <- forgetTypes (snd !(check !getEnv argTm))

68+ argTmTy <- forget (snd !(check !getEnv argTm))

69 argHoles <- apply (Var motiveName)

70 (replicate (length (getIndices info))

71− (True, 0) ++

71+ True ++

72− [(False,1)])

72+ [False])

73− argH <- snd <$> last argHoles

73+ argH <- last argHoles

74 focus argH

75 fill argTm; solve

76 solve -- attack

@@ -80,9 +80,9 @@ mkIh info motiveName recArg argty fam =

80elabMethodTy : TyConInfo -> TTName -> List CtorArg -> Raw -> Raw -> Elab ()

81elabMethodTy info motiveName [] res ctorApp =

82 do argHoles <- apply (Var motiveName)

83− (replicate (length (getIndices info)) (True, 0) ++

83+ (replicate (length (getIndices info)) True ++

84− [(False, 1)])

84+ [False])

85− argH <- snd <$> last argHoles

85+ argH <- last argHoles

86 focus argH; fill ctorApp; solve

87 solve

88elabMethodTy info motiveName (CtorParameter arg :: args) res ctorApp =

@@ -129,7 +129,7 @@ getElimTy info ctors =

129 [Var scrut])

130 apply (alphaRaw iren ret) []

131 solve

132− forgetTypes (fst ty)

132+ forget (fst ty)

133

134

135

@@ -167,9 +167,9 @@ getElimClause info elimn methCount (cn, args, resTy) whichCon =

167 -- We leave the RHS with a function type: motive -> method* -> res

168 -- to make it easier to map methods to constructors

169 holes <- apply paramApp (replicate (length (getIndices info))

170− (True, 0) ++

170+ True ++

171− [(False, 1)])

171+ [False])

172− scr <- snd <$> last holes

172+ scr <- last holes

173 focus scr; fill (Var scrutinee); solve

174 solve

175

@@ -204,12 +204,12 @@ getElimClause info elimn methCount (cn, args, resTy) whichCon =

204 ]

205 else return [NormalArgument n])

206

207− argHs <- apply (Var methN) (replicate (List.length argSpec) (True, 0))

207+ argHs <- apply (Var methN) (replicate (List.length argSpec) True)

208 solve

209

210 -- Now build the recursive calls for the induction hypotheses

211 for_ {a=(ElimArg, TTName)} {b=()}

212− !(zipH argSpec (map snd argHs))

212+ !(zipH argSpec argHs)

213 (\(spec, nh) =>

214 case spec of

215 NormalArgument n => do focus nh

@@ -220,12 +220,12 @@ getElimClause info elimn methCount (cn, args, resTy) whichCon =

220 attack

221 local <- intros

222 ihHs <- apply (Var elimn) $

223− replicate (length (TyConInfo.args info)) (True, 0) ++

223+ replicate (length (TyConInfo.args info)) True ++

224− [(False, 1)] ++

224+ [False] ++

225− replicate (S methCount) (True, 0)

225+ replicate (S methCount) True

226 solve -- application

227

228− let (arg::motive::methods) = map snd $ drop (length (TyConInfo.args info)) ihHs

228+ let (arg::motive::methods) = drop (length (TyConInfo.args info)) ihHs

229 focus arg

230

231 apply (mkApp (Var n) (map Var local)) []; solve

libs/pruviloj/Pruviloj/Disjoint.idr+4−4

@@ -46,8 +46,8 @@ getDisjointness l r = exists <|> declare

46 fail [ NamePart l', TextPart "and"

47 , NamePart r', TextPart "are clearly not disjoint!"

48 ]

49− (argsl, resl) <- stealBindings !(forgetTypes lty) noRenames

49+ (argsl, resl) <- stealBindings !(forget lty) noRenames

50− (argsr, resr) <- stealBindings !(forgetTypes rty) noRenames

50+ (argsr, resr) <- stealBindings !(forget rty) noRenames

51 let args = map {b=FunArg}

52 (\(n, b) => MkFunArg n (binderTy b) Implicit NotErased)

53 (argsl ++ argsr)

@@ -74,9 +74,9 @@ disjoint =

74 g <- snd <$> getGoal

75 case g of

76 `(((=) {A=~A} {B=~B} ~a ~b) -> Void) =>

77− do Just lHead <- headName <$> forgetTypes a

77+ do Just lHead <- headName <$> forget a

78 | Nothing => fail [TermPart a, TextPart "doesn't have a name at the head"]

79− Just rHead <- headName <$> forgetTypes b

79+ Just rHead <- headName <$> forget b

80 | Nothing => fail [TermPart b, TextPart "doesn't have a name at the head"]

81 [] <- refine (Var !(getDisjointness lHead rHead))

82 | _ => fail [TextPart "Didn't solve argument to disjointness lemma"]

libs/pruviloj/Pruviloj/Induction.idr+7−7

@@ -130,7 +130,7 @@ induction : Raw -> Elab (List TTName)

130induction subj =

131 do g <- goalType

132 (_, ty) <- check !getEnv subj

133− ty' <- forgetTypes ty

133+ ty' <- forget ty

134 case headName ty' of

135 Nothing => fail [TermPart ty, TextPart "is not an inductive family"]

136 Just fam =>

@@ -140,18 +140,18 @@ induction subj =

140 tydef <- lookupDatatypeExact fam

141 info <- getTyConInfo (tyConArgs tydef) (tyConRes tydef)

142 argHoles <- apply (Var elim)

143− (replicate (length (args info)) (True, 0) ++

143+ (replicate (length (args info)) True ++

144− [(False, 0), (False, 0)] ++ -- scrutinee, motive

144+ [False, False] ++ -- scrutinee, motive

145− replicate (length (constructors tydef)) (False, 1))

145+ replicate (length (constructors tydef)) False)

146 solve

147

148 -- Apply the eliminator to our scrutinee

149− scrutH <- snd <$> unsafeNth (length (args info)) argHoles

149+ scrutH <- unsafeNth (length (args info)) argHoles

150 focus scrutH

151 apply subj []

152 solve

153

154− motiveH <- snd <$> unsafeNth (length (args info) + 1) argHoles

154+ motiveH <- unsafeNth (length (args info) + 1) argHoles

155 focus motiveH; makeMotive info subj ty' g

156

157− return (map snd (drop (2 + length (tyConArgs tydef)) argHoles))

157+ return (drop (2 + length (tyConArgs tydef)) argHoles)

libs/pruviloj/Pruviloj/Injective.idr+9−9

@@ -34,8 +34,8 @@ getInjectivity cn = exists <|> declare

34 declare = do (cn', DCon _ _, cty) <- lookupTyExact cn

35 | _ => notConstructor cn

36 let fn = injName cn'

37− (args1, res1) <- stealBindings !(forgetTypes cty) noRenames

37+ (args1, res1) <- stealBindings !(forget cty) noRenames

38− (args2, res2) <- stealBindings !(forgetTypes cty) noRenames

38+ (args2, res2) <- stealBindings !(forget cty) noRenames

39 let impls1 = map (\(n, b) => MkFunArg n (binderTy b) Implicit NotErased)

40 args1

41 let impls2 = map (\(n, b) => MkFunArg n (binderTy b) Implicit NotErased)

@@ -62,11 +62,11 @@ getInjectivity cn = exists <|> declare

62

63 res

64 clause <- elabPatternClause

65− (do ((_, h)::_) <- reverse <$>

65+ (do (h::_) <- reverse <$>

66− apply (Var fn)

66+ apply (Var fn)

67− (replicate (2 * length args1)

67+ (replicate (2 * length args1)

68− (True, 0) ++

68+ True ++

69− [(False, 0)])

69+ [False])

70 | _ => fail [TextPart "Missing hole"]

71 solve

72 focus h; search)

@@ -96,7 +96,7 @@ covering public

96injective : (tm : Raw) -> (n : TTName) -> Elab ()

97injective tm n =

98 do (_, ty) <- check !getEnv tm

99− case !(forgetTypes ty) of

99+ case !(forget ty) of

100 `((=) {A=~A} {B=~B} ~x ~y) =>

101 case (headName x, headName y) of

102 (Just xHd, Just yHd) =>

@@ -112,7 +112,7 @@ injective tm n =

112 focus tmH

113 (_, _, fnTy) <- lookupTyExact fn

114

115− ((_, arg) :: _) <- reverse <$> apply (Var fn) (replicate (pred (countBinders fnTy)) (True, 0) ++ [(False,0)])

115+ (arg :: _) <- reverse <$> apply (Var fn) (replicate (pred (countBinders fnTy)) True ++ [False])

116 | _ => fail [TextPart "No hole for argument"]

117 solve

118

libs/pruviloj/Pruviloj/Internals.idr+2−2

@@ -113,13 +113,13 @@ elabPatternClause lhs rhs =

113 lhs

114 -- Convert all remaining holes to pattern variables

115 traverse_ {b=()} (\h => focus h *> patvar h) !getHoles

116− (pvars, `(MkInfer ~rhsTy ~lhsTm)) <- extractBinders <$> (forgetTypes pat)

116+ (pvars, `(MkInfer ~rhsTy ~lhsTm)) <- extractBinders <$> (forget pat)

117 | fail [TextPart "Couldn't infer type of left-hand pattern"]

118 rhsTm <- runElab (bindPatTys pvars rhsTy) $

119 do -- Introduce all the pattern variables from the LHS

120 repeatUntilFail bindPat <|> return ()

121 rhs

122− realRhs <- forgetTypes (fst rhsTm)

122+ realRhs <- forget (fst rhsTm)

123 return $ MkFunClause (bindPats pvars lhsTm) realRhs

124

125||| Introduce a unique binder name, returning it

src/Idris/Elab/Term.hs+1−4

@@ -1889,7 +1889,7 @@ runElabAction ist fc env tm ns = do tm' <- eval tm

1889 | n == tacN "prim__Apply" || n == tacN "prim__MatchApply"

1890 , [raw, argSpec] <- args

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

1892− argSpec' <- reifyList (reifyPair reifyBool reifyInt) argSpec

1892+ argSpec' <- map (\b -> (b, 0)) <$> reifyList reifyBool argSpec

1893 let op = if n == tacN "prim__Apply"

1894 then apply

1895 else match_apply

@@ -1920,9 +1920,6 @@ runElabAction ist fc env tm ns = do tm' <- eval tm

1920 fmap fst . checkClosed $

1921 rawPair (Var (reflm "TT"), Var (reflm "TT"))

1922 (reflect tm, reflect ty)

1923− | n == tacN "prim__Forget", [tt] <- args

1924− = do tt' <- reifyTT tt

1925− fmap fst . checkClosed . reflectRaw $ forget tt'

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

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

1927 = do attack

1924 = do attack

1928 returnUnit

1925 returnUnit

test/meta002/Tacs.idr+2

@@ -13,6 +13,8 @@ import Language.Reflection

13import Language.Reflection.Errors

14import Language.Reflection.Utils

15

16+import Pruviloj.Core

17+

16%default total

18%default total

17

19

18-- Tactics can now query the elaborator and bind variables

20-- Tactics can now query the elaborator and bind variables

test/meta002/expected+1−1

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

1−Tacs.idr:296:15:

1+Tacs.idr:298:15:

2When checking right hand side of testElab3:

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

test/meta002/run+1−1

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

1#!/usr/bin/env bash

2−idris $@ --nocolour --check --consolewidth 70 Tacs.idr

2+idris $@ -p pruviloj --nocolour --check --consolewidth 70 Tacs.idr

3rm -f *.ibc