c5f5dab · Idris-dev · git.iko.soy

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

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

257257 LT => Nothing

258258 GT => atIndex xs (n-1)

259259

260− %assert_total

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

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

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

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

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

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

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

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

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

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

267268 fe env (TType i) = Just RType

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

268270 fe env Erased = Just $ RConstant Forgot

269271

270272instance Show Raw where

libs/prelude/Language/Reflection/Elab.idr+13−26

@@ -115,19 +115,17 @@ data Elab : Type -> Type where

115115 prim__LookupTy : TTName -> Elab (List (TTName, NameType, TT))

116116 prim__LookupDatatype : TTName -> Elab (List Datatype)

117117

118− prim__Check : Raw -> Elab (TT, TT)

118+ prim__Check : List (TTName, Binder TT) -> Raw -> Elab (TT, TT)

119119

120120 prim__SourceLocation : Elab SourceLocation

121121 prim__Namespace : Elab (List String)

122122

123− prim__Forget : TT -> Elab Raw

124−

125123 prim__Gensym : String -> Elab TTName

126124

127125 prim__Solve : Elab ()

128126 prim__Fill : Raw -> Elab ()

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

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

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

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

131129 prim__Focus : TTName -> Elab ()

132130 prim__Unfocus : TTName -> Elab ()

133131 prim__Attack : Elab ()

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

187185 ||| Halt elaboration with an error

188186 fail : List ErrorReportPart -> Elab a

189187 fail err = prim__Fail err

190−

188+

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

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

193191 getEnv = prim__Env

@@ -231,18 +229,11 @@ namespace Tactics

231229 xs => fail [TextPart "More than one datatype named", NamePart n]

232230

233231 ||| Attempt to type-check a term, getting back itself and its type.

234− check : (tm : Raw) -> Elab (TT, TT)

235− check tm = prim__Check tm

236−

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

238− ||| equivalent.

239− forgetTypes : TT -> Elab Raw

240− forgetTypes tt = prim__Forget tt

241−

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

243− goalType : Elab Raw

244− goalType = do g <- getGoal

245− forgetTypes (snd g)

232+ |||

233+ ||| @ env the environment within which to check the type

234+ ||| @ tm the term to check

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

236+ check env tm = prim__Check env tm

246237

247238

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

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

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

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

280271 ||| so

281− apply : (op : Raw) ->

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

283− Elab (List (TTName, TTName))

284− apply tm argSpec = prim__Apply tm argSpec

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

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

285274

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

287276 ||| potentially solving arugments by matching.

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

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

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

302291 ||| so

303− matchApply : (op : Raw) ->

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

305− Elab (List (TTName, TTName))

306− matchApply tm argSpec = prim__Apply tm argSpec

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

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

307294

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

309296 ||| exist.

libs/pruviloj/Pruviloj/Core.idr+34−6

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

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

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

1919

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+

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

2149hypothesis : Elab ()

2250hypothesis =

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

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

156184 where

157185 startInfer : Elab ()

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

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

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

160188 solve

161189 focus tmH

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

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

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

183211refine tm =

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

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

185213 g <- goalType

186214

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

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

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

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

190218 solve

191219 actualHoles <- getHoles

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

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

193221

194222 where countPi : Raw -> Nat

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

@@ -201,12 +229,12 @@ refine tm =

201229both : Raw -> TTName -> TTName -> Elab ()

202230both tm n1 n2 =

203231 do -- We don't know that the term is canonical, so let-bind projections applied to it

204− (A, B) <- isPairTy (snd !(check tm))

232+ (A, B) <- isPairTy (snd !(check !getEnv tm))

