git.iko.soy/Idris-dev
on master help sign in
Add environment argument to Elab.Tactics.check

Now, type checking can be performed in arbitrary environments.

commit1edba410d475a9b661c2bddb1bc677fe2d763bd9 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateThu 15 Oct 2015, 14:42 (11 years ago) parent68c519e
6 files changed+14−11
compare with master
unifiedsplit
libs/prelude/Language/Reflection/Elab.idr+6−3 libs/pruviloj/Pruviloj/Core.idr+2−2 libs/pruviloj/Pruviloj/Derive/Eliminators.idr+1−1 libs/pruviloj/Pruviloj/Induction.idr+1−1 libs/pruviloj/Pruviloj/Injective.idr+1−1 src/Idris/Elab/Term.hs+3−3
libs/prelude/Language/Reflection/Elab.idr+6−3
@@ -115,7 +115,7 @@ 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)
@@ -231,8 +231,11 @@ namespace Tactics
231231 xs => fail [TextPart "More than one datatype named", NamePart n]
232232
233233 ||| 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
234+ |||
235+ ||| @ env the environment within which to check the type
236+ ||| @ tm the term to check
237+ check : (env : List (TTName, Binder TT)) -> (tm : Raw) -> Elab (TT, TT)
238+ check env tm = prim__Check env tm
236239
237240 ||| Convert a type-annotated reflected term to its untyped
238241 ||| equivalent.
libs/pruviloj/Pruviloj/Core.idr+2−2
@@ -181,7 +181,7 @@ andThen first after =
181181||| @ tm the term to apply to some number of goals
182182refine : (tm : Raw) -> Elab (List TTName)
183183refine tm =
184− do ty <- (snd <$> check tm) >>= forgetTypes
184+ do ty <- (snd <$> check !getEnv tm) >>= forgetTypes
185185 g <- goalType
186186
187187 -- we don't care about negative results because it'll just fail anyway
@@ -201,7 +201,7 @@ refine tm =
201201both : Raw -> TTName -> TTName -> Elab ()
202202both tm n1 n2 =
203203 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))
205205 remember n1 A; apply `(fst {a=~A} {b=~B} ~tm) []; solve
206206 remember n2 B; apply `(snd {a=~A} {b=~B} ~tm) []; solve
207207 where
libs/pruviloj/Pruviloj/Derive/Eliminators.idr+1−1
@@ -65,7 +65,7 @@ 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 <- forgetTypes (snd !(check !getEnv argTm))
6969 argHoles <- apply (Var motiveName)
7070 (replicate (length (getIndices info))
7171 (True, 0) ++
libs/pruviloj/Pruviloj/Induction.idr+1−1
@@ -129,7 +129,7 @@ public
129129induction : Raw -> Elab (List TTName)
130130induction subj =
131131 do g <- goalType
132− (_, ty) <- check subj
132+ (_, ty) <- check !getEnv subj
133133 ty' <- forgetTypes ty
134134 case headName ty' of
135135 Nothing => fail [TermPart ty, TextPart "is not an inductive family"]
libs/pruviloj/Pruviloj/Injective.idr+1−1
@@ -95,7 +95,7 @@ countBinders _ = Z
9595covering public
9696injective : (tm : Raw) -> (n : TTName) -> Elab ()
9797injective tm n =
98− do (_, ty) <- check tm
98+ do (_, ty) <- check !getEnv tm
9999 case !(forgetTypes ty) of
100100 `((=) {A=~A} {B=~B} ~x ~y) =>
101101 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
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"))