git.iko.soy/Idris-dev
on master help sign in
Reflected elab: look up in global context
commitf91e07c4185c5d12fbb486953db5a455ceff7df2 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateThu 16 Apr 2015, 13:03 (12 years ago) parenteed700a
2 files changed+26
compare with master
unifiedsplit
libs/prelude/Language/Reflection/Elab.idr+4 src/Idris/ElabTerm.hs+22
libs/prelude/Language/Reflection/Elab.idr+4
@@ -36,6 +36,7 @@ data Elab : Type -> Type where
3636 prim__Goal : Elab (TTName, TT)
3737 prim__Holes : Elab (List TTName)
3838 prim__Guess : Elab (Maybe TT)
39+ prim__LookupTy : TTName -> Elab (List (TTName, NameType, TT))
3940
4041 prim__SourceLocation : Elab SourceLocation
4142
@@ -96,6 +97,9 @@ getHoles = prim__Holes
9697getGuess : Elab (Maybe TT)
9798getGuess = prim__Guess
9899
100+lookupTy : TTName -> Elab (List (TTName, NameType, TT))
101+lookupTy n = prim__LookupTy n
102+
99103forgetTypes : TT -> Elab Raw
100104forgetTypes tt = prim__Forget tt
101105
src/Idris/ElabTerm.hs+22
@@ -1650,6 +1650,28 @@ runTactical fc env tm = do tm' <- eval tm
16501650 else fmap fst . get_type_val $
16511651 RApp (Var (sNS (sUN "Nothing") ["Maybe", "Prelude"]))
16521652 (Var (reflm "TT"))
1653+ | n == tacN "prim__LookupTy", [n] <- args
1654+ = do n' <- reifyTTName n
1655+ ctxt <- get_context
1656+ let getNameTypeAndType = \case Function ty _ -> (Ref, ty)
1657+ TyDecl nt ty -> (nt, ty)
1658+ Operator ty _ _ -> (Ref, ty)
1659+ CaseOp _ ty _ _ _ _ -> (Ref, ty)
1660+ -- Idris tuples nest to the right
1661+ reflectTriple (x, y, z) =
1662+ raw_apply (Var pairCon) [ Var (reflm "TTName")
1663+ , raw_apply (Var pairTy) [Var (reflm "NameType"), Var (reflm "TT")]
1664+ , x
1665+ , raw_apply (Var pairCon) [ Var (reflm "NameType"), Var (reflm "TT")
1666+ , y, z]]
1667+ let defs = [ reflectTriple (reflectName n, reflectNameType nt, reflect ty)
1668+ | (n, def) <- lookupNameDef n' ctxt
1669+ , let (nt, ty) = getNameTypeAndType def ]
1670+ fmap fst . get_type_val $
1671+ rawList (raw_apply (Var pairTy) [ Var (reflm "TTName")
1672+ , raw_apply (Var pairTy) [ Var (reflm "NameType")
1673+ , Var (reflm "TT")]])
1674+ defs
16531675 | n == tacN "prim__SourceLocation", [] <- args
16541676 = fmap fst . get_type_val $
16551677 reflectFC fc