205233 remember n1 A; apply `(fst {a=~A} {b=~B} ~tm) []; solve

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

207235 where

208236 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) |]

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

211239

212240||| 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 =

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

6666 forall n (getBinderTy b)

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

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

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

6969 argHoles <- apply (Var motiveName)

7070 (replicate (length (getIndices info))

71− (True, 0) ++

72− [(False,1)])

73− argH <- snd <$> last argHoles

71+ True ++

72+ [False])

73+ argH <- last argHoles

7474 focus argH

7575 fill argTm; solve

7676 solve -- attack

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

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

8181elabMethodTy info motiveName [] res ctorApp =

8282 do argHoles <- apply (Var motiveName)

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

84− [(False, 1)])

85− argH <- snd <$> last argHoles

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

84+ [False])

85+ argH <- last argHoles

8686 focus argH; fill ctorApp; solve

8787 solve

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

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

129129 [Var scrut])

130130 apply (alphaRaw iren ret) []

131131 solve

132− forgetTypes (fst ty)

132+ forget (fst ty)

133133

134134

135135

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

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

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

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

170− (True, 0) ++

171− [(False, 1)])

172− scr <- snd <$> last holes

170+ True ++

171+ [False])

172+ scr <- last holes

173173 focus scr; fill (Var scrutinee); solve

174174 solve

175175

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

204204 ]

205205 else return [NormalArgument n])

206206

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

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

208208 solve

209209

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

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

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

212+ !(zipH argSpec argHs)

213213 (\(spec, nh) =>

214214 case spec of

215215 NormalArgument n => do focus nh

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

220220 attack

221221 local <- intros

222222 ihHs <- apply (Var elimn) $

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

224− [(False, 1)] ++

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

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

224+ [False] ++

225+ replicate (S methCount) True

226226 solve -- application

227227

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

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

229229 focus arg

230230

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

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

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

4646 fail [ NamePart l', TextPart "and"

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

4848 ]

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

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

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

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

5151 let args = map {b=FunArg}

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

5353 (argsl ++ argsr)

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

7474 g <- snd <$> getGoal

7575 case g of

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

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

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

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

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

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

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

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

@@ -129,8 +129,8 @@ public

129129induction : Raw -> Elab (List TTName)

130130induction subj =

131131 do g <- goalType

132− (_, ty) <- check subj

133− ty' <- forgetTypes ty

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

133+ ty' <- forget ty

134134 case headName ty' of

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

136136 Just fam =>

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

140140 tydef <- lookupDatatypeExact fam

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

142142 argHoles <- apply (Var elim)

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

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

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

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

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

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

146146 solve

147147

148148 -- Apply the eliminator to our scrutinee

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

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

150150 focus scrutH

151151 apply subj []

152152 solve

153153

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

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

155155 focus motiveH; makeMotive info subj ty' g

156156

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

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

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

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

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

3535 | _ => notConstructor cn

3636 let fn = injName cn'

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

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

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

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

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

4040 args1

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

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

6262

6363 res

6464 clause <- elabPatternClause

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

66− apply (Var fn)

67− (replicate (2 * length args1)

68− (True, 0) ++

69− [(False, 0)])

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

66+ apply (Var fn)

67+ (replicate (2 * length args1)

68+ True ++

69+ [False])

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

7171 solve

7272 focus h; search)

@@ -95,8 +95,8 @@ countBinders _ = Z

9595covering public

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

9797injective tm n =

98− do (_, ty) <- check tm

99− case !(forgetTypes ty) of

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

99+ case !(forget ty) of

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

101101 case (headName x, headName y) of

102102 (Just xHd, Just yHd) =>

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

112112 focus tmH

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

114114

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

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

117117 solve

118118

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

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

113113 lhs

114114 -- Convert all remaining holes to pattern variables

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

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

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

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

118118 rhsTm <- runElab (bindPatTys pvars rhsTy) $

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

120120 repeatUntilFail bindPat <|> return ()

121121 rhs

122− realRhs <- forgetTypes (fst rhsTm)

122+ realRhs <- forget (fst rhsTm)

123123 return $ MkFunClause (bindPats pvars lhsTm) realRhs

124124

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

src/Idris/Core/WHNF.hs+8−8

@@ -1,7 +1,7 @@

11{-# LANGUAGE PatternGuards #-}

22{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

33

4−-- Reduction to Weak Head Normal Form

4+-- | Reduction to Weak Head Normal Form

55module Idris.Core.WHNF(whnf, WEnv) where

66

77import Idris.Core.TT

@@ -11,7 +11,7 @@ import qualified Idris.Core.Evaluate as Evaluate

1111

1212import Debug.Trace

1313

14−-- A stack entry consists of a term and the environment it is to be

14+-- | A stack entry consists of a term and the environment it is to be

1515-- evaluated in (i.e. it's a thunk)

1616type StackEntry = (Term, WEnv)

1717data WEnv = WEnv Int -- number of free variables

@@ -20,17 +20,17 @@ data WEnv = WEnv Int -- number of free variables

2020

2121type Stack = [StackEntry]

2222

23−-- A WHNF is a top level term evaluated in the empty environment. It is

23+-- | A WHNF is a top level term evaluated in the empty environment. It is

2424-- always headed by either an irreducible expression, i.e. a constructor,

2525-- a lambda, a constant, or a postulate

26−

26+--

2727-- Every 'Term' or 'Type' in this structure is associated with the

2828-- environment it was encountered in, so that when we quote back to a term

2929-- we get the substitutions right.

3030

31−data WHNF = WDCon Int Int Bool Name (Type, WEnv) -- data constructor

32− | WTCon Int Int Name (Type, WEnv) -- type constructor

33− | WPRef Name (Type, WEnv) -- irreducible global (e.g. a postulate)

31+data WHNF = WDCon Int Int Bool Name (Type, WEnv) -- ^ data constructor

32+ | WTCon Int Int Name (Type, WEnv) -- ^ type constructor

33+ | WPRef Name (Type, WEnv) -- ^irreducible global (e.g. a postulate)

3434 | WBind Name (Binder Term) (Term, WEnv)

3535 | WApp WHNF (Term, WEnv)

3636 | WConstant Const

@@ -40,7 +40,7 @@ data WHNF = WDCon Int Int Bool Name (Type, WEnv) -- data constructor

4040 | WErased

4141 | WImpossible

4242

43−-- Reduce a *closed* term to weak head normal form.

43+-- | Reduce a *closed* term to weak head normal form.

4444whnf :: Context -> Term -> Term

4545whnf ctxt tm = quote (do_whnf ctxt (WEnv 0 []) tm)

4646

src/Idris/Elab/Term.hs+5−8

@@ -1884,12 +1884,12 @@ runElabAction ist fc env tm ns = do tm' <- eval tm

18841884 try' (runTacTm first') (runTacTm alt') True

18851885 | n == tacN "prim__Fill", [raw] <- args

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

1887− fill raw'

1887+ apply raw' []

18881888 returnUnit

18891889 | n == tacN "prim__Apply" || n == tacN "prim__MatchApply"

18901890 , [raw, argSpec] <- args

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

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

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

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

18941894 then apply

18951895 else match_apply

@@ -1912,17 +1912,14 @@ runElabAction ist fc env tm ns = do tm' <- eval tm

19121912 ty' <- reifyRaw ty

19131913 claim n' ty'

19141914 returnUnit

1915− | n == tacN "prim__Check", [raw] <- args

1916− = do raw' <- reifyRaw =<< eval raw

1915+ | n == tacN "prim__Check", [env', raw] <- args

1916+ = do env <- reifyEnv env'

1917+ raw' <- reifyRaw =<< eval raw

19171918 ctxt <- get_context

1918− env <- get_env

19191919 (tm, ty) <- lift $ check ctxt env raw'

19201920 fmap fst . checkClosed $

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

19221922 (reflect tm, reflect ty)

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

1924− = do tt' <- reifyTT tt

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

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

19271924 = do attack

19281925 returnUnit

test/basic016/run+1−1

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

11#!/usr/bin/env bash

2−idris $@ CycleA.idr --check

2+idris $@ CycleA.idr --consolewidth 80 --nocolour --check

33rm -f *.ibc

test/meta002/Tacs.idr+2

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

1313import Language.Reflection.Errors

1414import Language.Reflection.Utils

1515

16+import Pruviloj.Core

17+

1618%default total

1719

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

22When checking right hand side of testElab3:

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

test/meta002/run+1−1

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

11#!/usr/bin/env bash

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

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

33rm -f *.ibc