1edba41 · Idris-dev · git.iko.soy

libs/prelude/Language/Reflection/Elab.idr+6−3

compare with master

unifiedsplit

@@ -115,7 +115,7 @@ data Elab : Type -> Type where

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

116 prim__LookupDatatype : TTName -> Elab (List Datatype)

117

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

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

119

120 prim__SourceLocation : Elab SourceLocation

121 prim__Namespace : Elab (List String)

@@ -231,8 +231,11 @@ namespace Tactics

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

232

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

234+ |||

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

236+ ||| @ tm the term to check

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

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

235− check tm = prim__Check tm

238+ check env tm = prim__Check env tm

236

239

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

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

238 ||| equivalent.

241 ||| equivalent.

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

@@ -181,7 +181,7 @@ andThen first after =

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

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

183refine tm =

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

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

185 g <- goalType

186

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

@@ -201,7 +201,7 @@ refine tm =

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

202both tm n1 n2 =

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

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

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

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

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

207 where

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

@@ -65,7 +65,7 @@ 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 argTm))

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

69 argHoles <- apply (Var motiveName)

70 (replicate (length (getIndices info))

71 (True, 0) ++

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

@@ -129,7 +129,7 @@ public

129induction : Raw -> Elab (List TTName)

130induction subj =

131 do g <- goalType

132− (_, ty) <- check subj

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

133 ty' <- forgetTypes ty

134 case headName ty' of

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

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

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

95covering public

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

97injective tm n =

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

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

99 case !(forgetTypes ty) of

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

101 case (headName x, headName y) of

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

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

1912 ty' <- reifyRaw ty

1913 claim n' ty'

1914 returnUnit

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

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

1916+ = do env <- reifyEnv env'

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

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

1917 ctxt <- get_context

1918 ctxt <- get_context

1918− env <- get_env

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

1920 fmap fst . checkClosed $

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