git.iko.soy/Idris-dev
on master help sign in
Reflected elab: look up in global context
f91e07cDavid Raymond Christiansen
libs/prelude/Language/Reflection/Elab.idr+4
compare with master
unifiedsplit
@@ -36,6 +36,7 @@ data Elab : Type -> Type where
36 prim__Goal : Elab (TTName, TT)
36 prim__Goal : Elab (TTName, TT)
37 prim__Holes : Elab (List TTName)
37 prim__Holes : Elab (List TTName)
38 prim__Guess : Elab (Maybe TT)
38 prim__Guess : Elab (Maybe TT)
39+ prim__LookupTy : TTName -> Elab (List (TTName, NameType, TT))
39
40
40 prim__SourceLocation : Elab SourceLocation
41 prim__SourceLocation : Elab SourceLocation
41
42
@@ -96,6 +97,9 @@ getHoles = prim__Holes
96getGuess : Elab (Maybe TT)
97getGuess : Elab (Maybe TT)
97getGuess = prim__Guess
98getGuess = prim__Guess
98
99
100+lookupTy : TTName -> Elab (List (TTName, NameType, TT))
101+lookupTy n = prim__LookupTy n
102+
99forgetTypes : TT -> Elab Raw
103forgetTypes : TT -> Elab Raw
100forgetTypes tt = prim__Forget tt
104forgetTypes tt = prim__Forget tt
101
105
src/Idris/ElabTerm.hs+22
@@ -1650,6 +1650,28 @@ runTactical fc env tm = do tm' <- eval tm
1650 else fmap fst . get_type_val $
1650 else fmap fst . get_type_val $
1651 RApp (Var (sNS (sUN "Nothing") ["Maybe", "Prelude"]))
1651 RApp (Var (sNS (sUN "Nothing") ["Maybe", "Prelude"]))
1652 (Var (reflm "TT"))
1652 (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
1653 | n == tacN "prim__SourceLocation", [] <- args
1675 | n == tacN "prim__SourceLocation", [] <- args
1654 = fmap fst . get_type_val $
1676 = fmap fst . get_type_val $
1655 reflectFC fc
1677 reflectFC fc